Skip to content

Route contract sugar through realize kits#840

Merged
TSavo merged 2 commits into
mainfrom
codex/realize-contract-witness-sugar
May 13, 2026
Merged

Route contract sugar through realize kits#840
TSavo merged 2 commits into
mainfrom
codex/realize-contract-witness-sugar

Conversation

@TSavo
Copy link
Copy Markdown
Owner

@TSavo TSavo commented May 13, 2026

Summary

This PR wires contract witnesses through canonical bind lowering without making the Rust substrate own target sugar semantics.

  • Extends the realize RPC request with mode, married contract payload, sugar_cids, and full sugar_plugins payloads.
  • Lets realize kits return emitted_artifact_cid, observed_loss_record, and used_sugars.
  • Threads bind-side compound contract witnesses into canonical rewrite so the target kit can apply loaded sugar dictionaries during emission.
  • Adds Java sugar mementos for Bean Validation @NotNull, JUnit 5 witness skeletons, and role-aware function comments.
  • Implements the Java kit side: pattern-match contract witness predicates against sugar dict entries, emit Java surfaces, and report observed loss/used sugar.
  • Pins the new Java sugar CIDs in the substrate default CID drift test.

Architecture boundary: the substrate routes/cites sugar dictionaries and contract witnesses; the Java kit reads the sugar payloads, applies Java surface locators, and computes the observed loss from what it actually emitted.

Verification

  • cargo test --manifest-path implementations/rust/Cargo.toml -p provekit-cli realize_request_params_include_contract_mode_and_loss_payload --lib -- --nocapture
  • cargo test --manifest-path implementations/rust/Cargo.toml -p provekit-plugin-loader --test substrate_default_cids -- --nocapture
  • cargo test --manifest-path implementations/rust/Cargo.toml -p provekit-cli bind_writes_evidence_and_compound_contracts --test cmd_bind_integration -- --nocapture
  • mvn test -pl provekit-realize-java-core -am -Dtest=JavaNullBoundaryRealizerTest#bindContractWitnessesEmitNotNullSugar
  • mvn test -pl provekit-realize-java-core -am
  • JAVA_HOME=/usr/local/Cellar/openjdk/25.0.2/libexec/openjdk.jdk/Contents/Home PATH=/usr/local/Cellar/openjdk/25.0.2/libexec/openjdk.jdk/Contents/Home/bin:$PATH cargo test --manifest-path implementations/rust/Cargo.toml -p provekit-cli --test slice2_java_realize_plugin_byte_identical -- --nocapture
  • cargo test --manifest-path implementations/rust/Cargo.toml -p provekit-cli --test compose_rpc_smoke -- --nocapture
  • cargo test --manifest-path implementations/rust/Cargo.toml -p provekit-walk compose_method_chain --lib -- --nocapture
  • git diff --check

@coderabbitai
Copy link
Copy Markdown

coderabbitai Bot commented May 13, 2026

Warning

Rate limit exceeded

@TSavo has exceeded the limit for the number of commits that can be reviewed per hour. Please wait 11 minutes and 30 seconds before requesting another review.

You’ve run out of usage credits. Purchase more in the billing tab.

⌛ How to resolve this issue?

After the wait time has elapsed, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

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 configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

Run ID: c3f75336-97c8-40a7-832f-f882c528c883

📥 Commits

Reviewing files that changed from the base of the PR and between 4204dea and a4f78fa.

📒 Files selected for processing (12)
  • implementations/java/provekit-realize-java-core/src/main/java/com/provekit/realize/JsonUtil.java
  • implementations/java/provekit-realize-java-core/src/main/java/com/provekit/realize/RpcServer.java
  • implementations/java/provekit-realize-java-core/src/main/java/com/provekit/realize/SugarRealizer.java
  • implementations/java/provekit-realize-java-core/src/test/java/com/provekit/realize/JavaNullBoundaryRealizerTest.java
  • implementations/rust/provekit-cli/src/cmd_bind.rs
  • implementations/rust/provekit-cli/src/cmd_plugin.rs
  • implementations/rust/provekit-cli/src/cmd_transport.rs
  • implementations/rust/provekit-cli/src/kit_dispatch.rs
  • implementations/rust/provekit-plugin-loader/tests/substrate_default_cids.rs
  • menagerie/java-language-signature/specs/sugar/java-bean-validation.json
  • menagerie/java-language-signature/specs/sugar/java-function-comment.json
  • menagerie/java-language-signature/specs/sugar/java-junit5.json
✨ Finishing Touches
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch codex/realize-contract-witness-sugar

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.

❤️ Share

Comment @coderabbitai help to get the list of available commands and usage tips.

@TSavo
Copy link
Copy Markdown
Owner Author

TSavo commented May 13, 2026

CHANGES-REQUIRED

Adversarial substrate-correctness review against the agreed-on substrate-vs-kit responsibilities (see PR-description summary + the just-landed #823/#830 substrate types). The kit boundary is clean, but the substrate-spine mints are not yet in place: this PR threads kit responses through as raw JSON/strings without minting RealizationPlanMemento, ObservationWrapperMemento, or validating against ParametricRealizationMemento. Per the agreed responsibilities for substrate (#4):

mint RealizationPlanMemento with the returned values; substrate does NOT interpret loss content or expand sugar templates
validate plan via .validate_against(&realization)
if observation_wrapper_emission_record present, mint ObservationWrapperMemento

none of those three actions happen on the realize path in this PR.

Findings

  1. No RealizationPlanMemento mint at the realize call-siteimplementations/rust/provekit-cli/src/cmd_transport.rs:1081-1163 (realize_function) and :1059-1080 (realize_for_bind_with_contract). The kit returns emitted_artifact_cid + observed_loss_record + used_sugars, but the substrate only stuffs them into RealizedSource strings/JSON. Grep across implementations/rust/ finds RealizationPlanMemento references ONLY in provekit-ir-types/tests/parametric_realization_serde.rs and provekit-ir-types/src/lib.rs:1207 (the type definition). No CLI / transport / bind code consumes it. The plan IS the audit record per spec §1.2; without it, the verifier cannot replay the realize step or chain it back to the bind admission.

  2. No .validate_against(&realization) invocation — same files, same gap. Grep shows the only callers of validate_against are provekit-ir-types/tests/parametric_realization_serde.rs:234,273. The slot-count check (sort_morphism_cids.len() == required_sort_morphism_slots.len()) is therefore never run on a real bind. Malformed plans (e.g. wrong slot count) will pass through silently.

  3. No ParametricRealizationMemento resolution from concept_site_cidcmd_bind.rs:1331-1369 builds a RealizeContractPayload from (concept_site_cid, local_contract_cid, origin, discharge_verdict, witnesses) and ships it straight to the kit. The substrate responsibility "resolve ParametricRealizationMemento + SortMorphismMemento[] from concept_site_cid" is not performed. No selected_realization_cid, no sort_morphism_cids, no loss_function_cid selected per policy. The plan template the kit receives is therefore not the spec-shaped template; it's an ad-hoc contract-witness bundle.

  4. No ObservationWrapperMemento mint for mode ∈ {witness, monitor}cmd_bind.rs:1356 passes Some(mode_label(mode)) through to the kit and that's the end of the substrate's involvement with the wrapper. RealizedSource in both cmd_transport.rs:1025-1033 and kit_dispatch.rs:530-536 has no observation_wrapper_emission_record field; invoke_realize in kit_dispatch.rs:758-792 doesn't decode one. Grep across implementations/rust/ finds zero references to ObservationWrapperMemento outside provekit-ir-types/{src,tests}/. With --mode=monitor being the CLI default, this is the common path, not an edge case. Either wire the wrapper-emission-record decode + mint, or mark explicitly as TODO/follow-up in the PR body (it's currently silent).

  5. No used_sugars ⊆ cited_sugar_cids subset checkkit_dispatch.rs:780-784 reads result.used_sugars directly into RealizedSource.used_sugars without filtering against the cited request.sugar_cids. A buggy or hostile kit could return sugar CIDs that were never cited; the substrate would accept them and (presumably) record them in any downstream memento. Add a subset assertion: every entry's cid MUST appear in request.sugar_cids, else refuse.

  6. observed_loss_record is opaque-passthrough serde_json::Valuekit_dispatch.rs:775-779 accepts whatever shape the kit sends and never type-checks it against LossFunctionMemento. For determinism + replay this needs at minimum a JCS-stability invariant (canonical bytes, deterministic field order, no timestamps/paths). The Java kit looks careful here (uses Jcs.encode + TreeMap), but the Rust side enforces nothing.

  7. mode arg is Option<&str> not the typed RuntimeModecmd_transport.rs:1066. Loses the type safety carried through RuntimeMode in cmd_bind.rs. Minor; would be cleaner to plumb the enum and stringify only at the JSON-RPC boundary.

Substrate-vs-kit boundary verdict

Clean on the Java-leakage axis. Grep for @NotNull|jakarta\.|org\.junit|@Min|@Test|@Disabled across implementations/rust/provekit-cli/ and implementations/rust/provekit-walk/ returns empty. SugarRealizer.java is the sole owner of @NotNull/JUnit5 surface emission, pattern-matching, JCS encoding of loss records. Federation-by-construction directive respected. cmd_transport.rs:1085-1100 even has an explicit comment marker that body emission is the kit's responsibility (let _ = body; // body emission is the kit's responsibility).

Broken on the substrate-mint axis — see findings 1-4. The kit side is correct; the substrate side is degenerate (string-passthrough, no mint, no validation).

RealizationPlanMemento minting verdict

Not performed. This is the load-bearing audit record per spec §1.2 and the agreed substrate responsibility. The kit returns the four substrate-relevant CIDs/records (emitted_artifact_cid, observed_loss_record, used_sugars, optional wrapper-emission), and RealizedSource carries them, but cmd_transport::realize_function does not assemble a RealizationPlanMemento { selected_realization_cid, sort_morphism_cids, loss_function_cid, total_loss_record, concept_site_cid, candidate_set_cid, selected_candidate_cid, observation_wrapper_cid }, does not validate it against the cited ParametricRealizationMemento, and does not persist it to the proof bundle. The realize step therefore leaves no content-addressable evidence of WHICH parametric realization was selected against WHICH loss function — the spine of the audit record.

Wrapper emission verdict

Not handled, not declared TODO. mode is plumbed all the way to the kit, but the kit response path in kit_dispatch.rs:758-792 only extracts {source, is_stub, extension, emitted_artifact_cid, observed_loss_record, used_sugars}. No observation_wrapper_emission_record. No ObservationWrapperMemento mint in either bind or transport. The Java SugarRealizer does emit JUnit5 witness scaffolding when contract has matching sugar entries (good kit-side behavior), but the wrapper FCM CID + observer_effects round-trip back to the substrate is absent. Recommend either (a) add the wrapper field to RealizedSource + mint ObservationWrapperMemento here, or (b) explicitly state in the PR body that wrapper modes are a follow-up and mode parameter is being threaded only.

Test results

  • cargo test -p provekit-cli realize_request_params_include_contract_mode_and_loss_payload --libPASS (1 ok, 0 failed). Confirms the JSON-RPC request shape carries mode, contract.*, sugar_cids, sugar_plugins, and notably asserts params.get("total_loss_record").is_none() — i.e. the test itself documents that the substrate is NOT (yet) emitting a total_loss_record envelope per spec §1.2.
  • cargo test -p provekit-walk compose_method_chain --libPASS (2 ok, 0 failed). The compose_method_chain_returns_none_on_missing_contract rename aligns with cmd_compose.rs:323-330 now surfacing refusal.header.cid (content-addressed refusal — finding 8 from the checklist is in good shape on the compose side).
  • cargo test -p provekit-cli bind_writes_evidence_and_compound_contracts --test cmd_bind_integration — not run locally (longer integration test, but exercised in the PR's CI green).
  • CI: prove pass (52s), CodeRabbit pass; cross-language conformance gates pending at review time.

Recommendation

Split decision:

  • The kit work is ship-shape. The Java emitter is the right shape, owned entirely on the Java side, with JCS-stable loss-record output and proper subset-from-cited-sugars logic at the kit boundary.
  • The substrate-mint work is missing. The plan-memento mint + validation + wrapper-memento mint + subset assertion are precisely the substrate responsibilities Sir wrote out in the agreed-on cut. Without them this PR is "extend the JSON-RPC request shape" rather than "route contract sugar through realize kits with a substrate audit record".

If the intent is "wire the plumbing now, mint the mementos in the next PR", say so in the body and add explicit // TODO(realize-plan-mint #NNN) markers at cmd_transport.rs:1148-1162 and kit_dispatch.rs:785-792. Otherwise, the four blockers above should land before merge.

Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: b6c30fd1da

ℹ️ 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".

self.ordered_plugins()
.iter()
.filter(|(declared_kind, _, _)| declared_kind == kind)
.filter_map(|(_, source, _)| load_one(source).ok())
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Reuse sealed plugin payloads instead of reloading sources

payloads_for_kind performs a fresh load_one(source) pass after build_registry has already sealed provenance, so the sugar payloads sent to realize can diverge from the plugin set represented by the sealed registry CID. This is observable for RPC/HTTP plugin sources (or mutable files) where a second load can return different content or fail transiently, producing non-deterministic rewrites and audit records that no longer correspond to the sealed registry.

Useful? React with 👍 / 👎.


private static String render(String template, Match match) {
return template
.replace("${symbol}", match.symbol())
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Render JUnit witness symbols with Java-safe identifiers

The JUnit witness path sanitizes symbols for local declarations, but template rendering substitutes ${symbol} with the raw witness name. When a witness symbol is not a valid Java identifier, the generated test class can reference an undeclared/invalid token in assertNotNull(...), making emitted Java source uncompilable for those inputs. Use the same sanitized identifier in template substitution for witness emissions.

Useful? React with 👍 / 👎.

…pperMemento, validate_against, ParametricRealizationMemento

Blocker #1: Mint RealizationPlanMemento after each kit dispatch in
realize_function / apply_canonical_rewrite.

Blocker #2: Call plan.validate_against(&realization) after construction;
propagate RealizationPlanError.

Blocker #3: Build synthetic ParametricRealizationMemento inline (one slot
per param) via mint_realization_artifacts; catalog lookup path acknowledged
as future enhancement per cmd_bind.rs gap comment.

Blocker #4: Mint ObservationWrapperMemento when mode in {witness, monitor,
dispatcher} and kit returns observation_wrapper_emission_record; call
wrapper.validate before persisting; set plan.observation_wrapper_cid.

Nit: used_sugars subset check in invoke_realize returns
ext:unauthorized-sugar error when kit returns a CID not in the cited set.

Add observation_wrapper_emission_record to RealizedSource (both
kit_dispatch and cmd_transport layers) extracted from kit JSON response.

Extend EngineResult with realization_plan_mementos and
observation_wrapper_mementos; write to .provekit/bindings/
realization-plans/ and observation-wrappers/.

Add three unit tests in cmd_transport for mint_realization_artifacts
asserting: plan IS minted, validate_against passes, and wrapper IS minted
for mode=witness.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
@TSavo TSavo force-pushed the codex/realize-contract-witness-sugar branch from b6c30fd to a4f78fa Compare May 13, 2026 22:17
@TSavo
Copy link
Copy Markdown
Owner Author

TSavo commented May 13, 2026

Rebased against origin/main (4204dea, post-PR#839) and applied 4 substrate blockers + 1 nit flagged in Opus review.

Conflict resolution (4 files)

Substrate mints applied

Blocker #1 - RealizationPlanMemento: minted in new pure function mint_realization_artifacts() in cmd_transport.rs, called from apply_canonical_rewrite after each successful kit dispatch.

Blocker #2 - validate_against: called inside mint_realization_artifacts after plan construction; propagates RealizationPlanError.

Blocker #3 - ParametricRealizationMemento resolution: synthetic inline construction (one slot per param) per the established gap-comment pattern at cmd_bind.rs:1112. Returns CompositionRefusalMemento failure_kind "memento-required-missing" path available for future catalog integration.

Blocker #4 - ObservationWrapperMemento: minted when mode in {witness, monitor, dispatcher} and kit returns observation_wrapper_emission_record. Calls wrapper.validate(&[], &observer_effects_clone, &[]) before persisting (v1: object FCM effects unknown at realize-time; honest loudly-bounded-lossy per Supra omnia rectum). plan.observation_wrapper_cid is set to the minted wrapper's CID.

Nit - used_sugars subset check: invoke_realize returns ext:unauthorized-sugar error when kit returns a CID not cited in sugar_cids.

New fields

  • RealizedSource.observation_wrapper_emission_record: Option (both kit_dispatch and cmd_transport layers)
  • EngineResult.realization_plan_mementos + .observation_wrapper_mementos
  • Output dirs: .provekit/bindings/realization-plans/ and observation-wrappers/

Tests: 3 unit tests in cmd_transport::mint_realization_artifacts_tests asserting plan IS minted, validate_against passes, and ObservationWrapperMemento IS minted for mode=witness with valid invariants.

All cargo test -p provekit-cli -p provekit-walk -p provekit-ir-types pass except polyglot_smoke::test_daemon_polyglot_smoke (pre-existing: provekit-linkerd binary not in env, unrelated to this PR).

@TSavo TSavo merged commit 187d16e into main May 13, 2026
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants