val spec_parser_log_entry_strong_prefix' (l l1: bytes)
    : Lemma
      (requires
        Some? (spec_parser_log_entry l) /\
        (let Some (le, pos) = spec_parser_log_entry l in
          pos <= Seq.length l1 /\ (Seq.slice l 0 pos) `Seq.equal` (Seq.slice l1 0 pos)))
      (ensures
        (Some? (spec_parser_log_entry l) /\
          (let Some (le, pos) = spec_parser_log_entry l in
            (pos <= Seq.length l1 /\ (Seq.slice l 0 pos) `Seq.equal` (Seq.slice l1 0 pos)) /\
            (match spec_parser_log_entry l1 with
              | None -> False
              | Some (le', pos') -> le' == le /\ eq2 #nat pos' pos /\ pos > 0))))
val spec_parser_log_entry_strong_prefix' (l l1: bytes)
    : Lemma
      (requires
        Some? (spec_parser_log_entry l) /\
        (let Some (le, pos) = spec_parser_log_entry l in
          pos <= Seq.length l1 /\ (Seq.slice l 0 pos) `Seq.equal` (Seq.slice l1 0 pos)))
      (ensures
        (Some? (spec_parser_log_entry l) /\
          (let Some (le, pos) = spec_parser_log_entry l in
            (pos <= Seq.length l1 /\ (Seq.slice l 0 pos) `Seq.equal` (Seq.slice l1 0 pos)) /\
            (match spec_parser_log_entry l1 with
              | None -> False
              | Some (le', pos') -> le' == le /\ eq2 #nat pos' pos /\ pos > 0))))
let spec_parser_log_entry_strong_prefix' (l l1:bytes)
  : Lemma
    (requires
       Some? (spec_parser_log_entry l) /\
       (let Some (le, pos) = spec_parser_log_entry l in
         pos <= Seq.length l1 /\
         Seq.slice l 0 pos `Seq.equal` Seq.slice l1 0 pos))
    (ensures (
       Some? (spec_parser_log_entry l) /\
       (let Some (le, pos) = spec_parser_log_entry l in (
         pos <= Seq.length l1 /\
         Seq.slice l 0 pos `Seq.equal` Seq.slice l1 0 pos) /\
         (match spec_parser_log_entry l1 with
          | None -> False
          | Some (le', pos') -> le' == le /\ eq2 #nat pos' pos /\ pos > 0))))
= 
  LowParse.Spec.Base.parse_strong_prefix Zeta.Formats.LogEntry.parse_log_entry l l1;
  spec_parser_log_entry_consumes_at_least_one_byte l1
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)

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

let spec_parser_log_entry_consumes_at_least_one_byte bytes =
  let _ = LowParse.Spec.Base.parse Zeta.Formats.LogEntry.parse_log_entry bytes in // SMT pattern
  LowParse.Spec.Base.parser_kind_prop_equiv Zeta.Formats.LogEntry.parse_log_entry_kind Zeta.Formats.LogEntry.parse_log_entry
/
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
l: Zeta.Steel.Parser.bytes -> l1: Zeta.Steel.Parser.bytes
  -> FStar.Pervasives.Lemma
      (requires
        Some? (Zeta.Steel.LogEntry.Spec.spec_parser_log_entry l) /\
        (let _ = Zeta.Steel.LogEntry.Spec.spec_parser_log_entry l in
          (let FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ _ pos) = _ in
            pos <= FStar.Seq.Base.length l1 /\
            FStar.Seq.Base.equal (FStar.Seq.Base.slice l 0 pos) (FStar.Seq.Base.slice l1 0 pos))
          <:
          Prims.logical))
      (ensures
        Some? (Zeta.Steel.LogEntry.Spec.spec_parser_log_entry l) /\
        (let _ = Zeta.Steel.LogEntry.Spec.spec_parser_log_entry l in
          (let FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ le pos) =
              _
            in
            pos <= FStar.Seq.Base.length l1 /\
            FStar.Seq.Base.equal (FStar.Seq.Base.slice l 0 pos) (FStar.Seq.Base.slice l1 0 pos) /\
            (match Zeta.Steel.LogEntry.Spec.spec_parser_log_entry l1 with
              | FStar.Pervasives.Native.None #_ -> Prims.l_False
              | FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ le' pos') ->
                le' == le /\ pos' == pos /\ pos > 0))
          <:
          Prims.logical))
Zeta.Steel.Parser.bytes Zeta.Steel.LogEntry.Spec.spec_parser_log_entry_consumes_at_least_one_byte Prims.unit LowParse.Spec.Base.parse_strong_prefix Zeta.Formats.LogEntry.parse_log_entry_kind Zeta.Steel.LogEntry.Types.log_entry Zeta.Formats.LogEntry.parse_log_entry Prims.l_and Prims.b2t FStar.Pervasives.Native.uu___is_Some FStar.Pervasives.Native.tuple2 Prims.nat Zeta.Steel.LogEntry.Spec.spec_parser_log_entry Prims.op_LessThanOrEqual FStar.Seq.Base.length Zeta.Steel.Parser.byte FStar.Seq.Base.equal FStar.Seq.Base.slice Prims.logical Zeta.Steel.Parser.parser_result Prims.squash Prims.l_False Prims.eq2 Prims.op_GreaterThan Prims.Nil FStar.Pervasives.pattern
let spec_parser_log_entry_strong_prefix' (l l1: bytes)
    : Lemma
      (requires
        Some? (spec_parser_log_entry l) /\
        (let Some (le, pos) = spec_parser_log_entry l in
          pos <= Seq.length l1 /\ (Seq.slice l 0 pos) `Seq.equal` (Seq.slice l1 0 pos)))
      (ensures
        (Some? (spec_parser_log_entry l) /\
          (let Some (le, pos) = spec_parser_log_entry l in
            (pos <= Seq.length l1 /\ (Seq.slice l 0 pos) `Seq.equal` (Seq.slice l1 0 pos)) /\
            (match spec_parser_log_entry l1 with
              | None -> False
              | Some (le', pos') -> le' == le /\ eq2 #nat pos' pos /\ pos > 0)))) =
  
LowParse.Spec.Base.parse_strong_prefix Zeta.Formats.LogEntry.parse_log_entry l l1;
spec_parser_log_entry_consumes_at_least_one_byte l1