fix(lol/abi): make the lol-abi Idris package typecheck

The lol-abi.ipkg package did not build. All failures were in
estate-authored (MPL-2.0) modules; fixed without any believe_me or holes.

Layout.idr:
- Every MkStructLayout left its erased `aligned : Divides alignment
  totalSize` auto-implicit to proof search, which cannot guess the
  quotient k. Supplied it explicitly per layout via
  {aligned = DivideBy k Refl} (32=4*8, 24=3*8, 56=7*8, 40=5*8, 16=4*4).
- paddingFor used `-` on Nat, resolving to a nonexistent `Neg Nat`;
  switched to truncating `minus`.
- Removed the unused `alignUpCorrect` lemma: its `Refl` body asserted
  `n = (n `div` a) * a`, which only holds definitionally for concrete
  args, so it never typechecked. A correct general proof needs the
  division theorem (absent from Idris2 base); the divisibility the
  concrete layouts need is discharged per-layout by the explicit
  DivideBy witnesses. Documented as future work.

I18nStore.idr:
- extractLanguage used Data.List1.split (wants a List) on a String;
  switched to Data.String.split.
- LookupError used `data X = .. | ..` with per-constructor `|||` doc
  comments (only valid in GADT form); converted to
  `data LookupError : Type where`.
- The CorrectStore interface ended with a dangling `|||` doc comment
  (no method after it), breaking the block's scope so the following
  top-level `data LookupError` failed to register; demoted to a plain
  comment.

`idris2 --build lol-abi.ipkg` now exits 0 (pre-existing shadowing
warnings only).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn

Author: claude

lol/src/Lol/ABI/I18nStore.idr

@@ -26,6 +26,7 @@ import Lol.ABI.PluralForm
 import Data.So
 import Data.List
 import Data.List1
+import Data.String
 
 %default total
 
@@ -150,7 +151,7 @@ lookupWithFallback lookupFn strategy reqLocale defLocale key =
 ||| "en-US" -> "en", "zh-Hans-CN" -> "zh"
 public export
 extractLanguage : String -> String
-extractLanguage s = let (lang ::: _) = split (== '-') s in lang
+extractLanguage s = let (lang ::: _) = Data.String.split (== '-') s in lang
 
 ||| Convert a plural category to its CLDR string suffix.
 public export
@@ -213,9 +214,11 @@ interface I18nStore store => CorrectStore (store : Type) where
     (prf : KeyExists locale key) ->
     lookup st locale key = Just (guaranteedLookup st prf)
 
-  ||| The store is monotonic: adding translations never removes existing ones
-  ||| (expressed as: if a key exists, it continues to exist)
-  ||| This is an invariant the Zig store must maintain.
+  -- The store is monotonic: adding translations never removes existing ones
+  -- (expressed as: if a key exists, it continues to exist). Stated as a plain
+  -- comment, not a `|||` doc comment: a trailing doc comment with no method
+  -- following it is dangling and breaks the interface block's scope. This
+  -- invariant is enforced on the Zig store side, not provable generically here.
 
 --------------------------------------------------------------------------------
 -- Error Classification
@@ -224,15 +227,15 @@ interface I18nStore store => CorrectStore (store : Type) where
 ||| Classification of lookup failures for error reporting.
 ||| The Zig FFI maps these to the Result enum in Types.idr.
 public export
-data LookupError
-  = ||| The requested locale is not in the corpus at all
-    NoSuchLocale String
-  | ||| The locale exists but the key is not defined
-    NoSuchKey String String
-  | ||| The plural form variant is missing (e.g. "items.few" missing)
-    MissingPluralForm String String PluralCategory
-  | ||| The entire fallback chain was exhausted without finding a translation
-    FallbackExhausted String String (List String)
+data LookupError : Type where
+  ||| The requested locale is not in the corpus at all
+  NoSuchLocale : String -> LookupError
+  ||| The locale exists but the key is not defined
+  NoSuchKey : String -> String -> LookupError
+  ||| The plural form variant is missing (e.g. "items.few" missing)
+  MissingPluralForm : String -> String -> PluralCategory -> LookupError
+  ||| The entire fallback chain was exhausted without finding a translation
+  FallbackExhausted : String -> String -> List String -> LookupError
 
 ||| Map a lookup error to the appropriate Result code for FFI transport
 public export

lol/src/Lol/ABI/Layout.idr

@@ -32,7 +32,7 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat
 paddingFor offset alignment =
   if offset `mod` alignment == 0
     then 0
-    else alignment - (offset `mod` alignment)
+    else alignment `minus` (offset `mod` alignment)
 
 ||| Proof that alignment divides aligned size
 public export
@@ -45,12 +45,21 @@ alignUp : (size : Nat) -> (alignment : Nat) -> Nat
 alignUp size alignment =
   size + paddingFor size alignment
 
-||| Proof that alignUp produces an aligned result.
-||| For any positive alignment, (alignUp s a) is divisible by a.
-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
+-- NOTE (2026-06-18): a general lemma
+--   alignUpCorrect : (size, align : Nat) -> So (align > 0)
+--                 -> Divides align (alignUp size align)
+-- was removed here. It was unused, and its body asserted
+--   alignUp size align = (alignUp size align `div` align) * align
+-- via `Refl`, which only holds definitionally for *concrete* arguments, not
+-- symbolic ones, so the lemma did not actually typecheck. A correct general
+-- proof needs the division theorem (n = d * (n `div` d) + n `mod` d), which
+-- Idris2 `base` does not export (only the `divNatNZ`/`modNatNZ`/`divmod'`
+-- functions exist, with no accompanying equational lemma), so it would have to
+-- be hand-proved from `Data.Nat.divmod'`. The divisibility that the concrete
+-- struct layouts actually rely on is discharged per-layout below by the
+-- explicit `{aligned = DivideBy k Refl}` witnesses (which compute, since the
+-- sizes/alignments there are concrete). Re-introducing the general lemma with a
+-- real proof is tracked as future work, not a `believe_me`.
 
 --------------------------------------------------------------------------------
 -- Struct Field Layout
@@ -117,6 +126,7 @@ localeLayout =
     ]
     32  -- Total size: 32 bytes
     8   -- Alignment: 8 bytes (pointer alignment)
+    {aligned = DivideBy 4 Refl}   -- 32 = 4 * 8
 
 ||| Layout of lol_translation_result_t.
 |||
@@ -138,6 +148,7 @@ translationResultLayout =
     ]
     24  -- Total size: 24 bytes
     8   -- Alignment: 8 bytes
+    {aligned = DivideBy 3 Refl}   -- 24 = 3 * 8
 
 ||| Layout of lol_language_info_t.
 |||
@@ -167,6 +178,7 @@ languageInfoLayout =
     ]
     56  -- Total size: 56 bytes
     8   -- Alignment: 8 bytes
+    {aligned = DivideBy 7 Refl}   -- 56 = 7 * 8
 
 ||| Layout of lol_plural_rule_t.
 |||
@@ -188,6 +200,7 @@ pluralRuleLayout =
     ]
     40  -- Total size: 40 bytes
     8   -- Alignment: 8 bytes
+    {aligned = DivideBy 5 Refl}   -- 40 = 5 * 8
 
 --------------------------------------------------------------------------------
 -- C ABI Compatibility Proofs
@@ -243,3 +256,4 @@ localeLayoutWasm32 =
     ]
     16  -- Total size: 16 bytes on WASM32
     4   -- Alignment: 4 bytes
+    {aligned = DivideBy 4 Refl}   -- 16 = 4 * 4