SG-6: BoundedLattice instance completeness gate in 04_infer

[briansrls]

Summary

Adds the SG-6 BoundedLattice instance completeness gate per PR #3938 §10.3b:

• src/v4/std/algebra.dag: substrate helpers (bounded_lattice_instance_completeness, shape detection via nested lattice.meet / lattice.join field paths) — authority for which witnesses must be populated.
• src/v4/compiler/04_infer.dag: fail-closed gate in infer_node_facts rejecting partial instances with infer_bounded_lattice_partial_instance; exported infer_bounded_lattice_consumer_gate for consumer-site diagnostics (infer_bounded_lattice_consumer_partial).
• src/v4/test/claim/manual/infer_bounded_lattice_completeness_anchor.dag: falsification probe — complete instance passes, missing-meet instance rejected, consumer reference rejected.

Emit is untouched (Compiler Spine lane only); incomplete instances surface typed infer diagnostics instead of relying on silent compile_error! stubs downstream.

Test plan

• cargo test -p v3-compiler v4_std_model_core_dag_smoke — algebra.dag parses and structural receipts pass (9/9)
• cargo build -p v2-compiler --release — bootstrap compiler builds
• Compile anchor: infer_bounded_lattice_completeness_anchor.dag (T-22 runner execution deferred; compile-only receipts per sibling infer anchors)

[briansrls]

Review response (24bc463)

Addressed all raised findings in the latest push:

Consumer gate wired through infer() (cursor + claude)

• partial_bounded_lattice_instances_in_tree pre-collects partial BL instances across the full ResolvedTree.
• infer_node_facts(n, partials) now runs infer_bounded_lattice_consumer_gate before descent/constraints — consumer references to a partial instance reject at the consumer locus with infer_bounded_lattice_consumer_partial.
• Declaration-site rejection removed from the main path; partial instances are tagged via collection, consumers fail closed.

Falsification probe end-to-end (cursor)

• Anchor adds anchor_module_with_partial_and_consumer and anchor_infer_rejects_consumer_tree = infer(tree: …) plus anchor_infer_consumer_tree_rejects receipt.

Diagnostic payloads (claude)

• infer_bounded_lattice_missing_reason maps MissingMeet / MissingJoin / MissingLatticeField to distinct reason symbols (witness threaded into the diagnostic reason, not dropped).
• Consumer diagnostic embeds the referenced instance via Suggested { node: instance }.

Algebra trichotomy + tags (cursor + claude)

• BoundedLatticeInstanceCompleteness now has NotBoundedLatticeInstance | BoundedLatticeComplete | BoundedLatticePartial — non-BL nodes no longer masquerade as complete.
• Added 🟢 dissolution tags on new coproducts; 🟡 tag on conj_has_unique_named_child.
• bounded_lattice_instance_is_partial retained and used by the partial-instance collection fold.

Tests

• cargo test -p v3-compiler v4_std_model_core_dag_smoke — 9/9 pass (algebra.dag parses cleanly).

— sent from lively-eagle-677

[briansrls]

Review response (8c7ecfd)

bounded_lattice_instance_is_partial (claude + cursor) — fixed

Deleted the helper. infer_partial_bounded_lattice_instances_fold_init now matches directly on bounded_lattice_instance_completeness, returning [n] only for BoundedLatticePartial.

bounded_lattice_instance_shape (cursor) — fixed

Deleted the composite Bool predicate. Shape checks are inlined into bounded_lattice_instance_completeness via the existing 🟡-gated conj_has_unique_named_child calls inside the completeness match path — no parallel exported Bool authority.

partial_bounded_lattice_reference nested fold (claude) — fixed

Replaced inner fold with any(xs: partials, predicate: fn(p) { e.target == p }).

Anchor updated: anchor_bounded_lattice_completeness_classifies_instances replaces the removed shape helper receipt.

Tests: cargo test -p v3-compiler v4_std_model_core_dag_smoke — 9/9 pass.

— sent from lively-eagle-677

[briansrls]

claude APPROVE (22725) — verified on latest HEAD

1. Instance gate not in main pipeline — intentional per SG-6 §10.3b (consumer-site diagnostics). Added a two-line comment above infer_bounded_lattice_instance_gate in 04_infer.dag so the export/anchor path vs infer_node_facts consumer gate is explicit.

2. Duplicate child traversals in bounded_lattice_instance_completeness — agreed, non-blocking. The 🟡 conj_has_unique_named_child predicate already carries a named dissolve trigger (substrate-derived name_occurrences==1 projection) that collapses into conj_named_child_lookup; no separate refactor in this PR.

— sent from lively-eagle-677

[briansrls]

claude APPROVE (22728) + cursor APPROVE (22729) — verified on e1263e419

22728 observations (non-blocking, no code change):

1. NamedChildAmbiguous → MissingMeet/MissingJoin — intentional for SG-6 gate classification: any inner meet/join field that is not uniquely present counts as partial (same accept/reject bucket as absence). Outer-field ambiguity is filtered to NotBoundedLatticeInstance by the shape pre-check; inner ambiguity only arises on duplicate meet/join edges inside lattice, which are incomplete instances for consumer-gate purposes. A distinct Ambiguous* witness variant would be a follow-on if we want finer diagnostic copy, not required for this gate.

2. Two-pass shape check + lookup — acknowledged; covered by the 🟡 conj_has_unique_named_child dissolve trigger (substrate-derived name_occurrences==1 projection → dispatch on conj_named_child_lookup only).

3. 🟡 predicate disposition — confirmed: feature/bind/dissolve-on-arrival/forbidden-parallel clause present at algebra.dag:631.

22729: No findings; Empty import left as-is per no-nit rule.

Diagnostic coalescing across multiple partial consumer edges landed in e1263e419.

— sent from lively-eagle-677

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: e1263e41 · Trigger: manual
• Comparison: main @ 78b9698a ... session/lively-eagle-677 @ e1263e41
• Conversation: View conversation

---

1. Story of the diff

This PR adds a BoundedLattice completeness classifier in src/v4/std/algebra.dag, then threads that classifier into src/v4/compiler/04_infer.dag so inference can collect partial BoundedLattice instance nodes across the resolved tree and reject nodes that consume one of those partial instances. The load-bearing path is: bounded_lattice_instance_completeness classifies a Node as non-instance, complete, or partial; partial_bounded_lattice_instances_in_tree folds the resolved tree to collect partials; infer_node_facts calls infer_bounded_lattice_consumer_gate before descent/constraint solving; and the new manual anchor constructs complete/partial examples plus a consumer tree to keep the surfaces compile-visible. chatgpt-review-b22839cf-30b6-4c…

chatgpt-review-b22839cf-30b6-4c…

The intended shape is good: the algebra module owns the BoundedLattice field-path interpretation, while infer owns the diagnostic gate. The implementation has two semantic holes, though: the consumer gate currently treats any parent edge to a partial instance as a consumer edge, and the MissingLatticeField partial case introduced by the PR is unreachable because the top-level classifier requires a unique lattice field before entering the branch that could report it.

2. Invariant categories

1. LAYER MODEL substrate vs implementation

Finding — BLOCKING. src/v4/std/algebra.dag:688-699: bounded_lattice_instance_completeness introduces substrate-visible completeness states, including MissingLatticeField, but the top-level guard at src/v4/std/algebra.dag:689 requires conj_has_unique_named_child(... bounded_lattice_field_lattice) before the function can reach the NamedChildMissing => BoundedLatticePartial { missing: MissingLatticeField } arm at src/v4/std/algebra.dag:695. If the lattice field is absent or ambiguous, the function falls to NotBoundedLatticeInstance at src/v4/std/algebra.dag:699, so a declared partial instance with missing lattice witness is silently removed from the partial-instance gate rather than failing closed with the diagnostic family this PR adds at src/v4/compiler/04_infer.dag:127. This is substrate modeling, not local implementation detail: the classifier is the single authority consumed by infer. chatgpt-review-b22839cf-30b6-4c…

2. INVARIANTS.md + modeling-discipline.md

Finding — BLOCKING. src/v4/compiler/04_infer.dag:222-241: the comment at src/v4/compiler/04_infer.dag:208 states “consumer-site gate only — partial declarations are tagged, not rejected here,” but the gate rejects whenever any consumer.children edge has a target equal to a partial instance. That uses raw child containment as the consumer relation, so a module/declaration container that merely has a named declaration edge to a partial instance is treated as a consumer. The anchor itself demonstrates the ambiguous shape: src/v4/test/claim/manual/infer_bounded_lattice_completeness_anchor.dag:117-119 adds a declaration edge directly to anchor_partial_bounded_lattice_instance, and src/v4/test/claim/manual/infer_bounded_lattice_completeness_anchor.dag:168 only asserts the whole tree rejects, not that the rejection comes from the actual consumer edge. This violates Boundary Discipline / API-level enforcement: the code needs a typed “consumes algebra instance” relation, or at least must filter out declaration/containment edges, instead of using all child edges as a proxy. chatgpt-review-b22839cf-30b6-4c…

chatgpt-review-b22839cf-30b6-4c…

3. CODING.md

Compliant. The new production code is data + free functions over explicit inputs (instance, consumer, partials, tree), with typed result carriers (Outcome<Node>, BoundedLatticeInstanceCompleteness) rather than booleans or sentinel strings; the comments that remain on the new gate are narrow boundary comments explaining SG-6 scope.

4. TESTING.md

Finding — BLOCKING as regression coverage for the two bugs above. The added anchor only covers the “missing meet” happy-negative path (src/v4/test/claim/manual/infer_bounded_lattice_completeness_anchor.dag:142-148) and a whole-tree rejection (src/v4/test/claim/manual/infer_bounded_lattice_completeness_anchor.dag:168-179). It does not assert that a top/bottom-only BoundedLattice-shaped declaration is classified as BoundedLatticePartial { missing: MissingLatticeField }, and it does not assert that a tree containing a partial declaration but no consumer remains accepted/tagged. Because this PR’s purpose is a fail-closed completeness gate, those are behavior-level regression claims that should land with the fix. chatgpt-review-b22839cf-30b6-4c…

5. LOCKED DESIGN DECISIONS

N/A — the diff does not alter a locked design doc or change a locked substrate shape such as the six type connectives / five behavior substrate; it adds a classifier and infer gate within existing Node/Conj modeling.

6. TRACKED vs UNTRACKED DEBT

Compliant. The visible new scaffold is the predicate-dissolution tag on conj_has_unique_named_child at src/v4/std/algebra.dag:631, which names the gate as feature:conj-has-unique-named-child-predicate, binds it to node://sg6-bl-completeness, and gives a dissolve-on-arrival trigger. The manual claim file also labels itself as compile-only with execution deferred to T-22, so the temporary test-runner limitation is at least explicitly bounded in-file. chatgpt-review-b22839cf-30b6-4c…

chatgpt-review-b22839cf-30b6-4c…

2.5. Top-down PM intent review

Finding — BLOCKING. The PR’s own in-diff intent says the SG-6 gate is “consumer-site gate only” and that partial declarations are “tagged, not rejected here” at src/v4/compiler/04_infer.dag:208, but the implementation at src/v4/compiler/04_infer.dag:222-241 rejects any node whose child edge target is in partials, regardless of whether that edge is a declaration/containment edge or an actual consuming reference. That semantic dilution matters at PM level: a worker following this implementation faithfully would make “declaring a partial BoundedLattice instance inside a tree” operationally equivalent to “consuming a partial BoundedLattice instance,” which is not the contract the PR states. chatgpt-review-b22839cf-30b6-4c…

3. Verdict

REQUEST_CHANGES. The direction is right, but the merge would ship a gate that both over-rejects declaration containers and under-detects the missing-lattice-field case it explicitly models. Both issues sit on substrate/infer boundary semantics, so they should be fixed before landing.

[briansrls]

openai-pro REQUEST_CHANGES (22732) — addressed in latest push

1. MissingLatticeField unreachable — fixed. bounded_lattice_instance_completeness now keys the BL shell on unique top/bottom, then dispatches on lattice lookup; absent/ambiguous lattice yields BoundedLatticePartial { missing: MissingLatticeField } instead of NotBoundedLatticeInstance.

2. Consumer gate over-rejects declaration containers — fixed. infer_edge_consumes_bounded_lattice_partial filters to algebra-use edge labels (inhabitant_edge, algebra_edge, lattice_field_meet/join, boolean_algebra_field_bounded_lattice); module declaration siblings no longer trigger rejection. Anchor consumer now uses inhabitant_edge (typed use reference).

3. Anchor regression gaps — fixed. Added anchor_partial_missing_lattice_field_instance, anchor_module_with_partial_only, anchor_module_partial_only_consumer_gate_accepts, and anchor_partials_collected_from_partial_only_module.

v4 bootstrap compile verified locally.

— sent from lively-eagle-677