Lean packet and transaction refinement foundation - #28
Conversation
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_b9c973f6-0d74-42de-9833-723801c7184d) |
![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: 3f4499ab02
ℹ️ 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_77327010-8959-4da6-82f7-1ba5e2bf49c5) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3441895750
ℹ️ 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_5d0621d1-7d0c-4337-bb22-35af48d6de4d) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 287ba3f301
ℹ️ 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_1de86faa-c54a-4487-8b11-3a8c5e51df05) |
# Conflicts: # SHA256SUMS
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_77479a21-e538-4f8c-a10b-3383f4376b7d) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 965317c464
ℹ️ 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".
1 participant
Summary
Scope boundaries
This PR does not change SystemVerilog, FPGA files, Python production semantics,
or the BLAKE3 protocol. The packet checksum remains an explicit refinement seam:
this slice does not claim a CRC-32 correctness theorem, an oracle refinement,
or an RTL/netlist refinement.
Validation
2fa58d4d00e007dbd806bf459db77ee643557cf53f4499ab023379567d1af3810ddeaa7b379dc7dfsorry|admit|axiom|unsafescan: exit 0native_decidescan: exit 0cd lean && lake build: exit 0cd lean && lake build LeanVMBMinCore: exit 0python3 tools/generate_checksums.py --check: exit 090210396329on nodeGitHub Actions 1000018601: success (exit 0) at exact headNote
Low Risk
Changes are confined to Lean proofs and documentation; production SystemVerilog, host runtime, and protocol transport are untouched, and the docs state no CRC-32 or RTL refinement claims yet.
Overview
Adds a Lean formal layer for LSC-1 v1 packet envelopes and transaction lifecycle, without changing RTL, host Python, or FPGA artifacts.
Packet.leanmodels parsed request/response wires with a checksum-parametric encode/decode API (CRC-32 left as a later refinement seam). It proves round-trip correctness for in-cap payloads and ordered request validation precedence (SOF → length cap → checksum → version → flags).Transaction.leanis a pure functional stage / RETIRE / abort / reset model where instruction semantics supply proposedTransitionvalues. Proved properties include atomic staging, index-range rejection, abort without committing, matching vs mismatched retirement, reset, and exactly-once successful retirement.Docs add a
THEOREM_INVENTORY, a proof-boundaries row and status ledger entry for this slice, andlean/READMEmodule notes;SHA256SUMSis refreshed. Open work (byte-stream decode, per-opcode payloads, CRC-32 instantiation, oracle/RTL refinement) is explicitly scoped out.Reviewed by Cursor Bugbot for commit 965317c. Bugbot is set up for automated code reviews on this repo. Configure here.