From a99dc6a614d3b7949cd8d38d787dfb6a592d84d4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Wed, 2 Aug 2023 15:40:36 -0700
Subject: [PATCH] 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.
---
 lib/steel/Steel.Memory.fst       | 5 +++--
 lib/steel/Steel.Memory.fsti      | 4 ++--
 lib/steel/Steel.ST.SpinLock.fst  | 2 +-
 lib/steel/Steel.ST.SpinLock.fsti | 2 +-
 4 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/lib/steel/Steel.Memory.fst b/lib/steel/Steel.Memory.fst
index b5218ec5b..15006aeaf 100644
--- 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
index e2d1f9a53..b9e8ed885 100644
--- 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
index d9608b716..d84592cd3 100644
--- 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
index ccd412727..33c8c9a8f 100644
--- 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