Formally verified mulExpRay - #599
Open
duncancmt wants to merge 122 commits into
Open
Conversation
Solidity `bool` may be any nonzero value for truthy when it enters an assembly block. This commit normalizes bool values at every site where they are used in arithmetic, bitwise operations, ABI encoding for external calls, or (transient) storage writes. Utility libraries (highest leverage — inlined throughout codebase): - Ternary: use iszero-inversion trick (single iszero, 3 gas) for ternary/maybeSwap; lt(0x00, c) for orZero - FastLogic.and: rewrite via De Morgan (was wrong: and(2,1)=0) - FastLogic.andNot: rewrite via gt(iszero(b), iszero(a)) - FastLogic.toUint, Math.toInt: normalize with lt(0x00, b) - UnsafeMath.unsafeInc/Dec(bool), Math.inc/dec: normalize with lt(0x00, b) External call encoding (mstore/mstore8/shl of bool): - EkuboV2, EkuboV3, MaverickV2, PancakeInfinity, UniswapV3Fork, FlashAccountingCommon, SafePermit, Hanji: wrap bool in lt(0x00, x) Transient storage: - CurveTricrypto: clean on write and read External callback data validation: - EkuboV2: revert with empty reason if bool > 1 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- FastLogic.andNot: use iszero(or(iszero(a), b)) — cleaner formulation - CurveTricrypto: remove redundant clean-on-read (write-side suffices) - CrossChainReceiverFactory: normalize bool immutable in mul (london EVM, uses iszero(iszero) since no PUSH0) - SettlerIntent.setSolver: normalize addNotRemove for xor/mul/sstore use - EulerSwap: validate bool from external staticcall returndata; normalize zeroForOne before shl - UniswapV2: normalize zeroForOne before shl in both getReserves and swap - FlashAccountingCommon, UniswapV3Fork: upgrade silent and(0x01,...) mask to reverting validation for callback bool data Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- FastLogic.and: mul(a, lt(0x00, b)) — cheaper than De Morgan (10 gas on Osaka vs 12; 11 on London vs 12) - FastLogic.andNot: mul(a, iszero(b)) — 8 gas, no PUSH0 needed - CrossChainReceiverFactory.deploy: normalize setOwnerNotCleanup bool before arithmetic use (iszero/iszero for London EVM) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…bility. Make 2 passes over `calls[]` to fix this.
Use the largest Q72 bias accepted by the 0.3383-ulp cap and keep the compiled runtime, floor bracket, error bound, and monotonicity proofs synchronized. Co-Authored-By: OpenAI Codex <codex@openai.com>
🛡️ Immunefi PR ReviewsWe 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: Once submitted, we'll take care of assigning a reviewer and follow up here. |
Model the generated mulExpRay conversion sequence in the Lean seam proof. Cache complete Lake package trees and reuse them across formal proof builds. Co-Authored-By: OpenAI Codex <codex@openai.com>
Sheriff is an Algebra Integral (v1.2.2) DEX on RobinHood chain (app.sheriff.exchange). Wire it as UniV3 fork ID 41: - New src/core/univ3forks/Sheriff.sol with the Algebra pool deployer (0x9ac30D72168a4498aE5C80226F4d3C86278e8f80), the Algebra Integral pool init code hash, and the fork ID constant. - Wire the fork into RobinHood's _uniV3ForkInfo using the Algebra swap callback (algebraSwapCallback). The Algebra salt (keccak256(abi.encode( token0, token1)), no fee/tickSpacing) is produced by the existing poolId==0 path in _toPool. - Add UNISWAPV3_FORKS.md and CHANGELOG.md entries. The init code hash was verified by recomputing the USDG/WETH pool address (0x536a7B19abB933bf6319e0b8817e733Bba166674) via CREATE2.
Use generated mixed interval-Horner/Kronecker and Bernstein cell certificates with variable-propagated Horner errors to certify the runtime core bound. Set the Solidity Q72 bias from the 0.3288640403604298097806-ulp bound, with reproducible formal generation and cache keys. Co-Authored-By: OpenAI Codex <codex@openai.com>
Align emitted-Yul seams with normalized boolean helpers and the shared int128 upcast. Co-Authored-By: OpenAI Codex <codex@openai.com>
Run cache actions on Node 24, pin workflow dependencies, suppress checkout initialization hints, and remove actionable Lean lints. Co-Authored-By: OpenAI Codex <codex@openai.com>
State the revert condition as one inequality in bitlen(|y|) and the octave index, with A-space never/always-revert thresholds as consequences. Round all doc approximations to 4 significant figures. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
mulExpRay computes the scale headroom as clz(ay) - (129 ^ (ay >> 127)). scaleShiftTree and its normal-form lemmas mirror the new word tree, the mulExpRay symbolic-execution reductions follow the emitted Yul's call sites and fuel positions, and the wrapping_add_t_uint256 reduction is removed along with the emitted function. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2 tasks
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
3 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.
No description provided.