Skip to content

give the host-CLI absence its own type, so a variant stops standing in type position - #10055

Merged
gunbai-bot[bot] merged 2 commits into
mainfrom
session/still-swift-363-absence-type
Sep 3, 2026
Merged

gunbai-bot[bot] merged 2 commits into
mainfrom
session/still-swift-363-absence-type

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 2, 2026 •

Copy link
Copy Markdown
Contributor

first_absent_codex_wet_materialization_host_cli_dependency named HostCliDependencyAbsent — a variant — as its element type. The type system has no such thing, so the column widened to the parent coproduct HostCliDependencyObservation, and both package_delivery matches were correctly reported non-exhaustive for a sibling (HostCliDependencyPresent) that cannot occur at a "first ABSENT" site.

The repair is at the root, not at the two sites. HostCliDependencyAbsence is now a type of its own, the variant carries it, and the finder returns HostCliDependencyAbsence?. Both consumer matches become exhaustive with the arms they already have.

This is the same move as the Divergent marker in #9964: a state carried implicitly — there, divergence as an absent name; here, absence as a variant in type position — gets a carrier of its own.

The receipt is the arm count, not a green

The failure mode here would look exactly like success: the sites become exhaustive because someone added a Present { value: HostCliDependencyPresent } arm at a refusal site — fabricated plausible output (DESIGN §5) dressed as exhaustiveness. That arm would be a semantic answer to a real caller asking "which dependency is missing", at a site reached only when one is.

So the discriminator is the diff, and it does not depend on any build: both sites still carry exactly their two arms (Present, Absent), and git diff -U0 | grep -c '^+.*HostCliDependencyPresent' is 0.

Blast radius

4 .dag files. There are no Rust seed or src/v2 consumers (grep -rl HostCliDependency src/ is empty) — consistent with gunbc.witness_row_cost's own dissolution note, which records that the seed only unmarshals the wire string the witness already emitted. That note's prose citation of HostCliDependencyAbsent stays accurate: it is still a real variant.

What this evidence does and does not establish

Verified by execution: the corpus compiles with the change, measured beside a mutation control (absence.tool → absence.tolo) so the zero is readable rather than an instrument that said nothing.

NOT established here: that the nested-exhaustiveness checker on session/cool-ferret-679 stops refusing these two sites. That checker is not on this branch; cool-ferret-679 owns that half of the acceptance test.

Second commit: routing the two wet witnesses

The type change forces a pattern edit in host_cli_dependency_wet_witness_test.dag, and the changed-witness gate blocked the PR for it — correctly. Those two identities' cadence, BinWitnessWet, has had no executing route since falsifier.yml was deleted at 611fd02770 on 2026-08-15 (std.witness_admission witness_cadence_has_scheduled_route answers BinWitnessWet => false). A witness changed today must be routed today; an author may not authorize their own witness's permanent non-execution.

They are now admitted to LocalRepoWetLane, additively. The lane's existing membership property — effects confined to a tempdir and a local git repository — survives verbatim for its eleven existing members; that sentence is false about these two, so they carry their own authority (excl_local_repo_wet_host_probe_reason), admitted on the shared negative half (no network, no cargo, no remote host, no install media) with the read-only host PATH probe named as a distinct effect. A property widened to accommodate its newest member stops bounding anything.

The admission condition was host-independence, and it was measured

npm is provisioned by apt install npm on falsifier cadence runner image — the cadence whose workflow was deleted — so its presence cannot be assumed either way, and admitting a host-conditional verdict would import a nondeterministic red into a lane that has none.

  • Structural, total over hosts: every arm of both fns is the literal true; zero arms can return false.
  • Executed, one host / one binary / one variable, with a control proving sh resolved and npm did not: the npm fn ran with the probe found and with the probe at exit=127, returning the same verdict in each.
  • Limit, stated: the echo fn's absent branch was never reached (echo resolves in every PATH tested); its host-independence rests on the structural argument alone.

What these can still red on is route-unreachability — no shell at all raises TypeError: failed to execute 'sh' and reaches no verdict — which every member of this lane already carries. The roster row records it so a future red is read against the right axis rather than blamed on the probed tool.

Verified by execution, not by the green

[local-repo-wet] observe_echo_... expected=passed observed=passed
[local-repo-wet] observe_npm_...  expected=passed observed=passed
[changed-witness] both -> standing=hermetic-route-gap-held-and-wet-passed
required-floor: changed_witnesses=3 changed_witness_blocking=0   (was 2)
required-floor: verdict=FloorClean unexpected_failures=0

🤖 Generated with Claude Code

https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23

…n type position

first_absent_codex_wet_materialization_host_cli_dependency named
HostCliDependencyAbsent as its element type. The type system has no such
thing: a variant is not a type, so the column widened to the parent
coproduct HostCliDependencyObservation, and both package_delivery matches
were correctly reported non-exhaustive for a sibling
(HostCliDependencyPresent) that cannot occur at a "first ABSENT" site.

The repair is at the root, not at the two sites: HostCliDependencyAbsence
is now a type of its own, the variant carries it, and the finder returns
HostCliDependencyAbsence?. Both consumer matches are exhaustive with the
arms they ALREADY have.

The receipt is the arm count, not a green. The failure mode that would
look like success here is adding a `Present { value:
HostCliDependencyPresent }` arm at a refusal site -- fabricated plausible
output (DESIGN section 5) dressed as exhaustiveness. Both sites still
carry exactly their two arms, Present and Absent, and no
HostCliDependencyPresent arm was added anywhere in the diff.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
@gunbai-bot gunbai-bot Bot changed the title Repair the first() interpreter/emitted semantic divergence — census the 187 candidate sites, then derive both arms from one authority give the host-CLI absence its own type, so a variant stops standing in type position Sep 2, 2026
…easured admission

The changed-witness gate blocked #10055 correctly: the type repair forces a
pattern edit in two WET witnesses whose cadence, BinWitnessWet, has had no
executing route since falsifier.yml was deleted at 611fd02 on
2026-08-15. std.witness_admission witness_cadence_has_scheduled_route says
so directly. A witness changed today must be routed today; an author may
not authorize their own witness's permanent non-execution.

THE ADMISSION IS ADDITIVE, NOT A WIDENED SENTENCE. The lane's existing
membership property -- effects confined to a tempdir and a local git
repository -- survives verbatim for its eleven existing members. These two
are admitted on its NEGATIVE half (no network, no cargo, no remote host, no
install media) with their own effect stated distinctly: a read-only host
PATH probe, building no repository and writing nothing. A property widened
to accommodate its newest member stops bounding anything, so
excl_local_repo_wet_host_probe_reason is a separate authority rather than
an edit to excl_local_repo_wet_reason.

THE HOST-DEPENDENCE RISK WAS MEASURED, NOT ASSUMED. npm is provisioned by
`apt install npm on falsifier cadence runner image` -- the cadence whose
workflow was deleted -- so its presence on this lane's hosts cannot be
assumed either way. Admitting a host-conditional verdict would import a
nondeterministic red into a lane that has none. Both fns return the literal
true from every arm, and the npm fn was executed on one host in both
conditions: probe found, and probe exit=127 with sh still resolvable,
yielding the same verdict in each. The echo fn's absent branch was not
reached by execution and is recorded as such; its host-independence rests
on the all-arms-true structure, which is total over hosts rather than
sampled.

What these can still red on is route-unreachability -- no shell at all
raises TypeError and reaches no verdict -- which every member of this lane
already carries. The roster row says so, so a future red is read against
the right axis rather than blamed on the probed tool.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review September 2, 2026 13:42
@gunbai-bot

gunbai-bot Bot commented Sep 2, 2026

Copy link
Copy Markdown
Contributor Author

Independent verification of the second half of the acceptance criterion (cool-ferret-679, who owns the nested-pattern exhaustiveness checker this PR's sites were refused by).

Their checker, same binary and same command, varying only this PR's four first-commit .dag files:

CONTROL (without the fix)   EXIT=1   2 blocking, 629 advisory
  error[dag/gunbc/package_delivery.dag:2160:3]: non-exhaustive match:
    missing variant(s) Present { value: HostCliDependencyPresent }
  error[dag/gunbc/package_delivery.dag:2499:3]: non-exhaustive match:
    missing variant(s) Present { value: HostCliDependencyPresent }

SUBJECT (with the fix)      EXIT=0   0 blocking, 627 advisory, 177 files emitted

So the two sites stop being refused, and they stop because of this diff and nothing else — a revert arm, not a bystander control.

This is the half I could not run myself: the checker lives on their branch, not on main or here. Together with the arm-count receipt already in the PR body (2 arms at each site, zero HostCliDependencyPresent arms added anywhere in the diff), both directions of the acceptance criterion are now closed — the sites became exhaustive because the model was repaired at the root, not because an arm was fabricated at a refusal site.

Note for sequencing: this PR is still open, so HostCliDependencyAbsence does not exist on origin/main and the verification above ran against this branch at f69acb8, not against main.

— sent from still-swift-363

@gunbai-bot
gunbai-bot Bot merged commit 992fd44 into main Sep 3, 2026
6 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/still-swift-363-absence-type branch September 3, 2026 00:37
gunbai-bot Bot pushed a commit that referenced this pull request Sep 3, 2026
…o host-probe rows across the roster's shape migration

main's #10055 added two rows in the OLD shape (`LocalRepoWetScheduled`, a
qualified `identity` string, `expected: LocalRepoWetExpectPassed`) to the same
roster this branch migrates to `WetScheduledClaim` / `WitnessIdentity` /
`expectation`. The conflict is that shape change meeting new members, so the
resolution ports both rows into the new shape rather than choosing a side:
their authored module_path and function are preserved verbatim, since which
witnesses that lane admits is #10055's authority and not this branch's.

The membership prose auto-merged to THIRTEEN MEMBERS IN THREE GROUPS and the
roster now holds thirteen rows, so the count and its prose agree. No consumer
hardcodes the old count; the roster's identity/function agreement witness
covers the new rows unchanged.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
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.

0 participants