Formally verified `expRayToWad` - #593

Open

duncancmt wants to merge 153 commits into

dcmt/formal-nopythonfrom

Commits on Jun 28, 2026

Add Exp.expRayToWad, the native-range inverse of lnWadToRay

duncancmt
and
claude
committed
89e12f6
AGENTS.md: assembly and tooling conventions

duncancmt
and
claude
committed
6b48449
Optimize the Exp range reduction to a Q128 ln2 basis

committed
2c5976f
Size the Exp margin to cover the range-reduction bias; never overestimate

duncancmt
and
claude
committed
1b06007
Carry ln2 in one wide word; shrink the Exp margin 8x

duncancmt
and
claude
committed
77c7798

Commits on Jun 29, 2026

Scaffold the expRayToWad EVMYulLean proof: importer exp kind + package

committed
397d852
Add reusable exp seam word-lemmas, overflow-guard, and revert reduction

committed
8c58232
Prove fun_expRayToWad_70 reverts above the supported range

committed
7a6e397
Parametrize the exp 70-revert by fuel slack and add the wrapper revert

committed
e9b89eb
Prove expRayToWad reverts above the supported range

committed
30c3f75
Add exp-formal CI pass and axiom-gated Theorems signpost

committed
c5f0dc1
Reduce the exp value-path functions at the scale point x=0

committed
2a43c71
Add branch-agnostic allocate/abi_encode directs for the exp value .ok path

committed
50ab83c
Prove expRayToWad(0) = 1e18

committed
c6e1751
Prove the wordNat_slt bridge for the general exp kernel reduction

committed
0d1618f
Reduce the general exp kernel to the evm* tree (symbolic x)

committed
8c7ca7d
Add the slt_thresh_lt guard-skip sibling for the exp value path

duncancmt
and
claude
committed
568099f
Prove the exp value-path function chain returns the evm* tree (symbolic x)

duncancmt
and
claude
committed
3a07533
Reduce the exp run-level value path to the evm* tree

committed
2a70ec2
Add the word-level transport foundation for exp monotonicity (Mono/WordMono)

duncancmt
and
claude
committed
6c43f9c
Add the exp layered tree definition and run-level bridge (Mono/Tree, Mono/RunBridge)

duncancmt
and
claude
committed
d90527e
Add the exp clamp/pin shell decomposition (Mono/Shell, Mono/ShellOn)

duncancmt
and
claude
committed
5900f7e
Reduce top-level exp monotonicity to the region analytic core (Mono/Top)

committed
6b913b5
Add the exp octave-index transport and its monotonicity (Mono/Octave)

duncancmt
and
claude
committed
acfea23
Add the exp k bound and reduced-argument transport (Mono/Octave)

duncancmt
and
claude
committed
3b835eb
Prove within-octave reduced-argument monotonicity (Mono/Octave)

duncancmt
and
claude
committed
002b79b
Add the Mono facade and the Theorems gate entry for monotonicity

committed
fa4903c
Port cert Foundation (Poly) and exp Horner-stage transports

committed
4b46b76
Add quotient-stage transports for the exp kernel (tod, num/den, r0)

committed
d4486b9
Discharge RegionMonotonicityFacts range and nonneg obligations

committed
dc95959
Reduce same-octave r0 monotonicity to the tod*ev cross inequality

committed
cb2c588
Add per-stage Lipschitz bound for the exp Horner accumulators

duncancmt
and
claude
committed
daad001
Add reduced/squared-argument step gaps for adjacent same-octave inputs

duncancmt
and
claude
committed
e86f5bf
Add composed Lipschitz bounds for the exp even/odd accumulators

duncancmt
and
claude
committed
e71fca9
Prove the same-octave cross inequality tod1*ev2 <= tod2*ev1

duncancmt
and
claude
committed
fc50b86
Prove the within-octave adjacent r0/r1 monotone step

duncancmt
and
claude
committed
5d1140d
Lift the adjacent step to region monotonicity of r1Tree

committed
88db2c7
Reduce RegionMonotonicityFacts to the octave-seam step

committed
26ea25f
Reduce the octave-seam step to the r0 doubling bound

duncancmt
and
claude
committed
2715aa0
Reduce runtime monotonicity to the single seam r0 doubling bound

committed
37e41ef
Add `Common` package: shared function-agnostic proof machinery

duncancmt
and
claude
committed
62539d2
Repoint `LnProof` at the shared `Common` package

duncancmt
and
claude
committed
725153c
Extract shared EVM-word lemmas to `Common.Word`; repoint `ExpProof`

duncancmt
and
claude
committed
71f949f
CI: build `Common` in the ln/exp formal checks

duncancmt
and
claude
committed
aacceb5
Add expRayToWad Real.exp floor-bracket spec

committed
1a400a6
Add expRayToWad real-free Nat cut predicates

committed
c9893d3
Add expRayToWad real bridge from cuts and accumulator to floor brackets

committed
21c1e1a
Add exp reduced-argument Taylor cut cert generator and symbolic defs

committed
ca4c0c7
Add exp reduced-argument Taylor cap bridge (Floor/Caps.lean)

committed
3a79e2d
Regenerate + verify exp cut certs in CI

duncancmt
and
claude
committed
f9b201e
Add exp floor brackets and worst-case comment

committed
d4f4946
Reduce the exp accumulator bound to the octave-folded r0 bound

committed
e02a358
Prove the exp reduced argument stays in the cert domain [-H128, H128]

duncancmt
and
claude
committed
1f91ade
Fix exp floor-bracket spec to target the signed input value

committed
a0e2a25
Prove the exp below-clamp target bound (RuntimeR0Bound.belowC)

committed
deb104b
Add the exp even-Horner truncation bridge (RuntimeR0Bound gap-2, even half)

duncancmt
and
claude
committed
b04d64c
Add the exp odd-Horner truncation bridge (RuntimeR0Bound gap-2, odd half)

duncancmt
and
claude
committed
59ff19b
Wire the discharged RuntimeR0Bound ingredients into the exp gate

duncancmt
and
claude
committed
0c91cad
Add the exp v-form Taylor cert for RuntimeR0Bound

committed
a7d05fe
Add the exp reduced-argument real bound (RuntimeR0Bound gap-1)

committed
4658fa1
Add the exp v-truncation cert-polynomial bridge (RuntimeR0Bound, even half)

duncancmt
and
claude
committed
8289fe5
Add the exp odd/tod/num/den cert brackets and the sdiv floor sandwich

duncancmt
and
claude
committed
5a28eb6
Tighten exp v-form cert margins to 2^-130 and gap-1 to 9/(8*2^128)

committed
879cf4f
Tighten the exp tod cert bracket to 4*2^1193

duncancmt
and
claude
committed
bfee642
Add the exp r0-vs-cert-rational bracket (RuntimeR0Bound/SeamR0Bound)

duncancmt
and
claude
committed
5889df8
Add the exp octave-fold target identity, cert real bounds, and loose per-point over

duncancmt
and
claude
committed
2c1bc43
Add the exp loose per-point deficit bound (nonnegative half)

duncancmt
and
claude
committed
d1485c0
Add the exp negative-half integer brackets and reciprocal symmetry

duncancmt
and
claude
committed
f1fe987
Add the exp negative-half and combined per-point real bounds

duncancmt
and
claude
committed
373ac16
Discharge SeamR0Bound for runtime monotonicity

committed
13cd65d
Use le_or_gt in the exp per-point sign split (drop deprecated le_or_lt)

duncancmt
and
claude
committed
7503a4a
Add the exp fractional gap-2 telescoping

committed
e06806f
Tighten the exp v-step bound to feed the joint over budget

duncancmt
and
claude
committed
2b0a9cf
Prove the exp joint per-point never-over (nonneg half) within the margin

committed
8ab5c66
Prove the exp joint never-over on the negative half

committed
e6188b2
Add the exp per-point deficit (under) brackets, both signs

duncancmt
and
claude
committed
8414069
Make exp global floor brackets hypothesis-free; reduce central exact floor to central exactness

committed
5d32b5a

Commits on Jun 30, 2026

Speed up the Floor/R0Exp.lean compile

duncancmt
and
claude
committed
b0c1fd6
Split the deficit side into Floor/R0ExpUnder.lean

committed
874a1b8
Speed up the over-side R0Exp tactics

duncancmt
and
claude
committed
25d16a3
Wire LnProof into the exp proof package for the round-trip

committed
717d0d8
Prove the expRayToWad/lnWadToRay round trip

committed
58fe2b6
Switch the exp cert pipeline to the v-form and restate the round trip

committed
5481ffa
Tighten planning-reference guidance and block new markdown files

duncancmt
and
codex
committed
c72c6a1
Tighten expRayToWad margin to the proof's decomposition floor

committed
f8dcb07
Tighten the proven maximum-underestimation bound for expRayToWad

committed
5ffd01e
Remove the expRayToWad fuzz tests

committed
52b42f3
Align exp formal CI and documentation

duncancmt
and
codex
committed
d104590
Strengthen exp clamp boundary proof

duncancmt
and
codex
committed
374cc75

Commits on Jul 1, 2026

Align the Exp.sol error-budget comment with the proofs

duncancmt
and
claude
committed
c23a4c1
Cover the exp edges, the 1-ulp witness, and oracle-free fuzz

duncancmt
and
claude
committed
acaef48
Re-run the exp proof on all its inputs; share the LnProof pipeline

duncancmt
and
claude
committed
73ae66e
Prune the dead exp proof pathway; signpost the unconditional surface

duncancmt
and
claude
committed
0c7f13a
State the exp proof comments in current terms

duncancmt
and
claude
committed
1ece210

Commits on Jul 2, 2026

Delete pyproject.toml
duncancmt
committed
5eae57f
WIP: clean up slop
duncancmt
committed
e7a0d6d
WIP: clean up slop
duncancmt
committed
29f469d
WIP: clean up slop
duncancmt
committed
f6049d0
WIP: clean up slop
duncancmt
committed
e3b45ef
WIP: clean up slop
duncancmt
committed
b26ab44
WIP: clean up slop
duncancmt
committed
2b85d70
WIP: clean up slop
duncancmt
committed
51a0ca9
WIP: clean up slop
duncancmt
committed
e444a7d
WIP: clean up slop
duncancmt
committed
5a6a6a3
WIP: clean up slop
duncancmt
committed
1276222
Fix missing CI trigger
duncancmt
committed
4f61b03
WIP: clean up slop
duncancmt
committed
e35bb61
Homogenize
duncancmt
committed
05ecaf1
Share the formal CI toolchain setup across the proof workflows

duncancmt
and
claude
committed
742f170
Add exact-floor witnesses across the exp negative octaves

duncancmt
and
claude
committed
9d7cad5
Refer to src/wrappers/ in AGENTS.md
duncancmt
committed
3531403
WIP: clean up slop
duncancmt
committed
cfdaa93
Carry v at Q123 so the exp monic stage is a bare add

duncancmt
and
claude
committed
46d670e
Carry the exp rational at full staircase precision; tighten the margin

duncancmt
and
claude
committed
0429f66
Document the fixed-point rational coefficient derivation pipeline

duncancmt
and
claude
committed
bc6b64e
WIP: clean up slop
duncancmt
committed
d5d72ca
Set the exp margin at the certifiable granularity envelope

duncancmt
and
claude
committed
32120e5
State the exact Ln bias margin

duncancmt
and
claude
committed
053090f
WIP: clean up slop
duncancmt
committed
5d22714
WIP: clean up slop
duncancmt
committed
456f1f0
WIP: clean up slop
duncancmt
committed
28802d2
Re-derive the exp proof for the Q123 kernel

duncancmt
and
claude
committed
51b4b79
Fold the exp output on the 5^18 grid; unsigned close; 32-piece margin

duncancmt
and
claude
committed
2ecccca
Certify the 5^18 fold, unsigned close, and 32-piece granularity

duncancmt
and
claude
committed
8efdde5
Merge fable/exp into dcmt/exp
duncancmt
committed
7e3577f
Cleanup
duncancmt
committed
1cbda8f
Notation
duncancmt
committed
e1b5dca
Post-merge cleanup
duncancmt
committed
1773fb9
Anchor the Ln runtime model to the Solidity-level guard

duncancmt
and
claude
committed
cc34ee4
Formatting
duncancmt
committed
542bb55
Style
duncancmt
committed
431f33b
Request the Yul IR from every compile in generate_from_forge.sh

duncancmt
and
claude
committed
384f015
Share the exp granularity piece table between the generator and the proof

duncancmt
and
claude
committed
3891092
Merge fable/exp into dcmt/exp
duncancmt
committed
3d3818c
Share the cover-certificate generator helpers in Common.GenCover

duncancmt
and
claude
committed
ed10526
Renumber the exp Seam reductions to the current compiled Yul

duncancmt
and
claude
committed
f2ecd31
Remove dead hypotheses, no-op tactics, and unused simp arguments

duncancmt
and
claude
committed
e82bfdf
Deduplicate the word-level proof machinery into Common.Word

duncancmt
and
claude
committed
7f13c76

Commits on Jul 3, 2026

Carry ev at Q88 and Od at Q89; tighten the margin to the new envelope

duncancmt
and
claude
committed
9b7d589
Refit the exp coefficients on the Q88/Q89 grids; halve the cut nudge

duncancmt
and
claude
committed
2001290
Comment style; clarity
duncancmt
committed
e24c696
Formatting
duncancmt
committed
8b3045d
Extend the supported exp range through the k = 64 octave

duncancmt
and
claude
committed
2505893
Merge fable/exp into dcmt/exp
duncancmt
committed
0341b5b
Write the clamp constant as a negation

duncancmt
and
claude
committed
7c732dc
Merge fable/exp into dcmt/exp
duncancmt
committed
13a4ca9
Fix comment
duncancmt
committed
48e3f29

Commits on Jul 4, 2026

Fold the exp output scale into the closing division; rebase CINV to 2^192

duncancmt
and
claude
committed
007cbee

Commits on Jul 5, 2026

Extend the supported exp range through the k = 65 octave

duncancmt
and
claude
committed
66aea3a
Express the even closing constant as the doubled odd constant

duncancmt
and
claude
committed
b5fe25a
Document settling negatives with the envelope instruments

duncancmt
and
claude
committed
e99a89a

Commits on Jul 7, 2026

Add decision-making discipline to the development guide

duncancmt
and
claude
committed
1712174
Clean up comments
duncancmt
committed
45cc47f