Skip to content

Commit 5c53d59

Browse files
ajewellamzajewellamz
authored
feat(dafny): Add bucket beacon support (#1943)
1 parent 105e862 commit 5c53d59

97 files changed

Lines changed: 6721 additions & 926 deletions

File tree

Some content is hidden

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

‎.github/workflows/ci_codegen.yml‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,9 @@ jobs:
4343
with:
4444
ref: ${{ inputs.branch || github.head_ref || github.ref }}
4545
submodules: recursive
46-
- run: git submodule update --init --recursive submodules/smithy-dafny
46+
- run: |
47+
git submodule update --init --recursive submodules/smithy-dafny
48+
git submodule update --init --recursive submodules/MaterialProviders
4749
4850
# Only used to format generated code
4951
# and to translate version strings such as "nightly-latest"

‎DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.2.0.patch‎

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

‎DynamoDbEncryption/codegen-patches/DynamoDbEncryption/dotnet/dafny-4.8.0.patch‎

Lines changed: 5 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -1,51 +1,15 @@
11
diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
2-
index 9601968..a2a04f8 100644
2+
index 64de7ab2..63a975a6 100644
33
--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
44
+++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/TypeConversion.cs
5-
@@ -7,10 +7,43 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
5+
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb
66
{
77
public static class TypeConversion
88
{
99
- private const string ISO8601DateFormat = "yyyy-MM-dd\\THH:mm:ss.fff\\Z";
1010
-
1111
- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
12-
+ // BEGIN MANUAL EDIT
13-
+ public static AWS.Cryptography.KeyStore.KeyStore FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S17_KeyStoreReference(software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient value)
14-
+ {
15-
+ if (value is software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient dafnyValue)
16-
+ {
17-
+ return new AWS.Cryptography.KeyStore.KeyStore(dafnyValue);
18-
+ }
19-
+ throw new System.ArgumentException("Custom implementations of AWS.Cryptography.KeyStore.KeyStore are not supported yet");
20-
+ }
21-
+ public static software.amazon.cryptography.keystore.internaldafny.types.IKeyStoreClient ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S17_KeyStoreReference(AWS.Cryptography.KeyStore.KeyStore value)
22-
+ {
23-
+ if (value is AWS.Cryptography.KeyStore.KeyStore nativeValue)
24-
+ {
25-
+ return nativeValue.impl();
26-
+ }
27-
+ throw new System.ArgumentException("Custom implementations of AWS.Cryptography.KeyStore.KeyStore are not supported yet");
28-
+ }
29-
+ public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ILegacyDynamoDbEncryptor FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S32_LegacyDynamoDbEncryptorReference(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.ILegacyDynamoDbEncryptor value)
30-
+ {
31-
+ if (value is NativeWrapper_LegacyDynamoDbEncryptor nativeWrapper) return nativeWrapper._impl;
32-
+ return new LegacyDynamoDbEncryptor(value);
33-
34-
+ }
35-
+ public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.ILegacyDynamoDbEncryptor ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S32_LegacyDynamoDbEncryptorReference(AWS.Cryptography.DbEncryptionSDK.DynamoDb.ILegacyDynamoDbEncryptor value)
36-
+ {
37-
+ switch (value)
38-
+ {
39-
+ case LegacyDynamoDbEncryptor valueWithImpl:
40-
+ return valueWithImpl._impl;
41-
+ case LegacyDynamoDbEncryptorBase nativeImpl:
42-
+ return new NativeWrapper_LegacyDynamoDbEncryptor(nativeImpl);
43-
+ default:
44-
+ throw new System.ArgumentException(
45-
+ "Custom implementations of LegacyDynamoDbEncryptor must extend LegacyDynamoDbEncryptorBase.");
46-
+ }
47-
+ }
48-
+ // END MANUAL EDIT
49-
public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.BeaconKeySource FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S15_BeaconKeySource(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IBeaconKeySource value)
12+
-
13+
public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
5014
{
51-
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconKeySource)value;
15+
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;

‎DynamoDbEncryption/codegen-patches/DynamoDbEncryptionTransforms/dotnet/dafny-4.8.0.patch‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
2-
index 2f95341..36226d3 100644
2+
index b7d2a823..0c973183 100644
33
--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
44
+++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs
55
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.Transforms
@@ -10,6 +10,6 @@ index 2f95341..36226d3 100644
1010
-
1111
- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
1212
-
13-
public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTablesEncryptionConfig FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S30_DynamoDbTablesEncryptionConfig(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IDynamoDbTablesEncryptionConfig value)
13+
public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S5_AsSet(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IAsSet value)
1414
{
15-
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbTablesEncryptionConfig concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.DynamoDbTablesEncryptionConfig)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTablesEncryptionConfig converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTablesEncryptionConfig(); converted.TableEncryptionConfigs = (System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.DynamoDb.DynamoDbTableEncryptionConfig>)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S30_DynamoDbTablesEncryptionConfig__M22_tableEncryptionConfigs(concrete._tableEncryptionConfigs); return converted;
15+
software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.AsSet)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.AsSet(); return converted;

‎DynamoDbEncryption/codegen-patches/DynamoDbItemEncryptor/dotnet/dafny-4.8.0.patch‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
diff --git b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
2-
index da904fc..c5b0bed 100644
2+
index b4a90d1b..b5d5046a 100644
33
--- b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
44
+++ a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbItemEncryptor/TypeConversion.cs
55
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor
@@ -10,6 +10,6 @@ index da904fc..c5b0bed 100644
1010
-
1111
- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
1212
-
13-
public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_DecryptItemInput(software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types._IDecryptItemInput value)
13+
public static System.Collections.Generic.Dictionary<string, AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.CryptoAction> FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions(Dafny.IMap<Dafny.ISequence<char>, software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._ICryptoAction> value)
1414
{
15-
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemInput concrete = (software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemInput)value; AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput converted = new AWS.Cryptography.DbEncryptionSDK.DynamoDb.ItemEncryptor.DecryptItemInput(); converted.EncryptedItem = (System.Collections.Generic.Dictionary<string, Amazon.DynamoDBv2.Model.AttributeValue>)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__N13_itemEncryptor__S16_DecryptItemInput__M13_encryptedItem(concrete._encryptedItem); return converted;
15+
return value.ItemEnumerable.ToDictionary(pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M3_key(pair.Car), pair => FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S16_AttributeActions__M5_value(pair.Cdr));

‎DynamoDbEncryption/codegen-patches/StructuredEncryption/dotnet/dafny-4.8.0.patch‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
diff --git b/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs a/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
2-
index d0a4e58..4e9890c 100644
2+
index df81f311..ac28fc2a 100644
33
--- b/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
44
+++ a/DynamoDbEncryption/runtimes/net/Generated/StructuredEncryption/TypeConversion.cs
55
@@ -7,10 +7,6 @@ namespace AWS.Cryptography.DbEncryptionSDK.StructuredEncryption
@@ -10,6 +10,6 @@ index d0a4e58..4e9890c 100644
1010
-
1111
- private const string ISO8601DateFormatNoMS = "yyyy-MM-dd\\THH:mm:ss\\Z";
1212
-
13-
public static AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.AuthenticateAction FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N20_structuredEncryption__S18_AuthenticateAction(software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types._IAuthenticateAction value)
13+
public static AWS.Cryptography.Primitives.AtomicPrimitives FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N20_structuredEncryption__S25_AtomicPrimitivesReference(software.amazon.cryptography.primitives.internaldafny.types.IAwsCryptographicPrimitivesClient value)
1414
{
15-
if (value.is_SIGN) return AWS.Cryptography.DbEncryptionSDK.StructuredEncryption.AuthenticateAction.SIGN;
15+
if (value is software.amazon.cryptography.primitives.internaldafny.types.IAwsCryptographicPrimitivesClient dafnyValue)

‎DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy‎

Lines changed: 87 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,10 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
4646
nameonly compoundBeacons: Option<CompoundBeaconList> := Option.None ,
4747
nameonly virtualFields: Option<VirtualFieldList> := Option.None ,
4848
nameonly encryptedParts: Option<EncryptedPartsList> := Option.None ,
49-
nameonly signedParts: Option<SignedPartsList> := Option.None
49+
nameonly signedParts: Option<SignedPartsList> := Option.None ,
50+
nameonly maximumNumberOfPartitions: Option<PartitionCount> := Option.None ,
51+
nameonly defaultNumberOfPartitions: Option<PartitionCount> := Option.None ,
52+
nameonly partitionSelector: Option<IPartitionSelector> := Option.None
5053
)
5154
type BeaconVersionList = x: seq<BeaconVersion> | IsValid_BeaconVersionList(x) witness *
5255
predicate method IsValid_BeaconVersionList(x: seq<BeaconVersion>) {
@@ -281,6 +284,14 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
281284
datatype GetEncryptedDataKeyDescriptionUnion =
282285
| header(header: seq<uint8>)
283286
| item(item: ComAmazonawsDynamodbTypes.AttributeMap)
287+
datatype GetPartitionNumberInput = | GetPartitionNumberInput (
288+
nameonly item: ComAmazonawsDynamodbTypes.AttributeMap ,
289+
nameonly numberOfPartitions: PartitionCount ,
290+
nameonly logicalTableName: string
291+
)
292+
datatype GetPartitionNumberOutput = | GetPartitionNumberOutput (
293+
nameonly partitionNumber: PartitionNumber
294+
)
284295
datatype GetPrefix = | GetPrefix (
285296
nameonly length: int32
286297
)
@@ -357,6 +368,79 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
357368
nameonly cache: Option<AwsCryptographyMaterialProvidersTypes.CacheType> := Option.None ,
358369
nameonly partitionId: Option<string> := Option.None
359370
)
371+
type PartitionCount = x: int32 | IsValid_PartitionCount(x) witness *
372+
predicate method IsValid_PartitionCount(x: int32) {
373+
( 1 <= x <= 255 )
374+
}
375+
type PartitionNumber = x: int32 | IsValid_PartitionNumber(x) witness *
376+
predicate method IsValid_PartitionNumber(x: int32) {
377+
( 0 <= x <= 254 )
378+
}
379+
class IPartitionSelectorCallHistory {
380+
ghost constructor() {
381+
GetPartitionNumber := [];
382+
}
383+
ghost var GetPartitionNumber: seq<DafnyCallEvent<GetPartitionNumberInput, Result<GetPartitionNumberOutput, Error>>>
384+
}
385+
trait {:termination false} IPartitionSelector
386+
{
387+
// Helper to define any additional modifies/reads clauses.
388+
// If your operations need to mutate state,
389+
// add it in your constructor function:
390+
// Modifies := {your, fields, here, History};
391+
// If you do not need to mutate anything:
392+
// Modifies := {History};
393+
394+
ghost const Modifies: set<object>
395+
// For an unassigned field defined in a trait,
396+
// Dafny can only assign a value in the constructor.
397+
// This means that for Dafny to reason about this value,
398+
// it needs some way to know (an invariant),
399+
// about the state of the object.
400+
// This builds on the Valid/Repr paradigm
401+
// To make this kind requires safe to add
402+
// to methods called from unverified code,
403+
// the predicate MUST NOT take any arguments.
404+
// This means that the correctness of this requires
405+
// MUST only be evaluated by the class itself.
406+
// If you require any additional mutation,
407+
// then you MUST ensure everything you need in ValidState.
408+
// You MUST also ensure ValidState in your constructor.
409+
predicate ValidState()
410+
ensures ValidState() ==> History in Modifies
411+
ghost const History: IPartitionSelectorCallHistory
412+
predicate GetPartitionNumberEnsuresPublicly(input: GetPartitionNumberInput , output: Result<GetPartitionNumberOutput, Error>)
413+
// The public method to be called by library consumers
414+
method GetPartitionNumber ( input: GetPartitionNumberInput )
415+
returns (output: Result<GetPartitionNumberOutput, Error>)
416+
requires
417+
&& ValidState()
418+
modifies Modifies - {History} ,
419+
History`GetPartitionNumber
420+
// Dafny will skip type parameters when generating a default decreases clause.
421+
decreases Modifies - {History}
422+
ensures
423+
&& ValidState()
424+
ensures GetPartitionNumberEnsuresPublicly(input, output)
425+
ensures History.GetPartitionNumber == old(History.GetPartitionNumber) + [DafnyCallEvent(input, output)]
426+
{
427+
output := GetPartitionNumber' (input);
428+
History.GetPartitionNumber := History.GetPartitionNumber + [DafnyCallEvent(input, output)];
429+
}
430+
// The method to implement in the concrete class.
431+
method GetPartitionNumber' ( input: GetPartitionNumberInput )
432+
returns (output: Result<GetPartitionNumberOutput, Error>)
433+
requires
434+
&& ValidState()
435+
modifies Modifies - {History}
436+
// Dafny will skip type parameters when generating a default decreases clause.
437+
decreases Modifies - {History}
438+
ensures
439+
&& ValidState()
440+
ensures GetPartitionNumberEnsuresPublicly(input, output)
441+
ensures unchanged(History)
442+
443+
}
360444
datatype PartOnly = | PartOnly (
361445

362446
)
@@ -397,7 +481,8 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
397481
nameonly name: string ,
398482
nameonly length: BeaconBitLength ,
399483
nameonly loc: Option<TerminalLocation> := Option.None ,
400-
nameonly style: Option<BeaconStyle> := Option.None
484+
nameonly style: Option<BeaconStyle> := Option.None ,
485+
nameonly numberOfPartitions: Option<PartitionCount> := Option.None
401486
)
402487
type StandardBeaconList = x: seq<StandardBeacon> | IsValid_StandardBeaconList(x) witness *
403488
predicate method IsValid_StandardBeaconList(x: seq<StandardBeacon>) {

0 commit comments

Comments
 (0)