val search_epoch (epmax: i_epoch) (logs: i_verifiable_logs)
    : GTot
      (o:
        option i_epoch
          { None? o /\ GG.aems_equal_upto epmax logs \/
            Some? o /\ ~(GG.add_set (Some?.v o) logs == GG.evict_set (Some?.v o) logs) /\
            Some?.v o <= epmax }) (decreases epmax)
val search_epoch (epmax: i_epoch) (logs: i_verifiable_logs)
    : GTot
      (o:
        option i_epoch
          { None? o /\ GG.aems_equal_upto epmax logs \/
            Some? o /\ ~(GG.add_set (Some?.v o) logs == GG.evict_set (Some?.v o) logs) /\
            Some?.v o <= epmax }) (decreases epmax)
let rec search_epoch (epmax: i_epoch)
                     (logs: i_verifiable_logs)
  : GTot (o:option i_epoch
    {
      None? o /\ GG.aems_equal_upto epmax logs
      \/
      Some? o /\ ~ (GG.add_set (Some?.v o) logs == GG.evict_set (Some?.v o) logs) /\
      Some?.v o <= epmax
    })
    (decreases epmax)
  = if Zeta.MultiSet.eq (GG.add_set epmax logs) (GG.evict_set epmax logs) then
      if epmax = 0 then None
      else search_epoch (epmax - 1) logs
    else
      Some epmax
module Zeta.Correctness

open Zeta.App
open Zeta.AppSimulate
open Zeta.Steel.ApplicationTypes
open Zeta.Steel.ThreadStateModel
open Zeta.Steel.MultiSetHash
open Zeta.Steel.Rel
open Zeta.Steel.ThreadRel
open Zeta.Steel.GlobalRel

module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module HA = Zeta.Steel.HashAccumulator
module GG = Zeta.Generic.Global
module AH = Zeta.Steel.AggregateEpochHashes

let hash_collision = Zeta.HashCollision.hash_collision app
/
Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.ThreadRel.fsti.checked Zeta.Steel.Rel.fsti.checked Zeta.Steel.MultiSetHash.fsti.checked Zeta.Steel.HashAccumulator.fsti.checked Zeta.Steel.GlobalRel.fsti.checked Zeta.Steel.ApplicationTypes.fsti.checked Zeta.Steel.AggregateEpochHashes.fsti.checked Zeta.SeqAux.fsti.checked Zeta.MultiSet.fsti.checked Zeta.Intermediate.Correctness.fst.checked Zeta.HashCollision.fsti.checked Zeta.Generic.Global.fsti.checked Zeta.AppSimulate.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Squash.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked
Zeta.Correctness.fst
epmax: Zeta.Steel.Rel.i_epoch -> logs: Zeta.Steel.GlobalRel.i_verifiable_logs
  -> Prims.GTot
    (o:
      FStar.Pervasives.Native.option Zeta.Steel.Rel.i_epoch
        { None? o /\ Zeta.Generic.Global.aems_equal_upto epmax logs \/
          Some? o /\
          ~(Zeta.Generic.Global.add_set (Some?.v o) logs ==
            Zeta.Generic.Global.evict_set (Some?.v o) logs) /\ Some?.v o <= epmax })
Zeta.Steel.Rel.i_epoch Zeta.Steel.GlobalRel.i_verifiable_logs Zeta.MultiSet.eq Zeta.MultiSetHashDomain.ms_hashfn_dom Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.Intermediate.Verifier.int_verifier_spec Zeta.Steel.Rel.i_vcfg Zeta.MultiSetHashDomain.ms_hashfn_dom_cmp Zeta.Generic.Global.add_set Zeta.Generic.Global.evict_set Prims.op_Equality Prims.int FStar.Pervasives.Native.None Prims.bool Zeta.Correctness.search_epoch Prims.op_Subtraction FStar.Pervasives.Native.option Prims.l_or Prims.l_and Prims.b2t FStar.Pervasives.Native.uu___is_None Zeta.Generic.Global.aems_equal_upto FStar.Pervasives.Native.uu___is_Some Prims.l_not Prims.eq2 Zeta.MultiSetHashDomain.mset_ms_hashfn_dom FStar.Pervasives.Native.__proj__Some__item__v Prims.op_LessThanOrEqual FStar.Pervasives.Native.Some
let rec search_epoch (epmax: i_epoch) (logs: i_verifiable_logs)
    : GTot
      (o:
        option i_epoch
          { None? o /\ GG.aems_equal_upto epmax logs \/
            Some? o /\ ~(GG.add_set (Some?.v o) logs == GG.evict_set (Some?.v o) logs) /\
            Some?.v o <= epmax }) (decreases epmax) =
  
if Zeta.MultiSet.eq (GG.add_set epmax logs) (GG.evict_set epmax logs)
then if epmax = 0 then None else search_epoch (epmax - 1) logs
else Some epmax