diff options
| -rw-r--r-- | riscv/prelude.sail | 629 | ||||
| -rw-r--r-- | src/sail_lib.ml | 284 |
2 files changed, 842 insertions, 71 deletions
diff --git a/riscv/prelude.sail b/riscv/prelude.sail index 9ecc35a0..10f789e9 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -11,81 +11,703 @@ val def_spc : unit <-> string val hex_bits : forall 'n . (atom('n), bits('n)) <-> string +val string_startswith = "string_startswith" : (string, string) -> bool +val string_drop = "string_drop" : (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) + +/* Python: +f = """val hex_bits_{0} : bits({0}) <-> string +val hex_bits_{0}_forwards = "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 + }} +""" + +for i in list(range(1, 34)) + [48, 64]: + print(f.format(i)) + +*/ +val hex_bits_1 : bits(1) <-> string +val hex_bits_1_forwards = "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 hex_bits_2 : bits(2) <-> string +val hex_bits_2_forwards = "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 hex_bits_3 : bits(3) <-> string val hex_bits_3_forwards = "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 hex_bits_4 : bits(4) <-> string val hex_bits_4_forwards = "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 hex_bits_5 : bits(5) <-> string val hex_bits_5_forwards = "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 hex_bits_6 : bits(6) <-> string val hex_bits_6_forwards = "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 hex_bits_7 : bits(7) <-> string val hex_bits_7_forwards = "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 hex_bits_8 : bits(8) <-> string val hex_bits_8_forwards = "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 hex_bits_9 : bits(9) <-> string val hex_bits_9_forwards = "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 hex_bits_10 : bits(10) <-> string val hex_bits_10_forwards = "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 hex_bits_11 : bits(11) <-> string val hex_bits_11_forwards = "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 hex_bits_12 : bits(12) <-> string val hex_bits_12_forwards = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 = "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 spc_forwards : unit -> string @@ -122,13 +744,6 @@ val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit 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 string_startswith = "string_startswith" : (string, string) -> bool -val string_drop = "string_drop" : (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_real = {ocaml: "eq_real", lem: "eq"} : (real, real) -> bool diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 09a90ba9..c04d469c 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -701,24 +701,39 @@ let spc_matches_prefix s = | 0 -> ZNone () | n -> ZSome ((), Big_int.of_int n) -let hex_bits_1_matches_prefix s = +(* Python: +f = """let hex_bits_{0}_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 2 then - ZSome ((bits_of_int 1 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 {0}) then + ZSome ((bits_of_big_int {0} n, len)) else ZNone () +""" + +for i in list(range(1, 34)) + [48, 64]: + print(f.format(i)) +*) +let hex_bits_1_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 1) then + ZSome ((bits_of_big_int 1 n, len)) + else + ZNone () let hex_bits_2_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 4 then - ZSome ((bits_of_int 2 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 2) then + ZSome ((bits_of_big_int 2 n, len)) else ZNone () @@ -726,9 +741,9 @@ let hex_bits_3_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 8 then - ZSome ((bits_of_int 4 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 3) then + ZSome ((bits_of_big_int 3 n, len)) else ZNone () @@ -736,9 +751,9 @@ let hex_bits_4_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 16 then - ZSome ((bits_of_int 8 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 4) then + ZSome ((bits_of_big_int 4 n, len)) else ZNone () @@ -746,9 +761,9 @@ let hex_bits_5_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 32 then - ZSome ((bits_of_int 16 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 5) then + ZSome ((bits_of_big_int 5 n, len)) else ZNone () @@ -756,9 +771,9 @@ let hex_bits_6_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 64 then - ZSome ((bits_of_int 32 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 6) then + ZSome ((bits_of_big_int 6 n, len)) else ZNone () @@ -766,9 +781,9 @@ let hex_bits_7_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 128 then - ZSome ((bits_of_int 64 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 7) then + ZSome ((bits_of_big_int 7 n, len)) else ZNone () @@ -776,9 +791,9 @@ let hex_bits_8_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 256 then - ZSome ((bits_of_int 128 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 8) then + ZSome ((bits_of_big_int 8 n, len)) else ZNone () @@ -786,9 +801,9 @@ let hex_bits_9_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 512 then - ZSome ((bits_of_int 256 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 9) then + ZSome ((bits_of_big_int 9 n, len)) else ZNone () @@ -796,9 +811,9 @@ let hex_bits_10_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 1024 then - ZSome ((bits_of_int 512 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 10) then + ZSome ((bits_of_big_int 10 n, len)) else ZNone () @@ -806,9 +821,9 @@ let hex_bits_11_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 2048 then - ZSome ((bits_of_int 1024 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 11) then + ZSome ((bits_of_big_int 11 n, len)) else ZNone () @@ -816,9 +831,9 @@ let hex_bits_12_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 4096 then - ZSome ((bits_of_int 2048 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 12) then + ZSome ((bits_of_big_int 12 n, len)) else ZNone () @@ -826,9 +841,9 @@ let hex_bits_13_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 8192 then - ZSome ((bits_of_int 4096 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 13) then + ZSome ((bits_of_big_int 13 n, len)) else ZNone () @@ -836,9 +851,9 @@ let hex_bits_14_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 16384 then - ZSome ((bits_of_int 8192 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 14) then + ZSome ((bits_of_big_int 14 n, len)) else ZNone () @@ -846,9 +861,9 @@ let hex_bits_15_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 32768 then - ZSome ((bits_of_int 16384 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 15) then + ZSome ((bits_of_big_int 15 n, len)) else ZNone () @@ -856,9 +871,39 @@ let hex_bits_16_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 65536 then - ZSome ((bits_of_int 32768 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 16) then + ZSome ((bits_of_big_int 16 n, len)) + else + ZNone () + +let hex_bits_17_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 17) then + ZSome ((bits_of_big_int 17 n, len)) + else + ZNone () + +let hex_bits_18_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 18) then + ZSome ((bits_of_big_int 18 n, len)) + else + ZNone () + +let hex_bits_19_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 19) then + ZSome ((bits_of_big_int 19 n, len)) else ZNone () @@ -866,9 +911,9 @@ let hex_bits_20_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 1048576 then - ZSome ((bits_of_int 524288 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 20) then + ZSome ((bits_of_big_int 20 n, len)) else ZNone () @@ -876,9 +921,69 @@ let hex_bits_21_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 2097152 then - ZSome ((bits_of_int 1048576 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 21) then + ZSome ((bits_of_big_int 21 n, len)) + else + ZNone () + +let hex_bits_22_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 22) then + ZSome ((bits_of_big_int 22 n, len)) + else + ZNone () + +let hex_bits_23_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 23) then + ZSome ((bits_of_big_int 23 n, len)) + else + ZNone () + +let hex_bits_24_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 24) then + ZSome ((bits_of_big_int 24 n, len)) + else + ZNone () + +let hex_bits_25_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 25) then + ZSome ((bits_of_big_int 25 n, len)) + else + ZNone () + +let hex_bits_26_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 26) then + ZSome ((bits_of_big_int 26 n, len)) + else + ZNone () + +let hex_bits_27_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 27) then + ZSome ((bits_of_big_int 27 n, len)) else ZNone () @@ -886,9 +991,39 @@ let hex_bits_28_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 268435456 then - ZSome ((bits_of_int 134217728 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 28) then + ZSome ((bits_of_big_int 28 n, len)) + else + ZNone () + +let hex_bits_29_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 29) then + ZSome ((bits_of_big_int 29 n, len)) + else + ZNone () + +let hex_bits_30_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 30) then + ZSome ((bits_of_big_int 30 n, len)) + else + ZNone () + +let hex_bits_31_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 31) then + ZSome ((bits_of_big_int 31 n, len)) else ZNone () @@ -896,9 +1031,9 @@ let hex_bits_32_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 4294967296 then - ZSome ((bits_of_int 2147483648 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 32) then + ZSome ((bits_of_big_int 32 n, len)) else ZNone () @@ -906,12 +1041,33 @@ let hex_bits_33_matches_prefix s = match maybe_int_of_prefix s with | ZNone () -> ZNone () | ZSome (n, len) -> - let n = Big_int.to_int n in - if 0 <= n && n < 8589934592 then - ZSome ((bits_of_int 4294967296 n, len)) + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 33) then + ZSome ((bits_of_big_int 33 n, len)) else ZNone () +let hex_bits_48_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 48) then + ZSome ((bits_of_big_int 48 n, len)) + else + ZNone () + +let hex_bits_64_matches_prefix s = + match maybe_int_of_prefix s with + | ZNone () -> ZNone () + | ZSome (n, len) -> + if Big_int.less_equal Big_int.zero n + && Big_int.less n (Big_int.pow_int_positive 2 64) then + ZSome ((bits_of_big_int 64 n, len)) + else + ZNone () + + let string_of_bool = function | true -> "true" | false -> "false" |