New matching: no backtracking on SMT results

.gitignore

@@ -26,3 +26,6 @@ _cache
 FStar
 _pak
 pulse.tar.gz
+
+# make touchfiles
+.*.touch

lib/common/Pulse.Lib.Core.fsti

@@ -23,29 +23,27 @@ module T = FStar.Tactics.V2
 open Pulse.Lib.Dv {}
 open FStar.ExtractAs
 
-(* This attribute can be used on the indexes of a slprop
-   to instruct the checker to call the SMT solver to relate
-   occurrences of that index.
-
-   For example, if you have
-
-     val pts_to (x:ref a) ([@@@equate_by_smt] v:a) : slprop
-
-   Then `pts_to x (a + b)` and `pts_to x (b + a)` will be
-   matched by the prover by emitting an SMT query (a + b) == (b + a). Of course,
-   `pts_to x a` and `pts_to x a` will be matched purely by unification without
-   emitted a trivial SMT query (a == a).
-
-   By default, if none of the indexes of a slprop are marked with "equate_by_smt",
-   the _last_ argument of a slprop is considered to be equated by SMT. This makes
-   it convenient to write slprops like the one below, without paying special
-   heed to this attribute.
-
-     val pts_to (x:ref a) (v:a) : slprop
+(* Arguments of slprops can be marked as a matching key to
+   1- Make sure we do no try to use the SMT to match resources with
+      different matching keys (in other words, we only use the unifier to
+      match the matching keys).
+   2- Indicate that we only expect a single instance of the resource for
+      a given set of matching keys, so we allow the use of SMT for the rest
+      of the arguments.
+
+     val pts_to ([@@@mkey] x : ref a) (v : a) : slprop
+
+   Then `pts_to x (a + b)` and `pts_to x (b + a)` will be matched by the
+   prover by emitting an SMT query `pts_to x (a + b) == pts_to x (b +
+   a)`. (Note we ask for this possibly weaker fact instead of `(a + b)
+   == (b + a)`; this can be useful when the definition of the resource
+   is not injective.)
+
+   Of course, `pts_to x a` and `pts_to x a` will be matched purely by
+   unification without even emitting a trivial SMT query (a == a).
 *)
-val equate_by_smt    : unit (* now meaningless. *)
-val equate_strict    : unit (* only use fastunif *)
-val equate_syntactic : unit (* only use term_eq *)
+val mkey : unit
+val no_mkeys : unit
 
 (** This attribute allows to do ambiguous proving when calling a function. *)
 val allow_ambiguous : unit
@@ -177,7 +175,10 @@ let (/!) (is1 is2 : inames) : Type0 =
   GhostSet.disjoint is1 is2
 
 val inv (i:iname) (p:slprop) : slprop
+
+[@@no_mkeys]
 val inames_live (inames:inames) : slprop
+
 let mem_iname (e:inames) (i:iname) : erased bool = elift2 (fun e i -> GhostSet.mem i e) e i
 let mem_inv (e:inames) (i:iname) : GTot bool = mem_iname e i
 
@@ -525,7 +526,7 @@ val later_equiv (p q: slprop) : squash (later (equiv p q) == equiv (later p) (la
 [@@erasable]
 val slprop_ref : Type0
 
-val slprop_ref_pts_to (x: slprop_ref) (y: slprop) : slprop
+val slprop_ref_pts_to ([@@@mkey]x: slprop_ref) (y: slprop) : slprop
 
 val slprop_ref_alloc (y: slprop)
 : stt_ghost slprop_ref emp_inames emp fun x -> slprop_ref_pts_to x y
@@ -688,7 +689,7 @@ let pcm_ref
 val pcm_pts_to
     (#a:Type u#1)
     (#p:pcm a)
-    ([@@@equate_strict] r:pcm_ref p)
+    ([@@@mkey] r:pcm_ref p)
     (v:a)
 : slprop
 
@@ -793,7 +794,7 @@ instance val non_informative_ghost_pcm_ref
 val ghost_pcm_pts_to
     (#a:Type u#1)
     (#p:pcm a)
-    ([@@@equate_strict] r:ghost_pcm_ref p)
+    ([@@@mkey] r:ghost_pcm_ref p)
     (v:a)
 : slprop
 
@@ -867,7 +868,7 @@ val ghost_gather
 val big_pcm_pts_to
     (#a:Type u#2)
     (#p:pcm a)
-    ([@@@equate_strict] r:pcm_ref p)
+    ([@@@mkey] r:pcm_ref p)
     (v:a)
 : slprop
 
@@ -946,7 +947,7 @@ val big_gather
 val big_ghost_pcm_pts_to
     (#a:Type u#2)
     (#p:pcm a)
-    ([@@@equate_strict] r:ghost_pcm_ref p)
+    ([@@@mkey] r:ghost_pcm_ref p)
     (v:a)
 : slprop
 

lib/core/Pulse.Lib.Core.fst

@@ -22,9 +22,9 @@ open PulseCore.FractionalPermission
 open PulseCore.Observability
 friend PulseCore.InstantiatedSemantics
 module Sep = PulseCore.IndirectionTheorySep
-let equate_by_smt = ()
-let equate_strict = ()
-let equate_syntactic = ()
+
+let mkey = ()
+let no_mkeys = ()
 
 let allow_ambiguous = ()
 

lib/pulse/c/Pulse.C.Types.Array.fsti

@@ -179,12 +179,12 @@ inline_for_extraction [@@noextract_to "krml"]
 let array_ref (#t: Type) (td: typedef t) = (a: array_ptr td { g_array_ptr_is_null a == false })
 
 (*
-val array_ref_base_size_type (#t: Type) (#td: typedef t) (a: array_ref td) : GTot Type0
+val array_ref_base_size_type (#t: Type) (#td: typedef t) (a: array_ref td) : Type0
 *)
 val array_ref_base_size (#t: Type) (#td: typedef t) (a: array_ptr td) : Ghost SZ.t
   (requires True)
   (ensures (fun y -> SZ.v y == 0 <==> a == null_array_ptr td))
-val has_array_ref_base (#t: Type) (#td: typedef t) (a: array_ref td) (#ty: Type) (r: ref (base_array0 ty td (array_ref_base_size a))) : GTot prop
+val has_array_ref_base (#t: Type) (#td: typedef t) (a: array_ref td) (#ty: Type) (r: ref (base_array0 ty td (array_ref_base_size a))) : prop
 val has_array_ref_base_inj (#t: Type) (#td: typedef t) (a: array_ref td) (#ty: Type) (r1 r2: ref (base_array0 ty td (array_ref_base_size a))) : Lemma
   (requires (has_array_ref_base a r1 /\ has_array_ref_base a r2))
   (ensures (r1 == r2))
@@ -323,7 +323,7 @@ let has_array_of_base
   (#td: typedef t)
   (r: ref (base_array0 tn td n))
   (a: array td)
-: GTot prop
+: prop
 =   let (| al, len |) = a in
     array_ref_base_size al == n /\
     has_array_ref_base al #tn r /\
@@ -390,7 +390,7 @@ let array_ref_of_base_post
   (r: ref (base_array0 tn td n))
   (a: array_ref td)
   (ar: array td)
-: GTot prop
+: prop
 =
        array_ptr_of ar == a /\
         array_ref_base_size a == Ghost.reveal n /\
@@ -521,7 +521,7 @@ ensures
 }
 
 
-let full_seq (#t: Type) (td: typedef t) (v: Seq.seq t) : GTot prop =
+let full_seq (#t: Type) (td: typedef t) (v: Seq.seq t) : prop =
   forall (i: nat { i < Seq.length v }) . {:pattern (Seq.index v i)} full td (Seq.index v i)
 
 let full_seq_seq_of_base_array
@@ -907,7 +907,7 @@ let array_ref_split_post
   (a: array td)
   (i: SZ.t)
   (sl sr: Ghost.erased (Seq.seq t))
-: GTot prop
+: prop
 = SZ.v i <= array_length a /\ Seq.length s == array_length a /\
   Ghost.reveal sl == Seq.slice s 0 (SZ.v i) /\
   Ghost.reveal sr == Seq.slice s (SZ.v i) (Seq.length s)
@@ -983,7 +983,7 @@ val array_join
     ))
     (fun _ -> array_pts_to a (sl `Seq.append` sr))
 
-let fractionable_seq (#t: Type) (td: typedef t) (s: Seq.seq t) : GTot prop =
+let fractionable_seq (#t: Type) (td: typedef t) (s: Seq.seq t) : prop =
   forall (i: nat). i < Seq.length s ==> fractionable td (Seq.index s i)
 
 let mk_fraction_seq (#t: Type) (td: typedef t) (s: Seq.seq t) (p: perm) : Ghost (Seq.seq t)
@@ -1055,7 +1055,7 @@ let array_blit_post
   (idx_dst: SZ.t)
   (len: SZ.t)
   (s1' : Ghost.erased (Seq.seq t))
-: GTot prop
+: prop
 =
   SZ.v idx_src + SZ.v len <= array_length src /\
   SZ.v idx_dst + SZ.v len <= array_length dst /\

lib/pulse/c/Pulse.C.Types.Base.fsti

@@ -33,7 +33,7 @@ val typedef (t: Type0) : Type0
 inline_for_extraction [@@noextract_to "krml"]
 let typeof (#t: Type0) (td: typedef t) : Tot Type0 = t
 
-val fractionable (#t: Type0) (td: typedef t) (x: t) : GTot prop
+val fractionable (#t: Type0) (td: typedef t) (x: t) : prop
 
 val mk_fraction (#t: Type0) (td: typedef t) (x: t) (p: perm) : Ghost t
   (requires (fractionable td x))
@@ -48,7 +48,7 @@ val mk_fraction_compose (#t: Type0) (td: typedef t) (x: t) (p1 p2: perm) : Lemma
   (requires (fractionable td x /\ p1 <=. 1.0R /\ p2 <=. 1.0R))
   (ensures (mk_fraction td (mk_fraction td x p1) p2 == mk_fraction td x (p1 `prod_perm` p2)))
 
-val full (#t: Type0) (td: typedef t) (v: t) : GTot prop
+val full (#t: Type0) (td: typedef t) (v: t) : prop
 
 val uninitialized (#t: Type0) (td: typedef t) : Ghost t
   (requires True)
@@ -115,10 +115,10 @@ let null (#t: Type) (td: typedef t) : Tot (ptr td) = null_gen t
 inline_for_extraction [@@noextract_to "krml"]
 let ref (#t: Type) (td: typedef t) : Tot Type0 = (p: ptr td { ~ (p == null td) })
 
-val pts_to (#t: Type) (#[@@@equate_by_smt]td: typedef t) (r: ref td) ([@@@equate_by_smt] v: Ghost.erased t) : slprop
+val pts_to (#t: Type) (#td: typedef t) ([@@@mkey]r: ref td) (v: Ghost.erased t) : slprop
 
 let pts_to_or_null
-  (#t: Type) (#[@@@equate_by_smt]td: typedef t) (p: ptr td) ([@@@equate_by_smt] v: Ghost.erased t) : slprop
+  (#t: Type) (#td: typedef t) ([@@@mkey]p: ptr td) (v: Ghost.erased t) : slprop
 = if FStar.StrongExcludedMiddle.strong_excluded_middle (p == null _)
   then emp
   else pts_to p v