Skip to content

Refactor tool acquisition: env node provides resources via edges - #12

Merged
briansrls merged 5 commits into
mainfrom
env-node-tool-acquisition
Jan 31, 2026
Merged

briansrls merged 5 commits into
mainfrom
env-node-tool-acquisition

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Replace implicit requires_tools mechanism with explicit env node that provides ToolHandles via DAG edges. This makes tool acquisition visible in the graph structure and naturally interceptable in DryRun mode.

Key changes:

  • Add path field to ToolHandle for resolved binary location
  • Create EnvOp that upserts tools and emits handles
  • Add runner_env node to CI graph that provides tool:clippy
  • Wire env node to clippy_lint via explicit edge
  • Remove requires_tools field from Node struct
  • Remove acquire_node_tools/acquire_tool from executor

Resources now flow from owners (env nodes) to consumers via edges, following the capability grant model where ownership is explicit and compile-time visible.

claude and others added 3 commits January 31, 2026 20:51
The node_overrides feature was a workaround for mocking non-transport
I/O nodes (e.g., CLI tool ops like clippy_lint) in flow tests. With
the clippy work in progress, this hack is no longer needed.

Removed from:
- BoundaryMocks: field, set_node_override(), get_node_override()
- MockSpec: NodeOverride struct, node_overrides field, builder method
- execute_flat: override check and tool-acquisition skip logic
- CI graph mock: clippy_lint node override usage

https://claude.ai/code/session_01TsKdtxekzTSGmEws3FwZNN
Replace implicit `requires_tools` mechanism with explicit env node that
provides ToolHandles via DAG edges. This makes tool acquisition visible
in the graph structure and naturally interceptable in DryRun mode.

Key changes:
- Add `path` field to ToolHandle for resolved binary location
- Create EnvOp that upserts tools and emits handles
- Add runner_env node to CI graph that provides tool:clippy
- Wire env node to clippy_lint via explicit edge
- Remove requires_tools field from Node struct
- Remove acquire_node_tools/acquire_tool from executor

Resources now flow from owners (env nodes) to consumers via edges,
following the capability grant model where ownership is explicit and
compile-time visible.

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Keep our changes that remove tool acquisition from executor.
The main branch had added node override checks before tool acquisition,
but since we removed tool acquisition entirely, we take our version.

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: ae722314f7

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

Comment thread gunbc-dag/src/ci/env.rs
Comment on lines +60 to +68
for tool_id in &self.tools {
// Look up the tool definition
let tool = get_tool_by_id(tool_id).ok_or_else(|| {
ExecError::new(format!("Unknown tool '{}' in environment", tool_id))
})?;

// Upsert: check if installed, install if needed, get path
let path = upsert_tool(tool)
.map_err(|e| ExecError::new(format!("Failed to acquire tool '{}': {}", tool_id, e)))?;

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Ensure DryRun/Simulate doesn't install tools

EnvOp always calls upsert_tool (check/install) during execution, but execute_flat only intercepts transport-executor nodes, so DryRun/Simulate will still run this I/O and can mutate the environment (e.g., installing clippy) even though the comments state it should be mocked. This makes dry runs side‑effectful and can break CI simulations; consider intercepting EnvOp or wiring mock_env_outputs into the DryRun mocks.

Useful? React with 👍 / 👎.

Comment on lines 164 to 168
/// Run the tool with the given arguments.
/// This is the ONLY way to execute a tool - you need the handle.
pub fn run(&self, args: &[&str]) -> CliToolOp {
CliToolOp::run(self.tool, args)
}

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Use ToolHandle’s resolved path when running tools

ToolHandle::run discards the resolved path and returns CliToolOp::run, which later executes via the tool’s run_cmd on PATH. That means the binary actually executed can differ from the acquired handle if PATH changes between the env node and use (or is shadowed), undermining the capability guarantee the handle is meant to provide. Consider binding the path in ToolHandle::run (or using execute_with_handle) so the resolved binary is actually used.

Useful? React with 👍 / 👎.

briansrls and others added 2 commits January 31, 2026 16:05
- Update CliToolOp::Run execution to use ToolHandle from inputs
- Add has_mock() method to BoundaryMocks for checking specific mocks
- Update docs to reflect env node as I/O boundary
- Update tests to count runner_env as a transport/tool node

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Merged claude/investigate-node-overrides-VShEq which removed node_overrides mechanism.

Key fixes:
- Add consumes_tool_handle() to detect nodes receiving ToolHandle inputs
- Update should_intercept to intercept tool consumer nodes in DryRun
- Add mock outputs for clippy_lint node (success, stdout, stderr, skip)

This ensures nodes consuming ToolHandle (like clippy_lint) are properly
intercepted in DryRun mode instead of trying to execute /mock/clippy.

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
@briansrls
briansrls merged commit 6080aaa into main Jan 31, 2026
1 check passed
@briansrls
briansrls deleted the env-node-tool-acquisition branch January 31, 2026 21:24
briansrls pushed a commit that referenced this pull request Feb 5, 2026
Correctness fixes:
1. HashBuilder now includes path + delimiter + length to prevent
   boundary collisions (e.g., A="ab",B="c" vs A="a",B="bc")
2. Glob errors propagated instead of silently dropped
3. CI "Fresh" check now verifies output files exist (handles case
   where manifest restored from cache but files weren't)
4. Manifest load errors return Error, not Missing (corrupted JSON
   no longer falls back to file existence)
5. Verify mode is strict: missing manifest = fail (can't prove
   freshness without it)

Design issues documented in TODO_hacks for future cleanup:
- #6: Duplicate codegen hash logic (fix with gunbc-infra)
- #8: GUNBC_EXEC_MODE env var bridge
- #9: ResourceHandle forgeable
- #10: ManagedResource::compute_key lacks manifest param
- #11: SimpleResource silent empty hash
- #12: check_state computes keys when entry missing

https://claude.ai/code/session_016pyUtRBESrZGpLuwNX7q1c
briansrls added a commit that referenced this pull request Apr 28, 2026
…pt-5-5-pro reflective)

Director synthesis 2026-04-28 surfaced 5 NEW design considerations from
gpt-5-5-pro reflective + exploratory analyses against main@74b1e46.
Director ask: items (1) and (2) feel critical to land before #1078
promotes since they're foundational to the lens framework declaration.
Items (3), (4), (5) named as cascade items.

==================================================
(1) Lens<C>: monoid-witness inhabitance
==================================================

gpt-5-5-pro Finding #4 (NOVEL): AnalysisDimension<Carrier> at
src/v3/std/dimensions.dag:63-78 already duplicates Monoid<Carrier>
(dsl/std/algebra.dag:108-112 — op + identity) under different field
names. The file documents the monoid law but can't mechanically
enforce it because the monoid witness isn't a field. Lens<C>'s prior
parallel `compose: (C, C) → C` + `unit: C` fields had the same drift.

Fix: replace the parallel pair with structural inhabitance:
  sequential: Monoid<C>     // BindNode composition; structural
                            // inhabitance of Monoid<C> from
                            // dsl/std/algebra.dag:110

Same modeling-discipline move as Q1's Interval<D> consolidation
(feedback_epistemic_stacking — every concept attaches to ontological
DAG; no parallel-rep). Monoid law (associativity + identity) becomes
structurally enforceable; downstream consumers project from
sequential.op / sequential.identity rather than reading two parallel
fields. Future algebraic refinements (CommutativeMonoid for unordered
sequential; Group for invertible composition) attach by extending the
parent.

`branch` stays NOT a monoid op — exclusive choice doesn't require an
identity (no "no-op branch"). It's a standalone (C, C) → C with
max/join semantics. User instances may declare branch: Monoid<C> for
their own use case.

3 worked instances updated to the inhabitance shape:
  - Complexity: sequential = Monoid<SymbolicCost> with op =
    work-additive + span-additive + class-max; identity = zero-cost
  - Tenant-flow: sequential = Monoid<CapSet> with op = set union;
    identity = {} (note: actually CommutativeMonoid since union is
    commutative; framework only requires Monoid)
  - IFC: sequential = Monoid<SecurityLabel> with op = lattice join;
    identity = Public (lattice bottom; refinement is BoundedSemilattice
    via BoundedLattice<SecurityLabel>)

==================================================
(2) SymbolicCost algebra witness
==================================================

gpt-5-5-pro Finding #6 (NOVEL): SymbolicCost has de-facto semiring/
lattice behavior but no declared algebra witness. sequential ≈
additive monoid, iterate ≈ multiplication, branch ≈ lattice meet/order.
Without explicit witnesses, complexity/cost consumers can't compose
generically.

Fix: declare the algebra explicitly in design-lens-framework.md
Instance 1 (cost basis):
  inhabits SymbolicCost : Monoid<SymbolicCost>          // sequential
  inhabits SymbolicCost : JoinSemilattice<SymbolicCost> // branch
  inhabits BigOClass    : BoundedLattice<BigOClass>     // class

The lens framework reads these via Dag::declarations(); the Lens<
SymbolicCost> instance projects from the inhabitance witnesses rather
than free-standing functions.

==================================================
(3) MethodContract consolidation — cascade item
==================================================

gpt-5-5-pro Finding #11 (NOVEL): runtime.dag declares MethodTranslation
{ dag_method, rust_template } AND emit.dag declares SimpleMethodSpec
{ method_name, template, wraps_result } — same fact, different
schemas, ALREADY-DRIFTED templates:
  Rust count: runtime "{recv}.len()" vs emit "({recv}.len() as i64)"
  placeholders: {arg0} (runtime) vs {arg} (emit)
Pattern across Rust/Python/Go = parallel-rep x 3.

Fix: named as substrate-completion sub-lane in design-emission-model.md
§"Cascade across upstream docs" — single MethodContract { dag_method,
runtime_template, emit_template, wraps_result, placeholder_convention }
per-target row in T-Ground-LanguageSpec scope. Method-translation IS
substrate; two parallel authorities violates engine-retraction
discipline directly.

==================================================
(4) Bool inhabits BooleanAlgebra<Bool> dissolution — cascade item
==================================================

gpt-5-5-pro Finding #1+#2: src/v3/compiler/src/bootstrap.rs:91-174
has patch_kernel_bool_boolean_algebra_inhabits because v2 compiler
surface doesn't accept `type … inhabits … =` in dsl/. Comment names
dissolution explicitly.

Fix: named as cascade target in design-emission-model.md §"Cascade
across upstream docs" — when v2 surface lands, declare
`type Bool inhabits BooleanAlgebra<Bool> = True | False`; patch +
operator-resolver fallback retire mechanically. Lane home: T-Ground-
Coercion-Fold (substrate-completion) or future T-Bridge-Retirement.

==================================================
(5) include_str! retirement — cascade item
==================================================

gpt-5-5-pro Finding #12: src/v3/compiler/src/pipeline_authority.rs:
135-178 does include_str!("../pipeline.dag") then line-parses source
text to extract stage names — same fact lives as PipelineStageBinding
data AND as compile-body source-text lines.

Fix: named as R3 T-Bridge-Retirement sub-lane in design-emission-model
§"Cascade across upstream docs" — unified ledger of include_str!
side-channels across the codebase; each instance retires when its
consumer can read the structured authority directly.

==================================================
Items (6)-(8) — Director-owned post-#1078 work
==================================================

These are tracked in PR thread; not in this commit:
  6. Substrate-self-inspection CI gate (INVARIANTS amendment) —
     "every Rust top-level substrate variant has corresponding .dag
     declaration"
  7. Patch ValueBody::List into substrate.dag (urgent integration fix
     per reflective)
  8. Promote FieldMap uniqueness into .dag model

Verification:
  scripts/check-release-doc-authority.sh    → PASS
  scripts/test-check-release-doc-authority.sh → PASS (9 tests)

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 6, 2026
…ition); add STOP #12 for toolchain/edition delta from pin
briansrls added a commit that referenced this pull request May 6, 2026
openai-pro reviewer (PR #1783, on commit 0d1bac6) flagged two
self-contradictions in dispatch authority:

1. **Manager routing R2 vs R3**: line 7 said "R2 Grounding Manager"
   but line 252 + cross-program signal use "R3 Grounding Manager
   (#1745)". Future workers would have conflicting STOP-escalation
   targets. Resolved: line 7 now reads "R3 Grounding Manager (#1745)"
   with explicit absorption note for the R2→R3 rename. All routing
   now targets #1745 consistently.

2. **Allocator-axis single-authority conflict**: line 85 said
   "every collection carrier carries hidden generic parameters
   (allocator A, hasher S) that the brief MUST surface" but line 89
   + STOP #11 say allocator is unstable on 1.86 stable / out of
   scope for Phase 1. Resolved: line 85 reframed as "stable
   parameters at the pinned 1.86.0 toolchain" — hasher is in scope
   (stable), allocator is held under STOP #11/#12 (unstable).
   Authoring an allocator-axis under the stable pin is itself a
   P1 violation (unstable spec fact under stable pin).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 6, 2026
…R-F (#1783)

* WIP: proud-lark-674

* fix(brief): use BoundedInterval shape per HEAD substrate

* fix(brief): replace machine-local path with host-neutral phrasing

* WIP: proud-lark-674

* fix(brief): restrict Never algebra inhabitance to operation-only algebras (no value witnesses)

* fix(brief): drop encoding axis — algebra choice (FreeMonoid<Char> vs FreeMonoid<Byte>) carries encoding per design lock

* WIP: proud-lark-674

* fix(brief): correct manager label to R2 Grounding Manager per live authority docs

* WIP: proud-lark-674

* fix(brief): replace host-local git plumbing language with durable repo/git-prerequisites phrasing

* WIP: proud-lark-674

* fix(brief): fold safety into representation axis; exclude Encoding from §H Step 3 leaves

* WIP: proud-lark-674

* fix(brief): route HashSet/BTreeSet to existing Set<T> = BooleanAlgebra<T> authority per M9

* WIP: proud-lark-674

* WIP: proud-lark-674

* fix(brief): gate Cardinal substrate, split function-item/pointer/closure, escalate Option/Result substrate parent

* WIP: proud-lark-674

* WIP: proud-lark-674

* fix(brief): hash/Ord admissibility axes; route Result via dsl/std/error_primitives; closure FnTrait derived from captures; FnQualifiers as record coords

* WIP: proud-lark-674

* fix(brief): route floats via ApproximateField; expand ReferenceModel rows to full four-axis records; clean stale Option/Result gate cross-ref

* WIP: proud-lark-674

* fix(brief): remove RealizationCost authoring from T-Ground-Rust scope (owned by T-Ground-LanguageSpec)

* WIP: proud-lark-674

* fix(brief): correct closure call-trait derivation per Rust Reference (cumulative tower; move is capture mode not trait selector)

* WIP: proud-lark-674

* fix(brief): align preamble gate list with §F (PR-F sole primary; PR-I/HigherOrder conditional)

* WIP: proud-lark-674

* fix(brief): split impl Trait into argument-position (universal) and return-position (existential) rows per Rust Reference

* WIP: proud-lark-674

* fix(brief): expand FunctionItemIdentity, CaptureSet capture-paths, and ImplTraitReturn opaque_captures per Rust Reference

* WIP: proud-lark-674

* fix(brief): add UniqueImmutableBorrow as fourth CaptureMode per Rust Reference closure types

* WIP: proud-lark-674

* fix(brief): gate float rows on Real/base-carrier STOP; add edition_capture_policy + use<> legality to ImplTraitReturn

* WIP: proud-lark-674

* fix(brief): derive default_capture from edition (illegal-states discipline) — store edition only

* WIP: proud-lark-674

* fix(brief): correct M9 receipt — Float inhabits ApproximateField is comment-only; live float.dag declares Field<Word*>; add Float migration gate

* WIP: proud-lark-674

* fix(brief): float row STOP-gated; ApproximateField is post-gate candidate parent, not dispatchable HEAD consumer

* WIP: proud-lark-674

* fix(brief): remove floats from Phase 1 slice; convert test 6 to STOP assertion; add Float migration gate to STOP #7

* WIP: proud-lark-674

* fix(brief): surface full std-carrier generic signatures (hasher S, allocator A) per extdeps fidelity

* fix(brief): add STOP #11 for non-default hasher/allocator instantiation (Phase 1 default-only scope)

* fix(brief): retarget §F RealizationCost escalation cross-ref (was pointing to STOP #7 = float gate)

* WIP: proud-lark-674

* fix(brief): expand FunctionItemIdentity generic_args (type/const/lifetime); add async_kind axis to ClosurePrimitive (sync vs async tower)

* WIP: proud-lark-674

* fix(brief): closure lends_to_future is derived from captures (not stored); rename is_async to async_kind per manager terminology

* fix(brief): std-carrier trait bounds (?Sized, Allocator, Allocator+Clone); invert closure lending suppression to sync tower; correct impl-Trait edition-affects-lifetimes-only + use<> trait-method legality

* fix(brief): enumerate all five derivation inputs for impl-Trait capture defaults + use<> legality (edition, item_kind, bounds, param kind, required trait generics)

* fix(brief): correct lending semantics — by-value capture by future IS lending; encode deref-projection exception

* fix(brief): use<> precise-capture cannot narrow type/const params (must include all in-scope per Rust Reference)

* fix(brief): structure TraitObjectPrimitive (base_trait/auto_traits/object_lifetime/dyn-compat); expand impl-Trait legality to seven inputs; replace stale grounding-manager:265 line ref

* fix(brief): expand impl-Trait use<> legality to full five-constraint matrix (bound-mentioned lifetimes; anonymous-arg-position forbids use<>)

* fix(brief): bound-mentioned-lifetime constraint covers other return bounds (multi-return signature case)

* fix(brief): pin Rust Reference + std authorities to 1.86 versioned URLs (extdeps fidelity)

* fix(brief): structure authority pin (toolchain + reference + std + edition); add STOP #12 for toolchain/edition delta from pin

* fix(brief): pin §A and §B authority URLs to 1.86.0 versioned bases (clean up two remaining floating URLs)

* fix(brief): drop allocator axis from §B std-carrier rows (allocator_api unstable on 1.86); update STOP #11 to forbid allocator-bearing instantiation under stable pin

* docs(brief): unescape inline-code backticks in T-Ground-Rust brief

Addresses PR #1783 reviewer note: two `\`RealizationCost\`` instances on
line 3 used escaped backticks that render literally in some markdown
viewers. Replaced with plain inline-code spans.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(brief): trait-object base_trait Optional (zero non-auto traits valid)

Reviewer (PR #1783 inline at line 68) correct: Rust Reference §Trait
object types says "not more than one" non-auto trait — zero is valid
(e.g., `dyn Send`, `dyn Send + Sync`). Requiring exactly one base_trait
dropped auto-traits-only trait-object facts under P1/extdeps fidelity.

- §A line 68: base_trait: TraitRef -> Option<TraitRef>; "exactly one"
  -> "at most one (zero valid for auto-traits-only objects)".
- §A line 71: dyn-compatibility check applies only when Some(_); None
  case vacuously satisfied (auto traits are always dyn-compatible).
- §C line 122: TraitObjectPrimitive mirrors the Optional shape +
  vacuous-satisfaction note.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(brief): FunctionItemPrimitive derived trait-inhabitance receipt

Reviewer (PR #1783 inline at line 112 + summary on 44cff1a) correct:
FunctionItemPrimitive carried identity + signature only and dropped
Rust Reference §Function-item-types trait facts (Copy/Clone/Send/Sync
unconditional; Fn/FnMut/FnOnce conditional on unsafe/target_feature/
non-Rust ABI). Downstream grounding lost callable/admissibility facts
under P1/P2.

Added derivation receipt sub-bullet on the FunctionItemPrimitive row:
- Unconditional Copy/Clone/Send/Sync (zero-sized, no captures).
- Conditional Fn/FnMut/FnOnce derived from item_decl qualifiers:
  inhabits all three iff unsafe = false AND abi = Rust AND
  target_feature = None; otherwise blocked.
- Trait-inhabitance is DERIVED not stored (P2; mirrors ClosurePrimitive
  derived-not-stored rule for the same trait family).

Authority pinned: https://doc.rust-lang.org/1.86.0/reference/types/function-item.html

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(brief): per-variant is_copy derivation receipt for C-axis expansion

Reviewer (PR #1783 inline at line 108) correct: pilot's
IntegerPrimitive/NonIntegerPrimitive carry Copy/is_copy facts that live
Rust emission consumers read; only FunctionItemPrimitive had explicit
trait derivation among the new variants. Other new variants
(FloatPrimitive, TextualPrimitive, NeverPrimitive, CompoundPrimitive,
FunctionPointerPrimitive, ClosurePrimitive, ReferencePrimitive,
TraitObjectPrimitive, ImplTraitArgPrimitive, ImplTraitReturnPrimitive)
dropped the fact under P2 facts-flow.

Added "Per-variant is_copy derivation receipt" section after the variant
list with structural derivation for every new variant, citing Rust
Reference §"Copy" + §"Special types and traits" + §"Auto traits"
(pinned to 1.86.0). is_copy is DERIVED not stored on every variant,
mirroring the lends_to_future/fn_traits discipline in ClosurePrimitive
and the FunctionItemPrimitive precedent. Companion is_clone/is_send/
is_sync facts follow the same per-variant rule.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(brief): FunctionPointerPrimitive — FnSignature shape + variadic + HRTB axes

Reviewer (PR #1783 inline at line 120) correct: FunctionPointerPrimitive
delegated to an undefined FnSignature and only named unsafe/abi,
leaving variadic extern signatures (e.g., unsafe extern "C" fn(*const u8,
...) -> i32) and higher-ranked binders (e.g., for<'a> fn(&'a T) -> &'a T)
without a substrate home under P1/P2.

Extended the row with three additions:

1. FnSignature shape pinned: { params: List<Param>, return: ReturnType }
   per Rust Reference §"Function pointer types"; ReturnType distinguishes
   Never from () (the -> ! divergent return is structurally distinct).
   Same type shared by FunctionItem/Closure signatures (not undefined).

2. variadic: Bool axis with cross-axis constraint (variadic = true ⇒
   abi ≠ Rust per Rust Reference §"Variadic functions"; emit-time error
   otherwise). Required to round-trip extern variadic signatures.

3. hrtb: List<LifetimeParam> axis carrying the for<'a, ...> binder list.
   HRTB lifetimes introduce a fresh binder, structurally distinct from
   outer-scope lifetimes — for<'a> fn(&'a T) and fn(&'static T) are
   distinct types and the row MUST distinguish them or P1 fidelity is
   lost.

Authority: https://doc.rust-lang.org/1.86.0/reference/types/function-pointer.html
+ Rust Reference §"Variadic functions" + §"Higher-ranked trait bounds".

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(brief): resolve R2/R3 manager + allocator-axis self-contradictions

openai-pro reviewer (PR #1783, on commit 0d1bac6) flagged two
self-contradictions in dispatch authority:

1. **Manager routing R2 vs R3**: line 7 said "R2 Grounding Manager"
   but line 252 + cross-program signal use "R3 Grounding Manager
   (#1745)". Future workers would have conflicting STOP-escalation
   targets. Resolved: line 7 now reads "R3 Grounding Manager (#1745)"
   with explicit absorption note for the R2→R3 rename. All routing
   now targets #1745 consistently.

2. **Allocator-axis single-authority conflict**: line 85 said
   "every collection carrier carries hidden generic parameters
   (allocator A, hasher S) that the brief MUST surface" but line 89
   + STOP #11 say allocator is unstable on 1.86 stable / out of
   scope for Phase 1. Resolved: line 85 reframed as "stable
   parameters at the pinned 1.86.0 toolchain" — hasher is in scope
   (stable), allocator is held under STOP #11/#12 (unstable).
   Authoring an allocator-axis under the stable pin is itself a
   P1 violation (unstable spec fact under stable pin).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(brief): closure is_copy derivation — UniqueImmutableBorrow blocks Copy

openai-pro reviewer (PR #1783, on commit 9729c35, REQUEST_CHANGES)
correct: ClosurePrimitive is_copy rule put UniqueImmutableBorrow in
the "true" branch, but per Rust Reference §"Closure types" → "Call
traits and coercions" a closure is Copy/Clone iff it does NOT capture
by unique-immutable-borrow OR by mutable reference. This was a
substrate-correctness defect — would mark &uniq-capturing closures
Copy contrary to Rust's own closure trait rules.

Two fixes in one commit:

1. ClosurePrimitive is_copy rule (line 154): "mode = SharedBorrow" only;
   both MutableBorrow AND UniqueImmutableBorrow now block Copy. Authority
   pinned: https://doc.rust-lang.org/1.86.0/reference/types/closure.html.

2. Acceptance test #9 added: behavior-driven coverage of derived
   is_copy + closure-trait correctness with six closure cases (no
   captures, SharedBorrow, MutableBorrow, UniqueImmutableBorrow
   negative, ByValue Copy, ByValue non-Copy) + one function-item case
   (unsafe/extern qualifier blocks Fn-tower). Catches drift in the
   per-variant derivation rules before walker rows land.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: proud-lark-674

* fix(brief): RPIT capture matrix — item_kind-scoped + per-abstract-type

openai-pro reviewer (PR #1783, on commit 251cabb, REQUEST_CHANGES)
correct on two RPIT capture-rule defects per Rust Reference §"Impl
Trait" → "Capturing":

1. **Default capture: edition rule scoped to item_kind** (line 136).
   Old text said "Rust 2015/2018/2021 captures lifetimes only if named
   in trait_bounds" (edition-only rule). The pre-2024 lifetime
   exception applies ONLY to free fns + inherent associated fns/methods.
   Trait methods + trait-impl methods capture ALL in-scope generics
   (type, const, AND lifetime) regardless of edition. Following the
   old rule would under-capture lifetimes on trait-method RPIT rows
   (P1 violation). Default-capture is now derived from
   (edition, item_kind, trait_bounds) jointly, with explicit
   item_kind-by-item_kind enumeration.

2. **use<> legality: per-abstract-type, NOT cross-sibling** (line 139).
   Old text said use<> must include lifetimes from "other return
   bounds in the same function signature" (cross-sibling). Rust
   Reference rule is per abstract return type: each return's use<>
   only needs lifetimes from its OWN bounds. Cross-sibling
   enforcement authors parallel/fictional authority and rejects
   legal Rust signatures (P1/P2). Removed other_return_bounds from
   the input list (was 7 inputs, now 6); rule reframed as
   "lifetimes appearing in THIS abstract type's own trait_bounds".

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(brief): §A RPIT capture summary defers to §C item_kind matrix

openai-pro reviewer (PR #1783, on commit 7f32aec, REQUEST_CHANGES)
correct: when fixing §C in commit 7f32aec, I left §A line 74 with
the old edition-only lifetime-capture rule. §A and §C now disagreed
on the same RPIT lifetime-capture fact — duplicate authority for a
substrate fact (P1/P2 violation).

Resolved at §A line 74:
- "Edition only governs lifetime default-capture" → "Default capture
  is item_kind-dependent, NOT edition-only".
- Pre-2024 lifetime exception explicitly scoped to free fns + inherent
  associated fns/methods only; trait methods + trait-impl methods
  capture ALL in-scope generics regardless of edition.
- §A explicitly defers to §C for the authoritative item_kind-by-
  item_kind matrix.
- use<> constraint #2 also synced to §C: per-abstract-type lifetime
  rule, NOT cross-sibling.

Single authority restored: §C is the source of truth, §A is a
summary that points at it.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(brief): R2/R3 file gap + ReturnType single-authority + AbiKind sum

codex reviewer (PR #1783, on commit 7f32aec, 3 BLOCKING) all valid:

1. **Manager-authority migration gap** (line 4): brief routes to R3
   Grounding Mgr (#1745) but live authority file is named
   r2-grounding-manager.md. Resolved by adding an explicit
   "Authority-file rename pending" note: file rename is
   Director-routed scope (out of this lane); citations to
   r2-grounding-manager.md:NN reference the live HEAD path verbatim
   and remain valid until rename lands; STOP routing already targets
   #1745. Treats the two as a single coordinated authority, not a
   contradiction.

2. **ReturnType = Type | Never duplicated NeverPrimitive** (line 94):
   FnSignature gave `!` a second representation alongside the
   existing NeverPrimitive row (P2 single-authority violation).
   Resolved: ReturnType reduced to `Type`. The `-> !` divergent
   return is a Type whose row is NeverPrimitive. `-> ()` is a Type
   whose row is CompoundPrimitive { kind: Tuple, elements: [] }.

3. **variadic + abi cross-axis precondition violated illegal-states
   discipline** (line 95): variadic: Bool + abi: AbiTag let
   variadic=true ∧ abi=Rust be representable, then relied on
   validation. Resolved: variadic moved INSIDE the AbiKind sum's
   Extern arm. AbiKind = Rust | Extern { abi: ExternAbi, variadic:
   Bool }. The illegal state is now un-representable at the type
   level (P2 / API-level enforcement, not runtime validation).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(brief): Vec<T> M9 parent + lending reads (mode, body_use) jointly

codex reviewer (PR #1783, on commit 007a47c, 2 BLOCKING) both valid:

1. **Vec<T> M9 parent naming** (line 93): Vec<T> row stated only the
   refinement axes (ownership/growability/cardinality) without naming
   its M9 substrate parent first. Per MODELING.md M9 (DFS the concept
   DAG), each row should attach to the existing concept it refines.
   Fixed: Vec<T> now opens with "Inhabits List<T> = FreeMonoid<T>"
   per the M9 substrate parent (consistent with String inhabiting
   FreeMonoid<Char>). Refinement axes follow as narrowing facts.

2. **Lending derivation reads (mode, body_use) jointly** (line 127):
   prior rule classified all UniqueImmutableBorrow captures as
   non-lending. But a &uniq T capture is itself a borrow of an
   &mut T referent — if the future MUTATES through the referent
   (body_use ∈ {mutate, consume}), the underlying mutable place is
   aliased across calls, which is lending. Fixed: lending rule now
   reads BOTH mode and body_use per capture. Three lending triggers:
   - mode = MutableBorrow (any body_use)
   - mode = ByValue (consumed by future)
   - mode = UniqueImmutableBorrow AND body_use ∈ {mutate, consume}
   Non-lending: SharedBorrow (any body_use) or UniqueImmutableBorrow
   with body_use = read only, OR deref-projection exception.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* fix(brief): line-13 manager citation + Phase-1 Q2 overclaim narrowed

openai-pro reviewer (PR #1783, on commit a7c8531, APPROVE_WITH_COMMENTS)
correct on two non-blocking findings:

1. **Line 13 stale manager citation**: cited grounding-manager.md
   (historical, classified as such later in the brief) for the
   two-authority discipline; live authority is r2-grounding-manager.md.
   Fixed: line 13 now cites r2-grounding-manager.md:60-74.

2. **Phase-1 Q2 overclaim**: line 283 said the u128/isize/usize slice
   "Validates PR-F's Q1 + Q2 locks end-to-end" — but Q2 is the
   ReferenceModel<T> pointer/reference axis set, and an integer-only
   slice doesn't exercise any pointer-family row. Fixed: claim
   narrowed to "Validates PR-F's Q1 lock only"; Q2 explicitly noted
   as NOT exercised by this slice (separate slice required).

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 added a commit that referenced this pull request May 6, 2026
Pre-auth queue (#1859): r3-v-pattern-a-tc2-v1-worker.md for gate #12
tc2_church_rosser_executable — deps P1–P6, bold-crane pin, STOP+PING,
dispatch triggers. Index in r3-verification-manager.md.

Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls added a commit that referenced this pull request May 6, 2026
* WIP: R3 Verification

* WIP: R3 Verification

* WIP: R3 Verification

* test(r3-l4): run each claim via run_claim; drop suite OnceLock

Address api-review (PR #1802): cache only the compiled L4 `Dag` and call
`TestRunner::run_claim` per `#[test]` so outcomes are not read from a shared
`Vec<ClaimEvaluation>` populated by whichever test hit the OnceLock first.

Removes unused `L4_SUITE` constant.

Co-authored-by: Cursor <cursoragent@cursor.com>

* docs(tests): clarify OnceLock warm comment; drop PR ref in L4 helper

- T-Demo `a_t_*` doc: serial libtest may warm first; parallel order not guaranteed.
- L4 `l4_run_named_claim` doc: cite TESTING.md only (avoid stale PR # link).

Co-authored-by: Cursor <cursoragent@cursor.com>

* test(t-demo): rename skeleton smoke; drop ordering-based warm-up story

Restore behavior-driven `t_demo_fixture_skeleton_compiles` and document only
the fixture contract plus OnceLock compile amortization (no `a_` prefix /
libtest ordering narrative).

Co-authored-by: Cursor <cursoragent@cursor.com>

* test(r3-l4): assert skeleton suite cardinality without index coupling

Add one `run_suite(L4_SUITE)` test that checks len==3, named membership,
and all Pass — restores suite-shape coverage called out in api-review.

Co-authored-by: Cursor <cursoragent@cursor.com>

* ci: extend self_host_ratchet job timeout to 60 minutes

Cold release builds for v3-compiler (determinism_test + self_host_fixed_point)
can exceed the prior 30m cap on ubuntu-latest when Actions cache misses,
causing mid-compile cancellation and a failing check unrelated to PR logic.

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: R3 Verification

* docs(r3): advance TC1 Q-PAFS brief PROPOSAL → DESIGN

Brian directive 2026-05-06: record engineering path choice (E6-G1.a static
representative first; defer G1.b/X1.b generic; RustDagIsomorphism reorder only
via Director). Update r3-program-plan §10.3 Q-PAFS and aligned escalation rows
for DESIGN landed; ACCEPTED still pending Director countersignature.

Co-authored-by: Cursor <cursoragent@cursor.com>

* docs(briefs): replace bare .md line refs with section anchors (Verification)

Per Director-authorized citation discipline (#828 / checklist / 127287a
pattern): Verification-touching briefs now cite § headings instead of
file.md:NNN for cross-doc pointers.

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: R3 Verification

* docs(r3): fix Codex BLOCKING — L7 matrix cites T-V-L4-L7-Direct; sync Q-PAFS ACCEPTED

- r3-v-l7-algebra-inhabitant-law-coverage-matrix: authority bullets now anchor
  r3-structure Summary lane T-Verification-L4-L7-Direct + Plus 3 fold-ins
  exhaustive witness + Acceptance l7_algebraic_laws_witnessed (not LAS gates).
- r3-program-plan §10.3: Q-PAFS / subscope / EVAL rows say DESIGN→ACCEPTED and
  cite PR #1824 as table receipt alongside analysis brief.
- TC1 analysis brief: canonical ratification = program plan §10.3; ACCEPTED
  footnote updated.
- Add r3-v-pattern-a-tc1-v1-worker.md + link from r3-verification-manager.

Co-authored-by: Cursor <cursoragent@cursor.com>

* docs(briefs): clarify r3-program-plan path for TC1 ACCEPTED authority link

Co-authored-by: Cursor <cursoragent@cursor.com>

* docs(r3): single authority for Q-PAFS ACCEPTED — plan §10.3 at HEAD

openai-pro APPROVE_WITH_COMMENTS: PR #1824 must not read as parallel receipt
vs this PR. Committed docs/r3-program-plan.md §10.3 table is sole source of truth;

Co-authored-by: Cursor <cursoragent@cursor.com>
#1824 is merge-record only.

* docs(briefs): V1 worker — scope line is narrative not second authority

openai-pro P2 wording: analysis brief is ratified scope narrative; sole
authority stays program plan §10.3 at HEAD (Status line).

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: R3 Verification

* WIP: R3 Verification

* docs(briefs): TC1 V1 brief — Director Branch B hold, unpairs argument-opaque E3

Record η non-vacuity ratification: tc1_eta_equivalence_executable stays held until
Q-Reification + ReflectedProgram carrier (or explicit §1.8 revision). Clarify
bold-crane pin excludes TC1 V1 until unblock; Track A otherwise unchanged.

Co-authored-by: Cursor <cursoragent@cursor.com>

* docs(r3): sync §10.3 Q-PAFS/Q-EVAL with Branch B TC1 V1 hold

Codex review on PR #1843: worker brief must not contradict canonical plan.
Record implementation supersession (η non-vacuity + Q-Reification) in
r3-program-plan.md §10.3; subordinate TC1 worker brief to that table (P2).

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: R3 Verification

* docs(briefs): add TC2 Pattern-A dispatch-ready worker brief

Pre-auth queue (#1859): r3-v-pattern-a-tc2-v1-worker.md for gate #12
tc2_church_rosser_executable — deps P1–P6, bold-crane pin, STOP+PING,
dispatch triggers. Index in r3-verification-manager.md.

Co-authored-by: Cursor <cursoragent@cursor.com>

* docs(briefs): add TC3 Pattern-A dispatch-ready worker brief

Pre-auth queue (#1859): gate #13 tc3_pattern_a_second_mover_executable —
two-stage bundle (a)/(b), D1–D6 deps, bold-crane pin, STOP+PING. Index in
r3-verification-manager.md.

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: R3 Verification

* docs(briefs): index tier-1 worker briefs in verification manager

§Sub-briefs listed TC3 but omitted RustDagIso, T-Tests-As-Data V4,
T-LBP partner, and T-LAS execution-split briefs landed alongside it.

Co-authored-by: Cursor <cursoragent@cursor.com>

* docs(r3): align T-LBP Summary, lane table, demos with option (b)

§Acceptance already narrowed T-LBP + gate #83 to complexity+cost; Summary
item 14 and §Lane structure table still described four in-R3 lenses and
full-register closure — conflicting authority vs partner brief (P2).

- r3-structure.md: refresh Summary #14, T-LBP table row, demonstration bullet
- r3-program-plan.md: sync §1.6 companion row + §1.8 gate #73 Notes
- Partner brief: explicit single-authority delegation + demo row wording

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: R3 Verification

* WIP: R3 Verification

---------

Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls added a commit that referenced this pull request May 10, 2026
briansrls added a commit that referenced this pull request May 10, 2026
briansrls added a commit that referenced this pull request May 10, 2026
@briansrls briansrls mentioned this pull request May 10, 2026
5 of 6 tasks
briansrls added a commit that referenced this pull request May 10, 2026
* WIP: R3 gate #12: tc2 church rosser executable

* WIP: R3 gate #12: tc2 church rosser executable

* test(v3): expect Pass for tc2_church_rosser_executable strict-fire suite

Gate #12 runner now evaluates LeftFirst vs RightFirst confluence; update
integration receipt and module docs accordingly.

Co-authored-by: Cursor <cursoragent@cursor.com>

* chore: apply cargo fmt (test_runner import order / wrap)

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: R3 gate #12: tc2 church rosser executable

* WIP: R3 gate #12: tc2 church rosser executable

* WIP: R3 gate #12: tc2 church rosser executable

---------

Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls added a commit that referenced this pull request May 10, 2026
Codex correctly flagged that both projection reports were calling
`evaluate_body(... LeftFirst)` and only differed by `dimension_name` —
that's one evaluation relabeled, not a genuine second-mover comparison.

Route the compare projection through `RightFirst` so the two projections
are genuinely distinct evaluator runs. Strong-normalization on the
embedded `succ(succ(0))` representative is now the load-bearing claim:
under any terminating reduction order, the program reaches the same
top-level `Value`, and disagreement here would be a real
strong-normalization counterexample. This mirrors the gate-#12 TC2
Church-Rosser strategy split (`LeftFirst` vs `RightFirst`).

Updated function doc + §1.8 ledger row #13 wording to make the
distinct-projection semantics explicit.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 10, 2026
…rows #9/#10/#11

Reviewer (claude-opus-4-7 on PR #2648) flagged that the prior status text
on rows #9, #10, #11 carried Director/PM-ratified semantic qualifiers that
must not be silently elided when citing a new slice receipt:

- #9 `l4_emit_eval_match`: §1.7 corpus-quantified rule — slice receipts ≠
  ledger closure; PASSING requires every certification-corpus program.
  Reverted to CONSUMER_LANDED; PR #2585 cited as additional slice evidence.
- #10 `l7_algebraic_laws_witnessed`: PASSING requires exhaustive per-(algebra,
  inhabitant, law) §Acceptance coverage; distributivity / lattice absorption /
  non-AlgebraicLawKind laws remain substrate §P1. Reverted to CONSUMER_LANDED;
  PR #2602 cited as incremental advancement.
- #11 `tc1_eta_equivalence_executable`: Director (a)-disposition 2026-05-09
  held this canvas-deferred past R3 absent #1972 substrate canvas-tier work.
  Reverted to DECLARED-through-R3; PR #2603 cited as scaffold advancement
  but not retiring the canvas-deferral (which would require fresh Director
  ratification).

Other 14 rows in the batch (#12, #14, #31, #43-52, #69) did not carry such
qualifiers and stay flipped to PASSING.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 10, 2026
* R3 gate #13: tc3 pattern a second mover executable

Bounded-runner Pattern-A second-mover bridge analogous to gate-#12 TC2
Church-Rosser: the test runner detects the fixture-local
`tc3_evaluation_step_baseline_dimension_report` /
`tc3_evaluation_step_compare_dimension_report` role pair, evaluates the
embedded `succ(succ(0))` top-level value bind under
`evaluate_body`, and materializes two `DimensionReport::DimensionOk`
projection reports with distinct `dimension_name` keys. Equivalence under
`BinaryDimensionReportEquals` (same `Value`, distinct projection-name keys,
empty witness lists) yields `Pass` for the §1.8 gate-#13 canonical claim
`tc3_pattern_a_second_mover_executable`.

Single forward dissolution trigger: D4 eval-step / bounded-step producer
surface + G1.a static-lens-fold producer-surface-wiring per
`docs/briefs/r3-evaluator-tc3-d4-eval-step-producer-worker.md` — when those
producers land on `origin/main`, this runner arm migrates to live
producer-emitted `DimensionReport<Dag>` values (replacing the proxy
`composed` clone + empty witness lists) without changing fixture or claim
name.

§1.8 ledger row #13 flipped to CONSUMER_LANDED + PASSING; integration test
flips from shape-valid `NotYetImplemented` to `Pass` without fixture edits.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* Address codex REQUEST_CHANGES (#2642): distinct projection runs

Codex correctly flagged that both projection reports were calling
`evaluate_body(... LeftFirst)` and only differed by `dimension_name` —
that's one evaluation relabeled, not a genuine second-mover comparison.

Route the compare projection through `RightFirst` so the two projections
are genuinely distinct evaluator runs. Strong-normalization on the
embedded `succ(succ(0))` representative is now the load-bearing claim:
under any terminating reduction order, the program reaches the same
top-level `Value`, and disagreement here would be a real
strong-normalization counterexample. This mirrors the gate-#12 TC2
Church-Rosser strategy split (`LeftFirst` vs `RightFirst`).

Updated function doc + §1.8 ledger row #13 wording to make the
distinct-projection semantics explicit.

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 added a commit that referenced this pull request May 10, 2026
…2648)

* docs(r3): §1.8 ledger-receipt sync — 2026-05-10 batch (V Mgr lane)

Flip §1.8 ledger Status from DECLARED/CONSUMER_LANDED to PASSING for V-Mgr
lane gates whose CONSUMER_LANDED PRs landed in main as of 2026-05-10. Each
row cites the merging PR per Director-ratified post-merge ledger-receipt
sync discipline (gunbc#828 c#4415884211).

Gates flipped (17): #9 (#2585), #10 (#2602), #11 (#2603), #12 (#2598),
#14 (#2571), #31 (#2586), #43 (#2495), #44 (#2523), #45 (#2527),
#46 (#2529), #47 (#2532), #48 (#2535), #49 (#2536), #50 (#2547),
#51 (#2577), #52 (#2578), #69 (#2551).

Skipped per discipline: #15 (PR #2604 not landed); #35 already PASSING.

Doc-only; no code or test changes. Closes #2640.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): preserve corpus-quantified + canvas-deferral qualifiers on rows #9/#10/#11

Reviewer (claude-opus-4-7 on PR #2648) flagged that the prior status text
on rows #9, #10, #11 carried Director/PM-ratified semantic qualifiers that
must not be silently elided when citing a new slice receipt:

- #9 `l4_emit_eval_match`: §1.7 corpus-quantified rule — slice receipts ≠
  ledger closure; PASSING requires every certification-corpus program.
  Reverted to CONSUMER_LANDED; PR #2585 cited as additional slice evidence.
- #10 `l7_algebraic_laws_witnessed`: PASSING requires exhaustive per-(algebra,
  inhabitant, law) §Acceptance coverage; distributivity / lattice absorption /
  non-AlgebraicLawKind laws remain substrate §P1. Reverted to CONSUMER_LANDED;
  PR #2602 cited as incremental advancement.
- #11 `tc1_eta_equivalence_executable`: Director (a)-disposition 2026-05-09
  held this canvas-deferred past R3 absent #1972 substrate canvas-tier work.
  Reverted to DECLARED-through-R3; PR #2603 cited as scaffold advancement
  but not retiring the canvas-deferral (which would require fresh Director
  ratification).

Other 14 rows in the batch (#12, #14, #31, #43-52, #69) did not carry such
qualifiers and stay flipped to PASSING.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* Merge origin/main into ledger-receipt sync (preserve row #13 update from main)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 12, 2026
Per Director ratification of Q1(a) + Q2(b) (msg_c1daa5ae 2026-05-12):

- dsl/ctrl/README.md — scaffold + path/module/receipt conventions
- docs/briefs/r4-ctrl-migration-pr-digests-worker.md — trio-anchor
  worker brief (catalog #8; smallest Phase 3 footprint)
- Mgr-brief Working-state: Director ratifications recorded; artifact
  index added; full 8-item Wave-1 dispatch queue ordered
  smallest-surface-first

Worker briefs for catalog #10/#16/#14/#12/#11/#3/#5 land in follow-up
PRs (one canonical brief per subsystem per
feedback_one_canonical_subissue_per_workitem.md).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 12, 2026
…#2777)

* docs(briefs): R4 ctrl-migration Subsystem-Modeling Mgr standing brief

Phase 1.5 Mgr-tier standing program for the ctrl/ → .dag migration
(parent program tree authored via PR #2775; landing as DRAFT pending
that PR's merge so authority chain is clean).

Operationalizes project-plan §3 (16-subsystem catalog) / §6 (parallel-
critical-path with staged-debt throttle) / §7 (Wave-1 / Wave-2 dispatch
shape) / §8 (per-worker brief template) as the Mgr-tier standing
program. Carries forward 7 cross-role discipline items from MEMORY.md
that apply to every dispatch this lane fires.

Key load-bearing elements:
- Wave-1-trio checkpoint (per claude #10327): block Wave-2 dispatch
  until one full trio (algebra ✓ + Phase 1.5 PR ✓ + Phase 3 emission ✓)
  converges; recommended anchor = catalog #8 (PR digests) for smallest
  Phase 3 footprint
- Staged-debt budget: 3 unmatched Phase 1.5 stagings pauses dispatch
  (structural enforcement, not soft signal)
- Per-worker brief template: Practice-4 receipts for EVERY enum/sum
  with ≥2 variants (per codex #10331 finding #5, not just open enums)
- Wave-1 / Wave-2 split derived from §3 catalog dependency annotations

Mgr session merry-newt-448 / work-item adhoc-5d3bbf79-ce5.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(briefs): scaffold + trio-anchor worker brief + dispatch queue

Per Director ratification of Q1(a) + Q2(b) (msg_c1daa5ae 2026-05-12):

- dsl/ctrl/README.md — scaffold + path/module/receipt conventions
- docs/briefs/r4-ctrl-migration-pr-digests-worker.md — trio-anchor
  worker brief (catalog #8; smallest Phase 3 footprint)
- Mgr-brief Working-state: Director ratifications recorded; artifact
  index added; full 8-item Wave-1 dispatch queue ordered
  smallest-surface-first

Worker briefs for catalog #10/#16/#14/#12/#11/#3/#5 land in follow-up
PRs (one canonical brief per subsystem per
feedback_one_canonical_subissue_per_workitem.md).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(briefs): apply Emission-Mgr placement correction to trio anchor

Per Emission-Targets Mgr deep-ibex-326 msg_c83099ac 2026-05-12:
dsl/extdeps/github/ owns GitHub-API source-of-record facts only.
PR-digest rendering is gunbc-owned, not an extdep field.

Updates:
- pr-digests-worker brief: Phase-3 partner renamed
  dsl/extdeps/github/digest_render.dag → dsl/gunbc/digest_render.dag
  (consumes dsl/extdeps/github/pulls.dag + dsl/std/render.dag)
- pr-digests-worker brief: explicit DO-NOT placement directive in
  acceptance gate 3 + STOP-criterion clarifies new GitHub source
  carriers must land in extdeps, not gunbc
- dsl/ctrl/README.md: 3-tier placement discipline (extdeps =
  third-party facts; gunbc = rendering/projection/policy; std =
  domain-agnostic primitives) explicit in consumer-receipt rule
- Mgr standing brief Working-state: cross-Mgr ping refs recorded;
  placement-correction memorialized; future worker briefs MUST
  name correct placement before dispatch (standing checklist item)

Direct application of feedback_extdeps_header_discriminator_before_
field_placement.md to this lane. Trio anchor no longer gates on
Emission Mgr's HTTP/SQL PR #2778 — converges via parallel
gunbc-owned render landing.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(briefs+audit): Director template-revise + receipt-trail ledger

Three concurrent Mgr ratifications landed 2026-05-12 in one cycle:

1. Director clever-ant-97 (msg_0707a7c8 + msg_d1589d17) — template
   revise: replace dsl/extdeps/github/digest_render.dag trigger with
   neutral 3-part Phase-3 trigger (digest source-fact authority +
   gunbc/std render projection + named parity harness green); do NOT
   inflate PullRequest with render/digest fields; update STOP
   criterion to route source-fact gaps to Emission, not invent on
   gunbc side.

2. Emission-Targets Mgr deep-ibex-326 (msg_f9d2bfab) — confirms #8
   trio anchor + extdep-gap finding: pulls.dag has PullRequest/
   PullRequestRef/IssueComment but NOT GithubPr/CiState/ConflictState.
   Initial brief invented those names — direct
   substrate-grep-before-authoring miss. Memorialized in Mgr brief
   self-correction + added grep-real-type-names discipline to
   per-worker-brief checklist.

3. Verification Mgr deep-badger-38 (msg_5f8db22f + msg_6faaf178) —
   receipt-trail ledger ratified. Single SoT landed at
   docs/audit/r4-ctrl-phase15-subsystem-receipt-trail.md with 4-tuple
   bool columns, derived open_receipt_debt flag, count≥3 dispatch-
   pause gate, full ownership division (Subsystem-Modeling owns row
   inserts; Verification owns column semantics + parity flips;
   Emission flips phase3_emission_landed). First row (catalog #8
   placeholder) inserted.

PR-digests worker brief revised:
- Module header carries neutral 3-part Phase-3 trigger
- Service-block sketch uses REAL PullRequest carrier from
  dsl/extdeps/github/pulls.dag (verified on main 2026-05-12)
- CI/conflict input facts noted as source-fact placeholders pending
  Emission-Mgr placement (NOT defined on gunbc side; NOT fields on
  PullRequest)
- STOP criterion updated per Director: route source-fact gaps to
  Emission, narrow to existing PullRequest fields, or wait

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(briefs): narrow trio-anchor scope to smaller-first-path

Per Emission-Targets Mgr deep-ibex-326 msg_c5b7d419 2026-05-12 ratification:
take the smaller first path; do not block trio anchor on new CI/conflict/
mergeability carriers; no pull_digest.dag prerequisite.

PR-digests worker brief:
- Carrier-import scope narrowed to existing PullRequest / PullRequestRef /
  PullReview (ListReviews output) / Diff operation output / IssueComment —
  all verified on main 2026-05-12
- Gunbc-side carriers shrunk: MergeReadinessVerdict reasons derive from
  existing fields only (draft/state/merged_at + review states); no
  CI/conflict reason types
- Service block reduced to 4 signatures: extract_attached_urls /
  render_pr_summary_line / merge_readiness_verdict / classify_rest_fallback
- render_ci_digest + render_conflict_digest deferred to follow-up
  Phase 1.5 PR (post-landing only if parity proves load-bearing)
- STOP criterion replaced: do NOT block this PR on CI/conflict source-fact
  placement; surface unrenderable-digest gaps to Mgr as follow-up routing,
  not prerequisite

Mgr brief Working-state: scope-narrow memorialized; removes Emission-side
prerequisite from trio anchor critical path.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(briefs): remove live-file assumption for dsl/std/markdown_render.dag

Per Director clever-ant-97 msg_96a23421 2026-05-12: dsl/std/markdown_render.dag
is NOT on main (verified — only a forward-reference comment in
dsl/std/render.dag mentions it as a future format-specific wrapper).

Citations replaced in both brief files:
- "composing dsl/std/render.dag + dsl/std/markdown_render.dag" →
  "render projection over dsl/std/render.dag; any Markdown-specific
  wrapper is a separate authority decision, not assumed live"
- Director attribution + 2026-05-12 verification date inline

No other behavioral changes; rest of placement correction (source facts
from extdeps.github.pulls, no PullRequest inflation, gunbc-owned digest
projection, receipt ledger shape) remains intact.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(briefs): fix cursor/composer-2 BLOCKING — extdep→gunbc projection

Per cursor/composer-2 review on PR #2777 2026-05-12T20:13Z: two stale
"render-helpers extdep" references in Wave-1-trio rationale sections
contradicted the corrected placement (gunbc-owned render projection,
not extdep) encoded elsewhere in the PR.

- Mgr brief §"Wave-1-trio checkpoint" / Recommended trio anchor:
  "smallest possible Phase 3 deliverable (a render-helpers extdep,
   essentially zero new external authority)" →
  "smallest possible — a gunbc-owned render projection over
   dsl/std/render.dag (proposed dsl/gunbc/digest_render.dag),
   consuming GitHub source facts already in dsl/extdeps/github/pulls.
   dag. Per INVARIANTS P1 + feedback_extdeps_header_discriminator_
   before_field_placement.md: extdeps own third-party source facts;
   rendering/projection is gunbc-owned. The trio's Phase-3 emission
   is NOT an extdep landing."

- PR-digests worker brief §"Wave-1-trio-anchor status":
  "Phase 3 render-helpers extdep ✓" →
  "Phase 3 gunbc-owned render projection over dsl/std/render.dag ✓
   + named parity-harness gate green ✓"
  plus explicit "Phase-3 is gunbc-owned render projection, NOT a new
  extdep" attribution to Director/Emission ratification 2026-05-12

Grep-verified: zero remaining "render-helpers" or "render helpers"
strings across briefs / README / ledger.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(briefs+audit): address operator codex BLOCKING (4 findings, a6bd5f5)

Per operator review on PR #2777 2026-05-12T20:11Z (4 BLOCKING):

#1 Ledger trio gate algebra ambiguity — clarified N/A semantics in
   docs/audit/r4-ctrl-phase15-subsystem-receipt-trail.md: algebra_landed
   ∈ {true, —} is treated as satisfied; only false is unsatisfied.
   open_receipt_debt explicitly does NOT reference algebra_landed (it's
   a per-row receipt, not a global gate). Wave-1-trio gate spelled
   out as the conjunction over the satisfied-set. Admits non-consumer
   trio anchor (catalog #8) without misclassification.

#2 Mgr brief restated throttle predicate — replaced restatement in
   §"Staged-debt budget" with single-source reference to ledger's
   open_receipt_debt + dispatch-pause gate. Mgr enforces; Verification
   owns column semantics; predicate adjustments land in ledger first.

#3 AttachedUrlSource dimensional check miss — split conflated sum
   into two independent coordinates per Practice 4:
   - AttachedUrlContainer: PrBody | IssueCommentBody | PullReviewBody
     | ReviewCommentBody  (source-container dimension)
   - AttachedUrlTextContext: Prose | InlineCode
     (text-context dimension)
   AttachedUrl record now carries both coordinates separately.
   Practice-4 receipts required on both sums.

#4 MergeReadinessVerdict bare-list cardinality — replaced
   NotReady(reasons: List<String>) with structural-cardinality form:
   NotReady { first_reason: String, more_reasons: List<String> }
   The ≥1 invariant is now encoded in the carrier shape; NotReady
   with zero reasons is uninhabitable by construction.

Acceptance gate 2 updated: 4 Practice-4 receipts (was 3) reflecting
dimensional split. Cost-of-change gate updated to cover new variant
additions on both AttachedUrl coordinate sums.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(audit): tighten algebra_landed type to bool | "—"

Reinforces operator-codex BLOCKING #1 (inline at ledger:21) fix landed
in c3eccb3: column type now structurally encodes the N/A admissibility
(was 'bool', now 'bool | "—"') and the evidence cell clarifies that
"—" is a structural assertion of non-consumer-status, not a placeholder
for "unknown". The §"N/A semantics" block remains the authoritative
gate-semantics definition.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(briefs): tighten staged-debt operational-meaning to include parity

Reinforces operator-codex BLOCKING #2 (inline at mgr brief :54) fix
landed in c3eccb3: the §"Staged-debt budget" §-tail operational
paragraph now explicitly states that clearing open_receipt_debt
requires BOTH phase3_emission_landed AND parity_passed (matching the
ledger's predicate exactly), removing the residual "Phase-3 partner"
phrasing that read as ignoring parity. The ledger remains the single
authority for the predicate; this brief defers verbatim.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs: fix competing-authority triggers (operator BLOCKING README:5)

Per operator inline review on PR #2777 dsl/ctrl/README.md:5 2026-05-12
T21:29Z: the README declared trio convergence as the STAGED→AUTHORITY
trigger, while the worker brief header AND the README's own line :3
declared the ctrl-side cut-over (TS deletion) as the authority event.
Two triggers for one authority flip violates INVARIANTS P2/P5 single-
trigger discipline.

Resolution: single-trigger discipline made explicit across all three
files. The ONLY event that flips STAGED → AUTHORITY for a subsystem
is the ctrl PR cut-over (Phase 4) deleting the corresponding TS
files. Trio convergence (algebra + Phase 1.5 PR + Phase 3 emission +
parity) is the *gating precondition* that authorizes cut-over
dispatch, not the authority flip itself.

- dsl/ctrl/README.md §"Authority": rewritten to name cut-over as the
  single trigger; trio as gating precondition.
- worker brief module-header receipt: STAGED → AUTHORITY trigger
  named as the cut-over event; trio reframed as the precondition
  list that authorizes cut-over dispatch.
- Mgr brief §"Wave-1-trio checkpoint": Wave-1-trio convergence
  qualified as "gating precondition for Phase 4 cut-over dispatch,
  NOT itself the STAGED→AUTHORITY flip."

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs: split parity-proof + deletion gates; remove ReviewCommentBody

Two operator BLOCKING findings (codex sha 42218c5 + inline at worker
brief :77) addressed:

#1 (codex BLOCKING / README): tightened §"Authority" to explicitly
   split the two gates by named role, matching the codex framing:
   - Parity-proof gate (readiness): trio convergence; proves the
     .dag substrate can stand in for TS; does NOT itself flip
     authority.
   - Source-authority deletion gate (STAGED → AUTHORITY flip):
     ctrl PR cut-over deleting TS files; only event that flips
     authority; the PR's merge IS the deletion receipt.
   Parity-proof is the precondition for cut-over dispatch; not
   sufficient alone. No overlap window between substrates.

#2 (inline BLOCKING / worker brief :77): AttachedUrlContainer
   widened to include ReviewCommentBody without matching source-fact
   import (extract_attached_urls only takes PullRequest +
   List<IssueComment> + List<PullReview>; no List<ReviewComment>).
   Resolved by dropping ReviewCommentBody from this worker's scope:
   AttachedUrlContainer = PrBody | IssueCommentBody | PullReviewBody,
   one-to-one with the imported source-fact set. ReviewCommentBody
   gates on a follow-up Phase 1.5 PR that adds ListReviewComments
   to imports. Until then no AttachedUrl value can claim a
   ReviewComment source — INVARIANTS P2 single-authority holds.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs: align Wave-1-trio algebra-leg wording with ledger SoT

Per cursor/composer-2 APPROVE_WITH_COMMENTS review on PR #2777
2026-05-12T21:46Z (2 P2 findings + 1 cosmetic):

1. Mgr brief :68 — "algebra ✓ (Phase 1 substrate landed)" omitted
   the ledger's N/A case for non-consumer rows. Rewritten to:
   "algebra_landed ✓ (per ledger N/A semantics: ∈ {true, —} is
   satisfied — non-consumer Wave-1 anchor like catalog #8 satisfies
   this leg with —, does NOT require Phase 1 substrate first)" with
   inline link to ledger §N/A semantics / §Wave-1-trio gate. P2
   compliance: ledger is sole SoT for predicates; brief defers.

2. README §"Authority" parity-proof gate — same shorthand widened
   to ledger-column names + N/A semantics + pointer to ledger as
   single source of truth.

3. Worker brief :39 cosmetic — broken **/doubled-** fixed.

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 added a commit that referenced this pull request May 13, 2026
…nvas:184)

Codex BLOCKING canvas:184: Lifecycle = OnMount | OnUnmount | OnUpdate
classified GREEN but the variants are NOT irreducible — they derive
from UseEffect arm structure:
  OnMount    ≡ UseEffect { body, dependencies: [],     cleanup: None }
  OnUnmount  ≡ UseEffect { body: None, dependencies: [], cleanup: Some(...) }
  OnUpdate(triggers) ≡ UseEffect { body, dependencies: triggers, ... }

Parallel-authority sum violates Practice 4 / P1. Lifecycle reasoning is
a derived projection of UseEffect facts, not its own carrier.

Fix-forward:
- §3 carrier sketch: Lifecycle DROPPED with dissolution receipt comment
- §8 Practice 4 table: Lifecycle struck-through, reclassified RED →
  dissolved; cite codex finding
- §2 audit snapshot: clarify Lifecycle + Effect not introduced
- §11 #12 (new Mgr-derived anti-pattern): forbid parallel Lifecycle sum
  alongside UseEffect

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 13, 2026
* docs(r4): full-stack omni-emission canvas (TS + React substrate)

Director ratified path (b) canvas dispatch via PM msg_83ce8113 relaying
msg_22a1c596 on 2026-05-13. Operator directive: generate full-stack
program from one .dag (Rust backend + TS client + React UI + OpenAPI +
SQL DDL all from single source).

Substrate audit at HEAD: dsl/extdeps/languages/ lacks TS; net-new
substrate authoring. Gate #28 omni_layers_share_one_node_tree CONSUMER_
LANDED + PASSING provides the cross-target invariant extension point.

Canvas surfaces 5 Director-framed questions:
- Q1 TS LanguageSpec shape (parallel-to-Rust vs structural-vs-nominal
  axis on InhabitantDecl); Mgr-rec Q1-b
- Q2 React carrier Shape-A vs Shape-B vs new Shape-F framework-tier;
  Mgr-rec Q2-a Shape-A
- Q3 ingest direction (.dag→JSX vs TS→Component vs bidirectional);
  Mgr-rec Q3-a single-authority
- Q4 cross-target consistency invariant extension (#28 expansion vs
  new gate); Director disposition required
- Q5 lens framework composition (Component as Behavior::Bind vs
  separate substrate-kind); Mgr-rec Q5-a uniform

Practice 4 sketch for new sum types: HookKind 🟡 YELLOW (Custom arm
consumer-evidence-required); others 🟢 GREEN.

R4 phase plan (5 phases) + 6 Director-pending anti-patterns + cost-of-
change accounting (5→1 file per new endpoint).

Hard-bound: canvas-only; NO implementation pre-R3 close. Companion is
Director-owned path (a) visceral 4-layer TODO demo.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r4): R4 full-stack canvas — Director-ratified state (msg_7d51b699)

Director RATIFIED all 6 dispositions on PR #2847 R4 canvas
(msg_7d51b699 via PM msg_1faad154 2026-05-13):

- Q1 RATIFY Q1-b: TypingDiscipline = Nominal | Structural on InhabitantDecl
- Q2 RATIFY Q2-a: Shape-A — components ARE TS source code (Rust/Axum etc.
  symmetric precedent)
- Q3 RATIFY Q3-a: .dag → JSX single-authority
- Q4 RATIFY EXTEND gate #28 (NOT new parallel gate; gate name is
  layer-count-agnostic — parallel gate = INVARIANTS P1 violation)
- Q5 RATIFY Q5-a: Component is Behavior::Bind
- Practice 4 HookKind RATIFY 🟡 YELLOW with R4-Phase-1.5 Practice-4-
  promotion canvas requirement (Mgr authors before Phase-2 dispatch)

Director-added anti-patterns §11 #7-#9:
- #7: Adding TypingDiscipline arms beyond Nominal | Structural without
  ratified consumer evidence
- #8: Custom HookKind in R4-Phase-2 without Practice-4-promotion canvas
- #9: Introducing parallel omni_*_share_one_node_tree gate when invariant
  cashed at gate #28

§10 R4 phase plan extended: Phase-1.5 Practice-4-promotion canvas
inserted between Phase-1 and Phase-2.

§12 reframed Q1-Q5 + Practice 4 as ratified-dispositions audit trail.
§3-§7 "Mgr recommendation" labels reframed as "Ratified disposition".

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r4): R4 canvas — HookKind arm-count framing consistency

Cursor 10817 (APPROVE w/ exploratory): §8 said "7-arm closed enumeration"
while §12 separately framed "6 standard hooks + Custom(Identifier)".
Reframe §8 to match §12: 6 standard-hook arms + 1 user-input boundary
arm. Eliminates two-different-coproduct-sizes reading.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r4): R4 canvas — codex BLOCKING substrate-shape corrections

Codex review d251b61 — 2 BLOCKING findings on R4 substrate sketch:

Finding 1: HookKind incomplete roster.
  Previous: 6 React-18 standard hooks + Custom(Identifier) — under-enumerated.
  Fix: 15-arm closed enumeration of all React 18.3 built-in hooks (authority
  anchor: react.dev/reference/react) — UseState/UseReducer/UseEffect/
  UseLayoutEffect/UseInsertionEffect/UseContext/UseRef/UseImperativeHandle/
  UseMemo/UseCallback/UseDebugValue/UseDeferredValue/UseTransition/UseId/
  UseSyncExternalStore + Custom(Identifier) boundary arm. Dissolution trigger:
  React version-anchor change (new 18.x/19.x built-in) re-ratifies roster.

Finding 2: ComponentBody coproduct treats subcomponents as alternate mode.
  Previous: ComponentBody = Render { jsx: JSXTree } | Composite { sub_components: ... }
  Fix: Component.body IS a JSXTree; subcomponents are JSXNode.ComponentRef
  nodes within the tree, not a separate body mode. Reshape:
    JSXNode = HtmlElement | ComponentRef | TextNode | ExpressionSlot | FragmentNode
  Dissolves the prior Render/Composite split — one render tree with component
  references as tree nodes.

Both findings reflect substrate-shape corrections needed before canvas becomes
R4 worker authority. §8 Practice 4 table + §12 ratification narrative updated.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r4): R4 canvas — cursor 10851 single-authority + sketch typo

Cursor APPROVE_WITH_COMMENTS review 10851 — 2 findings:

1. §6 L226 conflicting guidance: "React UI (new Shape-A or Shape-F)"
   contradicted ratified Q2-a (Shape-A only) + anti-pattern §11 #6.
   Fix: "React UI (new Shape-A per ratified Q2-a; Shape-F explicitly
   REJECTED — see anti-pattern §11 #6)". Single-authority restored.

2. §3 L124 self-referential typo: JSXNode.ComponentRef arm declared
   `component: ComponentRef` (recursive name collision). Rename arm to
   `ComponentRefNode` with field `component: ComponentName` — a distinct
   handle type referencing the named Component, not the JSXNode arm.
   Cascaded rename through §3 comment + §8 Practice 4 table.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r4): R4 canvas — TypingDiscipline fail-closed migration (codex 10864)

Codex REQUEST_CHANGES review 10864: §12 Q1 disposition said
"Rust/Python/Go default to Nominal", which reintroduces convention/
fallback semantics — missing field interpreted as plausible value
instead of failing closed. Violates INVARIANTS P3 + Practice 6.

Fix-forward: tighten migration story across §3 / §12 / §10 / §11:
- §3 Candidate Q1-b body + §3 Ratified disposition: explicit fail-closed
  framing — missing field MUST fail compilation; no implicit default
- §12 Q1 ratified disposition: atomic migration receipt encoded —
  same PR adds carrier extension + sets typing_discipline = Nominal on
  every existing inhabitant + compile-time exhaustiveness test
- §10 R4-Phase-1: fail-closed atomic migration framing inline
- §11 #10 (new Mgr-derived anti-pattern): explicit ban on implicit
  Nominal default for existing rows

The Q1-b ratification stands; only the migration shape tightens to fail
closed per P3.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r4): R4 canvas — cursor 10884 exploratory tweaks

Cursor APPROVE 10884 with 2 exploratory observations:
- L83 Q1-b Cons "lazy migration acceptable" contradicted §12 ratified
  atomic+fail-closed migration. Reworded to match ratified disposition
  + cite anti-pattern §11 #10.
- L313 Q3-a cited "INVARIANTS P1" for single-authority; the
  exactly-one-authoritative-place principle is P2 (Boundary Discipline).
  Fixed citation.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r4): R4 canvas — tighten Cost-of-Change citation (cursor 10898)

Cursor APPROVE 10898 exploratory: §9 cited "INVARIANTS.md Cost of
Change", but the named section lives in CLAUDE.md §"Cost of Change"
(the 1-file-edit-per-extension principle); INVARIANTS.md anchors the
substantive discipline at P2 boundary + P5 progress-is-dissolution.
Reframe citation to point at the canonical CLAUDE.md location + the
INVARIANTS.md principle anchors.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r4): R4 canvas — per-arm HookKind call signatures (codex BLOCKING canvas:76)

Codex BLOCKING canvas:76: Hook.dependencies on the uniform Hook record
let UseState/UseRef/UseContext (which don't take dependency arrays)
carry meaningless dependency facts AND erased the distinct call
signatures of effect/memo/callback/imperative-handle hooks. P1/P2/P6.

Fix-forward: drop uniform Hook.dependencies; move call-signature fields
into each HookKind arm directly per React 18.3 reference. Each arm now
carries exactly the fields its hook takes:
- UseState { initial }
- UseReducer { reducer, initial }
- UseEffect / UseLayoutEffect / UseInsertionEffect { body, dependencies, cleanup? }
- UseContext { context_ref }
- UseRef { initial }
- UseImperativeHandle { ref, factory, dependencies }
- UseMemo { factory, dependencies }
- UseCallback { callback, dependencies }
- UseDebugValue { value, format? }
- UseDeferredValue { value }
- UseTransition  (no args)
- UseId  (no args)
- UseSyncExternalStore { subscribe, get_snapshot, get_server_snapshot? }
- Custom(Identifier)

Hook record reduces to `{ name, kind: HookKind }`. Prior standalone
Effect type dropped (body+cleanup now on UseEffect arm directly).

New anti-pattern §11 #11: call-signature fields on uniform Hook record
are forbidden — they belong on the per-arm carrier.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r4): R4 canvas — dissolve Lifecycle into UseEffect arm (codex canvas:184)

Codex BLOCKING canvas:184: Lifecycle = OnMount | OnUnmount | OnUpdate
classified GREEN but the variants are NOT irreducible — they derive
from UseEffect arm structure:
  OnMount    ≡ UseEffect { body, dependencies: [],     cleanup: None }
  OnUnmount  ≡ UseEffect { body: None, dependencies: [], cleanup: Some(...) }
  OnUpdate(triggers) ≡ UseEffect { body, dependencies: triggers, ... }

Parallel-authority sum violates Practice 4 / P1. Lifecycle reasoning is
a derived projection of UseEffect facts, not its own carrier.

Fix-forward:
- §3 carrier sketch: Lifecycle DROPPED with dissolution receipt comment
- §8 Practice 4 table: Lifecycle struck-through, reclassified RED →
  dissolved; cite codex finding
- §2 audit snapshot: clarify Lifecycle + Effect not introduced
- §11 #12 (new Mgr-derived anti-pattern): forbid parallel Lifecycle sum
  alongside UseEffect

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 added a commit that referenced this pull request May 13, 2026
…b80bcaa8)

Director RATIFIED Option B on Q6 zero-degree Practice-2 tension via
msg_b80bcaa8 (relayed by PM msg_9d248cbd 2026-05-13). Practice-2
carrier-level `where nonzero` refinement preferred over Practice-4
canonicalize-fold dissolution; sign-admission intent preserved.

Director-distilled discipline rule (NEW, load-bearing):
> Same-variant redundancy → Practice-4 collapse (Q2-Y LinearCost ≡
> PolyCost(d=1)). Cross-variant redundancy → Practice-2 carrier
> refinement (PolyCost(d=0) ≡ ConstantCost(1)). Type-level state-space
> tightening beats API-level normalization when redundant state crosses
> variant boundaries.

Canvas + worker fix-forward:
- §1 PROMOTE / §3 Q2-Y candidate / §6 STOP-SIGNAL / §6.1 dissolution
  text: `Rational` → `Rational where nonzero` (sign-admission via msg_2c1bfb0e
  preserved; only degree=0 excluded)
- Canvas §6.1: reframed from canonicalize-fold to carrier-level
  refinement; Practice-2 vs Practice-4 disambiguation rule encoded
- Worker §5 Phase A KNOWN_PREDICATES list: add `nonzero` predicate
  (allowed_carriers: Rational; arg_shape: Bare); now 2 new predicates
  (gt_one + nonzero), not 1
- Worker §5 "ZERO new authority" line: cite cross-variant vs
  same-variant rule
- Worker §6 algebra table: canonicalize-fold rule REMOVED (type prevents
  construction); multiplicative cancellation rule split into d1+d2≠0
  and d1+d2=0 cases (=0 maps to ConstantCost(1) directly without
  PolyCost(d=0) intermediate which is type-rejected)
- Worker §7 bootstrap ratchet: type-rejection negative test added
  (PolyCost(_, Rational(0)) must be structurally rejected; ±n admits)
- §11 anti-pattern #12 (new, Director-added): forbid canonicalize-fold
  for cross-variant redundancy when carrier refinement available
- AP cite-list counts: 11 → 12 across §11 header / §12 / §13 / §15

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request May 13, 2026
* docs(briefs): S6 brief fix-forward — authority chain corrected per codex BLOCKING review on PR #2782 sha b28cf88

Earlier brief mis-cited high-level T-WAD substrate-shape framing; codex caught that the actual implementation authority for affected-set selection is:
- PR #2713 (upstream affected-set lens substrate; merged) per docs/design-affected-set-lens.md §2
- docs/design-t-wad-slice-7-binary-shim-affected-set-selection-canvas.md in main (§1 BinaryShim consumption / §3 fail-closed / §4 selection algorithm / §5 path-regex removal invariant)
- PR #2766 harness contract + Layer 2 path-regex inventory ratchet

§0 + §1 rewritten to encode the correct authority chain, canvas §4 algorithm verbatim, and canvas §5 path-regex removal invariant. STOP conditions tightened to the actual fail-closed surfaces (PR #2713 serialization form, path-regex inventory drift).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(briefs): S6 brief — surface 2-layer decomposition per canvas §6-§7 staging (substrate prerequisite + BinaryShim consumer/runner) — swift-wren-365 msg_29f68109

Earlier draft compressed both layers into one PR. swift-wren-365 surfaced (correctly) that PR #2798 in-flight is Layer 1 substrate (closure+topo over CIWorkflowDag + CiWorkflowDiff) — Layer 2 (BinaryShim consumer of PR #2713 lens output + TestClaim D(t)/Δ(t) mapping + canvas §5 path-regex removal) is a follow-on PR depending on Slice 5 BinaryShim hook per canvas §6-§7.

§1 reframed as two-layer decomposition with explicit scope boundaries. Phase A-C explicitly scoped to Layer 2. Layer 1 in-flight under PR #2798 not in this brief's scope.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(briefs): S6 brief §4 PR-body framing + §6 reference list harmonized with §1 canvas-vs-PR-#2766-harness split — cursor APPROVE 10477 exploratory note

§4 PR body framing now distinguishes three authority types: canvas (BinaryShim consumption + selection algorithm + path-regex removal) + upstream lens (PR #2713 / design-affected-set-lens.md) + harness/ratchet (PR #2766). §6 reference list expanded similarly. Removes the residual 'PR #2766 substrate authority' phrasing that conflicted with §1's three-source split.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #62 file-ingestion substrate-shape canvas

Surfaces the substrate-shape question for §1.8 row #62
substrate_gap_file_ingestion_closed before brief authoring.

bright-otter-731 was auto-spawned on this gate without an
authored brief and surfaced a clean audit (no include_str! at
HEAD in dsl/; PR #2819 read_utf8_file candidate shape held in
draft). §4.3 line 505 frames closure as workflow_substrate
extension to file-attachment (Candidate B), but PR #2819 implements
compile-time UTF-8 read (Candidate A) — parallel-authority risk.

This canvas frames the candidate shapes (A/B/C/d) for Director-or-
Substrate-Mgr-tier ratification before brief authoring proceeds.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #62 FileAttachment carrier-internals sub-canvas

Director ratified Candidate (b) on PR #2820 — workflow-substrate
FileAttachment carrier extending #53 — per PM msg_52c4a707. This
sub-canvas surfaces carrier internals (type def + fields + workflow
coupling + Practice 4 + lazy-vs-eager) for next-tier ratification
per recursive feedback_substrate_shape_belongs_in_mgr_canvas.

Three candidate shapes (B-1 minimal / B-2 path-keyed / B-3 anchor+entry
pair) anchored against gate #55 WorkflowObservationAnchor precedent at
src/v3/std/timing_lens.dag:98 (already CONSUMER_LANDED).

Director anti-patterns encoded for worker review enforcement.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #62 FileAttachment worker brief (Refined-B-1 ratified)

Director ratified Refined-B-1 carrier shape with full §8 Q1-Q6
dispositions + 7 anti-patterns per PM msg_bc8c23f6 (relaying Director
msg_61e302c6). Worker brief authored with:

- Exact 5-field carrier (subject_node + content_digest + producer_id +
  workflow_run_id + attached_at_ns) — strict 5-of-7-subset of #55
  WorkflowObservationAnchor
- Q1-Q6 dispositions encoded verbatim for reviewer enforcement
- 7 anti-patterns receipt-of-compliance requirement
- Phase A (carrier) / Phase B (ratchet test) / Phase C (existence-proof
  use case) / Phase D (ledger update) staging
- 5 STOP conditions including consumer-evidence-blob-store gap
- Workflow blob-store substrate flagged as Wave-2 sub-canvas-2 trigger
  (forward-looking, NOT blocking this brief)

Brief is DISPATCH-READY. PR #2819 stays held as Candidate A drift
(anti-pattern #1).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 SymbolicCost Tier 1 carrier-extension canvas

Director ratified Path A Tier 1 on 2026-05-13 (PM msg_4fd650b7
relaying msg_ad5e934d) with 5 sub-canvas questions Q1-Q5 routed
to Mgr. This canvas surfaces dispositions on each for next-tier
ratification before worker brief authoring.

Mgr recommendations:
- Q1 Rational ordering: c (layered OrderedField + lazy migration)
- Q2 Linear-vs-Polynomial: Y (collapse to PolynomialCost(degree=1)
  per §P5; net 10 variants not 11)
- Q3 algebra rules: tabulated 10 new interaction rules; PolyLog
  reserved for log^k only (n log n stays composite); Factorial²
  = UnknownCost (Tier-2 R4-deferral receipt)
- Q4 STOP SIGNAL: re-resets at 11th variant (or 12th if Tier-2)
- Q5 carrier-shape canvas: this document
- §8 Tier-2 mechanism: defer to R4 (InverseAckermann doesn't
  fit IteratedAlgebra; no uniform compositional surface)

5 Director anti-patterns encoded + 2 Mgr-derived for worker review.

Gates on §1.8 row #105 PR #2824 landing + Director ratification of
§12 questions before worker dispatch.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 SymbolicCost Tier 1 worker brief (canvas ratified)

Director ratified canvas PR #2828 Q1-Q5 + §8 Tier-2 disposition per
PM msg_a055c38b relaying msg_d86a5987. Worker brief encodes ratified
shape as single coordinated PR with 7 sub-phases:

- Phase A: OrderedField<T> witness landing + Rational re-declaration
- Phase B: STOP SIGNAL rewrite (cap at 11)
- Phase C: SymbolicCost carrier reshape (Q2-Y collapse Linear)
- Phase D: algebra interaction rules (13-rule table; §5.1 composite
  for poly·log; §5.2 (n!)² → UnknownCost verbatim)
- Phase E: bootstrap ratchet test
- Phase F: cost-lens consumer migration (LinearCost → PolyCost(d=1))
- Phase G: §1.8 row #105 ledger update

7 anti-patterns + 5 reviewer ratchets + 6 STOP conditions encoded.
DISPATCH GATES on PR #2824 (row anchor) AND PR #2828 (canvas) both
merged; brief is ready when cascade clears.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 — encode invariants in type carriers (codex BLOCKING fix)

codex BLOCKING #10726 on PR #2828 (Practice 2 + Practice 6 violations):
1. Worker brief moved invariants (degree>0, exponent≥1, base≥2) into
   fold normalizer instead of carrier — admits illegal states
2. Canvas §187 said 'Rational ≥ 0' while worker said 'degree > 0' —
   split authority on the invariant

Both findings valid. Fix:

Canvas §6 STOP-SIGNAL text:
- Replaced 'PolynomialCost(Rational ≥ 0)' with 'PolynomialCost { degree:
  PositiveRational }' + adds PolyLogCost { exponent: PositiveInt } +
  ExponentialCost { base: IntAtLeastTwo } verbatim
- Adds new "Type-level refinement carriers" subsection citing
  DegreeAtLeastTwo precedent (algebra.dag:171-173)

Worker brief §5:
- New §5.0 introduces PositiveRational, PositiveInt, IntAtLeastTwo as
  Peano-style inductive carriers (strict-mirror of DegreeAtLeastTwo)
- §5.1 SymbolicCost now uses these refinement types for fields:
  PolynomialCost.degree: PositiveRational
  PolyLogCost.exponent: PositiveInt
  ExponentialCost.base: IntAtLeastTwo
- Removed the "refinements live in fold normalizer" paragraph

Illegal states (degree≤0, exponent≤0, base≤1) now structurally
unrepresentable per Practice 2 + Practice 6.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 — fix variant arithmetic 10 → 9 per operator BLOCKING

Operator BLOCKING on PR #2828 canvas:135 caught real arithmetic error:
Q2-Y removes LinearCost (-1) and adds 3 NEW variants (PolyLogCost +
ExponentialCost + FactorialCost), so net is 7 - 1 + 3 = 9, not 10.
PolynomialCost is PROMOTED (degree type changed Rational), NOT added as
a new variant — that was the counting mistake.

Confirmed variant set per canvas §6 + worker §5.1:
1. ConstantCost
2. PolynomialCost { degree: PositiveRational }
3. PolyLogCost { exponent: PositiveInt }
4. LogCost
5. ProductCost
6. SumCost
7. ExponentialCost { base: IntAtLeastTwo }
8. FactorialCost
9. UnknownCost

Total: 9 variants. Confirmed.

All references updated:
- "10 variants" → "9 variants"
- "11th variant" → "10th variant" (STOP-SIGNAL trigger threshold)
- "Net 7 → 10/11" → "Net 7 → 9"
- "variant cap at 11" → "variant cap at 10"
- "10 ratified + 1 trigger" → "9 ratified + 1 trigger"
- "STOP-SIGNAL re-reset to 11" → "STOP-SIGNAL re-reset to 10"

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 — Q1 premise correction per operator BLOCKING canvas:48

Operator BLOCKING #2 on PR #2828 canvas:48 caught real authority error:
Field<T> at dsl/std/algebra.dag:294 ALREADY has compare: fn(T,T)->Ordering.
The canvas claim "Rational supports add+mul+inverse, NOT order" was wrong —
Field carries the foundational order primitive. Introducing OrderedField<T>
would create parallel order authority.

This invalidates the original Q1-c ratification premise (PM msg_a055c38b).
Q1 disposition needs RE-RATIFICATION:

Revised candidate set (canvas §3 REVISED):
- Q1-α (Mgr-rec): use existing Field.compare via Rational; lt/le/gt/ge as
  cost-lens-local free functions. Zero new substrate.
- Q1-β: extend Field<T> in-place with 6 derived predicate fields. Larger
  blast radius; mirrors OrderedRing predicate set on Field directly.
- Q1-γ: OrderedField as Field-superset via type-level inheritance. Requires
  DSL grammar prerequisite (worker grep-verifies).

Worker brief Phase A regenerated under Q1-α assumption (smallest scope):
- NO OrderedField type introduction
- NO Rational re-declaration
- Cost-lens-local rational_lt/le/gt/ge/max helpers derived from
  rational.compare (existing Field operation)

Anti-pattern #6 reworded: "Parallel order authority — adding any new
OrderedField or equivalent witness when Field.compare already exists at
algebra.dag:294 (Q1 premise-corrected anti-pattern)".

Canvas + worker brief both note re-ratification required; if Director
prefers Q1-β or Q1-γ, Phase A regenerates.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 — fix unsound multiplicative absorption rules per operator BLOCKING worker:140

Operator BLOCKING caught real asymptotic-analysis error: multiplicative
absorption rules like `PolyCost(d) · ExpCost(c, v) = ExpCost(c, v)` are
UNSOUND. n^d · c^n / c^n = n^d is unbounded as n → ∞, so n^d · c^n is
NOT O(c^n) strictly. Same problem with FactorialCost · PolyCost and
FactorialCost · ExpCost.

Fix: multiplicative absorption rules removed; replaced with composite
ProductCost retention:
- PolyCost(d) · ExpCost(c, v) → ProductCost([PolyCost(d), ExpCost(c, v)])
- FactorialCost(v) · PolyCost(d) → ProductCost([FactorialCost, PolyCost(d)])
- FactorialCost(v) · ExpCost(c, v) → ProductCost([FactorialCost, ExpCost])

ADDITIVE dominance rules unchanged (those ARE sound — n^d + c^n = O(c^n)
because dominant term wins; only multiplicative absorption is unsound).

Both canvas §5 + worker brief §6 rule tables updated.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 — Q1-α Director-RATIFIED; add 6th anti-pattern

Director re-ratified Q1 to Q1-α per msg_676ad4e7 (supersedes
msg_d86a5987 Q1-c), retraction explicit. Updates:

Canvas + worker brief §3:
- "PENDING re-ratification" framing removed
- Q1-c rejection cites INVARIANTS P1 + row #24 + Q-MachineConstraint-Carrier
- Q1-β + Q1-γ rejections documented (Director rationale verbatim)

Anti-patterns:
- NEW Director-ratified #6: "Introducing parallel ordered-algebraic-structure
  carriers (Ordered<X>) when underlying carrier already provides compare:
  fn(T,T) -> Ordering"
- NEW Mgr-derived #7: "Multiplicative absorption rules where one variant
  absorbs another asymptotically" (operator BLOCKING worker:140 retained as
  permanent anti-pattern receipt)

Canvas: 6 Director + 2 Mgr-derived = 8 total
Worker brief: 8 anti-patterns total (matches canvas)
PR body framing template + reviewer ratchet count updated 7 → 8

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 — refinement types for PolyLogExponent + ExponentialBase per operator BLOCKING PR #2824:333

Operator BLOCKING #4 on PR #2824 (relayed via PM msg_92bc8538):
- PolyLogCost { exponent: Int } admits exponent=0 (ConstantCost dup),
  exponent=1 (LogCost dup), negative; cannot represent log^7.5 (AKS
  Tier-1 case)
- ExponentialCost { base: Int } admits base=0/1 (degenerate/ConstantCost)
- Same Practice 2/6 illegal-states-unrepresentable class as prior codex
  BLOCKING (commit 3d21cb7)

Fix:
- NEW refinement carrier ExponentialBase (Int ≥ 2; renames IntAtLeastTwo
  to PM-ledger naming per row #105 commit 8049ccd)
- NEW refinement carrier PolyLogExponent (Rational > 1; admits 7.5/AKS)
- PolyLogCost.exponent: PositiveInt → PolyLogExponent
- ExponentialCost.base: IntAtLeastTwo → ExponentialBase
- PositiveRational unchanged (PolynomialCost.degree already correctly
  bounded > 0 by this carrier)

7th Director-pending anti-pattern added: "Tier-1 variant constructed
with raw Int/Rational bypassing refinement type" (matches PM's row #105
ledger 7th anti-pattern per PR #2824:8049ccde4).

Updated counts:
- Canvas §10: 6→7 Director + 2 Mgr-derived
- Worker brief §11: 8→9 anti-patterns total

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 worker brief — pre-wire P5 receipt requirement per claude APPROVE 10773

claude review 10773 exploratory observation (non-blocking): when worker
authors symbolic_cost_tier1_carrier_test.rs, INVARIANTS P5 requires
explicit single checkable receipt (deletion / SG-0 census shrink /
named-lane deferral) in PR body. Pre-wire so worker doesn't re-derive.

Added §13 verification bullet: canonical receipt is Phase F cost-lens
consumer migration (deletes LinearCost variant + collapses fallback
dispatch paths) — that net hand-Rust deletion is the P5 receipt for the
new test file.

Also corrected refinement carrier name list (was: PositiveRational/
PositiveInt/IntAtLeastTwo; now: PositiveRational/PositiveInt/
ExponentialBase/PolyLogExponent matching the post-d93e2eaffe naming).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 worker brief — address codex BLOCKING 014544f findings 2/3/4

codex review 014544f surfaced 4 BLOCKING findings (sha pre-d93e2eaffe).
Findings 1 + partial-2 covered by intervening d93e2ea (refinement
types). Residual findings 2/3/4 addressed in this commit:

Finding 2 — refinement-mixed-with-product on PolyLogExponent:
- Previous shape was `{ numerator, denominator }` with textual "numerator
  > denominator" invariant — exact refinement-mixed-with-product pattern
  codex forbids
- New inductive shape: PolyLogExponentSuccessor | PolyLogExponentFractional
  with FractionalPart in (0, 1] structurally; whole ≥ 1 + fraction > 0
  yields value > 1 by carrier shape
- HARD STOP added: do NOT author as record-with-comment-invariant
- Worker grep-verifies DSL refinement support; if not available, ratify
  inductive shape pre-authoring

Finding 3 — cross-variable dominance gap:
- §6 algebra rules table prefaced with explicit "Variable-scoping
  precondition" — rules assume same-variable operands; different-variable
  operations preserve as SumCost/ProductCost composite, not folded by
  dominance
- Cross-variable dominance explicitly named undefined within Tier-1
  substrate (Tier-2 / polynomial-multivariate scope post-R3)

Finding 4 — P5 receipt category specificity:
- §13 verification bullet now requires "exactly ONE P5 receipt category
  with concrete path + LOC count" (not narrative)
- 3 categories enumerated: (a) hand-Rust deletion + LOC; (b) SG-0 census
  shrink + delta; (c) T-PB-B ROADMAP row + dissolution-trigger
- Phase F LinearCost removal noted as LIKELY (a) source but worker MUST
  measure actual numbers, not assume narrative-equivalence

Finding 1 (refinement-over-existing-Rational vs fresh records) surfaces a
refinement-mechanism canvas question; routed to PM/Director (no fix in
this commit; the residual product-shape for PositiveRational is preserved
pending Director disposition on substrate-refinement-mechanism).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 — fix FactorialCost dominance over-reach per operator BLOCKING worker:158

Operator BLOCKING: 'FactorialCost(v) + anything = FactorialCost(v)' rule
would erase UnknownCost (conservative-top) and incomparable SizeVariable
dimensions, violating P2/P3.

Fix: expand FactorialCost addition rule from single 'anything' catch-all
to per-variant explicit enumeration:
- FactorialCost + same-variable cost (Factorial/Exp/Poly/PolyLog/Log/
  Constant) → FactorialCost (absorption valid)
- FactorialCost + UnknownCost → SumCost composite (UnknownCost is
  conservative-top per algebra.dag; NEVER absorbed)
- FactorialCost + FactorialCost different-variable → SumCost composite
  (cross-variable undefined per §6 precondition)

Same-variable precondition from prior commit (c787f75 finding #3 fix)
now explicitly applied per-rule for the FactorialCost row.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 — refinement mechanism IS ratified; reshape carriers per PM msg_a52ed981

PM-grep correction (msg_a52ed981): substrate refinement-mechanism `type
X = Y where predicate` is ALREADY RATIFIED at HEAD per gunbc#828
issuecomment-4390333451 Path 3 + Director Option 2. Mgr missed grep-
verifying this when authoring path (i)/(ii) framing — same discipline
class as feedback_grep_substrate_before_naming_ratification.

Precedent: dsl/std/integer.dag:181 (`PositiveInt = Nat where gt_zero`).
KNOWN_PREDICATES registry at lower.rs:798-862:
  range / non_empty / brand / gt_zero / unicode_scalar

Reshape (worker brief §5.0 + canvas §6):
- PositiveRational = Rational where gt_zero (REQUIRES gt_zero
  allowed_carriers extension to include Rational — Phase A atomic)
- ExponentialBase = Int where range(min: 2) (IMMEDIATELY available;
  range predicate has Int in allowed_carriers)
- PolyLogExponent = Rational where gt_one (REQUIRES NEW gt_one
  predicate; allowed_carriers Rational + Int; mirrors gt_zero shape;
  Phase A atomic)
- PositiveInt reuses existing dsl/std/integer.dag:181 declaration

ZERO new authority introduced. P1 single-authority + Practice 4 + Q-
MachineConstraint-Carrier "no dual representations" all satisfied via
refinement over canonical Rational/Int carriers.

NEW Mgr-derived anti-pattern #8 added: parallel rational-number
carriers when refinement-mechanism is available (PM-grep-corrected per
msg_a52ed981 + codex 014544f finding #1).

Phase A KNOWN_PREDICATES extensions:
1. gt_zero allowed_carriers + Rational
2. New gt_one predicate (Rational + Int; Bare arg)
Both atomic with carrier landing per §P5.

HARD STOP added: do NOT author fresh records/inductive sums when
refinement is available.

Anti-pattern counts: canvas §10 → 7 Director + 3 Mgr-derived = 10;
worker brief §11 → 10 anti-patterns total.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 canvas/worker — cursor 10801 stale-cite cleanup

Cursor review 10801 (PR #2828) — 6 stale-ratification cites cleaned to
the Q1-α / 9-variant ratified state:

Canvas (PR #2828):
- L13-14 front matter: Field<T>/Rational "no order" → carries compare
  (Director ratified Q1-α via existing Field.compare; line ref :287→:294)
- §6 L216 variant count: "10 post-Q2-Y" → "9 post-Q2-Y" (matches §5 L153
  and Q2-Y disposition; PolynomialCost.degree promotion is not a new
  variant)
- §6 algebra bullets: Q1-c OrderedField.add/compare → Field.add/compare
  on Rational + rational_max lens-local helper (Q1-α)
- §12 Q1 Mgr-rec: stale "c — OrderedField" replaced with full ratified
  Q1-α/Q2-Y/Q3/Q4/Q5/§8 disposition block as audit trail
- §13 reference list: Field<T> "no order" + Q1-c cite → Q1-α via compare

Worker brief:
- §7 phase E receipt: "10 variant count" / "All 10 variant names" → 9
- §10 STOP #3: "Q1-c re-declaration target" → "Q1-α refinement target"
- §14 out-of-scope: "Q1-c lazy migration" → Q1-α (Field unchanged)
- §15 PR body template: "Companion substrate (Q1-c)" → (Q1-α)
- §11 anti-patterns: duplicate #8 numbering fixed → renumber to 1-10
- §16 reference: feedback_strict_mirror Q1-c → Q1-α discipline

INVARIANTS P2 single-authority restored across both briefs.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 canvas — fix §10 Mgr-derived duplicate #8 numbering

Per claude/claude-opus-4-7 review 10819 cosmetic note: Mgr-derived
anti-patterns had 7,8,8 → renumber to 8,9,10 (continuing from
Director-enumerated 1-7). Matches the §11 worker brief enumeration.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 worker — fix Phase E sample-test multiplicative absorption

Codex REQUEST_CHANGES review 10837: worker brief §7 line 225 sample test
asserted ExpCost(2,n) · PolyCost(d) collapses to ExpCost(2,n), which
contradicts §6 algebra + anti-pattern #9 (multiplicative cross-class
absorption is unsound; only ProductCost composite is correct).

Fix-forward: corrected sample to assert ProductCost composite under
multiplication; added the additive-sound sibling test (ExpCost + PolyCost
DOES absorb to ExpCost) so both directions of the SUM-sound vs
PRODUCT-unsound asymmetry are receipt-tested.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 canvas — codex 10852 two contradictions in dispatch artifact

Codex REQUEST_CHANGES review 10852 — both findings load-bearing:

1. §5 L172 FactorialCost rule: "FactorialCost(v) + anything = FactorialCost(v)"
   contradicted worker brief's per-variant rules (preserve composites for
   UnknownCost + cross-variable FactorialCost(w)). Expanded canvas table
   to match worker:
   - Same-variable Tier-1-below: absorb to FactorialCost(v)
   - Cross-variable FactorialCost(w): SumCost composite
   - + UnknownCost: SumCost composite (conservative-top, never absorbed)
   - + SumCost/ProductCost composites: distribute and re-fold per §6
   Mirrors operator BLOCKING #5 fix to worker brief (commit adb8417).

2. §5.1 L183 n log n shape: "ProductCost([LinearCost(n), LogCost(n)])"
   reintroduced the LinearCost variant dissolved by ratified Q2-Y.
   Corrected to "ProductCost([PolynomialCost { var: n, degree: 1 },
   LogCost(n)])" — post-Q2-Y collapse via PolynomialCost(degree=1).

INVARIANTS P2 single-authority restored across canvas + worker for both
fold rules. Anti-pattern §11 #10 (LinearCost-consumer paths preserved)
no longer self-violated by the canvas guidance.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 worker — reconcile authority chain (codex 48328e4)

Codex BLOCKING review sha 48328e4: worker brief frontmatter / authority
chain / §9 ledger update / §15 PR body template cited the pre-Q1-α
ratification msg_d86a5987 alone, without msg_676ad4e7 (Q1-α supersession)
reconciliation. The substantive carrier + algebra fixes were clean but
the authority chain leaked the superseded shape.

Fix-forward: every load-bearing authority cite (frontmatter, §0 status,
§2 inputs ratification line, §4 cite-in-comment-block, §9 row-#105 ledger
update text, §13 PR body cite list, §15 PR template, §16 reference) now
cites the **composite ratification**:

  PM msg_a055c38b relaying Director msg_d86a5987 (Q2-Q5 + §8 base)
  RECONCILED BY Director msg_676ad4e7 (Q1-α supersedes prior Q1-c)

Worker dispatches on this composite — not the pre-Q1-α msg_d86a5987 alone.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 — Director scope-extension msg_2c1bfb0e (signed Rational)

Director RATIFIED scope-extension on PR #2828 (msg_2c1bfb0e via PM
msg_e5ed6db8 2026-05-13) per operator directive: PolynomialCost.degree
admits signed Rational (arbitrary roots + inverse/decay coverage), no
where-refinement. Q6 dominance ordering + Q7 SymbolicCost preserves full
expression both ratified; new anti-pattern #11 forbidding parallel
InverseCost/ReciprocalCost variants.

Canvas (PR #2828) updates:
- §1 PROMOTE: PolynomialCost.degree = signed Rational (no refinement);
  subsumes negative degrees for asymptotic-decay
- §4 Q2-Y candidate: drop "where degree > 0"; plain Rational
- §6 refinement-carriers: PositiveRational DROPPED (struck-through with
  Director cite); ExponentialBase + PolyLogExponent unchanged
- NEW §6.1 Q6 asymptotic-dominance ordering verbatim Director conjecture
  (reverse-sign-convention via Field.compare; Q1-α authority)
- NEW §6.2 Q7 SymbolicCost preserves full expression; Big-O is derived
  operation (dominant_term / asymptotic_class)
- §10 anti-pattern #11: no parallel InverseCost/ReciprocalCost when
  carrier-extension dissolves question
- §12 ratifications Q6 + Q7 added; Practice 4 GREEN per Director
  pre-emption

Worker brief updates:
- §1 PROMOTE: signed Rational, no refinement
- §5.0 PositiveRational refinement DROPPED with struck-through comment
- §5.1 PolynomialCost.degree: Rational (Q6 signed)
- NEW §6.0 Q7 canonical-form preservation: SymbolicCost preserves all
  terms; canonicalize ≠ dominant_term; mixed-sign canonicalization test
- NEW §6.1 Q6 dominance rule encoded via Field.compare reverse-sign
- §6.2 same-variable algebra fold rules header
- §11 anti-pattern #11 mirrored
- §16 Director msg_2c1bfb0e reference added

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 — purge stale PositiveRational refs (cursor 10886)

Cursor APPROVE_WITH_COMMENTS review 10886: post-Q6 scope-extension
(243fd63), several PositiveRational / degree≤0 refinement references
remained in canvas STOP-SIGNAL prose + worker brief verbatim STOP block,
"zero new authority" line, hard-stop directive, STOP condition #4,
anti-pattern #7, and §13 verification axis listing. Worker could follow
the verbatim STOP/anti-pattern text and encode wrong carrier shape
relative to ratified Q6/Q2-Y signed-Rational.

Fix-forward:
- Canvas §6 STOP-SIGNAL prose: PolynomialCost { degree: PositiveRational } → { degree: Rational } (signed per Q6)
- Canvas §10 anti-pattern #7: drop degree≤0/PositiveRational requirement on PolynomialCost; explicit exclusion citing Q6
- Worker §4 verbatim STOP block: same PolynomialCost.degree text fix
- Worker §5.0 "ZERO new authority": drop PositiveRational from refinement list; note PolynomialCost.degree plain signed
- Worker §5.0 hard-stop directive: drop PositiveRational; add Q6 carve-out note
- Worker §10 STOP #4 variant collision: drop PositiveRational from de-dup list; add anti-pattern-#7-fires note
- Worker §11 anti-pattern #7: degree≤0 dropped; explicit PolynomialCost.degree exclusion per Q6
- Worker §13 verification axis: PositiveRational removed from refinement-carriers test list

INVARIANTS P1/P2 single-authority restored across both briefs.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 — STOP-SIGNAL line range :60-72 → :69-72

Cursor REQUEST_CHANGES 10904: brief cited STOP-SIGNAL as :60-72 across
7 surfaces but the live file has STOP at :69-72 and Pattern 3/4
dissolution receipt at :49-67. A literal Phase B "replace :60-72" would
delete part of the dissolution receipt — INVARIANTS P1 (dispatch prose
must ground in identifiable file facts) + P2 (single edit locus).

Fix-forward:
- Canvas L10 / L46 / L325 STOP-cite: :60-72 → :69-72
- Worker L42 / L90 (Phase B replace) / L261 / L350 / L373: :60-72 → :69-72
- Worker §4 Phase B: explicit DO-NOT-TOUCH callout on :49-67 dissolution
  receipt; replacement is surgical 4-line STOP block only

Brief is now internally consistent with canvas:204 ("Current
src/v3/std/algebra.dag:69-72") which was already correct.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 worker — drop stale gt_zero extension from Phase A list

Cursor APPROVE_WITH_COMMENTS 10920: §5.0 KNOWN_PREDICATES extension list
still required extending gt_zero's allowed_carriers to Rational, but
PositiveRational was dropped in the Q6 scope-extension (243fd63) —
no in-scope refinement uses gt_zero on Rational anymore. Conflicting
dispatch vs the comment block above.

Fix-forward: Phase A list now has only the gt_one addition (genuinely
required for PolyLogExponent = Rational where gt_one). Explicit
parenthetical: gt_zero extension NOT required; range allowed_carriers
already includes Int for ExponentialBase. Only gt_one is new.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 — Q6 zero-degree collision + Q7 worker semantics + AP count

Codex BLOCKING review 4bd0cb5 — 2 BLOCKING + 1 non-blocking:

1. Q6 carrier admits degree=0 colliding with ConstantCost (n^0 ≡ 1):
   Fix-forward: keep ratified plain signed Rational carrier; add explicit
   canonicalize-fold rule canvas §6.1 + worker §6 algebra:
   `canonicalize(PolyCost(_, 0)) ⇒ ConstantCost(1)`. Same dissolution
   discipline class as Q2-Y LinearCost ≡ PolyCost(d=1) collapse. Single
   authority for "value=1 constant" via ConstantCost, not parallel via
   PolyCost(_, 0).

2. Q7 output-semantics drift between canvas + worker §14:
   Fix-forward: worker §14 reframed — symbolic_cost_of returns EXACT
   canonical SymbolicCost (Q7 contract change, not backwards-compatible
   reduction). Big-O is derived via dominant_term projection. Legacy
   single-term consumers MUST wrap with dominant_term; canonical-form
   change is expected and ratified.

3. Anti-pattern off-by-one (non-blocking): worker §11 enumerated 11
   items but header + §12 + §13 + §15 PR template said 10. Fix-forward:
   updated all 4 cite-list surfaces to 11 (7 Director-enumerated + 4
   Mgr-derived).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 — Q6 Option B Practice-2 carrier refinement (msg_b80bcaa8)

Director RATIFIED Option B on Q6 zero-degree Practice-2 tension via
msg_b80bcaa8 (relayed by PM msg_9d248cbd 2026-05-13). Practice-2
carrier-level `where nonzero` refinement preferred over Practice-4
canonicalize-fold dissolution; sign-admission intent preserved.

Director-distilled discipline rule (NEW, load-bearing):
> Same-variant redundancy → Practice-4 collapse (Q2-Y LinearCost ≡
> PolyCost(d=1)). Cross-variant redundancy → Practice-2 carrier
> refinement (PolyCost(d=0) ≡ ConstantCost(1)). Type-level state-space
> tightening beats API-level normalization when redundant state crosses
> variant boundaries.

Canvas + worker fix-forward:
- §1 PROMOTE / §3 Q2-Y candidate / §6 STOP-SIGNAL / §6.1 dissolution
  text: `Rational` → `Rational where nonzero` (sign-admission via msg_2c1bfb0e
  preserved; only degree=0 excluded)
- Canvas §6.1: reframed from canonicalize-fold to carrier-level
  refinement; Practice-2 vs Practice-4 disambiguation rule encoded
- Worker §5 Phase A KNOWN_PREDICATES list: add `nonzero` predicate
  (allowed_carriers: Rational; arg_shape: Bare); now 2 new predicates
  (gt_one + nonzero), not 1
- Worker §5 "ZERO new authority" line: cite cross-variant vs
  same-variant rule
- Worker §6 algebra table: canonicalize-fold rule REMOVED (type prevents
  construction); multiplicative cancellation rule split into d1+d2≠0
  and d1+d2=0 cases (=0 maps to ConstantCost(1) directly without
  PolyCost(d=0) intermediate which is type-rejected)
- Worker §7 bootstrap ratchet: type-rejection negative test added
  (PolyCost(_, Rational(0)) must be structurally rejected; ±n admits)
- §11 anti-pattern #12 (new, Director-added): forbid canonicalize-fold
  for cross-variant redundancy when carrier refinement available
- AP cite-list counts: 11 → 12 across §11 header / §12 / §13 / §15

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 canvas — reconcile Q2-Y refinement + variant arithmetic

Cursor APPROVE_WITH_COMMENTS 10980 — 2 internal-consistency findings:

1. Q2-Y parenthetical "no where refinement" contradicted the snippet
   directly above showing `where nonzero` (post msg_b80bcaa8 Option B).
   Reconciled: explicit "no positivity / gt_zero refinement" framing
   per Director msg_2c1bfb0e sign-admission intent, AND explicit
   acknowledgment that `where nonzero` IS present per msg_b80bcaa8
   Practice-2 carrier-level Option B (sign-orthogonal, excludes only 0).

2. Q2-Y Pros bullet "11 → 10 net" contradicted §4 closing "**9** net
   under Q2-Y". Reconciled: corrected to "7 → 9 net" matching §1
   ratified scope (+3 new variants -1 collapsed = +3 net over existing
   7) and §4 closing reconciliation pointer.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 — codex 77088ff non-blocking wording hygiene

Codex no-blocking + 2 non-blocking improvements (77088ff review):

- worker L156: "no such refinement" → "no positivity refinement, but
  DOES carry where nonzero" (clarifies sign-admission vs zero-exclusion
  distinction for downstream readers).
- canvas L285: §10 anti-pattern header "7 Director + 3 Mgr-derived"
  → "7 Director + 5 Mgr-derived; 12 total" (matches actual 12-item
  list per worker §11 cite-list).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: R3 Substrate Mgr — lane through R3 close

* docs(r3): gate #105 — named NonZeroRational alias (codex worker:167)

Codex BLOCKING worker:167: inline `Rational where nonzero` in struct
field types is unsupported by HEAD parser/lowerer — `where` refinements
attach only to type aliases / parameters (precedent
`type PositiveInt = Nat where gt_zero` at dsl/std/integer.dag:181).
Inline use would require unsupported substrate syntax instead of
making illegal degree=0 unrepresentable through a proper named
refinement carrier.

Fix-forward: introduce `type NonZeroRational = Rational where nonzero`
at the type-alias layer (alongside existing
`PolyLogExponent = Rational where gt_one` +
`ExponentialBase = Int where range(min: 2)`). PolynomialCost.degree
field type references the named alias: `degree: NonZeroRational`.

Updates across both briefs:
- All `degree: Rational where nonzero` → `degree: NonZeroRational`
  (5 canvas occurrences + 10 worker occurrences)
- Worker §5.0 dag block: NonZeroRational alias declaration added with
  rationale comment citing codex worker:167 + HEAD parser constraint
- Canvas §6 refinement-carriers list: NonZeroRational row added with
  named-alias note
- Worker §5.0 HARD STOP directive: NonZeroRational added to the
  hard-stop list (named alias, not fresh record); HEAD parser
  constraint cited
- Worker §10 STOP #4 variant-collision list: NonZeroRational added
- Worker §5.0 P1/P2 narrative: clarified "DOES carry NonZeroRational
  named-alias" framing
- Worker §7 bootstrap ratchet test: type-rejection test asserts both
  the type-alias declaration AND the degree=0 rejection at carrier
  level
- Worker §13 verification axis: NonZeroRational added to refinement-
  carriers test list

INVARIANTS P2 + Practice 2 carrier-level illegal-states-unrepresentable
satisfied via named alias (P5 / parser-supported substrate syntax).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): gate #105 canvas — fix §6 'no refinement' stale text (codex canvas:218)

Canvas §6 closing paragraph still said "PolynomialCost.degree intentionally
has no refinement" — pre-msg_b80bcaa8 framing that contradicts the
NonZeroRational alias declared 3 lines above + ratified by msg_b80bcaa8.

Fix-forward: reframe as "no positivity refinement, but DOES carry
NonZeroRational named alias for zero-exclusion". Sign-admission
preserved (msg_2c1bfb0e); zero-exclusion enforced (msg_b80bcaa8).
Also added explicit reference to degree=0 alongside exponent≤1 / base≤1
in the structurally-unrepresentable set.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* WIP: R3 Substrate Mgr — lane through R3 close

* docs(r3): gate #105 canvas — STOP-SIGNAL Tier-2 cite msg_ad5e934d → msg_d86a5987 (cursor 11087)

Cursor APPROVE_WITH_COMMENTS 11087: canvas §6 STOP-SIGNAL cited
msg_ad5e934d for Tier-2 R4-deferral, but the worker brief §4 verbatim
STOP block cited msg_d86a5987 for the same sentence. msg_ad5e934d was
the original Path A Tier-1 ratification; the §8 Tier-2-deferral
disposition was ratified in msg_d86a5987 (per composite-ratification
text already used elsewhere in worker §0/§2/§9/§13/§15). Canvas
STOP-SIGNAL aligned to msg_d86a5987 for single-authority trace.

INVARIANTS P2 single authoritative trace restored.

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 pushed a commit that referenced this pull request Jul 25, 2026
dag/test/claim/effect_expectation_probe_test.dag matched the `_test.dag`
suffix discovery enrolls on (cli_run.rs:1746) while containing zero
`test fn`. That is "enrolled, zero executions" — the coverage-by-illusion
the Phase-0 admission invariant exists to red — introduced in the same
session that removed a vacuous witness for being unable to fail.

Keeping it would have been worse than deleting it. Its arms cannot
discriminate in-language: all three corners of the seam return the same
Bool, and the observable that separates them is whether the Failed line
renders. Dressing that up as a `test fn` over the verdicts would have
produced exactly the shape ffc1eec's own commit message criticises.

The three-corner receipt is not lost — it is recorded verbatim in ffc1eec,
proven by execution. What is missing is an AUTOMATED consumer that fails if
the threading regresses, and that is now tracked (task #12) with the seed's
own precedent named: dispatch_shell_wiring_refuses_oversized_argv exists
because predicate-only tests do not exercise that call path, and the same
gap applies here.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013GELyMsZrGgZRrxte2TCsk
briansrls pushed a commit that referenced this pull request Jul 25, 2026
CI red on b2411f0, batch 3, and the failure is mine: both wall arms hit
"hermetic mode: no mock_response for operation Run — refusing to fabricate
Unit". The wall spawns claim_batch as a CHILD PROCESS to read a passing
corpus's own stderr, so it is Wet by construction, and I let filename
convention enroll it into the hermetic discovery corpus.

The refusal is correct and worth stating rather than routing around: a
mocked child emits no real observation stream, so a hermetic version of this
witness could only ever pass VACUOUSLY — which is precisely the defect class
the wall was built to end. ci_layer_roots' install_media_real_execution_wet_note
already described this exact failure ("no mock_response for operation Dir"),
so the lane and its idiom existed; I simply did not declare into it.

Fixed the way the corpus already does it: a WitnessExclusionRow carves the
file out of per-PR hermetic discovery with a typed reason, and two bin_wet
rows enroll both arms on the wet lane beside the other real-execution
witnesses. Not a mock, not a skip — the same mechanism, declared.

The dissolve_on says no dissolution is expected, deliberately. Reading a real
run's rendered stream is the irreducible content of this check, so it stays
Wet while the glyph wall exists; it deletes only if a structural lens over
the effect graph supersedes it (task #15).

I FLAGGED THIS ONE TURN EARLY AND MISREAD IT. I wrote that the wall's cost
was unmeasured and it "may need enrolling on the bin-wet lane" — right lane,
wrong reason. It is not a budget question at all: a Wet witness cannot live
in hermetic discovery at any cost, because the mode refuses it. Naming a risk
is not the same as classifying it, and I shipped on the weaker read.

Verified: ci_floor_plan_witnesses green, witness_exclusion_frontier_
reconciliation_holds green (the exclusion is reconciled, not orphaned), and
both wall arms still green locally.

ALSO CONFIRMED THIS TURN, by perturbation: re-hardwiring dispatch_shell's
binding back to ExpectSuccess and rebuilding all three bins REDS the wall.
So the wall is already an executing consumer for the threading — task #12's
core regression case is covered, and a separate Rust wiring test would have
been redundant. Its remaining residue is narrower than filed: the
ExpectFailure x ObservedSuccess divergence corner has no live site, and the
OutcomeIsData-consumer-disappears case still needs one.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013GELyMsZrGgZRrxte2TCsk
briansrls pushed a commit that referenced this pull request Jul 30, 2026
…e stages at arm time

Step 0 of the review disposition, plus the two findings fixable without the
run_stage extraction. The remaining findings are named, not silently
carried.

REBASE, and the conflict was load-bearing exactly as predicted. #7467 added
floor_component_receipt_ok to the walk verdict; this branch had replaced
that composition with ordinary_failed || on_success_failed. Resolved by
folding the component receipt INTO ordinary_failed, so a component-receipt
construction or write failure is an ordinary-floor failure that blocks
every success stage — dropping it would have reopened the very ordering
defect this branch exists to close. The test fixture also gained #7467's
new BatchRecord label/selection_tag fields.

THE CARRIER NOW DESCRIBES THE EXECUTOR IT HAS, not the one it wants. The
note claimed members within a stage run concurrently and that each stage
writes its receipt before the next begins; neither is true today — members
run serially and one aggregate receipt is written after the whole
sequence. A carrier promising a guarantee its executor does not provide is
the defect this type exists to end, and I had reintroduced it. The note
now states the barrier that IS real (stage N completes before N+1; a
failed stage prevents every later one) and names three gaps: serial
members, stages bypassing the ordinary unit-lane partition and therefore
governor admission and clamps, and the aggregate receipt. The repair —
extracting the ordinary batch machinery into a reusable run_stage so both
populations share one executor — is named on the carrier as the next step.

ARM-TIME STAGE VALIDATION. Success-stage admissibility is checked
immediately after the plan parses, BEFORE the governor arms and before any
ordinary batch runs: a plan-shape error is knowable at parse time, and
discovering it after a 20-30 minute floor spends the whole walk to report
something the parse already had. Refuses discovery runnables (no defined
green-only meaning), empty entry/function, and heavy-whole-tree-resolve
claims (which would bypass governor admission through the weaker route).

ONE HONEST NARROWING: I first wrote the validator against
profile.spawns_host_compiler and profile.memory — fields the Rust Runnable
does not carry. Only use_walk_memo (the parsed form of
heavy_whole_tree_resolve) and execution_mode survive parsing, so the
validator walls the heavy-resolve case and says so; walling the other two
requires retaining them on Runnable, which lands with the run_stage
extraction. The wall is narrower than intended and the code says which
part is missing rather than implying full coverage.

VERIFIED: cargo test 37/37 (including both floor-finalization arms against
the rebased BatchRecord); the WalkPlan parser RED still refuses a bare-list
plan post-rebase; generated artifacts regenerate clean; fmt clean.

STILL OWED, from the review and unstarted: run_stage extraction with real
intra-stage concurrency and per-stage receipts; finalization policy carried
by WalkPlan rather than selected by plan-function name; schedule-lens
projections that see the stage population; the discriminating executor
control set; then the admission occupants and the task #12 deletion.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K
briansrls added a commit that referenced this pull request Jul 30, 2026
…— see known gaps) (#7470)

* WalkPlan: give walk plans an on-success stage population, parsed strictly

Foundation commit of the success-stages redesign (operator design ruling
2026-07-30). This lands the carrier, the strict parser, the renames, and
sequential fail-fast stage execution in the executor. Every plan declares
on_success_stages: [] today, so runtime behavior is unchanged until the
merge-admission migration populates the floor plan's stages in a
follow-up commit on this branch.

THE CARRIER. std.realization_schedule gains

  type WalkPlan {
    batches: List<List<Runnable>>
    on_success_stages: List<List<Runnable>>
  }

Two populations with different ordering laws, and the type says so where
a bare List<List<Runnable>> could not: batches are the ordinary floor
under FloorBatchStopPolicy; on_success_stages run only after the ordinary
floor completed AND its receipts wrote, each stage a barrier, always
fail-fast between stages — FullLedger is an ordinary-floor policy and
never applies between stages. The carrier note records BOTH prior
defects: the trailing-batch fail-open, and its sibling — members WITHIN a
stage run concurrently, so anything sequential must be ONE claim whose
body sequences its steps (the first repair draft re-created exactly that
bug and the note names it so the next author does not).

THE RENAMES, because a function whose value now carries postcondition
stages must not keep a name that says it returns only batches:

  gunbc_ci_floor_batches         -> gunbc_ci_floor_plan
  gunbc_ci_regen_floor_batches   -> gunbc_ci_regen_floor_plan
  gunbc_ci_plan_artifact_batches -> gunbc_ci_plan_artifact_plan
  gunbc_falsifier_batches        -> gunbc_falsifier_plan

The four argv/step consumers followed automatically because they derive
from the floor_plan_function / plan_artifact_plan_function /
regen_floor_plan_function / falsifier_plan_function constants — the
constants are the single naming authority and were renamed with the
functions; ci.yml and falsifier.yml regenerate with the new names at all
three invocation sites. The internal batch builders survive as
*_ordinary_batches, which the structural witnesses now target. The
budget_red_control fixture renames with the floor fn it impersonates (the
clamp arms by name). Executor string keys (clamp gate, falsifier budget
flag, eager compile-clean install, arm-time refusal roster) renamed in
the same motion.

THE PARSER is one and strict. walk_plan_from_plan requires BOTH fields;
a plan with no postconditions declares an empty list, never omits the
field, and there is deliberately NO fallback from a failed record parse
to a bare-list reading — that fallback would run a malformed plan with
its success stages silently dropped, the silent-widen arm section 5
forbids.

STAGE EXECUTION in run_walk: gated on the whole ordinary floor contract
this process owns — batch verdicts AND every receipt write — not just
any_failed. Members execute serially in-process via run_memo_shared_claims
with a stage-local memo, so an entry shared by stages resolves once and
is reused; serial execution provides more order than the contract
promises, which is safe, while the contract itself promises none. A
non-claim runnable in a stage is a typed refusal, never a widen. Stage
materialization is structurally NOT folded into the floor materialization
receipt: stage memo contexts drop after it is written. A new receipt
class, target/floor-on-success-receipt.txt, records declared/run counts,
per-stage verdicts, and on_success_resolves_total — separate from the
ordinary resolve receipt BY LIFECYCLE, so ci_floor_declared_resolve_count
measures exactly the population it always did. On a red ordinary floor
the receipt still writes, loudly, with skipped=ordinary_floor_failed and
zero stages run — a typed diagnostic, never an admission artifact.

VERIFIED BY EXECUTION:

  RED  a bare-list plan fn refuses: "malformed plan value
       (gunbc_ci_floor_ordinary_batches): WalkPlan missing field
       `batches`", exit 1 — no fallback. (This control also caught a
       missed internal call site at ci_floor_plan.dag:1360.)
  GREEN gunbc_ci_floor_plan parses to the same 5 batches, then this
       container's pre-existing FloorBudgetBelowMinimumFootprint
       fail-fast — which itself proves the parse ran first.
  ci_floor_plan_witness_test 14/14 · ci_spec_witness_test 27/27 ·
  falsifier_workflow_witness_test 11/11 · gunbc_invoke_witness_test 7/7 ·
  pr_native_batch_test 2/2 · realization_schedule_witness 4/4.
  Generated artifacts regenerate; cargo fmt --check clean; claim_executor
  and gunbc build clean. (Workspace-wide cargo build fails in
  v1-stage0-std-core with 7 pre-existing errors, present on clean
  origin/main with this change stashed; CI builds named bins only.)

REMAINING ON THIS BRANCH, per the settled design: executor-level floor
finalization (resolve law + materialization disclosure in-process, the
two GitHub gate steps deleted), the tools.merge_admission entry
(capture_tested_subject as the first ordinary batch, stamp_tested_floor,
refresh_target_and_gate), attempt-scoped receipt schema v2, the task #12
dead-emitter deletion, timeout derivation as the two-budget sum, and the
operator's witness list including the stage-barrier latch test.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K

* Floor finalization moves in-executor; the two receipt-gate steps delete

Phase 1 of the success-stages redesign (operator ruling 2026-07-30): the
resolve-count law and the materialization disclosure law now run INSIDE
claim_executor as ordinary-floor finalization, after the receipts write
and before any on-success stage. The old shape ran them as two GitHub
shell steps AFTER the floor step, so a receipt-law violation could red
the job after admission had already stamped — the can-red-after-admission
hole. In here, a violation is an ordinary-floor failure and blocks every
on-success stage by construction.

MECHANISM. The floor plan projects its law into its own closure:
gunbc_ci_floor_declared_resolve_count in ci_floor_plan.dag reads the
ci_materialization authority (single authority; the projection is a read,
not a second declaration). The executor reads it fail-closed at arm time
for the floor plan only — a floor-named plan whose law cannot be read
refuses the run rather than walking without its contract — and validates:

  law 1: resolves_total (recomputed from batch_records by the SAME
         nonzero-resolve_nanos rule the receipt writer uses, never
         re-parsed from the file we just wrote) equals the declared count
  law 2: the materialization receipt exists, keyed/unkeyed/duplicated
         parse, and keyed_calls is nonzero

Violations are typed FLOOR-FINALIZATION-REFUSED lines, counted into
failure_details. Regen, falsifier, and plan-artifact declare no
finalization and are byte-unchanged in behavior.

DELETED, NOT UNWIRED: both gate scripts and their Scaffold rows in
ci_materialization, both step constructors in ci_workflow, and the two
aux terms in the ci job backstop (100 -> 90, still the exact step-sum +
prelude). A surviving script would be a second representation of the
floor-completion rule whose still-green tests could mask a live-path
regression — the exact shape that hid the lost admission fetch. The
receipt FILES keep writing; they are observability, and only the shell
re-validation of them is gone. ci_spec_witness_test gains the negative
witness that both step names are absent from the emitted workflow.

THE FIXTURE follows the name it impersonates: budget_red_control_plan
declares the law (1 — it runs exactly one single-claim batch) because the
floor name now arms finalization as well as the clamp; before that row
landed, running it WITHOUT the law was the executable RED of the
fail-closed read.

ONE MORE TRANSCRIPTION DELETED, caught by this change redding it:
ci_job_backstop_equals_one_hundred_minutes mirrored the derived step-sum
as a literal 100, so this correct change reported as a failure and the
reviewer move would have been editing the number to 90 — the same class
as the roadmap 63-declared pin, deleted under the same ruling. The
magnitude-independent invariants stay: exact step-sum + prelude (its
conscious double-entry copy updated to the four remaining aux terms) and
the dropped selection-control term.

VERIFIED BY EXECUTION:
  projection reads 1 from the plan closure (gunbc run)
  RED  fixture without the law: "gunbc_ci_floor_declared_resolve_count
       unavailable (fail-closed)", exit 1, before any batch walks
  unit arms (cargo test, 2 new): count mismatch refuses in BOTH
       directions; matching count leaves exactly the missing-receipt
       refusal when no materialization file exists — absence never passes
  ci_spec_witness_test 28/28 · ci_workflow_witness_holds PASS
  ci.yml regenerates: both gate steps gone, ci job timeout 100 -> 90

NOT PROVEN HERE: the full-floor green path through finalization — the
fixture walk now proceeds past the arm into the eager whole-tree
compile-clean install (~72min class) and was killed at a local 10-minute
cap, and the real floor fail-fasts on this container's memory. Owed to
the fleet run with the rest of the merge bar.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K

* Attempt-scoped admission carrier: receipt v2, TestedSubject, WrongAttempt

Phase 3 slice of the success-stages redesign (operator ruling 2026-07-30):
the pure carrier for attempt-scoped merge admission, landed add-replacement
beside the live v1 format. No consumer migrates yet — the wet entry, the
plan wiring, and the v1/emitter-web deletion follow on this branch — so
runtime behavior is unchanged; this slice is the vocabulary the migration
will speak, proven hermetically before anything wet depends on it.

THE CARRIER. MergeAdmissionReceiptV2 carries the walk-attempt identity IN
THE PAYLOAD, not just the path: a misrouted read must fail on content too.
TestedSubject {attempt_id, head_sha, base_ref, base_tree_hash} is the
subject the floor tested, captured pre-floor and bound into the receipt by
the stamp — the stamp must never re-read HEAD or re-observe the target at
stamp time, because main can advance during a tens-of-minutes floor and a
post-floor observation would claim the floor tested a tree it never saw.

THE VERDICT gains MergeDeniedWrongAttempt, checked FIRST: a receipt from
another attempt is neither stale nor fresh — it is not the subject, and
asking whether a foreign receipt's base is current answers a question
about the wrong run. Growing the coproduct forced every exhaustive match
to take a position (non-fold residue, no wildcards): the gate's
verdict_reason, would_block, and the enforcement/actuator witnesses each
gained the arm consciously, and the compiler's exhaustiveness refusal
located the one site the sweep missed (receipt_is_admissible) — the
coproduct growth is complete by construction, not by grep.

ATTEMPT IDENTITY composes from GITHUB_RUN_ID + RUN_ATTEMPT + JOB, pure
composition here, env observation deferred to the wet entry. Every part
must be nonempty or the composition refuses — never a silent 'local'
constant, which would make every non-GitHub run one attempt and leave the
wrong-attempt refusal unreachable off CI (the unreachable-arm shape §5
forbids). Non-GitHub execution supplies GUNBC_WALK_ATTEMPT_ID explicitly,
same nonempty law.

WIRES are self-identifying (schema tag line 1), unlike positional v1: a
v1 wire fed to the v2 parser refuses on the tag rather than mis-binding
fields by position, and the two v2 wire kinds refuse each other. Paths
are attempt-scoped: .gunbc/merge-admission/<attempt-id>/{tested-subject,
floor-receipt}.wire.

VERIFIED BY EXECUTION — 13/13 new hermetic witnesses, including the
ordering proof (a receipt that is simultaneously foreign, Failure, stale-
base, AND stale-roster classifies WrongAttempt — precedence, not
coincidence), both cross-parser refusals, both roundtrips, the nonempty
refusals, and path distinctness across attempts. Existing admission
witnesses regress clean: producer 15/15, enforcement 13/13, actuator 8/8.
Generated artifacts unchanged (model + tests only).

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K

* Carry finalization policy in WalkPlan; regenerate the stale stage0 seed

Two halves: review finding 4, and the fix for the regen red CI just
reported on this branch.

WALKFINALIZATION IN THE CARRIER. The finalization policy was selected by
plan-function name — `if plan_function == "gunbc_ci_floor_plan" read the
law from the closure` — which is the same hidden seed-roster convention
the WalkPlan carrier was built to remove, reintroduced in the same PR.
The RED fixture made the coupling visible: it had to impersonate the
production plan name and then define a projection fn because that name
silently enrolled the contract.

The policy is now a FIELD:

  type WalkFinalization
    = NoWalkFinalization
    | FloorFinalization {
        declared_resolve_count: Int
        require_materialization_disclosure: Bool
      }

  type WalkPlan { batches, finalization, on_success_stages }

Every plan declares it explicitly — the floor carries its law, regen /
plan-artifact / falsifier say NoWalkFinalization, never omission. The
strict parser requires the field, so a floor plan without its law is now
UNWRITABLE rather than discovered missing at arm time — the fail-closed
arm-time read this replaces is deleted along with the projection fn and
the fixture's name-impersonated law. Schedule lenses and plan artifacts
can now see the policy, because it is part of the parsed value.

THE REGEN RED, diagnosed from the job log: regen_verify_gate_passes
returned false on this branch's previous head because the WalkPlan
carrier change touched dag/std/realization_schedule.dag, which is in
v1's regen input closure, and the committed stage0 seed was stale
against it. regen_stage0 confirms the diagnosis exactly: of 108 written
files, precisely ONE differs — std_realization_schedule.rs, the emitted
Rust of the carrier — now regenerated against the current tree
(including WalkFinalization, so one seed covers both changes) and
proven byte-stable on a second regen run.

VERIFIED: cargo build clean; the two floor-finalization unit arms pass
against the field-carried struct; gunbc-eval of gunbc_ci_floor_plan
shows the plan value carrying FloorFinalization { declared_resolve_count
1, require_materialization_disclosure true }; generated artifacts
regenerate clean; fmt clean. Local executor parse probes of the fixture
and regen plans were killed by this container's timeout during the
multi-minute prelude, before reaching the parse line — inconclusive, not
failing; the pushed run is the parse evidence.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K

---------

Co-authored-by: Claude <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants