Skip to content
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

feat(TestModel): Add CallingAWSSDKFromLocal #538

Draft
wants to merge 179 commits into
base: Golang/dev
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
179 commits
Select commit Hold shift + click to select a range
d5b146a
Init CallingAWSSDKFromLocalService
rishav-karanjit Aug 21, 2024
8cad40d
Add Makefile
rishav-karanjit Aug 21, 2024
c3c4bcd
Add DotNet Extern
rishav-karanjit Aug 22, 2024
3f2766d
A lot of changes
rishav-karanjit Aug 23, 2024
5c1a475
A lot of changes
rishav-karanjit Aug 23, 2024
1428f53
Correct function name
rishav-karanjit Aug 23, 2024
b6153fc
Add externs
rishav-karanjit Aug 23, 2024
60536c2
Update Model
rishav-karanjit Aug 23, 2024
5937497
Update project file
rishav-karanjit Aug 23, 2024
fb78c09
Add project file
rishav-karanjit Aug 23, 2024
18f0711
Project file dotnet'
rishav-karanjit Aug 23, 2024
0adee61
Add all updates
rishav-karanjit Aug 24, 2024
fcb2ecf
Lot of changes
rishav-karanjit Aug 24, 2024
0030cd3
Add DDB call
rishav-karanjit Aug 25, 2024
5dd7d6f
Add KMS
rishav-karanjit Aug 25, 2024
9e0542f
Update make file
rishav-karanjit Aug 25, 2024
5db5cfe
Format Java
rishav-karanjit Aug 26, 2024
3bf0b36
Add CallKMSEnsuresPublicly
rishav-karanjit Aug 26, 2024
1a5b4b5
Fix CallKMSEnsuresPublicly func params
rishav-karanjit Aug 26, 2024
4bbf2a6
Add CallingAWSSDKFromLocalService in disabled tests
rishav-karanjit Aug 26, 2024
a92f50c
Check for SDK error - TODO wrapped getting error
rishav-karanjit Aug 26, 2024
06d7889
Add Encrypt API and refactoring
rishav-karanjit Aug 27, 2024
32f14f5
Rename CallDDB to CallDDBGetKey
rishav-karanjit Aug 27, 2024
473be0f
Update table name for CI
rishav-karanjit Aug 27, 2024
478a2e1
rename CallDDBGetKey to CallDDBGetItem
rishav-karanjit Aug 27, 2024
2b598e7
Add pre and post condition
rishav-karanjit Sep 2, 2024
56cd0eb
Make error to ComAmazonawsDynamodb and ComAmazonawsKms
rishav-karanjit Sep 2, 2024
76840fa
Fixes
rishav-karanjit Sep 3, 2024
eb832a8
Fixes
rishav-karanjit Sep 3, 2024
e8ce1f4
Merge branch 'main-1.x' into rishav-add-CallingAWSSDK
rishav-karanjit Sep 3, 2024
2615a73
Refactor makefile
rishav-karanjit Sep 3, 2024
20199da
Refactor makefile again
rishav-karanjit Sep 3, 2024
93684bb
Add proj ref and compile include
rishav-karanjit Sep 3, 2024
0b0f1ed
Fixes
rishav-karanjit Sep 3, 2024
4ac299e
Change dotnet and test
rishav-karanjit Sep 3, 2024
327746c
Revert "Change dotnet and test"
rishav-karanjit Sep 4, 2024
992c669
Add MakeFile
rishav-karanjit Sep 4, 2024
31ab1d9
Update Makefile
rishav-karanjit Sep 4, 2024
8769cee
Revert "Revert "Change dotnet and test""
rishav-karanjit Sep 4, 2024
046b73c
Add python runtime
rishav-karanjit Sep 4, 2024
38aae8e
Update dependencies
rishav-karanjit Sep 4, 2024
7791bae
Update dependencies
rishav-karanjit Sep 4, 2024
6a4e630
Merge remote-tracking branch 'origin/Golang/dev' into rishav-add-Call…
rishav-karanjit Sep 4, 2024
72b4384
Revert changes to model.json in KMS
rishav-karanjit Sep 4, 2024
4bd8251
Update MakeFile with Go module
rishav-karanjit Sep 4, 2024
a4431a7
Add Go comment
rishav-karanjit Sep 4, 2024
a2cf766
Revert "Revert changes to model.json in KMS"
rishav-karanjit Sep 4, 2024
0e8c581
Update smithy model for v2 smithy of kms
rishav-karanjit Sep 4, 2024
d37b806
Update to return keyid:
rishav-karanjit Sep 5, 2024
2af2588
Merge branch 'Golang/dev' of https://github.com/smithy-lang/smithy-da…
rishav-karanjit Sep 11, 2024
a4cb20b
Merge branch 'Golang/dev' into rishav-add-CallingAWSSDK
rishav-karanjit Sep 12, 2024
be7301c
Commit go mod
rishav-karanjit Sep 12, 2024
db0e27a
Add everything
rishav-karanjit Sep 13, 2024
712cbcf
Add extern
rishav-karanjit Sep 13, 2024
ec09dc1
Push KMS runtime
rishav-karanjit Sep 13, 2024
7783d4e
Merge from Golang/dev
rishav-karanjit Sep 17, 2024
ed8eca6
Update make file
rishav-karanjit Sep 17, 2024
1d832a8
If dep service has no local service trait then continue
rishav-karanjit Sep 17, 2024
b7ace1c
Update make file
rishav-karanjit Sep 17, 2024
ba93f86
Service does not have a special logic for Referred shape
rishav-karanjit Sep 17, 2024
51ca930
Update smithyTypesNamespace
rishav-karanjit Sep 17, 2024
d4b7c82
Update structure shape in reference with serviceShape
rishav-karanjit Sep 17, 2024
9a8e588
Runtime changes
rishav-karanjit Sep 18, 2024
f362bb0
push everything for now
rishav-karanjit Sep 19, 2024
fa53236
Add support for recursive shapes in Go (#607)
rishav-karanjit Sep 23, 2024
015825f
Remove redundant files
rishav-karanjit Sep 23, 2024
355d74a
CI fixes
rishav-karanjit Sep 23, 2024
aee93ba
Remove redundant files
rishav-karanjit Sep 23, 2024
9a452e2
Refactoring
rishav-karanjit Sep 23, 2024
e92d40c
Update src module name
rishav-karanjit Sep 23, 2024
99df7d7
Update module name
rishav-karanjit Sep 23, 2024
401c64d
Update module name
rishav-karanjit Sep 23, 2024
0d4547e
Add go mod
rishav-karanjit Sep 23, 2024
ae6eecb
update module name
rishav-karanjit Sep 23, 2024
de202ba
Format
rishav-karanjit Sep 23, 2024
bb25f0a
Change shape name
rishav-karanjit Sep 23, 2024
78cca65
Remove redundant codes
rishav-karanjit Sep 23, 2024
1870322
Remove redundant codes
rishav-karanjit Sep 23, 2024
7ce1847
Add go mod
rishav-karanjit Sep 23, 2024
c8883fb
Update Makefile
rishav-karanjit Sep 23, 2024
dd83e91
rm go mod
rishav-karanjit Sep 23, 2024
94afffe
Add api client and go mod
rishav-karanjit Sep 23, 2024
013b2dd
Add go mod
rishav-karanjit Sep 23, 2024
d1b6f1f
Add runtime
rishav-karanjit Sep 24, 2024
99c98a9
Add runtime
rishav-karanjit Sep 24, 2024
e7c8cde
Go mod Go sum
rishav-karanjit Sep 24, 2024
3ca8c6f
Update test model
rishav-karanjit Sep 24, 2024
aaa0ddd
Update test model
rishav-karanjit Sep 24, 2024
c23a6cf
fix dafny client
rishav-karanjit Sep 25, 2024
5779b87
Local service fixes
rishav-karanjit Sep 25, 2024
b910eeb
Fix var name
rishav-karanjit Sep 26, 2024
31fabcf
update runtime
rishav-karanjit Sep 26, 2024
f1e5936
Update test model
rishav-karanjit Sep 26, 2024
d5291a3
Remove redundant codes
rishav-karanjit Sep 26, 2024
1226428
Update go mod
rishav-karanjit Sep 26, 2024
b7eabcd
rm redundant files
rishav-karanjit Sep 26, 2024
417f9be
wrap not opaque error into opaque error
rishav-karanjit Sep 26, 2024
dc3f5fa
Revert "Revert "Revert "Change dotnet and test"""
rishav-karanjit Sep 26, 2024
f0e08c7
Recursive shape support in aws sdk go
rishav-karanjit Sep 28, 2024
135309b
Add is timestamp
rishav-karanjit Sep 28, 2024
ec28625
Copy local service changes to sdk
rishav-karanjit Sep 29, 2024
622071e
PR Comment fix
rishav-karanjit Sep 29, 2024
0c6ff38
comment fix
rishav-karanjit Sep 29, 2024
a21c2ef
Namespace fix
rishav-karanjit Sep 30, 2024
4a70ece
Service does not have special logic
rishav-karanjit Sep 30, 2024
0b85561
Fix error handling sdk v2
rishav-karanjit Sep 30, 2024
99ce8d5
Remove print
rishav-karanjit Sep 30, 2024
8155e77
Fix comments
rishav-karanjit Sep 30, 2024
f176be6
Add recursive shape to disabled test except in go
rishav-karanjit Sep 30, 2024
c00a978
Delete redundant file
rishav-karanjit Sep 30, 2024
60ad10c
Add recursive shape to disabled test except in go
rishav-karanjit Sep 30, 2024
be6c61b
Revert "Add recursive shape to disabled test except in go"
rishav-karanjit Sep 30, 2024
e093887
revert formating -- think about it later
rishav-karanjit Oct 1, 2024
12e2aed
Revert "Add recursive shape to disabled test except in go"
rishav-karanjit Oct 1, 2024
477e6ef
Add {} to if else and make data type final whereever possible
rishav-karanjit Oct 1, 2024
84aec71
Don't move extern rn
rishav-karanjit Oct 1, 2024
b2d454b
Add todo to make file
rishav-karanjit Oct 1, 2024
a285f84
ENABLE_EXTERN_PROCESSING
rishav-karanjit Oct 1, 2024
3601472
nit fix
rishav-karanjit Oct 1, 2024
1241dc0
Remove Rust benerated in makefile
rishav-karanjit Oct 1, 2024
0a37314
bring make the makefile
rishav-karanjit Oct 1, 2024
5bd09e1
remove shim
rishav-karanjit Oct 1, 2024
dbbca19
Bring back makefile
rishav-karanjit Oct 1, 2024
00b06ad
add final
rishav-karanjit Oct 1, 2024
2ea8dbf
rm redundant call
rishav-karanjit Oct 1, 2024
87260b7
used switch case
rishav-karanjit Oct 2, 2024
d8977b4
used concat
rishav-karanjit Oct 2, 2024
eab1449
Extract out into a var and concat
rishav-karanjit Oct 2, 2024
80d8381
remove a hack for initialized and not used
rishav-karanjit Oct 2, 2024
3a7ed5d
Add some comments
rishav-karanjit Oct 2, 2024
7bac1de
remove a hack for initialized and not used
rishav-karanjit Oct 2, 2024
d88e9d0
remove boolean casting in isOptional
rishav-karanjit Oct 2, 2024
03cc3f5
Update output type
rishav-karanjit Oct 2, 2024
89c6054
Use GoCodegenUtils
rishav-karanjit Oct 2, 2024
2fc55a4
remove () in return
rishav-karanjit Oct 2, 2024
4274db5
remove () in return
rishav-karanjit Oct 2, 2024
152922b
remove hack for init but not used
rishav-karanjit Oct 2, 2024
bd2619d
remove hack for init but not used
rishav-karanjit Oct 2, 2024
c00fd79
remove hack for init but not used
rishav-karanjit Oct 2, 2024
dd0a5db
remove hack for init but not used
rishav-karanjit Oct 2, 2024
368f395
remove hack for init but not used
rishav-karanjit Oct 2, 2024
aa207bb
bring back removed files
rishav-karanjit Oct 2, 2024
c51bed4
Combine these two statements
rishav-karanjit Oct 2, 2024
0b6e0ba
Add todo and remove unused imports
rishav-karanjit Oct 2, 2024
842d5da
refactor get smithy type
rishav-karanjit Oct 2, 2024
1cf85e6
use GoCodegenUtils
rishav-karanjit Oct 2, 2024
e1099df
use GoCodegenUtils
rishav-karanjit Oct 2, 2024
9631e0b
update list and map to not get init and not use error
rishav-karanjit Oct 2, 2024
4e535fd
remove commented code
rishav-karanjit Oct 2, 2024
64f2109
add timestamp import
rishav-karanjit Oct 2, 2024
9bcd8cc
unAssertDataSource
rishav-karanjit Oct 2, 2024
3163256
Union wrapper optional only if isoptional
rishav-karanjit Oct 2, 2024
d3fa74f
union is Wrappers.Option if optional
rishav-karanjit Oct 2, 2024
2faf98d
Move to function
rishav-karanjit Oct 2, 2024
6f5bb33
Move to a function
rishav-karanjit Oct 2, 2024
ce6c4cb
Nit comment
rishav-karanjit Oct 2, 2024
012ec0b
nit comments
rishav-karanjit Oct 2, 2024
1e3ca27
use interface instead of Hashmap
rishav-karanjit Oct 2, 2024
424f689
Use Map instead of hashmap
rishav-karanjit Oct 2, 2024
67f8f03
update kms and ddb extern
rishav-karanjit Oct 3, 2024
5280f59
rm redundant runtime files in kms:
rishav-karanjit Oct 3, 2024
5c31d4a
add disabled test in all languages
rishav-karanjit Oct 3, 2024
f8031b5
Merge branch 'Golang/dev' into rishav-add-CallingAWSSDK
rishav-karanjit Oct 3, 2024
e61d71f
remove check for num of items
rishav-karanjit Oct 3, 2024
111ca7e
Merge branch 'rishav-add-CallingAWSSDK' of https://github.com/smithy-…
rishav-karanjit Oct 3, 2024
841c7f3
fix namespace for TrentService and DynamoDB_20120810
rishav-karanjit Oct 3, 2024
bb01ef8
add imports
rishav-karanjit Oct 3, 2024
7969a94
merge with recursive shape branch
rishav-karanjit Oct 3, 2024
86a755f
fix output type for interface client (IDynamoDBClient or ikmsclient)
rishav-karanjit Oct 3, 2024
b270c53
fix reference shape
rishav-karanjit Oct 3, 2024
cedd2c2
fix gap from MPL
rishav-karanjit Oct 7, 2024
0135c25
remove shapeNamespaceDafnyTranspiled and replace it with DafnyNameRes…
rishav-karanjit Oct 8, 2024
ee3fd1c
Shim namespace in pascal case
rishav-karanjit Oct 8, 2024
6c31fb6
Merge branch 'rishav-add-CallingAWSSDK' of https://github.com/smithy-…
rishav-karanjit Oct 8, 2024
b186a1d
fix old commits
rishav-karanjit Oct 8, 2024
b34be61
fix old commits
rishav-karanjit Oct 8, 2024
c124806
add import errors
rishav-karanjit Oct 8, 2024
5afef0f
add import time
rishav-karanjit Oct 8, 2024
11823a9
add import time
rishav-karanjit Oct 8, 2024
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
2 changes: 1 addition & 1 deletion TestModels/Aggregate/src/Index.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -27,4 +27,4 @@ module {:extern "simple.aggregate.internaldafny"} SimpleAggregate refines Abstra
Modifies := Operations.ModifiesInternalConfig(config) + {History};
}
}
}
}
2 changes: 1 addition & 1 deletion TestModels/Aggregate/src/WrappedSimpleAggregateImpl.dfy
Original file line number Diff line number Diff line change
Expand Up @@ -7,4 +7,4 @@ module {:extern "simple.aggregate.internaldafny.wrapped"} WrappedSimpleAggregate
function method WrappedDefaultSimpleAggregateConfig(): SimpleAggregateConfig {
SimpleAggregateConfig
}
}
}
70 changes: 70 additions & 0 deletions TestModels/CallingAWSSDKFromLocalService/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
# Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: Apache-2.0

CORES=10

ENABLE_EXTERN_PROCESSING=1

include ../SharedMakefile.mk

PROJECT_SERVICES := \
SimpleCallingAWSSDKFromLocalService

PROJECT_DEPENDENCIES := \
aws-sdks/kms \
aws-sdks/ddb

PROJECT_INDEX := \
aws-sdks/kms/src/Index.dfy \
aws-sdks/ddb/src/Index.dfy

SERVICE_NAMESPACE_SimpleCallingAWSSDKFromLocalService=simple.callingawssdkfromlocalservice

SERVICE_DEPS_SimpleCallingAWSSDKFromLocalService := \
aws-sdks/kms \
aws-sdks/ddb

SMITHY_DEPS=dafny-dependencies/Model/traits.smithy

# Python

PYTHON_MODULE_NAME=simple_callingawssdkfromlocalservice

PYTHON_DEPENDENCY_MODULE_NAMES := \
--dependency-library-name=com.amazonaws.dynamodb=com_amazonaws_dynamodb \
--dependency-library-name=com.amazonaws.kms=com_amazonaws_kms

TRANSLATION_RECORD_PYTHON := \
--translation-record ../dafny-dependencies/StandardLibrary/runtimes/python/src/standard_library/internaldafny/generated/dafny_src-py.dtr \
--translation-record ../aws-sdks/ddb/runtimes/python/src/com_amazonaws_dynamodb/internaldafny/generated/dafny_src-py.dtr \
--translation-record ../aws-sdks/kms/runtimes/python/src/com_amazonaws_kms/internaldafny/generated/dafny_src-py.dtr

TRANSLATION_RECORD_PYTHON := \
--translation-record ../dafny-dependencies/StandardLibrary/runtimes/python/src/standard_library/internaldafny/generated/dafny_src-py.dtr

# Constants for languages that drop extern names (Python, Go)

TYPES_FILE_PATH=Model/SimpleCallingawssdkfromlocalserviceTypes.dfy
TYPES_FILE_WITH_EXTERN_STRING="module {:extern \"simple.callingawssdkfromlocalservice.internaldafny.types\" } SimpleCallingawssdkfromlocalserviceTypes"
TYPES_FILE_WITHOUT_EXTERN_STRING="module SimpleCallingawssdkfromlocalserviceTypes"

INDEX_FILE_PATH=src/Index.dfy
INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.callingawssdkfromlocalservice.internaldafny\" } SimpleCallingAWSSDKFromLocalService refines AbstractSimpleCallingawssdkfromlocalserviceService {"
INDEX_FILE_WITHOUT_EXTERN_STRING="module SimpleCallingAWSSDKFromLocalService refines AbstractSimpleCallingawssdkfromlocalserviceService {"

WRAPPED_INDEX_FILE_PATH=src/WrappedSimpleCallingAWSSDKFromLocalServiceImpl.dfy
WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"simple.callingawssdkfromlocalservice.internaldafny.wrapped\"} WrappedSimpleCallingAWSSDKFromLocalServiceService refines WrappedAbstractSimpleCallingawssdkfromlocalserviceService {"
WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedSimpleCallingAWSSDKFromLocalServiceService refines WrappedAbstractSimpleCallingawssdkfromlocalserviceService {"

# Go

GO_DEPENDENCY_MODULE_NAMES := \
--dependency-library-name=com.amazonaws.dynamodb=github.com/smithy-lang/smithy-dafny/ddb \
--dependency-library-name=com.amazonaws.kms=github.com/smithy-lang/smithy-dafny/kms

GO_MODULE_NAME="github.com/smithy-lang/smithy-dafny/TestModels/CallingAWSSDKFromLocalService"

TRANSLATION_RECORD_GO := \
dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
aws-sdks/kms/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
aws-sdks/ddb/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0
namespace simple.callingawssdkfromlocalservice

use aws.polymorph#reference
use com.amazonaws.dynamodb#DynamoDB_20120810
use com.amazonaws.kms#TrentService


@reference(service: DynamoDB_20120810)
structure DdbClientReference {}

@reference(service: TrentService)
structure KmsClientReference {}

@aws.polymorph#localService(
sdkId: "SimpleCallingAWSSDKFromLocalService",
config: SimpleCallingAWSSDKFromLocalServiceConfig,
dependencies: [
DynamoDB_20120810,
TrentService
]
)

service SimpleCallingAWSSDKFromLocalService {
version: "2021-11-01",
resources: [],
operations: [
CallDDBScan,
CallKMSEncrypt],
errors: [ SimpleCallingAWSSDKFromLocalServiceException ],
}

structure SimpleCallingAWSSDKFromLocalServiceConfig {}

operation CallDDBScan {
input: CallDDBScanInput,
output: CallDDBScanOutput,
}

structure CallDDBScanInput {
@required
ddbClient: DdbClientReference,
@required
tableArn: com.amazonaws.dynamodb#TableArn
}

structure CallDDBScanOutput {
@required
itemOutput: com.amazonaws.dynamodb#Integer,
}

operation CallKMSEncrypt {
input: CallKMSEncryptInput,
output: CallKMSEncryptOutput,
}

structure CallKMSEncryptInput {
@required
kmsClient: KmsClientReference,
@required
keyId: com.amazonaws.kms#KeyIdType,
@required
plaintext: com.amazonaws.kms#PlaintextType
}

structure CallKMSEncryptOutput {
@required
encryptOutput: com.amazonaws.kms#KeyIdType,
}

@error("client")
structure SimpleCallingAWSSDKFromLocalServiceException {
@required
message: String,
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
module github.com/smithy-lang/smithy-dafny/TestModels/CallingAWSSDKFromLocalService

go 1.23.0

require github.com/dafny-lang/DafnyStandardLibGo v0.0.0

require github.com/dafny-lang/DafnyRuntimeGo v0.0.0

require (
github.com/aws/smithy-go v1.20.4
github.com/smithy-lang/smithy-dafny/ddb v0.0.0
github.com/smithy-lang/smithy-dafny/kms 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/dynamodb v1.34.9 // 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/kms v1.35.7 // 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/jmespath/go-jmespath v0.4.0 // indirect
)

//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/

replace github.com/smithy-lang/smithy-dafny/kms => /Users/rishavkj/Documents/Storage/Team-Repos/smithy-dafny/TestModels/aws-sdks/kms/runtimes/go/ImplementationFromDafny-go/

replace github.com/smithy-lang/smithy-dafny/ddb => /Users/rishavkj/Documents/Storage/Team-Repos/smithy-dafny/TestModels/aws-sdks/ddb/runtimes/go/ImplementationFromDafny-go/
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
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/kms v1.35.7 h1:v0D1LeMkA/X+JHAZWERrr+sUGOt8KrCZKnJA6KszkcE=
github.com/aws/aws-sdk-go-v2/service/kms v1.35.7/go.mod h1:K9lwD0Rsx9+NSaJKsdAdlDK4b2G4KKOEve9PzHxPoMI=
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=
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
module github.com/smithy-lang/smithy-dafny/TestModels/CallingAWSSDKFromLocalService/test

go 1.23.0

require github.com/dafny-lang/DafnyStandardLibGo v0.0.0

require (
github.com/aws/smithy-go v1.20.4
github.com/dafny-lang/DafnyRuntimeGo v0.0.0
github.com/smithy-lang/smithy-dafny/TestModels/CallingAWSSDKFromLocalService v0.0.0
github.com/smithy-lang/smithy-dafny/ddb v0.0.0
github.com/smithy-lang/smithy-dafny/kms 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/dynamodb v1.34.9 // 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/kms v1.35.7 // 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/jmespath/go-jmespath v0.4.0 // indirect
)

replace github.com/smithy-lang/smithy-dafny/TestModels/CallingAWSSDKFromLocalService 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/

replace github.com/smithy-lang/smithy-dafny/kms => /Users/rishavkj/Documents/Storage/Team-Repos/smithy-dafny/TestModels/aws-sdks/kms/runtimes/go/ImplementationFromDafny-go/

replace github.com/smithy-lang/smithy-dafny/ddb => /Users/rishavkj/Documents/Storage/Team-Repos/smithy-dafny/TestModels/aws-sdks/ddb/runtimes/go/ImplementationFromDafny-go/
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
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/kms v1.35.7 h1:v0D1LeMkA/X+JHAZWERrr+sUGOt8KrCZKnJA6KszkcE=
github.com/aws/aws-sdk-go-v2/service/kms v1.35.7/go.mod h1:K9lwD0Rsx9+NSaJKsdAdlDK4b2G4KKOEve9PzHxPoMI=
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=
Loading
Loading