val valid : tsm: Zeta.Steel.ThreadStateModel.thread_state_model -> Prims.logical
let valid (tsm: thread_state_model)
  = U16.v tsm.thread_id < U32.v AT.n_threads /\
    tsm == run tsm.thread_id tsm.processed_entries /\
    not tsm.failed
module Zeta.Steel.ThreadRel

(* This module sets up the relationship between a steel verifier thread and a spec-level one *)

open Zeta.App
open Zeta.AppSimulate
open Zeta.Steel.KeyUtils
open Zeta.Steel.Rel
open Zeta.Steel.LogRel
open Zeta.Steel.StoreRel
open Zeta.Steel.MultiSetHash
open Zeta.Steel.ThreadStateModel
open Zeta.Steel.ThreadRelDef

module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module L = FStar.List.Tot
module GK = Zeta.GenKey
module K = Zeta.Key
module M = Zeta.Merkle
module GV = Zeta.GenericVerifier
module GT = Zeta.Generic.Thread
module IL = Zeta.Intermediate.Logs
module IV = Zeta.Intermediate.Verifier
module AT = Zeta.Steel.ApplicationTypes
module T = Zeta.Steel.FormatsManual
module TSM = Zeta.Steel.ThreadStateModel
module MS = Zeta.MultiSet

(* thread_state_model has some redundancy - for tsm's of interest, the state is obtained by
/
Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.ThreadRelDef.fst.checked Zeta.Steel.StoreRel.fsti.checked Zeta.Steel.Rel.fsti.checked Zeta.Steel.MultiSetHash.fsti.checked Zeta.Steel.LogRel.fsti.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Steel.ApplicationTypes.fsti.checked Zeta.MultiSet.fsti.checked Zeta.Merkle.fsti.checked Zeta.Key.fsti.checked Zeta.Intermediate.Verifier.fsti.checked Zeta.Intermediate.Thread.fsti.checked Zeta.Intermediate.Logs.fsti.checked Zeta.GenKey.fsti.checked Zeta.GenericVerifier.fsti.checked Zeta.Generic.Thread.fsti.checked Zeta.AppSimulate.fsti.checked Zeta.App.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked
Zeta.Steel.ThreadRel.fsti
tsm: Zeta.Steel.ThreadStateModel.thread_state_model -> Prims.logical
Zeta.Steel.ThreadStateModel.thread_state_model Prims.l_and Prims.b2t Prims.op_LessThan FStar.UInt16.v Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__thread_id FStar.UInt32.v Zeta.Steel.ApplicationTypes.n_threads Prims.eq2 Zeta.Steel.ThreadStateModel.run Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__processed_entries Prims.op_Negation Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__failed Prims.logical
let valid (tsm: thread_state_model) =
  
U16.v tsm.thread_id < U32.v AT.n_threads /\ tsm == run tsm.thread_id tsm.processed_entries /\
not tsm.failed