diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml
index 999e04e47..b05e4dbd5 100644
--- a/.github/workflows/ci_test_vector_net.yml
+++ b/.github/workflows/ci_test_vector_net.yml
@@ -89,7 +89,7 @@ jobs:
       - name: Test TestVectors on .NET 6.0
         working-directory: ./${{matrix.library}}/runtimes/net
         run: |
-          cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json ../java/decrypt_rust_*.json .
+          cp ../java/decrypt_java_*.json ../java/decrypt_dotnet_*.json ../java/decrypt_rust_*.json ../java/large_records.json .
           dotnet run
           cp ../java/*.json .
           dotnet run --framework net6.0
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy
index 1951f0ed6..eed02792d 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy
@@ -12,21 +12,61 @@ module DynamoToStruct {
   import opened StandardLibrary
   import opened StandardLibrary.UInt
   import opened DynamoDbEncryptionUtil
-  import AwsCryptographyDbEncryptionSdkDynamoDbTypes
+  import Types = AwsCryptographyDbEncryptionSdkDynamoDbTypes
   import UTF8
   import SortedSets
   import Seq
   import Norm = DynamoDbNormalizeNumber
   import SE = StructuredEncryptionUtil
   import StandardLibrary.Sequence
+  import DafnyLibraries
 
-  type Error = AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error
+  type Error = Types.Error
 
   type TerminalDataMap = map<AttributeName, StructuredDataTerminal>
 
-  // This file exists for these two functions : ItemToStructured and StructuredToItem
+  // This file exists for ItemToStructured and StructuredToItem and their variants,
   // which provide conversion between an AttributeMap and a StructuredDataMap
 
+
+  // Identical to ItemToStructured, except that the result does not include any attributes configured as DO_NOTHING\
+  // Such attributes are unneeded, as they do not partake in signing nor encryption
+  function method ItemToStructured2(item : AttributeMap, actions : Types.AttributeActions) : (ret : Result<TerminalDataMap, Error>)
+  {
+    // var m := new DafnyLibraries.MutableMap<AttributeName, StructuredDataTerminal>();
+    // return MakeError("Not valid attribute names : ");
+
+    var structuredMap := map k <- item | k !in actions || actions[k] != DO_NOTHING || ReservedPrefix <= k :: k := AttrToStructured(item[k]);
+    MapKeysMatchItems(item);
+    MapError(SimplifyMapValue(structuredMap))
+  }
+
+  // Identical to StructuredToItem, except that any non encrypted fields in the original are passed through unchanged
+  // and only encrypted fields are run through StructuredToAttr
+  // This one is used for encryption, and so anything in s but not in orig is also kept
+  function method StructuredToItemEncrypt(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result<AttributeMap, Error>)
+  {
+    var ddbMap := map k <- orig :: k := if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) then StructuredToAttr(s[k]) else Success(orig[k]);
+    MapKeysMatchItems(orig);
+    var oldMap :- MapError(SimplifyMapValue(ddbMap));
+
+    var ddbMap2 := map k <- s | k !in orig :: k := StructuredToAttr(s[k]);
+    MapKeysMatchItems(s);
+    var newMap :- MapError(SimplifyMapValue(ddbMap2));
+
+    Success(oldMap + newMap)
+  }
+
+  // Identical to StructuredToItem, except that any non encrypted fields in the original are passed through unchanged
+  // and only encrypted fields are run through StructuredToAttr\
+  // This one is used for decryption, and so anything in s but not in orig is ignored
+  function method StructuredToItemDecrypt(s : TerminalDataMap, orig : AttributeMap, actions : CryptoSchemaMap) : (ret : Result<AttributeMap, Error>)
+  {
+    var ddbMap := map k <- orig | !(ReservedPrefix <= k) :: k := if (k in s && k in actions && actions[k] == ENCRYPT_AND_SIGN) then StructuredToAttr(s[k]) else Success(orig[k]);
+    MapKeysMatchItems(orig);
+    MapError(SimplifyMapValue(ddbMap))
+  }
+
   // Convert AttributeMap to StructuredDataMap
   function method {:opaque} ItemToStructured(item : AttributeMap) : (ret : Result<TerminalDataMap, Error>)
 
@@ -92,35 +132,46 @@ module DynamoToStruct {
 
   // everything past here is to implement those two
 
-  // Prove round trip. A work in progress
-  lemma RoundTripFromItem(item : AttributeValue)
-    ensures  item.B? && AttrToStructured(item).Success? ==> StructuredToAttr(AttrToStructured(item).value).Success?
-    ensures  item.NULL? && AttrToStructured(item).Success? ==>
-               && StructuredToAttr(AttrToStructured(item).value).Success?
-    ensures  item.BOOL? && AttrToStructured(item).Success? ==> StructuredToAttr(AttrToStructured(item).value).Success?
+  const UINT32_MAX : uint32 := 0xFFFF_FFFF
+
+  // TO BE DONE -- move to StandardLibrary
+  function method SeqPosToUInt32(s: seq<uint8>, pos : uint32): (x: uint32)
+    requires Add32(4,pos) as int <= |s|
+    ensures UInt32ToSeq(x) == s[pos..pos+4]
   {
-    reveal AttrToStructured();
-    reveal StructuredToAttr();
-    reveal TopLevelAttributeToBytes();
-    reveal AttrToBytes();
-    reveal BytesToAttr();
+    var x0 := s[pos] as uint32 * 0x100_0000;
+    var x1 := x0 + s[pos+1] as uint32 * 0x1_0000;
+    var x2 := x1 + s[pos+2] as uint32 * 0x100;
+    x2 + s[pos+3] as uint32
+  }
 
+  function method BigEndianPosToU32(x : seq<uint8>, pos : uint32) : (ret : Result<uint32, string>)
+    requires |x| < UINT32_MAX as int
+  {
+    if |x| as uint32 < Add32(pos, LENGTH_LEN32) then
+      Failure("Length of 4-byte integer was less than 4")
+    else
+      Success(SeqPosToUInt32(x, pos))
   }
 
-  // Prove round trip. A work in progress
-  lemma RoundTripFromStructured(s : StructuredDataTerminal)
-    ensures  StructuredToAttr(s).Success? && s.typeId == SE.BINARY ==>
-               && AttrToStructured(StructuredToAttr(s).value).Success?
-    ensures  StructuredToAttr(s).Success? && s.typeId == SE.BOOLEAN ==>
-               && AttrToStructured(StructuredToAttr(s).value).Success?
-    ensures  StructuredToAttr(s).Success? && s.typeId == SE.NULL ==>
-               && AttrToStructured(StructuredToAttr(s).value).Success?
+  // This is safe because are dealing with DynamoDB items, and so no numbers will exceed 400K
+  function method {:opaque} Add32(x : uint32, y : uint32) : (ret : uint32)
+    ensures x as uint64 + y as uint64 <= UINT32_MAX as uint64
+    ensures ret == x + y
   {
-    reveal AttrToStructured();
-    reveal StructuredToAttr();
-    reveal TopLevelAttributeToBytes();
-    reveal AttrToBytes();
-    reveal BytesToAttr();
+    var value : uint64 := x as uint64 + y as uint64;
+    assume {:axiom} value <= UINT32_MAX as uint64;
+    value as uint32
+  }
+
+  // This is safe because are dealing with DynamoDB items, and so no numbers will exceed 400K
+  function method {:opaque} Add32_3(x : uint32, y : uint32, z : uint32) : (ret : uint32)
+    ensures x as uint64 + y as uint64 + z as uint64 <= UINT32_MAX as uint64
+    ensures ret == x + y + z
+  {
+    var value : uint64 := x as uint64 + y as uint64 + z as uint64;
+    assume {:axiom} value <= UINT32_MAX as uint64;
+    value as uint32
   }
 
   function method MakeError<T>(s : string) : Result<T, Error> {
@@ -156,10 +207,13 @@ module DynamoToStruct {
 
   function method  {:opaque} StructuredToAttr(s : StructuredDataTerminal) : (ret : Result<AttributeValue, string>)
   {
-    :- Need(|s.typeId| == 2, "Type ID must be two bytes");
-    var attrValueAndLength :- BytesToAttr(s.value, s.typeId, false);
-    :- Need(attrValueAndLength.len == |s.value|, "Mismatch between length of encoded data and length of data");
-    Success(attrValueAndLength.val)
+    :- Need(|s.typeId| == TYPEID_LEN, "Type ID must be two bytes");
+    :-Need(|s.value| < UINT32_MAX as int, "Structured Data Too Big.");
+    var attrValueAndLength :- BytesToAttr(s.value, s.typeId, Some(|s.value| as uint32));
+    if attrValueAndLength.len != |s.value| as uint32 then
+      Failure("Mismatch between length of encoded data and length of data")
+    else
+      Success(attrValueAndLength.val)
   }
 
   const BOOL_LEN : nat := 1   // number of bytes in an encoded boolean
@@ -167,6 +221,11 @@ module DynamoToStruct {
   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
 
+  const BOOL_LEN32 : uint32 := 1   // number of bytes in an encoded boolean
+  const TYPEID_LEN32 : uint32 := 2   // number of bytes in a TerminalTypeId
+  const LENGTH_LEN32 : uint32 := 4 // number of bytes in an encoded count or length
+  const PREFIX_LEN32 : uint32 := 6 // number of bytes in a prefix, i.e. 2-byte type and 4-byte length
+
   function method AttrToTypeId(a : AttributeValue) : TerminalTypeId
   {
     match a {
@@ -189,9 +248,10 @@ module DynamoToStruct {
 
   // convert AttributeValue to byte sequence
   // if `prefix` is true, prefix sequence with TypeID and Length
-  function method {:opaque} AttrToBytes(a : AttributeValue, prefix : bool, depth : nat := 1) : (ret : Result<seq<uint8>, string>)
+  function method {:opaque} AttrToBytes(a : AttributeValue, prefix : bool, depth : uint32 := 1) : (ret : Result<seq<uint8>, string>)
+    requires depth <= (MAX_STRUCTURE_DEPTH+1)
     decreases a
-    ensures ret.Success? && prefix ==> 6 <= |ret.value|
+    ensures ret.Success? && prefix ==> PREFIX_LEN <= |ret.value|
     ensures MAX_STRUCTURE_DEPTH < depth ==> ret.Failure?
 
     //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#boolean
@@ -355,13 +415,14 @@ module DynamoToStruct {
               && (|a.L| == 0 ==> |ret.value| == LENGTH_LEN)
 
     ensures a.L? && ret.Success? && prefix ==>
+              && depth <= MAX_STRUCTURE_DEPTH
               && U32ToBigEndian(|a.L|).Success?
               && |ret.value| >= PREFIX_LEN + LENGTH_LEN
               && ret.value[0..TYPEID_LEN] == SE.LIST
               && ListAttrToBytes(a.L, depth).Success?
               && ret.value[PREFIX_LEN..] == ListAttrToBytes(a.L, depth).value
               && ListAttrToBytes(a.L, depth).value[..LENGTH_LEN] == U32ToBigEndian(|a.L|).value
-              && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value
+                 // && ret.value[PREFIX_LEN..PREFIX_LEN+LENGTH_LEN] == U32ToBigEndian(|a.L|).value
               && (|a.L| == 0 ==> |ret.value| == PREFIX_LEN + LENGTH_LEN)
 
     //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#map-attribute
@@ -372,6 +433,7 @@ module DynamoToStruct {
     //# | Key Value Pair Count   | 4        |
     //# | Key Value Pair Entries  | Variable |
     ensures a.M? && ret.Success? && !prefix ==>
+              && depth <= MAX_STRUCTURE_DEPTH
               && U32ToBigEndian(|a.M|).Success?
               && |ret.value| >= LENGTH_LEN
 
@@ -476,8 +538,9 @@ module DynamoToStruct {
   // along with the corresponding precondition,
   // lets Dafny find the correct termination metric.
   // See "The Parent Trick" for details: <https://leino.science/papers/krml283.html>.
-  function method MapAttrToBytes(ghost parent: AttributeValue, m: MapAttributeValue, depth : nat): (ret: Result<seq<uint8>, string>)
+  function method MapAttrToBytes(ghost parent: AttributeValue, m: MapAttributeValue, depth : uint32): (ret: Result<seq<uint8>, string>)
     requires forall k <- m :: m[k] < parent
+    requires depth <= MAX_STRUCTURE_DEPTH
   {
     //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#value-type
     //# Value Type MUST be the [Type ID](#type-id) of the type of [Map Value](#map-value).
@@ -500,11 +563,13 @@ module DynamoToStruct {
     Success(count + body)
   }
 
-  function method ListAttrToBytes(l: ListAttributeValue, depth : nat): (ret: Result<seq<uint8>, string>)
+  function method ListAttrToBytes(l: ListAttributeValue, depth : uint32): (ret: Result<seq<uint8>, string>)
+    requires depth <= MAX_STRUCTURE_DEPTH
     ensures ret.Success? ==>
               && U32ToBigEndian(|l|).Success?
               && LENGTH_LEN <= |ret.value|
               && ret.value[..LENGTH_LEN] == U32ToBigEndian(|l|).value
+    decreases l
   {
     var count :- U32ToBigEndian(|l|);
     var body :- CollectList(l, depth);
@@ -546,6 +611,14 @@ module DynamoToStruct {
       Success(SeqToUInt32(x[..LENGTH_LEN]) as nat)
   }
 
+  function method BigEndianToU32F(x : seq<uint8>) : (ret : Result<uint32, string>)
+  {
+    if |x| < LENGTH_LEN then
+      Failure("Length of 4-byte integer was less than 4")
+    else
+      Success(SeqToUInt32(x[..LENGTH_LEN]))
+  }
+
   predicate IsSorted<T>(s: seq<T>, lessThanOrEq: (T, T) -> bool) {
     forall j, k :: 0 <= j < k < |s| ==> lessThanOrEq(s[j], s[k])
   }
@@ -644,21 +717,59 @@ module DynamoToStruct {
   //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#list-entry-value
   //# A List MAY hold any DynamoDB Attribute Value data type,
   //# and MAY hold values of different types.
-  function method {:opaque} CollectList(
+
+  function {:opaque} CollectListGhost(
     listToSerialize : ListAttributeValue,
-    depth : nat,
+    depth : uint32,
     serialized : seq<uint8> := []
   )
     : (ret : Result<seq<uint8>, string>)
+    requires depth <= MAX_STRUCTURE_DEPTH
     ensures (ret.Success? && |listToSerialize| == 0) ==> (ret.value == serialized)
     ensures (ret.Success? && |listToSerialize| == 0) ==> (|ret.value| == |serialized|)
+    decreases listToSerialize, 1
   {
     if |listToSerialize| == 0 then
       Success(serialized)
     else
-      // Can't do the `pos` optimization, because I can't appease the `decreases`
       var val :- AttrToBytes(listToSerialize[0], true, depth+1);
-      CollectList(listToSerialize[1..], depth, serialized + val)
+      CollectListGhost(listToSerialize[1..], depth, serialized + val)
+  }
+
+  // Can't be {:tailrecursion} because it calls AttrToBytes which might again call CollectList
+  // However, we really need this to loop and not recurse.
+  // This verifies without the `by method`, but Dafny is too broken to let it verify by method
+  // for example, a call to CollectList somehow does not satisfy the decreases clause
+  // hence the {:verify false}
+  function {:opaque} CollectList(
+    listToSerialize : ListAttributeValue,
+    depth : uint32,
+    serialized : seq<uint8> := []
+  )
+    : (ret : Result<seq<uint8>, string>)
+    requires depth <= MAX_STRUCTURE_DEPTH
+    ensures (ret.Success? && |listToSerialize| == 0) ==> (ret.value == serialized)
+    ensures (ret.Success? && |listToSerialize| == 0) ==> (|ret.value| == |serialized|)
+    decreases listToSerialize, 2
+  {
+    CollectListGhost(listToSerialize, depth, serialized)
+  }
+  by method {
+    reveal CollectList();
+    reveal CollectListGhost();
+    var result := serialized;
+    for i := 0 to |listToSerialize|
+    {
+      var val := AttrToBytes(listToSerialize[i], true, depth+1);
+      if val.Failure? {
+        ret := Failure(val.error);
+        assume {:axiom} ret == CollectListGhost(listToSerialize, depth, serialized);
+        return;
+      }
+      result := result + val.value;
+    }
+    ret := Success(result);
+    assume {:axiom} ret == CollectListGhost(listToSerialize, depth, serialized);
   }
 
   function method SerializeMapItem(key : string, value : seq<uint8>) : (ret : Result<seq<uint8>, string>)
@@ -752,7 +863,7 @@ module DynamoToStruct {
   // AttributeValue with number of bytes consumed in its construction
   datatype AttrValueAndLength = AttrValueAndLength(
     val : AttributeValue,
-    len : nat
+    len : uint32
   )
 
   predicate method IsUnique<T(==)>(s : seq<T>)
@@ -763,13 +874,14 @@ module DynamoToStruct {
   // Bytes to Binary Set
   function method {:tailrecursion} {:vcs_split_on_every_assert}  {:opaque} DeserializeBinarySet(
     serialized : seq<uint8>,
-    remainingCount : nat,
-    origSerializedSize : nat,
+    remainingCount : uint32,
+    origSerializedSize : uint32,
     resultSet : AttrValueAndLength)
     : (ret : Result<AttrValueAndLength, string>)
     requires resultSet.val.BS?
+    requires |serialized| < UINT32_MAX as int
     ensures ret.Success? ==> ret.value.val.BS?
-    requires |serialized| + resultSet.len == origSerializedSize
+    requires Add32(|serialized| as uint32, resultSet.len) == origSerializedSize
     ensures ret.Success? ==> ret.value.len <= origSerializedSize
 
     //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates
@@ -783,25 +895,26 @@ module DynamoToStruct {
     else if |serialized| < LENGTH_LEN then
       Failure("Out of bytes reading Binary Set")
     else
-      var len :- BigEndianToU32(serialized);
+      var len :- BigEndianToU32F(serialized);
       var serialized := serialized[LENGTH_LEN..];
       if |serialized| < len as int then
         Failure("Binary Set Structured Data has too few bytes")
       else
         var nattr := AttributeValue.BS(resultSet.val.BS + [serialized[..len]]);
-        DeserializeBinarySet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN))
+        DeserializeBinarySet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN32))
   }
 
   // Bytes to String Set
   function method {:tailrecursion} {:vcs_split_on_every_assert} {:opaque} DeserializeStringSet(
     serialized : seq<uint8>,
-    remainingCount : nat,
-    origSerializedSize : nat,
+    remainingCount : uint32,
+    origSerializedSize : uint32,
     resultSet : AttrValueAndLength)
     : (ret : Result<AttrValueAndLength, string>)
     requires resultSet.val.SS?
+    requires |serialized| < UINT32_MAX as int
     ensures ret.Success? ==> ret.value.val.SS?
-    requires |serialized| + resultSet.len == origSerializedSize
+    requires Add32(|serialized| as uint32, resultSet.len) == origSerializedSize
     ensures ret.Success? ==> ret.value.len <= origSerializedSize
 
     //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates
@@ -815,26 +928,27 @@ module DynamoToStruct {
     else if |serialized| < LENGTH_LEN then
       Failure("Out of bytes reading String Set")
     else
-      var len :- BigEndianToU32(serialized);
+      var len : uint32 :- BigEndianToU32F(serialized);
       var serialized := serialized[LENGTH_LEN..];
       if |serialized| < len as int then
         Failure("String Set Structured Data has too few bytes")
       else
         var nstring :- UTF8.Decode(serialized[..len]);
         var nattr := AttributeValue.SS(resultSet.val.SS + [nstring]);
-        DeserializeStringSet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN))
+        DeserializeStringSet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN32))
   }
 
   // Bytes to Number Set
   function method {:tailrecursion} {:vcs_split_on_every_assert} {:opaque} DeserializeNumberSet(
     serialized : seq<uint8>,
-    remainingCount : nat,
-    origSerializedSize : nat,
+    remainingCount : uint32,
+    origSerializedSize : uint32,
     resultSet : AttrValueAndLength)
     : (ret : Result<AttrValueAndLength, string>)
     requires resultSet.val.NS?
+    requires |serialized| < UINT32_MAX as int
     ensures ret.Success? ==> ret.value.val.NS?
-    requires |serialized| + resultSet.len == origSerializedSize
+    requires Add32(|serialized| as uint32, resultSet.len) == origSerializedSize
     ensures ret.Success? ==> ret.value.len <= origSerializedSize
 
     //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates
@@ -848,103 +962,254 @@ module DynamoToStruct {
     else if |serialized| < LENGTH_LEN then
       Failure("Out of bytes reading String Set")
     else
-      var len :- BigEndianToU32(serialized);
+      var len :- BigEndianToU32F(serialized);
       var serialized := serialized[LENGTH_LEN..];
       if |serialized| < len as int then
         Failure("Number Set Structured Data has too few bytes")
       else
         var nstring :- UTF8.Decode(serialized[..len]);
         var nattr := AttributeValue.NS(resultSet.val.NS + [nstring]);
-        DeserializeNumberSet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN))
+        DeserializeNumberSet(serialized[len..], remainingCount-1, origSerializedSize, AttrValueAndLength(nattr, resultSet.len + len + LENGTH_LEN32))
   }
 
-  // Bytes to List
-  // Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeList
-  function method {:vcs_split_on_every_assert} {:opaque} DeserializeList(
+  function method {:vcs_split_on_every_assert} DeserializeListEntry(
     serialized : seq<uint8>,
-    remainingCount : nat,
-    ghost origSerializedSize : nat,
-    depth : nat,
-    resultList : AttrValueAndLength)
-    : (ret : Result<AttrValueAndLength, string>)
+    pos : uint32,
+    depth : uint32,
+    resultList : AttrValueAndLength
+  )
+    : (ret : Result<(AttrValueAndLength, uint32), string>)
+    requires |serialized| < UINT32_MAX as int
+    requires pos as int <= |serialized|
+    requires depth <= MAX_STRUCTURE_DEPTH
     requires resultList.val.L?
-    ensures ret.Success? ==> ret.value.val.L?
-    requires |serialized| + resultList.len == origSerializedSize
-    ensures ret.Success? ==> ret.value.len <= origSerializedSize
-    decreases |serialized|
+    ensures ret.Success? ==> ret.value.0.val.L?
+    ensures ret.Success? ==> pos < ret.value.1 <= |serialized| as uint32
+    decreases |serialized| as uint32 - pos, 0
   {
-    if remainingCount == 0 then
-      Success(resultList)
-    else if |serialized| < 6 then
+    var serialized_size := |serialized| as uint32;
+    if serialized_size-pos < PREFIX_LEN32 then
       Failure("Out of bytes reading Type of List element")
     else
-      var TerminalTypeId := serialized[0..2];
-      var serialized := serialized[2..];
-      var len :- BigEndianToU32(serialized);
-      var serialized := serialized[LENGTH_LEN..];
-      if |serialized| < len then
+      var TerminalTypeId := serialized[pos..pos+2];
+      var len : uint32 :- BigEndianPosToU32(serialized, pos+2);
+      var new_pos : uint32 := pos + PREFIX_LEN32;
+      if serialized_size - new_pos < len then
         Failure("Out of bytes reading Content of List element")
       else
-        var nval :- BytesToAttr(serialized[..len], TerminalTypeId, false, depth+1);
+        assert serialized_size == |serialized| as uint32;
+        var nval :- BytesToAttr(serialized, TerminalTypeId, Some(len), depth+1, new_pos);
+        var new_pos := Add32(new_pos, nval.len);
         var nattr := AttributeValue.L(resultList.val.L + [nval.val]);
-        DeserializeList(serialized[len..], remainingCount-1, origSerializedSize, depth, AttrValueAndLength(nattr, resultList.len + len + 6))
+        var nResultList := AttrValueAndLength(nattr, Add32(resultList.len, new_pos-pos));
+        Success((nResultList, new_pos))
   }
 
-  // Bytes to Map
-  // Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeMap
-  function method {:vcs_split_on_every_assert} {:opaque} DeserializeMap(
+  function {:vcs_split_on_every_assert} {:opaque} DeserializeListGhost(
     serialized : seq<uint8>,
-    remainingCount : nat,
-    ghost origSerializedSize : nat,
-    depth : nat,
+    pos : uint32,
+    orig_pos : uint32,
+    remainingCount : uint32,
+    depth : uint32,
+    resultList : AttrValueAndLength
+  )
+    : (ret : Result<AttrValueAndLength, string>)
+    requires |serialized| < UINT32_MAX as int
+    requires pos as int <= |serialized|
+    requires orig_pos <= pos
+    requires depth <= MAX_STRUCTURE_DEPTH
+    requires resultList.val.L?
+    ensures ret.Success? ==> ret.value.val.L?
+    requires pos == Add32(orig_pos, resultList.len)
+    ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos
+    decreases |serialized| as uint32 - pos, 1
+  {
+    if remainingCount == 0 then
+      Success(resultList)
+    else
+      var (newResultList, npos) :- DeserializeListEntry(serialized, pos, depth, resultList);
+      DeserializeListGhost(serialized, npos, orig_pos, remainingCount - 1, depth, newResultList)
+  }
+
+  // Bytes to List
+  // Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeList
+  // However, we really need this to loop and not recurse.
+  // This verifies without the `by method`, but Dafny is too broken to let it verify by method
+  // for example, a call to DeserializeListEntry somehow does not satisfy the decreases clause
+  // hence the {:verify false}
+  function {:vcs_split_on_every_assert} {:opaque} DeserializeList(
+    serialized : seq<uint8>,
+    pos : uint32,
+    ghost orig_pos : uint32,
+    remainingCount : uint32,
+    depth : uint32,
+    resultList : AttrValueAndLength
+  )
+    : (ret : Result<AttrValueAndLength, string>)
+    requires |serialized| < UINT32_MAX as int
+    requires pos as int <= |serialized|
+    requires orig_pos <= pos
+    requires depth <= MAX_STRUCTURE_DEPTH
+    requires resultList.val.L?
+    ensures ret.Success? ==> ret.value.val.L?
+    requires pos == Add32(orig_pos, resultList.len)
+    ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos
+    decreases |serialized| as uint32 - pos, 2
+  {
+    DeserializeListGhost(serialized, pos, orig_pos, remainingCount, depth, resultList)
+  }
+  by method {
+    reveal DeserializeListGhost();
+    reveal DeserializeList();
+    var npos : uint32 := pos;
+    var newResultList := resultList;
+    for i := 0 to remainingCount
+      invariant serialized == old(serialized)
+      invariant newResultList.val.L?
+      invariant npos as int <= |serialized|
+      invariant npos == Add32(orig_pos, newResultList.len)
+      invariant npos >= pos
+    {
+      var test := DeserializeListEntry(serialized, npos, depth, newResultList);
+      if test.Failure? {
+        ret := Failure(test.error);
+        assume {:axiom} ret == DeserializeListGhost(serialized, pos, orig_pos, remainingCount, depth, resultList);
+        return;
+      }
+      newResultList := test.value.0;
+      npos := test.value.1;
+    }
+    ret := Success(newResultList);
+    assume {:axiom} ret == DeserializeListGhost(serialized, pos, orig_pos, remainingCount, depth, resultList);
+  }
+
+  function method {:vcs_split_on_every_assert} DeserializeMapEntry(
+    serialized : seq<uint8>,
+    pos : uint32,
+    depth : uint32,
+    resultMap : AttrValueAndLength
+  )
+    : (ret : Result<(AttrValueAndLength, uint32), string>)
+    requires |serialized| < UINT32_MAX as int
+    requires pos as int <= |serialized|
+    requires depth <= MAX_STRUCTURE_DEPTH
+    requires resultMap.val.M?
+    ensures ret.Success? ==> pos < ret.value.1 <= |serialized| as uint32
+    decreases |serialized| as uint32 - pos, 0
+  {
+    var serialized_size := |serialized| as uint32;
+    var orig_pos := pos;
+
+    // get typeId of key
+    :- Need(PREFIX_LEN32 <= serialized_size-pos, "Out of bytes reading Map Key");
+    var TerminalTypeId_key := serialized[pos..pos+TYPEID_LEN32];
+    :- Need(TerminalTypeId_key == SE.STRING, "Key of Map is not String");
+    var pos := pos + TYPEID_LEN32;
+
+    // get key
+    var len : uint32 :- BigEndianPosToU32(serialized, pos);
+    var pos := pos + LENGTH_LEN32;
+    :- Need(len <= serialized_size-pos, "Key of Map of Structured Data has too few bytes");
+    var key :- UTF8.Decode(serialized[pos..pos+len]);
+    var pos := pos + len;
+
+    // get typeId of value
+    :- Need(2 <= serialized_size-pos, "Out of bytes reading Map Value");
+    :- Need(IsValid_AttributeName(key), "Key is not valid AttributeName");
+    var TerminalTypeId_value := serialized[pos..pos+TYPEID_LEN32];
+    var pos := pos + TYPEID_LEN32;
+
+    // get value and construct result
+    var nval :- BytesToAttr(serialized, TerminalTypeId_value, None, depth+1, pos);
+    var pos := Add32(pos, nval.len);
+
+    //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#key-value-pair-entries
+    //# This sequence MUST NOT contain duplicate [Map Keys](#map-key).
+
+    //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates
+    //# - Conversion from a Structured Data Map MUST fail if it has duplicate keys
+
+    :- Need(key !in resultMap.val.M, "Duplicate key in map.");
+    var nattr := AttributeValue.M(resultMap.val.M[key := nval.val]);
+    var newResultMap := AttrValueAndLength(nattr, Add32(resultMap.len, (pos - orig_pos)));
+
+    Success((newResultMap, pos))
+  }
+
+  function {:vcs_split_on_every_assert} {:opaque}  DeserializeMapGhost(
+    serialized : seq<uint8>,
+    pos : uint32,
+    orig_pos : uint32,
+    remainingCount : uint32,
+    depth : uint32,
     resultMap : AttrValueAndLength)
     : (ret : Result<AttrValueAndLength, string>)
+    requires |serialized| < UINT32_MAX as int
+    requires pos as int <= |serialized|
+    requires orig_pos <= pos
     requires resultMap.val.M?
+    requires depth <= MAX_STRUCTURE_DEPTH
     ensures ret.Success? ==> ret.value.val.M?
-    requires |serialized| + resultMap.len == origSerializedSize
-    ensures ret.Success? ==> ret.value.len <= origSerializedSize
-    decreases |serialized|
+    requires pos == Add32(orig_pos, resultMap.len)
+    ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos
+    decreases |serialized| as uint32 - pos, 1
   {
-    ghost var serializedInitial := serialized;
-
     if remainingCount == 0 then
       Success(resultMap)
     else
-      // get typeId of key
-      :- Need(6 <= |serialized|, "Out of bytes reading Map Key");
-      var TerminalTypeId_key := serialized[0..2];
-      :- Need(TerminalTypeId_key == SE.STRING, "Key of Map is not String");
-      var serialized := serialized[2..];
-
-      // get key
-      var len :- BigEndianToU32(serialized);
-      var serialized := serialized[LENGTH_LEN..];
-      :- Need(len as int <= |serialized|, "Key of Map of Structured Data has too few bytes");
-      var key :- UTF8.Decode(serialized[..len]);
-      var serialized := serialized[len..];
-
-      assert |serialized| + 6 + len == |serializedInitial|;
-
-      // get typeId of value
-      :- Need(2 <= |serialized|, "Out of bytes reading Map Value");
-      :- Need(IsValid_AttributeName(key), "Key is not valid AttributeName");
-      var TerminalTypeId_value := serialized[0..2];
-      var serialized := serialized[2..];
-
-      // get value and construct result
-      var nval :- BytesToAttr(serialized, TerminalTypeId_value, true, depth+1);
-      var serialized := serialized[nval.len..];
-
-      //= specification/dynamodb-encryption-client/ddb-attribute-serialization.md#key-value-pair-entries
-      //# This sequence MUST NOT contain duplicate [Map Keys](#map-key).
-
-      //= specification/dynamodb-encryption-client/ddb-item-conversion.md#duplicates
-      //# - Conversion from a Structured Data Map MUST fail if it has duplicate keys
-      :- Need(key !in resultMap.val.M, "Duplicate key in map.");
-      var nattr := AttributeValue.M(resultMap.val.M[key := nval.val]);
-      var newResultMap := AttrValueAndLength(nattr, resultMap.len + nval.len + 8 + len);
-      assert |serialized| + newResultMap.len == origSerializedSize;
-      DeserializeMap(serialized, remainingCount - 1, origSerializedSize, depth, newResultMap)
+      var (newResultMap, npos) :- DeserializeMapEntry(serialized, pos, depth, resultMap);
+      DeserializeMapGhost(serialized, npos, orig_pos, remainingCount - 1, depth, newResultMap)
+  }
+
+  // Bytes to Map
+  // Can't be {:tailrecursion} because it calls BytesToAttr which might again call DeserializeMap
+  // However, we really need this to loop and not recurse.
+  // This verifies without the `by method`, but Dafny is too broken to let it verify by method
+  // for example, a call to DeserializeMapEntry somehow does not satisfy the decreases clause
+  // hence the {:verify false}
+  function {:vcs_split_on_every_assert} {:opaque}  DeserializeMap(
+    serialized : seq<uint8>,
+    pos : uint32,
+    ghost orig_pos : uint32,
+    remainingCount : uint32,
+    depth : uint32,
+    resultMap : AttrValueAndLength)
+    : (ret : Result<AttrValueAndLength, string>)
+    requires |serialized| < UINT32_MAX as int
+    requires pos as int <= |serialized|
+    requires orig_pos <= pos
+    requires resultMap.val.M?
+    requires depth <= MAX_STRUCTURE_DEPTH
+    ensures ret.Success? ==> ret.value.val.M?
+    requires pos == Add32(orig_pos, resultMap.len)
+    ensures ret.Success? ==> ret.value.len <= |serialized| as uint32 - orig_pos
+    decreases |serialized| as uint32 - pos, 2
+  {
+    DeserializeMapGhost(serialized, pos, orig_pos, remainingCount, depth, resultMap)
+  }
+  by method {
+    reveal DeserializeMapGhost();
+    reveal DeserializeMap();
+    var npos : uint32 := pos;
+    var newResultMap := resultMap;
+    for i := 0 to remainingCount
+      invariant serialized == old(serialized)
+      invariant newResultMap.val.M?
+      invariant npos as int <= |serialized|
+      invariant npos == Add32(orig_pos, newResultMap.len)
+      invariant npos >= pos
+    {
+      var test := DeserializeMapEntry(serialized, npos, depth, newResultMap);
+      if test.Failure? {
+        ret := Failure(test.error);
+        assume {:axiom} ret == DeserializeMapGhost(serialized, pos, orig_pos, remainingCount, depth, resultMap);
+        return;
+      }
+      newResultMap := test.value.0;
+      npos := test.value.1;
+    }
+    ret := Success(newResultMap);
+    assume {:axiom} ret == DeserializeMapGhost(serialized, pos, orig_pos, remainingCount, depth, resultMap);
   }
 
   // Bytes to AttributeValue
@@ -952,26 +1217,28 @@ module DynamoToStruct {
   function method {:vcs_split_on_every_assert} {:opaque} BytesToAttr(
     value : seq<uint8>,
     typeId : TerminalTypeId,
-    hasLen : bool,
-    depth : nat := 1
+    totalBytes : Option<uint32>, // Some(number of bytes past pos) or None for 'read first bytes to find length'
+    depth : uint32 := 1,
+    pos : uint32 := 0    // starting position within value
   )
     : (ret : Result<AttrValueAndLength, string>)
-    ensures ret.Success? ==> ret.value.len <= |value|
+    requires |value| < UINT32_MAX as int
+    requires pos <= |value| as uint32
+    requires totalBytes.Some? ==> Add32(pos, totalBytes.value) <= |value| as uint32
+    ensures ret.Success? ==> Add32(pos, ret.value.len) <= |value| as uint32
     ensures MAX_STRUCTURE_DEPTH < depth ==> ret.Failure?
-    decreases |value|
+    decreases |value| as uint32 - pos
   {
+    var value_size : uint32 := |value| as uint32;
     :- Need(depth <= MAX_STRUCTURE_DEPTH, "Depth of attribute structure to deserialize exceeds limit of " + MAX_STRUCTURE_DEPTH_STR);
-    var len :- if hasLen then
-                 if |value| < LENGTH_LEN then
-                   Failure("Out of bytes reading length")
-                 else
-                   BigEndianToU32(value)
-               else
-                 Success(|value|);
-    var value := if hasLen then value[LENGTH_LEN..] else value;
-    var lengthBytes := if hasLen then LENGTH_LEN else 0;
-
-    if |value| < len then
+    var len : uint32 :- if totalBytes.None? then
+                          BigEndianPosToU32(value, pos)
+                        else
+                          Success(totalBytes.value);
+    var pos := if totalBytes.None? then Add32(pos, LENGTH_LEN32) else pos;
+    var lengthBytes : uint32 := if totalBytes.None? then LENGTH_LEN32 else 0;
+
+    if value_size - pos < len then
       Failure("Structured Data has too few bytes")
 
     else if typeId == SE.NULL then
@@ -985,66 +1252,85 @@ module DynamoToStruct {
         Success(AttrValueAndLength(AttributeValue.NULL(true), lengthBytes))
 
     else if typeId == SE.STRING then
-      var str :- UTF8.Decode(value[..len]);
+      var str :- UTF8.Decode(value[pos..pos+len]);
       Success(AttrValueAndLength(AttributeValue.S(str), len+lengthBytes))
 
     else if typeId == SE.NUMBER then
-      var str :- UTF8.Decode(value[..len]);
+      var str :- UTF8.Decode(value[pos..pos+len]);
       Success(AttrValueAndLength(AttributeValue.N(str), len+lengthBytes))
 
     else if typeId == SE.BINARY then
-      Success(AttrValueAndLength(AttributeValue.B(value[..len]), len+lengthBytes))
+      Success(AttrValueAndLength(AttributeValue.B(value[pos..pos+len]), len+lengthBytes))
 
     else if typeId == SE.BOOLEAN then
-      if len != BOOL_LEN then
+      if len != BOOL_LEN32 then
         Failure("Boolean Structured Data has more than one byte")
-      else if value[0] == 0x00 then
-        Success(AttrValueAndLength(AttributeValue.BOOL(false), BOOL_LEN+lengthBytes))
-      else if value[0] == 0x01 then
-        Success(AttrValueAndLength(AttributeValue.BOOL(true), BOOL_LEN+lengthBytes))
+      else if value[pos] == 0x00 then
+        Success(AttrValueAndLength(AttributeValue.BOOL(false), BOOL_LEN32+lengthBytes))
+      else if value[pos] == 0x01 then
+        Success(AttrValueAndLength(AttributeValue.BOOL(true), BOOL_LEN32+lengthBytes))
       else
         Failure("Boolean Structured Data had inappropriate value")
 
     else if typeId == SE.STRING_SET then
-      if |value| < LENGTH_LEN then
+      if value_size - pos < LENGTH_LEN32 then
         Failure("String Set Structured Data has less than LENGTH_LEN bytes")
       else
-        var len :- BigEndianToU32(value);
-        var value := value[LENGTH_LEN..];
-        DeserializeStringSet(value, len, |value| + LENGTH_LEN + lengthBytes, AttrValueAndLength(AttributeValue.SS([]), LENGTH_LEN+lengthBytes))
+        var len : uint32 :- BigEndianPosToU32(value, pos);
+        var pos : uint32 := pos + LENGTH_LEN32;
+        var retval :- DeserializeStringSet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.SS([]), LENGTH_LEN32+lengthBytes));
+        // this is not needed with Dafny 4.10
+        assume {:axiom} Add32(pos, retval.len) <= |value| as uint32;
+        Success(retval)
 
     else if typeId == SE.NUMBER_SET then
-      if |value| < LENGTH_LEN then
+      if value_size - pos < LENGTH_LEN32 then
         Failure("Number Set Structured Data has less than 4 bytes")
       else
-        var len :- BigEndianToU32(value);
-        var value := value[LENGTH_LEN..];
-        DeserializeNumberSet(value, len, |value| + LENGTH_LEN + lengthBytes, AttrValueAndLength(AttributeValue.NS([]), LENGTH_LEN + lengthBytes))
+        var len : uint32 :- BigEndianPosToU32(value, pos);
+        var pos : uint32 := pos + LENGTH_LEN32;
+        var retval :- DeserializeNumberSet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.NS([]), LENGTH_LEN32 + lengthBytes));
+        // this is not needed with Dafny 4.10
+        assume {:axiom} Add32(pos, retval.len) <= |value| as uint32;
+        Success(retval)
 
     else if typeId == SE.BINARY_SET then
-      if |value| < LENGTH_LEN then
+      if value_size - pos < LENGTH_LEN32 then
         Failure("Binary Set Structured Data has less than LENGTH_LEN bytes")
       else
-        var len :- BigEndianToU32(value);
-        var value := value[LENGTH_LEN..];
-        DeserializeBinarySet(value, len, |value| + LENGTH_LEN + lengthBytes, AttrValueAndLength(AttributeValue.BS([]), LENGTH_LEN + lengthBytes))
+        var len : uint32 :- BigEndianPosToU32(value, pos);
+        var pos : uint32 := pos + LENGTH_LEN32;
+        var retval :- DeserializeBinarySet(value[pos..], len, Add32_3(value_size - pos, LENGTH_LEN32, lengthBytes), AttrValueAndLength(AttributeValue.BS([]), LENGTH_LEN32 + lengthBytes));
+        // this is not needed with Dafny 4.10
+        assume {:axiom} Add32(pos, retval.len) <= |value| as uint32;
+        Success(retval)
 
     else if typeId == SE.MAP then
-      if |value| < LENGTH_LEN then
+      if value_size < Add32(LENGTH_LEN32, pos) then
         Failure("List Structured Data has less than 4 bytes")
       else
-        var len :- BigEndianToU32(value);
-        var value := value[LENGTH_LEN..];
-        DeserializeMap(value, len, |value| + LENGTH_LEN + lengthBytes, depth, AttrValueAndLength(AttributeValue.M(map[]), LENGTH_LEN + lengthBytes))
+        var len : uint32 :- BigEndianPosToU32(value, pos);
+        var pos : uint32 := pos + LENGTH_LEN32;
+        var resultMap := AttrValueAndLength(AttributeValue.M(map[]), LENGTH_LEN32 + lengthBytes);
+        var retval :- DeserializeMap(value, pos, pos - resultMap.len, len, depth, resultMap);
+        // this is not needed with Dafny 4.10
+        assume {:axiom} Add32(pos, retval.len) <= |value| as uint32;
+        Success(retval)
 
     else if typeId == SE.LIST then
-      if |value| < LENGTH_LEN then
+      if value_size < Add32(LENGTH_LEN32, pos) then
         Failure("List Structured Data has less than 4 bytes")
       else
-        var len :- BigEndianToU32(value);
-        var value := value[LENGTH_LEN..];
-        DeserializeList(value, len, |value| + LENGTH_LEN + lengthBytes, depth, AttrValueAndLength(AttributeValue.L([]), LENGTH_LEN + lengthBytes))
-
+        var len : uint32 :- BigEndianPosToU32(value, pos);
+        var pos : uint32 := pos + LENGTH_LEN32;
+        assert pos <= value_size;
+        assert value_size == |value| as uint32;
+        assert pos <= |value| as uint32;
+        var resultList := AttrValueAndLength(AttributeValue.L([]), LENGTH_LEN32 + lengthBytes);
+        var retval :- DeserializeList(value, pos, pos - resultList.len, len, depth, resultList);
+        // this is not needed with Dafny 4.10
+        assume {:axiom} Add32(pos, retval.len) <= |value| as uint32;
+        Success(retval)
     else
       Failure("Unsupported TerminalTypeId")
 
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy
index bedbe19c7..348535a56 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy
@@ -223,6 +223,25 @@ module SearchableEncryptionInfo {
       return Success(keyLoc.keys);
     }
 
+    function method PosLongAdd(x : MP.PositiveLong, y : MP.PositiveLong) : MP.PositiveLong
+    {
+      assert MP.IsValid_PositiveLong(x);
+      assert MP.IsValid_PositiveLong(y);
+      if x as nat + y as nat < INT64_MAX_LIMIT then
+        x + y
+      else
+        INT64_MAX_LIMIT as MP.PositiveLong
+    }
+    function method PosLongSub(x : MP.PositiveLong, y : MP.PositiveLong) : MP.PositiveLong
+    {
+      assert MP.IsValid_PositiveLong(x);
+      assert MP.IsValid_PositiveLong(y);
+      if x <= y then
+        0
+      else
+        x - y
+    }
+
     // Checks if (time_now - cache creation time of the extracted cache entry) is less than the allowed
     // TTL of the current Beacon Key Source calling the getEntry method from the cache.
     // Mitigates risk if another Beacon Key Source wrote the entry with a longer TTL.
@@ -232,7 +251,10 @@ module SearchableEncryptionInfo {
       ttlSeconds: MP.PositiveLong
     ): (output: bool)
     {
-      now - creationTime <= ttlSeconds as MP.PositiveLong
+      if now <= creationTime then
+        true
+      else
+        PosLongSub(now, creationTime) <= ttlSeconds as MP.PositiveLong
     }
 
     method getKeysCache(
@@ -406,7 +428,6 @@ module SearchableEncryptionInfo {
         var keyMap :- getAllKeys(stdNames, key.value);
         var beaconKeyMaterials := rawBeaconKeyMaterials.beaconKeyMaterials.(beaconKey := None, hmacKeys := Some(keyMap));
 
-        expect now < UInt.BoundedInts.INT64_MAX - cacheTTL;
         //= specification/searchable-encryption/search-config.md#get-beacon-key-materials
         //# These materials MUST be put into the associated [Key Store Cache](#key-store-cache)
         //# with an [Expiry Time](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#expiry-time)
@@ -415,7 +436,7 @@ module SearchableEncryptionInfo {
           identifier := cacheDigest,
           materials := MP.Materials.BeaconKey(beaconKeyMaterials),
           creationTime := now,
-          expiryTime := now + cacheTTL,
+          expiryTime := PosLongAdd(now, cacheTTL),
           messagesUsed := None,
           bytesUsed := None
         );
diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy
index b0ec519f3..866a93684 100644
--- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy
@@ -14,7 +14,7 @@ module DynamoDbEncryptionUtil {
   const BeaconPrefix := "aws_dbe_b_"
   const VersionPrefix := "aws_dbe_v_"
 
-  const MAX_STRUCTURE_DEPTH := 32
+  const MAX_STRUCTURE_DEPTH : uint32 := 32
   const MAX_STRUCTURE_DEPTH_STR := "32"
 
   type HmacKeyMap = map<string, Bytes>
diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy
index c1b9681fa..972c51c4c 100644
--- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy
@@ -417,6 +417,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     ensures version == 1 <==> ret == CSE.SIGN_ONLY
     ensures version == 2 <==> ret == CSE.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
   {
+    assert StructuredEncryptionHeader.ValidVersion(version);
+    assert version == 1 || version == 2;
     if version == 2 then
       CSE.SIGN_AND_INCLUDE_IN_ENCRYPTION_CONTEXT
     else
@@ -546,7 +548,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
   // get CryptoSchema for this item
   function method ConfigToCryptoSchema(
     config : InternalConfig,
-    item : ComAmazonawsDynamodbTypes.AttributeMap)
+    item : DynamoToStruct.TerminalDataMap)
     : (ret : Result<CSE.CryptoSchemaMap, DDBE.Error>)
 
     //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
@@ -590,7 +592,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
   // get AuthenticateSchema for this item
   function method ConfigToAuthenticateSchema(
     config : InternalConfig,
-    item : ComAmazonawsDynamodbTypes.AttributeMap)
+    item : DynamoToStruct.TerminalDataMap)
     : (ret : CSE.AuthenticateSchemaMap)
     requires ValidInternalConfig?(config)
 
@@ -636,6 +638,8 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     ensures ret.Success? ==> forall k <- ret.value.Keys :: InSignatureScope(config, k)
     ensures ret.Success? ==> forall k <- ret.value.Keys :: !ret.value[k].DO_NOTHING?
   {
+    assert forall k <- schema :: SE.IsAuthAttr(schema[k]);
+    assert forall k <- schema :: !schema[k].DO_NOTHING?;
     :- Need(forall k <- schema :: InSignatureScope(config, k),
             DynamoDbItemEncryptorException( message := "Received unexpected Crypto Schema: mismatch with signature scope"));
     :- Need(forall k <- schema :: ComAmazonawsDynamodbTypes.IsValid_AttributeName(k),
@@ -747,22 +751,22 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
         && (|config.structuredEncryption.History.EncryptStructure| == |old(config.structuredEncryption.History.EncryptStructure)| + 1)
         && (Seq.Last(config.structuredEncryption.History.EncryptStructure).output.Success?)
 
-        //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
-        //= type=implication
-        //# - Crypto Schema MUST be a [Crypto Schema](../structured-encryption/structures.md#crypto-schema)
-        //# analogous to the [configured Attribute Actions](./ddb-table-encryption-config.md#attribute-actions).
-        && ConfigToCryptoSchema(config, input.plaintextItem).Success?
-        && Seq.Last(config.structuredEncryption.History.EncryptStructure).input.cryptoSchema
-           == ConfigToCryptoSchema(config, input.plaintextItem).value
-
         //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
         //= type=implication
         //# - Structured Data MUST be the Structured Data converted above.
-        && DynamoToStruct.ItemToStructured(input.plaintextItem).Success?
-        && var plaintextStructure := DynamoToStruct.ItemToStructured(input.plaintextItem).value;
+        && DynamoToStruct.ItemToStructured2(input.plaintextItem, config.attributeActionsOnEncrypt).Success?
+        && var plaintextStructure := DynamoToStruct.ItemToStructured2(input.plaintextItem, config.attributeActionsOnEncrypt).value;
         && Seq.Last(config.structuredEncryption.History.EncryptStructure).input.plaintextStructure
            == plaintextStructure
 
+        //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
+        //= type=implication
+        //# - Crypto Schema MUST be a [Crypto Schema](../structured-encryption/structures.md#crypto-schema)
+        //# analogous to the [configured Attribute Actions](./ddb-table-encryption-config.md#attribute-actions).
+        && ConfigToCryptoSchema(config, plaintextStructure).Success?
+        && Seq.Last(config.structuredEncryption.History.EncryptStructure).input.cryptoSchema
+           == ConfigToCryptoSchema(config, plaintextStructure).value
+
         //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
         //= type=implication
         //# - Encryption Context MUST be this input Item's [DynamoDB Item Base Context](#dynamodb-item-base-context).
@@ -800,8 +804,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
       ==>
         && output.value.encryptedItem == input.plaintextItem
         && output.value.parsedHeader == None
-
-    ensures output.Success? ==> |input.plaintextItem| <= MAX_ATTRIBUTE_COUNT
   {
     :- Need(
       && config.partitionKeyName in input.plaintextItem
@@ -811,12 +813,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     :- Need(ContextAttrsExist(config.attributeActionsOnEncrypt, input.plaintextItem),
             E(ContextMissingMsg(config.attributeActionsOnEncrypt, input.plaintextItem)));
 
-    if |input.plaintextItem| > MAX_ATTRIBUTE_COUNT {
-      var actCount := String.Base10Int2String(|input.plaintextItem|);
-      var maxCount := String.Base10Int2String(MAX_ATTRIBUTE_COUNT);
-      return Failure(E("Item to encrypt had " + actCount + " attributes, but maximum allowed is " + maxCount));
-    }
-
     //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
     //# If a [Legacy Policy](./ddb-table-encryption-config.md#legacy-policy) of
     //# `FORCE_LEGACY_ENCRYPT_ALLOW_LEGACY_DECRYPT` is specified,
@@ -839,10 +835,10 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
       return Success(passthroughOutput);
     }
 
-    var plaintextStructure :- DynamoToStruct.ItemToStructured(input.plaintextItem)
+    var plaintextStructure :- DynamoToStruct.ItemToStructured2(input.plaintextItem, config.attributeActionsOnEncrypt)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
     var context :- MakeEncryptionContextForEncrypt(config, plaintextStructure);
-    var cryptoSchema :- ConfigToCryptoSchema(config, input.plaintextItem)
+    var cryptoSchema :- ConfigToCryptoSchema(config, plaintextStructure)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
 
     //= specification/dynamodb-encryption-client/encrypt-item.md#behavior
@@ -893,7 +889,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
       e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(DDBE.AwsCryptographyDbEncryptionSdkStructuredEncryption(e)));
     var encryptedData := encryptVal.encryptedStructure;
     :- Need(forall k <- encryptedData :: DDB.IsValid_AttributeName(k), E(""));
-    var ddbKey :- DynamoToStruct.StructuredToItem(encryptedData)
+    var ddbKey :- DynamoToStruct.StructuredToItemEncrypt(encryptedData, input.plaintextItem, config.attributeActionsOnEncrypt)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
 
     var parsedActions :- ConvertCryptoSchemaToAttributeActions(config, encryptVal.cryptoSchema);
@@ -957,21 +953,21 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
         && (|config.structuredEncryption.History.DecryptStructure| == |old(config.structuredEncryption.History.DecryptStructure)| + 1)
         && (Seq.Last(config.structuredEncryption.History.DecryptStructure).output.Success?)
 
-        //= specification/dynamodb-encryption-client/decrypt-item.md#behavior
-        //= type=implication
-        //# - Authenticate Schema MUST be a [Authenticate Schema](../structured-encryption/structures.md#crypto-schema)
-        //# built with the following requirements:
-        && Seq.Last(config.structuredEncryption.History.DecryptStructure).input.authenticateSchema
-           == ConfigToAuthenticateSchema(config, input.encryptedItem)
-
         //= specification/dynamodb-encryption-client/decrypt-item.md#behavior
         //= type=implication
         //# - Encrypted Structured Data MUST be the Structured Data converted above.
-        && DynamoToStruct.ItemToStructured(input.encryptedItem).Success?
-        && var plaintextStructure := DynamoToStruct.ItemToStructured(input.encryptedItem).value;
+        && DynamoToStruct.ItemToStructured2(input.encryptedItem, config.attributeActionsOnEncrypt).Success?
+        && var plaintextStructure := DynamoToStruct.ItemToStructured2(input.encryptedItem, config.attributeActionsOnEncrypt).value;
         && Seq.Last(config.structuredEncryption.History.DecryptStructure).input.encryptedStructure
            == plaintextStructure
 
+        //= specification/dynamodb-encryption-client/decrypt-item.md#behavior
+        //= type=implication
+        //# - Authenticate Schema MUST be a [Authenticate Schema](../structured-encryption/structures.md#crypto-schema)
+        //# built with the following requirements:
+        && Seq.Last(config.structuredEncryption.History.DecryptStructure).input.authenticateSchema
+           == ConfigToAuthenticateSchema(config, plaintextStructure)
+
         //= specification/dynamodb-encryption-client/decrypt-item.md#dynamodb-item-base-context
         //= type=implication
         //# The item to be encrypted MUST have an attribute named `aws_dbe_head`.
@@ -1037,13 +1033,6 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
         && output.value.plaintextItem == input.encryptedItem
         && output.value.parsedHeader == None
   {
-    var realCount := |set k <- input.encryptedItem | !(ReservedPrefix <= k)|;
-    if realCount > MAX_ATTRIBUTE_COUNT {
-      var actCount := String.Base10Int2String(realCount);
-      var maxCount := String.Base10Int2String(MAX_ATTRIBUTE_COUNT);
-      return Failure(E("Item to decrypt had " + actCount + " attributes, but maximum allowed is " + maxCount));
-    }
-
     :- Need(
       && config.partitionKeyName in input.encryptedItem
       && (config.sortKeyName.None? || config.sortKeyName.value in input.encryptedItem)
@@ -1081,7 +1070,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
             DynamoDbItemEncryptorException(
               message := "Encrypted item missing expected header and footer attributes"));
 
-    var encryptedStructure :- DynamoToStruct.ItemToStructured(input.encryptedItem)
+    var encryptedStructure :- DynamoToStruct.ItemToStructured2(input.encryptedItem, config.attributeActionsOnEncrypt)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
     :- Need(SE.HeaderField in input.encryptedItem, E("Header field, \"aws_dbe_head\", not in item."));
     var header := input.encryptedItem[SE.HeaderField];
@@ -1089,7 +1078,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
     assert header.B?;
     :- Need(0 < |header.B|, E("Unexpected empty header field."));
     var context :- MakeEncryptionContextForDecrypt(config, header.B, encryptedStructure);
-    var authenticateSchema := ConfigToAuthenticateSchema(config, input.encryptedItem);
+    var authenticateSchema := ConfigToAuthenticateSchema(config, encryptedStructure);
 
     //= specification/dynamodb-encryption-client/decrypt-item.md#behavior
     //# This operation MUST create a
@@ -1123,7 +1112,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs
       e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(DDBE.AwsCryptographyDbEncryptionSdkStructuredEncryption(e)));
     var decryptedData := decryptVal.plaintextStructure;
     :- Need(forall k <- decryptedData :: DDB.IsValid_AttributeName(k), E(""));
-    var ddbItem :- DynamoToStruct.StructuredToItem(decryptedData)
+    var ddbItem :- DynamoToStruct.StructuredToItemDecrypt(decryptedData, input.encryptedItem, decryptVal.cryptoSchema)
     .MapFailure(e => Error.AwsCryptographyDbEncryptionSdkDynamoDb(e));
 
     var schemaToConvert := decryptVal.cryptoSchema;
diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
index 7bea3d88b..3f162a63d 100644
--- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/Util.dfy
@@ -18,7 +18,7 @@ module DynamoDbItemEncryptorUtil {
   const ReservedPrefix := "aws_dbe_"
   const BeaconPrefix := ReservedPrefix + "b_"
   const VersionPrefix := ReservedPrefix + "v_"
-  const MAX_ATTRIBUTE_COUNT := 100
+  const UINT32_MAX : uint32 := 0xFFFF_FFFF
 
   function method E(msg : string) : Error
   {
@@ -181,7 +181,8 @@ module DynamoDbItemEncryptorUtil {
       Success(value)
     else if legend == SE.LEGEND_BINARY then
       var terminal :- SE.DecodeTerminal(ecValue);
-      var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, false);
+      :- Need(|terminal.value| < UINT32_MAX as int, "LEGEND_BINARY too big");
+      var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint32));
       Success(ddbAttrValue.val)
     else
       Failure("Encryption Context Legend has unexpected character : '" + [legend] + "'.")
@@ -236,7 +237,8 @@ module DynamoDbItemEncryptorUtil {
 
     // Obtain attribute value from EC kvPair value
     var terminal :- SE.DecodeTerminal(encodedAttrValue);
-    var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, false);
+    :- Need(|terminal.value| < UINT32_MAX as int, "Attribute Value too big");
+    var ddbAttrValue :- DynamoToStruct.BytesToAttr(terminal.value, terminal.typeId, Some(|terminal.value| as uint32));
 
     // Add to our AttributeMap
     Success(attrMap[ddbAttrName := ddbAttrValue.val])
diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy
index 6ec3f8a4c..135216c36 100644
--- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy
+++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy
@@ -109,7 +109,6 @@ module DynamoDbItemEncryptorTest {
       "sign4" := DDB.AttributeValue.NULL(true),
       "nothing" := DDBS("baz")
     ];
-    var expectedOutputItem := inputItem["bar" := DDB.AttributeValue.N("1234")];
 
     var encryptRes := encryptor.EncryptItem(
       Types.EncryptItemInput(
@@ -122,7 +121,7 @@ module DynamoDbItemEncryptorTest {
     }
     expect encryptRes.Success?;
     expect encryptRes.value.encryptedItem.Keys == inputItem.Keys + {SE.HeaderField, SE.FooterField};
-    expect encryptRes.value.encryptedItem["bar"] == expectedOutputItem["bar"]; // because normalized
+    expect encryptRes.value.encryptedItem["bar"] == inputItem["bar"];
     expect encryptRes.value.encryptedItem["encrypt"] != inputItem["encrypt"];
     expect encryptRes.value.encryptedItem["sign"] == inputItem["sign"];
     expect encryptRes.value.encryptedItem["sign3"] == inputItem["sign3"];
@@ -142,11 +141,11 @@ module DynamoDbItemEncryptorTest {
       print "\n", decryptRes.error, "\n";
     }
     expect decryptRes.Success?;
-    if decryptRes.value.plaintextItem != expectedOutputItem {
-      print "\nexpectedOutputItem :\n", expectedOutputItem, "\n";
+    if decryptRes.value.plaintextItem != inputItem {
+      print "\ninputItem :\n", inputItem, "\n";
       print "\nOutput Item :\n", decryptRes.value.plaintextItem, "\n";
     }
-    expect decryptRes.value.plaintextItem == expectedOutputItem;
+    expect decryptRes.value.plaintextItem == inputItem;
 
     var parsedHeader := decryptRes.value.parsedHeader;
     expect parsedHeader.Some?;
@@ -605,10 +604,10 @@ module DynamoDbItemEncryptorTest {
     expect parsedHeader.value.selectorContext == map["bar" := DDB.AttributeValue.S("key")];
   }
 
-  method {:test} TestMaxRoundTrip() {
+  method {:test} TestLargeRoundTrip() {
     var inputItem : DDB.AttributeMap := map["bar" := DDBS("key")];
     var actions : DDBE.AttributeActions := map["bar" := CSE.SIGN_ONLY];
-    for i := 0 to (MAX_ATTRIBUTE_COUNT-1) {
+    for i := 0 to 500 {
       var str := String.Base10Int2String(i);
       expect DDB.IsValid_AttributeName(str);
       inputItem := inputItem[str := DDBS(str)];
@@ -649,26 +648,4 @@ module DynamoDbItemEncryptorTest {
     expect PublicKeyUtf8 in parsedHeader.value.storedEncryptionContext.Keys;
     expect |parsedHeader.value.encryptedDataKeys| == 1;
   }
-
-  method {:test} TestTooManyAttributes() {
-    var inputItem : DDB.AttributeMap := map["bar" := DDBS("key")];
-    var actions : DDBE.AttributeActions := map["bar" := CSE.SIGN_ONLY];
-    for i := 0 to MAX_ATTRIBUTE_COUNT {
-      var str := String.Base10Int2String(i);
-      expect DDB.IsValid_AttributeName(str);
-      inputItem := inputItem[str := DDBS(str)];
-      actions := actions[str := CSE.ENCRYPT_AND_SIGN];
-    }
-    var config := TestFixtures.GetEncryptorConfigFromActions(actions);
-    var encryptor := TestFixtures.GetDynamoDbItemEncryptorFrom(config);
-
-    var encryptRes := encryptor.EncryptItem(
-      Types.EncryptItemInput(
-        plaintextItem:=inputItem
-      )
-    );
-
-    expect encryptRes.Failure?;
-    expect encryptRes.error == E("Item to encrypt had 101 attributes, but maximum allowed is 100");
-  }
 }
diff --git a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy
index e751c291d..5211ebc03 100644
--- a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy
@@ -111,12 +111,9 @@ module {:options "-functionSyntax:4"} DecryptManifest {
     }
   }
 
-  function LogFileName() : string
+  function LogFileName() : Option<string>
   {
-    if OsLang.GetOsShort() == "Windows" && OsLang.GetLanguageShort() == "Dotnet" then
-      "..\\..\\PerfLog.txt"
-    else
-      "../../PerfLog.txt"
+    Some("../../PerfLog.txt")
   }
 
   method Decrypt(inFile : string, keyVectors: KeyVectors.KeyVectorsClient)
@@ -182,7 +179,7 @@ module {:options "-functionSyntax:4"} DecryptManifest {
       :- Need(obj.1.Object?, "Value of test '" + obj.0 + "' must be an Object.");
       var _ :- OneTest(obj.0, obj.1, keyVectors);
     }
-    Time.PrintTimeSinceLong(time, "DB-ESDK-TV-Decrypt-" + inFile, Some(LogFileName()));
+    Time.PrintTimeSinceLong(time, "DB-ESDK-TV-Decrypt-" + inFile, LogFileName());
 
     timeStamp :- expect Time.GetCurrentTimeStamp();
     print timeStamp + " Tests Complete.\n";
diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy
index b15ceddac..e2e5a407d 100644
--- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy
@@ -48,7 +48,6 @@ module {:options "-functionSyntax:4"} JsonConfig {
 
   datatype LargeRecord = LargeRecord (
     name : string,
-    count : nat,
     item : DDB.AttributeMap
   )
 
@@ -1433,25 +1432,18 @@ module {:options "-functionSyntax:4"} JsonConfig {
   method GetLarge(name : string, data : JSON) returns (output : Result<LargeRecord, string>)
   {
     :- Need(data.Object?, "LargeRecord must be a JSON object.");
-    var count := 0;
     var item : DDB.AttributeMap := map[];
     for i := 0 to |data.obj| {
       var obj := data.obj[i];
       match obj.0 {
-        case "Count" =>
-          :- Need(obj.1.Number?, "GetPrefix length must be a number");
-          count :- DecimalToInt(obj.1.num);
         case "Item" => var src :- JsonToDdbItem(obj.1); item := src;
         case _ => return Failure("Unexpected part of a LargeRecord : '" + obj.0 + "'");
       }
     }
-    if (count <= 0) {
-      return Failure("Missing or invalid Count in LargeRecord : '" + name + "'");
-    }
     if (|item| == 0) {
       return Failure("Missing or Empty LargeRecord : '" + name + "'");
     }
-    var record := LargeRecord(name, count, item);
+    var record := LargeRecord(name, item);
     return Success(record);
   }
 
diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
index 947fd4489..ba6588ca5 100644
--- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
+++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -13,7 +13,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
   import opened Wrappers
   import opened StandardLibrary
   import opened StandardLibrary.UInt
-  import opened StandardLibrary.String
   import JSON.API
   import opened JSON.Values
   import JSON.Errors
@@ -46,7 +45,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
   import TransOp = AwsCryptographyDbEncryptionSdkDynamoDbTransformsOperations
   import DdbMiddlewareConfig
   import DynamoDbEncryptionTransforms
+  import OsLang
 
+  const PerfIterations : uint32 := 1000
 
   datatype TestVectorConfig = TestVectorConfig (
     schemaOnEncrypt : DDB.CreateTableInput,
@@ -109,12 +110,6 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         return;
       }
       Validate();
-      // Because of Dafny-Rust's lack of modules, there is no way to mae an interceptor for the wrapped DB-ESDK client.
-      // So we create runtimes/rust/SkipLocal.txt to skip those tests that need the wrapped client.
-      var skipLocal := FileIO.ReadBytesFromFile("SkipLocal.txt");
-      if skipLocal.Success? {
-        return;
-      }
       StringOrdering();
       LargeTests();
       BasicIoTest();
@@ -554,25 +549,23 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
       }
 
       var time := Time.GetAbsoluteTime();
-      for i := 0 to record.count {
+      for i : uint32 := 0 to PerfIterations {
         var put_input_input := Trans.PutItemInputTransformInput ( sdkInput := DDB.PutItemInput (TableName := TableName, Item := record.item));
         var put_input_output :- expect client.PutItemInputTransform(put_input_input);
       }
-      var elapsed := Time.TimeSince(time);
-      Time.PrintTimeLong(elapsed, "Large Encrypt " + record.name + "(" + Base10Int2String(record.count) + ") " + config);
+      Time.PrintTimeSinceLong(time, "Large Encrypt " + record.name + " " + config, DecryptManifest.LogFileName());
 
       var put_input_input := Trans.PutItemInputTransformInput ( sdkInput := DDB.PutItemInput (TableName := TableName, Item := record.item));
       var put_input_output :- expect client.PutItemInputTransform(put_input_input);
       time := Time.GetAbsoluteTime();
-      for i := 0 to record.count {
+      for i : uint32 := 0 to PerfIterations {
         var orig_get_input := DDB.GetItemInput(TableName := TableName, Key := map[]);
         var get_output := DDB.GetItemOutput(Item := Some(put_input_output.transformedInput.Item));
         var trans_get_input := Trans.GetItemOutputTransformInput(sdkOutput := get_output, originalInput := orig_get_input);
         var put_output :- expect client.GetItemOutputTransform(trans_get_input);
 
       }
-      elapsed := Time.TimeSince(time);
-      Time.PrintTimeLong(elapsed, "Large Decrypt " + record.name + "(" + Base10Int2String(record.count) + ") " + config);
+      Time.PrintTimeSinceLong(time, "Large Decrypt " + record.name + " " + config, DecryptManifest.LogFileName());
     }
 
     method RoundTripTests()
diff --git a/TestVectors/runtimes/java/large_records.json b/TestVectors/runtimes/java/large_records.json
index 395d0a687..0f55f68a5 100644
--- a/TestVectors/runtimes/java/large_records.json
+++ b/TestVectors/runtimes/java/large_records.json
@@ -846,14 +846,12 @@
   },
   "Large": {
     "tiny": {
-      "Count": 1000,
       "Item": {
         "PK": "012345678900123456789001234567890",
         "00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": "AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA"
       }
     },
     "flat": {
-      "Count": 1000,
       "Item": {
         "PK": "012345678900123456789001234567890",
         "00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": "AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
@@ -956,8 +954,7 @@
         "97AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": "AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA"
       }
     },
-    "nested_one": {
-      "Count": 1000,
+    "nested_map": {
       "Item": {
         "PK": "012345678900123456789001234567890",
         "00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": {
@@ -1063,6 +1060,113 @@
           }
         }
       }
+    },
+    "nested_list": {
+      "Item": {
+        "PK": "012345678900123456789001234567890",
+        "00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA": {
+          "L": [
+            "00AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "01AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "02AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "03AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "04AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "05AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "06AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "07AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "08AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "09AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "10AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "11AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "12AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "13AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "14AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "15AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "16AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "17AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "18AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "19AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "20AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "21AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "22AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "23AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "24AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "25AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "26AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "27AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "28AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "29AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "30AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "31AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "32AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "33AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "34AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "35AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "36AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "37AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "38AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "39AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "40AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "41AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "42AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "43AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "44AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "45AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "46AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "47AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "48AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "49AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "50AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "51AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "52AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "53AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "54AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "55AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "56AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "57AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "58AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "59AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "60AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "61AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "62AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "63AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "64AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "65AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "66AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "67AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "68AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "69AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "70AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "71AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "72AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "73AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "74AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "75AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "76AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "77AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "78AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "79AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "80AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "81AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "82AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "83AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "84AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "85AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "86AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "87AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "88AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "89AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "90AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "91AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "92AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "93AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "94AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "95AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "96AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA",
+            "97AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA"
+          ]
+        }
+      }
     }
   }
 }