[
  "FW>xRx`�\u000e�\\*��`W",
  [
    [
      "Hacl.Chacha20.Vec128.chacha20",
      1,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqHacl.Chacha20.Vec128_Tm_refine_530be526726c3b66223dd819f9d65058",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Chacha20.Vec128.chacha20",
      2,
      0,
      1,
      [
        "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n",
        "haseqHacl.Chacha20.Vec128_Tm_refine_530be526726c3b66223dd819f9d65058",
        "projection_inverse_BoxInt_proj_0"
      ],
      0
    ],
    [
      "Hacl.Chacha20.Vec128.chacha20",
      3,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Chacha20.Vec128.chacha20",
      4,
      0,
      1,
      [ "@query", "assumption_Prims.HasEq_int" ],
      0
    ],
    [
      "Hacl.Chacha20.Vec128.chacha20",
      5,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp",
        "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
        "equation_FStar.Buffer.equal", "equation_FStar.UInt32.n",
        "equation_FStar.UInt32.t", "equation_FStar.UInt32.v",
        "equation_FStar.UInt8.t",
        "equation_Hacl.Chacha20.Vec128.op_String_Access",
        "equation_Hacl.Impl.Chacha20.Vec128.uint8_p",
        "equation_Spec.Chacha20.blocklen",
        "equation_Spec.Chacha20.chacha20_ctx",
        "equation_Spec.Chacha20.keylen", "equation_Spec.Chacha20.noncelen",
        "equation_Spec.Chacha20_vec.blocklen",
        "equation_Spec.Chacha20_vec.keylen",
        "equation_Spec.Chacha20_vec.noncelen",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
        "kinding_FStar.UInt8.t_@tok", "lemma_FStar.Buffer.no_upd_lemma_1",
        "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
        "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_655f435aca33aabc4a1ca1fab5c827b9",
        "refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_89cfbffaea7abb55d8cc65915541f2c9",
        "refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_94403ae1db118a2daa8d61fa9d371d82",
        "refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
        "typing_FStar.Buffer.as_seq"
      ],
      0
    ],
    [
      "Hacl.Chacha20.Vec128.chacha20",
      6,
      0,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.as_seq",
        "equation_FStar.Buffer.buffer", "equation_FStar.UInt32.t",
        "equation_FStar.UInt8.t",
        "equation_Hacl.Chacha20.Vec128.op_String_Access",
        "equation_Hacl.Impl.Chacha20.Vec128.uint8_p",
        "equation_Spec.Chacha20_vec.keylen",
        "equation_Spec.Chacha20_vec.noncelen",
        "fuel_guarded_inversion_FStar.Buffer._buffer",
        "kinding_FStar.UInt8.t_@tok",
        "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
        "refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_5ecfbc3b1fb0a18cc9b570ff75576d79",
        "refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_655f435aca33aabc4a1ca1fab5c827b9",
        "refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_89cfbffaea7abb55d8cc65915541f2c9",
        "refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_94403ae1db118a2daa8d61fa9d371d82",
        "refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
        "typing_FStar.Buffer.as_seq"
      ],
      0
    ]
  ]
]