examples/bignum.mlw

   1
   2 (** Big numbers as little-endian lists of digits.
   3
   4     This is borrowed from a PVS tutorial.
   5     (see for instance http://fm.csl.sri.com/SSFT11/ITPSummerFormal2011.pdf)
   6
   7     In addition, we show that the representation is valid (all digits in
   8     0..base-1) and canonical (no most significant 0 digits).
   9 *)
  10
  11 module BigNum
  12
  13   use int.Int
  14   use list.List
  15
  16   val constant base: int
  17     ensures { result > 1 }
  18
  19   type digit = int
  20   type num = list digit
  21
  22   function value (n: num) : int =
  23     match n with
  24     | Nil -> 0
  25     | Cons d r -> d + base * value r
  26     end
  27
  28   predicate valid (n: num) =
  29     match n with
  30     | Nil -> true
  31     | Cons d Nil -> 0 < d < base
  32     | Cons d r -> 0 <= d < base && valid r
  33     end
  34
  35   let rec lemma nonneg (n: num) : unit
  36     requires { valid n }
  37     ensures  { value n >= 0 }
  38     variant  { n }
  39   = match n with Nil -> () | Cons _ r -> nonneg r end
  40
  41   let rec lemma msd (n: num)
  42     requires { valid n }
  43     ensures  { value n = 0 <-> n = Nil }
  44     variant  { n }
  45   = match n with Nil -> () | Cons _ r -> msd r end
  46
  47   let rec add_digit (n: num) (d: digit) : num
  48     requires { valid n }
  49     requires { 0 <= d < base }
  50     ensures  { valid result }
  51     ensures  { value result = value n + d }
  52     variant  { n }
  53   = match n with
  54     | Nil ->
  55         if d = 0 then Nil else Cons d Nil
  56     | Cons d0 r ->
  57         if d + d0 < base then Cons (d + d0) r
  58         else Cons (d + d0 - base) (add_digit r 1)
  59     end
  60
  61   let rec add_cin (n1 n2: num) (cin: int) : num
  62     requires { valid n1 && valid n2 && 0 <= cin <= 1 }
  63     ensures  { valid result }
  64     ensures  { value result = value n1 + value n2 + cin }
  65     variant  { n1 }
  66   = match n1, n2 with
  67     | Nil, _ ->
  68         add_digit n2 cin
  69     | Cons _ _, Nil ->
  70         add_digit n1 cin
  71     | Cons d1 r1, Cons d2 r2 ->
  72         let d = cin + d1 + d2 in
  73         if d < base then Cons d          (add_cin r1 r2 0)
  74                     else Cons (d - base) (add_cin r1 r2 1)
  75     end
  76
  77   let add (n1 n2: num) : num
  78     requires { valid n1 && valid n2 }
  79     ensures  { valid result }
  80     ensures  { value result = value n1 + value n2 }
  81   = add_cin n1 n2 0
  82
  83 end