Phase 1B: common summaries/transitions/observables API - #2219
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_5a2994ea-038c-4629-8c26-dde3342429d2) |
![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
🟡 Scout triage only — not a full review. 2 finding(s) (2 high); a human or Codex must still cover the unflagged hunks and proof obligations.
Large Lean diff routed to bounded packet review: 4 Lean file(s), 183 changed supported line(s). Multi-lens scout (4/4 lens(es): provenance, verification-independence, environment-determinism, proof-soundness) surfaced 2/7 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 2 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 4 supported / 4 total; Lean 4, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 183 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 2; files 2; tokens 0; tool calls 0; warnings 1; duration 29s
- Largest changed files: Compiler/Proofs/ExecutionSummary.lean (+136/-0), Compiler/Proofs/YulGeneration/ExecutionSummary.lean (+32/-0), PrintAxioms.lean (+12/-1), Compiler.lean (+2/-0)
Packet coverage
- Packet review: enabled; selected 2/8 packet(s)
- Scout: configured; status success; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 2 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.9 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/ExecutionSummary.lean:1 score 100 [lenses: provenance, verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: Does RawSummary enumerate every field of IRResult/YulResult whose integrity the downstream proofs depend on, or does it project a subset? If a backend adds or changes a field not listed in RawSummary, does any proof become vacuous or bypassed?
- Compiler/Proofs/YulGeneration/ExecutionSummary.lean:1 score 100 [lenses: provenance, verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: List every field of YulResult and IRResult. For each field not projected into RawSummary, confirm whether any downstream proof's soundness depends on it. Can a producer alter an un-projected field to change runtime behavior while the summary check still passes?
Pilot mode: advisory only. Codex Review remains the merge gate.
![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: c30c914666
ℹ️ 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".
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_6c36fc05-bec6-4c3f-ae57-d1557aafcc63) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. 4 finding(s) (2 high / 2 low); a human or Codex must still cover the unflagged hunks and proof obligations.
Large Lean diff routed to bounded packet review: 4 Lean file(s), 206 changed supported line(s). Multi-lens scout (4/4 lens(es): provenance, verification-independence, environment-determinism, proof-soundness) surfaced 4/7 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 4 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 4 supported / 4 total; Lean 4, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 206 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 4; files 3; tokens 0; tool calls 0; warnings 1; duration 58s
- Largest changed files: Compiler/Proofs/ExecutionSummary.lean (+136/-0), Compiler/Proofs/YulGeneration/ExecutionSummary.lean (+55/-0), PrintAxioms.lean (+12/-1), Compiler.lean (+2/-0)
Packet coverage
- Packet review: enabled; selected 4/8 packet(s)
- Scout: configured; status success; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 4 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.9 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/YulGeneration/ExecutionSummary.lean:1 score 101 [lenses: provenance, verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: Is observableSlots pinned independently by the consumer/verifier, or can the producer choose which slots are observable? If the producer controls the list, what prevents silently omitting a slot whose value would reveal a refinement failure?
- Compiler/Proofs/ExecutionSummary.lean:1 score 100 [lenses: provenance, verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: Does RawSummary pin every observable artifact that downstream correctness proofs consume? Are there backend-result fields (gas, transient storage, log ordering) excluded from the summary that could be silently swapped by a backend adapter without detection?
- PrintAxioms.lean:1782 score 12 [lenses: provenance, proof-soundness] — hotspot path/churn; ask: Do these five entries exhaust every axiom or trusted lemma that ExecutionSummary.lean introduces, or are there additional axioms (e.g., in dependent IRGeneration files) that the manifest omits and could be silently swapped in?
- PrintAxioms.lean:6430 score 12 [lenses: provenance, proof-soundness] — hotspot path/churn; ask: Is RawSummary.ofYulResult_refines_of_eq the only axiom/trusted lemma in the new YulGeneration/ExecutionSummary.lean module, or does the manifest omit additional trusted artifacts a producer could silently add?
Pilot mode: advisory only. Codex Review remains the merge gate.
| funext slot | ||
| exact hStorage slot.1 slot.2 | ||
|
|
||
| end Compiler.Proofs.YulGeneration |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| storage := result.finalStorage | ||
| events := result.events } | ||
|
|
||
| end Compiler.Proofs |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| Compiler.Proofs.RawSummary.toExecutionSummary?_revert | ||
| Compiler.Proofs.RawSummary.toExecutionSummary?_failed_with_return | ||
| Compiler.Proofs.RawSummary.toExecutionSummary?_adequate | ||
|
|
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| ] | ||
|
|
||
| -- Total: 6026 theorems/lemmas (4173 public, 1853 private, 0 sorry'd) | ||
| -- Total: 6031 theorems/lemmas (4178 public, 1853 private, 0 sorry'd) |
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
| \n### CI Failure Hints\n\nFailed jobs: `build`\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_4817815f-f2d0-4209-b523-afc79a40293c) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. 4 finding(s) (2 high / 2 low); a human or Codex must still cover the unflagged hunks and proof obligations.
Large Lean diff routed to bounded packet review: 4 Lean file(s), 210 changed supported line(s). Multi-lens scout (4/4 lens(es): provenance, verification-independence, environment-determinism, proof-soundness) surfaced 4/7 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 4 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 4 supported / 4 total; Lean 4, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 210 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 4; files 3; tokens 0; tool calls 0; warnings 1; duration 38s
- Largest changed files: Compiler/Proofs/ExecutionSummary.lean (+136/-0), Compiler/Proofs/YulGeneration/ExecutionSummary.lean (+59/-0), PrintAxioms.lean (+12/-1), Compiler.lean (+2/-0)
Packet coverage
- Packet review: enabled; selected 4/8 packet(s)
- Scout: configured; status success; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 4 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.9 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/YulGeneration/ExecutionSummary.lean:1 score 101 [lenses: provenance, verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: How is
observableSlotsconstructed and verified at each call site? Is there a checksum or soundness lemma proving the list is complete with respect to the backend's actual storage writes, or can a caller silently omit slots the contract modified? - Compiler/Proofs/ExecutionSummary.lean:1 score 100 [lenses: provenance, verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: Does the RawSummary / ExecutionObservables structure capture every observable execution artifact that downstream proofs rely on? Are there backend result fields (e.g., transient storage, gas, logs metadata) not represented, and could a producer silently set those without being caught by toExecutionSummary? or by the adapter conversion?
- PrintAxioms.lean:1782 score 12 [lenses: verification-independence] — hotspot path/churn; ask: Is toExecutionSummary?_adequate proven from first principles or admitted/trusted? If trusted, what independent evidence confirms that the projection captures all observable execution effects?
- PrintAxioms.lean:6430 score 12 [lenses: verification-independence] — hotspot path/churn; ask: Is ofYulResult_refines_of_eq derived from an independent Yul semantics, or does its proof reuse the same backend code/harness that produced the Yul result being 'refined'?
- Compiler/Proofs/YulGeneration/ExecutionSummary.lean:1 score 101 [lenses: provenance, verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: How is
Pilot mode: advisory only. Codex Review remains the merge gate.
| simp [RawSummary.ofYulResultOn, RawSummary.ofIRResultOn, | ||
| hSuccess, hReturn, hEvents, hStorageOn] | ||
|
|
||
| end Compiler.Proofs.YulGeneration |
There was a problem hiding this comment.
OpenCodeReview [high]
Findings (3 lenses):
- Data & artifact provenance: Defines ObservableStorageSlot as a subtype restricting exposed storage to a finite
observableSlotslist, and RawSummary.ofIRResultOn uses that list as the observation boundary. The provenance risk is whetherobservableSlotsis itself pinned by a trusted source — if a producer can silently shrink, extend, or swap this list, the summary's coverage claim is hollow and storage mutations outside the boundary are invisible.- Ask the reviewer: How is
observableSlotsconstructed and verified at each call site? Is there a checksum or soundness lemma proving the list is complete with respect to the backend's actual storage writes, or can a caller silently omit slots the contract modified?
- Ask the reviewer: How is
- Verification independence: RawSummary.ofIRResultOn directly copies fields from IRResult (success, returnValue, storage via result.finalStorage, events) into the summary. The adapter trusts the IR-layer result wholesale; the only added constraint is ObservableStorageSlot membership. The storage function reads result.finalStorage directly — no independent recomputation or cross-check against an alternative semantics.
- Ask the reviewer: Is there an independent execution semantics (e.g., a Yul/IR interpreter separate from the one that produced IRResult) against which this projection's field values are ever cross-checked? Or does every downstream proof transitively trust the same IRResult producer?
- Lean proof soundness: Defines a finite observation boundary (ObservableStorageSlot) and a RawSummary adapter that projects IR-result storage through a caller-supplied observableSlots list. This is a trust-boundary definition: if the adapter can cherry-pick or under-specify observable slots, or if the projection via IRStorageSlot.ofNat is unsound, downstream refinement theorems become vacuous. The doc comment itself flags that the adapter must not expose a total storage function — exactly the kind of soundness-critica
- Ask the reviewer: Does ObservableStorageSlot faithfully bound the backend's actual observable storage? Could a downstream proof exploit an empty or too-small observableSlots list (e.g. []) to make a refinement or adequacy theorem vacuously true? Is the projection result.finalStorage (IRStorageSlot.ofNat slot.1) a faithful bijection between the summary's slot type and the IR's storage model?
Why flagged: public declaration/signature changed, changed imports; 59 changed line(s) near Compiler/Proofs/YulGeneration/ExecutionSummary.lean:1. Signals: public declaration/signature changed, changed imports.
Added-line sample:
- Ask the reviewer: Does ObservableStorageSlot faithfully bound the backend's actual observable storage? Could a downstream proof exploit an empty or too-small observableSlots list (e.g. []) to make a refinement or adequacy theorem vacuously true? Is the projection result.finalStorage (IRStorageSlot.ofNat slot.1) a faithful bijection between the summary's slot type and the IR's storage model?
- L1:
import Compiler.Proofs.ExecutionSummary - L2:
import Compiler.Proofs.YulGeneration.RuntimeTypes - L3:
(empty) - L4:
namespace Compiler.Proofs.YulGeneration - L5:
(empty)
Scout triage coverage marker — not a final OCR semantic review or approval.
| storage := result.finalStorage | ||
| events := result.events } | ||
|
|
||
| end Compiler.Proofs |
There was a problem hiding this comment.
OpenCodeReview [high]
Findings (3 lenses):
- Data & artifact provenance: Introduces RawSummary as a backend-neutral projection API that adapters fill in, with toExecutionSummary? validation rejecting inconsistent results. The provenance concern is manifest completeness: does the RawSummary structure enumerate ALL observable state (storage, events, return value, success/revert) or does it omit fields like transient storage or gas that a producer could silently swap without invalidating the summary?
- Ask the reviewer: Does the RawSummary / ExecutionObservables structure capture every observable execution artifact that downstream proofs rely on? Are there backend result fields (e.g., transient storage, gas, logs metadata) not represented, and could a producer silently set those without being caught by toExecutionSummary? or by the adapter conversion?
- Verification independence: The module docstring explicitly states this is 'deliberately a projection API rather than a new semantics.' RawSummary adapters re-expose existing backend result records (success, returnValue, storage, events) rather than independently re-deriving execution outcomes. Any downstream 'proof' that consumes ExecutionSummary is checking self-consistency with the producer's own result shape, not correctness.
- Ask the reviewer: Does any theorem that claims to verify backend correctness actually re-derive the execution outcome, or does it merely constrain a RawSummary that was projected from the backend's own result record? Where is the independent semantics that the projection is checked against?
- Lean proof soundness: Defines the core ExecutionOutcome inductive, ExecutionObservables structure, and RawSummary type, plus the toExecutionSummary? filter that rejects failed-with-return results. The invariant 'failed executions carrying a return value are rejected' is soundness-critical: if enforced only as a runtime Option-filter rather than at the type level, any theorem assuming toExecutionSummary? = some _ could be vacuously satisfied on inconsistent inputs. The structure's field constraints (e.g., storage as a
- Ask the reviewer: Is the 'no return value on failure' invariant enforced at the type level (making illegal states unrepresentable) or only via an Option-returning filter? For toExecutionSummary?_adequate and the other listed theorems, do the proofs contain any sorry/admit, and do they depend on any axioms beyond Lean's standard three? Could the RawSummary.storage field being total (fun slot => ...) contradict the stated goal of restricting to finite observable storage, creating a semantic gap that proofs could ex
Why flagged: public declaration/signature changed, changed imports; 136 changed line(s) near Compiler/Proofs/ExecutionSummary.lean:1. Signals: public declaration/signature changed, changed imports.
Added-line sample:
- Ask the reviewer: Is the 'no return value on failure' invariant enforced at the type level (making illegal states unrepresentable) or only via an Option-returning filter? For toExecutionSummary?_adequate and the other listed theorems, do the proofs contain any sorry/admit, and do they depend on any axioms beyond Lean's standard three? Could the RawSummary.storage field being total (fun slot => ...) contradict the stated goal of restricting to finite observable storage, creating a semantic gap that proofs could ex
- L1:
import Compiler.Proofs.IRGeneration.IRRuntimeTypes - L2:
(empty) - L3:
namespace Compiler.Proofs - L4:
(empty) - L5:
open Compiler.Proofs.IRGeneration
Scout triage coverage marker — not a final OCR semantic review or approval.
| Compiler.Proofs.RawSummary.toExecutionSummary?_revert | ||
| Compiler.Proofs.RawSummary.toExecutionSummary?_failed_with_return | ||
| Compiler.Proofs.RawSummary.toExecutionSummary?_adequate | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [low]
Finding: PrintAxioms lists RawSummary.toExecutionSummary?_adequate as an axiom-trusted lemma. If the adequacy of the summary conversion — i.e., the claim that the projection faithfully represents the execution — is itself an unproven axiom, then any verification that depends on this summary is replaying trust, not independently checking.
Ask the reviewer: Is toExecutionSummary?_adequate proven from first principles or admitted/trusted? If trusted, what independent evidence confirms that the projection captures all observable execution effects?
Why flagged: hotspot path/churn; 6 changed line(s) near PrintAxioms.lean:1782. Signals: hotspot path/churn.
Added-line sample:
- L1782:
-- Compiler/Proofs/ExecutionSummary.lean - L1783:
Compiler.Proofs.RawSummary.toExecutionSummary?_success - L1784:
Compiler.Proofs.RawSummary.toExecutionSummary?_revert - L1785:
Compiler.Proofs.RawSummary.toExecutionSummary?_failed_with_return - L1786:
Compiler.Proofs.RawSummary.toExecutionSummary?_adequate
Scout triage coverage marker — not a final OCR semantic review or approval.
| ] | ||
|
|
||
| -- Total: 6026 theorems/lemmas (4173 public, 1853 private, 0 sorry'd) | ||
| -- Total: 6031 theorems/lemmas (4178 public, 1853 private, 0 sorry'd) |
There was a problem hiding this comment.
OpenCodeReview [low]
Finding: PrintAxioms lists RawSummary.ofYulResult_refines_of_eq as an axiom-trusted refinement claim. A refinement relation between the Yul backend result and the summary is exactly the kind of bridge that must be independently derived; if it is taken as an axiom, the 'verification' is circular.
Ask the reviewer: Is ofYulResult_refines_of_eq derived from an independent Yul semantics, or does its proof reuse the same backend code/harness that produced the Yul result being 'refined'?
Why flagged: hotspot path/churn; 5 changed line(s) near PrintAxioms.lean:6430. Signals: hotspot path/churn.
Added-line sample:
- L6430:
-- Compiler/Proofs/YulGeneration/ExecutionSummary.lean - L6431:
Compiler.Proofs.YulGeneration.RawSummary.ofYulResult_refines_of_eq - L6432:
(empty) - L6443:
-- Total: 6031 theorems/lemmas (4178 public, 1853 private, 0 sorry'd)
Scout triage coverage marker — not a final OCR semantic review or approval.
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage + 1/2 paquet(s) reviewés sémantiquement. 2 finding(s) (2 high); les hunks hors paquets restent à couvrir par un humain ou Codex.
Paquets non couverts par la review sémantique
- Compiler/Proofs/ExecutionSummary.lean — error (spawnSync ocr ETIMEDOUT)
Large Lean diff routed to bounded packet review: 4 Lean file(s), 210 changed supported line(s). Multi-lens scout (3/4 lens(es): verification-independence, environment-determinism, proof-soundness) surfaced 2/7 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 2 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 4 supported / 4 total; Lean 4, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 210 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage_with_packet_review; comments 2; files 2; tokens 0; tool calls 0; warnings 1; duration 1464s
- Largest changed files: Compiler/Proofs/ExecutionSummary.lean (+136/-0), Compiler/Proofs/YulGeneration/ExecutionSummary.lean (+59/-0), PrintAxioms.lean (+12/-1), Compiler.lean (+2/-0)
Packet coverage
- Packet review: enabled; selected 2/8 packet(s)
- Scout: configured; status success; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness (1 lens(es) failed; union of the rest used); rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 2 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.9 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/YulGeneration/ExecutionSummary.lean:1 score 101 [lenses: verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: Are the result fields (success, returnValue, finalStorage, events) consumed by these adapters independently derived by a separate semantics, or are they the backend's own characterization of its output? Who supplies observableSlots, and can a buggy or adversarial producer shrink it to hide storage mutations from the summary?
- Compiler/Proofs/ExecutionSummary.lean:1 score 100 [lenses: verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: Is RawSummary/ExecutionSummary ever consumed as standalone correctness evidence, or is it always paired with a separately-derived expected outcome? Does toExecutionSummary?_adequate prove anything beyond the projection's own definitional well-formedness (failed executions must not carry a return value)?
Pilot mode: advisory only. Codex Review remains the merge gate.
| simp [RawSummary.ofYulResultOn, RawSummary.ofIRResultOn, | ||
| hSuccess, hReturn, hEvents, hStorageOn] | ||
|
|
||
| end Compiler.Proofs.YulGeneration |
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [high]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Findings (2 lenses):
- Verification independence: The summary adapters RawSummary.ofIRResultOn / ofYulResultOn directly read success, returnValue, finalStorage, and events from the IR/Yul result record, re-projecting producer-emitted state rather than independently re-deriving the observable outcome. The theorem RawSummary.ofYulResult_refines_of_eq only proves that two such projections agree — i.e., self-consistency between adapters that share the same trusted inputs — not independent verification of execution correctness. The ObservableStorage
- Ask the reviewer: Are the result fields (success, returnValue, finalStorage, events) consumed by these adapters independently derived by a separate semantics, or are they the backend's own characterization of its output? Who supplies observableSlots, and can a buggy or adversarial producer shrink it to hide storage mutations from the summary?
- Lean proof soundness: Defines the observable-storage subtype and IR/Yul summary adapters, plus the refinement theorem RawSummary.ofYulResult_refines_of_eq. This is soundness-critical because over-strong equality/refinement hypotheses or an adapter that projects native storage beyond the finite observation boundary can make the refinement result vacuous.
- Ask the reviewer: Does ofYulResult_refines_of_eq rely only on meaningful hypotheses, e.g. observableSlots covers exactly the result's reachable storage, and is it proved without sorry/axioms while preventing the total storage function from being silently exposed outside the observed boundary?
Why flagged: public declaration/signature changed, changed imports; 59 changed line(s) near Compiler/Proofs/YulGeneration/ExecutionSummary.lean:1. Signals: public declaration/signature changed, changed imports.
Added-line sample:
- Ask the reviewer: Does ofYulResult_refines_of_eq rely only on meaningful hypotheses, e.g. observableSlots covers exactly the result's reachable storage, and is it proved without sorry/axioms while preventing the total storage function from being silently exposed outside the observed boundary?
- L1:
import Compiler.Proofs.ExecutionSummary - L2:
import Compiler.Proofs.YulGeneration.RuntimeTypes - L3:
(empty) - L4:
namespace Compiler.Proofs.YulGeneration - L5:
(empty)
| storage := result.finalStorage | ||
| events := result.events } | ||
|
|
||
| end Compiler.Proofs |
There was a problem hiding this comment.
🟡 OCR scout — question de triage (non-review) [high]
Question de couverture pour le reviewer humain/Codex — pas une review sémantique finale ni une approbation.
Findings (2 lenses):
- Verification independence: The module explicitly states it is 'deliberately a projection API rather than a new semantics,' so RawSummary.toExecutionSummary? and the toExecutionSummary?_adequate theorem verify the projection's internal consistency, not independent correctness of the underlying execution. RawSummary.ofIRResult reads result fields straight from the IR result record, inheriting the producer's own execution characterization. If any downstream proof or audit treats this summary as independent verification, it w
- Ask the reviewer: Is RawSummary/ExecutionSummary ever consumed as standalone correctness evidence, or is it always paired with a separately-derived expected outcome? Does toExecutionSummary?_adequate prove anything beyond the projection's own definitional well-formedness (failed executions must not carry a return value)?
- Lean proof soundness: Introduces the core RawSummary/ExecutionSummary projection API plus @[simp] lemmas and an adequacy theorem. Soundness depends on the adequacy statement not being vacuous and on the failed-with-return rejection invariant being actually proven rather than encoded weakly enough to hold trivially.
- Ask the reviewer: Do the proof bodies for toExecutionSummary?_success/_revert/_failed_with_return and toExecutionSummary?_adequate avoid sorry/admit/axioms, and is _adequate strong enough to rule out inconsistent backend summaries rather than holding whenever toExecutionSummary? returns none?
Why flagged: public declaration/signature changed, changed imports; 136 changed line(s) near Compiler/Proofs/ExecutionSummary.lean:1. Signals: public declaration/signature changed, changed imports.
Added-line sample:
- Ask the reviewer: Do the proof bodies for toExecutionSummary?_success/_revert/_failed_with_return and toExecutionSummary?_adequate avoid sorry/admit/axioms, and is _adequate strong enough to rule out inconsistent backend summaries rather than holding whenever toExecutionSummary? returns none?
- L1:
import Compiler.Proofs.IRGeneration.IRRuntimeTypes - L2:
(empty) - L3:
namespace Compiler.Proofs - L4:
(empty) - L5:
open Compiler.Proofs.IRGeneration
|
@codex review |
|
Codex Review: Didn't find any major issues. Breezy! 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". |
|
Phase 1B frozen-head update — native storage projection boundary New frozen head: Exact-head remote Lean receipts (
Also clean at the frozen head: The earlier failed target receipt and direct |
1 participant
Summary
Adds the common typed summaries, transitions, and observables API on
EVMYulLean, providing shared interfaces for Phase 1B execution and proof integration.Validation
34b4f353-4419-4263-ac7a-168758bee34e0c30c9146663fbc7592c5ac1d2a3916b7eed729fclake build Compiler.Proofs.EndToEndleanprover/lean4:v4.31.0Note
Low Risk
Proof-layer API and projection lemmas only; no runtime compiler behavior or auth/data paths change.
Overview
Adds a backend-neutral typed execution summary layer so IR and Yul can expose the same outcome/observable shape without defining new semantics. Existing backend records map through
RawSummary, andtoExecutionSummary?fail-closes whensuccess = falsebut a return value is still present.The core API includes
ExecutionOutcome,ExecutionObservables,ExecutionSummary,ExecutionTransition, plus simp/adequacy lemmas for success, revert, and inconsistent failures.RawSummary.ofIRResultadapts currentIRResultrecords.Yul-specific wiring (
Compiler.Proofs.YulGeneration.ExecutionSummary) restricts storage to caller-listedobservableSlotsviaObservableStorageSlot, matching the native harness boundary (nativeResultsMatchOn).ofIRResultOn/ofYulResultOnbuild bounded raw summaries, andofYulResult_refines_of_eqlifts pointwise IR/Yul equality on that boundary to equal typed summaries.Imports are added in
Compiler.lean; new theorems are registered inPrintAxioms.lean.Reviewed by Cursor Bugbot for commit b7c5722. Bugbot is set up for automated code reviews on this repo. Configure here.