Revert ulib changes.

ulib/FStar.BigOps.fsti

@@ -174,7 +174,7 @@ let big_or #a (f: (a -> Type)) (l: list a) : prop =
 (** Mapping pairs of elements of [l] using [f] and combining them with
     [op]. *)
 [@@ __reduce__]
-let rec pairwise_op' #a #b (op: (b -> b -> GTot b)) (f: (a -> a -> GTot b)) (l: list a) (z: b) : GTot b =
+let rec pairwise_op' #a #b (op: (b -> b -> GTot b)) (f: (a -> a -> b)) (l: list a) (z: b) : GTot b =
   match l with
   | [] -> z
   | hd :: tl -> (map_op' op (f hd) tl z) `op` (pairwise_op' op f tl z)
@@ -195,7 +195,7 @@ let anti_reflexive (#a: Type) (f: (a -> a -> Type)) = forall x. ~(f x x)
 
       {[ pairwise_and f [a; b; c] = f a b /\ f a c /\ f b c ]} *)
 [@@ __reduce__]
-let pairwise_and' #a (f: (a -> a -> Type)) (l: list a) : Type = pairwise_op' (fun p q -> p /\ q) (fun x y -> f x y) l True
+let pairwise_and' #a (f: (a -> a -> Type)) (l: list a) : Type = pairwise_op' l_and f l True
 
 (** Equations for [pairwise_and] showing it to be a fold with [big_and] *)
 val pairwise_and'_nil (#a: Type) (f: (a -> a -> Type0)) : Lemma (pairwise_and' f [] == True)

ulib/FStar.Fin.fst

@@ -141,9 +141,9 @@ let rec pigeonhole_eq (#a:Type) (eq: equivalence_relation a)
       let index_of_first_pigeon = find_eq eq holes first_pigeon in //we carefully carve first_pigeon from (holes)
       let holes_except_first_pigeon = S.append (S.slice holes 0 (index_of_first_pigeon)) 
                                              (S.slice holes (index_of_first_pigeon+1) (S.length holes)) in 
-      introduce forall (x: items_of eq holes { not (eq x first_pigeon) }). contains_eq eq holes_except_first_pigeon x with
-        // all but first pigeon remain in reduced
-        (let index_of_x_in_holes = find_eq eq holes x in 
+      let all_but_first_pigeon_remain_in_reduced (x: items_of eq holes { not (eq x first_pigeon) }) 
+        : Lemma (contains_eq eq holes_except_first_pigeon x) 
+        = let index_of_x_in_holes = find_eq eq holes x in 
           reveal_opaque (`%contains_eq) (contains_eq eq);  
           if index_of_x_in_holes < index_of_first_pigeon 
           then assert (S.index holes index_of_x_in_holes == S.index holes_except_first_pigeon index_of_x_in_holes)
@@ -152,7 +152,8 @@ let rec pigeonhole_eq (#a:Type) (eq: equivalence_relation a)
             Classical.move_requires (trans_lemma eq x (S.index holes index_of_x_in_holes)) first_pigeon; 
             // append/slice smtpat hint
             assert (S.index holes index_of_x_in_holes == S.index holes_except_first_pigeon (index_of_x_in_holes-1))
-          end);
+          end 
+      in Classical.forall_intro all_but_first_pigeon_remain_in_reduced; 
       let i1, i2 = pigeonhole_eq (eq) (holes_except_first_pigeon)  
                                       (S.init #(items_of eq holes_except_first_pigeon)
                                               (S.length pigeons - 1) 

ulib/FStar.HyperStack.ST.fsti

@@ -409,7 +409,7 @@ val rfree (#a:Type) (#rel:preorder a) (r:mreference a rel{HS.is_mm r /\ HS.is_he
   :ST unit (requires (fun m0     -> r `is_live_for_rw_in` m0))
            (ensures (fun m0 _ m1 -> m0 `contains` r /\ m1 == HS.free r m0))
 
-unfold let assign_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) (m0:mem) (_:unit) (m1:mem) : GTot prop =
+unfold let assign_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) (m0:mem) (_:unit) (m1:mem) =
   m0 `contains` r /\ m1 == HyperStack.upd m0 r v
 
 (**
@@ -420,7 +420,7 @@ val op_Colon_Equals (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a)
   :STL unit (requires (fun m -> r `is_live_for_rw_in` m /\ rel (HS.sel m r) v))
             (ensures  (assign_post r v))
 
-unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem) (x:a) (m1:mem) : GTot prop =
+unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem) (x:a) (m1:mem) =
   m1 == m0 /\ m0 `contains` r /\ x == HyperStack.sel m0 r
 
 (**

ulib/FStar.IndefiniteDescription.fst

@@ -64,4 +64,4 @@ let stronger_markovs_principle (p: (nat -> GTot bool))
     boolean predicate *)
 let stronger_markovs_principle_prop (p: (nat -> GTot prop))
     : Ghost nat (requires (~(forall (n: nat). ~(p n)))) (ensures (fun n -> p n)) =
-    indefinite_description_ghost _ (fun x -> p x)
+    indefinite_description_ghost _ p

ulib/FStar.Modifies.fst

@@ -237,7 +237,7 @@ let loc_includes_region_union_l = MG.loc_includes_region_union_l
 
 let loc_includes_addresses_addresses = MG.loc_includes_addresses_addresses #_ cls
 
-let loc_disjoint s1 s2 = MG.loc_disjoint s1 s2
+let loc_disjoint = MG.loc_disjoint
 
 let loc_disjoint_sym = MG.loc_disjoint_sym
 

ulib/FStar.Modifies.fsti

@@ -238,7 +238,7 @@ val loc_includes_addresses_addresses
 
 val loc_disjoint
   (s1 s2: loc)
-: Type0
+: GTot Type0
 
 val loc_disjoint_sym
   (s1 s2: loc)

ulib/FStar.ModifiesGen.fst

@@ -1184,7 +1184,6 @@ let loc_includes_loc_regions_restrict_to_regions
   (loc_includes (loc_regions false rs) (restrict_to_regions l rs))
 = Classical.forall_intro (loc_aux_includes_refl #al #c)
 
-#push-options "--z3rlimit_factor 2"
 let modifies_only_live_regions #al #c rs l h h' =
   let s = l in
   let c_rs = Set.complement rs in
@@ -1206,7 +1205,6 @@ let modifies_only_live_regions #al #c rs l h h' =
   modifies_only_live_regions_weak rs s_c_rs h h';
   loc_includes_restrict_to_regions s c_rs;
   modifies_loc_includes s h h' s_c_rs
-#pop-options
 
 let no_upd_fresh_region #al #c r l h0 h1 =
   modifies_only_live_regions (HS.mod_set (Set.singleton r)) l h0 h1

ulib/FStar.Monotonic.Seq.fst

@@ -277,7 +277,7 @@ let map_prefix_stable (#a:Type) (#b:Type) (#i:rid) (r:m_rref i (seq a) grows) (f
 let map_has_at_index (#a:Type) (#b:Type) (#i:rid)
 		     (r:m_rref i (seq a) grows)
 		     (f:a -> Tot b)
-		     (n:nat) (v:b) : HST.mem_predicate = fun h ->
+		     (n:nat) (v:b) (h:mem) =
     let s = HS.sel h r in
     n < Seq.length s
   /\ Seq.index (map f s) n == v
@@ -347,7 +347,7 @@ let collect_prefix_stable (#a:Type) (#b:Type) (#i:rid) (r:m_rref i (seq a) grows
 let collect_has_at_index (#a:Type) (#b:Type) (#i:rid)
 			 (r:m_rref i (seq a) grows)
 			 (f:a -> Tot (seq b))
-			 (n:nat) (v:b) : HST.mem_predicate = fun (h:mem) ->
+			 (n:nat) (v:b) (h:mem) =
     let s = HS.sel h r in
     n < Seq.length (collect f s)
   /\ Seq.index (collect f s) n == v

ulib/FStar.ReflexiveTransitiveClosure.fst

@@ -182,4 +182,4 @@ let induct
       (x:a) (y:a) (xy:squash (closure r x y))
 : squash (p x y)
 = let xy = FStar.Squash.join_squash #(_closure r x y) xy in
-  FStar.Squash.bind_squash xy (fun xy -> induct_ r p f_refl f_step f_closure x y xy)
+  FStar.Squash.bind_squash xy (induct_ r p f_refl f_step f_closure x y)

ulib/FStar.SquashProperties.fst

@@ -108,7 +108,7 @@ let l1 (a:Type) (b:Type) =
 		   let f0 (x:pow a) (y:b) : GTot bool = false in
 		   let g0 (x:pow b) (y:a) : GTot bool = false in
 		   map_squash nr (fun (f:(retract (pow a) (pow b) -> GTot False)) -> 
-				  MkC (fun x y -> f0 x y) (fun x y -> g0 x y) (fun r x -> false_elim (f r))))
+				  MkC f0 g0 (fun r x -> false_elim (f r))))
 
 (* The paradoxical set *)
 type u = p:Type -> Tot (squash (pow p))

ulib/FStar.Tactics.BreakVC.fst

@@ -22,7 +22,7 @@ let aux (ps:proofstate) (p : __result unit -> Type0)
     spinoff (squash (p (Success () ps)));
     <==> { spinoff_equiv (squash (p (Success () ps))) }
     squash (p (Success () ps));
-    ==>> { squash_p_impl_p _ }
+    ==>> { squash_p_impl_p fun _ -> p (Success () ps) }
     p (Success () ps);
     ==> { () }
     tac_return_wp () ps p;

ulib/FStar.Tactics.Effect.fsti

@@ -25,11 +25,11 @@ open FStar.Stubs.Tactics.Result
  * will break. (`synth_by_tactic` is fine) *)
 
 type tac_wp_t0 (a:Type) =
-  proofstate -> (__result a -> Type0) -> Type0
+  proofstate -> (__result a -> GTot Type0) -> GTot Type0
 
 unfold
 let tac_wp_monotonic (#a:Type) (wp:tac_wp_t0 a) =
-  forall (ps:proofstate) (p q:__result a -> Type0).
+  forall (ps:proofstate) (p q:__result a -> GTot Type0).
     (forall x. p x ==> q x) ==> (wp ps p ==> wp ps q)
 
 type tac_wp_t (a:Type) = wp:tac_wp_t0 a{tac_wp_monotonic wp}

ulib/LowStar.Literal.fsti

@@ -90,7 +90,7 @@ unfold let buffer_of_literal_post (s: ascii_string) (h0: HS.mem) (b: IB.ibuffer
 val buffer_of_literal: (s: ascii_string) ->
   ST.Stack (IB.ibuffer UInt8.t)
     (requires (fun _ -> String.length s < pow2 32))
-    (ensures fun h0 b h1 -> buffer_of_literal_post s h0 b h1)
+    (ensures buffer_of_literal_post s)
 
 /// .. note::
 ///

ulib/LowStar.Monotonic.Buffer.fst

@@ -1047,7 +1047,7 @@ let loc_includes_union_l_regions
   [SMTPat (loc_includes (loc_union s1 s2) (loc_regions prf r))]
 = loc_includes_union_l s1 s2 (loc_regions prf r)
 
-let loc_disjoint s1 s2 = MG.loc_disjoint s1 s2
+let loc_disjoint = MG.loc_disjoint
 
 let loc_disjoint_sym = MG.loc_disjoint_sym
 

ulib/LowStar.Monotonic.Buffer.fsti

@@ -853,7 +853,7 @@ val loc_includes_union_l_regions
 
 val loc_disjoint
   (s1 s2: loc)
-: Type0
+: GTot Type0
 
 val loc_disjoint_sym
   (s1 s2: loc)

ulib/LowStar.PrefixFreezableBuffer.fsti

@@ -139,13 +139,13 @@ unfold let alloc_post_mem_common
 val gcmalloc (r:HS.rid) (len:u32)
   : ST (b:lbuffer len{frameOf b == r /\ recallable b})
        (requires fun _ -> malloc_pre r len)
-       (ensures fun h0 b h1 -> alloc_post_mem_common h0 b h1)
+       (ensures  alloc_post_mem_common)
 
 val malloc (r:HS.rid) (len:u32)
   : ST
     (b:lbuffer len{frameOf b == r /\ freeable b})
     (requires fun _ -> malloc_pre r len)
-    (ensures fun h0 b h1 -> alloc_post_mem_common h0 b h1)
+    (ensures  alloc_post_mem_common)
 
 unfold let alloca_pre (len:U32.t) =  //precondition for stack allocated prefix freezable buffers
   UInt.size (U32.v len + 4) 32 /\ alloca_pre len

ulib/Prims.fst

@@ -312,7 +312,7 @@ let pure_pre = Type0
     [pre] is also valid. This provides a way for postcondition formula
     to be typed in a context where they can assume the validity of the
     precondition. This is discussed extensively in Issue #57 *)
-let pure_post' (a pre: Type) = _: a{pre} -> pure_pre
+let pure_post' (a pre: Type) = _: a{pre} -> GTot Type0
 let pure_post (a: Type) = pure_post' a True
 
 (** A pure weakest precondition transforms postconditions on [a]-typed
@@ -322,7 +322,7 @@ let pure_post (a: Type) = pure_post' a True
     property over the postconditions
     To enforce it, we first define a vanilla wp type,
     and then refine it with the monotonicity condition *)
-let pure_wp' (a: Type) = pure_post a -> pure_pre
+let pure_wp' (a: Type) = pure_post a -> GTot pure_pre
 
 (** The monotonicity predicate is marked opaque_to_smt,
     meaning that its definition is hidden from the SMT solver,

ulib/legacy/FStar.Array.fsti

@@ -52,7 +52,7 @@ val op_At_Bar (#a:Type0) (s1:array a) (s2:array a)
                               modifies Set.empty h0 h1))
 
 unfold let create_post (#a:Type0) (s:seq a)
-: heap -> st_post' (array a) True
+: heap -> array a -> heap -> Type0
 = fun h0 x h1 ->
   x `unused_in` h0 /\
   contains h1 x /\

ulib/legacy/FStar.Pointer.Base.fst

@@ -3812,12 +3812,12 @@ let modifies_buffer_elim' #t1 b p h h' =
     assert (n > 0);
     let pre
       (i: UInt32.t)
-    : Tot Type0
+    : GTot Type0
     = UInt32.v i < n
     in
     let post
       (i: UInt32.t)
-    : Tot Type0
+    : GTot Type0
     = pre i /\ (
 	  let q = gpointer_of_buffer_cell b i in
 	  equal_values h q h' q