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

proof that conversion between List and Z are equivalent (under conditions)

parent 53332014
From Tweetnacl Require Export ListsOp.ZofList. From Tweetnacl Require Export ListsOp.ZofList.
From Tweetnacl Require Export ListsOp.Forall_ZopList. From Tweetnacl Require Export ListsOp.Forall_ZopList.
From Tweetnacl Require Export ListsOp.ListofZ.
From Tweetnacl Require Export ListsOp.Zipp. From Tweetnacl Require Export ListsOp.Zipp.
From Tweetnacl Require Export ListsOp.Forall_ZopList. From Tweetnacl Require Export ListsOp.Forall_ZopList.
From Tweetnacl Require Export ListsOp.Forall_ZofList. From Tweetnacl Require Export ListsOp.Forall_ZofList.
......
Require Import stdpp.list.
Require Import ssreflect.
From Tweetnacl Require Import Libs.Export.
From Tweetnacl Require Import ListsOp.ZofList.
From Tweetnacl Require Import ListsOp.Forall_ZofList.
Open Scope Z.
Section Integer.
Variable n:Z.
Hypothesis Hn: n > 0.
Fixpoint ListofZn_fp (a:Z) (fuel:nat) : list Z :=
match fuel with
| 0%nat => []
| S fuel => (Z.modulo a (Z.pow 2 n)) :: ListofZn_fp (Z.div a (Z.pow 2 n)) fuel
end.
Definition ListofZ16 (a:Z) : list Z := ListofZn_fp a 16.
Lemma ListofZ16_length : forall (a:Z), length (ListofZ16 a) = 16%nat.
Proof. done. Qed.
Definition ListofZ32 (a:Z) : list Z := ListofZn_fp a 32.
Lemma ListofZ32_length : forall (a:Z), length (ListofZ32 a) = 32%nat.
Proof. done. Qed.
Local Lemma next_ : forall a b, 0 <= a /\ a < 2^n -> (a + 2 ^ n * b) `div` 2 ^ n = b.
Proof.
move => a b Ha.
have Hn':= pown0 n Hn.
rewrite Z.mul_comm.
orewrite Z_div_plus_full.
rewrite Zdiv_small => //.
Qed.
Lemma ListofZ16_ZofList_length: forall (l:list Z) (a:Z),
Forall (fun x => 0 <= x < 2^n) l ->
(length l = 16)%nat ->
ZofList n l = a ->
ListofZ16 a = l.
Proof.
move => l a Hlbound HlLength.
repeat (destruct l ; tryfalse).
repeat match goal with
| [ H: Forall _ _ |- _ ] => apply Forall_cons_1 in H ; destruct H
end.
rewrite /ListofZ16.
move => <-.
simpl.
repeat match goal with
| [ |- _ :: _ = _ :: _ ] => f_equal
| _ => rewrite next_ => //
| _ => rewrite Z.mul_comm Z_mod_plus_full
| _ => apply Z.mod_small => //
end.
Qed.
Lemma ListofZ32_ZofList_impl_length: forall (l:list Z) (a:Z),
Forall (fun x => 0 <= x < 2^n) l ->
(length l = 32)%nat ->
ZofList n l = a ->
ListofZ32 a = l.
Proof.
move => l a Hlbound HlLength.
repeat (destruct l ; tryfalse).
repeat match goal with
| [ H: Forall _ _ |- _ ] => apply Forall_cons_1 in H ; destruct H
end.
rewrite /ListofZ32.
move => <-.
simpl.
repeat match goal with
| [ |- _ :: _ = _ :: _ ] => f_equal
| _ => rewrite next_ => //
| _ => rewrite Z.mul_comm Z_mod_plus_full
| _ => apply Z.mod_small => //
end.
Qed.
Lemma ListofZ32_ZofList_length: forall (l:list Z),
Forall (fun x => 0 <= x < 2^n) l ->
(length l = 32)%nat ->
ListofZ32 (ZofList n l) = l.
Proof.
move => l Hl Hll.
apply ListofZ32_ZofList_impl_length => //.
Qed.
Lemma ListofZ32_ZofList_Zlength: forall (l:list Z),
Forall (fun x => 0 <= x < 2^n) l ->
Zlength l = 32 ->
ListofZ32 (ZofList n l) = l.
Proof. convert_length_to_Zlength ListofZ32_ZofList_length. Qed.
End Integer.
Close Scope Z.
...@@ -258,4 +258,27 @@ Proof. ...@@ -258,4 +258,27 @@ Proof.
apply get_c_abstract_fn_montgomery_fn => //. apply get_c_abstract_fn_montgomery_fn => //.
Qed. Qed.
Corollary Crypto_Scalarmult_Eq2 : forall (n p: list Z),
Zlength n = 32 ->
Zlength p = 32 ->
Forall (λ x : , 0 x x < 2 ^ 8) n ->
Forall (λ x : , 0 x x < 2 ^ 8) p ->
Crypto_Scalarmult n p = ListofZ32 8 (ZCrypto_Scalarmult (ZofList 8 n) (ZofList 8 p)).
Proof.
move => n p Hn Hp Hbn Hbp.
rewrite -Crypto_Scalarmult_Eq => //.
rewrite ListofZ32_ZofList_Zlength => //.
all: rewrite -Crypto_Scalarmult_eq.
all: rewrite /Crypto_Scalarmult_proof.
2: rewrite /Pack25519.
2: apply Pack.pack_for_Zlength_32_16.
2: apply Reduce_by_P.get_t_subst_select_Zlength => //=.
2: do 3 apply car25519_Zlength.
apply Pack25519_bound.
2: apply M_bounded ; assumption.
all: apply M_Zlength.
1,3: apply Zlength_a ; assumption.
all: apply Inv25519_Zlength ; apply Zlength_c ; assumption.
Qed.
Close Scope Z. Close Scope Z.
\ No newline at end of file
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