Skip to content

Declare the rung drop D13 cut (c) took on the Network requirement - #12175

Merged
briansrls merged 1 commit into
mainfrom
fierce-seal-607/network-demand-rung-drop
Sep 23, 2026
Merged

briansrls merged 1 commit into
mainfrom
fierce-seal-607/network-demand-rung-drop

Conversation

@gunbai-bot

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

Copy link
Copy Markdown
Contributor

D13 cut (c) (#11993) and its final-base census (#12125) deleted an authored uses row whenever the function's derived service demand was nonempty. They never checked that the derived set covers each resource the row named.

  • Covered by name: a direct resource operation surfaces in ItemInfo.service_names under the resource's own name. Filesystem, Clock and Urandom all appear in the census data.
  • Not covered: Network never appears. Only the services a Network effect reaches do (ssh.Session, http.Client, redfish.Http, ...).

So every deleted net: Network identity lost its Network requirement with no derived stand-in. That is a silent rung loss on main. smart-tern-891 found it while modeling #12047; I confirmed it against the census data, and snappy-deer-443 ruled it a loss that must be declared.

The declaration

gunbc.rung_drop.network_requirement_unrepresented_after_uses_cut, enrolled in gunbc.rung_drop.roster, projected into docs/design-rung-drops.md:

I chose a declared drop over restoring the clauses. Restored rows would put a second authority back beside the derived carrier, and the capability that closes the loss is derivation. Building that carrier is EFFECTS-1's, and it is currently unowned. #12047 has been reduced to the emit-time refusal; its typecheck wall returns later as a consumer of the carrier.

🤖 Generated with Claude Code

Cut (c) (#11993) and its final-base census (#12125) deleted an authored uses row
when derived demand was NONEMPTY. They did not check that the derived set covers
each resource the row named. A direct resource operation surfaces in
service_names under the resource's name (Filesystem, Clock, Urandom), but Network
never does: only the services it reaches appear. So the Network requirement of
every deleted net: Network identity is represented nowhere. Population:
312 identities / 82 modules in the #11993 diff and 165 / 31 in #12125's.

DESIGN 4b(3): declared rather than silent. previous MechanicallyPreventable,
temporary Mitigatable, LostAsPassenger on the deleted rows. The restoration
trigger names the capability: DependencyDemand derives each resource requirement
keyed on the resource declaration's identity, established by a census over the
deleted identities. Restoring authored rows, or adding Network to service_names
by spelling, does not discharge it. Found by smart-tern-891 (#12047), confirmed
against the census data, ruled a silent loss by snappy-deer-443.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls added this pull request to the merge queue Sep 23, 2026
Merged via the queue into main with commit 3b0c61b Sep 23, 2026
5 checks passed
@briansrls
briansrls deleted the fierce-seal-607/network-demand-rung-drop branch September 23, 2026 21:39
@briansrls
briansrls restored the fierce-seal-607/network-demand-rung-drop branch September 24, 2026 00:20
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