val spec_serializer_log_entry : x: Zeta.Steel.LogEntry.Types.log_entry -> Prims.GTot LowParse.Bytes.bytes
let spec_serializer_log_entry x =
  assert (LowParse.Spec.Base.parse Zeta.Formats.LogEntry.parse_log_entry (Zeta.Formats.LogEntry.serialize_log_entry x) == Some (x, Seq.length (Zeta.Formats.LogEntry.serialize_log_entry x))); // pattern requires `LowParse.Spec.Base.parse`
  Zeta.Formats.LogEntry.serialize_log_entry x
module Zeta.Steel.LogEntry.Spec

let spec_parser_log_entry b = match Zeta.Formats.LogEntry.parse_log_entry b with
  | None -> None
  | Some (res, consumed) -> Some (res, consumed)
/
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
x: Zeta.Steel.LogEntry.Types.log_entry -> Prims.GTot LowParse.Bytes.bytes
Zeta.Steel.LogEntry.Types.log_entry Zeta.Formats.LogEntry.serialize_log_entry Prims.unit Prims._assert Prims.eq2 FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length LowParse.Spec.Base.parse Zeta.Formats.LogEntry.parse_log_entry FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 FStar.Seq.Base.length LowParse.Bytes.byte LowParse.Bytes.bytes
let spec_serializer_log_entry x =
  
assert (LowParse.Spec.Base.parse Zeta.Formats.LogEntry.parse_log_entry
      (Zeta.Formats.LogEntry.serialize_log_entry x) ==
    Some (x, Seq.length (Zeta.Formats.LogEntry.serialize_log_entry x)));
Zeta.Formats.LogEntry.serialize_log_entry x