audit: 2 Idris2 postulates in src/abi/Layout.idr — alignment + alignedSize correctness #27

Activity

1. hyperpolymath commented on May 24, 2026

   

   hyperpolymath

   on May 24, 2026 – with Claude

   OwnerAuthor

   More actions

   Worked through this — pushed claude/upbeat-mendel-lBO9G (commit aac48b7). One important audit finding before the mechanical part:

   Finding: the two postulates are not symmetric

   alignmentMatchesPlatformWord is unsound, not merely unproven

   HasAlignment t n is defined with a single information-free constructor:

   data HasAlignment : Type -> Nat -> Type where
     AlignProof : {0 t : Type} -> {n : Nat} -> HasAlignment t n

   so the postulate's HasAlignment t n -> So (n mod(ptrSize pdiv 8) == 0) quantifies over an n it has no evidence about. Concrete counterexample from the same file:

   CNOResultLayout.alignment : HasAlignment CNOVerificationResult 1

   Feed that to the postulate and you derive So (1 mod 8 == 0) ≡ So False. The unsoundness was hidden because the only consumer (programStateAlignmentValid) instantiated n at 8 — where the claim happens to hold on every supported platform.

   This is not in the same category as civic-connect's alignUpDivides (a genuine Nat-mod lemma). It's a load-bearing axiom that should never have shipped, and "moving the obligation to the producer" doesn't rescue it — the producer of AlignProof is anyone, including the lib itself for n=1.

   alignedSizeCorrect is a genuine deferred Nat lemma, but currently has zero consumers in-tree

   It's a forward-looking placeholder for the cross-estate div/mod work the issue describes. Worth keeping the signature, but it doesn't need to sit in Layout.idr.

   Fix applied

   1. Delete alignmentMatchesPlatformWord (unsound, see above).
   2. Re-prove programStateAlignmentValid directly by Platform case-split — every case reduces to So True so Oh discharges it. No axiom required.
   3. Drop verifyAlignment — orphan helper whose only purpose was calling the postulate.
   4. Move alignedSize + alignedSizeCorrect into a new shared module AbsoluteZero.ABI.Proofs.DivMod, structured as the estate-wide trusted div/mod surface:
      • Each lemma is an individually-named declaration, so discharge can be incremental (one Qed at a time, no consumer churn).
      • Names match the civic-connect deferrals' intent so alignUpDivides, mkFieldsAligned, offsetInBoundsPrf can migrate onto the same module rather than re-postulating per-repo.
      • Adjacent lemmas (divModIdentity, multModZero, addModDistrib) are stated explicitly so the proof reduction path is documented in the trusted base itself.
   5. Layout.idr re-exports alignedSize to preserve the public API.
   6. ADR-009 added to META.scm matching the project's audit-trail pattern (ADR-007/ADR-008).

   Net effect on the trusted base

   	Before	After
   Unsound axioms in src/abi/	1 (alignmentMatchesPlatformWord)	0
   Genuine deferred Nat lemmas	1 (alignedSizeCorrect, in Layout)	4 (in Proofs/DivMod.idr, but each individually trackable and shared with civic-connect)
   Module hosting the deferrals	src/abi/Layout.idr (mixed with concrete layout decls)	dedicated src/abi/Proofs/DivMod.idr

   The increase from 1→4 trusted lemmas is intentional: alignedSizeCorrect was previously a single postulate that hid three sub-obligations. Naming them surfaces the actual reduction path and lets civic-connect / other repos depend on the named lemmas rather than the composite.

   Upstream coordination

   The Proofs/DivMod.idr module documents (in its header + alignedSizeCorrect comment) that civic-connect's three deferrals should migrate to import from here rather than restating in each repo. That's a separate PR over there — happy to follow up if you want it raised.

   Caveat

   No Idris2 compiler is present in this environment / not wired into CI (Justfile has no build-idris2 target), so the changes are validated by inspection only. The pattern (Oh : So True after concrete Platform case-split, qualified re-export via DivMod.alignedSize) is standard and should typecheck, but worth a local idris2 --check before merge. Adding an Idris2 target to the Justfile would be a sensible follow-up so this whole module stops being a CI blind spot.

   Branch: claude/upbeat-mendel-lBO9G — no PR opened (per instructions, awaiting your call).

   ---

   Generated by Claude Code
2. hyperpolymath

   added a commit that references this issue on May 24, 2026

   proof(idris2/abi): delete unsound alignmentMatchesPlatformWord, isola… (

   ...

   4ff2e72
3. hyperpolymath commented on May 25, 2026

   

   hyperpolymath

   on May 25, 2026 – with Claude

   OwnerAuthor

   More actions

   Followup with idris2 0.8.0 now bootstrapped locally (Chez Scheme + libgmp from apt, then make bootstrap && make install to ~/.idris2). Two findings beyond the original audit:

   Finding 1: postulate doesn't parse in Idris2 0.8.0

   The postulate keyword has been removed; it now only survives as an IDE-protocol decoration tag (/tmp/Idris2/src/Protocol/IDE/Decoration.idr). So the original Layout.idr postulate syntax was never valid in the current compiler. The whole Idris2 surface in src/abi/ had been silently non-buildable — no build-idris2 target in Justfile to surface it.

   Canonical idiom for an axiom in Idris2 0.8.0:

   name : Ty
   name = believe_me ()

   Same semantic content as postulate, but each axiom is now grep-able as a believe_me occurrence in the trusted base.

   Finding 2: programStateAlignmentValid doesn't reduce via Oh even with concrete Platform

   The earlier comment claimed the discharge would be Oh : So True after Platform case-split. With the actual compiler in hand: it doesn't. Idris2 0.8.0 refuses to reduce through divNat's non-covering case (divNat _ Z has no clause) at type-level, even when both args are concrete literals after substitution. Minimal repro:

   data Platform = Linux
   public export
   ptrSize : Platform -> Nat
   ptrSize Linux = 64
   
   test : (p : Platform) -> So (8 `mod` (ptrSize p `div` 8) == 0)
   test Linux = Oh
   -- Error: Can't solve constraint between: True and
   --        equalNat (8 `mod` (ptrSize Linux `div` 8)) 0

   So the new programStateAlignmentValid is now also a believe_me () — but explicitly distinguished from the deleted unsound postulate:

   • Per-instance (n=8 only), not universal — no consumer can pivot from it to derive False.
   • The claim is computationally true; the gap is the unifier's reduction strategy, not the proposition itself.
   • Discharge becomes mechanical once Proofs.DivMod exports the explicit ptrSize p → concrete value rewrite equations to drive the proof.

   Other pre-existing breakage in src/abi/Types.idr (out of scope for #27)

   Surfacing for a separate audit issue:

   • import Decidable.Equality is missing (DecEq instances fail).
   • thisPlatform uses %runElab without %language ElabReflection.
   • createStateHandle ptr = Just (MkStateHandle ptr) and the program-handle equivalent: the catch-all branch doesn't supply the constructor's auto So (ptr /= 0) proof. Needs a choose-based case-split.
   • decEq _ _ = No absurd lacks an Uninhabited (Ctor1 = Ctor2) instance; needs explicit \Refl impossible lambdas per constructor pair (or a believe_me if hand-enumeration is too much).

   What's pushed (commit f0f9b8f, on top of aac48b7)

   • src/abi/Proofs/DivMod.idr rewritten to compile under Idris2 0.8.0 (believe_me axiom pattern; align minus remainder instead of align - remainder). Verified: idris2 --check clean.
   • src/abi/Layout.idr programStateAlignmentValid routed through believe_me with the distinguishing rationale above.
   • Added absolute-zero-abi.ipkg so idris2 --build absolute-zero-abi becomes a real CI target. Would recommend wiring this into Justfile as build-idris2 to prevent silent breakage from happening again — that's likely the highest-leverage followup.

   Net effect

   	Before	After this PR
   Unsound axioms in src/abi/	1 (alignmentMatchesPlatformWord)	0
   believe_me axioms (issue #27 surface)	0 (postulate syntax errors; whole module non-buildable)	4 in Proofs/DivMod.idr + 1 in Layout.idr, each individually named/audit-trackable
   Idris2 module typechecks under 0.8.0	No (postulate parse errors throughout)	Yes for Proofs/DivMod.idr standalone; Layout.idr blocked only by pre-existing Types.idr errors

   Branch claude/upbeat-mendel-lBO9G — still no PR opened per instructions.

   ---

   Generated by Claude Code
4. hyperpolymath

   added 3 commits that reference this issue on May 25, 2026

   proof(idris2/abi): port to Idris2 0.8.0 syntax; add ipkg for verifiab…

   ...

   a9f4350

   docs: Phase 1 per-axiom triage of 72 Coq Axioms (#58)

   ...

   e17256b

   refactor(proofs/coq): consolidate trusted-base dups (Follow-ups 1+2+3) (

   ...

   0b9b215
5. hyperpolymath

   added

   tech-debtKnown shortcut, drift, or hygiene owed - includes cleanupKnown shortcut, drift, or hygiene owed - includes cleanup

   on May 30, 2026
6. hyperpolymath commented on May 30, 2026

   

   hyperpolymath

   on May 30, 2026

   OwnerAuthor

   More actions

   Status (2026-05-31): still OPEN — no work landed this session

   Tracked under the new tech-debt label.

   The two postulates in src/abi/Layout.idr have since morphed into 5 believe_mes in src/abi/Proofs/DivMod.idr:

   • alignmentMatchesPlatformWord — DELETED (was unsound: AlignProof carried no evidence about n); replaced with the per-instance programStateAlignmentValid using believe_me.
   • alignedSizeCorrect — moved to Proofs/DivMod.idr:86-90; still believe_me (). Joined by divModIdentity, multModZero, addModDistrib — all believe_me.

   The bodies are computationally true ((size + align - r) mod align == 0) but per [[reference_idris2_0_8_0_reduction_map]] Idris2 0.8.0's divNat doesn't reduce through its non-covering case at type-level, so Refl won't close them. Discharge requires inductive proofs on Nat-mod algebra — multi-day work, gated on either an Idris2 reduction-strategy fix or hand-rolling div_mod_lemma infrastructure (same gap civic-connect's alignUpDivides defers).
7. hyperpolymath commented on Sep 19, 2026

   

   hyperpolymath

   on Sep 19, 2026

   OwnerAuthor

   More actions

   Re-measured today (2026-09-19) — the concern moved, it did not go away. Keeping it open with the current facts.

   The file moved: src/abi/Layout.idr no longer exists; the module is now src/abi/AbsoluteZero/ABI/Layout.idr (303 lines).

   The two postulates are gone — as postulates. Repo-wide there are now 0 postulate declarations. Consistent with the 2026-05-25 finding recorded here: postulate does not parse in Idris2 0.8.0 (removed; survives only as an IDE decoration tag).

   What replaced them: src/abi/AbsoluteZero/ABI/Proofs/DivMod.idr carries 7 believe_me () axioms, and its own header documents the pattern as "each believe_me-based axiom below is an individually-audit-trackable" and "so every axiom is grep-able as a believe_me occurrence". The obligations named in this issue survive there:

   alignedSizeCorrect _ _ = believe_me ()
   divModIdentity     _ _ = believe_me ()
   multModZero        _ _ = believe_me ()
   

   So the acceptance criteria should be restated, because the original ones cannot be met as written: the work is no longer "remove two postulates" (done — they cannot exist in current Idris2) but "discharge the seven believe_me axioms in Proofs/DivMod.idr", of which alignedSizeCorrect and the mod-arithmetic lemmas this issue is about are still believed rather than proved. Flagging for the owner rather than silently closing: the trust-escape this issue was filed to remove is still present, in a new form.
8. hyperpolymath

   added

   priority:p3Low - nice to haveLow - nice to have

   scope:repoConfined to this repositoryConfined to this repository

   status:blockedCannot proceed until a dependency clearsCannot proceed until a dependency clears

   feeds:valence-shellFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes thereFeeds valence-shell's proofs/engineering (D127): judge progress by what it contributes there

   on Sep 30, 2026