Merge branch 'main' of github.com:FStarLang/pulse into _taramana_slic…

…e_ghost_split

lib/pulse/core/PulseCore.Action.fst

@@ -181,28 +181,15 @@ let bind_pre_act_ghost
 let bind_pre_act_atomic
      (#a:Type u#a)
      (#b:Type u#b)
+     (#r1: reifiability)
+     (#r2: reifiability { r1 == Ghost \/ r2 == Ghost })
      (#except:inames)
      (#pre1 #post1 #post2:_)
-     (f:pre_act a Atomic except pre1 post1)
-     (g:(x:a -> pre_act b Atomic except (post1 x) post2))
+     (f:pre_act a r1 except pre1 post1)
+     (g:(x:a -> pre_act b r2 except (post1 x) post2))
 : pre_act b Atomic except pre1 post2
 = fun frame -> ST.bind (f frame) (fun x -> g x frame)
 
-let bind_pre_act
-     (#a:Type u#a)
-     (#b:Type u#b)
-     (#r:reifiability)
-     (#except:inames)
-     (#pre1 #post1 #post2:_)
-     (f:pre_act a r except pre1 post1)
-     (g:(x:a -> pre_act b r except (post1 x) post2))
-: pre_act b r except pre1 post2
-= match r with
-  | Ghost -> 
-    bind_pre_act_ghost #a #b #except #pre1 #post1 #post2 f g
-  | Atomic ->
-    bind_pre_act_atomic #a #b #except #pre1 #post1 #post2 f g
-
 let frame_pre_act_ghost
      (#a:Type u#a)
      (#except:inames)
@@ -250,16 +237,27 @@ let return
 : act a r emp_inames (post x) post
 = fun #ictx -> return_pre_act #a #ictx #post x
 
-let bind
+let bind_ghost
      (#a:Type u#a)
      (#b:Type u#b)
-     (#r:reifiability)
      (#opens:inames)
      (#pre1 #post1 #post2:_)
-     (f:act a r opens pre1 post1)
-     (g:(x:a -> act b r opens (post1 x) post2))
-: act b r opens pre1 post2
-= fun #ictx -> bind_pre_act #a #b #r #ictx #pre1 #post1 #post2 (f #ictx) (fun x -> g x #ictx)
+     (f:act a Ghost opens pre1 post1)
+     (g:(x:a -> act b Ghost opens (post1 x) post2))
+: act b Ghost opens pre1 post2
+= fun #ictx -> bind_pre_act_ghost #a #b #ictx #pre1 #post1 #post2 (f #ictx) (fun x -> g x #ictx)
+
+let bind_atomic
+     (#a:Type u#a)
+     (#b:Type u#b)
+     (#r1: reifiability)
+     (#r2: reifiability { r1 == Ghost \/ r2 == Ghost })
+     (#opens:inames)
+     (#pre1 #post1 #post2:_)
+     (f:act a r1 opens pre1 post1)
+     (g:(x:a -> act b r2 opens (post1 x) post2))
+: act b Atomic opens pre1 post2
+= fun #ictx -> bind_pre_act_atomic #a #b #r1 #r2 #ictx #pre1 #post1 #post2 (f #ictx) (fun x -> g x #ictx)
 
 let frame
      (#a:Type u#a)
@@ -395,23 +393,10 @@ let later_elim (p:slprop)
 : act unit Ghost emp_inames (later p ** later_credit 1) (fun _ -> p)
 = fun #ictx -> ITA.later_elim ictx p
 
-let maybe_p (p:slprop) (b:erased bool) : slprop = if b then p else emp
-
-let maybe_buy (n:nat)
-: stt (erased bool) emp (maybe_p (later_credit n))
-= stt_of_action0 (ITA.buy emp_inames n)
-
-let rec reveal_div #t (b:erased bool) (k: squash (reveal b == true) -> t) : Dv t = 
-  reveal_div b k
+let buy1 ()
+: stt unit emp (fun _ -> later_credit 1)
+= stt_of_action0 (ITA.buy emp_inames)
 
-let buy (n:nat)
-: stt unit emp (fun _ -> later_credit n)
-= I.bind 
-       (maybe_buy n) 
-       (fun (b:erased bool) ->
-        I.hide_div (fun _ -> 
-          reveal_div b (fun _ -> 
-          coerce_eq () <| I.return () (fun _ -> later_credit n))))
 ///////////////////////////////////////////////////////////////////
 // Core operations on references
 ///////////////////////////////////////////////////////////////////

lib/pulse/core/PulseCore.Action.fsti

@@ -66,15 +66,25 @@ val return
     (x:a)
 : act a r emp_inames (post x) post
 
-val bind
+val bind_ghost
      (#a:Type u#a)
      (#b:Type u#b)
-     (#r:reifiability)
      (#opens:inames)
      (#pre1 #post1 #post2:_)
-     (f:act a r opens pre1 post1)
-     (g:(x:a -> act b r opens (post1 x) post2))
-: act b r opens pre1 post2
+     (f:act a Ghost opens pre1 post1)
+     (g:(x:a -> act b Ghost opens (post1 x) post2))
+: act b Ghost opens pre1 post2
+
+val bind_atomic
+     (#a:Type u#a)
+     (#b:Type u#b)
+     (#r1: reifiability)
+     (#r2: reifiability { r1 == Ghost \/ r2 == Ghost })
+     (#opens:inames)
+     (#pre1 #post1 #post2:_)
+     (f:act a r1 opens pre1 post1)
+     (g:(x:a -> act b r2 opens (post1 x) post2))
+: act b Atomic opens pre1 post2
 
 val frame
      (#a:Type u#a)
@@ -182,8 +192,8 @@ val later_intro (p:slprop)
 val later_elim (p:slprop)
 : act unit Ghost emp_inames (later p ** later_credit 1) (fun _ -> p)
 
-val buy (n:nat)
-: stt unit emp (fun _ -> later_credit n)
+val buy1 ()
+: stt unit emp (fun _ -> later_credit 1)
 
 ////////////////////////////////////////////////////////////////////////
 // References

lib/pulse/core/PulseCore.Atomic.fst

@@ -95,9 +95,9 @@ let bind_atomic
     (e1:stt_atomic a #obs1 opens pre1 post1)
     (e2:(x:a -> stt_atomic b #obs2 opens (post1 x) post2))
 = match r_of_obs obs1, r_of_obs obs2 with
-  | Ghost, Ghost -> A.bind e1 e2
-  | Ghost, _ -> A.bind (A.lift_ghost_atomic e1) e2
-  | _, Ghost -> A.bind e1 (fun x -> A.lift_ghost_atomic (e2 x))
+  | Ghost, Ghost -> A.bind_ghost e1 e2
+  | Ghost, _ -> A.bind_atomic e1 e2
+  | _, Ghost -> A.bind_atomic e1 e2
 
 let lift_observability
     (#a:Type u#a)
@@ -205,7 +205,7 @@ let bind_ghost
 : stt_ghost b opens pre1 post2
 = let e1 = Ghost.reveal e1 in
   let e2 = FStar.Ghost.Pull.pull (fun (x:a) -> Ghost.reveal (e2 x)) in
-  Ghost.hide (A.bind e1 e2)
+  Ghost.hide (A.bind_ghost e1 e2)
 
 let lift_ghost_neutral
     (#a:Type u#a)
@@ -312,7 +312,7 @@ let with_invariant_g #a #fp #fp' #f_opens #p i $f =
 let invariant_name_identifies_invariant p q i j = Ghost.hide (A.invariant_name_identifies_invariant p q i)
 let later_intro p = Ghost.hide (A.later_intro p)
 let later_elim p = Ghost.hide (A.later_elim p)
-let buy = A.buy
+let buy1 = A.buy1
 
 let pts_to_not_null #a #p r v = Ghost.hide (A.pts_to_not_null #a #p r v)
 let alloc #a #pcm x = A.alloc x

lib/pulse/core/PulseCore.Atomic.fsti

@@ -316,8 +316,8 @@ val later_intro (p:slprop)
 val later_elim (p:slprop)
 : stt_ghost unit emp_inames (later p ** later_credit 1) (fun _ -> p)
 
-val buy (n:nat)
-: stt unit emp (fun _ -> later_credit n)
+val buy1 ()
+: stt unit emp (fun _ -> later_credit 1)
 
 ////////////////////////////////////////////////////////////////////////
 // References

lib/pulse/core/PulseCore.IndirectionTheoryActions.fst

@@ -309,43 +309,16 @@ let later_elim (e:inames) (p:slprop)
     assert (is_full s2);
     (), s2
 
-let buy (e:inames) (n:FStar.Ghost.erased nat)
-: act (erased bool) e emp (fun b -> if b then later_credit n else emp)
-= fun frame s0 ->
-    sep_laws();
-    let m0, m1 = split_mem emp (frame `star` mem_invariant e s0) s0 in
-    let m0' : erased mem = buy n m0 in
-    buy_lemma n m0;
-    interp_later_credit n m0';
-    assert (interp (later_credit n) m0');
-    buy_disjoint n m0 m1;
-    assert (disjoint m0' m1);
-    intro_star (later_credit n) (frame `star` mem_invariant e s0) m0' m1;
-    let m' : erased mem = join m0' m1 in
-    let s1 = buy_mem n s0 in
-    assert (reveal m' == s1);
-    mem_invariant_buy e n s0;
-    inames_ok_update e s0 s1;
-    let ok : erased bool = level s1 > credits s1 in
-    let s : (s:erased mem {
-      is_ghost_action s0 s /\
-      is_full s /\
-      interp 
-        ((if ok then later_credit n else emp) `star`
-         frame `star`
-         mem_invariant e s) s
-    })
-    = if ok
-      then (
-        hide s1
-      )
-      else (
-        is_ghost_action_refl s0;
-        hide s0
-      )
-    in
-    let s1 = update_ghost s0 s in
-    ok, s1
+let buy (e:inames)
+: act unit e emp (fun _ -> later_credit 1)
+= fun frame m0 -> (
+    let m1 = buy1_mem m0 in
+    interp_later_credit 1 m1;
+    intro_star (later_credit 1) (emp `star` frame `star` mem_invariant e m0) m1 m0;
+    disjoint_join_levels m1 m0;
+    sep_laws ();
+    (), join_mem m1 m0
+)
 
 let dup_inv (e:inames) (i:iref) (p:slprop)
 : ghost_act unit e 

lib/pulse/core/PulseCore.IndirectionTheoryActions.fsti

@@ -18,10 +18,12 @@ let _ACTION
   (frame:slprop)
 = HST.st #full_mem a
     (requires fun m0 ->
+        budget m0 >= 0 /\ (ATOMIC? ak ==> budget m0 > 0) /\
         inames_ok except m0 /\
         interp (expects `star` frame `star` mem_invariant except m0) m0)
     (ensures fun m0 x m1 ->
-        (GHOST? ak ==> is_ghost_action m0 m1) /\
+        budget m0 - budget m1 <= 1 /\
+        (GHOST? ak ==> is_ghost_action m0 m1 /\ budget m0 == budget m1) /\
         inames_ok except m1 /\
         interp (provides x `star` frame `star` mem_invariant except m1) m1 )
 
@@ -47,8 +49,8 @@ val later_intro (e:inames) (p:slprop)
 val later_elim (e:inames) (p:slprop) 
 : ghost_act unit e (later p `star` later_credit 1) (fun _ -> p)
 
-val buy (e:inames) (n:FStar.Ghost.erased nat)
-: act (FStar.Ghost.erased bool) e emp (fun b -> if b then later_credit n else emp)
+val buy (e:inames)
+: act unit e emp (fun _ -> later_credit 1)
 
 val dup_inv (e:inames) (i:iref) (p:slprop)
 : ghost_act unit e 

lib/pulse/core/PulseCore.IndirectionTheorySep.fst

@@ -813,18 +813,6 @@ let spend_lemma m = ()
 let spend_disjoint m0 m1 =
   mem_ext (spend (join m0 m1)) (join (spend m0) m1) fun _ -> ()
 
-let buy_mem n m =
-  PM.ghost_action_preorder ();
-  let m' = pack (level m) {
-    unpack m with
-    saved_credits = credits_ m + n;
-  } in
-  GS.lemma_equal_intro (hogs_dom m) (hogs_dom m');
-  m'
-let buy_lemma n m = ()
-let buy_disjoint n m0 m1 =
-  mem_ext (buy n (join m0 m1)) (join (buy n m0) m1) fun _ -> ()
-
 let iname_ok i m = hogs_iname_ok i m
 let inames_ok_single i p m = ()
 let iname_ok_inames_ok i m = ()
@@ -1061,9 +1049,6 @@ let mem_invariant_age e m0 m1 =
 let mem_invariant_spend e m =
   hogs_invariant_congr2 e m (spend m)
 
-let mem_invariant_buy e n m =
-  hogs_invariant_congr2 e m (buy n m)
-
 let hogs_single n (a: iref) (p: slprop) : mem =
   let m = pack n {
     saved_credits = 0;
@@ -1094,6 +1079,14 @@ let hogs_fresh_inv (p: slprop) (is: mem) (a: iref { None? (read is a) }) :
   hogs_single_invariant (level_ is) a p;
   is'
 
+let buy1_mem m =
+  PM.ghost_action_preorder ();
+  join_empty m;
+  let m' = update_credits (empty (level m)) 1 in
+  introduce forall (e: inames). mem_invariant e m == mem_invariant e (join_mem m' m) with
+    hogs_invariant_congr2 e m (join_mem m' m);
+  m'
+
 let inames_live (e:inames) : slprop =
   reveal_mem_le ();
   mk_slprop fun m ->

lib/pulse/core/PulseCore.IndirectionTheorySep.fsti

@@ -25,6 +25,7 @@ val mem: Type u#4
 val timeless_mem_of: mem -> timeless_mem
 val level (k:mem) : GTot nat
 val credits (k:mem) : GTot nat
+let budget (m: mem) : GTot int = level m - credits m - 1
 val update_timeless_mem (m: mem) (p: timeless_mem) :
   n:mem { timeless_mem_of n == p /\ level m == level n /\ credits m == credits n }
 
@@ -46,8 +47,7 @@ val update_ghost :
 
 let is_full (m:mem) 
 : prop
-= PM.pulse_heap_sig.full_mem_pred (timeless_mem_of m) /\
-  level m > credits m
+= PM.pulse_heap_sig.full_mem_pred (timeless_mem_of m)
 let full_mem = m:mem { is_full m  }
 
 val emp : slprop
@@ -295,26 +295,6 @@ val spend_disjoint (m0 m1:mem)
     disjoint (spend m0) m1 /\
     spend (join m0 m1) == join (spend m0) m1)
 
-val buy_mem (n:FStar.Ghost.erased nat) (m:mem) : m':mem {
-  is_ghost_action m m' /\
-  timeless_mem_of m' == timeless_mem_of m /\
-  (hogs_dom m == hogs_dom m')
-}
-let buy (n:nat) (m:mem) : mem = buy_mem n m
-val buy_lemma (n:nat) (m:mem)
-: Lemma (
-  let m' = buy n m in
-  level m' == level m /\
-  credits m' == credits m + n
-)
-val buy_disjoint (n:nat) (m0 m1:mem)
-: Lemma
-  (requires
-    disjoint m0 m1)
-  (ensures
-    disjoint (buy n m0) m1 /\
-    buy n (join m0 m1) == join (buy n m0) m1)
-
 let single (i:iref) : inames = FStar.GhostSet.singleton deq_iref i
 let add_inv (e:inames) (i:iref)
 : inames
@@ -404,9 +384,14 @@ val mem_invariant_spend (e:inames) (m:mem)
 : Lemma
   (ensures mem_invariant e m == mem_invariant e (spend_mem m))
 
-val mem_invariant_buy (e:inames) (n:nat) (m:mem)
-: Lemma
-  (ensures mem_invariant e m == mem_invariant e (buy_mem n m))
+val buy1_mem (m: mem { budget m > 0 }) : m': mem {
+  credits m' == 1 /\
+  disjoint m' m /\
+  (forall e. mem_invariant e m == mem_invariant e (join_mem m' m)) /\
+  (forall e. inames_ok e m <==> inames_ok e (join_mem m' m)) /\
+  (is_full m ==> is_full (join_mem m' m)) /\
+  is_ghost_action m (join_mem m' m)
+}
 
 val inames_live (e:inames) : slprop
 val inames_live_empty () : squash (emp == inames_live GhostSet.empty)

lib/pulse/core/PulseCore.InstantiatedSemantics.fst

@@ -32,8 +32,8 @@ let laws ()
 = Sep.sep_laws()
 
 let state0 (e:inames) : Sem.state u#4 = {
-    s = Sep.mem;
-    is_full_mem = Sep.is_full;
+    s = Sep.full_mem;
+    budget = Sep.budget;
     pred = slprop;
     emp = emp;
     star = star;
@@ -143,7 +143,7 @@ let sub (#a:Type u#a)
 : stt a pre2 post2
 = coerce_eq (conv pre1 pre2 post1 post2 pf1 pf2) e
 
-let par f0 f1 = fun _ -> Sem.par (f0 ()) (f1 ())
+let fork f0 = fun _ -> Sem.fork (f0 ())
 
 let hide_div #a #pre #post (f:unit -> Dv (stt a pre post))
 : stt a pre post

lib/pulse/core/PulseCore.InstantiatedSemantics.fsti

@@ -113,10 +113,8 @@ val sub (#a:Type u#a)
         (e:stt a pre1 post1)
 : stt a pre2 post2
 
-val par (#p0 #q0 #p1 #q1:_)
-        (f0:stt unit p0 (fun _ -> q0))
-        (f1:stt unit p1 (fun _ -> q1))
-: stt unit (p0 ** p1) (fun _ -> q0 ** q1)
+val fork #p0 (f0:stt unit p0 (fun _ -> emp))
+: stt unit p0 (fun _ -> emp)
 
 val hide_div #a #pre #post (f:unit -> Dv (stt a pre post))
 : stt a pre post