Merge branch 'sail2' into rmem_interpreter

18 files changed, 315 insertions, 214 deletions

diff --git a/aarch64_small/armV8.h.sail b/aarch64_small/armV8.h.sail
index ab69f323..d0278d9d 100644
--- a/aarch64_small/armV8.h.sail
+++ b/aarch64_small/armV8.h.sail
@@ -218,7 +218,7 @@ let _V : vector(32,dec,(register(bits(128)))) =
 
 
 /* lsl: used instead of the ARM ARM << over integers */
-val lsl : forall 'm 'n, 'm >= 0 & 'n >= 0. (atom('n), atom('m)) -> atom('n * (2 ^ 'm)) 
+val lsl : forall 'm 'n, 'm >= 0 & 'n >= 0. (int('n), int('m)) -> int('n * (2 ^ 'm)) 
 function lsl (n, m) = n * (2 ^ m)
 
 /* not_implemented is used to indicate something WE did not implement */
diff --git a/aarch64_small/armV8.sail b/aarch64_small/armV8.sail
index b2f493ad..8e893e4b 100644
--- a/aarch64_small/armV8.sail
+++ b/aarch64_small/armV8.sail
@@ -67,33 +67,33 @@ union ast =  {
   BranchRegister : (reg_index,BranchType),
   ExceptionReturn : unit, /* TODO: add to .hgen */
   DebugRestorePState : unit, /* TODO: add to .hgen */
-  LoadLiteral : {'D 'size, RegisterSize('D) & 'size in {1,2,4,8/* ,16 */} & 'size * 8 == 'D. (reg_index,MemOp,boolean,atom('size),bits(64),atom('D))},
-  LoadStoreAcqExc : {'D 'R 'elsize, 'D in {8, 16, 32, 64, 128} & RegisterSize('R) & 'elsize <= 'D. (reg_index,reg_index,reg_index,reg_index,AccType,boolean,boolean,MemOp,atom('elsize),atom('R),atom('D))},
-  LoadStorePairNonTemp : {'D, DataSize('D). (boolean,boolean,reg_index,reg_index,reg_index,AccType,MemOp,uinteger,atom('D),bits(64))},
-  LoadImmediate : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,AccType,MemOp,boolean,boolean,boolean,bits(64),atom('R),atom('D))},
-  LoadRegister : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,reg_index,AccType,MemOp,boolean,boolean,boolean,ExtendType,range(0,3),atom('R),atom('D))},
-  LoadStorePair : {'D, DataSize('D). (boolean,boolean,reg_index,reg_index,reg_index,AccType,MemOp,boolean,atom('D),bits(64))},
-  AddSubImmediate : {'R, RegisterSize('R). (reg_index,reg_index,atom('R),boolean,boolean,bits('R))},
-  BitfieldMove : {'R 'r 's, RegisterSize('R) & 0 <= 'r < 'R & 0 <= 's < 'R. (reg_index,reg_index,atom('R),boolean,boolean,atom('r),atom('s),bits('R),bits('R))},
-  ExtractRegister : {'R 'lsb, RegisterSize('R) & 0 <= 'lsb <= 'R. (reg_index,reg_index,reg_index,atom('R),atom('lsb))},
-  LogicalImmediate : {'R, RegisterSize('R). (reg_index,reg_index,atom('R),boolean,LogicalOp,bits('R))},
-  MoveWide : {'R 'pos, RegisterSize('R) & 0 <= 'pos < div('R, 2). (reg_index,atom('R),bits(16),atom('pos),MoveWideOp)},
+  LoadLiteral : {'D 'size, RegisterSize('D) & 'size in {1,2,4,8/* ,16 */} & 'size * 8 == 'D. (reg_index,MemOp,boolean,int('size),bits(64),int('D))},
+  LoadStoreAcqExc : {'D 'R 'elsize, 'D in {8, 16, 32, 64, 128} & RegisterSize('R) & 'elsize <= 'D. (reg_index,reg_index,reg_index,reg_index,AccType,boolean,boolean,MemOp,int('elsize),int('R),int('D))},
+  LoadStorePairNonTemp : {'D, DataSize('D). (boolean,boolean,reg_index,reg_index,reg_index,AccType,MemOp,uinteger,int('D),bits(64))},
+  LoadImmediate : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,AccType,MemOp,boolean,boolean,boolean,bits(64),int('R),int('D))},
+  LoadRegister : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,reg_index,AccType,MemOp,boolean,boolean,boolean,ExtendType,range(0,3),int('R),int('D))},
+  LoadStorePair : {'D, DataSize('D). (boolean,boolean,reg_index,reg_index,reg_index,AccType,MemOp,boolean,int('D),bits(64))},
+  AddSubImmediate : {'R, RegisterSize('R). (reg_index,reg_index,int('R),boolean,boolean,bits('R))},
+  BitfieldMove : {'R 'r 's, RegisterSize('R) & 0 <= 'r < 'R & 0 <= 's < 'R. (reg_index,reg_index,int('R),boolean,boolean,int('r),int('s),bits('R),bits('R))},
+  ExtractRegister : {'R 'lsb, RegisterSize('R) & 0 <= 'lsb <= 'R. (reg_index,reg_index,reg_index,int('R),int('lsb))},
+  LogicalImmediate : {'R, RegisterSize('R). (reg_index,reg_index,int('R),boolean,LogicalOp,bits('R))},
+  MoveWide : {'R 'pos, RegisterSize('R) & 0 <= 'pos < div('R, 2). (reg_index,int('R),bits(16),int('pos),MoveWideOp)},
   Address : (reg_index,boolean,bits(64)),
-  AddSubExtendRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean,boolean,ExtendType,range(0,7))},
-  AddSubShiftedRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean,boolean,ShiftType,range(0,63))},
-  AddSubCarry : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean,boolean)},
-  ConditionalCompareImmediate : {'R, RegisterSize('R). (reg_index,atom('R),boolean,bits(4),bits(4),bits('R))},
-  ConditionalCompareRegister : {'R, RegisterSize('R). (reg_index,reg_index,atom('R),boolean,bits(4),bits(4))},
-  ConditionalSelect : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),bits(4),boolean,boolean)},
-  Reverse : {'R, RegisterSize('R). (reg_index,reg_index,atom('R),RevOp)},
-  CountLeading : {'R, RegisterSize('R). (reg_index,reg_index,atom('R),CountOp)},
-  Division : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean)},
-  Shift : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),ShiftType)},
-  CRC : {'D, DataSize('D). (reg_index,reg_index,reg_index,atom('D),boolean)},
-  MultiplyAddSub : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,atom('R),atom('R),boolean)},
-  MultiplyAddSubLong : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,atom('R),atom('D),boolean,boolean)},
-  MultiplyHigh : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,atom('R),atom('R),boolean)},
-  LogicalShiftedRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean,LogicalOp,ShiftType,range(0,63),boolean)},
+  AddSubExtendRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,int('R),boolean,boolean,ExtendType,range(0,7))},
+  AddSubShiftedRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,int('R),boolean,boolean,ShiftType,range(0,63))},
+  AddSubCarry : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,int('R),boolean,boolean)},
+  ConditionalCompareImmediate : {'R, RegisterSize('R). (reg_index,int('R),boolean,bits(4),bits(4),bits('R))},
+  ConditionalCompareRegister : {'R, RegisterSize('R). (reg_index,reg_index,int('R),boolean,bits(4),bits(4))},
+  ConditionalSelect : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,int('R),bits(4),boolean,boolean)},
+  Reverse : {'R, RegisterSize('R). (reg_index,reg_index,int('R),RevOp)},
+  CountLeading : {'R, RegisterSize('R). (reg_index,reg_index,int('R),CountOp)},
+  Division : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,int('R),boolean)},
+  Shift : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,int('R),ShiftType)},
+  CRC : {'D, DataSize('D). (reg_index,reg_index,reg_index,int('D),boolean)},
+  MultiplyAddSub : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,int('R),int('R),boolean)},
+  MultiplyAddSubLong : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,int('R),int('D),boolean,boolean)},
+  MultiplyHigh : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,int('R),int('R),boolean)},
+  LogicalShiftedRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,int('R),boolean,LogicalOp,ShiftType,range(0,63),boolean)},
 }
 
 val execute : ast -> unit effect {rreg,wreg,rmem,barr,eamem,wmv,exmem,escape}
@@ -186,7 +186,7 @@ function decodeCompareBranchImmediate ([sf]@0b011010@[op]@(imm19:bits(19))@(Rt:b
   Some(CompareAndBranch(t,datasize,iszero,offset));
 }
 
-function clause execute (CompareAndBranch((t,(datasize as atom('R)),iszero,offset))) = {
+function clause execute (CompareAndBranch((t,(datasize as int('R)),iszero,offset))) = {
   operand1 : bits('R) = rX(datasize,t);
   if IsZero(operand1) == iszero then
     BranchTo(rPC() + offset, BranchType_JMP);
@@ -553,8 +553,8 @@ end decodeImplementationDefined
 val decodeTestBranchImmediate : bits(32) -> option(ast) effect {escape}
 function decodeTestBranchImmediate ([b5]@0b011011@[op]@(b40 : bits(5))@(imm14 : bits(14))@(Rt:bits(5))) = {
   t : reg_index = UInt_reg(Rt);
-
-  let datasize : {| 32, 64 |} /* as atom('R) */ = if b5 == b1 then 64 else 32;
+ 
+  let datasize : {| 32, 64 |} /* as int('R) */ = if b5 == b1 then 64 else 32;
   let bit_pos : uinteger = UInt([b5]@b40);
   bit_val : bit = op;
   offset : bits(64) = SignExtend(imm14@0b00);
@@ -564,7 +564,7 @@ function decodeTestBranchImmediate ([b5]@0b011011@[op]@(b40 : bits(5))@(imm14 :
   Some(TestBitAndBranch((t,datasize,bit_pos,bit_val,offset)));
 }
 
-function clause execute ( TestBitAndBranch((t:reg_index,datasize as atom('R),bit_pos,bit_val,offset)) ) = {
+function clause execute ( TestBitAndBranch((t:reg_index,datasize as int('R),bit_pos,bit_val,offset)) ) = {
 
   /* assert ('R == 32 | 'R == 64); */
 
@@ -696,12 +696,12 @@ function decodeLoadRegisterLiteral ((opc : bits(2))@0b011@0b0@0b00@(imm19 : bits
 
   /* CP: adding let bindings so typechecker has more information */
   let size = size;
-  let datasize /* as atom('D) */ = size*8; /* not in ARM ARM */
+  let datasize /* as int('D) */ = size*8; /* not in ARM ARM */
 
   Some(LoadLiteral(t,memop,_signed,size,offset,datasize));
 }
 
-function clause execute ( LoadLiteral((t,memop,_signed,size,offset,(datasize as atom('D)) )) ) = {
+function clause execute ( LoadLiteral((t,memop,_signed,size,offset,(datasize as int('D)) )) ) = {
   address : bits(64) = rPC() + offset;
   let data = Zeros(datasize); /* ARM: uninitialized */
   match memop {
@@ -759,13 +759,13 @@ function decodeLoadStoreExclusive ((size : bits(2))@0b001000@[o2]@[L]@[o1]@(Rs:b
   let excl : boolean = (o2 == b0);
   let pair : boolean = (o1 == b1);
   let memop : MemOp = if L == b1 then MemOp_LOAD else MemOp_STORE;
-  let size_uint as atom('size) = UInt(size);
-  let elsize : atom(8 * (2 ^ 'size)) = lsl(8, size_uint);
-  let elsize as atom('elsize) = elsize;
+  let size_uint as int('size) = UInt(size);
+  let elsize : int(8 * (2 ^ 'size)) = lsl(8, size_uint);
+  let elsize as int('elsize) = elsize;
   assert(elsize == 8 | elsize == 16 | elsize == 32 | elsize == 64); /*FIXME: CP: adding assertion to make typecheck*/
 
-  let regsize as atom('R) = if elsize == 64 then 64 else 32;
-  let datasize : {'n, 'n in {8,16,32,64,128} & 'elsize <= 'n. atom('n)} = if pair then elsize * 2 else elsize;
+  let regsize as int('R) = if elsize == 64 then 64 else 32;
+  let datasize : {'n, 'n in {8,16,32,64,128} & 'elsize <= 'n. int('n)} = if pair then elsize * 2 else elsize;
 
   /* lemma: pair --> datasize = 2*regsize */
   /* follows from "if o1 == 1 & size[1] == 0 then UnallocatedEncoding();" */
@@ -773,10 +773,10 @@ function decodeLoadStoreExclusive ((size : bits(2))@0b001000@[o2]@[L]@[o1]@(Rs:b
   Some(LoadStoreAcqExc((n,t,t2,s,acctype,excl,pair,memop,elsize,regsize,datasize)));
 }
 
-function clause execute ( LoadStoreAcqExc((n,t,t2,s,acctype,excl,pair,memop,elsize,(regsize as atom('R)),(datasize as atom('D)) ))) = {
+function clause execute ( LoadStoreAcqExc((n,t,t2,s,acctype,excl,pair,memop,elsize,(regsize as int('R)),(datasize as int('D)) ))) = {
   address : bits(64) = Zeros(); /* ARM: uninitialized */
   data : bits('D) = Zeros(datasize); /* ARM: uninitialized */
-  /*constant*/ dbytes : atom(div('D,8)) = quot (datasize,8);
+  /*constant*/ dbytes : int(div('D,8)) = quot (datasize,8);
   rt_unknown : boolean = false;
   rn_unknown : boolean = false;
 
@@ -847,7 +847,7 @@ function clause execute ( LoadStoreAcqExc((n,t,t2,s,acctype,excl,pair,memop,elsi
         data = UNKNOWN_BITS(datasize) /* : bits('D) */
       }
       else if pair then {
-        let halfsize : atom(div('D,2)) = quot(datasize,2);
+        let halfsize : int(div('D,2)) = quot(datasize,2);
         assert( excl ); /* FIXME: CP adding assertion: in the 'pair' case datasize > 8  */
         assert(datasize > 8);
         el1 /* : bits('R) */ = rX(halfsize/* regsize */,t); /* ARM: bits(datasize / 2) see lemma in the decoding */
@@ -960,18 +960,18 @@ function decodeLoadStoreNoAllocatePairOffset ((opc : bits(2))@0b101@0b0@0b000@[L
   memop : MemOp = if L == b1 then MemOp_LOAD else MemOp_STORE;
   if opc[0] == b1 then UnallocatedEncoding();
   let scale : {| 2, 3 |} = 2 + UInt([opc[1]]);
-  let datasize /* : {| 32,64 |} */  /* as atom('D) */ = lsl(8, scale);
+  let datasize /* : {| 32,64 |} */  /* as int('D) */ = lsl(8, scale);
   assert(datasize == 32 | datasize == 64); /*FIXME: CP adding assertion to make typecheck*/
   offset : bits(64) = LSL(SignExtend(imm7), scale);
 
   Some(LoadStorePairNonTemp(wback,postindex,n,t,t2,acctype,memop,scale,datasize,offset));
 }
 
-function clause execute ( LoadStorePairNonTemp((wback,postindex,n,t,t2,acctype,memop,scale,(datasize as atom('D)),offset)) ) = {
+function clause execute ( LoadStorePairNonTemp((wback,postindex,n,t,t2,acctype,memop,scale,(datasize as int('D)),offset)) ) = {
   address : bits(64) = Zeros(); /* ARM: uninitialized */
   data1 : bits('D) = Zeros(); /* ARM: uninitialized */
   data2 : bits('D) = Zeros(); /* ARM: uninitialized */
-  /*constant*/ dbytes : atom(div('D,8)) = quot(datasize,8);
+  /*constant*/ dbytes : int(div('D,8)) = quot(datasize,8);
   rt_unknown : boolean = false;
 
   if memop == MemOp_LOAD & t == t2 then {
@@ -1064,7 +1064,7 @@ function sharedDecodeLoadImmediate (opc : bits(2),size : bits(2), Rn : bits(5),
   acctype : AccType = AccType_NORMAL/AccType_UNPRIV; */
   memop : MemOp = MemOp_LOAD; /* ARM: uninitialized */
   _signed : boolean = false; /* ARM: uninitialized */
-  regsize : { 'R, RegisterSize('R). atom('R) } = 64; /* ARM: uninitialized */
+  regsize : { 'R, RegisterSize('R). int('R) } = 64; /* ARM: uninitialized */
 
   if opc[1] == b0 then {
     /* store or zero-extending load */
@@ -1090,7 +1090,7 @@ function sharedDecodeLoadImmediate (opc : bits(2),size : bits(2), Rn : bits(5),
     };
   };
 
-  let datasize /* : { 'D, DataSize('D). atom('D) } */ = lsl(8, scale);
+  let datasize /* : { 'D, DataSize('D). int('D) } */ = lsl(8, scale);
   assert (datasize == 8 | datasize == 16 | datasize == 32 | datasize == 64); /* FIXME: CP: adding assertion so it typechecks */
 
   Some(LoadImmediate(n,t,acctype,memop,_signed,wback,postindex,offset,regsize,datasize));
@@ -1112,7 +1112,7 @@ function decodeLoadStoreRegisterImmediatePostIndexed ((size:bits(2))@0b111@0b0@0
     (opc,size,Rn,Rt,wback,postindex,scale,offset,AccType_NORMAL,false);
 }
 
-function clause execute ( LoadImmediate ((n,t,acctype,memop,_signed,wback,postindex,offset,regsize as atom('R),datasize as atom('D))) ) = {
+function clause execute ( LoadImmediate ((n,t,acctype,memop,_signed,wback,postindex,offset,regsize as int('R),datasize as int('D))) ) = {
   address : bits(64) = Zeros(); /* ARM: uninitialized */
   data : bits('D) = Zeros(); /* ARM: uninitialized */
   wb_unknown : boolean = false;
@@ -1233,7 +1233,7 @@ function sharedDecodeLoadRegister(Rn:bits(5), Rt:bits(5), Rm:bits(5), opc : bits
   acctype : AccType = AccType_NORMAL;
   memop : MemOp = MemOp_LOAD; /* ARM: uninitialized */
   _signed : boolean = b0; /* ARM: uninitialized */
-  regsize : { 'R, RegisterSize('R). atom('R) }/* atom('R) */ = 64; /* ARM: uninitialized */
+  regsize : { 'R, RegisterSize('R). int('R) }/* int('R) */ = 64; /* ARM: uninitialized */
 
   if opc[1] == b0 then {
     /* store or zero-extending load */
@@ -1253,7 +1253,7 @@ function sharedDecodeLoadRegister(Rn:bits(5), Rt:bits(5), Rm:bits(5), opc : bits
     };
   };
 
-  let datasize /* : {'D, DataSize('D). atom('D)} */ /* : atom('D) */ = lsl(8, scale);
+  let datasize /* : {'D, DataSize('D). int('D)} */ /* : int('D) */ = lsl(8, scale);
   assert (datasize == 8 | datasize == 16 | datasize == 32 | datasize == 64); /* FIXME: CP: adding assertion so it typechecks */
   Some (LoadRegister (n,t,m,acctype,memop,_signed,wback,postindex,extend_type,shift,regsize,datasize));
 }
@@ -1278,7 +1278,7 @@ function decodeLoadStoreRegisterRegisterOffset ((size:bits(2))@0b111@0b0@0b00@(o
   sharedDecodeLoadRegister(Rn,Rt,Rm,opc,size,wback,postindex,scale,extend_type,shift);
 }
 
-function clause execute ( LoadRegister((n,t,m,acctype,memop,_signed,wback,postindex,extend_type,shift,regsize as atom('R),datasize as atom('D))) ) = {
+function clause execute ( LoadRegister((n,t,m,acctype,memop,_signed,wback,postindex,extend_type,shift,regsize as int('R),datasize as int('D))) ) = {
   offset : bits(64) = ExtendReg(m, extend_type, shift);
   address : bits(64) = Zeros(); /* ARM: uninitialized */
   data : bits('D) = Zeros(); /* ARM: uninitialized */
@@ -1437,7 +1437,7 @@ function sharedDecodeLoadStorePair (L:boolean,opc : bits(2),imm7:bits(7),Rn:bits
   if [L,opc[0]] == 0b01 | opc == 0b11 then UnallocatedEncoding();
   _signed : (boolean) = (opc[0] != b0);
   scale : range(2,3) = 2 + UInt([opc[1]]);
-  let datasize /* : { 'D, DataSize('D). atom('D) } */ = lsl(8, scale);
+  let datasize /* : { 'D, DataSize('D). int('D) } */ = lsl(8, scale);
   assert (datasize == 8 | datasize == 16 | datasize == 32 | datasize == 64); /* FIXME: CP: adding assertion so it typechecks */
   offset : (bits(64)) = LSL(SignExtend(imm7), scale);
 
@@ -1455,11 +1455,11 @@ function decodeLoadStoreRegisterPairOffset (opc:bits(2)@0b101@0b0@0b010@[L]@(imm
   sharedDecodeLoadStorePair(L,opc,imm7,Rn,Rt,Rt2,wback,postindex);
 }
 
-function clause execute ( LoadStorePair((wback,postindex,n,t,t2,acctype,memop,_signed,datasize as atom('D),offset)) ) = {
+function clause execute ( LoadStorePair((wback,postindex,n,t,t2,acctype,memop,_signed,datasize as int('D),offset)) ) = {
   address : bits(64) = Zeros(); /* ARM: uninitialized */
   data1 : (bits('D)) = Zeros(); /* ARM: uninitialized */
   data2 : (bits('D)) = Zeros(); /* ARM: uninitialized */
-  /*constant*/ let dbytes : {'db, 'db == div('D,8) & 'db in {1,2,4,8}. atom('db) } = quot (datasize,8);
+  /*constant*/ let dbytes : {'db, 'db == div('D,8) & 'db in {1,2,4,8}. int('db) } = quot (datasize,8);
   rt_unknown : (boolean) = false;
   wb_unknown : (boolean) = false;
 
@@ -1615,7 +1615,7 @@ function decodeAddSubtractImmediate ([sf]@[op]@[S]@0b10001@(shift:bits(2))@(imm1
   Some(AddSubImmediate((d,n,datasize,sub_op,setflags,imm)));
 }
 
-function clause execute (AddSubImmediate((d,n,datasize as atom('R),sub_op,setflags,imm))) = {
+function clause execute (AddSubImmediate((d,n,datasize as int('R),sub_op,setflags,imm))) = {
   operand1 : (bits('R)) = if n == 31 then rSP() else rX(n);
   operand2 : (bits('R)) = imm;
   carry_in : (bit) = b0; /* ARM: uninitialized */
@@ -1647,7 +1647,7 @@ function decodeBitfield ([sf]@(opc:bits(2))@0b100110@[N]@(immr : bits(6))@(imms
   d : (reg_index) = UInt_reg(Rd);
   n : (reg_index) = UInt_reg(Rn);
   let datasize : {|32,64|} = if sf == b1 then 64 else 32;
-  /* let datasize as atom('R) = datasize; */
+  /* let datasize as int('R) = datasize; */
 
   inzero : (boolean) = false; /* ARM: uninitialized */
   extend : (boolean) = false; /* ARM: uninitialized */
@@ -1675,7 +1675,7 @@ function decodeBitfield ([sf]@(opc:bits(2))@0b100110@[N]@(immr : bits(6))@(imms
 }}
 
 
-function clause execute (BitfieldMove((d,n,(datasize as atom('R)),inzero,extend,R,S,wmask,tmask))) = {
+function clause execute (BitfieldMove((d,n,(datasize as int('R)),inzero,extend,R,S,wmask,tmask))) = {
 
   dst : bits('R) = if inzero then Zeros() else rX(d);
   src : bits('R) = rX(n);
@@ -1707,7 +1707,7 @@ function decodeExtract ([sf]@0b00@0b100111@[N]@0b0@(Rm:bits(5))@(imms : bits(6))
   Some(ExtractRegister((d,n,m,datasize,lsb)));
 }
 
-function clause execute ( ExtractRegister((d,n,m,datasize as atom('R),lsb)) ) = {
+function clause execute ( ExtractRegister((d,n,m,datasize as int('R),lsb)) ) = {
   result : (bits('R)) = Zeros(); /* ARM: uninitialized */
   operand1 : (bits('R)) = rX(n);
   operand2 : (bits('R)) = rX(m);
@@ -1724,7 +1724,7 @@ val decodeLogicalImmediate : bits(32) -> option(ast) effect {escape}
 function decodeLogicalImmediate ([sf]@(opc:bits(2))@0b100100@[N]@(immr : bits(6))@(imms : bits(6))@(Rn:bits(5))@(Rd:bits(5))) = {
   d : (reg_index) = UInt_reg(Rd);
   n : (reg_index) = UInt_reg(Rn);
-  let datasize : {|32,64|} /* atom('R) */ = if sf == b1 then 64 else 32;
+  let datasize : {|32,64|} /* int('R) */ = if sf == b1 then 64 else 32;
   setflags : (boolean) = false; /* ARM: uninitialized */
   op : (LogicalOp) = LogicalOp_AND; /* ARM: uninitialized */
   match opc {
@@ -1740,7 +1740,7 @@ function decodeLogicalImmediate ([sf]@(opc:bits(2))@0b100100@[N]@(immr : bits(6)
   Some(LogicalImmediate((d,n,datasize,setflags,op,imm)));
 }}
 
-function clause execute (LogicalImmediate((d,n,datasize as atom('R),setflags,op,imm))) = {
+function clause execute (LogicalImmediate((d,n,datasize as int('R),setflags,op,imm))) = {
   result : (bits('R)) = Zeros(); /* ARM: uninitialized */
   operand1 : (bits('R)) = rX(n);
   operand2 : (bits('R)) = imm;
@@ -1766,7 +1766,7 @@ function clause execute (LogicalImmediate((d,n,datasize as atom('R),setflags,op,
 val decodeMoveWideImmediate : bits(32) -> option(ast) effect {escape}
 function decodeMoveWideImmediate ([sf]@(opc:bits(2))@0b100101@(hw : bits(2))@(imm16 : bits(16))@(Rd:bits(5))) = {
   d : (reg_index) = UInt_reg(Rd);
-  let datasize : {|32,64|} /* : atom('R) */ = if sf == b1 then 64 else 32;
+  let datasize : {|32,64|} /* : int('R) */ = if sf == b1 then 64 else 32;
   imm : (bits(16)) = imm16;
   pos : (uinteger) = 0; /* ARM: uninitialized */
   opcode : (MoveWideOp) = MoveWideOp_N; /* ARM: uninitialized */
@@ -1785,7 +1785,7 @@ function decodeMoveWideImmediate ([sf]@(opc:bits(2))@0b100101@(hw : bits(2))@(im
   Some(MoveWide(d,datasize,imm,pos,opcode));
 }
 
-function clause execute ( MoveWide((d,datasize as atom('R),imm,pos,opcode)) ) = {
+function clause execute ( MoveWide((d,datasize as int('R),imm,pos,opcode)) ) = {
   result : (bits('R)) = Zeros(); /* ARM: uninitialized */
 
   if opcode == MoveWideOp_K then
@@ -1831,7 +1831,7 @@ function decodeAddSubtractExtendedRegister ([sf]@[op]@[S]@0b01011@0b00@0b1@(Rm:b
   d : (reg_index) = UInt_reg(Rd);
   n : (reg_index) = UInt_reg(Rn);
   m : (reg_index) = UInt_reg(Rm);
-  datasize : {|32,64|} /* : atom('R) */ = if sf == b1 then 64 else 32;
+  datasize : {|32,64|} /* : int('R) */ = if sf == b1 then 64 else 32;
   sub_op : (boolean) = (op == b1);
   setflags : (boolean) = (S == b1);
   extend_type : (ExtendType) = DecodeRegExtend(option_v);
@@ -1841,7 +1841,7 @@ function decodeAddSubtractExtendedRegister ([sf]@[op]@[S]@0b01011@0b00@0b1@(Rm:b
   Some(AddSubExtendRegister(d,n,m,datasize,sub_op,setflags,extend_type,shift));
 }
 
-function clause execute (AddSubExtendRegister((d,n,m,datasize as atom('R),sub_op,setflags,extend_type,shift))) = {
+function clause execute (AddSubExtendRegister((d,n,m,datasize as int('R),sub_op,setflags,extend_type,shift))) = {
   operand1 : (bits('R)) = if n == 31 then rSP() else rX(n);
   operand2 : (bits('R)) = ExtendReg(m, extend_type, shift);
   carry_in : (bit) = b0; /* ARM: uninitialized */
@@ -1871,7 +1871,7 @@ function decodeAddSubtractShiftedRegister ([sf]@[op]@[S]@0b01011@(shift:bits(2))
   d : (reg_index) = UInt_reg(Rd);
   n : (reg_index) = UInt_reg(Rn);
   m : (reg_index) = UInt_reg(Rm);
-  datasize : {| 32,64 |} /* : atom('R) */ = if sf == b1 then 64 else 32;
+  datasize : {| 32,64 |} /* : int('R) */ = if sf == b1 then 64 else 32;
   sub_op : (boolean) = (op == b1);
   setflags : (boolean) = (S == b1);
 
@@ -1884,7 +1884,7 @@ function decodeAddSubtractShiftedRegister ([sf]@[op]@[S]@0b01011@(shift:bits(2))
   Some(AddSubShiftedRegister(d,n,m,datasize,sub_op,setflags,shift_type,shift_amount));
 }
 
-function clause execute (AddSubShiftedRegister((d,n,m,(datasize as atom('R)),sub_op,setflags,shift_type,shift_amount))) = {
+function clause execute (AddSubShiftedRegister((d,n,m,(datasize as int('R)),sub_op,setflags,shift_type,shift_amount))) = {
   operand1 : (bits('R)) = rX(n);
   operand2 : (bits('R)) = ShiftReg(m, shift_type, shift_amount);
   carry_in : (bit) = b0; /* ARM: uninitialized */
@@ -1914,14 +1914,14 @@ function decodeAddSubtractWithCarry ([sf]@[op]@[S]@0b11010000@(Rm:bits(5))@0b000
   d : (reg_index) = UInt_reg(Rd);
   n : (reg_index) = UInt_reg(Rn);
   m : (reg_index) = UInt_reg(Rm);
-  datasize : {| 32, 64 |} /* (atom('R)) */ = if sf == b1 then 64 else 32;
+  datasize : {| 32, 64 |} /* (int('R)) */ = if sf == b1 then 64 else 32;
   sub_op : (boolean) = (op == b1);
   setflags : (boolean) = (S == b1);
 
   Some(AddSubCarry(d,n,m,datasize,sub_op,setflags));
 }
 
-function clause execute( AddSubCarry((d,n,m,(datasize as atom('R)),sub_op,setflags))) = {
+function clause execute( AddSubCarry((d,n,m,(datasize as int('R)),sub_op,setflags))) = {
   operand1 : (bits('R)) = rX(n);
   operand2 : (bits('R)) = rX(m);
 
@@ -1941,7 +1941,7 @@ function clause execute( AddSubCarry((d,n,m,(datasize as atom('R)),sub_op,setfla
 val decodeConditionalCompareImmediate : bits(32) -> option(ast) effect pure
 function decodeConditionalCompareImmediate ([sf]@[op]@[b1]@0b11010010@(imm5 : bits(5))@(_cond:bits(4))@[b1]@[b0]@(Rn:bits(5))@[b0]@(nzcv:bits(4))) = {
   n : (reg_index) = UInt_reg(Rn);
-  let datasize : {| 32, 64 |} /* : atom('R) */ = if sf == b1 then 64 else 32;
+  let datasize : {| 32, 64 |} /* : int('R) */ = if sf == b1 then 64 else 32;
   sub_op : boolean = (op == b1);
   condition : bits(4) = _cond;
   flags : bits(4) = nzcv;
@@ -1950,7 +1950,7 @@ function decodeConditionalCompareImmediate ([sf]@[op]@[b1]@0b11010010@(imm5 : bi
   Some(ConditionalCompareImmediate((n,datasize,sub_op,condition,flags,imm)));
 }
 
-function clause execute(ConditionalCompareImmediate((n,datasize as atom('R),sub_op,condition,flags,imm))) = {
+function clause execute(ConditionalCompareImmediate((n,datasize as int('R),sub_op,condition,flags,imm))) = {
   operand1 : (bits('R)) = rX(n);
   operand2 : (bits('R)) = imm;
   carry_in : (bit) = b0;
@@ -1972,7 +1972,7 @@ val decodeConditionalCompareRegister : bits(32) -> option(ast) effect pure
 function decodeConditionalCompareRegister ([sf]@[op]@[b1]@0b11010010@(Rm:bits(5))@ (_cond:bits(4))@[b0]@[b0]@(Rn:bits(5))@[b0]@(nzcv:bits(4))) = {
   n : reg_index = UInt_reg(Rn);
   m : reg_index = UInt_reg(Rm);
-  datasize : {|32,64|} /* : atom('R) */ = if sf == b1 then 64 else 32;
+  datasize : {|32,64|} /* : int('R) */ = if sf == b1 then 64 else 32;
   sub_op : boolean = (op == b1);
   condition : bits(4) = _cond;
   flags : bits(4) = nzcv;
@@ -1980,7 +1980,7 @@ function decodeConditionalCompareRegister ([sf]@[op]@[b1]@0b11010010@(Rm:bits(5)
   Some(ConditionalCompareRegister(n,m,datasize,sub_op,condition,flags));
 }
 
-function clause execute (ConditionalCompareRegister((n,m,datasize as atom('R),sub_op,condition,flags))) = {
+function clause execute (ConditionalCompareRegister((n,m,datasize as int('R),sub_op,condition,flags))) = {
   operand1 : bits('R) = rX(n);
   operand2 : bits('R) = rX(m);
   carry_in : bit = b0;
@@ -2005,7 +2005,7 @@ function decodeConditionalSelect ([sf]@[op]@[b0]@0b11010100@(Rm:bits(5))@(_cond:
   d : (reg_index) = UInt_reg(Rd);
   n : (reg_index) = UInt_reg(Rn);
   m : (reg_index) = UInt_reg(Rm);
-  datasize : {|32,64|}/* (atom('R)) */ = if sf == b1 then 64 else 32;
+  datasize : {|32,64|}/* (int('R)) */ = if sf == b1 then 64 else 32;
   condition : (bits(4)) = _cond;
   else_inv : (boolean) = (op == b1);
   else_inc : (boolean) = (o2 == b1);
@@ -2013,7 +2013,7 @@ function decodeConditionalSelect ([sf]@[op]@[b0]@0b11010100@(Rm:bits(5))@(_cond:
   Some(ConditionalSelect(d,n,m,datasize,condition,else_inv,else_inc));
 }
 
-function clause execute ( ConditionalSelect((d,n,m,datasize as atom('R),condition,else_inv,else_inc)) ) = {
+function clause execute ( ConditionalSelect((d,n,m,datasize as int('R),condition,else_inv,else_inc)) ) = {
   result : (bits('R)) = Zeros(); /* ARM: uninitialized */
   operand1 : (bits('R)) = rX(n);
   operand2 : (bits('R)) = rX(m);
@@ -2040,7 +2040,7 @@ function clause decodeData1Source ([sf]@[b1]@[b0]@0b11010110@0b00000@0b0000@(opc
   d : (reg_index) = UInt_reg(Rd);
   n : (reg_index) = UInt_reg(Rn);
 
-  datasize : {|32,64|}/* (atom('R)) */ = if sf == b1 then 64 else 32;
+  datasize : {|32,64|}/* (int('R)) */ = if sf == b1 then 64 else 32;
 
   op : (RevOp) = RevOp_RBIT; /* ARM: uninitialized */
   match opc {
@@ -2059,7 +2059,7 @@ function clause decodeData1Source ([sf]@[b1]@[b0]@0b11010110@0b00000@0b0000@(opc
   Some(Reverse(d,n,datasize,op));
 }
 
-function clause execute ( Reverse((d,n,datasize as atom('R),op)) ) = {
+function clause execute ( Reverse((d,n,datasize as int('R),op)) ) = {
   result : (bits('R)) = Zeros(); /* ARM uninitialized */
   /* let V : (bits(6)) = Zeros(); /\* ARM uninitialized *\/ */
 
@@ -2096,13 +2096,13 @@ function clause execute ( Reverse((d,n,datasize as atom('R),op)) ) = {
 function clause decodeData1Source ([sf]@[b1]@[b0]@0b11010110@0b00000@0b00010@[op]@(Rn:bits(5))@(Rd:bits(5))) = {
   d : (reg_index) = UInt_reg(Rd);
   n : (reg_index) = UInt_reg(Rn);
-  datasize : {| 32,64 |} /* (atom('R)) */ = if sf == b1 then 64 else 32;
+  datasize : {| 32,64 |} /* (int('R)) */ = if sf == b1 then 64 else 32;
   opcode : (CountOp) = if op == b0 then CountOp_CLZ else CountOp_CLS;
 
   Some(CountLeading(d,n,datasize,opcode));
 }
 
-function clause execute (CountLeading((d,n,datasize as atom('R),opcode))) = {
+function clause execute (CountLeading((d,n,datasize as int('R),opcode))) = {
   result : integer = 0; /* ARM: uninitialized */
   operand1 : (bits('R)) = rX(n);
 
@@ -2125,13 +2125,13 @@ function clause decodeData2Source ([sf]@[b0]@[b0]@0b11010110@(Rm:bits(5))@0b0000
   d : (reg_index) = UInt_reg(Rd);
   n : (reg_index) = UInt_reg(Rn);
   m : (reg_index) = UInt_reg(Rm);
-  datasize : {| 32, 64 |} /* (atom('R)) */ = if sf == b1 then 64 else 32;
+  datasize : {| 32, 64 |} /* (int('R)) */ = if sf == b1 then 64 else 32;
   _unsigned : (boolean) = (o1 == b0);
 
   Some(Division(d,n,m,datasize,_unsigned));
 }
 
-function clause execute ( Division((d,n,m,datasize as atom('R),_unsigned)) ) = {
+function clause execute ( Division((d,n,m,datasize as int('R),_unsigned)) ) = {
   operand1 : (bits('R)) = rX(n);
   operand2 : (bits('R)) = rX(m);
   result : (integer) = 0; /* ARM: uninitialized */
@@ -2152,13 +2152,13 @@ function clause decodeData2Source ([sf]@[b0]@[b0]@0b11010110@(Rm:bits(5))@0b0010
   d : (reg_index) = UInt_reg(Rd);
   n : (reg_index) = UInt_reg(Rn);
   m : (reg_index) = UInt_reg(Rm);
-  datasize : {| 32, 64 |} /* (atom('R)) */ = if sf == b1 then 64 else 32;
+  datasize : {| 32, 64 |} /* (int('R)) */ = if sf == b1 then 64 else 32;
   shift_type : (ShiftType) = DecodeShift(op2);
 
   Some(Shift(d,n,m,datasize,shift_type));
 }
 
-function clause execute (Shift((d,n,m,datasize as atom('R),shift_type))) = {
+function clause execute (Shift((d,n,m,datasize as int('R),shift_type))) = {
   result : (bits('R)) = Zeros(); /* ARM: uninitialized */
   operand2 : (bits('R)) = rX(m);
 
@@ -2174,14 +2174,14 @@ function clause decodeData2Source ([sf]@[b0]@[b0]@0b11010110@(Rm:bits(5))@0b010@
   m : (reg_index) = UInt_reg(Rm);
   if sf == b1 & sz != 0b11 then UnallocatedEncoding();
   if sf == b0 & sz == 0b11 then UnallocatedEncoding();
-  let size /* : {| 8,16,32,64 |} */ /* (atom('D)) */ = lsl(8, UInt(sz)); /* 2-bit size field -> 8, 16, 32, 64 */
+  let size /* : {| 8,16,32,64 |} */ /* (int('D)) */ = lsl(8, UInt(sz)); /* 2-bit size field -> 8, 16, 32, 64 */
   assert (size == 8 | size == 16 | size == 32 | size == 64); /*FIXME: CP adding assertion to make typecheck*/
   crc32c : (boolean) = (C == b1);
 
   Some(CRC(d,n,m,size,crc32c));
 }
 
-function clause execute ( CRC((d,n,m,(size as atom('D)),crc32c)) ) = {
+function clause execute ( CRC((d,n,m,(size as int('D)),crc32c)) ) = {
   if ~(HaveCRCExt()) then
     UnallocatedEncoding();
 
@@ -2208,14 +2208,14 @@ function clause decodeData3Source ([sf]@0b00@0b11011@0b000@(Rm:bits(5))@[o0]@(Ra
   let n : (reg_index) = UInt_reg(Rn);
   let m : (reg_index) = UInt_reg(Rm);
   let a : (reg_index) = UInt_reg(Ra);
-  let destsize /* (atom('R)) */ = if sf == b1 then 64 else 32;
-  let datasize /* (atom('D)) */ = destsize;
+  let destsize /* (int('R)) */ = if sf == b1 then 64 else 32;
+  let datasize /* (int('D)) */ = destsize;
   let sub_op : (boolean) = (o0 == b1);
 
   Some(MultiplyAddSub((d,n,m,a,destsize,datasize,sub_op)));
 }
 
-function clause execute ( MultiplyAddSub((d,n,m,a,destsize as atom('D),datasize as atom('R),sub_op)) ) = {
+function clause execute ( MultiplyAddSub((d,n,m,a,destsize as int('D),datasize as int('R),sub_op)) ) = {
   operand1 : (bits('D)) = rX(n);
   operand2 : (bits('D)) = rX(m);
   operand3 : (bits('R)) = rX(a);
@@ -2239,15 +2239,15 @@ function clause decodeData3Source ([b1]@0b00@0b11011@[U]@0b01@(Rm:bits(5))@[o0]@
   n : (reg_index) = UInt_reg(Rn);
   m : (reg_index) = UInt_reg(Rm);
   a : (reg_index) = UInt_reg(Ra);
-  destsize /* : (atom('R)) */ = 64;
-  datasize /* : (atom('D)) */ = 32;
+  destsize /* : (int('R)) */ = 64;
+  datasize /* : (int('D)) */ = 32;
   sub_op : (boolean) = (o0 == b1);
   _unsigned : (boolean) = (U == b1);
 
   Some(MultiplyAddSubLong(d,n,m,a,destsize,datasize,sub_op,_unsigned));
 }
 
-function clause execute ( MultiplyAddSubLong((d,n,m,a,destsize as atom('R),datasize as atom('D),sub_op,_unsigned)) ) = {
+function clause execute ( MultiplyAddSubLong((d,n,m,a,destsize as int('R),datasize as int('D),sub_op,_unsigned)) ) = {
   operand1 : (bits('D)) = rX(n);
   operand2 : (bits('D)) = rX(m);
   operand3 : (bits('R)) = rX(a);
@@ -2269,14 +2269,14 @@ function clause decodeData3Source ([b1]@0b00@0b11011@[U]@0b10@(Rm:bits(5))@[b0]@
   n : (reg_index) = UInt_reg(Rn);
   m : (reg_index) = UInt_reg(Rm);
   a : (reg_index) = UInt_reg(Ra); /* ignored by UMULH/SMULH */
-  destsize /* : (atom('R)) */ = 64;
-  datasize /* : (atom('D)) */ = destsize;
+  destsize /* : (int('R)) */ = 64;
+  datasize /* : (int('D)) */ = destsize;
   _unsigned : (boolean) = (U == b1);
 
   Some(MultiplyHigh(d,n,m,a,destsize,datasize,_unsigned));
 }
 
-function clause execute ( MultiplyHigh((d,n,m,a,destsize as atom('R),datasize,_unsigned)) ) = {
+function clause execute ( MultiplyHigh((d,n,m,a,destsize as int('R),datasize,_unsigned)) ) = {
   operand1 : (bits('R)) = rX(n);
   operand2 : (bits('R)) = rX(m);
 
@@ -2300,7 +2300,7 @@ function decodeLogicalShiftedRegister ([sf]@(opc:bits(2))@0b01010@(shift:bits(2)
   d : (reg_index) = UInt_reg(Rd);
   n : (reg_index) = UInt_reg(Rn);
   m : (reg_index) = UInt_reg(Rm);
-  datasize : {| 32,64 |} /* : (atom('R)) */ = if sf == b1 then 64 else 32;
+  datasize : {| 32,64 |} /* : (int('R)) */ = if sf == b1 then 64 else 32;
   setflags : (boolean) = false; /* ARM: uninitialized */
   op : (LogicalOp) = LogicalOp_AND; /* ARM: uninitialized */
   match opc {
@@ -2319,7 +2319,7 @@ function decodeLogicalShiftedRegister ([sf]@(opc:bits(2))@0b01010@(shift:bits(2)
   Some(LogicalShiftedRegister((d,n,m,datasize,setflags,op,shift_type,shift_amount,invert)))
 }
 
-function clause execute (LogicalShiftedRegister((d,n,m,datasize as atom('R),setflags,op,shift_type,shift_amount,invert))) = {
+function clause execute (LogicalShiftedRegister((d,n,m,datasize as int('R),setflags,op,shift_type,shift_amount,invert))) = {
 
   operand1 : (bits('R)) = rX(n);
   operand2 : (bits('R)) = ShiftReg(m, shift_type, shift_amount);
diff --git a/aarch64_small/armV8_A64_lib.sail b/aarch64_small/armV8_A64_lib.sail
index 35961c02..ee9eabc9 100644
--- a/aarch64_small/armV8_A64_lib.sail
+++ b/aarch64_small/armV8_A64_lib.sail
@@ -288,7 +288,7 @@ function AArch64_CheckAlignment(address : bits(64), size : uinteger,
 
 /** FUNCTION:// AArch64.MemSingle[] - non-assignment (read) form */
 
-val AArch64_rMemSingle : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64), atom('N), AccType, boolean, bool) -> read_buffer_type effect {escape}
+val AArch64_rMemSingle : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64), int('N), AccType, boolean, bool) -> read_buffer_type effect {escape}
 function AArch64_rMemSingle (read_buffer, address, size, acctype, wasaligned, exclusive) = {
   /*assert size IN {1, 2, 4, 8, 16};*/
   assert(address == Align(address, size));
@@ -310,7 +310,7 @@ function AArch64_rMemSingle (read_buffer, address, size, acctype, wasaligned, ex
 
 /** FUNCTION:// AArch64.MemSingle[] - assignment (write) form */
 
-val AArch64_wMemSingle : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), atom('N), AccType, boolean, bool, bits('N*8)) -> write_buffer_type effect {escape}
+val AArch64_wMemSingle : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), int('N), AccType, boolean, bool, bits('N*8)) -> write_buffer_type effect {escape}
 function AArch64_wMemSingle (write_buffer, address, size, acctype, wasaligned, exclusive, value) = {
   /*assert size IN {1, 2, 4, 8, 16};*/
   assert(address == Align(address, size));
@@ -351,7 +351,7 @@ function CheckSPAlignment() = {
 
 /** FUNCTION://   Mem[] - non-assignment (read) form */
 
-val rMem' : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64),atom('N), AccType, bool) -> read_buffer_type effect {escape,rreg}
+val rMem' : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64),int('N), AccType, bool) -> read_buffer_type effect {escape,rreg}
 function rMem'(read_buffer, address, size, acctype, exclusive) =
 {
   /* ARM: assert size IN {1, 2, 4, 8, 16}; */
@@ -391,11 +391,11 @@ function rMem'(read_buffer, address, size, acctype, exclusive) =
   read_buffer'
 }
 
-val rMem : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64), atom('N), AccType) -> read_buffer_type effect {escape,rreg}
+val rMem : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64), int('N), AccType) -> read_buffer_type effect {escape,rreg}
 function rMem (read_buffer, address, size, acctype) =
   rMem'(read_buffer, address, size, acctype, false)
 
-val rMem_exclusive : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64), atom('N), AccType) -> read_buffer_type effect {escape,rreg}
+val rMem_exclusive : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, bits(64), int('N), AccType) -> read_buffer_type effect {escape,rreg}
 function rMem_exclusive(read_buffer, address, size, acctype) =
   rMem'(read_buffer, address, size, acctype, true)
 
@@ -405,7 +405,7 @@ function rMem_exclusive(read_buffer, address, size, acctype) =
    store-exclusive, this function should only be called indirectly by one
    of the functions that follow it.
    returns true if the store-exclusive was successful. */
-val wMem' : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), atom('N), AccType, bits('N*8), bool) -> write_buffer_type effect {escape,rreg}
+val wMem' : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), int('N), AccType, bits('N*8), bool) -> write_buffer_type effect {escape,rreg}
 function wMem' (write_buffer, address, size, acctype, value, exclusive) = {
   write_buffer' : write_buffer_type = write_buffer;
 
@@ -445,11 +445,11 @@ function wMem' (write_buffer, address, size, acctype, value, exclusive) = {
   write_buffer'
 }
 
-val wMem : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), atom('N), AccType, bits('N*8)) -> write_buffer_type effect {escape,rreg}
+val wMem : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), int('N), AccType, bits('N*8)) -> write_buffer_type effect {escape,rreg}
 function wMem (write_buffer, address, size, acctype, value) =
   wMem'(write_buffer, address, size, acctype, value, false)
 
-val wMem_exclusive : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), atom('N), AccType, bits('N*8)) -> write_buffer_type effect {escape,rreg}
+val wMem_exclusive : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, bits(64), int('N), AccType, bits('N*8)) -> write_buffer_type effect {escape,rreg}
 function wMem_exclusive(write_buffer, address, size, acctype, value) =
   wMem'(write_buffer, address, size, acctype, value, true)
 
@@ -780,7 +780,7 @@ function DecodeRegExtend (op : bits(3)) -> ExtendType = {
 /** FUNCTION:aarch64/instrs/extendreg/ExtendReg */
 
 val ExtendReg : forall 'N 'S, 'N in {8,16,32,64} & 'S >= 0 & 'S <= /* 4 */ 7.
-    (implicit('N), reg_index, ExtendType, atom('S)) -> bits('N) effect {rreg,escape} 
+    (implicit('N), reg_index, ExtendType, int('S)) -> bits('N) effect {rreg,escape} 
 function ExtendReg (N, _reg, etype, shift) = {
   /*assert( shift >= 0 & shift <= 4 );*/
   _val : bits('N) = rX(_reg);
@@ -810,7 +810,7 @@ function ExtendReg (N, _reg, etype, shift) = {
 /** FUNCTION:(bits(M), bits(M)) DecodeBitMasks (bit immN, bits(6) imms, bits(6) immr, boolean immediate) */
 
 val DecodeBitMasks : forall 'M, 'M >= 0 /* & 'E in {2,4,8,16,32,64} */. (implicit('M), bit, bits(6), bits(6), boolean) -> (bits('M), bits('M)) effect {escape} 
-function DecodeBitMasks(M : atom('M), immN : bit, imms : bits(6), immr : bits(6), immediate : boolean) = {
+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 *) */
@@ -837,7 +837,7 @@ function DecodeBitMasks(M : atom('M), immN : bit, imms : bits(6), immr : bits(6)
   let R = UInt (immr & levels);
   let diff : bits(6) = to_bits(S - R); /* 6-bit subtract with borrow */
 
-  let esize as atom('E) = lsl(1, len);
+  let esize as int('E) = lsl(1, len);
   let d /* : bits(6) */ = UInt (diff[(len - 1)..0]);
   assert(esize >= S+1); /* CP: adding this assertion to make typecheck */
   welem : bits('E) = ZeroExtend(Ones(S + 1));
diff --git a/aarch64_small/armV8_common_lib.sail b/aarch64_small/armV8_common_lib.sail
index 5b6cd52e..c2ed72ee 100644
--- a/aarch64_small/armV8_common_lib.sail
+++ b/aarch64_small/armV8_common_lib.sail
@@ -186,7 +186,7 @@ function ASR_C (x, shift) =  {
 
 /* SignExtend : */
 
-/* 'S+'N > 'N & 'N >= 1. (atom('S+'N),bits('N)) -> bits('S+'N) */
+/* 'S+'N > 'N & 'N >= 1. (int('S+'N),bits('N)) -> bits('S+'N) */
 
 
 /** FUNCTION:integer Align(integer x, integer y) */
@@ -314,11 +314,11 @@ function LSR_C(x, shift) = {
 
 /** FUNCTION:integer Min(integer a, integer b) */
 
-val Min : forall 'M 'N.(atom('M), atom('N)) -> min('M,'N)
+val Min : forall 'M 'N.(int('M), int('N)) -> min('M,'N)
 function Min (a,b) =
   if a <= b then a else b
 
-val uMin : forall 'M 'N, 'M >= 0 & 'N >= 0. (atom('M), atom('N)) -> min('M,'N)
+val uMin : forall 'M 'N, 'M >= 0 & 'N >= 0. (int('M), int('N)) -> min('M,'N)
 function uMin (a,b) =
   if a <= b then a else b
 
@@ -537,7 +537,7 @@ function BigEndian() = {
 val BigEndianReverse : forall 'W, 'W in {8,16,32,64,128}. bits('W) -> bits('W) effect pure
 function BigEndianReverse (value) = {
     let 'half = 'W / 2;
-    width : atom('W) = length(value);
+    width : int('W) = length(value);
     /* half : uinteger = width / 2; */
     if width == 8 then value
     else {
@@ -601,15 +601,15 @@ function Hint_Prefetch(addr,hint,target,stream) = ()
 /** FUNCTION:shared/functions/memory/_Mem */
 
 /* regular load */
-/* external */ val rMem_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,atom('N) /*size*/) -> bits('N*8) effect {rmem}
+/* external */ val rMem_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
 /* non-temporal load (LDNP), see ARM ARM for special exception to normal memory ordering rules */
-/* external */ val rMem_STREAM : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,atom('N) /*size*/) -> bits('N*8) effect {rmem}
+/* external */ val rMem_STREAM : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
 /* load-acquire */
-/* external */ val rMem_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,atom('N) /*size*/) -> bits('N*8) effect {rmem}
+/* external */ val rMem_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
 /* load-exclusive */
-/* external */ val rMem_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,atom('N) /*size*/) -> bits('N*8) effect {rmem}
+/* external */ val rMem_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
 /* load-exclusive+acquire */
-/* external */ val rMem_ATOMIC_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,atom('N) /*size*/) -> bits('N*8) effect {rmem}
+/* external */ val rMem_ATOMIC_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/,int('N) /*size*/) -> bits('N*8) effect {rmem}
 
 struct read_buffer_type = {
   acctype : AccType,
@@ -627,7 +627,7 @@ let empty_read_buffer : read_buffer_type =
     address = Zeros()
   }
 
-val _rMem : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, AddressDescriptor, atom('N), AccType, bool) -> read_buffer_type effect {escape}
+val _rMem : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, AddressDescriptor, int('N), AccType, bool) -> read_buffer_type effect {escape}
 function _rMem(read_buffer, desc, size, acctype, exclusive) = {
   if read_buffer.size == 0 then 
     struct { acctype = acctype,
@@ -644,7 +644,7 @@ function _rMem(read_buffer, desc, size, acctype, exclusive) = {
   }
 }
 
-val flush_read_buffer : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, atom('N)) -> bits('N*8) effect {rmem, rreg, escape}
+val flush_read_buffer : forall 'N, 'N in {1,2,4,8,16}. (read_buffer_type, int('N)) -> bits('N*8) effect {rmem, rreg, escape}
 function flush_read_buffer(read_buffer, size) =
 {
   assert(read_buffer.size == size);
@@ -677,15 +677,15 @@ function flush_read_buffer(read_buffer, size) =
 /** FUNCTION:_Mem[AddressDescriptor desc, integer size, AccType acctype] = bits(8*size) value; */
 
 /* regular store */
-/* external */ val wMem_Addr_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, atom('N) /*size*/) -> unit effect {eamem}
+/* external */ val wMem_Addr_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
 /* store-release */
-/* external */ val wMem_Addr_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, atom('N) /*size*/) -> unit effect {eamem}
+/* external */ val wMem_Addr_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
 /* store-exclusive */
-/* external */ val wMem_Addr_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, atom('N) /*size*/) -> unit effect {eamem}
+/* external */ val wMem_Addr_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
 /* store-exclusive+release */
-/* external */ val wMem_Addr_ATOMIC_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, atom('N) /*size*/) -> unit effect {eamem}
+/* external */ val wMem_Addr_ATOMIC_ORDERED : forall 'N, 'N in {1,2,4,8,16}. (bits(64) /*address*/, int('N) /*size*/) -> unit effect {eamem}
 
-val wMem_Addr : forall 'N, 'N in {1,2,4,8,16}. (bits(64), atom('N), AccType, boolean) -> unit effect {eamem, escape}
+val wMem_Addr : forall 'N, 'N in {1,2,4,8,16}. (bits(64), int('N), AccType, boolean) -> unit effect {eamem, escape}
 function wMem_Addr(address, size, acctype, excl) =
 {
   match (excl, acctype) {
@@ -701,9 +701,9 @@ function wMem_Addr(address, size, acctype, excl) =
 
 
 /* regular store */
-/* external */ val wMem_Val_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (atom('N) /*size*/, bits('N*8) /*value*/) -> unit effect {wmv}
+/* external */ val wMem_Val_NORMAL : forall 'N, 'N in {1,2,4,8,16}. (int('N) /*size*/, bits('N*8) /*value*/) -> unit effect {wmv}
 /* store-exclusive */
-/* external */ val wMem_Val_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (atom('N) /*size*/, bits('N*8) /*value*/) -> bool effect {wmv}
+/* external */ val wMem_Val_ATOMIC : forall 'N, 'N in {1,2,4,8,16}. (int('N) /*size*/, bits('N*8) /*value*/) -> bool effect {wmv}
 
 
 struct write_buffer_type = {
@@ -724,7 +724,7 @@ let empty_write_buffer : write_buffer_type = struct {
   value = Zeros()
 }
 
-val _wMem : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, AddressDescriptor, atom('N), AccType, bool, bits('N*8)) -> write_buffer_type effect {escape}
+val _wMem : forall 'N, 'N in {1,2,4,8,16}. (write_buffer_type, AddressDescriptor, int('N), AccType, bool, bits('N*8)) -> write_buffer_type effect {escape}
 function _wMem(write_buffer, desc, size, acctype, exclusive, value) = {
   let s = write_buffer.size;
   if s == 0 then {
diff --git a/aarch64_small/armV8_lib.h.sail b/aarch64_small/armV8_lib.h.sail
index 28be493c..66071b3a 100644
--- a/aarch64_small/armV8_lib.h.sail
+++ b/aarch64_small/armV8_lib.h.sail
@@ -153,10 +153,10 @@ struct AddressDescriptor = {
 
 enum PrefetchHint = {Prefetch_READ, Prefetch_WRITE, Prefetch_EXEC}
 
-val ASR_C : forall 'N 'S, 'N >= 1 & 'S >= 1. (bits('N),atom('S)) -> (bits('N), bit) effect {escape}
-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 >= 1 & 'S >= 1. (bits('N),atom('S)) -> (bits('N), bit) effect pure
-val ROR_C : forall 'N 'S, 'N >= 1 & 'S != 0. (bits('N),atom('S)) -> (bits('N), bit) effect pure
+val ASR_C : forall 'N 'S, 'N >= 1 & 'S >= 1. (bits('N),int('S)) -> (bits('N), bit) effect {escape}
+val LSL_C : forall 'N 'S, 'N >= 0 & 'S >= 1. (bits('N),int('S)) -> (bits('N), bit) effect pure
+val LSR_C : forall 'N 'S, 'N >= 1 & 'S >= 1. (bits('N),int('S)) -> (bits('N), bit) effect pure
+val ROR_C : forall 'N 'S, 'N >= 1 & 'S != 0. (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 >='M & 'M >=0. (implicit('N),bits('M)) -> bits('N) effect {escape}
 val SignExtend : forall 'N 'M, 'N > 'M & 'M >= 1. (implicit('N),bits('M)) -> bits('N) effect {escape}
diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail
index ffb91630..2dbd2bf4 100644
--- a/aarch64_small/prelude.sail
+++ b/aarch64_small/prelude.sail
@@ -35,8 +35,8 @@ overload operator << = {shift_bits_left, shift_left}
 overload operator >> = {shift_bits_right, shift_right}
 
 
-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)
+val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), int('m)) -> bits('n * 'm)
+val operator ^^ = "replicate_bits" : forall 'n 'm. (bits('n), int('m)) -> bits('n * 'm)
 
 
 
@@ -58,7 +58,7 @@ 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)
 
-val pow2_atom = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
+val pow2_atom = "pow2" : forall 'n. int('n) -> int(2 ^ 'n)
 val pow2_int = "pow2" : int -> int
 
 overload pow2 = {pow2_atom, pow2_int}
@@ -125,15 +125,15 @@ overload operator - = {sub_int, sub_vec, sub_vec_int}
 
 
 val quotient_nat = {ocaml: "quotient", lem: "integerDiv"} : 
-    forall 'M 'N, 'M >= 0 & 'N >= 0. (atom('M), atom('N)) -> atom(div('M,'N))
+    forall 'M 'N, 'M >= 0 & 'N >= 0. (int('M), int('N)) -> int(div('M,'N))
 val quotient = {ocaml: "quotient", lem: "integerDiv"} : 
-    forall 'M 'N. (atom('M), atom('N)) -> atom(div('M,'N))
+    forall 'M 'N. (int('M), int('N)) -> int(div('M,'N))
 overload quot = {quotient_nat, quotient}
 
 
-val __raw_GetSlice_int = "get_slice_int" : forall 'w, 'w >= 0. (atom('w), int, int) -> bits('w)
+val __raw_GetSlice_int = "get_slice_int" : forall 'w, 'w >= 0. (int('w), int, int) -> bits('w)
 
-val __GetSlice_int : forall 'n, 'n >= 0. (atom('n), int, int) -> bits('n)
+val __GetSlice_int : forall 'n, 'n >= 0. (int('n), int, int) -> bits('n)
 function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o)
 
 val to_bits : forall 'l, 'l >= 0.(implicit('l), int) -> bits('l)
@@ -158,7 +158,7 @@ val mod = {
   lem: "integerMod",
   c: "tmod_int",
   coq: "Z.rem"
-} : forall 'M 'N. (atom('M), atom('N)) -> {'O, 0 <= 'O & 'O < N . atom('O)}
+} : forall 'M 'N. (int('M), int('N)) -> {'O, 0 <= 'O & 'O < N . int('O)}
 
 /* overload operator % = {mod_int} */
 
@@ -170,7 +170,7 @@ function error(message) = {
   exit()
 }
 
-type min ('M : Int, 'N : Int) = {'O, ('O == 'M | 'O == 'N) & 'O <= 'M & 'O <= 'N. atom('O)}
+type min ('M : Int, 'N : Int) = {'O, ('O == 'M | 'O == 'N) & 'O <= 'M & 'O <= 'N. int('O)}
 
 
 val appendL : forall ('a:Type). (list('a),list('a)) -> list('a)
diff --git a/etc/regfp2.sail b/etc/regfp2.sail
new file mode 100644
index 00000000..85141853
--- /dev/null
+++ b/etc/regfp2.sail
@@ -0,0 +1,97 @@
+/* iR : input registers,
+ * oR : output registers,
+ * aR : registers feeding into the memory address */
+
+/* branch instructions currently are not writing to NIA */
+
+union regfp = {
+   RFull : string,
+   RSlice : (string,nat,nat),
+   RSliceBit : (string,nat),
+   RField : (string,string),
+}
+
+type regfps = list(regfp)
+
+union niafp = {
+  NIAFP_successor : unit,
+  NIAFP_concrete_address : bits(64),
+  NIAFP_indirect_address : unit,
+}
+
+type niafps = list(niafp)
+
+/* only for MIPS */
+union diafp = {
+  DIAFP_none : unit,
+  DIAFP_concrete : bits(64),
+  DIAFP_reg : regfp,
+}
+
+enum read_kind = {
+  Read_plain,
+  Read_reserve,
+  Read_acquire,
+  Read_exclusive,
+  Read_exclusive_acquire,
+  Read_stream,
+  Read_RISCV_acquire,
+  Read_RISCV_strong_acquire,
+  Read_RISCV_reserved,
+  Read_RISCV_reserved_acquire,
+  Read_RISCV_reserved_strong_acquire,
+  Read_X86_locked
+}
+
+enum write_kind = {
+  Write_plain,
+  Write_conditional,
+  Write_release,
+  Write_exclusive,
+  Write_exclusive_release,
+  Write_RISCV_release,
+  Write_RISCV_strong_release,
+  Write_RISCV_conditional,
+  Write_RISCV_conditional_release,
+  Write_RISCV_conditional_strong_release,
+  Write_X86_locked
+}
+
+enum barrier_kind = {
+  Barrier_Sync,
+  Barrier_LwSync,
+  Barrier_Eieio,
+  Barrier_Isync,
+  Barrier_DMB,
+  Barrier_DMB_ST,
+  Barrier_DMB_LD,
+  Barrier_DSB,
+  Barrier_DSB_ST,
+  Barrier_DSB_LD,
+  Barrier_ISB,
+  Barrier_MIPS_SYNC,
+  Barrier_RISCV_rw_rw,
+  Barrier_RISCV_r_rw,
+  Barrier_RISCV_r_r,
+  Barrier_RISCV_rw_w,
+  Barrier_RISCV_w_w,
+  Barrier_RISCV_tso,
+  Barrier_RISCV_i,
+  Barrier_x86_MFENCE
+}
+
+enum trans_kind = {
+  Transaction_start, 
+  Transaction_commit, 
+  Transaction_abort
+}
+
+union instruction_kind = {
+  IK_barrier : barrier_kind,
+  IK_mem_read : read_kind,
+  IK_mem_write : write_kind,
+  IK_mem_rmw : (read_kind, write_kind),
+  IK_branch : unit,
+  IK_trans : trans_kind,
+  IK_simple : unit,
+}
diff --git a/src/sail.ml b/src/sail.ml
index d97cbd22..9cd4d352 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -500,7 +500,7 @@ let main() =
       if !opt_memo_z3 then Constraint.save_digests () else ()
     end
 
-let _ =  try
+let _ = try
     begin
       try ignore (main ())
       with Failure s -> raise (Reporting.err_general Parse_ast.Unknown ("Failure " ^ s))
diff --git a/src/type_check.ml b/src/type_check.ml
index a69d24cf..37a152d4 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -112,7 +112,7 @@ type env =
     mappings : (typquant * typ * typ) Bindings.t;
     typ_vars : (Ast.l * kind_aux) KBindings.t;
     shadow_vars : int KBindings.t;
-    typ_synonyms : (Ast.l -> env -> typ_arg list -> typ_arg) Bindings.t;
+    typ_synonyms : (typquant * typ_arg) Bindings.t;
     overloads : (id list) Bindings.t;
     enums : IdSet.t Bindings.t;
     records : (typquant * (typ * id) list) Bindings.t;
@@ -431,7 +431,7 @@ module Env : sig
   val add_typ_var : l -> kinded_id -> t -> t
   val get_ret_typ : t -> typ option
   val add_ret_typ : typ -> t -> t
-  val add_typ_synonym : id -> (Ast.l -> t -> typ_arg list -> typ_arg) -> t -> t
+  val add_typ_synonym : id -> typquant -> typ_arg -> t -> t
   val get_typ_synonym : id -> t -> Ast.l -> t -> typ_arg list -> typ_arg
   val add_overloads : id -> id list -> t -> t
   val get_overloads : id -> t -> id list
@@ -609,6 +609,53 @@ end = struct
     then ()
     else typ_error env (id_loc id) ("Could not prove " ^ string_of_list ", " string_of_n_constraint ncs ^ " for type constructor " ^ string_of_id id)
 
+  let add_typ_synonym id typq arg env =
+    if Bindings.mem id env.typ_synonyms then
+      typ_error env (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists")
+    else
+      begin
+        typ_print (lazy (adding ^ "type synonym " ^ string_of_id id));
+        { env with typ_synonyms = Bindings.add id (typq, arg) env.typ_synonyms }
+      end
+
+  let mk_synonym typq typ_arg =
+    let kopts, ncs = quant_split typq in
+    let kopts = List.map (fun kopt -> kopt, fresh_existential (unaux_kind (kopt_kind kopt))) kopts in
+    let ncs = List.map (fun nc -> List.fold_left (fun nc (kopt, fresh) -> constraint_subst (kopt_kid kopt) (arg_kopt fresh) nc) nc kopts) ncs in
+    let typ_arg = List.fold_left (fun typ_arg (kopt, fresh) -> typ_arg_subst (kopt_kid kopt) (arg_kopt fresh) typ_arg) typ_arg kopts in
+    let kopts = List.map snd kopts in
+    let rec subst_args env l kopts args =
+      match kopts, args with
+      | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_int_kopt kopt ->
+         let typ_arg, ncs = subst_args env l kopts args in
+         typ_arg_subst (kopt_kid kopt) (arg_nexp arg) typ_arg,
+         List.map (constraint_subst (kopt_kid kopt) (arg_nexp arg)) ncs
+      | kopt :: kopts, A_aux (A_typ arg, _) :: args when is_typ_kopt kopt ->
+         let typ_arg, ncs = subst_args env l kopts args in
+         typ_arg_subst (kopt_kid kopt) (arg_typ arg) typ_arg, ncs
+      | kopt :: kopts, A_aux (A_order arg, _) :: args when is_order_kopt kopt ->
+         let typ_arg, ncs = subst_args env l kopts args in
+         typ_arg_subst (kopt_kid kopt) (arg_order arg) typ_arg, ncs
+      | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_bool_kopt kopt ->
+         let typ_arg, ncs = subst_args env l kopts args in
+         typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs
+      | [], [] -> typ_arg, ncs
+      | _, _ -> typ_error env l "Synonym applied to bad arguments"
+    in
+    fun l env args ->
+    let typ_arg, ncs = subst_args env l kopts args in
+    if (match env.prove with Some prover -> List.for_all (prover env) ncs | None -> false)
+    then typ_arg
+    else typ_error env l ("Could not prove constraints " ^ string_of_list ", " string_of_n_constraint ncs
+                          ^ " in type synonym " ^ string_of_typ_arg typ_arg
+                          ^ " with " ^ Util.string_of_list ", " string_of_n_constraint env.constraints)
+
+  let get_typ_synonym id env =
+    begin match Bindings.find_opt id env.typ_synonyms with
+    | Some (typq, arg) -> mk_synonym typq arg
+    | None -> raise Not_found
+    end
+
   let rec expand_constraint_synonyms env (NC_aux (aux, l) as nc) =
     typ_debug ~level:2 (lazy ("Expanding " ^ string_of_n_constraint nc));
     match aux with
@@ -620,7 +667,7 @@ end = struct
     | NC_bounded_ge (n1, n2) -> NC_aux (NC_bounded_ge (expand_nexp_synonyms env n1, expand_nexp_synonyms env n2), l)
     | NC_app (id, args) ->
        (try
-          begin match Bindings.find id env.typ_synonyms l env args with
+          begin match get_typ_synonym id env l env args with
           | A_aux (A_bool nc, _) -> expand_constraint_synonyms env nc
           | arg -> typ_error env l ("Expected Bool when expanding synonym " ^ string_of_id id ^ " got " ^ string_of_typ_arg arg)
           end
@@ -632,7 +679,7 @@ end = struct
     match aux with
     | Nexp_app (id, args) ->
        (try
-          begin match Bindings.find id env.typ_synonyms l env [] with
+          begin match get_typ_synonym id env l env [] with
           | A_aux (A_nexp nexp, _) -> expand_nexp_synonyms env nexp
           | _ -> typ_error env l ("Expected Int when expanding synonym " ^ string_of_id id)
           end
@@ -640,7 +687,7 @@ end = struct
         | Not_found -> Nexp_aux (Nexp_app (id, List.map (expand_nexp_synonyms env) args), l))
     | Nexp_id id ->
        (try
-          begin match Bindings.find id env.typ_synonyms l env [] with
+          begin match get_typ_synonym id env l env [] with
           | A_aux (A_nexp nexp, _) -> expand_nexp_synonyms env nexp
           | _ -> typ_error env l ("Expected Int when expanding synonym " ^ string_of_id id)
           end
@@ -661,7 +708,7 @@ end = struct
     | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (expand_synonyms env typ1, expand_synonyms env typ2), l)
     | Typ_app (id, args) ->
        (try
-          begin match Bindings.find id env.typ_synonyms l env args with
+          begin match get_typ_synonym id env l env args with
           | A_aux (A_typ typ, _) -> expand_synonyms env typ
           | _ -> typ_error env l ("Expected Type when expanding synonym " ^ string_of_id id)
           end
@@ -669,7 +716,7 @@ end = struct
         | Not_found -> Typ_aux (Typ_app (id, List.map (expand_synonyms_arg env) args), l))
     | Typ_id id ->
        (try
-          begin match Bindings.find id env.typ_synonyms l env [] with
+          begin match get_typ_synonym id env l env [] with
           | A_aux (A_typ typ, _) -> expand_synonyms env typ
           | _ -> typ_error env l ("Expected Type when expanding synonym " ^ string_of_id id)
           end
@@ -1210,17 +1257,6 @@ end = struct
     typ_print (lazy (adding ^ "cast " ^ string_of_id cast));
     { env with casts = cast :: env.casts }
 
-  let add_typ_synonym id synonym env =
-    if Bindings.mem id env.typ_synonyms
-    then typ_error env (id_loc id) ("Type synonym " ^ string_of_id id ^ " already exists")
-    else
-      begin
-        typ_print (lazy (adding ^ "type synonym " ^ string_of_id id));
-        { env with typ_synonyms = Bindings.add id synonym env.typ_synonyms }
-      end
-
-  let get_typ_synonym id env = Bindings.find id env.typ_synonyms
-
   let get_default_order env =
     match env.default_order with
     | None -> typ_error env Parse_ast.Unknown ("No default order has been set")
@@ -4855,44 +4891,13 @@ let check_type_union env variant typq (Tu_aux (tu, l)) =
      |> Env.add_val_spec v (typq, typ')
 
 (* FIXME: This code is duplicated with general kind-checking code in environment, can they be merged? *)
-let mk_synonym typq typ_arg =
-  let kopts, ncs = quant_split typq in
-  let kopts = List.map (fun kopt -> kopt, fresh_existential (unaux_kind (kopt_kind kopt))) kopts in
-  let ncs = List.map (fun nc -> List.fold_left (fun nc (kopt, fresh) -> constraint_subst (kopt_kid kopt) (arg_kopt fresh) nc) nc kopts) ncs in
-  let typ_arg = List.fold_left (fun typ_arg (kopt, fresh) -> typ_arg_subst (kopt_kid kopt) (arg_kopt fresh) typ_arg) typ_arg kopts in
-  let kopts = List.map snd kopts in
-  let rec subst_args env l kopts args =
-    match kopts, args with
-    | kopt :: kopts, A_aux (A_nexp arg, _) :: args when is_int_kopt kopt ->
-       let typ_arg, ncs = subst_args env l kopts args in
-       typ_arg_subst (kopt_kid kopt) (arg_nexp arg) typ_arg,
-       List.map (constraint_subst (kopt_kid kopt) (arg_nexp arg)) ncs
-    | kopt :: kopts, A_aux (A_typ arg, _) :: args when is_typ_kopt kopt ->
-       let typ_arg, ncs = subst_args env l kopts args in
-       typ_arg_subst (kopt_kid kopt) (arg_typ arg) typ_arg, ncs
-    | kopt :: kopts, A_aux (A_order arg, _) :: args when is_order_kopt kopt ->
-       let typ_arg, ncs = subst_args env l kopts args in
-       typ_arg_subst (kopt_kid kopt) (arg_order arg) typ_arg, ncs
-    | kopt :: kopts, A_aux (A_bool arg, _) :: args when is_bool_kopt kopt ->
-       let typ_arg, ncs = subst_args env l kopts args in
-       typ_arg_subst (kopt_kid kopt) (arg_bool arg) typ_arg, ncs
-    | [], [] -> typ_arg, ncs
-    | _, _ -> typ_error env l "Synonym applied to bad arguments"
-  in
-  fun l env args ->
-    let typ_arg, ncs = subst_args env l kopts args in
-    if List.for_all (prove __POS__ env) ncs
-    then typ_arg
-    else typ_error env Parse_ast.Unknown ("Could not prove constraints " ^ string_of_list ", " string_of_n_constraint ncs
-                                      ^ " in type synonym " ^ string_of_typ_arg typ_arg
-                                      ^ " with " ^ string_of_list ", " string_of_n_constraint (Env.get_constraints env))
 
 let rec check_typedef : 'a. Env.t -> 'a type_def -> (tannot def) list * Env.t =
   fun env (TD_aux (tdef, (l, _))) ->
   let td_err () = raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Unimplemented Typedef") in
   match tdef with
   | TD_abbrev (id, typq, typ_arg) ->
-     [DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id (mk_synonym typq typ_arg) env
+     [DEF_type (TD_aux (tdef, (l, None)))], Env.add_typ_synonym id typq typ_arg env
   | TD_record (id, typq, fields, _) ->
      [DEF_type (TD_aux (tdef, (l, None)))], Env.add_record id typq fields env
   | TD_variant (id, typq, arms, _) ->
@@ -5001,13 +5006,6 @@ and check_with_envs : 'a. Env.t -> 'a def list -> (tannot def list * Env.t) list
 let initial_env =
   Env.empty
   |> Env.set_prover (Some (prove __POS__))
-  (* |> Env.add_typ_synonym (mk_id "atom") (fun _ args -> mk_typ (Typ_app (mk_id "range", args @ args))) *)
-
-  (* Internal functions for Monomorphise.AtomToItself *)
-
-  (* |> Env.add_val_spec (mk_id "int")
-   *      (TypQ_aux (TypQ_no_forall, Parse_ast.Unknown), Typ_aux (Typ_bidir (int_typ, string_typ), Parse_ast.Unknown)) *)
-
   |> Env.add_extern (mk_id "size_itself_int") [("_", "size_itself_int")]
   |> Env.add_val_spec (mk_id "size_itself_int")
       (TypQ_aux (TypQ_tq [QI_aux (QI_id (mk_kopt K_int (mk_kid "n")),
diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
index 6ca2fc40..62992f2c 100644
--- a/test/typecheck/pass/Replicate/v2.expect
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -2,7 +2,7 @@ Type error:
 [Replicate/v2.sail]:10:4-30
 10 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Tried performing type coercion from {('ex41# : Int), true. vector(('M * 'ex41#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x)))
+   | Tried performing type coercion from {('ex80# : Int), true. vector(('M * 'ex80#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x)))
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | 
diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect
index c237ae2d..d63918b4 100644
--- a/test/typecheck/pass/exist_synonym/v3.expect
+++ b/test/typecheck/pass/exist_synonym/v3.expect
@@ -1,3 +1,6 @@
 Type error:
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8)
-
+[exist_synonym/v3.sail]:9:38-47
+9 |val test : forall 'n, 0 <= 'n <= 100. regno('n) -> unit
+  |                                      ^-------^
+  | Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= 'n & 'n <= 100), (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8)
+  | 
diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect
index abb232cb..8157c64f 100644
--- a/test/typecheck/pass/exist_synonym/v4.expect
+++ b/test/typecheck/pass/exist_synonym/v4.expect
@@ -1,3 +1,6 @@
 Type error:
-Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8)
-
+[exist_synonym/v4.sail]:9:35-44
+9 |val test : forall 'n, 0 <= 2 <= 4. regno('n) -> unit
+  |                                   ^-------^
+  | Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym int('n) with (0 <= '_x & '_x <= 8), (0 <= '_x#0 & '_x#0 <= 8)
+  | 
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index 1b6239bb..af2cf65f 100644
--- a/test/typecheck/pass/existential_ast/v3.expect
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -3,5 +3,5 @@ Type error:
 26 |  Some(Ctor1(a, x, c))
    |       ^------------^
    | Could not resolve quantifiers for Ctor1
-   | * datasize('ex59#)
+   | * datasize('ex157#)
    | 
diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect
index a1975425..e904aa61 100644
--- a/test/typecheck/pass/existential_ast3/v1.expect
+++ b/test/typecheck/pass/existential_ast3/v1.expect
@@ -4,17 +4,17 @@ Type error:
    |                                                ^---------------^
    | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a))
    | Coercion failed because:
-   | (int(33), int('ex62#)) is not a subtype of (int('ex57#), int('ex58#))
+   | (int(33), int('ex119#)) is not a subtype of (int('ex114#), int('ex115#))
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex57# bound here
+   |    | 'ex114# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex58# bound here
+   |    | 'ex115# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex62# bound here
+   |    | 'ex119# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect
index 1ac6c87c..fdd13607 100644
--- a/test/typecheck/pass/existential_ast3/v2.expect
+++ b/test/typecheck/pass/existential_ast3/v2.expect
@@ -4,17 +4,17 @@ Type error:
    |                                                ^---------------^
    | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a))
    | Coercion failed because:
-   | (int(31), int('ex62#)) is not a subtype of (int('ex57#), int('ex58#))
+   | (int(31), int('ex119#)) is not a subtype of (int('ex114#), int('ex115#))
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex57# bound here
+   |    | 'ex114# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex58# bound here
+   |    | 'ex115# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex62# bound here
+   |    | 'ex119# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect
index 05dcd0a1..2432e632 100644
--- a/test/typecheck/pass/existential_ast3/v3.expect
+++ b/test/typecheck/pass/existential_ast3/v3.expect
@@ -3,5 +3,5 @@ Type error:
 25 |    Some(Ctor(64, unsigned(0b0 @ b @ a)))
    |         ^-----------------------------^
    | Could not resolve quantifiers for Ctor
-   | * (datasize(64) & (0 <= 'ex78# & ('ex78# + 1) <= 64))
+   | * (datasize(64) & (0 <= 'ex158# & ('ex158# + 1) <= 64))
    | 
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index c3b453f2..a63f28f1 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -5,8 +5,8 @@ Type error:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex39# & ('ex39# + 1) <= 3)
+   |    * (0 <= 'ex76# & ('ex76# + 1) <= 3)
    | * plain_vector_access
    |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 'ex42# & ('ex42# + 1) <= 3)
+   |    * (0 <= 'ex79# & ('ex79# + 1) <= 3)
    | 
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index ba2ad410..f37d215f 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -5,8 +5,8 @@ Type error:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex39# & ('ex39# + 1) <= 4)
+   |    * (0 <= 'ex76# & ('ex76# + 1) <= 4)
    | * plain_vector_access
    |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 'ex42# & ('ex42# + 1) <= 4)
+   |    * (0 <= 'ex79# & ('ex79# + 1) <= 4)
    |