Path	Lines of Code
x86/proofs/base.ml	48
x86/proofs/bignum_add.ml	671
x86/proofs/bignum_add_p256.ml	144
x86/proofs/bignum_add_p256k1.ml	182
x86/proofs/bignum_add_p384.ml	164
x86/proofs/bignum_add_p521.ml	198
x86/proofs/bignum_amontifier.ml	2423
x86/proofs/bignum_amontmul.ml	851
x86/proofs/bignum_amontredc.ml	947
x86/proofs/bignum_amontsqr.ml	822
x86/proofs/bignum_bigendian_4.ml	196
x86/proofs/bignum_bigendian_6.ml	202
x86/proofs/bignum_bitfield.ml	251
x86/proofs/bignum_bitsize.ml	218
x86/proofs/bignum_cdiv.ml	1824
x86/proofs/bignum_cdiv_exact.ml	468
x86/proofs/bignum_cld.ml	208
x86/proofs/bignum_clz.ml	231
x86/proofs/bignum_cmadd.ml	491
x86/proofs/bignum_cmnegadd.ml	466
x86/proofs/bignum_cmod.ml	1293
x86/proofs/bignum_cmul.ml	363
x86/proofs/bignum_cmul_p256.ml	224
x86/proofs/bignum_cmul_p256_alt.ml	224
x86/proofs/bignum_cmul_p256k1.ml	174
x86/proofs/bignum_cmul_p256k1_alt.ml	179
x86/proofs/bignum_cmul_p384.ml	238
x86/proofs/bignum_cmul_p384_alt.ml	236
x86/proofs/bignum_cmul_p521.ml	346
x86/proofs/bignum_coprime.ml	2955
x86/proofs/bignum_copy.ml	172
x86/proofs/bignum_ctd.ml	175
x86/proofs/bignum_ctz.ml	189
x86/proofs/bignum_deamont_p256.ml	220
x86/proofs/bignum_deamont_p256_alt.ml	198
x86/proofs/bignum_deamont_p256k1.ml	220
x86/proofs/bignum_deamont_p384.ml	328
x86/proofs/bignum_deamont_p384_alt.ml	327
x86/proofs/bignum_deamont_p521.ml	305
x86/proofs/bignum_demont.ml	716
x86/proofs/bignum_demont_p256.ml	180
x86/proofs/bignum_demont_p256_alt.ml	166
x86/proofs/bignum_demont_p256k1.ml	160
x86/proofs/bignum_demont_p384.ml	282
x86/proofs/bignum_demont_p384_alt.ml	281
x86/proofs/bignum_demont_p521.ml	179
x86/proofs/bignum_digit.ml	112
x86/proofs/bignum_digitsize.ml	197
x86/proofs/bignum_divmod10.ml	227
x86/proofs/bignum_double_p256.ml	143
x86/proofs/bignum_double_p256k1.ml	202
x86/proofs/bignum_double_p384.ml	163
x86/proofs/bignum_double_p521.ml	139
x86/proofs/bignum_emontredc.ml	516
x86/proofs/bignum_emontredc_8n.ml	1854
x86/proofs/bignum_eq.ml	281
x86/proofs/bignum_even.ml	70
x86/proofs/bignum_ge.ml	398
x86/proofs/bignum_gt.ml	399
x86/proofs/bignum_half_p256.ml	146
x86/proofs/bignum_half_p256k1.ml	151
x86/proofs/bignum_half_p384.ml	158
x86/proofs/bignum_half_p521.ml	178
x86/proofs/bignum_iszero.ml	97
x86/proofs/bignum_kmul_16_32.ml	1803
x86/proofs/bignum_kmul_32_64.ml	3085
x86/proofs/bignum_ksqr_16_32.ml	1200
x86/proofs/bignum_ksqr_32_64.ml	2013
x86/proofs/bignum_le.ml	398
x86/proofs/bignum_littleendian_4.ml	187
x86/proofs/bignum_littleendian_6.ml	191
x86/proofs/bignum_lt.ml	399
x86/proofs/bignum_madd.ml	537
x86/proofs/bignum_mod_n256.ml	438
x86/proofs/bignum_mod_n256_4.ml	130
x86/proofs/bignum_mod_n256_alt.ml	439
x86/proofs/bignum_mod_n256k1_4.ml	130
x86/proofs/bignum_mod_n384.ml	475
x86/proofs/bignum_mod_n384_6.ml	150
x86/proofs/bignum_mod_n384_alt.ml	476
x86/proofs/bignum_mod_n521_9.ml	296
x86/proofs/bignum_mod_p256.ml	421
x86/proofs/bignum_mod_p256_4.ml	126
x86/proofs/bignum_mod_p256_alt.ml	418
x86/proofs/bignum_mod_p256k1_4.ml	179
x86/proofs/bignum_mod_p384.ml	468
x86/proofs/bignum_mod_p384_6.ml	142
x86/proofs/bignum_mod_p384_alt.ml	459
x86/proofs/bignum_mod_p521_9.ml	223
x86/proofs/bignum_modadd.ml	334
x86/proofs/bignum_moddouble.ml	362
x86/proofs/bignum_modifier.ml	2948
x86/proofs/bignum_modinv.ml	4493
x86/proofs/bignum_modoptneg.ml	219
x86/proofs/bignum_modsub.ml	274
x86/proofs/bignum_montifier.ml	2951
x86/proofs/bignum_montmul.ml	922
x86/proofs/bignum_montmul_p256.ml	450
x86/proofs/bignum_montmul_p256_alt.ml	451
x86/proofs/bignum_montmul_p256k1.ml	345
x86/proofs/bignum_montmul_p256k1_alt.ml	329
x86/proofs/bignum_montmul_p384.ml	746
x86/proofs/bignum_montmul_p384_alt.ml	725
x86/proofs/bignum_montmul_p521.ml	889
x86/proofs/bignum_montredc.ml	1036
x86/proofs/bignum_montsqr.ml	894
x86/proofs/bignum_montsqr_p256.ml	427
x86/proofs/bignum_montsqr_p256_alt.ml	415
x86/proofs/bignum_montsqr_p256k1.ml	315
x86/proofs/bignum_montsqr_p256k1_alt.ml	313
x86/proofs/bignum_montsqr_p384.ml	675
x86/proofs/bignum_montsqr_p384_alt.ml	638
x86/proofs/bignum_montsqr_p521.ml	750
x86/proofs/bignum_mul.ml	447
x86/proofs/bignum_mul_4_8.ml	198
x86/proofs/bignum_mul_4_8_alt.ml	169
x86/proofs/bignum_mul_6_12.ml	331
x86/proofs/bignum_mul_6_12_alt.ml	276
x86/proofs/bignum_mul_8_16.ml	496
x86/proofs/bignum_mul_p256k1.ml	319
x86/proofs/bignum_mul_p256k1_alt.ml	303
x86/proofs/bignum_mul_p521.ml	786
x86/proofs/bignum_muladd10.ml	163
x86/proofs/bignum_mux.ml	132
x86/proofs/bignum_mux16.ml	270
x86/proofs/bignum_mux_4.ml	96
x86/proofs/bignum_mux_6.ml	104
x86/proofs/bignum_neg_p256.ml	118
x86/proofs/bignum_neg_p256k1.ml	114
x86/proofs/bignum_neg_p384.ml	125
x86/proofs/bignum_neg_p521.ml	142
x86/proofs/bignum_negmodinv.ml	626
x86/proofs/bignum_nonzero.ml	96
x86/proofs/bignum_nonzero_4.ml	72
x86/proofs/bignum_nonzero_6.ml	74
x86/proofs/bignum_normalize.ml	452
x86/proofs/bignum_odd.ml	68
x86/proofs/bignum_of_word.ml	118
x86/proofs/bignum_optadd.ml	183
x86/proofs/bignum_optneg.ml	196
x86/proofs/bignum_optneg_p256.ml	146
x86/proofs/bignum_optneg_p256k1.ml	142
x86/proofs/bignum_optneg_p384.ml	160
x86/proofs/bignum_optneg_p521.ml	151
x86/proofs/bignum_optsub.ml	197
x86/proofs/bignum_optsubadd.ml	265
x86/proofs/bignum_pow2.ml	143
x86/proofs/bignum_shl_small.ml	287
x86/proofs/bignum_shr_small.ml	279
x86/proofs/bignum_sqr.ml	573
x86/proofs/bignum_sqr_4_8.ml	166
x86/proofs/bignum_sqr_4_8_alt.ml	151
x86/proofs/bignum_sqr_6_12.ml	260
x86/proofs/bignum_sqr_6_12_alt.ml	232
x86/proofs/bignum_sqr_8_16.ml	375
x86/proofs/bignum_sqr_p256k1.ml	287
x86/proofs/bignum_sqr_p256k1_alt.ml	287
x86/proofs/bignum_sqr_p521.ml	640
x86/proofs/bignum_sub.ml	722
x86/proofs/bignum_sub_p256.ml	137
x86/proofs/bignum_sub_p256k1.ml	135
x86/proofs/bignum_sub_p384.ml	149
x86/proofs/bignum_sub_p521.ml	162
x86/proofs/bignum_tomont_p256.ml	366
x86/proofs/bignum_tomont_p256_alt.ml	323
x86/proofs/bignum_tomont_p256k1.ml	170
x86/proofs/bignum_tomont_p256k1_alt.ml	178
x86/proofs/bignum_tomont_p384.ml	527
x86/proofs/bignum_tomont_p384_alt.ml	511
x86/proofs/bignum_tomont_p521.ml	314
x86/proofs/bignum_triple_p256.ml	226
x86/proofs/bignum_triple_p256_alt.ml	212
x86/proofs/bignum_triple_p256k1.ml	191
x86/proofs/bignum_triple_p256k1_alt.ml	180
x86/proofs/bignum_triple_p384.ml	243
x86/proofs/bignum_triple_p384_alt.ml	232
x86/proofs/bignum_triple_p521.ml	339
x86/proofs/decode.ml	1912
x86/proofs/instruction.ml	399
x86/proofs/make.ml	158
x86/proofs/word_bytereverse.ml	63
x86/proofs/word_clz.ml	67
x86/proofs/word_ctz.ml	61
x86/proofs/word_max.ml	58
x86/proofs/word_min.ml	58
x86/proofs/word_negmodinv.ml	117
x86/proofs/word_recip.ml	652
x86/proofs/x86.ml	2371