Revision 0d9153dc34ee2dcf0821e3f21e825fc5bb8895b4 authored by Santiago Zanella-Beguelin on 11 December 2019, 17:46:08 UTC, committed by Santiago Zanella-Beguelin on 12 December 2019, 10:33:01 UTC
1 parent 7405f78
Hacl.Impl.Frodo.Gen.fst.hints
[
"B>�\u0003zd}�\u0013�\u0014U�\u000f��",
[
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"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.unsigned",
"equation_Lib.IntTypes.v", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_typing", "lemma_Lib.IntTypes.mul_lemma",
"lemma_Lib.IntTypes.v_mk_int", "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_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_a6ee845210d1551d5d919623eeb737fd",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"46360b706aee6e08738591633d6f34b6"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake0",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"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.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "int_typing",
"lemma_Lib.IntTypes.v_mk_int", "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_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_a6ee845210d1551d5d919623eeb737fd",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.v", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"4eb3e0263ff52a365e908db5519b6e57"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake0",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U1",
"disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@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_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.lbytes", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.gsub",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder", "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.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Spec.AES.elem", "int_typing",
"lemma_Lib.IntTypes.mul_lemma",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"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_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_87f84014e78fea04ea8eec4fd7c636b6",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_a6ee845210d1551d5d919623eeb737fd",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_b631d18189656cc71916a40ddaf3e927",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v",
"typing_Lib.Sequence.sub", "typing_LowStar.Buffer.trivial_preorder",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"16f24154521019c6d2da1e2fab6f0488"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake1",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"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.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_a6ee845210d1551d5d919623eeb737fd",
"refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"186629a352fa4e26fb109609df4f7d1e"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake1",
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.S128", "disc_equation_Lib.IntTypes.U128",
"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.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_a6ee845210d1551d5d919623eeb737fd",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.v", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"17d57445c7bccd19aec6a24843274733"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake1",
3,
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",
"b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.SEC",
"disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"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.U64@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.lbytes",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.loop1_inv", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies1", "equation_Lib.Buffer.modifies2",
"equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint16",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.LoopCombinators.preserves",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length",
"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.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Matrix.matrix", "equation_Spec.SHA3.cshake128_frodo",
"function_token_typing_Lib.IntTypes.uint16",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Spec.Frodo.Gen.frodo_gen_matrix_cshake0",
"int_inversion", "int_typing",
"interpretation_Tm_abs_c8ea66a0dfe76dc76fa171149768a73c",
"interpretation_Tm_abs_f17c1a2105556539e599f0b423163342",
"l_and-interp", "l_quant_interp_6af828ec09924ed937a693f4a5a4d34a",
"l_quant_interp_a352609cb648c43dda137c3b8ec4b574",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
"lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mul_lemma",
"lemma_Lib.IntTypes.v_injective",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "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_0ad1594897a9127488ed7f1941a638e0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_2fa5537f636f3c1341e54801e3385c12",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_41aef3833b617e5c5b9322c9c48c2c29",
"refinement_interpretation_Tm_refine_427964005be28d37845727035e1dec26",
"refinement_interpretation_Tm_refine_460ce49837473aafb58331137146734e",
"refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7",
"refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_87f84014e78fea04ea8eec4fd7c636b6",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_a6ee845210d1551d5d919623eeb737fd",
"refinement_interpretation_Tm_refine_ad6f0d16c64df07f385c85c38367b535",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c9bc0d356497c4410690756d581b4ff2",
"refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
"refinement_interpretation_Tm_refine_f82b4538c9caa8ab74d4cf6bf5a77d6a",
"token_correspondence_Spec.Frodo.Gen.frodo_gen_matrix_cshake0",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length",
"typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar",
"typing_Lib.ByteSequence.uint_from_bytes_le",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.cast",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.mul",
"typing_Lib.IntTypes.op_At_Percent_Dot", "typing_Lib.IntTypes.v",
"typing_Lib.LoopCombinators.repeati_inductive_",
"typing_Lib.Sequence.lseq", "typing_Lib.Sequence.sub",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Matrix.mset", "typing_Spec.SHA3.cshake128_frodo",
"typing_Tm_abs_f17c1a2105556539e599f0b423163342",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U16@tok",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok"
],
0,
"962e0aac5d36aa2eb90efa2134cbe6b4"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_c13b644bab5aff5eb362bcfb396fb897",
"refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"7ae516db892ba707164ac52eaaf64beb"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake",
2,
0,
0,
[ "@query" ],
0,
"284e14063a97fa8098c258740c6e34b0"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Hacl.Impl.Frodo.Gen_interpretation_Tm_arrow_b6205b2e6d5fc4e08c155f0554d72d9c",
"Hacl.Impl.Frodo.Gen_interpretation_Tm_ghost_arrow_c1436a2e895ece7aa2122e63b467cf00",
"Lib.Buffer_interpretation_Tm_arrow_db3df7e9d023fa77f76f424ac2724764",
"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_1d401b2b8cb46084c94c0130192ab448",
"Spec.Frodo.Gen_interpretation_Tm_arrow_3c4cde532b089bb4b26a9ea12cbb0648",
"Spec.Frodo.Gen_interpretation_Tm_arrow_53a47b5197410448858f209d4d060609",
"Spec.Frodo.Gen_interpretation_Tm_arrow_721ae6c1516525a5380734a8206c89d3",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U1",
"disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"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_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.lbytes",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.loop_inv",
"equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
"equation_Lib.Buffer.modifies2",
"equation_Lib.Buffer.op_Bar_Plus_Bar",
"equation_Lib.Buffer.stack_allocated", "equation_Lib.Buffer.union",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.LoopCombinators.preserves",
"equation_Lib.LoopCombinators.preserves_predicate",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"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",
"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.create", "equation_Spec.Matrix.matrix",
"equation_Spec.SHA3.cshake128_frodo",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"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",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_117768405b3269eab5eb1619e555cede",
"interpretation_Tm_abs_5660c7c6b4d80856bd19aff1b0378a81",
"interpretation_Tm_abs_d887293d202df2d160b340fec83e8638",
"interpretation_Tm_abs_da6ec1348e18a0ac12af92ffe6708f05",
"interpretation_Tm_abs_f17c1a2105556539e599f0b423163342",
"l_and-interp", "l_quant_interp_60c91dab133fada44d2258e45e098e4b",
"l_quant_interp_6af828ec09924ed937a693f4a5a4d34a",
"l_quant_interp_a352609cb648c43dda137c3b8ec4b574",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.IntTypes.mul_lemma", "lemma_Lib.IntTypes.sub_lemma",
"lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int",
"lemma_Lib.Sequence.eq_elim",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Negation",
"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_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0ad1594897a9127488ed7f1941a638e0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2",
"refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605",
"refinement_interpretation_Tm_refine_1de8426f4795d59a42df9b22a452f23d",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_365abba901205a01d0ef28ebf2198c47",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_41aef3833b617e5c5b9322c9c48c2c29",
"refinement_interpretation_Tm_refine_427964005be28d37845727035e1dec26",
"refinement_interpretation_Tm_refine_460ce49837473aafb58331137146734e",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6631a36076361ce63441cef502d89699",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_695fc9bad57438f078f1918065bbd3eb",
"refinement_interpretation_Tm_refine_6a32a668cfa99ccaca30a148b05d66f4",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_873133828c907cbc2718aea6e8b831ae",
"refinement_interpretation_Tm_refine_8b40f4ba53055527eadf55a24b95d6ac",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
"refinement_interpretation_Tm_refine_be316ceec231ab35ef3ab6a2c3af1264",
"refinement_interpretation_Tm_refine_c13b644bab5aff5eb362bcfb396fb897",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e",
"refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e9c32a5fb00a4e8c339597118c871180",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f2cf336029ef2bddc10058d5bbede845",
"refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
"refinement_interpretation_Tm_refine_f82b4538c9caa8ab74d4cf6bf5a77d6a",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Spec.Frodo.Gen.frodo_gen_matrix_cshake0",
"token_correspondence_Spec.Frodo.Gen.frodo_gen_matrix_cshake_s",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.as_seq",
"typing_Lib.Buffer.gsub", "typing_Lib.Buffer.length",
"typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar",
"typing_Lib.ByteSequence.uint_from_bytes_le",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.sub",
"typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v",
"typing_Lib.LoopCombinators.repeat_gen_inductive",
"typing_Lib.LoopCombinators.repeati_inductive_",
"typing_Lib.Sequence.create", "typing_Lib.Sequence.lseq",
"typing_Lib.Sequence.sub", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.as_seq",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_LowStar.Monotonic.Buffer.mgsub", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred",
"typing_Spec.Frodo.Gen.frodo_gen_matrix_cshake_fc",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Matrix.create", "typing_Spec.Matrix.mset",
"typing_Spec.SHA3.cshake128_frodo",
"typing_Tm_abs_117768405b3269eab5eb1619e555cede",
"typing_Tm_abs_f17c1a2105556539e599f0b423163342",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"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,
"db9a2eef0e3adc118fd090653519bda3"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"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.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.lseq", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf", "int_typing",
"lemma_Lib.IntTypes.mul_lemma", "lemma_Lib.IntTypes.v_mk_int",
"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_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_a6ee845210d1551d5d919623eeb737fd",
"refinement_interpretation_Tm_refine_aea8c00d95c473fd0c9db37d35c829ae",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"69ff4a8390703ff91164979a0399a171"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"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.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "int_typing",
"lemma_Lib.IntTypes.v_mk_int", "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_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_a6ee845210d1551d5d919623eeb737fd",
"refinement_interpretation_Tm_refine_aea8c00d95c473fd0c9db37d35c829ae",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.v", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"066eace5758b37990d9b769dc48b31d5"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U1",
"disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@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_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.lbytes",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.gsub",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint16",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "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.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.uint16",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Spec.AES.elem", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.UInt32.uv_inv", "lemma_Lib.IntTypes.add_lemma",
"lemma_Lib.IntTypes.mul_lemma",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"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_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_a6ee845210d1551d5d919623eeb737fd",
"refinement_interpretation_Tm_refine_aea8c00d95c473fd0c9db37d35c829ae",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_b631d18189656cc71916a40ddaf3e927",
"refinement_interpretation_Tm_refine_c8eb59af2023712c07cc9396c8a6e1bd",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a",
"typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length",
"typing_Lib.Buffer.loc", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v",
"typing_Lib.Sequence.sub", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"474f023e35d4f043861b2387acad77b3"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake_4x1",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.PUB@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.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_a6ee845210d1551d5d919623eeb737fd",
"refinement_interpretation_Tm_refine_aea8c00d95c473fd0c9db37d35c829ae",
"refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U16@tok",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"fb627c1426ab4b8a99d5c262e898c95c"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake_4x1",
2,
0,
1,
[
"@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.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.PUB@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.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "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_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_a6ee845210d1551d5d919623eeb737fd",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U16@tok",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"bb53894ca428042f32e2efffbbe15619"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake_4x1",
3,
0,
1,
[
"@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",
"b2t_def", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.SEC",
"disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"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_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.lbytes",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.loop1_inv",
"equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
"equation_Lib.Buffer.modifies2",
"equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint16",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.LoopCombinators.preserves",
"equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length",
"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_fc",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Matrix.matrix", "equation_Spec.Matrix.mset",
"function_token_typing_Lib.IntTypes.uint16",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
"int_inversion", "int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"interpretation_Tm_abs_c28f7644875043e073ae92f55dca14c8",
"interpretation_Tm_abs_ef713836ba6db969935c25097ba4745c",
"l_and-interp", "l_quant_interp_626a241c403f7ec60dbd7e8787c0e225",
"l_quant_interp_7f19df5f1259b51f0d0399e786b05048",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
"lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.mul_lemma",
"lemma_Lib.IntTypes.v_injective", "lemma_Lib.IntTypes.v_mk_int",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"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_0ad1594897a9127488ed7f1941a638e0",
"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_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_3a37686bc3924efd748359da8c3fd202",
"refinement_interpretation_Tm_refine_3ef073281006f924f581a1e02d71a460",
"refinement_interpretation_Tm_refine_41aef3833b617e5c5b9322c9c48c2c29",
"refinement_interpretation_Tm_refine_427964005be28d37845727035e1dec26",
"refinement_interpretation_Tm_refine_4c82af8a46684f75d7fe12f75a0fb1a7",
"refinement_interpretation_Tm_refine_4d001fd32727920cd89f6a1e407fed3c",
"refinement_interpretation_Tm_refine_4f1cffa40412af126565457cc49b8cca",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_55ad6dde98f777fb8caf2adfada0d12e",
"refinement_interpretation_Tm_refine_66c713d37a6ed16eecfe1cdd673d1bf2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d795d377c76ee8f668c95d4c294c3f4",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_a5ac8e676229126926ab9c2d14ba1e90",
"refinement_interpretation_Tm_refine_a636b6491af501737c1eb06142217342",
"refinement_interpretation_Tm_refine_a6ee845210d1551d5d919623eeb737fd",
"refinement_interpretation_Tm_refine_a7681d5b86e6d39f33b9404ba40577ca",
"refinement_interpretation_Tm_refine_aea8c00d95c473fd0c9db37d35c829ae",
"refinement_interpretation_Tm_refine_b24c07c733bd26eae76e4fc1be68b79a",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_b8224c6c43e6e9f067a2437fa08acf99",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c3b2720f5a8667a73a16236a191e4010",
"refinement_interpretation_Tm_refine_c8eb59af2023712c07cc9396c8a6e1bd",
"refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
"refinement_interpretation_Tm_refine_f82b4538c9caa8ab74d4cf6bf5a77d6a",
"refinement_interpretation_Tm_refine_f8a2ab8862e52be2955c006e53fa3262",
"token_correspondence_Spec.Frodo.Gen.frodo_gen_matrix_cshake_4x0",
"true_interp", "typing_FStar.UInt32.v", "typing_Lib.Buffer.as_seq",
"typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
"typing_Lib.Buffer.op_Bar_Plus_Bar",
"typing_Lib.ByteSequence.uint_from_bytes_le",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.cast",
"typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.mul", "typing_Lib.IntTypes.op_At_Percent_Dot",
"typing_Lib.IntTypes.v",
"typing_Lib.LoopCombinators.repeati_inductive_",
"typing_Lib.Sequence.lseq", "typing_Lib.Sequence.sub",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Matrix.mset",
"typing_Tm_abs_c28f7644875043e073ae92f55dca14c8",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"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,
"6e2c18ba11b379d6a589677b32cc884e"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake_4x",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_30843da15c0f6e06dfd927cae8ed1ec8",
"refinement_interpretation_Tm_refine_6c9bddef1da919143345ce11c5e4abc9",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"6a8b722b74a4fe4f00204aeb0a5922df"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake_4x",
2,
1,
0,
[ "@query" ],
0,
"50721d6bab2ec67ab790292bb1795ac3"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_cshake_4x",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"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_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Int.op_Slash",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.lbytes",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.loop_inv",
"equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
"equation_Lib.Buffer.modifies2",
"equation_Lib.Buffer.op_Bar_Plus_Bar",
"equation_Lib.Buffer.stack_allocated", "equation_Lib.Buffer.union",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint16",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.abs",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf", "equation_Spec.Matrix.create",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"function_token_typing_Spec.AES.elem",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_2bd8614f1e834c79c58b9dbb4f341556",
"interpretation_Tm_abs_da6ec1348e18a0ac12af92ffe6708f05",
"interpretation_Tm_abs_fd3040415cb26c51efb16ad2ca4dd9ef",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.div_lemma", "lemma_Lib.IntTypes.mul_lemma",
"lemma_Lib.IntTypes.sub_lemma", "lemma_Lib.IntTypes.v_injective",
"lemma_Lib.IntTypes.v_mk_int", "lemma_Lib.Sequence.eq_elim",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.as_seq_gsub",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Negation",
"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_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_08086ebcab842d6522b1055177e23e81",
"refinement_interpretation_Tm_refine_0ad1594897a9127488ed7f1941a638e0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_156c49afb7e1e070fbb2e47dc0e3d4b2",
"refinement_interpretation_Tm_refine_1cc58e901e83e96dff5b4d1682343605",
"refinement_interpretation_Tm_refine_30843da15c0f6e06dfd927cae8ed1ec8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6c9bddef1da919143345ce11c5e4abc9",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_873133828c907cbc2718aea6e8b831ae",
"refinement_interpretation_Tm_refine_8b40f4ba53055527eadf55a24b95d6ac",
"refinement_interpretation_Tm_refine_8c5a12e9ae1414fb80937568ed475b6e",
"refinement_interpretation_Tm_refine_938daf4d3bd0bee39bfa48ffd969c411",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c6c18a7ceb46d419c35ff8551117551e",
"refinement_interpretation_Tm_refine_cfc41488cee641ca406ae764563b3947",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e1a4524ac2326cd718361637d55193c4",
"refinement_interpretation_Tm_refine_e450d0eda8ec6ce5c9eff42d01f0e81a",
"refinement_interpretation_Tm_refine_e9c32a5fb00a4e8c339597118c871180",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f2cf336029ef2bddc10058d5bbede845",
"refinement_interpretation_Tm_refine_f9a9908453039a29d1137446e7a649e5",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.gsub",
"typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
"typing_Lib.Buffer.op_Bar_Plus_Bar", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.sub",
"typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v",
"typing_Lib.Sequence.create", "typing_Lib.Sequence.sub",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_LowStar.Monotonic.Buffer.mgsub", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"805e67d0f763b8def6c69085880568ca"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_aes",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"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.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_cc28cda10485ad4c030ed99817830903",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_ff84d4adf0dc27bf22f93381b0719b0f",
"typing_Lib.IntTypes.v", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"4e0fe09e46314414b58a3722ee56817b"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_aes",
2,
0,
0,
[ "@query" ],
0,
"134b6daf6657eb1387949fa0b903ea5e"
],
[
"Hacl.Impl.Frodo.Gen.frodo_gen_matrix_aes",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"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_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Int.op_Slash",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Impl.Matrix.elem",
"equation_Hacl.Impl.Matrix.lbytes",
"equation_Hacl.Impl.Matrix.matrix_t", "equation_Lib.Buffer.as_seq",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies1",
"equation_Lib.Buffer.stack_allocated", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint16", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"equation_Lib.Sequence.seq", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.abs",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint16",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.int",
"function_token_typing_Spec.AES.elem",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.uv_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.div_lemma",
"lemma_Lib.IntTypes.mul_lemma",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.len_gsub",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Negation",
"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_0581b08fc69f9bad1f5e0160becc0e60",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_1de8426f4795d59a42df9b22a452f23d",
"refinement_interpretation_Tm_refine_249c5787f62288294e5c378fe3f0f289",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_4db2239783e805889c416970298d9e32",
"refinement_interpretation_Tm_refine_4de30c21f08f15ac84dc8946ab8669e3",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_b631d18189656cc71916a40ddaf3e927",
"refinement_interpretation_Tm_refine_cc28cda10485ad4c030ed99817830903",
"refinement_interpretation_Tm_refine_d9dd5cefc7c9ff355a8ef112d8c45598",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e450d0eda8ec6ce5c9eff42d01f0e81a",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a",
"refinement_interpretation_Tm_refine_ff84d4adf0dc27bf22f93381b0719b0f",
"refinement_kinding_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.length",
"typing_Lib.Buffer.loc", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.unsigned", "typing_Lib.IntTypes.v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"fd13f88612c5bb7807fdfe0fc5b57eb4"
]
]
]
Computing file changes ...
