Commit cc6d1e85 by Guillaume Melquiond

Define and prove mul_limbs.

parent 03d30160
 ... ... @@ -364,7 +364,7 @@ module N let add_aux_in_place (x:t) (y:array limb) : unit requires { p2i x.digits.length >= p2i y.length } writes { x.digits, x.digits.elts } writes { x.digits, x.digits.elts } ensures { value x = value (old x) + value_array y } raises { TooManyDigits -> true } = 'Init: ... ... @@ -388,7 +388,7 @@ module N end let add_in_place (x y:t) : unit writes { x.digits, x.digits.elts } writes { x.digits, x.digits.elts } ensures { value x = value (old x) + value y } raises { TooManyDigits -> true } = let lx = x.digits.length in ... ... @@ -440,7 +440,7 @@ module N 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 { forall j. 0 <= j < p2i z1 \/ p2i z1 + (p2i x2 - p2i x1) <= j < p2i z.length -> z[j] = (old z)[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: ... ... @@ -449,7 +449,7 @@ module N 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 -> invariant { forall j. 0 <= j < p2i z1 \/ p2i z1 + (p2i x2 - p2i x1) <= j < p2i z.length -> z[j] = (at z 'Init)[j] } invariant { p2i x1 <= p2i !i <= p2i x2 } invariant { ... ... @@ -470,6 +470,40 @@ module N done; !c let mul_limbs (z x y:array limb) (z1 x1 x2 y1 y2:int31) : limb requires { 0 <= p2i x1 <= p2i x2 <= p2i x.length } requires { 0 <= p2i y1 <= p2i y2 <= p2i y.length } requires { 0 <= p2i z1 } requires { p2i z1 + (p2i x2 - p2i x1) + (p2i y2 - p2i y1) <= p2i z.length } writes { z } ensures { forall j. 0 <= j < p2i z1 \/ p2i z1 + (p2i x2 - p2i x1) + (p2i y2 - p2i y1) <= j < p2i z.length -> x[j] = (old x)[j] } ensures { value_array z + power radix (p2i z1 + (p2i x2 - p2i x1) + (p2i y2 - p2i y1)) * l2i result = value_array (old z) + power radix (p2i z1) * (value_sub x.elts (p2i x1) (p2i x2) * value_sub y.elts (p2i y1) (p2i y2)) } = 'Init: let limb_zero = Limb.of_int 0 in let one = Int31.of_int 1 in let c = ref limb_zero in let i = ref y1 in while Int31.(<) !i y2 do invariant { forall j. 0 <= j < p2i z1 \/ p2i z1 + (p2i x2 - p2i x1) + (p2i y2 - p2i y1) <= j < p2i z.length -> z[j] = (at z 'Init)[j] } invariant { p2i y1 <= p2i !i <= p2i y2 } invariant { value_array z + power radix (p2i z1 + (p2i x2 - p2i x1) + (p2i !i - p2i y1)) * l2i !c = value_array (at z 'Init) + power radix (p2i z1) * (value_sub x.elts (p2i x1) (p2i x2) * value_sub y.elts (p2i y1) (p2i !i)) } invariant { 0 <= l2i !c <= 1 } variant { p2i y2 - p2i !i } let j = Int31.(+) z1 (Int31.(-) !i y1) in let d = mul_limb z x y[!i] j x1 x2 in let k = Int31.(+) j (Int31.(-) x2 x1) in let (v,c') = Limb.add_with_carry z[k] d !c in z[k] <- v; c := 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_limbs : forall (z:int31) (z1:(map.Map.map Z uint32)) (x:int31) (x1:(map.Map.map Z uint32)) (y:int31) (y1:(map.Map.map Z uint32)) (z11:int31) (x11:int31) (x2:int31) (y11:int31) (y2:int31), ((((0%Z <= (to_int z))%Z /\ (0%Z <= (to_int x))%Z) /\ (0%Z <= (to_int y))%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 y11))%Z /\ (((to_int y11) <= (to_int y2))%Z /\ ((to_int y2) <= (to_int y))%Z)) /\ ((0%Z <= (to_int z11))%Z /\ ((((to_int z11) + ((to_int x2) - (to_int x11))%Z)%Z + ((to_int y2) - (to_int y11))%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 (i:int31) (c:uint32) (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 + ((to_int y2) - (to_int y11))%Z)%Z <= j)%Z /\ (j < (to_int z))%Z)) -> ((map.Map.get z2 j) = (map.Map.get z1 j))) /\ ((((to_int y11) <= (to_int i))%Z /\ ((to_int i) <= (to_int y2))%Z) /\ ((((value_sub z2 0%Z (to_int z)) + ((int.Power.power (4294967295%Z + 1%Z)%Z (((to_int z11) + ((to_int x2) - (to_int x11))%Z)%Z + ((to_int i) - (to_int y11))%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 x2)) * (value_sub y1 (to_int y11) (to_int i)))%Z)%Z)%Z) /\ ((0%Z <= (to_int1 c))%Z /\ ((to_int1 c) <= 1%Z)%Z)))) -> forall (result:bool), ((result = true) <-> ((to_int i) < (to_int y2))%Z) -> ((result = true) -> ((in_bounds ((to_int i) - (to_int y11))%Z) -> forall (o:int31), ((to_int o) = ((to_int i) - (to_int y11))%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 i))%Z /\ ((to_int i) < (to_int y))%Z) -> (((0%Z <= (to_int z))%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 j))%Z /\ (((to_int j) + ((to_int x2) - (to_int x11))%Z)%Z <= (to_int z))%Z))) -> forall (z3:(map.Map.map Z uint32)), forall (d:uint32), ((0%Z <= (to_int z))%Z /\ ((forall (j1:Z), (((0%Z <= j1)%Z /\ (j1 < (to_int j))%Z) \/ ((((to_int j) + ((to_int x2) - (to_int x11))%Z)%Z <= j1)%Z /\ (j1 < (to_int z))%Z)) -> ((map.Map.get z3 j1) = (map.Map.get z2 j1))) /\ (((value_sub z3 0%Z (to_int z)) + ((int.Power.power (4294967295%Z + 1%Z)%Z ((to_int j) + ((to_int x2) - (to_int x11))%Z)%Z) * (to_int1 d))%Z)%Z = ((value_sub z2 0%Z (to_int z)) + ((int.Power.power (4294967295%Z + 1%Z)%Z (to_int j)) * ((value_sub x1 (to_int x11) (to_int x2)) * (to_int1 (map.Map.get y1 (to_int i))))%Z)%Z)%Z))) -> ((in_bounds ((to_int x2) - (to_int x11))%Z) -> forall (o1:int31), ((to_int o1) = ((to_int x2) - (to_int x11))%Z) -> ((in_bounds ((to_int j) + (to_int o1))%Z) -> forall (k:int31), ((to_int k) = ((to_int j) + (to_int o1))%Z) -> (((0%Z <= (to_int k))%Z /\ ((to_int k) < (to_int z))%Z) -> (((0%Z <= (to_int1 c))%Z /\ ((to_int1 c) <= 1%Z)%Z) -> forall (result1:uint32) (result2:uint32), (((to_int1 result1) + ((4294967295%Z + 1%Z)%Z * (to_int1 result2))%Z)%Z = (((to_int1 (map.Map.get z3 (to_int k))) + (to_int1 d))%Z + (to_int1 c))%Z) -> (((0%Z <= (to_int k))%Z /\ ((to_int k) < (to_int z))%Z) -> forall (z4:(map.Map.map Z uint32)), ((0%Z <= (to_int z))%Z /\ (z4 = (map.Map.set z3 (to_int k) result1))) -> forall (c1:uint32), (c1 = result2) -> ((in_bounds ((to_int i) + (to_int one))%Z) -> forall (o2:int31), ((to_int o2) = ((to_int i) + (to_int one))%Z) -> forall (i1:int31), (i1 = o2) -> (((value_sub z4 0%Z (to_int z)) + ((int.Power.power (4294967295%Z + 1%Z)%Z (((to_int z11) + ((to_int x2) - (to_int x11))%Z)%Z + ((to_int i1) - (to_int y11))%Z)%Z) * (to_int1 c1))%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 x2)) * (value_sub y1 (to_int y11) (to_int i1)))%Z)%Z)%Z)))))))))))))). Proof. intros z z1 x x1 y y1 z11 x11 x2 y11 y2 (((h1,h2),h3),((h4,(h5,h6)),((h7,(h8,h9)),(h10,h11)))) h12 limb_zero h13 h14 one h15 i c z2 (h16,((h17,h18),(h19,(h20,h21)))) result h22 h23 h24 o h25 h26 j h27 (h28,h29) (h30,((h31,(h32,h33)),(h34,h35))) z3 d (h36,(h37,h38)) h39 o1 h40 h41 k h42 (h43,h44) (h45,h46) result1 result2 h47 (h48,h49) z4 (h50,h51) c1 h52 h53 o2 h54 i1 h55. assert (Hr: forall p q r, Zplus p q = r -> p = Zminus r q) by (intros p q r H ; rewrite <- H ; ring). rewrite h51. rewrite value_sub_update by now split. rewrite Hr with (1 := h38). rewrite Hr with (1 := h19). rewrite h55, h54, h15. rewrite value_sub_tail with (1 := h17). rewrite Hr with (1 := h47). rewrite h52. set (radix := (4294967295 + 1)%Z). replace (to_int z11 + (to_int x2 - to_int x11) + (to_int i + 1 - to_int y11))%Z with (to_int z11 + (to_int x2 - to_int x11) + (to_int i - to_int y11) + 1)%Z by ring. rewrite Power.Power_s by (clear -h25 h40 h27 h42 h43 ; omega). rewrite Zminus_0_r. rewrite h42, h40, h27, h25. replace (to_int z11 + (to_int i - to_int y11) + (to_int x2 - to_int x11))%Z with (to_int z11 + (to_int x2 - to_int x11) + (to_int i - to_int y11))%Z by ring. apply Zminus_eq. ring_simplify. rewrite Power.Power_sum with (1 := h10). ring. now apply Zle_minus_le_0. Qed.
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!