## Optimal replay

Challenge proposed by Ernie Cohen

Auteurs: Jean-Christophe Filliâtre

Catégories: Array Data Structure / Ghost code

Outils: Why3

see also the index (by topic, by tool, by reference, by year)

(*
Author: Jean-Christophe Filliatre (CNRS)
Tool:   Why3 (see http://why3.lri.fr/)

The following problem was suggested to me by Ernie Cohen (Microsoft Research)

We are given an integer N>0 and a function f such that 0 <= f(i) < i
for all i in 1..N-1. We define a reachability as follows:
each integer i in 1..N-1 can be reached from any integer in f(i)..i-1
in one step.

The problem is then to compute the distance from 0 to N-1 in O(N).
Even better, we want to compute this distance, say d, for all i
in 0..N-1 and to build a predecessor function g such that

i <-- g(i) <-- g(g(i)) <-- ... <-- 0

is the path of length d[i] from 0 to i.
*)

module OptimalReplay

use int.Int
use ref.Refint
use array.Array

val constant n: int
ensures { 0 < result }

val function f (k:int): int
requires { 0 < k < n }
ensures { 0 <= result < k}

(* path from 0 to i of distance d *)
inductive path int int =
| path0: path 0 0
| paths: forall i: int. 0 <= i < n ->
forall d j: int. path d j -> f i <= j < i -> path (d+1) i

predicate distance (d i: int) =
path d i /\ forall d': int. path d' i -> d <= d'

(* function [g] is built into local array [g]
and ghost array [d] holds the distance *)
let distance () =
let g = make n 0 in
g[0] <- -1; (* sentinel *)
let ghost d = make n 0 in
let ghost count = ref 0 in
for i = 1 to n-1 do
invariant { d[0] = 0 /\ g[0] = -1 /\ !count + d[i-1] <= i-1 }
(* local optimality *)
invariant {
forall k: int. 0 < k < i ->
g[g[k]] < f k <= g[k] < k /\
0 < d[k] = d[g[k]] + 1 /\
forall k': int. g[k] < k' < k -> d[g[k]] < d[k'] }
(* could be deduced from above, but avoids induction *)
invariant { forall k: int. 0 <= k < i -> distance d[k] k }
let j = ref (i-1) in
while g[!j] >= f i do
invariant { f i <= !j < i /\ !count + d[!j] <= i-1 }
invariant { forall k: int. !j < k < i -> d[!j] < d[k] }
variant { !j }
incr count;
j := g[!j]
done;
d[i] <- 1 + d[!j];
g[i] <- !j
done;
assert { !count < n }; (* O(n) is thus ensured *)
assert { forall k: int. 0 <= k < n -> distance d[k] k } (* optimality *)

end