From 6d90d18e460450b604cbfbd3f5bbe6db6cf6a61a Mon Sep 17 00:00:00 2001 From: Jon French Date: Wed, 24 Oct 2018 11:32:54 +0100 Subject: Interpreter: don't silently use OCaml externs, only interpreter externs (Adds 'interpreter' externs as appropriate.) --- lib/arith.sail | 19 +- lib/elf.sail | 2 + lib/flow.sail | 8 +- lib/instr_kinds.sail | 28 + lib/vector_dec.sail | 13 +- lib/vector_inc.sail | 14 +- riscv/prelude.sail | 1789 +++++++++++++++++++++++++------------------------- src/interpreter.ml | 5 +- src/value.ml | 31 + 9 files changed, 980 insertions(+), 929 deletions(-) create mode 100644 lib/instr_kinds.sail diff --git a/lib/arith.sail b/lib/arith.sail index 61a1ff76..3a1b0927 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -5,19 +5,19 @@ $include // ***** Addition ***** -val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm. +val add_atom = {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm. (int('n), int('m)) -> int('n + 'm) -val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : (int, int) -> int +val add_int = {ocaml: "add_int", interpreter: "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", coq: "Z.sub"} : forall 'n 'm. +val sub_atom = {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm. (int('n), int('m)) -> int('n - 'm) -val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int +val sub_int = {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int overload operator - = {sub_atom, sub_int} @@ -29,18 +29,18 @@ val sub_nat = { // ***** Negation ***** -val negate_atom = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. int('n) -> int(- 'n) +val negate_atom = {ocaml: "negate", interpreter: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. int('n) -> int(- 'n) -val negate_int = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : int -> int +val negate_int = {ocaml: "negate", interpreter: "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", coq: "Z.mul"} : forall 'n 'm. +val mult_atom = {ocaml: "mult", interpreter: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm. (int('n), int('m)) -> int('n * 'm) -val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int +val mult_int = {ocaml: "mult", interpreter: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int overload operator * = {mult_atom, mult_int} @@ -59,6 +59,7 @@ val shr_int = "shr_int" : (int, int) -> int val div_int = { smt: "div", ocaml: "quotient", + interpreter: "quotient", lem: "integerDiv", c: "tdiv_int", coq: "Z.quot" @@ -69,6 +70,7 @@ overload operator / = {div_int} val mod_int = { smt: "mod", ocaml: "modulus", + interpreter: "modulus", lem: "integerMod", c: "tmod_int", coq: "Z.rem" @@ -79,6 +81,7 @@ overload operator % = {mod_int} val abs_int = { smt : "abs", ocaml: "abs_int", + interpreter: "abs_int", lem: "abs_int", coq: "Z.abs" } : (int, int) -> int diff --git a/lib/elf.sail b/lib/elf.sail index 2d799d4d..6ea5de19 100644 --- a/lib/elf.sail +++ b/lib/elf.sail @@ -3,12 +3,14 @@ $define _ELF val elf_entry = { ocaml: "Elf_loader.elf_entry", + interpreter: "Elf_loader.elf_entry", lem: "elf_entry", c: "elf_entry" } : unit -> int val elf_tohost = { ocaml: "Elf_loader.elf_tohost", + interpreter: "Elf_loader.elf_tohost", lem: "elf_tohost", c: "elf_tohost" } : unit -> int diff --git a/lib/flow.sail b/lib/flow.sail index 5ee9a74a..7c6f1ebb 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -21,7 +21,7 @@ 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", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool +val eq_atom = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool val neq_atom = {lem: "neq", coq: "neq_atom"} : forall 'n 'm. (atom('n), atom('m)) -> bool @@ -41,9 +41,9 @@ val lteq_atom_range = {coq: "leb_range_r", _: "lteq"} : forall 'n 'm 'o. (atom(' val gt_atom_range = {coq: "gtb_range_r", _: "gt"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool val gteq_atom_range = {coq: "geb_range_r", _: "gteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool -val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "eq_range"} : 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 eq_range = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", c: "eq_int", coq: "eq_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool +val eq_int = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : (int, int) -> bool +val eq_bool = {ocaml: "eq_bool", interpreter: "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/instr_kinds.sail b/lib/instr_kinds.sail new file mode 100644 index 00000000..66ef90c6 --- /dev/null +++ b/lib/instr_kinds.sail @@ -0,0 +1,28 @@ +union read_kind = { + Read_plain : unit, + Read_reserve : unit, + Read_acquire : unit, + Read_exclusive : unit, + Read_exclusive_acquire : unit, + Read_stream : unit, + Read_RISCV_acquire : unit, + Read_RISCV_strong_acquire : unit, + Read_RISCV_reserved : unit, + Read_RISCV_reserved_acquire : unit, + Read_RISCV_reserved_strong_acquire : unit, + Read_X86_locked : unit +} + +union write_kind = { + Write_plain : unit + Write_conditional : unit + Write_release : unit + Write_exclusive : unit + Write_exclusive_release : unit + Write_RISCV_release : unit + Write_RISCV_strong_release : unit + Write_RISCV_conditional : unit + Write_RISCV_conditional_release : unit + Write_RISCV_conditional_strong_release : unit + Write_X86_locked : unit +} \ No newline at end of file diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 8abcd218..9ac4d1a5 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -9,6 +9,7 @@ val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool val eq_bits = { ocaml: "eq_list", + interpreter: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec" @@ -20,6 +21,7 @@ val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) - val vector_length = { ocaml: "length", + interpreter: "length", lem: "length_list", c: "length", coq: "vec_length" @@ -39,6 +41,7 @@ val sail_zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom(' val truncate = { ocaml: "vector_truncate", + interpreter: "vector_truncate", lem: "vector_truncate", coq: "vector_truncate", c: "sail_truncate" @@ -50,7 +53,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", coq: "concat_vec"} : forall ('n : Int) ('m : Int). +val bitvector_concat = {ocaml: "append", interpreter: "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} @@ -60,6 +63,7 @@ val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64) val bitvector_access = { ocaml: "access", + interpreter: "access", lem: "access_vec_dec", coq: "access_vec_dec", c: "vector_access" @@ -67,6 +71,7 @@ val bitvector_access = { val plain_vector_access = { ocaml: "access", + interpreter: "access", lem: "access_list_dec", coq: "vec_access_dec", c: "vector_access" @@ -76,6 +81,7 @@ overload vector_access = {bitvector_access, plain_vector_access} val bitvector_update = { ocaml: "update", + interpreter: "update", lem: "update_vec_dec", coq: "update_vec_dec", c: "vector_update" @@ -83,6 +89,7 @@ val bitvector_update = { val plain_vector_update = { ocaml: "update", + interpreter: "update", lem: "update_list_dec", coq: "vec_update_dec", c: "vector_update" @@ -92,6 +99,7 @@ overload vector_update = {bitvector_update, plain_vector_update} val add_bits = { ocaml: "add_vec", + interpreter: "add_vec", lem: "add_vec", c: "add_bits", coq: "add_vec" @@ -99,6 +107,7 @@ val add_bits = { val add_bits_int = { ocaml: "add_vec_int", + interpreter: "add_vec_int", lem: "add_vec_int", c: "add_bits_int", coq: "add_vec_int" @@ -108,6 +117,7 @@ overload operator + = {add_bits, add_bits_int} val vector_subrange = { ocaml: "subrange", + interpreter: "subrange", lem: "subrange_vec_dec", c: "vector_subrange", coq: "subrange_vec_dec" @@ -116,6 +126,7 @@ val vector_subrange = { val vector_update_subrange = { ocaml: "update_subrange", + interpreter: "update_subrange", lem: "update_subrange_vec_dec", c: "vector_update_subrange", coq: "update_subrange_vec_dec" diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail index b295c92c..b8e1b91f 100644 --- a/lib/vector_inc.sail +++ b/lib/vector_inc.sail @@ -9,6 +9,7 @@ val "eq_bit" : (bit, bit) -> bool val eq_bits = { ocaml: "eq_list", + interpreter: "eq_list", lem: "eq_vec", c: "eq_bits", coq: "eq_vec" @@ -20,6 +21,7 @@ val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. bits('n) - val vector_length = { ocaml: "length", + interpreter: "length", lem: "length_list", c: "length", coq: "length_list" @@ -37,6 +39,7 @@ val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) val truncate = { ocaml: "vector_truncate", + interpreter: "vector_truncate", lem: "vector_truncate", coq: "vector_truncate", c: "truncate" @@ -48,7 +51,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", coq: "concat_vec"} : forall ('n : Int) ('m : Int). +val bitvector_concat = {ocaml: "append", interpreter: "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} @@ -58,6 +61,7 @@ val "append_64" : forall 'n. (bits('n), bits(64)) -> bits('n + 64) val bitvector_access = { ocaml: "access", + interpreter: "access", lem: "access_vec_inc", coq: "access_vec_inc", c: "vector_access" @@ -65,6 +69,7 @@ val bitvector_access = { val plain_vector_access = { ocaml: "access", + interpreter: "access", lem: "access_list_inc", coq: "access_list_inc", c: "vector_access" @@ -74,6 +79,7 @@ overload vector_access = {bitvector_access, plain_vector_access} val bitvector_update = { ocaml: "update", + interpreter: "update", lem: "update_vec_inc", coq: "update_vec_inc", c: "vector_update" @@ -81,6 +87,7 @@ val bitvector_update = { val plain_vector_update = { ocaml: "update", + interpreter: "update", lem: "update_list_inc", coq: "update_list_inc", c: "vector_update" @@ -90,11 +97,12 @@ overload vector_update = {bitvector_update, plain_vector_update} val add_bits = { ocaml: "add_vec", + interpreter: "add_vec", c: "add_bits" } : forall 'n. (bits('n), bits('n)) -> bits('n) val add_bits_int = { - ocaml: "add_vec_int", + ocaml: "add_vec_int", interpreter: "add_vec_int", c: "add_bits_int" } : forall 'n. (bits('n), int) -> bits('n) @@ -102,6 +110,7 @@ overload operator + = {add_bits, add_bits_int} val vector_subrange = { ocaml: "subrange", + interpreter: "subrange", lem: "subrange_vec_inc", c: "vector_subrange", coq: "subrange_vec_inc" @@ -110,6 +119,7 @@ val vector_subrange = { val vector_update_subrange = { ocaml: "update_subrange", + interpreter: "update_subrange", lem: "update_subrange_vec_inc", c: "vector_update_subrange", coq: "update_subrange_vec_inc" diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 24913719..36f361ea 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -5,779 +5,75 @@ $include type bits ('n : Int) = vector('n, dec, bit) union option ('a : Type) = {None : unit, Some : 'a} -val spc : unit <-> string -val opt_spc : unit <-> string -val def_spc : unit <-> string +$include -val hex_bits : forall 'n . (atom('n), bits('n)) <-> string +val eq_atom = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> 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 string_startswith = "string_startswith" : (string, string) -> bool -val string_drop = "string_drop" : (string, nat) -> string -val string_take = "string_take" : (string, nat) -> string -val string_length = "string_length" : string -> nat -val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string -val maybe_int_of_prefix = "maybe_int_of_prefix" : string -> option((int, nat)) -val maybe_nat_of_prefix = "maybe_nat_of_prefix" : string -> option((nat, nat)) -val maybe_int_of_string = "maybe_int_of_string" : string -> option(int) +val eq_int = {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", coq: "Z.eqb", c: "eq_int"} : (int, int) -> bool +val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit", coq: "eq_bit"} : (bit, bit) -> bool -/* Python: -f = """val hex_bits_{0} : bits({0}) <-> string -val hex_bits_{0}_forwards = "decimal_string_of_bits" : bits({0}) -> string -val hex_bits_{0}_forwards_matches : bits({0}) -> bool -function hex_bits_{0}_forwards_matches bv = true -val "hex_bits_{0}_matches_prefix" : string -> option((bits({0}), nat)) -val hex_bits_{0}_backwards_matches : string -> bool -function hex_bits_{0}_backwards_matches s = match s {{ - s if match hex_bits_{0}_matches_prefix(s) {{ - Some (_, n) if n == string_length(s) => true, - _ => false - }} => true, - _ => false -}} -val hex_bits_{0}_backwards : string -> bits({0}) -function hex_bits_{0}_backwards s = - match hex_bits_{0}_matches_prefix(s) {{ - Some (bv, n) if n == string_length(s) => bv - }} -""" +val eq_vec = {ocaml: "eq_list", interpreter: "eq_list", lem: "eq_vec", coq: "eq_vec", c: "eq_bits"} : forall 'n. (bits('n), bits('n)) -> bool -for i in list(range(1, 34)) + [48, 64]: - print(f.format(i)) +val eq_string = {c: "eq_string", ocaml: "eq_string", interpreter: "eq_string", lem: "eq", coq: "generic_eq"} : (string, string) -> bool -*/ -val hex_bits_1 : bits(1) <-> string -val hex_bits_1_forwards = "decimal_string_of_bits" : bits(1) -> string -val hex_bits_1_forwards_matches : bits(1) -> bool -function hex_bits_1_forwards_matches bv = true -val "hex_bits_1_matches_prefix" : string -> option((bits(1), nat)) -val hex_bits_1_backwards_matches : string -> bool -function hex_bits_1_backwards_matches s = match s { - s if match hex_bits_1_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_1_backwards : string -> bits(1) -function hex_bits_1_backwards s = - match hex_bits_1_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } +val eq_real = {ocaml: "eq_real", interpreter: "eq_real", lem: "eq"} : (real, real) -> bool -val hex_bits_2 : bits(2) <-> string -val hex_bits_2_forwards = "decimal_string_of_bits" : bits(2) -> string -val hex_bits_2_forwards_matches : bits(2) -> bool -function hex_bits_2_forwards_matches bv = true -val "hex_bits_2_matches_prefix" : string -> option((bits(2), nat)) -val hex_bits_2_backwards_matches : string -> bool -function hex_bits_2_backwards_matches s = match s { - s if match hex_bits_2_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_2_backwards : string -> bits(2) -function hex_bits_2_backwards s = - match hex_bits_2_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } +val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq"} : forall ('a : Type). ('a, 'a) -> bool -val hex_bits_3 : bits(3) <-> string -val hex_bits_3_forwards = "decimal_string_of_bits" : bits(3) -> string -val hex_bits_3_forwards_matches : bits(3) -> bool -function hex_bits_3_forwards_matches bv = true -val "hex_bits_3_matches_prefix" : string -> option((bits(3), nat)) -val hex_bits_3_backwards_matches : string -> bool -function hex_bits_3_backwards_matches s = match s { - s if match hex_bits_3_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_3_backwards : string -> bits(3) -function hex_bits_3_backwards s = - match hex_bits_3_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } +val bitvector_length = {ocaml: "length", interpreter: "length", lem: "length", coq: "length_mword"} : forall 'n. bits('n) -> atom('n) +val vector_length = {ocaml: "length", interpreter: "length", lem: "length_list", coq: "vec_length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) +val list_length = {ocaml: "length", interpreter: "length", lem: "length_list", coq: "length_list"} : forall ('a : Type). list('a) -> int -val hex_bits_4 : bits(4) <-> string -val hex_bits_4_forwards = "decimal_string_of_bits" : bits(4) -> string -val hex_bits_4_forwards_matches : bits(4) -> bool -function hex_bits_4_forwards_matches bv = true -val "hex_bits_4_matches_prefix" : string -> option((bits(4), nat)) -val hex_bits_4_backwards_matches : string -> bool -function hex_bits_4_backwards_matches s = match s { - s if match hex_bits_4_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_4_backwards : string -> bits(4) -function hex_bits_4_backwards s = - match hex_bits_4_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } +overload length = {bitvector_length, vector_length, list_length} -val hex_bits_5 : bits(5) <-> string -val hex_bits_5_forwards = "decimal_string_of_bits" : bits(5) -> string -val hex_bits_5_forwards_matches : bits(5) -> bool -function hex_bits_5_forwards_matches bv = true -val "hex_bits_5_matches_prefix" : string -> option((bits(5), nat)) -val hex_bits_5_backwards_matches : string -> bool -function hex_bits_5_backwards_matches s = match s { - s if match hex_bits_5_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_5_backwards : string -> bits(5) -function hex_bits_5_backwards s = - match hex_bits_5_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } +val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} +/* sneaky deref with no effect necessary for bitfield writes */ +val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a -val hex_bits_6 : bits(6) <-> string -val hex_bits_6_forwards = "decimal_string_of_bits" : bits(6) -> string -val hex_bits_6_forwards_matches : bits(6) -> bool -function hex_bits_6_forwards_matches bv = true -val "hex_bits_6_matches_prefix" : string -> option((bits(6), nat)) -val hex_bits_6_backwards_matches : string -> bool -function hex_bits_6_backwards_matches s = match s { - s if match hex_bits_6_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_6_backwards : string -> bits(6) -function hex_bits_6_backwards s = - match hex_bits_6_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } +overload operator == = {eq_atom, eq_int, eq_bit, eq_vec, eq_string, eq_real, eq_anything} -val hex_bits_7 : bits(7) <-> string -val hex_bits_7_forwards = "decimal_string_of_bits" : bits(7) -> string -val hex_bits_7_forwards_matches : bits(7) -> bool -function hex_bits_7_forwards_matches bv = true -val "hex_bits_7_matches_prefix" : string -> option((bits(7), nat)) -val hex_bits_7_backwards_matches : string -> bool -function hex_bits_7_backwards_matches s = match s { - s if match hex_bits_7_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_7_backwards : string -> bits(7) -function hex_bits_7_backwards s = - match hex_bits_7_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } +val vector_subrange = { + ocaml: "subrange", interpreter: "subrange", + lem: "subrange_vec_dec", + c: "vector_subrange", + coq: "subrange_vec_dec" +} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n. + (bits('n), atom('m), atom('o)) -> bits('m - 'o + 1) +/* +val vector_subrange = {ocaml: "subrange", interpreter: "subrange", lem: "subrange_vec_dec", 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 hex_bits_8 : bits(8) <-> string -val hex_bits_8_forwards = "decimal_string_of_bits" : bits(8) -> string -val hex_bits_8_forwards_matches : bits(8) -> bool -function hex_bits_8_forwards_matches bv = true -val "hex_bits_8_matches_prefix" : string -> option((bits(8), nat)) -val hex_bits_8_backwards_matches : string -> bool -function hex_bits_8_backwards_matches s = match s { - s if match hex_bits_8_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_8_backwards : string -> bits(8) -function hex_bits_8_backwards s = - match hex_bits_8_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } +val bitvector_access = {c: "bitvector_access", ocaml: "access", interpreter: "access", lem: "access_vec_dec", coq: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n. + (bits('n), atom('m)) -> bit -val hex_bits_9 : bits(9) <-> string -val hex_bits_9_forwards = "decimal_string_of_bits" : bits(9) -> string -val hex_bits_9_forwards_matches : bits(9) -> bool -function hex_bits_9_forwards_matches bv = true -val "hex_bits_9_matches_prefix" : string -> option((bits(9), nat)) -val hex_bits_9_backwards_matches : string -> bool -function hex_bits_9_backwards_matches s = match s { - s if match hex_bits_9_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_9_backwards : string -> bits(9) -function hex_bits_9_backwards s = - match hex_bits_9_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } +val any_vector_access = {ocaml: "access", interpreter: "access", lem: "access_list_dec", coq: "vec_access_dec"} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. + (vector('n, dec, 'a), atom('m)) -> 'a -val hex_bits_10 : bits(10) <-> string -val hex_bits_10_forwards = "decimal_string_of_bits" : bits(10) -> string -val hex_bits_10_forwards_matches : bits(10) -> bool -function hex_bits_10_forwards_matches bv = true -val "hex_bits_10_matches_prefix" : string -> option((bits(10), nat)) -val hex_bits_10_backwards_matches : string -> bool -function hex_bits_10_backwards_matches s = match s { - s if match hex_bits_10_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_10_backwards : string -> bits(10) -function hex_bits_10_backwards s = - match hex_bits_10_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } +overload vector_access = {bitvector_access, any_vector_access} -val hex_bits_11 : bits(11) <-> string -val hex_bits_11_forwards = "decimal_string_of_bits" : bits(11) -> string -val hex_bits_11_forwards_matches : bits(11) -> bool -function hex_bits_11_forwards_matches bv = true -val "hex_bits_11_matches_prefix" : string -> option((bits(11), nat)) -val hex_bits_11_backwards_matches : string -> bool -function hex_bits_11_backwards_matches s = match s { - s if match hex_bits_11_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_11_backwards : string -> bits(11) -function hex_bits_11_backwards s = - match hex_bits_11_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } +val bitvector_update = {ocaml: "update", interpreter: "update", lem: "update_vec_dec", coq: "update_vec_dec"} : forall 'n. + (bits('n), int, bit) -> bits('n) -val hex_bits_12 : bits(12) <-> string -val hex_bits_12_forwards = "decimal_string_of_bits" : bits(12) -> string -val hex_bits_12_forwards_matches : bits(12) -> bool -function hex_bits_12_forwards_matches bv = true -val "hex_bits_12_matches_prefix" : string -> option((bits(12), nat)) -val hex_bits_12_backwards_matches : string -> bool -function hex_bits_12_backwards_matches s = match s { - s if match hex_bits_12_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_12_backwards : string -> bits(12) -function hex_bits_12_backwards s = - match hex_bits_12_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_13 : bits(13) <-> string -val hex_bits_13_forwards = "decimal_string_of_bits" : bits(13) -> string -val hex_bits_13_forwards_matches : bits(13) -> bool -function hex_bits_13_forwards_matches bv = true -val "hex_bits_13_matches_prefix" : string -> option((bits(13), nat)) -val hex_bits_13_backwards_matches : string -> bool -function hex_bits_13_backwards_matches s = match s { - s if match hex_bits_13_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_13_backwards : string -> bits(13) -function hex_bits_13_backwards s = - match hex_bits_13_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_14 : bits(14) <-> string -val hex_bits_14_forwards = "decimal_string_of_bits" : bits(14) -> string -val hex_bits_14_forwards_matches : bits(14) -> bool -function hex_bits_14_forwards_matches bv = true -val "hex_bits_14_matches_prefix" : string -> option((bits(14), nat)) -val hex_bits_14_backwards_matches : string -> bool -function hex_bits_14_backwards_matches s = match s { - s if match hex_bits_14_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_14_backwards : string -> bits(14) -function hex_bits_14_backwards s = - match hex_bits_14_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_15 : bits(15) <-> string -val hex_bits_15_forwards = "decimal_string_of_bits" : bits(15) -> string -val hex_bits_15_forwards_matches : bits(15) -> bool -function hex_bits_15_forwards_matches bv = true -val "hex_bits_15_matches_prefix" : string -> option((bits(15), nat)) -val hex_bits_15_backwards_matches : string -> bool -function hex_bits_15_backwards_matches s = match s { - s if match hex_bits_15_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_15_backwards : string -> bits(15) -function hex_bits_15_backwards s = - match hex_bits_15_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_16 : bits(16) <-> string -val hex_bits_16_forwards = "decimal_string_of_bits" : bits(16) -> string -val hex_bits_16_forwards_matches : bits(16) -> bool -function hex_bits_16_forwards_matches bv = true -val "hex_bits_16_matches_prefix" : string -> option((bits(16), nat)) -val hex_bits_16_backwards_matches : string -> bool -function hex_bits_16_backwards_matches s = match s { - s if match hex_bits_16_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_16_backwards : string -> bits(16) -function hex_bits_16_backwards s = - match hex_bits_16_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_17 : bits(17) <-> string -val hex_bits_17_forwards = "decimal_string_of_bits" : bits(17) -> string -val hex_bits_17_forwards_matches : bits(17) -> bool -function hex_bits_17_forwards_matches bv = true -val "hex_bits_17_matches_prefix" : string -> option((bits(17), nat)) -val hex_bits_17_backwards_matches : string -> bool -function hex_bits_17_backwards_matches s = match s { - s if match hex_bits_17_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_17_backwards : string -> bits(17) -function hex_bits_17_backwards s = - match hex_bits_17_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_18 : bits(18) <-> string -val hex_bits_18_forwards = "decimal_string_of_bits" : bits(18) -> string -val hex_bits_18_forwards_matches : bits(18) -> bool -function hex_bits_18_forwards_matches bv = true -val "hex_bits_18_matches_prefix" : string -> option((bits(18), nat)) -val hex_bits_18_backwards_matches : string -> bool -function hex_bits_18_backwards_matches s = match s { - s if match hex_bits_18_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_18_backwards : string -> bits(18) -function hex_bits_18_backwards s = - match hex_bits_18_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_19 : bits(19) <-> string -val hex_bits_19_forwards = "decimal_string_of_bits" : bits(19) -> string -val hex_bits_19_forwards_matches : bits(19) -> bool -function hex_bits_19_forwards_matches bv = true -val "hex_bits_19_matches_prefix" : string -> option((bits(19), nat)) -val hex_bits_19_backwards_matches : string -> bool -function hex_bits_19_backwards_matches s = match s { - s if match hex_bits_19_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_19_backwards : string -> bits(19) -function hex_bits_19_backwards s = - match hex_bits_19_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_20 : bits(20) <-> string -val hex_bits_20_forwards = "decimal_string_of_bits" : bits(20) -> string -val hex_bits_20_forwards_matches : bits(20) -> bool -function hex_bits_20_forwards_matches bv = true -val "hex_bits_20_matches_prefix" : string -> option((bits(20), nat)) -val hex_bits_20_backwards_matches : string -> bool -function hex_bits_20_backwards_matches s = match s { - s if match hex_bits_20_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_20_backwards : string -> bits(20) -function hex_bits_20_backwards s = - match hex_bits_20_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_21 : bits(21) <-> string -val hex_bits_21_forwards = "decimal_string_of_bits" : bits(21) -> string -val hex_bits_21_forwards_matches : bits(21) -> bool -function hex_bits_21_forwards_matches bv = true -val "hex_bits_21_matches_prefix" : string -> option((bits(21), nat)) -val hex_bits_21_backwards_matches : string -> bool -function hex_bits_21_backwards_matches s = match s { - s if match hex_bits_21_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_21_backwards : string -> bits(21) -function hex_bits_21_backwards s = - match hex_bits_21_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_22 : bits(22) <-> string -val hex_bits_22_forwards = "decimal_string_of_bits" : bits(22) -> string -val hex_bits_22_forwards_matches : bits(22) -> bool -function hex_bits_22_forwards_matches bv = true -val "hex_bits_22_matches_prefix" : string -> option((bits(22), nat)) -val hex_bits_22_backwards_matches : string -> bool -function hex_bits_22_backwards_matches s = match s { - s if match hex_bits_22_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_22_backwards : string -> bits(22) -function hex_bits_22_backwards s = - match hex_bits_22_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_23 : bits(23) <-> string -val hex_bits_23_forwards = "decimal_string_of_bits" : bits(23) -> string -val hex_bits_23_forwards_matches : bits(23) -> bool -function hex_bits_23_forwards_matches bv = true -val "hex_bits_23_matches_prefix" : string -> option((bits(23), nat)) -val hex_bits_23_backwards_matches : string -> bool -function hex_bits_23_backwards_matches s = match s { - s if match hex_bits_23_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_23_backwards : string -> bits(23) -function hex_bits_23_backwards s = - match hex_bits_23_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_24 : bits(24) <-> string -val hex_bits_24_forwards = "decimal_string_of_bits" : bits(24) -> string -val hex_bits_24_forwards_matches : bits(24) -> bool -function hex_bits_24_forwards_matches bv = true -val "hex_bits_24_matches_prefix" : string -> option((bits(24), nat)) -val hex_bits_24_backwards_matches : string -> bool -function hex_bits_24_backwards_matches s = match s { - s if match hex_bits_24_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_24_backwards : string -> bits(24) -function hex_bits_24_backwards s = - match hex_bits_24_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_25 : bits(25) <-> string -val hex_bits_25_forwards = "decimal_string_of_bits" : bits(25) -> string -val hex_bits_25_forwards_matches : bits(25) -> bool -function hex_bits_25_forwards_matches bv = true -val "hex_bits_25_matches_prefix" : string -> option((bits(25), nat)) -val hex_bits_25_backwards_matches : string -> bool -function hex_bits_25_backwards_matches s = match s { - s if match hex_bits_25_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_25_backwards : string -> bits(25) -function hex_bits_25_backwards s = - match hex_bits_25_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_26 : bits(26) <-> string -val hex_bits_26_forwards = "decimal_string_of_bits" : bits(26) -> string -val hex_bits_26_forwards_matches : bits(26) -> bool -function hex_bits_26_forwards_matches bv = true -val "hex_bits_26_matches_prefix" : string -> option((bits(26), nat)) -val hex_bits_26_backwards_matches : string -> bool -function hex_bits_26_backwards_matches s = match s { - s if match hex_bits_26_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_26_backwards : string -> bits(26) -function hex_bits_26_backwards s = - match hex_bits_26_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_27 : bits(27) <-> string -val hex_bits_27_forwards = "decimal_string_of_bits" : bits(27) -> string -val hex_bits_27_forwards_matches : bits(27) -> bool -function hex_bits_27_forwards_matches bv = true -val "hex_bits_27_matches_prefix" : string -> option((bits(27), nat)) -val hex_bits_27_backwards_matches : string -> bool -function hex_bits_27_backwards_matches s = match s { - s if match hex_bits_27_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_27_backwards : string -> bits(27) -function hex_bits_27_backwards s = - match hex_bits_27_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_28 : bits(28) <-> string -val hex_bits_28_forwards = "decimal_string_of_bits" : bits(28) -> string -val hex_bits_28_forwards_matches : bits(28) -> bool -function hex_bits_28_forwards_matches bv = true -val "hex_bits_28_matches_prefix" : string -> option((bits(28), nat)) -val hex_bits_28_backwards_matches : string -> bool -function hex_bits_28_backwards_matches s = match s { - s if match hex_bits_28_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_28_backwards : string -> bits(28) -function hex_bits_28_backwards s = - match hex_bits_28_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_29 : bits(29) <-> string -val hex_bits_29_forwards = "decimal_string_of_bits" : bits(29) -> string -val hex_bits_29_forwards_matches : bits(29) -> bool -function hex_bits_29_forwards_matches bv = true -val "hex_bits_29_matches_prefix" : string -> option((bits(29), nat)) -val hex_bits_29_backwards_matches : string -> bool -function hex_bits_29_backwards_matches s = match s { - s if match hex_bits_29_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_29_backwards : string -> bits(29) -function hex_bits_29_backwards s = - match hex_bits_29_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_30 : bits(30) <-> string -val hex_bits_30_forwards = "decimal_string_of_bits" : bits(30) -> string -val hex_bits_30_forwards_matches : bits(30) -> bool -function hex_bits_30_forwards_matches bv = true -val "hex_bits_30_matches_prefix" : string -> option((bits(30), nat)) -val hex_bits_30_backwards_matches : string -> bool -function hex_bits_30_backwards_matches s = match s { - s if match hex_bits_30_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_30_backwards : string -> bits(30) -function hex_bits_30_backwards s = - match hex_bits_30_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_31 : bits(31) <-> string -val hex_bits_31_forwards = "decimal_string_of_bits" : bits(31) -> string -val hex_bits_31_forwards_matches : bits(31) -> bool -function hex_bits_31_forwards_matches bv = true -val "hex_bits_31_matches_prefix" : string -> option((bits(31), nat)) -val hex_bits_31_backwards_matches : string -> bool -function hex_bits_31_backwards_matches s = match s { - s if match hex_bits_31_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_31_backwards : string -> bits(31) -function hex_bits_31_backwards s = - match hex_bits_31_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_32 : bits(32) <-> string -val hex_bits_32_forwards = "decimal_string_of_bits" : bits(32) -> string -val hex_bits_32_forwards_matches : bits(32) -> bool -function hex_bits_32_forwards_matches bv = true -val "hex_bits_32_matches_prefix" : string -> option((bits(32), nat)) -val hex_bits_32_backwards_matches : string -> bool -function hex_bits_32_backwards_matches s = match s { - s if match hex_bits_32_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_32_backwards : string -> bits(32) -function hex_bits_32_backwards s = - match hex_bits_32_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_33 : bits(33) <-> string -val hex_bits_33_forwards = "decimal_string_of_bits" : bits(33) -> string -val hex_bits_33_forwards_matches : bits(33) -> bool -function hex_bits_33_forwards_matches bv = true -val "hex_bits_33_matches_prefix" : string -> option((bits(33), nat)) -val hex_bits_33_backwards_matches : string -> bool -function hex_bits_33_backwards_matches s = match s { - s if match hex_bits_33_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_33_backwards : string -> bits(33) -function hex_bits_33_backwards s = - match hex_bits_33_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_48 : bits(48) <-> string -val hex_bits_48_forwards = "decimal_string_of_bits" : bits(48) -> string -val hex_bits_48_forwards_matches : bits(48) -> bool -function hex_bits_48_forwards_matches bv = true -val "hex_bits_48_matches_prefix" : string -> option((bits(48), nat)) -val hex_bits_48_backwards_matches : string -> bool -function hex_bits_48_backwards_matches s = match s { - s if match hex_bits_48_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_48_backwards : string -> bits(48) -function hex_bits_48_backwards s = - match hex_bits_48_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - -val hex_bits_64 : bits(64) <-> string -val hex_bits_64_forwards = "decimal_string_of_bits" : bits(64) -> string -val hex_bits_64_forwards_matches : bits(64) -> bool -function hex_bits_64_forwards_matches bv = true -val "hex_bits_64_matches_prefix" : string -> option((bits(64), nat)) -val hex_bits_64_backwards_matches : string -> bool -function hex_bits_64_backwards_matches s = match s { - s if match hex_bits_64_matches_prefix(s) { - Some (_, n) if n == string_length(s) => true, - _ => false - } => true, - _ => false -} -val hex_bits_64_backwards : string -> bits(64) -function hex_bits_64_backwards s = - match hex_bits_64_matches_prefix(s) { - Some (bv, n) if n == string_length(s) => bv - } - - -val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> 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 eq_int = {ocaml: "eq_int", lem: "eq", coq: "Z.eqb", c: "eq_int"} : (int, int) -> bool -val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit", coq: "eq_bit"} : (bit, bit) -> bool - -val eq_vec = {ocaml: "eq_list", lem: "eq_vec", coq: "eq_vec", c: "eq_bits"} : forall 'n. (bits('n), bits('n)) -> bool - -val eq_string = {c: "eq_string", ocaml: "eq_string", lem: "eq", coq: "generic_eq"} : (string, string) -> bool - -val eq_real = {ocaml: "eq_real", lem: "eq"} : (real, real) -> bool - -val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", coq: "generic_eq"} : forall ('a : Type). ('a, 'a) -> bool - -val bitvector_length = {ocaml: "length", lem: "length", coq: "length_mword"} : forall 'n. bits('n) -> atom('n) -val vector_length = {ocaml: "length", lem: "length_list", coq: "vec_length"} : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n) -val list_length = {ocaml: "length", lem: "length_list", coq: "length_list"} : forall ('a : Type). list('a) -> int - -overload length = {bitvector_length, vector_length, list_length} - -val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} -/* sneaky deref with no effect necessary for bitfield writes */ -val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a - -overload operator == = {eq_atom, eq_int, eq_bit, eq_vec, eq_string, eq_real, eq_anything} - -val vector_subrange = { - ocaml: "subrange", - lem: "subrange_vec_dec", - c: "vector_subrange", - coq: "subrange_vec_dec" -} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n. - (bits('n), atom('m), atom('o)) -> bits('m - 'o + 1) -/* -val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", 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 bitvector_access = {c: "bitvector_access", ocaml: "access", lem: "access_vec_dec", coq: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n. - (bits('n), atom('m)) -> bit - -val any_vector_access = {ocaml: "access", lem: "access_list_dec", coq: "vec_access_dec"} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. - (vector('n, dec, 'a), atom('m)) -> 'a - -overload vector_access = {bitvector_access, any_vector_access} - -val bitvector_update = {ocaml: "update", lem: "update_vec_dec", coq: "update_vec_dec"} : forall 'n. - (bits('n), int, bit) -> bits('n) - -val any_vector_update = {ocaml: "update", lem: "update_list_dec", coq: "vector_update"} : forall 'n ('a : Type). +val any_vector_update = {ocaml: "update", interpreter: "update", lem: "update_list_dec", coq: "vector_update"} : forall 'n ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) overload vector_update = {bitvector_update, any_vector_update} -val update_subrange = {ocaml: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. +val update_subrange = {ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) val vcons = {lem: "cons_vec"} : forall ('n : Int) ('a : Type). ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a) -val bitvector_concat = {c: "append", ocaml: "append", lem: "concat_vec", coq: "concat_vec"} : forall ('n : Int) ('m : Int). +val bitvector_concat = {c: "append", ocaml: "append", interpreter: "append", lem: "concat_vec", coq: "concat_vec"} : forall ('n : Int) ('m : Int). (bits('n), bits('m)) -> bits('n + 'm) -val vector_concat = {ocaml: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type). +val vector_concat = {ocaml: "append", interpreter: "append", lem: "append_list"} : forall ('n : Int) ('m : Int) ('a : Type). (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a) overload append = {bitvector_concat, vector_concat} @@ -798,17 +94,17 @@ function neq_anything (x, y) = not_bool(x == y) overload operator != = {neq_vec, neq_anything} -val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec", ocaml: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) +val and_vec = {lem: "and_vec", c: "and_bits", coq: "and_vec", ocaml: "and_vec", interpreter: "and_vec" } : forall 'n. (bits('n), bits('n)) -> bits('n) overload operator & = {and_vec} -val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec", ocaml: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) +val or_vec = {lem: "or_vec", c: "or_bits", coq: "or_vec", ocaml: "or_vec", interpreter: "or_vec" } : forall 'n. (bits('n), bits('n)) -> bits('n) overload operator | = {or_vec} -val unsigned = {ocaml: "uint", lem: "uint", coq: "uint", c: "sail_unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) +val unsigned = {ocaml: "uint", interpreter: "uint", lem: "uint", coq: "uint", c: "sail_unsigned"} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) -val signed = {ocaml: "sint", lem: "sint", coq: "sint", c: "sail_signed"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) +val signed = {ocaml: "sint", interpreter: "sint", lem: "sint", coq: "sint", c: "sail_signed"} : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) val hex_slice = "hex_slice" : forall 'n 'm, 'n >= 'm. (string, atom('n), atom('m)) -> bits('n - 'm) @@ -849,9 +145,9 @@ val print = "print_endline" : string -> unit val putchar = "putchar" : forall ('a : Type). 'a -> unit -val concat_str = {c: "concat_str", ocaml: "concat_str", lem: "stringAppend", coq: "String.append"} : (string, string) -> string +val concat_str = {c: "concat_str", ocaml: "concat_str", interpreter: "concat_str", lem: "stringAppend", coq: "String.append"} : (string, string) -> string -val string_of_int = {c: "string_of_int", ocaml: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string +val string_of_int = {c: "string_of_int", ocaml: "string_of_int", interpreter: "string_of_int", lem: "stringFromInteger", coq: "string_of_int"} : int -> string val DecStr : int -> string @@ -862,30 +158,30 @@ val "decimal_string_of_bits" : forall 'n. bits('n) -> string val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) -val int_power = {ocaml: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int +val int_power = {ocaml: "int_power", interpreter: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int -val real_power = {ocaml: "real_power", lem: "realPowInteger"} : (real, int) -> real +val real_power = {ocaml: "real_power", interpreter: "real_power", lem: "realPowInteger"} : (real, int) -> real overload operator ^ = {xor_vec, int_power, real_power, concat_str} -val add_range = {ocaml: "add_int", c: "add_int", lem: "integerAdd", coq: "add_range"} : forall 'n 'm 'o 'p. +val add_range = {ocaml: "add_int", interpreter: "add_int", c: "add_int", lem: "integerAdd", coq: "add_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) -val add_int = {ocaml: "add_int", c: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int +val add_int = {ocaml: "add_int", interpreter: "add_int", c: "add_int", lem: "integerAdd", coq: "Z.add"} : (int, int) -> int val add_vec = {c: "add_bits", _: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n) val add_vec_int = {c: "add_bits_int", _: "add_vec_int"} : forall 'n. (bits('n), int) -> bits('n) -val add_real = {ocaml: "add_real", lem: "realAdd"} : (real, real) -> real +val add_real = {ocaml: "add_real", interpreter: "add_real", lem: "realAdd"} : (real, real) -> real overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real} -val sub_range = {ocaml: "sub_int", c: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p. +val sub_range = {ocaml: "sub_int", interpreter: "sub_int", c: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) -val sub_int = {ocaml: "sub_int", c: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int -val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)", +val sub_int = {ocaml: "sub_int", interpreter: "sub_int", c: "sub_int", lem: "integerMinus", coq: "Z.sub"} : (int, int) -> int +val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)", interpreter: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)", lem: "integerMinus", coq: "sub_nat", c: "sub_nat"} : (nat, nat) -> nat @@ -893,240 +189,911 @@ val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n) -val sub_real = {ocaml: "sub_real", lem: "realMinus"} : (real, real) -> real +val sub_real = {ocaml: "sub_real", interpreter: "sub_real", lem: "realMinus"} : (real, real) -> real -val negate_range = {ocaml: "negate", lem: "integerNegate", coq: "negate_range"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) +val negate_range = {ocaml: "negate", interpreter: "negate", lem: "integerNegate", coq: "negate_range"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) -val negate_int = {ocaml: "negate", lem: "integerNegate", coq: "Z.opp"} : int -> int +val negate_int = {ocaml: "negate", interpreter: "negate", lem: "integerNegate", coq: "Z.opp"} : int -> int -val negate_real = {ocaml: "Num.minus_num", lem: "realNegate"} : real -> real +val negate_real = {ocaml: "Num.minus_num", interpreter: "Num.minus_num", lem: "realNegate"} : real -> real overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real} overload negate = {negate_range, negate_int, negate_real} -val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm. +val mult_atom = {ocaml: "mult", interpreter: "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", coq: "Z.mul"} : (int, int) -> int +val mult_int = {ocaml: "mult", interpreter: "mult", lem: "integerMult", coq: "Z.mul"} : (int, int) -> int -val mult_real = {ocaml: "mult_real", lem: "realMult"} : (real, real) -> real +val mult_real = {ocaml: "mult_real", interpreter: "mult_real", lem: "realMult"} : (real, real) -> real overload operator * = {mult_atom, mult_int, mult_real} -val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt"} : real -> real +val Sqrt = {ocaml: "sqrt_real", interpreter: "sqrt_real", lem: "realSqrt"} : real -> real val gteq_int = {coq: "Z.geb", _: "gteq"} : (int, int) -> bool -val gteq_real = {ocaml: "gteq_real", lem: "gteq"} : (real, real) -> bool +val gteq_real = {ocaml: "gteq_real", interpreter: "gteq_real", lem: "gteq"} : (real, real) -> bool overload operator >= = {gteq_atom, gteq_int, gteq_real} val lteq_int = {coq: "Z.leb", _: "lteq"} : (int, int) -> bool -val lteq_real = {ocaml: "lteq_real", lem: "lteq"} : (real, real) -> bool +val lteq_real = {ocaml: "lteq_real", interpreter: "lteq_real", lem: "lteq"} : (real, real) -> bool overload operator <= = {lteq_atom, lteq_int, lteq_real} val gt_int = {coq: "Z.gtb", _: "gt"} : (int, int) -> bool -val gt_real = {ocaml: "gt_real", lem: "gt"} : (real, real) -> bool +val gt_real = {ocaml: "gt_real", interpreter: "gt_real", lem: "gt"} : (real, real) -> bool overload operator > = {gt_atom, gt_int, gt_real} val lt_int = {coq: "Z.ltb", _: "lt"} : (int, int) -> bool -val lt_real = {ocaml: "lt_real", lem: "lt"} : (real, real) -> bool +val lt_real = {ocaml: "lt_real", interpreter: "lt_real", lem: "lt"} : (real, real) -> bool + +overload operator < = {lt_atom, lt_int, lt_real} + +val RoundDown = {ocaml: "round_down", interpreter: "round_down", lem: "realFloor"} : real -> int + +val RoundUp = {ocaml: "round_up", interpreter: "round_up", lem: "realCeiling"} : real -> int + +val abs_int = {ocaml: "abs_int", interpreter: "abs_int", lem: "abs", coq: "Z.abs"} : int -> int + +val abs_real = {ocaml: "abs_real", interpreter: "abs_real", lem: "abs"} : real -> real + +overload abs = {abs_int, abs_real} + +val quotient_nat = {ocaml: "quotient", interpreter: "quotient", lem: "integerDiv"} : (nat, nat) -> nat + +val quotient_real = {ocaml: "quotient_real", interpreter: "quotient_real", lem: "realDiv"} : (real, real) -> real + +val quotient = {ocaml: "quotient", interpreter: "quotient", lem: "integerDiv"} : (int, int) -> int + +overload operator / = {quotient_nat, quotient, quotient_real} + +val quot_round_zero = {ocaml: "quot_round_zero", interpreter: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int"} : (int, int) -> int +val rem_round_zero = {ocaml: "rem_round_zero", interpreter: "rem_round_zero", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int + +val modulus = {ocaml: "modulus", interpreter: "modulus", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int + +overload operator % = {modulus} + +val Real = {ocaml: "Num.num_of_big_int", interpreter: "Num.num_of_big_int", lem: "realFromInteger"} : int -> real + +val shl_int = "shl_int" : (int, int) -> int +val shr_int = "shr_int" : (int, int) -> int +val lor_int = "lor_int" : (int, int) -> int +val land_int = "land_int" : (int, int) -> int +val lxor_int = "lxor_int" : (int, int) -> int + +val min_nat = {ocaml: "min_int", interpreter: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat + +val min_int = {ocaml: "min_int", interpreter: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int + +val max_nat = {ocaml: "max_int", interpreter: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat + +val max_int = {ocaml: "max_int", interpreter: "max_int", lem: "max", coq: "Z.max", c: "max_int"} : (int, int) -> int + +overload min = {min_nat, min_int} + +overload max = {max_nat, max_int} + +val __TraceMemoryWrite : forall 'n 'm. + (atom('n), bits('m), bits(8 * 'n)) -> unit + +val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit + +val replicate_bits = "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), atom('m)) -> bits('n * 'm) + +val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)} + +function ex_nat 'n = n + +val cast ex_int : int -> {'n, true. atom('n)} + +function ex_int 'n = n + +/* +val cast ex_range : forall 'n 'm. range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('o)} + +function ex_range (n as 'N) = n +*/ + +val coerce_int_nat : int -> nat effect {escape} + +function coerce_int_nat 'x = { + assert(constraint('x >= 0)); + x +} + +val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0. + (bits('m), int, atom('n)) -> bits('n) + +val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) + +val print_int = "print_int" : (string, int) -> unit +val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit +val print_string = "print_string" : (string, string) -> unit + +val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) +val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) + +val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) +val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) + +function EXTS v = sign_extend(v, sizeof('m)) +function EXTZ v = zero_extend(v, sizeof('m)) + +infix 4 <_s +infix 4 >=_s +infix 4 <_u +infix 4 >=_u +infix 4 <=_u + +val operator <_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool +val operator >=_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool +val operator <_u : forall 'n. (bits('n), bits('n)) -> bool +val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool +val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool + +function operator <_s (x, y) = signed(x) < signed(y) +function operator >=_s (x, y) = signed(x) >= signed(y) +function operator <_u (x, y) = unsigned(x) < unsigned(y) +function operator >=_u (x, y) = unsigned(x) >= unsigned(y) +function operator <=_u (x, y) = unsigned(x) <= unsigned(y) + +val cast bool_to_bits : bool -> bits(1) +function bool_to_bits x = if x then 0b1 else 0b0 + +val cast bit_to_bool : bit -> bool +function bit_to_bool b = match b { + bitone => true, + bitzero => false +} + +infix 7 >> +infix 7 << + +val operator >> = "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) +val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) + +val vector64 : int -> bits(64) + +function vector64 n = __raw_GetSlice_int(64, n, 0) + +val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l) +function to_bits (l, n) = __raw_GetSlice_int(l, n, 0) + +val vector_update_subrange_dec = {ocaml: "update_subrange", interpreter: "update_subrange", c: "vector_update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. + (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) -overload operator < = {lt_atom, lt_int, lt_real} +val vector_update_subrange_inc = {ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o. + (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit) -val RoundDown = {ocaml: "round_down", lem: "realFloor"} : real -> int +overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc} -val RoundUp = {ocaml: "round_up", lem: "realCeiling"} : real -> int +/* Ideally these would be sail builtin */ -val abs_int = {ocaml: "abs_int", lem: "abs", coq: "Z.abs"} : int -> int +function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) = + let v128 : bits(128) = EXTS(v) in + (v128 >> shift)[63..0] -val abs_real = {ocaml: "abs_real", lem: "abs"} : real -> real +function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) = + let v64 : bits(64) = EXTS(v) in + (v64 >> shift)[31..0] -overload abs = {abs_int, abs_real} +/* Special version of zero_extend that the Lem back-end knows will be at a + case split on 'm and uses a more generic type for. (Temporary hack, honest) */ +val zero_extend_type_hack = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) -val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : (nat, nat) -> nat +val spc : unit <-> string +val opt_spc : unit <-> string +val def_spc : unit <-> string -val quotient_real = {ocaml: "quotient_real", lem: "realDiv"} : (real, real) -> real +val hex_bits : forall 'n . (atom('n), bits('n)) <-> string -val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int +val string_startswith = "string_startswith" : (string, string) -> bool +val string_drop = "string_drop" : (string, nat) -> string +val string_take = "string_take" : (string, nat) -> string +val string_length = "string_length" : string -> nat +val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string +val maybe_int_of_prefix = "maybe_int_of_prefix" : string -> option((int, nat)) +val maybe_nat_of_prefix = "maybe_nat_of_prefix" : string -> option((nat, nat)) +val maybe_int_of_string = "maybe_int_of_string" : string -> option(int) -overload operator / = {quotient_nat, quotient, quotient_real} +/* Python: +f = """val hex_bits_{0} : bits({0}) <-> string +val hex_bits_{0}_forwards = "decimal_string_of_bits" : bits({0}) -> string +val hex_bits_{0}_forwards_matches : bits({0}) -> bool +function hex_bits_{0}_forwards_matches bv = true +val "hex_bits_{0}_matches_prefix" : string -> option((bits({0}), nat)) +val hex_bits_{0}_backwards_matches : string -> bool +function hex_bits_{0}_backwards_matches s = match s {{ + s if match hex_bits_{0}_matches_prefix(s) {{ + Some (_, n) if n == string_length(s) => true, + _ => false + }} => true, + _ => false +}} +val hex_bits_{0}_backwards : string -> bits({0}) +function hex_bits_{0}_backwards s = + match hex_bits_{0}_matches_prefix(s) {{ + Some (bv, n) if n == string_length(s) => bv + }} +""" -val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", c: "tdiv_int"} : (int, int) -> int -val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int +for i in list(range(1, 34)) + [48, 64]: + print(f.format(i)) -val modulus = {ocaml: "modulus", lem: "hardware_mod", c: "tmod_int"} : (int, int) -> int +*/ +val hex_bits_1 : bits(1) <-> string +val hex_bits_1_forwards = "decimal_string_of_bits" : bits(1) -> string +val hex_bits_1_forwards_matches : bits(1) -> bool +function hex_bits_1_forwards_matches bv = true +val "hex_bits_1_matches_prefix" : string -> option((bits(1), nat)) +val hex_bits_1_backwards_matches : string -> bool +function hex_bits_1_backwards_matches s = match s { + s if match hex_bits_1_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_1_backwards : string -> bits(1) +function hex_bits_1_backwards s = + match hex_bits_1_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -overload operator % = {modulus} +val hex_bits_2 : bits(2) <-> string +val hex_bits_2_forwards = "decimal_string_of_bits" : bits(2) -> string +val hex_bits_2_forwards_matches : bits(2) -> bool +function hex_bits_2_forwards_matches bv = true +val "hex_bits_2_matches_prefix" : string -> option((bits(2), nat)) +val hex_bits_2_backwards_matches : string -> bool +function hex_bits_2_backwards_matches s = match s { + s if match hex_bits_2_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_2_backwards : string -> bits(2) +function hex_bits_2_backwards s = + match hex_bits_2_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val Real = {ocaml: "Num.num_of_big_int", lem: "realFromInteger"} : int -> real +val hex_bits_3 : bits(3) <-> string +val hex_bits_3_forwards = "decimal_string_of_bits" : bits(3) -> string +val hex_bits_3_forwards_matches : bits(3) -> bool +function hex_bits_3_forwards_matches bv = true +val "hex_bits_3_matches_prefix" : string -> option((bits(3), nat)) +val hex_bits_3_backwards_matches : string -> bool +function hex_bits_3_backwards_matches s = match s { + s if match hex_bits_3_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_3_backwards : string -> bits(3) +function hex_bits_3_backwards s = + match hex_bits_3_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val shl_int = "shl_int" : (int, int) -> int -val shr_int = "shr_int" : (int, int) -> int -val lor_int = "lor_int" : (int, int) -> int -val land_int = "land_int" : (int, int) -> int -val lxor_int = "lxor_int" : (int, int) -> int +val hex_bits_4 : bits(4) <-> string +val hex_bits_4_forwards = "decimal_string_of_bits" : bits(4) -> string +val hex_bits_4_forwards_matches : bits(4) -> bool +function hex_bits_4_forwards_matches bv = true +val "hex_bits_4_matches_prefix" : string -> option((bits(4), nat)) +val hex_bits_4_backwards_matches : string -> bool +function hex_bits_4_backwards_matches s = match s { + s if match hex_bits_4_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_4_backwards : string -> bits(4) +function hex_bits_4_backwards s = + match hex_bits_4_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val min_nat = {ocaml: "min_int", lem: "min", c: "min_int"} : (nat, nat) -> nat +val hex_bits_5 : bits(5) <-> string +val hex_bits_5_forwards = "decimal_string_of_bits" : bits(5) -> string +val hex_bits_5_forwards_matches : bits(5) -> bool +function hex_bits_5_forwards_matches bv = true +val "hex_bits_5_matches_prefix" : string -> option((bits(5), nat)) +val hex_bits_5_backwards_matches : string -> bool +function hex_bits_5_backwards_matches s = match s { + s if match hex_bits_5_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_5_backwards : string -> bits(5) +function hex_bits_5_backwards s = + match hex_bits_5_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val min_int = {ocaml: "min_int", lem: "min", coq: "Z.min", c: "min_int"} : (int, int) -> int +val hex_bits_6 : bits(6) <-> string +val hex_bits_6_forwards = "decimal_string_of_bits" : bits(6) -> string +val hex_bits_6_forwards_matches : bits(6) -> bool +function hex_bits_6_forwards_matches bv = true +val "hex_bits_6_matches_prefix" : string -> option((bits(6), nat)) +val hex_bits_6_backwards_matches : string -> bool +function hex_bits_6_backwards_matches s = match s { + s if match hex_bits_6_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_6_backwards : string -> bits(6) +function hex_bits_6_backwards s = + match hex_bits_6_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val max_nat = {ocaml: "max_int", lem: "max", c: "max_int"} : (nat, nat) -> nat +val hex_bits_7 : bits(7) <-> string +val hex_bits_7_forwards = "decimal_string_of_bits" : bits(7) -> string +val hex_bits_7_forwards_matches : bits(7) -> bool +function hex_bits_7_forwards_matches bv = true +val "hex_bits_7_matches_prefix" : string -> option((bits(7), nat)) +val hex_bits_7_backwards_matches : string -> bool +function hex_bits_7_backwards_matches s = match s { + s if match hex_bits_7_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_7_backwards : string -> bits(7) +function hex_bits_7_backwards s = + match hex_bits_7_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val max_int = {ocaml: "max_int", lem: "max", coq: "Z.max", c: "max_int"} : (int, int) -> int +val hex_bits_8 : bits(8) <-> string +val hex_bits_8_forwards = "decimal_string_of_bits" : bits(8) -> string +val hex_bits_8_forwards_matches : bits(8) -> bool +function hex_bits_8_forwards_matches bv = true +val "hex_bits_8_matches_prefix" : string -> option((bits(8), nat)) +val hex_bits_8_backwards_matches : string -> bool +function hex_bits_8_backwards_matches s = match s { + s if match hex_bits_8_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_8_backwards : string -> bits(8) +function hex_bits_8_backwards s = + match hex_bits_8_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -overload min = {min_nat, min_int} +val hex_bits_9 : bits(9) <-> string +val hex_bits_9_forwards = "decimal_string_of_bits" : bits(9) -> string +val hex_bits_9_forwards_matches : bits(9) -> bool +function hex_bits_9_forwards_matches bv = true +val "hex_bits_9_matches_prefix" : string -> option((bits(9), nat)) +val hex_bits_9_backwards_matches : string -> bool +function hex_bits_9_backwards_matches s = match s { + s if match hex_bits_9_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_9_backwards : string -> bits(9) +function hex_bits_9_backwards s = + match hex_bits_9_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -overload max = {max_nat, max_int} +val hex_bits_10 : bits(10) <-> string +val hex_bits_10_forwards = "decimal_string_of_bits" : bits(10) -> string +val hex_bits_10_forwards_matches : bits(10) -> bool +function hex_bits_10_forwards_matches bv = true +val "hex_bits_10_matches_prefix" : string -> option((bits(10), nat)) +val hex_bits_10_backwards_matches : string -> bool +function hex_bits_10_backwards_matches s = match s { + s if match hex_bits_10_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_10_backwards : string -> bits(10) +function hex_bits_10_backwards s = + match hex_bits_10_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val __WriteRAM = "write_ram" : forall 'n 'm. - (atom('m), atom('n), bits('m), bits('m), bits(8 * 'n)) -> bool effect {wmv} +val hex_bits_11 : bits(11) <-> string +val hex_bits_11_forwards = "decimal_string_of_bits" : bits(11) -> string +val hex_bits_11_forwards_matches : bits(11) -> bool +function hex_bits_11_forwards_matches bv = true +val "hex_bits_11_matches_prefix" : string -> option((bits(11), nat)) +val hex_bits_11_backwards_matches : string -> bool +function hex_bits_11_backwards_matches s = match s { + s if match hex_bits_11_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_11_backwards : string -> bits(11) +function hex_bits_11_backwards s = + match hex_bits_11_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val __RISCV_write : forall 'n. (bits(64), atom('n), bits(8 * 'n)) -> bool effect {wmv} -function __RISCV_write (addr, width, data) = { - __WriteRAM(64, width, 0x0000_0000_0000_0000, addr, data) +val hex_bits_12 : bits(12) <-> string +val hex_bits_12_forwards = "decimal_string_of_bits" : bits(12) -> string +val hex_bits_12_forwards_matches : bits(12) -> bool +function hex_bits_12_forwards_matches bv = true +val "hex_bits_12_matches_prefix" : string -> option((bits(12), nat)) +val hex_bits_12_backwards_matches : string -> bool +function hex_bits_12_backwards_matches s = match s { + s if match hex_bits_12_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false } - -val __TraceMemoryWrite : forall 'n 'm. - (atom('n), bits('m), bits(8 * 'n)) -> unit - -val __ReadRAM = { lem: "MEMr", _ : "read_ram" } : forall 'n 'm, 'n >= 0. - (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} - -val __ReadRAM_acquire = { lem: "MEMr_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. - (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} - -val __ReadRAM_strong_acquire = { lem: "MEMr_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. - (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} - -val __ReadRAM_reserved = { lem: "MEMr_reserved", _ : "read_ram" } : forall 'n 'm, 'n >= 0. - (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} - -val __ReadRAM_reserved_acquire = { lem: "MEMr_reserved_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. - (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} - -val __ReadRAM_reserved_strong_acquire = { lem: "MEMr_reserved_strong_acquire", _ : "read_ram" } : forall 'n 'm, 'n >= 0. - (atom('m), atom('n), bits('m), bits('m)) -> bits(8 * 'n) effect {rmem} - -val __RISCV_read : forall 'n, 'n >= 0. (bits(64), atom('n), bool, bool, bool) -> option(bits(8 * 'n)) effect {rmem} -function __RISCV_read (addr, width, aq, rl, res) = - match (aq, rl, res) { - (false, false, false) => Some(__ReadRAM(64, width, 0x0000_0000_0000_0000, addr)), - (true, false, false) => Some(__ReadRAM_acquire(64, width, 0x0000_0000_0000_0000, addr)), - (true, true, false) => Some(__ReadRAM_strong_acquire(64, width, 0x0000_0000_0000_0000, addr)), - (false, false, true) => Some(__ReadRAM_reserved(64, width, 0x0000_0000_0000_0000, addr)), - (true, false, true) => Some(__ReadRAM_reserved_acquire(64, width, 0x0000_0000_0000_0000, addr)), - (true, true, true) => Some(__ReadRAM_reserved_strong_acquire(64, width, 0x0000_0000_0000_0000, addr)), - (false, true, false) => None(), - (false, true, true) => None() +val hex_bits_12_backwards : string -> bits(12) +function hex_bits_12_backwards s = + match hex_bits_12_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv } -val __TraceMemoryRead : forall 'n 'm. (atom('n), bits('m), bits(8 * 'n)) -> unit - -val replicate_bits = "replicate_bits" : forall 'n 'm, 'm >= 0. (bits('n), atom('m)) -> bits('n * 'm) - -val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)} - -function ex_nat 'n = n - -val cast ex_int : int -> {'n, true. atom('n)} - -function ex_int 'n = n - -/* -val cast ex_range : forall 'n 'm. range('n, 'm) -> {'o, 'n <= 'o <= 'm. atom('o)} - -function ex_range (n as 'N) = n -*/ - -val coerce_int_nat : int -> nat effect {escape} +val hex_bits_13 : bits(13) <-> string +val hex_bits_13_forwards = "decimal_string_of_bits" : bits(13) -> string +val hex_bits_13_forwards_matches : bits(13) -> bool +function hex_bits_13_forwards_matches bv = true +val "hex_bits_13_matches_prefix" : string -> option((bits(13), nat)) +val hex_bits_13_backwards_matches : string -> bool +function hex_bits_13_backwards_matches s = match s { + s if match hex_bits_13_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_13_backwards : string -> bits(13) +function hex_bits_13_backwards s = + match hex_bits_13_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -function coerce_int_nat 'x = { - assert(constraint('x >= 0)); - x +val hex_bits_14 : bits(14) <-> string +val hex_bits_14_forwards = "decimal_string_of_bits" : bits(14) -> string +val hex_bits_14_forwards_matches : bits(14) -> bool +function hex_bits_14_forwards_matches bv = true +val "hex_bits_14_matches_prefix" : string -> option((bits(14), nat)) +val hex_bits_14_backwards_matches : string -> bool +function hex_bits_14_backwards_matches s = match s { + s if match hex_bits_14_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false } +val hex_bits_14_backwards : string -> bits(14) +function hex_bits_14_backwards s = + match hex_bits_14_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0. - (bits('m), int, atom('n)) -> bits('n) +val hex_bits_15 : bits(15) <-> string +val hex_bits_15_forwards = "decimal_string_of_bits" : bits(15) -> string +val hex_bits_15_forwards_matches : bits(15) -> bool +function hex_bits_15_forwards_matches bv = true +val "hex_bits_15_matches_prefix" : string -> option((bits(15), nat)) +val hex_bits_15_backwards_matches : string -> bool +function hex_bits_15_backwards_matches s = match s { + s if match hex_bits_15_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_15_backwards : string -> bits(15) +function hex_bits_15_backwards s = + match hex_bits_15_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) +val hex_bits_16 : bits(16) <-> string +val hex_bits_16_forwards = "decimal_string_of_bits" : bits(16) -> string +val hex_bits_16_forwards_matches : bits(16) -> bool +function hex_bits_16_forwards_matches bv = true +val "hex_bits_16_matches_prefix" : string -> option((bits(16), nat)) +val hex_bits_16_backwards_matches : string -> bool +function hex_bits_16_backwards_matches s = match s { + s if match hex_bits_16_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_16_backwards : string -> bits(16) +function hex_bits_16_backwards s = + match hex_bits_16_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val print_int = "print_int" : (string, int) -> unit -val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit -val print_string = "print_string" : (string, string) -> unit +val hex_bits_17 : bits(17) <-> string +val hex_bits_17_forwards = "decimal_string_of_bits" : bits(17) -> string +val hex_bits_17_forwards_matches : bits(17) -> bool +function hex_bits_17_forwards_matches bv = true +val "hex_bits_17_matches_prefix" : string -> option((bits(17), nat)) +val hex_bits_17_backwards_matches : string -> bool +function hex_bits_17_backwards_matches s = match s { + s if match hex_bits_17_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_17_backwards : string -> bits(17) +function hex_bits_17_backwards s = + match hex_bits_17_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) -val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) +val hex_bits_18 : bits(18) <-> string +val hex_bits_18_forwards = "decimal_string_of_bits" : bits(18) -> string +val hex_bits_18_forwards_matches : bits(18) -> bool +function hex_bits_18_forwards_matches bv = true +val "hex_bits_18_matches_prefix" : string -> option((bits(18), nat)) +val hex_bits_18_backwards_matches : string -> bool +function hex_bits_18_backwards_matches s = match s { + s if match hex_bits_18_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_18_backwards : string -> bits(18) +function hex_bits_18_backwards s = + match hex_bits_18_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) -val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) +val hex_bits_19 : bits(19) <-> string +val hex_bits_19_forwards = "decimal_string_of_bits" : bits(19) -> string +val hex_bits_19_forwards_matches : bits(19) -> bool +function hex_bits_19_forwards_matches bv = true +val "hex_bits_19_matches_prefix" : string -> option((bits(19), nat)) +val hex_bits_19_backwards_matches : string -> bool +function hex_bits_19_backwards_matches s = match s { + s if match hex_bits_19_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_19_backwards : string -> bits(19) +function hex_bits_19_backwards s = + match hex_bits_19_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -function EXTS v = sign_extend(v, sizeof('m)) -function EXTZ v = zero_extend(v, sizeof('m)) +val hex_bits_20 : bits(20) <-> string +val hex_bits_20_forwards = "decimal_string_of_bits" : bits(20) -> string +val hex_bits_20_forwards_matches : bits(20) -> bool +function hex_bits_20_forwards_matches bv = true +val "hex_bits_20_matches_prefix" : string -> option((bits(20), nat)) +val hex_bits_20_backwards_matches : string -> bool +function hex_bits_20_backwards_matches s = match s { + s if match hex_bits_20_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_20_backwards : string -> bits(20) +function hex_bits_20_backwards s = + match hex_bits_20_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -infix 4 <_s -infix 4 >=_s -infix 4 <_u -infix 4 >=_u -infix 4 <=_u +val hex_bits_21 : bits(21) <-> string +val hex_bits_21_forwards = "decimal_string_of_bits" : bits(21) -> string +val hex_bits_21_forwards_matches : bits(21) -> bool +function hex_bits_21_forwards_matches bv = true +val "hex_bits_21_matches_prefix" : string -> option((bits(21), nat)) +val hex_bits_21_backwards_matches : string -> bool +function hex_bits_21_backwards_matches s = match s { + s if match hex_bits_21_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_21_backwards : string -> bits(21) +function hex_bits_21_backwards s = + match hex_bits_21_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val operator <_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool -val operator >=_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool -val operator <_u : forall 'n. (bits('n), bits('n)) -> bool -val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool -val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool +val hex_bits_22 : bits(22) <-> string +val hex_bits_22_forwards = "decimal_string_of_bits" : bits(22) -> string +val hex_bits_22_forwards_matches : bits(22) -> bool +function hex_bits_22_forwards_matches bv = true +val "hex_bits_22_matches_prefix" : string -> option((bits(22), nat)) +val hex_bits_22_backwards_matches : string -> bool +function hex_bits_22_backwards_matches s = match s { + s if match hex_bits_22_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_22_backwards : string -> bits(22) +function hex_bits_22_backwards s = + match hex_bits_22_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -function operator <_s (x, y) = signed(x) < signed(y) -function operator >=_s (x, y) = signed(x) >= signed(y) -function operator <_u (x, y) = unsigned(x) < unsigned(y) -function operator >=_u (x, y) = unsigned(x) >= unsigned(y) -function operator <=_u (x, y) = unsigned(x) <= unsigned(y) +val hex_bits_23 : bits(23) <-> string +val hex_bits_23_forwards = "decimal_string_of_bits" : bits(23) -> string +val hex_bits_23_forwards_matches : bits(23) -> bool +function hex_bits_23_forwards_matches bv = true +val "hex_bits_23_matches_prefix" : string -> option((bits(23), nat)) +val hex_bits_23_backwards_matches : string -> bool +function hex_bits_23_backwards_matches s = match s { + s if match hex_bits_23_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_23_backwards : string -> bits(23) +function hex_bits_23_backwards s = + match hex_bits_23_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val cast bool_to_bits : bool -> bits(1) -function bool_to_bits x = if x then 0b1 else 0b0 +val hex_bits_24 : bits(24) <-> string +val hex_bits_24_forwards = "decimal_string_of_bits" : bits(24) -> string +val hex_bits_24_forwards_matches : bits(24) -> bool +function hex_bits_24_forwards_matches bv = true +val "hex_bits_24_matches_prefix" : string -> option((bits(24), nat)) +val hex_bits_24_backwards_matches : string -> bool +function hex_bits_24_backwards_matches s = match s { + s if match hex_bits_24_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_24_backwards : string -> bits(24) +function hex_bits_24_backwards s = + match hex_bits_24_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val cast bit_to_bool : bit -> bool -function bit_to_bool b = match b { - bitone => true, - bitzero => false +val hex_bits_25 : bits(25) <-> string +val hex_bits_25_forwards = "decimal_string_of_bits" : bits(25) -> string +val hex_bits_25_forwards_matches : bits(25) -> bool +function hex_bits_25_forwards_matches bv = true +val "hex_bits_25_matches_prefix" : string -> option((bits(25), nat)) +val hex_bits_25_backwards_matches : string -> bool +function hex_bits_25_backwards_matches s = match s { + s if match hex_bits_25_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false } +val hex_bits_25_backwards : string -> bits(25) +function hex_bits_25_backwards s = + match hex_bits_25_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -infix 7 >> -infix 7 << +val hex_bits_26 : bits(26) <-> string +val hex_bits_26_forwards = "decimal_string_of_bits" : bits(26) -> string +val hex_bits_26_forwards_matches : bits(26) -> bool +function hex_bits_26_forwards_matches bv = true +val "hex_bits_26_matches_prefix" : string -> option((bits(26), nat)) +val hex_bits_26_backwards_matches : string -> bool +function hex_bits_26_backwards_matches s = match s { + s if match hex_bits_26_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_26_backwards : string -> bits(26) +function hex_bits_26_backwards s = + match hex_bits_26_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val operator >> = "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) -val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n) +val hex_bits_27 : bits(27) <-> string +val hex_bits_27_forwards = "decimal_string_of_bits" : bits(27) -> string +val hex_bits_27_forwards_matches : bits(27) -> bool +function hex_bits_27_forwards_matches bv = true +val "hex_bits_27_matches_prefix" : string -> option((bits(27), nat)) +val hex_bits_27_backwards_matches : string -> bool +function hex_bits_27_backwards_matches s = match s { + s if match hex_bits_27_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_27_backwards : string -> bits(27) +function hex_bits_27_backwards s = + match hex_bits_27_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val vector64 : int -> bits(64) +val hex_bits_28 : bits(28) <-> string +val hex_bits_28_forwards = "decimal_string_of_bits" : bits(28) -> string +val hex_bits_28_forwards_matches : bits(28) -> bool +function hex_bits_28_forwards_matches bv = true +val "hex_bits_28_matches_prefix" : string -> option((bits(28), nat)) +val hex_bits_28_backwards_matches : string -> bool +function hex_bits_28_backwards_matches s = match s { + s if match hex_bits_28_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_28_backwards : string -> bits(28) +function hex_bits_28_backwards s = + match hex_bits_28_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -function vector64 n = __raw_GetSlice_int(64, n, 0) +val hex_bits_29 : bits(29) <-> string +val hex_bits_29_forwards = "decimal_string_of_bits" : bits(29) -> string +val hex_bits_29_forwards_matches : bits(29) -> bool +function hex_bits_29_forwards_matches bv = true +val "hex_bits_29_matches_prefix" : string -> option((bits(29), nat)) +val hex_bits_29_backwards_matches : string -> bool +function hex_bits_29_backwards_matches s = match s { + s if match hex_bits_29_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_29_backwards : string -> bits(29) +function hex_bits_29_backwards s = + match hex_bits_29_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l) -function to_bits (l, n) = __raw_GetSlice_int(l, n, 0) +val hex_bits_30 : bits(30) <-> string +val hex_bits_30_forwards = "decimal_string_of_bits" : bits(30) -> string +val hex_bits_30_forwards_matches : bits(30) -> bool +function hex_bits_30_forwards_matches bv = true +val "hex_bits_30_matches_prefix" : string -> option((bits(30), nat)) +val hex_bits_30_backwards_matches : string -> bool +function hex_bits_30_backwards_matches s = match s { + s if match hex_bits_30_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_30_backwards : string -> bits(30) +function hex_bits_30_backwards s = + match hex_bits_30_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val vector_update_subrange_dec = {ocaml: "update_subrange", c: "vector_update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o. - (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n) +val hex_bits_31 : bits(31) <-> string +val hex_bits_31_forwards = "decimal_string_of_bits" : bits(31) -> string +val hex_bits_31_forwards_matches : bits(31) -> bool +function hex_bits_31_forwards_matches bv = true +val "hex_bits_31_matches_prefix" : string -> option((bits(31), nat)) +val hex_bits_31_backwards_matches : string -> bool +function hex_bits_31_backwards_matches s = match s { + s if match hex_bits_31_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_31_backwards : string -> bits(31) +function hex_bits_31_backwards s = + match hex_bits_31_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -val vector_update_subrange_inc = {ocaml: "update_subrange", lem: "update_subrange_vec_inc"} : forall 'n 'm 'o. - (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit) +val hex_bits_32 : bits(32) <-> string +val hex_bits_32_forwards = "decimal_string_of_bits" : bits(32) -> string +val hex_bits_32_forwards_matches : bits(32) -> bool +function hex_bits_32_forwards_matches bv = true +val "hex_bits_32_matches_prefix" : string -> option((bits(32), nat)) +val hex_bits_32_backwards_matches : string -> bool +function hex_bits_32_backwards_matches s = match s { + s if match hex_bits_32_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_32_backwards : string -> bits(32) +function hex_bits_32_backwards s = + match hex_bits_32_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc} +val hex_bits_33 : bits(33) <-> string +val hex_bits_33_forwards = "decimal_string_of_bits" : bits(33) -> string +val hex_bits_33_forwards_matches : bits(33) -> bool +function hex_bits_33_forwards_matches bv = true +val "hex_bits_33_matches_prefix" : string -> option((bits(33), nat)) +val hex_bits_33_backwards_matches : string -> bool +function hex_bits_33_backwards_matches s = match s { + s if match hex_bits_33_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_33_backwards : string -> bits(33) +function hex_bits_33_backwards s = + match hex_bits_33_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -/* Ideally these would be sail builtin */ +val hex_bits_48 : bits(48) <-> string +val hex_bits_48_forwards = "decimal_string_of_bits" : bits(48) -> string +val hex_bits_48_forwards_matches : bits(48) -> bool +function hex_bits_48_forwards_matches bv = true +val "hex_bits_48_matches_prefix" : string -> option((bits(48), nat)) +val hex_bits_48_backwards_matches : string -> bool +function hex_bits_48_backwards_matches s = match s { + s if match hex_bits_48_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_48_backwards : string -> bits(48) +function hex_bits_48_backwards s = + match hex_bits_48_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -function shift_right_arith64 (v : bits(64), shift : bits(6)) -> bits(64) = - let v128 : bits(128) = EXTS(v) in - (v128 >> shift)[63..0] +val hex_bits_64 : bits(64) <-> string +val hex_bits_64_forwards = "decimal_string_of_bits" : bits(64) -> string +val hex_bits_64_forwards_matches : bits(64) -> bool +function hex_bits_64_forwards_matches bv = true +val "hex_bits_64_matches_prefix" : string -> option((bits(64), nat)) +val hex_bits_64_backwards_matches : string -> bool +function hex_bits_64_backwards_matches s = match s { + s if match hex_bits_64_matches_prefix(s) { + Some (_, n) if n == string_length(s) => true, + _ => false + } => true, + _ => false +} +val hex_bits_64_backwards : string -> bits(64) +function hex_bits_64_backwards s = + match hex_bits_64_matches_prefix(s) { + Some (bv, n) if n == string_length(s) => bv + } -function shift_right_arith32 (v : bits(32), shift : bits(5)) -> bits(32) = - let v64 : bits(64) = EXTS(v) in - (v64 >> shift)[31..0] /* Special version of zero_extend that the Lem back-end knows will be at a case split on 'm and uses a more generic type for. (Temporary hack, honest) */ diff --git a/src/interpreter.ml b/src/interpreter.ml index 407f512a..e355b6d3 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -266,12 +266,11 @@ let rec build_letchain id lbs (E_aux (_, annot) as exp) = let is_interpreter_extern id env = let open Type_check in - Env.is_extern id env "interpreter" || Env.is_extern id env "ocaml" + Env.is_extern id env "interpreter" let get_interpreter_extern id env = let open Type_check in - try Env.get_extern id env "interpreter" with - | Type_error _ -> Env.get_extern id env "ocaml" + Env.get_extern id env "interpreter" let rec step (E_aux (e_aux, annot) as orig_exp) = let wrap e_aux' = return (E_aux (e_aux', annot)) in diff --git a/src/value.ml b/src/value.ml index 157c16fc..90f6d947 100644 --- a/src/value.ml +++ b/src/value.ml @@ -274,6 +274,10 @@ let value_or_vec = function | [v1; v2] -> mk_vector (Sail_lib.or_vec (coerce_bv v1, coerce_bv v2)) | _ -> failwith "value not_vec" +let value_xor_vec = function + | [v1; v2] -> mk_vector (Sail_lib.xor_vec (coerce_bv v1, coerce_bv v2)) + | _ -> failwith "value xor_vec" + let value_uint = function | [v] -> V_int (Sail_lib.uint (coerce_bv v)) | _ -> failwith "value uint" @@ -407,6 +411,14 @@ let value_shiftr = function | [v1; v2] -> mk_vector (Sail_lib.shiftr (coerce_bv v1, coerce_int v2)) | _ -> failwith "value shiftr" +let value_shift_bits_left = function + | [v1; v2] -> mk_vector (Sail_lib.shift_bits_left (coerce_bv v1, coerce_bv v2)) + | _ -> failwith "value shift_bits_left" + +let value_shift_bits_right = function + | [v1; v2] -> mk_vector (Sail_lib.shift_bits_right (coerce_bv v1, coerce_bv v2)) + | _ -> failwith "value shift_bits_right" + let value_vector_truncate = function | [v1; v2] -> mk_vector (Sail_lib.vector_truncate (coerce_bv v1, coerce_int v2)) | _ -> failwith "value vector_truncate" @@ -498,6 +510,14 @@ let value_round_down = function | [v] -> V_int (Sail_lib.round_down (coerce_real v)) | _ -> failwith "value round_down" +let value_quot_round_zero = function + | [v1; v2] -> V_int (Sail_lib.quot_round_zero (coerce_int v1, coerce_int v2)) + | _ -> failwith "value quot_round_zero" + +let value_rem_round_zero = function + | [v1; v2] -> V_int (Sail_lib.rem_round_zero (coerce_int v1, coerce_int v2)) + | _ -> failwith "value rem_round_zero" + let value_eq_real = function | [v1; v2] -> V_bool (Sail_lib.eq_real (coerce_real v1, coerce_real v2)) | _ -> failwith "value eq_real" @@ -522,6 +542,10 @@ let value_string_append = function | [v1; v2] -> V_string (Sail_lib.string_append (coerce_string v1, coerce_string v2)) | _ -> failwith "value string_append" +let value_decimal_string_of_bits = function + | [v] -> V_string (Sail_lib.decimal_string_of_bits (coerce_bv v)) + | _ -> failwith "value decimal_string_of_bits" + let primops = List.fold_left (fun r (x, y) -> StringMap.add x y r) @@ -536,6 +560,7 @@ let primops = ("putchar", value_putchar); ("string_of_int", fun vs -> V_string (string_of_value (List.hd vs))); ("string_of_bits", fun vs -> V_string (string_of_value (List.hd vs))); + ("decimal_string_of_bits", value_decimal_string_of_bits); ("print_bits", value_print_bits); ("print_int", value_print_int); ("print_string", value_print_string); @@ -568,6 +593,7 @@ let primops = ("not_vec", value_not_vec); ("and_vec", value_and_vec); ("or_vec", value_or_vec); + ("xor_vec", value_xor_vec); ("uint", value_uint); ("sint", value_sint); ("get_slice_int", value_get_slice_int); @@ -579,6 +605,8 @@ let primops = ("zeros", value_zeros); ("shiftr", value_shiftr); ("shiftl", value_shiftl); + ("shift_bits_left", value_shift_bits_left); + ("shift_bits_right", value_shift_bits_right); ("add_int", value_add_int); ("sub_int", value_sub_int); ("div_int", value_quotient); @@ -610,6 +638,8 @@ let primops = ("gteq_real", value_gt_real); ("round_up", value_round_up); ("round_down", value_round_down); + ("quot_round_zero", value_quot_round_zero); + ("rem_round_zero", value_rem_round_zero); ("quotient_real", value_quotient_real); ("undefined_unit", fun _ -> V_unit); ("undefined_bit", fun _ -> V_bit Sail_lib.B0); @@ -625,4 +655,5 @@ let primops = ("string_length", value_string_length); ("string_startswith", value_string_startswith); ("string_drop", value_string_drop); + ("skip", fun _ -> V_unit); ] -- cgit v1.2.3