Commit 6378c44b authored by Benoit Viguier's avatar Benoit Viguier
Browse files

proof a full Car25519 correctness

parent 5368de2a
Require Export A.
Require Export Reduce.
Import ListNotations.
Require Import Coq.Init.Datatypes.
Section FiniteFied.
......@@ -78,7 +79,7 @@ simpl.
flatten.
Qed.
Lemma Carrying_n_length: forall l (m:nat) a, m = length l -> Carrying_n m a l = Carrying a l.
Lemma Carrying_n_eq: 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.
......@@ -88,6 +89,12 @@ inversion Hm.
flatten ; f_equal ; go.
Qed.
Lemma Carrying_n_length: forall l (m:nat) a, (m < length l)%nat -> length (Carrying_n m a l) = length l.
Proof.
induction l as [|h q IHl]; intros [] a Hm; simpl ; flatten ; go.
Qed.
Lemma CarryPreserveConst : forall l a , a + ToFF n l = ToFF n (Carrying a l).
Proof.
induction l as [| h q IHl].
......@@ -139,7 +146,7 @@ Definition backCarry (l:list Z) : (list Z) :=
(h + 38 * getCarry 16 v) :: slice 14 q ++ [getResidute 16 v]
end.
Lemma backCarry_ToFF : forall l, (length l <= 16)%nat -> ToFF 16 l :𝓟 = (ToFF 16 (backCarry l) :𝓟).
Lemma backCarry_ToFF_25519 : forall l, (length l <= 16)%nat -> ToFF 16 l :𝓟 = (ToFF 16 (backCarry l) :𝓟).
Proof.
destruct l as [| h l]; intro Hlength.
- go.
......@@ -237,3 +244,20 @@ destruct l as [| h l]; intro Hlength.
inversion H.
Qed.
Definition car25519 (l:list Z) : list Z := backCarry (Carrying_n 16 14 0 l).
Lemma car25519_ToFF_25519 : forall l, (length l = 16)%nat -> ToFF 16 l :𝓟 = (ToFF 16 (car25519 l) :𝓟).
Proof.
intros l Hlength.
unfold car25519.
erewrite <- backCarry_ToFF_25519.
rewrite <- CarrynPreserve.
go.
go.
rewrite Carrying_n_length ; go.
Qed.
(* Yes I'm kinda cheating by fixing the length to 16 ! but it is still correct if
you were to compare to the tweetnacl implementation*)
......@@ -145,9 +145,10 @@ rewrite ToFF_app.
simpl ; ring.
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 )) ->
Theorem ToFF_transitive: forall (f g:list Z -> list Z) f' g' l l',
ToFF (g l) = g' (ToFF l) ->
ToFF (f l') = f' (ToFF l') ->
g l = l' ->
ToFF (f (g l)) = f' (g' (ToFF l)).
Proof.
go.
......
......@@ -7,7 +7,7 @@ all:
@echo generating tools and libs
${COQ} Tools.v
${COQ} notations.v
${COQ} reduce.v
${COQ} Reduce.v
${COQ} ToFF.v
${COQ} SumList.v
${COQ} ScalarMult.v
......
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