Merge branch 'sail2' into union_barrier

8 files changed, 2117 insertions, 34 deletions

diff --git a/lib/coq/Hoare.v b/lib/coq/Hoare.v
new file mode 100644
index 00000000..aff3a210
--- /dev/null
+++ b/lib/coq/Hoare.v
@@ -0,0 +1,742 @@
+Require Import String.
+Require Import Sail2_state_monad Sail2_state Sail2_state_monad_lemmas.
+Require Import Sail2_state_lemmas.
+
+(*adhoc_overloading
+  Monad_Syntax.bind State_monad.bindS*)
+
+(*section \<open>Hoare logic for the state, exception and nondeterminism monad\<close>
+
+subsection \<open>Hoare triples\<close>
+*)
+Definition predS regs := sequential_state regs -> Prop.
+
+Definition PrePost {Regs A E} (P : predS Regs) (f : monadS Regs A E) (Q : result A E -> predS Regs) : Prop :=
+ (*"\<lbrace>_\<rbrace> _ \<lbrace>_\<rbrace>"*)
+  forall s, P s -> (forall r s', List.In (r, s') (f s) -> Q r s').
+(*
+lemma PrePostI:
+  assumes "\<And>s r s'. P s \<Longrightarrow> (r, s') \<in> f s \<Longrightarrow> Q r s'"
+  shows "PrePost P f Q"
+  using assms unfolding PrePost_def by auto
+
+lemma PrePost_elim:
+  assumes "PrePost P f Q" and "P s" and "(r, s') \<in> f s"
+  obtains "Q r s'"
+  using assms by (fastforce simp: PrePost_def)
+*)
+Lemma PrePost_consequence Regs X E (A P : predS Regs) (f : monadS Regs X E) (B Q : result X E -> predS Regs) :
+  PrePost A f B ->
+  (forall s, P s -> A s) ->
+  (forall v s, B v s -> Q v s) ->
+  PrePost P f Q.
+intros Triple PA BQ.
+intros s Pre r s' IN.
+specialize (Triple s).
+auto.
+Qed.
+
+Lemma PrePost_strengthen_pre Regs X E (A B : predS Regs) (f : monadS Regs X E) (C : result X E -> predS Regs) :
+  PrePost A f C ->
+  (forall s, B s -> A s) ->
+  PrePost B f C.
+eauto using PrePost_consequence.
+Qed.
+
+Lemma PrePost_weaken_post Regs X E (A : predS Regs) (f : monadS Regs X E) (B C : result X E -> predS Regs) :
+  PrePost A f B ->
+  (forall v s, B v s -> C v s) ->
+  PrePost A f C.
+eauto using PrePost_consequence.
+Qed.
+
+Lemma PrePost_True_post (*[PrePost_atomI, intro, simp]:*) Regs A E (P : predS Regs) (m : monadS Regs A E) :
+  PrePost P m (fun _ _ => True).
+unfold PrePost. auto.
+Qed.
+
+Lemma PrePost_any Regs A E (m : monadS Regs A E) (Q : result A E -> predS Regs) :
+  PrePost (fun s => forall r s', List.In (r, s') (m s) -> Q r s') m Q.
+unfold PrePost. auto.
+Qed.
+
+Lemma PrePost_returnS (*[intro, PrePost_atomI]:*) Regs A E  (P : result A E -> predS Regs) (x : A) :
+  PrePost (P (Value x)) (returnS x) P.
+unfold PrePost, returnS.
+intros s p r s' IN.
+simpl in IN.
+destruct IN as [[=] | []].
+subst; auto.
+Qed.
+
+Lemma PrePost_bindS (*[intro, PrePost_compositeI]:*) Regs A B E (m : monadS Regs A E) (f : A -> monadS Regs B E) (P : predS Regs) (Q : result B E -> predS Regs) (R : A -> predS Regs) :
+  (forall s a s', List.In (Value a, s') (m s) -> PrePost (R a) (f a) Q) ->
+  (PrePost P m (fun r => match r with Value a => R a | Ex e => Q (Ex e) end)) ->
+  PrePost P (bindS m f) Q.
+intros F M s Pre r s' IN.
+destruct (bindS_cases IN) as [(a & a' & s'' & [= ->] & IN' & IN'') | [(e & [= ->] & IN') | (e & a & s'' & [= ->] & IN' & IN'')]].
+* eapply F. apply IN'. specialize (M s Pre (Value a') s'' IN'). apply M. assumption.
+* specialize (M _ Pre _ _ IN'). apply M.
+* specialize (M _ Pre _ _ IN'). simpl in M. eapply F; eauto.
+Qed.
+
+Lemma PrePost_bindS_ignore Regs A B E (m : monadS Regs A E) (f : monadS Regs B E) (P : predS Regs) (Q : result B E -> predS Regs) (R : predS Regs) :
+  PrePost R f Q ->
+  PrePost P m (fun r => match r with Value a => R | Ex e => Q (Ex e) end) ->
+  PrePost P (bindS m (fun _ => f)) Q.
+intros F M.
+eapply PrePost_bindS; eauto.
+* intros. apply F.
+* apply M.
+Qed.
+
+Lemma PrePost_bindS_unit Regs B E (m : monadS Regs unit E) (f : unit -> monadS Regs B E) P Q R :
+  PrePost R (f tt) Q ->
+  PrePost P m (fun r => match r with Value a => R | Ex e => Q (Ex e) end) ->
+  PrePost P (bindS m f) 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.
+intros s Pre r s' [H | []].
+inversion H; subst.
+assumption.
+Qed.
+
+Lemma PrePost_updateS (*[intro, PrePost_atomI]:*) Regs E (P : result unit E -> predS Regs) f :
+  PrePost (fun s => P (Value tt) (f s)) (updateS f) P.
+unfold PrePost, readS, returnS.
+intros s Pre r s' [H | []].
+inversion H; subst.
+assumption.
+Qed.
+
+Lemma PrePost_if Regs A E b (f g : monadS Regs A E) P Q :
+  (b = true  -> PrePost P f Q) ->
+  (b = false -> PrePost P g Q) ->
+  PrePost P (if b then f else g) Q.
+intros T F.
+destruct b; auto.
+Qed.
+
+Lemma PrePost_if_branch (*[PrePost_compositeI]:*) Regs A E b (f g : monadS Regs A E) Pf Pg Q :
+  (b = true  -> PrePost Pf f Q) ->
+  (b = false -> PrePost Pg g Q) ->
+  PrePost (if b then Pf else Pg) (if b then f else g) Q.
+destruct b; auto.
+Qed.
+
+Lemma PrePost_if_then Regs A E b (f g : monadS Regs A E) P Q :
+  b = true ->
+  PrePost P f Q ->
+  PrePost P (if b then f else g) Q.
+intros; subst; auto.
+Qed.
+
+Lemma PrePost_if_else Regs A E b (f g : monadS Regs A E) P Q :
+  b = false ->
+  PrePost P g Q ->
+  PrePost P (if b then f else g) Q.
+intros; subst; auto.
+Qed.
+
+Lemma PrePost_prod_cases (*[PrePost_compositeI]:*) Regs A B E (f : A -> B -> monadS Regs A E) P Q x :
+  PrePost P (f (fst x) (snd x)) Q ->
+  PrePost P (match x with (a, b) => f a b end) Q.
+destruct x; auto.
+Qed.
+
+Lemma PrePost_option_cases (*[PrePost_compositeI]:*) Regs A B E x (s : A -> monadS Regs B E) n PS PN Q :
+  (forall a, PrePost (PS a) (s a) Q) ->
+  PrePost PN n Q ->
+  PrePost (match x with Some a => PS a | None => PN end) (match x with Some a => s a | None => n end) Q.
+destruct x; auto.
+Qed.
+
+Lemma PrePost_let (*[intro, PrePost_compositeI]:*) Regs A B E y (m : A -> monadS Regs B E) P Q :
+  PrePost P (m y) Q ->
+  PrePost P (let x := y in m x) Q.
+auto.
+Qed.
+
+Lemma PrePost_and_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 true => R | _ => Q r end) ->
+  PrePost P (and_boolS l r) Q.
+intros Hr Hl.
+unfold and_boolS.
+eapply PrePost_bindS.
+2: { instantiate (1 := fun a => if a then R else Q (Value false)).
+     eapply PrePost_weaken_post.
+     apply Hl.
+     intros [[|] | ] s H; auto. }
+* intros. destruct a; eauto.
+  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) ->
+  PrePost P (or_boolS l r) Q.
+intros Hr Hl.
+unfold or_boolS.
+eapply PrePost_bindS.
+* intros.
+  instantiate (1 := fun a => if a then Q (Value true) else R).
+  destruct a; eauto.
+  apply PrePost_returnS.
+* eapply PrePost_weaken_post.
+  apply Hl.
+  intros [[|] | ] s H; auto.
+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' [[= <- <-] | []].
+assumption.
+Qed.
+
+Lemma PrePost_assert_expS (*[intro, PrePost_atomI]:*) Regs E (c : bool) m (P : result unit E -> predS Regs) :
+  PrePost (if c then P (Value tt) else P (Ex (Failure m))) (assert_expS c m) P.
+destruct c; simpl.
+* apply PrePost_returnS.
+* apply PrePost_failS. 
+Qed.
+
+Lemma PrePost_chooseS (*[intro, PrePost_atomI]:*) Regs A E xs (Q : result A E -> predS Regs) :
+  PrePost (fun s => forall x, List.In x xs -> Q (Value x) s) (chooseS xs) Q.
+unfold PrePost, chooseS.
+intros s IN r s' IN'.
+apply List.in_map_iff in IN'.
+destruct IN' as (x & [= <- <-] & IN').
+auto.
+Qed.
+
+Lemma case_result_combine (*[simp]:*) A E X r (Q : result A E -> X) :
+  (match r with Value a => Q (Value a) | Ex e => Q (Ex e) end) = Q r.
+destruct r; auto.
+Qed.
+
+Lemma PrePost_foreachS_Nil (*[intro, simp, PrePost_atomI]:*) Regs A Vars E vars body (Q : result Vars E -> predS Regs) :
+  PrePost (Q (Value vars)) (foreachS (A := A) nil vars body) Q.
+simpl. apply PrePost_returnS.
+Qed.
+
+Lemma PrePost_foreachS_Cons Regs A Vars E (x : A) xs vars body (Q : result Vars E -> predS Regs) :
+  (forall s vars' s', List.In (Value vars', s') (body x vars s) -> PrePost (Q (Value vars')) (foreachS xs vars' body) Q) ->
+  PrePost (Q (Value vars)) (body x vars) Q ->
+  PrePost (Q (Value vars)) (foreachS (x :: xs) vars body) Q.
+intros XS X.
+simpl.
+eapply PrePost_bindS.
+* apply XS.
+* apply PrePost_weaken_post with (B := Q).
+  assumption.
+  intros; rewrite case_result_combine.
+  assumption.
+Qed.
+
+Lemma PrePost_foreachS_invariant Regs A Vars E (xs : list A) vars body (Q : result Vars E -> predS Regs) :
+  (forall x vars, List.In x xs -> PrePost (Q (Value vars)) (body x vars) Q) ->
+  PrePost (Q (Value vars)) (foreachS xs vars body) Q.
+revert vars.
+induction xs.
+* intros. apply PrePost_foreachS_Nil.
+* intros. apply PrePost_foreachS_Cons.
+  + auto with datatypes.
+  + apply H. auto with datatypes.
+Qed.
+
+(*subsection \<open>Hoare quadruples\<close>
+
+text \<open>It is often convenient to treat the exception case separately.  For this purpose, we use
+a Hoare logic similar to the one used in [1]. It features not only Hoare triples, but also quadruples
+with two postconditions: one for the case where the computation succeeds, and one for the case where
+there is an exception.
+
+[1] D. Cock, G. Klein, and T. Sewell, ‘Secure Microkernels, State Monads and Scalable Refinement’,
+in Theorem Proving in Higher Order Logics, 2008, pp. 167–182.\<close>
+*)
+Definition PrePostE {Regs A Ety} (P : predS Regs) (f : monadS Regs A Ety) (Q : A -> predS Regs) (E : ex Ety -> predS Regs) : Prop :=
+(* ("\<lbrace>_\<rbrace> _ \<lbrace>_ \<bar> _\<rbrace>")*)
+  PrePost P f (fun v => match v with Value a => Q a | Ex e => E e end).
+
+(*lemmas PrePost_defs = PrePost_def PrePostE_def*)
+
+Lemma PrePostE_I (*[case_names Val Err]:*) Regs A Ety (P : predS Regs) f (Q : A -> predS Regs) (E : ex Ety -> predS Regs) :
+  (forall s a s', P s -> List.In (Value a, s') (f s) -> Q a s') ->
+  (forall s e s', P s -> List.In (Ex e, s') (f s) -> E e s') ->
+  PrePostE P f Q E.
+intros. unfold PrePostE.
+unfold PrePost.
+intros s Pre [a | e] s' IN; eauto.
+Qed.
+
+Lemma PrePostE_PrePost Regs A Ety P m (Q : A -> predS Regs) (E : ex Ety -> predS Regs) :
+  PrePost P m (fun v => match v with Value a => Q a | Ex e => E e end) ->
+  PrePostE P m Q E.
+auto.
+Qed.
+
+Lemma PrePostE_elim Regs A Ety P f r s s' (Q : A -> predS Regs) (E : ex Ety -> predS Regs) :
+  PrePostE P f Q E ->
+  P s ->
+  List.In (r, s') (f s) ->
+  (exists v, r = Value v /\ Q v s') \/
+  (exists e, r = Ex e /\ E e s').
+intros PP Pre IN.
+specialize (PP _ Pre _ _ IN).
+destruct r; eauto.
+Qed.
+
+Lemma PrePostE_consequence Regs Aty Ety (P : predS Regs) f A B C (Q : Aty -> predS Regs) (E : ex Ety -> predS Regs) :
+  PrePostE A f B C ->
+  (forall s, P s -> A s) ->
+  (forall v s, B v s -> Q v s) ->
+  (forall e s, C e s -> E e s) ->
+  PrePostE P f Q E.
+intros PP PA BQ CE.
+intros s Pre [a | e] s' IN.
+* apply BQ. specialize (PP _ (PA _ Pre) _ _ IN).
+  apply PP.
+* apply CE. specialize (PP _ (PA _ Pre) _ _ IN).
+  apply PP.
+Qed.
+
+Lemma PrePostE_strengthen_pre Regs Aty Ety (P : predS Regs) f R (Q : Aty -> predS Regs) (E : ex Ety -> predS Regs) :
+  PrePostE R f Q E ->
+  (forall s, P s -> R s) ->
+  PrePostE P f Q E.
+intros PP PR.
+eapply PrePostE_consequence; eauto.
+Qed.
+
+Lemma PrePostE_weaken_post Regs Aty Ety (A : predS Regs) f (B C : Aty -> predS Regs) (E : ex Ety -> predS Regs) :
+  PrePostE A f B E ->
+  (forall v s, B v s -> C v s) ->
+  PrePostE A f C E.
+intros PP BC.
+eauto using PrePostE_consequence.
+Qed.
+
+(*named_theorems PrePostE_compositeI
+named_theorems PrePostE_atomI*)
+
+Lemma PrePostE_conj_conds Regs Aty Ety (P1 P2 : predS Regs) m (Q1 Q2 : Aty -> predS Regs) (E1 E2 : ex Ety -> predS Regs) :
+  PrePostE P1 m Q1 E1 ->
+  PrePostE P2 m Q2 E2 ->
+  PrePostE (fun s => P1 s /\ P2 s) m (fun r s => Q1 r s /\ Q2 r s) (fun e s => E1 e s /\ E2 e s).
+intros H1 H2.
+apply PrePostE_I.
+* intros s a s' [p1 p2] IN.
+  specialize (H1 _ p1 _ _ IN).
+  specialize (H2 _ p2 _ _ IN).
+  simpl in *.
+  auto.
+* intros s a s' [p1 p2] IN.
+  specialize (H1 _ p1 _ _ IN).
+  specialize (H2 _ p2 _ _ IN).
+  simpl in *.
+  auto.
+Qed.
+
+(*lemmas PrePostE_conj_conds_consequence = PrePostE_conj_conds[THEN PrePostE_consequence]*)
+
+Lemma PrePostE_post_mp Regs Aty Ety (P : predS Regs) m (Q Q' : Aty -> predS Regs) (E: ex Ety -> predS Regs) :
+  PrePostE P m Q' E ->
+  PrePostE P m (fun r s => Q' r s -> Q r s) E ->
+  PrePostE P m Q E.
+intros H1 H2.
+eapply PrePostE_conj_conds in H1. 2: apply H2.
+eapply PrePostE_consequence. apply H1. all: simpl; intuition.
+Qed.
+
+Lemma PrePostE_cong Regs Aty Ety (P1 P2 : predS Regs) m1 m2 (Q1 Q2 : Aty -> predS Regs) (E1 E2 : ex Ety -> predS Regs) :
+  (forall s, P1 s <-> P2 s) ->
+  (forall s, P1 s -> m1 s = m2 s) ->
+  (forall r s, Q1 r s <-> Q2 r s) ->
+  (forall e s, E1 e s <-> E2 e s) ->
+  PrePostE P1 m1 Q1 E1 <-> PrePostE P2 m2 Q2 E2.
+intros P12 m12 Q12 E12.
+unfold PrePostE, PrePost.
+split.
+* intros. apply P12 in H0. rewrite <- m12 in H1; auto. specialize (H _ H0 _ _ H1).
+  destruct r; [ apply Q12 | apply E12]; auto.
+* intros. rewrite m12 in H1; auto. apply P12 in H0. specialize (H _ H0 _ _ H1).
+  destruct r; [ apply Q12 | apply E12]; auto.
+Qed.
+
+Lemma PrePostE_True_post (*[PrePostE_atomI, intro, simp]:*) Regs A E P (m : monadS Regs A E) :
+  PrePostE P m (fun _ _ => True) (fun _ _ => True).
+intros s Pre [a | e]; auto.
+Qed.
+
+Lemma PrePostE_any Regs A Ety m (Q : result A Ety -> predS Regs) E :
+  PrePostE (Ety := Ety) (fun s => forall r s', List.In (r, s') (m s) -> match r with Value a => Q a s' | Ex e => E e s' end) m Q E.
+apply PrePostE_I.
+intros. apply (H (Value a)); auto.
+intros. apply (H (Ex e)); auto.
+Qed.
+
+Lemma PrePostE_returnS (*[PrePostE_atomI, intro, simp]:*) Regs A E P (x : A) (Q : ex E -> predS Regs) :
+  PrePostE (P x) (returnS x) P Q.
+unfold PrePostE, PrePost.
+intros s Pre r s' [[= <- <-] | []].
+assumption.
+Qed.
+
+Lemma PrePostE_bindS (*[intro, PrePostE_compositeI]:*) Regs A B Ety P m (f : A -> monadS Regs B Ety) Q R E :
+  (forall s a s', List.In (Value a, s') (m s) -> PrePostE (R a) (f a) Q E) ->
+  PrePostE P m R E ->
+  PrePostE P (bindS m f) Q E.
+intros.
+unfold PrePostE in *.
+eauto using PrePost_bindS.
+Qed.
+
+Lemma PrePostE_bindS_ignore Regs A B Ety (P : predS Regs) (m : monadS Regs A Ety) (f : monadS Regs B Ety) R Q E :
+  PrePostE R f Q E ->
+  PrePostE P m (fun _ => R) E ->
+  PrePostE P (bindS m (fun _ => f)) Q E.
+apply PrePost_bindS_ignore.
+Qed.
+
+Lemma PrePostE_bindS_unit Regs A Ety (P : predS Regs) (m : monadS Regs unit Ety) (f : unit -> monadS Regs A Ety) Q R E :
+  PrePostE R (f tt) Q E ->
+  PrePostE P m (fun _ => R) E ->
+  PrePostE P (bindS m f) Q E.
+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 :
+  PrePostE (Ety := Ety) (fun s => Q (f s) s) (readS f) Q E.
+unfold PrePostE, PrePost, readS.
+intros s Pre [a | e] s' [[= <- <-] | []].
+assumption.
+Qed.
+
+Lemma PrePostE_updateS (*[PrePostE_atomI, intro]:*) Regs Ety f (Q : unit -> predS Regs) (E : ex Ety -> predS Regs) :
+  PrePostE (fun s => Q tt (f s)) (updateS f) Q E.
+intros s Pre [a | e] s' [[= <- <-] | []].
+assumption.
+Qed.
+
+Lemma PrePostE_if_branch (*[PrePostE_compositeI]:*) Regs A Ety (b : bool) (f g : monadS Regs A Ety) Pf Pg Q E :
+  (b = true  -> PrePostE Pf f Q E) ->
+  (b = false -> PrePostE Pg g Q E) ->
+  PrePostE (if b then Pf else Pg) (if b then f else g) Q E.
+destruct b; auto.
+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) ->
+  PrePostE P (if b then f else g) Q E.
+destruct b; auto.
+Qed.
+
+Lemma PrePostE_if_then Regs A Ety (b : bool) (f g : monadS Regs A Ety) P Q E :
+  b = true ->
+  PrePostE P f Q E ->
+  PrePostE P (if b then f else g) Q E.
+intros; subst; auto.
+Qed.
+
+Lemma PrePostE_if_else Regs A Ety (b : bool) (f g : monadS Regs A Ety) P Q E :
+  b = false ->
+  PrePostE P g Q E ->
+  PrePostE P (if b then f else g) Q E.
+intros; subst; auto.
+Qed.
+
+Lemma PrePostE_prod_cases (*[PrePostE_compositeI]:*) Regs A B C Ety x (f : A -> B -> monadS Regs C Ety) P Q E :
+  PrePostE P (f (fst x) (snd x)) Q E ->
+  PrePostE P (match x with (a, b) => f a b end) Q E.
+destruct x; auto.
+Qed.
+
+Lemma PrePostE_option_cases (*[PrePostE_compositeI]:*) Regs A B Ety x (s : option A -> monadS Regs B Ety) n PS PN Q E :
+  (forall a, PrePostE (PS a) (s a) Q E) ->
+  PrePostE PN n Q E ->
+  PrePostE (match x with Some a => PS a | None => PN end) (match x with Some a => s a | None => n end) Q E.
+apply PrePost_option_cases.
+Qed.
+
+Lemma PrePostE_sum_cases (*[PrePostE_compositeI]:*) Regs A B C Ety x (l : A -> monadS Regs C Ety) (r : B -> monadS Regs C Ety) Pl Pr Q E :
+  (forall a, PrePostE (Pl a) (l a) Q E) ->
+  (forall b, PrePostE (Pr b) (r b) Q E) ->
+  PrePostE (match x with inl a => Pl a | inr b => Pr b end) (match x with inl a => l a | inr b => r b end) Q E.
+intros; destruct x; auto.
+Qed.
+
+Lemma PrePostE_let (*[PrePostE_compositeI]:*) Regs A B Ety y (m : A -> monadS Regs B Ety) P Q E :
+  PrePostE P (m y) Q E ->
+  PrePostE P (let x := y in m x) Q E.
+auto.
+Qed.
+
+Lemma PrePostE_and_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 R else Q false) E ->
+  PrePostE P (and_boolS l r) Q E.
+intros Hr Hl.
+unfold and_boolS.
+eapply PrePostE_bindS.
+* intros.
+  instantiate (1 := fun a => if a then R else Q false).
+  destruct a; eauto.
+  apply PrePostE_returnS.
+* assumption.
+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 ->
+  PrePostE P (or_boolS l r) Q E.
+intros Hr Hl.
+unfold or_boolS.
+eapply PrePostE_bindS.
+* intros.
+  instantiate (1 := fun a => if a then Q true else R).
+  destruct a; eauto.
+  apply PrePostE_returnS.
+* assumption.
+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.
+intros s Pre r s' [[= <- <-] | []].
+assumption.
+Qed.
+
+Lemma PrePostE_assert_expS (*[PrePostE_atomI, intro]:*) Regs Ety (c : bool) m P (Q : ex Ety -> predS Regs) :
+  PrePostE (if c then P tt else Q (Failure m)) (assert_expS c m) P Q.
+unfold assert_expS.
+destruct c; auto using PrePostE_returnS, 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.
+destruct v; auto using PrePostE_returnS, PrePostE_failS.
+Qed.
+
+Lemma PrePostE_exitS (*[PrePostE_atomI, intro]:*) Regs A Ety msg (Q : A -> predS Regs) (E : ex Ety -> predS Regs) :
+  PrePostE (E (Failure "exit")) (exitS msg) Q E.
+unfold exitS.
+apply PrePostE_failS.
+Qed.
+
+Lemma PrePostE_chooseS (*[intro, PrePostE_atomI]:*) Regs A Ety (xs : list A) (Q : A -> predS Regs) (E : ex Ety -> predS Regs) :
+  PrePostE (fun s => forall x, List.In x xs -> Q x s) (chooseS xs) Q E.
+unfold chooseS.
+intros s IN r s' IN'.
+apply List.in_map_iff in IN'.
+destruct IN' as (x & [= <- <-] & IN').
+auto.
+Qed.
+
+Lemma PrePostE_throwS (*[PrePostE_atomI]:*) Regs A Ety e (Q : A -> predS Regs) (E : ex Ety -> predS Regs) :
+  PrePostE (E (Throw e)) (throwS e) Q E.
+unfold throwS.
+intros s Pre r s' [[= <- <-] | []].
+assumption.
+Qed.
+
+Lemma PrePostE_try_catchS (*[PrePostE_compositeI]:*) Regs A E1 E2 m h P (Ph : E1 -> predS Regs) (Q : A -> predS Regs) (E : ex E2 -> predS Regs) :
+  (forall s e s', List.In (Ex (Throw e), s') (m s) -> PrePostE (Ph e) (h e) Q E) ->
+  PrePostE P m Q (fun ex => match ex with Throw e => Ph e | Failure msg => E (Failure msg) end) ->
+  PrePostE P (try_catchS m h) Q E.
+intros.
+intros s Pre r s' IN.
+destruct (try_catchS_cases IN) as [(a' & [= ->] & IN') | [(msg & [= ->] & IN') | (e & s'' & IN1 & IN2)]].
+* specialize (H0 _ Pre _ _ IN'). apply H0.
+* specialize (H0 _ Pre _ _ IN'). apply H0.
+* specialize (H _ _ _ IN1). specialize (H0 _ Pre _ _ IN1). simpl in *.
+    specialize (H _ H0 _ _ IN2). apply H.
+Qed.
+
+Lemma PrePostE_catch_early_returnS (*[PrePostE_compositeI]:*) Regs A Ety m P (Q : A -> predS Regs) (E : ex Ety -> predS Regs) :
+  PrePostE P m Q (fun ex => match ex with Throw (inl a) => Q a | Throw (inr e) => E (Throw e) | Failure msg => E (Failure msg) end) ->
+  PrePostE P (catch_early_returnS m) Q E.
+unfold catch_early_returnS.
+intro H.
+apply PrePostE_try_catchS with (Ph := fun e => match e with inl a => Q a | inr e => E (Throw e) end).
+* intros. destruct e.
+  + apply PrePostE_returnS.
+  + apply PrePostE_throwS.
+* apply H.
+Qed.
+
+Lemma PrePostE_early_returnS (*[PrePostE_atomI]:*) Regs A E1 E2 r (Q : A -> predS Regs) (E : ex (E1 + E2) -> predS Regs) :
+  PrePostE (E (Throw (inl r))) (early_returnS r) Q E.
+unfold early_returnS.
+apply PrePostE_throwS.
+Qed.
+
+Lemma PrePostE_liftRS (*[PrePostE_compositeI]:*) Regs A E1 E2 m P (Q : A -> predS Regs) (E : ex (E1 + E2) -> predS Regs) :
+  PrePostE P m Q (fun ex => match ex with Throw e => E (Throw (inr e)) | Failure msg => E (Failure msg) end) ->
+  PrePostE P (liftRS m) Q E.
+unfold liftRS.
+apply PrePostE_try_catchS.
+auto using PrePostE_throwS.
+Qed.
+
+Lemma PrePostE_foreachS_Cons Regs A Vars Ety (x : A) xs vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) :
+  (forall s vars' s', List.In (Value vars', s') (body x vars s) -> PrePostE (Q vars') (foreachS xs vars' body) Q E) ->
+  PrePostE (Q vars) (body x vars) Q E ->
+  PrePostE (Q vars) (foreachS (x :: xs) vars body) Q E.
+intros.
+simpl.
+apply PrePostE_bindS with (R := Q); auto.
+Qed.
+
+Lemma PrePostE_foreachS_invariant Regs A Vars Ety (xs : list A) vars body (Q : Vars -> predS Regs) (E : ex Ety -> predS Regs) :
+  (forall x vars, List.In x xs -> PrePostE (Q vars) (body x vars) Q E) ->
+  PrePostE (Q vars) (foreachS xs vars body) Q E.
+unfold PrePostE.
+intros H.
+apply PrePost_foreachS_invariant with (Q := fun v => match v with Value a => Q a | Ex e => E e end).
+auto.
+Qed.
+(*
+Lemma PrePostE_untilS:
+  assumes dom: (forall s, Inv Q vars s -> untilS_dom (vars, cond, body, s)"
+    and cond: (forall vars, PrePostE (Inv' Q vars) (cond vars) (fun c s' => Inv Q vars s' /\ (c \<longrightarrow> Q vars s')) E"
+    and body: (forall vars, PrePostE (Inv Q vars) (body vars) (Inv' Q) E"
+  shows "PrePostE (Inv Q vars) (untilS vars cond body) Q E"
+proof (unfold PrePostE_def, rule PrePostI)
+  fix s r s'
+  assume Inv_s: "Inv Q vars s" and r: "(r, s') \<in> untilS vars cond body s"
+  with dom[OF Inv_s] cond body
+  show "(case r of Value a => Q a | result.Ex e => E e) s'"
+  proof (induction vars cond body s rule: untilS.pinduct[case_names Step])
+    case (Step vars cond body s)
+    consider
+        (Value) vars' c sb sc where "(Value vars', sb) \<in> body vars s" and "(Value c, sc) \<in> cond vars' sb"
+                                and "if c then r = Value vars' /\ s' = sc else (r, s') \<in> untilS vars' cond body sc"
+      | (Ex) e where "(Ex e, s') \<in> bindS (body vars) cond s" and "r = Ex e"
+      using Step(1,6)
+      by (auto simp: untilS.psimps returnS_def Ex_bindS_iff elim!: bindS_cases split: if_splits; fastforce)
+    then show ?case
+    proof cases
+      case Value
+      then show ?thesis using Step.IH[OF Value(1,2) _ Step(3,4)] Step(3,4,5)
+        by (auto split: if_splits elim: PrePostE_elim)
+    next
+      case Ex
+      then show ?thesis using Step(3,4,5) by (auto elim!: bindS_cases PrePostE_elim)
+    qed
+  qed
+qed
+
+lemma PrePostE_untilS_pure_cond:
+  assumes dom: (forall s, Inv Q vars s -> untilS_dom (vars, returnS \<circ> cond, body, s)"
+    and body: (forall vars, PrePostE (Inv Q vars) (body vars) (fun vars' s' => Inv Q vars' s' /\ (cond vars' \<longrightarrow> Q vars' s')) E"
+  shows "PrePostE (Inv Q vars) (untilS vars (returnS \<circ> cond) body) Q E"
+  using assms by (intro PrePostE_untilS) (auto simp: comp_def)
+
+lemma PrePostE_liftState_untilM:
+  assumes dom: (forall s, Inv Q vars s -> untilM_dom (vars, cond, body)"
+    and cond: (forall vars, PrePostE (Inv' Q vars) (liftState r (cond vars)) (fun c s' => Inv Q vars s' /\ (c \<longrightarrow> Q vars s')) E"
+    and body: (forall vars, PrePostE (Inv Q vars) (liftState r (body vars)) (Inv' Q) E"
+  shows "PrePostE (Inv Q vars) (liftState r (untilM vars cond body)) Q E"
+proof -
+  have domS: "untilS_dom (vars, liftState r \<circ> cond, liftState r \<circ> body, s)" if "Inv Q vars s" for s
+    using dom that by (intro untilM_dom_untilS_dom)
+  then have "PrePostE (Inv Q vars) (untilS vars (liftState r \<circ> cond) (liftState r \<circ> body)) Q E"
+    using cond body by (auto intro: PrePostE_untilS simp: comp_def)
+  moreover have "liftState r (untilM vars cond body) s = untilS vars (liftState r \<circ> cond) (liftState r \<circ> body) s"
+    if "Inv Q vars s" for s
+    unfolding liftState_untilM[OF domS[OF that] dom[OF that]] ..
+  ultimately show ?thesis by (auto cong: PrePostE_cong)
+qed
+
+lemma PrePostE_liftState_untilM_pure_cond:
+  assumes dom: (forall s, Inv Q vars s -> untilM_dom (vars, return \<circ> cond, body)"
+    and body: (forall vars, PrePostE (Inv Q vars) (liftState r (body vars)) (fun vars' s' => Inv Q vars' s' /\ (cond vars' \<longrightarrow> Q vars' s')) E"
+  shows "PrePostE (Inv Q vars) (liftState r (untilM vars (return \<circ> cond) body)) Q E"
+  using assms by (intro PrePostE_liftState_untilM) (auto simp: comp_def liftState_simp)
+*)
+Lemma PrePostE_choose_boolS_any (*[PrePostE_atomI]:*) Regs Ety unit_val (Q : bool -> predS Regs) (E : ex Ety -> predS Regs) :
+  PrePostE (fun s => forall b, Q b s) (choose_boolS unit_val) Q E.
+unfold choose_boolS, seqS.
+eapply PrePostE_strengthen_pre.
+apply PrePostE_chooseS.
+simpl. intros. destruct x; auto.
+Qed.
+
+Lemma PrePostE_bool_of_bitU_nondetS_any Regs Ety b (Q : bool -> predS Regs) (E : ex Ety -> predS Regs) :
+  PrePostE (fun s => forall b, Q b s) (bool_of_bitU_nondetS b) Q E.
+unfold bool_of_bitU_nondetS, undefined_boolS.
+destruct b.
+* intros s Pre r s' [[= <- <-] | []]. auto.
+* intros s Pre r s' [[= <- <-] | []]. auto.
+* apply PrePostE_choose_boolS_any.
+Qed.
+(*
+Lemma PrePostE_bools_of_bits_nondetS_any:
+  PrePostE (fun s => forall bs, Q bs s) (bools_of_bits_nondetS bs) Q E.
+  unfolding bools_of_bits_nondetS_def
+  by (rule PrePostE_weaken_post[where B = "fun _ s => forall bs, Q bs s"], rule PrePostE_strengthen_pre,
+      (rule PrePostE_foreachS_invariant[OF PrePostE_strengthen_pre] PrePostE_bindS PrePostE_returnS
+            PrePostE_bool_of_bitU_nondetS_any)+)
+     auto
+*)
+Lemma PrePostE_choose_boolsS_any Regs Ety n (Q : list bool -> predS Regs) (E : ex Ety -> predS Regs) :
+  PrePostE (fun s => forall bs, Q bs s) (choose_boolsS n) Q E.
+unfold choose_boolsS, genlistS.
+apply PrePostE_weaken_post with (B := fun _ s => forall bs, Q bs s).
+* apply PrePostE_foreachS_invariant with (Q := fun _ s => forall bs, Q bs s).
+  intros. apply PrePostE_bindS with (R := fun _ s => forall bs, Q bs s).
+  + intros. apply PrePostE_returnS with (P := fun _ s => forall bs, Q bs s).
+  + eapply PrePostE_strengthen_pre.
+    apply PrePostE_choose_boolS_any.
+    intuition.
+* intuition.
+Qed.
+
+Lemma nth_error_exists {A} {l : list A} {n} :
+  n < Datatypes.length l -> exists x, List.In x l /\ List.nth_error l n = Some x.
+revert n. induction l.
+* simpl. intros. apply PeanoNat.Nat.nlt_0_r in H. destruct H.
+* intros. destruct n.
+  + exists a. auto with datatypes.
+  + simpl in H. apply Lt.lt_S_n in H.
+    destruct (IHl n H) as [x H1].
+    intuition eauto with datatypes.
+Qed.
+
+Lemma nth_error_modulo {A} {xs : list A} n :
+  xs <> nil ->
+  exists x, List.In x xs /\ List.nth_error xs (PeanoNat.Nat.modulo n (Datatypes.length xs)) = Some x.
+intro notnil.
+assert (Datatypes.length xs <> 0) by (rewrite List.length_zero_iff_nil; auto).
+assert (PeanoNat.Nat.modulo n (Datatypes.length xs) < Datatypes.length xs) by auto using PeanoNat.Nat.mod_upper_bound.
+destruct (nth_error_exists H0) as [x [H1 H2]].
+exists x.
+auto.
+Qed.
+
+Lemma PrePostE_internal_pick Regs A Ety (xs : list A) (Q : A -> predS Regs) (E : ex Ety -> predS Regs) :
+  xs <> nil ->
+  PrePostE (fun s => forall x, List.In x xs -> Q x s) (internal_pickS xs) Q E.
+unfold internal_pickS.
+intro notnil.
+eapply PrePostE_bindS with (R := fun _ s => forall x, List.In x xs -> Q x s).
+* intros.
+  destruct (nth_error_modulo (Sail2_values.nat_of_bools a) notnil) as (x & IN & nth).
+  rewrite nth.
+  eapply PrePostE_strengthen_pre.
+  apply PrePostE_returnS.
+  intuition.
+* eapply PrePostE_strengthen_pre.
+  apply PrePostE_choose_boolsS_any.
+  intuition.
+Qed.
diff --git a/lib/coq/Makefile b/lib/coq/Makefile
index f763db6f..fa453d90 100644
--- a/lib/coq/Makefile
+++ b/lib/coq/Makefile
@@ -1,6 +1,8 @@
 BBV_DIR?=../../../bbv
 
-SRC=Sail2_prompt_monad.v  Sail2_prompt.v  Sail2_impl_base.v  Sail2_instr_kinds.v  Sail2_operators_bitlists.v  Sail2_operators_mwords.v  Sail2_operators.v  Sail2_values.v  Sail2_state_monad.v  Sail2_state.v  Sail2_state_lifting.v  Sail2_string.v  Sail2_real.v
+CORESRC=Sail2_prompt_monad.v  Sail2_prompt.v  Sail2_impl_base.v  Sail2_instr_kinds.v  Sail2_operators_bitlists.v  Sail2_operators_mwords.v  Sail2_operators.v  Sail2_values.v  Sail2_state_monad.v  Sail2_state.v  Sail2_state_lifting.v  Sail2_string.v  Sail2_real.v
+PROOFSRC=Sail2_state_monad_lemmas.v Sail2_state_lemmas.v Hoare.v
+SRC=$(CORESRC) $(PROOFSRC)
 
 COQ_LIBS = -R . Sail -R "$(BBV_DIR)/theories" bbv
 
diff --git a/lib/coq/Sail2_instr_kinds.v b/lib/coq/Sail2_instr_kinds.v
index 338bf10b..85d78226 100644
--- a/lib/coq/Sail2_instr_kinds.v
+++ b/lib/coq/Sail2_instr_kinds.v
@@ -139,12 +139,25 @@ instance (Show write_kind)
   end
 end
 *)
+
+Inductive a64_barrier_domain :=
+  A64_FullShare
+  | A64_InnerShare
+  | A64_OuterShare
+  | A64_NonShare.
+
+Inductive a64_barrier_type :=
+  A64_barrier_all
+  | A64_barrier_LD
+  | A64_barrier_ST.
+
 Inductive barrier_kind :=
   (* Power barriers *)
   Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync
   (* AArch64 barriers *)
-  | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB
-  | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB
+  | Barrier_DMB (*: a64_barrier_domain -> a64_barrier_type -> barrier_kind*)
+  | Barrier_DSB (*: a64_barrier_domain -> a64_barrier_type -> barrier_kind*)
+  | Barrier_ISB
  (* | Barrier_TM_COMMIT*)
   (* MIPS barriers *)
   | Barrier_MIPS_SYNC
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 68d097fb..b5e94e46 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -53,6 +53,10 @@ Definition foreach_ZM_down {rv e Vars} from to step vars body `{ArithFact (0 < s
 
 (*declare {isabelle} termination_argument foreachM = automatic*)
 
+Definition genlistM {A RV E} (f : nat -> monad RV A E) (n : nat) : monad RV (list A) E :=
+  let indices := List.seq 0 n in
+  foreachM indices [] (fun n xs => (f n >>= (fun x => returnm (xs ++ [x])))).
+
 (*val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e*)
 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).
@@ -181,23 +185,21 @@ Definition untilMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool
     else slice vec (start_vec - size_r1) (start_vec - size_vec) in
   write_reg r1 r1_v >> write_reg r2 r2_v*)
 
-Fixpoint pick_bit_list {rv e} (n:nat) : monad rv (list bool) e :=
-  match n with
-  | O => returnm []
-  | S m => choose_bool "pick_bit_list" >>= fun b =>
-           pick_bit_list m >>= fun t =>
-           returnm (b::t)
-  end%list.
+Definition choose_bools {RV E} (descr : string) (n : nat) : monad RV (list bool) E :=
+  genlistM (fun _ => choose_bool descr) n.
+
+Definition choose {RV A E} (descr : string) (xs : list A) : monad RV A E :=
+  (* Use sufficiently many nondeterministically chosen bits and convert into an
+     index into the list *)
+  choose_bools descr (List.length xs) >>= fun bs =>
+  let idx := ((nat_of_bools bs) mod List.length xs)%nat in
+  match List.nth_error xs idx with
+    | Some x => returnm x
+    | None => Fail ("choose " ++ descr)
+  end.
 
 Definition internal_pick {rv a e} (xs : list a) : monad rv a e :=
-  let n := length xs in
-  match xs with
-  | h::_ =>
-    pick_bit_list (2 + n) >>= fun bs =>
-    let i := (Word.wordToNat (wordFromBitlist bs) mod n)%nat in
-    returnm (List.nth i xs h)
-  | [] => Fail "internal_pick called on empty list"
-  end.
+  choose "internal_pick" xs.
 
 Fixpoint undefined_word_nat {rv e} n : monad rv (Word.word n) e :=
   match n with
diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v
index b73d5013..bd18783f 100644
--- a/lib/coq/Sail2_state.v
+++ b/lib/coq/Sail2_state.v
@@ -32,7 +32,7 @@ end.
 
 (*val genlistS : forall 'a 'rv 'e. (nat -> monadS 'rv 'a 'e) -> nat -> monadS 'rv (list 'a) 'e*)
 Definition genlistS {A RV E} (f : nat -> monadS RV A E) n : monadS RV (list A) E :=
-  let indices := genlist (fun n => n) n in
+  let indices := List.seq 0 n in
   foreachS indices [] (fun n xs => (f n >>$= (fun x => returnS (xs ++ [x])))).
 
 (*val and_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e*)
@@ -43,6 +43,31 @@ Definition and_boolS {RV E} (l r : monadS RV bool E) : monadS RV bool E :=
 Definition or_boolS {RV E} (l r : monadS RV bool E) : monadS RV bool E :=
  l >>$= (fun l => if l then returnS true else r).
 
+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.
+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.
+
 (*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 :=
 match b with
@@ -96,21 +121,45 @@ let rec untilS vars cond body s =
   (cond vars >>$= (fun cond_val s'' ->
   if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s
 *)
+
+Fixpoint whileST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E :=
+  if Z_ge_dec limit 0 then
+    cond vars >>$= fun cond_val =>
+    if cond_val then
+      body vars >>$= fun vars => whileST' (limit - 1) vars cond body (_limit_reduces acc)
+    else returnS vars
+  else failS "Termination limit reached".
+
+Definition whileST {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E :=
+  whileST' limit vars cond body (Zwf_guarded limit).
+
+(*val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
+                ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e*)
+Fixpoint untilST' {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) (acc : Acc (Zwf 0) limit) : monadS RV Vars E :=
+  if Z_ge_dec limit 0 then
+    body vars >>$= fun vars =>
+    cond vars >>$= fun cond_val =>
+    if cond_val then returnS vars else untilST' (limit - 1) vars cond body (_limit_reduces acc)
+  else failS "Termination limit reached".
+
+Definition untilST {RV Vars E} limit (vars : Vars) (cond : Vars -> monadS RV bool E) (body : Vars -> monadS RV Vars E) : monadS RV Vars E :=
+  untilST' limit vars cond body (Zwf_guarded limit).
+
+
 (*val choose_boolsS : forall 'rv 'e. nat -> monadS 'rv (list bool) 'e*)
 Definition choose_boolsS {RV E} n : monadS RV (list bool) E :=
  genlistS (fun _ => choose_boolS tt) n.
 
 (* TODO: Replace by chooseS and prove equivalence to prompt monad version *)
-(*val internal_pickS : forall 'rv 'a 'e. list 'a -> monadS 'rv 'a 'e
-let internal_pickS xs =
+(*val internal_pickS : forall 'rv 'a 'e. list 'a -> monadS 'rv 'a 'e*)
+Definition internal_pickS {RV A E} (xs : list A) : monadS RV A E :=
   (* Use sufficiently many nondeterministically chosen bits and convert into an
      index into the list *)
-  choose_boolsS (List.length xs) >>$= fun bs ->
-  let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
-  match index xs idx with
-    | Just x -> returnS x
-    | Nothing -> failS "choose internal_pick"
-  end
+  choose_boolsS (List.length xs) >>$= fun bs =>
+  let idx := ((nat_of_bools bs) mod List.length xs)%nat in
+  match List.nth_error xs idx with
+    | Some x => returnS x
+    | None => failS "choose internal_pick"
+  end.
 
 
-*)
diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v
new file mode 100644
index 00000000..563a17a6
--- /dev/null
+++ b/lib/coq/Sail2_state_lemmas.v
@@ -0,0 +1,796 @@
+Require Import Sail2_values Sail2_prompt_monad Sail2_prompt Sail2_state_monad Sail2_state Sail2_state Sail2_state_lifting.
+Require Import Sail2_state_monad_lemmas.
+
+(* Monad lifting *)
+
+Lemma liftState_bind Regval Regs A B E {r : Sail2_values.register_accessors Regs Regval} {m : monad Regval A E} {f : A -> monad Regval B E} {s} :
+  liftState r (bind m f) s = bindS (liftState r m) (fun x => liftState r (f x)) s.
+revert s. induction m; simpl.
+all: try (intros; unfold seqS; rewrite bindS_assoc; auto using bindS_ext_cong).
+all: try auto.
+* intro s.
+  rewrite bindS_returnS_left.
+  reflexivity.
+Qed.
+Hint Rewrite liftState_bind : liftState.
+
+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.
+
+(*
+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.
+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.
+
+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_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 s :
+  @liftState Regs Regval _ E r (and_boolM x y) s = and_boolS (liftState r x) (liftState r y) s.
+unfold and_boolM, and_boolS.
+rewrite liftState_bind.
+apply bindS_ext_cong; auto.
+intros. rewrite liftState_if_distrib.
+reflexivity.
+Qed.
+Lemma liftState_and_boolMP Regs Regval E P Q R r x y s H :
+  @liftState Regs Regval _ E r (@and_boolMP _ _ P Q R x y H) s = and_boolSP (liftState r x) (liftState r y) s.
+unfold and_boolMP, and_boolSP.
+rewrite liftState_bind.
+simpl.
+apply bindS_ext_cong; auto.
+intros [[|] [A]] s' ?.
+* rewrite liftState_bind;
+  simpl;
+  apply bindS_ext_cong; auto;
+  intros [a' A'] s'' ?;
+  rewrite liftState_return;
+  reflexivity.
+* rewrite liftState_return.
+  reflexivity.
+Qed.
+
+Lemma liftState_or_boolM Regs Regval E r x y s :
+  @liftState Regs Regval _ E r (or_boolM x y) s = or_boolS (liftState r x) (liftState r y) s.
+unfold or_boolM, or_boolS.
+rewrite liftState_bind.
+apply bindS_ext_cong; auto.
+intros. rewrite liftState_if_distrib.
+reflexivity.
+Qed.
+Lemma liftState_or_boolMP Regs Regval E P Q R r x y s H :
+  @liftState Regs Regval _ E r (@or_boolMP _ _ P Q R x y H) s = or_boolSP (liftState r x) (liftState r y) s.
+unfold or_boolMP, or_boolSP.
+rewrite liftState_bind.
+simpl.
+apply bindS_ext_cong; auto.
+intros [[|] [A]] s' ?.
+* rewrite liftState_return.
+  reflexivity.
+* rewrite liftState_bind;
+  simpl;
+  apply bindS_ext_cong; auto;
+  intros [a' A'] s'' ?;
+  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
+             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 s :
+  @liftState Regs Regval A E2 r (try_catch (E1 := E1) m h) s = try_catchS (liftState r m) (fun e => liftState r (h e)) s.
+revert s.
+induction m; intros; simpl;
+try solve
+[ auto
+| unfold seqS;
+  erewrite try_catchS_bindS_no_throw; intros;
+  only 2,3: (autorewrite with ignore_throw; reflexivity);
+  apply bindS_ext_cong; auto
+].
+rewrite try_catchS_throwS. reflexivity.
+Qed.
+Hint Rewrite 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.
+
+Lemma liftState_catch_early_return (*[liftState_simp]:*) Regs Regval A E r m s :
+  liftState (Regs := Regs) r (@catch_early_return Regval A E m) s = catch_early_returnS (liftState r m) s.
+unfold catch_early_return, catch_early_returnS.
+autorewrite with liftState.
+apply try_catchS_cong; auto.
+intros [a | e] s'; auto.
+Qed.
+Hint Rewrite liftState_catch_early_return : liftState.
+
+Lemma liftState_liftR Regs Regval A R E r m s :
+  liftState (Regs := Regs) r (@liftR Regval A R E m) s = liftRS (liftState r m) s.
+unfold liftR, liftRS. autorewrite with liftState.
+apply try_catchS_cong; auto.
+Qed.
+Hint Rewrite liftState_liftR : liftState.
+
+Lemma liftState_try_catchR Regs Regval A R E1 E2 r m h s :
+  liftState (Regs := Regs) r (@try_catchR Regval A R E1 E2 m h) s = try_catchRS (liftState r m) (fun x => liftState r (h x)) s.
+unfold try_catchR, try_catchRS. autorewrite with liftState.
+apply try_catchS_cong; auto.
+intros [r' | e] s'; auto.
+Qed.
+Hint Rewrite liftState_try_catchR : liftState.
+(*
+Lemma liftState_bool_of_bitU_nondet Regs Regval :
+  "liftState r (bool_of_bitU_nondet b) = bool_of_bitU_nondetS b"
+  by (cases b; auto simp: bool_of_bitU_nondet_def bool_of_bitU_nondetS_def liftState_simp)
+Hint Rewrite liftState_bool_of_bitU_nondet : liftState.
+*)
+Lemma liftState_read_memt Regs Regval A B E H rk a sz r s :
+  liftState (Regs := Regs) r (@read_memt Regval A B E H rk a sz) s = read_memtS rk a sz s.
+unfold read_memt, read_memt_bytes, read_memtS, maybe_failS. simpl.
+apply bindS_ext_cong; auto.
+intros [byte bit] s' valIn.
+destruct (option_map _); auto.
+Qed.
+Hint Rewrite liftState_read_memt : liftState.
+
+Lemma liftState_read_mem Regs Regval A B E H rk asz a sz r s :
+  liftState (Regs := Regs) r (@read_mem Regval A B E H rk asz a sz) s = read_memS rk a sz s.
+unfold read_mem, read_memS, read_memtS. simpl.
+unfold read_mem_bytesS, read_memt_bytesS.
+repeat rewrite bindS_assoc.
+apply bindS_ext_cong; auto.
+intros [ bytes | ] s' valIn; auto. simpl.
+apply bindS_ext_cong; auto.
+intros [byte bit] s'' valIn'.
+rewrite bindS_returnS_left. autorewrite with liftState.
+destruct (option_map _); auto.
+Qed.
+Hint Rewrite 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.
+
+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 (Sail2_values.mem_bytes_of_bits v); auto.
+Qed.
+Hint Rewrite 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 (Sail2_values.mem_bytes_of_bits v); simpl; auto.
+Qed.
+Hint Rewrite 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' s :
+  (forall s, map_bind reg.(of_regval) (get_regval' reg.(name) s) = Some (reg.(read_from) s)) ->
+  liftState (Regs := Regs) (get_regval', set_regval') (@read_reg _ Regval A E reg) s = readS (fun x => reg.(read_from) (regstate x)) s.
+intros.
+unfold read_reg. simpl. unfold readS.
+erewrite bindS_rw_left. 2: {
+  apply bindS_returnS_left.
+}
+specialize (H (regstate s)).
+destruct (get_regval' _ _) as [v | ]; only 2: discriminate H.
+rewrite bindS_returnS_left.
+simpl in *.
+rewrite H.
+reflexivity.
+Qed.
+
+Lemma liftState_write_reg_updateS Regs Regval A E get_regval' set_regval' reg (v : A) s :
+  (forall s, set_regval' (name reg) (regval_of reg v) s = Some (write_to reg v s)) ->
+  liftState (Regs := Regs) (Regval := Regval) (E := E) (get_regval', set_regval') (write_reg reg v) s = updateS (fun s => {| regstate := (write_to reg v s.(regstate)); memstate := s.(memstate); tagstate := s.(tagstate) |}) s.
+intros.
+unfold write_reg. simpl. unfold readS, seqS.
+erewrite bindS_rw_left. 2: {
+  apply bindS_returnS_left.
+}
+specialize (H (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.
+
+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 s :
+  liftState (Regs := Regs) r (foreachM xs vars body) s = foreachS xs vars (fun x vars => liftState r (body x vars)) s.
+revert vars s.
+induction xs as [ | h t].
+* reflexivity.
+* intros vars s. simpl.
+  autorewrite with liftState.
+  apply bindS_ext_cong; auto.
+Qed.
+Hint Rewrite liftState_foreachM : liftState.
+
+Lemma foreachS_cong {A RV Vars E} xs vars f f' s :
+  (forall a vars s, f a vars s = f' a vars s) ->
+  @foreachS A RV Vars E xs vars f s = foreachS xs vars f' s.
+intro H.
+revert s vars.
+induction xs.
+* reflexivity.
+* intros. simpl.
+  apply bindS_ext_cong; auto.
+Qed.
+
+Lemma liftState_genlistM Regs Regval A E r f n s :
+  liftState (Regs := Regs) r (@genlistM A Regval E f n) s = genlistS (fun x => liftState r (f x)) n s.
+unfold genlistM, genlistS.
+autorewrite with liftState.
+apply foreachS_cong.
+intros; autorewrite with liftState.
+apply bindS_ext_cong; auto.
+Qed.
+Hint Rewrite liftState_genlistM : liftState.
+
+Lemma liftState_choose_bools Regs Regval E descr n r s :
+  liftState (Regs := Regs) r (@choose_bools Regval E descr n) s = choose_boolsS n s.
+unfold choose_bools, choose_boolsS.
+autorewrite with liftState.
+reflexivity.
+Qed.
+Hint Rewrite liftState_choose_bools : liftState.
+
+(*
+Lemma liftState_bools_of_bits_nondet[liftState_simp]:
+  "liftState r (bools_of_bits_nondet bs) = bools_of_bits_nondetS bs"
+  unfolding bools_of_bits_nondet_def bools_of_bits_nondetS_def
+  by (auto simp: liftState_simp comp_def)
+Hint Rewrite liftState_choose_bools : liftState.
+*)
+
+Lemma liftState_internal_pick Regs Regval A E r (xs : list A) s :
+  liftState (Regs := Regs) (Regval := Regval) (E := E) r (internal_pick xs) s = internal_pickS xs s.
+unfold internal_pick, internal_pickS.
+unfold choose.
+autorewrite with liftState.
+apply bindS_ext_cong.
+* autorewrite with liftState.
+  reflexivity.
+* intros.
+  destruct (nth_error _ _); auto.
+Qed.
+Hint Rewrite liftState_internal_pick : 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) s :
+  @liftRS B R Regs E (bindS m f) s = bindS (liftRS m) (fun x => liftRS (f x)) 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
+*)
+
+Local Opaque _limit_reduces.
+Ltac gen_reduces :=
+  match goal with |- context[@_limit_reduces ?a ?b ?c] => generalize (@_limit_reduces a b c) end.
+
+Lemma liftState_whileM RV Vars E r limit vars cond (body : Vars -> monad RV Vars E) s :
+  liftState (Regs := RV) r (whileMT limit vars cond body) s = whileST limit vars (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)) s.
+unfold whileMT, whileST.
+revert vars s.
+destruct (Z.le_decidable 0 limit).
+* generalize (Zwf_guarded limit) as acc.
+  apply Wf_Z.natlike_ind with (x := limit).
+  + intros [acc] *; simpl.
+    autorewrite with liftState.
+    apply bindS_ext_cong; auto.
+    intros. rewrite liftState_if_distrib.
+    destruct a; autorewrite with liftState; auto.
+    apply bindS_ext_cong; auto.
+    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.
+    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 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 limit vars cond (body : Vars -> monad RV Vars E) s :
+  liftState (Regs := RV) r (untilMT limit vars cond body) s = untilST limit vars (fun vars => liftState r (cond vars)) (fun vars => liftState r (body vars)) s.
+unfold untilMT, untilST.
+revert vars s.
+destruct (Z.le_decidable 0 limit).
+* generalize (Zwf_guarded limit) as acc.
+  apply Wf_Z.natlike_ind with (x := limit).
+  + intros [acc] *; simpl.
+    autorewrite with liftState.
+    apply bindS_ext_cong; auto.
+    intros. autorewrite with liftState.
+    apply bindS_ext_cong; auto.
+    intros. rewrite liftState_if_distrib.
+    destruct a0; 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.
+    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.
+
+(*
+
+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
+*)
\ No newline at end of file
diff --git a/lib/coq/Sail2_state_monad.v b/lib/coq/Sail2_state_monad.v
index 235e4b9e..faee9569 100644
--- a/lib/coq/Sail2_state_monad.v
+++ b/lib/coq/Sail2_state_monad.v
@@ -50,10 +50,10 @@ Definition returnS {Regs A E} (a:A) : monadS Regs A E := fun s => [(Value a,s)].
 (*val bindS : forall 'regs 'a 'b 'e. monadS 'regs 'a 'e -> ('a -> monadS 'regs 'b 'e) -> monadS 'regs 'b 'e*)
 Definition bindS {Regs A B E} (m : monadS Regs A E) (f : A -> monadS Regs B E) : monadS Regs B E :=
  fun (s : sequential_state Regs) =>
-  List.concat (List.map (fun v => match v with
-                | (Value a, s') => f a s'
-                | (Ex e, s') => [(Ex e, s')]
-                end) (m s)).
+  List.flat_map (fun v => match v with
+             | (Value a, s') => f a s'
+             | (Ex e, s') => [(Ex e, s')]
+             end) (m s).
 
 (*val seqS: forall 'regs 'b 'e. monadS 'regs unit 'e -> monadS 'regs 'b 'e -> monadS 'regs 'b 'e*)
 Definition seqS {Regs B E} (m : monadS Regs unit E) (n : monadS Regs B E) : monadS Regs B E :=
@@ -96,11 +96,11 @@ Definition throwS {Regs A E} (e : E) :monadS Regs A E :=
 (*val try_catchS : forall 'regs 'a 'e1 'e2. monadS 'regs 'a 'e1 -> ('e1 -> monadS 'regs 'a 'e2) ->  monadS 'regs 'a 'e2*)
 Definition try_catchS {Regs A E1 E2} (m : monadS Regs A E1) (h : E1 -> monadS Regs A E2) : monadS Regs A E2 :=
 fun s =>
-  List.concat (List.map (fun v => match v with
+  List.flat_map (fun v => match v with
                 | (Value a, s') => returnS a s'
                 | (Ex (Throw e), s') => h e s'
                 | (Ex (Failure msg), s') => [(Ex (Failure msg), s')]
-                end) (m s)).
+                end) (m s).
 
 (*val assert_expS : forall 'regs 'e. bool -> string -> monadS 'regs unit 'e*)
 Definition assert_expS {Regs E} (exp : bool) (msg : string) : monadS Regs unit E :=
diff --git a/lib/coq/Sail2_state_monad_lemmas.v b/lib/coq/Sail2_state_monad_lemmas.v
new file mode 100644
index 00000000..e2b98d79
--- /dev/null
+++ b/lib/coq/Sail2_state_monad_lemmas.v
@@ -0,0 +1,479 @@
+Require Import Sail2_state_monad.
+(*Require Import Sail2_values_lemmas.*)
+
+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 ->
+  (forall a s', List.In (Value a, s') (m2 s) -> f1 a s' = f2 a s') ->
+  bindS m1 f1 s = bindS m2 f2 s.
+intros.
+unfold bindS.
+rewrite H.
+rewrite !List.flat_map_concat_map.
+f_equal.
+apply List.map_ext_in.
+intros [[a|a] s'] H_in; auto.
+Qed.
+
+(*
+lemma bindS_cong[fundef_cong]:
+  assumes m: "m1 = m2"
+    and f: "\<And>s a s'. (Value a, s') \<in> (m2 s) \<Longrightarrow> f1 a s' = f2 a s'"
+  shows "bindS m1 f1 = bindS m2 f2"
+  using assms by (intro ext bindS_ext_cong; blast)
+*)
+
+Lemma bindS_returnS_left (*[simp]:*) {Regs A B E} {x : A} {f : A -> monadS Regs B E} {s} :
+ bindS (returnS x) f s = f x s.
+unfold returnS, bindS.
+simpl.
+auto using List.app_nil_r.
+Qed.
+
+Lemma bindS_returnS_right (*[simp]:*) {Regs A E} {m : monadS Regs A E} {s} :
+ bindS m returnS s = m s.
+unfold returnS, bindS.
+induction (m s) as [|[[a|a] s'] t]; auto;
+simpl;
+rewrite IHt;
+reflexivity.
+Qed.
+
+Lemma bindS_readS {Regs A E} {f} {m : A -> monadS Regs A E} {s} :
+  bindS (readS f) m s = m (f s) s.
+unfold readS, bindS.
+simpl.
+rewrite List.app_nil_r.
+reflexivity.
+Qed.
+
+Lemma bindS_updateS {Regs A E} {f : sequential_state Regs -> sequential_state Regs} {m : unit -> monadS Regs A E} {s} :
+  bindS (updateS f) m s = m tt (f s).
+unfold updateS, bindS.
+simpl.
+auto using List.app_nil_r.
+Qed.
+
+Lemma bindS_assertS_True (*[simp]:*) {Regs A E msg} {f : unit -> monadS Regs A E} {s} :
+  bindS (assert_expS true msg) f s = f tt s.
+unfold assert_expS, bindS.
+simpl.
+auto using List.app_nil_r.
+Qed.
+
+Lemma bindS_chooseS_returnS (*[simp]:*) {Regs A B E} {xs : list A} {f : A -> B} {s} :
+  bindS (Regs := Regs) (E := E) (chooseS xs) (fun x => returnS (f x)) s = chooseS (List.map f xs) s.
+unfold chooseS, bindS, returnS.
+induction xs; auto.
+simpl. rewrite IHxs.
+reflexivity.
+Qed.
+
+Lemma result_cases : forall (A E : Type) (P : result A E -> Prop),
+  (forall a, P (Value a)) ->
+  (forall e, P (Ex (Throw e))) ->
+  (forall msg, P (Ex (Failure msg))) ->
+  forall r, P r.
+intros.
+destruct r; auto.
+destruct e; auto.
+Qed.
+
+Lemma result_state_cases {A E S} {P : result A E * S -> Prop} :
+  (forall a s, P (Value a, s)) ->
+  (forall e s, P (Ex (Throw e), s)) ->
+  (forall msg s, P (Ex (Failure msg), s)) ->
+  forall rs, P rs.
+intros.
+destruct rs as [[a|[e|msg]] s]; auto.
+Qed.
+
+(* TODO: needs sets, not lists
+Lemma monadS_ext_eqI {Regs A E} {m m' : monadS Regs A E} s :
+  (forall a s', List.In (Value a, s') (m s) <-> List.In (Value a, s') (m' s)) ->
+  (forall e s', List.In (Ex (Throw e), s') (m s) <-> List.In (Ex (Throw e), s') (m' s)) ->
+  (forall msg s', List.In (Ex (Failure msg), s') (m s) <-> List.In (Ex (Failure msg), s') (m' s)) ->
+  m s = m' s.
+proof (intro set_eqI)
+  fix x
+  show "x \<in> m s \<longleftrightarrow> x \<in> m' s" using assms by (cases x rule: result_state_cases) auto
+qed
+
+lemma monadS_eqI:
+  fixes m m' :: "('regs, 'a, 'e) monadS"
+  assumes "\<And>s a s'. (Value a, s') \<in> m s \<longleftrightarrow> (Value a, s') \<in> m' s"
+    and "\<And>s e s'. (Ex (Throw e), s') \<in> m s \<longleftrightarrow> (Ex (Throw e), s') \<in> m' s"
+    and "\<And>s msg s'. (Ex (Failure msg), s') \<in> m s \<longleftrightarrow> (Ex (Failure msg), s') \<in> m' s"
+  shows "m = m'"
+  using assms by (intro ext monadS_ext_eqI)
+*)
+
+Lemma bindS_cases {Regs A B E} {m} {f : A -> monadS Regs B E} {r s s'} :
+  List.In (r, s') (bindS m f s) ->
+  (exists a a' s'', r = Value a /\ List.In (Value a', s'') (m s) /\ List.In (Value a, s') (f a' s'')) \/
+  (exists e, r = Ex e /\ List.In (Ex e, s') (m s)) \/
+  (exists e a s'', r = Ex e /\ List.In (Value a, s'') (m s) /\ List.In (Ex e, s') (f a s'')).
+unfold bindS.
+intro IN.
+apply List.in_flat_map in IN.
+destruct IN as [[r' s''] [INr' INr]].
+destruct r' as [a'|e'].
+* destruct r as [a|e].
+  + left. eauto 10.
+  + right; right. eauto 10.
+* right; left. simpl in INr. destruct INr as [|[]]. inversion H. subst. eauto 10.
+Qed.
+
+Lemma bindS_intro_Value {Regs A B E} {m} {f : A -> monadS Regs B E} {s a s' a' s''} :
+ List.In (Value a', s'') (m s) -> List.In (Value a, s') (f a' s'') -> List.In (Value a, s') (bindS m f s).
+intros; unfold bindS.
+apply List.in_flat_map.
+eauto.
+Qed.
+Lemma bindS_intro_Ex_left {Regs A B E} {m} {f : A -> monadS Regs B E} {s e s'} :
+  List.In (Ex e, s') (m s) -> List.In (Ex e, s') (bindS m f s).
+intros; unfold bindS.
+apply List.in_flat_map.
+exists (Ex e, s').
+auto with datatypes.
+Qed.
+Lemma bindS_intro_Ex_right {Regs A B E} {m} {f : A -> monadS Regs B E} {s e s' a s''} :
+  List.In (Ex e, s') (f a s'') -> List.In (Value a, s'') (m s) -> List.In (Ex e, s') (bindS m f s).
+intros; unfold bindS.
+apply List.in_flat_map.
+eauto.
+Qed.
+Hint Resolve bindS_intro_Value bindS_intro_Ex_left bindS_intro_Ex_right : bindS_intros.
+
+Lemma bindS_assoc (*[simp]:*) {Regs A B C E} {m} {f : A -> monadS Regs B E} {g : B -> monadS Regs C E} {s} :
+  bindS (bindS m f) g s = bindS m (fun x => bindS (f x) g) s.
+unfold bindS.
+induction (m s) as [ | [[a | e] t]].
+* reflexivity.
+* simpl. rewrite <- IHl.
+  rewrite !List.flat_map_concat_map.
+  rewrite List.map_app.
+  rewrite List.concat_app.
+  reflexivity.
+* simpl. rewrite IHl. reflexivity.
+Qed.
+
+Lemma bindS_failS (*[simp]:*) {Regs A B E} {msg} {f : A -> monadS Regs B E} :
+  bindS (failS msg) f = failS msg.
+reflexivity.
+Qed.
+Lemma bindS_throwS (*[simp]:*) {Regs A B E} {e} {f : A -> monadS Regs B E} :
+  bindS (throwS e) f = throwS e.
+reflexivity.
+Qed.
+(*declare seqS_def[simp]*)
+
+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) ->
+  exists s'' a', List.In (Value a', s'') (m s) /\ List.In (Value a, s') (f a' s'').
+intro H.
+apply bindS_cases in H.
+destruct H as [(a0 & a' & s'' & [= <-] & [*]) | [(e & [= ] & _) | (_ & _ & _ & [= ] & _)]].
+eauto.
+Qed.
+
+Lemma Ex_bindS_elim {Regs A B E} {e m s s'} {f : A -> monadS Regs B E} :
+  List.In (Ex e, s') (bindS m f s) ->
+  List.In (Ex e, s') (m s) \/
+  exists s'' a', List.In (Value a', s'') (m s) /\ List.In (Ex e, s') (f a' s'').
+intro H.
+apply bindS_cases in H.
+destruct H as [(? & ? & ? & [= ] & _) | [(? & [= <-] & X) | (? & ? & ? & [= <-] & X)]];
+eauto.
+Qed.
+
+Lemma try_catchS_returnS (*[simp]:*) {Regs A E1 E2} {a} {h : E1 -> monadS Regs A E2}:
+  try_catchS (returnS a) h = returnS a.
+reflexivity.
+Qed.
+Lemma try_catchS_failS (*[simp]:*) {Regs A E1 E2} {msg} {h : E1 -> monadS Regs A E2}:
+  try_catchS (failS msg) h = failS msg.
+reflexivity.
+Qed.
+Lemma try_catchS_throwS (*[simp]:*) {Regs A E1 E2} {e} {h : E1 -> monadS Regs A E2} {s}:
+  try_catchS (throwS e) h s = h e s.
+unfold try_catchS, throwS.
+simpl.
+auto using List.app_nil_r.
+Qed.
+
+Lemma try_catchS_cong (*[cong]:*) {Regs A E1 E2 m1 m2} {h1 h2 : E1 -> monadS Regs A E2} {s} :
+  (forall s, m1 s = m2 s) ->
+  (forall e s, h1 e s = h2 e s) ->
+  try_catchS m1 h1 s = try_catchS m2 h2 s.
+intros H1 H2.
+unfold try_catchS.
+rewrite H1.
+rewrite !List.flat_map_concat_map.
+f_equal.
+apply List.map_ext_in.
+intros [[a|[e|msg]] s'] H_in; auto.
+Qed.
+
+Lemma try_catchS_cases {Regs A E1 E2 m} {h : E1 -> monadS Regs A E2} {r s s'} :
+  List.In (r, s') (try_catchS m h s) ->
+  (exists a, r = Value a /\ List.In (Value a, s') (m s)) \/
+  (exists msg, r = Ex (Failure msg) /\ List.In (Ex (Failure msg), s') (m s)) \/
+  (exists e s'', List.In (Ex (Throw e), s'') (m s) /\ List.In (r, s') (h e s'')).
+unfold try_catchS.
+intro IN.
+apply List.in_flat_map in IN.
+destruct IN as [[r' s''] [INr' INr]].
+destruct r' as [a'|[e'|msg]].
+* left. simpl in INr. destruct INr as [[= <- <-] | []]. eauto 10.
+* simpl in INr. destruct INr as [[= <- <-] | []]. eauto 10.
+* eauto 10.
+Qed.
+
+Lemma try_catchS_intros {Regs A E1 E2} {m} {h : E1 -> monadS Regs A E2} :
+  (forall s a s', List.In (Value a, s') (m s) -> List.In (Value a, s') (try_catchS m h s)) /\
+  (forall s msg s', List.In (Ex (Failure msg), s') (m s) -> List.In (Ex (Failure msg), s') (try_catchS m h s)) /\
+  (forall s e s'' r s', List.In (Ex (Throw e), s'') (m s) -> List.In (r, s') (h e s'') -> List.In (r, s') (try_catchS m h s)).
+repeat split; unfold try_catchS; intros;
+apply List.in_flat_map.
+* eexists; split; [ apply H | ]. simpl. auto.
+* eexists; split; [ apply H | ]. simpl. auto.
+* eexists; split; [ apply H | ]. simpl. auto.
+Qed.
+
+Lemma no_Ex_basic_builtins (*[simp]:*) {Regs E} {s s' : sequential_state Regs} {e : ex E} :
+  (forall A (a:A), ~ List.In (Ex e, s') (returnS a s)) /\
+  (forall A (f : _ -> A), ~ List.In (Ex e, s') (readS f s)) /\
+  (forall f, ~ List.In (Ex e, s') (updateS f s)) /\
+  (forall A (xs : list A), ~ List.In (Ex e, s') (chooseS xs s)).
+repeat split; intros;
+unfold returnS, readS, updateS, chooseS; simpl;
+try intuition congruence.
+* intro H.
+  apply List.in_map_iff in H.
+  destruct H as [x [X _]].
+  congruence.
+Qed.
+
+Import List.ListNotations.
+Definition ignore_throw_aux {A E1 E2 S} (rs : result A E1 * S) : list (result A E2 * S) :=
+match rs with
+| (Value a, s') => [(Value a, s')]
+| (Ex (Throw e), s') => []
+| (Ex (Failure msg), s') => [(Ex (Failure msg), s')]
+end.
+Definition ignore_throw {A E1 E2 S} (m : S -> list (result A E1 * S)) s : list (result A E2 * S) :=
+ List.flat_map ignore_throw_aux (m s).
+
+Lemma ignore_throw_cong {A E1 E2 S} {m1 m2 : S -> list (result A E1 * S)} s :
+  (forall s, m1 s = m2 s) ->
+  ignore_throw (E2 := E2) m1 s = ignore_throw m2 s.
+intro H.
+unfold ignore_throw.
+rewrite H.
+reflexivity.
+Qed.
+
+Lemma ignore_throw_aux_member_simps (*[simp]:*) {A E1 E2 S} {s' : S} {ms} :
+  (forall a:A, List.In (Value a, s') (ignore_throw_aux (E1 := E1) (E2 := E2) ms) <-> ms = (Value a, s')) /\
+  (forall e, ~ List.In (Ex (E := E2) (Throw e), s') (ignore_throw_aux ms)) /\
+  (forall msg, List.In (Ex (E := E2) (Failure msg), s') (ignore_throw_aux ms) <-> ms = (Ex (Failure msg), s')).
+destruct ms as [[a' | [e' | msg']] s]; simpl;
+intuition congruence.
+Qed.
+
+Lemma ignore_throw_member_simps (*[simp]:*) {A E1 E2 S} {s s' : S} {m} :
+  (forall {a:A}, List.In (Value (E := E2) a, s') (ignore_throw m s) <-> List.In (Value (E := E1) a, s') (m s)) /\
+  (forall {a:A}, List.In (Value (E := E2) a, s') (ignore_throw m s) <-> List.In (Value a, s') (m s)) /\
+  (forall e, ~ List.In (Ex (E := E2) (Throw e), s') (ignore_throw m s)) /\
+  (forall {msg}, List.In (Ex (E := E2) (Failure msg), s') (ignore_throw m s) <-> List.In (Ex (Failure msg), s') (m s)).
+unfold ignore_throw.
+repeat apply conj; intros; try apply conj;
+rewrite ?List.in_flat_map;
+solve
+[ intros [x [H1 H2]]; apply ignore_throw_aux_member_simps in H2; congruence
+| intro H; eexists; split; [ apply H | apply ignore_throw_aux_member_simps; reflexivity] ].
+Qed.
+
+Lemma ignore_throw_cases {A E S} {m : S -> list (result A E * S)} {r s s'} :
+  ignore_throw m s = m s ->
+  List.In (r, s') (m s) ->
+  (exists a, r = Value a) \/
+  (exists msg, r = Ex (Failure msg)).
+destruct r as [a | [e | msg]]; eauto.
+* intros H1 H2. rewrite <- H1 in H2.
+  apply ignore_throw_member_simps in H2.
+  destruct H2.
+Qed.
+
+(* *** *)
+Lemma flat_map_app {A B} {f : A -> list B} {l1 l2} :
+  List.flat_map f (l1 ++ l2) = (List.flat_map f l1 ++ List.flat_map f l2)%list.
+rewrite !List.flat_map_concat_map.
+rewrite List.map_app, List.concat_app.
+reflexivity.
+Qed.
+
+Lemma ignore_throw_bindS (*[simp]:*) Regs A B E E2 {m} {f : A -> monadS Regs B E} {s} :
+  ignore_throw (E2 := E2) (bindS m f) s = bindS (ignore_throw m) (fun s => ignore_throw (f s)) s.
+unfold bindS, ignore_throw.
+induction (m s) as [ | [[a | [e | msg]] t]].
+* reflexivity.
+* simpl. rewrite <- IHl. rewrite flat_map_app. reflexivity.
+* simpl. rewrite <- IHl. reflexivity.
+* simpl. apply IHl.
+Qed.
+Hint Rewrite ignore_throw_bindS : ignore_throw.
+
+Lemma try_catchS_bindS_no_throw {Regs A B E1 E2} {m1 : monadS Regs A E1} {m2 : monadS Regs A E2} {f : A -> monadS Regs B _} {s h} :
+  (forall s, ignore_throw m1 s = m1 s) ->
+  (forall s, ignore_throw m1 s = m2 s) ->
+  try_catchS (bindS m1 f) h s = bindS m2 (fun a => try_catchS (f a) h) s.
+intros Ignore1 Ignore2.
+transitivity ((ignore_throw m1 >>$= (fun a => try_catchS (f a) h)) s).
+* unfold bindS, try_catchS, ignore_throw.
+  specialize (Ignore1 s). revert Ignore1. unfold ignore_throw.
+  induction (m1 s) as [ | [[a | [e | msg]] t]]; auto.
+  + intro Ig. simpl. rewrite flat_map_app. rewrite IHl. auto. injection Ig. auto.
+  + intro Ig. simpl. rewrite IHl. reflexivity. injection Ig. auto.
+  + intro Ig. exfalso. clear -Ig.
+    assert (List.In (Ex (Throw msg), t) (List.flat_map ignore_throw_aux l)).
+    simpl in Ig. rewrite Ig. simpl. auto.
+    apply List.in_flat_map in H.
+    destruct H as [x [H1 H2]].
+    apply ignore_throw_aux_member_simps in H2.
+    assumption.
+* apply bindS_ext_cong; auto.
+Qed.
+
+Lemma concat_map_singleton {A B} {f : A -> B} {a : list A} :
+  List.concat (List.map (fun x => [f x]%list) a) = List.map f a.
+induction a; simpl; try rewrite IHa; auto with datatypes.
+Qed.
+
+(*lemma no_throw_basic_builtins[simp]:*)
+Lemma no_throw_basic_builtins_1 Regs A E E2 {a : A} :
+  ignore_throw (E1 := E2) (returnS a) = @returnS Regs A E a.
+reflexivity. Qed.
+Lemma no_throw_basic_builtins_2 Regs A E E2 {f : sequential_state Regs -> A} :
+  ignore_throw (E1 := E) (E2 := E2) (readS f) = readS f.
+reflexivity. Qed.
+Lemma no_throw_basic_builtins_3 Regs E E2 {f : sequential_state Regs -> sequential_state Regs} :
+  ignore_throw (E1 := E) (E2 := E2) (updateS f) = updateS f.
+reflexivity. Qed.
+Lemma no_throw_basic_builtins_4 Regs A E1 E2 {xs : list A} s :
+  ignore_throw (E1 := E1) (chooseS xs) s = @chooseS Regs A E2 xs s.
+unfold ignore_throw, chooseS.
+rewrite List.flat_map_concat_map, List.map_map. simpl.
+rewrite concat_map_singleton.
+reflexivity.
+Qed.
+Lemma no_throw_basic_builtins_5 Regs E1 E2 :
+  ignore_throw (E1 := E1) (choose_boolS tt) = @choose_boolS Regs E2 tt.
+reflexivity. Qed.
+Lemma no_throw_basic_builtins_6 Regs A E1 E2 msg :
+  ignore_throw (E1 := E1) (failS msg) = @failS Regs A E2 msg.
+reflexivity. Qed.
+Lemma no_throw_basic_builtins_7 Regs A E1 E2 msg x :
+  ignore_throw (E1 := E1) (maybe_failS msg x) = @maybe_failS Regs A E2 msg x. 
+destruct x; reflexivity. Qed.
+
+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.
+
+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 =
+    match c s with None => ignore_throw n s | Some b => ignore_throw (f b) s end.
+destruct (c s); auto.
+Qed.
+Lemma ignore_throw_option_case_distrib_2 Regs B C E1 E2 (c : option B) (n : monadS Regs C E1) (f : B -> monadS Regs C E1) :
+  ignore_throw (E2 := E2) (match c with None => n | Some b => f b end) =
+    match c with None => ignore_throw n | Some b => ignore_throw (f b) end.
+destruct c; auto.
+Qed.
+
+Lemma ignore_throw_let_distrib Regs A B E1 E2 (y : A) (f : A -> monadS Regs B E1) :
+  ignore_throw (E2 := E2) (let x := y in f x) = (let x := y in ignore_throw (f x)).
+reflexivity.
+Qed.
+
+Lemma no_throw_mem_builtins_1 Regs E1 E2 rk a sz s :
+  ignore_throw (E2 := E2) (@read_memt_bytesS Regs E1 rk a sz) s = read_memt_bytesS rk a sz s.
+unfold read_memt_bytesS. autorewrite with ignore_throw.
+apply bindS_ext_cong; auto. intros.  autorewrite with ignore_throw. reflexivity.
+Qed.
+Hint Rewrite no_throw_mem_builtins_1 : ignore_throw.
+Lemma no_throw_mem_builtins_2 Regs E1 E2 rk a sz s :
+  ignore_throw (E2 := E2) (@read_mem_bytesS Regs E1 rk a sz) s = read_mem_bytesS rk a sz s.
+unfold read_mem_bytesS. autorewrite with ignore_throw.
+apply bindS_ext_cong; intros; autorewrite with ignore_throw; auto.
+destruct a0; reflexivity.
+Qed.
+Hint Rewrite no_throw_mem_builtins_2 : ignore_throw.
+Lemma no_throw_mem_builtins_3 Regs A E1 E2 a s :
+  ignore_throw (E2 := E2) (@read_tagS Regs A E1 a) s = read_tagS a s.
+reflexivity. Qed.
+Hint Rewrite no_throw_mem_builtins_3 : ignore_throw.
+Lemma no_throw_mem_builtins_4 Regs A V E1 E2 rk a sz s H :
+  ignore_throw (E2 := E2) (@read_memtS Regs E1 A V rk a sz H) s = read_memtS rk a sz s.
+unfold read_memtS. autorewrite with ignore_throw.
+apply bindS_ext_cong; intros; autorewrite with ignore_throw.
+reflexivity. destruct a0; simpl. autorewrite with ignore_throw.
+reflexivity.
+Qed.
+Hint Rewrite no_throw_mem_builtins_4 : ignore_throw.
+Lemma no_throw_mem_builtins_5 Regs A V E1 E2 rk a sz s H :
+  ignore_throw (E2 := E2) (@read_memS Regs E1 A V rk a sz H) s = read_memS rk a sz s.
+unfold read_memS. autorewrite with ignore_throw.
+apply bindS_ext_cong; intros; autorewrite with ignore_throw; auto.
+destruct a0; auto.
+Qed.
+Hint Rewrite no_throw_mem_builtins_5 : ignore_throw.
+Lemma no_throw_mem_builtins_6 Regs E1 E2 wk addr sz v t s :
+  ignore_throw (E2 := E2) (@write_memt_bytesS Regs E1 wk addr sz v t) s = write_memt_bytesS wk addr sz v t s.
+unfold write_memt_bytesS. unfold seqS. autorewrite with ignore_throw.
+reflexivity.
+Qed.
+Hint Rewrite no_throw_mem_builtins_6 : ignore_throw.
+Lemma no_throw_mem_builtins_7 Regs E1 E2 wk addr sz v s :
+  ignore_throw (E2 := E2) (@write_mem_bytesS Regs E1 wk addr sz v) s = write_mem_bytesS wk addr sz v s.
+unfold write_mem_bytesS. autorewrite with ignore_throw. reflexivity.
+Qed.
+Hint Rewrite no_throw_mem_builtins_7 : ignore_throw.
+Lemma no_throw_mem_builtins_8 Regs E1 E2 A B wk addr sz v t s :
+  ignore_throw (E2 := E2) (@write_memtS Regs E1 A B wk addr sz v t) s = write_memtS wk addr sz v t s.
+unfold write_memtS. rewrite ignore_throw_option_case_distrib_2.
+destruct (Sail2_values.mem_bytes_of_bits v); autorewrite with ignore_throw; auto.
+Qed.
+Hint Rewrite no_throw_mem_builtins_8 : ignore_throw.
+Lemma no_throw_mem_builtins_9 Regs E1 E2 A B wk addr sz v s :
+  ignore_throw (E2 := E2) (@write_memS Regs E1 A B wk addr sz v) s = write_memS wk addr sz v s.
+unfold write_memS. autorewrite with ignore_throw; auto.
+Qed.
+Hint Rewrite no_throw_mem_builtins_9 : ignore_throw.
+Lemma no_throw_mem_builtins_10 Regs E1 E2 s :
+  ignore_throw (E2 := E2) (@excl_resultS Regs E1 tt) s = excl_resultS tt s.
+reflexivity. Qed.
+Hint Rewrite no_throw_mem_builtins_10 : ignore_throw.
+Lemma no_throw_mem_builtins_11 Regs E1 E2 s :
+  ignore_throw (E2 := E2) (@undefined_boolS Regs E1 tt) s = undefined_boolS tt s.
+reflexivity. Qed.
+Hint Rewrite no_throw_mem_builtins_11 : ignore_throw.
+
+Lemma no_throw_read_regvalS Regs RV E1 E2 r reg_name s :
+  ignore_throw (E2 := E2) (@read_regvalS Regs RV E1 r reg_name) s = read_regvalS r reg_name s.
+destruct r; simpl. autorewrite with ignore_throw.
+apply bindS_ext_cong; intros; auto. rewrite ignore_throw_option_case_distrib_2.
+autorewrite with ignore_throw. reflexivity.
+Qed.
+Hint Rewrite no_throw_read_regvalS : ignore_throw.
+
+Lemma no_throw_write_regvalS Regs RV E1 E2 r reg_name v s :
+  ignore_throw (E2 := E2) (@write_regvalS Regs RV E1 r reg_name v) s = write_regvalS r reg_name v s.
+destruct r; simpl. autorewrite with ignore_throw.
+apply bindS_ext_cong; intros; auto. rewrite ignore_throw_option_case_distrib_2.
+autorewrite with ignore_throw. reflexivity.
+Qed.
+Hint Rewrite no_throw_write_regvalS : ignore_throw.