diff --git a/.github/workflows/library_go_tests.yml b/.github/workflows/library_go_tests.yml index 85be32db6..6e930f80a 100644 --- a/.github/workflows/library_go_tests.yml +++ b/.github/workflows/library_go_tests.yml @@ -25,6 +25,7 @@ jobs: ComAmazonawsKms, ComAmazonawsDynamodb, AwsCryptographyPrimitives, + AwsCryptographicMaterialProviders, ] go-version: ["1.23"] os: [ diff --git a/AwsCryptographicMaterialProviders/Makefile b/AwsCryptographicMaterialProviders/Makefile index 2d052acf0..ab65f66c3 100644 --- a/AwsCryptographicMaterialProviders/Makefile +++ b/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 diff --git a/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/StormTrackingCMC/externs.go b/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/StormTrackingCMC/externs.go new file mode 100644 index 000000000..216f8052a --- /dev/null +++ b/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) +} diff --git a/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/SynchronizedLocalCMC/externs.go b/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/SynchronizedLocalCMC/externs.go new file mode 100644 index 000000000..1067396b0 --- /dev/null +++ b/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" +} diff --git a/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/go.mod b/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/go.mod new file mode 100644 index 000000000..7b1d1e3da --- /dev/null +++ b/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/ diff --git a/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/go.mod b/AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/go.mod new file mode 100644 index 000000000..dfc5ebe50 --- /dev/null +++ b/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 +) diff --git a/StandardLibrary/runtimes/go/ImplementationFromDafny-go/DafnyLibraries/externs.go b/StandardLibrary/runtimes/go/ImplementationFromDafny-go/DafnyLibraries/externs.go index c54ee4d86..1ee986421 100644 --- a/StandardLibrary/runtimes/go/ImplementationFromDafny-go/DafnyLibraries/externs.go +++ b/StandardLibrary/runtimes/go/ImplementationFromDafny-go/DafnyLibraries/externs.go @@ -7,9 +7,12 @@ import ( Std_Wrappers "github.com/dafny-lang/DafnyStandardLibGo/Wrappers" ) -// Definition of class MutableMap +// Definition of class MutableMap copied over from +// https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/src/Std_Concurrent/Std_Concurrent.go type MutableMap struct { - Internal sync.Map + mu sync.Mutex + + Internal _dafny.Map } func New_MutableMap_() *MutableMap { @@ -62,56 +65,42 @@ func (_this *MutableMap) Ctor__() { } func (_this *MutableMap) Keys() _dafny.Set { { - keys := make([]interface{}, 0) - - _this.Internal.Range(func(key, value interface{}) bool { - keys = append(keys, key) - return true - }) + _this.mu.Lock() + defer _this.mu.Unlock() - return _dafny.SetOf(keys[:]...) + return _this.Internal.Keys() } } func (_this *MutableMap) HasKey(k interface{}) bool { { - _, ok := _this.Internal.Load(k) - return ok + _this.mu.Lock() + defer _this.mu.Unlock() + + return _this.Internal.Contains(k) } } func (_this *MutableMap) Values() _dafny.Set { { - values := make([]interface{}, 0) + _this.mu.Lock() + defer _this.mu.Unlock() - _this.Internal.Range(func(key, value interface{}) bool { - values = append(values, value) - return true - }) - - return _dafny.SetOf(values[:]...) + return _this.Internal.Values() } } func (_this *MutableMap) Items() _dafny.Set { { - items := make([]interface{}, 0) - - _this.Internal.Range(func(key, value interface{}) bool { - items = append(items, _dafny.TupleOf(key, value)) - return true - }) + _this.mu.Lock() + defer _this.mu.Unlock() - return _dafny.SetOf(items[:]...) - } -} -func (_this *MutableMap) Select(k interface{}) interface{} { - r := _this.Get(k) - if r.Is_None() { - return nil + return _this.Internal.Items() } - return r.Dtor_value() } func (_this *MutableMap) Get(k interface{}) Std_Wrappers.Option { { - value, ok := _this.Internal.Load(k) + _this.mu.Lock() + defer _this.mu.Unlock() + + value, ok := _this.Internal.Find(k) if ok { return Std_Wrappers.Companion_Option_.Create_Some_(value) } else { @@ -121,23 +110,38 @@ func (_this *MutableMap) Get(k interface{}) Std_Wrappers.Option { } func (_this *MutableMap) Put(k interface{}, v interface{}) { { - _this.Internal.Store(k, v) + _this.mu.Lock() + defer _this.mu.Unlock() + + _this.Internal = _this.Internal.UpdateUnsafe(k, v) } } func (_this *MutableMap) Remove(k interface{}) { { - _this.Internal.Delete(k) + _this.mu.Lock() + defer _this.mu.Unlock() + + // This could be special-cased for a single remove to be a bit faster, + // but it's still going to be O(n) so likely not worth it. + _this.Internal = _this.Internal.Subtract(_dafny.SetOf(k)) } } func (_this *MutableMap) Size() _dafny.Int { { - var c _dafny.Int = _dafny.Zero + _this.mu.Lock() + defer _this.mu.Unlock() + + return _this.Internal.Cardinality() + } +} - _this.Internal.Range(func(key, value interface{}) bool { - c = c.Plus(_dafny.One) - return true - }) +// End of class MutableMap - return c +// This is handrolled extern +func (_this *MutableMap) Select(k interface{}) interface{} { + r := _this.Get(k) + if r.Is_None() { + return nil } + return r.Dtor_value() } diff --git a/StandardLibrary/runtimes/go/ImplementationFromDafny-go/Time_/externs.go b/StandardLibrary/runtimes/go/ImplementationFromDafny-go/Time_/externs.go index d52e81bc2..00deda5a9 100644 --- a/StandardLibrary/runtimes/go/ImplementationFromDafny-go/Time_/externs.go +++ b/StandardLibrary/runtimes/go/ImplementationFromDafny-go/Time_/externs.go @@ -18,7 +18,7 @@ func (CompanionStruct_Default___) CurrentRelativeTime() int64 { return CurrentRelativeTime() } func CurrentRelativeTime() int64 { - return int64(time.Now().Second()) + return int64(time.Now().Unix()) } func (CompanionStruct_Default___) GetCurrentTimeStamp() Wrappers.Result { diff --git a/smithy-dafny b/smithy-dafny index 5b66889c6..99d3dd9d1 160000 --- a/smithy-dafny +++ b/smithy-dafny @@ -1 +1 @@ -Subproject commit 5b66889c630658f963ebed04c4a4c33d2047f845 +Subproject commit 99d3dd9d1902b54e0cb1f659379c8db43aec29b9