val maybe_parse_log_entry (log_bytes: bytes) (log_pos: U32.t) : GTot (option (log_entry & nat))
val maybe_parse_log_entry (log_bytes: bytes) (log_pos: U32.t) : GTot (option (log_entry & nat))
let maybe_parse_log_entry (log_bytes:bytes)
                          (log_pos:U32.t)
  : GTot (option (log_entry & nat))
  = if can_parse_log_entry log_bytes log_pos
    then Some (spec_parse_log_entry log_bytes log_pos)
    else None
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))

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
/
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
  -> Prims.GTot (FStar.Pervasives.Native.option (Zeta.Steel.LogEntry.Types.log_entry * Prims.nat))
Zeta.Steel.Parser.bytes FStar.UInt32.t Zeta.Steel.LogEntry.Spec.can_parse_log_entry FStar.Pervasives.Native.Some FStar.Pervasives.Native.tuple2 Zeta.Steel.LogEntry.Types.log_entry Prims.nat Zeta.Steel.LogEntry.Spec.spec_parse_log_entry Prims.bool FStar.Pervasives.Native.None FStar.Pervasives.Native.option
let maybe_parse_log_entry (log_bytes: bytes) (log_pos: U32.t) : GTot (option (log_entry & nat)) =
  
if can_parse_log_entry log_bytes log_pos
then Some (spec_parse_log_entry log_bytes log_pos)
else None