diff --git a/INVARIANTS.md b/INVARIANTS.md index 3a9afebd05d..262998eb795 100644 --- a/INVARIANTS.md +++ b/INVARIANTS.md @@ -368,6 +368,7 @@ Per **Dispatch-Discipline Mechanisms (b)** above, each **new** path added to `EX | `src/v3/compiler/tests/integration/extdeps_sql_transport_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row `T-PB-B` / `pb_rust_tests_outside_residual_zero`; this Rust integration receipt keeps HTTP/SQL/audit extdeps compiled by the existing v3 parser before downstream emission-target consumers rely on them. **Dissolution:** remove when extdeps transport and Phase 3 emission-target files are covered by a `.dag`-native parse/authority suite or generated test harness rather than per-file Rust `compile_to_dag` probes. **Interim ratchet:** `rest_transport_dag_compiles_cleanly` and `sql_transport_dag_compiles_cleanly` pin `dsl/extdeps/transports/rest.dag` and `dsl/extdeps/transports/sql.dag`; `http_server_extdep_dag_compiles_cleanly`, `sql_migration_extdep_dag_compiles_cleanly`, and `audit_cloudevents_extdep_dag_compiles_cleanly` pin `dsl/extdeps/http/server.dag`, `dsl/extdeps/sql/migration.dag`, and `dsl/extdeps/audit/cloudevents.dag` as parseable staged emission-target substrate. The field-sensitive companions (`http_server_target_fields_are_authoritative_substrate_edges`, `sql_migration_target_fields_bound_raw_sql_scaffold`, `audit_cloudevents_target_fields_preserve_core_names`) consume the new target-contract fields directly so they fail on raw `String`/`Int` regressions, missing SQL scaffold bounds, or CloudEvents alias drift while the first real projection consumer is still staged; the audit ratchet also locks CloudEvents core fields to branded carriers and `std.types.Timestamp` rather than raw strings. | | `src/v3/compiler/tests/integration/v4_extdeps_react_dag_smoke_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** T-4.7 (`src/v4/extdeps/frameworks/react.dag`, React 19.2.0–pinned framework substrate). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `src/v4/extdeps/frameworks/react.dag` (or the v4 extdeps fixture set it belongs to) is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust `compile_to_dag` probe. **Interim ratchet:** `v4_extdeps_react_dag_compiles` asserts `compile_to_dag` succeeds with empty `dag.diagnostics()` for the pinned `include_str!` source. | | `src/v3/compiler/tests/integration/v4_extdeps_file_system_dag_smoke_test.rs` | **TASKS.md** T-4.5 / Wave-2-C2 (`src/v4/extdeps/file_system.dag` — external file-system resource + modeled read/write effects; Practice 11 companion: no `import v4.std.node`, no `NodeFileBinding`; POSIX substrate exports retained for `posix.dag` / `testgen.dag`). **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `file_system.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust probe. **Interim ratchet:** `v4_extdeps_file_system_dag_tokenizes_and_parses` plus Practice-11 companion tests (parse-surface import/type bans, POSIX-grounded `FilePath`, per-operation receipt record shapes, Wave-2 `ModeledFileEffects.file_read`/`file_write` arrow signatures + legacy `FileSystemOperations` / request-carrier coexistence). | +| `src/v3/compiler/tests/integration/v4_workflow_ci_runner_dag_smoke_test.rs` | **TASKS.md** T-21 + T-24 Wave-0 (`src/v4/workflow/ci.dag` — `ci_select_from_*` under canonical `v4.workflow.ci`; `affected_set_rerun_nodes` → `List`; narrow = identity-aware subtree frontier in `verification.dag`; fail-closed = full roster; `src/v4/test/claim/workflow/affected_set_ci_runner.dag` structural receipts). **Tracked substrate bridge:** `verification.dag` `test_claim_ci_selection_fail_closed` carries 🟡 gated Practice-10 predicate-dissolution mark (dissolve when `ci_select` consumes `TestClaimCacheKey` from `05_eval`). **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when Node-level TestClaim CI selection is exercised only by `.dag` `TestClaim` rows / generated harness / host runner without this parse probe (full wire: edit-locus + `TestClaimExerciseSurface` + `ci.yml` — follow-on A/B/C). **Interim ratchet:** `v4_workflow_ci_dag_tokenizes_and_parses`; `v4_workflow_ci_test_claim_selection_entrypoints`; `v4_workflow_affected_set_ci_runner_claim_*` — tokenize+parse + import/entrypoint wiring receipts. | | `src/v3/compiler/tests/integration/v4_test_bootstrap_infra_closeout_test.rs` | **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **TASKS.md** **T-19** (`src/v4/lens/testgen.dag`) + **T-20** (`src/v4/workflow/bootstrap.dag`) + **T-22** (`src/v4/compiler/05_eval.dag` DiagnosticAssert execution / `eval_rejected_assert_kind_deferred` dissolution; witnesses in `src/v4/test/claim/manual/diagnostic_assert_eval.dag`). **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the closeout ratchet; T-22 expansion in this PR updates this row (same path — no new census line). **Dissolution:** remove when the T-19/T-20/T-22 closeout checks are expressed as `.dag` `TestClaim` rows or generated harness coverage without this host parse-surface ratchet. **Interim ratchet:** `t19_testgen_concept_surface_stays_closed_and_classified` checks the closed testgen scheduling arms and the `Generator` claim kind / anchor / classification / slot field set; `t19_language_behavior_equivalence_generated_claims_parse` / `t19_language_behavior_equivalence_run_test_claim_receipts_present` pin the LBE generator slice; `t19_idempotent_operation_generated_claims_parse_and_pin_emission` pins the idempotent-operation generator slice (`src/v4/std/effects.dag` canonical `IdempotentShape`/`EffectShape` witnesses + `idempotent_operation_witness_node`; outside the six-way `TestgenConcept` coproduct; label-only skip); `t19_manual_manifest_matches_claim_anchor_discriminants` checks manual claim anchors join to the manifest by `T19ManualAnchorKey`; `t20_bootstrap_plan_keeps_self_hosting_chain_as_data` checks the seed/self0/self1/fixpt bootstrap chain is encoded as `CompileStage` / `BootstrapPlan` data; `t22_diagnostic_assert_eval_witnesses_parse` checks `diagnostic_assert_eval.dag` parses; `t22_eval_diagnostic_assert_not_deferred_in_substrate` checks `05_eval.dag` no longer contains `eval_rejected_assert_kind_deferred`, executes `DiagnosticAssert`, and routes `run_test_claim` through `aggregate_verdicts`. | | `src/v3/compiler/tests/integration/coverage_defect_acceptance_dag_test.rs` | **Coverage-defect acceptance keys:** `src/v4/lens/coverage.dag` carries the canonical coverage-key set for `docs/design-dissolution-lens.md` §5.1; the old emit-template key is retired into `TemplateHole`, and the old string-escape key is split into `TemplateHole` plus `CanonicalCarrier`. **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the parse-level ratchet. **Dissolution:** remove when the v4 coverage lens runs as `.dag` / generated coverage and can assert the same acceptance rows without this host parser check. **Interim ratchet:** `coverage_defect_acceptance_keys_match_declared_rows` tokenizes/parses `src/v4/lens/coverage.dag` and asserts the exact parsed `(coverage_defect_* data row, CoverageDefectKey variant)` set matches the expected acceptance-key table while rejecting retired emit-template / string-escape names. | | `src/v3/compiler/tests/integration/v4_bin_main_dag_smoke_test.rs` | **T-15** (`src/v4/bin/main.dag` — trampoline **`String`** authority + B1 digest **placeholder** `Node`s; closed-tree invariant #2 / pure-bootstrap zero-floor per `docs/design-pure-bootstrap-zero.md`). **Grounded-indicator authoring on `main.dag` is HOLD** pending hub-relayed canonical spec (operator-direct format under-spec; neat-hawk-87 cascade 2026-05-19). **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **PR receipt (P5 Mechanism (b)):** this INVARIANTS row + matching `EXPECTED_HAND_AUTHORED_TEST` line in `sg0_census_test.rs` land in the same PR as the smoke harness. **Dissolution:** remove when `main.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness without this per-file Rust probe. **Interim ratchet:** `v4_bin_main_dag_tokenizes_and_parses_with_trampoline_source_anchor` runs `tokenize_for_test` + `parse_for_test` on the pinned `include_str!` source and asserts the trampoline / stub `data` identifiers plus the escaped `include!` spelling remain present in source text (full `compile_to_dag` on `main.dag` alone is deferred: `import v4.std.node` is not linked in the single-file harness). | diff --git a/scripts/ci-merge/sg0-pr-body-append.3556.txt b/scripts/ci-merge/sg0-pr-body-append.3556.txt new file mode 100644 index 00000000000..2ef0afb93f5 --- /dev/null +++ b/scripts/ci-merge/sg0-pr-body-append.3556.txt @@ -0,0 +1,3 @@ +SG-0 hand-path delta: +1 + +SG-0 pairing: (c) follow-up dispatch via gunb-ai/gunbc#3556 — T-21/T-24 Wave-0 net +1 on `EXPECTED_HAND_AUTHORED_TEST` for `v4_workflow_ci_runner_dag_smoke_test.rs` (INVARIANTS §P5(b) parse smoke on `workflow/ci.dag` selection entrypoints). Dissolves when Node-level TestClaim CI selection runs via `.dag` harness / host runner (subtree work-items A/B/C). diff --git a/src/v3/compiler/tests/integration.rs b/src/v3/compiler/tests/integration.rs index ceac8d13671..12d24a6fc8a 100644 --- a/src/v3/compiler/tests/integration.rs +++ b/src/v3/compiler/tests/integration.rs @@ -295,6 +295,8 @@ mod v4_lens_testgen_dag_smoke_test; mod v4_std_model_core_dag_smoke_test; #[path = "integration/v4_test_bootstrap_infra_closeout_test.rs"] mod v4_test_bootstrap_infra_closeout_test; +#[path = "integration/v4_workflow_ci_runner_dag_smoke_test.rs"] +mod v4_workflow_ci_runner_dag_smoke_test; #[path = "integration/value_body_substrate_mirror_isomorphism_test.rs"] mod value_body_substrate_mirror_isomorphism_test; #[path = "integration/common/wiring_scanner_test.rs"] diff --git a/src/v3/compiler/tests/integration/sg0_census_test.rs b/src/v3/compiler/tests/integration/sg0_census_test.rs index 16a7fc51c9f..0b8f3b44f2a 100644 --- a/src/v3/compiler/tests/integration/sg0_census_test.rs +++ b/src/v3/compiler/tests/integration/sg0_census_test.rs @@ -870,6 +870,9 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[ // SG-0 + INVARIANTS §P5(b) receipt; dissolves when the same checks are `.dag` // TestClaims or generated harness coverage. "src/v3/compiler/tests/integration/v4_test_bootstrap_infra_closeout_test.rs", + // T-21/T-24: `workflow/ci.dag` Wave-0 selection consumes `RerunNodeSet` for TestClaim roster narrowing. + // SG-0 + INVARIANTS §P5(b) receipt; dissolves when `.dag` TestClaim harness replaces probe. + "src/v3/compiler/tests/integration/v4_workflow_ci_runner_dag_smoke_test.rs", // §1.8 gate #96 (`value_body_substrate_mirror_isomorphism_executable`): // CI-visible generated Rust `ValueBody` mirror vs `substrate.dag` // constructor isomorphism. Dissolves when `ValueBody` no longer has a diff --git a/src/v3/compiler/tests/integration/v4_workflow_ci_runner_dag_smoke_test.rs b/src/v3/compiler/tests/integration/v4_workflow_ci_runner_dag_smoke_test.rs new file mode 100644 index 00000000000..a79a9cb6f38 --- /dev/null +++ b/src/v3/compiler/tests/integration/v4_workflow_ci_runner_dag_smoke_test.rs @@ -0,0 +1,192 @@ +//! **Layer:** integration +//! +//! T-21/T-24 Wave-0: `src/v4/workflow/ci.dag` (`v4.workflow.ci`) exposes affected-set-driven +//! `TestClaim` roster selection over `RerunNodeSet` (kernel `filter`/`any`/`contains`; +//! evaluation-node projection in `verification.dag`). Receipt +//! claims live in `src/v4/test/claim/workflow/affected_set_ci_runner.dag`. +//! +//! **TESTING.md:** M1(2.7) tokenize/parse gate; full `compile_to_dag` import merge +//! deferred until cross-module v4 load lands (same posture as peer v4 smoke tests). +//! +//! **ROADMAP:** `ROADMAP.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; +//! **TASKS.md** T-21 + T-24. +//! +//! **Dissolution:** remove when `.dag` TestClaim execution covers these claims without +//! this hand-Rust parse harness. + +use v3_compiler::parse_for_test; +use v3_compiler::parse_surface::SurfaceItem; +use v3_compiler::tokenize_for_test; + +const CI_DAG: &str = include_str!("../../../../v4/workflow/ci.dag"); +const CI_DAG_PATH: &str = "src/v4/workflow/ci.dag"; +const CLAIM_DAG: &str = + include_str!("../../../../v4/test/claim/workflow/affected_set_ci_runner.dag"); +const CLAIM_PATH: &str = "src/v4/test/claim/workflow/affected_set_ci_runner.dag"; + +fn parse_module(source: &str, path: &str) -> v3_compiler::parse_surface::SurfaceModule { + let tokens = + tokenize_for_test(source, path).unwrap_or_else(|e| panic!("{path}: tokenize: {e:?}")); + parse_for_test(&tokens, path).unwrap_or_else(|e| panic!("{path}: parse: {e:?}")) +} + +fn module_paths(module: &v3_compiler::parse_surface::SurfaceModule) -> Vec> { + module + .items + .iter() + .filter_map(|item| match item { + SurfaceItem::Module { path, .. } => { + Some(path.iter().map(String::as_str).collect::>()) + } + _ => None, + }) + .collect() +} + +fn import_includes_name( + module: &v3_compiler::parse_surface::SurfaceModule, + path: &[&str], + name: &str, +) -> bool { + module.items.iter().any(|item| { + let SurfaceItem::Import { + path: item_path, + names, + .. + } = item + else { + return false; + }; + item_path.len() == path.len() + && item_path + .iter() + .zip(path.iter()) + .all(|(a, &b)| a.as_str() == b) + && names.iter().any(|n| n == name) + }) +} + +fn surface_declares_fn(module: &v3_compiler::parse_surface::SurfaceModule, name: &str) -> bool { + module.items.iter().any(|item| match item { + SurfaceItem::Fn { + name: item_name, .. + } + | SurfaceItem::FnExternalBody { + name: item_name, .. + } => item_name == name, + _ => false, + }) +} + +fn surface_declares_test_claim_data( + module: &v3_compiler::parse_surface::SurfaceModule, + name: &str, +) -> bool { + use v3_compiler::parse_surface::SurfaceType; + module.items.iter().any(|item| match item { + SurfaceItem::Data { + name: item_name, + ty: SurfaceType::Named { name: ty_name, .. }, + .. + } => item_name == name && ty_name == "TestClaim", + _ => false, + }) +} + +#[test] +fn v4_workflow_ci_dag_tokenizes_and_parses() { + let _module = parse_module(CI_DAG, CI_DAG_PATH); +} + +#[test] +fn v4_workflow_ci_test_claim_selection_entrypoints() { + let module = parse_module(CI_DAG, CI_DAG_PATH); + assert_eq!( + module_paths(&module), + vec![vec!["v4", "workflow", "ci"]], + "{CI_DAG_PATH}: module authority path" + ); + for name in [ + "ci_select_from_rerun_nodes", + "ci_select_from_affected_set", + "test_claim_in_rerun_frontier", + ] { + assert!( + surface_declares_fn(&module, name), + "{CI_DAG_PATH}: must declare {name}" + ); + } + assert!( + import_includes_name( + &module, + &["v4", "lens", "affected_set"], + "affected_set_rerun_nodes" + ), + "{CI_DAG_PATH}: must import affected_set_rerun_nodes from T-21 lens" + ); + assert!( + import_includes_name( + &module, + &["v4", "std", "verification"], + "test_claim_evaluation_touches_rerun_frontier" + ), + "{CI_DAG_PATH}: must import subtree-aware frontier membership from verification" + ); + assert!( + import_includes_name( + &module, + &["v4", "std", "verification"], + "test_claim_ci_selection_fail_closed" + ), + "{CI_DAG_PATH}: must import fail-closed diagnostic selection guard from verification" + ); + assert!( + import_includes_name(&module, &["v4", "std", "algebra"], "filter"), + "{CI_DAG_PATH}: must import filter from std.algebra" + ); +} + +#[test] +fn v4_workflow_affected_set_ci_runner_claim_dag_tokenizes_and_parses() { + let _module = parse_module(CLAIM_DAG, CLAIM_PATH); +} + +#[test] +fn v4_workflow_affected_set_ci_runner_claim_wiring() { + let module = parse_module(CLAIM_DAG, CLAIM_PATH); + assert_eq!( + module_paths(&module), + vec![vec![ + "v4", + "test", + "claim", + "workflow", + "affected_set_ci_runner" + ]], + "{CLAIM_PATH}: module authority path" + ); + for name in ["ci_select_from_rerun_nodes", "ci_select_from_affected_set"] { + assert!( + import_includes_name(&module, &["v4", "workflow", "ci"], name), + "{CLAIM_PATH}: must import {name} from canonical workflow/ci authority" + ); + } + for claim in [ + "ci_runner_narrow_selection_claim", + "ci_runner_fail_closed_superset_claim", + "ci_runner_shape_collision_claim", + "ci_runner_inner_frontier_claim", + ] { + assert!( + surface_declares_test_claim_data(&module, claim), + "{CLAIM_PATH}: must declare structural receipt `{claim}`" + ); + } + assert!( + surface_declares_fn(&module, "ci_runner_narrow_selection_holds") + && surface_declares_fn(&module, "ci_runner_fail_closed_superset_holds") + && surface_declares_fn(&module, "ci_runner_shape_collision_holds") + && surface_declares_fn(&module, "ci_runner_inner_frontier_holds"), + "{CLAIM_PATH}: receipt predicates must exercise ci selection entrypoints" + ); +} diff --git a/src/v4/extdeps/languages/swift.dag b/src/v4/extdeps/languages/swift.dag index d92a39c2c3a..77d5d44b95b 100644 --- a/src/v4/extdeps/languages/swift.dag +++ b/src/v4/extdeps/languages/swift.dag @@ -351,11 +351,14 @@ fn swift_nonnumeric_representation_node(facts: SwiftNonNumericPrimitiveFacts) -> fn swift_nonnumeric_scalar_classifier_node(facts: SwiftNonNumericPrimitiveFacts) -> Node { match facts { - SwiftBoolPrimitiveFacts { representation: _ } => swift_atom(id: swift_tag_scalar_bool) - SwiftCharacterPrimitiveFacts { representation: _ } => + SwiftBoolPrimitiveFacts { surface_spelling: _, representation: _ } => + swift_atom(id: swift_tag_scalar_bool) + SwiftCharacterPrimitiveFacts { surface_spelling: _, representation: _ } => swift_atom(id: swift_tag_scalar_character) - SwiftStringPrimitiveFacts { representation: _ } => swift_atom(id: swift_tag_scalar_string) - SwiftVoidPrimitiveFacts { representation: _ } => swift_atom(id: swift_tag_scalar_void) + SwiftStringPrimitiveFacts { surface_spelling: _, representation: _ } => + swift_atom(id: swift_tag_scalar_string) + SwiftVoidPrimitiveFacts { surface_spelling: _, representation: _ } => + swift_atom(id: swift_tag_scalar_void) } } diff --git a/src/v4/std/algebra.dag b/src/v4/std/algebra.dag index f292ae8e932..bc6db5a3005 100644 --- a/src/v4/std/algebra.dag +++ b/src/v4/std/algebra.dag @@ -130,6 +130,31 @@ fn for_all(xs: FreeMonoid, predicate: fn(T) -> Bool) -> Bool { } +fn any(xs: FreeMonoid, predicate: fn(T) -> Bool) -> Bool { + fold_list(xs: xs, empty: false, cons: fn(acc, item) { + match acc { + true => true + false => predicate(item) + } + }) +} + + +fn filter(xs: FreeMonoid, predicate: fn(T) -> Bool) -> FreeMonoid { + fold_list_right(xs: xs, empty: Empty, snoc: fn(acc, item) { + match predicate(item) { + true => Cons { head: item, tail: acc } + false => acc + } + }) +} + + +fn contains(xs: FreeMonoid, item: T, eq: fn(T, T) -> Bool) -> Bool { + any(xs: xs, predicate: fn(candidate) { eq(candidate, item) }) +} + + fn count_where(xs: FreeMonoid, predicate: fn(T) -> Bool) -> Int { fold_list(xs: xs, empty: 0, cons: fn(count, item) { match predicate(item) { diff --git a/src/v4/std/verification.dag b/src/v4/std/verification.dag index 40556767ff8..f403bd34ae9 100644 --- a/src/v4/std/verification.dag +++ b/src/v4/std/verification.dag @@ -7,14 +7,21 @@ module v4.std.verification -import v4.std.node { Node, Symbol } +import v4.std.algebra { Empty, any, fold_list } +import v4.std.collection { List, list_append, list_snoc_item } +import v4.std.node { Node, NodeFold, Symbol, fold_node } import v4.std.diagnostic { Accepted, + Correction, Diagnostic, Extent, + Locus, + NodeLocus, NonEmptyDiagnostics, + PortLocus, Outcome, Rejected, + Suggested, Textual, Unavailable, UserInputBoundary, @@ -143,6 +150,121 @@ fn test_claim_input(c: TestClaim) -> Node { } } + +fn locus_evaluation_nodes(at: Locus) -> List { + match at { + NodeLocus { anchor: a } => list_snoc_item(xs: Empty, item: a.at) + Textual { file: _, extent: _ } => Empty + PortLocus { anchor: _ } => Empty + } +} + + +fn correction_evaluation_nodes(c: Correction) -> List { + match c { + Suggested { node: n } => list_snoc_item(xs: Empty, item: n) + Unavailable { reason: _ } => Empty + } +} + + +fn diagnostic_evaluation_nodes(d: Diagnostic) -> List { + list_append( + left: locus_evaluation_nodes(at: d.at), + right: correction_evaluation_nodes(c: d.correction) + ) +} + + +fn diagnostic_list_evaluation_nodes(ds: List) -> List { + fold_list( + xs: ds, + empty: Empty, + cons: fn(acc, d) { + list_append(left: acc, right: diagnostic_evaluation_nodes(d: d)) + } + ) +} + + +fn non_empty_diagnostics_evaluation_nodes(d: NonEmptyDiagnostics) -> List { + list_append( + left: diagnostic_evaluation_nodes(d: d.head), + right: diagnostic_list_evaluation_nodes(ds: d.tail) + ) +} + + +// All Nodes whose mutation invalidates claim evaluation (IRT-4 / CI rerun frontier). +fn test_claim_evaluation_nodes(c: TestClaim) -> List { + match c { + EqualsClaim { lhs: l, rhs: r, label: _, t19_anchor: _, classification: _ } => + list_snoc_item(xs: list_snoc_item(xs: Empty, item: l), item: r) + CompilesClaim { input: n, expected_value: e, label: _, t19_anchor: _, classification: _ } => + list_snoc_item(xs: list_snoc_item(xs: Empty, item: n), item: e) + DiagnosticClaim { input: n, expected_rejection: e, label: _, t19_anchor: _, classification: _ } => + list_append( + left: list_snoc_item(xs: Empty, item: n), + right: non_empty_diagnostics_evaluation_nodes(d: e) + ) + RoundTripClaim { input: n, label: _, t19_anchor: _, classification: _ } => + list_snoc_item(xs: Empty, item: n) + } +} + + +fn node_subtree_nodes(root: Node) -> List { + fold_node( + n: root, + algebra: NodeFold { + init: fn(self) { list_snoc_item(xs: Empty, item: self) }, + step: fn(acc, edge, sub) { + list_snoc_item(xs: list_append(left: acc, right: sub), item: edge.target) + } + } + ) +} + + +fn node_in_subtree_by_identity(root: Node, needle: Node) -> Bool { + any( + xs: node_subtree_nodes(root: root), + predicate: fn(member) { member == needle } + ) +} + + +// Consume affected-set rerun nodes directly: frontier root equality or frontier node inside evaluation tree. +fn test_claim_evaluation_node_touches_frontier(n: Node, frontier: List) -> Bool { + any( + xs: frontier, + predicate: fn(f) { + (n == f) || node_in_subtree_by_identity(root: n, needle: f) + } + ) +} + + +fn test_claim_evaluation_touches_rerun_frontier(c: TestClaim, frontier: List) -> Bool { + any( + xs: test_claim_evaluation_nodes(c: c), + predicate: fn(n) { test_claim_evaluation_node_touches_frontier(n: n, frontier: frontier) } + ) +} + + +// 🟡 gated — predicate-dissolution interim (docs/modeling-discipline.md Practice 10) — feature: t21-t24-ci-selection-diagnostic-fail-closed — consumer: v4.workflow.ci ci_select_from_rerun_nodes — bind TASKS.md T-24 — dissolve-on-arrival: delete when workflow/ci.dag ci_select consumes TestClaimCacheKey from 05_eval (IRT-4 cache-key boundary); forbidden: permanent untagged Bool coproduct-arm CI policy in std/verification. +fn test_claim_ci_selection_fail_closed(c: TestClaim) -> Bool { + match c { + DiagnosticClaim { label: _, t19_anchor: _, input: _, expected_rejection: _, classification: _ } => + true + CompilesClaim { label: _, t19_anchor: _, input: _, expected_value: _, classification: _ } => + false + EqualsClaim { label: _, t19_anchor: _, lhs: _, rhs: _, classification: _ } => false + RoundTripClaim { label: _, t19_anchor: _, input: _, classification: _ } => false + } +} + fn test_claim_t19_anchor(c: TestClaim) -> T19ManualAnchorKey { match c { CompilesClaim { t19_anchor: k, label: _, input: _, expected_value: _, classification: _ } => k diff --git a/src/v4/test/claim/workflow/affected_set_ci_runner.dag b/src/v4/test/claim/workflow/affected_set_ci_runner.dag new file mode 100644 index 00000000000..c4adc7bfa19 --- /dev/null +++ b/src/v4/test/claim/workflow/affected_set_ci_runner.dag @@ -0,0 +1,298 @@ +// src/v4/test/claim/workflow/affected_set_ci_runner.dag +// Scope: T-21/T-24 receipt — CI runner narrows TestClaim roster via RerunNodeSet node frontier. +// Owns: ci_runner_narrow_selection_claim, ci_runner_fail_closed_superset_claim, +// ci_runner_shape_collision_claim, ci_runner_inner_frontier_claim. +// Consumes: v4.workflow.ci, v4.lens.affected_set, v4.std.change, v4.std.verification. +// Status: structural claims; host execution lands with generated TestClaim harness. + +module v4.test.claim.workflow.affected_set_ci_runner + +import v4.lens.affected_set { + RerunNodeSet, + RerunNodeSetProduced +} +import v4.std.change { + AffectedSet, + AffectedSetFailClosed, + AffectedSetEvidence, + AffectedSetReason, + ChangeSet +} +import v4.std.algebra { count_equal, length } +import v4.std.collection { List } +import v4.std.logic { Bool } +import v4.std.node { Atom, Conj, Edge, Node, Positional, Symbol, TypeNode } +import v4.std.verification { + EqualsClaim, + TestClaim, + TestClassification, + T19ManualAnchorAbsent, + Tier1, + Unit +} +import v4.workflow.ci { ci_select_from_affected_set, ci_select_from_rerun_nodes } + +data ci_runner_untouched_symbol: Symbol = ci_runner_untouched_symbol +data ci_runner_touched_symbol: Symbol = ci_runner_touched_symbol +data ci_runner_other_symbol: Symbol = ci_runner_other_symbol +data ci_runner_shape_a_symbol: Symbol = ci_runner_shape_a_symbol +data ci_runner_shape_b_symbol: Symbol = ci_runner_shape_b_symbol +data ci_runner_fail_closed_reason: Symbol = ci_runner_fail_closed_reason + +data ci_runner_untouched_node: Node = Node { + kind: TypeNode { connective: Atom { identity: ci_runner_untouched_symbol } }, + children: [] +} + +data ci_runner_touched_node: Node = Node { + kind: TypeNode { connective: Atom { identity: ci_runner_touched_symbol } }, + children: [] +} + +data ci_runner_other_node: Node = Node { + kind: TypeNode { connective: Atom { identity: ci_runner_other_symbol } }, + children: [] +} + +data ci_runner_shape_a_node: Node = Node { + kind: TypeNode { connective: Atom { identity: ci_runner_shape_a_symbol } }, + children: [] +} + +data ci_runner_shape_b_node: Node = Node { + kind: TypeNode { connective: Atom { identity: ci_runner_shape_b_symbol } }, + children: [] +} + +data ci_runner_conj_wrapped_touched_node: Node = Node { + kind: TypeNode { connective: Conj }, + children: [ + Edge { + label: Positional, + target: ci_runner_touched_node + } + ] +} + +data ci_runner_claim_untouched: TestClaim = EqualsClaim { + label: "workflow/affected_set_ci_runner: untouched claim input", + t19_anchor: T19ManualAnchorAbsent, + lhs: ci_runner_untouched_node, + rhs: ci_runner_untouched_node, + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data ci_runner_claim_touched: TestClaim = EqualsClaim { + label: "workflow/affected_set_ci_runner: touched claim input", + t19_anchor: T19ManualAnchorAbsent, + lhs: ci_runner_touched_node, + rhs: ci_runner_touched_node, + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data ci_runner_claim_other: TestClaim = EqualsClaim { + label: "workflow/affected_set_ci_runner: other claim input", + t19_anchor: T19ManualAnchorAbsent, + lhs: ci_runner_other_node, + rhs: ci_runner_other_node, + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data ci_runner_fixture_roster: List = [ + ci_runner_claim_untouched, + ci_runner_claim_touched, + ci_runner_claim_other +] + +data ci_runner_narrow_rerun_nodes: RerunNodeSet = RerunNodeSetProduced { + nodes: [ci_runner_touched_node] +} + +data ci_runner_fail_closed_evidence: AffectedSetEvidence = AffectedSetReason { + reason: ci_runner_fail_closed_reason +} + +data ci_runner_fail_closed_affected: AffectedSet = AffectedSetFailClosed { + changes: ChangeSet { changes: [] }, + evidence: ci_runner_fail_closed_evidence +} + +fn ci_runner_narrow_selection_holds() -> Bool { + let rerun = ci_select_from_rerun_nodes( + roster: ci_runner_fixture_roster, + rerun: ci_runner_narrow_rerun_nodes + ) + (length(xs: rerun) == 1) + && count_equal( + xs: rerun, + item: ci_runner_claim_touched, + eq: fn(left, right) { left == right } + ) != 0 +} + +fn ci_runner_fail_closed_superset_holds() -> Bool { + let roster = ci_select_from_affected_set( + roster: ci_runner_fixture_roster, + affected: ci_runner_fail_closed_affected + ) + (length(xs: roster) == 3) + && count_equal( + xs: roster, + item: ci_runner_claim_untouched, + eq: fn(left, right) { left == right } + ) != 0 + && count_equal( + xs: roster, + item: ci_runner_claim_touched, + eq: fn(left, right) { left == right } + ) != 0 + && count_equal( + xs: roster, + item: ci_runner_claim_other, + eq: fn(left, right) { left == right } + ) != 0 +} + +fn ci_runner_narrow_selection_rhs() -> Node { + if ci_runner_narrow_selection_holds() { + ci_runner_touched_node + } else { + Node { + kind: TypeNode { connective: Conj }, + children: [] + } + } +} + +fn ci_runner_fail_closed_superset_rhs() -> Node { + if ci_runner_fail_closed_superset_holds() { + ci_runner_untouched_node + } else { + Node { + kind: TypeNode { connective: Conj }, + children: [] + } + } +} + +data ci_runner_narrow_selection_claim: TestClaim = EqualsClaim { + label: "workflow/affected_set_ci_runner: RerunNodeSet narrows TestClaim roster to touched input", + t19_anchor: T19ManualAnchorAbsent, + lhs: ci_runner_touched_node, + rhs: ci_runner_narrow_selection_rhs(), + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data ci_runner_fail_closed_superset_claim: TestClaim = EqualsClaim { + label: "workflow/affected_set_ci_runner: fail-closed affected-set selects full roster", + t19_anchor: T19ManualAnchorAbsent, + lhs: ci_runner_untouched_node, + rhs: ci_runner_fail_closed_superset_rhs(), + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data ci_runner_claim_shape_a: TestClaim = EqualsClaim { + label: "workflow/affected_set_ci_runner: shape-a atom claim", + t19_anchor: T19ManualAnchorAbsent, + lhs: ci_runner_shape_a_node, + rhs: ci_runner_shape_a_node, + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data ci_runner_claim_shape_b: TestClaim = EqualsClaim { + label: "workflow/affected_set_ci_runner: shape-b atom claim (same shape, different Symbol)", + t19_anchor: T19ManualAnchorAbsent, + lhs: ci_runner_shape_b_node, + rhs: ci_runner_shape_b_node, + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data ci_runner_shape_collision_roster: List = [ + ci_runner_claim_shape_a, + ci_runner_claim_shape_b +] + +data ci_runner_shape_collision_rerun_nodes: RerunNodeSet = RerunNodeSetProduced { + nodes: [ci_runner_shape_a_node] +} + +fn ci_runner_shape_collision_holds() -> Bool { + let rerun = ci_select_from_rerun_nodes( + roster: ci_runner_shape_collision_roster, + rerun: ci_runner_shape_collision_rerun_nodes + ) + (length(xs: rerun) == 1) + && count_equal( + xs: rerun, + item: ci_runner_claim_shape_a, + eq: fn(left, right) { left == right } + ) != 0 +} + +fn ci_runner_shape_collision_rhs() -> Node { + if ci_runner_shape_collision_holds() { + ci_runner_shape_a_node + } else { + Node { + kind: TypeNode { connective: Conj }, + children: [] + } + } +} + +data ci_runner_shape_collision_claim: TestClaim = EqualsClaim { + label: "workflow/affected_set_ci_runner: shared Atom shape does not false-positive second claim", + t19_anchor: T19ManualAnchorAbsent, + lhs: ci_runner_shape_a_node, + rhs: ci_runner_shape_collision_rhs(), + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data ci_runner_claim_conj_wrapped: TestClaim = EqualsClaim { + label: "workflow/affected_set_ci_runner: inner frontier atom inside Conj lhs", + t19_anchor: T19ManualAnchorAbsent, + lhs: ci_runner_conj_wrapped_touched_node, + rhs: ci_runner_conj_wrapped_touched_node, + classification: TestClassification { tier: Tier1, layer: Unit } +} + +data ci_runner_inner_frontier_roster: List = [ + ci_runner_claim_untouched, + ci_runner_claim_conj_wrapped +] + +data ci_runner_inner_frontier_rerun_nodes: RerunNodeSet = RerunNodeSetProduced { + nodes: [ci_runner_touched_node] +} + +fn ci_runner_inner_frontier_holds() -> Bool { + let rerun = ci_select_from_rerun_nodes( + roster: ci_runner_inner_frontier_roster, + rerun: ci_runner_inner_frontier_rerun_nodes + ) + (length(xs: rerun) == 1) + && count_equal( + xs: rerun, + item: ci_runner_claim_conj_wrapped, + eq: fn(left, right) { left == right } + ) != 0 +} + +fn ci_runner_inner_frontier_rhs() -> Node { + if ci_runner_inner_frontier_holds() { + ci_runner_touched_node + } else { + Node { + kind: TypeNode { connective: Conj }, + children: [] + } + } +} + +data ci_runner_inner_frontier_claim: TestClaim = EqualsClaim { + label: "workflow/affected_set_ci_runner: dependent inner atom matches Conj-wrapped lhs", + t19_anchor: T19ManualAnchorAbsent, + lhs: ci_runner_touched_node, + rhs: ci_runner_inner_frontier_rhs(), + classification: TestClassification { tier: Tier1, layer: Unit } +} diff --git a/src/v4/workflow/ci.dag b/src/v4/workflow/ci.dag index 08f3be33b8b..7dc6d8b4248 100644 --- a/src/v4/workflow/ci.dag +++ b/src/v4/workflow/ci.dag @@ -1,8 +1,8 @@ // src/v4/workflow/ci.dag -// Scope: CI pipeline AS DATA; gunbc job/gate DAG + eager well-formedness; ci.yml projection deferred. -// Owns: CiCommand, CiJob, CiGate, CiPipeline, ci_pipeline_well_formed, ci_pipeline -// Consumes: v4.lens.registry, v4.std.node, v4.std.diagnostic, v4.std.algebra, v4.workflow.bootstrap -// Status: filled — declarative core + eager well-formedness; structural v2 gate only. +// Scope: CI pipeline AS DATA; gunbc job/gate DAG + eager well-formedness; Wave-0 TestClaim roster selection; ci.yml projection deferred. +// Owns: CiCommand, CiJob, CiGate, CiPipeline, ci_pipeline_well_formed, ci_pipeline, ci_select_from_affected_set, ci_select_from_rerun_nodes, test_claim_in_rerun_frontier +// Consumes: v4.lens.registry, v4.lens.affected_set, v4.std.change, v4.std.node, v4.std.diagnostic, v4.std.algebra, v4.std.verification, v4.workflow.bootstrap +// Status: filled — declarative core + eager well-formedness + T-21/T-24 affected-set TestClaim selection (structural v2 gate only). module v4.workflow.ci @@ -17,15 +17,28 @@ import v4.lens.registry { UnusedParameters, lens_registry_ids_resolve } -import v4.std.node { Symbol } +import v4.lens.affected_set { + RerunNodeSet, + RerunNodeSetFailClosed, + RerunNodeSetProduced, + affected_set_rerun_nodes +} +import v4.std.change { AffectedSet } +import v4.std.node { Node, Symbol } import v4.std.diagnostic {Correction, Diagnostic, Extent, Locus, NoCorrectionReason, Outcome, Accepted, None, diagnostics_singleton} import v4.std.algebra { count_equal, count_where, + filter, for_all, length, unique } +import v4.std.verification { + TestClaim, + test_claim_ci_selection_fail_closed, + test_claim_evaluation_touches_rerun_frontier +} import v4.workflow.bootstrap { v4_stage0_binary, bootstrap_plan, bootstrap_stage_output } @@ -240,3 +253,31 @@ fn ci_pipeline_well_formed(p: CiPipeline) -> Outcome { Rejected { diagnostics: diagnostics_singleton(d: ci_diagnostic(reason: ci_duplicate_job_id)) } } } + + +fn test_claim_in_rerun_frontier(claim: TestClaim, frontier: List) -> Bool { + test_claim_evaluation_touches_rerun_frontier(c: claim, frontier: frontier) +} + + +fn ci_select_from_rerun_nodes(roster: List, rerun: RerunNodeSet) -> List { + match rerun { + RerunNodeSetProduced { nodes: nodes } => + filter( + xs: roster, + predicate: fn(claim) { + test_claim_ci_selection_fail_closed(c: claim) + || test_claim_in_rerun_frontier(claim: claim, frontier: nodes) + } + ) + RerunNodeSetFailClosed { evidence: _ } => roster + } +} + + +fn ci_select_from_affected_set(roster: List, affected: AffectedSet) -> List { + ci_select_from_rerun_nodes( + roster: roster, + rerun: affected_set_rerun_nodes(affected_set_value: affected) + ) +}