diff options
| -rw-r--r-- | lib/coq/Sail2_state_lemmas.v | 239 | ||||
| -rw-r--r-- | lib/coq/Sail2_state_lifting.v | 6 | ||||
| -rw-r--r-- | lib/coq/Sail2_state_monad.v | 36 | ||||
| -rw-r--r-- | lib/coq/Sail2_state_monad_lemmas.v | 215 |
4 files changed, 291 insertions, 205 deletions
diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v index 54cf45cc..c07016dc 100644 --- a/lib/coq/Sail2_state_lemmas.v +++ b/lib/coq/Sail2_state_lemmas.v @@ -1,19 +1,22 @@ Require Import Sail2_values Sail2_prompt_monad Sail2_prompt Sail2_state_monad Sail2_state Sail2_state Sail2_state_lifting. Require Import Sail2_state_monad_lemmas. +Local Open Scope equiv_scope. + (* Monad lifting *) -Lemma liftState_bind Regval Regs A B E {r : Sail2_values.register_accessors Regs Regval} {m : monad Regval A E} {f : A -> monad Regval B E} {s} : - liftState r (bind m f) s = bindS (liftState r m) (fun x => liftState r (f x)) s. -revert s. induction m; simpl. -all: try (intros; unfold seqS; rewrite bindS_assoc; auto using bindS_ext_cong). -all: try auto. -* intro s. - rewrite bindS_returnS_left. - reflexivity. +Lemma liftState_bind Regval Regs A B E {r : Sail2_values.register_accessors Regs Regval} {m : monad Regval A E} {f : A -> monad Regval B E} : + liftState r (bind m f) === bindS (liftState r m) (fun x => liftState r (f x)). +induction m; simpl; autorewrite with state; auto using bindS_cong. Qed. Hint Rewrite liftState_bind : liftState. +(* TODO: I want a general tactic for this, but abstracting the hint db out + appears to break. + This does beta reduction when no rules apply to try and allow more rules to apply + (e.g., the application of f to x in the above lemma may introduce a beta redex). *) +Ltac rewrite_liftState := rewrite_strat topdown (choice (progress try hints liftState) progress eval cbn beta). + Lemma liftState_return Regval Regs A E {r : Sail2_values.register_accessors Regs Regval} {a :A} : liftState (E:=E) r (returnm a) = returnS a. reflexivity. @@ -30,7 +33,7 @@ Lemma Value_liftState_Run: lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra] *) -Lemma liftState_if_distrib {Regs Regval A E r x y} {c : bool} : +Lemma liftState_if_distrib Regs Regval A E {r x y} {c : bool} : @liftState Regs Regval A E r (if c then x else y) = if c then liftState r x else liftState r y. destruct c; reflexivity. Qed. @@ -98,52 +101,51 @@ Lemma liftState_maybe_fail Regs Regval A E r msg x : @liftState Regs Regval A E r (maybe_fail msg x) = maybe_failS msg x. destruct x; reflexivity. Qed. -Lemma liftState_and_boolM Regs Regval E r x y s : - @liftState Regs Regval _ E r (and_boolM x y) s = and_boolS (liftState r x) (liftState r y) s. +Lemma liftState_and_boolM Regs Regval E r x y : + @liftState Regs Regval _ E r (and_boolM x y) === and_boolS (liftState r x) (liftState r y). unfold and_boolM, and_boolS. rewrite liftState_bind. -apply bindS_ext_cong; auto. +apply bindS_cong; auto. intros. rewrite liftState_if_distrib. reflexivity. Qed. -Lemma liftState_and_boolMP Regs Regval E P Q R r x y s H : - @liftState Regs Regval _ E r (@and_boolMP _ _ P Q R x y H) s = and_boolSP (liftState r x) (liftState r y) s. +Lemma liftState_and_boolMP Regs Regval E P Q R r x y H : + @liftState Regs Regval _ E r (@and_boolMP _ _ P Q R x y H) === and_boolSP (liftState r x) (liftState r y). unfold and_boolMP, and_boolSP. rewrite liftState_bind. -simpl. -apply bindS_ext_cong; auto. -intros [[|] [A]] s' ?. +apply bindS_cong; auto. +intros [[|] [A]]. * rewrite liftState_bind; simpl; - apply bindS_ext_cong; auto; - intros [a' A'] s'' ?; + apply bindS_cong; auto; + intros [a' A']; rewrite liftState_return; reflexivity. * rewrite liftState_return. reflexivity. Qed. -Lemma liftState_or_boolM Regs Regval E r x y s : - @liftState Regs Regval _ E r (or_boolM x y) s = or_boolS (liftState r x) (liftState r y) s. +Lemma liftState_or_boolM Regs Regval E r x y : + @liftState Regs Regval _ E r (or_boolM x y) === or_boolS (liftState r x) (liftState r y). unfold or_boolM, or_boolS. rewrite liftState_bind. -apply bindS_ext_cong; auto. +apply bindS_cong; auto. intros. rewrite liftState_if_distrib. reflexivity. Qed. -Lemma liftState_or_boolMP Regs Regval E P Q R r x y s H : - @liftState Regs Regval _ E r (@or_boolMP _ _ P Q R x y H) s = or_boolSP (liftState r x) (liftState r y) s. +Lemma liftState_or_boolMP Regs Regval E P Q R r x y H : + @liftState Regs Regval _ E r (@or_boolMP _ _ P Q R x y H) === or_boolSP (liftState r x) (liftState r y). unfold or_boolMP, or_boolSP. rewrite liftState_bind. simpl. -apply bindS_ext_cong; auto. -intros [[|] [A]] s' ?. +apply bindS_cong; auto. +intros [[|] [A]]. * rewrite liftState_return. reflexivity. * rewrite liftState_bind; simpl; - apply bindS_ext_cong; auto; - intros [a' A'] s'' ?; + apply bindS_cong; auto; + intros [a' A']; rewrite liftState_return; reflexivity. Qed. @@ -154,18 +156,15 @@ Hint Rewrite liftState_throw liftState_assert liftState_exit liftState_exclResul liftState_or_boolM liftState_or_boolMP : liftState. -Lemma liftState_try_catch Regs Regval A E1 E2 r m h s : - @liftState Regs Regval A E2 r (try_catch (E1 := E1) m h) s = try_catchS (liftState r m) (fun e => liftState r (h e)) s. -revert s. -induction m; intros; simpl; -try solve +Lemma liftState_try_catch Regs Regval A E1 E2 r m h : + @liftState Regs Regval A E2 r (try_catch (E1 := E1) m h) === try_catchS (liftState r m) (fun e => liftState r (h e)). +induction m; intros; simpl; autorewrite with state; +solve [ auto -| unfold seqS; - erewrite try_catchS_bindS_no_throw; intros; +| erewrite try_catchS_bindS_no_throw; intros; only 2,3: (autorewrite with ignore_throw; reflexivity); - apply bindS_ext_cong; auto + apply bindS_cong; auto ]. -rewrite try_catchS_throwS. reflexivity. Qed. Hint Rewrite liftState_try_catch : liftState. @@ -175,25 +174,26 @@ reflexivity. Qed. Hint Rewrite liftState_early_return : liftState. -Lemma liftState_catch_early_return (*[liftState_simp]:*) Regs Regval A E r m s : - liftState (Regs := Regs) r (@catch_early_return Regval A E m) s = catch_early_returnS (liftState r m) s. +Lemma liftState_catch_early_return (*[liftState_simp]:*) Regs Regval A E r m : + liftState (Regs := Regs) r (@catch_early_return Regval A E m) === catch_early_returnS (liftState r m). unfold catch_early_return, catch_early_returnS. -autorewrite with liftState. +rewrite_liftState. apply try_catchS_cong; auto. intros [a | e] s'; auto. Qed. Hint Rewrite liftState_catch_early_return : liftState. -Lemma liftState_liftR Regs Regval A R E r m s : - liftState (Regs := Regs) r (@liftR Regval A R E m) s = liftRS (liftState r m) s. -unfold liftR, liftRS. autorewrite with liftState. -apply try_catchS_cong; auto. +Lemma liftState_liftR Regs Regval A R E r m : + liftState (Regs := Regs) r (@liftR Regval A R E m) === liftRS (liftState r m). +unfold liftR, liftRS. +rewrite_liftState. +reflexivity. Qed. Hint Rewrite liftState_liftR : liftState. -Lemma liftState_try_catchR Regs Regval A R E1 E2 r m h s : - liftState (Regs := Regs) r (@try_catchR Regval A R E1 E2 m h) s = try_catchRS (liftState r m) (fun x => liftState r (h x)) s. -unfold try_catchR, try_catchRS. autorewrite with liftState. +Lemma liftState_try_catchR Regs Regval A R E1 E2 r m h : + liftState (Regs := Regs) r (@try_catchR Regval A R E1 E2 m h) === try_catchRS (liftState r m) (fun x => liftState r (h x)). +unfold try_catchR, try_catchRS. rewrite_liftState. apply try_catchS_cong; auto. intros [r' | e] s'; auto. Qed. @@ -204,25 +204,25 @@ Lemma liftState_bool_of_bitU_nondet Regs Regval : by (cases b; auto simp: bool_of_bitU_nondet_def bool_of_bitU_nondetS_def liftState_simp) Hint Rewrite liftState_bool_of_bitU_nondet : liftState. *) -Lemma liftState_read_memt Regs Regval A B E H rk a sz r s : - liftState (Regs := Regs) r (@read_memt Regval A B E H rk a sz) s = read_memtS rk a sz s. +Lemma liftState_read_memt Regs Regval A B E H rk a sz r : + liftState (Regs := Regs) r (@read_memt Regval A B E H rk a sz) === read_memtS rk a sz. unfold read_memt, read_memt_bytes, read_memtS, maybe_failS. simpl. -apply bindS_ext_cong; auto. -intros [byte bit] s' valIn. +apply bindS_cong; auto. +intros [byte bit]. destruct (option_map _); auto. Qed. Hint Rewrite liftState_read_memt : liftState. -Lemma liftState_read_mem Regs Regval A B E H rk asz a sz r s : - liftState (Regs := Regs) r (@read_mem Regval A B E H rk asz a sz) s = read_memS rk a sz s. +Lemma liftState_read_mem Regs Regval A B E H rk asz a sz r : + liftState (Regs := Regs) r (@read_mem Regval A B E H rk asz a sz) === read_memS rk a sz. unfold read_mem, read_memS, read_memtS. simpl. unfold read_mem_bytesS, read_memt_bytesS. repeat rewrite bindS_assoc. -apply bindS_ext_cong; auto. -intros [ bytes | ] s' valIn; auto. simpl. -apply bindS_ext_cong; auto. -intros [byte bit] s'' valIn'. -rewrite bindS_returnS_left. autorewrite with liftState. +apply bindS_cong; auto. +intros [ bytes | ]; auto. simpl. +apply bindS_cong; auto. +intros [byte bit]. +rewrite bindS_returnS_left. rewrite_liftState. destruct (option_map _); auto. Qed. Hint Rewrite liftState_read_mem : liftState. @@ -253,15 +253,15 @@ Lemma bindS_rw_left Regs A B E m1 m2 (f : A -> monadS Regs B E) s : intro H. unfold bindS. rewrite H. reflexivity. Qed. -Lemma liftState_read_reg_readS Regs Regval A E reg get_regval' set_regval' s : +Lemma liftState_read_reg_readS Regs Regval A E reg get_regval' set_regval' : (forall s, map_bind reg.(of_regval) (get_regval' reg.(name) s) = Some (reg.(read_from) s)) -> - liftState (Regs := Regs) (get_regval', set_regval') (@read_reg _ Regval A E reg) s = readS (fun x => reg.(read_from) (regstate x)) s. + liftState (Regs := Regs) (get_regval', set_regval') (@read_reg _ Regval A E reg) === readS (fun x => reg.(read_from) (ss_regstate x)). intros. -unfold read_reg. simpl. unfold readS. +unfold read_reg. simpl. unfold readS. intro s. erewrite bindS_rw_left. 2: { apply bindS_returnS_left. } -specialize (H (regstate s)). +specialize (H (ss_regstate s)). destruct (get_regval' _ _) as [v | ]; only 2: discriminate H. rewrite bindS_returnS_left. simpl in *. @@ -269,15 +269,15 @@ rewrite H. reflexivity. Qed. -Lemma liftState_write_reg_updateS Regs Regval A E get_regval' set_regval' reg (v : A) s : +Lemma liftState_write_reg_updateS Regs Regval A E get_regval' set_regval' reg (v : A) : (forall s, set_regval' (name reg) (regval_of reg v) s = Some (write_to reg v s)) -> - liftState (Regs := Regs) (Regval := Regval) (E := E) (get_regval', set_regval') (write_reg reg v) s = updateS (fun s => {| regstate := (write_to reg v s.(regstate)); memstate := s.(memstate); tagstate := s.(tagstate) |}) s. -intros. + liftState (Regs := Regs) (Regval := Regval) (E := E) (get_regval', set_regval') (write_reg reg v) === updateS (fun s => {| ss_regstate := (write_to reg v s.(ss_regstate)); ss_memstate := s.(ss_memstate); ss_tagstate := s.(ss_tagstate) |}). +intros. intro s. unfold write_reg. simpl. unfold readS, seqS. erewrite bindS_rw_left. 2: { apply bindS_returnS_left. } -specialize (H (regstate s)). +specialize (H (ss_regstate s)). destruct (set_regval' _ _) as [v' | ]; only 2: discriminate H. injection H as H1. unfold updateS. @@ -299,42 +299,59 @@ lemma liftState_iter[liftState_simp]: "liftState r (iter f xs) = iterS (liftState r \<circ> f) xs" by (auto simp: iter_def iterS_def liftState_simp) *) -Lemma liftState_foreachM Regs Regval A Vars E (xs : list A) (vars : Vars) (body : A -> Vars -> monad Regval Vars E) r s : - liftState (Regs := Regs) r (foreachM xs vars body) s = foreachS xs vars (fun x vars => liftState r (body x vars)) s. -revert vars s. +Lemma liftState_foreachM Regs Regval A Vars E (xs : list A) (vars : Vars) (body : A -> Vars -> monad Regval Vars E) r : + liftState (Regs := Regs) r (foreachM xs vars body) === foreachS xs vars (fun x vars => liftState r (body x vars)). +revert vars. induction xs as [ | h t]. * reflexivity. -* intros vars s. simpl. - autorewrite with liftState. - apply bindS_ext_cong; auto. +* intros vars. simpl. + rewrite_liftState. + apply bindS_cong; auto. Qed. Hint Rewrite liftState_foreachM : liftState. -Lemma foreachS_cong {A RV Vars E} xs vars f f' s : - (forall a vars s, f a vars s = f' a vars s) -> - @foreachS A RV Vars E xs vars f s = foreachS xs vars f' s. +Lemma foreachS_cong {A RV Vars E} xs vars f f' : + (forall a vars, f a vars === f' a vars) -> + @foreachS A RV Vars E xs vars f === foreachS xs vars f'. intro H. -revert s vars. +revert vars. induction xs. * reflexivity. * intros. simpl. - apply bindS_ext_cong; auto. + rewrite H. + apply bindS_cong; auto. Qed. -Lemma liftState_genlistM Regs Regval A E r f n s : - liftState (Regs := Regs) r (@genlistM A Regval E f n) s = genlistS (fun x => liftState r (f x)) n s. -unfold genlistM, genlistS. -autorewrite with liftState. +Add Parametric Morphism {Regs A Vars E : Type} : (@foreachS A Regs Vars E) + with signature eq ==> eq ==> equiv ==> equiv as foreachS_morphism. apply foreachS_cong. -intros; autorewrite with liftState. -apply bindS_ext_cong; auto. +Qed. + +(*Tactic Notation "sail_rewrite" ident(hintdb) := rewrite_strat topdown (choice (hints hintdb) progress eval cbn beta). +Ltac sail_rewrite hintdb := rewrite_strat topdown (choice (hints hintdb) progress eval cbn beta).*) + +Lemma liftState_genlistM Regs Regval A E r f n : + liftState (Regs := Regs) r (@genlistM A Regval E f n) === genlistS (fun x => liftState r (f x)) n. +unfold genlistM, genlistS. +rewrite_liftState. +reflexivity. Qed. Hint Rewrite liftState_genlistM : liftState. -Lemma liftState_choose_bools Regs Regval E descr n r s : - liftState (Regs := Regs) r (@choose_bools Regval E descr n) s = choose_boolsS n s. +Add Parametric Morphism {A RV E : Type} : (@genlistS A RV E) + with signature equiv ==> eq ==> equiv as genlistS_morphism. +intros f g EQ n. +unfold genlistS. +apply foreachS_cong. +intros m vars. +rewrite EQ. +reflexivity. +Qed. + +Lemma liftState_choose_bools Regs Regval E descr n r : + liftState (Regs := Regs) r (@choose_bools Regval E descr n) === choose_boolsS n. unfold choose_bools, choose_boolsS. -autorewrite with liftState. +rewrite_liftState. reflexivity. Qed. Hint Rewrite liftState_choose_bools : liftState. @@ -347,16 +364,14 @@ Lemma liftState_bools_of_bits_nondet[liftState_simp]: Hint Rewrite liftState_choose_bools : liftState. *) -Lemma liftState_internal_pick Regs Regval A E r (xs : list A) s : - liftState (Regs := Regs) (Regval := Regval) (E := E) r (internal_pick xs) s = internal_pickS xs s. +Lemma liftState_internal_pick Regs Regval A E r (xs : list A) : + liftState (Regs := Regs) (Regval := Regval) (E := E) r (internal_pick xs) === internal_pickS xs. unfold internal_pick, internal_pickS. unfold choose. -autorewrite with liftState. -apply bindS_ext_cong. -* autorewrite with liftState. - reflexivity. -* intros. - destruct (nth_error _ _); auto. +rewrite_liftState. +apply bindS_cong; auto. +intros. +destruct (nth_error _ _); auto. Qed. Hint Rewrite liftState_internal_pick : liftState. @@ -372,8 +387,9 @@ rewrite app_nil_r. reflexivity. Qed. -Lemma liftRS_bindS Regs A B R E (m : monadS Regs A E) (f : A -> monadS Regs B E) s : - @liftRS B R Regs E (bindS m f) s = bindS (liftRS m) (fun x => liftRS (f x)) s. +Lemma liftRS_bindS Regs A B R E (m : monadS Regs A E) (f : A -> monadS Regs B E) : + @liftRS B R Regs E (bindS m f) === bindS (liftRS m) (fun x => liftRS (f x)). +intro s. unfold liftRS, try_catchS, bindS, throwS, returnS. induction (m s) as [ | [[a | [msg | e]] t]]. * reflexivity. @@ -480,20 +496,24 @@ Local Opaque _limit_reduces. Ltac gen_reduces := match goal with |- context[@_limit_reduces ?a ?b ?c] => generalize (@_limit_reduces a b c) end. -Lemma liftState_whileM RV Vars E r measure vars cond (body : Vars -> monad RV Vars E) s : - liftState (Regs := RV) r (whileMT vars measure cond body) s = whileST vars measure (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)) s. +(* TODO: rewrite_liftState is performing really badly here. We could add liftState_if_distrib + to the hint db, but then it starts failing in a way that causes the whole rewriting to fail. *) + +Lemma liftState_whileM RV Vars E r measure vars cond (body : Vars -> monad RV Vars E) : + liftState (Regs := RV) r (whileMT vars measure cond body) === whileST vars measure (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)). unfold whileMT, whileST. generalize (measure vars) as limit. intro. -revert vars s. +revert vars. destruct (Z.le_decidable 0 limit). * generalize (Zwf_guarded limit) as acc. apply Wf_Z.natlike_ind with (x := limit). + intros [acc] *; simpl. - autorewrite with liftState. - apply bindS_ext_cong; auto. - intros. rewrite liftState_if_distrib. - destruct a; autorewrite with liftState; auto. - apply bindS_ext_cong; auto. + match goal with |- context [Build_ArithFact _ ?prf] => generalize prf; intros ?Proof end. + rewrite_liftState. + setoid_rewrite liftState_if_distrib. + apply bindS_cong; auto. + destruct a; rewrite_liftState; auto. + apply bindS_cong; auto. intros. destruct (_limit_reduces _). simpl. reflexivity. + clear limit H. @@ -553,16 +573,17 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState qed auto qed*) -Lemma liftState_untilM RV Vars E r measure vars cond (body : Vars -> monad RV Vars E) s : - liftState (Regs := RV) r (untilMT vars measure cond body) s = untilST vars measure (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)) s. +Lemma liftState_untilM RV Vars E r measure vars cond (body : Vars -> monad RV Vars E) : + liftState (Regs := RV) r (untilMT vars measure cond body) === untilST vars measure (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)). unfold untilMT, untilST. generalize (measure vars) as limit. intro. -revert vars s. +revert vars. destruct (Z.le_decidable 0 limit). * generalize (Zwf_guarded limit) as acc. apply Wf_Z.natlike_ind with (x := limit). - + intros [acc] *; simpl. - autorewrite with liftState. + + intros [acc] * s; simpl. +(* TODO rewrite_liftState.*) +autorewrite with liftState. apply bindS_ext_cong; auto. intros. autorewrite with liftState. apply bindS_ext_cong; auto. diff --git a/lib/coq/Sail2_state_lifting.v b/lib/coq/Sail2_state_lifting.v index 633c0ef7..1544c3c9 100644 --- a/lib/coq/Sail2_state_lifting.v +++ b/lib/coq/Sail2_state_lifting.v @@ -42,12 +42,12 @@ match e with if success then Some (put_mem_bytes addr sz v tag s) else None | E_read_reg r v => let (read_reg, _) := ra in - option_bind (read_reg r s.(regstate)) (fun v' => + option_bind (read_reg r s.(ss_regstate)) (fun v' => if generic_eq v' v then Some s else None) | E_write_reg r v => let (_, write_reg) := ra in - option_bind (write_reg r v s.(regstate)) (fun rs' => - Some {| regstate := rs'; memstate := s.(memstate); tagstate := s.(tagstate) |}) + option_bind (write_reg r v s.(ss_regstate)) (fun rs' => + Some {| ss_regstate := rs'; ss_memstate := s.(ss_memstate); ss_tagstate := s.(ss_tagstate) |}) | _ => Some s end. diff --git a/lib/coq/Sail2_state_monad.v b/lib/coq/Sail2_state_monad.v index faee9569..552fa68e 100644 --- a/lib/coq/Sail2_state_monad.v +++ b/lib/coq/Sail2_state_monad.v @@ -14,17 +14,19 @@ Definition Memstate : Type := NatMap.t memory_byte. Definition Tagstate : Type := NatMap.t bitU. (* type regstate = map string (vector bitU) *) +(* We deviate from the Lem library and prefix the fields with ss_ to avoid + name clashes. *) Record sequential_state {Regs} := - { regstate : Regs; - memstate : Memstate; - tagstate : Tagstate }. + { ss_regstate : Regs; + ss_memstate : Memstate; + ss_tagstate : Tagstate }. Arguments sequential_state : clear implicits. (*val init_state : forall 'regs. 'regs -> sequential_state 'regs*) Definition init_state {Regs} regs : sequential_state Regs := - {| regstate := regs; - memstate := NatMap.empty _; - tagstate := NatMap.empty _ |}. + {| ss_regstate := regs; + ss_memstate := NatMap.empty _; + ss_tagstate := NatMap.empty _ |}. Inductive ex E := | Failure : string -> ex E @@ -146,7 +148,7 @@ end. (*val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e*) Definition read_tagS {Regs A E} (addr : mword A) : monadS Regs bitU E := let addr := Word.wordToNat (get_word addr) in - readS (fun s => opt_def B0 (NatMap.find addr s.(tagstate))). + readS (fun s => opt_def B0 (NatMap.find addr s.(ss_tagstate))). Fixpoint genlist_acc {A:Type} (f : nat -> A) n acc : list A := match n with @@ -160,8 +162,8 @@ Definition genlist {A} f n := @genlist_acc A f n []. (*val get_mem_bytes : forall 'regs. nat -> nat -> sequential_state 'regs -> maybe (list memory_byte * bitU)*) Definition get_mem_bytes {Regs} addr sz (s : sequential_state Regs) : option (list memory_byte * bitU) := let addrs := genlist (fun n => addr + n)%nat sz in - let read_byte s addr := NatMap.find addr s.(memstate) in - let read_tag s addr := opt_def B0 (NatMap.find addr s.(tagstate)) in + let read_byte s addr := NatMap.find addr s.(ss_memstate) in + let read_tag s addr := opt_def B0 (NatMap.find addr s.(ss_tagstate)) in option_map (fun mem_val => (mem_val, List.fold_left and_bit (List.map (read_tag s) addrs) B1)) (just_list (List.map (read_byte s) addrs)). @@ -203,9 +205,9 @@ Definition put_mem_bytes {Regs} addr sz (v : list memory_byte) (tag : bitU) (s : let a_v := List.combine addrs v in let write_byte mem '(addr, v) := NatMap.add addr v mem in let write_tag mem addr := NatMap.add addr tag mem in - {| regstate := s.(regstate); - memstate := List.fold_left write_byte a_v s.(memstate); - tagstate := List.fold_left write_tag addrs s.(tagstate) |}. + {| ss_regstate := s.(ss_regstate); + ss_memstate := List.fold_left write_byte a_v s.(ss_memstate); + ss_tagstate := List.fold_left write_tag addrs s.(ss_tagstate) |}. (*val write_memt_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e*) Definition write_memt_bytesS {Regs E} (_ : write_kind) addr sz (v : list memory_byte) (t : bitU) : monadS Regs bool E := @@ -231,7 +233,7 @@ Definition write_memS {Regs E A B} wk (addr : mword A) sz (v : mword B) : monadS (*val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e*) Definition read_regS {Regs RV A E} (reg : register_ref Regs RV A) : monadS Regs A E := - readS (fun s => reg.(read_from) s.(regstate)). + readS (fun s => reg.(read_from) s.(ss_regstate)). (* TODO let read_reg_range reg i j state = @@ -251,7 +253,7 @@ let read_reg_bitfield reg regfield = register_accessors 'regs 'rv -> string -> monadS 'regs 'rv 'e*) Definition read_regvalS {Regs RV E} (acc : register_accessors Regs RV) reg : monadS Regs RV E := let '(read, _) := acc in - readS (fun s => read reg s.(regstate)) >>$= (fun v => match v with + readS (fun s => read reg s.(ss_regstate)) >>$= (fun v => match v with | Some v => returnS v | None => failS ("read_regvalS " ++ reg) end). @@ -260,14 +262,14 @@ Definition read_regvalS {Regs RV E} (acc : register_accessors Regs RV) reg : mon register_accessors 'regs 'rv -> string -> 'rv -> monadS 'regs unit 'e*) Definition write_regvalS {Regs RV E} (acc : register_accessors Regs RV) reg (v : RV) : monadS Regs unit E := let '(_, write) := acc in - readS (fun s => write reg v s.(regstate)) >>$= (fun x => match x with - | Some rs' => updateS (fun s => {| regstate := rs'; memstate := s.(memstate); tagstate := s.(tagstate) |}) + readS (fun s => write reg v s.(ss_regstate)) >>$= (fun x => match x with + | Some rs' => updateS (fun s => {| ss_regstate := rs'; ss_memstate := s.(ss_memstate); ss_tagstate := s.(ss_tagstate) |}) | None => failS ("write_regvalS " ++ reg) end). (*val write_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> 'a -> monadS 'regs unit 'e*) Definition write_regS {Regs RV A E} (reg : register_ref Regs RV A) (v:A) : monadS Regs unit E := - updateS (fun s => {| regstate := reg.(write_to) v s.(regstate); memstate := s.(memstate); tagstate := s.(tagstate) |}). + updateS (fun s => {| ss_regstate := reg.(write_to) v s.(ss_regstate); ss_memstate := s.(ss_memstate); ss_tagstate := s.(ss_tagstate) |}). (* TODO val update_reg : forall 'regs 'rv 'a 'b 'e. register_ref 'regs 'rv 'a -> ('a -> 'b -> 'a) -> 'b -> monadS 'regs unit 'e diff --git a/lib/coq/Sail2_state_monad_lemmas.v b/lib/coq/Sail2_state_monad_lemmas.v index e2b98d79..99fef329 100644 --- a/lib/coq/Sail2_state_monad_lemmas.v +++ b/lib/coq/Sail2_state_monad_lemmas.v @@ -1,5 +1,22 @@ Require Import Sail2_state_monad. (*Require Import Sail2_values_lemmas.*) +Require Export Setoid. +Require Export Morphisms Equivalence. + +(* Ensure that pointwise equality on states is the preferred notion of + equivalence for the state monad. *) +Local Open Scope equiv_scope. +Instance monadS_equivalence {Regs A E} : + Equivalence (pointwise_relation (sequential_state Regs) (@eq (list (result A E * sequential_state Regs)))) | 9. +split; apply _. +Qed. + +Global Instance refl_eq_subrelation {A : Type} {R : A -> A -> Prop} `{Reflexive A R} : subrelation eq R. +intros x y EQ. subst. reflexivity. +Qed. + +Hint Extern 4 (_ === _) => reflexivity. +Hint Extern 4 (_ === _) => symmetry. Lemma bindS_ext_cong (*[fundef_cong]:*) {Regs A B E} {m1 m2 : monadS Regs A E} {f1 f2 : A -> monadS Regs B E} s : @@ -15,29 +32,40 @@ apply List.map_ext_in. intros [[a|a] s'] H_in; auto. Qed. -(* -lemma bindS_cong[fundef_cong]: - assumes m: "m1 = m2" - and f: "\<And>s a s'. (Value a, s') \<in> (m2 s) \<Longrightarrow> f1 a s' = f2 a s'" - shows "bindS m1 f1 = bindS m2 f2" - using assms by (intro ext bindS_ext_cong; blast) -*) +(* Weaker than the Isabelle version, but avoids talking about individual states *) +Lemma bindS_cong (*[fundef_cong]:*) Regs A B E m1 m2 (f1 f2 : A -> monadS Regs B E) : + m1 === m2 -> + (forall a, f1 a === f2 a) -> + bindS m1 f1 === bindS m2 f2. +intros M F s. +apply bindS_ext_cong; intros; auto. +apply F. +Qed. + +Add Parametric Morphism {Regs A B E : Type} : (@bindS Regs A B E) + with signature equiv ==> equiv ==> equiv as bindS_morphism. +auto using bindS_cong. +Qed. -Lemma bindS_returnS_left (*[simp]:*) {Regs A B E} {x : A} {f : A -> monadS Regs B E} {s} : - bindS (returnS x) f s = f x s. +Lemma bindS_returnS_left Regs A B E {x : A} {f : A -> monadS Regs B E} : + bindS (returnS x) f === f x. +intro s. unfold returnS, bindS. simpl. auto using List.app_nil_r. Qed. +Hint Rewrite bindS_returnS_left : state. -Lemma bindS_returnS_right (*[simp]:*) {Regs A E} {m : monadS Regs A E} {s} : - bindS m returnS s = m s. +Lemma bindS_returnS_right Regs A E {m : monadS Regs A E} : + bindS m returnS === m. +intro s. unfold returnS, bindS. induction (m s) as [|[[a|a] s'] t]; auto; simpl; rewrite IHt; reflexivity. Qed. +Hint Rewrite bindS_returnS_right : state. Lemma bindS_readS {Regs A E} {f} {m : A -> monadS Regs A E} {s} : bindS (readS f) m s = m (f s) s. @@ -54,20 +82,24 @@ simpl. auto using List.app_nil_r. Qed. -Lemma bindS_assertS_True (*[simp]:*) {Regs A E msg} {f : unit -> monadS Regs A E} {s} : - bindS (assert_expS true msg) f s = f tt s. +Lemma bindS_assertS_true Regs A E msg {f : unit -> monadS Regs A E} : + bindS (assert_expS true msg) f === f tt. +intro s. unfold assert_expS, bindS. simpl. auto using List.app_nil_r. Qed. +Hint Rewrite bindS_assertS_true : state. -Lemma bindS_chooseS_returnS (*[simp]:*) {Regs A B E} {xs : list A} {f : A -> B} {s} : - bindS (Regs := Regs) (E := E) (chooseS xs) (fun x => returnS (f x)) s = chooseS (List.map f xs) s. +Lemma bindS_chooseS_returnS (*[simp]:*) Regs A B E {xs : list A} {f : A -> B} : + bindS (Regs := Regs) (E := E) (chooseS xs) (fun x => returnS (f x)) === chooseS (List.map f xs). +intro s. unfold chooseS, bindS, returnS. induction xs; auto. simpl. rewrite IHxs. reflexivity. Qed. +Hint Rewrite bindS_chooseS_returnS : state. Lemma result_cases : forall (A E : Type) (P : result A E -> Prop), (forall a, P (Value a)) -> @@ -145,8 +177,9 @@ eauto. Qed. Hint Resolve bindS_intro_Value bindS_intro_Ex_left bindS_intro_Ex_right : bindS_intros. -Lemma bindS_assoc (*[simp]:*) {Regs A B C E} {m} {f : A -> monadS Regs B E} {g : B -> monadS Regs C E} {s} : - bindS (bindS m f) g s = bindS m (fun x => bindS (f x) g) s. +Lemma bindS_assoc Regs A B C E {m} {f : A -> monadS Regs B E} {g : B -> monadS Regs C E} : + bindS (bindS m f) g === bindS m (fun x => bindS (f x) g). +intro s. unfold bindS. induction (m s) as [ | [[a | e] t]]. * reflexivity. @@ -157,16 +190,26 @@ induction (m s) as [ | [[a | e] t]]. reflexivity. * simpl. rewrite IHl. reflexivity. Qed. +Hint Rewrite bindS_assoc : state. -Lemma bindS_failS (*[simp]:*) {Regs A B E} {msg} {f : A -> monadS Regs B E} : +Lemma bindS_failS Regs A B E {msg} {f : A -> monadS Regs B E} : bindS (failS msg) f = failS msg. reflexivity. Qed. -Lemma bindS_throwS (*[simp]:*) {Regs A B E} {e} {f : A -> monadS Regs B E} : +Hint Rewrite bindS_failS : state. + +Lemma bindS_throwS Regs A B E {e} {f : A -> monadS Regs B E} : bindS (throwS e) f = throwS e. reflexivity. Qed. +Hint Rewrite bindS_throwS : state. + (*declare seqS_def[simp]*) +Lemma seqS_def Regs A E m (m' : monadS Regs A E) : + m >>$ m' = m >>$= (fun _ => m'). +reflexivity. +Qed. +Hint Rewrite seqS_def : state. Lemma Value_bindS_elim {Regs A B E} {a m} {f : A -> monadS Regs B E} {s s'} : List.In (Value a, s') (bindS m f s) -> @@ -187,32 +230,49 @@ destruct H as [(? & ? & ? & [= ] & _) | [(? & [= <-] & X) | (? & ? & ? & [= <-] eauto. Qed. -Lemma try_catchS_returnS (*[simp]:*) {Regs A E1 E2} {a} {h : E1 -> monadS Regs A E2}: +Lemma try_catchS_returnS Regs A E1 E2 {a} {h : E1 -> monadS Regs A E2}: try_catchS (returnS a) h = returnS a. reflexivity. Qed. -Lemma try_catchS_failS (*[simp]:*) {Regs A E1 E2} {msg} {h : E1 -> monadS Regs A E2}: +Hint Rewrite try_catchS_returnS : state. +Lemma try_catchS_failS Regs A E1 E2 {msg} {h : E1 -> monadS Regs A E2}: try_catchS (failS msg) h = failS msg. reflexivity. Qed. -Lemma try_catchS_throwS (*[simp]:*) {Regs A E1 E2} {e} {h : E1 -> monadS Regs A E2} {s}: - try_catchS (throwS e) h s = h e s. +Hint Rewrite try_catchS_failS : state. +Lemma try_catchS_throwS Regs A E1 E2 {e} {h : E1 -> monadS Regs A E2}: + try_catchS (throwS e) h === h e. +intro s. unfold try_catchS, throwS. simpl. auto using List.app_nil_r. Qed. +Hint Rewrite try_catchS_throwS : state. -Lemma try_catchS_cong (*[cong]:*) {Regs A E1 E2 m1 m2} {h1 h2 : E1 -> monadS Regs A E2} {s} : - (forall s, m1 s = m2 s) -> - (forall e s, h1 e s = h2 e s) -> - try_catchS m1 h1 s = try_catchS m2 h2 s. -intros H1 H2. +Lemma try_catchS_cong (*[cong]:*) {Regs A E1 E2 m1 m2} {h1 h2 : E1 -> monadS Regs A E2} : + m1 === m2 -> + (forall e, h1 e === h2 e) -> + try_catchS m1 h1 === try_catchS m2 h2. +intros H1 H2 s. unfold try_catchS. rewrite H1. rewrite !List.flat_map_concat_map. f_equal. apply List.map_ext_in. -intros [[a|[e|msg]] s'] H_in; auto. +intros [[a|[e|msg]] s'] H_in; auto. apply H2. +Qed. + +Add Parametric Morphism {Regs A E1 E2 : Type} : (@try_catchS Regs A E1 E2) + with signature equiv ==> equiv ==> equiv as try_catchS_morphism. +intros. auto using try_catchS_cong. +Qed. + +Add Parametric Morphism {Regs A E : Type} : (@catch_early_returnS Regs A E) + with signature equiv ==> equiv as catch_early_returnS_morphism. +intros. +unfold catch_early_returnS. +rewrite H. +reflexivity. Qed. Lemma try_catchS_cases {Regs A E1 E2 m} {h : E1 -> monadS Regs A E2} {r s s'} : @@ -265,10 +325,10 @@ end. Definition ignore_throw {A E1 E2 S} (m : S -> list (result A E1 * S)) s : list (result A E2 * S) := List.flat_map ignore_throw_aux (m s). -Lemma ignore_throw_cong {A E1 E2 S} {m1 m2 : S -> list (result A E1 * S)} s : - (forall s, m1 s = m2 s) -> - ignore_throw (E2 := E2) m1 s = ignore_throw m2 s. -intro H. +Lemma ignore_throw_cong {Regs A E1 E2} {m1 m2 : monadS Regs A E1} : + m1 === m2 -> + ignore_throw (E2 := E2) m1 === ignore_throw m2. +intros H s. unfold ignore_throw. rewrite H. reflexivity. @@ -314,8 +374,9 @@ rewrite List.map_app, List.concat_app. reflexivity. Qed. -Lemma ignore_throw_bindS (*[simp]:*) Regs A B E E2 {m} {f : A -> monadS Regs B E} {s} : - ignore_throw (E2 := E2) (bindS m f) s = bindS (ignore_throw m) (fun s => ignore_throw (f s)) s. +Lemma ignore_throw_bindS (*[simp]:*) Regs A B E E2 {m} {f : A -> monadS Regs B E} : + ignore_throw (E2 := E2) (bindS m f) === bindS (ignore_throw m) (fun s => ignore_throw (f s)). +intro s. unfold bindS, ignore_throw. induction (m s) as [ | [[a | [e | msg]] t]]. * reflexivity. @@ -325,13 +386,14 @@ induction (m s) as [ | [[a | [e | msg]] t]]. Qed. Hint Rewrite ignore_throw_bindS : ignore_throw. -Lemma try_catchS_bindS_no_throw {Regs A B E1 E2} {m1 : monadS Regs A E1} {m2 : monadS Regs A E2} {f : A -> monadS Regs B _} {s h} : - (forall s, ignore_throw m1 s = m1 s) -> - (forall s, ignore_throw m1 s = m2 s) -> - try_catchS (bindS m1 f) h s = bindS m2 (fun a => try_catchS (f a) h) s. +Lemma try_catchS_bindS_no_throw {Regs A B E1 E2} {m1 : monadS Regs A E1} {m2 : monadS Regs A E2} {f : A -> monadS Regs B _} {h} : + ignore_throw m1 === m1 -> + ignore_throw m1 === m2 -> + try_catchS (bindS m1 f) h === bindS m2 (fun a => try_catchS (f a) h). intros Ignore1 Ignore2. -transitivity ((ignore_throw m1 >>$= (fun a => try_catchS (f a) h)) s). -* unfold bindS, try_catchS, ignore_throw. +transitivity ((ignore_throw m1 >>$= (fun a => try_catchS (f a) h))). +* intro s. + unfold bindS, try_catchS, ignore_throw. specialize (Ignore1 s). revert Ignore1. unfold ignore_throw. induction (m1 s) as [ | [[a | [e | msg]] t]]; auto. + intro Ig. simpl. rewrite flat_map_app. rewrite IHl. auto. injection Ig. auto. @@ -343,7 +405,7 @@ transitivity ((ignore_throw m1 >>$= (fun a => try_catchS (f a) h)) s). destruct H as [x [H1 H2]]. apply ignore_throw_aux_member_simps in H2. assumption. -* apply bindS_ext_cong; auto. +* apply bindS_cong; auto. Qed. Lemma concat_map_singleton {A B} {f : A -> B} {a : list A} : @@ -361,8 +423,9 @@ reflexivity. Qed. Lemma no_throw_basic_builtins_3 Regs E E2 {f : sequential_state Regs -> sequential_state Regs} : ignore_throw (E1 := E) (E2 := E2) (updateS f) = updateS f. reflexivity. Qed. -Lemma no_throw_basic_builtins_4 Regs A E1 E2 {xs : list A} s : - ignore_throw (E1 := E1) (chooseS xs) s = @chooseS Regs A E2 xs s. +Lemma no_throw_basic_builtins_4 Regs A E1 E2 {xs : list A} : + ignore_throw (E1 := E1) (chooseS xs) === @chooseS Regs A E2 xs. +intro s. unfold ignore_throw, chooseS. rewrite List.flat_map_concat_map, List.map_map. simpl. rewrite concat_map_singleton. @@ -399,81 +462,81 @@ Lemma ignore_throw_let_distrib Regs A B E1 E2 (y : A) (f : A -> monadS Regs B E1 reflexivity. Qed. -Lemma no_throw_mem_builtins_1 Regs E1 E2 rk a sz s : - ignore_throw (E2 := E2) (@read_memt_bytesS Regs E1 rk a sz) s = read_memt_bytesS rk a sz s. +Lemma no_throw_mem_builtins_1 Regs E1 E2 rk a sz : + ignore_throw (E2 := E2) (@read_memt_bytesS Regs E1 rk a sz) === read_memt_bytesS rk a sz. unfold read_memt_bytesS. autorewrite with ignore_throw. -apply bindS_ext_cong; auto. intros. autorewrite with ignore_throw. reflexivity. +apply bindS_cong; auto. intros. autorewrite with ignore_throw. reflexivity. Qed. Hint Rewrite no_throw_mem_builtins_1 : ignore_throw. -Lemma no_throw_mem_builtins_2 Regs E1 E2 rk a sz s : - ignore_throw (E2 := E2) (@read_mem_bytesS Regs E1 rk a sz) s = read_mem_bytesS rk a sz s. +Lemma no_throw_mem_builtins_2 Regs E1 E2 rk a sz : + ignore_throw (E2 := E2) (@read_mem_bytesS Regs E1 rk a sz) === read_mem_bytesS rk a sz. unfold read_mem_bytesS. autorewrite with ignore_throw. -apply bindS_ext_cong; intros; autorewrite with ignore_throw; auto. +apply bindS_cong; intros; autorewrite with ignore_throw; auto. destruct a0; reflexivity. Qed. Hint Rewrite no_throw_mem_builtins_2 : ignore_throw. -Lemma no_throw_mem_builtins_3 Regs A E1 E2 a s : - ignore_throw (E2 := E2) (@read_tagS Regs A E1 a) s = read_tagS a s. +Lemma no_throw_mem_builtins_3 Regs A E1 E2 a : + ignore_throw (E2 := E2) (@read_tagS Regs A E1 a) === read_tagS a. reflexivity. Qed. Hint Rewrite no_throw_mem_builtins_3 : ignore_throw. -Lemma no_throw_mem_builtins_4 Regs A V E1 E2 rk a sz s H : - ignore_throw (E2 := E2) (@read_memtS Regs E1 A V rk a sz H) s = read_memtS rk a sz s. +Lemma no_throw_mem_builtins_4 Regs A V E1 E2 rk a sz H : + ignore_throw (E2 := E2) (@read_memtS Regs E1 A V rk a sz H) === read_memtS rk a sz. unfold read_memtS. autorewrite with ignore_throw. -apply bindS_ext_cong; intros; autorewrite with ignore_throw. +apply bindS_cong; intros; autorewrite with ignore_throw. reflexivity. destruct a0; simpl. autorewrite with ignore_throw. reflexivity. Qed. Hint Rewrite no_throw_mem_builtins_4 : ignore_throw. -Lemma no_throw_mem_builtins_5 Regs A V E1 E2 rk a sz s H : - ignore_throw (E2 := E2) (@read_memS Regs E1 A V rk a sz H) s = read_memS rk a sz s. +Lemma no_throw_mem_builtins_5 Regs A V E1 E2 rk a sz H : + ignore_throw (E2 := E2) (@read_memS Regs E1 A V rk a sz H) === read_memS rk a sz. unfold read_memS. autorewrite with ignore_throw. -apply bindS_ext_cong; intros; autorewrite with ignore_throw; auto. +apply bindS_cong; intros; autorewrite with ignore_throw; auto. destruct a0; auto. Qed. Hint Rewrite no_throw_mem_builtins_5 : ignore_throw. -Lemma no_throw_mem_builtins_6 Regs E1 E2 wk addr sz v t s : - ignore_throw (E2 := E2) (@write_memt_bytesS Regs E1 wk addr sz v t) s = write_memt_bytesS wk addr sz v t s. +Lemma no_throw_mem_builtins_6 Regs E1 E2 wk addr sz v t : + ignore_throw (E2 := E2) (@write_memt_bytesS Regs E1 wk addr sz v t) === write_memt_bytesS wk addr sz v t. unfold write_memt_bytesS. unfold seqS. autorewrite with ignore_throw. reflexivity. Qed. Hint Rewrite no_throw_mem_builtins_6 : ignore_throw. -Lemma no_throw_mem_builtins_7 Regs E1 E2 wk addr sz v s : - ignore_throw (E2 := E2) (@write_mem_bytesS Regs E1 wk addr sz v) s = write_mem_bytesS wk addr sz v s. +Lemma no_throw_mem_builtins_7 Regs E1 E2 wk addr sz v : + ignore_throw (E2 := E2) (@write_mem_bytesS Regs E1 wk addr sz v) === write_mem_bytesS wk addr sz v. unfold write_mem_bytesS. autorewrite with ignore_throw. reflexivity. Qed. Hint Rewrite no_throw_mem_builtins_7 : ignore_throw. -Lemma no_throw_mem_builtins_8 Regs E1 E2 A B wk addr sz v t s : - ignore_throw (E2 := E2) (@write_memtS Regs E1 A B wk addr sz v t) s = write_memtS wk addr sz v t s. +Lemma no_throw_mem_builtins_8 Regs E1 E2 A B wk addr sz v t : + ignore_throw (E2 := E2) (@write_memtS Regs E1 A B wk addr sz v t) === write_memtS wk addr sz v t. unfold write_memtS. rewrite ignore_throw_option_case_distrib_2. destruct (Sail2_values.mem_bytes_of_bits v); autorewrite with ignore_throw; auto. Qed. Hint Rewrite no_throw_mem_builtins_8 : ignore_throw. -Lemma no_throw_mem_builtins_9 Regs E1 E2 A B wk addr sz v s : - ignore_throw (E2 := E2) (@write_memS Regs E1 A B wk addr sz v) s = write_memS wk addr sz v s. +Lemma no_throw_mem_builtins_9 Regs E1 E2 A B wk addr sz v : + ignore_throw (E2 := E2) (@write_memS Regs E1 A B wk addr sz v) === write_memS wk addr sz v. unfold write_memS. autorewrite with ignore_throw; auto. Qed. Hint Rewrite no_throw_mem_builtins_9 : ignore_throw. -Lemma no_throw_mem_builtins_10 Regs E1 E2 s : - ignore_throw (E2 := E2) (@excl_resultS Regs E1 tt) s = excl_resultS tt s. +Lemma no_throw_mem_builtins_10 Regs E1 E2 : + ignore_throw (E2 := E2) (@excl_resultS Regs E1 tt) === excl_resultS tt. reflexivity. Qed. Hint Rewrite no_throw_mem_builtins_10 : ignore_throw. -Lemma no_throw_mem_builtins_11 Regs E1 E2 s : - ignore_throw (E2 := E2) (@undefined_boolS Regs E1 tt) s = undefined_boolS tt s. +Lemma no_throw_mem_builtins_11 Regs E1 E2 : + ignore_throw (E2 := E2) (@undefined_boolS Regs E1 tt) === undefined_boolS tt. reflexivity. Qed. Hint Rewrite no_throw_mem_builtins_11 : ignore_throw. -Lemma no_throw_read_regvalS Regs RV E1 E2 r reg_name s : - ignore_throw (E2 := E2) (@read_regvalS Regs RV E1 r reg_name) s = read_regvalS r reg_name s. +Lemma no_throw_read_regvalS Regs RV E1 E2 r reg_name : + ignore_throw (E2 := E2) (@read_regvalS Regs RV E1 r reg_name) === read_regvalS r reg_name. destruct r; simpl. autorewrite with ignore_throw. -apply bindS_ext_cong; intros; auto. rewrite ignore_throw_option_case_distrib_2. +apply bindS_cong; intros; auto. rewrite ignore_throw_option_case_distrib_2. autorewrite with ignore_throw. reflexivity. Qed. Hint Rewrite no_throw_read_regvalS : ignore_throw. -Lemma no_throw_write_regvalS Regs RV E1 E2 r reg_name v s : - ignore_throw (E2 := E2) (@write_regvalS Regs RV E1 r reg_name v) s = write_regvalS r reg_name v s. +Lemma no_throw_write_regvalS Regs RV E1 E2 r reg_name v : + ignore_throw (E2 := E2) (@write_regvalS Regs RV E1 r reg_name v) === write_regvalS r reg_name v. destruct r; simpl. autorewrite with ignore_throw. -apply bindS_ext_cong; intros; auto. rewrite ignore_throw_option_case_distrib_2. +apply bindS_cong; intros; auto. rewrite ignore_throw_option_case_distrib_2. autorewrite with ignore_throw. reflexivity. Qed. Hint Rewrite no_throw_write_regvalS : ignore_throw. |