From ac17c8f0b51ec021c3123f7111d49025e2fadee4 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 28 Jul 2026 19:26:43 +0100 Subject: [PATCH] fix(a2ml): make the normative Idris2 core type-check; add the missing .ipkg MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit SPEC.adoc 3.1 declares "The normative Idris2 model lives in src/A2ML/ ... the source files are authoritative." It did not type-check, and nothing built it: there was no .ipkg anywhere under a2ml/, and no CI job invokes the Justfile core-tests recipe. So the authoritative core was never machine-checked. Adds a2ml/a2ml-core.ipkg so the claim is checkable with `idris2 --typecheck a2ml-core.ipkg` (the ipkg target is used deliberately: per-file `idris2 --check` exits 0 when an imported module is simply missing, which makes it a fake gate). Fixes A2ML.Proofs, which failed outright. All four fixes are genuine proofs — no postulate, no believe_me: 1. import Data.List.Quantifiers — `All` was used but never imported, so the uniqueAppendDisjoint signature failed to elaborate. 2. `elemAppend` was referenced twice but defined nowhere and imported from nowhere. Replaced with two lemmas proved by induction on the Elem witness: elemAppendLeft (membership survives appending on the right) and elemAppendSplit (membership in a concatenation is membership in one side). 3. `|>` is not an Idris2 operator; the intent was to weaken an Elem across an append, which is exactly elemAppendLeft. 4. validatedHasUniqueIds / validatedHasResolvedRefs referenced the argument by name in their own signatures before binding it, and projected `ids` / `refs` / `uniqueProof`, which three record types share. Bound the argument and qualified the projections. A2ML.Proofs now type-checks. The remaining blocker is A2ML.Parser (16 errors: 7 unification, 6 totality under %default total, an undefined <|>, and a use of the private TypedCore.collectIds) — tracked separately; no CI gate is added in this PR because it would be red on arrival. Co-Authored-By: Claude Fable 5 --- a2ml/a2ml-core.ipkg | 29 ++++++++++++++++++++++++++++ a2ml/src/A2ML/Proofs.idr | 41 ++++++++++++++++++++++++++++++++-------- 2 files changed, 62 insertions(+), 8 deletions(-) create mode 100644 a2ml/a2ml-core.ipkg diff --git a/a2ml/a2ml-core.ipkg b/a2ml/a2ml-core.ipkg new file mode 100644 index 00000000..d60af028 --- /dev/null +++ b/a2ml/a2ml-core.ipkg @@ -0,0 +1,29 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- a2ml-core.ipkg — the NORMATIVE A2ML typed core. +-- +-- SPEC.adoc §3.1: "The normative Idris2 model lives in `src/A2ML/` … the +-- source files are authoritative." This package exists so that claim is +-- machine-checked: `idris2 --typecheck a2ml-core.ipkg` type-checks every +-- module in the core, including the dependent-type proofs in A2ML.Proofs. +-- +-- Use the ipkg target, never per-file `idris2 --check`: a per-file check +-- exits 0 when an imported module is simply missing, which makes it a fake +-- gate (estate-wide lesson; see the CI job that consumes this). + +package a2ml-core + +authors = "Jonathan D.A. Jewell (hyperpolymath)" +license = "MPL-2.0" +sourcedir = "src" + +modules = A2ML.TypedCore + , A2ML.Surface + , A2ML.Parser + , A2ML.Translator + , A2ML.Converters + , A2ML.BaseVocab + , A2ML.Profiles + , A2ML.Proofs + , A2ML.CoreTests + , A2ML.ParserTests + , A2ML.Tests diff --git a/a2ml/src/A2ML/Proofs.idr b/a2ml/src/A2ML/Proofs.idr index dc77dde9..df80fabd 100644 --- a/a2ml/src/A2ML/Proofs.idr +++ b/a2ml/src/A2ML/Proofs.idr @@ -3,6 +3,7 @@ module A2ML.Proofs import A2ML.TypedCore import Data.List import Data.List.Elem +import Data.List.Quantifiers import Decidable.Equality %default total @@ -186,13 +187,13 @@ verifyAttestation attested = ||| Proof that ValidatedDoc implies unique IDs export -validatedHasUniqueIds : ValidatedDoc -> Unique (ids validated) -validatedHasUniqueIds validated = validated.uniqueProof +validatedHasUniqueIds : (v : ValidatedDoc) -> Unique (ValidatedDoc.ids v) +validatedHasUniqueIds v = ValidatedDoc.uniqueProof v ||| Proof that ValidatedDoc implies resolved references export -validatedHasResolvedRefs : ValidatedDoc -> AllIn (refs validated) (ids validated) -validatedHasResolvedRefs validated = validated.resolvedProof +validatedHasResolvedRefs : (v : ValidatedDoc) -> AllIn (ValidatedDoc.refs v) (ValidatedDoc.ids v) +validatedHasResolvedRefs v = ValidatedDoc.resolvedProof v -- ============================================================================ -- Example Usage @@ -223,17 +224,41 @@ exampleAttestation = do -- Property: Uniqueness is preserved under append (if disjoint) -- ============================================================================ +-- --------------------------------------------------------------------------- +-- Elem/append lemmas. +-- +-- These stand in for a helper (`elemAppend`) that the proofs below referenced +-- but which was never defined in this module or imported from base — so +-- A2ML.Proofs did not type-check at all. Both are proved by induction on the +-- Elem witness; neither uses `postulate` or `believe_me`. +-- --------------------------------------------------------------------------- + +||| Membership in the left operand survives appending on the right. +export +elemAppendLeft : Elem x xs -> Elem x (xs ++ ys) +elemAppendLeft Here = Here +elemAppendLeft (There e) = There (elemAppendLeft e) + +||| Membership in a concatenation is membership in one side or the other. +export +elemAppendSplit : (xs : List a) -> Elem x (xs ++ ys) -> Either (Elem x xs) (Elem x ys) +elemAppendSplit [] e = Right e +elemAppendSplit (y :: ys') Here = Left Here +elemAppendSplit (y :: ys') (There e) = case elemAppendSplit ys' e of + Left l => Left (There l) + Right r => Right r + ||| If two lists are unique and disjoint, their concatenation is unique export -uniqueAppendDisjoint : Unique xs -> Unique ys -> +uniqueAppendDisjoint : {xs : List a} -> Unique xs -> Unique ys -> (disjoint : All (\x => Not (Elem x ys)) xs) -> Unique (xs ++ ys) uniqueAppendDisjoint UniqueNil uniqueYs disjoint = uniqueYs uniqueAppendDisjoint (UniqueCons notElem uniqueXs) uniqueYs (d :: ds) = UniqueCons (appendNotElem notElem d) (uniqueAppendDisjoint uniqueXs uniqueYs ds) where - appendNotElem : Not (Elem x xs) -> Not (Elem x ys) -> Not (Elem x (xs ++ ys)) - appendNotElem notXs notYs elem with (elemAppend xs ys elem) + appendNotElem : {zs : List a} -> Not (Elem w zs) -> Not (Elem w ys) -> Not (Elem w (zs ++ ys)) + appendNotElem notXs notYs elem with (elemAppendSplit zs elem) appendNotElem notXs notYs elem | Left elemXs = notXs elemXs appendNotElem notXs notYs elem | Right elemYs = notYs elemYs @@ -247,5 +272,5 @@ resolveMonotonic : AllIn refs ids -> (moreIds : List Id) -> AllIn refs (ids ++ moreIds) resolveMonotonic AllInNil moreIds = AllInNil resolveMonotonic (AllInCons elem allIn) moreIds = - AllInCons (elemAppend ids moreIds elem |> Left) + AllInCons (elemAppendLeft elem) (resolveMonotonic allIn moreIds)