Track: envelope refinement — discriminating a verified boundary on declared request facts

[accuser]

The theme

Bynk's boundary can say how a party proved itself, but not what its request
carried. An actor declares an authentication scheme and the compiler generates
the verification; everything else the request brought — a header, a query
parameter, the content negotiation — is invisible to the language. Where a real
service needs one of those facts, Bynk has so far grown a bespoke compiler
section for it: cors { }, security { }, limits { }, @cache, the
Accept-Language negotiation inside the Locale provider. Five closed grammars
for one idea.

The forcing case is the inbound webhook. GitHub registers one URL, signs
every delivery with one secret, and then sends push, pull_request,
issues and a dozen more to it — each with a different body shape, discriminated
only by X-GitHub-Event. Bynk can verify the HMAC (ADR 0089, including GitHub's
sha256= shape) and then cannot tell the deliveries apart. The track's end state:
an actor declares the request facts it reads alongside the scheme that
verifies it; refinement over those facts is an ordinary predicate; and a route
can carry sibling handlers discriminated by provably-disjoint refinements, each
with its own typed body. Along the way the closed claim-predicate catalogue
(hasClaim/claimEquals) is retired rather than extended, collapsing two of the
three where tiers into one.

• Realises: design/bynk-design-notes.md §6 (actor declarations as
  contracts — the "authorisation invariants" and "replay and ordering" categories
  that never shipped), §7 Boundary validation via refined types (which already
  promises that "a header" is a trust boundary where refined types validate —
  the one clause of that sentence the compiler never implemented), and §21
  Authentication scheme extensibility (the residual half ADR 0175 left open).
• Track doc (added by the settling PR): design/tracks/envelope-refinement.md

Why a track (the ADR 0076 trigger)

• Multi-increment — the grammar change (actor body + envelope clause),
  the refinement generalisation and claim-catalogue retirement, the
  discrimination/dispatch rule, and the optional sum form are four independently
  shippable, independently reviewable surfaces with a forced order. A
  delete-on-merge proposal cannot carry the map across them, and the second of
  them is a breaking change to a Foundations-layer surface, which needs a
  decision recorded somewhere durable before the first one lands.
• Surface not yet settled — genuinely open: whether the envelope is a
  per-field keyword or a section; what the closed source vocabulary is beyond
  Header; whether discrimination lands at the route or in the by sum; how
  wide the provable-disjointness form is; and whether typed claims fully
  subsume the catalogue or leave a residue. Several of these were reversed
  during the exploration that produced this issue.
• Security/safety boundary — this is the authentication and
  authorisation seam. A wrong foundational shape here either weakens the 401
  channel (by letting app-shaped predicates influence verification rather than
  only admission), or introduces a pre-authentication attack surface (see the
  threat model below), or bakes a spoofable value into a decision that should
  never trust it. ADR 0087's bypass-class posture applies to every slice.

Open design questions

1. Where does the verification/admission line fall, and is it the organising
   commitment? ADR 0091 already split 401 (verification) from 403 (admission)
   but coupled admission to the Bearer mechanism, because claims happened to
   arrive from the JWT. The proposition to settle: verification stays closed,
   compiler-owned and widened only by enum (ADR 0080/0175 unchanged); admission
   is scheme-independent and predicate-shaped. If that holds, "refine a
   webhook" and "refine an OIDC user" stop being separate features. This is the
   ADR 0144-shaped call the rest of the track hangs off, so it must close first.
   Needs: a re-read of 0085/0091/0175's reasoning to confirm none of the
   anti-Verifier[T] argument applies to non-cryptographic admission.

2. The actor body shape. actor_decl is today a fixed, comma-separated
   two-clause body — auth and identity are grammar keywords, not author-named
   fields — so repeatable typed declarations do not fit it. The candidate is to
   follow agent_decl (newline-separated, keyword-introduced, fixed order) with
   a per-field envelope <name>: <Type> = <Source>(...) clause, store's shape.
   Open: per-field keyword vs a sectioned envelope { } block; and whether the
   comma-to-newline move is done as part of this or separately.
   Needs: a survey of the other body grammars for the least surprising shape.

3. The source vocabulary, and its admission criteria. Header(...) is
   clearly first. Is the closed set Header | Query | Method | Path | Cookie, or
   narrower? What makes a candidate admissible — and what keeps this from
   becoming the sixth accumulating closed section this track exists to stop?
   Needs: the §18 first-party-capability criteria applied to sources, and a
   check against what cors/security/limits would need to be re-expressed
   over this seam (they may not, and saying so explicitly matters).

4. Where discrimination lands. Two candidates with the same disjointness
   rule: (a) sibling handlers on one route, widening
   bynk.http.duplicate_route to "conflict unless the by refinements are
   provably disjoint"; (b) a sum of sibling refinements, which additionally
   needs duplicate_sum_scheme widened (the "distinct verifier" widening ADR
   0090 explicitly reserved), refinement_in_sum retired, and a per-arm body =
   on the refinement so the payload type can vary. (b) is arguably the better
   modelling — a discriminant implies a payload shape — but (a) needs strictly
   fewer changes. Open: which ships, and whether the other stays open.
   Needs: confirming (a) does not foreclose (b), and checking (a) against the
   router's existing matching order (ADR 0162's 405/OPTIONS fall-through and
   0159 D5's pre-auth preflight branch).

5. How wide is "provably disjoint"? ADR 0090 states the compiler does not
   reason about predicate-level disjointness, and that conservatism is right for
   open predicates. The floor here is narrow and decidable by inspection:
   equality on one shared field against distinct string literals. Open: does it
   extend to !=, to || of equalities, to a literal set — and what is the
   diagnostic when a sibling pair is outside the admissible form?
   Needs: the rule stated so a reviewer can check it by eye, per 0090's own bar.

6. The unmatched-kind outcome. An event kind no handler claims must not
   be a 4xx: a provider retries, then disables the webhook. Neither existing
   channel says this — 401 (0090's total-sum failure) is false because the sender
   did authenticate, and 403 (0091) is false because it is not forbidden. The
   candidate is the unrefined base as catch-all, reusing the existing
   must-come-last reachability rule verbatim (the Visitor rule, one level
   down), returning 204. Open: is a missing catch-all a diagnostic, or an
   implicit 204? Silence here is the production failure this feature exists to
   prevent, so it should probably be loud.

7. Does the claim catalogue fully retire? ADR 0091 closed tier 2 for a stated
   reason — "claims are untyped JSON, so an arbitrary typed expression has no
   surface to bind against". A declared claims = <RecordType> supplies the
   surface and the reason lapses, making the position tier 3 and collapsing 0189's
   three tiers to two. Open: the projection semantics (verified claims constructed
   through the record, refined fields validated, undeclared claims dropped); what
   a Bearer/Oidc actor that declares no claims can refine on; and whether any
   claim test genuinely resists expression as a predicate over a typed record.
   Confirmed already: is collects depth-1 payload bindings and
   collect_is_bindings_into recurses through BinOp::And, so
   claims.scope is Some(s) && s == "…" is expressible — optional claims need no
   builtin.

8. The predicate case rule, stated normatively. §16 already makes identifier
   case load-bearing (constructor vs binding). Under it, Matches/NonEmpty/
   Signature/Oidc are correctly capitalised — closed constructors, type
   position, never values — and hasClaim/claimEquals are the outliers, which
   is plausibly why they read as tier 3 when they are tier 2 (the confusion ADR
   0189 had to write down). Open: state the rule normatively, and audit whether
   anything else in the language violates it.

9. Explicitly in or out: secret sourcing. ADR 0175 B flagged
   Bearer(secret = "<ENV>") as configuration baked into the contract,
   established the public-parameters-only shape via Oidc, and deferred
   reworking Bearer/Signature. It sits on the same declaration this track
   reshapes, and inside the surface 1.0 freezes. Either it comes in scope here or
   the track says why not — it should not be deferred silently a second time.

Candidate slice decomposition

Provisional until the doc settles.

• Slice 1 — the envelope clause. Actor body to newline-separated;
  envelope <name>: <Type> = <Source>(...); the boundary reads and validates
  through the declared refined type; a binder on a Signature actor yields the
  envelope (today it is forbidden, identity being ()). No refinement or
  dispatch change. Carries the front-loaded ADRs.
• Slice 2 — scheme-independent admission + typed claims. Relax
  refinement_base_unsupported; the refinement predicate becomes an ordinary
  expression over envelope fields and a declared claims record; retire
  hasClaim/claimEquals. Oidc and Signature become refinement bases as a
  consequence, not as separate features. The breaking slice — see sequencing.
• Slice 3 — route-level discrimination. The disjointness rule; widen
  duplicate_route; the unrefined-base catch-all and its reachability rule;
  relax signature_requires_body (the HMAC is verified over raw bytes whether or
  not an arm parses them — parsing becomes per-arm, verification never was).
• Slice 4 — the third envelope field. X-GitHub-Delivery is an idempotency
  key, and ADR 0089 punted replay dedup with "that is the Idempotency
  capability's job — the declaration shape leaves room". Contingent on
  Idempotency shipping; if it has not, this slice states the wiring and defers.
• Slice 5 — the sum form (optional). Per-arm body =, refinement_in_sum
  retired, duplicate_sum_scheme widened. Only if Q4 keeps it open.

Slice status

• Slice 1 — the envelope clause
• Slice 2 — scheme-independent admission + typed claims
• Slice 3 — route-level discrimination
• Slice 4 — the delivery-id / Idempotency seam
• Slice 5 — the sum form (optional)

Front-loaded ADR candidates

Load-bearing and expensive to reverse once a slice ships surface against them.
Numbers taken at merge.

• Verification is closed; admission is open and scheme-independent. The
  organising commitment (Q1) — the ADR 0144 of this track. Every later slice
  cites it, and a proposal that would let a predicate influence verification is
  out of bounds on its strength alone.
• Scheme outputs vs request facts. auth/identity/claims describe what
  verification produced; envelope fields describe what the request carried,
  independent of scheme. This is the split that makes admission scheme-independent
  rather than merely permitted, so it belongs in the grammar, not in prose.
• The predicate case rule. Capitalised = closed constraint/descriptor
  constructor, type position, never a value. Lowercase = ordinary value
  expression. Retroactively justifies Matches/Signature, condemns hasClaim,
  and governs every future predicate spelling.
• Disjointness is decidable by inspection only. The closed admissible
  predicate form, and the refusal to reason further — the guarantee that keeps
  reachability checkable by a reviewer as well as by the compiler.
• The claim catalogue retires rather than recases. A removal from a
  Foundations-layer surface, and therefore a now-or-never call against the
  1.0 freeze.

Sequencing against 1.0

design/bynk-1.0-definition.md names the Foundations layer as including "actor
declarations for authentication", and commits that a breaking change to it is a
2.0 event. Two consequences the settling phase must confront:

• Slice 2 is a removal. A rename (hasClaim → HasClaim) could ship
  additively with a deprecation window at any point in 1.x; a retirement
  cannot. If the two-tier end state is wanted, it lands before the freeze or not
  for a major version.
• The layer boundary is itself ambiguous and should be settled here. The
  Foundations list says "for authentication" — on a literal reading, authorisation
  refinements are outside the frozen line, which would leave the whole 403 channel
  free to evolve through 1.x. It is silent on the scheme set, the predicate
  catalogue, and the cors/security/limits sections. That ambiguity decides
  how much of this track is urgent, so the track should either settle it or raise
  it against Strategy & positioning toward 1.0 (identity, blocker sequencing, cadence, comparison page) #540.

Threat model

Assets. The authentication decision (who is admitted, 401), the authorisation
decision (what an admitted party may reach, 403), and — new to this track — the
routing decision (which handler and which body type a verified request reaches).

Adversary. An unauthenticated caller; a caller holding a valid credential for
a different admission class; and, specific to webhooks, a party who can replay
or craft a request carrying attacker-chosen headers.

Where verification happens — unchanged. Compiler-generated, at the entry
dispatch / compose wrapper, fail-closed, before the body runs (ADRs 0082, 0085,
0089, 0175). This track adds no app-authored crypto and no user-supplied
verifier; the §21 Verifier[T] question stays closed and out of scope.

Risks the settling phase must resolve:

• The discriminant is not integrity-protected. GitHub's HMAC covers the
  body, not the headers — so X-GitHub-Event is attacker-chooseable even on a
  signature-valid request. It is therefore safe for routing (a mismatched
  body then fails its own typed validation) and never safe as an
  authorisation input. The track must state this boundary explicitly and decide
  whether the language should enforce it — e.g. by keeping envelope fields out of
  admission predicates on schemes that do not cover them, rather than trusting
  authors to know.
• Ordering: envelope validation vs verification. Validating a refined
  envelope field before the scheme verifies means running an author-supplied
  predicate over unauthenticated attacker input. With Matches that is a ReDoS
  surface — the exact attack ADR 0223 exists to bound, and 0223's guard is
  deliberately conservative, not total. Either envelope refinement runs strictly
  after verification, or the admissible source predicates are narrowed to
  constant-time forms. This is the sharpest open question in the model.
• Opening the predicate surface must not soften the 401 channel. Retiring the
  claim catalogue widens what an admission predicate may say. The track must
  confirm no widening reaches the verification decision, and that a predicate
  that fails to evaluate is fail-closed rather than fail-open.
• Route dispatch on a header changes the router's attack surface. A request
  can now select among sibling handlers. Disjointness plus a mandatory catch-all
  is what keeps that total; the bypass-class tests (ADR 0087) must cover
  no-arm-matches, wrong-arm-selected, and a spoofed discriminant against a
  valid signature.
• Catch-all correctness is a security property, not just an operational one.
  A 4xx on an unknown kind gets a provider to disable the webhook — an
  availability failure induced by any party who can send an unrecognised event.

Standing guards. Each slice carries behavioural bypass-class tests in the ADR
0087 posture, extending signature_auth.rs / refinement_auth.rs /
multi_actor_sum.rs rather than adding a parallel harness.