Misc changes

lib/pulse/lib/Pulse.Lib.Array.Core.fsti

@@ -69,7 +69,7 @@ val op_Array_Access
             pure (res == Seq.index s (SZ.v i)))
 
 
-(* Written x.(i) <- v *)
+(* Written a.(i) <- v *)
 val op_Array_Assignment
         (#t: Type)
         (a: array t)

share/pulse/Makefile.include-base

@@ -72,7 +72,6 @@ include $(FSTAR_DEP_FILE)
 
 $(ALL_CHECKED_FILES): %.checked:
 	$(call msg, "CHECK", $(basename $(notdir $@)))
-	@# You can debug with --debug $(basename $(notdir $<))
 	$(Q)$(RUNLIM) $(FSTAR) $(SIL) $(COMPAT_INDEXED_EFFECTS) $<
 	touch -c $@
 

share/pulse/examples/c/PulsePointStruct.fst

@@ -60,7 +60,7 @@ let _ = define_struct0 _point "PulsePointStruct.point" point_fields
 inline_for_extraction noextract
 let point = struct0 _point "PulsePointStruct.point" point_fields
 
-#push-options "--query_stats  --fuel 0"
+#push-options "--fuel 0"
 
 ```pulse
 fn swap_struct (p: ref point) (v: Ghost.erased (typeof point))

share/pulse/examples/dice/dpe/DPE.Messages.Parse.fst

@@ -146,7 +146,7 @@ type dpe_cmd = {
   dpe_cmd_args: cbor;
 }
 
-#push-options "--z3rlimit 64 --query_stats" // to let z3 cope with CDDL specs
+#push-options "--z3rlimit 64" // to let z3 cope with CDDL specs
 #restart-solver
 
 noextract [@@noextract_to "krml"]

src/checker/Pulse.Checker.Base.fst

@@ -365,7 +365,7 @@ let k_elab_equiv
     k_elab_equiv_prefix k d1 in
   k
 
-#push-options "--query_stats --fuel 3 --ifuel 2 --split_queries no --z3rlimit_factor 20"
+#push-options "--fuel 3 --ifuel 2 --split_queries no --z3rlimit_factor 20"
 open Pulse.PP
 let continuation_elaborator_with_bind (#g:env) (ctxt:term)
   (#c1:comp{stateful_comp c1})
@@ -646,7 +646,7 @@ let apply_checker_result_k (#g:env) (#ctxt:vprop) (#post_hint:post_hint_for_env
 
   k (Some post_hint) d
 
-#push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 1 --query_stats"
+#push-options "--z3rlimit_factor 4 --fuel 0 --ifuel 1"
 let checker_result_for_st_typing (#g:env) (#ctxt:vprop) (#post_hint:post_hint_opt g)
   (d:st_typing_in_ctxt g ctxt post_hint)
   (ppname:ppname)

src/checker/Pulse.Checker.Bind.fst

@@ -30,7 +30,7 @@ module PS = Pulse.Checker.Prover.Substs
 module Abs = Pulse.Checker.Abs
 
 
-#push-options "--query_stats --z3rlimit_factor 4 --split_queries no"
+#push-options "--z3rlimit_factor 4 --split_queries no"
 let check_bind_fn
   (g:env)
   (ctxt:vprop)

src/checker/Pulse.Checker.Prover.Substs.fst

@@ -66,6 +66,28 @@ type ss_t = {
   m : m:ss_map { is_dom l m }
 }
 
+let rec separate_map (sep:document)
+   (f : 'a -> T.Tac document)
+   (xs : list 'a)
+   : T.Tac document =
+  match xs with
+  | [] -> empty
+  | [x] -> f x
+  | x::xs ->
+    let doc = f x in
+    let docs = separate_map sep f xs in
+    doc ^^ sep ^^ docs
+
+instance pp_ss_t : printable ss_t = {
+  pp = (function {l;m} ->
+        //  doc_of_string "dom="
+        //  pp (l <: list int) ^^
+        //  doc_of_string " |-> " ^^
+        l |> separate_map comma (fun k ->
+               pp (k <: int) ^^ doc_of_string " -> " ^^ pp (Map.sel m k))
+        );
+}
+
 let ln_ss_t (s:ss_t) =
   List.Tot.for_all (fun x -> ln (Map.sel s.m x)) s.l
 
@@ -82,6 +104,8 @@ let is_dom_push
 
   assert (Map.equal (remove_map (Map.upd m x t) x) m)
 
+let lemma_dom_empty () = ()
+
 let push (ss:ss_t) (x:var { ~ (contains ss x) }) (t:term) : ss_t =
 
   is_dom_push ss.l ss.m x t;

src/checker/Pulse.Checker.Prover.Substs.fsti

@@ -21,6 +21,7 @@ open FStar.List.Tot
 open Pulse.Syntax
 open Pulse.Typing.Env
 open Pulse.Typing
+open Pulse.PP
 
 module L = FStar.List.Tot
 module T = FStar.Tactics
@@ -30,6 +31,8 @@ module Env = Pulse.Typing.Env
 
 val ss_t : Type0
 
+instance val pp_ss_t : printable ss_t
+
 val ln_ss_t (s:ss_t) : bool
 val as_map (ss:ss_t) : Map.t var term
 
@@ -39,6 +42,9 @@ let sel (ss:ss_t) (x:var { contains ss x }) = Map.sel (as_map ss) x
 
 val empty : ss_t
 
+val lemma_dom_empty ()
+  : Lemma (dom empty == Set.empty)
+
 val push (ss:ss_t) (x:var { ~ (contains ss x) }) (t:term) : ss_t
 
 val push_ss (ss1:ss_t) (ss2:ss_t { Set.disjoint (dom ss1) (dom ss2) }) : ss_t

src/checker/Pulse.Checker.Pure.fst

@@ -162,18 +162,18 @@ let readback_failure (s:R.term) =
   Printf.sprintf "Internal error: failed to readback F* term %s"
                  (T.term_to_string s)
 
-let ill_typed_term (t:term) (expected_typ:option term) (got_typ:option term) : Tac (list FStar.Stubs.Pprint.document) =
+let ill_typed_term (t:term) (expected_typ:option term) (got_typ:option term) : Tac (list document) =
   let open Pulse.PP in
   match expected_typ, got_typ with
   | None, _ ->
     [text "Ill-typed term: " ^^ pp t]
   | Some ty, None ->
-    [group (text "Expected term of type" ^/^ pp ty) ^/^
-     group (text "got term" ^/^ pp t)]
+    [prefix 2 1 (text "Expected term of type") (pp ty) ^/^
+     prefix 2 1 (text "got term") (pp t)]
   | Some ty, Some ty' ->
-    [group (text "Expected term of type" ^/^ pp ty) ^/^
-     group (text "got term" ^/^ pp t) ^/^
-     group (text "of type" ^/^ pp ty')]
+    [prefix 2 1 (text "Expected term of type") (pp ty) ^/^
+     prefix 2 1 (text "got term") (pp t) ^/^
+     prefix 2 1 (text "of type") (pp ty')]
 
 let maybe_fail_doc (issues:list FStar.Issue.issue)
                    (g:env) (rng:range) (doc:list FStar.Stubs.Pprint.document) =

src/checker/Pulse.Elaborate.Pure.fst

@@ -96,7 +96,6 @@ let elab_stt_equiv (g:R.env) (c:comp{C_ST? c}) (pre:R.term) (post:R.term)
     (comp_u c)
     (comp_res c)
     _ _ _ _ _ (RT.Rel_refl _ _ _) eq_pre eq_post
-#push-options "--query_stats"
 let elab_statomic_equiv (g:R.env) (c:comp{C_STAtomic? c}) (pre:R.term) (post:R.term)
   (eq_pre:RT.equiv g pre (comp_pre c))
   (eq_post:RT.equiv g post

src/checker/Pulse.Elaborate.fst

@@ -24,7 +24,7 @@ open Pulse.Syntax
 open Pulse.Typing
 open Pulse.Elaborate.Core
 
-#push-options "--fuel 10 --ifuel 10 --z3rlimit_factor 30 --query_stats --z3cliopt 'smt.qi.eager_threshold=100'"          
+#push-options "--fuel 10 --ifuel 10 --z3rlimit_factor 30 --z3cliopt 'smt.qi.eager_threshold=100'"
 
 let elab_open_commute' (e:term)
                        (v:term)

src/checker/Pulse.Soundness.Bind.fst

@@ -39,7 +39,7 @@ let mequiv_arrow (g:R.env) (t1:R.term) (u2:R.universe) (t2:R.term) (pre:R.term)
   = admit()
 
 
-#push-options "--fuel 2 --ifuel 1 --query_stats"
+#push-options "--fuel 2 --ifuel 1"
 let inst_bind_t1 #u1 #u2 #g #head
                    (head_typing: RT.tot_typing g head (bind_type u1 u2))
                    (#t1:_)
@@ -189,7 +189,7 @@ let elab_bind_typing (g:stt_env)
     d
 #pop-options
 
-#push-options "--query_stats --z3rlimit_factor 4 --split_queries no"
+#push-options "--z3rlimit_factor 4 --split_queries no"
 assume
 val open_close_inverse_t (e:R.term { RT.ln e }) (x:var) (t:R.term)
   : Lemma (RT.open_with (RT.close_term e x) t == e)

src/checker/Pulse.Soundness.Comp.fst

@@ -55,7 +55,7 @@ let stc_soundness
   let post_typing  = mk_t_abs_tot g ppname_default dres dpost in
   res_typing, pre_typing, post_typing
 
-#push-options "--query_stats --fuel 2 --ifuel 2 --z3rlimit_factor 2"
+#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 2"
 let comp_typing_soundness (g:stt_env)
                           (c:comp)
                           (uc:universe)

src/checker/Pulse.Soundness.STEquiv.fst

@@ -94,7 +94,7 @@ let inst_sub_stt (#g:R.env) (#u:_) (#a #pre1 #pre2 #post1 #post2 #r:R.term)
 
 let vprop_arrow (t:term) : term = tm_arrow (null_binder t) None (C_Tot tm_vprop)
 
-#push-options "--fuel 2 --ifuel 1 --z3rlimit_factor 4 --query_stats"
+#push-options "--fuel 2 --ifuel 1 --z3rlimit_factor 4"
 let st_equiv_soundness_aux (g:stt_env)
                            (c0:ln_comp) (c1:ln_comp { comp_res c0 == comp_res c1 })
                            (d:st_equiv g c0 c1)

src/checker/Pulse.Soundness.fst

@@ -231,7 +231,7 @@ let stequiv_soundness
     STEquiv.st_equiv_soundness _ _ _ equiv _ r_e_typing
 
 
-#push-options "--query_stats --fuel 2 --ifuel 2 --z3rlimit_factor 30"
+#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 30"
 
 let bind_soundness
   (#g:stt_env)
@@ -316,7 +316,7 @@ let if_soundness
   RT.T_If _ _ _ _ _ _ _ _ _ rb_typing re1_typing re2_typing c_typing
 #pop-options
 
-#push-options "--query_stats --fuel 2 --ifuel 2"
+#push-options "--fuel 2 --ifuel 2"
 let rec soundness (g:stt_env)
                   (t:st_term)
                   (c:comp)

src/checker/Pulse.Typing.Combinators.fst

@@ -141,7 +141,7 @@ let rec vprop_equiv_typing (#g:_) (#t0 #t1:term) (v:vprop_equiv g t0 t1)
         let t0_typing = d1 t1_typing in
         construct_forall_typing #g #u #b #t0 x b_typing t0_typing)
 
-#push-options "--z3rlimit_factor 8 --ifuel 1 --fuel 2 --query_stats"
+#push-options "--z3rlimit_factor 8 --ifuel 1 --fuel 2"
 
 let bind_t (case_c1 case_c2:comp_st -> bool) =
       (g:env) ->
@@ -263,7 +263,6 @@ let mk_bind_ghost_ghost : bind_t C_STGhost? C_STGhost? =
     (| _, _, T_Bind _ e1 e2 _ _ b _ _ d_e1 d_c1res d_e2 bc |)
   end 
 
-#push-options "--query_stats"
 let mk_bind_atomic_atomic
   : bind_t C_STAtomic? C_STAtomic?
   = fun g pre e1 e2 c1 c2 px d_e1 d_c1res d_e2 res_typing post_typing post_hint ->
@@ -298,7 +297,6 @@ let mk_bind_atomic_atomic
       else (
         T.fail "Should have been handled separately"
       )
-#pop-options
 
 #push-options "--z3rlimit_factor 10 --fuel 0 --ifuel 1"
 let rec mk_bind (g:env) 

src/checker/Pulse.Typing.FV.fst

@@ -33,7 +33,7 @@ let freevars_close_term_host_term (t:term) (x:var) (i:index)
              (freevars (wr t FStar.Range.range_0) `set_minus` x)))
   = admit()
 
-#push-options "--query_stats --z3rlimit_factor 2"
+#push-options "--z3rlimit_factor 2"
 let freevars_close_term' (e:term) (x:var) (i:index)
   : Lemma 
     (ensures freevars (close_term' e x i) `Set.equal`
@@ -464,7 +464,7 @@ let freevars_array (t:term)
   = admit()
 
 // FIXME: tame this proof
-#push-options "--fuel 3 --ifuel 1 --z3rlimit_factor 15 --query_stats --retry 5 --split_queries no"
+#push-options "--fuel 3 --ifuel 1 --z3rlimit_factor 15 --retry 5 --split_queries no"
 let rec st_typing_freevars (#g:_) (#t:_) (#c:_)
                            (d:st_typing g t c)
 : Lemma 

src/checker/Pulse.Typing.LN.fst

@@ -793,7 +793,7 @@ let close_proof_hint_ln (ht:proof_hint_type) (v:var) (i:index)
     | WILD
     | SHOW_PROOF_STATE _ -> ()
 
-#push-options "--query_stats --fuel 2 --ifuel 2 --z3rlimit_factor 8 --split_queries no"
+#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 8 --split_queries no"
 let rec close_st_term_ln' (t:st_term) (x:var) (i:index)
   : Lemma
     (requires ln_st' t (i - 1))
@@ -1050,7 +1050,7 @@ let ln_mk_array (t:term) (n:int)
       (ensures ln' (mk_array t) n) =
   admit ()
 
-#push-options "--z3rlimit_factor 15 --fuel 4 --ifuel 1 --query_stats --split_queries no"
+#push-options "--z3rlimit_factor 15 --fuel 4 --ifuel 1 --split_queries no"
 let rec st_typing_ln (#g:_) (#t:_) (#c:_)
                      (d:st_typing g t c)
   : Lemma 

src/checker/Pulse.Typing.Printer.fst

@@ -20,7 +20,7 @@ open Pulse.Syntax.Printer
 open Pulse.Typing
 
 
-#push-options "--query_stats --ifuel 1 --z3rlimit_factor 4 --split_queries no"
+#push-options "--ifuel 1 --z3rlimit_factor 4 --split_queries no"
 let rec print_st_typing #g #t #c (d:st_typing g t c)
   : T.Tac string 
   = match d with