What
The kernel's core safety property — no claimant-authored byte flows into the verdict — is today enforced by construction plus AST-pinned tests (believe_under_floor ignoring forgeable read-backs, admissible_under_floor's floor conjunction, the vendor-agnostic pins). This issue is the upgrade from "pinned by tests" to "machine-checked property": state it as an information-flow / non-interference property over the pure verdict core — reward.admit, overlap_policy.admissible_under_floor, improve.classify — and check it mechanically in CI.
Two candidate mechanizations (the plan should pick one and say why):
- Taint-style static pass over the pure modules: classify each input field as claimant-authored vs env-authored at the dataclass level, then verify by data-flow analysis that the admit/keep bit is computed only from env-authored fields (claimant fields may flow to display strings only).
- A small formal model (TLA+/Lean) of the admit lattice with the floor-conjunction theorem (
admit ⟺ floor ∧ policy can only refuse-more) and the non-interference statement, with the Python kept in sync by the existing byte-parity tests.
Why
The conjunctive-floor and zero-author-bytes arguments are the load-bearing claims of the whole substrate (docs/138/234); a mechanized check turns them from prose + pins into a property a skeptical reader can re-run. Scope honestly: the property covers the pure core, not the boundary readers — the boundary threat model stays #35/#107 territory and the doc must say so.
Done-condition
A CI job that fails when a claimant-authored field reaches a verdict computation in the covered modules (demonstrated by a deliberately-broken fixture), plus a docs/NN plan section stating exactly which modules and which fields the property covers.
Lane guess
verify-action/ci for the job, src for any field-classification metadata, docs for the plan.
Found while auditing which of the kernel's floor guarantees are enforced by construction vs merely pinned — this is the highest-leverage one to mechanize.
What
The kernel's core safety property — no claimant-authored byte flows into the verdict — is today enforced by construction plus AST-pinned tests (
believe_under_floorignoring forgeable read-backs,admissible_under_floor's floor conjunction, the vendor-agnostic pins). This issue is the upgrade from "pinned by tests" to "machine-checked property": state it as an information-flow / non-interference property over the pure verdict core —reward.admit,overlap_policy.admissible_under_floor,improve.classify— and check it mechanically in CI.Two candidate mechanizations (the plan should pick one and say why):
admit ⟺ floor ∧ policycan only refuse-more) and the non-interference statement, with the Python kept in sync by the existing byte-parity tests.Why
The conjunctive-floor and zero-author-bytes arguments are the load-bearing claims of the whole substrate (docs/138/234); a mechanized check turns them from prose + pins into a property a skeptical reader can re-run. Scope honestly: the property covers the pure core, not the boundary readers — the boundary threat model stays #35/#107 territory and the doc must say so.
Done-condition
A CI job that fails when a claimant-authored field reaches a verdict computation in the covered modules (demonstrated by a deliberately-broken fixture), plus a
docs/NNplan section stating exactly which modules and which fields the property covers.Lane guess
verify-action/cifor the job,srcfor any field-classification metadata,docsfor the plan.Found while auditing which of the kernel's floor guarantees are enforced by construction vs merely pinned — this is the highest-leverage one to mechanize.