val result : fc: Zeta.AppSimulate.appfn_call app {Zeta.AppSimulate.Helper.correct fc}
  -> Zeta.App.interp_code (Mkapp_params?.adm app)
      (Mkfn_sig?.fres_t (FStar.Map.sel (Mkapp_params?.tbl app) (Mkappfn_call?.fid_c fc)))
let result #app (fc: appfn_call app{correct fc})
  = let fn = appfn fc.fid_c in
    let _,res,_ = fn fc.arg_c fc.inp_c in
    res
module Zeta.AppSimulate.Helper

open Zeta.App
open Zeta.AppSimulate

(* Helper lemmas for reasoning about app simulate *)

(* equality of two app states *)
let app_state_feq #adm (st1 st2: app_state adm)
  = forall (k: app_key adm). {:pattern (st1 k = st2 k)} st1 k = st2 k

val app_state_feq_commutative (#adm:_) (st1 st2: app_state adm)
  : Lemma (ensures (app_state_feq st1 st2 <==> app_state_feq st2 st1))
          [SMTPat (app_state_feq st1 st2); SMTPat (app_state_feq st2 st1)]

val app_state_feq_transitive (#adm:_)  (st1 st2 st3: app_state adm)
  : Lemma (ensures (app_state_feq st1 st2 ==> app_state_feq st2 st3 ==> app_state_feq st1 st3))

(* a correct function call is one which does not fail on the input *)
let correct #app (fc: appfn_call app)
  = let fn = appfn fc.fid_c in
    let rc,_,_ = fn fc.arg_c fc.inp_c in
    rc = Fn_success
/
Zeta.SeqAux.fsti.checked Zeta.AppSimulate.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.AppSimulate.Helper.fsti
fc: Zeta.AppSimulate.appfn_call app {Zeta.AppSimulate.Helper.correct fc}
  -> Zeta.App.interp_code (Mkapp_params?.adm app)
      (Mkfn_sig?.fres_t (FStar.Map.sel (Mkapp_params?.tbl app) (Mkappfn_call?.fid_c fc)))
Zeta.App.app_params Zeta.AppSimulate.appfn_call Prims.b2t Zeta.AppSimulate.Helper.correct Zeta.App.fn_return_code Zeta.App.interp_code Zeta.App.__proj__Mkapp_params__item__adm Zeta.App.__proj__Mkfn_sig__item__fres_t FStar.Map.sel Zeta.App.fn_id Zeta.App.fn_sig Zeta.App.__proj__Mkapp_params__item__tbl Zeta.AppSimulate.__proj__Mkappfn_call__item__fid_c FStar.Seq.Base.seq Zeta.App.app_value_nullable Prims.eq2 Prims.nat FStar.Seq.Base.length Zeta.App.__proj__Mkfn_sig__item__arity FStar.Pervasives.Native.tuple3 Zeta.AppSimulate.__proj__Mkappfn_call__item__arg_c Zeta.AppSimulate.__proj__Mkappfn_call__item__inp_c Zeta.App.app_fn_t Zeta.App.__proj__Mkfn_sig__item__farg_t Zeta.App.appfn
let result #app (fc: appfn_call app {correct fc}) =
  
let fn = appfn fc.fid_c in
let _, res, _ = fn fc.arg_c fc.inp_c in
res