Revision 724d1045f60f13d79df1afc5190955afdfa73ec1 authored by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC, committed by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC
Co-authored-by: @protz
1 parent ca37fbf
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,
"03788193e1cd8324db8731b832180944"
],
[
"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,
"1cd0e8ba7b33db2cc066ade5779c4b4e"
],
[
"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,
"66fb66070cc959d335aff444a237923e"
],
[
"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,
"93cd4884cd43c906fa58845df0be95b7"
],
[
"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,
"3d582177eda481eaa3af7cf8c14681da"
],
[
"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,
"9dc5b387a3a08f8a7ccadff1904cb46e"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...