Toccata

Schorr-Waite algorithm for general-size records.

Author: Martin Clochard (Université Paris Sud)

Here the proof is carried out by proving an equivalent recursive program. The recursive program can be justified to be equivalent to the looping one: all side-effects/exception throwing are done by running the loop body (which features a minor modification to exit by exception), so the recursive programs amounts to execute an arbitrary number of time the loop body. It is immediately followed by an absurd statement to enforce the equivalence with the loop which runs its body an infinite number of times. Although the added recursive structure can be seen to be computationally irrelevant, it allows to discharge details about Schorr-Waite stack management through a recursive procedure proof. The method basically make explicit the derecursification used to obtain Schorr-Waite algorithm.

See example verifythis_2016_tree_traversal for details about the technique, applied to a similar algorithm for trees.

module Memory

  use int.Int
  use option.Option
  use map.Map

  type loc

  constant null : loc

  type color =
    | White
    | Black (option int)
  type pmem = map loc (map int loc)

  type memory = abstract {

    block_size : map loc int;

    mutable accessor : pmem;

    mutable colors : map loc color;
  }

  val memo : memory

  val null () : loc ensures { result = null }

  val is_null (l:loc) : bool ensures { result <-> l = null }

  val get_block_size (l:loc) : int
    requires { l <> null }
    reads { memo }
    ensures { result = memo.block_size[l] /\ result >= 0 }

  val get_color (l:loc) : color
    requires { l <> null }
    reads { memo }
    ensures { result = memo.colors[l] }

  val set_color (l:loc) (c:color) : unit
    requires { l <> null }
    requires { match c with
      | White -> true
      | Black None -> memo.block_size[l] = 0
      | Black (Some ind) -> 0 <= ind < memo.block_size[l]
      end }
    writes { memo.colors }
    ensures { memo.colors = old (memo.colors[l <- c]) }

  val get_acc (l:loc) (k:int) : loc
    requires { l <> null /\ 0 <= k < memo.block_size[l] }
    reads { memo }
    ensures { result = memo.accessor[l][k] }
  val set_acc (l:loc) (k:int) (d:loc) : unit
    requires { l <> null /\ 0 <= k < memo.block_size[l] }
    writes { memo.accessor }
    ensures { memo.accessor =
      old (memo.accessor[l <- memo.accessor[l][k <- d]]) }

  val ghost snapshot_acc () : pmem
    reads { memo }
    ensures { result = memo.accessor }
  val ghost snapshot_colors () : map loc color
    reads { memo }
    ensures { result = memo.colors }

end

module GraphShape

  use int.Int
  use set.Fset
  use map.Map
  use Memory

  predicate black (c:color) = c <> White

  predicate edge (m:memory) (x y:loc) =
    x <> null /\ (exists n. 0 <= n < m.block_size[x] /\ m.accessor[x][n] = y)

  inductive path memory (x y:loc) =
    | path_nil : forall m x. path m x x
    | path_cons : forall m x y z. edge m x y /\ path m y z -> path m x z

  predicate well_colored_on (graph gray:fset loc) (m:memory) (cl:map loc color) =
    subset gray graph /\
    (forall x y. mem x graph /\ edge m x y /\ y <> null /\ black cl[x] ->
      mem x gray \/ black cl[y]) /\
    (forall x. mem x gray -> black cl[x])

  predicate unchanged (m1 m2:memory) =
    forall x n. x <> null /\ 0 <= n < m1.block_size[x] ->
      m2.accessor[x][n] = m1.accessor[x][n]

end

module SchorrWaite

  use int.Int
  use option.Option
  use set.Fset
  use map.Map
  use map.Const
  use ref.Ref
  use Memory
  use GraphShape

  let black (l: loc) : bool
    requires { l <> null }
    reads { memo }
    ensures { result <-> black memo.colors[l] }
  = match get_color l with White -> false | _ -> true end

  exception Stop

  let schorr_waite (root: loc) (ghost graph: fset loc) : unit

    requires { mem root graph }

    requires { forall l n.
      mem l graph /\ l <> null /\ 0 <= n < memo.block_size[l] ->
      mem memo.accessor[l][n] graph }
    writes { memo.accessor, memo.colors }

    requires { forall x. mem x graph -> not black memo.colors[x] }

    ensures { unchanged (old memo) memo }

    ensures { forall x. path (old memo) root x /\ x <> null ->
      black memo.colors[x] }

    ensures { forall x. not path (old memo) root x /\ x <> null ->
      memo.colors[x] = (old memo).colors[x] }
  =
    label I in
    let t = ref root in
    let p = ref (null ()) in

    let body () : unit

      requires { !p <> null /\ (!t = null \/ black memo.colors[!t]) ->
        match memo.colors[!p] with
        | Black (Some m) -> 0 <= m < memo.block_size[!p]
        | _ -> false
        end }
      ensures { old (!p <> null \/ (!t <> null /\ not black memo.colors[!t])) }
      ensures { old (!t <> null /\ not black memo.colors[!t] /\
                     memo.block_size[!t] = 0) ->
        memo.colors = old memo.colors[!t <- Black None] /\
        !t = old !t /\ !p = old (!p) /\ memo.accessor = old memo.accessor
      }
      ensures { old (!t <> null /\ not black memo.colors[!t] /\
                     memo.block_size[!t] > 0) ->
        memo.colors = old memo.colors[!t <- Black (Some 0)] /\
        !t = old memo.accessor[!t][0] /\ !p = old (!t) /\
        memo.accessor = old memo.accessor[!t <- memo.accessor[!t][0 <- !p]] }
      ensures { old (!t = null \/ black memo.colors[!t]) ->
        match old (memo.colors[!p]) with
        | Black (Some m) ->
            let n = m + 1 in
            if n = old (memo.block_size[!p])
            then
              !t = old (!p) /\ !p = (old memo.accessor[!p])[m] /\
              memo.colors = old (memo.colors) /\
              memo.accessor =
                (old memo.accessor)[old !p <-
                                    (old memo.accessor[!p])[m <- old !t]]
            else !p = old !p /\ !t = (old memo.accessor[!p])[n] /\
              memo.colors = (old memo.colors)[old !p <- Black (Some n)] /\
              let pi = (old memo.accessor[!p])[m] in
              memo.accessor =
                (old memo.accessor)[old !p <-
                         (old memo.accessor[!p])[n <- pi][m <- old !t]]
        | _ -> false
        end }
      raises { Stop -> old(!p = null /\ (!t = null \/ black memo.colors[!t])) /\
        memo.colors = old memo.colors /\ memo.accessor = old memo.accessor }
    =

      if is_null !p && (is_null !t || black !t) then raise Stop;
      if is_null !t || black !t then begin
        match get_color !p with
        | Black (Some m) ->
            let s = get_block_size !p in
            let n = m + 1 in
            if n = s then begin (* Pop *)
              let q = !t in
              t := !p;
              p := get_acc !p m;
              set_acc !t m q
            end else begin (* Swing *)
              let q = !t in
              t := get_acc !p n;
              set_acc !p n (get_acc !p m);
              set_acc !p m q;
              set_color !p (Black (Some n))
            end
        | _ -> absurd
        end
      end else
        let s = get_block_size !t in
        if s = 0 then (* Mark & continue *) set_color !t (Black None)
        else begin (* Mark & Push *)
          let q = !p in
          p := !t;
          t := get_acc !t 0;
          set_acc !p 0 q;
          set_color !p (Black (Some 0))
        end
    in
    let rec aux (ghost gray:fset loc) : unit
      (* DFS invariant *)
      requires { well_colored_on graph gray (memo at I) memo.colors }
      requires { mem !t graph }
      (* Non-marked nodes have unchanged structure with
          respect to the initial one. *)
      requires { forall x n.
        x <> null /\ not black memo.colors[x] /\ 0 <= n < memo.block_size[x] ->
        memo.accessor[x][n] = (memo.accessor at I)[x][n] }
      (* 'stack frames' are maintained correctly *)
      ensures { !t = old !t /\ !p = old !p }
      (* Pointer buffer is left unchanged *)
      ensures { unchanged (old memo) memo }
      (* Maintain DFS invariant *)
      ensures { well_colored_on graph gray (memo at I) memo.colors }
      (* The top node get marked *)
      ensures { black memo.colors[!t] \/ !t = null }
      (* May not mark unreachable node, neither change marked node. *)
      ensures { forall x.
        x <> null -> not path (memo at I) !t x \/ black (old memo.colors)[x] ->
        memo.colors[x] = (old memo.colors)[x] }
      (* Never 'exit' the loop during the recursive calls *)
      raises { Stop -> false }
      (* Terminates because there is a limited number of 'grayable' nodes. *)
      variant { cardinal graph - cardinal gray }
    = label J in
      if is_null !t || black !t then () else begin
        let s = get_block_size !t in
        let ghost g2 = add !t gray in
        assert { path (memo at I) !t !t };
        body (); (* Either push or mark & continue. *)
        if s <> 0 then begin
          for i = 0 to s - 2 do (* Over all sub-blocs... *)
            (* DFS invariant. *)
            invariant { well_colored_on graph g2 (memo at I) memo.colors }
            (* Current stack frame invariants *)
            invariant { !p = !t at J }
            invariant { !t = (memo.accessor at I)[!p][i] }
            invariant { memo.colors[!p] = Black (Some i) }
            invariant { forall j. 0 <= j < s /\ j <> i ->
              memo.accessor[!p][j] = (memo.accessor at J)[!p][j] }
            invariant { memo.accessor[!p][i] = !p at J }
            (* Outside structure is unchanged. *)
            invariant { forall l n.
              l <> null /\ l <> !p /\ 0 <= n < memo.block_size[l] ->
              memo.accessor[l][n] = (memo.accessor at J)[l][n] }
            (* All nodes under !p & before i are either null or marked black. *)
            invariant { forall j. 0 <= j < i ->
              let l = memo.accessor[!p][j] in l = null \/ black memo.colors[l] }
            (* Unreachable/pre-marked blocks do not change. *)
            invariant { forall l. l <> null ->
              not path (memo at I) !p l \/ black (memo.colors at J)[l] ->
                memo.colors[l] = (memo.colors at J)[l] }
            label K in
            aux g2; (* Explore sub-bloc. *)
            body (); (* Swing to next sub-bloc. *)
            assert { !t = (memo.accessor at K)[!p][i+1]
              = (memo.accessor at J)[!p][i+1] }
          done;
          aux g2; (* Explore last sub-bloc. *)
          body (); (* Pop. *)
        end
      end in
    try aux (ghost empty); (* Explore main bloc *)
        body (); (* Exit *)
        absurd; (* Done. *)
    with Stop ->
      (* Need induction to recover path-based specification. *)
      assert { forall x y m. m = memo at I /\ x <> null /\ y <> null /\
        mem x graph /\ black memo.colors[x] ->
        ([@induction] path m x y) -> black memo.colors[y] }
    end

end