spec(amp): address #544 review nits - bind ctx, normalize body_cid, fix input_cids, MD040, paper-12 port count#565
Conversation
…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>
|
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 (2)
✨ 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 |
Summary
Applies the still-valid AMP/LSP spec review nits flagged on PR #544 (CodeRabbit + Codex):
ctxin the §2 refinement obligation (P1/Major): the formula previously usedctxfree, making it an open formula that backends interpret inconsistently. Both the prose form and the IrFormula encoding now quantify(i : LangAST) (ctx : Context), so it is a closed theorem.B.body_cidnormalization rule in §4 (P2): wasTBD. NowBLAKE3-512(JCS({ "files": <sorted-by-path array of { "path": repo-relative POSIX path NFC-normalized, "content_cid": "blake3-512:" + lowercase-hex(BLAKE3-512(<raw file bytes>)) } }))-- order-independent, separator-free, byte-reproducible across producers and platforms. §1.3'sbody_cidfield now points at the §4 rule.input_cidsrule consistent (Major): §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.text/json).Spec/docs only; no code. The remaining em-dashes in the AMP spec's field listings (
effects,body_cid,locus) are pre-existing and out of scope here -- a separate em-dash cleanup pass can take them.Test plan
grep -P '[—–]'over the changed lines returns nothingctx)🤖 Generated with Claude Code