examples/verifythis_PrefixSumRec.mlw

   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 module PrefixSumRec
  10
  11    use int.Int
  12    use int.ComputerDivision
  13    use int.Power
  14
  15    use map.Map
  16    use array.Array
  17    use array.ArraySum
  18
  19 (** {2 Preliminary lemmas on division by 2 and power of 2} *)
  20
  21   (** Needed for the proof of phase1_frame and phase1_frame2 *)
  22   lemma Div_mod_2:
  23     forall x:int. x >= 0 -> x >= 2 * div x 2 >= x-1
  24
  25   (** The step must be a power of 2 *)
  26   predicate is_power_of_2 (x:int) = exists k:int. (k >= 0 /\ x = power 2 k)
  27
  28   (* needed *)
  29   lemma is_power_of_2_1:
  30     forall x:int. is_power_of_2 x -> x > 1 -> 2 * div x 2 = x
  31
  32 (**
  33
  34 {2 Modeling the "upsweep" phase }
  35
  36 *)
  37
  38   (** Shortcuts *)
  39   function go_left (left right:int) : int =
  40     let space = right - left in left - div space 2
  41
  42   function go_right (left right:int) : int =
  43     let space = right - left in right - div space 2
  44
  45 (**
  46    Description in a purely logic way the effect of the first phase
  47      "upsweep" of the algorithm.  The second phase "downsweep" then
  48      traverses the array in the same way than the first phase. Hence,
  49      the inductive nature of this definition is not an issue. *)
  50
  51   inductive phase1 (left:int) (right:int) (a0: array int) (a: array int) =
  52     | Leaf : forall left right:int, a0 a : array int.
  53        right = left + 1 ->
  54        a[left] = a0[left] ->
  55        phase1 left right a0 a
  56     | Node : forall left right:int, a0 a : array int.
  57        right > left + 1 ->
  58        phase1 (go_left left right) left a0 a ->
  59        phase1 (go_right left right) right a0 a ->
  60        a[left] = sum a0 (left-(right-left)+1) (left+1) ->
  61        phase1 left right a0 a
  62
  63   (** Frame properties of the "phase1" inductive *)
  64
  65   (** frame lemma for "phase1" on fourth argument.
  66      needed to prove both upsweep, downsweep and compute_sums
  67    *)
  68   let rec lemma phase1_frame (left right:int) (a0 a a' : array int) : unit
  69     requires { forall i:int. left-(right-left) < i < right ->
  70                a[i] = a'[i]}
  71     requires { phase1 left right a0 a }
  72     variant { right-left }
  73     ensures { phase1 left right a0 a' } =
  74     if right > left + 1 then begin
  75        phase1_frame (go_left left right) left a0 a a';
  76        phase1_frame (go_right left right) right a0 a a'
  77     end
  78
  79   (** frame lemma for "phase1" on third argument.
  80      needed to prove upsweep and compute_sums
  81    *)
  82   let rec lemma phase1_frame2 (left right:int) (a0 a0' a : array int) : unit
  83     requires { forall i:int. left-(right-left) < i < right ->
  84                a0[i] = a0'[i]}
  85     requires { phase1 left right a0 a }
  86     variant { right-left }
  87     ensures { phase1 left right a0' a } =
  88     if right > left + 1 then begin
  89        phase1_frame2 (go_left left right) left a0 a0' a;
  90        phase1_frame2 (go_right left right) right a0 a0' a
  91     end
  92
  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     requires { 0 <= left < right < a.length }
 103     requires { -1 <= left - (right - left) }
 104     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       (forall i: int. i <= left-space -> a[i] = (old a)[i]) /\
 110       (forall i: int. i > right -> a[i] = (old a)[i]) }
 111   = let space = right - left in
 112     if right > left+1 then begin
 113       upsweep (left - div space 2) left a;
 114       upsweep (right - div space 2) right a;
 115       assert { phase1 (left - div space 2) left (old a) a };
 116       assert { phase1 (right - div space 2) right (old a) a };
 117       assert { a[left] = sum (old a) (left-(right-left)+1) (left+1) };
 118       assert { a[right] = sum (old a) (left+1) (right+1) }
 119     end;
 120     a[right] <- a[left] + a[right];
 121     assert {
 122       right > left+1 -> phase1 (left - div space 2) left (old a) a };
 123     assert {
 124       right > left+1 -> phase1 (right - div space 2) right (old a) a }
 125
 126 (** {2 The downsweep phase} *)
 127
 128   (** The property we ultimately want to prove *)
 129   predicate partial_sum (left:int) (right:int) (a0 a : array int) =
 130     forall i : int. (left-(right-left)) < i <= right -> a[i] = sum a0 0 i
 131
 132   (** Second function: complete the partial using the remaining intial
 133       value and the partial sum already computed *)
 134   let rec downsweep (left right: int) (ghost a0 : array int) (a : array int)
 135     requires { 0 <= left < right < a.length }
 136     requires { -1 <= left - (right - left) }
 137     requires { is_power_of_2 (right - left) }
 138     requires { a[right] = sum a0 0 (left-(right-left) + 1) }
 139     requires { phase1 left right a0 a }
 140     variant  { right - left }
 141     ensures { partial_sum left right a0 a }
 142     ensures { forall i: int. i <= left-(right-left) -> a[i] = (old a)[i] }
 143     ensures { forall i: int. i > right -> a[i] = (old a)[i] }
 144   = let tmp = a[right] in
 145     assert { a[right] = sum a0 0 (left-(right-left) + 1) };
 146     assert { a[left] = sum a0 (left-(right-left)+1) (left+1) };
 147     a[right] <- a[right] + a[left];
 148     a[left] <- tmp;
 149     assert { a[right] = sum a0 0 (left + 1) };
 150     if right > left+1 then
 151     let space = right - left in
 152     assert { phase1 (go_left left right) left a0 (old a) };
 153     assert { phase1 (go_right left right) right a0 (old a) };
 154     assert { phase1 (go_right left right) right a0 a };
 155     downsweep (left - div space 2) left a0 a;
 156     assert { phase1 (go_right left right) right a0 a };
 157     downsweep (right - div space 2) right a0 a;
 158     assert { partial_sum (left - div space 2) left a0 a };
 159     assert { partial_sum (right - div space 2) right a0 a }
 160
 161 (** {2 The main procedure} *)
 162
 163   let compute_sums a
 164     requires { a.length >= 2 }
 165     requires { is_power_of_2 a.length }
 166     ensures { forall i : int. 0 <= i < a.length -> a[i] = sum (old a) 0 i }
 167   = let a0 = ghost (copy a) in
 168     let l = a.length in
 169     let left = div l 2 - 1 in
 170     let right = l - 1 in
 171     upsweep left right a;
 172     (* needed for the precondition of downsweep *)
 173     assert { phase1 left right a0 a };
 174     a[right] <- 0;
 175     downsweep left right a0 a;
 176     (* needed to prove the post-condition *)
 177     assert { forall i : int.
 178       left-(right-left) < i <= right -> a[i] = sum a0 0 i }
 179
 180
 181 (** {2 A simple test} *)
 182
 183
 184   let test_harness () =
 185     let a = make 8 0 in
 186     (* needed for the precondition of compute_sums *)
 187     assert { power 2 3 = a.length };
 188     a[0] <- 3; a[1] <- 1; a[2] <- 7; a[3] <- 0;
 189     a[4] <- 4; a[5] <- 1; a[6] <- 6; a[7] <- 3;
 190     compute_sums a;
 191     assert { a[0] = 0 };
 192     assert { a[1] = 3 };
 193     assert { a[2] = 4 };
 194     assert { a[3] = 11 };
 195     assert { a[4] = 11 };
 196     assert { a[5] = 15 };
 197     assert { a[6] = 16 };
 198     assert { a[7] = 22 }
 199
 200
 201   exception BenchFailure
 202
 203   let bench () raises { BenchFailure -> true } =
 204     let a = make 8 0 in
 205     (* needed for the precondition of compute_sums *)
 206     assert { power 2 3 = a.length };
 207     a[0] <- 3; a[1] <- 1; a[2] <- 7; a[3] <- 0;
 208     a[4] <- 4; a[5] <- 1; a[6] <- 6; a[7] <- 3;
 209     compute_sums a;
 210     if a[0] <> 0 then raise BenchFailure;
 211     if a[1] <> 3 then raise BenchFailure;
 212     if a[2] <> 4 then raise BenchFailure;
 213     if a[3] <> 11 then raise BenchFailure;
 214     if a[4] <> 11 then raise BenchFailure;
 215     if a[5] <> 15 then raise BenchFailure;
 216     if a[6] <> 16 then raise BenchFailure;
 217     if a[7] <> 22 then raise BenchFailure;
 218     a
 219
 220 end