examples/multiprecision/lemmas.mlw

   1 module Lemmas
   2
   3   use array.Array
   4   use map.Map
   5   use map.MapEq
   6   use map.Const
   7   use int.Int
   8
   9   (** {3 Complements to map standard library} *)
  10
  11   predicate map_eq_sub_shift (x y:map int 'a) (xi yi sz:int) =
  12     forall i. 0 <= i < sz -> x[xi+i] = y[yi+i]
  13
  14   let lemma map_eq_shift (x y:map int 'a) (xi yi sz k:int)
  15     requires { map_eq_sub_shift x y xi yi sz }
  16     requires { 0 <= k < sz }
  17     ensures { x[xi+k] = y[yi+k] }
  18   = ()
  19
  20   let rec lemma map_eq_shift_zero (x y: map int 'a) (n m: int)
  21     requires { map_eq_sub_shift x y n n (m-n) }
  22     variant { m - n }
  23     ensures { MapEq.map_eq_sub x y n m }
  24   =
  25     if n < m then
  26     begin
  27       assert { forall i. 0 <= i < m-n -> x[n+i] = y[n+i] };
  28       assert { forall i. n <= i < m ->
  29                  let j = i - n in 0 <= j < m-n ->
  30                      x[n+j] = y[n+j] -> x[i] = y[i]};
  31       map_eq_shift_zero x y (n+1) m;
  32     end
  33     else ()
  34
  35   use mach.int.Int32
  36   use ref.Ref
  37   use import mach.int.UInt64GMP as Limb
  38   use int.Int
  39   use int.Power
  40   use mach.c.C
  41   use types.Types
  42   use types.Int32Eq
  43   use types.UInt64Eq
  44
  45   meta compute_max_steps 0x100000
  46
  47   (** {3 Long integers as arrays of libs} *)
  48
  49   lemma limb_max_bound: 1 <= max_uint64
  50
  51   function l2i (x:limb) : int = Limb.to_int x
  52
  53   function p2i (i:int32) : int = int32'int i
  54
  55   let lemma prod_compat_strict_r (a b c:int)
  56     requires { 0 <= a < b }
  57     requires { 0 < c }
  58     ensures { c * a < c * b }
  59   = ()
  60
  61   let lemma prod_compat_r (a b c:int)
  62     requires { 0 <= a <= b }
  63     requires { 0 <= c }
  64     ensures { c * a <= c * b }
  65   = ()
  66
  67   let lemma prod_compat_strict_lr (a b c d:int)
  68     requires { 0 <= a < b }
  69     requires { 0 <= c < d }
  70     ensures  { a * c < b * d }
  71   = () (* assert { a * c < a * d = d * a < d * b = b * d } *)
  72
  73   meta remove_prop axiom prod_compat_strict_lr
  74
  75   let lemma prod_compat_lr (a b c d:int)
  76     requires { 0 <= a <= b }
  77     requires { 0 <= c <= d }
  78     ensures  { a * c <= b * d }
  79   = ()
  80
  81   meta remove_prop axiom prod_compat_lr
  82
  83   let lemma simp_compat_strict_l (a b c:int)
  84     requires { 0 <= a * b < a * c }
  85     requires { 0 < a }
  86     ensures  { b < c }
  87   = ()
  88
  89   meta remove_prop axiom simp_compat_strict_l
  90
  91   (** {3 Integer value of a natural number} *)
  92
  93   (** `value_sub x n m` denotes the integer represented by
  94      the digits `x[n..m-1]` with lsb at index n *)
  95   let rec ghost function value_sub (x:map int limb) (n:int) (m:int) : int
  96      variant {m - n}
  97    =
  98      if n < m then
  99        l2i x[n] + radix * value_sub x (n+1) m
 100        else 0
 101
 102   let rec lemma value_sub_frame (x y:map int limb) (n m:int)
 103     requires { MapEq.map_eq_sub x y n m }
 104     variant  { m - n }
 105     ensures  { value_sub x n m = value_sub y n m }
 106   =
 107     if n < m then value_sub_frame x y (n+1) m else ()
 108
 109   let rec lemma value_sub_frame_shift (x y:map int limb) (xi yi sz:int)
 110     requires { map_eq_sub_shift x y xi yi sz }
 111     variant { sz }
 112     ensures { value_sub x xi (xi+sz) = value_sub y yi (yi+sz) }
 113  =
 114     if sz>0
 115     then begin
 116       map_eq_shift x y xi yi sz 0;
 117       assert { forall i. 0 <= i < sz-1 ->
 118                  let j = 1+i in x[xi+j] = y[yi+j] };
 119       value_sub_frame_shift x y (xi+1) (yi+1) (sz-1)
 120       end
 121     else assert { 1+2 = 3 }
 122
 123   let rec lemma value_sub_tail (x:map int limb) (n m:int)
 124     requires { n <= m }
 125     variant  { m - n }
 126     ensures  {
 127       value_sub x n (m+1) =
 128         value_sub x n m + (Map.get x m) * power radix (m-n) }
 129   = [@vc:sp] if n < m then value_sub_tail x (n+1) m else ()
 130
 131   let rec lemma value_sub_concat (x:map int limb) (n m l:int)
 132     requires { n <= m <= l}
 133     variant  { m - n }
 134     ensures  {
 135       value_sub x n l =
 136         value_sub x n m + value_sub x m l * power radix (m-n) }
 137   =
 138   if n < m then
 139      begin
 140      assert {n<m};
 141      value_sub_concat x (n+1) m l
 142      end
 143   else ()
 144
 145   let lemma value_sub_head (x:map int limb) (n m:int)
 146     requires { n < m }
 147     ensures { value_sub x n m = x[n] + radix * value_sub x (n+1) m }
 148   = value_sub_concat x n (n+1) m
 149
 150   let lemma value_sub_update (x:map int limb) (i n m:int) (v:limb)
 151     requires { n <= i < m }
 152     ensures {
 153       value_sub (Map.set x i v) n m =
 154       value_sub x n m + power radix (i - n) * (v -(Map.get x i))
 155     }
 156   = assert { MapEq.map_eq_sub x (Map.set x i v) n i };
 157     assert { MapEq.map_eq_sub x (Map.set x i v) (i+1) m };
 158     value_sub_concat x n i m;
 159     value_sub_concat (Map.set x i v) n i m;
 160     value_sub_head x i m;
 161     value_sub_head (Map.set x i v) i m
 162
 163   let rec lemma value_zero (x:map int limb) (n m:int)
 164     requires { MapEq.map_eq_sub x (Const.const Limb.zero_unsigned) n m }
 165     variant  { m - n }
 166     ensures  { value_sub x n m = 0 }
 167   = if n < m then value_zero x (n+1) m else ()
 168
 169   let lemma value_sub_update_no_change (x: map int limb) (i n m: int) (v:limb)
 170      requires { n <= m }
 171      requires { i < n \/ m <= i }
 172      ensures { value_sub x n m = value_sub (Map.set x i v) n m }
 173   = value_sub_frame x (Map.set x i v) n m
 174
 175   let lemma value_sub_shift_no_change (x:map int limb) (ofs i sz:int) (v:limb)
 176      requires { i < 0 \/ sz <= i }
 177      requires { 0 <= sz }
 178      ensures { value_sub x ofs (ofs + sz) =
 179                value_sub (Map.set x (ofs+i) v) ofs (ofs+sz) }
 180   = value_sub_frame_shift x (Map.set x (ofs+i) v) ofs ofs sz
 181
 182   (** {3 Comparisons} *)
 183
 184   let rec lemma value_sub_lower_bound (x:map int limb) (x1 x2:int)
 185     variant  { x2 - x1 }
 186     ensures  { 0 <= value_sub x x1 x2 }
 187   = if x2 <= x1 then () else
 188       begin
 189         value_sub_head x x1 x2;
 190         value_sub_lower_bound x (x1+1) x2
 191       end
 192
 193   let rec lemma value_sub_upper_bound (x:map int limb) (x1 x2:int)
 194     requires { x1 <= x2 }
 195     variant  { x2 - x1 }
 196     ensures  { value_sub x x1 x2 < power radix (x2 - x1) }
 197   = if x1 = x2 then () else
 198       begin
 199       value_sub_tail x x1 (x2-1);
 200       assert { value_sub x x1 x2
 201                <= value_sub x x1 (x2-1) + power radix (x2-x1-1) * (radix - 1) };
 202       value_sub_upper_bound x x1 (x2-1)
 203       end
 204
 205   let lemma value_sub_lower_bound_tight (x:map int limb) (x1 x2:int)
 206     requires { x1 < x2 }
 207     ensures  { power radix (x2-x1-1) *  l2i (Map.get x (x2-1)) <= value_sub x x1 x2 }
 208   = assert   { value_sub x x1 x2 = value_sub x x1 (x2-1)
 209                + power radix (x2-x1-1) * l2i (Map.get x (x2-1)) }
 210
 211   let lemma value_sub_upper_bound_tight (x:map int limb) (x1 x2:int)
 212     requires { x1 < x2 }
 213     ensures  { value_sub x x1 x2 < power radix (x2-x1-1) *  (l2i (Map.get x (x2-1)) + 1) }
 214   = value_sub_upper_bound x x1 (x2-1)
 215
 216   function value (x:t) (sz:int) : int =
 217      value_sub (pelts x) x.offset (x.offset + sz)
 218
 219   let lemma value_tail (x:t) (sz:int32)
 220     requires { 0 <= sz }
 221     ensures  { value x (sz+1) = value x sz + (pelts x)[x.offset + sz] * power radix sz }
 222   = value_sub_tail (pelts x) x.offset (x.offset + p2i sz)
 223
 224   meta remove_prop axiom value_tail
 225
 226   let lemma value_concat (x:t) (n m:int32)
 227     requires { 0 <= n <= m }
 228     ensures  { value x m
 229              = value x n + power radix n
 230                             * value_sub (pelts x) (x.offset + n) (x.offset + m) }
 231
 232   = value_sub_concat (pelts x) x.offset (x.offset + p2i n) (x.offset + p2i m)
 233
 234
 235   let lemma value_sub_eq (x1 x2: map int limb) (n1 n2 m1 m2: int)
 236     requires { x1 = x2 }
 237     requires { n1 = n2 }
 238     requires { m1 = m2 }
 239     ensures  { value_sub x1 n1 m1 = value_sub x2 n2 m2 }
 240   = ()
 241
 242   meta remove_prop axiom value_sub_eq
 243
 244 end