/// Moving on to something more exciting, we now strive to implement a
/// RingBuffer with push and pop operations.

module RingBuffer1


/// We define the canonical abbreviations, taking care to shadow ST to make sure
/// we don't end up referring to FStar.ST by accident.
module B = LowStar.Buffer
module U32 = FStar.UInt32
module HS = FStar.HyperStack
module M = LowStar.Modifies
module ST = FStar.HyperStack.ST
module S = FStar.Seq

/// This brings into scope the ``!*`` and ``*=`` operators, which are
/// specifically designed to operate on buffers of size 1, i.e. on pointers.
open LowStar.BufferOps
open FStar.HyperStack.ST

/// A ringbuffer is a view over a buffer, with a start index, a length (i.e. how
/// many elements are currently being stored) and a total length (i.e. the size
/// of the underlying ``b``). We chose this style, as opposed to a pair of
/// ``first`` and ``last`` indices, because it avoids modular arithmetic which
/// would be difficult to reason about.
noeq
type t a = {
  b: B.buffer a;
  first: B.pointer U32.t;
  length: B.pointer U32.t;
  total_length: U32.t
}

/// To facilitate writing predicates, we define a handy shortcut that is the
/// reflection of the ``!*`` operator at the proof level.
unfold
let deref #a (h: HS.mem) (x: B.pointer a) = B.get h x 0

/// You are expected to fill out this predicate, capturing memory safety,
/// disjointness and relations between the length and the indices.
let well_formed #a (h: HS.mem) (x: t a) =
  True


/// Once you have defined a suitable well-formedness predicate, you are expected
/// to fill out the implementation of pop, which simply mutates the ``first`` field.
let pop (#a: eqtype) (x: t a): Stack a
  (requires fun h ->
    True) // improve the precondition
  (ensures fun h0 r h1 ->
    True) // improve the postcondition
=
  admit ()

/// Once this is done, write out a memory-safe push, without any functional
/// specification. Push is slightly harder, and will require something beyond
/// just well-formedness in the precondition.
let push (#a: eqtype) (x: t a) (e: a): Stack unit
  (requires fun h ->
    True)
  (ensures fun h0 _ h1 ->
    True)
=
  admit ()