Port highly-optimized sqrt and cbrt from Solady and 0x-Settler - #6
Merged
Conversation
Add a shared `clz` helper using the de Bruijn trick
Add clz, sqrt, and cbrt proofs that connect the Verity equations to the mathematical specifications for the optimized implementations. Co-Authored-By: Codex <codex@openai.com>
Compute the final sqrt and cbrt correction by subtracting the comparison flag directly from the Newton estimate. Co-Authored-By: Codex <codex@openai.com>
Update the sqrt and cbrt correctness proofs for the flag-subtraction correction and keep the cbrt small-range bridge over the generated Verity execution path. Co-Authored-By: Codex <codex@openai.com>
Restructure the proof suites into parallel Sqrt/ and Cbrt/ directories
with consistent naming: Model, FloorBound, Contraction, OctaveCert,
ErrorChain, Wiring, Correctness (+ OverflowSafety for cbrt).
Key changes:
- Rename bstep -> sqrtStep, babylon_step_floor_bound -> sqrt_step_floor_bound
- Consistent namespaces: Sqrt.{File} / Cbrt.{File} everywhere
- Split monolithic SqrtCorrect (375L) and CbrtCorrect (747L) into focused modules
- Remove ~335 lines of dead code: StepMono, SmallRange, Sqrt512Cert,
perfect-cube exactness, unused bracket/witness wrappers, cbrt run6From
- Add Sqrt and Cbrt lean_libs to lakefile.toml
- Update FixedPointMathLibProof consumer imports and identifiers
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Remove an unused proof option, correct the cbrt wiring module comment, and fix proof file whitespace. Co-Authored-By: Codex <codex@openai.com>
Export clz through the FixedPointMathLib helper namespace, add its spec/proof/test/generated surface, and move Sqrt/Cbrt proof modules under Tamago.Proof.Utils. Co-Authored-By: Codex <codex@openai.com>
duncancmt
force-pushed
the
dcmt/golf-roots
branch
from
May 14, 2026 10:33
ee94de5 to
1e941db
Compare
Co-Authored-By: OpenAI Codex <codex@openai.com>
duncancmt
force-pushed
the
dcmt/golf-roots
branch
from
May 16, 2026 18:06
b2eba2e to
da198fa
Compare
Co-Authored-By: atarpara <akpatel0618@gmail.com>
Co-Authored-By: Codex <codex@openai.com>
Co-Authored-By: atarpara <akpatel0618@gmail.com>
Co-Authored-By: Codex <codex@openai.com>
Co-Authored-By: Codex <codex@openai.com>
Co-Authored-By: Codex <codex@openai.com>
Co-Authored-By: Codex <codex@openai.com>
Contributor
|
Looks great, appreciate this PR! CI is failing because |
The Verity pin bump surfaces WETH's withdraw/internal_withdraw reads of SELFBALANCE as a partially modeled runtime introspection surface, which `tama audit` rejects unless declared. Add `selfBalance` to [trust.allow_surfaces] to keep the trust boundary explicit. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`tama.lock` tracks a SHA-256 of `tama.toml` under [inputs]. Adding the [trust.allow_surfaces] section changed that hash, so the lock was stale and CI's `git diff --exit-code -- tama.lock ...` guard failed. Update the tracked hash to match. Co-Authored-By: Claude Opus 4.7 (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.
Vectorized/solady#1515 , Vectorized/solady#1523 , and Vectorized/solady#1527 implement highly-optimized
sqrtandcbrtroutines. 0xProject/0x-settler#511 includes a Lean proof of correctness for that implementation. Port both the implementation and the proof into Tamago. Commit messages correctly attribute which changes were produced with AI assistance (porting the proof) and which are "meatbag" changes (porting the implementation).The implementation of these optimized routines requires
clz, which is not implemented in Verity. Accordingly, the optimized, pre-Osakaclzimplementation using the de Bruijn table trick has also been ported to Verity. Obviously, this can be removed quite simply once support forclzarrives in Verity.