val serialize_timestamp
      (#bs: Ghost.erased (Seq.seq FStar.UInt8.t))
      (a: byte_array{A.length a == 8})
      (v: timestamp)
    : STT U32.t
      (A.pts_to a full_perm bs)
      (fun slice_len ->
          exists_ (fun (bs: bytes) ->
                (A.pts_to a full_perm bs) `star` (pure (spec_serializer_timestamp v == bs))))
val serialize_timestamp
      (#bs: Ghost.erased (Seq.seq FStar.UInt8.t))
      (a: byte_array{A.length a == 8})
      (v: timestamp)
    : STT U32.t
      (A.pts_to a full_perm bs)
      (fun slice_len ->
          exists_ (fun (bs: bytes) ->
                (A.pts_to a full_perm bs) `star` (pure (spec_serializer_timestamp v == bs))))
let serialize_timestamp (#bs:Ghost.erased (Seq.seq FStar.UInt8.t))
                        (a:byte_array { A.length a == 8 })
                        (v: timestamp)
 : STT U32.t
    (A.pts_to a full_perm bs)
    (fun slice_len ->
       exists_ (fun (bs:bytes) ->
         A.pts_to a full_perm bs `star`
         pure (
           spec_serializer_timestamp v == bs)))
 = intro_exists_erased bs (array_pts_to a);
   let n = zeta__serialize_timestamp 8ul 0ul a v in
   let bs = elim_exists () in
   elim_pure _;
   // intro_pure (eq2 #bytes (spec_serializer_timestamp v) bs);
   // intro_exists_erased bs (fun (bs:bytes) -> A.pts_to a full_perm bs `star`
   //                                        pure (spec_serializer_timestamp v == bs));
   return n
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

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)
/
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

    a: Zeta.Steel.Parser.byte_array{Steel.ST.Array.length a == 8} ->
    v: Zeta.Steel.LogEntry.Types.timestamp
  -> Steel.ST.Effect.STT FStar.UInt32.t
FStar.Ghost.erased FStar.Seq.Base.seq FStar.UInt8.t Zeta.Steel.Parser.byte_array Prims.eq2 Prims.int Steel.ST.Array.length Zeta.Steel.Parser.byte Zeta.Steel.LogEntry.Types.timestamp Steel.ST.Util.return FStar.UInt32.t FStar.Ghost.hide FStar.Set.set Steel.Memory.iname FStar.Set.empty Steel.ST.Util.exists_ Zeta.Steel.Parser.bytes Steel.Effect.Common.VStar Steel.ST.Array.pts_to Steel.FractionalPermission.full_perm Steel.ST.Util.pure Zeta.Steel.LogEntry.Spec.spec_serializer_timestamp Steel.Effect.Common.vprop Prims.unit Steel.ST.Util.elim_pure Prims.l_and Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.b2t Prims.op_GreaterThanOrEqual FStar.UInt32.v FStar.Seq.Base.length Zeta.Steel.Parser.len_offset_slice_ok FStar.UInt32.__uint_to_t Prims.nat FStar.Ghost.reveal Zeta.Steel.Parser.slice Steel.ST.Util.elim_exists Zeta.Steel.LogEntry.zeta__serialize_timestamp Steel.ST.Util.intro_exists_erased Zeta.Steel.Util.array_pts_to Steel.Effect.Common.star
let serialize_timestamp
      (#bs: Ghost.erased (Seq.seq FStar.UInt8.t))
      (a: byte_array{A.length a == 8})
      (v: timestamp)
    : STT U32.t
      (A.pts_to a full_perm bs)
      (fun slice_len ->
          exists_ (fun (bs: bytes) ->
                (A.pts_to a full_perm bs) `star` (pure (spec_serializer_timestamp v == bs)))) =
  
intro_exists_erased bs (array_pts_to a);
let n = zeta__serialize_timestamp 8ul 0ul a v in
let bs = elim_exists () in
elim_pure _;
return n