diff options
Diffstat (limited to 'lib/coq/State_lemmas.v')
| -rw-r--r-- | lib/coq/State_lemmas.v | 1263 |
1 files changed, 1263 insertions, 0 deletions
diff --git a/lib/coq/State_lemmas.v b/lib/coq/State_lemmas.v new file mode 100644 index 00000000..78a7d1de --- /dev/null +++ b/lib/coq/State_lemmas.v @@ -0,0 +1,1263 @@ +Require Import Sail.Values Sail.Prompt_monad Sail.Prompt Sail.State_monad Sail.State Sail.State Sail.State_lifting. +Require Import Sail.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'. +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. + +Lemma foreach_ZS_up_cong rv e Vars from to step vars body body' H : + (forall a pf vars, body a pf vars === body' a pf vars) -> + @foreach_ZS_up rv e Vars from to step vars body H === foreach_ZS_up from to step vars body'. +intro EQ. +unfold foreach_ZS_up. +match goal with +| |- @foreach_ZS_up' _ _ _ _ _ _ _ _ _ ?pf _ _ === _ => generalize pf +end. +generalize 0 at 2 3 4 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros; simpl. +* reflexivity. +* destruct (sumbool_of_bool (from + off <=? to)); auto. + rewrite EQ. + setoid_rewrite IHn. + reflexivity. +Qed. + +Lemma foreach_ZS_down_cong rv e Vars from to step vars body body' H : + (forall a pf vars, body a pf vars === body' a pf vars) -> + @foreach_ZS_down rv e Vars from to step vars body H === foreach_ZS_down from to step vars body'. +intro EQ. +unfold foreach_ZS_down. +match goal with +| |- @foreach_ZS_down' _ _ _ _ _ _ _ _ _ ?pf _ _ === _ => generalize pf +end. +generalize 0 at 1 3 4 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros; simpl. +* reflexivity. +* destruct (sumbool_of_bool (to <=? from + off)); auto. + rewrite EQ. + setoid_rewrite IHn. + reflexivity. +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. + +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. +apply bindS_cong; auto. +Qed. + +Lemma liftRS_cong {A R Regs E} m m' : + m === m' -> + @liftRS A R Regs E m === liftRS m'. +intros E1. +unfold liftRS. +apply try_catchS_cong; auto. +Qed. + +(* Monad lifting *) + +Lemma liftState_bind Regval Regs A B E {r : Sail.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. +Hint Resolve liftState_bind : liftState. + +Lemma liftState_bind0 Regval Regs B E {r : Sail.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 + (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).*) + +(* 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 [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' -> + 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 + | |- (_ >>$ _) === _ => eapply seqS_cong; intros; statecong db + | |- (if ?x then _ else _) === _ => + let ty := type of x in + match ty with + | bool => eapply if_bool_cong; statecong db + | sumbool _ _ => eapply if_sumbool_cong; statecong db (* There's also a dependent case below *) + | _ => apply equiv_reflexive + end + | |- (foreachS _ _ _) === _ => + solve [ eapply foreachS_cong; intros; statecong db ] + | |- (foreach_ZS_up _ _ _ _ _) === _ => + solve [ eapply foreach_ZS_up_cong; intros; statecong db ] + | |- (foreach_ZS_down _ _ _ _ _) === _ => + solve [ eapply foreach_ZS_down_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 ] + | |- (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 ] + | |- (liftRS _) === _ => + solve [ eapply liftRS_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 ] + | |- (match ?e1 with left _ => _ | right _ => _ end) === _ => + eapply (@equiv_transitive _ _ _ _ (match e1 with left _ => _ | right _ => _ end) _); + [ destruct e1; [> etransitivity; [> statecong db | apply equiv_reflexive ] ..] + | apply equiv_reflexive ] + | |- ?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 : Sail.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: + List.In (Value a, s') (liftState r m s) + exists t, Run m t a. + by (use assms in \<open>induction r m arbitrary: s s' rule: liftState.induct\<close>; + simp add: failS_def throwS_def returnS_def del: read_regvalS.simps; + blast elim: Value_bindS_elim) + +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} : + @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. +(* 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). Be careful about only applying to a suitable goal to + avoid slowing down proofs. *) +Hint Extern 0 (liftState _ ?t = _) => + match t with + | match ?x with _ => _ end => + match type of x with + | sumbool _ _ => apply liftState_if_distrib_sumbool + end + end : liftState. + +Lemma liftState_match_distrib_sumbool {Regs Regval A E P Q r x y} {c : sumbool P Q} : + @liftState Regs Regval A E r (match c with left H => x H | right H => y H end) = match c with left H => liftState r (x H) | right H => liftState r (y H) end. +destruct c; reflexivity. +Qed. +(* As above, but also need to beta reduce H into x and y. *) +Hint Extern 0 (liftState _ ?t = _) => + match t with + | match ?x with _ => _ end => + match type of x with + | sumbool _ _ => etransitivity; [apply liftState_match_distrib_sumbool | cbv beta; reflexivity ] + end + end : 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')). +split. +* intro H. + apply bindS_cases in H. + destruct H as [(? & ? & ? & [= <-] & ? & ?) | [(? & [= <-] & ?) | (? & ? & ? & [= <-] & ? & ?)]]; + eauto. +* intros (? & ? & ? & ?). + eauto with bindS_intros. +Qed. + +Lemma Ex_bindS_iff {Regs A B E} {f : A -> monadS Regs B E} {m e s s''} : + List.In (Ex e, s'') (bindS m f s) <-> List.In (Ex e, s'') (m s) \/ (exists a s', List.In (Value a, s') (m s) /\ List.In (Ex e, s'') (f a s')). +split. +* intro H. + apply bindS_cases in H. + destruct H as [(? & ? & ? & [= <-] & ? & ?) | [(? & [= <-] & ?) | (? & ? & ? & [= <-] & ? & ?)]]; + eauto. +* intros [H | (? & ? & H1 & H2)]; + eauto with bindS_intros. +Qed. + +Lemma liftState_throw Regs Regval A E {r} {e : E} : + @liftState Regval Regs A E r (throw e) = throwS e. +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_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. +Qed. +Lemma liftState_exclResult Regs Regval E r : + @liftState Regs Regval _ E r (excl_result tt) = excl_resultS tt. +reflexivity. +Qed. +Lemma liftState_barrier Regs Regval E r bk : + @liftState Regs Regval _ E r (barrier bk) = returnS tt. +reflexivity. +Qed. +Lemma liftState_footprint Regs Regval E r : + @liftState Regs Regval _ E r (footprint tt) = returnS tt. +reflexivity. +Qed. +Lemma liftState_choose_bool Regs Regval E r descr : + @liftState Regs Regval _ E r (choose_bool descr) = choose_boolS tt. +reflexivity. +Qed. +(*declare undefined_boolS_def[simp]*) +Lemma liftState_undefined Regs Regval E r : + @liftState Regs Regval _ E r (undefined_bool tt) = undefined_boolS tt. +reflexivity. +Qed. +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 : + @liftState Regs Regval _ E r (and_boolM x y) === and_boolS (liftState r x) (liftState r y). +unfold and_boolM, and_boolS. +rewrite_liftState. +reflexivity. +Qed. +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. +apply bindS_cong; auto. +intros [[|] [A]]. +* rewrite liftState_bind. + simpl; + 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 : + @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_cong; auto. +intros. rewrite liftState_if_distrib. +reflexivity. +Qed. +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_cong; auto. +intros [[|] [A]]. +* rewrite liftState_return. + reflexivity. +* rewrite liftState_bind; + simpl; + apply bindS_cong; auto; + intros [a' A']; + rewrite liftState_return; + reflexivity. +Qed. + +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. +unfold ArithFact. +intro. +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_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 : + @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 +| erewrite try_catchS_bindS_no_throw; intros; + only 2,3: (autorewrite with ignore_throw; reflexivity); + apply bindS_cong; auto +]. +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). +unfold catch_early_return, catch_early_returnS. +rewrite_liftState. +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). +unfold liftR, liftRS. +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)). +unfold try_catchR, try_catchRS. rewrite_liftState. +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. +unfold read_memt, read_memt_bytes, read_memtS, maybe_failS. simpl. +apply bindS_cong; auto. +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. +unfold read_mem, read_memS, read_memtS. simpl. +unfold read_mem_bytesS, read_memt_bytesS. +repeat rewrite bindS_assoc. +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. +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. +unfold write_memt, write_memtS. +destruct (Sail.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. +unfold write_mem, write_memS, write_memtS. +destruct (Sail.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 -> + bindS m1 f s = bindS m2 f s. +intro H. unfold bindS. rewrite H. reflexivity. +Qed. + +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) === readS (fun x => reg.(read_from) (ss_regstate x)). +intros. +unfold read_reg. simpl. unfold readS. intro s. +erewrite bindS_rw_left. 2: { + apply bindS_returnS_left. +} +specialize (H (ss_regstate s)). +destruct (get_regval' _ _) as [v | ]; only 2: discriminate H. +rewrite bindS_returnS_left. +simpl in *. +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) |}). +intros. intro s. +unfold write_reg. simpl. unfold readS, seqS. +erewrite bindS_rw_left. 2: { + apply bindS_returnS_left. +} +specialize (H (ss_regstate s)). +destruct (set_regval' _ _) as [v' | ]; only 2: discriminate H. +injection H as H1. +unfold updateS. +rewrite <- H1. +reflexivity. +Qed. +(* +Lemma liftState_iter_aux Regs Regval A E : + liftState r (iter_aux i f xs) = iterS_aux i (fun i x => liftState r (f i x)) xs. + 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" + by (auto simp: iteri_def iteriS_def liftState_simp) + +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 : + 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. simpl. + rewrite_liftState. + apply bindS_cong; auto. +Qed. +Hint Rewrite liftState_foreachM : liftState. +Hint Resolve liftState_foreachM : liftState. + +Lemma liftState_foreach_ZM_up Regs Regval Vars E from to step vars body H r : + liftState (Regs := Regs) r + (@foreach_ZM_up Regval E Vars from to step vars body H) === + foreach_ZS_up from to step vars (fun z H' a => liftState r (body z H' a)). +unfold foreach_ZM_up, foreach_ZS_up. +match goal with +| |- liftState _ (@foreach_ZM_up' _ _ _ _ _ _ _ _ _ ?pf _ _) === _ => generalize pf +end. +generalize 0 at 2 3 4 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros. +* simpl. + rewrite_liftState. + reflexivity. +* simpl. + rewrite_liftState. + destruct (sumbool_of_bool (from + off <=? to)); auto. + repeat replace_ArithFact_proof. + reflexivity. +Qed. +Hint Rewrite liftState_foreach_ZM_up : liftState. +Hint Resolve liftState_foreach_ZM_up : liftState. + +Lemma liftState_foreach_ZM_down Regs Regval Vars E from to step vars body H r : + liftState (Regs := Regs) r + (@foreach_ZM_down Regval E Vars from to step vars body H) === + foreach_ZS_down from to step vars (fun z H' a => liftState r (body z H' a)). +unfold foreach_ZM_down, foreach_ZS_down. +match goal with +| |- liftState _ (@foreach_ZM_down' _ _ _ _ _ _ _ _ _ ?pf _ _) === _ => generalize pf +end. +generalize 0 at 1 3 4 as off. +revert vars. +induction (S (Z.abs_nat (from - to))); intros. +* simpl. + rewrite_liftState. + reflexivity. +* simpl. + rewrite_liftState. + destruct (sumbool_of_bool (to <=? from + off)); auto. + repeat replace_ArithFact_proof. + reflexivity. +Qed. +Hint Rewrite liftState_foreach_ZM_down : liftState. +Hint Resolve liftState_foreach_ZM_down : 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. +unfold genlistM, genlistS. +rewrite_liftState. +reflexivity. +Qed. +Hint Rewrite liftState_genlistM : liftState. +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. +unfold choose_bools, choose_boolsS. +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. +unfold bools_of_bits_nondet, bools_of_bits_nondetS. +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. +unfold internal_pick, internal_pickS. +unfold choose. +rewrite_liftState. +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. +Qed. + +Lemma concat_singleton A (xs : list A) : + concat (xs::nil) = xs. +simpl. +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) : + @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. +* simpl. rewrite flat_map_app. rewrite IHl. reflexivity. +* simpl. rewrite IHl. reflexivity. +* simpl. rewrite IHl. reflexivity. +Qed. + +Lemma liftRS_assert_expS_True (*[simp]:*) Regs R E msg : + @liftRS _ R Regs E (assert_expS true msg) = returnS tt. +reflexivity. +Qed. + +(* +lemma untilM_domI: + fixes V :: "'vars \<Rightarrow> nat" + assumes "Inv vars" + and "\<And>vars t vars' t'. \<lbrakk>Inv vars; Run (body vars) t vars'; Run (cond vars') t' False\<rbrakk> \<Longrightarrow> V vars' < V vars \<and> Inv vars'" + shows "untilM_dom (vars, cond, body)" + using assms + by (induction vars rule: measure_induct_rule[where f = V]) + (auto intro: untilM.domintros) + +lemma untilM_dom_untilS_dom: + assumes "untilM_dom (vars, cond, body)" + shows "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" + using assms + by (induction vars cond body arbitrary: s rule: untilM.pinduct) + (rule untilS.domintros, auto elim!: Value_liftState_Run) + +lemma measure2_induct: + fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> nat" + assumes "\<And>x1 y1. (\<And>x2 y2. f x2 y2 < f x1 y1 \<Longrightarrow> P x2 y2) \<Longrightarrow> P x1 y1" + shows "P x y" +proof - + have "P (fst x) (snd x)" for x + by (induction x rule: measure_induct_rule[where f = "\<lambda>x. f (fst x) (snd x)"]) (auto intro: assms) + then show ?thesis by auto +qed + +lemma untilS_domI: + fixes V :: "'vars \<Rightarrow> 'regs sequential_state \<Rightarrow> nat" + assumes "Inv vars s" + and "\<And>vars s vars' s' s''. + \<lbrakk>Inv vars s; (Value vars', s') \<in> body vars s; (Value False, s'') \<in> cond vars' s'\<rbrakk> + \<Longrightarrow> V vars' s'' < V vars s \<and> Inv vars' s''" + shows "untilS_dom (vars, cond, body, s)" + using assms + by (induction vars s rule: measure2_induct[where f = V]) + (auto intro: untilS.domintros) + +lemma whileS_dom_step: + assumes "whileS_dom (vars, cond, body, s)" + and "(Value True, s') \<in> cond vars s" + and "(Value vars', s'') \<in> body vars s'" + shows "whileS_dom (vars', cond, body, s'')" + by (use assms in \<open>induction vars cond body s arbitrary: vars' s' s'' rule: whileS.pinduct\<close>) + (auto intro: whileS.domintros) + +lemma whileM_dom_step: + assumes "whileM_dom (vars, cond, body)" + and "Run (cond vars) t True" + and "Run (body vars) t' vars'" + shows "whileM_dom (vars', cond, body)" + by (use assms in \<open>induction vars cond body arbitrary: vars' t t' rule: whileM.pinduct\<close>) + (auto intro: whileM.domintros) + +lemma whileM_dom_ex_step: + assumes "whileM_dom (vars, cond, body)" + and "\<exists>t. Run (cond vars) t True" + and "\<exists>t'. Run (body vars) t' vars'" + shows "whileM_dom (vars', cond, body)" + using assms by (blast intro: whileM_dom_step) + +lemmas whileS_pinduct = whileS.pinduct[case_names Step] + +lemma liftState_whileM: + assumes "whileS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" + and "whileM_dom (vars, cond, body)" + shows "liftState r (whileM vars cond body) s = whileS vars (liftState r \<circ> cond) (liftState r \<circ> body) s" +proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState r \<circ> body" s rule: whileS.pinduct\<close>) + case Step: (1 vars s) + note domS = Step(1) and IH = Step(2) and domM = Step(3) + show ?case unfolding whileS.psimps[OF domS] whileM.psimps[OF domM] liftState_bind + proof (intro bindS_ext_cong, goal_cases cond while) + case (while a s') + have "bindS (liftState r (body vars)) (liftState r \<circ> (\<lambda>vars. whileM vars cond body)) s' = + bindS (liftState r (body vars)) (\<lambda>vars. whileS vars (liftState r \<circ> cond) (liftState r \<circ> body)) s'" + if "a" + proof (intro bindS_ext_cong, goal_cases body while') + case (while' vars' s'') + have "whileM_dom (vars', cond, body)" proof (rule whileM_dom_ex_step[OF domM]) + show "\<exists>t. Run (cond vars) t True" using while that by (auto elim: Value_liftState_Run) + show "\<exists>t'. Run (body vars) t' vars'" using while' that by (auto elim: Value_liftState_Run) + qed + then show ?case using while while' that IH by auto + qed auto + then show ?case by (auto simp: liftState_simp) + qed auto +qed +*) + + +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. +destruct (Z.le_decidable 0 limit). +* generalize (Zwf_guarded limit) at 1 as acc1. + generalize (Zwf_guarded limit) at 1 as acc2. + apply Wf_Z.natlike_ind with (x := limit). + + intros [acc1] [acc2] *; simpl. + rewrite_liftState. + apply bindS_cong; auto. + intros [|]; auto. + apply bindS_cong; auto. + intros. repeat destruct (_limit_reduces _). simpl. + reflexivity. + + clear limit H. + intros limit H IH [acc1] [acc2] vars s. simpl. + destruct (Z_ge_dec _ _); try omega. + rewrite_liftState. + apply bindS_cong; auto. + intros [|]; auto. + apply bindS_cong; auto. + intros. + repeat gen_reduces. + replace (Z.succ limit - 1) with limit; try omega. intros acc1' acc2'. + apply IH. + + assumption. +* intros. simpl. + destruct (Z_ge_dec _ _); try omega. + reflexivity. +Qed. +Hint Resolve liftState_whileM : liftState. + +(* +lemma untilM_dom_step: + assumes "untilM_dom (vars, cond, body)" + and "Run (body vars) t vars'" + and "Run (cond vars') t' False" + shows "untilM_dom (vars', cond, body)" + by (use assms in \<open>induction vars cond body arbitrary: vars' t t' rule: untilM.pinduct\<close>) + (auto intro: untilM.domintros) + +lemma untilM_dom_ex_step: + assumes "untilM_dom (vars, cond, body)" + and "\<exists>t. Run (body vars) t vars'" + and "\<exists>t'. Run (cond vars') t' False" + shows "untilM_dom (vars', cond, body)" + using assms by (blast intro: untilM_dom_step) + +lemma liftState_untilM: + assumes "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" + and "untilM_dom (vars, cond, body)" + shows "liftState r (untilM vars cond body) s = untilS vars (liftState r \<circ> cond) (liftState r \<circ> body) s" +proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState r \<circ> body" s rule: untilS.pinduct\<close>) + case Step: (1 vars s) + note domS = Step(1) and IH = Step(2) and domM = Step(3) + show ?case unfolding untilS.psimps[OF domS] untilM.psimps[OF domM] liftState_bind + proof (intro bindS_ext_cong, goal_cases body k) + case (k vars' s') + show ?case unfolding comp_def liftState_bind + proof (intro bindS_ext_cong, goal_cases cond until) + case (until a s'') + have "untilM_dom (vars', cond, body)" if "\<not>a" + proof (rule untilM_dom_ex_step[OF domM]) + show "\<exists>t. Run (body vars) t vars'" using k by (auto elim: Value_liftState_Run) + show "\<exists>t'. Run (cond vars') t' False" using until that by (auto elim: Value_liftState_Run) + qed + then show ?case using k until IH by (auto simp: comp_def liftState_simp) + qed auto + qed auto +qed*) + +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. +destruct (Z.le_decidable 0 limit). +* generalize (Zwf_guarded limit) at 1 as acc1. + generalize (Zwf_guarded limit) at 1 as acc2. + apply Wf_Z.natlike_ind with (x := limit). + + intros [acc1] [acc2] * s; simpl. + rewrite_liftState. + apply bindS_cong; auto. + intros. apply bindS_cong; auto. + intros [|]; auto. + repeat destruct (_limit_reduces _). simpl. + reflexivity. + + clear limit H. + intros limit H IH [acc1] [acc2] vars s. simpl. + destruct (Z_ge_dec _ _); try omega. + rewrite_liftState. + apply bindS_cong; auto. + intros. apply bindS_cong; auto. + intros [|]; auto. + repeat gen_reduces. + replace (Z.succ limit - 1) with limit; try omega. intros acc1' acc2'. + apply IH. + + assumption. +* intros. simpl. + destruct (Z_ge_dec _ _); try omega. + reflexivity. +Qed. +Hint Resolve liftState_untilM : liftState. + +(* + +text \<open>Simplification rules for monadic Boolean connectives\<close> + +lemma if_return_return[simp]: "(if a then return True else return False) = return a" by auto + +lemma and_boolM_simps[simp]: + "and_boolM (return b) (return c) = return (b \<and> c)" + "and_boolM x (return True) = x" + "and_boolM x (return False) = x \<bind> (\<lambda>_. return False)" + "\<And>x y z. and_boolM (x \<bind> y) z = (x \<bind> (\<lambda>r. and_boolM (y r) z))" + by (auto simp: and_boolM_def) + +lemma and_boolM_return_if: + "and_boolM (return b) y = (if b then y else return False)" + by (auto simp: and_boolM_def) + +lemma and_boolM_return_return_and[simp]: "and_boolM (return l) (return r) = return (l \<and> r)" + by (auto simp: and_boolM_def) + +lemmas and_boolM_if_distrib[simp] = if_distrib[where f = "\<lambda>x. and_boolM x y" for y] + +lemma or_boolM_simps[simp]: + "or_boolM (return b) (return c) = return (b \<or> c)" + "or_boolM x (return True) = x \<bind> (\<lambda>_. return True)" + "or_boolM x (return False) = x" + "\<And>x y z. or_boolM (x \<bind> y) z = (x \<bind> (\<lambda>r. or_boolM (y r) z))" + by (auto simp: or_boolM_def) + +lemma or_boolM_return_if: + "or_boolM (return b) y = (if b then return True else y)" + by (auto simp: or_boolM_def) + +lemma or_boolM_return_return_or[simp]: "or_boolM (return l) (return r) = return (l \<or> r)" + by (auto simp: or_boolM_def) + +lemmas or_boolM_if_distrib[simp] = if_distrib[where f = "\<lambda>x. or_boolM x y" for y] + +lemma if_returnS_returnS[simp]: "(if a then returnS True else returnS False) = returnS a" by auto + +lemma and_boolS_simps[simp]: + "and_boolS (returnS b) (returnS c) = returnS (b \<and> c)" + "and_boolS x (returnS True) = x" + "and_boolS x (returnS False) = bindS x (\<lambda>_. returnS False)" + "\<And>x y z. and_boolS (bindS x y) z = (bindS x (\<lambda>r. and_boolS (y r) z))" + by (auto simp: and_boolS_def) + +lemma and_boolS_returnS_if: + "and_boolS (returnS b) y = (if b then y else returnS False)" + by (auto simp: and_boolS_def) + +lemmas and_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. and_boolS x y" for y] + +lemma and_boolS_returnS_True[simp]: "and_boolS (returnS True) c = c" + by (auto simp: and_boolS_def) + +lemma or_boolS_simps[simp]: + "or_boolS (returnS b) (returnS c) = returnS (b \<or> c)" + "or_boolS (returnS False) m = m" + "or_boolS x (returnS True) = bindS x (\<lambda>_. returnS True)" + "or_boolS x (returnS False) = x" + "\<And>x y z. or_boolS (bindS x y) z = (bindS x (\<lambda>r. or_boolS (y r) z))" + by (auto simp: or_boolS_def) + +lemma or_boolS_returnS_if: + "or_boolS (returnS b) y = (if b then returnS True else y)" + by (auto simp: or_boolS_def) + +lemmas or_boolS_if_distrib[simp] = if_distrib[where f = "\<lambda>x. or_boolS x y" for y] + +lemma Run_or_boolM_E: + assumes "Run (or_boolM l r) t a" + obtains "Run l t True" and "a" + | tl tr where "Run l tl False" and "Run r tr a" and "t = tl @ tr" + using assms by (auto simp: or_boolM_def elim!: Run_bindE Run_ifE Run_returnE) + +lemma Run_and_boolM_E: + assumes "Run (and_boolM l r) t a" + obtains "Run l t False" and "\<not>a" + | tl tr where "Run l tl True" and "Run r tr a" and "t = tl @ tr" + using assms by (auto simp: and_boolM_def elim!: Run_bindE Run_ifE Run_returnE) + +lemma maybe_failS_Some[simp]: "maybe_failS msg (Some v) = returnS v" + by (auto simp: maybe_failS_def) + +text \<open>Event traces\<close> + +lemma Some_eq_bind_conv: "Some x = Option.bind f g \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)" + unfolding bind_eq_Some_conv[symmetric] by auto + +lemma if_then_Some_eq_Some_iff: "((if b then Some x else None) = Some y) \<longleftrightarrow> (b \<and> y = x)" + by auto + +lemma Some_eq_if_then_Some_iff: "(Some y = (if b then Some x else None)) \<longleftrightarrow> (b \<and> y = x)" + by auto + +lemma emitEventS_update_cases: + assumes "emitEventS ra e s = Some s'" + obtains + (Write_mem) wk addr sz v tag r + where "e = E_write_memt wk addr sz v tag r \<or> (e = E_write_mem wk addr sz v r \<and> tag = B0)" + and "s' = put_mem_bytes addr sz v tag s" + | (Write_reg) r v rs' + where "e = E_write_reg r v" and "(snd ra) r v (regstate s) = Some rs'" + and "s' = s\<lparr>regstate := rs'\<rparr>" + | (Read) "s' = s" + using assms + by (elim emitEventS.elims) + (auto simp: Some_eq_bind_conv bind_eq_Some_conv if_then_Some_eq_Some_iff Some_eq_if_then_Some_iff) + +lemma runTraceS_singleton[simp]: "runTraceS ra [e] s = emitEventS ra e s" + by (cases "emitEventS ra e s"; auto) + +lemma runTraceS_ConsE: + assumes "runTraceS ra (e # t) s = Some s'" + obtains s'' where "emitEventS ra e s = Some s''" and "runTraceS ra t s'' = Some s'" + using assms by (auto simp: bind_eq_Some_conv) + +lemma runTraceS_ConsI: + assumes "emitEventS ra e s = Some s'" and "runTraceS ra t s' = Some s''" + shows "runTraceS ra (e # t) s = Some s''" + using assms by auto + +lemma runTraceS_Cons_tl: + assumes "emitEventS ra e s = Some s'" + shows "runTraceS ra (e # t) s = runTraceS ra t s'" + using assms by (elim emitEventS.elims) (auto simp: Some_eq_bind_conv bind_eq_Some_conv) + +lemma runTraceS_appendE: + assumes "runTraceS ra (t @ t') s = Some s'" + obtains s'' where "runTraceS ra t s = Some s''" and "runTraceS ra t' s'' = Some s'" +proof - + have "\<exists>s''. runTraceS ra t s = Some s'' \<and> runTraceS ra t' s'' = Some s'" + proof (use assms in \<open>induction t arbitrary: s\<close>) + case (Cons e t) + from Cons.prems + obtain s_e where "emitEventS ra e s = Some s_e" and "runTraceS ra (t @ t') s_e = Some s'" + by (auto elim: runTraceS_ConsE simp: bind_eq_Some_conv) + with Cons.IH[of s_e] show ?case by (auto intro: runTraceS_ConsI) + qed auto + then show ?thesis using that by blast +qed + +lemma runTraceS_nth_split: + assumes "runTraceS ra t s = Some s'" and n: "n < length t" + obtains s1 s2 where "runTraceS ra (take n t) s = Some s1" + and "emitEventS ra (t ! n) s1 = Some s2" + and "runTraceS ra (drop (Suc n) t) s2 = Some s'" +proof - + have "runTraceS ra (take n t @ t ! n # drop (Suc n) t) s = Some s'" + using assms + by (auto simp: id_take_nth_drop[OF n, symmetric]) + then show thesis by (blast elim: runTraceS_appendE runTraceS_ConsE intro: that) +qed + +text \<open>Memory accesses\<close> + +lemma get_mem_bytes_put_mem_bytes_same_addr: + assumes "length v = sz" + shows "get_mem_bytes addr sz (put_mem_bytes addr sz v tag s) = Some (v, if sz > 0 then tag else B1)" +proof (unfold assms[symmetric], induction v rule: rev_induct) + case Nil + then show ?case by (auto simp: get_mem_bytes_def) +next + case (snoc x xs) + then show ?case + by (cases tag) + (auto simp: get_mem_bytes_def put_mem_bytes_def Let_def and_bit_eq_iff foldl_and_bit_eq_iff + cong: option.case_cong split: if_splits option.splits) +qed + +lemma memstate_put_mem_bytes: + assumes "length v = sz" + shows "memstate (put_mem_bytes addr sz v tag s) addr' = + (if addr' \<in> {addr..<addr+sz} then Some (v ! (addr' - addr)) else memstate s addr')" + unfolding assms[symmetric] + by (induction v rule: rev_induct) (auto simp: put_mem_bytes_def nth_Cons nth_append Let_def) + +lemma tagstate_put_mem_bytes: + assumes "length v = sz" + shows "tagstate (put_mem_bytes addr sz v tag s) addr' = + (if addr' \<in> {addr..<addr+sz} then Some tag else tagstate s addr')" + unfolding assms[symmetric] + by (induction v rule: rev_induct) (auto simp: put_mem_bytes_def nth_Cons nth_append Let_def) + +lemma get_mem_bytes_cong: + assumes "\<forall>addr'. addr \<le> addr' \<and> addr' < addr + sz \<longrightarrow> + (memstate s' addr' = memstate s addr' \<and> tagstate s' addr' = tagstate s addr')" + shows "get_mem_bytes addr sz s' = get_mem_bytes addr sz s" +proof (use assms in \<open>induction sz\<close>) + case 0 + then show ?case by (auto simp: get_mem_bytes_def) +next + case (Suc sz) + then show ?case + by (auto simp: get_mem_bytes_def Let_def + intro!: map_option_cong map_cong foldl_cong + arg_cong[where f = just_list] arg_cong2[where f = and_bit]) +qed + +lemma get_mem_bytes_tagged_tagstate: + assumes "get_mem_bytes addr sz s = Some (v, B1)" + shows "\<forall>addr' \<in> {addr..<addr + sz}. tagstate s addr' = Some B1" + using assms + by (auto simp: get_mem_bytes_def foldl_and_bit_eq_iff Let_def split: option.splits) + +end +*) |