From b73f6d13b4bf2291f71616abdb046e2ca657d868 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 15 Aug 2018 13:59:16 +0100
Subject: Get RISC-V on Coq into reasonable state to show - Fill in Coq
 builtins for more of the RISC-V prelude - Update Barriers - More general
 autocast - Temporary sub_nat definition (until the backend handles nat
 better) - Patch to bring results into a reasonable state - Use Let rather
 than Definition for non-dependent top-level values

---
 lib/coq/Sail2_instr_kinds.v      |  4 ++++
 lib/coq/Sail2_operators_mwords.v | 10 +++++-----
 lib/coq/Sail2_values.v           |  7 ++++++-
 3 files changed, 15 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_instr_kinds.v b/lib/coq/Sail2_instr_kinds.v
index 57532e92..c93e9e93 100644
--- a/lib/coq/Sail2_instr_kinds.v
+++ b/lib/coq/Sail2_instr_kinds.v
@@ -153,6 +153,10 @@ Inductive barrier_kind :=
   | Barrier_RISCV_r_r
   | Barrier_RISCV_rw_w
   | Barrier_RISCV_w_w
+  | Barrier_RISCV_w_rw
+  | Barrier_RISCV_rw_r
+  | Barrier_RISCV_r_w
+  | Barrier_RISCV_w_r
   | Barrier_RISCV_i
   (* X86 *)
   | Barrier_x86_MFENCE.
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index bb4bf053..1d4eb906 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -15,21 +15,21 @@ Definition eq_dec := Z.eq_dec.
 End Z_eq_dec.
 Module ZEqdep := DecidableEqDep (Z_eq_dec).
 
-Definition cast_mword {m n} (x : mword m) (eq : m = n) : mword n.
+Definition cast_T {T : Z -> Type} {m n} (x : T m) (eq : m = n) : T n.
 rewrite <- eq.
 exact x.
 Defined.
 
-Lemma cast_mword_refl {m} {H:m = m} (x : mword m) : cast_mword x H = x.
+Lemma cast_T_refl {T : Z -> Type} {m} {H:m = m} (x : T m) : cast_T x H = x.
 rewrite (ZEqdep.UIP _ _ H eq_refl).
 reflexivity.
 Qed.
 
-Definition autocast {m n} (x : mword m) `{H:ArithFact (m = n)} : mword n :=
-  cast_mword x (use_ArithFact H).
+Definition autocast {T : Z -> Type} {m n} (x : T m) `{H:ArithFact (m = n)} : T n :=
+  cast_T x (use_ArithFact H).
 
 Definition autocast_m {rv e m n} (x : monad rv (mword m) e) `{H:ArithFact (m = n)} : monad rv (mword n) e :=
-  x >>= fun x => returnm (cast_mword x (use_ArithFact H)).
+  x >>= fun x => returnm (cast_T x (use_ArithFact H)).
 
 Definition cast_word {m n} (x : Word.word m) (eq : m = n) : Word.word n.
 rewrite <- eq.
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index c63e8453..30df0672 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1635,4 +1635,9 @@ Definition map_bind {A B} (f : A -> option B) (a : option A) : option B :=
 match a with
 | Some a' => f a'
 | None => None
-end.
\ No newline at end of file
+end.
+
+Definition sub_nat (x : {x : Z & ArithFact (x >= 0)}) (y : {y : Z & ArithFact (y >= 0)}) :
+  {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.
-- 
cgit v1.2.3