measure(model-grounded-detection): the entailment ceiling is 2.2%, and it is depth not a wall

The analogue of the candidate ceiling, one rung up: not "can a site be
enumerated" (96.6%) but "can a deterministic abstract-interpretation model
DECIDE the vulnerability without trusting the LLM". Offline, no model calls.

  model_entailed today                2.2%  (2/92 web/logic pairs)
  model_corroborated, one-hop taint    24%  (22/92)
  taint reachable, multi-hop           35%  (26/74 flow families)
  candidate site enumerable          96.6%  (for comparison)

The gap between 96.6% and 2.2% is the gap between enumerating and arbitrating,
and it is the finding. The model cannot be a pure arbiter at v1. But the
measurement diagnoses depth, not impossibility: one-hop source resolution
(real taint sits 1-3 binds upstream: q = '...'+id; execute(q)), a closed
literal sink table (misses project wrappers and path/xss/prototype sinks), and
a function-naming gap that eats 20/50 injection pairs. Deepening the taint to
the candidate enumerator's depth-4 chain already moved injection 24% -> 48%.

So the course is a layered arbiter, not a pure one: report model_entailed
where the model proves it (deterministic, no LLM); let the LLM judge but check
its claim against the resolved taint on the ~35% corroboration band (noise
removed there); honest suspicion for the rest, which is where the deferred
execution/differential tier earns its place. Modeling confirmed as abstract
interpretation; SMT reserved for the memory/C tier; concolic avoided.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG

.kiro/specs/model-grounded-detection/brief.md

@@ -122,6 +122,36 @@ Two properties are the whole point:
   model rather than averaged over runs. The LLM stops being the oracle and becomes a proposer the model
   audits.
 
+**Measured, 2026-09-08 — the entailment ceiling** (`benchmarks/measurements/2026-09-08-model-entailment-ceiling.json`,
+offline, no LLM):
+
+| rung | web/logic taxonomy | for comparison |
+|---|---|---|
+| `model_entailed` today | **2.2%** (2/92) | — |
+| `model_corroborated`, one-hop taint | **24%** (22/92) | — |
+| taint reachable, multi-hop (flow families) | **35%** (26/74) | — |
+| candidate site enumerable | — | **96.6%** (constrained-detector group 1) |
+
+The gap between 96.6% (a site exists) and 2.2% (the model *decides* the vulnerability) is the gap between
+enumerating and arbitrating, and it is the whole finding. The model cannot be a *pure* arbiter at v1. But it
+is not a wall — the measurement diagnoses depth, not impossibility: one-hop source resolution (real taint sits
+1–3 binds upstream: `q = "…" + id; execute(q)`), a closed literal sink table (misses project wrappers and the
+path/xss/prototype sinks), and the function-naming gap that eats 20/50 injection pairs as `no_function`.
+Deepening the taint to reuse the candidate enumerator's depth-4 chain already moved injection 24% → 48%.
+
+So the architecture the numbers support is a **layered arbiter**, not a pure one:
+
+- where the model **entails** — report `model_entailed`, deterministic, the LLM not needed;
+- where the model **corroborates a taint path** (~35% and rising) — the LLM judges, but its claim is *checked*
+  against the resolved path, so run-to-run noise is removed on this band;
+- where the model can only **enumerate** (the rest, up to 96.6%) — honest `suspicion`, the LLM proposes with
+  no deterministic backstop, and this is exactly the band where the deferred execution / differential tier
+  earns its place.
+
+Pure `model_entailed`-as-arbiter is the north star. The v1 is the layered arbiter, and the near-term work is
+named by the measurement: fix function naming, build per-family sink/sanitizer tables, and lift the flow
+model onto the multi-hop binding chain we already have.
+
 This is the classical SAST arbiter — dataflow / abstract interpretation, the CodeQL and Infer lineage —
 with the LLM supplying the semantic judgement the model is weakest at (aliasing intent, whether a value is
 really untrusted, whether a guard really covers the case). It does not need soundness. A partial model that