why3/examples_in_progress/next_digit_sum.mlw

module M

(*
   ACM Portugese National Programming Contest (MIUP) 2010

   Given an integer X >= 0, with N digits, and another integer Y > 0,
   find the smallest Z > X such that digit_sum(Z) = Y.

   Ocaml code given at the end of file.
*)

  use int.Int
  use ref.Ref
  use array.Array
  use int.MinMax
  use int.EuclideanDivision
  use int.Power

  function sum_digits int : int

  axiom Sum_digits_def : forall n : int. sum_digits n =
    if n <= 0 then 0 else sum_digits (div n 10) + mod n 10

  (* interp x i j is the integer X[j-1]...X[i] *)

  function interp (int -> int) int int : int

  axiom Interp_1 :
    forall x : int -> int, i j : int.
    i >= j -> interp x i j = 0

  axiom Interp_2 :
    forall x : int -> int, i j : int.
    i < j -> interp x i j = x i + 10 * interp x (i+1) j

  (* to allow provers to prove that an assignment does not change the
     interpretation on the left (or on the right); requires induction *)
  let rec lemma interp_eq
    (x1 x2 : int -> int) (i j : int)
    requires { forall k : int. i <= k < j -> x1 k = x2 k }
    ensures  { interp x1 i j = interp x2 i j }
    variant  { j - i }
  = if i < j then interp_eq x1 x2 (i+1) j

  (* the sum of the elements of x[i..j[ *)
  use int.Sum

  function sum (m: int -> int) (i j: int) : int =
    Sum.sum m i (j - 1)

  lemma Sum_is_sum_digits_interp:
    forall x : int -> int, i j : int.
    sum x i j = sum_digits (interp x i j)

  lemma Sum_digits_a_set_eq:
    forall x : array int, i j k v : int.
    (k < i \/ k >= j) -> sum (Map.set x.elts k v) i j = sum x.elts i j

  (* interp9 X i j is the j-digit integer obtained by replacing the i least
     significant digits in X by 9, i.e. X[j-1]...X[i]9...9 *)

  function interp9 (x : int -> int) (i j : int) : int =
    power 10 i * (interp x i j + 1) - 1

  lemma Interp9_step:
    forall x : int -> int, i j : int.
    i < j -> interp9 (Map.set x i 9) i j = interp9 x (i+1) j

  val x : array int

  (* the number of digits of X *)
  val constant n : int
    ensures { 0 <= result }

  (* the target digit sum *)
  val constant y : int
    ensures { 0 < result }

  let constant m : int = 1 + max n (div y 9)

exception Success

(* 1. Safety: we only prove that array access are within bounds
   (and termination, implicitely proved since we only have for loops) *)

let search_safety ()
  requires { length x = m }
  ensures  { true }
  raises   { Success -> true }
= let s = ref 0 in
  for i = 0 to m - 1 do (* could be n instead of m *)
    s := !s + x[i]
  done;
  for d = 0 to m - 1 do
    invariant { length x = m }
    for c = x[d] + 1 to 9 do
      invariant { length x = m }
      let delta = y - !s - c + x[d] in
      if 0 <= delta && delta <= 9 * d then begin
        x[d] <- c;
        let k = div delta 9 in
        for i = 0 to d - 1 do
          invariant { length x = m }
          if i < k then x[i] <- 9
          else if i = k then x[i] <- mod delta 9
          else x[i] <- 0
        done;
        raise Success
      end
    done;
    s := !s - x[d]
  done

(* 2. Correctness, part 1: when Success is raised, x contains an integer
      with digit sum y *)

  (* x[0..m-1] is a well-formed integer i.e. has digits in 0..9 *)
  predicate is_integer (x : int -> int) =
    forall k : int. 0 <= k < m -> 0 <= x k <= 9

let search ()
  requires { length x = m /\ is_integer x.elts }
  ensures  { true }
  raises   { Success -> is_integer x.elts /\ sum x.elts 0 m = y }
= let s = ref 0 in
  for i = 0 to m - 1 do (* could be n instead of m *)
    invariant { !s = sum x.elts 0 i }
    s := !s + x[i]
  done;
  assert { !s = sum x.elts 0 m };
  for d = 0 to m - 1 do
    invariant {
      x = old x /\
      !s = sum x.elts d m
    }
    for c = x[d] + 1 to 9 do
      invariant { x = old x }
      let delta = y - !s - c + x[d] in
      if 0 <= delta && delta <= 9 * d then begin
        x[d] <- c;
        assert { sum x.elts d m = y - delta };
        let k = div delta 9 in
        assert { k <= d };
        for i = 0 to d - 1 do
          invariant { length x = m /\ is_integer x.elts /\
                      sum x.elts d m = y - delta /\
                      sum x.elts 0 i = if i <= k then 9*i else delta }
          if i < k then x[i] <- 9
          else if i = k then x[i] <- (mod delta 9)
          else x[i] <- 0
        done;
        (* assume { sum !x 0 d = delta }; *)
        assert { sum x.elts 0 d = delta };
        raise Success
      end
    done;
    s := !s - x[d]
  done

(* 3. Correctness, part 2: we now prove that, on success, x contains the
   smallest integer > old(x) with digit sum y

   4. Completeness: we always raise the Success exception *)

  (* x1 > x2 since x1[d] > x2[d] and x1[d+1..m-1] = x2[d+1..m-1] *)
  predicate gt_digit (x1 x2 : int -> int) (d : int) =
    is_integer x1 /\ is_integer x2 /\ 0 <= d < m /\
    x1 d > x2 d /\ forall k : int. d < k < m -> x1 k = x2 k

  lemma Gt_digit_interp:
    forall x1 x2 : int -> int, d : int.
    gt_digit x1 x2 d -> interp x1 0 m > interp x2 0 m

  lemma Gt_digit_update:
    forall x1 x2 : int -> int, d i v : int.
    gt_digit x1 x2 d -> 0 <= i < d -> 0 <= v <= 9 ->
    gt_digit (Map.set x1 i v) x2 d

  (* the number of digits of a given integer *)
  function nb_digits int : int

  axiom Nb_digits_0 :
    nb_digits 0 = 0

  axiom Nb_digits_def :
    forall y : int. y > 0 -> nb_digits y = 1 + nb_digits (div y 10)

  (* the smallest integer with digit sum y is (y mod 9)9..9
     with exactly floor(y/9) trailing 9s *)

  function smallest int : int -> int

  function smallest_size int : int

  axiom Smallest_size_def0:
    smallest_size 0 = 0

  axiom Smallest_size_def1:
    forall y : int. y > 0 ->
    smallest_size y = if mod y 9 = 0 then div y 9 else 1 + div y 9

  (* smallest(y) is an integer *)
  axiom Smallest_def1:
    forall y : int. y >= 0 ->
    forall k : int. 0 <= k < smallest_size y -> 0 <= smallest y k <= 9

  (* smallest(y) has digit sum y *)
  axiom Smallest_def2:
    forall y : int. y >= 0 ->
    sum (smallest y) 0 (smallest_size y) = y

  (* smallest(y) is the smallest integer with digit sum y *)
  axiom Smallest_def3:
    forall y : int. y >= 0 ->
    forall u : int. 0 <= u < interp (smallest y) 0 (smallest_size y) ->
    sum_digits u <> y

  lemma Smallest_shape_1:
    forall y : int. y >= 0 -> mod y 9 = 0 ->
    forall k : int. 0 <= k < smallest_size y -> smallest y k = 9

  lemma Smallest_shape_2:
    forall y : int. y >= 0 -> mod y 9 <> 0 ->
    (forall k : int. 0 <= k < smallest_size y - 1 -> smallest y k = 9) /\
    smallest y (smallest_size y - 1) = mod y 9

  lemma Smallest_nb_digits:
    forall y : int. y >= 0 ->
    nb_digits (interp (smallest y) 0 (smallest_size y)) = smallest_size y

  lemma Any_nb_digits_above_smallest_size:
    forall y : int. y > 0 ->
    forall d : int. d >= smallest_size y ->
    exists u : int. nb_digits u = d /\ sum_digits u = y

  (* there exists an integer u with m digits and digit sum y *)
  lemma Completeness:
    m >= smallest_size y /\ (* cut *)
    exists u : int. nb_digits u = m /\ sum_digits u = y

let search_smallest ()
  requires { length x = m /\ is_integer x.elts /\
    (* x has at most n digits *)
    forall k : int. n <= k < m -> x[k] = 0 }
  ensures  { false }
  raises   { Success -> is_integer x.elts /\ sum x.elts 0 m = y /\
    interp x.elts 0 m > interp (old x.elts) 0 m /\
    forall u : int. interp (old x.elts) 0 m < u < interp x.elts 0 m ->
      sum_digits u <> y }
= let s = ref 0 in
  for i = 0 to m - 1 do (* could be n instead of m *)
    invariant { !s = sum x.elts 0 i }
    s := !s + x[i]
  done;
  assert { !s = sum x.elts 0 m };
  for d = 0 to m - 1 do
    invariant {
      x = old x /\
      !s = sum x.elts d m /\
      forall u : int.
         interp (old x.elts) 0 m < u <= interp9 x.elts d m -> sum_digits u <> y
    }
    for c = x[d] + 1 to 9 do
      invariant {
        x = old x /\
        forall c' : int. x[d] < c' < c ->
          forall u : int.
          interp (old x.elts) 0 m < u <= interp9 (Map.set x.elts d c') d m ->
            sum_digits u <> y }
      let delta = y - !s - c + x[d] in
      if 0 <= delta && delta <= 9 * d then begin
        assert { smallest_size delta <= d };
        x[d] <- c;
        assert { sum x.elts d m = y - delta };
        assert { gt_digit x.elts (old x.elts) d };
        let k = div delta 9 in
        assert { k <= d };
        for i = 0 to d - 1 do
          invariant {
             length x = m /\ is_integer x.elts /\
             sum x.elts d m = y - delta /\
             sum x.elts 0 i = (if i <= k then 9*i else delta) /\
             (forall j : int. 0 <= j < i ->
                (j <  smallest_size delta -> x[j] = smallest delta j) /\
                (j >= smallest_size delta -> x[j] = 0)) /\
             gt_digit x.elts (old x.elts) d }
          if i < k then x[i] <- 9
          else if i = k then x[i] <- mod delta 9
          else x[i] <- 0;
          assert { is_integer x.elts }
        done;
        assert { sum x.elts 0 d = delta };
        assert { interp x.elts 0 d = interp (smallest delta) 0 d };
        raise Success
      end
    done;
    s := !s - x[d]
  done

end

(*
let ys = Sys.argv.(1)
let zs = Sys.argv.(2)
let n = String.length zs
let y = int_of_string ys

let max_digits = 1 + max n (y / 9)
let x = Array.create max_digits 0
let () =
  for i = 0 to n - 1 do x.(n - 1 - i) <- Char.code zs.[i] - Char.code '0' done

let () =
  let s = ref 0 in
  for i = 0 to max_digits - 1 do s := !s + x.(i) done;
  for d = 0 to max_digits - 1 do
    (* s is the sum of digits d..n-1 *)
    (* solution with digits > d intacts, and digit d increased by 1 or more *)
    for c = x.(d) + 1 to 9 do
      let delta = y - !s - c + x.(d) in
      if 0 <= delta && delta <= 9 * d then begin
        x.(d) <- c;
        let k = delta / 9 in
        for i = 0 to d-1 do
          x.(i) <- if i < k then 9 else if i = k then delta mod 9 else 0
        done;
        for i = max d (n-1) downto 0 do Format.printf "%d" x.(i) done;
        Format.printf "@.";
        exit 0
      end
    done;
    s := !s - x.(d)
  done
*)