Repository navigation
Ground srv1/srv2 memory via observed DIMM populations; retire deferral scaffolds - #6780
Merged
Merged
Conversation
…ntry conditions + validated verdict lattice (#6727 closed) Operator ruling 2026-07-16: no demo/throwaway code that breaks the repo's main patterns. Phase 4's demo-as-first-consumer element is superseded: the closed #6727 hand-wired evidence refs and a hand-typed receipt (a forged license) to simulate the derivation the real system must perform. Re-entry requires executed law-claim receipts (witness-realization lane), a real corpus fold as first consumer landing in the same PR as its carriers, and the refusal path as the corpus default proven by RED. The closed rework's validated license-check semantics (5-gate verdict lattice, all typed refusals) are preserved as the binding design. (Branch rebuilt from origin/main after dashboard automation reset it to a stale base and dropped the first application of this amendment.) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…l scaffolds srv1 (192.168.1.183) and srv2 (192.168.1.184) observed 2026-07-16 via BMC Redfish with operator-supplied rotated credentials: both uniform 8x HMA82GR7AFR4N-VK (SK Hynix, 1R x4, 16 GiB, DDR4-2666) = 128 GiB, matching MemorySummary. Both ground onto the existing cited hma82gr7afr4n_vk_catalog row - no new catalog rows needed. - srv1_host/srv2_host gibibyte(128) placeholders -> memory_devices_from_population - FleetHostMemoryPopulationDeferral type, rows, list, and Scaffold dispositions deleted: their dissolution trigger (rotated BMC creds) fired - fleet_host_memory_nominal_vs_usable_note updated to grounded state; the 125 GiB OS-usable budget on gunbc_ci_host stays untouched pending its own MemTotal provenance (scaffold in ci_fleet remains) - witnesses: deferral-count witness dissolved with its subject; added population==MemorySummary, host-derives-from-population, raw-Redfish-fields notes, and a RED 7-stick discriminator for srv1 All 11 witnesses green via claim-run; mutation control (stick_count 8->7) reds srv1_srv2_populations_match_bmc_memory_summary. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
gunbai-bot
Bot
changed the title
2 tasks done
briansrls
added a commit
that referenced
this pull request
Jul 17, 2026
…sistency) regen_stage0 on the merged tree (main-merge #6780/#6783 + my space-complexity work) changed exactly one seed file — v1_compiler_complexity.rs — activating space_classes (the ComplexityReport space-order surfacing) in the compiled compiler. main-merge seed was already consistent; this is the clean delta for my complexity.dag change, keeping regen --verify green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jul 18, 2026
…ane PR; P0 merged via #6663) (#6738) * P2 pure-spec half: content-addressed artifact store — the first read eviction field std.artifact_store (witness-realization plan P2, pure fold spec; host transport is the second half and this spec is its single authority): - ArtifactKey { closure_digest, emitter_identity, target_language, toolchain } -> artifact_key_hash via std.content_hash (one hash authority) — keying is ContentHash BY SHAPE; no mtime/existence input exists, so ExistenceKeyed is unwritable here (the #6352 wall by construction) - store_over_provider READS CacheProvider.eviction and refuses construction over a non-SpacePacked provider (typed StoreRefusedEviction) — the eviction field's first behavioral consumer (memory-control audit F5) - store_get bumps recency; store_put packs to budget by least-recent eviction with every eviction COUNTED in StorePutReceipt (refuse-or-count, never widen) - budget stays a typed parameter beside the row for now: EvictionClass.budget carries cited upstream policy PROSE in extdeps rows (two concepts in one field); dissolve-on recorded in the module note for the variant split Witnesses (all green by execution, current binary, SubstrateInputsOnly): - store_construction_reads_eviction_holds (ScopeExit provider -> typed refusal) - store_hit_and_stale_never_served_holds (toolchain mutation -> new key -> miss) - store_budget_evicts_least_recent_counted_holds (touch ka, put kc -> [kb] evicted, within budget, survivor still hits) - store_no_eviction_under_budget_holds Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * P2 host-transport half: filesystem realization of the artifact store extdeps.realization.artifact_store_fs — one transport handler bound to the pure spec (std.artifact_store stays the single authority; a remote CAS is the other handler). The keyed path ENCODES identity (store_root/<hash>.artifact), so presence-at-path is a ContentKeyed hit for exactly that identity — not the #6352 existence-keying (which keyed output presence over unhashed inputs). SCOPE, honest and named: put/get only. The cited Filesystem service exposes Write/Read but no Delete/List, so SpacePacked budget enforcement on the persistent tier is unrealizable until those operations are added — until then the disk tier grows unbounded and the in-process fold is the only packed tier. Recorded in the transport note as the next rung, never a silent widen. Witnesses green by wet execution (artifact observed on disk at its hash path): - artifact_fs_roundtrip_holds - artifact_fs_mutated_input_misses_holds (stale-never-served on the persistent tier) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Plan doc: P2 status (both halves landed, green by execution; two named gaps) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * P1 (code): ObservePeakResidentAtSubject + the space algebra — memory becomes observable - RealizationMeasureEffect gains ObservePeakResidentAtSubject (audit F2: the effect coproduct had exactly one variant, time; a Measured space fact was unproducible by construction) - space algebra as time's DUAL (audit F4): space_measure_seq = max (sequential steps release), space_measure_par = add (concurrent steps co-reside), plus space_measure_list_seq; duality note records why the old sum was wrong - fleet_intent receipt rollup: space summed over a sequential list -> now the peak (the parallel rule was applied to the serial axis); keystone witness FLIPPED to assert max AND assert != sum, so the old contract cannot silently return - host physics: observed_peak_resident_bytes builtin (VmHWM in bytes) — registered in v1.compiler.method builtins, realized in the hand-maintained interpreter, FAIL-CLOSED when the host cannot report it (a fabricated 0 would be a Measured lie, DESIGN section 5) - peak_resident_measured_witness_test: the plan's P1 ACCEPT — the first CostAccount.space with basis Measured produced BY EXECUTION — declared ReadsLiveTree honestly (reads /proc through a builtin, the classifier's declared blind-spot class); plus the seq=max/par=add RED control Receipts land in the follow-up commit with the regen-synced stage0 and the rebuilt binary (pipeline in flight); the pure-.dag half already compiles clean through the P0 wall. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * P1 (receipts): regen sync + green-by-execution verification Regen-synced stage0 (the observed_peak_resident_bytes registration reaching the generated method registry) after rebuilding the regen tool from merged main (its compiled-in roster predated the Wave-2 crate-layout file; two-generation discipline: build committed -> regen -> build). Receipts on the rebuilt binary: - peak_resident_measured_holds -> true : the FIRST CostAccount.space with basis Measured produced by execution (plan P1 ACCEPT; audit F2 discharged at the witness grain) - space_seq_is_peak_not_sum_holds -> true (seq=max=5, par=add=8, list_seq=5) - witness_space_rolls_up_across_receipts -> true FLIPPED (asserts max AND != sum; 1024/2048 samples discriminate) - P0 regression: diagnostics_witness record_field_walls suite exit 0 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * P3 MVP: emit-on-demand at the source grain — second run pays zero emit The emit cache wired through the P2 store, keyed on INPUT identity: inferred_tree_digest x emitter identity x target x artifact kind — the same Hash=ContentHash authority the fnv1a64 convergence landed, composed by artifact_key_hash. Cold: miss -> pure emit (v2 emit = serialize_target o translate) -> put. Warm: served from the store WITH NO EMIT CALL IN THE ARM, and the served bytes asserted equal to a fresh emit (the agreement receipt — plan P3 ACCEPT (a) at the source grain). Witnesses green by wet execution (emitted rust_add source observed on disk at its hash path): - emit_source_store_cold_then_warm_holds - emit_source_store_mutated_emitter_misses_holds (emitter version bump -> new key -> miss; stale emitter output never served) - emit_source_store_provider_gate_holds Rung remainder (named): the native-artifact tier (zero BUILD — needs FLAG A, the hermetic pinned-toolchain ruling, and the parse-census first customer) and enrollment of the wet witnesses. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Design: effect grants over namespaces — hermetic/wet dissolved into (frame x verb x subtree) Operator rulings captured (2026-07-16): "hermetic" conflates four axes (input closure / output reach / handler binding / selection eligibility — the doc's own state-space-conflation failure mode, effect-system edition), and the fix must reuse NAMESPACES directly rather than mint a "universe" vocabulary. An effect target is a position in a containment tree that already exists (filesystem, URI, proc, code names); permission is a grant of (verb x subtree) on a frame; admissibility is the same prefix relation the naming lane walks — effects become the containment structure's fourth consumer, not a fork. Convergence map covers the proto-envelopes already in-tree (the hand-rolled workspace_root path gate, std.resources.ResourceHandle, AuthScope, LiveTreeDisposition) — all dissolve into derived projections. FLAG A reframed: build admissibility becomes the first grant row (Read within closure + pinned toolchain; Write within own workspace), scaffold-marked, dissolving into the P-B enforcement seam — a row, not a mode exception. Bound into the doc graph via the witness-realization plan's FLAG A section (orphan wall re-verified green). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Effect-grants design: the containment law (target lifecycle) + fix inherited orphan Design refinement (operator, 2026-07-16): a write is frame-contained iff (target within a frame-controlled namespace) AND (target lifecycle within frame lifecycle) — the lifecycle conjunct is what the old "hermetic" intuition was actually about, graded on the section-5 construction/validation axis (LifecycleByConstruction: ephemeral container fs, netns-scoped loopback receiver — persistence unwritable past the frame; LifecycleByConvention: /tmp scratch + cleanup). Four named acceptance cases added up front so the model cannot mislead: netns loopback = contained; container write = contained by construction; /tmp scratch = contained by convention only (the artifact store witnesses' honest current grade); BMC POST / repo-tree write = wet under any grade. Also: bind docs/plans/emitted-crate-partition-design.md into the doc graph (frontier.dag provenance row) — it merged orphaned on main (8322580) and the doc-reachability wall was red on main; wall re-verified true here, and frontier.dag entry-compiles clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Record duplicate-computation direction: one ComputationIdentity, N grains (execution-frame is the gap) Operator direction (2026-07-16): duplicate-computation detection is not shell-specific — "same inputs + deterministic process → same content-identity → the second is duplicate work" is the whole law; the surface it's read on is a realization axis, not the concept. Records the three detection grains against ONE ComputationIdentity: - within-script (argv/ShellWord) — v2.lens.duplicate_computation, dissolves in (§7) - within-graph (content_hash over Node subtrees) — v2.std.materialize MVP - within-run execution-frame — the UNCOVERED grain, where the ~275s double-resolve lives (two compile_to_resolved calls in one v1-seed claim_executor process, invisible to both peers). Ladder-classed: shared-state frame ⇒ AuthoredDuplication ⇒ REWIRE (not cache), distinct from the cross-run isolation-boundary store obligation — same identity, remedy by frame. Direction: the general detector must reach the execution-frame grain; the argv lens then dissolves into it and the within-graph MVP extends down — one detector, the surfaces its realizations. Doc is the roadmap ④'s linked carrier; orphan wall re-verified green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Fix §5 fail-open: eval-call memo served stale world-reads (effect-dispatch odometer) Found via the artifact-store List-after-Delete witness: the interpreter's eval-call memo treated "no declared `uses` clause" as pure — and ZERO corpus funcs declare `uses`, so every effectful named func was memo-eligible. A func called twice with equal args in one eval served the FIRST result — e.g. a Filesystem.List after a Delete returned the pre-delete listing. That is a world-read served stale from cache: a silent §5 fail-open in the bootstrap engine, not a witness quirk. Fix (4 edits, transitive by construction): an effect-dispatch odometer on InterpContext, ticked at the single eval_service_call chokepoint; the memo refuses to STORE any call during which the odometer advanced. An observed effect poisons cacheability — exactly the ladder's "FreshEffect/WorldRead is never memoized" law, enforced at the realizer instead of by a vacuous uses-gate. Value::eq stays the sole equality authority; pure calls still memoize. Known residue (named): world-effecting BUILTINS (e.g. observed_peak_resident_bytes, filesystem via the service path already ticks) — the odometer covers service dispatch; a builtin-effect tick is the follow-up if a pure-memoized builtin ever reads the world. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Delete/List on the Filesystem service (operator Q2) — closes P2's persistent-tier gap The cited Filesystem service exposed only Write/Read, so P2's SpacePacked budget enforcement on the on-disk store was unrealizable (named gap in the P2 landing). Adds the two missing operations, keeping the extdeps interface faithful to the real dependency: - filesystem_io.dag: Delete + List operations (List readonly) - file transport gains a verb property (parse: 00_core file_transport_node + 02_parse parse_file_fields thread `verb`; interpreter: dispatch_file honors verb "delete"/"list" via remove_file / sorted read_dir). Absent verb keeps the original content-param convention (write iff `content` param, else read). - artifact_store_fs: artifact_fs_delete / artifact_fs_list wrappers - witness: artifact_fs_delete_then_misses_holds — put -> listed -> delete -> miss -> unlisted, green by wet execution (also the discriminating input that surfaced the memo fail-open fixed in the parent commit) Regen-synced (v1_compiler_parse.rs, v1_std_core.rs). Persistent-tier eviction (the SpacePacked enforcer using List+Delete) is the follow-up now that the ops exist. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * P4 v0: realize packing — width against MEASURED peaks, refuse-not-fabricate The memory-safe packing half of `realize` (spine FLAG D), consuming P1's measured space so the exit-137 failure mode (memory-blind packing OOMs) becomes arithmetic. std.realize_pack: - MeasuredPeak = PeakMeasured | PeakUnknown, derived from CostAccount.basis (P1's Measured space vs a Predicted guess) - HostBudget = BudgetReadable | BudgetUnreadable — the typed read - realize_pack_width -> RealizeVerdict = PackedWidth | MaturationReserve | BudgetRefused: * measured peak + readable budget -> PackedWidth min(independence, budget/peak), reusing realization_width.memory_bounded_shard_count (20% headroom reserved — the maturation-reserve margin; 100/25 packs to 3, not 4) * unknown peak -> MaturationReserve width-1 (first-run subject runs alone, its receipt converts it next round — the governor's admission logic, modeled) * unreadable budget -> BudgetRefused, NEVER the conservative_fallback_width fabrication (realization_width.dag:109 — the live §5 absorbing-fallback the memory-control audit flagged: budget unreadable answered with a number) Witnesses (6, green by execution): packs within budget; capped by independence; never exceeds budget (the exit-137 arithmetic control, W*peak <= budget by construction); unknown-peak -> maturation reserve; unreadable-budget -> refuses; measured-vs-predicted peak discrimination. Remaining for P4: the width-1 fabrication in memory_aware_spawn_width is now superseded for the measured path; wiring realize_pack into the executor's per-runnable scheduling (consuming real getrusage receipts) is the integration step. The math + refusal discipline land here first, green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Design: space complexity — the dual of the time/termination analysis Operator direction (2026-07-16): extend the complexity analysis to space (the gap). Derived, not measured (§4: bounded/forward ⇒ checked not discovered — measuring peak RSS is the reflection-evidence cop-out). Two readings: asymptotic (O(n)) AND concrete derived bytes ("known/defined to these bounds"). Underivable = counted frontier now, hard error later (fail-closed ratchet). The key finding that makes it a dual, not a new analysis: ComplexitySummary already carries work/span/output_size as CostExpr (axis-agnostic), and CostSum is a fold — time SUMS over iterations, space takes the MAX (sequential residency releases). That is exactly P1's space_measure_seq=max lifted to CostExpr. So peak_space = space_of(work) — one transform swapping sum/max, accumulator term reusing output_size, recursion depth bounded by the SAME DescentEvidence that proves termination. Two readings of one descent structure (§2). Folds five threads onto one page: audit F2/F3 (space unobserved/underived), P1 (the residency algebra — reused as the transform), P4 (re-point pack input from MeasuredPeak to derived bound; retire the reactive governor), the 2026-07-12 ruling (derived not authored literals), the allocation model (the derived per-witness bound IS the up-front allocation; Σ ≤ budget = GUARANTEED mode at witness grain). Sequence: witness-grain concrete space first (closed closures), then asymptotic, then re-point P4, then ratchet the frontier to error. Bound into the doc graph via the witness-realization P1 note (which this supersedes as the keystone); orphan wall green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Space complexity increment 1a: peak-working-set derivation, the dual of time The space-complexity analysis's core, as the structural dual of the existing time cost-expr — green by execution, no rebuild (interpreted from source). In src/v1/complexity.dag, beside the cost algebra it duals: - space_of(work: CostExpr) -> CostExpr : the transform. Sequential steps RELEASE so time's CostAdd becomes CostMax; concurrent steps CO-RESIDE so time's CostMax becomes CostAdd (P1's space_measure_seq=max / space_measure_par=add, lifted to CostExpr); a fold's CostSum collapses to its body's peak (iterations release). CostUnknown passes through fail-closed. - fold_peak_space(body_peak, output_size) : adds the accumulator/output_size term. - eval_cost_expr_concrete / eval_size_expr_concrete : lower a closed expr to concrete bytes (Absent on any unknown/free var — refuses, never fabricates). Witnesses (6, green by execution, --source-root src/v1): - reducing_fold_is_constant_space: O(n) time fold -> O(1) space (the headline) - sequential_releases_max_not_sum / parallel_coresides_add_not_max: the P1 duals - concrete_derived_bytes: closed expr -> exact bytes (40) - fold_that_builds_is_linear_space: output_size 100*4 + body 4 -> 404 bytes - unknown_cost_is_fail_closed_space: CostUnknown -> unknown space, concrete refuses (the SpaceBoundUnknown counted bottom; hard-error ratchet is the later stage) Design: space-complexity-design.md §2. Not floor-enrolled yet — imports v1.compiler.complexity so needs --source-root src/v1 (like the v1-internal tests); enrollment (host bin or v1-root discovery) is the follow-up, alongside the ComplexitySummary.peak_space field (38 construction sites) and the P4 re-point onto the derived bound. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Space complexity increment 2: asymptotic reading (O(n) etc.), space order below time The second reading the operator asked for — asymptotic space class — reusing std.induction's CostBound/cost_poly on space_of(work). Green by execution, no rebuild (interpreted). In src/v1/complexity.dag: - cost_expr_degree(e) -> Int? : polynomial degree. CostSum over a size var = +1 factor of n; seq/par take MAX degree; products ADD; bare log = degree 0 (sub-linear); Absent = frontier (fail-closed, never a fabricated degree). - space_asymptotic_bound(work, param) = degree_to_bound(cost_expr_degree(space_of(work))) -> ConstantBound | cost_poly(...) | ForeverBound. time_asymptotic_bound is the same on the raw work, for the side-by-side. Because space_of collapses the CostSum a reducing fold's TIME carries, space order is <= time order by construction. Witnesses (4, green): - reducing_fold: O(n) TIME (degree 1), O(1) SPACE (ConstantBound) - nested_reducing_loop: O(n^2) time, O(1) space (both CostSums collapse — the striking dual) - parallel_region: constant space - frontier_maps_to_forever_bound: CostUnknown -> ForeverBound, not a degree Design: space-complexity-design.md §3. Increments remaining: wire peak_space into ComplexitySummary (rebuild-gated, 38 sites), re-point P4, ratchet the frontier. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Wire space-complexity into ComplexitySummary (peak_space + concrete fill) Extend the landed space-complexity analysis (space_of / fold_peak_space / eval_cost_expr_concrete) into the compiler's per-function summary. - ComplexitySummary gains an OPTIONAL peak_space: CostExpr?. Optional so the P0 field wall (04_infer) skips it: all ~38 existing construction sites stay unchanged, an absent peak_space = the SpaceBoundUnknown counted frontier (fail-closed staging). Verified: complexity.dag entry-compiles 0 diagnostics. - Derived once at the finalized per-function summary (get_or_compute_summary's `simplified`) via derive_peak_space: space_of(work) for a scalar result, additive fold_peak_space(space_of(work) + output_term) for a collection result (the `result` output_size entry). Intermediate/error/external/seed summaries leave peak_space absent by design. - cost_account_space_from_summary(summary, size_env) -> ByteSize? fills CostAccount.space (basis Derived): eval peak_space at a closed size_env to a concrete ByteSize; absent peak_space or an underivable expr returns none, never a fabricated bound. - New witness complexity_summary_space_witness_test.dag (4 test fns, green by interpretation): derived peak yields expected bytes; absent peak -> none; underivable (CostUnknown) peak -> none (RED control); reducing-fold work is O(1) space regardless of n. Follow-up (out of scope): regen + rebuild-to-seed to activate the compiled realization. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * P4 re-point: pack against the DERIVED bound, not measured peak — seam closed Operator direction (derive, don't measure — §4). std.realize_pack re-pointed off P1's measured peak onto the statically DERIVED space bound: - MeasuredPeak/PeakMeasured/PeakUnknown -> DerivedBound/BoundDerived/BoundUnknown - measured_peak_of(CostAccount) -> derived_bound_of(derived_space: ByteSize?): Present = the derived working-set bound, Absent = SpaceBoundUnknown (the fail-closed frontier). P4 is now decoupled from CostBasis — it consumes the ByteSize? that cost_account_space_from_summary (eeeda2b, the subagent's ComplexitySummary wiring) produces. That closes the seam: ComplexitySummary.peak_space -> space_of derivation -> cost_account_space_from_summary -> ByteSize? -> derived_bound_of -> realize_pack_width. - realize_pack_width / realize_fits_budget take DerivedBound; BoundUnknown -> the width-1 maturation reserve (a not-yet-derivable subject runs alone, not a fabricated number); the refuse-not-fabricate discipline unchanged. Measurement (P1's ObservePeakResidentAtSubject) is demoted to at-most a falsifier, never a scheduler input — the whole memory-control line is now derived, not observed. Witnesses (6, green by execution, interpreted — no rebuild): packs within budget (headroom-reserved 3, not 4); capped by independence; never exceeds budget (the exit-137 arithmetic control); BoundUnknown -> maturation reserve; unreadable budget -> refuses; derived-vs-frontier bound discrimination (the new ByteSize? seam). Remaining for P4: activate in the seed (regen — gated with the space-complexity seed activation) + wire realize_pack into claim_executor per-runnable scheduling. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Regen seed: activate space-complexity peak_space in the compiled compiler regen_stage0 activated the complexity.dag changes (peak_space field + space_of + concrete evaluator, and the get_or_compute_summary derivation) into the generated seed v1_compiler_complexity.rs — the one file that changed (surgical; the other 94 generated files byte-identical). Built on srv1 (128 cores, 4m17s cold / 2m34s rebuild — off the memory-constrained Pi that watchdog-crashes on this crate). regen_stage0 --verify: regen_divergence_count=0 — committed stage0 matches a fresh self-compile, so the byte fixed point holds with peak_space live. The compiled compiler now derives peak_space during real complexity analysis (previously only interpreted from source). Remaining (flagged by the wiring pass): the interpreter RAISES on an omitted optional field while the seed reads None gracefully — latent-safe today (cost_account_space_from_summary is only called on simplified summaries, which always set peak_space), reconcile when a broader consumer lands. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Space classes in ComplexityReport (observable on real code) + floor-classify new witnesses Two things the srv1 corpus validation surfaced. 1. Observability: ComplexityReport gains space_classes: Map<String,String> beside function_classes — build_complexity_report now derives it via classify_complexity(space_of(work)) per function, so the derived SPACE order is observable for every REAL gunbc function (not just synthetic CostExpr witnesses). TopoBuildAcc threads it; empty_complexity_report seeds it. 2. Floor classification (validation caught my new witnesses breaking the hermetic floor — neither a space-complexity logic regression): - The three space witnesses import v1.compiler.complexity, unresolvable in the discovered corpus's roots -> a FATAL resolve halt at entry 46. Excluded from discovery (they run in the v1 lane via --source-root src/v1; host-bin enrollment like diagnostics_witness is the proper follow-up). - artifact_store_fs_witness does real Filesystem.Write -> hermetic refuses (correctly). Excluded from hermetic discovery (wet lane), same pattern as the existing ci_deploy_observed_wet / host_effect_apply wet exclusions. Interpreted entry-compile green; srv1 regen+rebuild+corpus re-validation follows. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Fix the debt srv1 corpus validation caught: residue wildcards + the last wet witness The srv1 corpus run (1900 PASS, and the space-complexity seed activation proven corpus-safe) surfaced 4 failures, all from witnesses I added this session — none a logic regression: - 2 non_fold_residue FAILs: my witnesses + realize_pack used `_ =>` wildcards over closed coproducts (CostExpr, CostBound, RealizeVerdict) — the §4 residue the lens bans. Fixed by making them exhaustive/behavioral: realize_pack + its witness list every RealizeVerdict arm; the space witnesses now assert through the concrete evaluator (eval_cost_expr_concrete, exhaustive Optional) and the polynomial degree (cost_expr_degree) instead of matching CostExpr/CostBound structure — cleaner behavioral tests (sequential releases -> eval 50 not sum 80; parallel co-resides -> eval 80 not max 50) with ZERO wildcards. non_fold_residue_clean_holds -> true (0 unrostered residue, re-verified). - 2 emit_source_store FAILs: real Filesystem.Write in hermetic mode. The path is test/claim/manual/ (not test/manual/), so the existing exclusion missed it; added emit_source_store_test.dag explicitly (wet lane). All rewritten witnesses green by interpretation; final srv1 corpus re-validation follows. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Regen seed: space_classes into the compiled compiler (merged-tree consistency) regen_stage0 on the merged tree (main-merge #6780/#6783 + my space-complexity work) changed exactly one seed file — v1_compiler_complexity.rs — activating space_classes (the ComplexityReport space-order surfacing) in the compiled compiler. main-merge seed was already consistent; this is the clean delta for my complexity.dag change, keeping regen --verify green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * P4 handoff: executor cutover is a bridge call, not a self-host dependency Records the corrected framing in the plan's P4 section: claim_executor is the terminal bootstrap kernel (not a self-host emit target) and already interprets .dag, so it can call realize_pack through run_in_context_with_args rather than forking the packing law into Rust (§2) or waiting on the 27-module frontier. Seam: surface the derived bound, read the governor's budget, call realize_pack, advisory-first then demote the governor. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * Fix compile-clean gate: move space-complexity witnesses out of dag/ tree The three space-complexity witnesses import v1.compiler.complexity (a src/v1 module), but lived in dag/test/claim/. The whole-tree compile-clean gate compiles [dag, src/v2] WITHOUT src/v1, so their imports could not resolve — red as 'module v1.compiler.complexity not found' whenever a src/v1 touch forces the whole-tree baseline. Discovery-exclusion handled the runner but not the gate; a dag/ file simply cannot import from src/v1. Move them to src/v1/test/claim/ (compiled with src/v1, not swept by regen's seed-closure walk, not in discovery scan dirs) and drop the now-dead exclusion substrings. All 6+4+4 test fns pass from the new home via claim_batch --source-root src/v1 --source-root dag --source-root src/v2. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * Fix batch-4 gate regressions: extdeps authority anchor + drop redundant frontier binding - extdeps_external_authority_gate: artifact_store_fs.dag (P2, new) was the only extdeps/realization module missing the extdeps_external_authority_anchor every sibling declares. Add it (Https -> the realization dir, matching v1_handler). All 9 realization modules now carry exactly one anchor. - self_host_realized_comparison / cleanup: drop emitted_crate_partition_plan_doc_provenance from frontier.dag. It was a doc-reachability workaround added when the design doc was orphaned; main #6828 now links it from DESIGN.md (line 92), so the row is a redundant duplicate binding (unreferenced). frontier.dag is now byte-identical to main. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * Fix self_host_realized_comparison: drop v2 import from relocated witnesses Moving the space witnesses to src/v1/ (to fix compile-clean) put them in regen_stage0's compile surface ([src/v1, dag]) — but they still imported v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } (src/v2, not in regen's roots), so 'regen_stage0 --emit-fresh' failed with unresolved import, and self_host_realized_comparison_reads_real_bytes then couldn't read the fresh-emitted bytes (No such file or directory) -> Bool(false). The v2 import fed only a 'data live_tree_disposition = SubstrateInputsOnly' metadata decl for discovery-based affected-set selection, used in no test fn and moot now that these run manually. Drop the import + decl; the witnesses become pure [src/v1, dag] (std + v1.compiler.complexity), compile clean under both regen and the manual runner, and all 6+4+4 test fns still pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * Delete homeless space-complexity witnesses (operator: 2026-07-18); declare Rust-test follow-up The three space-complexity .dag witnesses test v1.compiler.complexity (a src/v1 compiler-internal module) and had no clean home: dag/ fails the compile-clean gate's cross-layer import ([dag, src/v2] roots, no src/v1), and src/v1/ makes regen_stage0 --emit-fresh emit them as unregistered stage0 seed files (breaking self_host_realized_comparison). The analysis stays proven in-seed by execution (regen, runs every compile); the discriminating behavioral REDs are recorded in space-complexity-design.md as a declared follow-up to re-add as Rust tests in compiler_tests.rs when P4 makes the coverage load-bearing. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Completes the fleet
ComputeHost.memorygrounding started in #6764: srv1 and srv2 observed via BMC Redfish with operator-supplied rotated credentials (2026-07-16), theirgibibyte(128)placeholders dissolved throughHostMemoryPopulation, and the deferral scaffolds retired — their named dissolution trigger (rotated BMC creds) fired.HMA82GR7AFR4N-VK(SK Hynix, 1R x4, 16 GiB, DDR4-2666) = 128 GiB, matchingMemorySummary.TotalSystemMemoryGiB=128. Raw per-DIMM Redfish fields (RankCount=1, DataWidthBits=64, BusWidthBits=72, CapacityMiB=16384, OperatingSpeedMhz=2666) recorded in per-host observation notes, witness-pinned.hma82gr7afr4n_vk_catalog. Fleet composition now fully observed: srv1/srv2 uniform 8×AFR4N, srv3 mixed 7×AFR8N+1×AFR4N.FleetHostMemoryPopulationDeferraltype, both rows, the list, and bothScaffolddispositions deleted (theirbindtargetssrv1_memory_population/srv2_memory_populationnow exist as the single authority). The deferral-count witness dissolves with its subject.gunbc_ci_host.memorykeeps its MemTotal-shaped literal andci_fleetscaffold — its trigger (own OS MemTotal provenance) has NOT fired;fleet_host_memory_nominal_vs_usable_noteupdated to grounded state, "never blind-rewrite 125→128" preserved and witness-pinned.gibibyte,gibibyte_to_byte_size,std.disposition,std.decl_ref).Test plan
All 11 witnesses green via claim-run on the merged tree (
gunbc run --source-root dag --source-root src/v2 --claim-run --entry dag/test/claim/fleet_intent_memory_witness_test.dag --function <each>), including new:srv1_srv2_populations_match_bmc_memory_summarysrv1_srv2_host_memory_derives_from_cited_populationred_srv1_seven_stick_population_differs_from_observed(7-stick ≠ observed 8)srv1_srv2_observation_notes_record_raw_redfish_fieldsMutation control:
stick_count 8→7insrv1_memory_populationredssrv1_srv2_populations_match_bmc_memory_summary— the derived-vs-declared witness discriminates.🤖 Generated with Claude Code