4 files changed, 64 insertions, 4 deletions
diff --git a/lib/coq/Sail2_instr_kinds.v b/lib/coq/Sail2_instr_kinds.v
index eadc567a..c6fb866b 100644
--- a/lib/coq/Sail2_instr_kinds.v
+++ b/lib/coq/Sail2_instr_kinds.v
@@ -157,6 +157,7 @@ Inductive barrier_kind :=
   | Barrier_RISCV_rw_r
   | Barrier_RISCV_r_w
   | Barrier_RISCV_w_r
+  | Barrier_RISCV_tso
   | Barrier_RISCV_i
   (* X86 *)
   | Barrier_x86_MFENCE.
@@ -182,6 +183,11 @@ instance (Show barrier_kind)
     | Barrier_RISCV_r_r   -> "Barrier_RISCV_r_r"
     | Barrier_RISCV_rw_w  -> "Barrier_RISCV_rw_w"
     | Barrier_RISCV_w_w   -> "Barrier_RISCV_w_w"
+    | Barrier_RISCV_w_rw  -> "Barrier_RISCV_w_rw"
+    | Barrier_RISCV_rw_r  -> "Barrier_RISCV_rw_r"
+    | Barrier_RISCV_r_w   -> "Barrier_RISCV_r_w"
+    | Barrier_RISCV_w_r   -> "Barrier_RISCV_w_r"
+    | Barrier_RISCV_tso   -> "Barrier_RISCV_tso"
     | Barrier_RISCV_i     -> "Barrier_RISCV_i"
     | Barrier_x86_MFENCE  -> "Barrier_x86_MFENCE"
   end
@@ -295,8 +301,13 @@ instance (EnumerationType barrier_kind)
     | Barrier_RISCV_r_r -> 15
     | Barrier_RISCV_rw_w -> 16
     | Barrier_RISCV_w_w -> 17
-    | Barrier_RISCV_i -> 18
-    | Barrier_x86_MFENCE -> 19
+    | Barrier_RISCV_w_rw -> 18
+    | Barrier_RISCV_rw_r -> 19
+    | Barrier_RISCV_r_w -> 20
+    | Barrier_RISCV_w_r -> 21
+    | Barrier_RISCV_tso -> 22
+    | Barrier_RISCV_i -> 23
+    | Barrier_x86_MFENCE -> 24
   end
 end
 *)
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index e37e9d26..7e4abe29 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -172,16 +172,32 @@ Definition zero_extend {a} (v : mword a) (n : Z) `{ArithFact (n >= a)} : mword n
 
 Definition sign_extend {a} (v : mword a) (n : Z) `{ArithFact (n >= a)} : mword n := exts_vec n v.
 
+Definition zeros (n : Z) `{ArithFact (n >= 0)} : mword n.
+refine (cast_to_mword (Word.wzero (Z.to_nat n)) _).
+unwrap_ArithFacts.
+apply Z2Nat.id.
+auto with zarith.
+Defined.
+
 Lemma truncate_eq {m n} : m >= 0 -> m <= n -> (Z.to_nat n = Z.to_nat m + (Z.to_nat n - Z.to_nat m))%nat.
 intros.
 assert ((Z.to_nat m <= Z.to_nat n)%nat).
 { apply Z2Nat.inj_le; omega. }
 omega.
 Qed.
+Lemma truncateLSB_eq {m n} : m >= 0 -> m <= n -> (Z.to_nat n = (Z.to_nat n - Z.to_nat m) + Z.to_nat m)%nat.
+intros.
+assert ((Z.to_nat m <= Z.to_nat n)%nat).
+{ apply Z2Nat.inj_le; omega. }
+omega.
+Qed.
 
 Definition vector_truncate {n} (v : mword n) (m : Z) `{ArithFact (m >= 0)} `{ArithFact (m <= n)} : mword m :=
   cast_to_mword (Word.split1 _ _ (cast_word (get_word v) (ltac:(unwrap_ArithFacts; apply truncate_eq; auto) : Z.to_nat n = Z.to_nat m + (Z.to_nat n - Z.to_nat m))%nat)) (ltac:(unwrap_ArithFacts; apply Z2Nat.id; omega) : Z.of_nat (Z.to_nat m) = m).
 
+Definition vector_truncateLSB {n} (v : mword n) (m : Z) `{ArithFact (m >= 0)} `{ArithFact (m <= n)} : mword m :=
+  cast_to_mword (Word.split2 _ _ (cast_word (get_word v) (ltac:(unwrap_ArithFacts; apply truncateLSB_eq; auto) : Z.to_nat n = (Z.to_nat n - Z.to_nat m) + Z.to_nat m)%nat)) (ltac:(unwrap_ArithFacts; apply Z2Nat.id; omega) : Z.of_nat (Z.to_nat m) = m).
+
 Lemma concat_eq {a b} : a >= 0 -> b >= 0 -> Z.of_nat (Z.to_nat b + Z.to_nat a)%nat = a + b.
 intros.
 rewrite Nat2Z.inj_add.
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 85ca95f6..bd0d7750 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -86,6 +86,27 @@ red.
 omega.
 Defined.
 
+(* A version of well-foundedness of measures with a guard to ensure that
+   definitions can be reduced without inspecting proofs, based on a coq-club
+   thread featuring Barras, Gonthier and Gregoire, see
+     https://sympa.inria.fr/sympa/arc/coq-club/2007-07/msg00014.html *)
+
+Fixpoint pos_guard_wf {A:Type} {R:A -> A -> Prop} (p:positive) : well_founded R -> well_founded R :=
+ match p with
+ | xH => fun wfR x => Acc_intro x (fun y _ => wfR y)
+ | xO p' => fun wfR x => let F := pos_guard_wf p' in Acc_intro x (fun y _ => F (F 
+wfR) y)
+ | xI p' => fun wfR x => let F := pos_guard_wf p' in Acc_intro x (fun y _ => F (F 
+wfR) y)
+ end.
+
+Definition Zwf_guarded (z:Z) : Acc (Zwf 0) z :=
+  match z with
+  | Zpos p => pos_guard_wf p (Zwf_well_founded _) _
+  | _ => Zwf_well_founded _ _
+  end.
+
+
 (*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
 let rec whileM vars cond body =
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 37e75961..219a6f84 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -9,6 +9,7 @@ Require Export List.
 Require Export Sumbool.
 Require Export DecidableClass.
 Require Import Eqdep_dec.
+Require Export Zeuclid.
 Import ListNotations.
 
 Open Scope Z.
@@ -1125,6 +1126,10 @@ repeat
   end.
 *)
 
+(* The linear solver doesn't like existentials. *)
+Ltac destruct_exists :=
+  repeat match goal with H:@ex Z _ |- _ => destruct H end.
+
 Ltac prepare_for_solver :=
 (*dump_context;*)
  clear_irrelevant_defns;
@@ -1134,6 +1139,7 @@ Ltac prepare_for_solver :=
  extract_properties;
  repeat match goal with w:mword ?n |- _ => apply ArithFact_mword in w end;
  unwrap_ArithFacts;
+ destruct_exists;
  unbool_comparisons;
  unfold_In; (* after unbool_comparisons to deal with && and || *)
  reduce_list_lengths;
@@ -1175,6 +1181,8 @@ prepare_for_solver;
  [ match goal with |- ArithFact (?x _) => is_evar x; idtac "Warning: unknown constraint"; constructor; exact (I : (fun _ => True) _) end
  | apply ArithFact_mword; assumption
  | constructor; omega with Z
+   (* Try sail hints before dropping the existential *)
+ | constructor; eauto 3 with zarith sail
    (* The datatypes hints give us some list handling, esp In *)
  | constructor; drop_exists; eauto 3 with datatypes zarith sail
  | constructor; idtac "Unable to solve constraint"; dump_context; fail
@@ -1647,8 +1655,8 @@ end
 (* Arithmetic functions which return proofs that match the expected Sail
    types in smt.sail. *)
 
-Definition div_with_eq n m : {o : Z & ArithFact (o = Z.quot n m)} := build_ex (Z.quot n m).
-Definition mod_with_eq n m : {o : Z & ArithFact (o = Z.rem n m)} := build_ex (Z.rem n m).
+Definition ediv_with_eq n m : {o : Z & ArithFact (o = ZEuclid.div n m)} := build_ex (ZEuclid.div n m).
+Definition emod_with_eq n m : {o : Z & ArithFact (o = ZEuclid.modulo n m)} := build_ex (ZEuclid.modulo n m).
 Definition abs_with_eq n   : {o : Z & ArithFact (o = Z.abs n)} := build_ex (Z.abs n).
 
 (* Similarly, for ranges (currently in MIPS) *)
@@ -1798,3 +1806,7 @@ Definition sub_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
 Definition min_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
   {z : Z & ArithFact (z >= 0)} :=
   build_ex (Z.min x y).
+
+Definition max_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
+  {z : Z & ArithFact (z >= 0)} :=
+  build_ex (Z.max x y).