From 5b4477ef25ac863301c67fa63a1c87ab2767a99a Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 31 May 2026 15:40:37 +0000 Subject: [PATCH 1/3] WIP: SG-5 SG-6 implementation per collection-bounded-lattice worksheet on mai --- ...on-bounded-lattice-worksheet-2026-05-30.md | 52 ++++++++++++- ...4_std_target_realization_dag_smoke_test.rs | 73 +++++++++++++++++++ ...er_bounded_lattice_completeness_anchor.dag | 57 ++++++++++++++- 3 files changed, 180 insertions(+), 2 deletions(-) diff --git a/docs/planning/v4-sg5-sg6-collection-bounded-lattice-worksheet-2026-05-30.md b/docs/planning/v4-sg5-sg6-collection-bounded-lattice-worksheet-2026-05-30.md index c95b78ee9a3..6bb5cfb4d30 100644 --- a/docs/planning/v4-sg5-sg6-collection-bounded-lattice-worksheet-2026-05-30.md +++ b/docs/planning/v4-sg5-sg6-collection-bounded-lattice-worksheet-2026-05-30.md @@ -89,13 +89,63 @@ Emit must not fabricate meet/join stubs. --- +## §5 Landing order (implementation — not worksheet-only PR) + +```text +1. TargetCollectionRealization carrier + choice/witness coproducts in v4.std.target_model. +2. Rust Set collection_realization row on rust TargetModel bundle (extdeps/languages/rust.dag). +3. 06_translate collection projection consumes primary + alternatives OR fail-closed fallback. +4. bounded_lattice_completeness.dag (cycle-breaker) + 04_infer consumer completeness gate. +5. Manual falsification claims: sg5_set_non_ordable_falsification + infer_bounded_lattice_completeness_anchor. +``` + +**Lane split:** Target Realization owns steps 1–3; Compiler Spine owns step 4; Runtime/TestClaim owns step 5. + +--- + +## §6 Downstream worker brief (dispatch after §8) + +```text +Implement SG-5 + SG-6 per approved worksheet §10.0 on main. + +MUST: + - Author TargetCollectionRealization in v4.std.target_model; Rust Set row(s) in rust.dag; + refactor 06_translate collection projection to consume bundle rows (fail-closed fallback). + - Author bounded_lattice_instance_completeness in v4.std.bounded_lattice_completeness; + wire 04_infer consumer gate (partial declarations tagged; consumer sites reject). + - Land manual falsification probes: Set fail-closed (SG-5 CompilesClaim); + missing-meet BoundedLattice infer rejection (SG-6 CompilesClaim). + - Include variant-shape histogram for new coproduct arms (v4-substrate-pr-review-gate §3). + +MUST NOT: + - Rust-side T: Ord patches without model authority; silent BTreeSet default; dummy meet/join at emit. + - Fold SG-COLLECTION-PROJECTION FreeMonoid→Vec band into this PR without Modeling DFS ack. + - Use SG-5/6 rustc error-count reduction as acceptance. + +Escalate to Modeling DFS: + - declared_inhabitants witness wiring required before dissolving 🟡 SG-5-element-trait-eligibility. + - Structural set_carrier recognition without Cardinality predicate (🟡 SG-5-set-carrier-recognition). + - Need Map collection row beyond catalog scope without worksheet amendment. +``` + +--- + +## §7 Non-goals + +- SG-COLLECTION-PROJECTION (~170 FreeMonoid→Vec errors) — separate dispatch; do not fold into SG-5/6 PR +- SG-RC-LAYERING / SG-1b / emit-binary M1 probe as primary acceptance +- `ci.dag` / ci.yml / shell gate migration +- Dissolving 🟡 MVP-1 kernel-atom eligibility or set_carrier predicate without named dissolve-on + +--- + ## §8 Manager approval checklist (`cool-ibex-692`) — CLOSED 2026-05-30 - [x] Single-authority facts identified (collection realization + infer gate) - [x] Spot-fixes forbidden (Ord patches, stub meet/join) - [x] Two work items (not one "fix SG-5/6" blob) - [x] Falsification probes accepted -- [ ] Worker dispatch — **authorized** (may parallel SG-2/SG-1 chain; independent substrate) +- [x] Worker dispatch — **authorized** (`keen-bat-825`; Modeling DFS GO 2026-05-31) ## Related artifacts diff --git a/src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs b/src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs index c49cd105d82..be243ce1288 100644 --- a/src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs +++ b/src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs @@ -14,6 +14,11 @@ const TRANSLATE_DAG: &str = include_str!("../../../../v4/compiler/06_translate.d const TRANSLATE_PATH: &str = "src/v4/compiler/06_translate.dag"; const RUST_LANGUAGE_DAG: &str = include_str!("../../../../v4/extdeps/languages/rust.dag"); const RUST_LANGUAGE_PATH: &str = "src/v4/extdeps/languages/rust.dag"; +const BOUNDED_LATTICE_COMPLETENESS_DAG: &str = + include_str!("../../../../v4/std/bounded_lattice_completeness.dag"); +const BOUNDED_LATTICE_COMPLETENESS_PATH: &str = "src/v4/std/bounded_lattice_completeness.dag"; +const INFER_DAG: &str = include_str!("../../../../v4/compiler/04_infer.dag"); +const INFER_PATH: &str = "src/v4/compiler/04_infer.dag"; fn parse_module(source: &str, path: &str) -> v3_compiler::parse_surface::SurfaceModule { let tokens = @@ -299,3 +304,71 @@ fn v4_rust_language_model_declares_target_atom_realization_rows() { "{RUST_LANGUAGE_PATH}: row/catalog host_bundle must include collection_realization so target_model_bundle_core(host) decode matches" ); } + +#[test] +fn v4_std_target_model_declares_target_collection_realization_carrier() { + let module = parse_module(TARGET_MODEL_DAG, TARGET_MODEL_PATH); + assert!( + surface_declares_type(&module, "TargetCollectionRealization"), + "{TARGET_MODEL_PATH}: SG-5 canonical collection realization carrier" + ); + assert!( + surface_declares_type(&module, "TargetCollectionReprKind"), + "{TARGET_MODEL_PATH}: representation kind must be a coproduct (M6)" + ); + assert!( + surface_declares_type(&module, "RequiredTraitWitness"), + "{TARGET_MODEL_PATH}: per-alternative trait witnesses must be typed" + ); + assert!( + surface_declares_fn(&module, "target_collection_select_choice"), + "{TARGET_MODEL_PATH}: primary/alternatives selection must be substrate authority" + ); +} + +#[test] +fn v4_translate_dag_imports_collection_realization_consumer() { + let module = parse_module(TRANSLATE_DAG, TRANSLATE_PATH); + assert!( + import_includes_name( + &module, + &["v4", "std", "target_model"], + "target_model_edge_collection_realization" + ), + "{TRANSLATE_PATH}: translate must read collection_realization bundle edge" + ); + assert!( + surface_declares_fn(&module, "project_set_collection_type_node"), + "{TRANSLATE_PATH}: Set carrier projection must consume TargetCollectionRealization rows" + ); + assert!( + surface_declares_fn(&module, "collection_realization_from_target"), + "{TRANSLATE_PATH}: collection rows must decode from TargetModel bundle" + ); +} + +#[test] +fn v4_bounded_lattice_completeness_and_infer_gate_are_wired() { + let bl_module = parse_module(BOUNDED_LATTICE_COMPLETENESS_DAG, BOUNDED_LATTICE_COMPLETENESS_PATH); + assert!( + surface_declares_fn(&bl_module, "bounded_lattice_instance_completeness"), + "{BOUNDED_LATTICE_COMPLETENESS_PATH}: SG-6 completeness classifier must live in cycle-breaker module" + ); + let infer_module = parse_module(INFER_DAG, INFER_PATH); + assert!( + import_includes_name( + &infer_module, + &["v4", "std", "bounded_lattice_completeness"], + "bounded_lattice_instance_completeness" + ), + "{INFER_PATH}: infer must import completeness from bounded_lattice_completeness.dag" + ); + assert!( + surface_declares_fn(&infer_module, "infer_bounded_lattice_consumer_gate"), + "{INFER_PATH}: consumer sites must reject partial BoundedLattice references" + ); + assert!( + surface_declares_fn(&infer_module, "partial_bounded_lattice_instances_in_tree"), + "{INFER_PATH}: partial instances must be collected before consumer gate" + ); +} diff --git a/src/v4/test/claim/manual/infer_bounded_lattice_completeness_anchor.dag b/src/v4/test/claim/manual/infer_bounded_lattice_completeness_anchor.dag index 861f67560a9..6a1bf0d7a87 100644 --- a/src/v4/test/claim/manual/infer_bounded_lattice_completeness_anchor.dag +++ b/src/v4/test/claim/manual/infer_bounded_lattice_completeness_anchor.dag @@ -1,6 +1,6 @@ // src/v4/test/claim/manual/infer_bounded_lattice_completeness_anchor.dag // Scope: SG-6 falsification probe — BoundedLattice instance completeness gate in 04_infer. -// Status: compile-only anchor; execution deferred to T-22 runner bridge. +// Status: manual receipt; consumer-site infer rejection — not emit compile_error! stubs. module v4.test.claim.manual.infer_bounded_lattice_completeness_anchor @@ -29,7 +29,17 @@ import v4.std.algebra { } import v4.std.bounded_lattice_completeness { bounded_lattice_instance_completeness } import v4.std.diagnostic { Accepted, Outcome, Rejected } +import v4.std.logic { Bool } import v4.std.node { Atom, Arrow, Conj, Edge, Named, Node, Symbol, TypeNode } +import v4.std.verification { + CompilesClaim, + ManualAnchorAbsent, + TestClaim, + TestClassification, + Tier1, + Unit, + manual_claim_anchor +} data anchor_meet_sym: Symbol = anchor_meet_sym @@ -219,3 +229,48 @@ fn anchor_infer_consumer_tree_is_rejected() -> Bool { data anchor_infer_consumer_tree_rejects: Bool = anchor_infer_consumer_tree_is_rejected() + + +data sg6_pass_sym: Symbol = sg6_pass_sym +data sg6_fail_sym: Symbol = sg6_fail_sym + + +fn sg6_pass_node() -> Node { + Node { + kind: TypeNode { connective: Atom { identity: sg6_pass_sym } }, + children: [] + } +} + + +fn sg6_fail_node() -> Node { + Node { + kind: TypeNode { connective: Atom { identity: sg6_fail_sym } }, + children: [] + } +} + + +fn sg6_claim_input(ok: Bool) -> Node { + if ok { + sg6_pass_node() + } else { + sg6_fail_node() + } +} + + +fn sg6_missing_meet_consumer_infer_rejects() -> Bool { + anchor_infer_consumer_tree_rejects + && anchor_partial_bounded_lattice_missing_meet + && anchor_bounded_lattice_completeness_classifies_instances +} + + +data claim_sg6_bounded_lattice_missing_meet_infer_rejects: TestClaim = CompilesClaim { + label: "manual/sg6: BoundedLattice missing meet rejects at infer consumer (not emit stub)", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + input: sg6_claim_input(ok: sg6_missing_meet_consumer_infer_rejects()), + expected_value: sg6_pass_node(), + classification: TestClassification { tier: Tier1, layer: Unit } +} From 602a3cdea24948be5daa4201a48c08ad91d041e3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 31 May 2026 15:54:03 +0000 Subject: [PATCH 2/3] chore: cargo fmt for v4_std_target_realization smoke tests Co-authored-by: Cursor --- .../integration/v4_std_target_realization_dag_smoke_test.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs b/src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs index be243ce1288..31665c74d85 100644 --- a/src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs +++ b/src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs @@ -349,7 +349,10 @@ fn v4_translate_dag_imports_collection_realization_consumer() { #[test] fn v4_bounded_lattice_completeness_and_infer_gate_are_wired() { - let bl_module = parse_module(BOUNDED_LATTICE_COMPLETENESS_DAG, BOUNDED_LATTICE_COMPLETENESS_PATH); + let bl_module = parse_module( + BOUNDED_LATTICE_COMPLETENESS_DAG, + BOUNDED_LATTICE_COMPLETENESS_PATH, + ); assert!( surface_declares_fn(&bl_module, "bounded_lattice_instance_completeness"), "{BOUNDED_LATTICE_COMPLETENESS_PATH}: SG-6 completeness classifier must live in cycle-breaker module" From 70185ee2cd634e672cc7fad8be679b597f14e979 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 31 May 2026 16:04:07 +0000 Subject: [PATCH 3/3] fix(P5): same-path receipt for SG-5/6 smoke expansion in target_realization harness Per cursor REQUEST_CHANGES on #4121: module P5 receipt, INVARIANTS_OPS row (+0 SG-0 paths), sg0 census comment, and sg0-pr-body-append.4121.txt pairing. Co-authored-by: Cursor --- _internal/INVARIANTS_OPS.md | 2 +- scripts/ci-merge/sg0-pr-body-append.4121.txt | 2 ++ .../compiler/tests/integration/sg0_census_test.rs | 3 ++- .../v4_std_target_realization_dag_smoke_test.rs | 15 ++++++++++++--- 4 files changed, 17 insertions(+), 5 deletions(-) create mode 100644 scripts/ci-merge/sg0-pr-body-append.4121.txt diff --git a/_internal/INVARIANTS_OPS.md b/_internal/INVARIANTS_OPS.md index e0121ea7232..2846a05dcc8 100644 --- a/_internal/INVARIANTS_OPS.md +++ b/_internal/INVARIANTS_OPS.md @@ -63,7 +63,7 @@ Per **Dispatch-Discipline Mechanisms (b)** above, each **new** path added to `EX | `src/v3/compiler/tests/integration/v4_lens_registry_dag_smoke_test.rs` | **Operator pin** `docs/briefs/r4-lane-a-lens-interface-freeze-pin.md` §3 / **PREFIX T-23 v0** (`src/v4/lens/registry.dag` — **`LensIdV0`** closed sum + **`LensModulePathV0`**) plus Lens-CI activation (`src/v4/workflow/ci.dag` consumes registry-backed `LensIdV0` rows). **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`. **P2 / Practice 5:** this host harness is a **parse-surface structural ratchet** for `src/v4/lens/registry.dag` + its `src/v4/workflow/ci.dag` consumer + the live `.github/workflows/ci.yml` Lens-CI signal binding, while preserving the staged T-23/P9 registry parse-cleanliness receipts; the semantic interface is checked in CI by `gunbc compile` over a temporary `ci.dag` entry root plus `src/v4` dependency root (not `--target dag`, which is blocked by the known DAG-artifact hang). **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 / CI pairing. **Dissolution:** remove when `registry.dag` and Lens-CI workflow wiring are exercised only by `.dag` `TestClaim` rows / a generated harness that mechanically reads registry rows and workflow commands without this per-file Rust parse ratchet. **Interim ratchet:** `v4_lens_registry_dag_tokenizes_and_parses` tokenizes/parses the pinned registry source and asserts module path, `LensIdV0`/`LensModulePathV0`, `lens_registry_v0`, `lens_registry_ids_resolve`, `lens_registry_row_count`, and `lens_registry_bound_row_count`; `v4_lens_registry_t23_closed_lens_ids_present` pins the eight-arm closed set; `v4_lens_registry_structural_resolution_bound_to_module` pins `StructuralResolution` → `Bound { path: "v4.lens.structural_resolution" }`; `v4_lens_registry_p9_owned_fn_surface_present` pins the P9 `LensOwnedFnV0` / `lens_owned_fn_registry_v0` substrate rows; `v4_ci_workflow_consumes_lens_registry_for_lens_ci_signal` tokenizes/parses `ci.dag`, asserts the `lens_registry_ids_resolve` import, `LensCiCommand.required_lenses: List`, the six required `LensIdV0` policy rows, `lens_ci_registry_signal` gate data, `lens_ci_registry_execution.needs == [v2_compile_src_v4]`, and `lens_ci_live_workflow_signal` as the modeled live-step binding without re-authoring the `ci_pipeline` signal/job/policy facts. It then parses `.github/workflows/ci.yml` and checks those modeled step names execute the registry smoke plus rust-target semantic compile. **Paired CI semantic gate:** `Lens-CI registry semantic v4 compile (rust target)` copies `src/v4/workflow/ci.dag` into a temporary entry root, copies `src/v4` into a dependency root with `workflow/ci.dag` removed, and runs `target/release/gunbc compile --source-root "$entry_root" --source-root "$deps_root" --output-dir "$RUNNER_TEMP/v4-lens-ci-rust" --target rust` so lowering/inference of `ci_command_authority_ok -> lens_registry_ids_resolve` is checked through the workflow consumer and its transitive v4 imports without making unrelated v4 extdeps entry modules for this Lens-CI signal. | | `src/v3/compiler/tests/integration/v4_lens_testgen_dag_smoke_test.rs` | **ROADMAP:** `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; **`src/v4/TASKS.md` § T-19** (`lens/testgen.dag` — producer of `TestClaim` corpus from substrate; Wave-0 bootstrap / manual claim lookup remains keyed by **`ManualAnchorKey`**; **`Generator.anchor`** now reuses the same **`ClaimAnchorKey`** carrier as **`TestClaim.anchor`**, with manual rows wrapped by **`ManualClaimAnchor`** after **`Outcome`** rejects **`ManualAnchorAbsent`** on lookup and generated rows partitioned under **`GeneratedClaimAnchor`** (**Practice 5** single-anchor schema; **LB-P4-3212** ratchet — cite PR #3212 / review thread). **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/lens/testgen.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness / merged M2 multi-module lowering without this host `parse_for_test` structural ratchet (isolated `compile_to_dag` does not resolve `import v4.std.*` peers under M1(2.7); see harness module comment). **Interim ratchet:** focused `#[test]` slices in `v4_lens_testgen_dag_smoke_test.rs` (**openai-pro** review **#14812** / **TESTING.md** discipline): `v4_lens_testgen_wave0_modules_tokenize_and_parse`; `v4_lens_testgen_wave0_verification_manual_anchor_key_only`; `v4_lens_testgen_wave0_function_inventory_matches_wave0`; `v4_lens_testgen_wave0_nat_symbol_import_authority`; `v4_lens_testgen_wave0_outcome_return_surfaces`; `v4_lens_testgen_wave0_generator_anchor_field_is_claim_anchor_key`; `v4_lens_testgen_wave0_concept_projection_matches_claim_anchor`; `v4_lens_testgen_wave0_generator_carries_claim_classification_and_anchor`; `v4_lens_testgen_wave0_bootstrap_threads_claim_anchor_into_generator`; `v4_lens_testgen_nat_law_manual_claims_use_compiles_stub`; `v4_lens_testgen_nat_substrate_carries_algebra_law_subject_symbols`; `v4_lens_testgen_testgen_carries_six_nat_algebra_law_scheduling_arms` — collectively tokenize/parse `src/v4/lens/testgen.dag` + `src/v4/std/verification.dag`, assert Wave-0 function inventory + `Outcome` return surfaces + `Generator.anchor: ClaimAnchorKey` carrier, substring wiring receipts on bootstrap join, `nat_law_anchors.dag` per-claim `kind: Compiles` on identical stub `input`/`expected` (law-bearing `Node` + `Equals` deferred to T-22; codex #14833), three `AlgebraLawSubject` `Symbol` rows in `src/v4/std/nat.dag`, and six `value: AlgebraLaw {` constructor sites in testgen (file-wide count); plus the **T-19 witness-validity generator-category guard** (PR #3565 same-file expansion, **+0 census paths**, P5 Mechanism (b) same-path ratchet): `v4_lens_testgen_witness_validity_modules_tokenize_and_parse`, `v4_lens_testgen_witness_validity_helper_returns_outcome_testclaim`, `v4_lens_testgen_witness_validity_module_imports_helper_from_lens_testgen`, `v4_lens_testgen_witness_validity_module_pins_four_row_corpus_via_helper`, `v4_lens_testgen_witness_validity_module_authors_no_testclaim_literals` — pin both `src/v4/lens/testgen.dag` + `src/v4/test/claim/generated/witness_validity.dag` parse, `testgen_emit_witness_validity_claim` return type `Outcome`, helper-routing import, exact 4-row corpus (1 positive + 3 negative arms), and the no-`TestClaim`-literal tautology-skip discipline on the generated module. Parse-only structural ratchet; `Generator` carries `kind`, `anchor`, `classification`, and `slot` per TASKS T-19. plus the **T-19 anchor-strip + AlgebraLaw subject helper guard** (PR #3636 same-file expansion, **+0 census paths**, P5 Mechanism (b) same-path ratchet): `v4_lens_testgen_wave0_generator_anchor_field_is_claim_anchor_key` asserts `Generator.kind: TestClaimCoproductVariant` and `Generator.anchor: ClaimAnchorKey`; `v4_lens_testgen_wave0_concept_projection_matches_claim_anchor` asserts match on `test_claim_anchor(c: claim)`; `v4_lens_testgen_wave0_generator_carries_claim_classification_and_anchor` adds `kind: test_claim_coproduct_variant(c: claim)` substring check; `assert_six_algebra_law_subject_paths_in_testgen` asserts `algebra_law_subject_for_manual_anchor` helper exists, match dispatch in `testgen_concept_for_manual_claim`, single `value: AlgebraLaw {` constructor site, all six `ManualNat*` anchor names (`ManualNatAddLeftIdentity`, `ManualNatAddRightIdentity`, `ManualNatAddAssociativity`, `ManualNatMulLeftIdentity`, `ManualNatMulAnnihilator`, `ManualNatMulAssociativity`) in helper body, and six `value: AlgebraLawSubject {` projection arms; `assert_nat_algebra_law_subject_symbols_in_substrate` adds six forbidden `nat_algebra_law_subject_symbol_*` substring checks (nat substrate must not re-export mirror operation/value symbols); `generator_field_ty` (parametric field-name lookup) and `between<'a>` helper added. | | `src/v3/compiler/tests/integration/v4_std_model_core_dag_smoke_test.rs` | **TASKS.md** **T-33** (`src/v4/std/model_core.dag` — Ratified Q1 `ModelCore` shared substrate: primitive fact bundles, `AlgebraInhabitanceDecl`, `AlgebraLawObligation` over modeled inhabitance + law `Node`, T-33-Q10 `EffectSignature` / `ResourceAccess`, and effect/partiality scaffolds). **ROADMAP:** `_internal/ROADMAP_OPS.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; SG-0 census net +1 pairing `(c)` is mechanically prepended via `scripts/ci-merge/sg0-pr-body-append.3474.txt` in CI (`.github/workflows/ci.yml`). **Dissolution:** remove when `model_core.dag` is exercised only by `.dag` `TestClaim` rows / a generated harness / merged M2 multi-module lowering without this host `parse_for_test` structural ratchet (isolated `compile_to_dag` does not resolve `import v4.std.*` peers under M1(2.7); see harness module comment). **Interim ratchet:** `v4_std_model_core_dag_tokenizes_and_parses`; `v4_std_model_core_declares_ratified_q1_carriers`; `v4_std_model_core_bundles_five_facets`; `v4_std_model_core_algebra_law_obligation_structural`; `v4_std_model_core_effect_partiality_ops_use_node_authority`; `v4_std_model_core_effect_signature_resource_access_shape`; `v4_std_model_core_wave1_void_constructor_present` — tokenize/parse the pinned `include_str!` source, assert `v4.std.model_core` module path, closed carrier inventory (`ModelCore`, `PrimitiveFactBundle`, `AlgebraInhabitanceDecl`, `AlgebraLawObligation`, `EffectSignature`, `ResourceAccess`, `EffectSemanticsDecl`, `PartialitySemanticsDecl`), five-facet `ModelCore` field bundle, `AlgebraLawObligation { inhabitance_witness: Node, law: Node }` (joins canonical `ModelCore.inhabitance` rows by witness; no embedded duplicate decl or Symbol labels), `PrimitiveOperationRef.operation` / `PartialOperationDecl.operation` `Node` authority, `PrimitiveOperationRef.effect_signature: EffectSignature`, `EffectSignature { signature: Node }` with resource authority kept on `BoundaryAllowance.resource`, `ResourceAccess { resource: Node }`, and `wave1_void` scaffold constructor (🟡 `feature:model-core-wave1-void-scaffold`, dissolve-on T-4/T-34 non-empty `ModelCore`). | -| `src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs` | **SG-1** (`src/v4/std/target_model.dag` — `TargetAtomRealization` canonical carrier per design-target-realization-canonical-home.md Option A, catalog encode/decode, `TargetValueTemplate` fail-closed `Outcome` application; Rust Symbol/Bool/Char rows in `src/v4/extdeps/languages/rust.dag`; `src/v4/compiler/06_translate.dag` consumer). **ROADMAP:** `_internal/ROADMAP_OPS.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 `target_model.dag` SG-1 realization surface is exercised only by `.dag` `TestClaim` rows / a generated harness / merged M2 multi-module lowering without this host `parse_for_test` structural ratchet. **Interim ratchet:** `v4_std_target_realization_dag_tokenizes_and_parses`; `v4_std_target_realization_declares_target_atom_realization_carrier`; `v4_std_target_realization_declares_catalog_lookup`; `v4_translate_dag_imports_target_atom_realization_consumer`; `v4_rust_language_model_declares_target_atom_realization_rows` — tokenize/parse `target_model.dag`, assert `TargetAtomRealization` field bundle (`source_carrier`, `type_form`, `value_form`), catalog lookup + row-driven type/value consumers, translate imports + `translate_target_atom_realization_for_carrier`, Rust atom-realization rows without parallel `rust_std_projection_*` sentinels. | +| `src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs` | **SG-1** (`src/v4/std/target_model.dag` — `TargetAtomRealization` canonical carrier per design-target-realization-canonical-home.md Option A, catalog encode/decode, `TargetValueTemplate` fail-closed `Outcome` application; Rust Symbol/Bool/Char rows in `src/v4/extdeps/languages/rust.dag`; `src/v4/compiler/06_translate.dag` consumer) + **SG-5/SG-6** (`TargetCollectionRealization` + `bounded_lattice_completeness.dag` / `04_infer` consumer gate — worksheet `docs/planning/v4-sg5-sg6-collection-bounded-lattice-worksheet-2026-05-30.md` §6; substrate #3957 / #4085 on `main`). **ROADMAP:** `_internal/ROADMAP_OPS.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. **This PR (+0 SG-0 paths):** expands the existing harness with three parse/tokenize smokes for SG-5 collection realization + translate consumer + SG-6 infer gate wiring (`v4_std_target_model_declares_target_collection_realization_carrier`, `v4_translate_dag_imports_collection_realization_consumer`, `v4_bounded_lattice_completeness_and_infer_gate_are_wired`); pairs with manual `CompilesClaim` falsification in `infer_bounded_lattice_completeness_anchor.dag` (no new census literal). **Dissolution:** remove when `target_model.dag` realization surfaces are exercised only by `.dag` `TestClaim` rows / a generated harness / merged M2 multi-module lowering without this host `parse_for_test` structural ratchet. **Interim ratchet:** `v4_std_target_realization_dag_tokenizes_and_parses`; `v4_std_target_realization_declares_target_atom_realization_carrier`; `v4_std_target_realization_declares_catalog_lookup`; `v4_translate_dag_imports_target_atom_realization_consumer`; `v4_rust_language_model_declares_target_atom_realization_rows`; `v4_std_target_model_declares_target_collection_realization_carrier`; `v4_translate_dag_imports_collection_realization_consumer`; `v4_bounded_lattice_completeness_and_infer_gate_are_wired` — tokenize/parse pinned `.dag` sources, assert SG-1 atom-realization + SG-5 collection carrier/coproducts + translate collection consumer + SG-6 completeness import/gate symbols. | | `src/v3/compiler/tests/integration/file_attachment_substrate_carrier_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#62** `substrate_gap_file_ingestion_closed` (T-Workflow-As-Data substrate-gap class; worker brief `docs/briefs/r3-substrate-gate-62-file-attachment-carrier-worker.md`). **Dissolution:** remove when a `.dag` `TestClaim` / PB-B-1 runner receipt can assert `FileAttachment` field names + cross-module nominal wiring against `generated_full_bootstrap_dag()` without this hand-Rust structural ratchet (same dissolution posture as `timing_lens_substrate_carrier_test.rs` for gate #55). **Interim ratchet:** `file_attachment_shape_locked` + `file_attachment_field_types_locked` + `file_attachment_field_count_is_five` pin the ratified Refined-B-1 five-field subset of `WorkflowObservationAnchor` (`NodeId`, `ContentHash`, `WorkflowProducerId`, `WorkflowRunId`, `Nanoseconds`) exactly as declared in `src/v3/std/timing_lens.dag`; existence proof carrier construction stays in-module as `gate_62_file_attachment_demo_record`. | | `src/v3/compiler/tests/integration/lens_application_substrate_carrier_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#89** `section_ref_substrate_landed` (T-Lens-Application-Surface — `SectionRef` disjoint sum over `DeclarationScope` and `NodeScope` in `src/v3/std/lens_application.dag`; design authority `docs/design-lens-application-surface.md` §1.2–§2). **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 harness. **Dissolution:** remove when a `.dag` `TestClaim` / PB-B-1 runner receipt can assert `SectionRef` variant labels, field names, and `DeclarationId` / `NodeId` nominal wiring against `generated_full_bootstrap_dag()` without this hand-Rust structural ratchet (same dissolution posture as gate **#62** `file_attachment_substrate_carrier_test.rs`). **Interim ratchet:** `gate_89_section_ref_is_disjoint_sum_from_lens_application_authority` pins variant order (`DeclarationScope` then `NodeScope`) and payload fields to `lens_application.dag`. | | `src/v3/compiler/tests/integration/workflow_substrate_carriers_test.rs` | **R3 program plan:** `docs/r3-program-plan.md` §1.8 gate **#53** `workflow_substrate_carriers_landed` (T-Workflow-As-Data Slice 1; worker brief `docs/briefs/r3-substrate-t-workflow-as-data-slice-1-worker.md`). **Dissolution:** remove when a `.dag` `TestClaim` / PB-B-1 runner receipt can assert `WorkflowSecret`, `SecretScope`, `CronSchedule`, and `CronField` structural shape against `generated_full_bootstrap_dag()` without this hand-Rust ratchet. **Interim ratchet:** `workflow_secret_shape_locked` + `secret_scope_variants_locked` + `cron_schedule_shape_locked` + `cron_field_variants_locked` pin the Slice 1 β-ratified carriers (STOP+PING discipline on `CronSchedule` field-count drift >5 per brief). | diff --git a/scripts/ci-merge/sg0-pr-body-append.4121.txt b/scripts/ci-merge/sg0-pr-body-append.4121.txt new file mode 100644 index 00000000000..e02df632bfa --- /dev/null +++ b/scripts/ci-merge/sg0-pr-body-append.4121.txt @@ -0,0 +1,2 @@ + +SG-0 pairing: (c) Net +0 on `EXPECTED_HAND_AUTHORED_TEST` — same-path expansion of `v4_std_target_realization_dag_smoke_test.rs` (INVARIANTS §P5(b) parse/tokenize receipt for SG-5 `TargetCollectionRealization` + `06_translate` collection consumer + SG-6 `bounded_lattice_completeness` / `04_infer` gate wiring; substrate on `main` #3957 / #4085). Deferral: `_internal/ROADMAP_OPS.md` § **Nine lanes** row **T-PB-B** / `pb_rust_tests_outside_residual_zero`; dissolve when collection/BL surfaces execute from `.dag` `TestClaim` / T-22 eval only — gunb-ai/gunbc#4121. diff --git a/src/v3/compiler/tests/integration/sg0_census_test.rs b/src/v3/compiler/tests/integration/sg0_census_test.rs index f3bdbc9768e..5776f7b2b5b 100644 --- a/src/v3/compiler/tests/integration/sg0_census_test.rs +++ b/src/v3/compiler/tests/integration/sg0_census_test.rs @@ -944,7 +944,8 @@ const EXPECTED_HAND_AUTHORED_TEST: &[&str] = &[ // T-33: parse ratchet on `src/v4/std/model_core.dag` — Ratified Q1 ModelCore carrier. // SG-0 + INVARIANTS §P5(b) receipt — row `v4_std_model_core_dag_smoke_test.rs` in INVARIANTS.md. "src/v3/compiler/tests/integration/v4_std_model_core_dag_smoke_test.rs", - // SG-0 + INVARIANTS §P5(b) receipt — row `v4_std_target_realization_dag_smoke_test.rs` in INVARIANTS.md. + // SG-0 + INVARIANTS §P5(b) receipt — row `v4_std_target_realization_dag_smoke_test.rs` in INVARIANTS_OPS.md. + // PR #4121 (+0 paths): same-file SG-5/SG-6 smoke expansion per collection-bounded-lattice worksheet §6. "src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs", // T-15: bin/main.dag execution + bootstrap fixpt stage1==stage2 harness (`t_15_self_host_fixed_point`). "src/v3/compiler/tests/integration/v4_t15_self_host_fixed_point_harness_test.rs", diff --git a/src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs b/src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs index 31665c74d85..29002fc0d35 100644 --- a/src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs +++ b/src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs @@ -1,8 +1,14 @@ //! **Layer:** integration //! -//! SG-1 receipt: `src/v4/std/target_model.dag` — `TargetAtomRealization` canonical -//! carrier home (Option A per design-target-realization-canonical-home.md); Rust rows in -//! `extdeps/languages/rust.dag`; `06_translate.dag` consumer. +//! **PR receipt (P5 Mechanism (b)):** this harness + matching `EXPECTED_HAND_AUTHORED_TEST` +//! line in `sg0_census_test.rs` + `_internal/INVARIANTS_OPS.md` row land in the same PR. +//! **This PR (+0 SG-0 paths):** same-file expansion for SG-5/SG-6 collection-bounded-lattice +//! worksheet closure (substrate on `main` #3957 / #4085) — three additional parse/tokenize +//! smokes only; no new hand-Rust logic beyond `parse_for_test` surface checks. +//! +//! SG-1 + SG-5/SG-6 receipt: `src/v4/std/target_model.dag` — `TargetAtomRealization` and +//! `TargetCollectionRealization` carriers; `bounded_lattice_completeness.dag` + `04_infer` gate; +//! Rust rows in `extdeps/languages/rust.dag`; `06_translate.dag` consumers. use v3_compiler::parse_for_test; use v3_compiler::parse_surface::{SurfaceField, SurfaceItem, SurfaceType}; @@ -305,6 +311,9 @@ fn v4_rust_language_model_declares_target_atom_realization_rows() { ); } +// P5 receipt: same-path smoke expansion (SG-5 collection-bounded-lattice worksheet §6). +// Asserts `.dag` surface shape only — substrate edits landed #3957 / #4085 on `main`. +// Deferral: retired when `.dag` `TestClaim` / T-22 eval covers same facts (T-PB-B). #[test] fn v4_std_target_model_declares_target_collection_realization_carrier() { let module = parse_module(TARGET_MODEL_DAG, TARGET_MODEL_PATH);