val comp_typing_soundness (g:stt_env)
                          (c:comp)
                          (uc:universe)
                          (d:comp_typing g c uc)
  : GTot (RT.tot_typing (elab_env g) (elab_comp c) (RT.tm_type uc))
let comp_typing_soundness (g:stt_env)
                          (c:comp)
                          (uc:universe)
                          (d:comp_typing g c uc)
  : GTot (RT.tot_typing (elab_env g)
                        (elab_comp c)
                        (RT.tm_type uc))
         (decreases d)
  = match d with
    | CT_Tot _ t _ dt ->
      tot_typing_soundness dt
      
    | CT_ST _ st d_st -> 
      let res_typing, pre_typing, post_typing = stc_soundness d_st in
      STT.stt_typing res_typing pre_typing post_typing

    | CT_STAtomic _ i st d_i d_st -> 
      let i_typing = tot_typing_soundness d_i in
      let res_typing, pre_typing, post_typing = stc_soundness d_st in
      STT.stt_atomic_typing res_typing i_typing pre_typing post_typing

    | CT_STGhost _ i st d_i d_st -> 
      let i_typing = tot_typing_soundness d_i in
      let res_typing, pre_typing, post_typing = stc_soundness d_st in
      STT.stt_ghost_typing res_typing i_typing pre_typing post_typing
val comp_typing_soundness (g:stt_env)
                          (c:comp)
                          (uc:universe)
                          (d:comp_typing g c uc)
  : GTot (RT.tot_typing (elab_env g) (elab_comp c) (RT.tm_type uc))
let comp_typing_soundness (g: stt_env) (c: comp) (uc: universe) (d: comp_typing g c uc)
    : GTot (RT.tot_typing (elab_env g) (elab_comp c) (RT.tm_type uc)) (decreases d) =
match d with
| CT_Tot _ t _ dt -> tot_typing_soundness dt
| CT_ST _ st d_st ->
  let res_typing, pre_typing, post_typing = stc_soundness d_st in
  STT.stt_typing res_typing pre_typing post_typing
| CT_STAtomic _ i st d_i d_st ->
  let i_typing = tot_typing_soundness d_i in
  let res_typing, pre_typing, post_typing = stc_soundness d_st in
  STT.stt_atomic_typing res_typing i_typing pre_typing post_typing
| CT_STGhost _ i st d_i d_st ->
  let i_typing = tot_typing_soundness d_i in
  let res_typing, pre_typing, post_typing = stc_soundness d_st in
  STT.stt_ghost_typing res_typing i_typing pre_typing post_typing
Pulse.Soundness.Comp.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Soundness.STT.fsti.checked Pulse.Soundness.Common.fst.checked Pulse.Reflection.Util.fst.checked Pulse.Elaborate.Core.fst.checked Pulse.Elaborate.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Calc.fsti.checked
Pulse.Soundness.Comp.fst
Pulse.Soundness.Common.stt_env Pulse.Syntax.Base.comp Pulse.Syntax.Base.universe Pulse.Typing.comp_typing Pulse.Typing.Env.env Pulse.Syntax.Base.term Pulse.Typing.universe_of Pulse.Soundness.Common.tot_typing_soundness Pulse.Syntax.Pure.tm_type Pulse.Syntax.Base.st_comp Pulse.Typing.st_comp_typing FStar.Reflection.Typing.tot_typing Pulse.Typing.elab_env Pulse.Elaborate.Pure.elab_term Pulse.Syntax.Base.__proj__Mkst_comp__item__res FStar.Reflection.Typing.tm_type Pulse.Syntax.Base.__proj__Mkst_comp__item__u Pulse.Syntax.Base.__proj__Mkst_comp__item__pre Pulse.Reflection.Util.vprop_tm Pulse.Reflection.Util.mk_abs FStar.Reflection.V2.Data.Q_Explicit Pulse.Syntax.Base.__proj__Mkst_comp__item__post Pulse.Soundness.Common.post1_type_bind Pulse.Soundness.STT.stt_typing Pulse.Elaborate.Pure.elab_comp FStar.Pervasives.Native.tuple3 Pulse.Soundness.Comp.stc_soundness Pulse.Typing.tot_typing Pulse.Syntax.Base.tm_inames Pulse.Soundness.STT.stt_atomic_typing Pulse.Soundness.STT.stt_ghost_typing
module Pulse.Soundness.Comp

open Pulse.Syntax
open Pulse.Reflection.Util
open Pulse.Typing
open Pulse.Elaborate.Core
open Pulse.Elaborate
open Pulse.Soundness.Common

module STT = Pulse.Soundness.STT

let stc_soundness
  (#g:stt_env)
  (#st:st_comp)
  (d_st:st_comp_typing g st)
  
  : GTot (RT.tot_typing (elab_env g)
                        (elab_term st.res)
                        (RT.tm_type st.u) &
          RT.tot_typing (elab_env g)
                        (elab_term st.pre)
                        vprop_tm &
          RT.tot_typing (elab_env g)
                        (mk_abs (elab_term st.res) R.Q_Explicit
                           (elab_term st.post))
                        (post1_type_bind (elab_term st.res))) =
   
  let STC _ st x dres dpre dpost = d_st in
  let res_typing = tot_typing_soundness dres in
  let pre_typing = tot_typing_soundness dpre in      
  calc (==) {
    RT.close_term (elab_term (open_term st.post x)) x;
       (==) { elab_open_commute st.post x }
    RT.close_term (RT.open_term (elab_term st.post) x) x;
       (==) { 
              elab_freevars st.post;
              RT.close_open_inverse (elab_term st.post) x
            }
    elab_term st.post;
  };
  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"
let comp_typing_soundness (g:stt_env)
                          (c:comp)
                          (uc:universe)
                          (d:comp_typing g c uc)
  : GTot (RT.tot_typing (elab_env g)
                        (elab_comp c)
                        (RT.tm_type uc))
val comp_typing_soundness (g:stt_env)
                          (c:comp)
                          (uc:universe)
                          (d:comp_typing g c uc)
  : GTot (RT.tot_typing (elab_env g) (elab_comp c) (RT.tm_type uc))

    g: Pulse.Soundness.Common.stt_env ->
    c: Pulse.Syntax.Base.comp ->
    uc: Pulse.Syntax.Base.universe ->
    d: Pulse.Typing.comp_typing g c uc
  -> Prims.GTot
    (FStar.Reflection.Typing.tot_typing (Pulse.Typing.elab_env g)
        (Pulse.Elaborate.Pure.elab_comp c)
        (FStar.Reflection.Typing.tm_type uc))