val pointed_dir : st: Zeta.Intermediate.Store.vstore_raw vcfg ->
    s1: Zeta.Intermediate.VerifierConfig.slot_id vcfg ->
    s2: Zeta.Intermediate.VerifierConfig.slot_id vcfg {Zeta.Intermediate.Store.points_to st s1 s2}
  -> Zeta.BinTree.bin_tree_dir
let pointed_dir #vcfg (st: vstore_raw vcfg) s1 (s2: slot_id vcfg { points_to st s1 s2}) =
  if points_to_dir st s1 Left s2 then Left else Right
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
  ()

(* update a value of a key *)
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

noeq type madd_param (vcfg: verifier_config) =
  | MAP:   st: vstore vcfg ->
           s:empty_slot_id st ->
           r:record vcfg.app ->
           s':merkle_slot_id st ->
           d:bin_tree_dir {points_to_none st s' d} -> madd_param vcfg

let map_slot #vcfg (map: madd_param vcfg) =
  MAP?.s map

let map_record #vcfg (map: madd_param vcfg) =
  MAP?.r map

let map_dir #vcfg (map: madd_param vcfg) =
  MAP?.d map

let map_anc_slot #vcfg (map: madd_param vcfg) =
  MAP?.s' map

let apply_map #vcfg (map: madd_param vcfg) =
  match map with
  | MAP st s r s' d ->
    let p = (map_anc_slot map), (map_dir map) in
    let e = VStoreE r Spec.MAdd None None (Some p) in
    let st = update_slot st s e in
    let VStoreE r' am' ld' rd' p' = get_inuse_slot st s' in
    assert(None == (if d = Left then ld' else rd'));

    if d = Left then
      update_slot st s' (VStoreE r' am' (Some s) rd' p')
    else
      update_slot st s' (VStoreE r' am' ld' (Some s) p')

let map_store_pre #vcfg (map: madd_param vcfg) =
  MAP?.st map

let map_store_post #vcfg map =
  apply_map #vcfg map

///  The new edge added by the map
///
let map_new_edge #vcfg (map: madd_param vcfg): sds vcfg =
  (map_anc_slot map), (map_dir map), (map_slot map)

///  All slots except the two referenced slot in madd are unaffected by the operation
///
let map_identical_except #vcfg map
  : Lemma (ensures (identical_except2 (map_store_pre map) (map_store_post map)
                                      (map_slot map) (map_anc_slot map)))
          [SMTPat (apply_map #vcfg map)] = ()

///  Every edge in the store before madd is in the store after
///
let map_pre_edges_in_post #vcfg map e
  : Lemma (requires (is_edge (map_store_pre #vcfg map) e))
          (ensures (is_edge (map_store_post map) e)) = ()

///  Every edge in post except for the new edge is in pre
///
let map_post_edge_in_pre #vcfg map e
  : Lemma (requires (e <> map_new_edge #vcfg map /\
                     is_edge (map_store_post map) e))
          (ensures (is_edge (map_store_pre map) 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

    st: Zeta.Intermediate.Store.vstore_raw vcfg ->
    s1: Zeta.Intermediate.VerifierConfig.slot_id vcfg ->
    s2: Zeta.Intermediate.VerifierConfig.slot_id vcfg {Zeta.Intermediate.Store.points_to st s1 s2}
  -> Zeta.BinTree.bin_tree_dir
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Store.vstore_raw Zeta.Intermediate.VerifierConfig.slot_id Prims.b2t Zeta.Intermediate.Store.points_to Zeta.Intermediate.Store.points_to_dir Zeta.BinTree.Left Prims.bool Zeta.BinTree.Right Zeta.BinTree.bin_tree_dir
let pointed_dir #vcfg (st: vstore_raw vcfg) s1 (s2: slot_id vcfg {points_to st s1 s2}) =
  
if points_to_dir st s1 Left s2 then Left else Right