A separation logic prover for pulse

lib/steel/pulse/Pulse.Checker.Abs.fst

@@ -1,12 +1,12 @@
 module Pulse.Checker.Abs
 
 module T = FStar.Tactics.V2
-module RT = FStar.Reflection.Typing
 
 open Pulse.Syntax
 open Pulse.Typing
+open Pulse.Typing.Combinators
 open Pulse.Checker.Pure
-open Pulse.Checker.Common
+open Pulse.Checker.Base
 
 module P = Pulse.Syntax.Printer
 module FV = Pulse.Typing.FV
@@ -31,58 +31,71 @@ let check_effect_annotation g r (c_annot c_computed:comp) =
 
 
 #push-options "--z3rlimit_factor 2 --fuel 0 --ifuel 1"
-let check_abs
+let rec check_abs
   (g:env)
   (t:st_term{Tm_Abs? t.term})
-  (pre:term)
-  (pre_typing:tot_typing g pre tm_vprop)
-  (post_hint:post_hint_opt g)
   (check:check_t)
-  : T.Tac (checker_result_t g pre post_hint) =
-  if Some? post_hint then fail g None "Unexpected post-condition annotation from context for an abstraction" else 
+  : T.Tac (t:st_term & c:comp & st_typing g t c)=
+
   let range = t.range in
   match t.term with  
   | Tm_Abs { b = {binder_ty=t;binder_ppname=ppname}; q=qual; ascription=c; body } -> //pre=pre_hint; body; ret_ty; post=post_hint_body } ->
+
     (*  (fun (x:t) -> {pre_hint} body : t { post_hint } *)
     let (| t, _, _ |) = check_term g t in //elaborate it first
     let (| u, t_typing |) = check_universe g t in //then check that its universe ... We could collapse the two calls
     let x = fresh g in
     let px = ppname, x in
     let var = tm_var {nm_ppname=ppname;nm_index=x} in
     let g' = push_binding g x ppname t in
-    let pre_opened, ret_ty, post_hint_body = 
-      match c with
-      | C_Tot { t = Tm_Unknown } -> 
-        tm_emp, None, None
+    let body_opened = open_st_term_nv body px in
+    match body_opened.term with
+    | Tm_Abs _ ->
+      let (| body, c_body, body_typing |) = check_abs g' body_opened check in
+      check_effect_annotation g' body.range c c_body;
+      FV.st_typing_freevars body_typing;
+      let body_closed = close_st_term body x in
+      assume (open_st_term body_closed x == body);
+      let b = {binder_ty=t;binder_ppname=ppname} in
+      let tt = T_Abs g x qual b u body_closed c_body t_typing body_typing in
+      let tres = tm_arrow {binder_ty=t;binder_ppname=ppname} qual (close_comp c_body x) in
+      (| _, C_Tot tres, tt |)
+    | _ ->
+      let pre_opened, ret_ty, post_hint_body = 
+        match c with
+        | C_Tot _ ->
+          fail g (Some body.range)
+            "Unexpected error: found a total computation annotation on a top-level function" 
+
+        | _ -> 
+          open_term_nv (comp_pre c) px,
+          Some (open_term_nv (comp_res c) px),
+          Some (open_term' (comp_post c) var 1)
+      in
+      let (| pre_opened, pre_typing |) = check_vprop g' pre_opened in
+      let pre = close_term pre_opened x in
+      let post : post_hint_opt g' =
+        match post_hint_body with
+        | None -> fail g (Some body.range) "Top-level functions must be annotated with pre and post conditions"
+        | Some post ->
+          let post_hint_typing
+            : post_hint_t
+            = Pulse.Checker.Base.intro_post_hint (push_context "post_hint_typing" range g') (Some (ctag_of_comp_st c)) ret_ty post
+          in
+          Some post_hint_typing
+      in
+
+      let ppname = mk_ppname_no_range "_fret" in
+      let r  = check g' pre_opened pre_typing post ppname body_opened  in
+      let (| body, c_body, body_typing |) : st_typing_in_ctxt g' pre_opened post =
+        apply_checker_result_k #_ #_ #(Some?.v post) r ppname in
 
-      | C_Tot ty ->
-        tm_emp,
-        Some (open_term_nv ty px),
-        None
+      check_effect_annotation g' body.range c c_body;
 
-      | _ -> 
-        open_term_nv (comp_pre c) px,
-        Some (open_term_nv (comp_res c) px),
-        Some (open_term' (comp_post c) var 1)
-    in
-    let (| pre_opened, pre_typing |) = check_vprop g' pre_opened in
-    let pre = close_term pre_opened x in
-    let post =
-      match post_hint_body with
-      | None -> None
-      | Some post ->
-        let post_hint_typing
-          : post_hint_t
-          = Pulse.Checker.Common.intro_post_hint (push_context "post_hint_typing" range g') ret_ty post
-        in
-        Some post_hint_typing
-    in
-    let (| body', c_body, body_typing |) = check g' (open_st_term_nv body px) pre_opened pre_typing post in
-    check_effect_annotation g' body'.range c c_body;
-    FV.st_typing_freevars body_typing;
-    let body_closed = close_st_term body' x in
-    assume (open_st_term body_closed x == body');
-    let b = {binder_ty=t;binder_ppname=ppname} in
-    let tt = T_Abs g x qual b u body_closed c_body t_typing body_typing in
-    let tres = tm_arrow {binder_ty=t;binder_ppname=ppname} qual (close_comp c_body x) in
-    (| _, C_Tot tres, tt |)
+      FV.st_typing_freevars body_typing;
+      let body_closed = close_st_term body x in
+      assume (open_st_term body_closed x == body);
+      let b = {binder_ty=t;binder_ppname=ppname} in
+      let tt = T_Abs g x qual b u body_closed c_body t_typing body_typing in
+      let tres = tm_arrow {binder_ty=t;binder_ppname=ppname} qual (close_comp c_body x) in
+      (| _, C_Tot tres, tt |)

lib/steel/pulse/Pulse.Checker.Abs.fst.hints

@@ -1,5 +1,5 @@
 [
-  "ÌŽ—]Æê$žRm€ˆ\n™4",
+  "j›R\u0005¼–håÿ\u0004¶*Û“z",
   [
     [
       "Pulse.Checker.Abs.check_effect_annotation",
@@ -13,7 +13,7 @@
         "string_typing"
       ],
       0,
-      "99ab22c732cabb968a68fa9bb11ca57a"
+      "e3ed564cdb21aa89d1f311e001c5aa9a"
     ],
     [
       "Pulse.Checker.Abs.check_abs",
@@ -25,31 +25,30 @@
         "@fuel_correspondence_Pulse.Syntax.Naming.freevars_st.fuel_instrumented",
         "@query", "Prims_pretyping_ce036b6b736ef4e0bc3a9ff132a12aed",
         "Pulse.Syntax.Base_pretyping_fe09dc1e796799f4bac0760e63f30d40",
+        "Pulse.Typing_pretyping_85b09ae4ef91823fbf549acd09fde244",
         "bool_inversion",
         "constructor_distinct_FStar.Pervasives.Native.None",
         "constructor_distinct_FStar.Pervasives.Native.Some",
         "constructor_distinct_FStar.Tactics.Result.Failed",
         "constructor_distinct_FStar.Tactics.Result.Success",
-        "constructor_distinct_Pulse.Syntax.Base.C_Tot",
         "constructor_distinct_Pulse.Syntax.Base.Tm_Abs",
-        "constructor_distinct_Pulse.Syntax.Base.Tm_Unknown",
         "data_elim_FStar.Tactics.Result.Success",
         "data_elim_Pulse.Syntax.Base.Mkppname",
+        "data_elim_Pulse.Syntax.Base.Mkst_term",
         "disc_equation_FStar.Pervasives.Native.None",
-        "disc_equation_FStar.Pervasives.Native.Some",
         "disc_equation_Pulse.Syntax.Base.C_ST",
         "disc_equation_Pulse.Syntax.Base.C_STAtomic",
         "disc_equation_Pulse.Syntax.Base.C_STGhost",
         "disc_equation_Pulse.Syntax.Base.C_Tot",
         "disc_equation_Pulse.Syntax.Base.Tm_Abs",
-        "disc_equation_Pulse.Syntax.Base.Tm_Unknown",
-        "equality_tok_Pulse.Syntax.Base.Tm_Unknown@tok",
         "equation_FStar.Pervasives.Native.fst",
         "equation_FStar.Pervasives.Native.snd", "equation_FStar.Range.range",
-        "equation_FStar.Reflection.Typing.fstar_top_env",
         "equation_FStar.Reflection.Typing.pp_name_t",
-        "equation_FStar.Reflection.V2.Data.var", "equation_Prims.eqtype",
+        "equation_FStar.Reflection.V2.Data.var",
+        "equation_FStar.Sealed.Inhabited.sealed",
+        "equation_FStar.Sealed.Inhabited.sealed_", "equation_Prims.eqtype",
         "equation_Prims.nat", "equation_Pulse.Checker.Pure.push_context",
+        "equation_Pulse.Syntax.Base.comp_st",
         "equation_Pulse.Syntax.Base.index",
         "equation_Pulse.Syntax.Base.nvar",
         "equation_Pulse.Syntax.Base.ppname_default",
@@ -64,16 +63,14 @@
         "equation_Pulse.Typing.FV.set_minus",
         "equation_Pulse.Typing.post_hint_for_env",
         "equation_Pulse.Typing.post_hint_opt",
-        "fuel_guarded_inversion_FStar.Pervasives.Native.option",
         "fuel_guarded_inversion_FStar.Tactics.Result.__result",
         "fuel_guarded_inversion_Pulse.Syntax.Base.comp",
         "fuel_guarded_inversion_Pulse.Syntax.Base.ppname",
         "fuel_guarded_inversion_Pulse.Syntax.Base.st_term",
-        "function_token_typing_Prims.__cache_version_number__",
         "function_token_typing_Prims.int",
         "function_token_typing_Prims.string",
-        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
-        "int_typing", "kinding_Pulse.Syntax.Base.ppname@tok",
+        "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_typing",
+        "kinding_Pulse.Syntax.Base.ppname@tok",
         "kinding_Pulse.Syntax.Base.term@tok",
         "kinding_Pulse.Typing.post_hint_t@tok",
         "lemma_FStar.Map.lemma_ContainsDom",
@@ -88,12 +85,13 @@
         "proj_equation_FStar.Pervasives.Native.Mktuple2__1",
         "proj_equation_FStar.Pervasives.Native.Mktuple2__2",
         "proj_equation_FStar.Pervasives.Native.Some_v",
-        "proj_equation_Pulse.Syntax.Base.C_Tot__0",
         "proj_equation_Pulse.Syntax.Base.Mkbinder_binder_ppname",
         "proj_equation_Pulse.Syntax.Base.Mkbinder_binder_ty",
         "proj_equation_Pulse.Syntax.Base.Mknm_nm_ppname",
         "proj_equation_Pulse.Syntax.Base.Mkppname_name",
-        "proj_equation_Pulse.Syntax.Base.Mkterm_t",
+        "proj_equation_Pulse.Syntax.Base.Mkppname_range",
+        "proj_equation_Pulse.Syntax.Base.Mkst_term_range",
+        "proj_equation_Pulse.Syntax.Base.Mkst_term_term",
         "projection_inverse_BoxBool_proj_0",
         "projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
         "projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
@@ -106,41 +104,41 @@
         "projection_inverse_FStar.Tactics.Result.Success_a",
         "projection_inverse_FStar.Tactics.Result.Success_ps",
         "projection_inverse_FStar.Tactics.Result.Success_v",
-        "projection_inverse_Pulse.Syntax.Base.C_Tot__0",
         "projection_inverse_Pulse.Syntax.Base.Mkbinder_binder_ppname",
         "projection_inverse_Pulse.Syntax.Base.Mkbinder_binder_ty",
         "projection_inverse_Pulse.Syntax.Base.Mknm_nm_ppname",
         "projection_inverse_Pulse.Syntax.Base.Mkppname_name",
-        "projection_inverse_Pulse.Syntax.Base.Mkterm_t",
         "projection_inverse_Pulse.Syntax.Base.Tm_Abs__0",
         "refinement_interpretation_Tm_refine_0e05a441736ee1a990510e8440d3b4d7",
-        "refinement_interpretation_Tm_refine_262f039a938fc14ac016e995f8cd074e",
+        "refinement_interpretation_Tm_refine_25fe9861b42cf97d961ff4c8f44eb399",
         "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
         "refinement_interpretation_Tm_refine_484fe0819d1383a2c20d94ae027baa5f",
         "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
         "refinement_interpretation_Tm_refine_6c182d6f9819de8b46a7a4d39f909d33",
         "refinement_interpretation_Tm_refine_6e8e5238aadfc712ef5fa6bc6310c384",
+        "refinement_interpretation_Tm_refine_78cf9fabb706bab7e54de904b7db9d2a",
         "refinement_interpretation_Tm_refine_7f3ad0958305f2921bfac06f466396ae",
         "refinement_interpretation_Tm_refine_8c22aa61a47c16d0229ef090894097c8",
         "refinement_interpretation_Tm_refine_ba488b4f12660f6fd23fa65ec4b4a4ff",
         "refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
-        "string_typing", "typing_FStar.Map.contains",
-        "typing_FStar.Pervasives.Native.fst",
-        "typing_FStar.Pervasives.Native.uu___is_None",
-        "typing_FStar.Reflection.V2.Data.var", "typing_FStar.Set.complement",
-        "typing_FStar.Set.mem", "typing_FStar.Set.singleton",
+        "string_typing", "typing_FStar.Pervasives.Native.fst",
+        "typing_FStar.Reflection.V2.Data.var", "typing_FStar.Sealed.seal",
+        "typing_FStar.Set.complement", "typing_FStar.Set.mem",
+        "typing_FStar.Set.singleton",
         "typing_Pulse.Checker.Pure.push_context",
         "typing_Pulse.Syntax.Base.__proj__Mkppname__item__name",
-        "typing_Pulse.Syntax.Base.__proj__Mkst_term__item__range",
+        "typing_Pulse.Syntax.Base.__proj__Mkppname__item__range",
+        "typing_Pulse.Syntax.Base.ppname_default",
         "typing_Pulse.Syntax.Base.v_as_nv",
         "typing_Pulse.Syntax.Naming.close_st_term",
+        "typing_Pulse.Syntax.Naming.close_st_term_",
         "typing_Pulse.Syntax.Naming.freevars_st",
-        "typing_Pulse.Typing.Env.as_map", "typing_Pulse.Typing.Env.fresh",
-        "typing_Pulse.Typing.Env.fstar_env",
+        "typing_Pulse.Typing.Env.as_map", "typing_Pulse.Typing.Env.dom",
+        "typing_Pulse.Typing.Env.fresh",
         "typing_Pulse.Typing.Env.push_binding"
       ],
       0,
-      "25d95b794f02aa77026e3575b7127935"
+      "b392d6b9fe11f6e3b5eb6649a0773099"
     ]
   ]
 ]

lib/steel/pulse/Pulse.Checker.Abs.fsti

@@ -4,13 +4,10 @@ module T = FStar.Tactics.V2
 
 open Pulse.Syntax
 open Pulse.Typing
-open Pulse.Checker.Common
+open Pulse.Checker.Base
 
 val check_abs
   (g:env)
   (t:st_term{Tm_Abs? t.term})
-  (pre:term)
-  (pre_typing:tot_typing g pre tm_vprop)
-  (post_hint:post_hint_opt g)
   (check:check_t)
-  : T.Tac (checker_result_t g pre post_hint)
+  : T.Tac (t:st_term & c:comp & st_typing g t c)

lib/steel/pulse/Pulse.Checker.Abs.fsti.hints

@@ -1 +1 @@
-[ "ò¥µgÎJ½qŽ>`É fb-", [] ]
+[ "\u0004hë\u001c\f\u0011ÇmµuÇT\u000ev.®", [] ]

lib/steel/pulse/Pulse.Checker.Admit.fst

@@ -1,14 +1,14 @@
 module Pulse.Checker.Admit
 
 module T = FStar.Tactics.V2
-module RT = FStar.Reflection.Typing
 
 open Pulse.Syntax
 open Pulse.Typing
 open Pulse.Checker.Pure
-open Pulse.Checker.Common
+open Pulse.Checker.Base
+open Pulse.Checker.Prover
 
-module FV = Pulse.Typing.FV
+module P = Pulse.Syntax.Printer
 
 let post_hint_compatible (p:option post_hint_t) (x:var) (t:term) (u:universe) (post:vprop) =
   match p with
@@ -18,15 +18,20 @@ let post_hint_compatible (p:option post_hint_t) (x:var) (t:term) (u:universe) (p
     p.u == u /\
     p.ret_ty == t
 
-#push-options "--z3rlimit_factor 4"
-let check_admit
+let check
   (g:env)
-  (t:st_term{Tm_Admit? t.term})
   (pre:term)
   (pre_typing:tot_typing g pre tm_vprop)
   (post_hint:post_hint_opt g)
+  (res_ppname:ppname)
+  (t:st_term { Tm_Admit? t.term })
+
   : T.Tac (checker_result_t g pre post_hint) =
+
+  let g = Pulse.Typing.Env.push_context g "check_admit" t.range in
+
   let Tm_Admit { ctag = c; typ=t; post } = t.term in
+
   let x = fresh g in
   let px = v_as_nv x in
   let res
@@ -36,9 +41,14 @@ let check_admit
        post:vprop { post_hint_compatible post_hint x t u post } &
        tot_typing (push_binding g x (fst px) t) post tm_vprop)
     = match post, post_hint with
-      | None, None
-      | Some _, Some _ ->
-        fail g None "T_Admit: either no post or two posts"
+      | None, None ->
+        fail g None "could not find a post annotation on admit, please add one"
+
+      | Some post1, Some post2 ->
+        fail g None
+          (Printf.sprintf "found two post annotations on admit: %s and %s, please remove one"
+             (P.term_to_string post1)
+             (P.term_to_string post2.post))
 
       | Some post, _ ->
         let (| u, t_typing |) = check_universe g t in    
@@ -51,7 +61,7 @@ let check_admit
       | _, Some post ->
         let post : post_hint_t = post in
         if x `Set.mem` freevars post.post
-        then fail g None "Unexpected freevar clash in Tm_Admit"
+        then fail g None "Impossible: unexpected freevar clash in Tm_Admit, please file a bug-report"
         else (
           let post_typing_rec = post_hint_typing g post x in
           let post_opened = open_term_nv post.post px in              
@@ -64,9 +74,5 @@ let check_admit
   let s : st_comp = {u;res=t;pre;post} in
 
   assume (open_term (close_term post_opened x) x == post_opened);
-  (|
-     _, //Tm_Admit c u t None,
-     comp_admit c s,
-     T_Admit _ _ c (STC _ s x t_typing pre_typing post_typing)
-  |)
-#pop-options
+  let d = T_Admit _ _ c (STC _ s x t_typing pre_typing post_typing) in
+  prove_post_hint (try_frame_pre pre_typing d res_ppname) post_hint t.range