Skip to content

Commit 571e3c5

Browse files
ajewellamzajewellamz
authored
chore(dafny): more using uint64 instead of nat (#1490)
1 parent 49e596b commit 571e3c5

69 files changed

Lines changed: 957 additions & 564 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.

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsArnParsing.dfy‎

Lines changed: 38 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -9,19 +9,21 @@ module AwsArnParsing {
99
import opened Wrappers
1010
import opened Seq
1111
import opened UInt = StandardLibrary.UInt
12+
import opened StandardLibrary.MemoryMath
1213
import Types = AwsCryptographyMaterialProvidersTypes
1314
import DDB = ComAmazonawsDynamodbTypes
1415
import UTF8
1516

16-
const MAX_AWS_KMS_IDENTIFIER_LENGTH := 2048
17+
const MAX_AWS_KMS_IDENTIFIER_LENGTH := 2048 as uint64
1718

1819
datatype AwsResource = AwsResource(
1920
resourceType: string,
2021
value: string
2122
) {
2223
predicate method Valid()
2324
{
24-
&& 0 < |value|
25+
SequenceIsSafeBecauseItIsInMemory(value);
26+
&& 0 < |value| as uint64
2527
}
2628

2729
function method ToString(): string
@@ -43,11 +45,15 @@ module AwsArnParsing {
4345
) {
4446
predicate method Valid()
4547
{
48+
SequenceIsSafeBecauseItIsInMemory(partition);
49+
SequenceIsSafeBecauseItIsInMemory(service);
50+
SequenceIsSafeBecauseItIsInMemory(region);
51+
SequenceIsSafeBecauseItIsInMemory(account);
4652
&& arnLiteral == "arn"
47-
&& 0 < |partition|
48-
&& 0 < |service|
49-
&& 0 < |region|
50-
&& 0 < |account|
53+
&& 0 < |partition| as uint64
54+
&& 0 < |service| as uint64
55+
&& 0 < |region| as uint64
56+
&& 0 < |account| as uint64
5157
&& resource.Valid()
5258
}
5359

@@ -116,9 +122,10 @@ module AwsArnParsing {
116122
{
117123
var info := Split(identifier, '/');
118124

119-
:- Need(info[0] != "key", "Malformed raw key id: " + identifier);
125+
:- Need(info[0 as uint32] != "key", "Malformed raw key id: " + identifier);
126+
SequenceIsSafeBecauseItIsInMemory(info);
120127

121-
if |info| == 1 then
128+
if |info| as uint64 == 1 then
122129
ParseAwsKmsResources("key/" + identifier)
123130
else
124131
ParseAwsKmsResources(identifier)
@@ -127,11 +134,12 @@ module AwsArnParsing {
127134
function method ParseAwsKmsResources(identifier: string): (result: Result<AwsKmsResource, string>)
128135
{
129136
var info := Split(identifier, '/');
137+
SequenceIsSafeBecauseItIsInMemory(info);
130138

131-
:- Need(|info| > 1, "Malformed resource: " + identifier);
139+
:- Need(|info| as uint64 > 1, "Malformed resource: " + identifier);
132140

133-
var resourceType := info[0];
134-
var value := Join(info[1..], "/");
141+
var resourceType := info[0 as uint32];
142+
var value := Join(info[1 as uint32 ..], "/");
135143

136144
var resource := AwsResource(resourceType, value);
137145

@@ -239,17 +247,19 @@ module AwsArnParsing {
239247
&& |Split(identifier, ':')[4]| > 0
240248
{
241249
var components := Split(identifier, ':');
250+
SequenceIsSafeBecauseItIsInMemory(components);
242251

243-
:- Need(6 == |components|, "Malformed arn: " + identifier);
244252

245-
var resource :- ParseAwsKmsResources(components[5]);
253+
:- Need(6 == |components| as uint64, "Malformed arn: " + identifier);
254+
255+
var resource :- ParseAwsKmsResources(components[5 as uint32]);
246256

247257
var arn := AwsArn(
248-
components[0],
249-
components[1],
250-
components[2],
251-
components[3],
252-
components[4],
258+
components[0 as uint32],
259+
components[1 as uint32],
260+
components[2 as uint32],
261+
components[3 as uint32],
262+
components[4 as uint32],
253263
resource
254264
);
255265

@@ -268,17 +278,18 @@ module AwsArnParsing {
268278
&& |Split(identifier, ':')[4]| > 0
269279
{
270280
var components := Split(identifier, ':');
281+
SequenceIsSafeBecauseItIsInMemory(components);
271282

272-
:- Need(6 == |components|, "Malformed arn: " + identifier);
283+
:- Need(6 == |components| as uint64, "Malformed arn: " + identifier);
273284

274-
var resource :- ParseAmazonDynamodbResources(components[5]);
285+
var resource :- ParseAmazonDynamodbResources(components[5 as uint32]);
275286

276287
var arn := AwsArn(
277-
components[0],
278-
components[1],
279-
components[2],
280-
components[3],
281-
components[4],
288+
components[0 as uint32],
289+
components[1 as uint32],
290+
components[2 as uint32],
291+
components[3 as uint32],
292+
components[4 as uint32],
282293
resource
283294
);
284295

@@ -454,7 +465,8 @@ module AwsArnParsing {
454465
): (res: Result<AwsKmsIdentifier, string>)
455466
{
456467
:- Need(UTF8.IsASCIIString(s), "Not a valid ASCII string.");
457-
:- Need(0 < |s| <= MAX_AWS_KMS_IDENTIFIER_LENGTH , "Identifier exceeds maximum length.");
468+
SequenceIsSafeBecauseItIsInMemory(s);
469+
:- Need(0 < |s| as uint64 <= MAX_AWS_KMS_IDENTIFIER_LENGTH, "Identifier exceeds maximum length.");
458470
ParseAwsKmsIdentifier(s)
459471
}
460472

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsCryptographyMaterialProvidersOperations.dfy‎

Lines changed: 13 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,7 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
3939
import opened D = DiscoveryMultiKeyring
4040
import opened MD = MrkAwareDiscoveryMultiKeyring
4141
import opened M = MrkAwareStrictMultiKeyring
42+
import opened StandardLibrary.MemoryMath
4243
import AwsKmsKeyring
4344
import AwsKmsHierarchicalKeyring
4445
import AwsKmsMrkKeyring
@@ -493,7 +494,8 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
493494
method CreateMultiKeyring ( config: InternalConfig, input: CreateMultiKeyringInput )
494495
returns (output: Result<IKeyring, Error>)
495496
{
496-
:- Need(input.generator.Some? || |input.childKeyrings| > 0,
497+
SequenceIsSafeBecauseItIsInMemory(input.childKeyrings);
498+
:- Need(input.generator.Some? || |input.childKeyrings| as uint64 > 0,
497499
Types.AwsCryptographicMaterialProvidersException(
498500
message := "Must include a generator keyring and/or at least one child keyring"));
499501

@@ -539,10 +541,12 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
539541
var namespaceAndName :- ParseKeyNamespaceAndName(input.keyNamespace, input.keyName);
540542
var (namespace, name) := namespaceAndName;
541543

542-
:- Need(|input.wrappingKey| == 16 || |input.wrappingKey| == 24 || |input.wrappingKey| == 32,
544+
SequenceIsSafeBecauseItIsInMemory(input.wrappingKey);
545+
var wrapping_key_size := |input.wrappingKey| as uint64;
546+
:- Need(wrapping_key_size == 16 || wrapping_key_size == 24 || wrapping_key_size == 32,
543547
Types.AwsCryptographicMaterialProvidersException(
544548
message := "Invalid wrapping key length"));
545-
:- Need(|input.wrappingKey| == wrappingAlg.keyLength as int,
549+
:- Need(wrapping_key_size == wrappingAlg.keyLength as uint64,
546550
Types.AwsCryptographicMaterialProvidersException(
547551
message := "Wrapping key length does not match specified wrapping algorithm"));
548552

@@ -783,7 +787,8 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
783787
{
784788
:- Need(input.underlyingCMM.Some? && input.keyring.None?, CmpError("CreateRequiredEncryptionContextCMM currently only supports cmm."));
785789
var keySet : set<UTF8.ValidUTF8Bytes> := set k <- input.requiredEncryptionContextKeys;
786-
:- Need(0 < |keySet|, CmpError("RequiredEncryptionContextCMM needs at least one requiredEncryptionContextKey."));
790+
SetIsSafeBecauseItIsInMemory(keySet);
791+
:- Need(0 < |keySet| as uint64, CmpError("RequiredEncryptionContextCMM needs at least one requiredEncryptionContextKey."));
787792
var cmm := new RequiredEncryptionContextCMM.RequiredEncryptionContextCMM(
788793
input.underlyingCMM.value,
789794
keySet);
@@ -809,14 +814,14 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
809814
return Success(cmc);
810815
case SingleThreaded(c) =>
811816
var cmc := new LocalCMC.LocalCMC(
812-
c.entryCapacity as nat,
813-
OptionalCountingNumber(c.entryPruningTailSize).UnwrapOr(1) as nat
817+
c.entryCapacity as uint64,
818+
OptionalCountingNumber(c.entryPruningTailSize).UnwrapOr(1) as uint64
814819
);
815820
return Success(cmc);
816821
case MultiThreaded(c) =>
817822
var cmc := new LocalCMC.LocalCMC(
818-
c.entryCapacity as nat,
819-
OptionalCountingNumber(c.entryPruningTailSize).UnwrapOr(1) as nat
823+
c.entryCapacity as uint64,
824+
OptionalCountingNumber(c.entryPruningTailSize).UnwrapOr(1) as uint64
820825
);
821826
var synCmc := new SynchronizedLocalCMC.SynchronizedLocalCMC(cmc);
822827
return Success(synCmc);

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy‎

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ include "../../../../../libraries/src/MutableMap/MutableMap.dfy"
77
module {:options "/functionSyntax:4" } LocalCMC {
88
import opened Wrappers
99
import opened StandardLibrary.UInt
10+
import opened StandardLibrary.MemoryMath
1011
import opened DafnyLibraries
1112
import Time
1213
import Types = AwsCryptographyMaterialProvidersTypes
@@ -351,7 +352,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
351352
// with the tail MUST be in the cache
352353
&& (forall c <- queue.Items :: c.identifier in cache.Keys() && cache.Select(c.identifier) == c)
353354

354-
&& cache.Size() <= entryCapacity
355+
&& (ValueIsSafeBecauseItIsInMemory(cache.Size()); cache.Size() as uint64 <= entryCapacity)
355356
}
356357

357358
var queue: DoublyLinkedCacheEntryList
@@ -360,14 +361,14 @@ module {:options "/functionSyntax:4" } LocalCMC {
360361
//= type=implication
361362
//# The local CMC MUST accept entry capacity values between zero
362363
//# and an implementation-defined maximum, inclusive.
363-
const entryCapacity: nat
364+
const entryCapacity: uint64
364365
//= aws-encryption-sdk-specification/framework/local-cryptographic-materials-cache.md#entry-pruning-tail-size
365366
//= type=implication
366367
//# The _entry pruning tail size_
367368
//# is the number of least recently used entries that the local CMC
368369
//# MUST check during [pruning](#pruning)
369370
//# for TTL-expired entries to evict.
370-
const entryPruningTailSize: nat
371+
const entryPruningTailSize: uint64
371372

372373
//= aws-encryption-sdk-specification/framework/local-cryptographic-materials-cache.md#initialization
373374
//= type=implication
@@ -379,8 +380,8 @@ module {:options "/functionSyntax:4" } LocalCMC {
379380
//#
380381
//# - [Entry Pruning Tail Size](#entry-pruning-tail-size)
381382
constructor(
382-
entryCapacity': nat,
383-
entryPruningTailSize': nat := 1
383+
entryCapacity': uint64,
384+
entryPruningTailSize': uint64 := 1
384385
)
385386
requires entryPruningTailSize' >= 1
386387
ensures
@@ -506,7 +507,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
506507
//= aws-encryption-sdk-specification/framework/local-cryptographic-materials-cache.md#entry-capacity
507508
//# The local CMC MUST NOT store more entries than this value,
508509
//# except temporarily while performing a Put Cache Entry operation.
509-
if entryCapacity == cache.Size() {
510+
if entryCapacity == cache.Size() as uint64 {
510511
assert 0 < |multiset(cache.Values())|;
511512
assert queue.tail.deref.identifier in cache.Keys();
512513
var _ :- DeleteCacheEntry'(Types.DeleteCacheEntryInput(
@@ -596,7 +597,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
596597
LemmaMutableMapContainsPreservesInjectivity(old@CAN_REMOVE(cache), cache);
597598
}
598599
assert |cache.Keys()| == |old@CAN_REMOVE(cache.Keys())| - 1;
599-
assert cache.Size() <= old@CAN_REMOVE(cache.Size()) <= entryCapacity;
600+
assert cache.Size() as uint64 <= old@CAN_REMOVE(cache.Size()) as uint64 <= entryCapacity;
600601
queue.remove(cell);
601602
assert multiset(cache.Values()) == multiset(queue.Items) by {
602603
var cacheMultiset := multiset(cache.Values());

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/StormTracker.dfy‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -151,7 +151,7 @@ module {:options "/functionSyntax:4" } StormTracker {
151151
inFlightTTL := cache.inFlightTTL as Types.PositiveLong;
152152
}
153153

154-
this.wrapped := new LocalCMC.LocalCMC(cache.entryCapacity as nat, cache.entryPruningTailSize.UnwrapOr(1) as nat);
154+
this.wrapped := new LocalCMC.LocalCMC(cache.entryCapacity as uint64, cache.entryPruningTailSize.UnwrapOr(1) as uint64);
155155
this.inFlight := new MutableMap();
156156
this.gracePeriod := gracePeriod;
157157
this.graceInterval := graceInterval;
@@ -334,8 +334,8 @@ module {:options "/functionSyntax:4" } StormTracker {
334334
// and T[0] is the most recent.
335335
var keySet := inFlight.Keys();
336336
var keys := SortedSets.ComputeSetToSequence(keySet);
337-
for i := 0 to |keys|
338-
invariant forall k | i <= k < |keys| :: keys[k] in inFlight.Keys()
337+
for i : uint64 := 0 to |keys| as uint64
338+
invariant forall k | i as nat <= k < |keys| :: keys[k] in inFlight.Keys()
339339
invariant ValidState()
340340
{
341341
reveal Seq.HasNoDuplicates();

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy‎

Lines changed: 12 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ include "../Keyrings/MultiKeyring.dfy"
1313
module DefaultCMM {
1414
import opened Wrappers
1515
import opened UInt = StandardLibrary.UInt
16+
import opened StandardLibrary.MemoryMath
1617
import AlgorithmSuites
1718
import Materials
1819
import CMM
@@ -89,8 +90,8 @@ module DefaultCMM {
8990
}
9091

9192
// The following are requirements for the CMM interface.
92-
// However they are requirments of intent
93-
// rather than something that can be verified programaticly.
93+
// However they are requirements of intent
94+
// rather than something that can be verified programmatically.
9495
// The configured keyring could violate these properties.
9596
// This is why these are listed as exception and not implications.
9697
//
@@ -328,8 +329,8 @@ module DefaultCMM {
328329
}
329330

330331
// The following are requirements for the CMM interface.
331-
// However they are requirments of intent
332-
// rather than something that can be verified programaticly.
332+
// However they are requirements of intent
333+
// rather than something that can be verified programmatically.
333334
// The configured keyring could violate these properties.
334335
// This is why these are listed as exception and not implications.
335336
//
@@ -465,12 +466,13 @@ module DefaultCMM {
465466
var keysSet := input.reproducedEncryptionContext.value.Keys;
466467
ghost var keysSet' := keysSet;
467468
var keysSeq := SortedSets.ComputeSetToSequence(keysSet);
468-
var i := 0;
469-
while i < |keysSeq|
469+
var i : uint64 := 0;
470+
SequenceIsSafeBecauseItIsInMemory(keysSeq);
471+
while i < |keysSeq| as uint64
470472
invariant Seq.HasNoDuplicates(keysSeq)
471-
invariant forall j | 0 <= j < i && i < |keysSeq| :: keysSeq[j] !in keysSet'
472-
invariant forall j | i <= j < |keysSeq| :: keysSeq[j] in keysSet'
473-
invariant |keysSet'| == |keysSeq| - i
473+
invariant forall j | 0 <= j < i as nat && i as nat < |keysSeq| :: keysSeq[j] !in keysSet'
474+
invariant forall j | i as nat <= j < |keysSeq| :: keysSeq[j] in keysSet'
475+
invariant |keysSet'| == |keysSeq| - i as nat
474476
invariant forall key
475477
|
476478
&& key in input.reproducedEncryptionContext.value
@@ -490,7 +492,7 @@ module DefaultCMM {
490492
}
491493
keysSet' := keysSet' - {key};
492494
i := i + 1;
493-
assert forall j | i <= j < |keysSeq| :: keysSeq[j] in keysSet' by {
495+
assert forall j | i as nat <= j < |keysSeq| :: keysSeq[j] in keysSet' by {
494496
reveal Seq.HasNoDuplicates();
495497
}
496498
}

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CanonicalEncryptionContext.dfy‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ include "../Model/AwsCryptographyMaterialProvidersTypes.dfy"
66
module CanonicalEncryptionContext {
77
import opened StandardLibrary
88
import opened UInt = StandardLibrary.UInt
9+
import opened StandardLibrary.MemoryMath
910
import Types = AwsCryptographyMaterialProvidersTypes
1011
import opened Wrappers
1112
import Seq
@@ -24,11 +25,12 @@ module CanonicalEncryptionContext {
2425
):
2526
(res: Result<seq<uint8>, Types.Error>)
2627
{
27-
:- Need(|encryptionContext| < UINT16_LIMIT,
28+
MapIsSafeBecauseItIsInMemory(encryptionContext);
29+
:- Need(|encryptionContext| as uint64 < UINT16_LIMIT as uint64,
2830
Types.AwsCryptographicMaterialProvidersException( message := "Encryption Context is too large" ));
2931
var keys := SortedSets.ComputeSetToOrderedSequence2(encryptionContext.Keys, UInt.UInt8Less);
3032

31-
if |keys| == 0 then
33+
if |keys| as uint16 == 0 then
3234
Success([])
3335
else
3436
var KeyIntoPairBytes := k

0 commit comments

Comments
 (0)