Carrying universes through to the SMT encoding

Makefile

@@ -398,6 +398,10 @@ test-1: override FSTAR_EXE := $(abspath stage1/out/bin/fstar.exe)
 test-1: stage1
 	$(MAKE) _test FSTAR_EXE=$(FSTAR_EXE)
 
+_unit-tests-1: override FSTAR_EXE := $(abspath stage1/out/bin/fstar.exe)
+_unit-tests-1: stage1
+	$(MAKE) _unit-tests FSTAR_EXE=$(FSTAR_EXE)
+
 test-2: override FSTAR_EXE := $(abspath stage2/out/bin/fstar.exe)
 test-2: stage2
 	$(MAKE) _test FSTAR_EXE=$(FSTAR_EXE)

examples/algorithms/BinarySearch.fst

@@ -106,13 +106,15 @@ let hint1 y a = ()
 val hint2 : t:(seq int) -> a:int -> mid:int
   -> Lemma
        (requires
-          (forall i1 i2. (0 <= i1) ==> (i1 <= i2) ==> (i2 < length t) ==> (index t i1 <= index t i2)) /\
+          (forall i1 i2.
+            {:pattern index t i1; index t i2}
+             (0 <= i1) ==> (i1 <= i2) ==> (i2 < length t) ==> (index t i1 <= index t i2)) /\
           (0 <= mid) /\
           (mid < length t) /\
           (index t mid < a))
        (ensures
           (forall p. (((0 <= p) /\ (p < length t) /\ (index t p = a) /\ (p <= mid)) ==> False)))
-let hint2 t a mid = hint1 (index t mid) a
+let hint2 t a mid = ()
 
 val hint3 : y:int -> a:int -> Lemma
   (requires True)
@@ -122,7 +124,9 @@ let hint3 y a = ()
 val hint4 : t:(seq int) -> a:int -> mid:int
   -> Lemma
        (requires
-          (forall i1 i2. (0 <= i1) ==> (i1 <= i2) ==> (i2 < length t) ==> (index t i1 <= index t i2)) /\
+          (forall i1 i2. 
+              {:pattern index t i1; index t i2} 
+            (0 <= i1) ==> (i1 <= i2) ==> (i2 < length t) ==> (index t i1 <= index t i2)) /\
           (0 <= mid) /\
           (mid < length t) /\
           (a < index t mid))

examples/data_structures/BinaryTreesEnumeration.fsti

@@ -235,6 +235,7 @@ let memP_concatMap_intro #a #b (x: a) (y: b) (f:a -> list b) (l: list a) :
       can I get rid of them without cluttering the rest of the proof with many
       copies of the same function?  Can I infer them by unifying with the
       current “goal”? *)
+module T = FStar.Tactics
 let product_complete (#a #b: Type) (l1: list a) (l2: list b) x1 x2 :
   Lemma (List.memP x1 l1 ==>
          List.memP x2 l2 ==>
@@ -244,7 +245,7 @@ let product_complete (#a #b: Type) (l1: list a) (l2: list b) x1 x2 :
     let f1 = fun x1 -> List.Tot.map (f2 x1) l2 in
     let l = f1 x1 in
     let ls = List.Tot.map f1 l1 in
-    assert (product l1 l2 == List.Tot.concatMap f1 l1);
+    assert (product l1 l2 == List.Tot.concatMap f1 l1) by (T.trefl());
 
     memP_map_intro (f2 x1) x2 l2
       <: Lemma (List.memP x2 l2 ==> List.memP x l);

examples/data_structures/LowStar.Lens.Buffer.fsti

@@ -189,11 +189,11 @@ val mk (#a:_) (#p:_) (#q:_) (b:B.mbuffer a p q) (f:flavor b) (snap:HS.mem{B.live
   : Tot (l:buffer_lens b f{(lens_of l).snapshot == snap})
 
 /// `elim_inv`: Revealing the abstract invariant of buffer lenses
-val elim_inv (#a:_) (#p:_) (#q:_) 
+val elim_inv (#a:Type) (#p:_) (#q:_) 
              (#b:B.mbuffer a p q)
              (#f:flavor b)
              (bl:buffer_lens b f)
-  : Lemma (reveal_inv();
+  : Lemma (reveal_inv u#0 u#0 ();
           (forall (h:HS.mem).{:pattern (lens_of bl).invariant (lens_of bl).x h}
            let l = lens_of bl in
            (exists h'.{:pattern mk b f h'} B.live h' b /\ bl == mk b f h') /\

examples/data_structures/LowStar.Lens.Tuple2.fst

@@ -295,7 +295,7 @@ let elim_tup2_inv
        (bl1:LB.buffer_lens b1 f1)
        (bl2:LB.buffer_lens b2 f2{composable (LB.lens_of bl1) (LB.lens_of bl2)})
    : Lemma (let t = mk_tup2 bl1 bl2 in
-            reveal_inv();
+            reveal_inv u#0 u#0 ();
             (forall h. {:pattern inv (lens_of t) h}
               inv (lens_of t) h ==>
               (LB.lens_of bl1).invariant b1 h /\

examples/data_structures/LowStar.Lens.fsti

@@ -226,7 +226,7 @@ effect LensST (a:Type)
 
 /// `reveal_inv`: Revealing the abstract invariant
 val reveal_inv (_:unit)
-  : Lemma ((forall #a #b (l:hs_lens a b) h. {:pattern inv l h}
+  : Lemma ((forall (#a:Type u#a) (#b:Type u#b) (l:hs_lens a b) h. {:pattern inv l h}
             inv l h <==>
             (l.invariant l.x h /\
              B.modifies (as_loc l.footprint) l.snapshot h /\

examples/data_structures/RBTreeIntrinsic.fst

@@ -383,6 +383,7 @@ val balanceLB_preserves_sort : #h:nat -> #c:color -> a:almostNode h -> x:int ->
   (requires almostNode_sorted a /\ sorted b /\ chain (almostNode_max a) x (min b))
   (ensures  hiddenTree_sorted (balanceLB a x b))
 let balanceLB_preserves_sort #h #c left z d = ()
+#restart-solver
 
 val balanceRB_preserves_sort : #h:nat -> #c:color -> a:rbnode h c -> x:int -> b:almostNode h ->
   Lemma 

examples/doublylinkedlist/DoublyLinkedList.fst

@@ -1221,7 +1221,7 @@ let lemma_dll_links_contained (#t:Type) (h0:heap) (d:dll t) (i:nat) :
     lemma_unsnoc_is_last nl
 
 #set-options "--z3rlimit 10 --initial_ifuel 2"
-
+#restart-solver
 let lemma_dll_links_disjoint (#t:Type) (h0:heap) (d:dll t) (i:nat) :
   Lemma
     (requires (
@@ -1964,8 +1964,8 @@ let dll_append (#t:Type) (d1 d2:dll t) :
 
 #reset-options
 
-#set-options "--z3rlimit 60 --max_fuel 2 --max_ifuel 1"
-
+#set-options "--z3rlimit 200 --max_fuel 2 --max_ifuel 1 --query_stats --split_queries no --z3smtopt '(set-option :smt.qi.eager_threshold 5)'"
+#restart-solver
 let dll_split_using (#t:Type) (d:dll t) (e:pointer (node t)) :
   StackInline (dll t * dll t)
     (requires (fun h0 ->

examples/doublylinkedlist/DoublyLinkedListIface.fst

@@ -605,7 +605,7 @@ let dll_insert_at_tail #t d n =
 #reset-options
 
 #set-options "--z3rlimit 80 --max_fuel 2 --max_ifuel 1"
-
+#push-options "--z3rlimit_factor 4"
 let dll_insert_before #t n' d n =
   let h00 = HST.get () in
   HST.push_frame ();
@@ -694,7 +694,7 @@ let dll_insert_before #t n' d n =
   // assert (as_payload_list h11 d == l_insert_before'
   //           (as_list h00 d `L.index_of` n') (as_payload_list h00 d) (g_node_val h00 n));
   ()
-
+#pop-options
 #reset-options
 
 #set-options "--z3rlimit 80 --max_fuel 2 --max_ifuel 1"

examples/dsls/DSL.fst.config.json

@@ -1,7 +1,8 @@
 {
 	"fstar_exe": "fstar.exe",
 	"options": [
-		"--z3version", "4.13.3"
+		"--z3version", "4.13.3",
+		"--ext", "context_pruning"
 	],
 	"include_dirs": [
 		"bool_refinement",

examples/dsls/bool_refinement/BoolRefinement.fst

@@ -4,8 +4,7 @@ module R = FStar.Reflection.V2
 module L = FStar.List.Tot
 open FStar.List.Tot
 
-#set-options "--z3cliopt 'smt.qi.eager_threshold=100' --z3cliopt 'smt.arith.nl=false'"
-
+#set-options "--z3smtopt '(set-option :smt.qi.eager_threshold 20)' --z3smtopt '(set-option :smt.arith.nl false)'"
 let var = nat
 let index = nat
 
@@ -126,6 +125,7 @@ let rec close_exp' (e:src_exp) (v:var) (n:nat)
 
 let open_exp e v = open_exp' e v 0
 let close_exp e v = close_exp' e v 0
+#restart-solver
 
 let rec open_close' (e:src_exp) (x:var) (n:nat { ln' e (n - 1) })
   : Lemma (open_exp' (close_exp' e x n) x n == e)
@@ -607,6 +607,7 @@ let rec extend_env_l_lookup_bvar (g:R.env) (sg:src_env) (x:var)
 
 //key lemma about src types: Their elaborations are closed
 #push-options "--z3rlimit_factor 4 --fuel 8 --ifuel 2"
+#restart-solver
 let rec src_refinements_are_closed_core
                        (n:nat)
                        (e:src_exp {ln' e (n - 1) && closed e}) 
@@ -1146,7 +1147,8 @@ let rec src_typing_freevars #f (sg:src_env) (e:src_exp) (t:s_ty) (d:src_typing f
       src_typing_freevars _ _ _ dbody
 #pop-options
 
-#push-options "--z3rlimit_factor 4"
+#push-options "--z3rlimit_factor 8 --query_stats --split_queries no --fuel 2 --ifuel 2"
+#restart-solver
 let rec src_typing_renaming (#f:RT.fstar_top_env)
                             (sg sg':src_env)
                             (x:var { None? (lookup sg x) && None? (lookup sg' x) })
@@ -1259,6 +1261,7 @@ let rec src_typing_renaming (#f:RT.fstar_top_env)
       in
       let dt = src_ty_ok_renaming _ _ _ _ _ _ dt in
       T_If _ _ _ _ _ _ _ _ db dt1 dt2 st1 st2 dt
+#pop-options
 
 let sub_typing_weakening #f (sg sg':src_env) 
                          (x:var { None? (lookup sg x) && None? (lookup sg' x) })
@@ -1323,6 +1326,8 @@ let sub_typing_weakening #f (sg sg':src_env)
 
       | _ -> admit ())
 
+#push-options "--z3rlimit_factor 8 --query_stats --split_queries no --fuel 2 --ifuel 2"
+#restart-solver
 let rec src_typing_weakening #f (sg sg':src_env) 
                              (x:var { None? (lookup sg x) && None? (lookup sg' x) })
                              (b:binding)
@@ -1518,6 +1523,8 @@ let freevars_refinement (e:R.term) (bv0:_)
   = ()
 #pop-options
 
+#push-options "--z3rlimit_factor 8 --query_stats --split_queries no --fuel 2 --ifuel 2"
+#restart-solver
 let rec soundness (#f:RT.fstar_top_env)
                   (#sg:src_env { src_env_ok sg } ) 
                   (#se:src_exp { ln se })
@@ -1673,7 +1680,9 @@ and src_ty_ok_soundness (#f:RT.fstar_top_env)
      in
      freevars_refinement (elab_exp e) bv0;
      RT.T_Refine (extend_env_l f sg) x RT.bool_ty refinement' _ _ _ _ bool_typing dr
+#pop-options
 
+#restart-solver
 let soundness_lemma (f:RT.fstar_top_env)
                     (sg:src_env { src_env_ok sg }) 
                     (se:src_exp { ln se })

examples/layeredeffects/DM4F.fst

@@ -78,13 +78,13 @@ effect {
 }
 
 unfold
-let lift_wp (#a:Type) (#st:Type0) (w:pure_wp a) : wp st a =
-  elim_pure_wp_monotonicity_forall ();
+let lift_wp (#a:Type u#a) (#st:Type0) (w:pure_wp a) : wp st a =
+  elim_pure_wp_monotonicity_forall u#a ();
   fun s0 p -> w (fun x -> p (x, s0))
 
-let lift_pure_st a wp st (f : unit -> PURE a wp)
+let lift_pure_st (a:Type u#a) wp st (f : unit -> PURE a wp)
   : repr a st (lift_wp wp)
-  = elim_pure_wp_monotonicity_forall ();
+  = elim_pure_wp_monotonicity_forall u#a ();
     fun s0 -> (f (), s0)
 
 sub_effect PURE ~> ST = lift_pure_st

examples/layeredeffects/DM4F_layered.fst

@@ -128,12 +128,12 @@ let lift_pure_st_wp #a #st (w : pure_wp a) : wp st a =
   r
 
 let lift_id_st_wp #a #st (w : pure_wp a) : wp st a =
-  elim_pure_wp_monotonicity_forall ();
+  elim_pure_wp_monotonicity w;
   fun s0 p -> w (fun x -> p x s0)
 
 let lift_id_st a wp st (f : ID2.repr a wp)
   : repr a st (lift_id_st_wp wp)
-  = elim_pure_wp_monotonicity_forall ();
+  = elim_pure_wp_monotonicity wp;
     fun s0 -> (f (), s0)
 
 sub_effect ID ~> ST = lift_id_st

examples/layeredeffects/DM4F_layered5.fst

@@ -106,7 +106,7 @@ effect {
 }
 
 let lift_id_st_wp #a #st (w : ID5.wp a) : wp st a =
-  elim_pure_wp_monotonicity_forall ();
+  elim_pure_wp_monotonicity w;
   fun s0 p -> w (fun x -> p x s0)
 
 let lift_id_st a wp st (f : ID5.repr a wp)

examples/layeredeffects/GT.fst

@@ -20,22 +20,22 @@ let m (a:Type u#aa) (i:idx) : Type u#aa =
 let t_return #a (x:a) : m a T = (fun () -> x)
 let g_return #a (x:a) : m a G = (fun () -> x)
 let d_return #a (x:a) : m a D = raise_val (fun () -> x)
-
+#push-options "--print_universes --log_queries --query_stats"
+#restart-solver
 let return (a:Type) (x:a) (i:idx) : m a i =
-  match i with
+  match i returns m a i with
   | T -> t_return x
   | G -> g_return x
   | D -> d_return x
-
 let t_bind #a #b (c : m a T) (f : a -> m b T) : m b T = fun () -> f (c ()) ()
 let g_bind #a #b (c : m a G) (f : a -> m b G) : m b G = fun () -> f (c ()) ()
 let d_bind #a #b (c : m a D) (f : a -> m b D) : m b D =
   raise_val (fun () -> downgrade_val (f (downgrade_val c ())) ())
 
 let bind (a b : Type) (i:idx) (c : m a i) (f : a -> m b i) : m b i =
-  match i with
+  match i returns m b i with
   | T -> t_bind #a #b c f
-  | D -> coerce (d_bind #a #b c f) // GM: wow... still needs a coerce, how can that be?
+  | D -> d_bind #a #b (coerce c) f // GM: wow... still needs a coerce, how can that be?
   | G -> g_bind #a #b c f
 
 // Already somewhat usable
@@ -77,10 +77,10 @@ let lift_pure_gtd (a:Type) (wp : pure_wp a) (i : idx)
  //     case analyze [i].
  // GM: ok not anymore
  FStar.Monotonic.Pure.elim_pure_wp_monotonicity wp;
- match i with
+ match i returns m a i with
  | T -> f
  | G -> f
- | D -> coerce (raise_val (fun () -> f () <: Dv a))
+ | D -> raise_val (fun () -> f () <: Dv a)
 
 sub_effect PURE ~> GTD = lift_pure_gtd
 

examples/layeredeffects/GTWP.fst

@@ -17,8 +17,9 @@ let coerce #a #b (x:a{a == b}) : b = x
 let wp (a:Type) = pure_wp a
 
 unfold
-let bind_wp #a #b (wc : wp a) (wf : a -> wp b) : wp b =
-  elim_pure_wp_monotonicity_forall ();
+let bind_wp (#a:Type u#a) (#b:Type u#b) (wc : wp a) (wf : a -> wp b) : wp b =
+  elim_pure_wp_monotonicity_forall u#a ();
+  elim_pure_wp_monotonicity_forall u#b ();
   as_pure_wp (fun p -> wc (fun x -> wf x p))
 
 let m (a:Type u#aa) (i:idx) (w : wp a) : Type u#aa =
@@ -41,15 +42,24 @@ let return (a:Type) (x:a) (i:idx) : m a i (return_wp x) =
   | D -> coerce (d_return x)
 
 // these two rely on monotonicity since the computed WP is not exactly bind_wp
-let t_bind #a #b #wc #wf (c : m a T wc) (f : (x:a -> m b T (wf x))) : m b T (bind_wp wc wf) = elim_pure_wp_monotonicity_forall (); fun () -> f (c ()) ()
-let g_bind #a #b #wc #wf (c : m a G wc) (f : (x:a -> m b G (wf x))) : m b G (bind_wp wc wf) = elim_pure_wp_monotonicity_forall (); fun () -> f (c ()) ()
+let t_bind (#a:Type u#a) (#b:Type u#b) #wc #wf (c : m a T wc) (f : (x:a -> m b T (wf x)))
+: m b T (bind_wp wc wf)
+= elim_pure_wp_monotonicity_forall u#a ();
+  elim_pure_wp_monotonicity_forall u#b ();
+  fun () -> f (c ()) ()
+let g_bind (#a:Type u#a) (#b:Type u#b) #wc #wf (c : m a G wc) (f : (x:a -> m b G (wf x)))
+: m b G (bind_wp wc wf)
+= elim_pure_wp_monotonicity_forall u#a ();
+  elim_pure_wp_monotonicity_forall u#b ();
+  fun () -> f (c ()) ()
 
 let d_bind #a #b #wc #wf (c : m a D wc) (f : (x:a -> m b D (wf x))) : m b D (bind_wp wc wf) =
   raise_val (fun () -> let y = downgrade_val c () in // cannot inline this
                     downgrade_val (f y) ())
 
-let bind (a b : Type) (i:idx) (wc:wp a) (wf:a -> wp b) (c : m a i wc) (f : (x:a -> m b i (wf x))) : m b i (bind_wp wc wf) =
-  elim_pure_wp_monotonicity_forall ();
+let bind (a:Type u#a) (b : Type u#b) (i:idx) (wc:wp a) (wf:a -> wp b) (c : m a i wc) (f : (x:a -> m b i (wf x))) : m b i (bind_wp wc wf) =
+  elim_pure_wp_monotonicity_forall u#a ();
+  elim_pure_wp_monotonicity_forall u#b ();
   match i with
   | T -> t_bind #_ #_ #wc #wf c f
   | G -> g_bind #_ #_ #wc #wf c f
@@ -64,19 +74,26 @@ let subcomp (a:Type u#aa) (i:idx)
           (requires (forall p. wp2 p ==> wp1 p))
           (ensures (fun _ -> True))
    = match i with
-     | T -> f
-     | G -> f
+     | T ->
+       let f : m a T wp1 = coerce #(m a i wp1) #(m a T wp1) f in
+       let f : m a T wp2 = f in
+       coerce #(m a T wp2) #(m a i wp2) f
+     | G ->
+       let f : m a G wp1 = coerce #(m a i wp1) #(m a G wp1) f in
+       let f : m a G wp2 = f in
+       coerce #(m a G wp2) #(m a i wp2) f
      | D ->
        (* This case needs some handholding. *)
+       let f : m a D wp1 = coerce #(m a i wp1) #(m a D wp1) f in
        let f : raise_t (unit -> DIV a wp1) = f in
        let f : unit -> DIV a wp1 = downgrade_val f in
        let f : unit -> DIV a wp2 = f in
        assert_norm (m a i wp2 == raise_t (unit -> DIV a wp2));
        coerce (raise_val f)
 
 unfold
-let ite_wp #a (w1 w2 : wp a) (b:bool) : wp a =
-  elim_pure_wp_monotonicity_forall ();
+let ite_wp (#a:Type u#a) (w1 w2 : wp a) (b:bool) : wp a =
+  elim_pure_wp_monotonicity_forall u#a ();
   as_pure_wp (fun p -> if b then w1 p else w2 p)
 
 let if_then_else (a:Type) (i:idx) (w1 w2 : wp a)
@@ -99,18 +116,18 @@ effect {
   }
 }
 
-let lift_pure_gtd (a:Type) (w : wp a) (i : idx)
+let lift_pure_gtd (a:Type u#a) (w : wp a) (i : idx)
                   (f : unit -> PURE a w)
                  : Pure (m a i w)
                         (requires True)
                         (ensures (fun _ -> True))
- = elim_pure_wp_monotonicity_forall ();
+ = elim_pure_wp_monotonicity_forall u#a ();
    match i with
    | T -> f
    | G -> f
    | D -> let f' () : DIV a w = f () in
          let f'' : m a D w = raise_val f' in
-         f''
+         coerce f''
 
  // GM: Surprised that this works actually... I expected that I would need to
  //     case analyze [i].