Skip to content

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

Merged
briansrls merged 23 commits into
mainfrom
session/loyal-bat-373-instrument
Aug 5, 2026
Merged

briansrls merged 23 commits into
mainfrom
session/loyal-bat-373-instrument

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 5, 2026 •

Copy link
Copy Markdown
Contributor

Builds the first instrument over V0's real v1-deletion facts, and serves it at /sandbox/instrument. Nothing on the page is a mock: the subjects are the four finish lines declared in gunbc.v1_deletion_plan, the salience roles are derived rather than authored, and every audition verdict comes from the register's own admission gates.

What lands

Semantic camera (gunbc.design.instrument_camera). Four state owners, with owner_may_write_domain_fact true for exactly one of them and not reachable from the instrument. ProgramDepth = program · outcome · front · node · evidence on one axis; ProgramMode = status · remaining · why. History is deliberately absent — a mode with no historical projection behind it would be a fabricated affordance.

Two construction properties do the work. A ProgramCamera carries a depth, a mode, and a focus key — never a spec — so no gesture can carry a program fact to corrupt. And step_depth takes a direction, not a target, so a depth change crosses at most one detent and continuous zoom has no constructor.

Focal salience, derived (gunbc.design.instrument_projection). This fires the dissolve-on that gunbc.design.salience salience_note has been carrying: until now 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. project_salience decides them — selected → Focal, region siblings → Supporting, outside → Ground, aggregated refusal → one Critical — and hands the result to region_focal_admission, the same fold that judges hand-authored assignments. One authority, asked about derived rows instead of authored ones.

ActiveRefusals carries a std.integer PositiveInt, so "something is refusing, zero times" has no literal that constructs it.

Physical screen (gunbc.design.instrument_physical) — the register amendment, and the line it draws is the whole content. Still-until-touched governs the subjects; the instrument enclosing them is a physical object with its own idle behaviour. Drift, jitter, vertical shift and impulse glitch are admitted there and nowhere else, under three conditions that make them incapable of lying:

  • every channel carries no domain fact (channel_may_carry_domain_fact, total and constantly false — a fifth channel that did carry meaning would force an author to write a true into a function whose name says otherwise);
  • every channel is preference-controlled with a total off position;
  • the composed displacement of all four is bounded by attraction_travel_max_px, borrowed by reference from the register — because per-channel bounds are exactly what let four legal channels sum to an illegal instrument.

PhysicalImpulseSource names host capabilities (HostAccelerometer, HostDeviceMotion), not a browser, per the standing don't-anchor-to-browser/OS directive — a desktop realization inhabits the same shape. SensorAvailability has five states because the ones routinely collapsed into a single falsy "no sensor" are the ones that matter: absent, never-asked, denied, and could-not-interrogate have different remedies. SensorAvailabilityUnknown admits nothing and stays visibly distinct from absent.

Off / Short / Persistent is adopted verbatim from the cited Pip-Boy 3000's own setting rather than paraphrased, with the adoption recorded so the coincidence never reads as independent invention.

Focal audition (gunbc.design.instrument_audition). One real finish line at three energies. Restrained is the register as it stood before the amendment, so the baseline is the real previous state; hero sits at the emission envelope's admissible maximum, because an audition whose loudest option is comfortably inside the bound tells you nothing about where the bound is. Every intensity is admitted through emission_for, attraction_envelope and displacement_admission rather than audition-local bounds.

Why is not answered. No carrier in this repository records why a finish line has the shape it has, so it returns a typed ReadingUnavailable naming the missing carrier. Paraphrasing the claim into something that reads like a rationale is the fabricated-plausible-output arm wearing a UI — more dangerous than in a compiler, because nobody diffs a sentence on a screen. A focused key that resolves to nothing likewise refuses instead of reading as "no subject": collapsing those two is the empty-observation narrow.

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. Ambient motion has no constructor in this register by design (MotionTrigger carries no ambient variant; no keyframes constructor exists). Emitting raw animation text past that wall would be the unmarked-workaround class the design authority calls a line-stop signal. So the idle channels render as their measured budget, and the caused half — the impulse glitch on press — is real, built through the ordinary ResponseRule machinery. Dissolve-on is named in the module.

Two consolidations the work required

theme_scoped_blocks — the three-block theme-selector grammar (:root, [data-theme], prefers-color-scheme) was written longhand in theme_root_css and again in roadmap_style band_root_css. Rather than add a third copy for the emission vars, the declaration family is now a parameter and band_root_css is one call. A second copy of a selector grammar is a second place for the toggle to break in only one of them — the day/night switch working for colors and silently not for bands is a failure nobody would think to look for.

BoxShadow added to the cited CSS property enum (it is a real property; the alternative was RawProperty, the counted residue).

Register

PhysicalEnclosure lands as a principle row carried by displacement_admission. StillUntilTouched is restated to name its scope — "the causal world remains still until caused" — rather than reading as a blanket ban that the enclosure now contradicts.

Test plan

Green by execution, gunbc run --claim-run:

  • instrument_camera_witness_test — 14 claims (ownership, detent stepping, clamping, subject preservation, selection toggle, derived roles, refusal aggregation, focal budget)
  • instrument_physical_witness_test — 18 claims (no channel carries a domain fact, total off, composed budget, the over-budget refusal, glitch vocabulary, sensor five-way, impulse admission, three audition intensities, the supporting-role refusal, real V0 readings, the Why refusal, the drifted-key refusal)
  • instrument_sandbox_witness_test — 9 claims (the path serves HTML, V0's own claim text appears, the Why refusal prints as a refusal, derived roles render, all three audition cards, emission vars under all three theme selectors, restrained emits none, the press response, the impulse matrix)
  • salience_witness_test, roadmap_register_witness_test witness_roadmap_colors_all_routed — still green after the amendment and the theme_scoped_blocks consolidation

Discriminating control. Perturbing placement_role so region siblings fall to Ground reds the camera keystone (claim returned false). The projection witness discriminates; it is not decoration.

One local note. Running these against a wide closure surfaces dag/extdeps/cloud/gcp/secret_ref.dag: unresolved type 'GcpProjectId' — reproduced identically on the untouched roadmap_serve_witness_test, so it is the known Class B bare-reference/pool-membership defect in DESIGN's open threads, not this change.

Follow-on found while building this

The depth and mode variants were first named Program/Outcome/Front/Node/Evidence and Status/Remaining/Why. Node collided head-on with the substrate's own Node type. They now carry a type stem, matching the corpus convention (SalienceFocal, ReadingStatus). Same class as the Clock collision root-caused on #7809 this session — that one reached CI because it is invisible from inside the module that owns the name; this one was found by auditing for it.

gunbc-ci-auto-heal and others added 4 commits August 5, 2026 00:45
…al screen audition

Adds the model layer and a served /sandbox/instrument surface, all derived from
V0's four real v1-deletion finish lines rather than a demo roster.

- instrument_camera: four state owners (only the authoritative view may write a
  domain fact), ProgramDepth/ProgramMode/ProgramCamera. A camera carries a focus
  KEY, never a program fact, so no gesture can corrupt one. Depth crosses exactly
  one detent by construction (step takes a direction, not a target).
- instrument_projection: fires salience_note's declared dissolve-on. Roles are
  DERIVED from selection — selected Focal, region siblings Supporting, outside
  Ground, aggregated refusal one Critical — and judged by region_focal_admission,
  the same fold that judges hand-authored assignments.
- instrument_physical: the register amendment. Drift/jitter/shift/impulse are
  admitted on the ENCLOSURE only; every channel is preference-controlled with a
  total off position, carries no domain fact, and the COMPOSED displacement is
  bounded by the register's existing attraction travel. PhysicalImpulseSource
  names host capabilities, not a browser, per the standing don't-anchor directive.
- instrument_audition: one real finish line at three energies, each admitted
  through the register's own emission/attraction/displacement gates. Why has no
  rationale carrier, so it returns a typed refusal rather than paraphrasing the
  claim into something that reads like an answer.
- /sandbox/instrument: served page. The impulse glitch on press is real, built
  through the ordinary ResponseRule machinery. The IDLE channels are budgeted but
  not animated — ambient motion has no constructor in this register by design,
  and emitting past that wall would be an unmarked workaround. Dissolve-on named.
- theme_scoped_blocks: one theme-selector grammar, three var families. Removes
  the hand-rolled duplicate in roadmap_style band_root_css rather than adding a
  third copy.
- principles: PhysicalEnclosure added; StillUntilTouched restated to name its
  scope (the causal world, not the enclosure).

Verified by execution: 14 camera/projection witnesses, 18 physical/audition
witnesses, 9 served-page witnesses green; perturbing placement_role to drop
siblings to Ground reds the camera keystone, so the projection witness
discriminates.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
A bare nullary-variant identifier is a corpus-wide name in this substrate, not a
module-local one: the interpreter resolves an imported data item's free names
through a flat registry in the importing entry's closure. The first cut named
the depths Program/Outcome/Front/Node/Evidence and the modes Status/Remaining/
Why — and `Node` collided head-on with the substrate's own `Node` type, which is
the nicknaming violation before it is ever a resolution hazard. `Program` and
`Outcome` collide with real declarations too (product.compute_fabric,
v2.std.diagnostic).

Renamed to Depth*/Mode*, matching the convention the corpus already uses
(SalienceFocal, ReadingStatus, AuditionRestrained). Every projected key string
is unchanged — "program", "node", "why" — so nothing downstream moves.

Same class as the Clock collision this session root-caused on #7809; that one
reached CI because it is invisible from inside the module that owns the name.
This one was found by auditing for it instead.

Camera (14), physical/audition (18) and served-page (9) witnesses all still
green by execution after the rename.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot changed the title frontend First v1-deletion instrument: semantic camera, focal salience, and physical screen audition Aug 5, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 5, 2026 02:31
gunbc-ci-auto-heal and others added 19 commits August 5, 2026 03:34
CI red: witness_moodboard_html_digest_pinned. The moodboard renders
register_principles as a table, so the twelfth row and the restated
StillUntilTouched law move its bytes. Derived by execution
(moodboard_html_derived_digest), never chosen: e43de6d6 -> 4041adc0.

The four pins that did NOT move are the scope evidence, and CI established
that rather than this commit asserting it — of the five digest witnesses in
that file, exactly one went red:

- moodboard_css: the amendment is model-layer, adds no stylesheet rule
- moodboard_thesis_themes: register_thesis is untouched (the difference from
  the S1 re-pin, which DID revise the thesis)
- accent_study_html: renders the thesis, not the principles table
- roadmap_css: unchanged even though band_root_css was rewritten to call
  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

All five re-verified green by execution after the re-pin.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… prove the joins

Four blocking findings, all real. What each was and what closed it:

1. THE FOCAL VISUAL BYPASSED BOTH THE DERIVED ROLE AND ITS ADMISSION.
   audition_card passed SalienceFocal as a literal, and the stylesheet was
   generated from audition_emission regardless of the verdict — so a refused
   emission still painted and the admission only controlled the prose printed
   underneath it. Role now comes from project_finish_line_salience over the
   exemplar camera; emission is projected from AuditionAdmitted alone. The
   control that was missing is now the load-bearing one: render at a role the
   register refuses and no emission appears in the CSS at all.

2. THE CAMERA BYPASSED V0. This is the one worth stating plainly: the previous
   revision answered Why with a typed refusal whose cause read "no rationale
   carrier exists for a v1 finish line". That was FALSE when it was written.
   gunbc.roadmap_program_view was already on this branch's base, its header
   says it is "the world those cameras look at", and ConstraintView exists
   precisely to answer why-is-this-slow without inventing prose. The refusal
   was the empty-observation narrow — could-not-find rendered as does-not-exist
   — in the module whose own notes warn against it, and it reached review green
   because nothing about a refusal looks wrong without going to check.
   read_camera now takes a V1DeletionProgramView: Status reads FinishLineView,
   Remaining renders RemainingShape, Why renders ConstraintView, and the five
   depths project genuinely different grains. Evidence still refuses — that one
   is real, and gunbc.roadmap_program_view records the same gap.

3. PhysicalEnclosure STATED A GUARANTEE ITS CARRIER DID NOT ENFORCE, three ways.
   Amplitudes were signed Int so two channels could cancel and pass (now Nat).
   The prose said "below" while the check admitted equality (one rule now:
   composed may spend the envelope fully, enclosure character alone may not
   reach it). Enclosure and focal attraction were bounded by separate gates
   that could not see each other — now one ComposedVisualDisplacement over
   every positional contribution. That change has a consequence worth reading:
   the register's canonical focal_attraction spends 12 of its 14 declared
   pixels, so instrument character and canonical attraction are alternatives,
   not companions. The audition variants now differ by one channel each rather
   than hiding the trade.
   GlitchPersistent was a locally invented meaning on a cited word — the
   reference's persistent glitch is a LATCHED state a later tap reseats, not a
   longer decay. Our transients are named ImpulseOff/Brief/Long and the latch
   is recorded as an unmodelled interaction.

4. THE DISSOLVE-ON CLAUSES WERE ARMED. #7809 merged, so main is consumed and
   the prose provenance is replaced by the typed edge it promised:
   channel_behaviour_axis binds each channel to a reference_instrument axis,
   and ChannelBuoyantDrift resolving to an OriginatedHere axis is the case
   that makes the edge worth having.

Realization and witness cleanup, as asked: the page is called a static study,
declares lang and viewport, drops the header controls it cannot operate, makes
the press specimen a focusable button, and describes the translation as a press
response rather than a realized CRT glitch. The witnesses are reshaped around
the production joins — the three substring-theatre claims are gone, the theme
block check now asserts occurrence INSIDE each block by position, and the
refused-cannot-paint control exists.

Also fixed from the follow-up review: the DepthFront fold ignored its
accumulator, so last-wins ran under a first-wins comment and the exemplar
rendered v2-generation where namespace-pderive was promised. Selection is now
a separate take-first, witnessed against V0's own contributing order.

Green by execution: camera 14, physical/audition 20, sandbox 10.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…red witness edit

An automated gunbc-ci-auto-heal commit ("WIP: frontend", 499e736) swept an
uncommitted working tree onto this branch and pushed it. It carried two things
that were never meant to land:

  - dag/extdeps/cloud/gcp/secret_ref.dag: a transient `import ... { GcpProjectId }`
    used ONLY to work around the local Class B bare-reference resolution failure
    (DESIGN open threads) so the witness could be evaluated on this host. It is an
    unmarked workaround in an extdeps file, unrelated to this PR's brief, and
    DESIGN section 5 names that class a line-stop signal rather than a landing state.

  - dag/test/claim/instrument_sandbox_witness_test.dag: a restructure that threaded
    one shared render through the claims to cut a presumed six-renders cost shape.
    Measured under a controlled same-host comparison it changed nothing (old 19532ms
    vs new 20050ms) because nullary calls are memoized, so the duplicate renders were
    already free. The accompanying note asserted it fixed the fast-lane budget
    overage, which is false. Shipping a claim that measurement refutes is the exact
    defect class this PR has been correcting, so the edit is withdrawn rather than
    kept with softened prose.

Both files return to their 7df2afa content. The budget failure is real and remains
open; it is attributed in the PR discussion, not papered over here.
dag/test/claim/tmp_cost_attribution / tmp_pv_attribution were throwaway probes
used to split the sandbox witness's eval cost. A gunbc-ci-auto-heal "WIP: frontend"
commit swept the second one onto the branch and pushed it before it could be
deleted; this removes it. Nothing in the PR depends on it and its findings are
reported in the PR discussion, not carried as a test.
…the falsifier long lane

CI refused instrument_sandbox_keystone_holds at 5074ms thread-CPU against the
5000ms fast-lane budget (run 30986055960). Attribution by execution, not by
assumption:

  one served-page render        19098ms
    of which live_program_view   18510ms   (97%)
  instrument_css                   90ms
  derived role / emission / admission  0-2ms each

So the cost is one live V0 projection, and the register-gate claims are free.
Per the 2026-08-04 admission ruling a live-population subject decomposes into
small discriminating mechanism fixtures per PR plus the irreducible live half on
an enrolled cadence, and the mechanism half is never what moves:

  - per-PR (dag/test/claim/instrument_sandbox_witness_test.dag): derived role,
    the emission/admission join, the refused-role RED control, theme-block
    position, and the press CSS half. Measured 98ms, down from ~20050ms on this
    host, and it no longer pulls the serve closure at all.

  - falsifier long lane (dag/test/claim/long/instrument_sandbox_live_witness_test.dag):
    every claim that renders the page or reads the live view, including the
    front-grain claim from review 48579 and the evidence-refusal control.
    Measured 18399ms here; enrolled on falsifier_substrate_long_lane_rows with a
    WitnessExclusionRow so the carve-out from per-PR discovery is declared rather
    than implied by its directory.

The row does NOT claim irreducible corpus breadth. The projection's inputs cost
263ms to build and deriving over them costs 5132ms at n=25 nodes -- about 20x --
so the dissolve-on names the real fix: 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. program_relax_to_fixpoint
early-exits correctly and roadmap_dependency_graph is a trivial map; both were
checked and neither is the cause. When that derivation moves onto keyed lookup,
these claims re-merge per-PR and the long file, its roster row and its exclusion
row delete together.

Not done, and named because the diagnostic that produced this split names both:
the file was not relocated to drop it from discovery without an executing
consumer, 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 same evasion.
…itable (review 48719)

review 48719 is correct. read_line_view matched ProgramDepth and carried a
DepthProgram arm byte-identical to its DepthOutcome arm, and read_camera_at
routed BOTH into it whenever a subject was focused. So the program detent
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 held only with nothing selected. read_program_depth -- the sole
producer of ReadingProgramShape -- was unreachable under focus.

Fixed one rung above the report rather than at it. The suggestion was to route
DepthProgram to read_program_depth and reserve read_line_view for lower grains;
that corrects the arm but leaves the bad state writable, and this module has now
produced the same note-vs-code split three times. So the whole-program grain has
no representation in the line reader at all: SubjectDepth enumerates only the
grains that ARE a property of one finish line (Outcome, Node, Evidence),
DepthProgram cannot be projected into it, and no caller can hand the line reader
the program grain. A dead DepthFront arm went with it -- read_camera_at has
answered fronts through first_front_view since that fold landed.

Discriminating witness, per-PR because it is mechanism (117ms):
witness_the_program_detent_reads_program_grain_even_when_focused reads a PLANTED
view whose program remaining and line remaining are deliberately different
numbers (open_fronts 7 vs 1, startable_now 5 vs 0), so a collapse is caught by
VALUE, not merely by variant -- a variant-only assertion would still pass if some
future arm returned a program-shaped reading built from the line's own numbers.
witness_red_the_outcome_detent_still_reads_the_line is the other half, so the fix
cannot be satisfied by making every depth answer program-grain.

Proven by execution both ways: the witness FAILS when read_camera_at is perturbed
to route DepthProgram through SubjectOutcome, and PASSES on the fix. The original
bug is not reproducible by that perturbation because it is now unwritable -- the
perturbation simulates its effect. Long-lane live witness re-run green (17899ms).

reading_grain_note corrected in place to say what the code holds, and to record
that the sentence was false when written rather than quietly repairing it.
…next rung

Self-audit finding, not a reviewer's. The note claimed the derivation makes an
overrunning attraction impossible "by construction". It does not, for any
preference the envelope does not admit: the subtraction is total on Int, so 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 closed at the field in the composed-envelope fix is still reachable through
the derived path.

Bounded, which is why this is a prose correction rather than a carrier change:
it is unreached (preference_default spends 6 of 14) and the configuration that
would reach it is already refused by displacement_admission's
EnclosureCharacterReachesResponseTravel arm. The residual risk is a caller
reading headroom without consulting that admission first.

So the note now states the qualifier, records that the first version omitted it,
declares the rung honestly (mechanically preventable, ceiling structural
impossibility), and names the next-rung trigger per DESIGN 4b's no-untracked-stall
rule: headroom returns HeadroomAvailable { px: Nat } | HeadroomUnavailable, so a
caller cannot obtain a number when the enclosure has overspent. That change is
left for the operator rather than taken unilaterally -- it is a carrier change in
a PR already twice over its requested size, and the false claim is what needed
removing today.

Physical witness re-run green (3ms).
Same textual conflict as the last merge: main and this branch each appended a
SubstrateLongLaneRow to the end of falsifier_substrate_long_lane_rows. All three
kept, no semantic overlap -- they name three different entries.

Main's new row comes from #7822, which lands the keyed-lookup restructure of
gunbc.roadmap_program_view that this branch's long-lane row names as its dissolve-on
trigger. program_dedupe_ids is also fixed on that head (seen-map instead of the
per-element accumulator rescan), which was the residue flagged to clever-deer-217.

Whether this branch's dissolve-on actually fires is a measurement, not an inference,
and is checked separately rather than assumed here.
#7822 grew ProgramViewRefusalCause by DuplicateAcceptanceReceipt and
DuplicateProgramNodeId, and the compiler refused refusal_cause_text until both were
handled. Worth recording as a construction-wall receipt rather than a merge chore:
nobody had to NOTICE that V0 gained two refusal shapes, because no Accepted program
could be built without naming them.

The totality matters here beyond typechecking. This page's contract when the
projection refuses is that it renders the located causes instead of a smaller
program, so a cause the page could not name would be a cause the reader never sees --
the empty-observation narrow one layer out from where this PR already fixed it.
…easure after #7822

TWO FINDINGS, both by execution.

1. A RUNTIME BREAK THE TYPECHECK DID NOT CATCH. #7791 changed
roadmap_acceptance_receipts() from returning List<RoadmapAcceptanceReceipt> to
returning RoadmapAcceptanceReceiptsProjection, a coproduct. live_program_view_result
passed it straight into v1_program_view(receipts:), which compiled clean and failed
at runtime with "fold expects a list, got Variant". So a List-versus-coproduct swap
at a call site is a class the substrate does not currently wall -- worth naming,
since every other break this branch hit across merges was a compile refusal.

Fixed without fabricating: a receipts-projection refusal is NOT a
ProgramViewRefusalCause, so forwarding it as one would have put a cause in front of
the reader that the model never produced -- the exact failure this page exists to
avoid. LiveProgramView keeps both refusal sources and renders either as its own
located line, so the page contract is unchanged: refuse loudly with causes named,
never draw a smaller program.

2. THE DISSOLVE-ON IS RE-MEASURED, NOT INFERRED. #7822 landed the keyed-lookup
restructure this branch's long-lane row named, including program_dedupe_ids onto a
seen-map. This keystone re-measured 17899ms -> 1843ms on the same host and binary,
about a tenfold cut, which CLEARS the 5000ms condition the row originally named.

The row still does not dissolve, and the reason is that the bar moved the same day:
at the operator's 500ms per-witness warning threshold, re-merging a 1843ms witness
per-PR would sit 3.7x over the warning line and move the problem rather than close
it. The remaining residue is mostly the served-page render, not the projection --
different work from what #7822 did. Both the roster row and the witness header now
carry the new number, because a stale measurement inside a carrier whose only job is
to justify a deferral is the citation-rot class DESIGN section 3 names.

Verified: per-PR mechanism half PASS (147ms), long-lane live half PASS (1716-1843ms).
@briansrls
briansrls merged commit 4f91129 into main Aug 5, 2026
5 checks passed
@briansrls
briansrls deleted the session/loyal-bat-373-instrument branch August 5, 2026 18:25
gunbai-bot Bot pushed a commit that referenced this pull request Aug 5, 2026
The merge of main (#7824, #7790, #7844) into this branch collided at the
tail of falsifier_substrate_long_lane_rows — my seven C0(b1) census rows
and main's two new rows append at the same list position. Both sides are
kept; 39 rows, no duplicate (entry, function) pair, every entry file
present on disk.

The conflicted file was committed and pushed with markers intact by the
autocommit path before this resolution, so this commit is the repair of
that state, not a fresh merge.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls pushed a commit that referenced this pull request Aug 6, 2026
…1/b2 scope claims (#7821)

* WIP: cost analysis

* C0(b): v1 complexity capability census, typed and executed

Delivers deliverable (b) of the v2 complexity capability parity
program's C0 phase: one typed inventory row per capability that
src/v1/complexity.dag carries, each with a disposition from a closed
sum. Deliverables (a) the authority ruling and (c) the RatchetForever
re-classification are operator decisions and are deliberately absent.

Carrier: gunbc.v1_complexity_capability_census. Every arm carries
required non-empty payloads, so an unjustified disposition is
unwritable rather than lens-caught. Adds a sixth arm,
DispositionDeferred, because the five declared arms had no home for a
capability whose disposition is one of the note's own open questions;
forcing parser-progress into a neighbouring arm would have fabricated
a decision nobody made.

Witness: 15 checks green by execution, including two RED controls. Each
row's v1 symbol resolves against the live seed and each cited
destination symbol against the file its row names, so a stale citation
reds rather than reading plausibly.

Four findings, each executed rather than asserted:

1. C4 is smaller than the parity note's table implied. std.graph,
   std.termination, std.computation and std.induction already carry the
   SCC and descent vocabulary and v1 reaches it by import, while v2's
   lens modules import none of them — owed work is consumption, not
   migration. The v1-AST walkers that produce that vocabulary are the
   real C4 surface.
2. std.induction's CostBound/derive_bound vocabulary was missing from
   the do-not-re-mint list; added.
3. evict_summary overwrites an entry with a zero-cost Proven summary
   instead of removing it, so an evicted function reads as "costs
   nothing, proven" rather than "not computed". Rostered as a hazard
   that must not migrate with the capability.
4. cost_account_space_from_summary's note cites CostAccount.space with
   a Derived basis; it constructs no CostAccount, v1 does not import
   std.realization_schedule, and CostBasis has no Derived arm. Gives
   parity open question 3 a receipt.

Also corrects the sibling note's correction 1, which claimed no
valuation environment existed anywhere in the tree: the seed has one
(eval_cost_expr_concrete, env: Map<String, Int>), and it is
String-keyed. The narrower claim is the useful one — the seam is absent
from v2, and v1's key is the anemic identity parity §6 forbids carrying
across.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* WIP: cost analysis

* C0(b1): exact DeclarationRef citations, corrected disposition algebra

Reworks the census on operator review. The previous revision proved its
authored rows were well-formed and distinct; it did not prove its
citations resolved or that its dispositions stated the remaining work
honestly. Both are addressed, and the title is narrowed to what is
actually established.

Finding 1 — citations are exact, not substring. CitedSymbol { symbol,
file } is replaced by a typed DeclarationRef resolved through
v2.std.decl_ref_resolution. The file becomes an OBSERVED property of the
resolved declaration (rel_path) rather than a second authored identity.
The discriminating control: "Derived" appears verbatim in a seed note
string, so the old check found it; as a DeclarationRef it is not a
declaration and resolution refuses. Planted absent-declaration and
absent-module refusals accompany it.

Finding 2 — no closed denominator. Retitled C0(b1) "reviewed roster".
Declaration-to-capability totality is now an explicit C0(b2) slice that
derives the population from DeclFact. The 171/201 discrepancy is
resolved as a method identity: 171 counts top-level fn; 201 counts
fn+type+data+let (26 type, 4 data). Both correct; the method was
missing.

Finding 3 — disposition algebra. AvailableInSharedSubstrate projected as
discharged, understating C4; it is now IntegrationOwed with its own
work-state, because v2 must still consume std.graph et al.
DeliberatelyRetired belonged to no partition, so exhaustiveness was
green-by-vacancy; retirement now splits into RetirementOwed (replacement
has not executed) and Retired (discharged), and every arm — including
the two no row inhabits — carries a controlled fixture.
DispositionDeferred is removed per the parser-progress ruling.

Finding 4 — weak controls. Eviction is now proven by EXECUTION: cache a
summary with work 42, evict, look it up; the seed returns work 0, span
0, certainty Proven instead of Absent, while a never-cached function
correctly returns Absent. The constant-true finding uses the module's
own typed VacuousValidation carrier plus execution rather than
asserting the function exists.

Finding 5 — stale contract table: linearity_audit's WallAfterGrounding
boundary restored and complexity_lowering added with its distinct
SingleAuthority dissolution.

Operator rulings recorded: C0(a) signed (carried as the typed
CostAuthorityModule vocabulary, with the atomic-relocation nuance);
C0(c) split ruled as the next slice; parser progress split into
migration + retirement rows; WorkAtom closed-outer/open-identity shape;
CostBasis three-valued per resource axis; span stays in C2; C5 is two
changes never one; no blanket specialized-lens collapse.

Execution split stated rather than buried: exact resolution and the
eviction control need a decl_facts pool including src/v1, so they live
in the long lane and per-PR CI does not run them. The offline recipe is
named in gunbc.ci_layer_roots. Fast structural half: 10/10 green, max
2ms. Long lane: 9/9 green locally.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Move the vacuity control off the fast lane — measured closure cost

The floor red on this PR was not the two named witnesses being flaky.
Measured, same runner class: roadmap_program_view_witness_test
witness_live_constraint_present_iff_line_unaccepted ran 3901.9ms on
green main and 5019ms here, breaching the 5s budget without its own
semantic work changing.

Cause is mine. The fast-lane witness imported v2.lens.complexity,
v2.lens.cost and v2.std.refinement to execute the vacuity control, and
no other witness under dag/test/claim imports them — so this file was
the first to drag the v2 lens closure into the per-PR witness layer,
and every discovered entry paid for it.

Fix keeps ownership where it belongs: the control and its imports move
to the long-lane companion, which already pays a large closure. No
other lane's witness is relocated, and the long/ resident count does
not grow for anyone else's code.

Recorded as closure_cost_note rather than silently fixed: it is a
measured instance of this program's own subject — a per-witness cost
invisible until it lands on somebody else's budget, and a wall-clock
threshold that reports the victim rather than the cause.

Fast lane 9/9, long lane 10/10.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Enroll the orphan fixture helper (floor naming-hygiene refusal)

The floor refused at the pre-plan naming walk: all_disposition_fixtures
was a plain fn in a *_test.dag unreachable from any test fn — silent
de-enrollment, which the enroll-or-refuse hygiene rightly stops.

Fixed by making it load-bearing rather than deleting it. The new
w_fixture_set_covers_every_work_kind folds over all six arm fixtures
and asserts the set covers every one of the four work kinds, so an arm
added without a fixture now leaves a kind uncovered and reds. The
enumerated per-arm check states which arm maps where; this states the
fixture set is complete over the work-kind space.

Fast lane 10/10.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* WIP: cost analysis

* Split the v1-importing control out of the dag/ long lane (compile-clean)

Compile-clean refused with a precise diagnostic:

  dag/test/claim/long/v1_complexity_capability_census_resolution_test.dag:26:1:
  error: unresolved import: module 'v1.compiler.complexity' not found

The distinction the failure taught, now measured rather than assumed:
reaching v1 through decl_facts POOL ROOTS is fine for a dag/ entry —
pools are read independently of walk source roots — but IMPORTING a v1
module from a dag/ entry does not resolve under compile-clean's scope.

Only the executing eviction control needed the import. It moves to
src/v2/test/manual/v1_complexity_eviction_hazard_test.dag, beside the
existing v1-importing precedent (ownership_movable_test.dag imports
v1.compiler.ownership from that same directory). The resolution census
stays in the dag/ long lane and keeps resolving v1 DeclarationRefs
through pool roots, with no v1 import at all.

Verified in each file's real condition rather than a convenient one:
resolution census 7/7 with only dag + src/v2 as walk roots — exactly
compile-clean's condition, the one that failed; eviction control 3/3
with src/v1 added. Recipe rows updated for the split.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Remove the self-contradicting sentence from the long-lane exclusion row

review 48510: the WitnessExclusionRow reason said the resolution file
"carries the EXECUTING eviction control" and then, two sentences later,
that the control "does NOT live here" and was homed to
src/v2/test/manual/. Both were true at different points in this PR; only
the second is true now. The opening sentence survived the split I made
in the previous commit.

Operators read that row to run the local recipe, so a stale sentence
there misdocuments what the recipe covers — the same stale-prose class
this census exists to make decidable, committed in the row describing
the census. Removed rather than reworded: the correction already states
the fact completely.

Verified the row's --functions list matches the file exactly, 7 for 7.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* WIP: cost analysis

* Give every witness an executing consumer (admission-wall refusal)

The floor refused with WITNESS ADMISSION REFUSAL count=10
(10 UnclassifiedPathDeferral): enrolled witnesses excluded from
discovery that name zero executing consumers. As of 2026-08-04 a
directory is no longer an admission answer — moving a file under a
long/ or offline path removes it from per-PR discovery and executes it
NOWHERE.

This is the exact defect this census argues against, committed by the
census. I had said in prose that green CI proves nothing about these
rows unless the local recipe ran; the substrate now refuses to accept
that as an answer, and it is right to.

Two fixes, each verified under the cadence's real source roots rather
than a convenient set:

- The 7 resolution/vacuity witnesses get exact function-grain rows in
  gunbc.explicit_witness_admission on FalsifierSubstrateLongLane — the
  declared lane for SubstrateInputsOnly witnesses over the fast-lane
  budget. Verified 7/7 on dag + src/v2, the lane's roots.
- The 3 eviction witnesses move to src/v1/tests/claim/ and enroll on
  v1_claim_scoped_witness_entries, the only home with an executing
  consumer for a v1-importing witness (batch roots: dag + src/v1).
  Verified 3/3 on exactly those roots, without src/v2.

Both earlier homes were refuted by the floor, not by argument:
dag/test/claim/long/ failed compile-clean at the v1 import line, and
src/v2/test/manual/ compiled but was refused by this admission wall.

Also deletes the per-file OfflineLocalRecipe path row the exact
admissions supersede — precedence is total (a function with an exact
admission is decided by it), so keeping both would be the dual
representation that carrier exists to remove.

Fast 10/10, long 7/7, v1-scoped 3/3.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Regenerate artifacts after merging main

* WIP: cost analysis

* C0(b1) recut: split role/destination/producer axes; separate residues from capabilities; narrow the distinctness claim to validated

* Linearize the distinctness fold; record the wall-vs-cpu clock basis on the cost finding; regenerate

* Replace a tree-copied residue count with an identity join (DESIGN §5 oracle rule)

* Emit the stage0 artifact for the v1 eviction-hazard witness (self-host fixed-point)

* WIP: cost analysis

* Add the long-lane row separator comma (review 48680)

* Replace the unknown-size claim with the measured disjoint-range result

* Restore main's generated-artifact registrations dropped by the merge driver; re-derive the eviction row

* WIP: cost analysis

* WIP: cost analysis

* Correct the b2 trigger: capability discovery is closed by neither b1 nor b2

* Resolve ci_layer_roots long-lane conflict: keep both row sets

The merge of main (#7824, #7790, #7844) into this branch collided at the
tail of falsifier_substrate_long_lane_rows — my seven C0(b1) census rows
and main's two new rows append at the same list position. Both sides are
kept; 39 rows, no duplicate (entry, function) pair, every entry file
present on disk.

The conflicted file was committed and pushed with markers intact by the
autocommit path before this resolution, so this commit is the repair of
that state, not a fresh merge.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* WIP: cost analysis

* Regenerate ci.yml after the main merge; correct the ValueIdentity citation in parity section 6

The generated-artifact merge driver resolved .github/workflows/ci.yml to this
branch's stale side when main was merged, silently dropping #7856's
[ ! -f X ] -> ! [ -f X ] transposition at two floor-peak cgroup ascent sites.
That form was already present at the merge base, so this was a revert rather
than the branch being behind. Re-running the registered regeneration
(generated_artifact_gate main_wet) restores it; ci.yml now differs from main by
exactly the one AUTHORED_CONFLICTS entry this PR legitimately adds for its own
generated eviction-hazard test.

No rebuild was involved: the projection is interpreted from .dag at run time,
so the existing binary emits the current form. The drift was solely the merge
resolution never being followed by a regeneration.

Also corrects a section 6 citation the C1 lane caught. ValueIdentity was cited
as something the G1 cited-symbol work 'already makes resolvable'. It resolves
to no declaration anywhere in the corpus -- it exists only inside the sibling
note's proposed CostSubject / CostJustification code blocks. True of
DeclarationRef, false of ValueIdentity: the DESIGN section 3 cited-symbol
class, decidable by grep, sitting false in an authority doc while the mechanism
it described stayed correct. Edited in the carrier; the md is regenerated.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Resolve the main merge by hand: keep b2's landed work, restore this branch's three corrections

An autocommit committed conflict markers from the origin/main merge and pushed
them (64c0af2). This replaces that content with a real resolution; the merge
commit itself is kept, so no history rewrite and no force-push.

C0(b2) merged to main first, so main is authoritative for every shared carrier
and this branch is stale on all of them. Resolution was therefore per hunk, not
per side:

  v1_complexity_capability_census.dag - main wholesale, then re-apply the two
      note strings this branch corrected (c0_scope_note and
      complexity_capability_id_note: capability discovery is closed by NEITHER
      b1 nor b2). b2's algebra import, inventory_row_semantic_capability and
      concat rewrite are all kept.
  plans/v2_complexity_capability_parity.dag - main wholesale (it correctly
      records b2 DELIVERED ON MERGE and drops the now-closed C0(c) OPEN), then
      re-apply only the ValueIdentity citation correction.
  v1_complexity_capability_census_witness_test.dag - one differing line; this
      branch's measured disjoint-range cost result supersedes main's older
      its-actual-size-is-unknown wording.
  ci_layer_roots.dag - main wholesale. Verified by extracting (entry, function)
      pairs from both sides: the only rows this branch has that main lacks are
      the five direct_rust_door rows #7814 deliberately consolidated. Taking
      both sides would have duplicated seven b1 census rows that had already
      reached main through #7840.

Three files were also silently reverted and are restored to main. The merge
dropped #7865's std_unicode_types from the stage0 crate partition, and a
regeneration run reverted #7864's witness_report_line from claim_batch.rs plus
its instrument witness. claim_batch.rs is an emitted-code artifact whose
generation runs through the emit path baked into the binary, and this binary
predates #7864. Only the parity md needed regenerating, and that is an
interpreted projection, so it is correct.

Net diff against main is four files, five insertions, five deletions.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Drop the self-referential citation in c0_scope_note (review 49160)

c0_scope_note carried the parenthetical (see c0_scope_note) inside its own
declaration. It resolved to nothing a reader could follow: the citation names
the note containing it, and the capability-discovery explanation it points at
is already spelled out a few sentences later in the same string.

That is the DESIGN section 3 cited-symbol class -- a name-level claim a grep
decides -- landing in the one note whose subject is honest, resolvable scope.
The same PR fixes that class for ValueIdentity in the parity carrier, so
leaving it here would have been inconsistent on the exact point the note makes.

Dropped rather than repointed: the following sentences ARE the explanation, so
a forward reference would restate the structure the string already has, and a
positional pointer (see below) is the other half of what section 3 refuses.

Swept the other two carriers in this PR for the same shape -- a data note whose
body names its own declaration -- and found none.

---------

Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant