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

.github/workflows/cbrt-formal.yml

@@ -0,0 +1,66 @@
+name: Cbrt.sol Formal Check
+
+on:
+  push:
+    branches:
+      - master
+    paths:
+      - src/vendor/Cbrt.sol
+      - src/wrappers/CbrtWrapper.sol
+      - formal/cbrt/**
+      - formal/yul_to_lean.py
+      - test/0.8.25/Cbrt.t.sol
+      - test/0.8.25/formal-model/CbrtModel.t.sol
+      - .github/workflows/cbrt-formal.yml
+  pull_request:
+    paths:
+      - src/vendor/Cbrt.sol
+      - src/wrappers/CbrtWrapper.sol
+      - formal/cbrt/**
+      - formal/yul_to_lean.py
+      - test/0.8.25/Cbrt.t.sol
+      - test/0.8.25/formal-model/CbrtModel.t.sol
+      - .github/workflows/cbrt-formal.yml
+
+jobs:
+  cbrt-formal:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
+      - name: Install Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.11"
+
+      - name: Install Lean toolchain
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Generate Lean model from Cbrt.sol via Yul IR
+        run: |
+          forge inspect src/wrappers/CbrtWrapper.sol:CbrtWrapper ir | \
+            python3 -W error formal/cbrt/generate_cbrt_model.py \
+              --yul - \
+              --output formal/cbrt/CbrtProof/CbrtProof/GeneratedCbrtModel.lean
+
+      - name: Generate finite certificate from cbrt spec
+        run: |
+          python3 formal/cbrt/generate_cbrt_cert.py \
+            --output formal/cbrt/CbrtProof/CbrtProof/FiniteCert.lean
+
+      - name: Build Cbrt proof and model evaluator
+        working-directory: formal/cbrt/CbrtProof
+        run: lake build && lake build cbrt-model
+
+      - name: Fuzz-test Lean model against Solidity
+        run: |
+          FOUNDRY_PROFILE=formal-model forge test \
+            --skip 'src/*' --skip 'test/unit/*' --skip 'test/integration/*' --skip 'test/0.8.28/*' \
+            --match-contract CbrtModelTest

.github/workflows/sqrt-formal.yml

@@ -0,0 +1,66 @@
+name: Sqrt.sol Formal Check
+
+on:
+  push:
+    branches:
+      - master
+    paths:
+      - src/vendor/Sqrt.sol
+      - src/wrappers/SqrtWrapper.sol
+      - formal/sqrt/**
+      - formal/yul_to_lean.py
+      - test/0.8.25/Sqrt.t.sol
+      - test/0.8.25/formal-model/SqrtModel.t.sol
+      - .github/workflows/sqrt-formal.yml
+  pull_request:
+    paths:
+      - src/vendor/Sqrt.sol
+      - src/wrappers/SqrtWrapper.sol
+      - formal/sqrt/**
+      - formal/yul_to_lean.py
+      - test/0.8.25/Sqrt.t.sol
+      - test/0.8.25/formal-model/SqrtModel.t.sol
+      - .github/workflows/sqrt-formal.yml
+
+jobs:
+  sqrt-formal:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
+      - name: Install Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.11"
+
+      - name: Install Lean toolchain
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Generate Lean model from Sqrt.sol via Yul IR
+        run: |
+          forge inspect src/wrappers/SqrtWrapper.sol:SqrtWrapper ir | \
+            python3 -W error formal/sqrt/generate_sqrt_model.py \
+              --yul - \
+              --output formal/sqrt/SqrtProof/SqrtProof/GeneratedSqrtModel.lean
+
+      - name: Generate finite certificate from sqrt spec
+        run: |
+          python3 formal/sqrt/generate_sqrt_cert.py \
+            --output formal/sqrt/SqrtProof/SqrtProof/FiniteCert.lean
+
+      - name: Build Sqrt proof and model evaluator
+        working-directory: formal/sqrt/SqrtProof
+        run: lake build && lake build sqrt-model
+
+      - name: Fuzz-test Lean model against Solidity
+        run: |
+          FOUNDRY_PROFILE=formal-model forge test \
+            --skip 'src/*' --skip 'test/unit/*' --skip 'test/integration/*' --skip 'test/0.8.28/*' \
+            --match-contract SqrtModelTest

.github/workflows/sqrt512-formal.yml

@@ -0,0 +1,65 @@
+name: 512Math._sqrt Formal Check
+
+on:
+  push:
+    branches:
+      - master
+    paths:
+      - src/utils/512Math.sol
+      - src/wrappers/Sqrt512Wrapper.sol
+      - formal/sqrt/**
+      - formal/yul_to_lean.py
+      - test/0.8.25/formal-model/Sqrt512Model.t.sol
+      - .github/workflows/sqrt512-formal.yml
+  pull_request:
+    paths:
+      - src/utils/512Math.sol
+      - src/wrappers/Sqrt512Wrapper.sol
+      - formal/sqrt/**
+      - formal/yul_to_lean.py
+      - test/0.8.25/formal-model/Sqrt512Model.t.sol
+      - .github/workflows/sqrt512-formal.yml
+
+jobs:
+  sqrt512-formal:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
+      - name: Install Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.11"
+
+      - name: Install Lean toolchain
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Generate Lean model from 512Math._sqrt via Yul IR
+        run: |
+          FOUNDRY_SOLC_VERSION=0.8.33 \
+            forge inspect src/wrappers/Sqrt512Wrapper.sol:Sqrt512Wrapper ir | \
+            python3 -W error formal/sqrt/generate_sqrt512_model.py \
+              --yul - \
+              --output formal/sqrt/Sqrt512Proof/Sqrt512Proof/GeneratedSqrt512Model.lean
+
+      - name: Generate finite certificate from sqrt spec
+        run: |
+          python3 formal/sqrt/generate_sqrt_cert.py \
+            --output formal/sqrt/SqrtProof/SqrtProof/FiniteCert.lean
+
+      - name: Build Sqrt512 proof and model evaluator
+        working-directory: formal/sqrt/Sqrt512Proof
+        run: lake build && lake build sqrt512-model
+
+      - name: Fuzz-test Lean model against Solidity
+        run: |
+          FOUNDRY_PROFILE=formal-model forge test \
+            --skip 'src/*' --skip 'test/unit/*' --skip 'test/integration/*' --skip 'test/0.8.28/*' \
+            --match-contract Sqrt512ModelTest

.gitignore

@@ -30,3 +30,6 @@ node_modules
 
 # user-specific local configuration
 /config/
+
+# Python bytecode cache directories
+__pycache__/

formal/README.md

@@ -0,0 +1,53 @@
+# Formal Verification
+
+Machine-checked Lean 4 correctness proofs for root math libraries in 0x Settler. Zero `sorry`, no axioms beyond the Lean kernel.
+
+## Scope
+
+| Proof | Solidity source | What is proved |
+|-------|----------------|----------------|
+| `sqrt/SqrtProof` | `src/vendor/Sqrt.sol` | `_sqrt`, `sqrt`, `sqrtUp` correct on uint256 |
+| `sqrt/Sqrt512Proof` | `src/utils/512Math.sol` | `_sqrt` (512-bit) correct: `sqrt(x_hi * 2^256 + x_lo) = natSqrt(x)` |
+| `cbrt/CbrtProof` | `src/vendor/Cbrt.sol` | `_cbrt`, `cbrt`, `cbrtUp` correct on uint256 |
+
+## Method
+
+1. **Algebraic lemmas** prove one-step safety and correction logic (Babylonian / Newton-Raphson steps).
+2. **Finite domain certificates** (auto-generated by Python scripts) cover all uint256 octaves with `by decide` proofs.
+3. **Solidity-to-Lean generators** parse Yul IR into EVM-faithful and normalized Lean models.
+4. **End-to-end bridge theorems** prove the generated EVM models equal the hand-written mathematical specs.
+
+## Build
+
+All auto-generated files (`GeneratedSqrtModel.lean`, `FiniteCert.lean`, etc.) are `.gitignore`d and regenerated in CI. See `.github/workflows/sqrt-formal.yml`, `sqrt512-formal.yml`, and `cbrt-formal.yml` for the canonical build steps.
+
+```bash
+# --- 256-bit sqrt ---
+forge inspect src/wrappers/SqrtWrapper.sol:SqrtWrapper ir | \
+  python3 formal/sqrt/generate_sqrt_model.py --yul - \
+    --output formal/sqrt/SqrtProof/SqrtProof/GeneratedSqrtModel.lean
+
+python3 formal/sqrt/generate_sqrt_cert.py \
+  --output formal/sqrt/SqrtProof/SqrtProof/FiniteCert.lean
+
+cd formal/sqrt/SqrtProof && lake build
+
+# --- 512-bit sqrt ---
+FOUNDRY_SOLC_VERSION=0.8.33 \
+  forge inspect src/wrappers/Sqrt512Wrapper.sol:Sqrt512Wrapper ir | \
+  python3 formal/sqrt/generate_sqrt512_model.py --yul - \
+    --output formal/sqrt/Sqrt512Proof/Sqrt512Proof/GeneratedSqrt512Model.lean
+
+# FiniteCert.lean (shared with SqrtProof) must be generated first — see above.
+cd formal/sqrt/Sqrt512Proof && lake build
+
+# --- cbrt ---
+forge inspect src/wrappers/CbrtWrapper.sol:CbrtWrapper ir | \
+  python3 formal/cbrt/generate_cbrt_model.py --yul - \
+    --output formal/cbrt/CbrtProof/CbrtProof/GeneratedCbrtModel.lean
+
+python3 formal/cbrt/generate_cbrt_cert.py \
+  --output formal/cbrt/CbrtProof/CbrtProof/FiniteCert.lean
+
+cd formal/cbrt/CbrtProof && lake build
+```

formal/cbrt/CbrtProof/.gitignore

@@ -0,0 +1,8 @@
+/.lake
+lake-manifest.json
+
+# Auto-generated from `formal/cbrt/generate_cbrt_cert.py`
+/CbrtProof/FiniteCert.lean
+
+# Auto-generated from `formal/cbrt/generate_cbrt_model.py`
+/CbrtProof/GeneratedCbrtModel.lean

formal/cbrt/CbrtProof/CbrtProof.lean

@@ -0,0 +1,10 @@
+-- This module serves as the root of the `CbrtProof` library.
+-- Import modules here that should be built as part of the library.
+import CbrtProof.FloorBound
+import CbrtProof.CbrtCorrect
+import CbrtProof.FiniteCert
+import CbrtProof.CertifiedChain
+import CbrtProof.Wiring
+import CbrtProof.OverflowSafety
+import CbrtProof.GeneratedCbrtModel
+import CbrtProof.GeneratedCbrtSpec