Skip to content
New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Optimize & fix Edwards XYZT operations #1693

Merged
merged 7 commits into from
Oct 28, 2023
Merged

Optimize & fix Edwards XYZT operations #1693

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
0a1e8fe
switch to halved variant of precomputed coordinates
bMacSwigg Oct 27, 2023
8bc5477
Extend variant coords to Bedrock E2E
bMacSwigg Oct 27, 2023
b80db9d
Fix calculation of T in mixed addition
bMacSwigg Oct 27, 2023
9e666e0
Split T into parts to save a mul
bMacSwigg Oct 27, 2023
8c81ddf
Extend split T to precomputed addition
bMacSwigg Oct 27, 2023
f157471
Pipe split T through Bedrock code
bMacSwigg Oct 27, 2023
fe162e0
Newline at EOF
bMacSwigg Oct 27, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
164 changes: 83 additions & 81 deletions src/Bedrock/End2End/X25519/EdwardsXYZT.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,32 +51,33 @@ 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) {
Definition add_precomputed := func! (ox, oy, oz, ota, otb, X1, Y1, Z1, Ta1, Tb1, half_ypx, half_ymx, xyd) {
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);
fe25519_mul(A, YmX1, half_ymx);
stackalloc 40 as B;
fe25519_mul(B, YmX1, ymx2);
fe25519_mul(B, YpX1, half_ypx);
stackalloc 40 as T1;
fe25519_mul(T1, Ta1, Tb1);
stackalloc 40 as C;
fe25519_mul(C, xy2d2, T1);
stackalloc 40 as D;
fe25519_carry_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)
fe25519_mul(C, xyd, T1);
fe25519_sub(ota, B, A);
stackalloc 40 as F;
fe25519_sub(F, Z1, C);
stackalloc 40 as G;
fe25519_add(G, Z1, C);
fe25519_add(otb, B, A);
fe25519_mul(ox, ota, F);
fe25519_mul(oy, G, otb);
fe25519_mul(oz, F, G)
}.

(* Equivalent of m1double in src/Curves/Edwards/XYZT/Basic.v *)
(* Note: T is unused, but leaving in place in case we want to switch to a point struct in the future *)
Definition double := func! (ox, oy, oz, ot, X, Y, Z, T) {
(* Note: Ta/Tb are unused, but leaving in place in case we want to switch to a point struct in the future *)
Definition double := func! (ox, oy, oz, ota, otb, X, Y, Z, Ta, Tb) {
stackalloc 40 as trX;
fe25519_square(trX, X);
stackalloc 40 as trZ;
Expand All @@ -88,18 +89,15 @@ Definition double := func! (ox, oy, oz, ot, X, Y, Z, T) {
stackalloc 40 as rY;
fe25519_add(rY, X, Y);
fe25519_square(t0, rY);
stackalloc 40 as cY;
fe25519_carry_add(cY, trZ, trX);
fe25519_carry_add(otb, trZ, trX);
stackalloc 40 as cZ;
fe25519_carry_sub(cZ, trZ, trX);
stackalloc 40 as cX;
fe25519_sub(cX, t0, cY);
fe25519_sub(ota, t0, otb);
stackalloc 40 as cT;
fe25519_sub(cT, trT, cZ);
fe25519_mul(ox, cX, cT);
fe25519_mul(oy, cY, cZ);
fe25519_mul(oz, cZ, cT);
fe25519_mul(ot, cX, cY)
fe25519_mul(ox, ota, cT);
fe25519_mul(oy, otb, cZ);
fe25519_mul(oz, cZ, cT)
}.

Section WithParameters.
Expand Down Expand Up @@ -133,47 +131,51 @@ Local Notation m1double :=

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),
(oxK oyK ozK otaK otbK X1K Y1K Z1K Ta1K Tb1K half_ypxK half_ymxK xydK : word) /
(ox oy oz ota otb X1 Y1 Z1 Ta1 Tb1 half_ypx half_ymx xyd : felem) (R : _ -> Prop),
{ requires t m :=
bounded_by tight_bounds X1 /\
bounded_by tight_bounds Y1 /\
bounded_by tight_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;
bounded_by loose_bounds Ta1 /\
bounded_by loose_bounds Tb1 /\
bounded_by loose_bounds half_ypx /\
bounded_by loose_bounds half_ymx /\
bounded_by loose_bounds xyd /\
m =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem Ta1K Ta1) * (FElem Tb1K Tb1) * (FElem half_ypxK half_ypx) * (FElem half_ymxK half_ymx) * (FElem xydK xyd) * (FElem oxK ox) * (FElem oyK oy) * (FElem ozK oz) * (FElem otaK ota) * (FElem otbK otb) * R;
ensures t' m' :=
t = t' /\
exists ox' oy' oz' ot',
((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))) /\
exists ox' oy' oz' ota' otb',
((feval ox'), (feval oy'), (feval oz'), (feval ota'), (feval otb')) = (@m1add_precomputed_coordinates (F M_pos) (F.add) (F.sub) (F.mul) ((feval X1), (feval Y1), (feval Z1), (feval Ta1), (feval Tb1)) ((feval half_ypx), (feval half_ymx), (feval xyd))) /\
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 }.
bounded_by loose_bounds ota' /\
bounded_by loose_bounds otb' /\
m' =* (FElem X1K X1) * (FElem Y1K Y1) * (FElem Z1K Z1) * (FElem Ta1K Ta1) * (FElem Tb1K Tb1) * (FElem half_ypxK half_ypx) * (FElem half_ymxK half_ymx) * (FElem xydK xyd) * (FElem oxK ox') * (FElem oyK oy') * (FElem ozK oz') * (FElem otaK ota') * (FElem otbK otb') * R }.

Global Instance spec_of_double : spec_of "double" :=
fnspec! "double"
(oxK oyK ozK otK XK YK ZK TK : word) /
(ox oy oz ot X Y Z T : felem) (p : point) (R : _ -> Prop),
(oxK oyK ozK otaK otbK XK YK ZK TaK TbK : word) /
(ox oy oz ota otb X Y Z Ta Tb : felem) (p : point) (R : _ -> Prop),
{ requires t m :=
coordinates p = ((feval X), (feval Y), (feval Z), (feval T)) /\
coordinates p = ((feval X), (feval Y), (feval Z), (feval Ta), (feval Tb)) /\
bounded_by tight_bounds X /\
bounded_by tight_bounds Y /\
bounded_by loose_bounds Z /\
bounded_by loose_bounds T /\
m =* (FElem XK X) * (FElem YK Y) * (FElem ZK Z) * (FElem TK T) * (FElem oxK ox) * (FElem oyK oy) * (FElem ozK oz) * (FElem otK ot) * R;
bounded_by loose_bounds Ta /\
bounded_by loose_bounds Tb /\
m =* (FElem XK X) * (FElem YK Y) * (FElem ZK Z) * (FElem TaK Ta) * (FElem TbK Tb) * (FElem oxK ox) * (FElem oyK oy) * (FElem ozK oz) * (FElem otaK ota) * (FElem otbK otb) * R;
ensures t' m' :=
t = t' /\
exists ox' oy' oz' ot',
((feval ox'), (feval oy'), (feval oz'), (feval ot')) = coordinates (@m1double p) /\
exists ox' oy' oz' ota' otb',
((feval ox'), (feval oy'), (feval oz'), (feval ota'), (feval otb')) = coordinates (@m1double p) /\
bounded_by tight_bounds ox' /\
bounded_by tight_bounds oy' /\
bounded_by tight_bounds oz' /\
bounded_by tight_bounds ot' /\
m' =* (FElem XK X) * (FElem YK Y) * (FElem ZK Z) * (FElem TK T) * (FElem oxK ox') * (FElem oyK oy') * (FElem ozK oz') * (FElem otK ot') * R }.
bounded_by loose_bounds ota' /\ (* could be tight_bounds if we need it, but I don't think we do *)
bounded_by tight_bounds otb' /\
m' =* (FElem XK X) * (FElem YK Y) * (FElem ZK Z) * (FElem TaK Ta) * (FElem TbK Tb) * (FElem oxK ox') * (FElem oyK oy') * (FElem ozK oz') * (FElem otaK ota') * (FElem otbK otb') * R }.


Local Instance spec_of_fe25519_square : spec_of "fe25519_square" := Field.spec_of_UnOp un_square.
Expand Down Expand Up @@ -264,37 +266,37 @@ 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) *)
single_step. (* fe25519_mul(A, YpX1, ypx2) *)
single_step. (* fe25519_mul(B, YmX1, ymx2) *)
single_step. (* fe25519_mul(C, xy2d2, T1) *)
single_step. (* fe25519_carry_add(D, Z1, Z1) *)
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) *)
single_step. (* fe25519_mul(A, YmX1, half_ymx) *)
single_step. (* fe25519_mul(B, YpX1, half_ypx) *)
single_step. (* fe25519_mul(T1, Ta1, Tb1) *)
single_step. (* fe25519_mul(C, xyd, T1) *)
single_step. (* fe25519_sub(ota, B, A) *)
single_step. (* fe25519_sub(F, Z1, C) *)
single_step. (* fe25519_add(G, Z1, C) *)
single_step. (* fe25519_add(otb, B, A) *)
single_step. (* fe25519_mul(ox, ota, F) *)
single_step. (* fe25519_mul(oy, G, otb) *)
single_step. (* fe25519_mul(oz, F, G) *)

(* Solve the postconditions *)
repeat straightline.
(* Rewrites the FElems for the stack (in H88) to be about bytes instead *)
(* Rewrites the FElems for the stack (in H93) 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 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 H88.
remember (Bignum.Bignum felem_size_in_words ozK _) as Pz in H93.
remember (Bignum.Bignum felem_size_in_words oyK _) as Py in H93.
remember (Bignum.Bignum felem_size_in_words oxK _) as Px in H93.
remember (Bignum.Bignum felem_size_in_words otbK _) as Ptb in H93.
remember (Bignum.Bignum felem_size_in_words otaK _) as Pta in H93.
do 8 (seprewrite_in @Bignum.Bignum_to_bytes H93).
subst Pz Py Px Ptb Pta.
extract_ex1_and_emp_in H93.

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

(* Post-conditions *)
exists x9,x10,x11,x12; ssplit. 2,3,4,5:solve_bounds.
exists x9,x10,x11,x5,x8; ssplit. 2,3,4,5,6:solve_bounds.
{ (* Correctness: result matches Gallina *)
cbv [bin_model bin_mul bin_add bin_carry_add bin_sub] in *.
cbv match beta delta [m1add_precomputed_coordinates].
Expand All @@ -317,38 +319,38 @@ Proof.
single_step. (* fe25519_carry_add(trT, t0, t0) *)
single_step. (* fe25519_add(rY, X, Y) *)
single_step. (* fe25519_square(t0, rY) *)
single_step. (* fe25519_carry_add(cY, trZ, trX) *)
single_step. (* fe25519_carry_add(otb, trZ, trX) *)
single_step. (* fe25519_carry_sub(cZ, trZ, trX) *)
single_step. (* fe25519_sub(cX, t0, cY) *)
single_step. (* fe25519_sub(ota, t0, otb) *)
single_step. (* fe25519_sub(cT, trT, cZ) *)
single_step. (* fe25519_mul(ox, cX, cT) *)
single_step. (* fe25519_mul(oy, cY, cZ) *)
single_step. (* fe25519_mul(ox, ota, cT) *)
single_step. (* fe25519_mul(oy, otb, 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 H98) to be about bytes instead *)
(* Rewrites the FElems for the stack (in H87) 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 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 H98.
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.
remember (Bignum.Bignum felem_size_in_words otaK _) as Pta in H87.
remember (Bignum.Bignum felem_size_in_words otbK _) as Ptb in H87.
do 7 (seprewrite_in @Bignum.Bignum_to_bytes H87).
subst Pz Py Px Pta Ptb.
extract_ex1_and_emp_in H87.

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

(* Post-conditions *)
exists x9,x10,x11,x12; ssplit. 2,3,4,5:solve_bounds.
exists x9,x10,x11,x7,x5; ssplit. 2,3,4,5,6:solve_bounds.
{ (* Correctness: result matches Gallina *)
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.
destruct p. cbv [coordinates proj1_sig] in H12.
rewrite H12.
rewrite F.pow_2_r in *.
congruence.
}
Expand Down
47 changes: 23 additions & 24 deletions src/Curves/Edwards/XYZT/Basic.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,14 +29,14 @@ Section ExtendedCoordinates.
Local Notation onCurve x y := (a*x^2 + y^2 = 1 + d*x^2*y^2) (only parsing).
(** [Extended.point] represents a point on an elliptic curve using extended projective
* Edwards coordinates 1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
Definition point := { P | let '(X,Y,Z,T) := P in
Definition point := { P | let '(X,Y,Z,Ta,Tb) := P in
a * X^2*Z^2 + Y^2*Z^2 = (Z^2)^2 + d * X^2 * Y^2
/\ X * Y = Z * T
/\ X * Y = Z * Ta * Tb
/\ Z <> 0 }.
Definition coordinates (P:point) : F*F*F*F := proj1_sig P.
Definition coordinates (P:point) : F*F*F*F*F := proj1_sig P.
Definition eq (P1 P2:point) :=
let '(X1, Y1, Z1, _) := coordinates P1 in
let '(X2, Y2, Z2, _) := coordinates P2 in
let '(X1, Y1, Z1, _, _) := coordinates P1 in
let '(X2, Y2, Z2, _, _) := coordinates P2 in
Z2*X1 = Z1*X2 /\ Z2*Y1 = Z1*Y2.

Ltac t_step :=
Expand All @@ -58,14 +58,16 @@ Section ExtendedCoordinates.
Proof. intros P Q; destruct P as [ [ [ [ ] ? ] ? ] ?], Q as [ [ [ [ ] ? ] ? ] ? ]; exact _. Defined.

Program Definition from_twisted (P:Epoint) : point :=
let xy := E.coordinates P in (fst xy, snd xy, 1, fst xy * snd xy).
let xy := E.coordinates P in (fst xy, snd xy, 1, fst xy, snd xy).
Next Obligation. t. Qed.
Global Instance Proper_from_twisted : Proper (E.eq==>eq) from_twisted.
Proof using Type. cbv [from_twisted]; t. Qed.

Program Definition to_twisted (P:point) : Epoint :=
let XYZT := coordinates P in let T := snd XYZT in
let XYZ := fst XYZT in let Z := snd XYZ in
let XYZTT := coordinates P in let Ta := snd XYZTT in
let XYZT := fst XYZTT in
let Tb := snd XYZT in
let XYZ := fst XYZT in let Z := snd XYZ in
let XY := fst XYZ in let Y := snd XY in
let X := fst XY in
let iZ := Finv Z in ((X*iZ), (Y*iZ)).
Expand All @@ -78,36 +80,35 @@ Section ExtendedCoordinates.
Lemma from_twisted_to_twisted P : eq (from_twisted (to_twisted P)) P.
Proof using Type. cbv [to_twisted from_twisted]; t. Qed.

Program Definition zero : point := (0, 1, 1, 0).
Program Definition zero : point := (0, 1, 1, 0, 1).
Next Obligation. t. Qed.

Program Definition opp P : point :=
match coordinates P return F*F*F*F with (X,Y,Z,T) => (Fopp X, Y, Z, Fopp T) end.
match coordinates P return F*F*F*F*F with (X,Y,Z,Ta,Tb) => (Fopp X, Y, Z, Fopp Ta, Tb) end.
Next Obligation. t. Qed.

Section TwistMinusOne.
Context {a_eq_minus1:a = Fopp 1} {twice_d} {k_eq_2d:twice_d = d+d}.
Program Definition m1add
(P1 P2:point) : point :=
match coordinates P1, coordinates P2 return F*F*F*F with
(X1, Y1, Z1, T1), (X2, Y2, Z2, T2) =>
match coordinates P1, coordinates P2 return F*F*F*F*F with
(X1, Y1, Z1, Ta1, Tb1), (X2, Y2, Z2, Ta2, Tb2) =>
let A := (Y1-X1)*(Y2-X2) in
let B := (Y1+X1)*(Y2+X2) in
let C := T1*twice_d*T2 in
let C := (Ta1*Tb1)*twice_d*(Ta2*Tb2) in
let D := Z1*(Z2+Z2) in
let E := B-A in
let F := D-C in
let G := D+C in
let H := B+A in
let X3 := E*F in
let Y3 := G*H in
let T3 := E*H in
let Z3 := F*G in
(X3, Y3, Z3, T3)
(X3, Y3, Z3, E, H)
end.
Next Obligation.
match goal with
| [ |- match (let (_, _) := coordinates ?P1 in let (_, _) := _ in let (_, _) := _ in let (_, _) := coordinates ?P2 in _) with _ => _ end ]
| [ |- match (let (_, _) := coordinates ?P1 in let (_, _) := _ in let (_, _) := _ in let (_, _) := _ in let (_, _) := coordinates ?P2 in _) with _ => _ end ]
=> pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1)) _ _ (proj2_sig (to_twisted P2)))
end; t.
Qed.
Expand All @@ -134,8 +135,8 @@ Section ExtendedCoordinates.
Proof. pose proof isomorphic_commutative_group_m1 as H; destruct H as [ [] [] [] [] ]; trivial. Qed.

Program Definition m1double (P : point) : point :=
match coordinates P return F*F*F*F with
(X, Y, Z, _) =>
match coordinates P return F*F*F*F*F with
(X, Y, Z, _, _) =>
let trX := X^2 in
let trZ := Y^2 in
let trT := (let t0 := Z^2 in t0+t0) in
Expand All @@ -148,8 +149,7 @@ Section ExtendedCoordinates.
let X3 := cX*cT in
let Y3 := cY*cZ in
let Z3 := cZ*cT in
let T3 := cX*cY in
(X3, Y3, Z3, T3)
(X3, Y3, Z3, cX, cY)
end.
Next Obligation.
match goal with
Expand All @@ -167,8 +167,8 @@ Section ExtendedCoordinates.

(* https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#doubling-double-2008-hwcd *)
Program Definition double (P : point) : point :=
match coordinates P return F*F*F*F with
(X1, Y1, Z1, T1) =>
match coordinates P return F*F*F*F*F with
(X1, Y1, Z1, _, _) =>
let A := X1^2 in
let B := Y1^2 in
let t0 := Z1^2 in
Expand All @@ -183,9 +183,8 @@ Section ExtendedCoordinates.
let H := D-B in
let X3 := E*F in
let Y3 := G*H in
let T3 := E*H in
let Z3 := F*G in
(X3, Y3, Z3, T3)
(X3, Y3, Z3, E, H)
end.
Next Obligation.
match goal with
Expand Down
Loading