Coq: more fixes for AArch64

- implement set_slice and set_slice_int
- lemmas for more constraints
- make real sqrt visible
- unfolding list membership needs andb and orb to be handled first

3 files changed, 14 insertions, 1 deletions

diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 5f9c15f4..497b4a46 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -459,3 +459,15 @@ Qed.
 Definition reverse_endianness {n} (bits : mword n) := with_word (P := id) reverse_endianness_word bits.
 
 Definition get_slice_int {a} `{ArithFact (a >= 0)} : Z -> Z -> Z -> mword a := get_slice_int_bv.
+
+Definition set_slice n m (v : mword n) x (w : mword m) : mword n :=
+  update_subrange_vec_dec v (x + m - 1) x v.
+
+Definition set_slice_int len n lo (v : mword len) : Z :=
+  let hi := lo + len - 1 in
+  (* We don't currently have a constraint on lo in the sail prelude, so let's
+     avoid one here. *)
+  if sumbool_of_bool (Z.gtb hi 0) then
+    let bs : mword (hi + 1) := mword_of_int n in
+    (int_of_mword true (update_subrange_vec_dec bs hi lo v))
+  else n.
diff --git a/lib/coq/Sail2_real.v b/lib/coq/Sail2_real.v
index 23070935..e4e4316e 100644
--- a/lib/coq/Sail2_real.v
+++ b/lib/coq/Sail2_real.v
@@ -17,6 +17,7 @@ Definition lt_real (x y : R) : bool := if Rlt_dec x y then true else false.
 (* Export select definitions from outside of Rbase *)
 Definition powerRZ := powerRZ.
 Definition Rabs := Rabs.
+Definition sqrt := sqrt.
 
 (* Use flocq definitions, but without making the whole library a dependency. *)
 Definition Zfloor (x : R) := (up x - 1)%Z.
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index a91b2299..83fe1dc7 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1110,8 +1110,8 @@ Ltac prepare_for_solver :=
  extract_properties;
  repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end;
  unwrap_ArithFacts;
- unfold_In;
  unbool_comparisons;
+ unfold_In; (* after unbool_comparisons to deal with && and || *)
  reduce_list_lengths;
  reduce_pow;
  (* omega doesn't cope well with extra "True"s in the goal *)