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
99 changes: 93 additions & 6 deletions src/v3/compiler/tests/integration/v4_emit_host_harness_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,11 +17,13 @@
//! via `emit_host_bridge` / `emit_host_runner`. Rosters authored in #4046 (`rung_3_4`).
//! **W3.3 (+0 SG-0 paths):** go transport + rung-5 full law roster × rust/python/go
//! (`rung_5.dag`, `nat_semiring_rung5_eval.dag`); cross-target MVP-2 stdout parity via bridge.
//! **W3.4 (+0 SG-0 paths):** extends bridge with python transport + rung-6 additive-Monoid
//! roster (`rung_6.dag`, `rung_5_6_common.dag`, `nat_semiring_rung56_eval.dag`). Behavior receipts:
//! MVP-2 emit-vs-eval `Pass` per law×target via `emit_host_bridge` (five-byte stdout contract;
//! not per-law emitted artifacts until emit pipeline wires law subjects). Substrate rows stay
//! `Deferred` until T-22 dispatch. Dissolution: **ROADMAP.md** T-PB-B / **TASKS.md** T-22 T-38.
//! **W3.4 (+0 SG-0 paths):** extends bridge with python transport + rung-6 post-emit law
//! preservation (`rung_6.dag`, `rung_5_6_common.dag`, `nat_semiring_rung56_eval.dag`).
//! Tranche-1 additive-Monoid + tranche-2 multiplicative-Monoid + annihilator (rust + python).
//! Behavior receipts: MVP-2 emit-vs-eval `Pass` per law×target via `emit_host_bridge` (five-byte
//! stdout contract; not per-law emitted artifacts until emit pipeline wires law subjects).
//! Substrate rows stay `Deferred` until T-22 dispatch. Dissolution: **ROADMAP.md** T-PB-B /
//! **TASKS.md** T-22 T-38.
//!
//! **TESTING.md:** substrate `.dag` models receipt assembly; behavior tests exercise
//! `tools/emit_host_runner` / `emit_host_bridge` (real cargo + run).
Expand Down Expand Up @@ -297,6 +299,66 @@ fn nat_semiring_rung6_python_add_associativity_emit_vs_eval_transport_passes() {
);
}

#[test]
fn nat_semiring_rung6_rust_mul_left_identity_emit_vs_eval_transport_passes() {
assert_rung6_mvp2_emit_vs_eval_pass(
"gunbc_rung6_rust_mul_left_id",
"nat_mul_left_identity_input",
emit_host_bridge::run_emit_vs_eval_mvp2_transport,
EMIT_HOST_FIXTURE_SOURCE,
);
}

#[test]
fn nat_semiring_rung6_rust_mul_associativity_emit_vs_eval_transport_passes() {
assert_rung6_mvp2_emit_vs_eval_pass(
"gunbc_rung6_rust_mul_assoc",
"nat_mul_associativity_input",
emit_host_bridge::run_emit_vs_eval_mvp2_transport,
EMIT_HOST_FIXTURE_SOURCE,
);
}

#[test]
fn nat_semiring_rung6_rust_mul_annihilator_emit_vs_eval_transport_passes() {
assert_rung6_mvp2_emit_vs_eval_pass(
"gunbc_rung6_rust_mul_ann",
"nat_mul_annihilator_input",
emit_host_bridge::run_emit_vs_eval_mvp2_transport,
EMIT_HOST_FIXTURE_SOURCE,
);
}

#[test]
fn nat_semiring_rung6_python_mul_left_identity_emit_vs_eval_transport_passes() {
assert_rung6_mvp2_emit_vs_eval_pass(
"gunbc_rung6_py_mul_left_id",
"nat_mul_left_identity_input",
emit_host_bridge::run_emit_vs_eval_mvp2_python_transport,
EMIT_HOST_PYTHON_FIXTURE_SOURCE,
);
}

#[test]
fn nat_semiring_rung6_python_mul_associativity_emit_vs_eval_transport_passes() {
assert_rung6_mvp2_emit_vs_eval_pass(
"gunbc_rung6_py_mul_assoc",
"nat_mul_associativity_input",
emit_host_bridge::run_emit_vs_eval_mvp2_python_transport,
EMIT_HOST_PYTHON_FIXTURE_SOURCE,
);
}

#[test]
fn nat_semiring_rung6_python_mul_annihilator_emit_vs_eval_transport_passes() {
assert_rung6_mvp2_emit_vs_eval_pass(
"gunbc_rung6_py_mul_ann",
"nat_mul_annihilator_input",
emit_host_bridge::run_emit_vs_eval_mvp2_python_transport,
EMIT_HOST_PYTHON_FIXTURE_SOURCE,
);
}

#[test]
fn emit_host_bridge_rust_transport_builds_runs_and_parses_stdout() {
let work_dir = emit_host_runner::default_work_dir(&format!(
Expand Down Expand Up @@ -666,15 +728,21 @@ fn emit_host_runner_python_row_runs_and_parses_stdout() {
}

#[test]
fn v4_nat_semiring_rung_6_dag_tokenizes_and_parses_additive_monoid_emit_rows() {
fn v4_nat_semiring_rung_6_dag_tokenizes_and_parses_post_emit_law_preservation_emit_rows() {
let module = parse_module(NAT_SEMIRING_RUNG_6_DAG, NAT_SEMIRING_RUNG_6_PATH);
for name in [
"run_phase1_nat_semiring_rung6_rust_add_left_identity_emit_equals_eval",
"run_phase1_nat_semiring_rung6_rust_add_right_identity_emit_equals_eval",
"run_phase1_nat_semiring_rung6_rust_add_associativity_emit_equals_eval",
"run_phase1_nat_semiring_rung6_rust_mul_left_identity_emit_equals_eval",
"run_phase1_nat_semiring_rung6_rust_mul_associativity_emit_equals_eval",
"run_phase1_nat_semiring_rung6_rust_mul_annihilator_emit_equals_eval",
"run_phase1_nat_semiring_rung6_python_add_left_identity_emit_equals_eval",
"run_phase1_nat_semiring_rung6_python_add_right_identity_emit_equals_eval",
"run_phase1_nat_semiring_rung6_python_add_associativity_emit_equals_eval",
"run_phase1_nat_semiring_rung6_python_mul_left_identity_emit_equals_eval",
"run_phase1_nat_semiring_rung6_python_mul_associativity_emit_equals_eval",
"run_phase1_nat_semiring_rung6_python_mul_annihilator_emit_equals_eval",
] {
assert!(
surface_declares_data(&module, name),
Expand Down Expand Up @@ -713,4 +781,23 @@ fn v4_nat_semiring_rung56_eval_dag_tokenizes_and_parses_rung6_gate() {
),
"{NAT_SEMIRING_RUNG56_EVAL_PATH}: tranche-1 additive-Monoid roster"
);
assert!(
surface_declares_data(
&module,
"nat_semiring_rung6_mul_monoid_annihilator_runtime_value_rows"
),
"{NAT_SEMIRING_RUNG56_EVAL_PATH}: tranche-2 mul-Monoid + annihilator roster"
);
assert!(
surface_declares_data(
&module,
"nat_semiring_rung6_post_emit_law_preservation_runtime_value_rows"
),
"{NAT_SEMIRING_RUNG56_EVAL_PATH}: combined tranche-1+2 CorpusEval roster"
);
assert!(
NAT_SEMIRING_RUNG56_EVAL_DAG
.contains("nat_semiring_rung6_post_emit_law_preservation_runtime_value_rows"),
"{NAT_SEMIRING_RUNG56_EVAL_PATH}: CorpusEvalReport must consume full rung-6 roster"
);
}
53 changes: 47 additions & 6 deletions src/v4/test/claim/nat_semiring/rung_6.dag
Original file line number Diff line number Diff line change
@@ -1,9 +1,11 @@
// src/v4/test/claim/nat_semiring/rung_6.dag
// Scope: phase1/nat_semiring rung 6 — post-emit additive-Monoid law preservation (tranche-1 / F4).
// Status: W3.4 — three laws × rust + python via run_test_claim_emit_vs_eval.
// Tranche-1 scaffold: lhs/rhs pin the same law subject Node (mirrors rung_3_4.dag:38-39); Pass on
// substrate rows requires host stdout parsed as RuntimeValue matching eval once T-22 dispatches
// transport. Until then, `v4_emit_host_harness_test.rs` proves MVP-2 emit-vs-eval per law×target.
// Scope: phase1/nat_semiring rung 6 — post-emit semiring law preservation (F4).
// Status: W3.4 tranche-1 additive-Monoid + tranche-2 multiplicative-Monoid + annihilator.
// Tranche-1: add left/right identity + associativity × rust + python.
// Tranche-2: mul left identity + associativity + annihilator × rust + python (expands when tranche-1 PROVEN).
// Scaffold: lhs/rhs pin the same law subject Node (mirrors rung_3_4.dag:38-39); Pass on substrate rows
// requires host stdout parsed as RuntimeValue matching eval once T-22 dispatches transport. Until then,
// `v4_emit_host_harness_test.rs` proves MVP-2 emit-vs-eval per law×target.

module v4.test.claim.nat_semiring.rung_6

Expand All @@ -23,7 +25,10 @@ import v4.std.verification {
import v4.test.claim.algebra_laws.nat_semiring {
nat_add_associativity_input,
nat_add_left_identity_input,
nat_add_right_identity_input
nat_add_right_identity_input,
nat_mul_annihilator_input,
nat_mul_associativity_input,
nat_mul_left_identity_input
}
import v4.test.claim.rung_3_4_common { rung34_emit_host_rust_target_model }
import v4.test.claim.rung_5_6_common {
Expand Down Expand Up @@ -77,3 +82,39 @@ data run_phase1_nat_semiring_rung6_python_add_right_identity_emit_equals_eval: T


data run_phase1_nat_semiring_rung6_python_add_associativity_emit_equals_eval: TestClaimRun<Node, RuntimeValue> = rung56_emit_vs_eval_run(claim: claim_phase1_nat_semiring_rung6_python_add_associativity_emit_equals_eval, fixture_subject: nat_add_associativity_input, target: rung56_emit_host_python_target_model)


data claim_phase1_nat_semiring_rung6_rust_mul_left_identity_emit_equals_eval: TestClaim = rung6_emit_law_equals_claim(label: "fixture=phase1/nat_semiring rung=6 target=rust law=mul-left-identity predicate=R6-rust-emit-law-equals-eval", law_input: nat_mul_left_identity_input)


data claim_phase1_nat_semiring_rung6_rust_mul_associativity_emit_equals_eval: TestClaim = rung6_emit_law_equals_claim(label: "fixture=phase1/nat_semiring rung=6 target=rust law=mul-associativity predicate=R6-rust-emit-law-equals-eval", law_input: nat_mul_associativity_input)


data claim_phase1_nat_semiring_rung6_rust_mul_annihilator_emit_equals_eval: TestClaim = rung6_emit_law_equals_claim(label: "fixture=phase1/nat_semiring rung=6 target=rust law=mul-annihilator predicate=R6-rust-emit-law-equals-eval", law_input: nat_mul_annihilator_input)


data claim_phase1_nat_semiring_rung6_python_mul_left_identity_emit_equals_eval: TestClaim = rung6_emit_law_equals_claim(label: "fixture=phase1/nat_semiring rung=6 target=python law=mul-left-identity predicate=R6-python-emit-law-equals-eval", law_input: nat_mul_left_identity_input)


data claim_phase1_nat_semiring_rung6_python_mul_associativity_emit_equals_eval: TestClaim = rung6_emit_law_equals_claim(label: "fixture=phase1/nat_semiring rung=6 target=python law=mul-associativity predicate=R6-python-emit-law-equals-eval", law_input: nat_mul_associativity_input)


data claim_phase1_nat_semiring_rung6_python_mul_annihilator_emit_equals_eval: TestClaim = rung6_emit_law_equals_claim(label: "fixture=phase1/nat_semiring rung=6 target=python law=mul-annihilator predicate=R6-python-emit-law-equals-eval", law_input: nat_mul_annihilator_input)


data run_phase1_nat_semiring_rung6_rust_mul_left_identity_emit_equals_eval: TestClaimRun<Node, RuntimeValue> = rung56_emit_vs_eval_run(claim: claim_phase1_nat_semiring_rung6_rust_mul_left_identity_emit_equals_eval, fixture_subject: nat_mul_left_identity_input, target: rung34_emit_host_rust_target_model)


data run_phase1_nat_semiring_rung6_rust_mul_associativity_emit_equals_eval: TestClaimRun<Node, RuntimeValue> = rung56_emit_vs_eval_run(claim: claim_phase1_nat_semiring_rung6_rust_mul_associativity_emit_equals_eval, fixture_subject: nat_mul_associativity_input, target: rung34_emit_host_rust_target_model)


data run_phase1_nat_semiring_rung6_rust_mul_annihilator_emit_equals_eval: TestClaimRun<Node, RuntimeValue> = rung56_emit_vs_eval_run(claim: claim_phase1_nat_semiring_rung6_rust_mul_annihilator_emit_equals_eval, fixture_subject: nat_mul_annihilator_input, target: rung34_emit_host_rust_target_model)


data run_phase1_nat_semiring_rung6_python_mul_left_identity_emit_equals_eval: TestClaimRun<Node, RuntimeValue> = rung56_emit_vs_eval_run(claim: claim_phase1_nat_semiring_rung6_python_mul_left_identity_emit_equals_eval, fixture_subject: nat_mul_left_identity_input, target: rung56_emit_host_python_target_model)


data run_phase1_nat_semiring_rung6_python_mul_associativity_emit_equals_eval: TestClaimRun<Node, RuntimeValue> = rung56_emit_vs_eval_run(claim: claim_phase1_nat_semiring_rung6_python_mul_associativity_emit_equals_eval, fixture_subject: nat_mul_associativity_input, target: rung56_emit_host_python_target_model)


data run_phase1_nat_semiring_rung6_python_mul_annihilator_emit_equals_eval: TestClaimRun<Node, RuntimeValue> = rung56_emit_vs_eval_run(claim: claim_phase1_nat_semiring_rung6_python_mul_annihilator_emit_equals_eval, fixture_subject: nat_mul_annihilator_input, target: rung56_emit_host_python_target_model)
40 changes: 36 additions & 4 deletions src/v4/test/claim/workflow/nat_semiring_rung56_eval.dag
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// src/v4/test/claim/workflow/nat_semiring_rung56_eval.dag
// Scope: W3.4 rung 6 corpus eval + gate for phase1/nat_semiring additive-Monoid tranche-1.
// Status: tranche-1 only (left/right identity + associativity); rust + python emit-vs-eval rows.
// Scope: W3.4 rung 6 corpus eval + gate for phase1/nat_semiring post-emit law preservation (F4).
// Status: tranche-1 additive-Monoid + tranche-2 multiplicative-Monoid + annihilator; rust + python.

module v4.test.claim.workflow.nat_semiring_rung56_eval

Expand All @@ -16,9 +16,15 @@ import v4.test.claim.nat_semiring.rung_6 {
run_phase1_nat_semiring_rung6_python_add_associativity_emit_equals_eval,
run_phase1_nat_semiring_rung6_python_add_left_identity_emit_equals_eval,
run_phase1_nat_semiring_rung6_python_add_right_identity_emit_equals_eval,
run_phase1_nat_semiring_rung6_python_mul_annihilator_emit_equals_eval,
run_phase1_nat_semiring_rung6_python_mul_associativity_emit_equals_eval,
run_phase1_nat_semiring_rung6_python_mul_left_identity_emit_equals_eval,
run_phase1_nat_semiring_rung6_rust_add_associativity_emit_equals_eval,
run_phase1_nat_semiring_rung6_rust_add_left_identity_emit_equals_eval,
run_phase1_nat_semiring_rung6_rust_add_right_identity_emit_equals_eval
run_phase1_nat_semiring_rung6_rust_add_right_identity_emit_equals_eval,
run_phase1_nat_semiring_rung6_rust_mul_annihilator_emit_equals_eval,
run_phase1_nat_semiring_rung6_rust_mul_associativity_emit_equals_eval,
run_phase1_nat_semiring_rung6_rust_mul_left_identity_emit_equals_eval
}
import v4.test.claim.workflow.testclaim_corpus_runner {
CorpusEvalReport,
Expand All @@ -37,10 +43,36 @@ data nat_semiring_rung6_additive_monoid_runtime_value_rows: List<TestClaimRun<No
]


data nat_semiring_rung6_mul_monoid_annihilator_runtime_value_rows: List<TestClaimRun<Node, RuntimeValue>> = [
run_phase1_nat_semiring_rung6_rust_mul_left_identity_emit_equals_eval,
run_phase1_nat_semiring_rung6_rust_mul_associativity_emit_equals_eval,
run_phase1_nat_semiring_rung6_rust_mul_annihilator_emit_equals_eval,
run_phase1_nat_semiring_rung6_python_mul_left_identity_emit_equals_eval,
run_phase1_nat_semiring_rung6_python_mul_associativity_emit_equals_eval,
run_phase1_nat_semiring_rung6_python_mul_annihilator_emit_equals_eval
]


data nat_semiring_rung6_post_emit_law_preservation_runtime_value_rows: List<TestClaimRun<Node, RuntimeValue>> = [
run_phase1_nat_semiring_rung6_rust_add_left_identity_emit_equals_eval,
run_phase1_nat_semiring_rung6_rust_add_right_identity_emit_equals_eval,
run_phase1_nat_semiring_rung6_rust_add_associativity_emit_equals_eval,
run_phase1_nat_semiring_rung6_rust_mul_left_identity_emit_equals_eval,
run_phase1_nat_semiring_rung6_rust_mul_associativity_emit_equals_eval,
run_phase1_nat_semiring_rung6_rust_mul_annihilator_emit_equals_eval,
run_phase1_nat_semiring_rung6_python_add_left_identity_emit_equals_eval,
run_phase1_nat_semiring_rung6_python_add_right_identity_emit_equals_eval,
run_phase1_nat_semiring_rung6_python_add_associativity_emit_equals_eval,
run_phase1_nat_semiring_rung6_python_mul_left_identity_emit_equals_eval,
run_phase1_nat_semiring_rung6_python_mul_associativity_emit_equals_eval,
run_phase1_nat_semiring_rung6_python_mul_annihilator_emit_equals_eval
]


fn run_nat_semiring_rung56_eval() -> CorpusEvalReport {
CorpusEvalReport {
entries: corpus_entries_from_node_runtime_value_runs(
runs: nat_semiring_rung6_additive_monoid_runtime_value_rows
runs: nat_semiring_rung6_post_emit_law_preservation_runtime_value_rows
)
}
}
Expand Down
Loading