First v1-deletion instrument: semantic camera, focal salience, and physical screen audition

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"

dag/gunbc/ci_layer_roots.dag

@@ -446,6 +446,12 @@ data witness_exclusion_frontier: List<WitnessExclusionRow> = [
     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<SubstrateLongLaneRow> = [
     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",

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)
+}