some utilities to relate invariant names and invariants

lib/pulse/core/PulseCore.Action.fst

@@ -236,6 +236,15 @@ let with_invariant
     let m = with_invariant i f in
     mem_action_as_action _ _ _ _ m
 
+let distinct_invariants_have_distinct_names
+    #p #q i j pf
+= fun #ictx -> mem_action_as_action _ _ _ _ (distinct_invariants_have_distinct_names ictx p q i j)
+
+let invariant_name_identifies_invariant
+      (p q:slprop)
+      (i:inv p)
+      (j:inv q { name_of_inv i == name_of_inv j } )
+= fun #ictx -> mem_action_as_action _ _ _ _ (invariant_name_identifies_invariant ictx p q i j)
 
 ///////////////////////////////////////////////////////////////////
 // Core operations on references

lib/pulse/core/PulseCore.Action.fsti

@@ -115,6 +115,23 @@ val with_invariant
     (f:unit -> act a f_opens (p ** fp) (fun x -> p ** fp' x))
 : act a (add_inv f_opens i) fp fp'
 
+val distinct_invariants_have_distinct_names
+    (#p:slprop)
+    (#q:slprop)
+    (i:inv p)
+    (j:inv q)
+    (_:squash (p =!= q))
+: act (squash (name_of_inv i =!= name_of_inv j))
+    emp_inames 
+    emp
+    (fun _ -> emp)
+
+val invariant_name_identifies_invariant
+      (p q:slprop)
+      (i:inv p)
+      (j:inv q { name_of_inv i == name_of_inv j } )
+: act (squash (p == q /\ i == j)) emp_inames emp (fun _ -> emp)
+
 ////////////////////////////////////////////////////////////////////////
 // References
 ////////////////////////////////////////////////////////////////////////

lib/pulse/core/PulseCore.Atomic.fst

@@ -237,6 +237,9 @@ let with_invariant
 : stt_atomic a #obs (add_inv f_opens i) fp fp'
 = A.with_invariant i f
 
+let distinct_invariants_have_distinct_names = A.distinct_invariants_have_distinct_names
+let invariant_name_identifies_invariant = A.invariant_name_identifies_invariant
+
 let pts_to_not_null #a #p r v = Ghost.hide (A.pts_to_not_null #a #p r v)
 let alloc = A.alloc
 let read = A.read

lib/pulse/core/PulseCore.Atomic.fsti

@@ -223,6 +223,28 @@ val with_invariant
                             (fun x -> p ** fp' x))
 : stt_atomic a #(join_obs obs Unobservable) (add_inv f_opens i) fp fp'
 
+val distinct_invariants_have_distinct_names
+    (#p:slprop)
+    (#q:slprop)
+    (i:inv p)
+    (j:inv q)
+    (_:squash (p =!= q))
+: stt_atomic (squash (name_of_inv i =!= name_of_inv j))
+    #Unobservable
+    emp_inames 
+    emp
+    (fun _ -> emp)
+
+val invariant_name_identifies_invariant
+      (p q:slprop)
+      (i:inv p)
+      (j:inv q { name_of_inv i == name_of_inv j } )
+: stt_atomic (squash (p == q /\ i == j))
+    #Unobservable
+    emp_inames
+    emp
+    (fun _ -> emp)
+
 ////////////////////////////////////////////////////////////////////////
 // References
 ////////////////////////////////////////////////////////////////////////

lib/pulse/core/PulseCore.Memory.fst

@@ -1428,6 +1428,34 @@ let rec recall_all (ctx:list pre_inv)
       MSTTotal.recall _ mem_evolves (name_is_ok q) i;
       recall_all tl
 
+let distinct_invariants_have_distinct_names
+      (e:inames)
+      (p:slprop)
+      (q:slprop { p =!= q })
+      (i:inv p)
+      (j:inv q)
+      (frame:slprop u#1)
+: MstTot (squash (name_of_inv i =!= name_of_inv j)) e emp (fun _ -> emp) frame
+= let (| ni, wi, toki |) = i in
+  let (| nj, wj, tokj |) = j in
+  MSTTotal.recall _ _ _ toki;
+  MSTTotal.recall _ _ _ tokj
+
+let invariant_name_identifies_invariant
+      (e:inames)
+      (p:slprop)
+      (q:slprop)
+      (i:inv p)
+      (j:inv q { name_of_inv i == name_of_inv j })
+      (frame:slprop u#1)
+: MstTot (squash (p == q /\ i == j)) e emp (fun _ -> emp) frame
+= let (| ni, wi, toki |) = i in
+  let (| nj, wj, tokj |) = j in
+  MSTTotal.recall _ _ _ toki;
+  MSTTotal.recall _ _ _ tokj;
+  W.witnessed_proof_irrelevant _ _ _ wi wj;
+  W.witnessed_proof_irrelevant _ _ _ toki tokj
+
 let fresh_invariant (e:inames) (p:slprop) (ctx:list pre_inv) (frame:slprop)
   : MstTot (i:inv p { not (mem_inv e i) /\ fresh_wrt ctx (name_of_inv i)}) e p (fun _ -> emp) frame
   = let m0 = MSTTotal.get () in

lib/pulse/core/PulseCore.Memory.fsti

@@ -302,6 +302,21 @@ let fresh_wrt (ctx:list pre_inv)
               (i:iname)
   = forall i'. List.Tot.memP i' ctx ==> name_of_pre_inv i' <> i
 
+val distinct_invariants_have_distinct_names
+      (e:inames)
+      (p:slprop)
+      (q:slprop { p =!= q })
+      (i:inv p)
+      (j:inv q)
+  : action_except (squash (name_of_inv i =!= name_of_inv j)) e emp (fun _ -> emp)
+
+val invariant_name_identifies_invariant
+      (e:inames)
+      (p q:slprop)
+      (i:inv p)
+      (j:inv q { name_of_inv i == name_of_inv j } )
+  : action_except (squash (p == q /\ i == j)) e emp (fun _ -> emp)
+
 val fresh_invariant (e:inames) (p:slprop) (ctx:list pre_inv)
   : action_except (i:inv p { not (mem_inv e i) /\ fresh_wrt ctx (name_of_inv i) }) e p (fun _ -> emp)
 

lib/pulse/lib/Pulse.Lib.Core.fst

@@ -139,7 +139,8 @@ let lift_atomic1 = A.lift_atomic1
 let lift_atomic2 = A.lift_atomic2
 let new_invariant = A.new_invariant
 let with_invariant = A.with_invariant
-
+let distinct_invariants_have_distinct_names #p #q i j = A.distinct_invariants_have_distinct_names #p #q i j ()
+let invariant_name_identifies_invariant #p #q i j = A.invariant_name_identifies_invariant p q i j
 ////////////////////////////////////////////////////////////////////
 // Ghost computations
 ////////////////////////////////////////////////////////////////////

lib/pulse/lib/Pulse.Lib.Core.fsti

@@ -359,6 +359,26 @@ val with_invariant
                             (fun x -> p ** fp' x))
 : stt_atomic a #(join_obs obs Unobservable) (add_inv f_opens i) fp fp'
 
+val distinct_invariants_have_distinct_names
+    (#p #q:vprop)
+    (i:inv p)
+    (j:inv q { (p =!= q) })
+: stt_atomic (_:squash (name_of_inv i =!= name_of_inv j))
+    #Unobservable
+    emp_inames
+    emp
+    (fun _ -> emp)
+
+val invariant_name_identifies_invariant
+      (#p #q:vprop)
+      (i:inv p)
+      (j:inv q { name_of_inv i == name_of_inv j } )
+: stt_atomic (squash (p == q /\ i == j))
+    #Unobservable
+    emp_inames
+    emp
+    (fun _ -> emp)
+
 //////////////////////////////////////////////////////////////////////////
 // Ghost computations
 //////////////////////////////////////////////////////////////////////////