Skip to content

Commit aac48b7

Browse files
claudeclaude
committed
proof(idris2/abi): delete unsound alignmentMatchesPlatformWord, isolate alignedSizeCorrect into shared DivMod module (#27)
The `alignmentMatchesPlatformWord` postulate in src/abi/Layout.idr was not merely unproven but unsound. `HasAlignment t n` has a single information-free constructor `AlignProof`, so the universal claim `HasAlignment t n -> So (n `mod` (word/8) == 0)` could derive `So (1 `mod` 8 == 0)` from `CNOResultLayout.alignment : HasAlignment CNOVerificationResult 1`. The unsoundness was hidden by the postulate's single consumer only ever instantiating n at 8. Replace it with a per-Platform decidable proof of the only specific claim that was actually used (`programStateAlignmentValid`). The `verifyAlignment` helper, whose only purpose was to call the postulate, is removed (no other callers). The remaining `alignedSizeCorrect` postulate is moved to a new `AbsoluteZero.ABI.Proofs.DivMod` module that consolidates the estate-wide trusted div/mod base. Each lemma is named separately so discharge can be incremental, and civic-connect's `alignUpDivides` / `mkFieldsAligned` / `offsetInBoundsPrf` deferrals are intended to migrate onto the same surface. Tracked as ADR-009.
1 parent 4c171c8 commit aac48b7

3 files changed

Lines changed: 123 additions & 45 deletions

File tree

‎.machine_readable/META.scm‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,8 @@
1111
("ADR-005" "proposed" "Fix QuantumCNO.v Cexp: real exp -> complex phase factor")
1212
("ADR-006" "accepted" "state_eq excludes state_pc — PC is control-flow bookkeeping, not observable side effect (2026-05-18 rescue)")
1313
("ADR-007" "accepted" "Discharge eval_deterministic Axiom → Theorem via step_deterministic_strong helper (2026-05-20, PR #24); first post-T0 axiom audit win")
14-
("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)")))
14+
("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)")
15+
("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)")))
1516

1617
(development-practices
1718
(code-style "Coq proof engineering")

‎src/abi/Layout.idr‎

Lines changed: 23 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ import Data.Bits
1414
import Data.So
1515
import Data.Vect
1616
import AbsoluteZero.ABI.Types
17+
import AbsoluteZero.ABI.Proofs.DivMod
1718

1819
%default total
1920

@@ -238,33 +239,26 @@ instructionCrossPlatform = InvariantProof
238239
-- Alignment Verification
239240
--------------------------------------------------------------------------------
240241

241-
-- Axiom: a well-formed HasAlignment t n carries the semantic invariant
242-
-- that n is divisible by the platform word size (ptrSize p / 8).
243-
-- This cannot be derived internally because AlignProof is an information-free
244-
-- constructor (no constraint on n); strengthening HasAlignment to refine n would
245-
-- ripple through every call site. The obligation instead sits on the producer:
246-
-- AlignProof must only be constructed for types whose alignment genuinely
247-
-- matches the platform's word size.
248-
-- Follows the same deferral pattern as civic-connect/src/Abi/Layout.idr
249-
-- (alignUpDivides, mkFieldsAligned, offsetInBoundsPrf).
250-
export
251-
postulate alignmentMatchesPlatformWord :
252-
(p : Platform) -> {0 t : Type} -> {n : Nat} ->
253-
HasAlignment t n -> So (n `mod` (ptrSize p `div` 8) == 0)
254-
255-
||| Verify that a type's alignment is correct for the platform.
256-
||| All five platform cases derive from `alignmentMatchesPlatformWord`.
257-
public export
258-
verifyAlignment : (p : Platform) -> (t : Type) ->
259-
HasAlignment t n -> So (n `mod` (ptrSize p `div` 8) == 0)
260-
verifyAlignment p _ ha = alignmentMatchesPlatformWord p ha
261-
262-
||| ProgramState alignment is valid on all platforms
242+
-- Historical note (absolute-zero#27): a universally-quantified postulate
243+
-- `alignmentMatchesPlatformWord : HasAlignment t n -> So (n `mod` word == 0)`
244+
-- previously lived here. It was unsound: `AlignProof` carries no evidence
245+
-- about `n`, so the postulate would derive `So (1 `mod` 8 == 0)` from
246+
-- `CNOResultLayout.alignment : HasAlignment CNOVerificationResult 1`. It was
247+
-- removed in favour of per-type decidable proofs at each call site (the
248+
-- only previous caller was `programStateAlignmentValid`, dispatched below
249+
-- by Platform case-split since `8 `mod` (ptrSize p `div` 8)` reduces to 0
250+
-- on every supported platform).
251+
252+
||| ProgramState alignment is valid on all platforms.
253+
||| Proved directly by reduction; no axiom required.
263254
public export
264255
programStateAlignmentValid : (p : Platform) ->
265256
So (8 `mod` (ptrSize p `div` 8) == 0)
266-
programStateAlignmentValid p =
267-
verifyAlignment p ProgramState ProgramStateLayout.alignment
257+
programStateAlignmentValid Linux = Oh
258+
programStateAlignmentValid Windows = Oh
259+
programStateAlignmentValid MacOS = Oh
260+
programStateAlignmentValid BSD = Oh
261+
programStateAlignmentValid WASM = Oh
268262

269263
--------------------------------------------------------------------------------
270264
-- Size Calculation Utilities
@@ -275,27 +269,12 @@ public export
275269
arraySize : HasSize t elemSize -> (n : Nat) -> Nat
276270
arraySize _ n = elemSize * n
277271

278-
||| Calculate aligned size (round up to alignment boundary)
272+
||| Calculate aligned size (round up to alignment boundary).
273+
||| Definition and correctness lemma live in `AbsoluteZero.ABI.Proofs.DivMod`
274+
||| (re-exported here for API compatibility). See absolute-zero#27.
279275
public export
280-
alignedSize : (size : Nat) -> (alignment : Nat) -> Nat
281-
alignedSize size align =
282-
let remainder = size `mod` align
283-
in if remainder == 0
284-
then size
285-
else size + (align - remainder)
286-
287-
-- Prove that aligned size is a multiple of alignment.
288-
-- Case analysis on `size mod align`:
289-
-- * remainder = 0 → alignedSize = size, and `size mod align = 0` by hypothesis.
290-
-- * remainder /= 0 → alignedSize = size + (align - remainder); showing
291-
-- `(size + align - remainder) mod align = 0` needs the div/mod identity
292-
-- `size = (size `div` align) * align + remainder` plus congruence lemmas,
293-
-- i.e. the same `div_mod_lemma` infrastructure civic-connect's
294-
-- `alignUpDivides` defers. Deferred here too — kept as a postulate
295-
-- until those lemmas are in scope.
296-
export
297-
postulate alignedSizeCorrect : (size : Nat) -> (align : Nat) -> {auto 0 nonZero : So (align /= 0)} ->
298-
So (alignedSize size align `mod` align == 0)
276+
alignedSize : (size : Nat) -> (align : Nat) -> Nat
277+
alignedSize = DivMod.alignedSize
299278

300279
--------------------------------------------------------------------------------
301280
-- Compile-Time Verification

‎src/abi/Proofs/DivMod.idr‎

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
||| Div/mod lemma library for ABI alignment proofs.
2+
|||
3+
||| Consolidates the trusted base of number-theoretic lemmas used by ABI
4+
||| layout modules across the hyperpolymath estate (absolute-zero,
5+
||| civic-connect, and any future Idris2 ABI consumers).
6+
|||
7+
||| Design goals:
8+
||| * Single shared module — each estate repo imports the same lemmas
9+
||| rather than re-postulating per file.
10+
||| * Each lemma is an individually-named declaration so it can be
11+
||| discharged incrementally (one Qed/proof per audit pass) without
12+
||| touching consumers.
13+
||| * Definitions of the functions the lemmas talk about live here too,
14+
||| so the lemma statements don't drift from their referent.
15+
|||
16+
||| Discharge tracker: absolute-zero#27.
17+
|||
18+
||| @see https://github.com/hyperpolymath/absolute-zero/issues/27
19+
20+
-- SPDX-License-Identifier: PMPL-1.0-or-later
21+
22+
module AbsoluteZero.ABI.Proofs.DivMod
23+
24+
import Data.So
25+
import Data.Nat
26+
27+
%default total
28+
29+
--------------------------------------------------------------------------------
30+
-- Aligned size
31+
--------------------------------------------------------------------------------
32+
33+
||| Round `size` up to the next multiple of `align`.
34+
||| If `size` is already aligned, returns `size` unchanged.
35+
public export
36+
alignedSize : (size : Nat) -> (align : Nat) -> Nat
37+
alignedSize size align =
38+
let remainder = size `mod` align
39+
in if remainder == 0
40+
then size
41+
else size + (align - remainder)
42+
43+
--------------------------------------------------------------------------------
44+
-- Trusted lemma surface
45+
--
46+
-- Each `postulate` below is an individually-audit-trackable item. Discharge
47+
-- one at a time; the lemma name stays stable so consumers don't break.
48+
--
49+
-- Estate cross-reference (as of 2026-05-20):
50+
-- * civic-connect/src/Abi/Layout.idr defers the same family under
51+
-- `alignUpDivides`, `mkFieldsAligned`, `offsetInBoundsPrf`. Those
52+
-- should migrate to import these names.
53+
--------------------------------------------------------------------------------
54+
55+
||| `alignedSize size align` is always a multiple of `align`.
56+
|||
57+
||| Proof outline (deferred — see audit tracker):
58+
||| Let r = size `mod` align.
59+
||| Case r == 0: alignedSize = size, divisible by hypothesis.
60+
||| Case r /= 0: alignedSize = size + (align - r)
61+
||| = ((size `div` align) * align + r) + (align - r)
62+
||| [by divModIdentity]
63+
||| = ((size `div` align) + 1) * align
64+
||| [by Nat ring rewriting]
65+
||| and (k * align) `mod` align = 0
66+
||| [by multModZero].
67+
|||
68+
||| Reduces to: `divModIdentity` + `multModZero` + `addModDistrib`.
69+
export
70+
postulate alignedSizeCorrect :
71+
(size : Nat) -> (align : Nat) ->
72+
{auto 0 nonZero : So (align /= 0)} ->
73+
So (alignedSize size align `mod` align == 0)
74+
75+
||| Euclidean division identity: every Nat decomposes as q*d + r where r < d.
76+
||| The single most-used lemma in the alignment proofs — proving this
77+
||| (likely by induction on `size`, or via Idris2 stdlib `Data.Nat.Division`)
78+
||| would shrink the trusted base substantially.
79+
export
80+
postulate divModIdentity :
81+
(n : Nat) -> (d : Nat) ->
82+
{auto 0 nonZero : So (d /= 0)} ->
83+
n = (n `div` d) * d + (n `mod` d)
84+
85+
||| Any multiple of `d` is congruent to zero mod `d`.
86+
export
87+
postulate multModZero :
88+
(k : Nat) -> (d : Nat) ->
89+
{auto 0 nonZero : So (d /= 0)} ->
90+
So ((k * d) `mod` d == 0)
91+
92+
||| Mod distributes over addition (in the sense that `(a + b) mod d` is
93+
||| determined by `a mod d` and `b mod d`).
94+
export
95+
postulate addModDistrib :
96+
(a : Nat) -> (b : Nat) -> (d : Nat) ->
97+
{auto 0 nonZero : So (d /= 0)} ->
98+
(a + b) `mod` d = ((a `mod` d) + (b `mod` d)) `mod` d

0 commit comments

Comments
 (0)