Removed SMT call from inversion proof (now uses a long rewrite)

formosa-crypto · Oct 8, 2024 · c085b89 · c085b89
1 parent 32d6de0
commit c085b89
Showing 1 changed file with 1 addition and 44 deletions.
diff --git a/proof/crypto_scalarmult/curve25519/amd64/common/Curve25519_Operations.ec b/proof/crypto_scalarmult/curve25519/amd64/common/Curve25519_Operations.ec
@@ -195,53 +195,10 @@ op op_invert_p(z1 : zp) : zp =
   z_255_21 axiomatized by op_invert_pE.
 (* lemma: invert is the same as z1^(p-2) from fermat's little theorem *)
 
-lemma eq_op_invert_p_part1 (z1: zp):
-    op_invert_p z1 = op_invert_p_p3 (op_invert_p_p2 ((ZModpRing.exp z1 31))) ((ZModpRing.exp z1 11)).
-proof.
-    rewrite op_invert_pE.
-    rewrite /op_invert_p_p1 => />.
-    smt(ZModpRing.exprM ZModpRing.exprS ZModpRing.exprD_nneg).
-qed.
-
-lemma eq_op_invert_p_part2 (z1: zp):
-    op_invert_p_p3 (op_invert_p_p2 ((ZModpRing.exp z1 31))) ((ZModpRing.exp z1 11)) =
-        op_invert_p_p3 ((ZModpRing.exp z1 1125899906842623)) ((ZModpRing.exp z1 11)).
-proof.
-    rewrite /op_invert_p_p2 => />.
-    rewrite -!ZModpRing.exprM => />.
-    rewrite -!ZModpRing.exprD_nneg => />.
-    rewrite -!ZModpRing.exprM => />.
-    rewrite -!ZModpRing.exprD_nneg => />.
-    rewrite -!ZModpRing.exprM => />.
-    rewrite -!ZModpRing.exprD_nneg => />.
-    rewrite -!ZModpRing.exprM => />.
-    rewrite -!ZModpRing.exprD_nneg => />.
-qed.
-
-
-lemma eq_op_invert_p_part3 (z1: zp):
-   op_invert_p_p3 ((ZModpRing.exp z1 1125899906842623)) ((ZModpRing.exp z1 11)) = (ZModpRing.exp z1
-   57896044618658097711785492504343953926634992332820282019728792003956564819947).
-proof.
-    rewrite /op_invert_p_p3.
-    rewrite -!ZModpRing.exprM => />.
-    rewrite -!ZModpRing.exprD_nneg => />.
-    rewrite -!ZModpRing.exprM => />.
-    rewrite -!ZModpRing.exprD_nneg => />.
-    rewrite -!ZModpRing.exprM => />.
-    rewrite -!ZModpRing.exprD_nneg => />.
-    rewrite -!ZModpRing.exprM => />.
-    rewrite -!ZModpRing.exprD_nneg => />.
-qed.
-
 lemma eq_op_invert_p (z1: zp) :
   op_invert_p z1 = ZModpRing.exp z1 (p-2).
 proof.
-    rewrite pE.
-    rewrite eq_op_invert_p_part1.
-    rewrite eq_op_invert_p_part2.
-    rewrite eq_op_invert_p_part3.
-    by congr.
+    by rewrite pE op_invert_pE  /op_invert_p_p1 //= -!ZModpRing.exprM -!ZModpRing.exprS //= -!ZModpRing.exprD_nneg //= -!ZModpRing.exprM -!ZModpRing.exprD_nneg //= ZModpRing.exprM /op_invert_p_p2 //= -!ZModpRing.exprM -!ZModpRing.exprD_nneg //= -!ZModpRing.exprM -!ZModpRing.exprD_nneg //= -!ZModpRing.exprM -!ZModpRing.exprD_nneg //= -!ZModpRing.exprM //= -!ZModpRing.exprD_nneg  /op_invert_p_p3 -!ZModpRing.exprM //= -!ZModpRing.exprD_nneg //= -!ZModpRing.exprM -!ZModpRing.exprD_nneg //= -!ZModpRing.exprM -!ZModpRing.exprD_nneg //= -!ZModpRing.exprM -!ZModpRing.exprD_nneg; congr.
 qed.
 
 (* now we define invert as one op and prove it equiv to exp z1 (p-2) *)