Repository navigation
Wire emit_host_run_transport builtin and implement host process execution - #6359
Merged
Merged
Conversation
…0 slice) The fail-closed run_host_process stub becomes a real typed-argv host tap: - v1_interpreter.rs gains the emit_host_run_transport builtin (wet-only; hermetic mode refuses -- no mock arm): materialize workspace files under a temp workspace (path-escape refused), run the build argvs then the run argv via std::process::Command (typed argv, no shell), return exit/stdout/stderr octets + build log as data. - 04_method.dag + generated v1_compiler_infer_method.rs register the builtin name (in-sync pair, the #6270 backfill pattern). - emit_host.dag folds HostTransportDescriptor -> builtin call -> typed EmitHostRunReceipt; unknown host tool is a typed refusal; the not-wired diagnostic is deleted (wire-or-delete). - rust.dag MVP1 descriptor gains the runnable workspace its codec always implied: Cargo.toml (FixedText) + main harness (EmittedWithSuffix, prints add(2,3) as the 5-byte codec value) + --quiet flags. - rung_3_4_common fixture repaired: per-node-coherent InferredFacts (grounding.node == queried node, structured algebra evidence) and the real rust_mvp1_target_model_staging() instead of a hollow TargetModel. Receipts (local, wet): - NEW emit_host_transport_wire_test.dag: green run (stdout == [0,5,0,0,0], runtime_value_parse Accepted) + 2 REDs (nonzero exit -> logical_run Rejected; 4-byte stdout -> codec width Rejected): gunbc run --claim-run emit_host_transport_wire_all_holds -> true. - rust_add_emit_add_fn_accepts_holds -> true (emit side unchanged). - rung3 roundtrip -> Pass (unchanged); rung4 emit-vs-eval -> Fail at the pre-existing target_use_site_ownership_lookup_miss (unchanged; the claim subject has never had a translate-accepted shape). Phase pin stays ModelAndWitnessOnly: the kernel-D flip criterion is the rung-4 EqualsClaim green-not-Deferred, which now waits only on the emit side accepting a shared subject, not on transport. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018qZSaWfysRfg28bNVS7ueX
…d; flip kernel-D pin
Completes the kernel-D flip criterion (doc §4: run_test_claim_emit_vs_eval
GREEN on a rust EqualsClaim, no Deferred). A dedicated end-to-end witness
now composes the full pure-eval-emit path and passes by structural equality,
not fabrication:
eval(add-subgraph, octet-interpretation) -> RuntimePrimitive{P, octets(5)}
emit(add-fn) -> cargo build -> cargo run -> stdout 5 bytes
runtime_value_parse(stdout) -> RuntimePrimitive{P, octets(5)}
runtime_value_eq (==) -> Pass
The two sides meet only because they share the host row's primitive_type
node P (rust_emit_host_runtime_primitive_type_node) AND the octet byte
encoding (emit_host_octets_byte_string) — reconciling the value-representation
fork that made the pre-existing nat_semiring rung-4 subject uncomparable.
New witness (src/v2/test/claim/manual/emit_host_add_equals_eval_test.dag):
- GREEN: emit_host_add_equals_eval_holds (Pass).
- RED control: emit_host_add_wrong_oracle_refuses_holds — a wrong eval oracle
(returns 6) must NOT Pass, proving the comparison discriminates rather than
always-greening.
- one subject.tree serves both stages: emit walks tree.root (the rust add-fn,
real rust grounding facts); eval walks claim.rhs (the computation subgraph,
generic coherent facts) via a composed facts lookup (rust-detail then
generic fallback whose algebra == P to satisfy eval's resolved_type check).
Interpreter fix (v1_interpreter.rs): emit_host_run_transport now flattens
rope-shaped strings (free_monoid_to_string) for workspace path/text and argv
elements — emit(...).carried materializes as a FreeMonoid Cons-chain, not a
flat Value::Str, so the earlier expect_str rejected it (the transport wire
test passed only because it fed a String literal).
Phase pin: interpreter_kernel_d_current_phase ModelAndWitnessOnly ->
PureEvalEmitWired (transport is wired and proven), with a new
interpreter_kernel_d_phase_is_pure_eval_emit_wired predicate; the kernel-D
witness updated to assert the advanced phase.
Receipts (local, wet):
- emit_host_add_equals_eval_all_holds -> true (green + wrong-oracle RED)
- emit_host_transport_wire_all_holds -> true (unchanged)
- interpreter_kernel_model_witnesses -> true (phase now PureEvalEmitWired)
Not claimed: the nat_semiring rung-4 subject still Fails at translate's
target_use_site_ownership_lookup_miss — that is a translate limitation for
law-shaped subjects, a separate open item, not an emit_host/transport gap.
The kernel-D criterion is met by the dedicated witness above.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018qZSaWfysRfg28bNVS7ueX
…gy-discussion-313pvj
Multi-line format! wrapping to satisfy cargo fmt --check on the HAND interpreter file. Fixes the rust_tests fmt-diff failure on #6359. The ci_regen failure was pre-existing divergence on the stale base (pre-#6357 seed convergence), resolved by merging origin/main; regen --verify now reports regen_divergence_count=0 and the generated v1_compiler_infer_method.rs (carrying the emit_host_run_transport row) is byte-identical to a fresh self-compile. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018qZSaWfysRfg28bNVS7ueX
…d v2 parsing its own closure
Two additive wave1-grammar extensions so v2's parser accepts constructs its
own compiler source already uses (verified by interpreted execution; no Rust
rebuild — grammar is .dag, read at interpret time):
- `?` optional type sugar: `^dag_token_question` lexer rule + trailing
`optional(?)` on `qualified_type_expr`. `Int?`, `Outcome<Symbol?>` parse
CLEAN; `Optional<T>` is the emit-ready lowering target (v2 Node has no
cardinality field — Cardinality connective already has translate support).
Stash-verified additive: the deeper rejects it unmasks pre-date this change.
- keyword-as-name: `dag_grammar_binding_name_terminal` = ident | any wave1
keyword, wired into `field_decl` + `typed_param` name positions. v2 source
already uses `module:`/`loop:`/`match:` as field/param names (11+2+2 sites
across 5 closure files); the grammar just didn't accept existing valid code.
Name positions are type-context (name `:` type), so keyword tokens there
carry no expression-parse ambiguity — grammar validates clean, disjoint
FIRST sets.
Receipts (interpreted, inline via grammar_coverage_ingest):
- Int? / Outcome<Symbol?> / nested generics / `type X = A|B` → CLEAN
- `type Scope = ScopeRoot { module: Namespace } | ScopeFrame { locals: Map<Symbol, Symbol>, outer: Scope }` (the 03_resolve blocker) → CLEAN
- keyword field/param names (module/loop) → CLEAN
- regression: plain record type / coproduct / fn-with-params → CLEAN
S1 is not complete: full 74-file closure parse still iterating (masked layers
surface as each tokenize/parse gap clears). s1_closure_parse_probe.dag is the
closure receipt harness; s1_opt_probe.dag is the inline bisect tool.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018qZSaWfysRfg28bNVS7ueX
…gy-discussion-313pvj
…arse cost Startup (load+compile probe closure interpreted) measured at 3s via s1_noop; so the ~5min/file S1 cycle is the interpreted parse itself, not startup. Manual diagnostic harness (test/claim/manual, non-CI).
The `compile` command took all `.dag` files in the first --source-root as entries, so `--source-root src/v2 --source-root dag` compiled the whole 1867-module tree — reconcile-OOM before emit (the missing scoped-compile mode #6362 flagged). `--entry <file>` makes exactly that one module the entry; its transitive imports resolve from the full index as before, so a small closure emits without a whole-tree pass. Mirrors `run --entry`. Receipt (local): `gunbc compile --source-root src/v2 --source-root dag --entry src/v2/test/claim/manual/s1_opt_probe.dag --target rust` indexes 1873 modules, resolves 61 (transitive closure), emits 66 files in 10s, no OOM — vs whole-tree OOM at ~67s. HAND file (main.rs); regen unaffected (not in the GENERATED roster). fmt + clippy -D warnings clean. Unlocks compiled-parse iteration for S1 (v2 parser emitted native and run in ~ms, vs ~278s/file interpreted) and scoped emit-on-demand generally. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018qZSaWfysRfg28bNVS7ueX
…robes s1_parse_harness.dag calls tokenize -> parse_module -> normalize directly (no grammar_coverage wrapper), so `compile --entry` emits its closure with 0 compiler diagnostics — the minimal entry for probing v2-parser emit health. Receipt (local, via compile --entry): the v2 parse closure resolves to 41 sources, emits 45 Rust files in 8s. But the emitted Rust is NOT cargo-green: 4259 rustc errors, 84% (3567) a single E0308 type-mismatch class — the same shape as the v1 seed's fresh-emit (1667 -> ~2 emitter root causes). So a runnable compiled parser is blocked on emitter restoration for v2 code (the S2 self-emit lane), not on scoping. `compile --entry` (prior commit) makes this emit-health measurable cheaply; the near-term S1 iteration unlock stays the interpreted-parse fix (list_snoc_item O(n^2) accumulation), owned in the parse-perf lane. Removes s1_opt_probe.dag / s1_closure_parse_probe.dag (bisect scratch with hardcoded temp paths). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018qZSaWfysRfg28bNVS7ueX
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Jul 9, 2026
…urfaced by frontier) #6359 deleted rung34_emit_host_target_bundle from rung_3_4_common (folding it into rung34_emit_host_rust_target_model = rust_target_model_staging()) but left rung_5_6_common importing the now-deleted symbol. Compile-clean never resolved this fixture (not in the entry closure); the affected-set frontier does once rung_3_4_common is touched. Project the bundle from the TargetModel that replaced it (TargetModel.bundle: Node), which rung_5_6_common already imports. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jul 9, 2026
* WIP: remove all occurences of program names (i.e. mvp1) from the repo * Reword milestone-referencing labels and doc/bin refs (mvp nickname removal) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Reconcile mvp-nickname rename with merged main additions (rust emit/signature work) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: remove all occurences of program names (i.e. mvp1) from the repo * rustfmt: format the rename-destination test Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Fix dangling import in rung_5_6_common (pre-existing #6359 breakage surfaced by frontier) #6359 deleted rung34_emit_host_target_bundle from rung_3_4_common (folding it into rung34_emit_host_rust_target_model = rust_target_model_staging()) but left rung_5_6_common importing the now-deleted symbol. Compile-clean never resolved this fixture (not in the entry closure); the affected-set frontier does once rung_3_4_common is touched. Project the bundle from the TargetModel that replaced it (TargetModel.bundle: Node), which rung_5_6_common already imports. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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
2 participants
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.
Summary
Implements the
emit_host_run_transportbuiltin to execute host processes in a materialized workspace, bridging the v1 interpreter with v2's host transport layer (the kernel-D "emit_host transport wiring" residue). This is the first time v2-lane emitted code executes natively on the host through theemit_hostpipeline — previouslyrun_host_processwas a fail-closed stub and every emit-vs-eval claim landedDeferred.Key changes
v1_interpreter.rs, HAND):eval_emit_host_run_transport_builtin— wet-mode only (hermetic mode refuses with a typed error, no mock arm); materializes{path, text}workspace files into a temp workspace with path-escape refusal; runs build argvs then the run argv viastd::process::Command(typed argv, no shell, per the bash-minimization rule); returns exit/stdout-octets/stderr-octets/build-log as data.04_method.dag+ generatedv1_compiler_infer_method.rsas an in-sync pair (the pipeline.rs cluster: transport_emit rest+shell (16 tests) — triage migrate vs delete #6270 backfill pattern — flagged for the next regen cutover sweep).emit_host.dag:run_host_processfoldsHostTransportDescriptor→ builtin call → typedEmitHostRunReceipt; unknown host tool is a typed refusal; theemit_host_transport_not_wireddiagnostic is deleted (wire-or-delete). Octets ground intoByteString(Byte { bits }) LSB-first.rust.dagMVP1 descriptor gains the runnable workspace its codec always implied:Cargo.toml(FixedText) + main harness (EmittedWithSuffix, printsadd(2, 3)as the 5-byte codec value: tag0+ LE i32) +--quietflags. TheEmittedWithSuffixvariant existed for exactly this and was never populated (the TS MVP1 fixture uses the same prefix+suffix pattern).rung_3_4_common.dagfixture repair: the facts map returned canned facts whosegrounding.nodecould never equal the queried node (infer_canonical_grounding_incoherent— the lane rotted while unenrolled), and the target model was a hollow hand-rolledTargetModel(translate_target_bundle_malformed). Now: per-node-coherentInferredFacts(grounding.node == queried node, structured algebra evidence) and the realrust_mvp1_target_model_staging().Receipts (local, wet —
gunbc run --source-root src/v2 --source-root dag)emit_host_transport_wire_test.dag,--claim-run emit_host_transport_wire_all_holds→ true:cargo build --quiet→cargo run --quiet→ stdout== [0,5,0,0,0]→runtime_value_parseAcceptedstd::process::exit(3)→logical_runRejected (typed, not silent)FixedWidthBytes{width: 5}→ parse Rejected (byte_width_mismatch)rust_add_emit_add_fn_accepts_holds→ true (emit side unchanged)target_use_site_ownership_lookup_miss(unchanged by this PR — see below)cargo build --release -p v1-compiler→ greenHonest residue (deliberately NOT claimed by this PR)
ModelAndWitnessOnly. The plan's flip criterion is the rung-4EqualsClaimgreen-not-Deferred. Transport is no longer the blocker, but the emit side still rejects the law-shaped claim subject (target_use_site_ownership_lookup_missin06_translate) — the lane's two ends (eval's subject, translate's subject) have never shared a single green subject. That subject-unification is the remaining S0 residue, tracked separately.rust_mvp1_source_textthrough the descriptor;emit()producing that exact literal is proven by the separately-green translate test. Full one-subject composition arrives with the residue above.Test plan
./target/release/gunbc run --source-root src/v2 --source-root dag --entry src/v2/test/claim/manual/emit_host_transport_wire_test.dag --claim-run --function emit_host_transport_wire_all_holds→truerust_add_emit_add_fn_accepts_holds→true;run_nat_semiring_rung34_eval→ rung3 Pass / rung4 pre-existing Fail unchanged🤖 Generated with Claude Code
https://claude.ai/code/session_018qZSaWfysRfg28bNVS7ueX