Start fixing ulib.

ulib/FStar.All.fsti

@@ -28,7 +28,7 @@ unfold let lift_state_all (a : Type) (wp : st_wp a) (p : all_post a) = wp (fun a
 sub_effect STATE ~> ALL { lift_wp = lift_state_all }
 
 unfold
-let lift_exn_all (a : Type) (wp : ex_wp a) (p : all_post a) (h : heap) = wp (fun ra -> p ra h)
+let lift_exn_all (a : Type) (wp : ex_wp a) : all_wp_h heap a = fun (p : all_post a) (h : heap) -> wp (fun ra -> p ra h)
 sub_effect EXN ~> ALL { lift_wp = lift_exn_all }
 
 effect All (a:Type) (pre:all_pre) (post:(h:heap -> Tot (all_post' a (pre h)))) =

ulib/FStar.Classical.fst

@@ -40,11 +40,11 @@ let get_equality #t a b = get_squashed #(equals a b) (a == b)
 let impl_to_arrow #a #b impl sx =
   bind_squash #(a -> GTot b) impl (fun f -> bind_squash sx (fun x -> return_squash (f x)))
 
-let arrow_to_impl #a #b f = squash_double_arrow (return_squash (fun x -> f (return_squash x)))
+let arrow_to_impl #a #b f = squash_double_arrow (return_squash #(a -> GTot (squash b)) (fun x -> f (return_squash x)))
 
 let impl_intro_gtot #p #q f = return_squash f
 
-let impl_intro_tot #p #q f = return_squash #(p -> GTot q) f
+let impl_intro_tot #p #q f = return_squash #(p -> GTot q) fun x -> f x
 
 let impl_intro #p #q f =
   give_witness #(p ==> q) (squash_double_arrow (return_squash (lemma_to_squash_gtot f)))
@@ -92,13 +92,13 @@ let gtot_to_lemma #a #p f x = give_proof #(p x) (return_squash (f x))
 let forall_intro_squash_gtot #a #p f =
   bind_squash #(x: a -> GTot (p x))
     #(forall (x: a). p x)
-    (squash_double_arrow #a #p (return_squash f))
+    (squash_double_arrow #a #(fun x -> p x) (return_squash f))
     (fun f -> lemma_forall_intro_gtot #a #p f)
 
 let forall_intro_squash_gtot_join #a #p f =
   join_squash (bind_squash #(x: a -> GTot (p x))
         #(forall (x: a). p x)
-        (squash_double_arrow #a #p (return_squash f))
+        (squash_double_arrow #a #(fun x -> p x) (return_squash f))
         (fun f -> lemma_forall_intro_gtot #a #p f))
 
 let forall_intro #a #p f = give_witness (forall_intro_squash_gtot (lemma_to_squash_gtot #a #p f))
@@ -115,10 +115,10 @@ let forall_intro_2 #a #b #p f =
 let forall_intro_2_with_pat #a #b #c #p pat f = forall_intro_2 #a #b #p f
 
 let forall_intro_3 #a #b #c #p f =
-  let g: x: a -> Lemma (forall (y: b x) (z: c x y). p x y z) = fun x -> forall_intro_2 (f x) in
+  let g: x: a -> Lemma (forall (y: b x) (z: c x y). p x y z) = fun x -> forall_intro_2 #_ #_ #(fun y z -> p x y z) (f x) in
   forall_intro g
 
-let forall_intro_3_with_pat #a #b #c #d #p pat f = forall_intro_3 #a #b #c #p f
+let forall_intro_3_with_pat #a #b #c #d #p pat f = forall_intro_3 #a #b #c #(fun x y z -> p x y z) f
 
 let forall_intro_4 #a #b #c #d #p f =
   let g: x: a -> Lemma (forall (y: b x) (z: c x y) (w: d x y z). p x y z w) =
@@ -165,7 +165,7 @@ let exists_intro_not_all_not (#a:Type) (#p:a -> Type)
            (get_proof (forall x. ~ (p x)))
            (fun (g: (forall x. ~ (p x))) ->
              bind_squash #(x:a -> GTot (~(p x))) #Prims.empty g
-             (fun (h:(x:a -> GTot (~(p x)))) -> f h))
+             (fun (h:(x:a -> GTot (~(p x)))) -> f fun x -> h x))
     in
     ()
 #pop-options

ulib/FStar.Classical.fsti

@@ -321,7 +321,7 @@ val forall_intro_4
     TODO: Seems overly specific; could be removed?  *)
 val forall_impl_intro
       (#a: Type)
-      (#p #q: (a -> GTot Type))
+      (#p #q: (a -> Type))
       ($_: (x: a -> squash (p x) -> Lemma (q x)))
     : Lemma (forall x. p x ==> q x)
 
@@ -331,7 +331,7 @@ val forall_impl_intro
   *)
 val ghost_lemma
       (#a: Type)
-      (#p: (a -> GTot Type0))
+      (#p: (a -> Type0))
       (#q: (a -> unit -> GTot Type0))
       ($_: (x: a -> Lemma (requires p x) (ensures (q x ()))))
     : Lemma (forall (x: a). p x ==> q x ())

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 _ p
+    indefinite_description_ghost _ (fun x -> p x)

ulib/FStar.Pervasives.fsti

@@ -336,7 +336,7 @@ let reveal_opaque (s: string) = norm_spec [delta_only [s]; zeta]
     (with monotonicity refinement) *)
 
 unfold
-let pure_return (a:Type) (x:a) : pure_wp a =
+let pure_return (a:Type) (x:a) : GTot (pure_wp a) =
   reveal_opaque (`%pure_wp_monotonic) pure_wp_monotonic;
   pure_return0 a x
 
@@ -449,32 +449,35 @@ let st_wp_h (heap a: Type) = st_post_h heap a -> Tot (st_pre_h heap)
 
 (** Returning a value does not transform the state *)
 unfold
-let st_return (heap a: Type) (x: a) (p: st_post_h heap a) = p x
+let st_return (heap a: Type) (x: a) : GTot (st_wp_h heap a) = fun (p: st_post_h heap a) -> p x
 
 (** Sequential composition of stateful WPs *)
 unfold
 let st_bind_wp
       (heap: Type)
       (a b: Type)
       (wp1: st_wp_h heap a)
-      (wp2: (a -> GTot (st_wp_h heap b)))
+      (wp2: a -> st_wp_h heap b)
+    : st_wp_h heap b = fun
       (p: st_post_h heap b)
       (h0: heap)
-     = wp1 (fun a h1 -> wp2 a p h1) h0
+    -> wp1 (fun a h1 -> wp2 a p h1) h0
 
 (** Branching for stateful WPs *)
 unfold
 let st_if_then_else
       (heap a p: Type)
       (wp_then wp_else: st_wp_h heap a)
+    : st_wp_h heap a =
+    fun
       (post: st_post_h heap a)
       (h0: heap)
-     = wp_then post h0 /\ (~p ==> wp_else post h0)
+    -> wp_then post h0 /\ (~p ==> wp_else post h0)
 
 (** As with [PURE] the [wp] combinator names the postcondition as
     [k] to avoid duplicating it. *)
 unfold
-let st_ite_wp (heap a: Type) (wp: st_wp_h heap a) (post: st_post_h heap a) (h0: heap) =
+let st_ite_wp (heap a: Type) (wp: st_wp_h heap a) : st_wp_h heap a = fun (post: st_post_h heap a) (h0: heap) ->
   forall (k: st_post_h heap a).
     (forall (x: a) (h: heap). {:pattern (guard_free (k x h))} post x h ==> k x h) ==> wp k h0
 
@@ -485,12 +488,12 @@ let st_stronger (heap a: Type) (wp1 wp2: st_wp_h heap a) =
 
 (** Closing the scope of a binder within a stateful WP *)
 unfold
-let st_close_wp (heap a b: Type) (wp: (b -> GTot (st_wp_h heap a))) (p: st_post_h heap a) (h: heap) =
+let st_close_wp (heap a b: Type) (wp: b -> st_wp_h heap a) : st_wp_h heap a = fun (p: st_post_h heap a) (h: heap) ->
   (forall (b: b). wp b p h)
 
 (** Applying a stateful WP to a trivial postcondition *)
 unfold
-let st_trivial (heap a: Type) (wp: st_wp_h heap a) = (forall h0. wp (fun r h1 -> True) h0)
+let st_trivial (heap a: Type) (wp: st_wp_h heap a) : GTot prop = (forall h0. wp (fun r h1 -> True) h0)
 
 (** Introducing a new effect template [STATE_h] *)
 new_effect {
@@ -540,8 +543,7 @@ let ex_return (a: Type) (x: a) (p: ex_post a) : GTot Type0 = p (V x)
 (** Sequential composition of exception-raising code requires case analysing
     the result of the first computation before "running" the second one *)
 unfold
-let ex_bind_wp (a b: Type) (wp1: ex_wp a) (wp2: (a -> GTot (ex_wp b))) (p: ex_post b)
-    : GTot Type0 =
+let ex_bind_wp (a b: Type) (wp1: ex_wp a) (wp2: (a -> (ex_wp b))) : ex_wp b = fun p ->
   forall (k: ex_post b).
     (forall (rb: result b). {:pattern (guard_free (k rb))} p rb ==> k rb) ==>
     (wp1 (function
@@ -552,12 +554,12 @@ let ex_bind_wp (a b: Type) (wp1: ex_wp a) (wp2: (a -> GTot (ex_wp b))) (p: ex_po
 (** As for other effects, branching in [ex_wp] appears in two forms.
     First, a simple case analysis on [p] *)
 unfold
-let ex_if_then_else (a p: Type) (wp_then wp_else: ex_wp a) (post: ex_post a) =
+let ex_if_then_else (a p: Type) (wp_then wp_else: ex_wp a) : ex_wp a = fun (post: ex_post a) ->
   wp_then post /\ (~p ==> wp_else post)
 
 (** Naming continuations for use with branching *)
 unfold
-let ex_ite_wp (a: Type) (wp: ex_wp a) (post: ex_post a) =
+let ex_ite_wp (a: Type) (wp: ex_wp a) : ex_wp a = fun (post: ex_post a) ->
   forall (k: ex_post a).
     (forall (rb: result a). {:pattern (guard_free (k rb))} post rb ==> k rb) ==> wp k
 
@@ -567,11 +569,11 @@ let ex_stronger (a: Type) (wp1 wp2: ex_wp a) = (forall (p: ex_post a). wp1 p ==>
 
 (** Closing the scope of a binder for exceptional WPs *)
 unfold
-let ex_close_wp (a b: Type) (wp: (b -> GTot (ex_wp a))) (p: ex_post a) = (forall (b: b). wp b p)
+let ex_close_wp (a b: Type) (wp: b -> ex_wp a) : ex_wp a = fun (p: ex_post a) -> (forall (b: b). wp b p)
 
 (** Applying a computation with a trivial postcondition *)
 unfold
-let ex_trivial (a: Type) (wp: ex_wp a) = wp (fun r -> True)
+let ex_trivial (a: Type) (wp: ex_wp a) : GTot ex_pre = wp (fun r -> True)
 
 (** Introduce a new effect for [EXN] *)
 new_effect {
@@ -595,7 +597,7 @@ effect Exn (a: Type) (pre: ex_pre) (post: ex_post' a pre) =
     NOTE: BE WARNED, CODE IN THE [EXN] EFFECT IS ONLY CHECKED FOR
     PARTIAL CORRECTNESS *)
 unfold
-let lift_div_exn (a: Type) (wp: pure_wp a) (p: ex_post a) = wp (fun a -> p (V a))
+let lift_div_exn (a: Type) (wp: pure_wp a) : ex_wp a = fun (p: ex_post a) -> wp (fun a -> p (V a))
 sub_effect DIV ~> EXN { lift_wp = lift_div_exn }
 
 (** A variant of [Exn] with trivial pre- and postconditions *)
@@ -631,7 +633,7 @@ let all_wp_h (h a: Type) = all_post_h h a -> Tot (all_pre_h h)
 (** Returning a value [x] normally promotes it to the [V x] result
     without touching the [heap] *)
 unfold
-let all_return (heap a: Type) (x: a) (p: all_post_h heap a) = p (V x)
+let all_return (heap a: Type) (x: a) : GTot (all_wp_h heap a) = fun (p: all_post_h heap a) -> p (V x)
 
 (** Sequential composition for [ALL_h] is like [EXN]: case analysis of
     the exceptional result before "running" the continuation *)
@@ -640,10 +642,9 @@ let all_bind_wp
       (heap: Type)
       (a b: Type)
       (wp1: all_wp_h heap a)
-      (wp2: (a -> GTot (all_wp_h heap b)))
-      (p: all_post_h heap b)
-      (h0: heap)
-    : GTot Type0 =
+      (wp2: a -> all_wp_h heap b)
+    : all_wp_h heap b =
+  fun (p: all_post_h heap b) (h0: heap) ->
   wp1 (fun ra h1 ->
         (match ra with
           | V v -> wp2 v p h1
@@ -656,13 +657,13 @@ unfold
 let all_if_then_else
       (heap a p: Type)
       (wp_then wp_else: all_wp_h heap a)
-      (post: all_post_h heap a)
-      (h0: heap)
-     = wp_then post h0 /\ (~p ==> wp_else post h0)
+    : all_wp_h heap a
+    = fun (post: all_post_h heap a) (h0: heap)
+    -> wp_then post h0 /\ (~p ==> wp_else post h0)
 
 (** Naming postcondition for better sharing in [ALL_h] *)
 unfold
-let all_ite_wp (heap a: Type) (wp: all_wp_h heap a) (post: all_post_h heap a) (h0: heap) =
+let all_ite_wp (heap a: Type) (wp: all_wp_h heap a) : all_wp_h heap a = fun (post: all_post_h heap a) (h0: heap) ->
   forall (k: all_post_h heap a).
     (forall (x: result a) (h: heap). {:pattern (guard_free (k x h))} post x h ==> k x h) ==> wp k h0
 
@@ -675,14 +676,14 @@ let all_stronger (heap a: Type) (wp1 wp2: all_wp_h heap a) =
 unfold
 let all_close_wp
       (heap a b: Type)
-      (wp: (b -> GTot (all_wp_h heap a)))
-      (p: all_post_h heap a)
-      (h: heap)
-     = (forall (b: b). wp b p h)
+      (wp: b -> all_wp_h heap a)
+    : all_wp_h heap a
+    = fun (p: all_post_h heap a) (h: heap)
+    -> (forall (b: b). wp b p h)
 
 (** Applying an [ALL_h] wp to a trivial postcondition *)
 unfold
-let all_trivial (heap a: Type) (wp: all_wp_h heap a) = (forall (h0: heap). wp (fun r h1 -> True) h0)
+let all_trivial (heap a: Type) (wp: all_wp_h heap a) : GTot prop = (forall (h0: heap). wp (fun r h1 -> True) h0)
 
 (** Introducing the [ALL_h] effect template *)
 new_effect {

ulib/FStar.ST.fst

@@ -30,7 +30,7 @@ let gst_post' (a:Type) (pre:Type) = st_post_h' heap a pre
 let gst_post  (a:Type) = st_post_h heap a
 let gst_wp (a:Type)   = st_wp_h heap a
 
-unfold let lift_div_gst (a:Type) (wp:pure_wp a) (p:gst_post a) (h:heap) = wp (fun a -> p a h)
+unfold let lift_div_gst (a:Type) (wp:pure_wp a) : st_wp_h heap a = fun (p:gst_post a) (h:heap) -> wp (fun a -> p a h)
 sub_effect DIV ~> GST = lift_div_gst
 
 let heap_rel (h1:heap) (h2:heap) =

ulib/FStar.Squash.fst

@@ -35,15 +35,15 @@ let give_proof (#p:Type) _ = ()
 let proof_irrelevance (p:Type) x y = ()
 
 let squash_double_arrow #a #p f =
-    bind_squash f push_squash
+    bind_squash f fun g -> push_squash fun x -> g x
 
-let push_sum (#a:Type) (#b:(a -> Type)) ($p : dtuple2 a (fun (x:a) -> squash (b x))) =
+let push_sum (#a:Type) (#b:(a -> GTot Type)) ($p : dtuple2 a (fun (x:a) -> squash (b x))) =
     match p with
     | Mkdtuple2 x y ->
         bind_squash #(b x) #(dtuple2 a b) y (fun y' ->
         return_squash (Mkdtuple2 x y'))
 
-let squash_double_sum (#a:Type) (#b:(a -> Type)) (p : squash (dtuple2 a (fun (x:a) -> squash (b x)))) =
+let squash_double_sum (#a:Type) (#b:(a -> GTot Type)) (p : squash (dtuple2 a (fun (x:a) -> squash (b x)))) =
     bind_squash p (fun p' -> push_sum p') // Need eta...
 
 let map_squash (#a:Type) (#b:Type) s f =

ulib/FStar.Squash.fsti

@@ -76,13 +76,13 @@ val squash_double_arrow (#a: Type) (#p: (a -> Type)) ($f: (squash (x: a -> GTot
     : GTot (squash (x: a -> GTot (p x)))
 
 (** The analog of [push_squash] for sums (existential quantification *)
-val push_sum (#a: Type) (#b: (a -> Type)) ($p: (dtuple2 a (fun (x: a) -> squash (b x))))
+val push_sum (#a: Type) (#b: (a -> GTot Type)) ($p: (dtuple2 a (fun (x: a) -> squash (b x))))
     : Tot (squash (dtuple2 a b))
 
 (** The analog of [squash_double_arrow] for sums (existential quantification) *)
 val squash_double_sum
       (#a: Type)
-      (#b: (a -> Type))
+      (#b: (a -> GTot Type))
       ($p: (squash (dtuple2 a (fun (x: a) -> squash (b x)))))
     : Tot (squash (dtuple2 a b))
 

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}
@@ -58,7 +58,7 @@ let tac_bind_wp (#a #b:Type) (wp_f:tac_wp_t a) (wp_g:a -> tac_wp_t b) : tac_wp_t
 unfold
 let tac_wp_compact (a:Type) (wp:tac_wp_t a) : tac_wp_t a =
   fun ps post ->
-  forall (k:__result a -> Type0). (forall (r:__result a).{:pattern (guard_free (k r))} post r ==> k r) ==> wp ps k
+  forall (k:__result a -> GTot Type0). (forall (r:__result a).{:pattern (guard_free (k r))} post r ==> k r) ==> wp ps k
 
 
 /// tac_bind_interleave_begin is an ugly hack to get interface interleaving

ulib/FStar.Tactics.V1.Logic.Lemmas.fst

@@ -16,18 +16,18 @@
 module FStar.Tactics.V1.Logic.Lemmas
 
 let fa_intro_lem (#a:Type) (#p:a -> Type) (f:(x:a -> squash (p x))) : Lemma (forall (x:a). p x) =
-  FStar.Classical.lemma_forall_intro_gtot
+  FStar.Classical.lemma_forall_intro_gtot #_ #(fun x -> p x)
     ((fun x -> FStar.IndefiniteDescription.elim_squash (f x)) <: (x:a -> GTot (p x)))
 
 let split_lem #a #b sa sb = ()
 
 let imp_intro_lem #a #b f =
-  FStar.Classical.give_witness (FStar.Classical.arrow_to_impl (fun (x:squash a) -> FStar.Squash.bind_squash x f))
+  FStar.Classical.give_witness (FStar.Classical.arrow_to_impl (fun (x:squash a) -> FStar.Squash.bind_squash x (fun y -> f y)))
 
 let __lemma_to_squash #req #ens (_ : squash req) (h : (unit -> Lemma (requires req) (ensures ens))) : squash ens =
   h ()
 
-let vbind #p #q sq f = FStar.Classical.give_witness_from_squash (FStar.Squash.bind_squash sq f)
+let vbind #p #q sq f = FStar.Classical.give_witness_from_squash (FStar.Squash.bind_squash sq (fun y -> f y))
 
 let or_ind #p #q #phi o l r = ()
 

ulib/Prims.fst

@@ -351,7 +351,7 @@ type guard_free : Type0 -> Type0
     Clients should not use it directly,
     instead use FStar.Pervasives.pure_return *)
 unfold
-let pure_return0 (a: Type) (x: a) : pure_wp a =
+let pure_return0 (a: Type) : a -> GTot (pure_wp a) = fun x ->
   fun (p: pure_post a) ->
   forall (return_val: a). return_val == x ==> p return_val
 
@@ -363,7 +363,7 @@ unfold
 let pure_bind_wp0
       (a b: Type)
       (wp1: pure_wp a)
-      (wp2: (a -> GTot (pure_wp b)))
+      (wp2: (a -> pure_wp b))
       : pure_wp b
      = fun (p: pure_post b) ->
        wp1 (fun (bind_result_1: a) -> wp2 bind_result_1 p)
@@ -410,11 +410,11 @@ let pure_stronger (a: Type) (wp1 wp2: pure_wp a) = forall (p: pure_post a). wp1
     Clients should not use it directly,
     instead use FStar.Pervasives.pure_close_wp *)
 unfold
-let pure_close_wp0 (a b: Type) (wp: (b -> GTot (pure_wp a))) : pure_wp a = fun (p: pure_post a) -> forall (b: b). wp b p
+let pure_close_wp0 (a b: Type) (wp: (b -> (pure_wp a))) : pure_wp a = fun (p: pure_post a) -> forall (b: b). wp b p
 
 (** Trivial WP for PURE: Prove the WP with the trivial postcondition *)
 unfold
-let pure_trivial (a: Type) (wp: pure_wp a) = wp (fun (trivial_result: a) -> True)
+let pure_trivial (a: Type) : pure_wp a -> GTot Type = fun wp -> wp (fun (trivial_result: a) -> True)
 
 (** Introduces the PURE effect.
     The definition of the PURE effect is fixed.