spec: AtomicOrderingMemento — discharge Effect::AtomicAccess (closes #397)#431
Conversation
|
Warning Rate limit exceeded
To continue reviewing without waiting, purchase usage credits in the billing tab. ⌛ How to resolve this issue?After the wait time has elapsed, a review can be triggered using the We recommend that you space out your commits to avoid hitting the rate limit. 🚦 How do rate limits work?CodeRabbit enforces hourly rate limits for each developer per organization. Our paid plans have higher rate limits than the trial, open-source and free plans. In all cases, we re-allow further reviews after a brief timeout. Please see our FAQ for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (1)
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
There was a problem hiding this comment.
Pull request overview
This PR adds a new normative protocol spec for AtomicOrderingMemento, intended to define how atomic-access effects are discharged in the verifier/composition pipeline.
Changes:
- Adds a new atomic-ordering memento spec document under
protocol/specs/. - Defines a layered envelope/header/metadata wire shape and canonicalization/CID rules.
- Documents discharge semantics and worked examples for atomic accesses.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| # AtomicOrderingMemento — Normative Spec | ||
|
|
||
| **Status:** v1.0.0 normative | ||
| **Date:** 2026-05-06 |
| AtomicOrderingHeader = { | ||
| schemaVersion: "1", | ||
| kind: "AtomicOrderingMemento", | ||
| target: tstr, ; the atomic variable / expression name | ||
| ordering: Ordering, ; the concrete ordering | ||
| atomicKind: AtomicKind, ; Load / Store / Rmw / Cas | ||
| } |
|
|
||
| AtomicOrderingHeader = { | ||
| schemaVersion: "1", | ||
| kind: "AtomicOrderingMemento", |
| JCS encodes the memento as a flat object with keys in insertion order. The canonical key order for the memento value is: | ||
|
|
||
| ``` | ||
| envelope.header.target ; concrete target symbol | ||
| envelope.header.ordering ; concrete Ordering | ||
| envelope.header.atomicKind ; Load / Store / Rmw / Cas | ||
| envelope.header.schemaVersion ; "1" | ||
| envelope.header.kind ; "AtomicOrderingMemento" | ||
| metadata.atomicTargetType ; optional | ||
| metadata.producedBy ; optional | ||
| metadata.producedAt ; optional | ||
| envelope.metadata ; (the metadata object) | ||
| envelope.header ; (the header object) | ||
| envelope.signer ; signer pubkey | ||
| envelope.declaredAt ; ISO 8601 | ||
| envelope.signature ; Ed25519 sig over JCS({header, metadata}) | ||
| ``` |
| The canonical canonicalization follows the layered assembly rule from `2026-05-03-substrate-layers-envelope-header-body.md` §1: | ||
|
|
||
| 1. Build `{header, metadata}` as a JCS value. | ||
| 2. Build `envelope = {signer, declaredAt}`. | ||
| 3. Sign `JCS({header, metadata})` with Ed25519, producing `signature`. | ||
| 4. Add `signature` to envelope. | ||
| 5. Full memento = `{envelope, header, metadata}`. | ||
| 6. JCS-encode the full memento. | ||
| 7. CID = `BLAKE3-512(JCS(memento))`. | ||
|
|
||
| ## §3. Content-addressing (BLAKE3-512) | ||
|
|
||
| The memento's CID is: | ||
|
|
||
| ``` | ||
| blake3-512:hex(BLAKE3_512(JCS(memento))) | ||
| ``` |
| ## §4. Discharge rule | ||
|
|
||
| A function contract carrying `Effect::AtomicAccess { target, kind, ordering: None }` composes if and only if the verifier pool contains an `AtomicOrderingMemento` where: | ||
|
|
||
| - `header.target == target` — the affected atomic variable matches. | ||
| - `header.atomicKind == kind` — the operation class matches (`Load`, `Store`, `Rmw`, `Cas`). | ||
| - `header.ordering` is one of the five valid Ordering values. | ||
| - The envelope's signature verifies correctly against the signer's pubkey. | ||
|
|
||
| Once discharged, the effect is cleared from the contract's `effects` array and composition proceeds. The ordering value from the memento takes the place of the previously-None `ordering` field on the effect. | ||
|
|
||
| A function contract carrying `AtomicAccess { ordering: Some(ord) }` does NOT require a memento — the ordering is already statically known. |
| AtomicOrderingHeader = { | ||
| schemaVersion: "1", | ||
| kind: "AtomicOrderingMemento", | ||
| target: tstr, ; the atomic variable / expression name | ||
| ordering: Ordering, ; the concrete ordering | ||
| atomicKind: AtomicKind, ; Load / Store / Rmw / Cas | ||
| } | ||
|
|
||
| MementoMetadata = { | ||
| ? atomicTargetType: tstr, ; e.g. "AtomicU32", "AtomicBool" | ||
| ? producedBy: tstr, | ||
| ? producedAt: iso8601, | ||
| } | ||
|
|
||
| Ordering = "Relaxed" / "Acquire" / "Release" / "AcqRel" / "SeqCst" | ||
| AtomicKind = "Load" / "Store" / "Rmw" / "Cas" |
![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: c1154c81f1
ℹ️ 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".
| AtomicOrderingHeader = { | ||
| schemaVersion: "1", | ||
| kind: "AtomicOrderingMemento", | ||
| target: tstr, ; the atomic variable / expression name | ||
| ordering: Ordering, ; the concrete ordering | ||
| atomicKind: AtomicKind, ; Load / Store / Rmw / Cas | ||
| } |
There was a problem hiding this comment.
cid in AtomicOrderingHeader
This v1.4 layered wire shape defines header without a cid, but the substrate layering contract requires every memento header to carry a content CID. As written, an AtomicOrderingMemento minted from this spec cannot satisfy the common header validation/identity flow used by other v1.4 discharge mementos, so verifiers that expect a standard header.cid will reject or be unable to index these mementos consistently.
Useful? React with 👍 / 👎.
| - `header.target == target` — the affected atomic variable matches. | ||
| - `header.atomicKind == kind` — the operation class matches (`Load`, `Store`, `Rmw`, `Cas`). |
There was a problem hiding this comment.
The discharge rule matches only target and atomicKind, which is not specific enough when the same atomic target is accessed multiple times with unresolved runtime orderings. In that case a single memento can incorrectly discharge multiple effects or make selection ambiguous, even though the spec later says each site needs its own memento. Add a site-stable identifier (for example a call-site CID) to both effect and memento matching.
Useful? React with 👍 / 👎.
| envelope.header.target ; concrete target symbol | ||
| envelope.header.ordering ; concrete Ordering | ||
| envelope.header.atomicKind ; Load / Store / Rmw / Cas | ||
| envelope.header.schemaVersion ; "1" | ||
| envelope.header.kind ; "AtomicOrderingMemento" |
There was a problem hiding this comment.
The canonical key-order list starts with envelope.header.* paths, but this memento's wire shape has top-level header and metadata siblings next to envelope. Implementers following this list will canonicalize/hash a different structure than the one assembled in steps 1–5, causing CID/signature mismatches across implementations.
Useful? React with 👍 / 👎.
|
Substantive Review — PR #431 AtomicOrderingMemento HOLD. Three P1 blocking issues prevent merge: P1-A: TARGET FIELD — No Normalization Rule (Renames Break CID Stability) Issue: §1 defines Fix: Add normative rule to §1: "target MUST be the qualified fully-scoped symbol name from the lifter's def_id, with generic substitutions fully applied and lifetimes elided. NO leading ::. Form: module::path::symbol." Acceptance: Spec clarifies exact string form. P1-B: JCS CANONICAL KEY ORDER DIVERGENCE — kind Not First Issue: §2 lists key order with target FIRST. But #427 (PinInvariantMemento) and substrate layer spec establish kind MUST be first for deterministic CID computation. This breaks the pattern. JCS encodes keys in declaration order—if Python kit emits kind in different position, CIDs diverge even for identical content. Verifier cannot deduplicate. Fix: Reorder §2 key order to match #427: kind, schemaVersion, target, atomicKind, ordering. Acceptance: Multiple independent emitters produce identical CIDs. P1-C: SIGNING AUTHORITY — Left Undefined (P2 Blocker) Issue: §4 checks "signature verifies against signer's pubkey" but never specifies WHO IS THE SIGNER. Without signing authority, discharge is cosmetic—attacker can self-sign any memento. Fix: Either (a) name the signer: "MUST be FOUNDATION_V0_SEED or whitelisted key", OR (b) explicitly defer to #397 with note: "Signing authority: P2 follow-up. Spec requires signer whitelist check at discharge time." Acceptance: Signer is either named or P2 is explicitly referenced. P2-A: MEMENTOPOOL::INSERT() ARM MISSING Spec defines discharge rule but no implementation guidance for pool insert. #427 had same problem—trait method declared, impl left undefined, implementer guessed, rework was needed. Fix: Add to §4 the exact sequence: verify signer in whitelist, verify Ed25519 sig, compute CID, insert into atomicOrderingIndex keyed by (target, atomicKind), refuse duplicates. P2-B: COMPOSITION GUARD NOT EXPLICIT Issue: §4 never says "effects cleared from contract after discharge" or "composition proceeds downstream". Could be phantom like #419. Fix: Add: "Once discharged, effect REMOVED from contract.effects. Ordering from memento REPLACES the None. If any AtomicAccess with ordering: None remains, return OpacityError::AtomicOrderingNotDischarged." Minor: P3-A — Worked Examples Incomplete §5.1 is short. §5.2 missing. Add Load with Acquire example in same structure: Lifted output / Composition / Discharge / Result. |
…ity, functionCid anchoring
Closes #397. Normative spec for AtomicOrderingMemento. 159 lines, mirrors LoopInvariantMemento pattern. CDDL wire shape, JCS key order, BLAKE3 CID, discharge rule, 2 worked examples.