More monomorphisations for hex_bits_N...

I got bored of this so I wrote a Python script to generate all of them
between 1 and 33, plus 48 and 64. It's in a comment.

We should really get around to making the typechecker work with
polymorphic mappings...

1 files changed, 622 insertions, 7 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