From 68f7408e98e5cd61b551e0c707d2273aef33b4f6 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 9 Jun 2023 16:56:13 -0400 Subject: [PATCH 01/18] simple square_and_add function --- src/Bedrock/End2End/X25519/MontgomeryLadder.v | 214 ++++++++++++------ 1 file changed, 141 insertions(+), 73 deletions(-) diff --git a/src/Bedrock/End2End/X25519/MontgomeryLadder.v b/src/Bedrock/End2End/X25519/MontgomeryLadder.v index e2e2ee4e35..dfdef016a6 100644 --- a/src/Bedrock/End2End/X25519/MontgomeryLadder.v +++ b/src/Bedrock/End2End/X25519/MontgomeryLadder.v @@ -16,35 +16,42 @@ 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.Specs.Field. Local Open Scope string_scope. +Local Open Scope Z_scope. Import ListNotations. Local Instance frep25519 : Field.FieldRepresentation(field_parameters:=field_parameters) := field_representation n Field25519.s c. -Derive ladderstep SuchThat (ladderstep = ladderstep_body) As ladderstep_defn. -Proof. vm_compute. subst; exact eq_refl. Qed. - -Derive montladder SuchThat (montladder = montladder_body (Z.to_nat (Z.log2 Curve25519.order))) - As montladder_defn. -Proof. vm_compute. subst; exact eq_refl. Qed. Require Import bedrock2.NotationsCustomEntry. -Definition x25519 := func! (out, sk, pk) { - stackalloc 40 as U; - fe25519_from_bytes(U, pk); - stackalloc 40 as OUT; - montladder(OUT, sk, U); - fe25519_to_bytes(out, OUT) +(* Definition square_and_add := func! (o, x, y) { + stackalloc 40 as tmp; + fe25519_square(tmp, x); + fe25519_add(o, tmp, y) +}. *) + +Definition square_and_add := func! (o, x, y) { + fe25519_square(o, x); + fe25519_add(o, o, y) }. -Definition x25519_base := func! (out, sk) { - stackalloc 40 as U; - fe25519_from_word(U, $9); - stackalloc 40 as OUT; - montladder(OUT, sk, U); - fe25519_to_bytes(out, OUT) +Definition mul_and_add := func! (o, x, y) { + fe25519_mul(o, x, x); + fe25519_add(o, o, y) }. +Require Import bedrock2.FE310CSemantics bedrock2.Semantics . +Require Import bedrock2.WeakestPrecondition bedrock2.ProgramLogic. +Require Import coqutil.Word.Interface coqutil.Word.Bitwidth. +Require Import coqutil.Map.Interface bedrock2.Map.SeparationLogic. +Require Import bedrock2.Array bedrock2.Scalars. +Require Import bedrock2.ZnWords. +Require Import coqutil.Tactics.Tactics. + +Section WithParameters. + Check _: FieldRepresentation. + Import LittleEndianList. Local Coercion F.to_Z : F >-> Z. Require Import bedrock2.WeakestPrecondition bedrock2.Semantics bedrock2.ProgramLogic. @@ -53,74 +60,135 @@ 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 := montladder_gallina (Field.M_pos(FieldParameters:=field_parameters)) Field.a24 (Z.to_nat (Z.log2 (Z.pos order))). -Global Instance spec_of_x25519 : spec_of "x25519" := - fnspec! "x25519" out sk pk / (o s p : list Byte.byte) (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; - ensures t' m := t=t' /\ m=* s$@sk ⋆ p$@pk ⋆ R ⋆ - (le_split 32 (x25519_gallina (le_combine s) (Field.feval_bytes 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 Notation FElem := (FElem(FieldRepresentation:=frep25519)). +Local Notation bounded_by := (bounded_by(FieldRepresentation:=frep25519)). +Local Notation word := (Naive.word 32). +Local Notation felem := (felem(FieldRepresentation:=frep25519)). + +Global Instance spec_of_square_and_add : spec_of "square_and_add" := + fnspec! "square_and_add" (out xk yk: word) / (o x y : felem) (R : _ -> Prop), + { requires t m := + bounded_by loose_bounds x /\ + bounded_by tight_bounds y /\ + m =* (FElem xk x) * (FElem yk y) * (FElem out o) * R; + ensures t' m' := + t=t' /\ + exists o', feval o' = F.add (F.pow (feval x) 2) (feval y) + /\ bounded_by loose_bounds o' + /\ m' =* (FElem xk x) * (FElem yk y) * (FElem out o') * R }. + +Global Instance spec_of_mul_and_add : spec_of "mul_and_add" := + fnspec! "mul_and_add" (out xk yk: word) / (o x y : felem) (R : _ -> Prop), + { requires t m := + bounded_by loose_bounds x /\ + bounded_by tight_bounds y /\ + m =* (FElem xk x) * (FElem yk y) * (FElem out o) * R; + ensures t' m' := + t=t' /\ + exists o', feval o' = F.add (F.mul (feval x) (feval x)) (feval y) + /\ bounded_by loose_bounds o' + /\ m' =* (FElem xk x) * (FElem yk y) * (FElem out o') * R }. + +Local Instance spec_of_fe25519_square : spec_of "fe25519_square" := Field.spec_of_UnOp un_square. +Local Instance spec_of_fe25519_mul : spec_of "fe25519_mul" := Field.spec_of_BinOp bin_mul. +Local Instance spec_of_fe25519_add : spec_of "fe25519_add" := Field.spec_of_BinOp bin_add. + +Import WeakestPrecondition. + +From coqutil.Tactics Require Import Tactics letexists eabstract rdelta reference_to_string ident_of_string. +Require Import bedrock2.Syntax. +Require Import bedrock2.WeakestPrecondition. +Require Import bedrock2.WeakestPreconditionProperties. +Require Import bedrock2.Loops. +Require Import bedrock2.Map.SeparationLogic bedrock2.Scalars. 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. +Lemma square_and_add_ok : program_logic_goal_for_function! square_and_add. Proof. repeat straightline. - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a) H2. { transitivity 40%nat; trivial. } + repeat match goal with + | |- _ /\ _ => split + | |- call _ _ _ _ _ _ => straightline_call + | _ => straightline + end. + (* square *) + - (* square precondition bounds on x *) apply H1. + - (* mem sep for x *) eexists. ecancel_assumption. + - (* mem sep for out *) ecancel_assumption. + (* add *) + - (* add precondition bounds on x^2 *) apply H7. + - (* add precondition bounds on y *) apply H2. + - (* mem sep for o (holding x^2) *) eexists. ecancel_assumption. + - (* mem sep for y *) eexists. ecancel_assumption. + - (* mem sep for o (holding x^2+y) *) ecancel_assumption. + (* post-conditions *) + - exists x1. split. 2:split. + + (* math adds up *) simpl in H9. simpl in H6. rewrite H6 in H9. simpl. apply H9. (* Definitely better tactics for this *) + + (* postcondition bounds on out *) simpl in H10. simpl. apply H10. (* should just work to apply H10... *) + + (* postcondition mem sep *) ecancel_assumption. +Qed. - 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. } - { 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); []). - cbn; cbn [nth] in *. - cbv [COperationSpecifications.list_Z_bounded_by FoldBool.fold_andb_map map seq]; cbn. - pose proof byte.unsigned_range as HH. setoid_rewrite <-Le.Z.le_sub_1_iff in HH. cbn in HH. - setoid_rewrite Zle_is_le_bool in HH. setoid_rewrite <-Bool.andb_true_iff in HH. - rewrite 31HH; cbn. - eapply Bool.andb_true_iff; split; trivial. - eapply Bool.andb_true_iff; split; eapply Zle_is_le_bool; trivial. - eapply byte.unsigned_range. } - repeat straightline. +Local Ltac unwrap_calls := + repeat match goal with + | |- _ /\ _ => split + | |- call _ _ _ _ _ _ => straightline_call + | _ => straightline + end. - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H15. { transitivity 40%nat; trivial. } +Local Ltac solve_bounds := + repeat match goal with + | H: bounded_by loose_bounds _ |- bounded_by loose_bounds _ => apply H + | H: bounded_by tight_bounds _ |- bounded_by tight_bounds _ => apply H + | H: bounded_by _ _ |- bounded_by _ _ => cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add un_outbounds bin_outbounds] in * + end. - straightline_call; ssplit. - 3: { 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. - { instantiate (1:=None). exact I. } } - { reflexivity. } - { rewrite H3. vm_compute. inversion 1. } - repeat straightline. +Local Ltac solve_mem := + repeat match goal with + | |- exists _, _%sep _ => eexists + | |- _%sep _ => ecancel_assumption + end. - cbv [FElem] in H22. extract_ex1_and_emp_in H22. - straightline_call; ssplit. - { ecancel_assumption. } - { transitivity 32%nat; auto. } - { eexists. ecancel_assumption. } - { intuition idtac. } - repeat straightline_cleanup. +Lemma square_and_add_ok2 : program_logic_goal_for_function! square_and_add. +Proof. repeat straightline. + unwrap_calls. + all: try solve_mem. all: try solve_bounds. + (* post-conditions *) + - exists x1. split. 2:split. + + (* math adds up *) simpl in H9. simpl in H6. rewrite H6 in H9. simpl. apply H9. (* Definitely better tactics for this *) + + (* postcondition bounds on out *) simpl in H10. simpl. apply H10. (* should just work to apply H10... *) + + (* postcondition mem sep *) ecancel_assumption. +Qed. - cbv [Field.FElem] in *. - seprewrite_in @Bignum.Bignum_to_bytes H25. - seprewrite_in @Bignum.Bignum_to_bytes H25. - extract_ex1_and_emp_in H25. - - repeat straightline; intuition eauto. - rewrite H29 in *. cbv [x25519_gallina]. - use_sep_assumption; cancel. eapply RelationClasses.reflexivity. +Lemma mul_and_add_ok : program_logic_goal_for_function! mul_and_add. +Proof. + repeat straightline. + repeat match goal with + | |- _ /\ _ => split + | |- call _ _ _ _ _ _ => straightline_call + | _ => straightline + end. + (* square *) + - (* mul precondition bounds on x *) apply H1. + - (* same bounds gain *) apply H1. + - (* mem sep for x *) eexists. ecancel_assumption. + - (* same mem sep again *) eexists. ecancel_assumption. + - (* mem sep for out *) ecancel_assumption. + (* add *) + - (* add precondition bounds on x^2 *) apply H7. + - (* add precondition bounds on y *) apply H2. + - (* mem sep for o (holding x^2) *) eexists. ecancel_assumption. + - (* mem sep for y *) eexists. ecancel_assumption. + - (* mem sep for o (holding x^2+y) *) ecancel_assumption. + (* post-conditions *) + - exists x1. split. 2:split. + + (* math adds up *) simpl in H9. simpl in H6. rewrite H6 in H9. simpl. apply H9. (* Definitely better tactics for this *) + + (* postcondition bounds on out *) simpl in H10. simpl. apply H10. (* should just work to apply H10... *) + + (* postcondition mem sep *) ecancel_assumption. Qed. Global Instance spec_of_x25519_base : spec_of "x25519_base" := From 9c6fddc2da63766426827dd44fd1165434771814 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 9 Jun 2023 16:57:03 -0400 Subject: [PATCH 02/18] cleanup --- src/Bedrock/End2End/X25519/MontgomeryLadder.v | 110 ------------------ 1 file changed, 110 deletions(-) diff --git a/src/Bedrock/End2End/X25519/MontgomeryLadder.v b/src/Bedrock/End2End/X25519/MontgomeryLadder.v index dfdef016a6..c607b2812e 100644 --- a/src/Bedrock/End2End/X25519/MontgomeryLadder.v +++ b/src/Bedrock/End2End/X25519/MontgomeryLadder.v @@ -25,12 +25,6 @@ Local Instance frep25519 : Field.FieldRepresentation(field_parameters:=field_par Require Import bedrock2.NotationsCustomEntry. -(* Definition square_and_add := func! (o, x, y) { - stackalloc 40 as tmp; - fe25519_square(tmp, x); - fe25519_add(o, tmp, y) -}. *) - Definition square_and_add := func! (o, x, y) { fe25519_square(o, x); fe25519_add(o, o, y) @@ -191,107 +185,3 @@ Proof. + (* postcondition mem sep *) ecancel_assumption. 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 (x25519_gallina (le_combine s) (F.of_Z _ 9)))$@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. - { cbv [Field.FElem]. cbn. cbv [n]. ecancel_assumption. } - repeat straightline. - - 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. - { use_sep_assumption. cancel; repeat ecancel_step. - cancel_seps_at_indices 0%nat 0%nat; trivial. cbn; reflexivity. } - all : eauto. - { instantiate (1:=None). exact I. } } - { reflexivity. } - { rewrite H3. vm_compute. inversion 1. } - repeat straightline. - - unfold FElem in H20. extract_ex1_and_emp_in H20. - straightline_call; ssplit. - { ecancel_assumption. } - { transitivity 32%nat; auto. } - { eexists. ecancel_assumption. } - { intuition idtac. } - repeat straightline_cleanup. - 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. - - repeat straightline; intuition eauto. - rewrite H27 in *. cbv [x25519_gallina]. - use_sep_assumption; cancel. eapply RelationClasses.reflexivity. -Qed. - -Require Import coqutil.Word.Naive. -Require Import coqutil.Macros.WithBaseName. - -Definition felem_cswap := CSwap.felem_cswap(word:=word32)(field_parameters:=field_parameters)(field_representaton:=field_representation n s c). -Definition fe25519_inv := fe25519_inv(word:=word32)(field_parameters:=field_parameters). - -Definition funcs := - &[,x25519; x25519_base; - montladder; - fe25519_to_bytes; - fe25519_from_bytes; - fe25519_from_word; - felem_cswap; - fe25519_copy; - fe25519_inv; - ladderstep; - fe25519_mul; - fe25519_add; - fe25519_sub; - fe25519_square; - fe25519_scmula24 ]. - -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. -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. -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. From 789a135d2427ca49fa7dcc9fe4590285b5fb4f20 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 23 Jun 2023 07:28:03 -0400 Subject: [PATCH 03/18] Definition and spec for point add fn --- src/Bedrock/End2End/X25519/MontgomeryLadder.v | 53 ++++++++++++++++++- 1 file changed, 52 insertions(+), 1 deletion(-) diff --git a/src/Bedrock/End2End/X25519/MontgomeryLadder.v b/src/Bedrock/End2End/X25519/MontgomeryLadder.v index c607b2812e..c7bd0f38da 100644 --- a/src/Bedrock/End2End/X25519/MontgomeryLadder.v +++ b/src/Bedrock/End2End/X25519/MontgomeryLadder.v @@ -35,6 +35,30 @@ Definition mul_and_add := func! (o, x, y) { fe25519_add(o, o, y) }. +(* Better way to represent points in Bedrock2? *) +Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, xy2d2) { + stackalloc 40 as YpX1; + fe25519_add(YpX1, Y1, X1); + stackalloc 40 as YmX1; + fe25519_sub(YmX1, Y1, X1); + stackalloc 40 as A; + fe25519_mul(A, YpX1, ypx2); + stackalloc 40 as B; + fe25519_mul(B, YmX1, ymx2); + stackalloc 40 as C; + fe25519_mul(C, xy2d2, T1); + stackalloc 40 as D; + fe25519_add(D, Z1, Z1); + fe25519_sub(ox, A, B); + fe25519_add(oy, A, B); + fe25519_add(oz, D, C); + fe25519_sub(ot, D, C); + fe25519_mul(ox, ox, ot); + fe25519_mul(oy, oy, oz); + fe25519_mul(oz, ot, oz); + fe25519_mul(ot, ox, oy) +}. + Require Import bedrock2.FE310CSemantics bedrock2.Semantics . Require Import bedrock2.WeakestPrecondition bedrock2.ProgramLogic. Require Import coqutil.Word.Interface coqutil.Word.Bitwidth. @@ -58,7 +82,7 @@ Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, Local Notation FElem := (FElem(FieldRepresentation:=frep25519)). Local Notation bounded_by := (bounded_by(FieldRepresentation:=frep25519)). Local Notation word := (Naive.word 32). -Local Notation felem := (felem(FieldRepresentation:=frep25519)). +Local Notation felem := (felem(FieldRepresentation:=frep25519)). Global Instance spec_of_square_and_add : spec_of "square_and_add" := fnspec! "square_and_add" (out xk yk: word) / (o x y : felem) (R : _ -> Prop), @@ -84,9 +108,36 @@ Global Instance spec_of_mul_and_add : spec_of "mul_and_add" := /\ bounded_by loose_bounds o' /\ m' =* (FElem xk x) * (FElem yk y) * (FElem out o') * R }. +Require Import Curves.Edwards.XYZT.Precomputed. (* Move elsewhere *) + +Global Instance spec_of_add_precomputed : spec_of "add_precomputed" := + fnspec! "add_precomputed" + (oxK oyK ozK otK X1K Y1K Z1K T1K ypx2K ymx2K xy2d2K : word) / + (ox oy oz ot X1 Y1 Z1 T1 ypx2 ymx2 xy2d2 : felem) (R : _ -> Prop), + { requires t m := + bounded_by tight_bounds X1 /\ + bounded_by tight_bounds Y1 /\ + bounded_by tight_bounds Z1 /\ (* Could be loose if switch to mul *) + bounded_by loose_bounds T1 /\ + bounded_by loose_bounds ypx2 /\ + bounded_by loose_bounds ymx2 /\ + bounded_by loose_bounds xy2d2 /\ + m =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox) * (FElem oyK oy) * (FElem ozK oz) * (FElem otK ot) * R; + ensures t' m' := + t = t' /\ + exists ox' oy' oz' ot', + (* Need to specify implicit parameters? *) + ((feval ox'), (feval oy'), (feval oz'), (feval ot')) = (@m1add_precomputed_coordinates (F M_pos) (F.add) (F.sub) (F.mul) ((feval X1), (feval Y1), (feval Z1), (feval T1)) ((feval ypx2), (feval ymx2), (feval xy2d2))) /\ + bounded_by loose_bounds ox' /\ + bounded_by loose_bounds oy' /\ + bounded_by loose_bounds oz' /\ + bounded_by loose_bounds ot' /\ + m' =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox') * (FElem oyK oy') * (FElem ozK oz') * (FElem otK ot') * R }. + Local Instance spec_of_fe25519_square : spec_of "fe25519_square" := Field.spec_of_UnOp un_square. Local Instance spec_of_fe25519_mul : spec_of "fe25519_mul" := Field.spec_of_BinOp bin_mul. Local Instance spec_of_fe25519_add : spec_of "fe25519_add" := Field.spec_of_BinOp bin_add. +Local Instance spec_of_fe25519_sub : spec_of "fe25519_sub" := Field.spec_of_BinOp bin_sub. Import WeakestPrecondition. From 5b278d324875967d83e4ddf8c058da95d2d26325 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 30 Jun 2023 15:21:41 -0400 Subject: [PATCH 04/18] Proof for first four lines of precomputed --- src/Bedrock/End2End/X25519/AddPrecomputed.v | 228 ++++++++++++++++++++ 1 file changed, 228 insertions(+) create mode 100644 src/Bedrock/End2End/X25519/AddPrecomputed.v diff --git a/src/Bedrock/End2End/X25519/AddPrecomputed.v b/src/Bedrock/End2End/X25519/AddPrecomputed.v new file mode 100644 index 0000000000..9c3fb1381e --- /dev/null +++ b/src/Bedrock/End2End/X25519/AddPrecomputed.v @@ -0,0 +1,228 @@ +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Spec.Curve25519. +Require Import bedrock2.Map.Separation. +Require Import bedrock2.Syntax. +Require Import compiler.Pipeline. +Require Import compiler.Symbols. +Require Import compiler.MMIO. +Require Import coqutil.Word.Bitwidth32. +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Bedrock.Field.Interface.Compilation2. +Require Import Crypto.Bedrock.Field.Synthesis.New.UnsaturatedSolinas. +Require Import Crypto.Bedrock.Group.AdditionChains. +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.Specs.Field. +Require Import bedrock2.FE310CSemantics bedrock2.Semantics . +Require Import bedrock2.WeakestPrecondition bedrock2.ProgramLogic. +Require Import coqutil.Word.Interface coqutil.Word.Bitwidth. +Require Import coqutil.Map.Interface bedrock2.Map.SeparationLogic. +Require Import bedrock2.Array bedrock2.Scalars. +Require Import bedrock2.ZnWords. +Require Import coqutil.Tactics.Tactics. +Require Import bedrock2.NotationsCustomEntry. +Require Import Curves.Edwards.XYZT.Precomputed. +Local Open Scope string_scope. +Local Open Scope Z_scope. +Import ListNotations. + +Local Instance frep25519 : Field.FieldRepresentation(field_parameters:=field_parameters) := field_representation n Field25519.s c. + +(* Better way to represent points in Bedrock2? *) +Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, xy2d2) { + stackalloc 40 as YpX1; + fe25519_add(YpX1, Y1, X1); + stackalloc 40 as YmX1; + fe25519_sub(YmX1, Y1, X1); + stackalloc 40 as A; + fe25519_mul(A, YpX1, ypx2); + stackalloc 40 as B; + fe25519_mul(B, YmX1, ymx2); + stackalloc 40 as C; + fe25519_mul(C, xy2d2, T1); + stackalloc 40 as D; + fe25519_mul(D, Z1, $2); (* Should be Z1 + Z1, but mul has tighter bounds *) + fe25519_sub(ox, A, B); + fe25519_add(oy, A, B); + fe25519_add(oz, D, C); + fe25519_sub(ot, D, C); + fe25519_mul(ox, ox, ot); + fe25519_mul(oy, oy, oz); + fe25519_mul(oz, ot, oz); + fe25519_mul(ot, ox, oy) +}. + +Definition add_precomputed_partial := func! (X1, Y1) { + stackalloc 40 as YpX1; + fe25519_add(YpX1, Y1, X1); + stackalloc 40 as YmX1; + fe25519_sub(YmX1, Y1, X1) +}. + +Section WithParameters. + Check _: FieldRepresentation. + +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. +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"). + +Local Notation FElem := (FElem(FieldRepresentation:=frep25519)). +Local Notation bounded_by := (bounded_by(FieldRepresentation:=frep25519)). +Local Notation word := (Naive.word 32). +Local Notation felem := (felem(FieldRepresentation:=frep25519)). + + +Global Instance spec_of_add_precomputed : spec_of "add_precomputed" := + fnspec! "add_precomputed" + (oxK oyK ozK otK X1K Y1K Z1K T1K ypx2K ymx2K xy2d2K : word) / + (ox oy oz ot X1 Y1 Z1 T1 ypx2 ymx2 xy2d2 : felem) (R : _ -> Prop), + { requires t m := + bounded_by tight_bounds X1 /\ + bounded_by tight_bounds Y1 /\ + bounded_by loose_bounds Z1 /\ + bounded_by loose_bounds T1 /\ + bounded_by loose_bounds ypx2 /\ + bounded_by loose_bounds ymx2 /\ + bounded_by loose_bounds xy2d2 /\ + m =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox) * (FElem oyK oy) * (FElem ozK oz) * (FElem otK ot) * R; + ensures t' m' := + t = t' /\ + exists ox' oy' oz' ot', + (* Need to specify implicit parameters? *) + ((feval ox'), (feval oy'), (feval oz'), (feval ot')) = (@m1add_precomputed_coordinates (F M_pos) (F.add) (F.sub) (F.mul) ((feval X1), (feval Y1), (feval Z1), (feval T1)) ((feval ypx2), (feval ymx2), (feval xy2d2))) /\ + bounded_by loose_bounds ox' /\ + bounded_by loose_bounds oy' /\ + bounded_by loose_bounds oz' /\ + bounded_by loose_bounds ot' /\ + m' =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox') * (FElem oyK oy') * (FElem ozK oz') * (FElem otK ot') * R }. + +Global Instance spec_of_add_precomputed_partial : spec_of "add_precomputed_partial" := + fnspec! "add_precomputed_partial" + (X1K Y1K : word) / + (X1 Y1 : felem) (R : _ -> Prop), + { requires t m := + bounded_by tight_bounds X1 /\ + bounded_by tight_bounds Y1 /\ + m =* (FElem X1K X1) * (FElem Y1K Y1) * R; + ensures t' m' := + t = t' /\ + m' =* (FElem X1K X1) * (FElem Y1K Y1) * R }. + + +Local Instance spec_of_fe25519_square : spec_of "fe25519_square" := Field.spec_of_UnOp un_square. +Local Instance spec_of_fe25519_mul : spec_of "fe25519_mul" := Field.spec_of_BinOp bin_mul. +Local Instance spec_of_fe25519_add : spec_of "fe25519_add" := Field.spec_of_BinOp bin_add. +Local Instance spec_of_fe25519_sub : spec_of "fe25519_sub" := Field.spec_of_BinOp bin_sub. + +Import WeakestPrecondition. + +From coqutil.Tactics Require Import Tactics letexists eabstract rdelta reference_to_string ident_of_string. +Require Import bedrock2.Syntax. +Require Import bedrock2.WeakestPrecondition. +Require Import bedrock2.WeakestPreconditionProperties. +Require Import bedrock2.Loops. +Require Import bedrock2.Map.SeparationLogic bedrock2.Scalars. + +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. +Local Ltac unwrap_calls := + repeat match goal with + | |- _ /\ _ => split + | |- call _ _ _ _ _ _ => straightline_call + | _ => straightline + end. + +Local Ltac solve_stack := + match goal with + | |- 40 mod bytes_per_word 32 = 0 => auto + end. + +Local Ltac solve_bounds := + repeat match goal with + | H: bounded_by loose_bounds _ |- bounded_by loose_bounds _ => apply H + | H: bounded_by tight_bounds _ |- bounded_by tight_bounds _ => apply H + | H: bounded_by _ _ |- bounded_by _ _ => cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_sub un_outbounds bin_outbounds] in * + end. + +Local Ltac solve_mem := + repeat match goal with + | |- exists _ : _ -> Prop, _%sep _ => eexists + | |- _%sep _ => ecancel_assumption + end. + +Lemma add_precomputed_partial_ok : program_logic_goal_for_function! add_precomputed_partial. +Proof. + repeat straightline. + unwrap_calls. + all: try solve_stack. (* all: try solve_mem. all: try solve_bounds *) (* Too aggressive somewhere... *) + 3: solve_mem. 3: solve_mem. + solve_bounds. solve_bounds. + - (* (FElem a ?out ⋆ ?Rr)%sep m *) + (* Rewrites the `stack$@a` term in H3 to use a Bignum instead *) + cbv [FElem]. + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a) H3. { transitivity 40%nat; trivial. } + use_sep_assumption. + cancel. cancel_seps_at_indices 0%nat 0%nat; cbn; trivial. + eapply RelationClasses.reflexivity. + - apply H2. (* bounded_by bin_xbounds ?x@{a1:=a0; H12:=H13; mCombined:=a1} *) + - apply H1. (* bounded_by bin_ybounds ?y@{a1:=a0; H12:=H13; mCombined:=a1} *) + - solve_mem. + - solve_mem. + - (* (FElem a2 ?out@{a1:=a0; H12:=H13; mCombined:=a1} ⋆ ?Rr@{a1:=a0; H12:=H13; mCombined:=a1})%sep a1 *) + cbv [FElem]. + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H12. { transitivity 40%nat; trivial. } + use_sep_assumption. + cancel. repeat ecancel_step. cancel_seps_at_indices 0%nat 0%nat; cbn. admit. (* I think context of evars is causing problems? *) + eapply RelationClasses.reflexivity. + - (* exists m' mStack' : SortedListWord.map word Init.Byte.byte, + anybytes a 40 mStack' /\ + map.split a1 m' mStack' /\ list_map (get l0) [] (fun rets : list word => rets = [] /\ a0 = a0 /\ (FElem X1K X1 ⋆ FElem Y1K Y1 ⋆ R)%sep m') *) + (* Rewrites the FElem about `a` in H11 to be about bytes instead, so we can use it to prove things about `a` as bytes *) + cbv [FElem] in *. + seprewrite_in @Bignum.Bignum_to_bytes H17. + seprewrite_in @Bignum.Bignum_to_bytes H17. + extract_ex1_and_emp_in H17. + + repeat straightline; intuition eauto. +Admitted. + +Lemma add_precomputed_ok : program_logic_goal_for_function! add_precomputed. +Proof. + repeat straightline. + unwrap_calls. + - apply H14. (* bounded_by bin_xbounds Y1 *) (* solve_bounds. *) + - apply H13. (* bounded_by bin_ybounds X1 *) (* solve_bounds. *) + - eexists. ecancel_assumption. + - eexists. ecancel_assumption. + - shelve. (* (FElem a ?out ⋆ ?Rr)%sep m *) + - auto. (* 40 mod bytes_per_word 32 = 0 *) + - apply H14. (* bounded_by bin_xbounds ?x@{a1:=a0; H29:=H30; mCombined:=a1} *) + - apply H13. (* bounded_by bin_ybounds ?y@{a1:=a0; H29:=H30; mCombined:=a1} *) + - eexists. ecancel_assumption. (* exists Rx : SortedListWord.map word Init.Byte.byte -> Prop, (FElem Y1K Y1 ⋆ Rx)%sep a1 *) + - eexists. ecancel_assumption. (* exists Ry : SortedListWord.map word Init.Byte.byte -> Prop, (FElem X1K X1 ⋆ Ry)%sep a1 *) + - (* (FElem a2 ?out0@{a1:=a0; H29:=H30; mCombined:=a1} ⋆ ?Rr0@{a1:=a0; H29:=H30; mCombined:=a1})%sep a1 *) + - (* 40 mod bytes_per_word 32 = 0 *) + - (* bounded_by bin_xbounds ?x@{a1:=a5; H29:=H37; mCombined:=a1; a4:=a3; H34:=H35; mCombined0:=a4} *) + + (* (FElem a ?out ⋆ FElem Y1K ?x0)%sep m *) eexists. exists m. split. solve_mem. + + all: try solve_bounds. + (* post-conditions *) + - exists x1. split. 2:split. + + (* math adds up *) simpl in H9. simpl in H6. rewrite H6 in H9. simpl. apply H9. (* Definitely better tactics for this *) + + (* postcondition bounds on out *) simpl in H10. simpl. apply H10. (* should just work to apply H10... *) + + (* postcondition mem sep *) ecancel_assumption. +Qed. + +End WithParameters. From 5a84060c475d9d927cd44e44b1284a33bc2ba68e Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 30 Jun 2023 15:49:05 -0400 Subject: [PATCH 05/18] Fix admit --- src/Bedrock/End2End/X25519/AddPrecomputed.v | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/src/Bedrock/End2End/X25519/AddPrecomputed.v b/src/Bedrock/End2End/X25519/AddPrecomputed.v index 9c3fb1381e..1aa7eb46e8 100644 --- a/src/Bedrock/End2End/X25519/AddPrecomputed.v +++ b/src/Bedrock/End2End/X25519/AddPrecomputed.v @@ -163,9 +163,11 @@ Local Ltac solve_mem := Lemma add_precomputed_partial_ok : program_logic_goal_for_function! add_precomputed_partial. Proof. - repeat straightline. - unwrap_calls. - all: try solve_stack. (* all: try solve_mem. all: try solve_bounds *) (* Too aggressive somewhere... *) + repeat straightline. straightline_call. ssplit. + 6:repeat straightline. 6:straightline_call. 6:ssplit. + 11:repeat straightline. + (* unwrap_calls is apparently too aggressive; so I had to do the above instead *) + (* all: try solve_mem. all: try solve_bounds *) (* Also too aggressive somewhere... *) 3: solve_mem. 3: solve_mem. solve_bounds. solve_bounds. - (* (FElem a ?out ⋆ ?Rr)%sep m *) @@ -173,7 +175,7 @@ Proof. cbv [FElem]. seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a) H3. { transitivity 40%nat; trivial. } use_sep_assumption. - cancel. cancel_seps_at_indices 0%nat 0%nat; cbn; trivial. + cancel. cancel_seps_at_indices 0%nat 0%nat; cbn. trivial. eapply RelationClasses.reflexivity. - apply H2. (* bounded_by bin_xbounds ?x@{a1:=a0; H12:=H13; mCombined:=a1} *) - apply H1. (* bounded_by bin_ybounds ?y@{a1:=a0; H12:=H13; mCombined:=a1} *) @@ -183,19 +185,19 @@ Proof. cbv [FElem]. seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H12. { transitivity 40%nat; trivial. } use_sep_assumption. - cancel. repeat ecancel_step. cancel_seps_at_indices 0%nat 0%nat; cbn. admit. (* I think context of evars is causing problems? *) + cancel. cancel_seps_at_indices 0%nat 0%nat; cbn; trivial. (* I think context of evars is causing problems? *) eapply RelationClasses.reflexivity. - (* exists m' mStack' : SortedListWord.map word Init.Byte.byte, anybytes a 40 mStack' /\ map.split a1 m' mStack' /\ list_map (get l0) [] (fun rets : list word => rets = [] /\ a0 = a0 /\ (FElem X1K X1 ⋆ FElem Y1K Y1 ⋆ R)%sep m') *) (* Rewrites the FElem about `a` in H11 to be about bytes instead, so we can use it to prove things about `a` as bytes *) cbv [FElem] in *. - seprewrite_in @Bignum.Bignum_to_bytes H17. - seprewrite_in @Bignum.Bignum_to_bytes H17. - extract_ex1_and_emp_in H17. + seprewrite_in @Bignum.Bignum_to_bytes H19. + seprewrite_in @Bignum.Bignum_to_bytes H19. + extract_ex1_and_emp_in H19. repeat straightline; intuition eauto. -Admitted. +Qed. Lemma add_precomputed_ok : program_logic_goal_for_function! add_precomputed. Proof. From ede27d727a15fca8b9ffa90e2c5c270cf11d54f7 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 7 Jul 2023 11:41:35 -0400 Subject: [PATCH 06/18] more steps in add_precomputed_partial --- src/Bedrock/End2End/X25519/AddPrecomputed.v | 84 ++++++++++++++------- 1 file changed, 56 insertions(+), 28 deletions(-) diff --git a/src/Bedrock/End2End/X25519/AddPrecomputed.v b/src/Bedrock/End2End/X25519/AddPrecomputed.v index 1aa7eb46e8..a1a06a482b 100644 --- a/src/Bedrock/End2End/X25519/AddPrecomputed.v +++ b/src/Bedrock/End2End/X25519/AddPrecomputed.v @@ -56,11 +56,17 @@ Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, fe25519_mul(ot, ox, oy) }. -Definition add_precomputed_partial := func! (X1, Y1) { +Definition add_precomputed_partial := func! (X1, Y1, T1, ypx2, ymx2, xy2d2) { stackalloc 40 as YpX1; fe25519_add(YpX1, Y1, X1); stackalloc 40 as YmX1; - fe25519_sub(YmX1, Y1, X1) + fe25519_sub(YmX1, Y1, X1); + stackalloc 40 as A; + fe25519_mul(A, YpX1, ypx2); + stackalloc 40 as B; + fe25519_mul(B, YmX1, ymx2); + stackalloc 40 as C; + fe25519_mul(C, xy2d2, T1) }. Section WithParameters. @@ -107,15 +113,19 @@ Global Instance spec_of_add_precomputed : spec_of "add_precomputed" := Global Instance spec_of_add_precomputed_partial : spec_of "add_precomputed_partial" := fnspec! "add_precomputed_partial" - (X1K Y1K : word) / - (X1 Y1 : felem) (R : _ -> Prop), + (X1K Y1K T1K ypx2K ymx2K xy2d2K : word) / + (X1 Y1 T1 ypx2 ymx2 xy2d2 : felem) (R : _ -> Prop), { requires t m := bounded_by tight_bounds X1 /\ bounded_by tight_bounds Y1 /\ - m =* (FElem X1K X1) * (FElem Y1K Y1) * R; + bounded_by loose_bounds T1 /\ + bounded_by loose_bounds ypx2 /\ + bounded_by loose_bounds ymx2 /\ + bounded_by loose_bounds xy2d2 /\ + m =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * R; ensures t' m' := t = t' /\ - m' =* (FElem X1K X1) * (FElem Y1K Y1) * R }. + m' =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * R }. Local Instance spec_of_fe25519_square : spec_of "fe25519_square" := Field.spec_of_UnOp un_square. @@ -150,9 +160,9 @@ Local Ltac solve_stack := Local Ltac solve_bounds := repeat match goal with - | H: bounded_by loose_bounds _ |- bounded_by loose_bounds _ => apply H - | H: bounded_by tight_bounds _ |- bounded_by tight_bounds _ => apply H - | H: bounded_by _ _ |- bounded_by _ _ => cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_sub un_outbounds bin_outbounds] in * + | H: bounded_by loose_bounds ?x |- bounded_by loose_bounds ?x => apply H + | H: bounded_by tight_bounds ?x |- bounded_by tight_bounds ?x => apply H + | H: bounded_by _ ?x |- bounded_by _ ?x => cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_sub un_outbounds bin_outbounds] in * end. Local Ltac solve_mem := @@ -161,32 +171,50 @@ Local Ltac solve_mem := | |- _%sep _ => ecancel_assumption end. +Local Ltac unwrap_fn_step := repeat straightline; straightline_call; ssplit. + Lemma add_precomputed_partial_ok : program_logic_goal_for_function! add_precomputed_partial. Proof. - repeat straightline. straightline_call. ssplit. - 6:repeat straightline. 6:straightline_call. 6:ssplit. - 11:repeat straightline. - (* unwrap_calls is apparently too aggressive; so I had to do the above instead *) - (* all: try solve_mem. all: try solve_bounds *) (* Also too aggressive somewhere... *) - 3: solve_mem. 3: solve_mem. - solve_bounds. solve_bounds. - - (* (FElem a ?out ⋆ ?Rr)%sep m *) - (* Rewrites the `stack$@a` term in H3 to use a Bignum instead *) + (* slightly painful way to split out all the memory and bounds conditions, and the final postconditions *) + unwrap_fn_step. 6:unwrap_fn_step. 11:unwrap_fn_step. 16:unwrap_fn_step. 21:unwrap_fn_step. + 26:repeat straightline. + (* Solve each of the memory and bounds conditions piece-by-piece, as much as possible *) + 3,4:solve_mem. 1,2:solve_bounds. + { (* (FElem a ?out ⋆ ?Rr)%sep m *) + (* Rewrites the `stack$@a` term in H10 to use a Bignum instead *) cbv [FElem]. - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a) H3. { transitivity 40%nat; trivial. } + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a) H10. { transitivity 40%nat; trivial. } use_sep_assumption. cancel. cancel_seps_at_indices 0%nat 0%nat; cbn. trivial. - eapply RelationClasses.reflexivity. - - apply H2. (* bounded_by bin_xbounds ?x@{a1:=a0; H12:=H13; mCombined:=a1} *) - - apply H1. (* bounded_by bin_ybounds ?y@{a1:=a0; H12:=H13; mCombined:=a1} *) - - solve_mem. - - solve_mem. - - (* (FElem a2 ?out@{a1:=a0; H12:=H13; mCombined:=a1} ⋆ ?Rr@{a1:=a0; H12:=H13; mCombined:=a1})%sep a1 *) + eapply RelationClasses.reflexivity. } + 3,4:solve_mem. 1,2:solve_bounds. + { (* (FElem a2 ?out ⋆ ?Rr)%sep a1 *) + cbv [FElem]. + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H19. { transitivity 40%nat; trivial. } + use_sep_assumption. + cancel. cancel_seps_at_indices 0%nat 0%nat; cbn; trivial. + eapply RelationClasses.reflexivity. } + 3,4:solve_mem. 1,2:solve_bounds. + { (* (FElem a0 ?out ⋆ ?Rr)%sep a5 *) + cbv [FElem]. + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a0) H26. { transitivity 40%nat; trivial. } + use_sep_assumption. + cancel. cancel_seps_at_indices 0%nat 0%nat; cbn; trivial. + eapply RelationClasses.reflexivity. } + 3,4:solve_mem. 1,2:solve_bounds. + { (* (FElem a4 ?out ⋆ ?Rr)%sep a8 *) + cbv [FElem]. + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a4) H33. { transitivity 40%nat; trivial. } + use_sep_assumption. + cancel. cancel_seps_at_indices 0%nat 0%nat; cbn; trivial. + eapply RelationClasses.reflexivity. } + 3,4:solve_mem. 1,2:solve_bounds. + { (* (FElem a7 ?out ⋆ ?Rr)%sep a11 *) cbv [FElem]. - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H12. { transitivity 40%nat; trivial. } + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a7) H40. { transitivity 40%nat; trivial. } use_sep_assumption. - cancel. cancel_seps_at_indices 0%nat 0%nat; cbn; trivial. (* I think context of evars is causing problems? *) - eapply RelationClasses.reflexivity. + cancel. cancel_seps_at_indices 0%nat 0%nat; cbn; trivial. + eapply RelationClasses.reflexivity. } - (* exists m' mStack' : SortedListWord.map word Init.Byte.byte, anybytes a 40 mStack' /\ map.split a1 m' mStack' /\ list_map (get l0) [] (fun rets : list word => rets = [] /\ a0 = a0 /\ (FElem X1K X1 ⋆ FElem Y1K Y1 ⋆ R)%sep m') *) From b1cfb950f4e517fe6e41a44488788cf687da85b7 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 7 Jul 2023 12:15:58 -0400 Subject: [PATCH 07/18] automate stack solving! --- src/Bedrock/End2End/X25519/AddPrecomputed.v | 74 +++++++-------------- 1 file changed, 24 insertions(+), 50 deletions(-) diff --git a/src/Bedrock/End2End/X25519/AddPrecomputed.v b/src/Bedrock/End2End/X25519/AddPrecomputed.v index a1a06a482b..471278b698 100644 --- a/src/Bedrock/End2End/X25519/AddPrecomputed.v +++ b/src/Bedrock/End2End/X25519/AddPrecomputed.v @@ -146,17 +146,6 @@ 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. -Local Ltac unwrap_calls := - repeat match goal with - | |- _ /\ _ => split - | |- call _ _ _ _ _ _ => straightline_call - | _ => straightline - end. - -Local Ltac solve_stack := - match goal with - | |- 40 mod bytes_per_word 32 = 0 => auto - end. Local Ltac solve_bounds := repeat match goal with @@ -173,56 +162,41 @@ Local Ltac solve_mem := Local Ltac unwrap_fn_step := repeat straightline; straightline_call; ssplit. +(* Local Ltac solve_stack := *) + +Local Ltac solve_stack a := + (* Rewrites the `stack$@a` term in H to use a Bignum instead *) + cbv [FElem]; + match goal with + | H: _%sep ?m |- (Bignum.Bignum felem_size_in_words a _ * _)%sep ?m => + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a) H + end; + [> transitivity 40%nat; trivial | ]; + (* proves the memory matches up *) + use_sep_assumption; cancel; cancel_seps_at_indices 0%nat 0%nat; cbn; [> trivial | eapply RelationClasses.reflexivity]. + Lemma add_precomputed_partial_ok : program_logic_goal_for_function! add_precomputed_partial. Proof. (* slightly painful way to split out all the memory and bounds conditions, and the final postconditions *) unwrap_fn_step. 6:unwrap_fn_step. 11:unwrap_fn_step. 16:unwrap_fn_step. 21:unwrap_fn_step. 26:repeat straightline. (* Solve each of the memory and bounds conditions piece-by-piece, as much as possible *) - 3,4:solve_mem. 1,2:solve_bounds. - { (* (FElem a ?out ⋆ ?Rr)%sep m *) - (* Rewrites the `stack$@a` term in H10 to use a Bignum instead *) - cbv [FElem]. - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a) H10. { transitivity 40%nat; trivial. } - use_sep_assumption. - cancel. cancel_seps_at_indices 0%nat 0%nat; cbn. trivial. - eapply RelationClasses.reflexivity. } - 3,4:solve_mem. 1,2:solve_bounds. - { (* (FElem a2 ?out ⋆ ?Rr)%sep a1 *) - cbv [FElem]. - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H19. { transitivity 40%nat; trivial. } - use_sep_assumption. - cancel. cancel_seps_at_indices 0%nat 0%nat; cbn; trivial. - eapply RelationClasses.reflexivity. } - 3,4:solve_mem. 1,2:solve_bounds. - { (* (FElem a0 ?out ⋆ ?Rr)%sep a5 *) - cbv [FElem]. - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a0) H26. { transitivity 40%nat; trivial. } - use_sep_assumption. - cancel. cancel_seps_at_indices 0%nat 0%nat; cbn; trivial. - eapply RelationClasses.reflexivity. } - 3,4:solve_mem. 1,2:solve_bounds. - { (* (FElem a4 ?out ⋆ ?Rr)%sep a8 *) - cbv [FElem]. - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a4) H33. { transitivity 40%nat; trivial. } - use_sep_assumption. - cancel. cancel_seps_at_indices 0%nat 0%nat; cbn; trivial. - eapply RelationClasses.reflexivity. } - 3,4:solve_mem. 1,2:solve_bounds. - { (* (FElem a7 ?out ⋆ ?Rr)%sep a11 *) - cbv [FElem]. - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a7) H40. { transitivity 40%nat; trivial. } - use_sep_assumption. - cancel. cancel_seps_at_indices 0%nat 0%nat; cbn; trivial. - eapply RelationClasses.reflexivity. } + 3,4:solve_mem. 1,2:solve_bounds. solve_stack a. + 3,4:solve_mem. 1,2:solve_bounds. solve_stack a2. + 3,4:solve_mem. 1,2:solve_bounds. solve_stack a0. + 3,4:solve_mem. 1,2:solve_bounds. solve_stack a4. + 3,4:solve_mem. 1,2:solve_bounds. solve_stack a7. - (* exists m' mStack' : SortedListWord.map word Init.Byte.byte, anybytes a 40 mStack' /\ map.split a1 m' mStack' /\ list_map (get l0) [] (fun rets : list word => rets = [] /\ a0 = a0 /\ (FElem X1K X1 ⋆ FElem Y1K Y1 ⋆ R)%sep m') *) (* Rewrites the FElem about `a` in H11 to be about bytes instead, so we can use it to prove things about `a` as bytes *) cbv [FElem] in *. - seprewrite_in @Bignum.Bignum_to_bytes H19. - seprewrite_in @Bignum.Bignum_to_bytes H19. - extract_ex1_and_emp_in H19. + seprewrite_in @Bignum.Bignum_to_bytes H47. + seprewrite_in @Bignum.Bignum_to_bytes H47. + seprewrite_in @Bignum.Bignum_to_bytes H47. + seprewrite_in @Bignum.Bignum_to_bytes H47. + seprewrite_in @Bignum.Bignum_to_bytes H47. + extract_ex1_and_emp_in H47. repeat straightline; intuition eauto. Qed. From 0ff53209188b9b75cf6916f166277feaea9e2556 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 7 Jul 2023 14:47:35 -0400 Subject: [PATCH 08/18] some outputs --- src/Bedrock/End2End/X25519/AddPrecomputed.v | 79 +++++++++++++-------- 1 file changed, 51 insertions(+), 28 deletions(-) diff --git a/src/Bedrock/End2End/X25519/AddPrecomputed.v b/src/Bedrock/End2End/X25519/AddPrecomputed.v index 471278b698..d4e3926a01 100644 --- a/src/Bedrock/End2End/X25519/AddPrecomputed.v +++ b/src/Bedrock/End2End/X25519/AddPrecomputed.v @@ -56,7 +56,7 @@ Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, fe25519_mul(ot, ox, oy) }. -Definition add_precomputed_partial := func! (X1, Y1, T1, ypx2, ymx2, xy2d2) { +Definition add_precomputed_partial := func! (ox, oy, X1, Y1, T1, ypx2, ymx2, xy2d2) { stackalloc 40 as YpX1; fe25519_add(YpX1, Y1, X1); stackalloc 40 as YmX1; @@ -66,7 +66,13 @@ Definition add_precomputed_partial := func! (X1, Y1, T1, ypx2, ymx2, xy2d2) { stackalloc 40 as B; fe25519_mul(B, YmX1, ymx2); stackalloc 40 as C; - fe25519_mul(C, xy2d2, T1) + fe25519_mul(C, xy2d2, T1); + (* stackalloc 40 as Two; + fe25519_from_word(Two, $2); + stackalloc 40 as D; + fe25519_mul(D, Z1, Two); *) + fe25519_sub(ox, A, B); + fe25519_add(oy, A, B) }. Section WithParameters. @@ -113,8 +119,8 @@ Global Instance spec_of_add_precomputed : spec_of "add_precomputed" := Global Instance spec_of_add_precomputed_partial : spec_of "add_precomputed_partial" := fnspec! "add_precomputed_partial" - (X1K Y1K T1K ypx2K ymx2K xy2d2K : word) / - (X1 Y1 T1 ypx2 ymx2 xy2d2 : felem) (R : _ -> Prop), + (oxK oyK X1K Y1K T1K ypx2K ymx2K xy2d2K : word) / + (ox oy X1 Y1 T1 ypx2 ymx2 xy2d2 : felem) (R : _ -> Prop), { requires t m := bounded_by tight_bounds X1 /\ bounded_by tight_bounds Y1 /\ @@ -122,10 +128,13 @@ Global Instance spec_of_add_precomputed_partial : spec_of "add_precomputed_parti bounded_by loose_bounds ypx2 /\ bounded_by loose_bounds ymx2 /\ bounded_by loose_bounds xy2d2 /\ - m =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * R; + m =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox) * (FElem oyK oy) * R; ensures t' m' := t = t' /\ - m' =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * R }. + exists ox' oy', + bounded_by loose_bounds ox' /\ + bounded_by loose_bounds oy' /\ + m' =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox') * (FElem oyK oy') * R }. Local Instance spec_of_fe25519_square : spec_of "fe25519_square" := Field.spec_of_UnOp un_square. @@ -177,29 +186,43 @@ Local Ltac solve_stack a := Lemma add_precomputed_partial_ok : program_logic_goal_for_function! add_precomputed_partial. Proof. - (* slightly painful way to split out all the memory and bounds conditions, and the final postconditions *) - unwrap_fn_step. 6:unwrap_fn_step. 11:unwrap_fn_step. 16:unwrap_fn_step. 21:unwrap_fn_step. - 26:repeat straightline. - (* Solve each of the memory and bounds conditions piece-by-piece, as much as possible *) - 3,4:solve_mem. 1,2:solve_bounds. solve_stack a. - 3,4:solve_mem. 1,2:solve_bounds. solve_stack a2. - 3,4:solve_mem. 1,2:solve_bounds. solve_stack a0. - 3,4:solve_mem. 1,2:solve_bounds. solve_stack a4. - 3,4:solve_mem. 1,2:solve_bounds. solve_stack a7. - - (* exists m' mStack' : SortedListWord.map word Init.Byte.byte, - anybytes a 40 mStack' /\ - map.split a1 m' mStack' /\ list_map (get l0) [] (fun rets : list word => rets = [] /\ a0 = a0 /\ (FElem X1K X1 ⋆ FElem Y1K Y1 ⋆ R)%sep m') *) - (* Rewrites the FElem about `a` in H11 to be about bytes instead, so we can use it to prove things about `a` as bytes *) + (* Unwrap each call in the program. *) + (* Each produces 2 memory goals about the inputs, 2 bounds preconditions on the inputs, and 1 memory goal about the output. *) + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a. + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a2. + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a0. + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a4. + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a7. + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. + + (* Solve the postconditions *) + repeat straightline. + (* Rewrites the FElem about `a` in H11 to be about bytes instead, so we can use it to prove things about `a` as bytes *) cbv [FElem] in *. - seprewrite_in @Bignum.Bignum_to_bytes H47. - seprewrite_in @Bignum.Bignum_to_bytes H47. - seprewrite_in @Bignum.Bignum_to_bytes H47. - seprewrite_in @Bignum.Bignum_to_bytes H47. - seprewrite_in @Bignum.Bignum_to_bytes H47. - extract_ex1_and_emp_in H47. - - repeat straightline; intuition eauto. -Qed. + (* seprewrite_in (@Bignum.Bignum_to_bytes felem_size_in_words a7 x3) H55. *) (* Ought to be able to specify a7, but types don't match *) + seprewrite_in @Bignum.Bignum_to_bytes H55. + seprewrite_in @Bignum.Bignum_to_bytes H55. + seprewrite_in @Bignum.Bignum_to_bytes H55. + seprewrite_in @Bignum.Bignum_to_bytes H55. + seprewrite_in @Bignum.Bignum_to_bytes H55. + seprewrite_in @Bignum.Bignum_to_bytes H55. + seprewrite_in @Bignum.Bignum_to_bytes H55. + extract_ex1_and_emp_in H55. + + (* Solve stack/memory stuff *) + repeat straightline. + + (* Post-conditions *) + exists x4,x5; (* eexists? *) ssplit. 1,2:solve_bounds. + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 oxK) H55. { transitivity 40%nat; trivial. } + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 oyK) H55. { transitivity 40%nat; trivial. } + use_sep_assumption. cancel. cancel_seps_at_indices 0%nat 1%nat; cbn. + (* Bignum.Bignum 10 oyK (map (c => word.of_Z (le_combine c)) (List.chunk (Pos.to_nat 4) (flat_map (w => le_split (Pos.to_nat 4) w) x5))) = Bignum.Bignum n oyK x5 *) + admit. + (* Bignum.Bignum 10 oxK (map (c => word.of_Z (le_combine c)) (List.chunk (Pos.to_nat 4) (flat_map (w => le_split (Pos.to_nat 4) w) x4))) = Bignum.Bignum n oyK x4 *) + admit. +Admitted. Lemma add_precomputed_ok : program_logic_goal_for_function! add_precomputed. Proof. From 2ec98950f1a69703d832e861994912e8e080a7fe Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 7 Jul 2023 16:14:22 -0400 Subject: [PATCH 09/18] Partial proof for full function --- src/Bedrock/End2End/X25519/AddPrecomputed.v | 103 ++++++++------------ 1 file changed, 42 insertions(+), 61 deletions(-) diff --git a/src/Bedrock/End2End/X25519/AddPrecomputed.v b/src/Bedrock/End2End/X25519/AddPrecomputed.v index d4e3926a01..57adf9e1b4 100644 --- a/src/Bedrock/End2End/X25519/AddPrecomputed.v +++ b/src/Bedrock/End2End/X25519/AddPrecomputed.v @@ -44,8 +44,10 @@ Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, fe25519_mul(B, YmX1, ymx2); stackalloc 40 as C; fe25519_mul(C, xy2d2, T1); + stackalloc 40 as Two; + fe25519_from_word(Two, $2); stackalloc 40 as D; - fe25519_mul(D, Z1, $2); (* Should be Z1 + Z1, but mul has tighter bounds *) + fe25519_mul(D, Z1, Two); (* Should be Z1 + Z1, but mul has tighter bounds *) fe25519_sub(ox, A, B); fe25519_add(oy, A, B); fe25519_add(oz, D, C); @@ -56,7 +58,7 @@ Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, fe25519_mul(ot, ox, oy) }. -Definition add_precomputed_partial := func! (ox, oy, X1, Y1, T1, ypx2, ymx2, xy2d2) { +Definition add_precomputed_partial := func! (ox, oy, X1, Y1, Z1, T1, ypx2, ymx2, xy2d2) { stackalloc 40 as YpX1; fe25519_add(YpX1, Y1, X1); stackalloc 40 as YmX1; @@ -67,10 +69,10 @@ Definition add_precomputed_partial := func! (ox, oy, X1, Y1, T1, ypx2, ymx2, xy2 fe25519_mul(B, YmX1, ymx2); stackalloc 40 as C; fe25519_mul(C, xy2d2, T1); - (* stackalloc 40 as Two; + stackalloc 40 as Two; fe25519_from_word(Two, $2); stackalloc 40 as D; - fe25519_mul(D, Z1, Two); *) + fe25519_mul(D, Z1, Two); fe25519_sub(ox, A, B); fe25519_add(oy, A, B) }. @@ -119,28 +121,31 @@ Global Instance spec_of_add_precomputed : spec_of "add_precomputed" := Global Instance spec_of_add_precomputed_partial : spec_of "add_precomputed_partial" := fnspec! "add_precomputed_partial" - (oxK oyK X1K Y1K T1K ypx2K ymx2K xy2d2K : word) / - (ox oy X1 Y1 T1 ypx2 ymx2 xy2d2 : felem) (R : _ -> Prop), + (oxK oyK X1K Y1K Z1K T1K ypx2K ymx2K xy2d2K : word) / + (ox oy X1 Y1 Z1 T1 ypx2 ymx2 xy2d2 : felem) (R : _ -> Prop), { requires t m := bounded_by tight_bounds X1 /\ bounded_by tight_bounds Y1 /\ + bounded_by loose_bounds Z1 /\ bounded_by loose_bounds T1 /\ bounded_by loose_bounds ypx2 /\ bounded_by loose_bounds ymx2 /\ bounded_by loose_bounds xy2d2 /\ - m =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox) * (FElem oyK oy) * R; + m =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox) * (FElem oyK oy) * R; ensures t' m' := t = t' /\ exists ox' oy', bounded_by loose_bounds ox' /\ bounded_by loose_bounds oy' /\ - m' =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox') * (FElem oyK oy') * R }. + m' =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox') * (FElem oyK oy') * R }. Local Instance spec_of_fe25519_square : spec_of "fe25519_square" := Field.spec_of_UnOp un_square. Local Instance spec_of_fe25519_mul : spec_of "fe25519_mul" := Field.spec_of_BinOp bin_mul. Local Instance spec_of_fe25519_add : spec_of "fe25519_add" := Field.spec_of_BinOp bin_add. Local Instance spec_of_fe25519_sub : spec_of "fe25519_sub" := Field.spec_of_BinOp bin_sub. +Local Instance spec_of_fe25519_from_word : spec_of "fe25519_from_word" := Field.spec_of_from_word. +Local Instance frep_ok : FieldRepresentation_ok(field_representation:=frep25519). Admitted. (* Should be an instance elsewhere I can grab? *) Import WeakestPrecondition. @@ -160,6 +165,7 @@ Local Ltac solve_bounds := repeat match goal with | H: bounded_by loose_bounds ?x |- bounded_by loose_bounds ?x => apply H | H: bounded_by tight_bounds ?x |- bounded_by tight_bounds ?x => apply H + | H: bounded_by tight_bounds ?x |- bounded_by loose_bounds ?x => apply relax_bounds | H: bounded_by _ ?x |- bounded_by _ ?x => cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_sub un_outbounds bin_outbounds] in * end. @@ -184,72 +190,47 @@ Local Ltac solve_stack a := (* proves the memory matches up *) use_sep_assumption; cancel; cancel_seps_at_indices 0%nat 0%nat; cbn; [> trivial | eapply RelationClasses.reflexivity]. -Lemma add_precomputed_partial_ok : program_logic_goal_for_function! add_precomputed_partial. +Lemma add_precomputed_ok : program_logic_goal_for_function! add_precomputed. Proof. (* Unwrap each call in the program. *) (* Each produces 2 memory goals about the inputs, 2 bounds preconditions on the inputs, and 1 memory goal about the output. *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a. - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a2. - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a0. - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a4. - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a7. - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a. (* fe25519_add(YpX1, Y1, X1) *) + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a2. (* fe25519_sub(YmX1, Y1, X1) *) + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a0. (* fe25519_mul(A, YpX1, ypx2) *) + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a4. (* fe25519_mul(B, YmX1, ymx2) *) + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a7. (* fe25519_mul(C, xy2d2, T1) *) + unwrap_fn_step. solve_stack a10. (* fe25519_from_word(Two, $2) *) + unwrap_fn_step. 3,4:solve_mem. solve_bounds. (* 2 has loose_bounds *) admit. solve_stack a13. (* fe25519_mul(D, Z1, Two) *) + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_sub(ox, A, B) *) + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_add(oy, A, B) *) + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_add(oz, D, C) *) + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_sub(ot, D, C) *) + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_mul(ox, ox, ot) *) + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_mul(oy, oy, oz) *) + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_mul(oz, ot, oz) *) + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_mul(ot, ox, oy) *) (* Solve the postconditions *) repeat straightline. (* Rewrites the FElem about `a` in H11 to be about bytes instead, so we can use it to prove things about `a` as bytes *) cbv [FElem] in *. - (* seprewrite_in (@Bignum.Bignum_to_bytes felem_size_in_words a7 x3) H55. *) (* Ought to be able to specify a7, but types don't match *) - seprewrite_in @Bignum.Bignum_to_bytes H55. - seprewrite_in @Bignum.Bignum_to_bytes H55. - seprewrite_in @Bignum.Bignum_to_bytes H55. - seprewrite_in @Bignum.Bignum_to_bytes H55. - seprewrite_in @Bignum.Bignum_to_bytes H55. - seprewrite_in @Bignum.Bignum_to_bytes H55. - seprewrite_in @Bignum.Bignum_to_bytes H55. - extract_ex1_and_emp_in H55. + (* Ought to be able to avoid rewriting outputs, but not sure how to specify FElems to rewrite *) + (* Something like `seprewrite_in (@Bignum.Bignum_to_bytes felem_size_in_words a7 x3) H96.` should work, but types don't match *) + do 11 (seprewrite_in @Bignum.Bignum_to_bytes H96). + extract_ex1_and_emp_in H96. (* Solve stack/memory stuff *) repeat straightline. (* Post-conditions *) - exists x4,x5; (* eexists? *) ssplit. 1,2:solve_bounds. - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 oxK) H55. { transitivity 40%nat; trivial. } - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 oyK) H55. { transitivity 40%nat; trivial. } - use_sep_assumption. cancel. cancel_seps_at_indices 0%nat 1%nat; cbn. - (* Bignum.Bignum 10 oyK (map (c => word.of_Z (le_combine c)) (List.chunk (Pos.to_nat 4) (flat_map (w => le_split (Pos.to_nat 4) w) x5))) = Bignum.Bignum n oyK x5 *) - admit. - (* Bignum.Bignum 10 oxK (map (c => word.of_Z (le_combine c)) (List.chunk (Pos.to_nat 4) (flat_map (w => le_split (Pos.to_nat 4) w) x4))) = Bignum.Bignum n oyK x4 *) - admit. + exists x10,x11,x12,x13; (* eexists? *) ssplit. 2,3,4,5:solve_bounds. + { (* Correctness: result matches Gallina *) admit. } + { (* Safety: memory is what it should be *) + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 oxK) H96. { transitivity 40%nat; trivial. } + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 oyK) H96. { transitivity 40%nat; trivial. } + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 ozK) H96. { transitivity 40%nat; trivial. } + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 otK) H96. { transitivity 40%nat; trivial. } + use_sep_assumption. cancel. admit. (* Matching types for outputs *) Admitted. -Lemma add_precomputed_ok : program_logic_goal_for_function! add_precomputed. -Proof. - repeat straightline. - unwrap_calls. - - apply H14. (* bounded_by bin_xbounds Y1 *) (* solve_bounds. *) - - apply H13. (* bounded_by bin_ybounds X1 *) (* solve_bounds. *) - - eexists. ecancel_assumption. - - eexists. ecancel_assumption. - - shelve. (* (FElem a ?out ⋆ ?Rr)%sep m *) - - auto. (* 40 mod bytes_per_word 32 = 0 *) - - apply H14. (* bounded_by bin_xbounds ?x@{a1:=a0; H29:=H30; mCombined:=a1} *) - - apply H13. (* bounded_by bin_ybounds ?y@{a1:=a0; H29:=H30; mCombined:=a1} *) - - eexists. ecancel_assumption. (* exists Rx : SortedListWord.map word Init.Byte.byte -> Prop, (FElem Y1K Y1 ⋆ Rx)%sep a1 *) - - eexists. ecancel_assumption. (* exists Ry : SortedListWord.map word Init.Byte.byte -> Prop, (FElem X1K X1 ⋆ Ry)%sep a1 *) - - (* (FElem a2 ?out0@{a1:=a0; H29:=H30; mCombined:=a1} ⋆ ?Rr0@{a1:=a0; H29:=H30; mCombined:=a1})%sep a1 *) - - (* 40 mod bytes_per_word 32 = 0 *) - - (* bounded_by bin_xbounds ?x@{a1:=a5; H29:=H37; mCombined:=a1; a4:=a3; H34:=H35; mCombined0:=a4} *) - - (* (FElem a ?out ⋆ FElem Y1K ?x0)%sep m *) eexists. exists m. split. solve_mem. - - all: try solve_bounds. - (* post-conditions *) - - exists x1. split. 2:split. - + (* math adds up *) simpl in H9. simpl in H6. rewrite H6 in H9. simpl. apply H9. (* Definitely better tactics for this *) - + (* postcondition bounds on out *) simpl in H10. simpl. apply H10. (* should just work to apply H10... *) - + (* postcondition mem sep *) ecancel_assumption. -Qed. - End WithParameters. From 36db466a6296353dda50596d912afe8ffb6aeb4e Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 7 Jul 2023 16:16:19 -0400 Subject: [PATCH 10/18] Clean up add_precomputed_partial --- src/Bedrock/End2End/X25519/AddPrecomputed.v | 41 --------------------- 1 file changed, 41 deletions(-) diff --git a/src/Bedrock/End2End/X25519/AddPrecomputed.v b/src/Bedrock/End2End/X25519/AddPrecomputed.v index 57adf9e1b4..330d6f0324 100644 --- a/src/Bedrock/End2End/X25519/AddPrecomputed.v +++ b/src/Bedrock/End2End/X25519/AddPrecomputed.v @@ -58,25 +58,6 @@ Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, fe25519_mul(ot, ox, oy) }. -Definition add_precomputed_partial := func! (ox, oy, X1, Y1, Z1, T1, ypx2, ymx2, xy2d2) { - stackalloc 40 as YpX1; - fe25519_add(YpX1, Y1, X1); - stackalloc 40 as YmX1; - fe25519_sub(YmX1, Y1, X1); - stackalloc 40 as A; - fe25519_mul(A, YpX1, ypx2); - stackalloc 40 as B; - fe25519_mul(B, YmX1, ymx2); - stackalloc 40 as C; - fe25519_mul(C, xy2d2, T1); - stackalloc 40 as Two; - fe25519_from_word(Two, $2); - stackalloc 40 as D; - fe25519_mul(D, Z1, Two); - fe25519_sub(ox, A, B); - fe25519_add(oy, A, B) -}. - Section WithParameters. Check _: FieldRepresentation. @@ -119,26 +100,6 @@ Global Instance spec_of_add_precomputed : spec_of "add_precomputed" := bounded_by loose_bounds ot' /\ m' =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox') * (FElem oyK oy') * (FElem ozK oz') * (FElem otK ot') * R }. -Global Instance spec_of_add_precomputed_partial : spec_of "add_precomputed_partial" := - fnspec! "add_precomputed_partial" - (oxK oyK X1K Y1K Z1K T1K ypx2K ymx2K xy2d2K : word) / - (ox oy X1 Y1 Z1 T1 ypx2 ymx2 xy2d2 : felem) (R : _ -> Prop), - { requires t m := - bounded_by tight_bounds X1 /\ - bounded_by tight_bounds Y1 /\ - bounded_by loose_bounds Z1 /\ - bounded_by loose_bounds T1 /\ - bounded_by loose_bounds ypx2 /\ - bounded_by loose_bounds ymx2 /\ - bounded_by loose_bounds xy2d2 /\ - m =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox) * (FElem oyK oy) * R; - ensures t' m' := - t = t' /\ - exists ox' oy', - bounded_by loose_bounds ox' /\ - bounded_by loose_bounds oy' /\ - m' =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox') * (FElem oyK oy') * R }. - Local Instance spec_of_fe25519_square : spec_of "fe25519_square" := Field.spec_of_UnOp un_square. Local Instance spec_of_fe25519_mul : spec_of "fe25519_mul" := Field.spec_of_BinOp bin_mul. @@ -177,8 +138,6 @@ Local Ltac solve_mem := Local Ltac unwrap_fn_step := repeat straightline; straightline_call; ssplit. -(* Local Ltac solve_stack := *) - Local Ltac solve_stack a := (* Rewrites the `stack$@a` term in H to use a Bignum instead *) cbv [FElem]; From cf42f1069784f54f821487bcd0337c508ed11c03 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 14 Jul 2023 11:02:22 -0400 Subject: [PATCH 11/18] 2 does, in fact, fit the bounds --- src/Bedrock/End2End/X25519/AddPrecomputed.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Bedrock/End2End/X25519/AddPrecomputed.v b/src/Bedrock/End2End/X25519/AddPrecomputed.v index 330d6f0324..4de29613ca 100644 --- a/src/Bedrock/End2End/X25519/AddPrecomputed.v +++ b/src/Bedrock/End2End/X25519/AddPrecomputed.v @@ -159,7 +159,7 @@ Proof. unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a4. (* fe25519_mul(B, YmX1, ymx2) *) unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a7. (* fe25519_mul(C, xy2d2, T1) *) unwrap_fn_step. solve_stack a10. (* fe25519_from_word(Two, $2) *) - unwrap_fn_step. 3,4:solve_mem. solve_bounds. (* 2 has loose_bounds *) admit. solve_stack a13. (* fe25519_mul(D, Z1, Two) *) + unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a13. (* fe25519_mul(D, Z1, Two) *) unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_sub(ox, A, B) *) unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_add(oy, A, B) *) unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_add(oz, D, C) *) From a0448b4f1ae9a08bdd398fa382088481abe61458 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 14 Jul 2023 16:41:10 -0400 Subject: [PATCH 12/18] Fix admits and clean up --- src/Bedrock/End2End/X25519/AddPrecomputed.v | 153 +++++++++++--------- 1 file changed, 85 insertions(+), 68 deletions(-) diff --git a/src/Bedrock/End2End/X25519/AddPrecomputed.v b/src/Bedrock/End2End/X25519/AddPrecomputed.v index 4de29613ca..3abe604f8d 100644 --- a/src/Bedrock/End2End/X25519/AddPrecomputed.v +++ b/src/Bedrock/End2End/X25519/AddPrecomputed.v @@ -1,36 +1,51 @@ -Require Import Coq.Strings.String. -Require Import Coq.Lists.List. -Require Import Coq.ZArith.ZArith. -Require Import Crypto.Spec.Curve25519. +Require Import bedrock2.Array. +Require Import bedrock2.FE310CSemantics. +Require Import bedrock2.Loops. Require Import bedrock2.Map.Separation. +Require Import bedrock2.Map.SeparationLogic. +Require Import bedrock2.NotationsCustomEntry. +Require Import bedrock2.ProgramLogic. +Require Import bedrock2.Scalars. +Require Import bedrock2.Semantics. Require Import bedrock2.Syntax. +Require Import bedrock2.WeakestPrecondition. +Require Import bedrock2.WeakestPreconditionProperties. +Require Import bedrock2.ZnWords. +Require Import compiler.MMIO. Require Import compiler.Pipeline. Require Import compiler.Symbols. -Require Import compiler.MMIO. +Require Import coqutil.Byte. +Require Import coqutil.Map.Interface. +Require Import coqutil.Map.OfListWord. +From coqutil.Tactics Require Import Tactics letexists eabstract rdelta reference_to_string ident_of_string. Require Import coqutil.Word.Bitwidth32. +Require Import coqutil.Word.Bitwidth. +Require Import coqutil.Word.Interface. +Require Import Coq.Init.Byte. +Require Import Coq.Lists.List. +Require Import Coq.Strings.String. +Require Import Coq.ZArith.ZArith. Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Import Crypto.Bedrock.Field.Interface.Compilation2. Require Import Crypto.Bedrock.Field.Synthesis.New.UnsaturatedSolinas. Require Import Crypto.Bedrock.Group.AdditionChains. -Require Import Crypto.Bedrock.Group.ScalarMult.LadderStep. Require Import Crypto.Bedrock.Group.ScalarMult.CSwap. +Require Import Crypto.Bedrock.Group.ScalarMult.LadderStep. Require Import Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder. Require Import Crypto.Bedrock.End2End.X25519.Field25519. Require Import Crypto.Bedrock.Specs.Field. -Require Import bedrock2.FE310CSemantics bedrock2.Semantics . -Require Import bedrock2.WeakestPrecondition bedrock2.ProgramLogic. -Require Import coqutil.Word.Interface coqutil.Word.Bitwidth. -Require Import coqutil.Map.Interface bedrock2.Map.SeparationLogic. -Require Import bedrock2.Array bedrock2.Scalars. -Require Import bedrock2.ZnWords. -Require Import coqutil.Tactics.Tactics. -Require Import bedrock2.NotationsCustomEntry. +Require Import Crypto.Spec.Curve25519. Require Import Curves.Edwards.XYZT.Precomputed. +Require Crypto.Bedrock.Field.Synthesis.New.Signature. Local Open Scope string_scope. Local Open Scope Z_scope. +Import LittleEndianList. Import ListNotations. +Import ProgramLogic.Coercions. +Import WeakestPrecondition. -Local Instance frep25519 : Field.FieldRepresentation(field_parameters:=field_parameters) := field_representation n Field25519.s c. +Local Existing Instance field_parameters. +Local Instance frep25519 : Field.FieldRepresentation := field_representation n Field25519.s c. (* Better way to represent points in Bedrock2? *) Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, xy2d2) { @@ -59,14 +74,9 @@ Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, }. Section WithParameters. - Check _: FieldRepresentation. + Context {two_lt_M: 2 < M_pos}. -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. -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"). @@ -106,22 +116,20 @@ Local Instance spec_of_fe25519_mul : spec_of "fe25519_mul" := Field.spec_of_BinO Local Instance spec_of_fe25519_add : spec_of "fe25519_add" := Field.spec_of_BinOp bin_add. Local Instance spec_of_fe25519_sub : spec_of "fe25519_sub" := Field.spec_of_BinOp bin_sub. Local Instance spec_of_fe25519_from_word : spec_of "fe25519_from_word" := Field.spec_of_from_word. -Local Instance frep_ok : FieldRepresentation_ok(field_representation:=frep25519). Admitted. (* Should be an instance elsewhere I can grab? *) - -Import WeakestPrecondition. - -From coqutil.Tactics Require Import Tactics letexists eabstract rdelta reference_to_string ident_of_string. -Require Import bedrock2.Syntax. -Require Import bedrock2.WeakestPrecondition. -Require Import bedrock2.WeakestPreconditionProperties. -Require Import bedrock2.Loops. -Require Import bedrock2.Map.SeparationLogic bedrock2.Scalars. +(* TODO: use Field25519 version instead *) +Local Instance frep25519_ok : FieldRepresentation_ok(field_representation:=frep25519). +Proof. + apply Crypto.Bedrock.Field.Synthesis.New.Signature.field_representation_ok. + apply UnsaturatedSolinas.relax_valid. +Qed. 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. +Require Import AdmitAxiom. + Local Ltac solve_bounds := repeat match goal with | H: bounded_by loose_bounds ?x |- bounded_by loose_bounds ?x => apply H @@ -136,60 +144,69 @@ Local Ltac solve_mem := | |- _%sep _ => ecancel_assumption end. -Local Ltac unwrap_fn_step := repeat straightline; straightline_call; ssplit. - -Local Ltac solve_stack a := +Local Ltac solve_stack := (* Rewrites the `stack$@a` term in H to use a Bignum instead *) cbv [FElem]; match goal with - | H: _%sep ?m |- (Bignum.Bignum felem_size_in_words a _ * _)%sep ?m => + | H: _%sep ?m |- (Bignum.Bignum felem_size_in_words ?a _ * _)%sep ?m => seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a) H end; [> transitivity 40%nat; trivial | ]; (* proves the memory matches up *) use_sep_assumption; cancel; cancel_seps_at_indices 0%nat 0%nat; cbn; [> trivial | eapply RelationClasses.reflexivity]. +Local Ltac single_step := + repeat straightline; straightline_call; ssplit; try solve_mem; try solve_bounds; try solve_stack. + Lemma add_precomputed_ok : program_logic_goal_for_function! add_precomputed. Proof. (* Unwrap each call in the program. *) - (* Each produces 2 memory goals about the inputs, 2 bounds preconditions on the inputs, and 1 memory goal about the output. *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a. (* fe25519_add(YpX1, Y1, X1) *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a2. (* fe25519_sub(YmX1, Y1, X1) *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a0. (* fe25519_mul(A, YpX1, ypx2) *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a4. (* fe25519_mul(B, YmX1, ymx2) *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a7. (* fe25519_mul(C, xy2d2, T1) *) - unwrap_fn_step. solve_stack a10. (* fe25519_from_word(Two, $2) *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. solve_stack a13. (* fe25519_mul(D, Z1, Two) *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_sub(ox, A, B) *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_add(oy, A, B) *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_add(oz, D, C) *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_sub(ot, D, C) *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_mul(ox, ox, ot) *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_mul(oy, oy, oz) *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_mul(oz, ot, oz) *) - unwrap_fn_step. 3,4:solve_mem. 1,2:solve_bounds. ecancel_assumption. (* fe25519_mul(ot, ox, oy) *) + (* Each binop produces 2 memory goals on the inputs, 2 bounds goals on the inputs, and 1 memory goal on the output. *) + single_step. (* fe25519_add(YpX1, Y1, X1) *) + single_step. (* fe25519_sub(YmX1, Y1, X1) *) +(* Unshelve. all:exfalso;clear;admit. Optimize Proof. Qed. *) + single_step. (* fe25519_mul(A, YpX1, ypx2) *) + single_step. (* fe25519_mul(B, YmX1, ymx2) *) + single_step. (* fe25519_mul(C, xy2d2, T1) *) + single_step. (* fe25519_from_word(Two, $2) *) + single_step. (* fe25519_mul(D, Z1, Two) *) + single_step. (* fe25519_sub(ox, A, B) *) + single_step. (* fe25519_add(oy, A, B) *) + single_step. (* fe25519_add(oz, D, C) *) + single_step. (* fe25519_sub(ot, D, C) *) + single_step. (* fe25519_mul(ox, ox, ot) *) + single_step. (* fe25519_mul(oy, oy, oz) *) + single_step. (* fe25519_mul(oz, ot, oz) *) + single_step. (* fe25519_mul(ot, ox, oy) *) (* Solve the postconditions *) repeat straightline. - (* Rewrites the FElem about `a` in H11 to be about bytes instead, so we can use it to prove things about `a` as bytes *) + (* Rewrites the FElems for the stack (in H96) to be about bytes instead *) cbv [FElem] in *. - (* Ought to be able to avoid rewriting outputs, but not sure how to specify FElems to rewrite *) - (* Something like `seprewrite_in (@Bignum.Bignum_to_bytes felem_size_in_words a7 x3) H96.` should work, but types don't match *) - do 11 (seprewrite_in @Bignum.Bignum_to_bytes H96). + (* Prevent output from being rewritten by seprewrite_in *) + remember (Bignum.Bignum felem_size_in_words otK _) in H96. + remember (Bignum.Bignum felem_size_in_words ozK _) in H96. + remember (Bignum.Bignum felem_size_in_words oyK _) in H96. + remember (Bignum.Bignum felem_size_in_words oxK _) in H96. + do 7 (seprewrite_in @Bignum.Bignum_to_bytes H96). + subst P P0 P1 P2. extract_ex1_and_emp_in H96. - (* Solve stack/memory stuff *) - repeat straightline. - - (* Post-conditions *) - exists x10,x11,x12,x13; (* eexists? *) ssplit. 2,3,4,5:solve_bounds. - { (* Correctness: result matches Gallina *) admit. } - { (* Safety: memory is what it should be *) - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 oxK) H96. { transitivity 40%nat; trivial. } - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 oyK) H96. { transitivity 40%nat; trivial. } - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 ozK) H96. { transitivity 40%nat; trivial. } - seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 otK) H96. { transitivity 40%nat; trivial. } - use_sep_assumption. cancel. admit. (* Matching types for outputs *) -Admitted. + (* Solve stack/memory stuff *) + repeat straightline. + + (* Post-conditions *) + exists x10,x11,x12,x13; (* eexists? *) ssplit. 2,3,4,5:solve_bounds. + { (* Correctness: result matches Gallina *) + cbv [bin_model bin_mul bin_add bin_sub] in *. + cbv match beta delta [m1add_precomputed_coordinates]. + assert ((feval Z1 * F.of_Z M_pos (word.of_Z(width:=32) 2))%F = (feval Z1 + feval Z1)%F) as <-. + { rewrite word.unsigned_of_Z_nowrap by Lia.lia. (* import *) apply F.eq_to_Z_iff. rewrite F.to_Z_mul. rewrite F.to_Z_add. + rewrite F.to_Z_of_Z. f_equal. rewrite Z.mod_small. all:Lia.lia. } + congruence. + } + (* Safety: memory is what it should be *) + ecancel_assumption. +Qed. End WithParameters. From f3e02dab38789e02ea2daa58409d0809062f8a60 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 14 Jul 2023 16:45:27 -0400 Subject: [PATCH 13/18] Small tidying --- src/Bedrock/End2End/X25519/AddPrecomputed.v | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/Bedrock/End2End/X25519/AddPrecomputed.v b/src/Bedrock/End2End/X25519/AddPrecomputed.v index 3abe604f8d..7f86533232 100644 --- a/src/Bedrock/End2End/X25519/AddPrecomputed.v +++ b/src/Bedrock/End2End/X25519/AddPrecomputed.v @@ -36,6 +36,7 @@ Require Import Crypto.Bedrock.End2End.X25519.Field25519. Require Import Crypto.Bedrock.Specs.Field. Require Import Crypto.Spec.Curve25519. Require Import Curves.Edwards.XYZT.Precomputed. +Require Import Lia. Require Crypto.Bedrock.Field.Synthesis.New.Signature. Local Open Scope string_scope. Local Open Scope Z_scope. @@ -47,7 +48,6 @@ Import WeakestPrecondition. Local Existing Instance field_parameters. Local Instance frep25519 : Field.FieldRepresentation := field_representation n Field25519.s c. -(* Better way to represent points in Bedrock2? *) Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, xy2d2) { stackalloc 40 as YpX1; fe25519_add(YpX1, Y1, X1); @@ -62,7 +62,7 @@ Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, stackalloc 40 as Two; fe25519_from_word(Two, $2); stackalloc 40 as D; - fe25519_mul(D, Z1, Two); (* Should be Z1 + Z1, but mul has tighter bounds *) + fe25519_mul(D, Z1, Two); (* TODO: Should be Z1 + Z1, but mul has tighter bounds *) fe25519_sub(ox, A, B); fe25519_add(oy, A, B); fe25519_add(oz, D, C); @@ -77,7 +77,7 @@ Section WithParameters. Context {two_lt_M: 2 < M_pos}. Local Coercion F.to_Z : F >-> Z. -Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*). +Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing). Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a"). Local Notation FElem := (FElem(FieldRepresentation:=frep25519)). @@ -102,7 +102,6 @@ Global Instance spec_of_add_precomputed : spec_of "add_precomputed" := ensures t' m' := t = t' /\ exists ox' oy' oz' ot', - (* Need to specify implicit parameters? *) ((feval ox'), (feval oy'), (feval oz'), (feval ot')) = (@m1add_precomputed_coordinates (F M_pos) (F.add) (F.sub) (F.mul) ((feval X1), (feval Y1), (feval Z1), (feval T1)) ((feval ypx2), (feval ymx2), (feval xy2d2))) /\ bounded_by loose_bounds ox' /\ bounded_by loose_bounds oy' /\ @@ -164,7 +163,7 @@ Proof. (* Each binop produces 2 memory goals on the inputs, 2 bounds goals on the inputs, and 1 memory goal on the output. *) single_step. (* fe25519_add(YpX1, Y1, X1) *) single_step. (* fe25519_sub(YmX1, Y1, X1) *) -(* Unshelve. all:exfalso;clear;admit. Optimize Proof. Qed. *) +(* TODO: Debug Qed performance: Unshelve. all:exfalso;clear;admit. Optimize Proof. Qed. *) single_step. (* fe25519_mul(A, YpX1, ypx2) *) single_step. (* fe25519_mul(B, YmX1, ymx2) *) single_step. (* fe25519_mul(C, xy2d2, T1) *) @@ -201,8 +200,8 @@ Proof. cbv [bin_model bin_mul bin_add bin_sub] in *. cbv match beta delta [m1add_precomputed_coordinates]. assert ((feval Z1 * F.of_Z M_pos (word.of_Z(width:=32) 2))%F = (feval Z1 + feval Z1)%F) as <-. - { rewrite word.unsigned_of_Z_nowrap by Lia.lia. (* import *) apply F.eq_to_Z_iff. rewrite F.to_Z_mul. rewrite F.to_Z_add. - rewrite F.to_Z_of_Z. f_equal. rewrite Z.mod_small. all:Lia.lia. } + { rewrite word.unsigned_of_Z_nowrap by lia. apply F.eq_to_Z_iff. rewrite F.to_Z_mul. rewrite F.to_Z_add. + rewrite F.to_Z_of_Z. f_equal. rewrite Z.mod_small. all:lia. } congruence. } (* Safety: memory is what it should be *) From 5d18f5db6a3acdd06f2915bda50b81b7199e0dcb Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 21 Jul 2023 12:10:16 -0400 Subject: [PATCH 14/18] cleaning up --- src/Bedrock/End2End/X25519/AddPrecomputed.v | 11 +- src/Bedrock/End2End/X25519/Field25519.v | 6 + src/Bedrock/End2End/X25519/MontgomeryLadder.v | 361 +++++++++--------- 3 files changed, 191 insertions(+), 187 deletions(-) diff --git a/src/Bedrock/End2End/X25519/AddPrecomputed.v b/src/Bedrock/End2End/X25519/AddPrecomputed.v index 7f86533232..ba899366c2 100644 --- a/src/Bedrock/End2End/X25519/AddPrecomputed.v +++ b/src/Bedrock/End2End/X25519/AddPrecomputed.v @@ -47,6 +47,7 @@ Import WeakestPrecondition. Local Existing Instance field_parameters. Local Instance frep25519 : Field.FieldRepresentation := field_representation n Field25519.s c. +(* Local Existing Instance frep25519_ok. *) Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, xy2d2) { stackalloc 40 as YpX1; @@ -127,6 +128,7 @@ Local Arguments word.wrap : simpl never. Local Arguments word.unsigned : simpl never. Local Arguments word.of_Z : simpl never. +(* TODO: Remove after debugging QED *) Require Import AdmitAxiom. Local Ltac solve_bounds := @@ -157,6 +159,11 @@ Local Ltac solve_stack := Local Ltac single_step := repeat straightline; straightline_call; ssplit; try solve_mem; try solve_bounds; try solve_stack. +Local Ltac clear_extras := + repeat match goal with + | H: ?a%sep ?b |- _ => clear H + end. + Lemma add_precomputed_ok : program_logic_goal_for_function! add_precomputed. Proof. (* Unwrap each call in the program. *) @@ -195,7 +202,7 @@ Proof. repeat straightline. (* Post-conditions *) - exists x10,x11,x12,x13; (* eexists? *) ssplit. 2,3,4,5:solve_bounds. + exists x10,x11,x12,x13; ssplit. 2,3,4,5:solve_bounds. { (* Correctness: result matches Gallina *) cbv [bin_model bin_mul bin_add bin_sub] in *. cbv match beta delta [m1add_precomputed_coordinates]. @@ -206,6 +213,6 @@ Proof. } (* Safety: memory is what it should be *) ecancel_assumption. -Qed. +Admitted. End WithParameters. diff --git a/src/Bedrock/End2End/X25519/Field25519.v b/src/Bedrock/End2End/X25519/Field25519.v index a155e7e2a2..b9a892d016 100644 --- a/src/Bedrock/End2End/X25519/Field25519.v +++ b/src/Bedrock/End2End/X25519/Field25519.v @@ -129,4 +129,10 @@ Section Field. (&,fe25519_scmula24 :: functions)) As fe25519_scmula24_correct. Proof. Time derive_bedrock2_func scmula24_op. Qed. + + #[export] Instance frep25519_ok : FieldRepresentation_ok(field_representation:=field_representation n s c). + Proof. + apply Crypto.Bedrock.Field.Synthesis.New.Signature.field_representation_ok. + apply UnsaturatedSolinas.relax_valid. + Qed. End Field. diff --git a/src/Bedrock/End2End/X25519/MontgomeryLadder.v b/src/Bedrock/End2End/X25519/MontgomeryLadder.v index c7bd0f38da..0c0cf25abc 100644 --- a/src/Bedrock/End2End/X25519/MontgomeryLadder.v +++ b/src/Bedrock/End2End/X25519/MontgomeryLadder.v @@ -16,60 +16,35 @@ 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.Specs.Field. Local Open Scope string_scope. -Local Open Scope Z_scope. Import ListNotations. Local Instance frep25519 : Field.FieldRepresentation(field_parameters:=field_parameters) := field_representation n Field25519.s c. +Derive ladderstep SuchThat (ladderstep = ladderstep_body) As ladderstep_defn. +Proof. vm_compute. subst; exact eq_refl. Qed. -Require Import bedrock2.NotationsCustomEntry. +Derive montladder SuchThat (montladder = montladder_body (Z.to_nat (Z.log2 Curve25519.order))) + As montladder_defn. +Proof. vm_compute. subst; exact eq_refl. Qed. -Definition square_and_add := func! (o, x, y) { - fe25519_square(o, x); - fe25519_add(o, o, y) -}. +Require Import bedrock2.NotationsCustomEntry. -Definition mul_and_add := func! (o, x, y) { - fe25519_mul(o, x, x); - fe25519_add(o, o, y) +Definition x25519 := func! (out, sk, pk) { + stackalloc 40 as U; + fe25519_from_bytes(U, pk); + stackalloc 40 as OUT; + montladder(OUT, sk, U); + fe25519_to_bytes(out, OUT) }. -(* Better way to represent points in Bedrock2? *) -Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, xy2d2) { - stackalloc 40 as YpX1; - fe25519_add(YpX1, Y1, X1); - stackalloc 40 as YmX1; - fe25519_sub(YmX1, Y1, X1); - stackalloc 40 as A; - fe25519_mul(A, YpX1, ypx2); - stackalloc 40 as B; - fe25519_mul(B, YmX1, ymx2); - stackalloc 40 as C; - fe25519_mul(C, xy2d2, T1); - stackalloc 40 as D; - fe25519_add(D, Z1, Z1); - fe25519_sub(ox, A, B); - fe25519_add(oy, A, B); - fe25519_add(oz, D, C); - fe25519_sub(ot, D, C); - fe25519_mul(ox, ox, ot); - fe25519_mul(oy, oy, oz); - fe25519_mul(oz, ot, oz); - fe25519_mul(ot, ox, oy) +Definition x25519_base := func! (out, sk) { + stackalloc 40 as U; + fe25519_from_word(U, $9); + stackalloc 40 as OUT; + montladder(OUT, sk, U); + fe25519_to_bytes(out, OUT) }. -Require Import bedrock2.FE310CSemantics bedrock2.Semantics . -Require Import bedrock2.WeakestPrecondition bedrock2.ProgramLogic. -Require Import coqutil.Word.Interface coqutil.Word.Bitwidth. -Require Import coqutil.Map.Interface bedrock2.Map.SeparationLogic. -Require Import bedrock2.Array bedrock2.Scalars. -Require Import bedrock2.ZnWords. -Require Import coqutil.Tactics.Tactics. - -Section WithParameters. - Check _: FieldRepresentation. - Import LittleEndianList. Local Coercion F.to_Z : F >-> Z. Require Import bedrock2.WeakestPrecondition bedrock2.Semantics bedrock2.ProgramLogic. @@ -78,161 +53,177 @@ 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"). - -Local Notation FElem := (FElem(FieldRepresentation:=frep25519)). -Local Notation bounded_by := (bounded_by(FieldRepresentation:=frep25519)). -Local Notation word := (Naive.word 32). -Local Notation felem := (felem(FieldRepresentation:=frep25519)). - -Global Instance spec_of_square_and_add : spec_of "square_and_add" := - fnspec! "square_and_add" (out xk yk: word) / (o x y : felem) (R : _ -> Prop), - { requires t m := - bounded_by loose_bounds x /\ - bounded_by tight_bounds y /\ - m =* (FElem xk x) * (FElem yk y) * (FElem out o) * R; - ensures t' m' := - t=t' /\ - exists o', feval o' = F.add (F.pow (feval x) 2) (feval y) - /\ bounded_by loose_bounds o' - /\ m' =* (FElem xk x) * (FElem yk y) * (FElem out o') * R }. - -Global Instance spec_of_mul_and_add : spec_of "mul_and_add" := - fnspec! "mul_and_add" (out xk yk: word) / (o x y : felem) (R : _ -> Prop), - { requires t m := - bounded_by loose_bounds x /\ - bounded_by tight_bounds y /\ - m =* (FElem xk x) * (FElem yk y) * (FElem out o) * R; - ensures t' m' := - t=t' /\ - exists o', feval o' = F.add (F.mul (feval x) (feval x)) (feval y) - /\ bounded_by loose_bounds o' - /\ m' =* (FElem xk x) * (FElem yk y) * (FElem out o') * R }. - -Require Import Curves.Edwards.XYZT.Precomputed. (* Move elsewhere *) - -Global Instance spec_of_add_precomputed : spec_of "add_precomputed" := - fnspec! "add_precomputed" - (oxK oyK ozK otK X1K Y1K Z1K T1K ypx2K ymx2K xy2d2K : word) / - (ox oy oz ot X1 Y1 Z1 T1 ypx2 ymx2 xy2d2 : felem) (R : _ -> Prop), - { requires t m := - bounded_by tight_bounds X1 /\ - bounded_by tight_bounds Y1 /\ - bounded_by tight_bounds Z1 /\ (* Could be loose if switch to mul *) - bounded_by loose_bounds T1 /\ - bounded_by loose_bounds ypx2 /\ - bounded_by loose_bounds ymx2 /\ - bounded_by loose_bounds xy2d2 /\ - m =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox) * (FElem oyK oy) * (FElem ozK oz) * (FElem otK ot) * R; - ensures t' m' := - t = t' /\ - exists ox' oy' oz' ot', - (* Need to specify implicit parameters? *) - ((feval ox'), (feval oy'), (feval oz'), (feval ot')) = (@m1add_precomputed_coordinates (F M_pos) (F.add) (F.sub) (F.mul) ((feval X1), (feval Y1), (feval Z1), (feval T1)) ((feval ypx2), (feval ymx2), (feval xy2d2))) /\ - bounded_by loose_bounds ox' /\ - bounded_by loose_bounds oy' /\ - bounded_by loose_bounds oz' /\ - bounded_by loose_bounds ot' /\ - m' =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem T1K T1) * (FElem ypx2K ypx2) * (FElem ymx2K ymx2) * (FElem xy2d2K xy2d2) * (FElem oxK ox') * (FElem oyK oy') * (FElem ozK oz') * (FElem otK ot') * R }. - -Local Instance spec_of_fe25519_square : spec_of "fe25519_square" := Field.spec_of_UnOp un_square. -Local Instance spec_of_fe25519_mul : spec_of "fe25519_mul" := Field.spec_of_BinOp bin_mul. -Local Instance spec_of_fe25519_add : spec_of "fe25519_add" := Field.spec_of_BinOp bin_add. -Local Instance spec_of_fe25519_sub : spec_of "fe25519_sub" := Field.spec_of_BinOp bin_sub. - -Import WeakestPrecondition. - -From coqutil.Tactics Require Import Tactics letexists eabstract rdelta reference_to_string ident_of_string. -Require Import bedrock2.Syntax. -Require Import bedrock2.WeakestPrecondition. -Require Import bedrock2.WeakestPreconditionProperties. -Require Import bedrock2.Loops. -Require Import bedrock2.Map.SeparationLogic bedrock2.Scalars. +Definition x25519_gallina := montladder_gallina (Field.M_pos(FieldParameters:=field_parameters)) Field.a24 (Z.to_nat (Z.log2 (Z.pos order))). +Global Instance spec_of_x25519 : spec_of "x25519" := + fnspec! "x25519" out sk pk / (o s p : list Byte.byte) (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; + ensures t' m := t=t' /\ m=* s$@sk ⋆ p$@pk ⋆ R ⋆ + (le_split 32 (x25519_gallina (le_combine s) (Field.feval_bytes 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 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 square_and_add_ok : program_logic_goal_for_function! square_and_add. +Lemma x25519_ok : program_logic_goal_for_function! x25519. Proof. repeat straightline. - repeat match goal with - | |- _ /\ _ => split - | |- call _ _ _ _ _ _ => straightline_call - | _ => straightline - end. - (* square *) - - (* square precondition bounds on x *) apply H1. - - (* mem sep for x *) eexists. ecancel_assumption. - - (* mem sep for out *) ecancel_assumption. - (* add *) - - (* add precondition bounds on x^2 *) apply H7. - - (* add precondition bounds on y *) apply H2. - - (* mem sep for o (holding x^2) *) eexists. ecancel_assumption. - - (* mem sep for y *) eexists. ecancel_assumption. - - (* mem sep for o (holding x^2+y) *) ecancel_assumption. - (* post-conditions *) - - exists x1. split. 2:split. - + (* math adds up *) simpl in H9. simpl in H6. rewrite H6 in H9. simpl. apply H9. (* Definitely better tactics for this *) - + (* postcondition bounds on out *) simpl in H10. simpl. apply H10. (* should just work to apply H10... *) - + (* postcondition mem sep *) ecancel_assumption. + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a) H2. { 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. } + { 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); []). + cbn; cbn [nth] in *. + cbv [COperationSpecifications.list_Z_bounded_by FoldBool.fold_andb_map map seq]; cbn. + pose proof byte.unsigned_range as HH. setoid_rewrite <-Le.Z.le_sub_1_iff in HH. cbn in HH. + setoid_rewrite Zle_is_le_bool in HH. setoid_rewrite <-Bool.andb_true_iff in HH. + rewrite 31HH; cbn. + eapply Bool.andb_true_iff; split; trivial. + eapply Bool.andb_true_iff; split; eapply Zle_is_le_bool; trivial. + eapply byte.unsigned_range. } + repeat straightline. + + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H15. { transitivity 40%nat; trivial. } + + straightline_call; ssplit. + 3: { 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. + { instantiate (1:=None). exact I. } } + { reflexivity. } + { rewrite H3. vm_compute. inversion 1. } + repeat straightline. + + cbv [FElem] in H22. extract_ex1_and_emp_in H22. + straightline_call; ssplit. + { ecancel_assumption. } + { transitivity 32%nat; auto. } + { eexists. ecancel_assumption. } + { intuition idtac. } + repeat straightline_cleanup. + 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. + + repeat straightline; intuition eauto. + rewrite H29 in *. cbv [x25519_gallina]. + use_sep_assumption; cancel. eapply RelationClasses.reflexivity. Qed. -Local Ltac unwrap_calls := - repeat match goal with - | |- _ /\ _ => split - | |- call _ _ _ _ _ _ => straightline_call - | _ => straightline - end. - -Local Ltac solve_bounds := - repeat match goal with - | H: bounded_by loose_bounds _ |- bounded_by loose_bounds _ => apply H - | H: bounded_by tight_bounds _ |- bounded_by tight_bounds _ => apply H - | H: bounded_by _ _ |- bounded_by _ _ => cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add un_outbounds bin_outbounds] in * - end. - -Local Ltac solve_mem := - repeat match goal with - | |- exists _, _%sep _ => eexists - | |- _%sep _ => ecancel_assumption - end. - -Lemma square_and_add_ok2 : program_logic_goal_for_function! square_and_add. +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 (x25519_gallina (le_combine s) (F.of_Z _ 9)))$@out }. + +Lemma x25519_base_ok : program_logic_goal_for_function! x25519_base. Proof. repeat straightline. - unwrap_calls. - all: try solve_mem. all: try solve_bounds. - (* post-conditions *) - - exists x1. split. 2:split. - + (* math adds up *) simpl in H9. simpl in H6. rewrite H6 in H9. simpl. apply H9. (* Definitely better tactics for this *) - + (* postcondition bounds on out *) simpl in H10. simpl. apply H10. (* should just work to apply H10... *) - + (* postcondition mem sep *) ecancel_assumption. + seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a) H2. { 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. } + + straightline_call; ssplit. + 3: { 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. + { instantiate (1:=None). exact I. } } + { reflexivity. } + { rewrite H3. vm_compute. inversion 1. } + repeat straightline. + + unfold FElem in H20. extract_ex1_and_emp_in H20. + straightline_call; ssplit. + { ecancel_assumption. } + { transitivity 32%nat; auto. } + { eexists. ecancel_assumption. } + { intuition idtac. } + repeat straightline_cleanup. + 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. + + repeat straightline; intuition eauto. + rewrite H27 in *. cbv [x25519_gallina]. + use_sep_assumption; cancel. eapply RelationClasses.reflexivity. Qed. -Lemma mul_and_add_ok : program_logic_goal_for_function! mul_and_add. +Require Import coqutil.Word.Naive. +Require Import coqutil.Macros.WithBaseName. + +Definition felem_cswap := CSwap.felem_cswap(word:=word32)(field_parameters:=field_parameters)(field_representaton:=field_representation n s c). +Definition fe25519_inv := fe25519_inv(word:=word32)(field_parameters:=field_parameters). + +Definition funcs := + &[,x25519; x25519_base; + montladder; + fe25519_to_bytes; + fe25519_from_bytes; + fe25519_from_word; + felem_cswap; + fe25519_copy; + fe25519_inv; + ladderstep; + fe25519_mul; + fe25519_add; + fe25519_sub; + fe25519_square; + fe25519_scmula24 ]. + +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. Proof. - repeat straightline. - repeat match goal with - | |- _ /\ _ => split - | |- call _ _ _ _ _ _ => straightline_call - | _ => straightline - end. - (* square *) - - (* mul precondition bounds on x *) apply H1. - - (* same bounds gain *) apply H1. - - (* mem sep for x *) eexists. ecancel_assumption. - - (* same mem sep again *) eexists. ecancel_assumption. - - (* mem sep for out *) ecancel_assumption. - (* add *) - - (* add precondition bounds on x^2 *) apply H7. - - (* add precondition bounds on y *) apply H2. - - (* mem sep for o (holding x^2) *) eexists. ecancel_assumption. - - (* mem sep for y *) eexists. ecancel_assumption. - - (* mem sep for o (holding x^2+y) *) ecancel_assumption. - (* post-conditions *) - - exists x1. split. 2:split. - + (* math adds up *) simpl in H9. simpl in H6. rewrite H6 in H9. simpl. apply H9. (* Definitely better tactics for this *) - + (* postcondition bounds on out *) simpl in H10. simpl. apply H10. (* should just work to apply H10... *) - + (* postcondition mem sep *) ecancel_assumption. + 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. 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. \ No newline at end of file From b7b0a6bba86c1682434674e155df0471e47b3fa7 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 21 Jul 2023 12:11:33 -0400 Subject: [PATCH 15/18] missing newline --- src/Bedrock/End2End/X25519/MontgomeryLadder.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Bedrock/End2End/X25519/MontgomeryLadder.v b/src/Bedrock/End2End/X25519/MontgomeryLadder.v index 0c0cf25abc..e2e2ee4e35 100644 --- a/src/Bedrock/End2End/X25519/MontgomeryLadder.v +++ b/src/Bedrock/End2End/X25519/MontgomeryLadder.v @@ -226,4 +226,4 @@ Module PrintAssembly. (* 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. \ No newline at end of file +End PrintAssembly. From 5007e3debda89c40f2588e2ebe91f2e917ea02f5 Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 21 Jul 2023 12:33:16 -0400 Subject: [PATCH 16/18] use frep_ok from Field25519 --- src/Bedrock/End2End/X25519/AddPrecomputed.v | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/Bedrock/End2End/X25519/AddPrecomputed.v b/src/Bedrock/End2End/X25519/AddPrecomputed.v index ba899366c2..de83d819fa 100644 --- a/src/Bedrock/End2End/X25519/AddPrecomputed.v +++ b/src/Bedrock/End2End/X25519/AddPrecomputed.v @@ -47,7 +47,7 @@ Import WeakestPrecondition. Local Existing Instance field_parameters. Local Instance frep25519 : Field.FieldRepresentation := field_representation n Field25519.s c. -(* Local Existing Instance frep25519_ok. *) +Local Existing Instance frep25519_ok. Definition add_precomputed := func! (ox, oy, oz, ot, X1, Y1, Z1, T1, ypx2, ymx2, xy2d2) { stackalloc 40 as YpX1; @@ -116,12 +116,6 @@ Local Instance spec_of_fe25519_mul : spec_of "fe25519_mul" := Field.spec_of_BinO Local Instance spec_of_fe25519_add : spec_of "fe25519_add" := Field.spec_of_BinOp bin_add. Local Instance spec_of_fe25519_sub : spec_of "fe25519_sub" := Field.spec_of_BinOp bin_sub. Local Instance spec_of_fe25519_from_word : spec_of "fe25519_from_word" := Field.spec_of_from_word. -(* TODO: use Field25519 version instead *) -Local Instance frep25519_ok : FieldRepresentation_ok(field_representation:=frep25519). -Proof. - apply Crypto.Bedrock.Field.Synthesis.New.Signature.field_representation_ok. - apply UnsaturatedSolinas.relax_valid. -Qed. Local Arguments word.rep : simpl never. Local Arguments word.wrap : simpl never. From 7f23bce57879a856e74630be7cd635f07b25a6cc Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 21 Jul 2023 12:37:40 -0400 Subject: [PATCH 17/18] Remove unnecessary frep_ok steps --- src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v b/src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v index 00d85ac967..2b0cef4ee2 100644 --- a/src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v +++ b/src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v @@ -127,8 +127,6 @@ Proof. (* use montladder correctness proof *) rewrite montladder_defn. eapply @montladder_correct; try (typeclasses eauto). - { apply Signature.field_representation_ok. - apply UnsaturatedSolinas.relax_valid. } { reflexivity. } { cbv [Core.__rupicola_program_marker]. tauto. } { exact I. } @@ -140,8 +138,6 @@ Proof. cbv [LadderStep.spec_of_ladderstep]; intros. prepare_call. rewrite ladderstep_defn. eapply @LadderStep.ladderstep_correct; try (typeclasses eauto). - { apply Signature.field_representation_ok. - apply UnsaturatedSolinas.relax_valid. } { cbv [Core.__rupicola_program_marker]; tauto. } { repeat (apply peel_func_binop; [ lazy; congruence | ]). apply fe25519_mul_correct. } @@ -156,7 +152,6 @@ Proof. { ecancel_assumption. } } { repeat (apply peel_func_unop; [ lazy; congruence | ]). unshelve eapply AdditionChains.fe25519_inv_correct_exp; try exact I. - { unshelve eapply Signature.field_representation_ok, UnsaturatedSolinas.relax_valid. } { repeat (apply peel_func_binop; [ lazy; congruence | ]). apply fe25519_square_correct. } { repeat (apply peel_func_binop; [ lazy; congruence | ]). From 383842d19d1c979aae1b723cdde68e3f4d3fd5cf Mon Sep 17 00:00:00 2001 From: Brian McSwiggen Date: Fri, 21 Jul 2023 15:32:09 -0400 Subject: [PATCH 18/18] Fix Qed! Final cleanup --- src/Bedrock/End2End/X25519/AddPrecomputed.v | 60 ++++++++++++++++----- 1 file changed, 46 insertions(+), 14 deletions(-) diff --git a/src/Bedrock/End2End/X25519/AddPrecomputed.v b/src/Bedrock/End2End/X25519/AddPrecomputed.v index de83d819fa..7afcbc1bfe 100644 --- a/src/Bedrock/End2End/X25519/AddPrecomputed.v +++ b/src/Bedrock/End2End/X25519/AddPrecomputed.v @@ -122,15 +122,16 @@ Local Arguments word.wrap : simpl never. Local Arguments word.unsigned : simpl never. Local Arguments word.of_Z : simpl never. -(* TODO: Remove after debugging QED *) -Require Import AdmitAxiom. +Local Ltac cbv_bounds H := + cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_sub un_outbounds bin_outbounds] in H; + cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_sub un_outbounds bin_outbounds]. Local Ltac solve_bounds := repeat match goal with | H: bounded_by loose_bounds ?x |- bounded_by loose_bounds ?x => apply H | H: bounded_by tight_bounds ?x |- bounded_by tight_bounds ?x => apply H | H: bounded_by tight_bounds ?x |- bounded_by loose_bounds ?x => apply relax_bounds - | H: bounded_by _ ?x |- bounded_by _ ?x => cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_sub un_outbounds bin_outbounds] in * + | H: bounded_by _ ?x |- bounded_by _ ?x => cbv_bounds H end. Local Ltac solve_mem := @@ -153,18 +154,49 @@ Local Ltac solve_stack := Local Ltac single_step := repeat straightline; straightline_call; ssplit; try solve_mem; try solve_bounds; try solve_stack. -Local Ltac clear_extras := - repeat match goal with - | H: ?a%sep ?b |- _ => clear H - end. +(* An example that demonstrates why we need to set Strategy in add_precomputed_ok below *) +Example demo_strategy : forall x, + (@Field.bounded_by field_parameters (Zpos (xO (xO (xO (xO (xO xH)))))) + BW32 (Naive.word (Zpos (xO (xO (xO (xO (xO xH))))))) + (@SortedListWord.map (Zpos (xO (xO (xO (xO (xO xH)))))) + (Naive.word (Zpos (xO (xO (xO (xO (xO xH))))))) Naive.word32_ok + byte) frep25519 + (@loose_bounds field_parameters (Zpos (xO (xO (xO (xO (xO xH)))))) + BW32 (Naive.word (Zpos (xO (xO (xO (xO (xO xH))))))) + (@SortedListWord.map (Zpos (xO (xO (xO (xO (xO xH)))))) + (Naive.word (Zpos (xO (xO (xO (xO (xO xH))))))) Naive.word32_ok + byte) frep25519) x = + @Field.bounded_by field_parameters (Zpos (xO (xO (xO (xO (xO xH)))))) + BW32 (Naive.word (Zpos (xO (xO (xO (xO (xO xH))))))) + (@SortedListWord.map (Zpos (xO (xO (xO (xO (xO xH)))))) + (Naive.word (Zpos (xO (xO (xO (xO (xO xH))))))) Naive.word32_ok + byte) frep25519 + (@bin_outbounds (Zpos (xO (xO (xO (xO (xO xH)))))) BW32 + (Naive.word (Zpos (xO (xO (xO (xO (xO xH))))))) + (@SortedListWord.map (Zpos (xO (xO (xO (xO (xO xH)))))) + (Naive.word (Zpos (xO (xO (xO (xO (xO xH))))))) Naive.word32_ok + byte) field_parameters frep25519 (@add field_parameters) + (@bin_add (Zpos (xO (xO (xO (xO (xO xH)))))) BW32 + (Naive.word (Zpos (xO (xO (xO (xO (xO xH))))))) + (@SortedListWord.map (Zpos (xO (xO (xO (xO (xO xH)))))) + (Naive.word (Zpos (xO (xO (xO (xO (xO xH))))))) + Naive.word32_ok byte) field_parameters frep25519)) x). +Proof. + (* reflexivity. *) (* Does not complete within 1 minute. *) + (* Now set Strategy precedence... *) + Strategy -1000 [bin_outbounds bin_add]. + reflexivity. (* ...and completes immediately *) +Qed. Lemma add_precomputed_ok : program_logic_goal_for_function! add_precomputed. Proof. + (* Without this, resolution of cbv stalls out Qed. *) + Strategy -1000 [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_sub un_outbounds bin_outbounds]. + (* Unwrap each call in the program. *) (* Each binop produces 2 memory goals on the inputs, 2 bounds goals on the inputs, and 1 memory goal on the output. *) single_step. (* fe25519_add(YpX1, Y1, X1) *) single_step. (* fe25519_sub(YmX1, Y1, X1) *) -(* TODO: Debug Qed performance: Unshelve. all:exfalso;clear;admit. Optimize Proof. Qed. *) single_step. (* fe25519_mul(A, YpX1, ypx2) *) single_step. (* fe25519_mul(B, YmX1, ymx2) *) single_step. (* fe25519_mul(C, xy2d2, T1) *) @@ -184,12 +216,12 @@ Proof. (* Rewrites the FElems for the stack (in H96) to be about bytes instead *) cbv [FElem] in *. (* Prevent output from being rewritten by seprewrite_in *) - remember (Bignum.Bignum felem_size_in_words otK _) in H96. - remember (Bignum.Bignum felem_size_in_words ozK _) in H96. - remember (Bignum.Bignum felem_size_in_words oyK _) in H96. - remember (Bignum.Bignum felem_size_in_words oxK _) in H96. + remember (Bignum.Bignum felem_size_in_words otK _) as Pt in H96. + remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H96. + remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H96. + remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H96. do 7 (seprewrite_in @Bignum.Bignum_to_bytes H96). - subst P P0 P1 P2. + subst Pt Pz Py Px. extract_ex1_and_emp_in H96. (* Solve stack/memory stuff *) @@ -207,6 +239,6 @@ Proof. } (* Safety: memory is what it should be *) ecancel_assumption. -Admitted. +Qed. End WithParameters.