feat: remove skipKernelTC overrides and gate against reintroduction#100
Merged
Conversation
Clears the remaining `set_option (debug.)skipKernelTC` sites — the ShiftRightChip/Math.lean RV64-shift `.toNat` unfolds (via the abstract-BitVec bridge) and SailMemory.lean — and drops a few unneeded `native_decide` calls. Adds a CI guard so the override cannot be reintroduced: scripts/check_no_skipkerneltc.sh (any hit in SP1Clean/**/*.lean fails), wired into scripts/run_audit.sh and a standalone CI `guards` job in .github/workflows/lean_action_ci.yml, with the policy documented in AGENTS.md, docs/agents/proof-patterns.md, and docs/release-audit.md. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
dtumad
changed the title
tamirhemo
approved these changes
Jun 23, 2026
dtumad
added a commit
that referenced
this pull request
Jun 23, 2026
Resolved 8 conflicts between upstream spec/bridge work (#100 skipKernelTC gate, #101 immediate-type sail bridges, #102 jalr/jal/branch divisibility specs) and the cleanup-branch golf: - Math/Word.lean: kept my `val_4_ne_zero` one-liner golf; took upstream's `÷4` refactor (val_eq_mul_inv_four_mul_four core + new val_lt_65536_of_mul_inv_four_lt). My `isU64_four` hoist preserved. - FormalModel/Contracts/Chips.lean: took upstream's new JALR LSB-clearing Spec conjunct + doc; kept my rv64_mul_eq golf (auto-merged). - ShiftRightChip/Math.lean: kept my `show T by` golf (equivalent to upstream's `from by`). - JalrChip/Formal, Addw/Jal/Jalr Bridge: took upstream (authoritative #101/#102 rewrites supersede my cosmetic golf there). - BitwiseChip/Bridge: auto-merge silently duplicated the andi/ori/xori immediate bridges; took upstream's clean version. Build clean (3676 jobs), skipKernelTC pass, sorry still only SP1GatedVm.lean:223, axiom census PASS (sorryAx confined to the 5 allowed carriers). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
dtumad
added a commit
that referenced
this pull request
Jun 24, 2026
AGENTS.md: Restructure-status block updated (1 sorry not 4; 3676 jobs / 366 probes; DivRem/Shift/Mul completeness closed; cleanup campaign + main merge #100/#101/#102 noted); Clean dep is a pinned SHA (PR #398), not "@ main"; docs/ index completed (README/roadmap/bus-model/release-audit/extraction/ mul-learnings/cleanup-backlog). axiom-ledger.md + release-audit.md: honest staleness banners (DivRemChip.completeness is no longer a sorryAx carrier; single remaining sorry = sp1_witness_decode; census regenerated 2026-06-23). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Removes the remaining
set_option (debug.)skipKernelTCoverrides from the Clean-native proofs and adds a CI guard so they cannot be reintroduced.Changes (8 files)
SP1Clean/Proofs/Chips/ShiftRightChip/Math.lean— clears the kernel-TC overrides on the RV64-shift.toNatunfolds by isolating the2^64-unfold into an abstract-BitVecbridge proved once over variables, then applied symbolically (thesrl_toNat/sra_toNatpattern).SP1Clean/Model/SailMemory.lean— clears the remaining override site; drops a few unneedednative_decidecalls.scripts/check_no_skipkerneltc.sh(new) — fails if anyskipKernelTCappears inSP1Clean/**/*.lean.scripts/run_audit.sh— wires the guard into the audit harness..github/workflows/lean_action_ci.yml— adds a standaloneguardsCI job running the check.AGENTS.md,docs/agents/proof-patterns.md,docs/release-audit.md— document the policy and the abstract-BitVec-bridge fix.🤖 Generated with Claude Code