[codex] refresh ProvekIt docs for v1.6.2 surfaces#480
Conversation
WalkthroughProvekIt protocol is bumped from v1.6.0 to v1.6.2. A new lift-plugin-protocol contract-set constant is introduced and pinned in the self-contracts library. Twelve language kit CI job results are recorded as accepted witnesses in the CICP artifact store. Comprehensive documentation is refreshed across explanations, how-tos, references, tutorials, contributing guides, and security sections to reflect the v1.6.2 version and new protocol features. ChangesProtocol v1.6.2 & Lift-Plugin CID Pinning
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Possibly related PRs
Poem
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
|
TSavo
force-pushed
the
codex/centralize-protocol-pin
branch
from
064e433 to
224aeac
Compare
TSavo
changed the title
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 3
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
implementations/rust/provekit-self-contracts/src/lib.rs (1)
126-144:⚠️ Potential issue | 🟡 Minor | ⚡ Quick winDoc comment says "C1-C8" but
LIFT_PLUGIN_PROTOCOL_CONTRACT_NAMEShas 11 entries.The phrase "lift-plugin-protocol C1-C8" implies 8 contracts; the array has 11. The comment does say "split into concrete contract facets," which allows more than 8 facets, but the range annotation will still mislead contributors counting entries to validate coverage. Consider replacing "C1-C8" with the actual clause-to-facet mapping (e.g., "11 facets spanning spec clauses C1–C8") or removing the range entirely.
📝 Proposed fix
-/// The standard protocol-contract slab: lift-plugin-protocol C1-C8, split -/// into the concrete contract facets authored by `lift_plugin_protocol.rs`. +/// The standard protocol-contract slab: 11 facets covering lift-plugin-protocol +/// spec clauses C1–C8, authored by `lift_plugin_protocol.rs`.🤖 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 `@implementations/rust/provekit-self-contracts/src/lib.rs` around lines 126 - 144, Update the doc comment above the constant LIFT_PLUGIN_PROTOCOL_CONTRACT_NAMES to stop claiming "C1-C8" implies exactly eight contracts; instead state the actual mapping/size (e.g., "11 facets spanning spec clauses C1–C8" or simply "11 facets") so the comment matches the array contents and avoids misleading readers counting entries. Ensure the wording still notes these are concrete facets split from lift_plugin_protocol, and keep the reference to the stable ordering.
🧹 Nitpick comments (3)
docs/reference/error-codes.md (1)
20-23: 💤 Low valueMinor style note: repetitive sentence structure is acceptable here.
The static analysis tool flagged the repetitive "Use" sentence beginnings in the emission rules. While this creates parallel structure, it's appropriate and effective for a technical reference that enumerates rule categories. The parallel construction makes the severity-level rules easy to scan and compare.
🤖 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/reference/error-codes.md` around lines 20 - 23, The repeated "Use" sentence starters for the emission rules (lines referencing 'error', 'warning', 'information', 'hint') are intentional for parallel, scannable documentation — leave the four bullet lines unchanged; if you want to address the static analysis warning, add a single brief author note above or below the list (one sentence) stating that the repetition is intentional for readability, rather than rewording the bullets themselves.docs/contributing/release-process.md (1)
125-125: ⚡ Quick winMake the planned governance reference navigable in “Read next”.
This item is rendered as inline code, so it can’t be followed like the other entries. Consider converting it to a Markdown link (or a TODO issue link) for consistent navigation.
🤖 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/contributing/release-process.md` at line 125, In the "Read next" section replace the inline code entry `docs/governance/protocol-versions.md` (planned): version policy. with a proper Markdown link (or a TODO issue-style link) so it is navigable; locate the exact string in the "Read next" list in docs/contributing/release-process.md and change it to a link like [docs/governance/protocol-versions.md (planned): version policy](docs/governance/protocol-versions.md) or an appropriate placeholder link if the file is not yet published.bug-zoo/README.md (1)
5-5: 💤 Low valueConsider breaking this sentence into multiple sentences for improved readability.
This 50+ word sentence packs a lot of technical detail. While accurate, splitting it into 2-3 shorter sentences would make the concept easier to parse on first reading.
📝 Suggested refactor for readability
-A normal bug corpus says: this project failed, and this patch fixed it. Bug Zoo asks for a stronger receipt: can ProvekIt rediscover the missing obligation from the code, framework metadata, schemas, or annotations already present; name that obligation by CID; and accept a repair only after the repaired artifact re-lifts to a closed proof graph? +A normal bug corpus says: this project failed, and this patch fixed it. Bug Zoo asks for a stronger receipt. Can ProvekIt rediscover the missing obligation from the code, framework metadata, schemas, or annotations already present? Can it name that obligation by CID and accept a repair only after the repaired artifact re-lifts to a closed proof graph?🤖 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 `@bug-zoo/README.md` at line 5, The README contains one long 50+ word sentence starting "A normal bug corpus says: this project failed, and this patch fixed it..." that should be split into 2–3 shorter sentences for readability; edit the sentence in bug-zoo/README.md to break the ideas into separate sentences (e.g., one stating what a normal bug corpus does, a second asking whether ProvekIt can rediscover the missing obligation from code/framework metadata/schemas/annotations, and a third about naming the obligation by CID and accepting a repair only after the repaired artifact re-lifts to a closed proof graph) so each clause is clearer and flows logically.
🤖 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/contributing/build.md`:
- Around line 15-16: The two pseudocode lines "provekit ci ..." and "provekit
zoo ..." are incorrectly placed inside the "Make targets" sh code block; remove
those lines from the existing Make targets block and create a short separate
section (or a details/summary snippet) titled like "Additional CI commands (not
make targets)" that shows concrete examples using the real commands "provekit ci
check/shadow/result/reuse" and "provekit zoo [--all]" with brief comments;
ensure the Make targets block only contains actual make targets or valid shell
commands and that the new block clearly indicates these are non-make helper
commands.
In `@docs/explanation/compared-to/kani-prusti-creusot.md`:
- Line 142: The sentence currently reads in present tense for the planned
adapter "provekit-lift-kani"; change the phrasing to conditional or future tense
(for example, replace "walks" with "would walk" or "will walk") so the file's
status remains consistent; update the line referencing provekit-lift-kani to use
the chosen conditional/future verb to avoid implying the adapter already ships.
In `@docs/reference/lsp-plugin-protocol.md`:
- Around line 9-10: The doc is ambiguous about request vs response envelopes:
clarify that request messages include {id, method, params?} while responses
include {id, result? , error?} and do not require a method; update the two
sentences so the first explicitly describes the request envelope (mentioning
`id`, `method`, optional `params`) and the second explicitly describes the
response envelope (same `id` and either `result` or `error` without `method`),
using the exact field names (`id`, `method`, `params`, `result`, `error`) to
avoid ambiguity for helper/plugin implementers.
---
Outside diff comments:
In `@implementations/rust/provekit-self-contracts/src/lib.rs`:
- Around line 126-144: Update the doc comment above the constant
LIFT_PLUGIN_PROTOCOL_CONTRACT_NAMES to stop claiming "C1-C8" implies exactly
eight contracts; instead state the actual mapping/size (e.g., "11 facets
spanning spec clauses C1–C8" or simply "11 facets") so the comment matches the
array contents and avoids misleading readers counting entries. Ensure the
wording still notes these are concrete facets split from lift_plugin_protocol,
and keep the reference to the stable ordering.
---
Nitpick comments:
In `@bug-zoo/README.md`:
- Line 5: The README contains one long 50+ word sentence starting "A normal bug
corpus says: this project failed, and this patch fixed it..." that should be
split into 2–3 shorter sentences for readability; edit the sentence in
bug-zoo/README.md to break the ideas into separate sentences (e.g., one stating
what a normal bug corpus does, a second asking whether ProvekIt can rediscover
the missing obligation from code/framework metadata/schemas/annotations, and a
third about naming the obligation by CID and accepting a repair only after the
repaired artifact re-lifts to a closed proof graph) so each clause is clearer
and flows logically.
In `@docs/contributing/release-process.md`:
- Line 125: In the "Read next" section replace the inline code entry
`docs/governance/protocol-versions.md` (planned): version policy. with a proper
Markdown link (or a TODO issue-style link) so it is navigable; locate the exact
string in the "Read next" list in docs/contributing/release-process.md and
change it to a link like [docs/governance/protocol-versions.md (planned):
version policy](docs/governance/protocol-versions.md) or an appropriate
placeholder link if the file is not yet published.
In `@docs/reference/error-codes.md`:
- Around line 20-23: The repeated "Use" sentence starters for the emission rules
(lines referencing 'error', 'warning', 'information', 'hint') are intentional
for parallel, scannable documentation — leave the four bullet lines unchanged;
if you want to address the static analysis warning, add a single brief author
note above or below the list (one sentence) stating that the repetition is
intentional for readability, rather than rewording the bullets themselves.
🪄 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: 419fa9d6-ed4a-4c68-82c9-8161c80f5c98
📒 Files selected for processing (65)
.github/workflows/ci.yml.provekit/ci/README.md.provekit/ci/accepted/c/blake3-512:62a0c412512c0caadb734ef89dbe037a9c8125edc9f7f0dcd553bafdc3d1ec4b9d0ffd1e6267a625e6a006f7d15ed542f9fee045ba4c2990e5bb67806a3622c6.job-result.json.provekit/ci/accepted/cpp/blake3-512:5fbd5e703372ba39f1fecb111a87a3290e206bee7cab1d71dc6b590772a8ed6cd25aca7a3250f15217bd04184b3af5e771038f0953491b77bce1ac43d13cc854.job-result.json.provekit/ci/accepted/csharp/blake3-512:7b18a2a1208030708fc0f181950e3924fba180c015c12a24883a1643b1782ed88949e14fdb75532faa4b9cd82bbc7052eb7c54265053983ed947ab2093b4d6c0.job-result.json.provekit/ci/accepted/go/blake3-512:d0c24f41b43f77a2f29ea7bc7bcfa27843e63849069042f46738b08342e8038fe8c46ce3adb3034058cbd8b981355bdc0b7729f1a7fc185b73ac8b759cf2216b.job-result.json.provekit/ci/accepted/java/blake3-512:65ff1380c69021005518cb24fdfd183deaca60fe4e1ea18c6f9461e96c9616bf6bd4a285e69a84242de09408e821db89a04c0774b1f3124946b95b5bf24d9119.job-result.json.provekit/ci/accepted/python/blake3-512:e68d4db0b26dc2204eea435724e86bbb5857b681a587bba6a8cec5cdc2895103ede4e3e0cf69a67d246b119397064799091ed04b4de5c5e90f710e539a3d12c4.job-result.json.provekit/ci/accepted/ruby/blake3-512:53c2f0158f55a1da14b1ede806ace042a0f73a77adf08c348ff617a95fcb221096f2325c49e7332f45694f8e9bf69017f0cc5a392422de77492a13a48551c7a2.job-result.json.provekit/ci/accepted/rust/blake3-512:445c29af52235d5b3f15c1bf8b5c3a1e183ea6c12501a1556bab5c4e76a17b37add44a47122a4246eb46b65f24dd65a3761654e1a0b22236853e29c8e492da8f.job-result.json.provekit/ci/accepted/rust/blake3-512:49b8ecbb4465dbc370c5a0c81634e7edf89eef4ab93a7617d185061579e4958af9c263e7c3f60cef42184a226cf47611ed69bfdf0a97ff72386ecf1ed9541897.job-result.json.provekit/ci/accepted/swift/blake3-512:df2d6ae49a9d3bc105cad278ddf2d7e7091ca3549d33b36e3b561a978700ddeb96deb30b13c31533ae9e41cd35905ce4a77ca4aa4620a0d2bc00dcdb6bd96211.job-result.json.provekit/ci/accepted/ts/blake3-512:def5c32342ef31dc04c1a33a878e8c0e5aa6dc935398b5ebcb06d4dbb409f78329d7a36dbe57994f113d0c198c49463d65e5a4c3637f7e615180155e600c33ab.job-result.json.provekit/ci/accepted/zig/blake3-512:4f1a87bbd96d3c593f8f1e279e36f32d3abb46071e79ffcec2a9390f7293f0910c3078fd4e4c06f3b2749489366a9a4b70278c3526ac9a6945b2b970b168649b.job-result.jsonMakefileREADME.mdbug-zoo/README.mdbug-zoo/species/BZ-SHAPE-005-java-null-boundary-equivalence/README.mddocs/contributing/build.mddocs/contributing/proposing-a-spec-change.mddocs/contributing/release-process.mddocs/contributing/writing-a-kit/02-canonicalizer.mddocs/contributing/writing-an-LSP-plugin.mddocs/explanation/architecture.mddocs/explanation/compared-to/kani-prusti-creusot.mddocs/explanation/landing.mddocs/explanation/pitch.mddocs/explanation/product.mddocs/explanation/use-cases.mddocs/how-to/bug-zoo.mddocs/how-to/content-addressed-ci.mddocs/how-to/cross-domain-bridges.mddocs/how-to/debugging-a-failed-handshake.mddocs/how-to/ide-integration/jetbrains.mddocs/how-to/ide-integration/neovim.mddocs/how-to/ide-integration/overview.mddocs/how-to/ide-integration/vscode.mddocs/index.mddocs/papers/README.mddocs/quickstart-end-user.mddocs/quickstart-extender.mddocs/reference/cids.mddocs/reference/error-codes.mddocs/reference/ir/canonical-form.mddocs/reference/lsp-plugin-protocol.mddocs/reference/per-language-status.mddocs/reference/protocol-extensions.mddocs/security/supply-chain.mddocs/tutorials/c.mddocs/tutorials/cpp.mddocs/tutorials/csharp.mddocs/tutorials/go.mddocs/tutorials/java.mddocs/tutorials/python.mddocs/tutorials/ruby.mddocs/tutorials/rust.mddocs/tutorials/swift.mddocs/tutorials/typescript.mddocs/tutorials/zig.mdimplementations/rust/libprovekit/README.mdimplementations/rust/provekit-cli/tests/mint_kit_integration.rsimplementations/rust/provekit-self-contracts/src/lib.rsprotocol/conformance/cicp/README.mdprotocol/evolution/README.mdtools/cross-kit-conformance/src/lib.rs
| provekit ci ... # CICP supply-chain admission and result witnesses | ||
| provekit zoo ... # Bug Zoo specimen/exposure/dropper checks |
There was a problem hiding this comment.
provekit commands are misplaced in the Make targets block.
Lines 15–16 (provekit ci ... and provekit zoo ...) appear inside the sh code block under the "Make targets" heading, but they are neither make targets nor valid shell invocations — the ... placeholder is pseudocode. A contributor following this section literally would be confused.
Consider breaking these out into a short separate block, e.g.:
📝 Proposed fix
make clean # remove all build artifacts+Additional CI commands (not make targets):
+sh +provekit ci check/shadow/result/reuse # CICP supply-chain admission and result witnesses +provekit zoo [--all] # Bug Zoo specimen/exposure/dropper checks +
and removing lines 15–16 from the existing `make` block.
</details>
<details>
<summary>🤖 Prompt for AI Agents</summary>
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/contributing/build.md around lines 15 - 16, The two pseudocode lines
"provekit ci ..." and "provekit zoo ..." are incorrectly placed inside the "Make
targets" sh code block; remove those lines from the existing Make targets block
and create a short separate section (or a details/summary snippet) titled like
"Additional CI commands (not make targets)" that shows concrete examples using
the real commands "provekit ci check/shadow/result/reuse" and "provekit zoo
[--all]" with brief comments; ensure the Make targets block only contains actual
make targets or valid shell commands and that the new block clearly indicates
these are non-make helper commands.
</details>
<!-- fingerprinting:phantom:poseidon:churro -->
<!-- 4e71b3a2 -->
<!-- This is an auto-generated comment by CodeRabbit -->
| With ProvekIt: | ||
|
|
||
| 1. `provekit-lift-kani` (planned for v1.2) walks `#[kani::proof]` and lifts to canonical IR. | ||
| 1. `provekit-lift-kani` walks `#[kani::proof]` and lifts to canonical IR. |
There was a problem hiding this comment.
Clarify hypothetical wording to avoid implying the adapter already ships.
Line 142 uses present tense (“walks”), but this file still marks provekit-lift-kani as planned elsewhere. Consider switching to conditional/future wording (e.g., “would walk”) to keep status consistent.
🤖 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/explanation/compared-to/kani-prusti-creusot.md` at line 142, The
sentence currently reads in present tense for the planned adapter
"provekit-lift-kani"; change the phrasing to conditional or future tense (for
example, replace "walks" with "would walk" or "will walk") so the file's status
remains consistent; update the line referencing provekit-lift-kani to use the
chosen conditional/future verb to avoid implying the adapter already ships.
| - Each message has an `id`, `method`, and optional `params`. | ||
| - Responses carry the same `id` with either `result` or `error`. |
There was a problem hiding this comment.
Clarify request vs response envelope to avoid protocol ambiguity.
Line 9 implies all messages require method, but Line 10 defines responses as {id, result|error}. This contradiction can lead to incompatible helper/plugin implementations.
Suggested wording fix
-- Each message has an `id`, `method`, and optional `params`.
-- Responses carry the same `id` with either `result` or `error`.
+- Requests use `{ "id", "method", "params"? }`.
+- Responses use `{ "id", "result" }` or `{ "id", "error" }`.📝 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.
| - Each message has an `id`, `method`, and optional `params`. | |
| - Responses carry the same `id` with either `result` or `error`. | |
| - Requests use `{ "id", "method", "params"? }`. | |
| - Responses use `{ "id", "result" }` or `{ "id", "error" }`. |
🤖 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/reference/lsp-plugin-protocol.md` around lines 9 - 10, The doc is
ambiguous about request vs response envelopes: clarify that request messages
include {id, method, params?} while responses include {id, result? , error?} and
do not require a method; update the two sentences so the first explicitly
describes the request envelope (mentioning `id`, `method`, optional `params`)
and the second explicitly describes the response envelope (same `id` and either
`result` or `error` without `method`), using the exact field names (`id`,
`method`, `params`, `result`, `error`) to avoid ambiguity for helper/plugin
implementers.
Summary
Refreshes ProvekIt documentation around the current v1.6.2 protocol/tooling surface and the broader product framing: a toolchain for proving content-addressed claims, with software correctness across domains as the center use case.
What changed
Validation
python3relative-link check over changed/new Markdown files: 48 files checked, all links resolve.git diff --checkcargo run --release --manifest-path tools/recompute-spec-cids/Cargo.toml -- --verifycargo run --release --manifest-path implementations/rust/Cargo.toml --bin provekit -- ci check --body protocol/conformance/cicp/job-result-pass.jsoncargo run --release --manifest-path implementations/rust/Cargo.toml --bin provekit -- zooNotes: the Rust/Maven commands still emit existing warnings from generated/compiler/self-contract code and Maven shading; the commands exit successfully.
Summary by CodeRabbit
Release Notes
Documentation
Updates