fix: resolve post-merge bugs from #1716 and #1717#1718
Conversation
- Add `if: '!cancelled()'` to artifact upload steps in build-compiler-binaries to prevent cascade failures when an early upload fails (Bugbot report on #1716) - Update all documentation surfaces from "1 documented Lean axiom" to "0 documented Lean axioms" to match the axiom elimination in #1717: README.md, TRUST_ASSUMPTIONS.md, docs/VERIFICATION_STATUS.md, docs-site/content/index.mdx, docs-site/public/llms.txt - Fix check_layer2_boundary_sync.py expected/forbidden snippets for the zero-axiom state - Fix test_check_axioms.py: update test fixtures that referenced solidityMappingSlot_lt_evmModulus as a documented axiom (now empty DOCUMENTED_AXIOMS set) - Fix test_check_layer2_boundary_sync.py: update test assertions to match the new zero-axiom snippet wording Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…r proof modules Eliminate all remaining sorry placeholders in the proof codebase: - SpongeProperties: discharge wordToBytesLE_size, squeeze256_size, keccak256_core_size via simp/unfold - KeccakBound: discharge fromByteArrayBigEndian_lt_of_size by proving ByteArray.toList.loop_length via functional induction - MappingSlot: remove redundant omega (rewrite now closes goal) Add three new proof modules: - StorageBounds: standalone lemmas for dynamic array operations (setAt length preservation, dropLast length, writeStorageArray frame) - EventSemantics: event encoding structural properties and frame conditions (append distribution, log monotonicity) - HelperStepProofs: helper step interface assembly infrastructure (surface closure → full helper-aware witness composition) Update sorry baseline from 4 to 0 in hygiene checker and docs. Regenerate PrintAxioms.lean and verification_status.json. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
| \n### CI Failure Hints\n\nFailed jobs: `foundry`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
…st-path - Remove stale TODO comments from SpongeProperties.lean (proofs are done) - Enable @[implemented_by solidityMappingSlot_ffi] now that all proofs are complete — runtime uses FFI Keccak while proofs verify against the kernel-computable engine - Add helperFreeContractWitness and _disjoint fast-path theorems to HelperStepProofs.lean for contracts that don't use internal helpers - Regenerate PrintAxioms.lean Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Validate that local artifact cache actually contains expected files after restore (Yul files, difftest binary) — a stale .ready sentinel with empty content caused silent fallback failures on self-hosted runners. Add Lake package integrity check to all foundry jobs to detect and remove corrupted git packages before tests run. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
When .lake/packages/ doesn't exist (after git clean -ffdx), the glob .lake/packages/*/.git expands to its literal string, causing a spurious "Removing corrupted Lake package: .lake/packages/*" warning. Adding shopt -s nullglob makes the for loop iterate zero times when no matches exist. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Two changes to _compileYul() in YulTestBase.sol: 1. Use `bash -c` instead of `bash -lc` (login shell). Login shells read profile files and may have a different PATH than the GitHub Actions step environment, causing `solc` to not be found even though it's installed at /usr/local/bin/solc. 2. Replace the silent fallback (returning raw non-hex bytes as bytecode) with a require() that fails loudly when solc FFI returns non-hex output. Previously, failed compilation would silently deploy a contract with garbage bytecode, causing confusing "call to non-contract address" or wrong-value errors downstream. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Add a pre-flight check before foundry-gas-calibration that verifies solc can actually compile each .yul file in compiler/yul/ via the same pipeline used by _compileYul(). If solc fails, the step prints stderr to help diagnose the environment issue. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
When solc FFI returns non-hex output, retry with stderr captured and print PATH, solc location, and solc stderr to help diagnose the CI vm.ffi environment issue. Also add _solcPath() that uses `which solc` to detect the solc binary location from within the vm.ffi environment. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
…pipes The previous approach used bash pipes (solc | grep | tail) inside vm.ffi, which broke on the CI runner — likely due to the vm.ffi environment not supporting complex pipe chains reliably. New approach: - Call solc directly via vm.ffi(["solc", "--strict-assembly", "--bin", path]) - Parse the hex bytecode from solc output in Solidity (_extractLastHexLine) - This eliminates all shell dependencies (bash, grep, tail) - Add a CI diagnostic step that verifies solc can compile all Yul artifacts before running foundry tests Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
…in CI The foundry CI jobs were failing because _ensureVerityModuleYul called lake build from within vm.ffi, which failed due to corrupted .lake/packages/mathlib on self-hosted runners. Fix by: 1. Pre-building all smoke test Yul artifacts in build-compiler-binaries alongside the existing LocalObligationMacroSmoke pre-build 2. Changing smoke tests to output to _yulDir() so they find pre-built artifacts from CI 3. Adding vm.exists early exit to _ensureVerityModuleYul and _ensureVerityManifestYul to skip FFI when artifacts already exist Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 03298899fc
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| string memory outDir | ||
| ) internal { | ||
| string memory artifactPath = string.concat(outDir, "/", contractName, ".yul"); | ||
| if (vm.exists(artifactPath)) return; |
There was a problem hiding this comment.
This early return now treats any existing artifact as fresh, so forge test can silently reuse stale Yul when Lean sources or compiler binaries have changed since the last run. In practice this causes false-green smoke tests on persistent worktrees (local dev and long-lived runners), because tests execute outdated bytecode instead of recompiling; the same freshness regression is also present in _ensureVerityManifestYul.
Useful? React with 👍 / 👎.
Move smoke test Yul artifacts from compiler/yul/ into compiler/yul-smoke/ (and compiler/yul-patched-smoke/ for patched) to avoid triggering the gas model coverage check which scans compiler/yul/ and errors on opcodes not in the static gas model. - Add _smokeYulDir() to YulTestBase.sol with fallback to _yulDir() - Update 8 smoke tests to use _smokeYulDir() instead of _yulDir() - Pre-build smoke Yul in build-compiler-binaries CI job - Add publish/upload/download artifact steps for smoke Yul directories Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8016a30398
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| if [ -f "$source_dir/.ready" ]; then | ||
| mkdir -p compiler/yul-smoke | ||
| cp -a "$source_dir/." compiler/yul-smoke/ | ||
| rm -f compiler/yul-smoke/.ready |
There was a problem hiding this comment.
This restore block treats a .ready marker as success without verifying that any *.yul files were actually copied, so a partially published or corrupted local artifact can skip the fallback download and leave compiler/yul-smoke empty. In that state, smoke tests still select this directory (it exists) and then fall back to recompiling modules during test execution, which can make CI flaky or fail on runners where lake/Lean build state is unavailable. The same missing validation pattern appears in the other smoke restore blocks (generated-yul-patched-smoke and the multi-seed job).
Useful? React with 👍 / 👎.
- Regenerate verify_sync_spec.json to include smoke Yul artifact entries (generated-yul-smoke, generated-yul-patched-smoke) that were already in the source spec and workflow YAML but missing from the committed JSON - Update verify_sync_spec_source.py with smoke artifact upload/download entries for foundry, foundry-patched, and foundry-multi-seed jobs - Change bash -lc to bash -c in _ensureVerityModuleYul and _ensureVerityManifestYul to avoid login shell PATH issues on CI runners Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
There are 2 total unresolved issues (including 1 from previous review).
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 9090632. Configure here.
Forge's fs_permissions blocked vm.exists() and vm.readFile() for compiler/yul-smoke and compiler/yul-patched-smoke, causing all 8 smoke tests to fail with "not allowed to be accessed for read operations". Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2fce62f207
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| if: steps.local-restore-yul-smoke.outcome != 'success' | ||
| uses: actions/download-artifact@v7 | ||
| with: | ||
| name: generated-yul-smoke | ||
| path: compiler/yul-smoke |
There was a problem hiding this comment.
In verify.yml I checked the foundry, foundry-patched, and foundry-multi-seed jobs, and their smoke-artifact fallback downloads restore directly into compiler/yul-*-smoke without the flattening step that ./.github/actions/setup-foundry/action.yml uses for regular Yul (Normalize generated Yul artifact layout). If local restore misses and GitHub artifact extraction lands files under a nested path, _smokeYulDir() still selects the smoke directory but the expected top-level *.yul files are absent, so smoke tests silently recompile (or fail on runners without a usable lake toolchain). Add the same normalize/validate logic after these smoke fallback downloads.
Useful? React with 👍 / 👎.
- Remove unused _isHexBytes function (Bugbot: dead code after _compileYul refactor to use _extractLastHexLine) - Add .yul file count validation to all 3 smoke Yul local restore blocks (foundry, foundry-patched, foundry-multi-seed) so stale .ready sentinels with empty directories trigger fallback download - Add normalize+validate step after smoke Yul fallback downloads to flatten nested artifact paths and fail fast if no .yul files exist Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
All 7 foundry-multi-seed jobs hit the 25-minute timeout on the first push-to-main that included compiler changes (PR #1718 merge). Each matrix entry runs the full difftest suite for a single seed, and 25 minutes is too tight on the build runner. Bumping to 45 minutes gives comfortable headroom based on observed ~25-minute runtime. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
* ci: bump foundry-multi-seed timeout from 25 to 45 minutes All 7 foundry-multi-seed jobs hit the 25-minute timeout on the first push-to-main that included compiler changes (PR #1718 merge). Each matrix entry runs the full difftest suite for a single seed, and 25 minutes is too tight on the build runner. Bumping to 45 minutes gives comfortable headroom based on observed ~25-minute runtime. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * ci: update verify sync spec to match new 45-minute timeout The check_verify_sync.py script validates that workflow timeouts match the spec. Update the source spec and regenerated JSON to reflect the foundry-multi-seed timeout bump from 25 to 45 minutes. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude <noreply@anthropic.com>
2 participants
Summary
Fixes all bugs reported by Codex and Bugbot on PRs #1716 and #1717 after merging.
CI fixes (from #1716 Bugbot reports)
if: '!cancelled()'to all 8 sequential artifact upload steps inbuild-compiler-binaries. Previously, a transient failure on any early upload step (e.g., difftest interpreter) would skip all subsequent uploads since GitHub Actions defaults toif: success(). Now each upload runs independently.Documentation sync for zero axioms (from #1717 Codex reports)
PR #1717 eliminated the last axiom (
solidityMappingSlot_lt_evmModulus) but didn't update all documentation surfaces that referenced "1 documented Lean axiom". Updated:Test and validation fixes (from #1717 Codex reports)
solidityMappingSlot_lt_evmModulusfrom test fixtures sinceDOCUMENTED_AXIOMSis now empty.Runner script bugs (from #1716 Codex/Bugbot reports)
Investigated and verified these are false positives in the final merged code:
fastlaneandbuildlabels (line 36)ensure_runner_servicecall (line 237)installed_service_name()from.servicefile (line 197)Test plan
make checkpasses (425 tests)python3 scripts/check_axioms.pypasses (0 axioms)python3 scripts/check_layer2_boundary_sync.pypassespython3 scripts/test_check_axioms.pypasses (9 tests)python3 scripts/test_check_layer2_boundary_sync.pypasses (6 tests)python3 scripts/check_verify_sync.pypasses (9 invariant groups)🤖 Generated with Claude Code
Note
Medium Risk
Medium risk because it changes CI artifact restore/upload behavior and adds/rewires core proof lemmas (Keccak bound + mapping slot backend), which could affect verification runs and performance if assumptions are wrong.
Overview
Eliminates the last documented Lean axiom by proving Keccak output sizing and a
fromByteArrayBigEndianbound, then turningsolidityMappingSlot_lt_evmModulusinto a theorem and re-enabling@[implemented_by]for the FFI mapping-slot function.Hardens CI and Foundry pipelines: validates local artifact restores (Yul caches +
difftest-interpreter) before skipping downloads, adds independent artifact uploads viaif: '!cancelled()', and introduces separate smoke Yul artifacts (generated-yul-smoke/generated-yul-patched-smoke) that Foundry jobs restore/validate and tests prefer via_smokeYulDir().Adds new proof helper modules (
EventSemantics,StorageBounds,HelperStepProofs), updates axiom-reporting/sync scripts and docs to reflect 0 axioms / 0 sorries, and adjusts Foundry’ssolcinvocation/parsing to be more robust.Reviewed by Cursor Bugbot for commit 6b268fb. Bugbot is set up for automated code reviews on this repo. Configure here.