Repository navigation
feat(solidity-import): support calldata slices, Governor proposer description checks, bytes1..bytes31 locals/casts, and MemberAccess tuple assignments - #2503
Conversation
…cription checks, bytes1..bytes31 locals/casts, and MemberAccess tuple assignments
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. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f13260a576
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| if let some (slicePre, offsetExpr, lenExpr, _) ← lowerCalldataSlice? inner then | ||
| return (slicePre, true, offsetExpr, lenExpr) |
There was a problem hiding this comment.
When the source is a msg.data or _msgData() slice starting below byte 4, discarding isMsgData here sends the decoder through a plain calldataload(offset). The model's calldataloadWord returns only the selector at offset 0 and zero at offsets 1–3 (Verity/Core/Model/Denote.lean:140-143), so inputs such as abi.decode(msg.data[0:32], (bytes32)) omit the adjacent argument bytes and diverge from Solidity. Use the same selector/payload stitching already applied by lowerBytesToFixedBytes and lowerEncodedBytes, or reject these slice offsets.
Useful? React with 👍 / 👎.
| let pre := buf.pre ++ lhsVal.pre ++ #[ | ||
| .letVar addrVar (.add buf.pointer (.sub lhsVal.expr (.literal (32 + k)))), |
There was a problem hiding this comment.
For headerless buffers produced by expressions such as abi.encodePacked, this address translation is only equivalent while lhs >= 32 + k; otherwise the original Yul load reaches the dynamic-bytes length header, but the imported program reads unrelated memory before buf.pointer. For example, a one-byte buf and mload(add(buf, sub(mload(buf), 1))) returns the length word 1 in Solidity, whereas this lowers to mload(buf.pointer - 32) without ever storing that header. Either synthesize the length header or fail closed unless the address is guaranteed to remain in the payload.
Useful? React with 👍 / 👎.
| let env ← get | ||
| pure (env.stringBuffers.contains id.toNat || env.calldataBytes.contains id.toNat) |
There was a problem hiding this comment.
A direct bytes memory local initialized from abi.encode, abi.encodePacked, or another supported byte expression is registered in env.byteBuffers, but this predicate only recognizes stringBuffers and calldataBytes. Consequently, an ordinary b[i] on such a local skips the new byte-index lowering and fails in lowerRef with the encoded-byte-local restriction, despite this change advertising dynamic bytes element reads. Include env.byteBuffers.contains id.toNat in the recognized identifier cases.
Useful? React with 👍 / 👎.
1 participant
Summary
bytes calldataandmsg.data/_msgData()slice expressions (data[start:end],data[start:],data[:end],data[:]) in.length,bytesN(slice),abi.decode(slice, (...)), and memory materialization (bytes(slice),keccak256(slice),abi.encode*,bytes.concat) with exact bounds guards (start <= end <= base.length).Governor._isValidDescriptionForProposer: unaligned Yul byte-buffer tailmload(add(buf, sub(len, k)))(1 <= k <= 32), dynamicbytes/bytes(string)element readsb[i](bytes1withPanic(0x32)bounds check), and bounded tail-windowfor (uint256 i = bound - K; i < bound; ++i)loops (including earlyif (...) return ...;inside helpers).bytes1..bytes31) locals, helper parameters/returns,bytesN("...")string literal casts (N < 32), andbytes12/bytes20conversions (bytes12 <-> uint96 / bytes32,bytes20 <-> uint160 / address / bytes32,ERC2771Context._msgSender()).MemberAccesscomponents in tuple assignments ((_roles[roleId].grantDelay, effect) = _roles[roleId].grantDelay.withUpdate(...)inAccessManager).GovernorSliceProposerDelaySequencedifferential test fixture, rejection controls, and 4 mutation anchors.