fix: resolve post-merge bugs from #1716 and #1717

.github/actions/setup-foundry/action.yml

@@ -36,6 +36,15 @@ runs:
         cp -a "${source_dir}/." "${out_dir}/"
         rm -f "${out_dir}/.ready"
 
+        # Validate that .yul files were actually restored
+        shopt -s nullglob
+        restored_yul=("${out_dir}"/*.yul)
+        if [ "${#restored_yul[@]}" -eq 0 ]; then
+          echo "::warning::Local Yul cache had .ready sentinel but no .yul files — falling back to artifact download"
+          exit 1
+        fi
+        echo "Restored ${#restored_yul[@]} Yul files from local cache"
+
     - name: Download generated Yul
       if: inputs.download-yul == 'true' && steps.local-restore-yul.outcome != 'success'
       uses: actions/download-artifact@v7
@@ -84,6 +93,13 @@ runs:
         cp -a "${source_dir}/." .lake/build/bin/
         rm -f .lake/build/bin/.ready
 
+        # Validate that the interpreter binary was actually restored
+        if [ ! -f .lake/build/bin/difftest-interpreter ]; then
+          echo "::warning::Local difftest cache had .ready sentinel but no binary — falling back to artifact download"
+          exit 1
+        fi
+        echo "Restored difftest-interpreter from local cache"
+
     - name: Download difftest interpreter
       if: steps.local-restore-difftest.outcome != 'success'
       uses: actions/download-artifact@v7

.github/workflows/verify.yml

@@ -755,6 +755,27 @@ jobs:
             --module Contracts.LocalObligationMacroSmoke.LocalObligationMacroSmoke \
             --output compiler/yul >/dev/null
 
+      - name: Pre-build smoke test Yul artifacts (unpatched)
+        run: |
+          set -euo pipefail
+          smoke_modules=(
+            Contracts.BytesEqSmoke
+            Contracts.Smoke.LowLevelTryCatchSmoke
+            Contracts.StringArrayErrorSmoke
+            Contracts.StringArrayEventSmoke
+            Contracts.StringEqSmoke
+            Contracts.StringErrorSmokeContract
+            Contracts.StringEventSmoke
+            Contracts.StringSmoke
+          )
+          lake build "${smoke_modules[@]}" >/dev/null
+          mkdir -p compiler/yul-smoke
+          for module in "${smoke_modules[@]}"; do
+            ./compiler/bin/verity-compiler \
+              --module "$module" \
+              --output compiler/yul-smoke >/dev/null
+          done
+
       - name: Generate patched Yul + patch coverage report
         run: |
           ./compiler/bin/verity-compiler-patched \
@@ -772,12 +793,32 @@ jobs:
           if [ -f "${artifact}" ]; then
             exit 0
           fi
-          lake build Contracts.LocalObligationMacroSmoke.LocalObligationMacroSmoke >/dev/null
           ./compiler/bin/verity-compiler-patched \
             --module Contracts.LocalObligationMacroSmoke.LocalObligationMacroSmoke \
             --output compiler/yul-patched \
             --enable-patches >/dev/null
 
+      - name: Pre-build patched smoke test Yul artifacts for foundry-patched
+        run: |
+          set -euo pipefail
+          smoke_modules=(
+            Contracts.BytesEqSmoke
+            Contracts.Smoke.LowLevelTryCatchSmoke
+            Contracts.StringArrayErrorSmoke
+            Contracts.StringArrayEventSmoke
+            Contracts.StringEqSmoke
+            Contracts.StringErrorSmokeContract
+            Contracts.StringEventSmoke
+            Contracts.StringSmoke
+          )
+          mkdir -p compiler/yul-patched-smoke
+          for module in "${smoke_modules[@]}"; do
+            ./compiler/bin/verity-compiler-patched \
+              --module "$module" \
+              --output compiler/yul-patched-smoke \
+              --enable-patches >/dev/null
+          done
+
       - name: Save static gas report snapshot
         run: lake exe gas-report --manifest packages/verity-examples/contracts.manifest > gas-report-static.tsv
 
@@ -825,6 +866,20 @@ jobs:
             --name generated-yul-patched \
             --path compiler/yul-patched
 
+      - name: Publish smoke Yul locally
+        run: |
+          scripts/ci_local_persistence.sh publish \
+            --run-id "${{ github.run_id }}" \
+            --name generated-yul-smoke \
+            --path compiler/yul-smoke
+
+      - name: Publish patched smoke Yul locally
+        run: |
+          scripts/ci_local_persistence.sh publish \
+            --run-id "${{ github.run_id }}" \
+            --name generated-yul-patched-smoke \
+            --path compiler/yul-patched-smoke
+
       - name: Publish gas reports locally
         run: |
           staging="${RUNNER_TEMP}/gas-reports-${{ github.run_id }}"
@@ -838,50 +893,72 @@ jobs:
             --path "$staging"
 
       - name: Upload difftest interpreter
+        if: '!cancelled()'
         uses: actions/upload-artifact@v7
         with:
           name: difftest-interpreter
           path: .lake/build/bin/difftest-interpreter
 
       - name: Upload compiler binaries
+        if: '!cancelled()'
         uses: actions/upload-artifact@v7
         with:
           name: verity-compiler-binaries
           path: compiler/bin
           compression-level: 0
 
       - name: Upload compiler workspace build
+        if: '!cancelled()'
         uses: actions/upload-artifact@v7
         with:
           name: lean-workspace-compiler-build
           path: lean-workspace-compiler-build.tar
           compression-level: 0
 
       - name: Upload generated Yul
+        if: '!cancelled()'
         uses: actions/upload-artifact@v7
         with:
           name: generated-yul
           path: compiler/yul
 
       - name: Upload patched Yul
+        if: '!cancelled()'
         uses: actions/upload-artifact@v7
         with:
           name: generated-yul-patched
           path: compiler/yul-patched
 
+      - name: Upload smoke Yul
+        if: '!cancelled()'
+        uses: actions/upload-artifact@v7
+        with:
+          name: generated-yul-smoke
+          path: compiler/yul-smoke
+
+      - name: Upload patched smoke Yul
+        if: '!cancelled()'
+        uses: actions/upload-artifact@v7
+        with:
+          name: generated-yul-patched-smoke
+          path: compiler/yul-patched-smoke
+
       - name: Upload patch coverage report
+        if: '!cancelled()'
         uses: actions/upload-artifact@v7
         with:
           name: patch-coverage-report
           path: compiler/patch-report.tsv
 
       - name: Upload static gas report
+        if: '!cancelled()'
         uses: actions/upload-artifact@v7
         with:
           name: static-gas-report
           path: gas-report-static.tsv
 
       - name: Upload patched static gas report
+        if: '!cancelled()'
         uses: actions/upload-artifact@v7
         with:
           name: static-gas-report-patched
@@ -1149,11 +1226,38 @@ jobs:
         with:
           name: static-gas-report
 
+      - name: Verify Lake package integrity
+        run: |
+          shopt -s nullglob
+          for pkg_git in .lake/packages/*/.git; do
+            pkg="$(dirname "$pkg_git")"
+            if ! git -C "$pkg" rev-parse HEAD >/dev/null 2>&1; then
+              echo "::warning::Removing corrupted Lake package: $pkg"
+              rm -rf "$pkg"
+            fi
+          done
+
       - name: Setup Foundry environment
         uses: ./.github/actions/setup-foundry
         with:
           local-artifact-run-id: ${{ github.run_id }}
 
+      - name: Verify solc can compile Yul artifacts
+        run: |
+          echo "solc path: $(which solc)"
+          echo "solc version: $(solc --version 2>&1 | grep -i version)"
+          for yul in compiler/yul/*.yul; do
+            hex=$(solc --strict-assembly --bin "$yul" 2>/dev/null | grep -E '^[0-9a-fA-F]+$' | tail -n 1)
+            if [ -z "$hex" ]; then
+              echo "FAIL: solc produced no hex for $yul"
+              echo "--- solc stderr ---"
+              solc --strict-assembly --bin "$yul" 2>&1 || true
+              echo "---"
+              exit 1
+            fi
+            echo "OK: $yul (${#hex} hex chars)"
+          done
+
       - name: Check static-vs-foundry gas calibration
         env:
           FOUNDRY_PROFILE: difftest
@@ -1188,6 +1292,37 @@ jobs:
       - name: Restore compiler executable bits
         run: chmod +x compiler/bin/verity-compiler compiler/bin/verity-compiler-patched compiler/bin/difftest-interpreter
 
+      - name: Restore smoke Yul (local)
+        id: local-restore-yul-smoke
+        continue-on-error: true
+        run: |
+          source_dir="${VERIFY_LOCAL_ARTIFACT_ROOT}/${{ github.run_id }}/generated-yul-smoke"
+          if [ -f "$source_dir/.ready" ]; then
+            mkdir -p compiler/yul-smoke
+            cp -a "$source_dir/." compiler/yul-smoke/
+            rm -f compiler/yul-smoke/.ready
+          else
+            exit 1
+          fi
+
+      - name: Download smoke Yul (fallback)
+        if: steps.local-restore-yul-smoke.outcome != 'success'
+        uses: actions/download-artifact@v7
+        with:
+          name: generated-yul-smoke
+          path: compiler/yul-smoke
+
+      - name: Verify Lake package integrity
+        run: |
+          shopt -s nullglob
+          for pkg_git in .lake/packages/*/.git; do
+            pkg="$(dirname "$pkg_git")"
+            if ! git -C "$pkg" rev-parse HEAD >/dev/null 2>&1; then
+              echo "::warning::Removing corrupted Lake package: $pkg"
+              rm -rf "$pkg"
+            fi
+          done
+
       - name: Setup Foundry environment
         uses: ./.github/actions/setup-foundry
         with:
@@ -1232,6 +1367,37 @@ jobs:
       - name: Restore compiler workspace build
         run: tar -xf lean-workspace-compiler-build.tar
 
+      - name: Restore patched smoke Yul (local)
+        id: local-restore-yul-patched-smoke
+        continue-on-error: true
+        run: |
+          source_dir="${VERIFY_LOCAL_ARTIFACT_ROOT}/${{ github.run_id }}/generated-yul-patched-smoke"
+          if [ -f "$source_dir/.ready" ]; then
+            mkdir -p compiler/yul-patched-smoke
+            cp -a "$source_dir/." compiler/yul-patched-smoke/
+            rm -f compiler/yul-patched-smoke/.ready
+          else
+            exit 1
+          fi
+
+      - name: Download patched smoke Yul (fallback)
+        if: steps.local-restore-yul-patched-smoke.outcome != 'success'
+        uses: actions/download-artifact@v7
+        with:
+          name: generated-yul-patched-smoke
+          path: compiler/yul-patched-smoke
+
+      - name: Verify Lake package integrity
+        run: |
+          shopt -s nullglob
+          for pkg_git in .lake/packages/*/.git; do
+            pkg="$(dirname "$pkg_git")"
+            if ! git -C "$pkg" rev-parse HEAD >/dev/null 2>&1; then
+              echo "::warning::Removing corrupted Lake package: $pkg"
+              rm -rf "$pkg"
+            fi
+          done
+
       - name: Setup Foundry environment
         uses: ./.github/actions/setup-foundry
         with:
@@ -1276,6 +1442,37 @@ jobs:
       - name: Restore compiler executable bits
         run: chmod +x compiler/bin/verity-compiler compiler/bin/verity-compiler-patched compiler/bin/difftest-interpreter
 
+      - name: Restore smoke Yul (local)
+        id: local-restore-yul-smoke
+        continue-on-error: true
+        run: |
+          source_dir="${VERIFY_LOCAL_ARTIFACT_ROOT}/${{ github.run_id }}/generated-yul-smoke"
+          if [ -f "$source_dir/.ready" ]; then
+            mkdir -p compiler/yul-smoke
+            cp -a "$source_dir/." compiler/yul-smoke/
+            rm -f compiler/yul-smoke/.ready
+          else
+            exit 1
+          fi
+
+      - name: Download smoke Yul (fallback)
+        if: steps.local-restore-yul-smoke.outcome != 'success'
+        uses: actions/download-artifact@v7
+        with:
+          name: generated-yul-smoke
+          path: compiler/yul-smoke
+
+      - name: Verify Lake package integrity
+        run: |
+          shopt -s nullglob
+          for pkg_git in .lake/packages/*/.git; do
+            pkg="$(dirname "$pkg_git")"
+            if ! git -C "$pkg" rev-parse HEAD >/dev/null 2>&1; then
+              echo "::warning::Removing corrupted Lake package: $pkg"
+              rm -rf "$pkg"
+            fi
+          done
+
       - name: Setup Foundry environment
         uses: ./.github/actions/setup-foundry
         with:

Compiler/Keccak/SpongeProperties.lean

@@ -21,33 +21,21 @@ namespace KeccakEngine
 
 /-! ### Word-to-bytes size lemma -/
 
--- TODO: Prove that wordToBytesLE always produces exactly 8 bytes.
--- Proof strategy: unfold wordToBytesLE, it constructs a literal #[...] of 8 elements.
--- This should be provable by `rfl` or `simp [wordToBytesLE]` since the array literal
--- has a statically-known size.
 theorem wordToBytesLE_size (word : BitVec 64) :
     (wordToBytesLE word).size = 8 := by
-  sorry
+  simp [wordToBytesLE]
 
 /-! ### Squeeze output size lemma -/
 
--- TODO: Prove that squeeze256 always produces exactly 32 bytes.
--- Proof strategy: unfold squeeze256, it concatenates 4 × wordToBytesLE results.
--- Using wordToBytesLE_size (each is 8 bytes), 4 × 8 = 32.
--- May need Array.size_append lemmas from Lean's standard library.
 theorem squeeze256_size (state : Array (BitVec 64)) :
     (squeeze256 state).size = 32 := by
-  sorry
+  simp [squeeze256, ByteArray.size, Array.size_append, wordToBytesLE_size]
 
 /-! ### Full keccak256 output size -/
 
--- TODO: Prove that keccak256 always produces exactly 32 bytes.
--- Proof strategy: unfold keccak256 → keccak256_core → ... → squeeze256.
--- The sponge loop always ends with keccakF1600 → squeeze256, so the output
--- size is determined entirely by squeeze256_size.
 theorem keccak256_core_size (data : ByteArray) (variant : HashVariant) :
     (keccak256_core data variant).size = 32 := by
-  sorry
+  unfold keccak256_core; exact squeeze256_size _
 
 theorem keccak256_size (data : ByteArray) :
     (keccak256 data).size = 32 := by