Revision e56414221fb67ecff7d071497f8ba5d20e9c5ba9 authored by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC, committed by Dzomo, the Everest Yak on 01 May 2020, 08:20:34 UTC
1 parent db297bf
Spec.Frodo.Test.fst.hints
[
"���!h}\u0017�\u001e��2�\u0004T",
[
[
"Spec.Frodo.Test.print_and_compare",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"fuel_guarded_inversion_FStar.Pervasives.result",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"6a2bce9fc6d9eaf8befe06f30b653f3d"
],
[
"Spec.Frodo.Test.compare",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"cce986120f8799abd7b29d0a14331492"
],
[
"Spec.Frodo.Test.test_frodo",
1,
0,
1,
[ "@query" ],
0,
"46e3f38eb8a9ea09bce9dbe5d55ceca1"
],
[
"Spec.Frodo.Test.test_frodo",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "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",
"fuel_guarded_inversion_FStar.Pervasives.result",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Spec.AES.elem", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0620b258a6f11cb27ad9730a75d2bac5",
"refinement_interpretation_Tm_refine_09487a6d0139c340d9307f407b8b24c6",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_3220fed3646f93806dd397676d9cb32a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_68ee6d2c8678eb431259a3d4f412550b",
"refinement_interpretation_Tm_refine_6c4d0917f0123af6d52ee2d0c304a1d6",
"refinement_interpretation_Tm_refine_6d461cd473e8c77338c11e6a9a00df84",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_c6248fc27518d8196ba1f5e49810d77c",
"refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e8f00c92e4678ea1eb9b934e6fa46592",
"typing_FStar.List.Tot.Base.length",
"typing_FStar.Seq.Properties.seq_of_list",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned",
"typing_Spec.AES.gf8", "typing_Spec.Frodo.Params.bytes_mu",
"typing_Spec.Frodo.Params.crypto_bytes",
"typing_Spec.Frodo.Params.crypto_ciphertextbytes",
"typing_Spec.Frodo.Params.crypto_publickeybytes",
"typing_Spec.Frodo.Params.crypto_secretkeybytes",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"47636818f3688eae91bc13491ba82999"
],
[
"Spec.Frodo.Test.test",
1,
0,
1,
[ "@query" ],
0,
"b2bfc6999e14632c5b7de25b6cbce235"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...