chore(MPL): update MPL submodule and update to Dafny 4.1.0 (#182)

Author: josecorella

.github/workflows/ci_examples_java.yml

@@ -90,7 +90,7 @@ jobs:
         uses: dafny-lang/[email protected]
         with:
           # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
-          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || 'nightly-2023-04-12-f4836e9' }}
+          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.1.0' }}
 
       - name: Build and locally deploy dependencies for examples
         shell: bash

.github/workflows/ci_test_java.yml

@@ -86,7 +86,7 @@ jobs:
         uses: dafny-lang/[email protected]
         with:
           # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
-          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || 'nightly-2023-04-12-f4836e9' }}
+          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.1.0' }}
 
       - name: Setup Java ${{ matrix.java-version }}
         uses: actions/setup-java@v3

.github/workflows/ci_test_net.yml

@@ -71,7 +71,7 @@ jobs:
         uses: dafny-lang/[email protected]
         with:
           # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
-          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || 'nightly-2023-04-12-f4836e9' }}
+          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.1.0' }}
 
       - name: Download Dependencies 
         working-directory: ./${{ matrix.library }}

.github/workflows/ci_verification.yml

@@ -61,7 +61,7 @@ jobs:
         uses: dafny-lang/[email protected]
         with:
           # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
-          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || 'nightly-2023-04-12-f4836e9' }}
+          dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.1.0' }}
 
       - name: Verify ${{ matrix.library }} Dafny code
         shell: bash

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

@@ -305,7 +305,5 @@ module BaseBeacon {
       && BytesToHex(bytes, 6) == "37"
       && BytesToHex(bytes, 7) == "37"
       && BytesToHex(bytes, 8) == "b7"
-      && BytesToHex(bytes, 9) == "1b7"
-      && BytesToHex(bytes, 10) == "3b7"
   {}
 }

DynamoDbEncryption/dafny/StructuredEncryption/src/Header.dfy

@@ -49,8 +49,8 @@ module StructuredEncryptionHeader {
   type CMPEncryptionContext  = x : CMP.EncryptionContext | ValidEncryptionContext(x) witness *
   type CMPEncryptedDataKeyListEmptyOK = x : seq<CMPEncryptedDataKey> | |x| < UINT8_LIMIT
   type LegendByte = x : uint8 | ValidLegendByte(x) witness SIGN_ONLY_LEGEND
-  type Legend = x : seq<LegendByte> | |x| < UINT16_LIMIT
-  type CMPUtf8Bytes = x : CMP.Utf8Bytes | |x| < UINT16_LIMIT
+  type Legend = x : seq<LegendByte> | |x| <= UINT16_LIMIT
+  type CMPUtf8Bytes = x : CMP.Utf8Bytes | |x| <= UINT16_LIMIT
 
   predicate method ValidVersion(x : uint8) {
     x == 1
@@ -73,15 +73,15 @@ module StructuredEncryptionHeader {
   }
 
   predicate method ValidEncryptionContext(x : CMP.EncryptionContext) {
-    && |x| < UINT16_LIMIT
-    && (forall k <- x :: |k| < UINT16_LIMIT && |x[k]| < UINT16_LIMIT)
+    && |x| <= UINT16_LIMIT
+    && (forall k <- x :: |k| <= UINT16_LIMIT && |x[k]| <= UINT16_LIMIT)
   }
 
   predicate method ValidEncryptedDataKey(x : CMP.EncryptedDataKey)
   {
-    && |x.keyProviderId| < UINT16_LIMIT
-    && |x.keyProviderInfo| < UINT16_LIMIT
-    && |x.ciphertext| < UINT16_LIMIT
+    && |x.keyProviderId| <= UINT16_LIMIT
+    && |x.keyProviderInfo| <= UINT16_LIMIT
+    && |x.ciphertext| <= UINT16_LIMIT
   }
 
   // header without commitment
@@ -331,9 +331,9 @@ module StructuredEncryptionHeader {
 
   function method ToUInt16(x : nat)
     : (ret : Result<uint16, Error>)
-    ensures x < UINT16_LIMIT ==> ret.Success?
+    ensures x <= UINT16_LIMIT ==> ret.Success?
   {
-    :- Need(x < UINT16_LIMIT, E("Value too big for 16 bits"));
+    :- Need(x <= UINT16_LIMIT, E("Value too big for 16 bits"));
     Success(x as uint16)
   }
 
@@ -408,7 +408,7 @@ module StructuredEncryptionHeader {
     if |attrs| == 0 then
       Success(serialized)
     else
-      :- Need((|serialized| + 1) < UINT16_LIMIT, E("Legend Too Long."));
+      :- Need((|serialized| + 1) <= UINT16_LIMIT, E("Legend Too Long."));
       :- Need(data[attrs[0]].content.Action?, E("Schema must be flat"));
       var legendChar := GetActionLegend(data[attrs[0]].content.Action);
       MakeLegend2(attrs[1..], data, serialized + [legendChar])
@@ -579,7 +579,7 @@ module StructuredEncryptionHeader {
     if count == 0 then
       Success(deserialized)
     else
-      :- Need(|deserialized.0| + 1  < UINT16_LIMIT, E("Too much context"));
+      :- Need(|deserialized.0| + 1  <= UINT16_LIMIT, E("Too much context"));
       var kv :- GetOneKVPair(data);
       //= specification/structured-encryption/header.md#key-value-pair-entries
       //# This sequence MUST NOT contain duplicate entries.
@@ -852,6 +852,13 @@ module StructuredEncryptionHeader {
       assert provIdSize + 2 < |data|;
       var provId := data[2..2+provIdSize];
       assert provId == k.keyProviderId;
+
+      var part1Size := 2 + provIdSize;
+      assert part1Size+2 <= |data|;
+      var provInfoSize := SeqToUInt16(data[part1Size..part1Size+2]) as nat;
+      assert part1Size + provInfoSize + 2 < |data|;
+      var provInfo := data[part1Size+2..part1Size+2+provInfoSize];
+      assert provInfo == k.keyProviderInfo;
     }
 
   // GetOneDataKey ==> SerializeOneDataKey

DynamoDbEncryption/runtimes/java/build.gradle.kts

@@ -64,7 +64,7 @@ repositories {
 val dynamodb by configurations.creating
 
 dependencies {
-    implementation("org.dafny:DafnyRuntime:4.0.0")
+    implementation("org.dafny:DafnyRuntime:4.1.0")
     implementation("software.amazon.dafny:conversion:1.0-SNAPSHOT")
     implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
     implementation("software.amazon.cryptography:AwsCryptographyPrimitives:1.0-SNAPSHOT")