[
  "\u0002™‰}Y’\u0014·żŸ®…}„bd",
  [
    [
      "Spec.MD5.init_as_list",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@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.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "911b1ecba9feef86959f28fa39247620"
    ],
    [
      "Spec.MD5.h0",
      1,
      8,
      2,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
        "@query", "constructor_distinct_Prims.Cons",
        "constructor_distinct_Prims.Nil",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "data_elim_Prims.Cons", "data_typing_intro_Prims.Nil@tok",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equation_Lib.IntTypes.uint32", "equation_Prims.nat",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.MD5.init_as_list",
        "equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
        "function_token_typing_Lib.IntTypes.uint32", "int_inversion",
        "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
        "projection_inverse_Prims.Cons_a",
        "projection_inverse_Prims.Cons_hd",
        "projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_FStar.List.Tot.Base.length", "typing_Spec.MD5.init_as_list"
      ],
      0,
      "a541b6d99215ba00d34ae72990ae9617"
    ],
    [
      "Spec.MD5.t_as_list",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@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.maxint", "equation_Lib.IntTypes.minint",
        "equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "dc18ce6ff384439e8164b88085d07fb3"
    ],
    [
      "Spec.MD5.t",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.uint32",
        "equation_Spec.MD5.t_as_list",
        "function_token_typing_Lib.IntTypes.uint32",
        "refinement_interpretation_Tm_refine_d2d1ea66f2b3a92c2deb42edcbb784ce",
        "typing_FStar.Seq.Properties.seq_of_list",
        "typing_Spec.MD5.t_as_list"
      ],
      0,
      "b68d5bcf44150fdc53444fffbcdb28f5"
    ],
    [
      "Spec.MD5.round_op_gen_aux",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_FStar.Seq.Properties.lseq", "equation_Lib.IntTypes.uint32",
        "equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
        "equation_Spec.MD5.abcd_idx", "equation_Spec.MD5.abcd_t",
        "equation_Spec.MD5.t", "equation_Spec.MD5.t_idx",
        "equation_Spec.MD5.x_idx", "equation_Spec.MD5.x_t",
        "function_token_typing_Lib.IntTypes.uint32", "int_inversion",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_7acf795d50ec256996534a97e12bfa61",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_c2b2f0397c6f216bb58dc34f34f2bdfe",
        "refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f",
        "typing_Spec.MD5.t"
      ],
      0,
      "a0d5c7889fd6740323c0e2f57190aa9a"
    ],
    [
      "Spec.MD5.round1_aux",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "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.rotval", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Spec.MD5.rotate_idx", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0da46ef8643a6f8ea97a3358bc923338",
        "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "b5bf6e0866c5752070f1117f373a0010"
    ],
    [
      "Spec.MD5.round2_aux",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "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.rotval", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Spec.MD5.rotate_idx", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0da46ef8643a6f8ea97a3358bc923338",
        "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "83162727291abc898ff7328a3b3a70f9"
    ],
    [
      "Spec.MD5.round3_aux",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "b2t_def", "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equation_FStar.Seq.Properties.lseq", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
        "equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
        "equation_Lib.IntTypes.rotval", "equation_Lib.IntTypes.uint32",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Spec.MD5.rotate_idx", "equation_Spec.MD5.x_t",
        "function_token_typing_Lib.IntTypes.uint32", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0da46ef8643a6f8ea97a3358bc923338",
        "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.uint_to_t"
      ],
      0,
      "ef9bf2320c168383174ae6c9391a9d8e"
    ],
    [
      "Spec.MD5.round4_aux",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
        "bool_inversion", "bool_typing",
        "constructor_distinct_Lib.IntTypes.PUB",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U32",
        "equality_tok_Lib.IntTypes.PUB@tok",
        "equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
        "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
        "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
        "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.rotval", "equation_Lib.IntTypes.unsigned",
        "equation_Lib.IntTypes.v", "equation_Prims.nat",
        "equation_Spec.MD5.rotate_idx", "int_typing",
        "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.vu_inv",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_0da46ef8643a6f8ea97a3358bc923338",
        "refinement_interpretation_Tm_refine_0ea1fba779ad5718e28476faeef94d56",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
        "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "fd40794ca6714c66f136fb6e67e2edf8"
    ],
    [
      "Spec.MD5.overwrite_aux",
      1,
      2,
      1,
      [
        "@MaxIFuel_assumption", "@query",
        "equation_FStar.Seq.Properties.lseq", "equation_Lib.IntTypes.uint32",
        "equation_Spec.MD5.abcd_idx", "equation_Spec.MD5.abcd_t",
        "equation_Spec.MD5.ia", "equation_Spec.MD5.ib",
        "equation_Spec.MD5.ic", "equation_Spec.MD5.id",
        "function_token_typing_Lib.IntTypes.uint32",
        "lemma_FStar.Seq.Base.lemma_len_upd",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
        "refinement_interpretation_Tm_refine_7acf795d50ec256996534a97e12bfa61",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e"
      ],
      0,
      "1eb61b0351ece36e9d90ce5e2872f8b4"
    ],
    [
      "Spec.MD5.update_aux",
      1,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
        "equation_Prims.nat", "equation_Spec.Hash.Definitions.word_length",
        "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
        "primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
      ],
      0,
      "b0c2b0c051c90bbe0f6f1c7c9ce6de3f"
    ],
    [
      "Spec.MD5.update_aux",
      2,
      2,
      1,
      [
        "@MaxFuel_assumption", "@MaxIFuel_assumption",
        "@fuel_correspondence_Prims.pow2.fuel_instrumented",
        "@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
        "constructor_distinct_Lib.IntTypes.S16",
        "constructor_distinct_Lib.IntTypes.S8",
        "constructor_distinct_Lib.IntTypes.U1",
        "constructor_distinct_Lib.IntTypes.U32",
        "constructor_distinct_Lib.IntTypes.U8",
        "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Lib.IntTypes.U32@tok",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equation_FStar.Seq.Properties.lseq", "equation_Lib.IntTypes.bits",
        "equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
        "equation_Prims.nat", "equation_Spec.Hash.Definitions.is_md",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_length",
        "equation_Spec.Hash.Definitions.word_t",
        "equation_Spec.Hash.Definitions.words_state_",
        "equation_Spec.MD5.abcd_t", "equation_Spec.MD5.ia",
        "equation_Spec.MD5.ib", "equation_Spec.MD5.ic",
        "equation_Spec.MD5.id", "int_typing", "lemma_FStar.UInt.pow2_values",
        "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_778cda52ca3898c9d0220c148d4775e7",
        "refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
        "refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
        "typing_Lib.IntTypes.bits", "typing_Spec.Hash.Definitions.word_t",
        "typing_tok_Spec.Hash.Definitions.MD5@tok"
      ],
      0,
      "768694f5a8f7b4dc9260fa4c2c9ba1ce"
    ],
    [
      "Spec.MD5.update",
      1,
      2,
      1,
      [
        "@query", "constructor_distinct_Spec.Hash.Definitions.MD5",
        "equality_tok_Spec.Hash.Definitions.MD5@tok",
        "equation_Spec.Hash.Definitions.block_length",
        "equation_Spec.Hash.Definitions.block_word_length",
        "equation_Spec.Hash.Definitions.state_word_length",
        "equation_Spec.Hash.Definitions.word",
        "equation_Spec.Hash.Definitions.word_t"
      ],
      0,
      "49ba7053a0a182d56d737b7f3e76abda"
    ],
    [
      "Spec.MD5.finish",
      1,
      2,
      1,
      [ "@query" ],
      0,
      "d908abf4853a50729be3005efebed6d6"
    ]
  ]
]