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

merge Group.Scalarmult into MontgomeryLadder, use in x25519_base #1843

Merged
merged 1 commit into from
Apr 1, 2024
Merged

merge Group.Scalarmult into MontgomeryLadder, use in x25519_base #1843

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
14 changes: 3 additions & 11 deletions src/Bedrock/End2End/X25519/Field25519.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
Require Import Crypto.Spec.Curve25519.
Require Import Coq.Strings.String. Local Open Scope string_scope.
Require Import Coq.Lists.List.
Require Import Coq.ZArith.ZArith.
Expand Down Expand Up @@ -38,17 +39,8 @@ Section Field.
Instance translation_parameters_ok : Types.ok.
Proof using ext_spec_ok. constructor; try exact _; apply prefix_name_gen_unique. Qed.

(* Define Curve25519 field *)
Instance field_parameters : FieldParameters.
Proof using Type.
let M := (eval vm_compute in (Z.to_pos (UnsaturatedSolinas.m s c))) in
(* curve 'A' parameter *)
let a := constr:(F.of_Z M 486662) in
let prefix := constr:("fe25519_"%string) in
eapply
(field_parameters_prefixed
M ((a - F.of_Z _ 2) / F.of_Z _ 4)%F prefix).
Defined.
Instance field_parameters : FieldParameters :=
field_parameters_prefixed Curve25519.p Curve25519.M.a24 "fe25519_"%string.

(* Call fiat-crypto pipeline on all field operations *)
Instance fe25519_ops : unsaturated_solinas_ops (ext_spec:=ext_spec) n s c.
Expand Down
25 changes: 20 additions & 5 deletions src/Bedrock/End2End/X25519/GarageDoor.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,10 +40,25 @@ Local Open Scope string_scope.
Import Syntax Syntax.Coercions NotationsCustomEntry.
Import ListNotations.
Import Coq.Init.Byte.
Import Tuple LittleEndianList.
Local Coercion F.to_Z : F >-> Z.

Definition garageowner : list byte :=
[x7b; x06; x18; x0c; x54; x0c; xca; x9f; xa3; x16; x0b; x2f; x2b; x69; x89; x63; x77; x4c; xc1; xef; xdc; x04; x91; x46; x76; x8b; xb2; xbf; x43; x0e; x34; x34].

Definition garageowner_P : Curve25519.M.point.
refine (
let x := F.of_Z _ (le_combine garageowner) in
let y2 := (x*x*x + Curve25519.M.a*x*x +x)%F in
let sqrtm1 := (F.pow (F.of_Z _ 2) ((N.pos p-1)/4)) in
let y := F.sqrt_5mod8 sqrtm1 y2 in
exist _ (inl (x, y)) _).
Decidable.vm_decide.
Defined.

Lemma garageowner_P_correct : le_split 32 (Curve25519.M.X0 garageowner_P) = garageowner.
Proof. vm_compute. reflexivity. Qed.

Local Notation ST := 0x80000000.
Local Notation PK := 0x80000040.
Local Notation BUF:= 0x80000060.
Expand Down Expand Up @@ -164,7 +179,6 @@ Qed.

Local Open Scope list_scope.
Require Crypto.Bedrock.End2End.RupicolaCrypto.Spec.
Import Tuple LittleEndianList.
Local Definition be2 z := rev (le_split 2 z).
Local Coercion to_list : tuple >-> list.
Local Coercion Z.b2z : bool >-> Z.
Expand Down Expand Up @@ -200,7 +214,7 @@ Definition garagedoor_iteration : state -> list (lightbulb_spec.OP _) -> state -
(TracePredicate.one ("st", lightbulb_spec.GPIO_DATA_ADDR _, action))) ioh
/\ (
let m := firstn 16 garagedoor_payload in
let v := le_split 32 (F.to_Z (x25519_gallina (le_combine sk) (Field.feval_bytes(FieldRepresentation:=frep25519) garageowner))) in
let v := le_split 32 (M.X0 (Curve25519.M.scalarmult (le_combine sk mod 2^255) garageowner_P)) in
exists set0 set1 : Naive.word32,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does plain M refer to the same M as Curve25519.M? For readability, it would be good to be consistent within this line about how fully-qualified the names are.

Copy link
Contributor Author

@andres-erbsen andres-erbsen Apr 1, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

👍 ; the two are definitionally equal anyway. I intend to do another spec-cleanup pass anyway.

(word.unsigned set0 = 1 <-> firstn 16 v = m) /\
(word.unsigned set1 = 1 <-> skipn 16 v = m) /\
Expand All @@ -220,7 +234,7 @@ Definition garagedoor_iteration : state -> list (lightbulb_spec.OP _) -> state -
udp_local ++ udp_remote ++
be2 udp_length ++ be2 0 ++
garagedoor_header ++
le_split 32 (F.to_Z (x25519_gallina (le_combine sk) (F.of_Z _ 9)))))
le_split 32 (M.X0 (Curve25519.M.scalarmult (le_combine sk mod 2^255) Curve25519.M.B))))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

memrep below guarantees that sk is of length 32, so if you le_combine it, it should not be bigger than 2^256, but you have a mod 2^255, so what's going on with that one bit? Is this the intended spec? Or could you require in the pre and post of loopfn that this bit is 0? Or could it actually be 1? Would the scalar multiplication implementation really not work for scalars between 2^255 and 2^256?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, the ladder blatantly ignores that bit. There is no reason to use scalar this large, so this is a free fraction-1/256 speedup that has become a part of the spec. Currently the code does not actually clear this bit before calling the ladder, so memrep change would need a code change. (BoringSSL even sets that bit to have ladders that don't ignore it break in testing...).

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, so it looks like everything on this line is actually required. And it appears twice in almost the same form, so could you factor that out into a definition? Would be nice if the code snippet we'll show in the paper and on slides is actually literally what curious readers will find in the source. I could imagine one function taking a list of bytes representing a scalar and a highlevel Curve25519.M.point, and returning a curve point represented as a list of bytes, or two functions, one to convert from byte list to truncated scalar, and one converting from curve point to list of bytes. [end of gardening 🌷🌹🌻😉]

ioh /\ SEED=seed /\ SK=sk.

Local Instance spec_of_recvEthernet : spec_of "recvEthernet" := spec_of_recvEthernet.
Expand Down Expand Up @@ -363,6 +377,7 @@ Proof.
repeat straightline.
straightline_call; ssplit; try ecancel_assumption; try trivial; try ZnWords.
{ cbv. inversion 1. }
{ instantiate (1:=garageowner_P). Decidable.vm_decide. }

rename Lppp into Lihl; assert (List.length ppp = 40)%nat as Lppp by ZnWords.

Expand All @@ -387,7 +402,7 @@ Proof.
subst pPPP.
seprewrite_in_by (Array.bytearray_append cmp1) H33 SepAutoArray.listZnWords.

set (k := (Field.feval_bytes _)); remember (le_split 32 (F.to_Z (x25519_gallina (le_combine sk) k))) as vv; subst k.
remember (le_split 32 (M.X0 (Curve25519.M.scalarmult (le_combine sk mod 2^255) garageowner_P))) as vv.
repeat straightline.
pose proof (List.firstn_skipn 16 vv) as Hvv.
pose proof (@firstn_length_le _ vv 16 ltac:(subst vv; rewrite ?length_le_split; ZnWords)).
Expand Down Expand Up @@ -852,7 +867,7 @@ Optimize Proof. Optimize Heap.
{ rewrite ?app_length, ?length_le_split. SepAutoArray.listZnWords. }
{ ZnWords. }

pose proof length_le_split 32 (F.to_Z (x25519_gallina (le_combine sk) (F.of_Z _ 9))) as Hpkl.
pose proof length_le_split 32 (F.to_Z (M.X0 (Curve25519.M.scalarmult (le_combine sk mod 2^255) Curve25519.M.B))) as Hpkl.
seprewrite_in_by (fun xs ys=>@bytearray_address_merge _ _ _ _ _ xs ys buf) H37 SepAutoArray.listZnWords.
seprewrite_in_by (fun xs ys=>@bytearray_address_merge _ _ _ _ _ xs ys buf) H37 SepAutoArray.listZnWords.

Expand Down
1 change: 0 additions & 1 deletion src/Bedrock/End2End/X25519/GarageDoorTop.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,6 @@ Require Import bedrock2Examples.memswap.
Require Import bedrock2Examples.memconst.
Require Import Rupicola.Examples.Net.IPChecksum.IPChecksum.
Require Import Crypto.Bedrock.End2End.X25519.GarageDoor.
Require Import Crypto.Bedrock.End2End.X25519.MontgomeryLadderProperties.
Import Crypto.Bedrock.End2End.RupicolaCrypto.ChaCha20.
Local Open Scope string_scope.
Import Syntax Syntax.Coercions NotationsCustomEntry.
Expand Down
112 changes: 60 additions & 52 deletions src/Bedrock/End2End/X25519/MontgomeryLadder.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Spec.MontgomeryCurve.
Require Import Crypto.Spec.Curve25519.
Require Import bedrock2.Map.Separation.
Require Import bedrock2.Syntax.
Expand Down Expand Up @@ -53,25 +55,29 @@ Require Import coqutil.Map.OfListWord Coq.Init.Byte coqutil.Byte.
Import ProgramLogic.Coercions.
Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a").
Definition x25519_gallina K U : F (2^255-19) :=
@XZ.M.montladder _ F.zero F.one F.add F.sub F.mul F.inv (F.div (F.of_Z _ 486662 - F.of_Z _ 2) (F.of_Z _ 4))
(Z.to_nat (Z.log2 (Z.pos order))) (Z.testbit K) U.

Global Instance spec_of_x25519 : spec_of "x25519" :=
fnspec! "x25519" out sk pk / (o s p : list Byte.byte) (R : _ -> Prop),
fnspec! "x25519" out sk pk / (o s p : list Byte.byte) P (R : _ -> Prop),
{ requires t m := m =* s$@sk * p$@pk * o$@out * R /\
length s = 32%nat /\ length p = 32%nat /\ length o = 32%nat /\ byte.unsigned (nth 31 p x00) <= 0x7f;
length s = 32%nat /\ length p = 32%nat /\ length o = 32%nat /\
byte.unsigned (nth 31 p x00) <= 0x7f /\ Field.feval_bytes(field_parameters:=field_parameters) p = Curve25519.M.X0 P;
ensures t' m := t=t' /\ m=* s$@sk ⋆ p$@pk ⋆ R ⋆
(le_split 32 (x25519_gallina (le_combine s) (Field.feval_bytes p)))$@out }.
(le_split 32 (M.X0 (Curve25519.M.scalarmult (le_combine s mod 2^255) P))$@out) }.

Local Instance spec_of_fe25519_from_word : spec_of "fe25519_from_word" := Field.spec_of_from_word.
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)).
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).

Local Arguments word.rep : simpl never.
Local Arguments word.wrap : simpl never.
Local Arguments word.unsigned : simpl never.
Local Arguments word.of_Z : simpl never.

Lemma x25519_ok : program_logic_goal_for_function! x25519.
Proof.
repeat straightline.
Expand All @@ -94,10 +100,10 @@ Proof.
eapply byte.unsigned_range. }
repeat straightline.

seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H15. { transitivity 40%nat; trivial. }
seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H16. { transitivity 40%nat; trivial. }

straightline_call; ssplit.
3: { unfold FElem, Field.FElem in *; extract_ex1_and_emp_in_goal; ssplit.
{ unfold FElem, Field.FElem in *; extract_ex1_and_emp_in_goal; ssplit.
{ use_sep_assumption. cancel; repeat ecancel_step.
cancel_seps_at_indices 0%nat 0%nat; trivial. cbn; reflexivity. }
all : eauto.
Expand All @@ -106,7 +112,7 @@ Proof.
{ rewrite H3. vm_compute. inversion 1. }
repeat straightline.

cbv [FElem] in H22. extract_ex1_and_emp_in H22.
specialize (H23 P ltac:(assumption)). cbv [FElem] in H23. extract_ex1_and_emp_in H23.
straightline_call; ssplit.
{ ecancel_assumption. }
{ transitivity 32%nat; auto. }
Expand All @@ -116,21 +122,20 @@ Proof.
repeat straightline.

cbv [Field.FElem] in *.
seprewrite_in @Bignum.Bignum_to_bytes H25.
seprewrite_in @Bignum.Bignum_to_bytes H25.
extract_ex1_and_emp_in H25.
seprewrite_in @Bignum.Bignum_to_bytes H26.
seprewrite_in @Bignum.Bignum_to_bytes H26.
extract_ex1_and_emp_in H26.

repeat straightline; intuition eauto.
rewrite H29 in *. cbv [x25519_gallina].
use_sep_assumption; cancel. eapply RelationClasses.reflexivity.
rewrite H30 in *.
use_sep_assumption; cancel. reflexivity.
Qed.

Global Instance spec_of_x25519_base : spec_of "x25519_base" :=
fnspec! "x25519_base" out sk / (o s : list Byte.byte) (R : _ -> Prop),
{ requires t m := m =* s$@sk * o$@out * R /\
length s = 32%nat /\ length o = 32%nat;
{ requires t m := m =* s$@sk * o$@out * R /\ length s = 32%nat /\ length o = 32%nat;
ensures t' m := t=t' /\ m=* s$@sk ⋆ R ⋆
(le_split 32 (x25519_gallina (le_combine s) (F.of_Z _ 9)))$@out }.
le_split 32 (M.X0 (Curve25519.M.scalarmult (le_combine s mod 2^255) Curve25519.M.B))$@out }.

Lemma x25519_base_ok : program_logic_goal_for_function! x25519_base.
Proof.
Expand All @@ -143,7 +148,7 @@ Proof.
seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H13. { transitivity 40%nat; trivial. }

straightline_call; ssplit.
3: { unfold FElem, Field.FElem in *; extract_ex1_and_emp_in_goal; ssplit.
{ unfold FElem, Field.FElem in *; extract_ex1_and_emp_in_goal; ssplit.
{ use_sep_assumption. cancel; repeat ecancel_step.
cancel_seps_at_indices 0%nat 0%nat; trivial. cbn; reflexivity. }
all : eauto.
Expand All @@ -152,6 +157,7 @@ Proof.
{ rewrite H3. vm_compute. inversion 1. }
repeat straightline.

specialize (H20 Curve25519.M.B eq_refl).
unfold FElem in H20. extract_ex1_and_emp_in H20.
straightline_call; ssplit.
{ ecancel_assumption. }
Expand All @@ -167,8 +173,8 @@ Proof.
extract_ex1_and_emp_in H23.

repeat straightline; intuition eauto.
rewrite H27 in *. cbv [x25519_gallina].
use_sep_assumption; cancel. eapply RelationClasses.reflexivity.
rewrite H27 in *.
use_sep_assumption; cancel. reflexivity.
Qed.

Require Import coqutil.Word.Naive.
Expand Down Expand Up @@ -196,36 +202,38 @@ Definition funcs :=
Require Import bedrock2.ToCString.
Definition montladder_c_module := list_byte_of_string (ToCString.c_module funcs).

#[export]
Instance BWM_RV32IM : FlatToRiscvCommon.bitwidth_iset 32 Decode.RV32IM := eq_refl.

Derive montladder_compiler_result SuchThat
(compile
(compile_ext_call (funname_env:=SortedListString.map))
funcs = Success montladder_compiler_result)
As montladder_compiler_result_ok.
Lemma link_montladder : spec_of_montladder (map.of_list funcs).
Proof.
match goal with x := _ |- _ => cbv delta [x]; clear x end.
match goal with |- ?a = _ => set a end.
vm_compute.
match goal with |- @Success ?A ?x = Success ?e => is_evar e;
exact (@eq_refl (result A) (@Success A x)) end.
unfold spec_of_montladder, ScalarMult.MontgomeryLadder.spec_of_montladder.
unfold funcs.
(* use montladder correctness proof *)
rewrite montladder_defn.
eapply @montladder_correct; try (typeclasses eauto).
{ 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. }
{ eapply fe25519_copy_correct. reflexivity. }
{ eapply fe25519_from_word_correct. reflexivity. }
{
cbv [LadderStep.spec_of_ladderstep]; intros.
rewrite ladderstep_defn.
eapply @LadderStep.ladderstep_correct; try (typeclasses eauto).
{ cbv [Core.__rupicola_program_marker]; tauto. }
{ reflexivity. }
{ apply fe25519_mul_correct. reflexivity. }
{ apply fe25519_add_correct. reflexivity. }
{ apply fe25519_sub_correct. reflexivity. }
{ apply fe25519_square_correct. reflexivity. }
{ apply fe25519_scmula24_correct. reflexivity. }
{ ecancel_assumption. } }
{ unshelve eapply AdditionChains.fe25519_inv_correct_exp; [exact I|reflexivity| | ].
{ apply fe25519_square_correct. reflexivity. }
{ apply fe25519_mul_correct. reflexivity. } }
{ apply fe25519_mul_correct. reflexivity. }
Qed.

Definition montladder_stack_size := snd montladder_compiler_result.
Definition montladder_finfo := snd (fst montladder_compiler_result).
Definition montladder_insns := fst (fst montladder_compiler_result).
Definition montladder_bytes := Pipeline.instrencode montladder_insns.
Definition montladder_symbols : list byte := Symbols.symbols montladder_finfo.


Require riscv.Utility.InstructionNotations.
Require riscv.Utility.InstructionCoercions.
Module PrintAssembly.
Import riscv.Utility.InstructionNotations.
Import riscv.Utility.InstructionCoercions.
Unset Printing Coercions.

(* Compute garagedoor_finfo. (* fe25519_mul is more than 10KB in just one function *) *)
Goal True. let r := eval cbv in montladder_insns in idtac (* r *). Abort.
End PrintAssembly.
Loading
Loading