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

.machine_readable/META.scm

@@ -11,7 +11,8 @@
      ("ADR-005" "proposed" "Fix QuantumCNO.v Cexp: real exp -> complex phase factor")
      ("ADR-006" "accepted" "state_eq excludes state_pc — PC is control-flow bookkeeping, not observable side effect (2026-05-18 rescue)")
      ("ADR-007" "accepted" "Discharge eval_deterministic Axiom → Theorem via step_deterministic_strong helper (2026-05-20, PR #24); first post-T0 axiom audit win")
-     ("ADR-008" "accepted" "Delete unsound eval_respects_state_eq_{left,right} axioms; weaken logically_reversible to =st= (observational reversibility); re-prove cno_eval_on_equal_states + cno_logically_reversible via cno_terminates + cno_preserves_state (2026-05-20)")))
+     ("ADR-008" "accepted" "Delete unsound eval_respects_state_eq_{left,right} axioms; weaken logically_reversible to =st= (observational reversibility); re-prove cno_eval_on_equal_states + cno_logically_reversible via cno_terminates + cno_preserves_state (2026-05-20)")
+     ("ADR-009" "accepted" "Delete unsound alignmentMatchesPlatformWord Idris2 postulate (HasAlignment carries no evidence; would derive So (1 mod 8 == 0) from CNOResultLayout.alignment); replace single consumer with per-Platform decidable proof. Consolidate remaining alignedSizeCorrect postulate into shared AbsoluteZero.ABI.Proofs.DivMod module as the estate-wide div/mod lemma surface (absolute-zero#27, civic-connect alignUpDivides/mkFieldsAligned/offsetInBoundsPrf migrate here)")))
 
   (development-practices
     (code-style "Coq proof engineering")

src/abi/Layout.idr

@@ -14,6 +14,7 @@ import Data.Bits
 import Data.So
 import Data.Vect
 import AbsoluteZero.ABI.Types
+import AbsoluteZero.ABI.Proofs.DivMod
 
 %default total
 
@@ -238,33 +239,26 @@ instructionCrossPlatform = InvariantProof
 -- Alignment Verification
 --------------------------------------------------------------------------------
 
--- Axiom: a well-formed HasAlignment t n carries the semantic invariant
--- that n is divisible by the platform word size (ptrSize p / 8).
--- This cannot be derived internally because AlignProof is an information-free
--- constructor (no constraint on n); strengthening HasAlignment to refine n would
--- ripple through every call site. The obligation instead sits on the producer:
--- AlignProof must only be constructed for types whose alignment genuinely
--- matches the platform's word size.
--- Follows the same deferral pattern as civic-connect/src/Abi/Layout.idr
--- (alignUpDivides, mkFieldsAligned, offsetInBoundsPrf).
-export
-postulate alignmentMatchesPlatformWord :
-  (p : Platform) -> {0 t : Type} -> {n : Nat} ->
-  HasAlignment t n -> So (n `mod` (ptrSize p `div` 8) == 0)
-
-||| Verify that a type's alignment is correct for the platform.
-||| All five platform cases derive from `alignmentMatchesPlatformWord`.
-public export
-verifyAlignment : (p : Platform) -> (t : Type) ->
-                  HasAlignment t n -> So (n `mod` (ptrSize p `div` 8) == 0)
-verifyAlignment p _ ha = alignmentMatchesPlatformWord p ha
-
-||| ProgramState alignment is valid on all platforms
+-- Historical note (absolute-zero#27): a universally-quantified postulate
+-- `alignmentMatchesPlatformWord : HasAlignment t n -> So (n `mod` word == 0)`
+-- previously lived here. It was unsound: `AlignProof` carries no evidence
+-- about `n`, so the postulate would derive `So (1 `mod` 8 == 0)` from
+-- `CNOResultLayout.alignment : HasAlignment CNOVerificationResult 1`. It was
+-- removed in favour of per-type decidable proofs at each call site (the
+-- only previous caller was `programStateAlignmentValid`, dispatched below
+-- by Platform case-split since `8 `mod` (ptrSize p `div` 8)` reduces to 0
+-- on every supported platform).
+
+||| ProgramState alignment is valid on all platforms.
+||| Proved directly by reduction; no axiom required.
 public export
 programStateAlignmentValid : (p : Platform) ->
   So (8 `mod` (ptrSize p `div` 8) == 0)
-programStateAlignmentValid p =
-  verifyAlignment p ProgramState ProgramStateLayout.alignment
+programStateAlignmentValid Linux   = Oh
+programStateAlignmentValid Windows = Oh
+programStateAlignmentValid MacOS   = Oh
+programStateAlignmentValid BSD     = Oh
+programStateAlignmentValid WASM    = Oh
 
 --------------------------------------------------------------------------------
 -- Size Calculation Utilities
@@ -275,27 +269,12 @@ public export
 arraySize : HasSize t elemSize -> (n : Nat) -> Nat
 arraySize _ n = elemSize * n
 
-||| Calculate aligned size (round up to alignment boundary)
+||| Calculate aligned size (round up to alignment boundary).
+||| Definition and correctness lemma live in `AbsoluteZero.ABI.Proofs.DivMod`
+||| (re-exported here for API compatibility). See absolute-zero#27.
 public export
-alignedSize : (size : Nat) -> (alignment : Nat) -> Nat
-alignedSize size align =
-  let remainder = size `mod` align
-  in if remainder == 0
-     then size
-     else size + (align - remainder)
-
--- Prove that aligned size is a multiple of alignment.
--- Case analysis on `size mod align`:
---   * remainder = 0 → alignedSize = size, and `size mod align = 0` by hypothesis.
---   * remainder /= 0 → alignedSize = size + (align - remainder); 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. Deferred here too — kept as a postulate
---     until those lemmas are in scope.
-export
-postulate alignedSizeCorrect : (size : Nat) -> (align : Nat) -> {auto 0 nonZero : So (align /= 0)} ->
-  So (alignedSize size align `mod` align == 0)
+alignedSize : (size : Nat) -> (align : Nat) -> Nat
+alignedSize = DivMod.alignedSize
 
 --------------------------------------------------------------------------------
 -- Compile-Time Verification

src/abi/Proofs/DivMod.idr

@@ -0,0 +1,98 @@
+||| Div/mod lemma library for ABI alignment proofs.
+|||
+||| Consolidates the trusted base of number-theoretic lemmas used by ABI
+||| layout modules across the hyperpolymath estate (absolute-zero,
+||| civic-connect, and any future Idris2 ABI consumers).
+|||
+||| Design goals:
+|||   * Single shared module — each estate repo imports the same lemmas
+|||     rather than re-postulating per file.
+|||   * Each lemma is an individually-named declaration so it can be
+|||     discharged incrementally (one Qed/proof per audit pass) without
+|||     touching consumers.
+|||   * Definitions of the functions the lemmas talk about live here too,
+|||     so the lemma statements don't drift from their referent.
+|||
+||| Discharge tracker: absolute-zero#27.
+|||
+||| @see https://github.com/hyperpolymath/absolute-zero/issues/27
+
+-- SPDX-License-Identifier: PMPL-1.0-or-later
+
+module AbsoluteZero.ABI.Proofs.DivMod
+
+import Data.So
+import Data.Nat
+
+%default total
+
+--------------------------------------------------------------------------------
+-- Aligned size
+--------------------------------------------------------------------------------
+
+||| Round `size` up to the next multiple of `align`.
+||| If `size` is already aligned, returns `size` unchanged.
+public export
+alignedSize : (size : Nat) -> (align : Nat) -> Nat
+alignedSize size align =
+  let remainder = size `mod` align
+  in if remainder == 0
+     then size
+     else size + (align - remainder)
+
+--------------------------------------------------------------------------------
+-- Trusted lemma surface
+--
+-- Each `postulate` below is an individually-audit-trackable item. Discharge
+-- one at a time; the lemma name stays stable so consumers don't break.
+--
+-- Estate cross-reference (as of 2026-05-20):
+--   * civic-connect/src/Abi/Layout.idr defers the same family under
+--     `alignUpDivides`, `mkFieldsAligned`, `offsetInBoundsPrf`. Those
+--     should migrate to import these names.
+--------------------------------------------------------------------------------
+
+||| `alignedSize size align` is always a multiple of `align`.
+|||
+||| Proof outline (deferred — see audit tracker):
+|||   Let r = size `mod` align.
+|||   Case r == 0: alignedSize = size, divisible by hypothesis.
+|||   Case r /= 0: alignedSize = size + (align - r)
+|||                            = ((size `div` align) * align + r) + (align - r)
+|||                              [by divModIdentity]
+|||                            = ((size `div` align) + 1) * align
+|||                              [by Nat ring rewriting]
+|||                            and (k * align) `mod` align = 0
+|||                              [by multModZero].
+|||
+||| Reduces to: `divModIdentity` + `multModZero` + `addModDistrib`.
+export
+postulate alignedSizeCorrect :
+  (size : Nat) -> (align : Nat) ->
+  {auto 0 nonZero : So (align /= 0)} ->
+  So (alignedSize size align `mod` align == 0)
+
+||| Euclidean division identity: every Nat decomposes as q*d + r where r < d.
+||| The single most-used lemma in the alignment proofs — proving this
+||| (likely by induction on `size`, or via Idris2 stdlib `Data.Nat.Division`)
+||| would shrink the trusted base substantially.
+export
+postulate divModIdentity :
+  (n : Nat) -> (d : Nat) ->
+  {auto 0 nonZero : So (d /= 0)} ->
+  n = (n `div` d) * d + (n `mod` d)
+
+||| Any multiple of `d` is congruent to zero mod `d`.
+export
+postulate multModZero :
+  (k : Nat) -> (d : Nat) ->
+  {auto 0 nonZero : So (d /= 0)} ->
+  So ((k * d) `mod` d == 0)
+
+||| Mod distributes over addition (in the sense that `(a + b) mod d` is
+||| determined by `a mod d` and `b mod d`).
+export
+postulate addModDistrib :
+  (a : Nat) -> (b : Nat) -> (d : Nat) ->
+  {auto 0 nonZero : So (d /= 0)} ->
+  (a + b) `mod` d = ((a `mod` d) + (b `mod` d)) `mod` d