Merge branch 'Golang/dev' into rishav-awssdkFromLocal-Testmodel

.github/workflows/test_models_go_tests.yml

@@ -50,15 +50,16 @@ jobs:
         with:
           submodules: recursive
 
+      # TODO: Use the released version once all the Dafny issues aew fixed.
       - name: Setup Dafny
         uses: dafny-lang/[email protected]
         with:
-          dafny-version: ${{ inputs.dafny }}
+          dafny-version: "nightly-latest"
 
       - name: Install Go
         uses: actions/setup-go@v2
         with:
-          go-version: "1.21"
+          go-version: "1.23"
 
       - name: Install Go imports
         run: |

SmithyDafnyMakefile.mk

@@ -468,8 +468,7 @@ polymorph_go:
 _polymorph_go: OUTPUT_GO=--output-go $(LIBRARY_ROOT)/runtimes/go/
 _polymorph_go: MODULE_NAME=--library-name $(GO_MODULE_NAME)
 _polymorph_go: DEPENDENCY_MODULE_NAMES = $(GO_DEPENDENCY_MODULE_NAMES)
-#TODO: Drop go_imports till Dafny bugs are fix otherwise this fails
-_polymorph_go: _polymorph _mv_polymorph_go
+_polymorph_go: _polymorph _mv_polymorph_go run_goimports
 
 run_goimports:
 	cd runtimes/go/ImplementationFromDafny-go && goimports -w .
@@ -696,17 +695,19 @@ transpile_go: $(if $(ENABLE_EXTERN_PROCESSING), _no_extern_post_transpile, )
 
 transpile_implementation_go: TARGET=go
 transpile_implementation_go: OUT=runtimes/go/ImplementationFromDafny
+transpile_implementation_go: DAFNY_OPTIONS=--allow-warnings
 transpile_implementation_go: TRANSPILE_DEPENDENCIES=$(patsubst %, --library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX))
 transpile_implementation_go: TRANSLATION_RECORD=$(patsubst %, --translation-record:$(PROJECT_ROOT)/%, $(TRANSLATION_RECORD_GO))
 transpile_implementation_go: TRANSPILE_MODULE_NAME=--go-module-name $(GO_MODULE_NAME)
-transpile_implementation_go: _transpile_implementation_all_new_cli
+transpile_implementation_go: _transpile_implementation_all
 
 transpile_test_go: TARGET=go
 transpile_test_go: OUT=runtimes/go/TestsFromDafny
+transpile_test_go: DAFNY_OPTIONS=--allow-warnings --include-test-runner
 transpile_test_go: TRANSPILE_DEPENDENCIES=$(patsubst %, --library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX))
 transpile_test_go: TRANSLATION_RECORD=$(patsubst %, --translation-record:$(PROJECT_ROOT)/%, $(TRANSLATION_RECORD_GO)) $(patsubst %, --translation-record:$(LIBRARY_ROOT)/%, runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr)
 transpile_test_go: TRANSPILE_MODULE_NAME=--go-module-name $(GO_MODULE_NAME)/test
-transpile_test_go: _transpile_test_all_new_cli
+transpile_test_go: _transpile_test_all
 
 transpile_dependencies_go: LANG=go
 transpile_dependencies_go: transpile_dependencies
@@ -716,7 +717,7 @@ clean_go:
 	rm -rf $(LIBRARY_ROOT)/runtimes/go/TestsFromDafny-go
 
 test_go:
-	cd runtimes/go/TestsFromDafny-go && go run TestsFromDafny.go
+	cd runtimes/go/TestsFromDafny-go && go mod tidy && go run TestsFromDafny.go
 
 ########################## Python targets
 

TestModels/Aggregate/runtimes/go/ImplementationFromDafny-go/go.mod

@@ -4,9 +4,6 @@ go 1.23.0
 
 require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
 
-require github.com/dafny-lang/DafnyRuntimeGo v0.0.0
-
-//TODO: Drop this after Dafny fixes the https://t.corp.amazon.com/P150784381
-replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../DafnyRuntimeGo/
+require github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
 
 replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/

TestModels/Aggregate/runtimes/go/TestsFromDafny-go/go.mod

@@ -5,13 +5,10 @@ go 1.23.0
 require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
 
 require (
-	github.com/dafny-lang/DafnyRuntimeGo v0.0.0
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
 	github.com/smithy-lang/smithy-dafny/TestModels/Aggregate v0.0.0
 )
 
 replace github.com/smithy-lang/smithy-dafny/TestModels/Aggregate 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/

TestModels/CodegenPatches/Model/SimpleCodegenpatchesTypes.dfy

@@ -102,7 +102,7 @@ module {:extern "simple.codegenpatches.internaldafny.types" } SimpleCodegenpatch
     // || (!exit(A(I)) && !access(B(I)))
     | CollectionOfErrors(list: seq<Error>, nameonly message: string)
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object)
+    | Opaque(obj: object, alt_text : string)
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractSimpleCodegenpatchesService
@@ -197,4 +197,4 @@ abstract module AbstractSimpleCodegenpatchesOperations {
     ensures
       && ValidInternalConfig?(config)
     ensures GetStringEnsuresPublicly(input, output)
-}
+}

TestModels/CodegenPatches/Model/SimpleCodegenpatchesTypesWrapped.dfy

@@ -17,4 +17,4 @@ abstract module WrappedAbstractSimpleCodegenpatchesService {
               && fresh(res.value.Modifies)
               && fresh(res.value.History)
               && res.value.ValidState()
-}
+}

TestModels/CodegenPatches/runtimes/go/TestsFromDafny-go/go.mod

@@ -5,7 +5,7 @@ go 1.23.0
 require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
 
 require (
-	github.com/dafny-lang/DafnyRuntimeGo v0.0.0
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
 	github.com/smithy-lang/smithy-dafny/TestModels/CodegenPatches v0.0.0
 )
 

TestModels/Constraints/runtimes/go/ImplementationFromDafny-go/go.mod

@@ -2,11 +2,9 @@ module github.com/smithy-lang/smithy-dafny/TestModels/Constraints
 
 go 1.23.0
 
-require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
-
-require github.com/dafny-lang/DafnyRuntimeGo v0.0.0
-
-//TODO: Drop this after Dafny fixes the https://t.corp.amazon.com/P150784381
-replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../DafnyRuntimeGo/
+require (
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
+	github.com/dafny-lang/DafnyStandardLibGo v0.0.0
+)
 
 replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/

TestModels/Constraints/runtimes/go/TestsFromDafny-go/go.mod

@@ -5,13 +5,10 @@ go 1.23.0
 require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
 
 require (
-	github.com/dafny-lang/DafnyRuntimeGo v0.0.0
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
 	github.com/smithy-lang/smithy-dafny/TestModels/Constraints v0.0.0
 )
 
 replace github.com/smithy-lang/smithy-dafny/TestModels/Constraints 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/

TestModels/Dependencies/runtimes/go/ImplementationFromDafny-go/go.mod

@@ -4,18 +4,16 @@ 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/smithy-lang/smithy-dafny/TestModels/Constraints v0.0.0
 
 require github.com/smithy-lang/smithy-dafny/TestModels/Extendable v0.0.0
 
 require github.com/smithy-lang/smithy-dafny/TestModels/Resource v0.0.0
 
-require github.com/smithy-lang/smithy-dafny/TestModels/Errors v0.0.0
-
-//TODO: Drop this after Dafny fixes the https://t.corp.amazon.com/P150784381
-replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../DafnyRuntimeGo/
+require (
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
+	github.com/smithy-lang/smithy-dafny/TestModels/Errors v0.0.0
+)
 
 replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/
 

TestModels/Dependencies/runtimes/go/TestsFromDafny-go/go.mod

@@ -4,13 +4,14 @@ 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/smithy-lang/smithy-dafny/TestModels/Constraints v0.0.0
 
 require github.com/smithy-lang/smithy-dafny/TestModels/Extendable v0.0.0
 
-require github.com/smithy-lang/smithy-dafny/TestModels/Resource v0.0.0
+require (
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
+	github.com/smithy-lang/smithy-dafny/TestModels/Resource v0.0.0
+)
 
 require (
 	github.com/smithy-lang/smithy-dafny/TestModels/Dependencies v0.0.0
@@ -19,9 +20,6 @@ require (
 
 replace github.com/smithy-lang/smithy-dafny/TestModels/Dependencies 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/TestModels/Constraints v0.0.0 => ../../../../Constraints/runtimes/go/ImplementationFromDafny-go

TestModels/Errors/runtimes/go/ImplementationFromDafny-go/go.mod

@@ -2,11 +2,9 @@ module github.com/smithy-lang/smithy-dafny/TestModels/Errors
 
 go 1.23.0
 
-require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
-
-require github.com/dafny-lang/DafnyRuntimeGo v0.0.0
-
-//TODO: Drop this after Dafny fixes the https://t.corp.amazon.com/P150784381
-replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../DafnyRuntimeGo/
+require (
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
+	github.com/dafny-lang/DafnyStandardLibGo v0.0.0
+)
 
 replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/

TestModels/Errors/runtimes/go/TestsFromDafny-go/go.mod

@@ -5,7 +5,7 @@ go 1.23.0
 require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
 
 require (
-	github.com/dafny-lang/DafnyRuntimeGo v0.0.0
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
 	github.com/smithy-lang/smithy-dafny/TestModels/Errors v0.0.0
 )
 

TestModels/Extendable/runtimes/go/ImplementationFromDafny-go/go.mod

@@ -2,11 +2,9 @@ module github.com/smithy-lang/smithy-dafny/TestModels/Extendable
 
 go 1.23.0
 
-require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
-
-require github.com/dafny-lang/DafnyRuntimeGo v0.0.0
-
-//TODO: Drop this after Dafny fixes the https://t.corp.amazon.com/P150784381
-replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../DafnyRuntimeGo/
+require (
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
+	github.com/dafny-lang/DafnyStandardLibGo v0.0.0
+)
 
 replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/

TestModels/Extendable/runtimes/go/TestsFromDafny-go/NativeResourceFactory/extern.go

@@ -1,7 +1,7 @@
 package NativeResourceFactory
 
 import (
-	"github.com/dafny-lang/DafnyRuntimeGo/dafny"
+	"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
 	ExtendableResource "github.com/smithy-lang/smithy-dafny/TestModels/Extendable/ExtendableResource"
 	SimpleExtendableResourcesTypes "github.com/smithy-lang/smithy-dafny/TestModels/Extendable/SimpleExtendableResourcesTypes"
 	"github.com/smithy-lang/smithy-dafny/TestModels/Extendable/test/simpleextendableresourcessmithygenerated"

TestModels/Extendable/runtimes/go/TestsFromDafny-go/go.mod

@@ -5,13 +5,10 @@ go 1.23.0
 require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
 
 require (
-	github.com/dafny-lang/DafnyRuntimeGo v0.0.0
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
 	github.com/smithy-lang/smithy-dafny/TestModels/Extendable v0.0.0
 )
 
 replace github.com/smithy-lang/smithy-dafny/TestModels/Extendable 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/

TestModels/Extern/runtimes/go/ExternConstructor/ExternConstructor.go → TestModels/Extern/runtimes/go/ImplementationFromDafny-go/ExternConstructor/extern.go

@@ -3,10 +3,9 @@ package ExternConstructor
 import (
 	"fmt"
 
-	"github.com/Smithy-dafny/TestModels/Extern/simpledafnyexterninternaldafnytypes"
-	"github.com/Smithy-dafny/TestModels/Extern/simpledafnyexterntypes"
-	"github.com/dafny-lang/DafnyRuntimeGo/dafny"
+	"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
 	"github.com/dafny-lang/DafnyStandardLibGo/Wrappers"
+	"github.com/smithy-lang/smithy-dafny/TestModels/Extern/SimpleDafnyExternTypes"
 )
 
 type ExternConstructorClass struct {
@@ -25,9 +24,9 @@ var Companion_ExternConstructorClass_ = CompanionStruct_ExternConstructorClass_{
 func (CompanionStruct_ExternConstructorClass_) Build(input dafny.Sequence) Wrappers.Result {
 	if input.Equals(dafny.SeqOfChars([]dafny.Char("Error")...)) {
 		return Wrappers.Companion_Result_.Create_Failure_(
-			simpledafnyexterninternaldafnytypes.Companion_Error_.Create_Opaque_(simpledafnyexterntypes.OpaqueError{
-				ErrObject: fmt.Errorf("Exception"),
-			}))
+			SimpleDafnyExternTypes.Companion_Error_.Create_Opaque_(
+				fmt.Errorf("Exception"), dafny.SeqOfChars([]dafny.Char("ExceptionMessage")...)),
+		)
 	}
 	return Wrappers.Companion_Result_.Create_Success_(&ExternConstructorClass{func() *string {
 		var s string

TestModels/Extern/runtimes/go/ImplementationFromDafny-go/SimpleExternImpl/extern.go

@@ -0,0 +1,21 @@
+package SimpleExternImpl
+
+import (
+	"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
+	"github.com/dafny-lang/DafnyStandardLibGo/Wrappers"
+	"github.com/smithy-lang/smithy-dafny/TestModels/Extern/SimpleDafnyExternTypes"
+)
+
+func (CompanionStruct_Default___) GetExtern(c Config, input SimpleDafnyExternTypes.GetExternInput) Wrappers.Result {
+	return Wrappers.Companion_Result_.Create_Success_(SimpleDafnyExternTypes.Companion_GetExternOutput_.Create_GetExternOutput_(input.Dtor_blobValue(),
+		input.Dtor_booleanValue(),
+		input.Dtor_stringValue(),
+		input.Dtor_integerValue(),
+		input.Dtor_longValue()))
+
+}
+func (CompanionStruct_Default___) ExternMustError(c Config, input SimpleDafnyExternTypes.ExternMustErrorInput) Wrappers.Result {
+	return Wrappers.Companion_Result_.Create_Failure_(
+		SimpleDafnyExternTypes.Companion_Error_.Create_Opaque_(
+			input.Dtor_value(), dafny.SeqOfChars([]dafny.Char("ExceptionMessage")...)))
+}

TestModels/Extern/runtimes/go/ImplementationFromDafny-go/go.mod

@@ -2,11 +2,9 @@ module github.com/smithy-lang/smithy-dafny/TestModels/Extern
 
 go 1.23.0
 
-require github.com/dafny-lang/DafnyStandardLibGo v0.0.0
-
-require github.com/dafny-lang/DafnyRuntimeGo v0.0.0
-
-//TODO: Drop this after Dafny fixes the https://t.corp.amazon.com/P150784381
-replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../DafnyRuntimeGo/
+require (
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.8.0
+	github.com/dafny-lang/DafnyStandardLibGo v0.0.0
+)
 
 replace github.com/dafny-lang/DafnyStandardLibGo => ../../../../dafny-dependencies/StandardLibrary/runtimes/go/ImplementationFromDafny-go/