val uvp_store_post : uvp: Zeta.Intermediate.Store.update_val_param vcfg -> Zeta.Intermediate.Store.vstore_raw vcfg
let uvp_store_post #vcfg (uvp: update_val_param vcfg) =
  apply_update_val uvp
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

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

noeq type update_val_param (vcfg: verifier_config) =
  | UVP: st: vstore vcfg ->
         s: inuse_slot_id st ->
         v: value vcfg.app {compatible (stored_key st s) v} -> update_val_param vcfg

let uvp_slot #vcfg (uvp: update_val_param vcfg): slot_id vcfg =
  UVP?.s uvp

let uvp_val #vcfg (uvp: update_val_param vcfg) =
  UVP?.v uvp

let apply_update_val #vcfg (uvp: update_val_param vcfg) =
  match uvp with
  | UVP st s v ->
    let VStoreE (k,v') am lp rp p = get_inuse_slot st s in
    let e' = VStoreE (k,v) am lp rp p in
    update_slot st s e'

let uvp_store_pre #vcfg (uvp: update_val_param vcfg) =
  UVP?.st uvp
/
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
uvp: Zeta.Intermediate.Store.update_val_param vcfg -> Zeta.Intermediate.Store.vstore_raw vcfg
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Store.update_val_param Zeta.Intermediate.Store.apply_update_val Zeta.Intermediate.Store.vstore_raw
let uvp_store_post #vcfg (uvp: update_val_param vcfg) =
  
apply_update_val uvp