feat(spec): grow IR Sort grammar — FunctionSort + DependentSort (closes #329)#348
Merged
Conversation
|
Warning Rate limit exceeded
To keep reviews running without waiting, you can enable usage-based add-on for your organization. This allows additional reviews beyond the hourly cap. Account admins can enable it under billing. ⌛ 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 (9)
WalkthroughThe PR extends the IR Sort grammar to include FunctionSort and DependentSort variants, updates the formal specification and protocol catalog, and adds multi-project verification with call-edge tracking infrastructure. This includes new call-edge loading and processing logic in the verifier, configuration-driven and CLI-driven extra-project discovery, pool merging, and call-edge reporting across JSON and pretty-printed outputs. ChangesIR Grammar Extension
Call Edge Tracking & Multi-Project Verification
Sequence DiagramsequenceDiagram
participant User as User / CLI
participant CLI as provekit-cli
participant Config as ProjectConfig
participant Verifier as provekit-verifier
participant FSys as File System
participant Report as Report
User->>CLI: provekit prove [--with extra/proj]
CLI->>Config: read_project_config(project_root)
Config-->>CLI: ProjectConfig { callees: [...] }
CLI->>CLI: Build extra_projects from CLI args + callees
CLI->>Verifier: Runner::new(RunnerConfig { extra_projects, ... })
Verifier->>FSys: Load proofs from project_root
FSys-->>Verifier: Primary proofs
loop For each extra_project
Verifier->>FSys: load_all_proofs::run(extra_project)
FSys-->>Verifier: Additional proofs
Verifier->>Verifier: Merge pools (contract-name indexes)
end
Verifier->>FSys: load_call_edge_files(project_root)
FSys-->>Verifier: Call-edge JSON array
Verifier->>Verifier: process_call_edges(edges, merged_pool)
Verifier->>Verifier: Resolve source/target CIDs via pool indexes
Verifier->>Report: Populate report.call_edges with resolved edges
Report-->>CLI: Complete report with call edges
CLI->>CLI: Format report (JSON + pretty-print)
CLI-->>User: Output with call edges section
Estimated code review effort🎯 3 (Moderate) | ⏱️ ~25 minutes Possibly related issues
Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 3 | ❌ 2❌ Failed checks (2 warnings)
✅ Passed checks (3 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 |
There was a problem hiding this comment.
Pull request overview
This PR extends the IR Sort spec to include FunctionSort and DependentSort (with locked key orders and updated invariants/examples), and also introduces Rust-side verifier/CLI changes aimed at cross-project proof loading and call-edge ingestion/reporting.
Changes:
- Update
Sortgrammar in both CDDL and the formal-grammar spec to addFunctionSort+DependentSort, renamedomain/range→args/return, and document locked key orders and examples. - Add Rust verifier support for loading additional
.proofdirectories and reading.call-edges.jsonfiles, plus CLI/report plumbing. - Add a Rust binary to emit C-kit fixtures and commit new self-contracts attestation JSON files.
Reviewed changes
Copilot reviewed 14 out of 15 changed files in this pull request and generated 9 comments.
Show a summary per file
| File | Description |
|---|---|
| protocol/specs/2026-04-30-ir-formal-grammar.md | Documents new Sort variants, invariants, locked key orders, and examples. |
| protocol/provekit-ir.cddl | Extends Sort union to include FunctionSort and DependentSort. |
| implementations/rust/provekit-verifier/src/types.rs | Adds contract-name indexes and call-edge report types; adds MementoPool::merge. |
| implementations/rust/provekit-verifier/src/runner.rs | Loads extra projects; loads/processes call edges; records them in report. |
| implementations/rust/provekit-verifier/src/lib.rs | Exposes new call_edge_loader module. |
| implementations/rust/provekit-verifier/src/call_edge_loader.rs | New loader/processor for .call-edges.json files. |
| implementations/rust/provekit-cli/src/report_fmt.rs | Adds callEdges to JSON + pretty output. |
| implementations/rust/provekit-cli/src/project_config.rs | Adds [verify].callees config parsing. |
| implementations/rust/provekit-cli/src/main.rs | Adds prove --with ... CLI flag for extra project dirs. |
| implementations/rust/provekit-cli/src/cmd_prove.rs | Wires config/flag into verifier extra_projects. |
| implementations/rust/provekit-cli/src/cmd_mint.rs | Persists callEdges from lift responses into .call-edges.json files. |
| implementations/rust/provekit-claim-envelope/src/bin/emit_c_fixtures.rs | New fixture emitter binary for C-kit byte-equivalence tests. |
| implementations/rust/Cargo.lock | Adds walkdir dependency (workspace) for verifier traversal. |
| implementations/rust/.provekit/self-contracts-attestations/rust.json | Adds/updates on-disk self-contracts attestation for Rust kit. |
| implementations/rust/.provekit/self-contracts-attestations/openapi.json | Adds/updates on-disk self-contracts attestation for OpenAPI kit. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+144
to
+147
| for (source_cid, target_cid, locus) in &call_edge_loader::process_call_edges( | ||
| &call_edges, | ||
| &pool, | ||
| ) { |
Comment on lines
33
to
37
| use crate::types::{CallSite, MementoPool, ObligationVerdict, Report}; | ||
| use crate::{ | ||
| enumerate_callsites, instantiate, load_all_proofs, report as report_stage, resolve_target, | ||
| smt_emitter, | ||
| call_edge_loader, enumerate_callsites, instantiate, load_all_proofs, report as report_stage, | ||
| resolve_target, smt_emitter, | ||
| }; |
Comment on lines
+558
to
+562
| let json_str = serde_json::to_string(&edges_json).unwrap_or_default(); | ||
| let json_cid = provekit_canonicalizer::blake3_512_of(json_str.as_bytes()); | ||
| let json_path = out_dir.join(format!("{json_cid}.call-edges.json")); | ||
|
|
||
| if let Err(e) = std::fs::write(&json_path, &json_str) { |
Comment on lines
+27
to
+38
| let mut extra_projects: Vec<PathBuf> = args | ||
| .with | ||
| .iter() | ||
| .map(PathBuf::from) | ||
| .collect(); | ||
|
|
||
| for callee in &cfg_doc.callees { | ||
| let p = project_root.join(callee); | ||
| if p.exists() { | ||
| extra_projects.push(p); | ||
| } | ||
| } |
Comment on lines
+257
to
+276
| self.mementos.insert(memento_cid.clone(), envelope); | ||
|
|
||
| // Index by contract name for cross-kit resolution | ||
| let name = self.mementos | ||
| .get(&memento_cid) | ||
| .and_then(|env| { | ||
| env.pointer("/header/contractName") | ||
| .or_else(|| env.pointer("/header/name")) | ||
| .or_else(|| env.pointer("/evidence/body/contractName")) | ||
| .or_else(|| env.pointer("/evidence/body/name")) | ||
| .or_else(|| env.get("header").and_then(|h| h.get("name"))) | ||
| .or_else(|| env.get("header").and_then(|h| h.get("contractName"))) | ||
| }) | ||
| .and_then(|v| v.as_str()); | ||
|
|
||
| if let Some(n) = name { | ||
| let n = n.to_string(); | ||
| self.cid_to_name.insert(memento_cid.clone(), n.clone()); | ||
| self.name_to_cid.insert(n, memento_cid); | ||
| } |
Comment on lines
+321
to
+331
| /// Merge another pool into this one. | ||
| pub fn merge(&mut self, other: Self) { | ||
| self.mementos.extend(other.mementos); | ||
| self.formula_to_memento.extend(other.formula_to_memento); | ||
| self.bridges_by_symbol.extend(other.bridges_by_symbol); | ||
| for (k, vs) in other.bundle_members { | ||
| self.bundle_members.entry(k).or_default().extend(vs); | ||
| } | ||
| self.load_errors.extend(other.load_errors); | ||
| self.cid_to_name.extend(other.cid_to_name); | ||
| self.name_to_cid.extend(other.name_to_cid); |
| **DependentSort** (Section: Sorts) | ||
| | Invariant | Formula | | ||
| |-----------|---------| | ||
| | ValidFields | `∀s → HasKey("name")∧tstr(name) ∧ HasKey("indexVar")∧tstr(indexVar) ∧ HasKey("indexSort")∧IsSort(indexSort)` | |
Comment on lines
+100
to
+108
| let proof_input = ProofEnvelopeInput { | ||
| name: "@provekit/c-test".into(), | ||
| version: "0.0.1".into(), | ||
| binary_cid: None, | ||
| metadata: None, | ||
| members, | ||
| signer_cid: pubkey_str.clone(), | ||
| signer_seed: SEED, | ||
| declared_at: PRODUCED_AT.into(), |
Comment on lines
+132
to
+141
| // Load contracts from extra project dirs (e.g., OpenAPI spec) | ||
| for extra in &self.cfg.extra_projects { | ||
| let extra_pool = load_all_proofs::run(extra); | ||
| pool.merge(extra_pool); | ||
| } | ||
|
|
||
| // Load and process call edges | ||
| let call_edges = | ||
| call_edge_loader::load_call_edge_files(&self.cfg.project_root); | ||
| let obligations = call_edge_loader::process_call_edges(&call_edges, &pool); |
2 tasks
TSavo
force-pushed
the
feat/329-ir-sort-grammar-grow
branch
from
147d8fa to
ab4a510
Compare
- cmd_mint saves callEdges from RPC response as .call-edges.json - load_all_proofs indexes contracts by name for cross-kit resolution - call_edge_loader module: loads .call-edges.json, resolves targets - MementoPool::merge for combining multiple proof sources - RunnerConfig.extra_projects for --with <dir> flag - provekit prove --with <other-dir> loads contracts from both dirs - report_fmt shows resolved call edges in output
Developers specify upstream contract directories in their project config instead of passing --with on every invocation. CLI --with flag still works as an override/additive. [verify] callees = ["../api-project/", "../shared/"]
#329) CDDL (protocol/provekit-ir.cddl): Sort = PrimitiveSort / FunctionSort / DependentSort FunctionSort: {kind, args[+ Sort], return: Sort} DependentSort: {kind, name, indexVar, indexSort} Formal grammar (2026-04-30-ir-formal-grammar.md): - Updated FunctionSort BNF: domain->args, range->return - Added DependentSort BNF with locked key order - Updated invariants: ValidArgsAndReturn, ValidFields - 4 grammar-level examples (2 per variant, minimal + nested) Locked per #329. PrimitiveSortName unchanged. No per-kit IR types.
The CDDL/spec edits for FunctionSort + DependentSort change the canonical bytes of `2026-04-30-ir-formal-grammar.md`, so its catalog pin in `2026-04-30-protocol-catalog.json` needs to advance to the new BLAKE3-512. CI conformance gate (`recompute-spec-cids --verify`) was failing with the on-disk vs. recomputed CID drift; this commit restores it. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
force-pushed
the
feat/329-ir-sort-grammar-grow
branch
from
1f8c78c to
5791011
Compare
The RunnerConfig::extra_projects field was added by this branch but the example (stage4_driver.rs) and test (multi_solver_modes.rs) that construct RunnerConfig manually were not updated, leaving them with E0063 "missing field" build errors. Both call sites now set `extra_projects: Vec::new()` (the empty default, matching the default-derived behavior elsewhere). This unblocks the conformance gate's `make test-rust` step and lets #348 turn green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Owner
Author
|
CI now failing on a different bug after the call-site fix landed. Confirmed:
So this is something specific to the substrate changes in #348 — most likely the Dispatching to opencode for diagnosis. |
Two attestation files were accidentally checked in at `implementations/rust/.provekit/self-contracts-attestations/` (rust.json + openapi.json). The canonical attestation home is the workspace root `.provekit/self-contracts-attestations/`, which still holds the authoritative copies. The kit-local copies broke the `mint_kit_integration` rust tests because the test's scratch tempdir uses `symlink_contents` to mirror each kit's children. With kit-local attestation files present, the mint pipeline's `find_attestation_dir` walk-up canonicalizes through the symlinks, hits the kit-local dir, and writes the new attestation back into the canonical repo instead of the scratch's writable attestation directory. The test then can't find it inside the scratch and panics. Removing the kit-local copies restores the test (verified locally). Closes the regression introduced when these files were added in this branch's `feat(config): add [verify] callees` commit. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 7
🧹 Nitpick comments (3)
implementations/rust/provekit-claim-envelope/src/bin/emit_c_fixtures.rs (1)
66-68: ⚡ Quick winRepeated hex-encoding inline — consider extracting a helper.
The same byte-to-hex pattern appears three times:
let hex: String = <iter>.map(|b| format!("{:02x}", b)).collect();Extracting it reduces noise and prevents drift if the encoding format changes.
♻️ Proposed refactor
+fn to_hex(bytes: &[u8]) -> String { + bytes.iter().map(|b| format!("{:02x}", b)).collect() +} + fn main() { ... - let raw_sig = ed25519_sign_with_seed(&SEED, b"hello"); - let hex: String = raw_sig.iter().map(|b| format!("{:02x}", b)).collect(); + let raw_sig = ed25519_sign_with_seed(&SEED, b"hello"); + let hex = to_hex(&raw_sig); ... - let hex: String = m.canonical_bytes.iter().map(|b| format!("{:02x}", b)).collect(); + let hex = to_hex(&m.canonical_bytes); ... - let hex: String = proof_out.bytes.iter().map(|b| format!("{:02x}", b)).collect(); + let hex = to_hex(&proof_out.bytes);Also applies to: 87-89, 111-113
🤖 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-claim-envelope/src/bin/emit_c_fixtures.rs` around lines 66 - 68, The code repeats the byte-to-hex conversion (e.g., let hex: String = raw_sig.iter().map(|b| format!("{:02x}", b)).collect();) in multiple places (around usages with raw_sig and the other print blocks at the later occurrences); extract a small helper like fn to_hex(bytes: &[u8]) -> String and replace each inline map/collect with to_hex(&raw_sig) (and the other byte slices), and update the println calls (e.g., the ED25519_SIG_HELLO_RAW_HEX printing block and the two other blocks at the referenced spots) to use the helper to keep encoding logic centralized and consistent.implementations/rust/provekit-verifier/src/runner.rs (1)
139-147: ⚡ Quick winAvoid recomputing processed call edges
Line 141 already computes
obligations, but Lines 144-147 callprocess_call_edgesagain. Reuse the first result to remove duplicate work and the currently-unused local.Suggested cleanup
- let obligations = call_edge_loader::process_call_edges(&call_edges, &pool); + let obligations = call_edge_loader::process_call_edges(&call_edges, &pool); // Report call edge obligations - for (source_cid, target_cid, locus) in &call_edge_loader::process_call_edges( - &call_edges, - &pool, - ) { + for (source_cid, target_cid, locus) in &obligations { let file = locus .as_ref() .and_then(|l| l.get("file")) .and_then(|f| f.as_str()) .unwrap_or("<unknown>");🤖 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-verifier/src/runner.rs` around lines 139 - 147, You are recomputing processed call edges: remove the second call to call_edge_loader::process_call_edges(&call_edges, &pool) and iterate over the already-computed obligations variable instead (e.g., for (source_cid, target_cid, locus) in &obligations { ... }). Also remove any now-unused local(s) introduced by the duplicate call so the code uses the single obligations result from the earlier call to call_edge_loader::process_call_edges.implementations/rust/provekit-cli/src/cmd_prove.rs (1)
506-517: ⚡ Quick winNormalize
--withand[verify].calleespaths consistently; don’t silently skip missing entries.Line 506 currently treats
--withas raw paths, while Line 513 resolves config callees relative toproject_root. Also, missing callee dirs are ignored with no signal. This can quietly shrink verification scope.Suggested patch
- let mut extra_projects: Vec<PathBuf> = args - .with - .iter() - .map(PathBuf::from) - .collect(); + let mut extra_projects: Vec<PathBuf> = Vec::new(); + for p in args.with.iter().map(PathBuf::from) { + let p = if p.is_absolute() { p } else { project_root.join(p) }; + if p.exists() { + extra_projects.push(p); + } else { + eprintln!( + "{}: --with path does not exist: {}", + "warning".yellow().bold(), + p.display() + ); + } + } for callee in &cfg_doc.callees { let p = project_root.join(callee); if p.exists() { extra_projects.push(p); + } else { + eprintln!( + "{}: configured callee path does not exist: {}", + "warning".yellow().bold(), + p.display() + ); } }🤖 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-cli/src/cmd_prove.rs` around lines 506 - 517, The code builds extra_projects from args.with without resolving them relative to project_root while cfg_doc.callees are joined to project_root and non-existent callees are silently ignored; update the logic in the extra_projects construction so both sources are normalized the same way: for each path in args.with and each callee in cfg_doc.callees, resolve the path relative to project_root (use PathBuf::from + project_root.join when the input is relative), check existence, and if a path does not exist return or propagate a clear error (or fail fast) instead of silently skipping so verification scope isn’t silently reduced; adjust the code around extra_projects, args.with, cfg_doc.callees, and project_root accordingly.
🤖 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 `@implementations/rust/provekit-claim-envelope/src/bin/emit_c_fixtures.rs`:
- Around line 6-10: The header comment in emit_c_fixtures.rs is missing the
"raw-signature" output that main actually prints; update the file-level comment
to list five sections (pubkey string, sig string, raw signature hex,
mint_contract canonical_bytes + attestation CID, and proof envelope bytes + CID)
and add a short description for the raw-signature section (the hex-encoded raw
ed25519 signature produced in the block around lines 64–68) so the header
accurately documents what main prints.
In `@implementations/rust/provekit-verifier/src/call_edge_loader.rs`:
- Around line 42-69: The code currently ignores a direct targetContractCid and
skips edges without targetSymbol; update the resolution so you prefer a direct
"targetContractCid" from the edge before falling back to resolving via
"targetSymbol": read edge.get("targetContractCid").and_then(|v| v.as_str()) and
if present use that as tcid, otherwise derive the contract name from
"targetSymbol" (same logic around ':' into target_contract_name) and look up
pool.name_to_cid.get(target_contract_name); then, when you have a tcid (from
either source), push the obligation as obligations.push((source_cid.to_string(),
tcid, locus)) so edges with a concrete targetContractCid aren't skipped.
In `@implementations/rust/provekit-verifier/src/types.rs`:
- Around line 272-276: The code currently maps a single CID per contract name
via name_to_cid and overwrites on merges (using memento_cid and cid_to_name),
which can mis-resolve across projects; change name_to_cid from HashMap<String,
Cid> to HashMap<String, HashSet<Cid>> (or use a fully-qualified symbol key),
update the insertion site that currently does self.name_to_cid.insert(n,
memento_cid) to insert into the set (creating it if missing), and update any
merge/last-writer-wins logic that writes into name_to_cid (the same places that
call insert) to union sets instead of replacing; finally, update resolution code
that reads name_to_cid to detect ambiguous matches (multiple CIDs) and either
error/flag ambiguity or require disambiguation so call-edge resolution does not
pick a single lossy CID.
In `@protocol/provekit-ir.cddl`:
- Line 193: The Sort union was truncated and must include all formal-grammar
variants; update the Sort definition to reintroduce BitvecSort, SetSort, and
TupleSort so it matches the formal grammar (i.e., change "Sort = PrimitiveSort /
FunctionSort / DependentSort" back to include "/ BitvecSort / SetSort /
TupleSort"). Ensure the referenced variant types (BitvecSort, SetSort,
TupleSort) are defined in this CDDL file and referenced exactly by those names
so CDDL validation accepts IR conforming to
protocol/specs/2026-04-30-ir-formal-grammar.md.
- Around line 200-205: The CDDL changed FunctionSort field names from
domain/range to args/return; update the TypeScript side to match by renaming the
Sort type and all consumers from domain->args and range->return (or add a
compatibility shim that accepts both keys) so parsing and serialization stay
consistent: update the Sort type in
implementations/typescript/src/ir/formulas.ts, the FUNCTION_SORT_KEYS constant
and parseFunctionSort implementation in
implementations/typescript/src/ir/grammar/parse.ts to expect "args" and "return"
(or detect both forms and normalize to the new names), and adjust any downstream
code that serializes/deserializes FunctionSort to use the new field names.
In `@protocol/specs/2026-04-30-ir-formal-grammar.md`:
- Around line 187-190: Add blank lines before and after the Markdown table that
begins with the header "Invariant | Formula" so the table is separated from
surrounding text, and add fence languages to the two code fences referenced in
the grammar sections (the code blocks around the IR formal grammar examples) by
replacing triple backticks with language-specified fences (e.g., ```ebnf or
```text as appropriate for the grammar snippets) to satisfy MD058/MD040; update
the two unnamed code blocks in the grammar examples accordingly.
- Line 184: The invariant FunctionSort.ValidArgsAndReturn currently omits the
non-empty args requirement; update the definition (the symbol ValidArgsAndReturn
/ FunctionSort) to include a non-empty constraint (e.g., |args| ≥ 1 or ∃a ∈
args) in addition to HasKey("args") ∧ ∀a ∈ args → IsSort(a) ∧ HasKey("return") ∧
IsSort(return) so it matches the later requirement on the FunctionSort form.
---
Nitpick comments:
In `@implementations/rust/provekit-claim-envelope/src/bin/emit_c_fixtures.rs`:
- Around line 66-68: The code repeats the byte-to-hex conversion (e.g., let hex:
String = raw_sig.iter().map(|b| format!("{:02x}", b)).collect();) in multiple
places (around usages with raw_sig and the other print blocks at the later
occurrences); extract a small helper like fn to_hex(bytes: &[u8]) -> String and
replace each inline map/collect with to_hex(&raw_sig) (and the other byte
slices), and update the println calls (e.g., the ED25519_SIG_HELLO_RAW_HEX
printing block and the two other blocks at the referenced spots) to use the
helper to keep encoding logic centralized and consistent.
In `@implementations/rust/provekit-cli/src/cmd_prove.rs`:
- Around line 506-517: The code builds extra_projects from args.with without
resolving them relative to project_root while cfg_doc.callees are joined to
project_root and non-existent callees are silently ignored; update the logic in
the extra_projects construction so both sources are normalized the same way: for
each path in args.with and each callee in cfg_doc.callees, resolve the path
relative to project_root (use PathBuf::from + project_root.join when the input
is relative), check existence, and if a path does not exist return or propagate
a clear error (or fail fast) instead of silently skipping so verification scope
isn’t silently reduced; adjust the code around extra_projects, args.with,
cfg_doc.callees, and project_root accordingly.
In `@implementations/rust/provekit-verifier/src/runner.rs`:
- Around line 139-147: You are recomputing processed call edges: remove the
second call to call_edge_loader::process_call_edges(&call_edges, &pool) and
iterate over the already-computed obligations variable instead (e.g., for
(source_cid, target_cid, locus) in &obligations { ... }). Also remove any
now-unused local(s) introduced by the duplicate call so the code uses the single
obligations result from the earlier call to
call_edge_loader::process_call_edges.
🪄 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: bb887474-dc74-4271-b88e-6f66a434a2ef
📒 Files selected for processing (15)
examples/stage4-handshake-demo/stage4_driver.rsimplementations/rust/provekit-claim-envelope/src/bin/emit_c_fixtures.rsimplementations/rust/provekit-cli/src/cmd_mint.rsimplementations/rust/provekit-cli/src/cmd_prove.rsimplementations/rust/provekit-cli/src/main.rsimplementations/rust/provekit-cli/src/project_config.rsimplementations/rust/provekit-cli/src/report_fmt.rsimplementations/rust/provekit-verifier/src/call_edge_loader.rsimplementations/rust/provekit-verifier/src/lib.rsimplementations/rust/provekit-verifier/src/runner.rsimplementations/rust/provekit-verifier/src/types.rsimplementations/rust/provekit-verifier/tests/multi_solver_modes.rsprotocol/provekit-ir.cddlprotocol/specs/2026-04-30-ir-formal-grammar.mdprotocol/specs/2026-04-30-protocol-catalog.json
Comment on lines
+6
to
+10
| // Prints to stdout: | ||
| // 1. ed25519 pubkey string for seed=[0x42;32] | ||
| // 2. ed25519 sig string for (seed=[0x42;32], message=b"hello") | ||
| // 3. mint_contract canonical_bytes (hex) + attestation CID for the standard fixture | ||
| // 4. proof envelope bytes (hex) + CID for the standard fixture |
There was a problem hiding this comment.
File-header comment is missing the raw-signature section.
The header lists four output sections, but main prints five distinct ===-delimited sections (pubkey string, sig string, raw sig hex, mint-contract details, and proof envelope). The raw-signature hex section (lines 64–68) is not documented in the header, making the comment misleading for anyone relying on it to understand the output format.
📝 Proposed fix
// Prints to stdout:
// 1. ed25519 pubkey string for seed=[0x42;32]
// 2. ed25519 sig string for (seed=[0x42;32], message=b"hello")
-// 3. mint_contract canonical_bytes (hex) + attestation CID for the standard fixture
-// 4. proof envelope bytes (hex) + CID for the standard fixture
+// 3. ed25519 raw signature bytes (hex) for (seed=[0x42;32], message=b"hello")
+// 4. mint_contract canonical_bytes (hex) + attestation CID for the standard fixture
+// 5. proof envelope bytes (hex) + CID for the standard fixture📝 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
| // Prints to stdout: | |
| // 1. ed25519 pubkey string for seed=[0x42;32] | |
| // 2. ed25519 sig string for (seed=[0x42;32], message=b"hello") | |
| // 3. mint_contract canonical_bytes (hex) + attestation CID for the standard fixture | |
| // 4. proof envelope bytes (hex) + CID for the standard fixture | |
| // Prints to stdout: | |
| // 1. ed25519 pubkey string for seed=[0x42;32] | |
| // 2. ed25519 sig string for (seed=[0x42;32], message=b"hello") | |
| // 3. ed25519 raw signature bytes (hex) for (seed=[0x42;32], message=b"hello") | |
| // 4. mint_contract canonical_bytes (hex) + attestation CID for the standard fixture | |
| // 5. proof envelope bytes (hex) + CID for the standard fixture |
🤖 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-claim-envelope/src/bin/emit_c_fixtures.rs`
around lines 6 - 10, The header comment in emit_c_fixtures.rs is missing the
"raw-signature" output that main actually prints; update the file-level comment
to list five sections (pubkey string, sig string, raw signature hex,
mint_contract canonical_bytes + attestation CID, and proof envelope bytes + CID)
and add a short description for the raw-signature section (the hex-encoded raw
ed25519 signature produced in the block around lines 64–68) so the header
accurately documents what main prints.
Comment on lines
+200
to
+205
| ; Locked key order: kind, args, return | ||
| FunctionSort = { | ||
| kind: "function", | ||
| args: [+ Sort], ; argument sorts (one or more) | ||
| return: Sort, ; return sort | ||
| } |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Read-only verification: confirm whether old FunctionSort fields are still in use.
# Expected result after coordinated fix:
# - No active parser/type definitions using domain/range for FunctionSort.
# - Presence of args/return in parser/type definitions.
set -euo pipefail
echo "== FunctionSort key constants =="
rg -n --type=ts -C2 'FUNCTION_SORT_KEYS|domain|range|args|return'
echo
echo "== parseFunctionSort implementations =="
rg -n --type=ts -C4 'function\s+parseFunctionSort\s*\('
echo
echo "== Sort runtime type definitions =="
rg -n --type=ts -C4 'export\s+type\s+Sort\s*='Repository: TSavo/provekit
Length of output: 50371
🏁 Script executed:
# Check the specific files mentioned in the review
# parse.ts around lines 700-712
echo "=== parse.ts around lines 700-712 ==="
sed -n '695,720p' implementations/typescript/src/ir/grammar/parse.ts
echo ""
echo "=== formulas.ts around lines 25-30 ==="
sed -n '20,35p' implementations/typescript/src/ir/formulas.ts
echo ""
echo "=== Search for FunctionSort field definitions ==="
rg -n "FunctionSort|domain|range|args.*return" implementations/typescript/src/ir/ -A 3 -B 1Repository: TSavo/provekit
Length of output: 21173
Coordinate FunctionSort field names across CDDL and TypeScript before merge to prevent parse failures.
The CDDL now requires args/return fields, but the TypeScript parser and type definitions still expect domain/range. The mismatch affects:
implementations/typescript/src/ir/grammar/parse.ts(line 103: FUNCTION_SORT_KEYS; lines 707-711: parseFunctionSort implementation)implementations/typescript/src/ir/formulas.ts(line 30: Sort type definition)
All downstream type consumers and serialization logic also reference domain/range, so updates must be coordinated to avoid runtime breakage.
🤖 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/provekit-ir.cddl` around lines 200 - 205, The CDDL changed
FunctionSort field names from domain/range to args/return; update the TypeScript
side to match by renaming the Sort type and all consumers from domain->args and
range->return (or add a compatibility shim that accepts both keys) so parsing
and serialization stay consistent: update the Sort type in
implementations/typescript/src/ir/formulas.ts, the FUNCTION_SORT_KEYS constant
and parseFunctionSort implementation in
implementations/typescript/src/ir/grammar/parse.ts to expect "args" and "return"
(or detect both forms and normalize to the new names), and adjust any downstream
code that serializes/deserializes FunctionSort to use the new field names.
Comment on lines
+187
to
190
| | Invariant | Formula | | ||
| |-----------|---------| | ||
| | ValidFields | `∀s → HasKey("name")∧tstr(name) ∧ HasKey("indexVar")∧tstr(indexVar) ∧ HasKey("indexSort")∧IsSort(indexSort)` | | ||
|
|
There was a problem hiding this comment.
Fix markdownlint violations in changed grammar sections.
Please add blank lines around the table at Line 187 and add fence languages for the code blocks starting at Lines 1163 and 1172 to satisfy MD058/MD040.
Also applies to: 1163-1163, 1172-1172
🧰 Tools
🪛 markdownlint-cli2 (0.22.1)
[warning] 187-187: Tables should be surrounded by blank lines
(MD058, blanks-around-tables)
🤖 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-04-30-ir-formal-grammar.md` around lines 187 - 190, Add
blank lines before and after the Markdown table that begins with the header
"Invariant | Formula" so the table is separated from surrounding text, and add
fence languages to the two code fences referenced in the grammar sections (the
code blocks around the IR formal grammar examples) by replacing triple backticks
with language-specified fences (e.g., ```ebnf or ```text as appropriate for the
grammar snippets) to satisfy MD058/MD040; update the two unnamed code blocks in
the grammar examples accordingly.
Owner
Author
|
Holding merge — multiple load-bearing review concerns from Copilot + CodeRabbit. CI is now GREEN (kit-local attestation removal fix landed) and the test suite passes, but the reviews surface 7+ P1 concerns that need resolution before this v1.5.0 keystone lands. Consolidated: Spec/grammar
Protocol-correctness bugs
Verifier behavior
Coverage
This is significantly beyond the autonomous-fire scope (read review, address P1 inline, merge). Recommended: assign back to the keystone author / architect for triage, or split into smaller follow-ups. Skipping merge until P1s resolved. |
Sir's principle for ProvekIt is "Supra omnia, rectum" — above all, correctness. A spec/substrate PR cannot ship known-incorrect protocol behavior. This commit reconciles the P1 review concerns inline. Spec / wire-format reconciliation: - CDDL `Sort` union now matches the spec EBNF: 6 variants (PrimitiveSort / BitvecSort / SetSort / TupleSort / FunctionSort / DependentSort) instead of the 3 previously committed. Bitvec/Set/ Tuple grammars added to the CDDL with locked key orders matching the spec sections. - FunctionSort.ValidArgsAndReturn invariant now encodes `len(args) >= 1` and `IsArray(args)`, matching the CDDL `[+ Sort]` one-or-more constraint. - DependentSort.ValidFields uses `IsString` (consistent with rest of the spec) instead of `tstr` (which was undefined in this doc). - Catalog CID for ir-formal-grammar regenerated. Protocol-correctness bugs: - `save_call_edges_if_present` now derives the file-CID from `provekit_canonicalizer::encode_jcs(...)` instead of `serde_json::to_string(...)`. The previous code hashed non-canonical bytes, producing a CID that wasn't byte-deterministic across implementations — exactly the property the substrate exists to enforce. The file is also written using the canonical bytes rather than the non-canonical serde output. - `MementoPool::insert` no longer indexes `name_to_cid` / `cid_to_name` for non-contract mementos. Other kinds (implication, etc.) sometimes carry a `header.name` field that isn't a stable cross-kit identifier; indexing them would mis-resolve call edges. - `MementoPool::insert` now detects duplicate-name collisions (same name resolving to two CIDs) and surfaces them via `load_errors` instead of silently overwriting. - `MementoPool::merge` no longer uses `BTreeMap::extend`, which silently overwrote existing entries. Each map is merged with insert-only-if-absent + collision detection via `load_errors`. Verifier behavior: - `Runner::run_with_tiers` now reuses the single `obligations` Vec computed before the report loop, rather than calling `process_call_edges` a second time inside the loop. - `process_call_edges` now prefers `targetContractCid` (direct CID identity) before falling back to `targetSymbol`-based name resolution. Direct CID is the substrate's strong identity per the content-address principle. CLI: - `provekit prove --with <path>` now resolves relative paths against `project_root`, matching how `[verify].callees` is resolved. Without this, `--with foo` depended on CWD and broke when prove was invoked outside the project root. Documentation: - `ProofEnvelopeInput.signer_cid` doc now reflects that the underlying `signer` wire field accepts both `blake3-512:<hex>` (CID resolving to a pubkey memento) and `ed25519:<base64-pubkey>` (inline self-identifying), per the memento-envelope grammar. Verified locally: `rust_kit_mint_is_byte_deterministic` passes; `recompute-spec-cids --verify` is clean. Closes Copilot + CodeRabbit P1 concerns on #348. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 5, 2026
TSavo
added a commit
that referenced
this pull request
May 5, 2026
After #348 grew the IR Sort grammar to a 6-variant union (with the 3 implemented variants in the cpp kit: Primitive / Function / Dependent), `value_from_kit.cpp::sort_to_value` was still reading `sort.name` as a flat field, which doesn't compile against the new `std::variant<PrimitiveSort, FunctionSort, DependentSort>`. Replace the flat read with a `std::visit` dispatcher emitting the locked key order per variant from the spec (`protocol/specs/2026-04-30-ir-formal-grammar.md`): - PrimitiveSort: kind, name - FunctionSort: kind, args, return - DependentSort: kind, name, indexVar, indexSort Verified locally: `tools/build-cpp-self-contracts.sh --build-only` produces a clean `mint_cpp_self_contracts` binary. Per spec: bytes are byte-deterministic (RFC 8785 JCS) and produce identical canonical output to the Rust kit's reference. Closes part of the #361 cpp build failure. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo
added a commit
that referenced
this pull request
May 5, 2026
…riants After #348 grew the IR Sort grammar to PrimitiveSort / FunctionSort / DependentSort, the C# `Serialize.cs` was still reading `s.Name` flat, which doesn't compile against the new abstract record `Sort` with sealed sub-records `Primitive(string Name) / Function(Sort[] Args, Sort Return) / Dependent(string Name, string IndexVar, Sort IndexSort)`. Replaces the flat reads with pattern-match dispatchers in BOTH paths: - SortToValue (canonicalizer-Value path) emits the locked key order per spec (`protocol/specs/2026-04-30-ir-formal-grammar.md`): Primitive: kind, name Function: kind, args, return Dependent: kind, name, indexVar, indexSort - WriteSort (raw-JSON-string path) does the same dispatch, writing JCS-canonical bytes inline. Both paths now produce identical canonical bytes via the locked key orders. Verified locally: dotnet build clean; provekit mint --kit=csharp produces contractSetCid `blake3-512:ed7f1eb7bba9da19e6a27d531d7692f0c57121c3733119b9905d793a9dc0220d3e0ce03675df7ba57c905bc4d997289b97c8d80accec1dc606fd3b314b0ad7bf` matching the pinned canonical reference exactly. Cross-impl byte-equivalence holds. This mirrors the cpp `value_from_kit.cpp` visitor fix that landed earlier on this branch. The pattern is identical: tagged-union Sort needs variant dispatch, not flat `Name` reads. Closes the C# half of the per-kit Sort regen on #361 and unblocks the csharp self-contracts attestation gate. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 5, 2026
ConstCorrectness
pushed a commit
to ConstCorrectness/provekit
that referenced
this pull request
May 6, 2026
…) + DependentSort Per-kit IR type update for every language kit (blocked on TSavo#348 CDDL): All kits: - FunctionSort: domain->args, range->return (locked per TSavo#329) - Add DependentSort: {kind, name, indexVar, indexSort} - PrimitiveSort, BitvecSort, SetSort, TupleSort unchanged Kit coverage (23 files, 13 languages): typescript: type Sort, FuncOf, Parse, Emit, Canonicalize, SMT, Lean, tests go: funcSort -> args/return, + dependentSort java: Function(args, ret) record, + Dependent record python: Sort union, sort_to_value updated ruby: PrimitiveSort + FunctionSort + DependentSort structs csharp: abstract Sort -> Primitive | Function | Dependent c: PK_SORT_FUNCTION / PK_SORT_DEPENDENT enum + union data cpp: variant<PrimitiveSort, FunctionSort, DependentSort> swift: indirect enum Sort {primitive, function, dependent} zig: union Sort {primitive, function, dependent} php: abstract Sort -> PrimitiveSort | FunctionSort | DependentSort
This was referenced May 7, 2026
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.
Closes #329. Parent: #263. Blocks: all 12 per-kit IR regen sub-issues, Coq compiler, SMT-LIB compiler.
What changed
protocol/provekit-ir.cddlprotocol/specs/2026-04-30-ir-formal-grammar.mddomain→args,range→return(locked per [spec] grow IR Sort grammar — FunctionSort + DependentSort CDDL + formal-grammar update #329)argsrequires one or more elements (no empty function sort)DependentSortBNF with locked key orderValidArgsAndReturn,ValidFieldsValidDomainAndRangeLocked key orders
kind,args,returnkind,name,indexVar,indexSortWhat's NOT in this PR
PrimitiveSortNameunchangedBitvecSort,SetSort,TupleSortuntouchedAcceptance
Summary by CodeRabbit
Release Notes
New Features
--withCLI option to specify additional project directories for multi-project verification.calleesconfiguration option for declaring callee projects.Documentation