Skip to content

just a test run #1673

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 5 commits into
base: main
Choose a base branch
from
Draft

just a test run #1673

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
79ac320
Release mpl Go module 0.2.1
actions-user Aug 6, 2025
70e84f9
formatting and readme update
rishav-karanjit Aug 6, 2025
2df046a
auto commit
rishav-karanjit Aug 6, 2025
b36584e
auto commit
rishav-karanjit Aug 6, 2025
4369551
Update go.mod
rishav-karanjit Aug 7, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
56 changes: 22 additions & 34 deletions AwsCryptographicMaterialProviders/runtimes/go/TestsFromDafny-go/go.mod
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,43 +2,31 @@ module github.com/aws/aws-cryptographic-material-providers-library/releases/go/m

go 1.23.0

replace github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.0.0 => ../ImplementationFromDafny-go

replace (
github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.0.0 => ../../../../ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/
github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.0.0 => ../../../../ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/
github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.0.0 => ../../../../AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/

)

replace github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library => ../../../../StandardLibrary/runtimes/go/ImplementationFromDafny-go/

require (
github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.0.0
github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.0.0
github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.0.0
github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.0.0
github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.2.0
github.com/aws/aws-sdk-go-v2/service/dynamodb v1.39.2
github.com/aws/aws-sdk-go-v2/service/kms v1.36.0
github.com/aws/smithy-go v1.22.1
github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2
github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.2.1
github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.2.1
github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.2.1
github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.2.1
github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.2.1
github.com/aws/aws-sdk-go-v2/service/dynamodb v1.46.0
github.com/aws/aws-sdk-go-v2/service/kms v1.43.0
github.com/aws/smithy-go v1.22.5
github.com/dafny-lang/DafnyRuntimeGo/v4 v4.10.1
)

require (
github.com/aws/aws-sdk-go-v2 v1.32.8 // indirect
github.com/aws/aws-sdk-go-v2/config v1.28.10 // indirect
github.com/aws/aws-sdk-go-v2/credentials v1.17.51 // indirect
github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.23 // indirect
github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.27 // indirect
github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.27 // 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.12.1 // indirect
github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.10.8 // indirect
github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.12.8 // indirect
github.com/aws/aws-sdk-go-v2/service/sso v1.24.9 // indirect
github.com/aws/aws-sdk-go-v2/service/ssooidc v1.28.8 // indirect
github.com/aws/aws-sdk-go-v2/service/sts v1.33.6 // indirect
github.com/aws/aws-sdk-go-v2 v1.37.2 // indirect
github.com/aws/aws-sdk-go-v2/config v1.30.3 // indirect
github.com/aws/aws-sdk-go-v2/credentials v1.18.3 // indirect
github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.18.2 // indirect
github.com/aws/aws-sdk-go-v2/internal/configsources v1.4.2 // indirect
github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.7.2 // indirect
github.com/aws/aws-sdk-go-v2/internal/ini v1.8.3 // indirect
github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.13.0 // indirect
github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.11.2 // indirect
github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.13.2 // indirect
github.com/aws/aws-sdk-go-v2/service/sso v1.27.0 // indirect
github.com/aws/aws-sdk-go-v2/service/ssooidc v1.32.0 // indirect
github.com/aws/aws-sdk-go-v2/service/sts v1.36.0 // indirect
github.com/google/uuid v1.6.0 // indirect
github.com/jmespath/go-jmespath v0.4.0 // indirect
)
2 changes: 1 addition & 1 deletion TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/go.mod
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,4 +38,4 @@ require (
github.com/aws/smithy-go v1.22.1 // indirect
github.com/google/uuid v1.6.0 // indirect
github.com/jmespath/go-jmespath v0.4.0 // indirect
)
)
2 changes: 2 additions & 0 deletions releases/go/mpl/AlgorithmSuites/AlgorithmSuites.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,7 @@ import (
m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting"
m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary"
m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop"
m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath"
m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence"
m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String"
m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt"
Expand All @@ -80,6 +81,7 @@ var _ m__System.Dummy__
var _ m_Wrappers.Dummy__
var _ m_BoundedInts.Dummy__
var _ m_StandardLibrary_UInt.Dummy__
var _ m_StandardLibrary_MemoryMath.Dummy__
var _ m_StandardLibrary_Sequence.Dummy__
var _ m_StandardLibrary_String.Dummy__
var _ m_StandardLibrary.Dummy__
Expand Down
40 changes: 22 additions & 18 deletions releases/go/mpl/AwsArnParsing/AwsArnParsing.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ import (
m_Sorting "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Sorting"
m_StandardLibrary "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary"
m_StandardLibraryInterop "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibraryInterop"
m_StandardLibrary_MemoryMath "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_MemoryMath"
m_StandardLibrary_Sequence "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_Sequence"
m_StandardLibrary_String "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_String"
m_StandardLibrary_UInt "github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/StandardLibrary_UInt"
Expand All @@ -66,6 +67,7 @@ var _ m__System.Dummy__
var _ m_Wrappers.Dummy__
var _ m_BoundedInts.Dummy__
var _ m_StandardLibrary_UInt.Dummy__
var _ m_StandardLibrary_MemoryMath.Dummy__
var _ m_StandardLibrary_Sequence.Dummy__
var _ m_StandardLibrary_String.Dummy__
var _ m_StandardLibrary.Dummy__
Expand Down Expand Up @@ -158,27 +160,29 @@ func (_static *CompanionStruct_Default___) ValidAwsKmsArn(arn AwsArn) bool {
func (_static *CompanionStruct_Default___) ParseAwsKmsRawResources(identifier _dafny.Sequence) m_Wrappers.Result {
var _0_info _dafny.Sequence = m_StandardLibrary.Companion_Default___.Split(identifier, _dafny.Char('/'))
_ = _0_info
var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(!_dafny.Companion_Sequence_.Equal((_0_info).Select(0).(_dafny.Sequence), _dafny.SeqOfString("key")), _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOfString("Malformed raw key id: "), identifier))
var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(!_dafny.Companion_Sequence_.Equal((_0_info).Select(uint32(uint32(0))).(_dafny.Sequence), _dafny.SeqOfString("key")), _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOfString("Malformed raw key id: "), identifier))
_ = _1_valueOrError0
if (_1_valueOrError0).IsFailure() {
return (_1_valueOrError0).PropagateFailure()
} else if (_dafny.IntOfUint32((_0_info).Cardinality())).Cmp(_dafny.One) == 0 {
return Companion_Default___.ParseAwsKmsResources(_dafny.Companion_Sequence_.Concatenate(_dafny.SeqOfString("key/"), identifier))
} else {
return Companion_Default___.ParseAwsKmsResources(identifier)
if (uint64((_0_info).Cardinality())) == (uint64(1)) {
return Companion_Default___.ParseAwsKmsResources(_dafny.Companion_Sequence_.Concatenate(_dafny.SeqOfString("key/"), identifier))
} else {
return Companion_Default___.ParseAwsKmsResources(identifier)
}
}
}
func (_static *CompanionStruct_Default___) ParseAwsKmsResources(identifier _dafny.Sequence) m_Wrappers.Result {
var _0_info _dafny.Sequence = m_StandardLibrary.Companion_Default___.Split(identifier, _dafny.Char('/'))
_ = _0_info
var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((_dafny.IntOfUint32((_0_info).Cardinality())).Cmp(_dafny.One) > 0, _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOfString("Malformed resource: "), identifier))
var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((uint64((_0_info).Cardinality())) > (uint64(1)), _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOfString("Malformed resource: "), identifier))
_ = _1_valueOrError0
if (_1_valueOrError0).IsFailure() {
return (_1_valueOrError0).PropagateFailure()
} else {
var _2_resourceType _dafny.Sequence = (_0_info).Select(0).(_dafny.Sequence)
var _2_resourceType _dafny.Sequence = (_0_info).Select(uint32(uint32(0))).(_dafny.Sequence)
_ = _2_resourceType
var _3_value _dafny.Sequence = m_StandardLibrary.Companion_Default___.Join((_0_info).Drop(1), _dafny.SeqOfString("/"))
var _3_value _dafny.Sequence = m_StandardLibrary.Companion_Default___.Join((_0_info).Drop(uint32(uint32(1))), _dafny.SeqOfString("/"))
_ = _3_value
var _4_resource AwsResource = Companion_AwsResource_.Create_AwsResource_(_2_resourceType, _3_value)
_ = _4_resource
Expand Down Expand Up @@ -229,19 +233,19 @@ func (_static *CompanionStruct_Default___) ParseAmazonDynamodbResources(identifi
func (_static *CompanionStruct_Default___) ParseAwsKmsArn(identifier _dafny.Sequence) m_Wrappers.Result {
var _0_components _dafny.Sequence = m_StandardLibrary.Companion_Default___.Split(identifier, _dafny.Char(':'))
_ = _0_components
var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((_dafny.IntOfInt64(6)).Cmp(_dafny.IntOfUint32((_0_components).Cardinality())) == 0, _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOfString("Malformed arn: "), identifier))
var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((uint64(6)) == (uint64((_0_components).Cardinality())), _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOfString("Malformed arn: "), identifier))
_ = _1_valueOrError0
if (_1_valueOrError0).IsFailure() {
return (_1_valueOrError0).PropagateFailure()
} else {
var _2_valueOrError1 m_Wrappers.Result = Companion_Default___.ParseAwsKmsResources((_0_components).Select(5).(_dafny.Sequence))
var _2_valueOrError1 m_Wrappers.Result = Companion_Default___.ParseAwsKmsResources((_0_components).Select(uint32(uint32(5))).(_dafny.Sequence))
_ = _2_valueOrError1
if (_2_valueOrError1).IsFailure() {
return (_2_valueOrError1).PropagateFailure()
} else {
var _3_resource AwsResource = (_2_valueOrError1).Extract().(AwsResource)
_ = _3_resource
var _4_arn AwsArn = Companion_AwsArn_.Create_AwsArn_((_0_components).Select(0).(_dafny.Sequence), (_0_components).Select(1).(_dafny.Sequence), (_0_components).Select(2).(_dafny.Sequence), (_0_components).Select(3).(_dafny.Sequence), (_0_components).Select(4).(_dafny.Sequence), _3_resource)
var _4_arn AwsArn = Companion_AwsArn_.Create_AwsArn_((_0_components).Select(uint32(uint32(0))).(_dafny.Sequence), (_0_components).Select(uint32(uint32(1))).(_dafny.Sequence), (_0_components).Select(uint32(uint32(2))).(_dafny.Sequence), (_0_components).Select(uint32(uint32(3))).(_dafny.Sequence), (_0_components).Select(uint32(uint32(4))).(_dafny.Sequence), _3_resource)
_ = _4_arn
var _5_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(Companion_Default___.ValidAwsKmsArn(_4_arn), _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOfString("Malformed Arn:"), identifier))
_ = _5_valueOrError2
Expand All @@ -256,19 +260,19 @@ func (_static *CompanionStruct_Default___) ParseAwsKmsArn(identifier _dafny.Sequ
func (_static *CompanionStruct_Default___) ParseAmazonDynamodbTableArn(identifier _dafny.Sequence) m_Wrappers.Result {
var _0_components _dafny.Sequence = m_StandardLibrary.Companion_Default___.Split(identifier, _dafny.Char(':'))
_ = _0_components
var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((_dafny.IntOfInt64(6)).Cmp(_dafny.IntOfUint32((_0_components).Cardinality())) == 0, _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOfString("Malformed arn: "), identifier))
var _1_valueOrError0 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need((uint64(6)) == (uint64((_0_components).Cardinality())), _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOfString("Malformed arn: "), identifier))
_ = _1_valueOrError0
if (_1_valueOrError0).IsFailure() {
return (_1_valueOrError0).PropagateFailure()
} else {
var _2_valueOrError1 m_Wrappers.Result = Companion_Default___.ParseAmazonDynamodbResources((_0_components).Select(5).(_dafny.Sequence))
var _2_valueOrError1 m_Wrappers.Result = Companion_Default___.ParseAmazonDynamodbResources((_0_components).Select(uint32(uint32(5))).(_dafny.Sequence))
_ = _2_valueOrError1
if (_2_valueOrError1).IsFailure() {
return (_2_valueOrError1).PropagateFailure()
} else {
var _3_resource AwsResource = (_2_valueOrError1).Extract().(AwsResource)
_ = _3_resource
var _4_arn AwsArn = Companion_AwsArn_.Create_AwsArn_((_0_components).Select(0).(_dafny.Sequence), (_0_components).Select(1).(_dafny.Sequence), (_0_components).Select(2).(_dafny.Sequence), (_0_components).Select(3).(_dafny.Sequence), (_0_components).Select(4).(_dafny.Sequence), _3_resource)
var _4_arn AwsArn = Companion_AwsArn_.Create_AwsArn_((_0_components).Select(uint32(uint32(0))).(_dafny.Sequence), (_0_components).Select(uint32(uint32(1))).(_dafny.Sequence), (_0_components).Select(uint32(uint32(2))).(_dafny.Sequence), (_0_components).Select(uint32(uint32(3))).(_dafny.Sequence), (_0_components).Select(uint32(uint32(4))).(_dafny.Sequence), _3_resource)
_ = _4_arn
var _5_valueOrError2 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(Companion_Default___.ValidAmazonDynamodbArn(_4_arn), _dafny.Companion_Sequence_.Concatenate(_dafny.SeqOfString("Malformed Arn:"), identifier))
_ = _5_valueOrError2
Expand Down Expand Up @@ -360,7 +364,7 @@ func (_static *CompanionStruct_Default___) IsAwsKmsIdentifierString(s _dafny.Seq
if (_0_valueOrError0).IsFailure() {
return (_0_valueOrError0).PropagateFailure()
} else {
var _1_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(((_dafny.IntOfUint32((s).Cardinality())).Sign() == 1) && ((_dafny.IntOfUint32((s).Cardinality())).Cmp(Companion_Default___.MAX__AWS__KMS__IDENTIFIER__LENGTH()) <= 0), _dafny.SeqOfString("Identifier exceeds maximum length."))
var _1_valueOrError1 m_Wrappers.Outcome = m_Wrappers.Companion_Default___.Need(((uint64(0)) < (uint64((s).Cardinality()))) && ((uint64((s).Cardinality())) <= (Companion_Default___.MAX__AWS__KMS__IDENTIFIER__LENGTH())), _dafny.SeqOfString("Identifier exceeds maximum length."))
_ = _1_valueOrError1
if (_1_valueOrError1).IsFailure() {
return (_1_valueOrError1).PropagateFailure()
Expand Down Expand Up @@ -399,8 +403,8 @@ func (_static *CompanionStruct_Default___) ValidateDdbTableArn(tableArn _dafny.S
}
}
}
func (_static *CompanionStruct_Default___) MAX__AWS__KMS__IDENTIFIER__LENGTH() _dafny.Int {
return _dafny.IntOfInt64(2048)
func (_static *CompanionStruct_Default___) MAX__AWS__KMS__IDENTIFIER__LENGTH() uint64 {
return uint64(2048)
}

// End of class Default__
Expand Down Expand Up @@ -507,7 +511,7 @@ var _ _dafny.TraitOffspring = AwsResource{}

func (_this AwsResource) Valid() bool {
{
return (true) && ((_dafny.IntOfUint32(((_this).Dtor_value()).Cardinality())).Sign() == 1)
return (true) && ((uint64(0)) < (uint64(((_this).Dtor_value()).Cardinality())))
}
}
func (_this AwsResource) ToString() _dafny.Sequence {
Expand Down Expand Up @@ -640,7 +644,7 @@ var _ _dafny.TraitOffspring = AwsArn{}

func (_this AwsArn) Valid() bool {
{
return (((((_dafny.Companion_Sequence_.Equal((_this).Dtor_arnLiteral(), _dafny.SeqOfString("arn"))) && ((_dafny.IntOfUint32(((_this).Dtor_partition()).Cardinality())).Sign() == 1)) && ((_dafny.IntOfUint32(((_this).Dtor_service()).Cardinality())).Sign() == 1)) && ((_dafny.IntOfUint32(((_this).Dtor_region()).Cardinality())).Sign() == 1)) && ((_dafny.IntOfUint32(((_this).Dtor_account()).Cardinality())).Sign() == 1)) && (((_this).Dtor_resource()).Valid())
return (((((_dafny.Companion_Sequence_.Equal((_this).Dtor_arnLiteral(), _dafny.SeqOfString("arn"))) && ((uint64(0)) < (uint64(((_this).Dtor_partition()).Cardinality())))) && ((uint64(0)) < (uint64(((_this).Dtor_service()).Cardinality())))) && ((uint64(0)) < (uint64(((_this).Dtor_region()).Cardinality())))) && ((uint64(0)) < (uint64(((_this).Dtor_account()).Cardinality())))) && (((_this).Dtor_resource()).Valid())
}
}
func (_this AwsArn) ToString() _dafny.Sequence {
Expand Down
Loading
Loading