[
  "\u0017\u0016Ò!°»%;~œ!ÑPá\u001c†",
  [
    [
      "Hacl.Frodo64.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,
      "55d5b5527da9e087b1b489359de52aa9"
    ],
    [
      "Hacl.Frodo64.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.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S128",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Frodo.Params.Frodo64",
        "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.Frodo64@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.Frodo64@tok"
      ],
      0,
      "eed4fc9fd5682b197c872bdc0e13d74a"
    ],
    [
      "Hacl.Frodo64.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.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S128",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Frodo.Params.Frodo64",
        "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.Frodo64@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_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_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.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.Frodo64@tok"
      ],
      0,
      "bde59ab034fdded8897fee934912177b"
    ],
    [
      "Hacl.Frodo64.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.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S128",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U128",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Frodo.Params.Frodo64",
        "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.Frodo64@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",
        "lemma_Lib.IntTypes.v_injective", "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_Modulus", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_2a039e1a99d9d2644dcc4f59d4a41871",
        "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.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_Lib.IntTypes.v",
        "typing_Spec.AES.gf8",
        "typing_Spec.Frodo.Params.crypto_ciphertextbytes",
        "typing_Spec.Frodo.Params.ct1bytes_len",
        "typing_Spec.Frodo.Params.params_n",
        "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.Frodo64@tok"
      ],
      0,
      "c1736eb186fa0dfda6cd3a51bff003a8"
    ],
    [
      "Hacl.Frodo64.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,
      "2873efa65aacf9e0add45f8ed347d351"
    ],
    [
      "Hacl.Frodo64.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,
      "d2119ef9860978b11dc8f57343f93a58"
    ],
    [
      "Hacl.Frodo64.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,
      "47610508b4c84ddbabb676171b24ee41"
    ],
    [
      "Hacl.Frodo64.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,
      "6fe386fa41f7f016f1731d060c10110d"
    ],
    [
      "Hacl.Frodo64.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,
      "4d4effd1a36ced7350974bcb9deb57cd"
    ],
    [
      "Hacl.Frodo64.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,
      "99851da91ae800fbb24182f02abd03a8"
    ]
  ]
]