val lemma_points_to_inuse_update_val (#vcfg uvp: _)
    : Lemma (ensures (points_to_inuse (uvp_store_post uvp))) [SMTPat (apply_update_val #vcfg uvp)]
val lemma_points_to_inuse_update_val (#vcfg uvp: _)
    : Lemma (ensures (points_to_inuse (uvp_store_post uvp))) [SMTPat (apply_update_val #vcfg uvp)]
let lemma_points_to_inuse_update_val #vcfg uvp
  : Lemma (ensures (points_to_inuse (uvp_store_post uvp)))
          [SMTPat (apply_update_val #vcfg uvp)] =
  let stp = uvp_store_pre uvp in
  let stn = uvp_store_post uvp in
  let aux s1 s2
    : Lemma (ensures (points_to_inuse_local stn s1 s2))
            [SMTPat (points_to_inuse_local stn s1 s2)] =
    assert(points_to_inuse_local stp s1 s2);
    ()
  in
  ()
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

let uvp_store_post #vcfg (uvp: update_val_param vcfg) =
  apply_update_val uvp


///  The edges are unchanged after update value
///
let uvp_edges_unchanged #vcfg uvp e
  : Lemma (is_edge (uvp_store_pre #vcfg uvp) e =
           is_edge (uvp_store_post uvp) e) = ()

///  Each slot except the updated slot remains unchanged
///
let uvp_identical_except #vcfg uvp
  : Lemma (ensures (identical_except (uvp_store_pre uvp) (uvp_store_post uvp) (uvp_slot uvp)))
          [SMTPat (apply_update_val #vcfg 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
  -> FStar.Pervasives.Lemma
      (ensures Zeta.Intermediate.Store.points_to_inuse (Zeta.Intermediate.Store.uvp_store_post uvp))
      [SMTPat (Zeta.Intermediate.Store.apply_update_val uvp)]
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Store.update_val_param Zeta.Intermediate.VerifierConfig.slot_id Prims.unit Prims.l_True Prims.squash Zeta.Intermediate.Store.points_to_inuse_local Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.logical Prims.Nil Prims._assert Zeta.Intermediate.Store.vstore_raw Zeta.Intermediate.Store.uvp_store_post Zeta.Intermediate.Store.vstore Zeta.Intermediate.Store.uvp_store_pre Zeta.Intermediate.Store.points_to_inuse Zeta.Intermediate.Store.apply_update_val
let lemma_points_to_inuse_update_val #vcfg uvp
    : Lemma (ensures (points_to_inuse (uvp_store_post uvp))) [SMTPat (apply_update_val #vcfg uvp)] =
  
let stp = uvp_store_pre uvp in
let stn = uvp_store_post uvp in
let aux s1 s2
    : Lemma (ensures (points_to_inuse_local stn s1 s2)) [SMTPat (points_to_inuse_local stn s1 s2)] =
  assert (points_to_inuse_local stp s1 s2);
  ()
in
()