-
Notifications
You must be signed in to change notification settings - Fork 8
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Shubham Chaturvedi
committed
Sep 12, 2024
1 parent
79aecd5
commit 992a33e
Showing
8 changed files
with
3,971 additions
and
1,302 deletions.
There are no files selected for viewing
This file contains 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
Large diffs are not rendered by default.
Oops, something went wrong.
38 changes: 38 additions & 0 deletions
38
...dels/aws-sdks/ddb/runtimes/go/ImplementationFromDafny-go/Com_Amazonaws_Dynamodb/extern.go
This file contains 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,38 @@ | ||
| package Com_Amazonaws_Dynamodb | ||
|
|
||
| import ( | ||
| "context" | ||
|
|
||
| "github.com/aws/aws-sdk-go-v2/config" | ||
| "github.com/aws/aws-sdk-go-v2/service/dynamodb" | ||
| _dafny "github.com/dafny-lang/DafnyRuntimeGo/dafny" | ||
| "github.com/dafny-lang/DafnyStandardLibGo/Wrappers" | ||
| "github.com/smithy-lang/smithy-dafny/ddb/ComAmazonawsDynamodbTypes" | ||
| "github.com/smithy-lang/smithy-dafny/ddb/DynamoDBwrapped" | ||
| ) | ||
|
|
||
| func (_static *CompanionStruct_Default___) DynamoDBClient() Wrappers.Result { | ||
| cfg, err := config.LoadDefaultConfig(context.TODO(), config.WithSharedConfigProfile("default")) | ||
| if err != nil { | ||
| panic(err) | ||
| } | ||
| return Wrappers.Companion_Result_.Create_Success_(&DynamoDBwrapped.Shim{Client: dynamodb.NewFromConfig(cfg, func(o *dynamodb.Options) { | ||
| o.Region = "us-west-2" | ||
| })}) | ||
| } | ||
|
|
||
| func (_static *CompanionStruct_Default___) RegionMatch(k ComAmazonawsDynamodbTypes.IDynamoDBClient, S _dafny.Sequence) Wrappers.Option { | ||
| var r = func() *string { | ||
| var s string | ||
| for i := _dafny.Iterate(S); ; { | ||
| val, ok := i() | ||
| if !ok { | ||
| return &[]string{s}[0] | ||
| } else { | ||
| s = s + string(val.(_dafny.Char)) | ||
| } | ||
| } | ||
| }() | ||
| var nc = k.(*DynamoDBwrapped.Shim).Client | ||
| return Wrappers.Companion_Option_.Create_Some_(nc.Options().Region == *r) | ||
| } |
24 changes: 24 additions & 0 deletions
24
TestModels/aws-sdks/ddb/runtimes/go/ImplementationFromDafny-go/go.mod
This file contains 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,24 @@ | ||
| module github.com/smithy-lang/smithy-dafny/ddb | ||
|
|
||
| go 1.23.0 | ||
|
|
||
| //TODO: Drop this after Dafny fixes the https://t.corp.amazon.com/P150784381 | ||
| replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../../DafnyRuntimeGo/ | ||
|
|
||
| replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ | ||
|
|
||
| require ( | ||
| github.com/aws/aws-sdk-go-v2/service/dynamodb v1.34.9 | ||
| github.com/dafny-lang/DafnyRuntimeGo v0.0.0-00010101000000-000000000000 | ||
| github.com/dafny-lang/DafnyStandardLibGo v0.0.0-00010101000000-000000000000 | ||
| ) | ||
|
|
||
| require ( | ||
| github.com/aws/aws-sdk-go-v2 v1.30.5 // indirect | ||
| github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.17 // indirect | ||
| github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.17 // indirect | ||
| github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.4 // indirect | ||
| github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.18 // indirect | ||
| github.com/aws/smithy-go v1.20.4 // indirect | ||
| github.com/jmespath/go-jmespath v0.4.0 // indirect | ||
| ) |
26 changes: 26 additions & 0 deletions
26
TestModels/aws-sdks/ddb/runtimes/go/ImplementationFromDafny-go/go.sum
This file contains 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,26 @@ | ||
| github.com/aws/aws-sdk-go-v2 v1.30.5 h1:mWSRTwQAb0aLE17dSzztCVJWI9+cRMgqebndjwDyK0g= | ||
| github.com/aws/aws-sdk-go-v2 v1.30.5/go.mod h1:CT+ZPWXbYrci8chcARI3OmI/qgd+f6WtuLOoaIA8PR0= | ||
| github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.17 h1:pI7Bzt0BJtYA0N/JEC6B8fJ4RBrEMi1LBrkMdFYNSnQ= | ||
| github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.17/go.mod h1:Dh5zzJYMtxfIjYW+/evjQ8uj2OyR/ve2KROHGHlSFqE= | ||
| github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.17 h1:Mqr/V5gvrhA2gvgnF42Zh5iMiQNcOYthFYwCyrnuWlc= | ||
| github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.17/go.mod h1:aLJpZlCmjE+V+KtN1q1uyZkfnUWpQGpbsn89XPKyzfU= | ||
| github.com/aws/aws-sdk-go-v2/service/dynamodb v1.34.9 h1:jbqgtdKfAXebx2/l2UhDEe/jmmCIhaCO3HFK71M7VzM= | ||
| github.com/aws/aws-sdk-go-v2/service/dynamodb v1.34.9/go.mod h1:N3YdUYxyxhiuAelUgCpSVBuBI1klobJxZrDtL+olu10= | ||
| github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.4 h1:KypMCbLPPHEmf9DgMGw51jMj77VfGPAN2Kv4cfhlfgI= | ||
| github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.4/go.mod h1:Vz1JQXliGcQktFTN/LN6uGppAIRoLBR2bMvIMP0gOjc= | ||
| github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.18 h1:GACdEPdpBE59I7pbfvu0/Mw1wzstlP3QtPHklUxybFE= | ||
| github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.18/go.mod h1:K+xV06+Wni4TSaOOJ1Y35e5tYOCUBYbebLKmJQQa8yY= | ||
| github.com/aws/smithy-go v1.20.4 h1:2HK1zBdPgRbjFOHlfeQZfpC4r72MOb9bZkiFwggKO+4= | ||
| github.com/aws/smithy-go v1.20.4/go.mod h1:irrKGvNn1InZwb2d7fkIRNucdfwR8R+Ts3wxYa/cJHg= | ||
| 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/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= |
35 changes: 35 additions & 0 deletions
35
TestModels/aws-sdks/ddb/runtimes/go/TestsFromDafny-go/go.mod
This file contains 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,35 @@ | ||
| module github.com/smithy-lang/smithy-dafny/ddb/test | ||
|
|
||
| go 1.23.0 | ||
|
|
||
| replace github.com/smithy-lang/smithy-dafny/ddb v0.0.0 => ../ImplementationFromDafny-go | ||
|
|
||
| //TODO: Drop this after Dafny fixes the https://t.corp.amazon.com/P150784381 | ||
| replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../../DafnyRuntimeGo/ | ||
|
|
||
| replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ | ||
|
|
||
| require ( | ||
| github.com/aws/aws-sdk-go-v2/service/dynamodb v1.34.9 | ||
| github.com/dafny-lang/DafnyRuntimeGo v0.0.0-00010101000000-000000000000 | ||
| github.com/dafny-lang/DafnyStandardLibGo v0.0.0-00010101000000-000000000000 | ||
| github.com/smithy-lang/smithy-dafny/ddb v0.0.0 | ||
| ) | ||
|
|
||
| require ( | ||
| github.com/aws/aws-sdk-go-v2 v1.30.5 // indirect | ||
| github.com/aws/aws-sdk-go-v2/config v1.27.33 // indirect | ||
| github.com/aws/aws-sdk-go-v2/credentials v1.17.32 // indirect | ||
| github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.13 // indirect | ||
| github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.17 // indirect | ||
| github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.17 // 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.4 // indirect | ||
| github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.18 // indirect | ||
| github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.19 // indirect | ||
| github.com/aws/aws-sdk-go-v2/service/sso v1.22.7 // indirect | ||
| github.com/aws/aws-sdk-go-v2/service/ssooidc v1.26.7 // indirect | ||
| github.com/aws/aws-sdk-go-v2/service/sts v1.30.7 // indirect | ||
| github.com/aws/smithy-go v1.20.4 // indirect | ||
| github.com/jmespath/go-jmespath v0.4.0 // indirect | ||
| ) |
42 changes: 42 additions & 0 deletions
42
TestModels/aws-sdks/ddb/runtimes/go/TestsFromDafny-go/go.sum
This file contains 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,42 @@ | ||
| github.com/aws/aws-sdk-go-v2 v1.30.5 h1:mWSRTwQAb0aLE17dSzztCVJWI9+cRMgqebndjwDyK0g= | ||
| github.com/aws/aws-sdk-go-v2 v1.30.5/go.mod h1:CT+ZPWXbYrci8chcARI3OmI/qgd+f6WtuLOoaIA8PR0= | ||
| github.com/aws/aws-sdk-go-v2/config v1.27.33 h1:Nof9o/MsmH4oa0s2q9a0k7tMz5x/Yj5k06lDODWz3BU= | ||
| github.com/aws/aws-sdk-go-v2/config v1.27.33/go.mod h1:kEqdYzRb8dd8Sy2pOdEbExTTF5v7ozEXX0McgPE7xks= | ||
| github.com/aws/aws-sdk-go-v2/credentials v1.17.32 h1:7Cxhp/BnT2RcGy4VisJ9miUPecY+lyE9I8JvcZofn9I= | ||
| github.com/aws/aws-sdk-go-v2/credentials v1.17.32/go.mod h1:P5/QMF3/DCHbXGEGkdbilXHsyTBX5D3HSwcrSc9p20I= | ||
| github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.13 h1:pfQ2sqNpMVK6xz2RbqLEL0GH87JOwSxPV2rzm8Zsb74= | ||
| github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.13/go.mod h1:NG7RXPUlqfsCLLFfi0+IpKN4sCB9D9fw/qTaSB+xRoU= | ||
| github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.17 h1:pI7Bzt0BJtYA0N/JEC6B8fJ4RBrEMi1LBrkMdFYNSnQ= | ||
| github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.17/go.mod h1:Dh5zzJYMtxfIjYW+/evjQ8uj2OyR/ve2KROHGHlSFqE= | ||
| github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.17 h1:Mqr/V5gvrhA2gvgnF42Zh5iMiQNcOYthFYwCyrnuWlc= | ||
| github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.17/go.mod h1:aLJpZlCmjE+V+KtN1q1uyZkfnUWpQGpbsn89XPKyzfU= | ||
| 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.34.9 h1:jbqgtdKfAXebx2/l2UhDEe/jmmCIhaCO3HFK71M7VzM= | ||
| github.com/aws/aws-sdk-go-v2/service/dynamodb v1.34.9/go.mod h1:N3YdUYxyxhiuAelUgCpSVBuBI1klobJxZrDtL+olu10= | ||
| github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.4 h1:KypMCbLPPHEmf9DgMGw51jMj77VfGPAN2Kv4cfhlfgI= | ||
| github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.4/go.mod h1:Vz1JQXliGcQktFTN/LN6uGppAIRoLBR2bMvIMP0gOjc= | ||
| github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.18 h1:GACdEPdpBE59I7pbfvu0/Mw1wzstlP3QtPHklUxybFE= | ||
| github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.18/go.mod h1:K+xV06+Wni4TSaOOJ1Y35e5tYOCUBYbebLKmJQQa8yY= | ||
| github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.19 h1:rfprUlsdzgl7ZL2KlXiUAoJnI/VxfHCvDFr2QDFj6u4= | ||
| github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.19/go.mod h1:SCWkEdRq8/7EK60NcvvQ6NXKuTcchAD4ROAsC37VEZE= | ||
| github.com/aws/aws-sdk-go-v2/service/sso v1.22.7 h1:pIaGg+08llrP7Q5aiz9ICWbY8cqhTkyy+0SHvfzQpTc= | ||
| github.com/aws/aws-sdk-go-v2/service/sso v1.22.7/go.mod h1:eEygMHnTKH/3kNp9Jr1n3PdejuSNcgwLe1dWgQtO0VQ= | ||
| github.com/aws/aws-sdk-go-v2/service/ssooidc v1.26.7 h1:/Cfdu0XV3mONYKaOt1Gr0k1KvQzkzPyiKUdlWJqy+J4= | ||
| github.com/aws/aws-sdk-go-v2/service/ssooidc v1.26.7/go.mod h1:bCbAxKDqNvkHxRaIMnyVPXPo+OaPRwvmgzMxbz1VKSA= | ||
| github.com/aws/aws-sdk-go-v2/service/sts v1.30.7 h1:NKTa1eqZYw8tiHSRGpP0VtTdub/8KNk8sDkNPFaOKDE= | ||
| github.com/aws/aws-sdk-go-v2/service/sts v1.30.7/go.mod h1:NXi1dIAGteSaRLqYgarlhP/Ij0cFT+qmCwiJqWh/U5o= | ||
| github.com/aws/smithy-go v1.20.4 h1:2HK1zBdPgRbjFOHlfeQZfpC4r72MOb9bZkiFwggKO+4= | ||
| github.com/aws/smithy-go v1.20.4/go.mod h1:irrKGvNn1InZwb2d7fkIRNucdfwR8R+Ts3wxYa/cJHg= | ||
| 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/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= |
This file contains 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