val its_log : vspec: Zeta.GenericVerifier.verifier_spec -> n: Prims.nat -> Type0
let its_log vspec n = il:verifiable_log vspec n{clock_sorted il}
module Zeta.Generic.TSLog

open FStar.Seq
open Zeta.SeqAux
open Zeta.Interleave
open Zeta.Time
open Zeta.GenericVerifier
open Zeta.Generic.Thread
open Zeta.Generic.Global
open Zeta.Generic.Interleave

module I = Zeta.Interleave
module G = Zeta.Generic.Global
module T = Zeta.Generic.Thread
module S = FStar.Seq
module SA = Zeta.SeqAux

let clock_sorted (#vspec:_) (#n:_) (il: verifiable_log vspec n) =
  forall (i j: seq_index il). i <= j ==> clock il i `ts_leq` clock il j
/
Zeta.Time.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Interleave.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.Generic.Thread.fsti.checked Zeta.Generic.Interleave.fsti.checked Zeta.Generic.Global.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.Generic.TSLog.fsti
vspec: Zeta.GenericVerifier.verifier_spec -> n: Prims.nat -> Type0
Zeta.GenericVerifier.verifier_spec Prims.nat Zeta.Generic.Interleave.verifiable_log Zeta.Generic.TSLog.clock_sorted
let its_log vspec n =
  
il: verifiable_log vspec n {clock_sorted il}