val spec_parse_log_entry (log_bytes: bytes) (log_pos: U32.t{can_parse_log_entry log_bytes log_pos})
    : GTot (log_entry & nat)
val spec_parse_log_entry (log_bytes: bytes) (log_pos: U32.t{can_parse_log_entry log_bytes log_pos})
    : GTot (log_entry & nat)
let spec_parse_log_entry (log_bytes:bytes)
                         (log_pos:U32.t{
                            can_parse_log_entry log_bytes log_pos
                          })
  : GTot (log_entry & nat)
  = parse_result log_bytes log_pos spec_parser_log_entry
module Zeta.Steel.LogEntry.Spec
include Zeta.Steel.LogEntry.Types
open Zeta.Steel.Parser
module U8 = FStar.UInt8
module U32 = FStar.UInt32
val spec_parser_log_entry : spec_parser log_entry

let can_parse_log_entry (log_bytes:bytes)
                        (log_pos:U32.t)
  = U32.v log_pos <= Seq.length log_bytes &&
    Some? (spec_parser_log_entry (Zeta.Steel.Parser.bytes_from log_bytes log_pos))
/
Zeta.Steel.Parser.fst.checked Zeta.Steel.LogEntry.Types.fst.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Zeta.Steel.LogEntry.Spec.fsti

    log_bytes: Zeta.Steel.Parser.bytes ->
    log_pos: FStar.UInt32.t{Zeta.Steel.LogEntry.Spec.can_parse_log_entry log_bytes log_pos}
  -> Prims.GTot (Zeta.Steel.LogEntry.Types.log_entry * Prims.nat)
Zeta.Steel.Parser.bytes FStar.UInt32.t Prims.b2t Zeta.Steel.LogEntry.Spec.can_parse_log_entry Zeta.Steel.Parser.parse_result Zeta.Steel.LogEntry.Types.log_entry Zeta.Steel.LogEntry.Spec.spec_parser_log_entry FStar.Pervasives.Native.tuple2 Prims.nat
let spec_parse_log_entry (log_bytes: bytes) (log_pos: U32.t{can_parse_log_entry log_bytes log_pos})
    : GTot (log_entry & nat) =
  
parse_result log_bytes log_pos spec_parser_log_entry