diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy
index c1379da88..a6b9b428d 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/AwsCryptographyDbEncryptionSdkDynamoDbOperations.dfy
@@ -10,10 +10,11 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
   import AlgorithmSuites
   import Header = StructuredEncryptionHeader
   import opened DynamoDbEncryptionUtil
+  import opened StandardLibrary.MemoryMath
 
-  const SALT_LENGTH := 16
-  const IV_LENGTH := 12
-  const VERSION_LENGTH := 16
+  const SALT_LENGTH : uint64 := 16
+  const IV_LENGTH : uint64 := 12
+  const VERSION_LENGTH : uint64 := 16
 
   predicate ValidInternalConfig?(config: InternalConfig)
   {true}
@@ -70,7 +71,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
     var list : EncryptedDataKeyDescriptionList := [];
     //= specification/dynamodb-encryption-client/ddb-get-encrypted-data-key-description.md#behavior
     //# - For every Data Key in Data Keys, the operation MUST attempt to extract a description of the Data Key.
-    for i := 0 to |datakeys| {
+    for i : uint64 := 0 to |datakeys| as uint64 {
       var extractedKeyProviderId :- UTF8.Decode(datakeys[i].keyProviderId).MapFailure(e => E(e));
       var extractedKeyProviderIdInfo:= Option.None;
       var expectedBranchKeyVersion := Option.None;
@@ -91,7 +92,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbOperations refines AbstractAwsCrypt
           var EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX := SALT_LENGTH + IV_LENGTH;
           var EDK_CIPHERTEXT_VERSION_INDEX := EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX + VERSION_LENGTH;
           :- Need(EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX < EDK_CIPHERTEXT_VERSION_INDEX, E("Wrong branch key version index."));
-          :- Need(|providerWrappedMaterial| >= EDK_CIPHERTEXT_VERSION_INDEX, E("Incorrect ciphertext structure length."));
+          SequenceIsSafeBecauseItIsInMemory(providerWrappedMaterial);
+          :- Need(|providerWrappedMaterial| as uint64 >= EDK_CIPHERTEXT_VERSION_INDEX, E("Incorrect ciphertext structure length."));
           var branchKeyVersionUuid := providerWrappedMaterial[EDK_CIPHERTEXT_BRANCH_KEY_VERSION_INDEX .. EDK_CIPHERTEXT_VERSION_INDEX];
           var maybeBranchKeyVersion :- UUID.FromByteArray(branchKeyVersionUuid).MapFailure(e => E(e));
           expectedBranchKeyVersion := Some(maybeBranchKeyVersion);
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
index 3c102973c..77ed8b645 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
@@ -23,7 +23,7 @@ module SearchConfigToInfo {
   import opened DynamoDbEncryptionUtil
   import opened TermLoc
   import opened StandardLibrary.String
-  import opened MemoryMath
+  import opened StandardLibrary.MemoryMath
   import MaterialProviders
   import SortedSets
 
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy
index c609d5ac2..c92befb02 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy
@@ -19,6 +19,7 @@ module DynamoDBSupport {
   import opened Wrappers
   import opened StandardLibrary
   import opened StandardLibrary.UInt
+  import opened StandardLibrary.MemoryMath
   import opened DynamoDbEncryptionUtil
   import opened DdbVirtualFields
   import opened SearchableEncryptionInfo
@@ -33,23 +34,30 @@ module DynamoDBSupport {
   // At the moment, this means that no attribute names starts with "aws_dbe_",
   // as all other attribute names would need to be configured, and all the
   // other weird constraints were checked at configuration time.
-  function method IsWriteable(item : DDB.AttributeMap)
-    : (ret : Result<bool, string>)
+  method IsWriteable(item : DDB.AttributeMap)
+    returns (ret : Result<bool, string>)
     //= specification/dynamodb-encryption-client/ddb-support.md#writable
     //= type=implication
     //# Writeable MUST reject any item containing an attribute which begins with `aws_dbe_`.
     ensures ret.Success? ==> forall k <- item :: !(ReservedPrefix <= k)
   {
-    if forall k <- item :: !(ReservedPrefix <= k) then
-      Success(true)
-    else
-      var bad := set k <- item | ReservedPrefix <= k;
-      // We happen to order these values, but this ordering MUST NOT be relied upon.
-      var badSeq := SortedSets.ComputeSetToOrderedSequence2(bad, CharLess);
-      if |badSeq| == 0 then
-        Failure("")
-      else
-        Failure("Writing reserved attributes not allowed : " + Join(badSeq, "\n"))
+    var keys := SortedSets.ComputeSetToOrderedSequence2(item.Keys, CharLess);
+    SequenceIsSafeBecauseItIsInMemory(keys);
+    var rp := ReservedPrefix; // because the constant ReservedPrefix is actual an expensive function call
+    for i : uint64 := 0 to |keys| as uint64
+      invariant forall j | 0 <= j < i :: !(ReservedPrefix <= keys[j])
+    {
+      if rp <= keys[i] {
+        var result := "Writing reserved attributes not allowed : ";
+        for j : uint64 := i to |keys| as uint64 {
+          if rp <= keys[i] {
+            result := result + keys[i] + "\n";
+          }
+        }
+        return Failure(result);
+      }
+    }
+    return Success(true);
   }
 
   function method GetEncryptedAttributes(
@@ -83,7 +91,8 @@ module DynamoDBSupport {
   {
     if expr.Some? then
       var attrs := GetEncryptedAttributes(actions, expr, attrNames);
-      if |attrs| == 0 then
+      SequenceIsSafeBecauseItIsInMemory(attrs);
+      if |attrs| as uint64 == 0 then
         Success(true)
       else
         Failure("Condition Expressions forbidden on encrypted attributes : " + Join(attrs, ","))
@@ -121,7 +130,8 @@ module DynamoDBSupport {
     if expr.Some? then
       var attrs := Update.ExtractAttributes(expr.value, attrNames);
       var encryptedAttrs := Seq.Filter(s => IsSigned(actions, s), attrs);
-      if |encryptedAttrs| == 0 then
+      SequenceIsSafeBecauseItIsInMemory(encryptedAttrs);
+      if |encryptedAttrs| as uint64 == 0 then
         Success(true)
       else
         Failure("Update Expressions forbidden on signed attributes : " + Join(encryptedAttrs, ","))
@@ -169,11 +179,13 @@ module DynamoDBSupport {
       //# if the constructed compound beacon does not match
       //# the existing attribute value AddSignedBeacons MUST fail.
       var badAttrs := set k <- newAttrs | k in item && item[k] != newAttrs[k] :: k;
-      :- Need(|badAttrs| == 0, E("Signed beacons have generated values different from supplied values."));
+      SetIsSafeBecauseItIsInMemory(badAttrs);
+      :- Need(|badAttrs| as uint64 == 0, E("Signed beacons have generated values different from supplied values."));
       var version : DDB.AttributeMap := map[VersionTag := DS(" ")];
       var both := newAttrs.Keys * item.Keys;
       var bad := set k <- both | newAttrs[k] != item[k];
-      if 0 < |bad| {
+      SetIsSafeBecauseItIsInMemory(bad);
+      if 0 < |bad| as uint64 {
         // We happen to order these values, but this ordering MUST NOT be relied upon.
         var badSeq := SortedSets.ComputeSetToOrderedSequence2(bad, CharLess);
         return Failure(E("Supplied Beacons do not match calculated beacons : " + Join(badSeq, ", ")));
@@ -254,7 +266,8 @@ module DynamoDBSupport {
         req.FilterExpression,
         req.ExpressionAttributeNames,
         req.ExpressionAttributeValues);
-      :- Need(|newItems| < INT32_MAX_LIMIT, DynamoDbEncryptionUtil.E("This is impossible."));
+      SequenceIsSafeBecauseItIsInMemory(newItems);
+      :- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible."));
       var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), newItems);
       var count :=
         if resp.Count.Some? then
@@ -323,7 +336,8 @@ module DynamoDBSupport {
         req.FilterExpression,
         req.ExpressionAttributeNames,
         req.ExpressionAttributeValues);
-      :- Need(|newItems| < INT32_MAX_LIMIT, DynamoDbEncryptionUtil.E("This is impossible."));
+      SequenceIsSafeBecauseItIsInMemory(newItems);
+      :- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible."));
       var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), newItems);
       var count :=
         if resp.Count.Some? then
@@ -344,14 +358,15 @@ module DynamoDBSupport {
     requires forall x <- results :: x in bv.virtualFields
     ensures output.Success? ==> forall x <- output.value :: x in bv.virtualFields
   {
-    if |fields| == 0 then
+    SequenceIsSafeBecauseItIsInMemory(fields);
+    if |fields| as uint64 == 0 then
       Success(results)
     else
-      var optValue :- GetVirtField(bv.virtualFields[fields[0]], item);
+      var optValue :- GetVirtField(bv.virtualFields[fields[0 as uint32]], item);
       if optValue.Some? then
-        GetVirtualFieldsLoop(fields[1..], bv, item, results[fields[0] := optValue.value])
+        GetVirtualFieldsLoop(fields[1 as uint32..], bv, item, results[fields[0 as uint32] := optValue.value])
       else
-        GetVirtualFieldsLoop(fields[1..], bv, item, results)
+        GetVirtualFieldsLoop(fields[1 as uint32..], bv, item, results)
   }
 
   method GetVirtualFields(beaconVersion : SearchableEncryptionInfo.BeaconVersion, item : DDB.AttributeMap)
@@ -371,18 +386,19 @@ module DynamoDBSupport {
     requires forall x <- results :: x in bv.beacons
     ensures output.Success? ==> forall x <- output.value :: x in bv.beacons
   {
-    if |fields| == 0 then
+    SequenceIsSafeBecauseItIsInMemory(fields);
+    if |fields| as uint64  == 0 then
       Success(results)
     else
-      var beacon := bv.beacons[fields[0]];
+      var beacon := bv.beacons[fields[0 as uint32]];
       if beacon.Compound? then
         var optValue :- beacon.cmp.getNaked(item, bv.virtualFields);
         if optValue.Some? then
-          GetCompoundBeaconsLoop(fields[1..], bv, item, results[fields[0] := optValue.value])
+          GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results[fields[0] := optValue.value])
         else
-          GetCompoundBeaconsLoop(fields[1..], bv, item, results)
+          GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results)
       else
-        GetCompoundBeaconsLoop(fields[1..], bv, item, results)
+        GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results)
   }
 
   method GetCompoundBeacons(beaconVersion : SearchableEncryptionInfo.BeaconVersion, item : DDB.AttributeMap)
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy
index 28ec03ced..35a175195 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy
@@ -20,7 +20,7 @@ module DynamoToStruct {
   import SE = StructuredEncryptionUtil
   import StandardLibrary.Sequence
   import DafnyLibraries
-  import opened MemoryMath
+  import opened StandardLibrary.MemoryMath
 
   type Error = Types.Error
 
@@ -126,7 +126,7 @@ module DynamoToStruct {
       var badNames := set k <- s | !IsValid_AttributeName(k) :: k;
       OneBadKey(s, badNames, IsValid_AttributeName);
       // We happen to order these values, but this ordering MUST NOT be relied upon.
-      var orderedAttrNames := SetToOrderedSequence(badNames, CharLess);
+      var orderedAttrNames := SortedSets.ComputeSetToOrderedSequence2(badNames, CharLess);
       var attrNameList := Join(orderedAttrNames, ",");
       MakeError("Not valid attribute names : " + attrNameList)
   }
@@ -192,10 +192,10 @@ module DynamoToStruct {
       Success(attrValueAndLength.val)
   }
 
-  const BOOL_LEN : nat := 1   // number of bytes in an encoded boolean
-  const TYPEID_LEN : nat := 2   // number of bytes in a TerminalTypeId
-  const LENGTH_LEN : nat := 4 // number of bytes in an encoded count or length
-  const PREFIX_LEN : nat := 6 // number of bytes in a prefix, i.e. 2-byte type and 4-byte length
+  ghost const BOOL_LEN : nat := 1   // number of bytes in an encoded boolean
+  ghost const TYPEID_LEN : nat := 2   // number of bytes in a TerminalTypeId
+  ghost const LENGTH_LEN : nat := 4 // number of bytes in an encoded count or length
+  ghost const PREFIX_LEN : nat := 6 // number of bytes in a prefix, i.e. 2-byte type and 4-byte length
 
   const BOOL_LEN64 : uint64 := 1   // number of bytes in an encoded boolean
   const TYPEID_LEN64 : uint64 := 2   // number of bytes in a TerminalTypeId
@@ -448,7 +448,8 @@ module DynamoToStruct {
       case BOOL(b) => Success([BoolToUint8(b)])
     };
     if prefix then
-      var len :- U32ToBigEndian(|baseBytes|);
+      SequenceIsSafeBecauseItIsInMemory(baseBytes);
+      var len :- U32ToBigEndian64(|baseBytes| as uint64);
       Success(AttrToTypeId(a) + len + baseBytes)
     else
       Success(baseBytes)
@@ -458,13 +459,15 @@ module DynamoToStruct {
     ensures ret.Success? ==> Seq.HasNoDuplicates(ss)
   {
     var asSet := Seq.ToSet(ss);
-    :- Need(|asSet| == |ss|, "String Set had duplicate values");
+    SequenceIsSafeBecauseItIsInMemory(ss);
+    SetIsSafeBecauseItIsInMemory(asSet);
+    :- Need(|asSet| as uint64 == |ss| as uint64, "String Set had duplicate values");
     Seq.LemmaNoDuplicatesCardinalityOfSet(ss);
 
     //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entries
     //# Entries in a String Set MUST be ordered in ascending [UTF-16 binary order](./string-ordering.md#utf-16-binary-order).
     var sortedList := SortedSets.ComputeSetToOrderedSequence2(asSet, CharLess);
-    var count :- U32ToBigEndian(|sortedList|);
+    var count :- U32ToBigEndian64(|sortedList| as uint64);
     var body :- CollectString(sortedList);
     Success(count + body)
   }
@@ -473,12 +476,15 @@ module DynamoToStruct {
     ensures ret.Success? ==> Seq.HasNoDuplicates(ns)
   {
     var asSet := Seq.ToSet(ns);
-    :- Need(|asSet| == |ns|, "Number Set had duplicate values");
+    SequenceIsSafeBecauseItIsInMemory(ns);
+    SetIsSafeBecauseItIsInMemory(asSet);
+    :- Need(|asSet| as uint64 == |ns| as uint64, "Number Set had duplicate values");
     Seq.LemmaNoDuplicatesCardinalityOfSet(ns);
 
     var normList :- Sequence.MapWithResult(n => Norm.NormalizeNumber(n), ns);
     var asSet := Seq.ToSet(normList);
-    :- Need(|asSet| == |normList|, "Number Set had duplicate values after normalization.");
+    SetIsSafeBecauseItIsInMemory(asSet);
+    :- Need(|asSet| as uint64 == |normList| as uint64, "Number Set had duplicate values after normalization.");
 
     //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entries
     //# Entries in a Number Set MUST be ordered in ascending [UTF-16 binary order](./string-ordering.md#utf-16-binary-order).
@@ -486,7 +492,8 @@ module DynamoToStruct {
     //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entries
     //# This ordering MUST be applied after normalization of the number value.
     var sortedList := SortedSets.ComputeSetToOrderedSequence2(asSet, CharLess);
-    var count :- U32ToBigEndian(|sortedList|);
+    SequenceIsSafeBecauseItIsInMemory(sortedList);
+    var count :- U32ToBigEndian64(|sortedList| as uint64);
     var body :- CollectString(sortedList);
     Success(count + body)
   }
@@ -499,13 +506,16 @@ module DynamoToStruct {
               && ret.value[..LENGTH_LEN] == U32ToBigEndian(|bs|).value
   {
     var asSet := Seq.ToSet(bs);
-    :- Need(|asSet| == |bs|, "Binary Set had duplicate values");
+    SequenceIsSafeBecauseItIsInMemory(bs);
+    SetIsSafeBecauseItIsInMemory(asSet);
+    :- Need(|asSet| as uint64 == |bs| as uint64, "Binary Set had duplicate values");
     Seq.LemmaNoDuplicatesCardinalityOfSet(bs);
 
     //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#set-entries
     //# Entries in a Binary Set MUST be ordered lexicographically by their underlying bytes in ascending order.
     var sortedList := SortedSets.ComputeSetToOrderedSequence2(asSet, ByteLess);
-    var count :- U32ToBigEndian(|sortedList|);
+    SequenceIsSafeBecauseItIsInMemory(sortedList);
+    var count :- U32ToBigEndian64(|sortedList| as uint64);
     var body :- CollectBinary(sortedList);
     Success(count + body)
   }
@@ -533,7 +543,8 @@ module DynamoToStruct {
     //# and MAY hold values of different types.
     var bytesResults := map k <- m :: k := AttrToBytes(m[k], true, depth+1);
 
-    var count :- U32ToBigEndian(|m|);
+    MapIsSafeBecauseItIsInMemory(m);
+    var count :- U32ToBigEndian64(|m| as uint64);
     var bytes :- SimplifyMapValue(bytesResults);
     var body :- CollectMap(bytes);
     Success(count + body)
@@ -547,7 +558,8 @@ module DynamoToStruct {
               && ret.value[..LENGTH_LEN] == U32ToBigEndian(|l|).value
     decreases l
   {
-    var count :- U32ToBigEndian(|l|);
+    SequenceIsSafeBecauseItIsInMemory(l);
+    var count :- U32ToBigEndian64(|l| as uint64);
     var body :- CollectList(l, depth);
     Success(count + body)
   }
@@ -570,7 +582,8 @@ module DynamoToStruct {
               && U32ToBigEndian(BigEndianToU32(x).value).value == x
   {}
 
-  function method U32ToBigEndian(x : nat) : (ret : Result<seq<uint8>, string>)
+  // This ghost version is for use in ensures
+  function U32ToBigEndian(x : nat) : (ret : Result<seq<uint8>, string>)
     ensures ret.Success? ==> |ret.value| == LENGTH_LEN
   {
     if !HasUint32Size(x) then
@@ -579,28 +592,45 @@ module DynamoToStruct {
       Success(UInt32ToSeq(x as uint32))
   }
 
-  function method BigEndianToU32(x : seq<uint8>) : (ret : Result<nat, string>)
+  function method U32ToBigEndian64(x : uint64) : (ret : Result<seq<uint8>, string>)
+    ensures ret.Success? ==> |ret.value| == LENGTH_LEN
+    ensures ret == U32ToBigEndian(x as nat)
+  {
+    if x > 0xffff_ffff then
+      Failure("Length was too big")
+    else
+      Success(UInt32ToSeq(x as uint32))
+  }
+
+  function BigEndianToU32(x : seq<uint8>) : (ret : Result<nat, string>)
   {
-    if |x| < LENGTH_LEN then
+    SequenceIsSafeBecauseItIsInMemory(x);
+    if |x| as uint64 < LENGTH_LEN64 then
       Failure("Length of 4-byte integer was less than 4")
     else
-      Success(SeqToUInt32(x[..LENGTH_LEN]) as nat)
+      Success(SeqToUInt32(x[..LENGTH_LEN64]) as nat)
   }
 
   function method BigEndianToU32As32(x : seq<uint8>) : (ret : Result<uint32, string>)
+    ensures ret.Failure? ==> BigEndianToU32(x).Failure? && ret.error == BigEndianToU32(x).error
+    ensures ret.Success? ==> BigEndianToU32(x).Success? && ret.value as nat == BigEndianToU32(x).value
   {
-    if |x| < LENGTH_LEN then
+    SequenceIsSafeBecauseItIsInMemory(x);
+    if |x| as uint64 < LENGTH_LEN64 then
       Failure("Length of 4-byte integer was less than 4")
     else
-      Success(SeqToUInt32(x[..LENGTH_LEN]))
+      Success(SeqToUInt32(x[..LENGTH_LEN64]))
   }
 
   function method BigEndianToU32As64(x : seq<uint8>) : (ret : Result<uint64, string>)
+    ensures ret.Failure? ==> BigEndianToU32(x).Failure? && ret.error == BigEndianToU32(x).error
+    ensures ret.Success? ==> BigEndianToU32(x).Success? && ret.value as nat == BigEndianToU32(x).value
   {
-    if |x| < LENGTH_LEN then
+    SequenceIsSafeBecauseItIsInMemory(x);
+    if |x| as uint64 < LENGTH_LEN64 then
       Failure("Length of 4-byte integer was less than 4")
     else
-      Success(SeqToUInt32(x[..LENGTH_LEN]) as uint64)
+      Success(SeqToUInt32(x[..LENGTH_LEN64]) as uint64)
   }
 
   predicate IsSorted<T>(s: seq<T>, lessThanOrEq: (T, T) -> bool) {
@@ -618,7 +648,8 @@ module DynamoToStruct {
               && ret.value[LENGTH_LEN..] == UTF8.Encode(s).value
   {
     var val :- UTF8.Encode(s);
-    var len :- U32ToBigEndian(|val|);
+    SequenceIsSafeBecauseItIsInMemory(val);
+    var len :- U32ToBigEndian64(|val| as uint64);
     Success(len + val)
   }
   // String Set or Number Set to Bytes
@@ -658,7 +689,8 @@ module DynamoToStruct {
               && ret.value[0..LENGTH_LEN] == U32ToBigEndian(|b|).value
               && ret.value[LENGTH_LEN..] == b
   {
-    var len :- U32ToBigEndian(|b|);
+    SequenceIsSafeBecauseItIsInMemory(b);
+    var len :- U32ToBigEndian64(|b| as uint64);
     Success(len + b)
   }
 
@@ -784,7 +816,8 @@ module DynamoToStruct {
   {
     var name :- UTF8.Encode(key);
     assert UTF8.Decode(name).Success?;
-    var len :- U32ToBigEndian(|name|);
+    SequenceIsSafeBecauseItIsInMemory(name);
+    var len :- U32ToBigEndian64(|name| as uint64);
 
     //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#key-value-pair-entries
     //# Each key-value pair MUST be serialized as:
@@ -851,8 +884,16 @@ module DynamoToStruct {
   )
 
   predicate method IsUnique<T(==)>(s : seq<T>)
+    ensures IsUnique(s) ==> Seq.HasNoDuplicates(s)
   {
-    |set x:T | x in s :: x| == |s|
+    var asSet := Seq.ToSet(s);
+    SequenceIsSafeBecauseItIsInMemory(s);
+    SetIsSafeBecauseItIsInMemory(asSet);
+    if |asSet| as uint64 == |s| as uint64 then
+      Seq.LemmaNoDuplicatesCardinalityOfSet(s);
+      true
+    else
+      false
   }
 
   // Bytes to Binary Set
@@ -873,15 +914,16 @@ module DynamoToStruct {
     //# - Conversion from a Structured Data Binary Set MUST fail if it has duplicate values
     ensures ret.Success? && (remainingCount == 0) ==> IsUnique(resultSet.val.BS)
   {
+    SequenceIsSafeBecauseItIsInMemory(serialized);
     if remainingCount == 0 then
       :- Need(IsUnique(resultSet.val.BS), "Binary set values must not have duplicates");
       Success(resultSet)
-    else if |serialized| < LENGTH_LEN then
+    else if |serialized| as uint64 < LENGTH_LEN64 then
       Failure("Out of bytes reading Binary Set")
     else
       var len :- BigEndianToU32As64(serialized);
-      var serialized := serialized[LENGTH_LEN..];
-      if |serialized| < len as int then
+      var serialized := serialized[LENGTH_LEN64..];
+      if |serialized| as uint64 < len then
         Failure("Binary Set Structured Data has too few bytes")
       else
         var nattr := AttributeValue.BS(resultSet.val.BS + [serialized[..len]]);
@@ -906,15 +948,16 @@ module DynamoToStruct {
     //# - Conversion from a Structured Data String Set MUST fail if it has duplicate values
     ensures ret.Success? && (remainingCount == 0) ==> IsUnique(resultSet.val.SS)
   {
+    SequenceIsSafeBecauseItIsInMemory(serialized);
     if remainingCount == 0 then
       :- Need(IsUnique(resultSet.val.SS), "String set values must not have duplicates");
       Success(resultSet)
-    else if |serialized| < LENGTH_LEN then
+    else if |serialized| as uint64 < LENGTH_LEN64 then
       Failure("Out of bytes reading String Set")
     else
       var len : uint64 :- BigEndianToU32As64(serialized);
-      var serialized := serialized[LENGTH_LEN..];
-      if |serialized| < len as int then
+      var serialized := serialized[LENGTH_LEN64..];
+      if |serialized| as uint64 < len then
         Failure("String Set Structured Data has too few bytes")
       else
         var nstring :- UTF8.Decode(serialized[..len]);
@@ -940,15 +983,16 @@ module DynamoToStruct {
     //# - Conversion from a Structured Data Number Set MUST fail if it has duplicate values
     ensures ret.Success? && (remainingCount == 0) ==> IsUnique(resultSet.val.NS)
   {
+    SequenceIsSafeBecauseItIsInMemory(serialized);
     if remainingCount == 0 then
       :- Need(IsUnique(resultSet.val.NS), "Number set values must not have duplicates");
       Success(resultSet)
-    else if |serialized| < LENGTH_LEN then
+    else if |serialized| as uint64 < LENGTH_LEN64 then
       Failure("Out of bytes reading String Set")
     else
       var len :- BigEndianToU32As64(serialized);
-      var serialized := serialized[LENGTH_LEN..];
-      if |serialized| < len as int then
+      var serialized := serialized[LENGTH_LEN64..];
+      if |serialized| as uint64 < len then
         Failure("Number Set Structured Data has too few bytes")
       else
         var nstring :- UTF8.Decode(serialized[..len]);
@@ -1369,7 +1413,7 @@ module DynamoToStruct {
       var badValues := FlattenErrors(m);
       assert(|badValues| > 0);
       // We happen to order these values, but this ordering MUST NOT be relied upon.
-      var badValueSeq := SetToOrderedSequence(badValues, CharLess);
+      var badValueSeq := SortedSets.ComputeSetToOrderedSequence2(badValues, CharLess);
       Failure(Join(badValueSeq, "\n"))
   }
 }
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy
index 7bdc12b0a..101565456 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy
@@ -26,6 +26,7 @@ module TermLoc {
   import opened StandardLibrary.UInt
   import opened AwsCryptographyDbEncryptionSdkDynamoDbTypes
   import opened DynamoDbEncryptionUtil
+  import opened StandardLibrary.MemoryMath
   import StandardLibrary.String
   import DDB = ComAmazonawsDynamodbTypes
   import Seq
@@ -36,8 +37,7 @@ module TermLoc {
     | Map(key : string)
 
   type Bytes = seq<uint8>
-  type SelectorList = x : seq<Selector> | HasUint64Len(x)
-
+  type SelectorList = seq<Selector>
   //= specification/searchable-encryption/virtual.md#terminal-location
   //= type=implication
   //# A Terminal Location specification MUST be a list of one more [Segments](#segments),
@@ -45,39 +45,40 @@ module TermLoc {
   type TermLoc = x : seq<Selector> | ValidTermLoc(x) witness *
   predicate method ValidTermLoc(s : seq<Selector>)
   {
-    && 0 < |s|
-    && HasUint64Len(s)
-    && s[0].Map?
+    SequenceIsSafeBecauseItIsInMemory(s);
+    && 0 < |s| as uint64
+    && s[0 as uint32].Map?
   }
 
   function method TermLocToString(t : TermLoc) : string
   {
-    t[0].key + SelectorListToString(t[1..])
+    t[0 as uint32].key + SelectorListToString(t[1 as uint32..])
   }
   function method SelectorListToString(s : SelectorList) : string
   {
-    if |s| == 0 then
+    SequenceIsSafeBecauseItIsInMemory(s);
+    if |s| as uint64 == 0 then
       ""
-    else if s[0].Map? then
-      "." + s[0].key + SelectorListToString(s[1..])
+    else if s[0 as uint32].Map? then
+      "." + s[0 as uint32].key + SelectorListToString(s[1 as uint32..])
     else
-      "[" + String.Base10Int2String(s[0].pos as int) + "]" + SelectorListToString(s[1..])
+      "[" + String.Base10Int2String(s[0 as uint32].pos as int) + "]" + SelectorListToString(s[1 as uint32..])
   }
 
   // return true if item does not have the given terminal
   predicate method LacksAttribute(t : TermLoc, item : DDB.AttributeMap)
   {
-    t[0].key !in item
+    t[0 as uint32].key !in item
   }
 
   // return the AttributeValue for the given terminal in the given item
   function method TermToAttr(t : TermLoc, item : DDB.AttributeMap, names : Option<DDB.ExpressionAttributeNameMap>)
     : Option<DDB.AttributeValue>
   {
-    if t[0].key !in item then
+    if t[0 as uint32].key !in item then
       None
     else
-      var res := GetTerminal(item[t[0].key], t[1..], names);
+      var res := GetTerminal(item[t[0 as uint32].key], t[1 as uint32..], names);
       if res.Success? then
         Some(res.value)
       else
@@ -116,7 +117,8 @@ module TermLoc {
   )
     : Result<DDB.AttributeValue, Error>
   {
-    if |parts| == 0 then
+    SequenceIsSafeBecauseItIsInMemory(parts);
+    if |parts| as uint64 == 0 then
       Success(v)
     else
       match v {
@@ -129,22 +131,23 @@ module TermLoc {
         case BOOL(b) => Failure(E("Found boolean with parts left over."))
         case NULL(n) => Failure(E("Found null with parts left over."))
         case L(l) =>
-          if !parts[0].List? then
+          SequenceIsSafeBecauseItIsInMemory(l);
+          if !parts[0 as uint32].List? then
             Failure(E("Tried to access list with key"))
-          else if |l| <= parts[0].pos as int then
+          else if |l| as uint64 <= parts[0 as uint32].pos then
             Failure(E("Tried to access beyond the end of the list"))
           else
-            GetTerminal(l[parts[0].pos], parts[1..], names)
+            GetTerminal(l[parts[0 as uint32].pos], parts[1 as uint32..], names)
         case M(m) =>
-          if !parts[0].Map? then
+          if !parts[0 as uint32].Map? then
             Failure(E("Tried to access map with index"))
-          else if parts[0].key !in m then
-            if names.Some? && parts[0].key in names.value && names.value[parts[0].key] in m then
-              GetTerminal(m[names.value[parts[0].key]], parts[1..], names)
+          else if parts[0 as uint32].key !in m then
+            if names.Some? && parts[0 as uint32].key in names.value && names.value[parts[0 as uint32].key] in m then
+              GetTerminal(m[names.value[parts[0 as uint32].key]], parts[1 as uint32..], names)
             else
-              Failure(E("Tried to access " + parts[0].key + " which is not in the map."))
+              Failure(E("Tried to access " + parts[0 as uint32].key + " which is not in the map."))
           else
-            GetTerminal(m[parts[0].key], parts[1..], names)
+            GetTerminal(m[parts[0 as uint32].key], parts[1 as uint32..], names)
       }
   }
 
@@ -175,9 +178,9 @@ module TermLoc {
   // return the number of characters until the next part begins
   // that is, '[' or '.'
   function method  {:opaque} FindStartOfNext(s : string)
-    : (index : Option<nat>)
+    : (index : Option<uint64>)
     ensures index.Some? ==>
-              && index.value < |s|
+              && index.value as nat < |s|
               && (s[index.value] == '.' || s[index.value] == '[')
               && '.' !in s[..index.value]
               && '[' !in s[..index.value]
@@ -199,15 +202,22 @@ module TermLoc {
   }
 
   // read an unsigned decimal number, return value and length
-  function method {:opaque} GetNumber(s : string, acc : nat := 0)
-    : Result<nat, Error>
+  // error if value exceeds 2^64
+  function method {:opaque} GetNumber(s : string, acc : uint64 := 0, pos : uint64 := 0)
+    : Result<uint64, Error>
+    requires pos as nat <= |s|
+    decreases |s| - pos as nat
   {
-    if |s| == 0 then
+    SequenceIsSafeBecauseItIsInMemory(s);
+    if |s| as uint64 == pos then
       Success(acc)
-    else if '0' <= s[0] <= '9' then
-      GetNumber(s[1..], acc * 10 + s[0] as nat - '0' as nat)
+    else if '0' <= s[0 as uint32] <= '9' then
+      if acc < 0xfff_ffff_ffff_ffff then
+        GetNumber(s, acc * 10 + s[0 as uint32] as uint64 - '0' as uint64, Add(pos, 1))
+      else
+        Failure(E("Number is too big for list index : " + s))
     else
-      Failure(E("Unexpected character in number : " + [s[0]]))
+      Failure(E("Unexpected character in number : " + [s[0 as uint32]]))
   }
 
   // convert string to Selector
@@ -225,15 +235,15 @@ module TermLoc {
               && (s[0] == '.' ==> ret.value.Map?)
               && (s[0] == '[' ==> ret.value.List?)
   {
-    if s[0] == '.' then
-      Success(Map(s[1..]))
+    SequenceIsSafeBecauseItIsInMemory(s);
+    if s[0 as uint32] == '.' then
+      Success(Map(s[1 as uint32..]))
     else
-    if s[|s|-1] != ']' then
+    if s[|s| as uint64 - 1] != ']' then
       Failure(E("List index must end with ]"))
     else
-      var num :- GetNumber(s[1..|s|-1]);
-      :- Need(HasUint64Size(num), E("Array selector exceeds maximum."));
-      Success(List(num as uint64))
+      var num :- GetNumber(s[1 as uint32..|s| as uint64 - 1]);
+      Success(List(num))
   }
 
   // convert string to SelectorList
@@ -241,10 +251,10 @@ module TermLoc {
     : Result<SelectorList, Error>
     requires |s| > 0 && (s[0] == '.' || s[0] == '[')
   {
-    var pos := FindStartOfNext(s[1..]);
-    var end := if pos.None? then |s| else pos.value + 1;
+    SequenceIsSafeBecauseItIsInMemory(s);
+    var pos := FindStartOfNext(s[1 as uint32..]);
+    var end := if pos.None? then |s| as uint64 else Add(pos.value, 1);
     var sel : Selector :- GetSelector(s[..end]);
-    :- Need(HasUint64Size(|acc|+1), E("Selector Overflow"));
     if pos.None? then
       Success(acc + [sel])
     else
@@ -256,7 +266,8 @@ module TermLoc {
     : (ret : Result<TermLoc, Error>)
     ensures ret.Success? ==> 0 < |ret.value|
   {
-    :- Need(0 < |s|, E("Path specification must not be empty."));
+    SequenceIsSafeBecauseItIsInMemory(s);
+    :- Need(0 < |s| as uint64, E("Path specification must not be empty."));
     var pos := FindStartOfNext(s);
     if pos.None? then
       var m := Map(s);
@@ -264,7 +275,6 @@ module TermLoc {
     else
       var name := s[..pos.value];
       var selectors :- GetSelectors(s[pos.value..]);
-      :- Need(HasUint64Size(|selectors|+1), E("Selector Overflow"));
       Success([Map(name)] + selectors)
   }
 
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy
index ab5524224..4e9e956a8 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy
@@ -16,6 +16,7 @@ module DynamoDbMiddlewareSupport {
   import opened Wrappers
   import opened StandardLibrary
   import opened StandardLibrary.UInt
+  import opened StandardLibrary.MemoryMath
   import opened BS = DynamoDBSupport
   import opened DdbMiddlewareConfig
   import AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations
@@ -26,21 +27,23 @@ module DynamoDbMiddlewareSupport {
 
   predicate method NoMap<X,Y>(m : Option<map<X,Y>>)
   {
-    m.None? || |m.value| == 0
+    OptionalMapIsSafeBecauseItIsInMemory(m);
+    m.None? || |m.value| as uint64 == 0
   }
 
   predicate method NoList<X>(m : Option<seq<X>>)
   {
-    m.None? || |m.value| == 0
+    OptionalSequenceIsSafeBecauseItIsInMemory(m);
+    m.None? || |m.value| as uint64 == 0
   }
 
   // IsWritable examines an AttributeMap and fails if it is unsuitable for writing.
   // Generally this means that no attribute names starts with "aws_dbe_"
-  function method {:opaque} IsWriteable(config : ValidTableConfig, item : DDB.AttributeMap)
-    : Result<bool, Error>
+  method {:opaque} IsWriteable(config : ValidTableConfig, item : DDB.AttributeMap)
+    returns (ret : Result<bool, Error>)
   {
-    BS.IsWriteable(item)
-    .MapFailure(e => E(e))
+    var is_writable := BS.IsWriteable(item);
+    return is_writable.MapFailure(e => E(e));
   }
 
   // IsSigned returned whether this attribute is signed according to this config
@@ -160,9 +163,10 @@ module DynamoDbMiddlewareSupport {
       //# then `beacon key id` MUST be obtained from [Get beacon key id from parsed header](#get-beacon-key-id-from-parsed-header).
       :- Need(output.parsedHeader.Some?, E("In multi-tenant mode, the parsed header is required."));
       var keys := output.parsedHeader.value.encryptedDataKeys;
-      :- Need(|keys| == 1, E("Encrypt header has more than one Encrypted Data Key"));
-      :- Need(keys[0].keyProviderId == HierarchicalKeyringId, E("In multi-tenant mode, keyProviderId must be aws-kms-hierarchy"));
-      var keyId :- UTF8.Decode(keys[0].keyProviderInfo).MapFailure(e => E(e));
+      SequenceIsSafeBecauseItIsInMemory(keys);
+      :- Need(|keys| as uint64 == 1, E("Encrypt header has more than one Encrypted Data Key"));
+      :- Need(keys[0 as uint32].keyProviderId == HierarchicalKeyringId, E("In multi-tenant mode, keyProviderId must be aws-kms-hierarchy"));
+      var keyId :- UTF8.Decode(keys[0 as uint32].keyProviderInfo).MapFailure(e => E(e));
       Success(Some(keyId))
     else
       //= specification/searchable-encryption/search-config.md#get-beacon-key-after-encrypt
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy
index 376c92d95..dca21dff9 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy
@@ -34,18 +34,6 @@ module PutItemTransform {
               //# specifically Expected and ConditionalOperator MUST NOT be set.
               && NoMap(input.sdkInput.Expected) && input.sdkInput.ConditionalOperator.None?
 
-              // && var oldHistory := old(tableConfig.itemEncryptor.History.EncryptItem);
-              // && var newHistory := tableConfig.itemEncryptor.History.EncryptItem;
-              // && |newHistory| == |oldHistory|+1
-              // && Seq.Last(newHistory).output.Success?
-              // && var encryptInput := Seq.Last(newHistory).input;
-              // && var encryptOutput := Seq.Last(newHistory).output.value;
-
-              //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-putitem
-              //= type=implication
-              //# The Item MUST be [writable](ddb-support.md#writable).
-              && IsWriteable(tableConfig, input.sdkInput.Item).Success?
-
               //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-putitem
               //= type=implication
               //# The ConditionExpression MUST be [valid](ddb-support.md#testconditionexpression).
@@ -63,6 +51,8 @@ module PutItemTransform {
     :- Need(NoMap(input.sdkInput.Expected), E("Legacy parameter 'Expected' not supported in PutItem with Encryption."));
     :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in PutItem with Encryption."));
 
+    //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-putitem
+    //# The Item MUST be [writable](ddb-support.md#writable).
     var _ :- IsWriteable(tableConfig, input.sdkInput.Item);
     var _ :- TestConditionExpression(tableConfig,
                                      input.sdkInput.ConditionExpression,
diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy
index 972c51c4c..565f5550c 100644
--- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy
@@ -25,6 +25,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
   import DDBE = AwsCryptographyDbEncryptionSdkDynamoDbTypes
   import StandardLibrary.String
   import StructuredEncryptionHeader
+  import opened StandardLibrary.MemoryMath
 
   datatype Config = Config(
     nameonly version : StructuredEncryptionHeader.Version,
@@ -187,9 +188,9 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     //# If the Version Number is not 1 or 2, the operation MUST return an error.
     ensures ((header[0] != 1) && (header[0] != 2)) ==> ret.Failure?
   {
-    if header[0] == 2 then
+    if header[0 as uint32] == 2 then
       MakeEncryptionContextV2(config, item)
-    else if header[0] == 1 then
+    else if header[0 as uint32] == 1 then
       MakeEncryptionContextV1(config, item)
     else
       Failure(E("Header attribute has unexpected version number"))
@@ -251,7 +252,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
               SORT_NAME !in ret.value
   {
     UTF8.EncodeAsciiUnique();
-    :- Need(config.partitionKeyName in item, DDBError("Partition key " + config.partitionKeyName + " not found in Item to be encrypted or decrypted"));
+    :- FNeed(config.partitionKeyName in item, () => DDBError("Partition key " + config.partitionKeyName + " not found in Item to be encrypted or decrypted"));
     var logicalTableName : ValidUTF8Bytes :- DDBEncode(config.logicalTableName);
     var partitionName : ValidUTF8Bytes :- DDBEncode(config.partitionKeyName);
     var partitionKeyName : ValidUTF8Bytes :- EncodeName(config.partitionKeyName);
@@ -654,7 +655,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
   {
     // We happen to order these values, but this ordering MUST NOT be relied upon.
     var keys := SortedSets.ComputeSetToOrderedSequence2(item.Keys, CharLess);
-    if |keys| == 0 then
+    SequenceIsSafeBecauseItIsInMemory(keys);
+    if |keys| as uint64 == 0 then
       "item is empty"
     else
       Join(keys, " ")
@@ -693,10 +695,11 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
                  && actions[k] == CSE.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
                  && k !in item;
     var missing := SortedSets.ComputeSetToOrderedSequence2(s, CharLess);
-    if |missing| == 0 then
+    SequenceIsSafeBecauseItIsInMemory(missing);
+    if |missing| as uint64 == 0 then
       "No missing SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT attributes."
-    else if |missing| == 1 then
-      "Attribute " + missing[0] + " was configured with SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT but was not present in item to be encrypted."
+    else if |missing| as uint64 == 1 then
+      "Attribute " + missing[0 as uint32] + " was configured with SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT but was not present in item to be encrypted."
     else
       "These attributes were configured with SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT but were not present in item to be encrypted."
       + Join(missing, ",")
@@ -1076,7 +1079,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     var header := input.encryptedItem[SE.HeaderField];
     :- Need(header.B?, E("Header field, \"aws_dbe_head\", not binary"));
     assert header.B?;
-    :- Need(0 < |header.B|, E("Unexpected empty header field."));
+    SequenceIsSafeBecauseItIsInMemory(header.B);
+    :- Need(0 < |header.B| as uint64, E("Unexpected empty header field."));
     var context :- MakeEncryptionContextForDecrypt(config, header.B, encryptedStructure);
     var authenticateSchema := ConfigToAuthenticateSchema(config, encryptedStructure);
 
diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
index 56e03b1f0..823e0bcff 100644
--- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
@@ -8,7 +8,7 @@ module DynamoDbItemEncryptorUtil {
   import opened Wrappers
   import opened StandardLibrary
   import opened StandardLibrary.UInt
-  import opened MemoryMath
+  import opened StandardLibrary.MemoryMath
 
   import UTF8
   import MPL = AwsCryptographyMaterialProvidersTypes
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy
index 31f183c68..666b6bb09 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy
@@ -13,7 +13,7 @@ include "Canonize.dfy"
 module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines AbstractAwsCryptographyDbEncryptionSdkStructuredEncryptionOperations {
   import opened StructuredEncryptionUtil
   import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
-  import opened MemoryMath
+  import opened StandardLibrary.MemoryMath
 
   import Base64
   import CMP = AwsCryptographyMaterialProvidersTypes
@@ -141,7 +141,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
   } by method {
     reveal SumValueSize();
     var sum : uint64 := 0;
-    for i := |fields| downto 0
+    SequenceIsSafeBecauseItIsInMemory(fields);
+    for i : uint64 := |fields| as uint64 downto 0
       invariant sum == SumValueSize(fields[i..])
     {
       if fields[i].action == ENCRYPT_AND_SIGN {
@@ -174,8 +175,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     cmm : CMP.ICryptographicMaterialsManager,
     encryptionContext : Option<CMP.EncryptionContext>,
     algorithmSuiteId: Option<CMP.DBEAlgorithmSuiteId>,
-    encryptedTerminalDataNum : nat,
-    totalEncryptedTerminalValuesSize : nat
+    encryptedTerminalDataNum : uint64,
+    totalEncryptedTerminalValuesSize : uint64
   )
     returns (ret : Result<CMP.EncryptionMaterials, Error>)
     ensures ret.Success? ==>
@@ -216,16 +217,16 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
               // - `totalEncryptedTerminalValuesSize` is the sum of the length of all [Terminal Values](./structures.md#terminal-value)
               //   in the [input Structured Data](#structured-data) being encrypted,
               //   as defined by the [input Crypto Schema](#crypto-schema).
-              && var maxLength :=  encryptedTerminalDataNum * 2 + totalEncryptedTerminalValuesSize;
-              && maxLength < INT64_MAX_LIMIT
+              && var maxLength : uint64 :=  Add3(encryptedTerminalDataNum, encryptedTerminalDataNum, totalEncryptedTerminalValuesSize);
+              && maxLength as nat < INT64_MAX_LIMIT
               && (getEncIn.maxPlaintextLength == Some(maxLength as int64))
 
     modifies cmm.Modifies
     requires cmm.ValidState()
     ensures cmm.ValidState()
   {
-    var maxLength :=  encryptedTerminalDataNum * 2 + totalEncryptedTerminalValuesSize;
-    :- Need(maxLength < INT64_MAX_LIMIT, E("Encrypted Size too long."));
+    var maxLength : uint64 :=  Add3(encryptedTerminalDataNum, encryptedTerminalDataNum, totalEncryptedTerminalValuesSize);
+    :- Need(maxLength < INT64_MAX_LIMIT as uint64, E("Encrypted Size too long."));
 
     var algId := GetAlgorithmSuiteId(algorithmSuiteId);
 
@@ -360,8 +361,9 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
   method {:vcs_split_on_every_assert} GetV2EncryptionContext2(fields : CryptoList)
     returns (output : Result<CMP.EncryptionContext, Error>)
   {
+    SequenceIsSafeBecauseItIsInMemory(fields);
     var fieldMap : map<ValidUTF8Bytes, Path> := map[];
-    for i := 0 to |fields|
+    for i : uint64 := 0 to |fields| as uint64
     {
       //= specification/structured-encryption/encrypt-path-structure.md#encryption-context-naming
       //# When a key-value pair is added to the encryption context,
@@ -401,10 +403,11 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     //# - 'N' if the attribute was of type Number
     //# - 'L' if the attribute was of type Null or Boolean
     //# - 'B' otherwise
-    for i := 0 to |keys|
+    SequenceIsSafeBecauseItIsInMemory(keys);
+    for i : uint64 := 0 to |keys| as uint64
       invariant forall j | 0 <= j < i :: keys[j] in newContext
       invariant forall k <- newContext :: k in keys[..i]
-      invariant |legend| == |newContext| == i
+      invariant |legend| == |newContext| == i as nat
     {
       assert keys[i] !in newContext by {
         reveal Seq.HasNoDuplicates();
@@ -429,8 +432,9 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
         attrStr := attr.value;
       } else if attr.typeId == BOOLEAN {
         legendChar := LEGEND_LITERAL;
-        :- Need(|attr.value| == 1, E("Internal Error : boolean was not of length 1."));
-        attrStr := if attr.value[0] == 0 then FALSE_UTF8 else TRUE_UTF8;
+        SequenceIsSafeBecauseItIsInMemory(attr.value);
+        :- Need(|attr.value| as uint64 == 1, E("Internal Error : boolean was not of length 1."));
+        attrStr := if attr.value[0 as uint32] == 0 then FALSE_UTF8 else TRUE_UTF8;
       } else {
         legendChar := LEGEND_BINARY;
         attrStr := EncodeTerminal(attr);
@@ -619,9 +623,6 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
       EncryptStructureOutputHasSinglePaths(cryptoMap, pathOutput.encryptedStructure);
     }
 
-    // This should be provable, but I'm not smart enough
-    :- Need(forall k <- pathOutput.encryptedStructure :: |k.key| == 1, E("Internal Error"));
-
     //= specification/structured-encryption/encrypt-structure.md#behavior
     //= type=implication
     //# The output [Crypto List](encrypt-path-structure.md#crypto-list) produced by [Encrypt Path Structure](encrypt-path-structure.md)
@@ -788,7 +789,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     if exists x <- input.plaintextStructure :: x.action == SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT {
       assume {:axiom} input.cmm.Modifies !! {config.materialProviders.History};
       var newEncryptionContext :- GetV2EncryptionContext(input.plaintextStructure);
-      if |newEncryptionContext| != 0 {
+      MapIsSafeBecauseItIsInMemory(newEncryptionContext);
+      if |newEncryptionContext| as uint64 != 0 {
         //= specification/structured-encryption/encrypt-path-structure.md#create-new-encryption-context-and-cmm
         //# An error MUST be returned if any of the entries added to the encryption context in this step
         //# have the same key as any entry already in the encryption context.
@@ -822,8 +824,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
       cmm,
       Some(encryptionContext),
       input.algorithmSuiteId,
-      CountEncrypted(canonData) as nat,
-      SumValueSize(canonData) as nat);
+      CountEncrypted(canonData),
+      SumValueSize(canonData));
 
     var key : Key := mat.plaintextDataKey.value;
     var alg := mat.algorithmSuite;
@@ -835,7 +837,7 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     //= specification/structured-encryption/encrypt-path-structure.md#calculate-intermediate-encrypted-structured-data
     //# The process used to generate this identifier MUST use a good source of randomness
     //# to make the chance of duplicate identifiers negligible.
-    var randBytes := Random.GenerateBytes(MSGID_LEN as int32);
+    var randBytes := Random.GenerateBytes(MSGID_LEN64 as int32);
     var msgID :- randBytes.MapFailure(e => Error.AwsCryptographyPrimitives(e));
     var head :- Header.Create(input.tableName, canonData, msgID, mat);
     //= specification/structured-encryption/header.md#commit-key
@@ -851,7 +853,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     //# The Header Field Value MUST be the full serialized [header](header.md) with commitment.
     var headerAttribute := ValueToData(headerSerialized, BYTES_TYPE_ID);
 
-    :- Need(|canonData| < (UINT32_LIMIT / 3), E("Too many encrypted fields"));
+    SequenceIsSafeBecauseItIsInMemory(canonData);
+    :- Need(|canonData| as uint64 < Crypt.ONE_THIRD_MAX_INT as uint64, E("Too many encrypted fields"));
     // input canonData has all input fields, none encrypted
     // output canonData has all input fields, some encrypted
     var encryptedItems : CanonCryptoList :- Crypt.Encrypt(config.primitives, alg, key, head, canonData, input.tableName, input.plaintextStructure);
@@ -892,18 +895,19 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
     : string
     requires forall k <- inputFields :: k in inputContext
   {
-    if |inputFields| == 0 then
+    SequenceIsSafeBecauseItIsInMemory(inputFields);
+    if |inputFields| as uint64 == 0 then
       ""
     else
-      var key := inputFields[0];
+      var key := inputFields[0 as uint32];
       if key in headContext && headContext[key] != inputContext[key] then
         var keyStr := SafeDecode(key);
         var headStr := SafeDecode(headContext[key]);
         var inputStr := SafeDecode(inputContext[key]);
         var msg := "input context for " + keyStr + " was " + inputStr + " but stored context had " + headStr + "\n";
-        msg + DescribeMismatch(inputFields[1..], inputContext, headContext)
+        msg + DescribeMismatch(inputFields[1 as uint32..], inputContext, headContext)
       else
-        DescribeMismatch(inputFields[1..], inputContext, headContext)
+        DescribeMismatch(inputFields[1 as uint32..], inputContext, headContext)
   }
 
   function method DetectMismatch(inputContext : CMP.EncryptionContext, headContext : CMP.EncryptionContext)
@@ -911,7 +915,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
   {
     var inputFields := SortedSets.ComputeSetToOrderedSequence2(inputContext.Keys, ByteLess);
     var str := DescribeMismatch(inputFields, inputContext, headContext);
-    if |str| == 0 then
+    SequenceIsSafeBecauseItIsInMemory(str);
+    if |str| as uint64 == 0 then
       Pass
     else
       Fail(E("Encryption Context Mismatch\n" + str))
@@ -1143,7 +1148,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
       //# [Terminal Data](./structures.md#terminal-data)
       //# in the input record, plus the Legend.
       var newEncryptionContext :- GetV2EncryptionContext(UnCanon(canonData));
-      if |newEncryptionContext| != 0 {
+      MapIsSafeBecauseItIsInMemory(newEncryptionContext);
+      if |newEncryptionContext| as uint64 != 0 {
         //= specification/structured-encryption/decrypt-path-structure.md#create-new-encryption-context-and-cmm
         //# An error MUST be returned if any of the entries added to the encryption context in this step
         //# have the same key as any entry already in the encryption context.
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
index fdd117d26..8a2531579 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Canonize.dfy
@@ -11,7 +11,7 @@ module {:options "/functionSyntax:4" } Canonize {
   import opened Wrappers
   import opened StandardLibrary
   import opened StandardLibrary.UInt
-  import opened MemoryMath
+  import opened StandardLibrary.MemoryMath
   import Header = StructuredEncryptionHeader
   import Paths = StructuredEncryptionPaths
   import SortCanon
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy
index 54609b0ec..fc35fd511 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Crypt.dfy
@@ -13,6 +13,7 @@ module StructuredEncryptionCrypt {
   import opened Wrappers
   import opened StandardLibrary
   import opened StandardLibrary.UInt
+  import opened StandardLibrary.MemoryMath
   import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import opened StructuredEncryptionUtil
   import opened DafnyLibraries
@@ -29,6 +30,8 @@ module StructuredEncryptionCrypt {
     // import Relations
   import opened Canonize
 
+  const ONE_THIRD_MAX_INT : uint32 := 1431655765
+
   function method FieldKey(HKDFOutput : Bytes, offset : uint32)
     : (ret : Result<Bytes, Error>)
     requires |HKDFOutput| == KeySize
@@ -38,14 +41,14 @@ module StructuredEncryptionCrypt {
               //# The `FieldKey` for a given key and offset MUST be the first 44 bytes
               //# of the aes256ctr_stream
               //# of the `FieldRootKey` and the `FieldKeyNonce` of three times the given offset.
-              && offset as nat * 3 < UINT32_LIMIT
+              && offset < ONE_THIRD_MAX_INT
               && |ret.value| == KeySize+NonceSize
               && |ret.value| == 44
               && AesKdfCtr.Stream(FieldKeyNonce(offset * 3), HKDFOutput, (KeySize+NonceSize) as uint32).Success?
               && ret.value == AesKdfCtr.Stream(FieldKeyNonce(offset * 3), HKDFOutput, (KeySize+NonceSize) as uint32).value
   {
-    :- Need(offset as nat * 3 < UINT32_LIMIT, E("Too many encrypted fields."));
-    var keyR := AesKdfCtr.Stream(FieldKeyNonce(offset * 3), HKDFOutput, (KeySize+NonceSize) as uint32);
+    :- Need(offset < ONE_THIRD_MAX_INT, E("Too many encrypted fields."));
+    var keyR := AesKdfCtr.Stream(FieldKeyNonce(offset * 3), HKDFOutput, (KeySize64+NonceSize64) as uint32);
     keyR.MapFailure(e => AwsCryptographyPrimitives(e))
   }
 
@@ -71,7 +74,7 @@ module StructuredEncryptionCrypt {
             + UInt32ToSeq(offset)
   {
     AwsDbeField
-    + [(KeySize+NonceSize) as uint8] // length
+    + [(KeySize64+NonceSize64) as uint8] // length
     + UInt32ToSeq(offset)
   }
 
@@ -395,10 +398,11 @@ module StructuredEncryptionCrypt {
   {
     var result : CanonCryptoList := [];
     var pos : uint32 := 0;
-    :- Need(|data| < UINT32_LIMIT, E("Too many fields."));
-    for i := 0 to |data|
+    SequenceIsSafeBecauseItIsInMemory(data);
+    :- Need(|data| as uint64 < UINT32_LIMIT as uint64, E("Too many fields."));
+    for i : uint64 := 0 to |data| as uint64
       invariant pos <= (i as uint32)
-      invariant |result| == i
+      invariant |result| == i as nat
       invariant forall x | 0 <= x < |result| :: Updated(data[x], result[x], mode)
     {
       if data[i].action == ENCRYPT_AND_SIGN {
@@ -481,10 +485,10 @@ module StructuredEncryptionCrypt {
     var fieldKey :- FieldKey(fieldRootKey, offset);
     //= specification/structured-encryption/encrypt-path-structure.md#calculate-cipherkey-and-nonce
     //# The `Cipherkey` MUST be the first 32 bytes of the `FieldKey`
-    var cipherkey : Key := fieldKey[0..KeySize];
+    var cipherkey : Key := fieldKey[..KeySize64];
     //= specification/structured-encryption/encrypt-path-structure.md#calculate-cipherkey-and-nonce
     //# The `Nonce` MUST be the remaining 12 bytes of the `FieldKey`
-    var nonce : Nonce := fieldKey[KeySize..];
+    var nonce : Nonce := fieldKey[KeySize64..];
     var value := data.value;
 
     //= specification/structured-encryption/encrypt-path-structure.md#encrypted-terminal-value
@@ -506,7 +510,7 @@ module StructuredEncryptionCrypt {
 
     var encOutR := client.AESEncrypt(encInput);
     var encOut :- encOutR.MapFailure(e => AwsCryptographyPrimitives(e));
-    :- Need (|encOut.authTag| == AuthTagSize, E("Auth Tag Wrong Size."));
+    :- Need (|encOut.authTag| as uint64 == AuthTagSize64, E("Auth Tag Wrong Size."));
     return Success(ValueToData(data.typeId + encOut.cipherText + encOut.authTag, BYTES_TYPE_ID));
   }
 
@@ -534,11 +538,11 @@ module StructuredEncryptionCrypt {
     ensures client.ValidState()
   {
     var dataKey :- FieldKey(fieldRootKey, offset);
-    var encryptionKey : Key := dataKey[0..KeySize];
-    var nonce : Nonce := dataKey[KeySize..];
+    var encryptionKey : Key := dataKey[..KeySize64];
+    var nonce : Nonce := dataKey[KeySize64..];
     var value := data.value;
-
-    :- Need((AuthTagSize+2) <= |value|, E("cipherTxt too short."));
+    SequenceIsSafeBecauseItIsInMemory(value);
+    :- Need((AuthTagSize64+2) <= |value| as uint64, E("cipherTxt too short."));
 
     //= specification/structured-encryption/decrypt-path-structure.md#terminal-data-decryption
     //# The input [Terminal Value](./structures.md#terminal-value) MUST be deserialized as follows:
@@ -560,13 +564,13 @@ module StructuredEncryptionCrypt {
       encAlg := alg.encrypt.AES_GCM,
       iv := nonce,
       key := encryptionKey,
-      cipherTxt := value[TYPEID_LEN..|value| - AuthTagSize],
+      cipherTxt := value[TYPEID_LEN64..|value| as uint64- AuthTagSize64],
       aad := path,
-      authTag := value[|value|-AuthTagSize..]
+      authTag := value[|value| as uint64-AuthTagSize64..]
     );
 
     var decOutR := client.AESDecrypt(decInput);
     var decOut :- decOutR.MapFailure(e => AwsCryptographyPrimitives(e));
-    return Success(ValueToData(decOut, value[..TYPEID_LEN]));
+    return Success(ValueToData(decOut, value[..TYPEID_LEN64]));
   }
 }
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy
index 8fd348ecb..bbacea03e 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Footer.dfy
@@ -23,7 +23,7 @@ module StructuredEncryptionFooter {
   import opened StandardLibrary.UInt
   import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import opened StructuredEncryptionUtil
-  import opened MemoryMath
+  import opened StandardLibrary.MemoryMath
   import Primitives = AtomicPrimitives
   import Materials
   import Header = StructuredEncryptionHeader
@@ -35,11 +35,10 @@ module StructuredEncryptionFooter {
   import StandardLibrary.String
   import Seq
 
-  const RecipientTagSize := 48
-  //const SignatureSize := 96
-  const SignatureSize := 103
-  type RecipientTag = x : Bytes | |x| == RecipientTagSize witness *
-  type Signature = x : Bytes | |x| == SignatureSize witness *
+  const RecipientTagSize : uint64 := 48
+  const SignatureSize : uint64 := 103
+  type RecipientTag = x : Bytes | |x| == RecipientTagSize as nat witness *
+  type Signature = x : Bytes | |x| == SignatureSize as nat witness *
 
   //= specification/structured-encryption/footer.md#footer-format
   //= type=implication
@@ -93,7 +92,9 @@ module StructuredEncryptionFooter {
       requires client.ValidState()
       ensures client.ValidState()
     {
-      :- Need(|edks| == |tags|, E("There are a different number of recipient tags in the stored header than there are in the decryption materials."));
+      SequenceIsSafeBecauseItIsInMemory(edks);
+      SequenceIsSafeBecauseItIsInMemory(tags);
+      :- Need(|edks| as uint64 == |tags| as uint64, E("There are a different number of recipient tags in the stored header than there are in the decryption materials."));
       var canonicalHash :- CanonHash(data, header, mat.encryptionContext);
 
       var input := Prim.HMacInput (
@@ -104,10 +105,11 @@ module StructuredEncryptionFooter {
       var hashR := client.HMac(input);
       var hash :- hashR.MapFailure(e => AwsCryptographyPrimitives(e));
       // is there any way to get "48" from alg.symmetricSignature.HMAC?
-      :- Need(|hash| == 48, E("Bad hash length"));
+      SequenceIsSafeBecauseItIsInMemory(hash);
+      :- Need(|hash| as uint64 == 48, E("Bad hash length"));
 
       var foundTag := false;
-      for i := 0 to |tags| {
+      for i : uint64 := 0 to |tags| as uint64 {
         //= specification/structured-encryption/footer.md#recipient-tag-verification
         //# Recipient Tag comparisons MUST be constant time operations.
         if ConstantTimeEquals(hash, tags[i]) {
@@ -157,12 +159,14 @@ module StructuredEncryptionFooter {
   function method GetCanonicalType(value : StructuredDataTerminal, isEncrypted : bool)
     : Result<Bytes, Error>
   {
+    SequenceIsSafeBecauseItIsInMemory(value.value);
+    var value_len : uint64 := |value.value| as uint64;
     if isEncrypted then
-      :- Need(2 <= |value.value| && HasUint64Len(value.value), E("Bad length."));
-      Success(UInt64ToSeq((|value.value| - 2) as uint64) + ENCRYPTED)
+      :- Need(2 <= value_len, E("Bad length."));
+      Success(UInt64ToSeq((value_len - 2) as uint64) + ENCRYPTED)
     else
       :- Need(HasUint64Len(value.value), E("Bad length."));
-      Success(UInt64ToSeq((|value.value|) as uint64) + PLAINTEXT + value.typeId)
+      Success(UInt64ToSeq((value_len) as uint64) + PLAINTEXT + value.typeId)
   }
 
   function method GetCanonicalEncryptedField(fieldName : CanonicalPath, value : StructuredDataTerminal)
@@ -186,10 +190,11 @@ module StructuredEncryptionFooter {
                  + ENCRYPTED
                  + value.value // this is 2 bytes of unencrypted type, followed by encrypted value
   {
-    :- Need(2 <= |value.value| && HasUint64Len(value.value), E("Bad length."));
+    SequenceIsSafeBecauseItIsInMemory(value.value);
+    :- Need(2 <= |value.value| as uint64, E("Bad length."));
     Success(
       fieldName
-      + UInt64ToSeq((|value.value| - 2) as uint64)
+      + UInt64ToSeq((|value.value| as uint64 - 2) as uint64)
       + ENCRYPTED
       + value.value
     )
@@ -356,8 +361,9 @@ module StructuredEncryptionFooter {
   {
     var canonicalHash :- CanonHash(data, header, mat.encryptionContext);
     var tags : seq<RecipientTag> := [];
-    for i := 0 to |mat.encryptedDataKeys|
-      invariant |tags| == i
+    SequenceIsSafeBecauseItIsInMemory(mat.encryptedDataKeys);
+    for i : uint64 := 0 to |mat.encryptedDataKeys| as uint64
+      invariant |tags| == i as nat
     {
       //= specification/structured-encryption/footer.md#recipient-tags
       //# the Recipient Tag MUST be MUST be calculated over the [Canonical Hash](#canonical-hash)
@@ -374,7 +380,8 @@ module StructuredEncryptionFooter {
       var hashR := client.HMac(input);
       var hash :- hashR.MapFailure(e => AwsCryptographyPrimitives(e));
       // is there any way to get "48" from alg.symmetricSignature.HMAC?
-      :- Need(|hash| == 48, E("Bad hash length"));
+      SequenceIsSafeBecauseItIsInMemory(hash);
+      :- Need(|hash| as uint64 == 48, E("Bad hash length"));
 
       //= specification/structured-encryption/footer.md#recipient-tags
       //# the HMAC values MUST have the same order as the
@@ -398,8 +405,8 @@ module StructuredEncryptionFooter {
       );
       var sigR := client.ECDSASign(verInput);
       var sig :- sigR.MapFailure(e => AwsCryptographyPrimitives(e));
-      //assert |sig| == SignatureSize;
-      :- Need(|sig| == SignatureSize, E("Signature is " + String.Base10Int2String(|sig|) + " bytes, should have been " + String.Base10Int2String(SignatureSize) + " bytes."));
+      SequenceIsSafeBecauseItIsInMemory(sig);
+      :- Need(|sig| as uint64 == SignatureSize, E("Signature is " + String.Base10Int2String(|sig|) + " bytes, should have been " + String.Base10Int2String(SignatureSize as nat) + " bytes."));
       return Success(Footer(tags, Some(sig)));
     } else {
       return Success(Footer(tags, None));
@@ -435,24 +442,27 @@ module StructuredEncryptionFooter {
 
   function method GatherTags(data : Bytes)
     : seq<RecipientTag>
-    requires |data| % RecipientTagSize == 0
+    requires |data| % RecipientTagSize as nat == 0
   {
-    if |data| == 0 then
+    SequenceIsSafeBecauseItIsInMemory(data);
+    if |data| as uint64 == 0 then
       []
     else
-      [data[0..RecipientTagSize]] + GatherTags(data[RecipientTagSize..])
+      [data[0 as uint32..RecipientTagSize]] + GatherTags(data[RecipientTagSize..])
   }
 
   function method DeserializeFooter(data : Bytes, hasSig : bool)
     : Result<Footer, Error>
   {
+    SequenceIsSafeBecauseItIsInMemory(data);
+    var data_len : uint64 := |data| as uint64;
     if hasSig then
-      :- Need((|data| - SignatureSize)  % RecipientTagSize == 0, E("Mangled signed footer has strange size"));
-      :- Need(|data| >= RecipientTagSize + SignatureSize, E("Footer too short."));
-      Success(Footer(GatherTags(data[..|data|-SignatureSize]), Some(data[|data|-SignatureSize..])))
+      :- Need(data_len >= RecipientTagSize + SignatureSize, E("Footer too short."));
+      :- Need((data_len - SignatureSize) % RecipientTagSize == 0, E("Mangled signed footer has strange size"));
+      Success(Footer(GatherTags(data[..data_len-SignatureSize]), Some(data[data_len-SignatureSize..])))
     else
-      :- Need(|data| % RecipientTagSize == 0, E("Mangled unsigned footer has strange size"));
-      :- Need(|data| >= RecipientTagSize, E("Footer too short."));
+      :- Need(data_len % RecipientTagSize == 0, E("Mangled unsigned footer has strange size"));
+      :- Need(data_len >= RecipientTagSize, E("Footer too short."));
       Success(Footer(GatherTags(data), None))
   }
 }
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
index e48bc3d89..e9d0061d7 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy
@@ -13,8 +13,7 @@ module StructuredEncryptionHeader {
   import opened StandardLibrary.UInt
   import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import opened StructuredEncryptionUtil
-  import opened MemoryMath
-
+  import opened StandardLibrary.MemoryMath
   import CMP = AwsCryptographyMaterialProvidersTypes
   import Prim = AwsCryptographyPrimitivesTypes
   import SortedSets
@@ -26,11 +25,16 @@ module StructuredEncryptionHeader {
   import Functions
   import MaterialProviders
 
-  const VERSION_LEN := 1
-  const FLAVOR_LEN := 1
-  const COMMITMENT_LEN := 32
-  const PREFIX_LEN := VERSION_LEN + FLAVOR_LEN + MSGID_LEN
-  const UINT8_LIMIT := 256
+  ghost const VERSION_LEN := 1
+  ghost const FLAVOR_LEN := 1
+  ghost const COMMITMENT_LEN := 32
+  ghost const PREFIX_LEN := VERSION_LEN + FLAVOR_LEN + MSGID_LEN
+  const VERSION_LEN64 : uint64 := 1
+  const FLAVOR_LEN64 : uint64 := 1
+  const COMMITMENT_LEN64 : uint64 := 32
+  const PREFIX_LEN64 : uint64 := VERSION_LEN64 + FLAVOR_LEN64 + MSGID_LEN64
+  ghost const UINT8_LIMIT := 256
+  const UINT8_LIMIT64 : uint64 := 256
   const ENCRYPT_AND_SIGN_LEGEND : uint8 := 0x65
   const SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT_LEGEND : uint8 := 0x63
   const SIGN_ONLY_LEGEND : uint8 := 0x73
@@ -101,15 +105,29 @@ module StructuredEncryptionHeader {
   }
 
   predicate method ValidEncryptionContext(x : CMP.EncryptionContext) {
-    && |x| < UINT16_LIMIT
-    && (forall k <- x :: |k| < UINT16_LIMIT && |x[k]| < UINT16_LIMIT)
+    MapIsSafeBecauseItIsInMemory(x);
+    assert forall k <-x :: HasUint64Len(k) by {
+      forall k <- x {
+        SequenceIsSafeBecauseItIsInMemory(k);
+      }
+    }
+    assert forall k <-x :: HasUint64Len(x[k]) by {
+      forall k <- x {
+        SequenceIsSafeBecauseItIsInMemory(x[k]);
+      }
+    }
+    && |x| as uint64 < UINT16_LIMIT as uint64
+    && (forall k <- x :: |k| as uint64 < UINT16_LIMIT as uint64 && |x[k]| as uint64 < UINT16_LIMIT as uint64)
   }
 
   predicate method ValidEncryptedDataKey(x : CMP.EncryptedDataKey)
   {
-    && |x.keyProviderId| < UINT16_LIMIT
-    && |x.keyProviderInfo| < UINT16_LIMIT
-    && |x.ciphertext| < UINT16_LIMIT
+    SequenceIsSafeBecauseItIsInMemory(x.keyProviderId);
+    SequenceIsSafeBecauseItIsInMemory(x.keyProviderInfo);
+    SequenceIsSafeBecauseItIsInMemory(x.ciphertext);
+    && |x.keyProviderId| as uint64 < UINT16_LIMIT as uint64
+    && |x.keyProviderInfo| as uint64 < UINT16_LIMIT as uint64
+    && |x.ciphertext| as uint64 < UINT16_LIMIT as uint64
   }
 
   // header without commitment
@@ -174,9 +192,10 @@ module StructuredEncryptionHeader {
                 //# Header commitment comparisons MUST be constant time operations.
                 && ConstantTimeEquals(storedCommitment, calcCommitment)
     {
-      :- Need(COMMITMENT_LEN < |data|, E("Serialized header too short"));
-      var storedCommitment := data[|data|-COMMITMENT_LEN..];
-      var calcCommitment :- CalculateHeaderCommitment(client, alg, commitKey, data[..|data|-COMMITMENT_LEN]);
+      SequenceIsSafeBecauseItIsInMemory(data);
+      :- Need(COMMITMENT_LEN64 < |data| as uint64, E("Serialized header too short"));
+      var storedCommitment := data[|data| as uint64-COMMITMENT_LEN64..];
+      var calcCommitment :- CalculateHeaderCommitment(client, alg, commitKey, data[..|data|as uint64-COMMITMENT_LEN64]);
       :- Need(ConstantTimeEquals(storedCommitment, calcCommitment), E("Key commitment mismatch."));
       Success(true)
     }
@@ -243,14 +262,17 @@ module StructuredEncryptionHeader {
     //# the Version MUST be 0x02; otherwise, Version MUST be 0x01.
     ensures ret.Success? ==> |schema| < UINT32_LIMIT && ret.value.version == VersionFromSchema(schema)
   {
-    :- Need(|schema| < UINT32_LIMIT, E("Unexpected large schema"));
+    SequenceIsSafeBecauseItIsInMemory(schema);
+    SequenceIsSafeBecauseItIsInMemory(mat.encryptedDataKeys);
+    SequenceIsSafeBecauseItIsInMemory(mat.algorithmSuite.binaryId);
+    :- Need(|schema| as uint64 < UINT32_LIMIT as uint64, E("Unexpected large schema"));
     :- Need(ValidEncryptionContext(mat.encryptionContext), E("Invalid Encryption Context"));
-    :- Need(0 < |mat.encryptedDataKeys|, E("There must be at least one data key"));
-    :- Need(|mat.encryptedDataKeys| < UINT8_LIMIT, E("Too many data keys."));
+    :- Need(0 < |mat.encryptedDataKeys| as uint64, E("There must be at least one data key"));
+    :- Need(|mat.encryptedDataKeys| as uint64 < UINT8_LIMIT64, E("Too many data keys."));
     :- Need(forall x | x in mat.encryptedDataKeys :: ValidEncryptedDataKey(x), E("Invalid Data Key"));
-    :- Need(|mat.algorithmSuite.binaryId| == 2, E("Invalid Algorithm Suite Binary ID"));
-    :- Need(mat.algorithmSuite.binaryId[0] == DbeAlgorithmFamily, E("Algorithm Suite not suitable for structured encryption."));
-    :- Need(ValidFlavor(mat.algorithmSuite.binaryId[1]), E("Algorithm Suite has unexpected flavor."));
+    :- Need(|mat.algorithmSuite.binaryId| as uint64 == 2, E("Invalid Algorithm Suite Binary ID"));
+    :- Need(mat.algorithmSuite.binaryId[0 as uint32] == DbeAlgorithmFamily, E("Algorithm Suite not suitable for structured encryption."));
+    :- Need(ValidFlavor(mat.algorithmSuite.binaryId[1 as uint32]), E("Algorithm Suite has unexpected flavor."));
     var legend :- MakeLegend(schema);
 
     //= specification/structured-encryption/encrypt-path-structure.md#header-field
@@ -263,7 +285,7 @@ module StructuredEncryptionHeader {
     :- Need(ValidEncryptionContext(storedEC), E("Invalid Encryption Context"));
     Success(PartialHeader(
               version := VersionFromSchema(schema),
-              flavor := mat.algorithmSuite.binaryId[1],
+              flavor := mat.algorithmSuite.binaryId[1 as uint32],
               msgID := msgID,
               legend := legend,
               encContext := storedEC,
@@ -277,9 +299,9 @@ module StructuredEncryptionHeader {
     ensures ret.Success? ==>
               && PREFIX_LEN <= |data|
               && var v := ret.value;
-              && v.version == data[0]
+              && v.version == data[0 as uint32]
               && ValidVersion(v.version)
-              && v.flavor == data[1]
+              && v.flavor == data[1 as uint32]
               && ValidFlavor(v.flavor)
               && v.msgID == data[VERSION_LEN+FLAVOR_LEN..PREFIX_LEN]
               && var legendData := data[PREFIX_LEN..];
@@ -291,13 +313,14 @@ module StructuredEncryptionHeader {
               && var contextAndLen := GetContext(contextData).value;
               && v.encContext == contextAndLen.0
   {
-    :- Need(PREFIX_LEN <= |data|, E("Serialized PartialHeader too short."));
-    var version := data[0];
+    SequenceIsSafeBecauseItIsInMemory(data);
+    :- Need(PREFIX_LEN64 <= |data| as uint64, E("Serialized PartialHeader too short."));
+    var version := data[0 as uint32];
     :- Need(ValidVersion(version), E("Invalid Version Number"));
-    var flavor := data[1];
+    var flavor := data[1 as uint32];
     :- Need(ValidFlavor(flavor), E("Invalid Flavor"));
-    var msgID := data[2..PREFIX_LEN];
-    var legendData := data[PREFIX_LEN..];
+    var msgID := data[2 as uint32..PREFIX_LEN64];
+    var legendData := data[PREFIX_LEN64..];
 
     var legendAndLen :- GetLegend(legendData);
     var legend := legendAndLen.0;
@@ -311,8 +334,9 @@ module StructuredEncryptionHeader {
     var dataKeys := keysAndLen.0;
     var trailingData := keysData[keysAndLen.1..];
 
-    :- Need(|trailingData| >= COMMITMENT_LEN, E("Invalid header serialization: unexpected end of data."));
-    :- Need(|trailingData| <= COMMITMENT_LEN, E("Invalid header serialization: unexpected bytes."));
+    SequenceIsSafeBecauseItIsInMemory(trailingData);
+    :- Need(|trailingData| as uint64 >= COMMITMENT_LEN64, E("Invalid header serialization: unexpected end of data."));
+    :- Need(|trailingData| as uint64 <= COMMITMENT_LEN64, E("Invalid header serialization: unexpected bytes."));
     assert |trailingData| == COMMITMENT_LEN;
     Success(PartialHeader(
               version := version,
@@ -356,13 +380,14 @@ module StructuredEncryptionHeader {
                  );
     var outputR := client.HMac(input);
     var output :- outputR.MapFailure(e => AwsCryptographyPrimitives(e));
-    if |output| < COMMITMENT_LEN then
+    SequenceIsSafeBecauseItIsInMemory(output);
+    if |output| as uint64 < COMMITMENT_LEN64 then
       Failure(E("HMAC did not produce enough bits"))
     else
-      Success(output[..COMMITMENT_LEN])
+      Success(output[..COMMITMENT_LEN64])
   }
 
-  function method ToUInt16(x : nat)
+  function ToUInt16(x : nat)
     : (ret : Result<uint16, Error>)
     ensures x < UINT16_LIMIT ==> ret.Success?
   {
@@ -412,7 +437,7 @@ module StructuredEncryptionHeader {
     if |data| as uint64 == pos then
       Success(serialized)
     else if IsAuthAttr(data[pos].action) then
-      :- Need((|serialized| + 1) < UINT16_LIMIT, E("Legend Too Long."));
+      :- Need((|serialized| as uint64 + 1) < UINT16_LIMIT as uint64, E("Legend Too Long."));
       var legendChar := GetActionLegend(data[pos].action);
       MakeLegend2(data, pos+1, serialized + [legendChar])
     else
@@ -496,7 +521,7 @@ module StructuredEncryptionHeader {
     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];
+    var legend := data[2 as uint32..size];
     :- Need(forall x <- legend :: ValidLegendByte(x), E("Invalid byte in stored legend"));
     Success((legend, size))
   }
@@ -590,7 +615,8 @@ module StructuredEncryptionHeader {
     if count == 0 then
       Success(deserialized)
     else
-      :- Need(|deserialized.0| + 1  < UINT16_LIMIT, E("Too much context"));
+      :- Need(|deserialized.0| as uint64 + 1  < UINT16_LIMIT as uint64, E("Too much context"));
+
       var kv :- GetOneKVPair(data, deserialized.1 as uint64);
       //= specification/structured-encryption/header.md#key-value-pair-entries
       //# This sequence MUST NOT contain duplicate entries.
@@ -685,7 +711,7 @@ module StructuredEncryptionHeader {
               && 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)]
+              && SerializeOneDataKey(ret.value.0) == data[pos..pos + ret.value.1]
   {
     SequenceIsSafeBecauseItIsInMemory(data);
     var data_size : uint64 := |data| as uint64;
@@ -701,15 +727,22 @@ module StructuredEncryptionHeader {
     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];
+    var provInfo := data[pos+part1Size+2..pos+part2Size];
 
     :- 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 cipher := data[pos+part2Size+2..pos+part3Size];
 
     var edk : CMPEncryptedDataKey := CMP.EncryptedDataKey(keyProviderId := provId, keyProviderInfo := provInfo, ciphertext := cipher);
+
+    assert provIdSize as nat == |edk.keyProviderId|;
+    assert data[pos..pos+2] == UInt16ToSeq(provIdSize as uint16);
+    assert data[pos+2..pos+2+provIdSize] == edk.keyProviderId;
+    assert provInfoSize as nat == |edk.keyProviderInfo|;
+    assert data[pos+part1Size..pos+part1Size+2] == UInt16ToSeq(provInfoSize as uint16);
+    assert SerializeOneDataKey(edk) == data[pos..pos + part3Size];
     Success((edk, part3Size))
   }
 
@@ -778,10 +811,11 @@ module StructuredEncryptionHeader {
               && |ret.value.0| == data[0] as nat
               && 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 uint64;
+    SequenceIsSafeBecauseItIsInMemory(data);
+    :- Need(1 <= |data| as uint64, E("Unexpected end of header data."));
+    var count := data[0 as uint32] as uint64;
     var keys :- GetDataKeys2(count, count, data, ([], 1));
-    if |keys.0| == 0 then
+    if |keys.0| as uint64 == 0 then
       Failure(E("At least one Data Key required"))
     else
       Success(keys)
@@ -802,10 +836,10 @@ module StructuredEncryptionHeader {
               && (count > 0 ==> GetOneDataKey(data, deserialized.1 as uint64).Success?)
               && |ret.value.0| == origCount as nat
   {
+
     if count == 0 then
       Success(deserialized)
-    else
-    if |deserialized.0| >= 255 then
+    else if |deserialized.0| as uint64 >= 255 then
       Failure(E("Too Many Data Keys"))
     else
       var edk :- GetOneDataKey(data, deserialized.1 as uint64);
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
index 90be48143..726784f52 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/OptimizedMergeSort.dfy
@@ -8,9 +8,10 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
   import Relations
   import BoundedInts
   import InternalModule = Seq.MergeSort
-  import MemoryMath
+  import opened StandardLibrary.MemoryMath
+  import opened StandardLibrary.UInt
 
-  predicate HasUint64Len<T>(s: seq<T>) {
+  ghost predicate HasUint64Len<T>(s: seq<T>) {
     |s| < BoundedInts.TWO_TO_THE_64
   }
 
@@ -34,7 +35,7 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
     InternalModule.MergeSortBy(s, lessThanOrEq)
   }
   by method {
-    if |s| <= 1 {
+    if |s| as uint64 <= 1 {
       return s;
     } else {
 
@@ -45,13 +46,13 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
       // 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;
+      var left := new T[|s| as uint64](i requires 0 <= i < |s| => s[i as uint64]);
+      var right := new T[|s| as uint64](i requires 0 <= i < |s| => s[i as uint64]);
+      ghost var lo, hi := 0, right.Length;
 
       label BEFORE_WORK:
 
-      var boundedLo: BoundedInts.uint64, boundedHi: BoundedInts.uint64 := 0, right.Length as BoundedInts.uint64;
+      var boundedLo: uint64, boundedHi: uint64 := 0, right.Length as uint64;
       ghost var _ := MergeSortMethod(left, right, lessThanOrEq, boundedLo, boundedHi, Right);
 
       result :=  right[..];
@@ -95,7 +96,7 @@ 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)
   {
-    MemoryMath.SequenceIsSafeBecauseItIsInMemory(s);
+    SequenceIsSafeBecauseItIsInMemory(s);
     MergeSort(s, lessThanOrEq)
   }
 
@@ -111,16 +112,16 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
     left: array<T>,
     right: array<T>,
     lessThanOrEq: (T, T) -> bool,
-    lo: BoundedInts.uint64,
-    hi: BoundedInts.uint64,
+    lo: uint64,
+    hi: uint64,
     where: PlaceResults
   )
     returns (resultPlacement: ResultPlacement)
     requires Relations.TotalOrdering(lessThanOrEq)
     requires left.Length < BoundedInts.TWO_TO_THE_64
     requires right.Length < BoundedInts.TWO_TO_THE_64
-    requires lo < hi <= left.Length as BoundedInts.uint64
-    requires hi <= right.Length as BoundedInts.uint64
+    requires lo < hi <= left.Length as uint64
+    requires hi <= right.Length as uint64
     requires left != right
     // reads left, right
     modifies left, right
@@ -241,16 +242,16 @@ module {:options "-functionSyntax:4"} OptimizedMergeSort {
     nameonly left: array<T>,
     nameonly right: array<T>,
     nameonly lessThanOrEq: (T, T) -> bool,
-    nameonly lo: BoundedInts.uint64,
-    nameonly mid: BoundedInts.uint64,
-    nameonly hi: BoundedInts.uint64
+    nameonly lo: uint64,
+    nameonly mid: uint64,
+    nameonly hi: uint64
   )
     requires Relations.TotalOrdering(lessThanOrEq)
     requires
       && left.Length < BoundedInts.TWO_TO_THE_64
       && right.Length < BoundedInts.TWO_TO_THE_64
-    requires lo <= mid <= hi <= left.Length as BoundedInts.uint64
-    requires  hi <= right.Length as BoundedInts.uint64 && left != right
+    requires lo <= mid <= hi <= left.Length as uint64
+    requires  hi <= right.Length as uint64 && left != right
     // We store "left" in [lo..mid]
     requires Relations.SortedBy(left[lo..mid], lessThanOrEq)
     // We store "right" in [mid..hi]
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy
index 246f001ca..8341db874 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Paths.dfy
@@ -11,6 +11,7 @@ module StructuredEncryptionPaths {
   import opened Wrappers
   import opened StandardLibrary
   import opened StandardLibrary.UInt
+  import opened StandardLibrary.MemoryMath
   import opened StructuredEncryptionUtil
   import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import opened DafnyLibraries
@@ -19,14 +20,14 @@ module StructuredEncryptionPaths {
     | List(pos : uint64)
     | Map(key : GoodString)
 
-  type SelectorList = x : seq<Selector> | HasUint64Len(x)
+  type SelectorList = seq<Selector>
   type TerminalSelector = x : seq<Selector> | ValidTerminalSelector(x) witness *
 
   predicate method ValidTerminalSelector(s : seq<Selector>)
   {
-    && 0 < |s|
-    && HasUint64Len(s)
-    && s[0].Map?
+    SequenceIsSafeBecauseItIsInMemory(s);
+    && 0 < |s| as uint64
+    && s[0 as uint32].Map?
   }
 
   function method StringToUniPath(x : string) : (ret : Path)
@@ -44,32 +45,33 @@ module StructuredEncryptionPaths {
   function method UniPathToString(x : Path) : Result<string, Error>
     requires |x| == 1
   {
-    Success(x[0].member.key)
+    Success(x[0 as uint32].member.key)
   }
 
   predicate method ValidPath(path : Path)
   {
-    && HasUint64Len(path)
-    && forall x <- path :: ValidString(x.member.key)
+    forall x <- path :: ValidString(x.member.key)
   }
 
   function method CanonPath(table : GoodString, path : Path)
     : (ret : CanonicalPath)
     requires ValidPath(path)
-    ensures ret ==
-            //= specification/structured-encryption/header.md#canonical-path
-            //= type=implication
-            //# The canonical path MUST start with the UTF8 encoded table name.
-            UTF8.Encode(table).value
-            //= specification/structured-encryption/header.md#canonical-path
-            //= type=implication
-            //# This MUST be followed by the depth of the Terminal within Structured Data.
-            + UInt64ToSeq(|path| as uint64)
-            //= specification/structured-encryption/header.md#canonical-path
-            //= type=implication
-            //# This MUST be followed by the encoding for each Structured Data in the path, including the Terminal itself.
-            + MakeCanonicalPath(path)
+
+    ensures  HasUint64Len(path) && ret ==
+                                   //= specification/structured-encryption/header.md#canonical-path
+                                   //= type=implication
+                                   //# The canonical path MUST start with the UTF8 encoded table name.
+                                   UTF8.Encode(table).value
+                                   //= specification/structured-encryption/header.md#canonical-path
+                                   //= type=implication
+                                   //# This MUST be followed by the depth of the Terminal within Structured Data.
+                                   + UInt64ToSeq(|path| as uint64)
+                                   //= specification/structured-encryption/header.md#canonical-path
+                                   //= type=implication
+                                   //# This MUST be followed by the encoding for each Structured Data in the path, including the Terminal itself.
+                                   + MakeCanonicalPath(path)
   {
+    SequenceIsSafeBecauseItIsInMemory(path);
     var tableName := UTF8.Encode(table).value;
     var depth := UInt64ToSeq(|path| as uint64);
     var path := MakeCanonicalPath(path);
@@ -123,7 +125,8 @@ module StructuredEncryptionPaths {
       CanonicalPart(path[0]) + MakeCanonicalPath(path[1..])
   } by method {
     var result : CanonicalPath := [];
-    for i := |path| downto 0
+    SequenceIsSafeBecauseItIsInMemory(path);
+    for i : uint64 := |path| as uint64 downto 0
       invariant result == MakeCanonicalPath(path[i..])
     {
       result := CanonicalPart(path[i]) + result;
@@ -154,12 +157,13 @@ module StructuredEncryptionPaths {
   // e.g. ['a.b'] and ['a','b'] both return 'a.b'.
   function method PathToString(path : Path) : string
   {
-    if |path| == 0 then
+    SequenceIsSafeBecauseItIsInMemory(path);
+    if |path| as uint64 == 0 then
       ""
-    else if |path| == 1 then
-      path[0].member.key
+    else if |path| as uint64 == 1 then
+      path[0 as uint32].member.key
     else
-      path[0].member.key + "." + PathToString(path[1..])
+      path[0 as uint32].member.key + "." + PathToString(path[1 as uint32..])
   }
 
   // End code, begin lemmas.
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy
index f4a5fbde2..07956b027 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/SortCanon.dfy
@@ -20,6 +20,7 @@ module SortCanon {
   import opened Wrappers
   import opened StandardLibrary
   import opened StandardLibrary.UInt
+  import opened StandardLibrary.MemoryMath
   import opened Relations
   import opened Seq.MergeSort
   import opened StructuredEncryptionUtil
@@ -156,46 +157,9 @@ module SortCanon {
       && x[0] <= y[0]
       && (x[0] == y[0] ==> Below(x[1..], y[1..]))
   } by method {
-
-    // 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.
-
-    if HasUint64Len(x) && HasUint64Len(y) {
-      return BoundedBelow(x,y);
-    }
-
-    if |x| == 0 {
-      assert Below(x, y);
-      return true;
-    }
-
-    if |y| == 0 {
-      assert !Below(x, y);
-      return false;
-    }
-
-    for i := 0 to |x|
-      invariant i <= |y|
-      // The function on the initial arguments
-      // is equal to function applied to the intermediate arguments.
-      invariant Below(x, y) == Below(x[i..], y[i..])
-    {
-      if |y| <= i {
-        return false;
-      } else if y[i] < x[i] {
-        return false;
-      } else if x[i] < y[i] {
-        return true;
-      } else {
-        assert x[i] == y[i];
-      }
-    }
-
-    return true;
+    SequenceIsSafeBecauseItIsInMemory(x);
+    SequenceIsSafeBecauseItIsInMemory(y);
+    return BoundedBelow(x,y);
   }
 
   predicate BoundedBelow(x: seq64<uint8>, y: seq64<uint8>)
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy
index f71513ff7..e87e0b608 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/src/Util.dfy
@@ -8,7 +8,7 @@ module StructuredEncryptionUtil {
   import opened Wrappers
   import opened StandardLibrary
   import opened StandardLibrary.UInt
-  import opened MemoryMath
+  import opened StandardLibrary.MemoryMath
 
   import UTF8
   import CMP = AwsCryptographyMaterialProvidersTypes
@@ -111,12 +111,16 @@ module StructuredEncryptionUtil {
 
   predicate method CryptoListHasNoDuplicatesFromSet(xs: CryptoList)
   {
-    |CryptoListToSet(xs)| == |xs|
+    SequenceIsSafeBecauseItIsInMemory(xs);
+    SetIsSafeBecauseItIsInMemory(CryptoListToSet(xs));
+    |CryptoListToSet(xs)| as uint64 == |xs| as uint64
   }
 
   predicate method AuthListHasNoDuplicatesFromSet(xs: AuthList)
   {
-    |AuthListToSet(xs)| == |xs|
+    SequenceIsSafeBecauseItIsInMemory(xs);
+    SetIsSafeBecauseItIsInMemory(AuthListToSet(xs));
+    |AuthListToSet(xs)| as uint64 == |xs| as uint64
   }
 
   predicate CryptoListHasNoDuplicates(xs: CryptoList)
@@ -151,17 +155,22 @@ module StructuredEncryptionUtil {
     ensures FooterField == "aws_dbe_foot"
   {}
 
-  const TYPEID_LEN := 2
+  ghost const TYPEID_LEN := 2
+  const TYPEID_LEN64 : uint64 := 2
   const BYTES_TYPE_ID : seq<uint8> := [0xFF, 0xFF]
   lemma BYTES_TYPE_ID_OK()
     ensures |BYTES_TYPE_ID| == TYPEID_LEN
   {}
 
   // Currently, only one set of sizes are supported
-  const KeySize := 32 // 256 bits, for 256-bit AES keys
-  const NonceSize := 12 // 96 bits, per AES-GCM nonces
-  const AuthTagSize := 16
-  const MSGID_LEN := 32
+  ghost const KeySize := 32 // 256 bits, for 256-bit AES keys
+  ghost const NonceSize := 12 // 96 bits, per AES-GCM nonces
+  ghost const AuthTagSize := 16
+  ghost const MSGID_LEN := 32
+  const KeySize64 : uint64 := 32 // 256 bits, for 256-bit AES keys
+  const NonceSize64 : uint64 := 12 // 96 bits, per AES-GCM nonces
+  const AuthTagSize64 : uint64 := 16
+  const MSGID_LEN64 : uint64  := 32
   const DbeAlgorithmFamily : uint8 := 0x67
 
   lemma ValidSuiteSizes(alg : CMP.AlgorithmSuiteInfo)
@@ -330,9 +339,10 @@ module StructuredEncryptionUtil {
   {
     var utf8DecodedVal :- UTF8.Decode(t);
     var base64DecodedVal :- Base64.Decode(utf8DecodedVal);
-    :- Need(|base64DecodedVal| >= 2, "Invalid serialization of DDB Attribute in encryption context.");
-    var typeId := base64DecodedVal[..2];
-    var serializedValue := base64DecodedVal[2..];
+    SequenceIsSafeBecauseItIsInMemory(base64DecodedVal);
+    :- Need(|base64DecodedVal| as uint64 >= 2, "Invalid serialization of DDB Attribute in encryption context.");
+    var typeId := base64DecodedVal[..2 as uint32];
+    var serializedValue := base64DecodedVal[2 as uint32..];
     Success(StructuredDataTerminal(value := serializedValue, typeId := typeId))
   }
 
diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/test/Crypt.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/test/Crypt.dfy
index b7b1895ef..b5f257ac1 100644
--- a/DynamoDbEncryption/dafny/StructuredEncryption/test/Crypt.dfy
+++ b/DynamoDbEncryption/dafny/StructuredEncryption/test/Crypt.dfy
@@ -224,7 +224,7 @@ module TestStructuredEncryptionCrypt {
       expect IsHexString(FieldKeyTestVector[i].input);
       var input := FromHexString(FieldKeyTestVector[i].input);
       expect ToHexString(input) == FieldKeyTestVector[i].input;
-      expect |input| == KeySize;
+      expect |input| == KeySize64 as nat;
       expect FieldKeyTestVector[i].offset as nat * 3 < UINT32_LIMIT;
       var result :- expect FieldKey(input, FieldKeyTestVector[i].offset);
       if ToHexString(result) != FieldKeyTestVector[i].output {
diff --git a/DynamoDbEncryption/runtimes/rust/Cargo.toml b/DynamoDbEncryption/runtimes/rust/Cargo.toml
index a5877c06d..802c0b926 100644
--- a/DynamoDbEncryption/runtimes/rust/Cargo.toml
+++ b/DynamoDbEncryption/runtimes/rust/Cargo.toml
@@ -16,19 +16,19 @@ readme = "README.md"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-aws-config = "1.6.0"
-aws-lc-rs = "1.12.2"
-aws-lc-sys = "0.25.0"
-aws-sdk-dynamodb = "1.69.0"
-aws-sdk-kms = "1.63.0"
-aws-smithy-runtime-api = {version = "1.7.4", features = ["client"] }
-aws-smithy-types = "1.3.0"
-chrono = "0.4.40"
+aws-config = "1.6.2"
+aws-lc-rs = "1.13.0"
+aws-lc-sys = "0.28.2"
+aws-sdk-dynamodb = "1.73.0"
+aws-sdk-kms = "1.67.0"
+aws-smithy-runtime-api = {version = "1.8.0", features = ["client"] }
+aws-smithy-types = "1.3.1"
+chrono = "0.4.41"
 cpu-time = "1.0.0"
 dafny_runtime = { path = "../../../submodules/smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync","small-int"] }
 dashmap = "6.1.0"
-pem = "3.0.4"
-tokio = {version = "1.44.1", features = ["full"] }
+pem = "3.0.5"
+tokio = {version = "1.45.0", features = ["full"] }
 uuid = { version = "1.16.0", features = ["v4"] }
 
 [[example]]
diff --git a/TestVectors/runtimes/rust/Cargo.toml b/TestVectors/runtimes/rust/Cargo.toml
index 06133e82c..9faf67d5d 100644
--- a/TestVectors/runtimes/rust/Cargo.toml
+++ b/TestVectors/runtimes/rust/Cargo.toml
@@ -11,17 +11,17 @@ default = ["wrapped-client"]
 wrapped-client = []
 
 [dependencies]
-aws-config = "1.5.15"
-aws-lc-rs = "1.12.2"
-aws-lc-sys = "0.25.0"
-aws-sdk-dynamodb = "1.62.0"
-aws-sdk-kms = "1.57.0"
-aws-smithy-runtime-api = {version = "1.7.3", features = ["client"] }
-aws-smithy-types = "1.2.12"
-chrono = "0.4.39"
+aws-config = "1.6.2"
+aws-lc-rs = "1.13.0"
+aws-lc-sys = "0.28.2"
+aws-sdk-dynamodb = "1.73.0"
+aws-sdk-kms = "1.67.0"
+aws-smithy-runtime-api = {version = "1.8.0", features = ["client"] }
+aws-smithy-types = "1.3.1"
+chrono = "0.4.41"
 cpu-time = "1.0.0"
 dafny_runtime = { path = "../../../submodules/smithy-dafny/TestModels/dafny-dependencies/dafny_runtime_rust", features = ["sync","small-int"] }
 dashmap = "6.1.0"
-pem = "3.0.4"
-tokio = {version = "1.43.0", features = ["full"] }
-uuid = { version = "1.12.1", features = ["v4"] }
+pem = "3.0.5"
+tokio = {version = "1.45.0", features = ["full"] }
+uuid = { version = "1.16.0", features = ["v4"] }
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
index 49e596b1c..571e3c564 160000
--- a/submodules/MaterialProviders
+++ b/submodules/MaterialProviders
@@ -1 +1 @@
-Subproject commit 49e596b1cd8ce446d0b82074ff48ba0406aa8995
+Subproject commit 571e3c564f1989e3c3df1fd765f4939326bc0893