[ "àýûq\u0011¶žåã\u001cW¿Hý\u0012›", [ [ "Hacl.Frodo640.crypto_bytes", 1, 0, 0, [ "@query", "constructor_distinct_Lib.IntTypes.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U32", "equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned", "projection_inverse_BoxInt_proj_0" ], 0, "89a226c9d4bdc00c261679c4abd4ff4d" ], [ "Hacl.Frodo640.crypto_publickeybytes", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "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.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Frodo.Params.Frodo640", "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", "equality_tok_Spec.Frodo.Params.Frodo640@tok", "equation_FStar.Int.op_Slash", "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.Frodo.Params.bytes_seed_a", "equation_Hacl.Impl.Frodo.Params.crypto_publickeybytes", "equation_Hacl.Impl.Frodo.Params.params_logq", "equation_Hacl.Impl.Frodo.Params.params_n", "equation_Hacl.Impl.Frodo.Params.params_nbar", "equation_Hacl.Impl.Frodo.Params.publicmatrixbytes_len", "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.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.abs", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Frodo.Params.bytes_seed_a", "equation_Spec.Frodo.Params.crypto_publickeybytes", "equation_Spec.Frodo.Params.params_logq", "equation_Spec.Frodo.Params.params_n", "equation_Spec.Frodo.Params.params_nbar", "equation_Spec.Frodo.Params.publicmatrixbytes_len", "equation_Spec.GaloisField.gf", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.div_lemma", "lemma_Lib.IntTypes.mul_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Division", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "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_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86", "refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1", "refinement_interpretation_Tm_refine_d35c718b60e62e3f5c441bc01ea41a19", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e450d0eda8ec6ce5c9eff42d01f0e81a", "refinement_interpretation_Tm_refine_e91898aa1381266415975b8ad0f9dcea", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Hacl.Impl.Frodo.Params.bytes_seed_a", "typing_Hacl.Impl.Frodo.Params.crypto_publickeybytes", "typing_Hacl.Impl.Frodo.Params.params_logq", "typing_Hacl.Impl.Frodo.Params.params_n", "typing_Hacl.Impl.Frodo.Params.params_nbar", "typing_Hacl.Impl.Frodo.Params.publicmatrixbytes_len", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.div", "typing_Lib.IntTypes.mul", "typing_Lib.IntTypes.v", "typing_Spec.AES.gf8", "typing_Spec.Frodo.Params.crypto_publickeybytes", "typing_Spec.Frodo.Params.publicmatrixbytes_len", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Frodo.Params.Frodo640@tok" ], 0, "21f00d0117967415bf6617caa303be1f" ], [ "Hacl.Frodo640.crypto_secretkeybytes", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "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.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Frodo.Params.Frodo640", "disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128", "equality_tok_Lib.IntTypes.PUB@tok", "equality_tok_Lib.IntTypes.SEC@tok", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Frodo.Params.Frodo640@tok", "equation_FStar.Int.op_Slash", "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.Frodo.Params.bytes_pkhash", "equation_Hacl.Impl.Frodo.Params.bytes_seed_a", "equation_Hacl.Impl.Frodo.Params.crypto_bytes", "equation_Hacl.Impl.Frodo.Params.crypto_publickeybytes", "equation_Hacl.Impl.Frodo.Params.crypto_secretkeybytes", "equation_Hacl.Impl.Frodo.Params.params_logq", "equation_Hacl.Impl.Frodo.Params.params_n", "equation_Hacl.Impl.Frodo.Params.params_nbar", "equation_Hacl.Impl.Frodo.Params.publicmatrixbytes_len", "equation_Hacl.Impl.Frodo.Params.secretmatrixbytes_len", "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.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.abs", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Frodo.Params.bytes_pkhash", "equation_Spec.Frodo.Params.bytes_seed_a", "equation_Spec.Frodo.Params.crypto_bytes", "equation_Spec.Frodo.Params.crypto_publickeybytes", "equation_Spec.Frodo.Params.crypto_secretkeybytes", "equation_Spec.Frodo.Params.params_logq", "equation_Spec.Frodo.Params.params_n", "equation_Spec.Frodo.Params.params_nbar", "equation_Spec.Frodo.Params.publicmatrixbytes_len", "equation_Spec.Frodo.Params.secretmatrixbytes_len", "equation_Spec.GaloisField.gf", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.div_lemma", "lemma_Lib.IntTypes.mul_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Division", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "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_0ea1fba779ad5718e28476faeef94d56", "refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b", "refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86", "refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1", "refinement_interpretation_Tm_refine_d35c718b60e62e3f5c441bc01ea41a19", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e450d0eda8ec6ce5c9eff42d01f0e81a", "refinement_interpretation_Tm_refine_e91898aa1381266415975b8ad0f9dcea", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_f6ad5779fa2c329550b481a622c9645c", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_Hacl.Impl.Frodo.Params.bytes_seed_a", "typing_Hacl.Impl.Frodo.Params.crypto_bytes", "typing_Hacl.Impl.Frodo.Params.crypto_publickeybytes", "typing_Hacl.Impl.Frodo.Params.crypto_secretkeybytes", "typing_Hacl.Impl.Frodo.Params.params_logq", "typing_Hacl.Impl.Frodo.Params.params_n", "typing_Hacl.Impl.Frodo.Params.params_nbar", "typing_Hacl.Impl.Frodo.Params.publicmatrixbytes_len", "typing_Hacl.Impl.Frodo.Params.secretmatrixbytes_len", "typing_Lib.IntTypes.add", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.div", "typing_Lib.IntTypes.mul", "typing_Lib.IntTypes.v", "typing_Spec.AES.gf8", "typing_Spec.AES.irred", "typing_Spec.Frodo.Params.crypto_publickeybytes", "typing_Spec.Frodo.Params.crypto_secretkeybytes", "typing_Spec.Frodo.Params.secretmatrixbytes_len", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Frodo.Params.Frodo640@tok" ], 0, "72780fe4cf43479b1347ae933ad01e94" ], [ "Hacl.Frodo640.crypto_ciphertextbytes", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "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.S16", "constructor_distinct_Lib.IntTypes.S8", "constructor_distinct_Lib.IntTypes.U1", "constructor_distinct_Lib.IntTypes.U128", "constructor_distinct_Lib.IntTypes.U32", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Frodo.Params.Frodo640", "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", "equality_tok_Spec.Frodo.Params.Frodo640@tok", "equation_FStar.Int.op_Slash", "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.Frodo.Params.crypto_ciphertextbytes", "equation_Hacl.Impl.Frodo.Params.ct1bytes_len", "equation_Hacl.Impl.Frodo.Params.ct2bytes_len", "equation_Hacl.Impl.Frodo.Params.params_logq", "equation_Hacl.Impl.Frodo.Params.params_n", "equation_Hacl.Impl.Frodo.Params.params_nbar", "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.unsigned", "equation_Lib.IntTypes.v", "equation_Prims.abs", "equation_Prims.nat", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.Frodo.Params.crypto_ciphertextbytes", "equation_Spec.Frodo.Params.ct1bytes_len", "equation_Spec.Frodo.Params.ct2bytes_len", "equation_Spec.Frodo.Params.params_logq", "equation_Spec.Frodo.Params.params_n", "equation_Spec.Frodo.Params.params_nbar", "equation_Spec.GaloisField.gf", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_lemma", "lemma_Lib.IntTypes.div_lemma", "lemma_Lib.IntTypes.mul_lemma", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Division", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "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_44540322a5aeeac77ad2eb12638c2b4f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86", "refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1", "refinement_interpretation_Tm_refine_d35c718b60e62e3f5c441bc01ea41a19", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "refinement_interpretation_Tm_refine_e450d0eda8ec6ce5c9eff42d01f0e81a", "refinement_interpretation_Tm_refine_e91898aa1381266415975b8ad0f9dcea", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "refinement_interpretation_Tm_refine_feb9bb9f35b4e580b5c2b388310d192a", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_Hacl.Impl.Frodo.Params.crypto_ciphertextbytes", "typing_Hacl.Impl.Frodo.Params.ct1bytes_len", "typing_Hacl.Impl.Frodo.Params.ct2bytes_len", "typing_Hacl.Impl.Frodo.Params.params_logq", "typing_Hacl.Impl.Frodo.Params.params_n", "typing_Hacl.Impl.Frodo.Params.params_nbar", "typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.div", "typing_Lib.IntTypes.mul", "typing_Spec.AES.gf8", "typing_Spec.Frodo.Params.crypto_ciphertextbytes", "typing_Spec.Frodo.Params.ct1bytes_len", "typing_Spec.Frodo.Params.ct2bytes_len", "typing_Spec.GaloisField.__proj__GF__item__t", "typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok", "typing_tok_Spec.Frodo.Params.Frodo640@tok" ], 0, "525b49f17a7eeafddf601b921a79780c" ], [ "Hacl.Frodo640.crypto_kem_keypair", 1, 0, 0, [ "@query", "constructor_distinct_Spec.Frodo.Params.SHAKE128", "equality_tok_Spec.Frodo.Params.SHAKE128@tok", "equation_Hacl.Impl.Frodo.Params.is_supported", "projection_inverse_BoxBool_proj_0" ], 0, "9a8c62406652c6aa3d5b9362f9119359" ], [ "Hacl.Frodo640.crypto_kem_keypair", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Frodo.Params.SHAKE128", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Frodo.Params.SHAKE128@tok", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_Hacl.Impl.Frodo.Params.is_supported", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_FStar.Monotonic.Heap.heap", "lemma_FStar.Map.lemma_ContainsDom", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "f8fbf4aa7541d8c4d8aa3fb3ebcecee3" ], [ "Hacl.Frodo640.crypto_kem_enc", 1, 0, 0, [ "@query", "constructor_distinct_Spec.Frodo.Params.SHAKE128", "equality_tok_Spec.Frodo.Params.SHAKE128@tok", "equation_Hacl.Impl.Frodo.Params.is_supported", "projection_inverse_BoxBool_proj_0" ], 0, "15b29ae4dbc90bb1e7e35b61ab1c1b95" ], [ "Hacl.Frodo640.crypto_kem_enc", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Frodo.Params.SHAKE128", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Frodo.Params.SHAKE128@tok", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_Hacl.Impl.Frodo.Params.is_supported", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_FStar.Monotonic.Heap.heap", "lemma_FStar.Map.lemma_ContainsDom", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "1086cce4516ae4d1f1053e350a292353" ], [ "Hacl.Frodo640.crypto_kem_dec", 1, 0, 0, [ "@query", "constructor_distinct_Spec.Frodo.Params.SHAKE128", "equality_tok_Spec.Frodo.Params.SHAKE128@tok", "equation_Hacl.Impl.Frodo.Params.is_supported", "projection_inverse_BoxBool_proj_0" ], 0, "1f2ad42b0219ea9302ffe17c83d33148" ], [ "Hacl.Frodo640.crypto_kem_dec", 2, 0, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Lib.IntTypes.U8", "constructor_distinct_Spec.Frodo.Params.SHAKE128", "equality_tok_Lib.IntTypes.U1@tok", "equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Spec.Frodo.Params.SHAKE128@tok", "equation_FStar.Monotonic.HyperHeap.hmap", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip", "equation_FStar.Monotonic.HyperStack.mem", "equation_Hacl.Impl.Frodo.Params.is_supported", "equation_Lib.IntTypes.unsigned", "equation_Spec.AES.gf8", "equation_Spec.AES.irred", "equation_Spec.GaloisField.gf", "function_token_typing_FStar.Monotonic.Heap.heap", "lemma_FStar.Map.lemma_ContainsDom", "proj_equation_Spec.GaloisField.GF_t", "projection_inverse_Spec.GaloisField.GF_t", "refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a", "refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid", "typing_FStar.Monotonic.HyperStack.get_hmap", "typing_FStar.Monotonic.HyperStack.get_tip", "typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t" ], 0, "79e55df62456d103385a719d5e2c6a90" ] ] ]