Repository navigation
Conversation
…eality Operator: "node granularity only (file falls out of it); worked examples; a PR so i can see; how fast to dogfood via v2?" - GRANULARITY corrected: ONE real granularity = NODE. File/module view is node projected up (files containing ≥1 affected node), NOT a separate tier. (Retracts my earlier two-tier framing.) - 4 WORKED EXAMPLES embedded as the design contract: (1) change a NamedReason variant → forward-closure frontier, pure helper skipped; (2) cosmetic edit → content_hash unchanged (K-1/B1 α-equivalence) → ∅ frontier, zero recompute; (3) unbounded effect → fail-closed (include dependents, never optimistic skip — no-engine); (4) change isolated pure node → minimal cone only. - DOGFOOD REALITY (verified, honest): v2 has `run` + a MODULE-level dag-artifact.json, but is the FROZEN seed (can't enrich emission, A3) ⇒ NO node-granularity path through v2; that arrives at T-9. v2 also only compiles the v2-subset stubs (empty edges) — no real corpus to affect today; a demo over edge-empty stubs = theater = forbidden. Earliest honest dogfood = module-granularity over the artifact via `v2-compiler run`, gated on real .dag content (#3151 → T-1/T-3) + the v2-interpreter pre-flight. Stated in-file so it is not folklore. - Consumes tightened: + lens/effect.dag (effect-independence gates safe skip) + std/primitive.dag Hash (the structural Diff is the B1 hash). Isolated PR (only lens/affected_set.dag; disjoint from #3150/#3151). v2->v4 bootstrap viability OK (57 modules, 0 diagnostics). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Review metadata
1. Story of the diffThis PR tightens the design contract for 2. Invariant categories
Compliant — this is a v4 lens design-contract scaffold, not a new substrate type/variant or Dag mutation surface. It correctly keeps the substrate fact at
Compliant — fail-closed and facts-flow-forward are explicitly encoded in the contract: unprovable effect independence includes dependents instead of skipping them ( chatgpt-review-33e495cd-9f3b-43…
N/A — the diff adds no Rust implementation, functions, methods, error shapes, hidden state, or helper placement. The contract does, however, preserve the project’s preferred input→output shape by documenting the lens as
Compliant — no executable behavior changed, so no new test is required in this PR. The added worked examples are shaped like future behavior-driven test claims: Ex.1 names a dependency-cone behavior, Ex.2 names a cosmetic-change/no-recompute behavior, Ex.3 names fail-closed inclusion, and Ex.4 names a pure-helper minimal-frontier behavior (
Compliant — I do not see a divergence from the live v4/pure-bootstrap direction. The diff reinforces that v2 is a frozen seed and rejects enriching v2 emission for this feature (
Compliant — the file remains explicitly marked as a scaffold to fill under T-21 ( 2.5. Top-down PM intent reviewCompliant — the highest-level intent is preserved. The thesis requires dependency modeling from one graph, structural correctness as data, and incremental consequences from purity plus dependency graph structure; this PR makes affected-set selection a node-level structural fact rather than a shell/file-tier heuristic ( It also avoids semantic dilution of the bootstrap path: instead of claiming an easy v2 dogfood story, it states that v2 cannot provide node-granularity and that an edge-empty demo would be “theater” ( chatgpt-review-d9e7dc23-b3b4-4b… 3. VerdictAPPROVE. This is a documentation/design-contract PR, but it materially improves the downstream implementation contract: one node-level affected-set authority, structural hash-based diffing, fail-closed skip semantics, and an honest v2 dogfood boundary. I found no diff-cited invariant violation or PM-intent dilution. |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
75e2d5af· Trigger:schedule - Thinking:
181s wall
Non-blocking — Strengths
src/v4/lens/affected_set.dagClassified as mixed .dag model/design text; the added contract preserves node-granular affected-set authority, fail-closed inclusion, and an honest no-v2-shortcut dogfood boundary.
✅ No blocking concerns.
…ntracts Derisk (operator-requested). The Ex.1-4 worked examples proved correctness; these prove the MINIMALITY claim is falsifiable and bind its real gates: - Ex.R1 (effectful local edit): minimal IFF the effect algebra is fine-grained — an effect-GRANULARITY property, not effect-lens strength (B3 makes effects structural/read, so the lens is strong by construction; coarse effects are the open risk). Contract on lens/effect.dag. - Ex.R2 (widely-shared sub-node, partial change): minimal IFF infer emits NODE-PRECISE use→def edges to the consumed sub-Node. The dominant gate — more load-bearing than the effect lens. Contract on compiler/04_infer.dag (T-9). - Ex.R3: "what counts as changed" is retired-safe by B1-CANON (#3157) — fail-closed sequenced default ⇒ worst case over-fire, never a missed change. No residual research risk on Diff granularity. Consumes section sharpened with the two implied contracts + the B1-CANON Merkle dependency. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Extended (b9cfb0a) with the R1/R2/R3 adversarial minimality stress + two implied consumed-contracts, per the derisk discussion:
Coordination notes (honest): (1) this branch is based on an older — sent from deep-wolf-155 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
b9cfb0a2· Trigger:schedule - Thinking:
355s wall
BLOCKING (2)
Root Cause
src/v4/lens/affected_set.dagv2 artifact audit stopped at the module wrapper instead of the serialized item Nodes → rewrite the dogfood claim around the absent B1 canonical hash/use-def edge facts.src/v4/compiler/04_infer.dagT-21 now consumes a dependency-edge fact that T-9 has not placed in Node/Edge/InferredFacts or explicitly escalated as a substrate extension → name the carrier or reconcile the extension before treating minimality as contracted.
| // DOGFOOD REALITY via the frozen v2 seed (operator asked "how fast can we | ||
| // dogfood this using v2?" — honest answer, verified 2026-05-15): | ||
| // - v2 HAS a `run` interpreter + emits a structured `dag-artifact.json` | ||
| // (`compile --target dag`). But that artifact is MODULE-level |
There was a problem hiding this comment.
BLOCKING: The v2 dogfood section says dag-artifact.json is module-level and not the Node tree, but v2's emit_dag_artifact serializes TypedModule.items through serialize_node with recursive children/body/inferred fields, so this violates P1 Modeling Faithfulness; the honest boundary is missing v4 B1 content hashes/node-precise dependency edges, not absence of node structure.
| // all effectful code — else minimality degrades (still correct, | ||
| // fail-closed). Granularity, not lens strength | ||
| // - compiler/04_infer.dag: the typed dependency graph (Dag). | ||
| // CONTRACT (Ex.R2 — the dominant gate): edges MUST be NODE-PRECISE |
There was a problem hiding this comment.
BLOCKING: The Ex.R2 contract makes affected_set depend on node-precise use→def edges from infer, but the referenced v4 infer/node contracts do not name a carrier for cross-declaration dependency edges, leaving a load-bearing boundary fact without a substrate authority (INVARIANTS P1/P2 facts-flow-forward).
|
Review metadata
1. Story of the diffThis PR turns 2. Invariant categories
Compliant — this does not add a new substrate type or behavior; it keeps the affected-set lens as a consumer of existing/future substrate facts, and explicitly rejects a separate file/module tier by saying node is the only real granularity and file/CI is projection only at
Finding — BLOCKING, P2 Boundary Discipline / single authority for “changed node.” The R2 example says
N/A — no Rust implementation code, helper API, method shape, error/result shape, or naming surface changed; this is comment-only design-contract text in a
N/A — no executable behavior changed, so no new test is required in this PR. The worked examples are the intended future test contract, and the dogfood section correctly forbids an edge-empty v2 “demo” at
Compliant — the diff does not dilute the active v4/zero-floor direction; it says v2 is frozen and cannot be enriched for node-granularity, and that node-granularity arrives through the v4 typed Dag path at T-9 at
Compliant — the temporary v2 dogfood path is bounded as module-granularity only, blocks theater over empty artifacts, and names concrete gates before relying on it: real v4 imports/declarations via T-1/T-3/#3151 plus a v2-interpreter pre-flight at 2.5. Top-down PM intent reviewFinding — BLOCKING planning-contract ambiguity. The diff declares these worked examples to be “the design contract” that the T-21 worker must fill at 3. VerdictREQUEST_CHANGES — The PR is directionally strong and mostly strengthens the contract, especially around node granularity, fail-closed re-execution, and honest v2 dogfood limits. I would not land it until the R2 sub-node-vs-parent-hash ambiguity is resolved, because the PR’s main artifact is the future implementation contract. |
B-5 (affected_set R1 usefulness): effect is a per-Arrow-Node fact from the signature (B3), never aggregated coarse — a granularity invariant (coarse ⇒ R1 correct-but-useless). effect.dag B-5 block + affected_set Consumes/Ex.R1 cross-ref + DECISIONS B-5 row. Subsume #3153 (v4-affected-set-design, no worker — operator-directed): its 4 worked-examples + adversarial R1/R2/R3 + dogfood-reality folded into affected_set.dag as the T-21 design contract, reconciled to the now-ENCODED reciprocal contracts — Ex.R1→B-5 (effect.dag), Ex.R2→B-4 (04_infer.dag), Ex.R3→B-3 (drafted #3157 point-3 correction). #3153 superseded; recommend close. DECISIONS #3153-subsumed row. B-2 (PROOF-1 prover model lands): extdeps/languages/lean.dag (new) — Lean first, termination theorem class; Coq deferred second-prover probe. B2-OMNI requires the LanguageModel file PROOF-1 #3158 deferred. STRUCTURE enumeration+count 63→64; DECISIONS L-4; TASKS PROOF-1 note. Includes the already-committed origin/main merge (204b855: #3158 PROOF-1 + #3160 meta-cut; DECISIONS.md conflict resolved keeping D1/B-4/PROOF-1). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Subsumed by session/valiant-boar-161 (PR #3162) per operator direction 2026-05-15 — #3153 has no worker. This PR's
DECISIONS.md carries a — sent from valiant-boar-161 |
…3155) * v4 AGENT-1: place the non-text agent-surface contract (no new file) Operator-ratified 2026-05-15: include & design early, explicitly NOT the north star; an important/exclusive feature but a natural consequence of already-ratified pieces, not a new subsystem. A non-text client (LLM/agent) interacts with the program as data, never files: READ = apply_lens at SectionRef + affected_set(dag,diff) (the affected lens replaces file-reading exploration); WRITE = a structural Node Diff = an ingest (B2-OMNI), content-addressed (B1), not a text patch; BACK = Witness<ReExecFrontier> + faithful re-emit (C5/C4); GATE = apply_lens(Enforce) fail-closed (agent earns no special trust). Homed in lens/application.dag (T-23) as a conspicuous AGENT-SURFACE block — a CLIENT/composition of application.dag + affected_set + B2-OMNI + C5/C4, no new authority/noun/query subsystem (QRY-1 precedent). No new file (closed-tree invariant preserved). Cross-ref back-pointer in 00_compile.dag B2-OMNI; DECISIONS.md AGENT-1 row; TASKS.md T-23 note. affected_set.dag back-ref deferred to avoid conflict with PR #3153. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 AGENT-1 fix: write path enters at `core` (apply_diff), NOT ingest Self-correction. B2-OMNI `ingest:(Source,LanguageModel)->Node` is text-in- a-language → Node. An agent's structural Node Diff is ALREADY Node — it needs no parse/LanguageModel, so it is NOT a Source and NOT an ingest. Correct model: `apply_diff:(Node,Diff)->Node` entering at `core` — `emit ∘ core ∘ apply_diff`, a sibling entry point to ingest. Forcing it through ingest would need a contrived identity "Node-literal language" (the decorative bridge the closed system forbids). Fixed in application.dag (WRITE + BOUNDARY), 00_compile.dag back-ref, DECISIONS.md AGENT-1 row, TASKS.md T-23 note. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 AGENT-1: fix 2 BLOCKINGs — fail-closed apply_diff + defer to affected_set (briansrls #3155) Both valid; the D1↔AGENT-1 reconciliation. :52 — apply_diff:(Node,Diff)->Node is total on EXTERNAL (agent-supplied, possibly invalid/stale) input = fail-open, INVARIANTS P3. D1 (#3162) already ratified the correct shape: apply_diff:(Node,Diff)-> Result<Node,Diagnostic>, fail-closed all-or-nothing. AGENT-1 now USES the D1 op (not a restated total one). application.dag WRITE + DECISIONS AGENT-1 row. :59 — AGENT-1 coined `Witness<ReExecFrontier>` for BACK = an ungrounded noun while claiming "no new authority" (P1/P2). AGENT-1 is a CLIENT: it now defers to affected_set/T-21's OWN declared read shape and coins no return noun. Faithful re-emit tied to the ratified C5-1 (node-level hash-checked) + C5-2 (emit-locality) + C4. Pre-existing QRY-1 block (application.dag ~L31) still cites Witness<ReExecFrontier> as affected_set's archetype — that, and whether affected_set.dag's declared return is Witness<ReExecFrontier> vs Set<NodeRef>/receipts, is an affected_set/T-21 concern (surfaced, not silently changed here — out of #3155 scope). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 AGENT-1: fix the missed 00_compile.dag apply_diff residual (openai-pro #3155 REQUEST_CHANGES) openai-pro correctly caught that the prior BLOCKING fix (application.dag + DECISIONS.md → Result<Node,Diagnostic>) MISSED the 00_compile.dag:18 back-ref, which still showed the total apply_diff:(Node,Diff)->Node. Fixed: it now mirrors ingest's own ->Result<Node,Diagnostic> (sibling at `core`), fail-closed on external/stale agent Diffs (INVARIANTS P3). All three #3155 surfaces (application.dag, DECISIONS AGENT-1 row, 00_compile.dag) now state the D1 fail-closed signature consistently. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 AGENT-1: fix the last residual — TASKS.md T-23 note (codex #3155 REQUEST_CHANGES) codex correctly caught the 4th surface I'd missed: #3155 changed DECISIONS/application.dag/00_compile.dag/TASKS.md; prior fixes covered the first three but TASKS.md:74-80 still carried the total apply_diff:(Node,Diff)->Node + the removed Witness<ReExecFrontier> AGENT-1 noun = parallel authority / internal inconsistency. Now the T-23 note matches the other three: D1 apply_diff:(Node,Diff)-> Result<Node,Diagnostic> (fail-closed, P3) + defers to affected_set's declared shape (no coined noun). All four AGENT-1 surfaces consistent. (TASKS.md:614 + DECISIONS QRY-1 cite Witness<ReExecFrontier> as affected_set's OWN archetype — pre-existing, the affected_set/T-21 declared-shape concern already surfaced separately; out of #3155 scope.) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…#3162) * WIP: v4 design * v4 D1: Diff/Path structural-delta vocabulary over Node Side-session-ratified B-1. EdgeSelector/Path/Edit/Diff data types in std/node.dag (DATA ONLY; A1-clean — Node stays the sole recursive type; B1/Hash precedent for substrate-tier placement). Operations (subterm_at/apply_diff -> Result<Node,Diagnostic>, paths_independent/ diff_well_formed) contracted into lens/application.dag header — forced off node.dag by the diagnostic.dag->node.dag cycle (Correction= Suggested(Node)); the node.dag "consumers fail-close" discipline. affected_set.dag consumes the type. DECISIONS.md Part-1 row D1 carries the data/op-split PROPOSED sub-point for operator confirmation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: v4 design * v4 D1: dissolve two P2 illegal-state surfaces (codex #3162 REQUEST_CHANGES) Both findings valid; fixed structurally rather than patched. Finding 1 (node.dag:~478 ByPosition{index:Int} admits negatives): drop EdgeSelector/ByPosition entirely. Path = List<Symbol> — each step descends the Named edge keyed by that opaque Symbol. No ordinal exists, so the negative/out-of-range illegal state is structurally impossible (dissolved, not deferred to path resolution). Positional-connective children are reached by replacing the enclosing Named subtree (the safe over-fire #3157 blesses); surgical positional addressing is a future operator-ratified extension (consumes-nothing root has no Nat; recursive Peano = A1 STOP). Finding 2 (node.dag:~514 Diff=List<Edit> validity via external predicate): drop the set / pairwise-independence / parallel-positions framing and paths_independent/diff_well_formed. Diff = ORDERED List<Edit> applied SEQUENTIALLY; any List<Edit> is a valid rewrite program (no representable illegal state). A non-resolving Edit => fail-closed Diagnostic at apply time (operational, not a type-level illegal state); apply_diff is a fold, all-or-nothing. Both refine the operator-ratified shape — flagged in DECISIONS.md D1 PROPOSED-for-operator-eye for confirm/redirect. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 D1: add Practice-4 dissolution receipt; fix RATIFIED/PROPOSED contradiction (#3162 BLOCKING) BLOCKING (codex via briansrls relay, vs pre-fix sha a06a066 — verified against current HEAD): - "D1 sum vocabulary without coproduct receipt": the EdgeSelector sum was already deleted in 7c91f73, but the DECISION not to have a positional selector is itself a Practice-4 dissolution requiring the formal 4-pattern ledger (algebra.dag precedent). Added the receipt to std/node.dag D1 (🟢 GREEN terminal: positional addressing subsumed by enclosing-Named-subtree replacement; not a deferred gap). - "root-status driving the index carrier": resolved by the same dissolution — there is no index carrier; the receipt documents why none is needed (vs the reviewer's Nat/Fin suggestion) and why a future surgical form is an explicit operator-ratified extension. Non-blocking: DECISIONS.md D1 row no longer carries a "confirm or redirect" clause inside a RATIFIED row — refinements are stated as encoded-via-PR-review (the normal channel), not an open fork. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 D1: fix stale EdgeLabel cross-reference in node.dag header (cursor #3162 editorial) The D1 header block cited "lines ~221-230" for the no-stored-index discipline, but adding the D1 header block shifted line numbers — that range is now `Connective`. Re-anchored by construct name + corrected approx lines: `type EdgeLabel` ~284 and its "deliberately NO stored index" rationale ~278. Editorial only; cursor APPROVE on this PR. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 B-4: affected_set R2 node-precise-resolution contract Encodes the B-4 cross-cutting decision (operator-greenlit): affected_set minimality requires 04_infer resolution to bind each use-site name-ref to the EXACT declaration Node (not module/scope). The use->def graph is derived by traversal over already-resolved name-references, NOT a 5th InferredFacts field (IR-1-safe; same derive-don't-store discipline as content_hash/D1). Coarse resolution = correct but maximally over-fires. Reciprocal header contracts: 04_infer.dag B-4 block + affected_set.dag Consumes note. DECISIONS.md Part-1 row B-4. Scaffold headers only; no bodies. Continues the v4 design-survey on the session branch alongside D1 (operator sequences/carves at manual merge). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 B-5 + subsume #3153 + B-2 (lean.dag PROOF-1 model) B-5 (affected_set R1 usefulness): effect is a per-Arrow-Node fact from the signature (B3), never aggregated coarse — a granularity invariant (coarse ⇒ R1 correct-but-useless). effect.dag B-5 block + affected_set Consumes/Ex.R1 cross-ref + DECISIONS B-5 row. Subsume #3153 (v4-affected-set-design, no worker — operator-directed): its 4 worked-examples + adversarial R1/R2/R3 + dogfood-reality folded into affected_set.dag as the T-21 design contract, reconciled to the now-ENCODED reciprocal contracts — Ex.R1→B-5 (effect.dag), Ex.R2→B-4 (04_infer.dag), Ex.R3→B-3 (drafted #3157 point-3 correction). #3153 superseded; recommend close. DECISIONS #3153-subsumed row. B-2 (PROOF-1 prover model lands): extdeps/languages/lean.dag (new) — Lean first, termination theorem class; Coq deferred second-prover probe. B2-OMNI requires the LanguageModel file PROOF-1 #3158 deferred. STRUCTURE enumeration+count 63→64; DECISIONS L-4; TASKS PROOF-1 note. Includes the already-committed origin/main merge (204b855: #3158 PROOF-1 + #3160 meta-cut; DECISIONS.md conflict resolved keeping D1/B-4/PROOF-1). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: v4 design * v4 B-4: correct the use→def carrier (Symbol/K-1, not resolved_type) — #3162 BLOCKING Valid P2/Practice-3 finding (briansrls inline @ 04_infer.dag:54): resolved_type is the node's TYPE; many declarations share a type, so it is lossy for binding identity — the use→def fact had no named forward carrier. Corrected: the carrier is the post-resolution opaque Symbol (K-1) on the name-ref Atom, AUTHORED by 03_resolve.dag (binding = Symbol equality, node.dag name_occurrences pattern). 04_infer is preserve-only (no 5th InferredFacts field, IR-1-safe); affected_set derives by Symbol-equality traversal. Fixed consistently across 04_infer.dag B-4 block, new 03_resolve.dag B-4 authority note, affected_set.dag Consumes note, DECISIONS.md B-4 row. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * WIP: v4 design * WIP: v4 design * v4 C5-2 emit-locality + T-9 infer keystone contracts (operator-ratified) C5-2 (emit-locality): emit is structurally local — a D1 apply_diff at Path p re-emits ONLY p's subtree. Per operator code-as-data steer: locality is Node-relative, NOT file-relative; a file is a convenience projection, the substrate anchors no semantic on the file concept; non-local emit = declared normalization at the enclosing NODE scope, never "file scope". The C5↔D1 hinge (AGENT-1 faithful re-emit). 05_emit.dag header + Owns + DECISIONS C5-2 row. T-9 A+B: A — Find decidable by construction (closed declared-inhabitance candidate set, not a synthesized search; structural descent ⇒ the inferencer terminates; empty = decidable fail-closed Diagnostic). B — single-file discipline is the 03_resolve scope boundary (env/scope/ lookup/binding belongs to 03_resolve per B-4; infer owns only Find + cardinality + diagnostic precision). 04_infer.dag header + DECISIONS T-9 row. Receipts: in-header (operator decision; status quo, no change). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 D1: complete the Practice-4 receipt — add Pattern 5 (#3162 codex REQUEST_CHANGES) Valid finding. docs/modeling-discipline.md:112 requires FIVE dissolution patterns; the node.dag #3160 operator-ratified receipts already use 5. The D1 receipt did only 4 (I wrongly followed algebra.dag's older 4-pattern style). Added Pattern 5 (Parameterized family) — FAILS: ByName/ByPosition are not one mechanical F<X> over a declared set (different payload types + addressing semantics; mirror EdgeLabel's genuine 2-variant discriminant, not an enumerated copy à la Homomorphism-per-algebra); no source set to project over (Practice-7 N/A); post-dissolution one constructor = not a family. "four" → "five". Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4 C5-1 + C5-3 (operator-ratified) — node-level round-trip law + spec-provable F C5-1: the bidirectional_roundtrip TestClaim asserts ingest∘emit=id_Node via B1 content_hash (meaning round-trips), NOT text-byte identity. Text-level fidelity recorded as a DEFERRED orthogonal future layer (a trivia sidecar outside Node/content_hash, partial; the C5-fidelity Declared-normalized dispositions are its forward hook — node-level adoption preserves it zero-rework). Non-orthogonal route (lexical in the Node) explicitly rejected. C5-3: F = the spec-provable meaning core; spec silence ⇒ out of F (Declared-normalized or Fail-closed). Conservative/fail-safe — the spec decides, modeler has no discretion; per-language non-F shrinkage declared up front, not discovered at test time. Encoded: lens/testgen.dag C5-1/C5-3 header block + DECISIONS C5-1/C5-3 rows. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * v4: reconcile PROOF-1 row with L-4 — DECISIONS.md self-consistency (cursor #3162 APPROVE_WITH_COMMENTS) Valid NON-BLOCKING finding: B-2 added lean.dag + the L-4 row but the PROOF-1 row still ended "**NO new file** (closed-tree invariant)", contradicting L-4 (which lands extdeps/languages/lean.dag). Reconciled: PROOF-1's framing (#3158) added no file (framing-only, deferred the model "lands later"); that deferred model subsequently lands as lean.dag per B-2/L-4. One coherent story; PROOF-1 row now cross-refs L-4 and states "No contradiction" explicitly. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
D5 receipt: operator blocking review on PR #3349 flagged the synthetic affected_dimension_value sentinel as a fabricated AffectedDimension in ExclusionKey and the D1 current-Dag fold as requiring explicit post-edit Dag authority. Current head already carries AffectedCurrentDagRead through the ordered Diff fold; this commit removes the sentinel boundary-prune key and reconciles DECISIONS.md #3153-subsumed to the bridge-compatible current-Dag read shape.
D5 receipt: reconciles DECISIONS.md #3153-subsumed for non-empty changed-dimension receipts, edit-keyed boundary exclusions, and aggregated per-key ExclusionProof evidence in the T-21 affected_set.dag Wave-0 substrate front.
…graph gate (#3349) * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * Unify affected frontier rerun authority * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * Name transitive affected frontier receipt * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * Fit affected read hooks to bridge * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * Fix affected-set boundary dimension authority D5 receipt: operator blocking review on PR #3349 flagged the synthetic affected_dimension_value sentinel as a fabricated AffectedDimension in ExclusionKey and the D1 current-Dag fold as requiring explicit post-edit Dag authority. Current head already carries AffectedCurrentDagRead through the ordered Diff fold; this commit removes the sentinel boundary-prune key and reconciles DECISIONS.md #3153-subsumed to the bridge-compatible current-Dag read shape. * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * Fail closed post-edit dag receipt D5 receipt: codex current-head review on PR #3349 found the post_edit_dag hook was total despite D1 requiring stale/invalid edits to reject with Diagnostic. This commit makes the post-edit state read return AffectedPostEditDagReceipt with a diagnostic rejection arm and collapses rejected edits to WholeDagFailClosed during the ordered Diff fold. * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * Record affected-set exclusion receipt refinements D5 receipt: reconciles DECISIONS.md #3153-subsumed for non-empty changed-dimension receipts, edit-keyed boundary exclusions, and aggregated per-key ExclusionProof evidence in the T-21 affected_set.dag Wave-0 substrate front. * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * Fix affected-set boundary prune ordering * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * Document affected-set non-empty proof bridge * Import affected-set witness constructor * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra * WIP: T-21 affected_set.dag Wave-0 implementation — IRT-1 whole/changed-subgra
… gates with concrete feature/consumer gates per F11 analysis finding (#3671) * WIP: F11: replace invalid 🟡 tags in affected_set.dag — bare #3153-subsumed g * F11: add bind T-21 to 9 🟡 gates missing dissolution task reference Practice 4 requires each 🟡 gate carry a bound task/PR alongside the feature name and dissolve-on condition. All 9 gates had the feature: and dissolve-on: fields but no explicit bind reference; only BoundaryReceipt was already correct with '— bind T-21 —'. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: add bind T-21 to 9 🟡 gates in affected_set.dag per Practice 4 All 9 gates were missing the bound task token; ExclusionProof also had the bind reference misplaced at the tail of the dissolve-on clause. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
1 participant
Summary
Operator wanted to (a) understand the affected-set lens via worked examples, (b) see it in a PR, and (c) know how fast it can be dogfooded using the frozen v2 seed. This PR delivers the honest version of all three —
lens/affected_set.dagonly (disjoint from #3150/#3151).Granularity, corrected: there is ONE real granularity — node. "File/module-affected" is node-granularity projected up (files containing ≥1 affected node), not a separate tier. (Retracts my earlier two-tier framing.)
4 worked examples embedded as the T-21 design contract (node-granularity, target-agnostic fact):
NamedReasonvariant → forward-closure frontier; the pure helper is skipped (inputs unchanged + pure ⇒ provably same output).content_hashunchanged (K-1/B1 α-equivalence) → ∅ frontier, zero recompute — the payoff, by the hash.Honest v2-dogfood reality (verified, not hoped):
runinterpreter and emits a structureddag-artifact.json, but that artifact is module-level, not the Node tree — and v2 is the frozen seed (can't enrich its emission, A3). No node-granularity path through v2; node-granularity arrives with the v4 pipeline at T-9. No v2 shortcut exists.imports/items); it cannot compile its ownsrc/v2/*.dagor v3dsl/. So today there is no corpus with real edges to compute an affected-set over. A demo over edge-empty stubs would be theater — forbidden (no-engine). I did not build a fake "it runs."dag-artifact.jsonviav2-compiler run, once v4 files carry realimport/declarations (gated on v4 T-1: model std/node.dag — the substrate root #3151 → T-1/T-3) and the v2-interpreter pre-flight (canv2-compiler runexecute the affected-set.dagover the artifact?) is verified. That pre-flight is now on the critical path for the dogfood goal.This is the honest "see it": the precise design contract you can read + react to, and the real lever, with no fabricated demo.
Test plan
cargo fmt --all --checkclean🤖 Generated with Claude Code