https://github.com/project-everest/hacl-star
History
Tip revision: 979490eae06f54ec3a4768cdefdef741b6aa97b4 authored by Ann Weine on 23 September 2021, 10:43:48 UTC
Radix/Ml separation
Tip revision: 979490e
File Mode Size
AUTHORS.md -rw-r--r-- 134 bytes
Hacl.Bignum.Addition.fst -rw-r--r-- 9.8 KB
Hacl.Bignum.AlmostMontExponentiation.fst -rw-r--r-- 9.9 KB
Hacl.Bignum.AlmostMontgomery.fst -rw-r--r-- 3.2 KB
Hacl.Bignum.AlmostMontgomery.fsti -rw-r--r-- 2.9 KB
Hacl.Bignum.Base.fst -rw-r--r-- 3.7 KB
Hacl.Bignum.Comparison.fst -rw-r--r-- 3.5 KB
Hacl.Bignum.Convert.fst -rw-r--r-- 7.1 KB
Hacl.Bignum.Definitions.fst -rw-r--r-- 914 bytes
Hacl.Bignum.Exponentiation.fst -rw-r--r-- 8.5 KB
Hacl.Bignum.Exponentiation.fsti -rw-r--r-- 6.3 KB
Hacl.Bignum.Karatsuba.fst -rw-r--r-- 12.8 KB
Hacl.Bignum.Lib.fst -rw-r--r-- 4.9 KB
Hacl.Bignum.ModInv.fst -rw-r--r-- 3.9 KB
Hacl.Bignum.ModInvLimb.fst -rw-r--r-- 2.3 KB
Hacl.Bignum.ModInvLimb.fsti -rw-r--r-- 532 bytes
Hacl.Bignum.ModReduction.fst -rw-r--r-- 2.5 KB
Hacl.Bignum.MontArithmetic.fst -rw-r--r-- 4.8 KB
Hacl.Bignum.MontArithmetic.fsti -rw-r--r-- 13.1 KB
Hacl.Bignum.MontExponentiation.fst -rw-r--r-- 8.5 KB
Hacl.Bignum.Montgomery.fst -rw-r--r-- 8.4 KB
Hacl.Bignum.Montgomery.fsti -rw-r--r-- 6.5 KB
Hacl.Bignum.Multiplication.fst -rw-r--r-- 6.6 KB
Hacl.Bignum.SafeAPI.fst -rw-r--r-- 10.4 KB
Hacl.Bignum.fst -rw-r--r-- 4.4 KB
Hacl.Bignum.fsti -rw-r--r-- 15.0 KB
Hacl.Bignum256.fst -rw-r--r-- 4.5 KB
Hacl.Bignum256.fsti -rw-r--r-- 10.0 KB
Hacl.Bignum256_32.fst -rw-r--r-- 4.5 KB
Hacl.Bignum256_32.fsti -rw-r--r-- 10.0 KB
Hacl.Bignum32.fst -rw-r--r-- 2.4 KB
Hacl.Bignum32.fsti -rw-r--r-- 9.6 KB
Hacl.Bignum4096.fst -rw-r--r-- 4.6 KB
Hacl.Bignum4096.fsti -rw-r--r-- 10.2 KB
Hacl.Bignum4096_32.fst -rw-r--r-- 4.6 KB
Hacl.Bignum4096_32.fsti -rw-r--r-- 10.2 KB
Hacl.Bignum64.fst -rw-r--r-- 2.4 KB
Hacl.Bignum64.fsti -rw-r--r-- 9.6 KB
Hacl.GenericField32.fst -rw-r--r-- 1.5 KB
Hacl.GenericField32.fsti -rw-r--r-- 6.4 KB
Hacl.GenericField64.fst -rw-r--r-- 1.5 KB
Hacl.GenericField64.fsti -rw-r--r-- 6.4 KB
Hacl.Impl.Exponentiation.fst -rw-r--r-- 35.9 KB
Hacl.Impl.Exponentiation.fsti -rw-r--r-- 6.9 KB
Hacl.Impl.Lib.fst -rw-r--r-- 7.9 KB
Hacl.Impl.MultiExponentiation.fst -rw-r--r-- 14.0 KB
Hacl.Impl.MultiExponentiation.fsti -rw-r--r-- 2.2 KB
Hacl.Spec.AlmostMontgomery.Lemmas.fst -rw-r--r-- 3.8 KB
Hacl.Spec.Bignum.Addition.fst -rw-r--r-- 25.1 KB
Hacl.Spec.Bignum.AlmostMontExponentiation.fst -rw-r--r-- 5.3 KB
Hacl.Spec.Bignum.AlmostMontgomery.fst -rw-r--r-- 2.4 KB
Hacl.Spec.Bignum.AlmostMontgomery.fsti -rw-r--r-- 1.8 KB
Hacl.Spec.Bignum.Base.fst -rw-r--r-- 7.4 KB
Hacl.Spec.Bignum.Comparison.fst -rw-r--r-- 7.0 KB
Hacl.Spec.Bignum.Convert.fst -rw-r--r-- 16.6 KB
Hacl.Spec.Bignum.Definitions.fst -rw-r--r-- 12.8 KB
Hacl.Spec.Bignum.Exponentiation.fst -rw-r--r-- 4.7 KB
Hacl.Spec.Bignum.Exponentiation.fsti -rw-r--r-- 3.1 KB
Hacl.Spec.Bignum.Karatsuba.fst -rw-r--r-- 20.4 KB
Hacl.Spec.Bignum.Lib.fst -rw-r--r-- 18.9 KB
Hacl.Spec.Bignum.ModInv.fst -rw-r--r-- 3.8 KB
Hacl.Spec.Bignum.ModInvLimb.fst -rw-r--r-- 11.1 KB
Hacl.Spec.Bignum.ModInvLimb.fsti -rw-r--r-- 650 bytes
Hacl.Spec.Bignum.ModReduction.fst -rw-r--r-- 2.6 KB
Hacl.Spec.Bignum.MontArithmetic.fst -rw-r--r-- 4.5 KB
Hacl.Spec.Bignum.MontArithmetic.fsti -rw-r--r-- 3.9 KB
Hacl.Spec.Bignum.MontExponentiation.fst -rw-r--r-- 4.3 KB
Hacl.Spec.Bignum.Montgomery.fst -rw-r--r-- 18.2 KB
Hacl.Spec.Bignum.Montgomery.fsti -rw-r--r-- 4.9 KB
Hacl.Spec.Bignum.Multiplication.fst -rw-r--r-- 17.1 KB
Hacl.Spec.Bignum.Squaring.fst -rw-r--r-- 15.3 KB
Hacl.Spec.Bignum.fst -rw-r--r-- 7.9 KB
Hacl.Spec.Bignum.fsti -rw-r--r-- 10.8 KB
Hacl.Spec.Exponentiation.Lemmas.fst -rw-r--r-- 12.7 KB
Hacl.Spec.Karatsuba.Lemmas.fst -rw-r--r-- 4.4 KB
Hacl.Spec.Lib.fst -rw-r--r-- 9.8 KB
Hacl.Spec.Montgomery.Lemmas.fst -rw-r--r-- 29.0 KB
Hacl.Spec.PrecompTable.fst -rw-r--r-- 3.9 KB
Makefile -rw-r--r-- 1.1 KB
README.md -rw-r--r-- 4.7 KB

README.md

back to top