Skip to content

Commit

Permalink
Switch to carry_sub and complete proof
Browse files Browse the repository at this point in the history
  • Loading branch information
@bMacSwigg @andres-erbsen
bMacSwigg authored and andres-erbsen committed Sep 12, 2023
1 parent b46f316 commit f6a230f
Showing 1 changed file with 22 additions and 182 deletions.
204 changes: 22 additions & 182 deletions src/Bedrock/End2End/X25519/EdwardsXYZT.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ Definition double := func! (ox, oy, oz, ot, X, Y, Z, T) {
stackalloc 40 as cY;
fe25519_carry_add(cY, trZ, trX);
stackalloc 40 as cZ;
fe25519_sub(cZ, trZ, trX); (* TODO: use carry_sub once #1641 is merged *)
fe25519_carry_sub(cZ, trZ, trX);
stackalloc 40 as cX;
fe25519_sub(cX, t0, cY);
stackalloc 40 as cT;
Expand Down Expand Up @@ -181,176 +181,17 @@ 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_carry_add : spec_of "fe25519_carry_add" := Field.spec_of_BinOp bin_carry_add.
Local Instance spec_of_fe25519_sub : spec_of "fe25519_sub" := Field.spec_of_BinOp bin_sub.
Local Instance spec_of_fe25519_carry_sub : spec_of "fe25519_carry_sub" := Field.spec_of_BinOp bin_carry_sub.
Local Instance spec_of_fe25519_from_word : spec_of "fe25519_from_word" := Field.spec_of_from_word.

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.

(* TODO: Make these changes in ProgramLogic instead *)
Local Ltac straightline_cleanup :=
match goal with
(* TODO remove superfluous _ after .rep, but that will break some proofs that rely on
x not being cleared to instantiate evars with terms depending on x *)
| x : Word.Interface.word.rep _ |- _ => clear x
| x : Init.Byte.byte |- _ => clear x
| x : Semantics.trace |- _ => clear x
| x : Syntax.cmd |- _ => clear x
| x : Syntax.expr |- _ => clear x
| x : coqutil.Map.Interface.map.rep |- _ => clear x
| x : BinNums.Z |- _ => clear x
| x : unit |- _ => clear x
| x : bool |- _ => clear x
| x : list _ |- _ => clear x
| x : nat |- _ => clear x
(* same TODO as above *)
| x := _ : Word.Interface.word.rep _ |- _ => clear x
| x := _ : Init.Byte.byte |- _ => clear x
| x := _ : Semantics.trace |- _ => clear x
| x := _ : Syntax.cmd |- _ => clear x
| x := _ : Syntax.expr |- _ => clear x
| x := _ : coqutil.Map.Interface.map.rep |- _ => clear x
| x := _ : BinNums.Z |- _ => clear x
| x := _ : unit |- _ => clear x
| x := _ : bool |- _ => clear x
| x := _ : list _ |- _ => clear x
| x := _ : nat |- _ => clear x
| |- forall _, _ => intros
| |- let _ := _ in _ => intros
| |- dlet.dlet ?v (fun x => ?P) => change (let x := v in P); intros
| _ => progress (cbn [Semantics.interp_binop] in * )
| H: exists _, _ |- _ => destruct H; assert_fails (idtac; let __ := constr:(H) in idtac)
| H: _ /\ _ |- _ => destruct H
| x := ?y |- ?G => is_var y; subst x
| H: ?x = ?y |- _ => constr_eq x y; clear H
| H: ?x = ?y |- _ => is_var x; is_var y; assert_fails (idtac; let __ := eval cbv [x] in x in idtac); subst x
| H: ?x = ?y |- _ => is_var x; is_var y; assert_fails (idtac; let __ := eval cbv [y] in y in idtac); subst y
| H: ?x = ?v |- _ =>
is_var x;
assert_fails (idtac; let __ := eval cbv delta [x] in x in idtac);
lazymatch v with context[x] => fail | _ => idtac end;
let x' := fresh x in
rename x into x';
simple refine (let x := v in _);
change (x' = x) in H;
symmetry in H;
destruct H
end.

Local Ltac straightline :=
match goal with
| _ => straightline_cleanup
| |- program_logic_goal_for ?f _ =>
enter f; intros;
match goal with
| H: map.get ?functions ?fname = Some _ |- _ =>
eapply start_func; [exact H | clear H]
end;
cbv match beta delta [WeakestPrecondition.func]
| |- WeakestPrecondition.cmd _ (cmd.set ?s ?e) _ _ _ ?post =>
unfold1_cmd_goal; cbv beta match delta [cmd_body];
let __ := match s with String.String _ _ => idtac | String.EmptyString => idtac end in
ident_of_constr_string_cps s ltac:(fun x =>
ensure_free x;
(* NOTE: keep this consistent with the [exists _, _ /\ _] case far below *)
letexists _ as x; split; [solve [repeat straightline]|])
| |- cmd _ ?c _ _ _ ?post =>
let c := eval hnf in c in
lazymatch c with
| cmd.while _ _ => fail
| cmd.cond _ _ _ => fail
| cmd.interact _ _ _ => fail
| _ => unfold1_cmd_goal; cbv beta match delta [cmd_body]
end
| |- @list_map _ _ (get _) _ _ => unfold1_list_map_goal; cbv beta match delta [list_map_body]
| |- @list_map _ _ (expr _ _) _ _ => unfold1_list_map_goal; cbv beta match delta [list_map_body]
| |- @list_map _ _ _ nil _ => cbv beta match fix delta [list_map list_map_body]
| |- expr _ _ _ _ => unfold1_expr_goal; cbv beta match delta [expr_body]
| |- dexpr _ _ _ _ => cbv beta delta [dexpr]
| |- dexprs _ _ _ _ => cbv beta delta [dexprs]
| |- literal _ _ => cbv beta delta [literal]
| |- @get ?w ?W ?L ?l ?x ?P =>
let get' := eval cbv [get] in @get in
change (get' w W L l x P); cbv beta
| |- load _ _ _ _ => cbv beta delta [load]
| |- @Loops.enforce ?width ?word ?locals ?names ?values ?map =>
let values := eval cbv in values in
change (@Loops.enforce width word locals names values map);
exact (conj (eq_refl values) eq_refl)
| |- @eq (@coqutil.Map.Interface.map.rep String.string Interface.word.rep _) _ _ =>
eapply SortedList.eq_value; exact eq_refl
| |- @map.get String.string Interface.word.rep ?M ?m ?k = Some ?e' =>
let e := rdelta e' in
is_evar e;
once (let v := multimatch goal with x := context[@map.put _ _ M _ k ?v] |- _ => v end in
(* cbv is slower than this, cbv with whitelist would have an enormous whitelist, cbv delta for map is slower than this, generalize unrelated then cbv is slower than this, generalize then vm_compute is slower than this, lazy is as slow as this: *)
unify e v; exact (eq_refl (Some v)))
| |- @coqutil.Map.Interface.map.get String.string Interface.word.rep _ _ _ = Some ?v =>
let v' := rdelta v in is_evar v'; (change v with v'); exact eq_refl
| |- ?x = ?y =>
let y := rdelta y in is_evar y; change (x=y); exact eq_refl
| |- ?x = ?y =>
let x := rdelta x in is_evar x; change (x=y); exact eq_refl
| |- ?x = ?y =>
let x := rdelta x in let y := rdelta y in constr_eq x y; exact eq_refl
| |- store Syntax.access_size.one _ _ _ _ =>
eapply Scalars.store_one_of_sep; [solve[ecancel_assumption]|]
| |- store Syntax.access_size.two _ _ _ _ =>
eapply Scalars.store_two_of_sep; [solve[ecancel_assumption]|]
| |- store Syntax.access_size.four _ _ _ _ =>
eapply Scalars.store_four_of_sep; [solve[ecancel_assumption]|]
| |- store Syntax.access_size.word _ _ _ _ =>
eapply Scalars.store_word_of_sep; [solve[ecancel_assumption]|]
| |- bedrock2.Memory.load Syntax.access_size.one ?m ?a = Some ?ev =>
try subst ev; refine (@Scalars.load_one_of_sep _ _ _ _ _ _ _ _ _ _); ecancel_assumption
| |- @bedrock2.Memory.load _ ?word ?mem Syntax.access_size.two ?m ?a = Some ?ev =>
try subst ev; refine (@Scalars.load_two_of_sep _ word _ mem _ a _ _ m _); ecancel_assumption
| |- @bedrock2.Memory.load _ ?word ?mem Syntax.access_size.four ?m ?a = Some ?ev =>
try subst ev; refine (@Scalars.load_four_of_sep_32bit _ word _ mem _ eq_refl a _ _ m _); ecancel_assumption
| |- @bedrock2.Memory.load _ ?word ?mem Syntax.access_size.four ?m ?a = Some ?ev =>
try subst ev; refine (@Scalars.load_four_of_sep _ word _ mem _ a _ _ m _); ecancel_assumption
| |- @bedrock2.Memory.load _ ?word ?mem Syntax.access_size.word ?m ?a = Some ?ev =>
try subst ev; refine (@Scalars.load_word_of_sep _ word _ mem _ a _ _ m _); ecancel_assumption
| |- exists l', Interface.map.of_list_zip ?ks ?vs = Some l' /\ _ =>
letexists; split; [exact eq_refl|] (* TODO: less unification here? *)
| |- exists l', Interface.map.putmany_of_list_zip ?ks ?vs ?l = Some l' /\ _ =>
letexists; split; [exact eq_refl|] (* TODO: less unification here? *)
| _ => fwd_uniq_step
| |- exists x, ?P /\ ?Q =>
let x := fresh x in refine (let x := _ in ex_intro (fun x => P /\ Q) x _);
split; [solve [repeat straightline]|]
| |- exists x, Markers.split (?P /\ ?Q) =>
let x := fresh x in refine (let x := _ in ex_intro (fun x => P /\ Q) x _);
split; [solve [repeat straightline]|]
| |- Markers.unique (exists x, Markers.split (?P /\ ?Q)) =>
let x := fresh x in refine (let x := _ in ex_intro (fun x => P /\ Q) x _);
split; [solve [repeat straightline]|]
| |- Markers.unique (Markers.left ?G) =>
change G;
unshelve (idtac; repeat match goal with
| |- Markers.split (?P /\ Markers.right ?Q) =>
split; [eabstract (repeat straightline) | change Q]
| |- exists _, _ => letexists
end); []
| |- Markers.split ?G => change G; split
| |- True => exact I
| |- False \/ _ => right
| |- _ \/ False => left
| |- BinInt.Z.modulo ?z (Memory.bytes_per_word _) = BinInt.Z0 /\ _ =>
lazymatch Coq.setoid_ring.InitialRing.isZcst z with
| true => split; [exact eq_refl|]
end
| |- _ => straightline_stackalloc
| |- _ => straightline_stackdealloc
| |- context[sep (sep _ _) _] => progress (flatten_seps_in_goal; cbn [seps])
| H : context[sep (sep _ _) _] |- _ => progress (flatten_seps_in H; cbn [seps] in H)
end.
(* end of modified straightline section *)

Local Ltac cbv_bounds H :=
cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub un_outbounds bin_outbounds] in H;
cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub un_outbounds bin_outbounds].
cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_outbounds bin_outbounds] in H;
cbv [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_outbounds bin_outbounds].

Local Ltac solve_bounds :=
repeat match goal with
Expand Down Expand Up @@ -438,16 +279,16 @@ Proof.

(* Solve the postconditions *)
repeat straightline.
(* Rewrites the FElems for the stack (in H87) to be about bytes instead *)
(* Rewrites the FElems for the stack (in H88) to be about bytes instead *)
cbv [FElem] in *.
(* Prevent output from being rewritten by seprewrite_in *)
remember (Bignum.Bignum felem_size_in_words otK _) as Pt in H87.
remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H87.
remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H87.
remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H87.
do 6 (seprewrite_in @Bignum.Bignum_to_bytes H87).
remember (Bignum.Bignum felem_size_in_words otK _) as Pt in H88.
remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H88.
remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H88.
remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H88.
do 6 (seprewrite_in @Bignum.Bignum_to_bytes H88).
subst Pt Pz Py Px.
extract_ex1_and_emp_in H87.
extract_ex1_and_emp_in H88.

(* Solve stack/memory stuff *)
repeat straightline.
Expand All @@ -466,7 +307,7 @@ Qed.
Lemma double_ok : program_logic_goal_for_function! double.
Proof.
(* Without this, resolution of cbv stalls out Qed. *)
Strategy -1000 [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub un_outbounds bin_outbounds].
Strategy -1000 [un_xbounds bin_xbounds bin_ybounds un_square bin_mul bin_add bin_carry_add bin_sub bin_carry_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. *)
Expand All @@ -477,35 +318,34 @@ Proof.
single_step. (* fe25519_add(rY, X, Y) *)
single_step. (* fe25519_square(t0, rY) *)
single_step. (* fe25519_carry_add(cY, trZ, trX) *)
single_step. (* fe25519_sub(cZ, trZ, trX) *)
single_step. (* fe25519_carry_sub(cZ, trZ, trX) *)
single_step. (* fe25519_sub(cX, t0, cY) *)
single_step. (* fe25519_sub(cT, trT, cZ) *)
admit. (* TODO: bounds issue on cZ -- 3 lines up needs carry_sub instead *)
single_step. (* fe25519_mul(ox, cX, cT) *)
single_step. (* fe25519_mul(oy, cY, cZ) *)
single_step. (* fe25519_mul(oz, cZ, cT) *)
single_step. (* fe25519_mul(ot, cX, cY) *)

(* Solve the postconditions *)
repeat straightline.
(* Rewrites the FElems for the stack (in H97) to be about bytes instead *)
(* Rewrites the FElems for the stack (in H98) to be about bytes instead *)
cbv [FElem] in *.
(* Prevent output from being rewritten by seprewrite_in *)
remember (Bignum.Bignum felem_size_in_words otK _) as Pt in H97.
remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H97.
remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H97.
remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H97.
do 9 (seprewrite_in @Bignum.Bignum_to_bytes H97).
remember (Bignum.Bignum felem_size_in_words otK _) as Pt in H98.
remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H98.
remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H98.
remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H98.
do 9 (seprewrite_in @Bignum.Bignum_to_bytes H98).
subst Pt Pz Py Px.
extract_ex1_and_emp_in H97.
extract_ex1_and_emp_in H98.

(* Solve stack/memory stuff *)
repeat straightline.

(* Post-conditions *)
exists x9,x10,x11,x12; ssplit. 2,3,4,5:solve_bounds.
{ (* Correctness: result matches Gallina *)
cbv [bin_model bin_mul bin_add bin_carry_add bin_sub un_model un_square] in *.
cbv [bin_model bin_mul bin_add bin_carry_add bin_sub bin_carry_sub un_model un_square] in *.
cbv match beta delta [m1double coordinates proj1_sig].
destruct p. cbv [coordinates proj1_sig] in H13.
rewrite H13.
Expand All @@ -514,6 +354,6 @@ Proof.
}
(* Safety: memory is what it should be *)
ecancel_assumption.
Admitted.
Qed.

End WithParameters.

0 comments on commit f6a230f

Please sign in to comment.