Plato Data-Flow Lens

The story — what changes for Lukasz

Lukasz holds a path in his head: “a captured payload comes in, gets validated, deduped, written as a log entry.” His exact words: “I’m always not sure if the path I have in my mind is the only path — sometimes the data goes a different way because of an edge case, and without reading every method I can’t say 100% the flow I imagine is correct.”

Today Plato can tell him module A imports module B. It cannot tell him a value of type CapturedPayloadRequest moves from the ingest endpoint, through the validator, to a CaptureLogEntry in the database — and here are the three places it can branch off that path. That second thing is the data-flow lens.

The honest boundary is the product. Plenty of tools draw flow diagrams that quietly lie — they show a clean path and silently drop the branch they couldn’t follow, which is worse than nothing because it looks complete. Plato’s flow lens is the first one that, every time it cannot follow the value, says so by name instead of dropping the branch or guessing.

This turns Lukasz into an architect with a blueprint: he stops reading every method to be sure, and starts reading only the spots Plato fenced. The tool and his number one priority are the same arrow.

Decisions locked

The foundational choices — everything below is built to these.

Engine

Ride the existing world model

A value-flow edge is a sibling of the import edge Plato already extracts. The lens inherits currency proof, fail-closed fencing, and honest-result discipline for free — we are not writing a second Plato.

Honesty floor

Prove or fence — never drop

Every drawn edge is a real value move it proved. Every blind spot is a named fence. There is structurally no probably-flows-here. This is the entire reason to build inside Plato instead of buying a flow tool.

First proof

One real object, one real pipeline

Succeed only if it surfaces a path Lukasz didn’t know existed — confirmed by him, out loud. A diagram that only redraws his mental model is a null result and we say so.

Substrate

SCIP graph (C#) — honest split

The walk and finding union ride verified existing code. The value-flow edge extractor is net-new and currently unfed on C# — the adapter drops locals today (Call 0). The verified-walk credibility does NOT extend to the unbuilt extractor.

Your calls — all resolved 2026-06-29

All four calls resolved by Robert on 2026-06-29. Resolution shown in green in each card.

0 ★

Call 0 (build-blocking) — how fine can the first Prism trace honestly go?

The spec’s proven tier assumes Plato can see value-moves inside a method. Today it cannot on C#: the SCIP adapter silently drops every local symbol (scip-core/index.mjs:142 — a bare continue, not even a fence). So before any build, Step-0 probes what the C# index actually supplies for intra-method flow, and we never let a dropped local be silent — it becomes a named fence (SCIP_FLOW_GRANULARITY).

Why it matters: this is the gap the lens exists to prevent, sitting in the lens’s own foundation. A within-method branch through a local would be silently absent and read as complete. It also decides how rich the first Prism trace can be.

Option A (recommended): probe the C# index first. If it carries local Write/Read occurrences (the symbol_roles bits at scip-core:39, currently unused), build the C# intra-method extractor → fine-grained Prism trace day-one. If it does not, fence C# to method-granularity.

Option B: build the fine-grained extractor on the TS path first (Plato itself), prove the lens at full granularity, then port to C#. Richer first trace, but the first proof is not on Prism.

The floor, either way: a dropped local is never silent — it fences by name.

RESOLVED (Robert, 2026-06-29) → A. Probe the C# index first; build the finest granularity it honestly supplies; a dropped local always fences by name (SCIP_FLOW_GRANULARITY), never silent.

1 ★

Call 1 — the soundness floor: virtual/interface dispatch handling.

Day-one, the lens proves value flow inside one function soundly, and follows the value across a call only when the graph already resolves that call to exactly one target. Every other boundary becomes a named fence, not a guessed edge.

Why it matters: the lock-in decision. Set the floor too high (chase every dispatch) and we re-run the 17-cycle reactive-patching scar. Set it too low and the lens is a toy. The field widens to could-be-anywhere; Plato fences by name instead — honest and actionable.

Option A (recommended): intraprocedural-sound + single-resolved-target cross-call + fence everything else. Ships in days; honest on day one.

Option B (candidate-set fence): virtual/interface dispatch resolves to a candidate-set — the N type-compatible targets from the class hierarchy, shown as labeled UNPROVEN candidates, never a proven edge. Not the multi-week full CHA precision build.

Option C: full points-to / taint-grade interprocedural analysis. Out of scope permanently for the honest-core.

↘ go deeper — the soundness boundary contract (Layer 2)

PROVE rows (intraprocedural def-use + single-resolved cross-call):

Local assignment var x = source; within one method
Parameter pass / return value, across a call resolved to exactly one target
Field/property write entry.Url = req.Url; within one method
Constructor / object-initializer new CaptureLogEntry { Url = req.Url }

FENCE rows (named top):

DISPATCH_UNRESOLVED — virtual/interface call to more than 1 possible target; carries a candidates: [...] payload (N type-compatible targets, labeled UNPROVEN) when the class hierarchy is available; else blank. Call 1 → B (candidate-set form).
TYPE_ERASED — value cast to object/dynamic/var losing T
ALIASED_MUTATION — mutation through shared/aliased reference
UNRESOLVED_CALL — call SCIP could not resolve at all
ADAPTER_CANNOT_SUPPLY — reflection / serialization / EF materialization
SCIP_FLOW_GRANULARITY — intra-method local dropped by adapter (Call 0)

RESOLVED (Robert, 2026-06-29) → B, as a candidate-set fence (not the multi-week precision build). A virtual/interface dispatch is never a guessed single path and never a blank wall — it resolves to a candidate-set: one of these N type-compatible targets, enumerated from the class hierarchy, shown as labeled UNPROVEN candidates (a named, enumerated top), never a proven edge. Substrate dependency (a Call-0-style probe): the candidate list needs the C# index to supply implements / type-hierarchy relationships (SCIP relationships); Step-0 checks it — present → show the candidate-set; absent → fall back to the blank DISPATCH_UNRESOLVED fence. Honest in both forms: show the doors, assert none.

Call 2 — the experiment’s success bar.

The experiment succeeds iff the traced flow surfaces at least one real value path (or one named blind spot at a real branch) that Lukasz did not already have in his head — confirmed by Lukasz, out loud, on a recorded walk-through. A diagram that only redraws his mental model is a null result, logged as such.

RESOLVED (Robert, 2026-06-29) → confirmed. The success bar stands: his knowledge moves (at least 1 proven path OR at least 1 fence at a real branch he did not hold), or it is a logged null.

Call 3 — standing Plato lens, or Prism-only probe until proven?

Build it as a Prism-scoped probe first (one object type, one pipeline), and only promote it to a general Plato lens (any repo, any object type, over MCP) after the experiment clears Call 2’s bar.

Recommendation: probe first, promote on evidence. Protects against pouring a general build into a lens the one real user doesn’t pull.

RESOLVED (Robert, 2026-06-29) → confirmed. Prism-scoped probe first; promote to a standing Plato lens only on evidence.

What could go wrong

The over-claim trap

A flow graph that silently drops a branch reads as complete and lies — the same false-green Plato fights on reachability. Guard: the lens emits findings through the exact same two-kind union the Tribunal uses. A dropped branch is structurally impossible.

A fake edge

Showing a value move that doesn’t happen. Guard: an edge is drawn only on a proven assignment/parameter-pass/return within a function, or a single-resolved cross-call. Anything weaker fences. The degenerate-control gate (a gutted flow engine) MUST FAIL the planted-path fixture.

Cry-wolf (all-fenced)

If 99% fences, it’s noise like the 99.6%-fenced Neuron run. Guard: the experiment’s success bar (Call 2) is signal, not coverage. If the one real pipeline comes back all-fenced, that’s a measured null and a redirect signal.

Substrate gap (Call 0 teeth)

The C# adapter today drops every local symbol silently at line 142. A within-method branch through a local would be absent and read as complete. Guard: SCIP_FLOW_GRANULARITY fence is mandatory — never draw, never drop silently; probe first, build to the honest granularity the index supplies.

How we’ll know it works — the experiment

Point the lens at CapturedPayloadRequest in de-prism-api. It traces the value from the ingest endpoint through BatchPayloadValidator → PayloadDeduplicator → CaptureLogWriter → the CaptureLogEntry canonical entity, draws every value-move it can prove, names every branch it can’t follow, and Lukasz confirms it showed him a path he didn’t have.

Degenerate-control gate. A gutted engine (__gutFlow seam) draws zero edges. It MUST then FAIL a planted-path fixture (a hand-authored 3-hop value flow it is required to find). A flow engine that can’t go red on a deliberate break is vacuous and FAILS.
Cry-wolf gate + pre-commitment. The clean pipeline must not return all-fenced. Because the substrate gap (Call 0) makes a fence-heavy first run likely, success is pre-committed: an all-fenced OR SCIP_FLOW_GRANULARITY-dominated trace is a NULL/redirect, NOT a win. The win must be a proven path or a fence at a REAL branch Łukasz did not hold.
Adversary fixture (substrate-gap teeth). A method with a real intra-method branch through a dropped local — the walk MUST fence it SCIP_FLOW_GRANULARITY (never draw, never silently drop), proving the gap is named, not hidden.
Lukasz confirms (Call 2 bar). He sees at least one path or named blind spot he did not have in his mental model — confirmed out loud, on a recorded walk-through. Null result is logged, not hidden.

↘ go deeper — Layer 2: frontier brief, build sequence, file paths

Problem class (named abstractly): object-centric value-flow reachability with an honest unknown — for a named type T, compute the set of program points a value of T provably reaches, where every point not provably reachable-or-unreachable is an explicit top-element (a named unknown), never a silent omission and never a guess.

Field citations: dataflow analysis = abstract interpretation over a lattice with a top element [absint-lattice: UW-Madison CS704]. Intraprocedural + conservative interprocedural seam is the canonical decomposition [callgraph-framework: Grove and Chambers, TOPLAS]. The discipline has a name in the field: soundiness — Livshits, Sridharan, Smaragdakis et al., In Defense of Soundiness: A Manifesto (CACM 2015): every practical analyzer is unsound; the obligation is naming your deliberately-unsound subset, not hiding it. Plato’s FlowBlindAxis is that named subset [soundiness: Livshits et al., CACM 2015].

Call 1 candidate-set mechanic (DISPATCH_UNRESOLVED): when the C# index supplies type-hierarchy relationships (SCIP relationships), the fence carries a candidates: [valueSite...] payload — the N type-compatible dispatch targets, labeled UNPROVEN. This is the enumerated top: show the doors, assert none. When the hierarchy is absent, falls back to blank DISPATCH_UNRESOLVED. validateFinding still forbids any confidence/score field on either form.

New primitives (riding existing world model):

value-flow edge type — { kind: 'value-flow', type, from, to, via: 'assign'|'param'|'return'|'field-write'|'ctor' }
FlowBlindAxis frozen enum — members: DISPATCH_UNRESOLVED (optionally with candidates payload per Call 1 candidate-set), TYPE_ERASED, ALIASED_MUTATION, UNRESOLVED_CALL, ADAPTER_CANNOT_SUPPLY, SCIP_FLOW_GRANULARITY
flowWalk(repo, typeName, opts) — BFS walk; output: { provenPaths, fences, pin, currencyProof }

Files: src/flow/value-flow-edge.mjs, src/flow/flow-blind-axis.mjs, src/flow/walk.mjs, harness/flow/planted-path-fixture.mjs. Gate: extend scripts/gate.sh with flow-degenerate leg + flow-cry-wolf leg.

Build sequence: Frontier DONE (this spec). Next: Build (Workflows, Claude agents only) → Measure (recompute path/fence counts from raw) → Adversarial-verify (independent break attempt).