/// This is a continuation of the previous exercise. We start with the answers
/// from RingBuffer1, then present more challenges.
module RingBuffer2
/// 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
/// A first version of the well-formedness predicate for ring buffers. This
/// predicate refers to a sequence, not a buffer, and therefore does not need
/// the memory. It is useful in this module to have two versions of predicates:
/// one that takes into account the memory, disjointness, etc. and another one
/// that only focuses on index arithmetic. Nothing surprising here. Note that
/// zero-sized ringbuffers are not allowed.
let well_formed_f #a (b: S.seq a) (first length total_length: U32.t) =
let open U32 in
S.length b = v total_length /\
length <=^ total_length /\
first <^ total_length /\
total_length >^ 0ul
/// Same predicate as above, but this time operating on a memory state and using
/// a stateful ringbuffer.
let well_formed #a (h: HS.mem) (x: t a) =
B.live h x.b /\ B.live h x.first /\ B.live h x.length /\
M.(loc_disjoint (loc_buffer x.b) (loc_buffer x.first)) /\
M.(loc_disjoint (loc_buffer x.b) (loc_buffer x.length)) /\
M.(loc_disjoint (loc_buffer x.first) (loc_buffer x.length)) /\
well_formed_f (B.as_seq h x.b) (deref h x.first) (deref h x.length) x.total_length
/// We next define operators for moving around the ringbuffer with wraparound
/// semantics. Defining this using a modulo operator is not a good idea, because:
/// - writing ``i +^ 1ul %^ total_length`` may overflow
/// - Z3 is notoriously bad at reasoning with modular arithmetic.
/// So, instead, we just do a simple branch.
let next (i total_length: U32.t): Pure U32.t
(requires U32.(total_length >^ 0ul /\ i <^ total_length))
(ensures fun r -> U32.( r <^ total_length ))
=
let open U32 in
if i =^ total_length -^ 1ul then
0ul
else
i +^ 1ul
let prev (i total_length: U32.t): Pure U32.t
(requires U32.(total_length >^ 0ul /\ i <^ total_length))
(ensures fun r -> U32.( r <^ total_length ))
=
let open U32 in
if i >^ 0ul then
i -^ 1ul
else
total_length -^ 1ul
/// These two are useful from the client's perspective, to capture how many slots
/// are left in the buffer.
let remaining_space #a (h: HS.mem) (x: t a { well_formed h x }) =
U32.( x.total_length -^ (deref h x.length) )
let space_left #a (h: HS.mem) (x: t a { well_formed h x }) =
U32.( remaining_space h x >^ 0ul )
/// A predicate over indices that captures whether a given entry in the buffer
/// is occupied. Once again, we avoid modular arithmetic by branching.
let used_slot_f (first length total_length i: U32.t) =
let first = U32.v first in
let length = U32.v length in
let total_length = U32.v total_length in
let i = U32.v i in
first <= i /\ i < first + length \/
first <= i + total_length /\ i + total_length < first + length
/// Same thing, but over a memory and the actual references.
let used_slot #a (h: HS.mem) (x: t a { well_formed h x }) (i: U32.t) =
let first = deref h x.first in
let length = deref h x.length in
let total_length = x.total_length in
used_slot_f first length total_length i
/// The goal is now to reflect a given ringbuffer in a given heap as a list, so
/// that we can provide a functional specification for pop. Please fill out this predicate.
let as_list #a (h: HS.mem) (x: t a): Ghost (list a)
(requires well_formed h x)
(ensures fun _ -> True)
=
admit ()
/// Now, enrich the pre- and post-conditions of pop to add a functional
/// specification, then write out the body.
let pop (#a: eqtype) (x: t a): Stack a
(requires fun h ->
well_formed h x /\ U32.(deref h x.length >^ 0ul))
(ensures fun h0 r h1 ->
well_formed h1 x /\
M.(modifies (loc_union (loc_buffer x.length) (loc_buffer x.first)) h0 h1) /\
U32.(remaining_space h1 x = remaining_space h0 x +^ 1ul) /\ (
True)) // fill out here!
=
admit ()