val verifiable_log : app: Zeta.App.app_params -> n: Prims.nat -> Type0
let verifiable_log (app:_) (n:nat)
  = il:ilog app n {verifiable il}
module Zeta.High.Interleave

open FStar.Seq
open Zeta.Interleave
open Zeta.App
open Zeta.Key
open Zeta.GenKey
open Zeta.Record
open Zeta.GenericVerifier
open Zeta.High.Verifier
open Zeta.EAC
open Zeta.Generic.Interleave

module V = Zeta.GenericVerifier
module T = Zeta.Generic.Thread
module G = Zeta.Generic.Global
module GI = Zeta.Generic.Interleave
module HV = Zeta.High.Verifier
module I = Zeta.Interleave
module S = FStar.Seq
module SA = Zeta.SeqAux
module EAC=Zeta.EAC
module MSD = Zeta.MultiSetHashDomain

let ilog (app: app_params) = Zeta.Generic.Interleave.ilog (high_verifier_spec app)
/
Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.MultiSetHashDomain.fsti.checked Zeta.Key.fsti.checked Zeta.Interleave.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.Generic.Thread.fsti.checked Zeta.Generic.Interleave.fsti.checked Zeta.Generic.Global.fsti.checked Zeta.EAC.fsti.checked Zeta.BinTree.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.High.Interleave.fsti
app: Zeta.App.app_params -> n: Prims.nat -> Type0
Zeta.App.app_params Prims.nat Zeta.High.Interleave.ilog Zeta.Generic.Interleave.verifiable Zeta.High.Verifier.high_verifier_spec
let verifiable_log (app: _) (n: nat) =
  
il: ilog app n {verifiable il}