Path	Lines of Code
arm/fastmul/bignum_emontredc_8n.S	321
arm/fastmul/bignum_kmul_16_32.S	748
arm/fastmul/bignum_kmul_32_64.S	1013
arm/fastmul/bignum_ksqr_16_32.S	513
arm/fastmul/bignum_ksqr_32_64.S	696
arm/fastmul/bignum_mul_4_8.S	155
arm/fastmul/bignum_mul_4_8_alt.S	128
arm/fastmul/bignum_mul_6_12.S	234
arm/fastmul/bignum_mul_6_12_alt.S	227
arm/fastmul/bignum_mul_8_16.S	292
arm/fastmul/bignum_sqr_4_8.S	136
arm/fastmul/bignum_sqr_4_8_alt.S	103
arm/fastmul/bignum_sqr_6_12.S	225
arm/fastmul/bignum_sqr_6_12_alt.S	162
arm/fastmul/bignum_sqr_8_16.S	319
arm/generic/bignum_add.S	117
arm/generic/bignum_amontifier.S	349
arm/generic/bignum_amontmul.S	162
arm/generic/bignum_amontredc.S	157
arm/generic/bignum_amontsqr.S	161
arm/generic/bignum_bitfield.S	82
arm/generic/bignum_bitsize.S	64
arm/generic/bignum_cdiv.S	235
arm/generic/bignum_cdiv_exact.S	138
arm/generic/bignum_cld.S	51
arm/generic/bignum_clz.S	65
arm/generic/bignum_cmadd.S	102
arm/generic/bignum_cmnegadd.S	112
arm/generic/bignum_cmod.S	158
arm/generic/bignum_cmul.S	94
arm/generic/bignum_coprime.S	370
arm/generic/bignum_copy.S	58
arm/generic/bignum_ctd.S	50
arm/generic/bignum_ctz.S	69
arm/generic/bignum_demont.S	140
arm/generic/bignum_digit.S	55
arm/generic/bignum_digitsize.S	51
arm/generic/bignum_divmod10.S	66
arm/generic/bignum_emontredc.S	100
arm/generic/bignum_eq.S	74
arm/generic/bignum_even.S	35
arm/generic/bignum_ge.S	84
arm/generic/bignum_gt.S	84
arm/generic/bignum_iszero.S	44
arm/generic/bignum_le.S	84
arm/generic/bignum_lt.S	84
arm/generic/bignum_madd.S	106
arm/generic/bignum_modadd.S	79
arm/generic/bignum_moddouble.S	70
arm/generic/bignum_modifier.S	412
arm/generic/bignum_modinv.S	508
arm/generic/bignum_modoptneg.S	71
arm/generic/bignum_modsub.S	67
arm/generic/bignum_montifier.S	411
arm/generic/bignum_montmul.S	171
arm/generic/bignum_montredc.S	171
arm/generic/bignum_montsqr.S	170
arm/generic/bignum_mul.S	98
arm/generic/bignum_muladd10.S	59
arm/generic/bignum_mux.S	50
arm/generic/bignum_mux16.S	62
arm/generic/bignum_negmodinv.S	123
arm/generic/bignum_nonzero.S	44
arm/generic/bignum_normalize.S	98
arm/generic/bignum_odd.S	34
arm/generic/bignum_of_word.S	45
arm/generic/bignum_optadd.S	63
arm/generic/bignum_optneg.S	63
arm/generic/bignum_optsub.S	63
arm/generic/bignum_optsubadd.S	78
arm/generic/bignum_pow2.S	56
arm/generic/bignum_shl_small.S	88
arm/generic/bignum_shr_small.S	81
arm/generic/bignum_sqr.S	118
arm/generic/bignum_sub.S	114
arm/generic/word_bytereverse.S	42
arm/generic/word_clz.S	31
arm/generic/word_ctz.S	40
arm/generic/word_max.S	34
arm/generic/word_min.S	34
arm/generic/word_negmodinv.S	68
arm/generic/word_recip.S	104
arm/p256/bignum_add_p256.S	74
arm/p256/bignum_bigendian_4.S	127
arm/p256/bignum_cmul_p256.S	113
arm/p256/bignum_deamont_p256.S	95
arm/p256/bignum_demont_p256.S	79
arm/p256/bignum_double_p256.S	69
arm/p256/bignum_half_p256.S	67
arm/p256/bignum_littleendian_4.S	125
arm/p256/bignum_mod_n256.S	143
arm/p256/bignum_mod_n256_4.S	71
arm/p256/bignum_mod_p256.S	129
arm/p256/bignum_mod_p256_4.S	62
arm/p256/bignum_montmul_p256.S	241
arm/p256/bignum_montmul_p256_alt.S	176
arm/p256/bignum_montsqr_p256.S	216
arm/p256/bignum_montsqr_p256_alt.S	145
arm/p256/bignum_mux_4.S	56
arm/p256/bignum_neg_p256.S	62
arm/p256/bignum_nonzero_4.S	43
arm/p256/bignum_optneg_p256.S	72
arm/p256/bignum_sub_p256.S	64
arm/p256/bignum_tomont_p256.S	107
arm/p256/bignum_triple_p256.S	94
arm/p384/bignum_add_p384.S	86
arm/p384/bignum_bigendian_6.S	162
arm/p384/bignum_cmul_p384.S	128
arm/p384/bignum_deamont_p384.S	124
arm/p384/bignum_demont_p384.S	100
arm/p384/bignum_double_p384.S	82
arm/p384/bignum_half_p384.S	76
arm/p384/bignum_littleendian_6.S	161
arm/p384/bignum_mod_n384.S	165
arm/p384/bignum_mod_n384_6.S	80
arm/p384/bignum_mod_p384.S	148
arm/p384/bignum_mod_p384_6.S	73
arm/p384/bignum_montmul_p384.S	355
arm/p384/bignum_montmul_p384_alt.S	294
arm/p384/bignum_montsqr_p384.S	315
arm/p384/bignum_montsqr_p384_alt.S	228
arm/p384/bignum_mux_6.S	64
arm/p384/bignum_neg_p384.S	72
arm/p384/bignum_nonzero_6.S	46
arm/p384/bignum_optneg_p384.S	85
arm/p384/bignum_sub_p384.S	74
arm/p384/bignum_tomont_p384.S	122
arm/p384/bignum_triple_p384.S	111
arm/p521/bignum_add_p521.S	89
arm/p521/bignum_cmul_p521.S	129
arm/p521/bignum_deamont_p521.S	105
arm/p521/bignum_demont_p521.S	70
arm/p521/bignum_double_p521.S	62
arm/p521/bignum_half_p521.S	67
arm/p521/bignum_mod_n521_9.S	127
arm/p521/bignum_mod_p521_9.S	89
arm/p521/bignum_montmul_p521.S	513
arm/p521/bignum_montsqr_p521.S	551
arm/p521/bignum_mul_p521.S	512
arm/p521/bignum_neg_p521.S	78
arm/p521/bignum_optneg_p521.S	83
arm/p521/bignum_sqr_p521.S	531
arm/p521/bignum_sub_p521.S	84
arm/p521/bignum_tomont_p521.S	107
arm/p521/bignum_triple_p521.S	97
arm/proofs/arm.ml	660
arm/proofs/base.ml	48
arm/proofs/bignum_add.ml	632
arm/proofs/bignum_add_p256.ml	168
arm/proofs/bignum_add_p256k1.ml	171
arm/proofs/bignum_add_p384.ml	179
arm/proofs/bignum_add_p521.ml	165
arm/proofs/bignum_amontifier.ml	2226
arm/proofs/bignum_amontmul.ml	741
arm/proofs/bignum_amontredc.ml	858
arm/proofs/bignum_amontsqr.ml	732
arm/proofs/bignum_bigendian_4.ml	232
arm/proofs/bignum_bigendian_6.ml	266
arm/proofs/bignum_bitfield.ml	243
arm/proofs/bignum_bitsize.ml	220
arm/proofs/bignum_cdiv.ml	1746
arm/proofs/bignum_cdiv_exact.ml	495
arm/proofs/bignum_cld.ml	206
arm/proofs/bignum_clz.ml	222
arm/proofs/bignum_cmadd.ml	428
arm/proofs/bignum_cmnegadd.ml	451
arm/proofs/bignum_cmod.ml	1204
arm/proofs/bignum_cmul.ml	384
arm/proofs/bignum_cmul_p256.ml	221
arm/proofs/bignum_cmul_p256k1.ml	167
arm/proofs/bignum_cmul_p384.ml	238
arm/proofs/bignum_cmul_p521.ml	299
arm/proofs/bignum_coprime.ml	3250
arm/proofs/bignum_copy.ml	168
arm/proofs/bignum_ctd.ml	154
arm/proofs/bignum_ctz.ml	172
arm/proofs/bignum_deamont_p256.ml	167
arm/proofs/bignum_deamont_p256k1.ml	201
arm/proofs/bignum_deamont_p384.ml	475
arm/proofs/bignum_deamont_p521.ml	317
arm/proofs/bignum_demont.ml	646
arm/proofs/bignum_demont_p256.ml	133
arm/proofs/bignum_demont_p256k1.ml	145
arm/proofs/bignum_demont_p384.ml	430
arm/proofs/bignum_demont_p521.ml	160
arm/proofs/bignum_digit.ml	110
arm/proofs/bignum_digitsize.ml	198
arm/proofs/bignum_divmod10.ml	208
arm/proofs/bignum_double_p256.ml	122
arm/proofs/bignum_double_p256k1.ml	188
arm/proofs/bignum_double_p384.ml	133
arm/proofs/bignum_double_p521.ml	119
arm/proofs/bignum_emontredc.ml	471
arm/proofs/bignum_emontredc_8n.ml	1140
arm/proofs/bignum_eq.ml	272
arm/proofs/bignum_even.ml	68
arm/proofs/bignum_ge.ml	358
arm/proofs/bignum_gt.ml	358
arm/proofs/bignum_half_p256.ml	134
arm/proofs/bignum_half_p256k1.ml	138
arm/proofs/bignum_half_p384.ml	140
arm/proofs/bignum_half_p521.ml	157
arm/proofs/bignum_iszero.ml	91
arm/proofs/bignum_kmul_16_32.ml	1271
arm/proofs/bignum_kmul_32_64.ml	2097
arm/proofs/bignum_ksqr_16_32.ml	845
arm/proofs/bignum_ksqr_32_64.ml	1461
arm/proofs/bignum_le.ml	358
arm/proofs/bignum_littleendian_4.ml	228
arm/proofs/bignum_littleendian_6.ml	261
arm/proofs/bignum_lt.ml	358
arm/proofs/bignum_madd.ml	499
arm/proofs/bignum_mod_n256.ml	400
arm/proofs/bignum_mod_n256_4.ml	117
arm/proofs/bignum_mod_n256k1_4.ml	119
arm/proofs/bignum_mod_n384.ml	420
arm/proofs/bignum_mod_n384_6.ml	128
arm/proofs/bignum_mod_n521_9.ml	258
arm/proofs/bignum_mod_p256.ml	404
arm/proofs/bignum_mod_p256_4.ml	111
arm/proofs/bignum_mod_p256k1_4.ml	168
arm/proofs/bignum_mod_p384.ml	476
arm/proofs/bignum_mod_p384_6.ml	118
arm/proofs/bignum_mod_p521_9.ml	214
arm/proofs/bignum_modadd.ml	326
arm/proofs/bignum_moddouble.ml	345
arm/proofs/bignum_modifier.ml	2715
arm/proofs/bignum_modinv.ml	4606
arm/proofs/bignum_modoptneg.ml	205
arm/proofs/bignum_modsub.ml	269
arm/proofs/bignum_montifier.ml	2719
arm/proofs/bignum_montmul.ml	814
arm/proofs/bignum_montmul_p256.ml	1082
arm/proofs/bignum_montmul_p256_alt.ml	371
arm/proofs/bignum_montmul_p256k1.ml	697
arm/proofs/bignum_montmul_p256k1_alt.ml	331
arm/proofs/bignum_montmul_p384.ml	1628
arm/proofs/bignum_montmul_p384_alt.ml	603
arm/proofs/bignum_montmul_p521.ml	1637
arm/proofs/bignum_montredc.ml	941
arm/proofs/bignum_montsqr.ml	798
arm/proofs/bignum_montsqr_p256.ml	500
arm/proofs/bignum_montsqr_p256_alt.ml	340
arm/proofs/bignum_montsqr_p256k1.ml	353
arm/proofs/bignum_montsqr_p256k1_alt.ml	298
arm/proofs/bignum_montsqr_p384.ml	1011
arm/proofs/bignum_montsqr_p384_alt.ml	537
arm/proofs/bignum_montsqr_p521.ml	1234
arm/proofs/bignum_mul.ml	429
arm/proofs/bignum_mul_4_8.ml	257
arm/proofs/bignum_mul_4_8_alt.ml	146
arm/proofs/bignum_mul_6_12.ml	562
arm/proofs/bignum_mul_6_12_alt.ml	242
arm/proofs/bignum_mul_8_16.ml	772
arm/proofs/bignum_mul_p256k1.ml	452
arm/proofs/bignum_mul_p256k1_alt.ml	262
arm/proofs/bignum_mul_p521.ml	1630
arm/proofs/bignum_muladd10.ml	169
arm/proofs/bignum_mux.ml	116
arm/proofs/bignum_mux16.ml	259
arm/proofs/bignum_mux_4.ml	93
arm/proofs/bignum_mux_6.ml	101
arm/proofs/bignum_neg_p256.ml	107
arm/proofs/bignum_neg_p256k1.ml	106
arm/proofs/bignum_neg_p384.ml	115
arm/proofs/bignum_neg_p521.ml	127
arm/proofs/bignum_negmodinv.ml	579
arm/proofs/bignum_nonzero.ml	91
arm/proofs/bignum_nonzero_4.ml	68
arm/proofs/bignum_nonzero_6.ml	71
arm/proofs/bignum_normalize.ml	455
arm/proofs/bignum_odd.ml	65
arm/proofs/bignum_of_word.ml	110
arm/proofs/bignum_optadd.ml	173
arm/proofs/bignum_optneg.ml	182
arm/proofs/bignum_optneg_p256.ml	129
arm/proofs/bignum_optneg_p256k1.ml	136
arm/proofs/bignum_optneg_p384.ml	140
arm/proofs/bignum_optneg_p521.ml	136
arm/proofs/bignum_optsub.ml	182
arm/proofs/bignum_optsubadd.ml	248
arm/proofs/bignum_pow2.ml	133
arm/proofs/bignum_shl_small.ml	324
arm/proofs/bignum_shr_small.ml	345
arm/proofs/bignum_sqr.ml	559
arm/proofs/bignum_sqr_4_8.ml	182
arm/proofs/bignum_sqr_4_8_alt.ml	120
arm/proofs/bignum_sqr_6_12.ml	277
arm/proofs/bignum_sqr_6_12_alt.ml	177
arm/proofs/bignum_sqr_8_16.ml	488
arm/proofs/bignum_sqr_p256k1.ml	376
arm/proofs/bignum_sqr_p256k1_alt.ml	237
arm/proofs/bignum_sqr_p521.ml	1128
arm/proofs/bignum_sub.ml	715
arm/proofs/bignum_sub_p256.ml	134
arm/proofs/bignum_sub_p256k1.ml	129
arm/proofs/bignum_sub_p384.ml	142
arm/proofs/bignum_sub_p521.ml	138
arm/proofs/bignum_tomont_p256.ml	413
arm/proofs/bignum_tomont_p256k1.ml	168
arm/proofs/bignum_tomont_p384.ml	499
arm/proofs/bignum_tomont_p521.ml	306
arm/proofs/bignum_triple_p256.ml	194
arm/proofs/bignum_triple_p256k1.ml	170
arm/proofs/bignum_triple_p384.ml	210
arm/proofs/bignum_triple_p521.ml	254
arm/proofs/decode.ml	865
arm/proofs/instruction.ml	1160
arm/proofs/make.ml	158
arm/proofs/word_bytereverse.ml	73
arm/proofs/word_clz.ml	53
arm/proofs/word_ctz.ml	59
arm/proofs/word_max.ml	55
arm/proofs/word_min.ml	55
arm/proofs/word_negmodinv.ml	98
arm/proofs/word_recip.ml	605
arm/secp256k1/bignum_add_p256k1.S	71
arm/secp256k1/bignum_cmul_p256k1.S	85
arm/secp256k1/bignum_deamont_p256k1.S	97
arm/secp256k1/bignum_demont_p256k1.S	76
arm/secp256k1/bignum_double_p256k1.S	68
arm/secp256k1/bignum_half_p256k1.S	63
arm/secp256k1/bignum_mod_n256k1_4.S	71
arm/secp256k1/bignum_mod_p256k1_4.S	60
arm/secp256k1/bignum_montmul_p256k1.S	238
arm/secp256k1/bignum_montmul_p256k1_alt.S	192
arm/secp256k1/bignum_montsqr_p256k1.S	164
arm/secp256k1/bignum_montsqr_p256k1_alt.S	158
arm/secp256k1/bignum_mul_p256k1.S	208
arm/secp256k1/bignum_mul_p256k1_alt.S	168
arm/secp256k1/bignum_neg_p256k1.S	60
arm/secp256k1/bignum_optneg_p256k1.S	68
arm/secp256k1/bignum_sqr_p256k1.S	181
arm/secp256k1/bignum_sqr_p256k1_alt.S	143
arm/secp256k1/bignum_sub_p256k1.S	64
arm/secp256k1/bignum_tomont_p256k1.S	89
arm/secp256k1/bignum_triple_p256k1.S	86
benchmarks/benchmark.c	594
codebuild/cloudformation.yml	369
codebuild/proofs.yml	16
codebuild/tests.yml	9
common/bignum.ml	788
common/components.ml	2555
common/elf.ml	134
common/for_hollight.ml	158
common/interval.ml	980
common/misc.ml	955
common/overlap.ml	639
common/records.ml	137
common/relational.ml	2312
common/words2.ml	401
include/s2n-bignum-c89.h	191
include/s2n-bignum.h	191
x86/fastmul/bignum_emontredc_8n.S	348
x86/fastmul/bignum_kmul_16_32.S	416
x86/fastmul/bignum_kmul_32_64.S	1099
x86/fastmul/bignum_ksqr_16_32.S	450
x86/fastmul/bignum_ksqr_32_64.S	756
x86/fastmul/bignum_mul_4_8.S	127
x86/fastmul/bignum_mul_4_8_alt.S	104
x86/fastmul/bignum_mul_6_12.S	161
x86/fastmul/bignum_mul_6_12_alt.S	135
x86/fastmul/bignum_mul_8_16.S	208
x86/fastmul/bignum_sqr_4_8.S	114
x86/fastmul/bignum_sqr_4_8_alt.S	97
x86/fastmul/bignum_sqr_6_12.S	178
x86/fastmul/bignum_sqr_6_12_alt.S	143
x86/fastmul/bignum_sqr_8_16.S	252
x86/generic/bignum_add.S	120
x86/generic/bignum_amontifier.S	403
x86/generic/bignum_amontmul.S	195
x86/generic/bignum_amontredc.S	194
x86/generic/bignum_amontsqr.S	187
x86/generic/bignum_bitfield.S	90
x86/generic/bignum_bitsize.S	68
x86/generic/bignum_cdiv.S	274
x86/generic/bignum_cdiv_exact.S	149
x86/generic/bignum_cld.S	54
x86/generic/bignum_clz.S	68
x86/generic/bignum_cmadd.S	105
x86/generic/bignum_cmnegadd.S	113
x86/generic/bignum_cmod.S	186
x86/generic/bignum_cmul.S	96
x86/generic/bignum_coprime.S	417
x86/generic/bignum_copy.S	58
x86/generic/bignum_ctd.S	54
x86/generic/bignum_ctz.S	67
x86/generic/bignum_demont.S	161
x86/generic/bignum_digit.S	55
x86/generic/bignum_digitsize.S	52
x86/generic/bignum_divmod10.S	71
x86/generic/bignum_emontredc.S	121
x86/generic/bignum_eq.S	73
x86/generic/bignum_even.S	37
x86/generic/bignum_ge.S	84
x86/generic/bignum_gt.S	84
x86/generic/bignum_iszero.S	45
x86/generic/bignum_le.S	84
x86/generic/bignum_lt.S	84
x86/generic/bignum_madd.S	121
x86/generic/bignum_modadd.S	78
x86/generic/bignum_moddouble.S	73
x86/generic/bignum_modifier.S	471
x86/generic/bignum_modinv.S	587
x86/generic/bignum_modoptneg.S	74
x86/generic/bignum_modsub.S	67
x86/generic/bignum_montifier.S	470
x86/generic/bignum_montmul.S	204
x86/generic/bignum_montredc.S	208
x86/generic/bignum_montsqr.S	196
x86/generic/bignum_mul.S	116
x86/generic/bignum_muladd10.S	61
x86/generic/bignum_mux.S	53
x86/generic/bignum_mux16.S	68
x86/generic/bignum_negmodinv.S	150
x86/generic/bignum_nonzero.S	45
x86/generic/bignum_normalize.S	100
x86/generic/bignum_odd.S	36
x86/generic/bignum_of_word.S	52
x86/generic/bignum_optadd.S	66
x86/generic/bignum_optneg.S	66
x86/generic/bignum_optsub.S	67
x86/generic/bignum_optsubadd.S	81
x86/generic/bignum_pow2.S	60
x86/generic/bignum_shl_small.S	90
x86/generic/bignum_shr_small.S	82
x86/generic/bignum_sqr.S	139
x86/generic/bignum_sub.S	114
x86/generic/word_bytereverse.S	32
x86/generic/word_clz.S	37
x86/generic/word_ctz.S	36
x86/generic/word_max.S	35
x86/generic/word_min.S	35
x86/generic/word_negmodinv.S	60
x86/generic/word_recip.S	117
x86/p256/bignum_add_p256.S	76
x86/p256/bignum_bigendian_4.S	70
x86/p256/bignum_cmul_p256.S	100
x86/p256/bignum_cmul_p256_alt.S	114
x86/p256/bignum_deamont_p256.S	107
x86/p256/bignum_deamont_p256_alt.S	123
x86/p256/bignum_demont_p256.S	84
x86/p256/bignum_demont_p256_alt.S	102
x86/p256/bignum_double_p256.S	76
x86/p256/bignum_half_p256.S	68
x86/p256/bignum_littleendian_4.S	57
x86/p256/bignum_mod_n256.S	155
x86/p256/bignum_mod_n256_4.S	75
x86/p256/bignum_mod_n256_alt.S	159
x86/p256/bignum_mod_p256.S	148
x86/p256/bignum_mod_p256_4.S	67
x86/p256/bignum_mod_p256_alt.S	150
x86/p256/bignum_montmul_p256.S	152
x86/p256/bignum_montmul_p256_alt.S	168
x86/p256/bignum_montsqr_p256.S	153
x86/p256/bignum_montsqr_p256_alt.S	174
x86/p256/bignum_mux_4.S	57
x86/p256/bignum_neg_p256.S	71
x86/p256/bignum_nonzero_4.S	43
x86/p256/bignum_optneg_p256.S	79
x86/p256/bignum_sub_p256.S	67
x86/p256/bignum_tomont_p256.S	151
x86/p256/bignum_tomont_p256_alt.S	158
x86/p256/bignum_triple_p256.S	104
x86/p256/bignum_triple_p256_alt.S	106
x86/p384/bignum_add_p384.S	100
x86/p384/bignum_bigendian_6.S	77
x86/p384/bignum_cmul_p384.S	123
x86/p384/bignum_cmul_p384_alt.S	140
x86/p384/bignum_deamont_p384.S	137
x86/p384/bignum_deamont_p384_alt.S	137
x86/p384/bignum_demont_p384.S	103
x86/p384/bignum_demont_p384_alt.S	103
x86/p384/bignum_double_p384.S	99
x86/p384/bignum_half_p384.S	80
x86/p384/bignum_littleendian_6.S	61
x86/p384/bignum_mod_n384.S	179
x86/p384/bignum_mod_n384_6.S	89
x86/p384/bignum_mod_n384_alt.S	183
x86/p384/bignum_mod_p384.S	177
x86/p384/bignum_mod_p384_6.S	87
x86/p384/bignum_mod_p384_alt.S	179
x86/p384/bignum_montmul_p384.S	230
x86/p384/bignum_montmul_p384_alt.S	245
x86/p384/bignum_montsqr_p384.S	240
x86/p384/bignum_montsqr_p384_alt.S	278
x86/p384/bignum_mux_6.S	65
x86/p384/bignum_neg_p384.S	74
x86/p384/bignum_nonzero_6.S	45
x86/p384/bignum_optneg_p384.S	93
x86/p384/bignum_sub_p384.S	86
x86/p384/bignum_tomont_p384.S	230
x86/p384/bignum_tomont_p384_alt.S	251
x86/p384/bignum_triple_p384.S	119
x86/p384/bignum_triple_p384_alt.S	124
x86/p521/bignum_add_p521.S	99
x86/p521/bignum_cmul_p521.S	136
x86/p521/bignum_deamont_p521.S	121
x86/p521/bignum_demont_p521.S	78
x86/p521/bignum_double_p521.S	69
x86/p521/bignum_half_p521.S	77
x86/p521/bignum_mod_n521_9.S	120
x86/p521/bignum_mod_p521_9.S	95
x86/p521/bignum_montmul_p521.S	376
x86/p521/bignum_montsqr_p521.S	276
x86/p521/bignum_mul_p521.S	355
x86/p521/bignum_neg_p521.S	84
x86/p521/bignum_optneg_p521.S	88
x86/p521/bignum_sqr_p521.S	254
x86/p521/bignum_sub_p521.S	92
x86/p521/bignum_tomont_p521.S	111
x86/p521/bignum_triple_p521.S	128
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
x86/secp256k1/bignum_add_p256k1.S	76
x86/secp256k1/bignum_cmul_p256k1.S	80
x86/secp256k1/bignum_cmul_p256k1_alt.S	89
x86/secp256k1/bignum_deamont_p256k1.S	114
x86/secp256k1/bignum_demont_p256k1.S	87
x86/secp256k1/bignum_double_p256k1.S	74
x86/secp256k1/bignum_half_p256k1.S	67
x86/secp256k1/bignum_mod_n256k1_4.S	75
x86/secp256k1/bignum_mod_p256k1_4.S	64
x86/secp256k1/bignum_montmul_p256k1.S	178
x86/secp256k1/bignum_montmul_p256k1_alt.S	175
x86/secp256k1/bignum_montsqr_p256k1.S	167
x86/secp256k1/bignum_montsqr_p256k1_alt.S	163
x86/secp256k1/bignum_mul_p256k1.S	139
x86/secp256k1/bignum_mul_p256k1_alt.S	157
x86/secp256k1/bignum_neg_p256k1.S	65
x86/secp256k1/bignum_optneg_p256k1.S	72
x86/secp256k1/bignum_sqr_p256k1.S	137
x86/secp256k1/bignum_sqr_p256k1_alt.S	146
x86/secp256k1/bignum_sub_p256k1.S	66
x86/secp256k1/bignum_tomont_p256k1.S	80
x86/secp256k1/bignum_tomont_p256k1_alt.S	89
x86/secp256k1/bignum_triple_p256k1.S	93
x86/secp256k1/bignum_triple_p256k1_alt.S	94
x86_att/attrofy.sed	80
x86_att/fastmul/bignum_emontredc_8n.S	347
x86_att/fastmul/bignum_kmul_16_32.S	415
x86_att/fastmul/bignum_kmul_32_64.S	1098
x86_att/fastmul/bignum_ksqr_16_32.S	449
x86_att/fastmul/bignum_ksqr_32_64.S	755
x86_att/fastmul/bignum_mul_4_8.S	126
x86_att/fastmul/bignum_mul_4_8_alt.S	103
x86_att/fastmul/bignum_mul_6_12.S	160
x86_att/fastmul/bignum_mul_6_12_alt.S	134
x86_att/fastmul/bignum_mul_8_16.S	207
x86_att/fastmul/bignum_sqr_4_8.S	113
x86_att/fastmul/bignum_sqr_4_8_alt.S	96
x86_att/fastmul/bignum_sqr_6_12.S	177
x86_att/fastmul/bignum_sqr_6_12_alt.S	142
x86_att/fastmul/bignum_sqr_8_16.S	251
x86_att/generic/bignum_add.S	119
x86_att/generic/bignum_amontifier.S	402
x86_att/generic/bignum_amontmul.S	194
x86_att/generic/bignum_amontredc.S	193
x86_att/generic/bignum_amontsqr.S	186
x86_att/generic/bignum_bitfield.S	89
x86_att/generic/bignum_bitsize.S	67
x86_att/generic/bignum_cdiv.S	273
x86_att/generic/bignum_cdiv_exact.S	148
x86_att/generic/bignum_cld.S	53
x86_att/generic/bignum_clz.S	67
x86_att/generic/bignum_cmadd.S	104
x86_att/generic/bignum_cmnegadd.S	112
x86_att/generic/bignum_cmod.S	185
x86_att/generic/bignum_cmul.S	95
x86_att/generic/bignum_coprime.S	416
x86_att/generic/bignum_copy.S	57
x86_att/generic/bignum_ctd.S	53
x86_att/generic/bignum_ctz.S	66
x86_att/generic/bignum_demont.S	160
x86_att/generic/bignum_digit.S	54
x86_att/generic/bignum_digitsize.S	51
x86_att/generic/bignum_divmod10.S	70
x86_att/generic/bignum_emontredc.S	120
x86_att/generic/bignum_eq.S	72
x86_att/generic/bignum_even.S	36
x86_att/generic/bignum_ge.S	83
x86_att/generic/bignum_gt.S	83
x86_att/generic/bignum_iszero.S	44
x86_att/generic/bignum_le.S	83
x86_att/generic/bignum_lt.S	83
x86_att/generic/bignum_madd.S	120
x86_att/generic/bignum_modadd.S	77
x86_att/generic/bignum_moddouble.S	72
x86_att/generic/bignum_modifier.S	470
x86_att/generic/bignum_modinv.S	586
x86_att/generic/bignum_modoptneg.S	73
x86_att/generic/bignum_modsub.S	66
x86_att/generic/bignum_montifier.S	469
x86_att/generic/bignum_montmul.S	203
x86_att/generic/bignum_montredc.S	207
x86_att/generic/bignum_montsqr.S	195
x86_att/generic/bignum_mul.S	115
x86_att/generic/bignum_muladd10.S	60
x86_att/generic/bignum_mux.S	52
x86_att/generic/bignum_mux16.S	67
x86_att/generic/bignum_negmodinv.S	149
x86_att/generic/bignum_nonzero.S	44
x86_att/generic/bignum_normalize.S	99
x86_att/generic/bignum_odd.S	35
x86_att/generic/bignum_of_word.S	51
x86_att/generic/bignum_optadd.S	65
x86_att/generic/bignum_optneg.S	65
x86_att/generic/bignum_optsub.S	66
x86_att/generic/bignum_optsubadd.S	80
x86_att/generic/bignum_pow2.S	59
x86_att/generic/bignum_shl_small.S	89
x86_att/generic/bignum_shr_small.S	81
x86_att/generic/bignum_sqr.S	138
x86_att/generic/bignum_sub.S	113
x86_att/generic/word_bytereverse.S	31
x86_att/generic/word_clz.S	36
x86_att/generic/word_ctz.S	35
x86_att/generic/word_max.S	34
x86_att/generic/word_min.S	34
x86_att/generic/word_negmodinv.S	59
x86_att/generic/word_recip.S	116
x86_att/p256/bignum_add_p256.S	75
x86_att/p256/bignum_bigendian_4.S	69
x86_att/p256/bignum_cmul_p256.S	99
x86_att/p256/bignum_cmul_p256_alt.S	113
x86_att/p256/bignum_deamont_p256.S	106
x86_att/p256/bignum_deamont_p256_alt.S	122
x86_att/p256/bignum_demont_p256.S	83
x86_att/p256/bignum_demont_p256_alt.S	101
x86_att/p256/bignum_double_p256.S	75
x86_att/p256/bignum_half_p256.S	67
x86_att/p256/bignum_littleendian_4.S	56
x86_att/p256/bignum_mod_n256.S	154
x86_att/p256/bignum_mod_n256_4.S	74
x86_att/p256/bignum_mod_n256_alt.S	158
x86_att/p256/bignum_mod_p256.S	147
x86_att/p256/bignum_mod_p256_4.S	66
x86_att/p256/bignum_mod_p256_alt.S	149
x86_att/p256/bignum_montmul_p256.S	151
x86_att/p256/bignum_montmul_p256_alt.S	167
x86_att/p256/bignum_montsqr_p256.S	152
x86_att/p256/bignum_montsqr_p256_alt.S	173
x86_att/p256/bignum_mux_4.S	56
x86_att/p256/bignum_neg_p256.S	70
x86_att/p256/bignum_nonzero_4.S	42
x86_att/p256/bignum_optneg_p256.S	78
x86_att/p256/bignum_sub_p256.S	66
x86_att/p256/bignum_tomont_p256.S	150
x86_att/p256/bignum_tomont_p256_alt.S	157
x86_att/p256/bignum_triple_p256.S	103
x86_att/p256/bignum_triple_p256_alt.S	105
x86_att/p384/bignum_add_p384.S	99
x86_att/p384/bignum_bigendian_6.S	76
x86_att/p384/bignum_cmul_p384.S	122
x86_att/p384/bignum_cmul_p384_alt.S	139
x86_att/p384/bignum_deamont_p384.S	136
x86_att/p384/bignum_deamont_p384_alt.S	136
x86_att/p384/bignum_demont_p384.S	102
x86_att/p384/bignum_demont_p384_alt.S	102
x86_att/p384/bignum_double_p384.S	98
x86_att/p384/bignum_half_p384.S	79
x86_att/p384/bignum_littleendian_6.S	60
x86_att/p384/bignum_mod_n384.S	178
x86_att/p384/bignum_mod_n384_6.S	88
x86_att/p384/bignum_mod_n384_alt.S	182
x86_att/p384/bignum_mod_p384.S	176
x86_att/p384/bignum_mod_p384_6.S	86
x86_att/p384/bignum_mod_p384_alt.S	178
x86_att/p384/bignum_montmul_p384.S	229
x86_att/p384/bignum_montmul_p384_alt.S	244
x86_att/p384/bignum_montsqr_p384.S	239
x86_att/p384/bignum_montsqr_p384_alt.S	277
x86_att/p384/bignum_mux_6.S	64
x86_att/p384/bignum_neg_p384.S	73
x86_att/p384/bignum_nonzero_6.S	44
x86_att/p384/bignum_optneg_p384.S	92
x86_att/p384/bignum_sub_p384.S	85
x86_att/p384/bignum_tomont_p384.S	229
x86_att/p384/bignum_tomont_p384_alt.S	250
x86_att/p384/bignum_triple_p384.S	118
x86_att/p384/bignum_triple_p384_alt.S	123
x86_att/p521/bignum_add_p521.S	98
x86_att/p521/bignum_cmul_p521.S	135
x86_att/p521/bignum_deamont_p521.S	120
x86_att/p521/bignum_demont_p521.S	77
x86_att/p521/bignum_double_p521.S	68
x86_att/p521/bignum_half_p521.S	76
x86_att/p521/bignum_mod_n521_9.S	119
x86_att/p521/bignum_mod_p521_9.S	94
x86_att/p521/bignum_montmul_p521.S	375
x86_att/p521/bignum_montsqr_p521.S	275
x86_att/p521/bignum_mul_p521.S	354
x86_att/p521/bignum_neg_p521.S	83
x86_att/p521/bignum_optneg_p521.S	87
x86_att/p521/bignum_sqr_p521.S	253
x86_att/p521/bignum_sub_p521.S	91
x86_att/p521/bignum_tomont_p521.S	110
x86_att/p521/bignum_triple_p521.S	127
x86_att/secp256k1/bignum_add_p256k1.S	75
x86_att/secp256k1/bignum_cmul_p256k1.S	79
x86_att/secp256k1/bignum_cmul_p256k1_alt.S	88
x86_att/secp256k1/bignum_deamont_p256k1.S	113
x86_att/secp256k1/bignum_demont_p256k1.S	86
x86_att/secp256k1/bignum_double_p256k1.S	73
x86_att/secp256k1/bignum_half_p256k1.S	66
x86_att/secp256k1/bignum_mod_n256k1_4.S	74
x86_att/secp256k1/bignum_mod_p256k1_4.S	63
x86_att/secp256k1/bignum_montmul_p256k1.S	177
x86_att/secp256k1/bignum_montmul_p256k1_alt.S	174
x86_att/secp256k1/bignum_montsqr_p256k1.S	166
x86_att/secp256k1/bignum_montsqr_p256k1_alt.S	162
x86_att/secp256k1/bignum_mul_p256k1.S	138
x86_att/secp256k1/bignum_mul_p256k1_alt.S	156
x86_att/secp256k1/bignum_neg_p256k1.S	64
x86_att/secp256k1/bignum_optneg_p256k1.S	71
x86_att/secp256k1/bignum_sqr_p256k1.S	136
x86_att/secp256k1/bignum_sqr_p256k1_alt.S	145
x86_att/secp256k1/bignum_sub_p256k1.S	65
x86_att/secp256k1/bignum_tomont_p256k1.S	79
x86_att/secp256k1/bignum_tomont_p256k1_alt.S	88
x86_att/secp256k1/bignum_triple_p256k1.S	92
x86_att/secp256k1/bignum_triple_p256k1_alt.S	93