AMP v0.1.0 (draft): Algorithm Memento Protocol — substrate self-hosts its own production mechanism#544
Merged
Conversation
The substrate's first axiom is Supra omnia, rectum. Until today, the substrate's own lifters violated that axiom — the same algorithm implemented independently in 5 language ports, no canonical reference, no content-addressed identity, no mechanically-detectable drift. AMP closes the gap. Algorithms become content-addressed mementos. Language bindings become verifiable refinement-claims. Discharge produces receipts. The substrate hosts its own production mechanism under the same first axiom that governs its outputs. This draft (v0.1.0) defines: - Algorithm memento shape (FunctionContractMemento with conventions) - Binding-claim memento shape (refines an algorithm via input_cids) - Refinement relation (formalized in §2) - Minting protocol (§3, §4) - Discharge protocol (§5) - Projection mementos per language (§6) - Federation rule (§7) — same algorithm CID = same algorithm - Lifecycle (§8) — refine / deprecate / version through PEP - Worked example: TWO_ARMED_CONDITIONAL (§9) - Relation to PPP, CCP, FRP, PEP (§10) - Open questions deferred to future versions (§11) - Out of scope (§12) — implementation, migration, ProofIR effect extensions After AMP lands and is implemented, every contract emitted by every lifter carries provenance to a content-addressed algorithm + binding + discharge receipt. Drift detectable. Federation mechanical. The substrate finally applies its first axiom to itself. T Savo
|
Warning Rate limit exceeded
You’ve run out of usage credits. Purchase more 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 (3)
WalkthroughThis pull request introduces the Algorithm Memento Protocol (AMP) v0.1.0 specification and a supporting theoretical paper establishing the correctness and design rationale for substrate self-application. The changes add two new foundational documents and update the paper index without modifying any code or public APIs. ChangesAlgorithm Memento Protocol and Self-Hosted Verification
Poem
🎯 3 (Moderate) | ⏱️ ~22 minutes 🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ 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 |
![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: 3fc4e8827b
ℹ️ 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".
Comment on lines
+123
to
+127
| ∀ (i : LangAST). B.pre(i) → | ||
| ∃ (a : ASTPattern). P_lang.project(i) = Some(a) | ||
| ∧ A.pre(a) | ||
| ∧ B.post(i, ctx) = A.post(a, ctx) | ||
| ``` |
There was a problem hiding this comment.
The formal refinement claim uses ctx without binding it (B.post(i, ctx) = A.post(a, ctx)), which makes the obligation an open formula rather than a closed theorem. Open formulas are not directly dischargeable as stated and can be interpreted inconsistently across backends, so implementations will either fail lowering/proving or silently assume an implicit scope that is not specified.
Useful? React with 👍 / 👎.
| To mint a binding-claim `B` for algorithm `A` in language `L`: | ||
|
|
||
| 1. Identify the binding code (the lifter's source files). | ||
| 2. Compute `B.body_cid` as `BLAKE3-512` of the binding source code bytes (concatenated with file separators per a normalization rule TBD). |
There was a problem hiding this comment.
Step 2 makes B.body_cid mandatory for minting but leaves byte normalization as TBD, so different producers can hash different byte streams for identical binding code (file ordering, separators, newline normalization, path encoding). That breaks cross-port reproducibility and can invalidate attestation/federation because the same logical binding may receive different CIDs.
Useful? React with 👍 / 👎.
The substrate's first axiom Supra omnia, rectum binds the substrate's outputs but has not until now bound the substrate's own production mechanism. The lifter family is five-language reimplementations of the same algorithms with no canonical reference, no content-addressed identity for the algorithm itself, no mechanically-detectable drift. This paper extends the After-X arc one level inward: the substrate applies its first axiom to itself. Algorithms become content-addressed mementos. Language ports become verifiable refinement-claims. Discharge produces signed receipts. Federation across languages is by algorithm CID, mechanically. Contains nine lemmas with constructive proofs or proof sketches: L1 Federation by CID L2 Soundness Preservation L3 Drift Detection L4 Algorithm Identity is Syntactic, not Behavioral L5 Compositional Lifters L6 Language Closure L7 Cousot Equivalence (catalog = reduced product of abstract domains) L8 Algebraic Effects Embedding L9 Substrate Self-Hosting Engages six counterarguments (decidability, circularity, port resistance, foundational regress, catalog explosion, projection-memento friction). Companion to AMP v0.1.0 spec (PR #544). T Savo
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 4
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@docs/papers/12-after-languages-how-proofir-represents-every-language.md`:
- Line 11: The phrase "five Python ports, five Rust ports, five C ports" in the
opening paragraph is inconsistent with the rest of the paper which asserts five
total language ports; replace that sequence with wording that matches the
intended meaning (e.g., "five language ports" or list the five languages once).
Locate the sentence beginning "**What this paper argues.**" and update the
fragment "five Python ports, five Rust ports, five C ports of the same
algorithm" to a corrected form such as "five language ports of the same
algorithm" (or an explicit single list of the five languages) so the port-count
matches the paper's narrative and removes the copy error.
In `@protocol/specs/2026-05-09-algorithm-memento-protocol.md`:
- Around line 84-85: The spec currently has two conflicting normative
requirements: "input_cids must include the algorithm being bound" and a separate
mandatory requirement for P_lang.cid during minting; unify these into one rule
by making "input_cids MUST include the algorithm CID" the single normative
requirement and update the minting rules to derive/validate P_lang.cid from
input_cids (or mark P_lang.cid optional/derived), ensuring both references
(input_cids and P_lang.cid in minting) state the same requirement and include a
brief sentence describing how emitters should validate the algorithm CID against
input_cids to avoid incompatible emitters.
- Around line 33-35: Update the markdown fenced code blocks to include
appropriate language identifiers (e.g., ```text or ```json) to satisfy MD040;
specifically add language tags to the blocks containing "A : ASTPattern ×
Context → IrFormula", the AlgorithmMemento and BindingClaimMemento sections
(AlgorithmMemento ⊆ FunctionContractMemento and BindingClaimMemento ⊆
FunctionContractMemento), the AlgorithmCatalog JSON block, the formal/assertion
blocks referencing "∀ (i : LangAST). B.pre(i) →" and "B.post = forall
i:LangAST.", and the ASTProjectionMemento block so each fenced block has the
correct language hint (use ```text for math/notation and ```json for
AlgorithmCatalog).
- Around line 123-127: The formula uses ctx without binding; fix by quantifying
ctx and making the postcondition a forall over contexts (e.g. add "∀ (ctx :
CtxType)." so the clause becomes ∀ (i : LangAST). B.pre(i) → ∃ (a : ASTPattern).
P_lang.project(i) = Some(a) ∧ A.pre(a) ∧ ∀ (ctx : CtxType). B.post(i, ctx) =
A.post(a, ctx); apply the same change to the analogous formula at lines 132-137
and ensure the same CtxType (or explicit context sort) is used consistently for
B.post and A.post.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: d3c9aec4-eefc-439f-81c8-90389e2d7a18
📒 Files selected for processing (3)
docs/papers/12-after-languages-how-proofir-represents-every-language.mddocs/papers/README.mdprotocol/specs/2026-05-09-algorithm-memento-protocol.md
| > | ||
| > **Premise the earlier papers established.** A content-addressed federated substrate of canonical predicates, with signed implication edges, witnesses from a portfolio of solvers, droppers that close the loop with lifters, and a federation that asymptotically reduces verification cost to cache lookup. After Verification argued that this substrate makes leaf-discharge bug classes structurally impossible. After Types argued that invariants replace logging as the primary epistemic instrument. | ||
| > | ||
| > **What this paper argues.** That the substrate's first axiom — *Supra omnia, rectum*, above all correctness — has been load-bearing for substrate output but has not yet been applied to the substrate's own production mechanism. The lifters that emit substrate output have themselves been per-language reimplementations: five Python ports, five Rust ports, five C ports of the same algorithm, no canonical reference, no content-addressed identity for the algorithm itself, no mechanically-detectable drift. We close the gap. Algorithms become content-addressed mementos; language-specific lifters become verifiable refinement-claims; the substrate hosts its own production. We prove federation, drift detection, soundness preservation, and Cousot equivalence as nine lemmas. The substrate finally applies its first axiom to itself. |
There was a problem hiding this comment.
Port-count wording appears incorrect/inconsistent.
“five Python ports, five Rust ports, five C ports” conflicts with the rest of the paper/spec narrative (five total language ports). This reads like a copy error and should be corrected for clarity.
Proposed text fix
-... per-language reimplementations: five Python ports, five Rust ports, five C ports of the same algorithm ...
+... per-language reimplementations: one Python port, one Rust port, one C port, one Java port, and one Zig port of the same algorithm ...📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| > **What this paper argues.** That the substrate's first axiom — *Supra omnia, rectum*, above all correctness — has been load-bearing for substrate output but has not yet been applied to the substrate's own production mechanism. The lifters that emit substrate output have themselves been per-language reimplementations: five Python ports, five Rust ports, five C ports of the same algorithm, no canonical reference, no content-addressed identity for the algorithm itself, no mechanically-detectable drift. We close the gap. Algorithms become content-addressed mementos; language-specific lifters become verifiable refinement-claims; the substrate hosts its own production. We prove federation, drift detection, soundness preservation, and Cousot equivalence as nine lemmas. The substrate finally applies its first axiom to itself. | |
| > **What this paper argues.** That the substrate's first axiom — *Supra omnia, rectum*, above all correctness — has been load-bearing for substrate output but has not yet been applied to the substrate's own production mechanism. The lifters that emit substrate output have themselves been per-language reimplementations: one Python port, one Rust port, one C port, one Java port, and one Zig port of the same algorithm, no canonical reference, no content-addressed identity for the algorithm itself, no mechanically-detectable drift. We close the gap. Algorithms become content-addressed mementos; language-specific lifters become verifiable refinement-claims; the substrate hosts its own production. We prove federation, drift detection, soundness preservation, and Cousot equivalence as nine lemmas. The substrate finally applies its first axiom to itself. |
🧰 Tools
🪛 LanguageTool
[style] ~11-~11: To make your text as clear as possible to all readers, do not use this foreign term. Possible alternatives are “above”, “above-mentioned”, “aforementioned”, or “as previously mentioned” (in the document).
Context: ....** That the substrate's first axiom — Supra omnia, rectum, above all correctness —...
(SUPRA)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/papers/12-after-languages-how-proofir-represents-every-language.md` at
line 11, The phrase "five Python ports, five Rust ports, five C ports" in the
opening paragraph is inconsistent with the rest of the paper which asserts five
total language ports; replace that sequence with wording that matches the
intended meaning (e.g., "five language ports" or list the five languages once).
Locate the sentence beginning "**What this paper argues.**" and update the
fragment "five Python ports, five Rust ports, five C ports of the same
algorithm" to a corrected form such as "five language ports of the same
algorithm" (or an explicit single list of the five languages) so the port-count
matches the paper's narrative and removes the copy error.
Comment on lines
+33
to
+35
| ``` | ||
| A : ASTPattern × Context → IrFormula | ||
| ``` |
There was a problem hiding this comment.
Add language identifiers to fenced code blocks (MD040).
Several fenced blocks are missing a language tag, which is triggering markdownlint and reduces render/tooling quality.
Proposed spec fix
-```
+```text
A : ASTPattern × Context → IrFormula- +text
AlgorithmMemento ⊆ FunctionContractMemento where:
...
-```
+```text
BindingClaimMemento ⊆ FunctionContractMemento where:
...
- +json
AlgorithmCatalog := {
...
}
-```
+```text
∀ (i : LangAST). B.pre(i) →
...
- +text
B.post = forall i:LangAST.
...
-```
+```text
ASTProjectionMemento {
...
}
Also applies to: 51-63, 71-85, 103-109, 122-127, 131-137, 183-191
🧰 Tools
🪛 markdownlint-cli2 (0.22.1)
[warning] 33-33: Fenced code blocks should have a language specified
(MD040, fenced-code-language)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@protocol/specs/2026-05-09-algorithm-memento-protocol.md` around lines 33 -
35, Update the markdown fenced code blocks to include appropriate language
identifiers (e.g., ```text or ```json) to satisfy MD040; specifically add
language tags to the blocks containing "A : ASTPattern × Context → IrFormula",
the AlgorithmMemento and BindingClaimMemento sections (AlgorithmMemento ⊆
FunctionContractMemento and BindingClaimMemento ⊆ FunctionContractMemento), the
AlgorithmCatalog JSON block, the formal/assertion blocks referencing "∀ (i :
LangAST). B.pre(i) →" and "B.post = forall i:LangAST.", and the
ASTProjectionMemento block so each fenced block has the correct language hint
(use ```text for math/notation and ```json for AlgorithmCatalog).
Comment on lines
+84
to
+85
| - input_cids : [<algorithm_cid>] — must include the algorithm being bound | ||
| ``` |
There was a problem hiding this comment.
input_cids requirements are internally inconsistent.
Line 84-85 says input_cids “must include the algorithm being bound,” while Line 163-164 makes P_lang.cid mandatory in minting. This should be one normative rule to avoid incompatible emitters.
Proposed spec fix
- - input_cids : [<algorithm_cid>] — must include the algorithm being bound
+ - input_cids : [<algorithm_cid>, <projection_memento_cid>] — must include both the bound algorithm CID and the language projection CIDAlso applies to: 163-164
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@protocol/specs/2026-05-09-algorithm-memento-protocol.md` around lines 84 -
85, The spec currently has two conflicting normative requirements: "input_cids
must include the algorithm being bound" and a separate mandatory requirement for
P_lang.cid during minting; unify these into one rule by making "input_cids MUST
include the algorithm CID" the single normative requirement and update the
minting rules to derive/validate P_lang.cid from input_cids (or mark P_lang.cid
optional/derived), ensuring both references (input_cids and P_lang.cid in
minting) state the same requirement and include a brief sentence describing how
emitters should validate the algorithm CID against input_cids to avoid
incompatible emitters.
Comment on lines
+123
to
+127
| ∀ (i : LangAST). B.pre(i) → | ||
| ∃ (a : ASTPattern). P_lang.project(i) = Some(a) | ||
| ∧ A.pre(a) | ||
| ∧ B.post(i, ctx) = A.post(a, ctx) | ||
| ``` |
There was a problem hiding this comment.
ctx is free/unbound in the formal refinement formula.
The obligation quantifies i and a, but ctx is used without binding, making the formula formally ill-typed/ambiguous for implementation.
Proposed spec fix
-∀ (i : LangAST). B.pre(i) →
- ∃ (a : ASTPattern). P_lang.project(i) = Some(a)
- ∧ A.pre(a)
- ∧ B.post(i, ctx) = A.post(a, ctx)
+∀ (i : LangAST, ctx : Context). B.pre(i) →
+ ∃ (a : ASTPattern). P_lang.project(i) = Some(a)
+ ∧ A.pre(a)
+ ∧ B.post(i, ctx) = A.post(a, ctx)-B.post = forall i:LangAST.
+B.post = forall i:LangAST, ctx:Context.
B.pre(i) → ∃ a:ASTPattern.
P_lang.project(i) = Some(a)
∧ A.pre(a)
∧ B(i, ctx) = A(a, ctx)Also applies to: 132-137
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@protocol/specs/2026-05-09-algorithm-memento-protocol.md` around lines 123 -
127, The formula uses ctx without binding; fix by quantifying ctx and making the
postcondition a forall over contexts (e.g. add "∀ (ctx : CtxType)." so the
clause becomes ∀ (i : LangAST). B.pre(i) → ∃ (a : ASTPattern). P_lang.project(i)
= Some(a) ∧ A.pre(a) ∧ ∀ (ctx : CtxType). B.post(i, ctx) = A.post(a, ctx); apply
the same change to the analogous formula at lines 132-137 and ensure the same
CtxType (or explicit context sort) is used consistently for B.post and A.post.
Paper 13: After Grammars: Programming Languages as Content-Addressed Algebras. Extends paper 12 one level inward — not just algorithms become content-addressed mementos, but the LANGUAGES themselves do. Universal algebra and category theory established the math; this paper makes the algebras content-addressed and federated. Nine lemmas: L1 Signature CID Identity L2 Morphism Composition L3 Initial-Algebra Universality L4 Cross-Language Soundness via Homomorphism L5 Compilation Correctness as Homomorphism Discharge L6 Effect Signatures as Embedded Lawvere Theories L7 Equational Reasoning via Catalog Equations L8 Substrate Completeness for Algebraic Languages L9 Language Design as Algebra Construction Six counterarguments engaged. Companion spec LSP v0.1.0 (Language Signature Protocol): - SortMemento, EquationMemento, LanguageSignatureMemento, LanguageMorphismMemento wire shapes - Homomorphism obligation formalized - Catalog placement at protocol/language-catalog/ - Bootstrap path through v0.5.0 to mint signatures + morphisms for the existing ProvekIt language family After LSP lands, the substrate becomes the federation of programming language theory. Cross-language verification = morphism composition. Compiler correctness = morphism discharge receipt. Polyglot reasoning = graph traversal over the content-addressed catalog. The substrate's first axiom finally applies to the LANGUAGES it reasons about, not just to the contracts written in them. T Savo
This was referenced May 10, 2026
TSavo
added a commit
that referenced
this pull request
May 10, 2026
…ix input_cids, MD040, paper-12 port count Applies the still-valid AMP/LSP spec review nits from PR #544: - Bind `ctx` in the §2 refinement obligation (both the prose form and the IrFormula encoding): the formula now quantifies `(i : LangAST) (ctx : Context)` so it is a closed theorem, not an open formula that backends interpret inconsistently. - Define a deterministic `B.body_cid` normalization rule in §4 (was TBD): BLAKE3-512(JCS({ "files": <sorted-by-path array of { path: repo-relative POSIX path NFC-normalized, content_cid: BLAKE3-512 of the file bytes } })) -- order-independent, separator-free, byte-reproducible across producers. §1.3's body_cid field now points at the §4 rule. - Make the `input_cids` rule consistent: §1.3 now matches §4 step 5 -- [<algorithm_cid>, <projection_memento_cid>], must include both the bound algorithm CID and the language projection (P_lang) CID. - Tag the bare fenced code blocks in the AMP spec with a language id (markdownlint MD040). - Paper 12: fix the copy-error port count ("five Python ports, five Rust ports, five C ports") to "one Python port, one Rust port, one C port, one Java port, and one Zig port" (five total ports, one per language). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
3 tasks
TSavo
added a commit
that referenced
this pull request
May 10, 2026
spec(amp): address #544 review nits - bind ctx, normalize body_cid, fix input_cids, MD040, paper-12 port count
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Above all, correctness. The substrate's lifters have been the largest violation of the first axiom — same algorithm implemented independently across 5 language ports, no canonical reference. AMP makes algorithms content-addressed mementos and bindings verifiable refinement-claims. The substrate hosts its own production. See spec for the full design including formalized refinement relation, minting/discharge protocols, federation rule, worked example, relation to PPP/CCP/FRP/PEP. Design only — implementation comes after review. T Savo
Summary by CodeRabbit