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

Open

duncancmt wants to merge 181 commits intodcmt/newton-raphson-optimizationfrom

dcmt/codex-prove-sqrt-cbrt

Commits on Feb 26, 2026

Commits on Feb 27, 2026

Merge remote-tracking branch 'origin/dcmt/codex-prove-sqrt-cbrt' into HEAD
duncancmt
committed
cbrt: add one-step arithmetic bridge lemmas and i8rt formalization
duncancmt
committed
Merge commit '5de93000' into HEAD
duncancmt
committed
formal/cbrt: add arithmetic bridge scaffolding for cbrt upper bound
duncancmt
committed
Merge commit 'faab29a7' into HEAD
duncancmt
committed
formal/cbrt: prove stage contraction bridge side conditions
duncancmt
committed
Merge commit '1280853a' into HEAD
duncancmt
committed
formal/cbrt: close upper-bound gap with finite certificate proof

duncancmt
and
claude
committed
formal/cbrt: add CI workflow and update README

duncancmt
and
claude
committed
formal/cbrt: bridge auto-generated Cbrt.sol model to verified spec

duncancmt
and
claude
committed
Cleanup
duncancmt
committed
formal/cbrt: replace native_decide with decide

duncancmt
and
claude
committed
formal(cbrt): replace grind proofs in CbrtCorrect
duncancmt
committed
formal(cbrt): avoid Nat.pow_lt_pow_right in two_pow_lt_word
duncancmt
committed
formal(cbrt): remove Classical.choice from cbrtUp proofs
duncancmt
committed
formal/cbrt: prove cbrtUp gives exact ceiling cube root

duncancmt
and
claude
committed
Merge commit 'b78e0d6b' into HEAD
duncancmt
committed
formal/cbrt: eliminate native_decide from cbrtUp proof path

duncancmt
and
claude
committed
formal/cbrt: eliminate Classical.choice by replacing grind with polynomial expansion

duncancmt
and
claude
committed
formal/cbrt: remove dead proof apparatus and placeholder file

duncancmt
and
claude
committed
formal/cbrt: deduplicate 5-step error chain, add cbrtUp(0) coverage

duncancmt
and
claude
committed
Merge branch 'dcmt/newton-raphson-optimization' into dcmt/codex-prove-sqrt-cbrt
duncancmt
committed
formal/cbrt: prove overflow safety for new cbrtUp implementation

duncancmt
and
claude
committed
formal/cbrt: replace native_decide with decide in OverflowSafety

duncancmt
and
claude
committed
formal/cbrt: remove uint256 bound from Nat-level seed and model theorems

duncancmt
and
claude
committed

Commits on Feb 28, 2026

Commits on Mar 1, 2026

Commits on Mar 3, 2026

Commits on Mar 4, 2026

Commits on Mar 5, 2026

Commits on Mar 6, 2026

Commits on Mar 7, 2026