Capucine Example: Memoized Fibonacci

make examples/memo.gwhy

class Long
{
  value: int;
}

type option ('a)

logic none: option ('a)
logic some (x: 'a): option ('a)

logic get_some (x: option ('a)): 'a

axiom get_some_some:
  forall x: 'a.
  get_some (some (x)) = x

axiom none_or_some:
  forall x: option ('a).
  x = none() || exists y: 'a. x = some (y)

axiom none_xor_some:
  forall x: 'a. none() <> some (x)

axiom some_injective:
  forall x:'a. forall y:'a. some(x) = some(y) ==> x = y

type map ('a, 'b)

logic empty_map: map ('a, 'b)
logic store (x: map ('a, 'b), y: 'a, z: 'b): map ('a, 'b)
logic select (x: map ('a, 'b), y: 'a): option ('b)

axiom select_empty:
  forall y: 'a. select(empty_map(), y) = none()

class Table [Rval: Long]
{
  group Rkeys: Long;
  contents: map ([Rkeys], [Rval]);
}

logic model [Rv: Long, Rh: Table [Rv] ] (h: [Rh], i: int): option ([Rv])

axiom model_footprint :
   forall region Rv1: Long.
   forall region Rv2: Long.
   forall region Rh1: Table [Rv1].
   forall region Rh2: Table [Rv2].
   forall h: [?]. forall i:int.
   (get(Rh1, h, contents) = get(Rh2, h, contents)) ==>
   model [Rv1,Rh1](h,i) = model [Rv2,Rh2](h,i)

axiom model_typing:
  forall region Rv: Long.
  forall region Rh: Table [Rv].
  forall h: [?].
  forall x: int.
  forall y: [?].
  h in Rh ==>
  model [Rv, Rh] (h, x) = some (y) ==>
    y in Rv

(* signature typique des tables de hash à la Java, implémentée ici à
   l'aide d'une map logique pour simplifier *)

fun h_create [Rv: Long, R: Table [Rv]] (): [R]
  consumes R^e
  produces R^c
  post forall i: int. model[Rv, R](result, i) = none()
{
  let h = new [R];
  h.contents <- #empty_map ();
  return h
}

fun h_add [Rv: Long, R: Table [Rv], Rk: Long] (h: [R], k: [Rk], v: [Rv]): unit
  consumes R^c Rk^c
  produces R^c
  post
    model [Rv, R] (h, get(Rk, k, value)) = some (v) &&
    forall i: int.
    i <> get(Rk, k, value) ==> model [Rv, R] (h, i) = model [Rv, R] (h, i)@pre
{
  adopt Rk as h.Rkeys;
  h.contents <- #store (h.contents, k, v);
}

fun h_get [Rv: Long, R: Table [Rv], Rk: Long] (h: [R], k: [Rk]): option ([Rv])
  consumes R^c Rk^c
  produces R^c Rk^c
  post result = model [Rv, R] (h, get(Rk, k, value))
{
  return #none() (* just so it types, but we actually want to hide the implementation *)
}

(****************************************************************)

 (* l'idée c'est que si on ne voit que :

class Table [Rval: Long]

logic model [Rv: Long, Rh: Table [Rv]] (h: [Rh], k: int): option ([Rv])

   alors on peut toujours écrire Memo. *)

logic fibo (x: int): int

axiom fibo1: forall i:int. i <= 1 ==> fibo(i) = i
axiom fibo2: forall i:int. i >= 2 ==> fibo(i) = fibo(i-1) + fibo(i-2)

class Fibo
{
  group Rv: Long;
  single Rh: Table [Rv];
  hash: [Rh];
  invariant
    forall x: int.
    forall y: [?]. (* [Rv] *) (* y in Rv ==> *)
    model [Rv, Rh] (hash, x) = some (y) ==> get(Rv, y, value) = fibo(x)
}

(* l'invariant parle de la région Rv, possédée par Memo,
   mais ses locations sont stockées dans l'objet Table et pas dans Memo *)

fun new_fibo [R: Fibo] (): [R]
  consumes R^e
  produces R^c
{
  let f = new [R];
  let h = h_create [f.Rv, f.Rh] ();
  f.hash <- h;
  return f
}

(* pas besoin de mettre new_fibo dans la these *)

fun fibonacci [R: Fibo] (f: [R], i: int): int
  consumes R^c
  produces R^c
  pre i >= 0
  post result = fibo(i)
{
  use invariant f;
  let region Rr: Long;
  let r = new [Rr];

  if i <= 1 then
  {
    r.value <- i;
  } else {
    let region Rk: Long;
    let k = new [Rk];
    k.value <- i;

    let ro = h_get [f.Rv, f.Rh, Rk] (f.hash, k);
    if ro = #none() then
    {
      let f2 = fibonacci [R] (f, i - 2);
      let f1 = fibonacci [R] (f, i - 1);
      r.value <- f1 + f2;

      (* copy r to be able to adopt it in this branch of the if *)
      let region Rv: Long;
      let v = new [Rv];

      (* this should be a "use" statement instead of an "assert",
         but is not implemented yet in Capucine *)
      assert not (v in get(R, f, Rv));

      v.value <- r.value;
      use invariant f;
      use get(R, f, hash) in get(R, f, Rh);
(*
      assert forall x: int.
          forall y: [?].
          model [get(R,f,Rv), get(R,f,Rh)] (get(R,f,hash), x) = some (y) ==>
             y in get(R,f,Rv);
*)
      adopt Rv as f.Rv;
      (* use invariant f; *)
      let ignore = h_add [f.Rv, f.Rh, Rk] (f.hash, k, v);
    } else {
      let j = #get_some (ro);
      r.value <- j.value;

      (* hack to drop permission Rk^c *)
      let region Rtmp: Long;
      adopt Rk as Rtmp;
    };
  };

  return r.value
}