(* The 2nd Verified Software Competition (VSTTE 2012)
   https://sites.google.com/site/vstte2012/compet

   Problem 3:
   Queue data structure implemented using a ring buffer

   Alternative solution using a model stored in a ghost field *)

module RingBuffer

  use int.Int
  use option.Option
  use list.List
  use import list.NthLengthAppend as L
  use import array.Array as A

  type buffer 'a = {
    mutable first: int;
    mutable len  : int;
            data : array 'a;
    ghost mutable sequence: list 'a;
  }
  invariant {
    let size = A.length data in
    0 <= first <  size /\
    0 <= len   <= size /\
    len = L.length sequence /\
    forall i: int. 0 <= i < len ->
      (first + i < size ->
         nth i sequence = Some data[first + i]) /\
      (0 <= first + i - size ->
         nth i sequence = Some data[first + i - size])
  }
  by { first = 0; len = 0; data = make 1 (any 'a); sequence = Nil }

  (* total capacity of the buffer *)
  function size (b: buffer 'a) : int = A.length b.data

  (* length = number of elements *)
  function length (b: buffer 'a) : int = b.len

  (* code *)

  let create (n: int) (dummy: 'a) : buffer 'a
    requires { n > 0 }
    ensures  { size result = n }
    ensures  { result.sequence = Nil }
  = { first = 0; len = 0; data = make n dummy; sequence = Nil }

  let length (b: buffer 'a) : int
    ensures { result = length b }
  = b.len

  let clear (b: buffer 'a) : unit
    writes  { b.len, b.sequence }
    ensures { length b = 0 }
    ensures { b.sequence = Nil }
  = ghost (b.sequence <- Nil);
    b.len <- 0

  let push (b: buffer 'a) (x: 'a) : unit
    requires { length b < size b }
    writes   { b.data.elts, b.len, b.sequence }
    ensures  { length b = (old (length b)) + 1 }
    ensures  { b.sequence = (old b.sequence) ++ Cons x Nil }
  = ghost (b.sequence <- b.sequence ++ Cons x Nil);
    let i = b.first + b.len in
    let n = A.length b.data in
    b.data[if i >= n then i - n else i] <- x;
    b.len <- b.len + 1

  let head (b: buffer 'a) : 'a
    requires { length b > 0 }
    ensures  { match b.sequence with Nil -> false | Cons x _ -> result = x end }
  = b.data[b.first]

  let pop (b: buffer 'a) : 'a
    requires { length b > 0 }
    writes   { b.first, b.len, b.sequence }
    ensures  { length b = (old (length b)) - 1 }
    ensures  { match old b.sequence with
               | Nil -> false
               | Cons x l -> result = x /\ b.sequence = l end }
  = ghost match b.sequence with Nil -> absurd | Cons _ s -> b.sequence <- s end;
    let r = b.data[b.first] in
    b.len <- b.len - 1;
    let n = A.length b.data in
    b.first <- b.first + 1;
    if b.first = n then b.first <- 0;
    r
end

module Harness

  use RingBuffer
  use list.List

  let harness () =
    let b = create 10 0 in
    push b 1;
    push b 2;
    push b 3;
    let x = pop b in assert { x = 1 };
    let x = pop b in assert { x = 2 };
    let x = pop b in assert { x = 3 };
    ()

  let harness2 () =
    let b = create 3 0 in
    push b 1;
    assert { sequence b = Cons 1 Nil };
    push b 2;
    assert { sequence b = Cons 1 (Cons 2 Nil) };
    push b 3;
    assert { sequence b = Cons 1 (Cons 2 (Cons 3 Nil)) };
    let x = pop b in assert { x = 1 };
    assert { sequence b = Cons 2 (Cons 3 Nil) };
    push b 4;
    assert { sequence b = Cons 2 (Cons 3 (Cons 4 Nil)) };
    let x = pop b in assert { x = 2 };
    assert { sequence b = Cons 3 (Cons 4 Nil) };
    let x = pop b in assert { x = 3 };
    assert { sequence b = Cons 4 Nil };
    let x = pop b in assert { x = 4 };
    ()

  use int.Int

  let test (x: int) (y: int) (z: int) =
    let b = create 2 0 in
    push b x;
    push b y;
    assert { sequence b = Cons x (Cons y Nil) };
    let h = pop b in assert { h = x };
    assert { sequence b = Cons y Nil };
    push b z;
    assert { sequence b = Cons y (Cons z Nil) };
    let h = pop b in assert { h = y };
    let h = pop b in assert { h = z }

end

With sequences instead of lists

module RingBufferSeq

  use int.Int
  use import seq.Seq as S
  use import array.Array as A

  type buffer 'a = {
    mutable first: int;
    mutable len  : int;
            data : array 'a;
    ghost mutable sequence: S.seq 'a;
  }
  invariant {
    let size = A.length data in
    0 <= first <  size /\
    0 <= len   <= size /\
    len = S.length sequence /\
    forall i: int. 0 <= i < len ->
      (first + i < size ->
         S.get sequence i = data[first + i]) /\
      (0 <= first + i - size ->
         S.get sequence i = data[first + i - size])
  }
  by { first = 0; len = 0; data = make 1 (any 'a); sequence = S.empty }

  (* total capacity of the buffer *)
  function size (b: buffer 'a) : int = A.length b.data

  (* length = number of elements *)
  function length (b: buffer 'a) : int = b.len

  (* code *)

  let create (n: int) (dummy: 'a) : buffer 'a
    requires { n > 0 }
    ensures  { size result = n }
    ensures  { result.sequence = S.empty }
  = { first = 0; len = 0; data = make n dummy; sequence = S.empty }

  let length (b: buffer 'a) : int
    ensures { result = length b }
  = b.len

  let clear (b: buffer 'a) : unit
    writes  { b.len, b.sequence }
    ensures { length b = 0 }
    ensures { b.sequence = S.empty }
  = ghost (b.sequence <- S.empty);
    b.len <- 0

  let push (b: buffer 'a) (x: 'a) : unit
    requires { length b < size b }
    writes   { b.data.elts, b.len, b.sequence }
    ensures  { length b = (old (length b)) + 1 }
    ensures  { b.sequence = S.snoc (old b.sequence) x }
  = ghost (b.sequence <- S.snoc b.sequence x);
    let i = b.first + b.len in
    let n = A.length b.data in
    b.data[if i >= n then i - n else i] <- x;
    b.len <- b.len + 1

  let head (b: buffer 'a) : 'a
    requires { length b > 0 }
    ensures  { result = S.get b.sequence 0 }
  = b.data[b.first]

  let pop (b: buffer 'a) : 'a
    requires { length b > 0 }
    writes   { b.first, b.len, b.sequence }
    ensures  { length b = (old (length b)) - 1 }
    ensures  { result = S.get (old b.sequence) 0 }
    ensures  { b.sequence = (old b.sequence)[1..] }
  = ghost (b.sequence <- b.sequence[1..]);
    let r = b.data[b.first] in
    b.len <- b.len - 1;
    let n = A.length b.data in
    b.first <- b.first + 1;
    if b.first = n then b.first <- 0;
    r
end

module HarnessSeq

  use seq.Seq
  use RingBufferSeq

  let harness () =
    let b = create 10 0 in
    push b 1;
    push b 2;
    push b 3;
    let x = pop b in assert { x = 1 };
    let x = pop b in assert { x = 2 };
    let x = pop b in assert { x = 3 };
    ()

  let harness2 () =
    let b = create 3 0 in
    push b 1;
    assert { sequence b == cons 1 empty };
    push b 2;
    assert { sequence b == cons 1 (cons 2 empty) };
    push b 3;
    assert { sequence b == cons 1 (cons 2 (cons 3 empty)) };
    let x = pop b in assert { x = 1 };
    assert { sequence b == cons 2 (cons 3 empty) };
    push b 4;
    assert { sequence b == cons 2 (cons 3 (cons 4 empty)) };
    let x = pop b in assert { x = 2 };
    assert { sequence b == cons 3 (cons 4 empty) };
    let x = pop b in assert { x = 3 };
    assert { sequence b == cons 4 empty };
    let x = pop b in assert { x = 4 };
    ()

  use int.Int

  let test (x: int) (y: int) (z: int) =
    let b = create 2 0 in
    push b x;
    push b y;
    assert { sequence b == cons x (cons y empty) };
    let h = pop b in assert { h = x };
    assert { sequence b == cons y empty };
    push b z;
    assert { sequence b == cons y (cons z empty) };
    let h = pop b in assert { h = y };
    let h = pop b in assert { h = z }

end