proof: add ABI scalar encoding correctness library#2165
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_95943e33-5215-4a89-9fd6-b73b650220ee) |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: scout_triage · Mode: large-lean-hotspots · 5 finding(s) · 3 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 3 Lean file(s), 486 changed supported line(s). Scout model ranked 5/5 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 5 inline comment(s).
Warnings
- coverage : Large Lean scout mode covers ranked hotspots only. Codex/human review must cover skipped hunks and proof obligations; OCR strong packet review is not wired yet.
OCR pilot metrics
- Routing: large-lean-hotspots (router-v8)
- Changed files: 3 supported / 3 total; Lean 3, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 486 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 5; files 3; tokens 0; tool calls 0; warnings 1; duration 34s
- Largest changed files: Compiler/Proofs/AbiEncoding.lean (+435/-0), PrintAxioms.lean (+49/-1), Compiler.lean (+1/-0)
Packet coverage
- Packet review: enabled; selected 5/8 packet(s)
- Scout: configured; status success; model reviewer_scout
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 5 scout-ranked packet(s); remaining changed hunks/files require Codex or human proof review, and selected packets still need strong reviewer analysis.
- Strong packet-review blocker: OpenCodeReview 1.7.5 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
- Covered packets:
- Compiler/Proofs/AbiEncoding.lean:1 score 104 — public declaration/signature changed, changed imports; ask: Read the full new module end-to-end. (1) Confirm the encoders proven equal to abiScalarNormalize_* are exactly the production Yul encoders in Compiler.CompilationModel and not a parallel/spec formulation; pinpoint the theorem that connects abiScalarNormalize_uint256/uint8/uint16 to the real encoder. (2) Verify
abiScalarNormalize_newtypeOfdoes not silently coerce away representational differences (e.g. between newtype wrappers and their underlying types). (3) Explain whylit_255_mod_evm, `li - PrintAxioms.lean:974 score 14 — hotspot path/churn; ask: Open lines 974-1020 of PrintAxioms.lean in full. (1) Enumerate every new identifier added in this block (not just the 12 lines visible in the excerpt) and categorize each as public theorem / private lemma / instance / def. (2) Confirm that none of the added entries are
sorryd or axiom-bearing; if any are, request their proof. (3) Verify the listed names match exactly the symbols exported by Compiler/Proofs/AbiEncoding.lean — mismatched symbol names here would mean the tracking list drifts away - Compiler.lean:33 score 42 — changed imports; ask: Confirm
Compiler.Proofs.AbiEncodingis the intended import location and not duplicated in some other umbrella. (1) Check for a circular or duplicate import (e.g. viaCompiler.Proofs.IRGeneration.Expralready pulling it). (2) Verify nothing in Compiler.lean's surrounding imports already provides equivalent scalar-normalization facts, which would mean this module is redundant or in conflict. - PrintAxioms.lean:38 score 42 — changed imports; ask: Re-run
lake exe printAxioms(or equivalent) after this import lands and confirm the axiom set emitted for PrintAxioms contains only previously-trusted axioms plus the deliberateabiScalarNormalize_*theorems and nothing additional. (1) Also verify there is no unintended lexicographic reordering in the import list that could change elaboration order. - PrintAxioms.lean:6059 score 12 — hotspot path/churn; ask: Independently count the theorems, lemmas, and private helpers in the head of Compiler/Proofs/AbiEncoding.lean (lines 1-435) and confirm the deltas reconcile to (+40 public, +5 private, Δ_total = +45) with
0 sorry'd. (1) If the counts disagree, treat as a blocker. (2) Also confirm nononcomputable/axiom-only declarations are mis-classified as theorems.
- Compiler/Proofs/AbiEncoding.lean:1 score 104 — public declaration/signature changed, changed imports; ask: Read the full new module end-to-end. (1) Confirm the encoders proven equal to abiScalarNormalize_* are exactly the production Yul encoders in Compiler.CompilationModel and not a parallel/spec formulation; pinpoint the theorem that connects abiScalarNormalize_uint256/uint8/uint16 to the real encoder. (2) Verify
Pilot mode: advisory only. Codex Review remains the merge gate.
|
|
||
| end Examples | ||
|
|
||
| end Compiler.Proofs.AbiEncoding |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · high]
Large Lean packet selected for stronger review: public declaration/signature changed, changed imports; 435 changed line(s) near Compiler/Proofs/AbiEncoding.lean:1.
Risk signals: public declaration/signature changed, changed imports.
Scout reason: New 435-line proof module introducing a shared scalar-normalization library tied to issue #2082. Risk: the module is presented as a real-Yul characterization (encodeStaticCustomErrorArg, normalizeEventWord), so any parallel/word-level mismatch would silently invalidate the trusted bridge used by requireError/revertError and the event bridge in GenericInduction/EventBridge.lean. 8 new public abiScalarNormalize_* theorems plus 3 private helper lemmas (lit_255_mod_evm, lit_65535_mod_evm, addressMas
Question for stronger reviewer: Read the full new module end-to-end. (1) Confirm the encoders proven equal to abiScalarNormalize_* are exactly the production Yul encoders in Compiler.CompilationModel and not a parallel/spec formulation; pinpoint the theorem that connects abiScalarNormalize_uint256/uint8/uint16 to the real encoder. (2) Verify `abiScalarNormalize_newtypeOf` does not silently coerce away representational differences (e.g. between newtype wrappers and their underlying types). (3) Explain why `lit_255_mod_evm`, `li
Added-line sample:
- L1: import Compiler.CompilationModel.AbiEncoding
- L2: import Compiler.Proofs.IRGeneration.IRInterpreter
- L3:
- L4: /-!
- L5: # ABI scalar encoding correctness
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| Compiler.Proofs.AbiEncoding.eventHeadWordSize_static_scalar_eq_32 | ||
| -- Compiler.Proofs.AbiEncoding.foldl_eventHeadWordSize_static_scalar_eq -- private | ||
| Compiler.Proofs.AbiEncoding.abiHeadSize_static_scalars_eq | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 47 changed line(s) near PrintAxioms.lean:974.
Risk signals: hotspot path/churn.
Scout reason: Hotspot path/churn inside PrintAxioms.lean: a new section '-- Compiler/Proofs/AbiEncoding.lean' is appended to what appears to be the trusted-theorem tracking list, listing 8 abiScalarNormalize_* names (public) plus 3 private comments (lit_255_mod_evm, lit_65535_mod_evm, addressMask_mod_evm). Because this file is the audit/axiom-tracker the reviewer leans on, every name added here is implicitly being declared trusted; the diff_excerpt only covers lines 974-985, so an unknown number of further th
Question for stronger reviewer: Open lines 974-1020 of PrintAxioms.lean in full. (1) Enumerate every new identifier added in this block (not just the 12 lines visible in the excerpt) and categorize each as public theorem / private lemma / instance / def. (2) Confirm that none of the added entries are `sorry`d or axiom-bearing; if any are, request their proof. (3) Verify the listed names match exactly the symbols exported by Compiler/Proofs/AbiEncoding.lean — mismatched symbol names here would mean the tracking list drifts away
Added-line sample:
- L974: -- Compiler/Proofs/AbiEncoding.lean
- L975: Compiler.Proofs.AbiEncoding.abiScalarNormalize_uint256
- L976: Compiler.Proofs.AbiEncoding.abiScalarNormalize_int256
- L977: Compiler.Proofs.AbiEncoding.abiScalarNormalize_bytes32
- L978: Compiler.Proofs.AbiEncoding.abiScalarNormalize_uint8
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| import Compiler.Keccak.SpongeProperties | ||
| import Compiler.Proofs.KeccakBound | ||
| import Compiler.Proofs.MappingSlot | ||
| import Compiler.Proofs.AbiEncoding |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: changed imports; 1 changed line(s) near Compiler.lean:33.
Risk signals: changed imports.
Scout reason: Trusted top-level file Compiler.lean gains a new proof-library import (`Compiler.Proofs.AbiEncoding`). Because Compiler.lean is the umbrella that fixes which proofs are visible to the rest of the codebase and downstream consumers, adding an import here elevates the new module into the trusted top-level surface — every theorem in AbiEncoding.lean is now reachable from every other proof in the project.
Question for stronger reviewer: Confirm `Compiler.Proofs.AbiEncoding` is the intended import location and not duplicated in some other umbrella. (1) Check for a circular or duplicate import (e.g. via `Compiler.Proofs.IRGeneration.Expr` already pulling it). (2) Verify nothing in Compiler.lean's surrounding imports already provides equivalent scalar-normalization facts, which would mean this module is redundant or in conflict.
Added-line sample:
- L33: import Compiler.Proofs.AbiEncoding
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| import Verity.Proofs.Stdlib.ListSum | ||
| import Verity.Proofs.Stdlib.MappingAutomation | ||
| import Verity.Proofs.Stdlib.Math | ||
| import Compiler.Proofs.AbiEncoding |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: changed imports; 1 changed line(s) near PrintAxioms.lean:38.
Risk signals: changed imports.
Scout reason: PrintAxioms.lean top-of-file import list now pulls `Compiler.Proofs.AbiEncoding`, meaning the PrintAxioms dump (and whatever it drives, e.g. axiom-counting tooling) will need to traverse the full new module. Any hidden axioms introduced by the new module will now show up in PrintAxioms output.
Question for stronger reviewer: Re-run `lake exe printAxioms` (or equivalent) after this import lands and confirm the axiom set emitted for PrintAxioms contains only previously-trusted axioms plus the deliberate `abiScalarNormalize_*` theorems and nothing additional. (1) Also verify there is no unintended lexicographic reordering in the import list that could change elaboration order.
Added-line sample:
- L38: import Compiler.Proofs.AbiEncoding
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| ] | ||
|
|
||
| -- Total: 5635 theorems/lemmas (3888 public, 1747 private, 0 sorry'd) | ||
| -- Total: 5680 theorems/lemmas (3928 public, 1752 private, 0 sorry'd) |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 2 changed line(s) near PrintAxioms.lean:6059.
Risk signals: hotspot path/churn.
Scout reason: PrintAxioms.lean ending comment updates the global theorem/lemma count from 5635 → 5680 (Δ +45; +40 public, +5 private, 0 sorry'd). The `0 sorry'd` figure is the headline trust signal in this project, so any drift between this number and the actual module contents is a regression risk. The +40 public delta should reconcile against the 8 abiScalarNormalize_* entries visible in pkt-4 plus whatever else lines 986-1020 introduce.
Question for stronger reviewer: Independently count the theorems, lemmas, and private helpers in the head of Compiler/Proofs/AbiEncoding.lean (lines 1-435) and confirm the deltas reconcile to (+40 public, +5 private, Δ_total = +45) with `0 sorry'd`. (1) If the counts disagree, treat as a blocker. (2) Also confirm no `noncomputable`/axiom-only declarations are mis-classified as theorems.
Added-line sample:
- L6059: -- Total: 5680 theorems/lemmas (3928 public, 1752 private, 0 sorry'd)
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
|
Recovery gate disposition for current head |
| \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``` |
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_fad4955c-eea4-44f9-9ced-87b3a830f868) |
|
@codex review |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: scout_triage · Mode: large-lean-hotspots · 5 finding(s) · 3 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 3 Lean file(s), 486 changed supported line(s). Scout model ranked 5/5 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 5 inline comment(s).
Warnings
- coverage : Large Lean scout mode covers ranked hotspots only. Codex/human review must cover skipped hunks and proof obligations; OCR strong packet review is not wired yet.
OCR pilot metrics
- Routing: large-lean-hotspots (router-v8)
- Changed files: 3 supported / 3 total; Lean 3, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 486 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 5; files 3; tokens 0; tool calls 0; warnings 1; duration 43s
- Largest changed files: Compiler/Proofs/AbiEncoding.lean (+435/-0), PrintAxioms.lean (+49/-1), Compiler.lean (+1/-0)
Packet coverage
- Packet review: enabled; selected 5/8 packet(s)
- Scout: configured; status success; model reviewer_scout
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 5 scout-ranked packet(s); remaining changed hunks/files require Codex or human proof review, and selected packets still need strong reviewer analysis.
- Strong packet-review blocker: OpenCodeReview 1.7.5 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
- Covered packets:
- Compiler/Proofs/AbiEncoding.lean:1 score 104 — public declaration/signature changed, changed imports; ask: For each public abiScalarNormalize_* lemma, is the proof a faithful witness for the actual Yul/Solidity ABI encoding (sign/zero extension, byte width, endianness) of the encoder it claims to characterize, or does it silently introduce a parallel word-level model that diverges from the real encoder used at the call sites named in the module docstring? In particular, verify the newtypeOf, address, and bool normalizations against the real Yul encoder; confirm that no
sorry,axiom, or external c - PrintAxioms.lean:974 score 14 — hotspot path/churn; ask: Does the set of public abiScalarNormalize_* names here exactly match the public decls declared in Compiler/Proofs/AbiEncoding.lean (pkt-1), and is each one a proved theorem (not an axiom, sorry, or external constant) in the final environment? Are the three commented-out 'private' helpers truly
privatein pkt-1, or do they leak into the public namespace and need to be added here too? Are the 8 new entries inserted in a section that is actually included in the printed-axioms output? - Compiler.lean:33 score 42 — changed imports; ask: Is the new module's import position (between KeccakBound/MappingSlot and StorageLens) consistent with the existing organization of Compiler.Proofs.* imports in this file, and does any other Compiler.Proofs.* module already transitively re-export Compiler.Proofs.AbiEncoding such that this import is redundant, double-counted, or shadowing a different version of the namespace?
- PrintAxioms.lean:38 score 42 — changed imports; ask: Does the placement of this import (between Verity.Proofs.Stdlib.Math and Compiler.Proofs.ArithmeticProfile) match the convention used for the surrounding Compiler.Proofs.* entries, and is it logically consistent with the root Compiler.lean import added in pkt-2? Could a missing import here cause pkt-1's lemmas to be silently dropped from the axiom-walk output?
- PrintAxioms.lean:6060 score 12 — hotspot path/churn; ask: Does the +45 public, +5 private, +0 sorry delta match exactly the set of new decls introduced by pkt-1 (and registered in pkt-4)? Where do the extra 37 public and 2 private decls beyond the 8 public + 3 private in pkt-4 come from, and is the sorry count still genuinely 0 after the new module is loaded?
- Compiler/Proofs/AbiEncoding.lean:1 score 104 — public declaration/signature changed, changed imports; ask: For each public abiScalarNormalize_* lemma, is the proof a faithful witness for the actual Yul/Solidity ABI encoding (sign/zero extension, byte width, endianness) of the encoder it claims to characterize, or does it silently introduce a parallel word-level model that diverges from the real encoder used at the call sites named in the module docstring? In particular, verify the newtypeOf, address, and bool normalizations against the real Yul encoder; confirm that no
Pilot mode: advisory only. Codex Review remains the merge gate.
|
|
||
| end Examples | ||
|
|
||
| end Compiler.Proofs.AbiEncoding |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · high]
Large Lean packet selected for stronger review: public declaration/signature changed, changed imports; 435 changed line(s) near Compiler/Proofs/AbiEncoding.lean:1.
Risk signals: public declaration/signature changed, changed imports.
Scout reason: Brand new 435-line module Compiler/Proofs/AbiEncoding.lean is the dominant change in the diff. It introduces shared scalar-normalization lemmas for the real Yul-expression encoders (encodeStaticCustomErrorArg, normalizeEventWord) and the only 'public declaration/signature changed' signal in the changeset. Because the module is then wired into the root Compiler.lean and into PrintAxioms, any semantic flaw in its lemmas or proofs propagates straight into the trusted core.
Question for stronger reviewer: For each public abiScalarNormalize_* lemma, is the proof a faithful witness for the actual Yul/Solidity ABI encoding (sign/zero extension, byte width, endianness) of the encoder it claims to characterize, or does it silently introduce a parallel word-level model that diverges from the real encoder used at the call sites named in the module docstring? In particular, verify the newtypeOf, address, and bool normalizations against the real Yul encoder; confirm that no `sorry`, `axiom`, or external c
Added-line sample:
- L1: import Compiler.CompilationModel.AbiEncoding
- L2: import Compiler.Proofs.IRGeneration.IRInterpreter
- L3:
- L4: /-!
- L5: # ABI scalar encoding correctness
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| Compiler.Proofs.AbiEncoding.eventHeadWordSize_static_scalar_eq_32 | ||
| -- Compiler.Proofs.AbiEncoding.foldl_eventHeadWordSize_static_scalar_eq -- private | ||
| Compiler.Proofs.AbiEncoding.abiHeadSize_static_scalars_eq | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 47 changed line(s) near PrintAxioms.lean:974.
Risk signals: hotspot path/churn.
Scout reason: PrintAxioms registration block lists 8 new public lemmas (abiScalarNormalize_uint256/int256/bytes32/uint8/uint16/address/bool/newtypeOf) plus 3 commented-out 'private' helpers. This is the axiom-tracker surface for pkt-1; any name that drifts between the registration list and the real public decls would let a theorem silently drop out of axiom-tracking or, conversely, let a private helper be misreported as public.
Question for stronger reviewer: Does the set of public abiScalarNormalize_* names here exactly match the public decls declared in Compiler/Proofs/AbiEncoding.lean (pkt-1), and is each one a proved theorem (not an axiom, sorry, or external constant) in the final environment? Are the three commented-out 'private' helpers truly `private` in pkt-1, or do they leak into the public namespace and need to be added here too? Are the 8 new entries inserted in a section that is actually included in the printed-axioms output?
Added-line sample:
- L974: -- Compiler/Proofs/AbiEncoding.lean
- L975: Compiler.Proofs.AbiEncoding.abiScalarNormalize_uint256
- L976: Compiler.Proofs.AbiEncoding.abiScalarNormalize_int256
- L977: Compiler.Proofs.AbiEncoding.abiScalarNormalize_bytes32
- L978: Compiler.Proofs.AbiEncoding.abiScalarNormalize_uint8
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| import Compiler.Keccak.SpongeProperties | ||
| import Compiler.Proofs.KeccakBound | ||
| import Compiler.Proofs.MappingSlot | ||
| import Compiler.Proofs.AbiEncoding |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: changed imports; 1 changed line(s) near Compiler.lean:33.
Risk signals: changed imports.
Scout reason: Adding 'import Compiler.Proofs.AbiEncoding' to the root Compiler.lean promotes the new module to a top-level trust-boundary component: every theorem transitively loaded by the root now includes the new ABI lemmas. Placement and ordering here affects what is part of the trusted core.
Question for stronger reviewer: Is the new module's import position (between KeccakBound/MappingSlot and StorageLens) consistent with the existing organization of Compiler.Proofs.* imports in this file, and does any other Compiler.Proofs.* module already transitively re-export Compiler.Proofs.AbiEncoding such that this import is redundant, double-counted, or shadowing a different version of the namespace?
Added-line sample:
- L33: import Compiler.Proofs.AbiEncoding
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| import Verity.Proofs.Stdlib.ListSum | ||
| import Verity.Proofs.Stdlib.MappingAutomation | ||
| import Verity.Proofs.Stdlib.Math | ||
| import Compiler.Proofs.AbiEncoding |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: changed imports; 1 changed line(s) near PrintAxioms.lean:38.
Risk signals: changed imports.
Scout reason: PrintAxioms.lean also gains the same import, so the new module now participates in the printed-axiom walk. Cross-checking this against pkt-2 and pkt-4 is required to confirm consistent trust-boundary wiring.
Question for stronger reviewer: Does the placement of this import (between Verity.Proofs.Stdlib.Math and Compiler.Proofs.ArithmeticProfile) match the convention used for the surrounding Compiler.Proofs.* entries, and is it logically consistent with the root Compiler.lean import added in pkt-2? Could a missing import here cause pkt-1's lemmas to be silently dropped from the axiom-walk output?
Added-line sample:
- L38: import Compiler.Proofs.AbiEncoding
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| ] | ||
|
|
||
| -- Total: 5636 theorems/lemmas (3889 public, 1747 private, 0 sorry'd) | ||
| -- Total: 5681 theorems/lemmas (3929 public, 1752 private, 0 sorry'd) |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 2 changed line(s) near PrintAxioms.lean:6060.
Risk signals: hotspot path/churn.
Scout reason: Footer count in PrintAxioms.lean is bumped from 5636 to 5681 (public 3889 -> 3929, private 1747 -> 1752, sorry 0). This must reconcile exactly with the new decls introduced by pkt-1 and registered in pkt-4; a mismatch could indicate hidden decls, accidentally introduced `sorry`s, or proof deletions masked by the count.
Question for stronger reviewer: Does the +45 public, +5 private, +0 sorry delta match exactly the set of new decls introduced by pkt-1 (and registered in pkt-4)? Where do the extra 37 public and 2 private decls beyond the 8 public + 3 private in pkt-4 come from, and is the sorry count still genuinely 0 after the new module is loaded?
Added-line sample:
- L6060: -- Total: 5681 theorems/lemmas (3929 public, 1752 private, 0 sorry'd)
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
|
Codex Review: Didn't find any major issues. You're on a roll. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
1 participant
Summary
Adds
Compiler.Proofs.AbiEncoding, a scalar ABI normalization proof library tied directly to the real Yul-expression encoders andevalIRExpr.Files:
Compiler/Proofs/AbiEncoding.leanCompiler.leanPrintAxioms.leanBase:
origin/mainatbd54fa9c47b9abb43895c312fe1f874192ba8327Head:
b9674f85864a351df0b4a30cec550ad814262943Dependencies: none
Downstream Consumers
requireError/revertErrorinCompile.leanCompiler/Proofs/IRGeneration/GenericInduction/EventBridge.leanTheorems By Category
Spec and simp lemmas:
abiScalarNormalize_uint256abiScalarNormalize_int256abiScalarNormalize_bytes32abiScalarNormalize_uint8abiScalarNormalize_uint16abiScalarNormalize_addressabiScalarNormalize_boolabiScalarNormalize_newtypeOfnormalizeEventWordevaluation characterization:normalizeEventWord_uint8_evalnormalizeEventWord_uint16_evalnormalizeEventWord_address_evalnormalizeEventWord_bool_evalnormalizeEventWord_uint256_evalnormalizeEventWord_int256_evalnormalizeEventWord_bytes32_evalnormalizeEventWord_newtypeOf_evalencodeStaticCustomErrorArgevaluation characterization:encodeStaticCustomErrorArg_uint8_evalencodeStaticCustomErrorArg_uint16_evalencodeStaticCustomErrorArg_address_evalencodeStaticCustomErrorArg_bool_evalencodeStaticCustomErrorArg_uint256_evalencodeStaticCustomErrorArg_int256_evalencodeStaticCustomErrorArg_bytes32_evalEncoder agreement:
encodeStaticCustomErrorArg_eval_eq_normalizeEventWord_evalencodeStaticCustomErrorArg_agrees_with_normalizeEventWord_uint8encodeStaticCustomErrorArg_agrees_with_normalizeEventWord_uint16Spec facts:
abiScalarNormalize_bool_outputabiScalarNormalize_uint8_lt_evmabiScalarNormalize_uint16_lt_evmabiScalarNormalize_address_lt_evmabiScalarNormalize_bool_lt_evmabiScalarNormalize_lt_evm_of_lt_evmabiScalarNormalize_address_fixedabiScalarNormalize_uint8_idemabiScalarNormalize_uint16_idemabiScalarNormalize_address_idemabiScalarNormalize_bool_idemabiScalarNormalize_idempotentHead-size basics:
IsStaticScalarParamTypeeventHeadWordSize_static_scalar_eq_32abiHeadSize_static_scalars_eqProof Intuition
The scalar spec is intentionally small:
abiScalarNormalizecaptures exactly what the compiler's expression-level wrappers do once evaluated byevalIRExpr. For masked cases, the spec normalizes through EVM word modulus before applying the bitwise mask, matching the interpreter behavior for Yuland. Forbool, the spec followsyulToBoolthrough evaluation, so nonzero modulo-word values become1and zero becomes0.The encoder lemmas prove each scalar wrapper by unfolding the real compiler functions and the IR expression evaluator, then reducing the corresponding builtin call. The event lemmas do the same for
normalizeEventWord, and the agreement theorem packages the fact that both real encoder paths compute the same scalar normalization. Range, idempotence, bool, address-fixed, and head-size facts are stated at the shared spec level so downstream proofs can rewrite from either encoder into the same ABI scalar model.Validation
lean-slot lake build: passed (spark-build: remote build finished (exit=0)).lake build: passed.python3 scripts/generate_print_axioms.py --check: passed.python3 scripts/lean_lint.py --only axioms: passed.make check: passed (Ran 607 tests ... OK;All checks passed.).git diff --check: passed.git show --check --format=short HEAD: passed.sorry/admit/axiom/#exitinCompiler/Proofs/AbiEncoding.leanandCompiler.lean: no matches.Note
Low Risk
Proof-only additions with no changes to compiler codegen or runtime behavior; risk is limited to proof maintenance and axiom inventory size.
Overview
Adds
Compiler.Proofs.AbiEncoding, a shared proof layer for issue #2082 that ties ABI scalar words to the actual Yul encoders (normalizeEventWord,encodeStaticCustomErrorArg) viaevalIRExpr, instead of a separate word-level model.Introduces
abiScalarNormalize(Nat-level spec: masks, bool via EVM modulus, identity for full-word types) with simp lemmas,evalIRExprcharacterization theorems per scalar type for both encoder paths, and lemmas thatencodeStaticCustomErrorArgmatchesnormalizeEventWordon supported static scalars. Also adds spec-level facts (range belowevmModulus, idempotence, bool 0/1, address fixed when< 2^160),IsStaticScalarParamType, andabiHeadSize_static_scalars_eq, plus small executable examples.Compiler.leanandPrintAxioms.leanimport/register the new public theorems; no changes to compilation or runtime codegen behavior.Reviewed by Cursor Bugbot for commit 171f8a8. Bugbot is set up for automated code reviews on this repo. Configure here.