Skip to content

Commit

Permalink
Add TODO in comment
Browse files Browse the repository at this point in the history
  • Loading branch information
bMacSwigg authored and andres-erbsen committed Sep 12, 2023
1 parent 7b44206 commit b46f316
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Bedrock/End2End/X25519/EdwardsXYZT.v
Original file line number Diff line number Diff line change
Expand Up @@ -480,7 +480,7 @@ Proof.
single_step. (* fe25519_sub(cZ, trZ, trX) *)
single_step. (* fe25519_sub(cX, t0, cY) *)
single_step. (* fe25519_sub(cT, trT, cZ) *)
admit. (* bounds issue on cZ -- 3 lines up needs carry_sub instead *)
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) *)
Expand Down

0 comments on commit b46f316

Please sign in to comment.