val seq_suffix_is_zero : s: FStar.Seq.Base.seq Zeta.Steel.Parser.byte -> from: Prims.nat -> Prims.logical
let seq_suffix_is_zero (s:Seq.seq byte)
                       (from:nat)
  = from <= Seq.length s /\
    s `Seq.equal` Seq.append (Seq.slice s 0 from)
                             (Seq.create (Seq.length s - from) 0uy)
module Zeta.Steel.IV
open Zeta.Steel.LogEntry.Spec
open Zeta.Steel.LogEntry
open Zeta.Steel.Parser
open Steel.ST.Util
open Zeta.Steel.Util
module A = Steel.ST.Array
module U32 = FStar.UInt32

noextract
let timestamp_len = 8
/
Zeta.Steel.Util.fst.checked Zeta.Steel.Parser.fst.checked Zeta.Steel.LogEntry.Spec.fsti.checked Zeta.Steel.LogEntry.fsti.checked Steel.ST.Util.fsti.checked Steel.ST.Array.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.SizeT.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked
Zeta.Steel.IV.fst
s: FStar.Seq.Base.seq Zeta.Steel.Parser.byte -> from: Prims.nat -> Prims.logical
FStar.Seq.Base.seq Zeta.Steel.Parser.byte Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length FStar.Seq.Base.equal FStar.Seq.Base.append FStar.Seq.Base.slice FStar.Seq.Base.create Prims.op_Subtraction FStar.UInt8.__uint_to_t Prims.logical
let seq_suffix_is_zero (s: Seq.seq byte) (from: nat) =
  
from <= Seq.length s /\
s `Seq.equal` (Seq.append (Seq.slice s 0 from) (Seq.create (Seq.length s - from) 0uy))