m

ajewellamz · ajewellamz · commit 10a5068e19a7 · 2025-03-23T18:03:44.000-04:00
diff --git a/.github/workflows/ci_codegen.yml b/.github/workflows/ci_codegen.yml
@@ -39,7 +39,7 @@ jobs:
       # and to translate version strings such as "nightly-latest"
       # to an actual DAFNY_VERSION.
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/ci_examples_java.yml b/.github/workflows/ci_examples_java.yml
@@ -53,7 +53,7 @@ jobs:
           java-version: ${{ matrix.java-version }}
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/ci_examples_net.yml b/.github/workflows/ci_examples_net.yml
@@ -46,7 +46,7 @@ jobs:
           dotnet-version: ${{ matrix.dotnet-version }}
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/ci_test_java.yml b/.github/workflows/ci_test_java.yml
@@ -47,7 +47,7 @@ jobs:
           submodules: recursive
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/ci_test_latest_released_mpl_java.yml b/.github/workflows/ci_test_latest_released_mpl_java.yml
@@ -54,7 +54,7 @@ jobs:
           java-version: ${{ matrix.java-version }}
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ needs.getVersion.outputs.version }}
 
diff --git a/.github/workflows/ci_test_net.yml b/.github/workflows/ci_test_net.yml
@@ -47,7 +47,7 @@ jobs:
           dotnet-version: ${{ matrix.dotnet-version }}
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/ci_test_vector_java.yml b/.github/workflows/ci_test_vector_java.yml
@@ -56,7 +56,7 @@ jobs:
           submodules: recursive
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/ci_test_vector_net.yml b/.github/workflows/ci_test_vector_net.yml
@@ -52,7 +52,7 @@ jobs:
           submodules: recursive
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/dafny_interop_examples_java.yml b/.github/workflows/dafny_interop_examples_java.yml
@@ -47,7 +47,7 @@ jobs:
           fetch-depth: 0
 
       - name: Setup MPL Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.mpl-dafny }}
 
@@ -73,7 +73,7 @@ jobs:
           make build_java CORES=$CORES
 
       - name: Setup DBESDK Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dbesdk-dafny}}
 
diff --git a/.github/workflows/dafny_interop_examples_net.yml b/.github/workflows/dafny_interop_examples_net.yml
@@ -47,7 +47,7 @@ jobs:
           dotnet-version: ${{ matrix.dotnet-version }}
 
       - name: Setup MPL Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.mpl-dafny }}
 
@@ -80,7 +80,7 @@ jobs:
           make transpile_net CORES=$CORES
 
       - name: Setup DBESDK Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dbesdk-dafny}}
 
diff --git a/.github/workflows/dafny_interop_java.yml b/.github/workflows/dafny_interop_java.yml
@@ -47,7 +47,7 @@ jobs:
           fetch-depth: 0
 
       - name: Setup MPL Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.mpl-dafny }}
 
@@ -73,7 +73,7 @@ jobs:
           make build_java CORES=$CORES
 
       - name: Setup DBESDK Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dbesdk-dafny}}
 
diff --git a/.github/workflows/dafny_interop_test_net.yml b/.github/workflows/dafny_interop_test_net.yml
@@ -47,7 +47,7 @@ jobs:
           dotnet-version: ${{ matrix.dotnet-version }}
 
       - name: Setup MPL Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.mpl-dafny }}
 
@@ -80,7 +80,7 @@ jobs:
           make transpile_net CORES=$CORES
 
       - name: Setup DBESDK Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dbesdk-dafny}}
 
diff --git a/.github/workflows/dafny_interop_test_vector_java.yml b/.github/workflows/dafny_interop_test_vector_java.yml
@@ -56,7 +56,7 @@ jobs:
           fetch-depth: 0
 
       - name: Setup MPL Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.mpl-dafny }}
 
@@ -83,7 +83,7 @@ jobs:
           make mvn_local_deploy
 
       - name: Setup DBESDK Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dbesdk-dafny}}
 
diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml
@@ -52,7 +52,7 @@ jobs:
           dotnet-version: ${{ matrix.dotnet-version }}
 
       - name: Setup MPL Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.mpl-dafny }}
 
@@ -85,7 +85,7 @@ jobs:
           make transpile_net CORES=$CORES
 
       - name: Setup DBESDK Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dbesdk-dafny}}
 
diff --git a/.github/workflows/library_dafny_verification.yml b/.github/workflows/library_dafny_verification.yml
@@ -53,7 +53,7 @@ jobs:
           submodules: recursive
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/library_format.yml b/.github/workflows/library_format.yml
@@ -37,7 +37,7 @@ jobs:
           submodules: recursive
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/.github/workflows/library_rust_tests.yml b/.github/workflows/library_rust_tests.yml
@@ -68,7 +68,7 @@ jobs:
           components: rustfmt
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: nightly-2025-01-30-7db1e5f
 
diff --git a/.github/workflows/test_vector_verification.yml b/.github/workflows/test_vector_verification.yml
@@ -43,7 +43,7 @@ jobs:
           submodules: recursive
 
       - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.8.0
+        uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
         with:
           dafny-version: ${{ inputs.dafny }}
 
diff --git a/DynamoDbEncryption/runtimes/rust/examples/clientsupplier/regional_role_client_supplier.rs b/DynamoDbEncryption/runtimes/rust/examples/clientsupplier/regional_role_client_supplier.rs
@@ -35,7 +35,7 @@ impl ClientSupplier for RegionalRoleClientSupplier {
 
         let sdk_config = tokio::task::block_in_place(|| {
             tokio::runtime::Handle::current().block_on(async {
-                aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await
+                aws_config::load_defaults(aws_config::BehaviorVersion::latest()).await
             })
         });
         let kms_config = aws_sdk_kms::config::Builder::from(&sdk_config)
diff --git a/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy b/TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy
@@ -127,8 +127,7 @@ module {:options "-functionSyntax:4"} DecryptManifest {
   {
     var timeStamp :- expect Time.GetCurrentTimeStamp();
     print timeStamp + " Decrypt : ", inFile, "\n";
-    var configBv :- expect FileIO.ReadBytesFromFile(inFile);
-    var configBytes := BvToBytes(configBv);
+    var configBytes :- expect FileIO.ReadBytesFromFile(inFile);
     timeStamp :- expect Time.GetCurrentTimeStamp();
     print timeStamp + " File Read.\n";
     var json :- expect API.Deserialize(configBytes);
diff --git a/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy b/TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy
@@ -151,8 +151,7 @@ module {:options "-functionSyntax:4"} EncryptManifest {
   {
     var timeStamp :- expect Time.GetCurrentTimeStamp();
     print timeStamp + " Encrypt : ", inFile, "\n";
-    var configBv :- expect FileIO.ReadBytesFromFile(inFile);
-    var configBytes := BvToBytes(configBv);
+    var configBytes :- expect FileIO.ReadBytesFromFile(inFile);
     timeStamp :- expect Time.GetCurrentTimeStamp();
     print timeStamp + " File Read.\n";
     var json :- expect API.Deserialize(configBytes);
@@ -212,8 +211,7 @@ module {:options "-functionSyntax:4"} EncryptManifest {
 
     var final := Object(result + [("tests", Object(test))]);
     var jsonBytes :- expect API.Serialize(final);
-    var jsonBv := BytesBv(jsonBytes);
-    var x :- expect FileIO.WriteBytesToFile(outFile, jsonBv);
+    var x :- expect FileIO.WriteBytesToFile(outFile, jsonBytes);
 
     timeStamp :- expect Time.GetCurrentTimeStamp();
     print timeStamp + " Tests Complete.\n";
diff --git a/TestVectors/dafny/DDBEncryption/src/Index.dfy b/TestVectors/dafny/DDBEncryption/src/Index.dfy
@@ -26,13 +26,12 @@ module WrappedDDBEncryptionMain {
     modifies keyVectors.Modifies
     ensures keyVectors.ValidState()
   {
-    var configBv := FileIO.ReadBytesFromFile(file);
-    if configBv.Failure? {
+    var configBytes := FileIO.ReadBytesFromFile(file);
+    if configBytes.Failure? {
       print "Failed to open ", file, " continuing anyway.\n";
       return Success(MakeEmptyTestVector());
     }
-    var configBytes := BvToBytes(configBv.value);
-    var json :- expect API.Deserialize(configBytes);
+    var json :- expect API.Deserialize(configBytes.value);
     output := ParseTestVector(json, prev, keyVectors);
     if output.Failure? {
       print output.error, "\n";
diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy
@@ -560,8 +560,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
         jsonItems := jsonItems + [item];
       }
       var jsonBytes :- expect API.Serialize(Array(jsonItems));
-      var jsonBv := BytesBv(jsonBytes);
-      var x := FileIO.WriteBytesToFile(fileName, jsonBv);
+      var x := FileIO.WriteBytesToFile(fileName, jsonBytes);
       expect x.Success?;
     }
 
diff --git a/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy b/TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy
@@ -401,8 +401,7 @@ module {:options "-functionSyntax:4"} WriteManifest {
     var final := Object(result + [("tests", Object(tests))]);
 
     var jsonBytes :- expect API.Serialize(final);
-    var jsonBv := BytesBv(jsonBytes);
-    var x := FileIO.WriteBytesToFile(fileName, jsonBv);
+    var x := FileIO.WriteBytesToFile(fileName, jsonBytes);
     expect x.Success?;
     return Success(true);
   }
diff --git a/TestVectors/dafny/DDBEncryption/src/WriteSetPermutations.dfy b/TestVectors/dafny/DDBEncryption/src/WriteSetPermutations.dfy
@@ -117,11 +117,6 @@ module {:options "-functionSyntax:4"} WriteSetPermutations {
     return recs1 + recs2 + recs3 + recs4;
   }
 
-  function BytesBv(bits: seq<BoundedInts.uint8>): seq<bv8>
-  {
-    seq(|bits|, i requires 0 <= i < |bits| => bits[i] as bv8)
-  }
-
   method WriteSetPermutations()
   {
     var configs := GetConfigs();
@@ -132,11 +127,10 @@ module {:options "-functionSyntax:4"} WriteSetPermutations {
                           ]))]);
 
     var jsonBytes :- expect API.Serialize(whole);
-    var jsonBv := BytesBv(jsonBytes);
 
     var _ :- expect FileIO.WriteBytesToFile(
       "PermTest.json",
-      jsonBv
+      jsonBytes
     );
   }
 }
diff --git a/TestVectors/runtimes/rust/src/create_client.rs b/TestVectors/runtimes/rust/src/create_client.rs
@@ -27,7 +27,7 @@ impl _CreateInterceptedDDBClient_Compile::_default {
 
     let table_configs = crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_transforms::conversions::dynamo_db_tables_encryption_config::_dynamo_db_tables_encryption_config::plain_from_dafny(config);
     let shared_config = DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults(
-      aws_config::BehaviorVersion::v2024_03_28()));
+      aws_config::BehaviorVersion::latest()));
 
       let shared_config = shared_config
         .to_builder()
@@ -49,7 +49,7 @@ impl _CreateInterceptedDDBClient_Compile::_default {
   -> Rc<_Wrappers_Compile::Result<Object<dyn IDynamoDBClient>, Rc<Error>>>
   {
     let shared_config = DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults(
-            aws_config::BehaviorVersion::v2024_03_28()));
+            aws_config::BehaviorVersion::latest()));
 
     let shared_config = shared_config
         .to_builder()
diff --git a/releases/rust/db_esdk/examples/clientsupplier/regional_role_client_supplier.rs b/releases/rust/db_esdk/examples/clientsupplier/regional_role_client_supplier.rs
@@ -35,7 +35,7 @@ impl ClientSupplier for RegionalRoleClientSupplier {
 
         let sdk_config = tokio::task::block_in_place(|| {
             tokio::runtime::Handle::current().block_on(async {
-                aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await
+                aws_config::load_defaults(aws_config::BehaviorVersion::latest()).await
             })
         });
         let kms_config = aws_sdk_kms::config::Builder::from(&sdk_config)
diff --git a/releases/rust/db_esdk/src/ddb.rs b/releases/rust/db_esdk/src/ddb.rs
@@ -30,11 +30,11 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny:
         let shared_config = match tokio::runtime::Handle::try_current() {
             Ok(curr) => tokio::task::block_in_place(|| {
                 curr.block_on(async {
-                    aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await
+                    aws_config::load_defaults(aws_config::BehaviorVersion::latest()).await
                 })
             }),
             Err(_) => DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults(
-                aws_config::BehaviorVersion::v2024_03_28(),
+                aws_config::BehaviorVersion::latest(),
             )),
         };
         let shared_config = shared_config
@@ -58,11 +58,11 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny:
         let shared_config = match tokio::runtime::Handle::try_current() {
             Ok(curr) => tokio::task::block_in_place(|| {
                 curr.block_on(async {
-                    aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await
+                    aws_config::load_defaults(aws_config::BehaviorVersion::latest()).await
                 })
             }),
             Err(_) => DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults(
-                aws_config::BehaviorVersion::v2024_03_28(),
+                aws_config::BehaviorVersion::latest(),
             )),
         };
         let inner = aws_sdk_dynamodb::Client::new(&shared_config);
diff --git a/releases/rust/db_esdk/src/kms.rs b/releases/rust/db_esdk/src/kms.rs
@@ -26,11 +26,11 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def
         let shared_config = match tokio::runtime::Handle::try_current() {
             Ok(curr) => tokio::task::block_in_place(|| {
                 curr.block_on(async {
-                    aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await
+                    aws_config::load_defaults(aws_config::BehaviorVersion::latest()).await
                 })
             }),
             Err(_) => DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults(
-                aws_config::BehaviorVersion::v2024_03_28(),
+                aws_config::BehaviorVersion::latest(),
             )),
         };
 
@@ -51,11 +51,11 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def
         let shared_config = match tokio::runtime::Handle::try_current() {
             Ok(curr) => tokio::task::block_in_place(|| {
                 curr.block_on(async {
-                    aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await
+                    aws_config::load_defaults(aws_config::BehaviorVersion::latest()).await
                 })
             }),
             Err(_) => DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults(
-                aws_config::BehaviorVersion::v2024_03_28(),
+                aws_config::BehaviorVersion::latest(),
             )),
         };
 
diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders
