{{ message }}
iseriser: make Phase 0 ABI proofs genuinely compile and verify#67
Merged
Conversation
The hand-written Idris2 ABI was never compiler-checked and did not
typecheck under Idris2 0.7.0. Make the foundation real and machine-verified.
Layout.idr
- Discharge the two open holes: ?fieldsAlignedProof and ?offsetInBoundsProof.
- Add a sound decDivides decision procedure (builds genuine m = k*n
witnesses) and decFieldsAligned; checkCABI now returns a real
CABICompliant proof or an error.
- offsetInBounds had an unsound signature (claimed every field fits any
layout); make it an honest decidable Maybe.
- Fix paddingFor (Nat has no Neg; use minus) and give the three concrete
struct layouts explicit alignment witnesses.
- Replace alignUpCorrect's non-compiling Refl proof with a sound
alignUpDivides decision; the general lemma is noted as residual work.
Types.idr
- FullyResolved and GenerationComplete carried no obligation; give them
real So-proofs (no {{/}} markers remain; all seven categories present).
- thisPlatform was a %runElab stub needing ElabReflection; make it total.
- DecEq Result used `No absurd` with no Uninhabited instance; discharge
the off-diagonal cases explicitly.
- createHandle left the auto So (ptr /= 0) unsolved; use choose.
Proofs.idr (new)
- Machine-checked theorems: the three concrete FFI struct layouts are
provably C-ABI aligned; Result→C-int pins; generation-completeness.
Structure / tooling
- Move ABI into src/interface/abi/Iseriser/ABI/ so it builds as an Idris2
package (matches the chapeliser layout); add iseriser-abi.ipkg.
- Add `just proofs` recipe; ignore Idris build artifacts.
- verification/proofs/ now documents and points at the verified proofs.
Verified: `idris2 --build iseriser-abi.ipkg` clean (0 warnings);
cargo test green (57 unit + 9 integration).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA
The governance/licence-consistency check requires an SPDX-License-Identifier header on the LICENSE file and a `license` field in the manifest. The LICENSE body is MPL-2.0 text, so stamp `SPDX-License-Identifier: MPL-2.0` (matching the actual body) and set `license = "MPL-2.0"` (replacing `license-file`). Verified with standards/scripts/check-licence-consistency.sh (passes). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This is the foundation pass of the family-wide proofs review: make iseriser's own (Phase 0) Idris2 ABI proofs actually compile and machine-verify, so it can serve as the verified reference template before the per-iser fan-out.
Key finding: the hand-written ABI was never compiler-checked — it did not typecheck under Idris2 0.7.0 (the pinned version). The two advertised
?holeswere only part of it; several constructs simply don't elaborate. This is almost certainly systemic across the -iser family (same template-derived patterns seen verbatim in e.g.affinescriptiser).What was broken (and is now fixed)
Layout.idr?fieldsAlignedProof/?offsetInBoundsProof.decDividesdecision procedure (builds genuinem = k*nwitnesses) +decFieldsAligned;checkCABInow returns a realCABICompliantproof or an error.offsetInBoundshad an unsound signature (asserted every field fits any layout — false); now an honest decidableMaybe.paddingForusedNatsubtraction viaNeg(doesn't exist) →minus.alignUpCorrect'sReflproof can't hold for symbolic inputs → replaced with a soundalignUpDividesdecision (general lemma noted as residual).Types.idrFullyResolved/GenerationCompleteproved nothing → realSo-obligations (no{{/}}markers remain; all seven artifact categories present).thisPlatformwas a%runElabstub needingElabReflection→ made total.DecEq ResultusedNo absurdwith noUninhabited (x=y)instance → off-diagonal cases discharged explicitly.createHandleleftauto So (ptr /= 0)unsolved → useschoose.Proofs.idr(new) — machine-checked theorems (compile-time, not runtime tests):Result→ C-int encoding pins (okIsZero,nullPointerIsFive);Structure & tooling
src/interface/abi/Iseriser/ABI/so it builds as an Idris2 package (matches thechapeliserlayout); addediseriser-abi.ipkg.just proofsrecipe; ignore Idris build artifacts;verification/proofs/now documents and points at the verified proofs.Verification
idris2 --build iseriser-abi.ipkg→ clean, 0 warnings (Idris2 0.7.0, bootstrapped in-CI-env from source).cargo test→ green (57 unit + 9 integration).Next (per the review plan)
Fan out reverse-alphabetically, layer-by-layer, applying the same transform + real obligations, flagging per-repo blockers (notably AffineScriptiser, whose target toolchain is mid-migration).
🤖 Generated with Claude Code
Generated by Claude Code