import Base
import ./lib.bend as R

# Construction and empty-state laws.
law empty_is_new:
  for c: Nat
  { R.RingBuf.empty(c) == R.RingBuf.new(c) : R.RingBuf }

law capacity_new:
  for c: Nat
  { R.RingBuf.capacity(R.RingBuf.new(c)) == c : Nat }

law length_new:
  for c: Nat
  { R.RingBuf.length(R.RingBuf.new(c)) == 0n : Nat }

law empty_new:
  for c: Nat
  { R.RingBuf.is_empty(R.RingBuf.new(c)) == True{} : Bool }

law new_zero:
  { R.RingBuf.new(0n) == R.RB{0n, 0n, 0n, Nil{}} : R.RingBuf }

law new_one:
  { R.RingBuf.new(1n) == R.RB{1n, 0n, 0n, 0 <> Nil{}} : R.RingBuf }

# Empty observations and zero-capacity behavior.
law pop_empty:
  for c: Nat
  { R.RingBuf.pop(R.RingBuf.new(c)) == None{} : Maybe<&2, R.RingBuf.Pop> }

law peek_empty:
  for c: Nat
  { R.RingBuf.peek(R.RingBuf.new(c)) == None{} : Maybe<&2, U32> }

law to_list_empty:
  { R.RingBuf.to_list(R.RingBuf.new(0n)) == Nil{} : List<&2, U32> }

law zero_push_fails:
  for x: U32
  { R.RingBuf.push(R.RingBuf.new(0n), x) == None{} : Maybe<&2, R.RingBuf.Push> }

law zero_is_full:
  { R.RingBuf.is_full(R.RingBuf.new(0n)) == True{} : Bool }

# Singleton push/pop/peek behavior.
law push_one:
  for x: U32
  {
    R.RingBuf.push(R.RingBuf.new(1n), x)
      == Some{R.PushResult{R.RB{1n, 0n, 1n, x <> Nil{}}}}
    : Maybe<&2, R.RingBuf.Push>
  }

law one_is_full_after_push:
  for x: U32
  {
    R.RingBuf.is_full(R.RB{1n, 0n, 1n, x <> Nil{}}) == True{} : Bool
  }

law push_full_fails:
  for x: U32
  for y: U32
  {
    R.RingBuf.push(R.RB{1n, 0n, 1n, x <> Nil{}}, y)
      == None{}
    : Maybe<&2, R.RingBuf.Push>
  }

law peek_one:
  for x: U32
  {
    R.RingBuf.peek(R.RB{1n, 0n, 1n, x <> Nil{}})
      == Some{x}
    : Maybe<&2, U32>
  }

law pop_one:
  for x: U32
  {
    R.RingBuf.pop(R.RB{1n, 0n, 1n, x <> Nil{}})
      == Some{R.PopResult{x, R.RB{1n, 0n, 0n, x <> Nil{}}}}
    : Maybe<&2, R.RingBuf.Pop>
  }

law to_list_one:
  for x: U32
  {
    R.RingBuf.to_list(R.RB{1n, 0n, 1n, x <> Nil{}})
      == x <> Nil{}
    : List<&2, U32>
  }

# A two-slot buffer demonstrates FIFO order and physical wrap-around.
law to_list_two:
  for x: U32
  for y: U32
  {
    R.RingBuf.to_list(R.RB{2n, 0n, 2n, x <> y <> Nil{}})
      == x <> y <> Nil{}
    : List<&2, U32>
  }

law pop_two:
  for x: U32
  for y: U32
  {
    R.RingBuf.pop(R.RB{2n, 0n, 2n, x <> y <> Nil{}})
      == Some{R.PopResult{x, R.RB{2n, 1n, 1n, x <> y <> Nil{}}}}
    : Maybe<&2, R.RingBuf.Pop>
  }

law wrapped_push:
  for x: U32
  for y: U32
  for z: U32
  {
    R.RingBuf.push(R.RB{2n, 1n, 1n, x <> y <> Nil{}}, z)
      == Some{R.PushResult{R.RB{2n, 1n, 2n, z <> y <> Nil{}}}}
    : Maybe<&2, R.RingBuf.Push>
  }

law wrapped_to_list:
  for x: U32
  for y: U32
  {
    R.RingBuf.to_list(R.RB{2n, 1n, 2n, x <> y <> Nil{}})
      == y <> x <> Nil{}
    : List<&2, U32>
  }

law length_full:
  for x: U32
  for y: U32
  {
    R.RingBuf.length(R.RB{2n, 1n, 2n, x <> y <> Nil{}}) == 2n : Nat
  }