val parse_full_log (l: bytes) : GTot (option (Seq.seq log_entry)) (decreases (Seq.length l))
val parse_full_log (l: bytes) : GTot (option (Seq.seq log_entry)) (decreases (Seq.length l))
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)
module Zeta.Steel.Log
include Zeta.Steel.LogEntry.Spec
open Zeta.Steel.Parser
module U32 = FStar.UInt32
/
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
l: Zeta.Steel.Parser.bytes
  -> Prims.GTot
    (FStar.Pervasives.Native.option (FStar.Seq.Base.seq Zeta.Steel.LogEntry.Types.log_entry))
Zeta.Steel.Parser.bytes Prims.op_Equality Prims.int FStar.Seq.Base.length Zeta.Steel.Parser.byte FStar.Pervasives.Native.Some FStar.Seq.Base.seq Zeta.Steel.LogEntry.Types.log_entry FStar.Seq.Base.empty Prims.bool Zeta.Steel.LogEntry.Spec.spec_parser_log_entry FStar.Pervasives.Native.None Prims.nat Zeta.Steel.Log.parse_full_log FStar.Seq.Base.slice FStar.Seq.Base.cons FStar.Pervasives.Native.option Prims.unit Zeta.Steel.LogEntry.Spec.spec_parser_log_entry_consumes_at_least_one_byte
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)