val update_value
  (#vcfg:_)
  (st:vstore vcfg)
  (s:inuse_slot_id st)
  (v:value vcfg.app {compatible (stored_key st s) v})
  : Tot (st':vstore vcfg {identical_except st st' s /\
                          inuse_slot st' s /\
                          (let VStoreE (k1,_) am1 ld1 rd1 p1 = get_inuse_slot st s in
                           let VStoreE (k2,v2) am2 ld2 rd2 p2 = get_inuse_slot st' s in
                           k1 = k2 /\ am1 = am2 /\ ld1 = ld2 /\ rd1 = rd2 /\ p1 = p2 /\ v2 = v)})
val update_value
  (#vcfg:_)
  (st:vstore vcfg)
  (s:inuse_slot_id st)
  (v:value vcfg.app {compatible (stored_key st s) v})
  : Tot (st':vstore vcfg {identical_except st st' s /\
                          inuse_slot st' s /\
                          (let VStoreE (k1,_) am1 ld1 rd1 p1 = get_inuse_slot st s in
                           let VStoreE (k2,v2) am2 ld2 rd2 p2 = get_inuse_slot st' s in
                           k1 = k2 /\ am1 = am2 /\ ld1 = ld2 /\ rd1 = rd2 /\ p1 = p2 /\ v2 = v)})
let update_value
  (#vcfg:_)
  (st:vstore vcfg)
  (s:inuse_slot_id st)
  (v:value vcfg.app {compatible (stored_key st s) v})
  : Tot (st':vstore vcfg {identical_except st st' s /\
                          inuse_slot st' s /\
                          (let VStoreE (k1,_) am1 ld1 rd1 p1 = get_inuse_slot st s in
                           let VStoreE (k2,v2) am2 ld2 rd2 p2 = get_inuse_slot st' s in
                           k1 = k2 /\ am1 = am2 /\ ld1 = ld2 /\ rd1 = rd2 /\ p1 = p2 /\ v2 = v)})
  = let uvp = UVP st s v in
    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

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)]
  = ()

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
  ()

let lemma_parent_props_update_val #vcfg uvp
  : Lemma (ensures (parent_props (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
    : Lemma (ensures (parent_props_local stn s1))
            [SMTPat (parent_props_local stn s1)] =
    assert(parent_props_local stp s1);
    ()
  in
  ()

let lemma_madd_props_update_val #vcfg uvp
  : Lemma (ensures (madd_props (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
    : Lemma (ensures (madd_props_local stn s1))
            [SMTPat (madd_props_local stn s1)] =
    assert(madd_props_local stp s1);
    ()
  in
  ()

let lemma_no_self_edge_update_val #vcfg uvp
  : Lemma (ensures (no_self_edge (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
    : Lemma (ensures (no_self_edge_local stn s1))
            [SMTPat (no_self_edge_local stn s1)] =
    assert(no_self_edge_local stp s1);
    ()
  in
  ()
/
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 vcfg ->
    s: Zeta.Intermediate.Store.inuse_slot_id st ->
    v:
      Zeta.Record.value (VConfig?.app vcfg)
        {Zeta.Record.compatible (Zeta.Intermediate.Store.stored_key st s) v}
  -> st':
    Zeta.Intermediate.Store.vstore vcfg
      { Zeta.Intermediate.Store.identical_except st st' s /\
        Zeta.Intermediate.Store.inuse_slot st' s /\
        (let _ = Zeta.Intermediate.Store.get_inuse_slot st s in
          (let
            Zeta.Intermediate.Store.VStoreE
              #_
              (FStar.Pervasives.Native.Mktuple2 #_ #_ k1 _)
              am1
              ld1
              rd1
              p1 =
              _
            in
            let _ = Zeta.Intermediate.Store.get_inuse_slot st' s in
            (let
              Zeta.Intermediate.Store.VStoreE
                #_
                (FStar.Pervasives.Native.Mktuple2 #_ #_ k2 v2)
                am2
                ld2
                rd2
                p2 =
                _
              in
              k1 = k2 /\ am1 = am2 /\ ld1 = ld2 /\ rd1 = rd2 /\ p1 = p2 /\ v2 = v)
            <:
            Prims.logical)
          <:
          Prims.logical) }
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Store.vstore Zeta.Intermediate.Store.inuse_slot_id Zeta.Record.value Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__app Prims.b2t Zeta.Record.compatible Zeta.Intermediate.Store.stored_key Zeta.Intermediate.Store.apply_update_val Zeta.Intermediate.Store.update_val_param Zeta.Intermediate.Store.UVP Prims.l_and Zeta.Intermediate.Store.identical_except Zeta.Intermediate.Store.inuse_slot Zeta.GenKey.key Zeta.Intermediate.Store.add_method FStar.Pervasives.Native.option Zeta.Intermediate.VerifierConfig.slot_id FStar.Pervasives.Native.tuple2 Zeta.BinTree.bin_tree_dir Prims.op_Equality Prims.logical Zeta.Intermediate.Store.vstore_entry Zeta.Intermediate.Store.get_inuse_slot
let update_value
      (#vcfg: _)
      (st: vstore vcfg)
      (s: inuse_slot_id st)
      (v: value vcfg.app {compatible (stored_key st s) v})
    : Tot
    (st':
      vstore vcfg
        { identical_except st st' s /\ inuse_slot st' s /\
          (let VStoreE (k1, _) am1 ld1 rd1 p1 = get_inuse_slot st s in
            let VStoreE (k2, v2) am2 ld2 rd2 p2 = get_inuse_slot st' s in
            k1 = k2 /\ am1 = am2 /\ ld1 = ld2 /\ rd1 = rd2 /\ p1 = p2 /\ v2 = v) }) =
  
let uvp = UVP st s v in
apply_update_val uvp