let lbuffer (len:u32) =
  b:buffer{length b == U32.v len + 4}
let lbuffer (len: u32) =
b: buffer{length b == U32.v len + 4}
LowStar.PrefixFreezableBuffer.fsti.checked
prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Preorder.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
LowStar.PrefixFreezableBuffer.fsti
LowStar.PrefixFreezableBuffer.u32 LowStar.PrefixFreezableBuffer.buffer Prims.eq2 Prims.int LowStar.Monotonic.Buffer.length LowStar.PrefixFreezableBuffer.u8 LowStar.PrefixFreezableBuffer.prefix_freezable_preorder Prims.op_Addition FStar.UInt32.v
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module LowStar.PrefixFreezableBuffer

open FStar.HyperStack.ST

include LowStar.Monotonic.Buffer

module P = FStar.Preorder
module G = FStar.Ghost

module U32 = FStar.UInt32
module Seq = FStar.Seq

module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST

(*
 * A library for prefix freezable buffers of elements of type u8
 *
 * Our monotonicity theory does not easily support preorders and predicates over
 *   multiple references. So instead of keeping the frozen-until counter in a
 *   separate (ghost) reference, the library maintains the frozen-until counter (a u32)
 *   in the first four bytes of the buffer itself
 *
 * Buffer contents up to the frozen-until counter are stable and clients can witness
 *   and recall them
 *
 *)

type u8 = UInt8.t
type u32 = U32.t

#set-options "--max_fuel 0 --max_ifuel 0"


/// This is the frozen until index in the sequence representation of a PrefixFreezableBuffer

val le_to_n (s:Seq.seq u8) : Tot nat

let frozen_until (s:Seq.seq u8{Seq.length s >= 4}) = le_to_n (Seq.slice s 0 4)


/// Preorder for PrefixFreezableBuffers

private unfold let pre (s1 s2:Seq.seq u8) =
  Seq.length s1 == Seq.length s2 /\  //lengths are same
  (let len = Seq.length s1 in
   len >= 4 ==>  //if length >= 4 then
   (let frozen_until1 = frozen_until s1 in
    let frozen_until2 = frozen_until s2 in
    (4 <= frozen_until1 /\ frozen_until1 <= len) ==>  //if frozen_until1 is in the range [4, len] then
    (frozen_until1 <= frozen_until2 /\ frozen_until2 <= len /\  //frozen until index increases monotonically, but remains <= len
     (forall (i:nat).{:pattern Seq.index s2 i}
        (4 <= i /\ i < frozen_until1) ==> Seq.index s2 i == Seq.index s1 i))))  //and the contents until frozen_until1 remain same


val prefix_freezable_preorder : srel u8

/// Clients can call the following lemma to reveal the preorder

val prefix_freezable_preorder_elim (s1 s2:Seq.seq u8)
  : Lemma (prefix_freezable_preorder s1 s2 <==> pre s1 s2)


/// Predicate for the frozen_until index being at least n
///
/// It is stable w.r.t. the prefix_freezable_preorder

let frozen_until_at_least (n:nat) : spred u8 =
  fun s -> Seq.length s >= 4 /\  //it follows from the inequalities below, but we need it for typing of frozen_until
  
  4 <= n /\ n <= frozen_until s /\ frozen_until s <= Seq.length s


/// Predicate for the frozen slice with indices in the [4, frozen_until) range
///
/// It is stable w.r.t. the prefix_freezable_preorder

let slice_is (i j:u32) (snap:G.erased (Seq.seq u8)) : spred u8 =
  fun s -> let len = Seq.length s in len >= 4 /\  //for typing of frozen_until
  (let frozen_until = frozen_until s in
   let i = U32.v i in
   let j = U32.v j in
   let snap = G.reveal snap in
   4 <= i /\ i <= j /\ j <= frozen_until /\ frozen_until <= len /\
   Seq.length snap == j - i /\
   Seq.equal (Seq.slice s i j) snap)


/// Buffer type for PrefixfreezableBuffers
///
/// And abbreviation for the length indexed version

type buffer =
  b:mbuffer u8 (prefix_freezable_preorder) (prefix_freezable_preorder)
    {length b >= 4 /\ b `witnessed` frozen_until_at_least 4}
val lbuffer : len: LowStar.PrefixFreezableBuffer.u32 -> Type0
len: LowStar.PrefixFreezableBuffer.u32 -> Type0