val full_parse_log_entry : l: Zeta.Steel.Parser.bytes -> Prims.GTot Prims.logical
let full_parse_log_entry (l:bytes) =
  match spec_parser_log_entry l with
  | None -> False
  | Some (le, n) -> n == Seq.length l
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)
/
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 Prims.logical
Zeta.Steel.Parser.bytes Zeta.Steel.LogEntry.Spec.spec_parser_log_entry Prims.l_False Zeta.Steel.LogEntry.Types.log_entry Prims.nat Prims.eq2 FStar.Seq.Base.length Zeta.Steel.Parser.byte Prims.logical
let full_parse_log_entry (l: bytes) =
  
match spec_parser_log_entry l with
| None -> False
| Some (le, n) -> n == Seq.length l