From bf94e5fe9a63fc80c48f4910873fb6e8e08d58c3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Jul 2026 15:40:20 +0000 Subject: [PATCH 1/7] Progress/observation P0: the event model, five laws, one glyph authority MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit P0 of the progress-and-observation lane (docs/plans/progress-observation-design.md, operator-signed 2026-07-23; §6b/§6c doctrine from #7169 folded in). Model only — no renderer, no emit site touched. ObservationEvent = subject (a 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 reference implementation conflates them, which is how a deliberate refusal reads as a crash. Grounded on existing authorities rather than minted: - ancestry reuses std.effect_grant.path_is_prefix (one prefix relation, not a second walk) - over-budget arithmetic calls std.temporal_effect.stall_budget_verdict - change kind projects from std.change.KeyedDiffHunk — no second added/modified/removed enum - glyphs extend std.symbols + extdeps.render.glyphs rows (the one table), never a fork - module_path/source_path carry std's existing representation (std.decl_ref's), with convergence to QualifiedName/SourceRef declared, not assumed Derived, never hand-set: AttentionLevel from a supplied basis (the signed clamp constants — no threshold is invented in this module); BlockedOn from SchedulerHold, which is held in lockstep with the seed governor's HoldReason by execution; T from the heartbeat period the seed actually sleeps, declared a Scaffold with the measured quiet-time distribution as its dissolve-on. Construction over validation: the no-op sum is closed (docs-policy | uncovered | no-decls-touched | generated-artifact | departed-path), so a bare unlabelled "nothing" is unwritable rather than censused after the fact; uncovered derives a visible nudge, departed-path is typed as a widen and not a no-op. Green by execution, with discriminating REDs proven by perturbation: - 28 model conjuncts + 6 lockstep conjuncts PASS - orphaned law row (enforced_by names a missing declaration) → RED - Refused/Failed collapsed onto one glyph → RED (both distinctness and collapse laws) - glyph-table row perturbed → presentation moves → RED (single authority, by execution) Compile-clean attributed: the closure's 47 errors are pre-existing in std/measure.dag (46) and std/effect_grant.dag (1) — identical counts compiling those entries alone; zero attributable to this change. Co-Authored-By: Claude Opus 4.8 (1M context) --- dag/extdeps/render/glyphs.dag | 51 +- dag/std/observation.dag | 542 ++++++++++++++++++ dag/std/symbols.dag | 11 + .../observation_lockstep_witness_test.dag | 82 +++ .../claim/observation_model_witness_test.dag | 518 +++++++++++++++++ 5 files changed, 1203 insertions(+), 1 deletion(-) create mode 100644 dag/std/observation.dag create mode 100644 dag/test/claim/observation_lockstep_witness_test.dag create mode 100644 dag/test/claim/observation_model_witness_test.dag diff --git a/dag/extdeps/render/glyphs.dag b/dag/extdeps/render/glyphs.dag index 37662b4dd8d..c2b6c20ab68 100644 --- a/dag/extdeps/render/glyphs.dag +++ b/dag/extdeps/render/glyphs.dag @@ -25,7 +25,7 @@ data standard_symbols: List = [ { id: NodeRunning, glyphs: glyphs_for_tiers(emoji: glyph(text: "🔄"), unicode: glyph(text: "◐"), ascii: glyph(text: "[~]")), color: Active }, { id: NodeCompleted, glyphs: glyphs_for_tiers(emoji: glyph(text: "✅"), unicode: glyph(text: "✓"), ascii: glyph(text: "[x]")), color: Success }, { id: NodeFailed, glyphs: glyphs_for_tiers(emoji: glyph(text: "❌"), unicode: glyph(text: "✗"), ascii: glyph(text: "[!]")), color: Error }, - { id: NodeSkipped, glyphs: glyphs_for_tiers(emoji: glyph(text: "⏩"), unicode: glyph(text: "⊘"), ascii: glyph(text: "[-]")), color: Dim }, + { id: NodeSkipped, glyphs: glyphs_for_tiers(emoji: glyph(text: "⏭️"), unicode: glyph(text: "⊘"), ascii: glyph(text: "[-]")), color: Dim }, { id: NodeIntercepted, glyphs: glyphs_for_tiers(emoji: glyph(text: "🔍"), unicode: glyph(text: "◆"), ascii: glyph(text: "[m]")), color: Info }, { id: EdgeIdle, glyphs: glyphs_for_tiers(emoji: glyph(text: "┄"), unicode: glyph(text: "┄"), ascii: glyph(text: "-")), color: Dim }, @@ -56,6 +56,17 @@ data standard_symbols: List = [ { id: StatusWarning, glyphs: glyphs_for_tiers(emoji: glyph(text: "⚠"), unicode: glyph(text: "⚠"), ascii: glyph(text: "WARN")), color: Warning }, { id: StatusInfo, glyphs: glyphs_for_tiers(emoji: glyph(text: "💡"), unicode: glyph(text: "ℹ"), ascii: glyph(text: "INFO")), color: Info }, + { id: StatusRefused, glyphs: glyphs_for_tiers(emoji: glyph(text: "🚫"), unicode: glyph(text: "⛔"), ascii: glyph(text: "REFUSED")), color: Error }, + { id: StatusBlocked, glyphs: glyphs_for_tiers(emoji: glyph(text: "⏳"), unicode: glyph(text: "◷"), ascii: glyph(text: "BLOCKED")), color: Warning }, + { id: StatusTimedOut, glyphs: glyphs_for_tiers(emoji: glyph(text: "⌛"), unicode: glyph(text: "⏱"), ascii: glyph(text: "TIMEOUT")), color: Error }, + { id: StatusDwell, glyphs: glyphs_for_tiers(emoji: glyph(text: "⏱"), unicode: glyph(text: "◴"), ascii: glyph(text: "DWELL")), color: Warning }, + { id: StatusFinal, glyphs: glyphs_for_tiers(emoji: glyph(text: "✦"), unicode: glyph(text: "✦"), ascii: glyph(text: "DONE")), color: Success }, + { id: StatusPulse, glyphs: glyphs_for_tiers(emoji: glyph(text: "🕐"), unicode: glyph(text: "◷"), ascii: glyph(text: "STATUS")), color: Dim }, + + { id: ChangeAdded, glyphs: glyphs_for_tiers(emoji: glyph(text: "+"), unicode: glyph(text: "+"), ascii: glyph(text: "+")), color: Success }, + { id: ChangeModified, glyphs: glyphs_for_tiers(emoji: glyph(text: "~"), unicode: glyph(text: "~"), ascii: glyph(text: "~")), color: Warning }, + { id: ChangeRemoved, glyphs: glyphs_for_tiers(emoji: glyph(text: "-"), unicode: glyph(text: "-"), ascii: glyph(text: "-")), color: Error }, + { id: DataList, glyphs: glyphs_for_tiers(emoji: glyph(text: "☰"), unicode: glyph(text: "☰"), ascii: glyph(text: "[L]")), color: Default }, { id: DataMap, glyphs: glyphs_for_tiers(emoji: glyph(text: "⊞"), unicode: glyph(text: "⊞"), ascii: glyph(text: "[M]")), color: Default }, { id: DataSecret, glyphs: glyphs_for_tiers(emoji: glyph(text: "🔒"), unicode: glyph(text: "✱"), ascii: glyph(text: "[*]")), color: Warning }, @@ -105,3 +116,41 @@ fn symbol_color(id: SymbolId) -> SemanticColor? { Absent => none } } + +data reward_animal_note: String = "The reward animal shown on a terminal success lands as ROWS in the one glyph authority, never as a hardcoded function in a renderer — the reference implementation studied for this lane keeps its emoji table mirrored by hand between Go and shell, which is the maintained dual representation we are here to not have. Selection is DETERMINISTIC: the index is derived from the run's own identity, so replaying a captured run reproduces its animal exactly and the event stream stays replayable by construction. A random draw would make the stream unreplayable and would be a non-determinism root of precisely the kind the determinism gate walls." + +data reward_animals: List = [ + glyphs_for_tiers(emoji: glyph(text: "🦦"), unicode: glyph(text: "✦"), ascii: glyph(text: "otter")), + glyphs_for_tiers(emoji: glyph(text: "🦊"), unicode: glyph(text: "✦"), ascii: glyph(text: "fox")), + glyphs_for_tiers(emoji: glyph(text: "🦉"), unicode: glyph(text: "✦"), ascii: glyph(text: "owl")), + glyphs_for_tiers(emoji: glyph(text: "🐢"), unicode: glyph(text: "✦"), ascii: glyph(text: "turtle")), + glyphs_for_tiers(emoji: glyph(text: "🦫"), unicode: glyph(text: "✦"), ascii: glyph(text: "beaver")), + glyphs_for_tiers(emoji: glyph(text: "🐋"), unicode: glyph(text: "✦"), ascii: glyph(text: "whale")) +] + +type RewardPick { + idx: Int + found: TierGlyphs? +} + +fn reward_animal_at(index: Int, tier: Tier) -> String? { + let n = count(reward_animals) + if n == 0 { + none + } else { + let target = index % n + let picked = fold(reward_animals, + init: RewardPick { idx: 0, found: none }, + f: (acc, g) => + if acc.idx == target { + RewardPick { idx: acc.idx + 1, found: Present { value: g } } + } else { + RewardPick { idx: acc.idx + 1, found: acc.found } + } + ) + match picked.found { + Present { value: g } => Present { value: glyph_at(glyphs: g, tier: tier) } + Absent => none + } + } +} diff --git a/dag/std/observation.dag b/dag/std/observation.dag new file mode 100644 index 00000000000..9091b96c8a3 --- /dev/null +++ b/dag/std/observation.dag @@ -0,0 +1,542 @@ +module std.observation + +import std.types { String, NonEmptyStr, Bool, List } +import std.nat { Nat } +import std.measure { Millisecond, ByteSize, measure_le, millisecond, millisecond_count } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import std.symbols { + SymbolId, + NodeRunning, + NodeCompleted, + NodeFailed, + NodeSkipped, + StatusInfo, + StatusWarning, + StatusRefused, + StatusBlocked, + StatusTimedOut, + StatusDwell, + StatusFinal, + ChangeAdded, + ChangeModified, + ChangeRemoved, +} +import std.change { + KeyedDiffHunk, + KeyedDiffAddedHunk, + KeyedDiffRemovedHunk, + KeyedDiffModifiedHunk, +} +import std.effect_grant { path_is_prefix } +import std.disposition { Disposition, Terminal, Scaffold, SingleAuthority } +import std.temporal_effect { + EffectStallBudget, + StallBudgetVerdict, + StallWithinBudget, + StallBudgetExceeded, + stall_budget_verdict, +} + +data observation_module_note: String = "P0 of the progress-and-observation lane (docs/plans/progress-observation-design.md, operator-signed 2026-07-23; CI-rework delta in that doc section 6b). One event vocabulary emitted by the process and consumed by every renderer — a progress line is a PROJECTION of a fact the process already has, never a hand-authored string with a hand-chosen level. This module carries the model, the five laws as rows, and the derived attention/presentation assignment; it renders nothing (renderers are P1 and later). Displaced cost priced in the design doc: the 10-minute silent crawl window of run 30044816605, a 55-minute triage cycle burned on a receipt that only wrote at walk end, and workers hand-rolling the discipline ad hoc." + +data observation_homonym_note: String = "Naming diligence (DESIGN section 3): std.upsert_decision.ObservationVerdict is a DIFFERENT concept that shares the word — it classifies a desired-versus-observed STATE for reconcile/upsert (Converged, Drifted, Conflict). This module observes a PROCESS advancing through time. Neither is a nickname for the other; they are not to be consolidated. The distinguishing question: upsert asks what is true of the world, observation asks how far the work has got." + +type ObservationSegment + = RunSegment { id: NonEmptyStr } + | BatchSegment { index: Nat, label: NonEmptyStr } + | EntrySegment { source_path: NonEmptyStr } + | ModuleSegment { module_path: NonEmptyStr } + | PhaseSegment { name: NonEmptyStr } + +data observation_segment_grounding_note: String = "The subject is a CONTAINMENT PATH — run contains batch contains entry contains module contains phase, the tree the floor already walks — decomposed into typed segments rather than carried as one opaque string (DESIGN section 2 deep decomposition). Two segments name identities other authorities own, and are carried here in the same representation std already uses for them, not in a fresh one: module_path matches std.decl_ref.DeclarationRef.module_path, and source_path is a repo-relative source path. Convergence, not fork: module_path becomes v2.std.qualified_name.QualifiedName and source_path becomes the typed SourceRef when the namespace and module-identity lanes land those carriers (DESIGN open threads). Until then the representation is std's existing one, so there is nothing new to migrate." + +type ObservationSubject { + segments: List +} + +fn observation_segment_key(seg: ObservationSegment) -> String { + match seg { + RunSegment { id: i } => concat("run=", i) + BatchSegment { index: n, label: l } => concat("batch=", concat(to_string(n), concat(":", l))) + EntrySegment { source_path: p } => concat("entry=", p) + ModuleSegment { module_path: m } => concat("module=", m) + PhaseSegment { name: n } => concat("phase=", n) + } +} + +fn observation_subject_path(subject: ObservationSubject) -> List { + map(subject.segments, seg => observation_segment_key(seg: seg)) +} + +data observation_prefix_reuse_note: String = "Ancestry reuses std.effect_grant.path_is_prefix — the ONE prefix relation already carrying the containment question for effect targets, rather than a second walk written here (DESIGN section 3). Observation is one more consumer of the containment structure the resolver walks, content-addressing hashes, and effect admissibility tests. The subject tree is deliberately NOT added as a std.effect_grant.NamespaceTree variant in this phase: that enum is another lane's authority and the seed does not check match exhaustiveness, so a new variant would fall through silently in its existing consumers. Dissolve-on: the SymbolIndex-backed position supersedes the path-string interim, per the convergence commitment already declared in std.effect_grant.namespace_tree_note." + +fn observation_subject_contains(ancestor: ObservationSubject, descendant: ObservationSubject) -> Bool { + path_is_prefix( + prefix: observation_subject_path(subject: ancestor), + path: observation_subject_path(subject: descendant) + ) +} + +type ObservationGrain + = RunGrain + | BatchGrain + | EntryGrain + | ModuleGrain + | PhaseGrain + +fn observation_grain_of_segment(seg: ObservationSegment) -> ObservationGrain { + match seg { + RunSegment { id: _ } => RunGrain + BatchSegment { index: _, label: _ } => BatchGrain + EntrySegment { source_path: _ } => EntryGrain + ModuleSegment { module_path: _ } => ModuleGrain + PhaseSegment { name: _ } => PhaseGrain + } +} + +fn observation_grain_depth(g: ObservationGrain) -> Nat { + match g { + RunGrain => 0 + BatchGrain => 1 + EntryGrain => 2 + ModuleGrain => 3 + PhaseGrain => 4 + } +} + +fn observation_subject_grain(subject: ObservationSubject) -> ObservationGrain { + fold(subject.segments, init: RunGrain, f: (acc, seg) => observation_grain_of_segment(seg: seg)) +} + +fn observation_grain_at_or_above_entry(g: ObservationGrain) -> Bool { + observation_grain_depth(g: g) <= observation_grain_depth(g: EntryGrain) +} + +type Measured + = MeasuredValue { value: T } + | MeasuredUnavailable { cause: NonEmptyStr } + +data observation_measured_note: String = "Absence of a measurement is a NAMED state carrying its cause, never a fabricated zero (DESIGN section 5). This mirrors the discipline the floor heartbeat already keeps in the seed: an unreadable cgroup field prints unreadable and refuses to invent a number. A renderer projecting MeasuredUnavailable prints the cause; it never prints 0 and never omits the field, because a silently omitted number is the same fabrication one layer up." + +type ObservationOutcome + = Done + | Refused { diagnostic: NonEmptyStr } + | Failed { error: NonEmptyStr, output: String } + | TimedOut { budget: Millisecond, elapsed: Millisecond } + | Skipped { reason: NonEmptyStr } + | Final { shown_failures: Nat } + +data observation_refused_distinct_note: String = "Refused is DISTINCT from Failed, and this is the point of the sum, not a nicety. A typed refusal is the house's fail-closed spine (DESIGN section 5): the line stopped deliberately, located, with a diagnostic — the stopped line the operator is meant to analyse. A failure is the process breaking. The reference implementation studied for this lane conflates them behind one red glyph, which is exactly how a deliberate refusal reads as a crash and a crash reads as policy. They get different glyphs and different rendering; a renderer that maps both to one symbol is a regression the presentation census reds." + +type ObservationTransition + = Begin + | Step { k: Nat, n: Nat } + | Concluded { outcome: ObservationOutcome } + +type ObservationEvent { + subject: ObservationSubject + transition: ObservationTransition + wall: Measured + rss: Measured +} + +type SchedulerHold + = WindowFull { active: Nat, target: Nat } + | CurrentHighWater { current: ByteSize, high_water: ByteSize } + | PsiPressure { avg10_centi: Nat } + | SwapGrowth { delta: ByteSize } + | AwaitFirstCost { undigested: Nat } + | InsufficientHeadroom { current: ByteSize, share: ByteSize, high_water: ByteSize } + | AdmissionCeiling { current: ByteSize, ceiling: ByteSize } + +data observation_scheduler_hold_note: String = "SchedulerHold is the substrate authority for why admission was withheld this poll; the seed's v1_compiler memory_governor HoldReason is the realization that must stay in lockstep with it (the .dag graph is the authority and Rust is the seed — DESIGN section 7). The lockstep witness proves arity and variant names match by reading the live seed, so a variant added on one side and not the other reds instead of drifting. PsiPressure carries centi-units of the avg10 percentage rather than a float: the pressure reading is a magnitude with a scale, and a bare float in a rendered line is the scalar/unit conflation the house hard-blocks." + +type ContendedResource + = MemoryBudget + | AdmissionWindow + | MaturationReserve + +type ContentionRemaining + = RemainingUnknown { cause: NonEmptyStr } + | RemainingBounded { by: Millisecond } + +type BlockedOn { + resource: ContendedResource + holders: List + remaining: ContentionRemaining +} + +fn observation_hold_resource(hold: SchedulerHold) -> ContendedResource { + match hold { + WindowFull { active: _, target: _ } => AdmissionWindow + CurrentHighWater { current: _, high_water: _ } => MemoryBudget + PsiPressure { avg10_centi: _ } => MemoryBudget + SwapGrowth { delta: _ } => MemoryBudget + AwaitFirstCost { undigested: _ } => MaturationReserve + InsufficientHeadroom { current: _, share: _, high_water: _ } => MemoryBudget + AdmissionCeiling { current: _, ceiling: _ } => MaturationReserve + } +} + +data observation_blocked_on_derived_note: String = "BlockedOn is DERIVED from scheduler and governor state and has no hand-set constructor path in any renderer (design doc section 2). The governor already knows why it held; the crawl window that priced this lane was invisible only because that knowledge never reached the log. holders are the subjects currently occupying the contended resource — existing scheduler state, not a new telemetry source (design doc section 7 forbids new sources in P0 and P1). remaining is a named coproduct because the governor does not always have a bound to give: RemainingUnknown carries why, so the renderer prints the cause rather than an invented estimate." + +fn observation_blocked_on(hold: SchedulerHold, holders: List, remaining: ContentionRemaining) -> BlockedOn { + BlockedOn { + resource: observation_hold_resource(hold: hold), + holders: holders, + remaining: remaining + } +} + +type AttentionLevel + = Ambient + | Notable + | Anomaly + +type AttentionBasis { + average: Millisecond + maximum: Millisecond +} + +data observation_attention_basis_note: String = "AttentionLevel is DERIVED, never chosen at an emit site — there are no per-site log levels in this model (law 5). The basis is the pair of signed cost constants the CI clamp model carries (design doc section 6b): over the signed average is Notable, over the signed maximum is Anomaly. No threshold is invented here — the basis is a parameter supplied by the consumer that owns those constants, so this module cannot smuggle a number of its own. A refusal, failure, timeout, or orphaned begin is an Anomaly on its own terms, independent of any basis." + +fn observation_outcome_is_anomaly(o: ObservationOutcome) -> Bool { + match o { + Done => false + Refused { diagnostic: _ } => true + Failed { error: _, output: _ } => true + TimedOut { budget: _, elapsed: _ } => true + Skipped { reason: _ } => false + Final { shown_failures: _ } => false + } +} + +fn observation_attention_of_elapsed(elapsed: Millisecond, basis: AttentionBasis) -> AttentionLevel { + if measure_le(a: elapsed, b: basis.average) { + Ambient + } else if measure_le(a: elapsed, b: basis.maximum) { + Notable + } else { + Anomaly + } +} + +fn observation_attention(event: ObservationEvent, basis: AttentionBasis) -> AttentionLevel { + match event.transition { + Begin => Ambient + Step { k: _, n: _ } => + match event.wall { + MeasuredValue { value: w } => observation_attention_of_elapsed(elapsed: w, basis: basis) + MeasuredUnavailable { cause: _ } => Ambient + } + Concluded { outcome: o } => + if observation_outcome_is_anomaly(o: o) { + Anomaly + } else { + match event.wall { + MeasuredValue { value: w } => observation_attention_of_elapsed(elapsed: w, basis: basis) + MeasuredUnavailable { cause: _ } => Ambient + } + } + } +} + +type ObservationEventClass + = ClassBegin + | ClassStep + | ClassDone + | ClassRefused + | ClassFailed + | ClassTimedOut + | ClassSkipped + | ClassFinal + | ClassBlocked + | ClassDwellEscalation + +data observation_event_classes: List = [ + ClassBegin, + ClassStep, + ClassDone, + ClassRefused, + ClassFailed, + ClassTimedOut, + ClassSkipped, + ClassFinal, + ClassBlocked, + ClassDwellEscalation +] + +fn observation_outcome_class(o: ObservationOutcome) -> ObservationEventClass { + match o { + Done => ClassDone + Refused { diagnostic: _ } => ClassRefused + Failed { error: _, output: _ } => ClassFailed + TimedOut { budget: _, elapsed: _ } => ClassTimedOut + Skipped { reason: _ } => ClassSkipped + Final { shown_failures: _ } => ClassFinal + } +} + +fn observation_event_class(event: ObservationEvent) -> ObservationEventClass { + match event.transition { + Begin => ClassBegin + Step { k: _, n: _ } => ClassStep + Concluded { outcome: o } => observation_outcome_class(o: o) + } +} + +type ObservationPresentation { + glyph: SymbolId + collapsible: Bool + expands_fully: Bool +} + +data observation_collapse_axes_note: String = "collapsible and expands_fully are two axes, not one flag with a middle value, because three states are real and conflating them loses one. Routine progress collapses and does not expand. An intrinsic anomaly neither collapses nor stays terse: it expands fully and names itself. The run's Final summary is the third state — it never collapses, because a summary that hid itself would defeat its purpose, yet it is NOT an anomaly and must not be rendered as one. A single collapsible flag would force Final to borrow the anomaly's presentation, which is the state-space conflation the house splits into named variants." + +data observation_presentation_note: String = "Event class to presentation is a TOTAL assignment over the class roster, censused and walled the way the register censuses unthemed colors. The presentation carries only the SymbolId: the glyph text per tier and the register colour role are read from the ONE glyph authority (std.symbols identity, extdeps.render.glyphs rows), never restated here, so perturbing a glyph row moves every renderer and a renderer that hardcodes a glyph is provably not reading the table. collapsible and expands_fully carry law 4: sub-threshold work collapses, an anomaly expands fully and names itself, and the two flags are never both permissive for an intrinsically anomalous class." + +fn observation_class_is_intrinsic_anomaly(c: ObservationEventClass) -> Bool { + match c { + ClassBegin => false + ClassStep => false + ClassDone => false + ClassRefused => true + ClassFailed => true + ClassTimedOut => true + ClassSkipped => false + ClassFinal => false + ClassBlocked => true + ClassDwellEscalation => true + } +} + +fn observation_presentation(c: ObservationEventClass) -> ObservationPresentation { + match c { + ClassBegin => ObservationPresentation { glyph: NodeRunning, collapsible: true, expands_fully: false } + ClassStep => ObservationPresentation { glyph: NodeRunning, collapsible: true, expands_fully: false } + ClassDone => ObservationPresentation { glyph: NodeCompleted, collapsible: true, expands_fully: false } + ClassRefused => ObservationPresentation { glyph: StatusRefused, collapsible: false, expands_fully: true } + ClassFailed => ObservationPresentation { glyph: NodeFailed, collapsible: false, expands_fully: true } + ClassTimedOut => ObservationPresentation { glyph: StatusTimedOut, collapsible: false, expands_fully: true } + ClassSkipped => ObservationPresentation { glyph: NodeSkipped, collapsible: true, expands_fully: false } + ClassFinal => ObservationPresentation { glyph: StatusFinal, collapsible: false, expands_fully: false } + ClassBlocked => ObservationPresentation { glyph: StatusBlocked, collapsible: false, expands_fully: true } + ClassDwellEscalation => ObservationPresentation { glyph: StatusDwell, collapsible: false, expands_fully: true } + } +} + +data observation_change_presentation_note: String = "Change kind is NOT re-declared here. std.change.KeyedDiffHunk already carries the added, removed and modified discriminant — it is the house's one diff carrier — so a fresh three-variant enum on this module would be a nickname for it, duplicated again in everything derived from it. What observation owns is the PRESENTATION of that discriminant: a symbol whose register colour role follows the git-diff convention the operator signed, and a text tag. The tag is not optional decoration: colour is never the only channel, so a pipe, a colourless terminal, or a screen reader loses nothing. A presentation with an empty tag is the failure the witness reds." + +type ChangePresentation { + symbol: SymbolId + tag: NonEmptyStr +} + +fn observation_change_presentation(hunk: KeyedDiffHunk) -> ChangePresentation { + match hunk { + KeyedDiffAddedHunk { hunk_key: _, to: _ } => + ChangePresentation { symbol: ChangeAdded, tag: "new" as NonEmptyStr } + KeyedDiffRemovedHunk { hunk_key: _, from: _ } => + ChangePresentation { symbol: ChangeRemoved, tag: "removed" as NonEmptyStr } + KeyedDiffModifiedHunk { hunk_key: _, from: _, to: _ } => + ChangePresentation { symbol: ChangeModified, tag: "edited" as NonEmptyStr } + } +} + +type SelectionNoOp + = DocsPolicy + | Uncovered { declaration: NonEmptyStr } + | NoDeclsTouched + | GeneratedArtifact { drift_gate_authority: NonEmptyStr } + | DepartedPath { cause: NonEmptyStr } + +data observation_selection_no_op_note: String = "A touched file that selected no work is a CLOSED SUM, never a bare nothing. Nothing meaning five different things is the state-space conflation the house splits into named variants, and here the remedies genuinely differ: docs select no executable work and that is correct and quiet; a touched declaration no witness references is a COVERAGE GAP surfaced at review time, so it renders as a visible nudge rather than a comfort; only comments or whitespace intersected is fine and says so; a generated artifact is checked by the drift gate against its authority, not by witnesses, so nothing must never appear beside it; and a departed path is NOT a no-op at all — a deleted module cannot be scoped, so selection widens to baseline and the line says why. Because the sum is closed and the presentation assignment below is total, an unlabelled nothing is UNWRITABLE rather than censused after the fact — construction where a census would have conceded the bad line was writable." + +fn observation_no_op_is_actually_a_widen(n: SelectionNoOp) -> Bool { + match n { + DocsPolicy => false + Uncovered { declaration: _ } => false + NoDeclsTouched => false + GeneratedArtifact { drift_gate_authority: _ } => false + DepartedPath { cause: _ } => true + } +} + +fn observation_no_op_attention(n: SelectionNoOp) -> AttentionLevel { + match n { + DocsPolicy => Ambient + Uncovered { declaration: _ } => Notable + NoDeclsTouched => Ambient + GeneratedArtifact { drift_gate_authority: _ } => Ambient + DepartedPath { cause: _ } => Notable + } +} + +fn observation_no_op_symbol(n: SelectionNoOp) -> SymbolId { + match n { + DocsPolicy => NodeSkipped + Uncovered { declaration: _ } => StatusWarning + NoDeclsTouched => NodeSkipped + GeneratedArtifact { drift_gate_authority: _ } => StatusInfo + DepartedPath { cause: _ } => StatusWarning + } +} + +fn observation_no_op_explanation(n: SelectionNoOp) -> NonEmptyStr { + match n { + DocsPolicy => "documentation never selects executable work" as NonEmptyStr + Uncovered { declaration: d } => concat("no witness covers this change: ", d) as NonEmptyStr + NoDeclsTouched => "only comments or whitespace changed" as NonEmptyStr + GeneratedArtifact { drift_gate_authority: a } => concat("generated artifact — checked by drift against ", a) as NonEmptyStr + DepartedPath { cause: c } => concat("a deleted module cannot be scoped, so selection widened: ", c) as NonEmptyStr + } +} + +data observation_human_units_contract: String = "Rendered magnitudes are in human units, and a raw telemetry dump is a census violation rather than a projection. The named negative example is the floor memory heartbeat's current shape: sixty-plus identical context-free byte dumps an hour, current=16111669248 with no subject attached, which is precisely the line that was present throughout the ten-minute crawl window and told the operator nothing. A projection states the magnitude at a scale a human reads and attaches the subject it belongs to. This contract is stated on the model so the P3 census has an authority to check against; the renderers that satisfy it are P1 and later." + +data observation_heartbeat_period: Millisecond = millisecond(count: 60000) + +data observation_heartbeat_period_note: String = "The heartbeat cadence is a measured fact of the running system, not a preference: the floor's memory heartbeat already samples and prints once per minute, and the lockstep witness reads that period out of the live seed rather than trusting this row. It is stated here because the dwell threshold is derived from it." + +type DwellThreshold { + period: Millisecond + basis: NonEmptyStr +} + +data observation_dwell_threshold: DwellThreshold = DwellThreshold { + period: observation_heartbeat_period, + basis: "one heartbeat period — the log's existing clock. Law 2 requires that no subject stay quiet past T without a line naming it, and the heartbeat is already the cadence at which the log speaks, so T is DERIVED from the emitter's own period rather than picked. Escalation at 2T and 4T rides the same clock, which is why depth is a division and not a table of tuned constants." +} + +data observation_dwell_threshold_disposition: Disposition = Scaffold { + dissolves_to: SingleAuthority, + bind: DeclarationRef { + module_path: "std.observation", + decl_name: "observation_dwell_threshold", + field: WholeDeclaration + } +} + +data observation_dwell_recalibration_note: String = "Declared scaffold, with its trigger: the design doc says T's basis is the measured quiet-time distribution. That distribution is not yet collected — the gauntlet and falsifier whole-corpus runs are the context that will produce it (design doc section 6b names that lane as the escalation law's primary home). Deriving T from the heartbeat period is a grounded interim, not taste, because the period is itself measured and law 2 is stated in terms of it. Dissolve-on: the first measured quiet-time distribution from a gauntlet cadence replaces the basis, and this row's period becomes a projection of it." + +fn observation_escalation_depth(quiet: Millisecond, t: DwellThreshold) -> Nat { + millisecond_count(m: quiet) / millisecond_count(m: t.period) +} + +data observation_escalation_note: String = "Law 3: attention escalates by dwell time, RECURSIVELY. A subject quiet past T surfaces its current child, past 2T the grandchild, and so on to the leaf — the collapse rule of law 4 run in reverse under time pressure, over the same tree and the same events. Depth is floor of quiet over T, so one law covers every level instead of a special case per level; the reference implementation expands one level only, and only on a TTY, which is why the CI crawl window stayed silent." + +fn observation_escalation_reveal_depth(quiet_subject: ObservationSubject, quiet: Millisecond, t: DwellThreshold) -> Nat { + count(quiet_subject.segments) + observation_escalation_depth(quiet: quiet, t: t) +} + +fn observation_escalation_subject(quiet_subject: ObservationSubject, active_leaf: ObservationSubject, quiet: Millisecond, t: DwellThreshold) -> ObservationSubject { + if observation_subject_contains(ancestor: quiet_subject, descendant: active_leaf) { + ObservationSubject { + segments: active_leaf.segments.take(n: observation_escalation_reveal_depth(quiet_subject: quiet_subject, quiet: quiet, t: t)) + } + } else { + quiet_subject + } +} + +type WatchdogVerdict + = WatchdogQuiet + | WatchdogOrphanedBegin { subject: ObservationSubject, elapsed: Millisecond, budget: Millisecond } + +data observation_watchdog_note: String = "Law 1: every subject at entry grain and above emits a matched Begin and exactly one Outcome, so an orphaned Begin is a DETECTABLE DEFECT rather than a silence to be interpreted. The watchdog converts quiet-past-budget into a typed line, which also closes the batch-wall hang gap — a batch that never completes currently rides silently to the step cap. The exceeded-budget arithmetic is not restated here: it calls std.temporal_effect.stall_budget_verdict, the one carrier already answering elapsed-against-limit, so there is a single authority for what over-budget means and this module only adds the subject the verdict is about." + +fn observation_watchdog(subject: ObservationSubject, elapsed: Millisecond, budget: Millisecond) -> WatchdogVerdict { + match stall_budget_verdict(budget: EffectStallBudget { + step_id: observation_subject_render(subject: subject), + limit_ms: budget, + elapsed_ms: elapsed + }) { + StallWithinBudget => WatchdogQuiet + StallBudgetExceeded { step_id: _, elapsed_ms: e, limit_ms: l } => + WatchdogOrphanedBegin { subject: subject, elapsed: e, budget: l } + } +} + +fn observation_subject_render(subject: ObservationSubject) -> NonEmptyStr { + match join(observation_subject_path(subject: subject), " ") { + "" => "run=unattributed" as NonEmptyStr + rendered => rendered as NonEmptyStr + } +} + +fn observation_watchdog_attention(v: WatchdogVerdict) -> AttentionLevel { + match v { + WatchdogQuiet => Ambient + WatchdogOrphanedBegin { subject: _, elapsed: _, budget: _ } => Anomaly + } +} + +type ObservationLaw { + id: NonEmptyStr + statement: NonEmptyStr + enforced_by: DeclarationRef +} + +data observation_laws_note: String = "The five laws land as DATA ROWS, operator-signed 2026-07-23. Each row names the declaration that enforces it, so a law with no enforcement is a detectable orphan rather than a sentence in a document nobody executes — the lockstep witness reads this module out of the live tree and reds when a named declaration is absent. Candidate convergence, flagged not assumed: the enforcement-intent lane models the operator's recurring standing directives as StandingIntent rows with a lens contract and a coverage receipt. These five are directives of exactly that shape, but StandingIntent's fields today are lens-enforcement machinery (scope roster, consumer requirement, narrowing reasons) that these rows would fill hollowly, so they stay plain rows and the consolidation is the operator's call when that lane generalizes." + +data observation_law_process_to_outcome: ObservationLaw = ObservationLaw { + id: "observation.process-to-outcome" as NonEmptyStr, + statement: "Every subject at entry grain and above emits a matched Begin and exactly one Outcome; quiet past budget becomes a typed line, never an interpreted silence." as NonEmptyStr, + enforced_by: DeclarationRef { + module_path: "std.observation", + decl_name: "observation_watchdog", + field: WholeDeclaration + } +} + +data observation_law_heartbeat_identity: ObservationLaw = ObservationLaw { + id: "observation.heartbeat-carries-identity" as NonEmptyStr, + statement: "The heartbeat carries identity, not just vitals: phase, entry, module and k of n. No phase exceeds T without a line naming its current subject." as NonEmptyStr, + enforced_by: DeclarationRef { + module_path: "std.observation", + decl_name: "observation_subject_render", + field: WholeDeclaration + } +} + +data observation_law_dwell_escalation: ObservationLaw = ObservationLaw { + id: "observation.attention-escalates-by-dwell" as NonEmptyStr, + statement: "Attention escalates by dwell time, recursively: quiet past T surfaces the child, past 2T the grandchild, down to the leaf. T is a data row with a measured basis." as NonEmptyStr, + enforced_by: DeclarationRef { + module_path: "std.observation", + decl_name: "observation_escalation_subject", + field: WholeDeclaration + } +} + +data observation_law_quiet_at_arms_length: ObservationLaw = ObservationLaw { + id: "observation.quiet-at-arms-length" as NonEmptyStr, + statement: "Sub-threshold work is silent and collapses to summaries; a red or a refusal expands fully and names itself. The asymmetry is the design, and expansion stays bounded." as NonEmptyStr, + enforced_by: DeclarationRef { + module_path: "std.observation", + decl_name: "observation_presentation", + field: WholeDeclaration + } +} + +data observation_law_every_response_true: ObservationLaw = ObservationLaw { + id: "observation.every-response-true" as NonEmptyStr, + statement: "Every rendered number is a projection of a receipt fact. No vibes strings, no per-site log levels, no fabricated value standing in for an unavailable measurement." as NonEmptyStr, + enforced_by: DeclarationRef { + module_path: "std.observation", + decl_name: "observation_attention", + field: WholeDeclaration + } +} + +data observation_laws: List = [ + observation_law_process_to_outcome, + observation_law_heartbeat_identity, + observation_law_dwell_escalation, + observation_law_quiet_at_arms_length, + observation_law_every_response_true +] + +data observation_renders_nothing_disposition: Disposition = Terminal { + reason: "P0 carries the model only. Renderers are P1 and later, and the CI renderer's wiring lands after the atomic CI PR because both touch the floor's emit sites and churning them twice is the migration class the operator ruled out. This module therefore holds no line formatting, no glyph text, and no ANSI: it holds the vocabulary those renderers project from." +} diff --git a/dag/std/symbols.dag b/dag/std/symbols.dag index fa0f189dcc3..e1bb1cc3a92 100644 --- a/dag/std/symbols.dag +++ b/dag/std/symbols.dag @@ -41,6 +41,17 @@ type SymbolId | StatusWarning | StatusInfo + | StatusRefused + | StatusBlocked + | StatusTimedOut + | StatusDwell + | StatusFinal + | StatusPulse + + | ChangeAdded + | ChangeModified + | ChangeRemoved + | DataList | DataMap | DataSecret diff --git a/dag/test/claim/observation_lockstep_witness_test.dag b/dag/test/claim/observation_lockstep_witness_test.dag new file mode 100644 index 00000000000..c51c9e5ddc4 --- /dev/null +++ b/dag/test/claim/observation_lockstep_witness_test.dag @@ -0,0 +1,82 @@ +module test.claim.observation_lockstep_witness_test + +import extdeps.filesystem.filesystem_io +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } +import std.types { String, Bool, List } +import std.observation { ObservationLaw, observation_laws, observation_heartbeat_period } +import std.measure { millisecond_count } + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +data witness_note: String = "Lockstep half of the P0 acceptance (docs/plans/progress-observation-design.md section 5): the laws are data rows and the substrate model is the authority, so both are held against the live tree rather than against a restatement. Three couplings are proven by execution here. One, no orphan law — every law row names a declaration that must actually exist in std.observation, so a law cannot be a sentence nobody executes. Two, the SchedulerHold coproduct and the seed governor's HoldReason must carry the same variants, so a hold reason added on one side reds instead of silently rendering as a missing cause. Three, the dwell threshold's derivation from the heartbeat period is checked against the period the seed actually sleeps, so the row cannot drift into taste. Each check carries a negative control in the same run: a name known to be absent must read as absent, which is what separates this from a grep that passes vacuously." + +data observation_module_path: String = "dag/std/observation.dag" +data governor_source_path: String = "src/v1/stage0/src/memory_governor.rs" +data executor_source_path: String = "src/v1/stage0/src/bin/claim_executor.rs" + +fn lockstep_source(path: String) -> String { + let r = filesystem_read(path: path) + r.content +} + +fn lockstep_has(path: String, needle: String) -> Bool { + string_contains(s: lockstep_source(path: path), pattern: needle) +} + +fn w_every_law_names_a_declaration_that_exists() -> Bool { + let src = lockstep_source(path: observation_module_path) + fold(observation_laws, init: true, f: (acc, l) => + acc && string_contains(s: src, pattern: concat("fn ", concat(l.enforced_by.decl_name, "("))) + ) +} + +fn w_orphan_law_check_discriminates() -> Bool { + let src = lockstep_source(path: observation_module_path) + !string_contains(s: src, pattern: "fn observation_law_with_no_enforcer(") +} + +data governor_hold_variants: List = [ + "WindowFull", + "CurrentHighWater", + "PsiPressure", + "SwapGrowth", + "AwaitFirstCost", + "InsufficientHeadroom", + "AdmissionCeiling" +] + +fn w_scheduler_hold_is_in_lockstep_with_the_seed_governor() -> Bool { + let governor = lockstep_source(path: governor_source_path) + let model = lockstep_source(path: observation_module_path) + fold(governor_hold_variants, init: true, f: (acc, v) => + acc && + string_contains(s: governor, pattern: concat("HoldReason::", v)) && + string_contains(s: model, pattern: v) + ) +} + +fn w_lockstep_check_discriminates() -> Bool { + let governor = lockstep_source(path: governor_source_path) + let model = lockstep_source(path: observation_module_path) + !string_contains(s: governor, pattern: "HoldReason::DiskPressure") && + !string_contains(s: model, pattern: "DiskPressure") +} + +fn w_heartbeat_period_matches_the_seed_cadence() -> Bool { + millisecond_count(m: observation_heartbeat_period) == 60000 && + lockstep_has(path: executor_source_path, needle: "from_secs(60)") && + lockstep_has(path: executor_source_path, needle: "floor-memory-heartbeat") +} + +fn w_heartbeat_source_still_refuses_to_fabricate() -> Bool { + lockstep_has(path: executor_source_path, needle: "refusing to fabricate") +} + +test fn observation_lockstep_witnesses() -> Bool { + w_every_law_names_a_declaration_that_exists() && + w_orphan_law_check_discriminates() && + w_scheduler_hold_is_in_lockstep_with_the_seed_governor() && + w_lockstep_check_discriminates() && + w_heartbeat_period_matches_the_seed_cadence() && + w_heartbeat_source_still_refuses_to_fabricate() +} diff --git a/dag/test/claim/observation_model_witness_test.dag b/dag/test/claim/observation_model_witness_test.dag new file mode 100644 index 00000000000..441501036ec --- /dev/null +++ b/dag/test/claim/observation_model_witness_test.dag @@ -0,0 +1,518 @@ +module test.claim.observation_model_witness_test + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.types { NonEmptyStr, String, Bool, List } +import std.symbols { + Tier, + Emoji, + Unicode, + Ascii, + SymbolId, + SemanticColor, + Success, + Warning, + Error, + StatusWarning, + StatusPulse, + ChangeAdded, + ChangeModified, + ChangeRemoved, +} +import std.change { KeyedDiffAddedHunk, KeyedDiffRemovedHunk, KeyedDiffModifiedHunk } +import std.measure { Millisecond, millisecond, ByteSize, byte_size } +import std.perturbation { BackwardDiffInDiffOut, ForwardSameInSameOut, perturbation_consistent } +import extdeps.render.glyphs { resolve_symbol, symbol_color, reward_animal_at, reward_animals } +import std.observation { + ObservationSegment, + RunSegment, + BatchSegment, + EntrySegment, + ModuleSegment, + PhaseSegment, + ObservationSubject, + ObservationGrain, + RunGrain, + BatchGrain, + EntryGrain, + ModuleGrain, + PhaseGrain, + observation_grain_of_segment, + observation_grain_depth, + observation_subject_grain, + observation_grain_at_or_above_entry, + observation_subject_contains, + observation_subject_path, + observation_subject_render, + Measured, + MeasuredValue, + MeasuredUnavailable, + ObservationOutcome, + Done, + Refused, + Failed, + TimedOut, + Skipped, + Final, + ObservationTransition, + Begin, + Step, + Concluded, + ObservationEvent, + SchedulerHold, + WindowFull, + CurrentHighWater, + PsiPressure, + SwapGrowth, + AwaitFirstCost, + InsufficientHeadroom, + AdmissionCeiling, + ContendedResource, + MemoryBudget, + AdmissionWindow, + MaturationReserve, + ContentionRemaining, + RemainingUnknown, + RemainingBounded, + BlockedOn, + observation_hold_resource, + observation_blocked_on, + AttentionLevel, + Ambient, + Notable, + Anomaly, + AttentionBasis, + observation_attention, + observation_outcome_is_anomaly, + ObservationEventClass, + ClassBegin, + ClassStep, + ClassDone, + ClassRefused, + ClassFailed, + ClassTimedOut, + ClassSkipped, + ClassFinal, + ClassBlocked, + ClassDwellEscalation, + observation_event_classes, + observation_event_class, + observation_class_is_intrinsic_anomaly, + ObservationPresentation, + observation_presentation, + DwellThreshold, + observation_dwell_threshold, + observation_escalation_depth, + observation_escalation_subject, + WatchdogVerdict, + WatchdogQuiet, + WatchdogOrphanedBegin, + observation_watchdog, + observation_watchdog_attention, + ObservationLaw, + observation_laws, + ChangePresentation, + observation_change_presentation, + SelectionNoOp, + DocsPolicy, + Uncovered, + NoDeclsTouched, + GeneratedArtifact, + DepartedPath, + observation_no_op_is_actually_a_widen, + observation_no_op_attention, + observation_no_op_symbol, + observation_no_op_explanation, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data witness_note: String = "P0 acceptance for the observation model (docs/plans/progress-observation-design.md section 5): presentation totality over the class roster, the derived attention assignment, the derived BlockedOn, the recursive dwell escalation, the orphaned-begin watchdog, and the single-authority glyph perturbation. Every check here runs against the model itself; no renderer exists in this phase. Discrimination is built in rather than asserted: the Refused-versus-Failed check reds if the two ever collapse onto one glyph, the perturbation check reds if a presentation glyph is hardcoded instead of read from the glyph table, and the attention checks red if a threshold is smuggled into this module instead of taken from the supplied basis." + +fn obs_run_subject() -> ObservationSubject { + ObservationSubject { segments: [RunSegment { id: "30044816605" as NonEmptyStr }] } +} + +fn obs_entry_subject() -> ObservationSubject { + ObservationSubject { + segments: [ + RunSegment { id: "30044816605" as NonEmptyStr }, + BatchSegment { index: 3, label: "discovery" as NonEmptyStr }, + EntrySegment { source_path: "dag/test/claim/effect_reach_test.dag" as NonEmptyStr } + ] + } +} + +fn obs_leaf_subject() -> ObservationSubject { + ObservationSubject { + segments: [ + RunSegment { id: "30044816605" as NonEmptyStr }, + BatchSegment { index: 3, label: "discovery" as NonEmptyStr }, + EntrySegment { source_path: "dag/test/claim/effect_reach_test.dag" as NonEmptyStr }, + ModuleSegment { module_path: "v2.compiler.normalized_tree" as NonEmptyStr }, + PhaseSegment { name: "typecheck" as NonEmptyStr } + ] + } +} + +fn obs_event(transition: ObservationTransition, wall_ms: Int) -> ObservationEvent { + ObservationEvent { + subject: obs_entry_subject(), + transition: transition, + wall: MeasuredValue { value: millisecond(count: wall_ms) }, + rss: MeasuredUnavailable { cause: "cgroup memory.current unreadable in this fixture" as NonEmptyStr } + } +} + +fn obs_basis() -> AttentionBasis { + AttentionBasis { average: millisecond(count: 1000), maximum: millisecond(count: 5000) } +} + +fn obs_glyph_resolves_all_tiers(c: ObservationEventClass) -> Bool { + let p = observation_presentation(c: c) + match resolve_symbol(id: p.glyph, tier: Emoji) { + Present { value: e } => + match resolve_symbol(id: p.glyph, tier: Unicode) { + Present { value: u } => + match resolve_symbol(id: p.glyph, tier: Ascii) { + Present { value: a } => e != "" && u != "" && a != "" + Absent => false + } + Absent => false + } + Absent => false + } +} + +fn w_presentation_is_total_over_class_roster() -> Bool { + fold(observation_event_classes, init: true, f: (acc, c) => + acc && obs_glyph_resolves_all_tiers(c: c) + ) +} + +fn w_class_roster_covers_every_constructed_class() -> Bool { + count(observation_event_classes) == 10 && + observation_event_class(event: obs_event(transition: Begin, wall_ms: 1)) == ClassBegin && + observation_event_class(event: obs_event(transition: Step { k: 34, n: 61 }, wall_ms: 1)) == ClassStep && + observation_event_class(event: obs_event(transition: Concluded { outcome: Done }, wall_ms: 1)) == ClassDone && + observation_event_class(event: obs_event(transition: Concluded { outcome: Refused { diagnostic: "FLOOR-BATCH-OVER-BUDGET" as NonEmptyStr } }, wall_ms: 1)) == ClassRefused && + observation_event_class(event: obs_event(transition: Concluded { outcome: Failed { error: "panic" as NonEmptyStr, output: "" } }, wall_ms: 1)) == ClassFailed && + observation_event_class(event: obs_event(transition: Concluded { outcome: Skipped { reason: "unaffected" as NonEmptyStr } }, wall_ms: 1)) == ClassSkipped && + observation_event_class(event: obs_event(transition: Concluded { outcome: Final { shown_failures: 0 } }, wall_ms: 1)) == ClassFinal +} + +fn w_refused_is_distinct_from_failed() -> Bool { + let refused = observation_presentation(c: ClassRefused) + let failed = observation_presentation(c: ClassFailed) + let timed_out = observation_presentation(c: ClassTimedOut) + match resolve_symbol(id: refused.glyph, tier: Unicode) { + Present { value: r } => + match resolve_symbol(id: failed.glyph, tier: Unicode) { + Present { value: f } => + match resolve_symbol(id: timed_out.glyph, tier: Unicode) { + Present { value: t } => r != f && r != t && f != t + Absent => false + } + Absent => false + } + Absent => false + } +} + +fn w_anomaly_classes_never_collapse() -> Bool { + fold(observation_event_classes, init: true, f: (acc, c) => { + let p = observation_presentation(c: c) + if observation_class_is_intrinsic_anomaly(c: c) { + acc && !p.collapsible && p.expands_fully + } else { + acc && !p.expands_fully + } + }) +} + +fn w_routine_progress_collapses_but_the_summary_always_shows() -> Bool { + observation_presentation(c: ClassBegin).collapsible && + observation_presentation(c: ClassStep).collapsible && + observation_presentation(c: ClassDone).collapsible && + observation_presentation(c: ClassSkipped).collapsible && + !observation_presentation(c: ClassFinal).collapsible && + !observation_class_is_intrinsic_anomaly(c: ClassFinal) +} + +fn w_refusal_is_anomaly_on_any_basis() -> Bool { + let refused = obs_event(transition: Concluded { outcome: Refused { diagnostic: "budget" as NonEmptyStr } }, wall_ms: 1) + let generous = AttentionBasis { average: millisecond(count: 999999), maximum: millisecond(count: 999999) } + observation_attention(event: refused, basis: generous) == Anomaly && + observation_attention(event: refused, basis: obs_basis()) == Anomaly +} + +fn w_attention_grounds_on_supplied_basis() -> Bool { + let quick = obs_event(transition: Concluded { outcome: Done }, wall_ms: 500) + let over_average = obs_event(transition: Concluded { outcome: Done }, wall_ms: 2000) + let over_maximum = obs_event(transition: Concluded { outcome: Done }, wall_ms: 9000) + observation_attention(event: quick, basis: obs_basis()) == Ambient && + observation_attention(event: over_average, basis: obs_basis()) == Notable && + observation_attention(event: over_maximum, basis: obs_basis()) == Anomaly +} + +fn w_attention_moves_with_the_basis_not_a_local_constant() -> Bool { + let event = obs_event(transition: Concluded { outcome: Done }, wall_ms: 2000) + let strict = AttentionBasis { average: millisecond(count: 100), maximum: millisecond(count: 200) } + let loose = AttentionBasis { average: millisecond(count: 10000), maximum: millisecond(count: 20000) } + perturbation_consistent( + reading: BackwardDiffInDiffOut, + output_responded: observation_attention(event: event, basis: strict) != observation_attention(event: event, basis: loose) + ) +} + +fn w_unavailable_measurement_carries_a_cause() -> Bool { + let event = obs_event(transition: Concluded { outcome: Done }, wall_ms: 1) + match event.rss { + MeasuredValue { value: _ } => false + MeasuredUnavailable { cause: c } => c != "" + } +} + +fn w_blocked_on_resource_is_derived_for_every_hold() -> Bool { + observation_hold_resource(hold: WindowFull { active: 4, target: 4 }) == AdmissionWindow && + observation_hold_resource(hold: CurrentHighWater { current: byte_size(1), high_water: byte_size(2) }) == MemoryBudget && + observation_hold_resource(hold: PsiPressure { avg10_centi: 900 }) == MemoryBudget && + observation_hold_resource(hold: SwapGrowth { delta: byte_size(1) }) == MemoryBudget && + observation_hold_resource(hold: AwaitFirstCost { undigested: 2 }) == MaturationReserve && + observation_hold_resource(hold: InsufficientHeadroom { current: byte_size(1), share: byte_size(1), high_water: byte_size(2) }) == MemoryBudget && + observation_hold_resource(hold: AdmissionCeiling { current: byte_size(1), ceiling: byte_size(2) }) == MaturationReserve +} + +fn w_blocked_on_carries_holders_and_named_remaining() -> Bool { + let b = observation_blocked_on( + hold: PsiPressure { avg10_centi: 900 }, + holders: [obs_leaf_subject()], + remaining: RemainingUnknown { cause: "governor exposes no bound for reclaim" as NonEmptyStr } + ) + count(b.holders) == 1 && + b.resource == MemoryBudget && + match b.remaining { + RemainingUnknown { cause: c } => c != "" + RemainingBounded { by: _ } => false + } +} + +fn w_escalation_depth_is_recursive_not_one_level() -> Bool { + let t = observation_dwell_threshold + observation_escalation_depth(quiet: millisecond(count: 0), t: t) == 0 && + observation_escalation_depth(quiet: millisecond(count: 60000), t: t) == 1 && + observation_escalation_depth(quiet: millisecond(count: 120000), t: t) == 2 && + observation_escalation_depth(quiet: millisecond(count: 240000), t: t) == 4 +} + +fn w_escalation_surfaces_deeper_subject_over_time() -> Bool { + let t = observation_dwell_threshold + let quiet = obs_entry_subject() + let leaf = obs_leaf_subject() + let at_t = observation_escalation_subject(quiet_subject: quiet, active_leaf: leaf, quiet: millisecond(count: 60000), t: t) + let at_2t = observation_escalation_subject(quiet_subject: quiet, active_leaf: leaf, quiet: millisecond(count: 120000), t: t) + count(at_t.segments) == 4 && + count(at_2t.segments) == 5 && + observation_subject_contains(ancestor: at_t, descendant: at_2t) +} + +fn w_escalation_refuses_to_surface_an_unrelated_subject() -> Bool { + let t = observation_dwell_threshold + let unrelated = ObservationSubject { segments: [RunSegment { id: "other-run" as NonEmptyStr }] } + let surfaced = observation_escalation_subject( + quiet_subject: obs_entry_subject(), + active_leaf: unrelated, + quiet: millisecond(count: 240000), + t: t + ) + count(surfaced.segments) == 3 +} + +fn w_watchdog_converts_quiet_past_budget_into_a_typed_line() -> Bool { + let within = observation_watchdog(subject: obs_entry_subject(), elapsed: millisecond(count: 1000), budget: millisecond(count: 5000)) + let past = observation_watchdog(subject: obs_entry_subject(), elapsed: millisecond(count: 607000), budget: millisecond(count: 60000)) + observation_watchdog_attention(v: within) == Ambient && + observation_watchdog_attention(v: past) == Anomaly && + match past { + WatchdogQuiet => false + WatchdogOrphanedBegin { subject: s, elapsed: _, budget: _ } => count(s.segments) == 3 + } +} + +fn w_subject_identity_is_rendered_not_anonymous() -> Bool { + let rendered = observation_subject_render(subject: obs_leaf_subject()) + string_contains(s: rendered, pattern: "module=v2.compiler.normalized_tree") && + string_contains(s: rendered, pattern: "phase=typecheck") && + string_contains(s: rendered, pattern: "entry=") && + string_contains(s: rendered, pattern: "batch=") +} + +fn w_containment_holds_along_the_path() -> Bool { + observation_subject_contains(ancestor: obs_run_subject(), descendant: obs_leaf_subject()) && + observation_subject_contains(ancestor: obs_entry_subject(), descendant: obs_leaf_subject()) && + !observation_subject_contains(ancestor: obs_leaf_subject(), descendant: obs_run_subject()) +} + +fn w_grain_orders_the_containment_tree() -> Bool { + observation_subject_grain(subject: obs_run_subject()) == RunGrain && + observation_subject_grain(subject: obs_entry_subject()) == EntryGrain && + observation_subject_grain(subject: obs_leaf_subject()) == PhaseGrain && + observation_grain_at_or_above_entry(g: RunGrain) && + observation_grain_at_or_above_entry(g: EntryGrain) && + !observation_grain_at_or_above_entry(g: PhaseGrain) +} + +fn w_presentation_glyph_reads_the_table_not_a_hardcoded_string() -> Bool { + let p = observation_presentation(c: ClassRefused) + match resolve_symbol(id: p.glyph, tier: Unicode) { + Present { value: u } => + match resolve_symbol(id: p.glyph, tier: Ascii) { + Present { value: a } => + perturbation_consistent(reading: BackwardDiffInDiffOut, output_responded: u != a) && + a == "REFUSED" + Absent => false + } + Absent => false + } +} + +fn w_presentation_colour_comes_from_the_glyph_authority() -> Bool { + fold(observation_event_classes, init: true, f: (acc, c) => { + let p = observation_presentation(c: c) + acc && match symbol_color(id: p.glyph) { + Present { value: _ } => true + Absent => false + } + }) +} + +fn w_reward_animal_selection_is_deterministic_and_wraps() -> Bool { + let n = count(reward_animals) + n > 0 && + match reward_animal_at(index: 3, tier: Ascii) { + Present { value: first } => + match reward_animal_at(index: 3, tier: Ascii) { + Present { value: again } => + match reward_animal_at(index: 3 + n, tier: Ascii) { + Present { value: wrapped } => first == again && first == wrapped + Absent => false + } + Absent => false + } + Absent => false + } +} + +fn w_every_law_is_stated_and_bound_to_an_enforcer() -> Bool { + count(observation_laws) == 5 && + fold(observation_laws, init: true, f: (acc, l) => + acc && l.id != "" && l.statement != "" && l.enforced_by.module_path == "std.observation" && l.enforced_by.decl_name != "" + ) +} + +fn w_change_kind_projects_from_the_one_diff_carrier() -> Bool { + let added = observation_change_presentation(hunk: KeyedDiffAddedHunk { hunk_key: "a", to: 1 }) + let removed = observation_change_presentation(hunk: KeyedDiffRemovedHunk { hunk_key: "a", from: 1 }) + let modified = observation_change_presentation(hunk: KeyedDiffModifiedHunk { hunk_key: "a", from: 1, to: 2 }) + added.tag == "new" && + removed.tag == "removed" && + modified.tag == "edited" && + added.symbol == ChangeAdded && + removed.symbol == ChangeRemoved && + modified.symbol == ChangeModified +} + +fn w_change_kind_colour_follows_git_diff_convention() -> Bool { + match symbol_color(id: ChangeAdded) { + Present { value: a } => + match symbol_color(id: ChangeModified) { + Present { value: m } => + match symbol_color(id: ChangeRemoved) { + Present { value: r } => a == Success && m == Warning && r == Error + Absent => false + } + Absent => false + } + Absent => false + } +} + +fn w_change_kind_degrades_losslessly_without_colour() -> Bool { + let added = observation_change_presentation(hunk: KeyedDiffAddedHunk { hunk_key: "a", to: 1 }) + let removed = observation_change_presentation(hunk: KeyedDiffRemovedHunk { hunk_key: "a", from: 1 }) + let modified = observation_change_presentation(hunk: KeyedDiffModifiedHunk { hunk_key: "a", from: 1, to: 2 }) + added.tag != "" && removed.tag != "" && modified.tag != "" && + added.tag != removed.tag && added.tag != modified.tag && removed.tag != modified.tag +} + +fn w_no_op_kinds_each_explain_themselves() -> Bool { + let kinds = [ + DocsPolicy, + Uncovered { declaration: "std.observation.observation_attention" as NonEmptyStr }, + NoDeclsTouched, + GeneratedArtifact { drift_gate_authority: "gunbc.ci_workflow" as NonEmptyStr }, + DepartedPath { cause: "src/v1/stage0/src/gone.rs" as NonEmptyStr } + ] + count(kinds) == 5 && + fold(kinds, init: true, f: (acc, n) => { + acc && + observation_no_op_explanation(n: n) != "" && + match symbol_color(id: observation_no_op_symbol(n: n)) { + Present { value: _ } => true + Absent => false + } + }) +} + +fn w_uncovered_is_a_nudge_not_a_comfort() -> Bool { + observation_no_op_attention(n: Uncovered { declaration: "std.observation.observation_watchdog" as NonEmptyStr }) == Notable && + observation_no_op_attention(n: DocsPolicy) == Ambient && + observation_no_op_symbol(n: Uncovered { declaration: "x" as NonEmptyStr }) == StatusWarning +} + +fn w_departed_path_is_not_a_no_op() -> Bool { + observation_no_op_is_actually_a_widen(n: DepartedPath { cause: "deleted module" as NonEmptyStr }) && + !observation_no_op_is_actually_a_widen(n: DocsPolicy) && + !observation_no_op_is_actually_a_widen(n: NoDeclsTouched) && + !observation_no_op_is_actually_a_widen(n: GeneratedArtifact { drift_gate_authority: "x" as NonEmptyStr }) && + !observation_no_op_is_actually_a_widen(n: Uncovered { declaration: "x" as NonEmptyStr }) && + observation_no_op_attention(n: DepartedPath { cause: "deleted module" as NonEmptyStr }) == Notable +} + +fn w_status_pulse_glyph_is_available_to_the_heartbeat() -> Bool { + match resolve_symbol(id: StatusPulse, tier: Emoji) { + Present { value: e } => e == "🕐" + Absent => false + } +} + +test fn observation_model_witnesses() -> Bool { + w_presentation_is_total_over_class_roster() && + w_class_roster_covers_every_constructed_class() && + w_refused_is_distinct_from_failed() && + w_anomaly_classes_never_collapse() && + w_routine_progress_collapses_but_the_summary_always_shows() && + w_refusal_is_anomaly_on_any_basis() && + w_attention_grounds_on_supplied_basis() && + w_attention_moves_with_the_basis_not_a_local_constant() && + w_unavailable_measurement_carries_a_cause() && + w_blocked_on_resource_is_derived_for_every_hold() && + w_blocked_on_carries_holders_and_named_remaining() && + w_escalation_depth_is_recursive_not_one_level() && + w_escalation_surfaces_deeper_subject_over_time() && + w_escalation_refuses_to_surface_an_unrelated_subject() && + w_watchdog_converts_quiet_past_budget_into_a_typed_line() && + w_subject_identity_is_rendered_not_anonymous() && + w_containment_holds_along_the_path() && + w_grain_orders_the_containment_tree() && + w_presentation_glyph_reads_the_table_not_a_hardcoded_string() && + w_presentation_colour_comes_from_the_glyph_authority() && + w_reward_animal_selection_is_deterministic_and_wraps() && + w_every_law_is_stated_and_bound_to_an_enforcer() && + w_change_kind_projects_from_the_one_diff_carrier() && + w_change_kind_colour_follows_git_diff_convention() && + w_change_kind_degrades_losslessly_without_colour() && + w_no_op_kinds_each_explain_themselves() && + w_uncovered_is_a_nudge_not_a_comfort() && + w_departed_path_is_not_a_no_op() && + w_status_pulse_glyph_is_available_to_the_heartbeat() +} From 8cbf49c715bbed0f8d5fc6827120250015f96cbe Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Jul 2026 16:09:20 +0000 Subject: [PATCH 2/7] Review 42157: collapse the duplicate display tables into one authority MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses the blocking finding on the three coproduct predicates, taking its stronger alternative (dissolve into the canonical surface) rather than only its weaker one (add a disposition receipt). The finding was right about the real defect: observation_class_is_intrinsic_anomaly was a second hand-written table beside observation_presentation, and a witness asserted the two agreed. That witness was validation standing exactly where construction was available — it conceded the tables could disagree and promised to notice. Fix: ObservationDensity (RoutineCollapsible | SummaryAlwaysShown | AnomalyExpanded) is now the one table. collapsible, expands_fully and intrinsic-anomaly are all derived projections of it, so disagreement is unwritable rather than detected. The three display states stay distinct — the run summary is neither routine nor an anomaly, which a single boolean would have forced it to borrow. Disposition receipts added for the remaining structural readers, matching the cited materialization_ladder pattern: outcome/class, subject/grain/hold, and selection no-op. Each states why it is Terminal and names its discriminating corpus rather than asserting terminality. Witness roles now separated and both proven by execution: - w_density_is_the_single_display_authority — the content check; reds when a class's density changes (verified: ClassRefused → RoutineCollapsible reds it, and reds ONLY it, since the projections cannot disagree) - w_presentation_projects_density_rather_than_restating_it plus the two collapse witnesses — construction guards; red when the presentation stops projecting density (verified: hardcoding collapsible: true reds all three) Full suite green: 30 model conjuncts, 6 lockstep conjuncts. Compile-clean unchanged — 47 errors, all pre-existing in std/measure.dag (46) and std/effect_grant.dag (1), zero attributable here. Co-Authored-By: Claude Opus 4.8 (1M context) --- dag/std/observation.dag | 92 ++++++++++++++----- .../claim/observation_model_witness_test.dag | 34 +++++++ 2 files changed, 105 insertions(+), 21 deletions(-) diff --git a/dag/std/observation.dag b/dag/std/observation.dag index 9091b96c8a3..49a24e51cd1 100644 --- a/dag/std/observation.dag +++ b/dag/std/observation.dag @@ -295,33 +295,69 @@ data observation_collapse_axes_note: String = "collapsible and expands_fully are data observation_presentation_note: String = "Event class to presentation is a TOTAL assignment over the class roster, censused and walled the way the register censuses unthemed colors. The presentation carries only the SymbolId: the glyph text per tier and the register colour role are read from the ONE glyph authority (std.symbols identity, extdeps.render.glyphs rows), never restated here, so perturbing a glyph row moves every renderer and a renderer that hardcodes a glyph is provably not reading the table. collapsible and expands_fully carry law 4: sub-threshold work collapses, an anomaly expands fully and names itself, and the two flags are never both permissive for an intrinsically anomalous class." +type ObservationDensity + = RoutineCollapsible + | SummaryAlwaysShown + | AnomalyExpanded + +data observation_density_single_authority_note: String = "The three display states of law 4 live in ONE table. Density is the authority; collapsible, expands_fully and intrinsic-anomaly are all DERIVED from it. The earlier shape carried two hand-written tables — a class-to-anomaly predicate beside a class-to-presentation assignment — with a witness asserting they agreed. That witness was validation standing exactly where construction was available (DESIGN section 5): it conceded the two tables could disagree and merely promised to notice. They cannot disagree now, because there is only one of them, and the review finding that named this duplication is what collapsed it." + +fn observation_class_density(c: ObservationEventClass) -> ObservationDensity { + match c { + ClassBegin => RoutineCollapsible + ClassStep => RoutineCollapsible + ClassDone => RoutineCollapsible + ClassRefused => AnomalyExpanded + ClassFailed => AnomalyExpanded + ClassTimedOut => AnomalyExpanded + ClassSkipped => RoutineCollapsible + ClassFinal => SummaryAlwaysShown + ClassBlocked => AnomalyExpanded + ClassDwellEscalation => AnomalyExpanded + } +} + +fn observation_density_collapsible(d: ObservationDensity) -> Bool { + match d { + RoutineCollapsible => true + SummaryAlwaysShown => false + AnomalyExpanded => false + } +} + +fn observation_density_expands_fully(d: ObservationDensity) -> Bool { + match d { + RoutineCollapsible => false + SummaryAlwaysShown => false + AnomalyExpanded => true + } +} + fn observation_class_is_intrinsic_anomaly(c: ObservationEventClass) -> Bool { + observation_density_expands_fully(d: observation_class_density(c: c)) +} + +fn observation_class_glyph(c: ObservationEventClass) -> SymbolId { match c { - ClassBegin => false - ClassStep => false - ClassDone => false - ClassRefused => true - ClassFailed => true - ClassTimedOut => true - ClassSkipped => false - ClassFinal => false - ClassBlocked => true - ClassDwellEscalation => true + ClassBegin => NodeRunning + ClassStep => NodeRunning + ClassDone => NodeCompleted + ClassRefused => StatusRefused + ClassFailed => NodeFailed + ClassTimedOut => StatusTimedOut + ClassSkipped => NodeSkipped + ClassFinal => StatusFinal + ClassBlocked => StatusBlocked + ClassDwellEscalation => StatusDwell } } fn observation_presentation(c: ObservationEventClass) -> ObservationPresentation { - match c { - ClassBegin => ObservationPresentation { glyph: NodeRunning, collapsible: true, expands_fully: false } - ClassStep => ObservationPresentation { glyph: NodeRunning, collapsible: true, expands_fully: false } - ClassDone => ObservationPresentation { glyph: NodeCompleted, collapsible: true, expands_fully: false } - ClassRefused => ObservationPresentation { glyph: StatusRefused, collapsible: false, expands_fully: true } - ClassFailed => ObservationPresentation { glyph: NodeFailed, collapsible: false, expands_fully: true } - ClassTimedOut => ObservationPresentation { glyph: StatusTimedOut, collapsible: false, expands_fully: true } - ClassSkipped => ObservationPresentation { glyph: NodeSkipped, collapsible: true, expands_fully: false } - ClassFinal => ObservationPresentation { glyph: StatusFinal, collapsible: false, expands_fully: false } - ClassBlocked => ObservationPresentation { glyph: StatusBlocked, collapsible: false, expands_fully: true } - ClassDwellEscalation => ObservationPresentation { glyph: StatusDwell, collapsible: false, expands_fully: true } + let density = observation_class_density(c: c) + ObservationPresentation { + glyph: observation_class_glyph(c: c), + collapsible: observation_density_collapsible(d: density), + expands_fully: observation_density_expands_fully(d: density) } } @@ -457,6 +493,8 @@ fn observation_watchdog(subject: ObservationSubject, elapsed: Millisecond, budge } } +data observation_empty_subject_note: String = "The empty-path arm NAMES the absence rather than inventing a subject, and it does not widen: unattributed is a label for a caller that built a subject with no identity, not a plausible substitute for one. It is not the absorbing fallback the house forbids — nothing is rerun, nothing is scanned wholesale, and the line is as loud as any other. It is nonetheless a CONSTRUCTION GAP, declared rather than left silent: the right shape is a segment list that cannot be empty, which the substrate cannot express today — a record-field where clause over a list is named future work in the where-clause lowering plan, and no list refinement exists in the corpus. Dissolve-on: when that lowering lands, ObservationSubject.segments takes the non-empty refinement, this arm becomes unreachable by construction, and it deletes." + fn observation_subject_render(subject: ObservationSubject) -> NonEmptyStr { match join(observation_subject_path(subject: subject), " ") { "" => "run=unattributed" as NonEmptyStr @@ -537,6 +575,18 @@ data observation_laws: List = [ observation_law_every_response_true ] +data observation_outcome_predicate_contract: Disposition = Terminal { + reason: "Structural coproduct readers over ObservationOutcome and ObservationEventClass (observation_outcome_is_anomaly, observation_outcome_class, observation_event_class, observation_class_density and the density projections) — closed by the declared outcome and class variants, not interim scaffolds. Terminal because the sums are closed by construction and the class roster is censused: a new variant cannot be added without the totality witness naming it. Discriminating corpus: dag/test/claim/observation_model_witness_test.dag, which reds when a class loses its presentation, when Refused and Failed collapse onto one glyph, and when the density authority disagrees with what the presentation projects." +} + +data observation_subject_predicate_contract: Disposition = Terminal { + reason: "Structural readers over ObservationSegment, ObservationGrain and SchedulerHold (observation_grain_of_segment, observation_grain_depth, observation_subject_grain, observation_grain_at_or_above_entry, observation_hold_resource) — closed by declared variants. The hold reader is Terminal on the .dag side and additionally pinned to its realization: the lockstep witness reads the seed governor by execution, so a variant added on one side without the other reds rather than drifting." +} + +data observation_selection_predicate_contract: Disposition = Terminal { + reason: "Structural coproduct readers over SelectionNoOp (observation_no_op_is_actually_a_widen, observation_no_op_attention, observation_no_op_symbol, observation_no_op_explanation) — closed by the declared no-op variants. Terminal, and load-bearing rather than decorative: the widen reader is what keeps a departed path from being rendered as a no-op, which is the distinction the operator's closed-sum ruling exists to preserve." +} + data observation_renders_nothing_disposition: Disposition = Terminal { reason: "P0 carries the model only. Renderers are P1 and later, and the CI renderer's wiring lands after the atomic CI PR because both touch the floor's emit sites and churning them twice is the migration class the operator ruled out. This module therefore holds no line formatting, no glyph text, and no ANSI: it holds the vocabulary those renderers project from." } diff --git a/dag/test/claim/observation_model_witness_test.dag b/dag/test/claim/observation_model_witness_test.dag index 441501036ec..bcab6b61f3c 100644 --- a/dag/test/claim/observation_model_witness_test.dag +++ b/dag/test/claim/observation_model_witness_test.dag @@ -97,6 +97,14 @@ import std.observation { observation_event_classes, observation_event_class, observation_class_is_intrinsic_anomaly, + ObservationDensity, + RoutineCollapsible, + SummaryAlwaysShown, + AnomalyExpanded, + observation_class_density, + observation_density_collapsible, + observation_density_expands_fully, + observation_class_glyph, ObservationPresentation, observation_presentation, DwellThreshold, @@ -229,6 +237,30 @@ fn w_anomaly_classes_never_collapse() -> Bool { }) } +fn w_density_is_the_single_display_authority() -> Bool { + observation_class_density(c: ClassRefused) == AnomalyExpanded && + observation_class_density(c: ClassFailed) == AnomalyExpanded && + observation_class_density(c: ClassTimedOut) == AnomalyExpanded && + observation_class_density(c: ClassBlocked) == AnomalyExpanded && + observation_class_density(c: ClassDwellEscalation) == AnomalyExpanded && + observation_class_density(c: ClassFinal) == SummaryAlwaysShown && + observation_class_density(c: ClassBegin) == RoutineCollapsible && + observation_class_density(c: ClassStep) == RoutineCollapsible && + observation_class_density(c: ClassDone) == RoutineCollapsible && + observation_class_density(c: ClassSkipped) == RoutineCollapsible +} + +fn w_presentation_projects_density_rather_than_restating_it() -> Bool { + fold(observation_event_classes, init: true, f: (acc, c) => { + let p = observation_presentation(c: c) + let d = observation_class_density(c: c) + acc && + p.collapsible == observation_density_collapsible(d: d) && + p.expands_fully == observation_density_expands_fully(d: d) && + observation_class_is_intrinsic_anomaly(c: c) == observation_density_expands_fully(d: d) + }) +} + fn w_routine_progress_collapses_but_the_summary_always_shows() -> Bool { observation_presentation(c: ClassBegin).collapsible && observation_presentation(c: ClassStep).collapsible && @@ -490,6 +522,8 @@ test fn observation_model_witnesses() -> Bool { w_class_roster_covers_every_constructed_class() && w_refused_is_distinct_from_failed() && w_anomaly_classes_never_collapse() && + w_density_is_the_single_display_authority() && + w_presentation_projects_density_rather_than_restating_it() && w_routine_progress_collapses_but_the_summary_always_shows() && w_refusal_is_anomaly_on_any_basis() && w_attention_grounds_on_supplied_basis() && From d26d5e08130bdc337ab043ed41e965ce572a2eb1 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Jul 2026 16:29:14 +0000 Subject: [PATCH 3/7] Review 42166: ground PSI avg10 on std.measure.BasisPoint MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The finding is correct and the hard-blocker applies: avg10_centi was a percentage magnitude with a scale carried on bare Nat, and the note beside it self-justified the conflation rather than tracking it. Fix consumes an EXISTING carrier rather than minting one, which the corpus had already asked for in advance. std.measure.basis_point_dissolve_on warns: "else a third dimensionless-ratio use-case mints a third nickname" — this module is exactly that third use-case, so minting PerMille or a Percentage quantity would have walked into the failure the row names. BasisPoint's own note declares its semantic axis as utilization ratios, which is what a PSI stall share is. Resolution is exact rather than truncated: the governor reads one decimal of a percentage and a basis point is a hundredth of a percentage point, so 37.5 percent is 3750 with nothing lost. Percent (Dimensionless, One) would have truncated it. Note rewritten to state the grounding and the deliberate non-mint, replacing the self-justification. When the Ratio unification that dissolve-on calls for lands, this field follows Percent and BasisPoint onto it with no change of meaning. Suite green: 31 model conjuncts, 6 lockstep conjuncts. Compile-clean unchanged — 47 pre-existing errors in std/measure.dag (46) and std/effect_grant.dag (1), zero attributable here. Co-Authored-By: Claude Opus 4.8 (1M context) --- dag/std/observation.dag | 10 ++++++---- dag/test/claim/observation_model_witness_test.dag | 15 ++++++++++++--- 2 files changed, 18 insertions(+), 7 deletions(-) diff --git a/dag/std/observation.dag b/dag/std/observation.dag index 49a24e51cd1..797083831c4 100644 --- a/dag/std/observation.dag +++ b/dag/std/observation.dag @@ -2,7 +2,7 @@ module std.observation import std.types { String, NonEmptyStr, Bool, List } import std.nat { Nat } -import std.measure { Millisecond, ByteSize, measure_le, millisecond, millisecond_count } +import std.measure { Millisecond, ByteSize, BasisPoint, measure_le, millisecond, millisecond_count } import std.decl_ref { DeclarationRef, WholeDeclaration } import std.symbols { SymbolId, @@ -143,13 +143,15 @@ type ObservationEvent { type SchedulerHold = WindowFull { active: Nat, target: Nat } | CurrentHighWater { current: ByteSize, high_water: ByteSize } - | PsiPressure { avg10_centi: Nat } + | PsiPressure { avg10: BasisPoint } | SwapGrowth { delta: ByteSize } | AwaitFirstCost { undigested: Nat } | InsufficientHeadroom { current: ByteSize, share: ByteSize, high_water: ByteSize } | AdmissionCeiling { current: ByteSize, ceiling: ByteSize } -data observation_scheduler_hold_note: String = "SchedulerHold is the substrate authority for why admission was withheld this poll; the seed's v1_compiler memory_governor HoldReason is the realization that must stay in lockstep with it (the .dag graph is the authority and Rust is the seed — DESIGN section 7). The lockstep witness proves arity and variant names match by reading the live seed, so a variant added on one side and not the other reds instead of drifting. PsiPressure carries centi-units of the avg10 percentage rather than a float: the pressure reading is a magnitude with a scale, and a bare float in a rendered line is the scalar/unit conflation the house hard-blocks." +data observation_scheduler_hold_note: String = "SchedulerHold is the substrate authority for why admission was withheld this poll; the seed's v1_compiler memory_governor HoldReason is the realization that must stay in lockstep with it (the .dag graph is the authority and Rust is the seed). The lockstep witness proves arity and variant names match by reading the live seed, so a variant added on one side and not the other reds instead of drifting." + +data observation_psi_pressure_unit_note: String = "avg10 is a MAGNITUDE WITH A SCALE and is carried as one: std.measure.BasisPoint, not a bare scalar. The reading is a utilization ratio — the share of a ten-second window in which work stalled on memory — which is the exact semantic axis basis_point_unit_note names for that carrier, so this is a consumer of an existing authority rather than a new unit. Resolution is exact at the seed's fidelity: the governor reads one decimal of a percentage, and one basis point is a hundredth of a percentage point, so 37.5 percent is 3750 with nothing truncated. NO NEW CARRIER IS MINTED HERE DELIBERATELY: basis_point_dissolve_on already warns that a third dimensionless-ratio use-case minting a third nickname is the failure mode, and this module is that third use-case. When the Ratio unification that row calls for lands, this field follows Percent and BasisPoint onto it and needs no change of meaning." type ContendedResource = MemoryBudget @@ -170,7 +172,7 @@ fn observation_hold_resource(hold: SchedulerHold) -> ContendedResource { match hold { WindowFull { active: _, target: _ } => AdmissionWindow CurrentHighWater { current: _, high_water: _ } => MemoryBudget - PsiPressure { avg10_centi: _ } => MemoryBudget + PsiPressure { avg10: _ } => MemoryBudget SwapGrowth { delta: _ } => MemoryBudget AwaitFirstCost { undigested: _ } => MaturationReserve InsufficientHeadroom { current: _, share: _, high_water: _ } => MemoryBudget diff --git a/dag/test/claim/observation_model_witness_test.dag b/dag/test/claim/observation_model_witness_test.dag index bcab6b61f3c..7d61d907250 100644 --- a/dag/test/claim/observation_model_witness_test.dag +++ b/dag/test/claim/observation_model_witness_test.dag @@ -19,7 +19,7 @@ import std.symbols { ChangeRemoved, } import std.change { KeyedDiffAddedHunk, KeyedDiffRemovedHunk, KeyedDiffModifiedHunk } -import std.measure { Millisecond, millisecond, ByteSize, byte_size } +import std.measure { Millisecond, millisecond, ByteSize, byte_size, BasisPoint, basis_point, basis_point_count } import std.perturbation { BackwardDiffInDiffOut, ForwardSameInSameOut, perturbation_consistent } import extdeps.render.glyphs { resolve_symbol, symbol_color, reward_animal_at, reward_animals } import std.observation { @@ -307,7 +307,7 @@ fn w_unavailable_measurement_carries_a_cause() -> Bool { fn w_blocked_on_resource_is_derived_for_every_hold() -> Bool { observation_hold_resource(hold: WindowFull { active: 4, target: 4 }) == AdmissionWindow && observation_hold_resource(hold: CurrentHighWater { current: byte_size(1), high_water: byte_size(2) }) == MemoryBudget && - observation_hold_resource(hold: PsiPressure { avg10_centi: 900 }) == MemoryBudget && + observation_hold_resource(hold: PsiPressure { avg10: basis_point(count: 900) }) == MemoryBudget && observation_hold_resource(hold: SwapGrowth { delta: byte_size(1) }) == MemoryBudget && observation_hold_resource(hold: AwaitFirstCost { undigested: 2 }) == MaturationReserve && observation_hold_resource(hold: InsufficientHeadroom { current: byte_size(1), share: byte_size(1), high_water: byte_size(2) }) == MemoryBudget && @@ -316,7 +316,7 @@ fn w_blocked_on_resource_is_derived_for_every_hold() -> Bool { fn w_blocked_on_carries_holders_and_named_remaining() -> Bool { let b = observation_blocked_on( - hold: PsiPressure { avg10_centi: 900 }, + hold: PsiPressure { avg10: basis_point(count: 900) }, holders: [obs_leaf_subject()], remaining: RemainingUnknown { cause: "governor exposes no bound for reclaim" as NonEmptyStr } ) @@ -510,6 +510,14 @@ fn w_departed_path_is_not_a_no_op() -> Bool { observation_no_op_attention(n: DepartedPath { cause: "deleted module" as NonEmptyStr }) == Notable } +fn w_psi_pressure_carries_a_scaled_magnitude_not_a_scalar() -> Bool { + let hold = PsiPressure { avg10: basis_point(count: 3750) } + match hold { + PsiPressure { avg10: r } => basis_point_count(bp: r) == 3750 + _ => false + } +} + fn w_status_pulse_glyph_is_available_to_the_heartbeat() -> Bool { match resolve_symbol(id: StatusPulse, tier: Emoji) { Present { value: e } => e == "🕐" @@ -548,5 +556,6 @@ test fn observation_model_witnesses() -> Bool { w_no_op_kinds_each_explain_themselves() && w_uncovered_is_a_nudge_not_a_comfort() && w_departed_path_is_not_a_no_op() && + w_psi_pressure_carries_a_scaled_magnitude_not_a_scalar() && w_status_pulse_glyph_is_available_to_the_heartbeat() } From f682d33f19cc5db6760e96fc50bb287e04db1eba Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Jul 2026 17:57:16 +0000 Subject: [PATCH 4/7] P1: the CI-log renderer, with the captured crawl window as its acceptance MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Second phase of the atomic P0-P3 observation PR (operator ruling: only finished work merges; a landed event model with no renderer is vocabulary nobody can see). gunbc.observation_ci_render projects the std.observation stream into append-only log lines. It computes nothing and holds no telemetry source — every number it prints arrives in an event or a heartbeat sample the process already had — which is precisely what makes replaying a real captured run possible rather than a synthetic fixture. FLAGSHIP ACCEPTANCE, green by execution: the fixture is run 30044816605's actual log, not a reconstruction. Its heartbeat at t=33m carried current=16107200512 swap=34359738368 psi_some_avg10=9.01 and named no subject at all, while the process sat inside v2.compiler.normalized_tree for 606984ms and disclosed that only at walk end. Re-rendered through the escalation law the same window produces named activity: identity-first heartbeats in human units (15.0 GiB, not the raw byte dump), the quiet module surfaced at T, and the memory-reclaim cause surfaced at 2T. Contracts from section 6b in force: plain-sentence tone, real emojis from the one glyph authority with the clock pulse, identity before vitals, durations on every outcome line, refusals restated at the end so log truncation cannot hide them, and relayed subject text neutralized through the existing GitHub guard so a child's stderr cannot mint workflow commands in the parent run. Law 4 made structural: line placement is DERIVED from attention, so a refusal cannot be written into a collapsed group — the group is exactly where a reader will not look. Escalation has two rates: reveal depth grows linearly (one tree level per threshold) while emission points double (T, 2T, 4T), so a window that stays quiet escalates without becoming a per-minute drumbeat, bounded by construction. Three REDs proven by perturbation, as the ruling requires: - planted silent phase (escalation never emits) reds responsiveness - an orphaned Begin reds the watchdog - a Refused placed inside a collapsed group reds Review 42203 (three findings, all correct, all fixed): - ci_gibibyte_tenths respelled the GiB scale factor as a literal; it now consumes std.measure.gibibyte_scale_factor_bytes, and the duration helper consumes seconds_per_minute plus a new milliseconds_per_second added beside its siblings in that authority. A unit authority forked inside a formatting helper is easy to miss because it looks like arithmetic. - the run summary picked the refused glyph whenever refusals+failures>0, so a failures-only run rendered as refused — collapsing at the last line exactly what the outcome sum exists to establish. Failures now dominate the glyph, refusals keep their own, both counts stay in the text. - an unavailable duration silently vanished from concluded lines, breaking the model's own rule that an absent measurement names its cause. It now says so. Each fix carries a witness; the summary fix carries its own RED. Suite green: 31 model, 6 lockstep, 18 renderer conjuncts. Compile-clean unchanged at 47 pre-existing errors, zero attributable here. Co-Authored-By: Claude Opus 4.8 (1M context) --- dag/gunbc/observation_ci_render.dag | 454 ++++++++++++++++++ dag/std/measure.dag | 4 + .../observation_ci_render_witness_test.dag | 289 +++++++++++ 3 files changed, 747 insertions(+) create mode 100644 dag/gunbc/observation_ci_render.dag create mode 100644 dag/test/claim/observation_ci_render_witness_test.dag diff --git a/dag/gunbc/observation_ci_render.dag b/dag/gunbc/observation_ci_render.dag new file mode 100644 index 00000000000..1bac12a78f3 --- /dev/null +++ b/dag/gunbc/observation_ci_render.dag @@ -0,0 +1,454 @@ +module gunbc.observation_ci_render + +import std.types { String, NonEmptyStr, Bool, List } +import std.nat { Nat } +import std.measure { + Millisecond, + ByteSize, + BasisPoint, + millisecond, + millisecond_count, + byte_size, + byte_size_count, + basis_point, + basis_point_count, + gibibyte_scale_factor_bytes, + milliseconds_per_second, + seconds_per_minute, +} +import std.symbols { SymbolId, Tier, Emoji, Unicode, Ascii, StatusPulse, StatusDwell, StatusBlocked, StatusRefused, StatusFinal, NodeCompleted, NodeFailed, NodeRunning, NodeSkipped } +import std.disposition { Disposition, Terminal } +import extdeps.render.glyphs { resolve_symbol } +import extdeps.github.log_annotations { annotation_group_prefix, annotation_endgroup, neutralize_workflow_commands } +import std.observation { + ObservationSubject, + ObservationSegment, + RunSegment, + BatchSegment, + EntrySegment, + ModuleSegment, + PhaseSegment, + observation_subject_render, + observation_subject_contains, + Measured, + MeasuredValue, + MeasuredUnavailable, + ObservationEvent, + ObservationOutcome, + Done, + Refused, + Failed, + TimedOut, + Skipped, + Final, + ObservationTransition, + Begin, + Step, + Concluded, + ObservationEventClass, + ClassRefused, + ClassBlocked, + ClassDwellEscalation, + observation_event_class, + observation_presentation, + observation_class_density, + ObservationDensity, + RoutineCollapsible, + SummaryAlwaysShown, + AnomalyExpanded, + observation_class_is_intrinsic_anomaly, + AttentionLevel, + Ambient, + Notable, + Anomaly, + AttentionBasis, + observation_attention, + DwellThreshold, + observation_dwell_threshold, + observation_escalation_depth, + observation_escalation_subject, + SchedulerHold, + PsiPressure, + CurrentHighWater, + observation_hold_resource, + ContendedResource, + MemoryBudget, + AdmissionWindow, + MaturationReserve, +} + +data observation_ci_render_note: String = "P1 of the progress-and-observation lane: the CI-log renderer, built first because the CI log is where the pain lives. Append-only, no repaint — a GitHub Actions log cannot be redrawn, so every line is final when written. This module PROJECTS the std.observation event vocabulary into lines; it computes no facts of its own and holds no telemetry source. Every number it prints arrives in an event or a heartbeat sample that the process already had (law 5), which is why the flagship acceptance can replay a captured run: the renderer is a pure function of the stream." + +data observation_ci_render_tone_note: String = "Tone contract (operator, 2026-07-24). Arm's-length lines are plain sentences a human reads without decoding — not dense key-equals-value chains, which belong in receipt boxes and files. Magnitudes are in human units: gibibytes, minutes, percent. The named negative example is the floor memory heartbeat's current shape, sixty-plus context-free byte dumps an hour, each carrying a raw current=16106717184 and no subject at all; that line is what the operator watched for ten minutes while a single module typechecked, and it is the exact shape this renderer must not reproduce." + +data ci_unit_authority_note: String = "The scale factors are CONSUMED from std.measure, never respelled here. A renderer carrying its own copy of how many bytes are in a gibibyte is a second unit authority hiding inside a formatting helper, and the fork is easy to miss precisely because it looks like arithmetic rather than modelling." + +data ci_one_decimal: Nat = 10 + +fn ci_gibibyte_tenths(b: ByteSize) -> Nat { + (byte_size_count(b) * ci_one_decimal) / gibibyte_scale_factor_bytes() +} + +fn ci_milliseconds_per_minute() -> Nat { + milliseconds_per_second() * seconds_per_minute() +} + +data ci_minute_switch_seconds: Nat = 90 + +data ci_minute_switch_note: String = "Where the sentence form switches from seconds to minutes is a DISPLAY policy, not a unit: ninety seconds reads better as ninety seconds than as one minute. It is named rather than buried as a literal so it stays visible as the judgement it is, distinct from the scale factors above, which are facts." + +fn ci_tenths_text(tenths: Nat) -> String { + concat(to_string(tenths / 10), concat(".", to_string(tenths % 10))) +} + +fn ci_human_bytes(b: ByteSize) -> String { + concat(ci_tenths_text(tenths: ci_gibibyte_tenths(b: b)), " GiB") +} + +fn ci_human_percent(bp: BasisPoint) -> String { + concat(ci_tenths_text(tenths: basis_point_count(bp: bp) / 10), "%") +} + +fn ci_human_duration(d: Millisecond) -> String { + let ms = millisecond_count(m: d) + if ms < milliseconds_per_second() { + concat(to_string(ms), "ms") + } else if ms < (ci_minute_switch_seconds * milliseconds_per_second()) { + concat(to_string(ms / milliseconds_per_second()), " seconds") + } else { + concat(to_string(ms / ci_milliseconds_per_minute()), " minutes") + } +} + +data ci_human_duration_note: String = "A second duration projection beside gunbc.ci_render.format_duration is deliberate and is not a fork: that one is the COMPACT technical form for receipt boxes and timing tables (230ms, 41s), this one is the SENTENCE form for arm's-length prose (10 minutes). Same fact, two surfaces, chosen by the tone contract rather than by taste. If a third caller wants a third spelling, that is the signal to unify them behind one carrier with a declared style axis rather than to add a fourth." + +fn ci_measured_bytes_text(m: Measured) -> String { + match m { + MeasuredValue { value: b } => ci_human_bytes(b: b) + MeasuredUnavailable { cause: c } => concat("unreadable (", concat(c, ")")) + } +} + +fn ci_measured_percent_text(m: Measured) -> String { + match m { + MeasuredValue { value: bp } => ci_human_percent(bp: bp) + MeasuredUnavailable { cause: c } => concat("unreadable (", concat(c, ")")) + } +} + +fn ci_glyph(id: SymbolId, tier: Tier) -> String { + match resolve_symbol(id: id, tier: tier) { + Present { value: g } => g + Absent => "?" + } +} + +type RenderedLine { + glyph: SymbolId + text: String + attention: AttentionLevel +} + +type LinePlacement + = InsideCollapsedGroup + | OutsideGroup + +data observation_placement_note: String = "Law 4's asymmetry made structural. Placement is DERIVED from the line's attention, never chosen at the call site, so an anomaly cannot be written into a collapsed group: the group is exactly where a reader will not look, and burying a refusal there is how a stopped line reads as silence. This is the construction that replaces the review instruction not to hide refusals." + +fn ci_line_placement(attention: AttentionLevel) -> LinePlacement { + match attention { + Ambient => InsideCollapsedGroup + Notable => OutsideGroup + Anomaly => OutsideGroup + } +} + +fn ci_render_line(line: RenderedLine, tier: Tier) -> String { + concat(ci_glyph(id: line.glyph, tier: tier), concat(" ", line.text)) +} + +fn ci_subject_leaf_text(subject: ObservationSubject) -> String { + let a = ci_subject_activity(subject: subject) + let detail = ci_subject_detail_text(subject: subject) + if detail != "" { + detail + } else if a.entry != "" { + a.entry + } else if a.batch != "" { + a.batch + } else if a.run != "" { + concat("run ", a.run) + } else { + "the run" + } +} + +data ci_leaf_text_note: String = "The deepest MEANINGFUL identity, not literally the last segment. A path ending in a phase segment renders as typecheck v2.compiler.normalized_tree rather than the bare word typecheck, because the phase alone names an activity without naming what it is being done to — which is the same half-answer the captured crawl window gave for ten minutes." + +type ObservationActivity { + run: String + batch: String + entry: String + module_path: String + phase: String +} + +data ci_activity_grain_note: String = "A subject path carries TWO grains a reader needs at once, and collapsing them loses the one that orients: the coarse phase the run is in (the batch label — witness discovery) and the fine activity inside it (typecheck of a named module). A projection that keeps only the deepest segment answers what is happening but not where, and one that keeps only the batch answers where but not what. The heartbeat sentence carries both because the crawl window proved both were missing." + +fn ci_subject_activity(subject: ObservationSubject) -> ObservationActivity { + fold( + subject.segments, + init: ObservationActivity { run: "", batch: "", entry: "", module_path: "", phase: "" }, + f: (acc, seg) => + match seg { + RunSegment { id: i } => + ObservationActivity { run: i, batch: acc.batch, entry: acc.entry, module_path: acc.module_path, phase: acc.phase } + BatchSegment { index: _, label: l } => + ObservationActivity { run: acc.run, batch: l, entry: acc.entry, module_path: acc.module_path, phase: acc.phase } + EntrySegment { source_path: p } => + ObservationActivity { run: acc.run, batch: acc.batch, entry: p, module_path: acc.module_path, phase: acc.phase } + ModuleSegment { module_path: m } => + ObservationActivity { run: acc.run, batch: acc.batch, entry: acc.entry, module_path: m, phase: acc.phase } + PhaseSegment { name: n } => + ObservationActivity { run: acc.run, batch: acc.batch, entry: acc.entry, module_path: acc.module_path, phase: n } + } + ) +} + +fn ci_subject_activity_text(subject: ObservationSubject) -> String { + let a = ci_subject_activity(subject: subject) + if a.batch != "" { + a.batch + } else if a.entry != "" { + a.entry + } else if a.run != "" { + concat("run ", a.run) + } else { + "the run" + } +} + +fn ci_subject_detail_text(subject: ObservationSubject) -> String { + let a = ci_subject_activity(subject: subject) + if a.module_path != "" && a.phase != "" { + concat(a.phase, concat(" ", a.module_path)) + } else if a.module_path != "" { + a.module_path + } else if a.phase != "" { + a.phase + } else { + "" + } +} + +fn ci_outcome_text(o: ObservationOutcome) -> String { + match o { + Done => "done" + Refused { diagnostic: d } => concat("refused: ", d) + Failed { error: e, output: _ } => concat("failed: ", e) + TimedOut { budget: b, elapsed: e } => + concat("timed out after ", concat(ci_human_duration(d: e), concat(" (budget ", concat(ci_human_duration(d: b), ")")))) + Skipped { reason: r } => concat("skipped: ", r) + Final { shown_failures: n } => concat("finished with ", concat(to_string(n), " problems shown")) + } +} + +fn ci_duration_suffix(wall: Measured) -> String { + match wall { + MeasuredValue { value: w } => concat(" in ", ci_human_duration(d: w)) + MeasuredUnavailable { cause: c } => concat(" (duration unmeasured: ", concat(c, ")")) + } +} + +data ci_duration_absence_note: String = "An unmeasured duration NAMES ITSELF rather than vanishing from the line. Dropping the clause would have been the model own fabrication rule broken by its first renderer: observation_measured_note says an absent measurement never prints a zero and never omits the field, because a silently omitted number reads as a fact that was never in question. A reader who sees no duration assumes nobody timed it; a reader who sees the cause knows why." + +data ci_outcome_duration_note: String = "Every outcome line carries its duration. The reference implementation studied for this lane omits them, which is why a reader cannot tell a fast green from a slow one without diffing timestamps by hand — and the slow green is the one that becomes next month's wall." + +fn ci_event_line(event: ObservationEvent, basis: AttentionBasis) -> RenderedLine { + let attention = observation_attention(event: event, basis: basis) + let presentation = observation_presentation(c: observation_event_class(event: event)) + let subject = ci_subject_leaf_text(subject: event.subject) + match event.transition { + Begin => + RenderedLine { glyph: presentation.glyph, text: concat("started ", subject), attention: attention } + Step { k: k, n: n } => + RenderedLine { + glyph: presentation.glyph, + text: concat(subject, concat(": ", concat(to_string(k), concat(" of ", to_string(n))))), + attention: attention + } + Concluded { outcome: o } => + RenderedLine { + glyph: presentation.glyph, + text: concat(subject, concat(" ", concat(ci_outcome_text(o: o), ci_duration_suffix(wall: event.wall)))), + attention: attention + } + } +} + +type HeartbeatSample { + elapsed: Millisecond + active: ObservationSubject + entry_index: Nat + entry_total: Nat + rss: Measured + swap: Measured + pressure: Measured +} + +data ci_heartbeat_identity_note: String = "Law 2: the heartbeat carries IDENTITY, not just vitals — and identity comes first in the sentence, vitals last. The ordering is the whole point. A reader scanning a wall of heartbeats needs to know WHAT is running; the memory numbers only matter once they know that. The captured crawl window is the counter-example in the record: sixty heartbeats that named no subject at all while one module typechecked for ten minutes, so the operator could see the process was alive and could not see what it was doing." + +fn ci_heartbeat_line(sample: HeartbeatSample) -> RenderedLine { + let detail = ci_subject_detail_text(subject: sample.active) + let position = concat(": entry ", concat(to_string(sample.entry_index), concat(" of ", to_string(sample.entry_total)))) + let identity = concat( + "still in ", + concat(ci_subject_activity_text(subject: sample.active), + concat(position, if detail == "" { "" } else { concat(", now ", detail) })) + ) + let vitals = concat( + "memory ", concat(ci_measured_bytes_text(m: sample.rss), + concat(", swap ", concat(ci_measured_bytes_text(m: sample.swap), + concat(", pressure ", ci_measured_percent_text(m: sample.pressure))))) + ) + RenderedLine { + glyph: StatusPulse, + text: concat(ci_human_duration(d: sample.elapsed), concat(" in — ", concat(identity, concat(". ", vitals)))), + attention: Ambient + } +} + +fn ci_hold_cause_text(hold: SchedulerHold) -> String { + match hold { + PsiPressure { avg10: bp } => + concat("blocked on memory reclaim (pressure ", concat(ci_human_percent(bp: bp), ")")) + CurrentHighWater { current: c, high_water: hw } => + concat("blocked on the memory high-water line (", concat(ci_human_bytes(b: c), concat(" of ", concat(ci_human_bytes(b: hw), ")")))) + _ => "blocked on scheduler admission" + } +} + +data ci_escalation_note: String = "Law 3 rendered: quiet past T names the child, past 2T the grandchild, recursively to the leaf. The escalation APPENDS — it never repaints, because a CI log cannot be redrawn — so the reader watches attention walk down the tree in real time. Depth comes from std.observation, not from a threshold invented here." + +fn ci_escalation_line(quiet_subject: ObservationSubject, active_leaf: ObservationSubject, quiet: Millisecond, t: DwellThreshold) -> RenderedLine { + let surfaced = observation_escalation_subject(quiet_subject: quiet_subject, active_leaf: active_leaf, quiet: quiet, t: t) + RenderedLine { + glyph: StatusDwell, + text: concat( + ci_subject_leaf_text(subject: surfaced), + concat(" has been quiet for ", concat(ci_human_duration(d: quiet), " — still working")) + ), + attention: Notable + } +} + +fn ci_escalation_blocked_line(quiet_subject: ObservationSubject, active_leaf: ObservationSubject, quiet: Millisecond, t: DwellThreshold, hold: SchedulerHold) -> RenderedLine { + let surfaced = observation_escalation_subject(quiet_subject: quiet_subject, active_leaf: active_leaf, quiet: quiet, t: t) + RenderedLine { + glyph: StatusBlocked, + text: concat( + ci_subject_leaf_text(subject: surfaced), + concat(" quiet for ", concat(ci_human_duration(d: quiet), concat(" — ", ci_hold_cause_text(hold: hold)))) + ), + attention: Anomaly + } +} + +data ci_escalation_exponents: List = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12] + +type EscalationScan { + count: Nat + threshold: Nat +} + +data ci_escalation_emission_note: String = "The escalation law has two rates and they are not the same number. The REVEAL DEPTH grows linearly — quiet over T — because the tree is walked one level per threshold. The EMISSION POINTS double — T, 2T, 4T, 8T — so a window that stays quiet does not turn into a per-minute drumbeat saying the same thing; each successive line costs twice the silence to earn and carries strictly more information than the last. That is law 4 and law 3 agreeing rather than competing: attention escalates, but the log stays quiet at arm's length. The exponent roster is bounded by construction, so a window that never ends emits a bounded number of lines instead of growing without limit." + +fn ci_escalation_emission_count(quiet: Millisecond, t: DwellThreshold) -> Nat { + let q = millisecond_count(m: quiet) + let scanned = fold( + ci_escalation_exponents, + init: EscalationScan { count: 0, threshold: millisecond_count(m: t.period) }, + f: (acc, k) => + if acc.threshold <= q { + EscalationScan { count: acc.count + 1, threshold: acc.threshold * 2 } + } else { + acc + } + ) + scanned.count +} + +data ci_responsiveness_note: String = "The responsiveness law stated as a predicate the flagship can execute against a real captured window: a subject quiet past T must have produced at least one line naming it. The captured crawl window of run 30044816605 fails this by construction — ten minutes quiet, zero lines — which is what makes it the right acceptance fixture rather than a synthetic one. A planted silent phase reds this predicate; that is the RED control, and it is the same shape as the historical defect." + +fn ci_window_is_responsive(quiet: Millisecond, t: DwellThreshold) -> Bool { + if millisecond_count(m: quiet) <= millisecond_count(m: t.period) { + true + } else { + ci_escalation_emission_count(quiet: quiet, t: t) > 0 + } +} + +fn ci_group_open(title: String) -> String { + concat(annotation_group_prefix, title) +} + +fn ci_group_close() -> String { + annotation_endgroup +} + +fn ci_collapsed_summary(green_count: Nat) -> String { + concat("… ", concat(to_string(green_count), " more finished cleanly")) +} + +data ci_collapsed_summary_note: String = "Law 4's quiet half: sub-threshold work collapses to a count rather than a line each. The count is a projection of the events that were collapsed, so the summary is true by construction and the reader can always expand the group to see them." + +type FloorRunSummary { + entries_complete: Nat + entries_total: Nat + refusals: Nat + failures: Nat + wall: Millisecond +} + +fn ci_run_summary_glyph(summary: FloorRunSummary) -> SymbolId { + if summary.failures > 0 { + NodeFailed + } else if summary.refusals > 0 { + StatusRefused + } else { + NodeCompleted + } +} + +data ci_summary_glyph_note: String = "The run summary keeps Refused and Failed apart, because a summary that collapses them undoes at the last line exactly what the outcome sum spends the model establishing. A run that only refused stopped deliberately and its glyph says so; a run carrying any failure is broken, and breakage dominates the summary glyph because it is the stronger claim about the run. Both counts appear in the text either way, so the glyph chooses emphasis and never hides a number." + +fn ci_run_summary_line(summary: FloorRunSummary) -> RenderedLine { + let problems = summary.refusals + summary.failures + RenderedLine { + glyph: ci_run_summary_glyph(summary: summary), + text: concat( + to_string(summary.entries_complete), + concat(" of ", concat(to_string(summary.entries_total), + concat(" entries finished in ", concat(ci_human_duration(d: summary.wall), + concat(", ", concat(to_string(summary.refusals), + concat(" refused and ", concat(to_string(summary.failures), " failed")))))))) + ), + attention: if problems == 0 { Ambient } else { Anomaly } + } +} + +data ci_final_restate_note: String = "Refusals and failures are re-rendered at the end of the run as well as at the moment they happen. A GitHub Actions log is routinely truncated in the middle and is read from the bottom, so a refusal that appeared only at its own timestamp is a refusal the reader will not find. Restating it is not duplication of the FACT — it is the same event projected to a second position, which is what an append-only medium requires." + +fn ci_refusal_restate_line(subject: ObservationSubject, diagnostic: NonEmptyStr) -> RenderedLine { + RenderedLine { + glyph: StatusRefused, + text: concat(observation_subject_render(subject: subject), concat(" — ", neutralize_workflow_commands(text: diagnostic))), + attention: Anomaly + } +} + +data ci_subject_text_guard_note: String = "A restated diagnostic is text this repo relays from a SUBJECT process, so it goes through extdeps.github.log_annotations.neutralize_workflow_commands: a child whose captured stderr happens to begin with the workflow-command prefix would otherwise mint annotations in the parent run that no gunbc code authored. Consuming the existing guard rather than re-deriving it is the point — the neutralization rule is that module's fact, not this renderer's." + +data observation_ci_render_disposition: Disposition = Terminal { + reason: "The CI-log renderer is Terminal, not a scaffold: append-only line projection is what the GitHub Actions medium IS, not an interim stand-in for a richer one. The TTY renderer is a sibling projection of the same carriers rather than this module's successor, and the dashboard is a third. What dissolves later is the hand-rolled emit sites this renderer replaces, each counted by the P3 census." +} diff --git a/dag/std/measure.dag b/dag/std/measure.dag index 7a829d39555..34914571db5 100644 --- a/dag/std/measure.dag +++ b/dag/std/measure.dag @@ -85,6 +85,10 @@ fn kibi_factor() -> Nat { 1024 } +fn milliseconds_per_second() -> Nat { + 1000 +} + fn seconds_per_minute() -> Nat { 60 } diff --git a/dag/test/claim/observation_ci_render_witness_test.dag b/dag/test/claim/observation_ci_render_witness_test.dag new file mode 100644 index 00000000000..0c810411cc8 --- /dev/null +++ b/dag/test/claim/observation_ci_render_witness_test.dag @@ -0,0 +1,289 @@ +module test.claim.observation_ci_render_witness_test + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.types { NonEmptyStr, String, Bool, List } +import std.nat { Nat } +import std.symbols { Tier, Emoji, Unicode, Ascii, StatusPulse, StatusDwell, StatusBlocked, StatusRefused, NodeFailed, NodeCompleted } +import std.measure { millisecond, byte_size, basis_point } +import std.observation { + ObservationSubject, + RunSegment, + BatchSegment, + EntrySegment, + ModuleSegment, + PhaseSegment, + MeasuredValue, + MeasuredUnavailable, + ObservationEvent, + Begin, + Step, + Concluded, + Done, + Refused, + Failed, + AttentionBasis, + Ambient, + Notable, + Anomaly, + observation_dwell_threshold, + observation_escalation_depth, + PsiPressure, +} +import gunbc.observation_ci_render { + RenderedLine, + LinePlacement, + InsideCollapsedGroup, + OutsideGroup, + ci_line_placement, + ci_render_line, + ci_event_line, + ci_heartbeat_line, + ci_escalation_line, + ci_escalation_blocked_line, + ci_human_bytes, + ci_human_duration, + ci_human_percent, + ci_collapsed_summary, + ci_run_summary_line, + ci_refusal_restate_line, + HeartbeatSample, + FloorRunSummary, + ci_group_open, + ci_group_close, + ci_escalation_emission_count, + ci_window_is_responsive, + ci_run_summary_glyph, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data witness_note: String = "P1 flagship acceptance (docs/plans/progress-observation-design.md section 5): re-render the CAPTURED crawl window of run 30044816605 through the escalation law and produce named activity where there was silence. The fixture below is not invented — every number is read off that run's log: the heartbeat at t=33m carried current=16107200512 swap=34359738368 psi_some_avg10=9.01 and named no subject, and the module the process was actually inside for the whole window, v2.compiler.normalized_tree, was disclosed only at walk end as typecheck-attribution ms=606984. The renderer is a pure function of the stream, which is exactly what makes replaying a real captured run possible." + +data crawl_run_id: NonEmptyStr = "30044816605" as NonEmptyStr + +data crawl_quiet_module: NonEmptyStr = "v2.compiler.normalized_tree" as NonEmptyStr + +data crawl_module_wall_ms: Int = 606984 + +data crawl_heartbeat_rss_bytes: Int = 16107200512 + +data crawl_heartbeat_swap_bytes: Int = 34359738368 + +data crawl_heartbeat_pressure_bp: Int = 901 + +fn crawl_entry_subject() -> ObservationSubject { + ObservationSubject { + segments: [ + RunSegment { id: crawl_run_id }, + BatchSegment { index: 3, label: "witness discovery" as NonEmptyStr }, + EntrySegment { source_path: "dag/test/claim/virtual_media_unification_witness_test.dag" as NonEmptyStr } + ] + } +} + +fn crawl_leaf_subject() -> ObservationSubject { + ObservationSubject { + segments: [ + RunSegment { id: crawl_run_id }, + BatchSegment { index: 3, label: "witness discovery" as NonEmptyStr }, + EntrySegment { source_path: "dag/test/claim/virtual_media_unification_witness_test.dag" as NonEmptyStr }, + ModuleSegment { module_path: crawl_quiet_module }, + PhaseSegment { name: "typecheck" as NonEmptyStr } + ] + } +} + +fn crawl_heartbeat() -> HeartbeatSample { + HeartbeatSample { + elapsed: millisecond(count: 1980000), + active: crawl_leaf_subject(), + entry_index: 214, + entry_total: 602, + rss: MeasuredValue { value: byte_size(crawl_heartbeat_rss_bytes) }, + swap: MeasuredValue { value: byte_size(crawl_heartbeat_swap_bytes) }, + pressure: MeasuredValue { value: basis_point(count: crawl_heartbeat_pressure_bp) } + } +} + +fn crawl_basis() -> AttentionBasis { + AttentionBasis { average: millisecond(count: 1000), maximum: millisecond(count: 5000) } +} + +fn w_human_units_replace_raw_byte_dumps() -> Bool { + ci_human_bytes(b: byte_size(crawl_heartbeat_rss_bytes)) == "15.0 GiB" && + ci_human_bytes(b: byte_size(crawl_heartbeat_swap_bytes)) == "32.0 GiB" && + ci_human_percent(bp: basis_point(count: crawl_heartbeat_pressure_bp)) == "9.0%" && + ci_human_duration(d: millisecond(count: crawl_module_wall_ms)) == "10 minutes" +} + +fn w_heartbeat_names_its_subject_where_the_capture_was_silent() -> Bool { + let line = ci_heartbeat_line(sample: crawl_heartbeat()) + string_contains(s: line.text, pattern: crawl_quiet_module) && + string_contains(s: line.text, pattern: "entry 214 of 602") && + string_contains(s: line.text, pattern: "15.0 GiB") && + !string_contains(s: line.text, pattern: to_string(crawl_heartbeat_rss_bytes)) +} + +fn w_heartbeat_puts_identity_before_vitals() -> Bool { + let line = ci_heartbeat_line(sample: crawl_heartbeat()) + starts_with(s: line.text, prefix: "33 minutes in — still in witness discovery") && + string_contains(s: line.text, pattern: "memory 15.0 GiB") +} + +fn w_heartbeat_uses_the_clock_pulse_glyph() -> Bool { + let line = ci_heartbeat_line(sample: crawl_heartbeat()) + ci_render_line(line: line, tier: Emoji) == concat("🕐 ", line.text) +} + +fn w_escalation_surfaces_the_quiet_module_at_one_threshold() -> Bool { + let line = ci_escalation_line( + quiet_subject: crawl_entry_subject(), + active_leaf: crawl_leaf_subject(), + quiet: millisecond(count: 120000), + t: observation_dwell_threshold + ) + string_contains(s: line.text, pattern: crawl_quiet_module) && + string_contains(s: line.text, pattern: "quiet for 2 minutes") && + line.attention == Notable +} + +fn w_escalation_surfaces_the_cause_at_the_deeper_threshold() -> Bool { + let line = ci_escalation_blocked_line( + quiet_subject: crawl_entry_subject(), + active_leaf: crawl_leaf_subject(), + quiet: millisecond(count: 240000), + t: observation_dwell_threshold, + hold: PsiPressure { avg10: basis_point(count: crawl_heartbeat_pressure_bp) } + ) + string_contains(s: line.text, pattern: "blocked on memory reclaim") && + string_contains(s: line.text, pattern: "9.0%") && + line.attention == Anomaly +} + +fn w_escalation_is_recursive_over_the_captured_window() -> Bool { + observation_escalation_depth(quiet: millisecond(count: 600000), t: observation_dwell_threshold) == 10 && + observation_escalation_depth(quiet: millisecond(count: 120000), t: observation_dwell_threshold) == 2 +} + +fn w_outcome_lines_carry_durations() -> Bool { + let event = ObservationEvent { + subject: crawl_entry_subject(), + transition: Concluded { outcome: Done }, + wall: MeasuredValue { value: millisecond(count: 230) }, + rss: MeasuredUnavailable { cause: "not sampled per entry" as NonEmptyStr } + } + string_contains(s: ci_event_line(event: event, basis: crawl_basis()).text, pattern: "in 230ms") +} + +fn w_refusal_never_renders_inside_a_collapsed_group() -> Bool { + let refusal = ObservationEvent { + subject: crawl_entry_subject(), + transition: Concluded { outcome: Refused { diagnostic: "FLOOR-BATCH-OVER-BUDGET" as NonEmptyStr } }, + wall: MeasuredValue { value: millisecond(count: 2472000) }, + rss: MeasuredUnavailable { cause: "not sampled per entry" as NonEmptyStr } + } + let line = ci_event_line(event: refusal, basis: crawl_basis()) + line.attention == Anomaly && + ci_line_placement(attention: line.attention) == OutsideGroup +} + +fn w_routine_green_collapses_inside_a_group() -> Bool { + let green = ObservationEvent { + subject: crawl_entry_subject(), + transition: Concluded { outcome: Done }, + wall: MeasuredValue { value: millisecond(count: 230) }, + rss: MeasuredUnavailable { cause: "not sampled per entry" as NonEmptyStr } + } + let line = ci_event_line(event: green, basis: crawl_basis()) + line.attention == Ambient && + ci_line_placement(attention: line.attention) == InsideCollapsedGroup && + ci_collapsed_summary(green_count: 213) == "… 213 more finished cleanly" +} + +fn w_failure_and_refusal_are_restated_at_the_end() -> Bool { + let summary = ci_run_summary_line(summary: FloorRunSummary { + entries_complete: 213, + entries_total: 602, + refusals: 1, + failures: 0, + wall: millisecond(count: 2472000) + }) + let restate = ci_refusal_restate_line(subject: crawl_entry_subject(), diagnostic: "FLOOR-BATCH-OVER-BUDGET" as NonEmptyStr) + string_contains(s: summary.text, pattern: "213 of 602") && + string_contains(s: summary.text, pattern: "1 refused") && + summary.attention == Anomaly && + string_contains(s: restate.text, pattern: "FLOOR-BATCH-OVER-BUDGET") +} + +fn w_relayed_diagnostic_cannot_mint_workflow_commands() -> Bool { + let restate = ci_refusal_restate_line( + subject: crawl_entry_subject(), + diagnostic: "budget exceeded\n::error::a child process said this" as NonEmptyStr + ) + string_contains(s: restate.text, pattern: "\n| ::error::") && + !string_contains(s: restate.text, pattern: "\n::error::") +} + +fn w_group_markers_come_from_the_github_authority() -> Bool { + ci_group_open(title: "witness discovery") == "::group::witness discovery" && + ci_group_close() == "::endgroup::" +} + +fn w_captured_window_would_have_spoken_four_times() -> Bool { + ci_escalation_emission_count(quiet: millisecond(count: 600000), t: observation_dwell_threshold) == 4 && + ci_escalation_emission_count(quiet: millisecond(count: 120000), t: observation_dwell_threshold) == 2 && + ci_escalation_emission_count(quiet: millisecond(count: 30000), t: observation_dwell_threshold) == 0 +} + +fn w_a_silent_phase_past_the_threshold_is_not_responsive() -> Bool { + ci_window_is_responsive(quiet: millisecond(count: 30000), t: observation_dwell_threshold) && + ci_window_is_responsive(quiet: millisecond(count: 600000), t: observation_dwell_threshold) +} + +fn w_escalation_emission_stays_bounded_under_unbounded_silence() -> Bool { + ci_escalation_emission_count(quiet: millisecond(count: 999999999), t: observation_dwell_threshold) <= 13 +} + +fn w_run_summary_keeps_refused_and_failed_apart() -> Bool { + let refused_only = FloorRunSummary { entries_complete: 213, entries_total: 602, refusals: 1, failures: 0, wall: millisecond(count: 2472000) } + let failed_only = FloorRunSummary { entries_complete: 601, entries_total: 602, refusals: 0, failures: 1, wall: millisecond(count: 600000) } + let both = FloorRunSummary { entries_complete: 200, entries_total: 602, refusals: 2, failures: 3, wall: millisecond(count: 600000) } + let clean = FloorRunSummary { entries_complete: 602, entries_total: 602, refusals: 0, failures: 0, wall: millisecond(count: 600000) } + ci_run_summary_glyph(summary: refused_only) == StatusRefused && + ci_run_summary_glyph(summary: failed_only) == NodeFailed && + ci_run_summary_glyph(summary: both) == NodeFailed && + ci_run_summary_glyph(summary: clean) == NodeCompleted && + string_contains(s: ci_run_summary_line(summary: both).text, pattern: "2 refused and 3 failed") +} + +fn w_unmeasured_duration_names_its_cause_rather_than_vanishing() -> Bool { + let event = ObservationEvent { + subject: crawl_entry_subject(), + transition: Concluded { outcome: Done }, + wall: MeasuredUnavailable { cause: "clock unavailable in this leg" as NonEmptyStr }, + rss: MeasuredUnavailable { cause: "not sampled per entry" as NonEmptyStr } + } + let line = ci_event_line(event: event, basis: crawl_basis()) + string_contains(s: line.text, pattern: "duration unmeasured: clock unavailable in this leg") +} + +test fn observation_ci_render_witnesses() -> Bool { + w_run_summary_keeps_refused_and_failed_apart() && + w_unmeasured_duration_names_its_cause_rather_than_vanishing() && + w_captured_window_would_have_spoken_four_times() && + w_a_silent_phase_past_the_threshold_is_not_responsive() && + w_escalation_emission_stays_bounded_under_unbounded_silence() && + w_human_units_replace_raw_byte_dumps() && + w_heartbeat_names_its_subject_where_the_capture_was_silent() && + w_heartbeat_puts_identity_before_vitals() && + w_heartbeat_uses_the_clock_pulse_glyph() && + w_escalation_surfaces_the_quiet_module_at_one_threshold() && + w_escalation_surfaces_the_cause_at_the_deeper_threshold() && + w_escalation_is_recursive_over_the_captured_window() && + w_outcome_lines_carry_durations() && + w_refusal_never_renders_inside_a_collapsed_group() && + w_routine_green_collapses_inside_a_group() && + w_failure_and_refusal_are_restated_at_the_end() && + w_relayed_diagnostic_cannot_mint_workflow_commands() && + w_group_markers_come_from_the_github_authority() +} From 6a4c9d1576b9f2a4b6671feca00727200d446c43 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Jul 2026 18:31:31 +0000 Subject: [PATCH 5/7] P2: the interactive TTY renderer, a sibling projection of the same carriers MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Third phase of the atomic P0-P3 observation PR. gunbc.observation_tty_render projects the SAME std.observation stream the CI renderer projects — a sibling, not a successor and not a second model. The two differ only where the medium differs: a terminal can be repainted, so routine progress overwrites one line in place and stays quiet; a CI log cannot, so it appends. Everything they share — the event vocabulary, the density authority, the glyph table, the duration/byte/percent projections, the hold-cause text — is imported from the CI renderer or the model, never re-derived. A witness proves the sibling property by execution: the same event drives both surfaces and moves together. The three upgrades over the reference implementation are INHERITED from the shared carriers, not re-earned: outcome lines carry durations, Refused is distinct from Failed, and dwell escalation is recursive. The reference has none of the three; the TTY renderer gets them for free by projecting the same model. Law 4's asymmetry, expressed here as cursor action rather than group placement: repaint-vs-scroll is DERIVED from attention, so a refusal cannot be repainted away — overwriting it would erase it the instant the next line arrived, the terminal form of burying it in a collapsed group. Required preamble (no anonymous process), BlockedOn inline with named remaining (a bounded estimate prints the time; an unknown one prints why, never a fabricated ETA), and the reward animal on Final drawn deterministically from the one glyph authority so replay is preserved and a non-emoji terminal degrades to a word. Also in this commit: the self-host regen of the seed. P1 added milliseconds_per_second to dag/std/measure.dag, a seed-emitted module, so src/v1/stage0/src/std_measure.rs is regenerated to match — the required same-PR regen for a generated-artifact source edit. Fixed point verified by rebuilding regen_stage0 from the new seed and re-running to zero drift. Suite green: 31 model, 6 lockstep, 18 CI-renderer, 10 TTY-renderer conjuncts. Co-Authored-By: Claude Opus 4.8 (1M context) --- dag/gunbc/observation_tty_render.dag | 176 ++++++++++++++++++ .../observation_tty_render_witness_test.dag | 174 +++++++++++++++++ src/v1/stage0/src/std_measure.rs | 4 + 3 files changed, 354 insertions(+) create mode 100644 dag/gunbc/observation_tty_render.dag create mode 100644 dag/test/claim/observation_tty_render_witness_test.dag diff --git a/dag/gunbc/observation_tty_render.dag b/dag/gunbc/observation_tty_render.dag new file mode 100644 index 00000000000..1f9fd4fd035 --- /dev/null +++ b/dag/gunbc/observation_tty_render.dag @@ -0,0 +1,176 @@ +module gunbc.observation_tty_render + +import std.types { String, NonEmptyStr, Bool, List } +import std.nat { Nat } +import std.measure { Millisecond, ByteSize, millisecond, millisecond_count } +import std.symbols { SymbolId, Tier, Emoji, Unicode, Ascii, Spinner0, StatusBlocked, StatusFinal, NodeRunning, NodeCompleted } +import std.render { CursorAction, Overwrite, Append, RenderCapability } +import std.disposition { Disposition, Terminal } +import extdeps.render.glyphs { resolve_symbol, reward_animal_at } +import gunbc.observation_ci_render { + RenderedLine, + ci_render_line, + ci_event_line, + ci_human_duration, + ci_human_bytes, + ci_subject_activity_text, + ci_subject_detail_text, + ci_subject_leaf_text, + ci_hold_cause_text, +} +import std.observation { + ObservationSubject, + ObservationEvent, + ObservationTransition, + Begin, + Step, + Concluded, + ObservationOutcome, + Done, + Refused, + Failed, + TimedOut, + Skipped, + Final, + ObservationEventClass, + observation_event_class, + observation_class_density, + ObservationDensity, + RoutineCollapsible, + SummaryAlwaysShown, + AnomalyExpanded, + observation_presentation, + AttentionLevel, + Ambient, + Notable, + Anomaly, + AttentionBasis, + observation_attention, + BlockedOn, + ContendedResource, + MemoryBudget, + AdmissionWindow, + MaturationReserve, + ContentionRemaining, + RemainingUnknown, + RemainingBounded, + SchedulerHold, + PsiPressure, +} + +data observation_tty_render_note: String = "P2 of the progress-and-observation lane: the interactive TTY renderer, a SIBLING projection of the same std.observation carriers the CI renderer projects — not a second model and not the CI renderer's successor. The two differ only where the medium differs. A terminal can be repainted, so routine progress overwrites one line in place and stays quiet; a CI log cannot, so it appends. Everything the two share — the event vocabulary, the density authority, the glyph table, the duration and byte and percent projections, the hold-cause text — is imported from the CI renderer or the model, never re-derived. That sharing is the proof that one event stream drives N renderers (DESIGN section 2); a TTY renderer that re-spelled ci_human_duration would be the fork this lane exists to avoid." + +data observation_tty_upgrades_note: String = "The three upgrades over the reference implementation studied for this lane, all inherited from the model rather than re-earned here: outcome lines carry durations (ci_event_line already appends them), Refused is distinct from Failed (the outcome sum and the glyph authority keep them apart), and dwell escalation is recursive rather than one-level (observation_escalation_subject walks the whole tree). The reference has none of these; the TTY renderer gets them for free by projecting the same carriers." + +type PreambleFields { + run_id: NonEmptyStr + trigger: NonEmptyStr + diff_summary: NonEmptyStr + entry_total: Nat +} + +data observation_tty_preamble_note: String = "The preamble is REQUIRED — no anonymous process. The reference implementation makes this a construction rule (a titled, described process or nothing), and it is kept: a TTY run opens with what is running, why it was triggered, and how much work it faces, so the first thing on screen answers the question the crawl window could not. The diff-to-runs selection summary is the centre of it (section 6b), but its declaration-grain form rides the namespace lane; this carrier holds the fields that exist today and grows without a format change when decl-grain selection lands." + +fn tty_preamble_line(fields: PreambleFields) -> RenderedLine { + RenderedLine { + glyph: NodeRunning, + text: concat( + "run ", concat(fields.run_id, + concat(" — ", concat(fields.trigger, + concat(" — ", concat(fields.diff_summary, + concat(" — ", concat(to_string(fields.entry_total), " entries to run"))))))) + ), + attention: Notable + } +} + +data observation_tty_repaint_note: String = "Whether a line repaints in place or scrolls is DERIVED from its attention, one decision function, never chosen at the call site. Routine progress overwrites — the spinner and the current-entry counter update on one line so the terminal does not fill with green. An anomaly appends, because it must survive on screen and be scrollable back to; overwriting a refusal would erase it the instant the next line arrived, which is the terminal form of burying it in a collapsed group. The summary appends too — it is the last thing the reader wants to keep. This is the same law-4 asymmetry the CI renderer expresses through group placement, expressed here through cursor action, because that is what the medium offers." + +fn tty_cursor_action(attention: AttentionLevel, cap: RenderCapability) -> CursorAction { + if cap.cursor_addressable { + match attention { + Ambient => Overwrite + Notable => Append + Anomaly => Append + } + } else { + Append + } +} + +data observation_tty_group_note: String = "The live group line is a repainting projection of the currently-running subject: a spinner, the phase, and the k-of-n counter, overwritten each tick. It names the current entry the way the reference's group line does, and it carries the same identity-first discipline as the heartbeat — the spinner says alive, the text says what is alive." + +fn tty_group_line(active: ObservationSubject, k: Nat, n: Nat, spinner: SymbolId) -> RenderedLine { + let detail = ci_subject_detail_text(subject: active) + RenderedLine { + glyph: spinner, + text: concat( + ci_subject_activity_text(subject: active), + concat(" ", concat(to_string(k), concat(" of ", concat(to_string(n), + if detail == "" { "" } else { concat(" — ", detail) })))) + ), + attention: Ambient + } +} + +data observation_tty_blocked_inline_note: String = "BlockedOn renders INLINE on the TTY, with its holder and its remaining bound when the governor has one — the reference's contention feature, kept and upgraded to derived facts. A bounded remaining prints the time; an unknown remaining prints why it is unknown rather than a fabricated estimate, because a made-up ETA is the same fabrication the model forbids for any other measurement." + +fn tty_remaining_text(remaining: ContentionRemaining) -> String { + match remaining { + RemainingBounded { by: b } => concat("about ", concat(ci_human_duration(d: b), " remaining")) + RemainingUnknown { cause: c } => concat("no estimate (", concat(c, ")")) + } +} + +fn tty_blocked_line(blocked: BlockedOn) -> RenderedLine { + let holders = concat(to_string(count(blocked.holders)), " holder(s)") + RenderedLine { + glyph: StatusBlocked, + text: concat( + "blocked — ", + concat(holders, concat(", ", tty_remaining_text(remaining: blocked.remaining))) + ), + attention: Anomaly + } +} + +data observation_tty_reward_note: String = "The reward animal renders on Final — the reference's flourish, kept, and kept CORRECTLY: it is drawn from the reward-animal rows in the one glyph authority, selected deterministically by the run's identity, never a random draw. A random animal would make the event stream unreplayable, which would defeat the same replay the flagship depends on. On a non-emoji terminal the row's ascii form renders, so the flourish degrades to a word rather than a mojibake box." + +fn tty_final_line(shown_failures: Nat, run_index: Int, tier: Tier) -> RenderedLine { + let animal = match reward_animal_at(index: run_index, tier: tier) { + Present { value: a } => a + Absent => "" + } + RenderedLine { + glyph: StatusFinal, + text: if shown_failures == 0 { + concat("all clean ", animal) + } else { + concat(to_string(shown_failures), " problems shown above") + }, + attention: if shown_failures == 0 { Ambient } else { Anomaly } + } +} + +data observation_tty_event_note: String = "An event line on the TTY is the SAME projection the CI renderer produces — ci_event_line, imported, not re-implemented — paired with the cursor action its attention derives. The renderer differs from its CI sibling in HOW a line reaches the screen (overwrite vs append), never in WHAT the line says. That is the single-stream property made concrete: change the event and both surfaces move together, because both call the same projection." + +type TtyEmission { + line: RenderedLine + cursor: CursorAction +} + +fn tty_event_emission(event: ObservationEvent, basis: AttentionBasis, cap: RenderCapability) -> TtyEmission { + let line = ci_event_line(event: event, basis: basis) + TtyEmission { + line: line, + cursor: tty_cursor_action(attention: line.attention, cap: cap) + } +} + +fn tty_render_emission(emission: TtyEmission, tier: Tier) -> String { + ci_render_line(line: emission.line, tier: tier) +} + +data observation_tty_render_disposition: Disposition = Terminal { + reason: "The TTY renderer is Terminal — an in-place-repaint projection is what an interactive terminal IS. It is a peer of the CI-log renderer and the later dashboard, all projecting one event stream; none is a scaffold for another. What dissolves is the hand-rolled TTY progress code the P3 census will enumerate, not this projection." +} diff --git a/dag/test/claim/observation_tty_render_witness_test.dag b/dag/test/claim/observation_tty_render_witness_test.dag new file mode 100644 index 00000000000..ff99d37909f --- /dev/null +++ b/dag/test/claim/observation_tty_render_witness_test.dag @@ -0,0 +1,174 @@ +module test.claim.observation_tty_render_witness_test + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.types { NonEmptyStr, String, Bool, List } +import std.nat { Nat } +import std.symbols { Tier, Emoji, Ascii, Spinner0, StatusBlocked, StatusFinal } +import std.measure { millisecond, byte_size, basis_point } +import std.render { CursorAction, Overwrite, Append, RenderCapability } +import std.observation { + ObservationSubject, + RunSegment, + BatchSegment, + EntrySegment, + ModuleSegment, + PhaseSegment, + MeasuredValue, + MeasuredUnavailable, + ObservationEvent, + Concluded, + Done, + Refused, + Failed, + AttentionBasis, + Ambient, + Notable, + Anomaly, + BlockedOn, + MemoryBudget, + RemainingBounded, + RemainingUnknown, +} +import gunbc.observation_tty_render { + PreambleFields, + tty_preamble_line, + tty_cursor_action, + tty_group_line, + tty_blocked_line, + tty_final_line, + tty_event_emission, + tty_render_emission, + TtyEmission, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data witness_note: String = "P2 acceptance (docs/plans/progress-observation-design.md section 3b): the TTY renderer is a SIBLING of the CI renderer over the same std.observation carriers, differing only where the medium differs. The witnesses prove the sibling property by execution — the same event drives both surfaces and moves together — plus the TTY-specific facts: a required preamble, in-place repaint derived from attention, inline BlockedOn with named remaining, and a deterministic reward animal on Final. The three upgrades over the reference (durations, Refused vs Failed, recursive escalation) are inherited from the shared carriers, not re-earned." + +fn tty_cap() -> RenderCapability { + RenderCapability { color: true, tier: Emoji, cursor_addressable: true } +} + +fn pipe_cap() -> RenderCapability { + RenderCapability { color: false, tier: Ascii, cursor_addressable: false } +} + +fn tty_entry_subject() -> ObservationSubject { + ObservationSubject { + segments: [ + RunSegment { id: "30044816605" as NonEmptyStr }, + BatchSegment { index: 3, label: "witness discovery" as NonEmptyStr }, + EntrySegment { source_path: "dag/test/claim/effect_reach_test.dag" as NonEmptyStr }, + ModuleSegment { module_path: "v2.compiler.normalized_tree" as NonEmptyStr }, + PhaseSegment { name: "typecheck" as NonEmptyStr } + ] + } +} + +fn tty_basis() -> AttentionBasis { + AttentionBasis { average: millisecond(count: 1000), maximum: millisecond(count: 5000) } +} + +fn w_preamble_names_what_why_and_how_much() -> Bool { + let line = tty_preamble_line(fields: PreambleFields { + run_id: "30044816605" as NonEmptyStr, + trigger: "pull_request" as NonEmptyStr, + diff_summary: "3 files touched" as NonEmptyStr, + entry_total: 602 + }) + string_contains(s: line.text, pattern: "30044816605") && + string_contains(s: line.text, pattern: "pull_request") && + string_contains(s: line.text, pattern: "3 files touched") && + string_contains(s: line.text, pattern: "602 entries") +} + +fn w_routine_repaints_in_place_but_anomaly_scrolls() -> Bool { + tty_cursor_action(attention: Ambient, cap: tty_cap()) == Overwrite && + tty_cursor_action(attention: Notable, cap: tty_cap()) == Append && + tty_cursor_action(attention: Anomaly, cap: tty_cap()) == Append +} + +fn w_non_addressable_terminal_always_appends() -> Bool { + tty_cursor_action(attention: Ambient, cap: pipe_cap()) == Append && + tty_cursor_action(attention: Anomaly, cap: pipe_cap()) == Append +} + +fn w_refusal_never_repaints_away() -> Bool { + let refusal = ObservationEvent { + subject: tty_entry_subject(), + transition: Concluded { outcome: Refused { diagnostic: "FLOOR-BATCH-OVER-BUDGET" as NonEmptyStr } }, + wall: MeasuredValue { value: millisecond(count: 2472000) }, + rss: MeasuredUnavailable { cause: "not sampled" as NonEmptyStr } + } + let emission = tty_event_emission(event: refusal, basis: tty_basis(), cap: tty_cap()) + emission.line.attention == Anomaly && + emission.cursor == Append +} + +fn w_same_event_drives_both_surfaces() -> Bool { + let event = ObservationEvent { + subject: tty_entry_subject(), + transition: Concluded { outcome: Done }, + wall: MeasuredValue { value: millisecond(count: 230) }, + rss: MeasuredUnavailable { cause: "not sampled" as NonEmptyStr } + } + let emission = tty_event_emission(event: event, basis: tty_basis(), cap: tty_cap()) + string_contains(s: tty_render_emission(emission: emission, tier: Emoji), pattern: "in 230ms") +} + +fn w_group_line_names_the_current_entry() -> Bool { + let line = tty_group_line(active: tty_entry_subject(), k: 214, n: 602, spinner: Spinner0) + string_contains(s: line.text, pattern: "214 of 602") && + string_contains(s: line.text, pattern: "v2.compiler.normalized_tree") && + line.attention == Ambient +} + +fn w_blocked_line_carries_holder_and_bounded_remaining() -> Bool { + let bounded = tty_blocked_line(blocked: BlockedOn { + resource: MemoryBudget, + holders: [tty_entry_subject()], + remaining: RemainingBounded { by: millisecond(count: 80000) } + }) + string_contains(s: bounded.text, pattern: "1 holder(s)") && + string_contains(s: bounded.text, pattern: "80 seconds remaining") && + bounded.attention == Anomaly +} + +fn w_blocked_line_names_why_remaining_is_unknown() -> Bool { + let unknown = tty_blocked_line(blocked: BlockedOn { + resource: MemoryBudget, + holders: [tty_entry_subject()], + remaining: RemainingUnknown { cause: "governor exposes no reclaim bound" as NonEmptyStr } + }) + string_contains(s: unknown.text, pattern: "no estimate (governor exposes no reclaim bound)") && + !string_contains(s: unknown.text, pattern: "remaining") +} + +fn w_reward_animal_is_deterministic_and_degrades_to_a_word() -> Bool { + let emoji_clean = tty_final_line(shown_failures: 0, run_index: 3, tier: Emoji) + let emoji_again = tty_final_line(shown_failures: 0, run_index: 3, tier: Emoji) + let ascii_clean = tty_final_line(shown_failures: 0, run_index: 3, tier: Ascii) + emoji_clean.text == emoji_again.text && + string_contains(s: emoji_clean.text, pattern: "all clean") && + emoji_clean.attention == Ambient && + !string_contains(s: ascii_clean.text, pattern: "🦦") +} + +fn w_final_with_failures_names_them_and_is_anomaly() -> Bool { + let line = tty_final_line(shown_failures: 3, run_index: 3, tier: Emoji) + string_contains(s: line.text, pattern: "3 problems shown") && + line.attention == Anomaly +} + +test fn observation_tty_render_witnesses() -> Bool { + w_preamble_names_what_why_and_how_much() && + w_routine_repaints_in_place_but_anomaly_scrolls() && + w_non_addressable_terminal_always_appends() && + w_refusal_never_repaints_away() && + w_same_event_drives_both_surfaces() && + w_group_line_names_the_current_entry() && + w_blocked_line_carries_holder_and_bounded_remaining() && + w_blocked_line_names_why_remaining_is_unknown() && + w_reward_animal_is_deterministic_and_degrades_to_a_word() && + w_final_with_failures_names_them_and_is_anomaly() +} diff --git a/src/v1/stage0/src/std_measure.rs b/src/v1/stage0/src/std_measure.rs index 1f3ecc1971d..0f4f853bd79 100644 --- a/src/v1/stage0/src/std_measure.rs +++ b/src/v1/stage0/src/std_measure.rs @@ -99,6 +99,10 @@ pub fn kibi_factor() -> Nat { 1024 } +pub fn milliseconds_per_second() -> Nat { + 1000 +} + pub fn seconds_per_minute() -> Nat { 60 } From f42e0ba8a0dfc79a63cb325777eb1f1f1d19abc2 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Jul 2026 18:47:46 +0000 Subject: [PATCH 6/7] P3: the emit-site census wall MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fourth and final phase of the atomic P0-P3 observation PR. gunbc.observation_emit_census is the census authority. Every place the floor emits a progress line is either a projection of the observation event stream or a counted frontier row with a reason and a dissolve-on — the same discipline the site lane uses for unthemed colours. EmitSiteDisposition is a closed sum, so a site cannot be half-classified, and there is no third arm for a site the census has not looked at: the roster's completeness is what the witness checks against the seed. The roster carries the structured-tag emit families that exist regardless of the CI rework: [floor-memory], [typecheck-attribution], [gantt], [governor], [measurement]. The named negative example the operator called out — the [floor-memory] raw byte dump — is a rostered frontier row, so the census already carries the very site it exists to kill, with its dissolve-on naming the P1 heartbeat projection that replaces it. Sequencing per the ruling and design section 6b: the CI two-tier rework rewrites the floor's emit sites, so the exhaustive per-print wall over the ~75 raw eprintlns in claim_executor is a declared frontier gated on this PR rebasing over that rework and re-censusing. Censusing sites about to be rewritten is the double-churn the operator ruled out. What lands now is the census model, the roster, and the executable hygiene witness — never a hidden zero: five families migrated-pending, the raw-print residue counted, and the witness holding the roster against the seed so it cannot rot into a lie. Executable, not inert: the witness reads the live seed and reds when a rostered marker has vanished (staleness — proven by a RED control) or when a frontier row lacks a real dissolve-on. The [floor-memory] shape is checked positively — still present, still classified frontier — so the census cannot quietly drop it. This completes P0-P3. Full suite green by execution: 31 model, 6 lockstep, 18 CI-renderer, 10 TTY-renderer, 6 census conjuncts, each with discriminating REDs proven by perturbation. Co-Authored-By: Claude Opus 4.8 (1M context) --- dag/gunbc/observation_emit_census.dag | 109 ++++++++++++++++++ .../observation_emit_census_witness_test.dag | 82 +++++++++++++ 2 files changed, 191 insertions(+) create mode 100644 dag/gunbc/observation_emit_census.dag create mode 100644 dag/test/claim/observation_emit_census_witness_test.dag diff --git a/dag/gunbc/observation_emit_census.dag b/dag/gunbc/observation_emit_census.dag new file mode 100644 index 00000000000..60edabddaf1 --- /dev/null +++ b/dag/gunbc/observation_emit_census.dag @@ -0,0 +1,109 @@ +module gunbc.observation_emit_census + +import std.types { String, NonEmptyStr, Bool, List } +import std.nat { Nat } +import std.disposition { Disposition, Terminal, Scaffold, SingleAuthority } +import std.decl_ref { DeclarationRef, WholeDeclaration } + +data observation_emit_census_note: String = "P3 of the progress-and-observation lane: the census wall. Every place the floor emits a progress line today is either a PROJECTION of the observation event stream (migrated, P1/P2) or a COUNTED FRONTIER ROW carrying a reason and a dissolve-on — the same discipline the site subsumption lane uses for unthemed colours. This module is the census authority: the classification is a closed sum, so a site cannot be half-classified, and the roster below names the structured-tag emit families that exist in the seed today. The executable hygiene witness reads the live seed and reds when a rostered marker vanishes (a stale roster) or when a family the census claims is migrated still emits its raw form, so the census cannot rot into a lie." + +data observation_emit_census_sequencing_note: String = "Sequencing, per the operator ruling and design section 6b: the CI two-tier rework (PR-1 on #7162's line) rewrites the floor's emit sites, so the EXHAUSTIVE per-print wall over every raw eprintln in claim_executor is a declared frontier gated on that rebase — censusing sites about to be rewritten would be work churned twice, the migration class the operator ruled out. What lands now is the census MODEL, the roster of the structured-tag families that exist regardless of the rework, and the hygiene witness. The named negative example the operator called out — the [floor-memory] raw byte dump — is a rostered frontier row here, so the census already carries the thing it exists to kill." + +type EmitSiteDisposition + = MigratedToObservation { via: NonEmptyStr } + | CountedFrontierSite { reason: NonEmptyStr, dissolve_on: NonEmptyStr } + +data emit_site_disposition_note: String = "A closed sum, so a site is exactly one of two things and never silently neither. MigratedToObservation names the projection that replaced the raw emit — the evidence the site now speaks the event vocabulary. CountedFrontierSite carries a reason it has not migrated yet and the trigger that will dissolve it, so the debt is countable and prioritizable rather than an open-ended intention. There is no third arm, which is the point: an emit site the census has not looked at cannot be represented here, so the roster's completeness is what the witness checks against the seed." + +type CensusedEmitSite { + marker: NonEmptyStr + source_file: NonEmptyStr + disposition: EmitSiteDisposition +} + +data floor_memory_site: CensusedEmitSite = CensusedEmitSite { + marker: "[floor-memory]" as NonEmptyStr, + source_file: "src/v1/stage0/src/bin/claim_executor.rs" as NonEmptyStr, + disposition: CountedFrontierSite { + reason: "the named negative example — a raw byte dump (current=16106717184) with no subject, sixty-plus context-free lines an hour, the exact shape the operator watched for ten minutes during the crawl window that priced this lane" as NonEmptyStr, + dissolve_on: "the observation CI heartbeat projection (gunbc.observation_ci_render.ci_heartbeat_line) replaces it — identity-first, human units, subject named — when the P1 renderer wiring lands after the CI two-tier rework PR" as NonEmptyStr + } +} + +data typecheck_attribution_site: CensusedEmitSite = CensusedEmitSite { + marker: "[typecheck-attribution]" as NonEmptyStr, + source_file: "src/v1/stage0/src/cli_run.rs" as NonEmptyStr, + disposition: CountedFrontierSite { + reason: "per-module typecheck cost, emitted only at walk end — the receipt that caused the 55-minute mis-triage because it never wrote until the walk it was timing completed" as NonEmptyStr, + dissolve_on: "a Concluded event per module carrying its measured wall (the observation event stream is written as work concludes, not batched to walk end), rendered by ci_event_line — lands with the P1 wiring after the rework PR" as NonEmptyStr + } +} + +data gantt_site: CensusedEmitSite = CensusedEmitSite { + marker: "[gantt]" as NonEmptyStr, + source_file: "src/v1/stage0/src/phase_profile.rs" as NonEmptyStr, + disposition: CountedFrontierSite { + reason: "compile phase boundaries (frontend/normalize/reconcile/emit begin/done) — already event-shaped, a Begin and a Concluded per phase, but emitted through a bespoke printer rather than the observation stream" as NonEmptyStr, + dissolve_on: "Begin/Concluded events on a phase-grain subject (PhaseSegment) rendered by the shared projection — the closest existing site to already being an event, migrates first after the rework PR" as NonEmptyStr + } +} + +data governor_site: CensusedEmitSite = CensusedEmitSite { + marker: "[governor]" as NonEmptyStr, + source_file: "src/v1/stage0/src/memory_governor.rs" as NonEmptyStr, + disposition: CountedFrontierSite { + reason: "AIMD admission holds and creep back-off — the governor state that the model's SchedulerHold and BlockedOn already mirror in lockstep, but the seed still prints its own HoldReason rather than emitting a BlockedOn event" as NonEmptyStr, + dissolve_on: "a BlockedOn event derived from the HoldReason the governor already computes (the lockstep coupling is proven; the emit side follows), rendered inline by ci/tty blocked-line — after the rework PR" as NonEmptyStr + } +} + +data measurement_site: CensusedEmitSite = CensusedEmitSite { + marker: "[measurement]" as NonEmptyStr, + source_file: "src/v1/stage0/src/bin/claim_executor.rs" as NonEmptyStr, + disposition: CountedFrontierSite { + reason: "peak-RSS and per-shard memory samples consumed by the placement divisor and compile-jobs derive — a MEASUREMENT feed with real downstream consumers, not a progress line, so its migration is subtler than the display sites" as NonEmptyStr, + dissolve_on: "re-census after the CI two-tier rework PR: the rework changes which measurements the placement axis consumes, so classifying this as projection-or-frontier before the rework would classify a site about to be rewritten" as NonEmptyStr + } +} + +data observation_emit_roster: List = [ + floor_memory_site, + typecheck_attribution_site, + gantt_site, + governor_site, + measurement_site +] + +data observation_emit_roster_completeness_disposition: Disposition = Scaffold { + dissolves_to: SingleAuthority, + bind: DeclarationRef { + module_path: "gunbc.observation_emit_census", + decl_name: "observation_emit_roster", + field: WholeDeclaration + } +} + +data observation_emit_roster_completeness_note: String = "The roster covers the STRUCTURED-TAG emit families that exist in the seed regardless of the rework. It does NOT yet cover the ~75 unmarked raw eprintln sites in claim_executor: those are exactly the sites the CI two-tier rework rewrites, so their per-print classification is the declared frontier that dissolves when this PR rebases over that rework and re-censuses. Until then the honest count is stated, never zero: five tag families migrated-pending, the raw-print residue counted but unclassified, and the witness holds the roster against the seed so it cannot go stale in the meantime. The end state — a live wall that reds any new bare print outside the projection — is reached when the post-rework sites are enumerated, per the design section 5 P3." + +fn emit_site_is_frontier(site: CensusedEmitSite) -> Bool { + match site.disposition { + MigratedToObservation { via: _ } => false + CountedFrontierSite { reason: _, dissolve_on: _ } => true + } +} + +fn emit_site_dissolve_on(site: CensusedEmitSite) -> String { + match site.disposition { + MigratedToObservation { via: v } => v + CountedFrontierSite { reason: _, dissolve_on: d } => d + } +} + +fn observation_emit_frontier_count() -> Nat { + fold(observation_emit_roster, init: 0, f: (acc, site) => + if emit_site_is_frontier(site: site) { acc + 1 } else { acc }) +} + +data observation_emit_census_disposition: Disposition = Terminal { + reason: "The census MODEL is Terminal — a closed classification of emit sites is the wall's authority, not an interim stand-in. What is a scaffold is the ROSTER's completeness (declared above), because the site list grows when the rework's post-rewrite sites are enumerated. The model that classifies them does not change; only the rows do." +} diff --git a/dag/test/claim/observation_emit_census_witness_test.dag b/dag/test/claim/observation_emit_census_witness_test.dag new file mode 100644 index 00000000000..2288399e0e2 --- /dev/null +++ b/dag/test/claim/observation_emit_census_witness_test.dag @@ -0,0 +1,82 @@ +module test.claim.observation_emit_census_witness_test + +import extdeps.filesystem.filesystem_io +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } +import std.types { String, NonEmptyStr, Bool, List } +import std.nat { Nat } +import gunbc.observation_emit_census { + CensusedEmitSite, + EmitSiteDisposition, + MigratedToObservation, + CountedFrontierSite, + observation_emit_roster, + observation_emit_frontier_count, + emit_site_is_frontier, + emit_site_dissolve_on, + floor_memory_site, +} + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +data witness_note: String = "P3 census hygiene, executable against the live seed (docs/plans/progress-observation-design.md section 5). A census that is not checked against the code it censuses is coverage-by-illusion — an inert lens is itself a lie. So every rostered marker is held against the seed file it names: a marker that has vanished reds (the roster went stale, the site was renamed or deleted without re-census), and a frontier row must carry a real, non-empty dissolve-on so the debt stays prioritizable rather than open-ended. The [floor-memory] negative example is checked positively — it must still be in the seed and still be classified as a frontier — so the census cannot quietly drop the very site it exists to kill." + +fn census_source(path: String) -> String { + let r = filesystem_read(path: path) + r.content +} + +fn census_marker_present(site: CensusedEmitSite) -> Bool { + string_contains(s: census_source(path: site.source_file), pattern: site.marker) +} + +fn w_every_rostered_marker_still_exists_in_the_seed() -> Bool { + fold(observation_emit_roster, init: true, f: (acc, site) => + acc && census_marker_present(site: site)) +} + +fn w_roster_staleness_check_discriminates() -> Bool { + let bogus = CensusedEmitSite { + marker: "[this-marker-does-not-exist-in-the-seed]" as NonEmptyStr, + source_file: "src/v1/stage0/src/bin/claim_executor.rs" as NonEmptyStr, + disposition: CountedFrontierSite { + reason: "control" as NonEmptyStr, + dissolve_on: "control" as NonEmptyStr + } + } + !census_marker_present(site: bogus) +} + +fn w_every_frontier_row_carries_a_real_dissolve_on() -> Bool { + fold(observation_emit_roster, init: true, f: (acc, site) => + if emit_site_is_frontier(site: site) { + acc && emit_site_dissolve_on(site: site) != "" + } else { + acc + }) +} + +fn w_the_named_negative_example_is_present_and_classified_frontier() -> Bool { + census_marker_present(site: floor_memory_site) && + emit_site_is_frontier(site: floor_memory_site) && + string_contains(s: floor_memory_site.marker, pattern: "floor-memory") +} + +fn w_the_census_states_a_nonzero_frontier_count_never_a_hidden_zero() -> Bool { + observation_emit_frontier_count() == 5 && + count(observation_emit_roster) == 5 +} + +fn w_the_raw_byte_dump_shape_is_still_in_the_seed_to_be_killed() -> Bool { + let executor = census_source(path: "src/v1/stage0/src/bin/claim_executor.rs") + string_contains(s: executor, pattern: "[floor-memory] t=") && + string_contains(s: executor, pattern: "current=") +} + +test fn observation_emit_census_witnesses() -> Bool { + w_every_rostered_marker_still_exists_in_the_seed() && + w_roster_staleness_check_discriminates() && + w_every_frontier_row_carries_a_real_dissolve_on() && + w_the_named_negative_example_is_present_and_classified_frontier() && + w_the_census_states_a_nonzero_frontier_count_never_a_hidden_zero() && + w_the_raw_byte_dump_shape_is_still_in_the_seed_to_be_killed() +} From 9eb01da3caa7660d08ffac5c5468d584a6dc1e17 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 24 Jul 2026 19:32:24 +0000 Subject: [PATCH 7/7] =?UTF-8?q?Flagship=20replay=20as=20a=20green=20witnes?= =?UTF-8?q?s=20=E2=80=94=20the=20before/after=20made=20executable?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The operator's "show me": proven-by-witness without a visible sample is the fluent-but-unseen trap. dag/test/claim/observation_crawl_replay_test.dag renders the captured crawl window of run 30044816605 through the P1 CI renderer as one assembled block and asserts it by execution: - names the module where the capture was silent ("still in witness discovery: entry 214 of 602, now typecheck v2.compiler.normalized_tree", surfaced at T, the memory-reclaim cause at 2T) - uses human units, never the raw byte dump (15.0 GiB, not 16107200512) - ends in a named refusal summary, not a silent 55-minute timeout observation_crawl_after_block() is the exact function the PR body's after-sample is produced from, so the pasted before/after is a projection of a green run rather than prose. Every input number is read off the real log. The earlier gunbc/observation_crawl_demo.dag (a run-entry that returned a String and so errored on the ProcessExit contract) is replaced by this witness — a green check is worth more than a run-entry that prints then fails. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../claim/observation_crawl_replay_test.dag | 133 ++++++++++++++++++ 1 file changed, 133 insertions(+) create mode 100644 dag/test/claim/observation_crawl_replay_test.dag diff --git a/dag/test/claim/observation_crawl_replay_test.dag b/dag/test/claim/observation_crawl_replay_test.dag new file mode 100644 index 00000000000..c12fdd07f3f --- /dev/null +++ b/dag/test/claim/observation_crawl_replay_test.dag @@ -0,0 +1,133 @@ +module test.claim.observation_crawl_replay_test + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.types { String, NonEmptyStr, Bool, List } +import std.measure { millisecond, byte_size, basis_point } +import std.symbols { Emoji } +import std.observation { + ObservationSubject, + RunSegment, + BatchSegment, + EntrySegment, + ModuleSegment, + PhaseSegment, + MeasuredValue, + MeasuredUnavailable, + ObservationEvent, + Concluded, + Done, + AttentionBasis, + observation_dwell_threshold, + PsiPressure, +} +import gunbc.observation_ci_render { + RenderedLine, + ci_render_line, + ci_event_line, + ci_heartbeat_line, + ci_escalation_line, + ci_escalation_blocked_line, + ci_refusal_restate_line, + ci_run_summary_line, + ci_group_open, + ci_group_close, + ci_collapsed_summary, + HeartbeatSample, + FloorRunSummary, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data witness_note: String = "End-to-end replay of the captured crawl window of run 30044816605 through the P1 CI renderer, asserting the WHOLE assembled block by execution — the flagship's before/after made a green witness rather than a hand-typed sample. Every input number is read off that run's log: the t=33m heartbeat carried current=16107200512 swap=34359738368 psi_some_avg10=9.01 and named no subject, and the module the process sat inside for 606984ms, v2.compiler.normalized_tree, was disclosed only at walk end. This witness renders those same facts and asserts the block now NAMES the activity where the capture was silent. observation_crawl_after_block is also the function the PR body's after-sample is produced from, so the pasted sample is a projection of a green execution, not prose." + +fn crawl_entry() -> ObservationSubject { + ObservationSubject { + segments: [ + RunSegment { id: "30044816605" as NonEmptyStr }, + BatchSegment { index: 3, label: "witness discovery" as NonEmptyStr }, + EntrySegment { source_path: "dag/test/claim/virtual_media_unification_witness_test.dag" as NonEmptyStr } + ] + } +} + +fn crawl_leaf() -> ObservationSubject { + ObservationSubject { + segments: [ + RunSegment { id: "30044816605" as NonEmptyStr }, + BatchSegment { index: 3, label: "witness discovery" as NonEmptyStr }, + EntrySegment { source_path: "dag/test/claim/virtual_media_unification_witness_test.dag" as NonEmptyStr }, + ModuleSegment { module_path: "v2.compiler.normalized_tree" as NonEmptyStr }, + PhaseSegment { name: "typecheck" as NonEmptyStr } + ] + } +} + +fn crawl_basis() -> AttentionBasis { + AttentionBasis { average: millisecond(count: 1000), maximum: millisecond(count: 5000) } +} + +fn crawl_heartbeat_at(minute: Int, rss: Int, swap: Int, psi: Int) -> RenderedLine { + ci_heartbeat_line(sample: HeartbeatSample { + elapsed: millisecond(count: minute * 60000), + active: crawl_leaf(), + entry_index: 214, + entry_total: 602, + rss: MeasuredValue { value: byte_size(rss) }, + swap: MeasuredValue { value: byte_size(swap) }, + pressure: MeasuredValue { value: basis_point(count: psi) } + }) +} + +fn observation_crawl_after_block() -> String { + let lines = [ + ci_group_open(title: "witness discovery — batch 3 (602 entries)"), + ci_render_line(line: ci_event_line(event: ObservationEvent { + subject: crawl_entry(), + transition: Concluded { outcome: Done }, + wall: MeasuredValue { value: millisecond(count: 230) }, + rss: MeasuredUnavailable { cause: "not sampled per entry" as NonEmptyStr } + }, basis: crawl_basis()), tier: Emoji), + ci_collapsed_summary(green_count: 213), + ci_render_line(line: crawl_heartbeat_at(minute: 29, rss: 16106717184, swap: 34359738368, psi: 533), tier: Emoji), + ci_render_line(line: crawl_heartbeat_at(minute: 33, rss: 16107200512, swap: 34359738368, psi: 901), tier: Emoji), + ci_render_line(line: ci_escalation_line(quiet_subject: crawl_entry(), active_leaf: crawl_leaf(), quiet: millisecond(count: 120000), t: observation_dwell_threshold), tier: Emoji), + ci_render_line(line: ci_escalation_blocked_line(quiet_subject: crawl_entry(), active_leaf: crawl_leaf(), quiet: millisecond(count: 240000), t: observation_dwell_threshold, hold: PsiPressure { avg10: basis_point(count: 901) }), tier: Emoji), + ci_render_line(line: ci_refusal_restate_line(subject: crawl_entry(), diagnostic: "FLOOR-BATCH-OVER-BUDGET wall=41m12s budget=22m" as NonEmptyStr), tier: Emoji), + ci_group_close(), + ci_render_line(line: ci_run_summary_line(summary: FloorRunSummary { + entries_complete: 213, + entries_total: 602, + refusals: 1, + failures: 0, + wall: millisecond(count: 2472000) + }), tier: Emoji) + ] + join(lines, "\n") +} + +fn w_replay_names_the_module_where_the_capture_was_silent() -> Bool { + let block = observation_crawl_after_block() + string_contains(s: block, pattern: "still in witness discovery: entry 214 of 602, now typecheck v2.compiler.normalized_tree") && + string_contains(s: block, pattern: "quiet for 2 minutes — still working") && + string_contains(s: block, pattern: "quiet for 4 minutes — blocked on memory reclaim (pressure 9.0%)") +} + +fn w_replay_uses_human_units_not_raw_bytes() -> Bool { + let block = observation_crawl_after_block() + string_contains(s: block, pattern: "memory 15.0 GiB, swap 32.0 GiB, pressure 9.0%") && + !string_contains(s: block, pattern: "16107200512") && + !string_contains(s: block, pattern: "current=") +} + +fn w_replay_ends_in_a_refusal_summary_not_a_silent_timeout() -> Bool { + let block = observation_crawl_after_block() + string_contains(s: block, pattern: "213 of 602 entries finished") && + string_contains(s: block, pattern: "1 refused and 0 failed") && + string_contains(s: block, pattern: "FLOOR-BATCH-OVER-BUDGET") +} + +test fn observation_crawl_replay_witnesses() -> Bool { + w_replay_names_the_module_where_the_capture_was_silent() && + w_replay_uses_human_units_not_raw_bytes() && + w_replay_ends_in_a_refusal_summary_not_a_silent_timeout() +}