Formally verified expRayToWad - #593
Open
duncancmt wants to merge 153 commits into
Open
Conversation
Computes floor(10**18 * exp(x / 10**27)) or one less (never overestimating) for x up to the octave k = round(x / (10**27 * ln2)) = 63, reverting Panic(0x11) above that. The result is monotone, equals 10**18 exactly at x == 0, and is 0 for x at or below floor(10**27 * ln(10**-18)). On the central octave it is tight, so expRayToWad(lnWadToRay(w)) == w - 1 for w/10**18 in [1/sqrt2, sqrt2) (== w at the scale point), letting a consumer in that regime recover w by adding one. The kernel reduces x = k*ln2 + t and evaluates the reciprocal-symmetric rational exp(t) = (Ev(t^2) + t*Od(t^2)) / (Ev(t^2) - t*Od(t^2)) -- Od degree 4, Ev degree 5 and monic -- on a mixed fixed-point staircase, then floors with the 2**k scaling folded into the closing shift. test/0.8.34/Exp.t.sol checks it differentially against a 120-digit mpmath oracle over FFI, plus the lnWadToRay round trip, monotonicity, the scale point, the over-range revert, and underflow to zero. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Document putting literal operands on the left of commutative ops (using the operand-flipped opcode when only one variant is commutative), the zero-arm-first form for boolean Yul switches, and the prohibition on pkill/killall (target a specific PID instead). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Rework the reduction t = x/10^27 - k*ln2: K27*x now takes a single sar(107, ...) to Q128 and subtracts k*floor(ln2*2^128), replacing the Q135 form (sar(100, ...), subtract k*round(ln2*2^135), then a second sar(7, ...)). One fewer SAR and a 16-byte ln2 word instead of 17 bytes. Correct the documented magnitude of E at the revert threshold: ~1.30*10^37, not 10^19. Add testFuzzExpRayToWadCentralExact, a direct oracle check over the central reduced-argument band. Co-Authored-By: Codex <codex@openai.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…mate The 2^62 margin does not cover the upward bias of the Q128 range reduction (floor(ln2*2^128) under-subtracts k*ln2), so expRayToWad returned floor(E)+1 at k=62,63 -- violating the never-overestimate contract. Raise the one-sided margin to 0x594b01498486da8f, the least integer that covers the analytic worst-case overshoot S = 0.6976014718030033189 ulp, i.e. ceil(2^63*S) at the supported edge k=63. Both guarantees then close: A <= E (never over) and E-A < 1 (at most one ulp low). Document the exact per-source error budget and a monotonicity argument in the kernel comment, mirroring Ln.sol. Scrub comment references to identifiers absent from the code and correct the rational's stated precision (~135-bit approximation order, ~126-bit integer realization). Tests: raise the differential and central-exact FFI fuzz to 10000 runs; add deterministic octave-boundary monotonicity coverage and a high-k never-overestimate regression. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Subtract k*ln2 from K27*x at the Q235 product basis using a single 30-byte ln2 word, then one sar to Q128. This is the same op count (2 MUL, 1 SAR, 1 SUB) and runtime gas as the Q128 reduction -- only the ln2 constant widens (16 -> 30 bytes). The reduction's upward bias is negligible at this basis (~2.3e-6 ulp), so the analytic worst-case overshoot is S = 0.0858862987232991853 ulp and the one-sided margin its analytic minimum 0xafe527e18748a8a = ceil(2^63*S). Never-over and at-most-one-under still close; the error-budget comment is updated to match. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Add ExpWrapper.sol (selector 0x4187462b), an exp kind in formal/yul/YulImporter.lean
and generate_from_forge.sh, and the formal/exp/ExpProof lake package mirroring
formal/ln/LnProof. The generated ExpYul{,Runtime,Proof}.lean (gitignored) compile:
run_exp_ray_to_wad_evm is the EVMYulLean interpretation of the compiled Yul, with
the function chain external_fun_wrap_expRayToWad_99 -> fun_wrap_expRayToWad_99 ->
fun_expRayToWad_70 (overflow guard) -> fun__expRayToWad_80 (kernel), plus fun_panic_8.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Codex <codex@openai.com>
Direct on the EVMYulLean run_exp_ray_to_wad_evm interpretation (no hand model): - Seam/RuntimeShared.lean: u256 bounds, wordNat_sar/sdiv bridges, u256 idempotence (contract-agnostic; reused by both revert and the kernel arithmetic). - Seam/Guard.lean: slt(x, 0x8e383a2cdfa1b74a9422d2e1) = 0 for signed x at/above the threshold (the overflow-guard comparison; also bounds the in-range domain). - Seam/Revert.lean: primCall_revert_yul, the zero_value helper direct, and call_fun_panic_8_revert_direct (mstore;mstore;revert reduces to .error .Revert). All build and are axiom-clean ([propext, Classical.choice, Quot.sound]). This validates per-function interpreter reduction and revert mechanics on the exp contract. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Codex <codex@openai.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Adds Seam/Helpers.lean (the solc ABI/cleanup-plumbing per-function directs, shared with the value path) and call_fun_expRayToWad_70_revert_direct in Seam/Revert.lean: for 0x8e383a2cdfa1b74a9422d2e1 <= u256 x < 2^255 the overflow guard fires and the function reverts via fun_panic_8(ARITHMETIC_OVERFLOW). This is the core supported-range revert logic. Axioms: [propext, Classical.choice, Quot.sound]. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Codex <codex@openai.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Reformulate call_fun_expRayToWad_70_revert_direct to the (fuel + (extra + N)) slack form so callers can feed it inline, and add call_fun_wrap_expRayToWad_revert_direct (fun_wrap_expRayToWad_99 forwards to fun_expRayToWad_70). Completes the function-level supported-range revert chain. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Codex <codex@openai.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Adds Seam/Dispatcher.lean (branch-agnostic dispatcher/calldata seam for ExpYul:
expSharedAfterFreePtr, the ABI decode chain, shift_right_224, the 0x4187462b
selector switch-case, and the contract-polymorphic runContract_revert_of_exec_revert)
and the revert-specific external/dispatcher reductions in Seam/Revert.lean,
yielding the top-level
run_exp_ray_to_wad_evm_revert :
0x8e383a2cdfa1b74a9422d2e1 <= u256 x -> u256 x < 2^255 ->
run_exp_ray_to_wad_evm x = .error "revert"
proven directly on the EVMYulLean interpretation of the solc/forge Yul, with no
new models. Axioms: [propext, Classical.choice, Quot.sound].
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Codex <codex@openai.com>
Theorems.lean restates the supported-range revert theorem (run_exp_ray_to_wad_evm_revert) and runs the
axiom gate (#guard_msgs in #print axioms) pinning it to {propext, Classical.choice,
Quot.sound}; the root ExpProof.lean imports it so the default lake build covers the
whole proof and a stray axiom/sorry breaks the build. exp-formal.yml mirrors
ln-formal.yml: regenerate the EVMYulLean artifacts from the compiled ExpWrapper Yul
IR, then build the ExpProof package.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Codex <codex@openai.com>
Seam/Value.lean reduces fun__expRayToWad_80 / fun_expRayToWad_70 / fun_wrap_expRayToWad_99 at x=0 to 10^18: at the scale point every mul-by-x vanishes (k=t=v=0), the rational form is 2^126, and the iszero(0)=1 fix-up lands the result exactly at the wad unit. The overflow guard iszero(slt(0,threshold))=0 is concrete, so the panic branch is skipped without needing a general wordNat_slt. These are the function-level core of zero-input exactness; the ABI .ok dispatcher wrapping is next. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Codex <codex@openai.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… path Adds call_allocate_unbounded_direct and the two abi_encode directs (Nat-indexed value) to Seam/Dispatcher.lean, reusable by the value-path ABI return. The helper lemmas cover the allocation and ABI return encoding sub-calls used by the scale-point value-path reduction. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Codex <codex@openai.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Completes the value path at the scale point x=0 through the ABI .ok dispatcher: run_exp_ray_to_wad_evm_zero : run_exp_ray_to_wad_evm 0 = .ok 1000000000000000000 At x=0 the kernel collapses to concrete arithmetic (k=t=v=0, rational form 2^126) and the iszero(0)=1 fix-up lands exactly 10^18; the guard is skipped (concrete slt), and the external entrypoint ABI-encodes and returns it. Added to the Theorems.lean axiom gate. Axioms: [propext, Classical.choice, Quot.sound]. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Codex <codex@openai.com>
Adds wordNat_slt (wordNat (UInt256.slt a b) = evmSlt (wordNat a) (wordNat b)) and the evmSlt_u256 absorbers to Seam/RuntimeShared.lean. evmSlt already existed in FormalYul/Word.lean; this is the missing wordNat-preservation bridge, proven via a 4-way sign case-split on the excess-2^255 offset comparison. Prerequisite for the symbolic-x kernel reduction used by the runtime floor and monotonicity claims. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Codex <codex@openai.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
call_fun__expRayToWad_80_direct reduces fun__expRayToWad_80(x) to the inline let-shared evm* arithmetic tree (transcribed from Exp.sol _expRayToWad, no hand model) via eq_of_wordNat_eq + the wordNat_*/evm*_u256 bridges (incl. the new wordNat_slt). The foundation for the runtime floor and monotonicity claims. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Codex <codex@openai.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
slt(x, threshold) = 1 for signed x < threshold (either negative, or nonnegative below the threshold) — the complement of slt_thresh_ge. Lets the value-path fun_expRayToWad_70 reduction skip the panic branch. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ic x) call_fun_expRayToWad_70_direct (guard skipped via slt_thresh_lt) and call_fun_wrap_expRayToWad_direct forward the kernel evm* tree for any signed input below the threshold (u256 x < 0x8e3...2e1 or 2^255 <= u256 x). Completes the function-level value path (kernel -> 70 -> wrap), all returning the inline tree. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
run_exp_ray_to_wad_evm_eq_tree : for signed x below the threshold, run_exp_ray_to_wad_evm x = .ok <TREE x> (the inline evm* arithmetic tree). Value-preserving mirror of run_exp_ray_to_wad_evm_zero through the ABI dispatcher, threading hval into the wrapper. Adds the generic RuntimeShared.toNat_ofNat_evmAdd helper. In the Theorems.lean axiom gate. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Codex <codex@openai.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…rdMono) Ports the contract-agnostic int256 floor/division/shift transports the exp monotonicity argument needs into the ExpYul namespace: a general evmSar floor sandwich (arbitrary shift), evmSdiv sign-pinned transports, evmShr/evmShl in-range identities, cross-multiplied division monotonicity, and Int multiplication-monotonicity helpers. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…Mono/RunBridge) Captures <TREE x> as thin layered defs (kTree/tTree/vTree/evTree/odTree/todTree/ r0Tree/r1Tree/expTree) so the deep Horner accumulator is never forced into whnf (which overflows the kernel C stack). Proves run_exp_ray_to_wad_evm x = .ok (expTree x) on the supported domain, and the signed-comparison characterisation of the evmSlt clamp. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Reduces int256 (expTree ·) monotonicity to the meaningful region: below the clamp boundary C (a negative signed value) expTree x = 0 (clamp off, pin cannot fire); above it the decode is [x=0] + r1Tree x. Proved via an abstract body word so the kernel never reduces the Horner accumulator. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Bundles the analytic obligations as RegionMonotonicityFacts (r1Tree in range, nonnegative, nondecreasing, and the scale-point pin clearance) and derives expTree_mono over the whole supported domain by casing on the clamp boundary. Lifts it to the run level as run_exp_ray_to_wad_evm_mono, modulo the analytic core. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Codex <codex@openai.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Transports the rounding-shift argument 2^199 + CINV*x to Int (no overflow on the meaningful region, |int256 x| < 2^96), establishes the k floor sandwich, and proves k = round(x/(10^27 ln2)) is nondecreasing in the signed input. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Adds the octave-index bound (-61 <= k <= 63 on the region) and transports the reduced-argument shift K27*x - LN2*k to Int (products stay below 2^255). Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Adds the t floor sandwich and proves t is nondecreasing in the signed input within a fixed octave (K27 > 0, floor of an increasing affine map). Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Wires the Mono layer into the package and adds run_exp_ray_to_wad_evm_mono to the Theorems signpost with its axiom gate (axioms = the three standard ones). The theorem holds over the whole supported domain given the meaningful-region core RegionMonotonicityFacts; the clamp/pin shell, run-level bridge, and octave-index / reduced-argument transports and monotonicity are unconditional. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Codex <codex@openai.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Port ln's polynomial-nonnegativity certificate checker (Foundation/Poly.lean, namespace ExpPoly) into ExpProof, and add the Horner-stage Int transports (Mono/Stages.lean): - the reduced-argument bound |int256 (tTree x)| < 2^127 (from the coupled k-/t-octave sandwiches); - v = t² in Q128 as a Nat, < 2^126; - two-sided bounds on the even/odd Horner accumulators (0x4e14… ≤ ev < 2^127, 0x270a… ≤ od < 2^126) via a chained no-overflow stage bound. All axiom-clean ([propext, Classical.choice, Quot.sound]). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Codex <codex@openai.com> Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Mono/Quot.lean assembles the reciprocal-symmetric quotient from the Horner stage bounds, all via abstract opaque-word helpers so the deep Horner tree is never forced into whnf: - tod = t*Od in Q87 transported to Int, |tod| < 2^125; - num = ev+tod and den = ev-tod are strictly positive; - r0 = sdiv(2^126*num, den) satisfies 1 <= r0 < 2^128. These supply the range/nonneg obligations of RegionMonotonicityFacts. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Codex <codex@openai.com>
Mono/RangeNonneg.lean closes two of the four RegionMonotonicityFacts fields: - range: r1Tree x < 2^254 (the closing shift s = 126-k in [63,187] floors the shift argument WAD*r0-MARGIN < 2^188 down below 2^125 < 2^254); - nonneg: 0 <= (r1Tree x : Int) (trivial Nat cast), plus the signed int256 (r1Tree x) >= 0 used by the floor argument. Both via abstract opaque-word helpers (closing_shift, shiftArg_bounds_of, closingSar_facts) so the deep Horner tree is never forced. Adds r0Tree_lt to Tree.lean. Axiom-clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-Authored-By: Codex <codex@openai.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. |
forge inspect ... ir trusts whatever artifact the compile cache serves for the target; an artifact compiled without the ir extra output makes it fail with "IR output missing from artifact" instead of recompiling. The script's methodIdentifiers inspection compiles such artifacts, so the second generate in a job -- the LnWrapper step of exp-formal.yml, whose sources share Panic.sol with the ExpWrapper step before it -- hit that failure. Setting FOUNDRY_EXTRA_OUTPUT='["ir"]' on every invocation keeps the cache's artifact settings uniform across both inspections and across successive runs, in CI and against a developer's existing cache. The emitted Yul is unchanged: the generated runtime modules are byte-identical for the exp and ln wrappers. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…roof The 32 granularity pieces (vlo, vhi, T, DOver, DUnder) live once, in the tracked leaf module Floor/GranPieces.lean. GenExpVLit.lean instantiates the per-piece certDOverP/certDUnderP cover certificates from that table (output byte-identical), and Floor/GranV proves the per-piece facts over the same entries: granPieces_ok establishes PieceOK for every table entry, the kernel-decided cover and cap facts (granPieces_cover via piecesCover, granPieces_caps) replace the literal piece dispatch, and piece_select picks the runtime point's piece through the cover, keeping its statement unchanged (GranPair and everything downstream are untouched). The K cap is carried as evalPoly Kpoly vhi, derived from the tracked Kpoly at the piece's upper edge rather than restated per piece. The certificate-generation step builds ExpProof.Floor.GranPieces alongside ExpProof.Floor.CertDefsV before running the generator (exp-formal.yml and the README build block). Full lake build is green from scratch through the Theorems.lean axiom gates; every public statement is unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The trailing-zero trim, greedy checkCoverK cell walk (with its binary width search), zero-padded index, literal-list emitter, and the cover-cell / _nonneg-ladder text templates live once, in Common.GenCover; the four cover-walking generators (GenExpVLit, GenCover, GenErrLit, GenFloorCertLit) consume them instead of carrying per-file copies. GenErrLit keeps only its namespace-wrapping litText variant, expressed over the shared emitter, and GenFloorCertLit's whole-file assembler is renamed fileText to keep the shared name unambiguous. Every certificate-generation build line (exp-formal.yml, build-ln-proof, and the README blocks) builds Common.GenCover before running the generators. All generated certificate files and all four generators' stdout are byte-identical. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
expRayToWad returns the kernel result with a plain return statement, which shifts solc's AST ids: the compiled wrapper's generated functions are now fun_expRayToWad_68, fun__expRayToWad_78, and the wrap/external pair 97, and the kernel body ends in a leave statement rather than a dead let. The Seam reduction layer follows the regenerated artifacts: every generated-name reference is renumbered, and the fun_expRayToWad walk simp sets carry EvmYul.Yul.State.revive and EvmYul.Yul.State.setLeave to reduce the leave, matching the dispatcher walks. The reduction simp sets are also pruned to the lemmas the walks use. The emitted Yul is otherwise identical modulo internal variable ids; no statement outside the Seam layer changes. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Every fix removes the dead thing itself rather than silencing the linter: unused simp arguments are pruned from the reduction and cap proofs (exp Seam sets were pruned with the renumbering; this covers ln RuntimeModel, Floor/Caps, Error/FactoredCap, Error/LtFactoredCap, Common ExpSum and Word, and exp GranV); hypotheses nothing consumes are dropped from smooth_cross_of, DENv_ge_over, tele_step_frac, t_over_2128_le_half_log2, and exp_t_le_sqrt2, with their call sites updated; four ring calls after closing converts and an unused ipow255 are deleted; and Stages moves off the deprecated Int.ofNat_ediv to Int.natCast_ediv. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The general shift/division floor lemmas live once, in Common.Word: evmShr_lt, evmShl_lt, evmShr_eq_div, evmShl_eq, the signed evmSar floor sandwich at an arbitrary shift, and the truncated-division monotonicity chain (nat_div_cross_mono, toNat_mul_of_nonneg, cross_to_div). exp Mono/WordMono keeps its short names as one-line re-exports (the same shape it already uses for the FormalYul.Preservation transports); its ipow256/ipow255 delegate to intPow256/intPow255 and the dead le_of_mul_le_mul_pos is removed. ln stops re-proving shared facts: Foundation/Word's twelve int256/evm* transports delegate to FormalYul.Preservation, Foundation/WordDiv's seven per-shift evmSar sandwiches and three evmShr floor-division instances derive from the Common.Word general lemmas (statements unchanged, so no call site moves), Mono/Step's cross_to_div and toNat_mul_of_nonneg delegate likewise, Seam/RuntimeModel drops its verbatim copies of the Common.Word u256/wordNat bridge (u256_lt_word through wordNat_sdiv) in favor of the shared module, and Floor/Caps takes eval01 from Common.Foundation.Kronecker. Both proof packages build green through their axiom gates with the generated certificates byte-identical. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The closing bases take the two free bits the final coefficients' byte widths and the 256-bit t*Od product leave: Ev closes at Q88 (final stage shr 0x7e) and Od at Q89 (shr 0x80), with the t*Od sar landing at Q88 (0x81) to match Ev; both final coefficients are exact rescalings sharing the 16-byte literal 0x9c2948bcaca16a0dd2fe98bb4470c3c4, so the exact rational and its analytic certificates (the Taylor cut, the 32-piece granularity table, every generated cover) are unchanged. Halving the closing truncations halves the runtime-bridge budget: the Horner/div jitter certifies at 0.21706 (ev bracket width 142941343449089*2^480 at 2^527, od 269746241*2^480 at 2^508, alignment 2^637, tod grid 2^129), the never-over budget at B = 6013505372794194988/10^19, and the under deficit at 31/10 (link-1 5/2). The margin is the budget floor 0x2161b482a02 = floor(5^18*B) + 1 = 2293970250242; the k = 63 deficit envelope is 0.40131 < 1. The supported range stays pinned at k <= 63. Every documented property and test witness is unchanged; the supported-edge result is now certifiably the exact floor and its test asserts equality. Full lake build is green from the Theorems.lean axiom gates with certificate regeneration byte-identical; validated against a 60-digit reference on 8000+ adversarial points and the lnWadToRay round trip. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The joint low-bit refinement re-runs on the finer closing grids (sensitivity curves at 90 digits, LP min-max over the quasi-continuous dimensions, exhaustive search over the two constant-term dimensions, integer polish): six mid-stage coefficients move and the two constant terms move identically, keeping Ev(0) = 2*Od(0) exact. The kernel now binds that shared 16-byte literal once (c0 = 0x9c2948bcaca16a0dd2fe98bb4470c388) and closes both Horner chains from it. The realized relative envelope tightens to <= 0.0075 ulp (~133 of the form's ~135 bits, within 0.1% of the constrained continuous optimum), which carries the Taylor cut at the 2^-132 nudge with 2.1x slack and halves the Mp budget term to 220970869120796102/10^19. The never-over budget is B = 5792534503673398887/10^19 (jitter, granularity, and reduced-argument terms unchanged) and the margin is its exact grid floor 0x2027afc6c05 = floor(5^18*B) + 1 = 2209676553221, with strictness slack 1 - 1381252288818359375/10^19. The under side is unchanged at 31/10; the k = 63 deficit envelope is 0.39891 < 1. The proof re-derives the coefficient-bearing layers: CertDefsV literals and stagings (outer scales 2^1192/2^1040), the 2^132 cut scales through CapsV and the cert-real lemmas, GranV's Kpoly and cross expansion (the 32-piece table and its 2^131-folded budget inequalities are unchanged -- the fold is nudge-independent and the 2^132 amplification it feeds is strictly smaller), den_ge_194, and the margin word. Certificates regenerate with every cover reached; the bracket geometry from the Q88 carry is untouched. Full lake build is green from the Theorems.lean axiom gates; validated against a 60-digit reference on 8000+ adversarial points and the lnWadToRay round trip; all 11 tests and every witness are unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The revert threshold moves to the k = 65 boundary, 0x907595ccd30708cabec8a9db = ceil((65*2^200 - 2^199)/CINV) ~= 44.71e27 (E up to ~2.61e37): with the refit budget the deficit envelope ((31/10)*10^18 + 2^18*MARGIN)/2^(126-k) is 0.79781 at k = 64 and first exceeds one ulp at k = 65, so the guard now sits exactly where floor-or-one-less stops being certifiable. The octave count spans [-61, 64], the closing shift [44, 168], and the k*ln2 grid-residue and round-trip deficit chains carry the widened bounds (64/2^235 and ((31/10)*WAD + MARGIN)/2^44 respectively, each with ample slack). Every documented property is unchanged in form; the certificate layer is untouched and regeneration is byte-identical. Tests cover the new octave: never-overestimate witnesses with frac(E) > 0.9999 at k = 64, the supported-edge bracket (frac(E) ~= 0.52 inside the 0.80 envelope) beside the exact k = 63 top floor, a k = 64 one-ulp-underestimate witness at the octave's first input, and the boundary-monotonicity loop through the k = 65 seam. Full lake build is green from the Theorems.lean axiom gates (the public revert statement carries the new threshold); validated against a 60-digit reference across the new octave and its seams. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The clamp comparison spells its constant as sub(0x00, 0x85ebc478242540a11f5f1029) -- the 12-byte magnitude ceil(18*ln10*10^27) negated in-line -- rather than the 32-byte two's-complement literal. The representation choice stays with the optimizer: at 2000 runs the constant folds back into the single push, and at low runs settings the negated form gives the constant optimizer a 15-byte encoding to work from (5 gas over the push). The magnitude also states the boundary's derivation directly. The Seam value walks mirror the compiled form (evmSub 0x00 ... in the eight quoted trees); the runtime bridge closes by kernel evaluation, so Cmask and every downstream statement are unchanged. Full lake build green from the axiom gates; tests unchanged. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…^192 The closing sequence multiplies the numerator by 10^18*2^68 = 5^18*2^86 before the single DIV, so the quotient lands directly on the 2^68 output grid: one truncation at the finest achievable scale, margin 0x03 (the least grid integer above the never-over image 5^18*B/2^40 < 2.0097), and a closing shift of 68 - k. This saves 6 gas per call versus scaling after the division and strictly improves accuracy: the k = 64 deficit envelope is (33/4 + 3)/2^4 = 45/64 ~= 0.703 ulp, and 26 of 20,524 sampled outputs move from floor(E)-1 to floor(E), none the other way. The octave reciprocal is CINV = round(2^192/(10^27*ln2)), 13 bytes; the computed k is bit-identical for every live input (minimum per-tie safety factor 6.6x, binding at the j = -54 tie), so the guard threshold and all witnesses are unchanged. The proof re-derives the closing layer on the scaleQ68 grid pre-floor: the under deficit is 33/4 grid units including the one-unit DIV floor (link-1 6210/1000, Mp 2/25, reduced-argument gap 1267/1000, negative-half granularity 571/1000), the over side is covered by the margin with 0.99 units of strictness slack, and the k-extraction sandwich sits on the 2^192 basis. Full lake build is green from the Theorems.lean axiom gates. Tests: a central-octave round-trip fuzz test is added; every existing witness value is unchanged; 12/12 pass at 10k fuzz runs; forge fmt clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
One bit moves from the output grid into the closing polynomial bases: the numerator closes at Q89 (the even chain's closing constant is exactly twice the odd chain's, ending the shared literal), t is carried at Q129 in the freed t*Od headroom, the quotient pre-scale is 10^18*2^67 = 5^18*2^85, and the margin is the single grid unit 0x01. The revert threshold moves to the k = 66 boundary, 0x92b2f16cc66c5a4ae96e80d4 ~= 45.40e27 (E up to ~5.22e37). Runtime gas is identical; every documented property is unchanged in form. The rebalance was chosen by exact-rational measurement: the truncation deficit is owned by the odd-side closing sites, amplified antisymmetrically through the numerator and denominator, so the widened bases drop the true envelope 2.5x while the margin requantizes from 3/16 to 1/4 ulp at the edge octave. formal/README.md documents the procedure (measure the true envelope, attribute per truncation site, rebalance bases, certify piecewise) for future transcendental kernels, including the dead ends. The proof certifies the under deficit at 2993/1000 grid units (link-1 including the DIV floor <= 2378/1000 via a 32-piece kernel-checked certificate -- global worst-case aggregation provably cannot reach the target -- plus the reduced-argument gap at 307/1000 / 218/1000 per sign half, Mp <= 2/25, negative-half granularity <= 143/500), the over side under the one-unit margin with B-image ~0.99527, and the k = 65 deficit envelope at 3993/4000 ulp. The certificate domain doubles to H129 and all cover cells regenerate; the octave fold, seam, and round-trip chains carry the 2^67 grid. Full lake build is green from the Theorems.lean axiom gates. Tests: the supported-edge and underestimate witnesses re-mined for the new envelope, a k = 65 high-fraction never-over witness added, and the boundary-monotonicity loop extended through the k = 66 seam; 12/12 at 10k fuzz runs; forge fmt clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The closing constants share one binding: c0 carries the odd chain's constant term and the even chain's stage doubles it in place with shl(0x01, c0), making Ev(0) = 2*Od(0) visible in the source instead of split across two opaque literals. Semantics, tests, witnesses, and every certified budget are unchanged; runtime gas and deployed bytecode remain with the optimizer, whose constant folding materializes the doubled literal as before. The unoptimized Yul the proof anchors to carries the binding and the shift verbatim, so the eight quoted value walks mirror the compiled form (evmShl 0x1 c0 at the even closing, the same treatment the walks give the k-extraction's shl) and an evaluation lemma discharges the doubling where the walk trees meet the unchanged hand normal forms. Full lake build is green from the Theorems.lean axiom gates; 12/12 forge tests at 10k fuzz runs; forge fmt clean. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The measure/attribute/rebalance section gains its converse: the five instruments that drive a "leave it alone" answer to an exact floor (constrained-ideal fitting, the coefficient-count decay law, lattice search under the floored-and-margined objective, linear certificate-floor solves, and sweep suprema as lower bounds), with lnWadToRay as the worked example. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
duncancmt
force-pushed
the
dcmt/exp
branch
2 times, most recently
from
July 7, 2026 11:56
7bb1f1b to
d04c7e9
Compare
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.