2 files changed, 100 insertions, 1 deletions
diff --git a/lib/coq/Sail2_state.v b/lib/coq/Sail2_state.v
index 6e242caf..bd18783f 100644
--- a/lib/coq/Sail2_state.v
+++ b/lib/coq/Sail2_state.v
@@ -121,6 +121,31 @@ 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.
diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v
index cb491669..563a17a6 100644
--- a/lib/coq/Sail2_state_lemmas.v
+++ b/lib/coq/Sail2_state_lemmas.v
@@ -474,8 +474,46 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState
     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'"
@@ -512,7 +550,43 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState
       then show ?case using k until IH by (auto simp: comp_def liftState_simp)
     qed auto
   qed auto
-qed
+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>