Merge branch 'sail2' of github.com:rems-project/sail into sail2

2 files changed, 28 insertions, 15 deletions

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 79bf87eb..1c2a1b26 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -101,14 +101,26 @@ match b with
   | BU => Fail "bool_of_bitU"
 end.
 
-(*val bool_of_bitU_oracle : forall 'rv 'e. bitU -> monad 'rv bool 'e*)
-Definition bool_of_bitU_oracle {rv E} (b : bitU) : monad rv bool E :=
+Definition bool_of_bitU_nondet {rv E} (b : bitU) : monad rv bool E :=
 match b with
   | B0 => returnm false
   | B1 => returnm true
-  | BU => undefined_bool tt
+  | BU => choose_bool "bool_of_bitU"
 end.
 
+Definition bools_of_bits_nondet {rv E} (bits : list bitU) : monad rv (list bool) E :=
+  foreachM bits []
+    (fun b bools =>
+      bool_of_bitU_nondet b >>= fun b => 
+      returnm (bools ++ [b])).
+
+Definition of_bits_nondet {rv A E} `{Bitvector A} (bits : list bitU) : monad rv A E :=
+  bools_of_bits_nondet bits >>= fun bs =>
+  returnm (of_bools bs).
+
+Definition of_bits_fail {rv A E} `{Bitvector A} (bits : list bitU) : monad rv A E :=
+  maybe_fail "of_bits" (of_bits bits).
+
 (* For termination of recursive functions.  We don't name assertions, so use
    the type class mechanism to find it. *)
 Definition _limit_reduces {_limit} (_acc:Acc (Zwf 0) _limit) `{ArithFact (_limit >= 0)} : Acc (Zwf 0) (_limit - 1).
diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v
index c07016dc..a26b65d7 100644
--- a/lib/coq/Sail2_state_lemmas.v
+++ b/lib/coq/Sail2_state_lemmas.v
@@ -198,12 +198,13 @@ 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)
+
+Lemma liftState_bool_of_bitU_nondet Regs Regval E r b :
+  liftState (Regs := Regs) r (@bool_of_bitU_nondet Regval E b) = bool_of_bitU_nondetS b.
+destruct b; simpl; try reflexivity.
+Qed.
 Hint Rewrite liftState_bool_of_bitU_nondet : liftState.
-*)
+
 Lemma liftState_read_memt Regs Regval A B E H rk a sz r :
   liftState (Regs := Regs) r (@read_memt Regval A B E H rk a sz) === read_memtS rk a sz.
 unfold read_memt, read_memt_bytes, read_memtS, maybe_failS. simpl.
@@ -356,13 +357,13 @@ 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_bools_of_bits_nondet Regs Regval E r bs :
+  liftState (Regs := Regs) r (@bools_of_bits_nondet Regval E bs) === bools_of_bits_nondetS bs.
+unfold bools_of_bits_nondet, bools_of_bits_nondetS.
+rewrite_liftState.
+reflexivity.
+Qed.
+Hint Rewrite liftState_bools_of_bits_nondet : liftState.
 
 Lemma liftState_internal_pick Regs Regval A E r (xs : list A) :
   liftState (Regs := Regs) (Regval := Regval) (E := E) r (internal_pick xs) === internal_pickS xs.