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

4 files changed, 28 insertions, 2 deletions

diff --git a/aarch64/aarch64_extras.v b/aarch64/aarch64_extras.v
index 29e7198c..0bc2c96f 100644
--- a/aarch64/aarch64_extras.v
+++ b/aarch64/aarch64_extras.v
@@ -6,7 +6,6 @@ Require Import Sail2_prompt.
 Require Import Sail2_real.
 
 Axiom slice : forall {m} (_ : mword m) (_ : Z) (n : Z) `{ArithFact (m >= 0)} `{ArithFact (n >= 0)}, mword n.
-Axiom set_slice : forall (n : Z) (m : Z), mword n -> Z -> mword m -> mword n.
 Definition length {n} (x : mword n) := length_mword x.
 Hint Unfold length : sail.
 
@@ -142,6 +141,12 @@ rewrite Z.quot_mul; auto with zarith.
 Qed.
 Hint Resolve mul_quot_8_helper : sail.
 
+Lemma mul_quot_8_helper2 : forall x y, 8 * x = y -> 8 * x = 8 * (Z.quot y 8).
+intros. subst.
+apply mul_quot_8_helper.
+Qed.
+Hint Resolve mul_quot_8_helper2 : sail.
+
 (* For aarch64_vector_arithmetic_binary_uniform_mul_int_dotp *)
 Lemma quot4_ge {esize x} : 4 <= esize -> x = Z.quot esize 4 -> x >= 0.
 intros.
@@ -171,3 +176,11 @@ omega.
 Qed.
 Hint Resolve quot4_gt : sail.
 
+Lemma vector_single_nowb_lemma {x y} : 0 <= x -> 0 <= y ->
+  y * x >= 0.
+intros.
+apply Z.le_ge.
+apply Z.mul_nonneg_nonneg; auto.
+Qed.
+Hint Resolve vector_single_nowb_lemma : sail.
+
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 *)