Capucine Example: Sparse Arrays

ocamlbuild bench/sparse.gwhy

(* VACID Challenge: Sparse Arrays *)
(* version RTE: we want to check for Run Time Errors, that is the absence
of out-of-bounds array acces *)

(* Logic (Infinite) Arrays *)
logic type array (alpha)
logic function store (array (alpha), int, alpha): array (alpha)
logic function select (array (alpha), int): alpha

axiom select_eq:
  forall a: array (alpha).
  forall i: int.
  forall v: alpha.
  [select(store(a, i, v), i)] = [v]

axiom select_neq:
  forall a: array (alpha).
  forall i: int.
  forall j: int.
  forall v: alpha.
  [i] <> [j] ==>
  [select(store(a, i, v), j)] = [select(a, j)]

(* Array Reference *)
selector (length, cell)
class Array (alpha) =
  (int * array (alpha))
  invariant(a) = [0] <= [a.length]
end

val array_get(a: Array (alpha) [R], i:int) : alpha
  requires [0] <= [i] and [i] < [!a.length]
  ensures [result] = [select(!a.cell,i)] =
      select(!a.cell,i)

val array_set(a: Array (alpha) [R], i:int, v:a) : unit
  consumes R^c
  produces R^c
  requires [0] <= [i] and [i] < [!a.length]
  ensures [!a.length] = [old(!a.length)] and
          [!a.cell] = [store(old(!a.cell),i,v)]
  =
      (a := (!a.length, store(!a.cell,i,v)))

val array_create(size:int): Array (alpha) [R]
  consumes R^e
  produces R^c
  requires [0] <= [size]
  ensures [!result.length] = [size] =
    let tmp = new Array (alpha) in
    tmp := (size, !tmp.cell);
    tmp

(* Sparse Arrays *)

predicate interval(a:int, x:int, b:int) = [a] <= [x] and [x] < [b]

selector (value, idx, back, n, default, size)
(* value: actual values at their actual indexes
   idx: corresponding indexes in back
   back: corresponding indexes in idx, makes sense between 0 and n-1
   n: see back
   size: allocated size
*)

class Sparse (alpha) =
  own Rval, Ridx, Rback;

  (Array (alpha) [Rval] * Array (int) [Ridx] * Array (int) [Rback] *
   int * alpha * int)

  invariant (x) =
    [0] <= [x.n] and [x.n] <= [x.size] and
    [!(x.value).length] = [x.size] and
    [!(x.idx).length] = [x.size] and
    [!(x.back).length] = [x.size] and
    forall i: int. interval([0],[i],[x.n]) ==>
      interval([0],[select (!(x.back).cell, i)],[x.size]) and
      [select (!(x.idx).cell, select (!(x.back).cell, i))] = [i]
end

(* is_elt(a,i) tells whether index i points to a existing element. It
  can be checked as follows:

  (1) check that array idx maps i to a index j between 0 and n (excluded)
  (2) check that back(j) is i
*)

predicate is_elt(a: Sparse (alpha) [R], i: int) =
  [0] <= [select (!(!a.idx).cell, i)]
  and [select (!(!a.idx).cell, i)] < [!a.n]
  and [select (!(!a.back).cell, select (!(!a.idx).cell, i))] = [i]

logic function model (Sparse (alpha) [R], int): alpha

axiom model_in:
  forall a: Sparse (alpha) [R].
  forall i: int.
  is_elt([a], [i]) ==> [model(a, i)] = [select(!(!a.value).cell, i)]

axiom model_out:
  forall a: Sparse (alpha) [R].
  forall i: int.
  not is_elt([a], [i]) ==> [model(a, i)] = [!a.default]

val create(sz:int, def: alpha): Sparse (alpha) [R]
  consumes R^e
  produces R^c
  requires
    [0] <= [sz]
  ensures
    [!result.size] = [sz] and
    forall i: int. [model (result, i)] = [def]
  =
    let arr = new Sparse (alpha) in
    arr := (array_create (sz), array_create (sz),
            array_create (sz), 0, def, sz);
    arr

val get(a: Sparse (alpha) [R], i: int): alpha
  consumes R^c
  produces R^c
  requires [0] <= [i] and [i] < [!a.size]
  ensures [result] = [model(a, i)] =
    let index = array_get(!a.idx, i) in
    if 0 <= index and index < !a.n and array_get(!a.back, index) = i
    then
      array_get(!a.value, i)
    else
      !a.default

(* array maps [0;n[ into [0;k[ *)
predicate into(n:int, k:int, t:array(int)) =
  forall i:int. interval(0,i,n) ==> interval(0,[select(t,i)],k)

predicate injective(n:int, t:array(int)) =
  (forall i:int. forall j:int. interval(0,i,n) ==> interval(0,j,n) ==>
      [select(t,i)] = [select(t,j)] ==> i = j)

predicate surjective(n:int, t:array(int)) =
  forall k:int. interval(0,k,n) ==>
    exists j:int. interval(0,j,n) and [select(t,j)] = k

lemma array_injective_is_surjective:
  forall n:int. forall a:array(int).
  into(n,n,a) and injective(n,a) ==> surjective(n,a)

val set(a: Sparse (alpha) [R], i: int, v: alpha): unit
  consumes R^c
  produces R^c
  requires [0] <= [i] and [i] < [!a.size]
  ensures
    [!a.size] = [old(!a.size)] and
    (forall j: int. (* [0] <= [j] and [j] < [!a.size] and  *)
        [j] <> [i] ==> [model(a, j)] = [old(model(a, j))])
    and ([model(a, i)] = [v])
  =
    array_set((focus !a.value), i, v);
    let index = array_get(!a.idx, i) in
    if not (0 <= index and index < !a.n and array_get(!a.back, index) = i)
    then (
      (* array back maps [0;n[ into [0;size[ *)
      assert into([!a.n],[!a.size],[!(!a.back).cell]);
      (* array back is injective *)
      assert injective([!a.n],[!(!a.back).cell]);
      (* if n=size then array back is also surjective *)
      assert [!a.n] = [!a.size] ==> surjective([!a.n],[!(!a.back).cell]);
      assert [!a.n] = [!a.size] ==>
       interval(0,i,[!a.n]) ==>
        exists j:int.
          interval(0,j,[!a.n]) and [select(!(!a.back).cell,j)] = i;
        (* the hard assertion! *)
        assert [!a.n] < [!a.size];
        array_set((focus !a.idx), i, !a.n);
        array_set((focus !a.back), !a.n, i);
        a := (!a.value, !a.idx, !a.back, !a.n + 1, !a.default, !a.size)
    )

val main(): unit =
  region Ra: Sparse (int) in
  region Rb: Sparse (int) in
  let default = 0 in
  let a = (create(10,default): Sparse (int) [Ra]) in
  let b = (create(20,default): Sparse (int) [Rb]) in
  let x = get(a, 5) in
  let y = get(b, 7) in
  assert ([x] = [default] and [y] = [default]);
  set(a, 5, 1);
  set(b, 7, 2);
  let x = get(a, 5) in
  let y = get(b, 7) in
  assert ([x] = [1] and [y] = [2]);
  let x = get(a, 7) in
  let y = get(b, 5) in
  assert ([x] = [default] and [y] = [default]);
  let x = get(a, 0) in
  let y = get(b, 0) in
  assert ([x] = [default] and [y] = [default]);
  let x = get(a, 9) in
  let y = get(b, 9) in
  assert ([x] = [default] and [y] = [default])
(*
;
  assert false (* poorman's check for inconsistency *)
*)