Steel: use @@@unused for arguments of locks and invariants

This depends on FStarLang/FStar#3002, and allows to use locks and invariants in non-strictly-positive positions of recursive definitions.
mtzguido · Aug 3, 2023 · a99dc6a · a99dc6a
1 parent d764d70
commit a99dc6a
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 6 deletions.
diff --git a/lib/steel/Steel.Memory.fst b/lib/steel/Steel.Memory.fst
@@ -1110,7 +1110,7 @@ let iname_for_p_stable (i:iname) (p:slprop)
   : Lemma (W.stable full_mem mem_evolves (iname_for_p_mem i p))
   = ()
 
-let ( >--> ) (i:iname) (p:slprop) : Type0 = W.witnessed full_mem mem_evolves (iname_for_p_mem i p)
+let ( >--> ) (i:iname) ([@@@unused] p:slprop) : Type0 = W.witnessed full_mem mem_evolves (iname_for_p_mem i p)
 
 let hmem_with_inv_equiv e (m:mem) (p:slprop)
   : Lemma (interp (p `star` linv e m) m <==>
@@ -1202,7 +1202,8 @@ let new_invariant_tot_action (e:inames) (p:slprop) (m0:hmem_with_inv_except e p{
     assert (frame_related_mems p emp e m0 m1);
     ( i, m1 )
 
-let inv (p:slprop u#1) = i:erased iname & (i >--> p)
+let inv ([@@@unused] p:slprop u#1) = i:erased iname & (i >--> p)
+
 let name_of_inv #p (i:inv p) = dfst i
 
 let new_invariant (e:inames) (p:slprop) (frame:slprop)

diff --git a/lib/steel/Steel.Memory.fsti b/lib/steel/Steel.Memory.fsti
@@ -136,7 +136,7 @@ val h_and (p1 p2:slprop u#a) : slprop u#a
 val h_or  (p1 p2:slprop u#a) : slprop u#a
 val star  (p1 p2:slprop u#a) : slprop u#a
 val wand  (p1 p2:slprop u#a) : slprop u#a
-val h_exists (#a:Type u#b) (f: (a -> slprop u#a)) : slprop u#a
+val h_exists (# [@@@strictly_positive] a:Type u#b) ([@@@strictly_positive] f: (a -> slprop u#a)) : slprop u#a
 val h_forall (#a:Type u#b) (f: (a -> slprop u#a)) : slprop u#a
 
 (***** Properties of separation logic equivalence *)
@@ -501,7 +501,7 @@ val recall (#a:Type u#1) (#pcm:pcm a) (#fact:property a)
 (**** Invariants *)
 
 (**[i : inv p] is an invariant whose content is [p] *)
-val inv (p:slprop u#1) : Type0
+val inv ([@@@unused] p:slprop u#1) : Type0
 
 val name_of_inv (#p:slprop) (i:inv p) : GTot iname
 

diff --git a/lib/steel/Steel.ST.SpinLock.fst b/lib/steel/Steel.ST.SpinLock.fst
@@ -49,7 +49,7 @@ let lockinv (p:vprop) (r:ref U32.t) : vprop =
   exists_ (lockinv_predicate p r)
 
 noeq
-type lock (p:vprop) = {
+type lock ([@@@unused] p:vprop) = {
   r:ref U32.t;
   i:inv (lockinv p r)
 }

diff --git a/lib/steel/Steel.ST.SpinLock.fsti b/lib/steel/Steel.ST.SpinLock.fsti
@@ -22,7 +22,7 @@ open Steel.ST.Util
 
 /// The type of a lock.  This is implemented as a pair of a boolean
 /// reference, and an invariant name
-val lock (p:vprop): Type u#0
+val lock ([@@@unused] p:vprop): Type u#0
 
 /// If we have vprop [p] in the context, we can create a new lock
 /// associated to [p]. [p] is then removed from the context, and only