jcp §4.10: the flow gate had no spec section, and six code references cited it #190

Merged

dcharlot merged 1 commit from feat/revocation-freshness into main 2026-10-09 02:49:32 -04:00

Conversation 0 Commits 1 Files changed 2 +170

2026-10-08

Transaction Science

jcp §4.10: the flow gate had no spec section, and six code references cited it ...

`jcp-runtime` cites "SPEC §4.10" in six places — the taint floor, the flow gate,
check 6c — and jcp/SPEC.md had no §4.10. The section was never written. So the
mechanism that decides whether a value's provenance may exercise a grant is
implemented, gate-enforcing and tested, with no normative text behind it: the
mirror of the defects this sweep has mostly been closing, a check with no claim
rather than a claim with no check.

I found it by nearly colliding with it — #189 had taken §4.10 for durable spend
and is renumbered to §4.11, because the code had already spoken for the number.

§4.10 documents what is there, and every normative sentence is backed by an
existing test:

- the label's three independent components, `⊥` and `⊤`;
- the ceiling as a `FlowBelow` caveat, several composing to the strictest via
  `meet` on the label and `min` on the tainted sub-budget, so attenuation never
  widens one;
- the taint floor as the enforcement point's own refusal, the flow analogue of a
  trust root, default-open;
- the three-case table whose middle row is the point: provenance **absent** is
  not provenance **clean**, and a ceilinged grant fails closed on an unlabelled
  argument;
- the placement, which is normative: after capability and signature, because a
  ceiling inside an unauthenticated grant would seal a verdict over
  attacker-chosen policy; before caveats and budget, so a tainted call costs
  zero joules.

One sentence I had to pull back: I first wrote that the implementation
propagates labels. It does not — `flow_gate` takes the facts from its caller, so
propagation belongs to the host, which is the only party that sees the data move.
The spec now says so, and says what JCP does guarantee instead: a host that
propagates gets a decision bound to what it reported, and one that does not gets
a refusal rather than a pass.

Conformance class **C25** is declared and defined in §9's list. It cites only
behaviour `jcp-runtime` already tests — zero-debit flow denial, failing closed
without facts, the taint floor overriding a permissive ceiling, the tainted
sub-budget, and byte-identical encoding without a flow caveat.

**§4.3 gains a Propagation paragraph.** §4.3 binds an enforcement point *once it
holds* a revocation and says nothing about how it comes to hold one. With a
budget sharded across N points (§4.5), a revocation that reached three of five
leaves the grant live at two — and an allow from a point that had not yet heard
is indistinguishable, after the fact, from an allow by a point that heard and
ignored it. The first is propagation delay; the second violates this spec. An
implementation MUST now define how revocations reach its points and SHOULD let
each state how current its knowledge is; `Runtime::revocation_known_through`
records it, defaulting to `None`, which an auditor MUST read as *unverifiable*
rather than current.

Stated in the method's own docs rather than left implied: the marker is state on
the enforcement point and the `jcp/2` receipt does not carry it, so an auditor
needs it reported out of band. Binding it into the signed core is the stronger
fix and reaches every `Decision` construction site across six standards'
reference implementations — 75 of them, in workspaces that do not build
together — so it is a separate piece of work rather than a line in this one.

Falsifying the marker caught a vacuous assertion of my own. I had written that
declaring a marker changes no decision, and checked it by comparing two runtimes
that both held *no* revocation — which passes however the marker behaves. The
test now applies a real revocation first, so clearing the revocation set from
the setter is caught. Two earlier mutation attempts also "passed" because they
patched lines that do not exist: `Runtime` derives `Default`, so the marker's
`None` comes by derivation and there is no constructor literal to break.

jcp-rs workspace: 404 passed. The two clippy warnings in jcp-runtime are
pre-existing (2 on the baseline, checked against the stash).

Co-Authored-By: Claude Opus 5 <[email protected]>

0d107105c6

• View at this point in history

2026-10-08 11:13:38 -04:00