val madd_props : st: Zeta.Intermediate.Store.vstore_raw vcfg -> Prims.logical
let madd_props #vcfg (st: vstore_raw vcfg) =
  forall s. {:pattern madd_props_local st s} madd_props_local st s
module Zeta.Intermediate.Store

open Zeta.BinTree
open Zeta.App
open Zeta.Key
open Zeta.GenKey
open Zeta.Record
open Zeta.SeqAux
open Zeta.Intermediate.VerifierConfig
open Zeta.Intermediate.SlotKeyRel

module Spec = Zeta.High.Verifier
module GV = Zeta.GenericVerifier
module Merkle = Zeta.Merkle

(*** General Definitions & Basic Facts ***)

let add_method = Zeta.High.Verifier.add_method

(*
 * vstore_entry - reflect a Spec.vstore_entry with two additional fields tracking
 * whether a left/right descendant was added using merkle using this slot as "proof"
 *)
type vstore_entry (vcfg:verifier_config)  =
  | VStoreE: r:record vcfg.app ->
             am:add_method ->
             l_in_store : option (slot_id vcfg) ->
             r_in_store : option (slot_id vcfg) ->
             p: option (slot_id vcfg & bin_tree_dir) ->                     (* parent slot *)
             vstore_entry vcfg

(* vstore_raw: the raw version of the vstore; the actual vstore
 * is the raw version with some invariants *)
let vstore_raw vcfg = st:Seq.seq (option (vstore_entry vcfg)){Seq.length st = store_size vcfg}

let get_slot #vcfg (st:vstore_raw vcfg) (s: slot_id vcfg)
  : option (vstore_entry vcfg)
  = Seq.index st s

(* return true if s is a valid slot that is occupied *)
let inuse_slot #vcfg (st:vstore_raw vcfg) (s:slot_id vcfg) : bool
  = Some? (get_slot st s)

(* dep type of all slots in use *)
let inuse_slot_id #vcfg (st: vstore_raw vcfg) = s:slot_id vcfg{inuse_slot st s}

let get_inuse_slot #vcfg (st:vstore_raw vcfg) (s:inuse_slot_id st) =
  Some?.v (get_slot st s)

(* is this an empty slot *)
let empty_slot #vcfg (st:vstore_raw vcfg) (s:slot_id vcfg): bool
  = not (inuse_slot st s)

let empty_slot_id #vcfg (st: vstore_raw vcfg) = s:slot_id vcfg{empty_slot st s}

(* key stored at an occupied slot *)
let stored_key #vcfg (st:vstore_raw vcfg) (s:inuse_slot_id st) : key vcfg.app
  = key_of (VStoreE?.r (Some?.v (get_slot st s)))

let stored_record #vcfg (st: vstore_raw vcfg) (s: inuse_slot_id st)
  : record vcfg.app
  = VStoreE?.r (Some?.v (get_slot st s))

let stored_base_key #vcfg (st: vstore_raw vcfg) (s:inuse_slot_id st) : base_key
  = to_base_key (stored_key st s)

(* is this a slot containing a merkle key *)
let merkle_slot_id #vcfg (st:vstore_raw vcfg)
  = s:inuse_slot_id st{IntK? (stored_key st s)}

let data_slot_id #vcfg (st:vstore_raw vcfg)
  = s:inuse_slot_id st{AppK? (stored_key st s)}

let stored_value #vcfg (st:vstore_raw vcfg) (s:inuse_slot_id st) : value vcfg.app
  = value_of (VStoreE?.r (Some?.v (get_slot st s)))

let add_method_of #vcfg (st:vstore_raw vcfg) (s:inuse_slot_id st) : add_method
  = VStoreE?.am (Some?.v (get_slot st s))

let points_to_info #vcfg (st:vstore_raw vcfg) (s:inuse_slot_id st) (d:bin_tree_dir) =
  match d with
  | Left -> VStoreE?.l_in_store (Some?.v (get_slot st s))
  | Right -> VStoreE?.r_in_store (Some?.v (get_slot st s))

(* does the slot point to some slot along a direction *)
let points_to_some_slot #vcfg (st:vstore_raw vcfg) (s: inuse_slot_id st) (d:bin_tree_dir): bool =
  Some? (points_to_info st s d)

let points_to_none #vcfg (st: vstore_raw vcfg) (s: inuse_slot_id st) (d: bin_tree_dir): bool =
  None? (points_to_info st s d)

let pointed_slot #vcfg (st:vstore_raw vcfg) (s:inuse_slot_id st) (d:bin_tree_dir{points_to_some_slot st s d}): slot_id vcfg
  = Some?.v (points_to_info st s d)

let points_to_dir #vcfg (st:vstore_raw vcfg) (s1: slot_id vcfg) (d:bin_tree_dir) (s2: slot_id vcfg) =
  inuse_slot st s1 &&
  points_to_some_slot st s1 d && pointed_slot st s1 d = s2

(* points to relation of slots *)
let points_to #vcfg (st:vstore_raw vcfg) (s1:slot_id vcfg) (s2:slot_id vcfg) =
  points_to_dir st s1 Left s2 ||
  points_to_dir st s1 Right s2

(* the point of this trivial lemma is to trigger the SMTPat below; TODO: is their an idiomatically better way? *)
let lemma_points_to_dir_implies_points_to #vcfg (st:vstore_raw vcfg) (s1: slot_id vcfg) (d:bin_tree_dir) (s2: slot_id vcfg):
  Lemma (requires (points_to_dir st s1 d s2))
        (ensures (points_to st s1 s2))
        [SMTPat (points_to_dir st s1 d s2)] = ()

let parent_info #vcfg st s =
  VStoreE?.p (get_inuse_slot #vcfg st s)

(* does the slot s have a parent pointing to it *)
let has_parent #vcfg st s =
  Some? (parent_info #vcfg st s)

(* parent of slot s *)
let parent_slot #vcfg (st: vstore_raw vcfg) (s: inuse_slot_id st{has_parent st s}): slot_id vcfg =
  fst (Some?.v (parent_info #vcfg st s))

let parent_dir #vcfg (st: vstore_raw vcfg) (s: inuse_slot_id st{has_parent st s}): bin_tree_dir =
  snd (Some?.v (parent_info #vcfg st s))

(* if I have a parent, I should have been added with MAdd and the parent points to me *)
let parent_props_local #vcfg (st: vstore_raw vcfg) (s: slot_id vcfg) =
  inuse_slot st s ==>
  has_parent st s ==>
  (add_method_of st s = Spec.MAdd /\ points_to_dir st (parent_slot st s) (parent_dir st s) s)

(* parent implies madd holds for all slots in the store *)
let parent_props #vcfg (st: vstore_raw vcfg) =
  forall (s: slot_id vcfg). {:pattern parent_props_local st s} parent_props_local st s

(* a pointed slot is inuse *)
let points_to_inuse_local #vcfg (st:vstore_raw vcfg) (s1 s2: slot_id _) =
  (points_to_dir st s1 Left s2 ==> (inuse_slot st s2 /\ add_method_of st s2 = Spec.MAdd /\
                                  has_parent st s2 /\ parent_slot st s2 = s1 /\ parent_dir st s2 = Left)) /\
  (points_to_dir st s1 Right s2 ==> (inuse_slot st s2 /\ add_method_of st s2 = Spec.MAdd /\
                                    has_parent st s2 /\ parent_slot st s2 = s1 /\ parent_dir st s2 = Right))

let points_to_inuse #vcfg (st:vstore_raw vcfg) =
  forall (s1 s2: slot_id _). {:pattern (points_to_inuse_local st s1 s2) \/ (points_to st s1 s2)} points_to_inuse_local st s1 s2

let no_self_edge_local #vcfg (st: vstore_raw vcfg) (s: slot_id vcfg) =
  not (points_to st s s)

let no_self_edge #vcfg (st:vstore_raw vcfg) =
  forall s. {:pattern no_self_edge_local st s} no_self_edge_local st s

let madd_props_local #vcfg (st: vstore_raw vcfg) (s: slot_id vcfg) =
  inuse_slot st s ==>
  add_method_of st s = Spec.MAdd ==>
  stored_base_key st s <> Root ==>
  has_parent st s
/
Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.Merkle.fsti.checked Zeta.Key.fsti.checked Zeta.Intermediate.VerifierConfig.fsti.checked Zeta.Intermediate.SlotKeyRel.fsti.checked Zeta.High.Verifier.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.BinTree.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.Intermediate.Store.fsti
st: Zeta.Intermediate.Store.vstore_raw vcfg -> Prims.logical
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Store.vstore_raw Prims.l_Forall Zeta.Intermediate.VerifierConfig.slot_id Zeta.Intermediate.Store.madd_props_local Prims.logical
let madd_props #vcfg (st: vstore_raw vcfg) =
  
forall s. {:pattern madd_props_local st s} madd_props_local st s