val store_post : tl: Zeta.High.Thread.verifiable_log app -> i: Zeta.Generic.Thread.seq_index tl
  -> Prims.GTot (Zeta.High.Verifier.store_t app)
let store_post (#app:_) (tl: verifiable_log app) (i: seq_index tl)
  = let tl' = prefix tl (i+1) in
    store tl'
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)

let store (#app:_) (tl: verifiable_log app)
  = let vs = state tl in
    vs.st

let store_pre (#app:_) (tl: verifiable_log app) (i: seq_index tl)
  = let tl' = prefix tl i in
    store tl'
/
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 -> i: Zeta.Generic.Thread.seq_index tl
  -> Prims.GTot (Zeta.High.Verifier.store_t app)
Zeta.App.app_params Zeta.High.Thread.verifiable_log Zeta.Generic.Thread.seq_index Zeta.High.Verifier.high_verifier_spec Zeta.High.Thread.store Zeta.Generic.Thread.verifiable_log Prims.b2t Prims.op_Equality Prims.nat Zeta.Generic.Thread.length Prims.op_Addition Zeta.Generic.Thread.prefix Zeta.High.Verifier.store_t
let store_post (#app: _) (tl: verifiable_log app) (i: seq_index tl) =
  
let tl' = prefix tl (i + 1) in
store tl'