Repository navigation
Conversation
Adds six proposed Layer-1 lenses derived from the 2026-05-18 review ingest against `main@e7b8a8d` (corroborated against worktree HEAD). Each section follows the existing L1.x format (signature / decidability / verdict / escape / kills) and includes concrete code-level match cases + clean-shape examples, so the structural signature is reviewable without chasing repo paths. - L1.7 Off-substrate-fact — prose-asserted facts (F3 lattice, F4 width, F11 opacity). Generalizes the standing "machine-readable inhabitance" ruling. - L1.8 Wrong-home — orphan operations (F5 `nat_compare` in float.dag). Mechanizes MODELING M9. - L1.9 Vacuous-arm — exhaustive-but-empty match (F1 `ComputationNode { behavior: _ } => true`). - L1.10 String-escape-hatch — typed-model bypass via String (F6 `ShellCommand { command: String }` vs typed `process.Command`). Generalizes L1.6. - L1.11 Plausible-fallback — fabricated-sibling fallthrough (F10 `DELETE None => CreateEffect`). - L1.12 Parallel-authority — unmarked duplicate concept homes (F9 `dsl/std` vs `src/v4/std`; D2-resolver provisional + planned-absent). Each carries `Status: proposed` in the section header. Slipped-by ledger (§8) gains corresponding rows pinned to current main file locations so the evidence is grep-anchored per §3 methodology. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…y gap cursor/composer-2 review noted that the F9 "Concrete match" block implied both `dsl/std/types.dag` and `src/v4/std/logic.dag` were bare, when both files actually carry annotations above their `type Bool` line (legacy-scanner anchor prose in dsl/std/types.dag:163-172; 🟢 coproduct-dissolution classification tag at src/v4/std/logic.dag:13). The lens's case is sharper, not weaker, once the existing tags are visible: they classify the finding shape (dissolution status, scanner anchor) but neither *designates authority* between the two parallel declarations. L1.12 specifically requires a designator that picks a canonical winner, which is the gap classification tags don't fill. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Addresses three BLOCKING findings on the L1.7–L1.12 proposal:
L1.7 — width discharge must be recursive. The previous signature/clean
shape allowed a `Word64 { bytes: List<Byte> where len(_) == 8 }` that
bottomed out at an unconstrained `Byte`, so an arbitrary-bit-count
`Byte` still inhabited a "well-formed" `Word64`. Signature now requires
a recursively-discharged refinement chain down to a fixed-cardinality
leaf or primitive bit; clean-shape example shows the full
Word64 → Byte → Bit chain and structurally distinct Float32/Float64
exponent/significand widths instead of a shared `FloatBody`.
L1.8 — primary-concept selector replaces the argument-files heuristic.
Previous signature ("every argument's type lives in file X") missed
witness-target homing (a `meet` field of `Lattice<T>` belongs with T,
not with whichever file declared its argument types). New four-rule
structural cascade in priority order:
(1) declared witness target → algebra's type parameter is the home;
(2) same-type closure (`fn(T,T)→T` etc.) → T is the home;
(3) upstream argument+return convergence on file X → X is the home;
(4) no single owner → cross-cutting, lens does not fire.
L1.12 — escape valve must be structural, not prose. The previous
"// Authority: canonical | historical" comment markers were prose-
as-authority — exactly the shape L1.7 exists to kill. The lens is now
self-consistent: only structural shapes discharge it — alias/import
identity from historical to canonical, a `data ... :
HistoricalDeclaration` row in a retirement ledger read as data, or
deletion+migration in the same change. Comment markers explicitly do
not satisfy the escape, by construction.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…cts only Addresses three BLOCKING findings from codex review on cfbc247: L1.9 — replace function-name suffix vocabulary with intra-match asymmetry. The previous signature gated on `*_well_formed` / `*_valid` suffixes — naming as a structural fact, which violates P1 ("heuristics are never structurally necessary"). New signature is purely structural: a single match where ≥1 arm has a trivial-literal RHS AND ≥1 sibling arm does non-trivial structural work. The discipline-role is inferred from the fact that the author already wrote real work for some variants, which makes the trivial siblings a vacuum. The F1 node_locally_well_formed case still fires (TypeNode arm calls edges_conform, ComputationNode arm returns true). L1.10 — replace hardcoded `command`→Command / `path`→Path / `url`→Url field-name table with a substrate-declared canonical-carrier registry. A typed carrier declares `data X: CanonicalCarrier<X> = { supersedes_string: { in_role: <role-tag> } }`; the lens reads the registry. Adding a new typed carrier is now a `data` row in `extdeps/`, not an edit to the lens definition. The lens carries no domain names. L1.12 — split planned-absent-import out of the duplicate-authority lens. They are different failure shapes: duplicate `type T` in two files is a duplicate-authority finding; a dangling import path is an unresolved-reference / fail-closed P3 finding. Collapsing them under one verdict reports the wrong root cause. L1.12 narrows to duplicate-declaration; planned-absent moves to an L0.8-extended row in the slipped-by ledger. The D2-resolver concrete-match block is retitled as a cross-reference note explaining why it does *not* collapse into L1.12. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
codex review on 3fb3e4d raised two valid findings: L1.10 — the role-tag refinement created an opt-in opportunity for authors to bypass the typed-carrier rule by omitting the tag. The escape "no role-tag refinement, passes" was convention-level enforcement, not API-level. New signature drops the role-tag mechanism entirely. The CanonicalCarrier registry declares a `supersedes_string_at_field_named` set (substrate data); the lens fires on any String field whose name appears in any in-scope registry entry, unconditionally. The author cannot bypass by omitting an annotation because there is no annotation — the trigger is the field name they chose plus the registry-declared coverage. Legitimate raw-string exemptions move to structural Exemption rows in the same registry, read as data. L1.12 — the prior signature said "type T = ..." literally, which only matches the alias/sum form. The slipped-by ledger row claims coverage of duplicate machine-word homes, but `type Word64 { bytes: List<Byte> }` is record form and would have escaped the literal signature. Broadened to "any `type T` declaration form" — sum/alias, record, unit, generic — with explicit enumeration of the covered forms so the signature unambiguously matches the cases in the section's own examples and ledger. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The original L1.1–L1.6 sections describe each lens by signature /
decidability / verdict / escape / kills, but did not show what the
matching code or the discharging code actually look like. Adds the
same "Concrete match" + "Clean shape" example blocks the proposed
L1.7–L1.12 sections use, so each lens is concretely readable without
chasing the referenced PRs.
- L1.1: basic discriminant shape (`nat_is_zero`) + the laundered
constant-algebra fold (`free_monoid_is_empty`-via-fold).
- L1.2: (a) struct-of-functions (`ListMap<A,B>` wrapper) and (b) N
near-identical single-field structs (`{ spelling: String }` ×N).
- L1.3: declared-but-never-inhabited type (`ParseError` with no
constructor, no `data`, no alias, no field).
- L1.4: `Outcome<T>` clone (`NormalizeChildrenResult`), with the
three-variant `Cached | Produced | Rejected` shape as the escape.
- L1.5: clean recursion mirroring data shape (`ci_member` over List)
and the short-circuit `match acc { Rejected => propagate; Ok =>
continue }` ladder (resolve/normalize walkers).
- L1.6: type-construction template tables (`list_template: "Vec<{0}>"`)
vs. structural target-type modeling.
No signature, verdict, or escape semantics changed; this commit only
adds illustrative code blocks.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Implements the consolidation feedback as a middle path: tightens the
conceptual scaffolding without dismantling the lens catalog.
- §1: introduces A0 ("every semantic fact must have exactly one
structural witness") as the umbrella invariant, with A1 retained
underneath as the operation-specific specialization. Explicitly
framed as operationalizing modeling-discipline.md Practice 10, not
as a parallel rulebook, to avoid the L1.12-class parallel-authority
hazard of duplicating Practice 10's principles here.
- §5.0 (new): adds the three-levels framing (Invariant / Theme / Lens),
the lens → theme(s) catalog (derive / witness / canonical-home /
fail-closed), and the explicit disclaimer "themes are explanatory
tags only — they do not define CI gates, test-corpus boundaries, or
implementation passes; the mechanically enforced unit remains the
L1.x lens signature." Per the §3 methodology, each lens's signature
must be the smallest structural pattern that catches its finding's
class with zero false positives, so theme-sharing alone does not
collapse machinery.
- L1.6 → L1.10 merge: the only mechanical merge in this rev, because
the prior doc already stated that L1.10 generalizes L1.6. L1.10 is
renamed "Textual-bypass lens" with two sub-signatures:
L1.10.a TemplateHole — registry-free, catches `{0}`/`{1}`
positional-placeholder string
literals used as emitters
L1.10.b CanonicalCarrier — substrate-declared registry, catches
String fields whose name appears in
a CanonicalCarrier coverage set
L1.6 section becomes a one-paragraph pointer to L1.10.a, preserving
anchor compatibility. The slipped-by ledger's F6 row is repointed to
L1.10.b and a new F8 row is added for L1.10.a.
L1.2/L1.3/L1.4, L1.8/L1.12, and L1.9/L1.11 are intentionally not
merged — their detection machines are mechanically distinct (different
signatures, decidability arguments, escape valves) and the operator
TDD-pairs directive requires distinct test corpora per lens. They
share themes in the §5.0 catalog without sharing implementation.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Five sharpening edits from operator review of the A0/themes pass:
1. A0 rephrased: "exactly one structural witness" → "exactly one
canonical structural witness *path*". Alias / re-export edges,
retirement-ledger rows, and derived operations reading the same
witness all point at one authority; they are the path, not a
multiplicity that violates A0.
2. §2 "one substrate gap" claim updated. The original sentence was
true for the L1.1/L1.5 seed findings but too narrow for A0's
broader territory. Now distinguishes the seed gap (no derived
discriminant/catamorphism → workers hand-roll them) from the
general gap (missing witness table / authority map / refinement
edge / diagnostic carrier → workers encode locally in prose /
names / strings / duplicate homes / plausible defaults).
3. L1.10 explicitly renamed "Textual-bypass lens family" with an
"Exception to §5.0" note: L1.10.a TemplateHole and L1.10.b
CanonicalCarrier are the mechanical units, sharing a finding
family and reporting label but keeping separate signatures,
decidability arguments, escapes, and test corpora. Resolves the
tension between §5.0 ("the mechanically enforced unit is the L1.x
signature") and L1.10's two-detector structure.
4. L1.6 stub retitled "Deprecated alias — see L1.10.a `TemplateHole`"
so old test names and slipped-by references remain traceable.
5. §8 trailing prose fixed: "all four are burn-down substrate PRs"
was true when the ledger had four rows; now it has the four seed
rows plus the ingest extension. Reframed as "Pattern from the seed
PR rows" with an explicit note that the ingest rows extend the
ledger to A0's broader territory.
6. A0/A1 ratification sentence made authority-chain explicit: "Once
ratified into Practice 10, A0/A1 become citable hard rules; this
doc remains the enforcement mechanism." Avoids the rulebook-ish
phrasing that suggested A0/A1 were independently citable.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds a new §10 (renumbering audit to §11) answering the "how does this run / is it parallelizable / how much work" questions operationally. The core framing: there is no "lens framework" separate from the compiler pipeline. Lenses are .dag stages that declare consumes: edges against the existing parse/resolve/infer producers, and the compiler's stage-ordering schedules them automatically. - §10.1: shared-indices taxonomy — maps each shared structural fact (AST, symbol resolution, variant lists, inhabitance edges, witness registries, refinement clauses, import graph, fail-closed return- type carriers) to the existing pipeline stage that produces it and the lenses that consume it. Most of what lenses need is already computed; lenses just query. - §10.2: three small derived stages cover what the existing pipeline doesn't yet expose — match_arm_shape (reusable by L1.1, L1.9, L1.11, L0.7, L0.13), closed_vocab_scan (L1.7), concept_home (L1.8). Each is a single deterministic fold; reusable across multiple lenses by design. - §10.3: a lens is just another .dag stage with declared dependencies. Adding a lens = land a stage; the existing compiler stage-ordering handles scheduling. No new framework. - §10.4: per-file and per-lens parallelism fall out of the dependency graph automatically; affected_set integration scales CI cost with PR size, not corpus size. - §10.5: summary of operational properties — one dependency model across pipeline + lenses, lens addition = stage land, index addition = small derivation stage shared by all lenses that need it, self-application clean (the compiler enforces the discipline it follows). This is the L1.12-class self-consistency check: a separate "lens framework" with its own dependency model would itself be parallel authority, which the lens suite exists to kill. The dependency-model section makes explicit that the lens framework reuses the pipeline's existing modeling — one dependency system for everything. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Closing — #3313 (the original dissolution-lens design PR for this session) was squash-merged to main at |
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
Auto-opened by session-dashboard for session
sunny-wolf-435.Pushing to
session/sunny-wolf-435advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan