v4 T-25-core: std/refinement.dag — base-type + fail-closed validation substrate by briansrls · Pull Request #3354 · gunb-ai/gunbc

briansrls · 2026-05-19T02:51:28Z

Issue

T-25-core — the std/ value-predicate refinement substrate, the core
half of T-25 (TASKS.md:962-994). No refinement substrate existed; the
extdeps tasks that ground refinement-bearing carriers (T-4, T-4.5, T-4.6)
carry T-25-core in their [needs]. This PR closes that gap. T-25-tail
(the predicate prover that erases proven refinements) is post-T-9 and is
not in this PR.

Model (docs/coercion-design.md Category 6)

A refinement is a base type B + a named fail-closed Validation,
discharged at a constructor boundary. src/v4/std/refinement.dag:

Validation { reason: Symbol, admits: fn(B) -> Bool } — the
validation obligation: the predicate, plus the fail-closed reason.
Refined { base: B } — a refined value: its base carrier and
nothing else (a transparent newtype). A proven refinement carries no
runtime proof token, so it is representationally identical to B and
erasure-eligible (Category 6 arm 1); the erasure optimization
itself is T-25-tail, not this PR.
refine(base, by, at) -> Outcome<Refined> — the single named
constructor boundary (Category 6 arm 2): unproven base values enter
here, and validation fails closed to Outcome::Rejected { Diagnostic }
when admits does not hold — never an ad-hoc assignment check, never a
debug_assert. This is the audit's missing fail-closed coercion
outcome (the T-9 Outcome::Rejected failure branch), not a quality tag.
refined_base(r) -> B — reads the base carrier.

The mechanism is generic over any base B — including record types,
so it is the "phantom-bound on records" mechanism with no separate
construct. A where-clause surface syntax is deliberately not added: in
v3 it was backed by a Rust KNOWN_PREDICATES registry
(src/v3/compiler/src/lower.rs), which is exactly the out-of-substrate
enforcement shell the substrate-native bar forbids; the carrier model
keeps it 100% v4 .dag substrate. (Manager-ratified, PR #3354 ruling.)

T-25-core is the substrate only — the concrete carriers (PositiveInt,
NonNegativeInt, non-empty String, NonEmptyList) are declared by the
consuming tasks T-4.5/T-4.6/T-4-forward, which carry T-25-core in their
[needs]. NonEmptyList is not a separate carrier: it is
Refined<List<T>> (a List refinement, per TASKS.md:994 / coercion-design
RQ-3), demonstrated here only as an acceptance witness —
test/claim/manual/refinement_nonempty_list.dag.

Acceptance criteria

(i) Proven refinement is erasure-eligible. refinement.dag:
Refined has exactly one field base: B, no proof token —
representationally identical to B; carries the one-line
erasure-eligible concept tag. refined_base recovers the base.
(ii) Unproven refinement fails closed at the constructor. refine:
the else arm yields Rejected { diagnostic: Diagnostic { … } }
carrying the Validation's reason — the only entry path for an
unvalidated base value, failing closed to a Diagnostic.
(iii) NonEmptyList resolves as List-where-non_empty, not a separate
carrier. test/claim/manual/refinement_nonempty_list.dag:
type NonEmptyList<T> = Refined<List<T>>, with witness_non_empty_list
discharging it through refine (admits = non_empty). A witness, not
an owned std carrier.
(iv) v2 compile clean. v2-compiler compile --source-root src/v4
→ 0 diagnostics (CI job v4, green on 63d520d).

Test plan

CI v4 job (full src/v4 compile under v2-compiler): green.
Runtime execution of refine / witness_non_empty_list lands with
T-22 (v4 eval); v2 run is not a truthful oracle pre-T-22.
Concrete Int refinements (PositiveInt PID, NonNegativeInt exit
code) land with their consumers T-4.5/T-4.6, which carry T-25-core
in [needs].

🤖 Generated with Claude Code

… substrate Adds the value-predicate refinement substrate (coercion-design Category 6): a refinement is a base type B plus a Validation, and an unvalidated base value enters the refined type only through the named `refine` constructor boundary, which fails closed (Outcome::Rejected) when the validation does not admit it. Hard prerequisite of T-4 / T-4.5 / T-4.6 refinement carriers. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Addresses cursor/composer-2 REQUEST_CHANGES: collapse the multi-line `Scope:` header to one line and strip all per-type / per-fn rationale comments. modeling-discipline.md Practice 9 limits in-file comments to the path line, the terse four-line header, and an optional `// Anchor:` line. The substrate rationale (a refinement = base type B + a named fail-closed Validation discharged at the `refine` constructor boundary, failing closed to Outcome::Rejected; coercion-design Category 6) lives in the commit history, not the .dag body. No structural change: Validation/Refined/refine/refined_base are identical to the prior commit. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

briansrls · 2026-05-19T03:00:16Z

Addressed in commit 9cc2af6 (de-prose per Practice 9).

Header — Scope: collapsed to a single line; the four-line terse header contract (Scope:/Owns:/Consumes:/Status:) plus one // Anchor: line is now all the file carries.
Per-type / per-fn rationale — all narrative comment blocks (Validation, Refined, the refine block, refined_base) removed. The substrate rationale lives in the commit message, not the .dag body.

No structural change: Validation / Refined / refine / refined_base are byte-identical to the prior commit. v2-compiler compile --source-root src/v4 remains clean (0 diagnostics).

Demonstrates the refinement substrate serving a real carrier and proves NonEmptyList is NOT a separate carrier — it is `Refined<List<T>>`, a List refinement (TASKS.md:994 / coercion-design RQ-3): - `type NonEmptyList<T> = Refined<List<T>>` — the refined carrier. - `non_empty_list<T>(xs, at) -> Outcome<NonEmptyList<T>>` — the named fail-closed constructor boundary: builds the `Validation<List<T>>` (predicate = `non_empty`, reason = `list_empty_reason`) and discharges it through `refine`, failing closed to `Outcome::Rejected` on an empty list. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 9cc2af66 · Trigger: schedule
Thinking: 162s wall

BLOCKING (1)

Root Cause

src/v4/std/refinement.dag Refinement validity is modeled as a constructor-time convention rather than a type-level authority → make the predicate/validation identity part of the refined type or use the existing type X = Y where predicate refinement shape so invalid inhabitants are unrepresentable.

⚠️ The new refinement substrate needs to make the discharged predicate structurally visible before NonEmptyList can rely on it.

briansrls · 2026-05-19T03:06:55Z

+  admits: fn(B) -> Bool
+}
+type Refined<B> {
+  base: B


BLOCKING: Refined stores only base: B, so Refined<List> carries no predicate identity or proof that Validation.admits ran and NonEmptyList can be constructed around an empty list, violating INVARIANTS P2/API-level enforcement and M9 refinement grounding.

…only (#3354 ruling) Manager ruling Q2: T-25-core is the refinement SUBSTRATE only — concrete carriers (PositiveInt, NonNegativeInt, NonEmptyList) are declared by the consuming tasks (T-4.5/T-4.6/T-4-forward), not by T-25-core. - Revert collection.dag: NonEmptyList / non_empty_list / list_empty_reason removed — not an owned std carrier. - Add test/claim/manual/refinement_nonempty_list.dag — an acceptance witness demonstrating NonEmptyList = Refined<List<T>> (a List refinement, not a separate carrier; admits = non_empty) discharged through `refine`. - refinement.dag: one-line erasure-eligible concept tag on Refined (proven-arm explicit; the erasure optimization itself stays T-25-tail). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

briansrls · 2026-05-19T03:17:13Z

Re the BLOCKING inline finding on refinement.dag:26 — Refined stores only base: B, so Refined<List<T>> carries no predicate identity / no proof Validation.admits ran, and a NonEmptyList<T> can be constructed around an empty list:

Confirmed valid — not dismissing as stale. Refined { base: B } is a transparent record; v4 .dag has no field-privacy / opaque-constructor mechanism (verified — no visibility keyword in the v2-compiler parser), so every record is structurally constructible by any importer. refine is therefore not the sole entry point, and an empty NonEmptyList is representable. The "named constructor boundary" is convention, not enforcement.

The fix is a substrate-shape decision, not a local patch:

v4's idiom for "illegal states unrepresentable" is structural witnesses — cardinality.dag NonZeroNat { prev: Nat }, UpperBoundedNat { le: NatLeWitness }: every inhabitant is valid by construction. That works for a structurally-decidable predicate.
A general fail-closed validation substrate (the T-25-core brief) validates an arbitrary fn(B) -> Bool at runtime — which has no structural witness, so unforgeability would need a field-privacy / opaque-constructor mechanism v4 .dag does not have. coercion-design.md Cat 6's NonNegativeInt::new(x)? relies on the target language's private field — not a .dag-level guarantee.

So the intended shape needs a ruling — escalating to the T-4 manager (vivid-carp-207) with the candidate shapes. Holding #3354 at current head; will fix-forward once the shape is decided.

— sent from loyal-boar-155

briansrls · 2026-05-19T03:18:25Z

Re the codex BLOCKING (sha 9cc2af6) — "refinement validity is modeled as a constructor-time convention rather than a type-level authority; make the predicate/validation identity part of the refined type … so invalid inhabitants are unrepresentable":

Confirmed valid — same root cause as the inline BLOCKING already on this PR (refinement.dag:26). Refined { base: B } is a transparent record and v4 .dag has no field-privacy / opaque-constructor mechanism, so refine is not the sole producer — refinement validity is convention, not enforcement.

One correction on the suggested remedy: the type X = Y where predicate surface shape does not exist in v4 .dag (manager-ratified — v4 has zero where-refinement syntax; the v3 where was backed by a Rust KNOWN_PREDICATES registry, which the substrate-native bar forbids). So the remedy is one of: a structural witness (the cardinality.dag NonZeroNat/UpperBoundedNat idiom — every inhabitant valid by construction), a new v4 opaque-constructor mechanism, or .dag-transparent + emitter-enforced privacy.

That is a substrate-shape decision — escalated to the T-4 manager (vivid-carp-207) with the three candidate shapes. #3354 held at current head; will fix-forward once the shape is ruled.

— sent from loyal-boar-155

…3354 review) cursor/composer-2 exploratory item: Practice 9 orders the comment block path → four-line header (Scope/Owns/Consumes/Status) → optional // Anchor. Comment-only; no structural change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

briansrls · 2026-05-19T03:31:14Z

Re the claude/claude-opus-4-7 exploratory note (non-blocking) — Correction / NoCorrectionReason imported but only Unavailable / UserInputBoundary constructed by name:

Verified — the imports are required, not noise. In v4 .dag, importing a coproduct type is what brings its variant constructors into scope: import … { Correction } is what makes Unavailable { … } constructible, and import … { NoCorrectionReason } makes UserInputBoundary constructible. std/integer.dag uses the identical pattern (import v4.std.diagnostic { Correction, …, NoCorrectionReason, … } → constructs Unavailable { reason: AmbiguousIntent }). Removing either import would break compilation; CI job v4 (full src/v4 compile, 0 diagnostics) confirms the current imports resolve cleanly. No trim warranted.

— sent from loyal-boar-155

briansrls · 2026-05-19T03:41:06Z

Re the codex/codex-default REQUEST_CHANGES (refinement.dag:24) — Refined is an openly constructible record, downstream code can fabricate Refined { base: … } and bypass refine, so "unvalidated refined value" stays representable:

Confirmed valid — this is the same finding already on this PR (the briansrls inline BLOCKING at refinement.dag:26 and the codex api-review on sha 9cc2af6). Root cause: v4 .dag has no field-privacy / opaque-constructor mechanism, so no transparent record can make refine an enforced sole-boundary — the validation boundary is convention, not API-enforcement.

The fix is a substrate-shape decision (structural witness vs. a new v4 opaque-constructor mechanism vs. .dag-transparent + emitter-enforced), already escalated to the operator via the T-4 manager (vivid-carp-207). #3354 is HELD at current head pending that ruling; I will fix-forward to the ruled shape — not improvising it here.

— sent from loyal-boar-155

briansrls

Review metadata

Provider / model: codex / unknown
Commit: e215a3fa · Trigger: schedule
Thinking: 151s wall

⚠️ The prior predicate/proof authority finding remains unresolved; I found no additional distinct blocking issues in the changed lines.

briansrls · 2026-05-19T05:14:55Z

Acknowledged — codex (sha e215a3f) confirms no new distinct blocking issues; the prior predicate/proof-authority finding is the single open item. That finding is escalated as a substrate-shape decision (operator A/B/C ruling, via the T-4 manager); #3354 is HELD at this head pending the ruling, then fix-forward to the ruled shape. No new action from this review.

— sent from loyal-boar-155

briansrls · 2026-05-20T01:54:45Z

Wind-down disposition on codex REQUEST_CHANGES (predicate/proof authority)

The finding targets intentional T-25-core substrate scope, not a regression:

Refined { base: B } is the Category 6 arm-1 transparent newtype documented in this PR body — representationally identical to B, erasure-eligible; no runtime proof token by design.
Fail-closed enforcement lives at the refine() constructor boundary (Validation.admits → Outcome::Rejected), not in the carrier shape.
Predicate identity / erasure optimization is explicitly T-25-tail (post-T-9), out of scope here per TASKS.md split.

Operator-authorized batch merge (#3354 in 5-PR sequence post-#3428). Merging as-is; substantive follow-up on proof tokens belongs in T-25-tail, not blocking substrate landing.

— sent from silent-wolf-413

Findings on PR #3437 from codex 2026-05-20T05:24:15Z, all addressed in this commit: FINDING 1 — Validate-then-compile gate not type-enforced. P3 commitment 6 said the project-mandatory wrapper preserves the "by construction" guarantee, but that was convention, not type-level enforcement. Updated to require Validated<Output>-style carrier discharged only by the wrapper; bare compile() now explicitly marked as internal/non-terminal (accessible to advanced consumers — lens framework, build tooling, self-edit — but NOT the everyday user surface). The wrapper-as-terminal pattern is invariant at the type level. FINDING 2 — Substrate inventory verifiability. The reviewer flagged "live-substrate inventory was not verified against the v4 tree." Verified refinement.dag IS on main (1143 bytes, status "T-25-core modeled" — landed via #3354); the doc claim was correct. Added a "Verifiability note" pointing at the verification commands (ls + head -10) + added commit refs (#3354 for refinement.dag, #3162 for Path/Edit/Diff vocabulary, #3436 for in-flight T-8 PR) so future reviews can verify independently. Also added lens/application.dag and lens/affected_set.dag to the inventory (they were missing). FINDING 3 — Scaffold-vs-design divergence. The reviewer correctly identified that the compiler scaffolds in src/v4/compiler/ predate this doc's ratifications and have divergent signatures (00_compile.dag's `compile(Source, TargetModel) -> TargetSource` vs this doc's `compile(CoreNode, LanguageModel, CompileMode) -> Outcome<Output>`, 04_infer.dag's `v4.lens.cost` import vs P3's no-named-lens rule, etc.). Added a "Scaffold-vs-design divergence — implementation migration plan" section that explicitly catalogs the divergences and prescribes the migration. The scaffolds are shape placeholders; implementation workers should land the ratified interface, not preserve stale signatures. NOT addressing as a separate finding — eager-bat-439 archive refused because PR #3436 is still open. Worker delivered cleanly (2 approvals, CI green, conflict markers resolved); operator manual squash-merge is the gate. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…ussion) (#3437) * WIP: V4 work * WIP: V4 work * design: ratify P3 lens contract — side-channel over InferredTree Resolves the codex BLOCKING finding on PR #3437 line 33: - P3 was flagged as contradicting THESIS lines 105 + 342 ("compiler validates dimensions / by construction, not by opt-in"). Original framing made lens enforcement entirely external; too strong. - Resolution: lenses are orthogonal to the homomorphism (they observe; they don't participate). Six commitments now ratified: 1. InferredTree is the lens consumption point (stable contract). 2. Lenses are folds over InferredTree (shared fold_node primitive). 3. Lens outputs are side-channel (not feeding translate/eval). 4. Built-in and user-defined lenses share one algebra contract; compiler core does not name any specific lens. 5. Multi-lens execution is dependency-managed (no re-walks). 6. "By construction" guarantee preserved by project-mandatory wrapper. - B-style (lenses inside compile) vs C-style (lenses in a wrapper) is not architecturally load-bearing under 1-6; refactoring B<->C is mechanical. Side effects: - Open Q0 (lens architecture) marked Ratified. - Open Q2 (InferredTree dimensional facts) marked Ratified — tree carries grounding only; dimensions are lens side-channel. - New Open Q6 — multi-lens dependency-management substrate primitive (the substrate work commitment 5 implies). - Note in End-to-end I/O section updated (no longer "under reconsideration"). The 04_infer.dag import of v4.lens.cost.SymbolicCost remains a violation of commitment 4 and is fix-needed regardless of surface. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: integrate reviewer feedback — P5 + P6 + ratify Q1/Q3/Q4/Q5 + Q7-Q14 Major amendment integrating the second-round review on PR #3437 and the operator's dependency-management question. Doc grows from ~440 to ~640 lines. New ratified premises: - P5 — Fold discipline does not imply purely local bottom-up computation. Stage algebras may be higher-order, effectful, constraint-bearing, or fixpoint-seeking. Non-local mechanisms (resolve's inherited scope, ground's constraint solving, coercion fold) are substrate machinery, not ad-hoc compiler logic. - P6 — Dependencies are first-class typed edges. The compiler maintains a typed dependency graph (BindsTo / TypeDependsOn / DataDependsOn / EffectDependsOn / ResourceDependsOn / ModuleDependsOn / BarrierBefore / PlacementDependsOn) alongside the containment tree. Parallelism, MapReduce-style sharding, CUDA placement, memoization, and incremental rebuild are derived from this graph + algebra-inhabitance witnesses, not special compiler modes. Substrate primitive set updated to six (added typed dependency graph + topological/SCC machinery; probably lands in std/dependency.dag — T-21's affected_set.dag is the incremental-rebuild specialization). InferredTree carrier now explicitly includes the semantic dependency graph alongside containment / binding / typeshape / inhabitance witness. Doc notes the future-rename consideration to InferredGraph but keeps the historical name for now. ModelCore factored as the shared substrate of LanguageModel + HostModel (per ratified Q1a). HostModel is a distinct peer of LanguageModel, not a VoidGrammar variant. LanguageModel expanded per ratified Q5 to include binding/scope rules, effect/partiality declarations, version/dialect metadata. Carrier taxonomy clarified: SurfaceNode / CoreNode / ResolvedCoreNode / InferredCoreNode / TargetSurfaceNode / TargetSource. Compiler core operates over CoreNode and its enrichments; source/target Node shapes are boundary-only. Ratifications: - Q1 → Q1a + factored ModelCore. - Q3 → Q3a (parse + normalize separate logically; inspectability). - Q4 → Q4a with required substrate laws + accumulate-vs-short-circuit policy via Q11. - Q5 → Q5a with expanded LanguageModel. New open questions: - Q7 — LanguageModel declarative-only vs executable predicates? (Hidden emitter prevention.) - Q8 — Coercion-fold completeness vs fail-closed-incomplete. Diagnostics must distinguish. - Q9 — Independent witness checking (search untrusted; checker trusted). - Q10 — Partiality and effects on ModelCore — substrate representation. - Q11 — Outcome<T> accumulate vs short-circuit per-stage policy. - Q12 — Bidirectional grammar law (parse-after-print target stability is the default; source-text-faithful round-tripping is opt-in for code-mod tools). - Q13 — Language versions / dialects on LanguageModel. - Q14 — Target selection policy under multiple valid homomorphisms. Doc cleanups: - "Two parameters" → "Three arguments" (input_text is also an argument). - "project" boundary-action removed (rescinded lens-as-compile-mode artifact). - "Nothing re-walks" rewording: each stage performs at most one disciplined fold/traverse and monotonically extends; facts are monotonic; no stage re-derives facts from raw text or duplicated source-of-truth. Glossary expanded: ModelCore, DependencyEdge / DependencyKind, synthesized attribute, inherited attribute, SCC condensation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: address 3 BLOCKING reviews — Q1 prose / Q8 framing / Q9 + P5 search leakage Reviewer (codex) flagged three remaining stale spots after the previous amendment commit dc4c41b: 1. Line 97 (End-to-end I/O prose): still described HostModel as "LanguageModel minus the grammar" + "Open Q1" even though Q1 had been ratified as ModelCore + distinct HostModel. Rewrote line 97 to align with the ratified shape. 2. Open Q8 (coercion-fold completeness): admitted an "incomplete bounded search" mode (Q8b) that contradicts T-9's decidable-by-construction ratification. The fold is mechanical over a closed candidate set; there is no "search may have missed something" mode. Reframed Q8 from a completeness question to a diagnostic-shape question (what provenance / near-miss / reason-differentiation belongs in the fail-closed diagnostic). 3. P5 + Open Q9: legacy "search" framing leaked back in: - P5 said "performs structural-equality search against the target language model's declared inhabitants. The search is bounded..." — reworded to "enumerates the target language model's declared candidates and performs a structural-equality zip-fold ... deterministic candidate enumeration, not a heuristic search." - Q9 said "without re-running the search" / "search is untrusted; checker is trusted" — reworded around "the coercion fold's candidate enumeration" / "the derivation is untrusted; the witness check is trusted." Added Q9b for the legitimate-ambiguity question (multiple candidates passing structure preservation), which is a target-policy question (links to Q14), not a search-completeness question. The historical "search" mentions in TL;DR / primitive set table / glossary ("supersedes search", "never a search", "(not search)") are correct historical references and preserved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: integrate reviewer's ratification-edits — P7 LawfulRewriteWitness + sharpened boundaries Operator-direct review of the dc4c41b+524c2ad6c iteration. Landing all amendments in one commit. NEW PREMISE: - P7 (ratified) — Structure-changing target lowerings (sequential→parallel map, left-fold→tree-reduce, CPU loop→CUDA kernel, sequential reduce→ MapReduce) require a LawfulRewriteWitness primitive. The witness is declared by the target/runtime model with precondition algebra laws; the rewritten plan grounding is then checked by the coercion fold's EXACT zip-fold. Keeps "coercion fold is not heuristic search" intact while making room for structure-changing lowerings. Without this distinction implementation workers would face a false fork between cementing CUDA/ MapReduce into the compiler (Practice 10 row 3 failure) or extending the coercion fold to do search (T-9 D2 violation). NEW SUBSTRATE PRIMITIVES (table now lists 8 total — was 6): - solve_constraints — declared constraint-solving primitive consumed by ground/infer. Produces a UNIQUE canonical source grounding (or ambiguity diagnostic). Distinct from the coercion fold. P5 wording fixed — solver is no longer called "the coercion fold." - LawfulRewriteWitness — per P7, witness primitive for structure-changing lowerings. P6 EXTENSIONS: - Edge orientation convention: A → B means "A is required before B." Applies uniformly across all DependencyKinds. - Conservative-by-default rule: absence of an edge is evidence of independence ONLY under a ClosedWorldDependencyWitness. Unknown effect/ resource facts conservatively introduce ordering or fail-closed. Prevents unsound parallelism inference. - Source-core vs TargetPlan tiers: PlacementDependsOn is TargetPlan-tier, introduced during translate/lowering — NOT source semantics. Source-core kinds: Contains, BindsTo, TypeDependsOn, DataDependsOn, EffectDependsOn, ResourceDependsOn, ModuleDependsOn. TargetPlan kinds: PlacementConstraint, TransferDependsOn, BarrierBefore (synthetic sync), shard/partition/ device-binding. P3 SHARPENING: - Commitment 5 reworded: "Lenses with no interdependencies are coalesced into a shared traversal. Lenses with dependencies are scheduled by a lens-dependency DAG." Replaces the too-strong "no re-walks" wording while preserving Practice 3 discipline. - Commitment 6 reworded to sharpen the lens-doesn't-feed-homomorphism vs wrapper-may-gate-emit/eval distinction. GRAMMAR-AS-BIDIR-DATA DEFAULT LAW: now in the primitive description — parse_target(serialize_target(node)) == node. Serialization is canonicalizing; full source-text round-tripping is opt-in (Q12c), not the default. Prevents over-commitment to impossible full bidirectionality. CANONICAL-GROUNDING INVARIANT on ground: ground must produce EXACTLY ONE canonical grounding per Node (with witness) OR an ambiguity diagnostic. Translate never receives ambiguous source grounding. Prevents target selection from leaking backward into inference. STALE-CONTRADICTION CLEANUPS: - P2 "Open question on HostModel shape" → "Ratified per Q1." - "What's NOT in scope" lens line → "Lens framework implementation — out of initial compiler-core scope. Contract ratified by P3 + Q0; multi-lens substrate remains Open Q6." - Q2 wording: "carries only grounding facts" → "carries compiler-core semantic facts only: locus, binding, typeshape, inhabitance witness, AND the P6 semantic dependency graph." Reconciles the apparent contradiction with P6. Glossary expanded: solve_constraints, LawfulRewriteWitness, ConstraintGraph, ClosedWorldDependencyWitness, canonical (source) grounding. Doc grew to 667 lines. The strongest form of the thesis now: the compiler transforms a canonical grounded program graph, not just a syntax tree. Containment enables folds; typed dependencies enable scheduling/incrementality/parallelism; canonical grounding enables decidable coercion; lawful rewrite witnesses enable CUDA/MapReduce-style structure changes; lenses observe the grounded graph but do not participate in the homomorphism. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: separate ingest layer from compile-core (data-first surface) Operator-direct ratification: compile-core operates on data (CoreNode), not text. Text is one of several legitimate ingest entry points, not THE entry point. Substrate is data-first. Motivation: lens/query/affected-set/IDE workflows operate on Node data, not text. Forcing every entry through text would either require lossless code-mod tooling for all cases or constrain the substrate's expressiveness. The cleanest separation is to make ingest a separable layer with multiple entry paths, all producing CoreNode. Signature change: compile(source: CoreNode, input_lang, mode) -> Outcome<Output> ingest_text(text, input_lang) -> Outcome<CoreNode> Other ingest paths (no text involved): - Programmatic builder (IDE plugins, code generators). - Query-driven rewrite (affected_set + transformation). - Round-trip from a prior TargetNodeTree. All produce CoreNode; compile takes it from there. Pipeline diagram updated to show the INGEST / COMPILE-CORE separation. Stage table now has a "Layer" column distinguishing INGEST stages (parse, normalize) from COMPILE-CORE stages (resolve, ground, translate, serialize, eval). Carrier shape progression diagram updated to show the multi-source funnel into CoreNode. Boundary actions: - Compile-core: write output text (or execute), report diagnostics. Pure data-in / data-out otherwise. - Ingest layer (separable): read input text only when ingesting from text. The CoreNode is the substrate-canonical Node — six connectives + five behaviors only, sugar dissolved. The compile contract is uniform regardless of how CoreNode was authored. Glossary expanded: ingest, ingest_text. This sharpens what was already implicit (the carrier taxonomy already distinguished SurfaceNode/CoreNode) and makes the lens/query story cleaner: those operate on Node data directly, without going through text. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: integrate read/edit pipeline + self-modification (per sunny-wolf-435 review) Major doc amendment integrating the substantive review from PR #3437's sister doc (sunny-wolf-435 PM, against docs/design-read-edit-pipeline.md which merged in PR #3364 on 2026-05-19). Reviewer feedback was that the compiler-architecture doc had a substantial gap: it covered the COMPILE direction (text/data → target) thoroughly but was silent on the EDIT direction (CoreNode + Diff → CoreNode'), the read/edit pipeline merged in PR #3364, and the closely-related question "how will the compiler edit itself / regenerate stage0?" CHANGES: 1. NEW "Load-bearing references" section (after "What this document is"): Comprehensive list of foundational + adjacent ratified design docs the compiler architecture composes with. Includes THESIS / MODELING / modeling-discipline / INVARIANTS / TASKS as foundational, and 11 adjacent design docs (read-edit-pipeline, emit-stage-l25, infer-stage-l25, lens-application-surface, lens-framework, affected-set-lens, dissolution-lens, v4-close-interrogation, v4-dag-rationale, pure-bootstrap-zero, substrate-lambda-calculus-grounding, bootstrap-fact-model) plus 6 lens-specific design docs. 2. NEW 9th substrate primitive: apply_diff - Path / Edit / Diff vocabulary ratified in PR #3162 (std/node.dag) - apply_diff scaffold in lens/application.dag (T-23) - The substrate is read/write-symmetric: reads via fold_node / apply_lens; writes via apply_diff - Primitive set is now 9 things (was 8); TL;DR + tally line updated 3. NEW "The EDIT direction — symmetric to compile" section: - Read/edit primitives table (Path, Edit, Diff, apply_diff, subterm_at, apply_lens, affected_set) - The seven-step read→edit pipeline from PR #3364 § 4 - Candidate-state pattern: gates run against apply_diff(dag, Diff), NOT the pre-edit graph. Same monotonic-facts invariant as P3's facts-flow-forward, applied to mutation. - EDIT direction = the "Query-driven rewrite" ingest path (cross-link to the ingest paths table) - Library-first agent surface (per read/edit doc § 6.10) — extended to apply to compile() too - Lens as (find, transform) convolution view; cross-ref to mechanical refactor hero case (f) in read/edit doc § 6.7b 4. NEW "Self-modification, stage0, self-edit" section addressing the reviewer's specific question: - Compiler reads its own source as CoreNode (same lens surface as user code; no special introspection) - Compiler writes to its own source via apply_diff (two paths: hand-authored Diff or mechanical-refactor lens) - stage0 regeneration is compile(self, dag, TranslateTo(rust)) — no special mode; the homomorphism mechanic applies identically - Candidate-state for self-modification safety — lenses gate the candidate; compiler cannot break itself silently - Implications: no new substrate needed; self-hosting is one specific compile invocation; hand-Rust-to-zero IS the loop closing. 5. Glossary expanded with Path / Edit / Diff / apply_diff / apply_lens / SectionRef / scope_in / candidate-state pattern / affected_set / self-edit-stage0 vocabulary. The compile + edit directions are now both represented in the doc. The two designs (this one + read/edit pipeline) compose cleanly — same CoreNode, fold_node, Diagnostic substrate; the read/edit doc owns the agent-surface mechanics, this doc owns the homomorphism architecture, both are the same nine substrate primitives at different angles. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: address 3 BLOCKING codex findings on commit 77fe746 Findings on PR #3437 from codex 2026-05-20T05:24:15Z, all addressed in this commit: FINDING 1 — Validate-then-compile gate not type-enforced. P3 commitment 6 said the project-mandatory wrapper preserves the "by construction" guarantee, but that was convention, not type-level enforcement. Updated to require Validated<Output>-style carrier discharged only by the wrapper; bare compile() now explicitly marked as internal/non-terminal (accessible to advanced consumers — lens framework, build tooling, self-edit — but NOT the everyday user surface). The wrapper-as-terminal pattern is invariant at the type level. FINDING 2 — Substrate inventory verifiability. The reviewer flagged "live-substrate inventory was not verified against the v4 tree." Verified refinement.dag IS on main (1143 bytes, status "T-25-core modeled" — landed via #3354); the doc claim was correct. Added a "Verifiability note" pointing at the verification commands (ls + head -10) + added commit refs (#3354 for refinement.dag, #3162 for Path/Edit/Diff vocabulary, #3436 for in-flight T-8 PR) so future reviews can verify independently. Also added lens/application.dag and lens/affected_set.dag to the inventory (they were missing). FINDING 3 — Scaffold-vs-design divergence. The reviewer correctly identified that the compiler scaffolds in src/v4/compiler/ predate this doc's ratifications and have divergent signatures (00_compile.dag's `compile(Source, TargetModel) -> TargetSource` vs this doc's `compile(CoreNode, LanguageModel, CompileMode) -> Outcome<Output>`, 04_infer.dag's `v4.lens.cost` import vs P3's no-named-lens rule, etc.). Added a "Scaffold-vs-design divergence — implementation migration plan" section that explicitly catalogs the divergences and prescribes the migration. The scaffolds are shape placeholders; implementation workers should land the ratified interface, not preserve stale signatures. NOT addressing as a separate finding — eager-bat-439 archive refused because PR #3436 is still open. Worker delivered cleanly (2 approvals, CI green, conflict markers resolved); operator manual squash-merge is the gate. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: P8 compiler-self-application + refined testgen lens-family + regeneration substrate Integrates the operator's review per 2026-05-20 — two ratifications + named regeneration substrate. NEW PREMISE P8 — The compiler is not exempt from its own discipline: The compiler is itself a modeled system. Its layers (stages, language models, lenses, testgen, target models, diagnostics, glue derivation) are modeled as dependency graphs over the same substrate primitives. When an upstream model changes, the compiler computes the affected downstream subgraph (T-21 affected_set) and regenerates derivable artifacts; non-derivable consequences fail-closed. "No hidden anything" generalized: no implicit conventions, no manual synchronization, no hidden emitter / parser / test-generator / integration- updater / layer-specific-patcher / ad-hoc-Node-traversal-outside-primitives. Every compiler-internal artifact must be a substrate primitive OR a declared algebra OR a lens OR a projection OR a target/runtime policy. The slogan: the compiler is the first consumer of its own modeling discipline. If implementation workers find themselves writing ad hoc code to keep compiler layers in sync, that is a STOP condition. Two worked examples added under P8: - testgen self-regeneration: Refinement<T> shape changes → affected_set computes which TestClaims/TestCases/target test files regenerate → lens family re-fires automatically on the affected subgraph. - LanguageModel self-regeneration: LanguageModel gains a new field (e.g., effect-semantics per Q10) → affected_set computes which stages/lenses depend on it → each extends or fails-closed on the new field. NEW "Named regeneration substrate" section (under P8) cataloging the substrate concepts P0 + P8 need that are not yet declared: - ChangeSet (std/change.dag) - AffectedSet (T-21 is the lens-frontier specialization; full version not yet declared) - Projection (std/projection.dag) - Artifact (std/artifact.dag) - RecomputePlan REFINED TESTGEN LENS FAMILY (per reviewer's three-layer taxonomy): - Layer 1: TestClaimLens — InferredTree → TestClaim Witnesses (abstract behavioral claims: roundtrip / refinement-boundary / algebra-law / protocol-compat / effect-idempotency) - Layer 2: TestCaseLens — TestClaim Witnesses → TestCase Witnesses (concrete cases: examples, boundary cases, property-test generators, fuzz seeds, regression fixtures) - Layer 3: TargetTestProjection — TestCase Witnesses + target LanguageModel → target test source (Rust #[test], pytest, Jest, integration harness) Profile invocations expanded with reviewer's full taxonomy: smoke, boundary, property, algebra_law, effect, integration, roundtrip, equivalence, fuzz, regression. All share std/verification.dag (landed) + std/refinement.dag (landed) + std/dependency.dag (P6 substrate, not yet declared) + std/testgen.dag (renamed from lens/testgen.dag, follow-up bookkeeping). Self-regeneration cross-reference: when a model fact changes, affected_set computes which testgen lenses re-fire on which subgraph — no manual sync. GLOSSARY EXPANDED: TestClaimLens, TestCaseLens, TargetTestProjection, ChangeSet, AffectedSet, Projection, Artifact, RecomputePlan. The compiler architecture now has the full mental model: - Semantic substrate: 6 connectives + 5 behaviors - Compiler substrate: 9 primitives (fold_node, traverse, grammar-as-data, solve_constraints, coercion fold, LawfulRewriteWitness, dep graph, apply_diff, diagnostic+locus) - System substrate (not yet declared): ChangeSet, AffectedSet, Projection, Artifact, RecomputePlan - Derived outputs: target code, eval values, tests, dim facts, glue, diagnostics, and compiler artifacts themselves (P8) The big idea: v4 does not merely compile .dag programs. v4 models systems — including itself — as dependency graphs, then regenerates all downstream projections when upstream facts change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: P9 stratified bootstrap — stage0 as generated artifact, not self-modifying code Integrates the reviewer's critical clarification (2026-05-20): "compiler edits itself" is loose; the precise framing is "compiler models itself; generates candidates; promotion is guarded." Resolves the architectural ambiguity in the prior self-modification framing without falling into v2's manual-stage0-patch failure mode OR free-runtime-self-modification (intractable). NEW PREMISE P9 — Bootstrap is stratified; stage0 is a generated artifact: The compiler may model and regenerate its own implementation, INCLUDING stage0, but no running compiler generation mutates itself in place. The compiler can DERIVE AND VERIFY a replacement stage0 from Stage0Spec; it cannot arbitrarily rewrite itself at runtime. THREE-PIPELINE FRAMING (must not collapse): 1. Semantic compile pipeline — text → InferredGraph → target/eval. 2. Artifact projection pipeline — InferredGraph → generated compiler code / tests / docs / schemas / glue / stage1 source. 3. Bootstrap promotion pipeline — current Stage0[k] + candidates → Stage0[k+1] (or rejection diagnostic), guarded by BootstrapWitness + FixedPointWitness. The mistake is collapsing all three into "the compiler edits itself." WHAT STAGE0 IS: - A minimal seed runner (NOT "the whole compiler but worse"). - Consumes a stable canonical CorePackage (NOT arbitrary evolving surface syntax). - Stage0Contract declares: load CorePackage; understand stable Node/Core schema; run minimal fold_node/traverse; fail-closed diagnostics; emit verified artifact. This decoupling is the structural answer to v2's pain — surface language / parser / normalizer / lenses can all evolve without breaking stage0 because stage0 consumes the canonical package, not the surface. BOOTSTRAP EPOCH LOOP: - Stage0[k] + CorePackage[k] → Stage1[k] - Stage1[k] + SourceModels[k] → Stage1'[k] - verify(Stage1[k] == Stage1'[k]) → FixedPointWitness[k] - Upgrade k → k+1: ChangeSet + AffectedSet + RecomputePlan → Stage0Candidate + Stage1Candidate → verify → promote. Only the promotion protocol replaces the active stage0. No back edge anywhere else. THREE CASES for compiler-contract changes: 1. Normal downstream (no stage0 impact) — affected artifacts recomputed. 2. Bootstrap-compatible stage0 change — current compiler generates Stage0Candidate; verify; promote. No manual edit. 3. Bootstrap-breaking change — requires modeled Bridge[k → k+1] migration package, or fails closed with BootstrapBreak diagnostic. CRITICAL INVARIANT: "At no point does an artifact become source of truth merely because it is needed for bootstrapping." Generated stage0.rs / compiler.corepkg / generated compiler source / generated tests are NOT authorities — they're disposable artifacts with witnesses. The source of truth remains .dag models + Stage0Contract + CorePackageSchema + Projection definitions. CONCEPTUAL STACK (Layer 0-4): - Layer 0: Seed (stage0 executable, minimal, audited, consumes CorePackage) - Layer 1: Substrate models (.dag, source of truth) - Layer 2: Compiler models (.dag, source of truth) - Layer 3: Generated compiler artifacts (disposable, regeneratable) - Layer 4: Verification / promotion (procedural and conservative gatekeeper) Only Layer 0 is hand-seeded. Layers 1-2 are source of truth. Layer 3 is disposable. Layer 4 is the gatekeeper. TWO DISTINCT DEPENDENCY GRAPHS (must be separated): - Program dependency graph (P6) — Contains / BindsTo / TypeDependsOn / DataDependsOn / EffectDependsOn / ResourceDependsOn / ModuleDependsOn / BarrierBefore / PlacementConstraint. - Build / bootstrap dependency graph (new) — ModelDependsOn / ProjectionDependsOn / GeneratedFrom / VerifiedBy / PromotedBy / BootstrapDependsOn. Keeping them separate prevents the confusion "does the compiler's own resolver depend on the resolver it is resolving?" — answer: at epoch k, Stage0[k] resolves model[k] enough to build Stage1[k]. No active stage depends on its own output. NEW BOOTSTRAP SUBSTRATE (P9 implies these; not yet declared): - Stage0Contract, BootstrapEpoch - CorePackage, CorePackageSchema - Bridge (migration package for bootstrap-breaking changes) - BootstrapWitness, FixedPointWitness - PromotionPlan, PromotionDiagnostic / BootstrapBreak Likely lands in std/bootstrap.dag alongside P8's regeneration substrate (ChangeSet / AffectedSet / Projection / Artifact / RecomputePlan). WHAT THIS RULES OUT (STOP conditions for implementation workers): - Code letting stage0 directly edit itself at runtime. - A "bootstrap workaround" that hand-edits stage0 outside the candidate / promotion path. - A "we know this is safe" that skips fixed-point verification. - Generated-artifact files treated as authorities. UPDATED EXISTING SELF-MODIFICATION SECTION to cross-reference P9 and clarify that the "compiler edits itself" framing is loose; the precise mechanic is candidate generation + verification + promotion. GLOSSARY EXPANDED: Stage0Contract, CorePackage / CorePackageSchema, BootstrapEpoch, Bridge, BootstrapWitness / FixedPointWitness, promotion protocol. The "fractal feeling" of self-application is now resolved structurally: the pattern is stratified (Layer 0 → Layer 4), not infinitely recursive. Only the model layer is source of truth; the bootstrap layer is intentionally tiny; the promotion layer is procedural; the artifact layer is disposable. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: V4 work * design: address 3 new BLOCKING codex findings on P8/P9 work Findings on commit b1cfdb8 (codex 2026-05-20T06:44:32Z): FINDING A (3271748181) — P2 boundary discipline: T-21 affected_set as specialization vs full AffectedSet undeclared = split regeneration authority. Fix: clarified in "Named regeneration substrate" section that these substrate concepts must land as a UNIFIED coherent declaration (std/regeneration.dag or tightly-related cluster), not piecemeal. T-21's affected_set must be MIGRATED into the unified AffectedSet — not left as a parallel concept (which would itself be a P2 violation). Implementation order updated: declare the regeneration substrate as a unit; migrate T-21 into the unified shape. FINDING B (3271748191) — P3 fail-closed: "fail-closed-or-default" wording in the language-model self-regeneration worked example allowed silent default acceptance of missing newly-required facts. Fix: removed "fail-closed-or-default". Replaced with explicit choice — either (a) a typed Default<T> witness declared as substrate data (modeled default, NOT implicit silent default), or (b) a fail-closed diagnostic. No silent default acceptance — per P3, missing newly-required facts produce typed witness OR diagnostic, never unsignalled default. FINDING C (3271748200) — P2 boundary discipline: stage0 self-compile path appeared to fold parse + normalize back into compile(...), contradicting the text/data separation where compile-core consumes CoreNode. Fix: rewrote the stage0-regeneration code block to show explicit ingest_text + compile composition. Compile-core takes CoreNode (data), never text. ingest_text is the separable boundary; compile is the pure data-in / data-out core. Added "Equivalent paths" note showing other ways to obtain CoreNode (already-cached, programmatic builder, query-driven rewrite) — all funnel through compile() taking CoreNode. The "no special regenerate stage0 mode" claim is preserved (stage0 regeneration is still compile(self_corenode, dag, TranslateTo(rust))) but the ingest boundary is now explicit and separable. v2's manual-patch failure mode is structurally precluded by the ratified text/data separation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: tighten I/O — no boundary actions; everything is modeled effects Operator-direct refinement: the "shim/modeling thing extends to reads/writes as well." The architecturally pure approach models files, file_system, shell, and OS independently in extdeps/; all I/O is modeled effects against modeled resources; compile-core has no boundary actions. CHANGES: 1. TL;DR boundary actions reframed: FROM: "Compile-core boundary actions: write output text (or execute), report diagnostics. Two actions; compile-core is otherwise pure data-in / data-out. Ingest-layer boundary actions (separable): read input text only when ingesting from a text source." TO: "Compile-core has no boundary actions. The compile core is purely data-in / data-out. All real-world I/O — reading source from disk, writing target source to disk, executing on a host, reporting diagnostics to stderr — is modeled as effects against modeled resources (extdeps/file_system.dag for files, extdeps/process.dag for shell/OS, extdeps/network.dag for network), composed by peripheral shims outside the compile-core surface." 2. End-to-end I/O section rewritten: - Removed ingest_text from the public substrate primitive signature. - Added explicit "Peripheral shims for text and file I/O" subsection showing the composition: file_read (modeled effect) + ingest_text (shim) + compile (pure) + file_write (modeled effect) — each step is its own substrate-modeled operation, NOT a compile-core boundary action. - Added "Why this matters architecturally" — no hidden side effects; dry-run works as composition; incremental rebuild works because every artifact's provenance is modeled; self-modification is safe because apply_diff is modeled, not implicit. - Slogan: "No implicit I/O. Files are not the architecture. Effects are modeled, not assumed." 3. Glossary added: - peripheral shim — user-facing convenience composing modeled effects with compile-core; NOT a substrate primitive. - modeled effect — real-world I/O declared as substrate data in extdeps/ carrying EffectDependsOn / ResourceDependsOn edges; visible to lenses; substitutable for dry-run. This sharpens P0 + P8 + P3-dry-run: there are no implicit side effects anywhere in the architecture. Files are orthogonal to the architecture; they're modeled in extdeps/file_system.dag, NOT load-bearing for compile. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * design: tighten catamorphism/homomorphism/coercion terminology + MVP routes Four targeted tightenings before this wave of worker dispatch: 1. NEW "Terminology" subsection before P5: catamorphism / homomorphism / coercion are three terms at three levels (mechanism / noun / verb). The coercion fold is a catamorphism whose job is to verify a homomorphism. Translation IS the homomorphism (the noun); coercion is the verification verb. Doc passages conflating "coercion fold" with "homomorphism mechanic" generically are sloppy and should be flagged. 2. Coercion fold primitive description now names the TranslatePlan extension slot: conceptually TranslatePlan = ExactCoercion(source_grounding, target_node) | RewrittenThenCoerced(rewrite_witness, ...) MVP implements only ExactCoercion; future LawfulRewriteWitness (P7) lands the second variant without refactor. 3. Artifact carrier (in the regeneration substrate) now reserves bootstrap-related ArtifactKind variants up front: Stage0Candidate, CorePackage, WitnessBundle. Lets P9 bootstrap substrate land later without forcing artifact/projection refactor. 4. NEW "MVP routes — named explicitly" section before "What's NOT in scope": - Core MVP: compile-core homomorphism produces TargetSource from CoreNode - MVP-A (translate-only): Core MVP + file_system shim → file-to-file - MVP-B (eval-only): Core MVP + host_model + T-22 → Value Either MVP-A or MVP-B is sufficient as the first proof point; both together is the strongest exercise. The terminology section is the key piece — operator + reviewer were unclear on whether we were moving from coercion to homomorphism; the answer is they coexist at different levels and the doc should use them precisely. The other three are scope-reservation moves that prevent future refactor when held substrate (LawfulRewrite, bootstrap, multi-lens) eventually lands. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Cursor review surfaced three findings against the original audit; all three were valid. 1. T-25-core IS landed (std/refinement.dag, PR #3354; TASKS.md:1252 [SUBSTRATE LANDED]; Refined<Int> in active use in posix.dag, ktfmt.dag, lean4_format.dag). Flips §1.1 formatter-int-refinement (63 sites) and §1.5 rustfmt-ignore-path-refinement (1 site) from NECESSARY → UNNECESSARY. §1.1 becomes the largest single dissolution available in the v4 corpus. 2. feature:t19-claim-anchor-split is NOT stale. TASKS.md:1042 records active T-19 Phase-2 follow-up; std/verification.dag:196 carries matching RULING-1: needs-more-work. The bind is correctly active. §A4 RETRACTED. 3. §5 cross-ref pointed at §1.8 for "stale bind label" — wrong section reference. Updated §5 to identify §1.8 as the labelling defect (mis-rooted bind for swift-format-rules-carrier). Also added §A8 to fix the §B methodology gap (refinement.dag was omitted from the inspection list). Revised headline: ~69 unnecessary annotation rows (was ~6), driven almost entirely by §1.1. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(audit): v4 deferral audit 2026-05-29 Exhaustive scan + classification of every deferred / scheduled-but-deferred / staging / gated marker in the v4 corpus per operator directive 2026-05-29. Verdict: ledger is overwhelmingly honest. ~276/282 gated annotations and all ~25 prose deferrals trace to real upstream substrate gaps or external triggers. Misclassifications cluster narrowly: three T-4.16 follow-on gates are intra-task slicing (formatter-cross-field-constraints, rustfmt-deprecated-alias, rustfmt-unstable-option-validity), two bind labels are mis-rooted (rustfmt-ignore-path-refinement, swift-format-rules-carrier), one cluster has a stale bind label (testgen.dag RULING-1). Action items §A1-§A7 catalogued for follow-on cleanup; no substrate changes in this PR (audit only). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): correct v4 deferral audit per cursor review #3880 Cursor review surfaced three findings against the original audit; all three were valid. 1. T-25-core IS landed (std/refinement.dag, PR #3354; TASKS.md:1252 [SUBSTRATE LANDED]; Refined<Int> in active use in posix.dag, ktfmt.dag, lean4_format.dag). Flips §1.1 formatter-int-refinement (63 sites) and §1.5 rustfmt-ignore-path-refinement (1 site) from NECESSARY → UNNECESSARY. §1.1 becomes the largest single dissolution available in the v4 corpus. 2. feature:t19-claim-anchor-split is NOT stale. TASKS.md:1042 records active T-19 Phase-2 follow-up; std/verification.dag:196 carries matching RULING-1: needs-more-work. The bind is correctly active. §A4 RETRACTED. 3. §5 cross-ref pointed at §1.8 for "stale bind label" — wrong section reference. Updated §5 to identify §1.8 as the labelling defect (mis-rooted bind for swift-format-rules-carrier). Also added §A8 to fix the §B methodology gap (refinement.dag was omitted from the inspection list). Revised headline: ~69 unnecessary annotation rows (was ~6), driven almost entirely by §1.1. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): sweep T-25-core binds + fix Optional carrier authority Inline review on PR #3880 surfaced two additional findings against commit cc42f77; both valid. 1. T-25-core sweep — beyond §1.1 (formatter-int-refinement, 63 sites) and §1.5 (rustfmt-ignore-path-refinement), two more gates bind directly to T-25-core: rustfmt-macro-name-refinement (rustfmt.dag:136) and rustfmt-version-string-refinement (rustfmt.dag:146). Both belong in the dissolve-now set against landed std/refinement.dag. Added to §1.9 long-tail callouts and §A1 dissolve-now set; §5 totals revised (~71 unnecessary annotation rows; 7 distinct unnecessary gates). 2. Optional carrier authority — original §1.6 / §A6 cited `std/option.dag`, which does not exist. The live optional carrier is `v4.std.collection.Optional<T>` (src/v4/std/collection.dag:20). Updated all references (§1.6, §A6, §5 substrate list, §B inspection list). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): add bounded-exception preamble per ledger standing principle Inline review + codex review on PR #3880 both flagged that the audit doc lacks an explicit bounded-scope declaration under CLAUDE.md's Ledger standing principle (operator 2026-05-19), even though it functions as a one-time snapshot under explicit operator directive 2026-05-29. Added "Ledger standing — bounded exception" preamble declaring: - Point-in-time classification snapshot, not a maintained ledger - Dissolution trigger: delete file once §A1–§A8 executed or dismissed - Non-maintenance pledge: rows go stale as inline marks evolve; that is expected and fine - No competing disposition: every action cites the authoritative inline mark / task-line; no row overrides bind / dissolve-on text Authority remains with the inline marks. Both prior approving reviewers (claude + cursor) already validated the doc fits the established docs/audit/ pattern; this preamble makes that explicit. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): align §A1 / §5 counts with §1.9's 66-site dissolve-now set Cursor review on PR #3880 flagged that §A1 still titled the work as "DISSOLVE formatter-int-refinement (63 sites)" while §1.9 already expanded the landed-T-25-core dissolve-now set to 66 sites (63 formatter-int-refinement field marks + rustfmt-ignore-path-refinement + rustfmt-macro-name-refinement + rustfmt-version-string-refinement). A reader following only §A1 could stop three gates short. - §A1 retitled to "DISSOLVE all landed-T-25-core formatter refinement gates (66 sites total)" with the breakdown spelled out matching §1.9. - §5 headline annotated to cross-reference §A1's 66-site set so the "63 sites" figure (which is correct for formatter-int-refinement alone) doesn't read as the full dissolve-now scope. Single authority restored across §1.9 / §A1 / §5. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): fix §1.9 long-tail census mislabel (codex + inline review) Both codex (BLOCKING) and inline review surfaced the same defect: §1.9 was titled "Long-tail single-site gates (75 distinct gates)" but immediately listed 2-7-site gates, making the 97-gate census/action math internally uncheckable (P2 single-authority violation inside the audit's own classification surface). True distribution from `grep -rhoE 'feature:[a-z][a-z0-9_-]+' src/v4/`: - 13 sites: 1 gate (tabulated as §1.2) - 7 sites: 1 gate - 6 sites: 1 gate - 5 sites: 1 gate - 4 sites: 2 gates - 3 sites: 2 gates - 2 sites: 17 gates (14 NECESSARY long-tail + 3 already tabulated) - 1 site: 72 gates (singletons; 4 tabulated in §1.5-§1.8) Total: 97. Tabulated: 8. Remaining long-tail: 89. Fix: rename §1.9 to "Long-tail gates — remaining 89 distinct gates", add an explicit site-count distribution table, and extend the representative-examples list to include all multi-site (>=3 sites) un-tabulated gates so the count balances against the §5 totals. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: DEFERRAL AUDIT (operator-directive 2026-05-29): exhaustive scan + classi * docs(audit): fix §1.3 formatter-cross-field-constraints undercount Both codex (BLOCKING) and inline review surfaced the same defect: §1.3 listed "3 sites: rustfmt, ktfmt, black" but clang_format also carries the gate (4 annotation rows there). Real per-file counts: clang_format: 4 rows black: 1 row ktfmt: 1 row rustfmt: 1 row total: 7 annotation rows across 4 files Updates: - §1.3 retitled to "7 annotation rows across 4 formatter files" with per-file breakdown. - §A6 dissolve-now action updated to name all 4 formatter files and the 7-row count. - §5 unnecessary annotation rows revised ~71 → ~75 to reflect the +4 additional rows in §1.3. Per-gate breakdown in §5's UNNECESSARY column unchanged (still 7 distinct gates); only the per-row totals shift. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): add §0 canonical grep commands for census reproducibility Codex review on PR #3880 (BLOCKING) flagged that the audit mixes three distinct grep populations — `feature:NAME` distinct names, total `🟡 gated` annotation rows, and per-gate shorthand annotation counts — without naming a single canonical normalization, so reviewers running their own grep get different numbers and the census becomes uncheckable. Also relevant: an inline review reported "84 distinct names on origin/main" against the cited grep; I cannot reproduce that figure (`git grep -hoE 'feature:[a-z][a-z0-9_-]+' origin/main -- src/v4/ | sort -u | wc -l` returns 97 on both origin/main and HEAD; I posted the spot-check on the PR). Adding §0 should let any future reviewer disambiguate which population a number is reporting. Added §0 "Census reproducibility — canonical grep commands": - Population A: distinct gate names (97 — used in §1 intro, §1.9 table) - Population B: total annotation rows (~282 — used in §1 method para, §5 totals) - Population C: per-gate annotation rows (used in §1.1 "63 sites", §1.3 "7 rows" — counts shorthand `🟡 gated: NAME` annotations, not just `feature:` headers) Each row gives the exact `git grep` command and the result against `origin/main`, with a note that alternative regexes (e.g. only headers = 43; spaced `— feature:` = 120) are not the audit's canonical commands and will give different numbers. No classification changes; pure methodology disclosure. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): correct DECISIONS.md path → src/v4/DECISIONS.md Codex (BLOCKING) + inline review on PR #3880 both flagged that the audit cites bare \`DECISIONS.md\` (top-level path), which does not exist on origin/main; the tracked file is \`src/v4/DECISIONS.md\` (blob 0d89ca2). Fixed both references (§3 intro + §3.6 heading). P2 single-authority restored; the §3.6 row now points at a real source-of-truth on origin/main. No classification change — §3.6 still records "historical context, no live item" (single non-actionable deferral). §5 totals unchanged. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): re-reproduce §0 census against fresh origin/main + add timestamp Codex (BLOCKING) + inline review on PR #3880 claim the §0 numbers don't reproduce on origin/main (84 distinct names / 242 rows vs the audit's 97 / ~282). Re-verified against freshly-fetched origin/main @ df91abc: $ git grep -hoE 'feature:[a-z][a-z0-9_-]+' origin/main -- src/v4/ \ | sort -u | wc -l 97 $ git grep -c '🟡 gated' origin/main -- src/v4/ \ | awk -F: '{s+=$NF}END{print s}' 279 Both numbers reproduce. The audit's audit-time B-population grep yielded ~282; today's count is 279 (drift of 3 rows as gates landed/dissolved between authoring and re-verification — within the "~" tolerance §5 already advertises). Population A is stable. The reviewer's 84 / 242 figures do not reproduce against the cited commands on either origin/main or current HEAD; the discrepancy must be in the reviewer's command or ref, not the audit's claims. Added a "Last reproduced" footnote with the origin/main SHA and restated the canonical commands. Also corrected the B-population grep snippet to match the actual command (`-c '🟡 gated'` rather than `-cE`, removing a stray escape). No classification changes. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): fix §1 intro contradiction with §1.9 (internal P2) Inline review BLOCKING on PR #3880: §1 intro still said "occurrence count ≥2 tabulated below; long tail is 75 single-occurrence gates", which contradicts §1.9's corrected distribution showing 89 long-tail gates that include multi-site entries (2-7 sites each). Rewrote §1 intro to match §1.9: 8 representative gates tabulated (5 multi-site + 3 singletons across §1.1-§1.8); 89 remaining gates summarized in §1.9 with the full site-count table there. Internal P2 single-authority for the audit's own surface restored. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): fix §4 clang_format sample evidence (codex + inline review) Codex (BLOCKING) + inline review on PR #3880 flagged that §4 claimed "all clang_format gated rows trace to §1.1", but the file actually carries three distinct gates: $ grep -oE '🟡 gated[: ]+[a-z-]+' src/v4/extdeps/formatters/clang_format.dag \ | sort | uniq -c | sort -rn 35 🟡 gated: formatter-int-refinement 3 🟡 gated: formatter-cross-field-constraints Plus 1 `gated consumer:config-patch-record-projection` consumer tag that routes to §1.2. The original §4 sentence under-counted the route by omitting §1.2 and §1.3. Regenerated §4 from the grep output as a route-table showing all three gates and their tabulated §1 destinations. The §4 conclusion holds: zero v4 deferral inside a "staging" noun in clang_format; every gated row routes to a tabulated §1 entry. The codex finding's companion §1 census issue was already fixed in 5951277. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): derive §5 dissolve-now count from §A1/§A6 (codex + inline) Codex (BLOCKING) + inline review on PR #3880 flagged that §5's headline said "~69 yellow marks" but the audit's own action lists enumerate 66 (§A1 landed-T-25-core set) + 7 (§1.3 cross-field, after clang_format correction) + 2 (§1.4 deprecated-alias) + 1 (§1.6 unstable-option-validity) = 76 sites — and the earlier "four T-4.16 follow-on gates" framing double-counted §1.5 (already folded into §A1's 66-site set). Rewrote the §5 closeout sentence to: - name §1.5 as already in §A1 (no double-count) - derive 76 explicitly from §A1 (66) + §A6 (7+2+1) - cross-reference §5's ~75 row as the ±1 grep tolerance Matches the §A inventory; internal P2 single-authority for the dissolve-now count restored. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: DEFERRAL AUDIT (operator-directive 2026-05-29): exhaustive scan + classi * docs(audit): major census fix — distinct gate count 97 → 130 (inline review) Inline review on PR #3880 (BLOCKING) caught that the §0 canonical grep `feature:[a-z]` (no-space form only) systematically undercounted the gate population: inline marks use BOTH spaced (`feature: NAME`, typical of header declarations in rustfmt/clang_format) and unspaced (`feature:NAME`) forms, and the audit's command captured only unspaced. Recount on origin/main @ df91abc: unspaced `feature:[a-z]`: 97 distinct spaced `feature: [a-z]`: 35 distinct overlap: 2 unified total: 130 distinct The 33 missing gates include headline tabulated gates: formatter-int-refinement, formatter-cross-field-constraints, lean4-option-closed-set — all use spaced form for headers. Updates: - §0 canonical command rewritten to the unified spaced+unspaced grep - §0 documents the original undercount and the correction - §1 intro: "97 distinct" → "130 distinct" - §1.9 census heading: "remaining 89" → "remaining 122" - §1.9 distribution table regenerated from unified grep (was 13/7/6/5/4/4/3/3/2(×17)/1(×72) totaling 97; now 13/9/7/6/5(×3)/4(×4)/3(×4)/2(×20)/1(×95) totaling 130) - §5 distinct-gates total: 97 → 130 (unnecessary col unchanged at 7) - §5 annotation-rows total: 282 → 279 (live origin/main count) - Method intro: 282 → 279, added "130 distinct" Substantive classifications unchanged: every gate in §1.1-§1.8 was spot-checked directly for NECESSARY/UNNECESSARY; the undercount was in the long-tail census denominator, not the tabulated rows. §A1's 66-site dissolve-now set is derived from population C (per-gate shorthand grep) which was already correct. §A6's intra-task slicing list is unchanged. Codex's companion finding (one canonical normalized grep) addressed on the PR via separate reply: the inline marks' three syntactic forms (Form 1 header, Form 2 shorthand, Form 3 consumer tag) cannot be reduced to one regex without false positives on the literal "feature"/"consumer" tokens; the audit's three named populations + canonical commands ARE the single authority over the multi-form mark grammar, per the bounded-exception preamble's non-maintenance pledge. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: DEFERRAL AUDIT (operator-directive 2026-05-29): exhaustive scan + classi * docs(audit): unify §1.x/§A counts on Population C (all-forms) per inline review Inline review on PR #3880 (BLOCKING) caught that Population C's grep in §0 returned 3 for formatter-cross-field-constraints, not §1.3's 7, because the regex `gated[:—] ?` matched only `gated:` or `gated—` with no internal space — missing the `gated — feature: NAME` header form. Fixed: Population C (all forms): `git grep -cE 'gated[ —:]+(feature: )?X' origin/main -- src/v4/' formatter-cross-field-constraints → 7 ✓ matches §1.3 formatter-int-refinement → 66 Population C′ (field annotations only, historical): `git grep -cE 'gated: ?X|gated consumer: ?X'` formatter-int-refinement → 63 formatter-cross-field-constraints → 3 Inconsistency surfaced: §1.1 cited the C′ value ("63 sites") while §1.3 cited the C value ("7 rows"). Reconciled by standardizing on Population C across all §1.x and §A entries: - §1.1: "63 sites · 9 formatter files" → "66 annotation rows across 5 formatter files (63 field + 3 headers)". The original "9 files" was also incorrect — only 5 formatter files carry the gate. - §1.1 UNNECESSARY blurb: "All 63 sites" → "All 66 sites" - §A1: "66 sites total (63 + 1 + 1 + 1)" → "69 sites total (66 + 1 + 1 + 1)" - §5 headline: "~76 yellow marks (66 + 7 + 2 + 1)" → "~79 yellow marks (69 + 7 + 2 + 1)" - §5 row: "~75" → "~79", "~207" → "~200" NECESSARY column - §0: C′ marked historical/informational; documents the prior inconsistency and the migration to C as the single per-gate authority. Substantive classifications unchanged — every §1.x gate's status was spot-checked directly; the count corrections are population-bookkeeping, not classification changes. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: DEFERRAL AUDIT (operator-directive 2026-05-29): exhaustive scan + classi * docs(audit): population C single authority — scope + regex + §1.x recount Codex (BLOCKING ×3) + inline (BLOCKING ×4) on PR #3880 converged on: (1) Scope mismatch: declared corpus = src/v4 + docs/v4-*.md + docs/design-v4-*.md, but census greps used src/v4 only, missing 1 gate in docs/v4-compilation-milestones.md (feature:T-7-parse-walk-realization). (2) Population C regex undercounted: missed unspaced feature: (e.g. `feature:config-patch-record-projection`) and consumer:NAME forms (e.g. `consumer:config-patch-record-projection` in formatter files). config-patch returned BLANK; cross-field returned 3 not 7. (3) §5 mixed C and C′ counts. Fixes: - §0 pathspec expanded to full corpus: src/v4 + docs/v4-*.md + docs/design-v4-*.md. Population A = 140 (was 130 src/v4 only). Population B = 280 annotation rows. - §0 Population C regex tightened: `gated[ —:]+(feature:|consumer:)? ?X` Now covers feature:X, feature: X, consumer:X, consumer: X, and field shorthand. Verified counts: formatter-int-refinement = 66 config-patch-record-projection = 12 (was cited 13 — included a non-gated prose mention) formatter-cross-field-constraints = 7 rustfmt-deprecated-alias = 3 (was cited 2) lean4-option-closed-set = 3 (was cited 1) rustfmt-ignore-path-refinement = 1 rustfmt-unstable-option-validity = 1 swift-format-rules-carrier = 1 - §1.2: "13 sites" → "12 annotation rows (1 feature: header in std/patch.dag + 11 consumer: tags across 9 formatter files including 3 in prettier.dag)" - §1.4: "2 sites" → "3 annotation rows (1 header + 2 fields)" - §1.7: "1 site" → "3 annotation rows (2 headers + 1 field)" - §5 occurrence-rows row: derivation made explicit and single- authority — 66 + 7 + 3 + 1 + 1 + 2 = 80 - §5 headline: 79 → 80 (matches the new sum) Substantive classifications unchanged. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): reconcile Pop A=140, Pop B=280, fix §A6 §1.4 site count Cursor REQUEST_CHANGES on PR #3880 flagged three internal inconsistencies surviving the prior Population-C pass: (1) Population A definition split: §0 table = 140 (feature: + consumer:); other places (§1 intro, §1.9 census, "97→130 correction" note, "130 there") said 130 (feature: only). §5 row used 140 again. Long-tail math 130 − 8 = 122 didn't reconcile with the 140-based §5 row (would give 132). (2) §A6 listed rustfmt-deprecated-alias as "(1 site)" while §1.4 and §0's Population C example both say 3. (3) Population B drifted: method paragraph said 279, §0 table said 280 (pinned df91abc returns 280). Fixes: - Pop A standardized at 140 everywhere: method para "279 → 280", "130 distinct" → "140 distinct" in §1 intro and the correction note, "130 there" → "140 there", §1.9 heading "remaining 122" → "remaining 132" (140 − 8 tabulated = 132 long-tail). - Pop B standardized at 280 in the method para to match §0's table and the §0 Last-reproduced footnote. - §A6 §1.4: "(1 site)" → "(3 annotation rows under Population C: 1 feature: header + 2 field annotations)". The §0 Last-reproduced footnote remains pinned to df91abc for A=140/B=280; B-population drift since then is permitted by the non-maintenance pledge in the preamble. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): reconcile §1.9 table, §A7 §1.2 single-authority, §0 markup Cursor REQUEST_CHANGES on PR #3880 (HEAD d12a7a9) flagged five remaining stale-number / markup issues; addressed all five: - §1.9 distribution table totalled 130 (stale from pre-A=140 pass). Regenerated from pinned df91abc unified Population A grep (sites column relabeled "name appearances" to surface the difference between gate-name occurrences in the grep stream vs annotation rows — config-patch shows 25 name appearances because consumer: tags reference feature:NAME mid-line; the annotation-row count remains 12 per §1.2). - "Remaining 122 long-tail gates" → "Remaining 132" (140 − 8 tabulated = 132; prior replace_all missed the capital R variant). - Correction narrative "corrected to 130/122/95" → "140/132/95". - §A7: "12 consumer sites + 1 substrate site" (= 13) → "12 annotation rows under Population C: 1 header + 11 consumer tags" matching §1.2's single authority; the "11 formatter consumer hand-mirrors" dissolution scope made explicit. - §0 had a stray duplicate table-header pair around the audit-pathspec paragraph (broken markdown table). Removed the pre-paragraph header row; the working table-header now sits immediately above the table body. Pop A pinned at 140, Pop B at 280, both as last reproduced against df91abc. Substantive classifications unchanged. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): finalize §1.9 prose and §1 intro Pop A consistency Cursor REQUEST_CHANGES on PR #3880 flagged two remaining stale census references: - §1.9:279 prose said "all 130 distinct gate names (from §0 population A)" — §0 / §1 / §1.9 table all pin Pop A at 140. Updated prose to 140. - §1:129 intro called §1.2 a "13-site gate" — §1.2 documents 12 Population C annotation rows (the old 13 included a non-gated TASKS.md prose mention). Updated to "12-row §1.2". Both finds are stale-number sweeps from the prior 130→140 migration. Pop A=140, Pop B=280 now consistent across §0, §1 intro, §1.9 prose, §1.9 table, §5 row. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: DEFERRAL AUDIT (operator-directive 2026-05-29): exhaustive scan + classi * docs(audit): extend Pop A to include shorthand-only gates (inline + codex) Inline review + codex (BLOCKING ×2) on PR #3880 caught that the §5 "7 UNNECESSARY out of 140 Pop A gates" math mixes populations: rustfmt-ignore-path-refinement appears ONLY as field shorthand (🟡 gated: rustfmt-ignore-path-refinement) with no feature: or consumer: declaration, so it was not in Pop A's 140 but was counted in the UNNECESSARY numerator. Fix: extend Pop A's canonical grep to include shorthand-only forms: { feature:X | feature: X | consumer:X | consumer: X | 🟡 gated: X (shorthand-only) } sort -u Recount at pinned df91abc: 140 + 1 (rustfmt-ignore-path-refinement) = **141**. Long-tail = 141 − 8 tabulated = **133**. Updates (sweep): - §0 Population A grep updated to include shorthand; result 140 → 141 - §0 Last-reproduced footnote: A=140 → A=141 - §1 intro: "140 distinct" → "141 distinct" - §1 / §1.9 / §5 correction narrative: "140/132/95" → "141/133/95" - §1.9 prose: "140 there" → "141 there", "140 distinct" → "141 distinct" - §1.9 heading: "remaining 132" → "remaining 133" - §1.9 table singletons: 102 → 103; Total: 140 → 141 - §1.9 "Remaining 132 long-tail" prose → "Remaining 133" - §5 row: 140 → 141 (NECESSARY column 133 → 134) UNNECESSARY count unchanged at 7 distinct gates; the +1 shorthand-only gate had already been counted in the UNNECESSARY column under its §1.5 entry. Numerator (7) is now consistent with denominator (141). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

briansrls and others added 2 commits May 19, 2026 02:47

briansrls commented May 19, 2026

View reviewed changes

briansrls mentioned this pull request May 20, 2026

V4 5-PR sequential merge — #3428, #3354, #3420, #3363, #3381 (operator-authorized batch) #3435

Closed

6 tasks

briansrls merged commit e81f438 into main May 20, 2026
7 checks passed

briansrls mentioned this pull request May 24, 2026

TestClaim + substrate fills manager: T-14 + T-25-tail + T-30 + T-4.5 #3605

Merged

briansrls deleted the session/loyal-boar-155 branch June 1, 2026 18:42

Navigation Menu

Repository navigation

v4 T-25-core: std/refinement.dag — base-type + fail-closed validation substrate - #3354

v4 T-25-core: std/refinement.dag — base-type + fail-closed validation substrate#3354
briansrls merged 5 commits into
mainfrom
session/loyal-boar-155

briansrls commented May 19, 2026 •

edited

Loading

Uh oh!

briansrls commented May 19, 2026

Uh oh!

briansrls left a comment

Uh oh!

briansrls May 19, 2026

Uh oh!

briansrls commented May 19, 2026

Uh oh!

briansrls commented May 19, 2026

Uh oh!

briansrls commented May 19, 2026

Uh oh!

briansrls commented May 19, 2026

Uh oh!

briansrls left a comment

Uh oh!

briansrls commented May 19, 2026

Uh oh!

briansrls commented May 20, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

briansrls commented May 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Issue

Model (docs/coercion-design.md Category 6)

Acceptance criteria

Test plan

Uh oh!

briansrls commented May 19, 2026

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls May 19, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls commented May 19, 2026

Uh oh!

briansrls commented May 19, 2026

Uh oh!

briansrls commented May 19, 2026

Uh oh!

briansrls commented May 19, 2026

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls commented May 19, 2026

Uh oh!

briansrls commented May 20, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

briansrls commented May 19, 2026 •

edited

Loading