# FL-2 / `jcp-flow` — flow-lattice provenance propagation design

> Blueprint for upgrading JCP's one-bit `Trust::Control/Data` boundary into
> propagated provenance labels, sealed into JCR-1 receipts and the joule budget.
> Produced by a multi-agent design+adversarial-judging pass (4 designs × 3 attack
> lenses → synthesis), then verified against the real tree.
>
> **Status:** increment 1 of ~5 shipped — the flow lattice (`jcp-schema/src/flow.rs`,
> laws L1–L16). Remaining: witness/store/scan + L17–L20 (`jcp-flow`), the runtime
> gate (`jcp-runtime`), the `jcp/3` receipt seal (`jcp-receipt`), and the gateway
> Phase 0–4 relay (`jcp-gateway`). See §1's file list.

---

Verified against the real tree: `jcp-flow` does not exist yet, the gateway depends on `jcp-schema/jcp-grant/jcp-runtime/jcp-receipt/jcp-bridge` (not `jcp-policy`), and the runtime signatures match the grounding exactly (`check` at :272, `authorize` :320, `charge` :354, `decide` :227, `decide_chained` :385). That confirms the two structural facts the plan must respect: the gateway seals only through `ReceiptLog`/jcp-2 and drives `authorize`→`charge`, never `decide` and never a `PolicyEngine`.

Here is the synthesized plan.

---

# FL-2 / `jcp-flow`: a sealed flow lattice with a replayable provenance witness

**One-line thesis.** Keep FL-1's lattice-as-authorization core, but bind and seal the verdict on the path the gateway *actually runs* (`authorize`→`charge`→`ReceiptLog`, profile `jcp/3`), and make it replayable with PROV-1's content-addressed witness disclosed through a store — not through a `policy/1` sibling that has no emitter and not through a `store_root` that cannot be reopened.

## 0. What was grafted, and every winner fatal-flaw resolved

| Winner (FL-1) fatal flaw | Resolution in FL-2 |
|---|---|
| **F1** buzhash rolling hash is buggy; "Law L17" (39-byte carry guarantee) is false; short secrets below floor invisible | Replace the fragile rolling hash with an **exact `blake3` W-byte-window index** (TAS's mechanism, W=16, no rotate arithmetic to get wrong). Carry ≥ W bytes is *exactly* detectable. Add a **`SensitiveTerms` exact index** for short registered secrets (account numbers, recipients) so length-`<W` values are caught when a boundary adapter registers them. Sub-W, unregistered, non-high-water carry is a **stated residual** (§7). |
| **F2** `decide ≡ decide_flow(bottom)` self-contradicts the fail-closed rule `flow_gate(Some(c),None)=deny` | **Drop the false equivalence law.** Replace with an honest compat *pair* (§5): ceiling-free grants → gate is a no-op for *any* facts (byte-identical); ceiling grants on a facts-less caller → **fail closed**. `Some(bottom)` (computed-clean) and `None` (not-computed) are deliberately different inputs. |
| **F3** `eval_uj` folded into `cost_uj` breaks byte-identity and mutates a field's meaning | `flow_uj` is a **separate jcp/3-only field with its own `flow_energy_provenance`**, never folded into `cost_uj`. Clean frames stay `jcp/2` with `cost_uj` = tool cost, byte-for-byte. |
| **F4** Readers (confidentiality) half is inert; no ACL source of truth | Ship **integrity × origins** as load-bearing. `Readers` stays in the type and is sealed, but *enforcement over readers is explicitly v2*, gated behind a per-tool audience oracle. Stated as a scoped residual, not claimed to work. |
| **F5** `policy/1` has no emitter on the gateway path; verdict sealed nowhere | Seal into **`jcp/3` via `ReceiptLog`** — the profile-bump path the gateway already uses. `policy/1` additions become an *optional* second gate for deployments that run a `PolicyEngine`, not the primary binding. |
| **F6** `jcp/2` cannot carry a flow block (PayloadMismatch on recompute) | Correct — so **bump to `jcp/3`** and recompute under the new tag, retaining `to_jcr1_wire_v2` as the subtraction projection (exact `jcp/1→jcp/2` precedent). Clean frames still mint `jcp/2`. |
| **F7** `store_root` unrecomputable from the receipt (needs raw bytes) | Replace the running-hash `store_root` with a **self-contained `Witness`** (the minimal ancestor cut + edges + evidence), content-addressed, committed by id in the receipt, and **disclosed through a `WitnessStore`** (the `jcp-cite::Citation` pattern). Replay is honestly "receipt **+ disclosed witness**," not receipt-alone. |
| **F8** budget couplings live in `decide`/`decide_priced` (zero production callers); no `charge_flow` | Add **`authorize_flow`** (pre-checks the tainted sub-ceiling, like the main budget's `remaining==0`) and **`charge_flow`** (debits `spent_tainted_uj`). Both are wired into `Gateway::relay`. |

Grafted, beyond the flaw fixes:
- **PROV-1**: eager, `id()`-bearing, order-free `Label`; the `Witness`/edge-proof/replay-verifier; **cut-completeness anti-excision**; `Endorsement` (signed declassification); the `replay_spend` under-count bug fix.
- **FlowDAG**: content-addressed node id = `blake3` over parents ⇒ a `ValueId`/`Label::digest()` is a Merkle root, memoisable with no invalidation; `context_digest` binding consent to exact ancestry.
- **TAS**: exact W-window index (kills F1); the resource-keyed `TaintFloor` shaped like `trust_roots` (an enforcement-point-wide control needing no new grants); origins content-addressed by `mcp_resource` id (fixes TAS's own order-dependent-bit defect — an operator can author floor rules at startup).

---

## 1. Exact Rust types and where they live

### 1a. New crate `crates/jcp-flow/` (the lattice, store, witness, scan)

`Cargo.toml`: `jcp-schema = { workspace = true }`, `serde = { workspace = true }`, `blake3` (default-features=false). `#![cfg_attr(not(feature="std"), no_std)] #![forbid(unsafe_code)]`, `extern crate alloc`. **`BTreeMap`/`BTreeSet` only** — no `HashMap` anywhere (hash iteration order would make `store` roots and receipts non-reproducible).

`crates/jcp-flow/src/lattice.rs`:

```rust
use jcp_schema::{ContentId, Did, Trust};
use serde::{Deserialize, Serialize};
use alloc::collections::{BTreeMap, BTreeSet};

/// Integrity chain (total order); higher rank = more believable. Join in the
/// TAINT order takes the WEAKER (min) — same shape as jcp_trace::weaker.
#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
#[serde(rename_all = "kebab-case")]
pub enum Integrity { Untrusted = 0, Derived = 1, Attested = 2, Principal = 3 }
impl Integrity {
    pub const fn rank(self) -> u8 { self as u8 }
    pub const fn weaker(self, o: Self) -> Self { if (self as u8) <= (o as u8) { self } else { o } }
    pub const fn stronger(self, o: Self) -> Self { if (self as u8) >= (o as u8) { self } else { o } }
}
impl From<Trust> for Integrity {              // Data ↦ Untrusted, Control ↦ Principal
    fn from(t: Trust) -> Self { match t { Trust::Control => Integrity::Principal, Trust::Data => Integrity::Untrusted } }
}

/// Where a value came from: the CONTENT-ADDRESSED channel id (mcp_resource(server,tool))
/// plus the principal inside it. Content-addressed, not string-named, so it is
/// forgery-resistant AND floor rules are authorable at startup from a known channel id.
#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
pub struct Origin { pub channel: ContentId,
    #[serde(skip_serializing_if="Option::is_none", default)] pub principal: Option<Did> }

pub const MAX_ORIGINS: usize = 64;

#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all="kebab-case", try_from="OriginsWire")]
pub enum Origins { Set(BTreeSet<Origin>), Any }   // Any = saturation top; sound over-approx
// (norm(): |set|>MAX_ORIGINS ⇒ Any. `try_from` on the wire re-imposes norm so ⊑ stays antisymmetric.)
impl Origins {
    pub fn join(&self, o:&Self)->Self;  // union, saturating
    pub fn meet(&self, o:&Self)->Self;  // intersection; Any is identity (for ceilings)
    pub fn leq(&self, o:&Self)->bool;   // subset; _ ⊑ Any
    pub fn intersects(&self, mask:&Self)->bool;  // used by TaintFloor
    pub fn none()->Self; pub fn one(o:Origin)->Self; pub fn is_empty(&self)->bool;
}

/// Confidentiality half — PRESENT & SEALED, enforcement is v2 (see §7).
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all="kebab-case")]
pub enum Readers { Public, Only(BTreeSet<Did>) }
impl Readers { pub fn join(&self,o:&Self)->Self /*intersection, Public=id*/;
    pub fn meet(&self,o:&Self)->Self; pub fn leq(&self,o:&Self)->bool;
    pub fn permits(&self, audience:&BTreeSet<Did>)->bool; }

/// A point in the flow lattice. Private fields ⇒ equality is semantic ⇒ ⊑ antisymmetric.
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct Label { integrity: Integrity, origins: Origins, readers: Readers }
impl Label {
    pub fn bottom()->Self;  // (Principal, ∅, Public)  ← neutral / pre-flow
    pub fn top()->Self;     // (Untrusted, Any, Only(∅)) ← unknown id resolves here
    pub fn join(&self,o:&Self)->Self;   // weaker integrity, ∪ origins, ∩ readers  ← THE operator
    pub fn meet(&self,o:&Self)->Self;   // ceilings only
    pub fn leq(&self,o:&Self)->bool;    // rank≥ ∧ origins⊑ ∧ readers⊑   ← authorization
    pub fn is_bottom(&self)->bool;
    pub fn digest(&self)->ContentId;    // Merkle root: canonical-CBOR-legal by construction
    pub fn trust(&self)->Trust;         // Untrusted↦Data else Control   (retraction)
    pub fn integrity(&self)->Integrity; pub fn origins(&self)->&Origins; pub fn readers(&self)->&Readers;
}
impl From<Trust> for Label { /* (Integrity::from(t), none, Public) */ }
```

`crates/jcp-flow/src/witness.rs` — the replayable artifact (PROV-1's insight, made concrete):

```rust
/// Evidence class of a taint edge — SEALED, so the receipt shows whether the
/// verdict rested on hard bytes or the conservative floor.
#[derive(Clone,Copy,Debug,PartialEq,Eq,PartialOrd,Ord,Serialize,Deserialize)]
pub enum EdgeKind { Witnessed, Declared, Ambient }

#[derive(Clone,Debug,PartialEq,Eq,Serialize,Deserialize)]
pub struct Edge {
    pub parent: ContentId,      // the ancestor payload's content id (its store key)
    pub kind: EdgeKind,
    #[serde(skip_serializing_if="u64_is_zero", default)] pub witnessed_bytes: u64,
    // For a Witnessed edge, the fingerprints proving overlap — a third party
    // rechecks these against BOTH endpoints' window sets (subset test).
    #[serde(skip_serializing_if="BTreeSet::is_empty", default)] pub grams: BTreeSet<u64>,
}

/// The MINIMAL ancestor cut + its edges + the folded label. Content-addressed,
/// self-contained, offline-replayable. The receipt commits only `id()`.
#[derive(Clone,Debug,PartialEq,Eq,Serialize,Deserialize)]
pub struct Witness {
    pub schema: alloc::string::String,          // "flow/1"
    pub params: ScanParams,                     // W, and (later) sensitive-term set digest — pinned for exact replay
    pub subject: ContentId,                     // == frame.payload_hash of the decided call
    pub label: Label,                           // the folded effective label
    pub cut: alloc::vec::Vec<CutNode>,          // each direct ancestor: (content id, label, anchor)
    pub edges: alloc::vec::Vec<Edge>,
}
#[derive(Clone,Debug,PartialEq,Eq,Serialize,Deserialize)]
pub struct CutNode { pub id: ContentId, pub label: Label, pub anchor: ContentId } // anchor = ReceiptLog head when admitted
impl Witness { pub fn id(&self)->ContentId { ContentId::of(self).expect("canonical") } }

/// What the runtime consumes at gate time. Bottom ⇒ every existing path is byte-identical.
#[derive(Clone,Debug,PartialEq,Eq)]
pub struct FlowFacts {
    pub label: Label,
    pub witness_id: ContentId,   // commitment; the Witness itself lives in the WitnessStore
    pub eval_uj: u64,            // monitor's own metered cost — reported, never folded into cost_uj
    pub eval_prov: jcp_schema::Provenance,
}
impl FlowFacts { pub fn bottom()->Self; pub fn is_bottom(&self)->bool { self.label.is_bottom() } }
```

`crates/jcp-flow/src/store.rs` — session state + the **exact** carry detector (F1 fix):

```rust
pub const SCAN_W: usize = 16;                    // detection floor = exactly W bytes (blake3, not buzhash)
#[derive(Clone,Copy,Debug,PartialEq,Eq,Serialize,Deserialize)]
pub struct ScanParams { pub w: u16, pub sensitive_root: ContentId } // pinned in every Witness

/// Every W-byte window, DOMAIN-SEPARATED blake3 → u64. No rolling state, no
/// rotate arithmetic (the FL-1 bug lived there). Same bytes ⇒ same set, always.
fn windows(bytes: &[u8], w: usize) -> BTreeSet<u64> { /* blake3::keyed_hash("jcp/flow/window/v1", &bytes[i..i+w]) truncated */ }

pub struct FlowStore {
    labels: BTreeMap<ContentId, Label>,
    windows: BTreeMap<u64, BTreeSet<ContentId>>,   // fingerprint → admitted ids containing it
    sensitive: BTreeMap<alloc::vec::Vec<u8>, BTreeSet<ContentId>>, // short registered terms → source ids
    order: alloc::vec::Vec<ContentId>,             // FIFO eviction (deterministic; evicted ⇒ ⊤ ⇒ stricter)
    high_water: Label,                             // monotone session floor for Ambient mode
    head: ContentId,                               // ReceiptLog head at last admission (the Witness anchor)
    cap: usize, params: ScanParams,
}
impl FlowStore {
    /// Boundary: admit a tool RESULT. Label = channel origin (Untrusted) ⊔ args label.
    /// Also registers any adapter-declared sensitive terms for this output.
    pub fn admit_output(&mut self, bytes:&[u8], channel:ContentId, principal:Option<Did>,
                        args:&Label, readers:Readers, terms:&[&[u8]], anchor:ContentId) -> (ContentId, Label);
    pub fn admit_principal(&mut self, bytes:&[u8], anchor:ContentId) -> (ContentId, Label); // ⊥
    pub fn admit_attested(&mut self, bytes:&[u8], channel:ContentId, signer:Did, anchor:ContentId) -> (ContentId, Label);

    /// THE propagation entry point. Fold over declared ∪ window-found ∪ sensitive-found ∪ (Ambient? high_water),
    /// force ⊤ for any named-but-absent id, admit the payload, emit a self-contained Witness.
    pub fn label_payload(&mut self, bytes:&[u8], declared:&BTreeSet<ContentId>, mode:Mode, anchor:ContentId)
        -> (ContentId, Label, Witness);
    pub fn get(&self, id:&ContentId)->Option<&Label>; pub fn head(&self)->ContentId;
}
#[derive(Clone,Copy,Debug,PartialEq,Eq)] pub enum Mode { Explicit, HighWater } // HighWater = coarse implicit-flow floor
```

`crates/jcp-flow/src/ceiling.rs`:

```rust
/// A grant's flow ceiling — greatest label whose values may exercise the capability.
#[derive(Clone,Debug,PartialEq,Eq,Serialize,Deserialize)]
pub struct FlowCeiling { pub ceiling: Label,
    #[serde(skip_serializing_if="Option::is_none", default)] pub tainted_budget_uj: Option<u64> }
impl FlowCeiling {
    pub fn attenuate(&self, child:&FlowCeiling)->FlowCeiling; // meet on label, min on budget ⇒ amplification unrepresentable
    pub fn effective_budget(&self, grant_uj:u64, l:&Label)->u64;
}
/// Endorsement — signed declassification (PROV-1). Bound to ONE exact (subject,label) pair.
#[derive(Clone,Debug,PartialEq,Eq,Serialize,Deserialize)]
pub struct Endorsement { pub endorser:Did, pub subject:ContentId, pub from_label:ContentId,
    pub to_label:ContentId, pub sig:alloc::vec::Vec<u8> }
```

`crates/jcp-flow/src/replay.rs` — the actual deliverable (PROV-1's verifier):

```rust
pub trait WitnessStore { fn get(&self, id:&ContentId) -> Option<Witness>; }
pub struct ReplayReport { pub verified:usize, pub unjustified_edges:usize, pub ambient_only:usize }
pub enum ReplayError { Chain(usize), WitnessMismatch(ContentId), LabelMismatch(ContentId),
    UnjustifiedEdge(ContentId), FoldMismatch(ContentId), Excised(ContentId), VerdictMismatch(ContentId) }
/// Re-verify a jcp/2+jcp/3 receipt stream against disclosed witnesses. See §4E.
pub fn replay(receipts:&[alloc::vec::Vec<u8>], store:&dyn WitnessStore,
              steward:&str, pk:&[u8;32]) -> Result<ReplayReport, ReplayError>;
```

### 1b. `crates/jcp-schema/src/lib.rs` — two additive, encoding-preserving changes

```rust
pub enum Caveat { /* …6 existing… */
    /// NEW (SPEC §4.9). Flow-dependent: holds()=>true; the real test is the runtime flow gate.
    /// Additive to an externally-tagged enum ⇒ no grant that omits it moves its ContentId
    /// (same property `absent_money_ceiling_does_not_change_the_encoding` pins for budget_funds).
    FlowBelow(jcp_flow::FlowCeiling),
}
impl Caveat { pub fn is_flow_dependent(&self)->bool { matches!(self, Caveat::FlowBelow(_)) } }
// holds(): Caveat::FlowBelow(_) => true (never blocks the caveat path)

pub enum DenyReason { /* …14 existing… */
    TaintedFlow,          // label ⋢ ceiling, or resource floor refuses
    TaintBudgetExceeded,  // tainted sub-ceiling hit
}
// label(): "tainted-flow", "taint-budget-exceeded"

pub struct Grant { /* … */
    #[serde(skip_serializing_if="Option::is_none", default)] pub tainted_budget_uj: Option<u64>, // omit-when-absent
    /* … */ }
```

`Frame` is **not touched** (§5). `jcp-schema` gains a `jcp-flow` dep — acyclic (`jcp-flow` depends only on `jcp-schema`, so put `FlowCeiling` behind a `flow` feature *or* move `FlowCeiling`/`Label` into `jcp-schema` itself to avoid the cycle). **Decision: define `Label`/`Origins`/`Integrity`/`Readers`/`FlowCeiling` in `jcp-schema` (they are pure data types with no logic-heavy deps), and keep `FlowStore`/`Witness`/`replay`/scan in `jcp-flow`.** That removes the cycle cleanly and lets `Caveat::FlowBelow` reference the ceiling without a back-dep.

### 1c. `crates/jcp-runtime/src/lib.rs`

```rust
pub struct Runtime { /* …existing… */
    taint_floor: TaintFloor,                     // NEW — mirrors trust_roots (resource → forbidden origins)
    spent_tainted_uj: HashMap<ContentId, u64>,   // NEW — mirrors spent_minor
}
pub struct TaintFloor { forbidden: BTreeMap<ContentId, Origins>, default_forbidden: Origins }
impl TaintFloor { fn refuses(&self, resource:&ContentId, l:&Label)->bool {
    l.origins().intersects(self.forbidden.get(resource).unwrap_or(&self.default_forbidden)) } }
impl Runtime {
    pub fn forbid_flow(&mut self, resource:ContentId, mask:Origins);      // mirrors trust_root
    pub fn forbid_flow_by_default(&mut self, mask:Origins);               // fail-closed switch (off by default)
    pub fn spent_tainted(&self, gid:&ContentId)->u64;
    // flow-aware entry points; old ones delegate with facts=None (see §5).
    pub fn authorize_flow(&mut self, frame:&Frame, sg:&SignedGrant, caller:Did, now:u64, facts:&FlowFacts)->Decision;
    pub fn charge_flow(&mut self, grant:&Grant, measured:Energy, facts:&FlowFacts, flow_uj:u64)->Decision;
    pub fn decide_flow(&mut self, frame:&Frame, sg:&SignedGrant, caller:Did, cost:Energy, now:u64, facts:&FlowFacts)->Decision;
    pub fn decide_chained_flow(&mut self, frame:&Frame, chain:&[SignedGrant], caller:Did, cost:Energy, now:u64, facts:&FlowFacts)->Decision;
}
// check() gains one private param; it is private, so no public signature moves:
fn check(&self, frame:&Frame, sg:&SignedGrant, caller:Did, now:u64, facts:Option<&FlowFacts>) -> Option<DenyReason>;
```

The gate helpers (private):

```rust
fn ceiling_of(g:&Grant)->Option<FlowCeiling> {
    g.caveats.iter().fold(None,|a,c| match (a,c){
        (a,Caveat::FlowBelow(fc))=>Some(match a{Some(p)=>p.attenuate(fc),None=>fc.clone()}), (a,_)=>a })
}
fn flow_gate(g:&Grant, floor:&TaintFloor, resource:&ContentId, facts:Option<&FlowFacts>) -> Option<DenyReason> {
    if let Some(f)=facts { if floor.refuses(resource,&f.label) { return Some(DenyReason::TaintedFlow); } }
    match (ceiling_of(g), facts) {
        (None,_)                                   => None,                          // today's behaviour
        (Some(_),None)                             => Some(DenyReason::TaintedFlow), // fail CLOSED
        (Some(c),Some(f)) if f.label.leq(&c.ceiling) => None,
        (Some(_),Some(_))                          => Some(DenyReason::TaintedFlow),
    }
}
```

### 1d. `crates/jcp-receipt/src/lib.rs`

```rust
pub const PROFILE_FLOW: &str = "jcp/3";
#[derive(Clone,Debug,PartialEq,Eq,Default)]
pub struct FlowSeal { pub facts: Option<FlowFacts>, pub ceiling: Option<ContentId> } // ceiling digest, if any
fn profile_for(seal:&FlowSeal)->&'static str {              // jcp/2 unless the label is non-⊥
    match &seal.facts { Some(f) if !f.is_bottom() => PROFILE_FLOW, _ => PROFILE } }

pub fn to_jcr1_wire_flow(frame:&Frame, grant:&Grant, decision:&Decision, steward:&str, seal:&FlowSeal)->Value;
pub fn seal_flow(frame:&Frame, grant:&Grant, decision:&Decision, sk:&SigningKey, steward:&str, seal:&FlowSeal)->Vec<u8>;
// verify() gains ONE arm covering {PROFILE, PROFILE_FLOW}; PROFILE_V1 unchanged.
// ReceiptLog::append_flow(frame, grant, decision, seal) — the gateway's new seal call.
```

### 1e. `crates/jcp-policy/src/lib.rs` — optional second gate

```rust
#[non_exhaustive] pub enum Match { /* …4 existing… */
    FlowAbove(Label), OriginIn(BTreeSet<Origin>), IntegrityAtMost(Integrity),
    NotReadableBy(Did),                 // v2 (readers), present now
    Caller(Vec<Did>),                   // closes the noted gap: ctx.caller is sealed but unmatchable
}
#[non_exhaustive] pub struct PolicyContext<'a> { /* …4 existing… */ pub flow: Option<&'a FlowFacts> }
// flow==None ⇒ every flow variant matches false ⇒ byte-identical policy/1 receipts.
```

---

## 2. The propagation rule as unit-testable algebraic law

**The rule, once.** For a payload `p` with witness inputs `W(p)`:

```
label(p) = ⨆{ label(i) : i ∈ W(p) ∩ dom(store) }  ⊔  (⊤ if W(p) ⊄ dom(store) else ⊥)
```

folded **eagerly at admission**, stored under `ContentId::of_bytes(p)`, and accompanied by a self-contained `Witness`. `W(p) = declared ∪ window-found ∪ sensitive-found ∪ (high_water if Mode::HighWater)`.

The deliverable is a `proptest` suite over arbitrary `Label`s and a conformance vector set (so any FL-2 impl is checkable against the *laws*, not just fixtures):

| Law | Statement | Note |
|---|---|---|
| L1 idempotent | `a ⊔ a = a` | |
| L2 commutative | `a ⊔ b = b ⊔ a` | replay need not reproduce fold order |
| L3 associative | `(a⊔b)⊔c = a⊔(b⊔c)` | |
| L4 identity | `a ⊔ ⊥ = a` | ⊥ = degeneracy hook |
| L5 absorbing top | `a ⊔ ⊤ = ⊤` | unknown-id fail-closed |
| L6 order/join | `a ⊑ b ⟺ a⊔b = b` | |
| L7 partial order | reflexive ∧ transitive ∧ **antisymmetric** | antisymmetry needs `Origins::norm`; hence private fields + `try_from` on the wire |
| L8 monotone join | `a⊑a' ∧ b⊑b' ⇒ a⊔b ⊑ a'⊔b'` | |
| L9 no-laundering | `∀ u ∈ ancestors(v). label(u) ⊑ label(v)` | taint never decreases |
| L10 confluence | store labels invariant under any valid topological admission order | eager ≡ lazy fold |
| L11 downward-closed allow | `allow(l) ∧ l'⊑l ⇒ allow(l')` | |
| L12 delegation | `⨅` over a longer chain `⊑` `⨅` over any prefix | amplification unrepresentable (meet) |
| L13 saturation sound | `Set(s) ⊑ Any` | saturation only denies more |
| L14 determinism | `digest(l)` pure; no `HashMap` on any path | |
| L15 refinement | `allow_FL2 ⊆ allow_pre` | never allows what JCP denies today |
| L16 retraction | `Label::from(t).trust() == t`; `l⊑m ⇒ trust(l) ≤ trust(m)` (Data<Control) | one-bit path is a coarsening |
| **L17 carry (fixed)** | verbatim carry of `≥ SCAN_W` bytes ⇒ a `Witnessed` edge exists | now provable: exact `blake3` window match, no rolling-hash bug |
| L18 index over-approx | a fingerprint collision *adds* an origin, never removes one | collisions sound |
| **L19 sensitive-term** | any registered term (any length) appearing verbatim ⇒ a `Witnessed` edge | closes the sub-W gap for registered secrets |
| **L20 witness-fold** | `re-fold(witness.cut, witness.edges) == witness.label` | the replay anchor |

L17's proof is now clean: for a run of ≥ W verbatim bytes, at least one W-byte window is byte-identical between output and args, so its `blake3` fingerprint is equal and lands in the intersection — no dependence on stride/rotate arithmetic.

---

## 3. Where the check slots into `Runtime::decide`'s ordering, and why

**Position: the final step inside `check` (after capability 6b), reached by `decide`/`decide_priced`/`authorize` in one edit; mirrored once in `decide_chained` after its inline trust test (line 432).**

```rust
fn check(&self, frame:&Frame, sg:&SignedGrant, caller:Did, now:u64, facts:Option<&FlowFacts>) -> Option<DenyReason> {
    // 1  frame.trust==Data → UntrustedControl     (UNMOVED, still first)
    // 1b revocations → Revoked
    // 1c root → UntrustedRoot
    // 2  grant binding … 3 subject … 4 verify … 5 expiry … 6 capability      (all unmoved)
    // 6c FLOW — structural property of the arguments, decided before caveats & budget:
    if let Some(r) = flow_gate(&sg.grant, &self.taint_floor, &frame.resource, facts) { return Some(r); }
    None
}
```

Why exactly here — each pinned to something in the code:

1. **After check 1, never before.** `frame.trust==Data ⇒ UntrustedControl` stays byte-first, so conformance pattern 3 (`jcp-conformance/src/lib.rs:953–1008`) and `gen_vectors.rs`'s `deny_f` still name `untrusted-control`. The one-bit **boundary** tag and the **propagated** label are different questions with different reasons.
2. **After check 4 (`verify`).** The ceiling lives inside the grant; judging flow against an unauthenticated grant would seal a provenance verdict over attacker-chosen policy. `check` places 6c well past the signature.
3. **Before caveats (6b in the callers) and before budget (7), therefore before any debit.** A tainted call must cost **zero joules** — the same invariant `tool_poisoning_is_refused_structurally` asserts (`spent==0`). Because 6c is inside `check`, and every caller runs `check` before `caveats_unsatisfied` and before the budget test, `TaintedFlow` returns before `spent_uj.insert` on every path.
4. **`&self`-compatible, one insertion.** `check` is `&self` and shared by all three non-chained entry points; `facts` is *pre-computed by the gateway* and arrives as `Option<&FlowFacts>`, so no fold happens inside the runtime and no public signature moves. The fail-closed backstop `flow_gate(Some(_),None)=TaintedFlow` is the same code — a caller reaching the *old* `authorize` with a *new* ceiling grant is denied, never silently unenforced.

Reason precedence note (honest): a call that violates *both* a plain caveat and the flow ceiling now reports `tainted-flow` rather than `caveat-unsatisfied`. This changes **no** existing vector (no published grant carries `FlowBelow`), and origin-of-data is the more security-relevant fact, so this is a deliberate, documented choice.

`decide_chained` needs its own mirrored insertion because it re-implements the leaf checks inline and never calls `check`; there the ceiling is `chain_ceiling(chain) = ⨅` over every link, so a chain whose links disagree is *stricter* than the leaf — fail-closed by the meet, not by an extra branch. (Note: `decide_chained` still does not evaluate caveats — a pre-existing gap; the `TaintFloor` half *does* apply there, so a delegated call cannot escape the enforcement-point-wide refusal, but a self-attenuating `FlowBelow` on a chained grant is not honoured until that gap is fixed separately. Stated, not smuggled.)

**Why not `charge`.** `charge` takes a bare `&Grant`, no frame/caller/clock, and debits *before* it decides. The flow label is fully known at authorize time (a property of arguments, not execution), so it binds at authorize. Only the tainted **sub-budget** touches `charge_flow` (a real accumulator debit, §4C).

---

## 4. Binding the verdict into the receipt + joule budget, and third-party replay

### 4A. Where it seals — `jcp/3`, on the real gateway path

The gateway seals through `ReceiptLog::append` (jcp/2) today. FL-2 adds `ReceiptLog::append_flow(frame, grant, decision, seal)`. `profile_for(seal)` mints **`jcp/2` byte-for-byte when the label is ⊥**, and **`jcp/3` only when tainted**. `verify` gets one arm for `{PROFILE, PROFILE_FLOW}` recomputing the flow core; `to_jcr1_wire_v2` is retained by subtraction (the exact `jcp/1→jcp/2` precedent at `jcp-receipt/src/lib.rs:41`).

The `jcp/3` flow block (emitted iff `!label.is_bottom()`; all text/uint/array — no bool/null/float, so `cbor_value` accepts it; key order irrelevant, `signed_core_bytes` sorts length-first):

```json
"jcp_receipt": "jcp/3",
"flow": {
  "label":       "<hex Label::digest()>",
  "integrity":   "untrusted|derived|attested|principal",
  "origins":     ["<hex channel id>", …] | "any",
  "readers":     "public" | ["did:key:z…", …],
  "witness":     "<hex Witness::id()>",     // commitment; the artifact is disclosed via WitnessStore
  "ceiling":     "<hex FlowCeiling.ceiling.digest()>",
  "verdict":     "below" | "above",
  "flow_uj":     <uint>,                    // monitor's own metered cost — SEPARATE field
  "flow_energy_provenance": "HwShunt|ModelBased|Estimator"
}
```

This is the answer to F5/F6: the verdict binds where the gateway actually seals (jcp/3 via `ReceiptLog`), not in a `policy/1` that has no emitter, and not as a forbidden field under an unchanged `jcp/2` tag. `cost_uj` keeps its exact meaning (tool energy); `flow_uj` is a sibling with its own provenance (F3 fix).

`policy/1` receives the same fields **only for deployments that run a `PolicyEngine`** (additive, `verify` recovers fields, old bytes unchanged) — a second, optional gate, no longer the primary binding.

### 4B. Consent binds to provenance (FlowDAG/PROV-1 graft)

`context_digest` currently mixes `action ‖ 0x00 ‖ resource ‖ caller ‖ H(content)`. FL-2 appends `label.digest() ‖ witness_id` **only when the label is non-⊥**. Every approval ever minted was over a ⊥-flow call, so **every existing signature verifies bit-for-bit**; going forward, a human's consent is bound to *where the data came from*, so an approval cannot be replayed against the same call carrying differently-sourced arguments. `Endorsement` (signed declassification) is the one-way-ratchet escape hatch, bound to one exact `(subject, from_label, to_label)`.

### 4C. The joule budget — three couplings, all on paths the gateway runs

`Gateway::relay` becomes:

```rust
// Phase 0 — provenance, metered by the same PowerMeter the upstream call uses.
let (facts, tm) = self.meter.measure(|| {
    let declared = parse_declared(&params);                 // optional params._jcp_witness
    let (_id, label, witness) = self.flow.label_payload(&args_bytes, &declared, self.mode, self.log.head());
    self.witness_store.put(witness.clone());                // disclosure store
    FlowFacts { label, witness_id: witness.id(), eval_uj: 0, eval_prov: self.meter.provenance() }
});
let facts = FlowFacts { eval_uj: tm.total_uj(), ..facts };
let frame = mcp_call_frame(grant.id(), &self.server, tool, &args_bytes);

// Phase 1 — authorize_flow: flow gate + tainted sub-ceiling pre-check, no debit.
let auth = self.runtime.authorize_flow(&frame, &sg, self.caller, self.now, &facts);
if !auth.is_allow() {
    let seal = FlowSeal { facts: Some(facts), ceiling: ceiling_digest(&grant) };
    self.log.append_flow(&frame, &grant, &auth, &seal);     // tainted denial sealed, ZERO joules debited
    return Ok(Relayed::Denied { /* … */ });
}

// Phase 2 — metered upstream call (unchanged).
let (response, m) = self.meter.measure(|| up.call(line));
let measured_uj = m.total_uj();

// Phase 3 — charge_flow: debit tool joules AND (if tainted) the tainted sub-accumulator.
let decision = self.runtime.charge_flow(&grant, Energy::measured(measured_uj), &facts, facts.eval_uj);
let seal = FlowSeal { facts: Some(facts), ceiling: ceiling_digest(&grant) };
self.log.append_flow(&frame, &grant, &decision, &seal);

// Phase 4 — the result becomes a labelled source (mcp_result_frame goes live, Trust::Data unchanged).
self.flow.admit_output(response.as_bytes(), mcp_resource(&self.server, tool), None,
                       &facts.label, readers_for(tool), &sensitive_terms_for(tool, &response), self.log.head());
```

1. **Denied flows never debit.** 6c precedes budget/debit; `spent` unchanged on `TaintedFlow` — the exact `tool_poisoning_is_refused_structurally` assertion, extended to taint.
2. **Tainted work gets a smaller wallet — actually wired.** `authorize_flow` pre-checks `spent_tainted(gid) >= effective_tainted_budget` (mirroring the main budget's `remaining==0` degradation at authorize), denying `TaintBudgetExceeded` *before* the call; `charge_flow` debits `spent_tainted_uj` on the allow path. So "20 J clean / 200 mJ once you've touched the web" is a real, enforced control on the gateway path (F8 fix). `replay_spend` gains a `spent_tainted` reconstruction from the sealed `flow` block.
3. **The enforcer prices its own enforcement, honestly.** `flow_uj` (metered `PowerMeter` reading around `label_payload`, with its true `Provenance`) is **sealed as a separate field, not folded into `cost_uj`** (F3 + energy-tag fix). Default: reported, not debited. A deployment may opt to debit it against the tainted sub-budget via a flag; that choice is explicit, never a silent semantic change.

### 4D. Fix the pre-existing `replay_spend` under-count (PROV-1 catch)

`replay_spend`/`aggregate` filter `verdict=="allow"`, but `charge` debits then can return `Deny(CaveatUnsatisfied)` — so today the ledger under-counts by every cost-breached call. Fix both call sites to a debit predicate: `verdict=="allow" || deny_reason ∈ {"caveat-unsatisfied"}`. `tainted-flow` denies at authorize with zero debit, so it correctly stays in the non-debit branch. Ship this as its own commit (it is a real bug independent of FL-2).

### 4E. Third-party replay — receipt **+ disclosed witness** (honest scope, F7 fix)

`store_root` is gone. Replay is not "receipt-alone" (that was FL-1's false claim — `store_root` needed raw bytes). It is **receipt + the witnesses disclosed through a `WitnessStore`**, exactly the `jcp-cite::Citation` disclosure boundary: the receipt commits only `witness_id`; an entitled auditor fetches the `Witness` and rechecks it. Eight ordered checks (the ordering *is* the spec):

1. **Chain** — `verify_log`: `seq[i]==i`, `prev[i]==H(env[i-1])`, genesis `0…0`. Profile-agnostic; a mixed `jcp/2`+`jcp/3` stream verifies end-to-end unchanged.
2. **Witness binding** — `Witness::id() == receipt.flow.witness`.
3. **Label binding** — `witness.label.digest() == receipt.flow.label`.
4. **Edge justification** — each `Witnessed` edge's `grams ⊆ windows(parent) ∩ windows(subject-cut-node)` (rechecked from the disclosed cut). `Declared` edges require a named artifact (a `jcp-cite` citation or `Endorsement`) to verify. `Ambient` edges are free-but-flagged.
5. **Fold correctness** — re-fold `witness.cut` over `witness.edges`; assert `== witness.label` (safe in any order by L2/L3). This is **L20**.
6. **Cut completeness (anti-excision)** — every `cut[j].anchor` must appear at a *strictly earlier* index in the already-verified chain. Dropping the tainting read breaks the chain at that point; step 1 catches the excision and step 6 catches reordering. *You cannot remove the untrusted read without breaking the chain.*
7. **Verdict determinism** — re-evaluate `witness.label.leq(&ceiling)` against the sealed `flow.ceiling`; assert `== receipt.flow.verdict`. Pure, no clock, no LLM.
8. **Energy reconciliation** — `Σ flow_uj` and `Σ` tainted debits reconcile against the corrected `replay_spend`.

`ReplayReport` separately counts `unjustified_edges` and `ambient_only` verdicts, so an auditor can grade how much of a verdict rested on hard bytes versus the conservative floor — the on-wire evidence/floor distinction grafted from PROV-1/FlowDAG.

**Honest limit stated inline:** step 4 rechecks *consistency* (grams ⊆ the disclosed cut's own window sets), not *truth* against the original bytes, unless the `WitnessStore` also discloses boundary bytes to the entitled auditor (a second disclosure tier). Against a fully-adversarial prover that under-populates a cut node's evidence, truth-verification requires disclosing the boundary bytes; that tier is available but off by default (it widens the disclosure surface). This is the PROV-1-security-judge concern, addressed by making the tier explicit rather than pretending consistency = truth.

---

## 5. Backward-compatibility for the one-bit `Trust::Control/Data` path

The one-bit path is a **fixed point**, enforced by construction, not by care.

1. **`Frame` untouched.** It has no `skip_serializing_if` and no `impl` — any field is a hard wire break. FL-2 keys labels by `ContentId` (already how a frame names its payload) in a `Gateway.flow: FlowStore` side-store. Frame content ids, `Caveat::PayloadIs` bindings, every cross-language verifier: bit-unaffected.
2. **`Trust` embeds and retracts (L16).** `From<Trust> for Integrity`: `Control↦Principal`, `Data↦Untrusted`; `Label::trust()`: `Untrusted↦Data`, else `Control`. `Label::from(t).trust()==t`, and `l⊑m ⇒ trust(l)≤trust(m)` under `Data<Control`. The one-bit tag is exactly the coarsening; FL-2 refines, never contradicts. `Trust`'s definition/derives/serde are unchanged.
3. **Check 1 stays first and unchanged**, position 6 in `decide_chained`. Every `Trust::Data` frame is denied `untrusted-control`, same position, whether or not flow is configured.
4. **Grants without a ceiling behave exactly as today.** `ceiling_of(g)=None`, `TaintFloor` default-open ⇒ `flow_gate` is a no-op. Adding `Caveat::FlowBelow` to an externally-tagged enum changes the encoding of no grant that omits it (`absent_money_ceiling_does_not_change_the_encoding` precedent), so every published grant keeps its `ContentId`.
5. **The honest compat pair (F2 fix — replaces FL-1's false equivalence law).**
   - **Compat law:** `ceiling_of(g)==None ⟹ ∀ facts. flow_gate(g,·,·,facts)==None` — ceiling-free grants are a no-op for *any* facts, including `None` and `Some(bottom)`. Byte-identical verdicts and receipts. Every grant that exists today is ceiling-free, so *every* existing deployment is unaffected.
   - **Fail-closed law:** `ceiling_of(g)==Some(_) ∧ facts==None ⟹ flow_gate==TaintedFlow`. An un-migrated caller (old `authorize`) handed a *new* ceiling grant is denied, never silently unenforced.
   - `Some(bottom)` (provenance computed, clean) allows against a ceiling; `None` (provenance not computed) fails closed. These are **different inputs and should differ** — that is the resolution of FL-1's contradiction. A *pre-FL-2 binary* is stricter still: serde cannot deserialize the unknown `FlowBelow` variant, so the grant fails to parse and the call is denied. Every direction of version skew fails closed.
6. **Receipts.** `to_jcr1_wire` untouched; `jcp/3` minted only when tainted; `verify_log` reads only `seq`/`prev`; `ReceiptCore` gains `flow: Option<FlowReceipt>` (`None` on legacy, exactly as `payload_hash: None` documents for `jcp/1`). `published_v1_receipts_still_verify` and every `jcp/2` fixture unchanged.
7. **Refinement (L15).** 6c is inserted after all existing checks and can only return `Deny`. `allow_FL2 ⊆ allow_pre`: FL-2 never allows a call JCP denies today. Worst case is over-denial — the correct direction for a reference monitor.
8. **`jcp-policy` is the one honest semver-major** (`#[non_exhaustive]` on `Match`/`PolicyContext` + a `flow` field). `ctx.flow==None` ⇒ every flow variant matches false ⇒ no new denies, byte-identical `policy/1`. Do it in one release; `#[non_exhaustive]` now makes it the last such break. `Match::matches` is private, so widening it is free.

---

## 6. Concrete test list

**Lattice laws (proptest + conformance vectors):** `l1_idempotent` … `l20_witness_refold`, one test each per §2, shipped as vectors in `jcp-conformance`.

**Carry detector (F1 regression):**
- `carry_at_least_w_bytes_is_found` — a ≥16-byte verbatim run yields a `Witnessed` edge (L17). Directly replaces FL-1's broken buzhash guarantee.
- `blake3_window_index_is_platform_independent` — same bytes ⇒ same fingerprint set on two arches.
- `registered_sensitive_term_of_any_length_is_found` — an 11-char SSN registered by an adapter yields a `Witnessed` edge (L19).
- `sub_w_unregistered_carry_is_NOT_found` — a 12-byte unregistered token produces `⊥` from the scan alone; **documents the residual** so it can never be mistaken for a guarantee.

**Compatibility (F2/F3/F5/F6):**
- `bottom_flow_call_is_byte_identical_to_pre_fl2` — clean frame ⇒ `jcp/2` bytes, COSE envelope, `prev`, and `context_digest` identical to today. (F3: because `flow_uj` is jcp/3-only, `cost_uj` is unmoved.)
- `ceiling_free_grant_is_a_noop_for_any_facts` — the compat law, over `None`/`Some(bottom)`/`Some(tainted)`.
- `ceiling_grant_on_old_authorize_fails_closed` — the fail-closed law.
- `pre_fl2_binary_rejects_flowbelow_grant` — serde parse failure ⇒ deny.
- `published_v1_and_v2_receipts_still_verify` — mixed `jcp/1`+`jcp/2`+`jcp/3` chain verifies end-to-end.
- `absent_tainted_budget_does_not_change_grant_id`.

**Budget couplings (F8):**
- `tainted_flow_deny_debits_zero` — the `tool_poisoning` assertion, for `TaintedFlow`.
- `tainted_sub_ceiling_pre_checks_at_authorize` — `spent_tainted >= cap` ⇒ `TaintBudgetExceeded` before the upstream call.
- `charge_flow_debits_spent_tainted` — the accumulator actually accrues on the allow path (kills TAS's "accumulator stays 0" defect).
- `flow_uj_sealed_separately_with_own_provenance` — `cost_uj` unchanged; `flow_uj`/`flow_energy_provenance` present.

**Replay (F7):**
- `replay_refolds_witness_to_sealed_label` (L20).
- `excised_untrusted_read_breaks_the_chain` — remove the admission ⇒ `ReplayError::Chain`/`Excised` (cut-completeness).
- `unjustified_witnessed_edge_is_rejected` — grams not ⊆ endpoints ⇒ `UnjustifiedEdge`.
- `ambient_only_verdict_is_flagged_in_report` — evidence-vs-floor grading.
- `mixed_profile_stream_replays` — jcp/2 and jcp/3 interleaved.

**The multi-tool-call attack the security judges constructed (named `read_summarize_send_exfil`):**
The judges' canonical attack across the four designs is the *derived-from-untrusted-read exfiltration*: an agent reads an attacker-controlled source, then egresses attacker-chosen data two calls later, and `ContentContains` structurally cannot express the deny. FL-2's positive test:
- `read_email_then_send_email_denies_on_verbatim_carry`:
  1. `checkpoint`/principal turn at ⊥.
  2. `read_email` (attacker sender) → `admit_output` labels the result `(Untrusted, {Origin{channel=mcp_resource("mail","read_email"), principal=attacker}}, Public)`, indexes its windows, registers the exfil URL as a sensitive term.
  3. `summarize` (clean tool) → its args carry ≥16 verbatim bytes of the email → `label_payload` finds a `Witnessed` edge to the read; the summary is admitted tainted.
  4. `send_email(to=attacker, body=<summary>)` under a grant with `Caveat::FlowBelow{ ceiling: (integrity=Principal, origins=∅, readers=Public) }` → `send_email`'s args reach `Origin{mail.read_email, attacker}`, `label ⋢ ceiling`, 6c returns `TaintedFlow`, **zero joules debited**, `jcp/3` seals the `flow` block naming the origin, and the disclosed `Witness` lets a third party re-derive the deny. Assert: verdict `above`, `spent==0`, `verify` round-trips, `replay` re-folds.
- `send_money_recipient_must_reach_principal` — the banking shape: a `FlowBelow` ceiling requiring the recipient origin to be `Principal`; a recipient derived from a tool output is denied.
- `laundering_defeats_witness_but_high_water_holds` — the *negative* companion: base64/paraphrase the body so no window matches; assert the scan alone returns `⊥` (documents the residual), then assert `Mode::HighWater` on the egress sink denies via the session floor. This test exists precisely to prevent overclaiming §7.
- `short_account_number_needs_registration` — a 12-digit account number copied verbatim is caught **only** when the banking adapter registered it as a sensitive term; without registration it is invisible. Documents the F1 residual as a test, not a footnote.

---

## 7. What this still does not stop (honest residuals)

1. **Semantic laundering.** Base64, translation, summary-in-other-words, "spell the address with spaces" — all defeat the window index by construction. Against those, soundness rests on (a) harness declaration, (b) registered sensitive terms, or (c) `Mode::HighWater`'s coarse session floor. A monitor at the tool-call boundary cannot see the model's derivation; CaMeL sidesteps this only by owning the interpreter. This is the NeuroTaint thesis and FL-2 concedes it. **Accepted residual.**
2. **Sub-`SCAN_W` unregistered secrets.** An account number (8–16 chars) or bare email that is *not* registered by a boundary adapter and is below the 16-byte window floor is invisible to the monitor's own scan. Registration (L19) and declaration close it when a tool knows a field is sensitive; the fully-general case needs a sensitivity oracle JCP does not have. **Accepted residual, tested (`sub_w_unregistered_carry_is_NOT_found`).**
3. **Confidentiality (Readers) enforcement is v2.** `Readers` has correct algebra and is sealed, but JCP has no ACL model, so `readers_for(tool)` defaults to `Public` and the readers component is inert everywhere until per-tool audience oracles exist. v1 is **integrity × origins** only. The PROV-1-security-judge's readers-exfil (a restricted secret egressing with a clean verdict) is *not* solved in v1; the hook (`Match::NotReadableBy`, `permits(audience)`) is wired so v2 is additive. **Scoped, not claimed to work.**
4. **Implicit flows beyond `HighWater`.** No AST/interpreter, so branch-condition and loop-iterable dependencies are invisible; `Mode::HighWater` is a blunt over-approximation (everything after the first untrusted read joins the session label) that collapses utility within a few calls. Sound, not precise. **Accepted; opt-in per sink.**
5. **Replay is receipt + disclosed witness, and step-4 is consistency not truth against a hostile prover** unless boundary bytes are disclosed (second tier, off by default). Stated inline in §4E. **Accepted, explicit tier.**
6. **`FlowFacts` is in-process and unsigned** — it travels as a Rust argument from gateway to runtime; nothing binds it into the `Frame`. Fine in-process; the moment JCP goes cross-process over `jcp-wire`, the facts (or the `witness_id`) must ride the frame or a signed sidecar — the `Frame` wire break FL-2 deliberately avoids for now. **Deferred, not eliminated.**
7. **Boundary labellers are TCB.** Which channel/principal produced a byte, and which fields are sensitive, is ordinary adapter code with ordinary bugs; one adapter that mislabels an attacker sender as `Attested` is a silent bypass. The lattice laws (L1–L20) prove taint never decreases, authorization is downward-closed, delegation is monotone, and the verdict is reproducible — **none of them says "prompt injection cannot succeed."** Stating soundness precisely is not the same as being secure, and FL-2 says so rather than letting the algebra imply otherwise.
8. **Inherited non-goals** (CaMeL §3.1 / AuthGraph): pure text-to-text manipulation with no tool call, same-source poisoning (the attacker poisons the *authorized* channel's backend so the value legitimately carries the expected label), "read the email and do what it says" as a legitimate user instruction, and the ROP-style approximation of a denied call out of many allowed ones.

---

### Files to create / touch (all absolute)

- **New:** `/Users/dcharlot/data-share/vibe-coding/open-standards/jcp/jcp-rs/crates/jcp-flow/{Cargo.toml,src/{lib.rs,store.rs,witness.rs,replay.rs}}` (store/witness/scan/replay).
- **Edit `jcp-schema`** `/…/crates/jcp-schema/src/lib.rs`: define `Label/Origins/Integrity/Readers/FlowCeiling/Endorsement` here (breaks the dep cycle), add `Caveat::FlowBelow`, `DenyReason::{TaintedFlow,TaintBudgetExceeded}`, `Grant.tainted_budget_uj`.
- **Edit `jcp-runtime`** `/…/crates/jcp-runtime/src/lib.rs`: `check` gains `facts`; add `taint_floor`, `spent_tainted_uj`, `flow_gate`/`ceiling_of`/`chain_ceiling`, `authorize_flow`/`charge_flow`/`decide_flow`/`decide_chained_flow`, `forbid_flow*`; mirror 6c in `decide_chained`; fix `replay_spend`/`aggregate` debit predicate.
- **Edit `jcp-receipt`** `/…/crates/jcp-receipt/src/lib.rs`: `PROFILE_FLOW="jcp/3"`, `FlowSeal`, `to_jcr1_wire_flow`/`seal_flow`/`ReceiptLog::append_flow`, `to_jcr1_wire_v2` retention, one `verify` arm, `ReceiptCore.flow: Option<FlowReceipt>`.
- **Edit `jcp-gateway`** `/…/crates/jcp-gateway/src/lib.rs`: add `flow: FlowStore`, `witness_store`, `mode`; the Phase 0–4 relay above; add `jcp-flow` to its `Cargo.toml`.
- **Edit `jcp-policy`** `/…/crates/jcp-policy/src/lib.rs`: `#[non_exhaustive]` + new `Match` variants + `PolicyContext.flow` + `context_digest` provenance append.
- **Edit `jcp-bridge`** `/…/crates/jcp-bridge/src/lib.rs`: no signature change — `mcp_result_frame` (currently dead, `:54`) goes live from the gateway, still `Trust::Data`.