Revision 027cee49342e5e1ac0ccf4ca6e4b5b868e70a0a2 authored by Aseem Rastogi on 22 March 2020, 07:14:03 UTC, committed by Aseem Rastogi on 22 March 2020, 07:14:03 UTC
1 parent df0c85e
Spec.Frodo.Gen.fst.hints
[
"�\u0017p�Bj��b�\u0010��\u0011",
[
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake_fc",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.v", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"5d207be27e8e376f476012f9294577ba"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a"
],
0,
"168089b4d2d9f9932187f841dd4567e7"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake0",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a"
],
0,
"62427f7937767c6a6ae550de76fe6d49"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake0",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"284449656493928633be0c6a3aa5eb7b"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake1",
1,
0,
0,
[ "@query" ],
0,
"8b2c153430ff8488ec2a357fecde9912"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake1",
2,
0,
0,
[ "@query" ],
0,
"680a69f94e729b6f231f11f86ff7bda1"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake1",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.LoopCombinators.preserves",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake0",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake_fc",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Matrix.matrix", "function_token_typing_Spec.AES.elem",
"int_inversion", "int_typing",
"interpretation_Tm_abs_f17c1a2105556539e599f0b423163342",
"l_and-interp", "l_quant_interp_6af828ec09924ed937a693f4a5a4d34a",
"l_quant_interp_a352609cb648c43dda137c3b8ec4b574",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_45ef578a2fc54b3d2b9707f8bafe038f",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a",
"refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
"refinement_interpretation_Tm_refine_f82b4538c9caa8ab74d4cf6bf5a77d6a",
"token_correspondence_Spec.Frodo.Gen.frodo_gen_matrix_cshake0",
"typing_Lib.ByteSequence.uint_from_bytes_le",
"typing_Lib.IntTypes.v", "typing_Lib.Sequence.sub",
"typing_Spec.AES.gf8", "typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Matrix.mset", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U16@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"d1fa43a1b077af8cbc1d2a696e216359"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake",
1,
0,
0,
[ "@query" ],
0,
"8c5c3b76c033b7679a55c5163973ed1f"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_6e7ade9db1f37c96b082a4321d307f26",
"Lib.LoopCombinators_interpretation_Tm_arrow_c3cac0eaa5a8b41e6eb23c42c4532cc2",
"Spec.Frodo.Gen_interpretation_Tm_arrow_3c4cde532b089bb4b26a9ea12cbb0648",
"Spec.Frodo.Gen_interpretation_Tm_arrow_53a47b5197410448858f209d4d060609",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U16@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.numbytes", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned",
"equation_Lib.LoopCombinators.preserves",
"equation_Lib.LoopCombinators.preserves_predicate",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.l_Forall", "equation_Prims.nat",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake0",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake1",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake_fc",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake_s",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Matrix.matrix", "equation_Spec.Matrix.mget",
"equation_Spec.SHA3.cshake128_frodo",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Spec.Frodo.Gen.frodo_gen_matrix_cshake0",
"function_token_typing_Spec.Frodo.Gen.frodo_gen_matrix_cshake1",
"int_inversion", "int_typing",
"interpretation_Tm_abs_117768405b3269eab5eb1619e555cede",
"interpretation_Tm_abs_f17c1a2105556539e599f0b423163342",
"l_and-interp", "l_quant_interp_60c91dab133fada44d2258e45e098e4b",
"l_quant_interp_6af828ec09924ed937a693f4a5a4d34a",
"l_quant_interp_a352609cb648c43dda137c3b8ec4b574",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_41aef3833b617e5c5b9322c9c48c2c29",
"refinement_interpretation_Tm_refine_45ef578a2fc54b3d2b9707f8bafe038f",
"refinement_interpretation_Tm_refine_460ce49837473aafb58331137146734e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a",
"refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
"refinement_interpretation_Tm_refine_f82b4538c9caa8ab74d4cf6bf5a77d6a",
"token_correspondence_Spec.Frodo.Gen.frodo_gen_matrix_cshake_s",
"typing_Lib.ByteSequence.uint_from_bytes_le",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
"typing_Lib.LoopCombinators.repeati_inductive_",
"typing_Lib.Sequence.sub", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Matrix.matrix", "typing_Spec.Matrix.mset",
"typing_Spec.SHA3.cshake128_frodo",
"typing_Tm_abs_f17c1a2105556539e599f0b423163342",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U16@tok",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"be5b0a5527986af73dffd41e79de168e"
],
[
"Spec.Frodo.Gen.lemma_gen_matrix_4x",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_34eb3b45bf95008028b753bf0c3067f0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_885b88af73f9f6aa39d5ac9d217b273a",
"refinement_interpretation_Tm_refine_9d795d377c76ee8f668c95d4c294c3f4"
],
0,
"4fabe6f9237b044a76b0107ba5af3ee5"
],
[
"Spec.Frodo.Gen.lemma_gen_matrix_4x",
2,
0,
0,
[ "@query" ],
0,
"703081d016c8650fa6d2e6bc616d23a2"
],
[
"Spec.Frodo.Gen.lemma_gen_matrix_4x",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_34eb3b45bf95008028b753bf0c3067f0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_885b88af73f9f6aa39d5ac9d217b273a",
"refinement_interpretation_Tm_refine_9d795d377c76ee8f668c95d4c294c3f4",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"066591f696c5e3fe1f7e231a7dbc9ea5"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9d795d377c76ee8f668c95d4c294c3f4",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a"
],
0,
"37eb6a7446e81f2dfc73213190dee313"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9d795d377c76ee8f668c95d4c294c3f4",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a"
],
0,
"d78e2d835e896b9d6a877c925d786b6a"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9d795d377c76ee8f668c95d4c294c3f4",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"9819ff7da74aa6ef06f66bbff15eb812"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x1",
1,
0,
0,
[ "@query" ],
0,
"c300779ee3bfeec567cdd0fa268bba5a"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x1",
2,
0,
0,
[ "@query" ],
0,
"e1b06253a9620ab979a20b1c97eaacd5"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x1",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.LoopCombinators.preserves",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake_fc",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Matrix.matrix", "equation_Spec.Matrix.mset",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
"int_inversion", "int_typing",
"interpretation_Tm_abs_c28f7644875043e073ae92f55dca14c8",
"l_and-interp", "l_quant_interp_626a241c403f7ec60dbd7e8787c0e225",
"l_quant_interp_7f19df5f1259b51f0d0399e786b05048",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_34eb3b45bf95008028b753bf0c3067f0",
"refinement_interpretation_Tm_refine_45ef578a2fc54b3d2b9707f8bafe038f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_9d795d377c76ee8f668c95d4c294c3f4",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a",
"refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
"refinement_interpretation_Tm_refine_f82b4538c9caa8ab74d4cf6bf5a77d6a",
"typing_Lib.ByteSequence.uint_from_bytes_le",
"typing_Lib.Sequence.sub", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Matrix.mset", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U16@tok"
],
0,
"4bde0011b3ec576e876f2ac46ff17d1c"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x",
1,
0,
0,
[ "@query" ],
0,
"221781f4f3eb8d47d9526b86f9d81139"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_6e7ade9db1f37c96b082a4321d307f26",
"Lib.LoopCombinators_interpretation_Tm_arrow_c3cac0eaa5a8b41e6eb23c42c4532cc2",
"Spec.Frodo.Gen_interpretation_Tm_arrow_53a47b5197410448858f209d4d060609",
"Spec.Frodo.Gen_interpretation_Tm_arrow_70eec9171ca63ab51c1a8f7fc657f00d",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U16@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.numbytes", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned",
"equation_Lib.LoopCombinators.preserves",
"equation_Lib.LoopCombinators.preserves_predicate",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.l_Forall", "equation_Prims.nat",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x1",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x_s",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake_fc",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Matrix.matrix", "equation_Spec.Matrix.mget",
"equation_Spec.Matrix.mset", "equation_Spec.SHA3.cshake128_frodo",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
"function_token_typing_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x1",
"int_inversion", "int_typing",
"interpretation_Tm_abs_c28f7644875043e073ae92f55dca14c8",
"interpretation_Tm_abs_d2ec9847284d8babd708f41a40267d4e",
"l_and-interp", "l_quant_interp_626a241c403f7ec60dbd7e8787c0e225",
"l_quant_interp_7f19df5f1259b51f0d0399e786b05048",
"l_quant_interp_bc3077fb54c3fa4555f2dfd079272404",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_34eb3b45bf95008028b753bf0c3067f0",
"refinement_interpretation_Tm_refine_41aef3833b617e5c5b9322c9c48c2c29",
"refinement_interpretation_Tm_refine_45ef578a2fc54b3d2b9707f8bafe038f",
"refinement_interpretation_Tm_refine_460ce49837473aafb58331137146734e",
"refinement_interpretation_Tm_refine_4822116822fd2cd76140beff9d06b6d5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_885b88af73f9f6aa39d5ac9d217b273a",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d43da8652aa2a76ca42d32e0a308052",
"refinement_interpretation_Tm_refine_9d795d377c76ee8f668c95d4c294c3f4",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a",
"refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
"refinement_interpretation_Tm_refine_f82b4538c9caa8ab74d4cf6bf5a77d6a",
"refinement_interpretation_Tm_refine_f9ac8032e99c32a8e2fc75859e4875ad",
"token_correspondence_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x_s",
"typing_Lib.ByteSequence.uint_from_bytes_le",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
"typing_Lib.LoopCombinators.repeati_inductive_",
"typing_Lib.Sequence.sub", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Matrix.matrix", "typing_Spec.Matrix.mset",
"typing_Spec.SHA3.cshake128_frodo",
"typing_Tm_abs_c28f7644875043e073ae92f55dca14c8",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U16@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"1dc5547edf425c6d37f90d050708ea73"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x_lemma",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "primitive_Prims.op_Division",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_885b88af73f9f6aa39d5ac9d217b273a"
],
0,
"a599814b7c1b0c4cd5e4a67cf4c568b8"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x_lemma",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Lib.LoopCombinators_interpretation_Tm_arrow_6e7ade9db1f37c96b082a4321d307f26",
"Lib.LoopCombinators_interpretation_Tm_arrow_c3cac0eaa5a8b41e6eb23c42c4532cc2",
"Lib.LoopCombinators_interpretation_Tm_arrow_d14b5cd1226e414731f21670beedcc84",
"Lib.LoopCombinators_interpretation_Tm_arrow_e014b42c2cd3786c96d1d8eb3fa6faa7",
"Lib.LoopCombinators_interpretation_Tm_arrow_f77e174321f3ceca78193a141927037b",
"Spec.Frodo.Gen_interpretation_Tm_arrow_5266d3ddd41f233bb130ccea22a0539a",
"Spec.Frodo.Gen_interpretation_Tm_arrow_53a47b5197410448858f209d4d060609",
"Spec.Frodo.Gen_interpretation_Tm_arrow_643e86d8b9902161853422ed207ff6c5",
"Spec.Frodo.Gen_interpretation_Tm_arrow_70eec9171ca63ab51c1a8f7fc657f00d",
"Spec.Frodo.Gen_interpretation_Tm_arrow_a683709933459320ab8f2338926f7bf2",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U16@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.numbytes", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned",
"equation_Lib.LoopCombinators.preserves",
"equation_Lib.LoopCombinators.preserves_predicate",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.l_Forall", "equation_Prims.nat",
"equation_Prims.pos", "equation_Prims.squash",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x1",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x_s",
"equation_Spec.Frodo.Gen.frodo_gen_matrix_cshake_fc",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Matrix.create", "equation_Spec.Matrix.matrix",
"equation_Spec.Matrix.mget", "equation_Spec.Matrix.mset",
"equation_Spec.SHA3.cshake128_frodo",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
"function_token_typing_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x1",
"function_token_typing_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x_s",
"int_inversion", "int_typing",
"interpretation_Tm_abs_c28f7644875043e073ae92f55dca14c8",
"interpretation_Tm_abs_d2ec9847284d8babd708f41a40267d4e",
"l_and-interp", "l_quant_interp_626a241c403f7ec60dbd7e8787c0e225",
"l_quant_interp_7f19df5f1259b51f0d0399e786b05048",
"l_quant_interp_bc3077fb54c3fa4555f2dfd079272404",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_077e52fd302bb9692dad542ec8d3849e",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_34eb3b45bf95008028b753bf0c3067f0",
"refinement_interpretation_Tm_refine_41aef3833b617e5c5b9322c9c48c2c29",
"refinement_interpretation_Tm_refine_460ce49837473aafb58331137146734e",
"refinement_interpretation_Tm_refine_4822116822fd2cd76140beff9d06b6d5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_695fc9bad57438f078f1918065bbd3eb",
"refinement_interpretation_Tm_refine_6a32a668cfa99ccaca30a148b05d66f4",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_885b88af73f9f6aa39d5ac9d217b273a",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d43da8652aa2a76ca42d32e0a308052",
"refinement_interpretation_Tm_refine_9d795d377c76ee8f668c95d4c294c3f4",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a",
"refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
"refinement_interpretation_Tm_refine_f82b4538c9caa8ab74d4cf6bf5a77d6a",
"refinement_interpretation_Tm_refine_f9ac8032e99c32a8e2fc75859e4875ad",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"token_correspondence_Prims.pow2.fuel_instrumented",
"token_correspondence_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
"token_correspondence_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x_s",
"typing_Lib.ByteSequence.uint_from_bytes_le",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
"typing_Lib.LoopCombinators.repeat_gen_inductive",
"typing_Lib.LoopCombinators.repeati_inductive_",
"typing_Lib.Sequence.sub", "typing_Spec.AES.gf8",
"typing_Spec.Frodo.Gen.frodo_gen_matrix_cshake",
"typing_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x",
"typing_Spec.Frodo.Gen.frodo_gen_matrix_cshake_fc",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Matrix.create", "typing_Spec.Matrix.matrix",
"typing_Spec.Matrix.mset", "typing_Spec.SHA3.cshake128_frodo",
"typing_Tm_abs_c28f7644875043e073ae92f55dca14c8",
"typing_Tm_abs_d2ec9847284d8babd708f41a40267d4e",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U16@tok",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"1c1de134c138c343098a8f1d987bb422"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_aes",
1,
0,
0,
[ "@query" ],
0,
"89238ff0ac9b1d618c717c1bebe5806b"
],
[
"Spec.Frodo.Gen.frodo_gen_matrix_aes",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U16@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.numbytes", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "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", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_18ebd8e0ec6c86b3382530d87746c5c8",
"refinement_interpretation_Tm_refine_26d768cc241c6628db9e0d45d45d9136",
"refinement_interpretation_Tm_refine_3a9b5cf7d7cfe6b786ef97b48b07fc55",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5bb74aac50077bcd5aded404ff6ae1fd",
"refinement_interpretation_Tm_refine_81e672b1db343a35cc3b58b93c1f29b9",
"refinement_interpretation_Tm_refine_b4a38ef4372fc2a93e98b6af980e1854",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"3731eff40e59f15c3513c255db7b88c5"
]
]
]
Computing file changes ...
