Wiki Agenda Contact Version française

Random Access Lists


Authors: Jean-Christophe Filliâtre

Topics: Data Structures

Tools: 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 import int.Int
  use import int.ComputerDivision
  use import list.List
  use import list.Length
  use import list.Nth
  use import 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 import int.Int
  use import RandomAccessList as R
  use import list.List
  use import list.Length
  use import option.Option
  use import list.Nth

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

  let empty () : t 'a
    ensures { result.l = Nil }
    =
    { r = Empty; 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 import int.Int
  use import int.ComputerDivision
  use import 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)
           (\ i: int. let (x0, x1) = s[div i 2] in
                      if mod i 2 = 0 then x0 else x1)

  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) = lookup 0 l1 in One x1 (tail l1)
    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])

  function aux (i: int) (f: 'a -> 'a) : ('a, 'a) -> ('a, 'a) =
    \ 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  -> Zero (fupdate (aux i f) (div i 2) l1)
    end

  function f (y: 'a) : 'a -> 'a = \ _. 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

download ZIP archive

Why3 Proof Results for Project "random_access_list"

Theory "random_access_list.RandomAccessList": fully verified in 3.92 s

ObligationsAlt-Ergo (0.99.1)CVC4 (1.3)CVC4 (1.4)Z3 (4.3.1)
VC for length_flatten------------
split_goal_wp
  1. variant decrease0.02---------
2. postcondition------0.02---
3. postcondition0.02---------
VC for size0.02---------
VC for cons0.03---------
VC for nth_flatten------------
split_goal_wp
  1. postcondition0.02---------
2. variant decrease0.02---------
3. precondition0.02---------
4. postcondition---0.24------
5. postcondition------0.07---
VC for lookup0.47---------
VC for tail------------
split_goal_wp
  1. unreachable point0.01---------
2. postcondition0.02---------
3. precondition0.01---------
4. variant decrease0.01---------
5. precondition0.02---------
6. postcondition------0.07---
VC for update------------
split_goal_wp
  1. unreachable point0.02---------
2. postcondition0.01---------
3. postcondition0.02---------
4. postcondition0.02---------
5. postcondition0.02---------
6. variant decrease0.02---------
7. precondition0.02---------
8. unreachable point0.02---------
9. unreachable point0.02---------
10. postcondition0.02---------
11. postcondition0.04---------
12. postcondition0.03---------
13. postcondition0.02---------
14. precondition0.11---------
15. variant decrease0.02---------
16. precondition0.02---------
17. assertion------------
split_goal_wp
  1. assertion1.21---------
2. assertion---------0.03
3. assertion---------0.40
18. postcondition0.58---------
19. postcondition0.03---------
20. postcondition0.12---------
21. postcondition0.03---------

Theory "random_access_list.RAL": fully verified in 0.05 s

ObligationsAlt-Ergo (0.99.1)
VC for empty0.01
VC for size0.01
VC for cons0.01
VC for lookup0.02

Theory "random_access_list.RandomAccessListWithSeq": fully verified in 10.82 s

ObligationsAlt-Ergo (0.95.2)Alt-Ergo (0.99.1)
VC for size------
split_goal_wp
  1. postcondition0.01---
2. variant decrease0.02---
3. postcondition0.02---
4. variant decrease0.01---
5. postcondition0.02---
VC for cons------
split_goal_wp
  1. postcondition---0.03
2. postcondition---0.01
3. variant decrease---0.01
4. postcondition---1.27
VC for lookup---0.44
VC for tail------
split_goal_wp
  1. unreachable point0.03---
2. postcondition0.04---
3. precondition0.02---
4. variant decrease0.03---
5. precondition0.02---
6. postcondition5.55---
VC for fupdate---3.27
VC for update0.02---