val search_keys_subtree (f: (base_key -> bool)) (k: base_key)
    : Tot
      (o:
        (option base_key)
          { o = None /\ (forall (k': base_key). Zeta.BinTree.is_desc k' k ==> f k') \/
            Some? o /\ not (f (Some?.v o)) }) (decreases (height k))
val search_keys_subtree (f: (base_key -> bool)) (k: base_key)
    : Tot
      (o:
        (option base_key)
          { o = None /\ (forall (k': base_key). Zeta.BinTree.is_desc k' k ==> f k') \/
            Some? o /\ not (f (Some?.v o)) }) (decreases (height k))
let rec search_keys_subtree (f: base_key -> bool) (k: base_key)
  : Tot (o: (option base_key)
    {
      o = None /\ (forall (k': base_key). Zeta.BinTree.is_desc k' k ==> f k')
        \/
      Some? o /\ not ( f (Some?.v o) )
    })
    (decreases (height k))
    = let open Zeta.BinTree in
      if not (f k) then Some k
      else if height k = 0 then (
        let aux (k':base_key)
          : Lemma (ensures (is_desc k' k ==> f k'))
          = if k' = k then ()
            else if not (is_desc k' k) then ()
            else assert(is_proper_desc k' k)
        in
        FStar.Classical.forall_intro aux;
        None
      )
      else
        let ol = search_keys_subtree f (LeftChild k) in
        let or = search_keys_subtree f (RightChild k) in
        if Some? ol then ol
        else if Some? or then or
        else (
          let aux (k': base_key)
            : Lemma (ensures (is_desc k' k ==> f k'))
            = if k' = k then ()
              else if not (is_desc k' k) then ()
              else
                let d = desc_dir k' k in
                if d = Left then ()
                else ()
          in
          FStar.Classical.forall_intro aux;
          None
        )
module Zeta.EAC

open FStar.Classical

open Zeta.SeqMachine
open Zeta.SeqAux

let empty_log_implies_init_state
  (#app: _)
  (k: base_key)
  (l: vlog_ext app{length l = 0})
  : Lemma (ensures (eac_state_of_key k l = EACInit))
  = let smk = eac_smk app k in
    lemma_empty_seq_init smk l

let eac_state_transition
  (#app: app_params)
  (k: base_key)
  (l: vlog_ext app {length l > 0})
  : Lemma (ensures (let open Zeta.SeqAux in
                    let n = length l - 1 in
                    let l' = prefix l n in
                    let ee = index l n in
                    let es' = eac_state_of_key k l' in
                    let es = eac_state_of_key k l in
                    es = eac_add ee es'))
          [SMTPat (eac_state_of_key k l)]
  = let n = length l - 1 in
    let l' = prefix l n in
    let ee = index l n in
    let smk = eac_smk app k in
    lemma_hprefix_append_telem l;
    lemma_reduce_append (init_state smk) (trans_fn smk) l' ee

let eac_empty_log
  (#app: app_params)
  (l: vlog_ext app {length l = 0})
  : Lemma (ensures (eac l))
          [SMTPat (eac l)]
  = lemma_empty l;
    let aux (k: base_key)
        : Lemma (ensures (valid (eac_smk app k) l))
                  [SMTPat (valid (eac_smk app k) l)]
      = lemma_empty_seq_valid (eac_smk app k)
    in
    ()
/
Zeta.SeqMachine.fsti.checked Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.BinTree.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.EAC.fst
f: (_: Zeta.GenericVerifier.base_key -> Prims.bool) -> k: Zeta.GenericVerifier.base_key
  -> Prims.Tot
    (o:
      FStar.Pervasives.Native.option Zeta.GenericVerifier.base_key
        { o = FStar.Pervasives.Native.None /\
          (forall (k': Zeta.GenericVerifier.base_key). Zeta.BinTree.is_desc k' k ==> f k') \/
          Some? o /\ Prims.op_Negation (f (Some?.v o)) })
Zeta.GenericVerifier.base_key Prims.bool Prims.op_Negation FStar.Pervasives.Native.Some Prims.op_Equality Prims.int Zeta.Key.height FStar.Pervasives.Native.None Prims.unit FStar.Classical.forall_intro Prims.l_imp Prims.b2t Zeta.BinTree.is_desc Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern Prims._assert Zeta.BinTree.is_proper_desc FStar.Pervasives.Native.uu___is_Some Zeta.BinTree.bin_tree_dir Zeta.BinTree.Left Prims.op_AmpAmp Zeta.BinTree.child Zeta.BinTree.sibling Zeta.BinTree.desc_dir FStar.Pervasives.Native.option Prims.l_or Prims.l_and Prims.l_Forall FStar.Pervasives.Native.__proj__Some__item__v Zeta.BinTree.RightChild Zeta.EAC.search_keys_subtree Zeta.BinTree.LeftChild
let rec search_keys_subtree (f: (base_key -> bool)) (k: base_key)
    : Tot
      (o:
        (option base_key)
          { o = None /\ (forall (k': base_key). Zeta.BinTree.is_desc k' k ==> f k') \/
            Some? o /\ not (f (Some?.v o)) }) (decreases (height k)) =
  
let open Zeta.BinTree in
if not (f k)
then Some k
else
  if height k = 0
  then
    (let aux (k': base_key) : Lemma (ensures (is_desc k' k ==> f k')) =
        if k' = k then () else if not (is_desc k' k) then () else assert (is_proper_desc k' k)
      in
      FStar.Classical.forall_intro aux;
      None)
  else
    let ol = search_keys_subtree f (LeftChild k) in
    let or = search_keys_subtree f (RightChild k) in
    if Some? ol
    then ol
    else
      if Some? or
      then or
      else
        (let aux (k': base_key) : Lemma (ensures (is_desc k' k ==> f k')) =
            if k' = k
            then ()
            else
              if not (is_desc k' k)
              then ()
              else
                let d = desc_dir k' k in
                if d = Left then ()
          in
          FStar.Classical.forall_intro aux;
          None)