Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Hacl.Frodo.KEM.fst.hints
[
"���!���w|z�Hu5\n�",
[
[
"Hacl.Frodo.KEM.crypto_kem_keypair",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Impl.Frodo.KEM.crypto_publickeybytes",
"equation_Hacl.Impl.Frodo.KEM.crypto_secretkeybytes",
"equation_Prims.nat",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_4217a417164cd9f176884ac8e9b5b15e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_69549b60200c25e52f3ec15580491456",
"typing_Hacl.Impl.Frodo.KEM.crypto_publickeybytes",
"typing_Hacl.Impl.Frodo.KEM.crypto_secretkeybytes",
"typing_Spec.Frodo.Params.crypto_publickeybytes"
],
0,
"a1b4126e9f10a47548c407a30de82286"
],
[
"Hacl.Frodo.KEM.crypto_kem_keypair",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
"equation_Lib.Buffer.as_seq",
"equation_Spec.Frodo.KEM.crypto_kem_keypair",
"refinement_interpretation_Tm_refine_148a9e4bd44d8685602f741e69eaf8b6",
"refinement_interpretation_Tm_refine_bac3d0e24bb03b02d8e9b1701ecb7798"
],
0,
"8d4120728fd967450cb4f40d31afa8ce"
],
[
"Hacl.Frodo.KEM.crypto_kem_enc",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Impl.Frodo.KEM.crypto_ciphertextbytes",
"equation_Hacl.Impl.Frodo.KEM.crypto_publickeybytes",
"equation_Hacl.Impl.Matrix.lbytes", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Frodo.Params.bytes_seed_a",
"equation_Spec.Frodo.Params.crypto_bytes",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_68ee6d2c8678eb431259a3d4f412550b",
"refinement_interpretation_Tm_refine_69549b60200c25e52f3ec15580491456",
"refinement_interpretation_Tm_refine_8456759e660370b6e428c86ad6758869",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"typing_Hacl.Impl.Frodo.KEM.crypto_ciphertextbytes",
"typing_Hacl.Impl.Frodo.KEM.crypto_publickeybytes",
"typing_Lib.Buffer.length", "typing_Spec.Frodo.Params.bytes_seed_a",
"typing_Spec.Frodo.Params.crypto_ciphertextbytes",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"e48e268a7f11c21d3ccef8af772ed885"
],
[
"Hacl.Frodo.KEM.crypto_kem_enc",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
"equation_Lib.Buffer.as_seq",
"equation_Spec.Frodo.KEM.crypto_kem_enc",
"refinement_interpretation_Tm_refine_da64859381eb6be468ffc65716ff1ca4",
"refinement_interpretation_Tm_refine_f1cfbbcf1c55d03ed8d5565aa798aa5d"
],
0,
"42341b542cc78e31e1cf4948c7c04332"
],
[
"Hacl.Frodo.KEM.crypto_kem_dec",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Impl.Frodo.KEM.crypto_ciphertextbytes",
"equation_Hacl.Impl.Frodo.KEM.crypto_secretkeybytes",
"equation_Hacl.Impl.Matrix.lbytes", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Frodo.Params.crypto_bytes",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_4217a417164cd9f176884ac8e9b5b15e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_68ee6d2c8678eb431259a3d4f412550b",
"refinement_interpretation_Tm_refine_8456759e660370b6e428c86ad6758869",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Hacl.Impl.Frodo.KEM.crypto_ciphertextbytes",
"typing_Hacl.Impl.Frodo.KEM.crypto_secretkeybytes",
"typing_Lib.Buffer.length", "typing_Spec.Frodo.Params.crypto_bytes",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"73a21fa9b8c00c6dc7b2776a21053fec"
],
[
"Hacl.Frodo.KEM.crypto_kem_dec",
2,
0,
0,
[
"@query", "equality_tok_Lib.Buffer.MUT@tok",
"equation_Lib.Buffer.as_seq",
"equation_Spec.Frodo.KEM.crypto_kem_dec"
],
0,
"621eabc02c03c68d27ba754a2c8cc2f0"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...