diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
index a1d1125..9b27e2e 100644
--- a/.claude/CLAUDE.md
+++ b/.claude/CLAUDE.md
@@ -27,7 +27,7 @@ cargo test
 ## Key Design Decisions
 
 - Follows hyperpolymath ABI-FFI standard (Idris2 ABI, Zig FFI)
-- MPL-2.0 license
+- MPL-2.0 license (code) + CC-BY-SA-4.0 (docs); full texts in LICENSES/
 - RSR (Rhodium Standard Repository) template
 - Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/.github/workflows/rhodibot.yml b/.github/workflows/rhodibot.yml
index a82f178..1f45960 100644
--- a/.github/workflows/rhodibot.yml
+++ b/.github/workflows/rhodibot.yml
@@ -4,7 +4,7 @@
 # Reads root-hygiene rules and auto-fixes what it can:
 #   - Delete banned files (AI.djot, duplicate CONTRIBUTING.adoc, stale snapshots)
 #   - Rename misnamed files (AI.a2ml → 0-AI-MANIFEST.a2ml)
-#   - Fix SPDX headers (AGPL → PMPL in dotfiles)
+#   - Fix SPDX headers (AGPL → MPL-2.0 in dotfiles)
 #   - Create missing required files (SECURITY.md, CONTRIBUTING.md)
 #   - Report unfixable issues as PR comments
 #
@@ -87,7 +87,7 @@ jobs:
           for dotfile in .gitignore .gitattributes .editorconfig; do
             if [ -f "$dotfile" ] && grep -q "AGPL-3.0" "$dotfile" 2>/dev/null; then
               sed -i 's/AGPL-3.0-or-later/MPL-2.0/g; s/AGPL-3.0/MPL-2.0/g' "$dotfile"
-              FIXES="$FIXES\n- Fixed SPDX header in \`$dotfile\` (AGPL → PMPL)"
+              FIXES="$FIXES\n- Fixed SPDX header in \`$dotfile\` (AGPL → MPL-2.0)"
               CHANGED=true
             fi
           done
diff --git a/.gitignore b/.gitignore
index 73f5db0..3822e8d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,6 +18,11 @@ Thumbs.db
 /dist/
 /out/
 
+# Idris2 build artifacts
+**/build/
+*.ttc
+*.ttm
+
 # Dependencies
 /node_modules/
 /vendor/
diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml
index bc418c8..04e30a8 100644
--- a/.machine_readable/6a2/META.a2ml
+++ b/.machine_readable/6a2/META.a2ml
@@ -12,7 +12,7 @@ author = "Jonathan D.A. Jewell (hyperpolymath)"
 
 [architecture-decisions]
 decisions = [
-  "Licence migrated from PMPL-1.0-or-later to MPL-2.0 (commit ce87d4b).",
+  "Licence migrated from MPL-2.0 to MPL-2.0 (commit ce87d4b).",
 ]
 
 [development-practices]
diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
index 3818b62..a522b16 100644
--- a/.machine_readable/6a2/STATE.a2ml
+++ b/.machine_readable/6a2/STATE.a2ml
@@ -42,4 +42,4 @@ last-result = "unknown"  # unknown | pass | warn | fail
 
 [licence]
 spdx = "MPL-2.0"
-migration = "Migrated from PMPL-1.0-or-later to MPL-2.0 (commit ce87d4b)."
+migration = "Migrated from MPL-2.0 to MPL-2.0 (commit ce87d4b)."
diff --git a/.machine_readable/compliance/reuse/dep5 b/.machine_readable/compliance/reuse/dep5
index 49aaed6..bead9ed 100644
--- a/.machine_readable/compliance/reuse/dep5
+++ b/.machine_readable/compliance/reuse/dep5
@@ -52,3 +52,10 @@ License: MPL-2.0
 Files: cliff.toml
 Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}>
 License: MPL-2.0
+
+# Documentation prose is CC-BY-SA-4.0 (code/config is MPL-2.0).
+# Last-match-wins in the Debian copyright format, so this overrides the
+# `Files: *` default above for prose docs.
+Files: *.adoc *.md docs/* docs/**/*
+Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}>
+License: CC-BY-SA-4.0
diff --git a/.machine_readable/contractiles/must/Mustfile.a2ml b/.machine_readable/contractiles/must/Mustfile.a2ml
index badcedf..6577b73 100644
--- a/.machine_readable/contractiles/must/Mustfile.a2ml
+++ b/.machine_readable/contractiles/must/Mustfile.a2ml
@@ -57,7 +57,7 @@ These are hard requirements — CI fails if any check fails.
 - severity: warning
 
 ### no-agpl
-- description: No AGPL-3.0 references (superseded by PMPL)
+- description: No AGPL-3.0 references (superseded by MPL-2.0)
 - run: "! grep -r 'AGPL-3.0' .gitignore .gitattributes .editorconfig 2>/dev/null | head -1 | grep -q ."
 - severity: critical
 
diff --git a/.machine_readable/contractiles/trust/Trustfile.a2ml b/.machine_readable/contractiles/trust/Trustfile.a2ml
index 113a036..cc4c69f 100644
--- a/.machine_readable/contractiles/trust/Trustfile.a2ml
+++ b/.machine_readable/contractiles/trust/Trustfile.a2ml
@@ -33,8 +33,8 @@ is traceable.
 - severity: warning
 
 ### license-content
-- description: LICENSE contains PMPL identifier
-- run: grep -q 'PMPL' LICENSE
+- description: LICENSE contains MPL-2.0 identifier
+- run: grep -q 'MPL-2.0' LICENSE
 - severity: warning
 
 ### ci-pipeline-present
diff --git a/Cargo.toml b/Cargo.toml
index 250056d..eb2536c 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -5,7 +5,7 @@ version = "0.1.0"
 edition = "2024"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
 description = "Generate progressive-disclosure interfaces from complex APIs via My-Lang"
-license-file = "LICENSE"
+license = "MPL-2.0"
 repository = "https://github.com/hyperpolymath/mylangiser"
 keywords = ["mylang", "acceleration", "code-generation"]
 categories = ["command-line-utilities", "development-tools"]
diff --git a/LICENSE b/LICENSE
index 14e2f77..2a8b960 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,3 +1,5 @@
+SPDX-License-Identifier: MPL-2.0
+
 Mozilla Public License Version 2.0
 ==================================
 
diff --git a/QUICKSTART-MAINTAINER.adoc b/QUICKSTART-MAINTAINER.adoc
index 5bb1df8..363b9e0 100644
--- a/QUICKSTART-MAINTAINER.adoc
+++ b/QUICKSTART-MAINTAINER.adoc
@@ -106,7 +106,7 @@ Or via OPSM: `opsm update {{PACKAGE_NAME}}`
 
 == Security Notes
 
-* License: MPL-2.0 (Palimpsest License)
+* License: MPL-2.0 (code) / CC-BY-SA-4.0 (docs)
 * All dependencies SHA-pinned
 * `panic-attacker` scan results: link:INSTALL-SECURITY-REPORT.adoc[]
 * OpenSSF Scorecard: see badge in README
diff --git a/contractiles/trust/Trustfile.a2ml b/contractiles/trust/Trustfile.a2ml
index 82fa89b..9849f4b 100644
--- a/contractiles/trust/Trustfile.a2ml
+++ b/contractiles/trust/Trustfile.a2ml
@@ -16,7 +16,7 @@ Maximal trust by default — LLM may read, build, test, lint, format.
 
 ### license-content
 - description: LICENSE contains expected SPDX identifier
-- run: grep -q 'SPDX\|License\|MIT\|Apache\|PMPL\|MPL' LICENSE
+- run: grep -q 'SPDX\|MPL-2.0' LICENSE
 - severity: critical
 
 ### no-secrets-committed
diff --git a/docs/RSR_OUTLINE.adoc b/docs/RSR_OUTLINE.adoc
index 014b21c..8faf3bb 100644
--- a/docs/RSR_OUTLINE.adoc
+++ b/docs/RSR_OUTLINE.adoc
@@ -1,6 +1,6 @@
 = RSR Template Repository
 
-image:[Palimpsest-MPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"] image:[Palimpsest,link="https://github.com/hyperpolymath/palimpsest-license"]
+image:https://img.shields.io/badge/license-MPL--2.0-blue[MPL-2.0,link="LICENSES/MPL-2.0.txt"] image:https://img.shields.io/badge/docs-CC--BY--SA--4.0-blue[CC-BY-SA-4.0,link="LICENSES/CC-BY-SA-4.0.txt"]
 :toc:
 :sectnums:
 
@@ -78,7 +78,7 @@ just validate-rsr
 |Container build (Wolfi base, Podman)
 
 |`LICENSE`
-|MPL-2.0 (Palimpsest MPL)
+|MPL-2.0 (code) / CC-BY-SA-4.0 (docs)
 
 |`EXHIBIT-A-ETHICAL-USE.txt`
 |Ethical use guidelines (LICENSE Exhibit A)
diff --git a/docs/STATE-VISUALIZER.adoc b/docs/STATE-VISUALIZER.adoc
index 2af3297..4be8d44 100644
--- a/docs/STATE-VISUALIZER.adoc
+++ b/docs/STATE-VISUALIZER.adoc
@@ -87,7 +87,7 @@ CONTAINER ECOSYSTEM (Phase 2)
 
 REPO INFRASTRUCTURE
   .machine_readable/                ██████████ 100%    STATE/META/ECOSYSTEM active
-  Governance & License              ██████████ 100%    PMPL & Ethical use verified
+  Governance & License              ██████████ 100%    MPL-2.0 & Ethical use verified
   Development Shells (Nix/Guix)     ██████████ 100%    Reproducible env stable
 
 ─────────────────────────────────────────────────────────────────────────────
diff --git a/src/interface/abi/Foreign.idr b/src/interface/abi/Mylangiser/ABI/Foreign.idr
similarity index 100%
rename from src/interface/abi/Foreign.idr
rename to src/interface/abi/Mylangiser/ABI/Foreign.idr
diff --git a/src/interface/abi/Layout.idr b/src/interface/abi/Mylangiser/ABI/Layout.idr
similarity index 74%
rename from src/interface/abi/Layout.idr
rename to src/interface/abi/Mylangiser/ABI/Layout.idr
index f91930f..44b1212 100644
--- a/src/interface/abi/Layout.idr
+++ b/src/interface/abi/Mylangiser/ABI/Layout.idr
@@ -20,6 +20,8 @@ module Mylangiser.ABI.Layout
 import Mylangiser.ABI.Types
 import Data.Vect
 import Data.So
+import Data.Nat
+import Decidable.Equality
 
 %default total
 
@@ -33,24 +35,38 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
 paddingFor offset alignment =
   if offset `mod` alignment == 0
     then 0
-    else alignment - (offset `mod` alignment)
+    else minus alignment (offset `mod` alignment)
 
 ||| Proof that alignment divides aligned size
 public export
 data Divides : Nat -> Nat -> Type where
   DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m
 
+||| Decide whether @n divides @m, returning a constructive witness when it does.
+||| Division does NOT reduce during typechecking, so we verify the quotient by
+||| reconstructing m = q * n and checking it propositionally.
+public export
+decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m)
+decDivides Z m = Nothing
+decDivides (S k) m =
+  let q = div m (S k) in
+  case decEq m (q * (S k)) of
+    Yes prf => Just (DivideBy q prf)
+    No _    => Nothing
+
 ||| Round up to next alignment boundary
 public export
 alignUp : (size : Nat) -> (alignment : Nat) -> Nat
 alignUp size alignment =
   size + paddingFor size alignment
 
-||| Proof that alignUp produces aligned result
+||| Decide that @alignUp produces an @align-aligned result, returning a
+||| constructive Divides witness. The quotient cannot be reduced definitionally
+||| (division does not compute under the typechecker), so we verify it with the
+||| sound `decDivides` procedure defined below rather than asserting it.
 public export
-alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align)
-alignUpCorrect size align prf =
-  DivideBy ((size + paddingFor size align) `div` align) Refl
+alignUpAligned : (size : Nat) -> (align : Nat) -> Maybe (Divides align (alignUp size align))
+alignUpAligned size align = decDivides align (alignUp size align)
 
 --------------------------------------------------------------------------------
 -- Struct Field Layout
@@ -74,7 +90,7 @@ nextFieldOffset f = alignUp (f.offset + f.size) f.alignment
 public export
 record StructLayout where
   constructor MkStructLayout
-  fields : Vect n Field
+  fields : Vect len Field
   totalSize : Nat
   alignment : Nat
   {auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))}
@@ -82,7 +98,7 @@ record StructLayout where
 
 ||| Calculate total struct size with padding
 public export
-calcStructSize : Vect n Field -> Nat -> Nat
+calcStructSize : Vect k Field -> Nat -> Nat
 calcStructSize [] align = 0
 calcStructSize (f :: fs) align =
   let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs
@@ -91,23 +107,28 @@ calcStructSize (f :: fs) align =
 
 ||| Proof that field offsets are correctly aligned
 public export
-data FieldsAligned : Vect n Field -> Type where
+data FieldsAligned : Vect k Field -> Type where
   NoFields : FieldsAligned []
   ConsField :
     (f : Field) ->
-    (rest : Vect n Field) ->
+    (rest : Vect k Field) ->
     Divides f.alignment f.offset ->
     FieldsAligned rest ->
     FieldsAligned (f :: rest)
 
 ||| Verify a struct layout is valid
 public export
-verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout
+verifyLayout : (fields : Vect k Field) -> (align : Nat) -> Either String StructLayout
 verifyLayout fields align =
   let size = calcStructSize fields align
-   in case decSo (size >= sum (map (\f => f.size) fields)) of
-        Yes prf => Right (MkStructLayout fields size align)
-        No _ => Left "Invalid struct size"
+   in case choose (size >= sum (map (\f => f.size) fields)) of
+        Right _ => Left "Invalid struct size"
+        Left sizePrf =>
+          case decDivides align size of
+            Nothing => Left "Total size is not aligned"
+            Just alignPrf =>
+              Right (MkStructLayout fields size align
+                       {sizeCorrect = sizePrf} {aligned = alignPrf})
 
 ||| Proof that a struct follows C ABI rules
 public export
@@ -117,11 +138,26 @@ data CABICompliant : StructLayout -> Type where
     FieldsAligned layout.fields ->
     CABICompliant layout
 
+||| Decide whether every field's offset is aligned to its declared alignment,
+||| building a constructive FieldsAligned witness.
+public export
+decFieldsAligned : (fields : Vect k Field) -> Maybe (FieldsAligned fields)
+decFieldsAligned [] = Just NoFields
+decFieldsAligned (f :: fs) =
+  case decDivides f.alignment f.offset of
+    Nothing => Nothing
+    Just divPrf =>
+      case decFieldsAligned fs of
+        Nothing => Nothing
+        Just restPrf => Just (ConsField f fs divPrf restPrf)
+
 ||| Check if layout follows C ABI
 public export
 checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout)
 checkCABI layout =
-  Right (CABIOk layout ?fieldsAlignedProof)
+  case decFieldsAligned layout.fields of
+    Just prf => Right (CABIOk layout prf)
+    Nothing  => Left "Struct fields are not correctly aligned for the C ABI"
 
 --------------------------------------------------------------------------------
 -- API Surface Descriptor Layout
@@ -149,11 +185,8 @@ apiSurfaceLayout =
     ]
     24  -- Total size: 24 bytes
     8   -- Alignment: 8 bytes (due to u64 field)
-
-||| Proof that the API surface descriptor layout is C ABI compliant
-export
-apiSurfaceLayoutValid : CABICompliant Layout.apiSurfaceLayout
-apiSurfaceLayoutValid = CABIOk apiSurfaceLayout ?apiSurfaceFieldsAligned
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 3 Refl}  -- 24 = 3 * 8
 
 --------------------------------------------------------------------------------
 -- Endpoint Descriptor Layout
@@ -187,6 +220,8 @@ endpointDescriptorLayout =
     ]
     40  -- Total size: 40 bytes
     8   -- Alignment: 8 bytes (due to pointer field)
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 5 Refl}  -- 40 = 5 * 8
 
 --------------------------------------------------------------------------------
 -- Wrapper Descriptor Layout
@@ -220,6 +255,8 @@ wrapperDescriptorLayout =
     ]
     40  -- Total size: 40 bytes
     8   -- Alignment: 8 bytes
+    {sizeCorrect = Oh}
+    {aligned = DivideBy 5 Refl}  -- 40 = 5 * 8
 
 --------------------------------------------------------------------------------
 -- Platform-Specific Layouts
@@ -250,7 +287,13 @@ fieldOffset layout name =
     Just idx => Just (finToNat idx ** index idx layout.fields)
     Nothing => Nothing
 
-||| Proof that field offset is within struct bounds
+||| Decide whether a field lies within the struct's total size, returning a
+||| proof when it does. This is not universally true (a field may be declared
+||| outside the struct), so it must be checked rather than asserted.
 public export
-offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize)
-offsetInBounds layout f = ?offsetInBoundsProof
+offsetInBounds : (layout : StructLayout) -> (f : Field) ->
+                 Maybe (So (f.offset + f.size <= layout.totalSize))
+offsetInBounds layout f =
+  case choose (f.offset + f.size <= layout.totalSize) of
+    Left prf => Just prf
+    Right _  => Nothing
diff --git a/src/interface/abi/Mylangiser/ABI/Proofs.idr b/src/interface/abi/Mylangiser/ABI/Proofs.idr
new file mode 100644
index 0000000..0002efe
--- /dev/null
+++ b/src/interface/abi/Mylangiser/ABI/Proofs.idr
@@ -0,0 +1,93 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Machine-checked ABI theorems for Mylangiser.
+|||
+||| Each concrete StructLayout defined in Mylangiser.ABI.Layout is proven to be
+||| C-ABI compliant by constructing the FieldsAligned witness directly. For every
+||| field, offset = k * alignment, witnessed by `DivideBy k Refl` (multiplication
+||| reduces during typechecking; division does not, so the witnesses are built by
+||| hand rather than via decFieldsAligned).
+|||
+||| We also pin the FFI result-code encoding.
+
+module Mylangiser.ABI.Proofs
+
+import Mylangiser.ABI.Types
+import Mylangiser.ABI.Layout
+import Data.Vect
+
+%default total
+
+--------------------------------------------------------------------------------
+-- C-ABI compliance of the concrete layouts
+--------------------------------------------------------------------------------
+
+||| The API-surface descriptor layout obeys C-ABI field alignment.
+||| Field offsets: 0=0*4, 4=1*4, 8=2*4, 12=3*4, 16=2*8.
+export
+apiSurfaceCompliant : CABICompliant Layout.apiSurfaceLayout
+apiSurfaceCompliant =
+  CABIOk Layout.apiSurfaceLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 1 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+     NoFields)))))
+
+||| The endpoint descriptor layout obeys C-ABI field alignment.
+||| Field offsets: 0=0*8, 8=2*4, 12=3*4, 16=4*4, 20=5*4, 24=6*4, 28=7*4,
+||| 32=8*4, 36=9*4.
+export
+endpointDescriptorCompliant : CABICompliant Layout.endpointDescriptorLayout
+endpointDescriptorCompliant =
+  CABIOk Layout.endpointDescriptorLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 4 Refl)
+    (ConsField _ _ (DivideBy 5 Refl)
+    (ConsField _ _ (DivideBy 6 Refl)
+    (ConsField _ _ (DivideBy 7 Refl)
+    (ConsField _ _ (DivideBy 8 Refl)
+    (ConsField _ _ (DivideBy 9 Refl)
+     NoFields)))))))))
+
+||| The wrapper descriptor layout obeys C-ABI field alignment.
+||| Field offsets: 0=0*8, 8=2*4, 12=3*4, 16=4*4, 20=5*4, 24=6*4, 28=7*4,
+||| 32=8*4, 36=9*4.
+export
+wrapperDescriptorCompliant : CABICompliant Layout.wrapperDescriptorLayout
+wrapperDescriptorCompliant =
+  CABIOk Layout.wrapperDescriptorLayout
+    (ConsField _ _ (DivideBy 0 Refl)
+    (ConsField _ _ (DivideBy 2 Refl)
+    (ConsField _ _ (DivideBy 3 Refl)
+    (ConsField _ _ (DivideBy 4 Refl)
+    (ConsField _ _ (DivideBy 5 Refl)
+    (ConsField _ _ (DivideBy 6 Refl)
+    (ConsField _ _ (DivideBy 7 Refl)
+    (ConsField _ _ (DivideBy 8 Refl)
+    (ConsField _ _ (DivideBy 9 Refl)
+     NoFields)))))))))
+
+--------------------------------------------------------------------------------
+-- Result-code encoding
+--------------------------------------------------------------------------------
+
+||| The success code Ok encodes to the C integer 0.
+export
+okIsZero : resultToInt Ok = 0
+okIsZero = Refl
+
+||| The result-code encoding is injective on the first two codes:
+||| Ok and Error map to distinct integers, so the encoding distinguishes them.
+export
+okErrorDistinct : Not (resultToInt Ok = resultToInt Error)
+okErrorDistinct = \case Refl impossible
+
+||| Beginner is the least disclosure level: it encodes to 0.
+export
+beginnerIsZero : disclosureLevelToInt Beginner = 0
+beginnerIsZero = Refl
diff --git a/src/interface/abi/Types.idr b/src/interface/abi/Mylangiser/ABI/Types.idr
similarity index 74%
rename from src/interface/abi/Types.idr
rename to src/interface/abi/Mylangiser/ABI/Types.idr
index 58fa06f..f004b95 100644
--- a/src/interface/abi/Types.idr
+++ b/src/interface/abi/Mylangiser/ABI/Types.idr
@@ -20,6 +20,7 @@ module Mylangiser.ABI.Types
 import Data.Bits
 import Data.So
 import Data.Vect
+import Decidable.Equality
 
 %default total
 
@@ -32,13 +33,10 @@ public export
 data Platform = Linux | Windows | MacOS | BSD | WASM
 
 ||| Compile-time platform detection
-||| This will be set during compilation based on target
+||| This is set to the default target; override with compiler flags.
 public export
 thisPlatform : Platform
-thisPlatform =
-  %runElab do
-    -- Platform detection logic
-    pure Linux  -- Default, override with compiler flags
+thisPlatform = Linux
 
 --------------------------------------------------------------------------------
 -- Disclosure Levels
@@ -112,9 +110,9 @@ record ComplexityScore where
 public export
 mkComplexityScore : Bits32 -> Maybe ComplexityScore
 mkComplexityScore s =
-  case decSo (s <= 100) of
-    Yes prf => Just (MkComplexityScore s)
-    No _    => Nothing
+  case choose (s <= 100) of
+    Left prf  => Just (MkComplexityScore s {inBounds = prf})
+    Right _   => Nothing
 
 ||| Determine which disclosure level an endpoint belongs to based on score.
 ||| Thresholds: 0-33 -> Beginner, 34-66 -> Intermediate, 67-100 -> Expert
@@ -198,12 +196,18 @@ record LayeredWrapper where
   ||| Smart defaults applied at @beginner level
   defaultCount   : Bits32
 
-||| Proof that each layer exposes a non-decreasing number of parameters
+||| Decision procedure: does this wrapper expose a non-decreasing number of
+||| parameters across the three disclosure layers? Returns a proof when it does,
+||| Nothing otherwise (the property is not universally true — it must be checked).
 public export
 layerMonotonic : (w : LayeredWrapper) ->
-  So (w.beginnerParams <= w.intermediateParams &&
-      w.intermediateParams <= w.expertParams)
-layerMonotonic w = ?layerMonotonicProof
+  Maybe (So (w.beginnerParams <= w.intermediateParams &&
+             w.intermediateParams <= w.expertParams))
+layerMonotonic w =
+  case choose (w.beginnerParams <= w.intermediateParams &&
+               w.intermediateParams <= w.expertParams) of
+    Left prf => Just prf
+    Right _  => Nothing
 
 --------------------------------------------------------------------------------
 -- Result Codes
@@ -249,7 +253,49 @@ DecEq Result where
   decEq NullPointer NullPointer = Yes Refl
   decEq EndpointNotFound EndpointNotFound = Yes Refl
   decEq InvalidScore InvalidScore = Yes Refl
-  decEq _ _ = No absurd
+  -- Off-diagonal: every ordered pair of distinct constructors is decidably unequal.
+  decEq Ok Error = No (\case Refl impossible)
+  decEq Ok InvalidParam = No (\case Refl impossible)
+  decEq Ok OutOfMemory = No (\case Refl impossible)
+  decEq Ok NullPointer = No (\case Refl impossible)
+  decEq Ok EndpointNotFound = No (\case Refl impossible)
+  decEq Ok InvalidScore = No (\case Refl impossible)
+  decEq Error Ok = No (\case Refl impossible)
+  decEq Error InvalidParam = No (\case Refl impossible)
+  decEq Error OutOfMemory = No (\case Refl impossible)
+  decEq Error NullPointer = No (\case Refl impossible)
+  decEq Error EndpointNotFound = No (\case Refl impossible)
+  decEq Error InvalidScore = No (\case Refl impossible)
+  decEq InvalidParam Ok = No (\case Refl impossible)
+  decEq InvalidParam Error = No (\case Refl impossible)
+  decEq InvalidParam OutOfMemory = No (\case Refl impossible)
+  decEq InvalidParam NullPointer = No (\case Refl impossible)
+  decEq InvalidParam EndpointNotFound = No (\case Refl impossible)
+  decEq InvalidParam InvalidScore = No (\case Refl impossible)
+  decEq OutOfMemory Ok = No (\case Refl impossible)
+  decEq OutOfMemory Error = No (\case Refl impossible)
+  decEq OutOfMemory InvalidParam = No (\case Refl impossible)
+  decEq OutOfMemory NullPointer = No (\case Refl impossible)
+  decEq OutOfMemory EndpointNotFound = No (\case Refl impossible)
+  decEq OutOfMemory InvalidScore = No (\case Refl impossible)
+  decEq NullPointer Ok = No (\case Refl impossible)
+  decEq NullPointer Error = No (\case Refl impossible)
+  decEq NullPointer InvalidParam = No (\case Refl impossible)
+  decEq NullPointer OutOfMemory = No (\case Refl impossible)
+  decEq NullPointer EndpointNotFound = No (\case Refl impossible)
+  decEq NullPointer InvalidScore = No (\case Refl impossible)
+  decEq EndpointNotFound Ok = No (\case Refl impossible)
+  decEq EndpointNotFound Error = No (\case Refl impossible)
+  decEq EndpointNotFound InvalidParam = No (\case Refl impossible)
+  decEq EndpointNotFound OutOfMemory = No (\case Refl impossible)
+  decEq EndpointNotFound NullPointer = No (\case Refl impossible)
+  decEq EndpointNotFound InvalidScore = No (\case Refl impossible)
+  decEq InvalidScore Ok = No (\case Refl impossible)
+  decEq InvalidScore Error = No (\case Refl impossible)
+  decEq InvalidScore InvalidParam = No (\case Refl impossible)
+  decEq InvalidScore OutOfMemory = No (\case Refl impossible)
+  decEq InvalidScore NullPointer = No (\case Refl impossible)
+  decEq InvalidScore EndpointNotFound = No (\case Refl impossible)
 
 --------------------------------------------------------------------------------
 -- Opaque Handles
@@ -265,8 +311,10 @@ data Handle : Type where
 ||| Returns Nothing if pointer is null
 public export
 createHandle : Bits64 -> Maybe Handle
-createHandle 0 = Nothing
-createHandle ptr = Just (MkHandle ptr)
+createHandle ptr =
+  case choose (ptr /= 0) of
+    Left ok => Just (MkHandle ptr {nonNull = ok})
+    Right _ => Nothing
 
 ||| Extract pointer value from handle
 public export
@@ -304,10 +352,17 @@ ptrSize MacOS = 64
 ptrSize BSD = 64
 ptrSize WASM = 32
 
-||| Pointer type for platform
+||| Pointer type for platform.
+||| Represented as a platform-word-sized integer (the pointee type is phantom,
+||| recording the intended target type without affecting the representation):
+||| 64-bit words on Linux/Windows/MacOS/BSD, 32-bit on WASM.
 public export
 CPtr : Platform -> Type -> Type
-CPtr p _ = Bits (ptrSize p)
+CPtr Linux   _ = Bits64
+CPtr Windows _ = Bits64
+CPtr MacOS   _ = Bits64
+CPtr BSD     _ = Bits64
+CPtr WASM    _ = Bits32
 
 --------------------------------------------------------------------------------
 -- Memory Layout Proofs
diff --git a/src/interface/abi/mylangiser-abi.ipkg b/src/interface/abi/mylangiser-abi.ipkg
new file mode 100644
index 0000000..7bbc742
--- /dev/null
+++ b/src/interface/abi/mylangiser-abi.ipkg
@@ -0,0 +1,9 @@
+-- SPDX-License-Identifier: MPL-2.0
+package mylangiser-abi
+
+sourcedir = "."
+
+modules = Mylangiser.ABI.Types
+        , Mylangiser.ABI.Layout
+        , Mylangiser.ABI.Foreign
+        , Mylangiser.ABI.Proofs