fix(layout): restore Layout.* aggregate modules to full ipkg build

Unblocks the aggregate-library layout contracts that were gated out of
typed-wasm.ipkg in the previous commit, after resolving the 11 Idris2
0.8 compatibility issues catalogued in the Layout-fix entry of
PROOF-NEEDS.md (mutual recursion, visibility, imports, nested `with`
pattern unification, Refl-impossible reduction, auto-bound-implicit
shadowing, `(x y : T)` binder syntax, `prefix` reserved keyword,
non-linear SubStruct transitivity, `Bool`-vs-`Type` predicate mix, and
over-strong WasmGCEq constructor).

All 21 modules now build cleanly under Idris2 0.8.0-712523a89 with
zero believe_me / assert_total / postulate / sorry; %default total
preserved throughout.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

PROOF-NEEDS.md

@@ -483,48 +483,63 @@ After each session: run `idris2 --check` on every file in
 adjacent code (no new unsafe code should land), update this file's
 inventory table, commit.
 
-## Outstanding infrastructure work — Layout module fix (added 2026-04-18)
-
-`Layout/Types.idr` was never compiling cleanly under this Idris2 0.8
-build.  The directory rename `layout/` → `Layout/` (filesystem case
-matching the `Layout.*` module names) and the `import layout.Types`
-→ `import Layout.Types` typo fix in `TypedWasm/ABI/Layout.idr` were
-made on 2026-04-18, which surfaced the underlying issues:
-
-  1. **Mutual recursion not declared.**  `WasmHeapType` references
-     `WasmValType` (line 65) but `WasmValType` is declared later
-     (line 73).  Wrapping both in `mutual` is needed.
-  2. **Visibility annotations missing.**  `data WasmPrimitive` /
-     `WasmHeapType` / `WasmValType` and the layout values
-     (`stringLayout`, `optionLayout`, `resultLayout`, `enumLayout`,
-     `recordLayout`) all lack `public export`, so downstream
-     constructors are not visible and `Refl`-based proofs do not
-     unify.
-  3. **Imports missing.**  `Decidable.Equality` is used (`DecEq`,
-     `Yes`, `No`, `decEq`) but never imported; `Data.List` similarly.
-  4. **Nested `with` block patterns** in the `DecEq WasmHeapType`
-     instance (lines 178-234) trigger pattern-variable unification
-     errors under this Idris2 build.
-  5. **Refl-impossible patterns** (`stringOptionDistinct _ Refl
-     impossible` etc.) need the layout values to reduce at unification
-     time — even with `public export` the reduction does not happen
-     under this build, so a different proof strategy is needed
-     (probably explicit `case ... of` with constructor mismatch).
-
-**Current gating (2026-04-18):** the four `Layout.*` modules are
-commented out of `typed-wasm.ipkg` and the `import TypedWasm.ABI.Layout`
-line in `TypedWasm/ABI/Proofs.idr` is gated.  This unblocks the full
-ipkg build for the typed-wasm core (TypedWasm.ABI.* modules) — which
-is the primary purpose of typed-wasm.  The aggregate-library Layout
-contracts remain in the tree for restoration once the issues above
-are addressed.
-
-**Remediation plan:** add `public export` to every Layout type/value;
-add `import Decidable.Equality, Data.List`; rewrite the `DecEq
-WasmHeapType` and `DecEq WasmValType` instances without nested `with`
-(use case-of or explicit witness construction); replace the
-Refl-impossible patterns with `case ... of` + constructor analysis.
-Estimated effort: one focused session.
+## Outstanding infrastructure work — Layout module fix ✅ DONE 2026-04-18
+
+**Status:** resolved in the same session it was identified.  All four
+`Layout.*` modules plus the `TypedWasm.ABI.Layout` bridge are back in
+`typed-wasm.ipkg`, the `import TypedWasm.ABI.Layout` is restored in
+`TypedWasm/ABI/Proofs.idr`, and the full 21-module ipkg builds cleanly
+under Idris2 0.8.0-712523a89.
+
+**Fixes applied, by issue:**
+
+1. **Mutual recursion not declared** — wrapped `WasmHeapType` and
+   `WasmValType` in a single `mutual` block (and separately
+   `WasmValTypeValid` / `WasmGCLayoutValid` in `TypedWasm.ABI.Layout`).
+2. **Visibility annotations missing** — added `public export` to every
+   data type, constructor, function, layout value, and `DecEq` / data
+   instance in `Layout/Types.idr`, `Layout/ABI.idr`, `Layout/Stdlib.idr`,
+   `Layout/AirborneSubmarineSquadron.idr`, and `TypedWasm/ABI/Layout.idr`.
+3. **Imports missing** — added `Decidable.Equality` + `Data.List` to
+   `Layout/Types.idr`; `Data.List.Quantifiers` to `TypedWasm.ABI.Layout`;
+   `Data.List` to `Layout/AirborneSubmarineSquadron.idr`.
+4. **Nested `with` block patterns** — rewrote the `DecEq WasmHeapType`
+   and `DecEq WasmValType` instances as four plain mutual functions
+   (`decEqHT`, `decEqVT`, `decEqVTList`, `decEqFields`) with thin
+   non-mutual interface wrappers.  This sidesteps Idris2 0.8's
+   interface-resolution chain through `List (String, WasmValType)`.
+5. **Refl-impossible patterns** — replaced `LHS impossible` clauses
+   with `prf = case prf of Refl impossible`.  The scope change lets
+   Idris2 reduce the layout values after they see `public export`.
+6. **Auto-bound implicit shadowing** — lowercase references to
+   `stringLayout`, `resultLayout`, etc. inside type signatures were
+   being treated as implicit pattern variables that shadowed the real
+   definitions.  Fully qualifying as `Layout.Types.stringLayout` (and
+   friends) suppresses the auto-bind and lets the definitions reduce.
+7. **`(x y : T)` binder syntax** — Idris2 0.8 prefers comma-separated
+   `(x, y : T)`; updated all affected binders.
+8. **`prefix` is reserved** — renamed `SubStruct`'s `prefix` argument
+   to `pre` (operator fixity keyword in Idris2 0.8).
+9. **Non-linear SubStruct transitivity pattern** — rewrote
+   `data Subtype`'s `SubStruct` constructor to carry an explicit
+   equality witness `prf : fs = pre ++ rest`, then proved
+   `subTrans` for the SubStruct/SubStruct case using `trans`, `cong`,
+   and `sym appendAssociative`.  (The direction of
+   `appendAssociative : l ++ (c ++ r) = (l ++ c) ++ r` needs `sym` to
+   rearrange `(pre ++ rest1) ++ rest2` into `pre ++ (rest1 ++ rest2)`.)
+10. **`WasmGCLayoutValid` struct-field predicate** — replaced the
+    `case vt of … => True` predicate (which mixed `Bool` with `Type`)
+    with a proper `WasmValTypeValid` inductive in a mutual block.
+11. **`WasmGCEq` constructor** — replaced the over-strong
+    `MkGCEq : decEq h1 h2 = Yes Refl -> WasmGCEq h1 h2` with the
+    simpler propositional form `MkGCEq : h1 = h2 -> WasmGCEq h1 h2`.
+    The original encoding required a non-trivial theorem about `decEq`
+    to construct a reflexive witness.
+
+**Net result:** the aggregate-library Layout contracts (the secondary
+purpose of typed-wasm, per ADR-004) are back in the ipkg alongside
+the typed-wasm core, with zero `believe_me` / `assert_total` /
+`postulate` / `sorry`.  `%default total` preserved throughout.
 
 ## Pre-existing notes (preserved from prior revision)
 

src/abi/Layout/ABI.idr

@@ -27,6 +27,7 @@
 module Layout.ABI
 
 import Layout.Types
+import Data.List.Quantifiers
 
 %default total
 
@@ -36,6 +37,7 @@ import Layout.Types
 
 ||| How a source-language type is passed across a WasmGC module boundary.
 ||| This is the agreed mapping — both consumer languages must conform.
+public export
 data PassingConvention
   = ByValue WasmValType       -- primitive or small value type; copied
   | ByRef WasmHeapType        -- heap-allocated: passed as typed WasmGC reference
@@ -44,6 +46,7 @@ data PassingConvention
     --   Required for effect handlers (linear capabilities must not be duplicated).
 
 ||| A cross-language function signature at the ABI level.
+public export
 record CrossLangSig where
   constructor MkCrossLangSig
   params  : List PassingConvention
@@ -65,6 +68,7 @@ record CrossLangSig where
 ||| *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.
+public export
 passConvention : WasmValType -> PassingConvention
 passConvention (WVT_Prim p)     = ByValue (WVT_Prim p)
 passConvention (WVT_Ref h)      = ByRef h
@@ -75,26 +79,31 @@ passConvention (WVT_RefNull h)  = ByRef h
 -- ─────────────────────────────────────────────────────────────────────────────
 
 ||| Primitives are always passed by value.
+public export
 primByValue : (p : WasmPrimitive) -> passConvention (WVT_Prim p) = ByValue (WVT_Prim p)
 primByValue _ = Refl
 
 ||| Non-nullable heap references are always passed by reference.
+public export
 refByRef : (h : WasmHeapType) -> passConvention (WVT_Ref h) = ByRef h
 refByRef _ = Refl
 
 ||| Nullable heap references are passed by reference (null is a valid typed reference).
+public export
 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.
+public export
 noAffineRefFromPassConvention
     : (v : WasmValType)
+    -> {h : WasmHeapType}
     -> passConvention v = ByAffineRef h
     -> Void
-noAffineRefFromPassConvention (WVT_Prim _)    Refl impossible
-noAffineRefFromPassConvention (WVT_Ref _)     Refl impossible
-noAffineRefFromPassConvention (WVT_RefNull _) Refl impossible
+noAffineRefFromPassConvention (WVT_Prim _)    prf = case prf of Refl impossible
+noAffineRefFromPassConvention (WVT_Ref _)     prf = case prf of Refl impossible
+noAffineRefFromPassConvention (WVT_RefNull _) prf = case prf of Refl impossible
 
 -- ─────────────────────────────────────────────────────────────────────────────
 -- Signature helpers
@@ -103,13 +112,22 @@ noAffineRefFromPassConvention (WVT_RefNull _) Refl impossible
 ||| 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.
+public export
 pureSig : List WasmValType -> List WasmValType -> CrossLangSig
 pureSig ins outs = MkCrossLangSig (map passConvention ins) (map passConvention outs)
 
 ||| A pure signature never contains ByAffineRef in its parameters.
+|||
+||| The original pureSigNoAffineParams used an auto-bound implicit `h` that
+||| quantified at the wrong level (it became part of each list element's
+||| predicate rather than universally scoped over the whole list).  The fix is
+||| to bind the predicate concretely against *any* heap type the element might
+||| match, using an inner forall in the predicate itself.
+public export
 pureSigNoAffineParams
-    : (ins outs : List WasmValType)
-    -> All (\c => Not (c = ByAffineRef h)) (params (pureSig ins outs))
+    : (ins, outs : List WasmValType)
+    -> All (\c => (h : WasmHeapType) -> Not (c = ByAffineRef h))
+           (params (Layout.ABI.pureSig ins outs))
 pureSigNoAffineParams [] _ = []
 pureSigNoAffineParams (v :: vs) outs =
-  noAffineRefFromPassConvention v :: pureSigNoAffineParams vs outs
+  (\h => noAffineRefFromPassConvention v {h}) :: pureSigNoAffineParams vs outs

src/abi/Layout/AirborneSubmarineSquadron.idr

@@ -16,21 +16,27 @@ module Layout.AirborneSubmarineSquadron
 
 import Layout.Types
 import Layout.ABI
+import Data.List
 
 %default total
 
+public export
 snapshotAbiVersion : String
 snapshotAbiVersion = "airborne-submarine-squadron.step_state.v1"
 
+public export
 snapshotFieldCount : Nat
 snapshotFieldCount = 29
 
+public export
 inputFieldCount : Nat
 inputFieldCount = 5
 
+public export
 stepStateArity : Nat
 stepStateArity = snapshotFieldCount + inputFieldCount
 
+public export
 snapshotFieldNames : List String
 snapshotFieldNames =
   [ "tick"
@@ -64,6 +70,7 @@ snapshotFieldNames =
   , "mission_failed"
   ]
 
+public export
 inputFieldNames : List String
 inputFieldNames =
   [ "thrust_x"
@@ -73,35 +80,54 @@ inputFieldNames =
   , "toggle_env"
   ]
 
-snapshotFieldCountProof : length snapshotFieldNames = snapshotFieldCount
+public export
+snapshotFieldCountProof
+    : length Layout.AirborneSubmarineSquadron.snapshotFieldNames
+    = Layout.AirborneSubmarineSquadron.snapshotFieldCount
 snapshotFieldCountProof = Refl
 
-inputFieldCountProof : length inputFieldNames = inputFieldCount
+public export
+inputFieldCountProof
+    : length Layout.AirborneSubmarineSquadron.inputFieldNames
+    = Layout.AirborneSubmarineSquadron.inputFieldCount
 inputFieldCountProof = Refl
 
+public export
 snapshotResultHeap : WasmHeapType
 snapshotResultHeap = WHT_Array (WVT_Prim WasmI32)
 
+public export
 snapshotResultConvention : PassingConvention
 snapshotResultConvention = ByRef snapshotResultHeap
 
+public export
 i32Convention : PassingConvention
 i32Convention = ByValue (WVT_Prim WasmI32)
 
+public export
 stepStateParams : List PassingConvention
 stepStateParams = replicate stepStateArity i32Convention
 
-stepStateArityProof : length stepStateParams = stepStateArity
+public export
+stepStateArityProof
+    : length Layout.AirborneSubmarineSquadron.stepStateParams
+    = Layout.AirborneSubmarineSquadron.stepStateArity
 stepStateArityProof = Refl
 
+public export
 initStateSig : CrossLangSig
 initStateSig = MkCrossLangSig [] [snapshotResultConvention]
 
+public export
 stepStateSig : CrossLangSig
 stepStateSig = MkCrossLangSig stepStateParams [snapshotResultConvention]
 
-initStateNoParams : params initStateSig = []
+public export
+initStateNoParams : params Layout.AirborneSubmarineSquadron.initStateSig = []
 initStateNoParams = Refl
 
-stepStateReturnsSnapshot : returns stepStateSig = [snapshotResultConvention]
+public export
+stepStateReturnsSnapshot
+    : returns Layout.AirborneSubmarineSquadron.stepStateSig
+    = [Layout.AirborneSubmarineSquadron.snapshotResultConvention]
 stepStateReturnsSnapshot = Refl