Retire EVMYulLean fork-conformance burn-in window (#1828)

Th0rgal · claude · web-flow · commit cac7d44ccf57 · 2026-05-12T02:33:32.000+01:00
* Retire EVMYulLean fork-conformance burn-in window The two-week `continue-on-error` burn-in window for the EVMYulLean fork-conformance probe ended on 2026-05-04 (issue #1722 plan C4). Today is 2026-05-11, so the burn-in gating in the workflow, its test, and the audit/trust docs is stale. - `.github/workflows/evmyullean-fork-conformance.yml`: drop the `BURN_IN_END_UTC` env var, drop `continue-on-error: true` on the probe step (failures now propagate naturally), simplify the "Report probe outcome" step to a pass/fail message, drop the dedicated "Fail after burn-in conformance failure" step, and drop the `Date.now() < burnInEnd` guard inside `open-drift-issue`. - `scripts/test_evmyullean_fork_conformance_workflow.py`: assert the workflow no longer mentions burn-in / `BURN_IN_END_UTC` / `continue-on-error` / `burnInEnd`, and relax the issue-step body assertion to a presence check; rename the relevant tests. - `AUDIT.md`, `AXIOMS.md`, `TRUST_ASSUMPTIONS.md`: replace burn-in language with the steady-state "scheduled or manual failures fail the workflow and open or update a GitHub issue" wording. Verified: `python3 -m unittest scripts.test_evmyullean_fork_conformance_workflow` passes (4/4), and `make check` passes end-to-end (802 tests). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * Sync trust-file date stamps for burn-in retirement PR #1828 changed the CI-guard language in AUDIT.md, AXIOMS.md, and TRUST_ASSUMPTIONS.md but did not bump the Last Updated stamps. The synchronization non-negotiable (CLAUDE.md #1) covers date stamps for any CI-boundary change, so refresh them to 2026-05-12. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
diff --git a/.github/workflows/evmyullean-fork-conformance.yml b/.github/workflows/evmyullean-fork-conformance.yml
@@ -8,11 +8,8 @@ name: EVMYulLean fork conformance
 # public EndToEnd EVMYulLean target still builds, and all 123 concrete
 # `native_decide` bridge-equivalence tests still pass.
 #
-# Burn-in: the probe step is captured with `continue-on-error: true`
-# during the two-week window starting 2026-04-20 (see issue #1722 plan
-# C4 risk analysis). Before 2026-05-04 failures are reported as
-# warnings. After that cutoff, scheduled/manual failures open or update
-# a tracking issue and the job exits red.
+# On scheduled or manual failure the probe job exits red and the
+# follow-up job opens or updates a tracking issue.
 
 on:
   schedule:
@@ -75,9 +72,6 @@ on:
 permissions:
   contents: read
 
-env:
-  BURN_IN_END_UTC: '2026-05-04T00:00:00Z'
-
 concurrency:
   group: evmyullean-fork-conformance-${{ github.ref }}
   cancel-in-progress: ${{ github.event_name != 'schedule' }}
@@ -98,7 +92,6 @@ jobs:
 
       - name: Run EVMYulLean fork conformance probe
         id: probe
-        continue-on-error: true
         run: make test-evmyullean-fork
 
       - name: Report probe outcome
@@ -107,22 +100,7 @@ jobs:
           if [ "${{ steps.probe.outcome }}" = "success" ]; then
             echo "::notice::EVMYulLean fork conformance probe passed."
           else
-            now_epoch="$(date -u +%s)"
-            burn_in_epoch="$(date -u -d "$BURN_IN_END_UTC" +%s)"
-            if [ "$now_epoch" -lt "$burn_in_epoch" ]; then
-              echo "::warning::EVMYulLean fork conformance probe failed during burn-in window (ends $BURN_IN_END_UTC). Investigate locally with 'make test-evmyullean-fork'."
-            else
-              echo "::error::EVMYulLean fork conformance probe failed after burn-in. Investigate locally with 'make test-evmyullean-fork'."
-            fi
-          fi
-
-      - name: Fail after burn-in conformance failure
-        if: steps.probe.outcome != 'success'
-        run: |
-          now_epoch="$(date -u +%s)"
-          burn_in_epoch="$(date -u -d "$BURN_IN_END_UTC" +%s)"
-          if [ "$now_epoch" -ge "$burn_in_epoch" ]; then
-            exit 1
+            echo "::error::EVMYulLean fork conformance probe failed. Investigate locally with 'make test-evmyullean-fork'."
           fi
 
   open-drift-issue:
@@ -135,27 +113,16 @@ jobs:
     steps:
       - name: Open or update drift issue
         uses: actions/github-script@v7
-        env:
-          BURN_IN_END_UTC: ${{ env.BURN_IN_END_UTC }}
         with:
           script: |
-            const burnInEnd = Date.parse(process.env.BURN_IN_END_UTC);
-            if (!Number.isFinite(burnInEnd)) {
-              throw new Error(`Invalid BURN_IN_END_UTC: ${process.env.BURN_IN_END_UTC}`);
-            }
-            if (Date.now() < burnInEnd) {
-              core.notice(`EVMYulLean probe failed during burn-in; no issue opened until ${process.env.BURN_IN_END_UTC}.`);
-              return;
-            }
-
             const marker = "<!-- evmyullean-fork-conformance-failure -->";
             const owner = context.repo.owner;
             const repo = context.repo.repo;
             const runUrl = `${context.serverUrl}/${owner}/${repo}/actions/runs/${context.runId}`;
             const title = "EVMYulLean fork conformance probe failed";
             const bodyLines = [
               marker,
-              "The EVMYulLean fork conformance probe failed after the burn-in window.",
+              "The EVMYulLean fork conformance probe failed.",
               "",
               `Run: ${runUrl}`,
               `Workflow: ${context.workflow}`,
diff --git a/AUDIT.md b/AUDIT.md
@@ -54,9 +54,8 @@ theorem is proved.
   adapter report, rebuilds adapter correctness and the public EndToEnd
   EVMYulLean target, and runs the concrete bridge-equivalence tests.
 - `.github/workflows/evmyullean-fork-conformance.yml` runs the EVMYulLean fork
-  conformance probe weekly. During the burn-in ending 2026-05-04, failures are
-  warnings; after burn-in, scheduled/manual failures open or update a GitHub
-  issue and fail the workflow.
+  conformance probe weekly. Scheduled or manual failures fail the workflow and
+  open or update a GitHub issue for drift triage.
 
 ## Update Checklist
 
@@ -68,4 +67,4 @@ theorem is proved.
    command.
 5. Run `make check`; run targeted Lean builds for changed proof modules.
 
-**Last Updated**: 2026-04-21
+**Last Updated**: 2026-05-12
diff --git a/AXIOMS.md b/AXIOMS.md
@@ -121,8 +121,8 @@ the EVM.
   public EndToEnd EVMYulLean target, and the concrete `native_decide`
   bridge-equivalence tests.
 - `.github/workflows/evmyullean-fork-conformance.yml` runs the conformance probe
-  weekly; after the burn-in ending 2026-05-04, scheduled/manual failures fail
-  the workflow and open or update a GitHub issue for drift triage.
+  weekly; scheduled or manual failures fail the workflow and
+  open or update a GitHub issue for drift triage.
 
 ## External Call Module (ECM) Assumptions
 
@@ -204,4 +204,4 @@ Any commit that adds, removes, renames, or moves an axiom must update this file
 
 If this file is stale, trust analysis is stale.
 
-**Last Updated**: 2026-04-09
+**Last Updated**: 2026-05-12
diff --git a/TRUST_ASSUMPTIONS.md b/TRUST_ASSUMPTIONS.md
@@ -60,7 +60,7 @@ Current theorem totals, property-test coverage, and proof status live in [docs/V
 - **Role**: Runtime execution model.
 - **Status (native transition in progress)**: 25 universal pure bridge theorems (all fully proven) in `Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean`, plus 11 context/env/storage/helper builtin bridge theorems, cover the 36 builtin bridge cases used by the transition regressions. All pure bridge cases are now covered by universal symbolic lemmas. `EvmYulLeanRetarget.lean` now remains transition/regression evidence rather than public compiler-correctness authority. The public EndToEnd composition surface in `Compiler/Proofs/EndToEnd.lean` targets native `EvmYul.Yul.callDispatcher` execution through `Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeHarness`: the public surface is `nativeResultsMatchOn`, `sourceResultMatchesNativeOn`, the source/native result-composition theorem over that native result surface, and the concrete SimpleStorage native theorem. The fuel-indexed `nativeIRRuntimeMatchesIR` seams are file-local. The legacy `YulGeneration.Preservation` contract preservation theorem and the higher-level function equivalence ladder in `YulGeneration.Equivalence` are file-local reference-oracle transition code, and root `Compiler.lean` no longer re-exports the legacy Yul proof stack. Deeper generated/supported-Yul preservation is not yet fully retargeted to native EVMYulLean; `ReferenceOracle.Semantics`, `legacyExecYulFuel`, and related fuel-based helpers remain inside the isolated legacy stack. Gas is not modeled.
 - **Trust boundary (EVMYulLean EndToEnd target)**: For the native EndToEnd path, the runtime authority is EVMYulLean dispatcher execution after Verity Yul is lowered by the native harness and projected onto the observable result surface. The remaining legacy preservation/equivalence stack is transition evidence only until its generated/supported-Yul proofs are rebuilt directly against native EVMYulLean execution.
-- **Fork dependency**: Verity pins [`lfglabs-dev/EVMYulLean`](https://github.com/lfglabs-dev/EVMYulLean), a fork of [`NethermindEth/EVMYulLean`](https://github.com/NethermindEth/EVMYulLean). The pinned commit is recorded in `lake-manifest.json` under the `evmyul` package. The exact divergence from upstream is enumerated in [`artifacts/evmyullean_fork_audit.json`](artifacts/evmyullean_fork_audit.json), regenerated by `scripts/generate_evmyullean_fork_audit.py` and validated by `make check`. As of the current pin, the fork is 2 commits ahead of `upstream/main` and 0 behind; both commits are non-semantic (one visibility change on an exponentiation accumulator, one Lean 4.22.0 deprecation fix), so upstream Ethereum conformance test coverage applies transitively. In addition to the `make check` validation, a weekly scheduled GitHub Actions workflow ([`.github/workflows/evmyullean-fork-conformance.yml`](.github/workflows/evmyullean-fork-conformance.yml)) runs `make test-evmyullean-fork`, which re-verifies the fork audit artifact against `lake-manifest.json`, checks the EVMYulLean adapter report, rebuilds adapter correctness, rebuilds the native transition harness and smoke tests, rebuilds the public EndToEnd EVMYulLean target, and rebuilds the universal bridge lemmas (25 proven) together with the 123 concrete `native_decide` bridge-equivalence tests (`EvmYulLeanBridgeTest`), surfacing any upstream drift as a run annotation during the two-week `continue-on-error` burn-in ending 2026-05-04 and then as a red workflow plus an automatically opened or updated GitHub issue for scheduled/manual failures.
+- **Fork dependency**: Verity pins [`lfglabs-dev/EVMYulLean`](https://github.com/lfglabs-dev/EVMYulLean), a fork of [`NethermindEth/EVMYulLean`](https://github.com/NethermindEth/EVMYulLean). The pinned commit is recorded in `lake-manifest.json` under the `evmyul` package. The exact divergence from upstream is enumerated in [`artifacts/evmyullean_fork_audit.json`](artifacts/evmyullean_fork_audit.json), regenerated by `scripts/generate_evmyullean_fork_audit.py` and validated by `make check`. As of the current pin, the fork is 2 commits ahead of `upstream/main` and 0 behind; both commits are non-semantic (one visibility change on an exponentiation accumulator, one Lean 4.22.0 deprecation fix), so upstream Ethereum conformance test coverage applies transitively. In addition to the `make check` validation, a weekly scheduled GitHub Actions workflow ([`.github/workflows/evmyullean-fork-conformance.yml`](.github/workflows/evmyullean-fork-conformance.yml)) runs `make test-evmyullean-fork`, which re-verifies the fork audit artifact against `lake-manifest.json`, checks the EVMYulLean adapter report, rebuilds adapter correctness, rebuilds the native transition harness and smoke tests, rebuilds the public EndToEnd EVMYulLean target, and rebuilds the universal bridge lemmas (25 proven) together with the 123 concrete `native_decide` bridge-equivalence tests (`EvmYulLeanBridgeTest`), surfacing any upstream drift as a red workflow plus an automatically opened or updated GitHub issue for scheduled/manual failures.
 - **Remaining gap for whole-program retargeting**: The public EndToEnd native surface is in place, but whole-program generated/supported-Yul preservation still needs to be rebuilt directly over native EVMYulLean execution. The legacy reference-oracle preservation/equivalence modules remain importable as isolated transition code, and the external-call/function-table family stays carved out of `BridgedSafeStmts`.
 - **Implication**: Semantic correctness does not imply gas-safety.
 - **Proxy note**: `delegatecall`-based proxy / upgradeability flows still sit outside the current proof-interpreter model. Archive `--trust-report` and use `--deny-proxy-upgradeability` when proxy semantics must remain outside the selected verified subset (issue `#1420`).
@@ -113,5 +113,5 @@ High-level semantics can expose intermediate state in reverted computations. EVM
 
 ---
 
-**Last Updated**: 2026-04-20
+**Last Updated**: 2026-05-12
 **Maintainer Rule**: Update on every trust-boundary-relevant code change.
diff --git a/scripts/test_evmyullean_fork_conformance_workflow.py b/scripts/test_evmyullean_fork_conformance_workflow.py
@@ -38,10 +38,16 @@ def test_concrete_bridge_test_count_matches_adapter_report(self) -> None:
                 f"{path.relative_to(ROOT)} should not contain stale concrete bridge-test counts",
             )
 
-    def test_post_burn_in_failures_open_or_update_issue(self) -> None:
+    def test_scheduled_failures_open_or_update_issue(self) -> None:
         text = WORKFLOW.read_text(encoding="utf-8")
 
-        self.assertIn("BURN_IN_END_UTC: '2026-05-04T00:00:00Z'", text)
+        # The burn-in window ended 2026-05-04; the workflow now fails hard on
+        # any probe failure and the drift issue is unconditionally opened or
+        # updated for scheduled/manual runs.
+        self.assertNotIn("BURN_IN_END_UTC", text)
+        self.assertNotIn("burn-in", text)
+        self.assertNotIn("burnInEnd", text)
+        self.assertNotIn("continue-on-error", text)
         for path in [
             "Compiler/Proofs/EndToEnd.lean",
             "scripts/generate_evmyullean_adapter_report.py",
@@ -109,30 +115,20 @@ def test_post_burn_in_failures_open_or_update_issue(self) -> None:
             re.S,
         )
         self.assertIsNotNone(issue_step)
-        body = issue_step.group("body")
-        self.assertIn("Date.now() < burnInEnd", body)
 
-        fail_step = re.search(
-            r"- name: Fail after burn-in conformance failure\n(?P<body>.*?)(?=\n      - name:|\Z)",
-            text,
-            re.S,
-        )
-        self.assertIsNotNone(fail_step)
-        self.assertIn('if [ "$now_epoch" -ge "$burn_in_epoch" ]; then', fail_step.group("body"))
-        self.assertIn("exit 1", fail_step.group("body"))
-
-    def test_trust_assumptions_describe_post_burn_in_issue_path(self) -> None:
+    def test_trust_assumptions_describe_scheduled_issue_path(self) -> None:
         text = TRUST_ASSUMPTIONS.read_text(encoding="utf-8")
         self.assertIn("weekly scheduled GitHub Actions workflow", text)
-        self.assertIn("two-week `continue-on-error` burn-in ending 2026-05-04", text)
         self.assertIn("automatically opened or updated GitHub issue", text)
+        self.assertNotIn("burn-in", text)
 
     def test_axioms_document_non_axiom_evmyullean_controls(self) -> None:
         text = AXIOMS.read_text(encoding="utf-8")
         self.assertIn("## EVMYulLean Runtime Semantics (Non-Axiom)", text)
         self.assertIn("make test-evmyullean-fork", text)
         self.assertIn(".github/workflows/evmyullean-fork-conformance.yml", text)
         self.assertIn("open or update a GitHub issue", text)
+        self.assertNotIn("burn-in", text)
 
 
 if __name__ == "__main__":
