verifythis_PrefixSumRec.mlw 7.4 KB
Newer Older
1
(**
2

3
 {1 The VerifyThis competition at FM2012: Problem 2}
4 5

  see {h <a href="http://fm2012.verifythis.org/challenges">this web page</a>}
6 7 8 9 10 11 12 13 14

*)

module PrefixSumRec

   use import int.Int
   use import int.ComputerDivision
   use import int.Power

15
   use import map.Map as M
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
16 17
   use import array.Array
   use import array.ArraySum
18

19
(** {2 Preliminary lemmas on division by 2 and power of 2} *)
20 21 22 23 24 25 26 27

  (** Needed for the proof of phase1_frame and phase1_frame2 *)
  lemma Div_mod_2:
    forall x:int. x >= 0 -> x >= 2 * div x 2 >= x-1

  (** The step must be a power of 2 *)
  predicate is_power_of_2 (x:int) = exists k:int. (k >= 0 /\ x = power 2 k)

28
  (* needed *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
29 30
  lemma is_power_of_2_1:
    forall x:int. is_power_of_2 x -> x > 1 -> 2 * div x 2 = x
31

32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
(**

{2 Modeling the "upsweep" phase }

*)

  (** Shortcuts *)
  function go_left (left right:int) : int =
    let space = right - left in left - div space 2

  function go_right (left right:int) : int =
    let space = right - left in right - div space 2

(**
   Description in a purely logic way the effect of the first phase
     "upsweep" of the algorithm.  The second phase "downsweep" then
     traverses the array in the same way than the first phase. Hence,
     the inductive nature of this definition is not an issue. *)

51 52 53 54 55 56 57 58 59 60 61 62
  inductive phase1 (left:int) (right:int) (a0: array int) (a: array int) =
    | Leaf : forall left right:int, a0 a : array int.
       right = left + 1 ->
       a[left] = a0[left] ->
       phase1 left right a0 a
    | Node : forall left right:int, a0 a : array int.
       right > left + 1 ->
       phase1 (go_left left right) left a0 a ->
       phase1 (go_right left right) right a0 a ->
       a[left] = sum a0 (left-(right-left)+1) (left+1) ->
       phase1 left right a0 a

63 64 65 66 67
  (** Frame properties of the "phase1" inductive *)

  (** frame lemma for "phase1" on fourth argument.
     needed to prove both upsweep, downsweep and compute_sums
   *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
68
  let rec lemma phase1_frame (left right:int) (a0 a a' : array int) : unit
69 70 71
    requires { forall i:int. left-(right-left) < i < right ->
               a[i] = a'[i]}
    requires { phase1 left right a0 a }
72
    variant { right-left }
73 74 75 76 77
    ensures { phase1 left right a0 a' } =
    if right > left + 1 then begin
       phase1_frame (go_left left right) left a0 a a';
       phase1_frame (go_right left right) right a0 a a'
    end
78 79 80 81

  (** frame lemma for "phase1" on third argument.
     needed to prove upsweep and compute_sums
   *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
82
  let rec lemma phase1_frame2 (left right:int) (a0 a0' a : array int) : unit
83 84 85
    requires { forall i:int. left-(right-left) < i < right ->
               a0[i] = a0'[i]}
    requires { phase1 left right a0 a }
86
    variant { right-left }
87 88 89 90 91 92
    ensures { phase1 left right a0' a } =
    if right > left + 1 then begin
       phase1_frame2 (go_left left right) left a0 a0' a;
       phase1_frame2 (go_right left right) right a0 a0' a
    end

93

94
(** {2 The upsweep phase}
95 96

  First function: modify partially the table and compute some
97
      intermediate partial sums
98 99 100

*)

101
  let rec upsweep (left right: int) (a: array int)
102 103 104
    requires { 0 <= left < right < a.length }
    requires { -1 <= left - (right - left) }
    requires { is_power_of_2 (right - left) }
105
    variant { right - left }
106
    ensures { phase1 left right (old a) a }
107
    ensures { let space = right - left in
108
      a[right] = sum (old a) (left-space+1) (right+1) /\
109 110 111
      (forall i: int. i <= left-space -> a[i] = (old a)[i]) /\
      (forall i: int. i > right -> a[i] = (old a)[i]) }
  = 'Init:
112
    let space = right - left in
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
113 114 115 116 117 118 119 120 121
    if right > left+1 then begin
      upsweep (left - div space 2) left a;
      upsweep (right - div space 2) right a;
      assert { phase1 (left - div space 2) left (at a 'Init) a };
      assert { phase1 (right - div space 2) right (at a 'Init) a };
      assert { a[left] = sum (at a 'Init) (left-(right-left)+1) (left+1) };
      assert { a[right] = sum (at a 'Init) (left+1) (right+1) }
    end;
    a[right] <- a[left] + a[right];
122 123 124 125
    assert {
      right > left+1 -> phase1 (left - div space 2) left (at a 'Init) a };
    assert {
      right > left+1 -> phase1 (right - div space 2) right (at a 'Init) a }
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
126

127 128 129
(** {2 The downsweep phase} *)

  (** The property we ultimately want to prove *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
130 131 132 133 134
  predicate partial_sum (left:int) (right:int) (a0 a : array int) =
    forall i : int. (left-(right-left)) < i <= right -> a[i] = sum a0 0 i

  (** Second function: complete the partial using the remaining intial
      value and the partial sum already computed *)
135
  let rec downsweep (left right: int) (ghost a0 : array int) (a : array int)
136 137 138 139 140
    requires { 0 <= left < right < a.length }
    requires { -1 <= left - (right - left) }
    requires { is_power_of_2 (right - left) }
    requires { a[right] = sum a0 0 (left-(right-left) + 1) }
    requires { phase1 left right a0 a }
141
    variant  { right - left }
142 143 144
    ensures { partial_sum left right a0 a }
    ensures { forall i: int. i <= left-(right-left) -> a[i] = (old a)[i] }
    ensures { forall i: int. i > right -> a[i] = (old a)[i] }
145
  = 'Init:
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
146 147 148 149 150 151 152 153 154 155 156 157
    let tmp = a[right] in
    assert { a[right] = sum a0 0 (left-(right-left) + 1) };
    assert { a[left] = sum a0 (left-(right-left)+1) (left+1) };
    a[right] <- a[right] + a[left];
    a[left] <- tmp;
    assert { a[right] = sum a0 0 (left + 1) };
    if right > left+1 then
    let space = right - left in
    assert { phase1 (go_left left right) left a0 (at a 'Init) };
    assert { phase1 (go_right left right) right a0 (at a 'Init) };
    assert { phase1 (go_right left right) right a0 a };
    downsweep (left - div space 2) left a0 a;
158
    assert { phase1 (go_right left right) right a0 a };
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
159 160 161
    downsweep (right - div space 2) right a0 a;
    assert { partial_sum (left - div space 2) left a0 a };
    assert { partial_sum (right - div space 2) right a0 a }
162

163 164
(** {2 The main procedure} *)

165
  let compute_sums a
166 167
    requires { a.length >= 2 }
    requires { is_power_of_2 a.length }
168 169
    ensures { forall i : int. 0 <= i < a.length -> a[i] = sum (old a) 0 i }
  = let a0 = ghost (copy a) in
170 171 172 173
    let l = a.length in
    let left = div l 2 - 1 in
    let right = l - 1 in
    upsweep left right a;
174
    (* needed for the precondition of downsweep *)
175 176 177
    assert { phase1 left right a0 a };
    a[right] <- 0;
    downsweep left right a0 a;
178
    (* needed to prove the post-condition *)
179 180 181 182
    assert { forall i : int.
      left-(right-left) < i <= right -> a[i] = sum a0 0 i }


183 184
(** {2 A simple test} *)

MARCHE Claude's avatar
MARCHE Claude committed
185

186
  let test_harness () =
187
    let a = make 8 0 in
188
    (* needed for the precondition of compute_sums *)
189
    assert { power 2 3 = a.length };
190 191
    a[0] <- 3; a[1] <- 1; a[2] <- 7; a[3] <- 0;
    a[4] <- 4; a[5] <- 1; a[6] <- 6; a[7] <- 3;
192
    compute_sums a;
193 194 195 196 197 198 199 200 201
    assert { a[0] = 0 };
    assert { a[1] = 3 };
    assert { a[2] = 4 };
    assert { a[3] = 11 };
    assert { a[4] = 11 };
    assert { a[5] = 15 };
    assert { a[6] = 16 };
    assert { a[7] = 22 }

MARCHE Claude's avatar
MARCHE Claude committed
202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218

  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    let a = make 8 0 in
    (* needed for the precondition of compute_sums *)
    assert { power 2 3 = a.length };
    a[0] <- 3; a[1] <- 1; a[2] <- 7; a[3] <- 0;
    a[4] <- 4; a[5] <- 1; a[6] <- 6; a[7] <- 3;
    compute_sums a;
    if a[0] <> 0 then raise BenchFailure;
    if a[1] <> 3 then raise BenchFailure;
    if a[2] <> 4 then raise BenchFailure;
    if a[3] <> 11 then raise BenchFailure;
    if a[4] <> 11 then raise BenchFailure;
    if a[5] <> 15 then raise BenchFailure;
    if a[6] <> 16 then raise BenchFailure;
219 220
    if a[7] <> 22 then raise BenchFailure;
    a
MARCHE Claude's avatar
MARCHE Claude committed
221

222
end