val addm_precond0 : a: Zeta.Steel.AddMRel.addm_param -> Prims.logical
let addm_precond0 (a: addm_param)
  = match a with
    | AMP s p s' _ ->
    check_slot_bounds s /\
    check_slot_bounds s'
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
/
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 -> Prims.logical
Zeta.Steel.AddMRel.addm_param Zeta.Steel.Rel.s_slot_id Zeta.Steel.Rel.s_record Zeta.Steel.Rel.s_thread_state Prims.l_and Prims.b2t Zeta.Steel.ThreadStateModel.check_slot_bounds Prims.logical
let addm_precond0 (a: addm_param) =
  
match a with | AMP s p s' _ -> check_slot_bounds s /\ check_slot_bounds s'