val verify_post_out_bytes
      (tsm: M.thread_state_model)
      (out_bytes: bytes)
      (wrote: U32.t)
      (out: A.array U8.t)
      (les: M.log)
    : vprop
val verify_post_out_bytes
      (tsm: M.thread_state_model)
      (out_bytes: bytes)
      (wrote: U32.t)
      (out: A.array U8.t)
      (les: M.log)
    : vprop
let verify_post_out_bytes (tsm:M.thread_state_model)
                          (out_bytes:bytes)
                          (wrote:U32.t)
                          (out:A.array U8.t)
                          (les:M.log)
  : vprop
  = exists_ (fun (out_bytes1:Seq.seq U8.t) ->
     array_pts_to out out_bytes1 `star`  //the out array contains out_bytes
     pure (Application.n_out_bytes tsm (M.verify_model tsm les) 0ul wrote out_bytes out_bytes1))
module Zeta.Steel.Verifier
include 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
open Zeta.Steel.ApplicationTypes
module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
open Zeta.Steel.FormatsManual
open Zeta.Steel.Util
module T = Zeta.Steel.FormatsManual
module M = Zeta.Steel.ThreadStateModel
module AEH = Zeta.Steel.AggregateEpochHashes
module P = Zeta.Steel.Parser
module TLM = Zeta.Steel.ThreadLogMap

#push-options "--ide_id_info_off"
type verify_result =
  | Parsing_failure: log_pos:U32.t -> verify_result
  | App_failure: log_pos:U32.t -> verify_result
  | Verify_entry_failure: log_pos:U32.t -> verify_result
  | Verify_success: read:U32.t -> wrote:U32.t -> verify_result

let verify_result_complete (len:U32.t) res =
    match res with
    | Verify_success read _ ->
      read == len
    | _ -> True

[@@__steel_reduce__;__reduce__]
let some_failure (t:thread_state_t) //handle to the thread state
                 (out:A.array U8.t)
                 (aeh:AEH.aggregate_epoch_hashes) //lock & handle to the aggregate state
  : vprop
  = exists_ (thread_state_inv t) `star`
    exists_ (fun entries -> TLM.tid_pts_to aeh.mlogs (VerifierTypes.thread_id t) full entries false) `star`
    exists_ (array_pts_to out)
/
Zeta.Steel.VerifierTypes.fsti.checked Zeta.Steel.Util.fst.checked Zeta.Steel.ThreadStateModel.fst.checked Zeta.Steel.ThreadLogMap.fsti.checked Zeta.Steel.Parser.fst.checked Zeta.Steel.LogEntry.fsti.checked Zeta.Steel.Log.fst.checked Zeta.Steel.FormatsManual.fsti.checked Zeta.Steel.ApplicationTypes.fsti.checked Zeta.Steel.Application.fsti.checked Zeta.Steel.AggregateEpochHashes.fsti.checked Steel.ST.Util.fsti.checked Steel.ST.Reference.fsti.checked Steel.ST.GhostReference.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.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Zeta.Steel.Verifier.fsti

    tsm: Zeta.Steel.ThreadStateModel.thread_state_model ->
    out_bytes: Zeta.Steel.ApplicationTypes.bytes ->
    wrote: FStar.UInt32.t ->
    out: Steel.ST.Array.array FStar.UInt8.t ->
    les: Zeta.Steel.ThreadStateModel.log
  -> Steel.Effect.Common.vprop
Zeta.Steel.ThreadStateModel.thread_state_model Zeta.Steel.ApplicationTypes.bytes FStar.UInt32.t Steel.ST.Array.array FStar.UInt8.t Zeta.Steel.ThreadStateModel.log Steel.ST.Util.exists_ FStar.Seq.Base.seq Steel.Effect.Common.star Zeta.Steel.Util.array_pts_to Steel.ST.Util.pure Zeta.Steel.Application.n_out_bytes Zeta.Steel.ThreadStateModel.verify_model FStar.UInt32.__uint_to_t Steel.Effect.Common.vprop
let verify_post_out_bytes
      (tsm: M.thread_state_model)
      (out_bytes: bytes)
      (wrote: U32.t)
      (out: A.array U8.t)
      (les: M.log)
    : vprop =
  
exists_ (fun (out_bytes1: Seq.seq U8.t) ->
      (array_pts_to out out_bytes1)
      `star`
      (pure (Application.n_out_bytes tsm (M.verify_model tsm les) 0ul wrote out_bytes out_bytes1)))