Define and prove mul.

examples/in_progress/mp.mlw

@@ -166,10 +166,9 @@ module N
 
 
   let rec lemma value_sub_lower_bound (x:map int limb) (x1 x2:int)
-    requires { x1 <= x2 }
     variant  { x2 - x1 }
     ensures  { 0 <= value_sub x x1 x2 }
-  = if x1 = x2 then () else
+  = if x2 <= x1 then () else
       begin
         assert { value_sub x x1 x2 = l2i (Map.get x x1) + radix * value_sub x (x1+1) x2};
         value_sub_lower_bound x (x1+1) x2
@@ -505,6 +504,21 @@ module N
     done;
     !c
 
+  let mul (x y:t):t
+    ensures { value result = value x * value y }
+    raises  { TooManyDigits -> true }
+  = let limb_zero = Limb.of_int 0 in
+    let zero = Int31.of_int 0 in
+    let lx = x.digits.length in
+    let ly = y.digits.length in
+    if Int31.(>) lx (Int31.(-) (of_int 0x3FFFFFFF) ly) then raise TooManyDigits;
+    let zd = Array31.make (Int31.(+) lx ly) limb_zero in
+    assert { MapEq.map_eq_sub zd.elts (Map.const limb_zero) 0 (p2i lx + p2i ly) };
+    assert { value_sub zd.elts 0 (p2i lx + p2i ly) = 0 };
+    let c = mul_limbs zd x.digits y.digits zero zero lx zero ly in
+    assert { l2i c = 0 };
+    { digits = zd }
+
 end
 
 

examples/in_progress/mp/mp_N_WP_parameter_mul_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require map.Map.
+Require int.Int.
+Require int.Abs.
+Require int.ComputerDivision.
+Require int.Power.
+
+(* Why3 assumption *)
+Definition unit := unit.
+
+Axiom qtmark : Type.
+Parameter qtmark_WhyType : WhyType qtmark.
+Existing Instance qtmark_WhyType.
+
+Axiom int31 : Type.
+Parameter int31_WhyType : WhyType int31.
+Existing Instance int31_WhyType.
+
+Parameter to_int: int31 -> Z.
+
+(* Why3 assumption *)
+Definition in_bounds (n:Z): Prop := ((-1073741824%Z)%Z <= n)%Z /\
+  (n <= 1073741823%Z)%Z.
+
+Axiom to_int_in_bounds : forall (n:int31), (in_bounds (to_int n)).
+
+Axiom extensionality : forall (x:int31) (y:int31),
+  ((to_int x) = (to_int y)) -> (x = y).
+
+(* Why3 assumption *)
+Inductive array
+  (a:Type) :=
+  | mk_array : int31 -> (map.Map.map Z a) -> array a.
+Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
+Existing Instance array_WhyType.
+Implicit Arguments mk_array [[a]].
+
+(* Why3 assumption *)
+Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
+  match v with
+  | (mk_array x x1) => x1
+  end.
+
+(* Why3 assumption *)
+Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): int31 :=
+  match v with
+  | (mk_array x x1) => x
+  end.
+
+(* Why3 assumption *)
+Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
+  (map.Map.get (elts a1) i).
+
+(* Why3 assumption *)
+Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
+  a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
+
+(* Why3 assumption *)
+Definition make {a:Type} {a_WT:WhyType a} (n:int31) (v:a): (array a) :=
+  (mk_array n (map.Map.const v: (map.Map.map Z a))).
+
+(* Why3 assumption *)
+Inductive ref (a:Type) :=
+  | mk_ref : a -> ref a.
+Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
+Existing Instance ref_WhyType.
+Implicit Arguments mk_ref [[a]].
+
+(* Why3 assumption *)
+Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
+  match v with
+  | (mk_ref x) => x
+  end.
+
+Axiom uint32 : Type.
+Parameter uint32_WhyType : WhyType uint32.
+Existing Instance uint32_WhyType.
+
+Parameter to_int1: uint32 -> Z.
+
+(* Why3 assumption *)
+Definition in_bounds1 (n:Z): Prop := (0%Z <= n)%Z /\ (n <= 4294967295%Z)%Z.
+
+Axiom to_int_in_bounds1 : forall (n:uint32), (in_bounds1 (to_int1 n)).
+
+Axiom extensionality1 : forall (x:uint32) (y:uint32),
+  ((to_int1 x) = (to_int1 y)) -> (x = y).
+
+Parameter zero_unsigned: uint32.
+
+Axiom zero_unsigned_is_zero : ((to_int1 zero_unsigned) = 0%Z).
+
+(* Why3 assumption *)
+Definition limb := uint32.
+
+Axiom limb_max_bound : (1%Z <= 4294967295%Z)%Z.
+
+(* Why3 assumption *)
+Inductive t :=
+  | mk_t : (array uint32) -> t.
+Axiom t_WhyType : WhyType t.
+Existing Instance t_WhyType.
+
+(* Why3 assumption *)
+Definition digits (v:t): (array uint32) := match v with
+  | (mk_t x) => x
+  end.
+
+Parameter value_sub: (map.Map.map Z uint32) -> Z -> Z -> Z.
+
+Axiom value_sub_next : forall (x:(map.Map.map Z uint32)) (n:Z) (m:Z),
+  ((n < m)%Z -> ((value_sub x n m) = ((to_int1 (map.Map.get x
+  n)) + ((4294967295%Z + 1%Z)%Z * (value_sub x (n + 1%Z)%Z m))%Z)%Z)) /\
+  ((~ (n < m)%Z) -> ((value_sub x n m) = 0%Z)).
+
+(* Why3 assumption *)
+Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a))
+  (a2:(map.Map.map Z a)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\
+  (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)).
+
+Axiom value_sub_frame : forall (x:(map.Map.map Z uint32)) (y:(map.Map.map Z
+  uint32)) (n:Z) (m:Z), (map_eq_sub x y n m) -> ((value_sub x n
+  m) = (value_sub y n m)).
+
+Axiom value_sub_tail : forall (x:(map.Map.map Z uint32)) (n:Z) (m:Z),
+  (n <= m)%Z -> ((value_sub x n (m + 1%Z)%Z) = ((value_sub x n
+  m) + ((to_int1 (map.Map.get x m)) * (int.Power.power (4294967295%Z + 1%Z)%Z
+  (m - n)%Z))%Z)%Z).
+
+Axiom value_sub_concat : forall (x:(map.Map.map Z uint32)) (n:Z) (m:Z) (l:Z),
+  ((n <= m)%Z /\ (m <= l)%Z) -> ((value_sub x n l) = ((value_sub x n
+  m) + ((value_sub x m l) * (int.Power.power (4294967295%Z + 1%Z)%Z
+  (m - n)%Z))%Z)%Z).
+
+(* Why3 assumption *)
+Definition value_array (x:(array uint32)): Z := (value_sub (elts x) 0%Z
+  (to_int (length x))).
+
+(* Why3 assumption *)
+Definition value (x:t): Z := (value_array (digits x)).
+
+Axiom value_sub_update : forall (x:(map.Map.map Z uint32)) (i:Z) (n:Z) (m:Z)
+  (v:uint32), ((n <= i)%Z /\ (i < m)%Z) -> ((value_sub (map.Map.set x i v) n
+  m) = ((value_sub x n m) + ((int.Power.power (4294967295%Z + 1%Z)%Z
+  (i - n)%Z) * ((to_int1 v) - (to_int1 (map.Map.get x i)))%Z)%Z)%Z).
+
+Axiom value_zero : forall (x:(map.Map.map Z uint32)) (n:Z) (m:Z), (map_eq_sub
+  x (map.Map.const zero_unsigned: (map.Map.map Z uint32)) n m) ->
+  ((value_sub x n m) = 0%Z).
+
+Axiom value_sub_lower_bound : forall (x:(map.Map.map Z uint32)) (x1:Z)
+  (x2:Z), (0%Z <= (value_sub x x1 x2))%Z.
+
+Axiom value_sub_upper_bound : forall (x:(map.Map.map Z uint32)) (x1:Z)
+  (x2:Z), (x1 <= x2)%Z -> ((value_sub x x1
+  x2) < (int.Power.power (4294967295%Z + 1%Z)%Z (x2 - x1)%Z))%Z.
+
+Axiom value_sub_lower_bound_tight : forall (x:(map.Map.map Z uint32)) (x1:Z)
+  (x2:Z), (x1 < x2)%Z -> (((int.Power.power (4294967295%Z + 1%Z)%Z
+  ((x2 - x1)%Z - 1%Z)%Z) * (to_int1 (map.Map.get x
+  (x2 - 1%Z)%Z)))%Z <= (value_sub x x1 x2))%Z.
+
+Axiom value_sub_upper_bound_tight : forall (x:(map.Map.map Z uint32)) (x1:Z)
+  (x2:Z), (x1 <= x2)%Z -> ((value_sub x x1
+  x2) < (int.Power.power (4294967295%Z + 1%Z)%Z (x2 - x1)%Z))%Z.
+
+Axiom value_sub_upper_bound_tighter : forall (x:(map.Map.map Z uint32))
+  (x1:Z) (x2:Z), (x1 < x2)%Z -> ((value_sub x x1
+  x2) < ((int.Power.power (4294967295%Z + 1%Z)%Z
+  ((x2 - x1)%Z - 1%Z)%Z) * ((to_int1 (map.Map.get x
+  (x2 - 1%Z)%Z)) + 1%Z)%Z)%Z)%Z.
+
+Parameter compare_int: Z -> Z -> Z.
+
+Axiom compare_int_def : forall (x:Z) (y:Z), ((x < y)%Z -> ((compare_int x
+  y) = (-1%Z)%Z)) /\ ((~ (x < y)%Z) -> (((x = y) -> ((compare_int x
+  y) = 0%Z)) /\ ((~ (x = y)) -> ((compare_int x y) = 1%Z)))).
+
+(* Why3 goal *)
+Theorem WP_parameter_mul : forall (x:int31) (x1:(map.Map.map Z uint32))
+  (y:int31) (y1:(map.Map.map Z uint32)), ((0%Z <= (to_int x))%Z /\
+  (0%Z <= (to_int y))%Z) -> ((in_bounds1 0%Z) -> forall (limb_zero:uint32),
+  ((to_int1 limb_zero) = 0%Z) -> ((in_bounds 0%Z) -> forall (zero:int31),
+  ((to_int zero) = 0%Z) -> ((in_bounds 1073741823%Z) -> forall (o:int31),
+  ((to_int o) = 1073741823%Z) -> ((in_bounds ((to_int o) - (to_int y))%Z) ->
+  forall (o1:int31), ((to_int o1) = ((to_int o) - (to_int y))%Z) ->
+  forall (result:bool), ((result = true) <-> ((to_int o1) < (to_int x))%Z) ->
+  ((~ (result = true)) -> ((in_bounds ((to_int x) + (to_int y))%Z) ->
+  forall (o2:int31), ((to_int o2) = ((to_int x) + (to_int y))%Z) ->
+  ((0%Z <= (to_int o2))%Z -> ((0%Z <= (to_int o2))%Z -> ((map_eq_sub
+  (map.Map.const limb_zero: (map.Map.map Z uint32))
+  (map.Map.const limb_zero: (map.Map.map Z uint32)) 0%Z
+  ((to_int x) + (to_int y))%Z) ->
+  (((value_sub (map.Map.const limb_zero: (map.Map.map Z uint32)) 0%Z
+  ((to_int x) + (to_int y))%Z) = 0%Z) -> ((((0%Z <= (to_int zero))%Z /\
+  (((to_int zero) <= (to_int x))%Z /\ ((to_int x) <= (to_int x))%Z)) /\
+  (((0%Z <= (to_int zero))%Z /\ (((to_int zero) <= (to_int y))%Z /\
+  ((to_int y) <= (to_int y))%Z)) /\ ((0%Z <= (to_int zero))%Z /\
+  ((((to_int zero) + ((to_int x) - (to_int zero))%Z)%Z + ((to_int y) - (to_int zero))%Z)%Z <= (to_int o2))%Z))) ->
+  forall (zd:(map.Map.map Z uint32)), forall (c:uint32),
+  ((0%Z <= (to_int o2))%Z /\ (((value_sub zd 0%Z
+  (to_int o2)) + ((int.Power.power (4294967295%Z + 1%Z)%Z
+  (((to_int zero) + ((to_int x) - (to_int zero))%Z)%Z + ((to_int y) - (to_int zero))%Z)%Z) * (to_int1 c))%Z)%Z = ((value_sub (map.Map.const limb_zero: (map.Map.map
+  Z uint32)) 0%Z (to_int o2)) + ((int.Power.power (4294967295%Z + 1%Z)%Z
+  (to_int zero)) * ((value_sub x1 (to_int zero) (to_int x)) * (value_sub y1
+  (to_int zero) (to_int y)))%Z)%Z)%Z)) -> ((to_int1 c) = 0%Z)))))))))))).
+(* Why3 intros x x1 y y1 (h1,h2) h3 limb_zero h4 h5 zero h6 h7 o h8 h9 o1 h10
+        result h11 h12 h13 o2 h14 h15 h16 h17 h18
+        ((h19,(h20,h21)),((h22,(h23,h24)),(h25,h26))) zd c (h27,h28). *)
+Proof.
+intros x x1 y y1 (h1,h2) h3 limb_zero h4 h5 zero h6 h7 o h8 h9 o1 h10 result
+h11 h12 h13 o2 h14 h15 h16 h17 h18
+((h19,(h20,h21)),((h22,(h23,h24)),(h25,h26))) zd c (h27,h28).
+apply Zle_antisym.
+2: apply to_int_in_bounds1.
+apply Z.le_ngt.
+intros H.
+revert h28.
+rewrite h6, 2!Zminus_0_r, Power.Power_0, Zmult_1_l.
+rewrite h14, h18, 2!Zplus_0_l.
+intros H1.
+assert (H2 := value_sub_upper_bound_tight x1 0 (to_int x) h1).
+assert (H3 := value_sub_upper_bound_tight y1 0 (to_int y) h2).
+rewrite Zminus_0_r in H2, H3.
+refine (_ (Zmult_lt_compat _ _ _ _ (conj _ H2) (conj _ H3))).
+apply Z.le_ngt.
+rewrite <- H1.
+rewrite <- Power.Power_sum by easy.
+pattern ((4294967295 + 1) ^ (to_int x + to_int y))%Z at 1 ;
+  replace ((4294967295 + 1) ^ (to_int x + to_int y))%Z with (0 + (4294967295 + 1) ^ (to_int x + to_int y) * 1)%Z by ring.
+apply Zplus_le_compat.
+apply value_sub_lower_bound.
+apply Zmult_le_compat_l.
+apply (Zlt_le_succ _ _ H).
+apply Power.Power_non_neg.
+split.
+easy.
+now apply (Zplus_le_compat 0 _ 0).
+apply value_sub_lower_bound.
+apply value_sub_lower_bound.
+Qed.
+