val spec_parser_log_entry : spec_parser log_entry
val spec_parser_log_entry : spec_parser log_entry
let spec_parser_log_entry b = match Zeta.Formats.LogEntry.parse_log_entry b with
  | None -> None
  | Some (res, consumed) -> Some (res, consumed)
module Zeta.Steel.LogEntry.Spec
/
Zeta.Steel.LogEntry.Types.fst.checked Zeta.Formats.Synth.fsti.checked Zeta.Formats.LogEntry.fst.checked Zeta.Formats.LogEntry.fst.checked Zeta.Formats.Aux.Value.fsti.checked Zeta.Formats.Aux.U256.fsti.checked Zeta.Formats.Aux.Timestamp.fsti.checked Zeta.Formats.Aux.Stamped_record.fsti.checked Zeta.Formats.Aux.Log_entry_hdr.fsti.checked prims.fst.checked LowParse.Spec.VLData.fsti.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Bytes.fst.checked LowParse.Spec.Base.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked FStar.Bytes.fsti.checked
Zeta.Steel.LogEntry.Spec.fst
Zeta.Steel.Parser.spec_parser Zeta.Steel.LogEntry.Types.log_entry
Zeta.Steel.Parser.bytes Zeta.Formats.LogEntry.parse_log_entry FStar.Pervasives.Native.None FStar.Pervasives.Native.tuple2 Zeta.Steel.LogEntry.Types.log_entry Prims.nat LowParse.Spec.Base.consumed_length FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 Zeta.Steel.Parser.parser_result
let spec_parser_log_entry b =
  
match Zeta.Formats.LogEntry.parse_log_entry b with
| None -> None
| Some (res, consumed) -> Some (res, consumed)