## VerifyThis @ FM 2012, problem 2

Computes prefix sums of an array, in-place

**Authors:** Claude Marché / François Bobot

**Topics:** Array Data Structure / Trees / Ghost code

**Tools:** Why3

**References:** VerifyThis @ FM2012

see also the index (by topic, by tool, by reference, by year)

download ZIP archive

# The VerifyThis competition at FM2012: Problem 2

see this web page

module PrefixSumRec use import int.Int use import int.ComputerDivision use import int.Power use import map.Map as M use import array.Array use import array.ArraySum

## Preliminary lemmas on division by 2 and power of 2

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) (* needed *) lemma is_power_of_2_1: forall x:int. is_power_of_2 x -> x > 1 -> 2 * div x 2 = x

## 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.

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

Frame properties of the "phase1" inductive

frame lemma for "phase1" on fourth argument. needed to prove both upsweep, downsweep and compute_sums

let rec lemma phase1_frame (left right:int) (a0 a a' : array int) : unit requires { forall i:int. left-(right-left) < i < right -> a[i] = a'[i]} requires { phase1 left right a0 a } variant { right-left } 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

frame lemma for "phase1" on third argument. needed to prove upsweep and compute_sums

let rec lemma phase1_frame2 (left right:int) (a0 a0' a : array int) : unit requires { forall i:int. left-(right-left) < i < right -> a0[i] = a0'[i]} requires { phase1 left right a0 a } variant { right-left } 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

## The upsweep phase

First function: modify partially the table and compute some intermediate partial sums

let rec upsweep (left right: int) (a: array int) requires { 0 <= left < right < a.length } requires { -1 <= left - (right - left) } requires { is_power_of_2 (right - left) } variant { right - left } ensures { phase1 left right (old a) a } ensures { let space = right - left in a[right] = sum (old a) (left-space+1) (right+1) /\ (forall i: int. i <= left-space -> a[i] = (old a)[i]) /\ (forall i: int. i > right -> a[i] = (old a)[i]) } = 'Init: let space = right - left in 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]; 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 }

## The downsweep phase

The property we ultimately want to prove

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

let rec downsweep (left right: int) (ghost a0 : array int) (a : array int) 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 } variant { right - left } 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] } = 'Init: 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; assert { phase1 (go_right left right) right a0 a }; 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 }

## The main procedure

let compute_sums a requires { a.length >= 2 } requires { is_power_of_2 a.length } ensures { forall i : int. 0 <= i < a.length -> a[i] = sum (old a) 0 i } = let a0 = ghost (copy a) in let l = a.length in let left = div l 2 - 1 in let right = l - 1 in upsweep left right a; (* needed for the precondition of downsweep *) assert { phase1 left right a0 a }; a[right] <- 0; downsweep left right a0 a; (* needed to prove the post-condition *) assert { forall i : int. left-(right-left) < i <= right -> a[i] = sum a0 0 i }

## A simple test

let test_harness () = 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; 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 } 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; if a[7] <> 22 then raise BenchFailure; a end

# Why3 Proof Results for Project "verifythis_PrefixSumRec"

## Theory "verifythis_PrefixSumRec.PrefixSumRec": fully verified in 148.01 s

Obligations | Alt-Ergo (0.99.1) | CVC3 (2.4.1) | CVC4 (1.4) | Z3 (3.2) | Z3 (4.3.2) | |

Div_mod_2 | 0.01 | 0.02 | 0.03 | 0.02 | 0.02 | |

is_power_of_2_1 | 0.01 | 0.03 | 0.02 | --- | --- | |

VC for phase1_frame | --- | --- | --- | --- | --- | |

split_goal_wp | ||||||

1. variant decrease | 0.01 | --- | 0.02 | --- | 0.01 | |

2. precondition | 0.02 | --- | 0.03 | --- | 0.01 | |

3. precondition | 0.01 | --- | 0.02 | --- | --- | |

4. variant decrease | 0.01 | --- | 0.03 | --- | 0.01 | |

5. precondition | 0.01 | --- | 0.02 | --- | 0.02 | |

6. precondition | 0.02 | --- | 0.02 | --- | --- | |

7. postcondition | --- | --- | 0.06 | --- | --- | |

8. postcondition | --- | 0.04 | --- | 0.02 | --- | |

VC for phase1_frame2 | --- | --- | --- | --- | --- | |

split_goal_wp | ||||||

1. variant decrease | 0.01 | --- | 0.02 | --- | 0.01 | |

2. precondition | 0.02 | --- | 0.04 | --- | 0.01 | |

3. precondition | 0.01 | --- | 0.02 | --- | --- | |

4. variant decrease | 0.02 | --- | 0.03 | --- | 0.01 | |

5. precondition | 0.01 | --- | 0.02 | --- | 0.01 | |

6. precondition | 0.02 | --- | 0.03 | --- | --- | |

7. postcondition | --- | 0.32 | 0.27 | --- | --- | |

8. postcondition | --- | 0.04 | --- | 0.02 | --- | |

VC for upsweep | --- | --- | --- | --- | --- | |

split_goal_wp | ||||||

1. variant decrease | 0.02 | --- | --- | --- | --- | |

2. precondition | 0.02 | 0.01 | 0.02 | 2.08 | --- | |

3. precondition | 0.01 | 0.01 | 0.02 | 0.02 | 0.03 | |

4. precondition | 0.03 | 0.06 | 0.04 | --- | --- | |

5. variant decrease | 0.02 | --- | --- | --- | --- | |

6. precondition | 0.02 | 0.02 | 0.02 | 0.02 | 0.03 | |

7. precondition | 0.02 | 0.02 | 0.02 | 0.02 | 0.03 | |

8. precondition | 0.01 | 0.02 | 0.02 | 0.02 | 0.03 | |

9. assertion | 2.48 | --- | 1.02 | --- | --- | |

10. assertion | 2.32 | --- | 0.74 | --- | --- | |

11. assertion | 0.52 | 0.02 | --- | --- | --- | |

12. assertion | --- | 0.58 | --- | --- | --- | |

13. index in array bounds | 0.00 | 0.00 | 0.01 | 0.02 | 0.02 | |

14. index in array bounds | 0.01 | 0.03 | 0.02 | 0.00 | 0.00 | |

15. index in array bounds | 0.01 | 0.02 | 0.01 | 0.01 | 0.03 | |

16. assertion | 0.24 | 1.72 | 2.08 | --- | --- | |

17. assertion | 0.04 | 0.81 | 2.22 | --- | --- | |

18. postcondition | --- | 0.93 | --- | 0.18 | --- | |

19. postcondition | 1.25 | --- | 0.86 | --- | --- | |

20. index in array bounds | 0.01 | 0.00 | 0.02 | 0.00 | 0.00 | |

21. index in array bounds | 0.02 | 0.02 | 0.01 | 0.02 | 0.05 | |

22. index in array bounds | 0.02 | 0.02 | 0.02 | 0.02 | 0.02 | |

23. assertion | 0.00 | 0.01 | 0.02 | 0.02 | 0.03 | |

24. assertion | 0.01 | 0.01 | 0.01 | 0.02 | 0.04 | |

25. postcondition | 0.02 | 0.01 | --- | 0.09 | 0.11 | |

26. postcondition | 0.16 | 0.04 | 0.34 | --- | --- | |

VC for downsweep | --- | --- | --- | --- | --- | |

split_goal_wp | ||||||

1. index in array bounds | 0.03 | 0.03 | 0.03 | 0.04 | 0.04 | |

2. assertion | 0.00 | 0.06 | 0.01 | 0.01 | 0.00 | |

3. assertion | --- | 0.00 | 0.04 | --- | --- | |

4. index in array bounds | 0.01 | 0.02 | 0.02 | 0.03 | 0.02 | |

5. index in array bounds | 0.02 | 0.03 | 0.02 | 0.02 | 0.03 | |

6. index in array bounds | 0.01 | 0.02 | 0.02 | 0.03 | 0.03 | |

7. index in array bounds | 0.01 | 0.02 | 0.01 | 0.00 | 0.00 | |

8. assertion | 0.24 | --- | 0.02 | 9.16 | --- | |

9. assertion | 0.04 | 0.02 | 0.02 | --- | --- | |

10. assertion | 0.04 | 0.02 | 0.04 | --- | --- | |

11. assertion | 0.12 | --- | 1.08 | --- | --- | |

12. variant decrease | 0.02 | --- | --- | --- | --- | |

13. precondition | 0.01 | 0.03 | 0.01 | 0.02 | 0.04 | |

14. precondition | 0.02 | 0.02 | 0.03 | 0.04 | 0.03 | |

15. precondition | 0.11 | --- | 0.44 | --- | --- | |

16. precondition | 0.01 | 0.02 | 0.16 | 10.96 | --- | |

17. precondition | --- | 5.16 | --- | 2.11 | --- | |

18. assertion | --- | 13.35 | 6.92 | --- | --- | |

19. variant decrease | 0.06 | --- | --- | --- | --- | |

20. precondition | 0.00 | 0.02 | 0.01 | 0.00 | 0.00 | |

21. precondition | 0.02 | 0.06 | 0.02 | 0.02 | 0.03 | |

22. precondition | 0.02 | 0.03 | 0.01 | 0.02 | 0.03 | |

23. precondition | 0.40 | 0.09 | 0.06 | --- | --- | |

24. precondition | 0.03 | 0.17 | --- | 0.01 | --- | |

25. assertion | 0.25 | --- | 3.02 | 0.05 | 0.05 | |

26. assertion | 0.03 | 0.04 | 0.02 | 0.02 | 0.03 | |

27. postcondition | 0.74 | 2.38 | 0.98 | --- | --- | |

28. postcondition | 0.40 | 6.88 | 2.92 | --- | --- | |

29. postcondition | 0.11 | 8.43 | 2.75 | 1.13 | 0.11 | |

30. postcondition | 0.02 | 0.12 | --- | --- | --- | |

31. postcondition | 0.02 | 0.02 | 0.02 | 0.15 | 0.04 | |

32. postcondition | 0.02 | 0.05 | 0.02 | 0.11 | 0.01 | |

VC for compute_sums | --- | --- | --- | --- | --- | |

split_goal_wp | ||||||

1. precondition | 0.02 | 0.01 | 0.01 | 2.15 | --- | |

2. precondition | 0.01 | 0.01 | 0.03 | 0.04 | 0.06 | |

3. precondition | 0.10 | 0.03 | 0.04 | 10.43 | --- | |

4. assertion | 1.07 | 0.28 | 0.38 | --- | --- | |

5. index in array bounds | 0.02 | 0.03 | 0.02 | 0.02 | 0.03 | |

6. precondition | 0.02 | 0.02 | 0.01 | 0.02 | 0.03 | |

7. precondition | 0.02 | 0.02 | 0.01 | 0.03 | 0.03 | |

8. precondition | 0.02 | 0.02 | 0.02 | 0.03 | 0.03 | |

9. precondition | 0.02 | 0.03 | 0.02 | 0.07 | 0.05 | |

10. precondition | 0.02 | 0.34 | 0.80 | --- | --- | |

11. assertion | 0.20 | --- | 0.52 | 0.05 | 0.06 | |

12. postcondition | --- | 3.00 | 0.39 | --- | --- | |

VC for test_harness | --- | --- | --- | --- | --- | |

split_goal_wp | ||||||

1. array creation size | 0.01 | 0.01 | 0.01 | 0.00 | 0.00 | |

2. assertion | 0.07 | 0.02 | 0.04 | 0.05 | 0.05 | |

3. index in array bounds | 0.01 | 0.01 | 0.02 | 0.00 | 0.00 | |

4. index in array bounds | 0.02 | 0.02 | 0.01 | 0.00 | 0.00 | |

5. index in array bounds | 0.01 | 0.01 | 0.01 | 0.00 | 0.00 | |

6. index in array bounds | 0.01 | 0.02 | 0.01 | 0.00 | 0.00 | |

7. index in array bounds | 0.02 | 0.01 | 0.00 | 0.00 | 0.00 | |

8. index in array bounds | 0.00 | 0.02 | 0.01 | 0.00 | 0.00 | |

9. index in array bounds | 0.01 | 0.01 | 0.02 | 0.00 | 0.00 | |

10. index in array bounds | 0.01 | 0.01 | 0.00 | 0.00 | 0.00 | |

11. precondition | 0.02 | 0.01 | 0.01 | 0.00 | 0.00 | |

12. precondition | 0.01 | 0.03 | 0.02 | 0.02 | 0.03 | |

13. assertion | 0.02 | 0.03 | 0.04 | 0.02 | 0.01 | |

14. assertion | 0.02 | 0.03 | 0.06 | 1.11 | 0.16 | |

15. assertion | 0.03 | 0.03 | 0.03 | 16.65 | --- | |

16. assertion | 0.02 | 0.02 | 0.05 | --- | --- | |

17. assertion | 0.03 | 0.02 | 0.03 | --- | --- | |

18. assertion | 0.02 | 0.02 | 0.03 | --- | --- | |

19. assertion | 0.02 | 0.03 | 0.03 | --- | --- | |

20. assertion | 0.01 | 0.02 | 0.13 | 1.10 | 0.16 | |

VC for bench | 0.04 | --- | --- | --- | --- |