val serialize_iv (a: byte_array{A.length a == 96}) (v: timestamp)
    : Steel.ST.Util.STT unit
      (exists_ (fun bs ->
              (A.pts_to a full_perm bs) `star` (pure (seq_suffix_is_zero bs timestamp_len))))
      (fun slice_len ->
          exists_ (fun (bs: _) ->
                (A.pts_to a full_perm bs)
                `star`
                (pure (seq_suffix_is_zero bs timestamp_len /\ spec_serializer_iv v == bs))))
val serialize_iv (a: byte_array{A.length a == 96}) (v: timestamp)
    : Steel.ST.Util.STT unit
      (exists_ (fun bs ->
              (A.pts_to a full_perm bs) `star` (pure (seq_suffix_is_zero bs timestamp_len))))
      (fun slice_len ->
          exists_ (fun (bs: _) ->
                (A.pts_to a full_perm bs)
                `star`
                (pure (seq_suffix_is_zero bs timestamp_len /\ spec_serializer_iv v == bs))))
let serialize_iv (a:byte_array { A.length a == 96 })
                 (v: timestamp)
  : Steel.ST.Util.STT unit
    (exists_ (fun bs -> A.pts_to a full_perm bs `star` pure (seq_suffix_is_zero bs timestamp_len)))
    (fun slice_len ->
       exists_ (fun (bs:_) ->
         A.pts_to a full_perm bs `star`
         pure (
           seq_suffix_is_zero bs timestamp_len /\
           spec_serializer_iv v == bs)))
  = let bs = elim_exists () in
    A.pts_to_length a bs;
    elim_pure _;
    seq_suffix_is_zero_elim bs timestamp_len;
    let adj = A.ghost_split a 8sz in
    let n = serialize_timestamp (A.split_l a 8sz) v in 
    let bs_l = elim_exists () in
    A.pts_to_length (A.split_l a 8sz) bs_l;
    elim_pure _;
    assert_ (A.pts_to (A.split_l a 8sz) full_perm bs_l `star`
             A.pts_to (A.split_r a 8sz) full_perm (Seq.slice bs 8 (Seq.length bs)));
    A.ghost_join (A.split_l a 8sz) (A.split_r a 8sz) adj;
    rewrite (A.pts_to (A.merge (A.split_l a 8sz) (A.split_r a 8sz)) _ _)
            (A.pts_to a full_perm (spec_serializer_iv v));
    intro_pure (seq_suffix_is_zero (spec_serializer_iv v) timestamp_len /\
                spec_serializer_iv v == spec_serializer_iv v);
    return ()
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)


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
   

let seq_suffix_is_zero_elim (s:Seq.seq byte)
                            (from:nat)
  : Lemma 
    (requires seq_suffix_is_zero s from)
    (ensures
         from <= Seq.length s /\
         Seq.slice s from (Seq.length s) `Seq.equal` 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 == 96} ->
    v: Zeta.Steel.LogEntry.Types.timestamp
  -> Steel.ST.Effect.STT Prims.unit
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 Prims.unit FStar.Ghost.hide FStar.Set.set Steel.Memory.iname FStar.Set.empty Steel.ST.Util.exists_ FStar.Seq.Base.seq Steel.Effect.Common.VStar Steel.ST.Array.pts_to Steel.FractionalPermission.full_perm Steel.ST.Util.pure Prims.l_and Zeta.Steel.IV.seq_suffix_is_zero Zeta.Steel.IV.timestamp_len Zeta.Steel.LogEntry.Spec.spec_serializer_iv Steel.Effect.Common.vprop Steel.ST.Util.intro_pure Steel.ST.Util.rewrite Steel.ST.Array.merge Steel.ST.Array.split_l FStar.SizeT.t FStar.SizeT.__uint_to_t Steel.ST.Array.array Steel.ST.Array.split_r FStar.Seq.Base.append FStar.Ghost.reveal FStar.Seq.Base.slice FStar.Seq.Base.length Steel.ST.Array.ghost_join Steel.ST.Util.assert_ Steel.Effect.Common.star Steel.ST.Util.elim_pure Zeta.Steel.Parser.bytes Zeta.Steel.LogEntry.Spec.spec_serializer_timestamp Steel.ST.Array.pts_to_length FStar.Ghost.erased Steel.ST.Util.elim_exists FStar.UInt32.t Zeta.Steel.IV.serialize_timestamp FStar.UInt8.t FStar.SizeT.v Prims.squash Prims.b2t Prims.op_LessThanOrEqual FStar.SizeT.uint_to_t Steel.ST.Array.ghost_split Zeta.Steel.IV.seq_suffix_is_zero_elim
let serialize_iv (a: byte_array{A.length a == 96}) (v: timestamp)
    : Steel.ST.Util.STT unit
      (exists_ (fun bs ->
              (A.pts_to a full_perm bs) `star` (pure (seq_suffix_is_zero bs timestamp_len))))
      (fun slice_len ->
          exists_ (fun (bs: _) ->
                (A.pts_to a full_perm bs)
                `star`
                (pure (seq_suffix_is_zero bs timestamp_len /\ spec_serializer_iv v == bs)))) =
  
let bs = elim_exists () in
A.pts_to_length a bs;
elim_pure _;
seq_suffix_is_zero_elim bs timestamp_len;
let adj = A.ghost_split a 8sz in
let n = serialize_timestamp (A.split_l a 8sz) v in
let bs_l = elim_exists () in
A.pts_to_length (A.split_l a 8sz) bs_l;
elim_pure _;
assert_ ((A.pts_to (A.split_l a 8sz) full_perm bs_l)
    `star`
    (A.pts_to (A.split_r a 8sz) full_perm (Seq.slice bs 8 (Seq.length bs))));
A.ghost_join (A.split_l a 8sz) (A.split_r a 8sz) adj;
rewrite (A.pts_to (A.merge (A.split_l a 8sz) (A.split_r a 8sz)) _ _)
  (A.pts_to a full_perm (spec_serializer_iv v));
intro_pure (seq_suffix_is_zero (spec_serializer_iv v) timestamp_len /\
    spec_serializer_iv v == spec_serializer_iv v);
return ()