docs: sync whitepaper body with actual Idris2 ABI names

- Replace Schema/TypedGet/GetHere/GetThere listings with actual
  implementation names: Schema=List Field, FieldIn/FieldHere/FieldThere
- Add AllocResult to the QTT listing to show the full alloc/free protocol
- Expand freeRegion description to explain Level9/Level10 composition
- Add (1 _) quantity annotation to Linear.idr freeRegion — enforces
  exactly-once handle use at the type level (prevents leak and double-free)
- Update date from March 2026 to April 2026
- Apply all changes to both docs/whitepapers/academic/ and docs/arxiv/

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

docs/arxiv/typed-wasm.tex

@@ -738,24 +738,31 @@ \subsection{Idris~2 and Dependent Types}
 within the bounds of array of size~$n$'' is a proposition over the value
 of~$i$.
 
-A region schema is a value-level record:
+A region schema is a flat list of named, typed fields:
 
-\begin{lstlisting}[language=Idris2,caption={Region schema as a dependently typed list.}]
-data Schema : List (String, FieldType) -> Type where
-  Nil  : Schema []
-  (::) : Field name ty -> Schema rest -> Schema ((name, ty) :: rest)
+\begin{lstlisting}[language=Idris2,caption={Region schema as a list of named fields.}]
+-- Schema is a list of fields; order determines memory layout.
+Schema : Type
+Schema = List Field
+
+data Field : Type where
+  MkField : (name : String) -> (ty : WasmType) -> Field
 \end{lstlisting}
 
-A typed access is indexed by the schema:
+A compile-time field-lookup proof witnesses that a named field exists
+in the schema (Level~2 region-binding safety):
 
-\begin{lstlisting}[language=Idris2,caption={Typed memory access indexed by schema.}]
-data TypedGet : Schema fields -> (name : String) -> FieldType -> Type where
-  GetHere  : TypedGet (MkField {name} {ty} :: rest) name ty
-  GetThere : TypedGet rest name ty -> TypedGet (f :: rest) name ty
+\begin{lstlisting}[language=Idris2,caption={Field-lookup proof for Level~2 region-binding.}]
+data FieldIn : String -> Schema -> Type where
+  FieldHere  : {auto prf : fieldName f = name}
+             -> FieldIn name (f :: rest)
+  FieldThere : FieldIn name rest -> FieldIn name (f :: rest)
 \end{lstlisting}
 
 The result type of \texttt{region.get \$r .name} is \emph{computed} from
-the schema, not declared by the programmer.
+the schema via \texttt{FieldIn} --- not declared by the programmer.
+Without a valid \texttt{FieldIn} proof, the access is rejected at compile
+time.
 
 \subsection{Quantitative Type Theory}
 
@@ -776,14 +783,23 @@ \subsection{Quantitative Type Theory}
 \end{tabular}
 \end{table}
 
-Level~10 is implemented by binding allocation handles with quantity~1:
+Level~10 is implemented by binding allocation handles with quantity~1.
+The allocation protocol produces a linear handle plus a liveness witness;
+freeing consumes both:
+
+\begin{lstlisting}[language=Idris2,caption={Linear resource protocol: alloc produces, free consumes.}]
+data AllocResult : (token : Nat) -> Type where
+  MkAllocResult : LinHandle token -> RegionLive token -> AllocResult token
 
-\begin{lstlisting}[language=Idris2,caption={Linear resource handling via QTT quantity~1.}]
+-- (1 _) enforces exactly-once use: zero = leak, two = double-free.
 freeRegion : (1 _ : LinHandle token) -> RegionLive token -> FreeResult
 \end{lstlisting}
 
 The \texttt{(1 \_)} annotation means the type checker rejects any program
 where the handle is used zero times (leak) or more than once (double-free).
+After \texttt{freeRegion} returns, the \texttt{RegionLive} token is also
+consumed, invalidating all \texttt{LiveRef} borrows for that lifetime ---
+composing Level~10 linearity with Level~9 lifetime safety.
 
 \subsection{Proof Erasure}
 

docs/whitepapers/academic/typed-wasm.tex

@@ -76,7 +76,7 @@
   The Open University, Milton Keynes, UK\\
   \texttt{j.d.a.jewell@open.ac.uk}
 }
-\date{March 2026 --- Draft}
+\date{April 2026 --- Draft}
 
 \begin{document}
 
@@ -614,24 +614,32 @@ \subsection{Idris 2 and Dependent Types}
 ``index~$i$ is within the bounds of array of size~$n$'' is a proposition
 over the value of~$i$.
 
-A region schema is a value-level record:
+A region schema is a flat list of named, typed fields:
 
 \begin{lstlisting}[language=Idris]
-data Schema : List (String, FieldType) -> Type where
-  Nil  : Schema []
-  (::) : Field name ty -> Schema rest -> Schema ((name, ty) :: rest)
+-- Schema is a list of named fields; order determines memory layout.
+Schema : Type
+Schema = List Field
+
+data Field : Type where
+  MkField : (name : String) -> (ty : WasmType) -> Field
 \end{lstlisting}
 
-A typed access is indexed by the schema:
+A compile-time field-lookup proof witnesses that a given field exists
+in a schema (Level~2 region-binding safety):
 
 \begin{lstlisting}[language=Idris]
-data TypedGet : Schema fields -> (name : String) -> FieldType -> Type where
-  GetHere  : TypedGet (MkField {name} {ty} :: rest) name ty
-  GetThere : TypedGet rest name ty -> TypedGet (f :: rest) name ty
+data FieldIn : String -> Schema -> Type where
+  FieldHere  : {auto prf : fieldName f = name}
+             -> FieldIn name (f :: rest)
+  FieldThere : FieldIn name rest -> FieldIn name (f :: rest)
 \end{lstlisting}
 
 The result type of \lstinline{region.get \$r .name} is \emph{computed}
-from the schema, not declared by the programmer.
+from the schema via \lstinline{FieldIn} --- not declared by the programmer.
+Constructing a \lstinline{FieldHere} or \lstinline{FieldThere} proof is
+how the type checker verifies that the named field actually exists;
+without it, the access is rejected at compile time.
 
 \subsection{Quantitative Type Theory}
 \label{sec:qtt}
@@ -654,15 +662,28 @@ \subsection{Quantitative Type Theory}
 \end{tabularx}
 \end{table}
 
-Level~10 is implemented by binding allocation handles with quantity~1:
+Level~10 is implemented by binding allocation handles with quantity~1.
+The allocation protocol produces a linear handle plus a liveness witness;
+freeing consumes both:
 
 \begin{lstlisting}[language=Idris]
+-- Allocation returns a linear handle (must free exactly once)
+-- and a liveness witness (for Level 9 lifetime tracking).
+data AllocResult : (token : Nat) -> Type where
+  MkAllocResult : LinHandle token -> RegionLive token -> AllocResult token
+
+-- Free consumes the handle (quantity 1 = exactly once).
+-- The (1 _) annotation rejects zero uses (leak) or two uses (double-free).
 freeRegion : (1 _ : LinHandle token) -> RegionLive token -> FreeResult
 \end{lstlisting}
 
 The \lstinline{(1 _)} annotation means the type checker rejects any
 program where the handle is used zero times (leak) or more than once
-(double-free).
+(double-free).  After \lstinline{freeRegion} returns, both the
+\lstinline{LinHandle} and \lstinline{RegionLive} for that token are
+consumed, so all \lstinline{LiveRef} borrows with that token's lifetime
+become dead --- composing Level~10 linearity with Level~9 lifetime
+safety.
 
 \subsection{Proof Erasure}
 \label{sec:erasure}

src/abi/TypedWasm/ABI/Linear.idr

@@ -93,13 +93,16 @@ allocRegion sid off tok = MkAllocResult (MkLinHandle off sid) (MkRegionLive)
 
 ||| Free a region instance. Consumes the linear handle AND the
 ||| liveness witness. After this call:
-|||   - The LinHandle is consumed (no double-free possible)
+|||   - The LinHandle is consumed (no double-free possible — quantity 1)
 |||   - The RegionLive is consumed (no new borrows possible)
 |||   - All LiveRefs with lifetime (RegionLife token) become dead
 |||
 ||| This is the dual of allocRegion: alloc produces, free consumes.
+||| The (1 _) quantity annotation enforces at the type level that the
+||| handle is used exactly once: zero uses = leak (rejected), two uses =
+||| double-free (rejected).
 public export
-freeRegion : LinHandle token -> RegionLive token -> FreeResult
+freeRegion : (1 _ : LinHandle token) -> RegionLive token -> FreeResult
 freeRegion (MkLinHandle off _) _ = MkFreeResult off
 
 -- ============================================================================