Catalog starts empty, promotion torn out, the missing edge caught — on canonical Int#1565
Merged
Conversation
The catalog is the signature of witnesses having witnessed. At t=0, before any witness, it is empty. A hand-assembled initial population is the lie: concepts named/classified by fiat instead of accreted from witnessing. - seed_catalog() returns empty. Deleted the on-disk concept-shapes load (hand-authored, UNSIGNED_DEV_ONLY mementos) and legacy_classification_entries (two entries with EMPTY shape_cid -- not even content-addressed, pure fiction). - Removed the 8 now-dead catalog-loader fns (the disease's clean-up crew, dead the moment the lie stops being fed). - Deleted 3 tests that ENCODED the lie: seed_catalog_loads_real_concept_shape_catalog (asserted catalog ships pre-loaded, len>10), catalog_matches_loaded_shape_cid_before_legacy_classification (legacy precedence), bind_names_blake3_512_of_operations_from_catalog (naming from catalog). No honest refactor exists; the truth (starts empty, accretes by witnessing) is a fresh test written when accretion exists. Concept naming now falls back to UNNAMED until a real witness promotes a concept in. Grammar (ConceptOpCatalog/required_cid, still disk-loaded) is the NEXT stroke: grammar to code as pure name-free shapes. bind tests 8/0. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
A construct is the LANGUAGE or a promoted concept, never both. The IR grammar primitives (op-application/seq/ite/bind-result) are the language, so they come home to code: pinned by SHAPE, addressed by json_cid of a pure, name-free, positional structural shape compiled into the binary. - grammar_op_shape() authors each primitive's shape with fn_name, operator, formal parameter names, wp_note prose, and the memento envelope ABSENT BY CONSTRUCTION (born pure, never stripped). Slot refs positional. - ConceptOpCatalog is now a unit type: cid(name) = json_cid(grammar_op_shape(name)). No disk load, no CatalogIndex, no required_cid that can fail on an empty catalog -- the language is always present because it is the code. - Deleted find_concept_shapes_root, the CatalogIndex import, and the std::path imports: the disk-loading machinery is gone. We don't pin CIDs (a frozen hash is a magic number divorced from its preimage); we pin shapes, and the CID falls out by computation. Every old name-contaminated grammar address changes -- bundles that pinned them break, correctly. bind 8/0. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
… pinned literal CONCEPT_BIND_RESULT_CID was a pinned hash -- a magic number divorced from its preimage, and now inconsistent with the shape-computed address used everywhere else. concept_bind_result_cid() now returns ConceptOpCatalog.cid(CONCEPT_BIND_RESULT) = json_cid(grammar_op_shape(..)), the one true address. Const deleted. We pin shapes, not CIDs. libprovekit lib tests 99/0. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
… disk bind_kit_transform_emits_bind_result_op_tree asserted every payload op CID 'resolves in the concept catalog' -- but checked concept_catalog(), the on-disk catalog (the old, dying authority). Grammar CIDs now compute from code shapes, so they no longer match disk -> the invariant failed against the wrong oracle. The invariant (no dangling/fabricated op CIDs) is real and kept; it now checks each node's op_cid equals grammar_op_cid(op_name) -- the CODE shape-authority's computed address. Exposed pub grammar_op_cid as the single resolver consumers derive from. Deleted the disk concept_catalog() helper + CatalogIndex import. bind_kit 8/0. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…WitnessMemento A witness is raw external attestation: a JUnit suite's output, a vitest runner's JSON, a log line printing 2+2=4, a signature on a page. witness_ingest is the single converter that turns any such raw artifact, bound to a specific contract, into a canonical WitnessMemento. measurements carries the raw output verbatim (no schema imposed); witness_for binds it to the contract; the canonical envelope (CID + observed_at) is stamped here. The CID addresses WHAT is attested -- the observation (subject, fixture, measurements, outcome). It is NOT the substrate's job to say HOW it is attested: signed_by + signature are the attestation layer, excluded from the preimage. The same page signed by a different hand is the SAME CID, a different attestation. (Test asserts exactly this.) Underneath, fixes WitnessMemento::recompute_cid: it excluded only "cid", hashing the signature INTO the address -- circular, and self-consistency was impossible, so no minted witness could pass validate(). Now excludes cid + signed_by + signature (matching MigrateReceiptEnvelope), so a witness's CID matches its own content. ir-types + provekit-cli green. This is the production end of the pipeline: contract -> emit unit test -> run -> output -> ingest as witness against the contract -> cluster -> promote -> concept. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…te_cid Two fixes to the converter I committed red: - The CID was hand-rolled (own JCS over a hand-built observation) and didn't byte-match recompute_cid's serde serialization. Now the CID is derived THROUGH recompute_cid, so cid == recompute_cid by construction; the signature attests the address. - observed_at was stamped internally (Utc::now()), so two ingests of the same page got different CIDs (different timestamps). The observer reports when it observed -- observed_at is part of the observation, caller-provided, not fabricated. Same page + same observation time = same witness; same page + different signing key = same CID, different attestation (test asserts both). provekit-cli witness_ingest green. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Begin tearing out the promotion/consensus apparatus -- severable cruft per the SHARED-LANGUAGE dictionary (the spine is composition; concept-equivalence is the vendor's 3-axis-pinning call, not a promotion tier). prove/verify no longer bypass solver dispatch to query a promotion catalog: removed the --require-empirically-witnessed gate dispatch + run_empirically_witnessed_gate from both. (CLI arg fields + promotion_query + cmd_witness consensus + bind promotion + the registry + ir-types types follow in subsequent commits.) provekit-cli compiles clean. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…uery cmd_witness drops the consensus/status subcommands and all the consensus machinery (run_consensus, run_status, WitnessCatalog/ConsensusEvidence, collect_witness_catalog, consensus_evidence/_row_schema/_vector, promotion_decision_for_consensus). The single-witness path stays: prove a property from a contract via the solver (witness axis is real, kept). Deleted promotion_query.rs (zero consumers after the prove/verify gates + consensus went). provekit-cli compiles clean. Remaining promotion teardown: dead CLI arg fields, bind's promotion_decisions, libprovekit promotion_decision_registry, ir-types PromotionDecision*/Gate/Result, and the promotion tests. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
bind_term_document no longer mints PromotionDecisionMemento per entry (the promoted_cid = blake3(name) fiction + the PromotionGate::Proof decision). Removed the promotion_decision_mementos field from NamedTermDocument, its serde round-trip, and the promotion_decisions fn. Bind now produces named terms + gap records + witnesses; promotion is not bind's job (severable cruft per the dictionary). libprovekit compiles clean. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The promotion apparatus has no consumers left, so the registry module (libprovekit/promotion_decision_registry.rs) and the three promotion/consensus test files (registry test, witness_consensus_test, promotion_decision_serde) are deleted. Full workspace compiles clean (cargo check --workspace, exit 0). Remaining is inert residue: dead CLI arg fields and the unused ir-types PromotionDecision* type definitions (the latter entangled with the widely-shared, misnamed PromotionDecisionCanonicalizationError). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
A crate built to demonstrate 'a bug is a missing edge', run end-to-end through provekit mint / verify / prove. Records a FALSE GREEN: the buggy seam (serialize's post does not establish content_address's pre, broken at value=-1) reports discharged:1 violations:0. Root cause (traced, see RESULT.md): - verify enumerates @sugar/@boundary claims only; this crate has none. - prove's enumerate_callsites only walks declared-bridge sourceSymbols; an intra-body call (content_address(serialize(value))) is not a bridge, so the seam is never an obligation. - the lone address_of bridge discharged at Tier 0 (memento-is-verification): for a body-derived contract the consumer pre is trivially already in the pool, so discharge is by hash lookup, never reaching the solver (Tier 3). - bridge had no targetProofCid -> back-compat path, ConsequentBundlePinned not enforced. Leaves a substrate-scope question for T: is Tier-0 discharge of body-derived callsites sound, or a hole that passes real missing edges as false greens? The crate is the evidence; re-run the three verbs to reproduce. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The shared-language dictionary (lift/lower 2x2, sugar/boundary/contract, catalog=fiction, composition=implication, the 3-axis pinning) was committed only on spike/honest-domain-inventory and stranded in the honest-spike worktree. It is the canonical vocabulary every substrate decision references; bring the committed version (c9f8a82) onto the working line so it lives in the actual repo, not just a side worktree. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…nonical Int
The rust-missing-edge crate now reports a real refutation through
`provekit mint`/`prove`: 3 callsites, content_address UNSATISFIED (z3 sat,
the value<0 seam serialize.post cannot establish), serialize/address_of
discharged. The unit test passes; the solver does not. Four stacked fixes,
all below the language line:
Hole 2 (verifier pool category error): MementoPool::insert indexed a
contract's preHash/antecedentHash into formula_to_memento, the map Tier 0
trusts as proven-true. A precondition is an obligation, not a fact, so a
callsite's consumer-pre self-discharged. Index only postHash/invHash/
consequentHash (established facts). verify_implication no longer gates on the
antecedent being present in that index.
Hole 1 (lifter): lift_expr_to_term_inner had no Expr::Call arm, so a body
that is a nested call collapsed to a vacuous `true` post and the callees
were invisible to enumerate_callsites. Lift Expr::Call to a ctor named by the
callee's bare symbol; the call tree now survives into the contract (1 -> 3
callsites).
Hole 3 (verifier discharge): instantiate / build_implication_obligation
require forall-quantified pre/post, but body-derived contracts emit bare
predicates over named formals, and locate_producer_post read the v1.1
evidence.body shape while mint emits v1.2 header. Synthesize forall(formal)
from the contract's formals at the discharge boundary; make
locate_producer_post shape-agnostic so the producer post resolves and the
real producer_post -> consumer_pre implication is what the solver refutes.
Sort canonicalization: sort_translate emitted width-distinct Rust names
(I64/U32/Usize) as primitive sort names, violating canonicalization-grammar
§5 (fixed set {Bool,Int,Real,String,Ref,...}) and breaking cross-language
federation (Rust i64 vs Java long). Collapse integer widths to canonical
Int: width is a range refinement that rides the sugar, not a sort; the
source type system already owns width/narrowing; the solver reasons in LIA.
This deletes the smt_binder_sort verifier hack outright -- the lifter now
emits the canonical sort, so the verifier has nothing language-specific to
normalize. sort_translate + marriage tests updated to assert the collapse.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
WalkthroughRemoves promotion-decision plumbing and related tests, switches primitive-op CID derivation to in-code grammar shapes, adds witness ingestion/signing and CID recomputation, tightens verifier indexing/quantification and formula wrapping, canonicalizes integer sorts, updates lift behavior, and adds docs and a rust example. ChangesCore Infrastructure Refactoring
Estimated code review effort🎯 4 (Complex) | ⏱️ ~60 minutes Possibly related PRs
Suggested labels
Poem
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches📝 Generate docstrings
🧪 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: c443690f7c
ℹ️ 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".
| // Established facts: a function's `postHash`/`invHash` (guarantees on | ||
| // return / always), and a proven implication's `consequentHash` | ||
| // (gated by its implication memento via `verify_implication`). | ||
| for field in &["postHash", "invHash", "consequentHash"] { |
There was a problem hiding this comment.
When an implication memento P -> Q is loaded, indexing consequentHash into formula_to_memento makes Tier 0 pool.verify(Q) succeed without checking the current antecedent. In the runner, Tier 0 runs before the producer-post implication check, so once any bridge proves a consumer precondition Q, later callsites requiring the same Q can self-discharge even when their producer post is different or absent. Keep implication consequents out of the verified-formula index and require verify_implication/can_implies for those lookups.
Useful? React with 👍 / 👎.
Comment on lines
246
to
248
| pub fn run(args: VerifyArgs) -> u8 { | ||
| // Early dispatch: --require-empirically-witnessed bypasses the | ||
| // standard solver-dispatch flow and queries the promotion catalog. | ||
| if args.require_empirically_witnessed.is_some() { | ||
| return run_empirically_witnessed_gate(&args); | ||
| } | ||
|
|
||
| // Early dispatch: the supply-chain admission gate. When any of |
There was a problem hiding this comment.
The --require-empirically-witnessed option is still parsed and documented as bypassing normal verification, but this branch now falls straight through to the standard solver-dispatch path. In contexts where a caller expects provekit verify --require-empirically-witnessed ... to reject when the promotion catalog lacks the required concept/fixture, the request is silently ignored and the command can succeed based on unrelated project verification. Either restore the catalog gate or reject the flag explicitly.
Useful? React with 👍 / 👎.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 6
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (5)
implementations/rust/provekit-cli/src/cmd_verify.rs (1)
161-175:⚠️ Potential issue | 🟠 Major | ⚡ Quick winDon't silently ignore the empirically-witnessed gate flags.
VerifyArgsstill accepts--require-empirically-witnessed,--require-fixture, and--consensus-policy, butrun()never reads them anymore.provekit verify --require-empirically-witnessed ...now falls through to ordinary solver verification and can report success without performing the requested gate check. Either remove these flags from the CLI surface or fail fast until the replacement path exists.Also applies to: 246-445
🤖 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_verify.rs` around lines 161 - 175, The CLI flags require_empirically_witnessed, require_fixture, and consensus_policy are parsed into VerifyArgs but never used in run(), so either remove them from the CLI or make run() fail fast when they are present; update the run() function to inspect VerifyArgs.require_empirically_witnessed, VerifyArgs.require_fixture, and VerifyArgs.consensus_policy and return an error (with a clear message) if any are Some() (or implement the intended gate-check logic if available), ensuring the flags no longer silently have no effect.implementations/rust/libprovekit/src/core/bind.rs (1)
232-268:⚠️ Potential issue | 🟠 Major | ⚡ Quick winBump the named-term wire schema or keep a v1 compat field.
promotionDecisionMementosdisappeared from the serializedNamedTermDocument, but the emittedschemaVersionis still"1". That makes this a silent breaking change for existing v1 consumers;implementations/rust/provekit-cli/tests/cmd_bind_integration.rs:127-169still expectspromotionDecisionMementos[0].header.kind. Either preserve an empty compat field for v1 or bump the schema and update consumers in the same PR.Also applies to: 482-493
🤖 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/libprovekit/src/core/bind.rs` around lines 232 - 268, The NamedTermDocument struct removed the promotionDecisionMementos field but left schema_version as "1", causing a silent breaking change; either restore a compat field named promotionDecisionMementos (e.g., add pub promotion_decision_mementos: Vec<Json> with #[serde(default, rename = "promotionDecisionMementos", skip_serializing_if = "Vec::is_empty")] so v1 consumers continue to see an empty array) or explicitly bump schema_version to a new value (e.g., "2") and update all consumers/tests that expect promotionDecisionMementos (references: NamedTermDocument and its schema_version field and the test assertions checking promotionDecisionMementos[0].header.kind).implementations/rust/provekit-cli/src/cmd_witness.rs (2)
96-104:⚠️ Potential issue | 🟠 Major | ⚡ Quick winFail closed until the witness mint/write path is wired back in.
The successful
Unsatbranch exitsEXIT_OKafter printing a placeholder, but it never writes aWitnessMemento. That makes automation think a witness was minted when nothing was persisted. This path should error out until the real minting flow is restored.🤖 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_witness.rs` around lines 96 - 104, The SolverOutput::Unsat branch currently prints a placeholder and returns EXIT_OK without persisting a WitnessMemento; change this to fail closed: remove or stop printing any “proven/minting” success messaging and instead log an explicit error/notice that minting is disabled, and return a non-zero failure exit code (replace EXIT_OK with the existing failure constant or introduce EXIT_FAIL/EXIT_ERROR) so automation does not treat this as a successful mint; keep the code path for future minting (minting logic that would construct a WitnessMemento) but ensure it is not executed until the real mint/write flow is restored.
25-38:⚠️ Potential issue | 🟠 Major | ⚡ Quick winReject or remove the stale
witness consensusCLI surface.
run()now treats the first positional as a contract CID unconditionally, soprovekit witness consensus ...no longer hits a mode handler. With the currentWitnessArgsstill advertising consensus-related flags inimplementations/rust/provekit-cli/src/main.rs, users now get the generic<CONTRACT_CID> <PROPERTY>error instead of a clean unsupported-mode failure or a trimmed CLI surface.🤖 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_witness.rs` around lines 25 - 38, The CLI still advertises a stale "consensus" mode while run() in the Witness command treats the first positional as a contract CID unconditionally (see run(), WitnessArgs, command_or_contract, property), causing misleading "<CONTRACT_CID> <PROPERTY>" errors; fix by removing the consensus-related flags/options from the WitnessArgs definition and the CLI registration in main.rs so the surface no longer advertises consensus, or if you must keep the flags, add an early guard in run() that detects the legacy consensus invocation (e.g., if command_or_contract == "consensus" or a consensus flag is set) and print a clear unsupported-mode error and return EXIT_USER_ERROR.implementations/rust/provekit-verifier/src/types.rs (1)
305-309:⚠️ Potential issue | 🔴 Critical | ⚡ Quick winDon't index implication consequents as verified facts.
verify()treats everyformula_to_mementoentry as an unconditional truth. AddingconsequentHashhere means a standaloneP → Qmemento makespool.verify(Q)succeed even whenPwas never discharged, which recreates the same false-green class you just removed forpreHash.Suggested fix
- for field in &["postHash", "invHash", "consequentHash"] { + for field in &["postHash", "invHash"] { if let Some(hash) = memento_body_field(&envelope, field).and_then(|v| v.as_str()) { self.formula_to_memento .insert(hash.to_string(), memento_cid.clone()); } }🤖 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/types.rs` around lines 305 - 309, The code is incorrectly indexing implication consequents so that a memento containing a standalone implication makes the consequent appear as an unconditional fact; remove "consequentHash" from the loop that inserts into self.formula_to_memento (the block using memento_body_field(&envelope, field) and inserting hash.to_string() -> memento_cid) so only implication posts/invariants are indexed (e.g., keep "postHash" and "invHash" but not "consequentHash"); this ensures verify()/pool.verify() won’t treat consequents of P → Q as true unless P is discharged.
🧹 Nitpick comments (1)
implementations/rust/provekit-verifier/src/types.rs (1)
943-997: ⚡ Quick winAdd a layered-shape variant of this regression.
This only exercises the v1.1 flat contract path, but the fix relies on
memento_body_fieldstaying shape-agnostic. A matching v1.2 fixture would protect theheader/metadatapath that production-minted mementos use.🤖 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/types.rs` around lines 943 - 997, Add a sibling test that mirrors precondition_is_obligation_not_verified_fact but constructs a v1.2 "layered" memento shape (use make_contract_memento logic adapted to the layered/header+metadata/body model) so MementoPool and the memento_body_field codepath are exercised; specifically, create a layered memento with the same contractName/pre/post and derived hashes, insert it into the pool (using the same m_cid and pool.insert), then assert pool.verify(&post).is_some() and pool.verify(&pre).is_none(); reference the existing test function name precondition_is_obligation_not_verified_fact, the helper make_contract_memento (to mirror fields), and MementoPool/memento_body_field to locate where to add the new layered-shape fixture.
🤖 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 `@examples/rust-missing-edge/RESULT.md`:
- Around line 25-41: The fenced command block that begins with "$ cargo test
..." is missing a language tag; edit the opening triple-backtick so it specifies
a shell language (e.g., change "```" to "```bash" or "```sh") to satisfy
markdown linting and improve rendering for the block that contains the
cargo/provekit commands and verifier output.
In `@implementations/rust/libprovekit/src/core/bind.rs`:
- Around line 558-564: The function grammar_op_cid currently calls
ConceptOpCatalog.cid(name) but only recognizes fully-qualified names like
"concept:seq"; update grammar_op_cid to accept the plain names advertised by the
docs by normalizing input before lookup: if name does not start with "concept:"
prepend "concept:" and then call ConceptOpCatalog.cid, falling back to the
original call if needed so both "seq" and "concept:seq" resolve; apply the same
normalization pattern to the other similar helper(s) in this file (the related
helpers around lines 1281-1345) that also call ConceptOpCatalog.cid.
In `@implementations/rust/provekit-cli/src/witness_ingest.rs`:
- Around line 80-83: The code currently calls ed25519_sign_string(signer_seed,
cid.as_bytes()) which signs the CID string; instead sign the canonical
witness/observation bytes used to derive that CID so the attestation format
matches cmd_verify.rs. Locate the code path that builds the canonical
observation (the same bytes passed into your CID generation routine) and pass
those bytes into the ed25519 signing call (e.g., replace cid.as_bytes() with the
canonical_observation_bytes variable or call the helper that returns them), keep
assigning witness.cid = cid, and store the produced signature on the witness; if
there is a byte-oriented signing helper (vs. sign_string) use it to avoid
accidental encoding differences.
In `@implementations/rust/provekit-ir-types/src/lib.rs`:
- Around line 6343-6350: The CLI witness minting path still includes "signed_by"
in the CID preimage and must be updated to match the new CID contract used by
migration_cid_without_keys; change the CID derivation in the cmd_verify witness
creation code to exclude "signed_by" and "signature" (i.e., compute the CID the
same way WitnessMemento::recompute_cid() / validate() do) so witnesses minted by
the CLI produce the same CID as WitnessMemento::recompute_cid() and pass
validate().
In `@implementations/rust/provekit-verifier/src/handshake.rs`:
- Around line 164-170: The code is incorrectly deriving the `result` sort from
`formalSorts[0]`; change the construction of `sort` in handshake.rs to read the
producer's actual return sort (e.g., look up a return/result sort field on
`producer_body` such as `"resultSort"` or `"returnSort"`) and fall back to the
primitive Int only if that return sort is missing, then use that `sort` when
building the `forall` JSON for `"result"` instead of using `formalSorts[0]`.
In `@SHARED-LANGUAGE.md`:
- Around line 105-120: Add language identifiers to the two unlabeled fenced code
blocks in SHARED-LANGUAGE.md to satisfy markdownlint MD040: change the block
containing "post(B) → pre(A)" to a fenced block with a language tag (e.g., use
```text) and likewise add a language tag to the Hoare rule block containing "{P}
B {Q} {Q} A {R} ..." so both fenced blocks start with ```text; update the
two occurrences that wrap those exact snippets.
---
Outside diff comments:
In `@implementations/rust/libprovekit/src/core/bind.rs`:
- Around line 232-268: The NamedTermDocument struct removed the
promotionDecisionMementos field but left schema_version as "1", causing a silent
breaking change; either restore a compat field named promotionDecisionMementos
(e.g., add pub promotion_decision_mementos: Vec<Json> with #[serde(default,
rename = "promotionDecisionMementos", skip_serializing_if = "Vec::is_empty")] so
v1 consumers continue to see an empty array) or explicitly bump schema_version
to a new value (e.g., "2") and update all consumers/tests that expect
promotionDecisionMementos (references: NamedTermDocument and its schema_version
field and the test assertions checking
promotionDecisionMementos[0].header.kind).
In `@implementations/rust/provekit-cli/src/cmd_verify.rs`:
- Around line 161-175: The CLI flags require_empirically_witnessed,
require_fixture, and consensus_policy are parsed into VerifyArgs but never used
in run(), so either remove them from the CLI or make run() fail fast when they
are present; update the run() function to inspect
VerifyArgs.require_empirically_witnessed, VerifyArgs.require_fixture, and
VerifyArgs.consensus_policy and return an error (with a clear message) if any
are Some() (or implement the intended gate-check logic if available), ensuring
the flags no longer silently have no effect.
In `@implementations/rust/provekit-cli/src/cmd_witness.rs`:
- Around line 96-104: The SolverOutput::Unsat branch currently prints a
placeholder and returns EXIT_OK without persisting a WitnessMemento; change this
to fail closed: remove or stop printing any “proven/minting” success messaging
and instead log an explicit error/notice that minting is disabled, and return a
non-zero failure exit code (replace EXIT_OK with the existing failure constant
or introduce EXIT_FAIL/EXIT_ERROR) so automation does not treat this as a
successful mint; keep the code path for future minting (minting logic that would
construct a WitnessMemento) but ensure it is not executed until the real
mint/write flow is restored.
- Around line 25-38: The CLI still advertises a stale "consensus" mode while
run() in the Witness command treats the first positional as a contract CID
unconditionally (see run(), WitnessArgs, command_or_contract, property), causing
misleading "<CONTRACT_CID> <PROPERTY>" errors; fix by removing the
consensus-related flags/options from the WitnessArgs definition and the CLI
registration in main.rs so the surface no longer advertises consensus, or if you
must keep the flags, add an early guard in run() that detects the legacy
consensus invocation (e.g., if command_or_contract == "consensus" or a consensus
flag is set) and print a clear unsupported-mode error and return
EXIT_USER_ERROR.
In `@implementations/rust/provekit-verifier/src/types.rs`:
- Around line 305-309: The code is incorrectly indexing implication consequents
so that a memento containing a standalone implication makes the consequent
appear as an unconditional fact; remove "consequentHash" from the loop that
inserts into self.formula_to_memento (the block using
memento_body_field(&envelope, field) and inserting hash.to_string() ->
memento_cid) so only implication posts/invariants are indexed (e.g., keep
"postHash" and "invHash" but not "consequentHash"); this ensures
verify()/pool.verify() won’t treat consequents of P → Q as true unless P is
discharged.
---
Nitpick comments:
In `@implementations/rust/provekit-verifier/src/types.rs`:
- Around line 943-997: Add a sibling test that mirrors
precondition_is_obligation_not_verified_fact but constructs a v1.2 "layered"
memento shape (use make_contract_memento logic adapted to the
layered/header+metadata/body model) so MementoPool and the memento_body_field
codepath are exercised; specifically, create a layered memento with the same
contractName/pre/post and derived hashes, insert it into the pool (using the
same m_cid and pool.insert), then assert pool.verify(&post).is_some() and
pool.verify(&pre).is_none(); reference the existing test function name
precondition_is_obligation_not_verified_fact, the helper make_contract_memento
(to mirror fields), and MementoPool/memento_body_field to locate where to add
the new layered-shape fixture.
🪄 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: 6d4fbe56-6321-4cda-b660-2d5fbdb28a72
📒 Files selected for processing (29)
SHARED-LANGUAGE.mdexamples/rust-missing-edge/.gitignoreexamples/rust-missing-edge/.provekit/config.tomlexamples/rust-missing-edge/.provekit/lift/rust-tests/manifest.tomlexamples/rust-missing-edge/.provekit/lift/rust-walk-contracts/manifest.tomlexamples/rust-missing-edge/Cargo.tomlexamples/rust-missing-edge/RESULT.mdexamples/rust-missing-edge/src/lib.rsimplementations/rust/libprovekit/src/core/bind.rsimplementations/rust/libprovekit/src/core/mod.rsimplementations/rust/libprovekit/src/lib.rsimplementations/rust/libprovekit/src/promotion_decision_registry.rsimplementations/rust/libprovekit/tests/bind_kit.rsimplementations/rust/libprovekit/tests/promotion_decision_registry.rsimplementations/rust/provekit-cli/src/cmd_prove.rsimplementations/rust/provekit-cli/src/cmd_verify.rsimplementations/rust/provekit-cli/src/cmd_witness.rsimplementations/rust/provekit-cli/src/main.rsimplementations/rust/provekit-cli/src/promotion_query.rsimplementations/rust/provekit-cli/src/witness_ingest.rsimplementations/rust/provekit-cli/tests/witness_consensus_test.rsimplementations/rust/provekit-ir-types/src/lib.rsimplementations/rust/provekit-ir-types/tests/promotion_decision_serde.rsimplementations/rust/provekit-verifier/src/handshake.rsimplementations/rust/provekit-verifier/src/resolve_target.rsimplementations/rust/provekit-verifier/src/types.rsimplementations/rust/provekit-walk/src/lift.rsimplementations/rust/provekit-walk/src/marriage.rsimplementations/rust/provekit-walk/src/sort_translate.rs
💤 Files with no reviewable changes (7)
- implementations/rust/provekit-ir-types/tests/promotion_decision_serde.rs
- implementations/rust/libprovekit/tests/promotion_decision_registry.rs
- implementations/rust/provekit-cli/tests/witness_consensus_test.rs
- implementations/rust/libprovekit/src/promotion_decision_registry.rs
- implementations/rust/provekit-cli/src/cmd_prove.rs
- implementations/rust/provekit-cli/src/promotion_query.rs
- implementations/rust/libprovekit/src/lib.rs
Comment on lines
+25
to
+41
| ``` | ||
| $ cargo test # address_of_nonneg_round_trips ... ok (bug hides) | ||
|
|
||
| $ provekit mint --project examples/rust-missing-edge --out .../proofs --no-attest | ||
| mint ok # the rust lifter emits serialize/content_address/address_of contracts | ||
|
|
||
| $ provekit prove examples/rust-missing-edge | ||
| ProvekIt verifier report | ||
| total callsites : 3 | ||
| discharged : 2 | ||
| violations : 1 | ||
|
|
||
| [unsatisfied] content_address (source -> kit) | ||
| reason: solver 'z3' returned sat (counterexample found) | ||
| [discharged] serialize (source -> kit) unsat (obligation holds) | ||
| [discharged] address_of (source -> kit) unsat (obligation holds) | ||
| ``` |
There was a problem hiding this comment.
Add a language tag to the fenced command block.
Line 25 should specify a fence language (e.g., bash) to satisfy markdown linting and improve render/tooling behavior.
Suggested fix
-```
+```bash
$ cargo test # address_of_nonneg_round_trips ... ok (bug hides)
$ provekit mint --project examples/rust-missing-edge --out .../proofs --no-attest
mint ok # the rust lifter emits serialize/content_address/address_of contracts
$ provekit prove examples/rust-missing-edge
ProvekIt verifier report
total callsites : 3
discharged : 2
violations : 1
[unsatisfied] content_address (source -> kit)
reason: solver 'z3' returned sat (counterexample found)
[discharged] serialize (source -> kit) unsat (obligation holds)
[discharged] address_of (source -> kit) unsat (obligation holds)</details>
<!-- suggestion_start -->
<details>
<summary>📝 Committable suggestion</summary>
> ‼️ **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.
```suggestion
🧰 Tools
🪛 markdownlint-cli2 (0.22.1)
[warning] 25-25: 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 `@examples/rust-missing-edge/RESULT.md` around lines 25 - 41, The fenced
command block that begins with "$ cargo test ..." is missing a language tag;
edit the opening triple-backtick so it specifies a shell language (e.g., change
"```" to "```bash" or "```sh") to satisfy markdown linting and improve rendering
for the block that contains the cargo/provekit commands and verifier output.
Comment on lines
+558
to
564
| /// Resolve a grammar primitive's address from the code shape-authority. `Some` | ||
| /// iff `name` is a language primitive (op-application / seq / ite / bind-result); | ||
| /// the address is `json_cid` of its pinned shape, computed, never frozen. | ||
| /// Consumers derive handles from this; they never store a copy. | ||
| pub fn grammar_op_cid(name: &str) -> Option<Cid> { | ||
| ConceptOpCatalog.cid(name) | ||
| } |
There was a problem hiding this comment.
Make grammar_op_cid accept the names its docs advertise.
The new public helper documents op-application / seq / ite / bind-result, but the implementation only recognizes the fully qualified concept:* spellings. Right now grammar_op_cid("seq") and grammar_op_cid("bind-result") return None. Either normalize both forms here or document the required concept:* names consistently.
Also applies to: 1281-1345
🤖 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/libprovekit/src/core/bind.rs` around lines 558 - 564,
The function grammar_op_cid currently calls ConceptOpCatalog.cid(name) but only
recognizes fully-qualified names like "concept:seq"; update grammar_op_cid to
accept the plain names advertised by the docs by normalizing input before
lookup: if name does not start with "concept:" prepend "concept:" and then call
ConceptOpCatalog.cid, falling back to the original call if needed so both "seq"
and "concept:seq" resolve; apply the same normalization pattern to the other
similar helper(s) in this file (the related helpers around lines 1281-1345) that
also call ConceptOpCatalog.cid.
Comment on lines
+80
to
+83
| // HOW it is attested: ed25519 over the address (the WHAT). The mechanism is | ||
| // the attestor's, layered over the CID, not baked into it. | ||
| let signature = ed25519_sign_string(signer_seed, cid.as_bytes()); | ||
| witness.cid = cid; |
There was a problem hiding this comment.
Sign the canonical witness payload, not the CID string.
Line 82 signs cid.as_bytes(), but this module’s contract says the signature is over the same canonical observation bytes used to derive the CID, and implementations/rust/provekit-cli/src/cmd_verify.rs:668-741 already follows that payload-signing model. As written, this helper mints a different witness-attestation format than the rest of the CLI, so downstream signature verification will drift.
🤖 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/witness_ingest.rs` around lines 80 -
83, The code currently calls ed25519_sign_string(signer_seed, cid.as_bytes())
which signs the CID string; instead sign the canonical witness/observation bytes
used to derive that CID so the attestation format matches cmd_verify.rs. Locate
the code path that builds the canonical observation (the same bytes passed into
your CID generation routine) and pass those bytes into the ed25519 signing call
(e.g., replace cid.as_bytes() with the canonical_observation_bytes variable or
call the helper that returns them), keep assigning witness.cid = cid, and store
the produced signature on the witness; if there is a byte-oriented signing
helper (vs. sign_string) use it to avoid accidental encoding differences.
Comment on lines
+105
to
+120
| ``` | ||
| post(B) → pre(A) | ||
| ``` | ||
|
|
||
| The producer's postcondition implies the consumer's precondition. **That arrow is an | ||
| implication** — the trinity's third element, the thing `cmd_implicate` mints. (`a | b` and | ||
| `A(b())` collapse to the same invariant: *post of whoever runs first → pre of whoever runs | ||
| next*; direction follows the data, not the parentheses.) | ||
|
|
||
| This is **Hoare's rule of composition**, content-addressed: | ||
|
|
||
| ``` | ||
| {P} B {Q} {Q} A {R} | ||
| ─────────────────────── | ||
| {P} B;A {R} | ||
| ``` |
There was a problem hiding this comment.
Add language identifiers to fenced code blocks (markdownlint MD040).
Line 105 and Line 116 use unlabeled fenced blocks; add a language tag (e.g., text) to keep docs lint-clean.
Suggested patch
-```
+```text
post(B) → pre(A)@@
- +text
{P} B {Q} {Q} A {R}
───────────────────────
{P} B;A {R}
📝 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
| ``` | |
| post(B) → pre(A) | |
| ``` | |
| The producer's postcondition implies the consumer's precondition. **That arrow is an | |
| implication** — the trinity's third element, the thing `cmd_implicate` mints. (`a | b` and | |
| `A(b())` collapse to the same invariant: *post of whoever runs first → pre of whoever runs | |
| next*; direction follows the data, not the parentheses.) | |
| This is **Hoare's rule of composition**, content-addressed: | |
| ``` | |
| {P} B {Q} {Q} A {R} | |
| ─────────────────────── | |
| {P} B;A {R} | |
| ``` |
🧰 Tools
🪛 markdownlint-cli2 (0.22.1)
[warning] 105-105: Fenced code blocks should have a language specified
(MD040, fenced-code-language)
[warning] 116-116: 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 `@SHARED-LANGUAGE.md` around lines 105 - 120, Add language identifiers to the
two unlabeled fenced code blocks in SHARED-LANGUAGE.md to satisfy markdownlint
MD040: change the block containing "post(B) → pre(A)" to a fenced block with a
language tag (e.g., use ```text) and likewise add a language tag to the Hoare
rule block containing "{P} B {Q} {Q} A {R} ..." so both fenced blocks start
with ```text; update the two occurrences that wrap those exact snippets.
…ort Major, witness-mint consistency Address review feedback on the missing-edge + canonical-Int PR. * cmd_bind_integration: `bind_from_stdin_emits_named_term_document_with_promotion_decisions` asserted promotionDecisionMementos that the teardown removed → renamed to `_without_promotion` and inverted the assert to GUARD the teardown (promotionDecisionMementos MUST be null). Unblocks the conformance gate (this was the only real test-rust failure; the prove×2 are inherited exit-127 infra). * types.rs (Codex P1): preHash/antecedentHash were already pulled from formula_to_memento in Hole 2; consequentHash was left in. Codex flagged the same category error: an implication's consequent Q holds only GIVEN the antecedent P, so Tier 0 verify(Q) treating it as unconditional is wrong. Pulled. verify_implication/can_implies discharge through implication mementos directly and do not need the consequent in this index. * handshake.rs (CodeRabbit Major): wrap_post_forall bound the carrier `result` using formalSorts[0], which models PARAMETER sorts, not the return type (formalSorts is paired with formals). Bind `result` as canonical Int — matching build_implication_obligation's default and the verifier's LIA model. A non-Int return would need the contract's return sort, which the memento does not expose separately today. resolve_target's pre-binder uses formalSorts[0] for the FIRST FORMAL — that path is correct and unchanged. * cmd_verify.rs (CodeRabbit Major + consistency with witness_ingest): mint_verification_witness hashed a `signable` JSON that INCLUDED `signed_by` (so the CID encoded the attestor — violating the recompute_cid contract, signed_by/signature are HOW not WHAT) and signed JCS(signable). Aligned with witness_ingest: build the memento with empty signature, derive CID via recompute_cid() (excludes signed_by/signature from the preimage), sign the CID. Both witness-mint paths now share one scheme: same observation => same CID regardless of who attests, signature attests the CID. (Push-back on CodeRabbit's 'sign canonical bytes' — sign-the-address is the intentional design.) Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
There was a problem hiding this comment.
Actionable comments posted: 1
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-cli/src/cmd_verify.rs (1)
161-175:⚠️ Potential issue | 🟠 Major | ⚡ Quick winReject the removed promotion flags instead of accepting them as no-ops.
run()no longer consultsrequire_empirically_witnessed,require_fixture, orconsensus_policy, but the CLI still accepts them and advertises gating semantics. That lets callers believe an empirical-witness gate ran when they actually got a normal verification pass. Either remove these options now or returnEXIT_USER_ERRORwhen any of them is set.Suggested guard
pub fn run(args: VerifyArgs) -> u8 { + if args.require_empirically_witnessed.is_some() + || args.require_fixture.is_some() + || args.consensus_policy.is_some() + { + eprintln!( + "{}: promotion/consensus gating was removed; \ + --require-empirically-witnessed, --require-fixture, and \ + --consensus-policy are no longer supported", + "error".red().bold() + ); + return EXIT_USER_ERROR; + } + // Early dispatch: the supply-chain admission gate. When any ofAlso applies to: 246-261
🤖 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_verify.rs` around lines 161 - 175, The CLI still defines the flags require_empirically_witnessed, require_fixture, and consensus_policy but run() no longer honors them; update run() to reject these removed promotion flags by checking if any of require_empirically_witnessed, require_fixture, or consensus_policy is Some(...) and immediately return a user-error exit (use EXIT_USER_ERROR or equivalent) with a clear message that the flag is removed, so callers aren’t misled; apply the same guard for the duplicate flags in the later block (the other set at lines ~246-261) and ensure the help text is adjusted if you instead choose to delete the options.
🧹 Nitpick comments (2)
implementations/rust/provekit-verifier/src/types.rs (1)
303-309: ⚡ Quick winCover the
consequentHashside of this fix with a unit test.The new indexing rule protects both contract preconditions and implication consequents, but the added test only exercises
preHash. A small implication-memento test assertingpool.verify(Q).is_none()would keep theconsequentHashregression from slipping back independently.Also applies to: 964-1000
🤖 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/types.rs` around lines 303 - 309, Add a unit test that mirrors the existing preHash test but exercises implication consequents: construct an implication memento where antecedent P is indexed but consequent Q is present in the pool as a stand‑alone fact, then assert pool.verify(Q).is_none(); place the test alongside the existing preHash test (e.g., name it test_consequent_hash_protection) and rely on the pool.verify / verify_implication / can_implies code paths so it fails if the protection for consequentHash is removed.implementations/rust/provekit-cli/src/cmd_verify.rs (1)
698-722: ⚡ Quick winAdd a regression test for signer-independent witness CIDs.
This path's new contract is "same observation, different attestor => same
cid". The current test only checks that a signature exists, so a futurerecompute_cidchange could quietly pullsigned_byback into the preimage. Please add a two-signer test that asserts equalcids and different signatures.🤖 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_verify.rs` around lines 698 - 722, Add a regression test that ensures witness CIDs are signer-independent: construct a WitnessMemento with the same observation fields (e.g., witness_for, subject, fixture_state_cid, observed_at, sample_count, measurements, outcome) but with two different signers (different signed_by and signer seeds), call recompute_cid() on both, sign each CID with ed25519_sign_string, and assert that both recomputed cid values are equal while the signature fields differ; reference WitnessMemento, recompute_cid, signed_by, signature, cid, and ed25519_sign_string when locating where to build the test and perform the comparisons.
🤖 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-verifier/src/handshake.rs`:
- Around line 162-169: The code currently hardcodes the synthesized `result`
binder sort to Int (the `sort` variable near `producer_body`) which mis-types
non-integer producer returns; update the logic that assigns `sort` to instead
obtain the producer's actual return sort from the producer's memento/signature
(the same metadata used elsewhere when building obligations, e.g.,
`build_implication_obligation`), convert it into the expected JSON
representation rather than `{"kind":"primitive","name":"Int"}`, and use that
value for the `result` binder; if the producer return sort is not present in the
memento, fail closed by returning an error (or propagate a failure) rather than
defaulting to Int so we don't produce ill-typed obligations or change tier
hashes.
---
Outside diff comments:
In `@implementations/rust/provekit-cli/src/cmd_verify.rs`:
- Around line 161-175: The CLI still defines the flags
require_empirically_witnessed, require_fixture, and consensus_policy but run()
no longer honors them; update run() to reject these removed promotion flags by
checking if any of require_empirically_witnessed, require_fixture, or
consensus_policy is Some(...) and immediately return a user-error exit (use
EXIT_USER_ERROR or equivalent) with a clear message that the flag is removed, so
callers aren’t misled; apply the same guard for the duplicate flags in the later
block (the other set at lines ~246-261) and ensure the help text is adjusted if
you instead choose to delete the options.
---
Nitpick comments:
In `@implementations/rust/provekit-cli/src/cmd_verify.rs`:
- Around line 698-722: Add a regression test that ensures witness CIDs are
signer-independent: construct a WitnessMemento with the same observation fields
(e.g., witness_for, subject, fixture_state_cid, observed_at, sample_count,
measurements, outcome) but with two different signers (different signed_by and
signer seeds), call recompute_cid() on both, sign each CID with
ed25519_sign_string, and assert that both recomputed cid values are equal while
the signature fields differ; reference WitnessMemento, recompute_cid, signed_by,
signature, cid, and ed25519_sign_string when locating where to build the test
and perform the comparisons.
In `@implementations/rust/provekit-verifier/src/types.rs`:
- Around line 303-309: Add a unit test that mirrors the existing preHash test
but exercises implication consequents: construct an implication memento where
antecedent P is indexed but consequent Q is present in the pool as a stand‑alone
fact, then assert pool.verify(Q).is_none(); place the test alongside the
existing preHash test (e.g., name it test_consequent_hash_protection) and rely
on the pool.verify / verify_implication / can_implies code paths so it fails if
the protection for consequentHash is removed.
🪄 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: 03d7fccb-44bf-48bc-ba02-1c59b45e7559
📒 Files selected for processing (4)
implementations/rust/provekit-cli/src/cmd_verify.rsimplementations/rust/provekit-cli/tests/cmd_bind_integration.rsimplementations/rust/provekit-verifier/src/handshake.rsimplementations/rust/provekit-verifier/src/types.rs
Comment on lines
+162
to
+169
| // The carrier `result` is the producer's RETURN value, not a parameter, so | ||
| // its sort is NOT `formalSorts[i]` (those model parameter sorts, paired | ||
| // with `formals`). The verifier reasons in LIA; bind the carrier as the | ||
| // canonical `Int`, matching `build_implication_obligation`'s default. A | ||
| // non-Int return would need the contract's return sort, which the memento | ||
| // does not expose separately today. | ||
| let _ = producer_body; | ||
| let sort = serde_json::json!({"kind": "primitive", "name": "Int"}); |
There was a problem hiding this comment.
Don't hard-code every synthesized result binder to Int.
Canonicalizing i* widths to Int fixes the integer case, but this wrapper now also turns non-integer producer returns into forall result: Int, which makes the synthesized implication ill-typed and changes the Tier 1/Tier 2 hashes. Please plumb the producer's actual return sort here, or fail closed when it is not available.
🤖 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/handshake.rs` around lines 162 -
169, The code currently hardcodes the synthesized `result` binder sort to Int
(the `sort` variable near `producer_body`) which mis-types non-integer producer
returns; update the logic that assigns `sort` to instead obtain the producer's
actual return sort from the producer's memento/signature (the same metadata used
elsewhere when building obligations, e.g., `build_implication_obligation`),
convert it into the expected JSON representation rather than
`{"kind":"primitive","name":"Int"}`, and use that value for the `result` binder;
if the producer return sort is not present in the memento, fail closed by
returning an error (or propagate a failure) rather than defaulting to Int so we
don't produce ill-typed obligations or change tier hashes.
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
1 participant
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.
The honest-substrate arc from this session, one cohesive branch: the catalog is fiction, promotion/consensus is severable cruft, the witness axis is real, and ProvekIt's defining capability — catching the bug the unit test is designed to catch and doesn't — now works end-to-end through the real verbs, on a canonical
Intsort that federates cross-language.Catalog = fiction (starts empty; grammar pinned by code-shape, not disk)
cc9d00a9the catalog starts empty (kill the seed)06f67e90grammar pinned by shape in code, not disk8f8975d6concept_bind_result_cidcomputes from shape, kill the pinned literalb6df3567bind_kit resolves op CIDs against the code shape-authorityPromotion / consensus = cruft, removed
dd784bd5remove the empirically-witnessed promotion gate (prove/verify)f77dc269rip the witness-consensus promotion path + promotion_query85dd7030stop minting promotion decisions0005159edelete promotion_decision_registry + promotion/consensus testsWitness axis = real
eb0b70a0ingestion converter: contents-that-form-a-witness → WitnessMemento (the CID signs the WHAT — subject/fixture/measurements/outcome — not the HOW;signed_by/signatureexcluded from the preimage)f10f2485observed_atis caller-provided; CID viarecompute_cidThe missing edge, caught through the real verbs
a88a87b3therust-missing-edgecrate (landed first as a documented false green —provereported the buggy seam as discharged)c443690fthe four stacked fixes that make the catch real, all below the language line:MementoPool::insertindexed a contract'spreHashinto the map Tier 0 trusts as proven-true; a precondition is an obligation, not a fact. Index onlypostHash/invHash/consequentHash.lift_expr_to_term_innerhad noExpr::Callarm, so a nested-call body collapsed to a vacuoustrueand the callees were invisible. Lift the call tree (1 → 3 callsites).locate_producer_postread the v1.1 shape while mint emits v1.2. Synthesizeforall(formal)at the discharge boundary; make the producer-post lookup shape-agnostic.Int—sort_translateemitted width-distinct Rust names (I64/U32/Usize), violating canonicalization-grammar §5 (fixed set{Bool,Int,Real,String,Ref}) and breaking federation (Rusti64≠ Javalongat the CID level). Collapse integer widths →Int: width is a range refinement that rides the sugar, not a sort. Deletes thesmt_binder_sortverifier hack outright.Result:
provekit mint→provereports 3 callsites —content_addressunsatisfied (z3 sat on thevalue<0seamserialize.postcannot establish),serialize/address_ofdischarged. The unit test passes; the solver does not.Docs
1ce241d6SHARED-LANGUAGE.md — the canonical dictionary, pulled off thespike/honest-domain-inventoryworktree onto the main line.Verification
provekit-walk238,provekit-verifier65, CID-stability + source-round-trip +d7_v4_widen— all green. Width was already riding the sugar; theIntcollapse broke no round-trip or CID.🤖 Generated with Claude Code
Summary by CodeRabbit
New Features
Bug Fixes
Refactor
Tests/Chores