path: root/model/prelude_mapping.sail

/*=======================================================================================*/
/*  RISCV Sail Model                                                                     */
/*                                                                                       */
/*  This Sail RISC-V architecture model, comprising all files and                        */
/*  directories except for the snapshots of the Lem and Sail libraries                   */
/*  in the prover_snapshots directory (which include copies of their                     */
/*  licences), is subject to the BSD two-clause licence below.                           */
/*                                                                                       */
/*  Copyright (c) 2017-2023                                                              */
/*    Prashanth Mundkur                                                                  */
/*    Rishiyur S. Nikhil and Bluespec, Inc.                                              */
/*    Jon French                                                                         */
/*    Brian Campbell                                                                     */
/*    Robert Norton-Wright                                                               */
/*    Alasdair Armstrong                                                                 */
/*    Thomas Bauereiss                                                                   */
/*    Shaked Flur                                                                        */
/*    Christopher Pulte                                                                  */
/*    Peter Sewell                                                                       */
/*    Alexander Richardson                                                               */
/*    Hesham Almatary                                                                    */
/*    Jessica Clarke                                                                     */
/*    Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo  */
/*    Peter Rugg                                                                         */
/*    Aril Computer Corp., for contributions by Scott Johnson                            */
/*    Philipp Tomsich                                                                    */
/*    VRULL GmbH, for contributions by its employees                                     */
/*                                                                                       */
/*  All rights reserved.                                                                 */
/*                                                                                       */
/*  This software was developed by the above within the Rigorous                         */
/*  Engineering of Mainstream Systems (REMS) project, partly funded by                   */
/*  EPSRC grant EP/K008528/1, at the Universities of Cambridge and                       */
/*  Edinburgh.                                                                           */
/*                                                                                       */
/*  This software was developed by SRI International and the University of               */
/*  Cambridge Computer Laboratory (Department of Computer Science and                    */
/*  Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and                 */
/*  under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA                 */
/*  SSITH research programme.                                                            */
/*                                                                                       */
/*  This project has received funding from the European Research Council                 */
/*  (ERC) under the European Union’s Horizon 2020 research and innovation                */
/*  programme (grant agreement 789108, ELVER).                                           */
/*                                                                                       */
/*                                                                                       */
/*  Redistribution and use in source and binary forms, with or without                   */
/*  modification, are permitted provided that the following conditions                   */
/*  are met:                                                                             */
/*  1. Redistributions of source code must retain the above copyright                    */
/*     notice, this list of conditions and the following disclaimer.                     */
/*  2. Redistributions in binary form must reproduce the above copyright                 */
/*     notice, this list of conditions and the following disclaimer in                   */
/*     the documentation and/or other materials provided with the                        */
/*     distribution.                                                                     */
/*                                                                                       */
/*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''                   */
/*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED                    */
/*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A                      */
/*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR                  */
/*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,                         */
/*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT                     */
/*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF                     */
/*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND                  */
/*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,                   */
/*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT                   */
/*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF                   */
/*  SUCH DAMAGE.                                                                         */
/*=======================================================================================*/

/* Some helper functions for the assembler mappings. */

/* These mappings produce a lot of pattern match warnings that are not useful.
   The following directive suppresses them (and will be ignored by older versions of Sail
   with one additional warning). Would be better to fix the warnings properly but I don't
   know how. */
$suppress_warnings

/* 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
  }}
"""

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 = "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 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 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 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 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 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 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 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 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 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 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 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
// XXX TODO the following builtin does not exist (at least for C backend) so I have
// substituted a dummy one that always returns None. This means that assembly_backwards
// (i.e. string -> ast) might not work but we don't actually use that for anything.
//val "hex_bits_12_matches_prefix" : string -> option((bits(12), nat))
function hex_bits_12_matches_prefix (s : string) -> option((bits(12), nat)) = None()
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
  }