val spec_parser_log_entry_strong_prefix (l:bytes)
  : Lemma
    (requires
       Some? (spec_parser_log_entry l))
    (ensures (
       let Some (le, pos) = spec_parser_log_entry l in
       (forall (l1:bytes).{:pattern spec_parser_log_entry l1}
         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:bytes)
  : Lemma
    (requires
       Some? (spec_parser_log_entry l))
    (ensures (
       let Some (le, pos) = spec_parser_log_entry l in
       (forall (l1:bytes).{:pattern spec_parser_log_entry l1}
         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 bytes =
  Classical.forall_intro (Classical.move_requires (spec_parser_log_entry_strong_prefix' bytes))
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

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
/
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
  -> FStar.Pervasives.Lemma (requires Some? (Zeta.Steel.LogEntry.Spec.spec_parser_log_entry l))
      (ensures
        (let _ = Zeta.Steel.LogEntry.Spec.spec_parser_log_entry l in
          (let FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ le pos) =
              _
            in
            forall (l1: Zeta.Steel.Parser.bytes).
              {:pattern Zeta.Steel.LogEntry.Spec.spec_parser_log_entry l1}
              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))
          <:
          Type0))
Zeta.Steel.Parser.bytes FStar.Classical.forall_intro Prims.l_imp Prims.l_and Prims.b2t 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 Prims.op_LessThanOrEqual FStar.Seq.Base.length Zeta.Steel.Parser.byte FStar.Seq.Base.equal FStar.Seq.Base.slice Prims.logical Prims.l_False Prims.eq2 Prims.op_GreaterThan FStar.Classical.move_requires Zeta.Steel.LogEntry.Spec.spec_parser_log_entry_strong_prefix' Prims.unit
let spec_parser_log_entry_strong_prefix bytes =
  
Classical.forall_intro (Classical.move_requires (spec_parser_log_entry_strong_prefix' bytes))