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

3 files changed, 15 insertions, 6 deletions

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.