Obligation 2.3 of the proof map (#84), Tier 2.
Property: sensor/hardware handles are acquired and released exactly once — no leak, no use-after-release, no double-release at the logical level. This is a linearity property.
Where: sensors, neurophone-core.
Vehicle: affine typing (AffineScript) — the strongest candidate for static, compile-time proof rather than runtime tests. Encode handles as affine/linear resources so misuse is a type error.
Part of #84.
Obligation 2.3 of the proof map (#84), Tier 2.
Property: sensor/hardware handles are acquired and released exactly once — no leak, no use-after-release, no double-release at the logical level. This is a linearity property.
Where:
sensors,neurophone-core.Vehicle: affine typing (AffineScript) — the strongest candidate for static, compile-time proof rather than runtime tests. Encode handles as affine/linear resources so misuse is a type error.
Part of #84.