Model the ntfy notification principal and the human steps it actually costs

[gunbai-bot]

Toward the operator's stated goal: a real approval notification on the phone. This lands the principal the notification server runs as, and the enrollment steps a person must take, as typed facts.

What is here

gunbc.fleet_posix_accounts gains FleetAccountNotificationService — no-login service identity, persistent realization, and an empty sudo grant set declared by construction. The emptiness is the security claim: this principal runs the process that handles approval links, and an approval link is spendable, so any grant would let it act on what it delivers. Declared empty so a future grant is a visible edit rather than a roster append.

Persistent rather than a supervisor-managed dynamic identity for its own reason, not by copying the publication helper: the server owns a state directory across restarts (message database, subscriber read position), and a dynamic uid would not own yesterday's files.

gunbc.auth.approval_ntfy_deployment carries the deployment shape and six std.human_intervention rows — priced by frequency rather than summed, so one-time enrollment is not billed like per-run work.

step	frequency	why a person
system account	FleetOnce	temporary — argv is modeled, no member renders it yet
server binary + unit	FleetOnce	temporary — this repo does not package third-party binaries
publisher token	FleetOnce	does not exist until a person creates it
topic access policy	FleetOnce	ntfy defaults to read-write; a readable topic is a spendable approval
iPhone subscription	DeviceOnce	replacement phone pays it again
relay withdrawal	BreakGlassOnly	deliberate loss of delivery, not a tweak

Two things worth reviewing closely

Declaring a principal is not creating an account. An earlier revision of this module asserted that account creation was already converged because EnsureSystemAccount exists. It does — but it is rendered only by the live_deploy member that creates gunbc-publication, and nothing renders one for this principal. The module now says so, with a dissolution trigger, rather than implying coverage it does not have.

The loopback bind is asserted, not commented. 127.0.0.1 is what makes tailscale serve the sole route, and the sole route is what makes the injected Tailscale-User-Login header on the neighbouring approval route trustworthy. A 0.0.0.0 bind would let anything on the host reach the backend and forge that header — so it is a witness, not prose.

Evidence

7 witnesses, executing (claim_batch), plus 13/13 on posix_principal_allocation_witness_test after the enum widened.

The four frequency counts control each other: the roster holds 6 rows, so a counter ignoring its frequency argument would answer 6 to all four and fail three, and one stuck at zero would fail the other three. Only genuine partitioning satisfies 4 + 1 + 1 + 0 — which is what keeps witness_no_per_run_human_cost from passing vacuously.

The break-glass-is-not-routine property is deliberately not restated here; it belongs to std.human_intervention's comparison function and is tested there (§2 — the same check in two places is one authority forked).

Not here

The unit itself. Unit emission lives in live_deploy, which is scheduled for deletion with no declared cut, so this does not grow it — the two affected steps are declared temporary with triggers instead. Answering the live_deploy → fleet-convergence question is a separate piece of work.

🤖 Generated with Claude Code

https://claude.ai/code/session_01UBLsJSnmB8ZdDTh1RRVTe7

[gunbai-bot]

Both findings from review 61608 verified and fixed in d9392eef691.

F1 — the prose row. Correct, and it was the clearer §4c case of the two: an ordinary String whose sole purpose was commentary, duplicating the // block three lines above it. Deleted. The security argument now also reaches the operator through the install instruction itself, where they can act on it rather than only read it.

F2 — the dangling config values. The diagnosis was sharper than the remedy I'd have reached for. The declarations were not merely unconsumed; their values were retyped as English in the instruction string, so the only spelling anyone would ever act on was the prose one. Deleting the rows would have resolved §3c by conceding the fork.

So the instruction is now derived from them:

instruction: join([
  "Install the ntfy server on srv1 and run it as ", approval_ntfy_principal_name as String,
  " under a systemd unit named ", approval_ntfy_unit_name as String,
  ", configured at ", approval_ntfy_config_path as String,
  " with listen-http set to ", approval_ntfy_endpoint(),
  ...

The operator reads values the model owns, and a drift between declaration and instruction is a red witness instead of an invisible disagreement. notification_service_realization_standing gains the witness its sibling already had, naming its own principal so a copy-paste of the publication helper's row goes red.

Witnesses 7 → 12, all executing. Two new ones carry a positive control — the instruction must not contain 0.0.0.0:2586 — so string_contains is shown able to answer false rather than passing over any string.

One incidental catch worth recording: to_string over the branded Port had only ever been resolved, never evaluated. Casting into a brand is precisely where this corpus compiles clean and fails at evaluation, and the dangling declaration was hiding that. It passes, and now something runs it.

— sent from crisp-ram-671

[gunbai-bot]

Both findings from review 61619 fixed in 38107b40e8e, plus the CI cause and a defect the review indirectly surfaced.

F1 — misplaced annotation. Correct. Inserting the new function between the publication helper's leading block and its declaration left an operator ruling annotating the wrong symbol. Moved below; each block leads its own declaration.

F2 — the unused topic import. Correct, and it was the same fork the module's own annotation claims to have fixed for the port and state root — I fixed that pair and left this one. The topic is now joined into the grant instruction with two witnesses. It matters more than the endpoint did: on a default ntfy deployment the topic name is the access control, so an operator granting read on a different topic than the broker publishes to leaves the real one at read-write — silently, and in the direction that makes approval links public.

CI

FloorDiscoveryRefused — floor discovery enrolls test fn, my witnesses were plain fn, so the entry contributed zero. My local loop ran them by name through --functions, which never needed the keyword. All 14 now carry it and pass.

The measured defect

Worth flagging separately because it is not a modeling nit. I ran a wet probe of the modeled publish path against ntfy.sh. It reached the network — [rest] POST https://ntfy.sh/<topic> — and a junk bearer came back as:

TypeError { msg: "HTTP 401: {\"code\":40101,...}" }

An untyped throw where the model promised a typed refusal. extdeps.transports.rest raises on any status ≥ 400 unless the operation opts in to outcome: RestOutcome, and PublishMessage never did — so NtfyPublishRefused had no constructor on any real path and the response { 401 => … 5xx => … } block was decoration. That is §4b rung inflation in miniature: the model described a refusal arm the realization could not produce.

The field is now declared, and ntfy_publish_outcome_of is the single route from a transport observation to the outcome type.

Per merry-ibex-741 (upsert saga)

Dissolution triggers now name capabilities, not contributing artifacts: the account row retires only when convergence creates and verifies by readback, and the server row states plainly that it is two capabilities (verified binary AND converged unit) — a binary alone leaves a host that looks provisioned and serves nothing. Acquisition facts are recorded as an obligation rather than invented: no release tag chosen, no artifact hashed, so a version row would be a guess and a digest row would read as verification that never happened.

— sent from crisp-ram-671

[gunbai-bot]

Both findings from review 61651 addressed in 047a7fa3d21, and the first one led somewhere better than the remedies on offer.

F1 — the layer inversion

The finding is right, and I'd landed it knowing it was wrong, which is exactly what §5 says a dissolve-on: does not license. But both suggested landing states — a rostered §4b(3) drop, or an operator-approved scaffold — admit the debt, and re-reading §3 there's a way not to incur it:

the transport (shell, REST, SDK) is a §2 Realization handler bound to that shape, one of N, never a fact about the dependency

The endpoint wasn't the misplaced thing. The whole service block was. extdeps.ntfy now owns what ntfy is — message shape, priority and cache vocabularies, the outcome type, the two access-control facts a consumer must not get wrong. The REST binding and the address live in gunbc.auth.approval_ntfy_deployment, with the deployment they belong to. Five services already live under dag/gunbc, so this is the existing shape rather than a new one.

That also fixes the narrowing the review named: a second deployment is now a second binding beside this one, and extdeps.ntfy doesn't change. No drop rostered because there is no longer debt to roster.

F2 — the oracle

Correct, and witness_upstream_relay_is_declared was the plain case: approval_ntfy_upstream_base_url == "https://ntfy.sh" is measure() == measure(). The 4/1/1/6 counts were measurements of a roster authored three files away in the same PR — a legitimate seventh step would have reddened a test whose subject isn't the number of steps.

Replaced with properties that survive roster growth:

• every identity occurs exactly once, with a positive control proving the predicate can fail. This is also the check that catches a copy-pasted row — which no count can see, since duplicating one and dropping another keeps every count equal
• every row carries a non-empty instruction and subject

Two literals kept and justified rather than deleted, both grounded outside the tree as §5 permits: EveryProvision == 0 is a design claim (the loop must cost a person nothing per run), and the loopback address is an explicit policy requirement.

Measured, not asserted

The server is live on srv1 and the loop is closed end-to-end — a notification from the modeled path reached the operator's phone. Under real use the access split held: the phone's own publish attempt was refused error_code=40301 while its reads succeeded, and every actual publish was gunbc-broker, none by the operator account.

After the service move, the modeled path still publishes: NtfyPublished { message_id: znjShbquiXow }.

CI

The red on dc298b3 is inherited from main — 7 CITED-DECLARATION-ABSENT findings in src/v2/lens/* and src/v2/test/claim/..., a byte-identical roster to main's own failing witnesses run. I touch none of those files.

— sent from crisp-ram-671

[gunbai-bot]

Both findings from review 61668 fixed in cdbee1d270e.

F1 — RestOutcome unbound. Correct, and it is a floor issue rather than a style one. The type resolved only because extdeps.ntfy.ntfy — which this module does import — pulls it in for the outcome fold. That is exactly the accidental-coverage shape secret_manager already records: a reference that holds because something else in the closure dragged the definer in is not a binding, and it breaks the moment that fold or import moves.

Worth naming the provenance: I created this defect in the previous commit. Moving the service to the realization layer left the fold — and its import — behind in extdeps.ntfy. I checked that the module compiled rather than that it named what it uses, and a whole-corpus compile cannot tell those apart. Imported where used now.

F2 — the transcribed port. Also correct. == "127.0.0.1:2586" copied 2586 out of a data row three files away, so automating that literal collapses the check to measure() == measure() for the port half — the same tell that removed the upstream-URL and roster-count witnesses from this file two commits ago. I fixed the pattern there and reintroduced it here.

It now asserts the relation: the endpoint must be built from the declared listen address, which witness_server_binds_loopback_only separately holds to loopback as an explicit policy requirement. Neither witness restates the other's literal; changing the port freely is correct and reddens nothing; widening the address still goes red. A positive control pins that the prefix check can answer false.

13 witnesses in that file, all executing and passing.

CI: the 2 failing checks on 047a7fa are inherited from main — the same 7 CITED-DECLARATION-ABSENT findings in src/v2/lens/* and src/v2/test/claim/…, identity-matched against main's own failing witnesses run rather than counted. None of those files are touched here, and no red in that run names any module in this PR.

— sent from crisp-ram-671

[gunbai-bot]

Both findings from review 61680 addressed in d08d7b576e5.

F1 — the re-minted address

Correct, and the sharper half of the finding is that moving the binding out of extdeps fixed the layer and left the duplication. "https://srv1.tailecbe08.ts.net:8443" was one literal re-minting two facts the corpus owns — fleet_intent_network.tailnet_domain and operator_host_srv1. Now joined from both.

tailnet_domain is Optional and endpoint cannot carry one, so the Absent arm must answer something. It answers a host in the RFC 2606 .invalid TLD — guaranteed never to resolve. That is a structural failure rather than an absorbing fallback: it cannot succeed, cannot widen, and cannot be mistaken for a working endpoint. Both arms witnessed, with a positive control that the Present path does not produce the marker.

The second half of that finding is the one I'm most glad was caught. The annotation claimed "Both are declared, and witnesses hold them to their separate jobs" while no witness touched approval_ntfy_base_url at all. That is a citation wall in miniature — the symbols resolved, the quantified claim about them was simply false, and I wrote it. Four witnesses now make it true, as identity joins against the network model rather than transcriptions.

Because a derivation that changes the address would break the deployment silently, I checked it against the running server rather than by reading: the joined URL publishes to the live self-hosted ntfy at exactly https://srv1.tailecbe08.ts.net:8443/ — NtfyPublished { message_id: 8JLDpfuLw8D2 }.

F2 — no production consumer

True. PublishMessage, the RestOutcome opt-in, ntfy_publish_outcome_of and approval_ntfy_human_burden have no production caller, and §3c's middle state applies: a declared frontier, admissible only with its trigger stated. The module now states it at module scope so nobody has to grep:

• exercised today — a wet probe against the live server, plus every fold arm and intervention property under witnesses. That is execution, but a witness is not a production consumer and the note does not pretend otherwise
• named consumer — the broker publishing a notification for a pending AccessRequest
• trigger — the minting path (an AccessRequest from a real refusal, its capability signed) and ApprovalDecideHandler redeeming it rather than answering 501, which is what it does today
• disposition if it never lands — delete this binding. It is not infrastructure worth keeping for its own sake; with no requests it carries nothing

I considered wiring an intermediate caller to clear the finding, and didn't: it would move the danglingness up one level rather than remove it.

17 witnesses in the deployment file, 6 in the outcome file, all executing.

CI: still the inherited main breakage — 7 CITED-DECLARATION-ABSENT findings in src/v2/lens/* and src/v2/test/claim/…, identity-matched against main's own failing run. No red names any module in this PR, and this branch cannot go green until main does.

— sent from crisp-ram-671

[gunbai-bot]

All three findings from review 61738 fixed in f742b490211. Two of them catch overclaims I made in a commit message, not just in code, which is worth saying plainly.

F2 — the fabricated member (the sharpest)

NtfyUnitInstalled => [SystemdDaemonReload] named an obligation its projection did not discharge. It installs nothing. enable and start converged only because I had already placed the unit file by hand — so on this host the difference was invisible, and a fresh-host apply would have failed at exactly the step the member claimed to cover.

That makes my own commit message — "srv1's state is now rendered by the model" — false. It is rendered for the account, ownership, permissions and unit state; it is not rendered for the unit file, the config file, or the binary.

The member is renamed for what it does, the unused InstallFile import is gone, and the module now states the boundary rather than implying coverage: this roster cannot converge a fresh host. Those three members are absent from it, because file content is unmodeled and InstallFile needs a source that must already exist. Absent is honest; an adjacent member standing in for them is not.

F1 — two answers in one PR, and a false annotation

The account intervention still said "no converged member renders it for this principal yet" after the family landed. And the deeper half: the intervention rendered through executor_privileged_operation_shell_command while the member used executor_privileged_operation_converge_command — so the annotation claiming they were "one authority by construction" was false, and the operator's copy-paste would have exited 9 on a host that already had the account.

Both now call the converge renderer, and a witness holds them equal. That matters more than the fix: a prose claim is precisely what failed to catch this — the second time in this PR an annotation asserted coverage that no executing check provided.

F3 — the fabricated status

RestTransportRefused → NtfyPublishRefused { status: 0 } reintroduced one layer up the exact fabrication extdeps.transports.rest exists to prevent — its own annotation says "no response arrived, so no status can be fabricated". It also collapsed two states with different remedies: the server refused this publish vs no server was reached.

NtfyPublishUnreached is now its own arm carrying a cause and no status, witnessed both directions so neither collapses into the other.

Widening that coproduct made the exhaustiveness wall name every consumer — the floor doing its job on a change that would otherwise have been silent.

33 witnesses across the three files, all executing and passing.

CI: unchanged and not from this branch — the same 7 CITED-DECLARATION-ABSENT findings in src/v2/lens/*, identity-matched against main's own failing run.

— sent from crisp-ram-671

[gunbai-bot]

All four findings from review 61755 fixed in 62ace60c0af. (The dashboard notification truncated the third; I pulled the full artifact.)

F1 — the undecodable arm. Correct, and the uncomfortable part is that I wrote this collapse while splitting the transport arm one line above for exactly the same reason. A 200 whose body did not decode became "refused with status 200" — the server accepted, we failed to read the reply, and the remedies diverge completely. NtfyPublishUndecodable is its own arm now, keeping the status it really received, with a witness pinning all three failure outcomes mutually distinct.

F2 — re-minted paths. Correct, and the same nicknaming this PR removed from the base URL two commits earlier, in a file that already had the authorities in scope. The config directory is now the authority and the file path derives from it — a dirname would be a second computation over one fact — and the attachments dir joins the state root.

F3 — hand-spelled shell. Correct. The check is now a typed OperationPrecondition rendered as an argv through the same quoting authority as the operation it guards.

The group arm is deleted rather than modeled: usermod -aG appending a group the user already has exits 0 — measured on srv1, twice. So its id -nG | tr | grep -qx pipeline was a smuggled program solving a problem that does not exist, and removing it is strictly better than rendering it through grammar rows. What remains is one redirection and one ||, named as residue with a dissolution trigger pointing at the If-Not-ExitZero orchestration intent live_deploy already carries — so consolidating it later is one deletion, not a census.

F4 — the bare optional. The sharpest of the four, and thank you for chasing it to the cause: ntfy_member_ownership returned a bare Ensured where the type is Ownership?, and my witness greened only because the interpreter's raw-optional representation lets Present { value: o } match any non-null. A green for the wrong reason, in a witness I wrote specifically to prove that property. Now Present { value: Ensured }.

Consequences worth flagging

Quoting the guard changes live_deploy's emitted bytes. Its witness pinned the unquoted spelling, so it now asserts the guard's shape rather than its quoting — and two of my own witnesses needed the identical correction, having pinned the same stale form. All 59 live_deploy emit witnesses pass.

Re-verified on srv1 after the paths became derived and the quoting changed, because either could have silently altered what gets applied: the 7 rendered commands apply with 0 failures on both passes, service active, endpoint 200.

CI remains blocked by main's 7 inherited CITED-DECLARATION-ABSENT findings, identity-matched to main's own failing run — checks: pending and github_admissible: blocked both trace to that, not to this branch.

— sent from crisp-ram-671

[gunbai-bot]

Both findings from review 61791 fixed in 9cf7a56fef0.

F1 — three dangling declarations. Correct: ntfy_member_key_eq, ntfy_member_value_eq and approval_ntfy_member_argv had no consumer. I wrote them anticipating a membership_reconcile call I never made, and gave them none of the declared-frontier statement I'd carefully written for the publish binding one module over. Deleted.

The corroboration is the part worth keeping, and I've recorded it in the module rather than letting the functions disappear quietly: ntfy_member_value_eq compared members by key alone, so a NtfyStateDirectory and a NtfyConfigDirectory sharing a path compared equal — a wrong equality that would have silently collapsed two members in the very reconcile it existed for. Nothing caught it because nothing ran it. That is §3c's argument in a single artifact: unconsumed code is not idle, it is unexamined, and it quietly accrues defects that only surface when someone wires it up.

F2 — the false annotation. Correct, and the mechanism is worth naming: "The emitted bytes are unchanged" was true when written, and became false two commits later when the precondition started rendering through posix_single_quote. I changed the behaviour and didn't revisit the sentence — and the same diff contains the witness update that contradicts it.

It now says what actually happens (the login arrives single-quoted; equivalent shell; one fewer place deciding quoting) and cites what is actually verified: all 59 live_deploy emit witnesses pass — not byte identity, because the bytes are not identical.

That is the third annotation in this PR to claim something no executing check supported. The first two were caught by review; this one was caught by reading the diff against itself. The pattern is consistent enough to be worth stating plainly: prose I write about machine behaviour goes stale exactly when I change the behaviour, and nothing in the toolchain notices. Where a claim is checkable I've been converting it to a witness (the intervention/converge command equality is now one); where it isn't, it should describe intent rather than assert a result.

10 converge witnesses and 59 live_deploy emit witnesses pass.

Merge state unchanged and still not close: 0 approvals on this head, 1 open request-changes, merge_state_status: BLOCKED, checks pending on main's 7 inherited CITED-DECLARATION-ABSENT findings.

— sent from crisp-ram-671

[gunbai-bot]

Fixed in 0ebab71b714. This one lands harder than the previous rounds, so I'll be direct about it.

ntfy_member_ownership ignored its parameter and answered Present { value: Ensured } for every input. So witness_no_member_is_owned was permanently green by construction — no member could be Owned, and its failing arm was unreachable. §4b names precisely this:

the check is not a weak wall but a decoration — permanently green by construction, carrying no information, and worse than absent because it will be cited as coverage

It was cited as coverage. By me, in the annotation directly above it, for the claim that a retract cannot destroy pending-request history. That safety claim rested on a check that could not fail. I wrote the function, wrote the witness, and then wrote the prose citing the witness as the thing that made the guarantee real.

Both deleted. The constraint is real and is now stated as what it actually is: a requirement on a reconcile that does not exist yet, to be held at rung 4 — Owned unrepresentable for this family by construction, at which point no check is needed at all. Declaring an Optional that is never Absent would be a third representation of a decision nobody makes.

Second half of the finding, also correct: the heading "THE KEY IS CONSUMED" overstated things — ntfy_member_key's only consumers are two witnesses, not production. Rather than patch that one sentence, the module now carries a §3c frontier statement at module scope for the whole family: the named consumer (a member family in fleet_converge_plan reconciling this desired set against an observation, discharged through ConvergedEffect), its trigger, and what already executes — the rendered commands converge srv1 idempotently, 7 commands, 0 failures across two consecutive passes.

The desired side is real and runs. The observed side does not exist. The module now says that once, instead of implying coverage in three separate places.

9 witnesses, all executing, none green-by-construction as far as I can now tell — though that is exactly the claim this round proves I am bad at self-assessing.

Merge state: 0 approvals on this head, 1 open request-changes, BLOCKED, checks pending on main's 7 inherited findings. Not close, and the CI half is not this branch's to fix.

— sent from crisp-ram-671

[gunbai-bot]

Status: review floor met, blocked entirely on main

CI settled on 0ebab71b714:

check	result
required-witnesses-build	pass
heal-generated-artifacts	pass
required-witnesses-floor	fail — 7 findings, all inherited
witnesses (aggregate)	fail (reads the floor lane)

The 7 CITED-DECLARATION-ABSENT findings are byte-identical to main's own most recent completed witnesses run (5ee9cab5f, run 34085447859) — identity-matched, not merely equal in count. This branch touches none of those files and contributes no new finding.

The cause, since it is not a typo

#10706 "OutsideModeledGuarantee stamps and stall carriers (follow-up)" merged at 02:12 today. main's witnesses lane has been red on every completed run since.

src/v2/lens/grounding.dag:21 states the intent plainly:

The name-only should-ground residual is off the ladder until a confirm-judge capability is authored — then this stamp reds. confirm_judge_should_ground is deliberately not a decl.

The stamp exists to name a capability that does not exist, and expects to red when it is authored. The citation wall reds because it is absent. The two mechanisms have opposite polarity, so the repair is a modeling decision — the carrier needs a way to express "this required capability is deliberately unauthored" without a dangling DeclarationRef — in src/v2/lens/* and construction_justification, which DESIGN names load-bearing.

Why I have not fixed it here

At least two open PRs are working the same carrier right now — #10704 ("Restore wet_route_model_lags_seed_stall so two 4b triggers have a referent", the same shape as this defect) and #10747, with #10725 and #10755 nearby. Making the citations resolve could mean the opposite of what the stamps intend, and that is the authoring lane's call. Landing a competing fix from here would collide with work already in flight.

This PR

Review floor is met: 1 distinct approval (review 61821), no REQUEST_CHANGES, no active reviews on this head. mergeable: MERGEABLE, mergeStateStatus: BLOCKED — and the block resolves entirely to the floor lane above.

Awaiting the operator's call on whether to wait for the neighbouring PRs, land over a red floor main already carries, or coordinate a fix. Not merging from here either way.

— sent from crisp-ram-671