Partial types
The new partial
keyword allows to define a non-ghostifiable version of malloc
that never returns NULL
. I would like to specify types with pointer fields and invariants specifying that the pointers are not null. I cannot do so because I cannot prove the existence of non-null pointers, as partial terms cannot be witnesses.
I include an example below. It does not typecheck because the witness for t 'a
is rejected, which is the intended behavior.
Similarly to partial code, would it be possible to allow the user to define a "partial type" which does not need a witness but cannot have ghost elements?
use mach.c.C, mach.int.UInt32
val partial abort () : unit ensures { false }
let partial malloc_checked (sz:uint32) : ptr 'a
ensures { is_not_null result }
ensures { plength result = sz }
= let p = malloc sz in
if not (is_not_null) p then abort ();
p
type t 'a = { data : ptr 'a; len : uint32 }
invariant { is_not_null data /\ plength data = len }
by { data = malloc_checked 1; len = 1 }
let partial create (len:uint32) : t 'a =
{ data = malloc_checked len; len = len }