std/ algebraic structure consolidation (AI-1–AI-12)

[briansrls]

Summary

Seven algebraic structure fixes to src/v4/std/*.dag — eliminates duplicate type authorities (M2), grounds append helpers in the canonical FreeMonoid algebra, and extracts reusable combinators that were previously hand-rolled across compiler files.

• AI-1: Remove bodiless type StageDiagnosticPolicy dual authority from pipeline.dag; import canonical from diagnostic.dag, fix data values to proper record constructors (StageDiagnosticPolicy { accumulation: Accumulate/ShortCircuit })
• AI-3: Remove duplicate fn non_empty<T> from collection.dag (canonical authority is algebra.dag:133); all three callers updated in this PR (05_eval.dag, testgen.dag, refinement_nonempty_list.dag)
• AI-8: Add sequence_outcome<T> to diagnostic.dag; respects StageDiagnosticPolicy (ShortCircuit / Accumulate). traverse_outcome was removed — v2 bootstrap rejects fn(T) -> Outcome<U> in higher-order parameter types (Ratified Q4, same constraint as pre-existing fn(Node) -> Outcome<R> deferral). A Q4 lifting work item is required before traverse_outcome can land. Compiler-side AI-8 migrations (5 files) will use sequence_outcome with a map-first pattern.
• AI-9: Fix non_empty_diagnostics_append to use list_append instead of hand-rolled fold; grounds in FreeMonoid algebra
• AI-10: New src/v4/std/verdict.dag — Verdict<T> bounded lattice (Pass < Deferred < Fail), verdict_combine, verdict_monoid<T>() -> Monoid<Verdict<T>> (P1 substrate inhabitant), verdict_fold; extracted from compiler/05_eval.dag per M2 single-authority rule. BoundedLattice top not instantiable for general T (Fail carries actual: Outcome<T> payload) — documented in header.
• AI-11: Replace three hand-rolled fold/list_push append helpers in dependency.dag (append_dependency_views, append_nodes, append_readiness_layers) with list_append calls
• AI-12: Add bag_eq<T> multiset equality to algebra.dag; diagnostic.dag diagnostic_tail_eq now delegates to it. Placed in algebra (not collection) to avoid the collection→diagnostic circular import

P2 consolidation: list_append / list_snoc_item

algebra.dag is the canonical authority. collection.dag cannot be the authority because collection.dag imports diagnostic.dag, and diagnostic.dag needs list_append — keeping it in collection would be circular. All 12 callers (verification.dag, 06_translate.dag, edit_locus.dag, 9 extdeps language files) now import from v4.std.algebra.

Coordination

deep-bear-704 (compiler/):

• AI-3: 05_eval.dag import fixed in this PR (bf9b958) — may conflict with deep-bear-704's b29268d; they will absorb or drop their fix after std/ algebraic structure consolidation (AI-1–AI-12) #3598 merges
• AI-8: Migrate 5 compiler files to sequence_outcome (map-then-sequence pattern for traverse cases)
• AI-10: Import Verdict, verdict_fold from v4.std.verdict, delete local definitions in 05_eval.dag

tidy-otter-274 (lens/):

• AI-3: testgen.dag import fixed in this PR (bf9b958)
• AI-12: Rescan lens/workflow for bag_eq delegation candidates (bootstrap.dag bs_list_eq flagged)

Test plan

• v4 bootstrap viability passes (CI gate)
• pipeline.dag data constants produce correct StageDiagnosticPolicy record values
• verdict_combine laws: Pass identity, Fail absorb, Deferred sticky/promotable
• bag_eq order-insensitive: [a,b] equals [b,a] under symmetric eq

[briansrls]

Addressed both blocking findings:

Finding 1 — non_empty callers (3 files):

• src/v4/test/claim/manual/refinement_nonempty_list.dag — fixed in commit 19d2592. Import updated to v4.std.algebra { non_empty }.
• src/v4/compiler/05_eval.dag — out of scope for this PR (owned by deep-bear-704). Notified; they have confirmed the fix and will land it as a follow-on after this merges. Merge sequencing is the operator's call.
• src/v4/lens/testgen.dag — out of scope for this PR (owned by tidy-otter-274). Notified; they have confirmed the fix and will land it in a follow-on PR.

The scope constraint for this work item was src/v4/std/*.dag and explicitly excluded compiler/ and lens/. Both sibling sessions are aware and unblocked.

Finding 2 — Verdict<T> parallel authority (verdict.dag vs 05_eval.dag):

This is a real coordination gap. verdict.dag is the new single authority; 05_eval.dag still has its own local type Verdict<T> + aggregate_verdicts that predates this PR. The dissolution (import from v4.std.verdict, delete local defs) is compiler/ work owned by deep-bear-704, who has acknowledged it as an AI-10 follow-on after this merges.

The PR's verdict.dag:6 status comment ("moves Pass/Fail/Deferred algebra out of 05_eval.dag") describes the intent, not a completed dissolution — the compiler-side half is coordinated, not unilateral. The two type definitions are identical in shape so there is no semantic drift risk in the interim window between this merge and the follow-on.

If the policy requires the dissolution to be atomic with the declaration, the right fix is to include the 05_eval.dag changes here — but that crosses the scope boundary. Flagging for operator/reviewer decision.

— sent from valiant-lark-728

[briansrls]

Finding confirmed and fixed in commit 696999f.

What was wrong: verdict.dag described (Verdict<T>, verdict_combine, Pass) as a Monoid only in the header comment — no Monoid<Verdict<T>> inhabitant was declared, so the algebra was a prose claim rather than a substrate fact consumers can read.

Fix: Added verdict_monoid<T>() -> Monoid<Verdict<T>> following the nat.dag:57 pattern (Magma → Semigroup → Monoid nesting, op = verdict_combine, identity = Pass). Declared as a fn rather than data because Verdict<T> is polymorphic — data constants cannot carry free type variables.

BoundedLattice: Updated the header comment to explain why a full BoundedLattice<Verdict<T>> inhabitant cannot be expressed: Fail { actual: Outcome<T> } carries a T-dependent payload, so there is no payload-free top for general T. The ordering (Pass < Deferred < Fail) is structurally sound; the bounded-lattice top constraint is deferred to call sites that have a concrete T. The existing verdict_combine claim ("Fail absorbs") still correctly documents the join semilattice behavior.

— sent from valiant-lark-728

[briansrls]

Finding confirmed and fixed in commit 6e0bb04.

What was wrong: algebra.dag and collection.dag both defined list_append and list_snoc_item as independent function bodies (different implementations — algebra uses fold_list_right, collection uses direct structural recursion). Two independent bodies that can diverge is a P2 violation.

Why algebra.dag must be the authority: collection.dag imports diagnostic.dag (for Diagnostic, port_locus, etc. used by map_absent_diagnostic). If diagnostic.dag imported list_append from collection.dag, the result is a cycle: collection → diagnostic → collection. The algebra copies are structurally necessary.

Fix:

• Removed list_append and list_snoc_item function bodies from collection.dag; updated its Owns header and added a migration note explaining the circular dependency rationale
• Migrated all 12 callers to import v4.std.algebra { ..., list_append, list_snoc_item } (merged into each file's existing algebra import): verification.dag, 06_translate.dag, edit_locus.dag, and all 9 extdeps language files (wasm, lean, go, cpp, typescript, java, kotlin, swift, rust)

No remaining v4.std.collection imports of these functions.

— sent from valiant-lark-728

[briansrls]

Finding confirmed and fixed in commit 42afb09.

What was wrong: verdict.dag declared Verdict<T> as the new authority, but 05_eval.dag:125 still had an identical independent type Verdict<T> definition — two separately-declared bodies that could drift, which is the exact P2 single-authority violation.

Fix:

• Removed type Verdict<T> = Pass | Fail | Deferred from 05_eval.dag
• Added import v4.std.verdict { Verdict, verdict_fold } to 05_eval.dag
• Replaced the hand-rolled aggregate_verdicts fold body with verdict_fold(rs:, empty_verdict:) — the aggregate_verdicts wrapper is retained because it supplies the at: Node parameter for the empty-case eval_empty_verdict_list diagnostic, which is call-site policy rather than algebra
• Removed the now-unused non_empty import (was only called inside the old aggregate_verdicts body)
• Updated 05_eval.dag header: Verdict removed from Owns, v4.std.verdict added to Consumes

v4.std.verdict is now the single authority for Verdict<T>, verdict_combine, verdict_monoid, and verdict_fold.

— sent from valiant-lark-728

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 42afb096 · Trigger: schedule
• Thinking: 509s wall

---

BLOCKING (1)

Root Cause

• src/v4/std/diagnostic.dag sequence_outcome uses Outcome<List> itself as the fold accumulator, so Rejected has no place to carry later Accepted diagnostics → use a dedicated accumulator or merge later Accepted diagnostics into the rejected diagnostic set before finalizing.

⚠️ Fix the accumulating diagnostic loss in the new sequence_outcome primitive.

[briansrls]

BLOCKING: In Accumulate mode, once the fold has seen a Rejected outcome, this branch drops diagnostics carried by later Accepted outcomes, so diagnostic facts stop flowing forward (modeling-discipline facts-flow-forward/P2).

[briansrls]

Finding confirmed and fixed in commit 48473cc.

What was wrong: In Accumulate mode, when acc = Rejected { diagnostics: ra } and o = Accepted { value: _, diagnostics: od }, line 244 had diagnostics: _ — silently discarding od. Any warnings or info diagnostics attached to accepted items after the first rejection were dropped, violating the facts-flow-forward discipline.

Fix: Changed to Accepted { value: _, diagnostics: od } => Rejected { diagnostics: rejected_with_pending(pending: od, rejected: ra) }. This merges od into the accumulated rejection using the same rejected_with_pending helper already used for the Accepted→Rejected transition, preserving all diagnostic facts throughout the fold.

— sent from valiant-lark-728

[briansrls]

Codex finding (id:17094, sha:42afb096) addressed in commit 48473cc.

The diagnostic loss in sequence_outcome Accumulate mode was confirmed and fixed: line 244 now uses rejected_with_pending(pending: od, rejected: ra) to merge the Accepted outcome's diagnostics into the running rejection instead of discarding them. See the preceding comment for full details.

— sent from valiant-lark-728