| C.Endianness.fst.hints | -rwxr-xr-x | 18.5 KB |
| C.Loops.fst.hints | -rwxr-xr-x | 38.3 KB |
| C.String.fst.hints | -rwxr-xr-x | 3.3 KB |
| C.fst.hints | -rwxr-xr-x | 369 bytes |
| FStar.Kremlin.Endianness.fst.hints | -rwxr-xr-x | 108.7 KB |
| Frodo.KEM.fst.hints | -rw-r--r-- | 1.8 KB |
| Frodo.Params.fst.hints | -rw-r--r-- | 12.7 KB |
| Hacl.AES128.fsti.hints | -rw-r--r-- | 7.7 KB |
| Hacl.Blake2s.fst.hints | -rw-r--r-- | 15.8 KB |
| Hacl.Chacha20.Vec128.fst.hints | -rw-r--r-- | 2.8 KB |
| Hacl.Chacha20.Vec256.fst.hints | -rw-r--r-- | 2.8 KB |
| Hacl.Chacha20.Vec32.fst.hints | -rw-r--r-- | 3.2 KB |
| Hacl.Chacha20.fst.hints | -rw-r--r-- | 7.0 KB |
| Hacl.Chacha20Poly1305_128.fst.hints | -rw-r--r-- | 37 bytes |
| Hacl.Chacha20Poly1305_256.fst.hints | -rw-r--r-- | 32 bytes |
| Hacl.Chacha20Poly1305_32.fst.hints | -rw-r--r-- | 43 bytes |
| Hacl.Curve25519_51.fst.hints | -rw-r--r-- | 9.3 KB |
| Hacl.Curve25519_64.fst.hints | -rw-r--r-- | 9.3 KB |
| Hacl.Frodo.Clear.fsti.hints | -rw-r--r-- | 5.6 KB |
| Hacl.Frodo.KEM.fst.hints | -rw-r--r-- | 5.6 KB |
| Hacl.Frodo.Random.fsti.hints | -rw-r--r-- | 3.2 KB |
| Hacl.Hash.Core.SHA2.Constants.fst.hints | -rwxr-xr-x | 1.2 KB |
| Hacl.Hash.Core.SHA2.fst.hints | -rwxr-xr-x | 65.7 KB |
| Hacl.Hash.Core.SHA2.fsti.hints | -rwxr-xr-x | 37 bytes |
| Hacl.Hash.Definitions.fst.hints | -rwxr-xr-x | 13.8 KB |
| Hacl.Hash.Lemmas.fst.hints | -rwxr-xr-x | 8.4 KB |
| Hacl.Hash.MD.fst.hints | -rwxr-xr-x | 41.6 KB |
| Hacl.Hash.MD.fsti.hints | -rwxr-xr-x | 26 bytes |
| Hacl.Hash.PadFinish.fst.hints | -rwxr-xr-x | 45.8 KB |
| Hacl.Hash.PadFinish.fsti.hints | -rwxr-xr-x | 829 bytes |
| Hacl.Hash.SHA2.fst.hints | -rwxr-xr-x | 5.8 KB |
| Hacl.Hash.SHA2.fsti.hints | -rwxr-xr-x | 1.4 KB |
| Hacl.Impl.Blake2s.fst.hints | -rw-r--r-- | 202.5 KB |
| Hacl.Impl.Box.fst.hints | -rw-r--r-- | 90.7 KB |
| Hacl.Impl.Chacha20.Core32.fst.hints | -rw-r--r-- | 74.7 KB |
| Hacl.Impl.Chacha20.Core32xN.fst.hints | -rw-r--r-- | 123.5 KB |
| Hacl.Impl.Chacha20.Vec.fst.hints | -rw-r--r-- | 158.6 KB |
| Hacl.Impl.Chacha20.fst.hints | -rw-r--r-- | 90.2 KB |
| Hacl.Impl.Chacha20Poly1305.PolyCore.fst.hints | -rw-r--r-- | 14.1 KB |
| Hacl.Impl.Chacha20Poly1305.fst.hints | -rw-r--r-- | 63.8 KB |
| Hacl.Impl.Chacha20Poly1305.fsti.hints | -rw-r--r-- | 7.0 KB |
| Hacl.Impl.Curve25519.AddAndDouble.fst.hints | -rw-r--r-- | 116.5 KB |
| Hacl.Impl.Curve25519.Field51.fst.hints | -rw-r--r-- | 104.6 KB |
| Hacl.Impl.Curve25519.Field64.Core.fst.hints | -rw-r--r-- | 60.4 KB |
| Hacl.Impl.Curve25519.Field64.Core.fsti.hints | -rw-r--r-- | 14.3 KB |
| Hacl.Impl.Curve25519.Field64.fst.hints | -rw-r--r-- | 48.3 KB |
| Hacl.Impl.Curve25519.Fields.fst.hints | -rw-r--r-- | 82.3 KB |
| Hacl.Impl.Curve25519.Finv.fst.hints | -rw-r--r-- | 52.2 KB |
| Hacl.Impl.Curve25519.Generic.fst.hints | -rw-r--r-- | 229.8 KB |
| Hacl.Impl.Curve25519.Generic.fsti.hints | -rw-r--r-- | 8.5 KB |
| Hacl.Impl.Curve25519.Lemmas.fst.hints | -rw-r--r-- | 4.9 KB |
| Hacl.Impl.Frodo.Encode.fst.hints | -rw-r--r-- | 96.9 KB |
| Hacl.Impl.Frodo.Gen.fst.hints | -rw-r--r-- | 85.7 KB |
| Hacl.Impl.Frodo.KEM.Decaps.fst.hints | -rw-r--r-- | 142.8 KB |
| Hacl.Impl.Frodo.KEM.Encaps.fst.hints | -rw-r--r-- | 180.2 KB |
| Hacl.Impl.Frodo.KEM.KeyGen.fst.hints | -rw-r--r-- | 75.9 KB |
| Hacl.Impl.Frodo.KEM.fst.hints | -rw-r--r-- | 16.1 KB |
| Hacl.Impl.Frodo.Pack.fst.hints | -rw-r--r-- | 72.2 KB |
| Hacl.Impl.Frodo.Params.fst.hints | -rw-r--r-- | 27 bytes |
| Hacl.Impl.Frodo.Sample.fst.hints | -rw-r--r-- | 52.6 KB |
| Hacl.Impl.HSalsa20.fst.hints | -rw-r--r-- | 25.5 KB |
| Hacl.Impl.Matrix.fst.hints | -rw-r--r-- | 137.1 KB |
| Hacl.Impl.Poly1305.Field32xN.fst.hints | -rw-r--r-- | 282.8 KB |
| Hacl.Impl.Poly1305.Fields.fst.hints | -rw-r--r-- | 89.3 KB |
| Hacl.Impl.Poly1305.Lemmas.fst.hints | -rw-r--r-- | 44.3 KB |
| Hacl.Impl.Poly1305.fst.hints | -rw-r--r-- | 286.2 KB |
| Hacl.Impl.Poly1305.fsti.hints | -rw-r--r-- | 10.1 KB |
| Hacl.Impl.SHA3.fst.hints | -rw-r--r-- | 218.0 KB |
| Hacl.Impl.Salsa20.Core32.fst.hints | -rw-r--r-- | 67.3 KB |
| Hacl.Impl.Salsa20.fst.hints | -rw-r--r-- | 100.6 KB |
| Hacl.Impl.SecretBox.fst.hints | -rw-r--r-- | 98.3 KB |
| Hacl.Keccak.fsti.hints | -rw-r--r-- | 3.5 KB |
| Hacl.NaCl.fst.hints | -rw-r--r-- | 55.1 KB |
| Hacl.Poly1305.Field32xN.Lemmas.fst.hints | -rw-r--r-- | 344.7 KB |
| Hacl.Poly1305_128.fst.hints | -rw-r--r-- | 17.8 KB |
| Hacl.Poly1305_256.fst.hints | -rw-r--r-- | 17.9 KB |
| Hacl.Poly1305_32.fst.hints | -rw-r--r-- | 19.1 KB |
| Hacl.SHA3.fst.hints | -rw-r--r-- | 45.5 KB |
| Hacl.Salsa20.fst.hints | -rw-r--r-- | 12.8 KB |
| Hacl.Spec.Chacha20.Equiv.fst.hints | -rw-r--r-- | 84.4 KB |
| Hacl.Spec.Chacha20.Vec.Lemmas.fst.hints | -rw-r--r-- | 206.5 KB |
| Hacl.Spec.Chacha20.Vec.fst.hints | -rw-r--r-- | 57.1 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-- | 117.5 KB |
| Hacl.Spec.Curve25519.Field51.fst.hints | -rw-r--r-- | 69.8 KB |
| Hacl.Spec.Curve25519.Field64.Core.fst.hints | -rw-r--r-- | 50.6 KB |
| Hacl.Spec.Curve25519.Field64.Definition.fst.hints | -rw-r--r-- | 3.1 KB |
| Hacl.Spec.Curve25519.Field64.Lemmas.fst.hints | -rw-r--r-- | 35.3 KB |
| Hacl.Spec.Curve25519.Field64.fst.hints | -rw-r--r-- | 23.7 KB |
| Hacl.Spec.Curve25519.Finv.fst.hints | -rw-r--r-- | 17.3 KB |
| Hacl.Spec.Poly1305.Equiv.fst.hints | -rw-r--r-- | 76.5 KB |
| Hacl.Spec.Poly1305.Field32xN.Lemmas.fst.hints | -rw-r--r-- | 149.0 KB |
| Hacl.Spec.Poly1305.Field32xN.fst.hints | -rw-r--r-- | 63.5 KB |
| Hacl.Spec.Poly1305.Lemmas.fst.hints | -rwxr-xr-x | 11.7 KB |
| Hacl.Spec.Poly1305.Vec.fst.hints | -rw-r--r-- | 31.4 KB |
| Hacl.Test.Blake2s.fst.hints | -rw-r--r-- | 27 bytes |
| Hacl.Test.Frodo.fst.hints | -rw-r--r-- | 41.1 KB |
| Hacl.Test.SHA2.fst.hints | -rwxr-xr-x | 74.9 KB |
| Hacl.Test.SHA3.fst.hints | -rw-r--r-- | 135.8 KB |
| Lib.Buffer.fst.hints | -rw-r--r-- | 281.8 KB |
| Lib.Buffer.fsti.hints | -rw-r--r-- | 62.3 KB |
| Lib.ByteBuffer.fst.hints | -rw-r--r-- | 169.2 KB |
| Lib.ByteBuffer.fsti.hints | -rw-r--r-- | 28.8 KB |
| Lib.ByteSequence.Tuples.fsti.hints | -rw-r--r-- | 4.7 KB |
| Lib.ByteSequence.fst.hints | -rw-r--r-- | 193.1 KB |
| Lib.ByteSequence.fsti.hints | -rw-r--r-- | 34.4 KB |
| Lib.FixedSequence.fst.hints | -rw-r--r-- | 50.7 KB |
| Lib.IntTypes.Compatibility.fst.hints | -rw-r--r-- | 2.5 KB |
| Lib.IntTypes.fst.hints | -rw-r--r-- | 350.8 KB |
| Lib.IntTypes.fsti.hints | -rw-r--r-- | 39.8 KB |
| Lib.IntVector.Intrinsics.fsti.hints | -rw-r--r-- | 39 bytes |
| Lib.IntVector.Random.fsti.hints | -rw-r--r-- | 1.7 KB |
| Lib.IntVector.fst.hints | -rw-r--r-- | 184 bytes |
| Lib.IntVector.fsti.hints | -rw-r--r-- | 102.2 KB |
| Lib.LoopCombinators.fst.hints | -rw-r--r-- | 43.5 KB |
| Lib.LoopCombinators.fsti.hints | -rw-r--r-- | 11.2 KB |
| Lib.Loops.Lemmas.fst.hints | -rw-r--r-- | 53.2 KB |
| Lib.Loops.Lemmas.fsti.hints | -rw-r--r-- | 9.6 KB |
| Lib.Loops.fst.hints | -rw-r--r-- | 13.0 KB |
| Lib.Loops.fsti.hints | -rw-r--r-- | 1.2 KB |
| Lib.NatMod.fst.hints | -rw-r--r-- | 3.6 KB |
| Lib.NatMod.fsti.hints | -rw-r--r-- | 169 bytes |
| Lib.Network.fst.hints | -rw-r--r-- | 31 bytes |
| Lib.Network.fsti.hints | -rw-r--r-- | 39 bytes |
| Lib.NumericVector.fst.hints | -rw-r--r-- | 61.9 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.Hardware.fst.hints | -rw-r--r-- | 28.8 KB |
| Lib.RandomBuffer.Hardware.fsti.hints | -rw-r--r-- | 368 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.RawIntTypes.fst.hints | -rw-r--r-- | 10.2 KB |
| Lib.RawIntTypes.fsti.hints | -rw-r--r-- | 4.2 KB |
| Lib.Result.fst.hints | -rw-r--r-- | 1.2 KB |
| Lib.Sequence.fst.hints | -rwxr-xr-x | 72.7 KB |
| Lib.Sequence.fsti.hints | -rw-r--r-- | 22.2 KB |
| Loops.fst.hints | -rw-r--r-- | 65.7 KB |
| Spec.AES.fst.hints | -rw-r--r-- | 96.8 KB |
| Spec.AES128_CBC.fst.hints | -rw-r--r-- | 18.1 KB |
| Spec.AES128_GCM.fst.hints | -rw-r--r-- | 10.5 KB |
| Spec.AES256.fst.hints | -rw-r--r-- | 47.0 KB |
| Spec.AES256_CBC.fst.hints | -rw-r--r-- | 17.6 KB |
| Spec.AES256_GCM.fst.hints | -rw-r--r-- | 17.4 KB |
| Spec.AES_GCM.fst.hints | -rw-r--r-- | 13.8 KB |
| Spec.Agile.AEAD.fst.hints | -rwxr-xr-x | 14.1 KB |
| Spec.Agile.CTR.fst.hints | -rw-r--r-- | 12.0 KB |
| Spec.Agile.Cipher.fst.hints | -rw-r--r-- | 7.5 KB |
| Spec.Agile.DH.fst.hints | -rw-r--r-- | 3.6 KB |
| Spec.Agile.HKDF.fst.hints | -rw-r--r-- | 20.3 KB |
| Spec.Agile.HKDF.fsti.hints | -rw-r--r-- | 2.9 KB |
| Spec.Agile.HMAC.fst.hints | -rw-r--r-- | 7.5 KB |
| Spec.Agile.HMAC.fsti.hints | -rw-r--r-- | 1.1 KB |
| Spec.Agile.Hash.fst.hints | -rw-r--r-- | 19.1 KB |
| Spec.Agile.Hash.fsti.hints | -rw-r--r-- | 5.1 KB |
| Spec.Argon2i.fst.hints | -rw-r--r-- | 59.4 KB |
| Spec.Blake2.Incremental.fst.hints | -rw-r--r-- | 13.9 KB |
| Spec.Blake2.fst.hints | -rw-r--r-- | 57.3 KB |
| Spec.Box.fst.hints | -rw-r--r-- | 10.6 KB |
| Spec.Chacha20.fst.hints | -rw-r--r-- | 22.1 KB |
| Spec.Chacha20Poly1305.fst.hints | -rw-r--r-- | 12.2 KB |
| Spec.Curve25519.Lemmas.fst.hints | -rw-r--r-- | 748 bytes |
| Spec.Curve25519.fst.hints | -rw-r--r-- | 16.2 KB |
| Spec.Curve448.Lemmas.fst.hints | -rw-r--r-- | 747 bytes |
| Spec.Curve448.fst.hints | -rw-r--r-- | 15.1 KB |
| Spec.ESCH.fst.hints | -rw-r--r-- | 22.9 KB |
| Spec.Ed25519.fst.hints | -rw-r--r-- | 29.1 KB |
| Spec.Frodo.Encode.fst.hints | -rw-r--r-- | 58.3 KB |
| Spec.Frodo.Gen.fst.hints | -rw-r--r-- | 38.4 KB |
| Spec.Frodo.KEM.Decaps.fst.hints | -rw-r--r-- | 47.5 KB |
| Spec.Frodo.KEM.Encaps.fst.hints | -rw-r--r-- | 50.9 KB |
| Spec.Frodo.KEM.KeyGen.fst.hints | -rw-r--r-- | 16.4 KB |
| Spec.Frodo.KEM.fst.hints | -rw-r--r-- | 11.1 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.5 KB |
| Spec.Frodo.Params.fst.hints | -rw-r--r-- | 31 bytes |
| Spec.Frodo.Random.fst.hints | -rw-r--r-- | 834 bytes |
| Spec.Frodo.Sample.fst.hints | -rw-r--r-- | 36.5 KB |
| Spec.Frodo.Test.fst.hints | -rw-r--r-- | 5.4 KB |
| Spec.Frodo.Test.fsti.hints | -rw-r--r-- | 31 bytes |
| Spec.GF128.fst.hints | -rw-r--r-- | 10.5 KB |
| Spec.GaloisField.fst.hints | -rw-r--r-- | 19.3 KB |
| Spec.Gimli.fst.hints | -rw-r--r-- | 17.6 KB |
| Spec.HKDF.fst.hints | -rw-r--r-- | 30.6 KB |
| Spec.HKDF.fsti.hints | -rw-r--r-- | 5.4 KB |
| Spec.HMAC.fst.hints | -rw-r--r-- | 22.9 KB |
| Spec.HMAC.fsti.hints | -rw-r--r-- | 1.2 KB |
| Spec.Hash.Definitions.fst.hints | -rw-r--r-- | 17.9 KB |
| Spec.Hash.Incremental.fst.hints | -rw-r--r-- | 3.6 KB |
| Spec.Hash.Lemmas.fst.hints | -rw-r--r-- | 25.0 KB |
| Spec.Hash.Lemmas0.fst.hints | -rw-r--r-- | 2.8 KB |
| Spec.Hash.PadFinish.fst.hints | -rw-r--r-- | 5.5 KB |
| Spec.Hash.fst.hints | -rw-r--r-- | 8.5 KB |
| Spec.Kyber.fst.hints | -rw-r--r-- | 14.6 KB |
| Spec.Loops.fst.hints | -rwxr-xr-x | 14.3 KB |
| Spec.MD5.fst.hints | -rw-r--r-- | 16.8 KB |
| Spec.MD5.fsti.hints | -rw-r--r-- | 31 bytes |
| Spec.Matrix.fst.hints | -rw-r--r-- | 67.4 KB |
| Spec.P256.Montgomery.fst.hints | -rw-r--r-- | 39.1 KB |
| Spec.P256.fst.hints | -rw-r--r-- | 13.5 KB |
| Spec.Poly1305.fst.hints | -rw-r--r-- | 8.3 KB |
| Spec.RSAPSS.fst.hints | -rw-r--r-- | 25.7 KB |
| Spec.SHA1.fst.hints | -rw-r--r-- | 26.3 KB |
| Spec.SHA1.fsti.hints | -rw-r--r-- | 32 bytes |
| Spec.SHA2.Constants.fst.hints | -rw-r--r-- | 6.0 KB |
| Spec.SHA2.Fixed.fst.hints | -rw-r--r-- | 59.6 KB |
| Spec.SHA2.Normal.fst.hints | -rw-r--r-- | 67.9 KB |
| Spec.SHA2.fst.hints | -rw-r--r-- | 42.1 KB |
| Spec.SHA2.fsti.hints | -rw-r--r-- | 44 bytes |
| Spec.SHA3.Constants.fst.hints | -rw-r--r-- | 5.6 KB |
| Spec.SHA3.fst.hints | -rw-r--r-- | 44.5 KB |
| Spec.SPARKLE.fst.hints | -rw-r--r-- | 20.8 KB |
| Spec.Salsa20.fst.hints | -rw-r--r-- | 30.2 KB |
| Spec.SecretBox.fst.hints | -rw-r--r-- | 16.7 KB |
| Tutorial.fst.hints | -rw-r--r-- | 64.2 KB |
