[
  "���!���w|z�Hu5\n�",
  [
    [
      "Hacl.Frodo.KEM.crypto_kem_keypair",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_Hacl.Impl.Frodo.KEM.crypto_publickeybytes",
        "equation_Hacl.Impl.Frodo.KEM.crypto_secretkeybytes",
        "equation_Prims.nat",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_4217a417164cd9f176884ac8e9b5b15e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_69549b60200c25e52f3ec15580491456",
        "typing_Hacl.Impl.Frodo.KEM.crypto_publickeybytes",
        "typing_Hacl.Impl.Frodo.KEM.crypto_secretkeybytes",
        "typing_Spec.Frodo.Params.crypto_publickeybytes"
      ],
      0,
      "a1b4126e9f10a47548c407a30de82286"
    ],
    [
      "Hacl.Frodo.KEM.crypto_kem_keypair",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equation_Lib.Buffer.as_seq",
        "equation_Spec.Frodo.KEM.crypto_kem_keypair",
        "refinement_interpretation_Tm_refine_148a9e4bd44d8685602f741e69eaf8b6",
        "refinement_interpretation_Tm_refine_bac3d0e24bb03b02d8e9b1701ecb7798"
      ],
      0,
      "8d4120728fd967450cb4f40d31afa8ce"
    ],
    [
      "Hacl.Frodo.KEM.crypto_kem_enc",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Impl.Frodo.KEM.crypto_ciphertextbytes",
        "equation_Hacl.Impl.Frodo.KEM.crypto_publickeybytes",
        "equation_Hacl.Impl.Matrix.lbytes", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.AES.elem", "equation_Spec.AES.gf8",
        "equation_Spec.AES.irred", "equation_Spec.Frodo.Params.bytes_seed_a",
        "equation_Spec.Frodo.Params.crypto_bytes",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "function_token_typing_Spec.AES.elem",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_68ee6d2c8678eb431259a3d4f412550b",
        "refinement_interpretation_Tm_refine_69549b60200c25e52f3ec15580491456",
        "refinement_interpretation_Tm_refine_8456759e660370b6e428c86ad6758869",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "typing_Hacl.Impl.Frodo.KEM.crypto_ciphertextbytes",
        "typing_Hacl.Impl.Frodo.KEM.crypto_publickeybytes",
        "typing_Lib.Buffer.length", "typing_Spec.Frodo.Params.bytes_seed_a",
        "typing_Spec.Frodo.Params.crypto_ciphertextbytes",
        "typing_tok_Lib.Buffer.MUT@tok"
      ],
      0,
      "e48e268a7f11c21d3ccef8af772ed885"
    ],
    [
      "Hacl.Frodo.KEM.crypto_kem_enc",
      2,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equation_Lib.Buffer.as_seq",
        "equation_Spec.Frodo.KEM.crypto_kem_enc",
        "refinement_interpretation_Tm_refine_da64859381eb6be468ffc65716ff1ca4",
        "refinement_interpretation_Tm_refine_f1cfbbcf1c55d03ed8d5565aa798aa5d"
      ],
      0,
      "42341b542cc78e31e1cf4948c7c04332"
    ],
    [
      "Hacl.Frodo.KEM.crypto_kem_dec",
      1,
      0,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Lib.IntTypes.U8@tok",
        "equation_Hacl.Impl.Frodo.KEM.crypto_ciphertextbytes",
        "equation_Hacl.Impl.Frodo.KEM.crypto_secretkeybytes",
        "equation_Hacl.Impl.Matrix.lbytes", "equation_Lib.Buffer.lbuffer_t",
        "equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.range",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Spec.AES.elem",
        "equation_Spec.AES.gf8", "equation_Spec.AES.irred",
        "equation_Spec.Frodo.Params.crypto_bytes",
        "equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
        "function_token_typing_Spec.AES.elem",
        "proj_equation_Spec.GaloisField.GF_t",
        "projection_inverse_Spec.GaloisField.GF_t",
        "refinement_interpretation_Tm_refine_4217a417164cd9f176884ac8e9b5b15e",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_68ee6d2c8678eb431259a3d4f412550b",
        "refinement_interpretation_Tm_refine_8456759e660370b6e428c86ad6758869",
        "refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Hacl.Impl.Frodo.KEM.crypto_ciphertextbytes",
        "typing_Hacl.Impl.Frodo.KEM.crypto_secretkeybytes",
        "typing_Lib.Buffer.length", "typing_Spec.Frodo.Params.crypto_bytes",
        "typing_tok_Lib.Buffer.MUT@tok"
      ],
      0,
      "73a21fa9b8c00c6dc7b2776a21053fec"
    ],
    [
      "Hacl.Frodo.KEM.crypto_kem_dec",
      2,
      0,
      0,
      [
        "@query", "equality_tok_Lib.Buffer.MUT@tok",
        "equation_Lib.Buffer.as_seq",
        "equation_Spec.Frodo.KEM.crypto_kem_dec"
      ],
      0,
      "621eabc02c03c68d27ba754a2c8cc2f0"
    ]
  ]
]