## Optimal replay

Challenge proposed by Ernie Cohen

**Authors:** Jean-Christophe Filliâtre

**Topics:** Array Data Structure / Ghost code

**Tools:** 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

download ZIP archive

# Why3 Proof Results for Project "optimal_replay"

## Theory "optimal_replay.OptimalReplay": fully verified

Obligations | Alt-Ergo 2.0.0 | Alt-Ergo 2.3.0 | CVC3 2.4.1 | CVC4 1.4 | CVC4 1.5 | Z3 3.2 | Z3 4.3.2 | |||

VC for n | --- | 0.00 | --- | --- | --- | --- | --- | |||

VC for distance | --- | --- | --- | --- | --- | --- | --- | |||

split_goal_right | ||||||||||

array creation size | 0.01 | --- | --- | --- | --- | --- | --- | |||

index in array bounds | 0.02 | --- | --- | --- | --- | --- | --- | |||

array creation size | 0.01 | --- | --- | --- | --- | --- | --- | |||

loop invariant init | 0.01 | --- | --- | --- | --- | --- | --- | |||

loop invariant init | 0.02 | --- | --- | --- | --- | --- | --- | |||

loop invariant init | 0.02 | --- | --- | --- | --- | --- | --- | |||

loop invariant init | 0.02 | --- | --- | --- | --- | --- | --- | |||

loop invariant init | 0.02 | --- | --- | --- | --- | --- | --- | |||

precondition | 0.01 | --- | --- | --- | --- | --- | --- | |||

index in array bounds | 0.02 | --- | --- | --- | --- | --- | --- | |||

index in array bounds | 0.02 | --- | --- | --- | --- | --- | --- | |||

loop variant decrease | --- | --- | --- | 0.04 | --- | --- | --- | |||

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | --- | |||

loop invariant preservation | --- | --- | 0.04 | 0.05 | --- | --- | --- | |||

index in array bounds | 0.01 | --- | --- | --- | --- | --- | --- | |||

index in array bounds | 0.01 | --- | --- | --- | --- | --- | --- | |||

index in array bounds | 0.02 | --- | --- | --- | --- | --- | --- | |||

loop invariant preservation | --- | --- | 0.04 | 0.02 | --- | 0.02 | 0.03 | |||

loop invariant preservation | --- | --- | 0.78 | --- | --- | --- | --- | |||

loop invariant preservation | --- | --- | --- | --- | --- | --- | --- | |||

unfold distance | ||||||||||

loop invariant preservation | --- | --- | --- | --- | --- | --- | --- | |||

split_goal_right | ||||||||||

loop invariant preservation | --- | --- | --- | --- | 0.38 | --- | --- | |||

loop invariant preservation | --- | --- | --- | 1.39 | --- | --- | --- | |||

assertion | --- | --- | --- | 0.06 | --- | --- | --- | |||

assertion | 0.00 | --- | --- | --- | --- | --- | --- | |||

out of loop bounds | 0.02 | --- | --- | --- | --- | --- | --- |