yadunut/nus
1
0
Fork 0
Code Issues Pull Requests Actions Projects Releases Wiki Activity

feat: fix about_fetch_decode_execute_loop

Browse Source
This commit is contained in:
Yadunand Prem 2024-04-27 17:22:01 +08:00
parent ca30dc084a
commit 0758fad858
No known key found for this signature in database
1 changed files with 36 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

53
cs3234/labs/term-project.v
View File

@ -659,25 +659,44 @@ Qed.
Proposition about_fetch_decode_execute_loop : Proposition about_fetch_decode_execute_loop :
forall (bci1s bci2s : list byte_code_instruction) forall (bci1s bci2s : list byte_code_instruction)
(ds ds' : data_stack), (ds : data_stack),
fetch_decode_execute_loop bci1s ds = OK ds' -> (forall (ds' : data_stack),
fetch_decode_execute_loop (bci1s ++ bci2s) ds = fetch_decode_execute_loop bci1s ds = OK ds' ->
fetch_decode_execute_loop bci2s (ds'). fetch_decode_execute_loop (bci1s ++ bci2s) ds = fetch_decode_execute_loop bci2s (ds'))
/\
(forall (s : string),
fetch_decode_execute_loop bci1s ds = KO s ->
fetch_decode_execute_loop (bci1s ++ bci2s) ds = KO s).
Proof. Proof.
intros bci1s. intros bci1s bci2s.
induction bci1s as [ | bci bci1s' IHbci1s' ]; intros bci2s ds ds' H_fdel. induction bci1s as [ | bci bci1s' IHbci1s' ]; intros ds.
- rewrite -> fold_unfold_list_append_nil. - split.
rewrite -> fold_unfold_fetch_decode_execute_loop_nil in H_fdel. + intros ds' H_fdel.
injection H_fdel as ds_eq_ds'. rewrite -> fold_unfold_list_append_nil.
rewrite -> ds_eq_ds'. rewrite -> fold_unfold_fetch_decode_execute_loop_nil in H_fdel.
reflexivity. injection H_fdel as ds_eq_ds'.
- rewrite -> fold_unfold_list_append_cons. rewrite -> ds_eq_ds'.
rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
rewrite -> fold_unfold_fetch_decode_execute_loop_cons in H_fdel.
case (decode_execute bci ds) as [ ds1 | s ] eqn:H_decode_execute.
+ rewrite -> (IHbci1s' bci2s ds1 ds' H_fdel).
reflexivity. reflexivity.
+ discriminate H_fdel. + intros s H_fdel.
rewrite -> fold_unfold_fetch_decode_execute_loop_nil in H_fdel.
discriminate H_fdel.
- split.
+ intros ds' H_fdel.
rewrite -> fold_unfold_list_append_cons.
rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
rewrite -> fold_unfold_fetch_decode_execute_loop_cons in H_fdel.
case (decode_execute bci ds) as [ ds1 | s ] eqn:H_decode_execute.
* destruct (IHbci1s' ds1) as [IH_ok _].
exact (IH_ok ds' H_fdel).
* discriminate H_fdel.
+ intros s H_fdel.
rewrite -> fold_unfold_list_append_cons.
rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
rewrite -> fold_unfold_fetch_decode_execute_loop_cons in H_fdel.
case (decode_execute bci ds) as [ ds1 | s1 ] eqn:H_decode_execute.
* destruct (IHbci1s' ds1) as [_ IH_ko].
exact (IH_ko s H_fdel).
* exact H_fdel.
Qed. Qed.
(* ********** *) (* ********** *)