Merge branch 'main' into ajewell/bump-mpl2

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

@@ -596,7 +596,7 @@ module DynamoToStruct {
     ensures ret.Success? ==> |ret.value| == LENGTH_LEN
     ensures ret == U32ToBigEndian(x as nat)
   {
-    if x > 0xffff_ffff then
+    if !HasUint32Size(x) then
       Failure("Length was too big")
     else
       Success(UInt32ToSeq(x as uint32))

DynamoDbEncryption/dafny/DynamoDbEncryption/src/TermLoc.dfy

@@ -32,39 +32,12 @@ module TermLoc {
   import Seq
   import DynamoToStruct
 
-  // function method {:tailrecursion} CountEven(x : seq<uint8>, pos : nat) : nat
-  //   requires pos <= |x|
-  //   decreases |x| - pos
-  // {
-  //   if pos == |x| then
-  //     0
-  //   else if x[0] % 2 == 0 then
-  //     1 + CountEven(x, pos+1)
-  //   else
-  //     CountEven(x, pos+1)
-  // }
-
-  function method {:tailrecursion} CountEven(x : seq<uint8>, pos : uint64 := 0) : (ret : uint64)
-    requires pos as nat <= |x|
-    ensures ret as nat <= |x| - pos as nat
-    decreases |x| - pos as nat
-  {
-    SequenceIsSafeBecauseItIsInMemory(x);
-    if pos == |x| as uint64 then
-      0
-    else if x[0] % 2 == 0 then
-      1 + CountEven(x, pos+1)
-    else
-      CountEven(x, pos+1)
-  }
-
   datatype Selector =
     | List(pos : uint64)
     | 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),
@@ -73,7 +46,6 @@ module TermLoc {
   predicate method ValidTermLoc(s : seq<Selector>)
   {
     && 0 < |s|
-    && HasUint64Len(s)
     && s[0].Map?
   }
 
@@ -265,8 +237,9 @@ module TermLoc {
     if s[|s|-1] != ']' then
       Failure(E("List index must end with ]"))
     else
-      var num : uint64 :- GetNumber(s[1..|s|-1]);
-      Success(List(num))
+      var num :- GetNumber(s[1..|s|-1]);
+      :- Need(num < UINT64_LIMIT, E("Array selector exceeds maximum."));
+      Success(List(num as uint64))
   }
 
   // convert string to SelectorList

DynamoDbEncryption/dafny/StructuredEncryption/src/AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations.dfy

@@ -824,8 +824,8 @@ module AwsCryptographyDbEncryptionSdkStructuredEncryptionOperations refines Abst
       cmm,
       Some(encryptionContext),
       input.algorithmSuiteId,
-      CountEncrypted(canonData),
-      SumValueSize(canonData));
+      CountEncrypted(canonData) as nat,
+      SumValueSize(canonData) as nat);
 
     var key : Key := mat.plaintextDataKey.value;
     var alg := mat.algorithmSuite;

DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy

@@ -14,7 +14,6 @@ module StructuredEncryptionHeader {
   import opened AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes
   import opened StructuredEncryptionUtil
   import opened StandardLibrary.MemoryMath
-
   import CMP = AwsCryptographyMaterialProvidersTypes
   import Prim = AwsCryptographyPrimitivesTypes
   import SortedSets
@@ -617,6 +616,7 @@ module StructuredEncryptionHeader {
       Success(deserialized)
     else
       :- 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.