Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions dag/gunbc/ci_layer_roots.dag
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ data witness_exclusion_substrings: List<String> = [
"self_host_logic_behavioral_witness_test.dag",
"self_host_parse_engine_hooks_behavioral_witness_test.dag",
"self_host_use_site_verdict_behavioral_witness_test.dag",
"self_host_discovery_enumeration_behavioral_witness_test.dag",
"dag_collect_fingerprint_witness_test.dag",
"dag_compile_clean_perturb_receipts_test.dag",
"test/claim/diagnostics_test.dag",
Expand Down
4 changes: 3 additions & 1 deletion dag/gunbc/stage0_crate_layout_generated.dag
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ import std.types { List, String }

data stage0_crate_layout_generated_note: String = "Generated by gunbc stage0_crate_layout_emit — do not hand-edit. Authority: v2.compiler.self_host.frontier; regen via dag/tools/generated_artifact_gate.dag main_wet."

data generated_pub_mod_block: String = "\npub mod v1_interpreter;\npub mod cli_run;\npub mod coproduct_reflection;\npub mod resolved_graph_cache;\npub mod shared_typecheck_store;\npub mod recorded_fixture;\npub mod memory_governor;\npub mod module_path_index;\npub mod usv_pilot_v2_std_algebra;\npub mod usv_pilot_v2_std_collection;\npub mod usv_pilot_v2_std_node;\npub mod v2_compiler_parse_engine_hooks;\npub mod v2_compiler_use_site_verdict;"
data generated_pub_mod_block: String = "\npub mod v1_interpreter;\npub mod cli_run;\npub mod coproduct_reflection;\npub mod resolved_graph_cache;\npub mod shared_typecheck_store;\npub mod recorded_fixture;\npub mod memory_governor;\npub mod module_path_index;\npub mod usv_pilot_v2_std_algebra;\npub mod usv_pilot_v2_std_collection;\npub mod usv_pilot_v2_std_node;\npub mod v2_compiler_discovery_enumeration;\npub mod v2_compiler_parse_engine_hooks;\npub mod v2_compiler_use_site_verdict;"

data generated_pub_mod_basenames: List<String> = [
"v1_interpreter",
Expand All @@ -18,6 +18,7 @@ data generated_pub_mod_basenames: List<String> = [
"usv_pilot_v2_std_algebra",
"usv_pilot_v2_std_collection",
"usv_pilot_v2_std_node",
"v2_compiler_discovery_enumeration",
"v2_compiler_parse_engine_hooks",
"v2_compiler_use_site_verdict"
]
Expand All @@ -36,6 +37,7 @@ data generated_stage0_filenames: List<String> = [
"usv_pilot_v2_std_algebra.rs",
"usv_pilot_v2_std_collection.rs",
"usv_pilot_v2_std_node.rs",
"v2_compiler_discovery_enumeration.rs",
"v2_compiler_parse_engine_hooks.rs",
"v2_compiler_use_site_verdict.rs"
]
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
module test.claim.self_host_discovery_enumeration_behavioral_witness

import tools.self_host_discovery_enumeration_behavioral_transport { sde_behavioral_receipt_holds }

data self_host_discovery_enumeration_behavioral_witness_doc: String = "Wet self-host behavioral receipt probe for Wave 2 Band A (discovery_enumeration): tools.self_host_discovery_enumeration_behavioral_transport emits src/v2/compiler/discovery_enumeration.dag via gunbc --entry, assembles a shim-free v1_compiled crate (emitted lib.rs + seed-linked v1-compiler path dep), runs cargo build + witness (plain + --inject-fault), and claim-run on discovery_enumeration_test. Live host effects — nightly falsifier Wet batch when frontier row is SelfEmitted with binding."

test fn self_host_discovery_enumeration_behavioral_receipt_holds() -> Bool {
sde_behavioral_receipt_holds()
}
8 changes: 6 additions & 2 deletions dag/test/claim/stage0_crate_layout_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,13 @@ import v2.compiler.self_host.frontier {
}
import std.types { Bool, Int }

fn w_hand_maintained_stage0_filenames_include_use_site_verdict() -> Bool {
fn w_hand_maintained_stage0_filenames_include_self_emitted() -> Bool {
generated_stage0_filenames
|> any(f => f == "v2_compiler_use_site_verdict.rs")
&& generated_stage0_filenames
|> any(f => f == "v2_compiler_parse_engine_hooks.rs")
&& generated_stage0_filenames
|> any(f => f == "v2_compiler_discovery_enumeration.rs")
}

fn w_generated_stage0_filenames_match_frontier() -> Bool {
Expand All @@ -31,7 +35,7 @@ fn w_self_emitted_derived_count() -> Bool {
}

test fn stage0_crate_layout_witnesses() -> Bool {
w_hand_maintained_stage0_filenames_include_use_site_verdict()
w_hand_maintained_stage0_filenames_include_self_emitted()
&& w_generated_stage0_filenames_match_frontier()
&& w_generated_stage0_dirs_match_frontier()
&& w_self_emitted_derived_count()
Expand Down
96 changes: 96 additions & 0 deletions dag/tools/self_host_discovery_enumeration_behavioral_transport.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,96 @@
module tools.self_host_discovery_enumeration_behavioral_transport

import extdeps.shell
import extdeps.filesystem.filesystem_io
import extdeps.cargo_build
import extdeps.git
import extdeps.gunbc
import std.logic { Bool }
import tools.host_prelude { witness_bin, witness_bin_ensure_built_typed, witness_bin_release_path }

data sde_doc: String = "Wave 2 Band A (discovery_enumeration self-emit): shim-free seed-linked behavioral receipt. Emit ONLY v2.compiler.discovery_enumeration via gunbc compile --entry; the emitted lib.rs carries its std import closure (no hand dep shims). Seed oracle: v1_compiler::v2_compiler_discovery_enumeration (hand-retained in src/v1/stage0). Behavioral bar: cargo-green witness pairs emitted vs seed on data constants + OwnedDataDeclInitializer / OwnedDataDiscoveryReceipt shapes (plain + --inject-fault RED). String authority: std.string_type (not v2.std.text) keeps the emit closure free of v2.std.nat diagnostic debt."

data sde_seed_retained_note: String = "Seed oracle: v1_compiler::v2_compiler_discovery_enumeration in src/v1/stage0 (hand-retained, independent of emitted artifact). Dissolve-on: same as sde_scaffold_dissolution_trigger."

data sde_source_rel: String = "src/v2/compiler/discovery_enumeration.dag"

data sde_test_entry_rel: String = "src/v2/test/claim/discovery_enumeration_test.dag"

data sde_shim_driver_rel: String = "dag/tools/self_host_discovery_enumeration_shims/witness_main.rs"

data sde_scaffold_dissolution_trigger: String = "dissolve-on: dag/tools/self_host_discovery_enumeration_shims/witness_main.rs + sde_cargo_toml — hand-written equivalence driver + driver-crate manifest (mirrors slb/ssuv scaffold debt; shim-free for std deps only). DISSOLVES WHEN a modeled self-host behavioral-equivalence harness producer emits the comparison driver + manifest without hand shims."

data sde_receipt_pass_marker: String = "SELF_HOST_DISCOVERY_ENUMERATION_BEHAVIORAL_RECEIPT: PASS"

data sde_cargo_features_note: String = "Mirrors slb_cargo_features_note: text_lookup_work_counter feature declared for -D warnings consumers."

fn sde_repo_path(root: String, rel: String) -> String {
concat(root, concat("/", rel))
}

fn sde_cargo_toml(root: String) -> String {
concat(
"[package]\nname = \"v1_compiled\"\nversion = \"0.1.0\"\nedition = \"2021\"\n\n[features]\ntext_lookup_work_counter = []\n\n[[bin]]\nname = \"witness\"\npath = \"src/main.rs\"\n\n[dependencies]\nim-rc = { version = \"15.1\", features = [\"serde\"] }\nserde = { version = \"1\", features = [\"derive\", \"rc\"] }\nserde_json = \"1\"\nstacker = \"0.1\"\nlazy_static = \"1\"\nunicode-ident = \"1\"\nunicode-properties = { version = \"0.1\", features = [\"emoji\"] }\nv1-compiler = { path = \"",
concat(root, "/src/v1/stage0\" }\n")
)
}

fn sde_behavioral_receipt_holds() -> Bool {
let root = git.Core.Toplevel()
let module_read = Filesystem.Read(path: sde_repo_path(root: root.path, rel: sde_source_rel))
let driver_read = Filesystem.Read(path: sde_repo_path(root: root.path, rel: sde_shim_driver_rel))

let out_dir = shell.Mktemp.Dir()
let gunbc_built = witness_bin_ensure_built_typed(root: root.path, bin: witness_bin(var_name: "GUNBC", bin_name: "gunbc"))
let gunbc_bin = witness_bin_release_path(root: root.path, bin_name: "gunbc")
let emit = gunbc.WitnessBin.Run(
workdir: root.path,
bin_path: gunbc_bin,
args: [
"compile",
"--source-root", "dag",
"--source-root", "src/v2",
"--entry", sde_source_rel,
"--output-dir", out_dir.path,
"--target", "rust",
"--dependency-pool-index", "primary-precedence"
]
)

let manifest = Filesystem.Write(path: concat(out_dir.path, "/Cargo.toml"), content: sde_cargo_toml(root: root.path))
let main_rs = Filesystem.Write(path: concat(out_dir.path, "/src/main.rs"), content: driver_read.content)

let build = cargo.Build.BuildManifest(
workdir: out_dir.path,
manifest_path: concat(out_dir.path, "/Cargo.toml"),
target_dir: concat(out_dir.path, "/target"),
extra_args: ["--release"]
)

let witness_bin_path = concat(out_dir.path, "/target/release/witness")
let pass_run = gunbc.WitnessBin.Run(workdir: out_dir.path, bin_path: witness_bin_path)
let fault_run = gunbc.WitnessBin.Run(workdir: out_dir.path, bin_path: witness_bin_path, args: ["--inject-fault"])

let eval_constants = gunbc.WitnessBin.Run(
workdir: root.path,
bin_path: gunbc_bin,
args: [
"run", "--claim-run",
"--source-root", "dag",
"--source-root", "src/v2",
"--entry", sde_test_entry_rel,
"--function", "discovery_enumeration_unified_claim_arm_modules_holds"
]
)

let cleanup_out = shell.Remove.RecursiveForce(path: out_dir.path)

module_read.success && driver_read.success
&& out_dir.success && gunbc_built && emit.success
&& manifest.success && main_rs.success
&& build.success
&& pass_run.success && string_contains(s: pass_run.stdout, pattern: sde_receipt_pass_marker)
&& (fault_run.success == false)
&& eval_constants.success
&& cleanup_out.success
}
128 changes: 128 additions & 0 deletions dag/tools/self_host_discovery_enumeration_shims/witness_main.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,128 @@
use std::rc::Rc;
use v1_compiled::v2_compiler_discovery_enumeration as emitted;
use v1_compiler::v2_compiler_discovery_enumeration as seed;

fn rc_text_eq(e: &Rc<String>, s: &str) -> bool {
e.as_str() == s
}

fn resolved_eq(e: &emitted::ResolvedDeclRef, s: &seed::ResolvedDeclRef) -> bool {
rc_text_eq(&e.module, &s.module) && e.name == s.name
}

fn init_eq(e: &emitted::OwnedDataDeclInitializer, s: &seed::OwnedDataDeclInitializer) -> bool {
use emitted::OwnedDataDeclInitializer as E;
use seed::OwnedDataDeclInitializer as S;
match (e, s) {
(E::OwnedNodeCorpusInit, S::OwnedNodeCorpusInit) => true,
(
E::OwnedBoolWitnessClaimInit {
witness_entry: ee,
witness_function: ef,
},
S::OwnedBoolWitnessClaimInit {
witness_entry: se,
witness_function: sf,
},
) => rc_text_eq(ee, se) && rc_text_eq(ef, sf),
(E::OwnedOtherInit { resolved: er }, S::OwnedOtherInit { resolved: sr }) => {
resolved_eq(er, sr)
}
_ => false,
}
}

fn receipt_eq(e: &emitted::OwnedDataDiscoveryReceipt, s: &seed::OwnedDataDiscoveryReceipt) -> bool {
e.unified_claim_arm_count == s.unified_claim_arm_count
&& e.bool_witness_claim_arm_count == s.bool_witness_claim_arm_count
&& e.illegal_other_init_count == s.illegal_other_init_count
&& e.bool_witness_transport_row_count == s.bool_witness_transport_row_count
&& e.transport_projection_complete == s.transport_projection_complete
}

fn main() {
let inject_fault = std::env::args().any(|a| a == "--inject-fault");
let mut all_pass = true;

let e_bool_mod = emitted::unified_claim_arm_bool_witness_claim_module();
let s_bool_mod = seed::unified_claim_arm_bool_witness_claim_module();
let bool_mod_ok = rc_text_eq(&e_bool_mod, &s_bool_mod) && !inject_fault;
println!("bool_module emitted={e_bool_mod:?} seed={s_bool_mod:?} eq={bool_mod_ok}");
all_pass &= bool_mod_ok;

let e_corpus_mod = emitted::unified_claim_arm_node_corpus_module();
let s_corpus_mod = seed::unified_claim_arm_node_corpus_module();
let corpus_mod_ok = rc_text_eq(&e_corpus_mod, &s_corpus_mod);
println!("corpus_module emitted={e_corpus_mod:?} seed={s_corpus_mod:?} eq={corpus_mod_ok}");
all_pass &= corpus_mod_ok;

let cases: [(emitted::OwnedDataDeclInitializer, seed::OwnedDataDeclInitializer); 3] = [
(
emitted::OwnedDataDeclInitializer::OwnedNodeCorpusInit,
seed::OwnedDataDeclInitializer::OwnedNodeCorpusInit,
),
(
emitted::OwnedDataDeclInitializer::OwnedBoolWitnessClaimInit {
witness_entry: Rc::new("entry.dag".to_string()),
witness_function: Rc::new("witness_fn".to_string()),
},
seed::OwnedDataDeclInitializer::OwnedBoolWitnessClaimInit {
witness_entry: "entry.dag".to_string(),
witness_function: "witness_fn".to_string(),
},
),
(
emitted::OwnedDataDeclInitializer::OwnedOtherInit {
resolved: Rc::new(emitted::ResolvedDeclRef {
module: Rc::new("v2.example.mod".to_string()),
name: "sym".to_string(),
}),
},
seed::OwnedDataDeclInitializer::OwnedOtherInit {
resolved: seed::ResolvedDeclRef {
module: "v2.example.mod".to_string(),
name: "sym".to_string(),
},
},
),
];

for (i, (ev, sv)) in cases.iter().enumerate() {
let ev_cmp = if inject_fault && i == 0 {
emitted::OwnedDataDeclInitializer::OwnedBoolWitnessClaimInit {
witness_entry: Rc::new("fault".to_string()),
witness_function: Rc::new("fault".to_string()),
}
} else {
ev.clone()
};
let ok = init_eq(&ev_cmp, sv);
println!("init({i}) emitted={ev_cmp:?} seed={sv:?} eq={ok}");
all_pass &= ok;
}

let e_receipt = emitted::OwnedDataDiscoveryReceipt {
unified_claim_arm_count: 2,
bool_witness_claim_arm_count: 1,
illegal_other_init_count: 0,
bool_witness_transport_row_count: 1,
transport_projection_complete: true,
};
let s_receipt = seed::OwnedDataDiscoveryReceipt {
unified_claim_arm_count: 2,
bool_witness_claim_arm_count: 1,
illegal_other_init_count: 0,
bool_witness_transport_row_count: 1,
transport_projection_complete: true,
};
let receipt_ok = receipt_eq(&e_receipt, &s_receipt);
println!("receipt emitted={e_receipt:?} seed={s_receipt:?} eq={receipt_ok}");
all_pass &= receipt_ok;

if all_pass {
println!("SELF_HOST_DISCOVERY_ENUMERATION_BEHAVIORAL_RECEIPT: PASS");
std::process::exit(0);
}
println!("SELF_HOST_DISCOVERY_ENUMERATION_BEHAVIORAL_RECEIPT: FAIL");
std::process::exit(1);
}
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ pub const HAND_MAINTAINED_STAGE0_FILES: &[&str] = &[
"usv_pilot_v2_std_algebra.rs",
"usv_pilot_v2_std_collection.rs",
"usv_pilot_v2_std_node.rs",
"v2_compiler_discovery_enumeration.rs",
"v2_compiler_parse_engine_hooks.rs",
"v2_compiler_use_site_verdict.rs"
];
Expand Down
6 changes: 3 additions & 3 deletions src/v1/stage0/src/gunbc_stage0_crate_layout_generated.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ pub fn stage0_crate_layout_generated_note() -> String {
pub fn generated_pub_mod_block() -> String {
thread_local! {
static CACHED: String = {
"\npub mod v1_interpreter;\npub mod cli_run;\npub mod coproduct_reflection;\npub mod resolved_graph_cache;\npub mod shared_typecheck_store;\npub mod recorded_fixture;\npub mod memory_governor;\npub mod module_path_index;\npub mod usv_pilot_v2_std_algebra;\npub mod usv_pilot_v2_std_collection;\npub mod usv_pilot_v2_std_node;\npub mod v2_compiler_parse_engine_hooks;\npub mod v2_compiler_use_site_verdict;".to_string()
"\npub mod v1_interpreter;\npub mod cli_run;\npub mod coproduct_reflection;\npub mod resolved_graph_cache;\npub mod shared_typecheck_store;\npub mod recorded_fixture;\npub mod memory_governor;\npub mod module_path_index;\npub mod usv_pilot_v2_std_algebra;\npub mod usv_pilot_v2_std_collection;\npub mod usv_pilot_v2_std_node;\npub mod v2_compiler_discovery_enumeration;\npub mod v2_compiler_parse_engine_hooks;\npub mod v2_compiler_use_site_verdict;".to_string()
};
}
CACHED.with(|c: &String| c.clone())
Expand All @@ -32,7 +32,7 @@ pub fn generated_pub_mod_block() -> String {
pub fn generated_pub_mod_basenames() -> Rc<Vec<String>> {
thread_local! {
static CACHED: Rc<Vec<String>> = {
Rc::new(vec!["v1_interpreter".to_string(), "cli_run".to_string(), "coproduct_reflection".to_string(), "resolved_graph_cache".to_string(), "shared_typecheck_store".to_string(), "recorded_fixture".to_string(), "memory_governor".to_string(), "module_path_index".to_string(), "usv_pilot_v2_std_algebra".to_string(), "usv_pilot_v2_std_collection".to_string(), "usv_pilot_v2_std_node".to_string(), "v2_compiler_parse_engine_hooks".to_string(), "v2_compiler_use_site_verdict".to_string()])
Rc::new(vec!["v1_interpreter".to_string(), "cli_run".to_string(), "coproduct_reflection".to_string(), "resolved_graph_cache".to_string(), "shared_typecheck_store".to_string(), "recorded_fixture".to_string(), "memory_governor".to_string(), "module_path_index".to_string(), "usv_pilot_v2_std_algebra".to_string(), "usv_pilot_v2_std_collection".to_string(), "usv_pilot_v2_std_node".to_string(), "v2_compiler_discovery_enumeration".to_string(), "v2_compiler_parse_engine_hooks".to_string(), "v2_compiler_use_site_verdict".to_string()])
};
}
CACHED.with(|c: &Rc<Vec<String>>| c.clone())
Expand All @@ -41,7 +41,7 @@ pub fn generated_pub_mod_basenames() -> Rc<Vec<String>> {
pub fn generated_stage0_filenames() -> Rc<Vec<String>> {
thread_local! {
static CACHED: Rc<Vec<String>> = {
Rc::new(vec!["v1_interpreter.rs".to_string(), "cli_run.rs".to_string(), "coproduct_reflection.rs".to_string(), "resolved_graph_cache.rs".to_string(), "shared_typecheck_store.rs".to_string(), "recorded_fixture.rs".to_string(), "main.rs".to_string(), "phase_profile.rs".to_string(), "memory_governor.rs".to_string(), "std_lens_verdict.rs".to_string(), "usv_pilot_v2_std_algebra.rs".to_string(), "usv_pilot_v2_std_collection.rs".to_string(), "usv_pilot_v2_std_node.rs".to_string(), "v2_compiler_parse_engine_hooks.rs".to_string(), "v2_compiler_use_site_verdict.rs".to_string()])
Rc::new(vec!["v1_interpreter.rs".to_string(), "cli_run.rs".to_string(), "coproduct_reflection.rs".to_string(), "resolved_graph_cache.rs".to_string(), "shared_typecheck_store.rs".to_string(), "recorded_fixture.rs".to_string(), "main.rs".to_string(), "phase_profile.rs".to_string(), "memory_governor.rs".to_string(), "std_lens_verdict.rs".to_string(), "usv_pilot_v2_std_algebra.rs".to_string(), "usv_pilot_v2_std_collection.rs".to_string(), "usv_pilot_v2_std_node.rs".to_string(), "v2_compiler_discovery_enumeration.rs".to_string(), "v2_compiler_parse_engine_hooks.rs".to_string(), "v2_compiler_use_site_verdict.rs".to_string()])
};
}
CACHED.with(|c: &Rc<Vec<String>>| c.clone())
Expand Down
1 change: 1 addition & 0 deletions src/v1/stage0/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -116,6 +116,7 @@ pub mod v1_probe_emit_interp;
pub mod v1_rt;
pub mod v1_std_core;
pub mod v1_test_non_ascii_perf_fixture;
pub mod v2_compiler_discovery_enumeration;
pub mod v2_compiler_parse_engine_hooks;
pub mod v2_compiler_use_site_verdict;
pub mod wt_a;
Expand Down
Loading
Loading