Path	Lines of Code
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