val compatible : k: Zeta.Key.base_key -> r: Zeta.Record.record aprm -> Prims.bool
let compatible #aprm (k:base_key) (r:record aprm)
  = let kr,_ = r in
    to_base_key kr = 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 *)
/
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
k: Zeta.Key.base_key -> r: Zeta.Record.record aprm -> Prims.bool
Zeta.App.app_params Zeta.Key.base_key Zeta.Record.record Zeta.GenKey.key Zeta.Record.value Prims.op_Equality Zeta.GenKey.to_base_key Prims.bool
let compatible #aprm (k: base_key) (r: record aprm) =
  
let kr, _ = r in
to_base_key kr = k