Prove error bounds on formally-verified natural logarithm - #589
Open
duncancmt wants to merge 18 commits into
Open
Prove error bounds on formally-verified natural logarithm#589duncancmt wants to merge 18 commits into
duncancmt wants to merge 18 commits into
Conversation
Co-Authored-By: OpenAI Codex <codex@openai.com>
Axiom-clean Lean proof ([propext, Classical.choice, Quot.sound]) that lnWadToRay never overestimates the true log and underestimates it by less than 1.7035 ulp, at the bias margin in Ln.sol (line 117). The never-overshoot is the floor spec (FloorSpec/FloorAssembly over the exp partial-sum cell certificates); the error bound is the uniform-residue budget (ErrorBound/ErrorBoundCert). The ge-branch factored cell route (FactoredCap, ErrCertGe*) certifies the ge branch to 1.6921 ulp standalone. LN_ERROR_BOUND_*.md hold the precision analysis. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The capUB (upper-cap) analog of ge_x1_cap_d22 for the LT branch (X1<0): caps (-x1W)*10^27/QS by the degree-22 partial sum plus the 2*tn^23 remainder tail, via capUB22_of_int at the bracket (ltTN,ltTD) transported along bracket_lt_up by capUB_arg. First milestone of the LT error-bound cell route toward a tighter (~1.701) global bound. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The LT-branch analog of ge_pos_cut_reduced: assembles the curved cap (lt_x1_cap_d22), the c-independent octave collapse (octaveGeBound), the tight bias cap (capBLtight), and the LT phase (posPhaseNatLt/posAvailLt/minPosAvail) into the error-bound cut capLB (lnErrArg r) lnErrQ (wadRayNum x) wadRayStrictDen, reducing to a single c/r/x-independent cell obligation hred in m over [2^95, Sc-46]. hred carries the +2*tn^23 remainder (degree-23 capUB form, vs ge's degree-22). Axiom-clean [propext, Classical.choice, Quot.sound]. Milestone 2 of the LT cell route. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
certErrLt (deg-277, = errLtW*23!*ltTD^23 - errLtK*(m+1)*G with G=expNum22(ltTN,ltTD)*23*ltTD+2*ltTN^23) is discharged over [2^95, Sc-46] by a 16-cell checkCoverK cover (ErrCertLtC00..15); errLt_hred bridges 0 <= certErrLtLit to lt_pos_cut_reduced's hred (direct polySub margin, no sumGE), so lt_pos_cut_reduced . errLt_hred gives the LT error cut, axiom-clean. Measured LT cell cap (min provable lnErrorBoundNum over the branch) = 1698944562/1e9 = 1.698944562 ulp — the binding (global) branch (ge is 1.692115493), so the global lowest provable error bound at the deployed 0.3387 margin is 1.698944562 (below 1.7005, no margin cascade needed). Cert literal currently at the deployed 1.7035 boundNum; not yet wired into the top-level theorem. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The public theorem (renamed model_ln_wad_error_bound_1_7068 -> model_ln_wad_error_bound_1_6990) now proves error < 1.6990 ulp at lnErrorBoundNum=1699000000, down from 1.7035. The LT branch (the binding branch) is routed through the LT cell cut lt_pos_cut_reduced . errLt_hred over [2^95, Sc-46] (22-cell cover) plus a residue band budget rebound to [Sc-45, Sc) at cap 6990; GE (coarse residue, cap 6961) and the negative shift (cap 6785) already clear 1.6990. Full library builds (123 jobs); model_ln_wad_error_bound_1_6990 is axiom-clean [propext, Classical.choice, Quot.sound]. No Solidity changes -- same implementation, tighter proven bound; the deployed 0.3387 bias margin is unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…-units) Raises the Ln.sol bias constant (line 117) so the one-sided never-overshoot margin drops from 0.33866 to 0.33830 ulp, tightening the proven worst-case underestimate from 1.6990 to 1.6986 ulp. The never-overshoot re-derivation at the tighter margin splits the certificate margin floor into two directions: EUN=3382 for the never-overshoot certs (certGeUp, certLtUp; the +form EUD+EUN) and EUNl=3385 for the not-too-low certs (certGeLo, certLtLo; the -form EUD-EUN), since raising the bias tightens never-overshoot but relaxes the undershoot bound. capBU=3383/capBL=3384 bracket the new margin. The never-overshoot cell covers (certGeUp 15 cells, certLtUp 17) are regenerated at EUN=3382 via the GenCover walk; the not-too-low covers are unchanged. The error-bound cell covers are regenerated at the new bias (BIASCAPNUM) and published boundNum 1698600000 (errLt 18 cells, errGe 15). model_ln_wad_error_bound_1_6986 builds axiom-clean [propext, Classical.choice, Quot.sound]; full lake build green (121 jobs); all floor-spec / monotonicity / cut-spec theorems remain axiom-clean. The only Solidity change is the bias constant. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The lt/ge error-budget weights were 200-digit tracked literals. Replace them with their defining formulas: errLtW = BIASCAPNUM·(lnErrQ+minPosAvail)· wadRayStrictDen·10^40, and errGeW likewise with the ge-internal minPosAvail (692115493·2^99+2^27·10^9). They evaluate to the same values, so the cert literals and eval-identity bridges are unchanged; the eWn equality is now near-definitional. ErrorBound builds green, axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ack) The lt/ge error-bound certificate literals (ErrCertLtLit/ErrCertGeLit), their checkCoverK cell covers (ErrCertLtC*/ErrCertGeC*), and the cover modules (ErrCertLt/ErrCertGe) are deterministic functions of the bias and published boundNum, so they no longer belong in revision control. Untrack them and regenerate from the committed GenErrLit generator (a Lean #eval that computes BIASCAPNUM, errLtK/errLtW, and the certificate polynomials from the ErrorBoundCore constants, then walks the kShiftWitness/hornerIv cover that the in-kernel checkCoverK accepts). The ln-formal workflow regenerates them (lake build LnProof.ErrorBoundCore && lake env lean GenErrLit.lean) before the full build, mirroring the existing gen_cert_literals.py step for FloorCertLit. Verified by a clean-regen: deleting the artifacts, regenerating via the CI steps, and running the full lake build is green (121 jobs); model_ln_wad_error_bound_1_6986 stays axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Update the ln error-bound experiment log with the achieved 1.6986 result (superseding the earlier uniform-bracket "can't go below ~1.696" estimate) and the key correctness lesson: the +form certs are never-overshoot, the -form not-too-low, and the cert/lemma names do not line up with the direction in the obvious way. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…; clean lint
Finish moving generated values out of revision control:
- Floor cert cell covers (FloorCert{GeUp,LtUp,GeLo,LtLo}C*) are gitignored and
regenerated by GenCover, now covering all four floor covers. The cover modules
keep their hand-written eval_eq; only the cell files and the _nonneg ladder are
generated (spliced in deterministically).
- BIASCAPNUM is generated into BiasCapNum.lean by GenErr1 (the tight bias-cap
numerator ⌊expNum 130 (BIASc·2^27) QS·10^60 / (130!·QS^130)⌋) and referenced as
`biasCapNum` by capBLtight and the error weights, replacing the tracked
70-digit literal in four files.
- ln-formal CI regenerates the floor cells + BiasCapNum (GenCover, GenErr1)
before ErrorBoundCore, then the error covers (GenErrLit), then the full build.
- Lint: scope the EUN/EUNl simp arguments per FloorCaps lemma (the blanket set
left one unused per lemma) and drop the unused Nat.mul_assoc in ErrorBound.
Validated by a from-clean regeneration: delete every gitignored artifact (floor
cells, error covers, cert literals, BiasCapNum, FloorCertLit), regenerate via the
CI step sequence, and the full lake build is green (125 jobs);
model_ln_wad_error_bound_1_6986 stays axiom-clean [propext, Classical.choice,
Quot.sound].
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The `simp only [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm]` AC-normalization idiom left one argument unfired at a few goals (Nat.mul_assoc in five ErrorBoundCore reassociations; Nat.mul_left_comm in the capUB22_of_int / capLB22_of_int cast normalizations of FactoredCap and LtFactoredCap). Drop the unused argument at each. A full rebuild of every non-cell module is now warning-free; the proof stays green (125 jobs) and axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ator The floor-spec witness, monotonicity, and error-bound Python scripts were demonstrative only — none feed the Lean build. The proof's correctness is adjudicated by the Lean kernel (axiom gate in ln-formal.yml), so remove them along with their CI steps and the JSON they consumed. gen_cert_literals.py now inlines the ten polynomial coefficients it needs (mirrored from src/vendor/Ln.sol) instead of importing them from the deleted check_ln_counterexample.py; FloorCertLit.lean regenerates byte-identically. The Ln.t.sol seam-monotonicity comment now points at the Lean proof LnGeneratedModel.model_ln_wad_mono rather than the deleted Python certificate. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
🛡️ Immunefi PR ReviewsWe noticed that your project isn't set up for automatic code reviews. If you'd like this PR reviewed by the Immunefi team, you can request it manually using the link below: Once submitted, we'll take care of assigning a reviewer and follow up here. |
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
1 participant
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.