Skip to content

Commit 48db993

Browse files
committed
fix(abi): resolve size proof accessibility and pointer width typing
1 parent be301df commit 48db993

1 file changed

Lines changed: 7 additions & 3 deletions

File tree

src/abi/Types.idr

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -261,7 +261,7 @@ programStateSizeBytes = 40 -- Aligned to 8 bytes
261261

262262
||| Prove ProgramState has correct size
263263
public export
264-
programStateSize : HasSize ProgramState programStateSizeBytes
264+
programStateSize : HasSize ProgramState 40
265265
programStateSize = SizeProof
266266

267267
||| Prove ProgramState has 8-byte alignment
@@ -276,7 +276,7 @@ instructionSizeBytes = 16
276276

277277
||| Prove Instruction has correct size
278278
public export
279-
instructionSize : HasSize Instruction instructionSizeBytes
279+
instructionSize : HasSize Instruction 16
280280
instructionSize = SizeProof
281281

282282
||| Prove Instruction has 4-byte alignment
@@ -318,7 +318,11 @@ ptrSize WASM = 32
318318
||| Pointer type for platform
319319
public export
320320
CPtr : Platform -> Type -> Type
321-
CPtr p _ = Bits (ptrSize p)
321+
CPtr Linux _ = Bits64
322+
CPtr Windows _ = Bits64
323+
CPtr MacOS _ = Bits64
324+
CPtr BSD _ = Bits64
325+
CPtr WASM _ = Bits32
322326

323327
--------------------------------------------------------------------------------
324328
-- Verification Types

0 commit comments

Comments
 (0)