Hillel challenge
See Hillel challenge.
Authors: Jean-Christophe Filliâtre
Topics: Array Data Structure / Algorithms / Sorting Algorithms
Tools: Why3
see also the index (by topic, by tool, by reference, by year)
Hillel challenge
See https://www.hillelwayne.com/post/theorem-prover-showdown/
The challenge proposed by Hillel Wayne was to provide purely functional implementations and proofs for three imperative programs he proved using Dafny (as an attempt to understand whether the proof of FP code is easier than the proof of imperative programs).
Below are imperative implementations and proofs for the three Hillel challenges. Thus it is not really a response to the challenge, but rather an alternative to the Dafny proofs.
Author: Jean-Christophe Filliâtre (CNRS)
Challenge 1: Lefpad
Takes a padding character, a string, and a total length, returns the string padded to that length with that character. If length is less than the length of the string, does nothing.
module Leftpad use int.Int use int.MinMax use array.Array type char (* whatever it is *) type char_string = array char let leftpad (pad: char) (n: int) (s: char_string) : char_string ensures { length result = max n (length s) } ensures { forall i. 0 <= i < length result - length s -> result[i] = pad } ensures { forall i. 0 <= i < length s -> result[length result - 1 - i] = s[length s - 1 - i] } = let len = max n (length s) in let res = Array.make len pad in Array.blit s 0 res (len - length s) (length s); res end
Challenge 2: Unique
Takes a sequence of integers, returns the unique elements of that list. There is no requirement on the ordering of the returned values.
module Unique use int.Int use ref.Refint use fmap.MapImpInt as H use array.Array predicate mem (x: int) (a: array int) (i: int) = exists j. 0 <= j < i /\ a[j] = x let unique (a: array int) : array int ensures { forall x. mem x result (length result) <-> mem x a (length a) } ensures { forall i j. 0 <= i < j < length result -> result[i] <> result[j] } = let n = length a in let h = H.create () in let res = Array.make n 0 in let len = ref 0 in for i = 0 to n - 1 do invariant { 0 <= !len <= i } invariant { forall x. mem x a i <-> H.mem x h } invariant { forall x. mem x a i <-> mem x res !len } invariant { forall i j. 0 <= i < j < !len -> res[i]<>res[j] } if not (H.mem a[i] h) then begin H.add a[i] () h; res[!len] <- a[i]; incr len end done; Array.sub res 0 !len end
Challenge 3: Fulcrum
Given a sequence of integers, returns the index i
that minimizes
|sum(seq[..i]) - sum(seq[i..])|
. Does this in O(n) time and O(n)
memory.
We do it in O(n) time and O(1) space. A first loop computes the sum
of the array. A second scans the array from left to right, while
maintaining the left and right sums in two variables. Updating these
variables is simply of matter of adding a[i]
to left
and subtracting
a[i]
to right
.
module Fulcrum use int.Int use int.Abs use ref.Refint use array.Array use array.ArraySum function diff (a: array int) (i: int) : int = abs (sum a 0 i - sum a i (length a)) let fulcrum (a: array int) : int ensures { 0 <= result <= length a } ensures { forall i. 0 <= i <= length a -> diff a result <= diff a i } = let n = length a in let right = ref 0 in for i = 0 to n - 1 do invariant { !right = sum a 0 i } right += a[i] done; let left = ref 0 in let besti = ref 0 in let bestd = ref (abs !right) in for i = 0 to n - 1 do invariant { !left = sum a 0 i } invariant { !right = sum a i n } invariant { 0 <= !besti <= i } invariant { !bestd = diff a !besti } invariant { forall j. 0 <= j <= i -> !bestd <= diff a j } left += a[i]; right -= a[i]; let d = abs (!left - !right) in if d < !bestd then begin bestd := d; besti := i+1 end done; !besti end
Now, let's try to do the same with machine integers and avoiding
overflows. Obviously, computing the sum of the array elements may
overflow. We could limit the size of the array and the maximal value
of the elements. Instead, we choose here to compute the various sums
using "small big integers" implemented with pairs of machine
integers (basically, the sum of all the array elements cannot exceed
max_int^2
so two digits are enough).
For the purpose of illustration, we choose here 32-bit integers.
module FulcrumNoOverflow use int.Int use int.Sum as Sum use int.Abs use ref.Ref use mach.int.Int32 use mach.array.Array32 constant m : int = max_int32 + 1 (* thus 2^31 *) (* small big integers, within the range -m^2 .. m^2-1 *) type big = { mutable q: int32; mutable r: int32; mutable ghost v: int; } invariant { -m <= q <= m - 1 /\ 0 <= r <= m - 1 /\ v = q * m + r } by { q = 0:int32; r = 0:int32; v = 0 } meta coercion function v predicate biginv (_b: big) = 89>55 (* used to enforce the type invariant *) constant min_big : int = -m*m constant max_big : int = m*m - 1 let constant big_zero () : big = { q = 0:int32; r = 0:int32; v = 0 } let constant min_int32: int32 = -0x8000_0000 let constant max_int32: int32 = 0x7fff_ffff let add_big (b: big) (x: int32) : unit requires { min_big <= b.v + x <= max_big } ensures { b.v = old b.v + x } = if x < 0 then begin let r' = b.r + x in if r' < 0 then begin b.q <- b.q - 1; b.r <- (r'+1) + max_int32 end else b.r <- r' end else begin let r' = b.r + (min_int32 + x) in if r' < 0 then begin b.r <- (r'+1) + max_int32 end else begin b.q <- b.q + 1; b.r <- r' end end; b.v <- b.v + to_int x let sub_big (b: big) (x: int32) : unit requires { min_big <= b.v - x <= max_big } ensures { b.v = old b.v - x } = if x = min_int32 then begin b.q <- b.q + 1; b.v <- b.v - to_int x end else add_big b (-x) let delta (x y: big) : big requires { min_big <= abs (x.v - y.v) <= max_big } ensures { result.v = abs (x.v - y.v) } = let r = y.r - x.r in let ghost v = abs (x.v - y.v) in if y.q < x.q then (* -qM-r *) if r > 0 then { q = (x.q - 1) - y.q; r = (-r + 1) + max_int32; v = v } else { q = x.q - y.q; r = -r; v = v } else if y.q = x.q then (* abs r *) if r < 0 then { q = 0; r = -r; v = v } else { q = 0; r = r; v = v } else (* qM+r *) if r < 0 then { q = (y.q - 1) - x.q; r = (r+1) + max_int32; v = v } else { q = y.q - x.q; r = r; v = v } let big_lt (x y: big) : bool requires { x.v >= 0 /\ y.v >= 0 } ensures { result <-> x.v < y.v } = x.q < y.q || x.q = y.q && x.r < y.r function sum (a: array int32) (l u: int) : int = Sum.sum (fun i -> to_int a[i]) l u let lemma sum_bounds (a: array int32) (l u: int) requires { 0 <= l <= u <= length a } ensures { (u-l) * min_int32 <= sum a l u <= (u-l) * max_int32 } = let s = ref 0 in for i = l to u - 1 do invariant { !s = sum a l i } invariant { (i-l) * min_int32 <= !s <= (i-l) * max_int32 } s := !s + to_int (a.elts i) done function diff (a: array int32) (i: int) : int = abs (sum a 0 i - sum a i (length a)) let fulcrum (a: array int32) : int32 requires { length a < max_int32 } (* the only (and small) compromise *) ensures { 0 <= result <= length a } ensures { forall i. 0 <= i <= length a -> diff a result <= diff a i } = let n = length a in let right = big_zero () in for i = 0 to n - 1 do invariant { biginv right } invariant { right = sum a 0 i } add_big right a[i] done; let left = big_zero () in let besti = ref (0: int32) in let bestd = delta left right in for i = 0 to n - 1 do invariant { biginv right /\ biginv left /\ biginv bestd } invariant { left = sum a 0 i } invariant { right = sum a i n } invariant { 0 <= !besti <= i } invariant { bestd = diff a !besti } invariant { forall j. 0 <= j <= i -> bestd <= diff a j } add_big left a[i]; sub_big right a[i]; let d = delta left right in if big_lt d bestd then begin (* bestd <- d *) bestd.q <- d.q; bestd.r <- d.r; bestd.v <- d.v; besti := i + 1 end done; !besti end
download ZIP archive
Why3 Proof Results for Project "hillel_challenge"
Theory "hillel_challenge.Leftpad": fully verified
Obligations | Alt-Ergo 2.3.3 |
VC for leftpad | 0.40 |
Theory "hillel_challenge.Unique": fully verified
Obligations | Alt-Ergo 2.3.3 | CVC4 1.8 | Z3 4.8.10 | |||
VC for unique | --- | --- | --- | |||
split_vc | ||||||
array creation size | 0.01 | 0.07 | --- | |||
loop invariant init | 0.01 | 0.05 | --- | |||
loop invariant init | 0.01 | 0.08 | --- | |||
loop invariant init | 0.01 | 0.07 | --- | |||
loop invariant init | 0.01 | 0.07 | --- | |||
index in array bounds | 0.01 | 0.05 | --- | |||
index in array bounds | 0.00 | 0.05 | --- | |||
index in array bounds | 0.01 | 0.05 | --- | |||
index in array bounds | 0.01 | 0.06 | --- | |||
loop invariant preservation | 0.01 | 0.07 | --- | |||
loop invariant preservation | 0.08 | --- | --- | |||
loop invariant preservation | 0.15 | --- | --- | |||
loop invariant preservation | 0.04 | --- | --- | |||
loop invariant preservation | 0.01 | 0.07 | --- | |||
loop invariant preservation | 0.03 | 0.14 | --- | |||
loop invariant preservation | --- | --- | --- | |||
case x=a[i] | ||||||
true case (loop invariant preservation) | 0.01 | 0.08 | --- | |||
false case (loop invariant preservation) | --- | --- | --- | |||
assert (mem x a (i+1) <-> mem x a i) | ||||||
asserted formula | 0.01 | 0.08 | --- | |||
false case (loop invariant preservation) | 0.01 | 0.06 | --- | |||
loop invariant preservation | 0.01 | 0.08 | --- | |||
precondition | 0.01 | 0.07 | --- | |||
postcondition | --- | 0.15 | 0.35 | |||
postcondition | 0.01 | 0.08 | --- | |||
out of loop bounds | 0.01 | 0.07 | --- |
Theory "hillel_challenge.Fulcrum": fully verified
Obligations | Alt-Ergo 2.3.3 | CVC4 1.8 | |
VC for fulcrum | --- | --- | |
split_vc | |||
loop invariant init | 0.01 | 0.04 | |
index in array bounds | 0.00 | 0.03 | |
loop invariant preservation | 0.01 | 0.05 | |
loop invariant init | 0.01 | 0.04 | |
loop invariant init | 0.00 | 0.03 | |
loop invariant init | 0.00 | 0.03 | |
loop invariant init | 0.02 | 0.05 | |
loop invariant init | 0.00 | 0.04 | |
index in array bounds | 0.00 | 0.03 | |
index in array bounds | 0.00 | 0.03 | |
loop invariant preservation | 0.02 | 0.08 | |
loop invariant preservation | 0.02 | 0.06 | |
loop invariant preservation | 0.01 | 0.04 | |
loop invariant preservation | 0.01 | 0.06 | |
loop invariant preservation | 0.02 | 0.05 | |
loop invariant preservation | 0.02 | 0.07 | |
loop invariant preservation | 0.02 | 0.06 | |
loop invariant preservation | 0.00 | 0.04 | |
loop invariant preservation | 0.01 | 0.04 | |
loop invariant preservation | 0.01 | 0.55 | |
postcondition | 0.00 | 0.03 | |
postcondition | 0.00 | 0.04 | |
out of loop bounds | 0.00 | 0.03 | |
out of loop bounds | 0.00 | 0.05 |
Theory "hillel_challenge.FulcrumNoOverflow": fully verified
Obligations | Alt-Ergo 2.3.3 | CVC4 1.8 | ||
VC for big | 0.00 | 0.04 | ||
VC for big_zero | 0.00 | 0.04 | ||
VC for add_big | --- | --- | ||
split_vc | ||||
integer overflow | 0.01 | 0.05 | ||
integer overflow | 0.02 | 0.05 | ||
integer overflow | 0.01 | 0.04 | ||
integer overflow | 0.01 | 0.05 | ||
type invariant | 0.02 | 0.04 | ||
postcondition | 0.01 | 0.04 | ||
type invariant | --- | --- | ||
split_vc | ||||
type invariant | 0.01 | 0.04 | ||
type invariant | 0.01 | 0.05 | ||
type invariant | 0.01 | 0.03 | ||
type invariant | 0.01 | 0.05 | ||
type invariant | 0.01 | 0.05 | ||
postcondition | 0.01 | 0.03 | ||
integer overflow | 0.01 | 0.05 | ||
integer overflow | 0.02 | 0.04 | ||
integer overflow | 0.01 | 0.05 | ||
integer overflow | 0.01 | 0.05 | ||
type invariant | 0.03 | 0.04 | ||
postcondition | 0.01 | 0.04 | ||
integer overflow | 0.03 | 0.04 | ||
type invariant | 0.02 | 0.04 | ||
postcondition | 0.01 | 0.04 | ||
VC for sub_big | 0.04 | 0.06 | ||
VC for delta | --- | --- | ||
split_vc | ||||
integer overflow | 0.01 | 0.04 | ||
integer overflow | 0.01 | 0.05 | ||
integer overflow | 0.02 | 0.05 | ||
integer overflow | 0.02 | 0.05 | ||
integer overflow | 0.05 | 0.05 | ||
integer overflow | 0.03 | 0.05 | ||
precondition | 0.05 | 0.04 | ||
integer overflow | 0.01 | 0.04 | ||
integer overflow | 0.02 | 0.05 | ||
precondition | 0.03 | 0.05 | ||
integer overflow | 0.02 | 0.05 | ||
precondition | 0.02 | 0.05 | ||
precondition | 0.02 | 0.05 | ||
integer overflow | 0.01 | 0.05 | ||
integer overflow | 0.02 | 0.04 | ||
integer overflow | 0.05 | 0.05 | ||
integer overflow | 0.02 | 0.05 | ||
precondition | 0.04 | 0.06 | ||
integer overflow | 0.02 | 0.04 | ||
precondition | 0.02 | 0.06 | ||
postcondition | 0.02 | 0.04 | ||
VC for big_lt | 0.02 | 0.05 | ||
VC for sum_bounds | 1.28 | 0.07 | ||
VC for fulcrum | --- | --- | ||
split_vc | ||||
integer overflow | 0.01 | 0.04 | ||
loop invariant init | 0.00 | 0.04 | ||
loop invariant init | 0.01 | 0.05 | ||
index in array bounds | 0.01 | 0.04 | ||
precondition | 0.02 | 0.06 | ||
loop invariant preservation | 0.01 | 0.04 | ||
loop invariant preservation | 0.03 | 0.06 | ||
precondition | 0.02 | 0.05 | ||
integer overflow | 0.01 | 0.05 | ||
loop invariant init | 0.01 | 0.04 | ||
loop invariant init | 0.02 | 0.06 | ||
loop invariant init | 0.01 | 0.04 | ||
loop invariant init | 0.01 | 0.04 | ||
loop invariant init | 0.01 | 0.06 | ||
loop invariant init | 0.01 | 0.04 | ||
index in array bounds | 0.01 | 0.04 | ||
precondition | 0.03 | 0.06 | ||
index in array bounds | 0.02 | 0.05 | ||
precondition | 0.03 | 0.08 | ||
precondition | 0.06 | 0.15 | ||
precondition | 0.11 | 0.08 | ||
integer overflow | 0.02 | 0.06 | ||
type invariant | 0.03 | 0.07 | ||
loop invariant preservation | 0.02 | 0.04 | ||
loop invariant preservation | 0.12 | 0.19 | ||
loop invariant preservation | 0.15 | 0.49 | ||
loop invariant preservation | 0.02 | 0.05 | ||
loop invariant preservation | 0.03 | 1.86 | ||
loop invariant preservation | 0.08 | 1.00 | ||
loop invariant preservation | 0.02 | 0.04 | ||
loop invariant preservation | 0.12 | 0.16 | ||
loop invariant preservation | 0.12 | 2.06 | ||
loop invariant preservation | 0.02 | 0.05 | ||
loop invariant preservation | 0.02 | 0.04 | ||
loop invariant preservation | 0.04 | 1.62 | ||
postcondition | 0.01 | 0.04 | ||
postcondition | 0.02 | 0.05 | ||
out of loop bounds | 0.01 | 0.04 | ||
out of loop bounds | 0.02 | 0.08 |