val add_to_store (#aprm: app_params) (st: store_t aprm) (r: record aprm) (am: add_method)
    : (st':
      store_t aprm
        { let k, v = r in
          let k = to_base_key k in
          store_contains st' k /\ stored_value st' k = v })
val add_to_store (#aprm: app_params) (st: store_t aprm) (r: record aprm) (am: add_method)
    : (st':
      store_t aprm
        { let k, v = r in
          let k = to_base_key k in
          store_contains st' k /\ stored_value st' k = v })
let add_to_store (#aprm: app_params)
                 (st:store_t aprm)
                 (r: record aprm)
                 (am:add_method):
  (st':store_t aprm {let k,v = r in
                     let k = to_base_key k in
                     store_contains st' k /\ stored_value st' k = v})
  = let k,_ = r in
    let k = to_base_key k in
    fun k' -> if k' = k then Some ({ r; am }) else st k'
module Zeta.High.Verifier

open Zeta.App
open Zeta.Time
open Zeta.Thread
open Zeta.Key
open Zeta.GenKey
open Zeta.Record
open Zeta.HashFunction

module S = FStar.Seq
module SA = Zeta.SeqAux
module GV = Zeta.GenericVerifier
module T = Zeta.Time

(* for records in the store, how were they added? *)
type add_method =
  | MAdd: add_method       (* AddM *)
  | BAdd: add_method         (* AddB *)

let compatible #aprm (k:base_key) (r:record aprm)
  = let kr,_ = r in
    to_base_key kr = k

(* verifier store entry indexed by a key k *)
type vstore_entry (aprm: app_params) (k:base_key) = {
  r:  r:record aprm {compatible k r};
  am: add_method;
}

(* verifier store is a subset of (k,v) records *)
(* we also track how the key was added merkle/blum *)
let store_t (aprm: app_params) = (k:base_key) -> option (vstore_entry aprm k)

(* does the store contain a key *)
let store_contains (#aprm: app_params) (st:store_t aprm) (k:base_key)
  = Some? (st k)

(* lookup the value of a key in the store *)
let stored_value (#aprm: app_params) (st:store_t aprm) (k:base_key {store_contains st k})
  = let _, v = (Some?.v (st k)).r in
    v

let stored_key (#aprm: app_params) (st:store_t aprm) (k:base_key {store_contains st k})
  = let k, _ = (Some?.v (st k)).r in
    k

(* add method of a key in the store *)
let add_method_of (#aprm: app_params) (st:store_t aprm) (k:base_key {store_contains st k})
  = (Some?.v (st k)).am

(* update the store *)
let update_store (#aprm: app_params)
                 (st:store_t aprm)
                 (k:base_key {store_contains st k})
                 (r:record aprm {compatible k r}):
  Tot (st':store_t aprm {store_contains st' k /\ stored_value st' k = (value_of r)})
  = let am = add_method_of st k in
    fun k' -> if k' = k then Some ( { r; am } ) else st k'
/
Zeta.TimeKey.fsti.checked Zeta.Time.fsti.checked Zeta.Thread.fsti.checked Zeta.SeqIdx.fsti.checked Zeta.SeqAux.fsti.checked Zeta.Record.fsti.checked Zeta.Merkle.fsti.checked Zeta.Key.fsti.checked Zeta.HashFunction.fsti.checked Zeta.Hash.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.High.Verifier.fsti

    st: Zeta.High.Verifier.store_t aprm ->
    r: Zeta.Record.record aprm ->
    am: Zeta.High.Verifier.add_method
  -> st':
    Zeta.High.Verifier.store_t aprm
      { let _ = r in
        (let FStar.Pervasives.Native.Mktuple2 #_ #_ k v = _ in
          let k = Zeta.GenKey.to_base_key k in
          Zeta.High.Verifier.store_contains st' k /\ Zeta.High.Verifier.stored_value st' k = v)
        <:
        Type0 }
Zeta.App.app_params Zeta.High.Verifier.store_t Zeta.Record.record Zeta.High.Verifier.add_method Zeta.GenKey.key Zeta.Record.value Zeta.Key.base_key Prims.op_Equality FStar.Pervasives.Native.Some Zeta.High.Verifier.vstore_entry Zeta.High.Verifier.Mkvstore_entry Prims.bool FStar.Pervasives.Native.option Zeta.GenKey.to_base_key Prims.l_and Prims.b2t Zeta.High.Verifier.store_contains Zeta.High.Verifier.stored_value
let add_to_store (#aprm: app_params) (st: store_t aprm) (r: record aprm) (am: add_method)
    : (st':
      store_t aprm
        { let k, v = r in
          let k = to_base_key k in
          store_contains st' k /\ stored_value st' k = v }) =
  
let k, _ = r in
let k = to_base_key k in
fun k' -> if k' = k then Some ({ r = r; am = am }) else st k'