Merge branch 'main' into primitives-name

Author: lucasmcdonald3

.github/actions/polymorph_codegen/action.yml

@@ -97,6 +97,11 @@ runs:
       run: |
         echo "PROJECT_DEPENDENCIES=${{ inputs.update-and-regenerate-mpl != 'true' && 'PROJECT_DEPENDENCIES=' || '' }}" >> $GITHUB_OUTPUT
 
+    - name: Print dotnet version
+      shell: bash
+      run: |
+        dotnet --version
+
     - name: Regenerate Dafny code using smithy-dafny
       # Unfortunately Dafny codegen doesn't work on Windows:
       # https://github.com/smithy-lang/smithy-dafny/issues/317

.github/workflows/ci_codegen.yml

@@ -48,6 +48,9 @@ jobs:
         with:
           dotnet-version: ${{ matrix.dotnet-version }}
 
+      - name: Create temporary global.json
+        run: echo '{"sdk":{"rollForward":"latestFeature","version":"6.0.0"}}' > ./global.json
+
       - name: Setup Java 17 for codegen
         uses: actions/setup-java@v3
         with:

DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy

@@ -248,6 +248,11 @@ module SearchableEncryptionInfo {
       assume {:axiom} cache.Modifies == {};
       var getCacheOutput := cache.GetCacheEntry(getCacheInput);
 
+      // If error is not EntryDoesNotExist, return failure
+      if (getCacheOutput.Failure? && !getCacheOutput.error.EntryDoesNotExist?) {
+        return Failure(AwsCryptographyMaterialProviders(AwsCryptographyMaterialProviders:=getCacheOutput.error));
+      }
+
       if getCacheOutput.Failure? {
         //= specification/searchable-encryption/search-config.md#beacon-keys
         //# Beacon keys MUST be obtained from the configured [Beacon Key Source](#beacon-key-source).
@@ -280,7 +285,11 @@ module SearchableEncryptionInfo {
 
         verifyValidStateCache(cache);
         assume {:axiom} cache.Modifies == {};
-        var _ := cache.PutCacheEntry(putCacheEntryInput);
+
+        var putResult := cache.PutCacheEntry(putCacheEntryInput);
+        if (putResult.Failure? && !putResult.error.EntryAlreadyExists?) {
+          return Failure(AwsCryptographyMaterialProviders(AwsCryptographyMaterialProviders:=putResult.error));
+        }
         return Success(keyMap);
       } else {
         :- Need(

project.properties

@@ -3,4 +3,4 @@ mplDependencyJavaVersion=1.7.0
 dafnyVersion=4.8.0
 dafnyVerifyVersion=4.8.0
 dafnyRuntimeJavaVersion=4.8.0
-smithyDafnyJavaConversionVersion=0.1
+smithyDafnyJavaConversionVersion=0.1.1