val input_consistent : fc: Zeta.AppSimulate.appfn_call app -> st: Zeta.AppSimulate.app_state (Mkapp_params?.adm app)
  -> Prims.logical
let input_consistent #app (fc: appfn_call app) (st: app_state app.adm)
  = forall (k: app_key app.adm). ((fc `refs` k) ==> (refkey_inp_val fc k = st k))
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

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

let writes #app (fc: appfn_call app{correct fc})
  = let fn = appfn fc.fid_c in
    let _,_,ws = fn fc.arg_c fc.inp_c in
    ws

val refs_witness (#app:_) (fc: appfn_call app) (k: app_key app.adm)
 (i: Zeta.SeqAux.seq_index fc.inp_c {k = fst (FStar.Seq.index fc.inp_c i)})
  : Lemma (ensures (refs fc k))

(* for a referenced key, the input value provided to the function invocation *)
let refkey_inp_val (#app:_) (fc: appfn_call app) (k: app_key app.adm{fc `refs` k})
  = let open FStar.Seq in
    let i = refkey_idx fc k in
    let _,v = index fc.inp_c i in
    v

(* the written-value of a key *)
let write #app (fc: appfn_call app{correct fc}) (k: app_key app.adm{fc `refs` k})
  = let i = refkey_idx fc k in
    let ws = writes fc in
    let open FStar.Seq in
    index ws i

(* does a fncall succeed for a given state and input? *)
let succeeds #app (fc: appfn_call app) (st: app_state app.adm)
  = Some? (simulate_step fc st)

(* the inputs of a function call are consistent with a state, if the values of all referenced keys are those
/
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 -> st: Zeta.AppSimulate.app_state (Mkapp_params?.adm app)
  -> Prims.logical
Zeta.App.app_params Zeta.AppSimulate.appfn_call Zeta.AppSimulate.app_state Zeta.App.__proj__Mkapp_params__item__adm Prims.l_Forall Zeta.App.app_key Prims.l_imp Zeta.AppSimulate.refs Prims.b2t Prims.op_Equality Zeta.App.app_value_nullable Zeta.AppSimulate.Helper.refkey_inp_val Prims.logical
let input_consistent #app (fc: appfn_call app) (st: app_state app.adm) =
  
forall (k: app_key app.adm). ((fc `refs` k) ==> (refkey_inp_val fc k = st k))