small progress

5 files changed, 305 insertions, 140 deletions

diff --git a/aarch64_small/armV8.h.sail b/aarch64_small/armV8.h.sail
index f5c5aa1e..30309e30 100644
--- a/aarch64_small/armV8.h.sail
+++ b/aarch64_small/armV8.h.sail
@@ -98,14 +98,47 @@ register R2 : bits(64)
 register R1 : bits(64)
 register R0 : bits(64)
 
-let _R : vector(32,dec,(register(bits(64)))) =
-  [undefined,R30,R29,R28,R27,R26,R25,R24,R23,R22,R21,
-             R20,R19,R18,R17,R16,R15,R14,R13,R12,R11,
-             R10,R9 ,R8 ,R7 ,R6 ,R5 ,R4 ,R3 ,R2 ,R1 ,
-             R0]
+/* let _R : vector(32,dec,register(bits(64))) = */
+/*   [ref undefined */
+let _R : vector(31,dec,register(bits(64))) =
+  [ref R30
+  ,ref R29
+  ,ref R28
+  ,ref R27
+  ,ref R26
+  ,ref R25
+  ,ref R24
+  ,ref R23
+  ,ref R22
+  ,ref R21
+  ,ref R20
+  ,ref R19
+  ,ref R18
+  ,ref R17
+  ,ref R16
+  ,ref R15
+  ,ref R14
+  ,ref R13
+  ,ref R12
+  ,ref R11
+  ,ref R10
+  ,ref R9
+  ,ref R8
+  ,ref R7
+  ,ref R6
+  ,ref R5
+  ,ref R4
+  ,ref R3
+  ,ref R2
+  ,ref R1
+  ,ref R0
+  ]
 
-val reg_index : reg_size -> UInt_reg effect pure
-function reg_index x = (x : (reg_index))
+/* val reg_index : reg_size -> UInt_reg effect pure */
+/* function reg_index x = (x : (reg_index)) */
+
+val reg_index : reg_size -> reg_index
+function reg_index x = unsigned(x)
 
 /* SIMD and floating-point registers */
 
@@ -142,11 +175,46 @@ register V2 : bits(128)
 register V1 : bits(128)
 register V0 : bits(128)
 
+/* let _V : vector(33,dec,(register(bits(128)))) = */
+/*   [undefined,V31,V30,V29,V28,V27,V26,V25,V24,V23,V22, */
+/*              V21,V20,V19,V18,V17,V16,V15,V14,V13,V12, */
+/*              V11,V10,V9 ,V8 ,V7 ,V6 ,V5 ,V4 ,V3 ,V2 , */
+/*              V1 ,V0] */
+
 let _V : vector(32,dec,(register(bits(128)))) =
-  [undefined,V31,V30,V29,V28,V27,V26,V25,V24,V23,V22,
-             V21,V20,V19,V18,V17,V16,V15,V14,V13,V12,
-             V11,V10,V9 ,V8 ,V7 ,V6 ,V5 ,V4 ,V3 ,V2 ,
-             V1 ,V0]
+  [ref V31
+  ,ref V30
+  ,ref V29
+  ,ref V28
+  ,ref V27
+  ,ref V26
+  ,ref V25
+  ,ref V24
+  ,ref V23
+  ,ref V22
+  ,ref V21
+  ,ref V20
+  ,ref V19
+  ,ref V18
+  ,ref V17
+  ,ref V16
+  ,ref V15
+  ,ref V14
+  ,ref V13
+  ,ref V12
+  ,ref V11
+  ,ref V10
+  ,ref V9 
+  ,ref V8 
+  ,ref V7 
+  ,ref V6 
+  ,ref V5 
+  ,ref V4 
+  ,ref V3 
+  ,ref V2 
+  ,ref V1 
+  ,ref V0
+  ]
 
 
 /* lsl: used instead of the ARM ARM << over integers */
@@ -154,22 +222,22 @@ val lsl : forall 'm 'n, 'm >= 0 & 'n >= 0. (atom('n), atom('m)) -> atom('n * (2
 function lsl (n, m) = n * (2 ^ m)
 
 /* not_implemented is used to indicate something WE did not implement */
-val not_implemented : string -> unit effect { escape }
+val not_implemented : forall ('a : Type). string -> 'a effect { escape }
 function not_implemented message = exit () /* TODO message */
 
 /* not_implemented_extern is used to indicate something ARM did not define
    and we did not define yet either. Those functions used to be declared as
    external but undefined there. */
-val not_implemented_extern : forall 'a. string -> 'a effect { escape }
+/* val not_implemented_extern : forall 'a. string -> 'a effect { escape } */
+val not_implemented_extern : forall ('a : Type). string -> 'a effect { escape }
 function not_implemented_extern (message) =
   exit ()  /* message; TODO */
 
 /* info is used to convey information to the user */
 val info : string -> unit effect pure
-let info(message) = ()
+function info(message) = ()
 
-struct IMPLEMENTATION_DEFINED_type = 
-{
+struct IMPLEMENTATION_DEFINED_type =  {
   HaveCRCExt : boolean,
   HaveAArch32EL : boolean,
   HaveAnyAArch32 : boolean,
@@ -178,15 +246,15 @@ struct IMPLEMENTATION_DEFINED_type =
   HighestELUsingAArch32 : boolean,
   IsSecureBelowEL3 : boolean,
 }
-let IMPLEMENTATION_DEFINED =
-{
-  HaveCRCExt = true;
-  HaveAArch32EL = false;
-  HaveAnyAArch32 = false;
-  HaveEL2 = false;
-  HaveEL3 = false;
-  HighestELUsingAArch32 = false;
-  IsSecureBelowEL3 = false;
+
+let IMPLEMENTATION_DEFINED : IMPLEMENTATION_DEFINED_type = struct {
+  HaveCRCExt = true,
+  HaveAArch32EL = false,
+  HaveAnyAArch32 = false,
+  HaveEL2 = false,
+  HaveEL3 = false,
+  HighestELUsingAArch32 = false,
+  IsSecureBelowEL3 = false
 }
 
 /* FIXME: ask Kathy what should we do with this */
diff --git a/aarch64_small/armV8_common_lib.sail b/aarch64_small/armV8_common_lib.sail
index a7e14c62..fe719afd 100644
--- a/aarch64_small/armV8_common_lib.sail
+++ b/aarch64_small/armV8_common_lib.sail
@@ -34,12 +34,11 @@
 
 /** FUNCTION:shared/debug/DoubleLockStatus/DoubleLockStatus */
 
-function boolean DoubleLockStatus() =
-{
+function DoubleLockStatus() -> boolean= {
   if ELUsingAArch32(EL1) then
-    (DBGOSDLR.DLK == 1 & DBGPRCR.CORENPDRQ == 0 & ~(Halted()))
+    (DBGOSDLR.DLK() == 0b1 & DBGPRCR.CORENPDRQ() == 0b0 & ~(Halted()))
   else
-    (OSDLR_EL1.DLK == 1 & DBGPRCR_EL1.CORENPDRQ == 0 & ~(Halted()));
+    (OSDLR_EL1.DLK() == 0b1 & DBGPRCR_EL1.CORENPDRQ() == 0b0 & ~(Halted()));
 }
 
 /** FUNCTION:shared/debug/authentication/Debug_authentication */
@@ -48,15 +47,14 @@ function boolean DoubleLockStatus() =
 
 enum signalValue = {LOw, HIGH}
 
-function signalValue signalDBGEN () = not_implemented_extern("signalDBGEN")
-function signalValue signelNIDEN () = not_implemented_extern("signalNIDEN")
-function signalValue signalSPIDEN () = not_implemented_extern("signalSPIDEN")
-function signalValue signalDPNIDEN () = not_implemented_extern("signalSPNIDEN")
+function signalDBGEN () -> signalValue = not_implemented_extern("signalDBGEN")
+function signelNIDEN () -> signalValue = not_implemented_extern("signalNIDEN")
+function signalSPIDEN () -> signalValue = not_implemented_extern("signalSPIDEN")
+function signalDPNIDEN () -> signalValue = not_implemented_extern("signalSPNIDEN")
 
 /** FUNCTION:shared/debug/authentication/ExternalInvasiveDebugEnabled */
 
-function boolean ExternalInvasiveDebugEnabled() =
-{
+function ExternalInvasiveDebugEnabled() -> boolean = {
   /* In the recommended interface, ExternalInvasiveDebugEnabled returns the state of the DBGEN */
   /* signal. */
   signalDBGEN() == HIGH;
@@ -64,8 +62,7 @@ function boolean ExternalInvasiveDebugEnabled() =
 
 /** FUNCTION:shared/debug/authentication/ExternalSecureInvasiveDebugEnabled */
 
-function boolean ExternalSecureInvasiveDebugEnabled() =
-{
+function ExternalSecureInvasiveDebugEnabled() -> boolean = {
   /* In the recommended interface, ExternalSecureInvasiveDebugEnabled returns the state of the */
   /* (DBGEN AND SPIDEN) signal. */
   /* CoreSight allows asserting SPIDEN without also asserting DBGEN, but this is not recommended. */
@@ -76,15 +73,13 @@ function boolean ExternalSecureInvasiveDebugEnabled() =
 
 /** FUNCTION:shared/debug/halting/DCPSInstruction */
 
-function unit DCPSInstruction(target_el : bits(2)) =
-{
+function DCPSInstruction(target_el : bits(2)) -> unit = {
   not_implemented("DCPSInstruction");
 }
 
 /** FUNCTION:shared/debug/halting/DRPSInstruction */
 
-function unit DRPSInstruction() =
-{
+function DRPSInstruction() -> unit = {
   not_implemented("DRPSInstruction");
 }
 
@@ -104,22 +99,19 @@ let DebugHalt_Step_NoSyndrome   =   0b111011
 
 /** FUNCTION:shared/debug/halting/Halt */
 
-function unit Halt(reason : bits(6)) =
-{
+function Halt(reason : bits(6)) -> unit= {
   not_implemented("Halt");
 }
 
 /** FUNCTION:shared/debug/halting/Halted */
 
-function boolean Halted() =
-{
-  ~(EDSCR.STATUS == 0b000001 | EDSCR.STATUS == 0b000010); /* Halted */
+function Halted() -> boolean = {
+  ~(EDSCR.STATUS() == 0b000001 | EDSCR.STATUS() == 0b000010); /* Halted */
 }
 
 /** FUNCTION:shared/debug/halting/HaltingAllowed */
 
-function boolean HaltingAllowed() =
-{
+function HaltingAllowed() -> boolean = {
   if Halted() | DoubleLockStatus() then
     false
   else if IsSecure() then
@@ -130,8 +122,7 @@ function boolean HaltingAllowed() =
 
 /** FUNCTION:shared/exceptions/traps/ReservedValue */
 
-function unit ReservedValue() =
-{
+function ReservedValue() -> unit = {
   /* ARM: uncomment when adding aarch32
   if UsingAArch32() && !AArch32.GeneralExceptionsToAArch64() then
     AArch32.TakeUndefInstrException()
@@ -141,8 +132,7 @@ function unit ReservedValue() =
 
 /** FUNCTION:shared/exceptions/traps/UnallocatedEncoding */
 
-function unit UnallocatedEncoding() =
-{
+function UnallocatedEncoding() -> unit = {
   /* If the unallocated encoding is an AArch32 CP10 or CP11 instruction, FPEXC.DEX must be written */
   /* to zero. This is omitted from this code. */
   /* ARM: uncomment whenimplementing aarch32
@@ -154,74 +144,90 @@ function unit UnallocatedEncoding() =
 
 /** FUNCTION:shared/functions/aborts/IsFault */
 
-function boolean IsFault(addrdesc : AddressDescriptor) =
-{
+function IsFault(addrdesc : AddressDescriptor) ->  boolean= {
     (addrdesc.fault).faulttype != Fault_None;
 }
 
 /** FUNCTION:shared/functions/common/ASR */
 
-val ASR : forall 'N, 'N >= 0. (bits('N), uinteger) -> bits('N)
-function ASR (x, shift) = 
-{
+/* original: */
+
+/* val ASR : forall 'N, 'N >= 0. (bits('N), uinteger) -> bits('N) */
+/* function ASR (x, shift) =  */
+/* { */
+/*   /\*assert shift >= 0;*\/ */
+/*   result : bits('N) = 0; */
+/*   if shift == 0 then */
+/*     result = x */
+/*   else */
+/*     let (result', _) = ASR_C (x, shift) in { result = result' }; */
+/*   result; */
+/* } */
+
+/* CP: replacing this with the slightly simpler one below */
+
+val ASR : forall 'N, 'N >= 1. (bits('N), uinteger) -> bits('N)
+function ASR (x, shift) = {
   /*assert shift >= 0;*/
-  result : bits('N) = 0;
-  if shift == 0 then
-    result = x
-  else
-    let (result', _) = ASR_C (x, shift) in { result = result' };
-  result;
+  if shift == 0 then x
+  else let (result', _) = ASR_C (x, shift) in result'
 }
 
+
 /** FUNCTION:shared/functions/common/ASR_C */
 
-val ASR_C : forall 'N 'S, 'N >= 0 & 'S >= 1. (bits('N), atom('S)) -> (bits('N), bit)
-function ASR_C (x, shift) = 
-{
+val ASR_C : forall 'N 'S, 'N >= 1 & 'S >= 1. (bits('N), atom('S)) -> (bits('N), bit)
+function ASR_C (x, shift) =  {
   /*assert shift > 0;*/
-  extended_x : bits('S+'N) = SignExtend(x);
-  result : bits('N) = extended_x[(shift + length(x) - 1)..shift];
+  extended_x : bits('S+'N) = SignExtend(sizeof('S+'N),x);
+  result : bits('N) = extended_x[(shift + sizeof('N) - 1)..shift];
   carry_out : bit = extended_x[shift - 1];
   (result, carry_out);
 }
 
+/* SignExtend : */
+
+/* 'S+'N > 'N & 'N >= 1. (atom('S+'N),bits('N)) -> bits('S+'N) */
+
+
 /** FUNCTION:integer Align(integer x, integer y) */
 
-function uinteger Align'(x : uinteger, y : uinteger) =
+function Align'(x : uinteger, y : uinteger) -> uinteger =
     y * (quot (x,y))
 
 /** FUNCTION:bits(N) Align(bits(N) x, integer y) */
 
 val Align : forall 'N, 'N >= 0. (bits('N), uinteger) -> bits('N)
 function Align (x, y) =
-    Align'(UInt(x), y) : (bits('N))
+    to_bits (sizeof('N), Align'(UInt(x), y))
 
 /** FUNCTION:integer CountLeadingSignBits(bits(N) x) */
 
-val CountLeadingSignBits : forall 'N, 'N >= 0. bits('N) -> range(0,'N)
+val CountLeadingSignBits : forall 'N, 'N >= 2. bits('N) -> range(0,'N - 1)
 function CountLeadingSignBits(x) =
-  CountLeadingZeroBits(x[(length(x) - 1)..1] ^ x[(length(x) - 2)..0])
+  CountLeadingZeroBits( (x[(sizeof('N) - 1)..1]) ^ 
+                        (x[(sizeof('N) - 2)..0]) )
 
 /** FUNCTION:integer CountLeadingZeroBits(bits(N) x) */
 
 val CountLeadingZeroBits : forall 'N, 'N >= 0. bits('N) -> range(0,'N)
 function CountLeadingZeroBits(x) =
   match HighestSetBit(x) {
-    None  => length(x),
-    Some(n)  => length(x) - 1 - n
+    None()  => sizeof('N),
+    Some(n)  => sizeof('N) - 1 - n
   }
 /** FUNCTION:bits(N) Extend(bits(M) x, integer N, boolean unsigned) */
 
-val Extend : forall 'N 'M, 0 <= 'M & 'M <= 'N. (implicit('N),bits('M),bit) -> bits('N) effect pure
-function Extend (x, unsigned) =
-  if unsigned then ZeroExtend(x) else SignExtend(x)
+val Extend : forall 'N 'M, 1 <= 'M & 'M < 'N. (atom('N),bits('M),bit) -> bits('N) effect pure
+function Extend (n, x, _unsigned) =
+  if _unsigned then ZeroExtend(n,x) else SignExtend(n,x)
 
 /** FUNCTION:integer HighestSetBit(bits(N) x) */
 
-val HighestSetBit : forall 'N, 'N >= 0. bits('N) -> option(range(0, 'N + -1))
+val HighestSetBit : forall 'N, 'N >= 0. bits('N) -> option(range(0, 'N - 1))
 function HighestSetBit(x) = {
   let N = (length(x)) in {
-  result : range(0, 'N + -1) = 0;
+  result : atom(0) = 0;
   break : bool = false;
   foreach (i from (N - 1) downto 0)
     if ~(break) & x[i] == 1 then {
@@ -381,20 +387,18 @@ function SInt(x) = {
 
 /** FUNCTION:bits(N) SignExtend(bits(M) x, integer N) */
 
-val SignExtend : forall 'N 'M, 'N >= 0 & 'M >= 1. bits('M) -> bits('N)
-function SignExtend ([h]:remainder as x) =
+function SignExtend forall 'N 'M, 'N > M & 'M >= 1. (_ : atom('N), ([h]@remainder as x) : bits('M)) -> bits('N) =
   (Replicate([h]) : bits(('N - 'M))) @ x
 
 /** FUNCTION:integer UInt(bits(N) x) */
 
-/* function forall Nat 'N, Nat 'M, 'M = 2**'N. [|'M + -1|] UInt((bits('N)) x) = ([|'M + -1|]) x */
-val Uint : forall 'M 'N, 'M >= 0 & 'N >= 0. bits('N) -> atom('M)
-function UInt(x) = unsigned(x)
+function UInt forall 'N, 'N >=0 . (x : bits('N)) -> range(0, 2 ^ 'N + -1) =
+  unsigned(x)
 
 /** FUNCTION:bits(N) ZeroExtend(bits(M) x, integer N) */
 
-val ZeroExtend : forall 'M 'N, 'M >= 0 & 'N >= 0. bits('M) -> bits('N)
-function ZeroExtend (x) = (Zeros() : bits(('N + 'M * -1))) @ x
+val ZeroExtend : forall 'M 'N, N >= M & 'M >= 0. (atom('N),bits('M)) -> bits('N)
+function ZeroExtend (x) = (Zeros() : bits(('N - 'M))) @ x
 
 /** FUNCTION:shared/functions/common/Zeros */
 
diff --git a/aarch64_small/armV8_lib.h.sail b/aarch64_small/armV8_lib.h.sail
index 3b15a1cd..d2c5d1a5 100644
--- a/aarch64_small/armV8_lib.h.sail
+++ b/aarch64_small/armV8_lib.h.sail
@@ -153,21 +153,22 @@ struct AddressDescriptor = {
 
 enum PrefetchHint = {Prefetch_READ, Prefetch_WRITE, Prefetch_EXEC}
 
-val ASR_C : forall 'N 'S, 'N >= 0 & 'S >= 1. (bits('N),atom('S)) -> (bits('N), bit) effect pure
+val ASR_C : forall 'N 'S, 'N >= 1 & 'S >= 1. (bits('N),atom('S)) -> (bits('N), bit) effect pure
 val LSL_C : forall 'N 'S, 'N >= 0 & 'S >= 1. (bits('N),atom('S)) -> (bits('N), bit) effect pure
 val LSR_C : forall 'N 'S, 'N >= 0 & 'S >= 1. (bits('N),atom('S)) -> (bits('N), bit) effect pure
 val ROR_C : forall 'N 'S, 'N >= 0 & ('S >= 1 | 'S <= -1). (bits('N),int('S)) -> (bits('N), bit) effect pure
 val IsZero : forall 'N, 'N >=0. bits('N) -> boolean effect pure
 val Replicate : forall 'N 'M, 'N >=0 & 'M >=0. (implicit('N),bits('M)) -> bits('N) effect pure
-val SignExtend : forall 'N 'M, 'N >= 'M & 'M >= 0. (implicit('N),bits('M)) -> bits('N) effect pure
-val ZeroExtend : forall 'N 'M, 'N >= 'M & 'M >= 0. (implicit('N),bits('M)) -> bits('N) effect pure
+val SignExtend : forall 'N 'M, 'N > 'M & 'M >= 1. (atom('N),bits('M)) -> bits('N) effect pure
+val ZeroExtend : forall 'N 'M, 'N >= 'M & 'M >= 0. (atom('N),bits('M)) -> bits('N) effect pure
 val Zeros : forall 'N, 'N >=0. implicit('N) -> bits('N) effect pure
 val Ones : forall 'N, 'N >=0. implicit('N) -> bits('N) effect pure
 /* val UInt : forall Nat 'N, Nat 'M, 'M = 2**'N. bits('N) -> [|'M + -1|] effect pure */
-val UInt : forall 'N 'M, 'N >=0 & 'M >= 0. bits('N) -> atom('M) effect pure
+val UInt : forall 'N, 'N >=0 . bits('N) -> range(0, 2 ^ 'N + -1)
+/* val UInt : forall 'N 'M, 'N >=0 & 'M >= 0. bits('N) -> Int('M) effect pure */
 /* val SInt : forall Nat 'N, Nat 'M, Nat 'K, 'M = 'N + -1, 'K = 2**'M. bits('N) -> [|'K * -1:'K + -1|] effect pure */
 val SInt : forall 'N 'M, 'N >= 0 & 'M >=0. bits('N) -> atom('M) effect pure
-val HighestSetBit : forall 'N, 'N >= 0. bits('N+1) -> option(range(0,'N + -1)) effect pure
+val HighestSetBit : forall 'N, 'N >= 0. bits('N) -> option(range(0,'N - 1)) effect pure
 val CountLeadingZeroBits : forall 'N, 'N >= 0. bits('N) -> range(0,'N) effect pure
 val IsSecure : unit -> boolean effect {rreg}
 val IsSecureBelowEL3 : unit -> boolean effect {rreg}
diff --git a/aarch64_small/armV8_pstate.sail b/aarch64_small/armV8_pstate.sail
index dcf35488..9bc88891 100644
--- a/aarch64_small/armV8_pstate.sail
+++ b/aarch64_small/armV8_pstate.sail
@@ -33,61 +33,79 @@
 /*========================================================================*/
 
 /* register alias PSTATE_N   = NZCV.N  /\* Negative condition flag *\/ */
-function set_PSTATE_N(v) = {NZCV.N = v}
-function get_PSTATE_N() = NZCV.N
+val set_PSTATE_N : bits(1) -> unit effect{wreg}
+val get_PSTATE_N : unit -> bits(1) effect{rreg}
+function set_PSTATE_N(v) = {NZCV->N() = v}
+function get_PSTATE_N() = NZCV.N()
 overload PSTATE_N = {set_PSTATE_N, get_PSTATE_N}
 
 /* register alias PSTATE_Z   = NZCV.Z  /\* Zero condition flag *\/ */
-function set_PSTATE_Z(v) = {NZCV.Z = v}
-function get_PSTATE_Z() = NZCV.Z
+val set_PSTATE_Z : bits(1) -> unit effect{wreg}
+val get_PSTATE_Z : unit -> bits(1) effect{rreg}
+function set_PSTATE_Z(v) = {NZCV->Z() = v}
+function get_PSTATE_Z() = NZCV.Z()
 overload PSTATE_Z = {set_PSTATE_Z, get_PSTATE_Z}
 
 /* register alias PSTATE_C   = NZCV.C  /\* Carry condition flag *\/ */
-function set_PSTATE_C(v) = {NZCV.C = v}
-function get_PSTATE_C() = NZCV.C
+val set_PSTATE_C : bits(1) -> unit effect{wreg}
+val get_PSTATE_C : unit -> bits(1) effect{rreg}
+function set_PSTATE_C(v) = {NZCV->C() = v}
+function get_PSTATE_C() = NZCV.C()
 overload PSTATE_C = {set_PSTATE_C, get_PSTATE_C}
 
 /* register alias PSTATE_V   = NZCV.V  /\* oVerflow condition flag *\/ */
-function set_PSTATE_V(v) = {NZCV.V = v}
-function get_PSTATE_V() = NZCV.V
+val set_PSTATE_V : bits(1) -> unit effect{wreg}
+val get_PSTATE_V : unit -> bits(1) effect{rreg}
+function set_PSTATE_V(v) = {NZCV->V() = v}
+function get_PSTATE_V() = NZCV.V()
 overload PSTATE_V = {set_PSTATE_V, get_PSTATE_V}
 
 /* register alias PSTATE_D   = DAIF.D  /\* Debug mask bits(AArch64 only) *\/ */
-function set_PSTATE_D(v) = {NZCV.D = v}
-function get_PSTATE_D() = NZCV.D
+val set_PSTATE_D : bits(1) -> unit effect{wreg}
+val get_PSTATE_D : unit -> bits(1) effect{rreg}
+function set_PSTATE_D(v) = {DAIF->D() = v}
+function get_PSTATE_D() = DAIF.D()
 overload PSTATE_D = {set_PSTATE_D, get_PSTATE_D}
 
 /* register alias PSTATE_A   = DAIF.A  /\* Asynchronous abort mask bit *\/ */
-function set_PSTATE_A(v) = {NZCV.A = v}
-function get_PSTATE_A() = NZCV.A
+val set_PSTATE_A : bits(1) -> unit effect{wreg}
+val get_PSTATE_A : unit -> bits(1) effect{rreg}
+function set_PSTATE_A(v) = {DAIF->A() = v}
+function get_PSTATE_A() = DAIF.A()
 overload PSTATE_A = {set_PSTATE_A, get_PSTATE_A}
 
 /* register alias PSTATE_I   = DAIF.I  /\* IRQ mask bit *\/ */
-function set_PSTATE_I(v) = {NZCV.I = v}
-function get_PSTATE_I() = NZCV.I
+val set_PSTATE_I : bits(1) -> unit effect{wreg}
+val get_PSTATE_I : unit -> bits(1) effect{rreg}
+function set_PSTATE_I(v) = {DAIF->I() = v}
+function get_PSTATE_I() = DAIF.I()
 overload PSTATE_I = {set_PSTATE_I, get_PSTATE_I}
 
 /* register alias PSTATE_F   = DAIF.F  /\* FIQ mask bit *\/ */
-function set_PSTATE_F(v) = {NZCV.F = v}
-function get_PSTATE_F() = NZCV.F
+val set_PSTATE_F : bits(1) -> unit effect{wreg}
+val get_PSTATE_F : unit -> bits(1) effect{rreg}
+function set_PSTATE_F(v) = {DAIF->F() = v}
+function get_PSTATE_F() = DAIF.F()
 overload PSTATE_F = {set_PSTATE_F, get_PSTATE_F}
 
 /*    register alias PSTATE_SS  =         /* Software step bit */ */
 /*    register alias PSTATE_IL  =         /* Illegal execution state bit */ */
 
 /* register alias PSTATE_EL  = CurrentEL.EL /\* Exception Level *\/ */
-function set_PSTATE_EL(v) = {NZCV.EL = v}
-function get_PSTATE_EL() = NZCV.EL
+val set_PSTATE_EL : bits(2) -> unit effect{wreg}
+val get_PSTATE_EL : unit -> bits(2) effect{rreg}
+function set_PSTATE_EL(v) = {CurrentEL->EL() = v}
+function get_PSTATE_EL() = CurrentEL.EL()
 overload PSTATE_EL = {set_PSTATE_EL, get_PSTATE_EL}
 
-/* register PSTATE_nRW : bits(1)           /\* not Register Width: 0=64, 1=32 *\/ */
-function set_PSTATE_nRW(v) = {NZCV.nRW = v}
-function get_PSTATE_nRW() = NZCV.nRW
-overload PSTATE_nRW = {set_PSTATE_nRW, get_PSTATE_nRW}
+register PSTATE_nRW : bits(1)           /* not Register Width: 0=64, 1=32 */
+
 
 /* register alias PSTATE_SP = SPSel.SP /\* Stack pointer select: 0=SP0, 1=SPx [AArch64 only] *\/ /\* TODO: confirm this *\/ */
-function set_PSTATE_SP(v) = {NZCV.SP = v}
-function get_PSTATE_SP() = NZCV.SP
+val set_PSTATE_SP : bits(1) -> unit effect{wreg}
+val get_PSTATE_SP : unit -> bits(1) effect{rreg}
+function set_PSTATE_SP(v) = {SPSel->SP() = v}
+function get_PSTATE_SP() = SPSel.SP()
 overload PSTATE_SP = {set_PSTATE_SP, get_PSTATE_SP}
 
 /*    register alias PSTATE_Q   =         /* Cumulative saturation flag         [AArch32 only] */ */
@@ -95,33 +113,26 @@ overload PSTATE_SP = {set_PSTATE_SP, get_PSTATE_SP}
 /*    register alias PSTATE_IT  =         /* If-then bits, RES0 in CPSR         [AArch32 only] */ */
 /*    register alias PSTATE_J   =         /* J bit, RES0 in CPSR                [AArch32 only, RES0 in ARMv8] */ */
 /*    register alias PSTATE_T   =         /* T32 bit, RES0 in CPSR              [AArch32 only] */ */
-/* register PSTATE_E : bits(1)             /\* Endianness bits(AArch32 only) *\/ */
-function set_PSTATE_E(v) = {NZCV.E = v}
-function get_PSTATE_E() = NZCV.E
-overload PSTATE_E = {set_PSTATE_E, get_PSTATE_E}
+register PSTATE_E : bits(1)             /* Endianness bits(AArch32 only) */
 
-/* register PSTATE_M : bits(5)          /\* Mode field                         [AArch32 only] *\/ */
-function set_PSTATE_M(v) = {NZCV.M = v}
-function get_PSTATE_M() = NZCV.M
-overload PSTATE_M = {set_PSTATE_M, get_PSTATE_M}
+register PSTATE_M : bits(5)          /* Mode field                         [AArch32 only] */
 
 
 /* this is a convenient way to do "PSTATE.<N,Z,C,V> = nzcv;" */
 val wPSTATE_NZCV : (unit, bits(4)) -> unit effect {wreg}
-function wPSTATE_NZCV((), [n,z,c,v]) =
-{
-  PSTATE_N = n;
-  PSTATE_Z = z;
-  PSTATE_C = c;
-  PSTATE_V = v;
+function wPSTATE_NZCV((), [n,z,c,v]) = {
+  PSTATE_N() = [n];
+  PSTATE_Z() = [z];
+  PSTATE_C() = [c];
+  PSTATE_V() = [v];
 }
 
 /* this is a convenient way to do "PSTATE.<D,A,I,F> = daif;" */
 val wPSTATE_DAIF : (unit, bits(4)) -> unit effect {wreg}
 function wPSTATE_DAIF((), [d,a,i,f]) =
 {
-  PSTATE_D = d;
-  PSTATE_A = a;
-  PSTATE_I = i;
-  PSTATE_F = f;
+  PSTATE_D() = [d];
+  PSTATE_A() = [a];
+  PSTATE_I() = [i];
+  PSTATE_F() = [f];
 }
diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail
index 75fdc129..57139190 100644
--- a/aarch64_small/prelude.sail
+++ b/aarch64_small/prelude.sail
@@ -1,18 +1,30 @@
-default Order dec
+/* default Order dec */
 
-union option ('a : Type) = {None : unit, Some : 'a}
+val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
+/* sneaky deref with no effect necessary for bitfield writes */
+val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
+
+/* this is here because if we don't have it before including vector_dec 
+   we get infinite loops caused by interaction with bool/bit casts */
+/* val eq_bit2 = "eq_bit" : (bit, bit) -> bool */
+/* overload operator == = {eq_bit2} */
+
+
+
+$include <smt.sail>
+$include <flow.sail>
+$include <arith.sail>
+$include <option.sail>
+$include <vector_dec.sail>
 
-type bits ('n : Int) = vector('n, dec, bit)
 
 infix 7 >>
 infix 7 <<
+infix 7 ^^
 
 val operator >> = "shift_bits_right" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
 val operator << = "shift_bits_left" : forall 'n 'm. (bits('n), bits('m)) -> bits('n)
 
-
-infix 7 ^^
-
 val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
 val operator ^^ = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
 
@@ -33,4 +45,73 @@ function operator <_s  (x, y) = signed(x) < signed(y)
 function operator >=_s (x, y) = signed(x) >= signed(y)
 function operator <_u  (x, y) = unsigned(x) < unsigned(y)
 function operator >=_u (x, y) = unsigned(x) >= unsigned(y)
-function operator <=_u (x, y) = unsigned(x) <= unsigned(y)
\ No newline at end of file
+function operator <=_u (x, y) = unsigned(x) <= unsigned(y)
+
+val pow2_atom = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
+val pow2_int = "pow2" : int -> int
+
+overload pow2 = {pow2_atom, pow2_int}
+
+
+val cast cast_bool_bit : bool -> bit
+function cast_bool_bit(b) = 
+  match b {
+    true => bitzero,
+    false => bitone
+  }
+
+val cast cast_bit_bool : bit -> bool
+function cast_bit_bool (b) = 
+  match b {
+    bitzero => false,
+    bitone => true
+  }
+
+
+
+
+val and_bits = {c:"and_bits", _: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+overload operator & = {and_bool, and_bits}
+
+
+val not_vec = {c:"not_bits", _:"not_vec"} : forall 'n. bits('n) -> bits('n)
+
+overload ~ = {not_bool, not_vec}
+
+val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", coq: "generic_eq", _:"eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
+overload operator == = {eq_anything}
+
+
+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_atom, neq_int, neq_vec, neq_anything}
+
+
+/* val reg_index : reg_size -> reg_index */
+/* function reg_index x = unsigned(x) */
+
+
+val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : (nat, nat) -> nat
+val quotient = {ocaml: "quotient", lem: "integerDiv"} : (int, int) -> int
+overload quot = {quotient_nat, quotient}
+
+
+val __raw_GetSlice_int = "get_slice_int" : forall 'w, 'w >= 0. (atom('w), int, int) -> bits('w)
+
+val __GetSlice_int : forall 'n, 'n >= 0. (atom('n), int, int) -> bits('n)
+function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o)
+
+val to_bits : forall 'l, 'l >= 0.(atom('l), int) -> bits('l)
+function to_bits (l, n) = __raw_GetSlice_int(l, n, 0)
+
+
+val xor_vec = {c: "xor_bits", _: "xor_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+
+val int_power = {ocaml: "int_power", lem: "pow", coq: "pow", c: "pow_int"} : (int, int) -> int
+
+overload operator ^ = {xor_vec, int_power, concat_str}