Repository navigation
docs(r3): add affected-set Introspect-lens prototype canvas #2713
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
20 commits
Select commit
Hold shift + click to select a range
5e2fa8d
docs(r3): add affected-set lens prototype canvas
briansrls a1fecc2
Merge remote-tracking branch 'origin/main' into session/clever-tern-6…
briansrls ae04070
Merge remote-tracking branch 'origin/main' into session/clever-tern-6…
briansrls 0a97c31
docs(r3): preserve affected-set output carrier options
briansrls ca9ccdd
Merge remote-tracking branch 'origin/main' into session/clever-tern-6…
briansrls 92e8344
Merge remote-tracking branch 'origin/main' into session/clever-tern-6…
briansrls ecdf567
docs(r3): ground affected-set canvas in live substrate
briansrls c57ef3b
Merge remote-tracking branch 'origin/main' into session/clever-tern-6…
briansrls 79dcd07
Merge remote-tracking branch 'origin/main' into session/clever-tern-6…
briansrls 95a4a4b
Merge remote-tracking branch 'origin/main' into session/clever-tern-6…
briansrls 8151141
docs(r3): require executable affected-set fixture receipt
briansrls 13598c0
Merge remote-tracking branch 'origin/main' into session/clever-tern-6…
briansrls 19c1010
Merge remote-tracking branch 'origin/main' into session/clever-tern-6…
briansrls acf131e
Merge remote-tracking branch 'origin/main' into session/clever-tern-6…
briansrls b598a73
Merge branch 'main' into session/clever-tern-670-affected-set-canvas
briansrls efb3c7a
Merge remote-tracking branch 'origin/main' into session/clever-tern-6…
briansrls ff54d16
Merge remote-tracking branch 'origin/main' into session/clever-tern-6…
briansrls 0bdeec9
Merge remote-tracking branch 'origin/session/clever-tern-670-affected…
briansrls ca3c6f0
docs(r3): clarify affected-set fail-closed seeding
briansrls ee62573
Merge remote-tracking branch 'origin/main' into session/clever-tern-6…
briansrls File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
109 changes: 109 additions & 0 deletions
109
docs/briefs/r3-affected-set-introspect-lens-prototype-worker.md
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,109 @@ | ||
| # R3 affected-set Introspect-lens prototype — substrate-composition implementation | ||
|
|
||
| **Status:** PRE-AUTHED SUBSTRATE-FEASIBILITY PROBE before implementation. Canvas-driven rebuild for gunbc#2699; supersedes silent-bat-152 PR #2701 once a replacement implementation PR opens. The worker may proceed to implementation only after showing the before/after/dimension inputs can be represented with existing `.dag` substrate and tests-as-data fixtures; otherwise the correct outcome is escalation for substrate-extension authority, not a workaround PR. | ||
|
|
||
| **Owner:** worker TBD on dispatch. Coordinator: R3 Verification Mgr (`clever-tern-670`). PM/Director escalation path: deep-wolf-155 / zesty-bear-812. | ||
|
|
||
| **Design authority:** [`docs/design-affected-set-lens.md`](../design-affected-set-lens.md), especially §0 locked substrate-vs-adapter terminology, §2 dimension-parameterized affected-set definition, §3 substrate-composition algorithm sketch, and §4 worked examples. | ||
|
|
||
| **Context:** PR #2701 is being closed as superseded because it introduced a large hand-Rust affected-set implementation and increased the SG-0 hand surface. This rebuild must prove the same prototype shape through `.dag` substrate composition, not a new Rust analysis engine. | ||
|
|
||
| --- | ||
|
|
||
| ## §0. Locked framing | ||
|
|
||
| The affected-set surface is an **Introspect lens-family prototype**, not a new query substrate. | ||
|
|
||
| - The lens lives at `src/v3/lenses/affected_set_lens.dag`. | ||
| - The substrate output is `Set<NodeRef>` or a `NodeRef`-keyed record carrying dimension and provenance. | ||
| - User-facing CLI / IDE / agent rendering (`{file, span}`, symbols, line ranges) is an adapter boundary after substrate output exists. | ||
| - No `Query` type, no parallel affected-set Rust engine, and no hand-maintained downstream graph. | ||
|
|
||
| Live substrate check: `src/v3/std/lens_application.dag` currently exposes `IntrospectApplication<Output>` as `{ lens, section, span }`. It does **not** yet declare `Dag_before` / `Dag_after` / `dim` input fields. The worker composes only what exists. If the before/after/dimension inputs from the design cannot be represented with existing `.dag` facts and fixtures, STOP and escalate instead of inventing a new substrate carrier or filling the gap with Rust. | ||
|
|
||
| ## §1. Deliverable | ||
|
|
||
| Implement the pre-R3-close prototype from `docs/design-affected-set-lens.md` §7: | ||
|
|
||
| 1. First produce a substrate-feasibility receipt in the implementation PR body naming the actual carriers used for before/after/dimension inputs and output. If the only honest answer is "missing substrate", STOP and escalate before adding `affected_set_lens.dag`. | ||
| 2. Add `src/v3/lenses/affected_set_lens.dag` as the substrate authority for the affected-set Introspect lens only after that receipt is grounded. | ||
| 3. Keep the lens compact and compositional. Expected size is roughly 20-50 lines unless a clearly cited substrate shape forces slightly more. | ||
| 4. Add tests-as-data fixtures only under `src/v3/compiler/tests/dag/`. | ||
| 5. Demonstrate three real PR outputs from the gunbc#2699 charter: | ||
| - PR #2693: v2 directory delete | ||
| - PR #2679: gate #4 `workflow_idempotency` | ||
| - PR #2647: quantifier substrate | ||
| 6. Each real-PR output must include per-dimension affected-set data plus commentary on why the set is narrower than naive transitive-downstream. | ||
| 7. Prove the fixtures execute through an existing zero-SG-0 runner path. `tests/dag/` is not self-discovering on current main; live execution is still mediated by Rust `TestRunner` / suite wiring. The implementation PR must name the existing runner/suite path that executes the new `TestClaim`s, or STOP if execution would require adding a new Rust integration test/table entry. | ||
|
|
||
| ## §2. Required substrate composition | ||
|
|
||
| The implementation must cite and consume these substrate pieces: | ||
|
|
||
| | Piece | Authority | Required role | | ||
| | --- | --- | --- | | ||
| | `IntrospectApplication` output carrier | `src/v3/std/lens_application.dag` | User-surface introspect mode; no enforcement budget axis. Consume the existing `{ lens, section, span }` carrier shape only. Output must preserve the design's allowed substrate shape: `Set<NodeRef>` or a `NodeRef`-keyed record carrying dimension/provenance. If before/after/dimension inputs cannot be represented without new substrate, STOP. | | ||
| | `Dag` graph edges | v3 substrate / `Dag` shape | Reverse-edge traversal over the compiled graph. | | ||
| | `DescentEvidence` | `src/v3/std/termination.dag` | Call-site descent lattice; narrows propagation when evidence is known. | | ||
| | `SubValueRelation` | `src/v3/std/induction.dag` | Tracks which sub-piece flows through a call/refinement edge. | | ||
| | `Cardinality` substrate facts | `src/v3/std/substrate.dag` plus existing `src/v3/lenses/*` consumers of `Cardinality` | Distinguishes opaque-carrier changes from structural cardinality/data-shape changes. There is no dedicated `cardinality.dag` lens on `origin/main`; do not require one unless escalated. | | ||
| | `cross_target_coverage` | `src/v3/std/cross_target_coverage.dag` | Narrows target-specific propagation rather than marking every target consumer. | | ||
| | `TestClaim` | `src/v3/std/verification.dag` | Tests are data; affected-set can intersect with TestClaim references. | | ||
|
|
||
| If any required substrate piece is missing or cannot be consumed from `.dag`, STOP and escalate. Do not fill the gap with Rust. | ||
|
|
||
| ## §3. Dimension semantics | ||
|
|
||
| The prototype must preserve the dimension-parameterized shape from the design: | ||
|
|
||
| - dimensions: `value`, `cost`, `complexity`, `effect`, `refinement` | ||
| - seed nodes with a **PROVEN** delta in that dimension, plus nodes whose dimension delta cannot be proven empty | ||
| - exclude a node only when the lens emits a receipt proving `delta(dim) == empty` for that consumer | ||
| - propagate only through typed edges where that dimension is read by the consumer | ||
| - emit or fixture a per-dimension affected-set output, not just one undifferentiated set | ||
|
|
||
| Unknowns must not silently disappear. If the lens cannot prove `delta(dim) == empty`, the affected consumer stays in the affected-set and the fixture commentary must say why. | ||
|
|
||
| ## §4. Hard constraints | ||
|
|
||
| 1. **No hand-Rust analysis engine.** Do not add `src/v3/compiler/src/affected_set*.rs` or comparable host-side graph logic. | ||
| 2. **Near-zero Rust budget.** A user-surface adapter is legitimate only at a CLI/rendering boundary and only with explicit canvas-tier justification citing the substrate gap that prevents `.dag` rendering. This prototype should not need one. | ||
| 3. **Tests-as-data only.** Add `TestClaim` fixtures under `src/v3/compiler/tests/dag/`. Do not add Rust integration tests, unit tests, or SG-0 entries. | ||
| 4. **SG-0 delta must be zero or negative.** Positive SG-0 delta is a stop signal. Escalate to PM/Director before pushing. | ||
| 5. **No template-only fake.** The lens body must compose substrate facts. A table of hand-authored PR-name-to-output templates does not satisfy the brief. | ||
| 6. **No new substrate carriers unless escalated.** The prototype consumes existing carriers and substrate facts named above. New `DagDiff`, `DimensionInput`, query, or specialized cardinality-lens substrate requires canvas-tier approval before implementation. | ||
| 7. **No new Rust runner bridge.** The executable receipt must use an existing zero-SG-0 test-as-data runner path. Adding a Rust integration test, fixture registry, or ad hoc table entry just to discover this lens's fixtures is a stop condition, not part of this canvas. | ||
|
|
||
| ## §5. Acceptance | ||
|
|
||
| The implementation PR is acceptable when all are true: | ||
|
|
||
| - `src/v3/lenses/affected_set_lens.dag` exists and is the only affected-set lens authority. | ||
| - The PR body includes a substrate-feasibility receipt naming the actual existing carriers/fixtures used for before/after/dimension inputs and output. | ||
| - The lens is modeled against the existing `IntrospectApplication<Output>` carrier without pretending it already has `Dag_before` / `Dag_after` / `dim` fields. If the prototype uses fixture data to represent those design inputs, the PR body must identify that as prototype evidence and name the substrate gap for follow-up. | ||
| - The `.dag` tests-as-data fixtures cover: | ||
| - dimension-specific outputs for value, cost, complexity, effect, refinement | ||
| - fail-closed unknown-delta behavior | ||
| - the three real PRs named in §1 | ||
| - The PR body includes a zero-SG-0 executable receipt naming the existing `TestRunner` / suite path that executed those fixtures, with the command and result. | ||
| - Fixture commentary explains narrowing vs naive transitive-downstream for each real PR. | ||
| - SG-0 hand-authored Rust count does not increase. | ||
| - PR body includes: `Supersedes PR #2701` and a closure note that #2701 should close as superseded once the replacement PR is open. | ||
|
|
||
| ## §6. Stop and escalate | ||
|
|
||
| Escalate with `dashboard-message send --to parent --body "..."` if: | ||
|
|
||
| - implementing the lens appears to require Rust graph traversal outside an adapter boundary | ||
| - before/after/dimension inputs cannot be represented using existing `.dag` substrate and tests-as-data fixtures | ||
| - a required substrate fact is absent or only available through a host mirror | ||
| - a TestClaim cannot express the prototype output without a new predicate/carrier | ||
| - the new `TestClaim` fixtures cannot execute through an existing zero-SG-0 runner/suite path | ||
| - the SG-0 delta would be positive | ||
| - the worked real-PR outputs cannot be represented as `Set<NodeRef>` / dimension-keyed records | ||
|
|
||
| Do not push a workaround PR for any of these; the point of this rebuild is to avoid repeating PR #2701's hand-Rust path. | ||
|
|
||
| --- | ||
|
|
||
| **End of canvas.** | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This comment was marked as resolved.
Sorry, something went wrong.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed in 8151141: the brief now explicitly states that tests/dag is not self-discovering on current main, requires a zero-SG-0 executable receipt through an existing TestRunner/suite path, and makes missing runner coverage a STOP condition rather than allowing a new Rust integration test/table bridge. — sent from clever-tern-670