Commit 503ddd14 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add and prove mul_limb.

parent 0fac64a3
......@@ -284,7 +284,7 @@ module N
(** {2 addition} *)
(** {2 Addition} *)
exception Break
......@@ -307,7 +307,7 @@ module N
value_array x + power radix (p2i !i) * l2i !c =
value_array (at x 'Init) + power radix (p2i x1) * l2i y }
variant { p2i x2 - p2i !i }
let (r,c') = Limb.add_with_carry x[!i] limb_zero !c in
let (r,c') = Limb.add_with_carry x[!i] !c limb_zero in
'L:
x[!i] <- r;
assert { value_array x = value_array (at x 'L)
......@@ -341,6 +341,7 @@ module N
value_array x + power radix j * l2i !c
= value_array (at x 'Init) +
power radix (p2i x1) * value_sub y.elts (p2i y1) (p2i !i) }
invariant { 0 <= l2i !c <= 1 }
variant { p2i y2 - p2i !i }
let j = Int31.(+) x1 (Int31.(-) !i y1) in
let (r,c') = Limb.add_with_carry x[j] y[!i] !c in
......@@ -430,6 +431,44 @@ module N
else
{ digits = add_array y.digits x.digits }
(** {2 Multiplication} *)
let mul_limb (z x:array limb) (y:limb) (z1 x1 x2:int31) : limb
requires { 0 <= p2i x1 <= p2i x2 <= p2i x.length }
requires { 0 <= p2i z1 }
requires { p2i z1 + (p2i x2 - p2i x1) <= p2i z.length }
writes { z }
ensures { forall j. 0 <= j < p2i z1 \/ p2i z1 + (p2i x2 - p2i x1) <= j < p2i x.length -> x[j] = (old x)[j] }
ensures { value_array z + power radix (p2i z1 + (p2i x2 - p2i x1)) * l2i result
= value_array (old z) + power radix (p2i z1) * (value_sub x.elts (p2i x1) (p2i x2) * l2i y) }
= 'Init:
let limb_zero = Limb.of_int 0 in
let one = Int31.of_int 1 in
let i = ref x1 in
let c = ref limb_zero in
while Int31.(<) !i x2 do
invariant { forall j. 0 <= j < p2i z1 \/ p2i z1 + (p2i x2 - p2i x1) <= j < p2i x.length ->
z[j] = (at z 'Init)[j] }
invariant { p2i x1 <= p2i !i <= p2i x2 }
invariant {
value_array z + power radix (p2i z1 + (p2i !i - p2i x1)) * l2i !c =
value_array (at z 'Init) + power radix (p2i z1) * (value_sub x.elts (p2i x1) (p2i !i) * l2i y) }
variant { p2i x2 - p2i !i }
let (rl,rh) = Limb.mul_double x[!i] y in
let j = Int31.(+) z1 (Int31.(-) !i x1) in
let (v,c') = Limb.add3 z[j] rl !c in
assert { 0 <= l2i z[p2i j] + l2i !c + l2i x[p2i !i] * l2i y <= radix * radix - 1 };
assert { l2i v + radix * (l2i rh + l2i c') = l2i z[p2i j] + l2i !c + l2i x[p2i !i] * l2i y };
'L:
z[j] <- v;
assert { value_array z = value_array (at z 'L)
+ power radix (p2i z1 + (p2i !i - p2i x1)) * (l2i v - l2i (at z 'L)[p2i z1 + (p2i !i - p2i x1)]) };
c := Limb.(+) rh c';
i := Int31.(+) !i one;
done;
!c
end
......
(* 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), (x1 <= 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_limb : forall (z:int31) (z1:(map.Map.map Z uint32))
(x:int31) (x1:(map.Map.map Z uint32)) (y:uint32) (z11:int31) (x11:int31)
(x2:int31), (((0%Z <= (to_int z))%Z /\ (0%Z <= (to_int x))%Z) /\
(((0%Z <= (to_int x11))%Z /\ (((to_int x11) <= (to_int x2))%Z /\
((to_int x2) <= (to_int x))%Z)) /\ ((0%Z <= (to_int z11))%Z /\
(((to_int z11) + ((to_int x2) - (to_int x11))%Z)%Z <= (to_int z))%Z))) ->
((in_bounds1 0%Z) -> forall (limb_zero:uint32),
((to_int1 limb_zero) = 0%Z) -> ((in_bounds 1%Z) -> forall (one:int31),
((to_int one) = 1%Z) -> forall (c:uint32) (i:int31) (z2:(map.Map.map Z
uint32)), ((forall (j:Z), (((0%Z <= j)%Z /\ (j < (to_int z11))%Z) \/
((((to_int z11) + ((to_int x2) - (to_int x11))%Z)%Z <= j)%Z /\
(j < (to_int x))%Z)) -> ((map.Map.get z2 j) = (map.Map.get z1 j))) /\
((((to_int x11) <= (to_int i))%Z /\ ((to_int i) <= (to_int x2))%Z) /\
(((value_sub z2 0%Z (to_int z)) + ((int.Power.power (4294967295%Z + 1%Z)%Z
((to_int z11) + ((to_int i) - (to_int x11))%Z)%Z) * (to_int1 c))%Z)%Z = ((value_sub z1
0%Z (to_int z)) + ((int.Power.power (4294967295%Z + 1%Z)%Z
(to_int z11)) * ((value_sub x1 (to_int x11)
(to_int i)) * (to_int1 y))%Z)%Z)%Z))) -> forall (result:bool),
((result = true) <-> ((to_int i) < (to_int x2))%Z) -> ((result = true) ->
(((0%Z <= (to_int i))%Z /\ ((to_int i) < (to_int x))%Z) ->
forall (result1:uint32) (result2:uint32),
(((to_int1 result1) + ((4294967295%Z + 1%Z)%Z * (to_int1 result2))%Z)%Z = ((to_int1 (map.Map.get x1
(to_int i))) * (to_int1 y))%Z) -> ((in_bounds
((to_int i) - (to_int x11))%Z) -> forall (o:int31),
((to_int o) = ((to_int i) - (to_int x11))%Z) -> ((in_bounds
((to_int z11) + (to_int o))%Z) -> forall (j:int31),
((to_int j) = ((to_int z11) + (to_int o))%Z) -> (((0%Z <= (to_int z))%Z /\
((0%Z <= (to_int j))%Z /\ ((to_int j) < (to_int z))%Z)) ->
forall (result3:uint32) (result4:uint32),
(((to_int1 result3) + ((4294967295%Z + 1%Z)%Z * (to_int1 result4))%Z)%Z = (((to_int1 (map.Map.get z2
(to_int j))) + (to_int1 result1))%Z + (to_int1 c))%Z) ->
((0%Z <= (((to_int1 (map.Map.get z2
(to_int j))) + (to_int1 c))%Z + ((to_int1 (map.Map.get x1
(to_int i))) * (to_int1 y))%Z)%Z)%Z /\ ((((to_int1 (map.Map.get z2
(to_int j))) + (to_int1 c))%Z + ((to_int1 (map.Map.get x1
(to_int i))) * (to_int1 y))%Z)%Z <= (((4294967295%Z + 1%Z)%Z * (4294967295%Z + 1%Z)%Z)%Z - 1%Z)%Z)%Z)))))))).
Proof with try apply to_int_in_bounds1.
intros z z1 x x1 y z11 x11 x2 ((h1,h2),((h3,(h4,h5)),(h6,h7))) h8 limb_zero
h9 h10 one h11 c i z2 (h12,((h13,h14),h15)) result h16 h17 (h18,h19) result1
result2 h20 h21 o h22 h23 j h24 (h25,(h26,h27)) result3 result4 h28.
split.
replace 0%Z with (0 + 0 + 0 * 0)%Z by ring.
apply Zplus_le_compat...
apply Zplus_le_compat...
apply Zmult_le_compat ; try reflexivity...
set (max := 4294967295%Z).
replace ((max + 1) * (max + 1) - 1)%Z with (max + max + max * max)%Z by ring.
apply Zplus_le_compat...
apply Zplus_le_compat...
apply Zmult_le_compat...
Qed.
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -118,19 +118,20 @@ module Unsigned
axiom zero_unsigned_is_zero : to_int zero_unsigned = 0
val add_with_carry (x y:t) (c:t) : (t,t)
requires { 0 <= to_int c <= 1 }
returns { (r,d) ->
to_int r + (max+1) * to_int d =
to_int x + to_int y + to_int c }
val mul_with_carry (x y:t) : (t,t)
val add3 (x y z:t) : (t,t)
returns { (r,d) ->
to_int r + (max+1) * to_int d =
to_int x * to_int y }
to_int x + to_int y + to_int z }
val fused_mul_add (x y:t) (c:t) : (t,t)
val mul_double (x y:t) : (t,t)
returns { (r,d) ->
to_int r + (max+1) * to_int d =
to_int x * to_int y + to_int c }
to_int x * to_int y }
end
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment