diff --git a/dag/extdeps/languages/css/properties.dag b/dag/extdeps/languages/css/properties.dag index 0460dfbf2f8..229e2b093a9 100644 --- a/dag/extdeps/languages/css/properties.dag +++ b/dag/extdeps/languages/css/properties.dag @@ -23,6 +23,7 @@ type CssPropertyName | BorderLeft | BorderRadius | BorderStyle + | BoxShadow | BoxSizing | Color | ColorScheme @@ -82,6 +83,7 @@ fn css_property_wire(p: CssPropertyName) -> String { BorderLeft => "border-left" BorderRadius => "border-radius" BorderStyle => "border-style" + BoxShadow => "box-shadow" BoxSizing => "box-sizing" Color => "color" ColorScheme => "color-scheme" diff --git a/dag/gunbc/ci_layer_roots.dag b/dag/gunbc/ci_layer_roots.dag index 6cc415bd3ce..176cddb3868 100644 --- a/dag/gunbc/ci_layer_roots.dag +++ b/dag/gunbc/ci_layer_roots.dag @@ -446,6 +446,12 @@ data witness_exclusion_frontier: List = [ reason: excl_substrate_long_lane_reason, dissolve_on: excl_substrate_long_lane_dissolve }, + WitnessExclusionRow { + pattern: "long/instrument_sandbox_live_witness_test.dag", + classification: FalsifierSubstrateLongLane, + reason: excl_substrate_long_lane_reason, + dissolve_on: excl_substrate_long_lane_dissolve + }, WitnessExclusionRow { pattern: "synthetic_orphan_admission_witness_test.dag", classification: NoConsumer, @@ -1280,6 +1286,18 @@ data falsifier_substrate_long_lane_rows: List = [ reason: "v2_emitter_direct_rust_door_acceptance_admissions runs both production folds including ingest-path written-source assessment; exceeds 5s fast-lane budget. Closing frontier nonzero until ingest-path establishes WrittenSourceIndependentOfSeedEmitter (functional gap, not slowness alone)", dissolve_on: "production admissions close with frontier zero AND eval lands under gunbc_ci_fast_lane_witness_eval_budget — then re-enrolls per-PR discovery" }, + SubstrateLongLaneRow { + entry: "dag/test/claim/roadmap_program_view_witness_test.dag", + function: "witness_live_constraint_present_iff_line_unaccepted", + reason: "live_view() joins declared roadmap nodes, edges, receipts, and finish-line specs — measured ~3074ms cold locally but flaked at 5004ms in falsifier discovery-corpus batch 3 under host contention when ~6663 witnesses share the floor (run 30960560941, BudgetExceeded). Not caused by PR #7762 diff; borderline over the 5s fast-lane budget", + dissolve_on: "eval lands under gunbc_ci_fast_lane_witness_eval_budget on a measured cold run and re-enrolls per-PR discovery, or deletes as duplicate of a faster receipt" + }, + SubstrateLongLaneRow { + entry: "dag/test/claim/long/instrument_sandbox_live_witness_test.dag", + function: "instrument_sandbox_live_keystone_holds", + reason: "5074ms thread-CPU measured in falsifier discovery batch 3 (run 30986055960, BudgetExceeded against the 5000ms fast-lane budget). Attribution by execution (claim_batch, loyal-bat-373, 2026-08-05) puts 18510 of 19098ms of one served-page render inside a single live_program_view_result call, so every claim that renders the page or reads the live view pays it once and the cheap register-gate claims do not — those stay per-PR in dag/test/claim/instrument_sandbox_witness_test.dag at 0-2ms each. NOT declared irreducible corpus breadth: the projection's inputs cost 263ms to build (25 declared roadmap nodes, edges, receipts, finish-line and front specs) and deriving over them costs 5132ms, roughly 20x, at n=25. The cost is diffuse rather than one hot spot — program_relax_to_fixpoint early-exits correctly and roadmap_dependency_graph is a trivial map, but program_depth_lookup folds every row with no early exit, membership is tested by linear any-scans at every level, reverse adjacency is rebuilt per finish line where roadmap_focus already hoists it, and program_dedupe_ids rescans its accumulator per element, all nested inside per-node/per-front/per-line maps", + dissolve_on: "PARTIALLY MET AND RE-MEASURED, 2026-08-05 (do not read the 5074ms above as current). #7822 landed the keyed-lookup restructure this row named, and this witness re-measured 17899ms -> 1843ms on the same host and binary — so the original condition, eval under gunbc_ci_fast_lane_witness_eval_budget, now HOLDS. The row does not dissolve, because the bar moved: at the 500ms per-witness warning threshold (operator, 2026-08-05) a 1843ms witness re-merged per-PR would be 3.7x over the warning line, so re-merging now would move the problem rather than close it. Remaining condition: this witness lands under the 500ms warning threshold on a measured run — most of the residue is the served-page render itself, not the projection — then these claims re-merge into dag/test/claim/instrument_sandbox_witness_test.dag per-PR and this row, the exclusion row, and dag/test/claim/long/instrument_sandbox_live_witness_test.dag delete together" + }, SubstrateLongLaneRow { entry: "dag/test/claim/roadmap_program_view_live_corpus_receipt_test.dag", function: "live_roadmap_program_view_corpus_projection_receipt", diff --git a/dag/gunbc/design/instrument_audition.dag b/dag/gunbc/design/instrument_audition.dag new file mode 100644 index 00000000000..838c3272257 --- /dev/null +++ b/dag/gunbc/design/instrument_audition.dag @@ -0,0 +1,382 @@ +module gunbc.design.instrument_audition + +import std.types { String, Bool, Int, List } +import extdeps.languages.css.values { css_px } +import gunbc.design.salience { + SalienceRole, EmissionSpec, EmissionGrant, emission_for, + EmissionGranted, EmissionRefusedForRole, EmissionOutsideEnvelope, + EmissionUnitNotComparable, EmissionSoleDiscriminatorRefused, + AttractionField, attraction_envelope, focal_attraction, + attraction_travel_max_px, attraction_activation_min_px, +} +import gunbc.design.instrument_camera { + ProgramCamera, ProgramMode, ModeStatus, ModeRemaining, ModeWhy, + ProgramDepth, DepthProgram, DepthOutcome, DepthFront, DepthNode, DepthEvidence, + NoSubjectSelected, FinishLineFocused, program_mode_key, +} +import gunbc.design.instrument_physical { + InstrumentPreference, preference_still, preference_default, + compose_displacement, admit_composed_displacement, focal_attraction_headroom_px, + DisplacementAdmitted, DisplacementOverBudget, EnclosureCharacterReachesResponseTravel, +} +import gunbc.roadmap_program_view { + V1DeletionProgramView, FinishLineView, FrontView, RemainingShape, + ConstraintView, ConstraintKind, ImplementationConstraint, ContractConstraint, + program_front_key, +} + +data audition_note: String = "THE AUDITION IS A COMPARISON, NOT A DEMO. Its purpose is to let one focal control be seen at three energies on the SAME real subject, so the choice between restrained, expressive and hero is made by looking rather than by argument — which is the only way the selective-spectacle amendment can be calibrated without re-litigating it in prose every time. Two properties make it an audition rather than a mock-up: the subject is a real v1-deletion finish line carrying V0's own name, claim and roadmap node, so what the control says is true; and every intensity is admitted through the register's OWN gates (emission_for, attraction_envelope, displacement_admission) rather than through audition-local bounds, so a variant that looks good but breaks the register cannot be rendered at all. The hero variant deliberately sits at the envelope's admissible maximum: an audition whose loudest option is comfortably inside the bound tells you nothing about where the bound is." + +type AuditionIntensity + = AuditionRestrained + | AuditionExpressive + | AuditionHero + +fn audition_intensity_key(i: AuditionIntensity) -> String { + match i { + AuditionRestrained => "restrained" + AuditionExpressive => "expressive" + AuditionHero => "hero" + } +} + +data restrained_has_no_emission_note: String = "The restrained variant carries no emission at all, and that is what makes the comparison honest: it is the register as it stood BEFORE the amendment, so the audition's baseline is the real previous state rather than a slightly-dimmer version of the new one. If restrained wins, the amendment costs nothing to withdraw." + +type AuditionEmission + = AuditionNoEmission + | AuditionEmits { spec: EmissionSpec } + +fn audition_emission(i: AuditionIntensity) -> AuditionEmission { + match i { + AuditionRestrained => AuditionNoEmission + AuditionExpressive => AuditionEmits { + spec: EmissionSpec { + core_radius: css_px(4), + corona_radius: css_px(20), + core_alpha_pct: 60, + corona_alpha_pct: 10, + }, + } + AuditionHero => AuditionEmits { + spec: EmissionSpec { + core_radius: css_px(6), + corona_radius: css_px(48), + core_alpha_pct: 80, + corona_alpha_pct: 25, + }, + } + } +} + +type AuditionAttraction + = AuditionNoAttraction + | AuditionAttracts { field: AttractionField } + +fn audition_attraction(i: AuditionIntensity) -> AuditionAttraction { + match i { + AuditionRestrained => AuditionNoAttraction + AuditionExpressive => AuditionNoAttraction + AuditionHero => AuditionAttracts { + field: AttractionField { + activation_radius: css_px(attraction_activation_min_px), + max_travel: css_px(focal_attraction_headroom_px(p: audition_instrument(i: AuditionHero))), + settle: focal_attraction.settle, + }, + } + } +} + +fn audition_instrument(i: AuditionIntensity) -> InstrumentPreference { + match i { + AuditionRestrained => preference_still + AuditionExpressive => preference_default + AuditionHero => preference_default + } +} + +data discriminator_note: String = "The non-emission discriminator emission_for demands is not a placeholder string here: it names the channel that actually carries selection in the emitted control — the selected state class plus the subject's own name text — so a no-emission or reduced-motion rendering keeps both. Deriving it from the subject key rather than writing a literal is what stops the three intensities from silently sharing one hardcoded discriminator that belongs to none of them." + +fn focal_discriminator(subject_key: String) -> String { + concat("selected-state-class+name-text:", subject_key) +} + +data hero_travel_is_derived_note: String = "Hero used to request the register's full attraction travel while the enclosure independently carried its own six pixels, and both gates passed because neither saw the other — the review's composed-envelope finding. Its travel is now DERIVED from what the enclosure left unspent, so the loudest audition variant is by construction the largest one that still fits the single envelope. + +COMPOSING THE ENVELOPE CHANGED THE AUDITION, WHICH IS THE POINT. Expressive used to borrow the register's canonical focal_attraction — activation 150, travel 12 — and under one envelope that no longer fits: 12 of the register's 14 declared pixels are already spent by the canonical field, so an enclosure carrying any character at all cannot also grant it. Rather than shrink the canonical field or inflate the envelope, the three variants now differ by exactly one channel each: restrained has neither emission nor attraction, expressive adds emission, hero adds the attraction the enclosure left affordable. That ordering is more useful for an audition than three variants differing on everything at once, and it surfaces the real constraint instead of hiding it — the register's own focal field is expensive enough that instrument character and canonical attraction are alternatives, not companions. If that trade is wrong, the number to revisit is attraction_travel_max_px, in the register, deliberately." + +data audition_admission_note: String = "One admission per intensity, and every arm of it is the register's existing gate rather than a local re-check. A restrained variant is admitted with no emission grant to inspect; the other two must pass emission_for AT THE FOCAL ROLE, which is the point where an audition that tried to glow a Supporting subject would refuse. Instrument displacement is admitted separately because it is a property of the enclosure and not of the control, and both must hold for the variant to be renderable." + +type AuditionAdmission + = AuditionAdmitted { + intensity: String + emission: AuditionEmission + attraction: AuditionAttraction + displacement_px: Int + } + | AuditionEmissionRefused { intensity: String, grant: EmissionGrant } + | AuditionAttractionOutsideEnvelope { intensity: String } + | AuditionDisplacementOverBudget { intensity: String, total_px: Int, max_px: Int } + +fn attraction_travel_of(a: AuditionAttraction) -> Int { + match a { + AuditionNoAttraction => 0 + AuditionAttracts { field } => field.max_travel.n + } +} + +fn attraction_admissible(a: AuditionAttraction) -> Bool { + match a { + AuditionNoAttraction => true + AuditionAttracts { field } => attraction_envelope(f: field) + } +} + +data no_emission_skips_the_gate_note: String = "A restrained variant does not request emission, so it does not pass a zero-alpha spec through emission_for to obtain a grant it does not want. That shortcut was written first and is worth naming: fabricating an admissible-looking spec purely to satisfy a gate produces a REAL grant for emission nobody asked for, and the receipt then reports a granted emission on the one variant whose entire point is having none. NoEmissionRequested is a distinct outcome from a granted one, so the gate is skipped rather than gamed." + +type AuditionEmissionOutcome + = NoEmissionRequested + | EmissionResolved { grant: EmissionGrant } + +fn audition_emission_outcome( + i: AuditionIntensity, + role: SalienceRole, + subject_key: String, +) -> AuditionEmissionOutcome { + match audition_emission(i: i) { + AuditionNoEmission => NoEmissionRequested + AuditionEmits { spec } => EmissionResolved { + grant: emission_for( + role: role, + spec: spec, + discriminator: focal_discriminator(subject_key: subject_key), + ), + } + } +} + +fn emission_granted(g: EmissionGrant) -> Bool { + match g { + EmissionGranted { spec, discriminator } => true + EmissionRefusedForRole { role } => false + EmissionOutsideEnvelope { corona_alpha_pct, corona_radius_px } => false + EmissionUnitNotComparable { core_unit, corona_unit } => false + EmissionSoleDiscriminatorRefused => false + } +} + +fn admit_enclosure(i: AuditionIntensity) -> AuditionAdmission { + let key = audition_intensity_key(i: i) + let attraction = audition_attraction(i: i) + if !attraction_admissible(a: attraction) { + AuditionAttractionOutsideEnvelope { intensity: key } + } else { + match admit_composed_displacement(d: compose_displacement( + p: audition_instrument(i: i), + focal_attraction_px: attraction_travel_of(a: attraction), + )) { + DisplacementOverBudget { total_px, max_px } => + AuditionDisplacementOverBudget { intensity: key, total_px: total_px, max_px: max_px } + EnclosureCharacterReachesResponseTravel { character_px, max_px } => + AuditionDisplacementOverBudget { intensity: key, total_px: character_px, max_px: max_px } + DisplacementAdmitted { total_px } => AuditionAdmitted { + intensity: key, + emission: audition_emission(i: i), + attraction: attraction, + displacement_px: total_px, + } + } + } +} + +fn admit_audition(i: AuditionIntensity, role: SalienceRole, subject_key: String) -> AuditionAdmission { + match audition_emission_outcome(i: i, role: role, subject_key: subject_key) { + NoEmissionRequested => admit_enclosure(i: i) + EmissionResolved { grant } => + if emission_granted(g: grant) { + admit_enclosure(i: i) + } else { + AuditionEmissionRefused { intensity: audition_intensity_key(i: i), grant: grant } + } + } +} + +data audition_intensities: List = [AuditionRestrained, AuditionExpressive, AuditionHero] + +data reading_note: String = "THE CAMERA READS THE WORLD V0 ALREADY DERIVED, and the previous revision of this module did not — which is the defect worth recording rather than quietly fixing. It answered Status and Remaining out of gunbc.v1_deletion_plan's authored rows, and answered Why with a typed ReadingUnavailable carrying the cause 'no rationale carrier exists for a v1 finish line'. That cause was FALSE when it was written. gunbc.roadmap_program_view was already on this branch's base and its own header says the camera layers are deliberately absent because THAT module is the world the cameras look at; ConstraintView exists precisely to answer why-is-this-taking-so-long without inventing rationale prose. So the refusal was not the honest fail-closed arm its note claimed — it was the empty-observation narrow, rendering could-not-find as the verdict does-not-exist, in the module whose own notes warn against exactly that. It reached review green because nothing about a refusal looks wrong: no witness can tell a correct refusal from a lazy one without going and looking for the carrier, which is what nobody did. The lesson is cheap to state and was expensive here: before declaring a carrier absent, search for it." + +data reading_grain_note: String = "DEPTH SELECTS THE SUBJECT GRAIN, MODE SELECTS THE QUESTION, and the two are genuinely independent because V0 derives a RemainingShape and a ConstraintView at more than one grain. Program reads the whole program's shape — from view.remaining, at EVERY focus, which is a correction rather than a restatement: this sentence was written while read_camera_at routed a focused program detent into the line reader, so the claim held only with nothing selected and the page mislabelled outcome-grain rows as program ones (review 48719, fixed by making the program grain unrepresentable in SubjectDepth rather than by adding an arm — see subject_depth_note). Outcome reads one FinishLineView; Front reads one contributing FrontView; Node reads the primary constraint's own subject. Evidence is deliberately NOT answered from these carriers: acceptance here comes from RoadmapAcceptanceReceipt rows, but the verification-receipt join that would let a camera show WHY a receipt was granted is test-only until the belt wiring lands, and gunbc.roadmap_program_view says so itself. That is a real absence with a named trigger, so Evidence refuses — and it is the one place in this module where a refusal is the correct answer rather than a search nobody performed." + +type ProgramReading + = ReadingNoSubject + | ReadingProgramShape { remaining: RemainingShape } + | ReadingOutcomeStatus { name: String, node: String, accepted: Bool, open_fronts: Int } + | ReadingOutcomeRemaining { name: String, remaining: RemainingShape } + | ReadingConstraint { subject: String, kind: String, headline: String, in_flight: Bool, depth: Int } + | ReadingNoConstraint { subject_key: String, reason: String } + | ReadingFront { key: String, name: String, closed: Bool, gates_accepted: Int, gates_total: Int } + | ReadingUnavailable { mode: String, subject_key: String, cause: String } + +data evidence_grain_cause: String = "the verification-receipt join is test-only until the belt wiring seam lands (gunbc.roadmap_program_view records the same gap), so a camera can read THAT a node was accepted but not the evidence behind the receipt" + +data accepted_subject_has_no_constraint_reason: String = "the subject is accepted, so its closure holds no unresolved constraint — this is an answer, not a missing carrier" + +data no_workable_frontier_reason: String = "no workable frontier remains in the subject's unaccepted closure" + +fn constraint_kind_key(k: ConstraintKind) -> String { + match k { + ImplementationConstraint => "implementation" + ContractConstraint => "contract" + } +} + +fn read_constraint(subject_key: String, c: ConstraintView?, accepted: Bool) -> ProgramReading { + match c { + Absent => ReadingNoConstraint { + subject_key: subject_key, + reason: if accepted { accepted_subject_has_no_constraint_reason } else { no_workable_frontier_reason }, + } + Present { value } => ReadingConstraint { + subject: value.subject as String, + kind: constraint_kind_key(k: value.kind), + headline: value.headline, + in_flight: value.in_flight, + depth: value.depth, + } + } +} + +data subject_depth_note: String = "THE GRAIN THE LINE READER IS ALLOWED TO ANSWER AT, as a type rather than as a promise (review 48719, 2026-08-05). The bug it closes: read_line_view used to match ProgramDepth, so it carried a DepthProgram arm — and that arm was byte-identical to its DepthOutcome arm. read_camera_at then routed BOTH depths into it whenever a subject was focused, so the program detent silently produced outcome-grain readings while the page kept labelling the row program / …, and reading_grain_note's claim that Program reads the whole program's shape was true only when nothing was selected. That is the note-vs-code split this module has now produced three times, so the fix is not another corrected arm: the whole-program grain has no representation here at all. SubjectDepth enumerates exactly the grains that ARE a property of one finish line, DepthProgram cannot be projected into it, and read_line_view therefore cannot be handed the program grain by any caller. A DepthFront arm went with it, dead for a different reason — read_camera_at answers fronts through first_front_view, so the line reader's front arm had been unreachable since that fold landed." + +type SubjectDepth + = SubjectOutcome + | SubjectNode + | SubjectEvidence + +fn read_line_view(lv: FinishLineView, camera: ProgramCamera, d: SubjectDepth) -> ProgramReading { + match d { + SubjectOutcome => match camera.mode { + ModeStatus => ReadingOutcomeStatus { + name: lv.name, + node: lv.node as String, + accepted: lv.accepted, + open_fronts: lv.remaining.open_fronts, + } + ModeRemaining => ReadingOutcomeRemaining { name: lv.name, remaining: lv.remaining } + ModeWhy => read_constraint(subject_key: lv.key, c: lv.constraint, accepted: lv.accepted) + } + SubjectNode => read_constraint(subject_key: lv.key, c: lv.constraint, accepted: lv.accepted) + SubjectEvidence => ReadingUnavailable { + mode: program_mode_key(m: camera.mode), + subject_key: lv.key, + cause: evidence_grain_cause, + } + } +} + +data front_grain_note: String = "At front depth the camera shows the contributing fronts V0 derived for this outcome, and it shows the FIRST one rather than a list because a single reading is one answer — a camera at a grain reports the subject in view. Which front is in view is a tuning axis the operable instrument owns; this study fixes it at the first contributing front so the grain is genuinely different from Outcome rather than a relabelled copy of it. + +FIRST IS ENFORCED BY THE FOLD, NOT PROMISED BY THIS PARAGRAPH (review finding 48579, 2026-08-05). The first cut folded the contributing fronts with a step that ignored its accumulator, so the LAST match won while this note said first — and it was not hypothetical: the exemplar subject contributes to namespace-pderive and then v2-generation, so the study rendered the wrong front. A fold whose step drops acc is a last-wins selection wearing a first-wins comment, and nothing caught it because no witness read the front grain at all. Selection is now a separate take-first over the list, so the reading step cannot express a preference between candidates, and witness_the_front_grain_shows_the_first_contributing_front reads the rendered key." + +fn front_view_for(lv: FinishLineView, fronts: List) -> List { + fronts |> filter(fv => lv.contributing_fronts |> any(f => program_front_key(front: f) == fv.key)) +} + +fn first_front_view(lv: FinishLineView, fronts: List) -> List { + fold(front_view_for(lv: lv, fronts: fronts), init: [], + f: (acc, fv) => if count(acc) == 0 { [fv] } else { acc }) +} + +fn read_front_view(fv: FrontView, camera: ProgramCamera) -> ProgramReading { + match camera.mode { + ModeStatus => ReadingFront { + key: fv.key, + name: fv.name, + closed: fv.closed, + gates_accepted: fv.gates_accepted, + gates_total: fv.gates_total, + } + ModeRemaining => ReadingOutcomeRemaining { name: fv.name, remaining: fv.remaining } + ModeWhy => read_constraint(subject_key: fv.key, c: fv.constraint, accepted: fv.closed) + } +} + +data no_contributing_front_cause: String = "no convergence front contributes to this finish line in the derived view" + +fn read_front(lv: FinishLineView, camera: ProgramCamera) -> ProgramReading { + ReadingUnavailable { + mode: program_mode_key(m: camera.mode), + subject_key: lv.key, + cause: no_contributing_front_cause, + } +} + +data unresolved_subject_cause: String = "the focused subject key resolves to no finish line in the derived program view" + +fn line_view_for(view: V1DeletionProgramView, subject_key: String) -> List { + view.finish_lines |> filter(lv => lv.key == subject_key) +} + +fn first_line_view(view: V1DeletionProgramView, subject_key: String) -> List { + fold(line_view_for(view: view, subject_key: subject_key), init: [], + f: (acc, lv) => if count(acc) == 0 { [lv] } else { acc }) +} + +fn read_program_depth(view: V1DeletionProgramView, camera: ProgramCamera) -> ProgramReading { + match camera.mode { + ModeRemaining => ReadingProgramShape { remaining: view.remaining } + ModeStatus => ReadingProgramShape { remaining: view.remaining } + ModeWhy => ReadingUnavailable { + mode: "why", + subject_key: "v1-deletion-program", + cause: no_workable_frontier_reason, + } + } +} + +fn read_camera(camera: ProgramCamera, view: V1DeletionProgramView) -> ProgramReading { + match camera.focus { + NoSubjectSelected => match camera.depth { + DepthProgram => read_program_depth(view: view, camera: camera) + DepthOutcome => ReadingNoSubject + DepthFront => ReadingNoSubject + DepthNode => ReadingNoSubject + DepthEvidence => ReadingNoSubject + } + FinishLineFocused { line_key } => fold( + first_line_view(view: view, subject_key: line_key), + init: ReadingUnavailable { + mode: program_mode_key(m: camera.mode), + subject_key: line_key, + cause: unresolved_subject_cause, + }, + f: (acc, lv) => read_camera_at(lv: lv, camera: camera, view: view), + ) + } +} + +fn read_camera_at(lv: FinishLineView, camera: ProgramCamera, view: V1DeletionProgramView) -> ProgramReading { + match camera.depth { + DepthFront => fold( + first_front_view(lv: lv, fronts: view.fronts), + init: read_front(lv: lv, camera: camera), + f: (acc, fv) => read_front_view(fv: fv, camera: camera), + ) + DepthProgram => read_program_depth(view: view, camera: camera) + DepthOutcome => read_line_view(lv: lv, camera: camera, d: SubjectOutcome) + DepthNode => read_line_view(lv: lv, camera: camera, d: SubjectNode) + DepthEvidence => read_line_view(lv: lv, camera: camera, d: SubjectEvidence) + } +} + +fn reading_key(r: ProgramReading) -> String { + match r { + ReadingNoSubject => "no-subject" + ReadingProgramShape { remaining } => "program-shape" + ReadingOutcomeStatus { name, node, accepted, open_fronts } => "status" + ReadingOutcomeRemaining { name, remaining } => "remaining" + ReadingConstraint { subject, kind, headline, in_flight, depth } => "constraint" + ReadingNoConstraint { subject_key, reason } => "no-constraint" + ReadingFront { key, name, closed, gates_accepted, gates_total } => "front" + ReadingUnavailable { mode, subject_key, cause } => "unavailable" + } +} diff --git a/dag/gunbc/design/instrument_camera.dag b/dag/gunbc/design/instrument_camera.dag new file mode 100644 index 00000000000..4743376d5ef --- /dev/null +++ b/dag/gunbc/design/instrument_camera.dag @@ -0,0 +1,164 @@ +module gunbc.design.instrument_camera + +import std.types { String, Bool, Int, List } +import gunbc.v1_deletion_plan { V1FinishLine, v1_finish_line_key } + +data state_ownership_note: String = "FOUR OWNERS, AND THE SPLIT IS THE WHOLE POINT (instrument wave, operator directive 2026-08-04). Before physical-device input can drive presentation, it has to be impossible for it to drive anything else. The authoritative program view is V0's derived v1-deletion facts and this module NEVER writes it — no fn here returns a finish line, an acceptance, or a roadmap edge. Local instrument state is what the person operating the instrument chose: which subject is selected, how deep the camera sits, which mode it reads. Instrument observation is what the world told us: whether a sensor exists, whether permission was granted, whether an impulse arrived. Renderer ephemera is plate position, velocity, glow interpolation, glitch phase — none of it modelled here at all, because it is per-frame and belongs to the realization. The law that makes the split real rather than a naming convention: a ProgramCamera carries only a depth, a mode, and a focus KEY, so it structurally cannot hold a program fact to corrupt." + +type StateOwner + = AuthoritativeProgramView + | LocalInstrumentState + | InstrumentObservation + | RendererEphemera + +fn state_owner_key(o: StateOwner) -> String { + match o { + AuthoritativeProgramView => "authoritative-program-view" + LocalInstrumentState => "local-instrument-state" + InstrumentObservation => "instrument-observation" + RendererEphemera => "renderer-ephemera" + } +} + +data owner_write_authority_note: String = "Which owner may WRITE a domain fact: exactly one, and it is not reachable from the instrument. This is the predicate the physical-input lane needs, because 'a tap changed the screen' and 'a tap changed the program' differ only by whether the writing owner was authoritative — and the tap's owner never is." + +fn owner_may_write_domain_fact(o: StateOwner) -> Bool { + match o { + AuthoritativeProgramView => true + LocalInstrumentState => false + InstrumentObservation => false + RendererEphemera => false + } +} + +data depth_note: String = "The semantic camera's one axis, ordered outermost to innermost. The variants carry a Depth stem because a bare-name identifier is a corpus-wide name in this substrate, not a module-local one — an unprefixed Node variant would have collided head-on with the substrate's own Node type, which is the nicknaming violation before it is ever a resolution hazard. It is a DEPTH, not a zoom: each position is a discrete detent with its own subject grain, so there is no continuous scale and no arbitrary pan. History is deliberately absent — a mode that cannot be answered from a real historical projection would be a fabricated affordance, and the directive names it as out of scope until one exists." + +type ProgramDepth + = DepthProgram + | DepthOutcome + | DepthFront + | DepthNode + | DepthEvidence + +fn program_depth_key(d: ProgramDepth) -> String { + match d { + DepthProgram => "program" + DepthOutcome => "outcome" + DepthFront => "front" + DepthNode => "node" + DepthEvidence => "evidence" + } +} + +fn program_depth_index(d: ProgramDepth) -> Int { + match d { + DepthProgram => 0 + DepthOutcome => 1 + DepthFront => 2 + DepthNode => 3 + DepthEvidence => 4 + } +} + +data depth_ordering_note: String = "program_depth_index exists so a detent crossing is DERIVED rather than authored: one wheel threshold or one arrow key moves the index by exactly one, and the dial's rendered position is the index. Authoring a per-pair transition table would be the same ordering said twice." + +data depth_detent_step_note: String = "A depth change crosses AT MOST ONE detent, by construction: step_depth takes a direction, not a target, so no caller can jump from the outermost detent to the innermost in one gesture and no continuous zoom can exist. Clamping at the ends is deliberate and is not an absorbing fallback — the request is fully answered ('you are already at the outermost detent'), nothing is widened, and a caller that wants to know whether it moved compares the returned depth." + +type DepthStep + = Inward + | Outward + +fn step_depth(d: ProgramDepth, step: DepthStep) -> ProgramDepth { + match step { + Inward => match d { + DepthProgram => DepthOutcome + DepthOutcome => DepthFront + DepthFront => DepthNode + DepthNode => DepthEvidence + DepthEvidence => DepthEvidence + } + Outward => match d { + DepthProgram => DepthProgram + DepthOutcome => DepthProgram + DepthFront => DepthOutcome + DepthNode => DepthFront + DepthEvidence => DepthNode + } + } +} + +type ProgramMode + = ModeStatus + | ModeRemaining + | ModeWhy + +fn program_mode_key(m: ProgramMode) -> String { + match m { + ModeStatus => "status" + ModeRemaining => "remaining" + ModeWhy => "why" + } +} + +data focus_is_a_key_not_a_fact_note: String = "FocusSubject carries the finish line's KEY, not its spec. That is what keeps the camera structurally unable to hold a program fact: a key is an identity the authoritative view can resolve, while a spec would be a copy of V0's claim living in local state, free to drift from the thing it names. Selecting nothing is a real state — the instrument opens with no subject chosen — so it is a variant rather than an empty string." + +type FocusSubject + = NoSubjectSelected + | FinishLineFocused { line_key: String } + +fn focus_subject_key(f: FocusSubject) -> String { + match f { + NoSubjectSelected => "none" + FinishLineFocused { line_key } => line_key + } +} + +fn focus_finish_line(l: V1FinishLine) -> FocusSubject { + FinishLineFocused { line_key: v1_finish_line_key(l: l) } +} + +fn focus_subject_eq(a: FocusSubject, b: FocusSubject) -> Bool { + focus_subject_key(f: a) == focus_subject_key(f: b) +} + +type ProgramCamera { + depth: ProgramDepth + mode: ProgramMode + focus: FocusSubject +} + +data camera_opens_outermost_note: String = "The instrument opens at the outermost depth in Status mode with nothing selected — no subject is preselected, because a preselected subject is a claim about what matters that the program did not make." + +data camera_initial: ProgramCamera = ProgramCamera { + depth: DepthProgram, + mode: ModeStatus, + focus: NoSubjectSelected, +} + +fn camera_step_depth(c: ProgramCamera, step: DepthStep) -> ProgramCamera { + ProgramCamera { depth: step_depth(d: c.depth, step: step), mode: c.mode, focus: c.focus } +} + +fn camera_set_mode(c: ProgramCamera, m: ProgramMode) -> ProgramCamera { + ProgramCamera { depth: c.depth, mode: m, focus: c.focus } +} + +data selection_toggles_note: String = "Re-selecting the selected subject clears it, matching the production roadmap's row-selection rule so the two surfaces do not teach different gestures for the same act." + +fn camera_select(c: ProgramCamera, f: FocusSubject) -> ProgramCamera { + if focus_subject_eq(a: c.focus, b: f) { + ProgramCamera { depth: c.depth, mode: c.mode, focus: NoSubjectSelected } + } else { + ProgramCamera { depth: c.depth, mode: c.mode, focus: f } + } +} + +data camera_cannot_touch_the_program_note: String = "THE LAW THE PHYSICAL LANE DEPENDS ON, stated as a predicate over the camera's own shape rather than as a promise: every camera transition above returns a ProgramCamera built from a depth, a mode and a focus key, so no transition can carry a roadmap node, an acceptance, or a finish-line claim. A tap, a wheel, a key, or a pointer can therefore move the camera and nothing else. What this does NOT prove is that a RENDERER refrains from writing elsewhere; that is the renderer's own obligation and is witnessed at its own seam." + +fn camera_preserves_subject_across_depth(c: ProgramCamera, step: DepthStep) -> Bool { + focus_subject_eq(a: camera_step_depth(c: c, step: step).focus, b: c.focus) +} + +fn camera_preserves_subject_across_mode(c: ProgramCamera, m: ProgramMode) -> Bool { + focus_subject_eq(a: camera_set_mode(c: c, m: m).focus, b: c.focus) +} diff --git a/dag/gunbc/design/instrument_physical.dag b/dag/gunbc/design/instrument_physical.dag new file mode 100644 index 00000000000..188b4eb3178 --- /dev/null +++ b/dag/gunbc/design/instrument_physical.dag @@ -0,0 +1,287 @@ +module gunbc.design.instrument_physical + +import std.types { String, Bool, Int, List } +import std.integer { Nat } +import gunbc.design.material { TimingToken, respond_fast, restore_gentle } +import gunbc.design.salience { attraction_travel_max_px } +import gunbc.design.reference_instrument { + InstrumentBehaviourAxis, OpticalInstability, RestingOffsetCalibration, + ImpulseGlitch, BuoyantDrift, AxisProvenance, axis_provenance, axis_is_originated, +} + +data physical_character_note: String = "THE ENCLOSING INSTRUMENT MAY HAVE PHYSICAL CHARACTER; THE CAUSAL WORLD MAY NOT. This is the register amendment the audition needs, and the line it draws is the whole content: still-until-touched governs the SUBJECTS — a roadmap node, a finish line, an operation never moves without a cause — while the instrument ENCLOSING them is a physical object whose glass, phosphor and chassis have their own idle behaviour. A CRT that sits perfectly still is not restraint, it is a picture of a CRT. So drift, jitter, vertical shift and impulse glitch are admitted HERE and nowhere else, under three conditions that make them incapable of lying: every effect displaces or perturbs the instrument's own presentation layer and can carry no domain fact; every effect is preference-controlled and its off position is total; and the composed displacement is bounded below the register's existing attraction travel, so instrument character can never move a subject as far as a real response does. The reference precedent travels as a typed edge into gunbc.design.reference_instrument rather than as prose here — see provenance_edge_note and channel_behaviour_axis below." + +data preference_off_is_total_note: String = "EVERY CHANNEL'S OFF POSITION IS TOTAL, and that is a construction property rather than a promise: instrument_displacement_px returns zero for a disabled channel by matching the preference, so a realization reading the composed budget receives no displacement to apply. There is no global escape hatch and no 'reduced' middle mode that leaves a residue — a channel is off or it is at its declared amplitude." + +type InstrumentChannel + = ChannelOpticalJitter + | ChannelVerticalShift + | ChannelBuoyantDrift + | ChannelImpulseGlitch + +fn channel_key(c: InstrumentChannel) -> String { + match c { + ChannelOpticalJitter => "optical-jitter" + ChannelVerticalShift => "vertical-shift" + ChannelBuoyantDrift => "buoyant-drift" + ChannelImpulseGlitch => "impulse-glitch" + } +} + +data channel_carries_no_domain_fact_note: String = "The predicate the whole amendment rests on, stated over the channel set rather than per site: NO instrument channel may carry a domain fact. It is total and constantly false because that is the claim — if a fifth channel is ever added that DOES carry meaning, this match forces the author to write the arm and a reviewer sees a true in a function whose name says there should not be one. That is cheaper and louder than a lens over the same set." + +fn channel_may_carry_domain_fact(c: InstrumentChannel) -> Bool { + match c { + ChannelOpticalJitter => false + ChannelVerticalShift => false + ChannelBuoyantDrift => false + ChannelImpulseGlitch => false + } +} + +data glitch_vocabulary_note: String = "WE ADOPTED THE UPSTREAM'S WORD AND CHANGED ITS MEANING, WHICH IS WORSE THAN NOT ADOPTING IT (review finding, 2026-08-05). The first cut declared GlitchOff / GlitchShort / GlitchPersistent and claimed the set was taken verbatim from the cited Pip-Boy 3000's Glitch-on-tap setting — then defined Persistent as a slightly longer decay. The upstream word does not mean that. A persistent glitch on the reference device is a LATCHED out-of-sync display state that stays wrong until a later tap reseats it, which is precisely the unnecessary tactile detail that makes the thing read as equipment rather than as a themed screen. Redefining a cited word to mean the nearest thing we had implemented is nicknaming pointed at the upstream: a reader who trusts the adoption claim gets a fact that is false about the device. + +So the local vocabulary now says what it actually does. ImpulseOff and ImpulseBrief and ImpulseLong are transient decays of our own, named as ours. The cited Persistent behaviour is NOT adopted and is not silently approximated by ImpulseLong — it is a distinct interaction (latch, hold, reseat on a later impulse) that this study does not model. DISSOLVE-ON: a latched glitch state lands with the operable instrument, at which point it carries the upstream's own word because it will finally mean the same thing. The cited rows themselves live in extdeps.instrument.pip_boy_3000 and are referenced below rather than restated." + +type ImpulseGlitchDuration + = ImpulseOff + | ImpulseBrief + | ImpulseLong + +fn glitch_duration_key(g: ImpulseGlitchDuration) -> String { + match g { + ImpulseOff => "off" + ImpulseBrief => "brief" + ImpulseLong => "long" + } +} + +data latched_glitch_not_modelled_note: String = "The gap left by the correction above, stated so it is countable rather than forgotten: no arm of this type latches. Every value here decays on the settle timing, so an impulse cannot leave the display in a wrong state that a later impulse reseats. That is a missing INTERACTION, not a missing duration, which is why lengthening ImpulseLong would not close it." + +fn glitch_is_armed(g: ImpulseGlitchDuration) -> Bool { + match g { + ImpulseOff => false + ImpulseBrief => true + ImpulseLong => true + } +} + +fn glitch_settle(g: ImpulseGlitchDuration) -> TimingToken { + match g { + ImpulseOff => respond_fast + ImpulseBrief => respond_fast + ImpulseLong => restore_gentle + } +} + +data amplitude_note: String = "AN AMPLITUDE IS A NONNEGATIVE MAGNITUDE, and the first cut got this wrong in a way worth recording: the field was a bare Int and the composed total was a signed sum, so a large positive disturbance could be CANCELLED by a negative one and the pair admitted under the ceiling. That is the budget defeating itself — the review finding that caught it is the same shape as an accounting check that nets debits against credits and reports zero exposure. The carrier is now std.integer Nat, so a negative amplitude has no literal that constructs it rather than a guard that catches it downstream. A resting offset that genuinely points somewhere — a vertical calibration, say — is a direction plus a magnitude and is a different fact from this one; it is not modelled here and must not be smuggled in as a negative amplitude. Amplitudes stay px-denominated integers matching the register's existing attraction bounds: there is no CssLength here and therefore no unit straddle to guard, which is the honest reason this module carries no unit-comparability refusal while gunbc.design.salience does." + +type ChannelAmplitude + = ChannelDisabled + | ChannelAmplitudePx { px: Nat } + +fn amplitude_px(a: ChannelAmplitude) -> Int { + match a { + ChannelDisabled => 0 + ChannelAmplitudePx { px } => px + } +} + +type InstrumentPreference { + optical_jitter: ChannelAmplitude + vertical_shift: ChannelAmplitude + buoyant_drift: ChannelAmplitude + impulse_glitch: ChannelAmplitude + glitch_duration: ImpulseGlitchDuration +} + +data preference_still_note: String = "The all-off preference is a real, reachable configuration and not a degraded one: an instrument with every channel disabled is exactly the register's prior still surface, so the amendment strictly adds a lane rather than changing what the quiet setting produces." + +data preference_still: InstrumentPreference = InstrumentPreference { + optical_jitter: ChannelDisabled, + vertical_shift: ChannelDisabled, + buoyant_drift: ChannelDisabled, + impulse_glitch: ChannelDisabled, + glitch_duration: ImpulseOff, +} + +data preference_default_note: String = "The shipped default is deliberately restrained rather than the reference product's full character: one px of optical jitter and two of buoyant drift are perceptible as life without being perceptible as motion, vertical shift is off because a rolling frame reads as a fault rather than as character, and the impulse glitch is armed at short because it only ever fires on a real physical impulse." + +data preference_default: InstrumentPreference = InstrumentPreference { + optical_jitter: ChannelAmplitudePx { px: 1 }, + vertical_shift: ChannelDisabled, + buoyant_drift: ChannelAmplitudePx { px: 2 }, + impulse_glitch: ChannelAmplitudePx { px: 3 }, + glitch_duration: ImpulseBrief, +} + +fn channel_amplitude(p: InstrumentPreference, c: InstrumentChannel) -> ChannelAmplitude { + match c { + ChannelOpticalJitter => p.optical_jitter + ChannelVerticalShift => p.vertical_shift + ChannelBuoyantDrift => p.buoyant_drift + ChannelImpulseGlitch => p.impulse_glitch + } +} + +data displacement_budget_note: String = "ONE ENVELOPE OVER EVERYTHING THAT MOVES THE PLATE. The first cut bounded the four enclosure channels against the register's attraction travel and stopped there, which left the exact hole the review found: the focal plate's own attraction was admitted by a SEPARATE gate that could not see the enclosure, so a hero control could request the full attraction travel while the enclosure independently carried its whole character budget, each gate passing while the plate visibly moved farther than either bound describes. Two gates that each see half the motion do not bound the motion. So the envelope is now composed over every positional contribution at once — enclosure character, focal attraction, and the impulse transient — and the sub-budgets have to fit inside it rather than beside it. + +TWO RULES, STATED ONCE SO THE PROSE AND THE ARITHMETIC CANNOT DISAGREE (the review's second finding: the note said 'below' while the check refused only on strictly greater, so equality was quietly admissible). Rule one: the COMPOSED total may spend the envelope fully — admitted at or below, refused strictly above — because the envelope IS the register's declared maximum plate travel and a budget you may not spend to its stated limit is a mislabelled budget. Rule two: enclosure character ALONE must stay strictly below the envelope, because character that reaches the full travel of a real focal response is exactly the imitation the amendment exists to prevent. The first rule is an ordinary ceiling; the second is the one that carries the safety claim, and they differ deliberately." + +data instrument_displacement_max_px: Int = attraction_travel_max_px + +fn instrument_displacement_px(p: InstrumentPreference) -> Int { + amplitude_px(a: p.optical_jitter) + + amplitude_px(a: p.vertical_shift) + + amplitude_px(a: p.buoyant_drift) + + amplitude_px(a: p.impulse_glitch) +} + +data composed_displacement_note: String = "Every positional contribution the register can grant a single subject, carried as nonnegative magnitudes so the sum cannot cancel. focal_attraction_px is the plate travel a focal control may be granted; it is zero for a subject with no attraction. The record has no direction field on purpose: a direction would let two contributions be argued to oppose, which is how a composed budget gets talked out of being composed." + +type ComposedVisualDisplacement { + enclosure_character_px: Nat + focal_attraction_px: Nat + impulse_transient_px: Nat +} + +fn composed_total_px(d: ComposedVisualDisplacement) -> Int { + d.enclosure_character_px + d.focal_attraction_px + d.impulse_transient_px +} + +type DisplacementAdmission + = DisplacementAdmitted { total_px: Int } + | DisplacementOverBudget { total_px: Int, max_px: Int } + | EnclosureCharacterReachesResponseTravel { character_px: Int, max_px: Int } + +fn compose_displacement(p: InstrumentPreference, focal_attraction_px: Nat) -> ComposedVisualDisplacement { + ComposedVisualDisplacement { + enclosure_character_px: amplitude_px(a: p.optical_jitter) + + amplitude_px(a: p.vertical_shift) + + amplitude_px(a: p.buoyant_drift), + focal_attraction_px: focal_attraction_px, + impulse_transient_px: amplitude_px(a: p.impulse_glitch), + } +} + +data enclosure_character_px_note: String = "Character is the IDLE contribution — jitter, shift, drift — and deliberately excludes the impulse transient, because the impulse only fires on a real physical cause and is therefore not the thing that could be mistaken for an unprompted response. The transient still counts against the composed total, since a transient that overruns the envelope is still a plate leaving its declared travel." + +fn admit_composed_displacement(d: ComposedVisualDisplacement) -> DisplacementAdmission { + let total = composed_total_px(d: d) + if d.enclosure_character_px >= instrument_displacement_max_px { + EnclosureCharacterReachesResponseTravel { + character_px: d.enclosure_character_px, + max_px: instrument_displacement_max_px, + } + } else if total > instrument_displacement_max_px { + DisplacementOverBudget { total_px: total, max_px: instrument_displacement_max_px } + } else { + DisplacementAdmitted { total_px: total } + } +} + +data focal_attraction_headroom_note: String = "The travel a focal control may still be granted once the enclosure has spent its share — DERIVED, so an audition cannot silently keep its old number when the enclosure's default changes, and cannot author an attraction that overruns the composed envelope FOR ANY PREFERENCE THE ENVELOPE ADMITS. That qualifier is the honest limit of the claim and it is stated because the first version of this note omitted it (self-audit, 2026-08-05). The subtraction is total on Int, not on Nat: a preference whose channels sum past instrument_displacement_max_px yields a NEGATIVE headroom, and the composed record's focal_attraction_px is a Nat whose refinement is not re-checked on a computed value, so the sign-cancellation class this module closed at the field is still reachable through the derived path. It is not reached today — preference_default spends 6 of 14 — and the configuration that would reach it is already refused by displacement_admission's EnclosureCharacterReachesResponseTravel arm, so the residual risk is that a caller reads headroom WITHOUT consulting that admission first. Rung: mechanically preventable, not structurally guaranteed; the ceiling is structural impossibility and the gap is one function's return type. NEXT-RUNG TRIGGER (DESIGN 4b, no untracked stall): headroom returns a typed HeadroomAvailable { px: Nat } | HeadroomUnavailable coproduct rather than a bare Int, so a caller cannot obtain a number at all when the enclosure has overspent — at which point this paragraph collapses back to the one-sentence construction claim it originally made." + +fn focal_attraction_headroom_px(p: InstrumentPreference) -> Int { + instrument_displacement_max_px - instrument_displacement_px(p: p) +} + +fn displacement_admission(p: InstrumentPreference) -> DisplacementAdmission { + admit_composed_displacement(d: compose_displacement(p: p, focal_attraction_px: 0)) +} + +data provenance_edge_note: String = "THE PROVENANCE IS A TYPED EDGE NOW, NOT A PARAGRAPH. The first cut described the Pip-Boy precedent in prose and carried a DISSOLVE-ON saying the citation edge would arrive when the reference join reached main. It has (gunbc.design.reference_instrument, merged), so the prose is replaced by the edge it promised: every channel names the agnostic behaviour axis it inhabits, and that axis carries its own provenance — cited on a real declaration inside a product module, or originated here. Nothing in this module restates what the upstream shipped; it points at the join that does. ChannelBuoyantDrift resolving to an OriginatedHere axis is the case that makes the edge worth having: the drift is OURS, no reference product realizes it, and the edge says so rather than letting a reader assume the whole set was borrowed." + +fn channel_behaviour_axis(c: InstrumentChannel) -> InstrumentBehaviourAxis { + match c { + ChannelOpticalJitter => OpticalInstability + ChannelVerticalShift => RestingOffsetCalibration + ChannelBuoyantDrift => BuoyantDrift + ChannelImpulseGlitch => ImpulseGlitch + } +} + +fn channel_provenance(c: InstrumentChannel) -> AxisProvenance { + axis_provenance(a: channel_behaviour_axis(c: c)) +} + +fn channel_is_cited_precedent(c: InstrumentChannel) -> Bool { + !axis_is_originated(axis: channel_behaviour_axis(c: c)) +} + +data impulse_source_note: String = "NOT ANCHORED TO A BROWSER (operator standing directive: focus on the vision, then work backwards to what is available). An accelerometer is a HOST capability, so the variants name the capability and not the runtime that exposes it — HostAccelerometer and HostDeviceMotion are equally inhabited by a browser sensor API, a desktop application's platform binding, or a physical enclosure's own hardware, and choosing a desktop realization later adds a binding row rather than editing this coproduct. SyntheticImpulse is not a fallback for a missing sensor: it is the audition path, an authored impulse that lets the glitch be designed, reviewed and witnessed on a machine that has no accelerometer at all, which is every CI runner." + +type PhysicalImpulseSource + = SyntheticImpulse + | HostAccelerometer + | HostDeviceMotion + +fn impulse_source_key(s: PhysicalImpulseSource) -> String { + match s { + SyntheticImpulse => "synthetic" + HostAccelerometer => "host-accelerometer" + HostDeviceMotion => "host-device-motion" + } +} + +data sensor_availability_note: String = "FIVE STATES, BECAUSE THE THREE THAT GET COLLAPSED ARE THE ONES THAT MATTER. A sensor that is absent, one that exists but has not been asked for, one whose permission was refused, and one we could not interrogate are four different worlds with four different remedies, and every one of them is routinely flattened into a single falsy 'no sensor' — the empty-observation narrow, rendering could-not-observe as the verdict nothing-is-there. SensorAvailabilityUnknown is therefore NOT a synonym for absent: sensor_may_deliver_impulses admits only SensorPresent, so an uninterrogated sensor delivers nothing while remaining visibly distinct from one that is genuinely missing, and a surface can honestly say which." + +type SensorAvailability + = SensorPresent + | SensorAbsent + | SensorPermissionNotRequested + | SensorPermissionDenied + | SensorAvailabilityUnknown + +fn sensor_availability_key(a: SensorAvailability) -> String { + match a { + SensorPresent => "present" + SensorAbsent => "absent" + SensorPermissionNotRequested => "permission-not-requested" + SensorPermissionDenied => "permission-denied" + SensorAvailabilityUnknown => "availability-unknown" + } +} + +fn sensor_may_deliver_impulses(a: SensorAvailability) -> Bool { + match a { + SensorPresent => true + SensorAbsent => false + SensorPermissionNotRequested => false + SensorPermissionDenied => false + SensorAvailabilityUnknown => false + } +} + +data impulse_admission_note: String = "An impulse is admitted only when its SOURCE is available and the glitch channel is armed, and the refusal says which of the two failed rather than returning a bare false. The synthetic source is always available because it is authored input, which is what keeps the audition runnable on hardware that has no sensor — and it is a source in its own right rather than a simulation of one, so nothing here pretends a reading occurred." + +type ImpulseAdmission + = ImpulseAdmitted { source: String, settle: TimingToken } + | ImpulseSourceUnavailable { source: String, availability: String } + | ImpulseChannelDisabled { source: String } + +fn source_availability(s: PhysicalImpulseSource, sensor: SensorAvailability) -> SensorAvailability { + match s { + SyntheticImpulse => SensorPresent + HostAccelerometer => sensor + HostDeviceMotion => sensor + } +} + +fn admit_impulse( + p: InstrumentPreference, + s: PhysicalImpulseSource, + sensor: SensorAvailability, +) -> ImpulseAdmission { + let availability = source_availability(s: s, sensor: sensor) + if !sensor_may_deliver_impulses(a: availability) { + ImpulseSourceUnavailable { + source: impulse_source_key(s: s), + availability: sensor_availability_key(a: availability), + } + } else if amplitude_px(a: p.impulse_glitch) == 0 || !glitch_is_armed(g: p.glitch_duration) { + ImpulseChannelDisabled { source: impulse_source_key(s: s) } + } else { + ImpulseAdmitted { source: impulse_source_key(s: s), settle: glitch_settle(g: p.glitch_duration) } + } +} diff --git a/dag/gunbc/design/instrument_projection.dag b/dag/gunbc/design/instrument_projection.dag new file mode 100644 index 00000000000..34459135930 --- /dev/null +++ b/dag/gunbc/design/instrument_projection.dag @@ -0,0 +1,115 @@ +module gunbc.design.instrument_projection + +import std.types { String, Bool, Int, List } +import std.integer { PositiveInt } +import gunbc.design.salience { + SalienceRole, SalienceAssignment, SalienceGround, SalienceSupporting, + SalienceFocal, SalienceCritical, FocalAdmission, region_focal_admission, +} +import gunbc.design.instrument_camera { + ProgramCamera, FocusSubject, NoSubjectSelected, FinishLineFocused, + focus_subject_key, focus_finish_line, +} +import gunbc.v1_deletion_plan { V1FinishLineSpec, v1_exit_finish_lines, v1_finish_line_key } + +data projection_note: String = "THE PROJECTION THAT DECIDES A ROLE FROM REAL FACTS, firing gunbc.design.salience salience_note's declared dissolve-on. Until this landed, every SalienceRole in the corpus arrived as a hand-supplied input, so the budget table, the focal-admission fold, and the emission envelope were all lawful over roles NOBODY DERIVED — the section 6 coverage-by-illusion tier, one layer up from an inert lens. What decides a role here is the camera's selection and the region a subject sits in, and nothing else: there is no per-subject importance field, no authored priority, and no way for a caller to hand a role in. The four rules are exactly the operator's: the selected subject is Focal, the subjects sharing its region are Supporting, everything outside that region is Ground, and an active refusal needing action is Critical." + +data subject_placement_note: String = "A subject is a KEY and the REGION it occupies — the two facts the projection needs and no more. It deliberately does not carry the subject's claim, status, or acceptance: the projection decides visual energy, and a projection that could read a claim could make energy mean truth, which is precisely the fabricated affordance the register forbids." + +type SubjectPlacement { + key: String + region: String +} + +data refusal_is_aggregated_note: String = "AN ACTIVE REFUSAL IS ONE CRITICAL SUBJECT, NOT ONE PER REFUSAL (operator directive). Critical is the interrupt channel — strong chroma, admissible emission, sharp motion — so granting it per refusal would let a five-refusal state light five objects and destroy the calm field the register's whole thesis rests on. The count travels as data on the single aggregate so the surface can say how many without spending five energy budgets. NoActiveRefusal is a variant rather than a zero count because 'nothing is refusing' and 'something is refusing, zero times' are different states; the count is a std.integer PositiveInt so the second one has no literal that constructs it, rather than a guard that catches it after the fact." + +type RefusalAggregate + = NoActiveRefusal + | ActiveRefusals { refused_count: PositiveInt } + +fn refusal_count(r: RefusalAggregate) -> Int { + match r { + NoActiveRefusal => 0 + ActiveRefusals { refused_count } => refused_count + } +} + +data refusal_subject_key: String = "active-refusals" + +fn subject_region(placements: List, key: String) -> String { + fold(placements, init: "", f: (acc, p) => if p.key == key { p.region } else { acc }) +} + +data focal_region_note: String = "With nothing selected there is no focal region, so no subject can be Supporting-by-sibling and the whole field reads Ground. That is the correct still state rather than a degenerate one: the instrument opens with the energy unspent, and the first selection is what spends it." + +fn focal_region(camera: ProgramCamera, placements: List) -> String { + match camera.focus { + NoSubjectSelected => "" + FinishLineFocused { line_key } => subject_region(placements: placements, key: line_key) + } +} + +fn placement_role(p: SubjectPlacement, focus_key: String, focus_region: String) -> SalienceRole { + if p.key == focus_key { + SalienceFocal + } else if focus_region != "" && p.region == focus_region { + SalienceSupporting + } else { + SalienceGround + } +} + +fn refusal_assignments(refusal: RefusalAggregate) -> List { + match refusal { + NoActiveRefusal => [] + ActiveRefusals { refused_count } => [ + SalienceAssignment { subject: refusal_subject_key, role: SalienceCritical }, + ] + } +} + +fn project_salience( + camera: ProgramCamera, + placements: List, + refusal: RefusalAggregate, +) -> List { + let focus_key = focus_subject_key(f: camera.focus) + let region = focal_region(camera: camera, placements: placements) + (placements |> map(p => SalienceAssignment { + subject: p.key, + role: placement_role(p: p, focus_key: focus_key, focus_region: region), + })) + |> concat(refusal_assignments(refusal: refusal)) +} + +data admission_is_derived_not_asserted_note: String = "The at-most-one-Focal law is not restated here. project_salience produces assignments and region_focal_admission judges them, so the projection is checked by the SAME fold every hand-authored region is checked by — one authority, asked about derived rows instead of authored ones. A witness that runs the projection through it is therefore a real test of the projection, not a second copy of the rule." + +fn project_admission( + camera: ProgramCamera, + placements: List, + refusal: RefusalAggregate, +) -> FocalAdmission { + region_focal_admission( + region: focal_region(camera: camera, placements: placements), + assignments: project_salience(camera: camera, placements: placements, refusal: refusal), + ) +} + +data finish_line_region: String = "v1-finish-lines" + +data finish_line_placements_note: String = "The instrument's subjects are V0's four v1-deletion finish lines, read from gunbc.v1_deletion_plan rather than restated — so a fifth finish line appears in the instrument by being declared once, and a renamed one cannot drift out of alignment with the roadmap node it binds to. They share one region because they are one field of peers: selecting any of them makes the other three its siblings." + +fn finish_line_placements() -> List { + v1_exit_finish_lines() |> map(s => SubjectPlacement { + key: v1_finish_line_key(l: s.line), + region: finish_line_region, + }) +} + +fn project_finish_line_salience(camera: ProgramCamera, refusal: RefusalAggregate) -> List { + project_salience(camera: camera, placements: finish_line_placements(), refusal: refusal) +} + +fn assignment_role_for(assignments: List, subject: String) -> SalienceRole { + fold(assignments, init: SalienceGround, f: (acc, a) => if a.subject == subject { a.role } else { acc }) +} diff --git a/dag/gunbc/design/interaction.dag b/dag/gunbc/design/interaction.dag index 3df66742284..7f2af0499a3 100644 --- a/dag/gunbc/design/interaction.dag +++ b/dag/gunbc/design/interaction.dag @@ -2,17 +2,19 @@ module gunbc.design.interaction import gunbc.design.material { TimingToken, respond_fast, reveal_deliberate, - MotionTrigger, OnHover, OnActive, OnStateClass, scale_transform_wire, travel_scale_transform_wire, rest_scale_per_mille, press_scale_per_mille, } import gunbc.design.scale { ScaleToken, scale_var, travel_lift, travel_press } +import gunbc.design.interaction_cause { + InteractionCause, PointerApproach, FocusAcquired, PressEngaged, ObservedStateEntered, +} data interaction_note: String = "Layer 2 interaction machinery (lifted from gunbc.site.interaction). Verbs x Responses x TimingToken, held as rows. ElementId is a closed enum — coverage_gaps is total by construction (design-register-library.md sect 10 Class 3, A.0)." data machine_side_verb_note: String = "Approach, Enter, StepBack, Copy, Traverse and Dispatch are all things a PERSON does to a control. Await and Accept are things the MACHINE does to it, and they are on the same axis rather than a parallel one because the axis was never 'user gesture' — it is the event class a control answers, and a control does not care whose event it was. The analog reading is the whole justification: a physical control left in an actuated position while a request is in flight, and then released into a new detent when the answer arrives, is one continuous mechanical story, and splitting it across two vocabularies would mean the register could describe the press but not the release. -The consequence that matters is coverage: because these are ordinary verbs, an element declaring them is subject to the same total-assignment law as one declaring hover, so a machine-caused state with no declared response is a counted gap exactly like a dead hover. What they cannot use is a MotionTrigger — there is no pseudo-class for 'the server said yes' — which is why they realize through StateRule." +The consequence that matters is coverage: because these are ordinary verbs, an element declaring them is subject to the same total-assignment law as one declaring hover, so a machine-caused state with no declared response is a counted gap exactly like a dead hover. What they cannot use is a person-caused InteractionCause — nothing a hand does corresponds to 'the server said yes' — which is why they arrive as ObservedStateEntered and realize through StateRule." type InteractionVerb = Approach @@ -136,7 +138,7 @@ That is why a detent carries a position and how it is REACHED rather than a dura type DetentReach = AtRest - | ByTrigger { trigger: MotionTrigger } + | ByTrigger { cause: InteractionCause } type DetentTravel = NoTravel @@ -161,14 +163,14 @@ fn house_pointer_detents(rest_state: String, hover_state: String, pressed_state: Detent { state: rest_state, reach: AtRest, travel: NoTravel, scale_per_mille: rest_scale_per_mille, turn_deg: 0 }, Detent { state: hover_state, - reach: ByTrigger { trigger: OnHover }, + reach: ByTrigger { cause: PointerApproach }, travel: Travel { token: travel_lift }, scale_per_mille: rest_scale_per_mille, turn_deg: 0, }, Detent { state: pressed_state, - reach: ByTrigger { trigger: OnActive }, + reach: ByTrigger { cause: PressEngaged }, travel: Travel { token: travel_press }, scale_per_mille: press_scale_per_mille, turn_deg: 0, diff --git a/dag/gunbc/design/interaction_cause.dag b/dag/gunbc/design/interaction_cause.dag new file mode 100644 index 00000000000..7fd94fab141 --- /dev/null +++ b/dag/gunbc/design/interaction_cause.dag @@ -0,0 +1,37 @@ +module gunbc.design.interaction_cause + +import std.types { String, Bool } + +data interaction_cause_note: String = "WHAT CAUSED THE RESPONSE, SAID WITHOUT NAMING A RENDERER (F2, review call 2026-08-04). The register's motion vocabulary was MotionTrigger — OnHover, OnFocusVisible, OnActive, OnStateClass — whose variants are named for CSS pseudo-class spellings and whose only projection maps them to selector text. That fuses the interaction MEANING ('the pointer approached this subject') with one realization's SPELLING (':hover'), which is the DESIGN section 3 interface/transport fusion in the exact shape extdeps.browser.browser was condemned for on gunbc#7556. A desktop, native, or canvas renderer has pointer-approach, focus and press; it has no ':hover' to import. + +THIS MODULE IS THE INTERFACE HALF and it imports nothing but std by construction: a semantic module reaching for a cause cannot accidentally acquire selector or property vocabulary through it. The CSS half stays in gunbc.design.material, which lowers a cause to its MotionTrigger realization — one of N, not the definition. The lowering is a total match over this closed coproduct, so a renderer that omits a mapping fails to COMPILE rather than silently dropping the response, which is the acceptance criterion this split was asked to meet. + +WHY THE OBSERVED-STATE ARM CARRIES A NAME AND THE OTHERS DO NOT: the first three are events a renderer already knows how to detect, so the cause is fully determined by the variant. An observed state is a fact the client program decided and named — 'requested', 'accepted', 'open' — so the name is part of the cause, not part of its rendering. That the CSS realization happens to render it as a class suffix while the other three render as pseudo-classes is a REALIZATION asymmetry (material.dag's transition_carrier_selector already derives placement from it) and this module deliberately does not encode it: cause_is_machine_observed answers the semantic question — did the machine cause this, or did the person — and a renderer with no classes at all still gets a true answer." + +type InteractionCause + = PointerApproach + | FocusAcquired + | PressEngaged + | ObservedStateEntered { state_name: String } + +fn interaction_cause_key(c: InteractionCause) -> String { + match c { + PointerApproach => "pointer-approach" + FocusAcquired => "focus-acquired" + PressEngaged => "press-engaged" + ObservedStateEntered { state_name } => join(["observed-state:", state_name], "") + } +} + +data machine_observed_note: String = "The semantic reading of the split the register already relied on: PointerApproach, FocusAcquired and PressEngaged are things a PERSON does to a control; ObservedStateEntered is something the MACHINE did to it. The still-until-touched amendment (material.dag) turned on exactly this distinction — motion on user touch OR observed state change, never ambient — and it stated the distinction in terms of pseudo-class versus class, which is the realization's way of seeing it. This is the same fact said in the interface's terms, so a non-CSS renderer can honour the law without inheriting the vocabulary that happened to express it first." + +fn cause_is_machine_observed(c: InteractionCause) -> Bool { + match c { + PointerApproach => false + FocusAcquired => false + PressEngaged => false + ObservedStateEntered { state_name } => true + } +} + +data ambient_remains_unwritable_note: String = "There is still no ambient constructor, and that is load-bearing rather than incidental. Every variant here names a CAUSE, so motion with no cause cannot be expressed in this vocabulary at all — the same construction wall MotionTrigger carried, preserved verbatim across the de-fusion. The instrument-motion lane (InstrumentDrift) is the declared exception and it does NOT widen this coproduct: bounded instrument character is a property of the enclosing instrument, not a response of a semantic control, so it gets its own carrier rather than an ambient arm here." diff --git a/dag/gunbc/design/material.dag b/dag/gunbc/design/material.dag index dc7a638d01c..7b10eb14918 100644 --- a/dag/gunbc/design/material.dag +++ b/dag/gunbc/design/material.dag @@ -10,6 +10,9 @@ import extdeps.color.srgb { hsl_projection_s_pct, hsl_projection_l_pct, } +import gunbc.design.interaction_cause { + InteractionCause, PointerApproach, FocusAcquired, PressEngaged, ObservedStateEntered, +} import extdeps.languages.css.properties { CssPropertyName, Transition, css_property_wire } import extdeps.languages.css.selectors { SelectorSubject, selector_subject_wire } data tokens_note: String = "Layer 2 of the site stack: materials, themes, scales. Register laws living here as CONSTRUCTION. ChromaByArea: a Material carries its AreaClass; saturation ceilings are per-area. GlareEnvelope (operator seventh pass, 2026-07-20: the bright saturated cyan read as low-taste gamer blue): a material may be bright OR chromatic, never both — quiet_envelope refuses sat>45 AND light>68 together, so the gamer register is inadmissible by row. DataVizArea (review finding 4 on PR 6927, pre-modeled seam): status-dense product surfaces (node-level CI views, dashboards) need mutually distinguishable categorical series at exactly the chroma-and-brightness the quiet envelope forbids — so the envelope is AREA-SCOPED by construction: DataVizArea is the one declared exemption lane, its own admission law (distinguishability + CVD separation, cited categorical palettes) lands with its first consumer (the Dashboard archetype study), and today NO theme role projects it — the witness pins that its introduction is a conscious event, never a leak. ThemeCoherence: a Theme is a TOTAL assignment of roles to materials (theme_gaps countable, mirrors interaction coverage), each material's area class must equal the role's declared area class, and every color the page uses routes through a role var — one rule set, N themes; prefers-color-scheme selects, never forks. ContrastLaw (review finding 1, hardened 2026-07-21): theme contrast is computed WCAG relative-luminance contrast via extdeps.accessibility.wcag_contrast — the earlier HSL-lightness-gap check was a non-perceptual proxy that could green while legibility failed; text roles must clear AA normal text (4.5:1), figure/focus roles AA graphical (3:1), against BOTH canvas and surface. StillUntilTouched: MotionTrigger has no ambient variant; no animation/keyframes constructor exists." @@ -157,12 +160,27 @@ Mechanically the amendment is one trigger variant, and the reason it needed to b One genuine asymmetry has to be respected, and it is where the analog reading pays off. A pseudo-class response is SYMMETRIC — hover in, hover out, and you want both to animate — so its transition belongs on the BASE selector where it governs the edge in both directions. A state-class response is an edge into a DETENT, and each detent is entered with its own weight (a sharp 90 ms travel into pressed, a spring return into accepted), so its transition belongs on the STATE selector. Placing both on the base would make the last-written timing govern every edge of the element, silently, because CSS transition is a shorthand and not a list. Hence transition_carrier_selector: the placement is derived from the trigger's kind rather than chosen per site." +data motion_trigger_is_the_css_realization_note: String = "MotionTrigger IS THE CSS REALIZATION OF gunbc.design.interaction_cause.InteractionCause, not the register's motion vocabulary (F2, review call 2026-08-04). Its variants are named for selector spellings and its only projections produce selector text, which is what made it a fused carrier: a semantic module reaching for 'the pointer approached' had to import ':hover'. The meaning now lives renderer-neutrally in interaction_cause and this type is one realization of it — the one this repository emits today. css_trigger_for below is the lowering, and because it is a total match over a closed coproduct, a realization that omits a cause fails to compile rather than silently dropping the response. Emission is unchanged by the split: the lowering is spelling-preserving, so every generated byte holds." + type MotionTrigger = OnHover | OnFocusVisible | OnActive | OnStateClass { class_name: String } +fn css_trigger_for(cause: InteractionCause) -> MotionTrigger { + match cause { + PointerApproach => OnHover + FocusAcquired => OnFocusVisible + PressEngaged => OnActive + ObservedStateEntered { state_name } => OnStateClass { class_name: state_name } + } +} + +fn css_selector_suffix_for_cause(cause: InteractionCause) -> String { + trigger_selector_suffix(t: css_trigger_for(cause: cause)) +} + fn trigger_selector_suffix(t: MotionTrigger) -> String { match t { OnHover => ":hover" diff --git a/dag/gunbc/design/principles.dag b/dag/gunbc/design/principles.dag index ccb94c208f1..fc901324441 100644 --- a/dag/gunbc/design/principles.dag +++ b/dag/gunbc/design/principles.dag @@ -16,6 +16,7 @@ type PrincipleId | SelectiveSpectacle | EmissionOverMaterial | BoundedAttraction + | PhysicalEnclosure type RegisterPrinciple { id: PrincipleId @@ -73,7 +74,7 @@ data register_principles: List = [ }, RegisterPrinciple { id: StillUntilTouched, - law: "Still until touched; always answers when touched. No ambient motion, ever.", + law: "The causal world remains still until caused; it always answers when touched. No subject moves without a cause — no ambient motion, ever.", enforced_by: principle_ref(module_path: "gunbc.design.material", decl_name: "BuildRule"), }, RegisterPrinciple { @@ -91,6 +92,11 @@ data register_principles: List = [ law: "Physical response moves the visual plate, never the hit region: attraction is bounded travel inside a fixed local field, settles on the register's one spring, gives keyboard focus the same focal identity without displacement, and renderer-local motion never advances domain state.", enforced_by: principle_ref(module_path: "gunbc.design.salience", decl_name: "AttractionField"), }, + RegisterPrinciple { + id: PhysicalEnclosure, + law: "The enclosing instrument may exhibit bounded, preference-controlled physical character — drift, jitter, shift, impulse glitch — while the causal world it encloses stays still until caused: every channel is off-by-preference with a total off position, carries no domain fact, and the composed displacement of all channels stays below the register's attraction travel, so instrument character can never be mistaken for a real response.", + enforced_by: principle_ref(module_path: "gunbc.design.instrument_physical", decl_name: "displacement_admission"), + }, ] fn principle_id_key(id: PrincipleId) -> String { @@ -106,6 +112,7 @@ fn principle_id_key(id: PrincipleId) -> String { SelectiveSpectacle => "selective-spectacle" EmissionOverMaterial => "emission-over-material" BoundedAttraction => "bounded-attraction" + PhysicalEnclosure => "physical-enclosure" } } diff --git a/dag/gunbc/design/salience.dag b/dag/gunbc/design/salience.dag index e0a80a25f51..fc6a678e419 100644 --- a/dag/gunbc/design/salience.dag +++ b/dag/gunbc/design/salience.dag @@ -7,7 +7,7 @@ import extdeps.languages.css.values { } import gunbc.design.material { TimingToken, settle_spring } -data salience_note: String = "REGISTER AMENDMENT: SELECTIVE SPECTACLE (operator recalibration, 2026-08-02). The earlier register overcorrected against cheap spectacle into uniform austerity: QuietSurface, the glare envelope, and still-until-touched prevented bad spectacle and good FOCAL spectacle alike, which is why the site read coherent but emotionally flat. The corrected thesis is calm field, luminous focus, physical response, every response true: showiness is not forbidden, it is SCARCE, FOCAL, and CAUSED. This module is the salience model that makes that lawful rather than vibes: every energy channel (chroma, emission, motion, sound) is granted per role from one budget table, and the grants are typed refusals rather than per-site judgement. SCOPE, STATED PLAINLY: this is the model layer only. A salience role ARRIVES HERE AS AN INPUT — region_focal_admission is handed a region's assignments and emission_for is handed a role — so nothing here yet DECIDES a role from real facts. The projection that will decide it (selected subject, selected primary operation, active refusal needing action) is the declared next consumer, not a thing this module implements; until it lands, a caller supplying roles by hand is the only path, and that is the staging, not the end state. DISSOLVE-ON: the projection lands as a real fn over the roadmap's selection facts, with its own witnesses, and this paragraph loses its scope clause. The reference specimen is the operator's dynamic-tierlist login control (read from source 2026-08-02): a three-layer corona at 1:2:3 blur ratios with decaying alphas, proximity-scaled brightness, and a low-pass drift whose LAG is the material — its lesson is one focal object can be unusually alive when the surrounding field gives it room, NOT that every row glows. The field stays calm because the subject gets the energy." +data salience_note: String = "REGISTER AMENDMENT: SELECTIVE SPECTACLE (operator recalibration, 2026-08-02). The earlier register overcorrected against cheap spectacle into uniform austerity: QuietSurface, the glare envelope, and still-until-touched prevented bad spectacle and good FOCAL spectacle alike, which is why the site read coherent but emotionally flat. The corrected thesis is calm field, luminous focus, physical response, every response true: showiness is not forbidden, it is SCARCE, FOCAL, and CAUSED. This module is the salience model that makes that lawful rather than vibes: every energy channel (chroma, emission, motion, sound) is granted per role from one budget table, and the grants are typed refusals rather than per-site judgement. THE PROJECTION HAS LANDED, firing this paragraph's former scope clause (instrument wave, 2026-08-04). Roles are no longer only an input: gunbc.design.instrument_projection project_salience DECIDES a role from real facts — the camera's selected subject is Focal, its region siblings are Supporting, everything outside that region is Ground, and an aggregated active refusal is one Critical subject — and its output is judged by region_focal_admission below, the same fold that judges hand-authored assignments. A caller may still supply assignments by hand, which is correct rather than residual: this module is the budget authority and the projection is one consumer of it, not its only legitimate entry. The reference specimen is the operator's dynamic-tierlist login control (read from source 2026-08-02): a three-layer corona at 1:2:3 blur ratios with decaying alphas, proximity-scaled brightness, and a low-pass drift whose LAG is the material — its lesson is one focal object can be unusually alive when the surrounding field gives it room, NOT that every row glows. The field stays calm because the subject gets the energy." type SalienceRole = SalienceGround diff --git a/dag/gunbc/design/theme.dag b/dag/gunbc/design/theme.dag index d1825af3dbb..c765391c978 100644 --- a/dag/gunbc/design/theme.dag +++ b/dag/gunbc/design/theme.dag @@ -219,17 +219,23 @@ fn theme_var_decls(t: Theme) -> List { [decl(prop: ColorScheme, value: t.scheme)]) } -fn theme_root_css(base: Theme, alternate: Theme) -> String { +data theme_scoped_blocks_note: String = "ONE THEME-SELECTOR GRAMMAR, N VAR FAMILIES. The three-block shape below — :root for the base theme, :root[data-theme=NAME] for the alternate, and the same alternate again under prefers-color-scheme for readers who never touched the toggle — is what makes a theme switchable at all, and it was written out longhand once here for role vars and again in gunbc.roadmap_style band_root_css for band vars. A second copy of a selector grammar is a second place for the toggle to break in only one of them, which is precisely the failure a reader would never think to look for: the day/night switch would keep working for colors and silently stop working for bands. The family of declarations is now a parameter, so theme_root_css is the role-var instantiation, band_root_css is the band-var instantiation, and the instrument's emission vars are a third — one grammar, three families, and emission is unchanged in all of them." + +fn theme_scoped_blocks(base: Theme, alternate: Theme, decls_for: fn(Theme) -> List) -> String { join([ - css_block(selector: ":root", decls: theme_var_decls(t: base)), + css_block(selector: ":root", decls: decls_for(base)), css_block( selector: join([":root[data-theme=\"", alternate.name, "\"]"], ""), - decls: theme_var_decls(t: alternate)), + decls: decls_for(alternate)), join([ "@media (prefers-color-scheme: ", alternate.scheme, ") { ", - css_block(selector: ":root:not([data-theme])", decls: theme_var_decls(t: alternate)), + css_block(selector: ":root:not([data-theme])", decls: decls_for(alternate)), " }", ], ""), ], "\n") } +fn theme_root_css(base: Theme, alternate: Theme) -> String { + theme_scoped_blocks(base: base, alternate: alternate, decls_for: t => theme_var_decls(t: t)) +} + diff --git a/dag/gunbc/roadmap_instrument_sandbox.dag b/dag/gunbc/roadmap_instrument_sandbox.dag new file mode 100644 index 00000000000..7e6fc47c6eb --- /dev/null +++ b/dag/gunbc/roadmap_instrument_sandbox.dag @@ -0,0 +1,571 @@ +module gunbc.roadmap_instrument_sandbox + +import std.types { Int, String, Bool, List } +import std.markup { Fragment, Element, Attribute, attr } +import gunbc.site.markup { txt, el, el_class, el_attrs } +import gunbc.roadmap_style { roadmap_css } +import extdeps.languages.css.properties { + CssPropertyName, BoxShadow, Transform, CustomProperty, Border, Padding, Margin, + Display, Gap, Background, Color, BorderRadius, FontFamily, FontSize, MinWidth, +} +import extdeps.languages.css.selectors { SelectorSubject, ClassSelector } +import gunbc.design.material { + BuildRule, StaticRule, ResponseRule, CssDecl, decl, serialize_rules, + Material, paint_alpha, TriggerShape, SelfResponse, MotionTrigger, OnActive, + TimingToken, +} +import gunbc.design.theme { + Theme, day_theme, night_theme, theme_scoped_blocks, role_var, + ThemeRole, FocusRole, SurfaceRole, BorderRole, TextRole, TextDimRole, + assignment_material, +} +import gunbc.design.scale { scale_var, space_2, space_6, space_16, text_12, font_mono, radius_3 } +import gunbc.design.salience { + SalienceRole, SalienceGround, SalienceSupporting, SalienceFocal, SalienceCritical, + salience_key, SalienceAssignment, EmissionSpec, + attraction_travel_max_px, +} +import gunbc.design.instrument_camera { + ProgramCamera, ProgramDepth, DepthProgram, DepthOutcome, DepthFront, DepthNode, DepthEvidence, + ProgramMode, ModeStatus, ModeRemaining, ModeWhy, program_depth_key, program_depth_index, + program_mode_key, camera_initial, camera_select, camera_set_mode, focus_finish_line, + StateOwner, AuthoritativeProgramView, LocalInstrumentState, InstrumentObservation, + RendererEphemera, state_owner_key, owner_may_write_domain_fact, +} +import gunbc.design.instrument_projection { + RefusalAggregate, NoActiveRefusal, ActiveRefusals, + project_finish_line_salience, assignment_role_for, refusal_subject_key, +} +import gunbc.design.instrument_physical { + InstrumentChannel, ChannelOpticalJitter, ChannelVerticalShift, ChannelBuoyantDrift, ChannelImpulseGlitch, + channel_key, ChannelAmplitude, amplitude_px, channel_amplitude, + InstrumentPreference, preference_default, glitch_settle, glitch_duration_key, + instrument_displacement_px, instrument_displacement_max_px, + DisplacementAdmission, DisplacementAdmitted, DisplacementOverBudget, displacement_admission, + PhysicalImpulseSource, SyntheticImpulse, HostAccelerometer, HostDeviceMotion, impulse_source_key, + SensorAvailability, SensorPresent, SensorAbsent, SensorPermissionNotRequested, + SensorPermissionDenied, SensorAvailabilityUnknown, sensor_availability_key, + ImpulseAdmission, ImpulseAdmitted, ImpulseSourceUnavailable, ImpulseChannelDisabled, admit_impulse, +} +import gunbc.design.instrument_audition { + AuditionIntensity, AuditionRestrained, AuditionExpressive, AuditionHero, + audition_intensity_key, audition_intensities, audition_emission, + AuditionEmission, AuditionNoEmission, AuditionEmits, + AuditionAdmission, AuditionAdmitted, AuditionEmissionRefused, + AuditionAttractionOutsideEnvelope, AuditionDisplacementOverBudget, admit_audition, + ProgramReading, ReadingNoSubject, ReadingProgramShape, ReadingOutcomeStatus, + ReadingOutcomeRemaining, ReadingConstraint, ReadingNoConstraint, ReadingFront, + ReadingUnavailable, read_camera, +} +import gunbc.roadmap_program_view { + V1DeletionProgramView, RemainingShape, V1ProgramViewResult, + ProgramViewDerived, ProgramViewRefused, ProgramViewRefusalCause, + FinishLineNodeUnresolved, FrontGateUnresolved, v1_program_view, +} +import gunbc.roadmap_authority { + declared_roadmap_nodes, declared_roadmap_edges, roadmap_acceptance_receipts, +} +import gunbc.v1_deletion_plan { + V1FinishLine, V1FinishLineSpec, CompilerFixedPoint, v1_exit_finish_lines, v1_finish_line_key, +} + +data instrument_sandbox_note: String = "THE FIRST V1-DELETION INSTRUMENT, at /sandbox/instrument. Everything on this page is DERIVED from the same authorities the model layer is witnessed against — the four finish lines come from gunbc.v1_deletion_plan, the roles come from the projection rather than from hand-placed classes, the audition verdicts come from the register's own emission and displacement gates, and the impulse matrix is admit_impulse run over every source and every sensor state. Nothing here is a mock, so a page that renders a wrong role is a projection defect and not a styling one. WHAT IS DELIBERATELY ABSENT, named rather than faked: the IDLE half of the physical character — resting jitter, vertical shift, buoyant drift — is modelled, budgeted and witnessed but NOT animated here, because ambient motion has no constructor in this register by design (gunbc.design.material still_until_touched_amendment_note: MotionTrigger carries no ambient variant and no keyframes constructor exists). Emitting raw animation text past that wall would be the unmarked-workaround class the design authority names as a line-stop signal, so the idle channels are shown as their measured budget and the CAUSED half — the impulse glitch on press — is real, built through the ordinary ResponseRule machinery. DISSOLVE-ON: an enclosure-scoped ambient-motion constructor lands with its own admission law, and the idle channels animate through it." + +data derived_role_note: String = "THE ROLE THE AUDITION IS ADMITTED AT COMES FROM THE PROJECTION, NOT FROM THIS FILE. The first cut passed SalienceFocal as a literal at the one place the visual actually gets made, which meant the derived-salience work stopped one call short of the seam it existed to reach: the model derived roles, and then the first visual consumer authored one anyway. Role now comes from project_finish_line_salience over the same exemplar camera the readings use, so changing which subject is selected changes what the card is admitted at, and a subject that is NOT selected is admitted at Supporting and gets no emission — which is the whole law, finally applied where it can be seen." + +fn audition_subject_key() -> String { + focus_subject_key(f: exemplar_camera().focus) +} + +fn audition_subject_role() -> SalienceRole { + assignment_role_for( + assignments: project_finish_line_salience(camera: exemplar_camera(), refusal: NoActiveRefusal), + subject: audition_subject_key(), + ) +} + +data instrument_sandbox_page_class: String = "instrument-sandbox" +data instrument_frame_class: String = "instrument-frame" +data instrument_row_class: String = "instrument-row" +data instrument_cell_class: String = "instrument-cell" +data instrument_note_class: String = "instrument-note" +data instrument_refusal_class: String = "instrument-refusal" + +fn audition_card_class(i: AuditionIntensity) -> String { + concat("audition-", audition_intensity_key(i: i)) +} + +fn audition_emission_var(i: AuditionIntensity) -> String { + concat("instrument-emission-", audition_intensity_key(i: i)) +} + +data admitted_only_note: String = "THE STYLESHEET IS GENERATED FROM THE ADMISSION, NOT FROM THE REQUEST (review finding, 2026-08-05, and it was a real hole rather than a tidiness point). The first cut derived each card's box-shadow straight from audition_emission and printed the admission verdict as PROSE UNDERNEATH the already-painted glow. So a refused emission still painted: the gate decided what the page SAID about the effect, not whether the effect existed. That is the register's admission machinery reduced to a caption — the same coverage-by-illusion shape as an inert lens, one layer further out, and it would have failed silently the first time a budget change turned a grant into a refusal. Emission is now projected from AuditionAdmitted alone: a refused variant emits the literal value none and has no glow to inspect. The discriminating control is a witness that renders the specimen at a non-focal role and finds no emission anywhere in the emitted CSS." + +data emission_projection_note: String = "An EmissionSpec becomes a two-layer box-shadow: a crisp core near the object and one soft low-alpha corona, which is exactly the shape the emission envelope admits and no more. The colour is the theme's FOCUS material at the spec's own alphas, so the emission is the same hue the register already uses to say 'this one', and it is emitted per theme through the shared theme-selector grammar rather than pinned to one projection — the day/night toggle retunes the glow for free." + +fn emission_shadow_value(m: Material, spec: EmissionSpec) -> String { + join([ + "0 0 ", to_string(spec.core_radius.n), "px ", paint_alpha(m: m, alpha_pct: spec.core_alpha_pct), + ", 0 0 ", to_string(spec.corona_radius.n), "px ", paint_alpha(m: m, alpha_pct: spec.corona_alpha_pct), + ], "") +} + +fn no_emission_decl(i: AuditionIntensity) -> List { + [decl(prop: CustomProperty { name: audition_emission_var(i: i) }, value: "none")] +} + +fn emission_decl_for(t: Theme, i: AuditionIntensity, role: SalienceRole) -> List { + match admit_audition(i: i, role: role, subject_key: audition_subject_key()) { + AuditionAdmitted { intensity, emission, attraction, displacement_px } => match emission { + AuditionNoEmission => no_emission_decl(i: i) + AuditionEmits { spec } => [decl( + prop: CustomProperty { name: audition_emission_var(i: i) }, + value: emission_shadow_value(m: assignment_material(t: t, r: FocusRole), spec: spec), + )] + } + AuditionEmissionRefused { intensity, grant } => no_emission_decl(i: i) + AuditionAttractionOutsideEnvelope { intensity } => no_emission_decl(i: i) + AuditionDisplacementOverBudget { intensity, total_px, max_px } => no_emission_decl(i: i) + } +} + +fn emission_var_decls(t: Theme, role: SalienceRole) -> List { + flat_map(audition_intensities, i => emission_decl_for(t: t, i: i, role: role)) +} + +fn instrument_emission_root_css_for(role: SalienceRole) -> String { + theme_scoped_blocks(base: day_theme, alternate: night_theme, decls_for: t => emission_var_decls(t: t, role: role)) +} + +fn instrument_emission_root_css() -> String { + instrument_emission_root_css_for(role: audition_subject_role()) +} + +fn cls(name: String) -> SelectorSubject { + ClassSelector { name: name } +} + +fn audition_card_rule(i: AuditionIntensity) -> BuildRule { + StaticRule { + selector: cls(name: audition_card_class(i: i)), + decls: [ + decl(prop: BoxShadow, value: concat("var(--", concat(audition_emission_var(i: i), ")"))), + decl(prop: Border, value: join(["1px solid ", role_var(r: BorderRole)], "")), + decl(prop: BorderRadius, value: scale_var(t: radius_3)), + decl(prop: Padding, value: scale_var(t: space_6)), + decl(prop: Background, value: role_var(r: SurfaceRole)), + decl(prop: MinWidth, value: "14rem"), + ], + } +} + +data impulse_press_note: String = "THE CAUSED HALF, BUILT THROUGH THE ORDINARY MACHINERY. Pressing the instrument frame displaces it by the preference's own impulse amplitude and it settles on the glitch duration's timing — a ResponseRule with the OnActive trigger, the same construction every other control in this register uses, so the physical character is not a special case that bypasses the wall. The displacement is negative on the Y axis and read straight off the preference: an author who disables the impulse channel gets a rule that displaces by zero rather than a rule that has to be removed." + +fn impulse_translate_value(p: InstrumentPreference) -> String { + join(["translateY(-", to_string(amplitude_px(a: p.impulse_glitch)), "px)"], "") +} + +fn instrument_frame_rule(p: InstrumentPreference) -> BuildRule { + ResponseRule { + subject: cls(name: instrument_frame_class), + shape: SelfResponse, + trigger: OnActive, + transition_props: "transform", + timing: glitch_settle(g: p.glitch_duration), + base_decls: [ + decl(prop: Border, value: join(["1px solid ", role_var(r: BorderRole)], "")), + decl(prop: BorderRadius, value: scale_var(t: radius_3)), + decl(prop: Padding, value: scale_var(t: space_16)), + decl(prop: Background, value: role_var(r: SurfaceRole)), + decl(prop: Transform, value: "translateY(0)"), + ], + response_decls: [decl(prop: Transform, value: impulse_translate_value(p: p))], + } +} + +fn instrument_layout_rules() -> List { + [ + StaticRule { + selector: cls(name: instrument_row_class), + decls: [ + decl(prop: Display, value: "flex"), + decl(prop: Gap, value: scale_var(t: space_6)), + decl(prop: Margin, value: join([scale_var(t: space_6), " 0"], "")), + ], + }, + StaticRule { + selector: cls(name: instrument_cell_class), + decls: [ + decl(prop: FontFamily, value: scale_var(t: font_mono)), + decl(prop: FontSize, value: scale_var(t: text_12)), + decl(prop: Padding, value: scale_var(t: space_2)), + ], + }, + StaticRule { + selector: cls(name: instrument_note_class), + decls: [decl(prop: Color, value: role_var(r: TextDimRole))], + }, + StaticRule { + selector: cls(name: instrument_refusal_class), + decls: [ + decl(prop: Color, value: role_var(r: TextRole)), + decl(prop: Border, value: join(["1px dashed ", role_var(r: BorderRole)], "")), + decl(prop: Padding, value: scale_var(t: space_2)), + ], + }, + ] +} + +fn instrument_rules() -> List { + concat( + instrument_layout_rules(), + concat( + [instrument_frame_rule(p: preference_default)], + map(audition_intensities, i => audition_card_rule(i: i)))) +} + +fn instrument_css() -> String { + join([roadmap_css(), instrument_emission_root_css(), serialize_rules(rules: instrument_rules())], "\n") +} + +data css_at_role_note: String = "The stylesheet at an arbitrary role, exposed so a witness can render the study as if the specimen were NOT selected and prove no emission appears. Without this seam the refused-emission control could only be written by editing the page, which is the kind of test that passes because the author remembered to keep it in sync." + +fn instrument_css_at_role(role: SalienceRole) -> String { + join([instrument_emission_root_css_for(role: role), serialize_rules(rules: instrument_rules())], "\n") +} + +fn cell(s: String) -> Fragment { + el_class("span", instrument_cell_class, [ txt(s) ]) +} + +fn row(cells: List) -> Fragment { + el_class("div", instrument_row_class, cells) +} + +fn note(s: String) -> Fragment { + el_class("p", instrument_note_class, [ txt(s) ]) +} + +data exemplar_note: String = "THIS PAGE IS A STATIC STUDY, and calling it that is the correction rather than a hedge. It renders ONE camera state, server-side, with no client program: no pointer selection, no keyboard parity, no wheel detent, no persistence. What it is for is showing what each depth and mode PRODUCE from the real derived world, so the projections can be read and judged before an operable instrument is built on them. The operable tuner — persistent camera, selection parity, one-detent movement, working controls — is the declared follow-on, and describing this page as that instrument would be the rung inflation DESIGN section 4b names." + +data live_view_note: String = "THE WORLD IS THE ONE V0 DERIVES, read live from the roadmap authority — declared nodes, declared edges, and acceptance receipts, which is the same call the program-view witness makes. The previous revision passed an empty accepted list and read gunbc.v1_deletion_plan's authored rows directly, so every finish line rendered as not-accepted regardless of the real receipts and the remaining/why modes had nothing to project. A refusal from the projection renders AS a refusal here: if a finish-line node or front gate resolves to nothing, the page says so with the located causes rather than drawing a smaller program." + +fn exemplar_camera() -> ProgramCamera { + camera_select(c: camera_initial, f: focus_finish_line(l: CompilerFixedPoint)) +} + +data live_view_two_refusal_sources_note: String = "TWO INDEPENDENT WAYS THE LIVE WORLD CAN FAIL TO ARRIVE, flattened to located text exactly once. gunbc.roadmap_authority's roadmap_acceptance_receipts is a PROJECTION (#7791 receipt-continuity work), not a list — it can refuse before the program view is ever attempted — and gunbc.roadmap_program_view can then refuse on its own causes. Forwarding the first as the second was not available and would have been the fabrication this page exists to avoid: a receipts-projection refusal is not a ProgramViewRefusalCause, and inventing one would put a cause in front of the reader that the model never produced. So this carrier keeps both sources and renders either as its own located line. The page's contract is unchanged — refuse loudly with the causes named, never draw a smaller program. Found by execution rather than by typecheck: passing the projection straight into v1_program_view compiled clean and failed at runtime with 'fold expects a list, got Variant', so the List-versus-coproduct swap at a call site is a class the substrate does not currently wall." + +type LiveProgramView + = LiveViewDerived { view: V1DeletionProgramView } + | LiveViewRefused { causes: List } + +fn live_program_view_result() -> LiveProgramView { + match roadmap_acceptance_receipts() { + RoadmapAcceptanceReceiptsProjectionRefused { detail } => + LiveViewRefused { causes: [join(["acceptance receipts unavailable: ", detail], "")] } + RoadmapAcceptanceReceiptsProjected { receipts } => + match v1_program_view( + nodes: declared_roadmap_nodes(), + edges: declared_roadmap_edges(), + receipts: receipts, + in_flight: [], + ) { + ProgramViewDerived { view } => LiveViewDerived { view: view } + ProgramViewRefused { causes } => + LiveViewRefused { causes: map(causes, c => refusal_cause_text(c: c)) } + } + } +} + +fn program_depths() -> List { [DepthProgram, DepthOutcome, DepthFront, DepthNode, DepthEvidence] } +fn program_modes() -> List { [ModeStatus, ModeRemaining, ModeWhy] } + +fn depth_cell(d: ProgramDepth) -> Fragment { + cell(s: join([to_string(program_depth_index(d: d)), " · ", program_depth_key(d: d)], "")) +} + +fn owner_cell(o: StateOwner) -> Fragment { + cell(s: join([ + state_owner_key(o: o), " — ", + if owner_may_write_domain_fact(o: o) { "may write domain facts" } else { "presentation only" }, + ], "")) +} + +fn camera_section() -> Fragment { + el("section", concat( + [ + el("h2", [ txt("semantic camera") ]), + note(s: "Five depths on one axis, three modes across it. A depth change crosses exactly one detent, and every move carries the selected subject unchanged."), + row(cells: map(program_depths(), d => depth_cell(d: d))), + el("h3", [ txt("state ownership") ]), + note(s: "Only one owner may write a domain fact, and it is not reachable from the instrument."), + row(cells: map( + [AuthoritativeProgramView, LocalInstrumentState, InstrumentObservation, RendererEphemera], + o => owner_cell(o: o))), + ], + [ el("h3", [ txt("readings") ]), reading_rows() ])) +} + +data reading_render_note: String = "A refusal renders AS a refusal. The Why mode has no rationale carrier to read, so it produces a typed ReadingUnavailable and the page prints the cause — the alternative, printing the claim under a Why heading, would be indistinguishable from an answer and is exactly the fabricated-plausible-output arm this surface exists to make visible." + +fn remaining_text(r: RemainingShape) -> String { + join([ + "depth ", to_string(r.sequential_depth), + " · open fronts ", to_string(r.open_fronts), + " · startable ", to_string(r.startable_now), + " · in flight ", to_string(r.in_flight), + " · dependency-held ", to_string(r.dependency_held), + " · contract-held ", to_string(r.contract_held), + ], "") +} + +fn render_reading(label: String, r: ProgramReading) -> Fragment { + match r { + ReadingNoSubject => row(cells: [ cell(s: label), cell(s: "no subject selected") ]) + ReadingProgramShape { remaining } => + row(cells: [ cell(s: label), cell(s: "whole program"), cell(s: remaining_text(r: remaining)) ]) + ReadingOutcomeStatus { name, node, accepted, open_fronts } => row(cells: [ + cell(s: label), + cell(s: name), + cell(s: node), + cell(s: if accepted { "accepted" } else { "not accepted" }), + cell(s: join([to_string(open_fronts), " open fronts"], "")), + ]) + ReadingOutcomeRemaining { name, remaining } => + row(cells: [ cell(s: label), cell(s: name), cell(s: remaining_text(r: remaining)) ]) + ReadingConstraint { subject, kind, headline, in_flight, depth } => row(cells: [ + cell(s: label), + cell(s: join([kind, " constraint"], "")), + cell(s: subject), + cell(s: headline), + cell(s: if in_flight { "work observed" } else { "no work observed" }), + ]) + ReadingNoConstraint { subject_key, reason } => + row(cells: [ cell(s: label), cell(s: subject_key), cell(s: reason) ]) + ReadingFront { key, name, closed, gates_accepted, gates_total } => row(cells: [ + cell(s: label), + cell(s: name), + cell(s: join([to_string(gates_accepted), " of ", to_string(gates_total), " gates accepted"], "")), + cell(s: if closed { "closed" } else { "open" }), + ]) + ReadingUnavailable { mode, subject_key, cause } => + el_class("div", instrument_refusal_class, [ + txt(join([label, " · ", subject_key, " — unavailable: ", cause], "")), + ]) + } +} + +fn reading_at(view: V1DeletionProgramView, d: ProgramDepth, m: ProgramMode) -> Fragment { + render_reading( + label: join([program_depth_key(d: d), " / ", program_mode_key(m: m)], ""), + r: read_camera( + camera: camera_set_mode(c: camera_step_to(d: d), m: m), + view: view, + ), + ) +} + +fn camera_step_to(d: ProgramDepth) -> ProgramCamera { + ProgramCamera { depth: d, mode: exemplar_camera().mode, focus: exemplar_camera().focus } +} + +fn depth_readings(view: V1DeletionProgramView, d: ProgramDepth) -> List { + map(program_modes(), m => reading_at(view: view, d: d, m: m)) +} + +data refusal_cause_arms_note: String = "TOTAL OVER V0's REFUSAL COPRODUCT, and the totality is load-bearing rather than tidy. The page's whole contract when the projection refuses is that it draws the LOCATED causes instead of a smaller program, so a cause this page could not name would be a cause the reader never sees — the empty-observation narrow, one layer out. The duplicate arms arrived from PR #7822 and the compiler refused this match until they were handled, which is the construction wall working across a merge: nobody had to notice that V0 grew two refusal shapes, because an Accepted program could not be built without them." + +fn refusal_cause_text(c: ProgramViewRefusalCause) -> String { + match c { + FinishLineNodeUnresolved { line_key, node } => + join(["finish line ", line_key, " names no declared node: ", node as String], "") + FrontGateUnresolved { front_key, gate } => + join(["front ", front_key, " names no declared gate: ", gate as String], "") + DuplicateAcceptanceReceipt { node } => + join(["node ", node as String, " carries more than one acceptance receipt"], "") + DuplicateProgramNodeId { node } => + join(["node id ", node as String, " is declared more than once"], "") + } +} + +fn reading_rows() -> Fragment { + match live_program_view_result() { + LiveViewRefused { causes } => el("div", concat( + [ el_class("div", instrument_refusal_class, [ txt("program view refused — the page draws nothing rather than a smaller program") ]) ], + map(causes, c => el_class("div", instrument_refusal_class, [ txt(c) ])))) + LiveViewDerived { view } => + el("div", flat_map(program_depths(), d => depth_readings(view: view, d: d))) + } +} + +fn salience_row(assignments: List, spec: V1FinishLineSpec) -> Fragment { + let key = v1_finish_line_key(l: spec.line) + row(cells: [ + cell(s: salience_key(role: assignment_role_for(assignments: assignments, subject: key))), + cell(s: spec.name), + cell(s: key), + ]) +} + +fn salience_block(label: String, camera: ProgramCamera, refusal: RefusalAggregate) -> Fragment { + let assignments = project_finish_line_salience(camera: camera, refusal: refusal) + el("div", concat( + concat( + [ el("h3", [ txt(label) ]) ], + map(v1_exit_finish_lines(), s => salience_row(assignments: assignments, spec: s))), + [ row(cells: [ + cell(s: salience_key(role: assignment_role_for(assignments: assignments, subject: refusal_subject_key))), + cell(s: refusal_subject_key), + ]) ])) +} + +fn salience_section() -> Fragment { + el("section", [ + el("h2", [ txt("focal salience, derived") ]), + note(s: "No row on this page carries an authored role. The selected subject is Focal, its region siblings are Supporting, everything else is Ground, and an active refusal is one Critical subject however many refuse."), + salience_block(label: "nothing selected", camera: camera_initial, refusal: NoActiveRefusal), + salience_block(label: "compiler fixed point selected", camera: exemplar_camera(), refusal: NoActiveRefusal), + salience_block( + label: "selected, with three active refusals", + camera: exemplar_camera(), + refusal: ActiveRefusals { refused_count: 3 }, + ), + ]) +} + +fn audition_verdict_text(a: AuditionAdmission) -> String { + match a { + AuditionAdmitted { intensity, emission, attraction, displacement_px } => + join(["admitted · enclosure displacement ", to_string(displacement_px), "px"], "") + AuditionEmissionRefused { intensity, grant } => "refused: emission not admissible at this role" + AuditionAttractionOutsideEnvelope { intensity } => "refused: attraction outside the envelope" + AuditionDisplacementOverBudget { intensity, total_px, max_px } => + join(["refused: displacement ", to_string(total_px), "px over ", to_string(max_px), "px"], "") + } +} + +fn audition_card(i: AuditionIntensity) -> Fragment { + let verdict = admit_audition(i: i, role: audition_subject_role(), subject_key: audition_subject_key()) + el_class("div", audition_card_class(i: i), [ + el("h3", [ txt(audition_intensity_key(i: i)) ]), + cell(s: "Compiler fixed point"), + note(s: audition_verdict_text(a: verdict)), + ]) +} + +fn audition_section() -> Fragment { + el("section", [ + el("h2", [ txt("focal audition — one real subject, three energies") ]), + note(s: "The same finish line rendered at three grants of the same budget. Restrained is the register before the amendment; hero sits at the emission envelope's admissible maximum, so the comparison shows where the bound actually is."), + el_class("div", instrument_row_class, map(audition_intensities, i => audition_card(i: i))), + ]) +} + +fn channel_row(p: InstrumentPreference, c: InstrumentChannel) -> Fragment { + row(cells: [ + cell(s: channel_key(c: c)), + cell(s: join([to_string(amplitude_px(a: channel_amplitude(p: p, c: c))), "px"], "")), + cell(s: "carries no domain fact"), + ]) +} + +fn displacement_text(p: InstrumentPreference) -> String { + match displacement_admission(p: p) { + DisplacementAdmitted { total_px } => + join([ + "composed displacement ", to_string(total_px), "px, within the ", + to_string(instrument_displacement_max_px), "px ceiling borrowed from the register's attraction travel", + ], "") + DisplacementOverBudget { total_px, max_px } => + join(["refused: composed ", to_string(total_px), "px exceeds the ", to_string(max_px), "px envelope"], "") + EnclosureCharacterReachesResponseTravel { character_px, max_px } => + join([ + "refused: enclosure character alone reaches ", to_string(character_px), + "px, the full ", to_string(max_px), "px a real focal response may travel", + ], "") + } +} + +fn impulse_cell(s: PhysicalImpulseSource, a: SensorAvailability) -> Fragment { + cell(s: join([ + sensor_availability_key(a: a), " → ", + match admit_impulse(p: preference_default, s: s, sensor: a) { + ImpulseAdmitted { source, settle } => join(["admitted (", settle.name, ")"], "") + ImpulseSourceUnavailable { source, availability } => join(["refused (", availability, ")"], "") + ImpulseChannelDisabled { source } => "refused (channel disabled)" + }, + ], "")) +} + +fn sensor_states() -> List { + [SensorPresent, SensorAbsent, SensorPermissionNotRequested, SensorPermissionDenied, SensorAvailabilityUnknown] +} + +fn impulse_row(s: PhysicalImpulseSource) -> Fragment { + row(cells: concat( + [ cell(s: impulse_source_key(s: s)) ], + map(sensor_states(), a => impulse_cell(s: s, a: a)))) +} + +fn physical_section() -> Fragment { + el("section", concat( + concat( + [ + el("h2", [ txt("physical screen") ]), + note(s: "Press the frame below: the impulse glitch is a real response built through the ordinary ResponseRule machinery, so it obeys the same still-until-touched law every other control does. The idle channels are budgeted here but not animated — ambient motion has no constructor in this register yet, and emitting one past that wall would be an unmarked workaround."), + el_attrs("button", [ + attr(name: "class", value: instrument_frame_class ), + attr(name: "type", value: "button" ), + ], [ + el("h3", [ txt("instrument enclosure — press to see the impulse transient") ]), + note(s: join(["impulse decay: ", glitch_duration_key(g: preference_default.glitch_duration)], "")), + ]), + ], + map([ChannelOpticalJitter, ChannelVerticalShift, ChannelBuoyantDrift, ChannelImpulseGlitch], c => channel_row(p: preference_default, c: c))), + concat( + [ note(s: displacement_text(p: preference_default)), el("h3", [ txt("impulse admission") ]) ], + map([SyntheticImpulse, HostAccelerometer, HostDeviceMotion], s => impulse_row(s: s))))) +} + +data page_shell_note: String = "THE SHELL SAYS WHAT THE PAGE IS. It declares a language and a viewport because a document without them is not a finished page on a phone or to a screen reader, and it does NOT reuse the roadmap header: that header carries theme and sound toggles whose behaviour comes from a client program this static study does not load, so rendering them would put two dead controls on the page — an affordance that does nothing is the same lie as a caption under an unadmitted glow, just cheaper to notice. The title names it a study rather than an instrument, for the reason exemplar_note gives." + +fn instrument_study_header() -> Fragment { + el("header", [ + el_class("div", "header-inner", [ + el_class("span", "wordmark", [ txt("gunbc") ]), + el("h1", [ txt("instrument — static study") ]), + ]), + ]) +} + +fn instrument_sandbox_page() -> Fragment { + Element { + tag: "html", + attributes: [ attr(name: "lang", value: "en" ) ], + children: [ + el("head", [ + Element { tag: "meta", attributes: [ attr(name: "charset", value: "utf-8" ) ], children: [] }, + Element { + tag: "meta", + attributes: [ + attr(name: "name", value: "viewport" ), + attr(name: "content", value: "width=device-width, initial-scale=1" ), + ], + children: [], + }, + el("style", [ txt(instrument_css()) ]), + el("title", [ txt("gunbc — instrument study") ]), + ]), + el("body", [ + instrument_study_header(), + el_class("main", instrument_sandbox_page_class, [ + camera_section(), + salience_section(), + audition_section(), + physical_section(), + ]), + ]), + ], + } +} diff --git a/dag/gunbc/roadmap_interaction.dag b/dag/gunbc/roadmap_interaction.dag index e98c54dd878..5dc66a70984 100644 --- a/dag/gunbc/roadmap_interaction.dag +++ b/dag/gunbc/roadmap_interaction.dag @@ -4,7 +4,7 @@ import std.types { Int, String, Bool } import std.decl_ref { DeclarationRef, WholeDeclaration } import gunbc.design.material { TimingToken, respond_fast, reveal_deliberate, settle_spring, - MotionTrigger, OnHover, OnActive, OnStateClass, + MotionTrigger, OnHover, OnActive, OnStateClass, css_trigger_for, BuildRule, StaticRule, ResponseRule, SelfResponse, CssDecl, decl, rest_scale_per_mille, press_scale_per_mille, hold_scale_per_mille, @@ -15,6 +15,9 @@ import gunbc.design.state_response { StateVarRole, FillVar, InkVar, PressedVar, family_response_rules, } +import gunbc.design.interaction_cause { + InteractionCause, PointerApproach, FocusAcquired, PressEngaged, ObservedStateEntered, +} import gunbc.design.interaction { InteractionVerb, Approach, Dispatch, Await, Accept, Enter, Response, Brighten, Receipt, Lift, Depress, Settle, Turn, @@ -87,14 +90,14 @@ data roadmap_dispatch_detents: List = concat( [ Detent { state: detent_requested, - reach: ByTrigger { trigger: OnStateClass { class_name: dispatch_class_requested } }, + reach: ByTrigger { cause: ObservedStateEntered { state_name: dispatch_class_requested } }, travel: NoTravel, scale_per_mille: hold_scale_per_mille, turn_deg: 0, }, Detent { state: detent_accepted, - reach: ByTrigger { trigger: OnStateClass { class_name: dispatch_class_ok } }, + reach: ByTrigger { cause: ObservedStateEntered { state_name: dispatch_class_ok } }, travel: NoTravel, scale_per_mille: rest_scale_per_mille, turn_deg: 0, @@ -107,7 +110,7 @@ data roadmap_disclosure_detents: List = [ Detent { state: disclosure_detent_rest, reach: AtRest, travel: NoTravel, scale_per_mille: rest_scale_per_mille, turn_deg: 0 }, Detent { state: disclosure_open_class, - reach: ByTrigger { trigger: OnStateClass { class_name: disclosure_open_class } }, + reach: ByTrigger { cause: ObservedStateEntered { state_name: disclosure_open_class } }, travel: NoTravel, scale_per_mille: rest_scale_per_mille, turn_deg: 90, @@ -193,11 +196,11 @@ fn detent_rules(class_name: String, detents: List, state: String, timing let transform = decl(prop: Transform, value: detent_transform_wire(d: d)) match d.reach { AtRest => [ StaticRule { selector: ClassSelector { name: class_name }, decls: [transform] } ] - ByTrigger { trigger } => [ + ByTrigger { cause } => [ ResponseRule { subject: ClassSelector { name: class_name }, shape: SelfResponse, - trigger: trigger, + trigger: css_trigger_for(cause: cause), transition_props: "transform", timing: timing, base_decls: [], diff --git a/dag/gunbc/roadmap_serve.dag b/dag/gunbc/roadmap_serve.dag index fdead55652c..b481623b20c 100644 --- a/dag/gunbc/roadmap_serve.dag +++ b/dag/gunbc/roadmap_serve.dag @@ -38,6 +38,7 @@ import gunbc.roadmap_component { sandbox_client_js_source, sandbox_asset_path, } import gunbc.roadmap_sandbox { sandbox_page } +import gunbc.roadmap_instrument_sandbox { instrument_sandbox_page } import gunbc.roadmap_static_site { roadmap_site_roadmap_md_body, roadmap_site_dispatch_json_body, @@ -112,6 +113,7 @@ type RoadmapServeHandler | BeltDispatchHandler | DispatchAssetHandler | SandboxPageHandler + | InstrumentSandboxPageHandler | SandboxAssetHandler | SandboxEchoHandler | SessionsJsonHandler @@ -146,6 +148,7 @@ fn roadmap_serve_route_specs() -> List { RoadmapServeRouteSpec { method: GET, raw: "/workflow.json", handler: WorkflowJsonHandler }, RoadmapServeRouteSpec { method: GET, raw: roadmap_dispatch_asset_path, handler: DispatchAssetHandler }, RoadmapServeRouteSpec { method: GET, raw: "/sandbox", handler: SandboxPageHandler }, + RoadmapServeRouteSpec { method: GET, raw: "/sandbox/instrument", handler: InstrumentSandboxPageHandler }, RoadmapServeRouteSpec { method: GET, raw: sandbox_asset_path, handler: SandboxAssetHandler }, RoadmapServeRouteSpec { method: POST, raw: "/sandbox/echo", handler: SandboxEchoHandler }, RoadmapServeRouteSpec { method: POST, raw: "/dispatch/\{node_id\}", handler: BeltDispatchHandler }, @@ -396,6 +399,7 @@ fn roadmap_serve_invoke_for_instance( serve_dispatch_handler_response_for_instance(instance: instance, params: params) DispatchAssetHandler => serve_text_response(status: 200, content_type: text_javascript_utf8, body: dispatch_client_js_source()) SandboxPageHandler => serve_page_response(page: sandbox_page()) + InstrumentSandboxPageHandler => serve_page_response(page: instrument_sandbox_page()) SandboxAssetHandler => serve_text_response(status: 200, content_type: text_javascript_utf8, body: sandbox_client_js_source()) SandboxEchoHandler => sandbox_echo_response(request: request) SessionsJsonHandler => serve_sessions_response_for_instance(instance: instance) diff --git a/dag/gunbc/roadmap_style.dag b/dag/gunbc/roadmap_style.dag index 39aeea045f1..63b91a1fc6c 100644 --- a/dag/gunbc/roadmap_style.dag +++ b/dag/gunbc/roadmap_style.dag @@ -14,7 +14,7 @@ import gunbc.design.scale { radius_3, radius_999, border_1, border_2, measure_page, height_control, width_status, } import gunbc.design.theme { - Theme, day_theme, night_theme, theme_root_css, role_decl, + Theme, day_theme, night_theme, theme_root_css, theme_scoped_blocks, role_decl, CanvasRole, SurfaceRole, BorderRole, TextRole, TextDimRole, FigureRole, FocusRole, BoundaryRole, } @@ -217,17 +217,11 @@ fn auditioner_root_css() -> String { } fn band_root_css() -> String { - join([ - css_block(selector: ":root", decls: band_var_decls(rows: band_paints_for_theme(t: day_theme))), - css_block( - selector: join([":root[data-theme=\"", night_theme.name, "\"]"], ""), - decls: band_var_decls(rows: band_paints_for_theme(t: night_theme))), - join([ - "@media (prefers-color-scheme: ", night_theme.scheme, ") { ", - css_block(selector: ":root:not([data-theme])", decls: band_var_decls(rows: band_paints_for_theme(t: night_theme))), - " }", - ], ""), - ], "\n") + theme_scoped_blocks( + base: day_theme, + alternate: night_theme, + decls_for: t => band_var_decls(rows: band_paints_for_theme(t: t)), + ) } fn roadmap_rules() -> List { diff --git a/dag/test/claim/design_register_lift_parity_witness_test.dag b/dag/test/claim/design_register_lift_parity_witness_test.dag index 0d2bdc7541a..d9b6a2a51fb 100644 --- a/dag/test/claim/design_register_lift_parity_witness_test.dag +++ b/dag/test/claim/design_register_lift_parity_witness_test.dag @@ -20,7 +20,9 @@ Two digests deliberately did NOT move, which is itself evidence the change is sc data moodboard_css_lift_parity_digest: String = "deaf2b36826760c2" data moodboard_repin_s1_selective_spectacle_note: String = "Re-pinned 2026-08-02 for the S1 selective-spectacle amendment (operator recalibration): the moodboard HTML, thesis/themes, and accent-study HTML digests move intentionally because the thesis string is revised (calm field; luminous focus; physical response; every response true) — both pages render register_thesis — and the principles table gains the three salience rows (selective-spectacle, emission-over-material, bounded-attraction, each carried by a gunbc.design.salience declaration). moodboard_css deliberately did NOT move (re-derived deaf2b36826760c2, equal to its pin) — the amendment is model-layer only, no stylesheet change, which is itself the scope evidence. Behavioral receipts: test.claim.salience_witness (budget table, focal budget refusal, emission refusals incl. sole-discriminator, attraction envelope). All three digests derived by execution (moodboard_html_derived_digest / moodboard_digest / accent_study_html_derived_digest run 2026-08-02), never chosen." -data moodboard_html_lift_parity_digest: String = "e43de6d61dc662ce" +data moodboard_repin_physical_enclosure_note: String = "Re-pinned 2026-08-05 for the PhysicalEnclosure amendment (the first v1-deletion instrument): the moodboard renders register_principles as a table, so the twelfth principle row and the restated StillUntilTouched law move its HTML bytes. Derived by execution (moodboard_html_derived_digest, run 2026-08-05), never chosen. FOUR PINS DELIBERATELY DID NOT MOVE, and CI is what established that rather than an assertion here: of the five digest witnesses in this file, exactly one went red on the amendment. moodboard_css did not move because the amendment is model-layer and adds no stylesheet rule; moodboard_thesis_themes did not move because register_thesis is untouched — the amendment adds a principle, it does not revise the thesis, which is the difference from the S1 re-pin above; accent_study_html did not move because it renders the thesis and not the principles table; and roadmap_css did not move even though gunbc.roadmap_style band_root_css was rewritten to call the new theme_scoped_blocks, which is the emission-identity proof for that consolidation — the same three selector blocks, byte for byte, from one authority instead of two copies. Behavioral receipt: test.claim.salience_witness (principle keys distinct, all carried, physical-enclosure present) and test.claim.instrument_physical_witness (the composed displacement budget the new principle names as its carrier)." + +data moodboard_html_lift_parity_digest: String = "4041adc0584f8c45" data accent_study_html_lift_parity_digest: String = "013dfb213ad0128f" data roadmap_css_digest_repin_note: String = "Re-pinned across the UI-model migration and the #7104 (SupersededLine) merge. P2 (token migration, px/font -> gunbc.design.scale var tokens) was proven visually-neutral by execution: resolving every var(--scale-token) reproduced the pre-P2 CSS byte-for-byte. P3 (presentation mapping) then INTENTIONALLY adds styling: the dispatch button's reserved min-width (derived from the longest wire label, in ch) and the ok/refusal/requested chip material rules (each painting the P0 state's role). D5 (typed CSS grain) is a pure re-grounding — property names and selector subjects become typed, bytes unchanged. The #7104 merge folds in the .status-superseded / .node-superseded / .superseded-by rules, RE-GROUNDED here onto the same typed+tokenized grain (their raw 11px/6px/font-family literals routed through the scale tokens so the untokened-length census stays green), which shifts the bytes off main's hardcoded emission — hence this digest re-pin. The behavioral receipts (roadmap_register_keystone, dispatch_presentation_keystone) and the untokened-length census remain the substance; this digest only pins bytes. Re-pinned again for #7169 (roadmap workspace UX): roadmap_style gained centered .roadmap/.daily-workspace auto side margins and related layout rules — bytes shift, behavioral receipts (roadmap_register_keystone, dispatch_presentation_keystone) unchanged." diff --git a/dag/test/claim/instrument_camera_witness_test.dag b/dag/test/claim/instrument_camera_witness_test.dag new file mode 100644 index 00000000000..34bca7c2632 --- /dev/null +++ b/dag/test/claim/instrument_camera_witness_test.dag @@ -0,0 +1,178 @@ +module test.claim.instrument_camera_witness + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.types { String, Bool, Int, List } +import gunbc.design.instrument_camera { + StateOwner, AuthoritativeProgramView, LocalInstrumentState, InstrumentObservation, + RendererEphemera, state_owner_key, owner_may_write_domain_fact, + ProgramDepth, DepthProgram, DepthOutcome, DepthFront, DepthNode, DepthEvidence, + program_depth_key, program_depth_index, DepthStep, Inward, Outward, step_depth, + ProgramMode, ModeStatus, ModeRemaining, ModeWhy, program_mode_key, + FocusSubject, NoSubjectSelected, FinishLineFocused, focus_subject_key, + focus_finish_line, focus_subject_eq, + ProgramCamera, camera_initial, camera_step_depth, camera_set_mode, camera_select, + camera_preserves_subject_across_depth, camera_preserves_subject_across_mode, +} +import gunbc.design.instrument_projection { + SubjectPlacement, RefusalAggregate, NoActiveRefusal, ActiveRefusals, refusal_count, + refusal_subject_key, finish_line_region, finish_line_placements, + project_salience, project_finish_line_salience, project_admission, + assignment_role_for, +} +import gunbc.design.salience { + SalienceRole, SalienceGround, SalienceSupporting, SalienceFocal, SalienceCritical, + salience_key, SalienceAssignment, FocalAdmission, FocalAdmitted, FocalBudgetExceeded, +} +import gunbc.v1_deletion_plan { + V1FinishLine, CompilerFixedPoint, InterpreterDeleted, ProductsV1Free, + ZeroHandMaintainedRust, v1_exit_finish_lines, v1_finish_line_key, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data instrument_camera_witness_note: String = "First v1-deletion instrument, model layer. Each claim is a decided law with the control that reds when it breaks: the camera cannot write a program fact and cannot skip a detent; the salience role is DERIVED from selection rather than handed in (firing salience_note's dissolve-on); and the derived assignments are judged by the same focal-admission fold that judges hand-authored ones, so the projection is checked by the register's own authority instead of by a second copy of its rule. The subjects are V0's four real v1-deletion finish lines read from gunbc.v1_deletion_plan, not a demo roster, so a fifth line reaches the instrument by being declared once." + +fn role_key_for(assignments: List, subject: String) -> String { + salience_key(role: assignment_role_for(assignments: assignments, subject: subject)) +} + +fn camera_on(l: V1FinishLine) -> ProgramCamera { + camera_select(c: camera_initial, f: focus_finish_line(l: l)) +} + +fn witness_only_the_authoritative_view_may_write_a_domain_fact() -> Bool { + owner_may_write_domain_fact(o: AuthoritativeProgramView) + && state_owner_key(o: AuthoritativeProgramView) == "authoritative-program-view" +} + +fn witness_red_no_instrument_owner_may_write_a_domain_fact() -> Bool { + !owner_may_write_domain_fact(o: LocalInstrumentState) + && !owner_may_write_domain_fact(o: InstrumentObservation) + && !owner_may_write_domain_fact(o: RendererEphemera) +} + +fn witness_camera_opens_outermost_with_nothing_selected() -> Bool { + program_depth_key(d: camera_initial.depth) == "program" + && program_mode_key(m: camera_initial.mode) == "status" + && focus_subject_key(f: camera_initial.focus) == "none" +} + +fn witness_depth_crosses_exactly_one_detent() -> Bool { + program_depth_index(d: step_depth(d: DepthProgram, step: Inward)) == program_depth_index(d: DepthProgram) + 1 + && program_depth_index(d: step_depth(d: DepthOutcome, step: Inward)) == program_depth_index(d: DepthOutcome) + 1 + && program_depth_index(d: step_depth(d: DepthFront, step: Inward)) == program_depth_index(d: DepthFront) + 1 + && program_depth_index(d: step_depth(d: DepthNode, step: Inward)) == program_depth_index(d: DepthNode) + 1 + && program_depth_index(d: step_depth(d: DepthEvidence, step: Outward)) == program_depth_index(d: DepthEvidence) - 1 + && program_depth_index(d: step_depth(d: DepthNode, step: Outward)) == program_depth_index(d: DepthNode) - 1 +} + +fn witness_red_depth_clamps_at_both_ends_instead_of_wrapping() -> Bool { + program_depth_key(d: step_depth(d: DepthEvidence, step: Inward)) == "evidence" + && program_depth_key(d: step_depth(d: DepthProgram, step: Outward)) == "program" +} + +fn witness_camera_moves_carry_the_subject_unchanged() -> Bool { + let c = camera_on(l: InterpreterDeleted) + camera_preserves_subject_across_depth(c: c, step: Inward) + && camera_preserves_subject_across_depth(c: c, step: Outward) + && camera_preserves_subject_across_mode(c: c, m: ModeWhy) + && camera_preserves_subject_across_mode(c: c, m: ModeRemaining) + && focus_subject_key(f: camera_set_mode(c: c, m: ModeWhy).focus) == "interpreter-deleted" +} + +fn witness_selecting_the_selected_subject_clears_it() -> Bool { + let c = camera_on(l: ProductsV1Free) + focus_subject_key(f: c.focus) == "products-v1-free" + && focus_subject_key(f: camera_select(c: c, f: focus_finish_line(l: ProductsV1Free)).focus) == "none" + && focus_subject_key(f: camera_select(c: c, f: focus_finish_line(l: CompilerFixedPoint)).focus) == "compiler-fixed-point" +} + +fn witness_instrument_subjects_are_the_real_v0_finish_lines() -> Bool { + let placements = finish_line_placements() + count(placements) == count(v1_exit_finish_lines()) + && count(placements) == 4 + && (placements |> any(p => p.key == v1_finish_line_key(l: ZeroHandMaintainedRust))) + && (placements |> any(p => p.key == v1_finish_line_key(l: CompilerFixedPoint))) + && count(placements |> filter(p => p.region == finish_line_region)) == 4 +} + +fn witness_selection_derives_focal_and_siblings_derive_supporting() -> Bool { + let a = project_finish_line_salience(camera: camera_on(l: CompilerFixedPoint), refusal: NoActiveRefusal) + role_key_for(assignments: a, subject: "compiler-fixed-point") == salience_key(role: SalienceFocal) + && role_key_for(assignments: a, subject: "interpreter-deleted") == salience_key(role: SalienceSupporting) + && role_key_for(assignments: a, subject: "products-v1-free") == salience_key(role: SalienceSupporting) + && role_key_for(assignments: a, subject: "zero-hand-maintained-rust") == salience_key(role: SalienceSupporting) +} + +fn witness_red_nothing_selected_spends_no_focal_energy() -> Bool { + let a = project_finish_line_salience(camera: camera_initial, refusal: NoActiveRefusal) + count(a |> filter(x => salience_key(role: x.role) == salience_key(role: SalienceFocal))) == 0 + && role_key_for(assignments: a, subject: "compiler-fixed-point") == salience_key(role: SalienceGround) + && role_key_for(assignments: a, subject: "interpreter-deleted") == salience_key(role: SalienceGround) +} + +fn witness_a_subject_outside_the_focal_region_stays_ground() -> Bool { + let placements = [ + SubjectPlacement { key: "compiler-fixed-point", region: finish_line_region }, + SubjectPlacement { key: "interpreter-deleted", region: finish_line_region }, + SubjectPlacement { key: "instrument-chrome", region: "instrument-chrome" }, + ] + let a = project_salience( + camera: camera_on(l: CompilerFixedPoint), + placements: placements, + refusal: NoActiveRefusal, + ) + role_key_for(assignments: a, subject: "compiler-fixed-point") == salience_key(role: SalienceFocal) + && role_key_for(assignments: a, subject: "interpreter-deleted") == salience_key(role: SalienceSupporting) + && role_key_for(assignments: a, subject: "instrument-chrome") == salience_key(role: SalienceGround) +} + +fn witness_an_active_refusal_is_one_critical_subject_however_many_refuse() -> Bool { + let a = project_finish_line_salience( + camera: camera_on(l: CompilerFixedPoint), + refusal: ActiveRefusals { refused_count: 3 }, + ) + count(a |> filter(x => salience_key(role: x.role) == salience_key(role: SalienceCritical))) == 1 + && role_key_for(assignments: a, subject: refusal_subject_key) == salience_key(role: SalienceCritical) + && refusal_count(r: ActiveRefusals { refused_count: 3 }) == 3 + && refusal_count(r: NoActiveRefusal) == 0 +} + +fn witness_critical_interrupts_without_dethroning_the_derived_focal_subject() -> Bool { + match project_admission( + camera: camera_on(l: ZeroHandMaintainedRust), + placements: finish_line_placements(), + refusal: ActiveRefusals { refused_count: 2 }, + ) { + FocalAdmitted { focal_count, critical_count } => focal_count == 1 && critical_count == 1 + FocalBudgetExceeded { region, focal_count } => false + } +} + +fn witness_red_the_projection_never_spends_two_focal_budgets() -> Bool { + match project_admission( + camera: camera_on(l: InterpreterDeleted), + placements: finish_line_placements(), + refusal: NoActiveRefusal, + ) { + FocalAdmitted { focal_count, critical_count } => focal_count == 1 && critical_count == 0 + FocalBudgetExceeded { region, focal_count } => false + } +} + +test fn instrument_camera_keystone_holds() -> Bool { + witness_only_the_authoritative_view_may_write_a_domain_fact() + && witness_red_no_instrument_owner_may_write_a_domain_fact() + && witness_camera_opens_outermost_with_nothing_selected() + && witness_depth_crosses_exactly_one_detent() + && witness_red_depth_clamps_at_both_ends_instead_of_wrapping() + && witness_camera_moves_carry_the_subject_unchanged() + && witness_selecting_the_selected_subject_clears_it() + && witness_instrument_subjects_are_the_real_v0_finish_lines() + && witness_selection_derives_focal_and_siblings_derive_supporting() + && witness_red_nothing_selected_spends_no_focal_energy() + && witness_a_subject_outside_the_focal_region_stays_ground() + && witness_an_active_refusal_is_one_critical_subject_however_many_refuse() + && witness_critical_interrupts_without_dethroning_the_derived_focal_subject() + && witness_red_the_projection_never_spends_two_focal_budgets() +} diff --git a/dag/test/claim/instrument_physical_witness_test.dag b/dag/test/claim/instrument_physical_witness_test.dag new file mode 100644 index 00000000000..69e880a467b --- /dev/null +++ b/dag/test/claim/instrument_physical_witness_test.dag @@ -0,0 +1,259 @@ +module test.claim.instrument_physical_witness + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.types { String, Bool, Int, List } +import gunbc.design.instrument_physical { + InstrumentChannel, ChannelOpticalJitter, ChannelVerticalShift, ChannelBuoyantDrift, ChannelImpulseGlitch, + channel_key, channel_may_carry_domain_fact, + ImpulseGlitchDuration, ImpulseOff, ImpulseBrief, ImpulseLong, + glitch_duration_key, glitch_is_armed, glitch_settle, + ChannelAmplitude, ChannelDisabled, ChannelAmplitudePx, amplitude_px, + InstrumentPreference, preference_still, preference_default, channel_amplitude, + instrument_displacement_px, instrument_displacement_max_px, + ComposedVisualDisplacement, compose_displacement, admit_composed_displacement, + composed_total_px, focal_attraction_headroom_px, + DisplacementAdmission, DisplacementAdmitted, DisplacementOverBudget, + EnclosureCharacterReachesResponseTravel, displacement_admission, + channel_behaviour_axis, channel_provenance, channel_is_cited_precedent, + PhysicalImpulseSource, SyntheticImpulse, HostAccelerometer, HostDeviceMotion, + impulse_source_key, + SensorAvailability, SensorPresent, SensorAbsent, SensorPermissionNotRequested, + SensorPermissionDenied, SensorAvailabilityUnknown, + sensor_availability_key, sensor_may_deliver_impulses, + ImpulseAdmission, ImpulseAdmitted, ImpulseSourceUnavailable, ImpulseChannelDisabled, + admit_impulse, +} +import gunbc.design.reference_instrument { behaviour_axis_key } +import gunbc.design.instrument_audition { + AuditionIntensity, AuditionRestrained, AuditionExpressive, AuditionHero, + audition_intensity_key, audition_intensities, + AuditionEmission, AuditionNoEmission, AuditionEmits, audition_emission, + AuditionAttraction, AuditionNoAttraction, AuditionAttracts, audition_attraction, + AuditionAdmission, AuditionAdmitted, AuditionEmissionRefused, + AuditionAttractionOutsideEnvelope, AuditionDisplacementOverBudget, admit_audition, +} + +import gunbc.design.salience { + SalienceRole, SalienceFocal, SalienceSupporting, attraction_travel_max_px, +} + + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data instrument_physical_witness_note: String = "The physical-character amendment and the focal audition, each law with the control that reds it. Three of these claims exist because a review found the corresponding hole: an amplitude was a signed Int so two channels could cancel and pass the budget; the enclosure and the focal plate were admitted by SEPARATE gates so each passed while the plate moved farther than either bound described; and the composed law said below while the arithmetic admitted equality. The reading claims that used to live here moved to the sandbox witness when the camera was rewired to read gunbc.roadmap_program_view instead of authored rows." + +fn preference_over_budget() -> InstrumentPreference { + InstrumentPreference { + optical_jitter: ChannelAmplitudePx { px: 6 }, + vertical_shift: ChannelAmplitudePx { px: 6 }, + buoyant_drift: ChannelAmplitudePx { px: 6 }, + impulse_glitch: ChannelAmplitudePx { px: 6 }, + glitch_duration: ImpulseLong, + } +} + +fn witness_no_instrument_channel_may_carry_a_domain_fact() -> Bool { + !channel_may_carry_domain_fact(c: ChannelOpticalJitter) + && !channel_may_carry_domain_fact(c: ChannelVerticalShift) + && !channel_may_carry_domain_fact(c: ChannelBuoyantDrift) + && !channel_may_carry_domain_fact(c: ChannelImpulseGlitch) +} + +fn witness_every_channel_off_position_is_total() -> Bool { + instrument_displacement_px(p: preference_still) == 0 + && amplitude_px(a: channel_amplitude(p: preference_still, c: ChannelOpticalJitter)) == 0 + && amplitude_px(a: channel_amplitude(p: preference_still, c: ChannelVerticalShift)) == 0 + && amplitude_px(a: channel_amplitude(p: preference_still, c: ChannelBuoyantDrift)) == 0 + && amplitude_px(a: channel_amplitude(p: preference_still, c: ChannelImpulseGlitch)) == 0 + && !glitch_is_armed(g: preference_still.glitch_duration) +} + +fn witness_composed_displacement_stays_under_the_register_attraction_travel() -> Bool { + instrument_displacement_max_px == attraction_travel_max_px + && instrument_displacement_px(p: preference_default) < attraction_travel_max_px + && match displacement_admission(p: preference_default) { + DisplacementAdmitted { total_px } => total_px == 6 + DisplacementOverBudget { total_px, max_px } => false + EnclosureCharacterReachesResponseTravel { character_px, max_px } => false + } +} + +fn witness_red_four_legal_channels_can_sum_to_an_illegal_instrument() -> Bool { + match displacement_admission(p: preference_over_budget()) { + DisplacementOverBudget { total_px, max_px } => + total_px == 24 && max_px == attraction_travel_max_px + EnclosureCharacterReachesResponseTravel { character_px, max_px } => + character_px == 18 && max_px == attraction_travel_max_px + DisplacementAdmitted { total_px } => false + } +} + +fn witness_only_a_present_sensor_delivers_impulses() -> Bool { + sensor_may_deliver_impulses(a: SensorPresent) + && !sensor_may_deliver_impulses(a: SensorAbsent) + && !sensor_may_deliver_impulses(a: SensorPermissionNotRequested) + && !sensor_may_deliver_impulses(a: SensorPermissionDenied) + && !sensor_may_deliver_impulses(a: SensorAvailabilityUnknown) +} + +fn witness_red_an_uninterrogated_sensor_stays_distinct_from_a_missing_one() -> Bool { + sensor_availability_key(a: SensorAvailabilityUnknown) != sensor_availability_key(a: SensorAbsent) + && sensor_availability_key(a: SensorPermissionDenied) != sensor_availability_key(a: SensorAbsent) + && sensor_availability_key(a: SensorPermissionNotRequested) != sensor_availability_key(a: SensorPermissionDenied) + && match admit_impulse(p: preference_default, s: HostAccelerometer, sensor: SensorAvailabilityUnknown) { + ImpulseSourceUnavailable { source, availability } => availability == "availability-unknown" + ImpulseAdmitted { source, settle } => false + ImpulseChannelDisabled { source } => false + } +} + +fn witness_the_synthetic_source_auditions_on_a_machine_with_no_sensor() -> Bool { + match admit_impulse(p: preference_default, s: SyntheticImpulse, sensor: SensorAbsent) { + ImpulseAdmitted { source, settle } => source == "synthetic" && settle.duration_ms > 0 + ImpulseSourceUnavailable { source, availability } => false + ImpulseChannelDisabled { source } => false + } +} + +fn witness_red_a_disabled_glitch_channel_refuses_a_real_impulse() -> Bool { + match admit_impulse(p: preference_still, s: SyntheticImpulse, sensor: SensorPresent) { + ImpulseChannelDisabled { source } => source == "synthetic" + ImpulseAdmitted { source, settle } => false + ImpulseSourceUnavailable { source, availability } => false + } +} + +fn witness_red_a_denied_permission_refuses_with_its_own_cause() -> Bool { + match admit_impulse(p: preference_default, s: HostDeviceMotion, sensor: SensorPermissionDenied) { + ImpulseSourceUnavailable { source, availability } => + source == "host-device-motion" && availability == "permission-denied" + ImpulseAdmitted { source, settle } => false + ImpulseChannelDisabled { source } => false + } +} + +fn audition_admitted(i: AuditionIntensity) -> Bool { + match admit_audition(i: i, role: SalienceFocal, subject_key: "compiler-fixed-point") { + AuditionAdmitted { intensity, emission, attraction, displacement_px } => + intensity == audition_intensity_key(i: i) && displacement_px <= attraction_travel_max_px + AuditionEmissionRefused { intensity, grant } => false + AuditionAttractionOutsideEnvelope { intensity } => false + AuditionDisplacementOverBudget { intensity, total_px, max_px } => false + } +} + +fn witness_all_three_intensities_are_admitted_at_the_focal_role() -> Bool { + count(audition_intensities) == 3 + && audition_admitted(i: AuditionRestrained) + && audition_admitted(i: AuditionExpressive) + && audition_admitted(i: AuditionHero) +} + +fn witness_the_restrained_baseline_requests_no_emission_and_no_attraction() -> Bool { + match audition_emission(i: AuditionRestrained) { + AuditionNoEmission => match audition_attraction(i: AuditionRestrained) { + AuditionNoAttraction => true + AuditionAttracts { field } => false + } + AuditionEmits { spec } => false + } +} + +fn witness_red_the_same_audition_refuses_at_a_supporting_role() -> Bool { + match admit_audition(i: AuditionHero, role: SalienceSupporting, subject_key: "compiler-fixed-point") { + AuditionEmissionRefused { intensity, grant } => intensity == "hero" + AuditionAdmitted { intensity, emission, attraction, displacement_px } => false + AuditionAttractionOutsideEnvelope { intensity } => false + AuditionDisplacementOverBudget { intensity, total_px, max_px } => false + } +} + +fn witness_red_the_restrained_baseline_still_renders_at_a_supporting_role() -> Bool { + match admit_audition(i: AuditionRestrained, role: SalienceSupporting, subject_key: "compiler-fixed-point") { + AuditionAdmitted { intensity, emission, attraction, displacement_px } => + intensity == "restrained" && displacement_px == 0 + AuditionEmissionRefused { intensity, grant } => false + AuditionAttractionOutsideEnvelope { intensity } => false + AuditionDisplacementOverBudget { intensity, total_px, max_px } => false + } +} + +data composed_envelope_note: String = "The three holes the review found in the first displacement model, each with the control that would have caught it: signed amplitudes could cancel, the prose said below while the check admitted equality, and the enclosure and the focal plate were bounded by separate gates that could not see each other." + +fn witness_red_enclosure_and_attraction_cannot_pass_separately() -> Bool { + match admit_composed_displacement(d: compose_displacement( + p: preference_default, + focal_attraction_px: attraction_travel_max_px, + )) { + DisplacementOverBudget { total_px, max_px } => + total_px == 6 + attraction_travel_max_px && max_px == attraction_travel_max_px + DisplacementAdmitted { total_px } => false + EnclosureCharacterReachesResponseTravel { character_px, max_px } => false + } +} + +fn witness_the_headroom_is_what_the_enclosure_left_unspent() -> Bool { + focal_attraction_headroom_px(p: preference_default) == attraction_travel_max_px - 6 + && match admit_composed_displacement(d: compose_displacement( + p: preference_default, + focal_attraction_px: focal_attraction_headroom_px(p: preference_default), + )) { + DisplacementAdmitted { total_px } => total_px == attraction_travel_max_px + DisplacementOverBudget { total_px, max_px } => false + EnclosureCharacterReachesResponseTravel { character_px, max_px } => false + } +} + +fn witness_red_enclosure_character_alone_may_not_reach_response_travel() -> Bool { + match admit_composed_displacement(d: ComposedVisualDisplacement { + enclosure_character_px: attraction_travel_max_px, + focal_attraction_px: 0, + impulse_transient_px: 0, + }) { + EnclosureCharacterReachesResponseTravel { character_px, max_px } => + character_px == attraction_travel_max_px && max_px == attraction_travel_max_px + DisplacementAdmitted { total_px } => false + DisplacementOverBudget { total_px, max_px } => false + } +} + +data provenance_edge_witness_note: String = "The provenance is an edge now, so it is checkable: three channels resolve to axes cited on a real product declaration, and the drift resolves to an axis this repository originated. A prose paragraph could not be asked either question." + +fn witness_channel_provenance_is_a_typed_edge() -> Bool { + channel_is_cited_precedent(c: ChannelOpticalJitter) + && channel_is_cited_precedent(c: ChannelVerticalShift) + && channel_is_cited_precedent(c: ChannelImpulseGlitch) + && !channel_is_cited_precedent(c: ChannelBuoyantDrift) + && behaviour_axis_key(a: channel_behaviour_axis(c: ChannelBuoyantDrift)) == "buoyant-drift" + && behaviour_axis_key(a: channel_behaviour_axis(c: ChannelOpticalJitter)) == "optical-instability" +} + +data local_vocabulary_note: String = "The transient names are ours and say so; the cited Persistent behaviour is a latch we do not model, so no arm claims it." + +fn witness_the_transient_vocabulary_is_local_and_decaying() -> Bool { + glitch_duration_key(g: ImpulseOff) == "off" + && glitch_duration_key(g: ImpulseBrief) == "brief" + && glitch_duration_key(g: ImpulseLong) == "long" + && glitch_settle(g: ImpulseLong).duration_ms > glitch_settle(g: ImpulseBrief).duration_ms +} + +test fn instrument_physical_keystone_holds() -> Bool { + witness_no_instrument_channel_may_carry_a_domain_fact() + && witness_every_channel_off_position_is_total() + && witness_composed_displacement_stays_under_the_register_attraction_travel() + && witness_red_four_legal_channels_can_sum_to_an_illegal_instrument() + && witness_only_a_present_sensor_delivers_impulses() + && witness_red_an_uninterrogated_sensor_stays_distinct_from_a_missing_one() + && witness_the_synthetic_source_auditions_on_a_machine_with_no_sensor() + && witness_red_a_disabled_glitch_channel_refuses_a_real_impulse() + && witness_red_a_denied_permission_refuses_with_its_own_cause() + && witness_all_three_intensities_are_admitted_at_the_focal_role() + && witness_the_restrained_baseline_requests_no_emission_and_no_attraction() + && witness_red_the_same_audition_refuses_at_a_supporting_role() + && witness_red_the_restrained_baseline_still_renders_at_a_supporting_role() + && witness_red_enclosure_and_attraction_cannot_pass_separately() + && witness_the_headroom_is_what_the_enclosure_left_unspent() + && witness_red_enclosure_character_alone_may_not_reach_response_travel() + && witness_channel_provenance_is_a_typed_edge() + && witness_the_transient_vocabulary_is_local_and_decaying() +} diff --git a/dag/test/claim/instrument_sandbox_witness_test.dag b/dag/test/claim/instrument_sandbox_witness_test.dag new file mode 100644 index 00000000000..99980436593 --- /dev/null +++ b/dag/test/claim/instrument_sandbox_witness_test.dag @@ -0,0 +1,213 @@ +module test.claim.instrument_sandbox_witness + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.types { String, Bool, Int, List } +import gunbc.roadmap_instrument_sandbox { + instrument_css, instrument_css_at_role, + instrument_emission_root_css_for, audition_emission_var, + audition_subject_key, audition_subject_role, +} +import gunbc.design.instrument_audition { + AuditionIntensity, AuditionRestrained, AuditionExpressive, AuditionHero, + AuditionAdmission, AuditionAdmitted, AuditionEmissionRefused, + AuditionAttractionOutsideEnvelope, AuditionDisplacementOverBudget, admit_audition, +} +import gunbc.design.instrument_physical { preference_default, instrument_displacement_px } +import gunbc.design.salience { + SalienceRole, SalienceFocal, SalienceSupporting, SalienceGround, salience_key, +} +import gunbc.design.instrument_audition { + ProgramReading, ReadingNoSubject, ReadingProgramShape, ReadingOutcomeStatus, + ReadingOutcomeRemaining, ReadingConstraint, ReadingNoConstraint, ReadingFront, + ReadingUnavailable, read_camera, +} +import gunbc.design.instrument_camera { + ProgramCamera, ProgramDepth, ProgramMode, DepthProgram, DepthOutcome, + ModeStatus, ModeRemaining, FinishLineFocused, +} +import gunbc.roadmap_program_view { + V1DeletionProgramView, FinishLineView, RemainingShape, ProposedCarrierAbsent, + V1ConvergenceFront, NamespacePDeriveFront, +} +import gunbc.v1_deletion_plan { V1FinishLine, CompilerFixedPoint } +import gunbc.roadmap_model { RoadmapNodeId } +import v2.std.optional { Absent } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data instrument_sandbox_witness_note: String = "RESHAPED AROUND THE PRODUCTION JOINS, because the first set proved less than it claimed (review finding, 2026-08-05). Three of its claims were substring theatre: the role witness searched the page for the words focal / supporting / ground / critical, which any page mentioning salience contains whether or not a single role was derived; the theme-block helper checked that one variable existed somewhere and that three selectors existed somewhere, never that the variable appeared INSIDE each block; and the press witness equated one translateY rule with a realized CRT glitch. Worst of all, nothing tested the property that turned out to be broken — that a REFUSED audition cannot paint." + +data mechanism_half_note: String = "THE MECHANISM HALF, and the split is measured rather than aesthetic. Every claim below is a property of the register's own gates — which role the projection derives, whether emission is granted, whether a refused role can paint, whether the emission variable lands inside each theme block — and each measured 0-2ms by execution (claim_batch attribution, 2026-08-05). None of them renders the served page or reads the live program view, which is why they are cheap and why they belong per-PR: the 2026-08-04 admission ruling holds that the mechanism half of a live-population subject is NEVER the part that gets deferred. The page-rendering and live-view claims measured 5074ms thread-CPU together, exceeded the fast-lane budget, and moved to dag/test/claim/long/instrument_sandbox_live_witness_test.dag with a declared ceiling and a named executing consumer — not deleted, and not left in a directory that quietly removes them from discovery. Read that file's header for the cost attribution and the dissolve-on that brings these back together." + +fn emission_var_ref(i: AuditionIntensity) -> String { + concat("--", concat(audition_emission_var(i: i), ":")) +} + +fn emission_is_none_for(role: SalienceRole, i: AuditionIntensity) -> Bool { + string_contains( + s: instrument_emission_root_css_for(role: role), + pattern: concat(emission_var_ref(i: i), " none"), + ) +} + +fn admission_grants(role: SalienceRole, i: AuditionIntensity) -> Bool { + match admit_audition(i: i, role: role, subject_key: audition_subject_key()) { + AuditionAdmitted { intensity, emission, attraction, displacement_px } => true + AuditionEmissionRefused { intensity, grant } => false + AuditionAttractionOutsideEnvelope { intensity } => false + AuditionDisplacementOverBudget { intensity, total_px, max_px } => false + } +} + +fn last_segment(s: String, marker: String) -> String { + fold(split(s: s, delimiter: marker), init: "", f: (acc, part) => part) +} + +fn first_segment(s: String, marker: String) -> String { + fold(split(s: s, delimiter: marker), init: "", f: (acc, part) => if acc == "" { part } else { acc }) +} + +data derived_role_witness_note: String = "The load-bearing claim: the role the audition is admitted at is the one the projection derived for the selected subject, not a literal." + +fn witness_the_served_role_is_the_derived_one() -> Bool { + salience_key(role: audition_subject_role()) == salience_key(role: SalienceFocal) + && audition_subject_key() == "compiler-fixed-point" +} + +fn witness_emission_is_present_exactly_when_the_admission_grants_it() -> Bool { + let role = audition_subject_role() + admission_grants(role: role, i: AuditionExpressive) + && admission_grants(role: role, i: AuditionHero) + && !emission_is_none_for(role: role, i: AuditionExpressive) + && !emission_is_none_for(role: role, i: AuditionHero) + && emission_is_none_for(role: role, i: AuditionRestrained) +} + +data refused_cannot_paint_note: String = "THE CONTROL THE FIRST WITNESS SET DID NOT HAVE. Render the same study at a role the register refuses emission for; no emission may appear in the emitted CSS at all. This is the property that was actually broken — the glow painted while the verdict printed refused underneath it — so it is the one claim here whose failure would have caught the original defect." + +fn witness_red_a_refused_audition_paints_nothing() -> Bool { + !admission_grants(role: SalienceSupporting, i: AuditionHero) + && !admission_grants(role: SalienceGround, i: AuditionHero) + && emission_is_none_for(role: SalienceSupporting, i: AuditionRestrained) + && emission_is_none_for(role: SalienceSupporting, i: AuditionExpressive) + && emission_is_none_for(role: SalienceSupporting, i: AuditionHero) + && emission_is_none_for(role: SalienceGround, i: AuditionHero) + && !string_contains(s: instrument_css_at_role(role: SalienceSupporting), pattern: "0 0 20px") + && !string_contains(s: instrument_css_at_role(role: SalienceSupporting), pattern: "0 0 48px") +} + +data block_position_note: String = "Occurrence INSIDE each theme block, not merely somewhere in the stylesheet: the CSS is split on the two later block selectors and the variable is required in every resulting piece. The first version asserted the variable existed and the selectors existed, which one hand-written block would have satisfied while the toggle silently did nothing." + +fn witness_the_emission_var_occurs_inside_every_theme_block() -> Bool { + let css = instrument_emission_root_css_for(role: audition_subject_role()) + let v = emission_var_ref(i: AuditionHero) + let day_block = first_segment(s: css, marker: ":root[data-theme=") + let media_block = last_segment(s: css, marker: "@media (prefers-color-scheme:") + let alt_block = first_segment(s: last_segment(s: css, marker: ":root[data-theme="), marker: "@media") + string_contains(s: day_block, pattern: v) + && string_contains(s: alt_block, pattern: v) + && string_contains(s: media_block, pattern: v) + && string_contains(s: media_block, pattern: ":root:not([data-theme])") +} + +data press_css_note: String = "The CSS half of the press specimen — the bounded translation on the focusable control and the displacement budget behind it. The markup half (that the rendered page actually carries a button) needs the page, so it lives with the live claims; keeping the two halves apart is what lets the cheap half stay per-PR instead of riding the expensive one's budget." + +fn witness_the_press_response_is_a_bounded_translation() -> Bool { + let css = instrument_css() + string_contains(s: css, pattern: ".instrument-frame:active") + && string_contains(s: css, pattern: "translateY(-3px)") + && instrument_displacement_px(p: preference_default) == 6 +} + +data program_grain_fixture_note: String = "A PLANTED VIEW, because this claim's oracle must be independent of the live roadmap. The fixture's PROGRAM remaining and its one FINISH LINE's remaining are deliberately different numbers (open_fronts 7 versus 1, startable_now 5 versus 0), so a reader that collapses program grain onto outcome grain is caught by VALUE and not merely by variant — asserting the variant alone would still pass if some future arm returned a program-shaped reading built from the line's own shape. Cheap by construction: the record is built directly rather than derived through program_view, so this mechanism claim costs microseconds and stays per-PR while the live half runs on the falsifier lane." + +fn fixture_line_remaining() -> RemainingShape { + RemainingShape { + sequential_depth: 1, open_fronts: 1, startable_now: 0, in_flight: 0, + dependency_held: 0, contract_held: 0, unsized: 0, + } +} + +fn fixture_program_remaining() -> RemainingShape { + RemainingShape { + sequential_depth: 9, open_fronts: 7, startable_now: 5, in_flight: 0, + dependency_held: 0, contract_held: 0, unsized: 0, + } +} + +fn fixture_view() -> V1DeletionProgramView { + V1DeletionProgramView { + finish_lines: [ + FinishLineView { + line: CompilerFixedPoint, + key: "compiler-fixed-point", + name: "Compiler fixed point", + claim: "fixture", + node: "fixture-node" as RoadmapNodeId, + accepted: false, + contributing_fronts: [NamespacePDeriveFront], + remaining: fixture_line_remaining(), + constraint: Absent, + }, + ], + fronts: [], + remaining: fixture_program_remaining(), + proposed: ProposedCarrierAbsent, + } +} + +fn focused_camera(m: ProgramMode, d: ProgramDepth) -> ProgramCamera { + ProgramCamera { depth: d, mode: m, focus: FinishLineFocused { line_key: "compiler-fixed-point" } } +} + +data program_grain_witness_note: String = "The claim review 48719 found missing. With a subject FOCUSED, the program detent must still read the whole program's shape — before the fix read_camera_at routed a focused DepthProgram into read_line_view, whose DepthProgram arm was byte-identical to its DepthOutcome one, so the page rendered outcome-grain numbers under a program label. This reds on that exact behaviour: it demands the program's own remaining (open_fronts 7), which the collapsed reader could not produce because it only ever saw the line's 1." + +fn witness_the_program_detent_reads_program_grain_even_when_focused() -> Bool { + let status = read_camera(camera: focused_camera(m: ModeStatus, d: DepthProgram), view: fixture_view()) + let remaining = read_camera(camera: focused_camera(m: ModeRemaining, d: DepthProgram), view: fixture_view()) + match status { + ReadingProgramShape { remaining: rs } => rs.open_fronts == 7 && rs.startable_now == 5 + ReadingNoSubject => false + ReadingOutcomeStatus { name, node, accepted, open_fronts } => false + ReadingOutcomeRemaining { name, remaining: r } => false + ReadingConstraint { subject, kind, headline, in_flight, depth } => false + ReadingNoConstraint { subject_key, reason } => false + ReadingFront { key, name, closed, gates_accepted, gates_total } => false + ReadingUnavailable { mode, subject_key, cause } => false + } + && match remaining { + ReadingProgramShape { remaining: rs } => rs.open_fronts == 7 + ReadingNoSubject => false + ReadingOutcomeStatus { name, node, accepted, open_fronts } => false + ReadingOutcomeRemaining { name, remaining: r } => false + ReadingConstraint { subject, kind, headline, in_flight, depth } => false + ReadingNoConstraint { subject_key, reason } => false + ReadingFront { key, name, closed, gates_accepted, gates_total } => false + ReadingUnavailable { mode, subject_key, cause } => false + } +} + +data outcome_grain_still_line_scoped_note: String = "The other half of the same law, so the fix cannot be satisfied by making EVERY depth answer program-grain: at outcome depth the reading must still be the LINE's shape (open_fronts 1), not the program's 7." + +fn witness_red_the_outcome_detent_still_reads_the_line() -> Bool { + match read_camera(camera: focused_camera(m: ModeRemaining, d: DepthOutcome), view: fixture_view()) { + ReadingOutcomeRemaining { name, remaining: r } => r.open_fronts == 1 && name == "Compiler fixed point" + ReadingNoSubject => false + ReadingProgramShape { remaining: rs } => false + ReadingOutcomeStatus { name, node, accepted, open_fronts } => false + ReadingConstraint { subject, kind, headline, in_flight, depth } => false + ReadingNoConstraint { subject_key, reason } => false + ReadingFront { key, name, closed, gates_accepted, gates_total } => false + ReadingUnavailable { mode, subject_key, cause } => false + } +} + +test fn instrument_sandbox_keystone_holds() -> Bool { + witness_the_served_role_is_the_derived_one() + && witness_emission_is_present_exactly_when_the_admission_grants_it() + && witness_red_a_refused_audition_paints_nothing() + && witness_the_emission_var_occurs_inside_every_theme_block() + && witness_the_press_response_is_a_bounded_translation() + && witness_the_program_detent_reads_program_grain_even_when_focused() + && witness_red_the_outcome_detent_still_reads_the_line() +} diff --git a/dag/test/claim/long/instrument_sandbox_live_witness_test.dag b/dag/test/claim/long/instrument_sandbox_live_witness_test.dag new file mode 100644 index 00000000000..19668e8d3c1 --- /dev/null +++ b/dag/test/claim/long/instrument_sandbox_live_witness_test.dag @@ -0,0 +1,114 @@ +module test.claim.long.instrument_sandbox_live_witness + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.types { String, Bool, Int, List } +import gunbc.roadmap_serve { + InstrumentSandboxPageHandler, roadmap_serve_invoke_for_instance, +} +import gunbc.roadmap_dashboard_instance { srv2_preview_dashboard_instance } +import gunbc.roadmap_instrument_sandbox { + instrument_sandbox_page, instrument_css, live_program_view_result, + LiveProgramView, LiveViewDerived, LiveViewRefused, +} +import gunbc.v1_deletion_plan { v1_exit_finish_lines } +import gunbc.design.instrument_physical { preference_default, instrument_displacement_px } +import gunbc.roadmap_program_view { + V1ProgramViewResult, ProgramViewDerived, ProgramViewRefused, V1DeletionProgramView, +} +import extdeps.http.server { ServeHttpRequest, ServeHttpResponse, GET, media_type_wire_label } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data instrument_sandbox_live_long_note: String = "THE LIVE HALF OF THE INSTRUMENT SANDBOX WITNESS, re-homed off per-PR discovery (fast-lane BudgetExceeded, run 30986055960, 5074ms thread-CPU against the 5000ms budget). WHAT SPLIT AND WHY, measured rather than assumed: every claim here renders the served page or reads the live program view, and attribution by execution (claim_batch, this host, 2026-08-05) put 18510 of 19098ms of a single render inside ONE live_program_view_result call. The mechanism claims — the derived salience role, the emission/admission join, the refused-role controls, the theme-block position check — measured 0-2ms each and are NOT here: they stay per-PR in the parent file, because the 2026-08-04 admission ruling says a live-population subject decomposes into small discriminating mechanism fixtures per PR plus the irreducible live half on a cadence, and the mechanism half is never the part that moves. HONEST COST CLASSIFICATION, because the precedent rows on this lane each declare theirs: this is NOT settled corpus breadth. The projection's inputs cost 263ms to construct (25 declared roadmap nodes at 233ms, edges 2ms, receipts 15ms, finish-line and front specs 13ms) and deriving over them costs 5132ms — roughly twenty times the cost of building the data it reads, at n=25. No single hot spot survived inspection: program_relax_to_fixpoint does early-exit on a stable fixpoint, and roadmap_dependency_graph is a trivial map. The cost is diffuse — program_depth_lookup folds every row with no early exit, membership is tested by linear any-scans at every level, reverse adjacency is rebuilt once per finish line where roadmap_focus already hoists it, and program_dedupe_ids rescans its accumulator per element — each trivial at n=25 and summing to seconds only because they nest inside per-node, per-front and per-line maps in a tree-walking interpreter. So this row is enrolled with its cost declared and its improvement named, NOT relabelled as irreducible. WHAT WAS NOT DONE, named because the diagnostic that produced this split names it: the file was not moved to remove it from discovery and left unexecuted, and the keystone was not split into two per-PR test fns to draw two budgets — total cost would be unchanged and that is the relocation evasion wearing a different hat. Local recipe: claim_batch --source-root dag --source-root src/v2 --entry dag/test/claim/long/instrument_sandbox_live_witness_test.dag --function instrument_sandbox_live_keystone_holds. Dissolve-on: gunbc.roadmap_program_view's derivation is restructured off nested linear scans onto keyed lookup — then this eval lands under gunbc_ci_fast_lane_witness_eval_budget on a measured run, these claims re-merge into the parent file per-PR, and this file and its roster rows delete together." + +fn fixture_request(path: String) -> ServeHttpRequest { + ServeHttpRequest { method: GET, path: path, body: "" } +} + +fn served() -> ServeHttpResponse { + roadmap_serve_invoke_for_instance( + instance: srv2_preview_dashboard_instance(), + handler: InstrumentSandboxPageHandler, + params: [], + request: fixture_request(path: "/sandbox/instrument"), + ) +} + +fn last_segment(s: String, marker: String) -> String { + fold(split(s: s, delimiter: marker), init: "", f: (acc, part) => part) +} + +data study_not_instrument_note: String = "The page must not describe itself as the operable instrument, and the header must not carry controls it cannot operate. The dead-control claim is checked against the MARKUP, not the whole document: the register stylesheet is inlined in a style element and legitimately contains .theme-toggle and .sound-toggle rules, so searching the raw body for those words finds the CSS and reds on a page that has no such buttons. The first version of this claim did exactly that and was wrong for a reason worth keeping — a negative substring assertion over a document that embeds its own stylesheet is testing the stylesheet." + +fn body_markup(r: ServeHttpResponse) -> String { + last_segment(s: r.body, marker: "") +} + +fn witness_the_instrument_path_serves_html(r: ServeHttpResponse) -> Bool { + r.status == 200 + && media_type_wire_label(m: r.content_type) == "text/html; charset=utf-8" + && string_contains(s: r.body, pattern: "gunbc — instrument study") + && string_contains(s: r.body, pattern: "lang=\"en\"") + && string_contains(s: r.body, pattern: "width=device-width") +} + +fn witness_the_page_calls_itself_a_study_and_carries_no_dead_controls(body: String, markup: String) -> Bool { + string_contains(s: body, pattern: "instrument — static study") + && !string_contains(s: markup, pattern: "theme-toggle") + && !string_contains(s: markup, pattern: "sound-toggle") +} + +data post_7822_remeasure_note: String = "RE-MEASURED AFTER #7822, so the numbers in the header above are HISTORY not current state (2026-08-05). clever-deer-217's keyed-lookup restructure of gunbc.roadmap_program_view landed — program_depth_lookup onto map_get, membership maps, adjacency threaded once, and program_dedupe_ids onto a seen-map — and this keystone re-measured 17899ms -> 1843ms on the same host and binary, roughly a tenfold cut. That clears the 5000ms fast-lane budget the enrollment row originally named as its dissolve-on. It does NOT dissolve the row, because the operator moved the bar to a 500ms per-witness warning threshold on the same day: at 1843ms this would still be 3.7x over the warning line if re-merged per-PR. The residue is now mostly the served-page render rather than the projection, which is a different piece of work from the one #7822 did. Recorded here rather than left to inference because the header's 5074ms and its attribution are now stale, and a stale measurement in a carrier that exists to justify a deferral is the citation-rot class DESIGN section 3 names." + +data live_world_note: String = "The page reads the world V0 derives, live. If the projection refuses, the page renders the located causes rather than a smaller program. This is the claim the whole split exists to preserve: it is the one that cannot be proven on a planted fixture, because its subject is the real declared roadmap." + +fn witness_the_page_reads_the_live_derived_program_view() -> Bool { + match live_program_view_result() { + LiveViewDerived { view } => + count(view.finish_lines) == count(v1_exit_finish_lines()) + && count(view.fronts) > 0 + LiveViewRefused { causes } => false + } +} + +fn witness_the_page_renders_real_remaining_and_constraint_readings(body: String) -> Bool { + string_contains(s: body, pattern: "program / remaining") + && string_contains(s: body, pattern: "outcome / status") + && string_contains(s: body, pattern: "node / why") + && string_contains(s: body, pattern: "open fronts") +} + +data front_grain_witness_note: String = "The claim review 48579 found missing: the front grain renders the FIRST contributing front. The oracle is independent of the code under test — V0 derives the exemplar's contributing set as namespace-pderive then v2-generation, so the page must name the first front's own title and must NOT name the second's. A last-wins fold renders the second, which is exactly what the page did before the fix, so this claim reds on the real defect rather than on a restatement of the fix." + +fn witness_the_front_grain_shows_the_first_contributing_front(body: String, markup: String) -> Bool { + string_contains(s: body, pattern: "front / status") + && string_contains(s: body, pattern: "Namespace / P-derive") + && !string_contains(s: markup, pattern: "V2 generation and admission") +} + +data evidence_refusal_note: String = "Evidence depth refuses, and unlike the previous Why refusal this one is real: gunbc.roadmap_program_view records that the verification-receipt join is test-only, so no carrier can answer it yet. The witness pins the cause text so a future reader can tell this refusal from the fabricated one it replaced." + +fn witness_red_evidence_depth_refuses_with_its_real_cause(body: String) -> Bool { + string_contains(s: body, pattern: "evidence / status · compiler-fixed-point — unavailable:") + && string_contains(s: body, pattern: "verification-receipt join is test-only") +} + +data press_markup_note: String = "The markup half of the press specimen. Its CSS half — the :active rule, the bounded translation, the displacement budget — is cheap and stays per-PR in the parent file; only the assertion that the rendered page carries a real button lives here, because that one needs the page." + +fn witness_the_press_specimen_is_reachable_without_a_pointer(body: String) -> Bool { + string_contains(s: body, pattern: " Bool { + let r = served() + let body = r.body + let markup = body_markup(r: r) + witness_the_instrument_path_serves_html(r: r) + && witness_the_page_calls_itself_a_study_and_carries_no_dead_controls(body: body, markup: markup) + && witness_the_page_reads_the_live_derived_program_view() + && witness_the_page_renders_real_remaining_and_constraint_readings(body: body) + && witness_the_front_grain_shows_the_first_contributing_front(body: body, markup: markup) + && witness_red_evidence_depth_refuses_with_its_real_cause(body: body) + && witness_the_press_specimen_is_reachable_without_a_pointer(body: body) +} diff --git a/dag/test/claim/roadmap_serve_witness_test.dag b/dag/test/claim/roadmap_serve_witness_test.dag index c931c903cb6..d1f0b6d0751 100644 --- a/dag/test/claim/roadmap_serve_witness_test.dag +++ b/dag/test/claim/roadmap_serve_witness_test.dag @@ -5,7 +5,7 @@ import gunbc.roadmap_serve { RoadmapDailyPageHandler, RoadmapFullPageHandler, RoadmapMdHandler, DispatchJsonHandler, HealthzHandler, DashboardInstanceHandler, BeltDispatchHandler, DispatchAssetHandler, - SandboxPageHandler, SandboxAssetHandler, SandboxEchoHandler, + SandboxPageHandler, InstrumentSandboxPageHandler, SandboxAssetHandler, SandboxEchoHandler, SessionsJsonHandler, AttemptsJsonHandler, WorkflowJsonHandler, BeltStopHandler, BeltPublishHandler, RoadmapServeRouteSpec, @@ -68,6 +68,7 @@ test fn witness_serve_table_selection() -> Bool { && selects(method: GET, path: "/workflow.json", want: WorkflowJsonHandler) && selects(method: GET, path: roadmap_dispatch_asset_path, want: DispatchAssetHandler) && selects(method: GET, path: "/sandbox", want: SandboxPageHandler) + && selects(method: GET, path: "/sandbox/instrument", want: InstrumentSandboxPageHandler) && selects(method: GET, path: sandbox_asset_path, want: SandboxAssetHandler) && selects(method: POST, path: "/sandbox/echo", want: SandboxEchoHandler) && selects(method: POST, path: "/dispatch/some-node", want: BeltDispatchHandler) diff --git a/dag/test/claim/salience_witness_test.dag b/dag/test/claim/salience_witness_test.dag index e65a1f10951..5e4ff34f47f 100644 --- a/dag/test/claim/salience_witness_test.dag +++ b/dag/test/claim/salience_witness_test.dag @@ -185,12 +185,13 @@ test fn witness_principles_carry_the_amendment() -> Bool { register_thesis == "Calm field; luminous focus; physical response; every response true." && principles_all_carried(principles: register_principles) && principle_keys_distinct(principles: register_principles) - && count(register_principles) == 11 + && count(register_principles) == 12 && contains_key(keys: keys, key: "selective-spectacle") && contains_key(keys: keys, key: "emission-over-material") && contains_key(keys: keys, key: "bounded-attraction") && contains_key(keys: keys, key: "quiet-surface") && contains_key(keys: keys, key: "still-until-touched") + && contains_key(keys: keys, key: "physical-enclosure") } test fn salience_keystone_holds() -> Bool {