Bug 1376975 - Formally verified Curve25519 (64 bits) from HaCl* r=mt,…

…franziskus

Summary:
This patch replaces the legacy curve25519_64.c code by the formally verified HaCl* code.
The new code has been proven to have functional correctness, memory safety and a set of side-channel resistance properties.

Note: All files from the new `verified` folder are formally verified in F* but for 'kremlib.h' that remains in the trusted code base.

Reviewers: franziskus, ekr, ttaubert, mt

Differential Revision: https://nss-review.dev.mozaws.net/D395

--HG--
extra : rebase_source : b109a642a2d431d01414faff2fadd6f8daae7ec7

lib/freebl/Makefile

@@ -531,15 +531,12 @@ ifeq (,$(filter-out i386 x386 x86 x86_64,$(CPU_ARCH)))
     # All intel architectures get the 64 bit version
     # With custom uint128 if necessary (faster than generic 32 bit version).
     ECL_SRCS += curve25519_64.c
+    VERIFIED_SRCS += hacl_curve25519_64.c
 else
     # All non intel architectures get the generic 32 bit implementation (slow!)
     ECL_SRCS += curve25519_32.c
 endif
 
-ifndef HAVE_INT128_SUPPORT
-    ECL_SRCS += uint128.c
-endif
-
 #######################################################################
 # (5) Execute "global" rules. (OPTIONAL)                              #
 #######################################################################
@@ -563,12 +560,12 @@ rijndael_tables:
 	         $(DEFINES) $(INCLUDES) $(OBJDIR)/libfreebl.a
 	$(OBJDIR)/make_rijndael_tab
 
-vpath %.h mpi ecl
-vpath %.c mpi ecl
+vpath %.h mpi ecl verified
+vpath %.c mpi ecl verified
 vpath %.S mpi ecl
 vpath %.s mpi ecl
 vpath %.asm mpi ecl
-INCLUDES += -Impi -Iecl
+INCLUDES += -Impi -Iecl -Iverified
 
 
 DEFINES += -DMP_API_COMPATIBLE
@@ -587,6 +584,9 @@ ECL_OBJS += $(addprefix $(OBJDIR)/$(PROG_PREFIX), $(ECL_USERS:.c=$(OBJ_SUFFIX)))
 
 $(ECL_OBJS): $(ECL_HDRS)
 
+VERIFIED_OBJS = $(addprefix $(OBJDIR)/$(PROG_PREFIX), $(VERIFIED_SRCS:.c=$(OBJ_SUFFIX)))
+
+$(VERIFIED_OBJS): $(VERIFIED_HDRS)
 
 
 $(OBJDIR)/sysrand$(OBJ_SUFFIX): sysrand.c unix_rand.c win_rand.c