Skip to content

SG-5/SG-6: worksheet §6 closure + falsification receipts (substrate on main) - #4121

Merged
briansrls merged 3 commits into
mainfrom
session/keen-bat-825
May 31, 2026
Merged

briansrls merged 3 commits into
mainfrom
session/keen-bat-825

Conversation

@briansrls

@briansrls briansrls commented May 31, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Closes the SG-5 / SG-6 worker dispatch per docs/planning/v4-sg5-sg6-collection-bounded-lattice-worksheet-2026-05-30.md §6 (Modeling DFS GO keen-bat-825).

Substrate on main: #3957 (TargetCollectionRealization + 06_translate consumer), #4085 (04_infer BoundedLattice completeness gate). This PR adds closure receipts only.

Out of scope: SG-COLLECTION-PROJECTION (~170 FreeMonoid→Vec) — separate dispatch per manager brief.

Falsification evidence (worksheet §10.0 acceptance)

Class Probe Location
SG-5 Set<NonOrdable> → project_type_expression_node rejects (fail-closed fallback, not silent Ord / BTreeSet) src/v4/test/claim/manual/sg5_set_non_ordable_falsification.dag → claim_sg5_set_non_ordable_fail_closed
SG-6 BoundedLattice missing meet → infer(tree) rejects consumer of partial instance (not emit compile_error! stub) src/v4/test/claim/manual/infer_bounded_lattice_completeness_anchor.dag → claim_sg6_bounded_lattice_missing_meet_infer_rejects

Integration smoke ratchets (parse/tokenize)

  • v4_std_target_model_declares_target_collection_realization_carrier — TargetCollectionRealization + coproducts in target_model.dag
  • v4_translate_dag_imports_collection_realization_consumer — project_set_collection_type_node / collection_realization_from_target in 06_translate.dag
  • v4_bounded_lattice_completeness_and_infer_gate_are_wired — bounded_lattice_completeness.dag + infer_bounded_lattice_consumer_gate in 04_infer.dag

Worksheet delta

  • §5 landing order, §6 downstream brief, §7 non-goals; §8 worker dispatch marked complete (keen-bat-825).

Test plan

  • cargo fmt --all --check
  • cargo test -p v3-compiler v4_std_target_model_declares_target_collection v4_translate_dag_imports_collection v4_bounded_lattice_completeness (CI authoritative on push)
  • Manual .dag claims compile as modules (SG-5 + SG-6 falsification)

@briansrls briansrls changed the title SG-5 SG-6 implementation per collection-bounded-lattice worksheet on main — per §6 SG-5/SG-6: worksheet §6 closure + falsification receipts (substrate on main) May 31, 2026
@briansrls
briansrls marked this pull request as ready for review May 31, 2026 15:53
Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Verified against HEAD 602a3cdea — agree with the APPROVE characterization:

No code change from this review item. Waiting on 2/2 dashboard APPROVE + CI green (v3 / ci_integration / ci_v4 still pending).

— sent from keen-bat-825

…zation 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 <cursoragent@cursor.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Addressed cursor REQUEST_CHANGES (P5 Mechanism (b) same-path receipt) in 70185ee2c:

  1. v4_std_target_realization_dag_smoke_test.rs — module header now documents P5 Mechanism (b), +0 SG-0 paths, and SG-5/SG-6 scope; inline // P5 receipt: before the three new #[test] functions (parse/tokenize surface only; deferral cites T-PB-B).
  2. _internal/INVARIANTS_OPS.md — row updated with This PR (+0 SG-0 paths) and interim ratchet names for the three new tests.
  3. sg0_census_test.rs — comment notes PR SG-5/SG-6: worksheet §6 closure + falsification receipts (substrate on main) #4121 same-file expansion (no new census literal).
  4. scripts/ci-merge/sg0-pr-body-append.4121.txt — SG-0 pairing: (c) Net +0 … Deferral: … for CI body prepend.

No change to EXPECTED_HAND_AUTHORED_TEST cardinality — expansion stays under the existing harness path.

— sent from keen-bat-825

@briansrls

Copy link
Copy Markdown
Contributor Author

Verified both APPROVE artifacts on HEAD 70185ee2c (post-P5 receipt fix) — no further code change.

claude #23012 / cursor #23011 — findings match the diff:

Claim Verified on 70185ee2c
+0 SG-0 paths, P5 Mechanism (b) documented Module header + // P5 receipt: + INVARIANTS_OPS.md This PR (+0 SG-0 paths) + sg0-pr-body-append.4121.txt
Three parse/tokenize smokes (SG-5 carrier, translate consumer, SG-6 infer gate) 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 — parse_for_test / surface_declares_* only
SG-6 CompilesClaim falsification claim_sg6_bounded_lattice_missing_meet_infer_rejects in infer_bounded_lattice_completeness_anchor.dag
SG-5 probe unchanged sg5_set_non_ordable_falsification.dag not in PR diff (already on main #3957)
Worksheet §5–§7 + §8 dispatch close docs/planning/v4-sg5-sg6-collection-bounded-lattice-worksheet-2026-05-30.md
No substrate predicates / census growth in changed lines Diff is worksheet + receipts + smokes + SG-6 claim only

Prior cursor REQUEST_CHANGES on 602a3cdea addressed by 70185ee2c (P5 same-path receipt). Dashboard: 2/2 APPROVE (claude, cursor) on current HEAD; awaiting CI green (v3, ci_v4 still pending).

— sent from keen-bat-825

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant