verifythis_PrefixSumRec.mlw 7.4 KB
 MARCHE Claude committed Sep 13, 2012 1 ``````(** `````` François Bobot committed Sep 05, 2012 2 `````` `````` MARCHE Claude committed Apr 09, 2014 3 `````` {1 The VerifyThis competition at FM2012: Problem 2} `````` MARCHE Claude committed Sep 13, 2012 4 5 `````` see {h this web page} `````` François Bobot committed Sep 05, 2012 6 7 8 9 10 11 12 13 14 `````` *) module PrefixSumRec use import int.Int use import int.ComputerDivision use import int.Power `````` Andrei Paskevich committed Sep 24, 2013 15 `````` use import map.Map as M `````` Jean-Christophe Filliatre committed Sep 06, 2012 16 17 `````` use import array.Array use import array.ArraySum `````` François Bobot committed Sep 05, 2012 18 `````` `````` MARCHE Claude committed Sep 13, 2012 19 ``````(** {2 Preliminary lemmas on division by 2 and power of 2} *) `````` François Bobot committed Sep 05, 2012 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) `````` MARCHE Claude committed Sep 13, 2012 28 `````` (* needed *) `````` Jean-Christophe Filliatre committed Sep 06, 2012 29 30 `````` lemma is_power_of_2_1: forall x:int. is_power_of_2 x -> x > 1 -> 2 * div x 2 = x `````` François Bobot committed Sep 05, 2012 31 `````` `````` MARCHE Claude committed Sep 13, 2012 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. *) `````` François Bobot committed Sep 05, 2012 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 `````` MARCHE Claude committed Sep 13, 2012 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 committed Oct 11, 2013 68 `````` let rec lemma phase1_frame (left right:int) (a0 a a' : array int) : unit `````` Andrei Paskevich committed Sep 24, 2013 69 70 71 `````` requires { forall i:int. left-(right-left) < i < right -> a[i] = a'[i]} requires { phase1 left right a0 a } `````` MARCHE Claude committed Jan 21, 2014 72 `````` variant { right-left } `````` Andrei Paskevich committed Sep 24, 2013 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 `````` MARCHE Claude committed Sep 13, 2012 78 79 80 81 `````` (** frame lemma for "phase1" on third argument. needed to prove upsweep and compute_sums *) `````` Jean-Christophe Filliatre committed Oct 11, 2013 82 `````` let rec lemma phase1_frame2 (left right:int) (a0 a0' a : array int) : unit `````` Andrei Paskevich committed Sep 24, 2013 83 84 85 `````` requires { forall i:int. left-(right-left) < i < right -> a0[i] = a0'[i]} requires { phase1 left right a0 a } `````` MARCHE Claude committed Jan 21, 2014 86 `````` variant { right-left } `````` Andrei Paskevich committed Sep 24, 2013 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 `````` François Bobot committed Sep 05, 2012 93 `````` `````` Andrei Paskevich committed Oct 13, 2012 94 ``````(** {2 The upsweep phase} `````` MARCHE Claude committed Sep 13, 2012 95 96 `````` First function: modify partially the table and compute some `````` Andrei Paskevich committed Oct 13, 2012 97 `````` intermediate partial sums `````` MARCHE Claude committed Sep 13, 2012 98 99 100 `````` *) `````` Andrei Paskevich committed Oct 13, 2012 101 `````` let rec upsweep (left right: int) (a: array int) `````` MARCHE Claude committed Feb 12, 2013 102 103 104 `````` requires { 0 <= left < right < a.length } requires { -1 <= left - (right - left) } requires { is_power_of_2 (right - left) } `````` MARCHE Claude committed Jan 21, 2014 105 `````` variant { right - left } `````` MARCHE Claude committed Feb 12, 2013 106 `````` ensures { phase1 left right (old a) a } `````` Andrei Paskevich committed Oct 13, 2012 107 `````` ensures { let space = right - left in `````` MARCHE Claude committed Feb 12, 2013 108 `````` a[right] = sum (old a) (left-space+1) (right+1) /\ `````` Andrei Paskevich committed Oct 13, 2012 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: `````` François Bobot committed Sep 05, 2012 112 `````` let space = right - left in `````` Jean-Christophe Filliatre committed Sep 06, 2012 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]; `````` Andrei Paskevich committed Oct 13, 2012 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 committed Sep 06, 2012 126 `````` `````` MARCHE Claude committed Sep 13, 2012 127 128 129 ``````(** {2 The downsweep phase} *) (** The property we ultimately want to prove *) `````` Jean-Christophe Filliatre committed Sep 06, 2012 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 *) `````` Andrei Paskevich committed Oct 13, 2012 135 `````` let rec downsweep (left right: int) (ghost a0 : array int) (a : array int) `````` MARCHE Claude committed Feb 12, 2013 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 } `````` MARCHE Claude committed Jan 21, 2014 141 `````` variant { right - left } `````` MARCHE Claude committed Feb 12, 2013 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] } `````` Andrei Paskevich committed Oct 13, 2012 145 `````` = 'Init: `````` Jean-Christophe Filliatre committed Sep 06, 2012 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; `````` Andrei Paskevich committed Sep 24, 2013 158 `````` assert { phase1 (go_right left right) right a0 a }; `````` Jean-Christophe Filliatre committed Sep 06, 2012 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 } `````` François Bobot committed Sep 05, 2012 162 `````` `````` MARCHE Claude committed Sep 13, 2012 163 164 ``````(** {2 The main procedure} *) `````` Andrei Paskevich committed Oct 13, 2012 165 `````` let compute_sums a `````` MARCHE Claude committed Feb 12, 2013 166 167 `````` requires { a.length >= 2 } requires { is_power_of_2 a.length } `````` Andrei Paskevich committed Oct 13, 2012 168 169 `````` ensures { forall i : int. 0 <= i < a.length -> a[i] = sum (old a) 0 i } = let a0 = ghost (copy a) in `````` MARCHE Claude committed Sep 13, 2012 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; `````` MARCHE Claude committed Sep 13, 2012 174 `````` (* needed for the precondition of downsweep *) `````` MARCHE Claude committed Sep 13, 2012 175 176 177 `````` assert { phase1 left right a0 a }; a[right] <- 0; downsweep left right a0 a; `````` MARCHE Claude committed Sep 13, 2012 178 `````` (* needed to prove the post-condition *) `````` MARCHE Claude committed Sep 13, 2012 179 180 181 182 `````` assert { forall i : int. left-(right-left) < i <= right -> a[i] = sum a0 0 i } `````` MARCHE Claude committed Sep 13, 2012 183 184 ``````(** {2 A simple test} *) `````` MARCHE Claude committed Jan 15, 2014 185 `````` `````` MARCHE Claude committed Sep 13, 2012 186 `````` let test_harness () = `````` François Bobot committed Sep 05, 2012 187 `````` let a = make 8 0 in `````` MARCHE Claude committed Sep 13, 2012 188 `````` (* needed for the precondition of compute_sums *) `````` MARCHE Claude committed Sep 13, 2012 189 `````` assert { power 2 3 = a.length }; `````` MARCHE Claude committed Sep 13, 2012 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; `````` MARCHE Claude committed Sep 13, 2012 192 `````` compute_sums a; `````` François Bobot committed Sep 05, 2012 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 committed Jan 15, 2014 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; `````` MARCHE Claude committed Feb 03, 2014 219 220 `````` if a[7] <> 22 then raise BenchFailure; a `````` MARCHE Claude committed Jan 15, 2014 221 `````` `````` François Bobot committed Sep 05, 2012 222 ``end``