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 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 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 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

download ZIP archive

Why3 Proof Results for Project "random_access_list"

Theory "random_access_list.RandomAccessList": fully verified

ObligationsAlt-Ergo 2.0.0CVC4 1.5
VC length_flatten---0.06
VC size0.02---
VC cons---0.10
VC nth_flatten------
split_goal_right
VC nth_flatten.00.01---
VC nth_flatten.10.01---
VC nth_flatten.2---3.03
VC lookup0.34---
VC tail---0.08
VC update------
split_goal_right
VC update.00.01---
VC update.10.01---
VC update.20.01---
VC update.30.01---
VC update.40.01---
VC update.50.01---
VC update.60.03---
VC update.70.01---
VC update.80.01---
VC update.90.04---
VC update.100.05---
VC update.11------
split_goal_right
VC update.11.00.05---
VC update.11.10.31---
VC update.11.21.90---
VC update.120.28---
VC update.130.06---
VC update.140.04---
VC update.150.05---

Theory "random_access_list.RAL": fully verified

ObligationsCVC4 1.5
VC t0.01
VC empty0.02
VC size0.03
VC cons0.02
VC lookup0.03

Theory "random_access_list.RandomAccessListWithSeq": fully verified

ObligationsAlt-Ergo 2.0.0CVC4 1.5
cons_flatten------
split_goal_right
cons_flatten.00.00---
cons_flatten.10.03---
cons_flatten.20.08---
cons_flatten.30.46---
cons_flatten.40.01---
cons_flatten.50.01---
VC size0.02---
VC cons0.03---
VC lookup------
split_vc
VC lookup.00.00---
VC lookup.10.01---
VC lookup.20.01---
VC lookup.30.01---
VC lookup.40.02---
VC lookup.50.02---
VC lookup.60.01---
VC lookup.7------
split_vc
VC lookup.7.00.06---
VC lookup.7.10.01---
VC lookup.7.20.01---
VC tail0.30---
VC aux0.01---
VC fupdate------
split_goal_right
VC fupdate.00.00---
VC fupdate.10.01---
VC fupdate.20.02---
VC fupdate.30.01---
VC fupdate.40.03---
VC fupdate.50.04---
VC fupdate.6------
split_goal_right
VC fupdate.6.00.30---
VC fupdate.6.11.93---
VC fupdate.7------
split_goal_right
VC fupdate.7.00.03---
VC fupdate.7.10.06---
VC fupdate.7.20.09---
VC update---0.06