Merge remote-tracking branch 'origin/sail2' into separate_bv

29 files changed, 289 insertions, 4 deletions

diff --git a/aarch64_small/Makefile b/aarch64_small/Makefile
index fe4c5841..2e7c1a7b 100644
--- a/aarch64_small/Makefile
+++ b/aarch64_small/Makefile
@@ -1,5 +1,6 @@
 SAIL:=../sail -Ofast_undefined
 LEM:=../../lem/lem
+LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib
 
 default: all
 
@@ -17,12 +18,18 @@ SOURCES=prelude.sail\
   ../lib/regfp.sail\
   aarch64_regfp.sail
 
+MONO_SPLICES=$(wildcard mono-splices/*.sail)
+MONO_SPLICES_OPTS=$(foreach file,$(MONO_SPLICES),-splice $(file))
+
 all: armV8.lem for-rmem/armV8.lem for-rmem/armV8_toFromInterp2.ml for-rmem/armV8.defs
 
 armV8.lem: $(SOURCES)
 # also generates armV8_embed_sequential.lem, armV8_embed_types.lem, armV8_toFromInterp.lem
 	$(SAIL) $(SAILFLAGS) -lem -lem_lib ArmV8_extras_embed -o armV8 $^
 
+armV8.smt_model: $(SOURCES)
+	$(SAIL) $(SAILFLAGS) -smt_serialize -o armV8 $^
+
 for-rmem/armV8.lem: $(SOURCES)
 	mkdir -p $(dir $@)
 #	We do not need the isabelle .thy files, but sail always generates them
@@ -36,10 +43,24 @@ for-rmem/armV8.defs: $(SOURCES)
 	mkdir -p $(dir $@)
 	$(SAIL) -marshal -o $(basename $@) $^
 
+mono/armV8.lem mono/armV8_types.lem mono/ArmV8_lemmas.thy: $(SOURCES) $(MONO_SPLICES)
+	$(SAIL) $(SAILFLAGS) -lem -lem_mwords -auto_mono -mono_rewrites -lem_lib ArmV8_extras_embed -lem_output_dir $(dir $@) -isa_output_dir $(dir $@) -o armV8 ../lib/mono_rewrites.sail $(SOURCES) $(MONO_SPLICES_OPTS)
+
+mono/ArmV8.thy mono/ArmV8_mono.thy mono/ArmV8_extras_embed.thy: mono/armV8_types.lem mono/armV8.lem armV8_extras_embed.lem
+	cp armV8_extras_embed.lem mono/
+	$(LEM) -isa -lib Sail=../src/gen_lib -lib Sail=../src/lem_interp mono/armV8_types.lem mono/armV8.lem mono/armV8_extras_embed.lem
+
+.PHONY: mono-isa-build
+mono-isa-build: mono/ArmV8.thy
+	isabelle build -b -d $(LEM_ISA_LIB) -d ../lib/isabelle -D mono
+
 clean:
 	rm -f armV8.lem armV8.ml
 	rm -f armV8_embed*.lem armV8_toFromInterp.lem
 	rm -f for-rmem/*
+	rm -f mono/armV8_types.lem mono/armV8.lem mono/armV8_extras_embed.lem
+	rm -f mono/ArmV8_lemmas.thy mono/ArmV8_types_lemmas.thy
+	rm -f mono/ArmV8_types.thy mono/ArmV8.thy mono/ArmV8_extras_embed.thy
 
 ######################################################################
 ETCDIR=../etc
diff --git a/aarch64_small/armV8.sail b/aarch64_small/armV8.sail
index d8ee0bbe..5754b159 100644
--- a/aarch64_small/armV8.sail
+++ b/aarch64_small/armV8.sail
@@ -2142,10 +2142,12 @@ function clause execute ( Reverse((d,n,datasize as int('R),op)) ) = {
       assert (vsize > 0); /* FIXME: CP adding assertion to make typecheck */
       foreach (base from 0 to (datasize - 1) by (2 * vsize)) { /* ARM: while base < datasize do */
         assert (base+vsize*2 - 1 < datasize); /* FIXME: CP adding assertion to make typecheck */
-        let a = tmp[(base+(2*vsize) - 1)..(base+vsize)];
+/*        let a = tmp[(base+(2*vsize) - 1)..(base+vsize)];
         result[((base+vsize) - 1)..base] = a;
         let b = tmp[(base+vsize - 1)..base];
-        result[(base+(2*vsize) - 1)..(base+vsize)] = b;
+        result[(base+(2*vsize) - 1)..(base+vsize)] = b;*/
+        result[((base+vsize) - 1)..base] = tmp[(base+(2*vsize) - 1)..(base+vsize)];
+        result[(base+(2*vsize) - 1)..(base+vsize)] = tmp[(base+vsize - 1)..base];
         /* ARM: base = base + (2 * vsize); */
       };
     };
diff --git a/aarch64_small/armV8_A64_lib.sail b/aarch64_small/armV8_A64_lib.sail
index 8c684fc7..8b32e09f 100644
--- a/aarch64_small/armV8_A64_lib.sail
+++ b/aarch64_small/armV8_A64_lib.sail
@@ -799,7 +799,7 @@ function ExtendReg (N, _reg, etype, shift) = {
 
   let len = uMin(len, length(_val) - shift);
   assert( len >= 1 & 'S + len < 'N);
-  let a = (_val[(len - 1)..0]);
+/*  let a = (_val[(len - 1)..0]);*/
   /* Zeros() */
   Extend((_val[(len - 1)..0]) @ (Zeros() : bits('S)), _unsigned)
 }
diff --git a/aarch64_small/gen/ast.hgen b/aarch64_small/gen/ast.hgen
index 98148a5c..3f0ce79d 100644
--- a/aarch64_small/gen/ast.hgen
+++ b/aarch64_small/gen/ast.hgen
@@ -43,3 +43,5 @@
   | `AArch64TestBitAndBranch of inst_reg*reg_size*uinteger*bit*bit64 (* t,datasize,bit_pos,bit_val,offset *)
   | `AArch64MoveSystemRegister of inst_reg*uinteger*uinteger*uinteger*uinteger*uinteger*boolean (* t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read *)
   | `AArch64MoveSystemImmediate of bit4*pSTATEField (* operand,field *)
+  | `AArch64DataCache of inst_reg*dCOp
+  | `AArch64InstructionCache of inst_reg*iCOp
diff --git a/aarch64_small/gen/fold.hgen b/aarch64_small/gen/fold.hgen
index fbe52794..411262e5 100644
--- a/aarch64_small/gen/fold.hgen
+++ b/aarch64_small/gen/fold.hgen
@@ -43,3 +43,5 @@
 | `AArch64TestBitAndBranch (t,datasize,bit_pos,bit_val,offset) -> fold_reg t (y_reg, y_sreg)
 | `AArch64MoveSystemRegister (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read) -> fold_reg t (y_reg, y_sreg)
 | `AArch64MoveSystemImmediate (operand,field) -> (y_reg, y_sreg)
+| `AArch64DataCache (t, dc_op) -> fold_reg t (y_reg, y_sreg)
+| `AArch64InstructionCache (t, ic_op) -> fold_reg t (y_reg, y_sreg)
diff --git a/aarch64_small/gen/lexer.hgen b/aarch64_small/gen/lexer.hgen
index 6ff24317..e0550dd0 100644
--- a/aarch64_small/gen/lexer.hgen
+++ b/aarch64_small/gen/lexer.hgen
@@ -223,6 +223,9 @@
   "MRS" , MRS {txt="MRS"} ;
   "MSR" , MSR {txt="MSR"} ;
 
+  "DC" , DC {txt="DC"} ;
+  "IC" , IC {txt="IC"} ;
+
 
 (*** instructions/operands ***)
 
@@ -307,3 +310,17 @@
   "SPSel"   , PSTATEFIELD (PSTATEField_SP) ;
   "DAIFSet" , PSTATEFIELD (PSTATEField_DAIFSet) ;
   "DAIFClr" , PSTATEFIELD (PSTATEField_DAIFClr) ;
+
+  "IVAC"  , DCOP (IVAC) ;
+  "ISW"   , DCOP (ISW) ;
+  "CSW"   , DCOP (CSW) ;
+  "CISW"  , DCOP (CISW) ;
+  "ZVA"   , DCOP (ZVA) ;
+  "CVAC"  , DCOP (CVAC) ;
+  "CVAU"  , DCOP (CVAU) ;
+  "CIVAC" , DCOP (CIVAC) ;
+
+  "IALLUIS" , ICOP (IALLUIS) ;
+  "IALLU"   , ICOP (IALLU) ;
+  "IVAU"    , ICOP (IVAU) ;
+
diff --git a/aarch64_small/gen/map.hgen b/aarch64_small/gen/map.hgen
index 3d5419b4..1957a03d 100644
--- a/aarch64_small/gen/map.hgen
+++ b/aarch64_small/gen/map.hgen
@@ -43,3 +43,5 @@
 | `AArch64TestBitAndBranch (t,datasize,bit_pos,bit_val,offset) -> `AArch64TestBitAndBranch (map_reg t,datasize,bit_pos,bit_val,offset)
 | `AArch64MoveSystemRegister (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read) -> `AArch64MoveSystemRegister (map_reg t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read)
 | `AArch64MoveSystemImmediate (operand,field) -> `AArch64MoveSystemImmediate (operand,field)
+| `AArch64DataCache (t, dc_op) -> `AArch64DataCache (map_reg t, dc_op)
+| `AArch64InstructionCache (t, ic_op) -> `AArch64InstructionCache (map_reg t, ic_op)
diff --git a/aarch64_small/gen/parser.hgen b/aarch64_small/gen/parser.hgen
index 53fc1c8f..685dc218 100644
--- a/aarch64_small/gen/parser.hgen
+++ b/aarch64_small/gen/parser.hgen
@@ -1401,3 +1401,15 @@
   | MSR SYSREG COMMA xreg
     { if not (isregzr $4) then error_registers ("expected " ^ $1.txt ^ " <systemreg>, <Xt>")
       else `AArch64MoveSystemRegister($4,$2.sys_op0,$2.sys_op1,$2.sys_op2,$2.sys_crn,$2.sys_crm,false) }
+
+  /* DC */
+
+  | DC DCOP COMMA xreg
+    { if not (isregzr $4) then error_registers ("expected " ^ $1.txt ^ " <dc_op>, <Xt>")
+      else `AArch64DataCache($4,$2) }
+
+  /* IC */
+
+  | IC ICOP COMMA xreg
+    { if not (isregzr $4) then error_registers ("expected " ^ $1.txt ^ " <ic_op>, <Xt>")
+      else `AArch64InstructionCache($4,$2) }
diff --git a/aarch64_small/gen/pretty.hgen b/aarch64_small/gen/pretty.hgen
index b412fdda..998e58ad 100644
--- a/aarch64_small/gen/pretty.hgen
+++ b/aarch64_small/gen/pretty.hgen
@@ -394,3 +394,9 @@
 
 | `AArch64MoveSystemImmediate (operand,field) ->
       sprintf "MSR %s,%s" (pp_pstatefield field) (pp_imm operand)
+
+| `AArch64DataCache (t, dc_op) ->
+      sprintf "DC %s,%s" (pp_dcop dc_op) (pp_regzr Set64 t)
+
+| `AArch64InstructionCache (t, ic_op) ->
+      sprintf "IC %s,%s" (pp_icop ic_op) (pp_regzr Set64 t)
diff --git a/aarch64_small/gen/regs_out_in.hgen b/aarch64_small/gen/regs_out_in.hgen
index bab53be7..72b1ac3c 100644
--- a/aarch64_small/gen/regs_out_in.hgen
+++ b/aarch64_small/gen/regs_out_in.hgen
@@ -154,3 +154,9 @@
 
 | `AArch64MoveSystemImmediate (_operand,_field) ->
       ([], [], [], [Next])
+
+| `AArch64DataCache (_t, _dc_op) ->
+      failwith "is anyone using this?"
+
+| `AArch64InstructionCache (_t, _ic_op) ->
+      failwith "is anyone using this?"
diff --git a/aarch64_small/gen/sail_trans_out.hgen b/aarch64_small/gen/sail_trans_out.hgen
index 0399fa8b..9f84411b 100644
--- a/aarch64_small/gen/sail_trans_out.hgen
+++ b/aarch64_small/gen/sail_trans_out.hgen
@@ -326,3 +326,11 @@
 | "MoveSystemImmediate", [operand; field] ->
   `AArch64MoveSystemImmediate ( translate_out_int operand,
                                 translate_out_pSTATEField field)
+
+| "DataCache", [t; dc_op] ->
+  `AArch64DataCache ( translate_out_regzr Set64 t,
+                      translate_out_dCOp dc_op)
+
+| "InstructionCache", [t; ic_op] ->
+  `AArch64InstructionCache (translate_out_regzr Set64 t,
+                            translate_out_iCOp ic_op)
diff --git a/aarch64_small/gen/token_types.hgen b/aarch64_small/gen/token_types.hgen
index 411dddf9..bf17cd13 100644
--- a/aarch64_small/gen/token_types.hgen
+++ b/aarch64_small/gen/token_types.hgen
@@ -69,6 +69,8 @@ type token_RET = {txt : string}
 type token_TST = {txt : string}
 type token_MRS = {txt : string}
 type token_MSR = {txt : string}
+type token_DC  = {txt : string}
+type token_IC  = {txt : string}
 
 (*** instructions/operands ***)
 
@@ -83,3 +85,5 @@ type token_BARROP = {domain : mBReqDomain; types : mBReqTypes}
 type token_PRFOP = inst_reg (* this is an int that is encoded in a reg field *)
 type token_SYSREG = {sys_op0 : uinteger; sys_op1 : uinteger; sys_op2 : uinteger; sys_crn : uinteger; sys_crm : uinteger}
 type token_PSTATEFIELD = pSTATEField
+type token_DCOP = dCOp
+type token_ICOP = iCOp
diff --git a/aarch64_small/gen/tokens.hgen b/aarch64_small/gen/tokens.hgen
index bf49e463..18142bc7 100644
--- a/aarch64_small/gen/tokens.hgen
+++ b/aarch64_small/gen/tokens.hgen
@@ -62,6 +62,8 @@
 %token <AArch64HGenBase.token_TST> TST
 %token <AArch64HGenBase.token_MRS> MRS
 %token <AArch64HGenBase.token_MSR> MSR
+%token <AArch64HGenBase.token_DC> DC
+%token <AArch64HGenBase.token_IC> IC
 
 /*** instructions/operands ***/
 
@@ -75,4 +77,5 @@
 %token <AArch64HGenBase.token_PRFOP> PRFOP
 %token <AArch64HGenBase.token_SYSREG> SYSREG
 %token <AArch64HGenBase.token_PSTATEFIELD> PSTATEFIELD
-
+%token <AArch64HGenBase.token_DCOP> DCOP
+%token <AArch64HGenBase.token_ICOP> ICOP
diff --git a/aarch64_small/gen/trans_sail.hgen b/aarch64_small/gen/trans_sail.hgen
index df2ed81c..7ad837d9 100644
--- a/aarch64_small/gen/trans_sail.hgen
+++ b/aarch64_small/gen/trans_sail.hgen
@@ -379,3 +379,15 @@
       [translate_bit4 "operand" operand;
         translate_pSTATEField "field" field],
       [])
+
+| `AArch64DataCache (t, dc_op) ->
+    ("DataCache",
+      [translate_reg "t" t;
+        translate_dCOp "dc_op" dc_op],
+      [])
+
+| `AArch64InstructionCache (t, ic_op) ->
+    ("InstructionCache",
+      [translate_reg "t" t;
+        translate_iCOp "ic_op" ic_op],
+      [])
diff --git a/aarch64_small/gen/types.hgen b/aarch64_small/gen/types.hgen
index d581a233..c2a9c3e0 100644
--- a/aarch64_small/gen/types.hgen
+++ b/aarch64_small/gen/types.hgen
@@ -88,3 +88,7 @@ type revOp = RevOp_RBIT | RevOp_REV16 | RevOp_REV32 | RevOp_REV64
 
 type pSTATEField = PSTATEField_DAIFSet | PSTATEField_DAIFClr |
                    PSTATEField_SP
+
+type dCOp = IVAC | ISW | CSW | CISW | ZVA | CVAC | CVAU | CIVAC
+
+type iCOp = IALLUIS | IALLU | IVAU
diff --git a/aarch64_small/gen/types_sail_trans_out.hgen b/aarch64_small/gen/types_sail_trans_out.hgen
index 082a5464..89fbad42 100644
--- a/aarch64_small/gen/types_sail_trans_out.hgen
+++ b/aarch64_small/gen/types_sail_trans_out.hgen
@@ -187,3 +187,22 @@ let translate_out_pSTATEField inst =
     | 1 -> PSTATEField_DAIFClr
     | 2 -> PSTATEField_SP
     | _ -> assert false
+
+let translate_out_dCOp inst =
+  match translate_out_enum inst with
+    | 0 -> IVAC
+    | 1 -> ISW
+    | 2 -> CSW
+    | 3 -> CISW
+    | 4 -> ZVA
+    | 5 -> CVAC
+    | 6 -> CVAU
+    | 7 -> CIVAC
+    | _ -> assert false
+
+let translate_out_iCOp inst =
+  match translate_out_enum inst with
+    | 0 -> IALLUIS
+    | 1 -> IALLU
+    | 2 -> IVAU
+    | _ -> assert false
diff --git a/aarch64_small/gen/types_trans_sail.hgen b/aarch64_small/gen/types_trans_sail.hgen
index 7f2d5fe7..8081e316 100644
--- a/aarch64_small/gen/types_trans_sail.hgen
+++ b/aarch64_small/gen/types_trans_sail.hgen
@@ -117,3 +117,9 @@ let translate_revOp =
 
 let translate_pSTATEField =
   translate_enum [PSTATEField_DAIFSet; PSTATEField_DAIFClr; PSTATEField_SP]
+
+let translate_dCOp =
+  translate_enum [IVAC; ISW; CSW; CISW; ZVA; CVAC; CVAU; CIVAC]
+
+let translate_iCOp =
+  translate_enum [IALLUIS; IALLU; IVAU]
diff --git a/aarch64_small/mono-splices/ASR_C.sail b/aarch64_small/mono-splices/ASR_C.sail
new file mode 100644
index 00000000..0a47d8d7
--- /dev/null
+++ b/aarch64_small/mono-splices/ASR_C.sail
@@ -0,0 +1,8 @@
+val ASR_C : forall 'N 'S, 'N >= 1 & 'S >= 1.
+  (bits('N), int('S)) -> (bits('N), bit) effect {escape}
+
+function ASR_C (x, shift) = {
+  result : bits('N) = sail_arith_shiftright(x, shift);
+  carry_out : bit = if shift > 'N then x['N - 1] else x[shift - 1];
+  return((result, carry_out))
+}
diff --git a/aarch64_small/mono-splices/BigEndianReverse.sail b/aarch64_small/mono-splices/BigEndianReverse.sail
new file mode 100644
index 00000000..97893ed1
--- /dev/null
+++ b/aarch64_small/mono-splices/BigEndianReverse.sail
@@ -0,0 +1,8 @@
+val BigEndianReverse : forall 'W, 'W in {8,16,32,64,128}. bits('W) -> bits('W) effect pure
+
+function BigEndianReverse value_name = {
+  result : bits('W) = replicate_bits(0b0,'W);
+  foreach (i from 0 to ('W - 8) by 8)
+    result[i+7 .. i] = (value_name['W-i - 1 .. 'W-i - 8] : bits(8));
+  return result
+}
diff --git a/aarch64_small/mono-splices/CountLeadingSignBits.sail b/aarch64_small/mono-splices/CountLeadingSignBits.sail
new file mode 100644
index 00000000..7bbfd449
--- /dev/null
+++ b/aarch64_small/mono-splices/CountLeadingSignBits.sail
@@ -0,0 +1,3 @@
+val CountLeadingSignBits : forall 'N, 'N >= 2. bits('N) -> int
+
+function CountLeadingSignBits x = return(CountLeadingZeroBits((sail_shiftright(x, 1)) ^ (x & slice_mask(0,'N))))
diff --git a/aarch64_small/mono-splices/DecodeBitMasks.sail b/aarch64_small/mono-splices/DecodeBitMasks.sail
new file mode 100644
index 00000000..fc1d63fa
--- /dev/null
+++ b/aarch64_small/mono-splices/DecodeBitMasks.sail
@@ -0,0 +1,43 @@
+val DecodeBitMasks2 : forall 'M 'S 'd, 'M >= 'd + 1 & 'S >= 0 & 'd >= 0. (int, int('S), nat, int('d), int('M)) -> (bits('M), bits('M)) effect {escape}
+
+function DecodeBitMasks2(esize as 'E, S, R, d, M) = {
+  assert(constraint('E in {2,4,8,16,32,64} & 'M >= 'E & 'E >= 'd + 1));
+  assert(esize >= S+1); /* CP: adding this assertion to make typecheck */
+  welem : bits('E) = ZeroExtend(Ones(S + 1));
+  telem : bits('E) = ZeroExtend(Ones(d + 1));
+  wmask = Replicate(M,ROR(welem, R));
+  tmask = Replicate(M,telem);
+  (wmask, tmask);
+}
+
+function DecodeBitMasks(M : int('M), immN : bit, imms : bits(6), immr : bits(6), immediate : boolean) = {
+  /* let M = (length((bit['M]) 0)) in { */
+  /* ARM: (bit['M]) tmask := 0; (* ARM: uninitialized *) */
+  /* ARM: (bit['M]) wmask := 0; (* ARM: uninitialized *) */
+  levels : bits(6) = Zeros(); /* ARM: uninitialized */
+
+  /* Compute log2 of element size */
+  /* 2^len must be in range [2, 'M] */
+  let len : range(0,6) = match HighestSetBit([immN]@(~(imms))) {
+    None() => { assert (false, "DecodeBitMasks: HighestSetBit returned None"); 0; },
+    Some(c) => c
+  };
+  if len < 1 then {ReservedValue(); exit()} else {
+  assert(M >= lsl(1, len));
+
+  /* Determine S, R and S - R parameters */
+  levels = ZeroExtend(Ones(len));
+
+  /* For logical immediates an all-ones value of S is reserved */
+  /* since it would generate a useless all-ones result (many times) */
+  if immediate & ((imms & levels) == levels) then
+    ReservedValue();
+
+  let S = UInt (imms & levels);
+  let R = UInt (immr & levels);
+  let diff : bits(6) = to_bits(S - R); /* 6-bit subtract with borrow */
+
+  let esize as int('E) = lsl(1, len);
+  let d /* : bits(6) */ = UInt (diff[(len - 1)..0]);
+  DecodeBitMasks2(esize, S, R, d, M);
+}}
diff --git a/aarch64_small/mono-splices/LSL_C.sail b/aarch64_small/mono-splices/LSL_C.sail
new file mode 100644
index 00000000..fb9b352c
--- /dev/null
+++ b/aarch64_small/mono-splices/LSL_C.sail
@@ -0,0 +1,8 @@
+val LSL_C : forall 'N 'S, 'N >= 0 & 'S >= 1.
+  (bits('N), int('S)) -> (bits('N), bits(1)) effect pure
+
+function LSL_C (x, shift) = {
+  result : bits('N) = x << shift;
+  carry_out : bits(1) = if shift > 'N then 0b0 else [x['N - shift]];
+  return((result, carry_out))
+}
diff --git a/aarch64_small/mono-splices/LSR_C.sail b/aarch64_small/mono-splices/LSR_C.sail
new file mode 100644
index 00000000..5fed8ad6
--- /dev/null
+++ b/aarch64_small/mono-splices/LSR_C.sail
@@ -0,0 +1,8 @@
+val LSR_C : forall 'N 'S, 'N >= 1 & 'S >= 1.
+  (bits('N), int('S)) -> (bits('N), bit) effect pure
+
+function LSR_C (x, shift) = {
+  result : bits('N) = x >> shift;
+  carry_out : bit = if shift > 'N then bitzero else x[shift - 1];
+  return((result, carry_out))
+}
diff --git a/aarch64_small/mono-splices/Poly32Mod2.sail b/aarch64_small/mono-splices/Poly32Mod2.sail
new file mode 100644
index 00000000..5162d607
--- /dev/null
+++ b/aarch64_small/mono-splices/Poly32Mod2.sail
@@ -0,0 +1,8 @@
+function Poly32Mod2 (data__arg, poly) = {
+  data = data__arg;
+  assert('N > 32, "(N > 32)");
+  let poly' : bits('N) = extzv(poly) in
+  foreach (i from ('N - 1) to 32 by 1 in dec)
+    if [data[i]] == 0b1 then data = data | (poly' << i - 32) else ();
+  return(slice(data, 0, 32))
+}
diff --git a/aarch64_small/mono-splices/Replicate.sail b/aarch64_small/mono-splices/Replicate.sail
new file mode 100644
index 00000000..a3c464e5
--- /dev/null
+++ b/aarch64_small/mono-splices/Replicate.sail
@@ -0,0 +1,6 @@
+function Replicate(N, 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_small/mono-splices/SignExtend.sail b/aarch64_small/mono-splices/SignExtend.sail
new file mode 100644
index 00000000..6a263563
--- /dev/null
+++ b/aarch64_small/mono-splices/SignExtend.sail
@@ -0,0 +1,3 @@
+function SignExtend (N,x) = {
+  return(extsv(x))
+}
diff --git a/aarch64_small/mono-splices/ZeroExtend.sail b/aarch64_small/mono-splices/ZeroExtend.sail
new file mode 100644
index 00000000..9e55ee71
--- /dev/null
+++ b/aarch64_small/mono-splices/ZeroExtend.sail
@@ -0,0 +1,3 @@
+function ZeroExtend (N,x) = {
+  return(extzv(x))
+}
diff --git a/aarch64_small/mono-splices/_wMem.sail b/aarch64_small/mono-splices/_wMem.sail
new file mode 100644
index 00000000..8e37ca64
--- /dev/null
+++ b/aarch64_small/mono-splices/_wMem.sail
@@ -0,0 +1,57 @@
+function _wMem(write_buffer, desc, size, acctype, exclusive, value) = {
+  let s = write_buffer.size;
+  if s == 0 then {
+    struct { acctype = acctype,
+      exclusive = exclusive,
+      address = (desc.paddress).physicaladdress,
+      value = ZeroExtend(value),
+      size = size
+    }
+  } else {
+    assert(write_buffer.acctype == acctype);
+    assert(write_buffer.exclusive == exclusive);
+    assert((write_buffer.address + s) : bits(64) == (desc.paddress).physicaladdress);
+  assert((s * 8) + ('N * 8) <= 128);
+    value1 : bits(128) = sail_shiftleft(ZeroExtend(value), s * 8);
+    value1[((s * 8) - 1) .. 0] = (write_buffer.value)[((s * 8) - 1) .. 0];
+    { write_buffer with
+      value = value1,
+      size = s + size
+    }
+  }
+}
+
+val flush_write_buffer2 : forall 'n, 'n in {1,2,4,8,16}. (write_buffer_type, int('n)) -> unit effect {escape,wmv}
+
+function flush_write_buffer2 (write_buffer, s) ={
+  match write_buffer.acctype {
+    AccType_NORMAL   => wMem_Val_NORMAL (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_STREAM   => wMem_Val_NORMAL (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_UNPRIV   => wMem_Val_NORMAL (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_ORDERED  => wMem_Val_ORDERED (write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    _  => not_implemented("unrecognised memory access")
+  };
+}
+
+function flush_write_buffer(write_buffer) = {
+  assert(write_buffer.exclusive == false);
+  let s : range(0,16) = write_buffer.size;
+  assert (s == 1 | s == 2 | s == 4 | s == 8 | s == 16);
+  flush_write_buffer2(write_buffer, s);
+}
+
+val flush_write_buffer_exclusive2 : forall 'n, 'n in {1,2,4,8,16}. (write_buffer_type, int('n)) -> bool effect {escape, wmv}
+function flush_write_buffer_exclusive2(write_buffer, s) = {
+  match write_buffer.acctype {
+    AccType_ATOMIC   => wMem_Val_ATOMIC(write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    AccType_ORDERED  => wMem_Val_ATOMIC_ORDERED(write_buffer.address, s, (write_buffer.value)[((s * 8) - 1) .. 0]),
+    _  => { not_implemented("unrecognised memory access"); false; }
+  };
+}
+
+function flush_write_buffer_exclusive(write_buffer) = {
+  assert(write_buffer.exclusive);
+  let s = write_buffer.size;
+  assert (s == 1 | s == 2 | s == 4 | s == 8 | s == 16);
+  flush_write_buffer_exclusive2(write_buffer, s);
+}
diff --git a/aarch64_small/mono/ROOT b/aarch64_small/mono/ROOT
new file mode 100644
index 00000000..9c65d37d
--- /dev/null
+++ b/aarch64_small/mono/ROOT
@@ -0,0 +1,4 @@
+session "Sail-AArch64-small" = "Sail" +
+  options [document = false]
+  theories
+    ArmV8_lemmas