Repository navigation
human in the loop - #10761
human in the loop#10761gunbai-bot[bot] wants to merge 13 commits into
Conversation
… costs The approval loop's notification transport needs a place to run and a person to enroll a phone in it. This lands both as typed facts rather than a runbook. gunbc.fleet_posix_accounts gains FleetAccountNotificationService: no-login service identity, persistent realization (the server owns a state directory across restarts, so a supervisor-managed dynamic uid would not own yesterday's files), and an EMPTY sudo grant set declared by construction. The emptiness is the point: this principal runs the process that HANDLES approval links, and an approval link is spendable, so a grant would let it act on what it delivers. gunbc.auth.approval_ntfy_deployment carries the deployment's shape and, as std.human_intervention rows, the six steps a person must take -- priced by frequency rather than summed, so a one-time enrollment is not billed like per-run work. Two of them are declared TEMPORARY with dissolution triggers: the account and the unit are human steps only because no converged member renders them for this principal yet. Declaring a principal in the fleet roster is not creating an account, and the module says so instead of implying the convergence already covers it. The loopback bind is asserted, not commented. It is what makes tailscale serve the sole route, and the sole route is what makes the injected tailnet identity on the neighbouring approval route trustworthy; a 0.0.0.0 bind would let anything on the host forge that header. Witnesses (7, executing): the roster costs nothing per run, and the four frequency counts control each other -- a counter ignoring its argument would answer 6 to all four, one stuck at zero would fail the other three, so the zero is load-bearing rather than vacuous. The break-glass-is-not-routine property is left where it lives, in std.human_intervention, rather than restated here over our roster. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UBLsJSnmB8ZdDTh1RRVTe7
…consumer Both findings verified and fixed. F1 -- loopback_bind_is_the_boundary_note was an ordinary String row whose sole purpose was commentary, which DESIGN §4c names as misplaced data, and it duplicated the `//` block three lines above it. Deleted; the annotation carries the rationale, and the security argument now also reaches the operator through the install instruction, where it can act on it. F2 -- the config declarations were dangling (§3c) AND their values were retyped as English inside the instruction string, so the only spelling anyone acted on was the prose one. Rather than delete them, the instruction is now DERIVED from them by join: the operator reads values the model owns, and drift is a red witness rather than 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. The review's diagnosis was sharper than deleting the rows would have been: the declarations were not merely unused, they were a fork of facts the prose stated independently -- and the fix is to join them, not to drop one side. Witnesses 7 -> 12. Two of the 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). One incidental catch: to_string over the branded Port had never been evaluated, only resolved -- casting into a brand is exactly where this corpus fails at evaluation while compiling clean. It passes, and now something runs it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UBLsJSnmB8ZdDTh1RRVTe7
…d reachable
CI cause: floor discovery enrolls `test fn`, and my witnesses were plain `fn`,
so the entry contributed zero and the floor refused with FloorDiscoveryRefused.
My local loop ran them by name through --functions, which never needed the
keyword -- the three-rung loop had a gap exactly where the floor looks.
Review 61619, both findings correct:
F1 -- inserting notification_service_realization_standing between the
publication helper's leading annotation and its declaration left an operator
ruling annotating the wrong symbol (§4c/§3). Moved below; each block leads its
own declaration again.
F2 -- NtfyTopic and approval_ntfy_topic were imported and unused while the
grant instruction described "the approvals topic" in English: the same fork the
module's own annotation claims to have fixed for the port and state root. The
topic is now joined into the instruction with two witnesses, and it matters more
than the endpoint did -- the topic IS the access-control surface on a default
ntfy deployment, so granting read on a different topic than the broker
publishes to leaves the real one at read-write, silently.
MEASURED, and the reason this is not just modeling: a wet probe of the modeled
publish path against ntfy.sh reached the network ([rest] POST) and a junk bearer
came back as `TypeError { msg: "HTTP 401: ..." }` -- an untyped throw where the
model promised a typed refusal. The `response { 401 => ... }` block was
decoration: extdeps.transports.rest raises on >=400 unless an operation opts in
to `outcome: RestOutcome`, and this operation never did, so NtfyPublishRefused
had no constructor on any real path. The field is declared and
ntfy_publish_outcome_of is the single route from transport observation to the
outcome type.
Per merry-ibex-741: the dissolution triggers now name CAPABILITIES rather than
contributing artifacts -- the account row retires only when convergence creates
AND verifies the principal by readback, and the server row states it is two
capabilities (verified binary AND converged unit), since a binary alone leaves
a host that looks provisioned and serves nothing. The acquisition facts they
asked for are recorded as an obligation rather than invented: no release tag is
chosen and no artifact hashed, so a version row would be a guess and a digest
row would read as verification that never happened.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UBLsJSnmB8ZdDTh1RRVTe7
Three findings, all the same fork class, all correct:
F1 -- the account intervention hand-authored the useradd argv beside the
declared login while claiming to be "the exact argv EnsureSystemAccount
renders". It now CALLS that renderer, so the hand-run command and the eventual
converged one are one authority by construction rather than by anyone
remembering to keep them equal.
F2 -- the phone-subscription row said "the approvals topic" in English while
the grant row beside it already joined the declaration. Joined, with the reason
stated: subscribing to any other topic receives nothing, silently.
F3 -- ntfy_publish_outcome_of was dangling. It now has six witnesses covering
every arm, including the two statuses the live server actually returns (401 for
an unauthorized token, 403 for a token that authenticates but is not permitted
on the topic) and a control separating RestOk from a 200 whose body did not
decode.
Fixing F3's witnesses surfaced a real defect in the fold: `status as Int` over
an already-Int HttpStatus is refused at EVALUATION ("cannot cast Int to Int")
while compiling clean. The two arms that passed were exactly the two with no
status cast.
THE SERVER IS DEPLOYED on srv1 and its security properties are measured, not
asserted:
- bound 127.0.0.1:2586 only (ss confirms), reachable via `tailscale serve` on
:8443, tailnet-only, alongside the existing dashboard route rather than
replacing it
- anonymous publish answers 403 -- on a default ntfy it would be 200
- the broker token publishes to gunbc-approvals (200), CANNOT read it (403),
and CANNOT publish to any other topic (403)
- ntfy v2.28.0, sha256 verified against upstream's published checksums.txt
before install
The service config no longer pins the literal "https://ntfy.sh", which had
silently made the public service the destination for anything that did not say
otherwise -- for a topic carrying approval capabilities, the worst available
default. The correct form is an operation parameter; the resolver refuses config
identifiers bound to parameters, MEASURED on both compile and run, so the
endpoint is a named row with that gap declared and a trigger naming the resolver
capability.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UBLsJSnmB8ZdDTh1RRVTe7
MEASURED ON THE LIVE SERVER, and invisible to every static check. The operation
posted `{ message: body }` to /{topic}, but that path form takes the message as
a RAW body while this transport always converts `body:` to wire JSON -- so ntfy
stored the literal text `{"message":"..."}` as the notification. The publish
succeeded, the outcome folded to NtfyPublished, and the phone would have shown
JSON. Nothing was wrong except the only thing that mattered.
ntfy's documented JSON endpoint POSTs to "/" with topic and fields in the body,
which is exactly what a JSON-only transport can express faithfully. Cache stays
a header: it is a delivery directive, not message content.
Confirmed by reading the message back from the server:
title : gunbc: approval notifications are live
message : This arrived through the modeled path on your self-hosted server.
click : https://srv1.tailecbe08.ts.net:8443/gunbc-approvals
priority: 4
The §4c boundary caught the first attempt at the annotation, which sat inside
the service body; it now leads the declaration at module scope.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UBLsJSnmB8ZdDTh1RRVTe7
…ount tests
F1 -- ntfy_deployment_base_url was a deployment fact in an upstream-spec module.
The review's prescription was a rostered rung drop or an operator-approved
scaffold; both admit the debt, and DESIGN §3 offers a way to not 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."
So the SERVICE BLOCK ITSELF was in the wrong layer, not just its endpoint.
extdeps.ntfy now owns what ntfy IS -- message shape, priority and cache
vocabularies, outcome type, the two access-control facts -- and the REST binding
plus the address live in gunbc.auth.approval_ntfy_deployment, with the
deployment they belong to. There is precedent: five services already live under
dag/gunbc.
This removes the debt rather than rostering it, and it fixes the narrowing the
review identified: a second deployment is now another binding beside this one,
with extdeps.ntfy untouched.
F2 -- the count witnesses were measurements of a roster authored three files
away in the same PR, and witness_upstream_relay_is_declared compared a data row
to its own literal: `measure() == measure()`, §5's own review tell. Deleted.
What replaces them are properties that survive roster growth: every identity
occurs exactly once (with a positive control proving the predicate can fail --
it is also the check that catches a copy-paste, which no count can see), and
every row carries a non-empty instruction and subject.
Two literals are KEPT and justified rather than deleted: EveryProvision == 0 is
a design claim (the loop must cost a person nothing per run), not a measurement,
and the loopback address is an explicit policy requirement -- both grounded
outside the tree, which is what §5 permits.
MEASURED after the move: the modeled path still publishes to the live
self-hosted server, NtfyPublished { message_id: znjShbquiXow }.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UBLsJSnmB8ZdDTh1RRVTe7
… assertion F1 -- the moved service declares `outcome: RestOutcome` and this module never imported extdeps.transports.rest. It resolved only because extdeps.ntfy.ntfy, which this module does import, pulls in that type for the outcome fold. That is the accidental-coverage shape secret_manager already records: a bare reference that holds because some other module in the closure dragged the definer in is not a binding, and it breaks the moment the fold moves or that import changes. The type is now imported where it is used. It is a floor issue, not a style one. The defect was CREATED BY MY OWN SERVICE MOVE in the previous commit: the service went to the realization layer and the fold that carried its import stayed behind. Moving a declaration moves its obligations, and I checked that the module compiled rather than that it named what it uses. F2 -- `approval_ntfy_endpoint() == "127.0.0.1:2586"` transcribed the port out of a data row three files away, so automating that literal collapses the check to `measure() == measure()` for the port half. It now asserts the RELATION instead: 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, and widening the address still goes red. A positive control pins that the prefix check can answer false. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UBLsJSnmB8ZdDTh1RRVTe7
…ontier
F1 -- approval_ntfy_base_url was one literal re-minting two facts the corpus
owns: the tailnet domain at gunbc.fleet_intent_network `tailnet_domain` and
srv1's identity at `operator_host_srv1`. Moving the binding out of extdeps
fixed the LAYER and left the DUPLICATION, which is §3 nicknaming under a
different roof. It is now joined from both authorities, so renaming either
reddens a witness instead of leaving a stale string.
tailnet_domain is Optional and the service config's `endpoint` cannot carry an
Optional, so the Absent arm has to answer something. It answers a host in the
RFC 2606 `.invalid` TLD, which is guaranteed never to resolve -- a structural
failure rather than an absorbing fallback: it cannot succeed, cannot widen, and
cannot be mistaken for a working endpoint. Both arms are witnessed, with a
positive control that the Present path does NOT produce the marker.
The review also caught that the annotation CLAIMED "witnesses hold them to their
separate jobs" while no witness touched approval_ntfy_base_url at all. That is
the citation-wall failure in miniature -- the symbols resolved, the quantified
claim about them was never true. Four witnesses now make the claim true, and
they are identity joins against the network model rather than transcriptions.
VERIFIED AGAINST THE LIVE SERVER, because a derivation that changes the address
would break the deployment silently: the joined URL publishes to the running
self-hosted server, NtfyPublished { message_id: 8JLDpfuLw8D2 }, at exactly
https://srv1.tailecbe08.ts.net:8443/.
F2 -- the publish binding, the RestOutcome opt-in, ntfy_publish_outcome_of and
approval_ntfy_human_burden have no production caller. True, and §3c's middle
state applies: a declared frontier, admissible only with its trigger stated. The
module now states it at module scope rather than leaving a reviewer to grep for
it -- what is exercised (wet probe plus witnesses, execution but NOT production
consumption), the named consumer (the broker publishing for a pending
AccessRequest), its trigger (the minting path, and ApprovalDecideHandler
redeeming instead of answering 501), and the honest disposition: if that
consumer never lands, this binding is the thing to delete, because with no
requests it carries nothing.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UBLsJSnmB8ZdDTh1RRVTe7
…the model Operator ruling: what I built by hand on srv1 must be converged. It was the §6 tell stated plainly -- out-of-band actuation -- and this makes the model the author of that host's state instead of a runbook. THE GAP WAS NEVER THE OPERATIONS. gunbc.executor_privileged_operation already renders every step this deployment needs: EnsureSystemAccount, EnsureOwnedDirectory, the three systemd verbs. What was missing was a declaration of what the host SHOULD contain, so nothing could reconcile against it. gunbc.auth.approval_ntfy_converge is that declaration -- desired members, each projected to the operation that realizes it, keyed and Ensured rather than Owned so a retract can never delete the message cache or the subscriber's read position. A REAL DEFECT FOUND BY RUNNING IT, not by reading. `useradd` exits 9 when the account exists, so EnsureSystemAccount -- whose name promises otherwise -- fails on every convergence after the first. It read as idempotent because its ONE caller, live_deploy's publication-principal step, wrapped it in `id -u ... ||`: the guarantee lived in the neighbour, so the operation looked covered while any second caller inherited the failure. Measured on srv1: rc=9 for the account, rc=0 for the other six. The precondition now belongs to the operation, as an EXHAUSTIVE match with no wildcard arm so a new operation must decide whether it needs one rather than defaulting to "none" and inheriting the same silence. live_deploy now consumes that authority instead of spelling the guard inline; its emitted bytes are unchanged, which is not a claim -- all 59 live_deploy emit witnesses pass. VERIFIED AGAINST THE HOST, twice: the 7 rendered commands applied to srv1 with 0 failures on the first pass and 0 on the second, with the service still active and the endpoint answering 200. A convergence that fails on its second run is not a convergence, so idempotence is the property that was actually tested. WHAT THIS DOES NOT YET DO, stated because it decides whether the human steps may retire: it declares the desired side and applies it idempotently, but does not OBSERVE the host, so it cannot answer whether a member is already converged and an installer exiting zero over an absent member would pass unnoticed. That readback is std.realization_reconcile (merry-ibex-741); this family is shaped to plug into it rather than grow a second answer for "did the plan converge". The interventions therefore stand, with their triggers unchanged. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UBLsJSnmB8ZdDTh1RRVTe7
… own claim
Three findings, all correct, and the first two catch overclaims I made in the
commit message rather than only in code.
F1 -- the account intervention still said "no converged member renders it for
this principal yet" AFTER the converge family landed, which is two answers to
one question inside a single PR. Worse, the intervention rendered through
executor_privileged_operation_shell_command while the member used
executor_privileged_operation_converge_command, so the annotation's claim that
they are "one authority by construction" was FALSE: the operator's copy-paste
lacked the precondition and would exit 9 on a host that already had the account.
Both now call the converge renderer, and a witness holds them EQUAL -- because a
prose claim is exactly what failed to catch this, twice.
F2 -- `NtfyUnitInstalled => [SystemdDaemonReload]` named an obligation its
projection did not discharge. It installs nothing; enable and start converged
only because a human had already placed the unit file, so on this host the
difference was invisible. That is §5's plausible-realization failure, and it
made my commit message's "srv1's state is now rendered by the model" false. The
member is renamed for what it does, the unused InstallFile import is gone, and
the module states the boundary plainly: this roster CANNOT converge a fresh
host. The config file, the unit file and the binary 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.
F3 -- RestTransportRefused folded to NtfyPublishRefused { status: 0 }, which
reintroduced one layer up the exact fabrication extdeps.transports.rest exists
to prevent ("no response arrived, so no status can be fabricated"). It also
collapsed two states with different remedies: the server refused this publish,
versus no server was reached. NtfyPublishUnreached is now its own arm carrying a
cause and no status, with a witness each way so neither collapses into the
other.
The exhaustiveness wall found every consumer of the widened coproduct, which is
the floor doing its job on a change that would otherwise have been silent.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UBLsJSnmB8ZdDTh1RRVTe7
…lete the pipeline
Four findings, all correct.
F1 -- RestBodyUndecodable folded into NtfyPublishRefused { status }, so a 200
whose body did not decode became "refused with status 200". That is the SAME
collapse this PR's own annotation condemns one arm above, written while I was
splitting the transport arm for exactly that reason. The server accepted and we
failed to read the reply; the remedies diverge completely. NtfyPublishUndecodable
is its own arm, keeping the status it really received, with a witness pinning
all three failure outcomes mutually distinct.
F2 -- the converge roster re-minted "/etc/gunbc-ntfy" and
"/var/lib/gunbc-ntfy/attachments" while importing the declarations that own both
roots, so a rename would have left it ensuring directories the server does not
use. 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 -- the precondition arms authored shell as string literals with the login
interpolated unquoted, a second authorship of this module's own calling
convention. 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. The residual
redirection and `||` join are named as residue with a dissolution trigger
pointing at the If-Not-ExitZero orchestration intent live_deploy already uses.
F4 -- 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 to prove the property. Now Present { value: Ensured }.
Quoting the guard changed live_deploy's emitted bytes, so its witness -- which
pinned the unquoted spelling -- was updated to assert the guard's SHAPE rather
than its quoting, and two of my own witnesses needed the same correction. All 59
live_deploy emit witnesses pass.
RE-VERIFIED ON srv1 after the paths became derived and the quoting changed: the
7 rendered commands apply with 0 failures twice, service active, endpoint 200.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UBLsJSnmB8ZdDTh1RRVTe7
…alse claim F1 -- ntfy_member_key_eq, ntfy_member_value_eq and approval_ntfy_member_argv had no consumer anywhere in the tree. Written in anticipation of a membership_reconcile call I never made, and carrying none of the declared-frontier statement the sibling module writes for its publish binding. Deleted. The corroboration in the finding is the part worth keeping: 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 was written for. Nothing caught it because nothing ran it. That is §3c's argument in one artifact: unconsumed code is not merely idle, it is unexamined, and it accumulates defects that surface only when someone finally wires it up. The module now records that rather than just losing the functions quietly. F2 -- live_deploy's annotation asserted "The emitted bytes are unchanged". That was true when written and became FALSE two commits later when the precondition started rendering through posix_single_quote, and it was contradicted by this PR's own witness update in the same diff. §4c is explicit that an annotation is never evidence a machine claim holds; this one stated a machine claim that was wrong. It now says what actually happens -- the login arrives single-quoted, equivalent shell, one fewer place deciding quoting -- and cites what IS 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 because a reviewer read the diff against itself. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UBLsJSnmB8ZdDTh1RRVTe7
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 this exactly: "the check is not a weak wall but a
decoration ... 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 claim rested
on a check that could not fail.
Both are deleted. The constraint itself is real and is stated as what it is: a
requirement on the 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. Declaring an Optional that is never Absent would be a third
representation of a decision nobody makes.
Also corrected, from the same finding's second half: the heading "THE KEY IS
CONSUMED" overstated what ntfy_member_key's consumers are. They are two
witnesses, not production. The module now carries a §3c frontier statement at
module scope covering the whole family -- 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 and 0 failures across
two consecutive passes. The desired side is real; the observed side does not
exist, and the module says so once rather than implying coverage in three places.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UBLsJSnmB8ZdDTh1RRVTe7
|
Closing rather than flipping to ready: this PR has nothing to land, and readying it would be harmful. #10714 merged at 10:12:25Z, squash-merged as Verified rather than assumed — the squash flattens history, so a raw
The two paths that differ are That is the reason for closing rather than readying: this PR carries no new work, and advancing a stale branch over paths another lane has since changed risks reverting theirs for nothing gained. The CI failure reported here against If new work follows in this session it should start from a fresh branch off current main. -- sent from crisp-ram-671 |
Auto-opened by session-dashboard for session
crisp-ram-671.Pushing to
session/crisp-ram-671-ntfy-deployadvances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan