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

.machine_readable/REGISTRY.a2ml

@@ -171,7 +171,7 @@ name = "Consent-Aware HTTP"
 stream = "protocol"
 home = "consent-aware-http/"
 canonical_doc = "consent-aware-http/README.adoc"
-source_hash = "sha256:dbfc1d464ac7e9098d8115dda332eff832276b643bcea787a5f9b3900f09142b"
+source_hash = "sha256:fb2611536673928bd3ac6ac6f6097b431e2a6a6114f609674c6e9287f0c1f1e1"
 route = "consent headers / AI-usage boundaries for HTTP"
 
 [[spec]]

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