diff options
| -rw-r--r-- | lib/coq/Hoare.v | 193 | ||||
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 77 | ||||
| -rw-r--r-- | lib/coq/Sail2_state.v | 45 | ||||
| -rw-r--r-- | lib/coq/Sail2_state_lemmas.v | 194 | ||||
| -rw-r--r-- | lib/coq/Sail2_state_monad.v | 3 |
5 files changed, 455 insertions, 57 deletions
diff --git a/lib/coq/Hoare.v b/lib/coq/Hoare.v index 49b3afbb..2f16547b 100644 --- a/lib/coq/Hoare.v +++ b/lib/coq/Hoare.v @@ -103,6 +103,16 @@ eapply PrePost_bindS with (R := fun _ => R). * apply M. Qed. +Lemma PrePost_seqS Regs B E (m : monadS Regs unit E) (m' : monadS Regs B E) P Q R : + PrePost R m' Q -> + PrePost P m (fun r => match r with Value a => R | Ex e => Q (Ex e) end) -> + PrePost P (seqS m m') Q. +intros F M. +eapply PrePost_bindS with (R := fun _ => R). +* intros. destruct a. apply F. +* apply M. +Qed. + Lemma PrePost_readS (*[intro, PrePost_atomI]:*) Regs A E (P : result A E -> predS Regs) f : PrePost (fun s => P (Value (f s)) s) (readS f) P. unfold PrePost, readS, returnS. @@ -182,6 +192,34 @@ eapply PrePost_bindS. apply PrePost_returnS. Qed. +Lemma PrePost_and_boolSP (*[PrePost_compositeI]:*) Regs E PP QQ RR H + (l : monadS Regs {b : bool & Sail2_values.ArithFact (PP b)} E) + (r : monadS Regs {b : bool & Sail2_values.ArithFact (QQ b)} E) + P (Q : result {b : bool & Sail2_values.ArithFact (RR b)} E -> predS Regs) R : + (forall p, + PrePost R r + (fun r => + match r with + | Value (existT _ r q) => Q (Value (existT _ r (and_bool_full_proof p q H))) + | Ex e => Q (Ex e) end)) -> + PrePost P l + (fun r => match r with + | Value (existT _ true _) => R + | Value (existT _ false p) => Q (Value (existT _ _ (and_bool_left_proof p H))) + | Ex e => Q (Ex e) end) -> + PrePost P (@and_boolSP _ _ PP QQ RR l r H) Q. +intros Hr Hl. +unfold and_boolSP. +eapply (PrePost_bindS _ _ _ _ _ _ _ _ _ _ Hl). +Unshelve. +intros s [[|] p] s' IN. +* eapply PrePost_bindS. 2: apply Hr. + clear s s' IN. + intros s [b q] s' IN. + apply PrePost_returnS. +* apply PrePost_returnS. +Qed. + Lemma PrePost_or_boolS (*[PrePost_compositeI]:*) Regs E (l r : monadS Regs bool E) P Q R : PrePost R r Q -> PrePost P l (fun r => match r with Value false => R | _ => Q r end) -> @@ -198,6 +236,34 @@ eapply PrePost_bindS. intros [[|] | ] s H; auto. Qed. +Lemma PrePost_or_boolSP (*[PrePost_compositeI]:*) Regs E PP QQ RR H + (l : monadS Regs {b : bool & Sail2_values.ArithFact (PP b)} E) + (r : monadS Regs {b : bool & Sail2_values.ArithFact (QQ b)} E) + P (Q : result {b : bool & Sail2_values.ArithFact (RR b)} E -> predS Regs) R : + (forall p, + PrePost R r + (fun r => + match r with + | Value (existT _ r q) => Q (Value (existT _ r (or_bool_full_proof p q H))) + | Ex e => Q (Ex e) end)) -> + PrePost P l + (fun r => match r with + | Value (existT _ false _) => R + | Value (existT _ true p) => Q (Value (existT _ _ (or_bool_left_proof p H))) + | Ex e => Q (Ex e) end) -> + PrePost P (@or_boolSP _ _ PP QQ RR l r H) Q. +intros Hr Hl. +unfold or_boolSP. +eapply (PrePost_bindS _ _ _ _ _ _ _ _ _ _ Hl). +Unshelve. +intros s [[|] p] s' IN. +* apply PrePost_returnS. +* eapply PrePost_bindS. 2: apply Hr. + clear s s' IN. + intros s [b q] s' IN. + apply PrePost_returnS. +Qed. + Lemma PrePost_failS (*[intro, PrePost_atomI]:*) Regs A E msg (Q : result A E -> predS Regs) : PrePost (Q (Ex (Failure msg))) (failS msg) Q. intros s Pre r s' [[= <- <-] | []]. @@ -425,6 +491,13 @@ Lemma PrePostE_bindS_unit Regs A Ety (P : predS Regs) (m : monadS Regs unit Ety) apply PrePost_bindS_unit. Qed. +Lemma PrePostE_seqS Regs A Ety (P : predS Regs) (m : monadS Regs unit Ety) (m' : monadS Regs A Ety) Q R E : + PrePostE R m' Q E -> + PrePostE P m (fun _ => R) E -> + PrePostE P (seqS m m') Q E. +apply PrePost_seqS. +Qed. + 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. @@ -516,6 +589,30 @@ eapply PrePostE_bindS. * assumption. Qed. +Lemma PrePostE_and_boolSP (*[PrePost_compositeI]:*) Regs Ety PP QQ RR H + (l : monadS Regs {b : bool & Sail2_values.ArithFact (PP b)} Ety) + (r : monadS Regs {b : bool & Sail2_values.ArithFact (QQ b)} Ety) + P (Q : {b : bool & Sail2_values.ArithFact (RR b)} -> predS Regs) E R : + PrePostE R r (fun '(existT _ r _) s => forall pf, Q (existT _ r pf) s) E -> + PrePostE P l + (fun r => match r with + | existT _ true _ => R + | existT _ false _ => (fun s => forall pf, Q (existT _ false pf) s) + end) E -> + PrePostE P (@and_boolSP _ _ PP QQ RR l r H) Q E. +intros Hr Hl. +unfold and_boolSP. +refine (PrePostE_bindS _ _ _ _ _ _ _ _ _ _ _ Hl). +intros s [[|] p] s' IN. +* eapply PrePostE_bindS. 2: apply Hr. + clear s s' IN. + intros s [b q] s' IN. + eapply PrePostE_strengthen_pre. apply PrePostE_returnS. + intros s1 HQ. apply HQ. +* eapply PrePostE_strengthen_pre. apply PrePostE_returnS. + intros s1 HQ. apply HQ. +Qed. + Lemma PrePostE_or_boolS (*[PrePostE_compositeI]:*) Regs Ety (l r : monadS Regs bool Ety) P Q R E : PrePostE R r Q E -> PrePostE P l (fun r => if r then Q true else R) E -> @@ -530,6 +627,30 @@ eapply PrePostE_bindS. * assumption. Qed. +Lemma PrePostE_or_boolSP (*[PrePost_compositeI]:*) Regs Ety PP QQ RR H + (l : monadS Regs {b : bool & Sail2_values.ArithFact (PP b)} Ety) + (r : monadS Regs {b : bool & Sail2_values.ArithFact (QQ b)} Ety) + P (Q : {b : bool & Sail2_values.ArithFact (RR b)} -> predS Regs) E R : + PrePostE R r (fun '(existT _ r _) s => forall pf, Q (existT _ r pf) s) E -> + PrePostE P l + (fun r => match r with + | existT _ false _ => R + | existT _ true _ => (fun s => forall pf, Q (existT _ true pf) s) + end) E -> + PrePostE P (@or_boolSP _ _ PP QQ RR l r H) Q E. +intros Hr Hl. +unfold or_boolSP. +refine (PrePostE_bindS _ _ _ _ _ _ _ _ _ _ _ Hl). +intros s [[|] p] s' IN. +* eapply PrePostE_strengthen_pre. apply PrePostE_returnS. + intros s1 HQ. apply HQ. +* eapply PrePostE_bindS. 2: apply Hr. + clear s s' IN. + intros s [b q] s' IN. + eapply PrePostE_strengthen_pre. apply PrePostE_returnS. + intros s1 HQ. apply HQ. +Qed. + Lemma PrePostE_failS (*[PrePostE_atomI, intro]:*) Regs A Ety msg (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : PrePostE (E (Failure msg)) (failS msg) Q E. unfold PrePostE, PrePost, failS. @@ -543,6 +664,15 @@ unfold assert_expS. destruct c; auto using PrePostE_returnS, PrePostE_failS. Qed. +Lemma PrePostE_assert_expS' (*[PrePostE_atomI, intro]:*) Regs Ety (c : bool) m (P : c = true -> predS Regs) (Q : ex Ety -> predS Regs) : + PrePostE (if c then (fun s => forall pf, P pf s) else Q (Failure m)) (assert_expS' c m) P Q. +unfold assert_expS'. +destruct c. +* eapply PrePostE_strengthen_pre. eapply PrePostE_returnS. + auto. +* auto using PrePostE_failS. +Qed. + Lemma PrePostE_maybe_failS (*[PrePostE_atomI]:*) Regs A Ety msg v (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : PrePostE (fun s => match v with Some v => Q v s | None => E (Failure msg) s end) (maybe_failS msg v) Q E. unfold maybe_failS. @@ -819,6 +949,46 @@ eapply PrePostE_bindS with (R := fun _ s => forall x, List.In x xs -> Q x s). intuition. Qed. +Lemma PrePostE_undefined_word_natS_any Regs Ety n (Q : Word.word n -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE (fun s => forall w, Q w s) (undefined_word_natS n) Q E. +induction n. +* simpl. + eapply PrePostE_strengthen_pre. + apply PrePostE_returnS. + auto. +* simpl. + eapply PrePostE_strengthen_pre. + eapply PrePostE_bindS; intros. + eapply PrePostE_bindS; intros. + apply (PrePostE_returnS _ _ _ Q). + apply IHn. + apply PrePostE_choose_boolS_any. + simpl. auto. +Qed. + +Local Open Scope Z. + +Lemma PrePostE_undefined_bitvectorS_any Regs Ety n `{Sail2_values.ArithFact (n >= 0)} (Q : Sail2_values.mword n -> predS Regs) (E : ex Ety -> predS Regs) : + PrePostE (fun s => forall w, Q w s) (undefined_bitvectorS n) Q E. +unfold undefined_bitvectorS. +eapply PrePostE_strengthen_pre. +eapply PrePostE_bindS; intros. +apply (PrePostE_returnS _ _ _ Q). +apply PrePostE_undefined_word_natS_any. +simpl. +auto. +Qed. + +Lemma PrePostE_build_trivial_exS Regs (T:Type) Ety (m : monadS Regs T Ety) P (Q : {T & Sail2_values.ArithFact True} -> predS Regs) E : + PrePostE P m (fun v => Q (existT _ v (Sail2_values.Build_ArithFact _ I))) E -> + PrePostE P (build_trivial_exS m) Q E. +intro H. +unfold build_trivial_exS. +eapply PrePostE_bindS; intros. +* apply (PrePostE_returnS _ _ _ Q). +* apply H. +Qed. + (* Setoid rewriting *) Local Open Scope equiv_scope. @@ -860,9 +1030,13 @@ 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. *) +Create HintDb PrePostE_specs. + Ltac PrePostE_step := match goal with + | |- _ => solve [ clear; eauto with nocore PrePostE_specs ] | |- PrePostE _ (bindS _ _) _ _ => eapply PrePostE_bindS; intros + | |- PrePostE _ (seqS _ _) _ _ => eapply PrePostE_seqS; 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. *) @@ -874,4 +1048,23 @@ Ltac PrePostE_step := ] | |- PrePostE _ (readS _) _ _ => apply PrePostE_readS | |- PrePostE _ (assert_expS _ _) _ _ => apply PrePostE_assert_expS + | |- PrePostE _ (assert_expS' _ _) _ _ => apply PrePostE_assert_expS' + | |- PrePostE _ (exitS _) _ ?E => apply (PrePostE_exitS _ _ _ _ _ E) + | |- PrePostE _ (and_boolS _ _) _ _ => eapply PrePostE_and_boolS + | |- PrePostE _ (or_boolS _ _) _ _ => eapply PrePostE_or_boolS + | |- PrePostE _ (and_boolSP _ _) _ _ => eapply PrePostE_and_boolSP; intros + | |- PrePostE _ (or_boolSP _ _) _ _ => eapply PrePostE_or_boolSP; intros + | |- PrePostE _ (build_trivial_exS _) _ _ => eapply PrePostE_build_trivial_exS; intros + | |- PrePostE _ (let '(_,_) := ?x in _) _ _ => + is_var x; + let PAIR := fresh "PAIR" in + assert (PAIR : x = (fst x, snd x)) by (destruct x; reflexivity); + rewrite PAIR at - 1; + clear PAIR + | |- PrePostE _ (let '(existT _ _ _) := ?x in _) _ _ => + is_var x; + let PAIR := fresh "PAIR" in + assert (PAIR : x = existT _ (projT1 x) (projT2 x)) by (destruct x; reflexivity); + rewrite PAIR at - 1; + clear PAIR end. diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 1c2a1b26..d2a8c805 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -61,34 +61,71 @@ Definition genlistM {A RV E} (f : nat -> monad RV A E) (n : nat) : monad RV (lis Definition and_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E := l >>= (fun l => if l then r else returnm false). +(* We introduce explicit definitions for these proofs so that they can be used in + the state monad and program logic rules. They are not currently used in the proof + rules because it was more convenient to quantify over them instead. *) +Definition and_bool_left_proof {P Q R:bool -> Prop} : + ArithFact (P false) -> + ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r)) -> + ArithFact (R false). +intros [p] [h]. +constructor. +change false with (andb false false). +apply h; auto. +congruence. +Qed. + +Definition and_bool_full_proof {P Q R:bool -> Prop} {r} : + ArithFact (P true) -> + ArithFact (Q r) -> + ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r)) -> + ArithFact (R r). +intros [p] [q] [h]. +constructor. +change r with (andb true r). +apply h; auto. +Qed. + Definition and_boolMP {rv E} {P Q R:bool->Prop} (x : monad rv {b:bool & ArithFact (P b)} E) (y : monad rv {b:bool & ArithFact (Q b)} E) `{H:ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r))} - : monad rv {b:bool & ArithFact (R b)} E. -refine ( - x >>= fun '(existT _ x (Build_ArithFact _ p)) => (if x return P x -> _ then - fun p => y >>= fun '(existT _ y _) => returnm (existT _ y _) - else fun p => returnm (existT _ false _)) p -). -* constructor. destruct H. destruct a0. change y with (andb true y). auto. -* constructor. destruct H. change false with (andb false false). apply fact. - assumption. - congruence. -Defined. + : monad rv {b:bool & ArithFact (R b)} E := + x >>= fun '(existT _ x p) => (if x return ArithFact (P x) -> _ then + fun p => y >>= fun '(existT _ y q) => returnm (existT _ y (and_bool_full_proof p q H)) + else fun p => returnm (existT _ false (and_bool_left_proof p H))) p. (*val or_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e*) Definition or_boolM {rv E} (l : monad rv bool E) (r : monad rv bool E) : monad rv bool E := l >>= (fun l => if l then returnm true else r). + + +Definition or_bool_left_proof {P Q R:bool -> Prop} : + ArithFact (P true) -> + ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r)) -> + ArithFact (R true). +intros [p] [h]. +constructor. +change true with (orb true false). +apply h; auto. +congruence. +Qed. + +Definition or_bool_full_proof {P Q R:bool -> Prop} {r} : + ArithFact (P false) -> + ArithFact (Q r) -> + ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r)) -> + ArithFact (R r). +intros [p] [q] [h]. +constructor. +change r with (orb false r). +apply h; auto. +Qed. + Definition or_boolMP {rv E} {P Q R:bool -> Prop} (l : monad rv {b : bool & ArithFact (P b)} E) (r : monad rv {b : bool & ArithFact (Q b)} E) `{ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r))} - : monad rv {b : bool & ArithFact (R b)} E. -refine ( - l >>= fun '(existT _ l (Build_ArithFact _ p)) => - (if l return P l -> _ then fun p => returnm (existT _ true _) - else fun p => r >>= fun '(existT _ r _) => returnm (existT _ r _)) p -). -* constructor. destruct H. change true with (orb true true). apply fact. assumption. congruence. -* constructor. destruct H. destruct a0. change r with (orb false r). auto. -Defined. + : monad rv {b : bool & ArithFact (R b)} E := + l >>= fun '(existT _ l p) => + (if l return ArithFact (P l) -> _ then fun p => returnm (existT _ true (or_bool_left_proof p H)) + else fun p => r >>= fun '(existT _ r q) => returnm (existT _ r (or_bool_full_proof p q H))) p. Definition build_trivial_ex {rv E} {T:Type} (x:monad rv T E) : monad rv {x : T & ArithFact True} E := x >>= fun x => returnm (existT _ x (Build_ArithFact _ I)). diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v index dc635cb4..7a25cbe9 100644 --- a/lib/coq/Sail2_state.v +++ b/lib/coq/Sail2_state.v @@ -45,28 +45,20 @@ Definition or_boolS {RV E} (l r : monadS RV bool E) : monadS RV bool E := Definition and_boolSP {rv E} {P Q R:bool->Prop} (x : monadS rv {b:bool & ArithFact (P b)} E) (y : monadS rv {b:bool & ArithFact (Q b)} E) `{H:ArithFact (forall l r, P l -> (l = true -> Q r) -> R (andb l r))} - : monadS rv {b:bool & ArithFact (R b)} E. -refine ( - x >>$= fun '(existT _ x (Build_ArithFact _ p)) => (if x return P x -> _ then - fun p => y >>$= fun '(existT _ y _) => returnS (existT _ y _) - else fun p => returnS (existT _ false _)) p -). -* constructor. destruct H. destruct a0. change y with (andb true y). auto. -* constructor. destruct H. change false with (andb false false). apply fact. - assumption. - congruence. -Defined. + : monadS rv {b:bool & ArithFact (R b)} E := + x >>$= fun '(existT _ x p) => (if x return ArithFact (P x) -> _ then + fun p => y >>$= fun '(existT _ y q) => returnS (existT _ y (and_bool_full_proof p q H)) + else fun p => returnS (existT _ false (and_bool_left_proof p H))) p. + Definition or_boolSP {rv E} {P Q R:bool -> Prop} (l : monadS rv {b : bool & ArithFact (P b)} E) (r : monadS rv {b : bool & ArithFact (Q b)} E) `{ArithFact (forall l r, P l -> (l = false -> Q r) -> R (orb l r))} - : monadS rv {b : bool & ArithFact (R b)} E. -refine ( - l >>$= fun '(existT _ l (Build_ArithFact _ p)) => - (if l return P l -> _ then fun p => returnS (existT _ true _) - else fun p => r >>$= fun '(existT _ r _) => returnS (existT _ r _)) p -). -* constructor. destruct H. change true with (orb true true). apply fact. assumption. congruence. -* constructor. destruct H. destruct a0. change r with (orb false r). auto. -Defined. + : monadS rv {b : bool & ArithFact (R b)} E := + l >>$= fun '(existT _ l p) => + (if l return ArithFact (P l) -> _ then fun p => returnS (existT _ true (or_bool_left_proof p H)) + else fun p => r >>$= fun '(existT _ r q) => returnS (existT _ r (or_bool_full_proof p q H))) p. + +Definition build_trivial_exS {rv E} {T:Type} (x : monadS rv T E) : monadS rv {x : T & ArithFact True} E := + x >>$= fun x => returnS (existT _ x (Build_ArithFact _ I)). (*val bool_of_bitU_fail : forall 'rv 'e. bitU -> monadS 'rv bool 'e*) Definition bool_of_bitU_fail {RV E} (b : bitU) : monadS RV bool E := @@ -164,4 +156,17 @@ Definition internal_pickS {RV A E} (xs : list A) : monadS RV A E := | None => failS "choose internal_pick" end. +Fixpoint undefined_word_natS {rv e} n : monadS rv (Word.word n) e := + match n with + | O => returnS Word.WO + | S m => + choose_boolS tt >>$= fun b => + undefined_word_natS m >>$= fun t => + returnS (Word.WS b t) + end. + +Definition undefined_bitvectorS {rv e} n `{ArithFact (n >= 0)} : monadS rv (mword n) e := + undefined_word_natS (Z.to_nat n) >>$= fun w => + returnS (word_to_mword w). + diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v index d1b7dfd5..49d35770 100644 --- a/lib/coq/Sail2_state_lemmas.v +++ b/lib/coq/Sail2_state_lemmas.v @@ -3,6 +3,14 @@ Require Import Sail2_state_monad_lemmas. Local Open Scope equiv_scope. +Lemma seqS_cong A RV E (m1 m1' : monadS RV unit E) (m2 m2' : monadS RV A E) : + m1 === m1' -> + m2 === m2' -> + m1 >>$ m2 === m1' >>$ m2'. +unfold seqS. +auto using bindS_cong. +Qed. + 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'. @@ -105,6 +113,57 @@ apply genlistS_cong. auto. Qed. +Lemma and_boolS_cong {RV E} x x' y y' : + x === x' -> + y === y' -> + @and_boolS RV E x y === and_boolS x' y'. +intros E1 E2. +unfold and_boolS. +apply bindS_cong; auto. +intros [|]; auto. +Qed. + +Lemma and_boolSP_cong {RV E P Q R} H x x' y y' : + x === x' -> + y === y' -> + @and_boolSP RV E P Q R x y H === and_boolSP x' y'. +intros E1 E2. +unfold and_boolSP. +apply bindS_cong; auto. +intros [[|] [pf]]; auto. +apply bindS_cong; auto. +Qed. + +Lemma or_boolS_cong {RV E} x x' y y' : + x === x' -> + y === y' -> + @or_boolS RV E x y === or_boolS x' y'. +intros E1 E2. +unfold or_boolS. +apply bindS_cong; auto. +intros [|]; auto. +Qed. + +Lemma or_boolSP_cong {RV E P Q R} H x x' y y' : + x === x' -> + y === y' -> + @or_boolSP RV E P Q R x y H === or_boolSP x' y'. +intros E1 E2. +unfold or_boolSP. +apply bindS_cong; auto. +intros [[|] [pf]]; auto. +apply bindS_cong; auto. +Qed. + +Lemma build_trivial_exS_cong {RV T E} x x' : + x === x' -> + @build_trivial_exS RV T E x === build_trivial_exS x'. +intros E1. +unfold build_trivial_exS. +rewrite E1. +reflexivity. +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} : @@ -114,6 +173,13 @@ Qed. Hint Rewrite liftState_bind : liftState. Hint Resolve liftState_bind : liftState. +Lemma liftState_bind0 Regval Regs B E {r : Sail2_values.register_accessors Regs Regval} {m : monad Regval unit E} {m' : monad Regval B E} : + liftState r (bind0 m m') === seqS (liftState r m) (liftState r m'). +induction m; simpl; autorewrite with state; auto using bindS_cong. +Qed. +Hint Rewrite liftState_bind0 : liftState. +Hint Resolve liftState_bind0 : 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 @@ -134,7 +200,7 @@ auto. Qed. Local Ltac tryrw db := - try (etransitivity; [solve [eauto using eq_equiv with nocore db ] | ]; tryrw db). + try (etransitivity; [solve [clear; 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' -> @@ -156,10 +222,14 @@ Ltac statecong db := tryrw db; lazymatch goal with | |- (_ >>$= _) === _ => eapply bindS_cong; intros; statecong db + | |- (_ >>$ _) === _ => eapply seqS_cong; intros; statecong db | |- (if ?x then _ else _) === _ => - solve [ eapply if_bool_cong; statecong db - | eapply if_sumbool_cong; statecong db - | apply equiv_reflexive] + let ty := type of x in + match ty with + | bool => eapply if_bool_cong; statecong db + | sumbool _ _ => eapply if_sumbool_cong; statecong db + | _ => apply equiv_reflexive + end | |- (foreachS _ _ _) === _ => solve [ eapply foreachS_cong; intros; statecong db ] | |- (genlistS _ _) === _ => @@ -168,6 +238,28 @@ Ltac statecong db := solve [ eapply whileST_cong; intros; statecong db ] | |- (untilST _ _ _ _) === _ => solve [ eapply untilST_cong; intros; statecong db ] + | |- (and_boolS _ _) === _ => + solve [ eapply and_boolS_cong; intros; statecong db ] + | |- (or_boolS _ _) === _ => + solve [ eapply or_boolS_cong; intros; statecong db ] + | |- (and_boolSP _ _) === _ => + solve [ eapply and_boolSP_cong; intros; statecong db ] + | |- (or_boolSP _ _) === _ => + solve [ eapply or_boolSP_cong; intros; statecong db ] + | |- (build_trivial_exS _) === _ => + solve [ eapply build_trivial_exS_cong; intros; statecong db ] + | |- (let '(matchvar1, matchvar2) := ?e1 in _) === _ => + eapply (@equiv_transitive _ _ _ _ (let '(matchvar1,matchvar2) := e1 in _) _); + [ destruct e1; etransitivity; [ statecong db | apply equiv_reflexive ] + | apply equiv_reflexive ] + | |- (let '(existT _ matchvar1 matchvar2) := ?e1 in _) === _ => + eapply (@equiv_transitive _ _ _ _ (let '(existT _ matchvar1 matchvar2) := e1 in _) _); + [ destruct e1; etransitivity; [ statecong db | apply equiv_reflexive ] + | apply equiv_reflexive ] + | |- (match ?e1 with None => _ | Some _ => _ end) === _ => + eapply (@equiv_transitive _ _ _ _ (match e1 with None => _ | Some _ => _ end) _); + [ destruct e1; [> etransitivity; [> statecong db | apply equiv_reflexive ] ..] + | apply equiv_reflexive ] | |- ?X => solve [ apply equiv_reflexive @@ -204,11 +296,44 @@ Lemma liftState_if_distrib Regs Regval A E {r x y} {c : bool} : destruct c; reflexivity. Qed. Hint Resolve liftState_if_distrib : liftState. +(* TODO: try to find a way to make the above hint work when an alias is used for the + monad type. For some reason attempting to give a Resolve hint with a pattern doesn't + work, but an Extern one works: *) +Hint Extern 0 (liftState _ _ = _) => simple apply 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. +(* As above, but simple apply doesn't seem to work (again, due to unification problems + with the M alias for monad *) +Hint Extern 0 (liftState _ _ = _) => apply liftState_if_distrib_sumbool : liftState. + +Lemma liftState_let_pair Regs RegVal A B C E r (x : B * C) M : + @liftState Regs RegVal A E r (let '(y, z) := x in M y z) = + let '(y, z) := x in liftState r (M y z). +destruct x. +reflexivity. +Qed. +Hint Extern 0 (liftState _ (let '(x,y) := _ in _) = _) => + (rewrite liftState_let_pair; reflexivity) : liftState. + +Lemma liftState_let_Tpair Regs RegVal A B (P : B -> Prop) E r (x : sigT P) M : + @liftState Regs RegVal A E r (let '(existT _ y z) := x in M y z) = + let '(existT _ y z) := x in liftState r (M y z). +destruct x. +reflexivity. +Qed. +Hint Extern 0 (liftState _ (let '(existT _ x y) := _ in _) = _) => + (rewrite liftState_let_Tpair; reflexivity) : liftState. + +Lemma liftState_opt_match Regs RegVal A B E (x : option A) m f r : + @liftState Regs RegVal B E r (match x with None => m | Some v => f v end) = + match x with None => liftState r m | Some v => liftState r (f v) end. +destruct x; reflexivity. +Qed. +Hint Extern 0 (liftState _ (match _ with None => _ | Some _ => _ end) = _) => + (rewrite liftState_opt_match; reflexivity) : 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')). @@ -240,6 +365,10 @@ Lemma liftState_assert Regs Regval E {r c msg} : @liftState Regval Regs _ E r (assert_exp c msg) = assert_expS c msg. destruct c; reflexivity. Qed. +Lemma liftState_assert' Regs Regval E {r c msg} : + @liftState Regval Regs _ E r (assert_exp' c msg) = assert_expS' c msg. +destruct c; reflexivity. +Qed. Lemma liftState_exit Regs Regval A E r : @liftState Regval Regs A E r (exit tt) = exitS tt. reflexivity. @@ -281,11 +410,11 @@ unfold and_boolMP, and_boolSP. rewrite liftState_bind. apply bindS_cong; auto. intros [[|] [A]]. -* rewrite liftState_bind; +* rewrite liftState_bind. simpl; - apply bindS_cong; auto; - intros [a' A']; - rewrite liftState_return; + apply bindS_cong; auto. + intros [a' A']. + rewrite liftState_return. reflexivity. * rewrite liftState_return. reflexivity. @@ -315,17 +444,28 @@ intros [[|] [A]]. rewrite liftState_return; reflexivity. Qed. -Hint Rewrite liftState_throw liftState_assert liftState_exit liftState_exclResult - liftState_barrier liftState_footprint liftState_choose_bool - liftState_undefined liftState_maybe_fail + +Lemma liftState_build_trivial_ex Regs Regval E T r m : + @liftState Regs Regval _ E r (@build_trivial_ex _ _ T m) === + build_trivial_exS (liftState r m). +unfold build_trivial_ex, build_trivial_exS. +rewrite liftState_bind. +reflexivity. +Qed. + +Hint Rewrite liftState_throw liftState_assert 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_build_trivial_ex : liftState. -Hint Resolve liftState_throw liftState_assert liftState_exit liftState_exclResult - liftState_barrier liftState_footprint liftState_choose_bool - liftState_undefined liftState_maybe_fail +Hint Resolve liftState_throw liftState_assert 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_build_trivial_ex : liftState. Lemma liftState_try_catch Regs Regval A E1 E2 r m h : @@ -541,13 +681,33 @@ Lemma liftState_internal_pick Regs Regval A E r (xs : list A) : unfold internal_pick, internal_pickS. unfold choose. rewrite_liftState. -apply bindS_cong; auto. -intros. -destruct (nth_error _ _); auto. +reflexivity. Qed. Hint Rewrite liftState_internal_pick : liftState. Hint Resolve liftState_internal_pick : liftState. +Lemma liftState_undefined_word_nat Regs Regval E r n : + liftState (Regs := Regs) (Regval := Regval) (E := E) r (undefined_word_nat n) === undefined_word_natS n. +induction n. +* reflexivity. +* simpl. + apply bindS_cong; auto. + intro. + rewrite_liftState. + apply bindS_cong; auto. +Qed. +Hint Rewrite liftState_undefined_word_nat : liftState. +Hint Resolve liftState_undefined_word_nat : liftState. + +Lemma liftState_undefined_bitvector Regs Regval E r n `{ArithFact (n >= 0)} : + liftState (Regs := Regs) (Regval := Regval) (E := E) r (undefined_bitvector n) === undefined_bitvectorS n. +unfold undefined_bitvector, undefined_bitvectorS. +rewrite_liftState. +reflexivity. +Qed. +Hint Rewrite liftState_undefined_bitvector : liftState. +Hint Resolve liftState_undefined_bitvector : liftState. + Lemma liftRS_returnS (*[simp]:*) A R Regs E x : @liftRS A R Regs E (returnS x) = returnS x. reflexivity. diff --git a/lib/coq/Sail2_state_monad.v b/lib/coq/Sail2_state_monad.v index 552fa68e..bf5c5916 100644 --- a/lib/coq/Sail2_state_monad.v +++ b/lib/coq/Sail2_state_monad.v @@ -108,6 +108,9 @@ fun s => Definition assert_expS {Regs E} (exp : bool) (msg : string) : monadS Regs unit E := if exp then returnS tt else failS msg. +Definition assert_expS' {Regs E} (exp : bool) (msg : string) : monadS Regs (exp = true) E := + if exp return monadS Regs (exp = true) E then returnS eq_refl else failS msg. + (* For early return, we abuse exceptions by throwing and catching the return value. The exception type is "either 'r 'e", where "Right e" represents a proper exception and "Left r" an early return of value "r". *) |