search

FStarLang / pulse

The Pulse separation logic DSL for F*
Apache License 2.0
6 stars 7 forks source link

Storable invariants #156

Closed nikswamy closed 4 months ago

nikswamy commented 4 months ago

This PR adds support for a notion of storable invariants.

We now have

val storable_iname (i:iname) : GTot bool
val storable_inv (i:iname { storable_iname i }) (p:slprop3) : Lemma (is_slprop3 (inv i p))
val new_storable_invariant (p:slprop2) 
: stt_ghost (i:iname { storable_iname i }) emp_inames p (fun i -> inv i p)