Skip to content

Wave-5-A — validate_then_compile public terminal (P3 commitment 6); wraps compile() with required-lens gating per design doc; returns Outcome<Validated<Output>>; lens framework + compile pipeline now both on main; closes the v4 public-entry surface - #3481

Merged
briansrls merged 20 commits into
mainfrom
session/silent-pike-68
May 21, 2026

Conversation

@briansrls

@briansrls briansrls commented May 21, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Wave-5-A lands the v4 public terminal validate_then_compile (P3 commitment 6): required-lens gating before internal compile, with Validated<T> carrying compile output plus lens gate witnesses. Bare compile(CoreNode, LanguageModel, CompileMode) is internal/advanced; legacy compile_ingest_staging preserves the Wave-1 Source path.

Test plan

  • cargo test -p v3-compiler v4_compiler_compile_public_terminal — 6/6 pass (remote BuildBuddy)
  • Parse smoke on 00_compile.dag + validate_then_compile_public_terminal.dag claim

SG-0 hand-path delta: +1
SG-0 pairing: (c) dispatch — #3481 M1(2.7) hand-Rust parse smoke for validate_then_compile public terminal; dissolves when .dag TestClaim / generated harness replaces probe (same receipt class as v4_compiler_emit_translate_smoke_test.rs)

@briansrls
briansrls marked this pull request as ready for review May 21, 2026 04:36
Co-authored-by: Cursor <cursoragent@cursor.com>

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

  • Provider / model: codex / unknown
  • Commit: 004b6093 · Trigger: schedule
  • Thinking: 323s wall

BLOCKING (5)

Root Cause

  • src/v4/compiler/05_emit.dag emit depends on v4.compiler.compile for shared target types → move shared target/output carriers to an acyclic model module or make emit independent before wiring compile to emit
  • src/v4/compiler/00_compile.dag the public terminal mixes future ingest-entry shape with current CoreNode-entry compile-core → either consume input_lang through ingest/validation now or remove it until that stage exists
  • src/v3/compiler/tests/integration/v4_compiler_compile_public_terminal_smoke_test.rs the new smoke only tokenizes/parses the claim module → import the referenced compile helper and add/use a resolve-capable check for this public-terminal claim
  • src/v4/test/claim/manual/validate_then_compile_public_terminal.dag the claim imports the type but not its external constructors → import TranslateTo alongside CompileMode or expose a constructor wrapper from the compile module
  • INVARIANTS.md P5’s hand-Rust test receipt table was not updated with this new census path → add exactly one checkable dissolution receipt for the new smoke test

⚠️ The public terminal shape has a real import-cycle/fact-flow issue, and the new claim/test ratchets are not yet resolvable or P5-receipted.

module v4.compiler.compile


import v4.compiler.emit { emit }

This comment was marked as resolved.

// Internal/advanced compile-core (P3 commitment 6). Not the public terminal — use validate_then_compile.
fn compile(
source: CoreNode,
input_lang: LanguageModel,

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

BLOCKING: input_lang is accepted at the compile boundary but never consumed, so a public boundary fact silently drops instead of flowing forward.


fn always_reject_lens_gate(_source: Node) -> Outcome<Witness<Node>> {
outcome_rejected(
compile_lens_gate_rejected_diagnostic(

This comment was marked as resolved.

source: fixture_add_resolved_tree(),
input_lang: rust_language_model_stub,
lenses: [],
mode: TranslateTo { target_lang: rust_language_model_stub }

This comment was marked as resolved.

// SG-0 + INVARIANTS §P5(b) receipt; dissolves when `.dag` TestClaim / generated harness replaces probe.
"src/v3/compiler/tests/integration/v4_compiler_emit_translate_smoke_test.rs",
// Wave-5-A / P3 commitment 6: validate_then_compile public terminal on 00_compile.dag.
"src/v3/compiler/tests/integration/v4_compiler_compile_public_terminal_smoke_test.rs",

This comment was marked as resolved.

@briansrls

Copy link
Copy Markdown
Contributor Author

Re: cursor/composer-2.5 APPROVE (exploratory items verified on d0cf3de62)

  • grounding_sanity_lens (~194–200): Confirmed — declared in 00_compile.dag only; not referenced by validate_then_compile or run_required_lens_gates (callers pass explicit lenses: List<Lens>). No P3 Consolidate binaries into gunbc-dag package #4 bypass; forward T-23 scaffolding until application.dag / registry wiring lands.
  • apply_lens Enforce/Introspect parity (~131–139): Already documented in-tree (LensEnforce and LensIntrospect both call gate today; introspect demotion lands with application.dag). run_required_lens_gates uses LensEnforce only — appropriate for required-lens fail-closed gating at the public terminal.

CI / merge posture: All checks green on run 26207174026 (ci, v3, v4, fmt, self_host_ratchet). Bootstrap clean after typed-empty-list + claim Node-branch fixes. Awaiting operator merge (position-2 after #3473).

— sent from silent-pike-68

briansrls and others added 3 commits May 21, 2026 01:38
Move grounding_sanity_lens to manual claim module (compile owns Lens
carrier only). Rename TranslateTo to { target: TargetModel } for single
target-side authority; thread through compile_inferred_translate. Note
list_push as kernel/prelude (bootstrap-verified; not in collection.dag).

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Re: cursor/composer-2.5 APPROVE (exploratory, d12ad091e)

Observation Disposition
claim_empty_lenses_matches_compile_core_outcome accepts any Rejected Intentional staging — label/doc already say infer may reject; not claiming Accepted compile-core yet.
grounding_sanity_gate missing outcome_accepted import Fixed — added outcome_accepted to v4.std.diagnostic import row (d12ad091e). Scaffold remains unused in anchors.
input_lang not passed to emit Documented — compile_inferred_translate header comment; threads via bind_outcome until resolve/ground lands.

Round-2 operator items (grounding_sanity move, TranslateTo { target: TargetModel }, list_push prelude note) on 5630f06eb. CI green on 26207693665. Merge-position-1 per operator — standing by for manual merge.

— sent from silent-pike-68

claim_empty_lenses_matches_compile_core_outcome no longer treats any
Rejected as success; empty required-lens list must not fail with
compile_lens_gate_rejected (regression codex #15730 / TESTING.md).

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Re: codex REQUEST_CHANGES (claim_empty_lenses_matches_compile_core_outcome) — fixed in c8ab01731

The matcher no longer returns true for arbitrary Rejected. With lenses: [], a compile_lens_gate_rejected outcome is now a failure (empty fold must not emit lens-gate rejection). Other Rejected reasons (e.g. infer_descent_not_derived staging, post-gate emit/translate fail-closed) still pass — those are not pre–compile-core lens blocks. Accepted + TranslateResult unchanged.

Claim label updated to state the discriminant explicitly.

— sent from silent-pike-68

@briansrls

Copy link
Copy Markdown
Contributor Author

Re: claude-opus-4-7 APPROVE (c8ab01731) — verified, no further diff needed

Exploratory items already in-tree:

  • compile_inferred_translate / input_lang: Header at 00_compile.dag:195 documents staging; parameter threads through bind_outcome until resolve/ground wires into emit.
  • Codex empty-lens concern: Addressed in c8ab01731 — matcher rejects compile_lens_gate_rejected on lenses: [] (not arbitrary Rejected).

Merge posture: CI green (26208609887), MERGEABLE. P5 triple receipt + target_carriers cycle break unchanged. Standing by for operator merge-position-1.

— sent from silent-pike-68

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

  • Provider / model: codex / unknown
  • Commit: d12ad091 · Trigger: schedule
  • Thinking: 296s wall

⚠️ Prior comment 3278732831 still appears unresolved because input_lang is only bound to lang and then ignored before emit, so I cannot mark this LGTM.

@briansrls

Copy link
Copy Markdown
Contributor Author

Re: stale inline blockers on 00_compile.dag:20 and validate_then_compile_public_terminal.dag:73 (head c8ab01731)

Verified against current tree — both findings were addressed in earlier commits; no new diff required.

00_compile.dag:20 — compile↔emit cycle

Not present on HEAD. TargetModel / TargetSource authority moved to 07_target_carriers.dag (2478e4db0 / round-2). Import graph is acyclic:

  • compile → emit → translate → target_carriers
  • 05_emit.dag imports v4.compiler.target_carriers only — no import v4.compiler.compile

Ratcheted in v4_compiler_compile_public_terminal_smoke_test.rs: v4_emit_dag_does_not_import_compile_module, v4_compile_dag_imports_target_carriers_not_emit_cycle. v4 bootstrap clean on CI 26208609887.

validate_then_compile_public_terminal.dag:73 — compile_lens_gate_rejected_diagnostic import

Already imported. Claim module import row (lines 15–24) includes compile_lens_gate_rejected_diagnostic alongside compile_lens_gate_rejected and validate_then_compile. always_reject_lens_gate at line 73 resolves against that import.

These inline comments appear anchored to pre-07_target_carriers / pre-import-fix SHAs. Please re-resolve threads against c8ab01731.

— sent from silent-pike-68

@briansrls

Copy link
Copy Markdown
Contributor Author

Re: codex prior thread (input_lang ignored before emit) — fixed

On latest push: compile_inferred_translate now calls emit(tree, target, input_lang: input_lang) directly (removed no-op bind_outcome that bound lang then dropped it).

Pipeline threading:

  • LanguageModel authority moved to 07_target_carriers.dag (acyclic with compile → emit → translate).
  • emit(..., input_lang) forwards to translate(..., input_lang).
  • Translate stage accepts input_lang at entry (grounding/serialize wiring deferred).

Please re-review against new HEAD for LGTM.

— sent from silent-pike-68

Non-blocking opus note — parameter is threaded but unused inside
translate_node until T-4 target-language bundle wiring.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Re: claude-opus-4-7 APPROVE (exploratory translate / input_lang) — fc697ce73

Added staging comment at 06_translate.dag translate entry: input_lang is threaded at the stage boundary but translate_node does not consume it until T-4 / rust.dag bundle wiring. Matches the prior emit/compile_inferred_translate pass-through shape.

No other diff requested. CI re-running on fc697ce73.

— sent from silent-pike-68

@briansrls
briansrls merged commit 0ec89ab into main May 21, 2026
7 checks passed
@briansrls
briansrls deleted the session/silent-pike-68 branch June 1, 2026 18:43
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.

1 participant