fix: repolymorph to get default parameter for OpaqueError (#911)

ajewellamz · web-flow · commit 5669e0b709b2 · 2024-10-28T15:33:36.000-04:00
* fix: repolymorph to get default parameter for OpaqueError
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
@@ -1712,7 +1712,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
     // || (!exit(A(I)) && !access(B(I)))
     | CollectionOfErrors(list: seq<Error>, nameonly message: string)
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string)
+    | Opaque(obj: object, alt_text : string := "")
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractAwsCryptographyMaterialProvidersService
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
@@ -282,7 +282,7 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw
     // || (!exit(A(I)) && !access(B(I)))
     | CollectionOfErrors(list: seq<Error>, nameonly message: string)
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string)
+    | Opaque(obj: object, alt_text : string := "")
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractAwsCryptographyKeyStoreService
diff --git a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy b/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy
@@ -689,7 +689,7 @@ module {:extern "software.amazon.cryptography.primitives.internaldafny.types" }
     // || (!exit(A(I)) && !access(B(I)))
     | CollectionOfErrors(list: seq<Error>, nameonly message: string)
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string)
+    | Opaque(obj: object, alt_text : string := "")
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractAwsCryptographyPrimitivesService
diff --git a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy
@@ -2725,7 +2725,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty
 
 
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string)
+    | Opaque(obj: object, alt_text : string := "")
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractComAmazonawsDynamodbService {
diff --git a/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy b/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy
@@ -1976,7 +1976,7 @@ module {:extern "software.amazon.cryptography.services.kms.internaldafny.types"
 
 
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string)
+    | Opaque(obj: object, alt_text : string := "")
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractComAmazonawsKmsService {
diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy
@@ -260,7 +260,7 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in
     // || (!exit(A(I)) && !access(B(I)))
     | CollectionOfErrors(list: seq<Error>, nameonly message: string)
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string)
+    | Opaque(obj: object, alt_text : string := "")
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractAwsCryptographyMaterialProvidersTestVectorKeysService
diff --git a/smithy-dafny b/smithy-dafny
@@ -1 +1 @@
-Subproject commit e602cbf45e55108f3a753c1ea06d38bd5fcdbe3c
+Subproject commit cff81f5baa7104f6873aadc81d8e9a75121253cd

Original file line number	Diff line number	Diff line change
`@@ -1712,7 +1712,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty`
`1712`	`1712`	`// \|\| (!exit(A(I)) && !access(B(I)))`
`1713`	`1713`	`\| CollectionOfErrors(list: seq<Error>, nameonly message: string)`
`1714`	`1714`	`// The Opaque error, used for native, extern, wrapped or unknown errors`
`1715`		`- \| Opaque(obj: object, alt_text : string)`
	`1715`	`+ \| Opaque(obj: object, alt_text : string := "")`
`1716`	`1716`	`type OpaqueError = e: Error \| e.Opaque? witness *`
`1717`	`1717`	`}`
`1718`	`1718`	`abstract module AbstractAwsCryptographyMaterialProvidersService`
Original file line number	Diff line number	Diff line change
`@@ -282,7 +282,7 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw`
`282`	`282`	`// \|\| (!exit(A(I)) && !access(B(I)))`
`283`	`283`	`\| CollectionOfErrors(list: seq<Error>, nameonly message: string)`
`284`	`284`	`// The Opaque error, used for native, extern, wrapped or unknown errors`
`285`		`- \| Opaque(obj: object, alt_text : string)`
	`285`	`+ \| Opaque(obj: object, alt_text : string := "")`
`286`	`286`	`type OpaqueError = e: Error \| e.Opaque? witness *`
`287`	`287`	`}`
`288`	`288`	`abstract module AbstractAwsCryptographyKeyStoreService`
Original file line number	Diff line number	Diff line change
`@@ -689,7 +689,7 @@ module {:extern "software.amazon.cryptography.primitives.internaldafny.types" }`
`689`	`689`	`// \|\| (!exit(A(I)) && !access(B(I)))`
`690`	`690`	`\| CollectionOfErrors(list: seq<Error>, nameonly message: string)`
`691`	`691`	`// The Opaque error, used for native, extern, wrapped or unknown errors`
`692`		`- \| Opaque(obj: object, alt_text : string)`
	`692`	`+ \| Opaque(obj: object, alt_text : string := "")`
`693`	`693`	`type OpaqueError = e: Error \| e.Opaque? witness *`
`694`	`694`	`}`
`695`	`695`	`abstract module AbstractAwsCryptographyPrimitivesService`
Original file line number	Diff line number	Diff line change
`@@ -2725,7 +2725,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty`
`2725`	`2725`
`2726`	`2726`
`2727`	`2727`	`// The Opaque error, used for native, extern, wrapped or unknown errors`
`2728`		`- \| Opaque(obj: object, alt_text : string)`
	`2728`	`+ \| Opaque(obj: object, alt_text : string := "")`
`2729`	`2729`	`type OpaqueError = e: Error \| e.Opaque? witness *`
`2730`	`2730`	`}`
`2731`	`2731`	`abstract module AbstractComAmazonawsDynamodbService {`
Original file line number	Diff line number	Diff line change
`@@ -1976,7 +1976,7 @@ module {:extern "software.amazon.cryptography.services.kms.internaldafny.types"`
`1976`	`1976`
`1977`	`1977`
`1978`	`1978`	`// The Opaque error, used for native, extern, wrapped or unknown errors`
`1979`		`- \| Opaque(obj: object, alt_text : string)`
	`1979`	`+ \| Opaque(obj: object, alt_text : string := "")`
`1980`	`1980`	`type OpaqueError = e: Error \| e.Opaque? witness *`
`1981`	`1981`	`}`
`1982`	`1982`	`abstract module AbstractComAmazonawsKmsService {`
Original file line number	Diff line number	Diff line change
`@@ -260,7 +260,7 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in`
`260`	`260`	`// \|\| (!exit(A(I)) && !access(B(I)))`
`261`	`261`	`\| CollectionOfErrors(list: seq<Error>, nameonly message: string)`
`262`	`262`	`// The Opaque error, used for native, extern, wrapped or unknown errors`
`263`		`- \| Opaque(obj: object, alt_text : string)`
	`263`	`+ \| Opaque(obj: object, alt_text : string := "")`
`264`	`264`	`type OpaqueError = e: Error \| e.Opaque? witness *`
`265`	`265`	`}`
`266`	`266`	`abstract module AbstractAwsCryptographyMaterialProvidersTestVectorKeysService`