Skip to content

Lever 1: floor compile-clean receipt through the shared index — one typecheck universe per run - #6783

Merged
briansrls merged 4 commits into
mainfrom
lever1-gate-via-index
Jul 17, 2026
Merged

briansrls merged 4 commits into
mainfrom
lever1-gate-via-index

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Jul 16, 2026

Copy link
Copy Markdown
Contributor

What

Operator-signed lever 1 from the typecheck investigation (#6766, closed investigation record): the floor's whole-tree compile-clean receipt compile now rides the shared MultiEntryIndex cached path instead of the raw pipeline, and the executor's threading is lined up so the gate, the plan prelude, and batch-2's witness corpus share one content-keyed typecheck universe per run.

Why it matters (measured, srv3-class silicon): CI's ~55-min batch-1 = a ~7.5-min compile × ~2× srv3 per-core deficit × ~2× in-process double-pay. This PR deletes the double-pay factor and warms batch-2:

  • gate compile: verdict-equivalent, no wall regression (377.7s via-index vs 381.4s raw, whole tree)
  • planted-inject red: 4.3s (vs 361.6s raw — the failing stage refuses without typechecking the world)
  • heavy witness entries after the gate: 1.0–1.4s (vs 10–90s cold) — batch-2's ~44 min of per-entry resolve collapses

How

  • resolved_graph_from_sources_with_index — the sources-taking core extracted from resolve_entry_with_parse_cache (all memo tiers), with collect-then-refuse parse errors (all files, one run).
  • floor_compile_clean_emit_ok_via_index — the receipt's compile: via-index resolve + --target dag emit over the already-typed graph. The raw floor_compile_clean_emit_ok remains the cache-independent oracle (cargo tests / enrolled witnesses) and the equivalence second opinion.
  • Roots armed at enable_floor_compile_clean_lazy_install(&source_roots); a receipt demanded without them refuses (typed), never falls back to a second raw compile (§5).
  • claim_executor: eager receipt install on the main thread (plan already resolved — same ordering the lazy path guaranteed; lazy consume stays as fail-closed fallback) and Discovery pumps on the main-thread lane — process_shared_index is thread-local (Rc, !Send), so this is what makes the gate-filled store the one the corpus reads. No wall loss: the main thread previously idled at the join while the lone Discovery unit ran spawned.

Receipts

  • Whole-tree green/red agreement matrix + warm-entry walls: investigate typecheck #6766 (investigation record, prototype receipts).
  • Enrolled: compile_clean_via_index_verdict_equivalence — green corpus agrees green; planted unresolved import agrees red; planted variant-mismatch typecheck red agrees red (3/3 green in release cargo test). The raw path shares no caches with via-index, so agreement is an independent second opinion.
  • The ignored e2e broken-tree test now arms index roots, so it can no longer pass through a Refused receipt without compiling (masked-tooth fix).
  • Predicate audit: typecheck refusals and the gate's hardness filter reduce to the same 00_core interpreter-blocking authority on every producible class (ComplexityUnknown, the sole divergence, is unproducible on both paths — complexity analysis off).
  • This PR's own CI floor run is the whole-tree by-execution receipt for the new wiring.

Notes

  • Memory: the shared index now retains the whole-tree typed store for the executor's lifetime (~1.2–1.8 GB measured) — the same union batch-2 already grows toward, reached earlier. The A-lane eviction (PR-β, cross-entry-typed-module-memo sketch §2) bounds it on constrained hosts; at width>1 the cross-worker serde store remains the (separate) sharing carrier — follow-up with the A-lane so the gate's store and the claim-workers' store stay one carrier (§3).
  • Known pre-existing local reds (NOT this PR): emit_success_implies_resolve_success_on_live_witness_roots and primary_precedence_pool_fills_only_absent_modules fail identically on unmodified main in plain local cargo test ("source root does not exist: dag", cwd-dependent).
  • Discharges the compile half of the CLAUDE.md open thread "floor shared-computation memoization — make the double-paid full-tree compile UNREPEATABLE by construction": the receipt is the one compile, and its results are the store every later resolve reads.

🤖 Generated with Claude Code

briansrls and others added 4 commits July 16, 2026 23:22
…ex — one typecheck universe per run (kills the in-process double-pay, warms batch-2)

The floor's whole-tree compile-clean receipt previously ran the raw
compile_to_resolved/compile_sources pipeline — no cache tier at any grain — while
the same claim_executor process re-typechecked the affected closure AGAIN through
the MultiEntryIndex for batch-2's witness corpus (the CLAUDE.md "double-paid
full-tree compile" open thread, located and measured in the typecheck
investigation, PR #6766).

This change makes the receipt compile ride the same cached path entry resolves
use, and lines the threads up so the sharing is real:

- resolved_graph_from_sources_with_index: the sources-taking core extracted from
  resolve_entry_with_parse_cache (parse/normalize/typed/ownership memo tiers +
  subject memo), with parse errors collected across ALL files before refusing
  (collect-then-refuse; previously first-error-per-run).
- floor_compile_clean_emit_ok_via_index: the receipt's compile — via-index resolve
  + --target dag emit over the already-typed graph. The raw
  floor_compile_clean_emit_ok stays as the cache-independent oracle behind
  witness_layer_roots_compile_clean_emit_check (cargo tests / enrolled witnesses)
  and the equivalence second opinion.
- enable_floor_compile_clean_lazy_install now arms the executor's --source-root
  vector (same process_shared_index roots key as the plan prelude and batch-2);
  a receipt demanded without armed roots REFUSES (typed reason), never falls back
  to a second raw whole-tree compile.
- claim_executor: eager receipt install on the MAIN thread (plan already resolved
  at that point — same ordering the lazy path guaranteed), and Discovery pump
  units run on the main-thread lane, so the thread-local shared index the gate
  fills is the one the corpus reads. Lazy consume stays as the fail-closed
  fallback. No wall loss: the main thread previously idled at the join while the
  single Discovery unit ran spawned.

Receipts (PR #6766 comments; 128-core Neoverse-N1):
- whole tree green: via-index 377.7s vs raw 381.4s — verdicts agree
- planted GUNBC_TEST_FLOOR_COMPILE_CLEAN_INJECT_UNRESOLVED red: via-index 4.3s
  vs raw 361.6s — verdicts agree (fast red at the failing stage)
- heavy witness entries warm through the gate-filled store: 1.0-1.4s vs
  10-90s cold

Enrolled controls: compile_clean_via_index_verdict_equivalence (green corpus
agrees green; planted unresolved import agrees red; planted variant-mismatch
typecheck red agrees red — raw path shares no caches with via-index, so the
agreement is an independent second opinion). The ignored e2e broken-tree test now
arms index roots so it cannot pass through a Refused receipt without compiling.

Predicate note: typecheck refusals use the same 00_core interpreter-blocking
authority the gate filters with; the only class where the stage predicates differ
(ComplexityUnknown) is unproducible on both paths (complexity analysis off).

Pre-existing, unrelated: emit_success_implies_resolve_success_on_live_witness_roots
and primary_precedence_pool_fills_only_absent_modules fail in plain local cargo
test on unmodified main too ("source root does not exist: dag" — cwd-dependent);
verified identical on the control tree.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…R diff — transient, fail-closed unavailable; no code change)

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…(both prior heads hit the platform-wide 503; no code change)

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…and plan-relative spellings of one pool address ONE index

Review 39118 (cursor, REQUEST_CHANGES) caught the CI-path defect in the lever-1
wiring: the receipt armed process_shared_index with the executor's absolute CLI
roots ($ROOT/dag) while batch-2 discovery keys on the plan's relative
witness_layer_roots (dag, src/v2). process_shared_index holds ONE (key, index)
slot per thread and replaces on mismatch, so in CI the gate-warmed typed universe
was silently swapped for a cold one before the corpus read it — voiding the
sharing this PR exists to deliver.

Fix at the shared seam: canonical_shared_index_roots normalizes each root to its
repo-relative form (workspace-anchored absolute → relative; order preserved for
primary-precedence pool semantics; a root outside the workspace keeps its
spelling — genuinely a different pool) and process_shared_index uses the
canonical form for BOTH the key and the build, so no caller spelling can fork
the universe.

Discriminating control (enrolled):
shared_index_roots_key_canonicalizes_absolute_and_relative_spellings — absolute
and relative spellings must return the SAME Rc (pointer equality), run under a
workspace cwd (the executor's runtime context). 4/4 green with the existing
equivalence matrix.

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

gunbai-bot Bot commented Jul 17, 2026

Copy link
Copy Markdown
Contributor Author

review 39118 (cursor, REQUEST_CHANGES) — finding valid, fixed in 34dcdb85ee. The roots-key split was real: the receipt armed the index with the executor's absolute CLI roots while batch-2 discovery keys on the plan's relative witness_layer_roots, and process_shared_index replaces its single per-thread slot on key mismatch — so on the CI path the gate-warmed universe was swapped for a cold one before the corpus read it, voiding the sharing claim. Fixed at the shared seam per the review's recommendation: canonical_shared_index_roots normalizes every root to its repo-relative form (order preserved for primary-precedence semantics; non-workspace roots keep their spelling) and process_shared_index uses the canonical form for both the key and the build, so no caller spelling can fork the universe. Enrolled discriminating control: shared_index_roots_key_canonicalizes_absolute_and_relative_spellings (absolute vs relative spellings must return the same Rc, pointer-equality, under the executor's workspace cwd) — 4/4 green with the equivalence matrix. — sent from clever-seal-476

@gunbai-bot

gunbai-bot Bot commented Jul 17, 2026

Copy link
Copy Markdown
Contributor Author

CI receipt on head 34dcdb8 (run 29543941811, green): the shared-index reroute did what it was built to do — witness corpus collapsed from ~45–63 min (baseline runs on this runner class) to 5.7 min (batches 2–4: 01:29:42→01:35:25, discovery rows warm off the gate-warmed typed store; e.g. per-witness reconciles 1.3s/6.4s/22.9s vs 10–90s cold).

Full floor decomposition of the 104-min wall for the record:

  • plan-artifact prelude ~8 min (separate claim_executor process, own cold index)
  • whole-tree compile via shared index 47 min (the single cold pass — the per-module typecheck kernel × this runner's per-core speed; owned in the resolve-superlinearity lane, not this PR)
  • batch-1 gate claim node 11.6 min — residue: claim units run on spawned worker threads whose thread-local process_shared_index starts empty, so the gate node rebuilds its entry closure cold. Discovery units already ride the main thread. Follow-up (new PR): at governor target_width=1 run claim units on the main thread too — removes this term without touching Rc→Arc.
  • floor_skip selection control 9.7 min, regen 20.7 min (regen fires because this PR touches src/v1/**; absent on .dag-only PRs)

Net for a .dag-only PR: ~118 min baseline → ~73 min now → ~61 min with the width-1 follow-up. The remaining 47-min term decomposes per the #6766 attribution (per-module typecheck kernel; sharding + within-module work are the levers there).

@briansrls
briansrls merged commit d077057 into main Jul 17, 2026
3 checks passed
@briansrls
briansrls deleted the lever1-gate-via-index branch July 17, 2026 02:15
briansrls added a commit that referenced this pull request Jul 17, 2026
Keep branch compile_to_resolved_with_corpus_global_bare (import-strip
census path) and main's floor via-index receipt commentary from Lever 1.

Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls added a commit that referenced this pull request Jul 17, 2026
briansrls added a commit that referenced this pull request Jul 17, 2026
…sistency)

regen_stage0 on the merged tree (main-merge #6780/#6783 + my space-complexity
work) changed exactly one seed file — v1_compiler_complexity.rs — activating
space_classes (the ComplexityReport space-order surfacing) in the compiled
compiler. main-merge seed was already consistent; this is the clean delta for
my complexity.dag change, keeping regen --verify green.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jul 18, 2026
…ane PR; P0 merged via #6663) (#6738)

* P2 pure-spec half: content-addressed artifact store — the first read eviction field

std.artifact_store (witness-realization plan P2, pure fold spec; host transport
is the second half and this spec is its single authority):
- ArtifactKey { closure_digest, emitter_identity, target_language, toolchain }
  -> artifact_key_hash via std.content_hash (one hash authority) — keying is
  ContentHash BY SHAPE; no mtime/existence input exists, so ExistenceKeyed is
  unwritable here (the #6352 wall by construction)
- store_over_provider READS CacheProvider.eviction and refuses construction
  over a non-SpacePacked provider (typed StoreRefusedEviction) — the eviction
  field's first behavioral consumer (memory-control audit F5)
- store_get bumps recency; store_put packs to budget by least-recent eviction
  with every eviction COUNTED in StorePutReceipt (refuse-or-count, never widen)
- budget stays a typed parameter beside the row for now: EvictionClass.budget
  carries cited upstream policy PROSE in extdeps rows (two concepts in one
  field); dissolve-on recorded in the module note for the variant split

Witnesses (all green by execution, current binary, SubstrateInputsOnly):
- store_construction_reads_eviction_holds (ScopeExit provider -> typed refusal)
- store_hit_and_stale_never_served_holds (toolchain mutation -> new key -> miss)
- store_budget_evicts_least_recent_counted_holds (touch ka, put kc -> [kb] evicted,
  within budget, survivor still hits)
- store_no_eviction_under_budget_holds

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

* P2 host-transport half: filesystem realization of the artifact store

extdeps.realization.artifact_store_fs — one transport handler bound to the
pure spec (std.artifact_store stays the single authority; a remote CAS is
the other handler). The keyed path ENCODES identity (store_root/<hash>.artifact),
so presence-at-path is a ContentKeyed hit for exactly that identity — not the
#6352 existence-keying (which keyed output presence over unhashed inputs).

SCOPE, honest and named: put/get only. The cited Filesystem service exposes
Write/Read but no Delete/List, so SpacePacked budget enforcement on the
persistent tier is unrealizable until those operations are added — until then
the disk tier grows unbounded and the in-process fold is the only packed tier.
Recorded in the transport note as the next rung, never a silent widen.

Witnesses green by wet execution (artifact observed on disk at its hash path):
- artifact_fs_roundtrip_holds
- artifact_fs_mutated_input_misses_holds (stale-never-served on the persistent tier)

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

* Plan doc: P2 status (both halves landed, green by execution; two named gaps)

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

* P1 (code): ObservePeakResidentAtSubject + the space algebra — memory becomes observable

- RealizationMeasureEffect gains ObservePeakResidentAtSubject (audit F2: the
  effect coproduct had exactly one variant, time; a Measured space fact was
  unproducible by construction)
- space algebra as time's DUAL (audit F4): space_measure_seq = max (sequential
  steps release), space_measure_par = add (concurrent steps co-reside), plus
  space_measure_list_seq; duality note records why the old sum was wrong
- fleet_intent receipt rollup: space summed over a sequential list -> now the
  peak (the parallel rule was applied to the serial axis); keystone witness
  FLIPPED to assert max AND assert != sum, so the old contract cannot silently
  return
- host physics: observed_peak_resident_bytes builtin (VmHWM in bytes) —
  registered in v1.compiler.method builtins, realized in the hand-maintained
  interpreter, FAIL-CLOSED when the host cannot report it (a fabricated 0
  would be a Measured lie, DESIGN section 5)
- peak_resident_measured_witness_test: the plan's P1 ACCEPT — the first
  CostAccount.space with basis Measured produced BY EXECUTION — declared
  ReadsLiveTree honestly (reads /proc through a builtin, the classifier's
  declared blind-spot class); plus the seq=max/par=add RED control

Receipts land in the follow-up commit with the regen-synced stage0 and the
rebuilt binary (pipeline in flight); the pure-.dag half already compiles clean
through the P0 wall.

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

* P1 (receipts): regen sync + green-by-execution verification

Regen-synced stage0 (the observed_peak_resident_bytes registration reaching the
generated method registry) after rebuilding the regen tool from merged main
(its compiled-in roster predated the Wave-2 crate-layout file; two-generation
discipline: build committed -> regen -> build).

Receipts on the rebuilt binary:
- peak_resident_measured_holds -> true : the FIRST CostAccount.space with
  basis Measured produced by execution (plan P1 ACCEPT; audit F2 discharged
  at the witness grain)
- space_seq_is_peak_not_sum_holds -> true (seq=max=5, par=add=8, list_seq=5)
- witness_space_rolls_up_across_receipts -> true FLIPPED (asserts max AND
  != sum; 1024/2048 samples discriminate)
- P0 regression: diagnostics_witness record_field_walls suite exit 0

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

* P3 MVP: emit-on-demand at the source grain — second run pays zero emit

The emit cache wired through the P2 store, keyed on INPUT identity:
inferred_tree_digest x emitter identity x target x artifact kind — the same
Hash=ContentHash authority the fnv1a64 convergence landed, composed by
artifact_key_hash. Cold: miss -> pure emit (v2 emit = serialize_target o
translate) -> put. Warm: served from the store WITH NO EMIT CALL IN THE ARM,
and the served bytes asserted equal to a fresh emit (the agreement receipt —
plan P3 ACCEPT (a) at the source grain).

Witnesses green by wet execution (emitted rust_add source observed on disk at
its hash path):
- emit_source_store_cold_then_warm_holds
- emit_source_store_mutated_emitter_misses_holds (emitter version bump -> new
  key -> miss; stale emitter output never served)
- emit_source_store_provider_gate_holds

Rung remainder (named): the native-artifact tier (zero BUILD — needs FLAG A,
the hermetic pinned-toolchain ruling, and the parse-census first customer) and
enrollment of the wet witnesses.

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

* Design: effect grants over namespaces — hermetic/wet dissolved into (frame x verb x subtree)

Operator rulings captured (2026-07-16): "hermetic" conflates four axes (input
closure / output reach / handler binding / selection eligibility — the doc's own
state-space-conflation failure mode, effect-system edition), and the fix must
reuse NAMESPACES directly rather than mint a "universe" vocabulary. An effect
target is a position in a containment tree that already exists (filesystem, URI,
proc, code names); permission is a grant of (verb x subtree) on a frame;
admissibility is the same prefix relation the naming lane walks — effects become
the containment structure's fourth consumer, not a fork.

Convergence map covers the proto-envelopes already in-tree (the hand-rolled
workspace_root path gate, std.resources.ResourceHandle, AuthScope,
LiveTreeDisposition) — all dissolve into derived projections. FLAG A reframed:
build admissibility becomes the first grant row (Read within closure + pinned
toolchain; Write within own workspace), scaffold-marked, dissolving into the
P-B enforcement seam — a row, not a mode exception.

Bound into the doc graph via the witness-realization plan's FLAG A section
(orphan wall re-verified green).

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

* Effect-grants design: the containment law (target lifecycle) + fix inherited orphan

Design refinement (operator, 2026-07-16): a write is frame-contained iff
(target within a frame-controlled namespace) AND (target lifecycle within
frame lifecycle) — the lifecycle conjunct is what the old "hermetic" intuition
was actually about, graded on the section-5 construction/validation axis
(LifecycleByConstruction: ephemeral container fs, netns-scoped loopback
receiver — persistence unwritable past the frame; LifecycleByConvention:
/tmp scratch + cleanup). Four named acceptance cases added up front so the
model cannot mislead: netns loopback = contained; container write = contained
by construction; /tmp scratch = contained by convention only (the artifact
store witnesses' honest current grade); BMC POST / repo-tree write = wet
under any grade.

Also: bind docs/plans/emitted-crate-partition-design.md into the doc graph
(frontier.dag provenance row) — it merged orphaned on main (8322580) and
the doc-reachability wall was red on main; wall re-verified true here, and
frontier.dag entry-compiles clean.

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

* Record duplicate-computation direction: one ComputationIdentity, N grains (execution-frame is the gap)

Operator direction (2026-07-16): duplicate-computation detection is not
shell-specific — "same inputs + deterministic process → same content-identity
→ the second is duplicate work" is the whole law; the surface it's read on is a
realization axis, not the concept. Records the three detection grains against
ONE ComputationIdentity:
- within-script (argv/ShellWord) — v2.lens.duplicate_computation, dissolves in (§7)
- within-graph (content_hash over Node subtrees) — v2.std.materialize MVP
- within-run execution-frame — the UNCOVERED grain, where the ~275s double-resolve
  lives (two compile_to_resolved calls in one v1-seed claim_executor process,
  invisible to both peers). Ladder-classed: shared-state frame ⇒ AuthoredDuplication
  ⇒ REWIRE (not cache), distinct from the cross-run isolation-boundary store
  obligation — same identity, remedy by frame.

Direction: the general detector must reach the execution-frame grain; the argv
lens then dissolves into it and the within-graph MVP extends down — one detector,
the surfaces its realizations. Doc is the roadmap ④'s linked carrier; orphan
wall re-verified green.

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

* Fix §5 fail-open: eval-call memo served stale world-reads (effect-dispatch odometer)

Found via the artifact-store List-after-Delete witness: the interpreter's
eval-call memo treated "no declared `uses` clause" as pure — and ZERO corpus
funcs declare `uses`, so every effectful named func was memo-eligible. A func
called twice with equal args in one eval served the FIRST result — e.g. a
Filesystem.List after a Delete returned the pre-delete listing. That is a
world-read served stale from cache: a silent §5 fail-open in the bootstrap
engine, not a witness quirk.

Fix (4 edits, transitive by construction): an effect-dispatch odometer on
InterpContext, ticked at the single eval_service_call chokepoint; the memo
refuses to STORE any call during which the odometer advanced. An observed
effect poisons cacheability — exactly the ladder's "FreshEffect/WorldRead is
never memoized" law, enforced at the realizer instead of by a vacuous uses-gate.
Value::eq stays the sole equality authority; pure calls still memoize.

Known residue (named): world-effecting BUILTINS (e.g. observed_peak_resident_bytes,
filesystem via the service path already ticks) — the odometer covers service
dispatch; a builtin-effect tick is the follow-up if a pure-memoized builtin ever
reads the world.

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

* Delete/List on the Filesystem service (operator Q2) — closes P2's persistent-tier gap

The cited Filesystem service exposed only Write/Read, so P2's SpacePacked budget
enforcement on the on-disk store was unrealizable (named gap in the P2 landing).
Adds the two missing operations, keeping the extdeps interface faithful to the
real dependency:

- filesystem_io.dag: Delete + List operations (List readonly)
- file transport gains a verb property (parse: 00_core file_transport_node +
  02_parse parse_file_fields thread `verb`; interpreter: dispatch_file honors
  verb "delete"/"list" via remove_file / sorted read_dir). Absent verb keeps the
  original content-param convention (write iff `content` param, else read).
- artifact_store_fs: artifact_fs_delete / artifact_fs_list wrappers
- witness: artifact_fs_delete_then_misses_holds — put -> listed -> delete ->
  miss -> unlisted, green by wet execution (also the discriminating input that
  surfaced the memo fail-open fixed in the parent commit)

Regen-synced (v1_compiler_parse.rs, v1_std_core.rs). Persistent-tier eviction
(the SpacePacked enforcer using List+Delete) is the follow-up now that the ops
exist.

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

* P4 v0: realize packing — width against MEASURED peaks, refuse-not-fabricate

The memory-safe packing half of `realize` (spine FLAG D), consuming P1's
measured space so the exit-137 failure mode (memory-blind packing OOMs) becomes
arithmetic. std.realize_pack:
- MeasuredPeak = PeakMeasured | PeakUnknown, derived from CostAccount.basis
  (P1's Measured space vs a Predicted guess)
- HostBudget = BudgetReadable | BudgetUnreadable — the typed read
- realize_pack_width -> RealizeVerdict = PackedWidth | MaturationReserve | BudgetRefused:
  * measured peak + readable budget -> PackedWidth min(independence, budget/peak),
    reusing realization_width.memory_bounded_shard_count (20% headroom reserved —
    the maturation-reserve margin; 100/25 packs to 3, not 4)
  * unknown peak -> MaturationReserve width-1 (first-run subject runs alone, its
    receipt converts it next round — the governor's admission logic, modeled)
  * unreadable budget -> BudgetRefused, NEVER the conservative_fallback_width
    fabrication (realization_width.dag:109 — the live §5 absorbing-fallback the
    memory-control audit flagged: budget unreadable answered with a number)

Witnesses (6, green by execution): packs within budget; capped by independence;
never exceeds budget (the exit-137 arithmetic control, W*peak <= budget by
construction); unknown-peak -> maturation reserve; unreadable-budget -> refuses;
measured-vs-predicted peak discrimination.

Remaining for P4: the width-1 fabrication in memory_aware_spawn_width is now
superseded for the measured path; wiring realize_pack into the executor's
per-runnable scheduling (consuming real getrusage receipts) is the integration
step. The math + refusal discipline land here first, green.

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

* Design: space complexity — the dual of the time/termination analysis

Operator direction (2026-07-16): extend the complexity analysis to space (the
gap). Derived, not measured (§4: bounded/forward ⇒ checked not discovered —
measuring peak RSS is the reflection-evidence cop-out). Two readings: asymptotic
(O(n)) AND concrete derived bytes ("known/defined to these bounds"). Underivable
= counted frontier now, hard error later (fail-closed ratchet).

The key finding that makes it a dual, not a new analysis: ComplexitySummary
already carries work/span/output_size as CostExpr (axis-agnostic), and CostSum
is a fold — time SUMS over iterations, space takes the MAX (sequential residency
releases). That is exactly P1's space_measure_seq=max lifted to CostExpr. So
peak_space = space_of(work) — one transform swapping sum/max, accumulator term
reusing output_size, recursion depth bounded by the SAME DescentEvidence that
proves termination. Two readings of one descent structure (§2).

Folds five threads onto one page: audit F2/F3 (space unobserved/underived), P1
(the residency algebra — reused as the transform), P4 (re-point pack input from
MeasuredPeak to derived bound; retire the reactive governor), the 2026-07-12
ruling (derived not authored literals), the allocation model (the derived
per-witness bound IS the up-front allocation; Σ ≤ budget = GUARANTEED mode at
witness grain). Sequence: witness-grain concrete space first (closed closures),
then asymptotic, then re-point P4, then ratchet the frontier to error.

Bound into the doc graph via the witness-realization P1 note (which this
supersedes as the keystone); orphan wall green.

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

* Space complexity increment 1a: peak-working-set derivation, the dual of time

The space-complexity analysis's core, as the structural dual of the existing
time cost-expr — green by execution, no rebuild (interpreted from source).
In src/v1/complexity.dag, beside the cost algebra it duals:

- space_of(work: CostExpr) -> CostExpr : the transform. Sequential steps RELEASE
  so time's CostAdd becomes CostMax; concurrent steps CO-RESIDE so time's CostMax
  becomes CostAdd (P1's space_measure_seq=max / space_measure_par=add, lifted to
  CostExpr); a fold's CostSum collapses to its body's peak (iterations release).
  CostUnknown passes through fail-closed.
- fold_peak_space(body_peak, output_size) : adds the accumulator/output_size term.
- eval_cost_expr_concrete / eval_size_expr_concrete : lower a closed expr to
  concrete bytes (Absent on any unknown/free var — refuses, never fabricates).

Witnesses (6, green by execution, --source-root src/v1):
- reducing_fold_is_constant_space: O(n) time fold -> O(1) space (the headline)
- sequential_releases_max_not_sum / parallel_coresides_add_not_max: the P1 duals
- concrete_derived_bytes: closed expr -> exact bytes (40)
- fold_that_builds_is_linear_space: output_size 100*4 + body 4 -> 404 bytes
- unknown_cost_is_fail_closed_space: CostUnknown -> unknown space, concrete refuses
  (the SpaceBoundUnknown counted bottom; hard-error ratchet is the later stage)

Design: space-complexity-design.md §2. Not floor-enrolled yet — imports
v1.compiler.complexity so needs --source-root src/v1 (like the v1-internal
tests); enrollment (host bin or v1-root discovery) is the follow-up, alongside
the ComplexitySummary.peak_space field (38 construction sites) and the P4
re-point onto the derived bound.

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

* Space complexity increment 2: asymptotic reading (O(n) etc.), space order below time

The second reading the operator asked for — asymptotic space class — reusing
std.induction's CostBound/cost_poly on space_of(work). Green by execution, no
rebuild (interpreted). In src/v1/complexity.dag:

- cost_expr_degree(e) -> Int? : polynomial degree. CostSum over a size var = +1
  factor of n; seq/par take MAX degree; products ADD; bare log = degree 0
  (sub-linear); Absent = frontier (fail-closed, never a fabricated degree).
- space_asymptotic_bound(work, param) = degree_to_bound(cost_expr_degree(space_of(work)))
  -> ConstantBound | cost_poly(...) | ForeverBound. time_asymptotic_bound is the
  same on the raw work, for the side-by-side.

Because space_of collapses the CostSum a reducing fold's TIME carries, space
order is <= time order by construction. Witnesses (4, green):
- reducing_fold: O(n) TIME (degree 1), O(1) SPACE (ConstantBound)
- nested_reducing_loop: O(n^2) time, O(1) space (both CostSums collapse — the
  striking dual)
- parallel_region: constant space
- frontier_maps_to_forever_bound: CostUnknown -> ForeverBound, not a degree

Design: space-complexity-design.md §3. Increments remaining: wire peak_space into
ComplexitySummary (rebuild-gated, 38 sites), re-point P4, ratchet the frontier.

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

* Wire space-complexity into ComplexitySummary (peak_space + concrete fill)

Extend the landed space-complexity analysis (space_of / fold_peak_space /
eval_cost_expr_concrete) into the compiler's per-function summary.

- ComplexitySummary gains an OPTIONAL peak_space: CostExpr?. Optional so the
  P0 field wall (04_infer) skips it: all ~38 existing construction sites stay
  unchanged, an absent peak_space = the SpaceBoundUnknown counted frontier
  (fail-closed staging). Verified: complexity.dag entry-compiles 0 diagnostics.

- Derived once at the finalized per-function summary (get_or_compute_summary's
  `simplified`) via derive_peak_space: space_of(work) for a scalar result,
  additive fold_peak_space(space_of(work) + output_term) for a collection
  result (the `result` output_size entry). Intermediate/error/external/seed
  summaries leave peak_space absent by design.

- cost_account_space_from_summary(summary, size_env) -> ByteSize? fills
  CostAccount.space (basis Derived): eval peak_space at a closed size_env to a
  concrete ByteSize; absent peak_space or an underivable expr returns none,
  never a fabricated bound.

- New witness complexity_summary_space_witness_test.dag (4 test fns, green by
  interpretation): derived peak yields expected bytes; absent peak -> none;
  underivable (CostUnknown) peak -> none (RED control); reducing-fold work is
  O(1) space regardless of n.

Follow-up (out of scope): regen + rebuild-to-seed to activate the compiled
realization.

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

* P4 re-point: pack against the DERIVED bound, not measured peak — seam closed

Operator direction (derive, don't measure — §4). std.realize_pack re-pointed off
P1's measured peak onto the statically DERIVED space bound:
- MeasuredPeak/PeakMeasured/PeakUnknown -> DerivedBound/BoundDerived/BoundUnknown
- measured_peak_of(CostAccount) -> derived_bound_of(derived_space: ByteSize?):
  Present = the derived working-set bound, Absent = SpaceBoundUnknown (the
  fail-closed frontier). P4 is now decoupled from CostBasis — it consumes the
  ByteSize? that cost_account_space_from_summary (eeeda2b, the subagent's
  ComplexitySummary wiring) produces. That closes the seam:
  ComplexitySummary.peak_space -> space_of derivation -> cost_account_space_from_summary
  -> ByteSize? -> derived_bound_of -> realize_pack_width.
- realize_pack_width / realize_fits_budget take DerivedBound; BoundUnknown -> the
  width-1 maturation reserve (a not-yet-derivable subject runs alone, not a
  fabricated number); the refuse-not-fabricate discipline unchanged.

Measurement (P1's ObservePeakResidentAtSubject) is demoted to at-most a
falsifier, never a scheduler input — the whole memory-control line is now
derived, not observed.

Witnesses (6, green by execution, interpreted — no rebuild): packs within
budget (headroom-reserved 3, not 4); capped by independence; never exceeds
budget (the exit-137 arithmetic control); BoundUnknown -> maturation reserve;
unreadable budget -> refuses; derived-vs-frontier bound discrimination (the new
ByteSize? seam).

Remaining for P4: activate in the seed (regen — gated with the space-complexity
seed activation) + wire realize_pack into claim_executor per-runnable scheduling.

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

* Regen seed: activate space-complexity peak_space in the compiled compiler

regen_stage0 activated the complexity.dag changes (peak_space field + space_of +
concrete evaluator, and the get_or_compute_summary derivation) into the generated
seed v1_compiler_complexity.rs — the one file that changed (surgical; the other 94
generated files byte-identical). Built on srv1 (128 cores, 4m17s cold / 2m34s
rebuild — off the memory-constrained Pi that watchdog-crashes on this crate).

regen_stage0 --verify: regen_divergence_count=0 — committed stage0 matches a fresh
self-compile, so the byte fixed point holds with peak_space live. The compiled
compiler now derives peak_space during real complexity analysis (previously only
interpreted from source).

Remaining (flagged by the wiring pass): the interpreter RAISES on an omitted
optional field while the seed reads None gracefully — latent-safe today
(cost_account_space_from_summary is only called on simplified summaries, which
always set peak_space), reconcile when a broader consumer lands.

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

* Space classes in ComplexityReport (observable on real code) + floor-classify new witnesses

Two things the srv1 corpus validation surfaced.

1. Observability: ComplexityReport gains space_classes: Map<String,String> beside
   function_classes — build_complexity_report now derives it via
   classify_complexity(space_of(work)) per function, so the derived SPACE order
   is observable for every REAL gunbc function (not just synthetic CostExpr
   witnesses). TopoBuildAcc threads it; empty_complexity_report seeds it.

2. Floor classification (validation caught my new witnesses breaking the hermetic
   floor — neither a space-complexity logic regression):
   - The three space witnesses import v1.compiler.complexity, unresolvable in the
     discovered corpus's roots -> a FATAL resolve halt at entry 46. Excluded from
     discovery (they run in the v1 lane via --source-root src/v1; host-bin
     enrollment like diagnostics_witness is the proper follow-up).
   - artifact_store_fs_witness does real Filesystem.Write -> hermetic refuses
     (correctly). Excluded from hermetic discovery (wet lane), same pattern as the
     existing ci_deploy_observed_wet / host_effect_apply wet exclusions.

Interpreted entry-compile green; srv1 regen+rebuild+corpus re-validation follows.

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

* Fix the debt srv1 corpus validation caught: residue wildcards + the last wet witness

The srv1 corpus run (1900 PASS, and the space-complexity seed activation proven
corpus-safe) surfaced 4 failures, all from witnesses I added this session — none
a logic regression:

- 2 non_fold_residue FAILs: my witnesses + realize_pack used `_ =>` wildcards over
  closed coproducts (CostExpr, CostBound, RealizeVerdict) — the §4 residue the lens
  bans. Fixed by making them exhaustive/behavioral: realize_pack + its witness
  list every RealizeVerdict arm; the space witnesses now assert through the
  concrete evaluator (eval_cost_expr_concrete, exhaustive Optional) and the
  polynomial degree (cost_expr_degree) instead of matching CostExpr/CostBound
  structure — cleaner behavioral tests (sequential releases -> eval 50 not sum 80;
  parallel co-resides -> eval 80 not max 50) with ZERO wildcards.
  non_fold_residue_clean_holds -> true (0 unrostered residue, re-verified).
- 2 emit_source_store FAILs: real Filesystem.Write in hermetic mode. The path is
  test/claim/manual/ (not test/manual/), so the existing exclusion missed it;
  added emit_source_store_test.dag explicitly (wet lane).

All rewritten witnesses green by interpretation; final srv1 corpus re-validation
follows.

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

* Regen seed: space_classes into the compiled compiler (merged-tree consistency)

regen_stage0 on the merged tree (main-merge #6780/#6783 + my space-complexity
work) changed exactly one seed file — v1_compiler_complexity.rs — activating
space_classes (the ComplexityReport space-order surfacing) in the compiled
compiler. main-merge seed was already consistent; this is the clean delta for
my complexity.dag change, keeping regen --verify green.

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

* P4 handoff: executor cutover is a bridge call, not a self-host dependency

Records the corrected framing in the plan's P4 section: claim_executor is the
terminal bootstrap kernel (not a self-host emit target) and already interprets
.dag, so it can call realize_pack through run_in_context_with_args rather than
forking the packing law into Rust (§2) or waiting on the 27-module frontier.
Seam: surface the derived bound, read the governor's budget, call realize_pack,
advisory-first then demote the governor.

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

* Fix compile-clean gate: move space-complexity witnesses out of dag/ tree

The three space-complexity witnesses import v1.compiler.complexity (a src/v1
module), but lived in dag/test/claim/. The whole-tree compile-clean gate
compiles [dag, src/v2] WITHOUT src/v1, so their imports could not resolve —
red as 'module v1.compiler.complexity not found' whenever a src/v1 touch
forces the whole-tree baseline. Discovery-exclusion handled the runner but
not the gate; a dag/ file simply cannot import from src/v1.

Move them to src/v1/test/claim/ (compiled with src/v1, not swept by regen's
seed-closure walk, not in discovery scan dirs) and drop the now-dead exclusion
substrings. All 6+4+4 test fns pass from the new home via
claim_batch --source-root src/v1 --source-root dag --source-root src/v2.

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

* Fix batch-4 gate regressions: extdeps authority anchor + drop redundant frontier binding

- extdeps_external_authority_gate: artifact_store_fs.dag (P2, new) was the only
  extdeps/realization module missing the extdeps_external_authority_anchor every
  sibling declares. Add it (Https -> the realization dir, matching v1_handler).
  All 9 realization modules now carry exactly one anchor.
- self_host_realized_comparison / cleanup: drop emitted_crate_partition_plan_doc_provenance
  from frontier.dag. It was a doc-reachability workaround added when the design doc
  was orphaned; main #6828 now links it from DESIGN.md (line 92), so the row is a
  redundant duplicate binding (unreferenced). frontier.dag is now byte-identical to main.

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

* Fix self_host_realized_comparison: drop v2 import from relocated witnesses

Moving the space witnesses to src/v1/ (to fix compile-clean) put them in
regen_stage0's compile surface ([src/v1, dag]) — but they still imported
v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } (src/v2, not in
regen's roots), so 'regen_stage0 --emit-fresh' failed with unresolved import,
and self_host_realized_comparison_reads_real_bytes then couldn't read the
fresh-emitted bytes (No such file or directory) -> Bool(false).

The v2 import fed only a 'data live_tree_disposition = SubstrateInputsOnly'
metadata decl for discovery-based affected-set selection, used in no test fn
and moot now that these run manually. Drop the import + decl; the witnesses
become pure [src/v1, dag] (std + v1.compiler.complexity), compile clean under
both regen and the manual runner, and all 6+4+4 test fns still pass.

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

* Delete homeless space-complexity witnesses (operator: 2026-07-18); declare Rust-test follow-up

The three space-complexity .dag witnesses test v1.compiler.complexity (a src/v1
compiler-internal module) and had no clean home: dag/ fails the compile-clean
gate's cross-layer import ([dag, src/v2] roots, no src/v1), and src/v1/ makes
regen_stage0 --emit-fresh emit them as unregistered stage0 seed files (breaking
self_host_realized_comparison). The analysis stays proven in-seed by execution
(regen, runs every compile); the discriminating behavioral REDs are recorded in
space-complexity-design.md as a declared follow-up to re-add as Rust tests in
compiler_tests.rs when P4 makes the coverage load-bearing.

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

---------

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Sep 2, 2026
…o a file that exists was refused as absent

THE CUT SURFACED THIS; it is the root the deleted chdirs were hiding. `canonical_shared_index_roots`
is the KEY and the BUILD input both, and normalizing an absolute root to its repo-relative form is
right for the key -- the executor's `$ROOT/dag` and the plan's declared `dag` must address ONE index
(review 39118 / #6783). But the same relative spelling reached
`try_index_source_root_into_module_index`, which stat'd it against the PROCESS CWD.
`try_anchor_source_root` re-anchors above it, except that every one of its arms requires `is_dir`,
so a root that EXISTS BUT IS A FILE fell through unanchored. The two refusals then swapped: a file
that exists was reported as `source root does not exist`. That is a located lie about the
filesystem, and it collapses exactly the distinction the caller built two arms to hold apart --
create the file versus move it -- which is the state-space conflation section 5 names.

THE CONTROL IS THE ISOLATED SINGLE-TEST RUN, not the full suite, because the full suite's green is
the artifact under investigation. `cargo test --release -p v1-compiler --lib
a_file_named_as_a_source_root_refuses`, one test, nothing else in the process:

  main               0 passed; 1 failed   (identical panic, identical message)
  this branch before 0 passed; 1 failed
  this branch after  1 passed; 0 failed

MAIN ALREADY FAILS THIS TEST IN ISOLATION. It passes in main's full CI run only because another
test concurrently ran `set_current_dir(workspace_root())` inside its window. So main's green there
is not evidence that the code works -- it is evidence that a second test happened to move the
process. Deleting the seven dead chdirs did not break this test; it removed the cover that was
hiding an existing production defect, which is what a delete-first census is for. Reading the diff
as "main's 1 red becomes 2" inverts it: a defect became visible.

All 13 `entry_admission_tests` pass, so the neighbouring refusals and the module's own positive
control survive -- the fix restores the distinction rather than flattening it.

SCOPE: resolution added, JUDGMENT untouched. Still two arms, still fail-closed, no new parameter, no
fallback, and the stat is not made tolerant. Diagnostics keep the caller's own spelling of the root,
which is what the caller passed and can act on. `try_anchor_source_root` is deliberately NOT changed:
three other callers treat its result as a directory to walk, and widening it there would alter their
behaviour for no gain here.

HOW MANY OTHER TESTS WERE PASSING BY THE SAME ACCIDENT: exactly one, this one, measured rather than
estimated. main on GitHub Actions fails 1; this branch with the chdirs removed and before this fix
failed 2; the delta is this test alone.

Also in this commit, from review 58606: the raw-string close test took the next `hashes` characters
and required them all to be `#`, but over a remainder shorter than `hashes` that iterator is empty
and `all` is vacuously TRUE, so a quote near end-of-line would false-close the string and hand the
rest of a fixture back to the code scanner -- the same brace-depth skew the raw-string handling
exists to prevent, arriving by a different door. Bounded explicitly, with the end-of-line case added
to the control.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UafEkYSRqe8MgAXzykxEao
gunbai-bot Bot added a commit that referenced this pull request Sep 2, 2026
…e is seven dead chdirs in the gating lane (#10033)

* The memo-poisoning arm has an empty population; the occurring cwd race is seven dead chdirs in the gating lane

Dispatched on a candidate mechanism: workspace_root memoizes a .git-ancestor walk from the process
cwd, the suite holds dozens of set_current_dir sites, fixtures run git init, so the memo could
freeze onto a fixture. The census refutes it. Every forward set_current_dir in the repository
targets the checkout root: 37 of 38 in cli_run.rs bind workspace_root() one line above the call,
and the git-init fixture is only ever passed as Command::current_dir to a subprocess. No RED for
that arm is authorable against this tree, so it is UNSUPPORTED, not disproven -- one chdir to a
non-checkout path arms it.

What IS occurring needs no wrong root. The restore idiom hands the cwd back while a sibling test is
mid-read, so the victim population is every non-ignored test in the binary, not the mutators; the
file's own entry_admission_tests note already records the measurement, a different pair failing on
each run of identical code. Seven such tests run in the required unit lane, and in all seven the
chdir is DEAD -- every consumer already takes an explicit root -- so this is a pure removal, not
the chdir repair the source records as measured-wrong.

with_workspace_cwd is KEPT: enumerated first, 24 callers, 23 of them ignored live-corpus tests. The
gate keys on REACHABILITY, since all seven reached the write through a helper and a body-local grep
would be green over every one of them. RED shown by reintroducing one chdir behind a helper: the
gate names exactly wall_now_authority_graph_is_total, nothing else.

Rung: found below the ladder (a redirected read is a silently wrong answer, no typed refusal).
Ceiling 4 and decidable -- a root passed as a parameter has no shared cell to race on. The gating
population now sits at 2, mechanically preventable, this lens being what keeps the state absent.
Residue, named not hidden: 69 ignored mutators plus 7 in v1-compiler-tests, outside the gating lane;
next-rung trigger is the capability that every live-tree test resolves from an explicitly passed
root. No rung_drop row -- nothing is lowered.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UafEkYSRqe8MgAXzykxEao

* Re-project docs/design-ledgers.md after the merge took the incoming generated bytes

The generated-artifact merge driver refused docs/design-ledgers.md with no conflict markers (both
sides changed the path since the merge base), which is the driver working: taking the ours side
there would have dropped the other side's authority-derived bytes silently. Resolved by taking the
incoming bytes and re-running the projection over the merged .dag authority, so the file is derived
rather than hand-reconciled. Delta is exactly the one row this branch adds.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UafEkYSRqe8MgAXzykxEao

* Review #58565: seed the closure on the bare callee, and drop the orphaned doc block

Two findings from the approving review, both real.

The gate seeded on the fully-qualified spelling `std::env::set_current_dir`, which is only the
spelling the corpus happens to use today. A future author writing `use std::env;` and calling
`env::set_current_dir(..)`, or importing the function and calling it unqualified, would have
reintroduced the exact defect against a green gate -- a wall that holds only for one path spelling
of its subject. Seeding is now the identifier-bounded bare callee, so every path spelling seeds the
closure. The rename-import residue (`use std::env::set_current_dir as chdir`) is stated in the
module rather than left implied; it is strictly narrower than the qualified-only form it replaces.

The duplicate doc block was my own editing miss: rewriting the module on brace-depth containment, I
excised the old `mod` but left its doc comment orphaned above the new one, so the same four
paragraphs appeared twice.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UafEkYSRqe8MgAXzykxEao

* Review #58580: swallow raw strings in the projection, and control the brace-depth leak

The review called this minor on the grounds that the file has no raw strings. It has two: a TOML
manifest and a block of .dag source carrying three brace pairs. Both are brace-BALANCED, so the
depth array was not skewed and the gate was correct by coincidence of their content rather than by
construction — the third time in this lane that this check has been accidentally right.

The failure it leaves open is not minor. An unbalanced brace inside a fixture shifts the depth array
from that line to the end of the file, so containment is wrong for every declaration after it, and
the wall then misses real offenders while staying green. That is the UNDER-approximating direction:
the wall asserts emptiness so it cannot see it, and the over-approximation bound in the non-vacuity
control is the wrong side. A compiler's own test corpus is exactly where a deliberately unbalanced
fixture shows up — a parse-refusal probe for an unclosed brace is the obvious one.

`code_projection` now tracks raw strings across lines with their hash count, and refuses to read the
opener when it is the tail of an identifier. The control asserts on synthetic projections rather
than the live file, so it keeps its discriminating power when this file's own raw strings change:
an unbalanced brace inside a hash-delimited raw string must not leak into the depth array, the callee name inside a raw
string must seed nothing, and — the positive control — the same call outside one must still seed.

MEASURED: with the raw-string branch disabled the new control fails on the leaked depth array
([0,1,1,2,2,1,2,1], ending at 1) while the wall and the non-vacuity control both stay GREEN — 2
passed, 1 failed. That is the receipt that the existing controls could not have caught this.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UafEkYSRqe8MgAXzykxEao

* Re-project the doc artifacts after the merge, so the committed bytes are derived

The merge hit three conflicts on the same class of file. `dag/gunbc/recurring_failure_mode.dag` was
a REAL text conflict: another lane appended `liveness_probe_read_as_currency` to the roster while
this branch appended its own row, and the two collide on the closing bracket alone. That is the
additive contention the module's own header describes, and both classes are independent, so both
rows are kept. `DESIGN.md` and `docs/design-ledgers.md` conflicted with ZERO markers, which is the
generated-artifact driver refusing rather than silently taking a side.

Resolved by taking the incoming bytes for both projections and re-running the wet regen over the
MERGED `.dag` authority, so what lands is derived rather than reconciled by hand. The regen rewrites
the whole projected population and moved exactly these two files by one line each — this branch's
row, back in both the index and the ledger, with the other lane's row intact beside it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UafEkYSRqe8MgAXzykxEao

* Source discovery stat'd a relativized root against the process cwd, so a file that exists was refused as absent

THE CUT SURFACED THIS; it is the root the deleted chdirs were hiding. `canonical_shared_index_roots`
is the KEY and the BUILD input both, and normalizing an absolute root to its repo-relative form is
right for the key -- the executor's `$ROOT/dag` and the plan's declared `dag` must address ONE index
(review 39118 / #6783). But the same relative spelling reached
`try_index_source_root_into_module_index`, which stat'd it against the PROCESS CWD.
`try_anchor_source_root` re-anchors above it, except that every one of its arms requires `is_dir`,
so a root that EXISTS BUT IS A FILE fell through unanchored. The two refusals then swapped: a file
that exists was reported as `source root does not exist`. That is a located lie about the
filesystem, and it collapses exactly the distinction the caller built two arms to hold apart --
create the file versus move it -- which is the state-space conflation section 5 names.

THE CONTROL IS THE ISOLATED SINGLE-TEST RUN, not the full suite, because the full suite's green is
the artifact under investigation. `cargo test --release -p v1-compiler --lib
a_file_named_as_a_source_root_refuses`, one test, nothing else in the process:

  main               0 passed; 1 failed   (identical panic, identical message)
  this branch before 0 passed; 1 failed
  this branch after  1 passed; 0 failed

MAIN ALREADY FAILS THIS TEST IN ISOLATION. It passes in main's full CI run only because another
test concurrently ran `set_current_dir(workspace_root())` inside its window. So main's green there
is not evidence that the code works -- it is evidence that a second test happened to move the
process. Deleting the seven dead chdirs did not break this test; it removed the cover that was
hiding an existing production defect, which is what a delete-first census is for. Reading the diff
as "main's 1 red becomes 2" inverts it: a defect became visible.

All 13 `entry_admission_tests` pass, so the neighbouring refusals and the module's own positive
control survive -- the fix restores the distinction rather than flattening it.

SCOPE: resolution added, JUDGMENT untouched. Still two arms, still fail-closed, no new parameter, no
fallback, and the stat is not made tolerant. Diagnostics keep the caller's own spelling of the root,
which is what the caller passed and can act on. `try_anchor_source_root` is deliberately NOT changed:
three other callers treat its result as a directory to walk, and widening it there would alter their
behaviour for no gain here.

HOW MANY OTHER TESTS WERE PASSING BY THE SAME ACCIDENT: exactly one, this one, measured rather than
estimated. main on GitHub Actions fails 1; this branch with the chdirs removed and before this fix
failed 2; the delta is this test alone.

Also in this commit, from review 58606: the raw-string close test took the next `hashes` characters
and required them all to be `#`, but over a remainder shorter than `hashes` that iterator is empty
and `all` is vacuously TRUE, so a quote near end-of-line would false-close the string and hand the
rest of a fixture back to the code scanner -- the same brace-depth skew the raw-string handling
exists to prevent, arriving by a different door. Bounded explicitly, with the end-of-line case added
to the control.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UafEkYSRqe8MgAXzykxEao

* Roster the fourth instance: a predicate vacuously true on an empty domain is not a check until its domain is proven non-empty

Three of this PR's own defects and one review finding were the same class, and
the class was not on the roster. Files gunbc.recurring_failure_mode
predicate_vacuously_true_on_an_empty_domain and re-projects DESIGN.md and
docs/design-ledgers.md from it.

The specimen is this PR's own review-58606 repair: a raw-string scanner closed
its delimiter with take(hashes).all(..), which is TRUE over a remainder shorter
than hashes, so a quote near end-of-line closed a raw string that was still
open. The wrong answer was silent, well-formed, and in the under-approximating
direction -- the one direction neither the wall's emptiness nor the
over-approximation bound can see.

The row carries the recognition rule (ask what the universal returns on the
empty collection, and whether a boundary can produce empty), and is bounded
against the three neighbours a roster check cleared before it was written:
executed_conjunct_discriminates_nothing is about a corpus that never builds the
falsifying input; empty_observation_narrow is about evidence, one layer up;
incidental_denominator_as_wall is a guard holding on a coincidence that does
hold. Here nothing holds -- the guard returns TRUE about a population it never
examined.

Rung: outside the ladder. Ceiling 4, decidable per site.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UafEkYSRqe8MgAXzykxEao

* Widen the cwd wall to the population it declared: the range of a check is a degree of freedom its coverage can hide in

Review 58640 is right and the finding is this PR's own class, in this PR's own
guard: `closure_over_self` scanned only `cli_run.rs` while the scope declaration
claimed every test the required `--lib` lane runs. That puts the reported rung
above the executed evidence, which DESIGN §4b(1) reads as the minimum across
in-scope paths. Widening, not narrowing, because the cost was measured first.

WHAT IT COST. A change of input plus one algorithmic repair: the old edge
builder asked each known name against each line, quadratic in lines x
declarations, which does not survive 238 files. `called_names` extracts applied
identifiers once per line under the identical predicate (same identifier
boundary, same `(` follow). Crate-wide run is FASTER than the single-file one
was -- 0.46s against 8.42s -- so narrowing would have been buying the weaker
wall for nothing.

THE SECOND TRAP, MEASURED NOT REASONED. Resolving cross-file edges by bare name
merges every declaration of a shared spelling. This crate declares `main` 18
times, `run`, `new`, `probe`, `foo` besides, so one production seed
(`pre_push::run_inner`) bridged into hundreds of unrelated tests -- a wall
naming `two_identical_runs_mark_nothing_unstable` as a cwd offender is the
absorbing fallback §5 refuses, since it cannot be acted on and would be
silenced. Seeding the frontier from those callers and closing over it
reproduced the blowup one step later. What survives: intra-file edges always,
cross-file edges only for names declared exactly once, and the ambiguous
remainder returned and contracted on BY IDENTITY -- exactly {`main`, `run`},
the two entry points above the `pre_push` seed -- so a new ambiguous
mutator-reaching name refuses instead of silently leaving a hole.

BOUNDS RE-DERIVED AGAINST THE NEW DENOMINATOR, since a bound calibrated on one
file is the absorbing shape this guard already caught once. Measured crate-wide:
10199 declarations, 78 reaching, 687 non-ignored tests. The collapse guard moves
1000 -> 8000, which is above anything one file can supply, so a fallback to
single-file scanning fails it. The over-approximation bound moves decls/4 ->
decls/50: the old one would now admit 2549 and would have passed the name-merge
arm above.

Also extends `ambient_process_state_read_by_a_concurrent_reader` with the fifth
form and the general shape: every degree of freedom in a check's subject --
which call sites, which spellings, which lexical states, which domain, which
files -- is a place its coverage can be narrower than its claim.

Executed: gate 3/3 green crate-wide, clippy --all-targets -D warnings clean.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UafEkYSRqe8MgAXzykxEao

* Roster the class the whole PR is a specimen of: a check's subject is narrower than the claim it is cited for

Six instances of one defect turned up in a single guard tonight -- four found by
the author, one by review 58640, one produced by the fix for the fifth. That is
a class, and it was leading the tail of the cwd row where it did not belong.
Files gunbc.recurring_failure_mode check_subject_narrower_than_its_declared_claim
and re-projects DESIGN.md and docs/design-ledgers.md from it.

The generalisation leads the row: every degree of freedom in a check's subject
-- which call sites, which spellings, which lexical states, which domain, which
files -- is a place its coverage can silently be narrower than the population it
is read as covering. The route is what hides it: the narrowing is never a
decision, it is the shape of the first implementation. An author edits one file
so the scanner reads one file; the corpus spells the call one way so the seed
matches one spelling; the fixture has no raw strings so the projection has no
raw-string state; the window is never short so the universal is never vacuous.
Each is locally reasonable and none is written down, which is why the gap
survives a review that reads the check's LOGIC and never asks what its INPUT
was.

Rung: outside the ladder, and the reason is the load-bearing part -- a wall
whose range is too narrow is green for exactly the same reason a wall over a
clean corpus is green, so under DESIGN 4b(1) it inflates the rung of everything
it is cited for. Ceiling 3, decidable: a check whose subject is a VALUE it
receives rather than a scope its implementation re-derives cannot range over
less than it claims, because claim and range are then one object.

The row states what is NOT claimed: widening does not always win. Narrowing the
declaration to match the range is equally honest; what is forbidden is leaving
the two different, and the choice is a cost measurement. On this specimen
widening cost one change of input plus one linear-time rewrite of a quadratic
edge builder, and the wider check runs faster than the narrow one -- 0.46s
against 8.42s -- which is what settled it.

The cwd row now cites this class by identity instead of carrying the
generalisation itself, so the roster keeps one authority for it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UafEkYSRqe8MgAXzykxEao

* Write the gate down as machinery that dissolves, not a permanent lens

Review 58674 is right that this module is several hundred lines of hand-Rust
re-authoring a slice of Rust name resolution, and that it does not survive the
terminal architecture by DESIGN section 6 test. That is a property of the
artifact, so it belongs ON the artifact rather than in a review thread.

States the dissolution explicitly under section 4b(4): rung-2 machinery is
deleted BY the climb it enables, not kept beside it. When the trigger the module
already names lands -- every reader in the population resolving from an
explicitly passed root -- the ambient write has no consumer, the invalid state
has no constructor, and nothing remains to scan. The wall, the closure and the
projection controls all go together, since the controls exist only to make this
scanner honest and have no subject once it is gone.

Doc only, no behaviour change.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UafEkYSRqe8MgAXzykxEao

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <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