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

download ZIP archive

Why3 Proof Results for Project "random_access_list"

Theory "random_access_list.RandomAccessList": fully verified

ObligationsAlt-Ergo 2.3.3Alt-Ergo 2.4.2CVC4 1.8Z3 4.12.2
VC for length_flatten------------
split_vc
variant decrease0.01---------
postcondition------------
unfold flatten
postcondition---------0.01
VC for size0.02---------
VC for cons0.03---------
VC for nth_flatten------------
split_vc
variant decrease0.01---------
precondition0.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 formula0.01---------
false case (postcondition)------------
unfold flatten
false case (postcondition)0.02---------
equality hypothesis0.00---------
false case (postcondition)0.00---------
equality hypothesis0.00---------
equality hypothesis0.01---------
postcondition0.01---------
VC for lookup0.18---------
VC for tail------0.20---
VC for update------------
split_goal_right
unreachable point0.01---------
variant decrease0.00---------
precondition0.04---------
unreachable point0.01---------
unreachable point0.01---------
precondition0.00---------
precondition0.04---------
precondition0.00---------
precondition0.00---------
variant decrease0.06---------
precondition0.01---------
assertion------------
split_goal_right
assertion0.08---------
assertion0.12---------
assertion---0.25------
postcondition---0.14------
postcondition---0.05------
postcondition---0.07------
postcondition0.06---------

Theory "random_access_list.RAL": fully verified

ObligationsAlt-Ergo 2.3.3
VC for t0.00
VC for empty0.00
VC for size0.00
VC for cons0.01
VC for lookup0.01

Theory "random_access_list.RandomAccessListWithSeq": fully verified

ObligationsAlt-Ergo 2.3.0Alt-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 f0.01---
VC for update---0.01