val store : tl: Zeta.High.Thread.verifiable_log app -> Prims.GTot (Zeta.High.Verifier.store_t app)
let store (#app:_) (tl: verifiable_log app)
  = let vs = state tl in
    vs.st
module Zeta.High.Thread

open Zeta.GenKey
open Zeta.GenericVerifier
open Zeta.High.Verifier
open Zeta.Generic.Thread

let verifiable_log (app:_)
  = Zeta.Generic.Thread.verifiable_log (high_verifier_spec app)
/
Zeta.MultiSetHashDomain.fsti.checked Zeta.Key.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.Generic.Thread.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.High.Thread.fsti
tl: Zeta.High.Thread.verifiable_log app -> Prims.GTot (Zeta.High.Verifier.store_t app)
Zeta.App.app_params Zeta.High.Thread.verifiable_log Zeta.High.Verifier.__proj__Mkvtls_t__item__st Zeta.GenericVerifier.__proj__Mkverifier_spec_base__item__vtls_t Zeta.High.Verifier.high_verifier_spec Zeta.Generic.Thread.state Zeta.High.Verifier.store_t
let store (#app: _) (tl: verifiable_log app) =
  
let vs = state tl in
vs.st