feat(L10): add propositional state-machine theorems for linearity (A3)

Closes PROOF-NEEDS §P0.2.  The existing `NoDoubleFree` is a nullary
marker — documentation-as-data — that asserts QTT's structural
guarantee without producing a theorem a caller can hand to another
proof.  This change ADDS a witness-manipulating propositional layer
alongside (no existing API changed):

  data Usage       = Fresh | Consumed
  data LinHandleU  : Usage -> Nat -> Type
  consume          : LinHandleU Fresh tok -> LinHandleU Consumed tok

Theorems:

  distinctUsage        : Fresh = Consumed -> Void
                         — Usage constructors are distinct; without this
                           the state machine would collapse.

  consumePreservesData : consume (MkLinFresh off sid) =
                         MkLinConsumed off sid
                         — behavioural lemma for `consume`: offset and
                           schemaId carry through; only the state tag
                           changes.

  noReuse              : LinHandleU Consumed tok ->
                         (Consumed = Fresh) -> Void
                         — the main Level 10 theorem: the only way to
                           transport a consumed handle back to fresh is
                           through an absurd equality, so no total
                           `unconsume` exists in the safe fragment.

  noReuseEcho          : LinHandleU Consumed tok ->
                         LinHandleU Fresh tok ->
                         (Consumed = Fresh) -> Void
                         — cast as an echo-type / displayed-fiber statement:
                           the fiber of `consume` over any consumed handle
                           is at-most-one point.  Connects Linear to the
                           Echo.idr machinery landed in A0.

The existing (1 _ : LinHandle tok) QTT-based linearity enforcement and
`NoDoubleFree` marker remain untouched; this is purely additive.

idris2 --check clean.  panic-attack assail: 0 weak points.
Zero dangerous patterns.  %default total throughout.

Author: hyperpolymath

LEVEL-STATUS.md

@@ -51,7 +51,7 @@ the remaining v1.1 work.**
 | 7 | Aliasing safety | Pointer.idr (Unique) | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased** |
 | 8 | Effect-tracking | Effects.idr | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased** |
 | 9 | Lifetime safety | Lifetime.idr | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased** |
-| 10 | Linearity | Linear.idr (QTT q=1) | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased** |
+| 10 | Linearity | Linear.idr (QTT q=1) | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased.  Propositional state-machine theorems added A3 (2026-04-18): distinctUsage, consumePreservesData, noReuse, noReuseEcho — usage-indexed handle `LinHandleU Fresh/Consumed tok` with `consume` state transition, alongside the QTT structural layer.** |
 | 11 | Tropical cost-tracking | Tropical.idr | Not yet | None | **In package (A1, 2026-04-18).  Commutative-semiring closure PROVEN (A2, 2026-04-18): all 12 axioms — tropAddLeftId/RightId/Comm/Assoc, tropMulLeftId/RightId/Comm/Assoc, tropMulLeftAnn/RightAnn, tropMulDistrib/DistribR.  Uses structural `tropMin` (007-lang template).  Zero dangerous patterns.** |
 | 12 | Epistemic safety | Epistemic.idr | Not yet | None | **In package (A1, 2026-04-18); `writerKnowsFresh`, `freshOrStale`, `syncRestoresFresh` theorems live.  Full freshness propagation under concurrent writes deferred.** |
 | 13 | Module isolation | ModuleIsolation.idr | (per-module handles, future) | 12 parser/Checker tests | **v1.2 — Idris2 proof + surface checker live; 007 lowering DONE (task #5)** |

src/abi/TypedWasm/ABI/Linear.idr

@@ -157,7 +157,7 @@ data CompletedProtocol : (token : Nat) -> Type where
   MkCompleted : FreeResult -> CompletedProtocol token
 
 -- ============================================================================
--- No-Double-Free Proof
+-- No-Double-Free Proof (QTT structural layer)
 -- ============================================================================
 
 ||| Double-free is impossible by construction.
@@ -171,12 +171,109 @@ data CompletedProtocol : (token : Nat) -> Type where
 |||
 ||| This is not a separate proof to maintain — it falls out automatically
 ||| from QTT's linear quantity tracking. We document it here for clarity.
+|||
+||| The section below (Propositional State-Machine Theorems) adds a
+||| second, witness-manipulating layer for consumers that want an
+||| explicit proof term instead of just the QTT structural guarantee.
 public export
 data NoDoubleFree : Type where
   ||| Structural guarantee from QTT: consuming a linear value removes
   ||| it from scope, making re-consumption impossible.
   MkNoDoubleFree : NoDoubleFree
 
+-- ============================================================================
+-- Propositional State-Machine Theorems (PROOF-NEEDS §P0.2)
+-- ============================================================================
+--
+-- The `NoDoubleFree` marker above captures the QTT side of the story:
+-- the (1 _ : LinHandle token) quantity means consume-exactly-once is
+-- enforced by Idris2's quantity tracker at the binding site.  That is
+-- real but structural — it is not a proposition you can hand to another
+-- proof to consume.
+--
+-- This section adds an explicit witness-manipulating layer: a usage-
+-- indexed handle `LinHandleU u tok`, a state transition `consume`, and
+-- propositional theorems over the state machine.  `LinHandleU` is a
+-- displayed type (echo type) over `Usage` — the A0 machinery applies
+-- directly.
+--
+-- Zero dangerous patterns, %default total.
+
+||| Usage state of a linear resource handle.
+|||   Fresh    — not yet consumed; `consume` is callable.
+|||   Consumed — `consume` has been called; no further transition valid.
+public export
+data Usage : Type where
+  Fresh    : Usage
+  Consumed : Usage
+
+||| Linear handle indexed by its usage state.
+|||
+||| The constructor choice tracks the state in the type, so applying
+||| `consume` to a `LinHandleU Consumed tok` is a type error at the
+||| binding site (not a runtime check).  This is a state machine whose
+||| transitions are witnessed by the constructors of `consume`.
+public export
+data LinHandleU : (u : Usage) -> (token : Nat) -> Type where
+  ||| A fresh, unconsumed linear handle.
+  MkLinFresh    : (offset : Nat) -> (schemaId : Nat) -> LinHandleU Fresh tok
+  ||| A linear handle that has been consumed exactly once.
+  MkLinConsumed : (offset : Nat) -> (schemaId : Nat) -> LinHandleU Consumed tok
+
+||| State transition: a fresh handle becomes consumed.  The underlying
+||| offset and schema identifier are preserved so the runtime can still
+||| emit the free call after the type-level state has flipped.
+public export
+consume : LinHandleU Fresh tok -> LinHandleU Consumed tok
+consume (MkLinFresh off sid) = MkLinConsumed off sid
+
+-- ---- Theorems ----
+
+||| Fresh and Consumed are distinct usage states.
+|||
+||| Without this, any attestation built from the state index would be
+||| vacuous because the index could collapse.
+public export
+distinctUsage : Fresh = Consumed -> Void
+distinctUsage Refl impossible
+
+||| `consume` preserves the underlying offset and schemaId; only the
+||| state tag changes.  This is the behavioural lemma for `consume`:
+||| the function does what its type promises and no more.
+public export
+consumePreservesData :
+     {0 tok : Nat}
+  -> (off, sid : Nat)
+  -> consume {tok} (MkLinFresh off sid) = MkLinConsumed off sid
+consumePreservesData _ _ = Refl
+
+||| The central Level 10 theorem: once consumed, no path back to Fresh.
+|||
+||| Any hypothetical "unconsume" function would have to apply this
+||| transport.  Since its precondition `Consumed = Fresh` is uninhabited
+||| (by `distinctUsage`), no total function of type
+||| `LinHandleU Consumed tok -> LinHandleU Fresh tok` can be written in
+||| the safe fragment.
+|||
+||| Read: "the only way to move Consumed back to Fresh is to first prove
+||| the two states are equal, which produces Void."
+public export
+noReuse : (h : LinHandleU Consumed tok) ->
+          (absurd : Consumed = Fresh) ->
+          Void
+noReuse _ Refl impossible
+
+||| Corollary: given a consumed handle, the set of fresh handles that
+||| would `consume` to it is empty when the states are distinct.  This
+||| phrases the noReuse theorem as an echo type / displayed fiber: the
+||| fiber of `consume` over any consumed handle has cardinality exactly
+||| one (the fresh predecessor), not more.
+public export
+noReuseEcho : (h : LinHandleU Consumed tok) ->
+              (f : LinHandleU Fresh tok) ->
+              (Consumed = Fresh) -> Void
+noReuseEcho _ _ prf = distinctUsage (sym prf)
+
 -- ============================================================================
 -- Resource Counting (Bounded Linearity)
 -- ============================================================================