(feat): Add Positional Trait in Go codegen

.github/workflows/manual.yml

@@ -32,3 +32,7 @@ jobs:
     uses: ./.github/workflows/test_models_python_tests.yml
     with:
       dafny: ${{ inputs.dafny }}
+  manual-ci-go:
+    uses: ./.github/workflows/test_models_go_tests.yml
+    with:
+      dafny: ${{ inputs.dafny }}

.github/workflows/nightly_dafny.yml

@@ -50,6 +50,7 @@ jobs:
         dafny-nightly-java,
         dafny-nightly-net,
         dafny-nightly-rust,
+        dafny-nightly-python,
       ]
     if: ${{ always() && contains(needs.*.result, 'failure') }}
     env:

.github/workflows/pull.yml

@@ -10,10 +10,10 @@ jobs:
     steps:
       - name: Populate Dafny versions list
         id: populate-dafny-versions-list
-        run: echo "dafny-versions-list=['4.2.0', '4.4.0']" >> $GITHUB_OUTPUT
+        run: echo "dafny-versions-list=['4.2.0', '4.4.0', '4.8.0']" >> $GITHUB_OUTPUT
       - name: Populate Dafny versions list for "only new versions" languages (Python)
         id: populate-only-new-dafny-versions-list
-        run: echo "only-new-dafny-versions-list=['4.7.0']" >> $GITHUB_OUTPUT
+        run: echo "only-new-dafny-versions-list=['4.8.0']" >> $GITHUB_OUTPUT
     outputs:
       dafny-version-list: ${{ steps.populate-dafny-versions-list.outputs.dafny-versions-list }}
       only-new-dafny-version-list: ${{ steps.populate-only-new-dafny-versions-list.outputs.only-new-dafny-versions-list }}
@@ -66,3 +66,28 @@ jobs:
     uses: ./.github/workflows/test_models_python_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}
+  pr-ci-go:
+    needs: pr-populate-dafny-versions
+    strategy:
+      fail-fast: false
+      matrix:
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.only-new-dafny-version-list) }}
+    uses: ./.github/workflows/test_models_go_tests.yml
+    with:
+      dafny: ${{ matrix.dafny-version }}
+
+  pr-ci-all-required:
+    if: always()
+    needs:
+      - pr-ci-verification
+      - pr-ci-java
+      - pr-ci-net
+      - pr-ci-rust
+      - pr-ci-python
+      - pr-ci-go
+    runs-on: ubuntu-latest
+    steps:
+      - name: Verify all required jobs passed
+        uses: re-actors/alls-green@release/v1
+        with:
+          jobs: ${{ toJSON(needs) }}

.github/workflows/push.yml

@@ -12,10 +12,10 @@ jobs:
     steps:
       - name: Populate Dafny versions list
         id: populate-dafny-versions-list
-        run: echo "dafny-versions-list=['4.2.0', '4.4.0']" >> $GITHUB_OUTPUT
+        run: echo "dafny-versions-list=['4.2.0', '4.4.0', '4.8.0']" >> $GITHUB_OUTPUT
       - name: Populate Dafny versions list for "only new versions" languages (Python)
         id: populate-only-new-dafny-versions-list
-        run: echo "only-new-dafny-versions-list=['4.7.0']" >> $GITHUB_OUTPUT
+        run: echo "only-new-dafny-versions-list=['4.8.0']" >> $GITHUB_OUTPUT
     outputs:
       dafny-version-list: ${{ steps.populate-dafny-versions-list.outputs.dafny-versions-list }}
       only-new-dafny-version-list: ${{ steps.populate-only-new-dafny-versions-list.outputs.only-new-dafny-versions-list }}
@@ -68,3 +68,12 @@ jobs:
     uses: ./.github/workflows/test_models_python_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}
+  push-ci-go:
+    needs: pr-populate-dafny-versions
+    strategy:
+      fail-fast: false
+      matrix:
+        dafny-version: ${{ fromJson(needs.pr-populate-dafny-versions.outputs.only-new-dafny-version-list) }}
+    uses: ./.github/workflows/test_models_go_tests.yml
+    with:
+      dafny: ${{ matrix.dafny-version }}

.github/workflows/test_models_go_tests.yml

@@ -1,79 +1,64 @@
 name: Library Go tests
 
-on: ["pull_request", "push"]
+on:
+  workflow_call:
+    inputs:
+      dafny:
+        description: "The Dafny version to run"
+        required: true
+        type: string
+      num_shards:
+        required: false
+        type: number
+        default: 5
 
 jobs:
-  test_go:
+  populate-matrix-dimensions:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Populate shard list
+        id: populate-shard-list
+        run: echo "shard-list=[`seq -s , 1 ${{ inputs.num_shards }}`]" >> $GITHUB_OUTPUT
+    outputs:
+      shard-list: ${{ steps.populate-shard-list.outputs.shard-list }}
+  testGo:
+    needs: populate-matrix-dimensions
     strategy:
-      fail-fast: false
+      fail-fast: false # at least for development; see all errors
       matrix:
-        library: [
-          # TestModels/dafny-dependencies/StandardLibrary, # This stores current Polymorph dependencies that all TestModels depend on
-          TestModels/Aggregate,
-          # TestModels/AggregateReferences,
-          TestModels/CodegenPatches,
-          TestModels/Constraints,
-          TestModels/Constructor,
-          TestModels/Dependencies,
-          TestModels/Errors,
-          TestModels/Extendable,
-          TestModels/Extern,
-          # TestModels/LanguageSpecificLogic,
-          # TestModels/LocalService,
-          # TestModels/MultipleModels,
-          TestModels/Refinement,
-          TestModels/Resource,
-          # TestModels/SimpleTypes/BigDecimal,
-          # TestModels/SimpleTypes/BigInteger,
-          TestModels/SimpleTypes/SimpleBlob,
-          TestModels/SimpleTypes/SimpleBoolean,
-          # TestModels/SimpleTypes/SimpleByte,
-          TestModels/SimpleTypes/SimpleDouble,
-          TestModels/SimpleTypes/SimpleEnum,
-          # TestModels/SimpleTypes/SimpleEnumV2,
-          # TestModels/SimpleTypes/SimpleFloat,
-          TestModels/SimpleTypes/SimpleInteger,
-          TestModels/SimpleTypes/SimpleLong,
-          # TestModels/SimpleTypes/SimpleShort,
-          TestModels/SimpleTypes/SimpleString,
-          # TestModels/SimpleTypes/SimpleTimestamp,
-          TestModels/Union,
-          # TestModels/aws-sdks/ddb,
-          TestModels/aws-sdks/kms
-        ]
-    runs-on: "macos-12"
+        shard: ${{ fromJson(needs.populate-matrix-dimensions.outputs.shard-list) }}
+    runs-on: "ubuntu-latest"
+    permissions:
+      id-token: write
+      contents: read
+    env:
+      DOTNET_CLI_TELEMETRY_OPTOUT: 1
+      DOTNET_NOLOGO: 1
     steps:
-      - uses: actions/checkout@v2
+      - name: Support longpaths on Git checkout
+        run: |
+          git config --global core.longpaths true
 
-      # - name: Setup Dafny 4.5.0
-      #   uses: dafny-lang/setup-dafny-action@v1.7.0
-      #   with:
-      #     dafny-version: 4.5.0
-      # TODO: Setup Dafny once its released
-      - name: Setup dotnet
-        uses: actions/setup-dotnet@v4
+      - name: Configure AWS Credentials
+        uses: aws-actions/configure-aws-credentials@v1
         with:
-          dotnet-version: 6.0.x
+          aws-region: us-west-2
+          role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-PolymorphTestModels-Role-us-west-2
+          role-session-name: PythonTests
 
-      - name: Build Dafny from source
-        run: |
-          git clone https://github.com/dafny-lang/dafny.git --recurse-submodules
-          cd dafny
-          make exe
-
-      - name: Install Z3 version 4.12.1
-        run: |
-          cd $GITHUB_WORKSPACE/dafny
-          make z3-mac
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
 
-      - name: Add Dafny to PATH
-        run: |
-          echo "$GITHUB_WORKSPACE/dafny/Scripts" >> $GITHUB_PATH
+      - name: Setup Dafny
+        uses: dafny-lang/setup-dafny-action@v1.7.0
+        with:
+          dafny-version: ${{ inputs.dafny }}
 
       - name: Install Go
         uses: actions/setup-go@v2
         with:
-          go-version: '1.21'
+          go-version: "1.21"
 
       - name: Install Go imports
         run: |
@@ -82,33 +67,36 @@ jobs:
       - name: Add go mod to Dafny Runtime Go
         shell: bash
         working-directory: ./DafnyRuntimeGo
-        run: | 
+        run: |
           go mod init github.com/dafny-lang/DafnyRuntimeGo
           go mod tidy
 
-      - name: polymorph dafny dependencies
-        shell: bash
-        working-directory: ./TestModels/dafny-dependencies/StandardLibrary
-        run: |
-          export DAFNY_VERSION=4.6
-          make polymorph_dafny
-          make transpile_go
-          make polymorph_go 
-          cd ./runtimes/go/ImplementationFromDafny-go/
-          go mod init github.com/dafny-lang/DafnyStandardLibGo
-          # TODO: This should handwritten (in the makefile or something)          
-          echo "replace github.com/dafny-lang/DafnyRuntimeGo => ../../../../../DafnyRuntimeGo/" >> go.mod;
+      - name: Setup Java 17 for codegen
+        uses: actions/setup-java@v3
+        with:
+          distribution: "corretto"
+          java-version: 17
 
-      - name: Generate Polymorph Dafny and Go code
-        shell: bash
-        working-directory: ./${{ matrix.library }}
-        run: |
-          export DAFNY_VERSION=4.6
-          make polymorph_dafny
-          sh ./removeDotFromExtern.sh
-          make transpile_go
-          make polymorph_go
+      - name: Setup smithy-dafny-conversion
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: publishToMavenLocal
+          build-root-directory: smithy-dafny-conversion
 
-          goimports -w runtimes/go/
-          cd runtimes/go/TestsFromDafny-go/
-          go run TestsFromDafny.go
+      - name: Install Smithy-Dafny codegen dependencies
+        uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
+
+      - name: Install smithy-dafny-codegen locally
+        uses: gradle/gradle-build-action@v2
+        with:
+          arguments: :smithy-dafny-codegen:pTML
+          build-root-directory: codegen
+
+      - name: Execute smithy-dafny-codegen-test tests
+        uses: gradle/gradle-build-action@v2
+        env:
+          JUNIT_SHARD: ${{ matrix.shard }}
+          JUNIT_SHARD_COUNT: ${{ inputs.num_shards }}
+        with:
+          arguments: :smithy-dafny-codegen-test:test --tests '*smithygo*' --info
+          build-root-directory: codegen

.github/workflows/test_models_rust_tests.yml

@@ -59,7 +59,7 @@ jobs:
       - name: Set up Rust
         uses: actions-rust-lang/setup-rust-toolchain@v1
         with:
-          toolchain: "1.76.0"
+          toolchain: "1.80.0"
           rustflags: ""
           components: rustfmt
 

SmithyDafnyMakefile.mk

@@ -434,7 +434,7 @@ _polymorph_dafny: OUTPUT_DAFNY=\
 		--output-dafny $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(LIBRARY_ROOT)/Model)
 _polymorph_dafny: INPUT_DAFNY=\
 		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
-_polymorph_dafny: _polymorph removeDots
+_polymorph_dafny: _polymorph
 
 # Generates dotnet code for all namespaces in this project
 .PHONY: polymorph_dotnet
@@ -767,6 +767,10 @@ clean_go:
 	rm -rf $(LIBRARY_ROOT)/runtimes/go/ImplementationFromDafny-go
 	rm -rf $(LIBRARY_ROOT)/runtimes/go/TestsFromDafny-go
 
+test_go:
+	cd runtimes/go/TestFromDafny-go
+	go run TestsFromDafny.go
+
 ########################## Python targets
 
 # Python MUST transpile dependencies first to generate .dtr files
@@ -862,9 +866,3 @@ local_transpile_test_single: TRANSPILE_DEPENDENCIES= \
 		$(patsubst %, -library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX)) \
 		-library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
 local_transpile_test_single: transpile_test
-
-removeDots:
-	chmod +x ./removeDotFromExtern.sh
-	./removeDotFromExtern.sh
-
-transpile_implementation_go: removeDots

TestModels/Aggregate/runtimes/rust/src/standard_library_externs.rs

@@ -0,0 +1,80 @@
+// Annotation to ignore the case of this module
+use crate::r#_Wrappers_Compile;
+use crate::UTF8;
+
+impl crate::UTF8::_default {
+    pub fn Encode(
+        s: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
+    ) -> ::std::rc::Rc<
+        r#_Wrappers_Compile::Result<
+            UTF8::ValidUTF8Bytes,
+            ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
+        >,
+    > {
+        let v = s.to_array();
+        let mut _accumulator: Vec<u8> = vec![];
+        // Use of .encode_utf8 method.
+        let mut surrogate: Option<u16> = None;
+        for c in v.iter() {
+            let s = if let Some(s) = surrogate {
+                String::from_utf16(&[s, c.0])
+            } else {
+                String::from_utf16(&[c.0])
+            };
+            surrogate = None;
+            match s {
+                Ok(value) => {
+                    _accumulator.extend(value.as_bytes());
+                    continue;
+                }
+                Err(e) => {
+                    if 0xD800 <= c.0 && c.0 <= 0xDFFF {
+                        surrogate = Some(c.0);
+                        continue;
+                    }
+                    return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<UTF8::ValidUTF8Bytes, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure {
+            error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(
+              &e.to_string())
+          });
+                }
+            }
+        }
+        if let Some(s) = surrogate {
+            return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<UTF8::ValidUTF8Bytes, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure {
+        error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(
+          &format!("Surrogate pair missing: 0x{:04x}", s))
+      });
+        }
+        ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<
+            UTF8::ValidUTF8Bytes,
+            ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
+        >::Success {
+            value: ::dafny_runtime::Sequence::from_array_owned(_accumulator),
+        })
+    }
+    pub fn Decode(
+        b: &::dafny_runtime::Sequence<u8>,
+    ) -> ::std::rc::Rc<
+        r#_Wrappers_Compile::Result<
+            ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
+            ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
+        >,
+    > {
+        let b = String::from_utf8(b.to_array().as_ref().clone());
+        match b {
+      Ok(s) => {
+        ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
+          ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Success {
+            value: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&s)
+        })
+      },
+      Err(e) => {
+        return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
+          ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure {
+            error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(
+              &e.to_string())
+          })
+      }
+    }
+    }
+}