examples/tortoise_and_hare.mlw

   1
   2 (* Floyd's cycle detection, also known as ``tortoise and hare'' algorithm.
   3
   4    See The Art of Computer Programming, vol 2, exercise 6 page 7. *)
   5
   6 module TortoiseAndHareAlgorithm
   7
   8   use int.Int
   9   use int.EuclideanDivision
  10   use int.Iter
  11   use seq.Seq
  12   use seq.Distinct
  13   use ref.Refint
  14   use pigeon.Pigeonhole
  15
  16   val function f int : int
  17
  18   (* f maps 0..m-1 to 0..m-1 *)
  19   constant m: int
  20   axiom m_positive: m > 0
  21
  22   axiom f_range: forall x. 0 <= x < m -> 0 <= f x < m
  23
  24   (* given some initial value x0 *)
  25   val constant x0: int
  26     ensures { 0 <= result < m }
  27
  28   (* we can build the infinite sequence defined by x{i+1} = f(xi) *)
  29   function x (i: int): int = iter f i x0
  30
  31   let rec lemma x_in_range (n: int)
  32     requires { 0 <= n } ensures { 0 <= x n < m }
  33     variant  { n }
  34   = if n > 0 then x_in_range (n - 1)
  35
  36   (* First, we prove the existence of mu and lambda, with a ghost program.
  37      Starting with x0, we repeatedly apply f, storing the elements in
  38      a sequence, until we find a repetition. *)
  39   let ghost periodicity () : (mu:int, lambda:int)
  40     ensures { 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\
  41               x (mu + lambda) = x mu }
  42     ensures { forall i j. 0 <= i < j < mu + lambda -> x i <> x j }
  43   = let s = ref (singleton x0) in
  44     let cur = ref x0 in
  45     for k = 1 to m do
  46       invariant { 1 <= length !s = k <= m /\ !cur = !s[length !s - 1] }
  47       invariant { forall i. 0 <= i < length !s -> !s[i] = x i }
  48       invariant { distinct !s }
  49       cur := f !cur;
  50       (* look for a repetition *)
  51       for mu = 0 to length !s - 1 do
  52         invariant { forall i. 0 <= i < mu -> !s[i] <> !cur }
  53         if !cur = !s[mu] then return (mu, length !s - mu)
  54       done;
  55       s := snoc !s !cur;
  56       if k = m then pigeonhole (m+1) m (pure { fun i -> !s[i] })
  57     done;
  58     absurd
  59
  60   (* Then we can state the condition for two elements to be equal. *)
  61   let lemma equality (mu lambda: int)
  62     requires { 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\
  63                x (mu + lambda) = x mu }
  64     requires { forall i j. 0 <= i < j < mu + lambda -> x i <> x j }
  65     ensures  { forall r n. r > n >= 0 ->
  66                x r = x n <-> n >= mu /\ exists k. k >= 1 /\ r-n = k*lambda }
  67   = let rec lemma plus_lambda (n: int) variant { n }
  68       requires { mu <= n }
  69       ensures  { x (n + lambda) = x n } =
  70       if n > mu then plus_lambda (n - 1) in
  71     let rec lemma plus_lambdas (n k: int) variant { k }
  72       requires { mu <= n } requires { 0 <= k }
  73       ensures  { x (n + k * lambda) = x n } =
  74       if k > 0 then begin
  75         plus_lambdas n (k - 1); plus_lambda (n + (k - 1) * lambda) end in
  76     let decomp (i: int) : (qi:int, mi:int)
  77       requires { i >= mu }
  78       ensures  { i = mu + qi * lambda + mi && qi >= 0 &&
  79                  0 <= mi < lambda && x i = x (mu + mi) } =
  80       let qi = div (i - mu) lambda in
  81       let mi = mod (i - mu) lambda in
  82       plus_lambdas (mu + mi) qi;
  83       qi, mi in
  84     let lemma equ (r n: int)
  85       requires { r > n >= 0 } requires { x r = x n }
  86       ensures  { n >= mu /\ exists k. k >= 1 /\ r-n = k*lambda } =
  87       if n < mu then (if r >= mu then let _ = decomp r in absurd)
  88       else begin
  89         let qr,mr = decomp r in let qn, mn = decomp n in
  90         assert { mr = mn };
  91         assert { r-n = (qr-qn) * lambda }
  92       end in
  93     ()
  94
  95   (* Finally, we implement the tortoise and hare algorithm that computes
  96      the values of mu and lambda in time O(mu+lambda) and constant space *)
  97   let tortoise_and_hare () : (mu:int, lambda:int)
  98     ensures { 0 <= mu < m /\ 1 <= lambda <= m /\ mu + lambda <= m /\
  99               x (mu + lambda) = x mu }
 100     ensures { forall i j. 0 <= i < j < mu + lambda -> x i <> x j }
 101   = [@vc:do_not_keep_trace] (* traceability info breaks the proofs *)
 102     let mu, lambda = periodicity () in
 103     equality mu lambda;
 104     (* the first loop implements the tortoise and hare,
 105        and finds the smallest n >= 1 such that x n = x (2n), in O(mu+lambda) *)
 106     let tortoise = ref (f x0) in
 107     let hare = ref (f (f x0)) in
 108     let n = ref 1 in
 109     while !tortoise <> !hare do
 110       invariant {
 111         1 <= !n <= mu+lambda /\ !tortoise = x !n /\ !hare = x (2 * !n) /\
 112         forall i. 1 <= i < !n -> x i <> x (2*i) }
 113       variant { mu + lambda - !n }
 114       tortoise := f !tortoise;
 115       hare     := f (f !hare);
 116       incr n;
 117       if !n > mu + lambda then begin
 118         let m = lambda - mod mu lambda in
 119         let i = mu + m in
 120         assert { 2*i - i = (div mu lambda + 1) * lambda };
 121         absurd
 122       end
 123     done;
 124     let n = !n in
 125     assert { n >= mu };
 126     assert { exists k. k >= 1 /\ n = k * lambda >= 1 };
 127     assert { forall j. j >= mu -> x j = x (j + n) };
 128     let xn = !tortoise in
 129     (* then a second loop finds mu and lambda, in O(mu) *)
 130     let i   = ref 0  in
 131     let xi  = ref x0 in (* = x i     *)
 132     let xni = ref xn in (* = x (n+i) *)
 133     let lam = ref 0  in (* 0 or lambda *)
 134     while !xi <> !xni do
 135       invariant { 0 <= !i <= mu }
 136       invariant { !xi = x !i /\ !xni = x (n + !i) }
 137       invariant { forall j. 0 <= j < !i -> x j <> x (n + j) }
 138       invariant { if !lam = 0 then forall j. 0 < j < !i -> x (n + j) <> x n
 139                   else !lam = lambda }
 140       variant   { mu - !i }
 141       if !lam = 0 && !i > 0 && !xni = xn then lam := !i;
 142       xi  := f !xi;
 143       xni := f !xni;
 144       incr i;
 145     done;
 146     let m = !i in
 147     assert { m = mu };
 148     let l = if !lam = 0 then n else !lam in
 149     assert { l = lambda };
 150     m, l
 151
 152 end