diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/arith.sail | 25 | ||||
| -rw-r--r-- | lib/vector_dec.sail | 23 | ||||
| -rw-r--r-- | lib/vector_inc.sail | 17 |
3 files changed, 40 insertions, 25 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index 78d5425b..f713805a 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -5,36 +5,36 @@ $include <flow.sail> // ***** Addition ***** -val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int"} : forall 'n 'm. +val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm. (atom('n), atom('m)) -> atom('n + 'm) -val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int"} : (int, int) -> int +val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : (int, int) -> int overload operator + = {add_atom, add_int} // ***** Subtraction ***** -val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int"} : forall 'n 'm. +val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm. (atom('n), atom('m)) -> atom('n - 'm) -val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int"} : (int, int) -> int +val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int overload operator - = {sub_atom, sub_int} // ***** Negation ***** -val negate_atom = {ocaml: "negate", lem: "integerNegate", c: "neg_int"} : forall 'n. atom('n) -> atom(- 'n) +val negate_atom = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. atom('n) -> atom(- 'n) -val negate_int = {ocaml: "negate", lem: "integerNegate", c: "neg_int"} : int -> int +val negate_int = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : int -> int overload negate = {negate_atom, negate_int} // ***** Multiplication ***** -val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int"} : forall 'n 'm. +val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm. (atom('n), atom('m)) -> atom('n * 'm) -val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int"} : (int, int) -> int +val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int overload operator * = {mult_atom, mult_int} @@ -54,7 +54,8 @@ val div_int = { smt: "div", ocaml: "quotient", lem: "integerDiv", - c: "div_int" + c: "div_int", + coq: "Z.quot" } : (int, int) -> int overload operator / = {div_int} @@ -63,7 +64,8 @@ val mod_int = { smt: "mod", ocaml: "modulus", lem: "integerMod", - c: "mod_int" + c: "mod_int", + coq: "Z.rem" } : (int, int) -> int overload operator % = {mod_int} @@ -71,7 +73,8 @@ overload operator % = {mod_int} val abs_int = { smt : "abs", ocaml: "abs_int", - lem: "abs_int" + lem: "abs_int", + coq: "Z.abs" } : (int, int) -> int $endif diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 05c7e35b..60f49af8 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -10,7 +10,8 @@ val "eq_bit" : (bit, bit) -> bool val eq_bits = { ocaml: "eq_list", lem: "eq_vec", - c: "eq_bits" + c: "eq_bits", + coq: "eq_vec" } : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool overload operator == = {eq_bit, eq_bits} @@ -20,7 +21,8 @@ val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) - val vector_length = { ocaml: "length", lem: "length_list", - c: "length" + c: "length", + coq: "length_list" } : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) overload length = {bitvector_length, vector_length} @@ -48,7 +50,7 @@ function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail overload operator ^ = {sail_mask} -val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int). +val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) overload append = {bitvector_concat} @@ -73,13 +75,15 @@ val vector_update = { val add_bits = { ocaml: "add_vec", lem: "add_vec", - c: "add_bits" + c: "add_bits", + coq: "add_vec" } : forall 'n. (bits('n), bits('n)) -> bits('n) val add_bits_int = { ocaml: "add_vec_int", lem: "add_vec_int", - c: "add_bits_int" + c: "add_bits_int", + coq: "add_vec_int" } : forall 'n. (bits('n), int) -> bits('n) overload operator + = {add_bits, add_bits_int} @@ -87,14 +91,16 @@ overload operator + = {add_bits, add_bits_int} val vector_subrange = { ocaml: "subrange", lem: "subrange_vec_dec", - c: "vector_subrange" + c: "vector_subrange", + coq: "subrange_vec_dec" } : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) val vector_update_subrange = { ocaml: "update_subrange", lem: "update_subrange_vec_dec", - c: "vector_update_subrange" + c: "vector_update_subrange", + coq: "update_subrange_vec_dec" } : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) // Some ARM specific builtins @@ -115,7 +121,8 @@ val unsigned = { ocaml: "uint", lem: "uint", interpreter: "uint", - c: "sail_uint" + c: "sail_uint", + coq: "uint" } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) val signed = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail index c45fec6b..b13e053c 100644 --- a/lib/vector_inc.sail +++ b/lib/vector_inc.sail @@ -10,7 +10,8 @@ val "eq_bit" : (bit, bit) -> bool val eq_bits = { ocaml: "eq_list", lem: "eq_vec", - c: "eq_bits" + c: "eq_bits", + coq: "eq_vec" } : forall 'n. (vector('n, inc, bit), vector('n, inc, bit)) -> bool overload operator == = {eq_bit, eq_bits} @@ -20,7 +21,8 @@ val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) - val vector_length = { ocaml: "length", lem: "length_list", - c: "length" + c: "length", + coq: "length_list" } : forall 'n ('a : Type). vector('n, inc, 'a) -> atom('n) overload length = {bitvector_length, vector_length} @@ -46,7 +48,7 @@ function mask(len, v) = if len <= length(v) then truncate(v, len) else zero_exte overload operator ^ = {mask} -val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append"} : forall ('n : Int) ('m : Int). +val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) overload append = {bitvector_concat} @@ -83,14 +85,16 @@ overload operator + = {add_bits, add_bits_int} val vector_subrange = { ocaml: "subrange", lem: "subrange_vec_inc", - c: "vector_subrange" + c: "vector_subrange", + coq: "subrange_vec_inc" } : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n. (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) val vector_update_subrange = { ocaml: "update_subrange", lem: "update_subrange_vec_inc", - c: "vector_update_subrange" + c: "vector_update_subrange", + coq: "update_subrange_vec_inc" } : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) // Some ARM specific builtins @@ -110,7 +114,8 @@ val unsigned = { ocaml: "uint", lem: "uint", interpreter: "uint", - c: "sail_uint" + c: "sail_uint", + coq: "uint" } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) val signed = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) |