Merge branch 'sail2' into union_barrier

1 files changed, 742 insertions, 0 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.