examples/hillel_challenge.mlw

   1
   2 (** {1 Hillel challenge}
   3
   4   See https://www.hillelwayne.com/post/theorem-prover-showdown/
   5
   6   The challenge proposed by Hillel Wayne was to provide purely functional
   7   implementations and proofs for three imperative programs he proved using
   8   Dafny (as an attempt to understand whether the proof of FP code is easier
   9   than the proof of imperative programs).
  10
  11   Below are imperative implementations and proofs for the three Hillel
  12   challenges. Thus it is not really a response to the challenge, but rather
  13   an alternative to the Dafny proofs.
  14
  15   Author: Jean-Christophe Filliâtre (CNRS)
  16 *)
  17
  18 (** {2 Challenge 1: Lefpad}
  19
  20   Takes a padding character, a string, and a total length, returns the
  21   string padded to that length with that character. If length is less
  22   than the length of the string, does nothing.
  23 *)
  24
  25 module Leftpad
  26
  27   use int.Int
  28   use int.MinMax
  29   use array.Array
  30
  31   type char (* whatever it is *)
  32   type char_string = array char
  33
  34   let leftpad (pad: char) (n: int) (s: char_string) : char_string
  35     ensures { length result = max n (length s) }
  36     ensures { forall i. 0 <= i < length result - length s -> result[i] = pad }
  37     ensures { forall i. 0 <= i < length s ->
  38               result[length result - 1 - i] = s[length s - 1 - i] }
  39   = let len = max n (length s) in
  40     let res = Array.make len pad in
  41     Array.blit s 0 res (len - length s) (length s);
  42     res
  43
  44 end
  45
  46 (** {2 Challenge 2: Unique}
  47
  48   Takes a sequence of integers, returns the unique elements of that
  49   list. There is no requirement on the ordering of the returned
  50   values.
  51
  52 *)
  53
  54 module Unique
  55
  56   use int.Int
  57   use ref.Refint
  58   use fmap.MapImpInt as H
  59   use array.Array
  60
  61   predicate mem (x: int) (a: array int) (i: int) =
  62     exists j. 0 <= j < i /\ a[j] = x
  63
  64   let unique (a: array int) : array int
  65     ensures { forall x. mem x result (length result) <-> mem x a (length a) }
  66     ensures { forall i j. 0 <= i < j < length result -> result[i] <> result[j] }
  67   = let n = length a in
  68     let h = H.create () in
  69     let res = Array.make n 0 in
  70     let len = ref 0 in
  71     for i = 0 to n - 1 do
  72       invariant { 0 <= !len <= i }
  73       invariant { forall x. mem x a i <-> H.mem x h }
  74       invariant { forall x. mem x a i <-> mem x res !len }
  75       invariant { forall i j. 0 <= i < j < !len -> res[i]<>res[j] }
  76       if not (H.mem a[i] h) then begin
  77         H.add a[i] () h;
  78         res[!len] <- a[i];
  79         incr len
  80       end
  81     done;
  82     Array.sub res 0 !len
  83
  84 end
  85
  86 (** {2 Challenge 3: Fulcrum}
  87
  88   Given a sequence of integers, returns the index `i` that minimizes
  89   `|sum(seq[..i]) - sum(seq[i..])|`. Does this in O(n) time and O(n)
  90   memory.
  91
  92   We do it in O(n) time and O(1) space. A first loop computes the sum
  93   of the array. A second scans the array from left to right, while
  94   maintaining the left and right sums in two variables. Updating these
  95   variables is simply of matter of adding `a[i]` to `left` and subtracting
  96   `a[i]` to `right`.
  97
  98 *)
  99
 100 module Fulcrum
 101
 102   use int.Int
 103   use int.Abs
 104   use ref.Refint
 105   use array.Array
 106   use array.ArraySum
 107
 108   function diff (a: array int) (i: int) : int =
 109     abs (sum a 0 i - sum a i (length a))
 110
 111   let fulcrum (a: array int) : int
 112     ensures { 0 <= result <= length a }
 113     ensures { forall i. 0 <= i <= length a -> diff a result <= diff a i }
 114   = let n = length a in
 115     let right = ref 0 in
 116     for i = 0 to n - 1 do
 117       invariant { !right = sum a 0 i }
 118       right += a[i]
 119      done;
 120     let left = ref 0 in
 121     let besti = ref 0 in
 122     let bestd = ref (abs !right) in
 123     for i = 0 to n - 1 do
 124       invariant { !left = sum a 0 i }
 125       invariant { !right = sum a i n }
 126       invariant { 0 <= !besti <= i }
 127       invariant { !bestd = diff a !besti }
 128       invariant { forall j. 0 <= j <= i -> !bestd <= diff a j }
 129       left += a[i];
 130       right -= a[i];
 131       let d = abs (!left - !right) in
 132       if d < !bestd then begin bestd := d; besti := i+1 end
 133     done;
 134     !besti
 135
 136 end
 137
 138 (** Now, let's try to do the same with machine integers and avoiding
 139   overflows. Obviously, computing the sum of the array elements may
 140   overflow. We could limit the size of the array and the maximal value
 141   of the elements. Instead, we choose here to compute the various sums
 142   using "small big integers" implemented with pairs of machine
 143   integers (basically, the sum of all the array elements cannot exceed
 144   `max_int^2` so two digits are enough).
 145
 146   For the purpose of illustration, we choose here 32-bit integers.
 147 *)
 148
 149 module FulcrumNoOverflow
 150
 151   use int.Int
 152   use int.Sum as Sum
 153   use int.Abs
 154   use ref.Ref
 155   use mach.int.Int32
 156   use mach.array.Array32
 157
 158   constant m : int = max_int32 + 1 (* thus 2^31 *)
 159
 160   (* small big integers, within the range -m^2 .. m^2-1 *)
 161   type big = {
 162     mutable       q: int32;
 163     mutable       r: int32;
 164     mutable ghost v: int;
 165   } invariant { -m <= q <= m - 1 /\ 0 <= r <= m - 1 /\ v = q * m + r }
 166   by { q = 0:int32; r = 0:int32; v = 0 }
 167
 168   meta coercion function v
 169
 170   predicate biginv (_b: big) = 89>55 (* used to enforce the type invariant *)
 171
 172   constant min_big : int = -m*m
 173   constant max_big : int =  m*m - 1
 174
 175   let constant big_zero () : big =
 176     { q = 0:int32; r = 0:int32; v = 0 }
 177
 178   let constant min_int32: int32 = -0x8000_0000
 179   let constant max_int32: int32 =  0x7fff_ffff
 180
 181   let add_big (b: big) (x: int32) : unit
 182     requires { min_big <= b.v + x <= max_big }
 183     ensures  { b.v = old b.v + x }
 184   = if x < 0 then begin
 185       let r' = b.r + x in
 186       if r' < 0 then begin b.q <- b.q - 1; b.r <- (r'+1) + max_int32 end
 187       else b.r <- r'
 188     end else begin
 189       let r' = b.r + (min_int32 + x) in
 190       if r' < 0 then begin b.r <- (r'+1) + max_int32 end
 191       else begin b.q <- b.q + 1;  b.r <- r' end
 192     end;
 193     b.v <- b.v + to_int x
 194
 195   let sub_big (b: big) (x: int32) : unit
 196     requires { min_big <= b.v - x <= max_big }
 197     ensures  { b.v = old b.v - x }
 198   = if x = min_int32 then begin b.q <- b.q + 1; b.v <- b.v - to_int x end
 199     else add_big b (-x)
 200
 201   let delta (x y: big) : big
 202     requires { min_big <= abs (x.v - y.v) <= max_big }
 203     ensures  { result.v = abs (x.v - y.v) }
 204   = let r = y.r - x.r in
 205     let ghost v = abs (x.v - y.v) in
 206     if y.q < x.q then (* -qM-r *)
 207       if r > 0 then { q = (x.q - 1) - y.q; r = (-r + 1) + max_int32; v = v }
 208       else { q = x.q - y.q; r = -r; v = v }
 209     else if y.q = x.q then (* abs r *)
 210       if r < 0 then { q = 0; r = -r; v = v } else { q = 0; r = r; v = v }
 211     else (* qM+r *)
 212       if r < 0 then { q = (y.q - 1) - x.q; r = (r+1) + max_int32; v = v }
 213       else { q = y.q - x.q; r = r; v = v }
 214
 215   let big_lt (x y: big) : bool
 216     requires { x.v >= 0 /\ y.v >= 0 }
 217     ensures  { result <-> x.v < y.v }
 218   = x.q < y.q || x.q = y.q && x.r < y.r
 219
 220   function sum (a: array int32) (l u: int) : int =
 221     Sum.sum (fun i -> to_int a[i]) l u
 222
 223   let lemma sum_bounds (a: array int32) (l u: int)
 224     requires { 0 <= l <= u <= length a }
 225     ensures  { (u-l) * min_int32 <= sum a l u <= (u-l) * max_int32 }
 226   = let s = ref 0 in
 227     for i = l to u - 1 do
 228       invariant { !s = sum a l i }
 229       invariant { (i-l) * min_int32 <= !s <= (i-l) * max_int32 }
 230       s := !s + to_int (a.elts i)
 231     done
 232
 233   function diff (a: array int32) (i: int) : int =
 234     abs (sum a 0 i - sum a i (length a))
 235
 236   let fulcrum (a: array int32) : int32
 237     requires { length a < max_int32 } (* the only (and small) compromise *)
 238     ensures  { 0 <= result <= length a }
 239     ensures  { forall i. 0 <= i <= length a -> diff a result <= diff a i }
 240   = let n = length a in
 241     let right = big_zero () in
 242     for i = 0 to n - 1 do
 243       invariant { biginv right }
 244       invariant { right = sum a 0 i }
 245       add_big right a[i]
 246      done;
 247     let left = big_zero () in
 248     let besti = ref (0: int32) in
 249     let bestd = delta left right in
 250     for i = 0 to n - 1 do
 251       invariant { biginv right /\ biginv left /\ biginv bestd }
 252       invariant { left = sum a 0 i }
 253       invariant { right = sum a i n }
 254       invariant { 0 <= !besti <= i }
 255       invariant { bestd = diff a !besti }
 256       invariant { forall j. 0 <= j <= i -> bestd <= diff a j }
 257       add_big left  a[i];
 258       sub_big right a[i];
 259       let d = delta left right in
 260       if big_lt d bestd then begin
 261         (* bestd <- d *) bestd.q <- d.q; bestd.r <- d.r; bestd.v <- d.v;
 262         besti := i + 1
 263       end
 264     done;
 265     !besti
 266
 267 end
 268