Merge branch 'sail2' into mappings

(involved some manual tinkering with gitignore, type_check, riscv)

10 files changed, 101 insertions, 290 deletions

diff --git a/aarch64/Makefile b/aarch64/Makefile
index 0ef6b0f0..58281dc7 100644
--- a/aarch64/Makefile
+++ b/aarch64/Makefile
@@ -4,6 +4,15 @@ export SAIL_DIR
 SAIL_LIB_DIR:=$(SAIL_DIR)/lib
 SAIL:=$(SAIL_DIR)/sail
 
+aarch64.c: no_vector.sail
+	$(SAIL) $^ -c -O -undefined_gen -no_lexp_bounds_check -memo_z3 1> aarch64.c
+
+aarch64_c: aarch64.c
+	gcc -O2 $^ -o aarch64_c -lgmp -L $(SAIL_DIR)/lib
+
+aarch64: no_vector.sail
+	$(SAIL) $^ -o aarch64 -ocaml -undefined_gen -no_lexp_bounds_check -memo_z3
+
 aarch64.lem: no_vector.sail
 	$(SAIL) $^ -o aarch64 -lem -lem_lib Aarch64_extras -memo_z3 -undefined_gen -no_lexp_bounds_check
 aarch64_types.lem: aarch64.lem
diff --git a/aarch64/aarch64_extras.lem b/aarch64/aarch64_extras.lem
index ab67f506..7e3bb28a 100644
--- a/aarch64/aarch64_extras.lem
+++ b/aarch64/aarch64_extras.lem
@@ -15,38 +15,6 @@ type ty2048
 instance (Size ty2048) let size = 2048 end
 declare isabelle target_rep type ty2048 = `2048`
 
-val slice : list bitU -> integer -> integer -> list bitU
-let slice v lo len =
-  subrange_vec_dec v (lo + len - 1) lo
-
-val set_slice : integer -> integer -> list bitU -> integer -> list bitU -> list bitU
-let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
-  update_subrange_vec_dec out (n + slice_len - 1) n v
-
-let get_slice_int_bl len n lo =
-  (* TODO: Is this the intended behaviour? *)
-  let hi = lo + len - 1 in
-  let bs = bools_of_int (hi + 1) n in
-  subrange_list false bs hi lo
-
-val get_slice_int : integer -> integer -> integer -> list bitU
-let get_slice_int len n lo = of_bools (get_slice_int_bl len n lo)
-
-val set_slice_int : integer -> integer -> integer -> list bitU -> integer
-let set_slice_int len n lo v =
-  let hi = lo + len - 1 in
-  let bs = bits_of_int (hi + 1) n in
-  maybe_failwith (signed_of_bits (update_subrange_list false bs hi lo v))
-
-(*let ext_slice signed v i j =
-  let len = length v in
-  let bits = get_bits false (bits_of v) i j in
-  of_bits (if signed then exts_bits len bits else extz_bits len bits)
-val exts_slice : list bitU -> integer -> integer -> list bitU
-let exts_slice v i j = ext_slice true v i j
-val extz_slice : list bitU -> integer -> integer -> list bitU
-let extz_slice v i j = ext_slice false v i j*)
-
 let hexchar_to_bool_list c =
   if c = #'0' then      Just ([false;false;false;false])
   else if c = #'1' then Just ([false;false;false;true ])
diff --git a/aarch64/full/spec.sail b/aarch64/full/spec.sail
index f468302b..6920db48 100644
--- a/aarch64/full/spec.sail
+++ b/aarch64/full/spec.sail
@@ -2130,6 +2130,8 @@ val Replicate : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
 
 function Replicate x = {
   assert('N % 'M == 0, "((N MOD M) == 0)");
+  let 'O = 'N / 'M;
+  assert(constraint('O * 'M = 'N));
   return(replicate_bits(x, 'N / 'M))
 }
 
diff --git a/aarch64/mono/aarch64_extras.lem b/aarch64/mono/aarch64_extras.lem
index a50ba76f..f9027593 100644
--- a/aarch64/mono/aarch64_extras.lem
+++ b/aarch64/mono/aarch64_extras.lem
@@ -8,52 +8,15 @@ open import Prompt
 type ty512
 instance (Size ty512) let size = 512 end
 declare isabelle target_rep type ty512 = `512`
+declare hol target_rep type ty512 = `512`
 type ty1024
 instance (Size ty1024) let size = 1024 end
 declare isabelle target_rep type ty1024 = `1024`
+declare hol target_rep type ty1024 = `1024`
 type ty2048
 instance (Size ty2048) let size = 2048 end
 declare isabelle target_rep type ty2048 = `2048`
-
-val slice : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> integer -> mword 'b
-let slice v lo len =
-  subrange_vec_dec v (lo + len - 1) lo
-
-val set_slice : forall 'a 'b. Size 'a, Size 'b => integer -> integer -> mword 'a -> integer -> mword 'b -> mword 'a
-let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v =
-  update_subrange_vec_dec out (n + slice_len - 1) n v
-
-let get_slice_int_bl len n lo =
-  (* TODO: Is this the intended behaviour? *)
-  let hi = lo + len - 1 in
-  let bs = bools_of_int (hi + 1) n in
-  subrange_list false bs hi lo
-
-val get_slice_int : forall 'a. Size 'a => integer -> integer -> integer -> mword 'a
-let get_slice_int len n lo = of_bools (get_slice_int_bl len n lo)
-
-val set_slice_int :  forall 'a. Size 'a => integer -> integer -> integer -> mword 'a -> integer
-let set_slice_int len n lo v =
-  let hi = lo + len - 1 in
-  let bs = bools_of_int (hi + 1) n in
-  (*let len_n = max (hi + 1) (integerFromNat (List.length bs)) in
-  let ext_bs = exts_bools len_n bs in*)
-  signed_of_bools (update_subrange_list false bs hi lo (bitlistFromWord v))
-
-(*let ext_slice signed v i j =
-  let len = length v in
-  let bits = get_bits false (bits_of v) i j in
-  of_bits (if signed then exts_bits len bits else extz_bits len bits)
-val exts_slice : list bitU -> integer -> integer -> list bitU
-let exts_slice v i j = ext_slice true v i j
-val extz_slice : list bitU -> integer -> integer -> list bitU
-let extz_slice v i j = ext_slice false v i j*)
-
-val shr_int : ii -> ii -> ii
-let rec shr_int x s = if s > 0 then shr_int (x / 2) (s - 1) else x
-
-val shl_int : integer -> integer -> integer
-let rec shl_int i shift = if shift > 0 then 2 * shl_int i (shift - 1) else i
+declare hol target_rep type ty2048 = `2048`
 
 let hexchar_to_bool_list c =
   if c = #'0' then      Just ([false;false;false;false])
@@ -90,13 +53,10 @@ let hexstring_to_bools s =
 
 val hex_slice : forall 'rv 'n 'e. Size 'n => string -> integer -> integer -> monad 'rv (mword 'n) 'e
 let hex_slice v len lo =
-  match hexstring_to_bools v with
-    | Just bs ->
-       let hi = len + lo - 1 in
-       let bs = ext_list false (len + lo) bs in
-       return (of_bools (subrange_list false bs hi lo))
-    | Nothing -> Fail "hex_slice"
-  end
+  maybe_fail "hex_slice" (hexstring_to_bools v) >>= fun bs ->
+   let hi = len + lo - 1 in
+   let bs = ext_list false (len + lo) bs in
+   return (of_bools (subrange_list false bs hi lo))
 
 let internal_pick vs = return (head vs)
 
diff --git a/aarch64/mono/demo/Holmakefile b/aarch64/mono/demo/Holmakefile
new file mode 100644
index 00000000..47959f81
--- /dev/null
+++ b/aarch64/mono/demo/Holmakefile
@@ -0,0 +1,11 @@
+LEMDIR=../../../../lem/hol-lib
+
+INCLUDES = $(LEMDIR) ../../../lib/hol
+
+all: aarch64_monoTheory.uo
+.PHONY: all
+
+ifdef POLY
+HOLHEAP = ../../../lib/hol/sail-heap
+
+endif
diff --git a/aarch64/mono/demo/aarch64_no_vector/main.sail b/aarch64/mono/demo/aarch64_no_vector/main.sail
index 1e44f531..e9e2f84f 100644
--- a/aarch64/mono/demo/aarch64_no_vector/main.sail
+++ b/aarch64/mono/demo/aarch64_no_vector/main.sail
@@ -1,18 +1,24 @@
-val fetch_and_execute : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
+$include <elf.sail>
 
-function fetch_and_execute () = while true do {
-  let instr = aget_Mem(_PC, 4, AccType_IFETCH);
-  decode(instr);
-  if __BranchTaken then __BranchTaken = false else _PC = _PC + 4
-}
+// Simple top level fetch and execute loop.
+val fetch_and_execute : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
 
-val elf_entry = "Elf_loader.elf_entry" : unit -> int
+function fetch_and_execute () =
+  while true do {
+    try {
+      let instr = aget_Mem(_PC, 4, AccType_IFETCH);
+      decode(instr);
+    } catch {
+      Error_See("HINT") => (),
+      _ => exit(())
+    };
+    if __BranchTaken then __BranchTaken = false else _PC = _PC + 4
+  }
 
 val main : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
 
 function main () = {
   _PC = __GetSlice_int(64, elf_entry(), 0);
-  print(BitStr(_PC));
   SP_EL0 = ZeroExtend(0x3C00, 64);
   PSTATE.D = 0b1;
   PSTATE.A = 0b1;
diff --git a/aarch64/mono/demo/aarch64_no_vector/spec.sail b/aarch64/mono/demo/aarch64_no_vector/spec.sail
index 01b7660a..7f3fb09e 100644
--- a/aarch64/mono/demo/aarch64_no_vector/spec.sail
+++ b/aarch64/mono/demo/aarch64_no_vector/spec.sail
@@ -6760,10 +6760,10 @@ function AArch64_StateMatch (SSC__arg, HMC__arg, PxC__arg, linked__arg, LBN, isb
   priv_match : bool = undefined;
   if ~(ispriv) & ~(isbreakpnt) then priv_match = EL0_match
   else match PSTATE.EL {
-    EL3 => priv_match = EL3_match,
-    EL2 => priv_match = EL2_match,
-    EL1 => priv_match = EL1_match,
-    EL0 => priv_match = EL0_match
+    ? if ? == EL3 => priv_match = EL3_match,
+    ? if ? == EL2 => priv_match = EL2_match,
+    ? if ? == EL1 => priv_match = EL1_match,
+    ? if ? == EL0 => priv_match = EL0_match
   };
   security_state_match : bool = undefined;
   match SSC {
@@ -7067,20 +7067,20 @@ function Strip (A, data) = {
   else
     original_ptr = slice(extfield, 0, negate(bottom_PAC_bit) + 64) @ slice(A, 0, bottom_PAC_bit);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       TrapEL2 = false;
       TrapEL3 = false
     }
@@ -7115,23 +7115,23 @@ function AuthIB (X, Y) = {
   Enable : bits(1) = undefined;
   APIBKey_EL1 : bits(128) = slice(APIBKeyHi_EL1, 0, 64) @ slice(APIBKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[30]] else [SCTLR_EL2[30]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[30]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[30]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[30]];
       TrapEL2 = false;
       TrapEL3 = false
@@ -7189,23 +7189,23 @@ function AuthIA (X, Y) = {
   Enable : bits(1) = undefined;
   APIAKey_EL1 : bits(128) = slice(APIAKeyHi_EL1, 0, 64) @ slice(APIAKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[31]] else [SCTLR_EL2[31]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[31]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[31]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[31]];
       TrapEL2 = false;
       TrapEL3 = false
@@ -7276,23 +7276,23 @@ function AuthDB (X, Y) = {
   Enable : bits(1) = undefined;
   APDBKey_EL1 : bits(128) = slice(APDBKeyHi_EL1, 0, 64) @ slice(APDBKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[13]] else [SCTLR_EL2[13]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[13]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[13]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[13]];
       TrapEL2 = false;
       TrapEL3 = false
@@ -7319,23 +7319,23 @@ function AuthDA (X, Y) = {
   Enable : bits(1) = undefined;
   APDAKey_EL1 : bits(128) = slice(APDAKeyHi_EL1, 0, 64) @ slice(APDAKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[27]] else [SCTLR_EL2[27]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[27]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[27]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[27]];
       TrapEL2 = false;
       TrapEL3 = false
@@ -7362,23 +7362,23 @@ function AddPACIB (X, Y) = {
   Enable : bits(1) = undefined;
   APIBKey_EL1 : bits(128) = slice(APIBKeyHi_EL1, 0, 64) @ slice(APIBKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[30]] else [SCTLR_EL2[30]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[30]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[30]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[30]];
       TrapEL2 = false;
       TrapEL3 = false
@@ -7436,23 +7436,23 @@ function AddPACIA (X, Y) = {
   Enable : bits(1) = undefined;
   APIAKey_EL1 : bits(128) = slice(APIAKeyHi_EL1, 0, 64) @ slice(APIAKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[31]] else [SCTLR_EL2[31]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[31]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[31]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[31]];
       TrapEL2 = false;
       TrapEL3 = false
@@ -7509,20 +7509,20 @@ function AddPACGA (X, Y) = {
   TrapEL3 : bool = undefined;
   APGAKey_EL1 : bits(128) = slice(APGAKeyHi_EL1, 0, 64) @ slice(APGAKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       TrapEL2 = false;
       TrapEL3 = false
     }
@@ -7548,23 +7548,23 @@ function AddPACDB (X, Y) = {
   Enable : bits(1) = undefined;
   APDBKey_EL1 : bits(128) = slice(APDBKeyHi_EL1, 0, 64) @ slice(APDBKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[13]] else [SCTLR_EL2[13]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[13]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[13]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[13]];
       TrapEL2 = false;
       TrapEL3 = false
@@ -7591,23 +7591,23 @@ function AddPACDA (X, Y) = {
   Enable : bits(1) = undefined;
   APDAKey_EL1 : bits(128) = slice(APDAKeyHi_EL1, 0, 64) @ slice(APDAKeyLo_EL1, 0, 64);
   match PSTATE.EL {
-    EL0 => {
+    ? if ? == EL0 => {
       IsEL1Regime : bool = (~(HaveEL(EL2)) | [HCR_EL2[27]] == 0b0) | [HCR_EL2[34]] == 0b0;
       Enable = if IsEL1Regime then [SCTLR_EL1[27]] else [SCTLR_EL2[27]];
       TrapEL2 = ((HaveEL(EL2) & IsEL1Regime) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL1 => {
+    ? if ? == EL1 => {
       Enable = [SCTLR_EL1[27]];
       TrapEL2 = (HaveEL(EL2) & ~(IsSecure())) & [HCR_EL2[41]] == 0b0;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL2 => {
+    ? if ? == EL2 => {
       Enable = [SCTLR_EL2[27]];
       TrapEL2 = false;
       TrapEL3 = HaveEL(EL3) & [SCR_EL3[17]] == 0b0
     },
-    EL3 => {
+    ? if ? == EL3 => {
       Enable = [SCTLR_EL3[27]];
       TrapEL2 = false;
       TrapEL3 = false
diff --git a/aarch64/mono/demo/mk.hol b/aarch64/mono/demo/mk.hol
new file mode 100755
index 00000000..ac20717f
--- /dev/null
+++ b/aarch64/mono/demo/mk.hol
@@ -0,0 +1,9 @@
+#!/bin/bash
+set -ex
+../../../sail ../../prelude.sail ../mono_rewrites.sail \
+     aarch64_no_vector/spec.sail aarch64_no_vector/decode_start.sail aarch64_no_vector/decode.sail aarch64_no_vector/decode_end.sail \
+     -no_lexp_bounds_check -memo_z3 -undefined_gen \
+     -auto_mono -mono_rewrites -dall_split_errors -dmono_continue \
+     -lem -lem_mwords -lem_sequential -lem_lib Aarch64_extras -o aarch64_mono
+lem -hol -outdir . -lib ../../../lib/hol -lib ../../../src/gen_lib/ -lib ../../../src/lem_interp ../aarch64_extras.lem aarch64_mono_types.lem aarch64_mono.lem 
+Holmake
diff --git a/aarch64/mono/mono_rewrites.sail b/aarch64/mono/mono_rewrites.sail
index c9164b6c..10f2d07b 100644..120000
--- a/aarch64/mono/mono_rewrites.sail
+++ b/aarch64/mono/mono_rewrites.sail
@@ -1,157 +1 @@
-/* Definitions for use with the -mono_rewrites option */
-
-/* External definitions not in the usual asl prelude */
-
-infix 6 <<
-
-val shiftleft = "shiftl" : forall 'n ('ord : Order).
-    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
-
-overload operator << = {shiftleft}
-
-infix 6 >>
-
-val shiftright = "shiftr" : forall 'n ('ord : Order).
-    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
-
-overload operator >> = {shiftright}
-
-val arith_shiftright = "arith_shiftr" : forall 'n ('ord : Order).
-    (vector('n, 'ord, bit), int) -> vector('n, 'ord, bit) effect pure
-
-val "extz_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extzv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
-function extzv(v) = extz_vec(sizeof('m),v)
-
-val "exts_vec" : forall 'n 'm. (atom('m),vector('n, dec, bit)) -> vector('m, dec, bit) effect pure
-val extsv : forall 'n 'm. vector('n, dec, bit) -> vector('m, dec, bit) effect pure
-function extsv(v) = exts_vec(sizeof('m),v)
-
-/* This is generated internally to deal with case splits which reveal the size
-   of a bitvector */
-val bitvector_cast = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
-
-/* Definitions for the rewrites */
-
-val slice_mask : forall 'n, 'n >= 0. (int, int) -> bits('n) effect pure
-function slice_mask(i,l) =
-  let one : bits('n) = extzv(0b1) in
-  ((one << l) - one) << i
-
-val is_zero_subrange : forall 'n, 'n >= 0.
-  (bits('n), int, int) -> bool effect pure
-
-function is_zero_subrange (xs, i, j) = {
-  (xs & slice_mask(j, i-j)) == extzv(0b0)
-}
-
-val is_ones_subrange : forall 'n, 'n >= 0.
-  (bits('n), int, int) -> bool effect pure
-
-function is_ones_subrange (xs, i, j) = {
-  let m : bits('n) = slice_mask(j,j-i) in
-  (xs & m) == m
-}
-
-val slice_slice_concat : forall 'n 'm 'r, 'n >= 0 & 'm >= 0 & 'r >= 0.
-  (bits('n), int, int, bits('m), int, int) -> bits('r) effect pure
-
-function slice_slice_concat (xs, i, l, ys, i', l') = {
-  let xs = (xs & slice_mask(i,l)) >> i in
-  let ys = (ys & slice_mask(i',l')) >> i' in
-  extzv(xs) << l' | extzv(ys)
-}
-
-val slice_zeros_concat : forall 'n 'p 'q 'r, 'r = 'p + 'q & 'n >= 0 & 'p >= 0 & 'q >= 0 & 'r >= 0.
-  (bits('n), int, atom('p), atom('q)) -> bits('r) effect pure
-
-function slice_zeros_concat (xs, i, l, l') = {
-  let xs = (xs & slice_mask(i,l)) >> i in
-  extzv(xs) << l'
-}
-
-/* Assumes initial vectors are of equal size */
-
-val subrange_subrange_eq : forall 'n, 'n >= 0.
-  (bits('n), int, int, bits('n), int, int) -> bool effect pure
-
-function subrange_subrange_eq (xs, i, j, ys, i', j') = {
-  let xs = (xs & slice_mask(j,i-j)) >> j in
-  let ys = (ys & slice_mask(j',i'-j')) >> j' in
-  xs == ys
-}
-
-val subrange_subrange_concat : forall 'n 'o 'p 'm 'q 'r 's, 's = 'o - ('p - 1) + 'q - ('r - 1) & 'n >= 0 & 'm >= 0.
-  (bits('n), atom('o), atom('p), bits('m), atom('q), atom('r)) -> bits('s) effect pure
-
-function subrange_subrange_concat (xs, i, j, ys, i', j') = {
-  let xs = (xs & slice_mask(j,i-j)) >> j in
-  let ys = (ys & slice_mask(j',i'-j')) >> j' in
-  extzv(xs) << i' - (j' - 1) | extzv(ys)
-}
-
-val place_subrange : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (bits('n), int, int, int) -> bits('m) effect pure
-
-function place_subrange(xs,i,j,shift) = {
-  let xs = (xs & slice_mask(j,i-j)) >> j in
-  extzv(xs) << shift
-}
-
-val place_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (bits('n), int, int, int) -> bits('m) effect pure
-
-function place_slice(xs,i,l,shift) = {
-  let xs = (xs & slice_mask(i,l)) >> i in
-  extzv(xs) << shift
-}
-
-val zext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (bits('n), int, int) -> bits('m) effect pure
-
-function zext_slice(xs,i,l) = {
-  let xs = (xs & slice_mask(i,l)) >> i in
-  extzv(xs)
-}
-
-val sext_slice : forall 'n 'm, 'n >= 0 & 'm >= 0.
-  (bits('n), int, int) -> bits('m) effect pure
-
-function sext_slice(xs,i,l) = {
-  let xs = arith_shiftright(((xs & slice_mask(i,l)) << ('n - i - l)), 'n - l) in
-  extsv(xs)
-}
-
-/* This has different names in the aarch64 prelude (UInt) and the other
-   preludes (unsigned).  To avoid variable name clashes, we redeclare it
-   here with a suitably awkward name. */
-val _builtin_unsigned = {
-  ocaml: "uint",
-  lem: "uint",
-  interpreter: "uint",
-  c: "sail_uint"
-} : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
-
-val unsigned_slice : forall 'n, 'n >= 0.
-  (bits('n), int, int) -> int effect pure
-
-function unsigned_slice(xs,i,l) = {
-  let xs = (xs & slice_mask(i,l)) >> i in
-  _builtin_unsigned(xs)
-}
-
-val unsigned_subrange : forall 'n, 'n >= 0.
-  (bits('n), int, int) -> int effect pure
-
-function unsigned_subrange(xs,i,j) = {
-  let xs = (xs & slice_mask(j,i-j)) >> i in
-  _builtin_unsigned(xs)
-}
-
-
-val zext_ones : forall 'n, 'n >= 0. int -> bits('n) effect pure
-
-function zext_ones(m) = {
-  let v : bits('n) = extsv(0b1) in
-  v >> ('n - m)
-}
+../../lib/mono_rewrites.sail
\ No newline at end of file
diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail
index 775800f3..8710e66b 100644
--- a/aarch64/no_vector/spec.sail
+++ b/aarch64/no_vector/spec.sail
@@ -2064,10 +2064,12 @@ val Replicate : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
 
 function Replicate x = {
   assert('N % 'M == 0, "((N MOD M) == 0)");
+  let 'O = 'N / 'M;
+  assert(constraint('O * 'M = 'N));
   return(replicate_bits(x, 'N / 'M))
 }
 
-val Zeros__0 : forall ('N : Int), 'N >= 0. atom('N) -> bits('N)
+val Zeros__0  = {c: "zeros"} : forall ('N : Int), 'N >= 0. atom('N) -> bits('N)
 
 val Zeros__1 : forall ('N : Int), 'N >= 0. unit -> bits('N)
 
@@ -2084,7 +2086,7 @@ function __ResetMemoryState () = {
   __ExclusiveLocal = false
 }
 
-val ZeroExtend__0 : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
+val ZeroExtend__0 = {c: "zero_extend"} : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
   (bits('M), atom('N)) -> bits('N) effect {escape}
 
 val ZeroExtend__1 : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.