val verify_result_complete : len: FStar.UInt32.t -> res: Zeta.Steel.Verifier.verify_result -> Prims.logical
let verify_result_complete (len:U32.t) res =
    match res with
    | Verify_success read _ ->
      read == len
    | _ -> True
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
/
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
len: FStar.UInt32.t -> res: Zeta.Steel.Verifier.verify_result -> Prims.logical
FStar.UInt32.t Zeta.Steel.Verifier.verify_result Prims.eq2 Prims.l_True Prims.logical
let verify_result_complete (len: U32.t) res =
  
match res with
| Verify_success read _ -> read == len
| _ -> True