Merge pull request #140 from jargh/main

Extra P-256 functions for AWS-LC integration, popcount, basic P-384 scalar mul
awslabs · Aug 19, 2024 · 08bf556 · 08bf556
2 parents 7ff619c + eacef33
commit 08bf556
Show file tree

Hide file tree

Showing 48 changed files with 157,673 additions and 14 deletions.
diff --git a/arm/Makefile b/arm/Makefile
@@ -97,6 +97,8 @@ POINT_OBJ = curve25519/curve25519_ladderstep.o \
             p256/p256_montjdouble_alt.o \
             p256/p256_montjmixadd.o \
             p256/p256_montjmixadd_alt.o \
+            p256/p256_montjscalarmul.o \
+            p256/p256_montjscalarmul_alt.o \
             p256/p256_scalarmul.o \
             p256/p256_scalarmul_alt.o \
             p256/p256_scalarmulbase.o \
@@ -107,6 +109,8 @@ POINT_OBJ = curve25519/curve25519_ladderstep.o \
             p384/p384_montjdouble_alt.o \
             p384/p384_montjmixadd.o \
             p384/p384_montjmixadd_alt.o \
+            p384/p384_montjscalarmul.o \
+            p384/p384_montjscalarmul_alt.o \
             p521/p521_jadd.o \
             p521/p521_jadd_alt.o \
             p521/p521_jdouble.o \
@@ -243,6 +247,7 @@ BIGNUM_OBJ = curve25519/bignum_add_p25519.o \
              generic/word_max.o \
              generic/word_min.o \
              generic/word_negmodinv.o \
+             generic/word_popcount.o \
              generic/word_recip.o \
              p256/bignum_add_p256.o \
              p256/bignum_bigendian_4.o \
@@ -257,6 +262,7 @@ BIGNUM_OBJ = curve25519/bignum_add_p25519.o \
              p256/bignum_mod_n256_4.o \
              p256/bignum_mod_p256.o \
              p256/bignum_mod_p256_4.o \
+             p256/bignum_montinv_p256.o \
              p256/bignum_montmul_p256.o \
              p256/bignum_montmul_p256_alt.o \
              p256/bignum_montmul_p256_neon.o \
@@ -366,7 +372,6 @@ BIGNUM_OBJ = curve25519/bignum_add_p25519.o \
 UNOPT_OBJ = p256/unopt/p256_montjadd.o \
             p256/unopt/p256_montjdouble.o
 
-
 OBJ = $(POINT_OBJ) $(BIGNUM_OBJ)
 
 %.o : %.S ; cat $< | $(PREPROCESS) | $(SPLIT) | $(ASSEMBLE) -o $@ -
@@ -403,6 +408,16 @@ PROOFS = $(OBJ:.o=.correct)
 
 # Cases where a proof uses other proofs for lemmas and/or subroutines
 
+p256/bignum_montmul_p256_neon.correct: proofs/bignum_montmul_p256_neon.ml p256/bignum_montmul_p256_neon.o proofs/bignum_montmul_p256.ml p256/bignum_montmul_p256.o ; ../tools/run-proof.sh arm bignum_montmul_p256_neon "$(HOLLIGHT)" $@
+p384/bignum_montmul_p384_neon.correct: proofs/bignum_montmul_p384_neon.ml p384/bignum_montmul_p384_neon.o proofs/bignum_montmul_p384.ml p384/bignum_montmul_p384.o ; ../tools/run-proof.sh arm bignum_montmul_p384_neon "$(HOLLIGHT)" $@
+p521/bignum_montmul_p521_neon.correct: proofs/bignum_montmul_p521_neon.ml p521/bignum_montmul_p521_neon.o proofs/bignum_montmul_p521.ml p521/bignum_montmul_p521.o ; ../tools/run-proof.sh arm bignum_montmul_p521_neon "$(HOLLIGHT)" $@
+p256/bignum_montsqr_p256_neon.correct: proofs/bignum_montsqr_p256_neon.ml p256/bignum_montsqr_p256_neon.o proofs/bignum_montsqr_p256.ml p256/bignum_montsqr_p256.o ; ../tools/run-proof.sh arm bignum_montsqr_p256_neon "$(HOLLIGHT)" $@
+p384/bignum_montsqr_p384_neon.correct: proofs/bignum_montsqr_p384_neon.ml p384/bignum_montsqr_p384_neon.o proofs/bignum_montsqr_p384.ml p384/bignum_montsqr_p384.o ; ../tools/run-proof.sh arm bignum_montsqr_p384_neon "$(HOLLIGHT)" $@
+p521/bignum_montsqr_p521_neon.correct: proofs/bignum_montsqr_p521_neon.ml p521/bignum_montsqr_p521_neon.o proofs/bignum_montsqr_p521.ml p521/bignum_montsqr_p521.o ; ../tools/run-proof.sh arm bignum_montsqr_p521_neon "$(HOLLIGHT)" $@
+fastmul/bignum_mul_8_16_neon.correct: proofs/bignum_mul_8_16_neon.ml fastmul/bignum_mul_8_16_neon.o proofs/bignum_mul_8_16.ml fastmul/bignum_mul_8_16.o ; ../tools/run-proof.sh arm bignum_mul_8_16_neon "$(HOLLIGHT)" $@
+p521/bignum_mul_p521_neon.correct: proofs/bignum_mul_p521_neon.ml p521/bignum_mul_p521_neon.o proofs/bignum_mul_p521.ml p521/bignum_mul_p521.o ; ../tools/run-proof.sh arm bignum_mul_p521_neon "$(HOLLIGHT)" $@
+fastmul/bignum_sqr_8_16_neon.correct: proofs/bignum_sqr_8_16_neon.ml fastmul/bignum_sqr_8_16_neon.o proofs/bignum_sqr_8_16.ml fastmul/bignum_sqr_8_16.o ; ../tools/run-proof.sh arm bignum_sqr_8_16_neon "$(HOLLIGHT)" $@
+p521/bignum_sqr_p521_neon.correct: proofs/bignum_sqr_p521_neon.ml p521/bignum_sqr_p521_neon.o proofs/bignum_sqr_p521.ml p521/bignum_sqr_p521.o ; ../tools/run-proof.sh arm bignum_sqr_p521_neon "$(HOLLIGHT)" $@
 curve25519/curve25519_x25519.correct: curve25519/bignum_inv_p25519.o proofs/curve25519_x25519.ml curve25519/curve25519_x25519.o ; ../tools/run-proof.sh arm curve25519_x25519 "$(HOLLIGHT)" $@
 curve25519/curve25519_x25519_alt.correct: curve25519/bignum_inv_p25519.o proofs/curve25519_x25519_alt.ml curve25519/curve25519_x25519_alt.o ; ../tools/run-proof.sh arm curve25519_x25519_alt "$(HOLLIGHT)" $@
 curve25519/curve25519_x25519_byte.correct: curve25519/bignum_inv_p25519.o proofs/curve25519_x25519_byte.ml curve25519/curve25519_x25519_byte.o ; ../tools/run-proof.sh arm curve25519_x25519_byte "$(HOLLIGHT)" $@
@@ -416,10 +431,16 @@ curve25519/edwards25519_scalarmulbase_alt.correct: curve25519/bignum_inv_p25519.
 curve25519/edwards25519_scalarmuldouble.correct: curve25519/bignum_inv_p25519.o proofs/edwards25519_scalarmuldouble.ml curve25519/edwards25519_scalarmuldouble.o ; ../tools/run-proof.sh arm edwards25519_scalarmuldouble "$(HOLLIGHT)" $@
 curve25519/edwards25519_scalarmuldouble_alt.correct: curve25519/bignum_inv_p25519.o proofs/edwards25519_scalarmuldouble_alt.ml curve25519/edwards25519_scalarmuldouble_alt.o ; ../tools/run-proof.sh arm edwards25519_scalarmuldouble_alt "$(HOLLIGHT)" $@
 generic/bignum_modexp.correct: generic/bignum_amontifier.correct generic/bignum_amontmul.correct generic/bignum_demont.correct generic/bignum_mux.correct proofs/bignum_modexp.ml generic/bignum_modexp.o ; ../tools/run-proof.sh arm bignum_modexp "$(HOLLIGHT)" $@
-p256/p256_scalarmul.correct: proofs/bignum_demont_p256.ml p256/bignum_demont_p256.o proofs/bignum_inv_p256.ml p256/bignum_inv_p256.o proofs/bignum_montmul_p256.ml p256/bignum_montmul_p256.o proofs/bignum_montsqr_p256.ml p256/bignum_montsqr_p256.o proofs/bignum_tomont_p256.ml p256/bignum_tomont_p256.o proofs/p256_montjadd.ml p256/p256_montjadd.o proofs/p256_montjdouble.ml p256/p256_montjdouble.o proofs/p256_montjmixadd.ml p256/p256_montjmixadd.o proofs/p256_scalarmul.ml p256/p256_scalarmul.o ; ../tools/run-proof.sh arm p256_scalarmul "$(HOLLIGHT)" $@
+p256/p256_montjadd.correct: proofs/p256_montjadd.ml p256/p256_montjadd.o p256/unopt/p256_montjadd.o proofs/bignum_montsqr_p256_neon.ml p256/bignum_montsqr_p256_neon.o proofs/bignum_montsqr_p256.ml p256/bignum_montsqr_p256.o proofs/bignum_montmul_p256_neon.ml p256/bignum_montmul_p256_neon.o proofs/bignum_montmul_p256.ml p256/bignum_montmul_p256.o proofs/bignum_sub_p256.ml p256/bignum_sub_p256.o ; ../tools/run-proof.sh arm p256_montjadd "$(HOLLIGHT)" $@
+p256/p256_montjdouble.correct: proofs/p256_montjdouble.ml p256/p256_montjdouble.o p256/unopt/p256_montjdouble.o proofs/bignum_montsqr_p256_neon.ml p256/bignum_montsqr_p256_neon.o proofs/bignum_montsqr_p256.ml p256/bignum_montsqr_p256.o proofs/bignum_montmul_p256_neon.ml p256/bignum_montmul_p256_neon.o proofs/bignum_montmul_p256.ml p256/bignum_montmul_p256.o proofs/bignum_sub_p256.ml p256/bignum_sub_p256.o proofs/bignum_add_p256.ml p256/bignum_add_p256.o ; ../tools/run-proof.sh arm p256_montjdouble "$(HOLLIGHT)" $@
+p256/p256_montjscalarmul.correct: proofs/p256_montjadd.ml p256/p256_montjadd.o p256/unopt/p256_montjadd.o proofs/p256_montjdouble.ml p256/p256_montjdouble.o p256/unopt/p256_montjdouble.o proofs/bignum_montsqr_p256_neon.ml p256/bignum_montsqr_p256_neon.o proofs/bignum_montsqr_p256.ml p256/bignum_montsqr_p256.o proofs/bignum_montmul_p256_neon.ml p256/bignum_montmul_p256_neon.o proofs/bignum_montmul_p256.ml p256/bignum_montmul_p256.o proofs/bignum_sub_p256.ml p256/bignum_sub_p256.o proofs/bignum_add_p256.ml p256/bignum_add_p256.o proofs/p256_montjscalarmul.ml p256/p256_montjscalarmul.o ; ../tools/run-proof.sh arm p256_montjscalarmul "$(HOLLIGHT)" $@
+p256/p256_montjscalarmul_alt.correct: proofs/p256_montjadd_alt.ml p256/p256_montjadd_alt.o proofs/p256_montjdouble_alt.ml p256/p256_montjdouble_alt.o proofs/p256_montjscalarmul_alt.ml p256/p256_montjscalarmul_alt.o ; ../tools/run-proof.sh arm p256_montjscalarmul_alt "$(HOLLIGHT)" $@
+p256/p256_scalarmul.correct: proofs/bignum_demont_p256.ml p256/bignum_demont_p256.o proofs/bignum_inv_p256.ml p256/bignum_inv_p256.o proofs/bignum_montmul_p256.ml p256/bignum_montmul_p256.o proofs/bignum_montsqr_p256.ml p256/bignum_montsqr_p256.o proofs/bignum_tomont_p256.ml p256/bignum_tomont_p256.o proofs/p256_montjadd.ml p256/p256_montjadd.o p256/unopt/p256_montjadd.o proofs/p256_montjdouble.ml p256/p256_montjdouble.o p256/unopt/p256_montjdouble.o proofs/bignum_montsqr_p256_neon.ml p256/bignum_montsqr_p256_neon.o proofs/bignum_montsqr_p256.ml p256/bignum_montsqr_p256.o proofs/bignum_montmul_p256_neon.ml p256/bignum_montmul_p256_neon.o proofs/bignum_montmul_p256.ml p256/bignum_montmul_p256.o proofs/bignum_sub_p256.ml p256/bignum_sub_p256.o proofs/bignum_add_p256.ml p256/bignum_add_p256.o proofs/p256_montjmixadd.ml p256/p256_montjmixadd.o proofs/p256_scalarmul.ml p256/p256_scalarmul.o ; ../tools/run-proof.sh arm p256_scalarmul "$(HOLLIGHT)" $@
 p256/p256_scalarmul_alt.correct: proofs/bignum_demont_p256.ml p256/bignum_demont_p256.o proofs/bignum_inv_p256.ml p256/bignum_inv_p256.o proofs/bignum_montmul_p256_alt.ml p256/bignum_montmul_p256_alt.o proofs/bignum_montsqr_p256_alt.ml p256/bignum_montsqr_p256_alt.o proofs/bignum_tomont_p256.ml p256/bignum_tomont_p256.o proofs/p256_montjadd_alt.ml p256/p256_montjadd_alt.o proofs/p256_montjdouble_alt.ml p256/p256_montjdouble_alt.o proofs/p256_montjmixadd_alt.ml p256/p256_montjmixadd_alt.o proofs/p256_scalarmul_alt.ml p256/p256_scalarmul_alt.o ; ../tools/run-proof.sh arm p256_scalarmul_alt "$(HOLLIGHT)" $@
 p256/p256_scalarmulbase.correct: proofs/bignum_demont_p256.ml p256/bignum_demont_p256.o proofs/bignum_inv_p256.ml p256/bignum_inv_p256.o proofs/bignum_montmul_p256.ml p256/bignum_montmul_p256.o proofs/bignum_montsqr_p256.ml p256/bignum_montsqr_p256.o proofs/p256_montjmixadd.ml p256/p256_montjmixadd.o proofs/p256_scalarmulbase.ml p256/p256_scalarmulbase.o ; ../tools/run-proof.sh arm p256_scalarmulbase "$(HOLLIGHT)" $@
 p256/p256_scalarmulbase_alt.correct: proofs/bignum_demont_p256.ml p256/bignum_demont_p256.o proofs/bignum_inv_p256.ml p256/bignum_inv_p256.o proofs/bignum_montmul_p256_alt.ml p256/bignum_montmul_p256_alt.o proofs/bignum_montsqr_p256_alt.ml p256/bignum_montsqr_p256_alt.o proofs/p256_montjmixadd_alt.ml p256/p256_montjmixadd_alt.o proofs/p256_scalarmulbase_alt.ml p256/p256_scalarmulbase_alt.o ; ../tools/run-proof.sh arm p256_scalarmulbase_alt "$(HOLLIGHT)" $@
+p384/p384_montjscalarmul.correct: proofs/p384_montjadd.ml p384/p384_montjadd.o proofs/p384_montjdouble.ml p384/p384_montjdouble.o proofs/p384_montjscalarmul.ml p384/p384_montjscalarmul.o ; ../tools/run-proof.sh arm p384_montjscalarmul "$(HOLLIGHT)" $@
+p384/p384_montjscalarmul_alt.correct: proofs/p384_montjadd_alt.ml p384/p384_montjadd_alt.o proofs/p384_montjdouble_alt.ml p384/p384_montjdouble_alt.o proofs/p384_montjscalarmul_alt.ml p384/p384_montjscalarmul_alt.o ; ../tools/run-proof.sh arm p384_montjscalarmul_alt "$(HOLLIGHT)" $@
 
 # All other other instances are standalone
 

diff --git a/arm/generic/Makefile b/arm/generic/Makefile
@@ -93,6 +93,7 @@ OBJ = bignum_add.o \
       word_max.o \
       word_min.o \
       word_negmodinv.o \
+      word_popcount.o \
       word_recip.o
 
 %.o : %.S ; $(CC) -E -I../../include $< | $(GAS) -o $@ -

diff --git a/arm/generic/word_popcount.S b/arm/generic/word_popcount.S
@@ -0,0 +1,41 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT-0
+
+// ----------------------------------------------------------------------------
+// Count number of set bits in a single 64-bit word (population count)
+// Input a; output function return
+//
+//    extern uint64_t word_popcount (uint64_t a);
+//
+// Standard ARM ABI: X0 = a, returns X0
+// ----------------------------------------------------------------------------
+#include "_internal_s2n_bignum.h"
+
+        S2N_BN_SYM_VISIBILITY_DIRECTIVE(word_popcount)
+        S2N_BN_SYM_PRIVACY_DIRECTIVE(word_popcount)
+        .text
+        .balign 4
+
+// Very similar to the traditional algorithm, e.g. Hacker's Delight 5-2
+
+S2N_BN_SYMBOL(word_popcount):
+
+        and     x1, x0, #0xAAAAAAAAAAAAAAAA
+        sub     x0, x0, x1, lsr #1
+
+        bic     x1, x0, #0x3333333333333333
+        and     x0, x0, #0x3333333333333333
+        add     x0, x0, x1, lsr #2
+
+        add     x0, x0, x0, lsr #4
+        and     x0, x0, #0x0F0F0F0F0F0F0F0F
+
+        mov     x1, #0x101010101010101
+        mul     x0, x0, x1
+        lsr     x0, x0, #56
+
+        ret
+
+#if defined(__linux__) && defined(__ELF__)
+.section .note.GNU-stack,"",%progbits
+#endif
diff --git a/arm/p256/Makefile b/arm/p256/Makefile
@@ -34,6 +34,7 @@ OBJ = bignum_add_p256.o \
       bignum_mod_n256_4.o \
       bignum_mod_p256.o \
       bignum_mod_p256_4.o \
+      bignum_montinv_p256.o \
       bignum_montmul_p256.o \
       bignum_montmul_p256_alt.o \
       bignum_montmul_p256_neon.o \
@@ -53,6 +54,8 @@ OBJ = bignum_add_p256.o \
       p256_montjdouble_alt.o \
       p256_montjmixadd.o \
       p256_montjmixadd_alt.o \
+      p256_montjscalarmul.o \
+      p256_montjscalarmul_alt.o \
       p256_scalarmul.o \
       p256_scalarmul_alt.o \
       p256_scalarmulbase.o \