diff --git a/dag/gunbc/ci_layer_roots.dag b/dag/gunbc/ci_layer_roots.dag index 9aa4cf8a8c0..71b783a9bcf 100644 --- a/dag/gunbc/ci_layer_roots.dag +++ b/dag/gunbc/ci_layer_roots.dag @@ -980,6 +980,12 @@ type SubstrateLongLaneRow { data falsifier_substrate_long_lane_note: String = "Nightly falsifier batch 6 (test-decomposition Class C, 2026-07-25): the declared Hermetic lane for SubstrateInputsOnly ingest/parse pipeline witnesses whose own eval exceeds the per-PR 5s fast-lane budget (gunbc_ci_fast_lane_rule_note) but are not wet integration — the live-grain half of the provenance-producer Class C split (fixture fail-closed walls stay per-PR via hand-built rows in affected_set_provenance_producer_test.dag and sg_claims_test.dag selectivity receipts). Runs SelectionApplied after the rehomed-bin-wet batch; claim_executor halts this batch if an earlier one fails (fail-closed). Local recipe until enrolled: claim_batch --source-root dag --source-root src/v2 --entry --functions ." data falsifier_substrate_long_lane_rows: List = [ + SubstrateLongLaneRow { + entry: "src/v2/test/claim/long/direct_rust_door_observation_test.dag", + function: "direct_rust_door_observation_is_candidate_rejected", + reason: "12.7-15.1s measured eval per witness (wise-ram-22, 2026-08-04, four runs at --eval-budget-ms 900000): observe_direct_rust_door_provenance runs the real ingest-assemble-infer-mint path. The cost is fixture-shaped pipeline depth, not corpus breadth — the cost partition attributes ~79 percent to load_bare_edge_index, a corpus-wide index memoized per MultiEntryIndex that a single-entry harness pays in full and that amortizes across a real batch, so the witness's own work is roughly the 5s typecheck plus eval remainder", + dissolve_on: "eval lands under gunbc_ci_fast_lane_witness_eval_budget on a measured run and re-enrolls per-PR discovery — or this witness becomes stale because DirectRustDoorSourceProduced becomes reachable (containment lane PR D) - it asserts a CURRENT state, so it must be deleted or re-aimed in the change that fixes the source path, not left asserting a false negative; or the witness-evidence-lifecycle program lands per-witness declared execution requirements and route derives from those rather than from this file's directory (docs/plans/witness-evidence-lifecycle-design.md), at which point this row and the test/claim/long dir grain dissolve together" + }, SubstrateLongLaneRow { entry: "src/v2/test/claim/long/wave1_gate1_d_mvp_subsumption_witness_test.dag", function: "wave1_gate1_d_census_subsumption_witness_holds", diff --git a/dag/gunbc/doc_graph_roots.dag b/dag/gunbc/doc_graph_roots.dag index 69fc0aca5a6..9e2285fdcd5 100644 --- a/dag/gunbc/doc_graph_roots.dag +++ b/dag/gunbc/doc_graph_roots.dag @@ -107,6 +107,17 @@ fn hand_authored_doc_path(b: HandAuthoredDocBind) -> String { } data hand_authored_doc_binds: List = [ + HandAuthoredDocBind { + home: PlanDoc, + slug: "witness-evidence-lifecycle-design", + primary_work: DeclarationRef { module_path: "v2.workflow.floor_discovery_producer", decl_name: "floor_discovery_process_dag_file", field: WholeDeclaration }, + additional_works: [ + DeclarationRef { module_path: "gunbc.ci_layer_roots", decl_name: "long_lane_exclusion_note", field: WholeDeclaration }, + DeclarationRef { module_path: "gunbc.explicit_witness_admission", decl_name: "known_red_class_note", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.workflow.ci_floor_plan", decl_name: "falsifier_known_red_probe_batch_note", field: WholeDeclaration }, + ], + dissolution: HasTrigger { text: "steps 3-5 land or are honestly retired (steps 1-2 are done: the modeling decision was signed by the operator 2026-08-04 and the typed direct-rust-door observation executes green). Remaining: census-before-routing in floor_discovery_process_dag_file, the attempt/evidence algebra retiring QuarantineProbeExpectRed and batch-wide expect_red inversion, and route derived from execution requirement — with test/claim/long DELETED as the terminal state per the operator step-5 ruling (it may persist as migration scaffolding meanwhile, but no new semantic dependence may be added to it, and operator visibility comes from a generated long-route projection rather than the directory name). Then the surviving policy rows migrate to DESIGN or a registered gunbc.plan.Plan row and this bind deletes with the doc." }, + }, HandAuthoredDocBind { home: PlanDoc, slug: "candidate-scoped-gates-atomic-landing", diff --git a/docs/plans/witness-evidence-lifecycle-design.md b/docs/plans/witness-evidence-lifecycle-design.md new file mode 100644 index 00000000000..9b01ba97b3b --- /dev/null +++ b/docs/plans/witness-evidence-lifecycle-design.md @@ -0,0 +1,407 @@ +# Witness evidence lifecycle — route is a projection, evidence is the lifecycle + +**Status: MODELING DECISION SIGNED (operator, 2026-08-04). Steps 3-5 remain ungated +implementation work.** Step 2 (the typed direct-rust-door observation) ships in the same +PR as this note and is already implemented; the earlier "no implementation follows until +signed" line is retired as inaccurate. + +The sign, as issued: + +> Witness identity and expectation are declarations; complexity/resource requirements are +> declared or structurally derived; route is a projection; attempt termination and +> runner-scoped cost are observations; semantic evidence is the pending/current lifecycle; +> lane budget is scheduler policy. Census precedes routing. `Interrupted`, including +> `BudgetExceeded`, is not a verdict and satisfies no expectation. A timeout yields only a +> runner-bound cost lower bound and preserves the semantic obligation. Expectation +> matching is function-grain and pointwise, never batch-wide. + +## The incident that priced this + +Four witnesses introduced by gunbc#7683 (Lane B, direct v2 Rust door) are red on the +nightly falsifier. The falsifier is not reporting a regression. It is reporting the first +completed execution any of them has ever had. + +At the intermediate PR revision `c80605a`, all four terminated at the 5-second fast-lane +wall: + +``` +witness_direct_rust_door_provenanced_artifact_holds ... runtime error: eval budget +exceeded: 5002ms elapsed > 5000ms fast-lane budget (operator 5s rule 2026-07-12: a +witness this slow lives in a long/ test dir and runs via its dedicated lane, not per-PR +discovery) +``` + +The runner recorded `EvalBudgetExceeded`, prescribed relocation into `test/claim/long/`, +and never observed a returned Boolean. The witnesses were moved. The final revision +`79e5106` passed, because `test/claim/long/` is excluded from discovery. The pending +semantic obligation did not travel with the files; it ceased to exist. + +``` +semantic obligation is pending + -> fast attempt produces cost evidence but no semantic evidence + -> diagnostic prescribes a route change + -> route change removes the witness from the only enumerated population + -> pending semantic obligation disappears +``` + +The author did what the compiler instructed. At no point did the system represent +"this is slow AND its verdict is unknown"; it represented only "this is slow, move it", +and moving it discharged the only obligation the model carried. + +## Three coupled defects + +1. **State-space** — timeout and semantic failure share one red surface. +2. **Lifecycle** — a route transition does not carry the pending-verdict obligation forward. +3. **Population** — routing exclusions are applied before the witness universe is established. + +The third made the first two survivable through merge. + +### The population defect, verified + +`v2.workflow.floor_discovery_producer` `floor_discovery_process_dag_file` returns its +state unchanged when the path is excluded — before `Filesystem.Read`, before +`floor_discovery_apply_test_sidecar_rules`. The excluded file is never read, so its test +declarations are never enumerated. It is **absent from the universe**, not +present-with-a-long-route. + +Live consequence: adding a sibling test function to an existing long-lane file skips the +whole file before function enumeration, the existing path-pattern schedule row still +reconciles, and the new function has no executing consumer anywhere. Every admission +check stays green. + +`floor_discovery_path_excluded` matches by raw substring. The registered pattern carries +a trailing slash, so `test/claim/longish/` happens not to match — a property of how the +string was typed, not a guarantee. This is the DESIGN section 3 class: a positional path +policy standing where the containment tree already names the structure. + +### The state-space defect, located in the seed + +The typed fact already exists and is destroyed in transit. `v1_interpreter.rs` declares +`InterpError::EvalBudgetExceeded { elapsed_ms, budget_ms }` — a proper variant carrying +both numbers. It is rendered to a string, surfaces at the claim boundary as an ordinary +runtime error, and is then reconstituted downstream by substring match: + +``` +falsifier_failure_mode (claim_executor.rs) + d.contains("eval budget exceeded") -> "BudgetExceeded" +``` + +The same function's own comment reads: *"THIS LIST IS A FORK, and that is the defect — +not the individual substrings."* A second consumer repeats the match in `cli_run.rs`. + +Meanwhile a *typed* `ClaimOutcome::TimedOut { elapsed_ms, budget_ms, kind }` exists and is +used by the wall-clock kill path, and `claim_batch.rs` already carries the exact insight +this note formalizes: + +> "Named as a kill, not a duration: the row stopped AT the budget, so elapsed is a +> ceiling. The clock is named because a cpu-budget kill and a wall-budget kill have +> different remedies." + +So there are two representations of one concept — one typed, one stringly — and the +fast-lane eval deadline uses the stringly one. The interruption/verdict distinction is +recovered by grepping prose. That is simultaneously the DESIGN section 3 fork and the +section 5 conflation, and it is the mechanism that made the incident possible: a +`RuntimeError { message }` carrier cannot represent "no verdict was obtained", so nothing +downstream could preserve the pending obligation even in principle. + +This is load-bearing for the program below. Step 4 is not introducing a distinction the +system lacks; it is promoting one the seed already makes, and deleting the substring +reconstruction that stands in for it. + +## The modeling decision (step 1 — what this note asks to be signed) + +| Fact | Kind | +| --- | --- | +| Witness identity and expectation | Declaration | +| Complexity / resource requirement | Declaration or structural derivation | +| Route | Derived projection | +| Attempt termination | Observation | +| Runtime cost | Runner-scoped observation | +| Semantic evidence current/pending | Derived lifecycle state | +| Lane budget | Scheduler policy | + +**Route is neither a declaration nor a lifecycle. Route is a projection. Semantic +evidence is the lifecycle.** + +The conservation law: + +``` +identity(w) invariant under route changes +expectation(w) invariant under route changes +semantic obligation(w) invariant under route changes + +execution_plan(w) may change +``` + +Merge admission requires, for every witness in the candidate: + +``` +current completed evidence AND observation matches expectation +``` + +An interruption never satisfies that predicate. + +## Why the 5-second wall loses authority but need not disappear + +The wall currently does four jobs; only the first is legitimate: + +- limits resource consumption +- classifies the witness +- prescribes a source-tree relocation +- causes the witness to disappear from the enumerated population + +A wall-clock threshold selecting a failure arm is what DESIGN section 5 names a smuggled +heuristic: its existence locates the anemic modeling it papers over. Cost is a fact this +substrate claims to carry structurally (section 4b lists "a computation exceeding its +declared complexity bound" among the differentiating classes). A witness whose cost must +be discovered by racing a stopwatch is one whose cost was never modeled. + +The repository already declares the dissolution. `gunbc.ci_layer_roots` +`long_lane_exclusion_note` carries: + +> "Dissolve-on: per-witness declared cost envelopes (witness-cost-locality admission law) +> subsume the dir grain." + +So the directory-grain route is a declared scaffold with a named trigger, and this +incident is the displaced cost that fires it. + +The correct result of a budget interruption: + +``` +BudgetExceeded + => attempted route was insufficient + AND cost is at least the granted budget + AND semantic evidence remains pending +``` + +It must not imply `witness belongs under test/claim/long/`, and must never imply +`file moved under test/claim/long/ => obligation discharged`. + +## Outcome algebra + +`red` ceases to be a domain type. It is derived job colour. + +``` +WitnessVerdict = Holds | Violates { finding } + +WitnessAttemptOutcome + = Returned { verdict, cost } + | DiagnosedStop { stage, diagnostic, cost } + | Interrupted { cause, cost } + +WitnessInterruption + = BudgetExceeded { budget } + | ProcessKilled | EvaluatorCrashed | RunnerUnavailable + | TerminalReceiptMissing | Cancelled +``` + +Only `Returned` and `DiagnosedStop` project into a semantic observation; `Interrupted` +projects to absent. `verdict_matches_expectation` therefore cannot receive a timeout — +a construction wall, not a check. + +Expectation is function-grain, not file-grain or batch-grain: + +``` +WitnessExpectation + = MustReturnHolds + | AdmittedViolation { expected_finding } + | AdmittedDiagnosedStop { expected_stage, expected_diagnostic } +``` + +`Interrupted`, including `BudgetExceeded`, is accepted by none of these. This retires the +current `QuarantineProbeExpectRed` conflation of returned-false, stable-diagnosed-stop, +and interrupted execution, and it retires batch-wide `expect_red` inversion: a batch is +an execution grouping and has no uniform verdict semantics. Matching is pointwise. + +An unexpected green becomes useful — it refuses until the stale admission dissolves. + +## Cost observation is a lower bound under a runner contract + +Even a completed elapsed duration is not intrinsic to the witness. It is an observation +under a particular runner and environment. + +``` +CostObservation + = CompletedElapsed { elapsed, runner_contract } + | LowerBound { floor, runner_contract } +``` + +A budget interruption can construct only `LowerBound { floor: budget, .. }`. It cannot +construct a completed duration. + +The four figures recorded at `c80605a` — 5002 / 5002 / 5002 / 5001 ms against a 5000 ms +budget — are pinned to the deadline by the kill mechanism. True cost could be 5.1s or +500s. They establish `cost >= 5000ms under that runner contract` and nothing else. + +**No canonical runner exists to bind measurements to.** The CI hosts in this fleet are +broken differently from one another and the warm-cache host is the slowest. Three +consequences: + +1. A lifted-budget run on a development worktree yields `CompletedElapsed` under a local + contract no CI lane shares. Sufficient to produce semantic observations; sizes nothing. +2. `RunnerContractDigest` must be genuinely discriminating — host class, cache state, + concurrency, memory cap — not a nominal lane label. Collapsed to `"fast"`/`"long"`, + receipt currency silently accepts measurements from incomparable hosts and the reuse + rule fails open exactly where it looks strongest. +3. `WitnessExecutionRequirement` must lean on structural terms (evaluation work, subject + scale, memory, effects, isolation) and treat wall-clock as a derived expectation under + a named runner, never as the declared fact. A hand-authored `expected_duration: 30s` + unbacked by a completed measurement is the directory heuristic at function grain. + +### Live receipt: the wall does not separate slow witnesses from fast ones + +Measured on this note's own PR, 2026-08-04. `witness_coproduct_arms_parse_only` +(`src/v2/test/claim/concept_index_enumeration_test.dag`) on main: + +``` +3582ms elapsed / 5000ms budget drift receipt: WithinBasis +``` + +28% headroom, formally healthy, no row anywhere marks it at risk. A diff adding one +module to `src/v2` — touching nothing the witness reads — took it to: + +``` +eval budget exceeded: 5314ms elapsed > 5000ms fast-lane budget +``` + +The wall therefore does not partition witnesses by their own cost. It partitions them by +how much unrelated corpus happened to be in the tree on the day they ran. Any PR that +adds a module can push an unrelated, in-basis witness over, and the remedy the diagnostic +offers is always relocation into a population nothing enumerates. + +Two properties follow, both load-bearing for the program: + +1. **A witness's fast-lane admissibility is not a property of the witness.** It is a + property of the whole-corpus state at run time. So route cannot be a durable + declaration attached to the file; it must be derived per candidate, which is why + route is a projection rather than a stored fact. +2. **The remedy is corpus-coupled, so the population defect is reachable from any PR.** + The incident that priced this program is not specific to a slow witness or a + particular author; it is one module-add away from any diff in the repository. + +Handled correctly on that PR: the added module was removed, nothing was relocated, and +the obligation was not discharged by a move. + +## Semantic evidence lifecycle (route-independent) + +``` +SemanticEvidenceStatus + = PendingSemanticEvidence { reason } + | CurrentSemanticEvidence { receipt } + +PendingEvidenceReason + = NeverAttempted | SubjectChanged | EvaluatorChanged + | RunnerContractChanged | ExpectationChanged + | PriorAttemptInterrupted { cause } +``` + +A fast timeout produces route-suitability evidence (fast route insufficient) and +`PendingSemanticEvidence(PriorAttemptInterrupted(BudgetExceeded))`. Re-deriving a route +does not discharge that state; only a completed candidate-bound attempt does. + +A receipt binds witness identity, witness AST digest, dependency closure digest, +evaluator digest, runner contract digest (including budget), expectation digest, +execution environment digest, and the observation. "The file did not change" is not +sufficient for reuse. + +## Ordering + +Census must precede routing. Never the reverse. + +``` +parse all witness declarations + -> construct canonical witness universe W(T) + -> resolve expectation and execution requirement + -> derive route +``` + +Route projections partition `W(T)` exactly — no overlap, no omitted member, no +independently authored roster. + +## Program + +| Step | Deliverable | +| --- | --- | +| 1 | This note signed — the modeling decision above | +| 2 | `DirectRustDoorProvenanceObservation`; run all four functions to completion under a lifted budget | +| 3 | Census before routing in `v2.workflow.floor_discovery_producer` | +| 4 | Attempt and evidence algebra; expectation split; pointwise matching | +| 5 | Route derived from execution requirement; `test/claim/long/` deleted | + +### Step-5 ruling (operator, 2026-08-04): delete the directory + +`test/claim/long/` is deleted as the **terminal** state. It may remain as temporary +migration scaffolding while census-before-routing and derived execution requirements land, +but **no new semantic dependence may be added to it**. + +The reason is dual representation, not tidiness. Once route is derived, a source directory +named `long` asserts a second, stale answer to a question the derivation already answers: + +``` +derived route says where this runs +path name implies where this runs +``` + +Even with the exclusion removed, authors and future mechanisms will read the directory +semantically again — which is how this defect reappears under a different scheduler. + +Completion shape: + +``` +witness stays beside its subject/domain + -> canonical census enumerates it + -> execution requirement derives route + -> generated CI plan groups it +``` + +Operator visibility comes from a **generated** long-route-witness projection (dashboard or +receipt), never from encoding scheduler disposition in the source tree. + +Step 2 is independent of steps 3-5 and of this note's review. Its output is semantic +observations plus a local-runner cost datum — **not** envelope inputs, per the runner +caveat above. + +`witness_direct_rust_door_provenanced_artifact_holds` collapses five independent +assertions into one Boolean (candidate accepted, emitted bytes equal expected, realized +closure excludes the seed emitter, producer is `V2EmitterInterpreted`, `SourceProduced` +qualification present). The typed observation makes the completed false attributable +rather than merely visible. Three of the four failing functions carry no known-red +admission and are therefore `MustReturnHolds`; only +`witness_v2_emitter_direct_rust_door_closing_contract_holds` is admitted. All four block +at `c80605a` regardless, because an interrupted execution satisfies neither. + +## Mutation walls + +| Mutation | Required result | +| --- | --- | +| Ordinary witness exceeds fast budget | `Interrupted(BudgetExceeded)`; expectation unsatisfied | +| Admitted-failure witness exceeds fast budget | Same; admission cannot absorb it | +| Fast timeout, relocation, no completed rerun | `PendingSemanticEvidence` | +| Long attempt also exceeds its budget | Still pending; no second escape hatch | +| New sibling function in a long file | Canonical census grows by exactly one | +| File moved between ordinary and long directories | Route unchanged unless its execution requirement changes | +| Green and admitted-failure functions share a file or batch | Each matched against its own expectation | +| Admitted failure changes shape | `ExpectedOutcomeDrifted` | +| Admitted failure becomes green | `StaleAdmission` | +| Runner contract or budget changes | Previous runtime receipt is not current | +| Route projection omits a census member | `ExecutionProjectionMissingWitness` | +| Execution plan contains an unknown member | `ExecutionProjectionContainsUnknownWitness` | +| Path exclusion applied before census in a mutated producer | Census-equivalence falsifier fails | +| `LowerBound(5s)` read as a measured duration | Refused | + +The tests must call the production census, policy resolver, plan constructor, and receipt +matcher. A parallel validation checker reimplementing those rules recreates the +dual-authority risk this note exists to remove. + +## Completion criterion + +> A route change may alter where, when, and under what budget a witness executes. It may +> not alter whether the witness exists, what outcome it owes, or whether that outcome +> remains unobserved. + +## Out of scope + +Two unrelated falsifier reds discovered in the same run are dispatched separately and do +not belong in this closure: the Clone bound propagating onto a phantom type parameter +(`fn_wf_no_trigger_negative_control`, the #7691/#7708 fixpoint), and inert-carrier roster +drift on main. diff --git a/src/v2/compiler/self_host/direct_rust_door_observation.dag b/src/v2/compiler/self_host/direct_rust_door_observation.dag new file mode 100644 index 00000000000..17777bb388c --- /dev/null +++ b/src/v2/compiler/self_host/direct_rust_door_observation.dag @@ -0,0 +1,130 @@ +module v2.compiler.self_host.direct_rust_door_observation + +import v2.compiler.infer { infer } +import v2.compiler.program_assembly { assemble_program_from_ingest } +import v2.compiler.self_host.candidate_generation { + mint_provenanced_rust_artifact, + provenanced_rust_artifact_seed_independent +} +import v2.compiler.self_host.direct_rust_door_fixture { + direct_rust_door_admission, + direct_rust_door_expected_source, + direct_rust_door_ingest, + direct_rust_door_module_path, + direct_rust_door_target_model +} +import v2.compiler.self_host.emitter_producer_provenance { + emission_qualifications_list_contains, + SourceProduced, + V2EmitterInterpreted +} +import v2.extdeps.languages.dag { dag_language_model } +import v2.std.diagnostic { Accepted, Rejected } +import v2.std.logic { Bool } +import v2.std.node { Symbol } +import v2.std.text { String } + +data direct_rust_door_observation_note: String = "Typed observation for the direct v2 Rust door source path (wise-ram-22 containment lane, PR A). WHY THIS EXISTS: witness_direct_rust_door_provenanced_artifact_holds conjoined six independent assertions into one Bool, and every Rejected arm discarded its diagnostics. The falsifier could therefore report that the door claim fails without reporting WHICH boundary fails, and a decomposition had to be hand-authored to learn it. This fold returns the FIRST failing boundary with the refusing diagnostic's reason Symbol, so a completed false is attributable by execution rather than by reconstruction. The reason is carried as a Symbol, not a file position, per DESIGN section 3 cite-the-symbol." + +data direct_rust_door_observation_measured_note: String = "MEASURED 2026-08-04 on main (claim_batch, 600s budget, four separate runs): assemble_program_from_ingest ACCEPTS, infer over the assembled tree ACCEPTS, mint_provenanced_rust_artifact on the hand-authored direct_rust_door_inferred_tree ACCEPTS, and mint_provenanced_rust_artifact on infer(assemble(direct_rust_door_ingest())) REJECTS. Every stage passes in isolation; only the real composition fails. This fold's purpose is to name that rejection's reason rather than restate the Bool." + +data direct_rust_door_observation_arm_split_scaffold_note: String = "SCAFFOLD, marked (DESIGN 5 - a scaffold with a named trigger, not an unmarked workaround). CandidateRejected vs ReceiptRefused is discriminated by comparing the head diagnostic reason against ^direct_rust_door_producer_receipt_refused. That is symbol identity, not structure: mint_provenanced_rust_artifact returns one Outcome and gives its caller no structural way to tell WHICH of its two internal boundaries refused. The honest structural alternative - calling generate_rust_emission_candidate and mint_producer_emission_receipt separately here - would duplicate production composition inside an observation, a DESIGN 3 fork, so it is the worse trade today. DISSOLVE-ON: mint returns a boundary-tagged refusal (containment lane PR B, when production stage carriers gain origin and boundary fields); then this comparison and this note delete together and the two variants derive from the returned tag. MEASURED 2026-08-04: the live reason is NOT the receipt symbol, so the corpus today takes the CandidateRejected arm - generate_rust_emission_candidate refuses the real inferred tree while accepting the hand-authored fixture." + +data direct_rust_door_observation_parse_ambiguity_note: String = "MARKED WORKAROUND, with its defect named (DESIGN 5: noticing you are implementing a workaround IS the line-stop signal; the only landing states are the real fix or a declared scaffold). The two `let source_matches` / `let producer_ok` bindings below exist because a direct comparison is UNWRITABLE: `if artifact.producer_receipt.producer != V2EmitterInterpreted { ... } else { ... }` fails to parse. LANGUAGE DEFECT, reproduced by execution 2026-08-04: the parser reads `V2EmitterInterpreted {` as a variant literal, consumes the intended if-body as its fields, and then reports `expected LBrace, found keyword else` — a token several lines BELOW the actual ambiguity. The mislocated diagnostic is the expensive half: three separate repair attempts targeted the `else` form, which was never wrong, before the real cause was found. Same class as the escaped-brace receipt in DESIGN 5 (a confusing parse error with two real parser defects beneath it). SCOPE NOT ESTABLISHED: only `!=` against a bare constructor name in an if-condition was tested; whether other operators or positions share the ambiguity is unmeasured. DISSOLVE-ON: the grammar disambiguates a constructor name before an if-body brace (or the diagnostic locates the ambiguity rather than the downstream token) — then these two let bindings inline back into their conditions and this note deletes." + +type DirectRustDoorObservation + = AssemblyRefused { reason: Symbol } + | InferenceRefused { reason: Symbol } + | CandidateRejected { reason: Symbol } + | ReceiptRefused { reason: Symbol } + | EmittedSourceMismatch + | SeedEmitterReachable + | WrongProducer + | SourceProducedQualificationMissing + | DirectRustDoorSourceProduced + +fn observe_direct_rust_door_provenance() -> DirectRustDoorObservation { + match assemble_program_from_ingest( + ingest: direct_rust_door_ingest(), + admission: direct_rust_door_admission(), + lm: dag_language_model() + ) { + Rejected { diagnostics: ds } => AssemblyRefused { reason: ds.head.reason } + Accepted { value: resolved, diagnostics: _ } => + match infer(tree: resolved) { + Rejected { diagnostics: ds } => InferenceRefused { reason: ds.head.reason } + Accepted { value: inferred, diagnostics: _ } => + match mint_provenanced_rust_artifact( + inferred: inferred, + target: direct_rust_door_target_model(), + module_path: direct_rust_door_module_path + ) { + Rejected { diagnostics: ds } => + let receipt_refused = + (ds.head.reason == ^direct_rust_door_producer_receipt_refused) + if receipt_refused { + ReceiptRefused { reason: ds.head.reason } + } else { + CandidateRejected { reason: ds.head.reason } + } + Accepted { value: artifact, diagnostics: _ } => + let source_matches = + (artifact.source.carried == direct_rust_door_expected_source) + if !source_matches { + EmittedSourceMismatch + } else { + let producer_ok = + (artifact.producer_receipt.producer == V2EmitterInterpreted) + if !producer_ok { + WrongProducer + } else { + if !provenanced_rust_artifact_seed_independent(artifact: artifact) { + SeedEmitterReachable + } else { + if !emission_qualifications_list_contains( + xs: artifact.producer_receipt.qualifications, + wanted: SourceProduced + ) { + SourceProducedQualificationMissing + } else { + DirectRustDoorSourceProduced + } + } + } + } + } + } + } +} + +data direct_rust_door_observation_arm_order_note: String = "ARM ORDER IS LOAD-BEARING (operator review 2026-08-04). provenanced_rust_artifact_seed_independent is a CONJUNCTION - it requires producer == V2EmitterInterpreted AND the seed emitter absent from the realized closure. Testing it first made WrongProducer unreachable by construction: a wrong producer fails the conjunction and was reported as SeedEmitterReachable, naming the wrong cause. The producer check therefore runs FIRST, so each arm names the fact that actually failed. Residual: the seed-independence predicate still fuses two facts, so SeedEmitterReachable is only precise once the producer is known correct. Dissolve-on: seed independence exposes its two conjuncts separately and each arm consumes its own predicate." + +data direct_rust_door_observation_totality_note: String = "Total over DirectRustDoorObservation with no wildcard arm (DESIGN 6 non-fold residue). A `_ => false` arm here would make the coproduct grow in silence: a ninth observation variant would land as false and read as an honest negative rather than an unhandled case. With no wildcard the match is non-exhaustive the moment a variant is added, which is a hard diagnostic from the compile-clean gate." + +fn direct_rust_door_observation_establishes(o: DirectRustDoorObservation) -> Bool { + match o { + AssemblyRefused { reason: _ } => false + InferenceRefused { reason: _ } => false + CandidateRejected { reason: _ } => false + ReceiptRefused { reason: _ } => false + EmittedSourceMismatch => false + SeedEmitterReachable => false + WrongProducer => false + SourceProducedQualificationMissing => false + DirectRustDoorSourceProduced => true + } +} + +fn direct_rust_door_observation_is_candidate_rejection(o: DirectRustDoorObservation) -> Bool { + match o { + AssemblyRefused { reason: _ } => false + InferenceRefused { reason: _ } => false + CandidateRejected { reason: _ } => true + ReceiptRefused { reason: _ } => false + EmittedSourceMismatch => false + SeedEmitterReachable => false + WrongProducer => false + SourceProducedQualificationMissing => false + DirectRustDoorSourceProduced => false + } +} diff --git a/src/v2/test/claim/long/direct_rust_door_observation_test.dag b/src/v2/test/claim/long/direct_rust_door_observation_test.dag new file mode 100644 index 00000000000..46c83be26b1 --- /dev/null +++ b/src/v2/test/claim/long/direct_rust_door_observation_test.dag @@ -0,0 +1,23 @@ +module v2.test.long.direct_rust_door_observation + +import v2.compiler.self_host.direct_rust_door_observation { + DirectRustDoorObservation, + DirectRustDoorSourceProduced, + direct_rust_door_observation_is_candidate_rejection, + observe_direct_rust_door_provenance +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } +import v2.std.text { String } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data direct_rust_door_observation_deferred_terminal_note: String = "TERMINAL CONTROL DEFERRED (operator review 2026-08-04). An expecting-red witness asserting DirectRustDoorSourceProduced is NOT enrolled here. Enrolling it would have placed one function in both explicit_witness_admissions (which inverts) and falsifier_substrate_long_lane_rows (which does not) - the scheduler builds those as separate batches, so the same function would be inverted in one and read as a hard false in the other. That is precisely the batch-6 defect this lane exists to repair, and the first draft of this PR committed it. The terminal control lands after step 4 delivers pointwise, function-grain expectation matching; until then the existing direct-door known-red control carries the obligation. This witness asserts only the CURRENT measured state." + +data direct_rust_door_observation_long_note: String = "LONG lane (operator 5s rule): runs the full ingest-assemble-infer-mint path; measured 13-15s per evaluation on a cold single-entry index. Enrolled on falsifier_substrate_long_lane_rows. Local recipe: claim_batch --source-root dag --source-root src/v2 --entry src/v2/test/claim/long/direct_rust_door_observation_test.dag --functions direct_rust_door_observation_is_candidate_rejected" + +test fn direct_rust_door_observation_is_candidate_rejected() -> Bool { + direct_rust_door_observation_is_candidate_rejection(o: observe_direct_rust_door_provenance()) +} + +