Commit 0e49b657 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

Proof that the propagation of the carry in array mode is correct (ugly)

parent 6905bb75
......@@ -82,3 +82,118 @@ Definition reduce_light_bot n :=
let c := n / 2^(16) in
38 * c.
Definition backCarry (l:list Z) : (list Z) :=
match l with
| [] => []
| h :: q => let v := nth 15 l 0 in
(h + 38 * getCarry 16 v) :: slice 14 q ++ [getResidute 16 v]
end.
Lemma getResidute_0 : forall n, getResidute n 0 = 0.
Proof.
go.
Qed.
Lemma getCarry_0 : forall n, getCarry n 0 = 0.
Proof.
intro n.
apply Z.shiftr_0_l.
Qed.
Lemma backCarry_ToFF : forall l, (length l <= 16)%nat -> ToFF 16 l :𝓟 = (ToFF 16 (backCarry l) :𝓟).
Proof.
destruct l as [| h l]; intro Hlength.
- go.
- unfold backCarry.
rewrite ToFF_cons.
rewrite ToFF_cons.
rewrite ToFF_app ; try omega.
apply le_lt_eq_dec in Hlength.
destruct Hlength.
+ rename l0 into H.
replace (nth 15 (h :: l) 0) with 0.
simpl in H.
apply lt_S_n in H.
replace (slice 14 l) with l.
rewrite getResidute_0.
rewrite getCarry_0.
replace (ToFF 16 [0]) with 0.
f_equal.
ring.
go.
symmetry.
apply slice_length_le.
omega.
symmetry.
apply nth_overflow.
omega.
+ rename e into H.
destruct l ; [inversion H|].
destruct l ; [inversion H|].
destruct l ; [inversion H|].
destruct l ; [inversion H|].
destruct l ; [inversion H|].
destruct l ; [inversion H|].
destruct l ; [inversion H|].
destruct l ; [inversion H|].
destruct l ; [inversion H|].
destruct l ; [inversion H|].
destruct l ; [inversion H|].
destruct l ; [inversion H|].
destruct l ; [inversion H|].
destruct l ; [inversion H|].
destruct l ; [inversion H|].
destruct l ; [inversion H|].
{
clear H.
replace (nth 15 [h; z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13] 0) with z13 by go.
replace (slice 14 [z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13]) with
[z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12] by go.
replace ([z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12; z13]) with ([z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12] ++ [ z13]) by go.
rewrite ToFF_app ; try omega.
replace (length [z; z0; z1; z2; z3; z4; z5; z6; z7; z8; z9; z10; z11; z12]) with 14%nat by go.
replace (ToFF 16 [getResidute 16 z13]) with (getResidute 16 z13) by go.
replace (ToFF 16 [z13]) with z13 by go.
rewrite <- Zred_factor4.
rewrite <- Zred_factor4.
rewrite Zplus_assoc_reverse.
rewrite <- Z.add_mod_idemp_r by (compute ; omega).
symmetry.
rewrite <- Z.add_mod_idemp_r by (compute ; omega).
f_equal.
f_equal.
rewrite Z.add_shuffle3.
rewrite <- Z.add_mod_idemp_r by (compute ; omega).
symmetry.
rewrite <- Z.add_mod_idemp_r by (compute ; omega).
f_equal.
f_equal.
rewrite <- Z.add_mod_idemp_l by (compute ; omega).
symmetry.
rewrite Zmult_mod.
rewrite <- t2256is38.
rewrite <- Zmult_mod.
rewrite Z.add_mod_idemp_l by (compute ; omega).
replace 256 with (16 + 16 * 15) by omega.
rewrite Z.pow_add_r by omega.
rewrite Zmult_assoc_reverse.
rewrite Zred_factor4.
rewrite Zmult_mod.
symmetry.
rewrite Zmult_mod.
f_equal.
f_equal.
replace (2 ^ (16 * 15)) with (2 ^ (16 * 14) * 2 ^ 16) by (compute ; omega).
replace (. 14) with 14 by (compute ; omega).
rewrite Zmult_mod.
symmetry.
rewrite Zmult_assoc_reverse.
rewrite Zred_factor4.
rewrite Zmult_mod.
f_equal.
f_equal.
rewrite Z.add_comm.
rewrite residuteCarry ; go.
}
inversion H.
Qed.
......@@ -106,6 +106,10 @@ Proof.
intros a b ; go.
Qed.
Lemma ToFF_add : forall m a b, ToFF (m + a :: b) = m + ToFF (a :: b).
Proof.
intros m a b ; go.
Qed.
Lemma ToFF_app : forall a b, ToFF (a ++ b) = ToFF a + 2^(n * . (length a)) * ToFF b.
Proof.
......@@ -182,12 +186,35 @@ Fixpoint Carrying (a:Z) (l:list Z) : list Z := match a,l with
| a,h :: q => getResidute (a + h) :: Carrying (getCarry (a + h)) q
end.
Fixpoint Carrying_n (n:nat) (a:Z) (l:list Z) : list Z := match n,a,l with
| _, 0,[] => []
| _, a,[] => [a]
| 0%nat, a,h::q => (a + h) :: q
| S p,a,h :: q => getResidute (a + h) :: Carrying_n p (getCarry (a + h)) q
end.
Lemma Carry_n_step: forall m a h q, Carrying_n (S m) a (h :: q) = getResidute (a + h) :: Carrying_n m (getCarry (a + h)) q.
Proof.
intros.
simpl.
flatten.
Qed.
Lemma Carrying_n_length: forall l (m:nat) a, m = length l -> Carrying_n m a l = Carrying a l.
Proof.
induction l as [|h q IHl]; intros m a Hm; go.
destruct m.
inv Hm.
simpl in *.
inversion Hm.
flatten ; f_equal ; go.
Qed.
Lemma CarryPreserveConst : forall l a , a + ToFF l = ToFF (Carrying a l).
Proof.
induction l as [| h q IHl].
intro a ; destruct a ; assert(Hn0: 2 ^ n * 0 = 0) by (symmetry ; apply Zmult_0_r_reverse) ; simpl ; try rewrite Hn0 ; go.
intro a.
unfold Carrying ; fold Carrying.
intro a ; unfold Carrying ; fold Carrying.
flatten ;
unfold ToFF ; fold ToFF ; rewrite <- IHl ;
rewrite <- Zplus_assoc_reverse ;
......@@ -197,6 +224,20 @@ rewrite residuteCarry ;
reflexivity.
Qed.
Lemma CarrynPreserveConst : forall m l a , a + ToFF l = ToFF (Carrying_n m a l).
Proof.
assert(Hn0: 2 ^ n * 0 = 0) by (symmetry ; apply Zmult_0_r_reverse).
induction m ; intros l a.
- simpl ; flatten ; try rewrite <- ToFF_add ; go.
- simpl ; flatten ; go ;
rewrite! ToFF_cons ;
rewrite <- IHm ;
rewrite <- Zplus_assoc_reverse ;
rewrite <- Zred_factor4 ;
rewrite <- Zplus_assoc_reverse ;
rewrite residuteCarry ; go.
Qed.
Corollary CarryPreserve : forall l, ToFF l = ToFF (Carrying 0 l).
Proof.
intros.
......@@ -205,6 +246,16 @@ rewrite H ; clear H.
apply CarryPreserveConst.
Qed.
Corollary CarrynPreserve : forall m l, ToFF l = ToFF (Carrying_n m 0 l).
Proof.
intros.
assert(H: ToFF l = 0 + ToFF l) by go.
rewrite H ; clear H.
apply CarrynPreserveConst.
Qed.
Theorem ToFF_transitive: forall (f g:list Z -> list Z) f' g' l,
(forall l, ToFF (g l) = g' (ToFF l)) ->
(forall l, ToFF (f l) = f' (ToFF l )) ->
......@@ -248,4 +299,39 @@ rewrite ToFF_tail.
go.
Qed.
Lemma ToFF_slice_nth : forall l (m:nat), ToFF (slice m l) + 2^(n * . (length (slice m l))) * nth m l 0 = ToFF (slice (S m) l).
Proof.
induction l ; destruct m ; flatten ; simpl ; go.
- destruct l ; flatten ; simpl ; go ;
rewrite <-! Zmult_0_r_reverse ; ring.
- flatten.
+ simpl ; flatten ; simpl ; rewrite <-! Zmult_0_r_reverse ; try rewrite <- Zred_factor0 ; ring.
+ rewrite Zplus_assoc_reverse.
f_equal.
rewrite Zpos_P_of_succ_nat.
replace (n * Z.succ (. length (slice m (z :: l0)))) with (n + n * . length (slice m (z :: l0))) by ring.
rewrite Z.pow_add_r ; go.
rewrite Zmult_assoc_reverse.
rewrite Zred_factor4.
f_equal ; go.
Qed.
Lemma ToFF_slice_nth_tail : forall l (m:nat), ToFF (slice m l) + 2^(n * . (length (slice m l))) * nth m l 0 + 2^(n * . (length (slice (S m) l))) * ToFF (tail (S m) l) = ToFF l.
Proof.
Proof.
intros l m.
rewrite ToFF_slice_nth.
rewrite ToFF_slice_tail.
go.
Qed.
Lemma ToFF_app_null: forall l, ToFF l = ToFF (l ++ [0]).
Proof.
intro l.
rewrite ToFF_app.
simpl ; ring.
Qed.
End FiniteFied.
#include <stdio.h>
typedef long long i64;
typedef i64 gf[16];
#define BYTE_TO_BINARY_PATTERN "%c%c%c%c%c%c%c%c"
#define BYTE_TO_BINARY(byte) \
(byte & 0x80 ? '1' : '0'), \
(byte & 0x40 ? '1' : '0'), \
(byte & 0x20 ? '1' : '0'), \
(byte & 0x10 ? '1' : '0'), \
(byte & 0x08 ? '1' : '0'), \
(byte & 0x04 ? '1' : '0'), \
(byte & 0x02 ? '1' : '0'), \
(byte & 0x01 ? '1' : '0')
static void print_bin64(i64 val)
{
printf(" "BYTE_TO_BINARY_PATTERN" "BYTE_TO_BINARY_PATTERN" "BYTE_TO_BINARY_PATTERN" "BYTE_TO_BINARY_PATTERN,
BYTE_TO_BINARY(val>>56), BYTE_TO_BINARY(val>>48), BYTE_TO_BINARY(val>>40), BYTE_TO_BINARY(val >> 32));
printf(" "BYTE_TO_BINARY_PATTERN" "BYTE_TO_BINARY_PATTERN" "BYTE_TO_BINARY_PATTERN" "BYTE_TO_BINARY_PATTERN,
BYTE_TO_BINARY(val>>24), BYTE_TO_BINARY(val>>16), BYTE_TO_BINARY(val>>8), BYTE_TO_BINARY(val));
printf("\n");
}
static void car25519(gf o)
{
int i;
i64 c;
for (i = 0;i < 16;++i) {
o[i]+=(1LL<<16);
c=o[i]>>16;
o[(i+1)*(i<15)]+=c-1+37*(c-1)*(i==15);
o[i]-=c<<16;
// added to have a look at what is going on in there
printf("%2i : ---------------------------------------------\n",i);
for (int j = 0; j < 16; ++j)
{
printf("%2i: ", j);
print_bin64(o[j]);
}
}
}
int main(int argc, char const *argv[])
{
gf o;
i64 val = 1;
i64 val2 = 1;
for (int i = 0; i < 15; ++i)
// for (int i = 0; i < 61; ++i)
{
val |= val << 1;
}
for (int i = 0; i < 16; ++i)
{
o[i] = val;
}
o[15] = val | (val << 32);
for (int i = 0; i < 16; ++i)
{
printf("%2i: ", i);
print_bin64(o[i]);
}
printf("carry 1\n");
car25519(o);
printf("reult carry 1:__________________________________________\n");
for (int i = 0; i < 16; ++i)
{
printf("%2i: ", i);
print_bin64(o[i]);
}
printf("carry 2\n");
car25519(o);
printf("reult carry 2:__________________________________________\n");
for (int i = 0; i < 16; ++i)
{
printf("%2i: ", i);
print_bin64(o[i]);
}
return 0;
}
Supports Markdown
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