Skip to content

Commit 29bc52e

Browse files
ShubhamChaturvedi7Shubham Chaturvedi
andauthored
feat: mpl externs (#1105)
Co-authored-by: Shubham Chaturvedi <scchatur@amazon.com>
1 parent 6477639 commit 29bc52e

9 files changed

Lines changed: 300 additions & 44 deletions

File tree

.github/workflows/library_go_tests.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ jobs:
2525
ComAmazonawsKms,
2626
ComAmazonawsDynamodb,
2727
AwsCryptographyPrimitives,
28+
AwsCryptographicMaterialProviders,
2829
]
2930
go-version: ["1.23"]
3031
os: [

AwsCryptographicMaterialProviders/Makefile

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,6 @@
22
# SPDX-License-Identifier: Apache-2.0
33

44
CORES=2
5-
65
ENABLE_EXTERN_PROCESSING=1
76

87
include ../SharedMakefileV2.mk
@@ -68,6 +67,22 @@ SERVICE_DEPS_AwsCryptographyKeyStore := \
6867
ComAmazonawsDynamodb \
6968
AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
7069

70+
GO_MODULE_NAME="github.com/aws/aws-cryptographic-material-providers-library/mpl"
71+
72+
GO_DEPENDENCY_MODULE_NAMES := \
73+
--dependency-library-name=com.amazonaws.dynamodb=github.com/aws/aws-cryptographic-material-providers-library/dynamodb \
74+
--dependency-library-name=com.amazonaws.kms=github.com/aws/aws-cryptographic-material-providers-library/kms \
75+
--dependency-library-name=aws.cryptography.keyStore=github.com/aws/aws-cryptographic-material-providers-library/mpl \
76+
--dependency-library-name=aws.cryptography.primitives=github.com/aws/aws-cryptographic-material-providers-library/primitives \
77+
--dependency-library-name=sdk.com.amazonaws.dynamodb=github.com/aws/aws-sdk-go-v2/service/dynamodb \
78+
--dependency-library-name=sdk.com.amazonaws.kms=github.com/aws/aws-sdk-go-v2/service/kms
79+
80+
TRANSLATION_RECORD_GO := \
81+
StandardLibrary/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
82+
ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
83+
ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
84+
AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr
85+
7186
# Constants for languages that drop extern names (Python, Go)
7287

7388
MPL_CORE_TYPES_FILE_PATH=dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
package StormTrackingCMC
2+
3+
import (
4+
"sync"
5+
"time"
6+
7+
"github.com/aws/aws-cryptographic-material-providers-library/mpl/AwsCryptographyMaterialProvidersTypes"
8+
"github.com/aws/aws-cryptographic-material-providers-library/mpl/StormTracker"
9+
_dafny "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
10+
"github.com/dafny-lang/DafnyStandardLibGo/Wrappers"
11+
DafnyTime "github.com/dafny-lang/DafnyStandardLibGo/Time_"
12+
)
13+
14+
type StormTrackingCMC struct {
15+
stormTracker *StormTracker.StormTracker
16+
//The Lock contention is not tested.
17+
sync.Mutex
18+
}
19+
20+
func New_StormTrackingCMC_(stormTracker *StormTracker.StormTracker) *StormTrackingCMC {
21+
return &StormTrackingCMC{stormTracker: stormTracker}
22+
}
23+
24+
func (cmc *StormTrackingCMC) PutCacheEntry(input AwsCryptographyMaterialProvidersTypes.PutCacheEntryInput) Wrappers.Result {
25+
cmc.Lock()
26+
defer cmc.Unlock()
27+
return cmc.stormTracker.PutCacheEntry(input)
28+
}
29+
func (cmc *StormTrackingCMC) PutCacheEntry_k(input AwsCryptographyMaterialProvidersTypes.PutCacheEntryInput) Wrappers.Result {
30+
cmc.Lock()
31+
defer cmc.Unlock()
32+
return cmc.stormTracker.PutCacheEntry(input)
33+
}
34+
func (cmc *StormTrackingCMC) UpdateUsageMetadata(input AwsCryptographyMaterialProvidersTypes.UpdateUsageMetadataInput) Wrappers.Result {
35+
cmc.Lock()
36+
defer cmc.Unlock()
37+
return cmc.stormTracker.UpdateUsageMetadata(input)
38+
}
39+
func (cmc *StormTrackingCMC) UpdateUsageMetadata_k(input AwsCryptographyMaterialProvidersTypes.UpdateUsageMetadataInput) Wrappers.Result {
40+
cmc.Lock()
41+
defer cmc.Unlock()
42+
return cmc.stormTracker.UpdateUsageMetadata(input)
43+
}
44+
func (cmc *StormTrackingCMC) GetCacheEntry(input AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput) Wrappers.Result {
45+
return cmc.GetCacheEntry_k(input)
46+
}
47+
func (cmc *StormTrackingCMC) GetCacheEntry_k(input AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput) Wrappers.Result {
48+
maxInFlight := DafnyTime.CurrentRelativeTimeMilli() + cmc.stormTracker.InFlightTTL
49+
for {
50+
res := cmc.GetFromInner(input)
51+
if res.IsFailure() {
52+
return Companion_Default___.CreateGetCacheEntryFailure(res.Dtor_error().(AwsCryptographyMaterialProvidersTypes.Error))
53+
} else if res.Dtor_value().(StormTracker.CacheState).Is_Full() {
54+
return Companion_Default___.CreateGetCacheEntrySuccess(res.Dtor_value().(StormTracker.CacheState).Dtor_data())
55+
} else if res.Dtor_value().(StormTracker.CacheState).Is_EmptyFetch() {
56+
return Companion_Default___.CreateGetCacheEntryFailure(AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_EntryDoesNotExist_(_dafny.SeqOfChars([]_dafny.Char("Entry doesn't exists")...)))
57+
} else {
58+
if DafnyTime.CurrentRelativeTimeMilli() <= maxInFlight {
59+
time.Sleep(time.Duration(cmc.stormTracker.SleepMilli))
60+
} else {
61+
return Companion_Default___.CreateGetCacheEntryFailure(AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_InFlightTTLExceeded_(_dafny.SeqOfChars([]_dafny.Char("Storm cache inFlightTTL exceeded.")...)))
62+
}
63+
}
64+
}
65+
}
66+
func (cmc *StormTrackingCMC) DeleteCacheEntry(input AwsCryptographyMaterialProvidersTypes.DeleteCacheEntryInput) Wrappers.Result {
67+
cmc.Lock()
68+
defer cmc.Unlock()
69+
return cmc.stormTracker.DeleteCacheEntry(input)
70+
71+
}
72+
func (cmc *StormTrackingCMC) DeleteCacheEntry_k(input AwsCryptographyMaterialProvidersTypes.DeleteCacheEntryInput) Wrappers.Result {
73+
cmc.Lock()
74+
defer cmc.Unlock()
75+
return cmc.stormTracker.DeleteCacheEntry(input)
76+
}
77+
78+
func (cmc *StormTrackingCMC) String() string {
79+
return "StormTrackerCMC"
80+
}
81+
82+
func (cmc *StormTrackingCMC) GetFromInner(input AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput) Wrappers.Result {
83+
cmc.Lock()
84+
defer cmc.Unlock()
85+
return cmc.stormTracker.GetFromCache(input)
86+
}
Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
package SynchronizedLocalCMC
2+
3+
import (
4+
"sync"
5+
6+
"github.com/aws/aws-cryptographic-material-providers-library/mpl/AwsCryptographyMaterialProvidersTypes"
7+
"github.com/aws/aws-cryptographic-material-providers-library/mpl/LocalCMC"
8+
"github.com/dafny-lang/DafnyStandardLibGo/Wrappers"
9+
)
10+
11+
type SynchronizedLocalCMC struct {
12+
localCMC *LocalCMC.LocalCMC
13+
sync.Mutex
14+
}
15+
16+
func New_SynchronizedLocalCMC_(localCMC *LocalCMC.LocalCMC) *SynchronizedLocalCMC {
17+
return &SynchronizedLocalCMC{localCMC: localCMC}
18+
}
19+
20+
func (cmc *SynchronizedLocalCMC) PutCacheEntry(input AwsCryptographyMaterialProvidersTypes.PutCacheEntryInput) Wrappers.Result {
21+
cmc.Lock()
22+
defer cmc.Unlock()
23+
return cmc.localCMC.PutCacheEntry(input)
24+
}
25+
func (cmc *SynchronizedLocalCMC) PutCacheEntry_k(input AwsCryptographyMaterialProvidersTypes.PutCacheEntryInput) Wrappers.Result {
26+
cmc.Lock()
27+
defer cmc.Unlock()
28+
return cmc.localCMC.PutCacheEntry_k(input)
29+
}
30+
func (cmc *SynchronizedLocalCMC) UpdateUsageMetadata(input AwsCryptographyMaterialProvidersTypes.UpdateUsageMetadataInput) Wrappers.Result {
31+
cmc.Lock()
32+
defer cmc.Unlock()
33+
return cmc.localCMC.UpdateUsageMetadata(input)
34+
}
35+
func (cmc *SynchronizedLocalCMC) UpdateUsageMetadata_k(input AwsCryptographyMaterialProvidersTypes.UpdateUsageMetadataInput) Wrappers.Result {
36+
cmc.Lock()
37+
defer cmc.Unlock()
38+
return cmc.localCMC.UpdateUsageMetadata_k(input)
39+
}
40+
func (cmc *SynchronizedLocalCMC) GetCacheEntry(input AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput) Wrappers.Result {
41+
cmc.Lock()
42+
defer cmc.Unlock()
43+
return cmc.localCMC.GetCacheEntry(input)
44+
}
45+
func (cmc *SynchronizedLocalCMC) GetCacheEntry_k(input AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput) Wrappers.Result {
46+
cmc.Lock()
47+
defer cmc.Unlock()
48+
return cmc.localCMC.GetCacheEntry_k(input)
49+
}
50+
func (cmc *SynchronizedLocalCMC) DeleteCacheEntry(input AwsCryptographyMaterialProvidersTypes.DeleteCacheEntryInput) Wrappers.Result {
51+
cmc.Lock()
52+
defer cmc.Unlock()
53+
return cmc.localCMC.DeleteCacheEntry(input)
54+
}
55+
func (cmc *SynchronizedLocalCMC) DeleteCacheEntry_k(input AwsCryptographyMaterialProvidersTypes.DeleteCacheEntryInput) Wrappers.Result {
56+
cmc.Lock()
57+
defer cmc.Unlock()
58+
return cmc.localCMC.DeleteCacheEntry_k(input)
59+
}
60+
61+
func (*SynchronizedLocalCMC) String() string {
62+
return "SynchronizedLocalCMC"
63+
}
Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
module github.com/aws/aws-cryptographic-material-providers-library/mpl
2+
3+
go 1.23.0
4+
5+
require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
6+
7+
require (
8+
github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0
9+
github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0
10+
github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0
11+
github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1
12+
github.com/aws/aws-sdk-go-v2/service/kms v1.36.0
13+
github.com/aws/smithy-go v1.21.0
14+
github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.1
15+
16+
)
17+
18+
require (
19+
github.com/aws/aws-sdk-go-v2 v1.31.0 // indirect
20+
github.com/aws/aws-sdk-go-v2/config v1.27.37 // indirect
21+
github.com/aws/aws-sdk-go-v2/credentials v1.17.35 // indirect
22+
github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14 // indirect
23+
github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18 // indirect
24+
github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18 // indirect
25+
github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 // indirect
26+
github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5 // indirect
27+
github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19 // indirect
28+
github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20 // indirect
29+
github.com/aws/aws-sdk-go-v2/service/sso v1.23.1 // indirect
30+
github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1 // indirect
31+
github.com/aws/aws-sdk-go-v2/service/sts v1.31.1 // indirect
32+
github.com/google/uuid v1.6.0 // indirect
33+
github.com/jmespath/go-jmespath v0.4.0 // indirect
34+
)
35+
36+
replace (
37+
github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0 => ../../../../ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/
38+
github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0 => ../../../../ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/
39+
github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0 => ../../../../AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/
40+
41+
)
42+
43+
replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../StandardLibrary/runtimes/go/ImplementationFromDafny-go/
Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
module github.com/aws/aws-cryptographic-material-providers-library/mpl/test
2+
3+
go 1.23.0
4+
5+
replace github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0 => ../ImplementationFromDafny-go
6+
7+
replace (
8+
github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0 => ../../../../ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/
9+
github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0 => ../../../../ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/
10+
github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0 => ../../../../AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/
11+
12+
)
13+
14+
replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../StandardLibrary/runtimes/go/ImplementationFromDafny-go/
15+
16+
require (
17+
github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0
18+
github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0
19+
github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0
20+
github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0
21+
github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2
22+
github.com/dafny-lang/DafnyStandardLibGo v0.0.0
23+
)
24+
25+
require (
26+
github.com/aws/aws-sdk-go-v2 v1.31.0 // indirect
27+
github.com/aws/aws-sdk-go-v2/config v1.27.37 // indirect
28+
github.com/aws/aws-sdk-go-v2/credentials v1.17.35 // indirect
29+
github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14 // indirect
30+
github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18 // indirect
31+
github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18 // indirect
32+
github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 // indirect
33+
github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1 // indirect
34+
github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5 // indirect
35+
github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19 // indirect
36+
github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20 // indirect
37+
github.com/aws/aws-sdk-go-v2/service/kms v1.36.0 // indirect
38+
github.com/aws/aws-sdk-go-v2/service/sso v1.23.1 // indirect
39+
github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1 // indirect
40+
github.com/aws/aws-sdk-go-v2/service/sts v1.31.1 // indirect
41+
github.com/aws/smithy-go v1.21.0 // indirect
42+
github.com/google/uuid v1.6.0 // indirect
43+
github.com/jmespath/go-jmespath v0.4.0 // indirect
44+
)

0 commit comments

Comments
 (0)