Skip to content

Commit 4f7e715

Browse files
lucasmcdonald3lucasmcdonald3
authored
chore: Rename AtomicPrimitives Dafny module name (#589)
1 parent ce33f76 commit 4f7e715

Some content is hidden

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

41 files changed

+227
-232
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
5555
import StormTracker
5656
import StormTrackingCMC
5757
import Crypto = AwsCryptographyPrimitivesTypes
58-
import Aws.Cryptography.Primitives
58+
import AtomicPrimitives
5959
import opened AwsKmsUtils
6060
import DefaultClientSupplier
6161
import Materials
@@ -69,7 +69,7 @@ module AwsCryptographyMaterialProvidersOperations refines AbstractAwsCryptograph
6969
import UUID
7070

7171
datatype Config = Config(
72-
nameonly crypto: Primitives.AtomicPrimitivesClient
72+
nameonly crypto: AtomicPrimitives.AtomicPrimitivesClient
7373
)
7474

7575
type InternalConfig = Config

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ module DefaultCMM {
1919
import UTF8
2020
import Types = AwsCryptographyMaterialProvidersTypes
2121
import Crypto = AwsCryptographyPrimitivesTypes
22-
import Aws.Cryptography.Primitives
22+
import AtomicPrimitives
2323
import Defaults
2424
import Commitment
2525
import Seq
@@ -28,7 +28,7 @@ module DefaultCMM {
2828
class DefaultCMM
2929
extends CMM.VerifiableInterface
3030
{
31-
const cryptoPrimitives: Primitives.AtomicPrimitivesClient
31+
const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
3232

3333
predicate ValidState()
3434
ensures ValidState() ==> History in Modifies
@@ -51,7 +51,7 @@ module DefaultCMM {
5151
//# the caller MUST provide the following value:
5252
//# - [Keyring](#keyring)
5353
k: Types.IKeyring,
54-
c: Primitives.AtomicPrimitivesClient
54+
c: AtomicPrimitives.AtomicPrimitivesClient
5555
)
5656
requires k.ValidState() && c.ValidState()
5757
ensures keyring == k && cryptoPrimitives == c

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,11 @@
33

44
include "AwsCryptographyMaterialProvidersOperations.dfy"
55

6-
module
7-
{:extern "software.amazon.cryptography.materialproviders.internaldafny" }
8-
MaterialProviders refines AbstractAwsCryptographyMaterialProvidersService
6+
module {:extern "software.amazon.cryptography.materialproviders.internaldafny" } MaterialProviders refines AbstractAwsCryptographyMaterialProvidersService
97
{
108

119
import Operations = AwsCryptographyMaterialProvidersOperations
12-
import Aws.Cryptography.Primitives
10+
import AtomicPrimitives
1311
import Crypto = AwsCryptographyPrimitivesTypes
1412

1513
function method DefaultMaterialProvidersConfig(): MaterialProvidersConfig
@@ -22,11 +20,11 @@ module
2220
ensures res.Success? ==>
2321
&& res.value is MaterialProvidersClient
2422
{
25-
var maybeCrypto := Primitives.AtomicPrimitives();
23+
var maybeCrypto := AtomicPrimitives.AtomicPrimitives();
2624
var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto
2725
.MapFailure(e => Types.AwsCryptographyPrimitives(e));
28-
assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient;
29-
var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient;
26+
assert cryptoPrimitivesX is AtomicPrimitives.AtomicPrimitivesClient;
27+
var cryptoPrimitives := cryptoPrimitivesX as AtomicPrimitives.AtomicPrimitivesClient;
3028

3129
var client := new MaterialProvidersClient(Operations.Config( crypto := cryptoPrimitives ));
3230
return Success(client);

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EcdhEdkWrapping.dfy

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping {
2020
import opened AlgorithmSuites
2121
import PrimitiveTypes = AwsCryptographyPrimitivesTypes
2222
import Types = AwsCryptographyMaterialProvidersTypes
23-
import Aws.Cryptography.Primitives
23+
import AtomicPrimitives
2424
import Materials
2525

2626
datatype EcdhUnwrapInfo = EcdhUnwrapInfo()
@@ -34,15 +34,15 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping {
3434
const sharedSecret: seq<uint8>
3535
const keyringVersion: seq<uint8>
3636
const curveSpec: PrimitiveTypes.ECDHCurveSpec
37-
const crypto: Primitives.AtomicPrimitivesClient
37+
const crypto: AtomicPrimitives.AtomicPrimitivesClient
3838

3939
constructor(
4040
senderPublicKey: seq<uint8>,
4141
recipientPublicKey: seq<uint8>,
4242
sharedSecret: seq<uint8>,
4343
keyringVersion: seq<uint8>,
4444
curveSpec: PrimitiveTypes.ECDHCurveSpec,
45-
crypto: Primitives.AtomicPrimitivesClient
45+
crypto: AtomicPrimitives.AtomicPrimitivesClient
4646
)
4747
requires crypto.ValidState()
4848
ensures
@@ -228,12 +228,12 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping {
228228
{
229229
const sharedSecret: seq<uint8>
230230
const fixedInfo: seq<uint8>
231-
const crypto: Primitives.AtomicPrimitivesClient
231+
const crypto: AtomicPrimitives.AtomicPrimitivesClient
232232

233233
constructor(
234234
sharedSecret: seq<uint8>,
235235
fixedInfo: seq<uint8>,
236-
crypto: Primitives.AtomicPrimitivesClient
236+
crypto: AtomicPrimitives.AtomicPrimitivesClient
237237
)
238238
requires crypto.ValidState()
239239
ensures
@@ -316,12 +316,12 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping {
316316
{
317317
const sharedSecret: seq<uint8>
318318
const fixedInfo: seq<uint8>
319-
const crypto: Primitives.AtomicPrimitivesClient
319+
const crypto: AtomicPrimitives.AtomicPrimitivesClient
320320

321321
constructor(
322322
sharedSecret: seq<uint8>,
323323
fixedInfo: seq<uint8>,
324-
crypto: Primitives.AtomicPrimitivesClient
324+
crypto: AtomicPrimitives.AtomicPrimitivesClient
325325
)
326326
requires crypto.ValidState()
327327
ensures
@@ -461,7 +461,7 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping {
461461
sharedSecret: seq<uint8>,
462462
fixedInfo: seq<uint8>,
463463
salt: seq<uint8>,
464-
crypto: Primitives.AtomicPrimitivesClient
464+
crypto: AtomicPrimitives.AtomicPrimitivesClient
465465
) returns (res :Result<seq<uint8>, Types.Error>)
466466
requires crypto.ValidState()
467467
modifies crypto.Modifies

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ module EdkWrapping {
2020
import opened IntermediateKeyWrapping
2121
import Crypto = AwsCryptographyPrimitivesTypes
2222
import Types = AwsCryptographyMaterialProvidersTypes
23-
import Aws.Cryptography.Primitives
23+
import AtomicPrimitives
2424
import Materials
2525
import AlgorithmSuites
2626

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/IntermediateKeyWrapping.dfy

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ module IntermediateKeyWrapping {
1515
import opened AlgorithmSuites
1616
import Crypto = AwsCryptographyPrimitivesTypes
1717
import Types = AwsCryptographyMaterialProvidersTypes
18-
import Aws.Cryptography.Primitives
18+
import AtomicPrimitives
1919
import Materials
2020
import UTF8
2121
import HKDF
@@ -74,11 +74,11 @@ module IntermediateKeyWrapping {
7474
[])
7575

7676
{
77-
var maybeCrypto := Primitives.AtomicPrimitives();
77+
var maybeCrypto := AtomicPrimitives.AtomicPrimitives();
7878
var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto
7979
.MapFailure(e => Types.AwsCryptographyPrimitives(e));
80-
assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient;
81-
var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient;
80+
assert cryptoPrimitivesX is AtomicPrimitives.AtomicPrimitivesClient;
81+
var cryptoPrimitives := cryptoPrimitivesX as AtomicPrimitives.AtomicPrimitivesClient;
8282
// Deserialize the Intermediate-Wrapped material
8383
var deserializedWrapped :- DeserializeIntermediateWrappedMaterial(wrappedMaterial, algorithmSuite);
8484
var DeserializedIntermediateWrappedMaterial(encryptedPdk, providerWrappedIkm) := deserializedWrapped;
@@ -168,12 +168,12 @@ module IntermediateKeyWrapping {
168168
&& |maybeIntermediateWrappedMat.value.encryptedPdk| ==
169169
(AlgorithmSuites.GetEncryptKeyLength(algorithmSuite) + AlgorithmSuites.GetEncryptTagLength(algorithmSuite)) as nat
170170
{
171-
var maybeCrypto := Primitives.AtomicPrimitives();
171+
var maybeCrypto := AtomicPrimitives.AtomicPrimitives();
172172
var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto
173173
.MapFailure(e => Types.AwsCryptographyPrimitives(e));
174174

175-
assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient;
176-
var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient;
175+
assert cryptoPrimitivesX is AtomicPrimitives.AtomicPrimitivesClient;
176+
var cryptoPrimitives := cryptoPrimitivesX as AtomicPrimitives.AtomicPrimitivesClient;
177177

178178

179179
// Use the provider to get the intermediate key material, and wrapped intermediate key material
@@ -252,7 +252,7 @@ module IntermediateKeyWrapping {
252252
wrapInfo := res.value.wrapInfo)),
253253
[])
254254
{
255-
var maybeCrypto := Primitives.AtomicPrimitives();
255+
var maybeCrypto := AtomicPrimitives.AtomicPrimitives();
256256
var cryptoPrimitives :- maybeCrypto
257257
.MapFailure(e => Types.AwsCryptographyPrimitives(e));
258258

@@ -305,7 +305,7 @@ module IntermediateKeyWrapping {
305305
intermediateMaterial: seq<uint8>,
306306
algorithmSuite: Types.AlgorithmSuiteInfo,
307307
encryptionContext: Types.EncryptionContext,
308-
cryptoPrimitives: Primitives.AtomicPrimitivesClient
308+
cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
309309
)
310310
returns (res: Result<PdkEncryptionAndSymmetricSigningKeys, Types.Error>)
311311
requires cryptoPrimitives.ValidState()

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/MaterialWrapping.dfy

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ module MaterialWrapping {
1313
import opened Actions
1414
import opened Wrappers
1515
import Types = AwsCryptographyMaterialProvidersTypes
16-
import Aws.Cryptography.Primitives
16+
import AtomicPrimitives
1717
import Materials
1818
import AlgorithmSuites
1919

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
3838
import MaterialWrapping
3939
import EcdhEdkWrapping
4040
import ErrorMessages
41-
import Aws.Cryptography.Primitives
41+
import AtomicPrimitives
4242
import CanonicalEncryptionContext
4343

4444
const AWS_KMS_ECDH_KEYRING_VERSION := RawECDHKeyring.RAW_ECDH_KEYRING_VERSION
@@ -58,7 +58,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
5858
const keyAgreementScheme: Types.KmsEcdhStaticConfigurations
5959
const curveSpec: PrimitiveTypes.ECDHCurveSpec
6060
const grantTokens: KMS.GrantTokenList
61-
const cryptoPrimitives: Primitives.AtomicPrimitivesClient
61+
const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
6262

6363
ghost predicate ValidState()
6464
ensures ValidState() ==> History in Modifies
@@ -95,7 +95,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
9595
recipientPublicKey: KMS.PublicKeyType,
9696
compressedSenderPublicKey: Option<seq<uint8>>,
9797
compressedRecipientPublicKey: seq<uint8>,
98-
cryptoPrimitives : Primitives.AtomicPrimitivesClient
98+
cryptoPrimitives : AtomicPrimitives.AtomicPrimitivesClient
9999
)
100100
requires client.ValidState()
101101
requires cryptoPrimitives.ValidState()
@@ -438,7 +438,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
438438
Types.Error>
439439
{
440440
const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey
441-
const cryptoPrimitives: Primitives.AtomicPrimitivesClient
441+
const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
442442
const recipientPublicKey: seq<uint8>
443443
const client: KMS.IKMSClient
444444
const grantTokens: KMS.GrantTokenList
@@ -447,7 +447,7 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
447447

448448
constructor(
449449
materials: Materials.DecryptionMaterialsPendingPlaintextDataKey,
450-
cryptoPrimitives: Primitives.AtomicPrimitivesClient,
450+
cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient,
451451
recipientPublicKey: seq<uint8>,
452452
client: KMS.IKMSClient,
453453
grantTokens: KMS.GrantTokenList,

‎AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ module AwsKmsHierarchicalKeyring {
5252
import HKDF
5353
import HMAC
5454
import opened AESEncryption
55-
import Aws.Cryptography.Primitives
55+
import AtomicPrimitives
5656
import ErrorMessages
5757

5858
const BRANCH_KEY_STORE_GSI := "Active-Keys"
@@ -141,7 +141,7 @@ module AwsKmsHierarchicalKeyring {
141141
const branchKeyIdSupplier: Option<Types.IBranchKeyIdSupplier>
142142
const keyStore: KeyStore.IKeyStoreClient
143143
const ttlSeconds: Types.PositiveLong
144-
const cryptoPrimitives: Primitives.AtomicPrimitivesClient
144+
const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
145145
const cache: Types.ICryptographicMaterialsCache
146146
const partitionIdBytes: seq<uint8>
147147
const logicalKeyStoreNameBytes: seq<uint8>
@@ -181,7 +181,7 @@ module AwsKmsHierarchicalKeyring {
181181
cmc: Types.ICryptographicMaterialsCache,
182182
partitionIdBytes: seq<uint8>,
183183
logicalKeyStoreNameBytes: seq<uint8>,
184-
cryptoPrimitives : Primitives.AtomicPrimitivesClient
184+
cryptoPrimitives : AtomicPrimitives.AtomicPrimitivesClient
185185
)
186186
requires ttlSeconds >= 0
187187
requires keyStore.ValidState() && cryptoPrimitives.ValidState()
@@ -408,7 +408,7 @@ module AwsKmsHierarchicalKeyring {
408408
method GetActiveCacheId(
409409
branchKeyId: string,
410410
branchKeyIdUtf8: seq<uint8>,
411-
cryptoPrimitives: Primitives.AtomicPrimitivesClient
411+
cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
412412
)
413413
returns (cacheId: Result<seq<uint8>, Types.Error>)
414414

@@ -542,7 +542,7 @@ module AwsKmsHierarchicalKeyring {
542542
branchKey: seq<uint8>,
543543
salt: seq<uint8>,
544544
purpose: Option<seq<uint8>>,
545-
cryptoPrimitives: Primitives.AtomicPrimitivesClient
545+
cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
546546
)
547547
returns (output: Result<seq<uint8>, Types.Error>)
548548

@@ -657,7 +657,7 @@ module AwsKmsHierarchicalKeyring {
657657
{
658658
const materials: Materials.DecryptionMaterialsPendingPlaintextDataKey
659659
const keyStore: KeyStore.IKeyStoreClient
660-
const cryptoPrimitives: Primitives.AtomicPrimitivesClient
660+
const cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
661661
const branchKeyId: string
662662
const ttlSeconds: Types.PositiveLong
663663
const cache: Types.ICryptographicMaterialsCache
@@ -667,7 +667,7 @@ module AwsKmsHierarchicalKeyring {
667667
constructor(
668668
materials: Materials.DecryptionMaterialsPendingPlaintextDataKey,
669669
keyStore: KeyStore.IKeyStoreClient,
670-
cryptoPrimitives: Primitives.AtomicPrimitivesClient,
670+
cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient,
671671
branchKeyId: string,
672672
ttlSeconds: Types.PositiveLong,
673673
cache: Types.ICryptographicMaterialsCache,
@@ -757,11 +757,11 @@ module AwsKmsHierarchicalKeyring {
757757

758758
// We need to create a new client here so that we can reason about the state of the client
759759
// down the line. This is ok because the only state tracked is the client's history.
760-
var maybeCrypto := Primitives.AtomicPrimitives();
760+
var maybeCrypto := AtomicPrimitives.AtomicPrimitives();
761761
var cryptoPrimitivesX : Crypto.IAwsCryptographicPrimitivesClient :- maybeCrypto
762762
.MapFailure(e => Types.AwsCryptographyPrimitives(e));
763-
assert cryptoPrimitivesX is Primitives.AtomicPrimitivesClient;
764-
var cryptoPrimitives := cryptoPrimitivesX as Primitives.AtomicPrimitivesClient;
763+
assert cryptoPrimitivesX is AtomicPrimitives.AtomicPrimitivesClient;
764+
var cryptoPrimitives := cryptoPrimitivesX as AtomicPrimitives.AtomicPrimitivesClient;
765765

766766
var kmsHierarchyUnwrap := new KmsHierarchyUnwrapKeyMaterial(
767767
branchKey,
@@ -785,7 +785,7 @@ module AwsKmsHierarchicalKeyring {
785785
method GetVersionCacheId(
786786
branchKeyIdUtf8: seq<uint8>, // The branch key as Bytes
787787
branchKeyVersion: string,
788-
cryptoPrimitives: Primitives.AtomicPrimitivesClient
788+
cryptoPrimitives: AtomicPrimitives.AtomicPrimitivesClient
789789
)
790790
returns (cacheId: Result<seq<uint8>, Types.Error>)
791791
ensures cacheId.Success? ==> |cacheId.value| == 48
@@ -931,13 +931,13 @@ module AwsKmsHierarchicalKeyring {
931931
const branchKey: seq<uint8>
932932
const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes
933933
const branchKeyVersionAsBytes: seq<uint8>
934-
const crypto: Primitives.AtomicPrimitivesClient
934+
const crypto: AtomicPrimitives.AtomicPrimitivesClient
935935

936936
constructor(
937937
branchKey: seq<uint8>,
938938
branchKeyIdUtf8: UTF8.ValidUTF8Bytes,
939939
branchKeyVersionAsBytes: seq<uint8>,
940-
crypto: Primitives.AtomicPrimitivesClient
940+
crypto: AtomicPrimitives.AtomicPrimitivesClient
941941
)
942942
requires crypto.ValidState()
943943
ensures
@@ -1070,13 +1070,13 @@ module AwsKmsHierarchicalKeyring {
10701070
const branchKey: seq<uint8>
10711071
const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes
10721072
const branchKeyVersionAsBytes: seq<uint8>
1073-
const crypto: Primitives.AtomicPrimitivesClient
1073+
const crypto: AtomicPrimitives.AtomicPrimitivesClient
10741074

10751075
constructor(
10761076
branchKey: seq<uint8>,
10771077
branchKeyIdUtf8 : UTF8.ValidUTF8Bytes,
10781078
branchKeyVersionAsBytes: seq<uint8>,
1079-
crypto: Primitives.AtomicPrimitivesClient
1079+
crypto: AtomicPrimitives.AtomicPrimitivesClient
10801080
)
10811081
requires crypto.ValidState()
10821082
ensures
@@ -1160,13 +1160,13 @@ module AwsKmsHierarchicalKeyring {
11601160
const branchKey: seq<uint8>
11611161
const branchKeyIdUtf8 : UTF8.ValidUTF8Bytes
11621162
const branchKeyVersionAsBytes: seq<uint8>
1163-
const crypto: Primitives.AtomicPrimitivesClient
1163+
const crypto: AtomicPrimitives.AtomicPrimitivesClient
11641164

11651165
constructor(
11661166
branchKey: seq<uint8>,
11671167
branchKeyIdUtf8 : UTF8.ValidUTF8Bytes,
11681168
branchKeyVersionAsBytes: seq<uint8>,
1169-
crypto: Primitives.AtomicPrimitivesClient
1169+
crypto: AtomicPrimitives.AtomicPrimitivesClient
11701170
)
11711171
requires crypto.ValidState()
11721172
ensures

0 commit comments

Comments
 (0)