diff options
| -rw-r--r-- | lib/coq/Hoare.v | 71 | ||||
| -rw-r--r-- | lib/coq/Sail2_state_lemmas.v | 283 | ||||
| -rw-r--r-- | lib/coq/Sail2_state_monad_lemmas.v | 39 |
3 files changed, 330 insertions, 63 deletions
diff --git a/lib/coq/Hoare.v b/lib/coq/Hoare.v index d23ff322..49b3afbb 100644 --- a/lib/coq/Hoare.v +++ b/lib/coq/Hoare.v @@ -1,4 +1,4 @@ -Require Import String ZArith. +Require Import String ZArith Setoid Morphisms Equivalence. Require Import Sail2_state_monad Sail2_prompt Sail2_state Sail2_state_monad_lemmas. Require Import Sail2_state_lemmas. @@ -425,7 +425,7 @@ Lemma PrePostE_bindS_unit Regs A Ety (P : predS Regs) (m : monadS Regs unit Ety) apply PrePost_bindS_unit. Qed. -Lemma PrePostE_readS (*[PrePostE_atomI, intro]:*) Regs A Ety (P : predS Regs) f (Q : result A Ety -> predS Regs) E : +Lemma PrePostE_readS (*[PrePostE_atomI, intro]:*) Regs A Ety f (Q : A -> predS Regs) E : PrePostE (Ety := Ety) (fun s => Q (f s) s) (readS f) Q E. unfold PrePostE, PrePost, readS. intros s Pre [a | e] s' [[= <- <-] | []]. @@ -445,6 +445,16 @@ Lemma PrePostE_if_branch (*[PrePostE_compositeI]:*) Regs A Ety (b : bool) (f g : destruct b; auto. Qed. +Lemma PrePostE_if_sum_branch (*[PrePostE_compositeI]:*) Regs A Ety X Y (b : sumbool X Y) (f g : monadS Regs A Ety) Pf Pg Q E : + (forall H : X, b = left H -> PrePostE Pf f Q E) -> + (forall H : Y, b = right H -> PrePostE Pg g Q E) -> + PrePostE (if b then Pf else Pg) (if b then f else g) Q E. +intros HX HY. +destruct b as [H | H]. +* apply (HX H). reflexivity. +* apply (HY H). reflexivity. +Qed. + Lemma PrePostE_if Regs A Ety (b : bool) (f g : monadS Regs A Ety) P Q E : (b = true -> PrePostE P f Q E) -> (b = false -> PrePostE P g Q E) -> @@ -808,3 +818,60 @@ eapply PrePostE_bindS with (R := fun _ s => forall x, List.In x xs -> Q x s). apply PrePostE_choose_boolsS_any. intuition. Qed. + +(* Setoid rewriting *) + +Local Open Scope equiv_scope. + +Add Parametric Morphism {Regs A Ety} : (@PrePost Regs A Ety) + with signature eq ==> equiv ==> eq ==> iff + as PrePost_morphism. +intros. +unfold PrePost. +split; intros H' s. +* rewrite <- (H s). apply H'. +* rewrite -> (H s). apply H'. +Qed. + +Add Parametric Morphism {Regs A Ety} : (@PrePostE Regs A Ety) + with signature eq ==> equiv ==> eq ==> eq ==> iff + as PrePostE_morphism. +intros. +unfold PrePostE. +rewrite H. +reflexivity. +Qed. + +(* Applying rewrites in a Hoare quadruple. For example, [PrePostE_rewrite liftState] + will push liftState through all of the monad operations. *) + +Lemma PrePostE_code_rw {Regs A Ety} P {Q : A -> predS Regs} {E : ex Ety -> predS Regs} {m m'} : + m === m' -> + PrePostE P m' Q E -> + PrePostE P m Q E. +intro H. +rewrite H. +auto. +Qed. + +Ltac PrePostE_rewrite db := (eapply PrePostE_code_rw; [ statecong db | ]). +Tactic Notation "PrePostE_rewrite" ident(db) := PrePostE_rewrite db. + +(* Attempt to do a weakest precondition calculation step. Assumes that goal has + a metavariable for the precondition. *) + +Ltac PrePostE_step := + match goal with + | |- PrePostE _ (bindS _ _) _ _ => eapply PrePostE_bindS; intros + (* The precondition will often have the form (?R x), and Coq's higher-order + unification will try to unify x and a if we don't explicitly tell it to + use Q to form the precondition to unify with P. *) + | |- PrePostE ?P (returnS ?a) ?Q _ => apply (PrePostE_returnS _ _ _ Q) + | |- PrePostE _ (if _ then _ else _) _ _ => + first + [ eapply PrePostE_if_branch; intros + | eapply PrePostE_if_sum_branch; intros + ] + | |- PrePostE _ (readS _) _ _ => apply PrePostE_readS + | |- PrePostE _ (assert_expS _ _) _ _ => apply PrePostE_assert_expS + end. diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v index a26b65d7..d1b7dfd5 100644 --- a/lib/coq/Sail2_state_lemmas.v +++ b/lib/coq/Sail2_state_lemmas.v @@ -3,6 +3,108 @@ Require Import Sail2_state_monad_lemmas. Local Open Scope equiv_scope. +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 vars. +induction xs. +* reflexivity. +* intros. simpl. + rewrite H. + apply bindS_cong; auto. +Qed. + +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. +Qed. + +Local Opaque _limit_reduces. +Ltac gen_reduces := + match goal with |- context[@_limit_reduces ?a ?b ?c] => generalize (@_limit_reduces a b c) end. + +Lemma whileST_cong {RV Vars E} vars measure cond cond' body body' : + (forall vars, cond vars === cond' vars) -> + (forall vars, body vars === body' vars) -> + @whileST RV Vars E vars measure cond body === whileST vars measure cond' body'. +intros Econd Ebody. +unfold whileST. +generalize (measure vars) as limit. intro. +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. + apply bindS_cong; auto. + intros [|]; auto. + apply bindS_cong; auto. + intros. destruct (_limit_reduces _). simpl. + reflexivity. + + clear limit H. + intros limit H IH [acc] vars s. simpl. + destruct (Z_ge_dec _ _); try omega. + apply bindS_cong; auto. + intros [|]; auto. + apply bindS_cong; auto. + intros. + gen_reduces. + replace (Z.succ limit - 1) with limit; try omega. intro acc'. + apply IH. + + assumption. +* intros. simpl. + destruct (Z_ge_dec _ _); try omega. + reflexivity. +Qed. + +Lemma untilST_cong RV Vars E measure vars cond cond' (body body' : Vars -> monadS RV Vars E) : + (forall vars, cond vars === cond' vars) -> + (forall vars, body vars === body' vars) -> + untilST vars measure cond body === untilST vars measure cond' body'. +intros Econd Ebody. +unfold untilST. +generalize (measure vars) as limit. intro. +revert vars. +destruct (Z.le_decidable 0 limit). +* generalize (Zwf_guarded limit) as acc. + apply Wf_Z.natlike_ind with (x := limit). + + intros [acc] * s; simpl. + apply bindS_cong; auto. + intros. apply bindS_cong; auto. + intros [|]; auto. + destruct (_limit_reduces _). simpl. + reflexivity. + + clear limit H. + intros limit H IH [acc] vars s. simpl. + destruct (Z_ge_dec _ _); try omega. + apply bindS_cong; auto. + intros. apply bindS_cong; auto. + intros [|]; auto. + gen_reduces. + replace (Z.succ limit - 1) with limit; try omega. intro acc'. + apply IH. + + assumption. +* intros. simpl. + destruct (Z_ge_dec _ _); try omega. + reflexivity. +Qed. + +Lemma genlistS_cong {A RV E} f f' n : + (forall i, f i === f' i) -> + @genlistS A RV E f n === genlistS f' n. +intro H. +apply foreachS_cong. +intros. rewrite H. +reflexivity. +Qed. + +Add Parametric Morphism {A RV E : Type} : (@genlistS A RV E) + with signature equiv ==> eq ==> equiv as genlistS_morphism. +intros f g EQ n. +apply genlistS_cong. +auto. +Qed. + (* 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} : @@ -10,18 +112,82 @@ Lemma liftState_bind Regval Regs A B E {r : Sail2_values.register_accessors Regs induction m; simpl; autorewrite with state; auto using bindS_cong. Qed. Hint Rewrite liftState_bind : liftState. +Hint Resolve 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). +(*Ltac rewrite_liftState := rewrite_strat topdown (choice (progress try hints liftState) progress eval cbn beta).*) + +(* Set up some rewriting under congruences. We would use + rewrite_strat for this, but there are some issues, such as #10661 + where rewriting under if fails. This is also the reason the hints + above use Resolve as well as Rewrite. These are intended for a + goal of the form `term === ?evar`, e.g., from applying + PrePostE_code_rw in Hoare. *) + +Lemma eq_equiv A R (x y : A) (H : Equivalence R) : + x = y -> @equiv A R H x y. +intro EQ; subst. +auto. +Qed. + +Local Ltac tryrw db := + try (etransitivity; [solve [eauto using eq_equiv with nocore db ] | ]; tryrw db). + +Lemma if_bool_cong A (R : relation A) `{H:Equivalence _ R} (x x' y y' : A) (c : bool) : + x === x' -> + y === y' -> + (if c then x else y) === if c then x' else y'. +intros E1 E2. +destruct c; auto. +Qed. + +Lemma if_sumbool_cong A P Q (R : relation A) `{H:Equivalence _ R} (x x' y y' : A) (c : sumbool P Q) : + x === x' -> + y === y' -> + (if c then x else y) === if c then x' else y'. +intros E1 E2. +destruct c; auto. +Qed. + +Ltac statecong db := + tryrw db; + lazymatch goal with + | |- (_ >>$= _) === _ => eapply bindS_cong; intros; statecong db + | |- (if ?x then _ else _) === _ => + solve [ eapply if_bool_cong; statecong db + | eapply if_sumbool_cong; statecong db + | apply equiv_reflexive] + | |- (foreachS _ _ _) === _ => + solve [ eapply foreachS_cong; intros; statecong db ] + | |- (genlistS _ _) === _ => + solve [ eapply genlistS_cong; intros; statecong db ] + | |- (whileST _ _ _ _) === _ => + solve [ eapply whileST_cong; intros; statecong db ] + | |- (untilST _ _ _ _) === _ => + solve [ eapply untilST_cong; intros; statecong db ] + | |- ?X => + solve + [ apply equiv_reflexive + | apply eq_equiv; apply equiv_reflexive + ] + end. +Tactic Notation "statecong" ident(dbs) := statecong dbs. + +Ltac rewrite_liftState := + match goal with + | |- context [liftState ?r ?tm] => + try let H := fresh "H" in (eassert (H:liftState r tm === _); [ statecong liftState | rewrite H; clear H]) + end. 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. Qed. Hint Rewrite liftState_return : liftState. +Hint Resolve liftState_return : liftState. (* Lemma Value_liftState_Run: @@ -37,10 +203,12 @@ 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. +Hint Resolve liftState_if_distrib : liftState. Lemma liftState_if_distrib_sumbool {Regs Regval A E P Q r x y} {c : sumbool P Q} : @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. +Hint Resolve liftState_if_distrib_sumbool : liftState. Lemma Value_bindS_iff {Regs A B E} {f : A -> monadS Regs B E} {b m s s''} : List.In (Value b, s'') (bindS m f s) <-> (exists a s', List.In (Value a, s') (m s) /\ List.In (Value b, s'') (f a s')). @@ -104,9 +272,7 @@ Qed. 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_cong; auto. -intros. rewrite liftState_if_distrib. +rewrite_liftState. reflexivity. Qed. Lemma liftState_and_boolMP Regs Regval E P Q R r x y H : @@ -155,6 +321,12 @@ Hint Rewrite liftState_throw liftState_assert liftState_exit liftState_exclResul liftState_and_boolM liftState_and_boolMP liftState_or_boolM liftState_or_boolMP : liftState. +Hint Resolve liftState_throw liftState_assert liftState_exit liftState_exclResult + liftState_barrier liftState_footprint liftState_choose_bool + liftState_undefined liftState_maybe_fail + liftState_and_boolM liftState_and_boolMP + liftState_or_boolM liftState_or_boolMP + : liftState. 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)). @@ -167,12 +339,14 @@ solve ]. Qed. Hint Rewrite liftState_try_catch : liftState. +Hint Resolve liftState_try_catch : liftState. Lemma liftState_early_return Regs Regval A R E r x : liftState (Regs := Regs) r (@early_return Regval A R E x) = early_returnS x. reflexivity. Qed. Hint Rewrite liftState_early_return : liftState. +Hint Resolve liftState_early_return : liftState. 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). @@ -182,6 +356,7 @@ apply try_catchS_cong; auto. intros [a | e] s'; auto. Qed. Hint Rewrite liftState_catch_early_return : liftState. +Hint Resolve liftState_catch_early_return : liftState. Lemma liftState_liftR Regs Regval A R E r m : liftState (Regs := Regs) r (@liftR Regval A R E m) === liftRS (liftState r m). @@ -190,6 +365,7 @@ rewrite_liftState. reflexivity. Qed. Hint Rewrite liftState_liftR : liftState. +Hint Resolve liftState_liftR : 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)). @@ -198,12 +374,14 @@ apply try_catchS_cong; auto. intros [r' | e] s'; auto. Qed. Hint Rewrite liftState_try_catchR : liftState. +Hint Resolve liftState_try_catchR : liftState. Lemma liftState_bool_of_bitU_nondet Regs Regval E r b : liftState (Regs := Regs) r (@bool_of_bitU_nondet Regval E b) = bool_of_bitU_nondetS b. destruct b; simpl; try reflexivity. Qed. Hint Rewrite liftState_bool_of_bitU_nondet : liftState. +Hint Resolve liftState_bool_of_bitU_nondet : liftState. 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. @@ -213,6 +391,7 @@ intros [byte bit]. destruct (option_map _); auto. Qed. Hint Rewrite liftState_read_memt : liftState. +Hint Resolve liftState_read_memt : liftState. 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. @@ -227,12 +406,14 @@ rewrite bindS_returnS_left. rewrite_liftState. destruct (option_map _); auto. Qed. Hint Rewrite liftState_read_mem : liftState. +Hint Resolve liftState_read_mem : liftState. Lemma liftState_write_mem_ea Regs Regval A E rk asz a sz r : liftState (Regs := Regs) r (@write_mem_ea Regval A E rk asz a sz) = returnS tt. reflexivity. Qed. Hint Rewrite liftState_write_mem_ea : liftState. +Hint Resolve liftState_write_mem_ea : liftState. Lemma liftState_write_memt Regs Regval A B E wk addr sz v t r : liftState (Regs := Regs) r (@write_memt Regval A B E wk addr sz v t) = write_memtS wk addr sz v t. @@ -240,6 +421,7 @@ unfold write_memt, write_memtS. destruct (Sail2_values.mem_bytes_of_bits v); auto. Qed. Hint Rewrite liftState_write_memt : liftState. +Hint Resolve liftState_write_memt : liftState. Lemma liftState_write_mem Regs Regval A B E wk addrsize addr sz v r : liftState (Regs := Regs) r (@write_mem Regval A B E wk addrsize addr sz v) = write_memS wk addr sz v. @@ -247,6 +429,7 @@ unfold write_mem, write_memS, write_memtS. destruct (Sail2_values.mem_bytes_of_bits v); simpl; auto. Qed. Hint Rewrite liftState_write_mem : liftState. +Hint Resolve liftState_write_mem : liftState. Lemma bindS_rw_left Regs A B E m1 m2 (f : A -> monadS Regs B E) s : m1 s = m2 s -> @@ -270,6 +453,19 @@ rewrite H. reflexivity. Qed. +(* Generic tactic to apply liftState to register reads, so that we don't have to + generate lots of model-specific lemmas. This takes advantage of the fact that + if you fix the register then the lemma above is trivial by convertability. *) + +Ltac lift_read_reg := + match goal with + | |- context [liftState ?r (@read_reg ?s ?rv ?a ?e ?ref)] => + let f := eval simpl in (fun x => (read_from ref) (ss_regstate x)) in + change (liftState r (@read_reg s rv a e ref)) with (@readS s a e f) + end. + +Hint Extern 1 (liftState _ (read_reg _) === _) => lift_read_reg; reflexivity : liftState. + 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) === updateS (fun s => {| ss_regstate := (write_to reg v s.(ss_regstate)); ss_memstate := s.(ss_memstate); ss_tagstate := s.(ss_tagstate) |}). @@ -291,6 +487,7 @@ Lemma liftState_iter_aux Regs Regval A E : by (induction i "\<lambda>i x. liftState r (f i x)" xs rule: iterS_aux.induct) (auto simp: liftState_simp cong: bindS_cong) Hint Rewrite liftState_iter_aux : liftState. +Hint Resolve liftState_iter_aux : liftState. lemma liftState_iteri[liftState_simp]: "liftState r (iteri f xs) = iteriS (\<lambda>i x. liftState r (f i x)) xs" @@ -310,26 +507,7 @@ induction xs as [ | h t]. apply bindS_cong; auto. Qed. Hint Rewrite liftState_foreachM : liftState. - -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 vars. -induction xs. -* reflexivity. -* intros. simpl. - rewrite H. - apply bindS_cong; auto. -Qed. - -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. -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).*) +Hint Resolve liftState_foreachM : liftState. 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. @@ -338,16 +516,7 @@ rewrite_liftState. reflexivity. Qed. Hint Rewrite liftState_genlistM : liftState. - -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. +Hint Resolve liftState_genlistM : liftState. Lemma liftState_choose_bools Regs Regval E descr n r : liftState (Regs := Regs) r (@choose_bools Regval E descr n) === choose_boolsS n. @@ -356,6 +525,7 @@ rewrite_liftState. reflexivity. Qed. Hint Rewrite liftState_choose_bools : liftState. +Hint Resolve liftState_choose_bools : liftState. Lemma liftState_bools_of_bits_nondet Regs Regval E r bs : liftState (Regs := Regs) r (@bools_of_bits_nondet Regval E bs) === bools_of_bits_nondetS bs. @@ -364,6 +534,7 @@ rewrite_liftState. reflexivity. Qed. Hint Rewrite liftState_bools_of_bits_nondet : liftState. +Hint Resolve liftState_bools_of_bits_nondet : liftState. 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. @@ -375,6 +546,7 @@ intros. destruct (nth_error _ _); auto. Qed. Hint Rewrite liftState_internal_pick : liftState. +Hint Resolve liftState_internal_pick : liftState. Lemma liftRS_returnS (*[simp]:*) A R Regs E x : @liftRS A R Regs E (returnS x) = returnS x. @@ -493,12 +665,6 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState qed *) -Local Opaque _limit_reduces. -Ltac gen_reduces := - match goal with |- context[@_limit_reduces ?a ?b ?c] => generalize (@_limit_reduces a b c) end. - -(* 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)). @@ -511,20 +677,18 @@ destruct (Z.le_decidable 0 limit). + intros [acc] *; simpl. 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. + intros [|]; auto. apply bindS_cong; auto. intros. destruct (_limit_reduces _). simpl. reflexivity. + clear limit H. intros limit H IH [acc] vars s. simpl. destruct (Z_ge_dec _ _); try omega. - autorewrite with liftState. - apply bindS_ext_cong; auto. - intros. rewrite liftState_if_distrib. - destruct a; autorewrite with liftState; auto. - apply bindS_ext_cong; auto. + rewrite_liftState. + apply bindS_cong; auto. + intros [|]; auto. + apply bindS_cong; auto. intros. gen_reduces. replace (Z.succ limit - 1) with limit; try omega. intro acc'. @@ -534,6 +698,7 @@ destruct (Z.le_decidable 0 limit). destruct (Z_ge_dec _ _); try omega. reflexivity. Qed. +Hint Resolve liftState_whileM : liftState. (* lemma untilM_dom_step: @@ -583,24 +748,19 @@ destruct (Z.le_decidable 0 limit). * generalize (Zwf_guarded limit) as acc. apply Wf_Z.natlike_ind with (x := limit). + intros [acc] * s; simpl. -(* TODO rewrite_liftState.*) -autorewrite with liftState. - apply bindS_ext_cong; auto. - intros. autorewrite with liftState. - apply bindS_ext_cong; auto. - intros. rewrite liftState_if_distrib. - destruct a0; auto. + rewrite_liftState. + apply bindS_cong; auto. + intros. apply bindS_cong; auto. + intros [|]; auto. destruct (_limit_reduces _). simpl. reflexivity. + clear limit H. intros limit H IH [acc] vars s. simpl. destruct (Z_ge_dec _ _); try omega. - autorewrite with liftState. - apply bindS_ext_cong; auto. - intros. autorewrite with liftState; auto. - apply bindS_ext_cong; auto. - intros. rewrite liftState_if_distrib. - destruct a0; autorewrite with liftState; auto. + rewrite_liftState. + apply bindS_cong; auto. + intros. apply bindS_cong; auto. + intros [|]; auto. gen_reduces. replace (Z.succ limit - 1) with limit; try omega. intro acc'. apply IH. @@ -609,6 +769,7 @@ autorewrite with liftState. destruct (Z_ge_dec _ _); try omega. reflexivity. Qed. +Hint Resolve liftState_untilM : liftState. (* @@ -817,4 +978,4 @@ lemma get_mem_bytes_tagged_tagstate: by (auto simp: get_mem_bytes_def foldl_and_bit_eq_iff Let_def split: option.splits) end -*)
\ No newline at end of file +*) diff --git a/lib/coq/Sail2_state_monad_lemmas.v b/lib/coq/Sail2_state_monad_lemmas.v index 99fef329..e9ab36c1 100644 --- a/lib/coq/Sail2_state_monad_lemmas.v +++ b/lib/coq/Sail2_state_monad_lemmas.v @@ -3,6 +3,13 @@ Require Import Sail2_state_monad. Require Export Setoid. Require Export Morphisms Equivalence. +(* Basic results for reasoning about definitions which use the state monad. + + Note that rewriting results are put into both a rewriting hint database and + a normal automation one. The former can be used with autorewrite and friends, + but the latter can be used with the rewriting under congruence tactics, such as + statecong in Sail2_state_lemmas, and PrePostE_rewrite in Hoare. *) + (* Ensure that pointwise equality on states is the preferred notion of equivalence for the state monad. *) Local Open Scope equiv_scope. @@ -18,6 +25,8 @@ 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 : m1 s = m2 s -> @@ -55,6 +64,7 @@ simpl. auto using List.app_nil_r. Qed. Hint Rewrite bindS_returnS_left : state. +Hint Resolve bindS_returnS_left : state. Lemma bindS_returnS_right Regs A E {m : monadS Regs A E} : bindS m returnS === m. @@ -66,6 +76,7 @@ rewrite IHt; reflexivity. Qed. Hint Rewrite bindS_returnS_right : state. +Hint Resolve 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. @@ -90,6 +101,7 @@ simpl. auto using List.app_nil_r. Qed. Hint Rewrite bindS_assertS_true : state. +Hint Resolve bindS_assertS_true : state. 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). @@ -100,6 +112,7 @@ simpl. rewrite IHxs. reflexivity. Qed. Hint Rewrite bindS_chooseS_returnS : state. +Hint Resolve bindS_chooseS_returnS : state. Lemma result_cases : forall (A E : Type) (P : result A E -> Prop), (forall a, P (Value a)) -> @@ -191,18 +204,21 @@ induction (m s) as [ | [[a | e] t]]. * simpl. rewrite IHl. reflexivity. Qed. Hint Rewrite bindS_assoc : state. +Hint Resolve bindS_assoc : state. Lemma bindS_failS Regs A B E {msg} {f : A -> monadS Regs B E} : bindS (failS msg) f = failS msg. reflexivity. Qed. Hint Rewrite bindS_failS : state. +Hint Resolve 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. +Hint Resolve bindS_throwS : state. (*declare seqS_def[simp]*) Lemma seqS_def Regs A E m (m' : monadS Regs A E) : @@ -210,6 +226,7 @@ Lemma seqS_def Regs A E m (m' : monadS Regs A E) : reflexivity. Qed. Hint Rewrite seqS_def : state. +Hint Resolve 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) -> @@ -235,11 +252,13 @@ Lemma try_catchS_returnS Regs A E1 E2 {a} {h : E1 -> monadS Regs A E2}: reflexivity. Qed. Hint Rewrite try_catchS_returnS : state. +Hint Resolve 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. Hint Rewrite try_catchS_failS : state. +Hint Resolve 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. @@ -248,6 +267,7 @@ simpl. auto using List.app_nil_r. Qed. Hint Rewrite try_catchS_throwS : state. +Hint Resolve try_catchS_throwS : state. Lemma try_catchS_cong (*[cong]:*) {Regs A E1 E2 m1 m2} {h1 h2 : E1 -> monadS Regs A E2} : m1 === m2 -> @@ -385,6 +405,7 @@ induction (m s) as [ | [[a | [e | msg]] t]]. * simpl. apply IHl. Qed. Hint Rewrite ignore_throw_bindS : ignore_throw. +Hint Resolve 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 _} {h} : ignore_throw m1 === m1 -> @@ -445,6 +466,10 @@ Hint Rewrite no_throw_basic_builtins_1 no_throw_basic_builtins_2 no_throw_basic_builtins_3 no_throw_basic_builtins_4 no_throw_basic_builtins_5 no_throw_basic_builtins_6 no_throw_basic_builtins_7 : ignore_throw. +Hint Resolve no_throw_basic_builtins_1 no_throw_basic_builtins_2 + no_throw_basic_builtins_3 no_throw_basic_builtins_4 + no_throw_basic_builtins_5 no_throw_basic_builtins_6 + no_throw_basic_builtins_7 : ignore_throw. Lemma ignore_throw_option_case_distrib_1 Regs B C E1 E2 (c : sequential_state Regs -> option B) s (n : monadS Regs C E1) (f : B -> monadS Regs C E1) : ignore_throw (E2 := E2) (match c s with None => n | Some b => f b end) s = @@ -468,6 +493,7 @@ unfold read_memt_bytesS. autorewrite with ignore_throw. apply bindS_cong; auto. intros. autorewrite with ignore_throw. reflexivity. Qed. Hint Rewrite no_throw_mem_builtins_1 : ignore_throw. +Hint Resolve no_throw_mem_builtins_1 : ignore_throw. 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. @@ -475,10 +501,12 @@ apply bindS_cong; intros; autorewrite with ignore_throw; auto. destruct a0; reflexivity. Qed. Hint Rewrite no_throw_mem_builtins_2 : ignore_throw. +Hint Resolve no_throw_mem_builtins_2 : ignore_throw. 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. +Hint Resolve no_throw_mem_builtins_3 : ignore_throw. 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. @@ -487,6 +515,7 @@ reflexivity. destruct a0; simpl. autorewrite with ignore_throw. reflexivity. Qed. Hint Rewrite no_throw_mem_builtins_4 : ignore_throw. +Hint Resolve no_throw_mem_builtins_4 : ignore_throw. 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. @@ -494,36 +523,43 @@ apply bindS_cong; intros; autorewrite with ignore_throw; auto. destruct a0; auto. Qed. Hint Rewrite no_throw_mem_builtins_5 : ignore_throw. +Hint Resolve no_throw_mem_builtins_5 : ignore_throw. 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. +Hint Resolve no_throw_mem_builtins_6 : ignore_throw. 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. +Hint Resolve no_throw_mem_builtins_7 : ignore_throw. 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. +Hint Resolve no_throw_mem_builtins_8 : ignore_throw. 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. +Hint Resolve no_throw_mem_builtins_9 : ignore_throw. 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. +Hint Resolve no_throw_mem_builtins_10 : ignore_throw. 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. +Hint Resolve no_throw_mem_builtins_11 : ignore_throw. 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. @@ -532,6 +568,7 @@ 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. +Hint Resolve no_throw_read_regvalS : ignore_throw. 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. @@ -540,3 +577,5 @@ 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. +Hint Resolve no_throw_write_regvalS : ignore_throw. + |