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

[hyperpolymath]

Context

A 2026-05-20 cross-estate trust-escape sweep surfaced 2 Idris2 postulates in `src/abi/Layout.idr` that aren't tracked under the standards#133 POST-T0 axiom audit (that audit covered `proofs/lean4/` + `proofs/coq/` model-layer axioms — 117 declarations triaged to 73 Axioms + 42 Parameters, all owner-classified as legitimate model-layer assumptions about abstract Parameters).

The two Layout.idr postulates are a different kind: they're concrete number-theoretic lemmas about `mod` arithmetic, deferred awaiting a div/mod lemma library.

The two postulates

1. `alignmentMatchesPlatformWord` (line 251)

```idris
export
postulate alignmentMatchesPlatformWord :
(p : Platform) -> {0 t : Type} -> {n : Nat} ->
HasAlignment t n -> So (n `mod` (ptrSize p `div` 8) == 0)
```

Comment cites "the same deferral pattern as civic-connect/src/Abi/Layout.idr (alignUpDivides, mkFieldsAligned, offsetInBoundsPrf)" — so this is a known cross-repo pattern.

The obligation moves to the producer: `AlignProof` must only be constructed for types whose alignment genuinely matches platform word size. But the postulate itself sits in the trusted base.

2. `alignedSizeCorrect` (line 297)

```idris
export
postulate alignedSizeCorrect : (size : Nat) -> (align : Nat) -> {auto 0 nonZero : So (align /= 0)} ->
So (alignedSize size align `mod` align == 0)
```

Comment: "showing `(size + align - remainder) mod align = 0` needs the div/mod identity `size = (size `div` align) * align + remainder` plus congruence lemmas, i.e. the same `div_mod_lemma` infrastructure civic-connect's `alignUpDivides` defers."

Why this is worth filing

• These are provable (standard Nat-mod algebra), unlike the model-layer Parameters tracked under standards#133 (which are abstract physics/quantum/POSIX assumptions).
• They are concentrated in one ABI module + replicated across the estate per the comment trail (civic-connect, presumably others).
• A div/mod lemma library — once written — would discharge both at once, plus civic-connect's three deferrals, plus any future ABI alignment work.

Suggested labels

`audit` / `technical-debt` / `idris2` / `abi` — leave priority/timing to owner.

Audit scope context

Trust-escape sweep audit: 2026-05-20 evening, by Claude session bee4abf8-11ea-4236-bada-c4173ba54b3b. Other absolute-zero trust-escapes (52 Lean axioms + 114 Coq axioms/parameters) are all owner-authorised under standards#133.

[hyperpolymath]

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

[hyperpolymath]

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