Inside a proof: how the verifier narrows what your query could mean
Pick a query. Step through it clause by clause. Watch every possibility the verifier rules out — until what remains is a tight proven bound. This is the mechanism behind every tier verdict you see in the playground.
- T5provenT7proven
Orders: nullable key → bounded
Watch nullability ⊗ interval inference narrow x: integer | null down to x: integer ≥ 0 (per id), clause by clause.
Open trajectory →
- T8proven
PII flow: any sink → consented-marketing only
Information-flow tracking from raw_users down to a policy bounded by marketing consent ∧ post-opt-in.
Open trajectory →
- T6provenT7proven
Cardinality: unbounded → ≤ |distinct(order_id)|
Row-count abstract interpretation: ⊤ → |orders| → |gold customers' orders| → |distinct order_id|.
Open trajectory →