val aems_equal_or_hash_collision
      (epmax: epoch_id)
      (logs: all_logs{verifiable_and_certified logs epmax})
    : GTot
    (o:
      option ms_hash_collision
        { let i_logs = to_ilog logs in
          let i_epmax = lift_epoch epmax in
          None? o /\ GG.aems_equal_upto i_epmax i_logs \/ Some? o })
val aems_equal_or_hash_collision
      (epmax: epoch_id)
      (logs: all_logs{verifiable_and_certified logs epmax})
    : GTot
    (o:
      option ms_hash_collision
        { let i_logs = to_ilog logs in
          let i_epmax = lift_epoch epmax in
          None? o /\ GG.aems_equal_upto i_epmax i_logs \/ Some? o })
let aems_equal_or_hash_collision (epmax: epoch_id)
                                 (logs: all_logs {verifiable_and_certified logs epmax})
  : GTot (o:option ms_hash_collision
    {
      let i_logs = to_ilog logs in
      let i_epmax = lift_epoch epmax in
      None? o /\ GG.aems_equal_upto i_epmax i_logs
      \/
      Some? o
    })
  = let i_logs = to_ilog logs in
    let i_epmax = lift_epoch epmax in
    let o = search_epoch i_epmax i_logs in

    if None = o then
      None
    else (
      let i_ep = Some?.v o in
      let add_set = GG.add_set i_ep i_logs in
      let evict_set = GG.evict_set i_ep i_logs in
      assert(add_set =!= evict_set);

      assert(i_ep <= i_epmax);
      let ep = U32.uint_to_t i_ep in
      assert(AH.epoch_is_certified (as_tid_logs logs) ep);
      certified_epoch_aggregate_hashes_equal logs ep;
      aggr_add_hash_correct logs ep;
      aggr_evict_hash_correct logs ep;
      Some (MSCollision add_set evict_set)
    )
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

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
/
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.ThreadStateModel.epoch_id ->
    logs:
      Zeta.Steel.ThreadStateModel.all_logs{Zeta.Steel.GlobalRel.verifiable_and_certified logs epmax}
  -> Prims.GTot
    (o:
      FStar.Pervasives.Native.option Zeta.Steel.MultiSetHash.ms_hash_collision
        { let i_logs = Zeta.Steel.GlobalRel.to_ilog logs in
          let i_epmax = Zeta.Steel.Rel.lift_epoch epmax in
          None? o /\ Zeta.Generic.Global.aems_equal_upto i_epmax i_logs \/ Some? o })
Zeta.Steel.ThreadStateModel.epoch_id Zeta.Steel.ThreadStateModel.all_logs Zeta.Steel.GlobalRel.verifiable_and_certified Prims.op_Equality FStar.Pervasives.Native.option Zeta.Steel.Rel.i_epoch FStar.Pervasives.Native.None Zeta.Steel.MultiSetHash.ms_hash_collision Prims.bool FStar.Pervasives.Native.Some Zeta.Steel.MultiSetHash.MSCollision Prims.unit Zeta.Steel.GlobalRel.aggr_evict_hash_correct Zeta.Steel.GlobalRel.aggr_add_hash_correct Zeta.Steel.GlobalRel.certified_epoch_aggregate_hashes_equal Prims._assert Zeta.Steel.AggregateEpochHashes.epoch_is_certified Zeta.Steel.GlobalRel.as_tid_logs FStar.UInt32.t FStar.UInt32.uint_to_t Prims.b2t Prims.op_LessThanOrEqual Prims.l_not Prims.eq2 Zeta.MultiSetHashDomain.mset_ms_hashfn_dom Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__app Zeta.Intermediate.Verifier.int_verifier_spec Zeta.Steel.Rel.i_vcfg Zeta.Generic.Global.evict_set Zeta.Generic.Global.add_set FStar.Pervasives.Native.__proj__Some__item__v Prims.l_or Prims.l_and FStar.Pervasives.Native.uu___is_None Zeta.Generic.Global.aems_equal_upto FStar.Pervasives.Native.uu___is_Some Zeta.Steel.Rel.lift_epoch Zeta.Steel.GlobalRel.i_verifiable_logs Prims.int Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.Seq.Base.length Zeta.GenericVerifier.verifier_log Zeta.Steel.GlobalRel.n_threads_v Zeta.Steel.GlobalRel.to_ilog Zeta.Correctness.search_epoch
let aems_equal_or_hash_collision
      (epmax: epoch_id)
      (logs: all_logs{verifiable_and_certified logs epmax})
    : GTot
    (o:
      option ms_hash_collision
        { let i_logs = to_ilog logs in
          let i_epmax = lift_epoch epmax in
          None? o /\ GG.aems_equal_upto i_epmax i_logs \/ Some? o }) =
  
let i_logs = to_ilog logs in
let i_epmax = lift_epoch epmax in
let o = search_epoch i_epmax i_logs in
if None = o
then None
else
  (let i_ep = Some?.v o in
    let add_set = GG.add_set i_ep i_logs in
    let evict_set = GG.evict_set i_ep i_logs in
    assert (add_set =!= evict_set);
    assert (i_ep <= i_epmax);
    let ep = U32.uint_to_t i_ep in
    assert (AH.epoch_is_certified (as_tid_logs logs) ep);
    certified_epoch_aggregate_hashes_equal logs ep;
    aggr_add_hash_correct logs ep;
    aggr_evict_hash_correct logs ep;
    Some (MSCollision add_set evict_set))