From aac48b7e1f0c41339bb90d1e891412e0e8320681 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 24 May 2026 19:41:56 +0000 Subject: [PATCH] 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. --- .machine_readable/META.scm | 3 +- src/abi/Layout.idr | 67 +++++++++----------------- src/abi/Proofs/DivMod.idr | 98 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 123 insertions(+), 45 deletions(-) create mode 100644 src/abi/Proofs/DivMod.idr diff --git a/.machine_readable/META.scm b/.machine_readable/META.scm index bb017d6..5a1b1a6 100644 --- a/.machine_readable/META.scm +++ b/.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") diff --git a/src/abi/Layout.idr b/src/abi/Layout.idr index 504cb04..c9084f3 100644 --- a/src/abi/Layout.idr +++ b/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 diff --git a/src/abi/Proofs/DivMod.idr b/src/abi/Proofs/DivMod.idr new file mode 100644 index 0000000..957c769 --- /dev/null +++ b/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