val rewrite_with_squash (#o: _) (p q: vprop) (f: (unit -> squash (p == q)))
    : STGhostT unit o p (fun _ -> q)
val rewrite_with_squash (#o: _) (p q: vprop) (f: (unit -> squash (p == q)))
    : STGhostT unit o p (fun _ -> q)
let rewrite_with_squash #o (p q:vprop)
                        (f:unit -> squash (p == q))
  : STGhostT unit o p (fun _ -> q)
  = f();
    rewrite p q
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


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

let maybe_extend_processed_entries #o
                                   (#tsm:M.thread_state_model)
                                   (t:thread_state_t)
                                   (b:bool)
                                   (le:log_entry)
  : STGhost unit o
    (thread_state_inv_core t (update_if b tsm (M.verify_log_entry tsm le)))
    (fun _ -> thread_state_inv t (update_if b tsm (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)
  = if b
    then (
      rewrite
        (thread_state_inv_core t _)
        (thread_state_inv_core t (M.verify_log_entry tsm le));
      extend_processed_entries t le;
      rewrite
        (thread_state_inv t _)
        (thread_state_inv t (update_if b tsm (M.verify_step_model tsm le)))
    )
    else (
      rewrite (thread_state_inv_core t _)
              (thread_state_inv_core t (update_if b tsm (M.verify_step_model tsm le)));
      intro_thread_state_inv t
    )

let to_base_key (x:T.key)
  : ST T.base_key
    emp (fun _ -> emp)
    (requires True)
    (ensures fun b -> b == M.to_base_key x)
  = match x with
    | InternalKey k -> return k
    | ApplicationKey k ->
      let k' = Zeta.Steel.Application.key_type_to_base_key k in
      return k'

////////////////////////////////////////////////////////////////////////////////
//check_failed
////////////////////////////////////////////////////////////////////////////////

let check_failed #tsm t
  = elim_thread_state_inv t;
    let b = R.read t.failed in
    intro_thread_state_inv t;
    return b

////////////////////////////////////////////////////////////////////////////////
//vaddm
////////////////////////////////////////////////////////////////////////////////
/
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

    p: Steel.Effect.Common.vprop ->
    q: Steel.Effect.Common.vprop ->
    f: (_: Prims.unit -> Prims.squash (p == q))
  -> Steel.ST.Effect.Ghost.STGhostT Prims.unit
Steel.Memory.inames Steel.Effect.Common.vprop Prims.unit Prims.squash Prims.eq2 Steel.ST.Util.rewrite
let rewrite_with_squash #o (p: vprop) (q: vprop) (f: (unit -> squash (p == q)))
    : STGhostT unit o p (fun _ -> q) =
  
f ();
rewrite p q