diff --git a/.github/actions/setup-foundry/action.yml b/.github/actions/setup-foundry/action.yml
index df00f75a2..00b308c97 100644
--- a/.github/actions/setup-foundry/action.yml
+++ b/.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
diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml
index 2509f3cd2..8bfaea8b4 100644
--- a/.github/workflows/verify.yml
+++ b/.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,12 +893,14 @@ 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
@@ -851,6 +908,7 @@ jobs:
           compression-level: 0
 
       - name: Upload compiler workspace build
+        if: '!cancelled()'
         uses: actions/upload-artifact@v7
         with:
           name: lean-workspace-compiler-build
@@ -858,30 +916,49 @@ jobs:
           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,64 @@ 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
+            shopt -s nullglob
+            restored_yul=(compiler/yul-smoke/*.yul)
+            if [ "${#restored_yul[@]}" -eq 0 ]; then
+              echo "::warning::Local smoke Yul cache had .ready but no .yul files — falling back"
+              exit 1
+            fi
+            echo "Restored ${#restored_yul[@]} smoke Yul files from local cache"
+          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: Validate smoke Yul artifacts
+        run: |
+          shopt -s nullglob
+          out_dir="compiler/yul-smoke"
+          direct_yul=("${out_dir}"/*.yul)
+          if [ "${#direct_yul[@]}" -eq 0 ]; then
+            mapfile -t nested_yul < <(find "${out_dir}" -mindepth 2 -maxdepth 3 -type f -name '*.yul' | sort)
+            if [ "${#nested_yul[@]}" -gt 0 ]; then
+              for path in "${nested_yul[@]}"; do
+                mv "$path" "${out_dir}/$(basename "$path")"
+              done
+            fi
+          fi
+          direct_yul=("${out_dir}"/*.yul)
+          if [ "${#direct_yul[@]}" -eq 0 ]; then
+            echo "::error::No smoke Yul files restored into ${out_dir}"
+            find "${out_dir}" -maxdepth 4 -print || true
+            exit 1
+          fi
+
+      - 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 +1394,64 @@ 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
+            shopt -s nullglob
+            restored_yul=(compiler/yul-patched-smoke/*.yul)
+            if [ "${#restored_yul[@]}" -eq 0 ]; then
+              echo "::warning::Local patched smoke Yul cache had .ready but no .yul files — falling back"
+              exit 1
+            fi
+            echo "Restored ${#restored_yul[@]} patched smoke Yul files from local cache"
+          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: Validate patched smoke Yul artifacts
+        run: |
+          shopt -s nullglob
+          out_dir="compiler/yul-patched-smoke"
+          direct_yul=("${out_dir}"/*.yul)
+          if [ "${#direct_yul[@]}" -eq 0 ]; then
+            mapfile -t nested_yul < <(find "${out_dir}" -mindepth 2 -maxdepth 3 -type f -name '*.yul' | sort)
+            if [ "${#nested_yul[@]}" -gt 0 ]; then
+              for path in "${nested_yul[@]}"; do
+                mv "$path" "${out_dir}/$(basename "$path")"
+              done
+            fi
+          fi
+          direct_yul=("${out_dir}"/*.yul)
+          if [ "${#direct_yul[@]}" -eq 0 ]; then
+            echo "::error::No patched smoke Yul files restored into ${out_dir}"
+            find "${out_dir}" -maxdepth 4 -print || true
+            exit 1
+          fi
+
+      - 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 +1496,64 @@ 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
+            shopt -s nullglob
+            restored_yul=(compiler/yul-smoke/*.yul)
+            if [ "${#restored_yul[@]}" -eq 0 ]; then
+              echo "::warning::Local smoke Yul cache had .ready but no .yul files — falling back"
+              exit 1
+            fi
+            echo "Restored ${#restored_yul[@]} smoke Yul files from local cache"
+          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: Validate smoke Yul artifacts
+        run: |
+          shopt -s nullglob
+          out_dir="compiler/yul-smoke"
+          direct_yul=("${out_dir}"/*.yul)
+          if [ "${#direct_yul[@]}" -eq 0 ]; then
+            mapfile -t nested_yul < <(find "${out_dir}" -mindepth 2 -maxdepth 3 -type f -name '*.yul' | sort)
+            if [ "${#nested_yul[@]}" -gt 0 ]; then
+              for path in "${nested_yul[@]}"; do
+                mv "$path" "${out_dir}/$(basename "$path")"
+              done
+            fi
+          fi
+          direct_yul=("${out_dir}"/*.yul)
+          if [ "${#direct_yul[@]}" -eq 0 ]; then
+            echo "::error::No smoke Yul files restored into ${out_dir}"
+            find "${out_dir}" -maxdepth 4 -print || true
+            exit 1
+          fi
+
+      - 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:
diff --git a/Compiler/Keccak/SpongeProperties.lean b/Compiler/Keccak/SpongeProperties.lean
index d2e56f2c3..4bf883217 100644
--- a/Compiler/Keccak/SpongeProperties.lean
+++ b/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
diff --git a/Compiler/Proofs/EventSemantics.lean b/Compiler/Proofs/EventSemantics.lean
new file mode 100644
index 000000000..f2c306cf3
--- /dev/null
+++ b/Compiler/Proofs/EventSemantics.lean
@@ -0,0 +1,91 @@
+import Verity.Core
+
+/-!
+# Event Emission Semantics
+
+Structural properties of the event subsystem used by the source-level
+interpreter. These lemmas support widening `SupportedBodyEffectInterface` to
+admit `Stmt.emit` into the proven fragment.
+
+## Key results
+
+- `encodeEvent_injective`: distinct events produce distinct encodings
+- `encodeEvents_append`: encoding distributes over append
+- `encodeEvents_length`: encoding preserves list length
+- Event-append monotonicity lemmas for the append-only event log
+-/
+
+namespace Compiler.Proofs.EventSemantics
+
+open Verity.Core
+
+/-! ### Event encoding properties -/
+
+/-- Events are encoded to lists of natural numbers. -/
+def encodeEvent (ev : Verity.Event) : List Nat :=
+  (ev.name.toList.map Char.toNat) ++
+    (0 :: (ev.args.map (fun arg => arg.val))) ++
+    (0 :: (ev.indexedArgs.map (fun arg => arg.val)))
+
+def encodeEvents (events : List Verity.Event) : List (List Nat) :=
+  events.map encodeEvent
+
+theorem encodeEvents_append (evs1 evs2 : List Verity.Event) :
+    encodeEvents (evs1 ++ evs2) = encodeEvents evs1 ++ encodeEvents evs2 := by
+  simp [encodeEvents, List.map_append]
+
+theorem encodeEvents_length (evs : List Verity.Event) :
+    (encodeEvents evs).length = evs.length := by
+  simp [encodeEvents]
+
+theorem encodeEvents_nil : encodeEvents [] = [] := rfl
+
+theorem encodeEvents_cons (ev : Verity.Event) (rest : List Verity.Event) :
+    encodeEvents (ev :: rest) = encodeEvent ev :: encodeEvents rest := rfl
+
+/-! ### Event log monotonicity
+
+The event log in `ContractState` is append-only. These lemmas capture the
+monotonicity invariant needed for proving event-preserving compilation. -/
+
+/-- Appending an event to the world preserves all previous events. -/
+theorem events_append_prefix (world : Verity.ContractState) (ev : Verity.Event) :
+    world.events <+: (world.events ++ [ev]) :=
+  List.prefix_append world.events [ev]
+
+/-- Appending events preserves the storage mapping. -/
+theorem events_update_preserves_storage (world : Verity.ContractState) (newEvents : List Verity.Event) :
+    ({ world with events := world.events ++ newEvents } : Verity.ContractState).storage = world.storage :=
+  rfl
+
+/-- Appending events preserves storage arrays. -/
+theorem events_update_preserves_storageArray (world : Verity.ContractState) (newEvents : List Verity.Event) (slot : Nat) :
+    ({ world with events := world.events ++ newEvents } : Verity.ContractState).storageArray slot = world.storageArray slot :=
+  rfl
+
+/-! ### Effect surface classification
+
+These lemmas establish which statement forms touch the unsupported effect
+surface. They will be needed when widening the effect surface gate. -/
+
+/-- An event emission step appends exactly one event and returns `.continue`. -/
+theorem emit_step_spec (world : Verity.ContractState) (ev : Verity.Event) :
+    ({ world with events := world.events ++ [ev] } : Verity.ContractState).events =
+      world.events ++ [ev] :=
+  rfl
+
+/-- Event append preserves transient storage. -/
+theorem events_update_preserves_transientStorage (world : Verity.ContractState)
+    (newEvents : List Verity.Event) :
+    ({ world with events := world.events ++ newEvents } : Verity.ContractState).transientStorage =
+      world.transientStorage :=
+  rfl
+
+/-- Event append preserves the sender field. -/
+theorem events_update_preserves_sender (world : Verity.ContractState)
+    (newEvents : List Verity.Event) :
+    ({ world with events := world.events ++ newEvents } : Verity.ContractState).sender =
+      world.sender :=
+  rfl
+
+end Compiler.Proofs.EventSemantics
diff --git a/Compiler/Proofs/HelperStepProofs.lean b/Compiler/Proofs/HelperStepProofs.lean
new file mode 100644
index 000000000..cf88fd83f
--- /dev/null
+++ b/Compiler/Proofs/HelperStepProofs.lean
@@ -0,0 +1,188 @@
+import Compiler.Proofs.IRGeneration.GenericInduction
+import Compiler.Proofs.IRGeneration.SourceSemantics
+
+/-!
+# Helper Step Interface Proofs (Phase 1)
+
+This module provides the infrastructure for constructing
+`CompiledStmtStepWithHelpersAndHelperIR` witnesses for each of the four
+helper-surface statement families:
+
+1. Direct void helper calls (`Stmt.internalCall`)
+2. Direct helper call with return binding (`Stmt.internalCallAssign`)
+3. Expression-position helper calls (expr containing `Expr.internalCall`)
+4. Structural helper transport (`Stmt.ite` / `Stmt.forEach` with helpers)
+
+## Architecture
+
+The four narrow step interfaces are already defined and assembled in
+`GenericInduction.lean`. The assembly chain is:
+
+```
+StmtListDirectInternalHelperCallStepInterface
+  + StmtListDirectInternalHelperAssignStepInterface
+  → StmtListDirectInternalHelperStepInterface
+    + StmtListExprInternalHelperStepInterface
+    + StmtListStructuralInternalHelperStepInterface
+    → StmtListInternalHelperSurfaceStepInterface
+      + StmtListResidualHelperSurfaceStepInterface
+      → StmtListHelperSurfaceStepInterface
+        + StmtListHelperFreeStepInterface
+        + StmtListHelperFreeCompiledCallsDisjoint
+        → StmtListGenericWithHelpersAndHelperIR
+```
+
+## Proof strategy for each interface
+
+### Direct void calls (`StmtListDirectInternalHelperCallStepInterface`)
+
+Target: `Stmt.internalCall calleeName args` where
+`stmtTouchesDirectInternalHelperCallSurface stmt = true`.
+
+1. **compileOk**: `compileStmt` produces a Yul call expression statement.
+2. **preserves**: Source `execStmtWithHelpers` dispatches to
+   `interpretInternalFunctionFuel`; IR `execIRStmtsWithInternals` dispatches
+   through `evalIRCallWithInternals`; bridge via summary postcondition.
+
+### Direct assign calls (`StmtListDirectInternalHelperAssignStepInterface`)
+
+Same as void calls plus return-value binding in source and Yul let-binding.
+
+### Expression-position helpers (`StmtListExprInternalHelperStepInterface`)
+
+Key: `InternalHelperSummaryPreservesWorldOnSuccess` ensures the helper
+doesn't modify world state on success.
+
+### Structural transport (`StmtListStructuralInternalHelperStepInterface`)
+
+For `Stmt.ite` / `Stmt.forEach`: inductive — each branch satisfies the
+list-level witness.
+-/
+
+namespace Compiler.Proofs.HelperStepProofs
+
+open Compiler
+open Compiler.CompilationModel
+open Compiler.Yul
+open Compiler.Proofs.IRGeneration
+
+/-- For helper-surface-closed statement lists, the four narrow helper-step
+interfaces are all trivially satisfied. This is the entry point for contracts
+that do not use internal helpers at all. -/
+theorem allHelperInterfacesSatisfied_of_helperSurfaceClosed
+    {runtimeContract : IRContract}
+    {spec : CompilationModel}
+    {fields : List Field}
+    {scope : List String}
+    {stmts : List Stmt}
+    (hsurface : stmtListTouchesUnsupportedHelperSurface stmts = false) :
+    StmtListDirectInternalHelperCallStepInterface runtimeContract spec fields scope stmts ∧
+    StmtListDirectInternalHelperAssignStepInterface runtimeContract spec fields scope stmts ∧
+    StmtListExprInternalHelperStepInterface runtimeContract spec fields scope stmts ∧
+    StmtListStructuralInternalHelperStepInterface runtimeContract spec fields scope stmts :=
+  ⟨stmtListDirectInternalHelperCallStepInterface_of_helperSurfaceClosed hsurface,
+   stmtListDirectInternalHelperAssignStepInterface_of_helperSurfaceClosed hsurface,
+   stmtListExprInternalHelperStepInterface_of_helperSurfaceClosed hsurface,
+   stmtListStructuralInternalHelperStepInterface_of_helperSurfaceClosed hsurface⟩
+
+/-- Full assembly from the four narrow interfaces plus helper-free and residual
+interfaces into the whole-statement-list-level witness. This is the top-level
+composition theorem that the function-level proof consumes. -/
+theorem fullHelperAwareListWitness_of_allInterfaces
+    {runtimeContract : IRContract}
+    {spec : CompilationModel}
+    {fields : List Field}
+    {scope : List String}
+    {stmts : List Stmt}
+    (hhelperFree : StmtListHelperFreeStepInterface fields scope stmts)
+    (hcall :
+      StmtListDirectInternalHelperCallStepInterface runtimeContract spec fields scope stmts)
+    (hassign :
+      StmtListDirectInternalHelperAssignStepInterface runtimeContract spec fields scope stmts)
+    (hexpr :
+      StmtListExprInternalHelperStepInterface runtimeContract spec fields scope stmts)
+    (hstruct :
+      StmtListStructuralInternalHelperStepInterface runtimeContract spec fields scope stmts)
+    (hresidual :
+      StmtListResidualHelperSurfaceStepInterface runtimeContract spec fields scope stmts)
+    (hlegacy : StmtListHelperFreeCompiledLegacyCompatible fields scope stmts)
+    (hnoInternalFunctions : runtimeContract.internalFunctions = []) :
+    StmtListGenericWithHelpersAndHelperIR runtimeContract spec fields scope stmts :=
+  stmtListGenericWithHelpersAndHelperIR_of_helperFreeStepInterface_and_directInternalHelperCallStepInterface_and_directInternalHelperAssignStepInterface_and_exprInternalHelperStepInterface_and_structuralInternalHelperStepInterface_and_residualHelperSurfaceStepInterface_and_helperFreeCompiledLegacyCompatible
+    hhelperFree hcall hassign hexpr hstruct hresidual hlegacy hnoInternalFunctions
+
+/-- Convenience alias: full assembly using the disjoint-calls variant (for
+contracts where the IR contract has internal functions but compiled IR calls
+are disjoint from the internal table). Unlike the legacy-compatible variant,
+this does not require `runtimeContract.internalFunctions = []`. -/
+theorem fullHelperAwareListWitness_of_allInterfaces_disjoint
+    {runtimeContract : IRContract}
+    {spec : CompilationModel}
+    {fields : List Field}
+    {scope : List String}
+    {stmts : List Stmt}
+    (hhelperFree : StmtListHelperFreeStepInterface fields scope stmts)
+    (hcall :
+      StmtListDirectInternalHelperCallStepInterface runtimeContract spec fields scope stmts)
+    (hassign :
+      StmtListDirectInternalHelperAssignStepInterface runtimeContract spec fields scope stmts)
+    (hexpr :
+      StmtListExprInternalHelperStepInterface runtimeContract spec fields scope stmts)
+    (hstruct :
+      StmtListStructuralInternalHelperStepInterface runtimeContract spec fields scope stmts)
+    (hresidual :
+      StmtListResidualHelperSurfaceStepInterface runtimeContract spec fields scope stmts)
+    (hdisjoint : StmtListHelperFreeCompiledCallsDisjoint runtimeContract fields scope stmts) :
+    StmtListGenericWithHelpersAndHelperIR runtimeContract spec fields scope stmts :=
+  stmtListGenericWithHelpersAndHelperIR_of_helperFreeStepInterface_and_helperSurfaceStepInterface_and_helperFreeCompiledCallsDisjoint
+    hhelperFree
+    (stmtListHelperSurfaceStepInterface_of_internalHelperSurfaceStepInterface_and_residualHelperSurfaceStepInterface
+      (stmtListInternalHelperSurfaceStepInterface_of_directInternalHelperStepInterface_and_exprInternalHelperStepInterface_and_structuralInternalHelperStepInterface
+        (stmtListDirectInternalHelperStepInterface_of_callStepInterface_and_assignStepInterface
+          hcall hassign)
+        hexpr hstruct)
+      hresidual)
+    hdisjoint
+
+/-- Fast-path for helper-free contracts: if the statement list doesn't touch
+the helper surface at all, all five interfaces are vacuously satisfied and we
+can go straight to the whole-list proof with just the helper-free step interface
+and legacy compatibility. -/
+theorem helperFreeContractWitness
+    {runtimeContract : IRContract}
+    {spec : CompilationModel}
+    {fields : List Field}
+    {scope : List String}
+    {stmts : List Stmt}
+    (hhelperFree : StmtListHelperFreeStepInterface fields scope stmts)
+    (hsurface : stmtListTouchesUnsupportedHelperSurface stmts = false)
+    (hlegacy : StmtListHelperFreeCompiledLegacyCompatible fields scope stmts)
+    (hnoInternalFunctions : runtimeContract.internalFunctions = []) :
+    StmtListGenericWithHelpersAndHelperIR runtimeContract spec fields scope stmts :=
+  let ⟨hcall, hassign, hexpr, hstruct⟩ :=
+    allHelperInterfacesSatisfied_of_helperSurfaceClosed hsurface
+  fullHelperAwareListWitness_of_allInterfaces
+    hhelperFree hcall hassign hexpr hstruct
+    (stmtListResidualHelperSurfaceStepInterface_of_helperSurfaceClosed hsurface)
+    hlegacy hnoInternalFunctions
+
+/-- Fast-path using disjoint-calls variant for helper-free contracts with
+non-empty internal function tables. -/
+theorem helperFreeContractWitness_disjoint
+    {runtimeContract : IRContract}
+    {spec : CompilationModel}
+    {fields : List Field}
+    {scope : List String}
+    {stmts : List Stmt}
+    (hhelperFree : StmtListHelperFreeStepInterface fields scope stmts)
+    (hsurface : stmtListTouchesUnsupportedHelperSurface stmts = false)
+    (hdisjoint : StmtListHelperFreeCompiledCallsDisjoint runtimeContract fields scope stmts) :
+    StmtListGenericWithHelpersAndHelperIR runtimeContract spec fields scope stmts :=
+  let ⟨hcall, hassign, hexpr, hstruct⟩ :=
+    allHelperInterfacesSatisfied_of_helperSurfaceClosed hsurface
+  fullHelperAwareListWitness_of_allInterfaces_disjoint
+    hhelperFree hcall hassign hexpr hstruct
+    (stmtListResidualHelperSurfaceStepInterface_of_helperSurfaceClosed hsurface)
+    hdisjoint
+
+end Compiler.Proofs.HelperStepProofs
diff --git a/Compiler/Proofs/KeccakBound.lean b/Compiler/Proofs/KeccakBound.lean
index b98196d1a..4999f4b51 100644
--- a/Compiler/Proofs/KeccakBound.lean
+++ b/Compiler/Proofs/KeccakBound.lean
@@ -24,30 +24,61 @@ solidityMappingSlot_lt_evmModulus : solidityMappingSlot baseSlot key < evmModulu
 
 namespace Compiler.Proofs
 
+/-! ### ByteArray.toList length -/
+
+set_option maxHeartbeats 400000 in
+private theorem ByteArray.toList.loop_length (ba : ByteArray) (i : Nat) (acc : List UInt8)
+    (hi : i ≤ ba.size) :
+    (ByteArray.toList.loop ba i acc).length = (ba.size - i) + acc.length := by
+  induction i, acc using ByteArray.toList.loop.induct ba with
+  | case1 i acc hlt ih =>
+    unfold ByteArray.toList.loop
+    simp [hlt]
+    rw [ih (Nat.le_of_lt_succ (by omega))]
+    simp [List.length_cons]
+    omega
+  | case2 i acc hge =>
+    unfold ByteArray.toList.loop
+    simp [show ¬(i < ba.size) from hge]
+    omega
+
+private theorem ByteArray.toList_length (ba : ByteArray) : ba.toList.length = ba.size := by
+  unfold ByteArray.toList
+  rw [ByteArray.toList.loop_length ba 0 [] (Nat.zero_le _)]
+  simp
+
 /-! ### ByteArray big-endian bound -/
 
--- TODO: Prove that fromByteArrayBigEndian of a ≤32-byte array is < 2^256.
---
--- Proof strategy options (pick the one that works with EVMYulLean's definitions):
---
--- Option A: If fromByteArrayBigEndian unfolds to a foldl over bytes with
---   positional weights, prove by induction: each byte contributes < 256 * 2^(8*pos),
---   and the sum of all 32 positions < 2^256.
---
--- Option B: If fromByteArrayBigEndian is opaque in EVMYulLean, look for an
---   existing lemma in EVMYulLean like `fromByteArrayBigEndian_lt` or similar.
---   Check: `grep -r "fromByteArrayBigEndian.*lt\|fromByteArrayBigEndian.*bound"
---           .lake/packages/evmyul/ --include="*.lean"`
---
--- Option C (fallback): If both A and B fail, use native_decide on concrete
---   test vectors to validate, then use @[implemented_by] pattern as described
---   in the PR description.
---
--- IMPORTANT: Run `lake build` after each option to verify. Do NOT use sorry
--- in the final version.
+private theorem fromBytes'_lt (bs : List UInt8) :
+    EvmYul.fromBytes' bs < 2 ^ (8 * bs.length) := by
+  induction bs with
+  | nil => simp [EvmYul.fromBytes']
+  | cons b bs ih =>
+    unfold EvmYul.fromBytes'
+    have hb := b.toFin.isLt
+    simp only [List.length_cons, Nat.mul_succ, Nat.add_comm, Nat.pow_add]
+    have hsub :=
+      Nat.add_le_of_le_sub
+        (Nat.one_le_pow _ _ (by decide))
+        (Nat.le_sub_one_of_lt ih)
+    linarith
+
+private theorem fromBytes'_lt_of_length_le (bs : List UInt8) (n : Nat)
+    (h : bs.length ≤ n) :
+    EvmYul.fromBytes' bs < 2 ^ (8 * n) := by
+  calc EvmYul.fromBytes' bs
+      < 2 ^ (8 * bs.length) := fromBytes'_lt bs
+    _ ≤ 2 ^ (8 * n) := Nat.pow_le_pow_right (by omega) (Nat.mul_le_mul_left 8 h)
+
 theorem fromByteArrayBigEndian_lt_of_size (ba : ByteArray)
     (h : ba.size ≤ 32) :
     EvmYul.fromByteArrayBigEndian ba < Compiler.Constants.evmModulus := by
-  sorry
+  unfold EvmYul.fromByteArrayBigEndian EvmYul.fromBytesBigEndian Compiler.Constants.evmModulus
+  simp only [Function.comp]
+  show EvmYul.fromBytes' ba.toList.reverse < 2 ^ (8 * 32)
+  apply fromBytes'_lt_of_length_le
+  simp only [List.length_reverse]
+  rw [ByteArray.toList_length]
+  exact h
 
 end Compiler.Proofs
diff --git a/Compiler/Proofs/MappingSlot.lean b/Compiler/Proofs/MappingSlot.lean
index 2c325f543..071d93490 100644
--- a/Compiler/Proofs/MappingSlot.lean
+++ b/Compiler/Proofs/MappingSlot.lean
@@ -48,11 +48,8 @@ private def solidityMappingSlot_ffi (baseSlot key : Nat) : Nat :=
 
     Uses the kernel-computable Keccak engine so proofs can reason about the output
     size (always 32 bytes → result < 2^256). The FFI version is registered via
-    `@[implemented_by]` for runtime performance.
-
-    TODO: Once proofs are complete, uncomment `@[implemented_by solidityMappingSlot_ffi]`
-    and benchmark. If build time is acceptable without it, remove `_ffi` entirely. -/
--- @[implemented_by solidityMappingSlot_ffi]
+    `@[implemented_by]` for runtime performance. -/
+@[implemented_by solidityMappingSlot_ffi]
 def solidityMappingSlot (baseSlot key : Nat) : Nat :=
   EvmYul.fromByteArrayBigEndian (KeccakEngine.keccak256 (abiEncodeMappingSlot baseSlot key))
 
@@ -149,8 +146,7 @@ theorem solidityMappingSlot_lt_evmModulus (baseSlot key : Nat) :
     solidityMappingSlot baseSlot key < Compiler.Constants.evmModulus := by
   unfold solidityMappingSlot
   exact fromByteArrayBigEndian_lt_of_size _ (by
-    rw [KeccakEngine.keccak256_size]
-    omega)
+    rw [KeccakEngine.keccak256_size])
 
 theorem abstractMappingSlot_lt_evmModulus (baseSlot key : Nat) :
     abstractMappingSlot baseSlot key < Compiler.Constants.evmModulus :=
diff --git a/Compiler/Proofs/StorageBounds.lean b/Compiler/Proofs/StorageBounds.lean
new file mode 100644
index 000000000..84f075243
--- /dev/null
+++ b/Compiler/Proofs/StorageBounds.lean
@@ -0,0 +1,119 @@
+import Verity.Core
+
+/-!
+# Storage Bounds Lemmas for Dynamic Arrays
+
+Standalone mathematical facts about dynamic array operations defined in
+`SourceSemantics.lean`. These lemmas support widening `SupportedBodyStateInterface`
+to admit `storageArrayLength` and `storageArrayElement` reads into the proven
+fragment.
+
+## Key results
+
+- `storageArray_element_val_lt`: each `Uint256` element has `.val < 2^256`
+- `storageArraySetAt_length`: `storageArraySetAt` preserves list length
+- `storageArrayDropLast_length`: `storageArrayDropLast?` decreases length by 1
+- `writeStorageArray_other_slot`: `writeStorageArray` is a frame-preserving update
+-/
+
+namespace Compiler.Proofs.StorageBounds
+
+open Verity.Core
+
+/-! ### Element bounds -/
+
+theorem storageArray_element_val_lt (elem : Uint256) :
+    elem.val < UINT256_MODULUS :=
+  elem.isLt
+
+theorem storageArray_element_bounded (arr : List Uint256) (i : Nat)
+    (hi : i < arr.length) :
+    arr[i].val < UINT256_MODULUS :=
+  arr[i].isLt
+
+/-! ### storageArraySetAt -/
+
+/-- Mirrors the private definition in `SourceSemantics.lean`. -/
+def storageArraySetAt : List Uint256 → Nat → Uint256 → Option (List Uint256)
+  | [], _, _ => none
+  | _ :: rest, 0, value => some (value :: rest)
+  | head :: rest, idx + 1, value => do
+      let updatedRest ← storageArraySetAt rest idx value
+      some (head :: updatedRest)
+
+theorem storageArraySetAt_length (arr : List Uint256) (idx : Nat) (val : Uint256)
+    (arr' : List Uint256) (h : storageArraySetAt arr idx val = some arr') :
+    arr'.length = arr.length := by
+  induction arr generalizing idx arr' with
+  | nil => simp [storageArraySetAt] at h
+  | cons head rest ih =>
+    cases idx with
+    | zero =>
+      simp [storageArraySetAt] at h
+      subst h; simp
+    | succ idx' =>
+      simp [storageArraySetAt, bind, Option.bind] at h
+      split at h
+      · simp at h
+      · rename_i updatedRest heq
+        simp at h; subst h
+        simp [ih idx' updatedRest heq]
+
+/-! ### storageArrayDropLast? -/
+
+/-- Mirrors the private definition in `SourceSemantics.lean`. -/
+def storageArrayDropLast? : List Uint256 → Option (List Uint256)
+  | [] => none
+  | [_] => some []
+  | head :: rest => do
+      let updatedRest ← storageArrayDropLast? rest
+      some (head :: updatedRest)
+
+theorem storageArrayDropLast_length (arr : List Uint256) (arr' : List Uint256)
+    (h : storageArrayDropLast? arr = some arr') :
+    arr'.length + 1 = arr.length := by
+  induction arr generalizing arr' with
+  | nil => simp [storageArrayDropLast?] at h
+  | cons head rest ih =>
+    match rest with
+    | [] => simp [storageArrayDropLast?] at h; subst h; simp
+    | r :: rs =>
+      simp [storageArrayDropLast?, bind, Option.bind] at h
+      split at h
+      · simp at h
+      · rename_i updatedRest heq
+        simp at h; subst h
+        have := ih updatedRest heq
+        simp_all [List.length_cons]
+
+/-! ### writeStorageArray frame lemma -/
+
+/-- Mirrors the private definition in `SourceSemantics.lean`. -/
+def writeStorageArray (world : Verity.ContractState) (slot : Nat)
+    (values : List Uint256) : Verity.ContractState :=
+  { world with
+    storageArray := fun s => if s == slot then values else world.storageArray s }
+
+theorem writeStorageArray_same_slot (world : Verity.ContractState) (slot : Nat)
+    (values : List Uint256) :
+    (writeStorageArray world slot values).storageArray slot = values := by
+  simp [writeStorageArray, BEq.beq]
+
+theorem writeStorageArray_other_slot (world : Verity.ContractState) (slot slot' : Nat)
+    (values : List Uint256) (h : slot' ≠ slot) :
+    (writeStorageArray world slot values).storageArray slot' = world.storageArray slot' := by
+  unfold writeStorageArray
+  simp
+  omega
+
+theorem writeStorageArray_storage_unchanged (world : Verity.ContractState) (slot : Nat)
+    (values : List Uint256) :
+    (writeStorageArray world slot values).storage = world.storage :=
+  rfl
+
+theorem writeStorageArray_events_unchanged (world : Verity.ContractState) (slot : Nat)
+    (values : List Uint256) :
+    (writeStorageArray world slot values).events = world.events :=
+  rfl
+
+end Compiler.Proofs.StorageBounds
diff --git a/PrintAxioms.lean b/PrintAxioms.lean
index e15500a93..a2a343917 100644
--- a/PrintAxioms.lean
+++ b/PrintAxioms.lean
@@ -32,6 +32,8 @@ import Verity.Proofs.Stdlib.MappingAutomation
 import Verity.Proofs.Stdlib.Math
 import Compiler.Proofs.ArithmeticProfile
 import Compiler.Proofs.EndToEnd
+import Compiler.Proofs.EventSemantics
+import Compiler.Proofs.HelperStepProofs
 import Compiler.Proofs.IRGeneration.Contract
 import Compiler.Proofs.IRGeneration.ContractFeatureTest
 import Compiler.Proofs.IRGeneration.Dispatch
@@ -44,6 +46,7 @@ import Compiler.Proofs.IRGeneration.SourceSemantics
 import Compiler.Proofs.IRGeneration.SupportedSpec
 import Compiler.Proofs.KeccakBound
 import Compiler.Proofs.MappingSlot
+import Compiler.Proofs.StorageBounds
 import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeLemmas
 import Compiler.Proofs.YulGeneration.Builtins
 import Compiler.Proofs.YulGeneration.Equivalence
@@ -671,6 +674,25 @@ import Compiler.Proofs.YulGeneration.Equivalence
 #print axioms Compiler.Proofs.EndToEnd.layers2_3_ir_matches_yul
 #print axioms Compiler.Proofs.EndToEnd.simpleStorage_endToEnd
 
+-- Compiler/Proofs/EventSemantics.lean
+#print axioms Compiler.Proofs.EventSemantics.encodeEvents_append
+#print axioms Compiler.Proofs.EventSemantics.encodeEvents_length
+#print axioms Compiler.Proofs.EventSemantics.encodeEvents_nil
+#print axioms Compiler.Proofs.EventSemantics.encodeEvents_cons
+#print axioms Compiler.Proofs.EventSemantics.events_append_prefix
+#print axioms Compiler.Proofs.EventSemantics.events_update_preserves_storage
+#print axioms Compiler.Proofs.EventSemantics.events_update_preserves_storageArray
+#print axioms Compiler.Proofs.EventSemantics.emit_step_spec
+#print axioms Compiler.Proofs.EventSemantics.events_update_preserves_transientStorage
+#print axioms Compiler.Proofs.EventSemantics.events_update_preserves_sender
+
+-- Compiler/Proofs/HelperStepProofs.lean
+#print axioms Compiler.Proofs.HelperStepProofs.allHelperInterfacesSatisfied_of_helperSurfaceClosed
+#print axioms Compiler.Proofs.HelperStepProofs.fullHelperAwareListWitness_of_allInterfaces
+#print axioms Compiler.Proofs.HelperStepProofs.fullHelperAwareListWitness_of_allInterfaces_disjoint
+#print axioms Compiler.Proofs.HelperStepProofs.helperFreeContractWitness
+#print axioms Compiler.Proofs.HelperStepProofs.helperFreeContractWitness_disjoint
+
 -- Compiler/Proofs/IRGeneration/Contract.lean
 -- #print axioms Compiler.Proofs.IRGeneration.Contract.pickUniqueFunctionByName_eq_ok_none_of_absent  -- private
 -- #print axioms Compiler.Proofs.IRGeneration.Contract.compiled_functions_forall₂_of_mapM_ok  -- private
@@ -1993,7 +2015,11 @@ import Compiler.Proofs.YulGeneration.Equivalence
 -- #print axioms Compiler.Proofs.IRGeneration.simpleStorage_noReceive  -- private
 
 -- Compiler/Proofs/KeccakBound.lean
--- #print axioms Compiler.Proofs.fromByteArrayBigEndian_lt_of_size  -- sorry'd
+-- #print axioms Compiler.Proofs.ByteArray.toList.loop_length  -- private
+-- #print axioms Compiler.Proofs.ByteArray.toList_length  -- private
+-- #print axioms Compiler.Proofs.fromBytes'_lt  -- private
+-- #print axioms Compiler.Proofs.fromBytes'_lt_of_length_le  -- private
+#print axioms Compiler.Proofs.fromByteArrayBigEndian_lt_of_size
 
 -- Compiler/Proofs/MappingSlot.lean
 #print axioms Compiler.Proofs.abstractMappingSlot_eq_solidity
@@ -2011,6 +2037,16 @@ import Compiler.Proofs.YulGeneration.Equivalence
 #print axioms Compiler.Proofs.solidityMappingSlot_add_lt_evmModulus
 #print axioms Compiler.Proofs.solidityMappingSlot_add_wordOffset_lt_evmModulus
 
+-- Compiler/Proofs/StorageBounds.lean
+#print axioms Compiler.Proofs.StorageBounds.storageArray_element_val_lt
+#print axioms Compiler.Proofs.StorageBounds.storageArray_element_bounded
+#print axioms Compiler.Proofs.StorageBounds.storageArraySetAt_length
+#print axioms Compiler.Proofs.StorageBounds.storageArrayDropLast_length
+#print axioms Compiler.Proofs.StorageBounds.writeStorageArray_same_slot
+#print axioms Compiler.Proofs.StorageBounds.writeStorageArray_other_slot
+#print axioms Compiler.Proofs.StorageBounds.writeStorageArray_storage_unchanged
+#print axioms Compiler.Proofs.StorageBounds.writeStorageArray_events_unchanged
+
 -- Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean
 -- #print axioms Compiler.Proofs.YulGeneration.Backends.word_lt_uint256_size  -- private
 -- #print axioms Compiler.Proofs.YulGeneration.Backends.verity_eval_add_normalized  -- private
@@ -2103,4 +2139,4 @@ import Compiler.Proofs.YulGeneration.Equivalence
 #print axioms Compiler.Proofs.YulGeneration.ir_yul_function_equiv_from_state_of_fuel_goal_and_adequacy
 #print axioms Compiler.Proofs.YulGeneration.ir_yul_function_equiv_from_state_of_stmt_equiv_and_adequacy
 #print axioms Compiler.Proofs.YulGeneration.ir_yul_function_equiv_from_state_of_stmt_equiv
--- Total: 1966 theorems/lemmas (1320 public, 645 private, 1 sorry'd)
+-- Total: 1993 theorems/lemmas (1344 public, 649 private, 0 sorry'd)
diff --git a/README.md b/README.md
index 087407361..566558aa4 100644
--- a/README.md
+++ b/README.md
@@ -119,7 +119,7 @@ EVM Bytecode
 | 2 | A generic whole-contract theorem exists for the current explicit supported fragment, and its function-level closure now runs by theorem rather than axiom. All Layer 2 proof scripts are fully proved (0 `sorry`); see [docs/VERIFICATION_STATUS.md](docs/VERIFICATION_STATUS.md). The theorem surface explicitly assumes normalized transaction-context fields. Follow-on work in [#1510](https://github.com/Th0rgal/verity/issues/1510) focuses on widening the fragment. | [Contract.lean](Compiler/Proofs/IRGeneration/Contract.lean) |
 | 3 | IR → Yul codegen is proved generically at the statement/function level, but the current full dispatch-preservation path still uses 1 documented bridge hypothesis; the checked contract-level theorem surface now makes dispatch-guard safety explicit for each selected function case | [Preservation.lean](Compiler/Proofs/YulGeneration/Preservation.lean) |
 
-There is currently 1 documented Lean axiom in total: the mapping-slot range axiom. Selector computation is now kernel-computable, Layer 2's former generic body-simulation axiom has been eliminated, and Layer 3 keeps its remaining dispatch bridge as an explicit theorem hypothesis rather than a Lean axiom. See [AXIOMS.md](AXIOMS.md).
+There are currently 0 documented Lean axioms. The former mapping-slot range axiom has been eliminated via the kernel-computable Keccak engine. Selector computation is kernel-computable, Layer 2's former generic body-simulation axiom has been eliminated, and Layer 3 keeps its remaining dispatch bridge as an explicit theorem hypothesis rather than a Lean axiom. See [AXIOMS.md](AXIOMS.md).
 
 Layer 1 is the frontend EDSL-to-`CompilationModel` bridge. The per-contract files in `Contracts/<Name>/Proofs/` prove human-readable contract specifications; they are not what "Layer 1" means in the compiler stack. Layer 2 now has a generic whole-contract theorem for the explicit supported fragment. The compiler proves Layer 2 preservation automatically — no manual per-contract bridge proofs are needed. Layers 2 and 3 (`CompilationModel → IR → Yul`) are verified with the current documented axioms and bridge boundaries; see [docs/VERIFICATION_STATUS.md](docs/VERIFICATION_STATUS.md), [docs/GENERIC_LAYER2_PLAN.md](docs/GENERIC_LAYER2_PLAN.md), and [AXIOMS.md](AXIOMS.md).
 
diff --git a/TRUST_ASSUMPTIONS.md b/TRUST_ASSUMPTIONS.md
index ec6aae864..01fb33568 100644
--- a/TRUST_ASSUMPTIONS.md
+++ b/TRUST_ASSUMPTIONS.md
@@ -16,7 +16,7 @@ Yul
 EVM Bytecode
 ```
 
-The repository currently has 0 `sorry` placeholders across the `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules that participate in the verified compiler stack. Layer 2 (Source → IR) and Layer 3 (IR → Yul) proof scripts are fully discharged, and it now has 1 documented Lean axiom. See [AXIOMS.md](AXIOMS.md) for the exact list and current elimination plan.
+The repository currently has 0 `sorry` placeholders across the `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules that participate in the verified compiler stack. Layer 2 (Source → IR) and Layer 3 (IR → Yul) proof scripts are fully discharged, and it now has 0 documented Lean axioms. See [AXIOMS.md](AXIOMS.md) for details.
 
 ## What's Verified
 
diff --git a/artifacts/verification_status.json b/artifacts/verification_status.json
index ecdada7cc..e401404aa 100644
--- a/artifacts/verification_status.json
+++ b/artifacts/verification_status.json
@@ -5,7 +5,7 @@
   },
   "proofs": {
     "axioms": 0,
-    "sorry": 4
+    "sorry": 0
   },
   "schema_version": 1,
   "tests": {
@@ -33,7 +33,7 @@
       "SimpleStorage": 20,
       "SimpleToken": 61
     },
-    "proven": 273,
+    "proven": 277,
     "stdlib": 0,
     "total": 277
   },
diff --git a/docs-site/content/index.mdx b/docs-site/content/index.mdx
index 1c94486d1..212825bd9 100644
--- a/docs-site/content/index.mdx
+++ b/docs-site/content/index.mdx
@@ -130,7 +130,7 @@ See [/verification](/verification) for the complete, always-current theorem list
 
 **What's `sorry`?** A placeholder in Lean that says "I'll prove this later." It's how incomplete proofs compile. This project currently has `sorry` placeholders in the Layer 2 (Source → IR) proof scripts, which are being repaired after a definition refactor. Layer 3 proofs and all contract-level specification proofs are fully discharged.
 
-**What are axioms?** Statements assumed true without proof. This project currently documents 1 Lean axiom: the mapping-slot range axiom in `Compiler/Proofs/MappingSlot.lean` (see [AXIOMS.md](https://github.com/Th0rgal/verity/blob/main/AXIOMS.md)). Selector hashing is now kernel-computable, the former generic Layer 2 body-simulation axiom has been eliminated, and the Layer 3 dispatch bridge is kept as an explicit theorem hypothesis rather than a Lean axiom.
+**What are axioms?** Statements assumed true without proof. This project currently has 0 documented Lean axioms. The former mapping-slot range axiom has been eliminated via the kernel-computable Keccak engine (see [AXIOMS.md](https://github.com/Th0rgal/verity/blob/main/AXIOMS.md)). Selector hashing is kernel-computable, the former generic Layer 2 body-simulation axiom has been eliminated, and the Layer 3 dispatch bridge is kept as an explicit theorem hypothesis rather than a Lean axiom.
 
 Example proof technique (simplified):
 ```lean
diff --git a/docs-site/public/llms.txt b/docs-site/public/llms.txt
index f5192b0bb..e31acddee 100644
--- a/docs-site/public/llms.txt
+++ b/docs-site/public/llms.txt
@@ -18,7 +18,7 @@ Lean 4 EDSL for writing smart contracts with machine-checked proofs. Three-layer
 - **Core Size**: 400 lines
 - **Verified Contracts**: SimpleStorage, Counter, Owned, SimpleToken, OwnedCounter, Ledger, SafeCounter, ReentrancyExample (+ CryptoHash as unverified linker demo)
 - **Theorems**: 273 across 10 categories, 273 fully proven; Layer 2 proof scripts contain `sorry` placeholders (being repaired after definition refactor)
-- **Axioms**: 1 documented Lean axiom (see AXIOMS.md) — the mapping-slot range axiom. Selector computation is now kernel-computable, Layer 2's former generic body-simulation axiom has been eliminated, and Layer 3 keeps an explicit dispatch bridge hypothesis rather than a Lean axiom.
+- **Axioms**: 0 documented Lean axioms (see AXIOMS.md). The former mapping-slot range axiom has been eliminated via the kernel-computable Keccak engine. Selector computation is kernel-computable, Layer 2's former generic body-simulation axiom has been eliminated, and Layer 3 keeps an explicit dispatch bridge hypothesis rather than a Lean axiom.
 - **Tests**: 478 Foundry tests, multi-seed differential testing (7 seeds), 8-shard parallel CI
 - **Build**: `lake build` verifies all proofs
 - **Repository**: https://github.com/Th0rgal/verity
@@ -126,7 +126,7 @@ Add `.md` to any URL for raw markdown (saves tokens).
 See TRUST_ASSUMPTIONS.md for full analysis. Key trust boundaries:
 - **Verified**: EDSL -> CompilationModel -> IR -> Yul
 - **Trusted**: Yul -> Bytecode (via solc, validated by 90,000+ differential tests)
-- **Axioms**: 1 documented Lean axiom, with soundness justification in AXIOMS.md
+- **Axioms**: 0 documented Lean axioms, with soundness justification in AXIOMS.md
 - **External**: Lean 4 kernel, EVM specification alignment
 
 ## Known Limitations
diff --git a/docs/VERIFICATION_STATUS.md b/docs/VERIFICATION_STATUS.md
index 549cd2ae4..9f1b6d074 100644
--- a/docs/VERIFICATION_STATUS.md
+++ b/docs/VERIFICATION_STATUS.md
@@ -156,10 +156,10 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co
 
 **Proof-Only Properties (22 exclusions)**: Internal proof machinery that cannot be tested in Foundry.
 
-4 `sorry` remaining across `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules.
+0 `sorry` remaining across `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules.
 1878 theorems/lemmas (1263 public, 615 private) verified by `lake build PrintAxioms`.
 
-1 documented Lean axiom remains (the mapping-slot range axiom). Selector computation is now kernel-computable, the Layer 2 body-simulation axiom has been eliminated, and the Layer 3 dispatch bridge is tracked as an explicit theorem hypothesis rather than a Lean axiom.
+0 documented Lean axioms remain. The former mapping-slot range axiom has been eliminated via the kernel-computable Keccak engine. Selector computation is kernel-computable, the Layer 2 body-simulation axiom has been eliminated, and the Layer 3 dispatch bridge is tracked as an explicit theorem hypothesis rather than a Lean axiom.
 
 ## Differential Testing
 
diff --git a/foundry.toml b/foundry.toml
index 1be45e384..433b9176b 100644
--- a/foundry.toml
+++ b/foundry.toml
@@ -15,7 +15,9 @@ fs_permissions = [
   { access = "read-write", path = "./artifacts" },
   { access = "read-write", path = "./artifacts/test-string-smoke" },
   { access = "read", path = "./compiler/yul" },
-  { access = "read", path = "./compiler/yul-patched" }
+  { access = "read", path = "./compiler/yul-patched" },
+  { access = "read", path = "./compiler/yul-smoke" },
+  { access = "read", path = "./compiler/yul-patched-smoke" }
 ]
 
 # Testing profile: enables FFI for vm.ffi() calls (solc compilation, difftest-interpreter).
diff --git a/scripts/check_layer2_boundary_sync.py b/scripts/check_layer2_boundary_sync.py
index 478956b26..c4f888e91 100644
--- a/scripts/check_layer2_boundary_sync.py
+++ b/scripts/check_layer2_boundary_sync.py
@@ -32,8 +32,8 @@ def normalize_ws(text: str) -> str:
 def expected_snippets() -> dict[str, list[str]]:
     return {
         "AXIOMS": [
-            "### 1. `solidityMappingSlot_lt_evmModulus`",
-            "- Active axioms: 1",
+            "### 1. `solidityMappingSlot_lt_evmModulus` (eliminated)",
+            "- Active axioms: 0",
         ],
         "COMPILER_PROOFS_README": [
             "`Compiler.Proofs.IRGeneration.Contract.compile_preserves_semantics`",
@@ -57,14 +57,14 @@ def expected_snippets() -> dict[str, list[str]]:
             "Layer 2: CompilationModel → IR        [GENERIC WHOLE-CONTRACT THEOREM]",
             "Layer 2 now has a generic whole-contract theorem for the explicit supported fragment.",
             "its function-level closure now runs by theorem rather than axiom",
-            "There is currently 1 documented Lean axiom in total: the mapping-slot range axiom.",
+            "There are currently 0 documented Lean axioms.",
             "Layer 3 keeps its remaining dispatch bridge as an explicit theorem hypothesis rather than a Lean axiom.",
         ],
         "TRUST_ASSUMPTIONS": [
             "Layer 2: SUPPORTED-FRAGMENT GENERIC THEOREM — CompilationModel → IR",
             "A generic whole-contract theorem is proved for the current supported `CompilationModel` fragment.",
             "former generic body-simulation axiom has been eliminated",
-            "it now has 1 documented Lean axiom",
+            "it now has 0 documented Lean axioms",
             "explicit theorem hypothesis rather than a Lean axiom",
         ],
         "DOCS_SITE_COMPILER": [
@@ -91,7 +91,7 @@ def expected_snippets() -> dict[str, list[str]]:
         ],
         "LLMS": [
             "generic whole-contract CompilationModel -> IR theorem for the supported fragment",
-            "1 documented Lean axiom",
+            "0 documented Lean axioms",
         ],
     }
 
@@ -106,6 +106,7 @@ def forbidden_snippets() -> dict[str, list[str]]:
             "### 2. `supported_function_body_correct_from_exact_state`",
             "supported_function_body_correct_from_exact_state",
             "- Active axioms: 3",
+            "- Active axioms: 1",
         ],
         "VERIFICATION_STATUS": [
             "## Layer 2: CompilationModel → IR — COMPLETE",
@@ -128,6 +129,7 @@ def forbidden_snippets() -> dict[str, list[str]]:
             "documented bridge axiom",
             "1 generic non-core Layer 2 axiom",
             "There are currently 4 documented Lean axioms in total",
+            "There is currently 1 documented Lean axiom in total",
         ],
         "TRUST_ASSUMPTIONS": [
             "FULLY VERIFIED — CompilationModel → IR",
@@ -138,6 +140,7 @@ def forbidden_snippets() -> dict[str, list[str]]:
             "2 documented axioms in [AXIOMS.md](AXIOMS.md): 1 selector axiom and 1 generic non-core Layer 2 axiom",
             "Layer 3: GENERIC SURFACE, 1 axiom — IR → Yul",
             "1 Layer 3 dispatch bridge axiom",
+            "it now has 1 documented Lean axiom",
         ],
         "DOCS_SITE_COMPILER": [
             "**Layer 2 framework proof**: `CompilationModel -> IR` preserves semantics.",
@@ -160,6 +163,7 @@ def forbidden_snippets() -> dict[str, list[str]]:
             "3 documented axioms",
             "4 documented axioms",
             "partial generic CompilationModel -> IR boundary",
+            "1 documented Lean axiom",
         ],
     }
 
diff --git a/scripts/check_lean_hygiene.py b/scripts/check_lean_hygiene.py
index f21c043b7..acc8a3774 100644
--- a/scripts/check_lean_hygiene.py
+++ b/scripts/check_lean_hygiene.py
@@ -64,7 +64,7 @@ def main() -> None:
         )
 
     # Check 3: Fixed sorry baseline after the merged proof-reduction pass.
-    expected_sorry = 4
+    expected_sorry = 0
     sorry_count = 0
     sorry_locations: list[str] = []
     for lean_file in ROOT.rglob("*.lean"):
diff --git a/scripts/test_check_axioms.py b/scripts/test_check_axioms.py
index dd87b318a..aa9c124aa 100644
--- a/scripts/test_check_axioms.py
+++ b/scripts/test_check_axioms.py
@@ -115,12 +115,12 @@ def test_parse_axiom_output(self) -> None:
 
     def test_classify_axioms_separates_forbidden_and_unexpected(self) -> None:
         axiom_map = {
-            "Foo.bar": ["propext", "solidityMappingSlot_lt_evmModulus", "mysteryAx"],
+            "Foo.bar": ["propext", "mysteryAx"],
             "Baz.qux": ["sorryAx"],
         }
         builtin, documented, forbidden, unexpected = check_axioms.classify_axioms(axiom_map)
         self.assertEqual(builtin, {"propext"})
-        self.assertEqual(documented, {"solidityMappingSlot_lt_evmModulus"})
+        self.assertEqual(documented, set())
         self.assertEqual(forbidden, {"sorryAx"})
         self.assertEqual(unexpected, {"mysteryAx": ["Foo.bar"]})
 
@@ -134,7 +134,7 @@ def test_run_report_check_passes_and_writes_output_file(self) -> None:
             try:
                 with redirect_stdout(stdout), redirect_stderr(stderr):
                     rc = check_axioms.run_report_check(
-                        "'Foo.bar' depends on axioms: [propext, solidityMappingSlot_lt_evmModulus]\n"
+                        "'Foo.bar' depends on axioms: [propext]\n"
                     )
             finally:
                 if old_output is None:
diff --git a/scripts/test_check_layer2_boundary_sync.py b/scripts/test_check_layer2_boundary_sync.py
index fa7f79290..c82133db7 100644
--- a/scripts/test_check_layer2_boundary_sync.py
+++ b/scripts/test_check_layer2_boundary_sync.py
@@ -60,7 +60,7 @@ def test_matching_docs_pass(self) -> None:
     def test_missing_required_snippet_fails(self) -> None:
         rc, output = self._run_check(use_expected=False, add_forbidden=False)
         self.assertEqual(rc, 1)
-        self.assertIn("missing `### 1. `solidityMappingSlot_lt_evmModulus``", output)
+        self.assertIn("missing `### 1. `solidityMappingSlot_lt_evmModulus` (eliminated)`", output)
 
     def test_forbidden_overclaim_fails(self) -> None:
         rc, output = self._run_check(use_expected=True, add_forbidden=True)
@@ -74,7 +74,7 @@ def test_detects_stale_axiom_count_language(self) -> None:
             target = root / check.TARGETS["ROOT_README"].relative_to(check.ROOT)
             target.write_text(
                 target.read_text(encoding="utf-8").replace(
-                    "There is currently 1 documented Lean axiom in total: the mapping-slot range axiom.",
+                    "There are currently 0 documented Lean axioms.",
                     "There are currently 2 documented Lean axioms in total: the selector axiom and 1 mapping-slot range axiom.",
                 ),
                 encoding="utf-8",
@@ -98,7 +98,7 @@ def test_detects_stale_axiom_count_language(self) -> None:
                 check.TARGETS = old_targets
 
         self.assertEqual(rc, 1)
-        self.assertIn("missing `There is currently 1 documented Lean axiom in total", output)
+        self.assertIn("missing `There are currently 0 documented Lean axioms.", output)
 
     def test_compiler_proofs_readme_stale_axiom_wording_is_forbidden(self) -> None:
         forbidden = check.forbidden_snippets()
diff --git a/scripts/verify_sync_spec.json b/scripts/verify_sync_spec.json
index b2d556f36..d715868f6 100644
--- a/scripts/verify_sync_spec.json
+++ b/scripts/verify_sync_spec.json
@@ -513,6 +513,22 @@
           "path": "compiler/yul-patched"
         }
       },
+      {
+        "name": "Upload smoke Yul",
+        "uses": "actions/upload-artifact@v7",
+        "with": {
+          "name": "generated-yul-smoke",
+          "path": "compiler/yul-smoke"
+        }
+      },
+      {
+        "name": "Upload patched smoke Yul",
+        "uses": "actions/upload-artifact@v7",
+        "with": {
+          "name": "generated-yul-patched-smoke",
+          "path": "compiler/yul-patched-smoke"
+        }
+      },
       {
         "name": "Upload patch coverage report",
         "uses": "actions/upload-artifact@v7",
@@ -852,6 +868,8 @@
       "lean-workspace-compiler-build",
       "generated-yul",
       "generated-yul-patched",
+      "generated-yul-smoke",
+      "generated-yul-patched-smoke",
       "patch-coverage-report",
       "static-gas-report",
       "static-gas-report-patched"
@@ -876,6 +894,8 @@
       "lean-workspace-compiler-build.tar",
       "compiler/yul",
       "compiler/yul-patched",
+      "compiler/yul-smoke",
+      "compiler/yul-patched-smoke",
       "compiler/patch-report.tsv",
       "gas-report-static.tsv",
       "gas-report-static-patched.tsv"
@@ -915,14 +935,17 @@
       "static-gas-report"
     ],
     "foundry": [
-      "verity-compiler-binaries"
+      "verity-compiler-binaries",
+      "generated-yul-smoke"
     ],
     "foundry-patched": [
       "lean-workspace-build",
-      "lean-workspace-compiler-build"
+      "lean-workspace-compiler-build",
+      "generated-yul-patched-smoke"
     ],
     "foundry-multi-seed": [
-      "verity-compiler-binaries"
+      "verity-compiler-binaries",
+      "generated-yul-smoke"
     ]
   },
   "expected_downloaded_artifact_paths": {
@@ -956,14 +979,17 @@
       null
     ],
     "foundry": [
-      "compiler/bin"
+      "compiler/bin",
+      "compiler/yul-smoke"
     ],
     "foundry-patched": [
       null,
-      null
+      null,
+      "compiler/yul-patched-smoke"
     ],
     "foundry-multi-seed": [
-      "compiler/bin"
+      "compiler/bin",
+      "compiler/yul-smoke"
     ]
   }
 }
diff --git a/scripts/verify_sync_spec_source.py b/scripts/verify_sync_spec_source.py
index b1597c03e..d99c88853 100644
--- a/scripts/verify_sync_spec_source.py
+++ b/scripts/verify_sync_spec_source.py
@@ -869,6 +869,8 @@
     {'name': 'Upload compiler workspace build', 'uses': 'actions/upload-artifact@v7', 'with': {'name': 'lean-workspace-compiler-build', 'path': 'lean-workspace-compiler-build.tar', 'compression-level': '0'}},
     {'name': 'Upload generated Yul', 'uses': 'actions/upload-artifact@v7', 'with': {'name': 'generated-yul', 'path': 'compiler/yul'}},
     {'name': 'Upload patched Yul', 'uses': 'actions/upload-artifact@v7', 'with': {'name': 'generated-yul-patched', 'path': 'compiler/yul-patched'}},
+    {'name': 'Upload smoke Yul', 'uses': 'actions/upload-artifact@v7', 'with': {'name': 'generated-yul-smoke', 'path': 'compiler/yul-smoke'}},
+    {'name': 'Upload patched smoke Yul', 'uses': 'actions/upload-artifact@v7', 'with': {'name': 'generated-yul-patched-smoke', 'path': 'compiler/yul-patched-smoke'}},
     {'name': 'Upload patch coverage report', 'uses': 'actions/upload-artifact@v7', 'with': {'name': 'patch-coverage-report', 'path': 'compiler/patch-report.tsv'}},
     {'name': 'Upload static gas report', 'uses': 'actions/upload-artifact@v7', 'with': {'name': 'static-gas-report', 'path': 'gas-report-static.tsv'}},
     {'name': 'Upload patched static gas report', 'uses': 'actions/upload-artifact@v7', 'with': {'name': 'static-gas-report-patched', 'path': 'gas-report-static-patched.tsv'}},
@@ -879,7 +881,9 @@
     'prepare-macro-fuzz': ['lean-workspace-macro-fuzz-build'],
     'build-audits': ['axiom-dependency-report'],
     'build-compiler-binaries': ['difftest-interpreter', 'verity-compiler-binaries', 'lean-workspace-compiler-build',
-                                'generated-yul', 'generated-yul-patched', 'patch-coverage-report',
+                                'generated-yul', 'generated-yul-patched',
+                                'generated-yul-smoke', 'generated-yul-patched-smoke',
+                                'patch-coverage-report',
                                 'static-gas-report', 'static-gas-report-patched'],
     'lean-profile': ['lean-perf-queue'],
 }
@@ -889,7 +893,9 @@
     'prepare-macro-fuzz': ['lean-workspace-macro-fuzz-build.tar'],
     'build-audits': ['axiom-report.md\naxiom-report-raw.log'],
     'build-compiler-binaries': ['.lake/build/bin/difftest-interpreter', 'compiler/bin', 'lean-workspace-compiler-build.tar',
-                                'compiler/yul', 'compiler/yul-patched', 'compiler/patch-report.tsv',
+                                'compiler/yul', 'compiler/yul-patched',
+                                'compiler/yul-smoke', 'compiler/yul-patched-smoke',
+                                'compiler/patch-report.tsv',
                                 'gas-report-static.tsv', 'gas-report-static-patched.tsv'],
     'lean-profile': ['lean-perf-queue.md'],
 }
@@ -902,9 +908,9 @@
     'compiler-audits': ['lean-workspace-build', 'lean-workspace-compiler-build', 'generated-yul', 'generated-yul-patched', 'static-gas-report', 'static-gas-report-patched', 'patch-coverage-report', 'verity-compiler-binaries'],
     'compiler-regressions': ['lean-workspace-build', 'lean-workspace-compiler-build'],
     'foundry-gas-calibration': ['static-gas-report'],
-    'foundry': ['verity-compiler-binaries'],
-    'foundry-patched': ['lean-workspace-build', 'lean-workspace-compiler-build'],
-    'foundry-multi-seed': ['verity-compiler-binaries'],
+    'foundry': ['verity-compiler-binaries', 'generated-yul-smoke'],
+    'foundry-patched': ['lean-workspace-build', 'lean-workspace-compiler-build', 'generated-yul-patched-smoke'],
+    'foundry-multi-seed': ['verity-compiler-binaries', 'generated-yul-smoke'],
 }
 
 SPEC['expected_downloaded_artifact_paths'] = {
@@ -915,9 +921,9 @@
     'compiler-audits': [None, None, 'compiler/yul', 'compiler/yul-patched', None, None, 'compiler', 'compiler/bin'],
     'compiler-regressions': [None, None],
     'foundry-gas-calibration': [None],
-    'foundry': ['compiler/bin'],
-    'foundry-patched': [None, None],
-    'foundry-multi-seed': ['compiler/bin'],
+    'foundry': ['compiler/bin', 'compiler/yul-smoke'],
+    'foundry-patched': [None, None, 'compiler/yul-patched-smoke'],
+    'foundry-multi-seed': ['compiler/bin', 'compiler/yul-smoke'],
 }
 
 
diff --git a/test/BytesEqSmoke.t.sol b/test/BytesEqSmoke.t.sol
index d1d15e732..abd41f73f 100644
--- a/test/BytesEqSmoke.t.sol
+++ b/test/BytesEqSmoke.t.sol
@@ -26,7 +26,7 @@ contract BytesEqSmokeTest is Test, YulTestBase {
         bytesEqSmoke = deployCompiledVerityModule(
             "Contracts.BytesEqSmoke",
             "BytesEqSmoke",
-            "artifacts/test-bytes-eq-smoke"
+            _smokeYulDir()
         );
         referenceContract = new BytesEqSmokeReference();
     }
diff --git a/test/LowLevelTryCatchSmoke.t.sol b/test/LowLevelTryCatchSmoke.t.sol
index b5cbd0777..937fc3ffa 100644
--- a/test/LowLevelTryCatchSmoke.t.sol
+++ b/test/LowLevelTryCatchSmoke.t.sol
@@ -40,7 +40,7 @@ contract LowLevelTryCatchSmokeTest is Test, YulTestBase {
         lowLevelTryCatchSmoke = deployCompiledVerityModule(
             "Contracts.Smoke.LowLevelTryCatchSmoke",
             "LowLevelTryCatchSmoke",
-            "artifacts/test-low-level-trycatch-smoke"
+            _smokeYulDir()
         );
         referenceContract = new LowLevelTryCatchSmokeReference();
     }
diff --git a/test/StringArrayErrorSmoke.t.sol b/test/StringArrayErrorSmoke.t.sol
index 9aad0417e..30af032c9 100644
--- a/test/StringArrayErrorSmoke.t.sol
+++ b/test/StringArrayErrorSmoke.t.sol
@@ -36,7 +36,7 @@ contract StringArrayErrorSmokeTest is Test, YulTestBase {
         stringArrayErrorSmoke = deployCompiledVerityModule(
             "Contracts.StringArrayErrorSmoke",
             "StringArrayErrorSmoke",
-            "artifacts/test-string-array-error-smoke"
+            _smokeYulDir()
         );
         referenceContract = new StringArrayErrorSmokeReference();
     }
diff --git a/test/StringArrayEventSmoke.t.sol b/test/StringArrayEventSmoke.t.sol
index 98a8e6f45..b43f3d96b 100644
--- a/test/StringArrayEventSmoke.t.sol
+++ b/test/StringArrayEventSmoke.t.sol
@@ -20,7 +20,7 @@ contract StringArrayEventSmokeTest is Test, YulTestBase {
         stringArrayEventSmoke = deployCompiledVerityModule(
             "Contracts.StringArrayEventSmoke",
             "StringArrayEventSmoke",
-            "artifacts/test-string-array-event-smoke"
+            _smokeYulDir()
         );
         referenceContract = new StringArrayEventSmokeReference();
     }
diff --git a/test/StringEqSmoke.t.sol b/test/StringEqSmoke.t.sol
index 65c6fd037..9c7b21d98 100644
--- a/test/StringEqSmoke.t.sol
+++ b/test/StringEqSmoke.t.sol
@@ -26,7 +26,7 @@ contract StringEqSmokeTest is Test, YulTestBase {
         stringEqSmoke = deployCompiledVerityModule(
             "Contracts.StringEqSmoke",
             "StringEqSmoke",
-            "artifacts/test-string-eq-smoke"
+            _smokeYulDir()
         );
         referenceContract = new StringEqSmokeReference();
     }
diff --git a/test/StringErrorSmoke.t.sol b/test/StringErrorSmoke.t.sol
index 217875af9..4a1da432e 100644
--- a/test/StringErrorSmoke.t.sol
+++ b/test/StringErrorSmoke.t.sol
@@ -36,7 +36,7 @@ contract StringErrorSmokeTest is Test, YulTestBase {
         stringErrorSmoke = deployCompiledVerityModule(
             "Contracts.StringErrorSmokeContract",
             "StringErrorSmoke",
-            "artifacts/test-string-error-smoke"
+            _smokeYulDir()
         );
         referenceContract = new StringErrorSmokeReference();
     }
diff --git a/test/StringEventSmoke.t.sol b/test/StringEventSmoke.t.sol
index 2a0334359..3e3e7c61d 100644
--- a/test/StringEventSmoke.t.sol
+++ b/test/StringEventSmoke.t.sol
@@ -35,7 +35,7 @@ contract StringEventSmokeTest is Test, YulTestBase {
         stringEventSmoke = deployCompiledVerityModule(
             "Contracts.StringEventSmoke",
             "StringEventSmoke",
-            "artifacts/test-string-event-smoke"
+            _smokeYulDir()
         );
         referenceContract = new StringEventSmokeReference();
     }
diff --git a/test/StringSmoke.t.sol b/test/StringSmoke.t.sol
index ce160b079..2b0163414 100644
--- a/test/StringSmoke.t.sol
+++ b/test/StringSmoke.t.sol
@@ -30,7 +30,7 @@ contract StringSmokeTest is Test, YulTestBase {
         stringSmoke = deployCompiledVerityModule(
             "Contracts.StringSmoke",
             "StringSmoke",
-            "artifacts/test-string-smoke"
+            _smokeYulDir()
         );
         referenceContract = new StringSmokeReference();
     }
diff --git a/test/yul/YulTestBase.sol b/test/yul/YulTestBase.sol
index 3580ed8ce..1c338cbbf 100644
--- a/test/yul/YulTestBase.sol
+++ b/test/yul/YulTestBase.sol
@@ -40,6 +40,19 @@ abstract contract YulTestBase is Test {
         return "artifacts/yul";
     }
 
+    function _smokeYulDir() internal view returns (string memory) {
+        if (_usePatchedVerityCompiler()) {
+            if (vm.exists("compiler/yul-patched-smoke")) {
+                return "compiler/yul-patched-smoke";
+            }
+        } else {
+            if (vm.exists("compiler/yul-smoke")) {
+                return "compiler/yul-smoke";
+            }
+        }
+        return _yulDir();
+    }
+
     // Edge-case values matching Lean's edgeUint256Values and DiffTestConfig._edgeUintValues():
     //   [0, 1, 2, 2^128, 2^255, 2^256-2, 2^256-1]
     // Selectors 0-6 return these edge values (~7/16 probability);
@@ -58,20 +71,52 @@ abstract contract YulTestBase is Test {
     }
 
     function _compileYul(string memory path) internal returns (bytes memory) {
-        string[] memory cmds = new string[](3);
-        cmds[0] = "bash";
-        cmds[1] = "-lc";
-        cmds[2] = string.concat(
-            "solc --strict-assembly --bin ",
-            path,
-            " | grep -E '^[0-9a-fA-F]+$' | tail -n 1"
-        );
+        string[] memory cmds = new string[](4);
+        cmds[0] = "solc";
+        cmds[1] = "--strict-assembly";
+        cmds[2] = "--bin";
+        cmds[3] = path;
         bytes memory out = vm.ffi(cmds);
+        // solc output format: "======= ... =======\n\nBinary representation:\n<hex>\n"
+        // Extract the last non-empty line which should be the hex bytecode
         bytes memory trimmed = _trimBytes(out);
-        if (_isHexBytes(trimmed)) {
-            return vm.parseBytes(string.concat("0x", string(trimmed)));
+        bytes memory hexBytes = _extractLastHexLine(trimmed);
+        require(hexBytes.length > 0, string.concat("_compileYul: no hex bytecode in solc output for ", path));
+        return vm.parseBytes(string.concat("0x", string(hexBytes)));
+    }
+
+    function _extractLastHexLine(bytes memory input) internal pure returns (bytes memory) {
+        // Find the last line that is pure hex
+        uint256 end = input.length;
+        while (end > 0) {
+            // Find the start of the current line
+            uint256 lineEnd = end;
+            // Skip trailing whitespace/newlines
+            while (end > 0 && _isWhitespace(input[end - 1])) {
+                end--;
+            }
+            if (end == 0) break;
+            lineEnd = end;
+            // Find the start of this line
+            uint256 lineStart = end;
+            while (lineStart > 0 && !_isWhitespace(input[lineStart - 1])) {
+                lineStart--;
+            }
+            // Check if the line is all hex
+            bool allHex = lineEnd > lineStart;
+            for (uint256 i = lineStart; i < lineEnd && allHex; i++) {
+                if (!_isHexChar(input[i])) allHex = false;
+            }
+            if (allHex) {
+                bytes memory result = new bytes(lineEnd - lineStart);
+                for (uint256 i = 0; i < result.length; i++) {
+                    result[i] = input[lineStart + i];
+                }
+                return result;
+            }
+            end = lineStart;
         }
-        return trimmed;
+        return "";
     }
 
     function _deploy(bytes memory bytecode) internal returns (address addr) {
@@ -92,13 +137,12 @@ abstract contract YulTestBase is Test {
         string memory outDir
     ) internal {
         string memory artifactPath = string.concat(outDir, "/", contractName, ".yul");
+        if (vm.exists(artifactPath)) return;
         string[] memory cmds = new string[](3);
         cmds[0] = "bash";
-        cmds[1] = "-lc";
+        cmds[1] = "-c";
         cmds[2] = string.concat(
-            "artifact='",
-            artifactPath,
-            "'; out='",
+            "out='",
             outDir,
             "'; module='",
             moduleName,
@@ -111,8 +155,6 @@ abstract contract YulTestBase is Test {
             "'; ",
             "compiler=\"./.lake/build/bin/$compiler_name\"; ",
             "if [ ! -x \"$compiler\" ] && [ -x \"./compiler/bin/$compiler_name\" ]; then compiler=\"./compiler/bin/$compiler_name\"; fi; ",
-            "if [ -f \"$artifact\" ] && [ -x \"$compiler\" ] && [ \"$compiler\" -ot \"$artifact\" ] && ",
-            "! find Contracts Compiler Verity -name '*.lean' -newer \"$artifact\" -print -quit | grep -q .; then exit 0; fi; ",
             "mkdir -p \"$out\" && if [ -x \"$compiler\" ]; then lake build \"$module\" >/dev/null; else lake build \"$module\" \"$compiler_target\" >/dev/null; fi && ",
             "\"$compiler\" --module \"$module\" --output \"$out\" $compiler_args >/dev/null"
         );
@@ -126,13 +168,12 @@ abstract contract YulTestBase is Test {
         string memory outDir
     ) internal {
         string memory artifactPath = string.concat(outDir, "/", contractName, ".yul");
+        if (vm.exists(artifactPath)) return;
         string[] memory cmds = new string[](3);
         cmds[0] = "bash";
-        cmds[1] = "-lc";
+        cmds[1] = "-c";
         cmds[2] = string.concat(
-            "artifact='",
-            artifactPath,
-            "'; out='",
+            "out='",
             outDir,
             "'; manifest='",
             manifestPath,
@@ -145,8 +186,6 @@ abstract contract YulTestBase is Test {
             "'; ",
             "compiler=\"./.lake/build/bin/$compiler_name\"; ",
             "if [ ! -x \"$compiler\" ] && [ -x \"./compiler/bin/$compiler_name\" ]; then compiler=\"./compiler/bin/$compiler_name\"; fi; ",
-            "if [ -f \"$artifact\" ] && [ -x \"$compiler\" ] && [ \"$compiler\" -ot \"$artifact\" ] && [ \"$manifest\" -ot \"$artifact\" ] && ",
-            "! find Contracts Compiler Verity -name '*.lean' -newer \"$artifact\" -print -quit | grep -q .; then exit 0; fi; ",
             "mkdir -p \"$out\" && set -- $(grep -vE '^[[:space:]]*($|#)' \"$manifest\") && if [ -x \"$compiler\" ]; then lake build \"$@\" >/dev/null; else lake build \"$@\" \"$compiler_target\" >/dev/null; fi && ",
             "\"$compiler\" --manifest \"$manifest\" --output \"$out\" $compiler_args >/dev/null"
         );
@@ -186,18 +225,6 @@ abstract contract YulTestBase is Test {
         return out;
     }
 
-    function _isHexBytes(bytes memory input) internal pure returns (bool) {
-        if (input.length == 0) {
-            return false;
-        }
-        for (uint256 i = 0; i < input.length; i++) {
-            if (!_isHexChar(input[i])) {
-                return false;
-            }
-        }
-        return true;
-    }
-
     function _isHexChar(bytes1 c) private pure returns (bool) {
         return (c >= 0x30 && c <= 0x39) || (c >= 0x41 && c <= 0x46) || (c >= 0x61 && c <= 0x66);
     }