feat: mpl externs

.github/workflows/library_go_tests.yml

@@ -25,6 +25,7 @@ jobs:
             ComAmazonawsKms,
             ComAmazonawsDynamodb,
             AwsCryptographyPrimitives,
+            AwsCryptographicMaterialProviders,
           ]
         go-version: ["1.23"]
         os: [

AwsCryptographicMaterialProviders/Makefile

@@ -2,7 +2,6 @@
 # SPDX-License-Identifier: Apache-2.0
 
 CORES=2
-
 ENABLE_EXTERN_PROCESSING=1
 
 include ../SharedMakefileV2.mk
@@ -68,6 +67,22 @@ SERVICE_DEPS_AwsCryptographyKeyStore := \
 	ComAmazonawsDynamodb \
 	AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders \
 
+GO_MODULE_NAME="github.com/aws/aws-cryptographic-material-providers-library/mpl"
+
+GO_DEPENDENCY_MODULE_NAMES := \
+	--dependency-library-name=com.amazonaws.dynamodb=github.com/aws/aws-cryptographic-material-providers-library/dynamodb \
+	--dependency-library-name=com.amazonaws.kms=github.com/aws/aws-cryptographic-material-providers-library/kms \
+	--dependency-library-name=aws.cryptography.keyStore=github.com/aws/aws-cryptographic-material-providers-library/mpl \
+	--dependency-library-name=aws.cryptography.primitives=github.com/aws/aws-cryptographic-material-providers-library/primitives \
+	--dependency-library-name=sdk.com.amazonaws.dynamodb=github.com/aws/aws-sdk-go-v2/service/dynamodb \
+	--dependency-library-name=sdk.com.amazonaws.kms=github.com/aws/aws-sdk-go-v2/service/kms
+
+TRANSLATION_RECORD_GO := \
+    StandardLibrary/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
+    ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
+    ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
+    AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr
+
 # Constants for languages that drop extern names (Python, Go)
 
 MPL_CORE_TYPES_FILE_PATH=dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy

AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/StormTrackingCMC/externs.go

@@ -0,0 +1,86 @@
+package StormTrackingCMC
+
+import (
+	"sync"
+	"time"
+
+	"github.com/aws/aws-cryptographic-material-providers-library/mpl/AwsCryptographyMaterialProvidersTypes"
+	"github.com/aws/aws-cryptographic-material-providers-library/mpl/StormTracker"
+	_dafny "github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
+	"github.com/dafny-lang/DafnyStandardLibGo/Wrappers"
+	DafnyTime "github.com/dafny-lang/DafnyStandardLibGo/Time_"
+)
+
+type StormTrackingCMC struct {
+	stormTracker *StormTracker.StormTracker
+	//The Lock contention is not tested.
+	sync.Mutex
+}
+
+func New_StormTrackingCMC_(stormTracker *StormTracker.StormTracker) *StormTrackingCMC {
+	return &StormTrackingCMC{stormTracker: stormTracker}
+}
+
+func (cmc *StormTrackingCMC) PutCacheEntry(input AwsCryptographyMaterialProvidersTypes.PutCacheEntryInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.stormTracker.PutCacheEntry(input)
+}
+func (cmc *StormTrackingCMC) PutCacheEntry_k(input AwsCryptographyMaterialProvidersTypes.PutCacheEntryInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.stormTracker.PutCacheEntry(input)
+}
+func (cmc *StormTrackingCMC) UpdateUsageMetadata(input AwsCryptographyMaterialProvidersTypes.UpdateUsageMetadataInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.stormTracker.UpdateUsageMetadata(input)
+}
+func (cmc *StormTrackingCMC) UpdateUsageMetadata_k(input AwsCryptographyMaterialProvidersTypes.UpdateUsageMetadataInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.stormTracker.UpdateUsageMetadata(input)
+}
+func (cmc *StormTrackingCMC) GetCacheEntry(input AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput) Wrappers.Result {
+	return cmc.GetCacheEntry_k(input)
+}
+func (cmc *StormTrackingCMC) GetCacheEntry_k(input AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput) Wrappers.Result {
+	maxInFlight := DafnyTime.CurrentRelativeTimeMilli() + cmc.stormTracker.InFlightTTL
+	for {
+		res := cmc.GetFromInner(input)
+		if res.IsFailure() {
+			return Companion_Default___.CreateGetCacheEntryFailure(res.Dtor_error().(AwsCryptographyMaterialProvidersTypes.Error))
+		} else if res.Dtor_value().(StormTracker.CacheState).Is_Full() {
+			return Companion_Default___.CreateGetCacheEntrySuccess(res.Dtor_value().(StormTracker.CacheState).Dtor_data())
+		} else if res.Dtor_value().(StormTracker.CacheState).Is_EmptyFetch() {
+			return Companion_Default___.CreateGetCacheEntryFailure(AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_EntryDoesNotExist_(_dafny.SeqOfChars([]_dafny.Char("Entry doesn't exists")...)))
+		} else {
+			if DafnyTime.CurrentRelativeTimeMilli() <= maxInFlight {
+				time.Sleep(time.Duration(cmc.stormTracker.SleepMilli))
+			} else {
+				return Companion_Default___.CreateGetCacheEntryFailure(AwsCryptographyMaterialProvidersTypes.Companion_Error_.Create_InFlightTTLExceeded_(_dafny.SeqOfChars([]_dafny.Char("Storm cache inFlightTTL exceeded.")...)))
+			}
+		}
+	}
+}
+func (cmc *StormTrackingCMC) DeleteCacheEntry(input AwsCryptographyMaterialProvidersTypes.DeleteCacheEntryInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.stormTracker.DeleteCacheEntry(input)
+
+}
+func (cmc *StormTrackingCMC) DeleteCacheEntry_k(input AwsCryptographyMaterialProvidersTypes.DeleteCacheEntryInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.stormTracker.DeleteCacheEntry(input)
+}
+
+func (cmc *StormTrackingCMC) String() string {
+	return "StormTrackerCMC"
+}
+
+func (cmc *StormTrackingCMC) GetFromInner(input AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.stormTracker.GetFromCache(input)
+}

AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/SynchronizedLocalCMC/externs.go

@@ -0,0 +1,63 @@
+package SynchronizedLocalCMC
+
+import (
+	"sync"
+
+	"github.com/aws/aws-cryptographic-material-providers-library/mpl/AwsCryptographyMaterialProvidersTypes"
+	"github.com/aws/aws-cryptographic-material-providers-library/mpl/LocalCMC"
+	"github.com/dafny-lang/DafnyStandardLibGo/Wrappers"
+)
+
+type SynchronizedLocalCMC struct {
+	localCMC *LocalCMC.LocalCMC
+	sync.Mutex
+}
+
+func New_SynchronizedLocalCMC_(localCMC *LocalCMC.LocalCMC) *SynchronizedLocalCMC {
+	return &SynchronizedLocalCMC{localCMC: localCMC}
+}
+
+func (cmc *SynchronizedLocalCMC) PutCacheEntry(input AwsCryptographyMaterialProvidersTypes.PutCacheEntryInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.localCMC.PutCacheEntry(input)
+}
+func (cmc *SynchronizedLocalCMC) PutCacheEntry_k(input AwsCryptographyMaterialProvidersTypes.PutCacheEntryInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.localCMC.PutCacheEntry_k(input)
+}
+func (cmc *SynchronizedLocalCMC) UpdateUsageMetadata(input AwsCryptographyMaterialProvidersTypes.UpdateUsageMetadataInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.localCMC.UpdateUsageMetadata(input)
+}
+func (cmc *SynchronizedLocalCMC) UpdateUsageMetadata_k(input AwsCryptographyMaterialProvidersTypes.UpdateUsageMetadataInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.localCMC.UpdateUsageMetadata_k(input)
+}
+func (cmc *SynchronizedLocalCMC) GetCacheEntry(input AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.localCMC.GetCacheEntry(input)
+}
+func (cmc *SynchronizedLocalCMC) GetCacheEntry_k(input AwsCryptographyMaterialProvidersTypes.GetCacheEntryInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.localCMC.GetCacheEntry_k(input)
+}
+func (cmc *SynchronizedLocalCMC) DeleteCacheEntry(input AwsCryptographyMaterialProvidersTypes.DeleteCacheEntryInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.localCMC.DeleteCacheEntry(input)
+}
+func (cmc *SynchronizedLocalCMC) DeleteCacheEntry_k(input AwsCryptographyMaterialProvidersTypes.DeleteCacheEntryInput) Wrappers.Result {
+	cmc.Lock()
+	defer cmc.Unlock()
+	return cmc.localCMC.DeleteCacheEntry_k(input)
+}
+
+func (*SynchronizedLocalCMC) String() string {
+	return "SynchronizedLocalCMC"
+}

AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/go.mod

@@ -0,0 +1,43 @@
+module github.com/aws/aws-cryptographic-material-providers-library/mpl
+
+go 1.23.0
+
+require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
+
+require (
+	github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0
+	github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0
+	github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0
+	github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1
+	github.com/aws/aws-sdk-go-v2/service/kms v1.36.0
+	github.com/aws/smithy-go v1.21.0
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.1
+
+)
+
+require (
+	github.com/aws/aws-sdk-go-v2 v1.31.0 // indirect
+	github.com/aws/aws-sdk-go-v2/config v1.27.37 // indirect
+	github.com/aws/aws-sdk-go-v2/credentials v1.17.35 // indirect
+	github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20 // indirect
+	github.com/aws/aws-sdk-go-v2/service/sso v1.23.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/sts v1.31.1 // indirect
+	github.com/google/uuid v1.6.0 // indirect
+	github.com/jmespath/go-jmespath v0.4.0 // indirect
+)
+
+replace (
+	github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0 => ../../../../ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0 => ../../../../ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0 => ../../../../AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/
+
+)
+
+replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../StandardLibrary/runtimes/go/ImplementationFromDafny-go/

AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/go.mod

@@ -0,0 +1,44 @@
+module github.com/aws/aws-cryptographic-material-providers-library/mpl/test
+
+go 1.23.0
+
+replace github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0 => ../ImplementationFromDafny-go
+
+replace (
+	github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0 => ../../../../ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0 => ../../../../ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0 => ../../../../AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/
+
+)
+
+replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../StandardLibrary/runtimes/go/ImplementationFromDafny-go/
+
+require (
+	github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0
+	github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0
+	github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0
+	github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2
+	github.com/dafny-lang/DafnyStandardLibGo v0.0.0
+)
+
+require (
+	github.com/aws/aws-sdk-go-v2 v1.31.0 // indirect
+	github.com/aws/aws-sdk-go-v2/config v1.27.37 // indirect
+	github.com/aws/aws-sdk-go-v2/credentials v1.17.35 // indirect
+	github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20 // indirect
+	github.com/aws/aws-sdk-go-v2/service/kms v1.36.0 // indirect
+	github.com/aws/aws-sdk-go-v2/service/sso v1.23.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/sts v1.31.1 // indirect
+	github.com/aws/smithy-go v1.21.0 // indirect
+	github.com/google/uuid v1.6.0 // indirect
+	github.com/jmespath/go-jmespath v0.4.0 // indirect
+)