val input_correct_is_input_consistent (#app:_) (fc: appfn_call app) (st: app_state app.adm)
  : Lemma (ensures (let rs = fc.inp_c in
                   input_consistent fc st <==> input_correct st rs))
          [SMTPat (input_consistent fc st)]
val input_correct_is_input_consistent (#app:_) (fc: appfn_call app) (st: app_state app.adm)
  : Lemma (ensures (let rs = fc.inp_c in
                   input_consistent fc st <==> input_correct st rs))
          [SMTPat (input_consistent fc st)]
let input_correct_is_input_consistent (#app:_) (fc: appfn_call app) (st: app_state app.adm)
  : Lemma (ensures (let rs = fc.inp_c in
                   input_consistent fc st <==> input_correct st rs))
  = let rs = fc.inp_c in
    if input_correct st rs then (
      let aux (k:_)
        : Lemma (ensures (fc `refs` k ==> refkey_inp_val fc k = st k))
        = if fc `refs_comp` k then (
            let i = refkey_idx fc k in
            ()
          )
      in
      FStar.Classical.forall_intro aux
    )
    else (
      let open Zeta.SeqIdx in
      let i = last_idx (hoist_ghost (record_incorrect st)) rs in
      let k,v = S.index rs i in
      FStar.Classical.exists_intro (fun i -> (let k',v = S.index fc.inp_c i in k' = k)) i;
      assert(fc `refs` k);
      FStar.Classical.exists_intro (fun k -> (fc `refs` k /\ ~ (refkey_inp_val fc k = st k))) k
    )
module Zeta.AppSimulate.Helper

open FStar.Classical
module S = FStar.Seq

open Zeta.Ghost

let app_state_feq_comm_aux (#adm:_) (st1 st2: app_state adm)
  : Lemma (requires (app_state_feq st1 st2))
          (ensures (app_state_feq st2 st1))
  = let aux (k:_)
      : Lemma (ensures (st2 k = st1 k))
      = assert(st1 k = st2 k)
    in
    forall_intro aux

let app_state_feq_commutative (#adm) (st1 st2: app_state adm)
  : Lemma (ensures (app_state_feq st1 st2 <==> app_state_feq st2 st1))
  = introduce (app_state_feq st1 st2) ==> (app_state_feq st2 st1)
    with _. app_state_feq_comm_aux st1 st2;
    introduce (app_state_feq st2 st1) ==> (app_state_feq st1 st2)
    with _. app_state_feq_comm_aux st2 st1

let app_state_feq_transitive_aux (#adm) (st1 st2 st3: app_state adm)
  : Lemma (requires (app_state_feq st1 st2 /\ app_state_feq st2 st3))
          (ensures (app_state_feq st1 st3))
  = let aux(k:_)
      : Lemma (ensures (st1 k = st3 k))
      = assert(st1 k = st2 k);
        assert(st2 k = st3 k)
    in
    forall_intro aux

let 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))
  = introduce (app_state_feq st1 st2 /\ app_state_feq st2 st3) ==> (app_state_feq st1 st3)
    with _. app_state_feq_transitive_aux st1 st2 st3

let of_key (#adm:_) (ki: app_key adm) (r: app_record adm)
  = let k,_ = r in
    k = ki

let 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))
 = let open Zeta.SeqIdx in
   exists_elems_with_prop_intro (of_key k) fc.inp_c i

let record_incorrect (#adm:_) (st: app_state adm) (r: app_record adm)
  : GTot bool
  = let k,v = r in
    st k <> v

let feq_imnplies_input_consistent_identical_aux (#app:_) (fc: appfn_call app) (st1 st2: app_state app.adm)
  : Lemma (requires (app_state_feq st1 st2 /\ input_consistent fc st1))
          (ensures (input_consistent fc st2))
  = let aux (k:_)
      : Lemma (ensures (fc `refs` k ==> refkey_inp_val fc k = st2 k))
      = if fc `refs_comp` k then (
          assert(refkey_inp_val fc k = st1 k);
          assert(st1 k = st2 k)
        )
    in
    forall_intro aux

let feq_implies_input_consistent_identical (#app:_) (fc: appfn_call app) (st1 st2: app_state app.adm)
  : Lemma (requires (app_state_feq st1 st2))
          (ensures (input_consistent fc st1 <==> input_consistent fc st2))
  = introduce (input_consistent fc st1) ==> (input_consistent fc st2)
    with _. feq_imnplies_input_consistent_identical_aux fc st1 st2;
    introduce (input_consistent fc st2) ==> (input_consistent fc st1)
    with _. feq_imnplies_input_consistent_identical_aux fc st2 st1
/
Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Ghost.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.AppSimulate.Helper.fst
fc: Zeta.AppSimulate.appfn_call app -> st: Zeta.AppSimulate.app_state (Mkapp_params?.adm app)
  -> FStar.Pervasives.Lemma
      (ensures
        (let rs = Mkappfn_call?.inp_c fc in
          Zeta.AppSimulate.Helper.input_consistent fc st <==> Zeta.AppSimulate.input_correct st rs))
      [SMTPat (Zeta.AppSimulate.Helper.input_consistent fc st)]
Zeta.App.app_params Zeta.AppSimulate.appfn_call Zeta.AppSimulate.app_state Zeta.App.__proj__Mkapp_params__item__adm Zeta.AppSimulate.input_correct FStar.Classical.forall_intro Zeta.App.app_key Zeta.AppSimulate.refs Prims.l_imp Prims.b2t Prims.op_Equality Zeta.App.app_value_nullable Zeta.AppSimulate.Helper.refkey_inp_val Prims.unit Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Zeta.AppSimulate.refs_comp Prims.nat Prims.op_LessThan FStar.Seq.Base.length Zeta.App.app_record Zeta.AppSimulate.__proj__Mkappfn_call__item__inp_c FStar.Seq.Base.index Zeta.AppSimulate.refkey_idx Prims.bool FStar.Classical.exists_intro Prims.l_and Prims.l_not Prims._assert Zeta.SeqAux.seq_index Zeta.Ghost.hoist_ghost Zeta.AppSimulate.Helper.record_incorrect Zeta.SeqIdx.last_idx Zeta.App.appfn_rs_t Zeta.AppSimulate.__proj__Mkappfn_call__item__fid_c Prims.l_iff Zeta.AppSimulate.Helper.input_consistent
let input_correct_is_input_consistent (#app: _) (fc: appfn_call app) (st: app_state app.adm)
    : Lemma
    (ensures
      (let rs = fc.inp_c in
        input_consistent fc st <==> input_correct st rs)) =
  
let rs = fc.inp_c in
if input_correct st rs
then
  (let aux (k: _) : Lemma (ensures (fc `refs` k ==> refkey_inp_val fc k = st k)) =
      if fc `refs_comp` k
      then
        (let i = refkey_idx fc k in
          ())
    in
    FStar.Classical.forall_intro aux)
else
  (let open Zeta.SeqIdx in
    let i = last_idx (hoist_ghost (record_incorrect st)) rs in
    let k, v = S.index rs i in
    FStar.Classical.exists_intro (fun i ->
          (let k', v = S.index fc.inp_c i in
            k' = k))
      i;
    assert (fc `refs` k);
    FStar.Classical.exists_intro (fun k -> (fc `refs` k /\ ~(refkey_inp_val fc k = st k))) k)