Discovered while closing proof-debt in src/abi/Layout.idr (commit 02c2c85). Three pre-existing type errors in src/abi/Types.idr prevent the ABI modules from type-checking cleanly.
Failures
-
programStateSizeBytes not accessible — Types.idr:265
programStateSize : HasSize ProgramState programStateSizeBytes
programStateSize = SizeProof
Error: programStateSizeBytes is not accessible in this context.
Likely needs public export on programStateSizeBytes (currently public export on the binding declaration but accessibility flagged at the SizeProof site — possibly namespace or reducibility issue).
-
instructionSizeBytes not accessible — Types.idr:280 — same shape as above.
-
Bits (ptrSize p) kind mismatch — Types.idr:321
CPtr : Platform -> Type -> Type
CPtr p _ = Bits (ptrSize p)
Error: Mismatch between: Nat and Type.
Bits in Data.Bits is a type-class parameterised by a Type, not a constructor taking a Nat. Should probably use Bits32/Bits64 selected by the platform, or a different dependent bit-vector type.
Reproduction
idris2 --check --source-dir src src/abi/Layout.idr
or in isolation:
mkdir -p /tmp/az/AbsoluteZero/ABI
cp src/abi/{Types,Layout}.idr /tmp/az/AbsoluteZero/ABI/
cd /tmp/az && idris2 --check --source-dir . AbsoluteZero/ABI/Layout.idr
Notes
- The module-path mismatch (files in
src/abi/ but declared AbsoluteZero.ABI.*) is a separate build-config issue — ipkg missing from repo root. That blocks a canonical idris2 --build invocation entirely. Might be worth adding an .ipkg alongside this fix.
- No
.ipkg file exists anywhere in the repo — confirmed via find.
- Not related to proof debt; this is a preservation-of-types bug, separate from formal-verification work.
Discovered while closing proof-debt in
src/abi/Layout.idr(commit 02c2c85). Three pre-existing type errors insrc/abi/Types.idrprevent the ABI modules from type-checking cleanly.Failures
programStateSizeBytesnot accessible —Types.idr:265Error:
programStateSizeBytesis not accessible in this context.Likely needs
public exportonprogramStateSizeBytes(currentlypublic exporton the binding declaration but accessibility flagged at theSizeProofsite — possibly namespace or reducibility issue).instructionSizeBytesnot accessible —Types.idr:280— same shape as above.Bits (ptrSize p)kind mismatch —Types.idr:321Error: Mismatch between: Nat and Type.
BitsinData.Bitsis a type-class parameterised by aType, not a constructor taking aNat. Should probably useBits32/Bits64selected by the platform, or a different dependent bit-vector type.Reproduction
or in isolation:
Notes
src/abi/but declaredAbsoluteZero.ABI.*) is a separate build-config issue —ipkgmissing from repo root. That blocks a canonicalidris2 --buildinvocation entirely. Might be worth adding an.ipkgalongside this fix..ipkgfile exists anywhere in the repo — confirmed viafind.