Repository navigation
Pareto fidelity: signed Int256 storage reads (G28), ERC-20 hop lemmas (G14), kernel-eval scope (G2) - #2469
Merged
Conversation
…-20 hop lemmas (G14) - getStorage on an Int256 field binds an Int256 (ofUint256 of the word), so addPanic/subPanic on it resolve to the signed checked instance, matching the compilation model. Previously the word was Uint256 and Int256 operands were coerced, so int256 += with a negative operand panicked spuriously. - Core: hopCall_success_of_ne, hopCall_scoped_callee, hopCallView_getMapping, hopCallView_getMapping2. - Smoke: Int256 regression witnesses; Erc20BalanceHop (generated ERC-20 read and transfer through linked_contracts). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Contributor
| \n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
…moke state Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Th0rgal
marked this pull request as ready for review
October 5, 2026 12:15
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
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
1 participant
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.
Pareto fidelity gaps G28 / G14 / G2 (closure
pareto-credit-vault-proof-closure). Consumer notes: lfglabs-dev/pareto-credit-vault-proof-closure#36 (audit/pending/v-gaps.json).CI status: all checks green at
9422010693(2026-10-05). Verity main's latest "Verify proofs" run (98533b7) is also green, so no pre-existing failure is being waived.G28: signed
int256 +=was transcribed as an unsigned checked addExact semantics change. In the executable (
Contract) plane,getStorageon a non-packed, non-transientInt256storage field now bindsInt256.ofUint256 wordand types the local.int256. Before this change it bound the rawUint256word. As a result,addPanic/subPanicon that value now resolve to the signed checked instances (Core.Int256.safeAdd/safeSub, Panic 0x11 on signed overflow), not the unsignedAddPanic Uint256with theInt256operand coerced throughCoe Int256 Uint256. Packed, transient and non-Int256 fields are unchanged. The compilation-model / Yul plane is unchanged; it already lowered these as signed.Soundness argument. The storage word is the two's-complement encoding.
Int256.ofUint256is the identity on the 256-bit word, so writes round-trip unchanged. The only thing that changes is which arithmetic instance elaboration picks. That instance now matches the Solidityint256semantics, which the compiler plane already emitted, so the change removes a divergence between the two planes. Before the fix the executable plane had both spurious reverts (-1 + 25) and missed overflows (maxInt256 + 1succeeded).Tests. In
Contracts/Smoke/Arithmetic.lean(decide +kernel):applyDelta 25from a stored-1succeeds and stores24;applyDelta 1frommaxInt256panics. The existingInt256CheckedSmokeis now correct as well.G14: ERC-20 balance read through a hop
Semantics change: none. These are additive lemmas. On main, a typed call on a
linked_contractsbinding already runs the token body inhopCallView/hopCallat the runtime target.Added to
Verity/Core.lean:Contract.hopCall_success_of_ne,Contract.hopCall_scoped_callee(a committed hop parks the callee's plain map/address writes under.scoped callee),Contract.hopCallView_getMappingandContract.hopCallView_getMapping2. These are proved from the definitions with no new axioms.Tests.
Contracts/Smoke/Erc20BalanceHop.leanhas a generated ERC-20 and a strategy-shaped caller.held_eq_token_entryis proved for all states. Kernel witnesses show that a transfer through the hop moves the token's balances, leaves the caller's own slot untouched, and that an overdraw reverts. Foundry property testsPropertyHopToken/PropertyHopStrategyare included.G2: keccak / mapping-slot evaluation
Semantics change: none (test only). Since #2459, no executable accessor reaches keccak: single-key mappings use
.map/.mapUint/.map2, nested/struct mappings use the symbolic.mapChain, and selectors are hashed at elaboration time.Tests.
Contracts/Smoke/HashedMappings.leang2Runevaluates a sequence of generated bodies (setMappingN,setStructMember,getMappingN, struct members) withdecide +kernel. It does not usenative_decide.Remaining assumptions
.mapChainand.scopedstorage to real EVM slots assumes keccak collision-freedom. This affects the interpretation layer only; no execution path depends on it.strategy reserve <= token balanceis proof work in the consumer, not a Verity gap.No
sorry/admit/axiom/native_decideis added.🤖 Generated with Claude Code