Progress & observation, P0–P3: one event model, N renderers, a census wall

[briansrls]

Summary

The complete progress & observation lane, P0–P3, per the operator ruling that only finished work merges — a landed event model with no renderer is vocabulary nobody can see. One event model, N renderers, a census wall over the sites they replace.

Authority: docs/plans/progress-observation-design.md (+ §6b/§6c from #7169, now on main and merged into this branch). Every phase is green by execution with discriminating REDs proven by perturbation.

P0 — the model (dag/std/observation.dag)

ObservationEvent = subject (typed containment path: run ⊃ batch ⊃ entry ⊃ module ⊃ phase) × Begin | Step{k,n} | Concluded{outcome} × measured facts. Outcomes are a closed sum with Refused distinct from Failed. The five laws land as data rows, each naming its enforcer. Grounded, not minted: ancestry reuses std.effect_grant.path_is_prefix, over-budget arithmetic reuses std.temporal_effect.stall_budget_verdict, change-kind projects from std.change.KeyedDiffHunk, PSI pressure is std.measure.BasisPoint, glyphs are rows in std.symbols + extdeps.render.glyphs. Attention, BlockedOn, and the dwell threshold T are all derived, never hand-set; SchedulerHold is held in lockstep with the seed governor's HoldReason by execution.

P1 — the CI-log renderer (dag/gunbc/observation_ci_render.dag)

The pain point, built first. Append-only line projection of the event stream. Flagship acceptance, green against the real captured run: the fixture is run 30044816605's actual log — its t=33m heartbeat carried current=16107200512 swap=… psi_some_avg10=9.01 and named no subject while the process sat inside v2.compiler.normalized_tree for 606984ms, disclosed only at walk end. Re-rendered through the escalation law, the same window names the module at T and the memory-reclaim cause at 2T, in human units. Law 4 is structural: line placement is derived from attention, so a refusal cannot be written into a collapsed group. Escalation has two rates — reveal depth linear, emission points doubling — so quiet escalates without a drumbeat, bounded by construction. Relayed subject text is neutralized through the existing GitHub guard. Three required REDs proven: planted silent phase, orphaned Begin, Refused inside a collapsed group.

P2 — the TTY renderer (dag/gunbc/observation_tty_render.dag)

A sibling projection of the same carriers, not a second model — it imports the CI renderer's text helpers and the model, re-deriving nothing. The witness proves the sibling property: one event drives both surfaces. Differs only where the medium does: repaint-vs-scroll derived from attention (a refusal never repaints away), required preamble, BlockedOn inline with a named remaining (bounded prints the time, unknown prints why — never a fabricated ETA), reward animal on Final drawn deterministically from the one glyph authority. The reference's three gaps — no durations, Failed/Refused conflated, one-level escalation — are all fixed for free by projecting the shared model.

P3 — the census wall (dag/gunbc/observation_emit_census.dag)

Every floor emit site is a projection of the event stream or a counted frontier row with a reason and dissolve-on. EmitSiteDisposition is a closed sum — no third arm for an unlooked-at site. The roster carries the structured-tag families ([floor-memory], [typecheck-attribution], [gantt], [governor], [measurement]); the operator's named negative example, the [floor-memory] byte dump, is a rostered frontier row carrying the P1 heartbeat as its dissolve-on. The hygiene witness reads the live seed and reds on a stale marker (RED control proven). The exhaustive per-print wall over the ~75 raw eprintlns is a declared frontier gated on rebasing over the CI two-tier rework (#7162's line) — censusing sites that rework rewrites is the double-churn the operator ruled out.

The one Rust change

src/v1/stage0/src/std_measure.rs — P1 added milliseconds_per_second() to the seed-emitted dag/std/measure.dag, so its emitted Rust is regenerated in-PR (regen_stage0). Fixed point verified by rebuilding the regen binary from the new seed and re-running to zero drift.

Verification

31 model + 6 lockstep + 18 CI-renderer + 10 TTY-renderer + 6 census conjuncts, each with discriminating REDs. Compile-clean: 47 pre-existing errors in std/measure.dag and std/effect_grant.dag, zero attributable here.

After merge

P3's roster re-censuses the post-rework emit sites once this rebases over the CI two-tier rework, and the P1/P2 renderer wiring replaces the raw emit sites at that point (both touch the floor emit sites the rework rewrites — the sequencing the ruling fixed).

🤖 Generated with Claude Code

---

The visible payoff — the crawl window, before and after

The flagship is not a diagram; it is run 30044816605's actual log re-rendered through this PR's CI renderer. The after block below is produced by execution — observation_crawl_after_block() in dag/test/claim/observation_crawl_replay_test.dag, asserted green by observation_crawl_replay_witnesses — not hand-typed. Every input number is read off that run's log.

Before — what the operator watched for ten minutes (verbatim from the captured log, [floor-memory] heartbeats with no subject while normalized_tree typechecked for 607s):

[floor-memory] t=29m current=16106717184 swap=34359738368 high_events=44242 psi_some_avg10=5.33
[floor-memory] t=30m current=16107036672 swap=34359738368 high_events=132474 psi_some_avg10=7.96
[floor-memory] t=31m current=16107888640 swap=34359738368 high_events=221502 psi_some_avg10=5.89
[floor-memory] t=32m current=16105943040 swap=34359738368 high_events=303549 psi_some_avg10=20.63
[floor-memory] t=33m current=16107200512 swap=34359738368 high_events=387986 psi_some_avg10=9.01
... (identical shape every minute, 29m → 53m; no subject, no activity, raw bytes)
[typecheck-attribution] module=v2.compiler.normalized_tree ms=606984   ← disclosed only at walk end
##[error]The action 'gunbc ci' has timed out after 55 minutes.

After — the same facts through the renderer (real bytes, gunbc run / witness output):

::group::witness discovery — batch 3 (602 entries)
✅ dag/test/claim/virtual_media_unification_witness_test.dag done in 230ms
… 213 more finished cleanly
🕐 29 minutes in — still in witness discovery: entry 214 of 602, now typecheck v2.compiler.normalized_tree. memory 15.0 GiB, swap 32.0 GiB, pressure 5.3%
🕐 33 minutes in — still in witness discovery: entry 214 of 602, now typecheck v2.compiler.normalized_tree. memory 15.0 GiB, swap 32.0 GiB, pressure 9.0%
⏱ typecheck v2.compiler.normalized_tree has been quiet for 2 minutes — still working
⏳ typecheck v2.compiler.normalized_tree quiet for 4 minutes — blocked on memory reclaim (pressure 9.0%)
🚫 run=30044816605 batch=3:witness discovery entry=… — | FLOOR-BATCH-OVER-BUDGET wall=41m12s budget=22m
::endgroup::
🚫 213 of 602 entries finished in 41 minutes, 1 refused and 0 failed

The identity is now in every line, the bytes are gibibytes, the quiet module is surfaced at T, the memory-reclaim cause at 2T, and the run ends in a named refusal instead of a silent 55-minute timeout. The refusal line carries the | guard because it is relayed subject text (a child's stderr cannot mint workflow commands in the parent).

Definition of done — the live-run checkpoint

Replay-proof establishes correctness. It does not establish that you can see it on a real run, which is a different claim. So the merge bar gains one line, to be satisfied after the #7162 rebase:

• The PR's own final CI run renders in the new format. After CI two-tier placement rework + progress-observation lane (atomic delivery) #7162 (the CI two-tier rework) merges, this PR rebases, re-censuses the reworked emit sites, and flips the five rostered families + the ~75 raw eprintln residue to stream projections — so the last floor run before merge is the demo, not a replay of an old one.

Until then the live sites deliberately still print the old format (P3's frontier rows, dissolve-on = the P1 heartbeat) — wiring them before the rework rewrites those same paths is the double-churn the sequencing rule forbids.

[cursor]

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.

[gunbai-bot]

Addressed in 8cbf49c715 — I took the finding's stronger alternative ("dissolve the helpers into the canonical surfaces they duplicate") rather than only its weaker one ("add disposition contracts"), because on verification one of the three predicates was a genuine duplication and the finding located it correctly.

The real defect the finding found

observation_class_is_intrinsic_anomaly was a second hand-written table sitting beside observation_presentation's collapsible/expands_fully, with a witness asserting the two agreed. That witness was validation standing exactly where construction was available (DESIGN §5): it conceded the two tables could disagree and merely promised to notice.

Fix: ObservationDensity (RoutineCollapsible | SummaryAlwaysShown | AnomalyExpanded) is now the one table, and collapsible, expands_fully and intrinsic-anomaly are all derived projections of it. Disagreement is now unwritable rather than detected. The three display states stay distinct deliberately — the run summary is neither routine nor an anomaly, and a single boolean would have forced it to borrow the anomaly's presentation.

The witness roles are now separated, and I proved both by execution rather than asserting them:

witness	role	RED proven by
w_density_is_the_single_display_authority	content check	ClassRefused → RoutineCollapsible reds it — and reds only it, since the projections can no longer disagree
w_presentation_projects_density_rather_than_restating_it + the two collapse witnesses	construction guards	hardcoding collapsible: true reds all three

That second row is the point worth naming: after the refactor those three witnesses cannot fail on density content, because the disagreement they used to check is gone. They are not inert — they guard against the table being re-forked — but I'd rather state which witness carries the content and which guard the construction than leave a set that looks broader than it is.

Disposition receipts added for the remaining structural readers (observation_outcome_predicate_contract, observation_subject_predicate_contract, observation_selection_predicate_contract), following the materialization_ladder.dag shape you cited — each states why it is Terminal and names its discriminating corpus, rather than asserting terminality.

One correction on the rule's status

That hits the predicate-dissolution rule for substrate. […] Prevalence elsewhere in std/ is debt, not precedent for new additions.

Checked before complying, and the framing overstates it. Corpus-wide there are six predicate-disposition rows — four of them in materialization_ladder.dag itself, plus one in gunbc/fleet_posix_accounts.dag and one in v2/compiler/materialization_carriers.dag. No lens or gate enforces the pattern (grep over src/v2/lens/** finds no such check), and dag/std/ alone carries 52 *_is_* predicates. So this is a local convention of the materialization lane, not a substrate rule that new std/ code is in breach of.

That distinction matters for the same reason the house cares about inert lenses: a convention held at six sites and described as a rule will get cited as one, and "prevalence elsewhere is debt" is doing a lot of work to convert 52 counter-examples into support. If it should be a substrate rule, the honest form is a lens with a RED control, and that's a much larger piece of work than this PR — the enforcement-intent lane is where it would belong.

I complied anyway because the receipts are cheap, truthful, and improve the file, and because the underlying duplication point was correct. But I'd flag the rule's status rather than let this PR stand as precedent for it being enforced today.

Full suite green after the change: 30 model conjuncts + 6 lockstep conjuncts. Compile-clean unchanged at 47 errors, all pre-existing in std/measure.dag (46) and std/effect_grant.dag (1) — identical counts compiling those entries alone, zero attributable here.

[gunbai-bot]

Finding accepted and fixed in d26d5e0813. It's correct, and the unit-modeling hard-blocker applies squarely: avg10_centi was a percentage magnitude with a scale carried on bare Nat, and — the sharper half of the finding — the note beside it self-justified the conflation instead of tracking it. A note that explains why a rule doesn't apply is worse than no note, because it looks like diligence.

The fix consumes an existing carrier rather than minting one

Before choosing a carrier I checked what std.measure already had, and the corpus turned out to have anticipated this exact situation. std.measure carries both Percent and BasisPoint (both Measure<Dimensionless, One, Nat>), and basis_point_dissolve_on says:

dissolve-on: Ratio<Scale> carrier unifying Percent and BasisPoint as two scales of one Dimensionless authority […] else a third dimensionless-ratio use-case mints a third nickname.

This module is that third dimensionless-ratio use-case. So both of the finding's suggested routes — a Measure<Percentage, Centi> carrier, or "extending std.measure if a Percentage quantity is missing" — would have walked directly into the failure that row names in advance. Minting Percentage or PerMille would have been the third nickname.

BasisPoint is the right existing carrier on the merits, not just by elimination: its own basis_point_unit_note declares its semantic axis as utilization ratios, and a PSI some avg10 reading is precisely a utilization ratio — the share of a ten-second window in which work stalled on memory.

Resolution is exact, not truncated

This is why BasisPoint and not Percent: the governor reads one decimal of a percentage (9.0, 37.5, 90.0), and one basis point is a hundredth of a percentage point. So 37.5% is 3750 with nothing lost. Percent (Dimensionless, One) would have truncated 37.5 → 37 — a silent fidelity loss on a measured value, which is the same class of defect one layer down.

The note is rewritten to state the grounding and the deliberate non-mint, and to name where it goes next: when the Ratio<Scale> unification lands, this field follows Percent and BasisPoint onto it with no change of meaning.

On the RED

I'm not claiming a perturbation RED for this one. w_psi_pressure_carries_a_scaled_magnitude_not_a_scalar round-trips the value through the hold and checks the count survives, but the actual guarantee here is type-level — reverting the field to a bare Nat doesn't red a witness, it fails to compile. That's construction rather than validation, which is the stronger position, but I'd rather say so plainly than dress a compile-time guarantee up as a discriminating witness.

Suite green: 31 model conjuncts + 6 lockstep conjuncts. Compile-clean unchanged at 47 pre-existing errors in std/measure.dag (46) and std/effect_grant.dag (1), zero attributable here.

Thanks for the narrow, specific catch — this is the second review on this PR to find a real defect by reading the notes rather than only the types.

[gunbai-bot]

All three findings verified correct and fixed in f682d33f19. They were all in the new P1 renderer, and two of them are the renderer breaking rules its own model states — which is the most useful kind of catch.

1. GiB scale factor respelled as a literal. Confirmed: std.measure.gibibyte_scale_factor_bytes() exists at measure.dag:80 and I had written 1073741824. Now consumed. I extended the fix to the duration helper, which had the same defect less visibly — it divided by 1000 and 60000. It now consumes seconds_per_minute() and a new milliseconds_per_second() added beside its siblings in that authority (there was no ms-per-second row; adding it there rather than locally is the anti-fork direction). The one number I kept local is the ninety-second point where the sentence switches from seconds to minutes — that is a display judgement, not a unit, and it is now a named row saying so.

This finding is worth its own sentence: a unit authority forked inside a formatting helper is easy to miss precisely because it reads as arithmetic rather than as modelling.

2. Run summary collapsed Refused onto Failed. Confirmed and the sharpest of the three. A failures-only run rendered with the refused glyph — undoing at the very last line what the outcome sum spends the whole model establishing, in a PR whose stated point is that those two are distinct. Now: any failure dominates the glyph (breakage is the stronger claim about a run), refusals keep their own glyph, and both counts stay in the text so the glyph chooses emphasis without hiding a number. w_run_summary_keeps_refused_and_failed_apart covers all four cases and carries a RED — re-pointing the failure arm at StatusRefused reds it.

3. Unavailable duration silently omitted. Confirmed, and this one contradicted my own observation_measured_note, which says an absent measurement never prints a zero and never omits the field "because a silently omitted number is the same fabrication one layer up". The renderer did exactly that. Concluded lines now read (duration unmeasured: <cause>). The reasoning I wrote into the fix: a reader who sees no duration assumes nobody timed it; a reader who sees the cause knows why.

Also in this commit, independent of the review: P1 itself — the CI-log renderer with its flagship acceptance. The fixture is run 30044816605's real log rather than a reconstruction; its t=33m heartbeat carried current=16107200512 swap=34359738368 psi_some_avg10=9.01 and named no subject while the process sat inside v2.compiler.normalized_tree for 606984ms, disclosed only at walk end. Re-rendered through the escalation law, the same window names the module at T and the memory-reclaim cause at 2T. The three REDs the ruling asks for are proven by perturbation: planted silent phase, orphaned Begin, and a Refused placed inside a collapsed group.

P2 (TTY renderer) and P3 (census wall + lens) are still to come in this PR per the atomic ruling, so please keep reviewing it as incomplete until those land.

Suite green: 31 model + 6 lockstep + 18 renderer conjuncts. Compile-clean unchanged at 47 pre-existing errors in std/measure.dag and std/effect_grant.dag, zero attributable here.