Merge pull request #577 from FStarLang/gebner_rmsound

Remove soundness

Author: gebner

src/checker/Pulse.Checker.Abs.fst

@@ -28,7 +28,7 @@ open FStar.List.Tot
 module RT = FStar.Reflection.Typing
 module P = Pulse.Syntax.Printer
 module PSB = Pulse.Syntax.Builder
-module FV = Pulse.Typing.FV
+
 module T = FStar.Tactics.V2
 module R = FStar.Reflection.V2
 module RU = Pulse.RuntimeUtils
@@ -316,7 +316,7 @@ let preprocess_abs
     debug_abs g (fun _ -> Printf.sprintf "rebuild_abs = %s\n" (P.st_term_to_string abs));
     abs
 
-let sub_effect_comp g r (asc:comp_ascription) (c_computed:comp) : T.Tac (option (c2:comp & lift_comp g c_computed c2)) =
+let sub_effect_comp g r (asc:comp_ascription) (c_computed:comp) : T.Tac (option comp) =
   let nop = None in
   match asc.elaborated with
   | None -> nop
@@ -326,19 +326,17 @@ let sub_effect_comp g r (asc:comp_ascription) (c_computed:comp) : T.Tac (option
     | C_ST _, C_ST _ -> nop
     | C_STGhost _ _, C_STGhost _ _ -> nop
     | C_STAtomic i Neutral c1, C_STGhost _ _ ->
-      let lift = Lift_Neutral_Ghost g c_computed in
-      Some (| C_STGhost i c1, lift |)
+      Some (C_STGhost i c1)
     | C_STAtomic i o1 c1, C_STAtomic j o2 c2 ->
       if sub_observability o1 o2
-      then let lift = Lift_Observability g c_computed o2 in
-           Some (| C_STAtomic i o2 c1, lift |)
+      then Some (C_STAtomic i o2 c1)
       else nop
 
     (* FIXME: more lifts here *) 
     | _ -> nop
 
-let check_effect_annotation g r (asc:comp_ascription) (c_computed:comp) : T.Tac (c2:comp & st_sub g c_computed c2) =
-  let nop = (| c_computed, STS_Refl _ _ |) in
+let check_effect_annotation g r (asc:comp_ascription) (c_computed:comp) : T.Tac comp =
+  let nop = c_computed in
   match asc.elaborated with
   | None -> nop
   | Some c ->
@@ -360,10 +358,9 @@ let check_effect_annotation g r (asc:comp_ascription) (c_computed:comp) : T.Tac
 
       let b = mk_binder "res" Range.range_0 c2.res in
       let phi = tm_inames_subset j i in
-      let typing = tm_inames_subset_typing g j i in
       // Or:
       // let typing = core_check_tot_term g phi tm_prop in
-      let tok = T.with_policy T.ForceSMT (fun () -> try_check_prop_validity g phi typing) in
+      let tok = T.with_policy T.ForceSMT (fun () -> try_check_prop_validity g phi) in
       if None? tok then (
         let open Pulse.PP in
         fail_doc g (Some (RU.range_of_term i)) [
@@ -375,12 +372,7 @@ let check_effect_annotation g r (asc:comp_ascription) (c_computed:comp) : T.Tac
 
       let Some tok = tok in
 
-      let d_sub : st_sub g c_computed c =
-        match c_computed with
-        | C_STAtomic _ obs _ -> STS_AtomicInvs g c2 j i obs obs tok
-        | C_STGhost _ _ -> STS_GhostInvs g c2 j i tok
-      in
-      (| c, d_sub |)
+      c
 
     | _, _ ->
       let open Pulse.PP in
@@ -396,16 +388,15 @@ let check_effect_annotation g r (asc:comp_ascription) (c_computed:comp) : T.Tac
 (* Rewrite the comp c into the annotated one, if any,
 preserving the st_typing derivation d *)
 let maybe_rewrite_body_typing
-      (#g:_) (#e:st_term) (#c:comp)
-      (d:st_typing g e c)
+      (g:_) (e:st_term) (c:comp)
       (asc:comp_ascription)
-  : T.Tac (c':comp & st_typing g e c')
+  : T.Tac comp
   = let open Pulse.PP in
     match asc.annotated, c with
-    | None, _ -> (| c, d |)
+    | None, _ -> c
     | Some (C_Tot t), C_Tot t' -> (
         let t, _ = Pulse.Checker.Pure.instantiate_term_implicits g t None false in
-        let (| u, t_typing |) = Pulse.Checker.Pure.check_universe g t in
+        let u = Pulse.Checker.Pure.check_universe g t in
         match T.t_check_equiv true true (elab_env g) t t' with
         | None, _ ->
           Env.fail_doc g (Some e.range) [
@@ -419,15 +410,7 @@ let maybe_rewrite_body_typing
               (show c)
               (show (C_Tot t)));
           let sq : squash (RT.equiv_token (elab_env g) t t') = () in
-          let t'_typing : universe_of g t' u =
-            (* t is equiv to t', and t has universe t. *)
-            magic ()
-          in
-          let tok' : st_equiv g (C_Tot t') (C_Tot t) =
-            ST_TotEquiv _ t' t u t'_typing
-              (RT.Rel_sym _ _ _ (RT.Rel_eq_token _ _ _ sq))
-          in
-          (| C_Tot t, T_Equiv _ _ _ _ d tok' |)
+          C_Tot t
     )
 
     (* c is not a C_Tot *)
@@ -456,15 +439,15 @@ let rec check_abs_core
   (g:env)
   (t:st_term{Tm_Abs? t.term})
   (check:check_t)
-  : T.Tac (t:st_term & c:comp & st_typing g t c) =
+  : T.Tac (t:st_term & c:comp) =
   //warn g (Some t.range) (Printf.sprintf "check_abs_core, t = %s" (P.st_term_to_string t));
   let range = t.range in
   match t.term with  
   | Tm_Abs { b = {binder_ty=t;binder_ppname=ppname;binder_attrs}; q=qual; ascription=asc; body } -> //pre=pre_hint; body; ret_ty; post=post_hint_body } ->
     let qual = T.map_opt (check_qual g) qual in
     (*  (fun (x:t) -> {pre_hint} body : t { post_hint } *)
-    let (| t, _, _ |) = compute_tot_term_type g t in //elaborate it first
-    let (| u, t_typing |) = universe_of_well_typed_term g t in //then check that its universe ... We could collapse the two calls
+    let (| t, _ |) = compute_tot_term_type g t in //elaborate it first
+    let u = universe_of_well_typed_term 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
@@ -474,27 +457,21 @@ let rec check_abs_core
     match body_opened.term with
     | Tm_Abs _ ->
       (* Check the opened body *)
-      let (| body, c_body, body_typing |) = check_abs_core g' body_opened check in
+      let (| body, c_body |) = check_abs_core g' body_opened check in
 
       (* First lift into annotated effect *)
-      let (| c_body, body_typing |) : ( c_body:comp & st_typing g' body c_body ) =
+      let c_body : comp =
         match sub_effect_comp g' body.range asc c_body with
-        | None -> (| c_body, body_typing |)
-        | Some (| c_body, lift |) ->
-          let body_typing = T_Lift _ _ _ _ body_typing lift in
-          (| c_body, body_typing |)
+        | None -> c_body
+        | Some c_body -> c_body
       in
 
       (* Check if it matches annotation (if any, likely not), and adjust derivation
       if needed. Currently this only subtypes the invariants. *)
-      let (| c_body, d_sub |) = check_effect_annotation g' body.range asc c_body in
-      let body_typing = T_Sub _ _ _ _ body_typing d_sub in
-      (* Similar to above, fixes the type of the computation if we need to match
-      its annotation. TODO: merge these two by adding a tot subtyping (or equiv)
-      case to the st_sub judg. *)
-      let (| c_body, body_typing |) = maybe_rewrite_body_typing body_typing asc in
-
-      FV.st_typing_freevars body_typing;
+      let c_body = check_effect_annotation g' body.range asc c_body in
+
+      let c_body = maybe_rewrite_body_typing g' body c_body asc in
+
       let body_closed = close_st_term body x in
       assume (open_st_term body_closed x == body);
 
@@ -506,9 +483,9 @@ let rec check_abs_core
         |> FStar.Sealed.seal in
 
       let b = {binder_ty=t;binder_ppname=ppname;binder_attrs} 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;binder_attrs} qual (close_comp c_body x) in
-      (| _, C_Tot tres, tt |)
+      let abs_st = wtag None (Tm_Abs { b; q=qual; body=body_closed; ascription=empty_ascription}) in
+      (| abs_st, C_Tot tres |)
     | _ ->
       let elab_c, pre_opened, inames_opened, ret_ty, post_hint_body =
         match asc.elaborated with
@@ -547,7 +524,7 @@ let rec check_abs_core
           Some (open_term_nv (comp_res c) px),
           Some (open_term' (comp_post c) var 1)
       in
-      let (| pre_opened, pre_typing |) =
+      let pre_opened =
         (* In some cases F* can mess up the range in error reporting and make it
          point outside of this term. Bound it here. See e.g. Bug59, if we remove
          this bound then the range points to the span between the 'x' and 'y' binders. *)
@@ -571,7 +548,7 @@ let rec check_abs_core
       in
 
       let ppname_ret = mk_ppname_no_range "_fret" in
-      let r  = check g' pre_opened pre_typing post ppname_ret body_opened  in
+      let r  = check g' pre_opened post ppname_ret body_opened  in
       let (| post, r |) : (ph:post_hint_opt g' & checker_result_t g' pre_opened ph) =
         match post with
         | PostHint _ -> (| post, r |)
@@ -583,37 +560,34 @@ let rec check_abs_core
           let r = Pulse.Checker.Prover.prove_post_hint r (PostHint ph) (T.range_of_term t) in
           (| PostHint ph, r |)
       in
-      let (| body, c_body, body_typing |) : st_typing_in_ctxt g' pre_opened post =
+      let (| body, c_body |) : st_typing_in_ctxt g' pre_opened post =
         RU.record_stats "apply_checker_result_k" fun _ ->
         apply_checker_result_k #_ #_ #(PostHint?.v post) r ppname_ret in
 
       let c_opened : comp_ascription = { annotated = None; elaborated = Some (open_comp_nv elab_c px) } in
 
       (* First lift into annotated effect *)
-      let (| c_body, body_typing |) : ( c_body:comp & st_typing g' body c_body ) =
+      let c_body : comp =
         match sub_effect_comp g' body.range c_opened c_body with
-        | None -> (| c_body, body_typing |)
-        | Some (| c_body, lift |) ->
-          let body_typing = T_Lift _ _ _ _ body_typing lift in
-          (| c_body, body_typing |)
+        | None -> c_body
+        | Some c_body -> c_body
       in
 
-      let (| c_body, d_sub |) = check_effect_annotation g' body.range c_opened c_body in
-      let body_typing = T_Sub _ _ _ _ body_typing d_sub in
+      let c_body = check_effect_annotation g' body.range c_opened c_body in
+
 
-      let (| c_body, body_typing |) = maybe_rewrite_body_typing body_typing asc in
+      let c_body = maybe_rewrite_body_typing g' body c_body asc in
 
-      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;binder_attrs} 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;binder_attrs} qual (close_comp c_body x) in
+      let abs_st = wtag None (Tm_Abs { b; q=qual; body=body_closed; ascription=empty_ascription}) in
 
-      (| _, C_Tot tres, tt |)
+      (| abs_st, C_Tot tres |)
 #pop-options
 
 let check_abs (g:env) (t:st_term{Tm_Abs? t.term}) (check:check_t)
-  : T.Tac (t:st_term & c:comp & st_typing g t c) =
+  : T.Tac (t:st_term & c:comp) =
   let t = preprocess_abs g t in
   check_abs_core g t check

src/checker/Pulse.Checker.Abs.fsti

@@ -32,4 +32,4 @@ val check_abs
   (g:env)
   (t:st_term{Tm_Abs? t.term})
   (check:check_t)
-  : T.Tac (t:st_term & c:comp & st_typing g t c)
+  : T.Tac (t:st_term & c:comp)

src/checker/Pulse.Checker.Admit.fst

@@ -29,7 +29,6 @@ module P = Pulse.Syntax.Printer
 let check
   (g:env)
   (pre:term)
-  (pre_typing:tot_typing g pre tm_slprop)
   (post_hint:post_hint_opt g)
   (res_ppname:ppname)
   (t:st_term { Tm_Admit? t.term })
@@ -44,8 +43,7 @@ let check
   let x = fresh g in
   let px = v_as_nv x in
   let res
-    : (c:comp_st { comp_pre c == pre /\ comp_post_matches_hint c post_hint } &
-       comp_typing g c (universe_of_comp c))
+    : c:comp_st { comp_pre c == pre /\ comp_post_matches_hint c post_hint }
     = match post, post_hint with
       | None, NoHint
       | None, TypeHint _ ->
@@ -58,24 +56,29 @@ let check
              (P.term_to_string post2.post))
 
       | Some post, _ ->
-        let (| u, t_typing |) = check_universe g t in    
+        let u = check_universe g t in    
         let post_opened = open_term_nv post px in      
-        let (| post_opened, post_typing |) = 
+        let post_opened = 
           check_tot_term (push_binding g x (fst px) t) post_opened tm_slprop
         in
         let post = close_term post_opened x in
         let s : st_comp = {u;res=t;pre;post} in
         assume (open_term (close_term post_opened x) x == post_opened);
-        let d_s : st_comp_typing _ s = STC _ s x t_typing pre_typing post_typing in
+
         (match c with
-         | STT -> (| _,  CT_ST _ _ d_s |)
-         | STT_Ghost -> (| _, CT_STGhost _ tm_emp_inames _ (RU.magic ()) d_s |)
-         | STT_Atomic -> (| _, CT_STAtomic _ tm_emp_inames Neutral _ (RU.magic ()) d_s |))
+         | STT -> C_ST s
+         | STT_Ghost -> C_STGhost tm_emp_inames s
+         | STT_Atomic -> C_STAtomic tm_emp_inames Neutral s)
 
-      | _, PostHint post -> Pulse.Typing.Combinators.comp_for_post_hint pre_typing post x
+      | _, PostHint post -> Pulse.Typing.Combinators.comp_for_post_hint g pre post x
   in
-  let (| c, d_c |) = res in
-  let d = T_Admit _ _ d_c in
+  let c = res in
+  let admit_st = wtag (Some (ctag_of_comp_st c))
+                      (Tm_Admit { ctag=ctag_of_comp_st c;
+                                  u=comp_u c;
+                                  typ=comp_res c;
+                                  post=None }) in
+
   FStar.Tactics.BreakVC.break_vc ();
   // ^ This makes a big difference! Would be good to distill into
   // a smaller F*-only example and file an issue.
@@ -92,4 +95,4 @@ let check
     ] in
     info_doc_env g (Some t0.range) msg
   end else ()) <: T.Tac unit;
-  checker_result_for_st_typing (| _, _, d |) res_ppname
+  checker_result_for_st_typing (| admit_st, c |) res_ppname

src/checker/Pulse.Checker.Admit.fsti

@@ -25,7 +25,6 @@ open Pulse.Checker.Base
 val check
   (g:env)
   (pre:term)
-  (pre_typing:tot_typing g pre tm_slprop)
   (post_hint:post_hint_opt g)
   (res_ppname:ppname)
   (t:st_term { Tm_Admit? t.term })