val fail_as (#tsm: M.thread_state_model) (t: thread_state_t) (tsm': M.thread_state_model)
    : ST bool
      (thread_state_inv_core t tsm)
      (fun b -> thread_state_inv_core t (update_if b tsm tsm'))
      (requires tsm' == M.fail tsm)
      (ensures fun _ -> True)
val fail_as (#tsm: M.thread_state_model) (t: thread_state_t) (tsm': M.thread_state_model)
    : ST bool
      (thread_state_inv_core t tsm)
      (fun b -> thread_state_inv_core t (update_if b tsm tsm'))
      (requires tsm' == M.fail tsm)
      (ensures fun _ -> True)
let fail_as (#tsm:M.thread_state_model)
            (t:thread_state_t)
            (tsm':M.thread_state_model)
  : ST bool
    (thread_state_inv_core t tsm)
    (fun b -> thread_state_inv_core t (update_if b tsm tsm'))
    (requires tsm' == M.fail tsm)
    (ensures fun _ -> True)
  = R.write t.failed true;
    let b = true in
    intro_thread_state_inv_core (update_if b tsm tsm') t;
    return b
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"


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
/
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 -> tsm': Zeta.Steel.ThreadStateModel.thread_state_model
  -> Steel.ST.Effect.ST Prims.bool
Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.VerifierTypes.thread_state_t Steel.ST.Util.return Prims.bool FStar.Ghost.hide FStar.Set.set Steel.Memory.iname FStar.Set.empty Steel.Effect.Common.VStar Zeta.Steel.HashValue.inv Zeta.Steel.VerifierTypes.__proj__Mkthread_state_t__item__hasher Zeta.Steel.VerifierTypes.iv_buffer_inv Zeta.Steel.VerifierTypes.__proj__Mkthread_state_t__item__iv_buffer Steel.ST.Util.exists_ FStar.Seq.Base.seq FStar.UInt8.t Steel.ST.Array.pts_to Zeta.Steel.VerifierTypes.__proj__Mkthread_state_t__item__serialization_buffer Steel.FractionalPermission.full_perm Steel.Effect.Common.vprop Steel.ST.GhostReference.pts_to Zeta.Steel.ThreadStateModel.app_results Zeta.Steel.VerifierTypes.__proj__Mkthread_state_t__item__app_results Zeta.Steel.Util.full Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__app_results Zeta.Steel.Util.update_if Zeta.Steel.LogEntry.Types.log_entry Zeta.Steel.VerifierTypes.__proj__Mkthread_state_t__item__processed_entries Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__processed_entries Steel.ST.Reference.pts_to FStar.Pervasives.Native.option Zeta.Steel.ThreadStateModel.epoch_id Zeta.Steel.VerifierTypes.__proj__Mkthread_state_t__item__last_verified_epoch Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__last_verified_epoch Zeta.Steel.EpochMap.perm Zeta.Steel.EpochHashes.epoch_hashes_t Zeta.Steel.ThreadStateModel.epoch_hash Zeta.Steel.EpochHashes.epoch_hash_perm Zeta.Steel.VerifierTypes.__proj__Mkthread_state_t__item__epoch_hashes Zeta.Steel.ThreadStateModel.init_epoch_hash Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__epoch_hashes Zeta.Steel.EpochMap.empty_borrows Zeta.Steel.KeyUtils.base_key Zeta.Steel.VerifierTypes.__proj__Mkthread_state_t__item__last_evict_key Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__last_evict_key Zeta.Steel.LogEntry.Types.timestamp Zeta.Steel.VerifierTypes.__proj__Mkthread_state_t__item__clock Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__clock Zeta.Steel.ThreadStateModel.store_entry Zeta.Steel.VerifierTypes.__proj__Mkthread_state_t__item__store Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__store Zeta.Steel.VerifierTypes.__proj__Mkthread_state_t__item__failed Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__failed Prims.unit Zeta.Steel.VerifierTypes.intro_thread_state_inv_core Steel.ST.Reference.write Zeta.Steel.VerifierTypes.thread_state_inv_core Prims.eq2 Zeta.Steel.ThreadStateModel.fail Prims.l_True
let fail_as (#tsm: M.thread_state_model) (t: thread_state_t) (tsm': M.thread_state_model)
    : ST bool
      (thread_state_inv_core t tsm)
      (fun b -> thread_state_inv_core t (update_if b tsm tsm'))
      (requires tsm' == M.fail tsm)
      (ensures fun _ -> True) =
  
R.write t.failed true;
let b = true in
intro_thread_state_inv_core (update_if b tsm tsm') t;
return b