Skip to content

required-regen: discriminating REDs for the drift arms, which had none - #8603

Merged
briansrls merged 1 commit into
mainfrom
regen/drift-arm-controls
Aug 20, 2026
Merged

briansrls merged 1 commit into
mainfrom
regen/drift-arm-controls

Conversation

@gunbai-bot

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

Copy link
Copy Markdown
Contributor

Owned by session stern-tern-636 (opened from a non-session branch).

The headline: the existing control establishes nothing

The required-regen admission wall (v2.workflow.required_regen required_regen_sync_admission) already had a witness over its drift arms' neighbourhood. Mutating the wall and observing that witness:

wall mutation pre-existing witness this PR's witness
none (clean) true true
surface_is_drift: SurfaceDrifted => false true false
hand_is_unverifiable: HandUnverifiable => false true false
HandDrifted made to over-refuse (predicate and collector) true false

The pre-existing witness returns true under every mutation, including one that disables the entire SurfaceDrifted refusal arm outright. That is not a weak control; it is a control that establishes nothing, and it sat in the tree looking like coverage. This PR's witness goes false on three.

Measured, not inferred: executed with a gunbc built from main's own stage0 (c4642e0a8ae), against main's corpus.

Summary

The wall had discriminating REDs for its population arms only — zero planned, zero executed, planned/executed mismatch, plus one matching positive control. Its drift arms had none.

GeneratedDrift and HandUnverifiableRefused are the two refusals that exist precisely to catch a committed surface disagreeing with the emitter. Nothing established that they fire. This PR adds four controls so they do.

Claiming exactly what this establishes and no more: the drift arms now have discriminating REDs and a positive control, where before they had none. This does not claim the wall would have caught any particular historical staleness — the wall's subject may not even cover the deferred-regen case, and that has not been shown.

The four controls

  • witness_drifted_surface_refuses_naming_the_path — a SurfaceDrifted row refuses and the refusal names the drifted path, while a matching sibling is asserted absent from the named set. That second half turns "refused" into "refused for the right reason", which is the difference between a control and a smoke test.
  • witness_surface_population_asymmetry_refuses — an EmittedNotCommitted/CommittedNotEmitted pair refuses with both paths named.
  • witness_hand_unverifiable_refuses_naming_the_entry — a HandUnverifiable row refuses naming both filename and reason.
  • witness_hand_drift_alone_admits — the near-miss positive control. HandDrifted is one variant away from HandUnverifiable and must not refuse, since hand-maintained drift is expected on a clean tree. Without it the three REDs would prove only that the wall refuses something drift-shaped; they would not establish which distinction it draws.

One mutation reported as not discriminating

Flipping hand_is_unverifiable's HandDrifted arm alone is an equivalent mutant rather than a miss: collect_hand_unverifiable's HandDrifted arm returns the accumulator unchanged and neutralizes it. Both halves must be mutated together for the over-refusal to exist at all.

Noted rather than swept up: the variant classification is expressed twice across that predicate/collector pair, which is why a one-sided mutation cannot be seen — a §3 duplication whose consequence is an unobservable arm. Not changed here; it is not this PR's subject.

Execution on CI

These execute on CI as things stand. CI builds main's committed stage0 mirror, which resolves main's corpus — that is the binary this receipt used. They stop executing on the day the mirror is repaired, at which point corpus resolve currently fails for an unrelated reason: 46 reported / 72 constructed expected 'Product(NonEmptyStr)', got 'Primitive(String)' errors, latent in main today, invisible to main's mirror, reproduced on a clean main worktree under a non-stale binary.

That population has since been located and counted — one class, dominated by 51 sites in src/v2/std/node.dag passing bare symbol literals into content_hash_atom(value: NonEmptyStr), with no coercion path from String into the refinement at the call boundary. It is routed as its own lane and is not this PR's subject. One warning for whoever picks it up, because it is the most likely wrong fix and would look like a two-character cleanup: it should not be fixed by widening content_hash_atom's parameter to String, because that dissolves the refinement to silence the wall — the fail-open in the costume of maintenance.

— sent from stern-tern-636

The admission wall's population arms (zero planned, zero executed,
planned/executed mismatch) each had a control. Its DRIFT arms did not:
GeneratedDrift and HandUnverifiableRefused -- the two refusals that exist
precisely to catch a committed surface disagreeing with the emitter -- were
untested, so nothing established that they fire.

Adds four controls:
  - a SurfaceDrifted row refuses AND names the drifted path, asserting a
    matching sibling ABSENT from the named set, so the refusal is
    attributable rather than merely present
  - an EmittedNotCommitted/CommittedNotEmitted pair refuses naming both
  - a HandUnverifiable row refuses naming both filename and reason
  - the near-miss positive control: HandDrifted ALONE still ADMITS, since
    hand-maintained drift is expected on a clean tree

The admitting case is what gives the refusing cases meaning: a wall that
refused everything drift-shaped would satisfy all three REDs identically.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DY4WxMYnZKvxCpWTTwjaDy
@briansrls
briansrls merged commit 25cec73 into main Aug 20, 2026
1 check passed
@briansrls
briansrls deleted the regen/drift-arm-controls branch August 20, 2026 01:29
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