val addm_anc_key (a: addm_param{addm_precond1 a}) : GTot (T.internal_key)
val addm_anc_key (a: addm_param{addm_precond1 a}) : GTot (T.internal_key)
let addm_anc_key (a: addm_param {addm_precond1 a}): GTot (T.internal_key) =
  stored_base_key (addm_store_pre a) (addm_anc_slot a)
module Zeta.Steel.AddMRel

open Zeta.Steel.KeyUtils
open Zeta.Steel.ThreadStateModel
open Zeta.Steel.Rel
open Zeta.Steel.StoreRel
open Zeta.Steel.ThreadRelDef

module LT = Zeta.Steel.LogEntry.Types
module T = Zeta.Steel.FormatsManual
module SS = Zeta.Steel.StoreRel
module IV = Zeta.Intermediate.Verifier

(* steel-level addm param *)
noeq type addm_param =
  | AMP: s: s_slot_id ->
          p: s_record ->
          s': s_slot_id ->
          vs': s_thread_state -> addm_param

let addm_precond0 (a: addm_param)
  = match a with
    | AMP s p s' _ ->
    check_slot_bounds s /\
    check_slot_bounds s'

(* the key being added *)
let addm_key (a: addm_param {addm_precond0 a})
  = let AMP _ (gk,gv) _ _ = a in
    gk

let addm_base_key (a: addm_param {addm_precond0 a})
  = to_base_key (addm_key a)

(* slot where the record is being added *)
let addm_slot (a: addm_param) =
  match a with
  | AMP s _ _ _ -> s

(* the slot where the ancestore record is stored *)
let addm_anc_slot (a: addm_param) =
  match a with
  | AMP _ _ s' _ -> s'

(* the state of the store before the add *)
let addm_store_pre (a: addm_param) =
  match a with
  | AMP _ _ _ vs' ->  vs'.store

(* initial set of addm preconditions: vaddm fails if these are not met *)
let addm_precond1 (a: addm_param) =
  let st' = addm_store_pre a in
  let s = addm_slot a in
  let s' = addm_anc_slot a in
  addm_precond0 a /\
  s <> s' /\
  inuse_slot st' s' /\
  empty_slot st' s /\
  (let k' = stored_base_key st' s' in
   let gk = addm_key a in
   is_proper_descendent (to_base_key gk) k')

let addm_value_pre (a: addm_param {addm_precond1 a})  =
  match a with
  | AMP _ (gk,gv) _ _ -> gv

let addm_hash_val_pre (a: addm_param {addm_precond1 a}) =
  Zeta.Steel.HashValue.hashfn (addm_value_pre a)
/
Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.ThreadRelDef.fst.checked Zeta.Steel.StoreRel.fsti.checked Zeta.Steel.Rel.fsti.checked Zeta.Steel.LogEntry.Types.fst.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.HashValue.fsti.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Intermediate.Verifier.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked
Zeta.Steel.AddMRel.fsti
a: Zeta.Steel.AddMRel.addm_param{Zeta.Steel.AddMRel.addm_precond1 a}
  -> Prims.GTot Zeta.Steel.KeyUtils.internal_key
Zeta.Steel.AddMRel.addm_param Zeta.Steel.AddMRel.addm_precond1 Zeta.Steel.StoreRel.stored_base_key Zeta.Steel.AddMRel.addm_store_pre Zeta.Steel.AddMRel.addm_anc_slot Zeta.Steel.KeyUtils.internal_key
let addm_anc_key (a: addm_param{addm_precond1 a}) : GTot (T.internal_key) =
  
stored_base_key (addm_store_pre a) (addm_anc_slot a)