diff options
Diffstat (limited to 'lib/vector_dec.sail')
| -rw-r--r-- | lib/vector_dec.sail | 41 |
1 files changed, 26 insertions, 15 deletions
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 17603e03..d9b80b32 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,33 +21,36 @@ 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} -val "zeros" : forall 'n. atom('n) -> bits('n) +val sail_zeros = "zeros" : forall 'n. atom('n) -> bits('n) val "print_bits" : forall 'n. (string, bits('n)) -> unit -val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) +val "prerr_bits" : forall 'n. (string, bits('n)) -> unit -val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) +val sail_sign_extend = "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) + +val sail_zero_extend = "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) +} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit) -val mask : forall 'len 'v, 'v >= 0. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit) +val sail_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit) -function mask(len, v) = if len <= length(v) then truncate(v, len) else zero_extend(v, len) +function sail_mask(len, v) = if len <= length(v) then truncate(v, len) else sail_zero_extend(v, len) -overload operator ^ = {mask} +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} @@ -57,25 +61,29 @@ val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64) val vector_access = { ocaml: "access", lem: "access_list_dec", + coq: "access_list_dec", c: "vector_access" } : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a val vector_update = { ocaml: "update", lem: "update_list_dec", + coq: "update_list_dec", c: "vector_update" } : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) 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} @@ -83,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 @@ -111,7 +121,8 @@ val unsigned = { ocaml: "uint", lem: "uint", interpreter: "uint", - c: "sail_uint" + c: "sail_uint", + coq: "unsigned" } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) val signed = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) |