Commit ae94c40a authored by Benoit Viguier's avatar Benoit Viguier
Browse files

fix more proof

parent 7067f229
......@@ -38,7 +38,7 @@ Lemma CSM_Eq : forall (n p:list Z),
Zlength p = 32 ->
Forall (fun x => 0 <= x /\ x < 2 ^ 8) n ->
Forall (fun x => 0 <= x /\ x < 2 ^ 8) p ->
ZofList 8 (Crypto_Scalarmult n p) = val (curve25519_Fp_ladder (Z.to_nat (Zclamp (ZofList 8 n))) (Zmodp.pi (modP (ZUnpack25519 (ZofList 8 p))))).
ZofList 8 (Crypto_Scalarmult n p) = val (curve25519_Fp_ladder (Z.to_nat (Zclamp (ZofList 8 n))) (Zmodp.pi (ZUnpack25519 (ZofList 8 p)))).
Proof.
move => n p Hln Hlp HBn HBp.
rewrite -ZCrypto_Scalarmult_curve25519_ladder.
......@@ -74,7 +74,7 @@ rewrite expn_pown.
by move/ltP.
Qed.
Local Notation "'Fp2_x' P" := (Zmodp2.Zmodp2 (Zmodp.pi (modP P)) 0) (at level 30).
Local Notation "'Fp2_x' P" := (Zmodp2.Zmodp2 (Zmodp.pi P) 0) (at level 30).
Local Notation "P '_x0'" := (val ((P )#x0 /p)) (at level 30).
Theorem Crypto_Scalarmult_Correct: forall (n p:list Z) (P:mc curve25519_Fp2_mcuType),
......
......@@ -55,7 +55,7 @@ Proof.
reflexivity.
Qed.
Lemma ZCrypto_Scalarmult_curve25519_ladder n x :
Lemma ZCrypto_Scalarmult_curve25519_ladder_ n x :
ZCrypto_Scalarmult n x = val (curve25519_Fp_ladder (Z.to_nat (Zclamp n)) (Zmodp.pi (modP (ZUnpack25519 x)))).
Proof.
assert (Hn:= Zclamp_min n).
......@@ -146,4 +146,15 @@ f_equal.
}
Qed.
Lemma ZCrypto_Scalarmult_curve25519_ladder n x :
ZCrypto_Scalarmult n x = val (curve25519_Fp_ladder (Z.to_nat (Zclamp n)) (Zmodp.pi (ZUnpack25519 x))).
Proof.
replace (Zmodp.pi (ZUnpack25519 x)) with (Zmodp.pi (modP (ZUnpack25519 x))).
apply ZCrypto_Scalarmult_curve25519_ladder_.
apply val_inj => /=.
rewrite /p -lock /=.
rewrite /modP.
apply Zmod_mod.
Qed.
Close Scope Z.
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