Formatting fixes and added missing file

formosa-crypto · Jan 4, 2025 · b8830b2 · b8830b2
1 parent 097d3a2
commit b8830b2
Show file tree

Hide file tree

Showing 3 changed files with 1,060 additions and 3 deletions.
diff --git a/proof/crypto_scalarmult/curve25519/amd64/mulx/CorrectnessProof_Mulx.ec b/proof/crypto_scalarmult/curve25519/amd64/mulx/CorrectnessProof_Mulx.ec
@@ -339,7 +339,6 @@ proof.
     call eq_spec_impl_sqr_rr_mulx. skip. auto => />.
 qed.
 
-(** to bytes **)
 (** to bytes **)
 equiv eq_spec_impl_to_bytes_mulx : Ref4_scalarmult_s.M.__tobytes4 ~ Mulx_scalarmult_s.M.__tobytes4 :
     ={f} ==> ={res} by sim.

diff --git a/proof/crypto_scalarmult/curve25519/amd64/ref4/CorrectnessProof_Ref4.ec b/proof/crypto_scalarmult/curve25519/amd64/ref4/CorrectnessProof_Ref4.ec
@@ -489,7 +489,6 @@ proof.
     apply (h_to_bytes_cminus2P _f). smt().
 qed.
 
-
 lemma ill_to_bytes_ref4 : islossless M.__tobytes4 by islossless.
 
 lemma ph_to_bytes_ref4 r:
@@ -670,7 +669,7 @@ proof.
     rewrite (W64.and_mod 3 ctr{2}) //=  (W64.and_mod 6 (of_int (to_uint ctr{2} %% 8))%W64) //= !to_uint_shr //= !shr_shrw.
     smt(W64.to_uint_cmp  W64.of_uintK W64.to_uintK).
     rewrite /zeroextu64 /truncateu8 //=  !of_uintK => />.
-    + rewrite  of_intE modz_small.  apply bound_abs. smt(W8.to_uint_cmp JUtils.expS_minus JUtils.exp2_0).
+    + rewrite of_intE modz_small. apply bound_abs. smt(W8.to_uint_cmp JUtils.powS_minus JUtils.pow2_0).
     rewrite bits2wE /int2bs /mkseq -iotaredE => />.
     auto => />.
     rewrite (modz_small (to_uint ctr{2} %% 8) W64.modulus). apply bound_abs. smt(W64.to_uint_cmp).