Formally prove the correctness of Sqrt.sol and Cbrt.sol #29
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
| name: 512Math cbrt Formal Check | |
| on: | |
| push: | |
| branches: | |
| - master | |
| paths: | |
| - src/utils/512Math.sol | |
| - src/vendor/Cbrt.sol | |
| - src/wrappers/CbrtWrapper.sol | |
| - src/wrappers/Cbrt512Wrapper.sol | |
| - formal/cbrt/** | |
| - formal/yul_to_lean.py | |
| - test/0.8.25/formal-model/FormalModelFFI.t.sol | |
| - test/0.8.25/formal-model/Cbrt512Model.t.sol | |
| - .github/workflows/cbrt512-formal.yml | |
| pull_request: | |
| paths: | |
| - src/utils/512Math.sol | |
| - src/vendor/Cbrt.sol | |
| - src/wrappers/CbrtWrapper.sol | |
| - src/wrappers/Cbrt512Wrapper.sol | |
| - formal/cbrt/** | |
| - formal/yul_to_lean.py | |
| - test/0.8.25/formal-model/FormalModelFFI.t.sol | |
| - test/0.8.25/formal-model/Cbrt512Model.t.sol | |
| - .github/workflows/cbrt512-formal.yml | |
| jobs: | |
| cbrt512-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 pinned Lean toolchain | |
| run: | | |
| curl https://raw.githubusercontent.com/leanprover/elan/917c18d0ad52f649c2603dc8b973f5b9fa5f8f43/elan-init.sh -sSf | sh -s -- -y --default-toolchain none | |
| echo "$HOME/.elan/bin" >> "$GITHUB_PATH" | |
| LEAN_TOOLCHAIN="$(cat formal/cbrt/Cbrt512Proof/lean-toolchain)" | |
| test "$LEAN_TOOLCHAIN" = "$(cat formal/cbrt/CbrtProof/lean-toolchain)" | |
| "$HOME/.elan/bin/elan" toolchain install "$LEAN_TOOLCHAIN" | |
| "$HOME/.elan/bin/elan" default "$LEAN_TOOLCHAIN" | |
| - name: Generate 256-bit Lean model (CbrtProof dependency) | |
| 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: Generate 512-bit Lean model from Cbrt512Wrapper via Yul IR | |
| run: | | |
| FOUNDRY_SOLC_VERSION=0.8.33 \ | |
| forge inspect src/wrappers/Cbrt512Wrapper.sol:Cbrt512Wrapper ir | \ | |
| python3 -W error \ | |
| formal/cbrt/generate_cbrt512_model.py \ | |
| --yul - \ | |
| --output formal/cbrt/Cbrt512Proof/Cbrt512Proof/GeneratedCbrt512Model.lean | |
| - name: Build Cbrt512 proof and model evaluator | |
| working-directory: formal/cbrt/Cbrt512Proof | |
| run: lake build && lake build cbrt512-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 Cbrt512ModelTest |