From 104fd550bd99f2c22655f7d7aa173715054234fd Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 22 Oct 2018 17:36:17 +0100
Subject: Update Coq patch for RISC-V, add string_take to Coq library

---
 lib/coq/Sail2_string.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'lib/coq')

diff --git a/lib/coq/Sail2_string.v b/lib/coq/Sail2_string.v
index 0a63ff2c..a02556b2 100644
--- a/lib/coq/Sail2_string.v
+++ b/lib/coq/Sail2_string.v
@@ -11,6 +11,10 @@ Definition string_drop s (n : {n : Z & ArithFact (n >= 0)}) :=
   let n := Z.to_nat (projT1 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
+  String.substring 0 n s.
+
 Definition string_length s : {n : Z & ArithFact (n >= 0)} :=
  build_ex (Z.of_nat (String.length s)).
 
-- 
cgit v1.2.3


From c249747d681cb8e4c15af3d48f9191aa24777b27 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 20 Nov 2018 15:12:48 +0000
Subject: Minor coq updates

---
 lib/coq/Sail2_operators_mwords.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib/coq')

diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 497b4a46..b5bcfe5f 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -471,3 +471,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.
-- 
cgit v1.2.3


From 9b68baa58c1c6a3fc28df961624c522cca74cf8c Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 21 Nov 2018 13:58:26 +0000
Subject: Coq: add equality for records and polymorphic vectors

---
 lib/coq/Sail2_operators_mwords.v | 20 ++++++++++++++------
 lib/coq/Sail2_values.v           | 38 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 52 insertions(+), 6 deletions(-)

(limited to 'lib/coq')

diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index b5bcfe5f..e37e9d26 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
@@ -444,6 +438,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))))))) =>
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 83fe1dc7..48cfc222 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.
@@ -1736,6 +1760,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.
-- 
cgit v1.2.3


From 7fbf5d8ffb99e63d46d53fc3444764986764df9f Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 21 Nov 2018 13:58:39 +0000
Subject: Coq: min_nat

---
 lib/coq/Sail2_values.v | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'lib/coq')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 48cfc222..aebc3376 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1794,3 +1794,7 @@ Definition sub_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y
   {z : Z & ArithFact (z >= 0)} :=
   let z := projT1 x - projT1 y in
   if sumbool_of_bool (z >=? 0) then build_ex z else build_ex 0.
+
+Definition min_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y >= 0)}) :
+  {z : Z & ArithFact (z >= 0)} :=
+  build_ex (Z.min (projT1 x) (projT1 y)).
-- 
cgit v1.2.3


From 4f20163965e7c336f28740628fa9d64528006861 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 11 Dec 2018 11:54:36 +0000
Subject: Initial attempt at using termination measures in Coq This only
 applies to recursive functions and uses the termination measure merely as a
 limit to the recursive call depth, rather than proving the measure correct.

---
 lib/coq/Sail2_prompt.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'lib/coq')

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 1b12f360..8c0ca33c 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,13 @@ match b with
   | BU => undefined_bool tt
 end.
 
+(* For termination of recursive functions. *)
+Lemma _limit_is_limit {_limit : Z} : _limit >? 0 = true -> Zwf 0 (_limit - 1) _limit.
+intros.
+prepare_for_solver.
+red.
+omega.
+Qed.
 
 (*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-- 
cgit v1.2.3


From f8d88d4cf2439f4920fa948b054c4f0b2899e368 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 12 Dec 2018 18:23:00 +0000
Subject: Move much of recursive function termination to a rewrite It now
 includes updating the effects so that morally pure recursive functions can be
 turned into this impure termination-by-assertion form.

---
 lib/coq/Sail2_prompt.v | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'lib/coq')

diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v
index 8c0ca33c..85ca95f6 100644
--- a/lib/coq/Sail2_prompt.v
+++ b/lib/coq/Sail2_prompt.v
@@ -77,13 +77,14 @@ match b with
   | BU => undefined_bool tt
 end.
 
-(* For termination of recursive functions. *)
-Lemma _limit_is_limit {_limit : Z} : _limit >? 0 = true -> Zwf 0 (_limit - 1) _limit.
-intros.
-prepare_for_solver.
+(* 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.
-Qed.
+Defined.
 
 (*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) ->
                 ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-- 
cgit v1.2.3


From e5d108332cf700f73ea7b7527d0ae6006b0944c5 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 17 Dec 2018 12:23:30 +0000
Subject: Adapt Coq and termination measure support to typechecker changes Also
 output termination measures in Sail printer

---
 lib/coq/Sail2_string.v | 8 ++++----
 lib/coq/Sail2_values.v | 8 ++++----
 2 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'lib/coq')

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 aebc3376..37e75961 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1790,11 +1790,11 @@ 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 : {x : Z & ArithFact (x >= 0)}) (y : {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 (projT1 x) (projT1 y)).
+  build_ex (Z.min x y).
-- 
cgit v1.2.3