val can_parse_log_entry : log_bytes: Zeta.Steel.Parser.bytes -> log_pos: FStar.UInt32.t -> Prims.GTot Prims.bool
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))
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
/
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 Prims.bool
Zeta.Steel.Parser.bytes FStar.UInt32.t Prims.op_AmpAmp Prims.op_LessThanOrEqual FStar.UInt32.v FStar.Seq.Base.length Zeta.Steel.Parser.byte FStar.Pervasives.Native.uu___is_Some FStar.Pervasives.Native.tuple2 Zeta.Steel.LogEntry.Types.log_entry Prims.nat Zeta.Steel.LogEntry.Spec.spec_parser_log_entry Zeta.Steel.Parser.bytes_from Prims.bool
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))