val sds : vcfg: Zeta.Intermediate.VerifierConfig.verifier_config -> Type0
let sds vcfg = slot_id vcfg & bin_tree_dir & slot_id vcfg
module Zeta.Intermediate.Store

open FStar.Classical

let update_slot #vcfg (st:vstore_raw vcfg) (s:slot_id vcfg) (e:vstore_entry vcfg)
  : vstore_raw _
  = Seq.upd st s (Some e)
/
Zeta.SeqAux.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked
Zeta.Intermediate.Store.fst
vcfg: Zeta.Intermediate.VerifierConfig.verifier_config -> Type0
Zeta.Intermediate.VerifierConfig.verifier_config FStar.Pervasives.Native.tuple3 Zeta.Intermediate.VerifierConfig.slot_id Zeta.BinTree.bin_tree_dir
let sds vcfg =
  
slot_id vcfg & bin_tree_dir & slot_id vcfg