research: [1636] event exclusion map for Layer 2 proofs#1643
research: [1636] event exclusion map for Layer 2 proofs#1643
Conversation
![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: 49882a1cbd
ℹ️ 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".
|
|
||
| The problem is not code generation. | ||
|
|
||
| - `Stmt.emit` and `Stmt.rawLog` are first-class statement constructors in [Compiler/CompilationModel/Types.lean](/workspaces/mission-e5876dfd/repo/Compiler/CompilationModel/Types.lean):410 and [Compiler/CompilationModel/Types.lean](/workspaces/mission-e5876dfd/repo/Compiler/CompilationModel/Types.lean):416. |
There was a problem hiding this comment.
The document links source references using workspace-specific absolute paths such as /workspaces/mission-e5876dfd/repo/..., which only resolve on the author's machine and are broken in normal checkouts and on GitHub, so readers cannot verify the cited code locations. Please switch these links to repository-relative paths (or stable external URLs) so the research artifact remains usable across environments.
Useful? React with 👍 / 👎.
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
| - The typed-IR compiler lowers them in [Compiler/TypedIRCompiler.lean](/workspaces/mission-e5876dfd/repo/Compiler/TypedIRCompiler.lean):361-376. | ||
| - Typed IR lowers them to `logN` Yul in [Compiler/TypedIRLowering.lean](/workspaces/mission-e5876dfd/repo/Compiler/TypedIRLowering.lean):96-101. | ||
| - The typed interpreter appends events to `world.events` in [Verity/Core/Free/TypedIR.lean](/workspaces/mission-e5876dfd/repo/Verity/Core/Free/TypedIR.lean):248-260. | ||
| - The contract monad already models event append via `emitEvent` in [Verity/Core.lean](/workspaces/mission-e5876dfd/repo/Verity/Core.lean):463-470. |
There was a problem hiding this comment.
All links use hardcoded dev-environment workspace paths
Medium Severity
Every link in the document uses hardcoded absolute paths from a dev environment (e.g., /workspaces/mission-e5876dfd/repo/... and /workspaces/mission-e5876dfd/morpho-verity/...). These paths are specific to a Codespace/container workspace and will render as broken links on GitHub and anywhere else. Since this document's core value is serving as a "line-accurate exclusion map," having all ~25 reference links broken significantly undermines its utility.
Additional Locations (2)
1 participant
References #1636.
This is a research-only PR for issue #1636.
I chose Option A and produced
docs/research/1636-event-exclusion-map.mdbecause the repository already compilesemitandrawLogcorrectly; the immediate blocker is the Layer 2 proof-surface gating chain inSupportedSpec.lean. A line-accurate exclusion map is the fastest way to unblock the implementation work that will add event/log-trace support.The artifact documents:
SupportedSpec.lean, including the legacy compatibility scan, the effect-surface gate, the body witness chain, and the typed-eventspec.events = []gate;local_obligations+mstore+rawLogworkaround pattern inTh0rgal/morpho-verity, includingflashLoanandsetAuthorizationWithSig.Note
Low Risk
Low risk: this PR only adds research documentation and makes no code or proof changes.
Overview
Adds a research note
docs/research/1636-event-exclusion-map.mdthat line-maps whereStmt.emit/Stmt.rawLogare currently excluded from the Layer 2 proof surface (primarily via effect/contract-surface gates and thespec.events = []requirement), and outlines the minimal proof-surface edits needed to introduce event/log-trace support.Written by Cursor Bugbot for commit 49882a1. This will update automatically on new commits. Configure here.