Repository navigation
feat(v3): T-Substrate-Lens-Primitive — Lens<C> carrier + Q6.5 widening #1186
There are no files selected for viewing
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
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,163 @@ | ||
| //! **Layer:** integration | ||
| //! | ||
| //! Acceptance for the T-Substrate-Lens-Primitive first slice | ||
| //! (`docs/design-lens-framework.md`, `docs/briefs/r2-substrate-manager.md`). | ||
| //! | ||
| //! Director-locked option (c) per parent inbox #1130 dispatch: | ||
| //! - `Lens<C>` lands in `src/v3/std/lens.dag` with the locked 6-field | ||
| //! shape (`name`, `read`, `sequential: Monoid<C>`, `branch`, `iterate`, | ||
| //! `validate`). | ||
| //! - `Diagnostic.kind` widens from `CompilerDiagnosticKind` to | ||
| //! `AnyDiagnosticKind`; the Layer-1 closed sum stays unchanged. | ||
| //! - `LensInstanceKindWitness` is decl-only (no payload value field) | ||
| //! until refinement/dependent typing lands; this is the explicit | ||
| //! substrate gap receipt. | ||
|
|
||
| use std::collections::HashSet; | ||
| use v3_compiler::dag::{Dag, DeclarationId, TypeConnective}; | ||
| use v3_compiler::generated_full_bootstrap_dag; | ||
|
|
||
| fn conj_field_labels(dag: &Dag, name: &str) -> Vec<String> { | ||
| let decl = dag | ||
| .declaration_by_name(name) | ||
| .unwrap_or_else(|| panic!("`{name}` missing from full bootstrap")); | ||
| match &decl.connective { | ||
| TypeConnective::Conj { children } => children.iter().map(|f| f.label.clone()).collect(), | ||
| other => panic!("`{name}` is not a Conj: {other:?}"), | ||
| } | ||
| } | ||
|
|
||
| fn disj_variant_labels(dag: &Dag, name: &str) -> Vec<String> { | ||
| let decl = dag | ||
| .declaration_by_name(name) | ||
| .unwrap_or_else(|| panic!("`{name}` missing from full bootstrap")); | ||
| match &decl.connective { | ||
| TypeConnective::Disj { variants } => variants.iter().map(|v| v.label.clone()).collect(), | ||
| other => panic!("`{name}` is not a Disj: {other:?}"), | ||
| } | ||
| } | ||
|
|
||
| fn decl_id_by_name(dag: &Dag, name: &str) -> DeclarationId { | ||
| dag.declaration_by_name(name) | ||
| .unwrap_or_else(|| panic!("`{name}` missing from full bootstrap")) | ||
| .id | ||
| } | ||
|
|
||
| #[test] | ||
| fn lens_carrier_has_locked_six_field_shape() { | ||
| let dag = generated_full_bootstrap_dag(); | ||
| let labels: HashSet<String> = conj_field_labels(&dag, "Lens").into_iter().collect(); | ||
| let expected: HashSet<&str> = [ | ||
| "name", | ||
| "read", | ||
| "sequential", | ||
| "branch", | ||
| "iterate", | ||
| "validate", | ||
| ] | ||
| .into_iter() | ||
| .collect(); | ||
| let actual: HashSet<&str> = labels.iter().map(String::as_str).collect(); | ||
| assert_eq!( | ||
| actual, expected, | ||
| "Lens<C> field set diverged from Director-locked 6-field shape" | ||
| ); | ||
| } | ||
|
|
||
| #[test] | ||
| fn diagnostic_kind_widened_to_any_diagnostic_kind() { | ||
| let dag = generated_full_bootstrap_dag(); | ||
| let any_id = decl_id_by_name(&dag, "AnyDiagnosticKind"); | ||
|
|
||
| let diag_decl = dag | ||
| .declaration_by_name("Diagnostic") | ||
| .expect("Diagnostic missing from full bootstrap"); | ||
| let kind_field = match &diag_decl.connective { | ||
| TypeConnective::Conj { children } => children | ||
| .iter() | ||
| .find(|f| f.label == "kind") | ||
| .expect("Diagnostic missing `kind` field"), | ||
| other => panic!("Diagnostic is not a Conj: {other:?}"), | ||
| }; | ||
| assert_eq!( | ||
| kind_field.ty, any_id, | ||
| "Diagnostic.kind must point at AnyDiagnosticKind, not the Layer-1 closed sum" | ||
| ); | ||
| } | ||
|
|
||
| #[test] | ||
| fn compiler_diagnostic_kind_closed_sum_unchanged() { | ||
| let dag = generated_full_bootstrap_dag(); | ||
| let variants: HashSet<String> = disj_variant_labels(&dag, "CompilerDiagnosticKind") | ||
| .into_iter() | ||
| .collect(); | ||
| let expected: HashSet<&str> = [ | ||
| "TokenizerError", | ||
| "ParseError", | ||
| "TypeMismatch", | ||
| "UnitMismatch", | ||
| "ArityMismatch", | ||
| "ResolveError", | ||
| "NominalOpacityViolation", | ||
| ] | ||
| .into_iter() | ||
| .collect(); | ||
| let actual: HashSet<&str> = variants.iter().map(String::as_str).collect(); | ||
| assert_eq!( | ||
| actual, expected, | ||
| "CompilerDiagnosticKind closed sum changed — Layer-1 must stay locked; \ | ||
| lens-instance kinds enter via Layer-2 LensInstanceKindWitness, NOT \ | ||
| by extending this sum (anti-bridge invariant per Q6.5)" | ||
| ); | ||
| } | ||
|
|
||
| #[test] | ||
| fn any_diagnostic_kind_has_two_layer_constructors() { | ||
| let dag = generated_full_bootstrap_dag(); | ||
| let variants: HashSet<String> = disj_variant_labels(&dag, "AnyDiagnosticKind") | ||
| .into_iter() | ||
| .collect(); | ||
| let expected: HashSet<&str> = ["CompilerKind", "LensInstanceKind"].into_iter().collect(); | ||
| let actual: HashSet<&str> = variants.iter().map(String::as_str).collect(); | ||
| assert_eq!( | ||
| actual, expected, | ||
| "AnyDiagnosticKind must have exactly two constructors — Layer-1 \ | ||
| CompilerKind(CompilerDiagnosticKind) and Layer-2 \ | ||
| LensInstanceKind(LensInstanceKindWitness)" | ||
| ); | ||
| } | ||
|
|
||
| #[test] | ||
| fn lens_instance_kind_witness_payload_intentionally_absent() { | ||
| // Layer-2 substrate gap receipt (per parent #1130 dispatch + Q6.5 | ||
| // §State-space discipline). Today's .dag grammar cannot express | ||
| // `payload: <inhabits kind_decl.payload>` — a refinement-type-on- | ||
| // sibling-field shape. The flat alternative (free `TypeShape` | ||
| // payload coordinate) ratifies the very illegal state Q6.5 rejects: | ||
| // `(Lens<TenantFlow>, "WrongName", payload-of-different-shape)`. | ||
| // | ||
| // Director-approved option (c): land Layer-2 kind identity and | ||
| // namespace authority via `LensInstanceKindWitness { kind_decl }` | ||
| // alone; the structured payload value is intentionally NOT carried | ||
| // through the substrate until dependent-field typing or substrate | ||
| // inhabitance witnesses lower without hand-Rust scaffolding. | ||
| // | ||
| // This test pins the gap. When that grammar feature lands and | ||
| // `LensInstanceKindWitness` grows a checked `payload` field, this | ||
| // test fails loudly and forces the dissolution-trigger comment in | ||
| // `diagnostics.dag` to retire in lock-step. | ||
| let dag = generated_full_bootstrap_dag(); | ||
| let labels: HashSet<String> = conj_field_labels(&dag, "LensInstanceKindWitness") | ||
| .into_iter() | ||
| .collect(); | ||
| let expected: HashSet<&str> = ["kind_decl"].into_iter().collect(); | ||
| let actual: HashSet<&str> = labels.iter().map(String::as_str).collect(); | ||
| assert_eq!( | ||
| actual, expected, | ||
| "LensInstanceKindWitness field set drifted. Adding a `payload` \ | ||
| field is a substantive change — verify the dependent-field \ | ||
| typing trigger in `diagnostics.dag` has actually closed before \ | ||
| landing it (do not pretend payload is enforced via a free \ | ||
| TypeShape coordinate; that is the Q6.5-rejected illegal state)." | ||
| ); | ||
| } |
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
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
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 |
|---|---|---|
| @@ -1,14 +1,23 @@ | ||
| module v3.std.diagnostics | ||
|
|
||
| import std.list { List } | ||
| import v3.spec.v3_l1 { DeclarationRef } | ||
| import v3.std.substrate { SourceSpan, TypeShape } | ||
|
|
||
| // 🟡 SCAFFOLD. Mirrors the compiler's native diagnostic taxonomy for | ||
| // the staged v3 diagnostics surface. Kept distinct from | ||
| // `std.verification.DiagnosticKind` to avoid introducing a second | ||
| // imported top-level declaration with the same name during bootstrap. | ||
| // Dissolution trigger: reflected diagnostics or a shared diagnostic | ||
| // kind authority once the staged/bootstrap-local split disappears. | ||
| // | ||
| // Layer 1 (per `docs/design-lens-framework.md` Q6.5 two-layer | ||
| // authority): Substrate-Manager-owned closed sum of compiler-primitive | ||
| // diagnostic kinds. Layer-2 lens-instance kinds live separately under | ||
| // `DiagnosticKindDecl` / `LensInstanceKindWitness` below — they MUST | ||
| // NOT be added as variants here. Adding a Layer-1 kind is rare, | ||
| // design-locked, and requires SCAFFOLD-note acknowledgment of where | ||
| // the diagnostic surfaces. | ||
| type CompilerDiagnosticKind | ||
| = TokenizerError | ||
| | ParseError | ||
|
|
@@ -30,11 +39,87 @@ type Correction { | |
| new_source: String | ||
| } | ||
|
|
||
| // Layer 2 lens-instance diagnostic-kind declaration (per | ||
| // `docs/design-lens-framework.md` Q6.5). A `DiagnosticKindDecl` | ||
| // appears inside the `diagnostic_kinds` list of an `inhabits Lens<C>` | ||
| // declaration; the containing inhabitance IS the owning lens (P2 | ||
| // single-authority via structural containment, NOT via a duplicated | ||
| // `lens_instance` field). The decl's `name` MUST NOT collide with any | ||
| // `CompilerDiagnosticKind` Layer-1 variant name (anti-shadowing | ||
| // protocol per Q6.5 §Name-collision protocol). | ||
| // | ||
| // 🟡 TRANSITIONAL. Owner-by-containment is the structural authority, | ||
| // not a re-declared field. The decl name is a String today; refines | ||
| // to a typed `KindName` namespace-scoped to the parent lens once the | ||
| // substrate exposes namespace-typed identifiers. | ||
| type DiagnosticKindDecl { | ||
| name: String | ||
| payload: TypeShape | ||
| } | ||
|
|
||
| // Layer 2 lens-instance kind witness (per Q6.5 §Substrate change | ||
| // required). A structural pointer to a declared `DiagnosticKindDecl`. | ||
| // | ||
| // 🟡 SCAFFOLD coproduct (single-arm record). Pattern 1 (per-call | ||
| // payload typing) fails because the payload's TypeShape is dependent | ||
| // on the runtime-resolved `kind_decl.payload` field — `.dag` grammar | ||
| // today cannot express `payload: <inhabits kind_decl.payload>` | ||
| // (refinement-type-on-sibling-field). Pattern 2 (collapse to a flat | ||
| // `{ kind_decl, payload_kind_shape }` record with a free `TypeShape` | ||
| // payload coordinate) ratifies exactly the parallel-authority illegal | ||
| // state Q6.5's §State-space discipline rejected — three independent | ||
| // coordinates (lens / name / payload-shape) that admit | ||
| // `(Lens<TenantFlow>, "WrongName", payload-of-different-shape)`. | ||
| // Pattern 3 is the dissolution path: when refinement/dependent field | ||
| // typing OR declaration-shaped inhabitance witnesses land in the .dag | ||
| // substrate, this carrier grows a checked `payload` value field | ||
| // constrained to inhabit the shape `kind_decl.payload` names; until | ||
| // then the witness is decl-only — Layer-2 kind identity and | ||
| // namespace authority are present, but the structured payload value | ||
| // is intentionally NOT carried through the substrate. Trigger: | ||
| // dependent-field typing or substrate inhabitance witnesses lower | ||
| // without hand-Rust scaffolding. | ||
| // | ||
| // Note on `kind_decl` typing: bare `DeclarationRef` admits any | ||
| // declaration. The structural constraint (\"must resolve to a | ||
| // `DiagnosticKindDecl` whose parent is the owning `Lens<C>` | ||
| // inhabitance\") is checked fail-closed at the runtime resolution | ||
| // boundary — same residual class as `PatternRealization` (`emit_model.dag` | ||
| // lines 140–152, where `empty_variant`/`cons_variant` admit any | ||
| // declaration but are validated as variants-of-target at parse time) | ||
| // and `MethodTemplateContract.dag_method` (`emit_model.dag:371`). | ||
| // Refining to `DeclarationRef<DiagnosticKindDecl>` is part of the | ||
| // SAME dissolution trigger above — substrate-level | ||
| // refinement-typing-on-DeclarationRef is the mechanism that closes | ||
| // both the payload-typing gap and the kind-decl resolution gap in | ||
| // one move. | ||
| type LensInstanceKindWitness { | ||
| kind_decl: DeclarationRef | ||
|
Contributor
Author
There was a problem hiding this comment. Same residual class as the existing Per parent-inbox #1130 dispatch (verbatim) on the option (c) lock: "For Q6.5, do not encode a fake dependent payload. Add The dispatch explicitly accepted bare |
||
| } | ||
|
|
||
| // Two-layer diagnostic-kind parent (Q6.5). `Diagnostic.kind` widens | ||
| // from `CompilerDiagnosticKind` to this sum so a single `Diagnostic` | ||
| // value can carry either Layer-1 (substrate-owned closed sum) or | ||
| // Layer-2 (lens-namespace-scoped) kinds without re-introducing a | ||
| // cross-manager handoff for lens-instance kind authoring. | ||
| // | ||
| // Anti-bridge invariant (Q6.5): adding a lens-instance kind MUST NOT | ||
| // extend `CompilerDiagnosticKind` — Layer-2 kinds enter via | ||
| // `LensInstanceKind(LensInstanceKindWitness)` exclusively. The closed | ||
| // Layer-1 sum stays the authority for compiler-primitive kinds only. | ||
| type AnyDiagnosticKind | ||
| = CompilerKind(CompilerDiagnosticKind) | ||
| | LensInstanceKind(LensInstanceKindWitness) | ||
|
|
||
| // 🟡 SCAFFOLD until reflected diagnostics replace the compiler's | ||
| // native enum. The record shape is the authority for consumers that | ||
| // only need the diagnostic carrier, including `fixes`. | ||
| // | ||
| // `kind: AnyDiagnosticKind` carries either Layer-1 (closed-sum | ||
| // compiler-primitive) or Layer-2 (lens-instance, namespace-scoped) | ||
| // kinds per Q6.5 two-layer authority. | ||
| type Diagnostic { | ||
| kind: AnyDiagnosticKind | ||
| span: SourceSpan | ||
| message: String | ||
| fixes: List<Correction> | ||
|
|
||
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,77 @@ | ||
| // std.lens — `Lens<C>` substrate carrier (Director-locked 6-field shape). | ||
| // | ||
| // 🟡 TRANSITIONAL. First substrate slice for the lens framework | ||
| // (`docs/design-lens-framework.md`). This carrier authors the structural | ||
| // shape generic compositional analyses fold over the 5 L1 behaviors; | ||
| // `fold_lens<C>: Lens<C> → Dag → DimensionReport<C>` and the four worked | ||
| // instances (complexity / tenant-flow / IFC / cost-lens) consume this | ||
| // shape in subsequent lanes (R3-T-CostLens-Composition, | ||
| // R2-Evaluator PR-A..E, T-LensAPI rescope). | ||
| // | ||
| // The `Lens<C>` carrier deliberately reuses existing substrate types — | ||
| // `Witness<C>` / `OptionalDiagnostic` / `DimensionReport<C>` from | ||
| // `dimensions.dag`, `Monoid<C>` from `dsl/std/algebra.dag`, `Diagnostic` | ||
| // from `diagnostics.dag` — rather than authoring parallel | ||
| // representations (per `feedback_parallel_representation_debt`). | ||
| // | ||
| // Home: `src/v3/std/` (not `dsl/std/`). The carrier references v3-only | ||
| // substrate types (`Dag`, `Behavior`, `LoopBound`, `DeclarationRef`), | ||
| // so `dsl/std/lens.dag` would need import inversions. Convergence | ||
| // trigger: when v3 substrate types graduate into shared `dsl/std/`, | ||
| // this file moves to `dsl/std/lens.dag` alongside `dsl/std/algebra.dag`. | ||
|
|
||
| module v3.std.lens | ||
|
|
||
| import std.list { List } | ||
| import std.algebra { Monoid } | ||
| import std.substrate { Dag, Behavior, LoopBound } | ||
| import v3.std.dimensions { Witness, OptionalDiagnostic, DimensionReport } | ||
|
|
||
| // 🟢 TERMINAL at the lens-primitive scope. The six fields are the | ||
| // irreducible contract a generic compositional analysis publishes: | ||
| // | ||
| // - `name` — human-facing dimension identifier; populates | ||
| // `DimensionReport.dimension_name`. | ||
| // - `read` — per-Behavior cost-basis extraction. Returns | ||
| // `Witness<C>` (NOT `C`) so a missing per-Behavior | ||
| // substrate fact surfaces as `Violates` rather than | ||
| // fabricating a default carrier (fail-closed). | ||
| // - `sequential` — `Monoid<C>` for `BindNode` composition. Structural | ||
| // inhabitance over `Monoid<C>` (`dsl/std/algebra.dag`) | ||
| // means the monoid law (associativity + identity) is | ||
| // structurally enforceable, not merely documented. | ||
| // Replaces the prior parallel `compose: (C,C)->C` + | ||
| // `unit: C` field pair (Director directive 2026-04-28 | ||
| // + gpt-5-5-pro Finding #4: same drift shape as | ||
| // `AnalysisDimension<Carrier>` already carried). | ||
| // - `branch` — exclusive-choice composition for `BranchNode`. NOT | ||
| // a monoid op; only one arm runs at runtime, so | ||
| // composition is `max/join` over arms. No identity | ||
| // element is required (no "no-op branch"). | ||
| // - `iterate` — bounded iteration for `LoopNode`. Takes the body | ||
| // cost and the loop's `LoopBound` and returns the | ||
| // loop-iteration cost. | ||
| // - `validate` — aggregate side-condition check after the fold has | ||
| // composed all per-Behavior witnesses. Returns | ||
| // `OptionalDiagnostic` (NOT `Witness<C>`) because by | ||
| // this point there is no single Behavior to attach a | ||
| // per-node `at:` reference to; aggregate-level | ||
| // diagnostics use `Diagnostic.span`. The `Dag` | ||
| // parameter carries program-structure context | ||
| // (workflow capability grants, sink declarations, | ||
| // etc.) that side-conditions look up structurally. | ||
| // | ||
| // Why three composition operations and not four (sequential / branch / | ||
| // iterate, no parallel): v3 has three composition primitives among the | ||
| // 5 L1 behaviors — `BindNode`, `BranchNode`, `LoopNode`. There is no | ||
| // `ParallelNode`; auto-parallelism is *emergent* from dependency-graph | ||
| // analysis on `BindNode` sequences, not a declared substrate primitive. | ||
| // The lens framework declares operations over the actual L1 behaviors. | ||
| type Lens<C> { | ||
| name: String | ||
| read: fn(Dag, Behavior) -> Witness<C> | ||
| sequential: Monoid<C> | ||
| branch: fn(C, C) -> C | ||
| iterate: fn(C, LoopBound) -> C | ||
| validate: fn(Dag, C) -> OptionalDiagnostic | ||
| } |
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.
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.
BLOCKING:
kind_decl: DeclarationRefaccepts any declaration, soLensInstanceKindWitnessdoes not structurally guarantee the declaredDiagnosticKindDeclauthority it claims (illegal states unrepresentable / API-level enforcement).