From 53cb928a9b677fdfa6727076584da0c3209081f9 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 10:41:33 +0000 Subject: [PATCH 1/2] 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 Claude-Session: https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn --- lol/src/Lol/ABI/I18nStore.idr | 29 ++++++++++++++++------------- lol/src/Lol/ABI/Layout.idr | 28 +++++++++++++++++++++------- 2 files changed, 37 insertions(+), 20 deletions(-) diff --git a/lol/src/Lol/ABI/I18nStore.idr b/lol/src/Lol/ABI/I18nStore.idr index 5e73aef0..3f2355f0 100644 --- a/lol/src/Lol/ABI/I18nStore.idr +++ b/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 diff --git a/lol/src/Lol/ABI/Layout.idr b/lol/src/Lol/ABI/Layout.idr index 6606c884..5f518983 100644 --- a/lol/src/Lol/ABI/Layout.idr +++ b/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 From 152e07758967f57042ca0c372354aa25b277522b Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 18 Jun 2026 10:59:23 +0000 Subject: [PATCH 2/2] chore(registry): regenerate REGISTRY.a2ml to clear pre-existing drift MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `scripts/build-registry.sh --check` (the "Registry + topology in sync" gate) failed on this PR: the recorded source_hash for the consent-aware-http/ spec was stale. This is a PRE-EXISTING drift on the branch, unrelated to the lol/abi Idris fix (lol/ is not a registered spec home). Regenerated via the sanctioned generator `bash scripts/build-registry.sh` — the file MUST NOT be hand-edited. Only the consent-aware-http/ source_hash changed; TOPOLOGY.md was already in sync. This is an index content-hash update, not a license or content change to the carve-out repo. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn --- .machine_readable/REGISTRY.a2ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.machine_readable/REGISTRY.a2ml b/.machine_readable/REGISTRY.a2ml index 7b2956c2..1677c076 100644 --- a/.machine_readable/REGISTRY.a2ml +++ b/.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]]