Bit of hackery to MIPS prelude and Makefiles to get monomorphised CHERI

1 files changed, 11 insertions, 0 deletions

diff --git a/mips/prelude.sail b/mips/prelude.sail
index aa81175f..281ef5ea 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -1,8 +1,11 @@
+$include <smt.sail>
+
 default Order dec
 
 type bits ('n : Int) = vector('n, dec, bit)
 union option ('a : Type) = {None : unit, Some : 'a}
 
+
 val eq_bit = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", interpreter: "eq_anything", c: "eq_bit"} : (bit, bit) -> bool
 
 val eq_vec = {ocaml: "eq_list", lem: "eq_vec"} : forall 'n. (bits('n), bits('n)) -> bool
@@ -120,6 +123,9 @@ val int_power = {ocaml: "int_power", lem: "pow"} : (int, int) -> int
 
 overload operator ^ = {xor_vec, int_power}
 
+val add_atom = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm.
+  (atom('n), atom('m)) -> atom('n + 'm)
+
 val add_range = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
 
@@ -131,6 +137,9 @@ val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> bits('n)
 
 overload operator + = {add_range, add_int, add_vec, add_vec_int}
 
+val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int"} : forall 'n 'm.
+  (atom('n), atom('m)) -> atom('n - 'm)
+
 val sub_range = {ocaml: "sub_int", lem: "integerMinus"} : forall 'n 'm 'o 'p.
   (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
 
@@ -292,3 +301,5 @@ val mask : forall 'm 'n , 'm >= 'n > 0 . bits('m) -> bits('n)
 function mask bs = bs['n - 1 .. 0]
 
 val "get_time_ns" : unit -> int
+
+$include <mono_rewrites.sail>