val parse_full_log_trans (l0 l1: bytes)
    : Lemma (requires Some? (parse_full_log l0) /\ full_parse_log_entry l1)
      (ensures
        (let Some les = parse_full_log l0 in
          let Some (le, _) = spec_parser_log_entry l1 in
          match parse_full_log (l0 `Seq.append` l1) with
          | None -> False
          | Some s -> s `Seq.equal` (Seq.snoc les le)))
      (decreases (Seq.length l0))
val parse_full_log_trans (l0 l1: bytes)
    : Lemma (requires Some? (parse_full_log l0) /\ full_parse_log_entry l1)
      (ensures
        (let Some les = parse_full_log l0 in
          let Some (le, _) = spec_parser_log_entry l1 in
          match parse_full_log (l0 `Seq.append` l1) with
          | None -> False
          | Some s -> s `Seq.equal` (Seq.snoc les le)))
      (decreases (Seq.length l0))
let rec parse_full_log_trans (l0 l1:bytes)
  : Lemma
    (requires
      Some? (parse_full_log l0) /\
      full_parse_log_entry l1)
    (ensures (
      let Some les = parse_full_log l0 in
      let Some (le, _) = spec_parser_log_entry l1 in
      match parse_full_log (l0 `Seq.append` l1) with
      | None -> False
      | Some s -> s `Seq.equal` Seq.snoc les le))
    (decreases (Seq.length l0))
  = let Some les = parse_full_log l0 in
    let Some (le, pos) = spec_parser_log_entry l1 in
    spec_parser_log_entry_strong_prefix l1;
    assert (pos > 0);
    assert (Seq.length l1 = pos);
    if Seq.length l0 = 0
    then (
      assert (Seq.append l0 l1 `Seq.equal` l1)
    )
    else (
      let Some (le, n) = spec_parser_log_entry l0 in
      spec_parser_log_entry_strong_prefix l0;
      parse_full_log_trans (Seq.slice l0 n (Seq.length l0)) l1;
      assert (l0 `Seq.append` l1 `Seq.equal`
              (Seq.slice l0 0 n `Seq.append` (Seq.slice l0 n (Seq.length l0) `Seq.append` l1)));
      assert (Seq.slice (l0 `Seq.append` l1) n (Seq.length (Seq.append l0 l1)) `Seq.equal`
             (Seq.slice l0 n (Seq.length l0) `Seq.append` l1))
    )
module Zeta.Steel.Log
include Zeta.Steel.LogEntry.Spec
open Zeta.Steel.Parser
module U32 = FStar.UInt32

let rec parse_full_log (l:bytes)
  : GTot (option (Seq.seq log_entry))
         (decreases (Seq.length l))
  = if Seq.length l = 0 then Some Seq.empty
    else match spec_parser_log_entry l with
         | None -> None
         | Some (le, n) ->
           spec_parser_log_entry_consumes_at_least_one_byte l;
           match parse_full_log (Seq.slice l n (Seq.length l)) with
           | None -> None
           | Some out -> Some (Seq.cons le out)

let full_parse_log_entry (l:bytes) =
  match spec_parser_log_entry l with
  | None -> False
  | Some (le, n) -> n == Seq.length l
/
Zeta.Steel.Parser.fst.checked Zeta.Steel.LogEntry.Spec.fsti.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.Steel.Log.fst
l0: Zeta.Steel.Parser.bytes -> l1: Zeta.Steel.Parser.bytes
  -> FStar.Pervasives.Lemma
      (requires Some? (Zeta.Steel.Log.parse_full_log l0) /\ Zeta.Steel.Log.full_parse_log_entry l1)
      (ensures
        (let _ = Zeta.Steel.Log.parse_full_log l0 in
          (let FStar.Pervasives.Native.Some #_ les = _ in
            let _ = Zeta.Steel.LogEntry.Spec.spec_parser_log_entry l1 in
            (let FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ le _) =
                _
              in
              (match Zeta.Steel.Log.parse_full_log (FStar.Seq.Base.append l0 l1) with
                | FStar.Pervasives.Native.None #_ -> Prims.l_False
                | FStar.Pervasives.Native.Some #_ s ->
                  FStar.Seq.Base.equal s (FStar.Seq.Properties.snoc les le))
              <:
              Type0)
            <:
            Type0)
          <:
          Type0))
      (decreases FStar.Seq.Base.length l0)
Zeta.Steel.Parser.bytes FStar.Seq.Base.seq Zeta.Steel.LogEntry.Types.log_entry Prims.nat Prims.op_Equality Prims.int FStar.Seq.Base.length Zeta.Steel.Parser.byte Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.append Prims.bool FStar.Seq.Base.slice Prims.unit Zeta.Steel.Log.parse_full_log_trans Zeta.Steel.LogEntry.Spec.spec_parser_log_entry_strong_prefix Zeta.Steel.Parser.parser_result Zeta.Steel.LogEntry.Spec.spec_parser_log_entry Prims.b2t Prims.op_GreaterThan FStar.Pervasives.Native.option Zeta.Steel.Log.parse_full_log Prims.l_and FStar.Pervasives.Native.uu___is_Some Zeta.Steel.Log.full_parse_log_entry Prims.squash Prims.l_False FStar.Seq.Properties.snoc Prims.Nil FStar.Pervasives.pattern
let rec parse_full_log_trans (l0 l1: bytes)
    : Lemma (requires Some? (parse_full_log l0) /\ full_parse_log_entry l1)
      (ensures
        (let Some les = parse_full_log l0 in
          let Some (le, _) = spec_parser_log_entry l1 in
          match parse_full_log (l0 `Seq.append` l1) with
          | None -> False
          | Some s -> s `Seq.equal` (Seq.snoc les le)))
      (decreases (Seq.length l0)) =
  
let Some les = parse_full_log l0 in
let Some (le, pos) = spec_parser_log_entry l1 in
spec_parser_log_entry_strong_prefix l1;
assert (pos > 0);
assert (Seq.length l1 = pos);
if Seq.length l0 = 0
then (assert ((Seq.append l0 l1) `Seq.equal` l1))
else
  (let Some (le, n) = spec_parser_log_entry l0 in
    spec_parser_log_entry_strong_prefix l0;
    parse_full_log_trans (Seq.slice l0 n (Seq.length l0)) l1;
    assert ((l0 `Seq.append` l1)
        `Seq.equal`
        ((Seq.slice l0 0 n) `Seq.append` ((Seq.slice l0 n (Seq.length l0)) `Seq.append` l1)));
    assert ((Seq.slice (l0 `Seq.append` l1) n (Seq.length (Seq.append l0 l1)))
        `Seq.equal`
        ((Seq.slice l0 n (Seq.length l0)) `Seq.append` l1)))