Skip to content

Commit ffbced4

Browse files
josecorellajosecorella
committed
feat: update codegen to Dafny 4.7.0
1 parent 808a5b4 commit ffbced4

File tree

47 files changed

+807
-64
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

47 files changed

+807
-64
lines changed

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -873,7 +873,6 @@ structure CreateDynamoDbEncryptionBranchKeyIdSupplierOutput {
873873
branchKeyIdSupplier: BranchKeyIdSupplierReference
874874
}
875875

876-
/////////////
877876
// Errors
878877

879878
@error("client")

‎DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/DynamoDbItemEncryptor.smithy

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -224,7 +224,6 @@ structure AtomicPrimitivesReference {}
224224
@aws.polymorph#reference(service: aws.cryptography.dbEncryptionSdk.structuredEncryption#StructuredEncryption)
225225
structure StructuredEncryptionReference {}
226226

227-
/////////////
228227
// Errors
229228

230229
@error("client")

‎DynamoDbEncryption/dafny/StructuredEncryption/Model/StructuredEncryption.smithy

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -405,7 +405,6 @@ list AuthList {
405405
@aws.polymorph#reference(service: aws.cryptography.primitives#AwsCryptographicPrimitives)
406406
structure AtomicPrimitivesReference {}
407407

408-
/////////////
409408
// Errors
410409

411410
@error("client")

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbKeyBranchKeyIdSupplier.java

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -103,9 +103,17 @@ > GetBranchKeyIdFromDdbKey(
103103
this._impl.GetBranchKeyIdFromDdbKey(nativeInput);
104104
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput dafnyOutput =
105105
ToDafny.GetBranchKeyIdFromDdbKeyOutput(nativeOutput);
106-
return Result.create_Success(dafnyOutput);
106+
return Result.create_Success(
107+
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput._typeDescriptor(),
108+
Error._typeDescriptor(),
109+
dafnyOutput
110+
);
107111
} catch (RuntimeException ex) {
108-
return Result.create_Failure(ToDafny.Error(ex));
112+
return Result.create_Failure(
113+
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.GetBranchKeyIdFromDdbKeyOutput._typeDescriptor(),
114+
Error._typeDescriptor(),
115+
ToDafny.Error(ex)
116+
);
109117
}
110118
}
111119

‎DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java

Lines changed: 104 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66
import Wrappers_Compile.Option;
77
import dafny.DafnyMap;
88
import dafny.DafnySequence;
9+
import dafny.TypeDescriptor;
910
import java.lang.Boolean;
1011
import java.lang.Character;
1112
import java.lang.IllegalArgumentException;
@@ -129,31 +130,45 @@ public static BeaconVersion BeaconVersion(
129130
(Objects.nonNull(nativeValue.compoundBeacons()) &&
130131
nativeValue.compoundBeacons().size() > 0)
131132
? Option.create_Some(
133+
DafnySequence._typeDescriptor(CompoundBeacon._typeDescriptor()),
132134
ToDafny.CompoundBeaconList(nativeValue.compoundBeacons())
133135
)
134-
: Option.create_None();
136+
: Option.create_None(
137+
DafnySequence._typeDescriptor(CompoundBeacon._typeDescriptor())
138+
);
135139
Option<DafnySequence<? extends VirtualField>> virtualFields;
136140
virtualFields =
137141
(Objects.nonNull(nativeValue.virtualFields()) &&
138142
nativeValue.virtualFields().size() > 0)
139143
? Option.create_Some(
144+
DafnySequence._typeDescriptor(VirtualField._typeDescriptor()),
140145
ToDafny.VirtualFieldList(nativeValue.virtualFields())
141146
)
142-
: Option.create_None();
147+
: Option.create_None(
148+
DafnySequence._typeDescriptor(VirtualField._typeDescriptor())
149+
);
143150
Option<DafnySequence<? extends EncryptedPart>> encryptedParts;
144151
encryptedParts =
145152
(Objects.nonNull(nativeValue.encryptedParts()) &&
146153
nativeValue.encryptedParts().size() > 0)
147154
? Option.create_Some(
155+
DafnySequence._typeDescriptor(EncryptedPart._typeDescriptor()),
148156
ToDafny.EncryptedPartsList(nativeValue.encryptedParts())
149157
)
150-
: Option.create_None();
158+
: Option.create_None(
159+
DafnySequence._typeDescriptor(EncryptedPart._typeDescriptor())
160+
);
151161
Option<DafnySequence<? extends SignedPart>> signedParts;
152162
signedParts =
153163
(Objects.nonNull(nativeValue.signedParts()) &&
154164
nativeValue.signedParts().size() > 0)
155-
? Option.create_Some(ToDafny.SignedPartsList(nativeValue.signedParts()))
156-
: Option.create_None();
165+
? Option.create_Some(
166+
DafnySequence._typeDescriptor(SignedPart._typeDescriptor()),
167+
ToDafny.SignedPartsList(nativeValue.signedParts())
168+
)
169+
: Option.create_None(
170+
DafnySequence._typeDescriptor(SignedPart._typeDescriptor())
171+
);
157172
return new BeaconVersion(
158173
version,
159174
keyStore,
@@ -184,22 +199,33 @@ public static CompoundBeacon CompoundBeacon(
184199
(Objects.nonNull(nativeValue.encrypted()) &&
185200
nativeValue.encrypted().size() > 0)
186201
? Option.create_Some(
202+
DafnySequence._typeDescriptor(EncryptedPart._typeDescriptor()),
187203
ToDafny.EncryptedPartsList(nativeValue.encrypted())
188204
)
189-
: Option.create_None();
205+
: Option.create_None(
206+
DafnySequence._typeDescriptor(EncryptedPart._typeDescriptor())
207+
);
190208
Option<DafnySequence<? extends SignedPart>> signed;
191209
signed =
192210
(Objects.nonNull(nativeValue.signed()) && nativeValue.signed().size() > 0)
193-
? Option.create_Some(ToDafny.SignedPartsList(nativeValue.signed()))
194-
: Option.create_None();
211+
? Option.create_Some(
212+
DafnySequence._typeDescriptor(SignedPart._typeDescriptor()),
213+
ToDafny.SignedPartsList(nativeValue.signed())
214+
)
215+
: Option.create_None(
216+
DafnySequence._typeDescriptor(SignedPart._typeDescriptor())
217+
);
195218
Option<DafnySequence<? extends Constructor>> constructors;
196219
constructors =
197220
(Objects.nonNull(nativeValue.constructors()) &&
198221
nativeValue.constructors().size() > 0)
199222
? Option.create_Some(
223+
DafnySequence._typeDescriptor(Constructor._typeDescriptor()),
200224
ToDafny.ConstructorList(nativeValue.constructors())
201225
)
202-
: Option.create_None();
226+
: Option.create_None(
227+
DafnySequence._typeDescriptor(Constructor._typeDescriptor())
228+
);
203229
return new CompoundBeacon(name, split, encrypted, signed, constructors);
204230
}
205231

@@ -273,16 +299,22 @@ public static DynamoDbTableEncryptionConfig DynamoDbTableEncryptionConfig(
273299
sortKeyName =
274300
Objects.nonNull(nativeValue.sortKeyName())
275301
? Option.create_Some(
302+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
276303
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
277304
nativeValue.sortKeyName()
278305
)
279306
)
280-
: Option.create_None();
307+
: Option.create_None(
308+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
309+
);
281310
Option<SearchConfig> search;
282311
search =
283312
Objects.nonNull(nativeValue.search())
284-
? Option.create_Some(ToDafny.SearchConfig(nativeValue.search()))
285-
: Option.create_None();
313+
? Option.create_Some(
314+
SearchConfig._typeDescriptor(),
315+
ToDafny.SearchConfig(nativeValue.search())
316+
)
317+
: Option.create_None(SearchConfig._typeDescriptor());
286318
DafnyMap<
287319
? extends DafnySequence<? extends Character>,
288320
? extends CryptoAction
@@ -296,61 +328,78 @@ public static DynamoDbTableEncryptionConfig DynamoDbTableEncryptionConfig(
296328
(Objects.nonNull(nativeValue.allowedUnsignedAttributes()) &&
297329
nativeValue.allowedUnsignedAttributes().size() > 0)
298330
? Option.create_Some(
331+
DafnySequence._typeDescriptor(
332+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
333+
),
299334
software.amazon.cryptography.services.dynamodb.internaldafny.ToDafny.AttributeNameList(
300335
nativeValue.allowedUnsignedAttributes()
301336
)
302337
)
303-
: Option.create_None();
338+
: Option.create_None(
339+
DafnySequence._typeDescriptor(
340+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
341+
)
342+
);
304343
Option<DafnySequence<? extends Character>> allowedUnsignedAttributePrefix;
305344
allowedUnsignedAttributePrefix =
306345
Objects.nonNull(nativeValue.allowedUnsignedAttributePrefix())
307346
? Option.create_Some(
347+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
308348
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
309349
nativeValue.allowedUnsignedAttributePrefix()
310350
)
311351
)
312-
: Option.create_None();
352+
: Option.create_None(
353+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
354+
);
313355
Option<DBEAlgorithmSuiteId> algorithmSuiteId;
314356
algorithmSuiteId =
315357
Objects.nonNull(nativeValue.algorithmSuiteId())
316358
? Option.create_Some(
359+
DBEAlgorithmSuiteId._typeDescriptor(),
317360
software.amazon.cryptography.materialproviders.ToDafny.DBEAlgorithmSuiteId(
318361
nativeValue.algorithmSuiteId()
319362
)
320363
)
321-
: Option.create_None();
364+
: Option.create_None(DBEAlgorithmSuiteId._typeDescriptor());
322365
Option<IKeyring> keyring;
323366
keyring =
324367
Objects.nonNull(nativeValue.keyring())
325368
? Option.create_Some(
369+
TypeDescriptor.reference(IKeyring.class),
326370
software.amazon.cryptography.materialproviders.ToDafny.Keyring(
327371
nativeValue.keyring()
328372
)
329373
)
330-
: Option.create_None();
374+
: Option.create_None(TypeDescriptor.reference(IKeyring.class));
331375
Option<ICryptographicMaterialsManager> cmm;
332376
cmm =
333377
Objects.nonNull(nativeValue.cmm())
334378
? Option.create_Some(
379+
TypeDescriptor.reference(ICryptographicMaterialsManager.class),
335380
software.amazon.cryptography.materialproviders.ToDafny.CryptographicMaterialsManager(
336381
nativeValue.cmm()
337382
)
338383
)
339-
: Option.create_None();
384+
: Option.create_None(
385+
TypeDescriptor.reference(ICryptographicMaterialsManager.class)
386+
);
340387
Option<LegacyOverride> legacyOverride;
341388
legacyOverride =
342389
Objects.nonNull(nativeValue.legacyOverride())
343390
? Option.create_Some(
391+
LegacyOverride._typeDescriptor(),
344392
ToDafny.LegacyOverride(nativeValue.legacyOverride())
345393
)
346-
: Option.create_None();
394+
: Option.create_None(LegacyOverride._typeDescriptor());
347395
Option<PlaintextOverride> plaintextOverride;
348396
plaintextOverride =
349397
Objects.nonNull(nativeValue.plaintextOverride())
350398
? Option.create_Some(
399+
PlaintextOverride._typeDescriptor(),
351400
ToDafny.PlaintextOverride(nativeValue.plaintextOverride())
352401
)
353-
: Option.create_None();
402+
: Option.create_None(PlaintextOverride._typeDescriptor());
354403
return new DynamoDbTableEncryptionConfig(
355404
logicalTableName,
356405
partitionKeyName,
@@ -393,29 +442,38 @@ public static EncryptedDataKeyDescription EncryptedDataKeyDescription(
393442
keyProviderInfo =
394443
Objects.nonNull(nativeValue.keyProviderInfo())
395444
? Option.create_Some(
445+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
396446
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
397447
nativeValue.keyProviderInfo()
398448
)
399449
)
400-
: Option.create_None();
450+
: Option.create_None(
451+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
452+
);
401453
Option<DafnySequence<? extends Character>> branchKeyId;
402454
branchKeyId =
403455
Objects.nonNull(nativeValue.branchKeyId())
404456
? Option.create_Some(
457+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
405458
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
406459
nativeValue.branchKeyId()
407460
)
408461
)
409-
: Option.create_None();
462+
: Option.create_None(
463+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
464+
);
410465
Option<DafnySequence<? extends Character>> branchKeyVersion;
411466
branchKeyVersion =
412467
Objects.nonNull(nativeValue.branchKeyVersion())
413468
? Option.create_Some(
469+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
414470
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
415471
nativeValue.branchKeyVersion()
416472
)
417473
)
418-
: Option.create_None();
474+
: Option.create_None(
475+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
476+
);
419477
return new EncryptedDataKeyDescription(
420478
keyProviderId,
421479
keyProviderInfo,
@@ -570,11 +628,12 @@ public static LegacyOverride LegacyOverride(
570628
defaultAttributeFlag =
571629
Objects.nonNull(nativeValue.defaultAttributeFlag())
572630
? Option.create_Some(
631+
CryptoAction._typeDescriptor(),
573632
software.amazon.cryptography.dbencryptionsdk.structuredencryption.ToDafny.CryptoAction(
574633
nativeValue.defaultAttributeFlag()
575634
)
576635
)
577-
: Option.create_None();
636+
: Option.create_None(CryptoAction._typeDescriptor());
578637
return new LegacyOverride(
579638
policy,
580639
encryptor,
@@ -603,11 +662,12 @@ public static MultiKeyStore MultiKeyStore(
603662
cache =
604663
Objects.nonNull(nativeValue.cache())
605664
? Option.create_Some(
665+
CacheType._typeDescriptor(),
606666
software.amazon.cryptography.materialproviders.ToDafny.CacheType(
607667
nativeValue.cache()
608668
)
609669
)
610-
: Option.create_None();
670+
: Option.create_None(CacheType._typeDescriptor());
611671
return new MultiKeyStore(keyFieldName, cacheTTL, cache);
612672
}
613673

@@ -666,11 +726,14 @@ public static SignedPart SignedPart(
666726
loc =
667727
Objects.nonNull(nativeValue.loc())
668728
? Option.create_Some(
729+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
669730
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
670731
nativeValue.loc()
671732
)
672733
)
673-
: Option.create_None();
734+
: Option.create_None(
735+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
736+
);
674737
return new SignedPart(name, prefix, loc);
675738
}
676739

@@ -701,16 +764,22 @@ public static StandardBeacon StandardBeacon(
701764
loc =
702765
Objects.nonNull(nativeValue.loc())
703766
? Option.create_Some(
767+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR),
704768
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
705769
nativeValue.loc()
706770
)
707771
)
708-
: Option.create_None();
772+
: Option.create_None(
773+
DafnySequence._typeDescriptor(TypeDescriptor.CHAR)
774+
);
709775
Option<BeaconStyle> style;
710776
style =
711777
Objects.nonNull(nativeValue.style())
712-
? Option.create_Some(ToDafny.BeaconStyle(nativeValue.style()))
713-
: Option.create_None();
778+
? Option.create_Some(
779+
BeaconStyle._typeDescriptor(),
780+
ToDafny.BeaconStyle(nativeValue.style())
781+
)
782+
: Option.create_None(BeaconStyle._typeDescriptor());
714783
return new StandardBeacon(name, length, loc, style);
715784
}
716785

@@ -744,8 +813,13 @@ public static VirtualPart VirtualPart(
744813
Option<DafnySequence<? extends VirtualTransform>> trans;
745814
trans =
746815
(Objects.nonNull(nativeValue.trans()) && nativeValue.trans().size() > 0)
747-
? Option.create_Some(ToDafny.VirtualTransformList(nativeValue.trans()))
748-
: Option.create_None();
816+
? Option.create_Some(
817+
DafnySequence._typeDescriptor(VirtualTransform._typeDescriptor()),
818+
ToDafny.VirtualTransformList(nativeValue.trans())
819+
)
820+
: Option.create_None(
821+
DafnySequence._typeDescriptor(VirtualTransform._typeDescriptor())
822+
);
749823
return new VirtualPart(loc, trans);
750824
}
751825

0 commit comments

Comments
 (0)