diff options
| -rw-r--r-- | aarch64/aarch64_extras.v | 15 | ||||
| -rw-r--r-- | lib/coq/Sail2_operators_mwords.v | 12 | ||||
| -rw-r--r-- | lib/coq/Sail2_real.v | 1 | ||||
| -rw-r--r-- | lib/coq/Sail2_values.v | 2 |
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 *) |