Falsification record: behavioral comparison ceiling (can-climb-after-one-capability)

ROADMAP.md

@@ -89,5 +89,5 @@ The graph has eleven lanes: SCM compatibility · namespace · P-derive · observ
     - [ ] **One primitive identity: definition, per-target realization, and cost as three facts on one key** — PrimitiveDefinition (identity + PrimitiveSemanticContract), PrimitiveInvocationSurface, PrimitiveRealization per RealizationTarget, PrimitiveCostFact, and PrimitiveTraversalOrderFact — five separate carriers joined by PrimitiveIdentity, never one mega-row. TERMINAL acceptance: every primitive-bearing surface across all five authorities (registry, PrimitiveContract rows, algebra templates, interpreter dispatch, emit handlers) joins exactly one identity; population-wide join and realization refusals are the closing contract. D0 is a first slice only — not the closing contract. Namespace supplies declaration identity; this node supplies semantic primitive identity across invocation and realization. Why: Proves the determinism denominator is open (#7532 honest rung) and begins closing it: four surfaces feed primitive_surface_census_derived at runtime; mutation control is CLOSED on AlgebraTemplate and EmitHandler, PARTIAL on BuiltinRegistry and PrimitiveContractRow (parallel hand rosters — primitive_d0_derived_surface_drift_audit_note), NOT DISCOVERED on InterpreterDispatch. fold_list spelling fork and index_by registry+algebra dual absence are named specimens proving the denominator is not closed. Unlocks method ambiguity wall and D1 determinism consumption through PrimitiveIdentity rather than raw symbol. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
       - [ ] **Method ambiguity refuses: more than one resolution is a located error once primitive identity defines sameness** — The method-existence wall closes cardinality zero; this closes more-than-one — two distinct primitive identities (or a primitive and a user fn) resolving for one receiver/method pair refuse with both candidates named. Gated on primitive-identity-join because ambiguity is decidable only when sameness is: the length/count/size dispatch aliases make one method look like three today (the gunbc#7484 measured fork), so an ambiguity check before the join would refuse legitimate corpus or silently pick. Why: The silent-first-hit dispatch class: today arm order decides which of two candidates runs — an unstated tiebreak the census cannot even measure until sameness is defined. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md) — requires all: primitive-identity-join, method-zero-resolution-general-wall
       - [ ] **Determinism denominator closure: every primitive carries one traversal-order classification** — v2.std.determinism and v2.lens.determinism consume std.primitive_identity: every PrimitiveDefinition carries exactly one PrimitiveTraversalOrderFact, unclassified refuses, HostUnspecifiedOrder derives a determinism root, aliases resolve through PrimitiveIdentity not raw symbol. Adding a new invokable primitive realization without a traversal-order fact reds before any caller uses it. Why: Dissolves the interim two-root registry (#7532) into a closed denominator — the gate can tell an alias from a distinct operation, and keys/values false-positive class is eliminated by identity not spelling. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
-- [ ] **Write the closing check for: The capability audit: sole_constructor completeness, then seal the proof-carriers** — One executable check states when this is done, transcribed from the node's own bar: Refined authored outside the sealing module refuses at compile in every probed form; refine remains the only inhabitation path; a probe form that does NOT refuse is a counted audit finding, never silently absorbed. Why: Turns a prose bar into a runnable verdict, so the node it gates can be dispatched and its completion checked rather than judged. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
+- [ ] **Write the closing check for: The capability audit: sole_constructor completeness, then seal the proof-carriers** — One executable check states when this is done, transcribed from the node's own bar: Refined authored outside the sealing module refuses at compile in every probed form; refine remains the only inhabitation path; a probe form that does NOT refuse is a counted audit finding, never silently absorbed. BehavioralComparisonObservation: record literal outside declaring module → SoleConstructorViolation; exported mint call with caller stdout → counted leak (not silently absorbed). Why: Turns a prose bar into a runnable verdict, so the node it gates can be dispatched and its completion checked rather than judged. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)
   - [ ] **The capability audit: sole_constructor completeness, then seal the proof-carriers** — The language ALREADY has a construction wall: sole_constructor rejects cross-module construction with SoleConstructorViolation and carries a sealed-record specimen (post-merge review of gunbc#7486 refuted this node's earlier premise that no private/sealed/opaque capability exists). What is UNVERIFIED is its completeness: generic carriers (does type Refined<B> sole_constructor hold across instantiation?), every construction form (literals, casts like as TransportScript, coproduct variants, default values), and behavior under module_skips_direct_call_arg_check. Audit by falsification first; extend sole_constructor or ground the reference-grant algebra (the parked visibility-grants design) only where the audit reds. Why: Every capability-kind ceiling resolves together — either sole_constructor suffices (cheap: seal Refined, delete the stub-pack forge arm) or its named gaps price the visibility-grants work honestly instead of by assumption. [authority](docs/plans/compiler-guarantee-recovery-gap-analysis.md)

dag/gunbc/ci_layer_roots.dag

@@ -157,6 +157,12 @@ data witness_exclusion_frontier: List<WitnessExclusionRow> = [
     reason: "wet-integration class (wet_integration_offline_note posture), substantiated per-row: direct_rust_door_emit_write_compile_holds runs tools.direct_rust_door_transport.run_direct_rust_door_emit_write_compile_smoke, which performs live shell.Mktemp.Dir, Filesystem.Write, and cargo.Build.BuildManifest effects with no hermetic mock_response coverage. Hermetic discovery REFUSES rather than fabricating Unit, so per-PR discovery cannot exercise the write-to-disk + compile receipt. Ingest-path provenance and closing-contract witnesses live in src/v2/test/claim/long/ (5s budget rule); fast closure witnesses stay per-PR in src/v2/test/claim/self_host/.",
     dissolve_on: "the wet lane un-darkens and admits live cargo compile smokes under its own budget; this witness enrolls there as a declared execution row and this exclusion deletes. Local recipe until then: claim_batch --wet --source-root dag --source-root src/v2 --entry dag/test/claim/direct_rust_door_write_compile_witness_test.dag --function direct_rust_door_emit_write_compile_holds"
   },
+  WitnessExclusionRow {
+    pattern: "direct_rust_door_behavioral_qualification_witness_test.dag",
+    classification: OfflineLocalRecipe,
+    reason: "wet-integration class (royal-crab-235 Lane 4 PR2): direct_rust_door_behavioral_qualification_holds and direct_rust_door_divergent_behavioral_receipt_refused_reds run tools.direct_rust_door_transport behavioral qualification smokes — live shell.Mktemp, Filesystem.Write, cargo.Build.BuildManifest (lib + witness bin), and gunbc.WitnessBin.Run with --inject-fault. Hermetic discovery REFUSES rather than fabricating Unit. Fast construction + ladder RED controls stay per-PR in src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag.",
+    dissolve_on: "the wet lane un-darkens and admits Lane 4 behavioral qualification smokes under its own budget; this witness enrolls there as a declared execution row and this exclusion deletes. Local recipe until then: claim_batch --wet --source-root dag --source-root src/v2 --entry dag/test/claim/direct_rust_door_behavioral_qualification_witness_test.dag --function direct_rust_door_behavioral_qualification_holds"
+  },
   WitnessExclusionRow {
     pattern: "external_model_scope_live_cover_witness_test.dag",
     classification: OfflineLocalRecipe,

dag/gunbc/doc_graph_roots.dag

@@ -541,6 +541,16 @@ data hand_authored_doc_binds: List<HandAuthoredDocBind> = [
     ],
     dissolution: HasTrigger { text: "v2.lens.cost carries grounded SizeExpr/CostExpr with normalize_cost_expr_to_symbolic live, the C1 blocking-wall baseline roster is green post-carrier, bounded-summation and CostRefused witnesses execute green, and parity note C1 acceptance is met — then the carriers state the capability and this bind deletes with the doc." },
   },
+  HandAuthoredDocBind {
+    home: PlanDoc,
+    slug: "constructor-reference-admission-design",
+    primary_work: DeclarationRef { module_path: "v2.compiler.self_host.behavioral_comparison_receipt", decl_name: "behavioral_admission_seal_ceiling_note", field: WholeDeclaration },
+    additional_works: [
+      DeclarationRef { module_path: "v2.compiler.self_host.behavioral_comparison_receipt", decl_name: "mint_behavioral_comparison_observation", field: WholeDeclaration },
+      DeclarationRef { module_path: "v2.test.claim.self_host.direct_rust_door_qualification_witness_test", decl_name: "fully_matching_derived_seal_forgery_advance_succeeds_red", field: WholeDeclaration },
+    ],
+    dissolution: HasTrigger { text: "ConstructorReferenceAdmission lands on BehavioralComparisonObservation (call-edge admission in the operator-chosen infer authority — record-literal and call-edge in one construction-admission authority, no separate pass), fully_matching_derived_seal_forgery_advance_succeeds_red flips from green to refuse on the forge path, and the doc migrates into a registered gunbc.plan.Plan row or deletes with the std carrier — then this bind deletes with the md." },
+  },
   HandAuthoredDocBind {
     home: ProbeDoc,
     slug: "g1-cited-symbol-control-declaration-absent",

dag/gunbc/roadmap_authority.dag

@@ -2923,8 +2923,8 @@ fn guarantee_ladder_nodes() -> List<RoadmapNode> {
         headline: "The capability audit: sole_constructor completeness, then seal the proof-carriers",
         boundary: "The language ALREADY has a construction wall: sole_constructor rejects cross-module construction with SoleConstructorViolation and carries a sealed-record specimen (post-merge review of gunbc#7486 refuted this node's earlier premise that no private/sealed/opaque capability exists). What is UNVERIFIED is its completeness: generic carriers (does type Refined<B> sole_constructor hold across instantiation?), every construction form (literals, casts like as TransportScript, coproduct variants, default values), and behavior under module_skips_direct_call_arg_check. Audit by falsification first; extend sole_constructor or ground the reference-grant algebra (the parked visibility-grants design) only where the audit reds.",
         displaced_cost: "Every capability-kind ceiling resolves together — either sole_constructor suffices (cheap: seal Refined, delete the stub-pack forge arm) or its named gaps price the visibility-grants work honestly instead of by assumption.",
-        first_slice: "The falsification matrix on ONE carrier: type Refined<B> sole_constructor with cross-module forge probes per construction form, incl. inside v2.* modules; delete refined_vacuous_stub_pack's forged rejection arm if the wall holds.",
-        red_control: "Refined authored outside the sealing module refuses at compile in every probed form; refine remains the only inhabitation path; a probe form that does NOT refuse is a counted audit finding, never silently absorbed.",
+        first_slice: "The falsification matrix on ONE carrier: type Refined<B> sole_constructor with cross-module forge probes per construction form, incl. inside v2.* modules; delete refined_vacuous_stub_pack's forged rejection arm if the wall holds. BehavioralComparisonObservation row landed (record literal refused, exported mint call leaking); bounded opaque-effect probe concluded NEGATIVE — next slice is capability lane (export control or opaque service output type), not another module-structure carrier.",
+        red_control: "Refined authored outside the sealing module refuses at compile in every probed form; refine remains the only inhabitation path; a probe form that does NOT refuse is a counted audit finding, never silently absorbed. BehavioralComparisonObservation: record literal outside declaring module → SoleConstructorViolation; exported mint call with caller stdout → counted leak (not silently absorbed).",
         out_of_scope: "Publish-verb storage visibility (its own parked lane); retrofitting every brand in one motion; new language syntax before the audit reds.",
         handback: "The completeness matrix (form x module-context x verdict), the sealed-Refined receipt or the named counterexamples, and the roster of classes whose ceiling reason flips."
       )

dag/test/claim/direct_rust_door_behavioral_qualification_witness_test.dag

@@ -0,0 +1,20 @@
+module test.claim.direct_rust_door_behavioral_qualification_witness_test
+
+import tools.direct_rust_door_transport {
+  run_direct_rust_door_behavioral_qualification_smoke,
+  run_direct_rust_door_divergent_behavioral_receipt_refused
+}
+import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }
+import v2.std.logic { Bool }
+
+data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree
+
+data direct_rust_door_behavioral_qualification_witness_note: String = "Lane 4 wet fixture behavioral qualification (disposition 2): after FixtureCargoGreen, executed comparison must green before advance_written_synthetic_emitted_artifact_fixture_behaviorally_equivalent mints FixtureBehaviorallyEquivalent — not production BehavioralEquivalent. Positive control: run_direct_rust_door_behavioral_qualification_smoke. RED control: run_direct_rust_door_divergent_behavioral_receipt_refused. Local recipe: claim_batch --wet --source-root dag --source-root src/v2 --entry dag/test/claim/direct_rust_door_behavioral_qualification_witness_test.dag --function direct_rust_door_behavioral_qualification_holds"
+
+test fn direct_rust_door_behavioral_qualification_holds() -> Bool {
+  run_direct_rust_door_behavioral_qualification_smoke()
+}
+
+test fn direct_rust_door_divergent_behavioral_receipt_refused_reds() -> Bool {
+  run_direct_rust_door_divergent_behavioral_receipt_refused()
+}

dag/test/claim/roadmap_program_view_witness_test.dag

@@ -399,7 +399,6 @@ test fn witness_proposed_plane_carries_nothing_by_construction() -> Bool {
     }
   }
 }
-
 test fn witness_fixture_every_front_contributes_to_some_line() -> Bool {
   let view = fx_derived(receipts: [], in_flight: [])
   all(view.fronts, fv =>