feat: bump dafny verification and code gen to dafny 4.8.0 (#520)

Co-authored-by: Robin Salkeld <[email protected]>
aws · Sep 10, 2024 · e16539e · e16539e
1 parent 8a67843
commit e16539e
Show file tree

Hide file tree

Showing 59 changed files with 13,179 additions and 1,910 deletions.
diff --git a/AwsCryptographicMaterialProviders/.gitignore b/AwsCryptographicMaterialProviders/.gitignore
@@ -1,6 +1,8 @@
 TestResults
 ImplementationFromDafny.cs
 TestsFromDafny.cs
+ImplementationFromDafny-cs.dtr
+TestsFromDafny-cs.dtr
 
 **/bin
 **/obj

diff --git a/...terialProviders/codegen-patches/AwsCryptographicMaterialProviders/dafny/dafny-4.3.0.patch b/...terialProviders/codegen-patches/AwsCryptographicMaterialProviders/dafny/dafny-4.3.0.patch
diff --git a/...ptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy b/...ptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy
@@ -494,7 +494,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
           assert old@CAN_ADD(cache.Select(k)) != old@CAN_ADD(cache.Select(k'));
         }
       }
-
+      assert  (forall c <- queue.Items :: c.identifier in cache.Keys() && cache.Select(c.identifier) == c);
       assert Invariant();
     }
 

diff --git a/.../dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkMatchForDecrypt.dfy b/.../dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkMatchForDecrypt.dfy
@@ -86,6 +86,6 @@ module  AwsKmsMrkMatchForDecrypt {
           && m.value.service   == c.value.service
           && m.value.account   == c.value.account
           && m.value.resource  == c.value.resource
-             )
+        )
   {}
 }
diff --git a/AwsCryptographicMaterialProviders/project.properties b/AwsCryptographicMaterialProviders/project.properties
@@ -1,4 +1,4 @@
 # This file stores the top level dafny version information.
 # All elements of the project need to agree on this version.
-dafnyVersion=4.2.0
-dafnyRuntimeJavaVersion=4.2.0
+dafnyVersion=4.8.0
+dafnyRuntimeJavaVersion=4.8.0
diff --git a/...untimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/ToDafny.java b/...untimes/java/src/main/smithy-generated/software/amazon/cryptography/keystore/ToDafny.java
@@ -95,11 +95,14 @@ public static BeaconKeyMaterials BeaconKeyMaterials(
     beaconKey =
       Objects.nonNull(nativeValue.beaconKey())
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(TypeDescriptor.BYTE),
           software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence(
             nativeValue.beaconKey()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(TypeDescriptor.BYTE)
+        );
     Option<
       DafnyMap<
         ? extends DafnySequence<? extends Character>,
@@ -109,8 +112,19 @@ public static BeaconKeyMaterials BeaconKeyMaterials(
     hmacKeys =
       (Objects.nonNull(nativeValue.hmacKeys()) &&
           nativeValue.hmacKeys().size() > 0)
-        ? Option.create_Some(ToDafny.HmacKeyMap(nativeValue.hmacKeys()))
-        : Option.create_None();
+        ? Option.create_Some(
+          DafnyMap._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE)
+          ),
+          ToDafny.HmacKeyMap(nativeValue.hmacKeys())
+        )
+        : Option.create_None(
+          DafnyMap._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE)
+          )
+        );
     return new BeaconKeyMaterials(
       beaconKeyIdentifier,
       encryptionContext,
@@ -158,11 +172,14 @@ public static CreateKeyInput CreateKeyInput(
     branchKeyIdentifier =
       Objects.nonNull(nativeValue.branchKeyIdentifier())
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
           software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
             nativeValue.branchKeyIdentifier()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+        );
     Option<
       DafnyMap<
         ? extends DafnySequence<? extends Byte>,
@@ -173,9 +190,18 @@ public static CreateKeyInput CreateKeyInput(
       (Objects.nonNull(nativeValue.encryptionContext()) &&
           nativeValue.encryptionContext().size() > 0)
         ? Option.create_Some(
+          DafnyMap._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE),
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE)
+          ),
           ToDafny.EncryptionContext(nativeValue.encryptionContext())
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnyMap._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE),
+            DafnySequence._typeDescriptor(TypeDescriptor.BYTE)
+          )
+        );
     return new CreateKeyInput(branchKeyIdentifier, encryptionContext);
   }
 
@@ -328,37 +354,51 @@ public static KeyStoreConfig KeyStoreConfig(
     id =
       Objects.nonNull(nativeValue.id())
         ? Option.create_Some(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
           software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
             nativeValue.id()
           )
         )
-        : Option.create_None();
+        : Option.create_None(
+          DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+        );
     Option<
       DafnySequence<? extends DafnySequence<? extends Character>>
     > grantTokens;
     grantTokens =
       (Objects.nonNull(nativeValue.grantTokens()) &&
           nativeValue.grantTokens().size() > 0)
-        ? Option.create_Some(ToDafny.GrantTokenList(nativeValue.grantTokens()))
-        : Option.create_None();
+        ? Option.create_Some(
+          DafnySequence._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+          ),
+          ToDafny.GrantTokenList(nativeValue.grantTokens())
+        )
+        : Option.create_None(
+          DafnySequence._typeDescriptor(
+            DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
+          )
+        );
     Option<IDynamoDBClient> ddbClient;
     ddbClient =
       Objects.nonNull(nativeValue.ddbClient())
         ? Option.create_Some(
+          TypeDescriptor.reference(IDynamoDBClient.class),
           software.amazon.cryptography.services.dynamodb.internaldafny.ToDafny.DynamoDB_20120810(
             nativeValue.ddbClient()
           )
         )
-        : Option.create_None();
+        : Option.create_None(TypeDescriptor.reference(IDynamoDBClient.class));
     Option<IKMSClient> kmsClient;
     kmsClient =
       Objects.nonNull(nativeValue.kmsClient())
         ? Option.create_Some(
+          TypeDescriptor.reference(IKMSClient.class),
           software.amazon.cryptography.services.kms.internaldafny.ToDafny.TrentService(
             nativeValue.kmsClient()
           )
         )
-        : Option.create_None();
+        : Option.create_None(TypeDescriptor.reference(IKMSClient.class));
     return new KeyStoreConfig(
       ddbTableName,
       kmsConfiguration,

diff --git a/.../smithy-generated/software/amazon/cryptography/materialproviders/BranchKeyIdSupplier.java b/.../smithy-generated/software/amazon/cryptography/materialproviders/BranchKeyIdSupplier.java
@@ -99,9 +99,17 @@ > GetBranchKeyId(
           this._impl.GetBranchKeyId(nativeInput);
         software.amazon.cryptography.materialproviders.internaldafny.types.GetBranchKeyIdOutput dafnyOutput =
           ToDafny.GetBranchKeyIdOutput(nativeOutput);
-        return Result.create_Success(dafnyOutput);
+        return Result.create_Success(
+          software.amazon.cryptography.materialproviders.internaldafny.types.GetBranchKeyIdOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          dafnyOutput
+        );
       } catch (RuntimeException ex) {
-        return Result.create_Failure(ToDafny.Error(ex));
+        return Result.create_Failure(
+          software.amazon.cryptography.materialproviders.internaldafny.types.GetBranchKeyIdOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          ToDafny.Error(ex)
+        );
       }
     }
 

diff --git a/.../main/smithy-generated/software/amazon/cryptography/materialproviders/ClientSupplier.java b/.../main/smithy-generated/software/amazon/cryptography/materialproviders/ClientSupplier.java
@@ -4,6 +4,7 @@
 package software.amazon.cryptography.materialproviders;
 
 import Wrappers_Compile.Result;
+import dafny.TypeDescriptor;
 import java.lang.IllegalArgumentException;
 import java.lang.RuntimeException;
 import java.util.Objects;
@@ -93,9 +94,17 @@ public Result<IKMSClient, Error> GetClient(
         GetClientInput nativeInput = ToNative.GetClientInput(dafnyInput);
         KmsClient nativeOutput = this._impl.GetClient(nativeInput);
         IKMSClient dafnyOutput = new Shim(nativeOutput, null);
-        return Result.create_Success(dafnyOutput);
+        return Result.create_Success(
+          TypeDescriptor.reference(IKMSClient.class),
+          Error._typeDescriptor(),
+          dafnyOutput
+        );
       } catch (RuntimeException ex) {
-        return Result.create_Failure(ToDafny.Error(ex));
+        return Result.create_Failure(
+          TypeDescriptor.reference(IKMSClient.class),
+          Error._typeDescriptor(),
+          ToDafny.Error(ex)
+        );
       }
     }
 

diff --git a/...generated/software/amazon/cryptography/materialproviders/CryptographicMaterialsCache.java b/...generated/software/amazon/cryptography/materialproviders/CryptographicMaterialsCache.java
@@ -121,9 +121,17 @@ public Result<Tuple0, Error> DeleteCacheEntry(
           dafnyInput
         );
         this._impl.DeleteCacheEntry(nativeInput);
-        return Result.create_Success(Tuple0.create());
+        return Result.create_Success(
+          dafny.Tuple0._typeDescriptor(),
+          Error._typeDescriptor(),
+          Tuple0.create()
+        );
       } catch (RuntimeException ex) {
-        return Result.create_Failure(ToDafny.Error(ex));
+        return Result.create_Failure(
+          dafny.Tuple0._typeDescriptor(),
+          Error._typeDescriptor(),
+          ToDafny.Error(ex)
+        );
       }
     }
 
@@ -147,9 +155,17 @@ > GetCacheEntry(
           this._impl.GetCacheEntry(nativeInput);
         software.amazon.cryptography.materialproviders.internaldafny.types.GetCacheEntryOutput dafnyOutput =
           ToDafny.GetCacheEntryOutput(nativeOutput);
-        return Result.create_Success(dafnyOutput);
+        return Result.create_Success(
+          software.amazon.cryptography.materialproviders.internaldafny.types.GetCacheEntryOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          dafnyOutput
+        );
       } catch (RuntimeException ex) {
-        return Result.create_Failure(ToDafny.Error(ex));
+        return Result.create_Failure(
+          software.amazon.cryptography.materialproviders.internaldafny.types.GetCacheEntryOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          ToDafny.Error(ex)
+        );
       }
     }
 
@@ -170,9 +186,17 @@ public Result<Tuple0, Error> PutCacheEntry(
           dafnyInput
         );
         this._impl.PutCacheEntry(nativeInput);
-        return Result.create_Success(Tuple0.create());
+        return Result.create_Success(
+          dafny.Tuple0._typeDescriptor(),
+          Error._typeDescriptor(),
+          Tuple0.create()
+        );
       } catch (RuntimeException ex) {
-        return Result.create_Failure(ToDafny.Error(ex));
+        return Result.create_Failure(
+          dafny.Tuple0._typeDescriptor(),
+          Error._typeDescriptor(),
+          ToDafny.Error(ex)
+        );
       }
     }
 
@@ -189,9 +213,17 @@ public Result<Tuple0, Error> UpdateUsageMetadata(
         UpdateUsageMetadataInput nativeInput =
           ToNative.UpdateUsageMetadataInput(dafnyInput);
         this._impl.UpdateUsageMetadata(nativeInput);
-        return Result.create_Success(Tuple0.create());
+        return Result.create_Success(
+          dafny.Tuple0._typeDescriptor(),
+          Error._typeDescriptor(),
+          Tuple0.create()
+        );
       } catch (RuntimeException ex) {
-        return Result.create_Failure(ToDafny.Error(ex));
+        return Result.create_Failure(
+          dafny.Tuple0._typeDescriptor(),
+          Error._typeDescriptor(),
+          ToDafny.Error(ex)
+        );
       }
     }
 

diff --git a/...nerated/software/amazon/cryptography/materialproviders/CryptographicMaterialsManager.java b/...nerated/software/amazon/cryptography/materialproviders/CryptographicMaterialsManager.java
@@ -113,9 +113,17 @@ > DecryptMaterials(
           this._impl.DecryptMaterials(nativeInput);
         software.amazon.cryptography.materialproviders.internaldafny.types.DecryptMaterialsOutput dafnyOutput =
           ToDafny.DecryptMaterialsOutput(nativeOutput);
-        return Result.create_Success(dafnyOutput);
+        return Result.create_Success(
+          software.amazon.cryptography.materialproviders.internaldafny.types.DecryptMaterialsOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          dafnyOutput
+        );
       } catch (RuntimeException ex) {
-        return Result.create_Failure(ToDafny.Error(ex));
+        return Result.create_Failure(
+          software.amazon.cryptography.materialproviders.internaldafny.types.DecryptMaterialsOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          ToDafny.Error(ex)
+        );
       }
     }
 
@@ -141,9 +149,17 @@ > GetEncryptionMaterials(
           this._impl.GetEncryptionMaterials(nativeInput);
         software.amazon.cryptography.materialproviders.internaldafny.types.GetEncryptionMaterialsOutput dafnyOutput =
           ToDafny.GetEncryptionMaterialsOutput(nativeOutput);
-        return Result.create_Success(dafnyOutput);
+        return Result.create_Success(
+          software.amazon.cryptography.materialproviders.internaldafny.types.GetEncryptionMaterialsOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          dafnyOutput
+        );
       } catch (RuntimeException ex) {
-        return Result.create_Failure(ToDafny.Error(ex));
+        return Result.create_Failure(
+          software.amazon.cryptography.materialproviders.internaldafny.types.GetEncryptionMaterialsOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          ToDafny.Error(ex)
+        );
       }
     }
 

diff --git a/...ava/src/main/smithy-generated/software/amazon/cryptography/materialproviders/Keyring.java b/...ava/src/main/smithy-generated/software/amazon/cryptography/materialproviders/Keyring.java
@@ -102,9 +102,17 @@ > OnDecrypt(
         OnDecryptOutput nativeOutput = this._impl.OnDecrypt(nativeInput);
         software.amazon.cryptography.materialproviders.internaldafny.types.OnDecryptOutput dafnyOutput =
           ToDafny.OnDecryptOutput(nativeOutput);
-        return Result.create_Success(dafnyOutput);
+        return Result.create_Success(
+          software.amazon.cryptography.materialproviders.internaldafny.types.OnDecryptOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          dafnyOutput
+        );
       } catch (RuntimeException ex) {
-        return Result.create_Failure(ToDafny.Error(ex));
+        return Result.create_Failure(
+          software.amazon.cryptography.materialproviders.internaldafny.types.OnDecryptOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          ToDafny.Error(ex)
+        );
       }
     }
 
@@ -128,9 +136,17 @@ > OnEncrypt(
         OnEncryptOutput nativeOutput = this._impl.OnEncrypt(nativeInput);
         software.amazon.cryptography.materialproviders.internaldafny.types.OnEncryptOutput dafnyOutput =
           ToDafny.OnEncryptOutput(nativeOutput);
-        return Result.create_Success(dafnyOutput);
+        return Result.create_Success(
+          software.amazon.cryptography.materialproviders.internaldafny.types.OnEncryptOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          dafnyOutput
+        );
       } catch (RuntimeException ex) {
-        return Result.create_Failure(ToDafny.Error(ex));
+        return Result.create_Failure(
+          software.amazon.cryptography.materialproviders.internaldafny.types.OnEncryptOutput._typeDescriptor(),
+          Error._typeDescriptor(),
+          ToDafny.Error(ex)
+        );
       }
     }
-Original file line number
+Diff line change
@@ Expand Up / @@ -494,7 +494,7 @@ module {:options "/functionSyntax:4" } LocalCMC { @@
               assert old@CAN_ADD(cache.Select(k)) != old@CAN_ADD(cache.Select(k'));
             }
           }
+          assert  (forall c <- queue.Items :: c.identifier in cache.Keys() && cache.Select(c.identifier) == c);
           assert Invariant();
         }
@@ Expand Down @@