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

## Summary

First unit of bringing **standards** toward proof/RSR compliance:
**making the `lol-abi` Idris package typecheck** (it previously did not
build at all). `lol/` is hyperpolymath's port of Ehsaneddin Asgari's
*1000Langs*; the Idris ABI modules fixed here are estate-authored
(`MPL-2.0`).

`idris2 --build lol-abi.ipkg` now exits 0 (pre-existing shadowing
warnings only). **No `believe_me`, no holes.**

## `Layout.idr`
- Every `MkStructLayout` left its erased `aligned : Divides alignment
totalSize` auto-implicit to proof search, which cannot guess the
quotient `k`. Supplied 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` (resolves to a nonexistent `Neg Nat`) →
truncating `minus`.
- Removed the **unused, unsound** `alignUpCorrect` lemma: its `Refl`
body asserted `n = (n div a)·a`, true only for concrete args. A correct
general proof needs the division theorem (absent from Idris2 `base`);
the divisibility the real 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` → `Data.String.split`.
- `LookupError` used `data X = .. | ..` with per-constructor `|||` doc
comments (only valid in GADT form) → `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.

## Flagged for owner (NOT touched — license guardrail)
- **`lol/proofs/theories/information_theory.agda`** is
third-party-attributed (`MIT AND LicenseRef-Palimpsest-0.8`, ©
Ehsaneddin Asgari). It has a trivial syntax bug (illegal `where` inside
`postulate`), but editing a third-party-attributed file is owner-only —
**left untouched, flagged**.
- **`rhodium-standard-repositories/rsr-audit.sh`** hardcodes `MIT AND
Palimpsest` as the required license, contradicting the estate's current
MPL-2.0-for-sole-owner policy. Updating what license the standard
mandates is owner-only — **flagged, not changed**. RSR
format-brittleness fixes + real gaps (`.well-known`, Justfile
`validate`) will follow on this branch.

> Note: the branch history carries a pre-existing merge commit
(`66271d3`) not introduced by this work.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn

---
_Generated by [Claude
Code](https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.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