val fail (#tsm: M.thread_state_model) (t: thread_state_t)
    : STT unit (thread_state_inv_core t tsm) (fun _ -> thread_state_inv_core t (M.fail tsm))
val fail (#tsm: M.thread_state_model) (t: thread_state_t)
    : STT unit (thread_state_inv_core t tsm) (fun _ -> thread_state_inv_core t (M.fail tsm))
let fail (#tsm:M.thread_state_model)
         (t:thread_state_t)
  : STT unit
    (thread_state_inv_core t tsm)
    (fun _ -> thread_state_inv_core t (M.fail tsm))
  = R.write t.failed true
module Zeta.Steel.VerifierSteps
friend Zeta.Steel.VerifierTypes
open Zeta.Steel.VerifierTypes
open FStar.Ghost
open Steel.ST.Util
module G = Steel.ST.GhostReference
module R = Steel.ST.Reference
module A = Steel.ST.Array
module Lock = Steel.ST.CancellableSpinLock
module TLM = Zeta.Steel.ThreadLogMap
open Zeta.Steel.ApplicationTypes
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
open Zeta.Steel.LogEntry
open Zeta.Steel.Util
open Zeta.Steel.IV
module T = Zeta.Steel.FormatsManual
module M = Zeta.Steel.ThreadStateModel
module AEH = Zeta.Steel.AggregateEpochHashes
module Cast = FStar.Int.Cast
open Zeta.Steel.EpochHashes
module KU = Zeta.Steel.KeyUtils
module EH = Zeta.Steel.EpochHashes
module HA = Zeta.Steel.HashAccumulator
#push-options "--ide_id_info_off"
#push-options "--query_stats --fuel 0 --ifuel 1"
/
Zeta.Steel.VerifierTypes.fst.checked Zeta.Steel.Util.fst.checked Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.ThreadLogMap.fsti.checked Zeta.Steel.LogEntry.fsti.checked Zeta.Steel.KeyUtils.fsti.checked Zeta.Steel.IV.fst.checked Zeta.Steel.HashValue.fsti.checked Zeta.Steel.HashAccumulator.fsti.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Steel.EpochMap.fsti.checked Zeta.Steel.EpochHashes.fst.checked Zeta.Steel.ApplicationTypes.fsti.checked Zeta.Steel.Application.fsti.checked Zeta.Steel.AggregateEpochHashes.fsti.checked Zeta.SeqAux.fsti.checked Steel.ST.Util.fsti.checked Steel.ST.Reference.fsti.checked Steel.ST.GhostReference.fsti.checked Steel.ST.CancellableSpinLock.fsti.checked Steel.ST.Array.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.PartialMap.fsti.checked FStar.Map.fsti.checked FStar.Int.Cast.fst.checked FStar.Ghost.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Calc.fsti.checked
Zeta.Steel.VerifierSteps.fst
t: Zeta.Steel.VerifierTypes.thread_state_t -> Steel.ST.Effect.STT Prims.unit
Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.VerifierTypes.thread_state_t Steel.ST.Reference.write Prims.bool FStar.Ghost.hide Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__failed Zeta.Steel.VerifierTypes.__proj__Mkthread_state_t__item__failed Prims.unit Zeta.Steel.VerifierTypes.thread_state_inv_core Zeta.Steel.ThreadStateModel.fail Steel.Effect.Common.vprop
let fail (#tsm: M.thread_state_model) (t: thread_state_t)
    : STT unit (thread_state_inv_core t tsm) (fun _ -> thread_state_inv_core t (M.fail tsm)) =
  
R.write t.failed true