val search_keys (f: (base_key -> bool))
    : o:
    (option base_key){o = None /\ (forall (k: base_key). f k) \/ Some? o /\ not (f (Some?.v o))}
val search_keys (f: (base_key -> bool))
    : o:
    (option base_key){o = None /\ (forall (k: base_key). f k) \/ Some? o /\ not (f (Some?.v o))}
let search_keys (f: base_key -> bool)
  : o: (option base_key)
    {
      o = None /\ (forall (k: base_key). f k)
        \/
      Some? o /\ not (f (Some?.v o))
    }
  = let open Zeta.BinTree in
    let o = search_keys_subtree f Root in
    if None = o then (
      let aux (k: base_key)
        : Lemma (ensures (f k))
                [SMTPat (f k)]
        = lemma_root_is_univ_ancestor k
      in
      o
    )
    else o
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
    ()

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
        )

(* since the space of keys is finite, we can computationally determine if a property is true for all keys
/
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)
  -> o:
    FStar.Pervasives.Native.option Zeta.GenericVerifier.base_key
      { o = FStar.Pervasives.Native.None /\ (forall (k: Zeta.GenericVerifier.base_key). f k) \/
        Some? o /\ Prims.op_Negation (f (Some?.v o)) }
Zeta.GenericVerifier.base_key Prims.bool Prims.op_Equality FStar.Pervasives.Native.option FStar.Pervasives.Native.None Prims.unit Prims.l_True Prims.squash Prims.b2t Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil Zeta.BinTree.lemma_root_is_univ_ancestor Prims.l_or Prims.l_and Prims.l_Forall FStar.Pervasives.Native.uu___is_Some Prims.op_Negation FStar.Pervasives.Native.__proj__Some__item__v Prims.l_imp Zeta.BinTree.is_desc Zeta.BinTree.Root Zeta.EAC.search_keys_subtree
let search_keys (f: (base_key -> bool))
    : o:
    (option base_key){o = None /\ (forall (k: base_key). f k) \/ Some? o /\ not (f (Some?.v o))} =
  
let open Zeta.BinTree in
let o = search_keys_subtree f Root in
if None = o
then
  (let aux (k: base_key) : Lemma (ensures (f k)) [SMTPat (f k)] = lemma_root_is_univ_ancestor k in
    o)
else o