Skip to content

Commit 65fe119

Browse files
lucasmcdonald3josecorella
lucasmcdonald3
authored and
josecorella
committed
m
1 parent 6a33fb3 commit 65fe119

17 files changed

+89
-297
lines changed

‎AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk/internaldafny/generated/AwsCryptographyEncryptionSdkTypes.py

Lines changed: 30 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -139,6 +139,10 @@ def IsValid__CountingNumbers(x):
139139
def IsValid__FrameLength(x):
140140
return ((1) <= (x)) and ((x) <= (4294967296))
141141

142+
@staticmethod
143+
def IsDummySubsetType(x):
144+
return (0) < (x)
145+
142146

143147
class DafnyCallEvent:
144148
@classmethod
@@ -350,6 +354,9 @@ def is_CollectionOfErrors(self) -> bool:
350354
@property
351355
def is_Opaque(self) -> bool:
352356
return isinstance(self, Error_Opaque)
357+
@property
358+
def is_OpaqueWithText(self) -> bool:
359+
return isinstance(self, Error_OpaqueWithText)
353360

354361
class Error_AwsEncryptionSdkException(Error, NamedTuple('AwsEncryptionSdkException', [('message', Any)])):
355362
def __dafnystr__(self) -> str:
@@ -383,11 +390,19 @@ def __eq__(self, __o: object) -> bool:
383390
def __hash__(self) -> int:
384391
return super().__hash__()
385392

386-
class Error_Opaque(Error, NamedTuple('Opaque', [('obj', Any), ('alt__text', Any)])):
393+
class Error_Opaque(Error, NamedTuple('Opaque', [('obj', Any)])):
394+
def __dafnystr__(self) -> str:
395+
return f'AwsCryptographyEncryptionSdkTypes.Error.Opaque({_dafny.string_of(self.obj)})'
396+
def __eq__(self, __o: object) -> bool:
397+
return isinstance(__o, Error_Opaque) and self.obj == __o.obj
398+
def __hash__(self) -> int:
399+
return super().__hash__()
400+
401+
class Error_OpaqueWithText(Error, NamedTuple('OpaqueWithText', [('obj', Any), ('objMessage', Any)])):
387402
def __dafnystr__(self) -> str:
388-
return f'AwsCryptographyEncryptionSdkTypes.Error.Opaque({_dafny.string_of(self.obj)}, {_dafny.string_of(self.alt__text)})'
403+
return f'AwsCryptographyEncryptionSdkTypes.Error.OpaqueWithText({_dafny.string_of(self.obj)}, {_dafny.string_of(self.objMessage)})'
389404
def __eq__(self, __o: object) -> bool:
390-
return isinstance(__o, Error_Opaque) and self.obj == __o.obj and self.alt__text == __o.alt__text
405+
return isinstance(__o, Error_OpaqueWithText) and self.obj == __o.obj and self.objMessage == __o.objMessage
391406
def __hash__(self) -> int:
392407
return super().__hash__()
393408

@@ -401,4 +416,15 @@ def default():
401416
return Error.default()()
402417
def _Is(source__):
403418
d_2_e_: Error = source__
404-
return (d_2_e_).is_Opaque
419+
return ((d_2_e_).is_Opaque) or ((d_2_e_).is_OpaqueWithText)
420+
421+
class DummySubsetType:
422+
def __init__(self):
423+
pass
424+
425+
@staticmethod
426+
def default():
427+
return 1
428+
def _Is(source__):
429+
d_3_x_: int = source__
430+
return default__.IsDummySubsetType(d_3_x_)

‎AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk/internaldafny/generated/EncryptionSdk.py

Lines changed: 0 additions & 234 deletions
This file was deleted.

‎AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk/internaldafny/generated/dafny_src-py.dtr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,6 @@ python-module-name = "aws_encryption_sdk.internaldafny.generated"
5454
[options_by_module.AwsEncryptionSdkOperations]
5555
legacy-module-names = false
5656
python-module-name = "aws_encryption_sdk.internaldafny.generated"
57-
[options_by_module.EncryptionSdk]
57+
[options_by_module.ESDK]
5858
legacy-module-names = false
5959
python-module-name = "aws_encryption_sdk.internaldafny.generated"

‎AwsEncryptionSDK/runtimes/python/src/aws_encryption_sdk/internaldafny/generated/module_.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -140,7 +140,7 @@
140140
import aws_encryption_sdk.internaldafny.generated.KeyDerivation as KeyDerivation
141141
import aws_encryption_sdk.internaldafny.generated.EncryptDecryptHelpers as EncryptDecryptHelpers
142142
import aws_encryption_sdk.internaldafny.generated.AwsEncryptionSdkOperations as AwsEncryptionSdkOperations
143-
import aws_encryption_sdk.internaldafny.generated.EncryptionSdk as EncryptionSdk
143+
import aws_encryption_sdk.internaldafny.generated.ESDK as ESDK
144144
import smithy_dafny_standard_library.internaldafny.generated.JSON_Utils_Views_Core as JSON_Utils_Views_Core
145145
import smithy_dafny_standard_library.internaldafny.generated.JSON_Utils_Views_Writers as JSON_Utils_Views_Writers
146146
import smithy_dafny_standard_library.internaldafny.generated.JSON_Utils_Lexers_Core as JSON_Utils_Lexers_Core

‎AwsEncryptionSDK/runtimes/python/test/internaldafny/generated/Fixtures.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@
105105
import aws_encryption_sdk.internaldafny.generated.KeyDerivation as KeyDerivation
106106
import aws_encryption_sdk.internaldafny.generated.EncryptDecryptHelpers as EncryptDecryptHelpers
107107
import aws_encryption_sdk.internaldafny.generated.AwsEncryptionSdkOperations as AwsEncryptionSdkOperations
108-
import aws_encryption_sdk.internaldafny.generated.EncryptionSdk as EncryptionSdk
108+
import aws_encryption_sdk.internaldafny.generated.ESDK as ESDK
109109
import aws_cryptography_primitives.internaldafny.generated.AesKdfCtr as AesKdfCtr
110110
import aws_cryptographic_material_providers.internaldafny.generated.KeyStoreErrorMessages as KeyStoreErrorMessages
111111
import aws_cryptographic_material_providers.internaldafny.generated.KmsArn as KmsArn

‎AwsEncryptionSDK/runtimes/python/test/internaldafny/generated/TestCreateEsdkClient.py

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@
105105
import aws_encryption_sdk.internaldafny.generated.KeyDerivation as KeyDerivation
106106
import aws_encryption_sdk.internaldafny.generated.EncryptDecryptHelpers as EncryptDecryptHelpers
107107
import aws_encryption_sdk.internaldafny.generated.AwsEncryptionSdkOperations as AwsEncryptionSdkOperations
108-
import aws_encryption_sdk.internaldafny.generated.EncryptionSdk as EncryptionSdk
108+
import aws_encryption_sdk.internaldafny.generated.ESDK as ESDK
109109
import aws_cryptography_primitives.internaldafny.generated.AesKdfCtr as AesKdfCtr
110110
import aws_cryptographic_material_providers.internaldafny.generated.KeyStoreErrorMessages as KeyStoreErrorMessages
111111
import aws_cryptographic_material_providers.internaldafny.generated.KmsArn as KmsArn
@@ -155,20 +155,20 @@ def __init__(self):
155155
@staticmethod
156156
def TestClientCreation():
157157
d_0_defaultConfig_: AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig
158-
d_0_defaultConfig_ = EncryptionSdk.default__.DefaultAwsEncryptionSdkConfig()
158+
d_0_defaultConfig_ = ESDK.default__.DefaultAwsEncryptionSdkConfig()
159159
d_1_valueOrError0_: Wrappers.Result = None
160160
out0_: Wrappers.Result
161-
out0_ = EncryptionSdk.default__.ESDK(d_0_defaultConfig_)
161+
out0_ = ESDK.default__.ESDK(d_0_defaultConfig_)
162162
d_1_valueOrError0_ = out0_
163163
if not(not((d_1_valueOrError0_).IsFailure())):
164164
raise _dafny.HaltException("dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy(55,51): " + _dafny.string_of(d_1_valueOrError0_))
165165
d_2_esdk_: AwsCryptographyEncryptionSdkTypes.IAwsEncryptionSdkClient
166166
d_2_esdk_ = (d_1_valueOrError0_).Extract()
167167
def iife0_(_is_0):
168-
return isinstance(_is_0, EncryptionSdk.ESDKClient)
168+
return isinstance(_is_0, ESDK.ESDKClient)
169169
if not(iife0_(d_2_esdk_)):
170170
raise _dafny.HaltException("dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy(56,8): " + _dafny.string_of(_dafny.Seq("expectation violation")))
171-
d_3_esdkClient_: EncryptionSdk.ESDKClient
171+
d_3_esdkClient_: ESDK.ESDKClient
172172
d_3_esdkClient_ = d_2_esdk_
173173
if not((((d_3_esdkClient_).config).commitmentPolicy) == (((d_0_defaultConfig_).commitmentPolicy).value)):
174174
raise _dafny.HaltException("dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy(59,8): " + _dafny.string_of(_dafny.Seq("expectation violation")))
@@ -205,11 +205,11 @@ def TestNetRetryFlag():
205205
d_8_esdkConfig_ = AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig_AwsEncryptionSdkConfig(Wrappers.Option_Some(AwsCryptographyMaterialProvidersTypes.ESDKCommitmentPolicy_REQUIRE__ENCRYPT__REQUIRE__DECRYPT()), Wrappers.Option_None(), Wrappers.Option_Some(AwsCryptographyEncryptionSdkTypes.NetV4__0__0__RetryPolicy_FORBID__RETRY()))
206206
d_9_valueOrError2_: Wrappers.Result = None
207207
out2_: Wrappers.Result
208-
out2_ = EncryptionSdk.default__.ESDK(d_8_esdkConfig_)
208+
out2_ = ESDK.default__.ESDK(d_8_esdkConfig_)
209209
d_9_valueOrError2_ = out2_
210210
if not(not((d_9_valueOrError2_).IsFailure())):
211211
raise _dafny.HaltException("dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy(85,27): " + _dafny.string_of(d_9_valueOrError2_))
212-
d_10_noRetryEsdk_: EncryptionSdk.ESDKClient
212+
d_10_noRetryEsdk_: ESDK.ESDKClient
213213
d_10_noRetryEsdk_ = (d_9_valueOrError2_).Extract()
214214
d_11_expectFailureDecryptOutput_: Wrappers.Result
215215
out3_: Wrappers.Result
@@ -218,14 +218,14 @@ def TestNetRetryFlag():
218218
if not((d_11_expectFailureDecryptOutput_).is_Failure):
219219
raise _dafny.HaltException("dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy(94,8): " + _dafny.string_of(_dafny.Seq("expectation violation")))
220220
d_12_defaultConfig_: AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig
221-
d_12_defaultConfig_ = EncryptionSdk.default__.DefaultAwsEncryptionSdkConfig()
221+
d_12_defaultConfig_ = ESDK.default__.DefaultAwsEncryptionSdkConfig()
222222
d_13_valueOrError3_: Wrappers.Result = None
223223
out4_: Wrappers.Result
224-
out4_ = EncryptionSdk.default__.ESDK(d_12_defaultConfig_)
224+
out4_ = ESDK.default__.ESDK(d_12_defaultConfig_)
225225
d_13_valueOrError3_ = out4_
226226
if not(not((d_13_valueOrError3_).IsFailure())):
227227
raise _dafny.HaltException("dafny/AwsEncryptionSdk/test/TestCreateEsdkClient.dfy(99,20): " + _dafny.string_of(d_13_valueOrError3_))
228-
d_14_esdk_: EncryptionSdk.ESDKClient
228+
d_14_esdk_: ESDK.ESDKClient
229229
d_14_esdk_ = (d_13_valueOrError3_).Extract()
230230
d_15_decryptOutput_: Wrappers.Result
231231
out5_: Wrappers.Result

‎AwsEncryptionSDK/runtimes/python/test/internaldafny/generated/TestEncryptDecrypt.py

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@
105105
import aws_encryption_sdk.internaldafny.generated.KeyDerivation as KeyDerivation
106106
import aws_encryption_sdk.internaldafny.generated.EncryptDecryptHelpers as EncryptDecryptHelpers
107107
import aws_encryption_sdk.internaldafny.generated.AwsEncryptionSdkOperations as AwsEncryptionSdkOperations
108-
import aws_encryption_sdk.internaldafny.generated.EncryptionSdk as EncryptionSdk
108+
import aws_encryption_sdk.internaldafny.generated.ESDK as ESDK
109109
import aws_cryptography_primitives.internaldafny.generated.AesKdfCtr as AesKdfCtr
110110
import aws_cryptographic_material_providers.internaldafny.generated.KeyStoreErrorMessages as KeyStoreErrorMessages
111111
import aws_cryptographic_material_providers.internaldafny.generated.KmsArn as KmsArn
@@ -158,14 +158,14 @@ def TestEncryptDecrypt():
158158
d_1_asdf_: _dafny.Seq
159159
d_1_asdf_ = _dafny.Seq([97, 115, 100, 102])
160160
d_2_defaultConfig_: AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig
161-
d_2_defaultConfig_ = EncryptionSdk.default__.DefaultAwsEncryptionSdkConfig()
161+
d_2_defaultConfig_ = ESDK.default__.DefaultAwsEncryptionSdkConfig()
162162
d_3_valueOrError0_: Wrappers.Result = None
163163
out0_: Wrappers.Result
164-
out0_ = EncryptionSdk.default__.ESDK(d_2_defaultConfig_)
164+
out0_ = ESDK.default__.ESDK(d_2_defaultConfig_)
165165
d_3_valueOrError0_ = out0_
166166
if not(not((d_3_valueOrError0_).IsFailure())):
167167
raise _dafny.HaltException("dafny/AwsEncryptionSdk/test/TestEncryptDecrypt.dfy(24,20): " + _dafny.string_of(d_3_valueOrError0_))
168-
d_4_esdk_: EncryptionSdk.ESDKClient
168+
d_4_esdk_: ESDK.ESDKClient
169169
d_4_esdk_ = (d_3_valueOrError0_).Extract()
170170
d_5_valueOrError1_: Wrappers.Result = None
171171
out1_: Wrappers.Result

‎AwsEncryptionSDK/runtimes/python/test/internaldafny/generated/TestReproducedEncryptionContext.py

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@
105105
import aws_encryption_sdk.internaldafny.generated.KeyDerivation as KeyDerivation
106106
import aws_encryption_sdk.internaldafny.generated.EncryptDecryptHelpers as EncryptDecryptHelpers
107107
import aws_encryption_sdk.internaldafny.generated.AwsEncryptionSdkOperations as AwsEncryptionSdkOperations
108-
import aws_encryption_sdk.internaldafny.generated.EncryptionSdk as EncryptionSdk
108+
import aws_encryption_sdk.internaldafny.generated.ESDK as ESDK
109109
import aws_cryptography_primitives.internaldafny.generated.AesKdfCtr as AesKdfCtr
110110
import aws_cryptographic_material_providers.internaldafny.generated.KeyStoreErrorMessages as KeyStoreErrorMessages
111111
import aws_cryptographic_material_providers.internaldafny.generated.KmsArn as KmsArn
@@ -157,14 +157,14 @@ def TestEncryptionContextOnDecrypt():
157157
d_1_asdf_: _dafny.Seq
158158
d_1_asdf_ = _dafny.Seq([97, 115, 100, 102])
159159
d_2_defaultConfig_: AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig
160-
d_2_defaultConfig_ = EncryptionSdk.default__.DefaultAwsEncryptionSdkConfig()
160+
d_2_defaultConfig_ = ESDK.default__.DefaultAwsEncryptionSdkConfig()
161161
d_3_valueOrError0_: Wrappers.Result = None
162162
out0_: Wrappers.Result
163-
out0_ = EncryptionSdk.default__.ESDK(d_2_defaultConfig_)
163+
out0_ = ESDK.default__.ESDK(d_2_defaultConfig_)
164164
d_3_valueOrError0_ = out0_
165165
if not(not((d_3_valueOrError0_).IsFailure())):
166166
raise _dafny.HaltException("dafny/AwsEncryptionSdk/test/TestReproducedEncContext.dfy(24,20): " + _dafny.string_of(d_3_valueOrError0_))
167-
d_4_esdk_: EncryptionSdk.ESDKClient
167+
d_4_esdk_: ESDK.ESDKClient
168168
d_4_esdk_ = (d_3_valueOrError0_).Extract()
169169
d_5_valueOrError1_: Wrappers.Result = None
170170
out1_: Wrappers.Result
@@ -228,14 +228,14 @@ def TestEncryptionContextOnDecryptFailure():
228228
d_1_asdf_: _dafny.Seq
229229
d_1_asdf_ = _dafny.Seq([97, 115, 100, 102])
230230
d_2_defaultConfig_: AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig
231-
d_2_defaultConfig_ = EncryptionSdk.default__.DefaultAwsEncryptionSdkConfig()
231+
d_2_defaultConfig_ = ESDK.default__.DefaultAwsEncryptionSdkConfig()
232232
d_3_valueOrError0_: Wrappers.Result = None
233233
out0_: Wrappers.Result
234-
out0_ = EncryptionSdk.default__.ESDK(d_2_defaultConfig_)
234+
out0_ = ESDK.default__.ESDK(d_2_defaultConfig_)
235235
d_3_valueOrError0_ = out0_
236236
if not(not((d_3_valueOrError0_).IsFailure())):
237237
raise _dafny.HaltException("dafny/AwsEncryptionSdk/test/TestReproducedEncContext.dfy(71,20): " + _dafny.string_of(d_3_valueOrError0_))
238-
d_4_esdk_: EncryptionSdk.ESDKClient
238+
d_4_esdk_: ESDK.ESDKClient
239239
d_4_esdk_ = (d_3_valueOrError0_).Extract()
240240
d_5_valueOrError1_: Wrappers.Result = None
241241
out1_: Wrappers.Result
@@ -304,14 +304,14 @@ def TestMismatchedEncryptionContextOnDecrypt():
304304
d_1_namespace_ = out0_
305305
d_2_name_ = out1_
306306
d_3_defaultConfig_: AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig
307-
d_3_defaultConfig_ = EncryptionSdk.default__.DefaultAwsEncryptionSdkConfig()
307+
d_3_defaultConfig_ = ESDK.default__.DefaultAwsEncryptionSdkConfig()
308308
d_4_valueOrError0_: Wrappers.Result = None
309309
out2_: Wrappers.Result
310-
out2_ = EncryptionSdk.default__.ESDK(d_3_defaultConfig_)
310+
out2_ = ESDK.default__.ESDK(d_3_defaultConfig_)
311311
d_4_valueOrError0_ = out2_
312312
if not(not((d_4_valueOrError0_).IsFailure())):
313313
raise _dafny.HaltException("dafny/AwsEncryptionSdk/test/TestReproducedEncContext.dfy(117,20): " + _dafny.string_of(d_4_valueOrError0_))
314-
d_5_esdk_: EncryptionSdk.ESDKClient
314+
d_5_esdk_: ESDK.ESDKClient
315315
d_5_esdk_ = (d_4_valueOrError0_).Extract()
316316
d_6_valueOrError1_: Wrappers.Result = None
317317
out3_: Wrappers.Result

0 commit comments

Comments
 (0)