Fix CI, csproj

.github/workflows/ci_examples_java.yml

@@ -62,6 +62,15 @@ jobs:
           # A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
           dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
+      - name: Regenerate code using smithy-dafny if necessary
+        if: ${{ github.event_name == 'schedule' || inputs.nightly }}
+        uses: ./.github/actions/polymorph_codegen
+        with:
+          dafny: ${{ env.DAFNY_VERSION }}
+          library: DynamoDbEncryption
+          diff-generated-code: false
+          update-and-regenerate-mpl: true
+
       - name: Build and locally deploy dependencies for examples
         shell: bash
         working-directory: ./DynamoDbEncryption

.github/workflows/ci_test_java.yml

@@ -59,7 +59,7 @@ jobs:
           dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
       - name: Regenerate code using smithy-dafny if necessary
-        if: ${{ inputs.nightly }}
+        if: ${{ github.event_name == 'schedule' || inputs.nightly }}
         uses: ./.github/actions/polymorph_codegen
         with:
           dafny: ${{ env.DAFNY_VERSION }}

.github/workflows/ci_test_net.yml

@@ -66,7 +66,7 @@ jobs:
           dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
       - name: Regenerate code using smithy-dafny if necessary
-        if: ${{ inputs.nightly }}
+        if: ${{ github.event_name == 'schedule' || inputs.nightly }}
         uses: ./.github/actions/polymorph_codegen
         with:
           dafny: ${{ env.DAFNY_VERSION }}

.github/workflows/ci_verification.yml

@@ -54,7 +54,7 @@ jobs:
           dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}
 
       - name: Regenerate code using smithy-dafny if necessary
-        if: ${{ inputs.nightly }}
+        if: ${{ github.event_name == 'schedule' || inputs.nightly }}
         uses: ./.github/actions/polymorph_codegen
         with:
           dafny: ${{ env.DAFNY_VERSION }}

DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj

@@ -31,11 +31,35 @@
     <NoWarn>CS0105,CS0618</NoWarn>
   </PropertyGroup>
 
+  <PropertyGroup>
+    <!-- This is somewhat brittle,
+         but having the value in a properties file
+         that can be shared is worth it.
+         See: https://learn.microsoft.com/en-us/visualstudio/msbuild/property-functions?view=vs-2022
+         for more details on property functions
+         
+         This takes a properties file (a=b)
+         1. Loads the file
+         2. Splits on `dafnyVersion=` and takes everything to the right of that
+           e.g. the version + any trailing data
+         3. Splits on newline and takes the second element.
+           This SHOULD be the value of `dafnyVersion` and not contain any trailing data
+     -->
+    <projectProperties>
+      $([System.IO.File]::ReadAllText('$(MSBuildProjectDirectory)/../../../project.properties'))
+    </projectProperties>
+    <dropBeforeDafnyVersionProperty>
+      $([System.Text.RegularExpressions.Regex]::Split("$(projectProperties)", "dafnyVersion=")[1])
+    </dropBeforeDafnyVersionProperty>
+    <DafnyVersion>
+      $([System.Text.RegularExpressions.Regex]::Split("$(dropBeforeDafnyVersionProperty)", "\n")[1])
+    </DafnyVersion>
+  </PropertyGroup>
 
   <ItemGroup>
     <PackageReference Include="AWSSDK.DynamoDBv2" Version="3.7.300.2"/>
     <PackageReference Include="AWSSDK.Core" Version="3.7.300.2"/>
-    <PackageReference Include="DafnyRuntime" Version="4.2.0" />
+    <PackageReference Include="DafnyRuntime" Version="$(DafnyVersion)" />
     <ProjectReference Include="../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj"/>
     <!--
               System.Collections.Immutable can be removed once dafny.msbuild is updated with