Skip to content

Lane 7: inert-abstraction lens keystone + non-fold-residue audit (fail-closed walls) - #5566

Merged
briansrls merged 21 commits into
mainfrom
session/lively-gull-506
Jun 23, 2026
Merged

briansrls merged 21 commits into
mainfrom
session/lively-gull-506

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Jun 22, 2026 •

Copy link
Copy Markdown
Contributor

Lane 7 — inert-abstraction lens keystone + non-fold-residue audit

Two fail-closed walls (DESIGN §5/§6), per docs/plans/upcoming-work-dispatch-plan.md Lane 7 and docs/plans/fold-ergonomics.md §3 #3.

1. Inert-abstraction lens (the keystone)

Generalizes the #5433 inert-lens floor backstop (walls unreached v2.lens.* modules) to type carriers: a carrier that is defined + self-tested + zero real consumer is DESIGN §5 coverage-by-illusion (a green test, no production consumer). The self-tested gate is what makes it a clean keystone rather than "every unused type" — it filters from the project's deliberate model-first staging (extdeps surfaces, the realization loop) down to the precise §5 trap.

  • Host census src/v1/stage0/src/inert_carrier_project.rs (mirrors doc_reachability_project.rs): inert iff declared once ∧ self-tested ∧ zero use outside its own declaration block (same-file fn use counts as a consumer — so lens-local fact types are not false-flagged).
  • .dag surface v2.lens.inert_carrier with construction_justification (WallAfterGrounding).
  • Floor witness src/v2/lens/inert_carrier_test.dag (fail-closed, importing the lens so it is itself reached → not inert-lens).
  • 8 inert carriers (AccessPolicy, CargoDependency, CargoPackage, FilePermissions, FloorWitnessRow, GitCliReportedVersion, ReactHookSite, SecretValue) on a named, shrinking roster with a stale-roster ratchet. (Seeded at 9; RbacPolicy then dropped off the roster when a real consumer landed via the ae891fcf8f main merge — extdeps/bmc/access.dag's redfish_rbac_policy — i.e. the stale-roster ratchet working as intended.)

2. Non-fold-residue audit

DESIGN §6: a finished stage is one fold; any non-fold residue is a named irreducible kernel or un-migrated modeling. A match over a CLOSED coproduct with a _ => wildcard carries a fail-open escape a total fold would not.

  • Host census src/v1/stage0/src/non_fold_residue_project.rs: flags a match whose scrutinee is a bare fn-param of a known closed-coproduct type carrying a top-level _ => arm (conservative — field accesses / open domains / field-placeholder _ excluded).
  • .dag surface v2.lens.non_fold_residue + floor witness src/v2/lens/non_fold_residue_test.dag.
  • 71 seeded residue sites (eq-functions, lattice joins, node-eval handlers) on a named, shrinking roster + stale ratchet.

Verification bar (DESIGN §5: green-by-execution, discriminating)

Each census has synthetic RED/GREEN host controls proving discrimination by execution: inert→RED / consumed→GREEN; residue→RED / total-fold→GREEN; plus open-domain and same-file-consumer negative controls. Both floor witnesses run green through claim_batch (the real floor consumer), and floor discovery passes the inert-lens + construction-justification hygiene gates. No raw counts — the walls are named rosters; a new inert carrier / new residue reds CI, a fixed one reds the stale-roster ratchet until removed.

CONSTRUCTION-FIRST: neither class is unwritable-by-construction today (modeling-ahead-of-consumer is deliberate; exhaustiveness-by-default is a load-bearing typechecker change) — so each is the genuinely-unstructurable residue a lens is for. Both are additive corpus-gate builtins (sibling to doc_graph_* / fact_cardinality_*); they do NOT touch cli_run.rs's #5433 closure. DISSOLUTION at gunbc#5364 (.dag compile-graph access) → pure .dag Node-tree readers.

Piggybacked fix (not Lane 7, but required to keep this branch green)

src/v1/tests/src/helpers.rs + src/v1/tests/src/parse.rs — the two parse perf-fixture tests (tokenizer_non_ascii_performance_regression, source_text_at_lookup_flat_in_file_size) assert !source.is_ascii() on src/v1/02_parse.dag, but #5567's tree-wide comment-strip removed all non-ASCII (it lived in comments), so they fail on main for every PR that merges it. Fixed with a read_v2_file_with_distributed_non_ascii helper that injects an EM DASH at a prime stride (preserving char count and the byte≠char-offset condition the perf tests check). Cleanly scoped, ASCII-only logic; called out here so it isn't invisible in review.

🤖 Generated with Claude Code

@gunbai-bot gunbai-bot Bot changed the title Walls Lane 7 inert-abstraction lens keystone plus non-fold-residue audit over closed coproducts, per docs/plans/upcoming-work-dispatch-plan.md Lane 7 Lane 7: inert-abstraction lens keystone + non-fold-residue audit (fail-closed walls) Jun 22, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review June 22, 2026 22:44
briansrls added a commit that referenced this pull request Jun 22, 2026
…add ByteSize algebra to std.measure

Finding 1 (predicate dissolution / §4 ops-from-inhabitance): deleted priority_eq
(Bool helper minted per-coproduct with a `_ => false` wildcard) — claims_of_priority
now routes through canonical `==` (Value::eq, the single CanonKey authority; same
form as extdeps oci linux.dag namespace equality). Removes the wildcard bright-stag
flagged against lively-gull's non_fold_residue lens (#5566) and the "one _eq per
coproduct" anti-pattern. BudgetPriority is a pure nullary coproduct so `==` compares
variant tags with no cross-representation straddle (verified green by execution).

Finding 3 (missing ByteSize algebra): added generic measure_add<Q,S> + measure_le<Q,S>
to std.measure (the canonical home all reviewers named). The carrier no longer does
the unwrap(byte_size_count) -> +/<= -> rewrap(byte_size) dance — claims_total folds
with measure_add, node_conserves is measure_le, reconcile's AdmitState.used is ByteSize.
Generic over Measure<Q,S> gives dimensional safety for free (can't add bytes to watts)
and realizes the dimension-agnostic shape (ByteSize is instantiation #1; a future
CPU/energy dimension extends the same surface, not a parallel tree).

Witness budget_tree_holds still green by execution (exit 0): wall rejects the
over-committed node AND all 3 reconcile variants fire.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jun 23, 2026
…Appropriation/LineItem/zero-based; recursive conservation + admission construction) (#5582)

* budget-tree carrier: hierarchical memory budget, two-verdict (static conservation WALL + runtime reconcile HANDLER)

Foundational §1 carrier for ROADMAP 1-budget-tree (operator: "model the whole
machine as a memory budget tree; each level inherits a budget from its parent as
a transaction"). Zero consumers yet — routed for review before any consumer edit.

product.budget_tree models a node's allocated budget (capacity_intent) and its
children's claims, with TWO DISTINCT regimes (never conflated — else a runtime
ratchet masquerades as a compile wall):

  REGIME 1  node_conserves : Bool  — STATIC conservation over AUTHORED budgets.
    Sum(children claims) <= parent budget. Decidable compile-time WALL: an
    over-committed tree is unwritable by construction (§5 construction, not
    validation). This is the stern-otter co-residence OOM made unwritable.

  REGIME 2  reconcile : Reconciliation  — RUNTIME intent x MEASURED-actual.
    A fail-closed HANDLER (Realization), NOT a wall. Admit in QoS order
    (Guaranteed > Burstable > BestEffort); classify:
      AllSatisfied        actual covers all claims
      Evicted             best-effort/burstable shed to fit actual
      GuaranteedShortfall typed LOUD error — guaranteed set exceeds actual
                          (genuinely under-provisioned; never a silent OOM,
                          which matters most on the UNCAPPED fleet where the
                          physical OOM-killer would otherwise pick random victims)

Levels (L0 host / L1 concurrent runs / L2 within-run rustc+spawn-width) are
BudgetNode INSTANCES; spawn-width #5444, placement R #5559, compile-jobs N #5546
become consumer leaves that IMPORT their parent allocation (divide-once), not
parallel facts that re-divide host_ram.

Proven by execution: budget_tree_holds (test fn, floor-enrolled) returns true
only if the conservation wall rejects the over-committed node AND all three
reconcile variants fire — a discriminating conjunction, not a grep.

Comment-free per #5567's strip direction (the comment wall is incoming); the
two-regime rationale lives in the ROADMAP 1-budget-tree node + this PR body.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* review fixes (opus-4-7 #5582): dissolve priority_eq to canonical ==, add ByteSize algebra to std.measure

Finding 1 (predicate dissolution / §4 ops-from-inhabitance): deleted priority_eq
(Bool helper minted per-coproduct with a `_ => false` wildcard) — claims_of_priority
now routes through canonical `==` (Value::eq, the single CanonKey authority; same
form as extdeps oci linux.dag namespace equality). Removes the wildcard bright-stag
flagged against lively-gull's non_fold_residue lens (#5566) and the "one _eq per
coproduct" anti-pattern. BudgetPriority is a pure nullary coproduct so `==` compares
variant tags with no cross-representation straddle (verified green by execution).

Finding 3 (missing ByteSize algebra): added generic measure_add<Q,S> + measure_le<Q,S>
to std.measure (the canonical home all reviewers named). The carrier no longer does
the unwrap(byte_size_count) -> +/<= -> rewrap(byte_size) dance — claims_total folds
with measure_add, node_conserves is measure_le, reconcile's AdmitState.used is ByteSize.
Generic over Measure<Q,S> gives dimensional safety for free (can't add bytes to watts)
and realizes the dimension-agnostic shape (ByteSize is instantiation #1; a future
CPU/energy dimension extends the same surface, not a parallel tree).

Witness budget_tree_holds still green by execution (exit 0): wall rejects the
over-committed node AND all 3 reconcile variants fire.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

* ground budget tree in real accounting (extdeps); add tree recursion + admission-as-construction (opus-4-7 round 2)

Operator: ground budget_tree in the real budgeting/accounting framework (start from
en.wikipedia.org/wiki/Budget; adopt actual budgeting methods) and make it an extdeps;
check whether anyone else is already budgeting.

NEW extdeps/accounting/budget.dag — the single §3 authority for the budgeting framework,
anchored to en.wikipedia.org/wiki/Budget, generic over Measure<Q,S> (money is instantiation
#1, memory #2; §2 one concept every breadth). Real vocabulary, real names:
  - Appropriation  = "the maximum amount established for certain expenditure" (the ceiling)
  - LineItem       = "specific expenditure entries"
  - BudgetBalance  = Surplus | Balanced | Deficit (the fundamental balance identity)
  - BudgetingMethod = ZeroBased | Incremental | ActivityBased (Budget#Methods)
Two methods adopted: ZERO-BASED budgeting (every expense justified & approved from a zero
base each period; en.wikipedia.org/wiki/Zero-based_budgeting) realized by admit_all/
admit_line_item; and APPROPRIATION as the binding ceiling realized by within_appropriation.

budget_tree.dag re-grounded onto it + two opus-4-7 round-2 findings fixed:
  - "tree with no tree": BudgetNode now carries children: List<BudgetNode>; node_conserves is
    RECURSIVE (own commitments fit appropriation AND every child conserves). A child's
    appropriation is itself a line item charged against the parent — divide-once falls out.
  - "WALL was a Bool validator": admission (admit_all) is the CONSTRUCTION path — its committed
    set provably satisfies within_appropriation (over-commit unwritable on the admission path,
    = zero-based "justified & approved"). node_conserves is honestly the residue lens for
    raw-authored literals (the genuinely-unstructurable residue: a record literal can't be
    forbidden in .dag), NOT relabeled a wall.

Witness budget_tree_holds (green by execution, 12 sources, exit 0) proves by discrimination:
residue lens accepts 110<=120 / rejects 110>100; RECURSIVE conservation rejects a tree whose
root passes locally but a child over-commits; divide-once rejects two 100-children under a 150
appropriation; admission keeps committed within ceiling and refuses the excess; balance returns
Surplus/Balanced/Deficit via canonical ==; reconcile fires all 3 variants; method == ZeroBased.

Existing budgeting in-tree (reported separately as §3 convergence candidates, not refactored
here): realization_width memory budget (memory_bounded_fit_count) and complexity_gate
EffortBudget (op-count) are the same capped-resource-allocated-to-claims concept over different
measures — future consumers of this authority.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansrls@gunb.ai>
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
briansrls and others added 2 commits June 23, 2026 01:07
 merge + §6 kernel-vs-un-migrated dissolve-on wording

- strip_line_comment in both census modules now blanks string-literal interiors
  (so // in URLs and _ =>/braces/| inside string literals are not read as code);
  + 2 discriminating controls (in-string decoy green; real wildcard + decoy red).
- re-derive rosters against main merge ae891fc (#5568 unified the 3 drift gates):
  drop deleted ci_yaml/gitignore/roadmap_gate exit_ok; add generated_artifact.dag
  artifact_eq/artifact_extra_valid + generated_artifact_gate exit_ok; drop RbacPolicy
  (now consumed by extdeps/bmc/access.dag).
- concrete declaring-file homes for AccessPolicy/FilePermissions/GitCliReportedVersion.
- correct dissolve-on wording: §6 named irreducible kernels (eq/lattice/collapse)
  wall permanently; only un-migrated modeling shrinks. per-entry tag deferred to gunbc#5364.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Addressed all review feedback in c1812402d8 (+ roster re-derivation in 5900690dac):

1. Vague roster home (FilePermissions recorded as dsl/std/*) — fixed to concrete declaring files so the stale-ratchet reviewer can grep them: FilePermissions → dsl/extdeps/access/posix.dag, and while there I corrected two more that were vague/wrong: AccessPolicy → dsl/std/access.dag (was rbac.dag), GitCliReportedVersion → dsl/extdeps/git/versioning.dag.

2. No string-literal awareness (// in a URL, match /_ => inside a string literal) — fixed at the single lexical authority: strip_line_comment in both census modules now blanks string-literal interiors (each interior byte → a space, delimiters kept, byte-length preserved for stable brace matching) and only treats // as a comment outside strings. One pass removes all three false-signal classes (//, _ =>, {/}/| inside strings). Added two discriminating controls that run the production predicate: green_control_wildcard_and_slashes_inside_string_literal_are_ignored (in-string _ =>/https:// → not flagged) and red_control_real_wildcard_survives_an_in_string_decoy (same decoy + a real wildcard → still flagged, so blanking can't suppress genuine residue).

3. dissolve-on wording more aggressive than §6 demands; kernel-vs-residue tag — valid. Corrected the roster header: §6's two categories now dissolve differently — un-migrated modeling (emit_yaml_value, the eval_*_node* handlers, dag_grammar_terminal_*) shrinks as each migrates to a fold; named irreducible kernels (the *_eq _ => false off-diagonals, lattice *_join/*_meet/*_combine, *_dominates, the exit_ok/program_runtime_bool_*/is_* collapses) wall permanently and are expected to remain. The roster no longer claims it shrinks uniformly to zero. The per-entry structural tag is deferred to the gunbc#5364 dissolution (the pure .dag Node-tree reader carries each site's match shape + scrutinee type, so the classification is derived there) — hand-maintaining a 71-way tag now risks the §5-bad direction (mistagging migratable debt as a permanent kernel hides debt).

4. Each gate fn re-walks the corpus (8× per witness pass) — acknowledged; consistent with the doc_reachability_project/fact_cardinality_census sibling pattern and dissolves with the same gunbc#5364 reader. Left as-is (out of scope to block on).

Separately, the main merge ae891fcf8f pulled in #5568 (which unified the three per-artifact drift gates into one universal generated-artifact policy), so I re-derived both rosters against current main: dropped the now-deleted ci_yaml_gate/gitignore_gate/roadmap_gate exit_ok entries, added generated_artifact.dag::artifact_eq/::artifact_extra_valid + generated_artifact_gate.dag::exit_ok, and dropped RbacPolicy (now consumed by extdeps/bmc/access.dag). All 4 floor witnesses pass green-by-execution via claim_batch; both modules' suites pass (11/11 each); fmt + clippy clean. Also fixed the two parse perf-fixture tests that #5567's comment-strip broke (the non-ASCII they relied on lived in comments) by injecting distributed non-ASCII into the fixture.

— sent from lively-gull-506

…olicy dissolved)

RbacPolicy dropped off the inert roster when extdeps/bmc/access.dag gained a real
consumer (redfish_rbac_policy) via the main merge — the stale-roster ratchet working
as intended. Plan doc now reflects the 8-carrier roster.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Both addressed:

  1. inert-layer-lens.md count drift → fixed in 1a1ada4899: 9 seeded → 8 carriers, with a note that RbacPolicy dissolved off the roster when extdeps/bmc/access.dag's redfish_rbac_policy consumer landed (the stale-roster ratchet doing its job).
  2. Piggybacked fixture fix not called out → added a "Piggybacked fix" section to the PR body explaining the helpers.rs/parse.rs change repairs the two parse perf tests Strip .dag comments (flush — no grammar change, no ctrl dependency) #5567's comment-strip broke on main (the non-ASCII they assert lived in comments).

— sent from lively-gull-506

briansrls and others added 2 commits June 23, 2026 01:37
…_on with §6 kernel wording

- both census modules now route the *_count builtins through a OnceLock-memoized
  build_report(): the four builtins + live-tree tests share ONE dsl/+src/v2 walk per
  process instead of re-walking per call (the thrice-flagged 8x-walk nit). Pure
  compute_report/residue_sites still take &[files] so synthetic RED/GREEN controls
  drive them with in-memory corpora, bypassing the cache.
- non_fold_residue.dag dissolve_on: 'reaches 0' -> the un-migrated subset shrinks to 0
  while named irreducible kernels (eq/lattice/collapse) remain by §6, matching the Rust
  comment (no longer overstated).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Both addressed in bd8d9192d4:

  1. Per-call corpus re-walk (the OnceLock suggestion) — done. Both census modules now route their four *_count builtins through a OnceLock-memoized build_report(), so a witness eval (which calls the builtins one-by-one) plus the live-tree tests share one dsl/+src/v2/ walk + report per process instead of N. The pure compute_report/residue_sites/closed_coproduct_names still take &[files] so the synthetic RED/GREEN controls keep driving them with in-memory corpora (which never touch the cache). All 4 floor witnesses re-confirmed green-by-execution via claim_batch; both suites 11/11.

  2. .dag dissolve_on says "reaches 0" but ~half the roster is permanent kernels — valid inconsistency vs the Rust comment; fixed. non_fold_residue.dag now reads: the un-migrated-modeling subset shrinks to 0 as each match migrates to a fold, while the named irreducible kernels (eq / lattice join+meet / collapse algebraic totals) remain by §6. The Rust comment and the .dag rationale now say the same thing.

— sent from lively-gull-506

@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

Valid §2/§3 finding — fixed before merge (extracted, not deferred). Commit 3f3b9114ab:

The byte-identical workspace_root/repo_rel/is_test_dag/collect_dag_files/corpus_dag_files/strip_line_comment/brace_delta are lifted into one new crate::corpus_lex module that both census modules import. The string-literal-aware strip (and any future raw-string handling) now lives in exactly one place. The census-specific logic (compute_report/type_carrier_blocks for inert; residue_sites/closed_coproduct_names/parse_fns for non-fold) stays local. corpus_lex carries its own unit tests (string-interior blanking, brace-delta-ignores-strings, test-dag suffix) and is added to the self-emit hand_maintained_mods list in both v1_compiler_emit_rust.rs and src/v1/05_emit_rust.dag.

Verified: corpus_lex 3/3, inert 11/11, non-fold 11/11; both gate witnesses still green-by-execution via claim_batch; fmt + clippy clean.

(The sibling doc_reachability_project/fact_cardinality_census modules carry their own older copies of the walk — pre-existing, untouched here; corpus_lex is the convergence point they can migrate onto, and all of it dissolves into the pure .dag Node-tree reader at gunbc#5364.)

— sent from lively-gull-506

@gunbai-bot

gunbai-bot Bot commented Jun 23, 2026

Copy link
Copy Markdown
Contributor Author

The REQUEST_CHANGES (review 31934) reviewed abe0339368 — an intermediate commit the background auto-committer snapshotted mid-extraction, where corpus_lex.rs existed but the wiring + duplicate-removal hadn't landed yet. Every point it raises is resolved on current HEAD 3f3b9114ab:

  • (a) lib.rs adds pub mod corpus_lex; — present on HEAD.
  • (b) duplicated helpers removed from both modules — inert_carrier_project.rs and non_fold_residue_project.rs now have zero local defs of workspace_root/repo_rel/is_test_dag/collect_dag_files/corpus_dag_files/strip_line_comment/brace_delta (verified grep -c = 0); both carry use crate::corpus_lex::{brace_delta, corpus_dag_files, is_test_dag, strip_line_comment};.
  • (c) corpus_lex added to hand_maintained_mods — present in both v1_compiler_emit_rust.rs and src/v1/05_emit_rust.dag (so re-emit keeps it).

So the "new single-authority module is unwired/unused" state was real for exactly that one transient commit and is fixed on HEAD — corpus_lex is the sole definition and both censuses import it. corpus_lex 3/3 + inert 11/11 + non-fold 11/11 pass, both gate witnesses green via claim_batch, fmt + clippy clean on HEAD. A fresh review on 3f3b9114ab should clear this.

— sent from lively-gull-506

…an (#5544/#5579) + fix #5584 orphan doc

- parse.rs/helpers.rs: converge on main's dedicated non_ascii_perf.dag fixture (#5579);
  drop my read_v2_file_with_distributed_non_ascii (don't fork the fix).
- emit lists (emit_rust.rs + 05_emit_rust.dag): keep corpus_lex + main's mod additions.
- strip // comments from the 4 Lane 7 lens .dag files (inert_carrier{,_test}, non_fold_residue{,_test})
  — the parser-wall now rejects DAG comments; construction_justification rationale lives in data fields, preserved.
- DESIGN.md: link docs/plans/intent-linearity-design-draft.md (orphaned by #5584, fail-closed orphan-doc gate
  reds every PR merging main) from the open-thread bullet it was authored to serve.

Verified: 4 floor witnesses green via claim_batch; 6 census live gates + orphan-doc gate pass; fmt clean.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
@briansrls
briansrls merged commit 6ff13ec into main Jun 23, 2026
2 checks passed
@briansrls
briansrls deleted the session/lively-gull-506 branch June 23, 2026 03:15
gunbai-bot Bot pushed a commit that referenced this pull request Jun 23, 2026
…n dissolution trigger (§6)

Clears bright-stag's §6 inert-abstraction finding (the class lively-gull's Lane 7
lens #5566 is built to flag): unit_must_run is defined + self-tested but not yet
consumed by the live gate (should_run_gates fires coarsely via any_declared_closure_hit).
Per parent: option (b) — keep it as an intentionally-STAGED primitive with a named
consumer/dissolution trigger = the future per-unit rust-test selection slice (the
affordability direction) that replaces all-or-nothing should_run_gates. Marker encoded
as a typed data-string (§6 mark-on-carrier; #5579 removed comment trivia).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls pushed a commit that referenced this pull request Jun 23, 2026
…not a hand-rolled SymbolicCost wildcard

Replaces cost_is_nested_product (a nested match over the closed SymbolicCost
coproduct with _ => false arms -- non-fold residue per #5566) with class-equality
against cost.dag's exhaustive asymptotic_class_of_cost. The module now carries zero
wildcard-over-coproduct matches (single authority, total), and minimized_class
inherently checks the realized class equals the rewrite's before-class -- addressing
both non-blocking reviewer notes on the earlier APPROVE. Semantics unchanged: an
O(n^2) cost (ClassPolynomial degree 2) is rewritable to ClassLinear; linear / sum
costs are not.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Jun 23, 2026
…YamlValue (#5566 floor unblock)

The non_fold_residue gate (#5566) was RED on main: block_sequence_element_doc
and project_yaml_to_doc each carried a `_ =>` wildcard over the closed YamlValue
coproduct (a fail-open escape a fold would not have), landed unrostered; and the
roster carried a stale `emit_yaml_value` entry for a fn that no longer exists.

Per operator directive ("I would just dissolve"): migrate both matches to total
form rather than roster them. Each wildcard is replaced with explicit arms for the
variants it caught (YamlNull/Bool/Int/Float[/Sequence]), each delegating to the
exact same emit_scalar expression — behavior-preserving by construction. The stale
roster entry is removed so the roster shrinks (live_tree_residue_roster_has_no_stale_entries).

Verified by execution: all 11 non_fold_residue gate tests green (was 2 RED);
all 38 yaml serializer/quoting/multiline witnesses green (behavior unchanged).
No comments added to .dag (post-#5567 comment-wall).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jun 23, 2026
 floor unblock (#5612)

* WIP: roadmap discussion

* Dissolve yaml.dag non-fold residue: 2 wildcards → total matches over YamlValue (#5566 floor unblock)

The non_fold_residue gate (#5566) was RED on main: block_sequence_element_doc
and project_yaml_to_doc each carried a `_ =>` wildcard over the closed YamlValue
coproduct (a fail-open escape a fold would not have), landed unrostered; and the
roster carried a stale `emit_yaml_value` entry for a fn that no longer exists.

Per operator directive ("I would just dissolve"): migrate both matches to total
form rather than roster them. Each wildcard is replaced with explicit arms for the
variants it caught (YamlNull/Bool/Int/Float[/Sequence]), each delegating to the
exact same emit_scalar expression — behavior-preserving by construction. The stale
roster entry is removed so the roster shrinks (live_tree_residue_roster_has_no_stale_entries).

Verified by execution: all 11 non_fold_residue gate tests green (was 2 RED);
all 38 yaml serializer/quoting/multiline witnesses green (behavior unchanged).
No comments added to .dag (post-#5567 comment-wall).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jun 23, 2026
…nformance_test's consumed-.dag closure on the existing NodeArtifactProvenance carrier + fire should_run_gates on a closure-path change (fail-closed: undeclared test = must-run), proven green-by-execution with a discriminating contr (#5605)

* WIP: Edge-(b) coverage keystone — slice 1: declare coproduct_reflection_confo

* Edge-(b) slice-1: dsl ConsumedInputClosure carrier + should_run_gates coverage fire

Comments → typed `data` marks (DAG comment trivia removed in #5579, so `//`
fails to parse — fixes the rust_stage0_gates.dag:18 parse error that fail-closed
both the floor and the rust gate on the WIP commit).

Slice 1 of the Edge-(b) coverage keystone (docs/plans/edge-b-rust-dag-provenance-brief.md):
- New dsl-layer authority ConsumedInputClosure (unit-identity → consumed-.dag paths)
  in dsl/tools/rust_stage0_gates.dag. Homed in dsl (not v2 NodeArtifactProvenance)
  because the consumer should_run_gates runs in the v1/dsl tree, which cannot import
  v2 (imports point toward std). General "consumed-input/affected-set selection" name
  per bright-stag (rust test = one kind of unit) with a convergence-candidate marker
  toward v2 affected_set + the .dag-floor selection. First authority for a distinct
  CONSUMES-input fact, not a parallel mint of NodeArtifactProvenance (PRODUCES-artifact).
- should_run_gates additively fires when a changed .dag is in the union of declared
  closures; unit_must_run is fail-closed (no declared closure → must-run).
- coproduct_reflection_conformance_test's 8-file closure hand-listed; labelled
  NON-SOUND/WIRING-ONLY, dissolution = structural closure derivation (shared blocker).
- Discriminating control proven by execution: in-closure .dag FIRES (true),
  out-of-closure does NOT (false), undeclared unit must-run (true).

Also restores docs/plans/self-applying-lenses.md (unrelated edit swept in by auto-WIP).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* Edge-(b) slice-1: mark unit_must_run as STAGED with per-unit-selection dissolution trigger (§6)

Clears bright-stag's §6 inert-abstraction finding (the class lively-gull's Lane 7
lens #5566 is built to flag): unit_must_run is defined + self-tested but not yet
consumed by the live gate (should_run_gates fires coarsely via any_declared_closure_hit).
Per parent: option (b) — keep it as an intentionally-STAGED primitive with a named
consumer/dissolution trigger = the future per-unit rust-test selection slice (the
affordability direction) that replaces all-or-nothing should_run_gates. Marker encoded
as a typed data-string (§6 mark-on-carrier; #5579 removed comment trivia).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jun 23, 2026
…ows (one engine, N rows, two axes). cost.dag computes runtime cost as a fold_node over the AST (SumCost for a sequence, ProductCost for a nested loop -> AsymptoticClass). Formalize its DECIDABLE rewrite catalog -- the §5 'O(n^2)->O (#5600)

* WIP: Bring complexity into the intent_linearity registry as RunTime-axis rows

* WIP: Bring complexity into the intent_linearity registry as RunTime-axis rows

* WIP: Bring complexity into the intent_linearity registry as RunTime-axis rows

* Drop ROADMAP doc-link from #5600 — unblock fix moves to a standalone PR

The doc-reachability floor fix (linking the orphaned intent-linearity design
draft) requires editing the generated-artifact authority dsl/gunbc/roadmap_authority.dag
+ regen, which collides with #5596 and is owned by witty-crane-380 (the orphan
came in with #5584). Handing the queue-wide unblock to a standalone PR; #5600
stays the pure complexity RunTime-axis feature and rebases once main is green.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* complexity_rewrite: match rewrite preconditions on asymptotic class, not a hand-rolled SymbolicCost wildcard

Replaces cost_is_nested_product (a nested match over the closed SymbolicCost
coproduct with _ => false arms -- non-fold residue per #5566) with class-equality
against cost.dag's exhaustive asymptotic_class_of_cost. The module now carries zero
wildcard-over-coproduct matches (single authority, total), and minimized_class
inherently checks the realized class equals the rewrite's before-class -- addressing
both non-blocking reviewer notes on the earlier APPROVE. Semantics unchanged: an
O(n^2) cost (ClassPolynomial degree 2) is rewritable to ClassLinear; linear / sum
costs are not.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* catalog_sound_test: drop the removed 'applies' field from bogus rewrite controls

Follow-on to the class-based refactor: ComplexityRewrite no longer carries an
'applies' fn field, so the identity/widening RED-control constructors must not set it.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* intent_linearity: RunTime axis is a candidate detector, not the redundancy wall (§5 fail-closed)

Addresses the REQUEST_CHANGES finding: wiring the RunTime row into chain_is_redundant
made the wall flag a genuine all-pairs O(n^2) loop as 'redundant intent' -- a §5
fail-OPEN (a false positive on the wall) since the row's sufficiency is ungrounded.

Fix: the two axes now compose differently. chain_is_redundant folds ONLY the ChangeTime
rows (anti-unification proves redundancy -> sound wall, no false positive), so
level_is_linear / body_is_linear never call a genuine program redundant. The RunTime axis
is read via a new chain_has_runtime_rewrite_candidate -- honestly a CANDIDATE (O(n^2) is the
decidable necessary condition; sufficiency waits on the independence carrier), so it does
not feed the wall. Both rows stay in linearity_registry() (one engine, N rows, two axes);
cost_axis_equal partitions them by axis with an exhaustive match (no wildcard residue).

Witnesses: nested_loop_not_changetime_redundant (the wall does NOT flag a genuine nested
loop) + nested_loop_is_runtime_candidate (the RunTime axis still fires) green by execution.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant