feat: algebraic minter (AMP/LSP mementos) + provekit mint CLI#547
Conversation
…nt CLI Mints AlgorithmMemento, BindingMemento, SortMemento, EquationMemento, EffectSignatureMemento, LanguageSignatureMemento, LanguageMorphismMemento per AMP/LSP. Content-addressed CIDs via provekit-canonicalizer, Ed25519 signing (foundation v0, or --unsigned dev mode that refuses production catalog paths), catalog write per AMP §3 / LSP §3. Discharge is a separate step. 5 integration tests, fixtures, README. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
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 ignored due to path filters (1)
📒 Files selected for processing (25)
✨ 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: a9cd56afc3
ℹ️ 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".
| "reference `{s}` is neither a CID nor an existing spec path" | ||
| ))); | ||
| } | ||
| mint_spec_path(&path, signer, catalog, expected) |
There was a problem hiding this comment.
When a reference value is a path, this code always recurses into mint_spec_path without tracking an in-progress stack, so a self-reference or mutual reference cycle (for example two specs that point to each other via algorithm/input_cids) will recurse until stack overflow/abort instead of producing a validation error. This can hard-crash provekit mint on malformed input and block catalog generation.
Useful? React with 👍 / 👎.
| if existing.get("cid").and_then(Value::as_str) == Some(cid) | ||
| && existing.get("memento") == Some(payload) | ||
| { |
There was a problem hiding this comment.
The reuse path accepts an existing envelope whenever cid and memento match, but it does not validate the stored signature. If a file’s signature is tampered or corrupted while payload stays the same, reminting reports success and keeps the bad signature in place, leaving a catalog entry that later signature checks will fail to verify.
Useful? React with 👍 / 👎.
| if libprovekit::canonical::is_blake3_512_cid(s) { | ||
| return Ok(s.to_string()); | ||
| } |
There was a problem hiding this comment.
This early return accepts any syntactically valid CID before consulting the expected kind, so typed fields like formal_sorts/operations can silently ingest CIDs of the wrong memento type when passed directly as CIDs instead of paths. That produces structurally invalid cross-references in minted payloads that only fail downstream.
Useful? React with 👍 / 👎.
1 participant
Summary
New
provekit-mint-ampcrate plusprovekit mintCLI subcommands that mint the seven AMP/LSP memento kinds into the catalog:AlgorithmMemento,BindingMemento,SortMemento,EquationMemento,EffectSignatureMemento,LanguageSignatureMemento,LanguageMorphismMemento.provekit-canonicalizer(BLAKE3-512 of JCS canonical bytes).--signer PATH, or--unsigneddev mode which refuses to write to non-test catalog roots.LanguageSignatureMementocan citeSortMemento/AlgorithmMemento/EquationMementoCIDs, or paths the minter resolves recursively).discharge_status: "pending"; discharge (homomorphism/refinement obligations) is a separate step using the existing prove portfolio.5 integration tests (round-trip read by CID, deterministic CID across orderings, CID-collision refused, signature round-trips, unsigned refuses production path), fixtures, README.
cargo build,cargo test -p provekit-mint-amp(5 pass),cargo clippy -p provekit-mint-amp -- -D warningsall clean locally. Companion specs: AMP/LSP (already on main via #544).Test plan
cargo test -p provekit-mint-ampgreencargo clippy -p provekit-mint-amp -- -D warningscleanprovekit mint sort --spec <fixture> --unsigned --catalog /tmp/cprints<cid>\t<path>and round-trips🤖 Generated with Claude Code