4 files changed, 91 insertions, 13 deletions
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 497b4a46..809f9d89 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -9,12 +9,6 @@ Require Import ZArith.
 Require Import Omega.
 Require Import Eqdep_dec.
 
-Module Z_eq_dec.
-Definition U := Z.
-Definition eq_dec := Z.eq_dec.
-End Z_eq_dec.
-Module ZEqdep := DecidableEqDep (Z_eq_dec).
-
 Fixpoint cast_positive (T : positive -> Type) (p q : positive) : T p -> p = q -> T q.
 refine (
 match p, q with
@@ -178,6 +172,13 @@ 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).
@@ -444,6 +445,20 @@ Definition sgteq_vec := sgteq_bv.
 
 *)
 
+Definition eq_vec_dec {n} : forall (x y : mword n), {x = y} + {x <> y}.
+refine (match n with
+| Z0 => _
+| Zpos m => _
+| Zneg m => _
+end).
+* simpl. apply Word.weq.
+* simpl. apply Word.weq.
+* simpl. destruct x.
+Defined.
+
+Instance Decidable_eq_mword {n} : forall (x y : mword n), Decidable (x = y) :=
+  Decidable_eq_from_dec eq_vec_dec.
+
 Program Fixpoint reverse_endianness_word {n} (bits : word n) : word n :=
   match n with
   | S (S (S (S (S (S (S (S m))))))) =>
@@ -471,3 +486,5 @@ Definition set_slice_int len n lo (v : mword len) : Z :=
     let bs : mword (hi + 1) := mword_of_int n in
     (int_of_mword true (update_subrange_vec_dec bs hi lo v))
   else n.
+
+Definition prerr_bits {a} (s : string) (bs : mword a) : unit := tt.
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 1b12f360..85ca95f6 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -1,7 +1,7 @@
 (*Require Import Sail_impl_base*)
 Require Import Sail2_values.
 Require Import Sail2_prompt_monad.
-
+Require Export ZArith.Zwf.
 Require Import List.
 Import ListNotations.
 (*
@@ -77,6 +77,14 @@ match b with
   | BU => undefined_bool tt
 end.
 
+(* For termination of recursive functions.  We don't name assertions, so use
+   the type class mechanism to find it. *)
+Definition _limit_reduces {_limit} (_acc:Acc (Zwf 0) _limit) `{ArithFact (_limit >= 0)} : Acc (Zwf 0) (_limit - 1).
+refine (Acc_inv _acc _).
+destruct H.
+red.
+omega.
+Defined.
 
 (*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v
index a02556b2..0a00f8d7 100644
--- a/lib/coq/Sail2_string.v
+++ b/lib/coq/Sail2_string.v
@@ -7,12 +7,12 @@ Definition string_startswith s expected :=
   let prefix := String.substring 0 (String.length expected) s in
   generic_eq prefix expected.
 
-Definition string_drop s (n : {n : Z & ArithFact (n >= 0)}) :=
-  let n := Z.to_nat (projT1 n) in
+Definition string_drop s (n : Z) `{ArithFact (n >= 0)} :=
+  let n := Z.to_nat n in
   String.substring n (String.length s - n) s.
 
-Definition string_take s (n : {n : Z & ArithFact (n >= 0)}) :=
-  let n := Z.to_nat (projT1 n) in
+Definition string_take s (n : Z) `{ArithFact (n >= 0)} :=
+  let n := Z.to_nat n in
   String.substring 0 n s.
 
 Definition string_length s : {n : Z & ArithFact (n >= 0)} :=
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 83fe1dc7..e3e039c2 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -8,10 +8,18 @@ Require Import bbv.Word.
 Require Export List.
 Require Export Sumbool.
 Require Export DecidableClass.
+Require Import Eqdep_dec.
 Import ListNotations.
 
 Open Scope Z.
 
+Module Z_eq_dec.
+Definition U := Z.
+Definition eq_dec := Z.eq_dec.
+End Z_eq_dec.
+Module ZEqdep := DecidableEqDep (Z_eq_dec).
+
+
 (* Constraint solving basics.  A HintDb which unfolding hints and lemmata
    can be added to, and a typeclass to wrap constraint arguments in to
    trigger automatic solving. *)
@@ -93,6 +101,22 @@ split.
   tauto.
 Qed.
 
+Definition generic_dec {T:Type} (x y:T) `{Decidable (x = y)} : {x = y} + {x <> y}.
+refine ((if Decidable_witness as b return (b = true <-> x = y -> _) then fun H' => _ else fun H' => _) Decidable_spec).
+* left. tauto.
+* right. intuition.
+Defined.
+
+(* Used by generated code that builds Decidable equality instances for records. *)
+Ltac cmp_record_field x y :=
+  let H := fresh "H" in
+  case (generic_dec x y);
+  intro H; [ |
+    refine (Build_Decidable _ false _);
+    split; [congruence | intros Z; destruct H; injection Z; auto]
+  ].
+
+
 
 (* Project away range constraints in comparisons *)
 Definition ltb_range_l {lo hi} (l : {x & ArithFact (lo <= x /\ x <= hi)}) r := Z.ltb (projT1 l) r.
@@ -1101,6 +1125,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;
@@ -1110,6 +1138,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;
@@ -1151,6 +1180,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
@@ -1736,6 +1767,20 @@ Qed.
 
 Definition list_of_vec {A n} (v : vec A n) : list A := projT1 v.
 
+Definition vec_eq_dec {T n} (D : forall x y : T, {x = y} + {x <> y}) (x y : vec T n) :
+  {x = y} + {x <> y}.
+refine (if List.list_eq_dec D (projT1 x) (projT1 y) then left _ else right _).
+* apply eq_sigT_hprop; auto using ZEqdep.UIP.
+* contradict n0. rewrite n0. reflexivity.
+Defined.
+
+Instance Decidable_eq_vec {T : Type} {n} `(DT : forall x y : T, Decidable (x = y)) :
+  forall x y : vec T n, Decidable (x = y) := {
+  Decidable_witness := proj1_sig (bool_of_sumbool (vec_eq_dec (fun x y => generic_dec x y) x y))
+}.
+destruct (vec_eq_dec _ x y); simpl; split; congruence.
+Defined.
+
 Program Definition vec_of_list {A} n (l : list A) : option (vec A n) :=
   if sumbool_of_bool (n =? length_list l) then Some (existT _ l _) else None.
 Next Obligation.
@@ -1752,7 +1797,15 @@ match a with
 | None => None
 end.
 
-Definition sub_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y >= 0)}) :
+Definition sub_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} :
   {z : Z & ArithFact (z >= 0)} :=
-  let z := projT1 x - projT1 y in
+  let z := x - y in
   if sumbool_of_bool (z >=? 0) then build_ex z else build_ex 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).