Use fstar.exe to verify Pulse code and interpret the errors reported
This skill is used when:
#lang-pulse directivePULSE_HOME is usually located adjacent to the FStar directory.
# Verify Pulse file (--include <PULSE_HOME>/out/lib/pulse is required)
fstar.exe --include <PULSE_HOME>/out/lib/pulse Module.fst
# With include paths for Pulse library
fstar.exe --include <PULSE_HOME>/out/lib/pulse --include out/lib/pulse --include lib/pulse/lib Module.fst
# Verify interface first, then implementation
fstar.exe --include <PULSE_HOME>/out/lib/pulse --include paths... Module.fsti
fstar.exe --include <PULSE_HOME>/out/lib/pulse --include paths... Module.fst
# In pulse repository root
make -j4
# Or verify specific file
cd /path/to/pulse
fstar.exe --include out/lib/pulse --include lib/pulse/lib lib/pulse/lib/Module.fst
Cause: Trying to call a stateful stt function inside a ghost context
Diagnosis:
with x y z. _ are ghostif condition uses ghost values, both branches become ghostSolutions:
// WRONG: bucket_ptrs is ghost from 'with'
let ptr = Seq.index bucket_ptrs idx;
// RIGHT: Read from actual vector
let ptr = V.op_Array_Access vec idx;
// Do stateful work first
let result = stateful_operation();
// Then do ghost reasoning
if ghost_condition then ... else ...
Cause: Binding a concrete type from a ghost expression Solutions:
// WRONG
let x : list entry = Seq.index ghost_seq idx;
// RIGHT
assert (pure (Cons? (Seq.index ghost_seq idx)));
let x : erased (list entry) = Seq.index ghost_seq idx;
Cause: Resources don't match expected slprop
Diagnosis Steps:
Solutions:
unfold (my_predicate args);
// ... work with internal structure ...
fold (my_predicate args);
rewrite (pred x) as (pred y); // when x == y is known
get_bucket_at ptrs contents lo hi idx; // Extract element
// ... use element ...
put_bucket_at ptrs contents lo hi idx; // Put back
Cause: Predicate arguments don't match definition Solutions:
// ALWAYS call this before FiniteSet assertions
FS.all_finite_set_facts_lemma();
// Now SMT can prove these
assert (pure (FS.mem x (FS.insert x s)));
assert (pure (FS.cardinality (FS.remove x s) == FS.cardinality s - 1));
// Use extensional equality
assert (pure (Seq.equal s1 s2));
// NOT propositional equality
// assert (pure (s1 == s2)); // Often fails
// Call F* lemmas in ghost context
my_lemma arg1 arg2;
assert (pure (lemma_conclusion));
Look for:
drop_ calls - should only be on empty/null resources// OK: Empty linked list (null pointer)
drop_ (LL.is_list null_ptr []);
// NOT OK: Non-empty resources
// drop_ (LL.is_list ptr (hd::tl)); // Memory leak!
Before considering code complete:
admit() callsassume_ callsdrop_ of non-empty resources