val is_edge : st: Zeta.Intermediate.Store.vstore_raw vcfg -> e: Zeta.Intermediate.Store.sds vcfg -> Prims.bool
let is_edge #vcfg st (e:sds vcfg) =
  let s1,d,s2 = e in
  inuse_slot st s1 && points_to_dir st s1 d s2
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)

let sds vcfg = slot_id vcfg & bin_tree_dir & slot_id vcfg
/
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
st: Zeta.Intermediate.Store.vstore_raw vcfg -> e: Zeta.Intermediate.Store.sds vcfg -> Prims.bool
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Store.vstore_raw Zeta.Intermediate.Store.sds Zeta.Intermediate.VerifierConfig.slot_id Zeta.BinTree.bin_tree_dir Prims.op_AmpAmp Zeta.Intermediate.Store.inuse_slot Zeta.Intermediate.Store.points_to_dir Prims.bool
let is_edge #vcfg st (e: sds vcfg) =
  
let s1, d, s2 = e in
inuse_slot st s1 && points_to_dir st s1 d s2