Capucine Example: Sparse Arrays

make examples/sparse.gwhy

type larray ('a)

logic store (a: larray ('a), i: int, v: 'a): larray ('a)

logic select (a: larray ('a), i: int): 'a

axiom select_eq:
  forall a: larray ('a).
  forall i: int.
  forall v: 'a.
  select(store(a, i, v), i) = v

axiom select_neq:
  forall a: larray ('a).
  forall i: int.
  forall j: int.
  forall v: 'a.
  i <> j ==>
  select(store(a, i, v), j) = select(a, j)

class array ('a)
{
  length: int;
  contents: larray ('a);
  invariant length >= 0
}

fun array_create [R: array ('a)] (size: int): [R]
  consumes R^e
  produces R^c
  pre size >= 0
  post get(R, result, length) = size
{
  let res = new [R];
  res.length <- size;
  return res
}

fun array_get [R: array ('a)] (a: [R], i: int): 'a
  consumes R^c
  produces R^c
  pre 0 <= i && i < get(R, a, length)
  post result = select(get(R, a, contents), i)
{
  return #select(a.contents, i)
}

fun array_set [R: array ('a)] (a: [R], i: int, v: 'a): unit
  consumes R^c
  produces R^c
  pre 0 <= i && i < get(R, a, length)
  post
    get(R, a, contents) = store(get(R, a, contents)@pre, i, v) &&
    get(R, a, length) = get(R, a, length)@pre
{
  use invariant a;
  a.contents <- #store(a.contents, i, v);
}

logic interval (a: int, x: int, b: int) = a <= x && x < b

class sparse ('a)
{
  single Rvalue: array ('a);
  single Ridx: array (int);
  single Rback: array (int);
  value: [Rvalue];
  idx: [Ridx];
  back: [Rback];
  n: int;
  default: 'a;
  size: int;
  invariant
    0 <= n && n <= size &&
    get(Rvalue, value, length) = size &&
    get(Ridx, idx, length) = size &&
    get(Rback, back, length) = size &&
    forall i: int.
    interval(0, i, n) ==>
    interval(0, select(get(Rback, back, contents), i), size) &&
    select(get(Ridx, idx, contents), select(get(Rback, back, contents), i)) = i
}

logic is_elt [R: sparse ('a)] (a: [R], i: int) =
  interval(
    0,
    select(
      get(get(R, a, Ridx), get(R, a, idx), contents),
      i
    ),
    get(R, a, n)) &&
  select(
    get(get(R, a, Rback), get(R, a, back), contents),
    select(
      get(get(R, a, Ridx), get(R, a, idx), contents),
      i
    )
  ) = i

logic model [R: sparse ('a)] (a: [R], i: int): 'a

axiom model_in:
  forall region R: sparse ('a).
  forall a: [?].
  (* pas besoin de "a in R" : on est en train de définir "model" *)
  forall i: int.
  is_elt [R] (a, i) ==>
  model [R] (a, i) =
    select(get(get(R, a, Rvalue), get(R, a, value), contents), i)

axiom model_out:
  forall region R: sparse ('a).
  forall a: [?].
  (* pas besoin de "a in R" : on est en train de définir "model" *)
  forall i: int.
  not is_elt [R] (a, i) ==>
  model [R] (a, i) = get(R, a, default)

(* Sans chapeaux : prouvé entièrement par CVC3 grâce à l'assert.
   Avec chapeaux : prouvé entièrement par Alt-Ergo sans l'assert. *)
fun create [R: sparse ('a)] (sz: int, def: 'a): [R]
  consumes R^e
  produces R^c
  pre 0 <= sz
  post
    get(R, result, size) = sz &&
    forall i: int. model [R] (result, i) = def
{
  let a = new [R];
  let a_value = array_create [a.Rvalue] (sz);
  a.value <- a_value;
  let a_idx = array_create [a.Ridx] (sz);
  a.idx <- a_idx;
  let a_back = array_create [a.Rback] (sz);
  a.back <- a_back;
  a.n <- 0;
  a.default <- def;
  a.size <- sz;
(*  assert forall i: int. not (is_elt [R] (a, i));*)
  return a
}

class Ref ('a)
{
  ref_value: 'a;
}

(* Sans chapeaux : prouvé entièrement par CVC3 grâce à l'assert.
   Avec chapeaux : prouvé entièrement par Alt-Ergo sans l'assert. *)
(* TODO: read-only permission for array_get, so as not to have to unpack a *)
fun sget [R: sparse ('a)] (a: [R], i: int): 'a
  consumes R^c
  produces R^c
  pre interval(0, i, get(R, a, size))
  post result = model [R] (a, i)
{
  use invariant a;
  let index = array_get(a.idx, i); (* unpack inféré pour récupérer a.idx^c *)
  let region Rres: Ref ('a);
  let res = new [Rres];
  if 0 <= index && index < a.n then
  {
    let back_index = array_get(a.back, index);
    if back_index = i then
    {
      let value_i = array_get(a.value, i);
      res.ref_value <- value_i;
    }
    else
    {
      res.ref_value <- a.default;
    };
  }
  else
  {
(*    assert not (is_elt [R] (a, i));*)
    res.ref_value <- a.default;
  };
  return res.ref_value
}

(* pas besoin de focus, grâce au "single" dans la définition de la classe *)
(* le assert final est inutile avec les chapeaux et c'est même plus
   rapide en l'enlevant *)
fun sset [R: sparse ('a)] (a: [R], i: int, v: 'a): unit
  consumes R^c
  produces R^c
  pre interval(0, i, get(R, a, size))
  post
    get(R, a, size) = get(R, a, size)@pre &&
    (forall j: int. j <> i ==> model [R] (a, j) = model [R] (a, j)@pre) &&
    model [R] (a, i) = v
{
  use invariant a;

  let x = array_set [a.Rvalue] (a.value, i, v);
  let index = array_get [a.Ridx] (a.idx, i);

  if 0 <= index && index < a.n then
  {
    let back_index = array_get [a.Rback] (a.back, index);
    if back_index = i then
    {
(*      assert is_elt [R] (a, i);*)
    }
    else
    {
      assert get(R, a, n) < get(R, a, size); (* pigeons *)
(*      assert not (is_elt [R] (a, i));*)
      let x = array_set [a.Ridx] (a.idx, i, a.n);
      let x = array_set [a.Rback] (a.back, a.n, i);
      a.n <- a.n + 1;
(*      assert is_elt [R] (a, i);*)
    };
  }
  else
  {
    assert get(R, a, n) < get(R, a, size); (* pigeons *)
(*    assert not (is_elt [R] (a, i));*)
    let x = array_set [a.Ridx] (a.idx, i, a.n);
    let x = array_set [a.Rback] (a.back, a.n, i);
    a.n <- a.n + 1;
(*      assert is_elt [R] (a, i);*)
  };

  (* permet de prouver model(a, i) = v quand on change idx et back *)
(*  assert is_elt [R] (a, i);*)
}

(*
Autre version factorisée avec une référence sur un booléen mais les PO
deviennent illisibles : en fait c'est moins bien.

(* pas besoin de focus, grâce au "single" dans la définition de la classe *)
fun sset [R: sparse ('a)] (a: [R], i: int, v: 'a): unit
  consumes R^c
  produces R^c
  pre interval(0, i, get(R, a, size))
  post
    get(R, a, size) = get(R, a, size)@pre &&
    (forall j: int. j <> i ==> model [R] (a, j) = model [R] (a, j)@pre) &&
    model [R] (a, i) = v
{
  use invariant a;

  let x = array_set [a.Rvalue] (a.value, i, v);
  let index = array_get [a.Ridx] (a.idx, i);

  let region Rnew: Ref (bool);
  let is_new = new [Rnew];

  if 0 <= index && index < a.n then
  {
    let back_index = array_get [a.Rback] (a.back, index);
    if back_index = i then
    {
      is_new.ref_value <- false;
    }
    else
    {
      is_new.ref_value <- true;
    };
  }
  else
  {
    is_new.ref_value <- true;
  };

  if is_new.ref_value then
  {
    assert get(R, a, n) < get(R, a, size); (* pidgeons *)
    let x = array_set [a.Ridx] (a.idx, i, a.n);
    let x = array_set [a.Rback] (a.back, a.n, i);
    a.n <- a.n + 1;
  }
  else {};
}
*)

fun test(x: unit): unit
{
  let region Ra: sparse (int);
  let region Rb: sparse (int);
  let default = 0;
  let a = create [Ra] (10, default);
  let b = create [Rb] (10, default);
  let x = sget [Ra] (a, 5);
  let y = sget [Rb] (b, 7);
  assert x = default && y = default;
  let ignore = sset [Ra] (a, 5, 1);
  let ignore = sset [Rb] (b, 7, 2);
  let x = sget [Ra] (a, 5);
  let y = sget [Rb] (b, 7);
  assert x = 1 && y = 2;
  let x = sget [Ra] (a, 7);
  let y = sget [Rb] (b, 5);
  assert x = default && y = default;
  let x = sget [Ra] (a, 0);
  let y = sget [Rb] (b, 0);
  assert x = default && y = default;
  let x = sget [Ra] (a, 9);
  let y = sget [Rb] (b, 9);
  assert false;
}