val extend_processed_entries
      (#o: _)
      (#tsm: M.thread_state_model)
      (t: thread_state_t)
      (le: log_entry)
    : STGhost unit
      o
      (thread_state_inv_core t (M.verify_log_entry tsm le))
      (fun _ -> thread_state_inv t (M.verify_step_model tsm le))
      (requires
        not tsm.failed /\ tsm_entries_invariant tsm /\ t.thread_id == tsm.thread_id /\
        not (VerifyEpoch? le))
      (ensures fun _ -> True)
val extend_processed_entries
      (#o: _)
      (#tsm: M.thread_state_model)
      (t: thread_state_t)
      (le: log_entry)
    : STGhost unit
      o
      (thread_state_inv_core t (M.verify_log_entry tsm le))
      (fun _ -> thread_state_inv t (M.verify_step_model tsm le))
      (requires
        not tsm.failed /\ tsm_entries_invariant tsm /\ t.thread_id == tsm.thread_id /\
        not (VerifyEpoch? le))
      (ensures fun _ -> True)
let extend_processed_entries #o
                             (#tsm:M.thread_state_model)
                             (t:thread_state_t)
                             (le:log_entry)
  : STGhost unit o
    (thread_state_inv_core t (M.verify_log_entry tsm le))
    (fun _ -> thread_state_inv t (M.verify_step_model tsm le))
    (requires
      not tsm.failed /\
      tsm_entries_invariant tsm /\
      t.thread_id == tsm.thread_id /\
      not (VerifyEpoch? le))
    (ensures fun _ -> True)
  = M.tsm_entries_invariant_verify_step tsm le;
    rewrite
        (thread_state_inv_core t _)
        (thread_state_inv_core t (M.verify_log_entry tsm le));
    G.write t.processed_entries (Seq.snoc tsm.processed_entries le);
    intro_thread_state_inv_core (M.verify_step_model tsm le) t;
    intro_thread_state_inv t
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

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
/
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 -> le: Zeta.Steel.LogEntry.Types.log_entry
  -> Steel.ST.Effect.Ghost.STGhost Prims.unit
Steel.Memory.inames Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.VerifierTypes.thread_state_t Zeta.Steel.LogEntry.Types.log_entry Zeta.Steel.VerifierTypes.intro_thread_state_inv Zeta.Steel.ThreadStateModel.verify_step_model Prims.unit Zeta.Steel.VerifierTypes.intro_thread_state_inv_core Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__failed Zeta.Steel.ThreadStateModel.verify_log_entry Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__store Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__clock Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__last_evict_key Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__epoch_hashes Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__last_verified_epoch FStar.Seq.Properties.snoc Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__processed_entries Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__app_results Steel.ST.GhostReference.write FStar.Seq.Base.seq FStar.Ghost.hide Zeta.Steel.VerifierTypes.__proj__Mkthread_state_t__item__processed_entries Steel.ST.Util.rewrite Zeta.Steel.VerifierTypes.thread_state_inv_core Zeta.Steel.ThreadStateModel.tsm_entries_invariant_verify_step Zeta.Steel.VerifierTypes.thread_state_inv Steel.Effect.Common.vprop Prims.l_and Prims.b2t Prims.op_Negation Zeta.Steel.VerifierTypes.tsm_entries_invariant Prims.eq2 Zeta.Steel.ApplicationTypes.tid Zeta.Steel.VerifierTypes.__proj__Mkthread_state_t__item__thread_id Zeta.Steel.ThreadStateModel.__proj__Mkthread_state_model__item__thread_id Zeta.Steel.LogEntry.Types.uu___is_VerifyEpoch Prims.l_True
let extend_processed_entries #o (#tsm: M.thread_state_model) (t: thread_state_t) (le: log_entry)
    : STGhost unit
      o
      (thread_state_inv_core t (M.verify_log_entry tsm le))
      (fun _ -> thread_state_inv t (M.verify_step_model tsm le))
      (requires
        not tsm.failed /\ tsm_entries_invariant tsm /\ t.thread_id == tsm.thread_id /\
        not (VerifyEpoch? le))
      (ensures fun _ -> True) =
  
M.tsm_entries_invariant_verify_step tsm le;
rewrite (thread_state_inv_core t _) (thread_state_inv_core t (M.verify_log_entry tsm le));
G.write t.processed_entries (Seq.snoc tsm.processed_entries le);
intro_thread_state_inv_core (M.verify_step_model tsm le) t;
intro_thread_state_inv t