Merge branch 'mono-tweaks' into sail2

7 files changed, 65 insertions, 15 deletions

diff --git a/lib/arith.sail b/lib/arith.sail
index 58f25bbc..d57fd559 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -56,19 +56,21 @@ A common idiom in asl is to take two bits of an opcode and convert in into a var
 let elsize = shl_int(8, UInt(size))
 ```
 THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}`
+
+Similarly, we define shifts of 32 and 1 (i.e., powers of two).
 */
 val _shl8 = {c: "shl_mach_int", coq: "shl_int_8", _: "shl_int"} :
   forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> {'m, 'm in {8, 16, 32, 64}. int('m)}
 
-/*!
-Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}`
-*/
 val _shl32 = {c: "shl_mach_int", coq: "shl_int_32", _: "shl_int"} :
   forall 'n, 'n in {0, 1}. (int(32), int('n)) -> {'m, 'm in {32, 64}. int('m)}
 
+val _shl1 = {c: "shl_mach_int", coq: "shl_int_32", _: "shl_int"} :
+  forall 'n, 0 <= 'n <= 3. (int(1), int('n)) -> {'m, 'm in {1, 2, 4, 8}. int('m)}
+
 val _shl_int = "shl_int" : (int, int) -> int
 
-overload shl_int = {_shl8, _shl32, _shl_int}
+overload shl_int = {_shl1, _shl8, _shl32, _shl_int}
 
 val _shr32 = {c: "shr_mach_int", coq: "shr_int_32", _: "shr_int"} : forall 'n, 0 <= 'n <= 31. (int('n), int(1)) -> {'m, 0 <= 'm <= 15. int('m)}
 
diff --git a/lib/coq/Makefile b/lib/coq/Makefile
index d16191cb..806b0ff0 100644
--- a/lib/coq/Makefile
+++ b/lib/coq/Makefile
@@ -1,10 +1,10 @@
-BBV_DIR?=../../../bbv
+BBV_DIR?=../../../bbv/src/bbv
 
 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_values_lemmas.v Sail2_state_monad_lemmas.v Sail2_state_lemmas.v Hoare.v
 SRC=$(CORESRC) $(PROOFSRC)
 
-COQ_LIBS = -R . Sail -R "$(BBV_DIR)/theories" bbv
+COQ_LIBS = -R . Sail -R "$(BBV_DIR)" bbv
 
 TARGETS=$(SRC:.v=.vo)
 
diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy
index 98b7d077..848cd042 100644
--- a/lib/isabelle/Hoare.thy
+++ b/lib/isabelle/Hoare.thy
@@ -96,6 +96,14 @@ lemma PrePost_readS[intro, PrePost_atomI]: "PrePost (\<lambda>s. P (Value (f s))
 lemma PrePost_updateS[intro, PrePost_atomI]: "PrePost (\<lambda>s. P (Value ()) (f s)) (updateS f) P"
   unfolding PrePost_def updateS_def returnS_def by auto
 
+lemma PrePost_read_regS[intro, PrePost_atomI]:
+  "PrePost (\<lambda>s. P (Value (read_from reg (regstate s))) s) (read_regS reg) P"
+  unfolding read_regS_def by (rule PrePost_readS)
+
+lemma PrePost_write_regS[intro, PrePost_atomI]:
+  "PrePost (\<lambda>s. P (Value ()) (s\<lparr>regstate := write_to reg v (regstate s)\<rparr>)) (write_regS reg v) P"
+  unfolding write_regS_def by (rule PrePost_updateS)
+
 lemma PrePost_if:
   assumes "b \<Longrightarrow> PrePost P f Q" and "\<not>b \<Longrightarrow> PrePost P g Q"
   shows "PrePost P (if b then f else g) Q"
@@ -311,6 +319,14 @@ lemma PrePostE_readS[PrePostE_atomI, intro]: "PrePostE (\<lambda>s. Q (f s) s) (
 lemma PrePostE_updateS[PrePostE_atomI, intro]: "PrePostE (\<lambda>s. Q () (f s)) (updateS f) Q E"
   unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre)
 
+lemma PrePostE_read_regS[PrePostE_atomI, intro]:
+  "PrePostE (\<lambda>s. Q (read_from reg (regstate s)) s) (read_regS reg) Q E"
+  unfolding read_regS_def by (rule PrePostE_readS)
+
+lemma PrePostE_write_regS[PrePostE_atomI, intro]:
+  "PrePostE (\<lambda>s. Q () (s\<lparr>regstate := write_to reg v (regstate s)\<rparr>)) (write_regS reg v) Q E"
+  unfolding write_regS_def by (rule PrePostE_updateS)
+
 lemma PrePostE_if_branch[PrePostE_compositeI]:
   assumes "b \<Longrightarrow> PrePostE Pf f Q E" and "\<not>b \<Longrightarrow> PrePostE Pg g Q E"
   shows "PrePostE (if b then Pf else Pg) (if b then f else g) Q E"
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index 8be5cc6b..8fbcf093 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -122,22 +122,22 @@ lemma liftState_write_mem[liftState_simp]:
   by (auto simp: write_mem_def write_memS_def write_memtS_def write_mem_bytesS_def liftState_simp
            split: option.splits)
 
-lemma liftState_read_reg_readS:
+lemma liftState_read_reg:
   assumes "\<And>s. Option.bind (get_regval' (name reg) s) (of_regval reg) = Some (read_from reg s)"
-  shows "liftState (get_regval', set_regval') (read_reg reg) = readS (read_from reg \<circ> regstate)"
+  shows "liftState (get_regval', set_regval') (read_reg reg) = read_regS reg"
 proof
   fix s :: "'a sequential_state"
   obtain rv v where "get_regval' (name reg) (regstate s) = Some rv"
     and "of_regval reg rv \<equiv> Some v" and "read_from reg (regstate s) = v"
     using assms unfolding bind_eq_Some_conv by blast
-  then show "liftState (get_regval', set_regval') (read_reg reg) s = readS (read_from reg \<circ> regstate) s"
+  then show "liftState (get_regval', set_regval') (read_reg reg) s = read_regS reg s"
     by (auto simp: read_reg_def bindS_def returnS_def read_regS_def readS_def)
 qed
 
-lemma liftState_write_reg_updateS:
+lemma liftState_write_reg:
   assumes "\<And>s. set_regval' (name reg) (regval_of reg v) s = Some (write_to reg v s)"
-  shows "liftState (get_regval', set_regval') (write_reg reg v) = updateS (regstate_update (write_to reg v))"
-  using assms by (auto simp: write_reg_def updateS_def returnS_def bindS_readS)
+  shows "liftState (get_regval', set_regval') (write_reg reg v) = write_regS reg v"
+  using assms by (auto simp: write_reg_def updateS_def returnS_def bindS_readS write_regS_def)
 
 lemma liftState_iter_aux[liftState_simp]:
   shows "liftState r (iter_aux i f xs) = iterS_aux i (\<lambda>i x. liftState r (f i x)) xs"
diff --git a/lib/mono_rewrites.sail b/lib/mono_rewrites.sail
index 81d42663..0702b374 100644
--- a/lib/mono_rewrites.sail
+++ b/lib/mono_rewrites.sail
@@ -66,6 +66,12 @@ function slice_zeros_concat (xs, i, l, l') = {
   sail_shiftleft(extzv(l + l', xs), l')
 }
 
+val subrange_zeros_concat : forall 'n 'hi 'lo 'q, 'n >= 0 & 'hi - 'lo + 1 + 'q >= 0.
+  (bits('n), atom('hi), atom('lo), atom('q)) -> bits('hi - 'lo + 1 + 'q) effect pure
+
+function subrange_zeros_concat (xs, hi, lo, l') =
+  slice_zeros_concat(xs, lo, hi - lo + 1, l')
+
 /* Assumes initial vectors are of equal size */
 
 val subrange_subrange_eq : forall 'n, 'n >= 0.
@@ -103,13 +109,19 @@ function place_slice(m,xs,i,l,shift) = {
 }
 
 val set_slice_zeros : forall 'n, 'n >= 0.
-  (atom('n), bits('n), int, int) -> bits('n) effect pure
+  (implicit('n), bits('n), int, int) -> bits('n) effect pure
 
 function set_slice_zeros(n, xs, i, l) = {
   let ys : bits('n) = slice_mask(n, i, l) in
   xs & not_vec(ys)
 }
 
+val set_subrange_zeros : forall 'n, 'n >= 0.
+  (implicit('n), bits('n), int, int) -> bits('n) effect pure
+
+function set_subrange_zeros(n, xs, hi, lo) =
+  set_slice_zeros(n, xs, lo, hi - lo + 1)
+
 val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
   (implicit('m), bits('n), int, int) -> bits('m) effect pure
 
@@ -118,6 +130,11 @@ function zext_slice(m,xs,i,l) = {
   extzv(m, xs)
 }
 
+val zext_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
+  (implicit('m), bits('n), int, int) -> bits('m) effect pure
+
+function zext_subrange(m, xs, i, j) = zext_slice(m, xs, j, i - j + 1)
+
 val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
   (implicit('m), bits('n), int, int) -> bits('m) effect pure
 
@@ -126,6 +143,11 @@ function sext_slice(m,xs,i,l) = {
   extsv(m, xs)
 }
 
+val sext_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
+  (implicit('m), bits('n), int, int) -> bits('m) effect pure
+
+function sext_subrange(m, xs, i, j) = sext_slice(m, xs, j, i - j + 1)
+
 val place_slice_signed : forall 'n 'm, 'n >= 0 & 'm >= 0.
   (implicit('m), bits('n), int, int, int) -> bits('m) effect pure
 
@@ -202,4 +224,13 @@ function vector_update_subrange_from_subrange(n,v1,s1,e1,v2,s2,e2) = {
   xs | ys
 }
 
+val vector_update_subrange_from_integer_subrange : forall 'n1 's1 'e1 's2 'e2,
+    0 <= 'e1 <= 's1 < 'n1 & 0 <= 'e2 <= 's2 & 's1 - 'e1 == 's2 - 'e2.
+    (implicit('n1), bits('n1), int('s1), int('e1), int, int('s2), int('e2)) -> bits('n1)
+
+function vector_update_subrange_from_integer_subrange(n1, v1, s1, e1, i, s2, e2) = {
+  let v2 : bits('n1) = get_slice_int(n1, i, e2) in
+  vector_update_subrange_from_subrange(n1, v1, s1, e1, v2, s2 - e2, 0)
+}
+
 $endif
diff --git a/lib/smt.sail b/lib/smt.sail
index 93fe0827..2e72e791 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -23,7 +23,7 @@ val emod_int = {
 val abs_int_atom = {
   ocaml: "abs_int",
   interpreter: "abs_int",
-  lem: "abs_int",
+  lem: "integerAbs",
   c: "abs_int",
   coq: "abs_with_eq"
 } : forall 'n. int('n) -> int(abs('n))
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 2a9e96f0..32443560 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -146,6 +146,7 @@ overload operator + = {add_bits, add_bits_int}
 
 val sub_bits = {
   ocaml: "sub_vec",
+  interpreter: "sub_vec",
   lem: "sub_vec",
   c: "sub_bits",
   coq: "sub_vec"
@@ -230,7 +231,7 @@ val get_slice_int = "get_slice_int" : forall 'w. (int('w), int, int) -> bits('w)
 val set_slice_int = "set_slice_int" : forall 'w. (int('w), int, int, bits('w)) -> int
 
 val set_slice_bits = "set_slice" : forall 'n 'm.
-  (int('n), int('m), bits('n), int, bits('m)) -> bits('n)
+  (implicit('n), int('m), bits('n), int, bits('m)) -> bits('n)
 
 /*!
 converts a bit vector of length $n$ to an integer in the range $0$ to $2^n - 1$.