val runapp_payload_offset' (e: log_entry)
    : Pure U32.t
      (requires (RunApp? e))
      (ensures
        (fun res ->
            let s = Zeta.Formats.LogEntry.serialize_log_entry e in
            let RunApp r = e in
            let off = U32.v res in
            off <= Seq.length s /\
            (Ghost.reveal r.rest.ebytes) `Seq.equal` (Seq.slice s off (Seq.length s))))
val runapp_payload_offset' (e: log_entry)
    : Pure U32.t
      (requires (RunApp? e))
      (ensures
        (fun res ->
            let s = Zeta.Formats.LogEntry.serialize_log_entry e in
            let RunApp r = e in
            let off = U32.v res in
            off <= Seq.length s /\
            (Ghost.reveal r.rest.ebytes) `Seq.equal` (Seq.slice s off (Seq.length s))))
let runapp_payload_offset'
  (e: log_entry)
: Pure U32.t
  (requires (RunApp? e))
  (ensures (fun res ->
    let s = Zeta.Formats.LogEntry.serialize_log_entry e in
    let RunApp r = e in
    let off = U32.v res in
    off <= Seq.length s /\
    Ghost.reveal r.rest.ebytes `Seq.equal` Seq.slice s off (Seq.length s)
  ))
=
  let RunApp r = e in
  let b = Ghost.hide (FStar.Bytes.hide (Ghost.reveal r.rest.ebytes)) in
  let h = Zeta.Formats.LogEntry.synth_log_entry_recip_hdr e in
  assert (spec_serializer_log_entry e == Zeta.Formats.Aux.Log_entry_hdr.log_entry_hdr_serializer h `Seq.append` LowParse.Spec.Bytes.serialize_bounded_vlbytes 0 2147483647 (Ghost.reveal b));
  assert (LowParse.Spec.VLData.log256' 2147483647 == 4);
  LowParse.Spec.Combinators.serialize_synth_eq
    _
    (LowParse.Spec.Bytes.synth_bounded_vlbytes 0 2147483647)
    (LowParse.Spec.Bytes.serialize_bounded_vlbytes_aux 0 2147483647 4)
    (LowParse.Spec.Bytes.synth_bounded_vlbytes_recip 0 2147483647)
    ()
    (Ghost.reveal b)
  ;
  assert (LowParse.Spec.Bytes.serialize_bounded_vlbytes 0 2147483647 (Ghost.reveal b) == LowParse.Spec.VLData.serialize_bounded_integer 4 r.rest.len `Seq.append` r.rest.ebytes);
  Zeta.Formats.Aux.Log_entry_hdr.log_entry_hdr_size32 h `U32.add` 4ul
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

let spec_parser_log_entry_strong_prefix bytes =
  Classical.forall_intro (Classical.move_requires (spec_parser_log_entry_strong_prefix' bytes))

friend Zeta.Formats.LogEntry
/
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
e: Zeta.Steel.LogEntry.Types.log_entry -> Prims.Pure FStar.UInt32.t
Zeta.Steel.LogEntry.Types.log_entry Zeta.Steel.LogEntry.Types.runApp_payload FStar.UInt32.add Zeta.Formats.Aux.Log_entry_hdr.log_entry_hdr_size32 FStar.UInt32.__uint_to_t Prims.unit Prims._assert Prims.eq2 FStar.Seq.Base.seq LowParse.Bytes.byte LowParse.Spec.Bytes.serialize_bounded_vlbytes FStar.Ghost.reveal LowParse.Spec.Bytes.parse_bounded_vlbytes_t FStar.Seq.Base.append LowParse.Spec.BoundedInt.serialize_bounded_integer Zeta.Steel.LogEntry.Types.__proj__Mkuninterpreted__item__len Zeta.Steel.LogEntry.Types.__proj__MkrunApp_payload__item__rest FStar.UInt8.t Zeta.Steel.LogEntry.Types.__proj__Mkuninterpreted__item__ebytes LowParse.Spec.Combinators.serialize_synth_eq LowParse.Spec.VLData.parse_bounded_vldata_strong_kind LowParse.Spec.Bytes.parse_all_bytes_kind LowParse.Spec.VLData.parse_bounded_vldata_strong_t FStar.Bytes.bytes LowParse.Spec.Bytes.parse_all_bytes LowParse.Spec.Bytes.serialize_all_bytes LowParse.Spec.Bytes.parse_bounded_vlbytes_aux LowParse.Spec.Bytes.synth_bounded_vlbytes LowParse.Spec.Bytes.serialize_bounded_vlbytes_aux LowParse.Spec.Bytes.synth_bounded_vlbytes_recip Prims.int LowParse.Spec.BoundedInt.log256' Zeta.Steel.LogEntry.Spec.spec_serializer_log_entry Zeta.Formats.Aux.Log_entry_hdr.log_entry_hdr_serializer Zeta.Formats.Aux.Log_entry_hdr.log_entry_hdr Zeta.Formats.LogEntry.synth_log_entry_recip_hdr FStar.Ghost.erased FStar.Ghost.hide FStar.Bytes.hide FStar.UInt32.t Prims.b2t Zeta.Steel.LogEntry.Types.uu___is_RunApp Prims.l_and Prims.op_LessThanOrEqual FStar.Seq.Base.length FStar.Seq.Base.equal FStar.Seq.Base.slice FStar.UInt.uint_t FStar.UInt32.v LowParse.Bytes.bytes Zeta.Formats.LogEntry.serialize_log_entry
let runapp_payload_offset' (e: log_entry)
    : Pure U32.t
      (requires (RunApp? e))
      (ensures
        (fun res ->
            let s = Zeta.Formats.LogEntry.serialize_log_entry e in
            let RunApp r = e in
            let off = U32.v res in
            off <= Seq.length s /\
            (Ghost.reveal r.rest.ebytes) `Seq.equal` (Seq.slice s off (Seq.length s)))) =
  
let RunApp r = e in
let b = Ghost.hide (FStar.Bytes.hide (Ghost.reveal r.rest.ebytes)) in
let h = Zeta.Formats.LogEntry.synth_log_entry_recip_hdr e in
assert (spec_serializer_log_entry e ==
    (Zeta.Formats.Aux.Log_entry_hdr.log_entry_hdr_serializer h)
    `Seq.append`
    (LowParse.Spec.Bytes.serialize_bounded_vlbytes 0 2147483647 (Ghost.reveal b)));
assert (LowParse.Spec.VLData.log256' 2147483647 == 4);
LowParse.Spec.Combinators.serialize_synth_eq _
  (LowParse.Spec.Bytes.synth_bounded_vlbytes 0 2147483647)
  (LowParse.Spec.Bytes.serialize_bounded_vlbytes_aux 0 2147483647 4)
  (LowParse.Spec.Bytes.synth_bounded_vlbytes_recip 0 2147483647)
  ()
  (Ghost.reveal b);
assert (LowParse.Spec.Bytes.serialize_bounded_vlbytes 0 2147483647 (Ghost.reveal b) ==
    (LowParse.Spec.VLData.serialize_bounded_integer 4 r.rest.len)
    `Seq.append`
    r.rest.ebytes);
(Zeta.Formats.Aux.Log_entry_hdr.log_entry_hdr_size32 h) `U32.add` 4ul