Skip to content

Commit b287021

Browse files
ajewellamzajewellamz
committed
m
1 parent 20ada7c commit b287021

File tree

37 files changed

+1136
-1123
lines changed

37 files changed

+1136
-1123
lines changed

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

Lines changed: 81 additions & 81 deletions
Original file line numberDiff line numberDiff line change
@@ -55,79 +55,6 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
5555
predicate method IsValid_BeaconVersionList(x: seq<BeaconVersion>) {
5656
( 1 <= |x| <= 1 )
5757
}
58-
type PartitionCount = x: int32 | IsValid_PartitionCount(x) witness *
59-
predicate method IsValid_PartitionCount(x: int32) {
60-
( 1 <= x <= 255 )
61-
}
62-
type PartitionNumber = x: int32 | IsValid_PartitionNumber(x) witness *
63-
predicate method IsValid_PartitionNumber(x: int32) {
64-
( 0 <= x <= 254 )
65-
}
66-
class IPartitionSelectorCallHistory {
67-
ghost constructor() {
68-
GetPartitionNumber := [];
69-
}
70-
ghost var GetPartitionNumber: seq<DafnyCallEvent<GetPartitionNumberInput, Result<GetPartitionNumberOutput, Error>>>
71-
}
72-
trait {:termination false} IPartitionSelector
73-
{
74-
// Helper to define any additional modifies/reads clauses.
75-
// If your operations need to mutate state,
76-
// add it in your constructor function:
77-
// Modifies := {your, fields, here, History};
78-
// If you do not need to mutate anything:
79-
// Modifies := {History};
80-
81-
ghost const Modifies: set<object>
82-
// For an unassigned field defined in a trait,
83-
// Dafny can only assign a value in the constructor.
84-
// This means that for Dafny to reason about this value,
85-
// it needs some way to know (an invariant),
86-
// about the state of the object.
87-
// This builds on the Valid/Repr paradigm
88-
// To make this kind requires safe to add
89-
// to methods called from unverified code,
90-
// the predicate MUST NOT take any arguments.
91-
// This means that the correctness of this requires
92-
// MUST only be evaluated by the class itself.
93-
// If you require any additional mutation,
94-
// then you MUST ensure everything you need in ValidState.
95-
// You MUST also ensure ValidState in your constructor.
96-
predicate ValidState()
97-
ensures ValidState() ==> History in Modifies
98-
ghost const History: IPartitionSelectorCallHistory
99-
predicate GetPartitionNumberEnsuresPublicly(input: GetPartitionNumberInput , output: Result<GetPartitionNumberOutput, Error>)
100-
// The public method to be called by library consumers
101-
method GetPartitionNumber ( input: GetPartitionNumberInput )
102-
returns (output: Result<GetPartitionNumberOutput, Error>)
103-
requires
104-
&& ValidState()
105-
modifies Modifies - {History} ,
106-
History`GetPartitionNumber
107-
// Dafny will skip type parameters when generating a default decreases clause.
108-
decreases Modifies - {History}
109-
ensures
110-
&& ValidState()
111-
ensures GetPartitionNumberEnsuresPublicly(input, output)
112-
ensures History.GetPartitionNumber == old(History.GetPartitionNumber) + [DafnyCallEvent(input, output)]
113-
{
114-
output := GetPartitionNumber' (input);
115-
History.GetPartitionNumber := History.GetPartitionNumber + [DafnyCallEvent(input, output)];
116-
}
117-
// The method to implement in the concrete class.
118-
method GetPartitionNumber' ( input: GetPartitionNumberInput )
119-
returns (output: Result<GetPartitionNumberOutput, Error>)
120-
requires
121-
&& ValidState()
122-
modifies Modifies - {History}
123-
// Dafny will skip type parameters when generating a default decreases clause.
124-
decreases Modifies - {History}
125-
ensures
126-
&& ValidState()
127-
ensures GetPartitionNumberEnsuresPublicly(input, output)
128-
ensures unchanged(History)
129-
130-
}
13158
type Char = x: string | IsValid_Char(x) witness *
13259
predicate method IsValid_Char(x: string) {
13360
( 1 <= |x| <= 1 )
@@ -348,14 +275,6 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
348275
datatype GetBranchKeyIdFromDdbKeyOutput = | GetBranchKeyIdFromDdbKeyOutput (
349276
nameonly branchKeyId: string
350277
)
351-
datatype GetPartitionNumberInput = | GetPartitionNumberInput (
352-
nameonly item: ComAmazonawsDynamodbTypes.AttributeMap ,
353-
nameonly numberOfPartitions: PartitionCount ,
354-
nameonly logicalTableName: string
355-
)
356-
datatype GetPartitionNumberOutput = | GetPartitionNumberOutput (
357-
nameonly partitionNumber: PartitionNumber
358-
)
359278
datatype GetEncryptedDataKeyDescriptionInput = | GetEncryptedDataKeyDescriptionInput (
360279
nameonly input: GetEncryptedDataKeyDescriptionUnion
361280
)
@@ -365,6 +284,14 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
365284
datatype GetEncryptedDataKeyDescriptionUnion =
366285
| header(header: seq<uint8>)
367286
| 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+
)
368295
datatype GetPrefix = | GetPrefix (
369296
nameonly length: int32
370297
)
@@ -441,6 +368,79 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald
441368
nameonly cache: Option<AwsCryptographyMaterialProvidersTypes.CacheType> := Option.None ,
442369
nameonly partitionId: Option<string> := Option.None
443370
)
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+
}
444444
datatype PartOnly = | PartOnly (
445445

446446
)

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -333,7 +333,7 @@ module SearchConfigToInfo {
333333
&& fresh(output.value.partitionSelector.Modifies)
334334
{
335335
var maxPartitions : PartitionCount := config.maximumNumberOfPartitions.UnwrapOr(1);
336-
:- Need(0 <= maxPartitions as nat < MAX_BUCKET_COUNT, E("Invalid maximumNumberOfPartitions specified, " + Base10Int2String(maxPartitions as int) + ", must be 0 < maximumNumberOfPartitions <= 255."));
336+
:- Need(0 <= maxPartitions as nat < MAX_PARTITION_COUNT, E("Invalid maximumNumberOfPartitions specified, " + Base10Int2String(maxPartitions as int) + ", must be 0 < maximumNumberOfPartitions <= 255."));
337337
// Zero is invalid, but in Java we can't distinguish None from Some(0)
338338
if maxPartitions == 0 {
339339
maxPartitions := 1;

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/Util.dfy‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -81,10 +81,10 @@ module DynamoDbEncryptionUtil {
8181
}
8282
}
8383

84-
const MAX_BUCKET_COUNT : nat := 255
84+
const MAX_PARTITION_COUNT : nat := 255
8585

8686
type PartitionBytes = x: seq<uint8> | Valid_PartitionBytes(x) witness []
87-
newtype OptPartitionCount = x: int | 0 <= x <= MAX_BUCKET_COUNT
87+
newtype OptPartitionCount = x: int | 0 <= x <= MAX_PARTITION_COUNT
8888

8989
function method PartitionBytesToNumber(x : PartitionBytes) : PartitionNumber
9090
{
@@ -115,7 +115,7 @@ module DynamoDbEncryptionUtil {
115115
predicate method Valid_PartitionBytes(x : seq<uint8>)
116116
{
117117
&& |x| <= 1
118-
&& (|x| == 1 ==> (0 < x[0] < (MAX_BUCKET_COUNT as uint8)))
118+
&& (|x| == 1 ==> (0 < x[0] < (MAX_PARTITION_COUNT as uint8)))
119119
}
120120

121121
function printFromFunction<T>(x: T): () {

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -625,7 +625,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
625625
nameonly input: ComAmazonawsDynamodbTypes.QueryInput
626626
)
627627
datatype GetNumberOfQueriesOutput = | GetNumberOfQueriesOutput (
628-
nameonly numberOfQueries: AwsCryptographyDbEncryptionSdkDynamoDbTypes.BucketCount
628+
nameonly numberOfQueries: AwsCryptographyDbEncryptionSdkDynamoDbTypes.PartitionCount
629629
)
630630
datatype PutItemInputTransformInput = | PutItemInputTransformInput (
631631
nameonly sdkInput: ComAmazonawsDynamodbTypes.PutItemInput
@@ -796,8 +796,8 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
796796
tmp5.search.Some? ==>
797797
var tmps6 := set t6 | t6 in tmp5.search.value.versions;
798798
forall tmp6 :: tmp6 in tmps6 ==>
799-
tmp6.bucketSelector.Some? ==>
800-
tmp6.bucketSelector.value.ValidState()
799+
tmp6.partitionSelector.Some? ==>
800+
tmp6.partitionSelector.value.ValidState()
801801
requires var tmps7 := set t7 | t7 in config.tableEncryptionConfigs.Values;
802802
forall tmp7 :: tmp7 in tmps7 ==>
803803
tmp7.search.Some? ==>
@@ -836,8 +836,8 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
836836
modifies set tmps16 <- set t16 <- config.tableEncryptionConfigs.Values | true
837837
&& t16.search.Some?
838838
, t17 <- t16.search.value.versions | true
839-
&& t17.bucketSelector.Some?
840-
:: t17.bucketSelector.value,
839+
&& t17.partitionSelector.Some?
840+
:: t17.partitionSelector.value,
841841
obj <- tmps16.Modifies | obj in tmps16.Modifies :: obj
842842
modifies set tmps18 <- set t18 <- config.tableEncryptionConfigs.Values | true
843843
&& t18.search.Some?
@@ -878,8 +878,8 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
878878
) - ( set tmps27 <- set t27 <- config.tableEncryptionConfigs.Values | true
879879
&& t27.search.Some?
880880
, t28 <- t27.search.value.versions | true
881-
&& t28.bucketSelector.Some?
882-
:: t28.bucketSelector.value,
881+
&& t28.partitionSelector.Some?
882+
:: t28.partitionSelector.value,
883883
obj <- tmps27.Modifies | obj in tmps27.Modifies :: obj
884884
) - ( set tmps29 <- set t29 <- config.tableEncryptionConfigs.Values | true
885885
&& t29.search.Some?
@@ -923,8 +923,8 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
923923
tmp38.search.Some? ==>
924924
var tmps39 := set t39 | t39 in tmp38.search.value.versions;
925925
forall tmp39 :: tmp39 in tmps39 ==>
926-
tmp39.bucketSelector.Some? ==>
927-
tmp39.bucketSelector.value.ValidState()
926+
tmp39.partitionSelector.Some? ==>
927+
tmp39.partitionSelector.value.ValidState()
928928
ensures var tmps40 := set t40 | t40 in config.tableEncryptionConfigs.Values;
929929
forall tmp40 :: tmp40 in tmps40 ==>
930930
tmp40.search.Some? ==>

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ use aws.cryptography.dbEncryptionSdk.dynamoDb.itemEncryptor#DynamoDbItemEncrypto
1414
use aws.cryptography.dbEncryptionSdk.dynamoDb#VersionNumber
1515
use aws.cryptography.dbEncryptionSdk.structuredEncryption#StructuredEncryption
1616
use aws.cryptography.materialProviders#AwsCryptographicMaterialProviders
17-
use aws.cryptography.dbEncryptionSdk.dynamoDb#BucketCount
17+
use aws.cryptography.dbEncryptionSdk.dynamoDb#PartitionCount
1818

1919
use aws.polymorph#localService
2020
use aws.polymorph#javadoc
@@ -76,7 +76,7 @@ map StringMap {
7676
value : String
7777
}
7878

79-
@javadoc("Return the necessary number of query operations for this query, based on bucket usage.")
79+
@javadoc("Return the necessary number of query operations for this query, based on partition usage.")
8080
operation GetNumberOfQueries {
8181
input: GetNumberOfQueriesInput,
8282
output: GetNumberOfQueriesOutput,
@@ -95,7 +95,7 @@ structure GetNumberOfQueriesInput {
9595
//# This operation MUST return the number of queries necessary.
9696
structure GetNumberOfQueriesOutput {
9797
@required
98-
numberOfQueries: BucketCount
98+
numberOfQueries: PartitionCount
9999
}
100100

101101

DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/BucketSelector.go renamed to DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/PartitionSelector.go

Lines changed: 6 additions & 6 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)