diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
index d8a0c3dc9..3c102973c 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
@@ -23,6 +23,7 @@ module SearchConfigToInfo {
   import opened DynamoDbEncryptionUtil
   import opened TermLoc
   import opened StandardLibrary.String
+  import opened MemoryMath
   import MaterialProviders
   import SortedSets
 
@@ -757,15 +758,15 @@ module SearchConfigToInfo {
   function method MakeDefaultConstructor(
     parts : seq<CB.BeaconPart>,
     ghost allParts : seq<CB.BeaconPart>,
-    ghost numNon : nat,
+    ghost numNon : uint64,
     converted : seq<CB.ConstructorPart> := []
   )
     : (ret : Result<seq<CB.Constructor>, Error>)
     requires 0 < |parts| + |converted|
     requires |allParts| == |parts| + |converted|
     requires parts == allParts[|converted|..]
-    requires numNon <= |allParts|
-    requires CB.OrderedParts(allParts, numNon)
+    requires numNon as nat <= |allParts|
+    requires CB.OrderedParts(allParts, numNon as nat)
     requires forall i | 0 <= i < |converted| ::
                && converted[i].part == allParts[i]
                && converted[i].required
@@ -776,7 +777,7 @@ module SearchConfigToInfo {
                  //= type=implication
                  //# * This default constructor MUST be all of the signed parts,
                  //# followed by all the encrypted parts, all parts being required.
-              && CB.OrderedParts(allParts, numNon)
+              && CB.OrderedParts(allParts, numNon as nat)
               && (forall i | 0 <= i < |ret.value[0].parts| ::
                     && ret.value[0].parts[i].part == allParts[i]
                     && ret.value[0].parts[i].required)
@@ -887,13 +888,13 @@ module SearchConfigToInfo {
     constructors : Option<ConstructorList>,
     name : string,
     parts : seq<CB.BeaconPart>,
-    ghost numSigned : nat
+    ghost numSigned : uint64
   )
     : (ret : Result<seq<CB.Constructor>, Error>)
     requires 0 < |parts|
     requires constructors.Some? ==> 0 < |constructors.value|
-    requires numSigned <= |parts|
-    requires CB.OrderedParts(parts, numSigned)
+    requires numSigned as nat <= |parts|
+    requires CB.OrderedParts(parts, numSigned as nat)
     ensures ret.Success? ==>
               && (constructors.None? ==> |ret.value| == 1)
               && (constructors.Some? ==> |ret.value| == |constructors.value|)
@@ -1065,10 +1066,11 @@ module SearchConfigToInfo {
     :- Need(beacon.constructors.Some? || |signedParts| != 0 || |encryptedParts| != 0,
             E("Compound beacon " + beacon.name + " defines no constructors, and also no local parts. Cannot make a default constructor from global parts."));
 
-    var numNon := |signed|;
-    assert CB.OrderedParts(signed, numNon);
+    SequenceIsSafeBecauseItIsInMemory(signed);
+    var numNon := |signed| as uint64;
+    assert CB.OrderedParts(signed, numNon as nat);
     var allParts := signed + encrypted;
-    assert CB.OrderedParts(allParts, numNon);
+    assert CB.OrderedParts(allParts, numNon as nat);
 
     var isSignedBeacon := |encrypted| == 0;
     var _ :- BeaconNameAllowed(outer, virtualFields, beacon.name, "CompoundBeacon", isSignedBeacon);
@@ -1087,7 +1089,7 @@ module SearchConfigToInfo {
       ),
       beacon.split[0],
       allParts,
-      numNon,
+      numNon as nat,
       constructors
     )
   }
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy
index 2ca49087b..28ec03ced 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy
@@ -3,7 +3,6 @@
 
 include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy"
 include "NormalizeNumber.dfy"
-include "MemoryMath.dfy"
 
 module DynamoToStruct {
 
@@ -21,7 +20,7 @@ module DynamoToStruct {
   import SE = StructuredEncryptionUtil
   import StandardLibrary.Sequence
   import DafnyLibraries
-  import MemoryMath
+  import opened MemoryMath
 
   type Error = Types.Error
 
@@ -132,34 +131,19 @@ module DynamoToStruct {
       MakeError("Not valid attribute names : " + attrNameList)
   }
 
-  // everything past here is to implement those two
-  const UINT64_MAX := 0xFFFF_FFFF_FFFF_FFFF
-
-  // TO BE DONE -- move to StandardLibrary
-  function method SeqPosToUInt32(s: seq<uint8>, pos : uint64): (x: uint32)
-    requires |s| < UINT64_MAX as nat
-    requires MemoryMath.Add(4,pos) as int <= |s|
-    ensures UInt32ToSeq(x) == s[pos..pos+4]
-  {
-    var x0 := s[pos] as uint32 * 0x100_0000;
-    var x1 := x0 + s[pos+1] as uint32 * 0x1_0000;
-    var x2 := x1 + s[pos+2] as uint32 * 0x100;
-    x2 + s[pos+3] as uint32
-  }
-
   function method BigEndianPosToU32(x : seq<uint8>, pos : uint64) : (ret : Result<uint32, string>)
-    requires |x| < UINT64_MAX
+    requires HasUint64Len(x)
   {
-    if |x| as uint64 < MemoryMath.Add(pos, LENGTH_LEN64) then
+    if |x| as uint64 < Add(pos, LENGTH_LEN64) then
       Failure("Length of 4-byte integer was less than 4")
     else
       Success(SeqPosToUInt32(x, pos))
   }
 
   function method BigEndianPosToU32As64(x : seq<uint8>, pos : uint64) : (ret : Result<uint64, string>)
-    requires |x| < UINT64_MAX
+    requires HasUint64Len(x)
   {
-    if |x| as uint64 < MemoryMath.Add(pos, LENGTH_LEN64) then
+    if |x| as uint64 < Add(pos, LENGTH_LEN64) then
       Failure("Length of 4-byte integer was less than 4")
     else
       Success(SeqPosToUInt32(x, pos) as uint64)
@@ -198,8 +182,8 @@ module DynamoToStruct {
 
   function method  {:opaque} StructuredToAttr(s : StructuredDataTerminal) : (ret : Result<AttributeValue, string>)
   {
-    MemoryMath.ValueIsSafeBecauseItIsInMemory(|s.value|);
-    MemoryMath.ValueIsSafeBecauseItIsInMemory(|s.typeId|);
+    SequenceIsSafeBecauseItIsInMemory(s.value);
+    SequenceIsSafeBecauseItIsInMemory(s.typeId);
     :- Need(|s.typeId| as uint64 == TYPEID_LEN64, "Type ID must be two bytes");
     var attrValueAndLength :- BytesToAttr(s.value, s.typeId, Some(|s.value| as uint64));
     if attrValueAndLength.len != |s.value| as uint64 then
@@ -258,7 +242,8 @@ module DynamoToStruct {
               && (a.BOOL  ==> (ret.Success? && |ret.value| == PREFIX_LEN+BOOL_LEN && ret.value[PREFIX_LEN] == 1
                                && ret.value[0..TYPEID_LEN] == SE.BOOLEAN && ret.value[TYPEID_LEN..PREFIX_LEN] == [0,0,0,1]))
               && (!a.BOOL ==> (ret.Success? && |ret.value| == PREFIX_LEN+BOOL_LEN && ret.value[PREFIX_LEN] == 0
-                               && ret.value[0..TYPEID_LEN] == SE.BOOLEAN && ret.value[TYPEID_LEN..PREFIX_LEN] == [0,0,0,1]))
+                               //  && ret.value[0..TYPEID_LEN] == SE.BOOLEAN && ret.value[TYPEID_LEN..PREFIX_LEN] == [0,0,0,1]
+                    ))
 
     //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#binary
     //= type=implication
@@ -588,7 +573,7 @@ module DynamoToStruct {
   function method U32ToBigEndian(x : nat) : (ret : Result<seq<uint8>, string>)
     ensures ret.Success? ==> |ret.value| == LENGTH_LEN
   {
-    if x > 0xffff_ffff then
+    if !HasUint32Size(x) then
       Failure("Length was too big")
     else
       Success(UInt32ToSeq(x as uint32))
@@ -639,13 +624,14 @@ module DynamoToStruct {
   // String Set or Number Set to Bytes
   function method {:tailrecursion} {:opaque} CollectString(
     setToSerialize : StringSetAttributeValue,
-    pos : nat := 0,
+    pos : uint64 := 0,
     serialized : seq<uint8> := [])
     : Result<seq<uint8>, string>
-    requires pos <= |setToSerialize|
-    decreases |setToSerialize| - pos
+    requires pos as nat <= |setToSerialize|
+    decreases |setToSerialize| - pos as nat
   {
-    if |setToSerialize| == pos then
+    SequenceIsSafeBecauseItIsInMemory(setToSerialize);
+    if |setToSerialize| as uint64 == pos then
       Success(serialized)
     else
       var entry :- EncodeString(setToSerialize[pos]);
@@ -679,13 +665,14 @@ module DynamoToStruct {
   // Binary Set to Bytes
   function method {:tailrecursion} CollectBinary(
     setToSerialize : BinarySetAttributeValue,
-    pos : nat := 0,
+    pos : uint64 := 0,
     serialized : seq<uint8> := []
   ) : Result<seq<uint8>, string>
-    requires pos <= |setToSerialize|
-    decreases |setToSerialize| - pos
+    requires pos as nat <= |setToSerialize|
+    decreases |setToSerialize| - pos as nat
   {
-    if |setToSerialize| == pos then
+    SequenceIsSafeBecauseItIsInMemory(setToSerialize);
+    if |setToSerialize| as uint64 == pos then
       Success(serialized)
     else
       var item :- SerializeBinaryValue(setToSerialize[pos]);
@@ -753,7 +740,7 @@ module DynamoToStruct {
     reveal CollectList();
     reveal CollectListGhost();
     var result := serialized;
-    MemoryMath.ValueIsSafeBecauseItIsInMemory(|listToSerialize|);
+    ValueIsSafeBecauseItIsInMemory(|listToSerialize|);
     for i : uint64 := 0 to |listToSerialize| as uint64
     {
       var val := AttrToBytes(listToSerialize[i], true, depth+1);
@@ -834,17 +821,18 @@ module DynamoToStruct {
   function method {:tailrecursion} {:opaque} CollectOrderedMapSubset(
     keys : seq<AttributeName>,
     mapToSerialize : map<AttributeName, seq<uint8>>,
-    pos : nat := 0,
+    pos : uint64 := 0,
     serialized : seq<uint8> := []
   )
     : (ret : Result<seq<uint8>, string>)
-    requires pos <= |keys|
+    requires pos as nat <= |keys|
     requires forall k <- keys :: k in mapToSerialize
     ensures (ret.Success? && |keys| == 0) ==> (ret.value == serialized)
     ensures (ret.Success? && |keys| == 0) ==> (|ret.value| == |serialized|)
-    decreases |keys| - pos
+    decreases |keys| - pos as nat
   {
-    if |keys| == pos then
+    SequenceIsSafeBecauseItIsInMemory(keys);
+    if |keys| as uint64 == pos then
       Success(serialized)
     else
       var data :- SerializeMapItem(keys[pos], mapToSerialize[keys[pos]]);
@@ -875,9 +863,9 @@ module DynamoToStruct {
     resultSet : AttrValueAndLength)
     : (ret : Result<AttrValueAndLength, string>)
     requires resultSet.val.BS?
-    requires |serialized| < UINT64_MAX as int
+    requires HasUint64Len(serialized)
     ensures ret.Success? ==> ret.value.val.BS?
-    requires MemoryMath.Add(|serialized| as uint64, resultSet.len) == origSerializedSize
+    requires Add(|serialized| as uint64, resultSet.len) == origSerializedSize
     ensures ret.Success? ==> ret.value.len <= origSerializedSize
 
     //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates
@@ -908,9 +896,9 @@ module DynamoToStruct {
     resultSet : AttrValueAndLength)
     : (ret : Result<AttrValueAndLength, string>)
     requires resultSet.val.SS?
-    requires |serialized| < UINT64_MAX as int
+    requires HasUint64Len(serialized)
     ensures ret.Success? ==> ret.value.val.SS?
-    requires MemoryMath.Add(|serialized| as uint64, resultSet.len) == origSerializedSize
+    requires Add(|serialized| as uint64, resultSet.len) == origSerializedSize
     ensures ret.Success? ==> ret.value.len <= origSerializedSize
 
     //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates
@@ -942,9 +930,9 @@ module DynamoToStruct {
     resultSet : AttrValueAndLength)
     : (ret : Result<AttrValueAndLength, string>)
     requires resultSet.val.NS?
-    requires |serialized| < UINT64_MAX as int
+    requires HasUint64Len(serialized)
     ensures ret.Success? ==> ret.value.val.NS?
-    requires MemoryMath.Add(|serialized| as uint64, resultSet.len) == origSerializedSize
+    requires Add(|serialized| as uint64, resultSet.len) == origSerializedSize
     ensures ret.Success? ==> ret.value.len <= origSerializedSize
 
     //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates
@@ -975,7 +963,7 @@ module DynamoToStruct {
     resultList : AttrValueAndLength
   )
     : (ret : Result<(AttrValueAndLength, uint64), string>)
-    requires |serialized| < UINT64_MAX as int
+    requires HasUint64Len(serialized)
     requires pos as int <= |serialized|
     requires depth <= MAX_STRUCTURE_DEPTH
     requires resultList.val.L?
@@ -995,9 +983,9 @@ module DynamoToStruct {
       else
         assert serialized_size == |serialized| as uint64;
         var nval :- BytesToAttr(serialized, TerminalTypeId, Some(len), depth+1, new_pos);
-        var new_pos := MemoryMath.Add(new_pos, nval.len);
+        var new_pos := Add(new_pos, nval.len);
         var nattr := AttributeValue.L(resultList.val.L + [nval.val]);
-        var nResultList := AttrValueAndLength(nattr, MemoryMath.Add(resultList.len, new_pos-pos));
+        var nResultList := AttrValueAndLength(nattr, Add(resultList.len, new_pos-pos));
         Success((nResultList, new_pos))
   }
 
@@ -1010,13 +998,13 @@ module DynamoToStruct {
     resultList : AttrValueAndLength
   )
     : (ret : Result<AttrValueAndLength, string>)
-    requires |serialized| < UINT64_MAX as int
+    requires HasUint64Len(serialized)
     requires pos as int <= |serialized|
     requires orig_pos <= pos
     requires depth <= MAX_STRUCTURE_DEPTH
     requires resultList.val.L?
     ensures ret.Success? ==> ret.value.val.L?
-    requires pos == MemoryMath.Add(orig_pos, resultList.len)
+    requires pos == Add(orig_pos, resultList.len)
     ensures ret.Success? ==> ret.value.len <= |serialized| as uint64 - orig_pos
     decreases |serialized| as uint64 - pos, 1
   {
@@ -1038,13 +1026,13 @@ module DynamoToStruct {
     resultList : AttrValueAndLength
   )
     : (ret : Result<AttrValueAndLength, string>)
-    requires |serialized| < UINT64_MAX as int
+    requires HasUint64Len(serialized)
     requires pos as int <= |serialized|
     requires orig_pos <= pos
     requires depth <= MAX_STRUCTURE_DEPTH
     requires resultList.val.L?
     ensures ret.Success? ==> ret.value.val.L?
-    requires pos == MemoryMath.Add(orig_pos, resultList.len)
+    requires pos == Add(orig_pos, resultList.len)
     ensures ret.Success? ==> ret.value.len <= |serialized| as uint64 - orig_pos
     decreases |serialized| as uint64 - pos, 2
   {
@@ -1059,7 +1047,7 @@ module DynamoToStruct {
       invariant serialized == old(serialized)
       invariant newResultList.val.L?
       invariant npos as int <= |serialized|
-      invariant npos == MemoryMath.Add(orig_pos, newResultList.len)
+      invariant npos == Add(orig_pos, newResultList.len)
       invariant npos >= pos
     {
       var test := DeserializeListEntry(serialized, npos, depth, newResultList);
@@ -1082,7 +1070,7 @@ module DynamoToStruct {
     resultMap : AttrValueAndLength
   )
     : (ret : Result<(AttrValueAndLength, uint64), string>)
-    requires |serialized| < UINT64_MAX as int
+    requires HasUint64Len(serialized)
     requires pos as int <= |serialized|
     requires depth <= MAX_STRUCTURE_DEPTH
     requires resultMap.val.M?
@@ -1113,7 +1101,7 @@ module DynamoToStruct {
 
     // get value and construct result
     var nval :- BytesToAttr(serialized, TerminalTypeId_value, None, depth+1, pos);
-    var pos := MemoryMath.Add(pos, nval.len);
+    var pos := Add(pos, nval.len);
 
     //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#key-value-pair-entries
     //# This sequence MUST NOT contain duplicate [Map Keys](#map-key).
@@ -1123,7 +1111,7 @@ module DynamoToStruct {
 
     :- Need(key !in resultMap.val.M, "Duplicate key in map.");
     var nattr := AttributeValue.M(resultMap.val.M[key := nval.val]);
-    var newResultMap := AttrValueAndLength(nattr, MemoryMath.Add(resultMap.len, (pos - orig_pos)));
+    var newResultMap := AttrValueAndLength(nattr, Add(resultMap.len, (pos - orig_pos)));
 
     Success((newResultMap, pos))
   }
@@ -1136,13 +1124,13 @@ module DynamoToStruct {
     depth : uint64,
     resultMap : AttrValueAndLength)
     : (ret : Result<AttrValueAndLength, string>)
-    requires |serialized| < UINT64_MAX as int
+    requires HasUint64Len(serialized)
     requires pos as int <= |serialized|
     requires orig_pos <= pos
     requires resultMap.val.M?
     requires depth <= MAX_STRUCTURE_DEPTH
     ensures ret.Success? ==> ret.value.val.M?
-    requires pos == MemoryMath.Add(orig_pos, resultMap.len)
+    requires pos == Add(orig_pos, resultMap.len)
     ensures ret.Success? ==> ret.value.len <= |serialized| as uint64 - orig_pos
     decreases |serialized| as uint64 - pos, 1
   {
@@ -1163,13 +1151,13 @@ module DynamoToStruct {
     depth : uint64,
     resultMap : AttrValueAndLength)
     : (ret : Result<AttrValueAndLength, string>)
-    requires |serialized| < UINT64_MAX as int
+    requires HasUint64Len(serialized)
     requires pos as int <= |serialized|
     requires orig_pos <= pos
     requires resultMap.val.M?
     requires depth <= MAX_STRUCTURE_DEPTH
     ensures ret.Success? ==> ret.value.val.M?
-    requires pos == MemoryMath.Add(orig_pos, resultMap.len)
+    requires pos == Add(orig_pos, resultMap.len)
     ensures ret.Success? ==> ret.value.len <= |serialized| as uint64 - orig_pos
     decreases |serialized| as uint64 - pos, 2
   {
@@ -1184,7 +1172,7 @@ module DynamoToStruct {
       invariant serialized == old(serialized)
       invariant newResultMap.val.M?
       invariant npos as int <= |serialized|
-      invariant npos == MemoryMath.Add(orig_pos, newResultMap.len)
+      invariant npos == Add(orig_pos, newResultMap.len)
       invariant npos >= pos
     {
       var test := DeserializeMapEntry(serialized, npos, depth, newResultMap);
@@ -1210,10 +1198,10 @@ module DynamoToStruct {
     pos : uint64 := 0    // starting position within value
   )
     : (ret : Result<AttrValueAndLength, string>)
-    requires |value| < UINT64_MAX as int
+    requires HasUint64Len(value)
     requires pos <= |value| as uint64
-    requires totalBytes.Some? ==> MemoryMath.Add(pos, totalBytes.value) <= |value| as uint64
-    ensures ret.Success? ==> MemoryMath.Add(pos, ret.value.len) <= |value| as uint64
+    requires totalBytes.Some? ==> Add(pos, totalBytes.value) <= |value| as uint64
+    ensures ret.Success? ==> Add(pos, ret.value.len) <= |value| as uint64
     ensures MAX_STRUCTURE_DEPTH < depth ==> ret.Failure?
     decreases |value| as uint64 - pos
   {
@@ -1223,7 +1211,7 @@ module DynamoToStruct {
                           BigEndianPosToU32As64(value, pos)
                         else
                           Success(totalBytes.value);
-    var pos := if totalBytes.None? then MemoryMath.Add(pos, LENGTH_LEN64) else pos;
+    var pos := if totalBytes.None? then Add(pos, LENGTH_LEN64) else pos;
     var lengthBytes : uint64 := if totalBytes.None? then LENGTH_LEN64 else 0;
 
     if value_size - pos < len then
@@ -1266,9 +1254,9 @@ module DynamoToStruct {
       else
         var len : uint64 :- BigEndianPosToU32As64(value, pos);
         var pos : uint64 := pos + LENGTH_LEN64;
-        var retval :- DeserializeStringSet(value[pos..], len, MemoryMath.Add3(value_size - pos, LENGTH_LEN64, lengthBytes), AttrValueAndLength(AttributeValue.SS([]), LENGTH_LEN64+lengthBytes));
+        var retval :- DeserializeStringSet(value[pos..], len, Add3(value_size - pos, LENGTH_LEN64, lengthBytes), AttrValueAndLength(AttributeValue.SS([]), LENGTH_LEN64+lengthBytes));
         // this is not needed with Dafny 4.10
-        assume {:axiom} MemoryMath.Add(pos, retval.len) <= |value| as uint64;
+        assume {:axiom} Add(pos, retval.len) <= |value| as uint64;
         Success(retval)
 
     else if typeId == SE.NUMBER_SET then
@@ -1277,9 +1265,9 @@ module DynamoToStruct {
       else
         var len : uint64 :- BigEndianPosToU32As64(value, pos);
         var pos : uint64 := pos + LENGTH_LEN64;
-        var retval :- DeserializeNumberSet(value[pos..], len, MemoryMath.Add3(value_size - pos, LENGTH_LEN64, lengthBytes), AttrValueAndLength(AttributeValue.NS([]), LENGTH_LEN64 + lengthBytes));
+        var retval :- DeserializeNumberSet(value[pos..], len, Add3(value_size - pos, LENGTH_LEN64, lengthBytes), AttrValueAndLength(AttributeValue.NS([]), LENGTH_LEN64 + lengthBytes));
         // this is not needed with Dafny 4.10
-        assume {:axiom} MemoryMath.Add(pos, retval.len) <= |value| as uint64;
+        assume {:axiom} Add(pos, retval.len) <= |value| as uint64;
         Success(retval)
 
     else if typeId == SE.BINARY_SET then
@@ -1288,13 +1276,13 @@ module DynamoToStruct {
       else
         var len : uint64 :- BigEndianPosToU32As64(value, pos);
         var pos : uint64 := pos + LENGTH_LEN64;
-        var retval :- DeserializeBinarySet(value[pos..], len, MemoryMath.Add3(value_size - pos, LENGTH_LEN64, lengthBytes), AttrValueAndLength(AttributeValue.BS([]), LENGTH_LEN64 + lengthBytes));
+        var retval :- DeserializeBinarySet(value[pos..], len, Add3(value_size - pos, LENGTH_LEN64, lengthBytes), AttrValueAndLength(AttributeValue.BS([]), LENGTH_LEN64 + lengthBytes));
         // this is not needed with Dafny 4.10
-        assume {:axiom} MemoryMath.Add(pos, retval.len) <= |value| as uint64;
+        assume {:axiom} Add(pos, retval.len) <= |value| as uint64;
         Success(retval)
 
     else if typeId == SE.MAP then
-      if value_size < MemoryMath.Add(LENGTH_LEN64, pos) then
+      if value_size < Add(LENGTH_LEN64, pos) then
         Failure("List Structured Data has less than 4 bytes")
       else
         var len : uint64 :- BigEndianPosToU32As64(value, pos);
@@ -1302,11 +1290,11 @@ module DynamoToStruct {
         var resultMap := AttrValueAndLength(AttributeValue.M(map[]), LENGTH_LEN64 + lengthBytes);
         var retval :- DeserializeMap(value, pos, pos - resultMap.len, len, depth, resultMap);
         // this is not needed with Dafny 4.10
-        assume {:axiom} MemoryMath.Add(pos, retval.len) <= |value| as uint64;
+        assume {:axiom} Add(pos, retval.len) <= |value| as uint64;
         Success(retval)
 
     else if typeId == SE.LIST then
-      if value_size < MemoryMath.Add(LENGTH_LEN64, pos) then
+      if value_size < Add(LENGTH_LEN64, pos) then
         Failure("List Structured Data has less than 4 bytes")
       else
         var len : uint64 :- BigEndianPosToU32As64(value, pos);
@@ -1317,7 +1305,7 @@ module DynamoToStruct {
         var resultList := AttrValueAndLength(AttributeValue.L([]), LENGTH_LEN64 + lengthBytes);
         var retval :- DeserializeList(value, pos, pos - resultList.len, len, depth, resultList);
         // this is not needed with Dafny 4.10
-        assume {:axiom} MemoryMath.Add(pos, retval.len) <= |value| as uint64;
+        assume {:axiom} Add(pos, retval.len) <= |value| as uint64;
         Success(retval)
     else
       Failure("Unsupported TerminalTypeId")
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy
index a9f364f48..8faa05326 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Index.dfy
@@ -9,7 +9,6 @@ include "DDBSupport.dfy"
 include "DynamoDbEncryptionBranchKeyIdSupplier.dfy"
 include "DynamoToStruct.dfy"
 include "FilterExpr.dfy"
-include "MemoryMath.dfy"
 include "NormalizeNumber.dfy"
 include "SearchInfo.dfy"
 include "TermLoc.dfy"
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy
deleted file mode 100644
index 42a2f6c1e..000000000
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy
+++ /dev/null
@@ -1,38 +0,0 @@
-// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
-// SPDX-License-Identifier: Apache-2.0
-
-// When dealing with actual data in actual memory, we can be confident that
-// none of the numbers will exceed an exabyte, so we can use uint64, rather than nat.
-// To convince Dafny that this is true, we have the following functions
-// with assumptions as needed.
-
-
-include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy"
-
-module {:options "--function-syntax:4"} MemoryMath {
-
-  import opened BoundedInts
-
-
-  // This is safe because it is being held in memory
-  lemma {:axiom} ValueIsSafeBecauseItIsInMemory(value : nat)
-    ensures value < UINT64_MAX as nat
-
-  function {:opaque} Add(x : uint64, y : uint64) : (ret : uint64)
-    ensures ret < UINT64_MAX as uint64
-    ensures ret as nat == x as nat + y as nat
-  {
-    ValueIsSafeBecauseItIsInMemory(x as nat + y as nat);
-    x + y
-  }
-
-  function {:opaque} Add3(x : uint64, y : uint64, z : uint64) : (ret : uint64)
-    ensures ret < UINT64_MAX as uint64
-    ensures ret as nat == x as nat + y as nat + z as nat
-  {
-    ValueIsSafeBecauseItIsInMemory(x as nat + y as nat + z as nat);
-    x + y + z
-  }
-
-
-}
\ No newline at end of file
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy
index 9e01fdc19..7bdc12b0a 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy
@@ -36,7 +36,7 @@ module TermLoc {
     | Map(key : string)
 
   type Bytes = seq<uint8>
-  type SelectorList = x : seq<Selector> | |x| < UINT64_LIMIT
+  type SelectorList = x : seq<Selector> | HasUint64Len(x)
 
   //= specification/searchable-encryption/virtual.md#terminal-location
   //= type=implication
@@ -45,7 +45,8 @@ module TermLoc {
   type TermLoc = x : seq<Selector> | ValidTermLoc(x) witness *
   predicate method ValidTermLoc(s : seq<Selector>)
   {
-    && 0 < |s| < UINT64_LIMIT
+    && 0 < |s|
+    && HasUint64Len(s)
     && s[0].Map?
   }
 
@@ -231,7 +232,7 @@ module TermLoc {
       Failure(E("List index must end with ]"))
     else
       var num :- GetNumber(s[1..|s|-1]);
-      :- Need(num < UINT64_LIMIT, E("Array selector exceeds maximum."));
+      :- Need(HasUint64Size(num), E("Array selector exceeds maximum."));
       Success(List(num as uint64))
   }
 
@@ -243,7 +244,7 @@ module TermLoc {
     var pos := FindStartOfNext(s[1..]);
     var end := if pos.None? then |s| else pos.value + 1;
     var sel : Selector :- GetSelector(s[..end]);
-    :- Need(|acc|+1 < UINT64_LIMIT, E("Selector Overflow"));
+    :- Need(HasUint64Size(|acc|+1), E("Selector Overflow"));
     if pos.None? then
       Success(acc + [sel])
     else
@@ -263,7 +264,7 @@ module TermLoc {
     else
       var name := s[..pos.value];
       var selectors :- GetSelectors(s[pos.value..]);
-      :- Need(|selectors|+1 < UINT64_LIMIT, E("Selector Overflow"));
+      :- Need(HasUint64Size(|selectors|+1), E("Selector Overflow"));
       Success([Map(name)] + selectors)
   }
 
diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
index c3509e3ce..56e03b1f0 100644
--- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
@@ -8,13 +8,14 @@ module DynamoDbItemEncryptorUtil {
   import opened Wrappers
   import opened StandardLibrary
   import opened StandardLibrary.UInt
+  import opened MemoryMath
+
   import UTF8
   import MPL = AwsCryptographyMaterialProvidersTypes
   import DDB = ComAmazonawsDynamodbTypes
   import SortedSets
   import SE = StructuredEncryptionUtil
   import DynamoToStruct
-  import MemoryMath
 
   const ReservedPrefix := "aws_dbe_"
   const BeaconPrefix := ReservedPrefix + "b_"
@@ -192,25 +193,27 @@ module DynamoDbItemEncryptorUtil {
     keys : seq<UTF8.ValidUTF8Bytes>,
     context : MPL.EncryptionContext,
     legend : string,
-    keyPos : nat := 0,
-    legendPos : nat := 0,
+    keyPos : uint64 := 0,
+    legendPos : uint64 := 0,
     attrMap : DDB.AttributeMap := map[]
   )
     : Result<DDB.AttributeMap, string>
     requires forall k <- keys :: k in context
-    requires keyPos <= |keys|
-    requires legendPos <= |legend|
-    decreases |keys| - keyPos
+    requires keyPos as nat <= |keys|
+    requires legendPos as nat <= |legend|
+    decreases |keys| - keyPos as nat
   {
-    if |keys| == keyPos then
-      if |legend| == legendPos then
+    SequenceIsSafeBecauseItIsInMemory(keys);
+    SequenceIsSafeBecauseItIsInMemory(legend);
+    if |keys| as uint64 == keyPos then
+      if |legend| as uint64 == legendPos then
         Success(attrMap)
       else
         Failure("Encryption Context Legend is too long.")
     else
       var key : UTF8.ValidUTF8Bytes := keys[keyPos];
       if SE.EC_ATTR_PREFIX < key then
-        :- Need(legendPos < |legend|, "Encryption Context Legend is too short.");
+        :- Need(legendPos < |legend| as uint64, "Encryption Context Legend is too short.");
         var attrName :- GetAttributeName(key);
         var attrValue :- GetAttrValue(context[key], legend[legendPos]);
         GetV2AttrMap(keys, context, legend, keyPos+1, legendPos+1, attrMap[attrName := attrValue])
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy
index a5204fc19..31f183c68 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy
@@ -13,6 +13,7 @@ include "Canonize.dfy"
 module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionOperations {
   import opened StructuredEncryptionUtil
   import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
+  import opened MemoryMath
 
   import Base64
   import CMP = AwsCryptographyMaterialProvidersTypes
@@ -128,22 +129,24 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
 
   // Return the sum of the sizes of the given fields
   function {:opaque}  SumValueSize(fields : CanonCryptoList)
-    : nat
+    : uint64
   {
     if |fields| == 0 then
       0
     else if fields[0].action == ENCRYPT_AND_SIGN then
-      |fields[0].data.value| + SumValueSize(fields[1..])
+      SequenceIsSafeBecauseItIsInMemory(fields[0].data.value);
+      Add(|fields[0].data.value| as uint64, SumValueSize(fields[1..]))
     else
       SumValueSize(fields[1..])
   } by method {
     reveal SumValueSize();
-    var sum : nat := 0;
+    var sum : uint64 := 0;
     for i := |fields| downto 0
       invariant sum == SumValueSize(fields[i..])
     {
       if fields[i].action == ENCRYPT_AND_SIGN {
-        sum := |fields[i].data.value| + sum;
+        SequenceIsSafeBecauseItIsInMemory(fields[i].data.value);
+        sum := Add(|fields[i].data.value| as uint64, sum);
       }
     }
     return sum;
@@ -269,19 +272,20 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     output := GetV2EncryptionContext2(contextAttrs);
   }
 
-  function {:opaque} Find(haystack : CryptoList, needle : Path, start : nat := 0) : (res : Result<nat, Error>)
-    requires start <= |haystack|
+  function {:opaque} Find(haystack : CryptoList, needle : Path, start : uint64 := 0) : (res : Result<uint64, Error>)
+    requires start as nat <= |haystack|
     requires forall i | 0 <= i < start :: haystack[i].key != needle
     ensures (exists x <- haystack :: x.key == needle) <==> res.Success?
     ensures (forall x <- haystack :: x.key != needle) <==> res.Failure?
     ensures (forall x <- haystack :: x.key != needle) <==> res == Failure(E("Not Found"))
     ensures res.Success? ==>
-              && 0 <= res.value < |haystack|
+              && 0 <= res.value as nat < |haystack|
               && haystack[res.value].key == needle
               && (forall i | 0 <= i < res.value :: haystack[i].key != needle)
-    decreases |haystack| - start
+    decreases |haystack| - start as nat
   {
-    if |haystack| == start then
+    SequenceIsSafeBecauseItIsInMemory(haystack);
+    if |haystack| as uint64 == start then
       Failure(E("Not Found"))
     else if haystack[start].key == needle then
       Success(start)
@@ -289,7 +293,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
       Find(haystack, needle, start + 1)
   }
   by method {
-    for i := 0 to |haystack|
+    SequenceIsSafeBecauseItIsInMemory(haystack);
+    for i : uint64 := 0 to |haystack| as uint64
       invariant forall x <- haystack[..i] :: x.key != needle
     {
       if haystack[i].key == needle {
@@ -299,18 +304,19 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     return Failure(E("Not Found"));
   }
 
-  function {:opaque} FindAuth(haystack : AuthList, needle : Path, start : nat := 0) : (res : Option<nat>)
-    requires start <= |haystack|
+  function {:opaque} FindAuth(haystack : AuthList, needle : Path, start : uint64 := 0) : (res : Option<uint64>)
+    requires start as nat <= |haystack|
     requires forall i | 0 <= i < start :: haystack[i].key != needle
     ensures (exists x <- haystack :: x.key == needle) <==> res.Some?
     ensures (forall x <- haystack :: x.key != needle) <==> res == None
     ensures res.Some? ==>
-              && 0 <= res.value < |haystack|
+              && 0 <= res.value as nat < |haystack|
               && haystack[res.value].key == needle
               && (forall i | 0 <= i < res.value :: haystack[i].key != needle)
-    decreases |haystack| - start
+    decreases |haystack| - start as nat
   {
-    if |haystack| == start then
+    SequenceIsSafeBecauseItIsInMemory(haystack);
+    if |haystack| as uint64 == start then
       None
     else if haystack[start].key == needle then
       Some(start)
@@ -318,7 +324,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
       FindAuth(haystack, needle, start + 1)
   }
   by method {
-    for i := 0 to |haystack|
+    SequenceIsSafeBecauseItIsInMemory(haystack);
+    for i : uint64 := 0 to |haystack| as uint64
       invariant forall x <- haystack[..i] :: x.key != needle
     {
       if haystack[i].key == needle {
@@ -328,22 +335,23 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     return None;
   }
 
-  function {:opaque} CountEncrypted(list : CanonCryptoList) : nat
+  function {:opaque} CountEncrypted(list : CanonCryptoList) : uint64
   {
     if |list| == 0 then
       0
     else if list[0].action == ENCRYPT_AND_SIGN then
-      1 + CountEncrypted(list[1..])
+      Add(1, CountEncrypted(list[1..]))
     else
       CountEncrypted(list[1..])
   } by method {
     reveal CountEncrypted();
-    var result : nat := 0;
-    for i := |list| downto 0
+    SequenceIsSafeBecauseItIsInMemory(list);
+    var result : uint64 := 0;
+    for i : uint64 := |list| as uint64 downto 0
       invariant result == CountEncrypted(list[i..])
     {
       if list[i].action == ENCRYPT_AND_SIGN {
-        result := result + 1;
+        result := Add(result, 1);
       }
     }
     return result;
@@ -444,18 +452,18 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     keys : seq<string>,
     plaintextStructure: StructuredDataMap,
     cryptoSchema: CryptoSchemaMap,
-    pos : nat := 0,
+    pos : uint64 := 0,
     acc : CryptoList := []
   )
     : (ret : Result<CryptoList, Error>)
-    requires 0 <= pos <= |keys|
-    requires |acc| == pos
+    requires 0 <= pos as nat <= |keys|
+    requires |acc| == pos as nat
     requires forall k <- keys :: k in plaintextStructure
     requires forall k <- keys :: k in cryptoSchema
     requires forall k <- acc :: |k.key| == 1
     requires forall i | 0 <= i < |acc| :: acc[i].key == Paths.StringToUniPath(keys[i])
     requires Seq.HasNoDuplicates(keys)
-    decreases |keys| - pos
+    decreases |keys| - pos as nat
 
     ensures ret.Success? ==>
               && (forall k <- ret.value :: |k.key| == 1)
@@ -463,7 +471,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
   {
     reveal Seq.HasNoDuplicates();
     Paths.StringToUniPathUnique();
-    if |keys| == pos then
+    SequenceIsSafeBecauseItIsInMemory(keys);
+    if |keys| as uint64 == pos then
       Success(acc)
     else
       var key := keys[pos];
@@ -488,26 +497,27 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     keys : seq<string>,
     plaintextStructure: StructuredDataMap,
     authSchema: AuthenticateSchemaMap,
-    pos : nat := 0,
+    pos : uint64 := 0,
     acc : AuthList := []
   )
     : (ret : Result<AuthList, Error>)
-    requires 0 <= pos <= |keys|
-    requires |acc| == pos
+    requires 0 <= pos as nat <= |keys|
+    requires |acc| == pos as nat
     requires forall k <- keys :: k in plaintextStructure
     requires forall k <- keys :: k in authSchema
     requires forall k <- acc :: |k.key| == 1
     requires forall i | 0 <= i < |acc| :: acc[i].key == Paths.StringToUniPath(keys[i])
     requires AuthListHasNoDuplicates(acc)
     requires Seq.HasNoDuplicates(keys)
-    decreases |keys| - pos
+    decreases |keys| - pos as nat
 
     ensures ret.Success? ==>
               && (forall k <- ret.value :: |k.key| == 1)
               && AuthListHasNoDuplicates(ret.value)
   {
     reveal Seq.HasNoDuplicates();
-    if |keys| == pos then
+    SequenceIsSafeBecauseItIsInMemory(keys);
+    if |keys| as uint64 == pos then
       Success(acc)
     else
       var key := keys[pos];
@@ -528,20 +538,21 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     BuildAuthMap2(keys, plaintextStructure, authSchema)
   }
 
-  function method {:tailrecursion} UnBuildCryptoMap(list : CryptoList, pos : nat := 0, dataSoFar : StructuredDataMap := map[], actionsSoFar : CryptoSchemaMap := map[]) :
+  function method {:tailrecursion} UnBuildCryptoMap(list : CryptoList, pos : uint64 := 0, dataSoFar : StructuredDataMap := map[], actionsSoFar : CryptoSchemaMap := map[]) :
     (res : Result<(StructuredDataMap, CryptoSchemaMap), Error>)
-    requires 0 <= pos <= |list|
-    requires |dataSoFar| == pos
-    requires |actionsSoFar| <= pos
+    requires 0 <= pos as nat <= |list|
+    requires |dataSoFar| == pos as nat
+    requires |actionsSoFar| <= pos as nat
     requires forall k <- actionsSoFar :: k in dataSoFar
     requires (forall v :: v in actionsSoFar.Values ==> IsAuthAttr(v))
     requires forall k <- list :: |k.key| == 1
-    decreases |list| - pos
+    decreases |list| - pos as nat
     ensures res.Success? ==>
               && (forall k <- res.value.1 :: k in res.value.0)
               && (forall v :: v in res.value.1.Values ==> IsAuthAttr(v))
   {
-    if |list| == pos then
+    SequenceIsSafeBecauseItIsInMemory(list);
+    if |list| as uint64 == pos then
       Success((dataSoFar, actionsSoFar))
     else
       var key :- Paths.UniPathToString(list[pos].key);
@@ -811,8 +822,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
       cmm,
       Some(encryptionContext),
       input.algorithmSuiteId,
-      CountEncrypted(canonData),
-      SumValueSize(canonData));
+      CountEncrypted(canonData) as nat,
+      SumValueSize(canonData) as nat);
 
     var key : Key := mat.plaintextDataKey.value;
     var alg := mat.algorithmSuite;
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
index e8b0eb240..fdd117d26 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
@@ -11,6 +11,7 @@ module {:options "/functionSyntax:4" } Canonize {
   import opened Wrappers
   import opened StandardLibrary
   import opened StandardLibrary.UInt
+  import opened MemoryMath
   import Header = StructuredEncryptionHeader
   import Paths = StructuredEncryptionPaths
   import SortCanon
@@ -139,27 +140,28 @@ module {:options "/functionSyntax:4" } Canonize {
   opaque function {:tailrecursion} ResolveLegend(
     fields : CanonAuthList,
     legend : Header.Legend,
-    pos : nat := 0,
-    legendPos : nat := 0,
+    pos : uint64 := 0,
+    legendPos : uint64 := 0,
     acc : CanonCryptoList := []
   )
     : (ret : Result<CanonCryptoList, Error>)
-    requires 0 <= pos <= |fields|
-    requires 0 <= legendPos <= |legend|
-    requires pos == |acc|
+    requires 0 <= pos as nat <= |fields|
+    requires 0 <= legendPos as nat <= |legend|
+    requires pos as nat == |acc|
     requires forall i | 0 <= i < pos :: Same(fields[i], acc[i])
     ensures ret.Success? ==>
               && |fields| == |ret.value|
               && forall i | 0 <= i < |fields| :: Same(fields[i], ret.value[i])
-    decreases |fields| - pos
+    decreases |fields| - pos as nat
   {
-    if |fields| == pos then
-      :- Need(|legend| == legendPos, E("Schema changed : something that was signed is now unsigned."));
+    SequenceIsSafeBecauseItIsInMemory(fields);
+    if |fields| as uint64 == pos then
+      :- Need(|legend| as uint64 == legendPos, E("Schema changed : something that was signed is now unsigned."));
       Success(acc)
     else if fields[pos].action == DO_NOT_SIGN then
       ResolveLegend(fields, legend, pos+1, legendPos, acc + [MakeCryptoItem(fields[pos], DO_NOTHING)])
     else
-      :- Need(legendPos < |legend|, E("Schema changed : something that was unsigned is now signed."));
+      :- Need(legendPos < |legend| as uint64, E("Schema changed : something that was unsigned is now signed."));
       ResolveLegend(fields, legend, pos+1, legendPos+1, acc + [MakeCryptoItem(fields[pos], LegendToAction(legend[legendPos]))])
   }
 
@@ -625,15 +627,16 @@ module {:options "/functionSyntax:4" } Canonize {
     && x.action == y.action
   }
 
-  function {:tailrecursion} UnCanon(input : CanonCryptoList, pos : nat := 0, acc : CryptoList := []) : (ret : CryptoList)
-    requires 0 <= pos <= |input|
-    requires pos == |acc|
+  function {:tailrecursion} UnCanon(input : CanonCryptoList, pos : uint64 := 0, acc : CryptoList := []) : (ret : CryptoList)
+    requires 0 <= pos as nat <= |input|
+    requires pos as nat == |acc|
     requires forall i | 0 <= i < |acc| :: SameUnCanon(input[i], acc[i])
     ensures |ret| == |input|
     ensures forall i | 0 <= i < |input| :: SameUnCanon(input[i], ret[i])
-    decreases |input| - pos
+    decreases |input| - pos as nat
   {
-    if |input| == pos then
+    SequenceIsSafeBecauseItIsInMemory(input);
+    if |input| as uint64 == pos then
       acc
     else
       var newItem := CryptoItem(key := input[pos].origKey, data := input[pos].data, action := input[pos].action);
@@ -800,9 +803,9 @@ module {:options "/functionSyntax:4" } Canonize {
     && CryptoListHasNoDuplicates(finalData)
   }
 
-  opaque function {:tailrecursion} RemoveHeaderPaths(xs : CryptoList, pos : nat := 0, acc : CryptoList := []) : (ret : CryptoList)
+  opaque function {:tailrecursion} RemoveHeaderPaths(xs : CryptoList, pos : uint64 := 0, acc : CryptoList := []) : (ret : CryptoList)
     requires CryptoListHasNoDuplicates(xs)
-    requires 0 <= pos <= |xs|
+    requires 0 <= pos as nat <= |xs|
     requires !exists x :: x in acc && x.key in [HeaderPath, FooterPath]
     requires !exists x :: x in acc && x.key == HeaderPath
     requires !exists x :: x in acc && x.key == FooterPath
@@ -819,9 +822,10 @@ module {:options "/functionSyntax:4" } Canonize {
     ensures forall x <- xs :: (x.key in [HeaderPath, FooterPath] || x in ret)
     ensures CryptoListHasNoDuplicates(ret)
 
-    decreases |xs| - pos
+    decreases |xs| - pos as nat
   {
-    if |xs| == pos then
+    SequenceIsSafeBecauseItIsInMemory(xs);
+    if |xs| as uint64 == pos then
       acc
     else if xs[pos].key in [HeaderPath, FooterPath] then
       RemoveHeaderPaths(xs, pos+1, acc)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy
index e994c382e..8fd348ecb 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy
@@ -23,6 +23,7 @@ module StructuredEncryptionFooter {
   import opened StandardLibrary.UInt
   import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import opened StructuredEncryptionUtil
+  import opened MemoryMath
   import Primitives = AtomicPrimitives
   import Materials
   import Header = StructuredEncryptionHeader
@@ -157,10 +158,10 @@ module StructuredEncryptionFooter {
     : Result<Bytes, Error>
   {
     if isEncrypted then
-      :- Need(2 <= |value.value| < UINT64_LIMIT, E("Bad length."));
+      :- Need(2 <= |value.value| && HasUint64Len(value.value), E("Bad length."));
       Success(UInt64ToSeq((|value.value| - 2) as uint64) + ENCRYPTED)
     else
-      :- Need(|value.value| < UINT64_LIMIT, E("Bad length."));
+      :- Need(HasUint64Len(value.value), E("Bad length."));
       Success(UInt64ToSeq((|value.value|) as uint64) + PLAINTEXT + value.typeId)
   }
 
@@ -177,14 +178,15 @@ module StructuredEncryptionFooter {
               //# | "ENCRYPTED" | 9 | Literal Ascii text |
               //# | TypeID | 2 | the type ID of the unencrypted Terminal |
               //# | value | Variable | the encrypted Terminal value |
-              && 2 <= |value.value| < UINT64_LIMIT
+              && 2 <= |value.value|
+              && HasUint64Len(value.value)
               && ret.value ==
                  fieldName
                  + UInt64ToSeq((|value.value| - 2) as uint64)
                  + ENCRYPTED
                  + value.value // this is 2 bytes of unencrypted type, followed by encrypted value
   {
-    :- Need(2 <= |value.value| < UINT64_LIMIT, E("Bad length."));
+    :- Need(2 <= |value.value| && HasUint64Len(value.value), E("Bad length."));
     Success(
       fieldName
       + UInt64ToSeq((|value.value| - 2) as uint64)
@@ -206,7 +208,7 @@ module StructuredEncryptionFooter {
               //# | "PLAINTEXT" | 9 | Literal Ascii text |
               //# | TypeID | 2 | the type ID of the Terminal |
               //# | value | Variable | the Terminal value |
-              && |value.value| < UINT64_LIMIT
+              && HasUint64Len(value.value)
               && ret.value ==
                  fieldName
                  + UInt64ToSeq((|value.value|) as uint64)
@@ -214,7 +216,7 @@ module StructuredEncryptionFooter {
                  + value.typeId
                  + value.value
   {
-    :- Need(|value.value| < UINT64_LIMIT, E("Bad length."));
+    :- Need(HasUint64Len(value.value), E("Bad length."));
     Success(
       fieldName
       + UInt64ToSeq((|value.value|) as uint64)
@@ -246,7 +248,8 @@ module StructuredEncryptionFooter {
       var newPart :- GetCanonicalItem(data[0]);
       Success(newPart + tail)
   } by method {
-    var i: nat := |data|;
+    SequenceIsSafeBecauseItIsInMemory(data);
+    var i: uint64 := |data| as uint64;
     var vectors : Bytes := [];
 
     while i != 0
@@ -293,7 +296,7 @@ module StructuredEncryptionFooter {
               && CanonContent(data).Success?
               && var canon := CanonContent(data).value;
               && var AAD := Header.SerializeContext(enc);
-              && |AAD| < UINT64_LIMIT
+              && HasUint64Len(AAD)
               && var len := UInt64ToSeq(|AAD| as uint64);
               && ret.value ==
                  header
@@ -303,7 +306,7 @@ module StructuredEncryptionFooter {
   {
     var canon :- CanonContent(data);
     var AAD := Header.SerializeContext(enc);
-    :- Need(|AAD| < UINT64_LIMIT, E("AAD too long."));
+    :- Need(HasUint64Len(AAD), E("AAD too long."));
     var len := UInt64ToSeq(|AAD| as uint64);
     Success(header + len + AAD + canon)
   }
@@ -412,7 +415,8 @@ module StructuredEncryptionFooter {
       tags[0] + SerializeTags(tags[1..])
   } by method {
     var result : Bytes := [];
-    for i := |tags| downto 0
+    SequenceIsSafeBecauseItIsInMemory(tags);
+    for i : uint64 := |tags| as uint64 downto 0
       invariant result == SerializeTags(tags[i..])
     {
       result := tags[i] + result;
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
index cd6b36e99..e48bc3d89 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
@@ -13,6 +13,7 @@ module StructuredEncryptionHeader {
   import opened StandardLibrary.UInt
   import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import opened StructuredEncryptionUtil
+  import opened MemoryMath
 
   import CMP = AwsCryptographyMaterialProvidersTypes
   import Prim = AwsCryptographyPrimitivesTypes
@@ -383,11 +384,12 @@ module StructuredEncryptionHeader {
               //= type=implication
               //# The length of this serialized value (in bytes) MUST equal the number of authenticated fields indicated
               //# by the caller's [Authenticate Schema](./structures.md#authenticate-schema).
-              && |ret.value| == CountAuthAttrs(schema)
+              && |ret.value| == CountAuthAttrs(schema) as nat
   {
     var legend :- MakeLegend2(schema);
     var authCount := CountAuthAttrs(schema);
-    :- Need(authCount == |legend|, E("Internal Error : bad legend calculation."));
+    SequenceIsSafeBecauseItIsInMemory(legend);
+    :- Need(authCount == |legend| as uint64, E("Internal Error : bad legend calculation."));
     Success(legend)
   }
 
@@ -399,14 +401,15 @@ module StructuredEncryptionHeader {
   // Create a Legend for the given attrs of the Schema
   function method {:tailrecursion} MakeLegend2(
     data : CanonCryptoList,
-    pos : nat := 0,
+    pos : uint64 := 0,
     serialized : Legend := EmptyLegend
   )
     : (ret : Result<Legend, Error>)
-    requires 0 <= pos <= |data|
-    decreases |data| - pos
+    requires 0 <= pos as nat <= |data|
+    decreases |data| - pos as nat
   {
-    if |data| == pos then
+    SequenceIsSafeBecauseItIsInMemory(data);
+    if |data| as uint64 == pos then
       Success(serialized)
     else if IsAuthAttr(data[pos].action) then
       :- Need((|serialized| + 1) < UINT16_LIMIT, E("Legend Too Long."));
@@ -447,15 +450,16 @@ module StructuredEncryptionHeader {
   }
 
   // How many elements of Schema are included in the signature?
-  function method CountAuthAttrs(data : CanonCryptoList, pos : nat := 0, acc : nat := 0)
-    : nat
-    requires 0 <= pos <= |data|
-    decreases |data| - pos
+  function method CountAuthAttrs(data : CanonCryptoList, pos : uint64 := 0, acc : uint64 := 0)
+    : uint64
+    requires 0 <= pos as nat <= |data|
+    decreases |data| - pos as nat
   {
-    if |data| == pos then
+    SequenceIsSafeBecauseItIsInMemory(data);
+    if |data| as uint64 == pos then
       acc
     else if IsAuthAttr(data[pos].action) then
-      CountAuthAttrs(data, pos+1, acc+1)
+      CountAuthAttrs(data, pos+1, Add(acc, 1))
     else
       CountAuthAttrs(data, pos+1, acc)
   }
@@ -480,16 +484,18 @@ module StructuredEncryptionHeader {
 
   // Bytes to Legend
   function method GetLegend(data : Bytes)
-    : (ret : Result<(Legend, nat), Error>)
+    : (ret : Result<(Legend, uint64), Error>)
     ensures ret.Success? ==>
-              && ret.value.1 <= |data|
-              && ret.value.1 == |ret.value.0| + 2
+              && ret.value.1 as nat <= |data|
+              && ret.value.1 as nat == |ret.value.0| + 2
               && ret.value.0 == data[2..ret.value.1]
   {
-    :- Need(2 <= |data|, E("Unexpected end of header data."));
-    var len := SeqPosToUInt16(data, 0);
-    var size := len as nat + 2;
-    :- Need(size <= |data|, E("Unexpected end of header data."));
+    SequenceIsSafeBecauseItIsInMemory(data);
+    var data_size : uint64 := |data| as uint64;
+    :- Need(2 <= data_size, E("Unexpected end of header data."));
+    var len := SeqPosToUInt16(data, 0) as uint64;
+    var size := Add(len, 2);
+    :- Need(size <= data_size, E("Unexpected end of header data."));
     var legend := data[2..size];
     :- Need(forall x <- legend :: ValidLegendByte(x), E("Invalid byte in stored legend"));
     Success((legend, size))
@@ -497,58 +503,71 @@ module StructuredEncryptionHeader {
 
   // Bytes to Encryption Context
   function method GetContext(data : Bytes)
-    : (ret : Result<(CMPEncryptionContext, nat), Error>)
+    : (ret : Result<(CMPEncryptionContext, uint64), Error>)
     ensures ret.Success? ==>
-              && ret.value.1 <= |data|
+              && ret.value.1 as nat <= |data|
     ensures (
+              && HasUint64Len(data)
               && 2 <= |data|
-              && GetContext2(SeqPosToUInt16(data, 0) as nat, data, (map[], 2)).Success?
+              && GetContext2(SeqPosToUInt16(data, 0) as uint64, data, (map[], 2)).Success?
             ) ==> ret.Success?
   {
-    :- Need(2 <= |data|, E("Unexpected end of header data."));
-    var count := SeqPosToUInt16(data, 0) as nat;
+    SequenceIsSafeBecauseItIsInMemory(data);
+    var data_size : uint64 := |data| as uint64;
+    :- Need(2 <= data_size, E("Unexpected end of header data."));
+    var count := SeqPosToUInt16(data, 0) as uint64;
     var context :- GetContext2(count, data, (map[], 2));
     Success(context)
   }
 
   // Bytes to one Key Value pair
-  function method GetOneKVPair(data : Bytes, pos : nat)
-    : (ret : Result<(CMPUtf8Bytes, CMPUtf8Bytes, nat), Error>)
+  function method GetOneKVPair(data : Bytes, pos : uint64)
+    : (ret : Result<(CMPUtf8Bytes, CMPUtf8Bytes, uint64), Error>)
     ensures ret.Success? ==>
-              && ret.value.2 + pos <= |data|
+              && HasUint64Len(data)
+              && Add(ret.value.2, pos) <= |data| as uint64
     ensures (
-              && 2 + pos <= |data|
-              && var keyLen := SeqPosToUInt16(data, pos) as nat;
-              && keyLen + 4 + pos <= |data|
-              && UTF8.ValidUTF8Seq(data[2+pos..keyLen+2+pos])
-              && var valueLen := SeqPosToUInt16(data, keyLen+2+pos) as nat;
-              && keyLen + valueLen + 4 + pos <= |data|
-              && UTF8.ValidUTF8Seq(data[keyLen+4+pos..keyLen + valueLen + 4 + pos])
+              && HasUint64Len(data)
+              && var data_size : uint64 := |data| as uint64;
+              && Add(2, pos) <= data_size
+              && var keyLen := SeqPosToUInt16(data, pos) as uint64;
+              && Add3(keyLen, 4, pos) <= data_size
+              && var key := data[2+pos..Add3(keyLen, 2, pos)];
+              && UTF8.ValidUTF8Seq(key)
+              && var valueLen := SeqPosToUInt16(data, keyLen+2+pos) as uint64;
+              && var kvLen := 2 + keyLen + 2 + valueLen;
+              && Add(kvLen, pos) <= data_size
+              && var value := data[keyLen+4+pos..kvLen+pos];
+              && UTF8.ValidUTF8Seq(value)
             ) <==> ret.Success? && SerializeOneKVPair(ret.value.0, ret.value.1) == data[pos..pos+ret.value.2]
   {
-    :- Need(2 + pos <= |data|, E("Unexpected end of header data."));
-    var keyLen := SeqPosToUInt16(data, pos) as nat;
-    :- Need(keyLen + 4 +pos <= |data|, E("Unexpected end of header data."));
-    var key := data[2+pos..keyLen+2+pos];
+    SequenceIsSafeBecauseItIsInMemory(data);
+    var data_size : uint64 := |data| as uint64;
+    :- Need(Add(2, pos) <= data_size, E("Unexpected end of header data."));
+    var keyLen := SeqPosToUInt16(data, pos) as uint64;
+    :- Need(Add3(keyLen, 4, pos) <= data_size, E("Unexpected end of header data."));
+    var key := data[2+pos..Add3(keyLen, 2, pos)];
     :- Need(UTF8.ValidUTF8Seq(key), E("Invalid UTF8 found in header."));
-    var valueLen := SeqPosToUInt16(data, keyLen+2+pos) as nat;
+    var valueLen := SeqPosToUInt16(data, Add3(keyLen, 2, pos)) as uint64;
     var kvLen := 2 + keyLen + 2 + valueLen;
-    :- Need(kvLen + pos <= |data|, E("Unexpected end of header data."));
+    :- Need(Add(kvLen, pos) <= data_size as uint64, E("Unexpected end of header data."));
     var value := data[keyLen+4+pos..kvLen+pos];
     :- Need(UTF8.ValidUTF8Seq(value), E("Invalid UTF8 found in header."));
     Success((key, value, kvLen))
   }
 
-  predicate method {:tailrecursion} BytesLess(a: Bytes, b : Bytes, pos : nat := 0)
-    requires 0 <= pos <= |a|
-    requires 0 <= pos <= |b|
-    decreases |a| - pos
+  predicate method {:tailrecursion} BytesLess(a: Bytes, b : Bytes, pos : uint64 := 0)
+    requires 0 <= pos as nat <= |a|
+    requires 0 <= pos as nat <= |b|
+    decreases |a| - pos as nat
   {
+    SequenceIsSafeBecauseItIsInMemory(a);
+    SequenceIsSafeBecauseItIsInMemory(b);
     if a == b then
       false
-    else if |a| == pos then
+    else if |a| as uint64 == pos then
       true
-    else if |b| == pos then
+    else if |b| as uint64 == pos then
       false
     else if a[pos] != b[pos] then
       a[pos] < b[pos]
@@ -558,21 +577,21 @@ module StructuredEncryptionHeader {
 
   // For "count" items, Deserialize key value pairs into an Encryption Context
   function method {:tailrecursion} GetContext2(
-    count : nat,
+    count : uint64,
     data : Bytes,
-    deserialized : (CMPEncryptionContext, nat),
+    deserialized : (CMPEncryptionContext, uint64),
     prevKey : CMPUtf8Bytes := [])
-    : (ret : Result<(CMPEncryptionContext, nat), Error>)
-    requires deserialized.1 <= |data|
+    : (ret : Result<(CMPEncryptionContext, uint64), Error>)
+    requires deserialized.1 as nat <= |data|
     ensures ret.Success? ==>
-              && ret.value.1 <= |data|
-              && (count > 0 ==> GetOneKVPair(data, deserialized.1).Success?)
+              && ret.value.1 as nat <= |data|
+              && (count > 0 ==> GetOneKVPair(data, deserialized.1 as uint64).Success?)
   {
     if count == 0 then
       Success(deserialized)
     else
       :- Need(|deserialized.0| + 1  < UINT16_LIMIT, E("Too much context"));
-      var kv :- GetOneKVPair(data, deserialized.1);
+      var kv :- GetOneKVPair(data, deserialized.1 as uint64);
       //= specification/structured-encryption/header.md#key-value-pair-entries
       //# This sequence MUST NOT contain duplicate entries.
       // if the previous key is always less than the current key, there can be no duplicates
@@ -581,7 +600,7 @@ module StructuredEncryptionHeader {
       //# These entries MUST have entries sorted, by key,
       //# in ascending order according to the UTF-8 encoded binary value.
       :- Need(BytesLess(prevKey, kv.0), E("Context keys out of order."));
-      GetContext2(count-1, data, (deserialized.0[kv.0 := kv.1], deserialized.1 + kv.2), kv.0)
+      GetContext2(count-1, data, (deserialized.0[kv.0 := kv.1], Add(deserialized.1, kv.2)), kv.0)
   }
 
   // Encryption Context to Bytes
@@ -659,33 +678,38 @@ module StructuredEncryptionHeader {
   }
 
   // Bytes to Data Key
-  function method {:vcs_split_on_every_assert} GetOneDataKey(data : Bytes, pos : nat)
-    : (ret : Result<(CMPEncryptedDataKey, nat), Error>)
+  function method {:vcs_split_on_every_assert} GetOneDataKey(data : Bytes, pos : uint64)
+    : (ret : Result<(CMPEncryptedDataKey, uint64), Error>)
     ensures ret.Success? ==>
-              && ret.value.1 + pos <= |data|
-              && |SerializeOneDataKey(ret.value.0)| == ret.value.1
-              && SerializeOneDataKey(ret.value.0) == data[pos..pos+ret.value.1]
-  {
-    :- Need(2 + pos < |data|, E("Unexpected end of header data."));
-    var provIdSize := SeqPosToUInt16(data, pos) as nat;
-    :- Need(provIdSize + 2 + pos < |data|, E("Unexpected end of header data."));
+              && HasUint64Len(data)
+              && var data_size : uint64 := |data| as uint64;
+              && Add(ret.value.1, pos) <= |data| as uint64
+              && |SerializeOneDataKey(ret.value.0)| == ret.value.1 as nat
+              && SerializeOneDataKey(ret.value.0) == data[pos..Add(pos, ret.value.1 as uint64)]
+  {
+    SequenceIsSafeBecauseItIsInMemory(data);
+    var data_size : uint64 := |data| as uint64;
+
+    :- Need(Add(2, pos) < data_size, E("Unexpected end of header data."));
+    var provIdSize := SeqPosToUInt16(data, pos) as uint64;
+    :- Need(Add3(provIdSize, 2, pos) < data_size, E("Unexpected end of header data."));
     var provId := data[pos+2..pos+2+provIdSize];
     :- Need(UTF8.ValidUTF8Seq(provId), E("Invalid UTF8 found in header."));
     var part1Size := 2 + provIdSize;
 
-    :- Need(part1Size+2 + pos <= |data|, E("Unexpected end of header data."));
-    var provInfoSize := SeqPosToUInt16(data, pos+part1Size) as nat;
-    :- Need(part1Size + provInfoSize + 2 + pos < |data|, E("Unexpected end of header data."));
-    var provInfo := data[pos+part1Size+2..pos+part1Size+2+provInfoSize];
+    :- Need(Add3(part1Size, 2, pos) <= data_size, E("Unexpected end of header data."));
+    var provInfoSize := SeqPosToUInt16(data, pos+part1Size) as uint64;
     var part2Size := part1Size + 2 + provInfoSize;
+    :- Need(Add(part2Size, pos) < data_size, E("Unexpected end of header data."));
+    var provInfo := data[pos+part1Size+2..pos+part1Size+2+provInfoSize];
 
-    :- Need(part2Size+2+pos <= |data|, E("Unexpected end of header data."));
-    var cipherSize := SeqPosToUInt16(data, pos+part2Size) as nat;
-    :- Need(part2Size + cipherSize + 2 + pos <= |data|, E("Unexpected end of header data."));
-    var cipher := data[pos+part2Size+2..pos+part2Size+2+cipherSize];
+    :- Need(Add3(part2Size, 2, pos) <= data_size, E("Unexpected end of header data."));
+    var cipherSize := SeqPosToUInt16(data, pos+part2Size) as uint64;
     var part3Size := part2Size + 2 + cipherSize;
+    :- Need(Add(part3Size, pos) <= data_size, E("Unexpected end of header data."));
+    var cipher := data[pos+part2Size+2..pos+part2Size+2+cipherSize];
 
-    var edk := CMP.EncryptedDataKey(keyProviderId := provId, keyProviderInfo := provInfo, ciphertext := cipher);
+    var edk : CMPEncryptedDataKey := CMP.EncryptedDataKey(keyProviderId := provId, keyProviderInfo := provInfo, ciphertext := cipher);
     Success((edk, part3Size))
   }
 
@@ -693,15 +717,16 @@ module StructuredEncryptionHeader {
   function method {:tailrecursion} SerializeContext2(
     keys : seq<CMPUtf8Bytes>,
     x : CMPEncryptionContext,
-    pos : nat := 0,
+    pos : uint64 := 0,
     acc : Bytes := []
   )
     : (ret : Bytes)
     requires forall k <- keys :: k in x
-    requires 0 <= pos <= |keys|
-    decreases |keys| - pos
+    requires 0 <= pos as nat <= |keys|
+    decreases |keys| - pos as nat
   {
-    if |keys| == pos then
+    SequenceIsSafeBecauseItIsInMemory(keys);
+    if |keys| as uint64 == pos then
       acc
     else
       SerializeContext2(keys, x, pos+1, acc + SerializeOneKVPair(keys[pos], x[keys[pos]]))
@@ -729,14 +754,15 @@ module StructuredEncryptionHeader {
   // Data Keys to Bytes
   function method {:tailrecursion} SerializeDataKeys2(
     x : CMPEncryptedDataKeyListEmptyOK,
-    pos : nat := 0,
+    pos : uint64 := 0,
     acc : Bytes := []
   )
     : (ret : Bytes)
-    requires 0 <= pos <= |x|
-    decreases |x| - pos
+    requires 0 <= pos as nat <= |x|
+    decreases |x| - pos as nat
   {
-    if |x| == pos then
+    SequenceIsSafeBecauseItIsInMemory(x);
+    if |x| as uint64 == pos then
       acc
     else
       SerializeDataKeys2(x, pos+1, acc + SerializeOneDataKey(x[pos]))
@@ -744,16 +770,16 @@ module StructuredEncryptionHeader {
 
   // Bytes to Data Key List
   function method GetDataKeys(data : Bytes)
-    : (ret : Result<(CMPEncryptedDataKeyList, nat), Error>)
+    : (ret : Result<(CMPEncryptedDataKeyList, uint64), Error>)
     ensures ret.Success? ==>
-              && ret.value.1 <= |data|
+              && ret.value.1 as nat <= |data|
               && 1 <= |data|
               && 1 <= ret.value.1
               && |ret.value.0| == data[0] as nat
-              && GetDataKeys2(|ret.value.0|, |ret.value.0|, data, ([], 1)).Success?
+              && GetDataKeys2(|ret.value.0| as uint64, |ret.value.0| as uint64, data, ([], 1)).Success?
   {
     :- Need(1 <= |data|, E("Unexpected end of header data."));
-    var count := data[0] as nat;
+    var count := data[0] as uint64;
     var keys :- GetDataKeys2(count, count, data, ([], 1));
     if |keys.0| == 0 then
       Failure(E("At least one Data Key required"))
@@ -763,18 +789,18 @@ module StructuredEncryptionHeader {
 
   // Convert "count" items from Bytes to Data Keys
   function method {:tailrecursion} GetDataKeys2(
-    count : nat,
-    origCount : nat,
+    count : uint64,
+    origCount : uint64,
     data : Bytes,
-    deserialized : (CMPEncryptedDataKeyListEmptyOK, nat))
-    : (ret : Result<(CMPEncryptedDataKeyListEmptyOK, nat), Error>)
-    requires deserialized.1 <= |data|
-    requires origCount == count + |deserialized.0|
+    deserialized : (CMPEncryptedDataKeyListEmptyOK, uint64))
+    : (ret : Result<(CMPEncryptedDataKeyListEmptyOK, uint64), Error>)
+    requires deserialized.1 as nat <= |data|
+    requires origCount as nat == count as nat + |deserialized.0|
     ensures ret.Success? ==>
-              && ret.value.1 <= |data|
+              && ret.value.1 as nat <= |data|
               && ret.value.1 >= deserialized.1
-              && (count > 0 ==> GetOneDataKey(data, deserialized.1).Success?)
-              && |ret.value.0| == origCount
+              && (count > 0 ==> GetOneDataKey(data, deserialized.1 as uint64).Success?)
+              && |ret.value.0| == origCount as nat
   {
     if count == 0 then
       Success(deserialized)
@@ -782,7 +808,7 @@ module StructuredEncryptionHeader {
     if |deserialized.0| >= 255 then
       Failure(E("Too Many Data Keys"))
     else
-      var edk :- GetOneDataKey(data, deserialized.1);
+      var edk :- GetOneDataKey(data, deserialized.1 as uint64);
       assert SerializeOneDataKey(edk.0) == data[deserialized.1..deserialized.1+edk.1];
       GetDataKeys2(count-1, origCount, data, (deserialized.0 + [edk.0], deserialized.1+edk.1))
   }
@@ -804,8 +830,8 @@ module StructuredEncryptionHeader {
     ensures GetLegend(SerializeLegend(x)).Success?
     ensures var ret := GetLegend(SerializeLegend(x)).value;
             && ret.0 == x
-            && ret.1 == |x| + 2
-            && ret.1 == |SerializeLegend(x)|
+            && ret.1 as nat == |x| + 2
+            && ret.1 as nat == |SerializeLegend(x)|
   {}
 
   // GetLegend ==> SerializeLegend
@@ -833,7 +859,7 @@ module StructuredEncryptionHeader {
   }
 
   // GetOneKVPair ==> SerializeOneKVPair
-  lemma GetOneKVPairRoundTrip(data : Bytes, pos : nat)
+  lemma GetOneKVPairRoundTrip(data : Bytes, pos : uint64)
     requires GetOneKVPair(data, pos).Success?
     ensures
       && var cont := GetOneKVPair(data, pos).value;
@@ -846,7 +872,7 @@ module StructuredEncryptionHeader {
       && var data := SerializeOneDataKey(k);
       && GetOneDataKey(data, 0).Success?
       && GetOneDataKey(data, 0).value.0 == k
-      && GetOneDataKey(data, 0).value.1 == |data|
+      && GetOneDataKey(data, 0).value.1 as nat == |data|
   {
     var data := SerializeOneDataKey(k);
     assert 2 <= |data|;
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
index 2ed337996..90be48143 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
@@ -8,6 +8,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
   import Relations
   import BoundedInts
   import InternalModule = Seq.MergeSort
+  import MemoryMath
 
   predicate HasUint64Len<T>(s: seq<T>) {
     |s| < BoundedInts.TWO_TO_THE_64
@@ -94,75 +95,8 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
   function {:isolate_assertions} MergeSortNat<T(!new)>(s: seq<T>, lessThanOrEq: (T, T) -> bool): (result :seq<T>)
     requires Relations.TotalOrdering(lessThanOrEq)
   {
-    InternalModule.MergeSortBy(s, lessThanOrEq)
-  }
-  by method {
-    if |s| <= 1 {
-      return s;
-    } else {
-
-      // The slice x[1..], y[1..] are un-optimized operations in Dafny.
-      // This means that their usage will result in a lot of data copying.
-      // Additional, it is very likely that these size of these sequences
-      // will be less than uint64.
-      // So writing an optimized version that only works on bounded types
-      // should further optimized this hot code.
-
-      var left := new T[|s|](i requires 0 <= i < |s| => s[i]);
-      var right := new T[|s|](i requires 0 <= i < |s| => s[i]);
-      var lo, hi := 0, right.Length;
-
-      label BEFORE_WORK:
-
-      if HasUint64Len(s) {
-        var boundedLo: BoundedInts.uint64, boundedHi: BoundedInts.uint64 := 0, right.Length as BoundedInts.uint64;
-        ghost var _ := MergeSortMethod(left, right, lessThanOrEq, boundedLo, boundedHi, Right);
-
-        result :=  right[..];
-      } else {
-        // Fallback to `nat` or BigInt.
-        // This is a little silly, but this ensures
-        // that the behavior for very large seq will be the same.
-        // Though it is likely if any such seq existed in the real world,
-        // the performance improvement here would still not be enough to complete the sort...
-        ghost var _ := NatMergeSortMethod(left, right, lessThanOrEq, lo, hi, Right);
-
-        result :=  right[..];
-      }
-
-      ghost var other := InternalModule.MergeSortBy(s, lessThanOrEq);
-
-      assert Relations.SortedBy(right[..], lessThanOrEq) by {
-        assert right[..] == right[lo..hi];
-      }
-      assert multiset(right[..]) == multiset(other) by {
-        calc {
-          multiset(right[..]);
-        == {assert right[..] == right[lo..hi];}
-          multiset(right[lo..hi]);
-        ==
-          multiset(old@BEFORE_WORK(left[lo..hi]));
-        == {assert old@BEFORE_WORK(left[lo..hi]) == s;}
-          multiset(s);
-        ==
-          multiset(other);
-        }
-      }
-
-      // Implementing a by method can be complicated.
-      // Because methods can have non-determinism,
-      // where functions can not.
-      // This means that Dafny normally wants to know
-      // that the method and function maintain equality at every step.
-      // But this is hard for this kind of optimized sorting.
-      // Because what is the functional state at every step
-      // and how does it correspond the state of 2 optimized arrays?
-      // This lemma works around this
-      // by proving that the outcomes are always deterministic and the same.
-      // It does this by proving that given a total ordering,
-      // there is one and only one way to sort a given sequence.
-      TotalOrderingImpliesSortingIsUnique(right[..], other, lessThanOrEq);
-    }
+    MemoryMath.SequenceIsSafeBecauseItIsInMemory(s);
+    MergeSort(s, lessThanOrEq)
   }
 
   datatype PlaceResults = Left | Right | Either
@@ -493,235 +427,4 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
     requires hi <= |s|
     ensures s[lo..hi] == s[lo..split] + s[split..hi]
   {}
-
-  // This is the nat version of merge sort.
-  // This is an exact copy of the bounded integer implementation above
-  // but with `nat` instead of BoundedInts.uint64.
-
-  method {:isolate_assertions} NatMergeSortMethod<T(!new)>(
-    left: array<T>,
-    right: array<T>,
-    lessThanOrEq: (T, T) -> bool,
-    lo: nat,
-    hi: nat,
-    where: PlaceResults
-  )
-    returns (resultPlacement: ResultPlacement)
-    requires Relations.TotalOrdering(lessThanOrEq)
-    requires lo < hi <= left.Length
-    requires hi <= right.Length && left != right
-    // reads left, right
-    modifies left, right
-    ensures !where.Either? ==> where == resultPlacement
-
-    // We do not modify anything before lo
-    ensures left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo])
-    // We do not modify anything above hi
-    ensures left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..])
-
-    ensures multiset(left[lo..hi]) == multiset(old(left[lo..hi]))
-    ensures resultPlacement.Left? ==> Relations.SortedBy(left[lo..hi], lessThanOrEq)
-    ensures resultPlacement.Right? ==> Relations.SortedBy(right[lo..hi], lessThanOrEq)
-    ensures resultPlacement.Right? ==> multiset(right[lo..hi]) == multiset(old(left[lo..hi]))
-
-    decreases hi - lo
-  {
-    if hi - lo == 1 {
-      if where == Right {
-        right[lo] := left[lo];
-        return Right;
-      } else {
-        return Left;
-      }
-    }
-
-    ghost var beforeWork := multiset(left[lo..hi]);
-    var mid :=  ((hi - lo)/2) + lo;
-    var placement? := NatMergeSortMethod(left, right, lessThanOrEq, lo, mid, Either);
-    assert left[mid..hi] == old(left[mid..hi]);
-    ghost var placement2? := NatMergeSortMethod(left, right, lessThanOrEq, mid, hi, placement?);
-    assert placement2? == placement?;
-
-    ghost var preMergeResult := if placement?.Left? then left else right;
-    calc {
-      multiset(preMergeResult[lo..hi]);
-    == { LemmaSplitAt(preMergeResult[..], lo as nat, mid as nat, hi as nat); }
-      multiset(preMergeResult[lo..mid] + preMergeResult[mid..hi]);
-    ==
-      multiset(old(left[lo..mid]) + old(left[mid..hi]));
-    ==  { LemmaSplitAt(old(left[..]), lo as nat, mid as nat, hi as nat); }
-      beforeWork;
-    }
-
-    ghost var mergedResult;
-    if placement?.Left? {
-      NatMergeIntoRight(left := left, right := right, lessThanOrEq := lessThanOrEq, lo := lo, mid := mid, hi := hi);
-      resultPlacement, mergedResult := Right, right[lo..hi];
-
-      assert left[hi..] == old(left[hi..]);
-      assert right[hi..] == old(right[hi..]);
-      assert left[..lo] == old(left[..lo]);
-      assert right[..lo] == old(right[..lo]);
-    } else {
-      assert placement?.Right?;
-      NatMergeIntoRight(left := right, right := left, lessThanOrEq := lessThanOrEq, lo := lo, mid := mid, hi := hi);
-      resultPlacement, mergedResult := Left, left[lo..hi];
-
-      assert left[hi..] == old(left[hi..]);
-      assert right[hi..] == old(right[hi..]);
-      assert left[..lo] == old(left[..lo]);
-      assert right[..lo] == old(right[..lo]);
-    }
-
-    label BEFORE_RETURN:
-    assert left[hi..] == old(left[hi..]);
-    assert right[hi..] == old(right[hi..]);
-    assert left[..lo] == old(left[..lo]);
-    assert right[..lo] == old(right[..lo]);
-    if resultPlacement.Left? && where == Right {
-      // A forall comprehension might seem like a nice fit here,
-      // however this does not good for two reasons.
-      // First, Dafny currently creates a range for the full bounds of the bounded number
-      // see: https://github.com/dafny-lang/dafny/issues/5897
-      // Second this would create two loops.
-      // First loop would create the `lo to hi` range of numbers.
-      // The second loop would then loop over these elements.
-      // A single loop with
-      for i := lo to hi
-        modifies right
-        invariant left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo])
-        invariant left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..])
-        invariant right[lo..i] == left[lo..i]
-      {
-        right[i] := left[i];
-        assert right[lo..i] == left[lo..i];
-      }
-
-      assert right[lo..hi] == mergedResult by {
-        assert mergedResult == left[lo..hi];
-      }
-      assert left[..] == old@BEFORE_RETURN(left[..]);
-      assert right[..lo] == old(right[..lo]);
-
-      resultPlacement := Right;
-    }
-    if resultPlacement.Right? && where == Left {
-      for i := lo to hi
-        modifies left
-        invariant left[..lo] == old(left[..lo]) && right[..lo] == old(right[..lo])
-        invariant left[hi..] == old(left[hi..]) && right[hi..] == old(right[hi..])
-        invariant left[lo..i] == right[lo..i]
-      {
-        left[i] := right[i];
-        assert right[lo..i] == left[lo..i];
-      }
-
-      assert left[lo..hi] == mergedResult by {
-        assert mergedResult == right[lo..hi];
-      }
-      assert right[..] == old@BEFORE_RETURN(right[..]);
-      assert left[..lo] == old(left[..lo]);
-
-      resultPlacement := Left;
-    }
-  }
-
-  method {:isolate_assertions} NatMergeIntoRight<T(!new)>(
-    nameonly left: array<T>,
-    nameonly right: array<T>,
-    nameonly lessThanOrEq: (T, T) -> bool,
-    nameonly lo: nat,
-    nameonly mid: nat,
-    nameonly hi: nat
-  )
-    requires Relations.TotalOrdering(lessThanOrEq)
-    requires lo <= mid <= hi <= left.Length
-    requires  hi <= right.Length && left != right
-    // We store "left" in [lo..mid]
-    requires Relations.SortedBy(left[lo..mid], lessThanOrEq)
-    // We store "right" in [mid..hi]
-    requires Relations.SortedBy(left[mid..hi], lessThanOrEq)
-    modifies right
-    // reads left, right
-    // We do not modify anything before lo
-    ensures right[..lo] == old(right[..lo]) && left[..lo] == old(left[..lo])
-    // We do not modify anything above hi
-    ensures right[hi..] == old(right[hi..]) && left[..lo] == old(left[..lo])
-    ensures Relations.SortedBy(right[lo..hi], lessThanOrEq)
-    ensures multiset(right[lo..hi]) == multiset(old(left[lo..hi]))
-    ensures multiset(left[lo..hi]) == multiset(old(left[lo..hi]))
-  {
-    var leftPosition, rightPosition, iter := lo, mid, lo;
-    while iter < hi
-      modifies right
-
-      invariant lo <= leftPosition <= mid <= rightPosition <= hi
-      invariant leftPosition as nat - lo as nat + rightPosition as nat - mid as nat == iter as nat - lo as nat
-      invariant right[..lo] == old(right[..lo])
-      invariant right[hi..] == old(right[hi..])
-
-      invariant Relations.SortedBy(left[leftPosition..mid], lessThanOrEq)
-      invariant Relations.SortedBy(left[rightPosition..hi], lessThanOrEq)
-      invariant Below(right[lo..iter], left[leftPosition..mid], lessThanOrEq)
-      invariant Below(right[lo..iter], left[rightPosition..hi], lessThanOrEq)
-      invariant Relations.SortedBy(right[lo..iter], lessThanOrEq)
-      invariant multiset(right[lo..iter]) == multiset(left[lo..leftPosition] + left[mid..rightPosition])
-    {
-
-      ghost var oldRightPosition, oldIter, oldLeftPosition := rightPosition, iter, leftPosition;
-      if leftPosition == mid || (rightPosition < hi && lessThanOrEq(left[rightPosition], left[leftPosition])) {
-        right[iter] := left[rightPosition];
-
-        PushStillSortedBy(right, lo as nat, iter as nat, lessThanOrEq);
-        rightPosition, iter := rightPosition + 1, iter + 1;
-
-        BelowIsTransitive(right[lo..iter], left[leftPosition..mid], lessThanOrEq);
-
-        assert 0 < |right[lo..iter]| && 0 < |left[rightPosition..hi]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[rightPosition..hi][0]) by {
-          if 0 == |right[lo..iter]| || 0 == |left[rightPosition..hi]| {
-          } else {
-            assert Relations.SortedBy(left[oldRightPosition..hi], lessThanOrEq);
-            assert lessThanOrEq(left[oldRightPosition..hi][0], left[oldRightPosition..hi][1]);
-          }
-        }
-        BelowIsTransitive(right[lo..iter], left[rightPosition..hi], lessThanOrEq);
-
-        assert multiset(right[lo..iter]) == multiset(left[lo..leftPosition] + left[mid..rightPosition]) by {
-          // Dafny just wants to be reminded
-        }
-      } else {
-        right[iter] := left[leftPosition];
-
-        PushStillSortedBy(right, lo as nat, iter as nat, lessThanOrEq);
-        leftPosition, iter := leftPosition + 1, iter + 1;
-
-        assert 0 < |right[lo..iter]| && 0 < |left[leftPosition..mid]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[leftPosition..mid][0]) by {
-          if 0 == |right[lo..iter]| || 0 == |left[leftPosition..mid]| {
-          } else {
-            assert Relations.SortedBy(left[oldLeftPosition..mid], lessThanOrEq);
-            assert lessThanOrEq(left[oldLeftPosition..mid][0], left[oldLeftPosition..mid][1]);
-          }
-        }
-        BelowIsTransitive(right[lo..iter], left[leftPosition..mid], lessThanOrEq);
-        assert 0 < |right[lo..iter]| && 0 < |left[rightPosition..hi]| ==> lessThanOrEq(right[lo..iter][|right[lo..iter]| - 1], left[rightPosition..hi][0]) by {
-          if 0 == |right[lo..iter]| || 0 == |left[rightPosition..hi]| {
-          } else {
-            assert right[lo..iter][|right[lo..iter]| - 1] == right[iter - 1];
-            assert left[rightPosition..hi][0] == left[rightPosition];
-          }
-        }
-        BelowIsTransitive(right[lo..iter], left[rightPosition..hi], lessThanOrEq);
-
-        assert multiset(right[lo..iter]) == multiset(left[lo..leftPosition] + left[mid..rightPosition]) by {
-          // Dafny just wants to be reminded
-        }
-      }
-    }
-    assert multiset(right[lo..hi]) == multiset(old(left[lo..hi])) by {
-      assert leftPosition == mid && rightPosition == hi;
-      LemmaSplitAt(left[..], lo as nat, mid as nat, hi as nat);
-      assert old(left[lo..hi]) == left[lo..hi] == left[lo..mid] + left[mid..hi];
-    }
-  }
-
 }
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy
index 5b64497bb..246f001ca 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy
@@ -19,12 +19,13 @@ module StructuredEncryptionPaths {
     | List(pos : uint64)
     | Map(key : GoodString)
 
-  type SelectorList = x : seq<Selector> | |x| < UINT64_LIMIT
+  type SelectorList = x : seq<Selector> | HasUint64Len(x)
   type TerminalSelector = x : seq<Selector> | ValidTerminalSelector(x) witness *
 
   predicate method ValidTerminalSelector(s : seq<Selector>)
   {
-    && 0 < |s| < UINT64_LIMIT
+    && 0 < |s|
+    && HasUint64Len(s)
     && s[0].Map?
   }
 
@@ -48,7 +49,7 @@ module StructuredEncryptionPaths {
 
   predicate method ValidPath(path : Path)
   {
-    && |path| < UINT64_LIMIT
+    && HasUint64Len(path)
     && forall x <- path :: ValidString(x.member.key)
   }
 
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy
index adef22ed7..f71513ff7 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy
@@ -8,6 +8,7 @@ module StructuredEncryptionUtil {
   import opened Wrappers
   import opened StandardLibrary
   import opened StandardLibrary.UInt
+  import opened MemoryMath
 
   import UTF8
   import CMP = AwsCryptographyMaterialProvidersTypes
@@ -182,7 +183,7 @@ module StructuredEncryptionUtil {
   type GoodString = x : string | ValidString(x)
   predicate method ValidString(x : string)
   {
-    && |x| <  UINT64_LIMIT
+    && HasUint64Len(x)
     && UTF8.Encode(x).Success?
   }
 
@@ -199,12 +200,13 @@ module StructuredEncryptionUtil {
 
   // sequences are equal if zero is returned
   // Some care should be taken to ensure that target languages don't over optimize this.
-  function method {:tailrecursion} ConstantTimeCompare(a : Bytes, b : Bytes, pos : nat := 0, acc : bv8 := 0) : bv8
+  function method {:tailrecursion} ConstantTimeCompare(a : Bytes, b : Bytes, pos : uint64 := 0, acc : bv8 := 0) : bv8
     requires |a| == |b|
-    requires 0 <= pos <= |a|
-    decreases |a| - pos
+    requires 0 <= pos as nat <= |a|
+    decreases |a| - pos as nat
   {
-    if |a| == pos then
+    SequenceIsSafeBecauseItIsInMemory(a);
+    if |a| as uint64 == pos then
       acc
     else
       var x := ((a[pos] as bv8) ^ (b[pos] as bv8));
@@ -288,7 +290,8 @@ module StructuredEncryptionUtil {
   {
     var keys : seq<UTF8.ValidUTF8Bytes> := SortedSets.ComputeSetToOrderedSequence2(ec.Keys, ByteLess);
     var ret : map<string, string> := map[];
-    for i := 0 to |keys| {
+    SequenceIsSafeBecauseItIsInMemory(keys);
+    for i : uint64 := 0 to |keys| as uint64 {
       var key :- expect UTF8.Decode(keys[i]);
       var value :- expect UTF8.Decode(ec[keys[i]]);
       ret := ret[key := value];
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy
index fbd200499..e7f7af88e 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/test/Header.dfy
@@ -114,7 +114,7 @@ module TestHeader {
     var newCont := GetContext(serCont);
     expect newCont.Success?;
     expect newCont.value.0 == cont;
-    expect newCont.value.1 == |serCont|;
+    expect newCont.value.1 == |serCont| as uint64;
 
     var badSerCont := [
       0,3, // three items
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index 515995e68..49e596b1c 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit 515995e68400e56fc720412fe355e6965715136e
+Subproject commit 49e596b1cd8ce446d0b82074ff48ba0406aa8995