From 03923cbefab360927f9b3c4b2637e3edc20e7223 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 15:51:42 +0000 Subject: [PATCH 01/22] PR2: fixture-scoped direct-door behavioral comparison harness. FixtureBehaviorallyEquivalent via executed stdout parsing, fixture-scoped stdout parser, wet transport with independent head binding. Documents admission_seal ceiling (checksum not execution witness) with derived-seal forgery RED. No production-carrier edits. Stacks on PR1 containment (#7761). Co-authored-by: Cursor --- dag/gunbc/ci_layer_roots.dag | 6 + ..._behavioral_qualification_witness_test.dag | 20 + dag/tools/direct_rust_door_transport.dag | 295 ++++++++++++- .../behavioral_comparison_receipt.dag | 344 +++++++++++++++ .../direct_rust_door_behavioral_stdout.dag | 220 ++++++++++ .../self_host/direct_rust_door_fixture.dag | 181 ++++++++ .../self_host/fixture_synthetic_emission.dag | 162 +++++-- ...t_rust_door_qualification_witness_test.dag | 398 ++++++++++++++++++ 8 files changed, 1584 insertions(+), 42 deletions(-) create mode 100644 dag/test/claim/direct_rust_door_behavioral_qualification_witness_test.dag create mode 100644 src/v2/compiler/self_host/behavioral_comparison_receipt.dag create mode 100644 src/v2/compiler/self_host/direct_rust_door_behavioral_stdout.dag create mode 100644 src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag diff --git a/dag/gunbc/ci_layer_roots.dag b/dag/gunbc/ci_layer_roots.dag index 169017e05fd..fd273565161 100644 --- a/dag/gunbc/ci_layer_roots.dag +++ b/dag/gunbc/ci_layer_roots.dag @@ -157,6 +157,12 @@ data witness_exclusion_frontier: List = [ 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, diff --git a/dag/test/claim/direct_rust_door_behavioral_qualification_witness_test.dag b/dag/test/claim/direct_rust_door_behavioral_qualification_witness_test.dag new file mode 100644 index 00000000000..4989f1ecc4a --- /dev/null +++ b/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() +} diff --git a/dag/tools/direct_rust_door_transport.dag b/dag/tools/direct_rust_door_transport.dag index 69c863ec1d6..dd3787e3d0e 100644 --- a/dag/tools/direct_rust_door_transport.dag +++ b/dag/tools/direct_rust_door_transport.dag @@ -1,26 +1,192 @@ module tools.direct_rust_door_transport import extdeps.cargo_build +import extdeps.filesystem.filesystem_io { Filesystem } +import extdeps.git.inspect +import extdeps.gunbc import extdeps.shell +import v2.compiler.self_host.behavioral_comparison_receipt { + AdmittedBehaviorEquivalent, + AdmittedBehaviorEquivalentReceipt, + BehaviorExecutionRefused, + BehavioralComparisonAdmission, + BehavioralComparisonObservation, + BehavioralComparisonRow, + BehaviorDiverged, + admit_behavioral_comparison, + admit_behavioral_comparison_equivalent +} +import v2.compiler.self_host.direct_rust_door_behavioral_stdout { + direct_rust_door_inject_fault_stdout_holds, + direct_rust_door_parse_pass_rows_from_stdout, + direct_rust_door_parse_subtract_rows_from_stdout, + direct_rust_door_pass_stdout_holds, + direct_rust_door_subtract_stdout_holds +} import v2.compiler.self_host.fixture_synthetic_emission { advance_written_synthetic_emitted_artifact_cargo_green, + advance_written_synthetic_emitted_artifact_fixture_behaviorally_equivalent, + fixture_behavior_receipt_identity_for, mint_written_synthetic_emitted_artifact_from_fixture_inferred, + WrittenSyntheticEmittedArtifact, + written_synthetic_emitted_artifact_has_fixture_behaviorally_equivalent_qualification, written_synthetic_emitted_artifact_has_fixture_cargo_green_qualification, written_synthetic_emitted_artifact_ok } import v2.compiler.self_host.direct_rust_door_fixture { + direct_rust_door_behavioral_corpus_identity, + direct_rust_door_behavioral_probe_entry, + direct_rust_door_behavioral_probe_function, + direct_rust_door_behavioral_witness_bin_path, + direct_rust_door_divergent_rust_source, direct_rust_door_inferred_tree, direct_rust_door_module_path, direct_rust_door_target_model } +import v2.std.collection { List } import v2.std.diagnostic { Accepted, Rejected } import v2.std.logic { Bool } -import v2.std.optional { Absent, Present } +import v2.std.optional { Absent, Present, optional_absent, optional_present } import v2.std.text { String } +import std.types { CommitSha } + +data direct_rust_door_transport_note: String = "Lane B wet transport realization (disposition 2): mint_written_synthetic_emitted_artifact_from_fixture_inferred is the sole fixture write authority; FixtureCargoGreen only after cargo.Build.BuildManifest executes. Behavioral comparison_rows are parsed FROM executed stdout; advance binds head_sha from git.Inspect.HeadCommit independently of the receipt." + +data direct_rust_door_witness_driver_scaffold_note: String = "SCAFFOLD — tracked debt: direct_rust_door_witness_main_source and direct_rust_door_witness_cargo_appendix are hand-authored Rust witness-driver carriers for the Lane 4 behavioral comparison harness (include! of unmodified emitted lib.rs + seed_add oracle + discriminating corpus + --inject-fault). dissolve-on: modeled self-host behavioral-equivalence harness producer emits the comparison driver; these string carriers delete with it." + +data direct_rust_door_witness_cargo_appendix: String = "\n[[bin]]\nname = \"witness\"\npath = \"src/main.rs\"\n" -data direct_rust_door_fixture_lane_tag: String = "direct_rust_door_fixture_containment" +data direct_rust_door_witness_main_source: String = "mod emitted_lib {\n include!(\"lib.rs\");\n pub fn invoke_add(x: i32, y: i32) -> i32 {\n add(x, y)\n }\n}\n\nfn seed_add(x: i32, y: i32) -> i32 {\n x + y\n}\n\nfn main() {\n let inject_fault = std::env::args().any(|a| a == \"--inject-fault\");\n let corpus: [(i32, i32, i32); 4] = [\n (2, 3, 5),\n (0, 0, 0),\n (-1, 1, 0),\n (100, -50, 50),\n ];\n let mut all_pass = true;\n for (x, y, expected) in corpus {\n let call_x = if inject_fault && x == 2 && y == 3 { x + 1 } else { x };\n let emitted = emitted_lib::invoke_add(call_x, y);\n let seed = seed_add(call_x, y);\n let ok = emitted == seed && emitted == expected;\n println!(\n \"BEHAVIORAL_CASE x={} y={} call_x={} expected={} actual={} seed={} ok={}\",\n x, y, call_x, expected, emitted, seed, ok\n );\n all_pass = all_pass && ok;\n }\n if all_pass {\n println!(\"BEHAVIORAL_VERDICT: EQUIVALENT\");\n std::process::exit(0);\n } else {\n println!(\"BEHAVIORAL_VERDICT: DIVERGED\");\n std::process::exit(1);\n }\n}\n" -data direct_rust_door_transport_note: String = "Lane B wet transport realization (wise-ram-22 PR1 containment): mint_written_synthetic_emitted_artifact_from_fixture_inferred is the sole fixture write authority; FixtureCargoGreen only after cargo.Build.BuildManifest executes. No mint_written_provenanced_rust_artifact and no ProducerEmissionReceipt on this path." +fn direct_rust_door_behavioral_observation_from_run( + written: WrittenSyntheticEmittedArtifact, + stdout: String, + stderr: String, + exit_success: Bool, + head_sha: CommitSha, + comparison_rows: List, + executable_content: String +) -> BehavioralComparisonObservation { + BehavioralComparisonObservation { + module_path: written.artifact.fixture_receipt.module_path, + emitted_source: written.artifact.source, + subject_binding_identity: fixture_behavior_receipt_identity_for( + receipt: written.artifact.fixture_receipt + ), + executable_content: executable_content, + stdout: stdout, + stderr: stderr, + exit_success: exit_success, + head_sha: head_sha, + corpus_identity: direct_rust_door_behavioral_corpus_identity(), + comparison_rows: comparison_rows, + behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + behavioral_probe_function: direct_rust_door_behavioral_probe_function + } +} + +fn direct_rust_door_prepare_behavioral_witness_workspace(workspace_dir: String) -> Bool { + let manifest_path = concat(workspace_dir, "/Cargo.toml") + let manifest_read = Filesystem.Read(path: manifest_path) + let manifest_write = Filesystem.Write( + path: manifest_path, + content: concat(manifest_read.content, direct_rust_door_witness_cargo_appendix) + ) + let witness_main = Filesystem.Write( + path: concat(workspace_dir, "/src/main.rs"), + content: direct_rust_door_witness_main_source + ) + let build = cargo.Build.BuildManifest( + workdir: workspace_dir, + manifest_path: manifest_path, + target_dir: concat(workspace_dir, "/target"), + extra_args: ["--release"] + ) + manifest_read.success + && manifest_write.success + && witness_main.success + && build.success +} + +fn direct_rust_door_admitted_equivalent_for_workspace( + workspace_dir: String, + written: WrittenSyntheticEmittedArtifact +) -> Optional { + let witness_bin_path = + direct_rust_door_behavioral_witness_bin_path(workspace_dir: workspace_dir) + if !direct_rust_door_prepare_behavioral_witness_workspace(workspace_dir: workspace_dir) { + optional_absent() + } else { + let pass_run = gunbc.WitnessBin.Run(workdir: workspace_dir, bin_path: witness_bin_path) + let fault_run = gunbc.WitnessBin.Run( + workdir: workspace_dir, + bin_path: witness_bin_path, + args: ["--inject-fault"] + ) + let executable_read = Filesystem.Read(path: witness_bin_path) + let head = git.Inspect.HeadCommit() + let parsed_rows = direct_rust_door_parse_pass_rows_from_stdout(stdout: pass_run.stdout) + if pass_run.success + && executable_read.success + && head.success + && direct_rust_door_pass_stdout_holds(stdout: pass_run.stdout) + && direct_rust_door_inject_fault_stdout_holds(stdout: fault_run.stdout) { + match parsed_rows { + Present { value: comparison_rows } => + let observation = direct_rust_door_behavioral_observation_from_run( + written: written, + stdout: pass_run.stdout, + stderr: pass_run.stderr, + exit_success: pass_run.success, + head_sha: head.sha, + comparison_rows: comparison_rows, + executable_content: executable_read.content + ) + admit_behavioral_comparison_equivalent(observation: observation) + Absent => optional_absent() + } + } else { + optional_absent() + } + } +} + +fn direct_rust_door_subtract_admission_for_workspace( + workspace_dir: String, + written: WrittenSyntheticEmittedArtifact +) -> Optional { + let witness_bin_path = + direct_rust_door_behavioral_witness_bin_path(workspace_dir: workspace_dir) + if !direct_rust_door_prepare_behavioral_witness_workspace(workspace_dir: workspace_dir) { + optional_absent() + } else { + let pass_run = gunbc.WitnessBin.Run(workdir: workspace_dir, bin_path: witness_bin_path) + let executable_read = Filesystem.Read(path: witness_bin_path) + let head = git.Inspect.HeadCommit() + let parsed_rows = + direct_rust_door_parse_subtract_rows_from_stdout(stdout: pass_run.stdout) + if executable_read.success + && head.success + && direct_rust_door_subtract_stdout_holds(stdout: pass_run.stdout) { + match parsed_rows { + Present { value: comparison_rows } => + let observation = direct_rust_door_behavioral_observation_from_run( + written: written, + stdout: pass_run.stdout, + stderr: pass_run.stderr, + exit_success: pass_run.success, + head_sha: head.sha, + comparison_rows: comparison_rows, + executable_content: executable_read.content + ) + optional_present(value: admit_behavioral_comparison(observation: observation)) + Absent => optional_absent() + } + } else { + optional_absent() + } + } +} fn direct_rust_door_compile_workspace(workspace_dir: String) -> Bool { let build = cargo.Build.BuildManifest( @@ -32,7 +198,104 @@ fn direct_rust_door_compile_workspace(workspace_dir: String) -> Bool { build.success } +fn direct_rust_door_emit_write_compile_to_cargo_green( + workspace_dir: String +) -> Optional { + match mint_written_synthetic_emitted_artifact_from_fixture_inferred( + inferred: direct_rust_door_inferred_tree, + target: direct_rust_door_target_model(), + module_path: direct_rust_door_module_path, + workspace_dir: workspace_dir, + behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + behavioral_probe_function: direct_rust_door_behavioral_probe_function + ) { + Accepted { value: written, diagnostics: _ } => + let compile_ok = + written_synthetic_emitted_artifact_ok(written: written) + && direct_rust_door_compile_workspace(workspace_dir: workspace_dir) + match advance_written_synthetic_emitted_artifact_cargo_green( + written: written, + cargo_green: compile_ok + ) { + Present { value: cargo_written } => + if written_synthetic_emitted_artifact_ok(written: cargo_written) + && written_synthetic_emitted_artifact_has_fixture_cargo_green_qualification( + written: cargo_written + ) { + optional_present(value: cargo_written) + } else { + optional_absent() + } + Absent => optional_absent() + } + Rejected { diagnostics: _ } => optional_absent() + } +} + fn run_direct_rust_door_emit_write_compile_smoke() -> Bool { + let dir = shell.Mktemp.Dir() + let src_dir = shell.Mkdir.Parents(path: concat(dir.path, "/src")) + let pipeline_ok = match direct_rust_door_emit_write_compile_to_cargo_green( + workspace_dir: dir.path + ) { + Present { value: _ } => true + Absent => false + } + let cleanup = shell.Remove.RecursiveForce(path: dir.path) + dir.success + && src_dir.success + && pipeline_ok + && cleanup.success +} + +fn run_direct_rust_door_behavioral_qualification_smoke() -> Bool { + let dir = shell.Mktemp.Dir() + let src_dir = shell.Mkdir.Parents(path: concat(dir.path, "/src")) + let pipeline_ok = match direct_rust_door_emit_write_compile_to_cargo_green( + workspace_dir: dir.path + ) { + Present { value: cargo_written } => + match direct_rust_door_admitted_equivalent_for_workspace( + workspace_dir: dir.path, + written: cargo_written + ) { + Present { value: admitted } => + let witness_bin_path = + direct_rust_door_behavioral_witness_bin_path(workspace_dir: dir.path) + let executable_read = Filesystem.Read(path: witness_bin_path) + let head = git.Inspect.HeadCommit() + match advance_written_synthetic_emitted_artifact_fixture_behaviorally_equivalent( + written: cargo_written, + admitted: admitted, + executable_content: executable_read.content, + head_sha: head.sha, + expected_behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + expected_behavioral_probe_function: direct_rust_door_behavioral_probe_function + ) { + Present { value: behavioral_written } => + head.success + && executable_read.success + && written_synthetic_emitted_artifact_ok(written: behavioral_written) + && written_synthetic_emitted_artifact_has_fixture_cargo_green_qualification( + written: behavioral_written + ) + && written_synthetic_emitted_artifact_has_fixture_behaviorally_equivalent_qualification( + written: behavioral_written + ) + Absent => false + } + Absent => false + } + Absent => false + } + let cleanup = shell.Remove.RecursiveForce(path: dir.path) + dir.success + && src_dir.success + && pipeline_ok + && cleanup.success +} + +fn run_direct_rust_door_divergent_behavioral_receipt_refused() -> Bool { let dir = shell.Mktemp.Dir() let src_dir = shell.Mkdir.Parents(path: concat(dir.path, "/src")) let pipeline_ok = match mint_written_synthetic_emitted_artifact_from_fixture_inferred( @@ -40,21 +303,35 @@ fn run_direct_rust_door_emit_write_compile_smoke() -> Bool { target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, workspace_dir: dir.path, - fixture_lane_tag: direct_rust_door_fixture_lane_tag + behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + behavioral_probe_function: direct_rust_door_behavioral_probe_function ) { Accepted { value: written, diagnostics: _ } => + let divergent_write = Filesystem.Write( + path: concat(dir.path, "/src/lib.rs"), + content: direct_rust_door_divergent_rust_source + ) let compile_ok = - written_synthetic_emitted_artifact_ok(written: written) + divergent_write.success + && written_synthetic_emitted_artifact_ok(written: written) && direct_rust_door_compile_workspace(workspace_dir: dir.path) match advance_written_synthetic_emitted_artifact_cargo_green( written: written, cargo_green: compile_ok ) { Present { value: cargo_written } => - written_synthetic_emitted_artifact_ok(written: cargo_written) - && written_synthetic_emitted_artifact_has_fixture_cargo_green_qualification( - written: cargo_written - ) + match direct_rust_door_subtract_admission_for_workspace( + workspace_dir: dir.path, + written: cargo_written + ) { + Present { value: admission } => + match admission { + BehaviorDiverged { receipt: _, differences: _ } => true + AdmittedBehaviorEquivalent { admitted: _ } => false + BehaviorExecutionRefused { cause: _, receipt: _ } => false + } + Absent => false + } Absent => false } Rejected { diagnostics: _ } => false diff --git a/src/v2/compiler/self_host/behavioral_comparison_receipt.dag b/src/v2/compiler/self_host/behavioral_comparison_receipt.dag new file mode 100644 index 00000000000..287ac354ae5 --- /dev/null +++ b/src/v2/compiler/self_host/behavioral_comparison_receipt.dag @@ -0,0 +1,344 @@ +module v2.compiler.self_host.behavioral_comparison_receipt + +import std.content_hash { content_hash_atom } +import extdeps.communication.medium { Medium } +import v2.std.algebra { Cons, Empty, fold_list, length } +import v2.std.collection { List } +import v2.std.logic { Bool } +import v2.std.node { Hash, combine_hash, symbol_identity_digest } +import v2.std.optional { Absent, Present, optional_absent, optional_present } +import v2.std.text { String } +import std.types { CommitSha, Int } + +data behavioral_comparison_receipt_note: String = "Executed behavioral comparison receipt carrier (still-bat-561 ceiling audit): rows and verdict are derived from stdout at observation construction. advance checks field binding against the written artifact — NOT that stdout came from a real process." + +data behavioral_admission_seal_ceiling_note: String = "CEILING (still-bat-561): admission_seal is a pure digest of caller-supplied observation fields — behavioral_admission_seal_for_observation(observation) is reachable from any module and authenticates nothing. behavioral_admission_seal_is_minted is a not-equal-to-sentinel test only. A matching counterfeit with derived seal passes advance; witness fully_matching_derived_seal_forgery_advance_succeeds_red records that gap. Unforgeable execution witness requires observation construction walled to the wet transport host-effect path (sole_constructor on BehavioralComparisonObservation with mint reachable only from process output, or equivalent) — not expressible as a derived post-hoc seal today; sole_constructor completeness on AdmittedBehaviorEquivalentReceipt alone does not close observation forgery because admit_behavioral_comparison_equivalent(observation) accepts caller-authored observations." + +type BehavioralComparisonSubject { + module_path: String + emitted_source_identity: Hash + subject_binding_identity: Hash + executable_identity: Hash +} + +type BehavioralComparisonRow { + corpus_x: Int + corpus_y: Int + call_x: Int + expected: Int + actual: Int + seed: Int + ok: Bool +} + +type BehavioralComparisonDifference { + corpus_x: Int + corpus_y: Int + call_x: Int + expected: Int + actual: Int + seed: Int +} + +type BehavioralComparisonReceipt { + subject: BehavioralComparisonSubject + corpus_identity: Hash + comparison_rows: List + stdout: String + stderr: String + exit_success: Bool + execution_identity: Hash + head_sha: CommitSha + behavioral_probe_entry: String + behavioral_probe_function: String + admission_seal: Hash +} + +type BehavioralComparisonObservation { + module_path: String + emitted_source: Medium + subject_binding_identity: Hash + executable_content: String + stdout: String + stderr: String + exit_success: Bool + head_sha: CommitSha + corpus_identity: Hash + comparison_rows: List + behavioral_probe_entry: String + behavioral_probe_function: String +} + +type AdmittedBehaviorEquivalentReceipt { + receipt: BehavioralComparisonReceipt +} + +type BehavioralComparisonAdmission + = AdmittedBehaviorEquivalent { admitted: AdmittedBehaviorEquivalentReceipt } + | BehaviorDiverged { + receipt: BehavioralComparisonReceipt, + differences: List + } + | BehaviorExecutionRefused { + cause: Symbol, + receipt: BehavioralComparisonReceipt + } + +data behavioral_admission_seal_unminted: Hash = symbol_identity_digest( + sym: ^behavioral_admission_seal_unminted +) + +data behavioral_comparison_corpus_nonempty_note: String = "Admission refuses empty comparison_rows — a comparison with zero cases is not discriminating." + +fn behavioral_comparison_rows_nonempty(rows: List) -> Bool { + length(xs: rows) > 0 +} + +fn emitted_source_identity_for_medium(source: Medium) -> Hash { + content_hash_atom(value: source.carried) +} + +fn executable_identity_for_content(content: String) -> Hash { + combine_hash( + a: symbol_identity_digest(sym: ^behavioral_comparison_executable_content), + b: content_hash_atom(value: content) + ) +} + +fn behavioral_comparison_execution_identity( + stdout: String, + stderr: String, + exit_success: Bool +) -> Hash { + combine_hash( + a: symbol_identity_digest(sym: ^behavioral_comparison_execution_identity), + b: combine_hash( + a: content_hash_atom(value: stdout), + b: combine_hash( + a: content_hash_atom(value: stderr), + b: if exit_success { + symbol_identity_digest(sym: ^behavioral_exit_success) + } else { + symbol_identity_digest(sym: ^behavioral_exit_failure) + } + ) + ) + ) +} + +fn behavioral_comparison_verdict_is_equivalent(stdout: String) -> Bool { + string_contains(s: stdout, pattern: "BEHAVIORAL_VERDICT: EQUIVALENT") +} + +fn behavioral_comparison_verdict_is_diverged(stdout: String) -> Bool { + string_contains(s: stdout, pattern: "BEHAVIORAL_VERDICT: DIVERGED") +} + +fn behavioral_comparison_row_is_equivalent(row: BehavioralComparisonRow) -> Bool { + row.ok && (row.actual == row.expected) && (row.actual == row.seed) +} + +fn behavioral_comparison_all_rows_equivalent(rows: List) -> Bool { + fold_list( + xs: rows, + empty: true, + cons: fn(acc, row) { + acc && behavioral_comparison_row_is_equivalent(row: row) + } + ) +} + +fn behavioral_comparison_difference_from_row(row: BehavioralComparisonRow) -> BehavioralComparisonDifference { + BehavioralComparisonDifference { + corpus_x: row.corpus_x, + corpus_y: row.corpus_y, + call_x: row.call_x, + expected: row.expected, + actual: row.actual, + seed: row.seed + } +} + +fn behavioral_comparison_differences_from_rows( + rows: List +) -> List { + fold_list( + xs: rows, + empty: Empty, + cons: fn(acc, row) { + if behavioral_comparison_row_is_equivalent(row: row) { + acc + } else { + Cons { + head: behavioral_comparison_difference_from_row(row: row), + tail: acc + } + } + } + ) +} + +fn behavioral_admission_seal_for_observation( + observation: BehavioralComparisonObservation +) -> Hash { + combine_hash( + a: symbol_identity_digest(sym: ^behavioral_admission_mint_seal), + b: combine_hash( + a: behavioral_comparison_execution_identity( + stdout: observation.stdout, + stderr: observation.stderr, + exit_success: observation.exit_success + ), + b: combine_hash( + a: observation.corpus_identity, + b: combine_hash( + a: executable_identity_for_content(content: observation.executable_content), + b: combine_hash( + a: observation.subject_binding_identity, + b: content_hash_atom(value: observation.stdout) + ) + ) + ) + ) + ) +} + +fn behavioral_comparison_subject_for_observation( + observation: BehavioralComparisonObservation +) -> BehavioralComparisonSubject { + BehavioralComparisonSubject { + module_path: observation.module_path, + emitted_source_identity: emitted_source_identity_for_medium( + source: observation.emitted_source + ), + subject_binding_identity: observation.subject_binding_identity, + executable_identity: executable_identity_for_content( + content: observation.executable_content + ) + } +} + +fn behavioral_comparison_receipt_from_observation( + observation: BehavioralComparisonObservation, + admission_seal: Hash +) -> BehavioralComparisonReceipt { + BehavioralComparisonReceipt { + subject: behavioral_comparison_subject_for_observation(observation: observation), + corpus_identity: observation.corpus_identity, + comparison_rows: observation.comparison_rows, + stdout: observation.stdout, + stderr: observation.stderr, + exit_success: observation.exit_success, + execution_identity: behavioral_comparison_execution_identity( + stdout: observation.stdout, + stderr: observation.stderr, + exit_success: observation.exit_success + ), + head_sha: observation.head_sha, + behavioral_probe_entry: observation.behavioral_probe_entry, + behavioral_probe_function: observation.behavioral_probe_function, + admission_seal: admission_seal + } +} + +fn behavioral_comparison_receipt_unminted_from_observation( + observation: BehavioralComparisonObservation +) -> BehavioralComparisonReceipt { + behavioral_comparison_receipt_from_observation( + observation: observation, + admission_seal: behavioral_admission_seal_unminted + ) +} + +fn admit_behavioral_comparison( + observation: BehavioralComparisonObservation +) -> BehavioralComparisonAdmission { + if !behavioral_comparison_rows_nonempty(rows: observation.comparison_rows) { + BehaviorExecutionRefused { + cause: ^behavioral_comparison_empty_rows, + receipt: behavioral_comparison_receipt_unminted_from_observation( + observation: observation + ) + } + } else if behavioral_comparison_all_rows_equivalent(rows: observation.comparison_rows) + && observation.exit_success + && behavioral_comparison_verdict_is_equivalent(stdout: observation.stdout) { + AdmittedBehaviorEquivalent { + admitted: AdmittedBehaviorEquivalentReceipt { + receipt: behavioral_comparison_receipt_from_observation( + observation: observation, + admission_seal: behavioral_admission_seal_for_observation( + observation: observation + ) + ) + } + } + } else if behavioral_comparison_verdict_is_diverged(stdout: observation.stdout) { + BehaviorDiverged { + receipt: behavioral_comparison_receipt_unminted_from_observation( + observation: observation + ), + differences: behavioral_comparison_differences_from_rows( + rows: observation.comparison_rows + ) + } + } else if !observation.exit_success { + BehaviorExecutionRefused { + cause: ^behavioral_comparison_execution_failed, + receipt: behavioral_comparison_receipt_unminted_from_observation( + observation: observation + ) + } + } else { + BehaviorExecutionRefused { + cause: ^behavioral_comparison_stdout_unbound, + receipt: behavioral_comparison_receipt_unminted_from_observation( + observation: observation + ) + } + } +} + +fn admit_behavioral_comparison_equivalent( + observation: BehavioralComparisonObservation +) -> Optional { + match admit_behavioral_comparison(observation: observation) { + AdmittedBehaviorEquivalent { admitted } => optional_present(value: admitted) + BehaviorDiverged { receipt: _, differences: _ } => optional_absent() + BehaviorExecutionRefused { cause: _, receipt: _ } => optional_absent() + } +} + +fn behavioral_admission_seal_is_minted(admitted: AdmittedBehaviorEquivalentReceipt) -> Bool { + admitted.receipt.admission_seal != behavioral_admission_seal_unminted +} + +fn admitted_behavioral_comparison_receipt_matches_binding( + admitted: AdmittedBehaviorEquivalentReceipt, + module_path: String, + emitted_source: Medium, + subject_binding_identity: Hash, + executable_content: String, + head_sha: CommitSha, + expected_behavioral_probe_entry: String, + expected_behavioral_probe_function: String +) -> Bool { + let receipt = admitted.receipt + let expected_subject = BehavioralComparisonSubject { + module_path: module_path, + emitted_source_identity: emitted_source_identity_for_medium(source: emitted_source), + subject_binding_identity: subject_binding_identity, + executable_identity: executable_identity_for_content(content: executable_content) + } + behavioral_admission_seal_is_minted(admitted: admitted) + && (receipt.subject.module_path == expected_subject.module_path) + && (receipt.subject.emitted_source_identity == expected_subject.emitted_source_identity) + && (receipt.subject.subject_binding_identity == expected_subject.subject_binding_identity) + && (receipt.subject.executable_identity == expected_subject.executable_identity) + && behavioral_comparison_all_rows_equivalent(rows: receipt.comparison_rows) + && behavioral_comparison_verdict_is_equivalent(stdout: receipt.stdout) + && receipt.exit_success + && (receipt.head_sha == head_sha) + && (receipt.behavioral_probe_entry == expected_behavioral_probe_entry) + && (receipt.behavioral_probe_function == expected_behavioral_probe_function) +} diff --git a/src/v2/compiler/self_host/direct_rust_door_behavioral_stdout.dag b/src/v2/compiler/self_host/direct_rust_door_behavioral_stdout.dag new file mode 100644 index 00000000000..604a4c22fc9 --- /dev/null +++ b/src/v2/compiler/self_host/direct_rust_door_behavioral_stdout.dag @@ -0,0 +1,220 @@ +module v2.compiler.self_host.direct_rust_door_behavioral_stdout + +import v2.compiler.self_host.behavioral_comparison_receipt { + BehavioralComparisonRow, + behavioral_comparison_verdict_is_diverged, + behavioral_comparison_verdict_is_equivalent +} +import std.algebra { Cons, Empty } +import v2.std.collection { List } +import v2.std.logic { Bool } +import v2.std.optional { Absent, Present, optional_absent, optional_present } +import v2.std.text { String } + +data direct_rust_door_behavioral_stdout_note: String = "Direct-door add fixture stdout parser (still-bat-561 recut): fixture-specific BEHAVIORAL_CASE / BEHAVIORAL_VERDICT patterns and row extraction live here, not in behavioral_comparison_receipt." + +data direct_rust_door_equivalent_stdout_text: String = "BEHAVIORAL_CASE x=2 y=3 call_x=2 expected=5 actual=5 seed=5 ok=true\nBEHAVIORAL_CASE x=0 y=0 call_x=0 expected=0 actual=0 seed=0 ok=true\nBEHAVIORAL_CASE x=-1 y=1 call_x=-1 expected=0 actual=0 seed=0 ok=true\nBEHAVIORAL_CASE x=100 y=-50 call_x=100 expected=50 actual=50 seed=50 ok=true\nBEHAVIORAL_VERDICT: EQUIVALENT" + +fn direct_rust_door_pass_stdout_holds(stdout: String) -> Bool { + string_contains( + s: stdout, + pattern: "BEHAVIORAL_CASE x=2 y=3 call_x=2 expected=5 actual=5 seed=5 ok=true" + ) + && string_contains( + s: stdout, + pattern: "BEHAVIORAL_CASE x=0 y=0 call_x=0 expected=0 actual=0 seed=0 ok=true" + ) + && string_contains( + s: stdout, + pattern: "BEHAVIORAL_CASE x=-1 y=1 call_x=-1 expected=0 actual=0 seed=0 ok=true" + ) + && string_contains( + s: stdout, + pattern: "BEHAVIORAL_CASE x=100 y=-50 call_x=100 expected=50 actual=50 seed=50 ok=true" + ) + && behavioral_comparison_verdict_is_equivalent(stdout: stdout) +} + +fn direct_rust_door_inject_fault_stdout_holds(stdout: String) -> Bool { + behavioral_comparison_verdict_is_diverged(stdout: stdout) + && string_contains( + s: stdout, + pattern: "BEHAVIORAL_CASE x=2 y=3 call_x=3 expected=5 actual=6 seed=6 ok=false" + ) +} + +fn direct_rust_door_subtract_stdout_holds(stdout: String) -> Bool { + behavioral_comparison_verdict_is_diverged(stdout: stdout) + && string_contains( + s: stdout, + pattern: "BEHAVIORAL_CASE x=2 y=3 call_x=2 expected=5 actual=-1 seed=5 ok=false" + ) +} + +fn direct_rust_door_pass_stdout_derived_rows() -> List { + Cons { + head: BehavioralComparisonRow { + corpus_x: 2, + corpus_y: 3, + call_x: 2, + expected: 5, + actual: 5, + seed: 5, + ok: true + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: 0, + corpus_y: 0, + call_x: 0, + expected: 0, + actual: 0, + seed: 0, + ok: true + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: -1, + corpus_y: 1, + call_x: -1, + expected: 0, + actual: 0, + seed: 0, + ok: true + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: 100, + corpus_y: -50, + call_x: 100, + expected: 50, + actual: 50, + seed: 50, + ok: true + }, + tail: Empty + } + } + } + } +} + +fn direct_rust_door_inject_fault_stdout_derived_rows() -> List { + Cons { + head: BehavioralComparisonRow { + corpus_x: 2, + corpus_y: 3, + call_x: 3, + expected: 5, + actual: 6, + seed: 6, + ok: false + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: 0, + corpus_y: 0, + call_x: 0, + expected: 0, + actual: 0, + seed: 0, + ok: true + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: -1, + corpus_y: 1, + call_x: -1, + expected: 0, + actual: 0, + seed: 0, + ok: true + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: 100, + corpus_y: -50, + call_x: 100, + expected: 50, + actual: 50, + seed: 50, + ok: true + }, + tail: Empty + } + } + } + } +} + +fn direct_rust_door_subtract_stdout_derived_rows() -> List { + Cons { + head: BehavioralComparisonRow { + corpus_x: 2, + corpus_y: 3, + call_x: 2, + expected: 5, + actual: -1, + seed: 5, + ok: false + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: 0, + corpus_y: 0, + call_x: 0, + expected: 0, + actual: 0, + seed: 0, + ok: true + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: -1, + corpus_y: 1, + call_x: -1, + expected: 0, + actual: 0, + seed: 0, + ok: true + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: 100, + corpus_y: -50, + call_x: 100, + expected: 50, + actual: 50, + seed: 50, + ok: true + }, + tail: Empty + } + } + } + } +} + +fn direct_rust_door_parse_pass_rows_from_stdout(stdout: String) -> Optional> { + if direct_rust_door_pass_stdout_holds(stdout: stdout) { + optional_present(value: direct_rust_door_pass_stdout_derived_rows()) + } else { + optional_absent() + } +} + +fn direct_rust_door_parse_inject_fault_rows_from_stdout(stdout: String) -> Optional> { + if direct_rust_door_inject_fault_stdout_holds(stdout: stdout) { + optional_present(value: direct_rust_door_inject_fault_stdout_derived_rows()) + } else { + optional_absent() + } +} + +fn direct_rust_door_parse_subtract_rows_from_stdout(stdout: String) -> Optional> { + if direct_rust_door_subtract_stdout_holds(stdout: stdout) { + optional_present(value: direct_rust_door_subtract_stdout_derived_rows()) + } else { + optional_absent() + } +} diff --git a/src/v2/compiler/self_host/direct_rust_door_fixture.dag b/src/v2/compiler/self_host/direct_rust_door_fixture.dag index 6dbe6b092dd..65825d66dc2 100644 --- a/src/v2/compiler/self_host/direct_rust_door_fixture.dag +++ b/src/v2/compiler/self_host/direct_rust_door_fixture.dag @@ -43,7 +43,11 @@ import v2.std.optional { optional_present } import v2.std.node { Node } +import v2.std.collection { List } +import v2.std.logic { Bool } import v2.std.text { String } +import v2.std.node { Hash, symbol_identity_digest } +import v2.compiler.self_host.behavioral_comparison_receipt { BehavioralComparisonRow } import v2.std.witness { Holds, StructuralPropertyWitness, @@ -57,6 +61,183 @@ data direct_rust_door_module_path: String = "src/v2/compiler/self_host/direct_ru data direct_rust_door_expected_source: String = rust_source_text +data direct_rust_door_divergent_rust_source: String = "fn add(x: i32, y: i32) -> i32 { x - y }" + +data direct_rust_door_behavioral_corpus_note: String = "Lane 4 discriminating corpus authority (DESIGN section 7): behavioral equivalence to add_probe semantics (x+y), not byte agreement with v1.compiler.emit_rust. The witness driver compares emitted add against a seed_add reference oracle on multiple input pairs; --inject-fault perturbs one call so the comparison must fail. comparison_rows in the typed receipt are admitted only after stdout carries the matching BEHAVIORAL_CASE lines for this corpus." + +data direct_rust_door_behavioral_corpus_revision: String = "direct_rust_door_corpus_v1" + +data direct_rust_door_behavioral_probe_entry: String = "dag/test/claim/direct_rust_door_behavioral_qualification_witness_test.dag" + +data direct_rust_door_behavioral_probe_function: String = "direct_rust_door_behavioral_qualification_holds" + +fn direct_rust_door_behavioral_corpus_identity() -> Hash { + symbol_identity_digest(sym: ^direct_rust_door_corpus_v1) +} + +fn direct_rust_door_behavioral_corpus_rows() -> List { + Cons { + head: BehavioralComparisonRow { + corpus_x: 2, + corpus_y: 3, + call_x: 2, + expected: 5, + actual: 5, + seed: 5, + ok: true + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: 0, + corpus_y: 0, + call_x: 0, + expected: 0, + actual: 0, + seed: 0, + ok: true + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: -1, + corpus_y: 1, + call_x: -1, + expected: 0, + actual: 0, + seed: 0, + ok: true + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: 100, + corpus_y: -50, + call_x: 100, + expected: 50, + actual: 50, + seed: 50, + ok: true + }, + tail: Empty + } + } + } + } +} + +fn direct_rust_door_inject_fault_divergence_row() -> BehavioralComparisonRow { + BehavioralComparisonRow { + corpus_x: 2, + corpus_y: 3, + call_x: 3, + expected: 5, + actual: 6, + seed: 6, + ok: false + } +} + +fn direct_rust_door_inject_fault_comparison_rows() -> List { + Cons { + head: direct_rust_door_inject_fault_divergence_row(), + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: 0, + corpus_y: 0, + call_x: 0, + expected: 0, + actual: 0, + seed: 0, + ok: true + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: -1, + corpus_y: 1, + call_x: -1, + expected: 0, + actual: 0, + seed: 0, + ok: true + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: 100, + corpus_y: -50, + call_x: 100, + expected: 50, + actual: 50, + seed: 50, + ok: true + }, + tail: Empty + } + } + } + } +} + +fn direct_rust_door_subtract_divergence_row() -> BehavioralComparisonRow { + BehavioralComparisonRow { + corpus_x: 2, + corpus_y: 3, + call_x: 2, + expected: 5, + actual: -1, + seed: 5, + ok: false + } +} + +fn direct_rust_door_subtract_comparison_rows() -> List { + Cons { + head: direct_rust_door_subtract_divergence_row(), + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: 0, + corpus_y: 0, + call_x: 0, + expected: 0, + actual: 0, + seed: 0, + ok: true + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: -1, + corpus_y: 1, + call_x: -1, + expected: 0, + actual: 0, + seed: 0, + ok: true + }, + tail: Cons { + head: BehavioralComparisonRow { + corpus_x: 100, + corpus_y: -50, + call_x: 100, + expected: 50, + actual: 50, + seed: 50, + ok: true + }, + tail: Empty + } + } + } + } +} + +fn direct_rust_door_behavioral_witness_bin_rel_path() -> String { + "target/release/witness" +} + +fn direct_rust_door_behavioral_witness_bin_path(workspace_dir: String) -> String { + concat( + workspace_dir, + concat("/", direct_rust_door_behavioral_witness_bin_rel_path()) + ) +} + data direct_rust_door_dag_module_source: String = "module add_probe\n\nfn add(x: Int, y: Int) -> Int { x + y }\n" data direct_rust_door_ingest_artifact: Artifact = Artifact { diff --git a/src/v2/compiler/self_host/fixture_synthetic_emission.dag b/src/v2/compiler/self_host/fixture_synthetic_emission.dag index 02ba991f991..5f5a437d86b 100644 --- a/src/v2/compiler/self_host/fixture_synthetic_emission.dag +++ b/src/v2/compiler/self_host/fixture_synthetic_emission.dag @@ -3,6 +3,11 @@ module v2.compiler.self_host.fixture_synthetic_emission import std.content_hash { content_hash_atom } import extdeps.communication.medium { Medium } import v2.compiler.infer { InferredTree } +import v2.compiler.self_host.behavioral_comparison_receipt { + AdmittedBehaviorEquivalentReceipt, + admitted_behavioral_comparison_receipt_matches_binding, + emitted_source_identity_for_medium +} import v2.compiler.self_host.candidate_generation { generate_rust_emission_candidate, RustWorkspaceWriteReceipt, @@ -22,10 +27,11 @@ import v2.std.logic { Bool } import v2.std.node { Hash, Node, combine_hash, symbol_identity_digest } import v2.std.optional { Absent, Present, optional_absent, optional_present } import v2.std.text { String } +import std.types { CommitSha } -data fixture_synthetic_emission_note: String = "Parallel fixture-scoped emission authority (wise-ram-22 disposition PR1 containment): SyntheticEmittedArtifact / FixtureBehaviorReceipt carry FixtureEmissionQualification only — no constructor into ProducerEmissionReceipt or production EmissionQualification." +data fixture_synthetic_emission_note: String = "Parallel fixture-scoped emission authority (royal-crab-235 disposition 2, wise-ram-22 ruling): SyntheticEmittedArtifact / FixtureBehaviorReceipt carry fixture qualifications only — no constructor into ProducerEmissionReceipt or EmissionQualification, so fixture mint cannot reach the production frontier by mistake." -data fixture_synthetic_emission_dissolution_trigger: String = "dissolve-on disposition 1 (wise-ram-22 containment lane): real source-ingest qualification after infer(assemble(fixture ingest)) accepts without hand-authored DerivedGrounding. When that path greens, fixture mint on direct_rust_door_inferred_tree deletes and production ProvenancedRustArtifact subsumes the subject." +data fixture_synthetic_emission_dissolution_trigger: String = "dissolve-on disposition 1 (wise-ram-22 containment lane): real source-ingest behavioral qualification — generate_written_rust_candidate_from_ingest mints ProvenancedRustArtifact with production BehavioralEquivalent after infer(assemble(fixture ingest)) accepts without hand-authored DerivedGrounding. When that path greens, this module's fixture ladder, wet transport mints on direct_rust_door_inferred_tree, and FixtureBehaviorallyEquivalent delete together; production BehavioralEquivalent subsumes the behavioral receipt machinery for the direct-door subject." type FixtureEmissionQualification = FixtureSourceProduced @@ -35,7 +41,8 @@ type FixtureEmissionQualification type FixtureBehaviorReceipt { module_path: String emitted_source_identity: Hash - fixture_lane_tag: String + behavioral_probe_entry: String + behavioral_probe_function: String qualifications: List build_green: Bool } @@ -60,9 +67,11 @@ data fixture_cargo_green_qualifications: List = [ FixtureCargoGreen ] -fn fixture_emitted_source_identity_for_medium(source: Medium) -> Hash { - content_hash_atom(value: source.carried) -} +data fixture_behaviorally_equivalent_qualifications: List = [ + FixtureSourceProduced, + FixtureCargoGreen, + FixtureBehaviorallyEquivalent +] fn fixture_emission_qualification_eq( left: FixtureEmissionQualification, @@ -102,17 +111,33 @@ fn fixture_emission_qualifications_list_contains( ) } +fn fixture_behavior_receipt_identity_for(receipt: FixtureBehaviorReceipt) -> Hash { + combine_hash( + a: symbol_identity_digest(sym: ^fixture_behavior_receipt_identity), + b: combine_hash( + a: content_hash_atom(value: receipt.module_path), + b: combine_hash( + a: receipt.emitted_source_identity, + b: combine_hash( + a: content_hash_atom(value: receipt.behavioral_probe_entry), + b: content_hash_atom(value: receipt.behavioral_probe_function) + ) + ) + ) + ) +} + fn mint_fixture_behavior_receipt( module_path: String, emitted_source: Medium, - fixture_lane_tag: String + behavioral_probe_entry: String, + behavioral_probe_function: String ) -> FixtureBehaviorReceipt { FixtureBehaviorReceipt { module_path: module_path, - emitted_source_identity: fixture_emitted_source_identity_for_medium( - source: emitted_source - ), - fixture_lane_tag: fixture_lane_tag, + emitted_source_identity: emitted_source_identity_for_medium(source: emitted_source), + behavioral_probe_entry: behavioral_probe_entry, + behavioral_probe_function: behavioral_probe_function, qualifications: fixture_source_produced_qualifications, build_green: false } @@ -135,6 +160,20 @@ fn fixture_behavior_receipt_admits_cargo_green_advance( ) } +fn fixture_behavior_receipt_admits_behaviorally_equivalent_advance( + receipt: FixtureBehaviorReceipt +) -> Bool { + receipt.build_green + && fixture_emission_qualifications_list_contains( + xs: receipt.qualifications, + wanted: FixtureCargoGreen + ) + && !fixture_emission_qualifications_list_contains( + xs: receipt.qualifications, + wanted: FixtureBehaviorallyEquivalent + ) +} + fn advance_fixture_behavior_receipt_cargo_green( prior: FixtureBehaviorReceipt, cargo_green: Bool @@ -147,7 +186,8 @@ fn advance_fixture_behavior_receipt_cargo_green( value: FixtureBehaviorReceipt { module_path: prior.module_path, emitted_source_identity: prior.emitted_source_identity, - fixture_lane_tag: prior.fixture_lane_tag, + behavioral_probe_entry: prior.behavioral_probe_entry, + behavioral_probe_function: prior.behavioral_probe_function, qualifications: fixture_cargo_green_qualifications, build_green: true } @@ -155,11 +195,33 @@ fn advance_fixture_behavior_receipt_cargo_green( } } +fn advance_fixture_behavior_receipt_behaviorally_equivalent( + prior: FixtureBehaviorReceipt, + behavioral_probe_entry: String, + behavioral_probe_function: String +) -> Optional { + if !fixture_behavior_receipt_admits_behaviorally_equivalent_advance(receipt: prior) { + optional_absent() + } else { + optional_present( + value: FixtureBehaviorReceipt { + module_path: prior.module_path, + emitted_source_identity: prior.emitted_source_identity, + behavioral_probe_entry: behavioral_probe_entry, + behavioral_probe_function: behavioral_probe_function, + qualifications: fixture_behaviorally_equivalent_qualifications, + build_green: true + } + ) + } +} + fn mint_synthetic_emitted_artifact_from_fixture_inferred( inferred: InferredTree, target: TargetModel, module_path: String, - fixture_lane_tag: String + behavioral_probe_entry: String, + behavioral_probe_function: String ) -> Outcome { bind_outcome( o: generate_rust_emission_candidate(inferred: inferred, target: target), @@ -171,7 +233,8 @@ fn mint_synthetic_emitted_artifact_from_fixture_inferred( fixture_receipt: mint_fixture_behavior_receipt( module_path: module_path, emitted_source: candidate.source, - fixture_lane_tag: fixture_lane_tag + behavioral_probe_entry: behavioral_probe_entry, + behavioral_probe_function: behavioral_probe_function ) } ) @@ -184,14 +247,16 @@ fn mint_written_synthetic_emitted_artifact_from_fixture_inferred( target: TargetModel, module_path: String, workspace_dir: String, - fixture_lane_tag: String + behavioral_probe_entry: String, + behavioral_probe_function: String ) -> Outcome { bind_outcome( o: mint_synthetic_emitted_artifact_from_fixture_inferred( inferred: inferred, target: target, module_path: module_path, - fixture_lane_tag: fixture_lane_tag + behavioral_probe_entry: behavioral_probe_entry, + behavioral_probe_function: behavioral_probe_function ), f: fn(artifact) { outcome_accepted( @@ -230,6 +295,54 @@ fn advance_written_synthetic_emitted_artifact_cargo_green( } } +data advance_written_synthetic_emitted_artifact_fixture_behaviorally_equivalent_note: String = "Fixture ladder terminal (disposition 2): FixtureBehaviorallyEquivalent minted ONLY from AdmittedBehaviorEquivalentReceipt after FixtureCargoGreen, with binding identity and probe/head checked against the written synthetic artifact — never production BehavioralEquivalent." + +fn advance_written_synthetic_emitted_artifact_fixture_behaviorally_equivalent( + written: WrittenSyntheticEmittedArtifact, + admitted: AdmittedBehaviorEquivalentReceipt, + executable_content: String, + head_sha: CommitSha, + expected_behavioral_probe_entry: String, + expected_behavioral_probe_function: String +) -> Optional { + if !written_synthetic_emitted_artifact_has_fixture_cargo_green_qualification( + written: written + ) + || !admitted_behavioral_comparison_receipt_matches_binding( + admitted: admitted, + module_path: written.artifact.fixture_receipt.module_path, + emitted_source: written.artifact.source, + subject_binding_identity: fixture_behavior_receipt_identity_for( + receipt: written.artifact.fixture_receipt + ), + executable_content: executable_content, + head_sha: head_sha, + expected_behavioral_probe_entry: expected_behavioral_probe_entry, + expected_behavioral_probe_function: expected_behavioral_probe_function + ) { + optional_absent() + } else { + match advance_fixture_behavior_receipt_behaviorally_equivalent( + prior: written.artifact.fixture_receipt, + behavioral_probe_entry: expected_behavioral_probe_entry, + behavioral_probe_function: expected_behavioral_probe_function + ) { + Present { value: receipt } => + optional_present( + value: WrittenSyntheticEmittedArtifact { + artifact: SyntheticEmittedArtifact { + source: written.artifact.source, + emitted: written.artifact.emitted, + fixture_receipt: receipt + }, + write: written.write + } + ) + Absent => optional_absent() + } + } +} + fn written_synthetic_emitted_artifact_ok( written: WrittenSyntheticEmittedArtifact ) -> Bool { @@ -253,20 +366,3 @@ fn written_synthetic_emitted_artifact_has_fixture_behaviorally_equivalent_qualif wanted: FixtureBehaviorallyEquivalent ) } - -fn synthetic_emitted_artifact_has_fixture_source_produced_only( - artifact: SyntheticEmittedArtifact -) -> Bool { - fixture_emission_qualifications_list_contains( - xs: artifact.fixture_receipt.qualifications, - wanted: FixtureSourceProduced - ) - && !fixture_emission_qualifications_list_contains( - xs: artifact.fixture_receipt.qualifications, - wanted: FixtureCargoGreen - ) - && !fixture_emission_qualifications_list_contains( - xs: artifact.fixture_receipt.qualifications, - wanted: FixtureBehaviorallyEquivalent - ) -} diff --git a/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag b/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag new file mode 100644 index 00000000000..5c6b689cd60 --- /dev/null +++ b/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag @@ -0,0 +1,398 @@ +module v2.test.claim.self_host.direct_rust_door_qualification_witness_test + +import v2.std.algebra { Empty } +import v2.compiler.self_host.behavioral_comparison_receipt { + AdmittedBehaviorEquivalentReceipt, + BehavioralComparisonObservation, + BehavioralComparisonReceipt, + admit_behavioral_comparison_equivalent, + behavioral_admission_seal_for_observation, + behavioral_admission_seal_unminted, + behavioral_comparison_execution_identity, + behavioral_comparison_receipt_from_observation, + behavioral_comparison_subject_for_observation +} +import v2.compiler.self_host.direct_rust_door_behavioral_stdout { + direct_rust_door_equivalent_stdout_text, + direct_rust_door_parse_pass_rows_from_stdout +} +import v2.compiler.self_host.fixture_synthetic_emission { + advance_written_synthetic_emitted_artifact_cargo_green, + advance_written_synthetic_emitted_artifact_fixture_behaviorally_equivalent, + fixture_behavior_receipt_identity_for, + mint_synthetic_emitted_artifact_from_fixture_inferred, + SyntheticEmittedArtifact, + WrittenSyntheticEmittedArtifact, + written_synthetic_emitted_artifact_has_fixture_behaviorally_equivalent_qualification, + written_synthetic_emitted_artifact_has_fixture_cargo_green_qualification, + written_synthetic_emitted_artifact_ok +} +import v2.compiler.self_host.candidate_generation { RustWorkspaceWriteReceipt } +import v2.compiler.self_host.direct_rust_door_fixture { + direct_rust_door_behavioral_corpus_identity, + direct_rust_door_behavioral_probe_entry, + direct_rust_door_behavioral_probe_function, + direct_rust_door_inferred_tree, + direct_rust_door_module_path, + direct_rust_door_subtract_comparison_rows, + direct_rust_door_target_model +} +import v2.std.diagnostic { Accepted, Rejected } +import v2.std.logic { Bool } +import v2.std.optional { Absent, Present, Optional, optional_absent, optional_present } +import v2.std.text { String } + +data direct_rust_door_qualification_witness_note: String = "Lane 4 fast per-PR construction witnesses (still-bat-561): fixture ladder only. Sentinel RED: unminted admission_seal refuses. Derived-seal RED (ceiling): behavioral_admission_seal_for_observation on a matching authored observation forges a valid seal and advance succeeds — the seal is a checksum, not execution proof. Honest ceiling documented in behavioral_admission_seal_ceiling_note." + +data direct_rust_door_qualification_fixture_workspace: String = "hermetic_fixture/direct_rust_door_qualification" + +data direct_rust_door_qualification_fixture_head_sha: String = "0000000000000000000000000000000000000000" + +data direct_rust_door_qualification_fixture_executable: String = "hermetic_fixture_executable_bytes" + +fn direct_rust_door_qualification_written_from_synthetic( + artifact: SyntheticEmittedArtifact +) -> WrittenSyntheticEmittedArtifact { + WrittenSyntheticEmittedArtifact { + artifact: artifact, + write: RustWorkspaceWriteReceipt { + workspace_dir: direct_rust_door_qualification_fixture_workspace, + manifest_path: concat( + direct_rust_door_qualification_fixture_workspace, + "/Cargo.toml" + ), + main_rs_path: concat( + direct_rust_door_qualification_fixture_workspace, + "/src/lib.rs" + ), + manifest_write_ok: true, + main_write_ok: true + } + } +} + +fn direct_rust_door_fully_matching_observation( + written: WrittenSyntheticEmittedArtifact +) -> BehavioralComparisonObservation { + let stdout = direct_rust_door_equivalent_stdout_text + match direct_rust_door_parse_pass_rows_from_stdout(stdout: stdout) { + Present { value: comparison_rows } => + BehavioralComparisonObservation { + module_path: written.artifact.fixture_receipt.module_path, + emitted_source: written.artifact.source, + subject_binding_identity: fixture_behavior_receipt_identity_for( + receipt: written.artifact.fixture_receipt + ), + executable_content: direct_rust_door_qualification_fixture_executable, + stdout: stdout, + stderr: "", + exit_success: true, + head_sha: direct_rust_door_qualification_fixture_head_sha, + corpus_identity: direct_rust_door_behavioral_corpus_identity(), + comparison_rows: comparison_rows, + behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + behavioral_probe_function: direct_rust_door_behavioral_probe_function + } + Absent => + BehavioralComparisonObservation { + module_path: written.artifact.fixture_receipt.module_path, + emitted_source: written.artifact.source, + subject_binding_identity: fixture_behavior_receipt_identity_for( + receipt: written.artifact.fixture_receipt + ), + executable_content: direct_rust_door_qualification_fixture_executable, + stdout: stdout, + stderr: "", + exit_success: true, + head_sha: direct_rust_door_qualification_fixture_head_sha, + corpus_identity: direct_rust_door_behavioral_corpus_identity(), + comparison_rows: Empty, + behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + behavioral_probe_function: direct_rust_door_behavioral_probe_function + } + } +} + +fn direct_rust_door_fully_matching_counterfeit_admitted( + written: WrittenSyntheticEmittedArtifact +) -> AdmittedBehaviorEquivalentReceipt { + let observation = direct_rust_door_fully_matching_observation(written: written) + let subject = behavioral_comparison_subject_for_observation(observation: observation) + AdmittedBehaviorEquivalentReceipt { + receipt: BehavioralComparisonReceipt { + subject: subject, + corpus_identity: direct_rust_door_behavioral_corpus_identity(), + comparison_rows: observation.comparison_rows, + stdout: observation.stdout, + stderr: observation.stderr, + exit_success: observation.exit_success, + execution_identity: behavioral_comparison_execution_identity( + stdout: observation.stdout, + stderr: observation.stderr, + exit_success: observation.exit_success + ), + head_sha: direct_rust_door_qualification_fixture_head_sha, + behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + behavioral_probe_function: direct_rust_door_behavioral_probe_function, + admission_seal: behavioral_admission_seal_unminted + } + } +} + +fn direct_rust_door_admitted_from_fully_matching_observation( + written: WrittenSyntheticEmittedArtifact +) -> Optional { + admit_behavioral_comparison_equivalent( + observation: direct_rust_door_fully_matching_observation(written: written) + ) +} + +fn direct_rust_door_derived_seal_forgery_admitted( + written: WrittenSyntheticEmittedArtifact +) -> AdmittedBehaviorEquivalentReceipt { + let observation = direct_rust_door_fully_matching_observation(written: written) + AdmittedBehaviorEquivalentReceipt { + receipt: behavioral_comparison_receipt_from_observation( + observation: observation, + admission_seal: behavioral_admission_seal_for_observation( + observation: observation + ) + ) + } +} + +test fn fully_matching_derived_seal_forgery_advance_succeeds_red() -> Bool { + match mint_synthetic_emitted_artifact_from_fixture_inferred( + inferred: direct_rust_door_inferred_tree, + target: direct_rust_door_target_model(), + module_path: direct_rust_door_module_path, + behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + behavioral_probe_function: direct_rust_door_behavioral_probe_function + ) { + Accepted { value: artifact, diagnostics: _ } => + let written = direct_rust_door_qualification_written_from_synthetic( + artifact: artifact + ) + match advance_written_synthetic_emitted_artifact_cargo_green( + written: written, + cargo_green: true + ) { + Present { value: cargo_written } => + let forged = direct_rust_door_derived_seal_forgery_admitted( + written: cargo_written + ) + match advance_written_synthetic_emitted_artifact_fixture_behaviorally_equivalent( + written: cargo_written, + admitted: forged, + executable_content: direct_rust_door_qualification_fixture_executable, + head_sha: direct_rust_door_qualification_fixture_head_sha, + expected_behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + expected_behavioral_probe_function: direct_rust_door_behavioral_probe_function + ) { + Present { value: behavioral_written } => + written_synthetic_emitted_artifact_has_fixture_behaviorally_equivalent_qualification( + written: behavioral_written + ) + Absent => false + } + Absent => false + } + Rejected { diagnostics: _ } => false + } +} + +test fn fully_matching_counterfeit_without_admission_seal_advance_refuses() -> Bool { + match mint_synthetic_emitted_artifact_from_fixture_inferred( + inferred: direct_rust_door_inferred_tree, + target: direct_rust_door_target_model(), + module_path: direct_rust_door_module_path, + behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + behavioral_probe_function: direct_rust_door_behavioral_probe_function + ) { + Accepted { value: artifact, diagnostics: _ } => + let written = direct_rust_door_qualification_written_from_synthetic( + artifact: artifact + ) + match advance_written_synthetic_emitted_artifact_cargo_green( + written: written, + cargo_green: true + ) { + Present { value: cargo_written } => + let admit_would_accept = match direct_rust_door_admitted_from_fully_matching_observation( + written: cargo_written + ) { + Present { value: _ } => true + Absent => false + } + let counterfeit = direct_rust_door_fully_matching_counterfeit_admitted( + written: cargo_written + ) + let advance_refused = match advance_written_synthetic_emitted_artifact_fixture_behaviorally_equivalent( + written: cargo_written, + admitted: counterfeit, + executable_content: direct_rust_door_qualification_fixture_executable, + head_sha: direct_rust_door_qualification_fixture_head_sha, + expected_behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + expected_behavioral_probe_function: direct_rust_door_behavioral_probe_function + ) { + Absent => true + Present { value: _ } => false + } + written_synthetic_emitted_artifact_has_fixture_cargo_green_qualification( + written: cargo_written + ) + && admit_would_accept + && advance_refused + Absent => false + } + Rejected { diagnostics: _ } => false + } +} + +test fn witness_behavioral_advance_refuses_without_cargo_green_reds() -> Bool { + match mint_synthetic_emitted_artifact_from_fixture_inferred( + inferred: direct_rust_door_inferred_tree, + target: direct_rust_door_target_model(), + module_path: direct_rust_door_module_path, + behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + behavioral_probe_function: direct_rust_door_behavioral_probe_function + ) { + Accepted { value: artifact, diagnostics: _ } => + let written = direct_rust_door_qualification_written_from_synthetic( + artifact: artifact + ) + let counterfeit = direct_rust_door_fully_matching_counterfeit_admitted( + written: written + ) + !written_synthetic_emitted_artifact_has_fixture_cargo_green_qualification( + written: written + ) + && match advance_written_synthetic_emitted_artifact_fixture_behaviorally_equivalent( + written: written, + admitted: counterfeit, + executable_content: direct_rust_door_qualification_fixture_executable, + head_sha: direct_rust_door_qualification_fixture_head_sha, + expected_behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + expected_behavioral_probe_function: direct_rust_door_behavioral_probe_function + ) { + Absent => true + Present { value: _ } => false + } + Rejected { diagnostics: _ } => false + } +} + +test fn witness_behavioral_advance_refuses_diverged_observation_reds() -> Bool { + match mint_synthetic_emitted_artifact_from_fixture_inferred( + inferred: direct_rust_door_inferred_tree, + target: direct_rust_door_target_model(), + module_path: direct_rust_door_module_path, + behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + behavioral_probe_function: direct_rust_door_behavioral_probe_function + ) { + Accepted { value: artifact, diagnostics: _ } => + let written = direct_rust_door_qualification_written_from_synthetic( + artifact: artifact + ) + match advance_written_synthetic_emitted_artifact_cargo_green( + written: written, + cargo_green: true + ) { + Present { value: cargo_written } => + let diverged_observation = BehavioralComparisonObservation { + module_path: cargo_written.artifact.fixture_receipt.module_path, + emitted_source: cargo_written.artifact.source, + subject_binding_identity: fixture_behavior_receipt_identity_for( + receipt: cargo_written.artifact.fixture_receipt + ), + executable_content: direct_rust_door_qualification_fixture_executable, + stdout: "BEHAVIORAL_VERDICT: DIVERGED", + stderr: "", + exit_success: false, + head_sha: direct_rust_door_qualification_fixture_head_sha, + corpus_identity: direct_rust_door_behavioral_corpus_identity(), + comparison_rows: direct_rust_door_subtract_comparison_rows(), + behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + behavioral_probe_function: direct_rust_door_behavioral_probe_function + } + match admit_behavioral_comparison_equivalent( + observation: diverged_observation + ) { + Absent => true + Present { value: _ } => false + } + Absent => false + } + Rejected { diagnostics: _ } => false + } +} + +test fn witness_behavioral_advance_refuses_mismatched_executable_identity_reds() -> Bool { + match mint_synthetic_emitted_artifact_from_fixture_inferred( + inferred: direct_rust_door_inferred_tree, + target: direct_rust_door_target_model(), + module_path: direct_rust_door_module_path, + behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + behavioral_probe_function: direct_rust_door_behavioral_probe_function + ) { + Accepted { value: artifact, diagnostics: _ } => + let written = direct_rust_door_qualification_written_from_synthetic( + artifact: artifact + ) + match advance_written_synthetic_emitted_artifact_cargo_green( + written: written, + cargo_green: true + ) { + Present { value: cargo_written } => + match direct_rust_door_admitted_from_fully_matching_observation( + written: cargo_written + ) { + Present { value: admitted } => + match advance_written_synthetic_emitted_artifact_fixture_behaviorally_equivalent( + written: cargo_written, + admitted: admitted, + executable_content: "wrong_executable_bytes", + head_sha: direct_rust_door_qualification_fixture_head_sha, + expected_behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + expected_behavioral_probe_function: direct_rust_door_behavioral_probe_function + ) { + Absent => true + Present { value: _ } => false + } + Absent => false + } + Absent => false + } + Rejected { diagnostics: _ } => false + } +} + +test fn witness_cargo_green_advance_does_not_imply_behavioral_equivalent_holds() -> Bool { + match mint_synthetic_emitted_artifact_from_fixture_inferred( + inferred: direct_rust_door_inferred_tree, + target: direct_rust_door_target_model(), + module_path: direct_rust_door_module_path, + behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, + behavioral_probe_function: direct_rust_door_behavioral_probe_function + ) { + Accepted { value: artifact, diagnostics: _ } => + let written = direct_rust_door_qualification_written_from_synthetic( + artifact: artifact + ) + match advance_written_synthetic_emitted_artifact_cargo_green( + written: written, + cargo_green: true + ) { + Present { value: cargo_written } => + written_synthetic_emitted_artifact_ok(written: cargo_written) + && written_synthetic_emitted_artifact_has_fixture_cargo_green_qualification( + written: cargo_written + ) + && !written_synthetic_emitted_artifact_has_fixture_behaviorally_equivalent_qualification( + written: cargo_written + ) + Absent => false + } + Rejected { diagnostics: _ } => false + } +} From c4b8a3e58091ba4ca1b17b96f408945941cb49be Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 16:03:55 +0000 Subject: [PATCH 02/22] Probe sole_constructor on BehavioralComparisonObservation; document ceiling. Cross-module record literals refuse SoleConstructorViolation; mint export with caller-supplied stdout remains the forge path. Ceiling note records executed probe outcome and routes next trigger to host-effect-only mint input at the wet transport boundary. Co-authored-by: Cursor --- dag/tools/direct_rust_door_transport.dag | 7 ++-- .../behavioral_comparison_receipt.dag | 34 +++++++++++++++++-- ...t_rust_door_qualification_witness_test.dag | 17 +++++----- 3 files changed, 45 insertions(+), 13 deletions(-) diff --git a/dag/tools/direct_rust_door_transport.dag b/dag/tools/direct_rust_door_transport.dag index dd3787e3d0e..cb65ba735d2 100644 --- a/dag/tools/direct_rust_door_transport.dag +++ b/dag/tools/direct_rust_door_transport.dag @@ -14,7 +14,8 @@ import v2.compiler.self_host.behavioral_comparison_receipt { BehavioralComparisonRow, BehaviorDiverged, admit_behavioral_comparison, - admit_behavioral_comparison_equivalent + admit_behavioral_comparison_equivalent, + mint_behavioral_comparison_observation } import v2.compiler.self_host.direct_rust_door_behavioral_stdout { direct_rust_door_inject_fault_stdout_holds, @@ -67,7 +68,7 @@ fn direct_rust_door_behavioral_observation_from_run( comparison_rows: List, executable_content: String ) -> BehavioralComparisonObservation { - BehavioralComparisonObservation { + mint_behavioral_comparison_observation( module_path: written.artifact.fixture_receipt.module_path, emitted_source: written.artifact.source, subject_binding_identity: fixture_behavior_receipt_identity_for( @@ -82,7 +83,7 @@ fn direct_rust_door_behavioral_observation_from_run( comparison_rows: comparison_rows, behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, behavioral_probe_function: direct_rust_door_behavioral_probe_function - } + ) } fn direct_rust_door_prepare_behavioral_witness_workspace(workspace_dir: String) -> Bool { diff --git a/src/v2/compiler/self_host/behavioral_comparison_receipt.dag b/src/v2/compiler/self_host/behavioral_comparison_receipt.dag index 287ac354ae5..bb6c98441aa 100644 --- a/src/v2/compiler/self_host/behavioral_comparison_receipt.dag +++ b/src/v2/compiler/self_host/behavioral_comparison_receipt.dag @@ -12,7 +12,7 @@ import std.types { CommitSha, Int } data behavioral_comparison_receipt_note: String = "Executed behavioral comparison receipt carrier (still-bat-561 ceiling audit): rows and verdict are derived from stdout at observation construction. advance checks field binding against the written artifact — NOT that stdout came from a real process." -data behavioral_admission_seal_ceiling_note: String = "CEILING (still-bat-561): admission_seal is a pure digest of caller-supplied observation fields — behavioral_admission_seal_for_observation(observation) is reachable from any module and authenticates nothing. behavioral_admission_seal_is_minted is a not-equal-to-sentinel test only. A matching counterfeit with derived seal passes advance; witness fully_matching_derived_seal_forgery_advance_succeeds_red records that gap. Unforgeable execution witness requires observation construction walled to the wet transport host-effect path (sole_constructor on BehavioralComparisonObservation with mint reachable only from process output, or equivalent) — not expressible as a derived post-hoc seal today; sole_constructor completeness on AdmittedBehaviorEquivalentReceipt alone does not close observation forgery because admit_behavioral_comparison_equivalent(observation) accepts caller-authored observations." +data behavioral_admission_seal_ceiling_note: String = "CEILING probe (still-bat-561 msg_63187749, EXECUTED): admission_seal is a caller-derivable checksum — not execution proof. BehavioralComparisonObservation sole_constructor landed; cross-module record-literal construction is REFUSED (SoleConstructorViolation on probe.behavioral_observation_sole_constructor_probe, construction form: record literal outside v2.compiler.self_host.behavioral_comparison_receipt). LEAK: exported mint_behavioral_comparison_observation — construction form: cross-module function call with caller-supplied stdout/stderr/exit_success/comparison_rows; fully_matching_derived_seal_forgery_advance_succeeds_red still greens via mint + derived seal. Next trigger (reference-edge admission thread): wall mint INPUT with a host-effect-only process-output carrier at the wet transport boundary so witness cannot fabricate stdout. fully_matching_derived_seal_forgery_advance_succeeds_red stays enrolled; flips to refuse when input wall lands, does not retire (DESIGN 4b(4))." type BehavioralComparisonSubject { module_path: String @@ -54,7 +54,7 @@ type BehavioralComparisonReceipt { admission_seal: Hash } -type BehavioralComparisonObservation { +type BehavioralComparisonObservation sole_constructor { module_path: String emitted_source: Medium subject_binding_identity: Hash @@ -69,6 +69,36 @@ type BehavioralComparisonObservation { behavioral_probe_function: String } +fn mint_behavioral_comparison_observation( + module_path: String, + emitted_source: Medium, + subject_binding_identity: Hash, + executable_content: String, + stdout: String, + stderr: String, + exit_success: Bool, + head_sha: CommitSha, + corpus_identity: Hash, + comparison_rows: List, + behavioral_probe_entry: String, + behavioral_probe_function: String +) -> BehavioralComparisonObservation { + BehavioralComparisonObservation { + module_path: module_path, + emitted_source: emitted_source, + subject_binding_identity: subject_binding_identity, + executable_content: executable_content, + stdout: stdout, + stderr: stderr, + exit_success: exit_success, + head_sha: head_sha, + corpus_identity: corpus_identity, + comparison_rows: comparison_rows, + behavioral_probe_entry: behavioral_probe_entry, + behavioral_probe_function: behavioral_probe_function + } +} + type AdmittedBehaviorEquivalentReceipt { receipt: BehavioralComparisonReceipt } diff --git a/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag b/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag index 5c6b689cd60..9c8b8e1de1e 100644 --- a/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag +++ b/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag @@ -10,7 +10,8 @@ import v2.compiler.self_host.behavioral_comparison_receipt { behavioral_admission_seal_unminted, behavioral_comparison_execution_identity, behavioral_comparison_receipt_from_observation, - behavioral_comparison_subject_for_observation + behavioral_comparison_subject_for_observation, + mint_behavioral_comparison_observation } import v2.compiler.self_host.direct_rust_door_behavioral_stdout { direct_rust_door_equivalent_stdout_text, @@ -42,7 +43,7 @@ import v2.std.logic { Bool } import v2.std.optional { Absent, Present, Optional, optional_absent, optional_present } import v2.std.text { String } -data direct_rust_door_qualification_witness_note: String = "Lane 4 fast per-PR construction witnesses (still-bat-561): fixture ladder only. Sentinel RED: unminted admission_seal refuses. Derived-seal RED (ceiling): behavioral_admission_seal_for_observation on a matching authored observation forges a valid seal and advance succeeds — the seal is a checksum, not execution proof. Honest ceiling documented in behavioral_admission_seal_ceiling_note." +data direct_rust_door_qualification_witness_note: String = "Lane 4 fast per-PR construction witnesses (still-bat-561): fixture ladder only. sole_constructor on BehavioralComparisonObservation blocks cross-module record literals (SoleConstructorViolation); witnesses route through mint_behavioral_comparison_observation. Sentinel RED: unminted admission_seal refuses. Derived-seal RED (ceiling): mint + behavioral_admission_seal_for_observation forges advance — checksum not witness. Ceiling + next trigger in behavioral_admission_seal_ceiling_note." data direct_rust_door_qualification_fixture_workspace: String = "hermetic_fixture/direct_rust_door_qualification" @@ -77,7 +78,7 @@ fn direct_rust_door_fully_matching_observation( let stdout = direct_rust_door_equivalent_stdout_text match direct_rust_door_parse_pass_rows_from_stdout(stdout: stdout) { Present { value: comparison_rows } => - BehavioralComparisonObservation { + mint_behavioral_comparison_observation( module_path: written.artifact.fixture_receipt.module_path, emitted_source: written.artifact.source, subject_binding_identity: fixture_behavior_receipt_identity_for( @@ -92,9 +93,9 @@ fn direct_rust_door_fully_matching_observation( comparison_rows: comparison_rows, behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, behavioral_probe_function: direct_rust_door_behavioral_probe_function - } + ) Absent => - BehavioralComparisonObservation { + mint_behavioral_comparison_observation( module_path: written.artifact.fixture_receipt.module_path, emitted_source: written.artifact.source, subject_binding_identity: fixture_behavior_receipt_identity_for( @@ -109,7 +110,7 @@ fn direct_rust_door_fully_matching_observation( comparison_rows: Empty, behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, behavioral_probe_function: direct_rust_door_behavioral_probe_function - } + ) } } @@ -299,7 +300,7 @@ test fn witness_behavioral_advance_refuses_diverged_observation_reds() -> Bool { cargo_green: true ) { Present { value: cargo_written } => - let diverged_observation = BehavioralComparisonObservation { + let diverged_observation = mint_behavioral_comparison_observation( module_path: cargo_written.artifact.fixture_receipt.module_path, emitted_source: cargo_written.artifact.source, subject_binding_identity: fixture_behavior_receipt_identity_for( @@ -314,7 +315,7 @@ test fn witness_behavioral_advance_refuses_diverged_observation_reds() -> Bool { comparison_rows: direct_rust_door_subtract_comparison_rows(), behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, behavioral_probe_function: direct_rust_door_behavioral_probe_function - } + ) match admit_behavioral_comparison_equivalent( observation: diverged_observation ) { From e77d560ec466cd8272cb9a0627deec2c9bfb4716 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 16:07:16 +0000 Subject: [PATCH 03/22] File sole_constructor probe on roadmap row; fix next trigger routing. Record literal refused and exported mint call leaking on BehavioralComparisonObservation in gunbc.roadmap_authority unforgeable-construction-capability. Ceiling note routes next step to buildable sole_constructor process-output wall at wet transport (next PR), not parked reference-edge admission. Co-authored-by: Cursor --- dag/gunbc/roadmap_authority.dag | 6 +++--- src/v2/compiler/self_host/behavioral_comparison_receipt.dag | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/dag/gunbc/roadmap_authority.dag b/dag/gunbc/roadmap_authority.dag index 8e35996d0df..fab3fa01707 100644 --- a/dag/gunbc/roadmap_authority.dag +++ b/dag/gunbc/roadmap_authority.dag @@ -2921,10 +2921,10 @@ fn guarantee_ladder_nodes() -> List { volume: VolumeLarge, t: fields( 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 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.", + 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 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. EXECUTED FALSIFICATION RECEIPT (2026-08-04, royal-crab-235, specimen v2.compiler.self_host.behavioral_comparison_receipt BehavioralComparisonObservation): cross-module record literal → SoleConstructorViolation (refused); cross-module exported-function call to mint_behavioral_comparison_observation with caller-supplied stdout/stderr/exit_success/rows → leaks (fully_matching_derived_seal_forgery_advance_succeeds_red greens). Counted audit finding: sole_constructor refuses record-literal construction outside the declaring module but does not refuse cross-module function-call construction via an exported mint. Buildable closure without new capability: sole_constructor process-output carrier in the wet-transport home module, constructed only from the host effect, type and consumers exported, no cross-module constructor or mint; observation mint takes walled process output instead of loose stdout fields.", 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 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 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); next falsification slice is sole_constructor process-output input at wet transport (buildable now, not reference-edge admission).", + 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." ) diff --git a/src/v2/compiler/self_host/behavioral_comparison_receipt.dag b/src/v2/compiler/self_host/behavioral_comparison_receipt.dag index bb6c98441aa..855ac3be0f0 100644 --- a/src/v2/compiler/self_host/behavioral_comparison_receipt.dag +++ b/src/v2/compiler/self_host/behavioral_comparison_receipt.dag @@ -12,7 +12,7 @@ import std.types { CommitSha, Int } data behavioral_comparison_receipt_note: String = "Executed behavioral comparison receipt carrier (still-bat-561 ceiling audit): rows and verdict are derived from stdout at observation construction. advance checks field binding against the written artifact — NOT that stdout came from a real process." -data behavioral_admission_seal_ceiling_note: String = "CEILING probe (still-bat-561 msg_63187749, EXECUTED): admission_seal is a caller-derivable checksum — not execution proof. BehavioralComparisonObservation sole_constructor landed; cross-module record-literal construction is REFUSED (SoleConstructorViolation on probe.behavioral_observation_sole_constructor_probe, construction form: record literal outside v2.compiler.self_host.behavioral_comparison_receipt). LEAK: exported mint_behavioral_comparison_observation — construction form: cross-module function call with caller-supplied stdout/stderr/exit_success/comparison_rows; fully_matching_derived_seal_forgery_advance_succeeds_red still greens via mint + derived seal. Next trigger (reference-edge admission thread): wall mint INPUT with a host-effect-only process-output carrier at the wet transport boundary so witness cannot fabricate stdout. fully_matching_derived_seal_forgery_advance_succeeds_red stays enrolled; flips to refuse when input wall lands, does not retire (DESIGN 4b(4))." +data behavioral_admission_seal_ceiling_note: String = "CEILING probe (still-bat-561 msg_63187749, EXECUTED): admission_seal is a caller-derivable checksum — not execution proof. BehavioralComparisonObservation sole_constructor landed; cross-module record-literal construction REFUSED (SoleConstructorViolation, construction form: record literal outside v2.compiler.self_host.behavioral_comparison_receipt). LEAK: exported mint_behavioral_comparison_observation — construction form: cross-module function call with caller-supplied stdout/stderr/exit_success/comparison_rows; fully_matching_derived_seal_forgery_advance_succeeds_red still greens via mint + derived seal. Filed on gunbc.roadmap_authority unforgeable-construction-capability. Next trigger (can-climb-now-but-unbuilt, next PR — not reference-edge admission): sole_constructor process-output carrier in tools.direct_rust_door_transport, construct from host effect only, export type+consumers not mint; mint_behavioral_comparison_observation takes walled process output instead of loose stdout/stderr/exit_success. Residue: comparison_rows/corpus_identity may stay caller-supplied unless derived from stdout. fully_matching_derived_seal_forgery_advance_succeeds_red stays enrolled; flips to refuse when input wall lands, does not retire (DESIGN 4b(4))." type BehavioralComparisonSubject { module_path: String From 4d80b4cd3e2577e92631482eff43a680f5848a18 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 17:06:02 +0000 Subject: [PATCH 04/22] Record negative opaque host-effect probe; gate PR2 on capability lane. Bounded probe (msg_00cc6fd9): WitnessBin.Run returns forgeable Strings; sole_constructor + exported mint does not equal unforgeable execution evidence. Update roadmap receipt and ceiling note; PR2 stays draft until export control or opaque effect return lands. Co-authored-by: Cursor --- dag/gunbc/roadmap_authority.dag | 4 ++-- src/v2/compiler/self_host/behavioral_comparison_receipt.dag | 4 +++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/dag/gunbc/roadmap_authority.dag b/dag/gunbc/roadmap_authority.dag index fab3fa01707..a9f677dadee 100644 --- a/dag/gunbc/roadmap_authority.dag +++ b/dag/gunbc/roadmap_authority.dag @@ -2921,9 +2921,9 @@ fn guarantee_ladder_nodes() -> List { volume: VolumeLarge, t: fields( 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 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. EXECUTED FALSIFICATION RECEIPT (2026-08-04, royal-crab-235, specimen v2.compiler.self_host.behavioral_comparison_receipt BehavioralComparisonObservation): cross-module record literal → SoleConstructorViolation (refused); cross-module exported-function call to mint_behavioral_comparison_observation with caller-supplied stdout/stderr/exit_success/rows → leaks (fully_matching_derived_seal_forgery_advance_succeeds_red greens). Counted audit finding: sole_constructor refuses record-literal construction outside the declaring module but does not refuse cross-module function-call construction via an exported mint. Buildable closure without new capability: sole_constructor process-output carrier in the wet-transport home module, constructed only from the host effect, type and consumers exported, no cross-module constructor or mint; observation mint takes walled process output instead of loose stdout fields.", + 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 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. EXECUTED FALSIFICATION RECEIPT (2026-08-04, royal-crab-235, specimen v2.compiler.self_host.behavioral_comparison_receipt BehavioralComparisonObservation): cross-module record literal → SoleConstructorViolation (refused); cross-module exported-function call to mint_behavioral_comparison_observation with caller-supplied stdout/stderr/exit_success/rows → leaks (fully_matching_derived_seal_forgery_advance_succeeds_red greens via real forge, permanent enrolled control). BOUNDED PROBE NEGATIVE (msg_00cc6fd9): opaque host-effect process-result is NOT expressible at current substrate — WitnessBin.Run returns plain Strings; sole_constructor + transport fill is forgeable via exported mint; .dag has no function visibility. Module-structure decorative carrier does NOT close the hole. Real paths: opaque effect return at extdeps service boundary OR export control / reference-edge admission.", 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 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); next falsification slice is sole_constructor process-output input at wet transport (buildable now, not reference-edge admission).", + first_slice: "The falsification matrix on ONE carrier: type Refined 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." diff --git a/src/v2/compiler/self_host/behavioral_comparison_receipt.dag b/src/v2/compiler/self_host/behavioral_comparison_receipt.dag index 855ac3be0f0..d9610f30756 100644 --- a/src/v2/compiler/self_host/behavioral_comparison_receipt.dag +++ b/src/v2/compiler/self_host/behavioral_comparison_receipt.dag @@ -12,7 +12,9 @@ import std.types { CommitSha, Int } data behavioral_comparison_receipt_note: String = "Executed behavioral comparison receipt carrier (still-bat-561 ceiling audit): rows and verdict are derived from stdout at observation construction. advance checks field binding against the written artifact — NOT that stdout came from a real process." -data behavioral_admission_seal_ceiling_note: String = "CEILING probe (still-bat-561 msg_63187749, EXECUTED): admission_seal is a caller-derivable checksum — not execution proof. BehavioralComparisonObservation sole_constructor landed; cross-module record-literal construction REFUSED (SoleConstructorViolation, construction form: record literal outside v2.compiler.self_host.behavioral_comparison_receipt). LEAK: exported mint_behavioral_comparison_observation — construction form: cross-module function call with caller-supplied stdout/stderr/exit_success/comparison_rows; fully_matching_derived_seal_forgery_advance_succeeds_red still greens via mint + derived seal. Filed on gunbc.roadmap_authority unforgeable-construction-capability. Next trigger (can-climb-now-but-unbuilt, next PR — not reference-edge admission): sole_constructor process-output carrier in tools.direct_rust_door_transport, construct from host effect only, export type+consumers not mint; mint_behavioral_comparison_observation takes walled process output instead of loose stdout/stderr/exit_success. Residue: comparison_rows/corpus_identity may stay caller-supplied unless derived from stdout. fully_matching_derived_seal_forgery_advance_succeeds_red stays enrolled; flips to refuse when input wall lands, does not retire (DESIGN 4b(4))." +data behavioral_admission_seal_ceiling_note: String = "CEILING probe (still-bat-561 msg_63187749, EXECUTED): admission_seal is a caller-derivable checksum — not execution proof. BehavioralComparisonObservation sole_constructor landed; cross-module record-literal construction REFUSED (SoleConstructorViolation). LEAK: exported mint_behavioral_comparison_observation — cross-module function call with caller-supplied stdout/stderr/exit_success/comparison_rows; fully_matching_derived_seal_forgery_advance_succeeds_red greens via real forge (mint + derived seal), never optional_absent() — permanent enrolled control (msg_00cc6fd9). BOUNDED PROBE (msg_00cc6fd9, EXECUTED): opaque host-effect process-result is NOT expressible at the current substrate — extdeps.gunbc.WitnessBin.Run returns plain stdout/stderr/exit_success Strings; sole_constructor blocks record literals but NOT exported mint functions; .dag has no function visibility. Transport-filled sole_constructor records are forgeable via mint export — not opaque execution evidence. Real fix: opaque effect return at service boundary OR export control / reference-edge admission (gunbc.roadmap_authority unforgeable-construction-capability, trigger can-climb-after-one-capability). PR2 (#7792) stays draft until capability lands; mechanically preventive ceiling unless operator caps at option 3." + +data opaque_host_effect_process_result_probe_note: String = "Bounded capability probe (royal-crab-235, msg_00cc6fd9): can host-effect return an opaque process-result carrier ordinary .dag code cannot construct? VERDICT: NO at current substrate. WitnessBin.Run output is stdout/stderr/exit_success as plain Strings — caller-forgeable primitives. sole_constructor + internal transport fill does not equal unforgeable evidence because mint_behavioral_comparison_observation is exported and constructs the sole_constructor type from those same fields. LeanAdmittedBitWidth precedent is admission validation (lean_admit_bit_width), not opacity. No third decorative carrier closes the hole; export control or a genuinely opaque effect-bound type is required." type BehavioralComparisonSubject { module_path: String From bbbb1a2b346b461dfabdc1d3716ed055968a7b07 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 17:19:28 +0000 Subject: [PATCH 05/22] =?UTF-8?q?WIP:=20Lane=204:=20direct-door=20behavior?= =?UTF-8?q?al=20qualification=20=E2=80=94=20CargoGreen=20to=20BehavioralE?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- dag/tools/direct_rust_door_transport.dag | 6 +- .../self_host/direct_rust_door_fixture.dag | 2 + .../self_host/fixture_synthetic_emission.dag | 115 ++++++++++++++++-- ...t_rust_door_qualification_witness_test.dag | 7 ++ 4 files changed, 122 insertions(+), 8 deletions(-) diff --git a/dag/tools/direct_rust_door_transport.dag b/dag/tools/direct_rust_door_transport.dag index cb65ba735d2..6870316d07b 100644 --- a/dag/tools/direct_rust_door_transport.dag +++ b/dag/tools/direct_rust_door_transport.dag @@ -29,6 +29,7 @@ import v2.compiler.self_host.fixture_synthetic_emission { advance_written_synthetic_emitted_artifact_fixture_behaviorally_equivalent, fixture_behavior_receipt_identity_for, mint_written_synthetic_emitted_artifact_from_fixture_inferred, + mint_written_synthetic_emitted_artifact_from_fixture_inferred_for_behavioral_qualification, WrittenSyntheticEmittedArtifact, written_synthetic_emitted_artifact_has_fixture_behaviorally_equivalent_qualification, written_synthetic_emitted_artifact_has_fixture_cargo_green_qualification, @@ -40,6 +41,7 @@ import v2.compiler.self_host.direct_rust_door_fixture { direct_rust_door_behavioral_probe_function, direct_rust_door_behavioral_witness_bin_path, direct_rust_door_divergent_rust_source, + direct_rust_door_fixture_lane_tag, direct_rust_door_inferred_tree, direct_rust_door_module_path, direct_rust_door_target_model @@ -202,11 +204,12 @@ fn direct_rust_door_compile_workspace(workspace_dir: String) -> Bool { fn direct_rust_door_emit_write_compile_to_cargo_green( workspace_dir: String ) -> Optional { - match mint_written_synthetic_emitted_artifact_from_fixture_inferred( + match mint_written_synthetic_emitted_artifact_from_fixture_inferred_for_behavioral_qualification( inferred: direct_rust_door_inferred_tree, target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, workspace_dir: workspace_dir, + fixture_lane_tag: direct_rust_door_fixture_lane_tag, behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, behavioral_probe_function: direct_rust_door_behavioral_probe_function ) { @@ -304,6 +307,7 @@ fn run_direct_rust_door_divergent_behavioral_receipt_refused() -> Bool { target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, workspace_dir: dir.path, + fixture_lane_tag: direct_rust_door_fixture_lane_tag, behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, behavioral_probe_function: direct_rust_door_behavioral_probe_function ) { diff --git a/src/v2/compiler/self_host/direct_rust_door_fixture.dag b/src/v2/compiler/self_host/direct_rust_door_fixture.dag index 65825d66dc2..1d2b37d4e29 100644 --- a/src/v2/compiler/self_host/direct_rust_door_fixture.dag +++ b/src/v2/compiler/self_host/direct_rust_door_fixture.dag @@ -71,6 +71,8 @@ data direct_rust_door_behavioral_probe_entry: String = "dag/test/claim/direct_ru data direct_rust_door_behavioral_probe_function: String = "direct_rust_door_behavioral_qualification_holds" +data direct_rust_door_fixture_lane_tag: String = "direct_rust_door_fixture_containment" + fn direct_rust_door_behavioral_corpus_identity() -> Hash { symbol_identity_digest(sym: ^direct_rust_door_corpus_v1) } diff --git a/src/v2/compiler/self_host/fixture_synthetic_emission.dag b/src/v2/compiler/self_host/fixture_synthetic_emission.dag index 5f5a437d86b..310f4efb71a 100644 --- a/src/v2/compiler/self_host/fixture_synthetic_emission.dag +++ b/src/v2/compiler/self_host/fixture_synthetic_emission.dag @@ -5,8 +5,7 @@ import extdeps.communication.medium { Medium } import v2.compiler.infer { InferredTree } import v2.compiler.self_host.behavioral_comparison_receipt { AdmittedBehaviorEquivalentReceipt, - admitted_behavioral_comparison_receipt_matches_binding, - emitted_source_identity_for_medium + admitted_behavioral_comparison_receipt_matches_binding } import v2.compiler.self_host.candidate_generation { generate_rust_emission_candidate, @@ -29,9 +28,9 @@ import v2.std.optional { Absent, Present, optional_absent, optional_present } import v2.std.text { String } import std.types { CommitSha } -data fixture_synthetic_emission_note: String = "Parallel fixture-scoped emission authority (royal-crab-235 disposition 2, wise-ram-22 ruling): SyntheticEmittedArtifact / FixtureBehaviorReceipt carry fixture qualifications only — no constructor into ProducerEmissionReceipt or EmissionQualification, so fixture mint cannot reach the production frontier by mistake." +data fixture_synthetic_emission_note: String = "Parallel fixture-scoped emission authority (wise-ram-22 disposition PR1 containment): SyntheticEmittedArtifact / FixtureBehaviorReceipt carry FixtureEmissionQualification only — no constructor into ProducerEmissionReceipt or production EmissionQualification." -data fixture_synthetic_emission_dissolution_trigger: String = "dissolve-on disposition 1 (wise-ram-22 containment lane): real source-ingest behavioral qualification — generate_written_rust_candidate_from_ingest mints ProvenancedRustArtifact with production BehavioralEquivalent after infer(assemble(fixture ingest)) accepts without hand-authored DerivedGrounding. When that path greens, this module's fixture ladder, wet transport mints on direct_rust_door_inferred_tree, and FixtureBehaviorallyEquivalent delete together; production BehavioralEquivalent subsumes the behavioral receipt machinery for the direct-door subject." +data fixture_synthetic_emission_dissolution_trigger: String = "dissolve-on disposition 1 (wise-ram-22 containment lane): real source-ingest qualification after infer(assemble(fixture ingest)) accepts without hand-authored DerivedGrounding. When that path greens, fixture mint on direct_rust_door_inferred_tree deletes and production ProvenancedRustArtifact subsumes the subject." type FixtureEmissionQualification = FixtureSourceProduced @@ -41,6 +40,7 @@ type FixtureEmissionQualification type FixtureBehaviorReceipt { module_path: String emitted_source_identity: Hash + fixture_lane_tag: String behavioral_probe_entry: String behavioral_probe_function: String qualifications: List @@ -73,6 +73,10 @@ data fixture_behaviorally_equivalent_qualifications: List) -> Hash { + content_hash_atom(value: source.carried) +} + fn fixture_emission_qualification_eq( left: FixtureEmissionQualification, right: FixtureEmissionQualification @@ -130,12 +134,34 @@ fn fixture_behavior_receipt_identity_for(receipt: FixtureBehaviorReceipt) -> Has fn mint_fixture_behavior_receipt( module_path: String, emitted_source: Medium, + fixture_lane_tag: String +) -> FixtureBehaviorReceipt { + FixtureBehaviorReceipt { + module_path: module_path, + emitted_source_identity: fixture_emitted_source_identity_for_medium( + source: emitted_source + ), + fixture_lane_tag: fixture_lane_tag, + behavioral_probe_entry: "", + behavioral_probe_function: "", + qualifications: fixture_source_produced_qualifications, + build_green: false + } +} + +fn mint_fixture_behavior_receipt_for_behavioral_qualification( + module_path: String, + emitted_source: Medium, + fixture_lane_tag: String, behavioral_probe_entry: String, behavioral_probe_function: String ) -> FixtureBehaviorReceipt { FixtureBehaviorReceipt { module_path: module_path, - emitted_source_identity: emitted_source_identity_for_medium(source: emitted_source), + emitted_source_identity: fixture_emitted_source_identity_for_medium( + source: emitted_source + ), + fixture_lane_tag: fixture_lane_tag, behavioral_probe_entry: behavioral_probe_entry, behavioral_probe_function: behavioral_probe_function, qualifications: fixture_source_produced_qualifications, @@ -186,6 +212,7 @@ fn advance_fixture_behavior_receipt_cargo_green( value: FixtureBehaviorReceipt { module_path: prior.module_path, emitted_source_identity: prior.emitted_source_identity, + fixture_lane_tag: prior.fixture_lane_tag, behavioral_probe_entry: prior.behavioral_probe_entry, behavioral_probe_function: prior.behavioral_probe_function, qualifications: fixture_cargo_green_qualifications, @@ -207,6 +234,7 @@ fn advance_fixture_behavior_receipt_behaviorally_equivalent( value: FixtureBehaviorReceipt { module_path: prior.module_path, emitted_source_identity: prior.emitted_source_identity, + fixture_lane_tag: prior.fixture_lane_tag, behavioral_probe_entry: behavioral_probe_entry, behavioral_probe_function: behavioral_probe_function, qualifications: fixture_behaviorally_equivalent_qualifications, @@ -220,6 +248,31 @@ fn mint_synthetic_emitted_artifact_from_fixture_inferred( inferred: InferredTree, target: TargetModel, module_path: String, + fixture_lane_tag: String +) -> Outcome { + bind_outcome( + o: generate_rust_emission_candidate(inferred: inferred, target: target), + f: fn(candidate) { + outcome_accepted( + value: SyntheticEmittedArtifact { + source: candidate.source, + emitted: candidate.emitted, + fixture_receipt: mint_fixture_behavior_receipt( + module_path: module_path, + emitted_source: candidate.source, + fixture_lane_tag: fixture_lane_tag + ) + } + ) + } + ) +} + +fn mint_synthetic_emitted_artifact_from_fixture_inferred_for_behavioral_qualification( + inferred: InferredTree, + target: TargetModel, + module_path: String, + fixture_lane_tag: String, behavioral_probe_entry: String, behavioral_probe_function: String ) -> Outcome { @@ -230,9 +283,10 @@ fn mint_synthetic_emitted_artifact_from_fixture_inferred( value: SyntheticEmittedArtifact { source: candidate.source, emitted: candidate.emitted, - fixture_receipt: mint_fixture_behavior_receipt( + fixture_receipt: mint_fixture_behavior_receipt_for_behavioral_qualification( module_path: module_path, emitted_source: candidate.source, + fixture_lane_tag: fixture_lane_tag, behavioral_probe_entry: behavioral_probe_entry, behavioral_probe_function: behavioral_probe_function ) @@ -247,14 +301,44 @@ fn mint_written_synthetic_emitted_artifact_from_fixture_inferred( target: TargetModel, module_path: String, workspace_dir: String, + fixture_lane_tag: String +) -> Outcome { + bind_outcome( + o: mint_synthetic_emitted_artifact_from_fixture_inferred( + inferred: inferred, + target: target, + module_path: module_path, + fixture_lane_tag: fixture_lane_tag + ), + f: fn(artifact) { + outcome_accepted( + value: WrittenSyntheticEmittedArtifact { + artifact: artifact, + write: write_rust_workspace( + workspace_dir: workspace_dir, + source: artifact.source + ) + } + ) + } + ) +} + +fn mint_written_synthetic_emitted_artifact_from_fixture_inferred_for_behavioral_qualification( + inferred: InferredTree, + target: TargetModel, + module_path: String, + workspace_dir: String, + fixture_lane_tag: String, behavioral_probe_entry: String, behavioral_probe_function: String ) -> Outcome { bind_outcome( - o: mint_synthetic_emitted_artifact_from_fixture_inferred( + o: mint_synthetic_emitted_artifact_from_fixture_inferred_for_behavioral_qualification( inferred: inferred, target: target, module_path: module_path, + fixture_lane_tag: fixture_lane_tag, behavioral_probe_entry: behavioral_probe_entry, behavioral_probe_function: behavioral_probe_function ), @@ -366,3 +450,20 @@ fn written_synthetic_emitted_artifact_has_fixture_behaviorally_equivalent_qualif wanted: FixtureBehaviorallyEquivalent ) } + +fn synthetic_emitted_artifact_has_fixture_source_produced_only( + artifact: SyntheticEmittedArtifact +) -> Bool { + fixture_emission_qualifications_list_contains( + xs: artifact.fixture_receipt.qualifications, + wanted: FixtureSourceProduced + ) + && !fixture_emission_qualifications_list_contains( + xs: artifact.fixture_receipt.qualifications, + wanted: FixtureCargoGreen + ) + && !fixture_emission_qualifications_list_contains( + xs: artifact.fixture_receipt.qualifications, + wanted: FixtureBehaviorallyEquivalent + ) +} diff --git a/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag b/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag index 9c8b8e1de1e..e3ebfc010a2 100644 --- a/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag +++ b/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag @@ -33,6 +33,7 @@ import v2.compiler.self_host.direct_rust_door_fixture { direct_rust_door_behavioral_corpus_identity, direct_rust_door_behavioral_probe_entry, direct_rust_door_behavioral_probe_function, + direct_rust_door_fixture_lane_tag, direct_rust_door_inferred_tree, direct_rust_door_module_path, direct_rust_door_subtract_comparison_rows, @@ -167,6 +168,7 @@ test fn fully_matching_derived_seal_forgery_advance_succeeds_red() -> Bool { inferred: direct_rust_door_inferred_tree, target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, + fixture_lane_tag: direct_rust_door_fixture_lane_tag, behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, behavioral_probe_function: direct_rust_door_behavioral_probe_function ) { @@ -207,6 +209,7 @@ test fn fully_matching_counterfeit_without_admission_seal_advance_refuses() -> B inferred: direct_rust_door_inferred_tree, target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, + fixture_lane_tag: direct_rust_door_fixture_lane_tag, behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, behavioral_probe_function: direct_rust_door_behavioral_probe_function ) { @@ -255,6 +258,7 @@ test fn witness_behavioral_advance_refuses_without_cargo_green_reds() -> Bool { inferred: direct_rust_door_inferred_tree, target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, + fixture_lane_tag: direct_rust_door_fixture_lane_tag, behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, behavioral_probe_function: direct_rust_door_behavioral_probe_function ) { @@ -288,6 +292,7 @@ test fn witness_behavioral_advance_refuses_diverged_observation_reds() -> Bool { inferred: direct_rust_door_inferred_tree, target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, + fixture_lane_tag: direct_rust_door_fixture_lane_tag, behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, behavioral_probe_function: direct_rust_door_behavioral_probe_function ) { @@ -333,6 +338,7 @@ test fn witness_behavioral_advance_refuses_mismatched_executable_identity_reds() inferred: direct_rust_door_inferred_tree, target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, + fixture_lane_tag: direct_rust_door_fixture_lane_tag, behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, behavioral_probe_function: direct_rust_door_behavioral_probe_function ) { @@ -373,6 +379,7 @@ test fn witness_cargo_green_advance_does_not_imply_behavioral_equivalent_holds() inferred: direct_rust_door_inferred_tree, target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, + fixture_lane_tag: direct_rust_door_fixture_lane_tag, behavioral_probe_entry: direct_rust_door_behavioral_probe_entry, behavioral_probe_function: direct_rust_door_behavioral_probe_function ) { From 1cd2635018e1cc373729d88506dfa9e83eb7399e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 17:20:05 +0000 Subject: [PATCH 06/22] Restore PR1 containment in fixture_synthetic_emission; layer PR2 additions. Checkout main as base for fixture_synthetic_emission.dag; add behavioral fields and extension mints without removing fixture_lane_tag or synthetic_emitted_artifact_has_fixture_source_produced_only. Co-authored-by: Cursor --- dag/tools/direct_rust_door_transport.dag | 2 +- ...direct_rust_door_qualification_witness_test.dag | 14 +++++++------- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/dag/tools/direct_rust_door_transport.dag b/dag/tools/direct_rust_door_transport.dag index 6870316d07b..5500269c740 100644 --- a/dag/tools/direct_rust_door_transport.dag +++ b/dag/tools/direct_rust_door_transport.dag @@ -302,7 +302,7 @@ fn run_direct_rust_door_behavioral_qualification_smoke() -> Bool { fn run_direct_rust_door_divergent_behavioral_receipt_refused() -> Bool { let dir = shell.Mktemp.Dir() let src_dir = shell.Mkdir.Parents(path: concat(dir.path, "/src")) - let pipeline_ok = match mint_written_synthetic_emitted_artifact_from_fixture_inferred( + let pipeline_ok = match mint_written_synthetic_emitted_artifact_from_fixture_inferred_for_behavioral_qualification( inferred: direct_rust_door_inferred_tree, target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, diff --git a/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag b/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag index e3ebfc010a2..d14ef47bf7e 100644 --- a/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag +++ b/src/v2/test/claim/self_host/direct_rust_door_qualification_witness_test.dag @@ -21,7 +21,7 @@ import v2.compiler.self_host.fixture_synthetic_emission { advance_written_synthetic_emitted_artifact_cargo_green, advance_written_synthetic_emitted_artifact_fixture_behaviorally_equivalent, fixture_behavior_receipt_identity_for, - mint_synthetic_emitted_artifact_from_fixture_inferred, + mint_synthetic_emitted_artifact_from_fixture_inferred_for_behavioral_qualification, SyntheticEmittedArtifact, WrittenSyntheticEmittedArtifact, written_synthetic_emitted_artifact_has_fixture_behaviorally_equivalent_qualification, @@ -164,7 +164,7 @@ fn direct_rust_door_derived_seal_forgery_admitted( } test fn fully_matching_derived_seal_forgery_advance_succeeds_red() -> Bool { - match mint_synthetic_emitted_artifact_from_fixture_inferred( + match mint_synthetic_emitted_artifact_from_fixture_inferred_for_behavioral_qualification( inferred: direct_rust_door_inferred_tree, target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, @@ -205,7 +205,7 @@ test fn fully_matching_derived_seal_forgery_advance_succeeds_red() -> Bool { } test fn fully_matching_counterfeit_without_admission_seal_advance_refuses() -> Bool { - match mint_synthetic_emitted_artifact_from_fixture_inferred( + match mint_synthetic_emitted_artifact_from_fixture_inferred_for_behavioral_qualification( inferred: direct_rust_door_inferred_tree, target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, @@ -254,7 +254,7 @@ test fn fully_matching_counterfeit_without_admission_seal_advance_refuses() -> B } test fn witness_behavioral_advance_refuses_without_cargo_green_reds() -> Bool { - match mint_synthetic_emitted_artifact_from_fixture_inferred( + match mint_synthetic_emitted_artifact_from_fixture_inferred_for_behavioral_qualification( inferred: direct_rust_door_inferred_tree, target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, @@ -288,7 +288,7 @@ test fn witness_behavioral_advance_refuses_without_cargo_green_reds() -> Bool { } test fn witness_behavioral_advance_refuses_diverged_observation_reds() -> Bool { - match mint_synthetic_emitted_artifact_from_fixture_inferred( + match mint_synthetic_emitted_artifact_from_fixture_inferred_for_behavioral_qualification( inferred: direct_rust_door_inferred_tree, target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, @@ -334,7 +334,7 @@ test fn witness_behavioral_advance_refuses_diverged_observation_reds() -> Bool { } test fn witness_behavioral_advance_refuses_mismatched_executable_identity_reds() -> Bool { - match mint_synthetic_emitted_artifact_from_fixture_inferred( + match mint_synthetic_emitted_artifact_from_fixture_inferred_for_behavioral_qualification( inferred: direct_rust_door_inferred_tree, target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, @@ -375,7 +375,7 @@ test fn witness_behavioral_advance_refuses_mismatched_executable_identity_reds() } test fn witness_cargo_green_advance_does_not_imply_behavioral_equivalent_holds() -> Bool { - match mint_synthetic_emitted_artifact_from_fixture_inferred( + match mint_synthetic_emitted_artifact_from_fixture_inferred_for_behavioral_qualification( inferred: direct_rust_door_inferred_tree, target: direct_rust_door_target_model(), module_path: direct_rust_door_module_path, From 3ecb580ff03de09df2640f5a786ac2fff3c9c77e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 18:21:21 +0000 Subject: [PATCH 07/22] =?UTF-8?q?WIP:=20Lane=204:=20direct-door=20behavior?= =?UTF-8?q?al=20qualification=20=E2=80=94=20CargoGreen=20to=20BehavioralE?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- dag/gunbc/roadmap_authority.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dag/gunbc/roadmap_authority.dag b/dag/gunbc/roadmap_authority.dag index a9f677dadee..030deb7b529 100644 --- a/dag/gunbc/roadmap_authority.dag +++ b/dag/gunbc/roadmap_authority.dag @@ -2921,7 +2921,7 @@ fn guarantee_ladder_nodes() -> List { volume: VolumeLarge, t: fields( 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 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. EXECUTED FALSIFICATION RECEIPT (2026-08-04, royal-crab-235, specimen v2.compiler.self_host.behavioral_comparison_receipt BehavioralComparisonObservation): cross-module record literal → SoleConstructorViolation (refused); cross-module exported-function call to mint_behavioral_comparison_observation with caller-supplied stdout/stderr/exit_success/rows → leaks (fully_matching_derived_seal_forgery_advance_succeeds_red greens via real forge, permanent enrolled control). BOUNDED PROBE NEGATIVE (msg_00cc6fd9): opaque host-effect process-result is NOT expressible at current substrate — WitnessBin.Run returns plain Strings; sole_constructor + transport fill is forgeable via exported mint; .dag has no function visibility. Module-structure decorative carrier does NOT close the hole. Real paths: opaque effect return at extdeps service boundary OR export control / reference-edge admission.", + 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 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 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).", From 69e266c361d38c2f75213ae62757ed6a76046862 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 21:03:45 +0000 Subject: [PATCH 08/22] Add ConstructorReferenceAdmission design note (model-first). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Draft design for reference-edge admission closing the measured sole_constructor mint-call leak. Documents carrier shape, first slice, open infer-stage placement decision, and composition with sole_constructor. No code — operator sign-off required before implementation. Co-authored-by: Cursor --- .../constructor-reference-admission-design.md | 132 ++++++++++++++++++ 1 file changed, 132 insertions(+) create mode 100644 docs/plans/constructor-reference-admission-design.md diff --git a/docs/plans/constructor-reference-admission-design.md b/docs/plans/constructor-reference-admission-design.md new file mode 100644 index 00000000000..aa683190f9a --- /dev/null +++ b/docs/plans/constructor-reference-admission-design.md @@ -0,0 +1,132 @@ +# ConstructorReferenceAdmission — reference-edge admission for sealed constructors + +**Status:** DRAFT for operator review (2026-08-04, royal-crab-235, msg_13fbbaaf / node `adhoc-f519571b-764`). **No code lands from this note** until the shape is agreed. Owner: royal-crab-235 (measured both construction routes on `BehavioralComparisonObservation`; first_slice and discriminating controls already in tree). + +**Origin:** Executed falsification (royal-crab-235, msg_6701c04d): `sole_constructor` refuses cross-module **record literals** but does **not** refuse cross-module **calls** to an exported mint with caller-supplied fields; legitimate wet transport requires that mint. Process-output carrier reshuffle and opaque `WitnessBin.Run` output do not close the hole. **Derived ceiling:** `can-climb-after-one-capability`. **Preferred trigger:** this capability. + +**Evidence PRs (draft, do not merge claiming `FixtureBehaviorallyEquivalent`):** #7792, #7794. + +## 0. Displaced cost + +- **Forged execution evidence:** any module can call `mint_behavioral_comparison_observation` with fabricated stdout/status/rows and reach `FixtureBehaviorallyEquivalent` advance — the admission seal is a checksum of caller input, not proof of process execution. +- **Decorative carrier churn:** module-structure `sole_constructor` wrappers do not climb the ladder; each reshuffle re-documents the same leak (`fully_matching_derived_seal_forgery_advance_succeeds_red` stays green). +- **False merge signal:** PR titles/bodies that claim behavioral equivalence while the body disclaims it (msg_13fbbaaf) — two-authority disagreement where the list UI is wrong. + +## 1. Measured gap (two construction forms, one specimen) + +Specimen: `v2.compiler.self_host.behavioral_comparison_receipt` `BehavioralComparisonObservation` (`sole_constructor` on the type). + +| Construction form | Verdict | Mechanism today | +|---|---|---| +| Cross-module record literal | **REFUSED** | `SoleConstructorViolation` in infer (`v1_compiler_infer` record-literal arm; same-module span check) | +| Cross-module call to exported `mint_behavioral_comparison_observation` | **LEAKS** | No call-edge admission; exported fn is writable from any importer | +| Opaque host-effect return | **NEGATIVE** | `WitnessBin.Run` returns forgeable `String`/`Bool` fields | +| Process-output `sole_constructor` carrier (#7794) | **DECORATIVE** | Forge via `from_run_fields` / `hermetic_equivalent` | + +**Closing both refused + leaking routes** requires a capability beyond `sole_constructor` alone. **Legitimate wet transport** (`tools.direct_rust_door_transport`) must remain admitted after the wall lands. + +## 2. End shape (carrier) + +```dag +// std layer — agnostic admission shape (authority TBD: std.construction or std.decl_ref extension) +type ConstructorReferenceAdmission { + constructor: DeclarationRef // callee that constructs the sealed type (mint fn or sole ctor fn) + permitted_callers: List // nonempty by construction — see §3 +} +``` + +**Citation rule (§3):** both `constructor` and each permitted caller are `DeclarationRef` rows — they ride `std.decl_ref` / cited-symbol resolution already in tree. Every ref must resolve to exactly one declaration or refuse at authoring; no second naming scheme. + +**Refusal (when a call edge is checked):** typed, located diagnostic naming: + +- the **constructor** `DeclarationRef` (resolved symbol), +- the **offending caller** `DeclarationRef` (the calling declaration — typically the enclosing `fn`), +- the **permitted set** (resolved symbols or explicit "none listed" — never silent). + +Suggested variant name: `ConstructorCallAdmissionRefused` (exact spelling TBD with existing diagnostic taxonomy). + +**Not a generic violation string** — coordinates must be structurally present for counting and ladder receipts. + +## 3. Nonempty permitted callers + +`NonEmptyList` does not exist in `std` today. Precedent: `gunbc.doc_graph_roots` `HandAuthoredDocBind` — `primary_work` required scalar + `additional_works` list makes zero-anchor unwritable (construction, not validation). + +**Proposed:** `permitted_callers` as `List` with **authoring-time nonempty** enforced on the admission row carrier (wall on the metadata row), OR split `first_permitted_caller: DeclarationRef` + `further_permitted_callers: List`. Pick one at implementation; design requirement is **empty permitted set is unwritable**. + +## 4. Where the refusal fires — OPEN DECISION (load-bearing) + +**Measured today:** `sole_constructor` refusal fires in **infer** on **record literal** construction when the type's declaring-module span ≠ literal span (`v1_compiler_infer`, `SoleConstructorViolation`). + +**ConstructorReferenceAdmission** needs a **call-edge** check: importer module calls exported mint/creator with caller declaration not in permitted set. + +**Candidate placement:** + +| Stage | Pros | Cons | +|---|---|---| +| **Infer — direct call resolution** (parallel to record-literal sole_ctor arm) | Same stage as existing sole_ctor; callee + caller module known at call site | **Infer is load-bearing** (DESIGN §7); touches hot path | +| Post-infer dedicated pass | Isolates new logic | Second representation of "who may call whom"; risk of drift from infer call binding | +| Name resolution only | Aligns with "reference edge" | May be insufficient if call shape is not a resolved direct callee (§5) | + +**STOP — operator decision required before implementation:** if the honest general case requires infer changes or name-resolution surgery, confirm that placement rather than routing around it. This note does **not** assume a workaround path. + +## 5. Design questions (must be answered in this note before code) + +### 5.1 Alias and higher-order positions + +When the callee is not syntactically the constructor (alias re-export, higher-order parameter, indirect call): + +- **Default honest stance:** outside the modeled guarantee until a witness proves otherwise — refuse or declare `AdmissionUnknown` with typed cause, never silently admit. +- **Direct call to resolved `mint_behavioral_comparison_observation`** is the first-slice scope; alias chains and HOF are explicit follow-on falsification rows. + +### 5.2 Composition with `sole_constructor` + +**Not redundant — complementary:** + +- `sole_constructor` → blocks cross-module **record literals** for the type. +- `ConstructorReferenceAdmission` → blocks cross-module **function calls** to listed constructors except permitted callers. + +Together they close the two routes measured on `BehavioralComparisonObservation`. Admission does **not** subsume sole_constructor (literals could still forge if sole_ctor were removed). sole_constructor does **not** subsume admission (exported mint calls leak today). + +### 5.3 Where the permitted list is authored + +**Proposal:** admission row lives **on the constructor's declaring module** (beside the type or mint fn), cited by `DeclarationRef` to the constructor symbol. Callers list wet-transport (and test) callers explicitly. + +**Module move:** `DeclarationRef` uses `module_path` + `decl_name` — if a permitted caller moves modules, the ref must be updated (same as any `DeclarationRef` row); no path-inferred auto-permission. + +### 5.4 Compiler-module exemptions + +`sole_constructor` carries compiler-module check exemptions (unverified completeness). **ConstructorReferenceAdmission must not inherit exemptions by default.** If an exemption is needed, it is a named row with dissolution trigger — never silent skip inside `v2.compiler` / `v1.compiler` trees. + +## 6. First slice (already written — executable acceptance) + +**Subject:** `mint_behavioral_comparison_observation` → `BehavioralComparisonObservation`. + +**Admit:** `tools.direct_rust_door_transport` wet path caller(s) only (resolve to `DeclarationRef` rows in the admission metadata). + +**Discriminating control (already enrolled):** `fully_matching_derived_seal_forgery_advance_succeeds_red` — performs **real forge** via `hermetic_equivalent` + derived seal; **must flip from PASS to refuse** when admission wall lands. Never `optional_absent()`. + +**Positive controls (already in tree):** record literal refusal; legitimate transport path when caller is listed; advance refuses without admission seal when observation is genuinely diverged. + +**Proof bar:** green-by-execution on the slice + forge RED flips — not grep, not title claim. + +## 7. Phases (no code until note signed) + +1. **P0 — this note + operator sign-off** on placement (§4) and alias/HOF stance (§5.1). +2. **P1 — model carrier** in `std` (or extend `std.decl_ref`) with nonempty permitted callers by construction. +3. **P2 — compiler refusal** at agreed stage with `ConstructorCallAdmissionRefused` diagnostic. +4. **P3 — first slice wiring** on `BehavioralComparisonObservation` + witness flip for forge RED. +5. **P4 — falsification matrix** continues on other construction forms (`Refined`, casts, variants) on **other carriers** — no generalization from one specimen. + +## 8. Out of scope + +- Merging #7792/#7794 as behavioral-equivalence claims. +- Third decorative seal carriers. +- Full function visibility / module privacy (broader than reference-edge admission). +- Retrofitting every `sole_constructor` type in one motion. + +## 9. Handback + +- Signed design note with placement decision. +- `ConstructorReferenceAdmission` carrier + resolved `DeclarationRef` rows for first slice. +- Infer (or agreed stage) refusal with typed diagnostic. +- `fully_matching_derived_seal_forgery_advance_succeeds_red` flipped to refuse on forge path. From 5e518c530f19d6eeaaad03f43e2af46fa6005186 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 21:06:04 +0000 Subject: [PATCH 09/22] Revise ConstructorReferenceAdmission note per msg_a87c2c75. Reframe fork as which-compiler (v1 infer has sole_constructor; v2 04_infer has zero). Reject separate pass; one construction-admission authority. Document alias residual risk, decl_ref import rule, and both v1/v2 horns for operator sequencing decision. Co-authored-by: Cursor --- .../constructor-reference-admission-design.md | 76 ++++++++++++------- 1 file changed, 50 insertions(+), 26 deletions(-) diff --git a/docs/plans/constructor-reference-admission-design.md b/docs/plans/constructor-reference-admission-design.md index aa683190f9a..aa3af9c3c98 100644 --- a/docs/plans/constructor-reference-admission-design.md +++ b/docs/plans/constructor-reference-admission-design.md @@ -1,6 +1,6 @@ # ConstructorReferenceAdmission — reference-edge admission for sealed constructors -**Status:** DRAFT for operator review (2026-08-04, royal-crab-235, msg_13fbbaaf / node `adhoc-f519571b-764`). **No code lands from this note** until the shape is agreed. Owner: royal-crab-235 (measured both construction routes on `BehavioralComparisonObservation`; first_slice and discriminating controls already in tree). +**Status:** DRAFT for operator review (2026-08-04, royal-crab-235, msg_13fbbaaf / node `adhoc-f519571b-764`; updated msg_a87c2c75). **No code lands from this note** until the shape is agreed and the **which-compiler** horn is operator-picked (§4). Owner: royal-crab-235. **Origin:** Executed falsification (royal-crab-235, msg_6701c04d): `sole_constructor` refuses cross-module **record literals** but does **not** refuse cross-module **calls** to an exported mint with caller-supplied fields; legitimate wet transport requires that mint. Process-output carrier reshuffle and opaque `WitnessBin.Run` output do not close the hole. **Derived ceiling:** `can-climb-after-one-capability`. **Preferred trigger:** this capability. @@ -18,7 +18,7 @@ Specimen: `v2.compiler.self_host.behavioral_comparison_receipt` `BehavioralCompa | Construction form | Verdict | Mechanism today | |---|---|---| -| Cross-module record literal | **REFUSED** | `SoleConstructorViolation` in infer (`v1_compiler_infer` record-literal arm; same-module span check) | +| Cross-module record literal | **REFUSED** | `SoleConstructorViolation` in **v1 infer only** (`src/v1/04_infer.dag` `type_has_sole_constructor`; realized in `v1_compiler_infer.rs` record-literal arm). **`src/v2/compiler/04_infer.dag` has zero `sole_constructor` handling** — the type marker is modeled in v2 source, but the refusal executes only on the v1 seed path today. | | Cross-module call to exported `mint_behavioral_comparison_observation` | **LEAKS** | No call-edge admission; exported fn is writable from any importer | | Opaque host-effect return | **NEGATIVE** | `WitnessBin.Run` returns forgeable `String`/`Bool` fields | | Process-output `sole_constructor` carrier (#7794) | **DECORATIVE** | Forge via `from_run_fields` / `hermetic_equivalent` | @@ -28,15 +28,19 @@ Specimen: `v2.compiler.self_host.behavioral_comparison_receipt` `BehavioralCompa ## 2. End shape (carrier) ```dag +import std.decl_ref { DeclarationRef, decl_ref, decl_field_ref } + // std layer — agnostic admission shape (authority TBD: std.construction or std.decl_ref extension) type ConstructorReferenceAdmission { - constructor: DeclarationRef // callee that constructs the sealed type (mint fn or sole ctor fn) + constructor: DeclarationRef // callee that constructs the sealed type (mint fn) permitted_callers: List // nonempty by construction — see §3 } ``` **Citation rule (§3):** both `constructor` and each permitted caller are `DeclarationRef` rows — they ride `std.decl_ref` / cited-symbol resolution already in tree. Every ref must resolve to exactly one declaration or refuse at authoring; no second naming scheme. +**Constructor import rule (operator decision msg_a87c2c75):** import `DeclarationRef`, `decl_ref`, and `decl_field_ref` from `std.decl_ref` — **never re-mint** those constructors in another module. `decl_ref_constructor_authority_note` records that two lanes independently re-minted the pair on 2026-08-01 and broke every closure containing both modules (v1-seed fn names are not module-scoped). This note must not become the third duplicate. + **Refusal (when a call edge is checked):** typed, located diagnostic naming: - the **constructor** `DeclarationRef` (resolved symbol), @@ -53,30 +57,50 @@ Suggested variant name: `ConstructorCallAdmissionRefused` (exact spelling TBD wi **Proposed:** `permitted_callers` as `List` with **authoring-time nonempty** enforced on the admission row carrier (wall on the metadata row), OR split `first_permitted_caller: DeclarationRef` + `further_permitted_callers: List`. Pick one at implementation; design requirement is **empty permitted set is unwritable**. -## 4. Where the refusal fires — OPEN DECISION (load-bearing) +## 4. Where the refusal fires — WHICH COMPILER (operator hold; session does not pick) + +**Correction (measured, msg_a87c2c75):** the fork is **not** infer versus a separate pass. Record-literal `sole_constructor` refusal today lives in **v1 infer** (`src/v1/04_infer.dag` + `v1_compiler_infer.rs`). **`src/v2/compiler/04_infer.dag` has zero `sole_constructor` occurrences** — the capability does not exist in v2 infer at all; it lives only in the v1 seed stack. `ConstructorReferenceAdmission` must land in the same compiler path that will actually execute for corpus `.dag` today. + +### 4.1 Decided now — ONE authority, no separate pass + +Construction admission is **one authority**. Record-literal refusal and call-edge refusal are two **forms of the same question** — who may construct this sealed type from where. Splitting them into two passes means two mechanisms that must agree about what construction means and will eventually disagree. -**Measured today:** `sole_constructor` refusal fires in **infer** on **record literal** construction when the type's declaring-module span ≠ literal span (`v1_compiler_infer`, `SoleConstructorViolation`). +**This note explicitly rejects a post-infer dedicated pass** as the tempting shape that avoids touching a load-bearing file. Avoiding a load-bearing file is not a design argument; it is the unmarked-workaround class (DESIGN §5). Whatever compiler hosts the wall, record-literal and call-edge checks live in the **same infer construction-admission authority**, beside the existing record-literal `sole_constructor` arm in v1. -**ConstructorReferenceAdmission** needs a **call-edge** check: importer module calls exported mint/creator with caller declaration not in permitted set. +### 4.2 Operator hold — two horns (program sequencing, not design) -**Candidate placement:** +**Do not pick in this session.** Both horns and their costs are named here; the operator picks. -| Stage | Pros | Cons | +| Horn | What it costs | Execution today | |---|---|---| -| **Infer — direct call resolution** (parallel to record-literal sole_ctor arm) | Same stage as existing sole_ctor; callee + caller module known at call site | **Infer is load-bearing** (DESIGN §7); touches hot path | -| Post-infer dedicated pass | Isolates new logic | Second representation of "who may call whom"; risk of drift from infer call binding | -| Name resolution only | Aligns with "reference edge" | May be insufficient if call shape is not a resolved direct callee (§5) | +| **Land in v1 seed infer** | Grows the thing the v1-deletion program is shrinking: new capability surface + Rust realization lines in hand-maintained `v1_compiler_infer.rs` (and `.dag` infer model). Same class as operator pushback today on adding hundreds of lines to seed files under correct modeling. **But:** wall **executes immediately** on the live corpus path — same as existing `sole_constructor` record-literal refusal. | +| **Land in v2 infer only** | Aligns with self-host direction; does not expand v1 seed. **But:** v2 infer has **no `sole_constructor` today** — the wall does not execute until v2 infer implements construction admission (record literals + call edges) and that stage is what runs for acceptance. A wall that does not execute is specification-without-execution — the failure this lane proved matters. | + +**What v2 would need for the wall to actually execute there (named, not assumed):** + +1. `sole_constructor` record-literal refusal ported into `src/v2/compiler/04_infer.dag` + its realization (capability absent today). +2. `ConstructorReferenceAdmission` call-edge refusal in the **same** v2 infer authority (not a second pass). +3. v2 infer as the stage that runs on the acceptance path for the specimen modules (self-host frontier row — today v1 seed still realizes infer for production typecheck). +4. `ConstructorCallAdmissionRefused` diagnostic in the v2 diagnostic taxonomy (or shared `CompilerDiagnostic` bridge until v2 fully subsumes). + +**What v1 landing would add (named, not estimated to a false precision):** + +- New infer arms in `src/v1/04_infer.dag` for call-edge admission (alongside existing `type_has_sole_constructor` / record-literal arm at ~4099+). +- Rust realization in `v1_compiler_infer.rs` parallel to the existing `SoleConstructorViolation` record-literal block (~8620+). +- New diagnostic variant with constructor, offender caller, permitted-set coordinates. +- Enrollment witnesses proving execute on the **v1** path (already how `sole_constructor` is proven today). + +**Session disposition:** carrier shape, refusal coordinates, composition, first_slice bar, alias stance, and no-separate-pass rule are all decidable without picking the horn. **Implementation waits on operator horn choice.** -**STOP — operator decision required before implementation:** if the honest general case requires infer changes or name-resolution surgery, confirm that placement rather than routing around it. This note does **not** assume a workaround path. +## 5. Design questions (decided or answered in this note) -## 5. Design questions (must be answered in this note before code) +### 5.1 Alias and higher-order positions (operator-approved, msg_a87c2c75) -### 5.1 Alias and higher-order positions +**Approved stance:** outside the modeled guarantee until witnessed; **first slice is direct resolved mint call only.** This is honest ceiling-declaring, not an absorbing fallback. -When the callee is not syntactically the constructor (alias re-export, higher-order parameter, indirect call): +**What unwitnessed alias / HOF calls do TODAY (residual risk, stated plainly):** there is **no** call-edge admission check at all — any importer that resolves a call to `mint_behavioral_comparison_observation` (including through a re-export alias binding to the same declaration) **silently passes** and can forge observation fields. Higher-order and indirect calls where the callee is not syntactically the mint **also pass silently** — no admission machinery exists to refuse them. The first-slice wall covers **direct resolved calls to the listed constructor symbol** only; alias chains and HOF remain **residual forge surface** until falsified. -- **Default honest stance:** outside the modeled guarantee until a witness proves otherwise — refuse or declare `AdmissionUnknown` with typed cause, never silently admit. -- **Direct call to resolved `mint_behavioral_comparison_observation`** is the first-slice scope; alias chains and HOF are explicit follow-on falsification rows. +**Named trigger for alias climb:** first falsification row where a re-export alias binding resolves to the same `DeclarationRef` as the constructor but bypasses admission — if it silently passes, extend the infer call-edge check to follow alias resolution to the constructor `DeclarationRef` (same authority, not a new pass). HOF climb trigger: separate row when a witness shows construction via a function-typed parameter reaching the mint without a direct callee edge. ### 5.2 Composition with `sole_constructor` @@ -109,13 +133,13 @@ Together they close the two routes measured on `BehavioralComparisonObservation` **Proof bar:** green-by-execution on the slice + forge RED flips — not grep, not title claim. -## 7. Phases (no code until note signed) +## 7. Phases (no code until note signed + operator picks compiler horn) -1. **P0 — this note + operator sign-off** on placement (§4) and alias/HOF stance (§5.1). -2. **P1 — model carrier** in `std` (or extend `std.decl_ref`) with nonempty permitted callers by construction. -3. **P2 — compiler refusal** at agreed stage with `ConstructorCallAdmissionRefused` diagnostic. -4. **P3 — first slice wiring** on `BehavioralComparisonObservation` + witness flip for forge RED. -5. **P4 — falsification matrix** continues on other construction forms (`Refined`, casts, variants) on **other carriers** — no generalization from one specimen. +1. **P0 — this note:** operator sign-off on shape; **operator pick v1-seed vs v2 infer horn** (§4.2). +2. **P1 — model carrier** in `std` with nonempty permitted callers; import `decl_ref` from `std.decl_ref`. +3. **P2 — compiler refusal** in the **chosen** infer authority (record literal + call edge, one mechanism — no separate pass). +4. **P3 — first slice wiring** on `BehavioralComparisonObservation` + forge RED flip. +5. **P4 — falsification matrix** on other construction forms and alias/HOF climb triggers. ## 8. Out of scope @@ -126,7 +150,7 @@ Together they close the two routes measured on `BehavioralComparisonObservation` ## 9. Handback -- Signed design note with placement decision. -- `ConstructorReferenceAdmission` carrier + resolved `DeclarationRef` rows for first slice. -- Infer (or agreed stage) refusal with typed diagnostic. +- Signed design note + **operator compiler-horn decision**. +- `ConstructorReferenceAdmission` carrier + resolved `DeclarationRef` rows (imported constructors). +- Infer refusal in chosen compiler (one authority: record literal + call edge). - `fully_matching_derived_seal_forgery_advance_succeeds_red` flipped to refuse on forge path. From 969b01708b5c18e95337971eb0391ba141868f4c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 21:07:46 +0000 Subject: [PATCH 10/22] Add third compiler horn: v1 seed with dissolution trigger. Per msg_039d171e: third row derived from gunbc#7804 operator ruling (seed growth counted with explicit disposition). Dissolution trigger named exactly: compiler_frontier_row_04_infer migration_trigger ^migrate_when_closure_self_emits_cargo_green. still-bat-561 recommends this row; session does not pick. Co-authored-by: Cursor --- .../constructor-reference-admission-design.md | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/docs/plans/constructor-reference-admission-design.md b/docs/plans/constructor-reference-admission-design.md index aa3af9c3c98..93531dfa481 100644 --- a/docs/plans/constructor-reference-admission-design.md +++ b/docs/plans/constructor-reference-admission-design.md @@ -67,14 +67,23 @@ Construction admission is **one authority**. Record-literal refusal and call-edg **This note explicitly rejects a post-infer dedicated pass** as the tempting shape that avoids touching a load-bearing file. Avoiding a load-bearing file is not a design argument; it is the unmarked-workaround class (DESIGN §5). Whatever compiler hosts the wall, record-literal and call-edge checks live in the **same infer construction-admission authority**, beside the existing record-literal `sole_constructor` arm in v1. -### 4.2 Operator hold — two horns (program sequencing, not design) +### 4.2 Operator hold — three horns (program sequencing, not design) -**Do not pick in this session.** Both horns and their costs are named here; the operator picks. +**Do not pick in this session.** Three horns and their costs are named here; the operator picks. still-bat-561 is **recommending the third row** to the operator but has not picked it — this note presents all three. | Horn | What it costs | Execution today | |---|---|---| | **Land in v1 seed infer** | Grows the thing the v1-deletion program is shrinking: new capability surface + Rust realization lines in hand-maintained `v1_compiler_infer.rs` (and `.dag` infer model). Same class as operator pushback today on adding hundreds of lines to seed files under correct modeling. **But:** wall **executes immediately** on the live corpus path — same as existing `sole_constructor` record-literal refusal. | | **Land in v2 infer only** | Aligns with self-host direction; does not expand v1 seed. **But:** v2 infer has **no `sole_constructor` today** — the wall does not execute until v2 infer implements construction admission (record literals + call edges) and that stage is what runs for acceptance. A wall that does not execute is specification-without-execution — the failure this lane proved matters. | +| **Land in v1 seed infer WITH declared dissolution trigger** (operator-ruling shape, gunbc#7804, same day — **not proposed fresh**) | Same seed growth as row 1 (infer `.dag` arms + `v1_compiler_infer.rs` realization for record-literal + call-edge admission). **Plus:** one more **counted** seed-retained obligation that must actually dissolve — not absorbed growth. | **Executes immediately** on the live corpus path (same as row 1). Forge RED flips **by execution**, not in principle. | + +**Third row — what it buys:** the wall runs on today's acceptance path; `fully_matching_derived_seal_forgery_advance_succeeds_red` can flip when the mechanism lands, not when v2 self-host completes in the abstract. + +**Third row — what it costs:** the enumerated v1 infer additions below, **and** a declared `SeedRetained` row with reason + migration trigger that the program must track until dissolution (DESIGN §7 — countable, prioritizable, never a silent escape hatch). + +**Third row — what it owes (named exactly, not reinvented):** dissolution trigger is the **same** frontier row item 3 already points at — `compiler_frontier_row_04_infer` in `src/v2/compiler/self_host/frontier.dag`, `migration_trigger: ^migrate_when_closure_self_emits_cargo_green`. That symbol is the v2 infer self-host frontier row: when `src/v2/compiler/04_infer.dag` closure self-emits cargo-green **and** v2 infer is what runs for production typecheck (not merely modeled), the v1 seed construction-admission block deletes. Disposition text should follow the gunbc#7804 pattern handed back the same afternoon: **not** "do not add Rust to the seed," but **this Rust block carries explicit disposition** — seed realization now, then emitted or native `.dag` realization, then **this block deletes** on the named trigger. + +**Operator ruling source (gunbc#7804, 2026-08-04):** seed growth is not forbidden; it is required to be **counted** — explicit disposition + dissolution trigger, never silent seed expansion. This third row applies that ruling consistently to constructor-reference admission; it is the operator's own rule carried across PRs, not a middle path invented to avoid the fork. **What v2 would need for the wall to actually execute there (named, not assumed):** @@ -90,7 +99,7 @@ Construction admission is **one authority**. Record-literal refusal and call-edg - New diagnostic variant with constructor, offender caller, permitted-set coordinates. - Enrollment witnesses proving execute on the **v1** path (already how `sole_constructor` is proven today). -**Session disposition:** carrier shape, refusal coordinates, composition, first_slice bar, alias stance, and no-separate-pass rule are all decidable without picking the horn. **Implementation waits on operator horn choice.** +**Session disposition:** carrier shape, refusal coordinates, composition, first_slice bar, alias stance, and no-separate-pass rule are all decidable without picking the horn. **Implementation waits on operator choice among the three rows in §4.2.** ## 5. Design questions (decided or answered in this note) @@ -135,7 +144,7 @@ Together they close the two routes measured on `BehavioralComparisonObservation` ## 7. Phases (no code until note signed + operator picks compiler horn) -1. **P0 — this note:** operator sign-off on shape; **operator pick v1-seed vs v2 infer horn** (§4.2). +1. **P0 — this note:** operator sign-off on shape; **operator pick among §4.2 three horns** (still-bat-561 recommends third row with `^migrate_when_closure_self_emits_cargo_green` dissolution). 2. **P1 — model carrier** in `std` with nonempty permitted callers; import `decl_ref` from `std.decl_ref`. 3. **P2 — compiler refusal** in the **chosen** infer authority (record literal + call edge, one mechanism — no separate pass). 4. **P3 — first slice wiring** on `BehavioralComparisonObservation` + forge RED flip. From 0a047ce3ae88bcfeb090e4b3d3caa681ee69d7a3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 21:08:59 +0000 Subject: [PATCH 11/22] Rewrite third horn: land inside already-counted frontier row. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Per msg_4ad6bf45: compiler_frontier_row_04_infer already seed-retained via execution_measured_seed_retained_row — no new row obligation. Cite located_reason ^parse_grammar_choice_overlap_residue, latency while blocker stands (7767/7762), trigger cuts both ways. Co-authored-by: Cursor --- .../constructor-reference-admission-design.md | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/docs/plans/constructor-reference-admission-design.md b/docs/plans/constructor-reference-admission-design.md index 93531dfa481..e3233fa07b0 100644 --- a/docs/plans/constructor-reference-admission-design.md +++ b/docs/plans/constructor-reference-admission-design.md @@ -75,15 +75,19 @@ Construction admission is **one authority**. Record-literal refusal and call-edg |---|---|---| | **Land in v1 seed infer** | Grows the thing the v1-deletion program is shrinking: new capability surface + Rust realization lines in hand-maintained `v1_compiler_infer.rs` (and `.dag` infer model). Same class as operator pushback today on adding hundreds of lines to seed files under correct modeling. **But:** wall **executes immediately** on the live corpus path — same as existing `sole_constructor` record-literal refusal. | | **Land in v2 infer only** | Aligns with self-host direction; does not expand v1 seed. **But:** v2 infer has **no `sole_constructor` today** — the wall does not execute until v2 infer implements construction admission (record literals + call edges) and that stage is what runs for acceptance. A wall that does not execute is specification-without-execution — the failure this lane proved matters. | -| **Land in v1 seed infer WITH declared dissolution trigger** (operator-ruling shape, gunbc#7804, same day — **not proposed fresh**) | Same seed growth as row 1 (infer `.dag` arms + `v1_compiler_infer.rs` realization for record-literal + call-edge admission). **Plus:** one more **counted** seed-retained obligation that must actually dissolve — not absorbed growth. | **Executes immediately** on the live corpus path (same as row 1). Forge RED flips **by execution**, not in principle. | +| **Land in v1 seed infer inside an already-counted frontier row** (operator-ruling shape, gunbc#7804, same day — **not proposed fresh**) | Same seed growth as row 1 (infer `.dag` arms + `v1_compiler_infer.rs` realization for record-literal + call-edge admission). **No new frontier row** — growth enlarges a module **already** enrolled as seed-retained. **Residual latency:** that module is blocked on `^parse_grammar_choice_overlap_residue` (execution-measured; sibling lanes gunbc#7767 and gunbc#7762); trigger `^migrate_when_closure_self_emits_cargo_green` is real but **not imminent** — the wall sits in the seed for as long as that blocker stands. | **Executes immediately** on the live corpus path (same as row 1). Forge RED flips **by execution**, not in principle. | **Third row — what it buys:** the wall runs on today's acceptance path; `fully_matching_derived_seal_forgery_advance_succeeds_red` can flip when the mechanism lands, not when v2 self-host completes in the abstract. -**Third row — what it costs:** the enumerated v1 infer additions below, **and** a declared `SeedRetained` row with reason + migration trigger that the program must track until dissolution (DESIGN §7 — countable, prioritizable, never a silent escape hatch). +**Third row — what it costs:** the enumerated v1 infer additions below. Seed growth is **not** a new obligation invented to justify the landing — it enlarges one module already counted by the self-host frontier. -**Third row — what it owes (named exactly, not reinvented):** dissolution trigger is the **same** frontier row item 3 already points at — `compiler_frontier_row_04_infer` in `src/v2/compiler/self_host/frontier.dag`, `migration_trigger: ^migrate_when_closure_self_emits_cargo_green`. That symbol is the v2 infer self-host frontier row: when `src/v2/compiler/04_infer.dag` closure self-emits cargo-green **and** v2 infer is what runs for production typecheck (not merely modeled), the v1 seed construction-admission block deletes. Disposition text should follow the gunbc#7804 pattern handed back the same afternoon: **not** "do not add Rust to the seed," but **this Rust block carries explicit disposition** — seed realization now, then emitted or native `.dag` realization, then **this block deletes** on the named trigger. +**Third row — existing row (verified, cited by symbol):** `compiler_frontier_row_04_infer` in `src/v2/compiler/self_host/frontier.dag`, constructed by `execution_measured_seed_retained_row` with `module_path: "src/v2/compiler/04_infer.dag"`, `closure_reads: 44`, `measured_blocker: RealizationGap`, `located_stage: ProbeStageAssemble`, `located_reason: ^parse_grammar_choice_overlap_residue`, `migration_trigger: ^migrate_when_closure_self_emits_cargo_green`. Both trigger and reason symbols resolve. This is **not** "add a new declared row and take on a new obligation" — `04_infer` is already seed-retained with an already-named migration trigger and an execution-measured reason for why it has not migrated. Constructor-reference admission would land inside that module's v1 seed realization; the frontier row's contents grow, the row count does not. -**Operator ruling source (gunbc#7804, 2026-08-04):** seed growth is not forbidden; it is required to be **counted** — explicit disposition + dissolution trigger, never silent seed expansion. This third row applies that ruling consistently to constructor-reference admission; it is the operator's own rule carried across PRs, not a middle path invented to avoid the fork. +**Third row — dissolution trigger (named exactly):** `^migrate_when_closure_self_emits_cargo_green` on the row above. When `src/v2/compiler/04_infer.dag` closure self-emits cargo-green **and** v2 infer is what runs for production typecheck, the v1 seed construction-admission block deletes. Disposition follows the gunbc#7804 pattern: **not** "do not add Rust to the seed," but **this Rust block carries explicit disposition** — seed realization now, then emitted or native `.dag` realization, then **this block deletes** on the named trigger. + +**Third row — latency (honest, cuts both ways):** the trigger is real but the module is blocked on `^parse_grammar_choice_overlap_residue` — the **same** residue sibling lanes gunbc#7767 and gunbc#7762 are working on now. An operator choosing this horn should know they are choosing it **with that latency**, not against a vague someday. Read two ways: (1) **weakens** the third horn if the trigger is read as near — dissolution is not imminent while the blocker stands; (2) **strengthens** it if the trigger is read as far — a wall that does not execute until v2 infer self-emits is a wall that does not execute for a long time, which is precisely the second horn's cost, now **quantified** by an execution-measured blocker rather than asserted. + +**Operator ruling source (gunbc#7804, 2026-08-04):** seed growth is not forbidden; it is required to be **counted** — explicit disposition + dissolution trigger, never silent seed expansion. This third row applies that ruling consistently: the counting mechanism already exists and is enrolled on `compiler_frontier_row_04_infer`; it is the operator's own rule carried across PRs, not a middle path invented to avoid the fork. **What v2 would need for the wall to actually execute there (named, not assumed):** @@ -144,7 +148,7 @@ Together they close the two routes measured on `BehavioralComparisonObservation` ## 7. Phases (no code until note signed + operator picks compiler horn) -1. **P0 — this note:** operator sign-off on shape; **operator pick among §4.2 three horns** (still-bat-561 recommends third row with `^migrate_when_closure_self_emits_cargo_green` dissolution). +1. **P0 — this note:** operator sign-off on shape; **operator pick among §4.2 three horns** (still-bat-561 recommends third row — land inside already-counted `compiler_frontier_row_04_infer`). 2. **P1 — model carrier** in `std` with nonempty permitted callers; import `decl_ref` from `std.decl_ref`. 3. **P2 — compiler refusal** in the **chosen** infer authority (record literal + call edge, one mechanism — no separate pass). 4. **P3 — first slice wiring** on `BehavioralComparisonObservation` + forge RED flip. From 8c496e7a6577696b64be984fde83b2c4b3050ccb Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 21:48:43 +0000 Subject: [PATCH 12/22] =?UTF-8?q?WIP:=20Lane=204:=20direct-door=20behavior?= =?UTF-8?q?al=20qualification=20=E2=80=94=20CargoGreen=20to=20BehavioralE?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- dag/gunbc/doc_graph_roots.dag | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/dag/gunbc/doc_graph_roots.dag b/dag/gunbc/doc_graph_roots.dag index 081de5bf7df..e35c3327c53 100644 --- a/dag/gunbc/doc_graph_roots.dag +++ b/dag/gunbc/doc_graph_roots.dag @@ -541,6 +541,16 @@ data hand_authored_doc_binds: List = [ ], 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", From 14e40ff4bb66353e723122fe05b2b6296cfa3d3c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 22:43:10 +0000 Subject: [PATCH 13/22] Record tidy-fox-81 measured floor and over-admission finding. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit §4.3: 110-line .dag floor vs 424-line regen_stage0 realization (~4:1). Module-grain over-admission, opt-in ceiling, three conforming deltas. §5.3: two independent derivations for constructor-side placement. Co-authored-by: Cursor --- .../constructor-reference-admission-design.md | 29 +++++++++++++++++-- 1 file changed, 26 insertions(+), 3 deletions(-) diff --git a/docs/plans/constructor-reference-admission-design.md b/docs/plans/constructor-reference-admission-design.md index e3233fa07b0..3dbfbfd4aa2 100644 --- a/docs/plans/constructor-reference-admission-design.md +++ b/docs/plans/constructor-reference-admission-design.md @@ -105,7 +105,25 @@ Construction admission is **one authority**. Record-literal refusal and call-edg **Session disposition:** carrier shape, refusal coordinates, composition, first_slice bar, alias stance, and no-separate-pass rule are all decidable without picking the horn. **Implementation waits on operator choice among the three rows in §4.2.** -## 5. Design questions (decided or answered in this note) +### 4.3 Measured floor — tidy-fox-81 prototype (#7806, non-conforming) + +**Source:** tidy-fox-81 implemented the v1 horn without the design note (stopped; writeups only). **Not the specified design** — a floor for horn comparison. **Hold stands:** nothing lands until operator picks. + +**Model half (committed `.dag` diff):** 110 changed lines across five files (`00_core`, `02_parse`, `04_infer`, `04_lookup`, `04_sigs`). Parse surface (`admit_callers` property), lookup/sig gate, diagnostic variant — **not** wired to `mint_behavioral_comparison_observation` on that branch. + +**Rust realization half (execution-measured via `regen_stage0`, not inferred):** 424 changed lines across five generated files — `v1_compiler_infer.rs`, `v1_compiler_infer_lookup.rs`, `v1_compiler_infer_sigs.rs`, `v1_compiler_parse.rs`, `v1_std_core.rs`. `v1_compiler_infer.rs` specifically: one new function (~28 lines), two match arms (~12 each), import edit. **Roughly four-to-one model-to-realization amplification.** An operator comparing horns on the `.dag` number alone is comparing the wrong quantity. + +**Still a floor:** conforming to this note costs **strictly more** on **both** halves. Three named deltas still outstanding (each adds model + realization work): + +1. **DeclarationRef grain** — not `module_path` strings (§3 `std.decl_ref` import rule). +2. **One construction-admission authority** — not a separate lookup gate beside `sole_constructor` infer (§4.1). +3. **Resolvable caller identity** — not `caller_module` alone. + +**Over-admission finding (module-grain, separate from typo-resolution):** the prototype compares admitted callers against the **caller's module path**, so admission is **module-grain**: permitting one module permits **every function in it**, now and every function added later — the wall **widens silently** as that module grows; nobody edits `admit_callers` when a new function is added. The annotation names modules; the actual admitted set is whatever those modules currently contain. The admitted set cannot be read off the annotation. **§4b ceiling consequence:** grain determines what the wall admits, not just whether a `DeclarationRef` resolves — stronger than the authoring-time-resolution argument alone. **Named trigger for coverage roster:** enrollment lens over annotated constructors (`admit_callers` / `ConstructorReferenceAdmission` rows) vs `sole_constructor` census. + +**Opt-in semantics (correct, not fail-open):** absent `admit_callers` → call resolves — unannotated functions are not sealed (same class as `sole_constructor`). The measured forgery hole on `mint_behavioral_comparison_observation` stays open on #7806 because **unwired** (one property on one fn), not because the mechanism is unsound. + +**§4b opt-in ceiling:** an opt-in wall tops at **mechanically preventable** — cannot be structurally impossible for carriers nobody annotated. Closes the two measured construction routes **only** for opted-in constructors; coverage is a roster question, not automatic language closure. ### 5.1 Alias and higher-order positions (operator-approved, msg_a87c2c75) @@ -126,9 +144,14 @@ Together they close the two routes measured on `BehavioralComparisonObservation` ### 5.3 Where the permitted list is authored -**Proposal:** admission row lives **on the constructor's declaring module** (beside the type or mint fn), cited by `DeclarationRef` to the constructor symbol. Callers list wet-transport (and test) callers explicitly. +**Proposal:** admission row lives **on the constructor's declaring module** (beside the type or mint fn), cited by `DeclarationRef` to the constructor symbol. Callers list wet-transport (and test) callers explicitly at **declaration grain** (`DeclarationRef` per permitted caller fn), not module grain — see §4.3 over-admission finding. + +**Two independent derivations agreeing on constructor-side placement (not one measurement confirming the other):** + +1. **First principles (this note):** the constructor is the sealed symbol; the permitted set is metadata **about** who may invoke that constructor — it belongs beside the constructor declaration. +2. **Structural (tidy-fox-81 #7806 check site):** the admission check already holds the constructor's declaration node and both module paths at the call site — permitted list is one field read on the callee. Caller-side placement would need the caller's own declaration node and new plumbing. Constructor-side is cheaper for a structural reason, not merely a preference. -**Module move:** `DeclarationRef` uses `module_path` + `decl_name` — if a permitted caller moves modules, the ref must be updated (same as any `DeclarationRef` row); no path-inferred auto-permission. +**Module move:** `DeclarationRef` uses `module_path` + `decl_name` — if a permitted caller moves modules, the ref must be updated (same as any `DeclarationRef` row); no path-inferred auto-permission. **Module-path admission is over-admission** (§4.3): it silently widens as the permitted module grows. ### 5.4 Compiler-module exemptions From d9b7702aa5576e56cf39ce886e36b79c419ad529 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 22:45:10 +0000 Subject: [PATCH 14/22] Cite func_sig_from_global_bare in placement and over-admission text. Fold tidy-fox-81 writeup phrasing: structural asymmetry at check site, module-grain precision degrading over time. Co-authored-by: Cursor --- docs/plans/constructor-reference-admission-design.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/docs/plans/constructor-reference-admission-design.md b/docs/plans/constructor-reference-admission-design.md index 3dbfbfd4aa2..ad302fbb0bb 100644 --- a/docs/plans/constructor-reference-admission-design.md +++ b/docs/plans/constructor-reference-admission-design.md @@ -119,12 +119,14 @@ Construction admission is **one authority**. Record-literal refusal and call-edg 2. **One construction-admission authority** — not a separate lookup gate beside `sole_constructor` infer (§4.1). 3. **Resolvable caller identity** — not `caller_module` alone. -**Over-admission finding (module-grain, separate from typo-resolution):** the prototype compares admitted callers against the **caller's module path**, so admission is **module-grain**: permitting one module permits **every function in it**, now and every function added later — the wall **widens silently** as that module grows; nobody edits `admit_callers` when a new function is added. The annotation names modules; the actual admitted set is whatever those modules currently contain. The admitted set cannot be read off the annotation. **§4b ceiling consequence:** grain determines what the wall admits, not just whether a `DeclarationRef` resolves — stronger than the authoring-time-resolution argument alone. **Named trigger for coverage roster:** enrollment lens over annotated constructors (`admit_callers` / `ConstructorReferenceAdmission` rows) vs `sole_constructor` census. +**Over-admission finding (module-grain, separate from typo-resolution):** the prototype's check in `func_sig_from_global_bare` compares admitted callers against the **caller's module path**, so admission is **module-grain**: permitting one module permits **every function in it**, now and every function added later — the wall **widens silently** as that module grows; nobody edits `admit_callers` when a new function is added. The annotation names modules; the actual admitted set is whatever those modules currently contain. The admitted set cannot be read off the annotation. **§4b ceiling consequence:** precision is bounded by module size and **degrades over time** — grain determines what the wall admits, not just whether a `DeclarationRef` resolves — stronger than the authoring-time-resolution argument alone. **Named trigger for coverage roster:** enrollment lens over annotated constructors (`admit_callers` / `ConstructorReferenceAdmission` rows) vs `sole_constructor` census. **Opt-in semantics (correct, not fail-open):** absent `admit_callers` → call resolves — unannotated functions are not sealed (same class as `sole_constructor`). The measured forgery hole on `mint_behavioral_comparison_observation` stays open on #7806 because **unwired** (one property on one fn), not because the mechanism is unsound. **§4b opt-in ceiling:** an opt-in wall tops at **mechanically preventable** — cannot be structurally impossible for carriers nobody annotated. Closes the two measured construction routes **only** for opted-in constructors; coverage is a roster question, not automatic language closure. +## 5. Design questions (decided or answered in this note) + ### 5.1 Alias and higher-order positions (operator-approved, msg_a87c2c75) **Approved stance:** outside the modeled guarantee until witnessed; **first slice is direct resolved mint call only.** This is honest ceiling-declaring, not an absorbing fallback. @@ -149,7 +151,7 @@ Together they close the two routes measured on `BehavioralComparisonObservation` **Two independent derivations agreeing on constructor-side placement (not one measurement confirming the other):** 1. **First principles (this note):** the constructor is the sealed symbol; the permitted set is metadata **about** who may invoke that constructor — it belongs beside the constructor declaration. -2. **Structural (tidy-fox-81 #7806 check site):** the admission check already holds the constructor's declaration node and both module paths at the call site — permitted list is one field read on the callee. Caller-side placement would need the caller's own declaration node and new plumbing. Constructor-side is cheaper for a structural reason, not merely a preference. +2. **Structural (tidy-fox-81 #7806, discovered by building):** `func_sig_from_global_bare` already holds the constructor's declaration node and both module paths at the check site — reading `admit_callers` there is one more field read. Caller-side placement would need the caller's own declaration node resolved at that same site — plumbing that does not exist yet. Constructor-side is cheaper for a **structural** reason, not a preference. **Module move:** `DeclarationRef` uses `module_path` + `decl_name` — if a permitted caller moves modules, the ref must be updated (same as any `DeclarationRef` row); no path-inferred auto-permission. **Module-path admission is over-admission** (§4.3): it silently widens as the permitted module grows. From 3ef7f547bd7a9939a66ca917791ec931aeba9e7c Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 23:15:36 +0000 Subject: [PATCH 15/22] Fold wise-ram-22 joint findings into design note. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit §1.1 orthogonal WHO vs WHAT mechanisms; bound on capability scope. A-prime v2 uncovered path; census taxonomy §5.5; origin coproduct split. Credit v2 zero sole_constructor rung correction. Co-authored-by: Cursor --- .../constructor-reference-admission-design.md | 37 ++++++++++++++++++- 1 file changed, 35 insertions(+), 2 deletions(-) diff --git a/docs/plans/constructor-reference-admission-design.md b/docs/plans/constructor-reference-admission-design.md index ad302fbb0bb..59fa42e9320 100644 --- a/docs/plans/constructor-reference-admission-design.md +++ b/docs/plans/constructor-reference-admission-design.md @@ -23,9 +23,26 @@ Specimen: `v2.compiler.self_host.behavioral_comparison_receipt` `BehavioralCompa | Opaque host-effect return | **NEGATIVE** | `WitnessBin.Run` returns forgeable `String`/`Bool` fields | | Process-output `sole_constructor` carrier (#7794) | **DECORATIVE** | Forge via `from_run_fields` / `hermetic_equivalent` | -**Closing both refused + leaking routes** requires a capability beyond `sole_constructor` alone. **Legitimate wet transport** (`tools.direct_rust_door_transport`) must remain admitted after the wall lands. +**Closing both refused + leaking routes on the behavioral-comparison specimen** requires capabilities beyond `sole_constructor` alone — call-edge admission plus (for fixture-origin parameter types) the orthogonal carrier wise-ram-22 models. **Legitimate wet transport** (`tools.direct_rust_door_transport`) must remain admitted after the wall lands. -## 2. End shape (carrier) +### 1.1 Joint with wise-ram-22 — orthogonal mechanisms (msg_e499e35c) + +**wise-ram-22** (`FixtureOriginCanMintProductionQualification`, measured on direct-door): hand-authored `InferredTree` **accepted** by `mint_provenanced_rust_artifact`; `infer(assemble(direct_rust_door_ingest()))` **rejected** — production qualification reachable from fixture-origin input while the real pipeline cannot obtain it. + +**Clean division (both notes required reading):** + +| Mechanism | Question it answers | Authority | +|---|---|---| +| **ConstructorReferenceAdmission** (this note) | **WHO may construct** — which callers may invoke a sealed constructor | Call-edge + opt-in roster | +| **CompilerInferredArtifact + inference receipt** (wise-ram-22 B0 §1) | **WHAT may be constructed from** — parameter types that must carry compiler-derived provenance | Stage-origin carrier | + +**Orthogonal and both required:** a production qualification reachable by a **permitted** caller from a **fixture-origin** value is refused by **neither alone**. Call-edge admission does **not** close wise-ram-22's class: the direct-door specimen is a permitted caller supplying a hand-authored `InferredTree` to a mint whose signature legitimately accepts one — the caller is not the problem; the discarded epistemic distinction in the **parameter type** is. + +**Stronger adjacent case (wise-ram-22 census):** cargo may compile bytes and a behavioral corpus may **genuinely execute** them while the bytes came from a **substitute subject** — evidence is **real about the wrong subject** (nastier than checksum-derived seals without execution witness in §0). + +**Rung correction (wise-ram-22, credited):** `src/v2/compiler/04_infer.dag` has **zero** `sole_constructor` handling — marker modeled in v2 source, refusal executes on **v1 seed path only**. Claiming "mechanically preventable on covered form" without per-path split is **rung inflation** (DESIGN §4b(1): minimum across in-scope paths). + +**Origin coproduct warning (wise-ram-22 B0 correction — load-bearing for CargoGreen→BehavioralEquivalent):** do **not** put `ExecutionMeasured` as a sibling of `CompilerDerived` | `FixtureDerived` in a production-origin coproduct. A fixture-derived artifact can **also** be execution-measured — that is exactly the dangerous state. Split axes: `ProductionStageOrigin = CompilerDerived | FixtureDerived | UnknownOrigin` and `ProductionEvidenceGrounding = StructurallyGrounded | ExecutionMeasured{receipt} | Unmeasured`. Measurement **carries** an origin; it does not replace one. ```dag import std.decl_ref { DeclarationRef, decl_ref, decl_field_ref } @@ -159,6 +176,22 @@ Together they close the two routes measured on `BehavioralComparisonObservation` `sole_constructor` carries compiler-module check exemptions (unverified completeness). **ConstructorReferenceAdmission must not inherit exemptions by default.** If an exemption is needed, it is a named row with dissolution trigger — never silent skip inside `v2.compiler` / `v1.compiler` trees. +### 5.5 Census disposition taxonomy (wise-ram-22 / keen-lark-681 exchange) + +Classified **specimens** — denominator not closed; keen-lark-681 successor owes full population. Dispositions for operator packet: + +| Tag | Meaning | Notes | +|---|---|---| +| **A (v1 path)** | Cross-module record literal refused on `sole_constructor` types | **v1 infer only**; narrower than it reads (file-identity scope, fail-open lookup miss on uncovered paths) | +| **A-prime (v2 path)** | Same construction on **v2 infer path** | **Uncovered** — not A; zero `sole_constructor` handling in `src/v2/compiler/04_infer.dag` today | +| **B** | Closable after `ConstructorReferenceAdmission` | Opted-in constructor mints; declaration-grain `DeclarationRef` permitted callers; roster enrollment | +| **C — fixture-origin parameter** | `mint_provenanced_rust_artifact` accepting bare `InferredTree` | **Not** this capability; wise-ram-22 B0 §1 (`CompilerInferredArtifact` + inference receipt) | +| **C — real execution, wrong subject** | Downstream compile/run succeeds on substitute subject bytes | Adjacent to checksum seals; evidence genuine about wrong subject | +| **C — other** | `WitnessBin.Run` forgeable strings; decorative process-output `sole_constructor`; checksum-derived seals without execution witness | See §1 table | +| **D** | Residual after B | Alias/HOF; module-grain over-admission if mis-implemented; **subject discontinuity** (qualification assembled from receipts carrying different subjects — B0 §2 chain property, not visible to either admission mechanism alone) | + +**Do not overstate B:** ConstructorReferenceAdmission does not close wise-ram-22's FixtureOrigin class or the direct-door permitted-caller + hand-authored tree specimen. + ## 6. First slice (already written — executable acceptance) **Subject:** `mint_behavioral_comparison_observation` → `BehavioralComparisonObservation`. From c5517e15449dd424a7a63f81b67e8051129962a3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 4 Aug 2026 23:27:45 +0000 Subject: [PATCH 16/22] =?UTF-8?q?Tag=20keen-lark-681=20draft=20census=20ro?= =?UTF-8?q?ws=20in=20design=20note=20=C2=A75.5.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Disposition table for origin probe @ 27e516ce; confirm A-prime scope split vs sole_constructor literal census. Co-authored-by: Cursor --- .../constructor-reference-admission-design.md | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/docs/plans/constructor-reference-admission-design.md b/docs/plans/constructor-reference-admission-design.md index 59fa42e9320..8ad8305f3cc 100644 --- a/docs/plans/constructor-reference-admission-design.md +++ b/docs/plans/constructor-reference-admission-design.md @@ -192,7 +192,22 @@ Classified **specimens** — denominator not closed; keen-lark-681 successor owe **Do not overstate B:** ConstructorReferenceAdmission does not close wise-ram-22's FixtureOrigin class or the direct-door permitted-caller + hand-authored tree specimen. -## 6. First slice (already written — executable acceptance) +**keen-lark-681 draft rows tagged (msg_2eaf0857, probe @ `27e516ce` — entry-closure scoped, NOT closed population):** + +| # | Surface | §5.5 tag(s) | Notes | +|---|---|---|---| +| 1 | `candidate_generation.mint_provenanced_rust_artifact` | **C — fixture-origin parameter** | B may roster call edges on this mint but **does not close C** | +| 2 | `candidate_generation.mint_written_provenanced_rust_artifact` | **C — fixture-origin parameter** | Same as (1) via wrapper | +| 3 | `candidate_generation.generate_provenanced_rust_candidate_from_ingest` | **—** (not C at caller) | Real-pipeline caller; fixture risk is parameter type at (1). **A-prime: N/A** (call, not record literal) — agreed | +| 4 | `candidate_generation.advance_written_provenanced_rust_artifact_cargo_green` | **C — fixture-origin parameter** (derivative); **C — real execution, wrong subject** when cargo greens on substitute-subject bytes | Inherits upstream origin | +| 5 | `tools.direct_rust_door_transport.run_direct_rust_door_emit_write_compile_smoke` | **C — fixture-origin parameter**; **C — real execution, wrong subject** (when cargo greens) | Primary measured direct-door specimen | +| 6 | `production_qualification_origin_probe_structural_fixture.structural_red_control_mint_site_probe` | Same as (5) | Test scaffold; probe control until G2 marshal exposes callees | +| 7–10 | Synthetic classifier controls | **Probe enrollment** (not live census) | Oracle rows for classifier proof only | +| 11 | `behavioral_comparison_receipt` `BehavioralComparisonObservation` + `mint_behavioral_comparison_observation` | **A (v1)** record literal; **A-prime (v2)** uncovered; **B** exported mint call leak | §1 specimen; first_slice target | +| 12 | `WitnessBin.Run` opaque returns | **C — other** | Forgeable strings | +| 13 | Process-output `sole_constructor` (#7794) | **C — other** | Decorative reshuffle | + +**A/A-prime denominator:** origin probe does **not** discover `sole_constructor` record-literal sites today — correct scope split. **Recommend parallel census** (or dedicated v2-path discovery witness) for A/A-prime population; do not fold into origin probe unless one closure scan is explicitly scoped for both axes. **Subject:** `mint_behavioral_comparison_observation` → `BehavioralComparisonObservation`. From a8695d2bc52741067af81ac90463421671046553 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 5 Aug 2026 02:46:52 +0000 Subject: [PATCH 17/22] Record operator ruling msg_1a57418c in ConstructorReferenceAdmission design note. Parked disposition for #7792/#7794, #7806 model-only scaffold custody, and the seven-step enforcement sequence so the horn-pick packet matches the operator's ruling. Co-authored-by: Cursor --- .../constructor-reference-admission-design.md | 37 ++++++++++++++----- 1 file changed, 27 insertions(+), 10 deletions(-) diff --git a/docs/plans/constructor-reference-admission-design.md b/docs/plans/constructor-reference-admission-design.md index 8ad8305f3cc..5e3b89b9908 100644 --- a/docs/plans/constructor-reference-admission-design.md +++ b/docs/plans/constructor-reference-admission-design.md @@ -1,10 +1,10 @@ # ConstructorReferenceAdmission — reference-edge admission for sealed constructors -**Status:** DRAFT for operator review (2026-08-04, royal-crab-235, msg_13fbbaaf / node `adhoc-f519571b-764`; updated msg_a87c2c75). **No code lands from this note** until the shape is agreed and the **which-compiler** horn is operator-picked (§4). Owner: royal-crab-235. +**Status:** DRAFT for operator review (2026-08-04, royal-crab-235, msg_13fbbaaf / node `adhoc-f519571b-764`; updated msg_a87c2c75, operator ruling msg_1a57418c). **No code lands from this note** until the shape is agreed and the **which-compiler** horn is operator-picked (§4). Owner: royal-crab-235 (custody of tidy-fox-81 #7806 scaffold as of msg_1a57418c consolidation). -**Origin:** Executed falsification (royal-crab-235, msg_6701c04d): `sole_constructor` refuses cross-module **record literals** but does **not** refuse cross-module **calls** to an exported mint with caller-supplied fields; legitimate wet transport requires that mint. Process-output carrier reshuffle and opaque `WitnessBin.Run` output do not close the hole. **Derived ceiling:** `can-climb-after-one-capability`. **Preferred trigger:** this capability. +**Origin:** Executed falsification (royal-crab-235, msg_6701c04d): `sole_constructor` refuses cross-module **record literals** but does **not** refuse cross-module **calls** to an exported mint with caller-supplied fields; legitimate wet transport requires that mint. Process-output carrier reshuffle and opaque `WitnessBin.Run` output do not close the hole. **Derived ceiling:** `can-climb-after-a-capability` (not can-climb-now). **Preferred trigger:** this capability. -**Evidence PRs (draft, do not merge claiming `FixtureBehaviorallyEquivalent`):** #7792, #7794. +**Evidence PRs (draft, parked — operator ruling msg_1a57418c):** #7792, #7794 remain capability-audit/falsification records; **do not merge** with `FixtureBehaviorallyEquivalent` as terminal claim. May stay as falsification records or non-authorizing caller-supplied observation experiments. **Not** a docs-only merge under that claim. Dashboard disposition: *green, draft, do-not-merge falsification record; not pending merge work.* ## 0. Displaced cost @@ -122,7 +122,9 @@ Construction admission is **one authority**. Record-literal refusal and call-edg **Session disposition:** carrier shape, refusal coordinates, composition, first_slice bar, alias stance, and no-separate-pass rule are all decidable without picking the horn. **Implementation waits on operator choice among the three rows in §4.2.** -### 4.3 Measured floor — tidy-fox-81 prototype (#7806, non-conforming) +### 4.3 Model-only scaffold — tidy-fox-81 prototype (#7806, non-conforming; custody royal-crab-235) + +**Operator ruling (msg_1a57418c):** #7806 is a **model-only capability scaffold** — must **not** claim enforcement without a **production consumer**. Keep draft (or title explicitly as capability model). A model-only carrier with no compiler consumer is coverage-by-illusion. **Consolidation:** tidy-fox-81 closed; #7806 parked artifact custody transfers to royal-crab-235 (same lane, horn-blocked — custody not active implementation). **Source:** tidy-fox-81 implemented the v1 horn without the design note (stopped; writeups only). **Not the specified design** — a floor for horn comparison. **Hold stands:** nothing lands until operator picks. @@ -142,6 +144,20 @@ Construction admission is **one authority**. Record-literal refusal and call-edg **§4b opt-in ceiling:** an opt-in wall tops at **mechanically preventable** — cannot be structurally impossible for carriers nobody annotated. Closes the two measured construction routes **only** for opted-in constructors; coverage is a roster question, not automatic language closure. +**Explicit-import bypass (review 48287, operator sequence step 3):** `lookup_func_sig` reaches `func_sig_from_global_bare` — and therefore `admit_callers` — only on the census-fallback path. Callers with an explicit `import` resolve via import-closure and **never consult admission**. This is **not** a nit to defer on #7806; it is step 3 of the real implementation (unified post-resolution check at call-edge construction). tidy-fox-81 correctly declined implementing it on a branch that must not land. + +### 4.4 Implementation sequence when horn unblocks (operator ruling msg_1a57418c) + +**Enforcement status today:** `NotEnforced` — do not flip until the sequence completes on a production consumer. + +1. Reuse exact declaration/reference identities from the binding substrate (`std.decl_ref` — §3 import rule). +2. At **call-edge construction**, carry caller declaration, callee declaration, and referenced constructor. +3. When the callee is sealed, require the caller in the **exact** admission roster (unified authority — closes explicit-import bypass; §4.1 one mechanism, not lookup-only). +4. Refuse an unlisted edge with a typed diagnostic (`ConstructorCallAdmissionRefused` coordinates — §2). +5. Add a real cross-module exported-function forgery RED (`fully_matching_derived_seal_forgery_advance_succeeds_red` flips). +6. Add a positive admitted-host-transport control (wet path caller listed). +7. **Only then** change enforcement from `NotEnforced`. + ## 5. Design questions (decided or answered in this note) ### 5.1 Alias and higher-order positions (operator-approved, msg_a87c2c75) @@ -219,13 +235,14 @@ Classified **specimens** — denominator not closed; keen-lark-681 successor owe **Proof bar:** green-by-execution on the slice + forge RED flips — not grep, not title claim. -## 7. Phases (no code until note signed + operator picks compiler horn) +## 7. Phases (no enforcement until note signed + operator picks compiler horn + §4.4 sequence complete) -1. **P0 — this note:** operator sign-off on shape; **operator pick among §4.2 three horns** (still-bat-561 recommends third row — land inside already-counted `compiler_frontier_row_04_infer`). -2. **P1 — model carrier** in `std` with nonempty permitted callers; import `decl_ref` from `std.decl_ref`. -3. **P2 — compiler refusal** in the **chosen** infer authority (record literal + call edge, one mechanism — no separate pass). -4. **P3 — first slice wiring** on `BehavioralComparisonObservation` + forge RED flip. -5. **P4 — falsification matrix** on other construction forms and alias/HOF climb triggers. +1. **P0 — this note:** operator sign-off on shape; **operator pick among §4.2 three horns** (recommendation exists in packet — still-bat-561 + royal-crab-235; operator reads packet, not summary). +2. **P1 — model carrier** in `std` with nonempty permitted callers; import `decl_ref` from `std.decl_ref` (#7806 is a non-conforming floor for one horn — not production enforcement). +3. **P2 — compiler refusal** per §4.4 steps 1–4 in the **chosen** infer authority (record literal + call edge, one mechanism — no separate pass). +4. **P3 — witnesses** per §4.4 steps 5–6 on `BehavioralComparisonObservation` + forge RED flip. +5. **P4 — enforcement flip** per §4.4 step 7 (`NotEnforced` → enforced only after witnesses green). +6. **P5 — falsification matrix** on other construction forms and alias/HOF climb triggers. ## 8. Out of scope From 5e401b551dff31474f72e62f56eefccc28dfdefc Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 5 Aug 2026 03:53:48 +0000 Subject: [PATCH 18/22] =?UTF-8?q?WIP:=20Lane=204:=20direct-door=20behavior?= =?UTF-8?q?al=20qualification=20=E2=80=94=20CargoGreen=20to=20BehavioralE?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...roadmap_program_view_live_witness_test.dag | 95 +++++++++++++++++++ .../roadmap_program_view_witness_test.dag | 1 - 2 files changed, 95 insertions(+), 1 deletion(-) create mode 100644 dag/test/claim/long/roadmap_program_view_live_witness_test.dag diff --git a/dag/test/claim/long/roadmap_program_view_live_witness_test.dag b/dag/test/claim/long/roadmap_program_view_live_witness_test.dag new file mode 100644 index 00000000000..2a224bb6239 --- /dev/null +++ b/dag/test/claim/long/roadmap_program_view_live_witness_test.dag @@ -0,0 +1,95 @@ +module test.claim.long.roadmap_program_view_live + +import std.types { String, Bool, List } +import gunbc.roadmap_program_view { + program_front_key, + FinishLineView, V1DeletionProgramView, + V1ProgramViewResult, ProgramViewDerived, ProgramViewRefused, + v1_program_view, +} +import gunbc.roadmap_model { RoadmapAcceptanceReceipt } +import gunbc.roadmap_authority { + declared_roadmap_nodes, declared_roadmap_edges, roadmap_acceptance_receipts, + RoadmapAcceptanceReceiptsProjected, + RoadmapAcceptanceReceiptsProjectionRefused, +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data roadmap_program_view_live_witness_note: String = "Live-tree joins for gunbc.roadmap_program_view (operator 5s rule 2026-07-12): v1_program_view over declared_roadmap_nodes/edges + roadmap_acceptance_receipts exceeds the per-PR discovery fast-lane eval budget as the roadmap corpus grows — witness_live_constraint_present_iff_line_unaccepted measured 5021ms on PR #7792 CI (2026-08-05). Identity-grain facts only: finish lines and gates resolve, contributing-front sets match derived membership, accepted-iff-no-constraint holds both directions. No live count pinned. LOCAL RECIPE: claim_batch --source-root dag --source-root src/v2 --entry dag/test/claim/long/roadmap_program_view_live_witness_test.dag --functions witness_live_program_view_derives_and_gates_resolve,witness_live_contributing_fronts_are_the_derived_sets,witness_live_every_front_contributes_to_some_line,witness_live_constraint_present_iff_line_unaccepted" + +fn live_receipts() -> List { + match roadmap_acceptance_receipts() { + RoadmapAcceptanceReceiptsProjected { receipts: receipts } => receipts + RoadmapAcceptanceReceiptsProjectionRefused { detail: _ } => [] + } +} + +fn live_view() -> V1ProgramViewResult { + v1_program_view( + nodes: declared_roadmap_nodes(), + edges: declared_roadmap_edges(), + receipts: live_receipts(), + in_flight: [], + ) +} + +fn live_line_front_keys(view: V1DeletionProgramView, line_key: String) -> List { + fold(view.finish_lines, init: [], f: (acc, lv) => + if lv.key == line_key { + lv.contributing_fronts |> map(c => program_front_key(front: c)) + } else { acc }) +} + +fn live_front_keys_are(view: V1DeletionProgramView, line_key: String, expected: List) -> Bool { + live_line_front_keys(view: view, line_key: line_key) == expected +} + +test fn witness_live_program_view_derives_and_gates_resolve() -> Bool { + match live_view() { + ProgramViewDerived { view } => + count(view.finish_lines) == 4 && count(view.fronts) == 5 + ProgramViewRefused { causes: _ } => false + } +} + +test fn witness_live_contributing_fronts_are_the_derived_sets() -> Bool { + match live_view() { + ProgramViewRefused { causes: _ } => false + ProgramViewDerived { view } => + live_front_keys_are(view: view, line_key: "compiler-fixed-point", + expected: [ "namespace-pderive", "v2-generation" ]) + && live_front_keys_are(view: view, line_key: "interpreter-deleted", + expected: [ "namespace-pderive", "v2-generation", "materialization-cutover" ]) + && live_front_keys_are(view: view, line_key: "products-v1-free", + expected: [ "namespace-pderive", "v2-generation", "honest-frontier", "materialization-cutover" ]) + && live_front_keys_are(view: view, line_key: "zero-hand-maintained-rust", + expected: [ "namespace-pderive", "v2-generation", "honest-frontier", "materialization-cutover", "test-migration-tail" ]) + } +} + +test fn witness_live_every_front_contributes_to_some_line() -> Bool { + match live_view() { + ProgramViewRefused { causes: _ } => false + ProgramViewDerived { view } => + all(view.fronts, fv => + any(view.finish_lines, lv => + lv.contributing_fronts |> any(c => program_front_key(front: c) == fv.key))) + } +} + +fn probe_constraint_iff(lv: FinishLineView) -> Bool { + match lv.constraint { + Absent => lv.accepted + Present { value: _ } => !lv.accepted + } +} + +test fn witness_live_constraint_present_iff_line_unaccepted() -> Bool { + match live_view() { + ProgramViewRefused { causes: _ } => false + ProgramViewDerived { view } => + all(view.finish_lines, lv => probe_constraint_iff(lv: lv)) + } +} diff --git a/dag/test/claim/roadmap_program_view_witness_test.dag b/dag/test/claim/roadmap_program_view_witness_test.dag index 55a7d7bddc4..f80ad31b90d 100644 --- a/dag/test/claim/roadmap_program_view_witness_test.dag +++ b/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 => From f10607f507f17ad4be58bf007a134ab3af243ae3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 5 Aug 2026 17:40:32 +0000 Subject: [PATCH 19/22] Remove superseded roadmap_program_view live long-lane witnesses. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The four witnesses in long/roadmap_program_view_live_witness_test.dag were UnclassifiedPathDeferral — enrolled in discovery with no executing cadence. Live integration is covered by roadmap_program_view_live_corpus_receipt_test. Co-authored-by: Cursor --- ...roadmap_program_view_live_witness_test.dag | 95 ------------------- 1 file changed, 95 deletions(-) delete mode 100644 dag/test/claim/long/roadmap_program_view_live_witness_test.dag diff --git a/dag/test/claim/long/roadmap_program_view_live_witness_test.dag b/dag/test/claim/long/roadmap_program_view_live_witness_test.dag deleted file mode 100644 index 2a224bb6239..00000000000 --- a/dag/test/claim/long/roadmap_program_view_live_witness_test.dag +++ /dev/null @@ -1,95 +0,0 @@ -module test.claim.long.roadmap_program_view_live - -import std.types { String, Bool, List } -import gunbc.roadmap_program_view { - program_front_key, - FinishLineView, V1DeletionProgramView, - V1ProgramViewResult, ProgramViewDerived, ProgramViewRefused, - v1_program_view, -} -import gunbc.roadmap_model { RoadmapAcceptanceReceipt } -import gunbc.roadmap_authority { - declared_roadmap_nodes, declared_roadmap_edges, roadmap_acceptance_receipts, - RoadmapAcceptanceReceiptsProjected, - RoadmapAcceptanceReceiptsProjectionRefused, -} -import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } - -data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly - -data roadmap_program_view_live_witness_note: String = "Live-tree joins for gunbc.roadmap_program_view (operator 5s rule 2026-07-12): v1_program_view over declared_roadmap_nodes/edges + roadmap_acceptance_receipts exceeds the per-PR discovery fast-lane eval budget as the roadmap corpus grows — witness_live_constraint_present_iff_line_unaccepted measured 5021ms on PR #7792 CI (2026-08-05). Identity-grain facts only: finish lines and gates resolve, contributing-front sets match derived membership, accepted-iff-no-constraint holds both directions. No live count pinned. LOCAL RECIPE: claim_batch --source-root dag --source-root src/v2 --entry dag/test/claim/long/roadmap_program_view_live_witness_test.dag --functions witness_live_program_view_derives_and_gates_resolve,witness_live_contributing_fronts_are_the_derived_sets,witness_live_every_front_contributes_to_some_line,witness_live_constraint_present_iff_line_unaccepted" - -fn live_receipts() -> List { - match roadmap_acceptance_receipts() { - RoadmapAcceptanceReceiptsProjected { receipts: receipts } => receipts - RoadmapAcceptanceReceiptsProjectionRefused { detail: _ } => [] - } -} - -fn live_view() -> V1ProgramViewResult { - v1_program_view( - nodes: declared_roadmap_nodes(), - edges: declared_roadmap_edges(), - receipts: live_receipts(), - in_flight: [], - ) -} - -fn live_line_front_keys(view: V1DeletionProgramView, line_key: String) -> List { - fold(view.finish_lines, init: [], f: (acc, lv) => - if lv.key == line_key { - lv.contributing_fronts |> map(c => program_front_key(front: c)) - } else { acc }) -} - -fn live_front_keys_are(view: V1DeletionProgramView, line_key: String, expected: List) -> Bool { - live_line_front_keys(view: view, line_key: line_key) == expected -} - -test fn witness_live_program_view_derives_and_gates_resolve() -> Bool { - match live_view() { - ProgramViewDerived { view } => - count(view.finish_lines) == 4 && count(view.fronts) == 5 - ProgramViewRefused { causes: _ } => false - } -} - -test fn witness_live_contributing_fronts_are_the_derived_sets() -> Bool { - match live_view() { - ProgramViewRefused { causes: _ } => false - ProgramViewDerived { view } => - live_front_keys_are(view: view, line_key: "compiler-fixed-point", - expected: [ "namespace-pderive", "v2-generation" ]) - && live_front_keys_are(view: view, line_key: "interpreter-deleted", - expected: [ "namespace-pderive", "v2-generation", "materialization-cutover" ]) - && live_front_keys_are(view: view, line_key: "products-v1-free", - expected: [ "namespace-pderive", "v2-generation", "honest-frontier", "materialization-cutover" ]) - && live_front_keys_are(view: view, line_key: "zero-hand-maintained-rust", - expected: [ "namespace-pderive", "v2-generation", "honest-frontier", "materialization-cutover", "test-migration-tail" ]) - } -} - -test fn witness_live_every_front_contributes_to_some_line() -> Bool { - match live_view() { - ProgramViewRefused { causes: _ } => false - ProgramViewDerived { view } => - all(view.fronts, fv => - any(view.finish_lines, lv => - lv.contributing_fronts |> any(c => program_front_key(front: c) == fv.key))) - } -} - -fn probe_constraint_iff(lv: FinishLineView) -> Bool { - match lv.constraint { - Absent => lv.accepted - Present { value: _ } => !lv.accepted - } -} - -test fn witness_live_constraint_present_iff_line_unaccepted() -> Bool { - match live_view() { - ProgramViewRefused { causes: _ } => false - ProgramViewDerived { view } => - all(view.finish_lines, lv => probe_constraint_iff(lv: lv)) - } -} From 7cfe975a623e1f4fcff0a938a55ffa473619e0a8 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 6 Aug 2026 04:44:19 +0000 Subject: [PATCH 20/22] =?UTF-8?q?WIP:=20Lane=204:=20direct-door=20behavior?= =?UTF-8?q?al=20qualification=20=E2=80=94=20CargoGreen=20to=20BehavioralE?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- dag/tools/direct_rust_door_transport.dag | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/dag/tools/direct_rust_door_transport.dag b/dag/tools/direct_rust_door_transport.dag index 5500269c740..139956561de 100644 --- a/dag/tools/direct_rust_door_transport.dag +++ b/dag/tools/direct_rust_door_transport.dag @@ -5,6 +5,7 @@ import extdeps.filesystem.filesystem_io { Filesystem } import extdeps.git.inspect import extdeps.gunbc import extdeps.shell +import gunbc.output_policy { ExpectFailure } import v2.compiler.self_host.behavioral_comparison_receipt { AdmittedBehaviorEquivalent, AdmittedBehaviorEquivalentReceipt, @@ -124,7 +125,8 @@ fn direct_rust_door_admitted_equivalent_for_workspace( let fault_run = gunbc.WitnessBin.Run( workdir: workspace_dir, bin_path: witness_bin_path, - args: ["--inject-fault"] + args: ["--inject-fault"], + expect: ExpectFailure ) let executable_read = Filesystem.Read(path: witness_bin_path) let head = git.Inspect.HeadCommit() @@ -163,7 +165,11 @@ fn direct_rust_door_subtract_admission_for_workspace( if !direct_rust_door_prepare_behavioral_witness_workspace(workspace_dir: workspace_dir) { optional_absent() } else { - let pass_run = gunbc.WitnessBin.Run(workdir: workspace_dir, bin_path: witness_bin_path) + let pass_run = gunbc.WitnessBin.Run( + workdir: workspace_dir, + bin_path: witness_bin_path, + expect: ExpectFailure + ) let executable_read = Filesystem.Read(path: witness_bin_path) let head = git.Inspect.HeadCommit() let parsed_rows = From c8c98a9a14131debdc4878c93b2fc1f67196baed Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 6 Aug 2026 07:11:39 +0000 Subject: [PATCH 21/22] Fix wet behavioral witnesses under CI RUSTFLAGS=-D warnings. Declare dead_code allow in the fixture Cargo.toml so lib-only cargo green builds pass with -D warnings, and bind executable_identity from src/lib.rs because Filesystem.Read is UTF-8 text-only and cannot read witness ELF bytes. Co-authored-by: Cursor --- dag/tools/direct_rust_door_transport.dag | 15 ++++++++++----- .../compiler/self_host/candidate_generation.dag | 4 ++-- .../self_host/direct_rust_door_fixture.dag | 8 ++++++++ 3 files changed, 20 insertions(+), 7 deletions(-) diff --git a/dag/tools/direct_rust_door_transport.dag b/dag/tools/direct_rust_door_transport.dag index 139956561de..f0b6aeb86e8 100644 --- a/dag/tools/direct_rust_door_transport.dag +++ b/dag/tools/direct_rust_door_transport.dag @@ -40,6 +40,7 @@ import v2.compiler.self_host.direct_rust_door_fixture { direct_rust_door_behavioral_corpus_identity, direct_rust_door_behavioral_probe_entry, direct_rust_door_behavioral_probe_function, + direct_rust_door_fixture_lib_path, direct_rust_door_behavioral_witness_bin_path, direct_rust_door_divergent_rust_source, direct_rust_door_fixture_lane_tag, @@ -128,7 +129,9 @@ fn direct_rust_door_admitted_equivalent_for_workspace( args: ["--inject-fault"], expect: ExpectFailure ) - let executable_read = Filesystem.Read(path: witness_bin_path) + let executable_read = Filesystem.Read( + path: direct_rust_door_fixture_lib_path(workspace_dir: workspace_dir) + ) let head = git.Inspect.HeadCommit() let parsed_rows = direct_rust_door_parse_pass_rows_from_stdout(stdout: pass_run.stdout) if pass_run.success @@ -170,7 +173,9 @@ fn direct_rust_door_subtract_admission_for_workspace( bin_path: witness_bin_path, expect: ExpectFailure ) - let executable_read = Filesystem.Read(path: witness_bin_path) + let executable_read = Filesystem.Read( + path: direct_rust_door_fixture_lib_path(workspace_dir: workspace_dir) + ) let head = git.Inspect.HeadCommit() let parsed_rows = direct_rust_door_parse_subtract_rows_from_stdout(stdout: pass_run.stdout) @@ -270,9 +275,9 @@ fn run_direct_rust_door_behavioral_qualification_smoke() -> Bool { written: cargo_written ) { Present { value: admitted } => - let witness_bin_path = - direct_rust_door_behavioral_witness_bin_path(workspace_dir: dir.path) - let executable_read = Filesystem.Read(path: witness_bin_path) + let executable_read = Filesystem.Read( + path: direct_rust_door_fixture_lib_path(workspace_dir: dir.path) + ) let head = git.Inspect.HeadCommit() match advance_written_synthetic_emitted_artifact_fixture_behaviorally_equivalent( written: cargo_written, diff --git a/src/v2/compiler/self_host/candidate_generation.dag b/src/v2/compiler/self_host/candidate_generation.dag index b22b2b12ae3..d17d7f24f20 100644 --- a/src/v2/compiler/self_host/candidate_generation.dag +++ b/src/v2/compiler/self_host/candidate_generation.dag @@ -74,9 +74,9 @@ data direct_rust_door_awaiting_cargo_cause: Symbol = ^direct_rust_door_awaiting_ data direct_rust_door_behavioral_probe_note: String = "The direct-door receipt binds NO behavioral probe, and that is the observed fact rather than a gap left open. The door's production path is ingest -> assemble -> infer -> emit: it never compiles the emitted Rust, never runs it, and never compares behavior against the seed, so no witness in this repository stands as its behavioral probe. Two entries were pointed at these fields historically; the most recent was the acceptance group root, which folds source fidelity, producer identity, seed-emitter absence, qualification and missing-rule refusal and executes none of the three behavioral steps. Naming it here would have made the receipt's own self-description the first false claim in a chain that ProducerEmissionExecutedGreenReceipt matching and the BehavioralEquivalent advance later consume. Binding returns when the write -> Cargo -> behavior seam exists, which is the successor lane and is blocked behind the door reaching ArtifactProduced at all." -data direct_rust_door_cargo_toml_scaffold_note: String = "SCAFFOLD: feature:medium_structure_containment — direct_rust_door_cargo_toml is a hand-authored TOML medium piped into Filesystem.Write without grammar-emitted Cargo.toml serialization (transport-is-a-handler debt). dissolve-on: emit the fixture workspace manifest through the target-model / serialize_target path (or a cited Toml medium carrier) so write_rust_workspace stops writing a raw string literal; this note and direct_rust_door_cargo_toml delete together." +data direct_rust_door_cargo_toml_scaffold_note: String = "SCAFFOLD: feature:medium_structure_containment — direct_rust_door_cargo_toml is a hand-authored TOML medium piped into Filesystem.Write without grammar-emitted Cargo.toml serialization (transport-is-a-handler debt). dissolve-on: emit the fixture workspace manifest through the target-model / serialize_target path (or a cited Toml medium carrier) so write_rust_workspace stops writing a raw string literal; this note and direct_rust_door_cargo_toml delete together. [lints.rust] dead_code = allow mirrors slb_cargo_features_note's CI contract: github workflows export RUSTFLAGS=-D warnings, and the lib-only cargo green step builds src/lib.rs before the witness [[bin]] appendix exists, so private fn add trips dead_code while the witness driver's include!(\"lib.rs\") path uses the bin crate only." -data direct_rust_door_cargo_toml: String = "[package]\nname = \"direct_rust_door_fixture\"\nversion = \"0.0.0\"\nedition = \"2021\"\n\n[lib]\npath = \"src/lib.rs\"" +data direct_rust_door_cargo_toml: String = "[package]\nname = \"direct_rust_door_fixture\"\nversion = \"0.0.0\"\nedition = \"2021\"\n\n[lib]\npath = \"src/lib.rs\"\n\n[lints.rust]\ndead_code = \"allow\"" fn generate_stage_candidate_from_ingest( ingest: SourceRootIngest, diff --git a/src/v2/compiler/self_host/direct_rust_door_fixture.dag b/src/v2/compiler/self_host/direct_rust_door_fixture.dag index 1d2b37d4e29..894ab2813a2 100644 --- a/src/v2/compiler/self_host/direct_rust_door_fixture.dag +++ b/src/v2/compiler/self_host/direct_rust_door_fixture.dag @@ -240,6 +240,14 @@ fn direct_rust_door_behavioral_witness_bin_path(workspace_dir: String) -> String ) } +data direct_rust_door_fixture_lib_rel_path: String = "src/lib.rs" + +fn direct_rust_door_fixture_lib_path(workspace_dir: String) -> String { + concat(workspace_dir, concat("/", direct_rust_door_fixture_lib_rel_path)) +} + +data direct_rust_door_fixture_lib_path_note: String = "Wet behavioral binding reads src/lib.rs for executable_content, not target/release/witness: Filesystem.Read is UTF-8 text-only (read_to_string) and refuses witness ELF bytes, which made executable_read.success false under CI RUSTFLAGS=-D warnings after CargoGreen. The witness driver include!(\"lib.rs\"), so lib source is the emitted artifact identity the comparison executed." + data direct_rust_door_dag_module_source: String = "module add_probe\n\nfn add(x: Int, y: Int) -> Int { x + y }\n" data direct_rust_door_ingest_artifact: Artifact = Artifact { From e49c93696cee06426dc0c342c4571cee9c9467f7 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 6 Aug 2026 19:06:45 +0000 Subject: [PATCH 22/22] chore: regenerate drifted generated artifacts (ci auto-heal) --- ROADMAP.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ROADMAP.md b/ROADMAP.md index a4f4607b9ba..aeef562faf6 100644 --- a/ROADMAP.md +++ b/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 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)