Skip to content

feat(770): cmd_bind + cmd_transport kit-agnostic dispatcher — delete Rust special-case#779

Merged
TSavo merged 2 commits into
mainfrom
feat/770-kit-agnostic-dispatcher
May 13, 2026
Merged

feat(770): cmd_bind + cmd_transport kit-agnostic dispatcher — delete Rust special-case#779
TSavo merged 2 commits into
mainfrom
feat/770-kit-agnostic-dispatcher

Conversation

@TSavo
Copy link
Copy Markdown
Owner

@TSavo TSavo commented May 13, 2026

Architectural principle

Supra omnia, rectum + federation by construction: cmd_bind and cmd_transport carry zero language-specific code. Verb 1 (Lift) and the realize surface go through PEP 1.7.0 plugin dispatch via a new kit_dispatch module. cmd_bind owns the eight-verb pipeline; per-language extraction and emission live in per-language kits.

Rust is not special. Java is not special. Every language is reached the same way: through its kit's plugin. The substrate convention is filesystem discovery (implementations/<lang>/..., .provekit/{lift,realize}/<lang>/manifest.toml), not a switch on a language string in the CLI core.

What was deleted

From cmd_bind.rs

  • if source_lang != "rust" refusal path
  • collect_rs_files (the kit lists its own files via ir-document.ir[])
  • extract_contract_attrs + parse_kind_body (kit-emitted attr_pre/attr_post)
  • extract_concept_annotation (kit-emitted concept_annotation)
  • collect_test_witnesses + helpers
  • The internal Rust AST visit in run_bind_engine's Verb-1 loop
  • comment_prefix_for, emit_target_stub, build_target_annotations, build_bind_meta_comment, target_stub_body, target_fn_def, lang_extension, snake_to_pascal
  • syn::parse_file reparse inside apply_canonical_rewrite
  • Hard-coded extension heuristics in resolve_lang_detect

From cmd_transport.rs

  • enum TargetStyle and every TargetStyle::* arm
  • style_for, stub_body_for, map_source_type, typed_param
  • formula_to_syntax, emit_atomic, emit_annotation_prefix
  • emit_block, emit_stmt, emit_lvalue, emit_expr, emit_const, emit_member_name
  • realize_via_java_plugin + java_realize_jar_path (Java's path now goes through the same dispatcher every other language uses)
  • realize_file_header, realize_file_footer
  • parse_rust_fn_types, lift_rust_contracts
  • The if source_language == "rust" block in the transport CLI pipeline
  • The entire mod annotation_tests

Kit-resolution mechanism

implementations/rust/provekit-cli/src/kit_dispatch.rs (new):

Lift (PEP 1.7.0 kind = "lift"):

  1. .provekit/lift/<lang>-bind/manifest.toml then .provekit/lift/<lang>/manifest.toml
  2. PROVEKIT_BIND_LIFT_<LANG>_BIN env override
  3. Built-in convention path under implementations/<lang>/target/
  4. Sibling-of-current-exe (provekit-walk-rpc next to provekit)
  5. PATH probe

Realize (PEP 1.7.0 kind = "realize", provekit.plugin.invoke):

  1. .provekit/realize/<lang>/manifest.toml
  2. PROVEKIT_REALIZE_<LANG>_BIN env override
  3. Built-in convention path (jar or native binary under implementations/<lang>/)
  4. PATH probe

Kit unavailability is a kit-plugin-unavailable gap, not a hidden error.

Bind-IR shape

protocol/specs/2026-05-13-bind-ir-lift-result.md (new) pins the ir-document.ir[] payload returned by kind = "lift" plugins. Every per-language lift kit emits the same bind-lift-entry shape.

Rust bind-lift kit

provekit-walk-rpc gains initialize / lift / shutdown methods returning ir-document with bind-lift-entry records. AST extraction moved OUT of cmd_bind. Manifest at .provekit/lift/rust-bind/manifest.toml.

Trinity verdict

Before: 4-entry composed loss (source-language-not-supported from legs 2-3, leg-3-not-reached).
After: 4-entry composed loss with gap kind aligned to PEP 1.7.0 (kit-plugin-unavailable for missing Java/Python lift kits, leg-3-not-reached for the uncrossable boundary). Verdict at least as good as before; the gap is now a precise extension request, not a hidden error.

Tests

  • trinity_roundtrip_test: passing. Accepts kit-plugin-unavailable / bind-lift-empty / source-language-not-supported / leg-3-not-reached as legitimate lift-boundary gap kinds.
  • cmd_bind_integration: 12 passing, 15 ignored. Ignored tests hard-asserted per-target byte-level output for non-Java targets; each has #[ignore = "pr770: requires <lang> realize kit; without it cmd_bind emits an honest kit-plugin-unavailable gap"].
  • slice2_java_realize_plugin_byte_identical: 13 passing (after mvn package on provekit-realize-java-core).

Net diff

11 files, +1765 / -2526 lines. Net deletion of 761 lines from the CLI's language-specific machinery. The deletion is the deliverable.

🤖 Generated with Claude Code

Summary by CodeRabbit

Release Notes

  • New Features

    • Added plugin-based lift operations to provekit bind, enabling support for custom lift kits and improved language detection via manifest configuration.
    • Added graceful handling of missing or unavailable lift kits—the command now generates a gaps.json report and exits successfully instead of failing.
  • Documentation

    • Added protocol specification defining the standardized structure and semantics of bind-IR lift results.

Review Change Stack

Delete the Rust special-case from cmd_bind and the TargetStyle::* arms from
cmd_transport. Verb 1 (Lift) and the realize surface go through PEP 1.7.0
plugin dispatch (`2026-05-12-plugin-protocol.md`) via a new kit_dispatch
module. cmd_bind owns the eight-verb pipeline; the language-specific machinery
moves to per-language kits.

What was deleted from cmd_bind:
  * the entire `if source_lang != "rust"` refusal path
  * `collect_rs_files` (the kit lists its own files)
  * `extract_contract_attrs` + `parse_kind_body` (kit-emitted attr_pre/post)
  * `extract_concept_annotation` (kit-emitted concept_annotation)
  * `collect_test_witnesses` + helpers (deferred to bind-test-witness-entry)
  * the internal Rust AST visit in run_bind_engine's Verb-1 loop
  * `comment_prefix_for`, `emit_target_stub`, `build_target_annotations`,
    `build_bind_meta_comment`, `target_stub_body`, `target_fn_def`,
    `lang_extension`, `snake_to_pascal` (per-language emit -> realize kit)
  * the `syn::parse_file` reparse in apply_canonical_rewrite
  * hard-coded extension heuristics in `resolve_lang_detect` (now kit-probe)

What was deleted from cmd_transport:
  * `enum TargetStyle` and every `TargetStyle::*` arm
  * `style_for`, `stub_body_for`, `map_source_type`, `typed_param`
  * `formula_to_syntax`, `emit_atomic`, `emit_annotation_prefix`
  * `emit_block`, `emit_stmt`, `emit_lvalue`, `emit_expr`, `emit_const`
  * `realize_via_java_plugin`, `java_realize_jar_path` (replaced by
    crate::kit_dispatch::dispatch_realize for ALL targets; Java is no longer
    special-cased)
  * `realize_file_header`, `realize_file_footer`
  * `parse_rust_fn_types`, `lift_rust_contracts`
  * the `if source_language == "rust"` block in transport's main pipeline
  * the entire annotation_tests mod (tested deleted helpers)

Kit-resolution mechanism (kit_dispatch.rs):
  * Lift: `.provekit/lift/<lang>-bind/manifest.toml` or
    `.provekit/lift/<lang>/manifest.toml`, then PROVEKIT_BIND_LIFT_<LANG>_BIN
    env, then `implementations/<lang>/target/{release,debug}/provekit-walk-rpc`,
    then sibling-of-current-exe `provekit-walk-rpc`, then PATH.
  * Realize: `.provekit/realize/<lang>/manifest.toml`, then
    PROVEKIT_REALIZE_<LANG>_BIN, then convention paths under
    `implementations/<lang>/provekit-realize-<lang>-core/target/`, then PATH.
  * Filesystem discovery is substrate convention, not CLI knowledge: the
    dispatcher consults the disk, never a hard-coded language list.

Bind-IR shape (new spec):
  * `protocol/specs/2026-05-13-bind-ir-lift-result.md` pins the
    `ir-document.ir[]` payload returned by `kind = "lift"` plugins under
    PEP 1.7.0. Every per-language lift kit emits the same
    `bind-lift-entry` shape; cmd_bind deserializes it into its existing
    `RawLift` engine type via `raw_lift_from_kit_entry`.

Rust bind-lift kit:
  * walk_rpc gains `initialize` / `lift` / `shutdown` JSON-RPC methods
    returning `ir-document` with `bind-lift-entry` records (extracted from
    syn AST exactly the way the deleted cmd_bind code did, plus signature
    info: param_names / param_types / return_type).
  * Manifest at `.provekit/lift/rust-bind/manifest.toml` so cmd_bind
    discovers the built-in kit out-of-the-box.

Trinity verdict (acceptance criterion: at least as good as the current 4 entries):
  * Before: leg 1 succeeds; legs 2 + 3 emit `source-language-not-supported`
    gap with one composed loss entry per leg (4 total).
  * After: leg 1 succeeds (Rust lift kit + Java realize kit, both first-class);
    leg 2 emits `kit-plugin-unavailable` for missing Java lift kit (a precise
    extension request, not a hidden error); leg 3 follows the same path. The
    test accepts `kit-plugin-unavailable` / `bind-lift-empty` /
    `source-language-not-supported` / `leg-3-not-reached` as legitimate
    lift-boundary gap kinds.

Tests:
  * trinity_roundtrip_test: passes (gap kinds updated to accept the post-cut
    `kit-plugin-unavailable` shape).
  * cmd_bind_integration: 12 passing, 15 marked `#[ignore]` with explicit
    reason "requires <lang> realize kit; without it cmd_bind emits an honest
    kit-plugin-unavailable gap". Java tests pass when provekit-realize-java.jar
    is built.
  * slice2_java_realize_plugin_byte_identical: 13 passing (after Java jar
    built); the test now exercises the dispatcher contract directly via
    `realize_for_bind` which routes through `dispatch_realize` for Java.

Net diff: -2526 / +1765 lines.

The architectural principle (federation by construction; zero language-specific
code in implementations/rust/provekit-cli/) is now enforceable mechanically: the
single `match target_lang { TargetStyle::* }` site that previously embodied
violation is gone, and the dispatcher routes every language through the same
PEP 1.7.0 surface.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@chatgpt-codex-connector
Copy link
Copy Markdown

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.
To continue using code reviews, add credits to your account and enable them for code reviews in your settings.

@coderabbitai
Copy link
Copy Markdown

coderabbitai Bot commented May 13, 2026

Caution

Review failed

The pull request is closed.

ℹ️ Recent review info
⚙️ Run configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

Run ID: 6f9e39b0-395e-418e-b858-2351908cd3ff

📥 Commits

Reviewing files that changed from the base of the PR and between d9ea20c and ff77338.

📒 Files selected for processing (11)
  • .provekit/lift/rust-bind/manifest.toml
  • implementations/rust/provekit-cli/src/cmd_bind.rs
  • implementations/rust/provekit-cli/src/cmd_transport.rs
  • implementations/rust/provekit-cli/src/kit_dispatch.rs
  • implementations/rust/provekit-cli/src/lib.rs
  • implementations/rust/provekit-cli/src/main.rs
  • implementations/rust/provekit-cli/tests/cmd_bind_integration.rs
  • implementations/rust/provekit-cli/tests/slice2_java_realize_plugin_byte_identical.rs
  • implementations/rust/provekit-cli/tests/trinity_roundtrip_test.rs
  • implementations/rust/provekit-walk/src/bin/walk_rpc.rs
  • protocol/specs/2026-05-13-bind-ir-lift-result.md

Walkthrough

The PR refactors provekit bind from inline Rust AST parsing to a plugin-based architecture. A new kit_dispatch module discovers and invokes lift kits (returning per-function metadata) and realize kits (emitting target-language code). cmd_bind now dispatches lifts instead of scanning source; cmd_transport delegates realization to kits. walk_rpc implements the bind-lift JSON-RPC surface. A new manifest and protocol spec formalize the bind-lift-entry contract.

Changes

Plugin Dispatcher and Bind Pipeline Integration

Layer / File(s) Summary
Kit Dispatcher - Bind Lift Surface
implementations/rust/provekit-cli/src/kit_dispatch.rs (lines 1–415)
Introduces dispatch_bind_lift, BindLiftEntry, and BindLiftResult types. Resolves lift kit commands via .provekit/lift/*/manifest.toml, environment override, built-in candidates (provekit-walk-rpc, provekit-bind-lift-<lang>), and PATH probing. Spawns kit with --rpc, sends newline-delimited initialize/lift/shutdown JSON-RPC requests, validates responses, and decodes ir-document into entries and diagnostics.
Kit Dispatcher - Realize Surface
implementations/rust/provekit-cli/src/kit_dispatch.rs (lines 454–742)
Implements dispatch_realize with RealizeRequest and RealizedSource types. Resolves realize kit via .provekit/realize/<lang>/manifest.toml, environment, built-ins (including Java jar convention), and PATH. Invokes kit via provekit.plugin.invoke, parsing response to extract source, is_stub, and extension with language-based fallback convention.
Bind Command Plugin Integration
implementations/rust/provekit-cli/src/cmd_bind.rs
run() dispatches dispatch_bind_lift() instead of scanning Rust AST, writes gaps.json and exits early if kit unavailable or empty. BindingRecord extended with param_names, param_types, return_type. run_bind_engine accepts raw_lifts instead of src_files. Canonical rewrite rewrites to call realize_for_bind with stored signature fields instead of re-parsing. Language detection prefers detect_lift_language(), and local collect_rs_files helper removed. TermShape updated to represent lift-kit JSON values with cached CID.
Transport Realization Delegation
implementations/rust/provekit-cli/src/cmd_transport.rs
Calls dispatch_bind_lift for signature data instead of inline Rust parsing. realize_for_bind signature changed to accept param_types and return_type directly instead of source_text. realize_function constructs RealizeRequest and calls kit_dispatch::dispatch_realize instead of containing in-file target-language emission. Removed parse_rust_fn_types, lift_rust_contracts, and formula/annotation emission helpers.
Walk RPC Bind-Lift Implementation
implementations/rust/provekit-walk/src/bin/walk_rpc.rs
Extended JSON-RPC dispatcher to route initialize/lift/shutdown to bind-lift handlers. bind_lift scans workspace .rs files, parses with syn, extracts per-function contract attributes (including cfg_attr forms), concept annotations via // concept: comments, and generates canonical term-shape AST representation with blake3_512_of(encode_jcs(...)) CID. Added file collection, signature extraction, contract/concept parsing, and term-shape generation helpers for common control-flow and expression forms.
Module Wiring and Protocol Specification
implementations/rust/provekit-cli/src/lib.rs, implementations/rust/provekit-cli/src/main.rs, .provekit/lift/rust-bind/manifest.toml, protocol/specs/2026-05-13-bind-ir-lift-result.md
Added public kit_dispatch module in lib.rs and main.rs. Created .provekit/lift/rust-bind/manifest.toml specifying provekit-walk-rpc --rpc. Added protocol spec defining bind-lift-entry JSON shape (required fields, JCS canonicalization rules, term-shape fingerprinting, per-function gap vs. kit-plugin-unavailable semantics).
Test Adaptation for Plugin Architecture
implementations/rust/provekit-cli/tests/cmd_bind_integration.rs, implementations/rust/provekit-cli/tests/slice2_java_realize_plugin_byte_identical.rs, implementations/rust/provekit-cli/tests/trinity_roundtrip_test.rs
Skipped canonical emission and syntax-checker tests (pr770 markers) pending language realize kits. Refactored assert_byte_identical to normalize param/return types instead of extracting from source text. Expanded trinity_roundtrip_test to accept kit-plugin-unavailable, bind-lift-empty, and leg-3-not-reached gap kinds.

Sequence Diagram

sequenceDiagram
  participant CmdBind as cmd_bind::run
  participant Dispatcher as kit_dispatch
  participant LiftKit as Lift Kit<br/>(walk_rpc)
  participant Engine as bind_engine
  participant RealizeKit as Realize Kit<br/>(lang plugin)
  CmdBind->>Dispatcher: dispatch_bind_lift(workspace, lang)
  Dispatcher->>Dispatcher: resolve lift kit command<br/>(manifest/env/builtin/PATH)
  Dispatcher->>LiftKit: spawn with --rpc
  Dispatcher->>LiftKit: initialize, lift requests<br/>(JSON-RPC)
  LiftKit-->>Dispatcher: ir-document with<br/>bind-lift-entries
  Dispatcher-->>CmdBind: BindLiftResult<br/>(entries + diagnostics)
  CmdBind->>Engine: run_bind_engine(raw_lifts)
  Engine-->>CmdBind: EngineResult<br/>(BindingRecords)
  loop for each binding
    CmdBind->>Dispatcher: realize_for_bind<br/>(param_types, return_type)
    Dispatcher->>Dispatcher: resolve realize kit<br/>(manifest/env/builtin/PATH)
    Dispatcher->>RealizeKit: provekit.plugin.invoke<br/>request (JSON)
    RealizeKit-->>Dispatcher: source, is_stub,<br/>extension
    Dispatcher-->>CmdBind: RealizedSource
  end
Loading

Estimated code review effort

🎯 4 (Complex) | ⏱️ ~75 minutes

Possibly related issues

  • TSavo/provekit#760: Directly related refactor implementing the same plugin-based lift dispatch and removal of inline Rust AST parsing from cmd_transport/cmd_bind into kit_dispatch and walk_rpc lift surface.

Possibly related PRs

  • TSavo/provekit#225: Introduces a lift kit adapter (provekit-lift-openapi) with manifest.toml and --rpc support—a direct consumer of the new dispatch_bind_lift dispatcher introduced in this PR.
  • TSavo/provekit#761: Implements Java realize plugin with provekit.plugin.invoke RPC handling, directly complementing the PR's new realize dispatch through kit_dispatch::dispatch_realize.
  • TSavo/provekit#758: Introduces provekit-plugin-loader and plugin registry plumbing (PluginFlags in cmd_bind.rs), providing foundational infrastructure that the kit_dispatch dispatcher now builds upon.

Poem

🐰 A lift kit stands tall, a dispatcher calls,
No more parsing deep in Rust's hallowed halls!
Plugins now dance through JSON-RPC's delight,
From term-shape to realize, each piece shines bright.
The bind pipeline flies—no more code in sight! ✨

✨ Finishing Touches
📝 Generate docstrings
  • Create stacked PR
  • Commit on current branch
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch feat/770-kit-agnostic-dispatcher

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.

… jar

Post PR #779 the realize path dispatches through kit_dispatch, which
returns kit-plugin-unavailable when the Java jar isn't built. The CI
`make test-rust` target runs cargo test before `mvn package`, so all
12 trinity_*_byte_identical tests panicked on the dispatcher's clean
refusal.

The pep_describe_returns_valid_sugar_plugin test in the same file
already self-bootstraps via ensure_jar_built() (thread-safe OnceLock<
Mutex>-guarded one-shot Maven build). Extend the same pattern to the
trinity tests by calling ensure_jar_built() at the top of
assert_byte_identical.

13/13 byte-identical tests pass locally with the jar absent at start.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@TSavo TSavo merged commit 91c408d into main May 13, 2026
4 of 6 checks passed
@TSavo TSavo deleted the feat/770-kit-agnostic-dispatcher branch May 13, 2026 15:53
TSavo pushed a commit that referenced this pull request May 13, 2026
The Java side of bind's Verb 1 (Lift). New BindRpcServer.java exposes
JavaBindLifter over PEP 1.7.0 JSON-RPC on '--rpc'. JavaBindLifter walks
Java source via the javac compiler API and emits bind-lift-entry records
per protocol/specs/2026-05-13-bind-ir-lift-result.md: language-neutral
term_shape (body/if/while/for/exit/assign/let/rel/bin/call/opaque) plus
the concept_annotation pulled from '// concept: NAME' lines preceding
each method.

ProofIR is concept-language. The kit emits CONCEPTS via term_shape +
concept_annotation, not java:* surface ops. The asymmetric counterpart
that existed before was provekit-lift-java-source's legacy RpcServer,
which emitted function-contract IR for the realize side; that file is
deleted in this PR — no legacy support — and Program.java's '--rpc'
flag now dispatches straight to BindRpcServer.

Empirical: 'provekit bind --root <java-dir> --lang java
--target-language python' resolves the kit through PR #779's
kit_dispatch (.provekit/lift/java-bind/manifest.toml registered),
spawns the Java plugin, parses the bind-lift-entry stream, clusters
three test methods to concept:identity / concept:bool-cell /
concept:option with zero unnamed clusters.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo pushed a commit that referenced this pull request May 13, 2026
The Python side of bind's Verb 1 (Lift). Mirror of the Java bind-lift
kit shipped in PR #780. Walks Python source via the `ast` module and
emits bind-lift-entry records per
protocol/specs/2026-05-13-bind-ir-lift-result.md:

- Language-neutral term_shape (body/if/while/for/exit/assign/let/rel/
  bin/call/opaque) with JCS-stable serialization and BLAKE3-512 CIDs.
- concept_annotation from # concept: NAME lines preceding each function;
  UNNAMED-CONCEPT-* filter retained so anonymous clusters re-derive
  from shape_cid each run (self-naming flow).
- attr_pre / attr_post from # @requires: / # @ensures: comments.
- Signature metadata (param_names, param_types, return_type, fn_name,
  fn_line, file).

bind_rpc.py exposes it over PEP 1.7.0 JSON-RPC on the same `--rpc` flag.
Manifest at .provekit/lift/python-bind/manifest.toml registers the kit
with PR #779's kit_dispatch.

Empirical: wrap_identity term_shape_cid matches Java/Rust/C versions
byte-for-byte (blake3-512:e24e7d66...204b) — cross-language structural
equivalence operational across four kits.

14 unit tests pass in tests/test_bind_lifter.py.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo pushed a commit that referenced this pull request May 13, 2026
The C side of bind's Verb 1 (Lift). Mirror of PR #780 (Java) and #781
(Python). New `provekit-bind-lift-c` binary in
implementations/c/provekit-walk-c/ walks .c files via libclang and emits
bind-lift-entry records per protocol/specs/2026-05-13-bind-ir-lift-result.md.

- Language-neutral term_shape (body/if/while/for/exit/assign/let/rel/
  bin/call/opaque) with JCS-stable serialization.
- term_shape_cid via vendored BLAKE3-512.
- concept_annotation from // concept: NAME or /* concept: NAME */
  preceding the function; UNNAMED-CONCEPT-* filter retained for self-
  naming flow.
- attr_pre / attr_post from /* @requires(...) */ and /* @ensures(...) */
  block comments.
- Signature metadata via libclang type queries.

Manifest at .provekit/lift/c-bind/manifest.toml registers the kit with
PR #779's kit_dispatch.

Empirical: wrap_identity term_shape_cid matches Rust/Java/Python sibling
kits byte-for-byte (blake3-512:e24e7d66...204b) — cross-language
structural equivalence operational across all four kits.

Local test: make -C implementations/c/provekit-walk-c builds clean,
tests/bind_lift_rpc.sh exits 0.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo pushed a commit that referenced this pull request May 13, 2026
PR #779 made cmd_bind kit-agnostic via kit_dispatch; dispatch to non-Rust
bind-lift kits is real once a kit registers. But run_bind_engine still
unconditionally pushed two v0-capability-gap entries to every gaps.json:

  "multi-lang lift_plugin dispatch deferred to v1 (only Rust lifting in v0)"
  "real ConceptAbstractionMemento catalog lookup deferred to v1 ..."

Both claims are false post-#779. The first is contradicted by the Java
(PR #780), Python (PR #781), and C (PR #782) bind-lift kits actually
running through the dispatcher and producing real concept-shaped IR.
The second conflates a substrate choice (soft-match classification) with
a missing capability. Per Supra omnia rectum, gaps must reflect REAL
substrate state, not legacy carved-in-rock pessimism.

Honest replacements already exist and emit per-situation:
- kit-plugin-unavailable (dispatcher, when no kit registers)
- bind-stub-body-emitted (apply_canonical_rewrite, per concept)
- below-threshold (per concept under threshold)

This PR deletes the two unconditional gap pushes and flips the existing
integration test gaps_doc_records_v0_capability_gaps to assert the
ABSENCE of those stale kinds (renamed gaps_doc_reflects_real_substrate_state).

Empirical demo: `provekit bind --root <c-fixture> --lang c --target-language
java` now produces gaps.json containing only real per-concept entries,
not the legacy lie.

12/12 cmd_bind_integration tests pass.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo added a commit that referenced this pull request May 13, 2026
The Java side of bind's Verb 1 (Lift). New BindRpcServer.java exposes
JavaBindLifter over PEP 1.7.0 JSON-RPC on '--rpc'. JavaBindLifter walks
Java source via the javac compiler API and emits bind-lift-entry records
per protocol/specs/2026-05-13-bind-ir-lift-result.md: language-neutral
term_shape (body/if/while/for/exit/assign/let/rel/bin/call/opaque) plus
the concept_annotation pulled from '// concept: NAME' lines preceding
each method.

ProofIR is concept-language. The kit emits CONCEPTS via term_shape +
concept_annotation, not java:* surface ops. The asymmetric counterpart
that existed before was provekit-lift-java-source's legacy RpcServer,
which emitted function-contract IR for the realize side; that file is
deleted in this PR — no legacy support — and Program.java's '--rpc'
flag now dispatches straight to BindRpcServer.

Empirical: 'provekit bind --root <java-dir> --lang java
--target-language python' resolves the kit through PR #779's
kit_dispatch (.provekit/lift/java-bind/manifest.toml registered),
spawns the Java plugin, parses the bind-lift-entry stream, clusters
three test methods to concept:identity / concept:bool-cell /
concept:option with zero unnamed clusters.

Co-authored-by: Claude Code <agentwopr@gmail.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo added a commit that referenced this pull request May 13, 2026
The Python side of bind's Verb 1 (Lift). Mirror of the Java bind-lift
kit shipped in PR #780. Walks Python source via the `ast` module and
emits bind-lift-entry records per
protocol/specs/2026-05-13-bind-ir-lift-result.md:

- Language-neutral term_shape (body/if/while/for/exit/assign/let/rel/
  bin/call/opaque) with JCS-stable serialization and BLAKE3-512 CIDs.
- concept_annotation from # concept: NAME lines preceding each function;
  UNNAMED-CONCEPT-* filter retained so anonymous clusters re-derive
  from shape_cid each run (self-naming flow).
- attr_pre / attr_post from # @requires: / # @ensures: comments.
- Signature metadata (param_names, param_types, return_type, fn_name,
  fn_line, file).

bind_rpc.py exposes it over PEP 1.7.0 JSON-RPC on the same `--rpc` flag.
Manifest at .provekit/lift/python-bind/manifest.toml registers the kit
with PR #779's kit_dispatch.

Empirical: wrap_identity term_shape_cid matches Java/Rust/C versions
byte-for-byte (blake3-512:e24e7d66...204b) — cross-language structural
equivalence operational across four kits.

14 unit tests pass in tests/test_bind_lifter.py.

Co-authored-by: Claude Code <agentwopr@gmail.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo added a commit that referenced this pull request May 13, 2026
The C side of bind's Verb 1 (Lift). Mirror of PR #780 (Java) and #781
(Python). New `provekit-bind-lift-c` binary in
implementations/c/provekit-walk-c/ walks .c files via libclang and emits
bind-lift-entry records per protocol/specs/2026-05-13-bind-ir-lift-result.md.

- Language-neutral term_shape (body/if/while/for/exit/assign/let/rel/
  bin/call/opaque) with JCS-stable serialization.
- term_shape_cid via vendored BLAKE3-512.
- concept_annotation from // concept: NAME or /* concept: NAME */
  preceding the function; UNNAMED-CONCEPT-* filter retained for self-
  naming flow.
- attr_pre / attr_post from /* @requires(...) */ and /* @ensures(...) */
  block comments.
- Signature metadata via libclang type queries.

Manifest at .provekit/lift/c-bind/manifest.toml registers the kit with
PR #779's kit_dispatch.

Empirical: wrap_identity term_shape_cid matches Rust/Java/Python sibling
kits byte-for-byte (blake3-512:e24e7d66...204b) — cross-language
structural equivalence operational across all four kits.

Local test: make -C implementations/c/provekit-walk-c builds clean,
tests/bind_lift_rpc.sh exits 0.

Co-authored-by: Claude Code <agentwopr@gmail.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo added a commit that referenced this pull request May 13, 2026
PR #779 made cmd_bind kit-agnostic via kit_dispatch; dispatch to non-Rust
bind-lift kits is real once a kit registers. But run_bind_engine still
unconditionally pushed two v0-capability-gap entries to every gaps.json:

  "multi-lang lift_plugin dispatch deferred to v1 (only Rust lifting in v0)"
  "real ConceptAbstractionMemento catalog lookup deferred to v1 ..."

Both claims are false post-#779. The first is contradicted by the Java
(PR #780), Python (PR #781), and C (PR #782) bind-lift kits actually
running through the dispatcher and producing real concept-shaped IR.
The second conflates a substrate choice (soft-match classification) with
a missing capability. Per Supra omnia rectum, gaps must reflect REAL
substrate state, not legacy carved-in-rock pessimism.

Honest replacements already exist and emit per-situation:
- kit-plugin-unavailable (dispatcher, when no kit registers)
- bind-stub-body-emitted (apply_canonical_rewrite, per concept)
- below-threshold (per concept under threshold)

This PR deletes the two unconditional gap pushes and flips the existing
integration test gaps_doc_records_v0_capability_gaps to assert the
ABSENCE of those stale kinds (renamed gaps_doc_reflects_real_substrate_state).

Empirical demo: `provekit bind --root <c-fixture> --lang c --target-language
java` now produces gaps.json containing only real per-concept entries,
not the legacy lie.

12/12 cmd_bind_integration tests pass.

Co-authored-by: Claude Code <agentwopr@gmail.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo added a commit that referenced this pull request May 13, 2026
* fix(789): ship discoverable provekit-realize-python wrapper

PR #788 shipped the python realize package source but no executable
shim. The dispatcher's built-in discovery looks for
`implementations/python/target/release/provekit-realize-python`
(per the substrate convention mirroring Rust's target/release/ path).
Without the shim the dispatcher returns kit-plugin-unavailable even
when the package is on disk.

The shim is a 4-line bash wrapper that sets PYTHONPATH to the
package src and execs `python3 -m provekit_realize_python_core`.
No build step required; the kit is plain Python.

Empirical: with this in place,
`provekit bind --root <java-dir> --lang java --target-language python`
now lifts via the Java bind-lift kit and realizes via this Python
realize kit, producing real Python bodies (def wrap_identity(x):
return x, def toggle(flag): return not flag, etc.). Leg 2 of the
C→Java→Python→C trinity is now empirically demonstrable end-to-end.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* feat(790): c realize kit — native C, emits real free()

Replaces the closed #777 which wrote C realize in Rust (federation
violation per Sir). This kit is written in C, lives at
implementations/c/provekit-realize-c-core/, speaks PEP 1.7.0
provekit.plugin.invoke over stdio, and loads body templates + sugar
dict from menagerie/c-language-signature/specs/.

THE CONCEPT:FREE CASE — the canonical demonstration of native-surface
fidelity. Realization is plain free(${ptr}); loss_record_contribution
is empty. C's free IS the natural surface.

Empirical via the dispatcher:
- concept:identity -> return x;
- concept:free -> free(p);
- gaps.json empty

Pin tests now 6/6: java + python + c sugar/bodies all CID-pinned in
substrate_default_cids.rs.

This is the realize half of the trinity's leg 3 (Python -> C). Combined
with PR #779 (kit-agnostic dispatcher), #780-#788 (lift kits + realize
kits + the bind-IR plumbing), and #789 (Python realize discovery shim),
the full C -> Java -> Python -> C round-trip has all four kits operational.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Code <agentwopr@gmail.com>
Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
TSavo added a commit that referenced this pull request May 14, 2026
…859) (#861)

Closes the regression from commit 91c408d / PR #779 (kit-agnostic
dispatcher delete Rust special-case). PR 2 of #859 per the locked
execution plan; diagnosis at docs/incidents/2026-05-14-trinity-baseline-
diagnosis.md (PR #860, merged) identifies this as the first blocker.

## Root cause

PR #779 moved Rust Verb 1 lift from cmd_bind into kit_dispatch. The
dispatcher resolves manifests under <workspace_root>/.provekit/lift/...,
then sibling-binary, then PATH. The trinity harness passes the temp
fixture root as workspace_root, but the temp root only contains
src/lib.rs, not .provekit/lift/rust-bind/manifest.toml. Sibling-binary
discovery also failed in a fresh cargo target dir because cargo built
debug/provekit for the integration test but not debug/provekit-walk-rpc.

Net: dispatcher emitted kit-plugin-unavailable into gaps.json and
exited success, but downstream assertion "Leg 1 must produce
translated/java/ dir" still fired.

## Fix

Test-only. No substrate code changed.

In trinity_roundtrip_test.rs the harness now:

1. Builds provekit-walk-rpc into the same target dir as the tested
   provekit binary (option c from diagnosis §7)
2. Writes a temp-fixture .provekit/lift/rust-bind/manifest.toml pointing
   at that built binary (not at the repo-root debug/provekit-walk-rpc,
   which would reintroduce target-dir state dependence)

This makes the test hermetic: it passes the same way in a fresh
CARGO_TARGET_DIR as in a warm one. No ambient build state leaks in.

## Acceptance gate (passes both ways)

Fresh CARGO_TARGET_DIR:

  CARGO_TARGET_DIR=$(mktemp -d /private/tmp/pk-trinity-fresh-XXXXXX) \
    cargo test --manifest-path implementations/rust/Cargo.toml \
    -p provekit-cli --test trinity_roundtrip_test -- --nocapture

  test result: ok. 1 passed; 0 failed; finished in 5.74s

Warm target dir:

  cargo test --manifest-path implementations/rust/Cargo.toml \
    -p provekit-cli --test trinity_roundtrip_test -- --nocapture

  test result: ok. 1 passed; 0 failed; finished in 2.94s

Output reports: "trinity_round_trip: v0 loudly-bounded-lossy outcome
(14 loss entries; Branch 2 per-line characterization gated until real
lifters land)" - the existing v0 lossy semantics. Branch 2 byte-identity
remains future work (PR 3 territory: Rust realize kit + body templates).

## Not in scope

- C realizer parseability (PR 4 of #859)
- Rust realize kit + rust-canonical-bodies.json (PR 3 of #859)
- HTTP trinity (Bridge D, paused)
- v0 lossy semantics / overclaim wording cleanup (separate docs PR)

If the substrate consumer chooses to gate on byte-identity rather than
loudly-bounded-lossy, those PRs are needed. This PR delivers a
hermetic, fresh-target-dir-passing baseline for the existing v0 test.

## Pre-existing formatting drift surfaced (not fixed)

cargo fmt --check on the provekit-cli manifest reports unrelated
formatting drift in cmd_bind.rs, cmd_transport.rs, kit_dispatch.rs.
Direct rustfmt --check on the touched test file passes. The pre-existing
drift is not caused by this PR and is not in scope.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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