Random Access Lists

Auteurs: Jean-Christophe Filliâtre

Catégories: Data Structures

Outils: Why3

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

Random Access Lists. (Okasaki, "Purely Functional Data Structures", 10.1.2.)

The code below uses polymorphic recursion (both in the logic and in the programs).

Author: Jean-Christophe FilliĆ¢tre (CNRS)

```module RandomAccessList

use int.Int
use int.ComputerDivision
use list.List
use list.Length
use list.Nth
use option.Option

type ral 'a =
| Empty
| Zero    (ral ('a, 'a))
| One  'a (ral ('a, 'a))

function flatten (l: list ('a, 'a)) : list 'a =
match l with
| Nil -> Nil
| Cons (x, y) l1 -> Cons x (Cons y (flatten l1))
end

let rec lemma length_flatten (l:list ('a, 'a))
ensures { length (flatten l) = 2 * length l }
variant { l }
=
match l with
| Cons (_,_) q -> length_flatten q
| Nil -> ()
end

function elements (l: ral 'a) : list 'a =
match l with
| Empty    -> Nil
| Zero l1  -> flatten (elements l1)
| One x l1 -> Cons x (flatten (elements l1))
end

let rec size (l: ral 'a) : int
variant { l }
ensures { result = length (elements l) }
=
match l with
| Empty    -> 0
| Zero  l1 ->     2 * size l1
| One _ l1 -> 1 + 2 * size l1
end

let rec cons (x: 'a) (l: ral 'a) : ral 'a
variant { l }
ensures { elements result = Cons x (elements l) }
=
match l with
| Empty    -> One x Empty
| Zero l1  -> One x l1
| One y l1 -> Zero (cons (x, y) l1)
end

let rec lemma nth_flatten (i: int) (l: list ('a, 'a))
requires { 0 <= i < length l }
variant  { l }
ensures  { match nth i l with
| None -> false
| Some (x0, x1) -> Some x0 = nth (2 * i)     (flatten l) /\
Some x1 = nth (2 * i + 1) (flatten l) end }
=
match l with
| Nil -> ()
| Cons _ r -> if i > 0 then nth_flatten (i-1) r
end

let rec lookup (i: int) (l: ral 'a) : 'a
requires { 0 <= i < length (elements l) }
variant  { i, l }
ensures  { nth i (elements l) = Some result }
=
match l with
| Empty    -> absurd
| One x l1 -> if i = 0 then x else lookup (i-1) (Zero l1)
| Zero l1  -> let (x0, x1) = lookup (div i 2) l1 in
if mod i 2 = 0 then x0 else x1
end

let rec tail (l: ral 'a) : ral 'a
requires { elements l <> Nil }
variant  { l }
ensures  { match elements l with
| Nil -> false
| Cons _ l -> elements result = l
end }
=
match l with
| Empty    -> absurd
| One _ l1 -> Zero l1
| Zero  l1 -> let (_, x1) = lookup 0 l1 in One x1 (tail l1)
end

let rec update (i: int) (y: 'a) (l: ral 'a) : ral 'a
requires { 0 <= i < length (elements l) }
variant  { i, l}
ensures  { nth i (elements result) = Some y}
ensures  { forall j. 0 <= j < length (elements l) ->
j <> i -> nth j (elements result) = nth j (elements l) }
ensures  { length (elements result) = length (elements l) }
ensures  { match result, l with
| One _ _, One _ _ | Zero _, Zero _ -> true
| _                                 -> false
end }
=
match l with
| Empty    -> absurd
| One x l1 -> if i = 0 then One y l1 else
match update (i-1) y (Zero l1) with
| Empty | One _ _ -> absurd
| Zero l1         -> One x l1
end
| Zero l1  ->
let (x0, x1) = lookup (div i 2) l1 in
let l1' =
update (div i 2) (if mod i 2 = 0 then (y,x1) else (x0,y)) l1 in
assert { forall j. 0 <= j < length (elements l) -> j <> i ->
match nth (div j 2) (elements l1) with
| None -> false
| Some (x0,_) -> Some x0 = nth (2 * (div j 2)) (elements l)
end
&& nth j (elements l) = nth j (elements (Zero l1')) };
Zero l1'
end

end

```

A straightforward encapsulation with a list ghost model (in anticipation of module refinement)

```module RAL

use int.Int
use list.List
use list.Length
use option.Option
use list.Nth
use RandomAccessList

type t 'a = { r: ral 'a; ghost l: list 'a }
invariant { l = elements r }

let constant empty : t 'a = { r = Empty; l = Nil }
ensures { result.l = Nil }

let size (t: t 'a) : int
ensures { result = length t.l }
=
size t.r

let cons (x: 'a) (s: t 'a) : t 'a
ensures { result.l = Cons x s.l }
=
{ r = cons x s.r; l = Cons x s.l }

let lookup (i: int) (s: t 'a) : 'a
requires { 0 <= i < length s.l }
ensures { Some result = nth i s.l }
=
lookup i s.r

end

```

Model using sequences instead of lists

```module RandomAccessListWithSeq

use int.Int
use int.ComputerDivision
use seq.Seq

type ral 'a =
| Empty
| Zero    (ral ('a, 'a))
| One  'a (ral ('a, 'a))

function flatten (s: seq ('a, 'a)) : seq 'a =
create (2 * length s)
(fun i -> let (x0, x1) = s[div i 2] in
if mod i 2 = 0 then x0 else x1)

lemma cons_flatten : forall x y :'a,s:seq ('a,'a).
let a = flatten (cons (x,y) s) in
let b = cons x (cons y (flatten s)) in
a = b by a == b by forall i. 0 <= i < a.length -> a[i] = b[i]
by (i <= 1 so (cons (x,y) s)[div i 2] = (x,y))
\/ (i >= 2 so (cons (x,y) s)[div i 2] = s[div (i-2) 2]
)

function elements (l: ral 'a) : seq 'a =
match l with
| Empty    -> empty
| Zero l1  -> flatten (elements l1)
| One x l1 -> cons x (flatten (elements l1))
end

let rec size (l: ral 'a) : int
variant { l }
ensures { result = length (elements l) }
=
match l with
| Empty    -> 0
| Zero  l1 ->     2 * size l1
| One _ l1 -> 1 + 2 * size l1
end

let rec cons (x: 'a) (l: ral 'a) : ral 'a
variant { l }
ensures { elements result == cons x (elements l) }
=
match l with
| Empty    -> One x Empty
| Zero l1  -> One x l1
| One y l1 -> Zero (cons (x, y) l1)
end

let rec lookup (i: int) (l: ral 'a) : 'a
requires { 0 <= i < length (elements l) }
variant  { i, l }
ensures  { (elements l)[i] = result }
=
match l with
| Empty    -> absurd
| One x l1 -> if i = 0 then x else lookup (i-1) (Zero l1)
| Zero l1  -> let (x0, x1) = lookup (div i 2) l1 in
if mod i 2 = 0 then x0 else x1
end

let rec tail (l: ral 'a) : ral 'a
requires { 0 < length (elements l) }
variant  { l }
ensures  { elements result == (elements l)[1..] }
=
match l with
| Empty    -> absurd
| One _ l1 -> Zero l1
| Zero  l1 -> let (_, x1) as p = lookup 0 l1 in
let tl = tail l1 in
assert { elements l1 == cons p (elements tl) };
One x1 tl
end

```

update in O(log n) for this, we need to pass a function that will update the element when we find it

```  function setf (s: seq 'a) (i: int) (f: 'a -> 'a) : seq 'a =
set s i (f s[i])

let function aux (i: int) (f: 'a -> 'a) : ('a, 'a) -> ('a, 'a) =
fun z -> let (x,y) = z in if mod i 2 = 0 then (f x, y) else (x, f y)

let rec fupdate (f: 'a -> 'a) (i: int) (l: ral 'a) : ral 'a
requires { 0 <= i < length (elements l) }
variant  { i, l }
ensures  { elements result == setf (elements l) i f }
=
match l with
| Empty    -> absurd
| One x l1 -> if i = 0 then One (f x) l1 else
cons x (fupdate f (i-1) (Zero l1))
| Zero l1  ->
let ul1 = fupdate (aux i f) (div i 2) l1 in
let res = Zero ul1 in
assert { forall j. 0 <= j < length (elements res) ->
(elements res)[j] = (setf (elements l) i f)[j]
by div j 2 <> div i 2 ->
(elements ul1)[div j 2] = (elements l1)[div j 2]
};
res
end

let function f (y: 'a) : 'a -> 'a = fun _ -> y

let update (i: int) (y: 'a) (l: ral 'a) : ral 'a
requires { 0 <= i < length (elements l) }
ensures  { elements result == set (elements l) i y}
=
fupdate (f y) i  l

end
```

Why3 Proof Results for Project "random_access_list"

Theory "random_access_list.RandomAccessList": fully verified

 Obligations Alt-Ergo 2.3.3 Alt-Ergo 2.4.2 CVC4 1.8 Z3 4.12.2 VC for length_flatten --- --- --- --- split_vc variant decrease 0.01 --- --- --- postcondition --- --- --- --- unfold flatten postcondition --- --- --- 0.01 VC for size 0.02 --- --- --- VC for cons 0.03 --- --- --- VC for nth_flatten --- --- --- --- split_vc variant decrease 0.01 --- --- --- precondition 0.00 --- --- --- postcondition --- --- --- --- destruct_term_subst l postcondition --- --- --- --- case (i = 0) true case (postcondition) --- --- --- --- subst i true case (postcondition) --- --- --- --- destruct_term_subst x1 true case (postcondition) --- --- --- --- compute_in_goal false case (postcondition) --- --- --- --- replace (nth i (Cons x1 x)) (nth (i - 1) x) false case (postcondition) --- --- --- --- destruct_term_subst x1 false case (postcondition) --- --- --- --- replace (2 * i) ((2 * (i - 1) + 1) + 1) false case (postcondition) --- --- --- --- destruct_term_subst (nth (i - 1) x) false case (postcondition) --- --- --- --- destruct_term_subst x false case (postcondition) --- --- --- --- replace (nth (i - 1) x2) (Some (x1, x)) false case (postcondition) --- --- --- --- assert (match Some (x1, x) with None -> false | Some (x0, x11) -> Some x0 = nth (2 * (i - 1)) (flatten x2) /\ Some x11 = nth ((2 * (i - 1)) + 1) (flatten x2) end) asserted formula 0.01 --- --- --- false case (postcondition) --- --- --- --- unfold flatten false case (postcondition) 0.02 --- --- --- equality hypothesis 0.00 --- --- --- false case (postcondition) 0.00 --- --- --- equality hypothesis 0.00 --- --- --- equality hypothesis 0.01 --- --- --- postcondition 0.01 --- --- --- VC for lookup 0.18 --- --- --- VC for tail --- --- 0.20 --- VC for update --- --- --- --- split_goal_right unreachable point 0.01 --- --- --- variant decrease 0.00 --- --- --- precondition 0.04 --- --- --- unreachable point 0.01 --- --- --- unreachable point 0.01 --- --- --- precondition 0.00 --- --- --- precondition 0.04 --- --- --- precondition 0.00 --- --- --- precondition 0.00 --- --- --- variant decrease 0.06 --- --- --- precondition 0.01 --- --- --- assertion --- --- --- --- split_goal_right assertion 0.08 --- --- --- assertion 0.12 --- --- --- assertion --- 0.25 --- --- postcondition --- 0.14 --- --- postcondition --- 0.05 --- --- postcondition --- 0.07 --- --- postcondition 0.06 --- --- ---

Theory "random_access_list.RAL": fully verified

 Obligations Alt-Ergo 2.3.3 VC for t 0.00 VC for empty 0.00 VC for size 0.00 VC for cons 0.01 VC for lookup 0.01

Theory "random_access_list.RandomAccessListWithSeq": fully verified

 Obligations Alt-Ergo 2.3.0 Alt-Ergo 2.3.3 cons_flatten --- --- split_vc cons_flatten.0 --- 0.00 cons_flatten.1 --- 0.01 cons_flatten.2 --- 0.06 cons_flatten.3 --- 0.60 cons_flatten.4 --- 0.02 cons_flatten.5 --- 0.01 VC for size --- 0.03 VC for cons --- 0.05 VC for lookup --- --- split_vc unreachable point --- 0.01 variant decrease --- 0.01 precondition --- 0.01 precondition --- 0.00 variant decrease --- 0.04 precondition --- 0.03 precondition --- 0.01 postcondition --- --- split_vc postcondition --- 0.01 postcondition --- 0.01 VC for tail --- 0.11 VC for aux --- 0.01 VC for fupdate --- --- split_vc unreachable point --- 0.01 variant decrease --- 0.01 precondition --- 0.01 precondition --- 0.01 variant decrease --- 0.04 precondition --- 0.03 assertion --- 1.51 postcondition --- --- split_vc postcondition --- 0.03 postcondition --- 0.03 VC for f 0.01 --- VC for update --- 0.01