v2 memory-control audit + witness-realization plan + P0 field wall (568→45 drained) by briansrls · Pull Request #6663 · gunb-ai/gunbc

briansrls · 2026-07-15T04:05:39Z

What

Two plan docs, no source changes. Investigation triggered by the first whole-corpus witness run on a memory-constrained host (Raspberry Pi 3, 905 MB): all 1837/1837 hermetic witnesses PASS at da71e41d0, but the run needed 13 GB of swap (VmSize 6.25 GB, ~8.4 MB/entry retained, never released) and 87% of its 95 minutes was resolve, not execution. That receipt prompted the question this PR answers: is memory understood/controlled ahead of the Realization switch (ROADMAP ④)?

`docs/plans/v2-memory-control-audit.md` — findings (each green- or refuted-by-execution, with a calibration control)

F1 (headline, corpus-wide, not memory-specific): record-literal field presence and field types are unchecked. gunbc compile --target dag (the compile-clean gate's own path) accepts a CacheProvider with eviction omitted, eviction: 42, a CostAccount missing 3 of 4 fields, and a DependencyView with kind: 999 — all 0 diagnostics. Calibration: a bogus field name hard-errors, so the typechecker runs — it checks names only. materialization_ladder.dag:28's "CacheProvider cannot be written without an EvictionClass" is false by execution, and every "by construction = required field" claim in the tree rests on an unenforced property.
F2 (keystone): RealizationMeasureEffect has exactly one variant (ObserveElapsedAtSubject). v2 has no effect that can observe space, so CostAccount.space can never be Measured.
F7: spine FLAG D assigns memory-packing to realize over measured peak RSS (min(width, budget/peak); §6-1 names the exit-137 failure mode). F2 makes that input unproducible — realize is unbuildable as designed, and the memory_governor's dissolve-on can never fire.
F6: of run ≜ realize ∘ materialize ∘ dependency_view, realize and dependency_view have 0 definitions; materialize is analysis-only; spine.dag doesn't import v2.std.dependency; DependencyView is flat (no frames).
F4: space has no seq/par algebra; fleet_intent.dag:168 sums space over a sequential rollup (peak composes as max serially, add in parallel) and a keystone witness asserts the sum.
F5: eviction has no reader anywhere; inverting every eviction class in the ladder witness leaves 24/24 green.
F10 (ordering constraint): every v2 witness evaluates on the v1 tree-walker (claim_executor.rs:26); the only realized eviction is two v1 Rust mechanisms the ladder never dispatches. Deleting v1 zeroes realized eviction while declared eviction stays green.

`docs/plans/witness-realization-plan.md` — the forward path (P0–P6)

Anchor scenario (operator): emit witnesses to native code and schedule the runs with realization. Splits the v1 crutch into the execution crutch (removed by this plan, riding the seed emitter — the emitter is part of the artifact key, not the architecture) and the compiler crutch (self-hosting, separate lane).

P0 field wall (F1; staged ledger→drain→wall) → P1 space observable (ObservePeakResidentAtSubject; host physics already in claim_batch, unmodeled; space seq=max/par=add) → P2 content-addressed artifact store (first real CacheProvider, first reader of eviction, ExistenceKeyed unwritable by shape) → P3 emit-on-demand v0 (wrap the landed emit_host transport; ROADMAP's own accept criteria) → P4 realize v0 (measured-peak packing; CostUnknown → width-1 maturation reserve; governor dissolve-on fires; acceptance host: the 905 MB Pi with flat VmSwap) → P5 demands derived from dependency_view (materialize Share drives real reuse) → P6 cutover + nightly interpreted==native falsifier; F10 cleared.

Operator FLAGs left open: A hermetic admissibility of pinned-toolchain builds · B artifact granularity (per-entry v0; module-grain derived later) · C the C target (rows cheap, runtime realization is the real cost; defer until priced by a displaced cost).

Test plan

Whole hermetic corpus: claim_batch --roster-from-discovery ... → 1837/1837 PASS (554 entry groups) on aarch64 at da71e41d0
Every audit claim executed against the live tree with a calibration control (bogus-field-name hard error) — probe sources in the audit doc; probes not committed
Docs-only diff; git status clean apart from the untracked local run log

🤖 Generated with Claude Code

…re unenforced Investigation (no source changes) into whether v2's memory management is "perfectly understood/controlled" ahead of the Realization switch. Every claim is green-by-execution or refuted-by-execution against da71e41, with a calibration control. Headline (F1, corpus-wide, NOT memory-specific): record-literal field PRESENCE and field TYPES are unchecked. `gunbc compile --target dag` (the compile-clean gate's own path) reports `0 diagnostics` for a CacheProvider with `eviction` omitted, for `eviction: 42`, for CostAccount missing 3 of 4 fields, and for DependencyView missing 3 of 4 with `kind: 999`. Calibration: a bogus field NAME hard-errors, so the typechecker runs -- it checks names only. Therefore materialization_ladder.dag:28's "CacheProvider cannot be written without an EvictionClass" is false by execution, and every "by construction, it's a required field" claim in the corpus rests on an unenforced property (DESIGN section 5, correctness-by-construction). Memory findings: - F2 (keystone): RealizationMeasureEffect has ONE variant, ObserveElapsedAtSubject. v2 has no effect that observes space, so CostAccount.space can never be Measured. - F7: FLAG D assigns memory-packing to `realize` over "per-node MEASURED peak RSS" (min(width, budget/peak); section 6-1 names the exit-137 failure mode). F2 makes that input unproducible -- `realize` is unbuildable as designed. - F6: of run = realize . materialize . dependency_view, `realize` and `dependency_view` have 0 definitions; materialize is analysis-only. spine.dag does not import v2.std.dependency; DependencyView is flat (no frames). - F4: space has no seq/par algebra; fleet_intent.dag:168 SUMS space over a sequential rollup (peak is max, not sum) and a witness asserts the sum. - F5: `eviction` has no reader; inverting every eviction class leaves 24/24 green. - F10 (ordering): claim_executor evaluates every v2 witness on the v1 tree-walker, so the only realized eviction is two hand-written v1 Rust mechanisms the ladder does not dispatch. Deleting v1 zeroes realized eviction while declared eviction stays green. Receipt: whole hermetic corpus green on a Raspberry Pi 3 (1837/1837 PASS, 554 entry groups) at VmSize 6.25 GB / 6.0 GB swapped, ~8.4 MB per entry, never released; 13 GB swap to finish. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…rutch Companion to the memory-control audit. Anchor scenario (operator): emit witnesses to native code and schedule the runs with realization. Splits the "v1 crutch" into the execution crutch (every v2 witness evaluates on the v1 tree-walker) and the compiler crutch (self-hosting, separate lane); this plan removes the first without waiting for the second — the seed emitter is part of the artifact KEY, not the architecture. P0 field wall (audit F1, staged ledger->drain->wall) -> P1 space observable (ObservePeakResidentAtSubject; host physics already in claim_batch, unmodeled; space seq=max/par=add) -> P2 content-addressed artifact store (first real CacheProvider; first READER of eviction; ExistenceKeyed unwritable by shape) -> P3 emit-on-demand v0 (wrap emit_host with the store; ROADMAP's own a/b/c) -> P4 realize v0 (min(width, budget/measured_peak); CostUnknown -> width-1 maturation reserve; governor dissolve-on fires; ACCEPT = whole corpus on this 905MB Pi with flat VmSwap) -> P5 demands derived from dependency_view (materialize Share drives real reuse) -> P6 cutover + interpreted==native falsifier; F10 ordering constraint cleared. FLAGs for operator: A hermetic admissibility of pinned-toolchain builds; B artifact granularity (per-entry v0, module-grain derived later); C the C target (rows are cheap, the runtime realization is not; defer until a displaced cost names it). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

cursor · 2026-07-15T04:05:42Z

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.

…#6654's restored wall) Reviewing gunbc#6654 in this branch's context proved its restored never-skip tooth by execution: doc_graph_has_no_orphan_docs ran RED here — the two plan docs this branch adds were a mutually-linked island unreachable from any root, exactly the class #6654's correction note describes (its own doc merged orphaned the same way under the false SubstrateInputsOnly stamp). Fix per #6654's staging precedent: one bind row in the most-related carrier — ci_floor_plan.dag, whose adaptive-width note's dissolve-on ("CostAccount.space measured replaces the reactive estimator") is precisely what the plan's P4 lands. The row reaches witness-realization-plan.md, which links the audit, so both docs are reachable from one bind. Receipts: doc_graph_has_no_orphan_docs false->true, doc_graph_has_no_dangling_links true, entry compile of the edited module 0 diagnostics. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

- Amendment 1: the 'evidence carried by construction' claim is gated on the record-field wall (witness-realization P0 / #6663 audit F1) — the typechecker checks field NAMES only (refuted-by-execution: Known omitting evidence compiles at 0 diagnostics); P0 named a Phase-1 acceptance precondition. Asymmetry recorded: the no-kind wall rests on field-name checking, which DOES hard-error — it holds today; evidence-required does not. - Amendment 2: Phase 2 claims the DerivedFrom fill of CostAccount.space only; the AIMD governor's dissolve-on additionally requires MeasuredBy per-runnable peaks (witness-realization P1) — derived operand footprint and measured peak are different space facts (receipt: 6.25GB VmSize vs KB operands — retention, not operands; the v1 run-stability axis). - Cross-refs: P4 composition note in the supersession paragraph; P1 named third party to the Quantified/CostBasis convergence (one carrier, not three; realization_measurement.dag merge-order flagged); Energy/Watt divergence deduped with audit F3 (owner TBD). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…eck + kernel-vs-declared type tier in infer_record_lit and direct call args .dag authority edits only (generated .rs regen follows in the landing commit): - v1.std.core: MissingField { field, type_name, span } variant + span/message arms (auto-hard via the _ catch-alls in the blocking classifiers) - v1.compiler.infer: presence check in infer_record_lit — every declared field that is not CardOptional and carries no default must appear in the literal; missing -> MissingField at the literal's name_span, gated on a resolvable authority (tn_str nonempty, struct_fields nonempty) - v1.compiler.infer: kernel_value_declared_type_mismatch — a kernel-typed value (Int/String/Bool/Float/...) against a differently-named declared formal fires TypeMismatch unless dag_can_cast sanctions it; wired into BOTH the record-field arm (after the existing string-for-optional-coproduct reject, preserved byte-identical) and direct_call_arg_type_mismatch (calls get the same tier) Receipts: audit probes B/C/D classes (omitted eviction / eviction:42 / kernel-vs- nominal) — RED verification lands with the rebuilt binary; regen on the pre-merge base was surgical (95 written, 2 changed: v1_compiler_infer.rs +159, v1_std_core.rs +21). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…ebuild)

…uite Narrowings found by the closure-scoped ledger (56 -> 0 on the ladder closure): - presence trusts only real field authorities: record_lit_instantiated_fields (generic + annotation), direct non-generic Conj decl children, or the variant-owner path; the record_lit_alias_struct_fields fallback leaked a generic alias's TYPE ARGUMENTS as "fields" (52/56 of the first ledger: every Measure alias literal) - aliases now abstain - kernel tier unwraps where-refinements to their base before comparing (type NonEmptyStr = String where non_empty parses as an anonymous Conj with one child + type_annotation; String literals legitimately inhabit it, 4/56) and excludes equal structural-carrier templates (brands) Receipts (rebuilt binary, by execution): - complete CacheProvider literal: 0 diagnostics - eviction omitted: exactly 1 MissingField naming field + type - eviction: 42: exactly 1 TypeMismatch (Coproduct(EvictionClass) vs Primitive(Int)) - CostAccount<Int> missing 3/4: exactly 3 MissingField (generic instantiation path) - DependencyView kind:999: TypeMismatch + 3 MissingField - call args get the same tier: wants(e: 9) where e: Ev refuses - diagnostics_witness record_field_walls suite: 5 REDs + 3 GREENs (optional-field omission, dag_can_cast Int->Float, complete literal), exit 0 New suite registered in the diagnostics witness bin + transport row + claim test fn (diagnostics_record_field_walls_hold). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Round-1 whole-tree ledger: 568. Three classes root-caused and dissolved: - none-sentinel: `none` into optional coproduct fields infers as Unit (462/568). Unit excluded from the kernel tier - the Value::Null/Absent grounding is its own open thread (DESIGN model-realization fork note); firing there would be an error arm where grounding is owed. - refinement-decl misclassification: `type X = String where p` decls read as records by the final arm when the call path's substitution strips the annotation; excluded via refinement-over-actual shape test. - homonym variants: flat lookup_type_by_name resolved openai's FunctionCall TYPE for github/expressions' FunctionCall VARIANT literals; presence now consults variant_owner_node first - the same disambiguator that stamps parent_enum, so presence agrees with what the literal BECOMES. Round-2 residue: 45 counted rows (roster: .forensics/p0_drain_roster.txt, local), awaiting drain + three operator rulings: 1. `discriminant(v: X {})` empty-literal tag-reference idiom (16+ sites, src/v2/std/compilers/target_model.dag) - sanction zero-field literals as tag references, or mint a first-class variant-tag carrier? 2. String literal into a Secret field (filesystem_write_closure_scale_witness) - fix the test, or is a String->Secret construction sanctioned anywhere? 3. `Coproduct(FreeMonoid)` vs String (01_tokenize) - if String grounds FreeMonoid<Char>, the escape is a dag_cast_rules row, not a source edit. Genuine partial-literal TPs confirmed: RunnableDiscoveryBatch witnesses omit exclude_substrings + discovery_scope_dirs (eval null-fills today); plus MarkdownSpellings/OrderingComparison/EqualityComparison/etc. rows. Probes and the record_field_walls suite stay green through all three fixes. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

The rulings block the final ~25-row drain; recorded with sites, options, and recommendations so the lane is resumable from the doc alone. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

briansrls · 2026-07-15T17:25:19Z

Session handoff — resume context (lively-heron-614, 2026-07-15)

This PR grew beyond its original docs-only scope: it now carries P0 of the witness-realization plan, implemented and 92% drained. Everything needed to resume from any machine is below.

Branch state (`session/lively-heron-614`, pushed through `5e8cd86eb`)

commit	what
`711b5ae8d`	v2 memory-control audit (F1–F10)
`1b199dc3d`	witness-realization plan P0–P6
`44b596cdd`	doc-graph bind row (de-orphan; caught by #6654's restored wall)
`6968b7421`	P0 wall, authority half: `MissingField` diagnostic + presence check + kernel-vs-declared type tier in `src/v1/04_infer.dag` / `00_core.dag`
`af0f3fb91`	merge of origin/main (`00aa9ae2e`)
`513a7b968`	FP narrowings (alias/type-arg leak; refinement carriers; brand templates) + regen sync + `record_field_walls` witness suite (5 REDs, 3 GREENs)
`b13be208c`	whole-tree ledger 568 → 45; three FP classes dissolved by root cause
`5e8cd86eb`	P0 status + the three open rulings recorded in the plan doc

What is proven, by execution

CacheProvider without eviction → exactly 1 MissingField; eviction: 42 → exactly 1 TypeMismatch (Coproduct(EvictionClass) vs Primitive(Int)); CostAccount<Int> missing 3/4 → 3 MissingField (generic instantiation path); DependencyView kind: 999 → TypeMismatch + 3 MissingField; call args covered (wants(e: 9) refuses); complete/optional/defaulted/cast-sanctioned literals stay green.
diagnostics_witness record_field_walls → exit 0 (suite registered in the bin + dag/tools/diagnostics_witness_transport.dag + dag/test/claim/diagnostics_test.dag).
Whole-tree self-compile residue: 45 rows (was 568). Reproduce the roster: gunbc compile --source-root dag --source-root src/v2 --output-dir /tmp/wt --target dag (≈35 min on the Pi 3; grep missing required|type mismatch).

BLOCKED: three operator rulings (full text in `docs/plans/witness-realization-plan.md` §P0 STATUS)

discriminant(v: X {}) empty-literal tag idiom (16+ sites, target_model.dag) — sanction zero-field literals as tag references (recommended, with dissolve-on) or mint a variant-tag carrier.
String literal into a Secret field (filesystem_write_closure_scale_witness.dag:302) — fix the test (recommended; name the sanctioned constructor) vs a cast row (gutting Secret).
String vs Coproduct(FreeMonoid) (01_tokenize.dag:2875) — if String grounds FreeMonoid<Char>, one dag_cast_rules row; else fix the site. Operator modeling call.

After the rulings: drain ~25 mechanical rows (partial literals listed in the doc; plus one probable real bug — Bool into a FreeMonoid container, card_intake.dag:5890), re-run the whole-tree ledger to 0, land.

Working mechanics (hard-won; also in project memory)

Compiler-change loop: edit src/v1/*.dag → ./target/debug/regen_stage0 (~8–9 min; it is also the first typecheck of your edit) → cargo build --bin gunbc --bin claim_batch --bin diagnostics_witness -j1 (~29 min on the Pi). Commit .dag + regenerated .rs together.
Grammar traps: no newline after let x = (cascade of phantom cross-module errors — read the FIRST error); check the whole v1.std.core import block before adding an import (E0252).
Pi discipline: never -j2 (two watchdog hard-resets on 2026-07-15 — swap livelock, journal empty-tailed); -j1 nice ionice is safe. cgroup memory fencing is impossible until cgroup_disable=memory is removed from /boot/firmware/cmdline.txt (+ reboot). Exit codes through | tail lie — capture ${PIPESTATUS[0]} and verify artifacts (binary mtime).
Ledger method: entry-scoped gunbc compile --entry <probe>.dag --target dag prints a closure's hard diagnostics in seconds — triage FP classes per-closure before paying whole-tree runs.

Queue after P0

P1 (task queued): ObservePeakResidentAtSubject second variant on RealizationMeasureEffect; peak-RSS into PerformanceReceipt (host physics already in claim_batch's getrusage — mark-on-carrier); space_measure_seq=max / space_measure_par=add; fix the fleet_intent.dag:168 sum + flip the keystone witness. One regen+rebuild cycle.
Related lanes: docs/plans: machine-shape orthogonal scheduling — end shape, no-kind rule, convergence map #6654 (machine-shape; two amendments pending — F1 precondition now largely DISCHARGED by this P0, worth noting there), v1 resolve: collapse redundant per-module ancestry_str_bindings recompute to Rc-borrow #6660 (superlinearity; implementer notes + baseline posted; standing offer to re-fit the exponent on this Pi post-merge).

PR admin

This PR's original body describes docs only. Either update the body to cover P0 or split P0 into its own PR — operator's call; the branch is coherent either way (docs → plan → implementation of the plan's first step).

🤖 Generated with Claude Code

…rule, convergence map (#6654) * WIP: map reduce * WIP: map reduce * WIP: map reduce * WIP: map reduce * machine-shape plan: end shape agreed, no-kind rule, convergence map to existing carriers - §2 terminal model pinned (operator rulings 2026-07-15): one locality lattice (lifted to std, converging BOTH existing latency enums), divergence/idle-lane/ crossing laws, Placement dissolution trigger, kind-erasure at the ComputeHost→MachineShape derivation boundary - convergence map: every end-shape element bound to its existing carrier (HardwareThreadCount reused for lane_count; PlacementSupplyRow identified as the degenerate single-domain MachineShape; PTX ThreadHierarchyShape/PtxCost gain their consumer; MemoryKind.UnifiedShared flagged as topology-in-technology) - MemoryLevel.sharing dropped: sharing derives from SharedLevelEdge graph structure (single authority) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: map reduce * machine-shape plan: address operator request-changes (7 blocking findings) - MachineShape is now a representable graph: DomainId/LevelId identities, explicit edge endpoints, SharedLevelEdge references the owner's level by id (embedding duplicated it), InterconnectLink coproduct holds NetworkAttach (LinkEdge was PcieLink-only while the map claimed NetworkInterface as a fill), terminal Placement = DomainId reference; dangling refs refuse - Phase 3 batching vs signed scheduling authority: conflict acknowledged, now an EXPLICIT supersession proposal (topology = pure fn of declared shape; MeasuredBy banned from topology; schedule_eq generalized to equal-given-equal- declared-inputs) gated on operator sign-off, with a confined fallback - both §5 fallback arms converted to refusals: Priced|PricingRefused{missing} (no term-incomplete Predicted accounts), Placed|PlacementRefused{missing} (no stay-at-current-domain answer) - Quantified<T> restructured: Precision (Exact|Interval) x Evidence (Cited|MeasuredBy{ExecutionReceiptDigest}|DerivedFrom) — evidence-bearing constructors make the authored-literal RED enforceable - locality/latency split into two axes: latency = per-level magnitude with one std class projection (converging ReadLatencyClass + network LatencyClass); locality = graph-derived, domain-relative (no universal total order) - OperandFlow total derivation spelled out: operand_root (fail-closed), hash- authority convergence precondition (v2.std.node.Hash vs ContentHash — the fnv1a64 thread), edge->root mapping for node_keyed_graph_transitive_bytes, OperandFlowRefused rows - AssociativityEvidence subject-bound: {combine, inhabitant, law, receipt}, license requires structural identity with the scheduled combine; keyed-patch witness scoped to mechanism-precedent-only; within-fold expansion scoped kernel-internal (never central Schedule topology) - corrections: PlacementSupplyRow has zero production callers (grep -l overcount); document-level dissolution trigger added (Plan-row registration = part of Phase 1 definition of done) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * de-orphan machine-shape plan doc + correct doc_reachability lying live-tree stamp Two fixes from the docs-enforcement audit (operator-directed): 1. bind: provenance row in accelerator_demo_plan.dag makes docs/plans/machine-shape-orthogonal-scheduling.md doc-graph-reachable (the established hand-authored-design-md convention: accelerator_demo_plan :51, live_read_classification.dag:66). Registration as a gunbc.plan.Plan row stays the md's declared Phase-1 dissolution — registering now would flip the actively-evolving doc into a generated artifact prematurely. Verified by build_doc_graph_report replication: doc_count=107, orphan_count 1->0, dangling 0. 2. doc_reachability_witness_test live_tree_disposition: SubstrateInputsOnly -> ReadsLiveTree. The 2026-07-12 machine stamp (#6479 entry-text batch) was false: every test fn reads the live docs/ tree via doc_graph_* host builtins — the exact classifier blind spot live_tree.dag:5 declares. The false stamp made the orphan wall predict-skippable, which composed with the docs-only floor shortcut into a pre-merge false-green (this PR minted an orphan with green CI). ReadsLiveTree restores the never-skip tooth: the wall now runs on every full floor, including this PR's. This diff leaves the docs-only shortcut class, so this PR runs the full floor with the corrected stamp — the wall itself verifies the de-orphan by execution, pre-merge. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * bind main's orphaned no-smuggled-programs-wall.md from its lens carrier The doc merged to main orphaned (docs-only shortcut + then-lying doc_reachability stamp — the same false-green class this PR fixes). With the stamp corrected, the orphan wall's first live pre-merge run (this PR's floor) caught it: 1 of 1880 witnesses red. Bound from medium_structure_containment.dag, the wall the design doc signs — same bind-from-carrier convention as accelerator_demo_plan.dag:51. Verified by build_doc_graph_report replication on the merged tree: doc_count=108, orphan_count 1->0, dangling 0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: map reduce * machine-shape plan: apply #6663 review amendments 1+2 - Amendment 1: the 'evidence carried by construction' claim is gated on the record-field wall (witness-realization P0 / #6663 audit F1) — the typechecker checks field NAMES only (refuted-by-execution: Known omitting evidence compiles at 0 diagnostics); P0 named a Phase-1 acceptance precondition. Asymmetry recorded: the no-kind wall rests on field-name checking, which DOES hard-error — it holds today; evidence-required does not. - Amendment 2: Phase 2 claims the DerivedFrom fill of CostAccount.space only; the AIMD governor's dissolve-on additionally requires MeasuredBy per-runnable peaks (witness-realization P1) — derived operand footprint and measured peak are different space facts (receipt: 6.25GB VmSize vs KB operands — retention, not operands; the v1 run-stability axis). - Cross-refs: P4 composition note in the supersession paragraph; P1 named third party to the Quantified/CostBasis convergence (one carrier, not three; realization_measurement.dag merge-order flagged); Energy/Watt divergence deduped with audit F3 (owner TBD). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: map reduce * heal main's composed drift + re-anchor vacuity design docs (unblocks all full-floor PRs) Main's tree (post #6638/#6664) fails generated_artifact_drift_gate_passes on every full floor: the vacuity lane hand-added a 'Sibling family' paragraph to the GENERATED docs/plans/inert-layer-lens.md without updating its generating Plan row (dag/gunbc/plans/inert_layer_lens.dag) — committed != regenerated. Their docs-only PRs merged through the docs-only shortcut, which skipped both the drift gate and the doc-graph wall. 1. Regenerate inert-layer-lens.md (paragraph removed; byte-identical to warm-crab-65's independent main_wet regen on #6658 — same blob 2b36cf2). 2. That hand-edit was ALSO the only doc-graph anchor for the vacuity lane's two design docs; regen alone orphans vacuity-lens-design.md and (via its link chain) lens-consolidation-design.md. Re-anchored with a bind: provenance row in dag/std/materialization_ladder.dag — the file whose AuthoredDuplication verdict the vacuity doc's load-bearing correction is about — migrating to the vacuity lens .dag carrier when it lands. Verified by build_doc_graph_report replication: doc_count=110, orphan_count=0, dangling=0. Follow-up for the vacuity lane: re-add the sibling-family paragraph via the inert_layer_lens Plan row (the authority), not the generated md. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

# Conflicts: # src/v1/stage0/src/cli_run.rs

gunbai-bot · 2026-07-15T17:39:32Z

Addressed the cursor REQUEST_CHANGES (review 38376) — the finding was correct.

Fix (pushed 50c11865a0): restored crate::v1_compiler_infer_env::empty_symbol_index() as the final argument at both compiler_tests.rs call sites (build_type_env, typecheck_module). Both APIs still require symbol_index: Rc<SymbolIndex> as the last parameter (v1_compiler_infer.rs:12822, :14581), and the emit authority compiler_tests_rust.dag:1170/:1206 still emits it — the .rs had drifted from its authority, so #[cfg(test)] compilation broke with a wrong-argument-count error. Restored to match the authority byte-for-byte (== regen output).

Verified green by execution: cargo test -p v1-compiler --lib --no-run forced recompile → exit 0 (the --bin gunbc build missed it because it skips the test cfg).

Also in this push: merge of origin/main (bc76f2f42c) resolving the one conflict in cli_run.rs — a rename collision where main refactored fast_lane_eval_budget_ms → witness_budget_policy(); took main's calling convention (unrelated to the field-wall feature).

The three P0 modeling rulings remain open (empty-literal tag idiom / String→Secret / String↔FreeMonoid) before the final ~25-row ledger drain.

gunbai-bot · 2026-07-15T17:53:37Z

Re: cursor REQUEST_CHANGES (review 38378) — confirmed correct, on-principle.

Verified against the current tree: the P0 field wall is wired as a hard compile-clean gate (cli_run.rs:1767-1773 fails on every diagnostic except ComplexityUnknown), but the whole-tree corpus is not drained to 0. Current failing set at 50c1186 (dag_compile_clean_gate, --target dag):

~22 rows = the target_model.dag empty-literal tag idiom (AlgebraPrimitive {}, PrefixToken {}, CallIdent {}, …) — gated on open operator Ruling 1 (sanction zero-field coproduct-variant literals as tag references, or mint a tag carrier).
~13 rows = merge-induced (Node.occurrence_id, TargetModel.runtime_row) — main's Dissolve the docs-only CI floor shortcut per its named dissolve-on: replace path-prefix skip (ci_spec.dag:344-465, ci.yml:180-199) with affected-set-scoped compile-clean (Ruling 1 path grain). Context: the shortcut's skip class (docs-only diffs) exactly shadows the doc_reachability orphan wall's sub #6658 rewrote ci_floor_plan.dag after the author's last drain; occurrence_id is genuinely required, so these are real (mechanical) drain rows.

Merging the hard wall on an undrained corpus violates §5 (the line must stay green / deficits cleared before restart) and the plan's own P0 ACCEPT ("corpus green after drain"). Not merging it that way. Disposition is with the operator: either (b) put the wall in ledger-only mode (counted + located, non-gating on the whole-tree compile) until corpus-green is achievable — the plan's stage (ii) — or (c) split the P0 implementation into a follow-up PR and land this as the audit + witness-realization-plan docs. Holding for that call rather than force a drain past the open ruling.

(claude review 38377 APPROVE noted — the wall's design, witness suite, and diagnostic authority are sound; the objection is purely the premature hard-gate on an undrained corpus.)

- R5 compute_fabric relationship: Shape IS the degenerate one-axis MachineShape; market stays thin (no #5904 rebuild); Fabric = outermost rung of the recursive supply tower. Convergence-map row added. - R6 evidence carriers: staged convergence (Quantified for greenfield, P1 receipts reuse Evidence.MeasuredBy, CostBasis migrates on forced join); owner = #6663 lane. - R7 Energy: derived quantity (Power x Time), lands Phase 1, is the F3 dedupe. - R8 scheduling invariant REFINED not superseded (operator: determinism was being conflated with input-invariance — different machines are different inputs). Surviving wall: no UNSTABLE (MeasuredBy) inputs to topology; declared shape is a stable input; cross-host schedule_eq demoted to corollary under equal declared shapes. Phase 3 UNBLOCKED. Open list rewritten: law-carrier home, SymbolIndex sequencing, hash convergence (dispatched), P0 field wall (#6663) remain. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

gunbai-bot · 2026-07-15T19:16:50Z

P0 drain complete — Path A landed (operator, 2026-07-15).

The whole-tree ledger is now 0 (was 45) and the ci_floor_plan compile-clean closure is 0 (was 22 target_model + 12 occurrence_id + 1 runtime_row). Verified green-by-execution on a fresh regen+rebuild:

gunbc compile --source-root dag --source-root src/v2 --target dag → 0 diagnostics
gunbc compile --entry src/v2/workflow/ci_floor_plan.dag … → 0 diagnostics
diagnostics_witness record_field_walls → exit 0 (RED/GREEN discrimination intact)
cargo fmt --all --check → clean

How the 45+12 drained, by operator ruling:

Ruling 1(a) — zero-field coproduct-variant literals sanctioned as tag references (is_zero_field_variant_tag_reference, carrier-marked zero_field_variant_tag_reference_frontier_note with dissolve-on = variant-tag carrier). Drains the 22 target_model.dag discriminant(v: X {}) sites. Partial literals stay red.
Ruling 3 — Int→Nat + String→FreeMonoid dag_cast_rules rows (grounded identities: Numeric-tower grounding: ground Nat construction-side so native form == modeled form (§0) #5428 numeric tower, String = FreeMonoid<Char>; documented grounded_primitive_coproduct_cast_note). Drains 8 rows; non-grounded straddles stay red.
Ruling 2(a) — cap: "" as Secret (the sanctioned nominal_opaque cast idiom).
Mechanical schema fill: occurrence_id: SyntheticOccurrence ×12, RunnableDiscoveryBatch fields ×6, thematic_break ×2, runtime_row ×1.
Two genuine bugs the wall correctly surfaced: String "Bearer"→AuthScheme.Bearer variant (auth), and a for-comprehension (flat-map) scalar-Bool body → map (card_intake).

Re: the drift review (38396) — resolved. The Ruling-1a .dag logic is now emitted into v1_compiler_infer.rs (regen, 95 files). Also fixed a named-arg-reorder false-positive the drain surfaced in the wall itself: direct_call_arg_mismatch_diags paired formals/actuals positionally, so a reordered named-arg call (emit_sudo_wrapped_script_body(marker:…, inner:…)) mis-flagged inner:Doc against the marker String — now matched by name. That was the 2 live_deploy/emit.dag Doc rows (call sites were correct).

…t regression Placing Int→Nat / String→FreeMonoid in dag_cast_rules made Nat and String into cast-DOMAIN types (is_dag_cast_domain_type), which newly triggered `as`-cast validation of pre-existing well-typed casts whose reverse rule is absent — `Nat as Int` (bmc_onboard), `Int as String` (srv3_os_install, host_effect_realize) — reddening the floor compile-clean gate. Those casts were skipped before because their far type was not a domain type. Move the two grounded identities into their own list that dag_can_cast consults (so kernel_value_declared_type_mismatch still stops flagging an Int where a Nat / a String where a FreeMonoid is expected), while is_dag_cast_domain_type continues reading only dag_cast_rules — so the explicit-`as`-cast validation domain is unchanged. Verified: the CI gate's own closure (floor_effect_gate_witness.dag) now compiles clean, whole-tree ledger stays 0, record_field_walls witnesses green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

P0 field wall (#6663) exposed false Monoid/BooleanAlgebra MissingField reds: presence checking used global lookup_type_by_name (std.algebra flat Monoid) instead of the instantiated decl from the type annotation. Use type_node_label for applied-type matching, decl.children for template fields, and record_lit_fields_from_expected before bare-name fallback. Co-authored-by: Cursor <cursoragent@cursor.com>

The #6663 record-field wall enforces std.algebra's flat carrier shapes; v2 modules still used nested v2.std.algebra literals (semigroup/magma/ring). Route carriers through std.algebra and update dependent field access. Co-authored-by: Cursor <cursoragent@cursor.com>

…ebra (#6696) * Consolidate markdown helpers onto gunbc.plans.md_helpers (§3). Remove duplicate h2/p/li/ul/cell/row declarations from ci_oom_reclassification, wiring_liveness_preflight, and design_document; import the shared authority instead. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix CI: flatten v2 algebra literals for P0 field-wall compliance. The #6663 record-field wall enforces std.algebra's flat carrier shapes; v2 modules still used nested v2.std.algebra literals (semigroup/magma/ring). Route carriers through std.algebra and update dependent field access. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com>

Composer review flagged 04_infer/v1_compiler_infer.rs as out of scope for this PR (#6663 field-wall belongs in session/infer-record-lit-field-authority). Restores both files to origin/main and fixes the cargo fmt build gate. Co-authored-by: Cursor <cursoragent@cursor.com>

…main-red root fix) + fmt-immune crate-layout emitter (#6701) * Unbreak main: revert #6686's v2 hash-grounding surface (cross-root import x #6663 field wall) Partial revert of 4a60303: src/v2/std/node.dag, materialize.dag, materialize_witness_test.dag, inert_carrier.dag, and the DESIGN Sec-3-thread note pair (carrier + generated doc together). Keeps #6686's orthogonal cli_run.rs nfr-roster backfill (reverting it would re-red the falsifier lane). Root cause (proven by execution): #6663's new MissingField presence check resolves a literal's expected type by unqualified name through the flat module type env; #6686's 'import std.types { ContentHash }' in v2.std.node pulls dag-root std.algebra into the typecheck closure of every v2 module importing v2.std.node (704 files), so dag-root Monoid/Semigroup/BooleanAlgebra/ OrderedRing/CommutativeMonoid/CommutativeSemiring/AbelianGroup shadow the v2.std.algebra declarations at 28 literal sites in src/v2/std/{diagnostic,logic,nat,integer}.dag -> ci_floor_plan resolve fails -> every main push red. Neither PR alone was red: zero file overlap, merged 31 minutes apart, and the squash union tree was never CI'd (the PR's only CI run began 8 minutes before #6686 landed). Receipt: on the 60286e0 tree with the same seed binary, reverting exactly this .dag surface takes the plan resolve from 28 missing-required-field errors to green with the floor executing witnesses (control: #6678/#6685 left in tree). Re-land trigger (dissolution): the wall's presence leg consults the resolver's binding (or fails closed on ambiguous names) instead of the flat-env name lookup; the follow-up re-lands these files with that fix, using this exact 28-error tree as the RED control. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Keep #6686's LocalAlias inert-carrier roster line (orthogonal to the poisoning surface) The floor's inert_carrier_no_unrostered_or_stale witness reds without it: the LocalAlias fixture it rosters landed in #6641, not #6686 — the roster line was a bundled orthogonal fix (same class as the kept cli_run.rs backfill), not part of the hash-grounding surface. Receipt: local floor on the revert tree, 300 PASS / 1 FAIL (this witness), FAIL clears with the line restored. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: field-wall env precedence fix (scratch) * WIP2: kernel/container guard + final regen * Fix generated_artifact_drift_gate: make the crate-layout emitter fmt-immune (rustfmt::skip) Batch-4 generated_artifact_drift_gate_passes red on this PR is the first run of that gate since main broke at 60286e0 -- #6677 landed its derived crate-layout artifact during the red window, so no tree ever executed batch 4 against it. Two writers disagreed on one artifact: the wet leg (stage0_crate_layout_emit.dag) emits plain multi-line arrays, while the committed bytes were rustfmt'd (trailing comma, collapsed one-liner). Committed bytes: fmt-clean, drift-red; emitter bytes: drift-clean, fmt-red -- no tree could satisfy both gates. Fix: the emitter stamps #[rustfmt::skip] on both consts, so its output is the fixed point of cargo fmt; artifact regenerated via main_wet. Receipts: wet regen leaves the tree clean, cargo fmt --check -p v1-compiler green, regen_stage0 --verify divergence 0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

P0 field wall (#6663) exposed false Monoid/BooleanAlgebra MissingField reds: presence checking used global lookup_type_by_name (std.algebra flat Monoid) instead of the instantiated decl from the type annotation. Use type_node_label for applied-type matching, decl.children for template fields, and record_lit_fields_from_expected before bare-name fallback. Co-authored-by: Cursor <cursoragent@cursor.com>

…main-red) (#6709) * P0 field wall: stand down on census-ambiguous bare type names (fixes main-red since 60286e0) Main has been red for every PR since #6663 merged: whole-tree resolve of ci_floor_plan refuses with 'missing required field' across src/v2/std/{diagnostic,logic,nat,integer}.dag. The literals are correct — they inhabit v2.std.algebra's NESTED shapes (Monoid { semigroup, identity }). The new presence check resolves its field template by bare name through the overlay-wins binding pool, where dag/std/algebra's FLAT shapes (Monoid { op, identity }) win the ledgered fork, so correct v2 literals were enforced against the wrong layer's fields. Enforcing the overlay winner of a known binding fork is a guess (§5) — the wall now stands down exactly where the corpus-wide bare-name census says the name is ambiguous (GlobalBareAmbiguousBinding, order-independent), and stays live for census-unique names. Marked with a dissolve-on: the namespace lane's containment SymbolIndex makes expected types scope-resolved, after which the gate is dead code and the wall goes total. Also: record_lit_instantiated_fields now takes its field template from the SAME decl that supplies the generic substitution (decl.children) instead of a second name-keyed lookup — params from one decl and fields from another was incoherent independent of the collision. Proof by execution (scratch build from origin/main): - repro: claim_executor resolve of ci_floor_plan reproduced the exact CI signature pre-fix; post-fix 0 missing-required-field errors and the executor proceeds into the batch walk. - RED control: diagnostics_witness record_field_walls (the #6663 wall's own presence cases, census-unique types) still passes — the wall still refuses genuinely missing fields. - regen_stage0 --verify: regen_divergence_count=0 (emitted seed is the fixed point of the edited authority). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * gate note: record the accepted counted-ledger ratchet (also bumps sccache keys past a poisoned zero-byte probe_bin cache entry) The drift-gate red on this PR's CI is a cached sccache truncation: the first run's zero-byte probe_bin artifact was cached, so reruns replay it (identical failure twice, refused fail-closed by build verification both times; regen_stage0 --verify is divergence-0 locally on this exact tree). Extending the on-carrier note with the review-accepted ratchet is a real content change to the emitted constant, which re-keys the compilation unit. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

* WIP: Triage the non-markup ambiguous names: §3 fork (consolidate) vs genuine * Land tier-2 namespace homonym triage for emit, extdeps anchor, and live_tree. Records typed verdict rows so Wave-0 (c) can skip construction-protocol stamps and only qualify genuine cross-subtree homonyms. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Triage the non-markup ambiguous names: §3 fork (consolidate) vs genuine * Address review nits and revert accidental infer.rs drift. Restore v1_compiler_infer.rs to main (fixes CI lookup_func_sig arity break from an accidental WIP commit), alpha-order the census test mod in lib.rs, and document the census probes as diagnostic-only instruments. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Triage the non-markup ambiguous names: §3 fork (consolidate) vs genuine * WIP: Triage the non-markup ambiguous names: §3 fork (consolidate) vs genuine * Revert out-of-scope infer record-literal edits; fmt census test. Composer review correctly flagged 04_infer/v1_compiler_infer.rs changes as unrelated to tier-2 triage — restore both to origin/main. Keep only the plan carrier, diagnostic census probe, and lib.rs registration. Co-authored-by: Cursor <cursoragent@cursor.com> * Wire census probe into seed-retained scaffold discipline. Add dissolve-on bind in the test module header and name the probe on the tier-2 plan carrier (path + note row; dissolve trigger names deletion). Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Triage the non-markup ambiguous names: §3 fork (consolidate) vs genuine * Drop re-landed infer edits; keep tier-2 triage scope only. Composer review flagged 04_infer/v1_compiler_infer.rs as out of scope for this PR (#6663 field-wall belongs in session/infer-record-lit-field-authority). Restores both files to origin/main and fixes the cargo fmt build gate. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Triage the non-markup ambiguous names: §3 fork (consolidate) vs genuine * WIP: Triage the non-markup ambiguous names: §3 fork (consolidate) vs genuine * Fix tier-2 invariant gate: absent census is not ambiguous. Construction-protocol names may be absent from the global bare census (entry-grain stamps are not export bindings). Gate only refuses GlobalBareAmbiguousBinding plus zero AmbiguousBare reachability sites. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Cursor <cursoragent@cursor.com>

P0 field wall (#6663) exposed false Monoid/BooleanAlgebra MissingField reds: presence checking used global lookup_type_by_name (std.algebra flat Monoid) instead of the instantiated decl from the type annotation. Use type_node_label for applied-type matching, decl.children for template fields, and record_lit_fields_from_expected before bare-name fallback. Co-authored-by: Cursor <cursoragent@cursor.com>

…ipline (#6698) * Unbreak main: revert #6686's v2 hash-grounding surface (cross-root import x #6663 field wall) Partial revert of 4a60303: src/v2/std/node.dag, materialize.dag, materialize_witness_test.dag, inert_carrier.dag, and the DESIGN Sec-3-thread note pair (carrier + generated doc together). Keeps #6686's orthogonal cli_run.rs nfr-roster backfill (reverting it would re-red the falsifier lane). Root cause (proven by execution): #6663's new MissingField presence check resolves a literal's expected type by unqualified name through the flat module type env; #6686's 'import std.types { ContentHash }' in v2.std.node pulls dag-root std.algebra into the typecheck closure of every v2 module importing v2.std.node (704 files), so dag-root Monoid/Semigroup/BooleanAlgebra/ OrderedRing/CommutativeMonoid/CommutativeSemiring/AbelianGroup shadow the v2.std.algebra declarations at 28 literal sites in src/v2/std/{diagnostic,logic,nat,integer}.dag -> ci_floor_plan resolve fails -> every main push red. Neither PR alone was red: zero file overlap, merged 31 minutes apart, and the squash union tree was never CI'd (the PR's only CI run began 8 minutes before #6686 landed). Receipt: on the 60286e0 tree with the same seed binary, reverting exactly this .dag surface takes the plan resolve from 28 missing-required-field errors to green with the floor executing witnesses (control: #6678/#6685 left in tree). Re-land trigger (dissolution): the wall's presence leg consults the resolver's binding (or fails closed on ambiguous names) instead of the flat-env name lookup; the follow-up re-lands these files with that fix, using this exact 28-error tree as the RED control. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Keep #6686's LocalAlias inert-carrier roster line (orthogonal to the poisoning surface) The floor's inert_carrier_no_unrostered_or_stale witness reds without it: the LocalAlias fixture it rosters landed in #6641, not #6686 — the roster line was a bundled orthogonal fix (same class as the kept cli_run.rs backfill), not part of the hash-grounding surface. Receipt: local floor on the revert tree, 300 PASS / 1 FAIL (this witness), FAIL clears with the line restored. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: field-wall env precedence fix (scratch) * WIP2: kernel/container guard + final regen * Fix generated_artifact_drift_gate: make the crate-layout emitter fmt-immune (rustfmt::skip) Batch-4 generated_artifact_drift_gate_passes red on this PR is the first run of that gate since main broke at 60286e0 -- #6677 landed its derived crate-layout artifact during the red window, so no tree ever executed batch 4 against it. Two writers disagreed on one artifact: the wet leg (stage0_crate_layout_emit.dag) emits plain multi-line arrays, while the committed bytes were rustfmt'd (trailing comma, collapsed one-liner). Committed bytes: fmt-clean, drift-red; emitter bytes: drift-clean, fmt-red -- no tree could satisfy both gates. Fix: the emitter stamps #[rustfmt::skip] on both consts, so its output is the fixed point of cargo fmt; artifact regenerated via main_wet. Receipts: wet regen leaves the tree clean, cargo fmt --check -p v1-compiler green, regen_stage0 --verify divergence 0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * MachineShape construction wall: compile gate + witnesses only. Rebuilt from origin/main per operator recovery: three-file scope only (lens, compile enrollment, claim witnesses). Stacked on #6687 for std.machine_shape / extdeps.gpu.machine_shape subjects — no Phase 1 content copied. Removed unused std.algebra import that poisoned CI resolve. Co-authored-by: Cursor <cursoragent@cursor.com> * machine_shape gate: fail-closed Cons/Empty match (determinism precedent) Replace is_empty + list_head/HeadAbsent absorb arm with Cons/Empty fold match — HeadAbsent silently accepted on invariant violation (§5). Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Fable 5 <noreply@anthropic.com> Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Cursor <cursoragent@cursor.com>

…haustive theorem gunbc.merge_lifecycle (new): lifecycle dynamics over the existing gunbc.merge_admission authority — the merge step consumes policy_admits, never restates it. Squash lands the PR onto CURRENT main (squash_result_tree); receipts mint through mint_merge_admission_receipt; latest-receipt-per-PR matches GitHub required-check semantics; the unverified-tip latch fires only where main advances. test.claim.merge_lifecycle_interleaving_witness (new, floor-discovered): the 2026-07-16 #6663 x #6686 main-red as the permanent RED fixture (admitted under the live PerPrGateOnly policy, refused under KeyedReceipt, remedy path lands verified), plus bounded-exhaustive enumeration of all 625 length-4 event interleavings: KeyedReceipt admits zero unverified tips; PerPrGateOnly admits violations (enumerator-teeth control); RequireUpToDateBase (GitHub's strict boolean) still misses the roster axis. Quantifies gunbc.plans.branch_merge_admission_model section 4 over every interleaving instead of two authored scenarios. Additive checkpoint-1 extension: no enforcement flip (merge_freshness_gating_status stays GatingComputedDeferred), no settings change, no seed .rs touched. All 7 claims green by execution via gunbc run --claim-run; whole-tree compile-clean 0 diagnostics. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

P0 field wall (#6663) exposed false Monoid/BooleanAlgebra MissingField reds: presence checking used global lookup_type_by_name (std.algebra flat Monoid) instead of the instantiated decl from the type annotation. Use type_node_label for applied-type matching, decl.children for template fields, and record_lit_fields_from_expected before bare-name fallback. Co-authored-by: Cursor <cursoragent@cursor.com>

…haustive theorem (#6725) * Unbreak main: revert #6686's v2 hash-grounding surface (cross-root import x #6663 field wall) Partial revert of 4a60303: src/v2/std/node.dag, materialize.dag, materialize_witness_test.dag, inert_carrier.dag, and the DESIGN Sec-3-thread note pair (carrier + generated doc together). Keeps #6686's orthogonal cli_run.rs nfr-roster backfill (reverting it would re-red the falsifier lane). Root cause (proven by execution): #6663's new MissingField presence check resolves a literal's expected type by unqualified name through the flat module type env; #6686's 'import std.types { ContentHash }' in v2.std.node pulls dag-root std.algebra into the typecheck closure of every v2 module importing v2.std.node (704 files), so dag-root Monoid/Semigroup/BooleanAlgebra/ OrderedRing/CommutativeMonoid/CommutativeSemiring/AbelianGroup shadow the v2.std.algebra declarations at 28 literal sites in src/v2/std/{diagnostic,logic,nat,integer}.dag -> ci_floor_plan resolve fails -> every main push red. Neither PR alone was red: zero file overlap, merged 31 minutes apart, and the squash union tree was never CI'd (the PR's only CI run began 8 minutes before #6686 landed). Receipt: on the 60286e0 tree with the same seed binary, reverting exactly this .dag surface takes the plan resolve from 28 missing-required-field errors to green with the floor executing witnesses (control: #6678/#6685 left in tree). Re-land trigger (dissolution): the wall's presence leg consults the resolver's binding (or fails closed on ambiguous names) instead of the flat-env name lookup; the follow-up re-lands these files with that fix, using this exact 28-error tree as the RED control. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Keep #6686's LocalAlias inert-carrier roster line (orthogonal to the poisoning surface) The floor's inert_carrier_no_unrostered_or_stale witness reds without it: the LocalAlias fixture it rosters landed in #6641, not #6686 — the roster line was a bundled orthogonal fix (same class as the kept cli_run.rs backfill), not part of the hash-grounding surface. Receipt: local floor on the revert tree, 300 PASS / 1 FAIL (this witness), FAIL clears with the line restored. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: field-wall env precedence fix (scratch) * WIP2: kernel/container guard + final regen * Fix generated_artifact_drift_gate: make the crate-layout emitter fmt-immune (rustfmt::skip) Batch-4 generated_artifact_drift_gate_passes red on this PR is the first run of that gate since main broke at 60286e0 -- #6677 landed its derived crate-layout artifact during the red window, so no tree ever executed batch 4 against it. Two writers disagreed on one artifact: the wet leg (stage0_crate_layout_emit.dag) emits plain multi-line arrays, while the committed bytes were rustfmt'd (trailing comma, collapsed one-liner). Committed bytes: fmt-clean, drift-red; emitter bytes: drift-clean, fmt-red -- no tree could satisfy both gates. Fix: the emitter stamps #[rustfmt::skip] on both consts, so its output is the fixed point of cargo fmt; artifact regenerated via main_wet. Receipts: wet regen leaves the tree clean, cargo fmt --check -p v1-compiler green, regen_stage0 --verify divergence 0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Merge-lifecycle interleaving witness: the squash race as a bounded-exhaustive theorem gunbc.merge_lifecycle (new): lifecycle dynamics over the existing gunbc.merge_admission authority — the merge step consumes policy_admits, never restates it. Squash lands the PR onto CURRENT main (squash_result_tree); receipts mint through mint_merge_admission_receipt; latest-receipt-per-PR matches GitHub required-check semantics; the unverified-tip latch fires only where main advances. test.claim.merge_lifecycle_interleaving_witness (new, floor-discovered): the 2026-07-16 #6663 x #6686 main-red as the permanent RED fixture (admitted under the live PerPrGateOnly policy, refused under KeyedReceipt, remedy path lands verified), plus bounded-exhaustive enumeration of all 625 length-4 event interleavings: KeyedReceipt admits zero unverified tips; PerPrGateOnly admits violations (enumerator-teeth control); RequireUpToDateBase (GitHub's strict boolean) still misses the roster axis. Quantifies gunbc.plans.branch_merge_admission_model section 4 over every interleaving instead of two authored scenarios. Additive checkpoint-1 extension: no enforcement flip (merge_freshness_gating_status stays GatingComputedDeferred), no settings change, no seed .rs touched. All 7 claims green by execution via gunbc run --claim-run; whole-tree compile-clean 0 diagnostics. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Wire the merge queue: merge_group trigger, typed end to end extdeps.github.actions gains the MergeGroup WorkflowTrigger variant (cited; nullary — checks_requested is the only documented activity and GitHub's default, so a one-inhabitant types parameter carries no information per the phantom-parameter collapse ruling). The yaml serializer answers it; gunbc.ci_workflow enrolls it in the ci on: list; ci.yml regenerated via generated_artifact_gate main_wet — the artifact diff is exactly one line (merge_group:). Queue runs are already absorbed by the existing seams, noted on the carrier: deploy's main-push guard skips them, the concurrency group falls through pull_request.number to run_id, the merge-admission stamp takes its non-PR arm, and an unresolvable merge-base diff on a queue ref falls through to the full floor (fail-closed, never widening). The trigger is inert until the operator adds the merge_queue rule to the main ruleset (Rulesets write needs the admin grant this integration lacks). Land this FIRST, flip the rule SECOND — the queue realizes gunbc.merge_admission KeyedReceipt on the tree axis, the policy test.claim.merge_lifecycle_interleaving_witness proves total. Whole-tree compile-clean: 0 diagnostics. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Fable 5 <noreply@anthropic.com>

…ia the existing value-expression path, prove behavioral equivalence to v1 seed (hermetic per-PR + wet oracle), flip frontier row SeedRetained->SelfEmitted. Copy the use_site_verdict pilot template (#6675). v2-only leaf, shim-free. (#6704) * WIP: Wave 2 Band A self-emit: discovery_enumeration — self-emit its Rust via * WIP: Wave 2 Band A self-emit: discovery_enumeration — self-emit its Rust via * Fix record-lit field authority for v2.std.algebra annotated literals. P0 field wall (#6663) exposed false Monoid/BooleanAlgebra MissingField reds: presence checking used global lookup_type_by_name (std.algebra flat Monoid) instead of the instantiated decl from the type annotation. Use type_node_label for applied-type matching, decl.children for template fields, and record_lit_fields_from_expected before bare-name fallback. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Wave 2 Band A self-emit: discovery_enumeration — self-emit its Rust via * WIP: Wave 2 Band A self-emit: discovery_enumeration — self-emit its Rust via * Fix compile-clean parse error in stage0 crate layout witness. Keep the self-emitted count comparison on one line; a newline before == broke DAG parsing (expected expression, found EqEq). Co-authored-by: Cursor <cursoragent@cursor.com> * Drop redundant infer cherry-pick; main already has record-lit fix. Reverts src/v1/04_infer.dag and v1_compiler_infer.rs to origin/main (#6701/#6696). The cherry-picked #6705 delta was redundant after rebase and caused generated-artifact / regen drift. Co-authored-by: Cursor <cursoragent@cursor.com> * Align infer with main after rebase (drop surviving cherry-pick hunk). Keeps src/v1/04_infer.dag and v1_compiler_infer.rs identical to origin/main so regen_verify and generated-artifact drift gates stay clean. Co-authored-by: Cursor <cursoragent@cursor.com> * Regen bootstrap_stage0_crate_layout_generated.rs (trailing-comma drift). main_wet byte-compare caught a hand-merge comma in the last filename entry; aligns bootstrap with stage0_crate_layout_emit output. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Wave 2 Band A self-emit: discovery_enumeration — self-emit its Rust via * WIP: Wave 2 Band A self-emit: discovery_enumeration — self-emit its Rust via --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Cursor <cursoragent@cursor.com>

… (orphan from #6811) (#6822) #6811 (5f3c76d) added docs/plans/effect-namespace-grants.md with no inbound link and no bind: provenance row, orphaning it in the doc-reachability graph. doc_graph_has_no_orphan_docs reds on it — main has been RED since that push (last green: ab4d99b; failing: 5f3c76d, ccdf35f). It only surfaces on whole-tree floor runs (most PRs affected-set-skip the witness), so it slipped in on the main push itself and blocks every subsequent whole-tree run. Fix is the established staged-design-doc remediation (same pattern as witness-realization-plan / machine-shape / rc-ownership, #6654/#6663): one standalone `data <x>_doc_provenance: String = "bind: <path> — …"` carrier in the topical authority (host_effect_orchestration.dag — the doc is the HostEffect grant/envelope shape). The note paraphrases the doc's own abstract and cites its own FLAG-A §6 dissolve trigger; no design content added. Verified: the doc-reachability graph goes orphans=1 → orphans=0 with this row (reproduced by a faithful port of cli_run.rs build_doc_graph_report). Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…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>

briansrls and others added 2 commits July 14, 2026 23:54

briansrls mentioned this pull request Jul 15, 2026

docs/plans: machine-shape orthogonal scheduling — end shape, no-kind rule, convergence map #6654

Merged

briansrls and others added 2 commits July 15, 2026 01:01

Merge origin/main into session/lively-heron-614 (catch up before P0 r…

af0f3fb

…ebuild)

briansrls mentioned this pull request Jul 15, 2026

v1 resolve: collapse redundant per-module ancestry_str_bindings recompute to Rc-borrow #6660

Merged

briansrls and others added 3 commits July 15, 2026 11:35

P0 status + three open operator rulings recorded in the plan doc

5e8cd86

The rulings block the final ~25-row drain; recorded with sites, options, and recommendations so the lane is resumable from the doc alone. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

briansrls changed the title ~~v2 memory-control audit + witness-realization plan (docs only)~~ v2 memory-control audit + witness-realization plan + P0 field wall (568→45 drained) Jul 15, 2026

briansrls added 2 commits July 15, 2026 17:33

Merge remote-tracking branch 'origin/main' into session/lively-heron-614

bc76f2f

# Conflicts: # src/v1/stage0/src/cli_run.rs

WIP: v2 memory control audit

50c1186

gunbai-bot Bot mentioned this pull request Jul 15, 2026

v1 resolve is still superlinear #6676

Closed

6 tasks

This was referenced Jul 15, 2026

machine-shape plan: record operator rulings 5-8 (fabric relationship, evidence carriers, Energy, scheduling-invariant refinement) #6685

Merged

std.machine_shape: allocation-as-contract Phase 1 landing #6687

Merged

briansrls added 4 commits July 15, 2026 18:38

WIP: v2 memory control audit

b4c45ee

WIP: v2 memory control audit

a3e13c6

WIP: v2 memory control audit

43dd899

WIP: v2 memory control audit

9f55faf

briansrls and others added 2 commits July 15, 2026 19:21

WIP: v2 memory control audit

9edb928

gunbai-bot Bot mentioned this pull request Jul 16, 2026

Namespace homonym triage tier 2: emit, extdeps anchor, live_tree #6697

Merged

3 tasks done

gunbai-bot Bot mentioned this pull request Jul 16, 2026

P0 field wall: stand down on census-ambiguous bare type names (fixes main-red) #6709

Merged

This was referenced Jul 16, 2026

Merge-lifecycle interleaving witness: the squash race as a bounded-exhaustive theorem #6725

Merged

Phase B / F7: scope+design decl-emission de-fork (emit_semantic_decl rust-hardwired) #6684

Merged

briansrls mentioned this pull request Jul 16, 2026

Witness realization P1–P6: measured space + the artifact store (the lane PR; P0 merged via #6663) #6738

Merged

4 of 5 tasks

gunbai-bot Bot mentioned this pull request Jul 17, 2026

Restore doc-reachability wall: bind effect-namespace-grants.md (orphan from #6811, main is RED) #6822

Merged

gunbai-bot Bot mentioned this pull request Jul 17, 2026

Regen DESIGN.md: link 4 remaining orphan plan docs (green doc-orphan wall + drift gate) #6828

Merged

gunbai-bot Bot mentioned this pull request Aug 27, 2026

Record the semantic-merge class as declared debt on the lifecycle authority that already models it #9386

Merged

gunbai-bot Bot mentioned this pull request Oct 8, 2026

Isolate fixture census on a scratch MultiEntryIndex #13575

Closed

2 of 3 tasks

Navigation Menu

Repository navigation

v2 memory-control audit + witness-realization plan + P0 field wall (568→45 drained) - #6663

v2 memory-control audit + witness-realization plan + P0 field wall (568→45 drained)#6663
briansrls merged 32 commits into
mainfrom
session/lively-heron-614

briansrls commented Jul 15, 2026

Uh oh!

cursor Bot commented Jul 15, 2026

Uh oh!

briansrls commented Jul 15, 2026

Uh oh!

gunbai-bot Bot commented Jul 15, 2026

Uh oh!

gunbai-bot Bot commented Jul 15, 2026

Uh oh!

gunbai-bot Bot commented Jul 15, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

briansrls commented Jul 15, 2026

What

docs/plans/v2-memory-control-audit.md — findings (each green- or refuted-by-execution, with a calibration control)

docs/plans/witness-realization-plan.md — the forward path (P0–P6)

Test plan

Uh oh!

cursor Bot commented Jul 15, 2026

Uh oh!

briansrls commented Jul 15, 2026

Session handoff — resume context (lively-heron-614, 2026-07-15)

Branch state (session/lively-heron-614, pushed through 5e8cd86eb)

What is proven, by execution

BLOCKED: three operator rulings (full text in docs/plans/witness-realization-plan.md §P0 STATUS)

Working mechanics (hard-won; also in project memory)

Queue after P0

PR admin

Uh oh!

gunbai-bot Bot commented Jul 15, 2026

Uh oh!

gunbai-bot Bot commented Jul 15, 2026

Uh oh!

gunbai-bot Bot commented Jul 15, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

`docs/plans/v2-memory-control-audit.md` — findings (each green- or refuted-by-execution, with a calibration control)

`docs/plans/witness-realization-plan.md` — the forward path (P0–P6)

Branch state (`session/lively-heron-614`, pushed through `5e8cd86eb`)

BLOCKED: three operator rulings (full text in `docs/plans/witness-realization-plan.md` §P0 STATUS)