Use EVMYulLean as the source of truth for Lean-based formal verification#591
Open
duncancmt wants to merge 362 commits into
Open
Use EVMYulLean as the source of truth for Lean-based formal verification#591duncancmt wants to merge 362 commits into
duncancmt wants to merge 362 commits into
Conversation
…imous This bug also found by V12
Prove the compiled lnWad runtime computes Stages.lnWadBody (run_ln_wad_evm_eq_body, reusing the lnWadToRay gate + the sdiv-by-1e9 tail), then compose to make LnYulCorrect.lnWadRuntimeCorrect unconditional and axiom-clean (pinned in AxiomCheck). Both CutCorrect predicates are now discharged: C1 is complete for lnWadToRay and lnWad. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ize axiom gate Prove the compiled runtimes revert for nonpositive inputs (run_ln_wad_to_ray_evm_revert / run_ln_wad_evm_revert via a local runContract revert-bridge) and discharge the RevertsNonpositive predicates. Transport monotonicity, negative-iff, and exact-zero-at-1e18 to the runtime level via the equivalence. AxiomCheck now pins the full public surface (correctness, reverts, transports) to [propext, Classical.choice, Quot.sound]; its note is trimmed to the gate mechanism. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Drop unnecessary simpa wrappers and unused simp arguments flagged by linter.unnecessarySimpa / linter.unusedSimpArgs. No change to proof content or axiom dependencies; full lake build is green and warning-free. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The error-bound constant is lnErrorBoundNum = 1698600000 (1.6986 ulp) and the theorem is lnWadToRayBody_error_bound_1_6986, but four doc comments still cited the old 1699000000 / 1.6990 figure. Update them to the current value. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add runtime-level lnWad zero, sign, and monotonicity theorems and pin their axiom dependencies. Clean stale Lean comments around the ln error budget and lnWad naming. Co-Authored-By: OpenAI Codex <codex@openai.com>
Preserve solc Yul names that differ only by repeated underscores, align ln proof references with generated ABI helper names, and expand 512-bit formal workflow triggers to cover shared helper imports. Co-Authored-By: Codex <codex@openai.com>
…nerators in triggers
The cbrt512/sqrt512 formal-check jobs build Cbrt512Proof/Sqrt512Proof, which
require the CbrtProof/SqrtProof packages and transitively import their
gitignored, Python-generated FiniteCert.lean. Those jobs never ran the
generator, so a clean checkout with a cold build cache could not build the
dependency. Add the generate_*_cert.py step (mirroring the 256-bit jobs) and
extend the untracked-artifact guard to cover the regenerated cert.
Add formal/python/{cbrt,sqrt}/** to the push/pull_request path filters of all
four cbrt/sqrt formal workflows so a change to a cert generator re-triggers
every job that runs it.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Codex <codex@openai.com>
Clean up label-style and external-task references in formal proof comments and add repository guidance forbidding opaque outside identifiers in work product. Co-Authored-By: Codex <codex@openai.com>
Replace the flat LnProof module directory with role-named layer subdirectories (Foundation, Spec, Model, Mono, Floor, Error, Seam), each with a facade module, and quarantine generated certificates under Cert/. Add Theorems.lean as the entry-point signpost: it states every proven property of the compiled runtime, restates the headline guarantees explicitly, and runs the #guard_msgs axiom gate (absorbing AxiomCheck.lean). Add ErrorBoundRuntime.lean, transporting the 1.6986-ulp error bound from the model to run_ln_wad_to_ray_evm via the runtime-model equality, so the published bound holds for the implementation interpretation, not just the model; the new theorem is axiom-clean and gated. The move is path+import only: namespaces and theorem names are unchanged. The generated EVM artifacts (LnYulRuntime/Proof) stay at the lib root because the shared Yul importer derives module names from the last two path components. Generators, .gitignore, CI build targets, and the READMEs are updated to the new layout. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Split the 6912-line Error/Core.lean into 17 component files under Error/Core/, with Error/Core.lean as a re-export aggregator so consumers importing LnProof.Error.Core are unchanged. The source was already in topological order with no private declarations, so contiguous thematic blocks form an acyclic dependency DAG; each file imports only its real backward dependencies. All 363 declarations are preserved and the axiom gate still passes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
State, under Critical Reminders, that comments belong only where the code cannot speak for itself; that a comment explains only its associated code, never the chat/task/plan/diff; and that comments address behavior and intent rather than identifiers, justifying only the obtuse or non-idiomatic. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Mathlib's `cache get` fetches the ProofWidgets cloud release and then removes its `lib`/`ir` build outputs, which throws when those directories are absent and fails the job. Fetch the release and pre-create the directories before each `cache get` so the removal always has a target. Applied to both `cache get` invocations (Mathlib cache and proof dependency cache) in all five formal-proof workflows. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The proofs are anchored to the exact Yul emitted by `forge inspect`, which is governed by the compiler and optimizer settings in `foundry.toml` and the import resolution in `remappings.txt`; add both to every formal workflow's trigger paths so a change to either re-runs verification. Drop the `test/*.t.sol` trigger paths from the cbrt, sqrt, and ln workflows: these jobs build only the Lean proofs and never run the Solidity tests, which are exercised by the regular test workflow on every pull request. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
duncancmt
force-pushed
the
dcmt/formal-nopython
branch
from
89e1010 to
c0e5cca
Compare
e1Ru1o
reviewed
Jun 26, 2026
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
7 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.
No description provided.