val stored_record (#vcfg: _) (st: vstore_raw vcfg) (s: inuse_slot_id st) : record vcfg.app
val stored_record (#vcfg: _) (st: vstore_raw vcfg) (s: inuse_slot_id st) : record vcfg.app
let stored_record #vcfg (st: vstore_raw vcfg) (s: inuse_slot_id st)
  : record vcfg.app
  = VStoreE?.r (Some?.v (get_slot 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)))
/
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 -> s: Zeta.Intermediate.Store.inuse_slot_id st
  -> Zeta.Record.record (VConfig?.app vcfg)
Zeta.Intermediate.VerifierConfig.verifier_config Zeta.Intermediate.Store.vstore_raw Zeta.Intermediate.Store.inuse_slot_id Zeta.Intermediate.Store.__proj__VStoreE__item__r FStar.Pervasives.Native.__proj__Some__item__v Zeta.Intermediate.Store.vstore_entry Zeta.Intermediate.Store.get_slot Zeta.Record.record Zeta.Intermediate.VerifierConfig.__proj__VConfig__item__app
let stored_record #vcfg (st: vstore_raw vcfg) (s: inuse_slot_id st) : record vcfg.app =
  
VStoreE?.r (Some?.v (get_slot st s))