val addm_anc_points_null : a: Zeta.Steel.AddMRel.addm_param{Zeta.Steel.AddMRel.addm_precond2 a} -> Prims.GTot Prims.bool
let addm_anc_points_null (a: addm_param {addm_precond2 a}) =
  mv_points_to_none (addm_anc_val_pre a) (addm_dir 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)

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)

let addm_anc_val_pre (a: addm_param {addm_precond1 a}) =
  let st' = addm_store_pre a in
  let s' = addm_anc_slot a in
  let Some mv = to_merkle_value (stored_value st' s') in
  mv

let addm_dir (a: addm_param {addm_precond1 a}) =
  desc_dir (addm_base_key a) (addm_anc_key a)

let mv_points_to_none (mv: T.mval_value) (d: bool)
  = T.Dh_vnone? (desc_hash_dir mv d)

let mv_points_to_some (v:T.mval_value) (d:bool): bool =
  T.Dh_vsome? (desc_hash_dir v d)

let mv_pointed_key (v:T.mval_value) (d: bool{mv_points_to_some v d}): T.base_key =
  let T.Dh_vsome dh = desc_hash_dir v d in
  dh.dhd_key

let mv_pointed_hash (v:T.mval_value) (d: bool{mv_points_to_some v d}): T.hash_value =
  let T.Dh_vsome dh = desc_hash_dir v d in
  dh.dhd_h

let mv_points_to (v:T.mval_value) (d:bool) (k:T.base_key) =
  mv_points_to_some v d /\
  mv_pointed_key v d == k

let mv_evicted_to_blum (v: T.mval_value) (d: bool {mv_points_to_some v d})
  = let T.Dh_vsome dh = desc_hash_dir v d in
    dh.evicted_to_blum = T.Vtrue

let addm_precond2 (a: addm_param) =
  addm_precond1 a /\
  (let mv' = addm_anc_val_pre a in
   let d = addm_dir a in
   mv_points_to_none mv' d \/                          // case A: ancestor points to nothing along d
   mv_points_to mv' d (addm_base_key a) \/                  // case B: ancestor points to key being added
   is_proper_descendent (mv_pointed_key mv' d) (addm_base_key a)) // case C: ancestor points to some key below key being added
/
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_precond2 a} -> Prims.GTot Prims.bool
Zeta.Steel.AddMRel.addm_param Zeta.Steel.AddMRel.addm_precond2 Zeta.Steel.AddMRel.mv_points_to_none Zeta.Steel.AddMRel.addm_anc_val_pre Zeta.Steel.AddMRel.addm_dir Prims.bool
let addm_anc_points_null (a: addm_param{addm_precond2 a}) =
  
mv_points_to_none (addm_anc_val_pre a) (addm_dir a)