val its_log : vcfg: Zeta.Intermediate.VerifierConfig.verifier_config -> Type0
let its_log (vcfg:_)
  = T.its_log (int_verifier_spec vcfg) (vcfg.thread_count)
module Zeta.Intermediate.TSLog

open FStar.Seq
open Zeta.Interleave
open Zeta.Generic.Interleave
open Zeta.Generic.TSLog
open Zeta.Intermediate.VerifierConfig
open Zeta.Intermediate.Verifier
open Zeta.Intermediate.Interleave

module T = Zeta.Generic.TSLog
module I = Zeta.Interleave
module HT = Zeta.High.TSLog
/
Zeta.Intermediate.VerifierConfig.fsti.checked Zeta.Intermediate.Verifier.fsti.checked Zeta.Intermediate.Interleave.fsti.checked Zeta.Interleave.fsti.checked Zeta.High.TSLog.fsti.checked Zeta.Generic.TSLog.fsti.checked Zeta.Generic.Interleave.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.Intermediate.TSLog.fsti
vcfg: Zeta.Intermediate.VerifierConfig.verifier_config -> Type0
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Generic.TSLog.its_log Zeta.Intermediate.Verifier.int_verifier_spec Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__thread_count
let its_log (vcfg: _) =
  
T.its_log (int_verifier_spec vcfg) (vcfg.thread_count)