Pulseverifier

# 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

Pulse-Specific Errors

"Application of stateful computation cannot have ghost effect"

Cause: Trying to call a stateful stt function inside a ghost context Diagnosis:

• Variables bound with with x y z. _ are ghost
• If an if condition uses ghost values, both branches become ghost

Solutions:

1. Read from actual data structures instead of ghost sequences:

// 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;

2. Restructure to perform stateful ops before ghost conditionals:

// Do stateful work first
let result = stateful_operation();
// Then do ghost reasoning
if ghost_condition then ... else ...

"Expected a term with non-informative (erased) type"

Cause: Binding a concrete type from a ghost expression Solutions:

1. Use assertion instead of let binding:

// WRONG
let x : list entry = Seq.index ghost_seq idx;

// RIGHT
assert (pure (Cons? (Seq.index ghost_seq idx)));

2. Keep ghost values as ghost:

let x : erased (list entry) = Seq.index ghost_seq idx;

"Could not prove post-condition" (separation logic)

Cause: Resources don't match expected slprop

Diagnosis Steps:

1. Check fold/unfold balance
2. Verify rewrite statements are correct
3. Ensure all resources are accounted for

Solutions:

1. Add explicit fold/unfold:

unfold (my_predicate args);
// ... work with internal structure ...
fold (my_predicate args);

2. Use rewrite for type equality:

rewrite (pred x) as (pred y);  // when x == y is known

3. For OnRange predicates:

get_bucket_at ptrs contents lo hi idx;  // Extract element
// ... use element ...
put_bucket_at ptrs contents lo hi idx;  // Put back

"Ill-typed application" in fold/unfold

Cause: Predicate arguments don't match definition Solutions:

1. Check all arguments are provided
2. Verify implicit arguments are inferable
3. Add explicit type annotations

Proof Patterns

FiniteSet Reasoning

// 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));

Sequence Equality

// Use extensional equality
assert (pure (Seq.equal s1 s2));

// NOT propositional equality
// assert (pure (s1 == s2));  // Often fails

Ghost Lemma Calls

// Call F* lemmas in ghost context
my_lemma arg1 arg2;
assert (pure (lemma_conclusion));

Resource Management Verification

Checking for Memory Leaks

Look for:

1. drop_ calls - should only be on empty/null resources
2. All allocated resources must be freed or returned
3. Box.box allocations must have corresponding B.free

Acceptable Drops

// 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!

Verification Checklist

Before considering code complete:

• No admit() calls
• No assume_ calls
• No drop_ of non-empty resources
• Interface (.fsti) verified separately
• Implementation (.fst) verified
• rlimits ≤10 throughout
• All queries pass (no cancelled in --query_stats)