Towards supporting universe branch.

Author: gebner

lib/common/Pulse.Lib.PCM.Raise.fst

@@ -30,7 +30,7 @@ let raise_compatible
       op p frame x == y
   returns compatible (raise u#a u#b p) (U.raise_val x) (U.raise_val y)
   with _ . (
-    assert (composable (raise p) (U.raise_val x) (U.raise_val frame))
+    assert (composable (raise u#a u#b p) (U.raise_val x) (U.raise_val frame))
   )
 
 
@@ -49,7 +49,7 @@ let raise_refine
   let ya = f va in
   let y = U.raise_val ya in
   assert (compatible p ya va);
-  raise_compatible p ya va;
+  raise_compatible u#a u#b p ya va;
   y
 
   let raise_upd
@@ -60,5 +60,5 @@ let raise_refine
   = fun x -> 
       let ra = f (U.downgrade_val x) in
       let res = U.raise_val ra in
-      raise_compatible p y ra;
+      raise_compatible u#a u#b p y ra;
       res

lib/core/PulseCore.BaseHeapSig.fst

@@ -27,15 +27,15 @@ let star_equiv (p q:slprop) (m:mem u#a)
 let slprop_extensionality (p q:slprop)
 : Lemma ((forall c. interp p c <==> interp q c) ==> p == q)
         [SMTPat (p == q)]
-= introduce (forall c. interp p c <==> interp q c) ==> p == q with _.
+= introduce (forall c. H2.interp p c <==> interp q c) ==> p == q with _.
   H2.slprop_extensionality p q
 
-let star_commutative (p q: slprop) : Lemma (star p q == star q p) =
+let star_commutative (p q: slprop u#a) : Lemma (star p q == star q p) =
   introduce forall c. interp (star p q) c <==> interp (star q p) c with (
     star_equiv p q c;
     star_equiv q p c;
-    introduce forall (a b: mem). disjoint_mem a b <==> disjoint_mem b a with H2.disjoint_sym a b;
-    introduce forall (h0 h1: mem). disjoint_mem h0 h1 ==> disjoint_mem h1 h0 /\ join_mem h0 h1 == join_mem h1 h0 with
+    introduce forall (a b: mem u#a). disjoint_mem a b <==> disjoint_mem b a with H2.disjoint_sym a b;
+    introduce forall (h0 h1: mem u#a). disjoint_mem h0 h1 ==> disjoint_mem h1 h0 /\ join_mem h0 h1 == join_mem h1 h0 with
       introduce _ ==> _ with _. H2.join_commutative h0 h1
   );
   slprop_extensionality (star p q) (star q p)
@@ -124,30 +124,29 @@ let lower (frame: slprop) (m: mem) : p:H2.slprop { forall h. H2.interp p h <==>
 
 let ac_lemmas ()
 : Lemma (
-    (forall p q r. (p `star` q) `star` r == p `star` (q `star` r)) /\
-    (forall p q. p `star` q == q `star` p) /\
-    (forall p. p `star` emp == p)
+    (forall (p q r : slprop u#a). (p `star` q) `star` r == p `star` (q `star` r)) /\
+    (forall (p q: slprop u#a). p `star` q == q `star` p) /\
+    (forall (p: slprop u#a). p `star` emp == p)
 )
-= FStar.Classical.forall_intro_3 (star_associative);
-  FStar.Classical.forall_intro_2 (star_commutative);
-  FStar.Classical.forall_intro emp_unit
+= FStar.Classical.forall_intro_3 (star_associative u#a);
+  FStar.Classical.forall_intro_2 (star_commutative u#a);
+  FStar.Classical.forall_intro (emp_unit u#a)
 
 let destruct_star_l (p q:slprop) (m:mem)
 : Lemma (interp (p `star` q) m ==> interp p m)
 = star_equiv p q m
 
-let destruct_star (p q:slprop) (m:mem)
+let destruct_star (p q:slprop u#a) (m:mem)
 : Lemma (interp (p `star` q) m ==> interp p m /\ interp q m)
-= ac_lemmas ();
+= ac_lemmas u#a ();
   destruct_star_l p q m;
   destruct_star_l q p m
 
 let elim_init (fp: H2.slprop) (frame:slprop u#a) (m:mem)
 : Lemma 
   (requires interp (fp `star` frame) m)
   (ensures H2.interp fp m /\ H2.interp (fp `H2.star` lower frame m) m)
-= ac_lemmas ();
-  destruct_star fp frame m;
+= destruct_star fp frame m;
   assert H2.interp fp m;
   star_equiv fp frame m;
   let m1 = IndefiniteDescription.indefinite_description_ghost _ fun m1 -> exists m2.
@@ -190,9 +189,8 @@ let intro_fin (post: H2.slprop) (frame:slprop) (m:mem)
   assert disjoint_mem m1 m2;
   assert join_mem m1 m2 == m;
   star_equiv post frame m;
-  assert interp (post `star` frame) m;
-  ac_lemmas ()
-              
+  assert interp (post `star` frame) m
+
 let lift_heap_action
       (#fp:H2.slprop u#a)
       (#a:Type u#b)

lib/core/PulseCore.Heap.fst

@@ -33,10 +33,10 @@ let ctr (h: heap) : nat = Seq.length h
 let select i h =
   if i < ctr h then Seq.index h i else None
 
-let empty_heap' n = Seq.create n None
+let empty_heap' n : heap u#a = Seq.create n None
 
-let select_empty_heap' a n : Lemma (select a (empty_heap' n) == None) [SMTPat (select a (empty_heap' n))] =
-  reveal_opaque (`%select) (select a (empty_heap' n))
+let select_empty_heap' a n : Lemma (select a (empty_heap' u#a n) == None) [SMTPat (select a (empty_heap' u#a n))] =
+  reveal_opaque (`%select) (select a (empty_heap' u#a n))
 
 let empty_heap = empty_heap' 0
 
@@ -59,11 +59,11 @@ let update_addr' (m:heap) (a:addr { a < ctr m }) (c:option cell)
   : heap
   = Seq.upd m a c
 
-let select_update_addr' m a b c :
+let select_update_addr' (m: heap u#a) a b c :
     Lemma (select a (update_addr' m b c) ==
       (if a = b then c else select a m))
     [SMTPat (select a (update_addr' m b c))] =
-  reveal_opaque (`%select) (select a)
+  reveal_opaque (`%select) (select u#a a)
 
 let update_addr (m:heap) (a:addr { a < ctr m }) (c:cell)
   : heap
@@ -151,7 +151,7 @@ let join (m0:heap) (m1:heap{disjoint m0 m1})
 let ctr_join_def m0 m1 : Lemma (ctr (join m0 m1) == max (ctr m0) (ctr m1)) [SMTPat (ctr (join m0 m1))] =
   reveal_opaque (`%join) (join m0 m1)
 
-let select_join_def a m0 m1 :
+let select_join_def a (m0: heap u#a) m1 :
     Lemma (select a (join m0 m1) ==
       (match select a m0, select a m1 with
       | None, None -> None
@@ -160,7 +160,7 @@ let select_join_def a m0 m1 :
       | Some c0, Some c1 ->
         Some (join_cells c0 c1)))
       [SMTPat (select a (join m0 m1))] =
-  reveal_opaque (`%select) (select a);
+  reveal_opaque (`%select) (select u#a a);
   reveal_opaque (`%join) (join m0 m1)
 
 let disjoint_join_cells_assoc (c0 c1 c2:cell u#h)
@@ -202,14 +202,14 @@ let disjoint_join' (m0 m1 m2:heap u#h)
 let mem_equiv (m0 m1:heap) =
   ctr m0 == ctr m1 /\ forall a. select a m0 == select a m1
 
-let mem_equiv_eq (m0 m1:heap)
+let mem_equiv_eq (m0 m1:heap u#a)
   : Lemma
     (requires
       m0 `mem_equiv` m1)
     (ensures
       m0 == m1)
     [SMTPat (m0 `mem_equiv` m1)]
-  = reveal_opaque (`%select) select; assert Seq.equal m0 m1
+  = reveal_opaque (`%select) (select u#a); assert Seq.equal m0 m1
 
 let join_cells_commutative (c0:cell u#h) (c1:cell u#h{disjoint_cells c0 c1})
   : Lemma (disjoint_cells_sym c0 c1; join_cells c0 c1 == join_cells c1 c0)
@@ -422,24 +422,11 @@ let affine_star p q h = ()
 
 let equiv_symmetric (p1 p2:slprop u#a) = ()
 let equiv_extensional_on_star (p1 p2 p3:slprop u#a) = ()
-let emp_unit p
-  = let emp_unit_1 p m
-      : Lemma
-        (requires interp p m)
-        (ensures  interp (p `star` emp) m)
-        [SMTPat (interp (p `star` emp) m)]
-      = assert (disjoint empty_heap m);
-        assert (interp (p `star` emp) (join m empty_heap));
-        assert (mem_equiv m (join m empty_heap))
-    in
-    let emp_unit_2 p m
-      : Lemma
-        (requires interp (p `star` emp) m)
-        (ensures interp p m)
-        [SMTPat (interp (p `star` emp) m)]
-      = affine_star p emp m
-    in
-    ()
+
+let emp_unit (p: slprop u#a) =
+  introduce forall (m: heap u#a). interp p m <==> interp (p `star` emp) m with
+    (join_empty m; affine_star p emp m)
+
 
 let intro_emp h = ()
 
@@ -793,21 +780,17 @@ let sel_action' (#a:_) (#pcm:_)
   = sel_v r v0 h
 
 let refined_pre_action (#immut:bool)
-                       (#[T.exact (`trivial_pre)]pre:heap ->prop)
-                       (#[T.exact (`trivial_pre)]post:heap -> prop)
                        (fp0:slprop) (a:Type) (fp1:a -> slprop) =
   m0:full_hheap fp0 ->
   Pure (x:a &
         full_hheap (fp1 x))
-       (requires pre m0)
+       (requires True)
        (ensures fun  (| x, m1 |) ->
-         post m1 /\
          (forall frame. frame_related_heaps m0 m1 fp0 (fp1 x) frame immut))
 
-#restart-solver
-let refined_pre_action_as_action #immut #pre #post (#fp0:slprop) (#a:Type) (#fp1:a -> slprop)
-                                 ($f:refined_pre_action #immut #pre #post fp0 a fp1)
-  : action #immut #pre #post fp0 a fp1
+let refined_pre_action_as_action #immut (#fp0:slprop) (#a:Type) (#fp1:a -> slprop)
+                                 ($f:refined_pre_action #immut fp0 a fp1)
+  : action #immut fp0 a fp1
   = let g : pre_action fp0 a fp1 = fun m -> f m in
     g
 
@@ -1162,10 +1145,10 @@ let pts_to_not_null_action #a #pcm r v
     refined_pre_action_as_action g
 
 ////////////////////////////////////////////////////////////////////////////////
-let select_snoc (h: heap) (c: option cell) a :
+let select_snoc (h: heap u#a) (c: option cell) a :
     Lemma (select a (Seq.snoc h c) == (if a = ctr h then c else select a h))
       [SMTPat (select a (Seq.snoc h c))] =
-  reveal_opaque (`%select) (select a)
+  reveal_opaque (`%select) (select u#a a)
 
 let extend_full_heap_with (h: full_heap) (c: cell {full_cell c}) :
     h':full_heap {
@@ -1220,13 +1203,13 @@ let extend #a #pcm
 #push-options "--z3rlimit_factor 4 --max_fuel 1 --max_ifuel 1"
 #restart-solver
 let frame (#a:Type)
-          (#immut #hpre #hpost:_)
+          #immut
           (#pre:slprop)
           (#post:a -> slprop)
           (frame:slprop)
           ($f:action pre a post)
   = let g 
-      : refined_pre_action #immut #hpre #hpost 
+      : refined_pre_action #immut
           (pre `star` frame) a (fun x -> post x `star` frame)
         = fun h0 ->
               assert (interp (pre `star` frame) h0);
@@ -1264,15 +1247,14 @@ let pts_to_evolve (#a:Type u#a) (#pcm:_) (r:ref a pcm) (x y : a) (h:heap)
     compatible_trans pcm y x v'
 
 let erase_action_result
-      (#pre #post:_)
       (#immut:_)
       (#fp:slprop)
       (#a:Type)
       (#fp':a -> slprop)
-      (act:action #immut #pre #post fp a fp')
-: action #immut #pre #post fp (erased a) (fun x -> fp' x)
+      (act:action #immut fp a fp')
+: action #immut fp (erased a) (fun x -> fp' x)
 = let g
-  : refined_pre_action #immut #pre #post fp (erased a) (fun x -> fp' x)
+  : refined_pre_action #immut fp (erased a) (fun x -> fp' x)
   = fun h ->
     let (| x, h1 |) = act h in
     let y : erased a = hide x in
@@ -1282,13 +1264,12 @@ let erase_action_result
   refined_pre_action_as_action g
 
 let erase_action_result_identity
-      (#pre #post:_)
       (#immut:_)
       (#fp:slprop)
       (#a:Type)
       (#fp':a -> slprop)
-      (act:action #immut #pre #post fp a fp')
-      (h:full_hheap fp { pre h})
+      (act:action #immut fp a fp')
+      (h:full_hheap fp)
 : Lemma (
     let (| x, h1 |) = act h in
     let (| y, h2 |) = erase_action_result act h in

lib/core/PulseCore.Heap.fsti

@@ -390,14 +390,11 @@ let full_hheap fp = h:hheap fp { full_heap_pred h }
   The base type for an action is indexed by two separation logic propositions, representing
   the heap specification of the action before and after.
 *)
-let trivial_pre (h:heap) : prop = True
 module T = FStar.Tactics
-let pre_action (#[T.exact (`trivial_pre)]pre:heap -> prop)
-               (#[T.exact (`trivial_pre)]post:heap -> prop)
-               (fp:slprop u#a)
+let pre_action (fp:slprop u#a)
                (a:Type u#b)
                (fp':a -> slprop u#a)
-  = h0:full_hheap fp { pre h0 } -> res:(x:a & full_hheap (fp' x)) { post (dsnd res) }
+  = full_hheap fp -> x:a & full_hheap (fp' x)
 
 (**
   This is how the heaps before and after the action relate:
@@ -422,24 +419,21 @@ let action_related_heaps
 *)
 let is_frame_preserving
   (#a: Type u#a)
-  (#pre #post:_)
   (#fp: slprop u#b)
   (#fp': a -> slprop u#b)
   (immut:bool)
-  (f:pre_action #pre #post fp a fp')
+  (f:pre_action fp a fp')
   =
-  forall (frame: slprop u#b) (h0:full_hheap (fp `star` frame) { pre h0 }).
+  forall (frame: slprop u#b) (h0:full_hheap (fp `star` frame)).
      (affine_star fp frame h0;
       let (| x, h1 |) = f h0 in
       interp (fp' x `star` frame) h1 /\
       action_related_heaps #immut h0 h1)
 
 (** Every action is frame-preserving *)
 let action (#[T.exact (`mut_heap)] immut:bool)
-           (#[T.exact (`trivial_pre)]pre:heap -> prop)
-           (#[T.exact (`trivial_pre)]post:heap -> prop)
            (fp:slprop u#b) (a:Type u#a) (fp':a -> slprop u#b) =
-  f:pre_action #pre #post fp a fp'{ is_frame_preserving immut f }
+  f:pre_action fp a fp'{ is_frame_preserving immut f }
 
 (**
   Two heaps [h0] and [h1] are frame-related if you can get from [h0] to [h1] with a
@@ -460,13 +454,11 @@ let action_framing
   (#immut:bool)
   (#fp: slprop u#b)
   (#fp': a -> slprop u#b)
-  (#pre #post: heap u#b -> prop)
-  ($f:action #immut #pre #post fp a fp')
-  (frame:slprop) (h0:full_hheap (fp `star` frame) { pre h0 })
+  ($f:action #immut fp a fp')
+  (frame:slprop) (h0:full_hheap (fp `star` frame))
     : Lemma (
       affine_star fp frame h0;
       let (| x, h1 |) = f h0 in
-      post h1 /\
       frame_related_heaps h0 h1 fp (fp' x) frame immut
     )
   =
@@ -628,34 +620,32 @@ val extend
       (fun r -> pts_to r x)
 
 val frame (#a:Type)
-          #immut #hpre #hpost
+          #immut
           (#pre:slprop)
           (#post:a -> slprop)
           (frame:slprop)
-          ($f:action #immut #hpre #hpost pre a post)
-  : action #immut #hpre #hpost (pre `star` frame) a (fun x -> post x `star` frame)
+          ($f:action #immut pre a post)
+  : action #immut (pre `star` frame) a (fun x -> post x `star` frame)
 
 val pts_to_evolve (#a:Type u#a) (#pcm:_) (r:ref a pcm) (x y : a) (h:heap)
   : Lemma (requires (interp (pts_to r x) h /\ compatible pcm y x))
           (ensures  (interp (pts_to r y) h))
 
 val erase_action_result
-      (#pre #post:_)
       (#immut:_)
       (#fp:slprop)
       (#a:Type)
       (#fp':a -> slprop)
-      (act:action #immut #pre #post fp a fp')
-: action #immut #pre #post fp (erased a) (fun x -> fp' x)
+      (act:action #immut fp a fp')
+: action #immut fp (erased a) (fun x -> fp' x)
 
 val erase_action_result_identity
-      (#pre #post:_)
       (#immut:_)
       (#fp:slprop)
       (#a:Type)
       (#fp':a -> slprop)
-      (act:action #immut #pre #post fp a fp')
-      (h:full_hheap fp { pre h})
+      (act:action #immut fp a fp')
+      (h:full_hheap fp)
 : Lemma (
     let (| x, h1 |) = act h in
     let (| y, h2 |) = erase_action_result act h in