Commit 0076f329 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

WIP

parent e0f1a70f
......@@ -22,6 +22,8 @@ _CoqProject
*#
.#*
*.aux
graph.dpd
graph.png
*.bck
*.bak
......
......@@ -51,7 +51,7 @@ Section OptimizedLadder.
Lemma opt_montgomery_rec_equiv:
forall m n x a b c d,
opt_montgomery_rec M n m x a b c d = get_a (opt_montgomery_rec_extr n m x a b c d) / get_c (opt_montgomery_rec_extr n m x a b c d).
opt_montgomery_rec M n m x a b c d = get_a (opt_montgomery_rec_extr n m x a b c d) * (get_c (opt_montgomery_rec_extr n m x a b c d))^-1.
Proof.
elim => [|m IHm] n x a b c d //=.
by do! case: (cswap _ _ _) => *.
......
......@@ -10,10 +10,7 @@ From Tweetnacl.Gen Require Import ABCDEF.
From Tweetnacl.Gen Require Import abstract_fn_rev.
From Tweetnacl.Gen Require Import abstract_fn_rev_eq.
From Tweetnacl.Gen Require Import abstract_fn_rev_abcdef.
(* From Tweetnacl.Low Require Import A. *)
(* From Tweetnacl.Low Require Import Z. *)
From Tweetnacl.Low Require Import M.
(* From Tweetnacl.Low Require Import S. *)
From Tweetnacl.Low Require Import Pack25519.
From Tweetnacl.Low Require Import Unpack25519.
From Tweetnacl.Low Require Import Inv25519.
......@@ -98,7 +95,7 @@ Definition Crypto_Scalarmult n p :=
let c := get_c (montgomery_fn List_Z_Ops 255 254 (clamp n) One16 (Unpack25519 p) nul16 One16 nul16 nul16 (Unpack25519 p)) in
Pack25519 (M.M a (Inv25519 c)).
Lemma impl_omega_simpl_0 : x : , (λ x0 : , 0 x0 x0 < 2 ^ 16) x -38 x x < 2 ^ 16 + 38.
Local Lemma impl_omega_simpl_0 : x : , (λ x0 : , 0 x0 x0 < 2 ^ 16) x -38 x x < 2 ^ 16 + 38.
Proof.
intros ; simpl in *.
change (2^16 + 38) with 65574.
......@@ -106,7 +103,7 @@ Proof.
omega.
Qed.
Lemma impl_omega_simpl_1 : x : , (λ x0 : , -38 x0 x0 < 2 ^ 16 + 38) x - 2 ^ 26 < x x < 2 ^ 26.
Local Lemma impl_omega_simpl_1 : x : , (λ x0 : , -38 x0 x0 < 2 ^ 16 + 38) x - 2 ^ 26 < x x < 2 ^ 26.
Proof.
intros ; simpl in *.
change (2^16 + 38) with 65574 in H.
......@@ -114,7 +111,7 @@ Proof.
omega.
Qed.
Lemma impl_omega_simpl_2 : x : , (λ x0 : , -38 x0 x0 < 2 ^ 16 + 38) x - 2 ^ 62 < x x < 2 ^ 62.
Local Lemma impl_omega_simpl_2 : x : , (λ x0 : , -38 x0 x0 < 2 ^ 16 + 38) x - 2 ^ 62 < x x < 2 ^ 62.
Proof.
intros ; simpl in *.
change (2^16 + 38) with 65574 in H.
......
......@@ -4,3 +4,17 @@ clean::
$(HIDE)rm */.*.aux 2> /dev/null || true
$(HIDE)rm */*.glob 2> /dev/null || true
$(HIDE)rm */*.v.d 2> /dev/null || true
$(HIDE)rm graph.dpd 2> /dev/null || true
$(HIDE)rm graph.png 2> /dev/null || true
DPD = $(wildcard *.dpd)
DOT = $(DPD:%.dpd=%.dot)
PNG = $(DPD:%.dpd=%.png)
%.dot: %.dpd
dpd2dot $<
%.png: %.dot
dot -Tpng $< -o $@
graph: $(PNG)
......@@ -138,22 +138,26 @@ rewrite /Mod /Sel25519 ; flatten.
intros; simpl.
apply Zgetbit_bitn.
Defined.
(*
Lemma ZCrypto_Scalarmult_curve25519_ladder n x : (*(x : Zmodp.type) :*)
ZCrypto_Scalarmult n x = val (curve25519_ladder (Z.to_nat (Zclamp n)) (Zmodp.pi x)).
(* TODO : move this *)
Local Lemma Zunpack: forall x, 0 <= x < 2^255 - 19 -> 0 <= ZUnpack25519 x < 2 ^ 255 - 19.
Proof.
(* rewrite *)
(* get_a (Zmontgomery_rec 255 (Zclamp n) 1 (ZUnpack25519 x) 0 1 0 0 (ZUnpack25519 x)) :𝓖𝓕 *
((get_c (Zmontgomery_rec 255 (Zclamp n) 1 (ZUnpack25519 x) 0 1 0 0 (ZUnpack25519 x)) :𝓖𝓕) ^ (2 ^ 255 - 21) :𝓖𝓕) :𝓖𝓕
move => x Hx.
rewrite /ZUnpack25519.
rewrite Z.land_ones //=.
rewrite Zmod_small //=.
split ; omega.
Qed.
Lemma ZCrypto_Scalarmult_curve25519_ladder n x : (*(x : Zmodp.type) :*)
ZCrypto_Scalarmult n x = val (curve25519_ladder (Z.to_nat (Zclamp n)) (Zmodp.pi x)).
*)
Lemma ZCrypto_Scalarmult_curve25519_ladder n x :
0 <= x < 2 ^ 255 - 19 ->
0 <= Zclamp n ->
ZCrypto_Scalarmult n x = val (curve25519_ladder (Z.to_nat (Zclamp n)) (Zmodp.pi (ZUnpack25519 x))).
Proof.
intros Hx Hn.
assert(Hxx:= Zunpack x Hx).
rewrite /ZCrypto_Scalarmult.
rewrite -Fp_Crypto_Scalarmult_rec_gen_equiv.
(* rewrite /curve25519_ladder. *)
(* rewrite /opt_montgomery. *)
(* rewrite /ZCrypto_Scalarmult_rev_gen. *)
rewrite /ZPack25519.
rewrite /ZInv25519.
rewrite Zmult_mod.
......@@ -163,24 +167,69 @@ rewrite /Zmontgomery_rec.
rewrite /Fp_Crypto_Scalarmult_rec_gen.
rewrite /val /Zmodp_subType.
rewrite -modZp /p -lock.
SearchAbout "/".
SearchAbout Zmodp.repr.
assert(case: (boolP (b == 0)) => [/eqP|] Hb)
SearchAbout div.
SearchAbout Znumtheory.rel_prime Znumtheory.prime.
assert(Znumtheory.prime (2 ^ 255 - 19)).
apply primo.
Check Znumtheory.rel_prime_le_prime.
Check Zp.Zorder_power_is_1.
SearchAbout Zp.Zorder.
SearchAbout Z.divide.
SearchAbout "^-1".
GRing.mulr1_eq.
SearchAbout Znumtheory.prime.
SearchAbout Zp.Zorder.
SearchAbout Z.div Z.pow.
remember (get_a
(montgomery_rec 255 (Z.to_nat (Zclamp n)) Zmodp.one (Zmodp.pi (ZUnpack25519 x)) Zmodp.zero Zmodp.one Zmodp.zero
Zmodp.zero (Zmodp.pi (ZUnpack25519 x)))) as GETA.
remember (get_c
(montgomery_rec 255 (Z.to_nat (Zclamp n)) Zmodp.one (Zmodp.pi (ZUnpack25519 x)) Zmodp.zero Zmodp.one Zmodp.zero
Zmodp.zero (Zmodp.pi (ZUnpack25519 x)))) as GETC.
assert(Mequiv:= M_eq GETA (GETC ^-1)).
cbn in Mequiv.
remember (Zmodp.repr (GETA / GETC)%R :𝓖𝓕) as HM.
cbn in HeqHM.
rewrite Mequiv in HeqHM.
rewrite /M in HeqHM.
do 2 rewrite -Zcar25519_correct in HeqHM.
clear Mequiv.
rewrite Zmult_mod in HeqHM.
rewrite HeqHM.
f_equal.
f_equal.
- {
subst.
change 255%nat with (S (Z.to_nat 254)).
rewrite ?montgomery_rec_eq_fn_rev.
2,3: done.
assert(H255: 0 <= 254 + 1).
by compute.
assert(Hxxx: val (Zmodp.pi (ZUnpack25519 x)) = (ZUnpack25519 x)).
simpl; apply Z.mod_small; rewrite /p -lock //=.
assert(Hnn: . Z.to_nat (Zclamp n) = Zclamp n).
rewrite Z2Nat.id //.
assert(Habstr:= abstract_fn_rev_eq_a_Fp (254 + 1) 254 (Z.to_nat (Zclamp n)) (Zmodp.pi (ZUnpack25519 x)) (Zclamp n) (ZUnpack25519 x) H255 Hxxx Hnn).
rewrite /Mod in Habstr.
rewrite /P in Habstr.
rewrite /Crypto_Scalarmult_Fp.Z25519_Z_Eq in Habstr.
rewrite /val in Habstr.
rewrite /Zmodp_subType in Habstr.
symmetry.
assumption.
}
- {
subst.
change 255%nat with (S (Z.to_nat 254)).
rewrite ?montgomery_rec_eq_fn_rev.
2,3: done.
assert(H255: 0 <= 254 + 1).
by compute.
assert(Hxxx: val (Zmodp.pi (ZUnpack25519 x)) = (ZUnpack25519 x)).
simpl; apply Z.mod_small; rewrite /p -lock //=.
assert(Hnn: . Z.to_nat (Zclamp n) = Zclamp n).
rewrite Z2Nat.id //.
assert(Habstr:= abstract_fn_rev_eq_c_Fp (254 + 1) 254 (Z.to_nat (Zclamp n)) (Zmodp.pi (ZUnpack25519 x)) (Zclamp n) (ZUnpack25519 x) H255 Hxxx Hnn).
rewrite /Mod in Habstr.
rewrite /P in Habstr.
rewrite /Crypto_Scalarmult_Fp.Z25519_Z_Eq in Habstr.
rewrite /val in Habstr.
rewrite /Zmodp_subType in Habstr.
symmetry.
rewrite -Habstr.
remember (get_c
(abstract_fn_rev (254 + 1) 254 (Z.to_nat (Zclamp n)) Zmodp.one (Zmodp.pi (ZUnpack25519 x))
Zmodp.zero Zmodp.one Zmodp.zero Zmodp.zero (Zmodp.pi (ZUnpack25519 x)))) as GETC.
clear.
admit.
}
Admitted.
*)
Close Scope Z.
......@@ -87,7 +87,7 @@ Defined.
Definition Fp_Crypto_Scalarmult_rec_gen n p :=
let t := montgomery_rec.montgomery_rec 255 n Zmodp.one p Zmodp.zero Zmodp.one Zmodp.zero Zmodp.zero p in
(get_a t) / (get_c t).
(get_a t) * (get_c t)^-1.
Local Lemma v4inv : Zmodp.repr 4%:R^-1 = 43422033463993573283839119378257965444976244249615211514796594002967423614962.
Proof.
......
#!/usr/bin/env python3
import os
def save(fn, z):
d = open(fn, 'w', encoding="utf-8")
d.write(z)
d.close()
def main():
# MAIN
list_parse = []
dirs = ['Gen', 'Libs', 'ListsOp', 'Low', 'Mid']
for dir in dirs:
coqfiles = os.listdir(dir)
for coqfile in coqfiles:
if coqfile[-2:] == '.v':
list_parse.append(dir + '.' + coqfile[:-2])
requires = ''
prints = 'Print FileDependGraph \n'
for cq in list_parse:
requires += 'Require Import Tweetnacl.'+ cq + '.\n'
prints += '\t' + cq + '\n'
output = requires + '\n'
output += 'Require dpdgraph.dpdgraph.\n'
output += 'Set DependGraph File "graph.dpd".\n'
output += prints + '.\n'
# print(list_parse)
print(output)
save('gen_graph_main.v', output)
# High
list_parse = []
dirs = ['High']
for dir in dirs:
coqfiles = os.listdir(dir)
for coqfile in coqfiles:
if coqfile[-2:] == '.v':
list_parse.append(dir + '.' + coqfile[:-2])
requires = ''
prints = 'Print FileDependGraph \n'
for cq in list_parse:
requires += 'Require Import Tweetnacl.'+ cq + '.\n'
prints += '\t' + cq + '\n'
output = requires + '\n'
output += 'Require dpdgraph.dpdgraph.\n'
output += 'Set DependGraph File "graph.dpd".\n'
output += prints + '.\n'
# print(list_parse)
print(output)
save('gen_graph_high.v', output)
if __name__ == '__main__':
main()
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