https://github.com/project-everest/hacl-star
Revision f4a8271e221b6cf83df5944f736d6f1654bd117f authored by Aymeric Fromherz on 17 January 2020, 20:51:08 UTC, committed by Aymeric Fromherz on 17 January 2020, 20:51:08 UTC
2 parent s d16d18e + 95467d2
History
Tip revision: f4a8271e221b6cf83df5944f736d6f1654bd117f authored by Aymeric Fromherz on 17 January 2020, 20:51:08 UTC
Merge branch '_afromher_nicer_asm' into afromher_nicer_asm
Tip revision: f4a8271
File Mode Size
CanonCommMonoid.fst.hints -rw-r--r-- 24.3 KB
CanonCommSemiring.fst.hints -rw-r--r-- 23.4 KB
CanonCommSwaps.fst.hints -rw-r--r-- 19.1 KB
Cipher16.fst.hints -rw-r--r-- 375 bytes
Cipher16.fsti.hints -rw-r--r-- 1.4 KB
Client.fst.hints -rw-r--r-- 1.6 KB
EverCrypt.AEAD.fst.hints -rw-r--r-- 130.1 KB
EverCrypt.AEAD.fsti.hints -rw-r--r-- 6.0 KB
EverCrypt.AutoConfig2.fst.hints -rw-r--r-- 95.5 KB
EverCrypt.AutoConfig2.fsti.hints -rw-r--r-- 27 bytes
EverCrypt.BCrypt.fsti.hints -rw-r--r-- 47 bytes
EverCrypt.Bytes.fsti.hints -rw-r--r-- 1.2 KB
EverCrypt.CTR.Keys.fst.hints -rw-r--r-- 24.1 KB
EverCrypt.CTR.Keys.fsti.hints -rw-r--r-- 31 bytes
EverCrypt.CTR.fst.hints -rw-r--r-- 106.9 KB
EverCrypt.CTR.fsti.hints -rw-r--r-- 5.6 KB
EverCrypt.Chacha20Poly1305.fst.hints -rw-r--r-- 17.9 KB
EverCrypt.Chacha20Poly1305.fsti.hints -rw-r--r-- 8.7 KB
EverCrypt.Cipher.fst.hints -rw-r--r-- 3.5 KB
EverCrypt.Cipher.fsti.hints -rw-r--r-- 3.2 KB
EverCrypt.Ciphers.fst.hints -rw-r--r-- 851 bytes
EverCrypt.Ciphers.fsti.hints -rw-r--r-- 710 bytes
EverCrypt.Curve25519.fst.hints -rw-r--r-- 16.1 KB
EverCrypt.Curve25519.fsti.hints -rw-r--r-- 8.8 KB
EverCrypt.DRBG.fst.hints -rw-r--r-- 124.6 KB
EverCrypt.DRBG.fsti.hints -rw-r--r-- 15.2 KB
EverCrypt.Ed25519.fst.hints -rw-r--r-- 777 bytes
EverCrypt.Ed25519.fsti.hints -rw-r--r-- 41 bytes
EverCrypt.Error.fsti.hints -rw-r--r-- 184 bytes
EverCrypt.HKDF.fst.hints -rw-r--r-- 7.5 KB
EverCrypt.HKDF.fsti.hints -rw-r--r-- 4.9 KB
EverCrypt.HMAC.fst.hints -rw-r--r-- 5.6 KB
EverCrypt.HMAC.fsti.hints -rw-r--r-- 1.9 KB
EverCrypt.Hacl.fsti.hints -rw-r--r-- 28 bytes
EverCrypt.Hash.Incremental.fst.hints -rw-r--r-- 119.3 KB
EverCrypt.Hash.Incremental.fsti.hints -rw-r--r-- 3.5 KB
EverCrypt.Hash.fst.hints -rw-r--r-- 141.3 KB
EverCrypt.Hash.fsti.hints -rw-r--r-- 9.3 KB
EverCrypt.Helpers.fsti.hints -rw-r--r-- 590 bytes
EverCrypt.OpenSSL.fsti.hints -rw-r--r-- 31 bytes
EverCrypt.Poly1305.fst.hints -rw-r--r-- 22.1 KB
EverCrypt.Poly1305.fsti.hints -rw-r--r-- 532 bytes
EverCrypt.Specs.fsti.hints -rw-r--r-- 33 bytes
EverCrypt.StaticConfig.fst.hints -rw-r--r-- 36 bytes
EverCrypt.StaticConfig.fsti.hints -rw-r--r-- 31 bytes
EverCrypt.TargetConfig.fst.hints -rw-r--r-- 31 bytes
EverCrypt.TargetConfig.fsti.hints -rw-r--r-- 26 bytes
EverCrypt.Vale.fsti.hints -rw-r--r-- 31 bytes
EverCrypt.Wasm.fsti.hints -rw-r--r-- 61 bytes
EverCrypt.fst.hints -rw-r--r-- 16.2 KB
EverCrypt.fsti.hints -rw-r--r-- 1.9 KB
Example.fst.hints -rw-r--r-- 105.0 KB
Fast_stdcalls.fst.hints -rw-r--r-- 332.5 KB
Fast_stdcalls.fsti.hints -rw-r--r-- 5.3 KB
Frodo.Params.fst.hints -rw-r--r-- 13.2 KB
Hacl.AES128.fsti.hints -rw-r--r-- 7.0 KB
Hacl.Bignum25519.fst.hints -rw-r--r-- 229.8 KB
Hacl.Bignum25519.fsti.hints -rw-r--r-- 15.6 KB
Hacl.Chacha20.Vec128.fst.hints -rw-r--r-- 6.5 KB
Hacl.Chacha20.Vec256.fst.hints -rw-r--r-- 6.5 KB
Hacl.Chacha20.Vec32.fst.hints -rw-r--r-- 7.7 KB
Hacl.Chacha20.fst.hints -rw-r--r-- 7.0 KB
Hacl.Chacha20Poly1305_128.fst.hints -rw-r--r-- 46 bytes
Hacl.Chacha20Poly1305_256.fst.hints -rw-r--r-- 41 bytes
Hacl.Chacha20Poly1305_32.fst.hints -rw-r--r-- 42 bytes
Hacl.Curve25519.Finv.Field51.fst.hints -rw-r--r-- 2.1 KB
Hacl.Curve25519.Finv.Field51.fsti.hints -rw-r--r-- 898 bytes
Hacl.Curve25519_51.fst.hints -rw-r--r-- 5.8 KB
Hacl.Curve25519_51.fsti.hints -rw-r--r-- 36 bytes
Hacl.Curve25519_64.fst.hints -rw-r--r-- 4.2 KB
Hacl.Curve25519_64.fsti.hints -rw-r--r-- 26 bytes
Hacl.Curve25519_64_Local.fst.hints -rw-r--r-- 4.2 KB
Hacl.Curve25519_64_Local.fsti.hints -rw-r--r-- 36 bytes
Hacl.Curve25519_64_Slow.fst.hints -rw-r--r-- 4.2 KB
Hacl.Curve25519_64_Slow.fsti.hints -rw-r--r-- 36 bytes
Hacl.Ed25519.fst.hints -rw-r--r-- 15.4 KB
Hacl.Ed25519.fsti.hints -rw-r--r-- 15.0 KB
Hacl.Frodo.KEM.fst.hints -rw-r--r-- 5.6 KB
Hacl.Frodo.Random.fst.hints -rw-r--r-- 10.4 KB
Hacl.Frodo.Random.fsti.hints -rw-r--r-- 3.2 KB
Hacl.HKDF.fst.hints -rw-r--r-- 24.1 KB
Hacl.HKDF.fsti.hints -rw-r--r-- 4.0 KB
Hacl.HMAC.fst.hints -rw-r--r-- 59.8 KB
Hacl.HMAC.fsti.hints -rw-r--r-- 2.2 KB
Hacl.HMAC_DRBG.fst.hints -rw-r--r-- 109.3 KB
Hacl.HMAC_DRBG.fsti.hints -rw-r--r-- 14.3 KB
Hacl.Hash.Agile.fst.hints -rw-r--r-- 6.9 KB
Hacl.Hash.Core.MD5.fst.hints -rw-r--r-- 48.9 KB
Hacl.Hash.Core.MD5.fsti.hints -rw-r--r-- 37 bytes
Hacl.Hash.Core.SHA1.fst.hints -rw-r--r-- 66.1 KB
Hacl.Hash.Core.SHA1.fsti.hints -rw-r--r-- 36 bytes
Hacl.Hash.Core.SHA2.Constants.fst.hints -rw-r--r-- 2.4 KB
Hacl.Hash.Core.SHA2.fst.hints -rw-r--r-- 71.2 KB
Hacl.Hash.Core.SHA2.fsti.hints -rw-r--r-- 37 bytes
Hacl.Hash.Definitions.fst.hints -rw-r--r-- 13.5 KB
Hacl.Hash.Lemmas.fst.hints -rw-r--r-- 8.4 KB
Hacl.Hash.MD.fst.hints -rw-r--r-- 42.3 KB
Hacl.Hash.MD.fsti.hints -rw-r--r-- 26 bytes
Hacl.Hash.MD5.fst.hints -rw-r--r-- 31 bytes
Hacl.Hash.MD5.fsti.hints -rw-r--r-- 33 bytes
Hacl.Hash.PadFinish.fst.hints -rw-r--r-- 45.2 KB
Hacl.Hash.PadFinish.fsti.hints -rw-r--r-- 536 bytes
Hacl.Hash.SHA1.fst.hints -rw-r--r-- 32 bytes
Hacl.Hash.SHA1.fsti.hints -rw-r--r-- 42 bytes
Hacl.Hash.SHA2.fst.hints -rw-r--r-- 6.6 KB
Hacl.Hash.SHA2.fsti.hints -rw-r--r-- 2.0 KB
Hacl.Impl.BignumQ.Mul.fst.hints -rw-r--r-- 31.7 KB
Hacl.Impl.BignumQ.Mul.fsti.hints -rw-r--r-- 20.1 KB
Hacl.Impl.Box.fst.hints -rw-r--r-- 91.9 KB
Hacl.Impl.Chacha20.Core32.fst.hints -rw-r--r-- 75.1 KB
Hacl.Impl.Chacha20.Core32xN.fst.hints -rw-r--r-- 86.9 KB
Hacl.Impl.Chacha20.Vec.fst.hints -rw-r--r-- 128.6 KB
Hacl.Impl.Chacha20.fst.hints -rw-r--r-- 90.9 KB
Hacl.Impl.Chacha20Poly1305.Poly.fst.hints -rw-r--r-- 84.8 KB
Hacl.Impl.Chacha20Poly1305.PolyCore.fst.hints -rw-r--r-- 12.4 KB
Hacl.Impl.Chacha20Poly1305.PolyCore.fsti.hints -rw-r--r-- 11.2 KB
Hacl.Impl.Chacha20Poly1305.PolyLemmas.fst.hints -rw-r--r-- 1.4 KB
Hacl.Impl.Chacha20Poly1305.PolyLemmas.fsti.hints -rw-r--r-- 1.4 KB
Hacl.Impl.Chacha20Poly1305.fst.hints -rw-r--r-- 62.2 KB
Hacl.Impl.Chacha20Poly1305.fsti.hints -rw-r--r-- 8.0 KB
Hacl.Impl.Curve25519.AddAndDouble.fst.hints -rw-r--r-- 81.8 KB
Hacl.Impl.Curve25519.Field26.fst.hints -rw-r--r-- 65.6 KB
Hacl.Impl.Curve25519.Field51.fst.hints -rw-r--r-- 97.2 KB
Hacl.Impl.Curve25519.Field64.Core.fst.hints -rw-r--r-- 58.2 KB
Hacl.Impl.Curve25519.Field64.Core.fsti.hints -rw-r--r-- 13.0 KB
Hacl.Impl.Curve25519.Field64.Hacl.fst.hints -rw-r--r-- 52.5 KB
Hacl.Impl.Curve25519.Field64.Hacl.fsti.hints -rw-r--r-- 31 bytes
Hacl.Impl.Curve25519.Field64.Local.fsti.hints -rw-r--r-- 42 bytes
Hacl.Impl.Curve25519.Field64.Vale.fst.hints -rw-r--r-- 56.5 KB
Hacl.Impl.Curve25519.Field64.Vale.fsti.hints -rw-r--r-- 46 bytes
Hacl.Impl.Curve25519.Field64.fst.hints -rw-r--r-- 55.1 KB
Hacl.Impl.Curve25519.Fields.Core.fsti.hints -rw-r--r-- 46.4 KB
Hacl.Impl.Curve25519.Fields.fst.hints -rw-r--r-- 21.9 KB
Hacl.Impl.Curve25519.Finv.fst.hints -rw-r--r-- 42.8 KB
Hacl.Impl.Curve25519.Generic.fst.hints -rw-r--r-- 213.3 KB
Hacl.Impl.Curve25519.Generic.fsti.hints -rw-r--r-- 8.8 KB
Hacl.Impl.Curve25519.Lemmas.fst.hints -rw-r--r-- 5.2 KB
Hacl.Impl.Curve25519.Lemmas.fsti.hints -rw-r--r-- 2.5 KB
Hacl.Impl.Ed25519.Field51.fst.hints -rw-r--r-- 6.9 KB
Hacl.Impl.Ed25519.Field56.fst.hints -rw-r--r-- 13.6 KB
Hacl.Impl.Ed25519.Ladder.fst.hints -rw-r--r-- 62.7 KB
Hacl.Impl.Ed25519.PointAdd.fst.hints -rw-r--r-- 36.3 KB
Hacl.Impl.Ed25519.PointCompress.fst.hints -rw-r--r-- 38.6 KB
Hacl.Impl.Ed25519.PointDecompress.fst.hints -rw-r--r-- 35.0 KB
Hacl.Impl.Ed25519.PointDouble.fst.hints -rw-r--r-- 35.5 KB
Hacl.Impl.Ed25519.PointEqual.fst.hints -rw-r--r-- 38.1 KB
Hacl.Impl.Ed25519.Pow2_252m2.fst.hints -rw-r--r-- 27.4 KB
Hacl.Impl.Ed25519.RecoverX.fst.hints -rw-r--r-- 93.6 KB
Hacl.Impl.Ed25519.SecretExpand.fst.hints -rw-r--r-- 9.4 KB
Hacl.Impl.Ed25519.SecretExpand.fsti.hints -rw-r--r-- 3.2 KB
Hacl.Impl.Ed25519.SecretToPublic.fst.hints -rw-r--r-- 11.9 KB
Hacl.Impl.Ed25519.Sign.Expanded.fst.hints -rw-r--r-- 40.4 KB
Hacl.Impl.Ed25519.Sign.Steps.fst.hints -rw-r--r-- 68.4 KB
Hacl.Impl.Ed25519.Sign.fst.hints -rw-r--r-- 20.7 KB
Hacl.Impl.Ed25519.SwapConditional.fst.hints -rw-r--r-- 25.4 KB
Hacl.Impl.Ed25519.Verify.fst.hints -rw-r--r-- 67.7 KB
Hacl.Impl.Frodo.Encode.fst.hints -rw-r--r-- 96.3 KB
Hacl.Impl.Frodo.Gen.fst.hints -rw-r--r-- 87.7 KB
Hacl.Impl.Frodo.KEM.Decaps.fst.hints -rw-r--r-- 142.7 KB
Hacl.Impl.Frodo.KEM.Encaps.fst.hints -rw-r--r-- 181.6 KB
Hacl.Impl.Frodo.KEM.KeyGen.fst.hints -rw-r--r-- 76.2 KB
Hacl.Impl.Frodo.KEM.fst.hints -rw-r--r-- 16.6 KB
Hacl.Impl.Frodo.Pack.fst.hints -rw-r--r-- 70.4 KB
Hacl.Impl.Frodo.Params.fst.hints -rw-r--r-- 27 bytes
Hacl.Impl.Frodo.Sample.fst.hints -rw-r--r-- 53.7 KB
Hacl.Impl.HSalsa20.fst.hints -rw-r--r-- 25.6 KB
Hacl.Impl.Load56.fst.hints -rw-r--r-- 45.0 KB
Hacl.Impl.Matrix.fst.hints -rw-r--r-- 138.0 KB
Hacl.Impl.Poly1305.Field32xN.fst.hints -rw-r--r-- 222.0 KB
Hacl.Impl.Poly1305.Field32xN_128.fst.hints -rw-r--r-- 23.1 KB
Hacl.Impl.Poly1305.Field32xN_256.fst.hints -rw-r--r-- 23.2 KB
Hacl.Impl.Poly1305.Field32xN_32.fst.hints -rw-r--r-- 22.2 KB
Hacl.Impl.Poly1305.Field64.fst.hints -rw-r--r-- 98.4 KB
Hacl.Impl.Poly1305.Fields.fst.hints -rw-r--r-- 91.8 KB
Hacl.Impl.Poly1305.Lemmas.fst.hints -rw-r--r-- 45.5 KB
Hacl.Impl.Poly1305.Lemmas.fsti.hints -rw-r--r-- 15.9 KB
Hacl.Impl.Poly1305.fst.hints -rw-r--r-- 268.6 KB
Hacl.Impl.Poly1305.fsti.hints -rw-r--r-- 14.4 KB
Hacl.Impl.SHA3.fst.hints -rw-r--r-- 219.6 KB
Hacl.Impl.SHA512.ModQ.fst.hints -rw-r--r-- 61.6 KB
Hacl.Impl.Salsa20.Core32.fst.hints -rw-r--r-- 69.9 KB
Hacl.Impl.Salsa20.fst.hints -rw-r--r-- 100.7 KB
Hacl.Impl.SecretBox.fst.hints -rw-r--r-- 99.3 KB
Hacl.Impl.Store56.fst.hints -rw-r--r-- 26.5 KB
Hacl.Keccak.fst.hints -rw-r--r-- 12.2 KB
Hacl.Keccak.fsti.hints -rw-r--r-- 3.5 KB
Hacl.Loops.Lemmas.fst.hints -rw-r--r-- 54.8 KB
Hacl.Loops.Lemmas.fsti.hints -rw-r--r-- 9.7 KB
Hacl.Meta.Chacha20.Vec.fst.hints -rw-r--r-- 2.6 KB
Hacl.Meta.Chacha20Poly1305.fst.hints -rw-r--r-- 41 bytes
Hacl.Meta.Curve25519.fst.hints -rw-r--r-- 26 bytes
Hacl.Meta.Curve25519.fsti.hints -rw-r--r-- 31 bytes
Hacl.Meta.Poly1305.fst.hints -rw-r--r-- 31 bytes
Hacl.Meta.Poly1305.fsti.hints -rw-r--r-- 26 bytes
Hacl.NaCl.fst.hints -rw-r--r-- 80.6 KB
Hacl.Poly1305.Field32xN.Lemmas0.fst.hints -rw-r--r-- 124.3 KB
Hacl.Poly1305.Field32xN.Lemmas1.fst.hints -rw-r--r-- 226.8 KB
Hacl.Poly1305.Field32xN.Lemmas2.fst.hints -rw-r--r-- 153.1 KB
Hacl.Poly1305_128.fst.hints -rw-r--r-- 1.1 KB
Hacl.Poly1305_128.fsti.hints -rw-r--r-- 1.1 KB
Hacl.Poly1305_256.fst.hints -rw-r--r-- 1.1 KB
Hacl.Poly1305_256.fsti.hints -rw-r--r-- 1.1 KB
Hacl.Poly1305_32.fst.hints -rw-r--r-- 1.1 KB
Hacl.Poly1305_32.fsti.hints -rw-r--r-- 1.1 KB
Hacl.SHA3.fst.hints -rw-r--r-- 45.5 KB
Hacl.Salsa20.fst.hints -rw-r--r-- 13.2 KB
Hacl.Spec.BignumQ.Definitions.fst.hints -rw-r--r-- 4.5 KB
Hacl.Spec.BignumQ.Lemmas.fst.hints -rw-r--r-- 92.5 KB
Hacl.Spec.BignumQ.Mul.fst.hints -rw-r--r-- 75.4 KB
Hacl.Spec.Chacha20.Equiv.fst.hints -rw-r--r-- 271.2 KB
Hacl.Spec.Chacha20.Lemmas.fst.hints -rw-r--r-- 51.7 KB
Hacl.Spec.Chacha20.Vec.fst.hints -rw-r--r-- 52.5 KB
Hacl.Spec.Curve25519.AddAndDouble.fst.hints -rw-r--r-- 3.5 KB
Hacl.Spec.Curve25519.Field51.Definition.fst.hints -rw-r--r-- 8.3 KB
Hacl.Spec.Curve25519.Field51.Lemmas.fst.hints -rw-r--r-- 119.4 KB
Hacl.Spec.Curve25519.Field51.fst.hints -rw-r--r-- 70.1 KB
Hacl.Spec.Curve25519.Field64.Core.fst.hints -rw-r--r-- 49.8 KB
Hacl.Spec.Curve25519.Field64.Definition.fst.hints -rw-r--r-- 3.1 KB
Hacl.Spec.Curve25519.Field64.Lemmas.fst.hints -rw-r--r-- 36.8 KB
Hacl.Spec.Curve25519.Field64.fst.hints -rw-r--r-- 22.7 KB
Hacl.Spec.Curve25519.Finv.fst.hints -rw-r--r-- 17.5 KB
Hacl.Spec.Ed25519.Field56.Definition.fst.hints -rw-r--r-- 3.9 KB
Hacl.Spec.Poly1305.Equiv.Lemmas.fst.hints -rw-r--r-- 73.5 KB
Hacl.Spec.Poly1305.Equiv.fst.hints -rw-r--r-- 75.0 KB
Hacl.Spec.Poly1305.Field32xN.Lemmas.fst.hints -rw-r--r-- 195.1 KB
Hacl.Spec.Poly1305.Field32xN.fst.hints -rw-r--r-- 68.8 KB
Hacl.Spec.Poly1305.Lemmas.fst.hints -rw-r--r-- 10.8 KB
Hacl.Spec.Poly1305.Vec.fst.hints -rw-r--r-- 32.6 KB
Hacl.Test.CSHAKE.fst.hints -rw-r--r-- 17.8 KB
Hacl.Test.Ed25519.fst.hints -rw-r--r-- 41.8 KB
Hacl.Test.HMAC_DRBG.fst.hints -rw-r--r-- 244.3 KB
Hacl.Test.SHA2.fst.hints -rwxr-xr-x 75.1 KB
Hacl.Test.SHA3.fst.hints -rw-r--r-- 134.0 KB
Interface.fsti.hints -rw-r--r-- 317 bytes
Interop_Printer.fst.hints -rw-r--r-- 52.6 KB
Lib.Buffer.fst.hints -rw-r--r-- 283.0 KB
Lib.Buffer.fsti.hints -rw-r--r-- 62.0 KB
Lib.ByteBuffer.fst.hints -rw-r--r-- 175.3 KB
Lib.ByteBuffer.fsti.hints -rw-r--r-- 28.3 KB
Lib.ByteSequence.fst.hints -rw-r--r-- 233.3 KB
Lib.ByteSequence.fsti.hints -rw-r--r-- 44.9 KB
Lib.CurveLemmas.fst.hints -rw-r--r-- 5.2 KB
Lib.IntTypes.Compatibility.fst.hints -rw-r--r-- 2.5 KB
Lib.IntTypes.fst.hints -rw-r--r-- 395.6 KB
Lib.IntTypes.fsti.hints -rw-r--r-- 40.5 KB
Lib.IntVector.Intrinsics.fsti.hints -rw-r--r-- 39 bytes
Lib.IntVector.fst.hints -rw-r--r-- 193 bytes
Lib.IntVector.fsti.hints -rw-r--r-- 107.7 KB
Lib.Lemmas.fst.hints -rw-r--r-- 34.1 KB
Lib.LoopCombinators.fst.hints -rw-r--r-- 43.5 KB
Lib.LoopCombinators.fsti.hints -rw-r--r-- 11.2 KB
Lib.Loops.fst.hints -rw-r--r-- 13.0 KB
Lib.Loops.fsti.hints -rw-r--r-- 1.2 KB
Lib.Memzero.fsti.hints -rw-r--r-- 5.6 KB
Lib.Meta.fst.hints -rw-r--r-- 5.5 KB
Lib.PrintBuffer.fsti.hints -rw-r--r-- 41 bytes
Lib.PrintSequence.fst.hints -rw-r--r-- 11.2 KB
Lib.PrintSequence.fsti.hints -rw-r--r-- 47 bytes
Lib.RandomBuffer.System.fsti.hints -rw-r--r-- 193 bytes
Lib.RandomBuffer.fsti.hints -rw-r--r-- 185 bytes
Lib.RandomSequence.fsti.hints -rw-r--r-- 36 bytes
Lib.RawBuffer.fst.hints -rw-r--r-- 7.8 KB
Lib.RawBuffer.fsti.hints -rw-r--r-- 1.5 KB
Lib.RawIntTypes.fst.hints -rw-r--r-- 10.2 KB
Lib.RawIntTypes.fsti.hints -rw-r--r-- 4.4 KB
Lib.Sequence.Lemmas.fst.hints -rw-r--r-- 48.3 KB
Lib.Sequence.Lemmas.fsti.hints -rw-r--r-- 9.5 KB
Lib.Sequence.fst.hints -rw-r--r-- 80.3 KB
Lib.Sequence.fsti.hints -rw-r--r-- 25.5 KB
Lib.Unlib.fst.hints -rw-r--r-- 501 bytes
Lib.Unlib.fsti.hints -rw-r--r-- 36 bytes
MerkleTree.New.High.Correct.Base.fst.hints -rw-r--r-- 193.6 KB
MerkleTree.New.High.Correct.Flushing.fst.hints -rw-r--r-- 32.8 KB
MerkleTree.New.High.Correct.Insertion.fst.hints -rw-r--r-- 38.5 KB
MerkleTree.New.High.Correct.Path.fst.hints -rw-r--r-- 96.2 KB
MerkleTree.New.High.Correct.Rhs.fst.hints -rw-r--r-- 94.0 KB
MerkleTree.New.High.Correct.fst.hints -rw-r--r-- 15.5 KB
MerkleTree.New.High.fst.hints -rw-r--r-- 114.6 KB
MerkleTree.New.Low.Serialization.fst.hints -rw-r--r-- 159.6 KB
MerkleTree.New.Low.fst.hints -rw-r--r-- 691.0 KB
MerkleTree.Spec.fst.hints -rw-r--r-- 125.8 KB
Meta.Attribute.fst.hints -rw-r--r-- 36 bytes
Meta.Interface.fst.hints -rw-r--r-- 7.7 KB
MetaAttribute.fst.hints -rw-r--r-- 38 bytes
MetaInterface.fst.hints -rw-r--r-- 4.6 KB
Spec.AEAD.fst.hints -rw-r--r-- 32.9 KB
Spec.AEAD.fsti.hints -rw-r--r-- 5.2 KB
Spec.AES.Test.fst.hints -rwxr-xr-x 36 bytes
Spec.AES.fst.hints -rw-r--r-- 96.2 KB
Spec.Agile.AEAD.fst.hints -rw-r--r-- 37.8 KB
Spec.Agile.AEAD.fsti.hints -rw-r--r-- 6.2 KB
Spec.Agile.CTR.fst.hints -rw-r--r-- 2.4 KB
Spec.Agile.Cipher.fst.hints -rw-r--r-- 16.2 KB
Spec.Agile.Cipher.fsti.hints -rw-r--r-- 9.2 KB
Spec.Agile.HKDF.fst.hints -rw-r--r-- 14.8 KB
Spec.Agile.HKDF.fsti.hints -rw-r--r-- 2.2 KB
Spec.Agile.HMAC.fst.hints -rw-r--r-- 16.8 KB
Spec.Agile.HMAC.fsti.hints -rw-r--r-- 1.2 KB
Spec.Agile.Hash.fst.hints -rw-r--r-- 12.9 KB
Spec.Agile.Hash.fsti.hints -rw-r--r-- 2.6 KB
Spec.Box.Test.fst.hints -rw-r--r-- 41 bytes
Spec.Box.fst.hints -rw-r--r-- 15.8 KB
Spec.Chacha20.Test.fst.hints -rw-r--r-- 31 bytes
Spec.Chacha20.fst.hints -rw-r--r-- 22.2 KB
Spec.Chacha20Poly1305.Test.fst.hints -rw-r--r-- 32 bytes
Spec.Chacha20Poly1305.fst.hints -rw-r--r-- 15.0 KB
Spec.Cipher.Expansion.fst.hints -rw-r--r-- 14.2 KB
Spec.Cipher.Expansion.fsti.hints -rw-r--r-- 490 bytes
Spec.Cipher16.fsti.hints -rw-r--r-- 2.1 KB
Spec.Curve25519.Lemmas.fst.hints -rw-r--r-- 748 bytes
Spec.Curve25519.Test.fst.hints -rw-r--r-- 36 bytes
Spec.Curve25519.fst.hints -rw-r--r-- 16.4 KB
Spec.Ed25519.Test.fst.hints -rwxr-xr-x 31 bytes
Spec.Ed25519.fst.hints -rw-r--r-- 32.1 KB
Spec.Frodo.Encode.fst.hints -rw-r--r-- 58.2 KB
Spec.Frodo.Gen.fst.hints -rw-r--r-- 38.2 KB
Spec.Frodo.KEM.Decaps.fst.hints -rw-r--r-- 47.4 KB
Spec.Frodo.KEM.Encaps.fst.hints -rw-r--r-- 50.9 KB
Spec.Frodo.KEM.KeyGen.fst.hints -rw-r--r-- 16.5 KB
Spec.Frodo.KEM.fst.hints -rw-r--r-- 1.8 KB
Spec.Frodo.Lemmas.fst.hints -rw-r--r-- 28.6 KB
Spec.Frodo.Lemmas.fsti.hints -rw-r--r-- 6.4 KB
Spec.Frodo.Pack.fst.hints -rw-r--r-- 18.4 KB
Spec.Frodo.Params.fst.hints -rw-r--r-- 11.0 KB
Spec.Frodo.Random.fst.hints -rw-r--r-- 834 bytes
Spec.Frodo.Sample.fst.hints -rw-r--r-- 36.9 KB
Spec.Frodo.Test.fst.hints -rw-r--r-- 5.4 KB
Spec.Frodo.Test.fsti.hints -rw-r--r-- 36 bytes
Spec.GaloisField.fst.hints -rw-r--r-- 32.2 KB
Spec.HKDF.Test.fst.hints -rwxr-xr-x 41 bytes
Spec.HKDF.fst.hints -rw-r--r-- 13.5 KB
Spec.HKDF.fsti.hints -rw-r--r-- 2.9 KB
Spec.HMAC.Test.fst.hints -rwxr-xr-x 36 bytes
Spec.HMAC.fst.hints -rw-r--r-- 14.9 KB
Spec.HMAC.fsti.hints -rw-r--r-- 924 bytes
Spec.HMAC_DRBG.Test.Vectors.fst.hints -rw-r--r-- 405 bytes
Spec.HMAC_DRBG.Test.fst.hints -rw-r--r-- 380 bytes
Spec.HMAC_DRBG.fst.hints -rw-r--r-- 28.3 KB
Spec.HMAC_DRBG.fsti.hints -rw-r--r-- 706 bytes
Spec.Hash.Definitions.fst.hints -rw-r--r-- 19.2 KB
Spec.Hash.Incremental.fst.hints -rw-r--r-- 3.7 KB
Spec.Hash.Lemmas.fst.hints -rw-r--r-- 43.7 KB
Spec.Hash.Lemmas.fsti.hints -rw-r--r-- 6.5 KB
Spec.Hash.Lemmas0.fst.hints -rw-r--r-- 3.2 KB
Spec.Hash.PadFinish.fst.hints -rw-r--r-- 5.2 KB
Spec.Hash.Test.fst.hints -rw-r--r-- 2.3 KB
Spec.Hash.fst.hints -rw-r--r-- 8.3 KB
Spec.Loops.fst.hints -rw-r--r-- 15.2 KB
Spec.MD5.fst.hints -rw-r--r-- 17.3 KB
Spec.MD5.fsti.hints -rw-r--r-- 31 bytes
Spec.Matrix.fst.hints -rw-r--r-- 68.6 KB
Spec.Poly1305.Test.fst.hints -rwxr-xr-x 31 bytes
Spec.Poly1305.fst.hints -rw-r--r-- 8.6 KB
Spec.SHA1.fst.hints -rw-r--r-- 26.7 KB
Spec.SHA1.fsti.hints -rw-r--r-- 32 bytes
Spec.SHA2.Constants.fst.hints -rw-r--r-- 6.0 KB
Spec.SHA2.Lemmas.fst.hints -rw-r--r-- 27.7 KB
Spec.SHA2.Lemmas.fsti.hints -rw-r--r-- 2.4 KB
Spec.SHA2.Test.fst.hints -rwxr-xr-x 32 bytes
Spec.SHA2.fst.hints -rw-r--r-- 36.0 KB
Spec.SHA2.fsti.hints -rw-r--r-- 44 bytes
Spec.SHA3.Constants.fst.hints -rw-r--r-- 5.8 KB
Spec.SHA3.Test.fst.hints -rw-r--r-- 26 bytes
Spec.SHA3.fst.hints -rw-r--r-- 44.5 KB
Spec.Salsa20.Test.fst.hints -rw-r--r-- 7.7 KB
Spec.Salsa20.fst.hints -rw-r--r-- 30.4 KB
Spec.SecretBox.Test.fst.hints -rw-r--r-- 31 bytes
Spec.SecretBox.fst.hints -rw-r--r-- 16.3 KB
Test.Bytes.fst.hints -rw-r--r-- 6.9 KB
Test.Hash.fst.hints -rw-r--r-- 10.9 KB
Test.Lowstarize.fst.hints -rw-r--r-- 11.3 KB
Test.NoHeap.fst.hints -rw-r--r-- 77.0 KB
Test.NoHeap.fsti.hints -rw-r--r-- 874 bytes
Test.Vectors.Aes128.fst.hints -rw-r--r-- 27.8 KB
Test.Vectors.Aes128Gcm.fst.hints -rw-r--r-- 48.9 KB
Test.Vectors.Chacha20Poly1305.fst.hints -rw-r--r-- 119.7 KB
Test.Vectors.Curve25519.fst.hints -rw-r--r-- 36.7 KB
Test.Vectors.Poly1305.fst.hints -rw-r--r-- 169.1 KB
Test.Vectors.fst.hints -rw-r--r-- 470.5 KB
Test.fst.hints -rw-r--r-- 88.0 KB
Test.fsti.hints -rw-r--r-- 31 bytes
Vale.AES.AES256_helpers.fst.hints -rw-r--r-- 21.4 KB
Vale.AES.AES256_helpers.fsti.hints -rw-r--r-- 3.1 KB
Vale.AES.AES_helpers.fst.hints -rw-r--r-- 30.0 KB
Vale.AES.AES_helpers.fsti.hints -rw-r--r-- 4.8 KB
Vale.AES.AES_s.fst.hints -rw-r--r-- 31.6 KB
Vale.AES.GCM.fst.hints -rw-r--r-- 64.6 KB
Vale.AES.GCM.fsti.hints -rw-r--r-- 15.7 KB
Vale.AES.GCM_helpers.fst.hints -rw-r--r-- 60.5 KB
Vale.AES.GCM_helpers.fsti.hints -rw-r--r-- 5.6 KB
Vale.AES.GCM_s.fst.hints -rw-r--r-- 14.4 KB
Vale.AES.GCTR.fst.hints -rw-r--r-- 76.5 KB
Vale.AES.GCTR.fsti.hints -rw-r--r-- 11.9 KB
Vale.AES.GCTR_s.fst.hints -rw-r--r-- 10.7 KB
Vale.AES.GF128.fst.hints -rw-r--r-- 43.7 KB
Vale.AES.GF128.fsti.hints -rw-r--r-- 2.2 KB
Vale.AES.GF128_s.fst.hints -rw-r--r-- 41 bytes
Vale.AES.GF128_s.fsti.hints -rw-r--r-- 31 bytes
Vale.AES.GHash.fst.hints -rw-r--r-- 56.3 KB
Vale.AES.GHash.fsti.hints -rw-r--r-- 10.2 KB
Vale.AES.GHash_s.fst.hints -rw-r--r-- 3.9 KB
Vale.AES.Gcm_simplify.fst.hints -rw-r--r-- 70.6 KB
Vale.AES.Gcm_simplify.fsti.hints -rw-r--r-- 15.1 KB
Vale.AES.OptPublic.fst.hints -rw-r--r-- 5.3 KB
Vale.AES.OptPublic.fsti.hints -rw-r--r-- 32 bytes
Vale.AES.X64.AES.fst.hints -rw-r--r-- 29.0 KB
Vale.AES.X64.AES.fsti.hints -rw-r--r-- 9.2 KB
Vale.AES.X64.AES128.fst.hints -rw-r--r-- 73.9 KB
Vale.AES.X64.AES128.fsti.hints -rw-r--r-- 6.3 KB
Vale.AES.X64.AES256.fst.hints -rw-r--r-- 88.3 KB
Vale.AES.X64.AES256.fsti.hints -rw-r--r-- 3.7 KB
Vale.AES.X64.AESCTR.fst.hints -rw-r--r-- 127.7 KB
Vale.AES.X64.AESCTR.fsti.hints -rw-r--r-- 4.4 KB
Vale.AES.X64.AESCTRplain.fst.hints -rw-r--r-- 61.6 KB
Vale.AES.X64.AESCTRplain.fsti.hints -rw-r--r-- 765 bytes
Vale.AES.X64.AESGCM.fst.hints -rw-r--r-- 317.5 KB
Vale.AES.X64.AESGCM.fsti.hints -rw-r--r-- 1.4 KB
Vale.AES.X64.AESGCM_expected_code.fst.hints -rw-r--r-- 561 bytes
Vale.AES.X64.AESGCM_expected_code.fsti.hints -rw-r--r-- 31 bytes
Vale.AES.X64.AESopt.fst.hints -rw-r--r-- 189.8 KB
Vale.AES.X64.AESopt.fsti.hints -rw-r--r-- 14.9 KB
Vale.AES.X64.AESopt2.fst.hints -rw-r--r-- 156.8 KB
Vale.AES.X64.AESopt2.fsti.hints -rw-r--r-- 3.4 KB
Vale.AES.X64.GCMdecrypt.fst.hints -rw-r--r-- 224.3 KB
Vale.AES.X64.GCMdecrypt.fsti.hints -rw-r--r-- 11.2 KB
Vale.AES.X64.GCMdecryptOpt.fst.hints -rw-r--r-- 110.2 KB
Vale.AES.X64.GCMdecryptOpt.fsti.hints -rw-r--r-- 9.9 KB
Vale.AES.X64.GCMencrypt.fst.hints -rw-r--r-- 224.7 KB
Vale.AES.X64.GCMencrypt.fsti.hints -rw-r--r-- 11.2 KB
Vale.AES.X64.GCMencryptOpt.fst.hints -rw-r--r-- 288.6 KB
Vale.AES.X64.GCMencryptOpt.fsti.hints -rw-r--r-- 34.6 KB
Vale.AES.X64.GCTR.fst.hints -rw-r--r-- 155.5 KB
Vale.AES.X64.GCTR.fsti.hints -rw-r--r-- 18.7 KB
Vale.AES.X64.GF128_Init.fst.hints -rw-r--r-- 43.3 KB
Vale.AES.X64.GF128_Init.fsti.hints -rw-r--r-- 2.3 KB
Vale.AES.X64.GF128_Mul.fst.hints -rw-r--r-- 94.4 KB
Vale.AES.X64.GF128_Mul.fsti.hints -rw-r--r-- 850 bytes
Vale.AES.X64.GHash.fst.hints -rw-r--r-- 186.5 KB
Vale.AES.X64.GHash.fsti.hints -rw-r--r-- 18.7 KB
Vale.AES.X64.PolyOps.fst.hints -rw-r--r-- 45.4 KB
Vale.AES.X64.PolyOps.fsti.hints -rw-r--r-- 1.6 KB
Vale.Arch.BufferFriend.fst.hints -rw-r--r-- 58.3 KB
Vale.Arch.BufferFriend.fsti.hints -rw-r--r-- 11.3 KB
Vale.Arch.Heap.fst.hints -rw-r--r-- 475 bytes
Vale.Arch.Heap.fsti.hints -rw-r--r-- 31 bytes
Vale.Arch.HeapImpl.fst.hints -rw-r--r-- 2.0 KB
Vale.Arch.HeapImpl.fsti.hints -rw-r--r-- 36 bytes
Vale.Arch.HeapTypes_s.fst.hints -rw-r--r-- 31 bytes
Vale.Arch.MachineHeap.fst.hints -rw-r--r-- 27.9 KB
Vale.Arch.MachineHeap.fsti.hints -rw-r--r-- 31 bytes
Vale.Arch.MachineHeap_s.fst.hints -rw-r--r-- 4.1 KB
Vale.Arch.Types.fst.hints -rw-r--r-- 85.1 KB
Vale.Arch.Types.fsti.hints -rw-r--r-- 9.8 KB
Vale.Arch.TypesNative.fst.hints -rw-r--r-- 92.2 KB
Vale.Arch.TypesNative.fsti.hints -rw-r--r-- 36.5 KB
Vale.AsLowStar.LowStarSig.fst.hints -rw-r--r-- 55.9 KB
Vale.AsLowStar.MemoryHelpers.fst.hints -rw-r--r-- 118.9 KB
Vale.AsLowStar.MemoryHelpers.fsti.hints -rw-r--r-- 34.9 KB
Vale.AsLowStar.Test.fst.hints -rw-r--r-- 67.8 KB
Vale.AsLowStar.ValeSig.fst.hints -rw-r--r-- 7.9 KB
Vale.AsLowStar.Wrapper.fst.hints -rw-r--r-- 129.5 KB
Vale.AsLowStar.Wrapper.fsti.hints -rw-r--r-- 17.9 KB
Vale.Bignum.Defs.fst.hints -rw-r--r-- 12.7 KB
Vale.Bignum.Defs.fsti.hints -rw-r--r-- 8.8 KB
Vale.Bignum.Lemmas.fst.hints -rw-r--r-- 43.4 KB
Vale.Bignum.Lemmas.fsti.hints -rw-r--r-- 12.8 KB
Vale.Bignum.X64.fst.hints -rw-r--r-- 18.1 KB
Vale.Bignum.X64.fsti.hints -rw-r--r-- 552 bytes
Vale.Curve25519.FastHybrid_helpers.fst.hints -rw-r--r-- 9.2 KB
Vale.Curve25519.FastHybrid_helpers.fsti.hints -rw-r--r-- 3.0 KB
Vale.Curve25519.FastMul_helpers.fst.hints -rw-r--r-- 23.0 KB
Vale.Curve25519.FastMul_helpers.fsti.hints -rw-r--r-- 5.7 KB
Vale.Curve25519.FastSqr_helpers.fst.hints -rw-r--r-- 7.6 KB
Vale.Curve25519.FastSqr_helpers.fsti.hints -rw-r--r-- 1.9 KB
Vale.Curve25519.FastUtil_helpers.fst.hints -rw-r--r-- 8.2 KB
Vale.Curve25519.FastUtil_helpers.fsti.hints -rw-r--r-- 1.6 KB
Vale.Curve25519.Fast_defs.fst.hints -rw-r--r-- 10.6 KB
Vale.Curve25519.Fast_lemmas_external.fst.hints -rw-r--r-- 933 bytes
Vale.Curve25519.Fast_lemmas_external.fsti.hints -rw-r--r-- 46 bytes
Vale.Curve25519.Fast_lemmas_internal.fst.hints -rw-r--r-- 2.8 KB
Vale.Curve25519.Fast_lemmas_internal.fsti.hints -rw-r--r-- 335 bytes
Vale.Curve25519.X64.FastHybrid.fst.hints -rw-r--r-- 187.3 KB
Vale.Curve25519.X64.FastHybrid.fsti.hints -rw-r--r-- 12.4 KB
Vale.Curve25519.X64.FastMul.fst.hints -rw-r--r-- 102.1 KB
Vale.Curve25519.X64.FastMul.fsti.hints -rw-r--r-- 3.9 KB
Vale.Curve25519.X64.FastSqr.fst.hints -rw-r--r-- 76.6 KB
Vale.Curve25519.X64.FastSqr.fsti.hints -rw-r--r-- 4.5 KB
Vale.Curve25519.X64.FastUtil.fst.hints -rw-r--r-- 126.1 KB
Vale.Curve25519.X64.FastUtil.fsti.hints -rw-r--r-- 9.3 KB
Vale.Curve25519.X64.FastWide.fst.hints -rw-r--r-- 93.9 KB
Vale.Curve25519.X64.FastWide.fsti.hints -rw-r--r-- 13.6 KB
Vale.Def.Opaque_s.fst.hints -rw-r--r-- 679 bytes
Vale.Def.Opaque_s.fsti.hints -rw-r--r-- 47 bytes
Vale.Def.PossiblyMonad.fst.hints -rw-r--r-- 12.1 KB
Vale.Def.Prop_s.fst.hints -rw-r--r-- 36 bytes
Vale.Def.TypesNative_s.fst.hints -rw-r--r-- 11.2 KB
Vale.Def.Types_s.fst.hints -rw-r--r-- 32.1 KB
Vale.Def.Words.Four_s.fst.hints -rw-r--r-- 4.1 KB
Vale.Def.Words.Four_s.fsti.hints -rw-r--r-- 4.1 KB
Vale.Def.Words.Seq.fst.hints -rw-r--r-- 39.0 KB
Vale.Def.Words.Seq.fsti.hints -rw-r--r-- 3.8 KB
Vale.Def.Words.Seq_s.fst.hints -rw-r--r-- 20.4 KB
Vale.Def.Words.Seq_s.fsti.hints -rw-r--r-- 11.8 KB
Vale.Def.Words.Two.fst.hints -rw-r--r-- 5.1 KB
Vale.Def.Words.Two.fsti.hints -rw-r--r-- 695 bytes
Vale.Def.Words.Two_s.fst.hints -rw-r--r-- 4.1 KB
Vale.Def.Words.Two_s.fsti.hints -rw-r--r-- 4.1 KB
Vale.Def.Words_s.fst.hints -rw-r--r-- 1.7 KB
Vale.Def.Words_s.fsti.hints -rw-r--r-- 610 bytes
Vale.FDefMulx.X64.fst.hints -rw-r--r-- 12.9 KB
Vale.FDefMulx.X64.fsti.hints -rw-r--r-- 46 bytes
Vale.Inline.X64.Fadd_inline.fst.hints -rw-r--r-- 63.6 KB
Vale.Inline.X64.Fadd_inline.fsti.hints -rw-r--r-- 950 bytes
Vale.Inline.X64.Fmul_inline.fst.hints -rw-r--r-- 65.2 KB
Vale.Inline.X64.Fmul_inline.fsti.hints -rw-r--r-- 2.7 KB
Vale.Inline.X64.Fsqr_inline.fst.hints -rw-r--r-- 39.1 KB
Vale.Inline.X64.Fsqr_inline.fsti.hints -rw-r--r-- 1.8 KB
Vale.Inline.X64.Fswap_inline.fst.hints -rw-r--r-- 26.3 KB
Vale.Inline.X64.Fswap_inline.fsti.hints -rw-r--r-- 951 bytes
Vale.Interop.Assumptions.fst.hints -rw-r--r-- 580 bytes
Vale.Interop.Base.fst.hints -rw-r--r-- 66.5 KB
Vale.Interop.Cast.fst.hints -rw-r--r-- 42.0 KB
Vale.Interop.Cast.fsti.hints -rw-r--r-- 6.3 KB
Vale.Interop.Heap_s.fst.hints -rw-r--r-- 6.2 KB
Vale.Interop.Types.fst.hints -rw-r--r-- 6.4 KB
Vale.Interop.Views.fst.hints -rw-r--r-- 41.8 KB
Vale.Interop.Views.fsti.hints -rw-r--r-- 21.4 KB
Vale.Interop.X64.fst.hints -rw-r--r-- 74.9 KB
Vale.Interop.X64.fsti.hints -rw-r--r-- 57.5 KB
Vale.Interop.fst.hints -rw-r--r-- 89.8 KB
Vale.Interop.fsti.hints -rw-r--r-- 5.1 KB
Vale.Lib.Basic.fst.hints -rw-r--r-- 198 bytes
Vale.Lib.Basic.fsti.hints -rw-r--r-- 32 bytes
Vale.Lib.BufferViewHelpers.fst.hints -rw-r--r-- 2.9 KB
Vale.Lib.Bv_s.fst.hints -rw-r--r-- 695 bytes
Vale.Lib.Lists.fst.hints -rw-r--r-- 16.3 KB
Vale.Lib.Lists.fsti.hints -rw-r--r-- 1.9 KB
Vale.Lib.Map16.fst.hints -rw-r--r-- 4.7 KB
Vale.Lib.Map16.fsti.hints -rw-r--r-- 1.4 KB
Vale.Lib.MapTree.fst.hints -rw-r--r-- 21.7 KB
Vale.Lib.MapTree.fsti.hints -rw-r--r-- 31 bytes
Vale.Lib.Meta.fst.hints -rw-r--r-- 839 bytes
Vale.Lib.Meta.fsti.hints -rw-r--r-- 41 bytes
Vale.Lib.Operator.fst.hints -rw-r--r-- 36 bytes
Vale.Lib.Operator.fsti.hints -rw-r--r-- 36 bytes
Vale.Lib.Seqs.fst.hints -rw-r--r-- 20.4 KB
Vale.Lib.Seqs.fsti.hints -rw-r--r-- 3.1 KB
Vale.Lib.Seqs_s.fst.hints -rw-r--r-- 2.0 KB
Vale.Lib.Set.fst.hints -rw-r--r-- 2.8 KB
Vale.Lib.Set.fsti.hints -rw-r--r-- 36 bytes
Vale.Lib.Tactics.fst.hints -rw-r--r-- 1.1 KB
Vale.Lib.Workarounds.fst.hints -rw-r--r-- 2.7 KB
Vale.Lib.Workarounds.fsti.hints -rw-r--r-- 1017 bytes
Vale.Lib.X64.Cpuid.fst.hints -rw-r--r-- 64.2 KB
Vale.Lib.X64.Cpuid.fsti.hints -rw-r--r-- 2.1 KB
Vale.Lib.X64.Cpuidstdcall.fst.hints -rw-r--r-- 64.2 KB
Vale.Lib.X64.Cpuidstdcall.fsti.hints -rw-r--r-- 9.8 KB
Vale.LowStarHelpers.fst.hints -rw-r--r-- 27 bytes
Vale.Math.Bits.fst.hints -rw-r--r-- 41.3 KB
Vale.Math.Bits.fsti.hints -rw-r--r-- 18.9 KB
Vale.Math.Lemmas.Int.fst.hints -rw-r--r-- 24.4 KB
Vale.Math.Lemmas.Int.fsti.hints -rw-r--r-- 11.1 KB
Vale.Math.Poly2.Bits.fst.hints -rw-r--r-- 62.5 KB
Vale.Math.Poly2.Bits.fsti.hints -rw-r--r-- 2.2 KB
Vale.Math.Poly2.Bits_s.fst.hints -rw-r--r-- 6.5 KB
Vale.Math.Poly2.Bits_s.fsti.hints -rw-r--r-- 5.7 KB
Vale.Math.Poly2.Defs.fst.hints -rw-r--r-- 61.4 KB
Vale.Math.Poly2.Defs_s.fst.hints -rw-r--r-- 32.0 KB
Vale.Math.Poly2.Galois.IntTypes.fst.hints -rw-r--r-- 11.1 KB
Vale.Math.Poly2.Galois.IntTypes.fsti.hints -rw-r--r-- 4.1 KB
Vale.Math.Poly2.Galois.Lemmas.fst.hints -rw-r--r-- 3.3 KB
Vale.Math.Poly2.Galois.Lemmas.fsti.hints -rw-r--r-- 33 bytes
Vale.Math.Poly2.Galois.fst.hints -rw-r--r-- 77.1 KB
Vale.Math.Poly2.Galois.fsti.hints -rw-r--r-- 1.9 KB
Vale.Math.Poly2.Lemmas.fst.hints -rw-r--r-- 26.5 KB
Vale.Math.Poly2.Lemmas.fsti.hints -rw-r--r-- 1.4 KB
Vale.Math.Poly2.Words.fst.hints -rw-r--r-- 9.4 KB
Vale.Math.Poly2.Words.fsti.hints -rw-r--r-- 41 bytes
Vale.Math.Poly2.fst.hints -rw-r--r-- 36.5 KB
Vale.Math.Poly2.fsti.hints -rw-r--r-- 900 bytes
Vale.Math.Poly2_s.fst.hints -rw-r--r-- 7.6 KB
Vale.Math.Poly2_s.fsti.hints -rw-r--r-- 1.9 KB
Vale.Poly1305.Bitvectors.fst.hints -rw-r--r-- 65.5 KB
Vale.Poly1305.Bitvectors.fsti.hints -rw-r--r-- 24.9 KB
Vale.Poly1305.CallingFromLowStar.fst.hints -rw-r--r-- 50.0 KB
Vale.Poly1305.CallingFromLowStar.fsti.hints -rw-r--r-- 7.5 KB
Vale.Poly1305.Equiv.fst.hints -rw-r--r-- 21.1 KB
Vale.Poly1305.Equiv.fsti.hints -rw-r--r-- 3.3 KB
Vale.Poly1305.Math.fst.hints -rw-r--r-- 50.7 KB
Vale.Poly1305.Math.fsti.hints -rw-r--r-- 4.0 KB
Vale.Poly1305.Spec_s.fst.hints -rw-r--r-- 2.5 KB
Vale.Poly1305.Util.fst.hints -rw-r--r-- 9.8 KB
Vale.Poly1305.Util.fsti.hints -rw-r--r-- 3.0 KB
Vale.Poly1305.X64.fst.hints -rw-r--r-- 137.1 KB
Vale.Poly1305.X64.fsti.hints -rw-r--r-- 3.2 KB
Vale.SHA.SHA_helpers.fst.hints -rw-r--r-- 163.6 KB
Vale.SHA.SHA_helpers.fsti.hints -rw-r--r-- 10.4 KB
Vale.SHA.Simplify_Sha.fst.hints -rw-r--r-- 14.3 KB
Vale.SHA.Simplify_Sha.fsti.hints -rw-r--r-- 2.0 KB
Vale.SHA.X64.fst.hints -rw-r--r-- 192.7 KB
Vale.SHA.X64.fsti.hints -rw-r--r-- 3.2 KB
Vale.Stdcalls.X64.Aes.fst.hints -rw-r--r-- 23.0 KB
Vale.Stdcalls.X64.Aes.fsti.hints -rw-r--r-- 20.9 KB
Vale.Stdcalls.X64.AesHash.fst.hints -rw-r--r-- 51.4 KB
Vale.Stdcalls.X64.Cpuid.fst.hints -rw-r--r-- 50.8 KB
Vale.Stdcalls.X64.Cpuid.fsti.hints -rw-r--r-- 39.6 KB
Vale.Stdcalls.X64.Fadd.fst.hints -rw-r--r-- 27.5 KB
Vale.Stdcalls.X64.Fadd.fsti.hints -rw-r--r-- 25.1 KB
Vale.Stdcalls.X64.Fmul.fst.hints -rw-r--r-- 38.6 KB
Vale.Stdcalls.X64.Fmul.fsti.hints -rw-r--r-- 35.1 KB
Vale.Stdcalls.X64.Fsqr.fst.hints -rw-r--r-- 23.5 KB
Vale.Stdcalls.X64.Fsqr.fsti.hints -rw-r--r-- 21.1 KB
Vale.Stdcalls.X64.Fsub.fst.hints -rw-r--r-- 12.0 KB
Vale.Stdcalls.X64.Fsub.fsti.hints -rw-r--r-- 10.6 KB
Vale.Stdcalls.X64.Fswap.fst.hints -rw-r--r-- 14.7 KB
Vale.Stdcalls.X64.Fswap.fsti.hints -rw-r--r-- 13.3 KB
Vale.Stdcalls.X64.GCM_IV.fst.hints -rw-r--r-- 25.4 KB
Vale.Stdcalls.X64.GCMdecrypt.fst.hints -rw-r--r-- 60.0 KB
Vale.Stdcalls.X64.GCMdecryptOpt.fst.hints -rw-r--r-- 54.1 KB
Vale.Stdcalls.X64.GCMencrypt.fst.hints -rw-r--r-- 52.6 KB
Vale.Stdcalls.X64.GCMencrypt.fsti.hints -rw-r--r-- 40.5 KB
Vale.Stdcalls.X64.GCMencryptOpt.fst.hints -rw-r--r-- 53.6 KB
Vale.Stdcalls.X64.GCTR.fst.hints -rw-r--r-- 54.1 KB
Vale.Stdcalls.X64.Poly.fst.hints -rw-r--r-- 15.3 KB
Vale.Stdcalls.X64.Poly.fsti.hints -rw-r--r-- 13.6 KB
Vale.Stdcalls.X64.Sha.fst.hints -rw-r--r-- 16.5 KB
Vale.Stdcalls.X64.Sha.fsti.hints -rw-r--r-- 14.7 KB
Vale.Test.X64.Args.fst.hints -rw-r--r-- 8.0 KB
Vale.Test.X64.Args.fsti.hints -rw-r--r-- 1.2 KB
Vale.Test.X64.Memcpy.fst.hints -rw-r--r-- 6.9 KB
Vale.Test.X64.Memcpy.fsti.hints -rw-r--r-- 42 bytes
Vale.Test.X64.Vale_memcpy.fst.hints -rw-r--r-- 10.9 KB
Vale.Test.X64.Vale_memcpy.fsti.hints -rw-r--r-- 1.2 KB
Vale.Transformers.BoundedInstructionEffects.fst.hints -rw-r--r-- 242.6 KB
Vale.Transformers.BoundedInstructionEffects.fsti.hints -rw-r--r-- 4.7 KB
Vale.Transformers.DebugPrint.fst.hints -rw-r--r-- 3.6 KB
Vale.Transformers.InstructionReorder.fst.hints -rw-r--r-- 365.3 KB
Vale.Transformers.InstructionReorderSanityChecks.fst.hints -rw-r--r-- 4.5 KB
Vale.Transformers.InstructionReorderSanityChecks.fsti.hints -rw-r--r-- 31 bytes
Vale.Transformers.Locations.fst.hints -rw-r--r-- 29.6 KB
Vale.Transformers.Locations.fsti.hints -rw-r--r-- 4.1 KB
Vale.Transformers.Transform.fst.hints -rw-r--r-- 15.9 KB
Vale.Transformers.Transform.fsti.hints -rw-r--r-- 37 bytes
Vale.Wrapper.X64.AES.fst.hints -rw-r--r-- 28.3 KB
Vale.Wrapper.X64.AES.fsti.hints -rw-r--r-- 5.9 KB
Vale.Wrapper.X64.AEShash.fst.hints -rw-r--r-- 19.7 KB
Vale.Wrapper.X64.AEShash.fsti.hints -rw-r--r-- 1.4 KB
Vale.Wrapper.X64.Cpuid.fst.hints -rw-r--r-- 4.6 KB
Vale.Wrapper.X64.Cpuid.fsti.hints -rw-r--r-- 31 bytes
Vale.Wrapper.X64.Fadd.fst.hints -rw-r--r-- 16.2 KB
Vale.Wrapper.X64.Fadd.fsti.hints -rw-r--r-- 950 bytes
Vale.Wrapper.X64.Fmul.fst.hints -rw-r--r-- 24.3 KB
Vale.Wrapper.X64.Fmul.fsti.hints -rw-r--r-- 1.8 KB
Vale.Wrapper.X64.Fsqr.fst.hints -rw-r--r-- 17.0 KB
Vale.Wrapper.X64.Fsqr.fsti.hints -rw-r--r-- 1.8 KB
Vale.Wrapper.X64.Fsub.fst.hints -rw-r--r-- 9.3 KB
Vale.Wrapper.X64.Fsub.fsti.hints -rw-r--r-- 31 bytes
Vale.Wrapper.X64.Fswap.fst.hints -rw-r--r-- 9.2 KB
Vale.Wrapper.X64.Fswap.fsti.hints -rw-r--r-- 37 bytes
Vale.Wrapper.X64.GCM_IV.fst.hints -rw-r--r-- 42.8 KB
Vale.Wrapper.X64.GCM_IV.fsti.hints -rw-r--r-- 2.2 KB
Vale.Wrapper.X64.GCMdecrypt.fst.hints -rw-r--r-- 61.3 KB
Vale.Wrapper.X64.GCMdecrypt.fsti.hints -rw-r--r-- 5.3 KB
Vale.Wrapper.X64.GCMdecryptOpt.fst.hints -rw-r--r-- 82.6 KB
Vale.Wrapper.X64.GCMdecryptOpt.fsti.hints -rw-r--r-- 9.8 KB
Vale.Wrapper.X64.GCMdecryptOpt256.fst.hints -rw-r--r-- 78.8 KB
Vale.Wrapper.X64.GCMdecryptOpt256.fsti.hints -rw-r--r-- 6.8 KB
Vale.Wrapper.X64.GCMencrypt.fst.hints -rw-r--r-- 29.5 KB
Vale.Wrapper.X64.GCMencrypt.fsti.hints -rw-r--r-- 7.9 KB
Vale.Wrapper.X64.GCMencryptOpt.fst.hints -rw-r--r-- 83.7 KB
Vale.Wrapper.X64.GCMencryptOpt.fsti.hints -rw-r--r-- 9.8 KB
Vale.Wrapper.X64.GCMencryptOpt256.fst.hints -rw-r--r-- 78.2 KB
Vale.Wrapper.X64.GCMencryptOpt256.fsti.hints -rw-r--r-- 6.8 KB
Vale.Wrapper.X64.GCTR.fst.hints -rw-r--r-- 75.8 KB
Vale.Wrapper.X64.GCTR.fsti.hints -rw-r--r-- 2.0 KB
Vale.Wrapper.X64.Poly.fst.hints -rw-r--r-- 14.7 KB
Vale.Wrapper.X64.Poly.fsti.hints -rw-r--r-- 5.8 KB
Vale.Wrapper.X64.Sha.fst.hints -rw-r--r-- 38.1 KB
Vale.Wrapper.X64.Sha.fsti.hints -rw-r--r-- 1.2 KB
Vale.X64.BufferViewStore.fst.hints -rw-r--r-- 35.3 KB
Vale.X64.BufferViewStore.fsti.hints -rw-r--r-- 5.5 KB
Vale.X64.Bytes_Code_s.fst.hints -rw-r--r-- 68.5 KB
Vale.X64.Bytes_Semantics.fst.hints -rw-r--r-- 37 bytes
Vale.X64.Bytes_Semantics.fsti.hints -rw-r--r-- 31 bytes
Vale.X64.CPU_Features_s.fst.hints -rw-r--r-- 46 bytes
Vale.X64.CryptoInstructions_s.fst.hints -rw-r--r-- 6.3 KB
Vale.X64.CryptoInstructions_s.fsti.hints -rw-r--r-- 36 bytes
Vale.X64.Decls.fst.hints -rw-r--r-- 76.3 KB
Vale.X64.Decls.fsti.hints -rw-r--r-- 41.2 KB
Vale.X64.Flags.fst.hints -rw-r--r-- 4.7 KB
Vale.X64.Flags.fsti.hints -rw-r--r-- 32 bytes
Vale.X64.InsAes.fst.hints -rw-r--r-- 221.9 KB
Vale.X64.InsAes.fsti.hints -rw-r--r-- 2.6 KB
Vale.X64.InsBasic.fst.hints -rw-r--r-- 664.5 KB
Vale.X64.InsBasic.fsti.hints -rw-r--r-- 11.2 KB
Vale.X64.InsLemmas.fst.hints -rw-r--r-- 18.2 KB
Vale.X64.InsLemmas.fsti.hints -rw-r--r-- 6.4 KB
Vale.X64.InsMem.fst.hints -rw-r--r-- 90.7 KB
Vale.X64.InsMem.fsti.hints -rw-r--r-- 1.1 KB
Vale.X64.InsSha.fst.hints -rw-r--r-- 66.5 KB
Vale.X64.InsSha.fsti.hints -rw-r--r-- 4.4 KB
Vale.X64.InsStack.fst.hints -rw-r--r-- 140.4 KB
Vale.X64.InsStack.fsti.hints -rw-r--r-- 2.3 KB
Vale.X64.InsVector.fst.hints -rw-r--r-- 790.4 KB
Vale.X64.InsVector.fsti.hints -rw-r--r-- 14.2 KB
Vale.X64.Instruction_s.fst.hints -rw-r--r-- 22.1 KB
Vale.X64.Instruction_s.fsti.hints -rw-r--r-- 14.3 KB
Vale.X64.Instructions_s.fst.hints -rw-r--r-- 8.7 KB
Vale.X64.Instructions_s.fsti.hints -rw-r--r-- 7.3 KB
Vale.X64.Leakage.fst.hints -rw-r--r-- 89.6 KB
Vale.X64.Leakage.fsti.hints -rw-r--r-- 33 bytes
Vale.X64.Leakage_Helpers.fst.hints -rw-r--r-- 34.2 KB
Vale.X64.Leakage_Ins.fst.hints -rw-r--r-- 285.0 KB
Vale.X64.Leakage_Ins.fsti.hints -rw-r--r-- 32 bytes
Vale.X64.Leakage_s.fst.hints -rw-r--r-- 6.8 KB
Vale.X64.Lemmas.fst.hints -rw-r--r-- 113.8 KB
Vale.X64.Lemmas.fsti.hints -rw-r--r-- 11.0 KB
Vale.X64.Machine_Semantics_s.fst.hints -rw-r--r-- 103.5 KB
Vale.X64.Machine_s.fst.hints -rw-r--r-- 39.9 KB
Vale.X64.Memory.fst.hints -rw-r--r-- 161.6 KB
Vale.X64.Memory.fsti.hints -rw-r--r-- 2.8 KB
Vale.X64.MemoryAdapters.fst.hints -rw-r--r-- 8.9 KB
Vale.X64.MemoryAdapters.fsti.hints -rw-r--r-- 452 bytes
Vale.X64.Memory_Sems.fst.hints -rw-r--r-- 151.5 KB
Vale.X64.Memory_Sems.fsti.hints -rw-r--r-- 3.5 KB
Vale.X64.Print_Inline_s.fst.hints -rw-r--r-- 33.5 KB
Vale.X64.Print_s.fst.hints -rw-r--r-- 27.0 KB
Vale.X64.QuickCode.fst.hints -rw-r--r-- 13.6 KB
Vale.X64.QuickCodes.fst.hints -rw-r--r-- 92.9 KB
Vale.X64.QuickCodes.fsti.hints -rw-r--r-- 48.3 KB
Vale.X64.Regs.fst.hints -rw-r--r-- 12.5 KB
Vale.X64.Regs.fsti.hints -rw-r--r-- 3.6 KB
Vale.X64.Stack.fst.hints -rw-r--r-- 18.7 KB
Vale.X64.Stack.fsti.hints -rw-r--r-- 576 bytes
Vale.X64.Stack_Sems.fst.hints -rw-r--r-- 6.3 KB
Vale.X64.Stack_Sems.fsti.hints -rw-r--r-- 191 bytes
Vale.X64.Stack_i.fst.hints -rw-r--r-- 17.7 KB
Vale.X64.Stack_i.fsti.hints -rw-r--r-- 381 bytes
Vale.X64.State.fst.hints -rw-r--r-- 4.5 KB
Vale.X64.State.fsti.hints -rw-r--r-- 4.5 KB
Vale.X64.StateLemmas.fst.hints -rw-r--r-- 20.1 KB
Vale.X64.StateLemmas.fsti.hints -rw-r--r-- 3.7 KB
Vale.X64.Taint_Semantics.fst.hints -rw-r--r-- 335 bytes
Vale.X64.Xmms.fst.hints -rw-r--r-- 56 bytes
Vale.X64.Xmms.fsti.hints -rw-r--r-- 32 bytes
WasmSupport.fst.hints -rw-r--r-- 974 bytes
X64.AESstdcall.fst.hints -rw-r--r-- 39.4 KB
X64.AESstdcall.fsti.hints -rw-r--r-- 8.4 KB
X64.GCMencryptstdcall.fst.hints -rw-r--r-- 16.5 KB
X64.GCMencryptstdcall.fsti.hints -rw-r--r-- 3.3 KB
X64.GCTRstdcall.fst.hints -rw-r--r-- 55.4 KB
X64.GCTRstdcall.fsti.hints -rw-r--r-- 10.0 KB
X64.GHashstdcall.fst.hints -rw-r--r-- 50.2 KB
X64.GHashstdcall.fsti.hints -rw-r--r-- 5.8 KB
X64.Leakage_Ins_Xmm.fst.hints -rw-r--r-- 64.8 KB
X64.Leakage_Ins_Xmm.fsti.hints -rw-r--r-- 46 bytes
X64.Util.fst.hints -rw-r--r-- 71.5 KB
X64.Util.fsti.hints -rw-r--r-- 11.1 KB

back to top