From 9b5f833346c4dd62e1792ea4112b5dc03bd366ed Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 2 Apr 2024 04:33:24 -0400 Subject: [PATCH] implement and prove Curve25519 scalar clamping (#1845) --- src/Bedrock/End2End/X25519/GarageDoor.v | 25 +-- src/Bedrock/End2End/X25519/GarageDoorTop.v | 2 + src/Bedrock/End2End/X25519/MontgomeryLadder.v | 97 +++++++---- src/Bedrock/End2End/X25519/clamp.v | 152 ++++++++++++++++++ src/Spec/Curve25519.v | 2 + 5 files changed, 227 insertions(+), 51 deletions(-) create mode 100644 src/Bedrock/End2End/X25519/clamp.v diff --git a/src/Bedrock/End2End/X25519/GarageDoor.v b/src/Bedrock/End2End/X25519/GarageDoor.v index a77054bdef..b1161ab8ec 100644 --- a/src/Bedrock/End2End/X25519/GarageDoor.v +++ b/src/Bedrock/End2End/X25519/GarageDoor.v @@ -23,18 +23,7 @@ Require Import bedrock2Examples.memequal. Require Import bedrock2Examples.memswap. Require Import bedrock2Examples.memconst. Require Import Rupicola.Examples.Net.IPChecksum.IPChecksum. - -(******) - Require Crypto.Bedrock.End2End.RupicolaCrypto.ChaCha20. -(* -Require bedrock2.BasicC32Semantics. -Goal bedrock2.BasicC32Semantics.ext_spec = bedrock2.FE310CSemantics.ext_spec. - reflexivity. - cbn. -Require bedrock2.FE310CSemantics*) - -(******) Local Open Scope string_scope. Import Syntax Syntax.Coercions NotationsCustomEntry. @@ -214,7 +203,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 (M.X0 (Curve25519.M.scalarmult (le_combine sk mod 2^255) garageowner_P)) in + let v := x25519_spec sk garageowner_P in exists set0 set1 : Naive.word32, (word.unsigned set0 = 1 <-> firstn 16 v = m) /\ (word.unsigned set1 = 1 <-> skipn 16 v = m) /\ @@ -234,7 +223,7 @@ Definition garagedoor_iteration : state -> list (lightbulb_spec.OP _) -> state - udp_local ++ udp_remote ++ be2 udp_length ++ be2 0 ++ garagedoor_header ++ - le_split 32 (M.X0 (Curve25519.M.scalarmult (le_combine sk mod 2^255) Curve25519.M.B)))) + x25519_spec sk Curve25519.M.B)) ioh /\ SEED=seed /\ SK=sk. Local Instance spec_of_recvEthernet : spec_of "recvEthernet" := spec_of_recvEthernet. @@ -402,16 +391,16 @@ Proof. subst pPPP. seprewrite_in_by (Array.bytearray_append cmp1) H33 SepAutoArray.listZnWords. - remember (le_split 32 (M.X0 (Curve25519.M.scalarmult (le_combine sk mod 2^255) garageowner_P))) as vv. + remember (x25519_spec sk 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)). + pose proof (@firstn_length_le _ vv 16 ltac:(subst vv; rewrite length_x25519_spec; ZnWords)). pose proof skipn_length 16 vv. forget (List.firstn 16 vv) as vv0. forget (List.skipn 16 vv) as vv1. subst vv. rewrite <-Hvv in H33. - rewrite length_le_split in *. + rewrite length_x25519_spec in *. seprewrite_in_by (Array.bytearray_append vv0) H33 SepAutoArray.listZnWords. repeat straightline. @@ -864,10 +853,10 @@ Optimize Proof. Optimize Heap. progress rewrite ?word.unsigned_sru_nowrap, ?word.unsigned_of_Z_nowrap in H37 by ZnWords. straightline_call; [ssplit; cycle -1|]; try ecancel_assumption. - { rewrite ?app_length, ?length_le_split. SepAutoArray.listZnWords. } + { rewrite ?app_length, ?length_x25519_spec. SepAutoArray.listZnWords. } { ZnWords. } - 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. + pose proof length_x25519_spec sk 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. diff --git a/src/Bedrock/End2End/X25519/GarageDoorTop.v b/src/Bedrock/End2End/X25519/GarageDoorTop.v index 5d27632c9b..d53d4b3269 100644 --- a/src/Bedrock/End2End/X25519/GarageDoorTop.v +++ b/src/Bedrock/End2End/X25519/GarageDoorTop.v @@ -93,6 +93,8 @@ Proof. pose_correctness spi_write_ok. pose_correctness spi_read_ok. pose_correctness (ip_checksum_br2fn_ok I). + pose_correctness memmove.memmove_ok_array. + pose_correctness clamp.clamp_correct. pose_correctness x25519_base_ok. pose_correctness fe25519_from_word_correct. pose_correctness fe25519_to_bytes_correct. diff --git a/src/Bedrock/End2End/X25519/MontgomeryLadder.v b/src/Bedrock/End2End/X25519/MontgomeryLadder.v index fcf467ee29..ed73654c57 100644 --- a/src/Bedrock/End2End/X25519/MontgomeryLadder.v +++ b/src/Bedrock/End2End/X25519/MontgomeryLadder.v @@ -6,6 +6,8 @@ Require Import Crypto.Spec.MontgomeryCurve. Require Import Crypto.Spec.Curve25519. Require Import bedrock2.Map.Separation. Require Import bedrock2.Syntax. +Require Import bedrock2Examples.memmove. +Require Import bedrock2.SepAutoArray. Require Import compiler.Pipeline. Require Import compiler.Symbols. Require Import compiler.MMIO. @@ -18,6 +20,7 @@ Require Import Crypto.Bedrock.Group.ScalarMult.LadderStep. Require Import Crypto.Bedrock.Group.ScalarMult.CSwap. Require Import Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder. Require Import Crypto.Bedrock.End2End.X25519.Field25519. +Require Import Crypto.Bedrock.End2End.X25519.clamp. Local Open Scope string_scope. Import ListNotations. @@ -32,18 +35,24 @@ Proof. vm_compute. subst; exact eq_refl. Qed. Require Import bedrock2.NotationsCustomEntry. Definition x25519 := func! (out, sk, pk) { + stackalloc 32 as K; + memmove(K, sk, $32); + clamp(K); stackalloc 40 as U; fe25519_from_bytes(U, pk); stackalloc 40 as OUT; - montladder(OUT, sk, U); + montladder(OUT, K, U); fe25519_to_bytes(out, OUT) }. Definition x25519_base := func! (out, sk) { + stackalloc 32 as K; + memmove(K, sk, $32); + clamp(K); stackalloc 40 as U; fe25519_from_word(U, $9); stackalloc 40 as OUT; - montladder(OUT, sk, U); + montladder(OUT, K, U); fe25519_to_bytes(out, OUT) }. @@ -51,19 +60,27 @@ Import LittleEndianList. Local Coercion F.to_Z : F >-> Z. Require Import bedrock2.WeakestPrecondition bedrock2.Semantics bedrock2.ProgramLogic. Require Import bedrock2.Syntax bedrock2.Map.SeparationLogic. -Require Import coqutil.Map.OfListWord Coq.Init.Byte coqutil.Byte. +Require Import 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_spec s P := le_split 32 (M.X0 (Curve25519.M.scalarmult (Curve25519.clamp (le_combine s)) P)). +Lemma length_x25519_spec s P : length (x25519_spec s P) = 32%nat. Proof. apply length_le_split. Qed. + Global Instance spec_of_x25519 : spec_of "x25519" := 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 /\ 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 (M.X0 (Curve25519.M.scalarmult (le_combine s mod 2^255) P))$@out) }. + ensures t' m := t=t' /\ m=* s$@sk ⋆ p$@pk ⋆ R ⋆ (x25519_spec s P)$@out }. +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; + ensures t' m := t=t' /\ m=* s$@sk ⋆ R ⋆ (x25519_spec s Curve25519.M.B)$@out }. + +Local Instance spec_of_memmove_array : spec_of "memmove" := spec_of_memmove_array. 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. @@ -81,12 +98,16 @@ Local Arguments word.of_Z : simpl never. Lemma x25519_ok : program_logic_goal_for_function! x25519. Proof. repeat straightline. - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a) H2. { transitivity 40%nat; trivial. } + + straightline_call; ssplit; try ecancel_assumption; repeat straightline; try listZnWords; []. + straightline_call; ssplit; try ecancel_assumption; repeat straightline; try listZnWords; []. + + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a0) H17. { transitivity 40%nat; trivial. } straightline_call; ssplit. { eexists. ecancel_assumption. } { cbv [Field.FElem]. - use_sep_assumption. cancel. cancel_seps_at_indices 0%nat 0%nat; cbn; trivial. eapply RelationClasses.reflexivity. } + use_sep_assumption. cancel. cancel_seps_at_indices 0%nat 0%nat; cbn [seps]; eapply RelationClasses.reflexivity. } { unfold Field.bytes_in_bounds, frep25519, field_representation, Signature.field_representation, Representation.frep. match goal with |- ?P ?x ?z => let y := eval cbv in x in change (P y z) end; cbn. repeat (destruct p as [|? p]; try (cbn [length] in *;discriminate); []). @@ -100,7 +121,7 @@ Proof. eapply byte.unsigned_range. } repeat straightline. - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H16. { transitivity 40%nat; trivial. } + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H24. { transitivity 40%nat; trivial. } straightline_call; ssplit. { unfold FElem, Field.FElem in *; extract_ex1_and_emp_in_goal; ssplit. @@ -109,10 +130,10 @@ Proof. all : eauto. { instantiate (1:=None). exact I. } } { reflexivity. } - { rewrite H3. vm_compute. inversion 1. } + { rewrite ?length_le_split. vm_compute. inversion 1. } repeat straightline. - specialize (H23 P ltac:(assumption)). cbv [FElem] in H23. extract_ex1_and_emp_in H23. + specialize (H31 P ltac:(assumption)). cbv [FElem] in H31. extract_ex1_and_emp_in H31. straightline_call; ssplit. { ecancel_assumption. } { transitivity 32%nat; auto. } @@ -122,43 +143,46 @@ Proof. repeat straightline. cbv [Field.FElem] in *. - seprewrite_in @Bignum.Bignum_to_bytes H26. - seprewrite_in @Bignum.Bignum_to_bytes H26. - extract_ex1_and_emp_in H26. + seprewrite_in @Bignum.Bignum_to_bytes H34. + seprewrite_in @Bignum.Bignum_to_bytes H34. + extract_ex1_and_emp_in H34. + pose proof length_le_split 32 (Curve25519.clamp (le_combine s)). repeat straightline; intuition eauto. - rewrite H30 in *. - use_sep_assumption; cancel. reflexivity. + cbv [x25519_spec]. + use_sep_assumption; cancel. + 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. 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; - ensures t' m := t=t' /\ m=* s$@sk ⋆ R ⋆ - 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. repeat straightline. - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a) H2. { transitivity 40%nat; trivial. } + + straightline_call; ssplit; try ecancel_assumption; repeat straightline; try listZnWords; []. + straightline_call; ssplit; try ecancel_assumption; repeat straightline; try listZnWords; []. + + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a0) H14. { transitivity 40%nat; trivial. } straightline_call; ssplit. { cbv [Field.FElem]. cbn. cbv [n]. ecancel_assumption. } repeat straightline. - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H13. { transitivity 40%nat; trivial. } + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H21. { transitivity 40%nat; trivial. } straightline_call; 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. } + cancel_seps_at_indices 0%nat 0%nat; trivial. cbn [seps]. reflexivity. } all : eauto. { instantiate (1:=None). exact I. } } { reflexivity. } - { rewrite H3. vm_compute. inversion 1. } + { rewrite length_le_split. vm_compute. inversion 1. } repeat straightline. - specialize (H20 Curve25519.M.B eq_refl). - unfold FElem in H20. extract_ex1_and_emp_in H20. + specialize (H28 Curve25519.M.B eq_refl). + unfold FElem in H28. extract_ex1_and_emp_in H28. straightline_call; ssplit. { ecancel_assumption. } { transitivity 32%nat; auto. } @@ -168,13 +192,18 @@ Proof. repeat straightline. cbv [Field.FElem] in *. - seprewrite_in @Bignum.Bignum_to_bytes H23. - seprewrite_in @Bignum.Bignum_to_bytes H23. - extract_ex1_and_emp_in H23. + seprewrite_in @Bignum.Bignum_to_bytes H31. + seprewrite_in @Bignum.Bignum_to_bytes H31. + extract_ex1_and_emp_in H31. + pose proof length_le_split 32 (Curve25519.clamp (le_combine s)). repeat straightline; intuition eauto. - rewrite H27 in *. - use_sep_assumption; cancel. reflexivity. + cbv [x25519_spec]. + use_sep_assumption; cancel. + 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. Qed. Require Import coqutil.Word.Naive. @@ -197,7 +226,9 @@ Definition funcs := fe25519_add; fe25519_sub; fe25519_square; - fe25519_scmula24 ]. + fe25519_scmula24; + clamp; + memmove ]. Require Import bedrock2.ToCString. Definition montladder_c_module := list_byte_of_string (ToCString.c_module funcs). diff --git a/src/Bedrock/End2End/X25519/clamp.v b/src/Bedrock/End2End/X25519/clamp.v new file mode 100644 index 0000000000..d5336185c9 --- /dev/null +++ b/src/Bedrock/End2End/X25519/clamp.v @@ -0,0 +1,152 @@ +From Coq Require Import ZArith Lia. Local Open Scope Z_scope. + +Module Z. + Lemma testbit_pow2 n i (H : 0 <= n) : Z.testbit (2^n) i = Z.eqb i n. + Proof. + rewrite <-(Z.mul_1_l (2^n)), Z.mul_pow2_bits by trivial. + case (Z.eqb_spec i n) as [->|]; rewrite ?Z.sub_diag; trivial. + case (Z.ltb_spec (i-n) 0) as []; rewrite ?Z.testbit_neg_r by lia; trivial. + eapply Z.bits_above_log2; cbn; lia. + Qed. +End Z. + +Local Ltac t := + try (eapply Z.bits_inj'; intros i Hi); + repeat match goal with + | _ => progress subst + | _ => solve [trivial | lia] + | _ => progress rewrite + ?Z.sub_simpl_r, + ?Z.testbit_0_l, ?Z.testbit_neg_r, ?Z.testbit_pow2, ?Z.testbit_ones, + ?Z.lor_spec, ?Z.land_spec, ?Z.lxor_spec, ?Z.ldiff_spec, + ?Z.testbit_mod_pow2, ?Z.shiftl_spec, ?Z.shiftl_spec_low, ?Z.shiftr_spec + by lia + | _ => progress rewrite + ?Bool.andb_false_r, ?Bool.andb_true_r, + ?Bool.andb_false_l, ?Bool.andb_true_l, + ?Bool.orb_false_r, ?Bool.orb_true_r, + ?Bool.orb_false_l, ?Bool.orb_true_l, + ?Bool.xorb_false_r, ?Bool.xorb_true_r, + ?Bool.xorb_false_l, ?Bool.xorb_true_l, + ?Bool.negb_involutive + | |- _ => progress cbn [negb] + | |- context [Z.leb ?x ?y] => destruct (Z.leb_spec x y) as [] + | |- context [Z.ltb ?x ?y] => destruct (Z.ltb_spec x y) as [] + | |- context [Z.eqb ?x ?y] => destruct (Z.eqb_spec x y) as [] + end. + +Require Import Crypto.Spec.Curve25519. + +Lemma mod8_clamp' k : clamp k mod 8 = 0. +Proof. cbv [clamp]. Z.div_mod_to_equations. lia. Qed. + +Lemma clamp_range k : 2^254 <= clamp k < 2^255. +Proof. cbv [clamp]. Z.div_mod_to_equations. lia. Qed. + +Definition clamp' k := Z.lor (Z.ldiff k (Z.ones 3) mod 2^255) (2^254). + +Lemma clamp'_correct k : clamp' k = Curve25519.clamp k. +Proof. + cbv [Curve25519.clamp clamp']; change 8 with (2^3). + rewrite Z.mul_comm, <-Z.shiftl_mul_pow2, <-Z.shiftr_div_pow2, ?Z.add_nocarry_lxor; try lia; t. +Qed. + + +From Coq Require Import ZArith Lia. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import Coq.Init.Byte. +Require Import bedrock2.Map.Separation. +Require Import bedrock2.Syntax. +Require Import bedrock2.NotationsCustomEntry. + +Local Open Scope Z_scope. +Local Open Scope string_scope. +Import Syntax Syntax.Coercions NotationsCustomEntry. +Import ListNotations. + +Definition clamp := func! (sk) { + store1(sk, load1(sk) & $248); + store1(sk+$31, (load1(sk+$31) & $127) | $64) +}. + +From coqutil Require Import Word.Interface Word.Naive. +From coqutil Require Import SortedListWord. +From coqutil Require Import symmetry. +Require Import bedrock2.FE310CSemantics. +Local Existing Instances SortedListString.map SortedListWord.map coqutil.Word.Naive.word. + +From coqutil Require Import LittleEndianList. +Require Import bedrock2.Syntax bedrock2.WeakestPrecondition bedrock2.Map.SeparationLogic. +Import Coq.Lists.List. (* TODO: SeparationLogic should not override skipn and etc *) +From bedrock2 Require Import ProgramLogic. 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"). +Import Byte Word.Properties. +Local Coercion byte.unsigned : byte >-> Z. +Local Arguments le_combine !_. + +Global Instance spec_of_clamp : spec_of "clamp" := + fnspec! "clamp" sk / (s : list Byte.byte) (R : _ -> Prop), + { requires t m := m =* s$@sk ⋆ R /\ length s = 32%nat; + ensures t' m := t=t' /\ m=* (le_split 32 (Curve25519.clamp (le_combine s)))$@sk ⋆ R }. + +Lemma clamp_correct : program_logic_goal_for_function! clamp. +Proof. + straightline; repeat straightline_cleanup. + + do 1 try destruct s as [|?b s]; try (cbn [length] in *; congruence). + cbn [Array.array] in *; cbn [length] in *. + repeat straightline. + + rewrite <-(firstn_skipn 30 s) in H1 |- *. + seprewrite_in @Array.bytearray_append H1; rewrite ?app_length, ?firstn_length_le in * by lia. + rewrite <-!Properties.word.add_assoc, <-!Properties.word.ring_morph_add in *; simpl Z.add in *. + + assert (length (skipn 30 s) = 1)%nat by (rewrite skipn_length; lia). + assert (length (firstn 30 s) = 30)%nat by (rewrite firstn_length; lia). + destruct (skipn 30 s) as [|b31 [] ] eqn:? in *; try (cbn [length] in *; congruence). + cbn [Array.array] in *. + + repeat straightline. + + eassert (Hrw : Lift1Prop.iff1 (ptsto a (Byte.byte.of_Z v0)) ([Byte.byte.of_Z v0]$@a)) by (cbn [Array.array]; cancel). + repeat seprewrite_in Hrw H4. + repeat seprewrite_in (symmetry! @Array.array_cons) H4. + seprewrite_in @Array.bytearray_index_merge H4. + { cbn [length]; rewrite ?app_length, ?length_firstn, ?Properties.word.unsigned_of_Z_nowrap; try lia. } + + eassert (le_split _ _ = _) as ->; [|ecancel_assumption]. + clear -H0 Heql0. + + eapply le_combine_inj; rewrite ?le_combine_split. + { repeat (cbn [length]; rewrite ?length_le_split, ?app_length, ?firstn_length). lia. } + + rewrite <-clamp'_correct. + + repeat (cbn [le_combine]; rewrite ?le_combine_app, ?le_combine_firstn). + + subst v v0. + + cbn [length]; rewrite ?firstn_length_le by lia. + simpl Z.mul at 1 2. + rewrite ?byte.unsigned_of_Z; cbv [byte.wrap]. + repeat rewrite ?word.unsigned_and_nowrap, ?word.unsigned_or_nowrap. + + pose proof byte.unsigned_range b. + pose proof byte.unsigned_range b31. + rewrite ?word.unsigned_of_Z_nowrap; try lia. + cbv [clamp']. + + rewrite <-(byte.wrap_unsigned b); + rewrite <-(byte.wrap_unsigned b31); + cbv [byte.wrap]. + change 127 with (Z.ones 7). + change 64 with (2^6). + change 248 with (Z.ldiff (Z.ones 8) (Z.ones 3)). + change (31%nat * 8) with 248 in *. + + t. + + f_equal; lia. +Qed. diff --git a/src/Spec/Curve25519.v b/src/Spec/Curve25519.v index aedd4e9e3b..f8a7d55650 100644 --- a/src/Spec/Curve25519.v +++ b/src/Spec/Curve25519.v @@ -109,3 +109,5 @@ Module M. Definition X0 := (M.X0(Feq:=eq)(Fzero:=F.zero)(Fadd:=F.add)(Fmul:=F.mul)(a:=a)(b:=b)). Definition scalarmult := (@ScalarMult.scalarmult_ref _ add M.zero opp). End M. + +Definition clamp k := let s := k/8 mod 2^251 in 8*(2^251 + s).