val valid_tsm : Type0
let valid_tsm = tsm: thread_state_model { valid tsm }
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
 * running the log from an initial state. *)
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
/
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
Type0
Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.ThreadRel.valid
let valid_tsm =
  
tsm: thread_state_model{valid tsm}