Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make the montladder proof short again. #1856

Closed
wants to merge 2 commits into from
Closed

Make the montladder proof short again. #1856

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d1920b9
checkpoint
jadephilipoom Apr 6, 2024
23360f2
done
jadephilipoom Apr 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 28 additions & 14 deletions src/Bedrock/End2End/X25519/MontgomeryLadder.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,10 +85,7 @@ Local Instance spec_of_fe25519_from_word : spec_of "fe25519_from_word" := Field.
Local Instance spec_of_fe25519_from_bytes : spec_of "fe25519_from_bytes" := Field.spec_of_from_bytes.
Local Instance spec_of_fe25519_to_bytes : spec_of "fe25519_to_bytes" := Field.spec_of_to_bytes.
Local Instance spec_of_montladder : spec_of "montladder" :=
spec_of_montladder
(Z.to_nat (Z.log2 Curve25519.order))
Crypto.Spec.Curve25519.field
Curve25519.M.a Curve25519.M.b Curve25519.M.b_nonzero (char_ge_3:=Curve25519.char_ge_3).
spec_of_montladder (Z.to_nat (Z.log2 Curve25519.order)).

Local Arguments word.rep : simpl never.
Local Arguments word.wrap : simpl never.
Expand Down Expand Up @@ -132,12 +129,22 @@ Proof.
{ reflexivity. }
{ rewrite ?length_le_split. vm_compute. inversion 1. }
repeat straightline.

specialize (H31 P ltac:(assumption)). cbv [FElem] in H31. extract_ex1_and_emp_in H31.
lazymatch goal with
| H : Field.feval_bytes ?x = M.X0 ?P, H' : context [montladder_gallina] |- _ =>
rewrite H in H'; unfold M.X0 in H'
end.
lazymatch goal with
| H : context [montladder_gallina] |- _ =>
rewrite (@montladder_gallina_equiv_affine (Curve25519.p) _ _ (Curve25519.field)) with
(b_nonzero:=Curve25519.M.b_nonzero) (char_ge_3:=Curve25519.char_ge_3) in H;
[ unfold FElem, Field.FElem in H; extract_ex1_and_emp_in H | Lia.lia | vm_decide | apply M.a2m4_nonsq ]
end.
straightline_call; ssplit.
{ ecancel_assumption. }
{ transitivity 32%nat; auto. }
{ eexists. ecancel_assumption. }
{ eexists.
unfold FElem, Field.FElem in *; extract_ex1_and_emp_in_goal; ssplit.
ecancel_assumption. }
{ intuition idtac. }
repeat straightline_cleanup.
repeat straightline.
Expand All @@ -154,7 +161,8 @@ Proof.
rewrite H38, le_combine_split.
do 7 Morphisms.f_equiv.
pose proof clamp_range (le_combine s).
(rewrite_strat bottomup Z.mod_small); change (Z.of_nat (Z.to_nat (Z.log2 (Z.pos order)))) with 255; try Lia.lia.
change (Z.of_nat (Z.to_nat (Z.log2 (Z.pos order)))) with 255.
(rewrite_strat bottomup Z.mod_small); [ reflexivity | .. ]; try Lia.lia.
Qed.

Lemma x25519_base_ok : program_logic_goal_for_function! x25519_base.
Expand All @@ -180,8 +188,6 @@ Proof.
{ reflexivity. }
{ rewrite length_le_split. vm_compute. inversion 1. }
repeat straightline.

specialize (H28 Curve25519.M.B eq_refl).
unfold FElem in H28. extract_ex1_and_emp_in H28.
straightline_call; ssplit.
{ ecancel_assumption. }
Expand All @@ -203,7 +209,18 @@ Proof.
rewrite H35, le_combine_split.
do 7 Morphisms.f_equiv.
pose proof clamp_range (le_combine s).
(rewrite_strat bottomup Z.mod_small); change (Z.of_nat (Z.to_nat (Z.log2 (Z.pos order)))) with 255; try Lia.lia.
change (Z.of_nat (Z.to_nat (Z.log2 (Z.pos order)))) with 255.
(rewrite_strat bottomup Z.mod_small); [ | Lia.lia .. ].
lazymatch goal with
| |- montladder_gallina _ _ _ ?x = _ => change x with (M.X0 M.B)
end.
unfold M.X0.
rewrite (@montladder_gallina_equiv_affine (Curve25519.p) _ _ (Curve25519.field)) with
(b_nonzero:=Curve25519.M.b_nonzero) (char_ge_3:=Curve25519.char_ge_3);
[ | Lia.lia | vm_decide | apply M.a2m4_nonsq ].
change (Z.of_nat (Z.to_nat (Z.log2 (Z.pos order)))) with 255.
(rewrite_strat bottomup Z.mod_small); [ | Lia.lia .. ].
reflexivity.
Qed.

Require Import coqutil.Word.Naive.
Expand Down Expand Up @@ -243,9 +260,6 @@ Proof.
{ reflexivity. }
{ Decidable.vm_decide. }
{ Decidable.vm_decide. }
{ Decidable.vm_decide. }
{ eapply M.a2m4_nonsq. }
{ exact I. }
{ reflexivity. }
{ eapply CSwap.cswap_body_correct; [|exact I|reflexivity].
unfold field_representation, Signature.field_representation, Representation.frep; cbn; unfold n; cbv; trivial. }
Expand Down
24 changes: 4 additions & 20 deletions src/Bedrock/Group/ScalarMult/MontgomeryLadder.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -198,8 +198,7 @@ Section __.
Z.of_nat scalarbits <= 8*Z.of_nat (length Kbytes);
ensures tr' mem' :=
tr' = tr /\ (
forall P, U = MontgomeryCurve.M.X0 (Fzero:=F.zero) P ->
let OUT := MontgomeryCurve.M.X0 (Fzero:=F.zero) (scalarmult (K mod 2^Z.of_nat scalarbits) P) in
let OUT := montladder_gallina a24 scalarbits K U in
(FElem (Some tight_bounds) pOUT OUT * Kbytes$@pK
* FElem (Some tight_bounds) pU U
* R)%sep mem') }.
Expand Down Expand Up @@ -404,6 +403,8 @@ Section __.
Hint Extern 1 (spec_of "fe25519_inv") => (simple refine (spec_of_exp_large)) : typeclass_instances.
Hint Extern 1 (spec_of "felem_cswap") => (simple refine (spec_of_cswap)) : typeclass_instances.

Hint Extern 1 => simple eapply compile_felem_cswap; shelve : compiler.
Local Hint Extern 10 => lia : compiler_side_conditions.
Derive montladder_body SuchThat
(defn! "montladder" ("OUT", "K", "U")
{ montladder_body },
Expand All @@ -413,24 +414,7 @@ Section __.
As montladder_correct.
Proof.
pose proof scalarbits_bound.
cbv [spec_of_montladder]; intros; eapply Semantics.weaken_call with
(post1:=fun t' m' rets => rets = [] /\ t' = tr /\
((FElem (Some tight_bounds) pOUT (montladder_gallina a24 scalarbits K U)
⋆ Kbytes $@ pK ⋆ FElem (Some tight_bounds) pU U ⋆ R) m')); cycle 1; intros.
{ DestructHead.destruct_head and; Tactics.ssplit; trivial; intros.
pose proof LittleEndianList.le_combine_bound Kbytes. subst U.
erewrite montladder_gallina_equiv_affine in *; eauto; try lia. }

compile_setup.
repeat compile_step; shelve_unifiable.
eapply compile_nlet_as_nlet_eq.
eapply compile_felem_cswap; repeat compile_step.

eapply compile_nlet_as_nlet_eq.
eapply compile_felem_cswap; repeat compile_step.

lia. (* m = 2^255-19 *)
compile_step.
compile.
Qed.

End MontLadder.
Expand Down
Loading