Simplify prelude.sail by including generic_equality.sail and mapping.sail

This change includes `generic_equality.sail` and `mapping.sail` from the Sail standard library which defines a lot of things that were defined in `prelude.sail`.

I also removed `reg_deref` which is no longer required.

The `mapping.sail` and `hex_bits.sail` files are in Sail 0.18 which is not yet released, so they have been temporarily copied here.

7 files changed, 268 insertions, 863 deletions

diff --git a/Makefile b/Makefile
index be4339d..2552241 100644
--- a/Makefile
+++ b/Makefile
@@ -82,7 +82,7 @@ SAIL_VM_SRCS += $(SAIL_RV64_VM_SRCS)
 endif
 
 # Non-instruction sources
-PRELUDE = prelude.sail prelude_mapping.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail
+PRELUDE = prelude.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.sail
 
 SAIL_REGS_SRCS = riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail
 SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail
diff --git a/model/hex_bits.sail b/model/hex_bits.sail
new file mode 100644
index 0000000..81e25e1
--- /dev/null
+++ b/model/hex_bits.sail
@@ -0,0 +1,124 @@
+// Note: This file is temporarily copied here from the Sail compiler. It can
+// be removed when Sail 0.18 is released.
+
+/*==========================================================================*/
+/*     Sail                                                                 */
+/*                                                                          */
+/*  Sail and the Sail architecture models here, comprising all files and    */
+/*  directories except the ASL-derived Sail code in the aarch64 directory,  */
+/*  are subject to the BSD two-clause licence below.                        */
+/*                                                                          */
+/*  The ASL derived parts of the ARMv8.3 specification in                   */
+/*  aarch64/no_vector and aarch64/full are copyright ARM Ltd.               */
+/*                                                                          */
+/*  Copyright (c) 2013-2021                                                 */
+/*    Kathyrn Gray                                                          */
+/*    Shaked Flur                                                           */
+/*    Stephen Kell                                                          */
+/*    Gabriel Kerneis                                                       */
+/*    Robert Norton-Wright                                                  */
+/*    Christopher Pulte                                                     */
+/*    Peter Sewell                                                          */
+/*    Alasdair Armstrong                                                    */
+/*    Brian Campbell                                                        */
+/*    Thomas Bauereiss                                                      */
+/*    Anthony Fox                                                           */
+/*    Jon French                                                            */
+/*    Dominic Mulligan                                                      */
+/*    Stephen Kell                                                          */
+/*    Mark Wassell                                                          */
+/*    Alastair Reid (Arm Ltd)                                               */
+/*                                                                          */
+/*  All rights reserved.                                                    */
+/*                                                                          */
+/*  This work was partially supported by EPSRC grant EP/K008528/1 <a        */
+/*  href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous          */
+/*  Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA   */
+/*  KTF funding, and donations from Arm.  This project has received         */
+/*  funding from the European Research Council (ERC) under the European     */
+/*  Union’s Horizon 2020 research and innovation programme (grant           */
+/*  agreement No 789108, ELVER).                                            */
+/*                                                                          */
+/*  This software was developed by SRI International and the University of  */
+/*  Cambridge Computer Laboratory (Department of Computer Science and       */
+/*  Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV")        */
+/*  and FA8750-10-C-0237 ("CTSRD").                                         */
+/*                                                                          */
+/*  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.                                                            */
+/*==========================================================================*/
+
+$ifndef _HEX_BITS
+$define _HEX_BITS
+
+$include <vector.sail>
+$include <string.sail>
+
+val "parse_hex_bits" : forall 'n, 'n > 0. (int('n), string) -> bits('n)
+val "valid_hex_bits" : forall 'n, 'n > 0. (int('n), string) -> bool
+
+val hex_bits : forall 'n, 'n > 0. bits('n) <-> (int('n), string)
+
+function hex_bits_forwards(bv) = (length(bv), hex_str(unsigned(bv)))
+function hex_bits_forwards_matches(bv) = true
+
+function hex_bits_backwards(n, str) = parse_hex_bits(n, str)
+function hex_bits_backwards_matches(n, str) = valid_hex_bits(n, str)
+
+mapping hex_bits_1 : bits(1) <-> string = { hex_bits(1, s) <-> s }
+mapping hex_bits_2 : bits(2) <-> string = { hex_bits(2, s) <-> s }
+mapping hex_bits_3 : bits(3) <-> string = { hex_bits(3, s) <-> s }
+mapping hex_bits_4 : bits(4) <-> string = { hex_bits(4, s) <-> s }
+mapping hex_bits_5 : bits(5) <-> string = { hex_bits(5, s) <-> s }
+mapping hex_bits_6 : bits(6) <-> string = { hex_bits(6, s) <-> s }
+mapping hex_bits_7 : bits(7) <-> string = { hex_bits(7, s) <-> s }
+mapping hex_bits_8 : bits(8) <-> string = { hex_bits(8, s) <-> s }
+mapping hex_bits_9 : bits(9) <-> string = { hex_bits(9, s) <-> s }
+
+mapping hex_bits_10 : bits(10) <-> string = { hex_bits(10, s) <-> s }
+mapping hex_bits_11 : bits(11) <-> string = { hex_bits(11, s) <-> s }
+mapping hex_bits_12 : bits(12) <-> string = { hex_bits(12, s) <-> s }
+mapping hex_bits_13 : bits(13) <-> string = { hex_bits(13, s) <-> s }
+mapping hex_bits_14 : bits(14) <-> string = { hex_bits(14, s) <-> s }
+mapping hex_bits_15 : bits(15) <-> string = { hex_bits(15, s) <-> s }
+mapping hex_bits_16 : bits(16) <-> string = { hex_bits(16, s) <-> s }
+mapping hex_bits_17 : bits(17) <-> string = { hex_bits(17, s) <-> s }
+mapping hex_bits_18 : bits(18) <-> string = { hex_bits(18, s) <-> s }
+mapping hex_bits_19 : bits(19) <-> string = { hex_bits(19, s) <-> s }
+
+mapping hex_bits_20 : bits(20) <-> string = { hex_bits(20, s) <-> s }
+mapping hex_bits_21 : bits(21) <-> string = { hex_bits(21, s) <-> s }
+mapping hex_bits_22 : bits(22) <-> string = { hex_bits(22, s) <-> s }
+mapping hex_bits_23 : bits(23) <-> string = { hex_bits(23, s) <-> s }
+mapping hex_bits_24 : bits(24) <-> string = { hex_bits(24, s) <-> s }
+mapping hex_bits_25 : bits(25) <-> string = { hex_bits(25, s) <-> s }
+mapping hex_bits_26 : bits(26) <-> string = { hex_bits(26, s) <-> s }
+mapping hex_bits_27 : bits(27) <-> string = { hex_bits(27, s) <-> s }
+mapping hex_bits_28 : bits(28) <-> string = { hex_bits(28, s) <-> s }
+mapping hex_bits_29 : bits(29) <-> string = { hex_bits(29, s) <-> s }
+
+mapping hex_bits_30 : bits(30) <-> string = { hex_bits(30, s) <-> s }
+mapping hex_bits_31 : bits(31) <-> string = { hex_bits(31, s) <-> s }
+mapping hex_bits_32 : bits(32) <-> string = { hex_bits(32, s) <-> s }
+
+$endif _HEX_BITS
diff --git a/model/mapping.sail b/model/mapping.sail
new file mode 100644
index 0000000..ec8b759
--- /dev/null
+++ b/model/mapping.sail
@@ -0,0 +1,136 @@
+// Note: This file is temporarily copied here from the Sail compiler. It can
+// be removed when Sail 0.18 is released.
+
+/*==========================================================================*/
+/*     Sail                                                                 */
+/*                                                                          */
+/*  Sail and the Sail architecture models here, comprising all files and    */
+/*  directories except the ASL-derived Sail code in the aarch64 directory,  */
+/*  are subject to the BSD two-clause licence below.                        */
+/*                                                                          */
+/*  The ASL derived parts of the ARMv8.3 specification in                   */
+/*  aarch64/no_vector and aarch64/full are copyright ARM Ltd.               */
+/*                                                                          */
+/*  Copyright (c) 2013-2021                                                 */
+/*    Kathyrn Gray                                                          */
+/*    Shaked Flur                                                           */
+/*    Stephen Kell                                                          */
+/*    Gabriel Kerneis                                                       */
+/*    Robert Norton-Wright                                                  */
+/*    Christopher Pulte                                                     */
+/*    Peter Sewell                                                          */
+/*    Alasdair Armstrong                                                    */
+/*    Brian Campbell                                                        */
+/*    Thomas Bauereiss                                                      */
+/*    Anthony Fox                                                           */
+/*    Jon French                                                            */
+/*    Dominic Mulligan                                                      */
+/*    Stephen Kell                                                          */
+/*    Mark Wassell                                                          */
+/*    Alastair Reid (Arm Ltd)                                               */
+/*                                                                          */
+/*  All rights reserved.                                                    */
+/*                                                                          */
+/*  This work was partially supported by EPSRC grant EP/K008528/1 <a        */
+/*  href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous          */
+/*  Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA   */
+/*  KTF funding, and donations from Arm.  This project has received         */
+/*  funding from the European Research Council (ERC) under the European     */
+/*  Union’s Horizon 2020 research and innovation programme (grant           */
+/*  agreement No 789108, ELVER).                                            */
+/*                                                                          */
+/*  This software was developed by SRI International and the University of  */
+/*  Cambridge Computer Laboratory (Department of Computer Science and       */
+/*  Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV")        */
+/*  and FA8750-10-C-0237 ("CTSRD").                                         */
+/*                                                                          */
+/*  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.                                                            */
+/*==========================================================================*/
+
+$ifndef _MAPPING
+$define _MAPPING
+
+$include <arith.sail>
+$include <option.sail>
+
+val string_take = pure "string_take" : (string, nat) -> string
+val string_drop = pure "string_drop" : (string, nat) -> string
+val string_length = pure "string_length" : string -> nat
+val string_append = pure {coq: "String.append", c: "concat_str", _: "string_append"} : (string, string) -> string
+val string_startswith = pure "string_startswith" : (string, string) -> bool
+
+val n_leading_spaces = pure { coq: "n_leading_spaces_Z" } : string -> nat
+function n_leading_spaces s =
+  match s {
+    "" => 0,
+    _ => match string_take(s, 1) {
+      " " => 1 + n_leading_spaces(string_drop(s, 1)),
+      _ => 0
+    }
+  }
+
+/*!
+In a string mapping this is treated as `[ ]+`, i.e one or more space
+characters. It is printed as a single space `" "`.
+*/
+val spc : unit <-> string
+
+function spc_forwards() = " "
+function spc_forwards_matches() = true
+
+function spc_backwards _ = ()
+function spc_backwards_matches s = {
+  let len = string_length(s);
+  n_leading_spaces(s) == len & len > 0
+}
+
+/*!
+In a string mapping this is treated as `[ ]*`, i.e. zero or more space
+characters. It is printed as the empty string.
+*/
+val opt_spc : unit <-> string
+
+function opt_spc_forwards() = ""
+function opt_spc_forwards_matches() = true
+
+function opt_spc_backwards _ = ()
+function opt_spc_backwards_matches s = n_leading_spaces(s) == string_length(s)
+
+/*!
+Like `opt_spc`, in a string mapping this is treated as `[ ]*`, i.e. zero or more space
+characters. It differs however in that it is printed as a single space `" "`.
+*/
+val def_spc : unit <-> string
+
+function def_spc_forwards() = " "
+function def_spc_forwards_matches() = true
+
+function def_spc_backwards _ = ()
+function def_spc_backwards_matches s = n_leading_spaces(s) == string_length(s)
+
+mapping sep : unit <-> string = {
+  () <-> opt_spc() ^ "," ^ def_spc()
+}
+
+$endif
diff --git a/model/prelude.sail b/model/prelude.sail
index 6b5e46c..c5eb94f 100644
--- a/model/prelude.sail
+++ b/model/prelude.sail
@@ -74,53 +74,21 @@ $include <smt.sail>
 $include <option.sail>
 $include <arith.sail>
 $include <string.sail>
+$include "mapping.sail"
 $include <vector_dec.sail>
 $include <regfp.sail>
+$include <generic_equality.sail>
+$include "hex_bits.sail"
 
-val string_startswith = "string_startswith" : (string, string) -> bool
-val string_drop = "string_drop" : (string, nat) -> string
-val string_take = "string_take" : (string, nat) -> string
-val string_length = "string_length" : string -> nat
-val string_append = {c: "concat_str", _: "string_append"} : (string, string) -> string
-
-val eq_anything = {ocaml: "(fun (x, y) -> x = y)", interpreter: "eq_anything", lem: "eq", coq: "generic_eq", c: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
-
-overload operator == = {eq_string, eq_anything}
-
-val "reg_deref" : forall ('a : Type). register('a) -> 'a
-/* sneaky deref with no effect necessary for bitfield writes */
-val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
-
-val any_vector_update = {ocaml: "update", lem: "update_list_dec", coq: "vector_update"} : forall 'n ('a : Type).
-  (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
-
-overload vector_update = {any_vector_update}
-
-val update_subrange = {ocaml: "update_subrange", interpreter: "update_subrange", lem: "update_subrange_vec_dec", coq: "update_subrange_vec_dec"} : forall 'n 'm 'o.
-  (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
-
-val vector_concat = {ocaml: "append", lem: "append_list", coq: "vec_concat"} : forall ('n : Int) ('m : Int) ('a : Type).
-  (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
-
-overload append = {vector_concat}
 
 val not_bit : bit -> bit
-
 function not_bit(b) = if b == bitone then bitzero else bitone
 
 overload ~ = {not_bool, not_vec, not_bit}
 
-val not = pure {coq: "negb", _: "not"} : forall ('p : Bool). bool('p) -> bool(not('p))
-
-val neq_vec = {lem: "neq"} : forall 'n. (bits('n), bits('n)) -> bool
-
-function neq_vec (x, y) = not_bool(eq_bits(x, y))
-
-val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
-
-function neq_anything (x, y) = not_bool(x == y)
-
-overload operator != = {neq_vec, neq_anything}
+// not_bool alias.
+val not : forall ('p : Bool). bool('p) -> bool(not('p))
+function not(b) = not_bool(b)
 
 overload operator & = {and_vec}
 
@@ -284,53 +252,6 @@ function reverse_bits_in_byte (xs : bits(8)) -> bits(8) = {
 
 overload reverse = {reverse_bits_in_byte}
 
-/* helpers for mappings */
-
-val spc : unit <-> string
-val opt_spc : unit <-> string
-val def_spc : unit <-> string
-
-val "decimal_string_of_bits" : forall 'n. bits('n) -> string
-val hex_bits : forall 'n . (atom('n), bits('n)) <-> string
-
-val n_leading_spaces : string -> nat
-function n_leading_spaces s =
-  match s {
-    "" => 0,
-    _ => match string_take(s, 1) {
-      " " => 1 + n_leading_spaces(string_drop(s, 1)),
-      _ => 0
-    }
-  }
-
-val spc_forwards : unit -> string
-function spc_forwards () = " "
-val spc_backwards : string -> unit
-function spc_backwards s = ()
-val spc_matches_prefix : string -> option((unit, nat))
-function spc_matches_prefix s = {
-  let n = n_leading_spaces(s);
-  match n {
-    0 => None(),
-    _ => Some((), n)
-  }
-}
-
-val opt_spc_forwards : unit -> string
-function opt_spc_forwards () = ""
-val opt_spc_backwards : string -> unit
-function opt_spc_backwards s = ()
-val opt_spc_matches_prefix : string -> option((unit, nat))
-function opt_spc_matches_prefix s =
-  Some((), n_leading_spaces(s))
-
-val def_spc_forwards : unit -> string
-function def_spc_forwards () = " "
-val def_spc_backwards : string -> unit
-function def_spc_backwards s = ()
-val def_spc_matches_prefix : string -> option((unit, nat))
-function def_spc_matches_prefix s = opt_spc_matches_prefix(s)
-
 overload operator / = {quot_round_zero}
 overload operator * = {mult_atom, mult_int}
 
diff --git a/model/prelude_mapping.sail b/model/prelude_mapping.sail
deleted file mode 100644
index ff449d1..0000000
--- a/model/prelude_mapping.sail
+++ /dev/null
@@ -1,771 +0,0 @@
-/*=======================================================================================*/
-/*  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
-  }
diff --git a/model/riscv_types.sail b/model/riscv_types.sail
index b940286..14916c7 100644
--- a/model/riscv_types.sail
+++ b/model/riscv_types.sail
@@ -419,11 +419,6 @@ enum extop_zbb = {RISCV_SEXTB, RISCV_SEXTH, RISCV_ZEXTH}
 
 enum zicondop = {RISCV_CZERO_EQZ, RISCV_CZERO_NEZ}
 
-val sep : unit <-> string
-mapping sep : unit <-> string = {
-  ()     <-> opt_spc() ^ "," ^ def_spc()
-}
-
 mapping bool_bits : bool <-> bits(1) = {
   true   <-> 0b1,
   false  <-> 0b0
diff --git a/sail-riscv.install b/sail-riscv.install
index 5a83673..7a539df 100644
--- a/sail-riscv.install
+++ b/sail-riscv.install
@@ -1,2 +1,2 @@
 bin: ["c_emulator/riscv_sim_RV64" "c_emulator/riscv_sim_RV32"]
-share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mapping.sail" {"model/prelude_mapping.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ]
+share: [ "model/main.sail" {"model/main.sail"} "model/prelude.sail" {"model/prelude.sail"} "model/prelude_mem.sail" {"model/prelude_mem.sail"} "model/prelude_mem_metadata.sail" {"model/prelude_mem_metadata.sail"} "model/riscv_addr_checks.sail" {"model/riscv_addr_checks.sail"} "model/riscv_addr_checks_common.sail" {"model/riscv_addr_checks_common.sail"} "model/riscv_analysis.sail" {"model/riscv_analysis.sail"} "model/riscv_csr_ext.sail" {"model/riscv_csr_ext.sail"} "model/riscv_csr_map.sail" {"model/riscv_csr_map.sail"} "model/riscv_decode_ext.sail" {"model/riscv_decode_ext.sail"} "model/riscv_ext_regs.sail" {"model/riscv_ext_regs.sail"} "model/riscv_fdext_control.sail" {"model/riscv_fdext_control.sail"} "model/riscv_fdext_regs.sail" {"model/riscv_fdext_regs.sail"} "model/riscv_fetch.sail" {"model/riscv_fetch.sail"} "model/riscv_fetch_rvfi.sail" {"model/riscv_fetch_rvfi.sail"} "model/riscv_flen_D.sail" {"model/riscv_flen_D.sail"} "model/riscv_flen_F.sail" {"model/riscv_flen_F.sail"} "model/riscv_freg_type.sail" {"model/riscv_freg_type.sail"} "model/riscv_insts_aext.sail" {"model/riscv_insts_aext.sail"} "model/riscv_insts_base.sail" {"model/riscv_insts_base.sail"} "model/riscv_insts_begin.sail" {"model/riscv_insts_begin.sail"} "model/riscv_insts_cdext.sail" {"model/riscv_insts_cdext.sail"} "model/riscv_insts_cext.sail" {"model/riscv_insts_cext.sail"} "model/riscv_insts_cfext.sail" {"model/riscv_insts_cfext.sail"} "model/riscv_insts_dext.sail" {"model/riscv_insts_dext.sail"} "model/riscv_insts_end.sail" {"model/riscv_insts_end.sail"} "model/riscv_insts_fext.sail" {"model/riscv_insts_fext.sail"} "model/riscv_insts_hints.sail" {"model/riscv_insts_hints.sail"} "model/riscv_insts_mext.sail" {"model/riscv_insts_mext.sail"} "model/riscv_insts_next.sail" {"model/riscv_insts_next.sail"} "model/riscv_insts_rmem.sail" {"model/riscv_insts_rmem.sail"} "model/riscv_insts_zba.sail" {"model/riscv_insts_zba.sail"} "model/riscv_insts_zbb.sail" {"model/riscv_insts_zbb.sail"} "model/riscv_insts_zbc.sail" {"model/riscv_insts_zbc.sail"} "model/riscv_insts_zbkb.sail" {"model/riscv_insts_zbkb.sail"} "model/riscv_insts_zbkx.sail" {"model/riscv_insts_zbkx.sail"} "model/riscv_insts_zbs.sail" {"model/riscv_insts_zbs.sail"} "model/riscv_insts_zfh.sail" {"model/riscv_insts_zfh.sail"} "model/riscv_insts_zicsr.sail" {"model/riscv_insts_zicsr.sail"} "model/riscv_insts_zkn.sail" {"model/riscv_insts_zkn.sail"} "model/riscv_insts_zks.sail" {"model/riscv_insts_zks.sail"} "model/riscv_jalr_rmem.sail" {"model/riscv_jalr_rmem.sail"} "model/riscv_jalr_seq.sail" {"model/riscv_jalr_seq.sail"} "model/riscv_mem.sail" {"model/riscv_mem.sail"} "model/riscv_misa_ext.sail" {"model/riscv_misa_ext.sail"} "model/riscv_next_control.sail" {"model/riscv_next_control.sail"} "model/riscv_next_regs.sail" {"model/riscv_next_regs.sail"} "model/riscv_pc_access.sail" {"model/riscv_pc_access.sail"} "model/riscv_platform.sail" {"model/riscv_platform.sail"} "model/riscv_pmp_control.sail" {"model/riscv_pmp_control.sail"} "model/riscv_pmp_regs.sail" {"model/riscv_pmp_regs.sail"} "model/riscv_pte.sail" {"model/riscv_pte.sail"} "model/riscv_ptw.sail" {"model/riscv_ptw.sail"} "model/riscv_reg_type.sail" {"model/riscv_reg_type.sail"} "model/riscv_regs.sail" {"model/riscv_regs.sail"} "model/riscv_softfloat_interface.sail" {"model/riscv_softfloat_interface.sail"} "model/riscv_step.sail" {"model/riscv_step.sail"} "model/riscv_step_common.sail" {"model/riscv_step_common.sail"} "model/riscv_step_ext.sail" {"model/riscv_step_ext.sail"} "model/riscv_step_rvfi.sail" {"model/riscv_step_rvfi.sail"} "model/riscv_sync_exception.sail" {"model/riscv_sync_exception.sail"} "model/riscv_sys_control.sail" {"model/riscv_sys_control.sail"} "model/riscv_sys_exceptions.sail" {"model/riscv_sys_exceptions.sail"} "model/riscv_sys_regs.sail" {"model/riscv_sys_regs.sail"} "model/riscv_termination_common.sail" {"model/riscv_termination_common.sail"} "model/riscv_termination_rv32.sail" {"model/riscv_termination_rv32.sail"} "model/riscv_termination_rv64.sail" {"model/riscv_termination_rv64.sail"} "model/riscv_types.sail" {"model/riscv_types.sail"} "model/riscv_types_common.sail" {"model/riscv_types_common.sail"} "model/riscv_types_ext.sail" {"model/riscv_types_ext.sail"} "model/riscv_types_kext.sail" {"model/riscv_types_kext.sail"} "model/riscv_vmem_common.sail" {"model/riscv_vmem_common.sail"} "model/riscv_vmem_rv32.sail" {"model/riscv_vmem_rv32.sail"} "model/riscv_vmem_rv64.sail" {"model/riscv_vmem_rv64.sail"} "model/riscv_vmem_sv32.sail" {"model/riscv_vmem_sv32.sail"} "model/riscv_vmem_sv39.sail" {"model/riscv_vmem_sv39.sail"} "model/riscv_vmem_sv48.sail" {"model/riscv_vmem_sv48.sail"} "model/riscv_vmem_tlb.sail" {"model/riscv_vmem_tlb.sail"} "model/riscv_vmem_types.sail" {"model/riscv_vmem_types.sail"} "model/riscv_xlen32.sail" {"model/riscv_xlen32.sail"} "model/riscv_xlen64.sail" {"model/riscv_xlen64.sail"} "model/rvfi_dii.sail" {"model/rvfi_dii.sail"} "c_emulator/riscv_platform.c" {"c_emulator/riscv_platform.c"} "c_emulator/riscv_platform_impl.c" {"c_emulator/riscv_platform_impl.c"} "c_emulator/riscv_prelude.c" {"c_emulator/riscv_prelude.c"} "c_emulator/riscv_sim.c" {"c_emulator/riscv_sim.c"} "c_emulator/riscv_softfloat.c" {"c_emulator/riscv_softfloat.c"} "c_emulator/riscv_config.h" {"c_emulator/riscv_config.h"} "c_emulator/riscv_platform.h" {"c_emulator/riscv_platform.h"} "c_emulator/riscv_platform_impl.h" {"c_emulator/riscv_platform_impl.h"} "c_emulator/riscv_prelude.h" {"c_emulator/riscv_prelude.h"} "c_emulator/riscv_sail.h" {"c_emulator/riscv_sail.h"} "c_emulator/riscv_softfloat.h" {"c_emulator/riscv_softfloat.h"} "handwritten_support/mem_metadata.lem" {"handwritten_support/mem_metadata.lem"} "handwritten_support/riscv_extras.lem" {"handwritten_support/riscv_extras.lem"} "handwritten_support/riscv_extras_fdext.lem" {"handwritten_support/riscv_extras_fdext.lem"} "handwritten_support/riscv_extras_sequential.lem" {"handwritten_support/riscv_extras_sequential.lem"} "handwritten_support/hgen/ast.hgen" {"handwritten_support/hgen/ast.hgen"} "handwritten_support/hgen/fold.hgen" {"handwritten_support/hgen/fold.hgen"} "handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen" {"handwritten_support/hgen/herdtools_ast_to_shallow_ast.hgen"} "handwritten_support/hgen/herdtools_types_to_shallow_types.hgen" {"handwritten_support/hgen/herdtools_types_to_shallow_types.hgen"} "handwritten_support/hgen/lexer.hgen" {"handwritten_support/hgen/lexer.hgen"} "handwritten_support/hgen/lexer_regexps.hgen" {"handwritten_support/hgen/lexer_regexps.hgen"} "handwritten_support/hgen/map.hgen" {"handwritten_support/hgen/map.hgen"} "handwritten_support/hgen/parser.hgen" {"handwritten_support/hgen/parser.hgen"} "handwritten_support/hgen/pretty.hgen" {"handwritten_support/hgen/pretty.hgen"} "handwritten_support/hgen/pretty_xml.hgen" {"handwritten_support/hgen/pretty_xml.hgen"} "handwritten_support/hgen/sail_trans_out.hgen" {"handwritten_support/hgen/sail_trans_out.hgen"} "handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen" {"handwritten_support/hgen/shallow_ast_to_herdtools_ast.hgen"} "handwritten_support/hgen/shallow_types_to_herdtools_types.hgen" {"handwritten_support/hgen/shallow_types_to_herdtools_types.hgen"} "handwritten_support/hgen/token_types.hgen" {"handwritten_support/hgen/token_types.hgen"} "handwritten_support/hgen/tokens.hgen" {"handwritten_support/hgen/tokens.hgen"} "handwritten_support/hgen/trans_sail.hgen" {"handwritten_support/hgen/trans_sail.hgen"} "handwritten_support/hgen/types.hgen" {"handwritten_support/hgen/types.hgen"} "handwritten_support/hgen/types_sail_trans_out.hgen" {"handwritten_support/hgen/types_sail_trans_out.hgen"} "handwritten_support/hgen/types_trans_sail.hgen" {"handwritten_support/hgen/types_trans_sail.hgen"} "handwritten_support/0.11/mem_metadata.lem" {"handwritten_support/0.11/mem_metadata.lem"} "handwritten_support/0.11/riscv_extras.lem" {"handwritten_support/0.11/riscv_extras.lem"} "handwritten_support/0.11/riscv_extras_fdext.lem" {"handwritten_support/0.11/riscv_extras_fdext.lem"} "handwritten_support/0.11/riscv_extras_sequential.lem" {"handwritten_support/0.11/riscv_extras_sequential.lem"} "generated_definitions/for-rmem/riscv.lem" {"generated_definitions/for-rmem/riscv.lem"} "generated_definitions/for-rmem/riscv_types.lem" {"generated_definitions/for-rmem/riscv_types.lem"} "generated_definitions/for-rmem/riscv_toFromInterp2.ml" {"generated_definitions/for-rmem/riscv_toFromInterp2.ml"} "generated_definitions/for-rmem/riscv.defs" {"generated_definitions/for-rmem/riscv.defs"} ]