open-standards/jcp/jcp-rs/crates/jcp-schema/FLOW_LATTICE_PLAN.md

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:

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):

/// 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):

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:

/// 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):

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

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

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):

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

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

#[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 Labels 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).

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):

"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:

// 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.