Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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 @@ -39,6 +39,7 @@ data witness_exclusion_substrings: List<String> = [
"self_host_use_site_verdict_behavioral_witness_test.dag",
"self_host_discovery_enumeration_behavioral_witness_test.dag",
"self_host_target_carriers_behavioral_witness_test.dag",
"self_host_body_producer_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_target_carriers;\npub mod v2_compiler_discovery_enumeration;\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_body_producer;\npub mod v2_compiler_target_carriers;\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_body_producer",
"v2_compiler_target_carriers",
"v2_compiler_discovery_enumeration",
"v2_compiler_parse_engine_hooks",
Expand All @@ -39,6 +40,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_body_producer.rs",
"v2_compiler_target_carriers.rs",
"v2_compiler_discovery_enumeration.rs",
"v2_compiler_parse_engine_hooks.rs",
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
module test.claim.self_host_body_producer_behavioral_witness

import tools.self_host_body_producer_behavioral_transport { sbp_behavioral_receipt_holds }

data self_host_body_producer_behavioral_witness_doc: String = "Wet self-host behavioral receipt probe for Wave 2 easy-flip lane (03_body_producer): tools.self_host_body_producer_behavioral_transport emits src/v2/compiler/03_body_producer.dag via gunbc --entry, assembles a seed-linked v1_compiled crate (gunbc-emitted entry + dep shims + v1-compiler path dep), runs cargo build + witness (plain + --inject-fault), and claim-run on structured_body_dispatch. Live host effects — nightly falsifier Wet batch when frontier row is SelfEmitted with binding."

test fn self_host_body_producer_behavioral_receipt_holds() -> Bool {
sbp_behavioral_receipt_holds()
}
49 changes: 49 additions & 0 deletions dag/tools/self_host_body_producer_behavioral_transport.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
module tools.self_host_body_producer_behavioral_transport

import tools.self_host_curated_seed_linked_harness {
CuratedSeedLinkedShimWrite,
cssl_seed_linked_behavioral_receipt
}
import v2.std.collection { List }
import std.logic { Bool }

data sbp_doc: String = "Wave 2 easy-flip lane (03_body_producer self-emit): curated seed-linked behavioral receipt via tools.self_host_curated_seed_linked_harness. Emit ONLY v2.compiler.body_producer via gunbc compile --entry; seed-retained v2.std.node/diagnostic/algebra surfaces are NOT re-emitted — minimal typed shims under dag/tools/self_host_body_producer_shims/ supply the ABI (text-free, low-Rc; independent of emitter Track-B body fixes). Seed oracle: v1_compiler::v2_compiler_body_producer. Behavioral bar: cargo-green witness pairs emitted vs seed on dispatch/produce (plain + --inject-fault RED) plus supplementary claim-run on structured_body_dispatch."

data sbp_source_rel: String = "src/v2/compiler/03_body_producer.dag"

data sbp_test_entry_rel: String = "src/v2/test/claim/manual/structured_body_dispatch.dag"

data sbp_shim_lib_rel: String = "dag/tools/self_host_body_producer_shims/lib.rs"

data sbp_shim_driver_rel: String = "dag/tools/self_host_body_producer_shims/witness_main.rs"

data sbp_scaffold_dissolution_trigger: String = "dissolve-on: dag/tools/self_host_body_producer_shims/* + sbp behavioral transport wiring — seed-linked dep shim files, driver-crate manifest via cssl_v1_compiled_cargo_toml, and witness driver. DISSOLVES WHEN v2.std.node and v2.std.diagnostic self-emit and gunbc emits seed-linked extern imports without hand shims, and a modeled self-host behavioral-equivalence harness producer emits the comparison driver + manifest (parallel to cssl_doc dissolution)."

data sbp_receipt_pass_marker: String = "SELF_HOST_BODY_PRODUCER_BEHAVIORAL_RECEIPT: PASS"

data sbp_body_producer_shim_writes: List<CuratedSeedLinkedShimWrite> = [
CuratedSeedLinkedShimWrite {
dest_rel: "v2_std_node.rs",
source_rel: "dag/tools/self_host_body_producer_shims/v2_std_node.rs"
},
CuratedSeedLinkedShimWrite {
dest_rel: "v2_std_algebra.rs",
source_rel: "dag/tools/self_host_body_producer_shims/v2_std_algebra.rs"
},
CuratedSeedLinkedShimWrite {
dest_rel: "v2_std_diagnostic.rs",
source_rel: "dag/tools/self_host_body_producer_shims/v2_std_diagnostic.rs"
}
]

fn sbp_behavioral_receipt_holds() -> Bool {
cssl_seed_linked_behavioral_receipt(
source_rel: sbp_source_rel,
shim_lib_rel: sbp_shim_lib_rel,
shim_writes: sbp_body_producer_shim_writes,
driver_rel: sbp_shim_driver_rel,
pass_marker: sbp_receipt_pass_marker,
claim_entry_rel: sbp_test_entry_rel,
claim_function: "structured_body_dispatch_accepts_transform_call"
)
}
10 changes: 10 additions & 0 deletions dag/tools/self_host_body_producer_shims/lib.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
// seed-linked pilot lib — entry module gunbc-emitted, seed-retained dep shims
#![allow(clippy::all, dead_code, unused_imports)]
#![recursion_limit = "256"]
pub mod v1_rt;
pub mod v2_std_algebra;
pub mod v2_std_diagnostic;
pub mod v2_std_node;
pub mod v2_compiler_body_producer;
pub use v1_compiler::NonEmptyVec;
pub use v1_compiler::NonEmptyBTreeSet;
8 changes: 8 additions & 0 deletions dag/tools/self_host_body_producer_shims/v2_std_algebra.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
use im_rc::Vector as Vec;
use std::rc::Rc;

pub fn list_snoc_item<T: Clone>(xs: Rc<Vec<T>>, item: T) -> Rc<Vec<T>> {
let mut out = xs.as_ref().clone();
out.push_back(item);
Rc::new(out)
}
75 changes: 75 additions & 0 deletions dag/tools/self_host_body_producer_shims/v2_std_diagnostic.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,75 @@
use im_rc::Vector as Vec;
use std::rc::Rc;

use crate::v2_std_node::{Node, Symbol};

#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
#[serde(tag = "_variant")]
pub enum NoCorrectionReason {
ExternalContractUnknown,
UserInputBoundary,
}

#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
#[serde(tag = "_variant")]
pub enum Correction {
Unavailable { reason: NoCorrectionReason },
}

#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
pub struct Locus {
pub reason: Symbol,
}

#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
pub struct Diagnostic {
pub reason: Symbol,
pub at: Rc<Locus>,
pub correction: Rc<Correction>,
}

#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
#[serde(tag = "_variant")]
pub enum Outcome<T> {
Accepted {
value: T,
diagnostics: Rc<Vec<Rc<Diagnostic>>>,
},
Rejected {
diagnostics: Rc<Vec<Rc<Diagnostic>>>,
},
}

pub fn node_locus(node: Rc<Node>) -> Rc<Locus> {
let _ = node;
Rc::new(Locus {
reason: "synthetic".to_string(),
})
}

pub fn outcome_accepted<T>(value: T) -> Rc<Outcome<T>> {
Rc::new(Outcome::Accepted {
value,
diagnostics: Rc::new(Vec::new()),
})
}

pub fn outcome_rejected<T>(d: Rc<Diagnostic>) -> Rc<Outcome<T>> {
let mut diags = Vec::new();
diags.push_back(d);
Rc::new(Outcome::Rejected {
diagnostics: Rc::new(diags),
})
}

pub fn bind_outcome<T: Clone, U, F>(o: Rc<Outcome<T>>, f: F) -> Rc<Outcome<U>>
where
F: Fn(T) -> Rc<Outcome<U>> + Clone,
{
match &*o {
Outcome::Accepted { value, .. } => f(value.clone()),
Outcome::Rejected { diagnostics } => Rc::new(Outcome::Rejected {
diagnostics: diagnostics.clone(),
}),
}
}
81 changes: 81 additions & 0 deletions dag/tools/self_host_body_producer_shims/v2_std_node.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,81 @@
// seed-linked dep shim — minimal v2.std.node surface for body_producer pilot
use im_rc::{vector as vec, Vector as Vec};
use std::rc::Rc;

pub type Symbol = String;

#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
#[serde(tag = "_variant")]
pub enum NodeOccurrenceId {
SyntheticOccurrence,
}

#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
#[serde(tag = "_variant")]
pub enum Connective {
Atom { identity: String },
Conj,
Disj,
Arrow,
Cardinality,
Instantiation,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
#[serde(tag = "_variant")]
pub enum Behavior {
Value,
Transform,
Branch,
Loop,
Bind,
Match,
}

#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
#[serde(tag = "_variant")]
pub enum NodeKind {
TypeNode { connective: Rc<Connective> },
ComputationNode { behavior: Behavior },
}

#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
#[serde(tag = "_variant")]
pub enum EdgeLabel {
Named { name: String },
Positional,
}

#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
pub struct Edge {
pub label: Rc<EdgeLabel>,
pub target: Rc<Node>,
}

#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
pub struct Node {
pub kind: Rc<NodeKind>,
pub children: Rc<Vec<Rc<Edge>>>,
pub occurrence_id: Rc<NodeOccurrenceId>,
}

pub fn node_synthetic(kind: Rc<NodeKind>, children: Rc<Vec<Rc<Edge>>>) -> Rc<Node> {
Rc::new(Node {
kind,
children,
occurrence_id: Rc::new(NodeOccurrenceId::SyntheticOccurrence),
})
}

pub fn node_rebuild(n: Rc<Node>, children: Rc<Vec<Rc<Edge>>>) -> Rc<Node> {
Rc::new(Node {
kind: n.kind.clone(),
children,
occurrence_id: n.occurrence_id.clone(),
})
}

pub fn well_formed(n: Rc<Node>) -> bool {
let _ = n;
true
}
124 changes: 124 additions & 0 deletions dag/tools/self_host_body_producer_shims/witness_main.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,124 @@
use im_rc::{vector as vec, Vector as Vec};
use std::rc::Rc;
use v1_compiled::v2_compiler_body_producer as emitted;
use v1_compiled::v2_std_node::{
node_synthetic as emitted_node_synthetic, Behavior as EBehavior, Connective as EConnective,
Edge as EEdge, EdgeLabel as EEdgeLabel, Node as ENode, NodeKind as ENodeKind,
};
use v1_compiler::v2_compiler_body_producer as seed;
use v1_compiler::usv_pilot_v2_std_node::{
node_synthetic as seed_node_synthetic, Behavior as SBehavior, Connective as SConnective,
Edge as SEdge, EdgeLabel as SEdgeLabel, Node as SNode, NodeKind as SNodeKind,
};

fn outcome_is_accepted_emitted<T>(o: &Rc<emitted::Outcome<T>>) -> bool {
matches!(&**o, emitted::Outcome::Accepted { .. })
}

fn outcome_is_accepted_seed<T>(o: &Rc<seed::Outcome<T>>) -> bool {
matches!(&**o, seed::Outcome::Accepted { .. })
}

fn transform_body_emitted() -> Rc<ENode> {
emitted_node_synthetic(
Rc::new(ENodeKind::ComputationNode {
behavior: EBehavior::Transform,
}),
Rc::new(vec![]),
)
}

fn transform_body_seed() -> Rc<SNode> {
seed_node_synthetic(
Rc::new(SNodeKind::ComputationNode {
behavior: SBehavior::Transform,
}),
Rc::new(vec![]),
)
}

fn atom_body_emitted() -> Rc<ENode> {
emitted_node_synthetic(
Rc::new(ENodeKind::TypeNode {
connective: Rc::new(EConnective::Atom {
identity: "residual".to_string(),
}),
}),
Rc::new(vec![]),
)
}

fn atom_body_seed() -> Rc<SNode> {
seed_node_synthetic(
Rc::new(SNodeKind::TypeNode {
connective: Rc::new(SConnective::Atom {
identity: "residual".to_string(),
}),
}),
Rc::new(vec![]),
)
}

fn arrow_signature_emitted() -> Rc<ENode> {
emitted_node_synthetic(
Rc::new(ENodeKind::TypeNode {
connective: Rc::new(EConnective::Arrow),
}),
Rc::new(vec![]),
)
}

fn arrow_signature_seed() -> Rc<SNode> {
seed_node_synthetic(
Rc::new(SNodeKind::TypeNode {
connective: Rc::new(SConnective::Arrow),
}),
Rc::new(vec![]),
)
}

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

let e_dispatch = emitted::body_producer_dispatch_structured_body(transform_body_emitted());
let s_dispatch = seed::body_producer_dispatch_structured_body(transform_body_seed());
let dispatch_ok =
outcome_is_accepted_emitted(&e_dispatch) && outcome_is_accepted_seed(&s_dispatch);
println!("dispatch_transform eq_accept={dispatch_ok}");
all_pass &= dispatch_ok;

let e_reject = emitted::body_producer_dispatch_structured_body(atom_body_emitted());
let s_reject = seed::body_producer_dispatch_structured_body(atom_body_seed());
let reject_ok =
!outcome_is_accepted_emitted(&e_reject) && !outcome_is_accepted_seed(&s_reject);
println!("dispatch_non_behavior eq_reject={reject_ok}");
all_pass &= reject_ok;

let e_produce = emitted::produce_arrow_with_structured_body(
arrow_signature_emitted(),
if inject_fault {
atom_body_emitted()
} else {
transform_body_emitted()
},
);
let s_produce = seed::produce_arrow_with_structured_body(
arrow_signature_seed(),
transform_body_seed(),
);
let produce_ok = outcome_is_accepted_emitted(&e_produce)
== outcome_is_accepted_seed(&s_produce)
&& (!inject_fault || !outcome_is_accepted_emitted(&e_produce));
println!(
"produce_arrow inject_fault={inject_fault} parity={produce_ok}"
);
all_pass &= produce_ok;

if all_pass {
println!("SELF_HOST_BODY_PRODUCER_BEHAVIORAL_RECEIPT: PASS");
std::process::exit(0);
}
println!("SELF_HOST_BODY_PRODUCER_BEHAVIORAL_RECEIPT: FAIL");
std::process::exit(1);
}
Loading
Loading