fix: Re-Polymorph w/ Smithy-Dafny@3378be16 & fix Java Testing (#190)

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy

@@ -755,62 +755,62 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
   }
   datatype CreateAwsKmsDiscoveryKeyringInput = | CreateAwsKmsDiscoveryKeyringInput (
     nameonly kmsClient: ComAmazonawsKmsTypes.IKMSClient ,
-    nameonly discoveryFilter: Option<DiscoveryFilter> ,
-    nameonly grantTokens: Option<GrantTokenList>
+    nameonly discoveryFilter: Option<DiscoveryFilter> := Option.None ,
+    nameonly grantTokens: Option<GrantTokenList> := Option.None
   )
   datatype CreateAwsKmsDiscoveryMultiKeyringInput = | CreateAwsKmsDiscoveryMultiKeyringInput (
     nameonly regions: RegionList ,
-    nameonly discoveryFilter: Option<DiscoveryFilter> ,
-    nameonly clientSupplier: Option<IClientSupplier> ,
-    nameonly grantTokens: Option<GrantTokenList>
+    nameonly discoveryFilter: Option<DiscoveryFilter> := Option.None ,
+    nameonly clientSupplier: Option<IClientSupplier> := Option.None ,
+    nameonly grantTokens: Option<GrantTokenList> := Option.None
   )
   datatype CreateAwsKmsHierarchicalKeyringInput = | CreateAwsKmsHierarchicalKeyringInput (
-    nameonly branchKeyId: Option<string> ,
-    nameonly branchKeyIdSupplier: Option<IBranchKeyIdSupplier> ,
+    nameonly branchKeyId: Option<string> := Option.None ,
+    nameonly branchKeyIdSupplier: Option<IBranchKeyIdSupplier> := Option.None ,
     nameonly keyStore: AwsCryptographyKeyStoreTypes.IKeyStoreClient ,
     nameonly ttlSeconds: PositiveLong ,
-    nameonly cache: Option<CacheType>
+    nameonly cache: Option<CacheType> := Option.None
   )
   datatype CreateAwsKmsKeyringInput = | CreateAwsKmsKeyringInput (
     nameonly kmsKeyId: KmsKeyId ,
     nameonly kmsClient: ComAmazonawsKmsTypes.IKMSClient ,
-    nameonly grantTokens: Option<GrantTokenList>
+    nameonly grantTokens: Option<GrantTokenList> := Option.None
   )
   datatype CreateAwsKmsMrkDiscoveryKeyringInput = | CreateAwsKmsMrkDiscoveryKeyringInput (
     nameonly kmsClient: ComAmazonawsKmsTypes.IKMSClient ,
-    nameonly discoveryFilter: Option<DiscoveryFilter> ,
-    nameonly grantTokens: Option<GrantTokenList> ,
+    nameonly discoveryFilter: Option<DiscoveryFilter> := Option.None ,
+    nameonly grantTokens: Option<GrantTokenList> := Option.None ,
     nameonly region: Region
   )
   datatype CreateAwsKmsMrkDiscoveryMultiKeyringInput = | CreateAwsKmsMrkDiscoveryMultiKeyringInput (
     nameonly regions: RegionList ,
-    nameonly discoveryFilter: Option<DiscoveryFilter> ,
-    nameonly clientSupplier: Option<IClientSupplier> ,
-    nameonly grantTokens: Option<GrantTokenList>
+    nameonly discoveryFilter: Option<DiscoveryFilter> := Option.None ,
+    nameonly clientSupplier: Option<IClientSupplier> := Option.None ,
+    nameonly grantTokens: Option<GrantTokenList> := Option.None
   )
   datatype CreateAwsKmsMrkKeyringInput = | CreateAwsKmsMrkKeyringInput (
     nameonly kmsKeyId: KmsKeyId ,
     nameonly kmsClient: ComAmazonawsKmsTypes.IKMSClient ,
-    nameonly grantTokens: Option<GrantTokenList>
+    nameonly grantTokens: Option<GrantTokenList> := Option.None
   )
   datatype CreateAwsKmsMrkMultiKeyringInput = | CreateAwsKmsMrkMultiKeyringInput (
-    nameonly generator: Option<KmsKeyId> ,
-    nameonly kmsKeyIds: Option<KmsKeyIdList> ,
-    nameonly clientSupplier: Option<IClientSupplier> ,
-    nameonly grantTokens: Option<GrantTokenList>
+    nameonly generator: Option<KmsKeyId> := Option.None ,
+    nameonly kmsKeyIds: Option<KmsKeyIdList> := Option.None ,
+    nameonly clientSupplier: Option<IClientSupplier> := Option.None ,
+    nameonly grantTokens: Option<GrantTokenList> := Option.None
   )
   datatype CreateAwsKmsMultiKeyringInput = | CreateAwsKmsMultiKeyringInput (
-    nameonly generator: Option<KmsKeyId> ,
-    nameonly kmsKeyIds: Option<KmsKeyIdList> ,
-    nameonly clientSupplier: Option<IClientSupplier> ,
-    nameonly grantTokens: Option<GrantTokenList>
+    nameonly generator: Option<KmsKeyId> := Option.None ,
+    nameonly kmsKeyIds: Option<KmsKeyIdList> := Option.None ,
+    nameonly clientSupplier: Option<IClientSupplier> := Option.None ,
+    nameonly grantTokens: Option<GrantTokenList> := Option.None
   )
   datatype CreateAwsKmsRsaKeyringInput = | CreateAwsKmsRsaKeyringInput (
-    nameonly publicKey: Option<Secret> ,
+    nameonly publicKey: Option<Secret> := Option.None ,
     nameonly kmsKeyId: KmsKeyId ,
     nameonly encryptionAlgorithm: ComAmazonawsKmsTypes.EncryptionAlgorithmSpec ,
-    nameonly kmsClient: Option<ComAmazonawsKmsTypes.IKMSClient> ,
-    nameonly grantTokens: Option<GrantTokenList>
+    nameonly kmsClient: Option<ComAmazonawsKmsTypes.IKMSClient> := Option.None ,
+    nameonly grantTokens: Option<GrantTokenList> := Option.None
   )
   datatype CreateCryptographicMaterialsCacheInput = | CreateCryptographicMaterialsCacheInput (
     nameonly cache: CacheType
@@ -822,7 +822,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
     nameonly keyring: IKeyring
   )
   datatype CreateMultiKeyringInput = | CreateMultiKeyringInput (
-    nameonly generator: Option<IKeyring> ,
+    nameonly generator: Option<IKeyring> := Option.None ,
     nameonly childKeyrings: KeyringList
   )
   datatype CreateRawAesKeyringInput = | CreateRawAesKeyringInput (
@@ -835,12 +835,12 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
     nameonly keyNamespace: string ,
     nameonly keyName: string ,
     nameonly paddingScheme: PaddingScheme ,
-    nameonly publicKey: Option<seq<uint8>> ,
-    nameonly privateKey: Option<seq<uint8>>
+    nameonly publicKey: Option<seq<uint8>> := Option.None ,
+    nameonly privateKey: Option<seq<uint8>> := Option.None
   )
   datatype CreateRequiredEncryptionContextCMMInput = | CreateRequiredEncryptionContextCMMInput (
-    nameonly underlyingCMM: Option<ICryptographicMaterialsManager> ,
-    nameonly keyring: Option<IKeyring> ,
+    nameonly underlyingCMM: Option<ICryptographicMaterialsManager> := Option.None ,
+    nameonly keyring: Option<IKeyring> := Option.None ,
     nameonly requiredEncryptionContextKeys: EncryptionContextKeys
   )
   class ICryptographicMaterialsCacheCallHistory {
@@ -1128,16 +1128,16 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
     nameonly algorithmSuite: AlgorithmSuiteInfo ,
     nameonly encryptionContext: EncryptionContext ,
     nameonly requiredEncryptionContextKeys: EncryptionContextKeys ,
-    nameonly plaintextDataKey: Option<Secret> ,
-    nameonly verificationKey: Option<Secret> ,
-    nameonly symmetricSigningKey: Option<Secret>
+    nameonly plaintextDataKey: Option<Secret> := Option.None ,
+    nameonly verificationKey: Option<Secret> := Option.None ,
+    nameonly symmetricSigningKey: Option<Secret> := Option.None
   )
   datatype DecryptMaterialsInput = | DecryptMaterialsInput (
     nameonly algorithmSuiteId: AlgorithmSuiteId ,
     nameonly commitmentPolicy: CommitmentPolicy ,
     nameonly encryptedDataKeys: EncryptedDataKeyList ,
     nameonly encryptionContext: EncryptionContext ,
-    nameonly reproducedEncryptionContext: Option<EncryptionContext>
+    nameonly reproducedEncryptionContext: Option<EncryptionContext> := Option.None
   )
   datatype DecryptMaterialsOutput = | DecryptMaterialsOutput (
     nameonly decryptionMaterials: DecryptionMaterials
@@ -1180,9 +1180,9 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
     nameonly encryptionContext: EncryptionContext ,
     nameonly encryptedDataKeys: EncryptedDataKeyList ,
     nameonly requiredEncryptionContextKeys: EncryptionContextKeys ,
-    nameonly plaintextDataKey: Option<Secret> ,
-    nameonly signingKey: Option<Secret> ,
-    nameonly symmetricSigningKeys: Option<SymmetricSigningKeyList>
+    nameonly plaintextDataKey: Option<Secret> := Option.None ,
+    nameonly signingKey: Option<Secret> := Option.None ,
+    nameonly symmetricSigningKeys: Option<SymmetricSigningKeyList> := Option.None
   )
   datatype ESDKAlgorithmSuiteId =
     | ALG_AES_128_GCM_IV12_TAG16_NO_KDF
@@ -1208,7 +1208,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
   )
   datatype GetCacheEntryInput = | GetCacheEntryInput (
     nameonly identifier: seq<uint8> ,
-    nameonly bytesUsed: Option<int64>
+    nameonly bytesUsed: Option<int64> := Option.None
   )
   datatype GetCacheEntryOutput = | GetCacheEntryOutput (
     nameonly materials: Materials ,
@@ -1223,9 +1223,9 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
   datatype GetEncryptionMaterialsInput = | GetEncryptionMaterialsInput (
     nameonly encryptionContext: EncryptionContext ,
     nameonly commitmentPolicy: CommitmentPolicy ,
-    nameonly algorithmSuiteId: Option<AlgorithmSuiteId> ,
-    nameonly maxPlaintextLength: Option<int64> ,
-    nameonly requiredEncryptionContextKeys: Option<EncryptionContextKeys>
+    nameonly algorithmSuiteId: Option<AlgorithmSuiteId> := Option.None ,
+    nameonly maxPlaintextLength: Option<int64> := Option.None ,
+    nameonly requiredEncryptionContextKeys: Option<EncryptionContextKeys> := Option.None
   )
   datatype GetEncryptionMaterialsOutput = | GetEncryptionMaterialsOutput (
     nameonly encryptionMaterials: EncryptionMaterials
@@ -1249,8 +1249,8 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
     nameonly algorithmSuiteId: AlgorithmSuiteId ,
     nameonly encryptionContext: EncryptionContext ,
     nameonly requiredEncryptionContextKeys: EncryptionContextKeys ,
-    nameonly signingKey: Option<Secret> ,
-    nameonly verificationKey: Option<Secret>
+    nameonly signingKey: Option<Secret> := Option.None ,
+    nameonly verificationKey: Option<Secret> := Option.None
   )
   datatype IntermediateKeyWrapping = | IntermediateKeyWrapping (
     nameonly keyEncryptionKeyKdf: DerivationAlgorithm ,
@@ -1368,7 +1368,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
     | BeaconKey(BeaconKey: AwsCryptographyKeyStoreTypes.BeaconKeyMaterials)
   datatype MultiThreadedCache = | MultiThreadedCache (
     nameonly entryCapacity: CountingNumber ,
-    nameonly entryPruningTailSize: Option<CountingNumber>
+    nameonly entryPruningTailSize: Option<CountingNumber> := Option.None
   )
   datatype NoCache = | NoCache (
 
@@ -1408,8 +1408,8 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
     nameonly materials: Materials ,
     nameonly creationTime: PositiveLong ,
     nameonly expiryTime: PositiveLong ,
-    nameonly messagesUsed: Option<PositiveInteger> ,
-    nameonly bytesUsed: Option<PositiveInteger>
+    nameonly messagesUsed: Option<PositiveInteger> := Option.None ,
+    nameonly bytesUsed: Option<PositiveInteger> := Option.None
   )
   type Region = string
   type RegionList = seq<Region>
@@ -1419,11 +1419,11 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
     | None(None: None)
   datatype SingleThreadedCache = | SingleThreadedCache (
     nameonly entryCapacity: CountingNumber ,
-    nameonly entryPruningTailSize: Option<CountingNumber>
+    nameonly entryPruningTailSize: Option<CountingNumber> := Option.None
   )
   datatype StormTrackingCache = | StormTrackingCache (
     nameonly entryCapacity: CountingNumber ,
-    nameonly entryPruningTailSize: Option<CountingNumber> ,
+    nameonly entryPruningTailSize: Option<CountingNumber> := Option.None ,
     nameonly gracePeriod: CountingNumber ,
     nameonly graceInterval: CountingNumber ,
     nameonly fanOut: CountingNumber ,
@@ -1529,13 +1529,20 @@ abstract module AbstractAwsCryptographyMaterialProvidersService
   import Operations : AbstractAwsCryptographyMaterialProvidersOperations
   function method DefaultMaterialProvidersConfig(): MaterialProvidersConfig
   method MaterialProviders(config: MaterialProvidersConfig := DefaultMaterialProvidersConfig())
-    returns (res: Result<MaterialProvidersClient, Error>)
+    returns (res: Result<IAwsCryptographicMaterialProvidersClient, Error>)
     ensures res.Success? ==>
               && fresh(res.value)
               && fresh(res.value.Modifies)
               && fresh(res.value.History)
               && res.value.ValidState()
 
+  // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals
+  function method CreateSuccessOfClient(client: IAwsCryptographicMaterialProvidersClient): Result<IAwsCryptographicMaterialProvidersClient, Error> {
+    Success(client)
+  } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals
+  function method CreateFailureOfError(error: Error): Result<IAwsCryptographicMaterialProvidersClient, Error> {
+    Failure(error)
+  }
   class MaterialProvidersClient extends IAwsCryptographicMaterialProvidersClient
   {
     constructor(config: Operations.InternalConfig)

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy

@@ -10,20 +10,26 @@ module
 
   import Operations = AwsCryptographyMaterialProvidersOperations
   import Aws.Cryptography.Primitives
+  import Crypto = AwsCryptographyPrimitivesTypes
 
   function method DefaultMaterialProvidersConfig(): MaterialProvidersConfig
   {
     MaterialProvidersConfig
   }
 
   method MaterialProviders(config: MaterialProvidersConfig)
-    returns (res: Result<MaterialProvidersClient, Error>)
+    returns (res: Result<IAwsCryptographicMaterialProvidersClient, Error>)
+    ensures res.Success? ==>
+              && res.value is MaterialProvidersClient
   {
     var maybeCrypto := Primitives.AtomicPrimitives();
-    var crypto :- maybeCrypto
-    .MapFailure(e => AwsCryptographyPrimitives(e));
-    var client := new MaterialProvidersClient(Operations.Config( crypto := crypto ));
-    return Success(client);
+    var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto
+    .MapFailure(e => Types.AwsCryptographyPrimitives(e));
+    assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient;
+    var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient;
+
+    var client := new MaterialProvidersClient(Operations.Config( crypto := cryptoPrimitives ));
+    return Success(client as IAwsCryptographicMaterialProvidersClient);
   }
 
   class MaterialProvidersClient... {

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy

@@ -75,9 +75,10 @@ module IntermediateKeyWrapping {
 
   {
     var maybeCrypto := Primitives.AtomicPrimitives();
-    var cryptoPrimitives :- maybeCrypto
+    var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto
     .MapFailure(e => Types.AwsCryptographyPrimitives(e));
-
+    assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient;
+    var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient;
     // Deserialize the Intermediate-Wrapped material
     var deserializedWrapped :- DeserializeIntermediateWrappedMaterial(wrappedMaterial, algorithmSuite);
     var DeserializedIntermediateWrappedMaterial(encryptedPdk, providerWrappedIkm) := deserializedWrapped;
@@ -168,9 +169,13 @@ module IntermediateKeyWrapping {
            (AlgorithmSuites.GetEncryptKeyLength(algorithmSuite) + AlgorithmSuites.GetEncryptTagLength(algorithmSuite)) as nat
   {
     var maybeCrypto := Primitives.AtomicPrimitives();
-    var cryptoPrimitives :- maybeCrypto
+    var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto
     .MapFailure(e => Types.AwsCryptographyPrimitives(e));
 
+    assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient;
+    var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient;
+
+
     // Use the provider to get the intermediate key material, and wrapped intermediate key material
     var generateAndWrapOutput :- generateAndWrap.Invoke(
       GenerateAndWrapInput(

AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy

@@ -693,14 +693,16 @@ module AwsKmsHierarchicalKeyring {
       // We need to create a new client here so that we can reason about the state of the client
       // down the line. This is ok because the only state tracked is the client's history.
       var maybeCrypto := Primitives.AtomicPrimitives();
-      var crypto :- maybeCrypto
+      var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto
       .MapFailure(e => Types.AwsCryptographyPrimitives(e));
+      assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient;
+      var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient;
 
       var kmsHierarchyUnwrap := new KmsHierarchyUnwrapKeyMaterial(
         branchKey,
         branchKeyIdUtf8,
         branchKeyVersionAsBytes,
-        crypto
+        cryptoPrimitives
       );
 
       var unwrapOutputRes := EdkWrapping.UnwrapEdkMaterial(

AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy

@@ -19,8 +19,8 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw
   datatype BeaconKeyMaterials = | BeaconKeyMaterials (
     nameonly beaconKeyIdentifier: string ,
     nameonly encryptionContext: EncryptionContext ,
-    nameonly beaconKey: Option<Secret> ,
-    nameonly hmacKeys: Option<HmacKeyMap>
+    nameonly beaconKey: Option<Secret> := Option.None ,
+    nameonly hmacKeys: Option<HmacKeyMap> := Option.None
   )
   datatype BranchKeyMaterials = | BranchKeyMaterials (
     nameonly branchKeyIdentifier: string ,
@@ -29,8 +29,8 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw
     nameonly branchKey: Secret
   )
   datatype CreateKeyInput = | CreateKeyInput (
-    nameonly branchKeyIdentifier: Option<string> ,
-    nameonly encryptionContext: Option<EncryptionContext>
+    nameonly branchKeyIdentifier: Option<string> := Option.None ,
+    nameonly encryptionContext: Option<EncryptionContext> := Option.None
   )
   datatype CreateKeyOutput = | CreateKeyOutput (
     nameonly branchKeyIdentifier: string
@@ -225,10 +225,10 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw
     nameonly ddbTableName: ComAmazonawsDynamodbTypes.TableName ,
     nameonly kmsConfiguration: KMSConfiguration ,
     nameonly logicalKeyStoreName: string ,
-    nameonly id: Option<string> ,
-    nameonly grantTokens: Option<GrantTokenList> ,
-    nameonly ddbClient: Option<ComAmazonawsDynamodbTypes.IDynamoDBClient> ,
-    nameonly kmsClient: Option<ComAmazonawsKmsTypes.IKMSClient>
+    nameonly id: Option<string> := Option.None ,
+    nameonly grantTokens: Option<GrantTokenList> := Option.None ,
+    nameonly ddbClient: Option<ComAmazonawsDynamodbTypes.IDynamoDBClient> := Option.None ,
+    nameonly kmsClient: Option<ComAmazonawsKmsTypes.IKMSClient> := Option.None
   )
   datatype KMSConfiguration =
     | kmsKeyArn(kmsKeyArn: ComAmazonawsKmsTypes.KeyIdType)
@@ -285,7 +285,7 @@ abstract module AbstractAwsCryptographyKeyStoreService
   import Operations : AbstractAwsCryptographyKeyStoreOperations
   function method DefaultKeyStoreConfig(): KeyStoreConfig
   method KeyStore(config: KeyStoreConfig := DefaultKeyStoreConfig())
-    returns (res: Result<KeyStoreClient, Error>)
+    returns (res: Result<IKeyStoreClient, Error>)
     requires config.ddbClient.Some? ==>
                config.ddbClient.value.ValidState()
     requires config.kmsClient.Some? ==>
@@ -313,6 +313,13 @@ abstract module AbstractAwsCryptographyKeyStoreService
     ensures config.kmsClient.Some? ==>
               config.kmsClient.value.ValidState()
 
+  // Helper function for the benefit of native code to create a Success(client) without referring to Dafny internals
+  function method CreateSuccessOfClient(client: IKeyStoreClient): Result<IKeyStoreClient, Error> {
+    Success(client)
+  } // Helper function for the benefit of native code to create a Failure(error) without referring to Dafny internals
+  function method CreateFailureOfError(error: Error): Result<IKeyStoreClient, Error> {
+    Failure(error)
+  }
   class KeyStoreClient extends IKeyStoreClient
   {
     constructor(config: Operations.InternalConfig)