Merge branch 'sail2' into mappings

5 files changed, 32 insertions, 23 deletions

diff --git a/lib/arith.sail b/lib/arith.sail
index fa091772..54ecdbbc 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -5,7 +5,7 @@ $include <flow.sail>
 
 // ***** Addition *****
 
-val add_atom = {ocaml: "add_int", lem: "integerAdd"} : forall 'n 'm.
+val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int"} : forall 'n 'm.
   (atom('n), atom('m)) -> atom('n + 'm)
 
 val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int"} : (int, int) -> int
diff --git a/lib/elf.sail b/lib/elf.sail
index e953839d..2d799d4d 100644
--- a/lib/elf.sail
+++ b/lib/elf.sail
@@ -3,11 +3,13 @@ $define _ELF
 
 val elf_entry = {
   ocaml: "Elf_loader.elf_entry",
+  lem: "elf_entry",
   c: "elf_entry"
 } : unit -> int
 
 val elf_tohost = {
   ocaml: "Elf_loader.elf_tohost",
+  lem: "elf_tohost",
   c: "elf_tohost"
 } : unit -> int
 
diff --git a/lib/flow.sail b/lib/flow.sail
index ef213ada..cd3665b4 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -1,33 +1,33 @@
 $ifndef _FLOW
 $define _FLOW
 
-val not_bool = "not" : bool -> bool
-val and_bool = "and_bool" : (bool, bool) -> bool
-val or_bool = "or_bool" : (bool, bool) -> bool
+val not_bool = {coq: "negb", _: "not"} : bool -> bool
+val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
+val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool
 
-val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 
 val neq_atom = {lem: "neq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
 
 function neq_atom (x, y) = not_bool(eq_atom(x, y))
 
-val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
-val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
-val lt_atom = "lt"     : forall 'n 'm. (atom('n), atom('m)) -> bool
-val gt_atom = "gt"     : forall 'n 'm. (atom('n), atom('m)) -> bool
-
-val lt_range_atom = "lt"     : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
-val lteq_range_atom = "lteq" : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
-val gt_range_atom = "gt"     : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
-val gteq_range_atom = "gteq" : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
-val lt_atom_range = "lt"     : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
-val lteq_atom_range = "lteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
-val gt_atom_range = "gt"     : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
-val gteq_atom_range = "gteq" : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
-
-val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
-val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int"} : (int, int) -> bool
-val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool"} : (bool, bool) -> bool
+val lteq_atom = {coq: "Z.leb", _: "lteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool
+val lt_atom = {coq: "Z.ltb", _: "lt"}     : forall 'n 'm. (atom('n), atom('m)) -> bool
+val gt_atom = {coq: "Z.gtb", _: "gt"}     : forall 'n 'm. (atom('n), atom('m)) -> bool
+
+val lt_range_atom = {coq: "Z.ltb", _: "lt"}     : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
+val lteq_range_atom = {coq: "Z.lte", _: "lteq"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
+val gt_range_atom = {coq: "Z.gtb", _: "gt"}     : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
+val gteq_range_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool
+val lt_atom_range = {coq: "Z.ltb", _: "lt"}     : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
+val lteq_atom_range = {coq: "Z.leb", _: "lteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
+val gt_atom_range = {coq: "Z.gtb", _: "gt"}     : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
+val gteq_atom_range = {coq: "Z.geb", _: "gteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool
+
+val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
+val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : (int, int) -> bool
+val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool", coq: "Bool.eqb"} : (bool, bool) -> bool
 
 val neq_range = {lem: "neq"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool
 function neq_range (x, y) = not_bool(eq_range(x, y))
diff --git a/lib/smt.sail b/lib/smt.sail
index f8521a4a..ae672947 100644
--- a/lib/smt.sail
+++ b/lib/smt.sail
@@ -10,6 +10,8 @@ val div = {
   c: "div_int"
 } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = div('n, 'm). atom('o)}
 
+overload operator / = {div}
+
 val mod = {
   smt: "mod",
   ocaml: "modulus",
@@ -17,6 +19,8 @@ val mod = {
   c: "mod_int"
 } : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = mod('n, 'm). atom('o)}
 
+overload operator % = {mod}
+
 val abs_atom = {
   smt : "abs",
   ocaml: "abs_int",
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index eb2c9b7e..17603e03 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -15,7 +15,7 @@ val eq_bits = {
 
 overload operator == = {eq_bit, eq_bits}
 
-val bitvector_length = "length" : forall 'n. bits('n) -> atom('n)
+val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) -> atom('n)
 
 val vector_length = {
   ocaml: "length",
@@ -36,6 +36,7 @@ val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m)
 val truncate = {
   ocaml: "vector_truncate",
   lem: "vector_truncate",
+  coq: "vector_truncate",
   c: "truncate"
 } : forall 'm 'n, 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit)
 
@@ -67,11 +68,13 @@ val vector_update = {
 
 val add_bits = {
   ocaml: "add_vec",
+  lem: "add_vec",
   c: "add_bits"
 } : forall 'n. (bits('n), bits('n)) -> bits('n)
 
 val add_bits_int = {
   ocaml: "add_vec_int",
+  lem: "add_vec_int",
   c: "add_bits_int"
 } : forall 'n. (bits('n), int) -> bits('n)