Formally prove the correctness of Sqrt.sol and Cbrt.sol by duncancmt · Pull Request #511 · 0xProject/0x-settler

duncancmt · 2026-02-26T22:06:19Z

No description provided.

immunefi-magnus · 2026-02-27T17:29:42Z

🛡️ Immunefi PR Reviews

We 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:

🔗 Send this PR in for review

Once submitted, we'll take care of assigning a reviewer and follow up here.

_gensym("blk") produces _blk_N names that are valid Yul identifiers. User code can legitimately declare variables with the same pattern, causing "assigned 2 times" errors. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Add an `avoid` parameter to _gensym that skips counter values whose generated name appears in the given set. The bare-block handler passes all source identifier tokens (lazily collected via _all_source_names) so generated _blk_N names never collide with user-visible identifiers. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…licit Ite/Project IR nodes Multi-return projections and conditional expressions were encoded as fake Call names (`__component_N_M(...)`, `__ite(cond, t, f)`) decoded by regex at every consumption site. This made the IR fragile — a typo in a regex or a new traversal forgetting to special-case these names would silently miscompile. Add two new Expr node types (Ite, Project) to the union alongside IntLit, Var, Call. Update all 14 traversal functions, 3 creation sites, 5 consumption sites, and ~20 test locations. Semantics are identical; all 263 tests pass unchanged. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…nation Track expression-statements per-branch (on ParsedIfBlock) instead of per-function. When constant-folding proves a branch dead during inlining or model generation, its expr_stmts are silently discarded. Live or non-constant branches still reject expr_stmts as before. This enables the transpiler to handle Solidity's `/ 3` pattern where the compiler emits a divide-by-zero guard (`if iszero(y) { panic() }`) that becomes dead code when the divisor is a known non-zero constant. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Three bugs in a7e98d6 where branch expr_stmts were silently lost: 1. Bare-block scoping dropped ParsedIfBlocks that carried body_expr_stmts but had no outer-scope assignments. 2. _flatten_scoped_block reconstructed ParsedIfBlock without propagating body_expr_stmts / else_body_expr_stmts. 3. Constant-true if and constant-switch parse-time paths did not isolate _expr_stmts, so dead-branch expr_stmts leaked to function level and live-branch nested expr_stmts were lost. Root cause: the save/restore pattern for _expr_stmts was manually duplicated at each call site, making it easy to miss new sites. Fix: introduce _parse_scoped_body() that encapsulates the entire _expect("{") + save/restore + _parse_assignment_loop + _expect("}") pattern. All 6 branch-body parsing sites now use it. The bare-block emit check also considers branch expr_stmts. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

- Add assert_never() for exhaustive isinstance checks on Expr/RawStatement unions (_alpha_rename, _validate_expr_shape, _check_calls, _wrap_u256_literals) - Add assert narrowing for else_body before iteration in ELSE_LIVE paths - Fix dict key type in _has_live/_has_dead helpers (int, not str) - Rename shadowed variable (chosen_summary → switch_chosen, a → maybe_a) - Annotate ParsedIfBlock switch normalization locals (if_body, else_body, parsed_condition) to avoid type narrowing mismatch - Annotate rename_subst as dict[str, Expr] to satisfy substitute_expr variance - Extract assertEqual arguments to typed locals in test file to avoid list[Any]/set[Any] under disallow_any_expr Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Remove the two custom NoReturn helpers and use typing.assert_never at all exhaustive isinstance dispatch sites. This gives mypy a proper exhaustiveness check rather than a hand-rolled TypeError. Also remove the sole type: ignore comment by building a typed list[int] instead of filtering tuple[int | None, ...] in _try_const_eval, and add the missing explicit Var early-return there so the union is fully covered. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

_inline_yul_function was the only sequential statement processor that did not maintain a substitution map. When an intermediate variable was assigned a constant (e.g. `let expr_1 := cleanup(3)`) and then passed to a helper with branch expr_stmts (e.g. `wrapping_div(x, expr_1)`), the helper saw `Var('expr_1')` instead of `IntLit(3)`, making the branch condition non-constant and incorrectly rejecting the code. Add a `const_subst` dict that tracks variables assigned to compile-time-constant values: - Before inline_calls: substitute known constants into expressions - After inline_calls on PlainAssignment: record constant results, or remove the variable if the new value is non-constant - After ParsedIfBlock: invalidate conditionally-assigned variables Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

- Skip is_declaration assignments in definite-init analysis so branch- local `let` shadows don't suppress return variable zero-initialization - Preserve nested helpers that shadow a selected target's Yul name instead of dropping them from the helper table during fn_map cleanup - Reject negative IntLit values in validation (Yul integers are unsigned) - Reject negative Project indices (prevented Python negative-index wrap) - Reject Project of scalar calls: total < 2 in validate_function_model, builtin inner calls, and single-return models in validate_selected_models Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

The previous is_declaration check only skipped the `let` itself but not subsequent reassignments of the branch-local binding. Replace it with proper branch-local scope tracking (matching the existing pattern in _stmt_targets): declarations add to a branch_locals set, and only assignments to names NOT in that set count as outer-variable writes. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

1. _inline_yul_function: branch-local declarations that shadow outer variables were not respected — const_subst from the outer scope was applied blindly to all if/switch body expressions, causing branch-local reassignments to be overwritten by outer-scope values. Fixed by using per-branch copies of const_subst that track branch-local bindings. 2. Constant-folded switch: when the discriminant was constant the parser bypassed all shape validation, silently accepting missing-default and default-before-case forms. Added structural checks (require exactly 2 branches with a default, reject trailing branches after default). 3. evaluate_model_expr: IntLit values were returned without u256 wrapping, so out-of-range literals evaluated incorrectly. Fixed with % WORD_MOD. 4. emit_expr: IntLit values were stringified without u256 wrapping, so generated Lean code could contain out-of-range literals. Fixed with % WORD_MOD. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

The prior fix incorrectly enforced 'exactly 2 branches with a default' for constant-folded switches. Constant folding handles any valid Yul switch shape — it just selects the matching branch — so branch counts, missing defaults, and nonzero case values are all valid. The only structural check retained is that default must be the last branch, since the parser loop breaks on default and trailing branches would be silently dropped. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

The constant-fold switch path now validates three invariants that the previous too-lax fix missed: - Empty switches (no branches at all) are rejected - Non-constant case values are rejected — _try_const_eval returning None silently marked the branch as dead, which could drop a matching branch - Duplicate case values are rejected as ambiguous These checks are orthogonal to the shape constraints enforced on non-constant switches (case 0 + default only). The constant-fold path continues to accept nonzero case values, missing defaults, and any branch count, since it just selects the matching branch. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Use a compact three-entry fixed-point seed table so Cbrt converges in five Newton-Raphson iterations. Co-Authored-By: Codex <codex@openai.com>

Update the 256-bit Cbrt proof for the compact seed and five Newton-Raphson steps, and adjust the 512-bit wrapper bridges to the new inlined 256-bit model. Co-Authored-By: Codex <codex@openai.com>

Use post-Newton-optimal 8-bit seed multipliers and decode the compact table with BYTE. Co-Authored-By: Codex <codex@openai.com>

Use b = 255 − clz(x) = ⌊log₂(x)⌋ instead of y = 258 − clz(x). Since y = b + 3 and 3 ≡ 0 (mod 3), the octave index mod(b,3) = mod(y,3) is unchanged and div(b,3) = div(y,3) − 1, which is compensated by shifting shr from 8 to 7. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Co-Authored-By: Codex <codex@openai.com>

Each workflow now diffs the output of `#print axioms` against an exact expected string after building the proofs. If a `sorry` or custom axiom sneaks in, the diff fails immediately. Cbrt expected axioms verified locally. Sqrt expected axioms are best guesses from the proof structure and will be validated on first CI run. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

- sqrt proofs also use Classical.choice; update expected axiom strings - sqrtUp512_correct is top-level, not in Sqrt512Spec namespace - Redirect stderr into actual_axioms.txt so unknown-constant errors show up in the diff instead of silently passing - Fix mypy: rewrite_norm_ast was removed from generate_cbrt_model.py but test_yul_to_lean.py still imported it; define a local replacement Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

The tests now expect the faithful Nat translation (normSub, normClz) instead of a rewrite-based shortcut. Equivalence between the Nat model and the mathematical specification is proved in Lean, not papered over in the Python generator. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…instead of `div`

Co-Authored-By: Codex <codex@openai.com>

Co-Authored-By: OpenAI Codex <codex@openai.com>

Co-Authored-By: atarpara <akpatel0618@gmail.com>

Co-Authored-By: OpenAI Codex <codex@openai.com>

Co-Authored-By: atarpara <akpatel0618@gmail.com>

Co-Authored-By: Codex <codex@openai.com>

e1Ru1o · 2026-06-26T11:03:35Z

+      - src/wrappers/Sqrt512Wrapper.sol
+      - formal/sqrt/**
+      - formal/python/**
+      - test/0.8.25/formal-model/FormalModelFFI.t.sol
+      - test/0.8.25/formal-model/Sqrt512Model.t.sol
+      - .github/workflows/sqrt512-formal.yml
+  pull_request:
+    paths:
+      - src/utils/512Math.sol
+      - src/vendor/Sqrt.sol
+      - src/wrappers/Sqrt512Wrapper.sol


SqrtWrapper should be included as it is a dependency.

Suggested change

- src/wrappers/Sqrt512Wrapper.sol

- formal/sqrt/**

- formal/python/**

- test/0.8.25/formal-model/FormalModelFFI.t.sol

- test/0.8.25/formal-model/Sqrt512Model.t.sol

- .github/workflows/sqrt512-formal.yml

pull_request:

paths:

- src/utils/512Math.sol

- src/vendor/Sqrt.sol

- src/wrappers/Sqrt512Wrapper.sol

- src/wrappers/SqrtWrapper.sol

- src/wrappers/Sqrt512Wrapper.sol

- formal/sqrt/**

- formal/python/**

- test/0.8.25/formal-model/FormalModelFFI.t.sol

- test/0.8.25/formal-model/Sqrt512Model.t.sol

- .github/workflows/sqrt512-formal.yml

pull_request:

paths:

- src/utils/512Math.sol

- src/vendor/Sqrt.sol

- src/wrappers/SqrtWrapper.sol

- src/wrappers/Sqrt512Wrapper.sol

This is fixed in #591

e1Ru1o · 2026-06-26T11:56:43Z

It seems that this one got tracked before the gitignore was added.

yeah, this should be cleaned up by the time you get to #591

e1Ru1o · 2026-06-26T11:59:43Z

+import Init
+
+/-!
+Legacy symbolic certificate version (kept for reference).


are we keeping it?

e1Ru1o · 2026-06-26T17:44:33Z

+            '#print axioms Cbrt512Spec.model_cbrt512_evm_within_1ulp' \
+            '#print axioms Cbrt512Spec.model_cbrtUp512_wrapper_evm_correct' \


Maybe good to add the Cbrt512Spec.model_cbrt512_wrapper_evm_correct as well to the list of checked axioms depencies, technically to include the floor version of the cbrt512.

e1Ru1o · 2026-06-26T17:47:20Z

Might be good to add a test case that forces overflow in the operations, similar to how it is done in Sqrt.t.sol to make sure it is checked.

Optionally which might be even better, consider extracting the relevant sqrt and cbrt from Lib512MathTest into a separated contracts that you can inherit in Sqrt512Model using the same override trick in SqrtModel, that way we avoid code duplication and we get the overflow case that is already implemented there plus any other like the existing regression test.

All of it applies as well to Cbrt512Model.t.sol

duncancmt mentioned this pull request Feb 27, 2026

⚡️ Golf sqrt and cbrt by getting a better initial estimate and removing an iteration Vectorized/solady#1515

Merged

2 tasks

duncancmt marked this pull request as ready for review February 27, 2026 17:29

duncancmt requested a review from dekz as a code owner February 27, 2026 17:29

duncancmt requested a review from e1Ru1o February 27, 2026 22:40

duncancmt self-assigned this Feb 27, 2026

duncancmt force-pushed the dcmt/codex-prove-sqrt-cbrt branch from 66c27b4 to 9e9f388 Compare March 3, 2026 11:53

duncancmt and others added 23 commits March 12, 2026 22:03

chore: remove working plan files

1c79a12

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

test: cover branch expr stmt regressions

020dcbd

style: apply black formatting to formal/ Python files

7de4c54

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Simplify

b9ad46d

test: add yul-to-lean regression cases

6f5b5a5

test: cover branch-local return shadow reassignment bug

aa40220

fix: align branch read analysis with local scope

cb14078

test: add yul_to_lean regression coverage

0fbe42c

test: cover constant-switch parser regressions

06146f1

test: cover malformed constant-switch regressions

9e2918f

duncancmt and others added 15 commits April 14, 2026 11:47

Merge branch 'master' into dcmt/codex-prove-sqrt-cbrt

b06f081

Optimize Cbrt seed

29c0efe

Use a compact three-entry fixed-point seed table so Cbrt converges in five Newton-Raphson iterations. Co-Authored-By: Codex <codex@openai.com>

Prove optimized Cbrt seed

e19b30e

Update the 256-bit Cbrt proof for the compact seed and five Newton-Raphson steps, and adjust the 512-bit wrapper bridges to the new inlined 256-bit model. Co-Authored-By: Codex <codex@openai.com>

Clean up after AI

0657d5a

Require that AI agents add a Co-Authored-By: to each commit message

2948de3

Style

8499110

More AGENTS.md instructions for coauthorship

b7719c3

Optimize compact Cbrt seed table

432bfe0

Use post-Newton-optimal 8-bit seed multipliers and decode the compact table with BYTE. Co-Authored-By: Codex <codex@openai.com>

Cleaning up after AI

2577ae6

Update Cbrt proof for compact seed

7219797

Co-Authored-By: Codex <codex@openai.com>

Fix Cbrt512 wrapper byte bridge

e7a48ae

Co-Authored-By: Codex <codex@openai.com>

duncancmt mentioned this pull request May 12, 2026

⚡️ Golf cbrt by using a small table for an even better initial estimate and removing another iteration Vectorized/solady#1523

Merged

2 tasks

duncancmt and others added 3 commits May 12, 2026 19:31

Explicitly optimize the first Babylonian step of sqrt to use shr …

c87056c

…instead of `div`

Expose Sqrt first step strength reduction

d663a99

Co-Authored-By: Codex <codex@openai.com>

Merge codex/codex-prove-sqrt-cbrt into dcmt/codex-prove-sqrt-cbrt

4d8a0a0

duncancmt mentioned this pull request May 14, 2026

Port highly-optimized sqrt and cbrt from Solady and 0x-Settler Bacon-labs/tamago#6

Merged

Optimize cbrt further after Vectorized/solady#1527

f317ddc

duncancmt force-pushed the dcmt/codex-prove-sqrt-cbrt branch from f317ddc to 4d8a0a0 Compare May 16, 2026 16:57

duncancmt and others added 2 commits May 16, 2026 19:42

Repair cbrt seed constants

f97eabd

Co-Authored-By: OpenAI Codex <codex@openai.com>

Update cbrt proof seed model

c975e79

Co-Authored-By: OpenAI Codex <codex@openai.com>

duncancmt force-pushed the dcmt/codex-prove-sqrt-cbrt branch from f2aeed9 to c975e79 Compare May 16, 2026 17:43

duncancmt and others added 4 commits May 17, 2026 11:20

Apply further cbrt initial estimate optimization

8709477

Co-Authored-By: atarpara <akpatel0618@gmail.com>

Prove Solady cbrt initial estimate optimization

5152f98

Co-Authored-By: OpenAI Codex <codex@openai.com>

Tweak cbrt initialization constants for improved error bound

2266d22

Co-Authored-By: atarpara <akpatel0618@gmail.com>

Update cbrt proof for adjusted seed constants

09a4311

Co-Authored-By: Codex <codex@openai.com>

e1Ru1o reviewed Jun 26, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Formally prove the correctness of Sqrt.sol and Cbrt.sol#511

Formally prove the correctness of Sqrt.sol and Cbrt.sol#511
duncancmt wants to merge 573 commits into
dcmt/cbrt512from
dcmt/codex-prove-sqrt-cbrt

duncancmt commented Feb 26, 2026

Uh oh!

immunefi-magnus Bot commented Feb 27, 2026

Uh oh!

e1Ru1o Jun 26, 2026

Uh oh!

duncancmt Jun 26, 2026

Uh oh!

e1Ru1o Jun 26, 2026

Uh oh!

duncancmt Jun 26, 2026

Uh oh!

e1Ru1o Jun 26, 2026

Uh oh!

duncancmt Jun 26, 2026

Uh oh!

e1Ru1o Jun 26, 2026

Uh oh!

e1Ru1o Jun 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		'#print axioms Cbrt512Spec.model_cbrt512_evm_within_1ulp' \
		'#print axioms Cbrt512Spec.model_cbrtUp512_wrapper_evm_correct' \

Uh oh!

Conversation

duncancmt commented Feb 26, 2026

Uh oh!

immunefi-magnus Bot commented Feb 27, 2026

🛡️ Immunefi PR Reviews

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants