Merge pull request #488 from FStarLang/nik_univs

Fixes in anticipation of F* universes in SMT encoding

Author: gebner

lib/core/PulseCore.BaseHeapSig.fst

@@ -89,10 +89,9 @@ let emp_unit (p:slprop) : Lemma (p == (p `star` emp)) =
     star_equiv p emp h
   );
   slprop_extensionality p (p `star` emp)
-
-let pure_true_emp () : Lemma (pure True == emp) =
-  introduce forall h. interp (pure True) h <==> interp emp h with H2.intro_emp h;
-  slprop_extensionality (pure True) emp
+let pure_true_emp () : Lemma (pure u#a True == emp) =
+  introduce forall h. interp (pure u#a True) h <==> interp emp h with H2.intro_emp h;
+  slprop_extensionality (pure u#a True) emp
 let intro_emp (h:mem) : Lemma (interp emp h) = H2.intro_emp h
 let pure_interp (p:prop) (c:mem) : Lemma (interp (pure p) c == p) =
   H2.pure_interp p c; PropositionalExtensionality.apply (interp (pure p) c) p

lib/core/PulseCore.Heap2.fst

@@ -161,9 +161,9 @@ let lift_star (l:tag) (p q:H.slprop)
   );
   slprop_extensionality (llift l (p `H.star` q)) (llift l p `star` llift l q)
 #pop-options
-let lift_emp : squash (lift H.emp == emp) = 
-  FStar.Classical.forall_intro H.intro_emp;
-  slprop_extensionality (lift H.emp) emp
+let lift_emp : squash (lift H.emp == emp u#a) = 
+  FStar.Classical.forall_intro (H.intro_emp u#a);
+  slprop_extensionality (lift u#a H.emp) (emp u#a)
 
 let pts_to_compatible #a #pcm (x:ref a pcm) (v0 v1:a) h = 
   H.pts_to_compatible #a #pcm x v0 v1 h.concrete;
@@ -571,9 +571,9 @@ let lift_action_ghost
 let ni_erased a : non_informative (erased a) = fun x -> reveal x
 let ni_unit : non_informative unit = fun x -> reveal x
 
-let lift_ghost_emp : squash (llift GHOST H.emp == emp) = 
-  FStar.Classical.forall_intro H.intro_emp;
-  slprop_extensionality (llift GHOST H.emp) emp
+let lift_ghost_emp : squash (llift GHOST H.emp == emp u#a) = 
+  FStar.Classical.forall_intro (H.intro_emp u#a);
+  slprop_extensionality (llift GHOST H.emp) (emp u#a)
 
 let core_ghost_ref_as_addr i = H.core_ref_as_addr i
 let core_ghost_ref_is_null c = H.core_ref_is_null c

lib/core/PulseCore.MemoryAlt.fst

@@ -60,8 +60,10 @@ let emp_unit (p:slprop)
 : Lemma (p `equiv` (p `star` emp))
 = B.emp_unit p
 
+#push-options "--print_implicits --print_universes"
+
 let pure_equiv (p q:prop)
-: Lemma ((p <==> q) ==> (pure p `equiv` pure q))
+: Lemma ((p <==> q) ==> (pure u#a p `equiv` pure u#a q))
 = FStar.PropositionalExtensionality.apply p q
 
 let pure_true_emp (_:unit)

lib/pulse/lib/Pulse.Lib.HashTable.fst

@@ -505,6 +505,7 @@ fn insert_if_not_full
   }
 }
 
+#restart-solver
 #push-options "--z3rlimit_factor 6"
 fn delete
   (#[@@@ Rust_generics_bounds ["Copy"; "PartialEq"; "Clone"]] kt:eqtype)

mk/checker.mk

@@ -9,6 +9,8 @@ ROOTS += lib/common/Pulse.Lib.Tactics.fsti
 
 FSTAR_OPTIONS += --already_cached 'Prims,FStar'
 FSTAR_OPTIONS += --include lib/common
+FSTAR_OPTIONS += --smtencoding.elim_box true
+FSTAR_OPTIONS += --z3smtopt '(set-option :smt.arith.nl false)'
 EXTRACT += --extract '-*,+Pulse,+PulseSyntaxExtension'
 DEPFLAGS += --already_cached 'Prims,FStar,FStarC'
 

src/checker/Pulse.Checker.AssertWithBinders.fst

@@ -410,6 +410,7 @@ let rec add_rem_uvs (g:env) (t:typ) (uvs:env { Env.disjoint g uvs }) (v:slprop)
     let v = tm_pureapp v qopt (tm_var {nm_index = x; nm_ppname = ppname}) in
     add_rem_uvs g (comp_res ct) uvs v
 
+#push-options "--fuel 0 --ifuel 0"
 let check
   (g:env)
   (pre:term)
@@ -424,7 +425,7 @@ let check
   let g = push_context g "check_assert" st.range in
 
   let Tm_ProofHintWithBinders { hint_type; binders=bs; t=body } = st.term in
-
+  allow_invert hint_type;
   match hint_type with
   | WILD ->
     let st = check_wild g pre st in
@@ -543,3 +544,4 @@ let check
         { t with effect_tag = st.effect_tag }
     in
     check g pre pre_typing post_hint res_ppname st
+#pop-options

src/checker/Pulse.Checker.Base.fst

@@ -176,6 +176,7 @@ let post_hint_from_comp_typing #g #c ct =
   in
   p
 
+#push-options "--z3rlimit_factor 4"
 let comp_typing_from_post_hint
     (#g: env)
     (c: comp_st)
@@ -297,7 +298,7 @@ let comp_with_pre (c:comp_st) (pre:term) =
   | C_STGhost i st -> C_STGhost i { st with pre }
   | C_STAtomic i obs st -> C_STAtomic i obs {st with pre}
 
-
+#push-options "--fuel 0 --ifuel 0"
 let st_equiv_pre (#g:env) (#t:st_term) (#c:comp_st) (d:st_typing g t c)
                  (pre:term)
                  (veq: slprop_equiv g (comp_pre c) pre)
@@ -312,8 +313,6 @@ let st_equiv_pre (#g:env) (#t:st_term) (#c:comp_st) (d:st_typing g t c)
       in
       t_equiv d st_equiv
 
-
-#push-options "--z3rlimit_factor 4 --ifuel 2 --fuel 0"
 let k_elab_equiv_continuation (#g1:env) (#g2:env { g2 `env_extends` g1 }) (#ctxt #ctxt1 #ctxt2:term)
   (k:continuation_elaborator g1 ctxt g2 ctxt1)
   (d:slprop_equiv g2 ctxt1 ctxt2)
@@ -324,15 +323,13 @@ let k_elab_equiv_continuation (#g1:env) (#g2:env { g2 `env_extends` g1 }) (#ctxt
     assert (comp_pre c == ctxt2);
     let st_d' : st_typing g2 st (comp_with_pre c ctxt1) = st_equiv_pre st_d _ (VE_Sym _ _ _ d) in
     k post_hint (| st, _, st_d' |)
-#pop-options
 
 let slprop_equiv_typing_fwd (#g:env) (#ctxt:_) (ctxt_typing:tot_typing g ctxt tm_slprop)
                            (#p:_) (d:slprop_equiv g ctxt p)
   : tot_typing g p tm_slprop 
   = let fwd, _ = slprop_equiv_typing d in
     fwd ctxt_typing
 
-#push-options "--z3rlimit_factor 4 --ifuel 1 --fuel 0"
 let k_elab_equiv_prefix
   (#g1:env) (#g2:env { g2 `env_extends` g1 }) (#ctxt1 #ctxt2 #ctxt:term)
   (k:continuation_elaborator g1 ctxt1 g2 ctxt)
@@ -347,7 +344,6 @@ let k_elab_equiv_prefix
   let (| st, c, st_d |) = res in
   assert (comp_pre c == ctxt1);
   (| _, _, st_equiv_pre st_d _ d |)
- #pop-options
 
 let k_elab_equiv
   (#g1:env) (#g2:env { g2 `env_extends` g1 }) (#ctxt1 #ctxt1' #ctxt2 #ctxt2':term)                 
@@ -362,7 +358,7 @@ let k_elab_equiv
     k_elab_equiv_prefix k d1 in
   k
 
-#push-options "--fuel 3 --ifuel 2 --split_queries no --z3rlimit_factor 20"
+#push-options "--fuel 3 --ifuel 1 --split_queries no --z3rlimit_factor 20"
 open Pulse.PP
 let continuation_elaborator_with_bind' (#g:env) (ctxt:term)
   (#c1:comp{stateful_comp c1})
@@ -571,6 +567,7 @@ let emp_inames_included (g:env) (i:term) (_:tot_typing g i tm_inames)
 : prop_validity g (tm_inames_subset tm_emp_inames i)
 = RU.magic()
 
+#push-options "--ifuel 1"
 let return_in_ctxt (g:env) (y:var) (y_ppname:ppname) (u:universe) (ty:term) (ctxt:slprop)
   (ty_typing:universe_of g ty u)
   (post_hint0:post_hint_opt g { PostHint? post_hint0 /\ checker_res_matches_post_hint g post_hint0 y ty ctxt})
@@ -614,8 +611,9 @@ let return_in_ctxt (g:env) (y:var) (y_ppname:ppname) (u:universe) (ty:term) (ctx
   | _ -> 
     (| _, _, d |)
 
-#push-options "--z3rlimit_factor 2"
+#push-options "--z3rlimit_factor 4 --ifuel 1 --split_queries always"
 #restart-solver
+#show-options
 let match_comp_res_with_post_hint (#g:env) (#t:st_term) (#c:comp_st)
   (d:st_typing g t c)
   (post_hint:post_hint_opt g)
@@ -651,6 +649,7 @@ let match_comp_res_with_post_hint (#g:env) (#t:st_term) (#c:comp_st)
 
            (| t, c', Pulse.Typing.Combinators.t_equiv d d_stequiv |)
 #pop-options
+#pop-options
 
 let apply_checker_result_k (#g:env) (#ctxt:slprop) (#post_hint:post_hint_for_env g)
   (r:checker_result_t g ctxt (PostHint post_hint))
@@ -667,7 +666,7 @@ let apply_checker_result_k (#g:env) (#ctxt:slprop) (#post_hint:post_hint_for_env
 
   k (PostHint post_hint) d
 
-#push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 1"
+#push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 0"
 //TODO: refactor and merge with continuation_elaborator_with_bind
 let checker_result_for_st_typing (#g:env) (#ctxt:slprop) (#post_hint:post_hint_opt g)
   (d:st_typing_in_ctxt g ctxt post_hint)
@@ -723,6 +722,7 @@ let readback_comp_res_as_comp (c:T.comp) : option comp =
   )
   | _ -> None
 
+#push-options "--ifuel 1"
 let rec is_stateful_arrow (g:env) (c:option comp) (args:list T.argv) (out:list T.argv)
   : T.Tac (option (list T.argv & T.argv))
   = let open R in
@@ -779,6 +779,7 @@ let rec is_stateful_arrow (g:env) (c:option comp) (args:list T.argv) (out:list T
         )
         else None
     )
+#pop-options
 
 let checker_result_t_equiv_ctxt (g:env) (ctxt ctxt' : slprop)
   (post_hint:post_hint_opt g)
@@ -796,14 +797,17 @@ let is_stateful_application (g:env) (e:term)
 : T.Tac (option st_term) = 
   RU.record_stats "Pulse.is_stateful_application" fun _ -> 
   let head, args = T.collect_app_ln e in
-  if Nil? args then None else
-  match RU.tc_term_phase1 (elab_env g) head false with
-  | None, _ -> None
-  | Some (_, ht, _), _ -> 
-    let head_t = wr ht (T.range_of_term ht) in
-    match is_stateful_arrow g (Some (C_Tot head_t)) args [] with 
-    | None -> None
-    | Some _ -> Some (as_stateful_application e head args)
+  match args with
+  | _ :: _ -> (
+    match RU.tc_term_phase1 (elab_env g) head false with
+    | None, _ -> None
+    | Some (_, ht, _), _ -> 
+      let head_t = wr ht (T.range_of_term ht) in
+      match is_stateful_arrow g (Some (C_Tot head_t)) args [] with 
+      | None -> None
+      | Some _ -> Some (as_stateful_application e head args)
+  )
+  | _ -> None
 
 let apply_conversion
       (#g:env) (#e:term) (#eff:_) (#t0:term)
@@ -888,6 +892,7 @@ let norm_st_typing_inverse
 
 open FStar.List.Tot    
 module RT = FStar.Reflection.Typing
+#push-options "--ifuel 1"
 let decompose_app (g:env) (tt:either term st_term)
 : T.Tac (option (term & list T.argv & (args:list T.argv{ Cons? args } -> T.Tac (res:either term st_term { Inr? tt ==> Inr? res }))))
 = let decompose_st_app (t:st_term)
@@ -919,6 +924,7 @@ let decompose_app (g:env) (tt:either term st_term)
       Some (head, args, rebuild)
   )
   | Inr st -> decompose_st_app st
+#pop-options
 
 let anf_binder name = T.pack (T.Tv_FVar (T.pack_fv (Pulse.Reflection.Util.mk_pulse_lib_core_lid (Printf.sprintf "__%s_binder__" name))))
 
@@ -958,11 +964,14 @@ let rec maybe_hoist (g:env) (arg:T.argv)
   )
   | Some _ -> (
     let g, binders, args = maybe_hoist_args g args in
-    if Nil? args then T.fail "Impossible";
-    let st_app = as_stateful_application t head args  in
-    let g, b, x, t = bind_st_term g st_app in
-    let arg = t, q in
-    g, binders@[b, x, st_app], arg
+    if Cons? args 
+    then (
+      let st_app = as_stateful_application t head args  in
+      let g, b, x, t = bind_st_term g st_app in
+      let arg = t, q in
+      g, binders@[b, x, st_app], arg
+    )
+    else T.fail "Impossible: is_stateful_application returned true but no args to hoist"
   )
 
 and maybe_hoist_args (g:env) (args:list T.argv)
@@ -975,6 +984,7 @@ and maybe_hoist_args (g:env) (args:list T.argv)
     args
     (g, [], [])
 
+#push-options "--ifuel 1"
 let maybe_hoist_top 
   (hoist_top_level:bool)
   (g:env)

src/checker/Pulse.Checker.Bind.fst

@@ -31,7 +31,7 @@ module Metatheory = Pulse.Typing.Metatheory
 module Abs = Pulse.Checker.Abs
 module RU = Pulse.Reflection.Util
 
-#push-options "--z3rlimit_factor 4 --split_queries no"
+#push-options "--z3rlimit_factor 8 --split_queries no --query_stats --fuel 0 --ifuel 1"
 let check_bind_fn
   (g:env)
   (ctxt:slprop)
@@ -62,7 +62,6 @@ let check_bind_fn
     checker_result_for_st_typing d res_ppname
   )
   | _ -> fail g (Some t.range) "check_bind_fn: head is not an abstraction"
-#pop-options
 
 let check_if_seq_lhs
   (g:env) (ctxt : slprop) (post_hint : post_hint_opt g)
@@ -226,4 +225,5 @@ let check_tot_bind
       Printf.sprintf "Elaborated and proceeding back to top-level\n%s\nto\n%s\n" 
       (show t)
       (show t'));
-    check g pre pre_typing post_hint res_ppname t'
+    check g pre pre_typing post_hint res_ppname t'
+#pop-options

src/checker/Pulse.Checker.If.fst

@@ -43,7 +43,7 @@ let retype_checker_result (#g:env) (#ctxt:slprop) (#ph:post_hint_opt g) (ph':pos
 = let (| x, g1, t, ctxt, k |) = r in
   (| x, g1, t, ctxt, k |)
 
-#push-options "--fuel 0 --ifuel 1 --z3rlimit_factor 2"
+#push-options "--fuel 0 --ifuel 0 --z3rlimit_factor 2"
 #restart-solver
 let check
   (g:env)

src/checker/Pulse.Checker.Match.fst

@@ -139,6 +139,8 @@ let lemma_map_opt_dec_index (top:'z) (f : (x:'a{x << top}) -> option 'b) (xs : l
           (ensures forall i. f (xs `L.index` i) == Some (ys `L.index` i))
   = Classical.forall_intro (Classical.move_requires (__lemma_map_opt_dec_index top f xs ys))
 
+#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 2 --query_stats"
+#restart-solver
 let rec elab_readback_pat_x (rp : R.pattern) (p : pattern)
   : Lemma (requires readback_pat rp == Some p)
           (ensures elab_pat p == rp)
@@ -195,6 +197,7 @@ and elab_readback_subpat (pb : R.pattern & bool)
           (ensures elab_sub_pat (Some?.v (readback_sub_pat pb)) == pb)
   = let (p, b) = pb in
     elab_readback_pat_x p (Some?.v (readback_pat p))
+#pop-options
 
 val tot_typing_weakening_n
    (#g:env) (#t:term) (#ty:term)
@@ -236,8 +239,8 @@ let rec bindings_to_string (bs : list binding) : T.Tac string =
   | b::bs ->
     (string_of_int (fst b) ^ ":" ^ Pulse.Syntax.Printer.term_to_string (snd b) ^ " ") ^ bindings_to_string bs
 
-#push-options "--z3rlimit 20"
-
+#push-options "--z3rlimit 40 --fuel 0 --ifuel 1"
+#restart-solver
 let check_branch
         (norw:bool)
         (g:env)
@@ -437,7 +440,7 @@ let rec least_tag (#g #pre #post_hint #sc_u #sc_ty #sc:_)
     | C_STAtomic i _ _ -> STT_Atomic
 
 
-#push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 1"
+#push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 0"
 #restart-solver
 let weaken_branch_tag_to 
       (#g #pre #post_hint #sc_u #sc_ty #sc:_) 
@@ -448,6 +451,7 @@ let weaken_branch_tag_to
   if ctag_of_comp_st c = ct then br
   else
     let r = pe.e.range in
+    allow_invert ct; allow_invert c;
     match ct, c with
     | STT_Ghost, C_STAtomic _ _ _
     | STT_Ghost, C_ST _ -> T.fail "Unexpected least effect"
@@ -464,6 +468,7 @@ let weaken_branch_tag_to
       let d = TBRV g sc_u sc_ty sc _ p e bs pf1 pf2 pf3 h d in
       (| pe, _, d |)
     )
+    
 
 
 let weaken_branch_tags
@@ -473,7 +478,9 @@ let weaken_branch_tags
 = let ct = least_tag checked_brs in
   let brs = T.map (weaken_branch_tag_to ct) checked_brs in
   (| ct, brs |)
+#pop-options
 
+#push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 1"
 let maybe_weaken_branch_tags
       (#g #pre #post_hint #sc_u #sc_ty #sc:_) 
       (checked_brs : list (check_branches_aux_t #g pre post_hint sc_u sc_ty sc))
@@ -531,7 +538,7 @@ let check_branches
   let brs = List.Tot.map dfst checked_brs in
   let d : brs_typing g sc_u sc_ty sc brs c0 = check_branches_aux2 g sc_u sc_ty sc c0 checked_brs in
   (| brs, c0, d |)
-
+#push-options "--fuel 0 --ifuel 1 --z3rlimit_factor 4 --query_stats"
 let check
         (g:env)
         (pre:term)
@@ -598,3 +605,4 @@ let check
   let c_typing = comp_typing_from_post_hint c pre_typing post_hint in
   let d = T_Match g sc_u sc_ty sc sc_ty_typing sc_typing c (E c_typing) brs brs_d complete_d in
   checker_result_for_st_typing (| _, _, d |) res_ppname
+#pop-options