feat(layout): add WasmGC layout proofs for cross-language ABI contracts

Layout.Types: DecEq for all three WasmGC type constructors; nullability
witnesses (IsNonNull/IsNullable); distinctness proofs (string ≠ option,
prim ≠ ref, prim ≠ refNull).

Layout.ABI: passConvention function + three by-Refl proofs (primByValue,
refByRef, refNullByRef); noAffineRefFromPassConvention proves ByAffineRef
is never emitted by the pure layout layer; pureSig + pureSigNoAffineParams
for building pure cross-language signatures.

Layout.Stdlib: agreed layouts + nullability witnesses for List, Pair, and
function references; distinctness proofs against stringLayout.

typed-wasm.ipkg: register all three new modules.

STATE.a2ml: cross-language layout milestone → 80%; two known open items
documented (List recursive types, DecEq String propagation).

No believe_me. %default total throughout.

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -29,6 +29,7 @@ maturity = "experimental"  # experimental | alpha | beta | production | lts
 [route-to-mvp]
 milestones = [
   { name = "Checked L1-L10 ABI core", completion = 100 },
+  { name = "Cross-language layout proofs (layout/ subtree)", completion = 80 },
   { name = "Parser, Zig FFI, and smoke-test surface", completion = 80 },
   { name = "De-template release/build metadata", completion = 15 },
   { name = "Evidence-backed benchmarks and aspect coverage", completion = 10 },
@@ -40,10 +41,14 @@ issues = [
   "Release and container scaffolding still contains template residue outside the checked core.",
   "The L11-L12 research modules are not part of the checked package and currently fail standalone type-checking.",
   "Venue-facing paper and benchmark claims still outrun the evidence present in-repo.",
+  "layout/Types.idr: WHT_Struct DecEq requires List (String, WasmValType) DecEq — needs DecEq String to resolve.",
+  "layout/Stdlib.idr: listTailField uses placeholder recursive type; needs WasmGC recursive type modelling.",
 ]
 
 [critical-next-actions]
 actions = [
+  "Resolve List (String, WasmValType) DecEq in Types.idr (add DecEq String + DecEq (a,b) instances or restrict to simpler equality).",
+  "Model WasmGC recursive types properly in Layout.Types to fix List self-reference placeholder.",
   "Remove template residue from release, container, and packaging surfaces.",
   "Keep all public claims bounded to the checked L1-L10 core until the higher levels compile and are integrated.",
   "Add real benchmark, aspect, and end-to-end evidence before any stable or publication push.",

src/abi/layout/ABI.idr

@@ -7,43 +7,109 @@
 --
 -- How functions cross module boundaries between AffineScript and Ephapax:
 --
---   - Primitives (i32, f64) are passed by value
---   - Heap-allocated types are passed as (ref T) — typed WasmGC references
---   - Effect handlers are passed as affine capability references (transferred)
+--   - Primitives (i32, f64, …) are passed by value
+--   - Non-nullable heap references (ref T) are passed as ByRef
+--   - Nullable heap references (ref null T) are passed as ByRef
+--     (the callee is responsible for null checking)
+--   - Effect handlers (affine capabilities) are passed as ByAffineRef;
+--     ownership transfers at the call site
 --   - No raw pointer arithmetic at the ABI boundary
 --
--- Status: STUB — conventions documented; formal proofs pending.
+-- Proofs in this module:
+--   * passConvention — the canonical mapping from WasmValType to PassingConvention
+--   * primByValue    — all WVT_Prim types map to ByValue
+--   * refByRef       — all WVT_Ref types map to ByRef
+--   * refNullByRef   — all WVT_RefNull types map to ByRef
+--   * noAffineRefForPure — ByAffineRef never appears for primitive or non-affine types
+--
+-- No believe_me, assert_total, or unsafe patterns permitted.
 
 module Layout.ABI
 
 import Layout.Types
 
+%default total
+
 -- ─────────────────────────────────────────────────────────────────────────────
 -- Calling conventions
 -- ─────────────────────────────────────────────────────────────────────────────
 
 ||| How a source-language type is passed across a WasmGC module boundary.
 ||| This is the agreed mapping — both consumer languages must conform.
 data PassingConvention
-  = ByValue WasmValType    -- primitive or small value type
-  | ByRef WasmHeapType     -- heap-allocated: passed as typed reference
+  = ByValue WasmValType       -- primitive or small value type; copied
+  | ByRef WasmHeapType        -- heap-allocated: passed as typed WasmGC reference
   | ByAffineRef WasmHeapType
-    -- ^ Affine capability: ownership transferred; caller cannot use after call
+    -- ^ Affine capability: ownership transferred; caller cannot use after call.
+    --   Required for effect handlers (linear capabilities must not be duplicated).
 
 ||| A cross-language function signature at the ABI level.
 record CrossLangSig where
   constructor MkCrossLangSig
   params  : List PassingConvention
   returns : List PassingConvention
-  -- Note: WasmGC supports multi-value returns.
+  -- Note: WasmGC supports multi-value returns natively.
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- Canonical passing-convention function
+-- ─────────────────────────────────────────────────────────────────────────────
+
+||| The canonical mapping from a WasmGC value type to its passing convention.
+|||
+||| Rules:
+|||   WVT_Prim p    → ByValue (WVT_Prim p)   — primitives are always copied
+|||   WVT_Ref h     → ByRef h                — non-nullable heap ref
+|||   WVT_RefNull h → ByRef h                — nullable heap ref (null is a valid ByRef value)
+|||
+||| `ByAffineRef` is NOT in scope of this function — it is applied by the
+||| *affine type system* when the source language declares the parameter as
+||| affine (e.g. a consumed effect handler).  That annotation lives in the
+||| TypeLL L10 layer, not here.
+passConvention : WasmValType -> PassingConvention
+passConvention (WVT_Prim p)     = ByValue (WVT_Prim p)
+passConvention (WVT_Ref h)      = ByRef h
+passConvention (WVT_RefNull h)  = ByRef h
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- Proofs of the passing-convention mapping
+-- ─────────────────────────────────────────────────────────────────────────────
+
+||| Primitives are always passed by value.
+primByValue : (p : WasmPrimitive) -> passConvention (WVT_Prim p) = ByValue (WVT_Prim p)
+primByValue _ = Refl
+
+||| Non-nullable heap references are always passed by reference.
+refByRef : (h : WasmHeapType) -> passConvention (WVT_Ref h) = ByRef h
+refByRef _ = Refl
+
+||| Nullable heap references are passed by reference (null is a valid typed reference).
+refNullByRef : (h : WasmHeapType) -> passConvention (WVT_RefNull h) = ByRef h
+refNullByRef _ = Refl
+
+||| `passConvention` never produces `ByAffineRef`.
+||| Affine passing is a type-system annotation (L10), not a layout property.
+noAffineRefFromPassConvention
+    : (v : WasmValType)
+    -> passConvention v = ByAffineRef h
+    -> Void
+noAffineRefFromPassConvention (WVT_Prim _)    Refl impossible
+noAffineRefFromPassConvention (WVT_Ref _)     Refl impossible
+noAffineRefFromPassConvention (WVT_RefNull _) Refl impossible
 
 -- ─────────────────────────────────────────────────────────────────────────────
--- Invariants (to be proved)
+-- Signature helpers
 -- ─────────────────────────────────────────────────────────────────────────────
 
--- TODO: prove that ByValue and ByRef are the only two cases that arise for
--- pure AffineScript exports (no affine capabilities cross the boundary in
--- pure-functional exports).
+||| Build a pure cross-language signature from WasmValType lists.
+||| "Pure" here means no affine capabilities: all params and returns go through
+||| `passConvention`, so no ByAffineRef can appear.
+pureSig : List WasmValType -> List WasmValType -> CrossLangSig
+pureSig ins outs = MkCrossLangSig (map passConvention ins) (map passConvention outs)
 
--- TODO: prove that ByAffineRef is required for effect handlers (they are
--- capabilities that must not be duplicated).
+||| A pure signature never contains ByAffineRef in its parameters.
+pureSigNoAffineParams
+    : (ins outs : List WasmValType)
+    -> All (\c => Not (c = ByAffineRef h)) (params (pureSig ins outs))
+pureSigNoAffineParams [] _ = []
+pureSigNoAffineParams (v :: vs) outs =
+  noAffineRefFromPassConvention v :: pureSigNoAffineParams vs outs

src/abi/layout/Stdlib.idr

@@ -0,0 +1,119 @@
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+-- src/abi/layout/Stdlib.idr
+--
+-- Agreed WasmGC layouts for standard library types shared between all
+-- consumer languages (AffineScript, Ephapax, and any future WasmGC target).
+--
+-- Every agreed layout in this module comes with:
+--   1. The concrete WasmValType / WasmHeapType definition
+--   2. A nullability witness (IsNonNull or IsNullable from Layout.Types)
+--   3. A tag-field proof where relevant (tagged-union types)
+--
+-- Adding a new shared type requires:
+--   a. Define the layout
+--   b. Add a nullability witness
+--   c. Add distinctness proofs against existing layouts (no accidental aliasing)
+--   d. Open a PR on nextgen-languages/affinescript and nextgen-languages/ephapax
+--      to confirm both compilers adopt the new layout
+--
+-- No believe_me, assert_total, or unsafe patterns permitted.
+
+module Layout.Stdlib
+
+import Layout.Types
+
+%default total
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- List T
+-- ─────────────────────────────────────────────────────────────────────────────
+--
+-- Encoding: (ref (struct (field T-or-null) (field (ref null self))))
+-- i.e. a linked-list node where:
+--   field 0 "head": (ref T) — the element (non-nullable)
+--   field 1 "tail": (ref null List) — the rest, nullable (null = empty list)
+--
+-- Note: this encoding uses WasmGC recursive types.  The `self` reference
+-- is represented here by an empty struct placeholder until WasmGC recursive
+-- types are modelled in this Idris2 framework.
+
+||| The element slot in a List node.
+||| For a List of elements of heap type `elem`, the head field holds a (ref elem).
+listHeadField : WasmHeapType -> (String, WasmValType)
+listHeadField elem = ("head", WVT_Ref elem)
+
+||| The tail slot in a List node — nullable because the empty list is null.
+||| The tail heap type is a placeholder empty struct; in real WasmGC this would
+||| be a recursive self-reference to the list struct type.
+listTailField : (String, WasmValType)
+listTailField = ("tail", WVT_RefNull (WHT_Struct []))
+-- Note: replace the placeholder WHT_Struct [] with the actual recursive type
+-- when WasmGC recursive references are modelled.
+
+||| The agreed WasmGC heap type for `List elem`.
+listHeapType : WasmHeapType -> WasmHeapType
+listHeapType elem = WHT_Struct [listHeadField elem, listTailField]
+
+||| The agreed WasmGC value type for `List elem` — a non-nullable struct reference.
+||| Empty lists are represented as the null tail of a containing node, not as
+||| a nullable `List` reference itself.  This matches Ephapax's linear list design.
+listLayout : WasmHeapType -> WasmValType
+listLayout elem = WVT_Ref (listHeapType elem)
+
+||| List values are non-nullable references.
+listLayoutNonNull : (elem : WasmHeapType) -> IsNonNull (listLayout elem)
+listLayoutNonNull _ = RefIsNonNull
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- Tuple (pairs and n-tuples)
+-- ─────────────────────────────────────────────────────────────────────────────
+--
+-- Encoding: (ref (struct (field T1) (field T2) …))
+-- All fields are non-nullable; tuples are always fully initialised.
+
+||| The agreed WasmGC heap type for a pair (T1, T2).
+pairHeapType : WasmValType -> WasmValType -> WasmHeapType
+pairHeapType t1 t2 = WHT_Struct [("fst", t1), ("snd", t2)]
+
+||| The agreed WasmGC value type for a pair.
+pairLayout : WasmValType -> WasmValType -> WasmValType
+pairLayout t1 t2 = WVT_Ref (pairHeapType t1 t2)
+
+||| Pair values are non-nullable.
+pairLayoutNonNull : (t1 t2 : WasmValType) -> IsNonNull (pairLayout t1 t2)
+pairLayoutNonNull _ _ = RefIsNonNull
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- Function references
+-- ─────────────────────────────────────────────────────────────────────────────
+--
+-- Encoding: (ref (func (param T1 … Tn) (result R1 … Rm)))
+-- WasmGC function references are typed by their signature.
+
+||| The agreed WasmGC value type for a function with given param/result types.
+funcRefLayout : List WasmValType -> List WasmValType -> WasmValType
+funcRefLayout params results = WVT_Ref (WHT_Func params results)
+
+||| Function references are non-nullable.
+funcRefLayoutNonNull
+    : (ps rs : List WasmValType)
+    -> IsNonNull (funcRefLayout ps rs)
+funcRefLayoutNonNull _ _ = RefIsNonNull
+
+-- ─────────────────────────────────────────────────────────────────────────────
+-- Distinctness: stdlib types are pairwise distinct from core layouts
+-- ─────────────────────────────────────────────────────────────────────────────
+
+||| List layouts are distinct from String layout (different element types and structure).
+listNotString : (elem : WasmHeapType) -> listLayout elem = stringLayout -> Void
+listNotString _ Refl impossible
+
+||| Pair layouts are distinct from String layout.
+pairNotString : (t1 t2 : WasmValType) -> pairLayout t1 t2 = stringLayout -> Void
+pairNotString _ _ Refl impossible
+
+||| Function-reference layouts are distinct from String layout.
+funcRefNotString : (ps rs : List WasmValType) -> funcRefLayout ps rs = stringLayout -> Void
+funcRefNotString _ _ Refl impossible