-
Notifications
You must be signed in to change notification settings - Fork 15
chore(Go): Add interop test with CI #1721
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.
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
Merged
rishav-karanjit
merged 17 commits into
Golang/DynamoDbEncryptionModule
from
Golang/TestVectors
Mar 17, 2025
Merged
Changes from all commits
Commits
Show all changes
17 commits
Select commit
Hold shift + click to select a range
9012781
workflow
rishav-karanjit 991a330
submodules
rishav-karanjit 8793aeb
Update data.json
rishav-karanjit 43e38a2
key path
rishav-karanjit 10ba751
Merge branch 'Golang/TestVectors' of https://github.com/aws/aws-datab…
rishav-karanjit 92e3fa3
Revert "key path"
rishav-karanjit c7e5630
path
rishav-karanjit 02ba132
json files
rishav-karanjit dacae91
remove redundant code
rishav-karanjit 77ddecd
remove unwanted diff
rishav-karanjit 195e7bb
Comment
rishav-karanjit c702be7
Use EndpointResolverV2
rishav-karanjit 1558e02
update data.json
rishav-karanjit 328b638
submodules
rishav-karanjit 400f247
submodules
rishav-karanjit 3998705
copy from java
rishav-karanjit 2e63281
rm json
rishav-karanjit File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -27,14 +27,25 @@ jobs: | |
testGo: | ||
strategy: | ||
matrix: | ||
library: [DynamoDbEncryption] | ||
library: [DynamoDbEncryption, TestVectors] | ||
os: [ubuntu-22.04] | ||
go-version: ["1.23"] | ||
runs-on: ${{ matrix.os }} | ||
permissions: | ||
id-token: write | ||
contents: read | ||
steps: | ||
- name: Setup Docker | ||
if: matrix.os == 'macos-13' && matrix.library == 'TestVectors' | ||
uses: douglascamata/setup-docker-macos-action@v1-alpha | ||
|
||
- name: Setup DynamoDB Local | ||
if: matrix.library == 'TestVectors' | ||
uses: rrainn/[email protected] | ||
with: | ||
port: 8000 | ||
cors: "*" | ||
|
||
- name: Support longpaths | ||
run: | | ||
git config --global core.longpaths true | ||
|
@@ -97,12 +108,6 @@ jobs: | |
- name: Install Smithy-Dafny codegen dependencies | ||
uses: ./.github/actions/install_smithy_dafny_codegen_dependencies | ||
|
||
- name: Regenerate code using smithy-dafny | ||
shell: bash | ||
working-directory: ./${{ matrix.library }} | ||
run: | | ||
make polymorph_go | ||
|
||
- name: Build ${{ matrix.library }} implementation | ||
shell: bash | ||
working-directory: ./${{ matrix.library }} | ||
|
@@ -111,6 +116,19 @@ jobs: | |
CORES=$(node -e 'console.log(os.cpus().length)') | ||
make transpile_go CORES=$CORES | ||
|
||
- name: Regenerate code using smithy-dafny | ||
shell: bash | ||
working-directory: ./${{ matrix.library }} | ||
run: | | ||
make polymorph_go | ||
|
||
- name: Copy ${{ matrix.library }} Vector Files | ||
if: ${{ matrix.library == 'TestVectors' }} | ||
shell: bash | ||
working-directory: ./${{ matrix.library }} | ||
run: | | ||
cp runtimes/java/*.json runtimes/go/TestsFromDafny-go/ | ||
|
||
- name: Test ${{ matrix.library }} | ||
working-directory: ./${{ matrix.library }} | ||
run: | | ||
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
61 changes: 61 additions & 0 deletions
61
TestVectors/runtimes/go/ImplementationFromDafny-go/CreateInterceptedDDBClient/extern.go
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,61 @@ | ||
package CreateInterceptedDDBClient | ||
|
||
import ( | ||
"context" | ||
"net/url" | ||
|
||
"github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb/DynamoDBwrapped" | ||
"github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library/Wrappers" | ||
"github.com/aws/aws-database-encryption-sdk-dynamodb/AwsCryptographyDbEncryptionSdkDynamoDbTypes" | ||
"github.com/aws/aws-database-encryption-sdk-dynamodb/awscryptographydbencryptionsdkdynamodbsmithygenerated" | ||
"github.com/aws/aws-database-encryption-sdk-dynamodb/dbesdkmiddleware" | ||
"github.com/aws/aws-sdk-go-v2/config" | ||
"github.com/aws/aws-sdk-go-v2/service/dynamodb" | ||
smithyendpoints "github.com/aws/smithy-go/endpoints" | ||
) | ||
|
||
type resolverV2 struct { | ||
} | ||
|
||
func (*resolverV2) ResolveEndpoint(ctx context.Context, params dynamodb.EndpointParameters) ( | ||
smithyendpoints.Endpoint, error, | ||
) { | ||
u, err := url.Parse("http://localhost:8000") | ||
if err != nil { | ||
return smithyendpoints.Endpoint{}, err | ||
} | ||
return smithyendpoints.Endpoint{ | ||
URI: *u, | ||
}, nil | ||
} | ||
|
||
func CreateVanillaDDBClient() Wrappers.Result { | ||
cfg, err := config.LoadDefaultConfig(context.TODO()) | ||
if err != nil { | ||
panic(err) | ||
} | ||
ddbClient := dynamodb.NewFromConfig(cfg, func(o *dynamodb.Options) { | ||
o.EndpointResolverV2 = &resolverV2{} | ||
}) | ||
return Wrappers.Companion_Result_.Create_Success_(&DynamoDBwrapped.Shim{ | ||
Client: ddbClient, | ||
}) | ||
} | ||
|
||
func CreateInterceptedDDBClient(ddbEncryptionConfig AwsCryptographyDbEncryptionSdkDynamoDbTypes.DynamoDbTablesEncryptionConfig) Wrappers.Result { | ||
cfg, err := config.LoadDefaultConfig(context.TODO()) | ||
if err != nil { | ||
panic(err) | ||
} | ||
nativeConfig := awscryptographydbencryptionsdkdynamodbsmithygenerated.DynamoDbTablesEncryptionConfig_FromDafny(ddbEncryptionConfig) | ||
dbEsdkMiddleware, err := dbesdkmiddleware.NewDBEsdkMiddleware(nativeConfig) | ||
if err != nil { | ||
panic(err) | ||
} | ||
ddbClient := dynamodb.NewFromConfig(cfg, dbEsdkMiddleware.CreateMiddleware(), func(o *dynamodb.Options) { | ||
o.EndpointResolverV2 = &resolverV2{} | ||
}) | ||
return Wrappers.Companion_Result_.Create_Success_(&DynamoDBwrapped.Shim{ | ||
Client: ddbClient, | ||
}) | ||
} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,45 @@ | ||
module github.com/aws/aws-database-encryption-sdk-dynamodb/testvectors | ||
|
||
go 1.23.2 | ||
|
||
replace ( | ||
github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb => ../../../../submodules/MaterialProviders/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/ | ||
github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms => ../../../../submodules/MaterialProviders/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/ | ||
github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl => ../../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ | ||
github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives => ../../../../submodules/MaterialProviders/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ | ||
github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library => ../../../../submodules/MaterialProviders/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ | ||
github.com/aws/aws-cryptographic-material-providers-library/testvectors => ../../../../submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ | ||
github.com/aws/aws-database-encryption-sdk-dynamodb => ../../../../DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/ | ||
) | ||
|
||
require ( | ||
github.com/aws/aws-cryptographic-material-providers-library/releases/go/dynamodb v0.1.0 | ||
github.com/aws/aws-cryptographic-material-providers-library/releases/go/kms v0.0.1 | ||
github.com/aws/aws-cryptographic-material-providers-library/releases/go/mpl v0.1.0 | ||
github.com/aws/aws-cryptographic-material-providers-library/releases/go/primitives v0.0.1 | ||
github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library v0.1.0 | ||
github.com/aws/aws-cryptographic-material-providers-library/testvectors v0.0.0 | ||
github.com/aws/aws-database-encryption-sdk-dynamodb v0.0.0 | ||
github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2 | ||
) | ||
|
||
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/dynamodb v1.39.2 // 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/kms v1.37.10 // 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/smithy-go v1.22.1 // indirect | ||
github.com/google/uuid v1.6.0 // indirect | ||
github.com/jmespath/go-jmespath v0.4.0 // indirect | ||
) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,48 @@ | ||
github.com/aws/aws-sdk-go-v2 v1.32.8 h1:cZV+NUS/eGxKXMtmyhtYPJ7Z4YLoI/V8bkTdRZfYhGo= | ||
github.com/aws/aws-sdk-go-v2 v1.32.8/go.mod h1:P5WJBrYqqbWVaOxgH0X/FYYD47/nooaPOZPlQdmiN2U= | ||
github.com/aws/aws-sdk-go-v2/config v1.28.10 h1:fKODZHfqQu06pCzR69KJ3GuttraRJkhlC8g80RZ0Dfg= | ||
github.com/aws/aws-sdk-go-v2/config v1.28.10/go.mod h1:PvdxRYZ5Um9QMq9PQ0zHHNdtKK+he2NHtFCUFMXWXeg= | ||
github.com/aws/aws-sdk-go-v2/credentials v1.17.51 h1:F/9Sm6Y6k4LqDesZDPJCLxQGXNNHd/ZtJiWd0lCZKRk= | ||
github.com/aws/aws-sdk-go-v2/credentials v1.17.51/go.mod h1:TKbzCHm43AoPyA+iLGGcruXd4AFhF8tOmLex2R9jWNQ= | ||
github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.23 h1:IBAoD/1d8A8/1aA8g4MBVtTRHhXRiNAgwdbo/xRM2DI= | ||
github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.23/go.mod h1:vfENuCM7dofkgKpYzuzf1VT1UKkA/YL3qanfBn7HCaA= | ||
github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.27 h1:jSJjSBzw8VDIbWv+mmvBSP8ezsztMYJGH+eKqi9AmNs= | ||
github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.27/go.mod h1:/DAhLbFRgwhmvJdOfSm+WwikZrCuUJiA4WgJG0fTNSw= | ||
github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.27 h1:l+X4K77Dui85pIj5foXDhPlnqcNRG2QUyvca300lXh8= | ||
github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.27/go.mod h1:KvZXSFEXm6x84yE8qffKvT3x8J5clWnVFXphpohhzJ8= | ||
github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 h1:VaRN3TlFdd6KxX1x3ILT5ynH6HvKgqdiXoTxAF4HQcQ= | ||
github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1/go.mod h1:FbtygfRFze9usAadmnGJNc8KsP346kEe+y2/oyhGAGc= | ||
github.com/aws/aws-sdk-go-v2/service/dynamodb v1.39.2 h1:XcdIh35yg1J8bAiUOLtL/PoPMSGsD72Zanwmim8jEXc= | ||
github.com/aws/aws-sdk-go-v2/service/dynamodb v1.39.2/go.mod h1:516U/KQM3zdcahNBjHUZKGWNfNnIYyt7sxLeqOx78b0= | ||
github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.12.1 h1:iXtILhvDxB6kPvEXgsDhGaZCSC6LQET5ZHSdJozeI0Y= | ||
github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.12.1/go.mod h1:9nu0fVANtYiAePIBh2/pFUSwtJ402hLnp854CNoDOeE= | ||
github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.10.8 h1:h56mLNgpqWIL7RZOIQO634Xr569bXGTlIE83t/a0LSE= | ||
github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.10.8/go.mod h1:kK04550Xx95KI0sNmwoB7ciS9QkRwt9TojhoTMXyJdo= | ||
github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.12.8 h1:cWno7lefSH6Pp+mSznagKCgfDGeZRin66UvYUqAkyeA= | ||
github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.12.8/go.mod h1:tPD+VjU3ABTBoEJ3nctu5Nyg4P4yjqSH5bJGGkY4+XE= | ||
github.com/aws/aws-sdk-go-v2/service/kms v1.37.10 h1:nqYgJ+twjn6hrhTS97j3tlpNXrw4E9N2zQBgw2FAQMg= | ||
github.com/aws/aws-sdk-go-v2/service/kms v1.37.10/go.mod h1:wHYtyttsH+A6d2MzXYl8cIf4O2Kw1Kg0qzromSX/wOs= | ||
github.com/aws/aws-sdk-go-v2/service/sso v1.24.9 h1:YqtxripbjWb2QLyzRK9pByfEDvgg95gpC2AyDq4hFE8= | ||
github.com/aws/aws-sdk-go-v2/service/sso v1.24.9/go.mod h1:lV8iQpg6OLOfBnqbGMBKYjilBlf633qwHnBEiMSPoHY= | ||
github.com/aws/aws-sdk-go-v2/service/ssooidc v1.28.8 h1:6dBT1Lz8fK11m22R+AqfRsFn8320K0T5DTGxxOQBSMw= | ||
github.com/aws/aws-sdk-go-v2/service/ssooidc v1.28.8/go.mod h1:/kiBvRQXBc6xeJTYzhSdGvJ5vm1tjaDEjH+MSeRJnlY= | ||
github.com/aws/aws-sdk-go-v2/service/sts v1.33.6 h1:VwhTrsTuVn52an4mXx29PqRzs2Dvu921NpGk7y43tAM= | ||
github.com/aws/aws-sdk-go-v2/service/sts v1.33.6/go.mod h1:+8h7PZb3yY5ftmVLD7ocEoE98hdc8PoKS0H3wfx1dlc= | ||
github.com/aws/smithy-go v1.22.1 h1:/HPHZQ0g7f4eUeK6HKglFz8uwVfZKgoI25rb/J+dnro= | ||
github.com/aws/smithy-go v1.22.1/go.mod h1:irrKGvNn1InZwb2d7fkIRNucdfwR8R+Ts3wxYa/cJHg= | ||
github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2 h1:g/xAj4F7Zt9wXJ6QjfbfocVi/ZYlAFpNddHCFyfzRDg= | ||
github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto= | ||
github.com/davecgh/go-spew v1.1.0 h1:ZDRjVQ15GmhC3fiQ8ni8+OwkZQO4DARzQgrnXU1Liz8= | ||
github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38= | ||
github.com/google/uuid v1.6.0 h1:NIvaJDMOsjHA8n1jAhLSgzrAzy1Hgr+hNrb57e+94F0= | ||
github.com/google/uuid v1.6.0/go.mod h1:TIyPZe4MgqvfeYDBFedMoGGpEw/LqOeaOT+nhxU+yHo= | ||
github.com/jmespath/go-jmespath v0.4.0 h1:BEgLn5cpjn8UN1mAw4NjwDrS35OdebyEtFe+9YPoQUg= | ||
github.com/jmespath/go-jmespath v0.4.0/go.mod h1:T8mJZnbsbmF+m6zOOFylbeCJqk5+pHWvzYPziyZiYoo= | ||
github.com/jmespath/go-jmespath/internal/testify v1.5.1 h1:shLQSRRSCCPj3f2gpwzGwWFoC7ycTf1rcQZHOlsJ6N8= | ||
github.com/jmespath/go-jmespath/internal/testify v1.5.1/go.mod h1:L3OGu8Wl2/fWfCI6z80xFu9LTZmf1ZRjMHUOPmWr69U= | ||
github.com/pmezard/go-difflib v1.0.0 h1:4DBwDE0NGyQoBHbLQYPwSUPoCMWR5BEzIk/f1lZbAQM= | ||
github.com/pmezard/go-difflib v1.0.0/go.mod h1:iKH77koFhYxTK1pcRnkKkqfTogsbg7gZNVY4sRDYZ/4= | ||
github.com/stretchr/objx v0.1.0/go.mod h1:HFkY916IF+rwdDfMAkV7OtwuqBVzrE8GR6GFx+wExME= | ||
gopkg.in/check.v1 v0.0.0-20161208181325-20d25e280405/go.mod h1:Co6ibVJAznAaIkqp8huTwlJQCZ016jof/cbN4VW5Yz0= | ||
gopkg.in/yaml.v2 v2.2.8 h1:obN1ZagJSUGI0Ek/LBmuj4SNLPfIny3KsKFopxRdj10= | ||
gopkg.in/yaml.v2 v2.2.8/go.mod h1:hI93XBmqTisBFMUTm0b8Fm+jr3Dg1NNxqwp+5A1VGuI= |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You could also write a Dafny function like
if OsLang.GetLanguageShort() == "Go" then
"something/keys.json"
else
"something_else/keys.json"
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks. I did not know I could get name of transpiling language in dafny.
I will look into it later.