let frozen_until (s:Seq.seq u8{Seq.length s >= 4}) = le_to_n (Seq.slice s 0 4)
let frozen_until (s: Seq.seq u8 {Seq.length s >= 4}) =
le_to_n (Seq.slice s 0 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
FStar.Seq.Base.seq LowStar.PrefixFreezableBuffer.u8 Prims.b2t Prims.op_GreaterThanOrEqual FStar.Seq.Base.length LowStar.PrefixFreezableBuffer.le_to_n FStar.Seq.Base.slice Prims.nat
(*
   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
val frozen_until : s: FStar.Seq.Base.seq LowStar.PrefixFreezableBuffer.u8 {FStar.Seq.Base.length s >= 4} -> Prims.nat
s: FStar.Seq.Base.seq LowStar.PrefixFreezableBuffer.u8 {FStar.Seq.Base.length s >= 4} -> Prims.nat