Add coq builtins for MIPS

2 files changed, 32 insertions, 4 deletions

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 55d85b3a..229a9c09 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -852,7 +852,7 @@ Ltac solve_arithfact :=
  reduce_list_lengths;
  reduce_pow;
  solve [apply ArithFact_mword; assumption
-       | constructor; omega
+       | constructor; omega with Z
          (* The datatypes hints give us some list handling, esp In *)
        | constructor; auto with datatypes zbool zarith sail].
 Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances.
@@ -1281,3 +1281,28 @@ Definition diafp_to_dia reginfo = function
 end
 *)
 *)
+
+(* Arithmetic functions which return proofs that match the expected Sail
+   types in smt.sail. *)
+
+Definition div_with_eq n m : {o : Z & ArithFact (o = Z.quot n m)} := build_ex (Z.quot n m).
+Definition mod_with_eq n m : {o : Z & ArithFact (o = Z.rem n m)} := build_ex (Z.rem n m).
+Definition abs_with_eq n   : {o : Z & ArithFact (o = Z.abs n)} := build_ex (Z.abs n).
+
+(* Similarly, for ranges (currently in MIPS) *)
+
+Definition add_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)})
+  : {x & ArithFact (n+o <= x <= m+p)} :=
+  build_ex ((projT1 l) + (projT1 r)).
+Definition sub_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)})
+  : {x & ArithFact (n-p <= x <= m-o)} :=
+  build_ex ((projT1 l) - (projT1 r)).
+Definition negate_range {n m} (l : {l : Z & ArithFact (n <= l <= m)})
+  : {x : Z & ArithFact ((- m) <= x <= (- n))} :=
+  build_ex (- (projT1 l)).
+
+Definition min_atom (a : Z) (b : Z) : {c : Z & ArithFact (c = a \/ c = b /\ c <= a /\ c <= b)} :=
+  build_ex (Z.min a b).
+Definition max_atom (a : Z) (b : Z) : {c : Z & ArithFact (c = a \/ c = b /\ c >= a /\ c >= b)} :=
+  build_ex (Z.max a b).
+
diff --git a/lib/smt.sail b/lib/smt.sail
index c9312819..efcbe48c 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -7,7 +7,8 @@ val div = {
   smt: "div",
   ocaml: "quotient",
   lem: "integerDiv",
-  c: "tdiv_int"
+  c: "tdiv_int",
+  coq: "div_with_eq"
 } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)}
 
 overload operator / = {div}
@@ -16,7 +17,8 @@ val mod = {
   smt: "mod",
   ocaml: "modulus",
   lem: "integerMod",
-  c: "tmod_int"
+  c: "tmod_int",
+  coq: "mod_with_eq"
 } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)}
 
 overload operator % = {mod}
@@ -25,7 +27,8 @@ val abs_atom = {
   smt : "abs",
   ocaml: "abs_int",
   lem: "abs_int",
-  c: "abs_int"
+  c: "abs_int",
+  coq: "abs_with_eq"
 } : forall 'n. atom('n) -> {'o, 'o = abs_atom('n). atom('o)}
 
 $ifdef TEST