val addm_base_key : a: Zeta.Steel.AddMRel.addm_param{Zeta.Steel.AddMRel.addm_precond0 a}
  -> Prims.GTot Zeta.Steel.KeyUtils.base_key
let addm_base_key (a: addm_param {addm_precond0 a})
  = to_base_key (addm_key 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
/
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_precond0 a}
  -> Prims.GTot Zeta.Steel.KeyUtils.base_key
Zeta.Steel.AddMRel.addm_param Zeta.Steel.AddMRel.addm_precond0 Zeta.Steel.ThreadStateModel.to_base_key Zeta.Steel.AddMRel.addm_key Zeta.Steel.KeyUtils.base_key
let addm_base_key (a: addm_param{addm_precond0 a}) =
  
to_base_key (addm_key a)