ci: Use commit from Dafny feature branch for testing Rust support

.github/actions/build_dafny_from_source/action.yml

@@ -0,0 +1,55 @@
+#
+# This local action builds Dafny from source
+# rather than using the setup-dafny-action.
+# Currently it's only used to test Rust support
+# against a feature branch of Dafny.
+#
+
+name: "Build Dafny from source"
+description: "Drop-in replacement for setup-dafny-action that builds the given branch of Dafny from source"
+inputs:
+  dafny:
+    description: "The Dafny branch to use"
+    required: true
+    type: string
+runs:
+  using: "composite"
+  steps:
+    - name: Checkout Dafny
+      uses: actions/checkout@v4
+      with:
+        repository: dafny-lang/dafny
+        path: dafny
+        ref: ${{ inputs.dafny }}
+
+    - name: Load Z3
+      shell: bash
+      run: |
+        sudo apt-get install -qq libarchive-tools
+        mkdir -p dafny/Binaries/z3/bin
+        wget -qO- https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip | bsdtar -xf -
+        mv z3-4.12.1 dafny/Binaries/z3/bin/
+        chmod +x dafny/Binaries/z3/bin/z3-4.12.1
+        mkdir -p unzippedRelease/dafny/z3/bin
+        ln dafny/Binaries/z3/bin/z3-4.12.1 unzippedRelease/dafny/z3/bin/z3-4.12.1
+
+    - name: Setup dotnet
+      uses: actions/setup-dotnet@v4
+      with:
+        dotnet-version: 6.0.x
+
+    - name: Build Dafny
+      shell: bash
+      run: |
+        dotnet build dafny/Source/Dafny.sln
+
+    - name: Add dafny to PATH
+      shell: bash
+      run: |
+        echo ${{ github.workspace }}/dafny/Scripts >> $GITHUB_PATH
+
+    # Hard-coding this for now since it's a pain to extract from an arbitrary branch
+    - name: Export DAFNY_VERSION
+      shell: bash
+      run: |
+        echo "DAFNY_VERSION=4.7.0" >> $GITHUB_ENV

.github/workflows/pull.yml

@@ -47,10 +47,9 @@ jobs:
       fail-fast: false
       matrix:
         # Rust code generation is under development and depends on pending changes to the
-        # Dafny Rust code generation, so we only test on a relatively recent prerelease instead.
-        # This can be updated as needed when new features/fixes land in Dafny master.
+        # Dafny Rust code generation, so we test on a specific commit from the feat-rust feature branch instead.
         dafny-version:
-          - nightly-2024-05-14-8da3ddd
+          - 00fe7ff70d3858d67d69a2b897a65c7f9d209e0a
     uses: ./.github/workflows/test_models_rust_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}

.github/workflows/push.yml

@@ -49,10 +49,9 @@ jobs:
       fail-fast: false
       matrix:
         # Rust code generation is under development and depends on pending changes to the
-        # Dafny Rust code generation, so we only test on a relatively recent prerelease instead.
-        # This can be updated as needed when new features/fixes land in Dafny master.
+        # Dafny Rust code generation, so we test on a specific commit from the feat-rust feature branch instead.
         dafny-version:
-          - nightly-2024-05-14-8da3ddd
+          - 00fe7ff70d3858d67d69a2b897a65c7f9d209e0a
     uses: ./.github/workflows/test_models_rust_tests.yml
     with:
       dafny: ${{ matrix.dafny-version }}

.github/workflows/test_models_rust_tests.yml

@@ -69,16 +69,17 @@ jobs:
 
       - uses: actions/checkout@v3
 
-      - name: Setup Dafny
-        uses: dafny-lang/setup-dafny-action@v1.7.0
+      - name: Setup Dafny (build from source)
+        uses: ./.github/actions/build_dafny_from_source
         with:
-          dafny-version: ${{ inputs.dafny }}
+          dafny: ${{ inputs.dafny }}
 
       - name: Set up Rust
         uses: actions-rust-lang/setup-rust-toolchain@v1
         with:
           toolchain: "1.74.1"
           rustflags: ""
+          components: rustfmt
 
       - name: Generate Polymorph Dafny
         working-directory: ./${{ matrix.library }}

SmithyDafnyMakefile.mk

@@ -194,6 +194,7 @@ transpile_implementation:
 		-functionSyntax:3 \
 		-useRuntimeLib \
 		-out $(OUT) \
+		$(DAFNY_OPTIONS) \
 		$(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
 		$(TRANSPILE_DEPENDENCIES)
 
@@ -505,12 +506,18 @@ transpile_rust: | transpile_implementation_rust transpile_dependencies_rust
 transpile_implementation_rust: TARGET=rs
 transpile_implementation_rust: OUT=implementation_from_dafny
 transpile_implementation_rust: SRC_INDEX=$(RUST_SRC_INDEX)
+# The Dafny Rust code generator is not complete yet,
+# so we want to emit code even if there are unsupported features in the input.
+transpile_implementation_rust: DAFNY_OPTIONS=-emitUncompilableCode
 transpile_implementation_rust: _transpile_implementation_all _mv_implementation_rust
 
 transpile_test_rust: TARGET=rs
 transpile_test_rust: OUT=tests_from_dafny
 transpile_test_rust: SRC_INDEX=$(RUST_SRC_INDEX)
 transpile_test_rust: TEST_INDEX=$(RUST_TEST_INDEX)
+# The Dafny Rust code generator is not complete yet,
+# so we want to emit code even if there are unsupported features in the input.
+transpile_test_rust: DAFNY_OPTIONS=-emitUncompilableCode
 transpile_test_rust: _transpile_test_all _mv_test_rust
 
 transpile_dependencies_rust: LANG=rust
@@ -519,12 +526,16 @@ transpile_dependencies_rust: transpile_dependencies
 _mv_implementation_rust:
 	rm -rf runtimes/rust/dafny_impl/src
 	mkdir -p runtimes/rust/dafny_impl/src
-	mv implementation_from_dafny-rust/src/implementation_from_dafny.rs runtimes/rust/dafny_impl/src/implementation_from_dafny.rs
+# TODO: Currently need to insert an import of the the StandardLibrary.
+	python -c "import sys; data = sys.stdin.buffer.read(); sys.stdout.buffer.write(data.replace(b'\npub mod', b'\npub use dafny_standard_library::implementation_from_dafny::*;\n\npub mod', 1) if b'\npub mod' in data else data)" \
+	  < implementation_from_dafny-rust/src/implementation_from_dafny.rs > runtimes/rust/dafny_impl/src/implementation_from_dafny.rs
+	rustfmt runtimes/rust/dafny_impl/src/implementation_from_dafny.rs
 	rm -rf implementation_from_dafny-rust
 _mv_test_rust:
 	rm -rf runtimes/rust/dafny_impl/tests
 	mkdir -p runtimes/rust/dafny_impl/tests
 	mv tests_from_dafny-rust/src/tests_from_dafny.rs runtimes/rust/dafny_impl/tests/tests_from_dafny.rs
+	rustfmt runtimes/rust/dafny_impl/tests/tests_from_dafny.rs
 	rm -rf tests_from_dafny-rust
 
 build_rust:

TestModels/SharedMakefile.mk

@@ -65,5 +65,3 @@ _polymorph_dotnet: _polymorph
 _polymorph_dotnet: OUTPUT_DOTNET_WRAPPED=\
     $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/Wrapped/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/Wrapped)
 _polymorph_dotnet: _polymorph_wrapped
-
-

TestModels/SimpleTypes/SimpleBlob/Makefile

@@ -18,5 +18,3 @@ SMITHY_DEPS=dafny-dependencies/Model/traits.smithy
 
 # This project has no dependencies 
 # DEPENDENT-MODELS:= 
-
-RUST_SRC_INDEX=src_for_rust