Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
2fccc2a
docs(briefs): Substrate bridge SourceSpan.file participation retireme…
briansrls May 7, 2026
8c5f054
docs(briefs): S5 Variant-aware projection carrier canvas (#1947)
briansrls May 7, 2026
d826950
docs(briefs): SourceSpan.file brief — same-slice prerequisite + secti…
briansrls May 7, 2026
f26a582
docs(briefs): SourceSpan.file brief — umbrella stays Open per P2 ledg…
briansrls May 7, 2026
beabfa4
docs(briefs): S5 CoproductProjection worker brief — γ ratified (#1947)
briansrls May 7, 2026
925a412
docs(briefs): SourceSpan.file brief — resolve Acceptance #4 / Cross-M…
briansrls May 7, 2026
5b3a9f8
WIP: R3 Substrate Mgr — lane through R3 close
briansrls May 7, 2026
2900228
docs(briefs): S5 brief — absorb Director pre-ratifications for 3 STOP…
briansrls May 7, 2026
313d1a6
Merge remote-tracking branch 'origin/main' into session/warm-wolf-698
briansrls May 7, 2026
0e8724b
docs(r3): Q-Reification Gate A receipt — Option A (Dag-as-carrier)
briansrls May 7, 2026
2601d7d
docs(briefs): S5 — delete superseded canvas + name dissolution trigge…
briansrls May 7, 2026
1b9f743
docs(r3): Q-Reification row — fix invariant cite (C-1 → P2)
briansrls May 7, 2026
55470a1
docs(briefs): S5 — name dissolution trigger for DeclarationRef alias …
briansrls May 7, 2026
8a1f5c7
docs: complete Q-Reification stale-cite sweep — e6-g1a brief :169 + Q…
briansrls May 7, 2026
5fc9221
docs(briefs): S5 — fix InputFieldRef mis-read; reframe observations #…
briansrls May 7, 2026
598776f
docs(briefs): S5 — consolidate split per-variant maps into single key…
briansrls May 7, 2026
4656801
docs(briefs): S5 — fix stale split-map vocab in path (a) + scope STOP…
briansrls May 7, 2026
0ac8ca7
Merge remote-tracking branch 'origin/main' into session/warm-wolf-698
briansrls May 7, 2026
85ceb85
Merge remote-tracking branch 'origin/main' into session/warm-wolf-698
briansrls May 7, 2026
9f0b9de
Merge remote-tracking branch 'origin/main' into session/warm-wolf-698
briansrls May 7, 2026
aac5b3b
docs(briefs): descent_execution_proof canvas — 4-residual coproduct-d…
briansrls May 7, 2026
622361c
docs(briefs): SourceSpan brief Row #6 — derive from bootstrap_authori…
briansrls May 7, 2026
e2741c4
docs(briefs): descent_execution_proof worker brief — γ ratified (2-va…
briansrls May 7, 2026
0a0491c
WIP: R3 Substrate Mgr — lane through R3 close
briansrls May 7, 2026
0cfea88
docs(briefs): descent_execution_proof — narrow EvidenceUnknown payloa…
briansrls May 7, 2026
ce12428
docs(briefs): descent_execution_proof — section-anchor cite for §10.3…
briansrls May 7, 2026
1a0756a
Merge remote-tracking branch 'origin/main' into session/warm-wolf-698
briansrls May 7, 2026
93c6f76
docs(briefs): T-CostLens-Composition canvas — Lens<SymbolicCost> comp…
briansrls May 7, 2026
054dcde
docs(briefs): T-Workflow-As-Data canvas — audit-receipt-honoring scop…
briansrls May 7, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
76 changes: 76 additions & 0 deletions docs/briefs/r3-substrate-t-costlens-composition-canvas.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
# Canvas — Substrate T-CostLens-Composition (`Lens<SymbolicCost>` instance shape)

**Sub-issue**: gunbc#1957 (parented under #1939 Substrate Mgr lane).
**Authority**: `docs/r3-program-plan.md` §10.3 T-CostLens-Composition row at line 399 ("(TBD from Substrate canvas)" — explicitly Substrate Mgr canvas territory); `docs/r3-design-schedule-2026-05-06.md:72` cost-lens-as-discriminator framing.
**Closure predicate**: §1.8 gates #37-40 (structural-fold + thesis-unification + no-separate-cost-dimension + executable predicate) + #70 demonstration.
**Status**: **canvas — Director-tier ratification needed on composition shape before worker brief authoring**.

## Adjacent substrate (grep-verified at HEAD)

- `src/v3/std/lens.dag:70-77` defines the generic `Lens<C>` carrier (`read`, `sequential: Monoid<C>`, `branch`, `iterate`, `validate`). Already-landed; NOT subject to redesign.
- `src/v3/std/algebra.dag:12+` defines `SymbolicCost` 7-variant coproduct (`ProductCost`, `SumCost`, etc.) + `Semiring<SymbolicCost>` inhabitance. Algebra-cost side already-substrate.
- `src/v3/std/lookup.dag:48-60` scaffolds `Lookup<SymbolicCost>` + `MissingCost` lens-boundary-fallback shape.
- `src/v3/std/machine_constraints.dag` (per memory + #1933) defines `MachineWidth<bits>` substrate; target-realization side has structural facts available.
- `src/v3/std/dimensions.dag:10` notes `data symbolic_cost_dimension: AnalysisDimension<SymbolicCost>` is **deferred** — that's part of the canvas territory.

## Scope

T-CostLens-Composition lands a **single `Lens<SymbolicCost>` instance** (or near-equivalent) that composes algebra-cost (already-substrate via `Semiring<SymbolicCost>`) with target-realization-cost (read via `MachineConstraint<C>` / target language spec) end-to-end. Per Director's "cost-lens-as-discriminator" framing: the cost lens orders faithful-representation alternatives by per-primitive realization cost; Grounding selects lowest-cost faithful representation.

**Key invariant** (gate #39 `no_coercion_cost_dimension`): NO separate cost dimension for coercion vs realization vs algebra — one `SymbolicCost` algebra, all three sources feed into it via `Semiring` operations.

## Carrier-composition options

### Option α — Two separate lenses, externally joined

`Lens<SymbolicCost>` reads algebra-cost only (structural-fold over Behavior + algebra inhabitance); separate `Lens<RealizationCost>` reads target-realization-cost from LanguageSpec; composition happens at the consumer (Grounding).

**Pro**: Each lens has a single concern; algebra-cost is target-independent (purer).
**Con**: Violates gate #39 by construction — TWO cost dimensions, joined by convention not by carrier shape. `coercion_cost_equals_complexity_by_construction` (gate #38) would have to be a derived theorem rather than structural-by-construction. Rejected.

### Option β — Single `Lens<SymbolicCost>` with composed witness in `read`

`Lens<SymbolicCost>::read(dag, behavior) -> Witness<SymbolicCost>` reads BOTH algebra-cost AND target-realization-cost, composing them via `Semiring<SymbolicCost>` (sum for sequential operations, product for branch/iterate as appropriate). Target-realization-cost obtained via per-primitive lookup keyed on `MachineConstraint<C>` instances at the Behavior's primitives.

**Pro**: Single cost dimension by construction (gate #39 satisfied structurally); `coercion_cost_equals_complexity_by_construction` is true by construction (gate #38) because coercion is just another operation feeding into the same algebra. End-to-end composition is the carrier's `read` signature.
**Con**: `read` becomes target-aware — needs target-language-spec context threaded through. May force Lens<C> generic's `read: fn(Dag, Behavior) -> Witness<C>` to gain a third parameter (target-context) — substrate-impacting refactor of the generic lens carrier, OR cost lens carries a captured target reference (closure-shape, less structural).

### Option γ — `Lens<SymbolicCost>` reads structural; target-realization via `Lookup<SymbolicCost>`

`Lens<SymbolicCost>::read` reads structural-cost via algebra-fold (Behavior + `SymbolicCost` algebra inhabitance); target-realization-cost composed via existing `Lookup<SymbolicCost>` infrastructure at `lookup.dag:48-60`. The lookup is keyed on per-primitive identity (target-spec-derived); when present, lookup-cost composes into the lens output via `Semiring<SymbolicCost>::sum`.

**Pro**: Reuses existing `Lookup<SymbolicCost>` substrate (per `feedback_audit_adjacent_authority_first` — already authored). Generic `Lens<C>` carrier unchanged; target-realization-cost enters via Lookup's `MissingCost` lens-boundary-fallback shape (already-substrate). Single-cost-dimension preserved (Lookup output IS `SymbolicCost`). `cost_lens_reads_target_realization` (gate #37) is satisfied by Lookup composition; `no_coercion_cost_dimension` (gate #39) is satisfied because Lookup output composes into the same algebra.
**Con**: Lookup-via-Lens-during-read is slightly indirect; consumers must know Lookup is part of the cost computation (vs being lens-internal). Mitigation: lens implementation hides Lookup composition; consumers see only `Lens<SymbolicCost>::read` interface.

## Mgr-tier recommendation

Provisional **γ**: composes via existing `Lookup<SymbolicCost>` substrate (already-authored at `lookup.dag:48-60`); preserves generic `Lens<C>` carrier shape unchanged; satisfies all 4 §1.8 gates by construction (#37 via Lookup, #38 via Semiring composition, #39 via single algebra, #40 via the carrier's typed `read` output). Aligns with `feedback_audit_adjacent_authority_first` + `feedback_compositional_not_templating`.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

BLOCKING: Option γ claims Lookup closes target-realization reading, but Lookup<SymbolicCost> is only an absent/present result carrier and the canvas never names the target/language-keyed realization-cost authority, violating INVARIANTS P1/P2.


**β** is second-best if Lookup composition turns out to be insufficient for end-to-end realization-cost reading at canvas-implementation time (e.g., target-realization-cost requires more context than a per-primitive lookup can carry).

**α rejected** — violates gate #39 by construction.

## Director ratification ask

1. **Pick α / β / γ** (or surface fourth option). Provisional Mgr recommendation: **γ** (Lookup composition).
2. Confirm `Lens<C>` generic at `lens.dag:70-77` is authoritative starting point (no carrier-shape refactor in T-CostLens scope). Per option γ this is unchanged; per option β it would refactor.
3. Confirm `data symbolic_cost_dimension: AnalysisDimension<SymbolicCost>` (currently deferred per `dimensions.dag:10`) lands as part of T-CostLens-Composition or stays separately deferred to a Dimensions sub-lane.

## On ratification — worker brief scope

Will author execution brief covering:
- `Lens<SymbolicCost>` instance authoring in DSL (likely `src/v3/lenses/cost.dag` per existing convention; verify-via-grep at brief time)
- `read` implementation per chosen option (γ Lookup composition / β composed witness)
- `cost_lens_demonstration` (gate #70): ≥2 algebra-instances composed + ≥1 recursive call + observable cost-bound output — fixture program + executor wiring same-slice
- 4 §1.8 gates (#37-40) advance to executable status
- `data symbolic_cost_dimension` lands or stays deferred per question 3

## Worker pin (Mgr disposition)

Substrate-fact-introduction precedent owners — valiant-ibex-312 (delivered IntPlatform/UIntPlatform, S5 candidate) OR smart-ram-167. Final pin at dispatch.

## Auto-spawn caveat

Per Director's standing note + cache-staleness cluster ctrl#217: HOLD dispatch on this canvas's worker brief until auto-spawn fix lands per L-sized substrate-fact-introduction threshold.

— Authored by warm-wolf-698 (Substrate Mgr) 2026-05-07 post-#2105 merge per Director endorsement of pre-staging T-CostLens-Composition canvas-shape.
77 changes: 77 additions & 0 deletions docs/briefs/r3-substrate-t-workflow-as-data-canvas.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,77 @@
# Canvas — Substrate T-Workflow-As-Data carriers (5-row scope-narrowing)

**Sub-issue**: gunbc#1956 (T-Workflow-As-Data CI-workflow-as-.dag-data demo, parented under #1939); umbrella scope is §10.3 row Q-Workflow-As-Data-Carriers (line 983, OPEN — Substrate Mgr scoping needed).
**Authority**: `docs/r3-program-plan.md:474-480` (5 carrier names) + `docs/r3-design-schedule-2026-05-06.md:84-88` (audit-first directive); `dsl/extdeps/github/actions.dag` (218 lines, already-substrate); audit-and-delta receipt landed 2026-05-06 via #1771 (closed #1873).
**Closure predicate**: §1.8 gates #53 (workflow_substrate_carriers_landed), #54 (timing_lens_carrier_landed), #55 (shared_external_attachment_pattern_documented), #56 (ci_workflow_modeled_as_dag), #62 (substrate_gap_file_ingestion_closed), #63 (substrate_gap_workflow_scheduling_closed).
**Status**: **canvas — Director-tier ratification needed on reuse-vs-new scope before worker brief authoring**.

## Observation: 4 of 5 named carriers ALREADY exist in `extdeps.github.actions`

Per §S4 design-schedule directive line 84 (codex BLOCKING 2026-05-06): "S4 worker brief MUST audit `extdeps.github.actions` first and either (a) extend/refine existing carriers via T-Workflow-As-Data lens-consumption-shape additions (preferred per `feedback_audit_adjacent_authority_first` + `feedback_parallel_representation_debt`), or (b) explicitly dissolve `extdeps.github.actions` with a migration path before introducing parallel carriers."

Grep-verified `dsl/extdeps/github/actions.dag` at HEAD:

| §10.3 row 983 carrier name | extdeps.github.actions HEAD | Reuse/refine | Net new substrate |
|---|---|---|---|
| `WorkflowTrigger` (Push / PullRequest / Cron<Schedule> / Manual<Inputs>) | `WorkflowTrigger` (Push / PullRequest / Schedule / WorkflowDispatch / WorkflowCall) at `:40` | Refine: `Schedule { cron: String }` → typed `Cron<Schedule>` carrier (per design-schedule:87) | minimal |
| `WorkflowStep` (run command + dependencies + outputs) | `Step` at `:103` | Reuse name `Step`; lens-consumption may add observation anchor | none if pure reuse |
| `WorkflowMatrix<Axes>` (parameter expansion) | `MatrixStrategy` at `:66+` (inside `Job`) | Reuse + possibly extract as standalone carrier for lens consumption | minimal |
| `WorkflowSecret<Name>` (provider-typed, opaque-at-rest, scoped-by-step) | NOT EXTANT in actions.dag at HEAD | **NEW substrate** | full carrier |
| `RunnerResource<C>` (compute class, OS, hardware) | `RunnerSpec` + `RunnerLabel` at `:88+` | Reuse + parameterize as `RunnerResource<C>` for lens-shape consumption | minimal |
| `Workflow<Trigger, Steps, Resources>` composing carrier | `Workflow` at `:20` (untyped composition) | Refine to parameterized form for lens generic dispatch | minimal |

**Key finding**: of the 5 named carriers in §10.3 row 983, **only `WorkflowSecret<Name>` is wholly new substrate**. The other 4 are reuse-or-refine of existing `extdeps.github.actions` types. The audit-and-delta receipt (#1771, closed via #1873) confirmed this shape; the canvas territory now is **the lens-consumption-shape question**, NOT a 5-carrier-introduction question.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

BLOCKING: The “only WorkflowSecret<Name> is wholly new substrate” conclusion is not supported by the full adjacent audit: Step lacks the required dependency/output facts and dsl/extdeps/cron.dag already owns CronSchedule, so the worker scope risks both dropped facts and duplicate authority.


## Real canvas question (post-audit)

Given the existing `extdeps.github.actions` substrate is the reuse-base, what's the **minimum additional substrate** needed for T-Workflow-As-Data closure?

### Option α — Maximalist: introduce all 5 named carriers in `dsl/std/workflow.dag` as parametric refinements

New file `dsl/std/workflow.dag` declares parameterized versions of all 5 carriers; `extdeps.github.actions` types become specialized instances via composition. New `WorkflowSecret<Name>` lands here.

**Pro**: clean substrate-internal home for T-Workflow-As-Data; lens consumption talks to `dsl/std/workflow.dag` (compiler-internal vocabulary), not `dsl/extdeps/github/` (external-tool vocabulary).
**Con**: introduces parallel-representation debt with `extdeps.github.actions` (per `feedback_parallel_representation_debt`). The audit-receipt's reuse-first directive argues against this. 5 new types when only 1 is wholly novel.

### Option β — Minimalist (audit-receipt-honoring): land only `WorkflowSecret<Name>` + `Cron<Schedule>` refinement; lens consumes existing `extdeps.github.actions` types directly

Single new file `dsl/std/workflow_secret.dag` (or fold into `extdeps.github.actions` if scope-cohering) carrying `WorkflowSecret<Name>` + the typed `Cron<Schedule>` refinement. Lens-consumption shapes (e.g., `WorkflowObservationAnchor`) land in `dsl/std/workflow.dag` separately if/when needed by the lens; T-Workflow-As-Data's CI-workflow-as-.dag-data demo (#1956) consumes the refined `extdeps.github.actions` directly.

**Pro**: minimal substrate addition; honors audit-receipt's reuse-first directive (`feedback_audit_adjacent_authority_first`); single point of new-substrate, single point of refinement. No parallel-representation debt.
**Con**: lens consumption talks to `extdeps.github.actions` (external-tool vocabulary) — may look conceptually inconsistent with other lens consumers reading `dsl/std/*` types. Mitigation: documented as deliberate audit-receipt outcome.

### Option γ — Lens-consumption-shape carrier separately + minimal new substrate

Like β but with `WorkflowObservationAnchor` (per Substrate Mgr design stance at gunbc#1130 comment-4374109666) explicitly authored alongside `WorkflowSecret<Name>`. The lens-consumption layer is its own typed carrier; doesn't conflate with `extdeps.github.actions` reuse.

**Pro**: separates "external-tool vocabulary" (extdeps.github.actions, reuse) from "lens-consumption substrate" (new `WorkflowObservationAnchor`); each layer has single concern. Lens consumers read `WorkflowObservationAnchor`, which references `extdeps.github.actions::Workflow` structurally.
**Con**: 2 new substrate carriers vs β's 1; mild scope expansion. Justifiable IF lens-consumption-shape genuinely needs typed handle distinct from `extdeps.github.actions::Workflow`.

## Mgr-tier recommendation

Provisional **β** (minimalist, audit-receipt-honoring): only `WorkflowSecret<Name>` + `Cron<Schedule>` refinement land as net-new substrate. Lens consumes `extdeps.github.actions` directly until evidence shows a typed lens-handle is needed. **γ** is the natural ratchet from β if lens-consumption-shape evidence accumulates (per `feedback_construction_over_ratchets` — model first, dissolve later if substrate evidence forces).

**α rejected** — admits parallel-representation debt against `extdeps.github.actions` audit-receipt findings.

## Director ratification ask

1. **Pick α / β / γ** (or surface fourth). Mgr recommendation: **β**.
2. Confirm `extdeps.github.actions` audit-receipt at #1771 is the binding precedent for reuse-first posture (i.e., the audit confirmed reuse is the right shape, not deprecation).
3. Confirm `WorkflowSecret<Name>` location: `dsl/std/workflow_secret.dag` (new file) vs fold into existing `extdeps.github.actions` (extension). Provisional Mgr preference: **new file** (compiler-internal substrate, distinct from external-tool vocabulary; honors layer model).
4. Confirm whether §1.8 gate #54 (`timing_lens_carrier_landed`) and gate #55 (`shared_external_attachment_pattern_documented`) are in T-Workflow-As-Data scope or fold to T-LBP / separate sub-lane.

## On ratification — worker brief scope

Will author execution brief covering:
- `WorkflowSecret<Name>` carrier (`dsl/std/workflow_secret.dag` per option β/γ)
- `Cron<Schedule>` typed refinement (location TBD per question 3)
- (γ only) `WorkflowObservationAnchor` lens-consumption-shape carrier
- Worker pin: substrate-fact-introduction precedent owners (valiant-ibex-312 / smart-ram-167)
- Acceptance: §1.8 gates #53-#56 + #62-#63 advance per closure-predicate scope
- T-Workflow-As-Data #1956 demo consumer wiring (CI-workflow-as-.dag-data) in same-slice or cross-Mgr handoff per Director ratification

## Sequencing caveat

Per §S4 design-schedule line 95: "post-T-Lens-Behavioral-Parity COMPLETE (per `r3-structure.md` §"Dependency on R2"; lens consumption needs lenses COMPLETE)". This canvas is dispatch-ready post-T-LBP COMPLETE; brief authoring can land in advance per pre-staging discipline but worker dispatch waits.

— Authored by warm-wolf-698 (Substrate Mgr) 2026-05-07 post-#2105 merge per Director endorsement of pre-staging next-up substrate canvases. Honors audit-and-delta receipt #1771 (closed #1873) reuse-first directive.
Loading