[
  "Åeœ–‰zû(\u0007.ÂW¦®Ë\u0006",
  [
    [
      "Vale.X64.InsSha.va_lemma_SHA256_rnds2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.X64.Decls.va_require_total",
        "equation_Vale.X64.Machine_s.reg_xmm",
        "fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_1ac5541806f355944a04e7bdf6a74b55",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b023f92fdc85789979f7b1f8b2bc8a31",
        "refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
        "typing_Vale.SHA.SHA_helpers.k"
      ],
      0,
      "4f58bbd8246f8a5b4a398c50ea55d596"
    ],
    [
      "Vale.X64.InsSha.va_wp_SHA256_rnds2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
        "refinement_interpretation_Tm_refine_b023f92fdc85789979f7b1f8b2bc8a31",
        "typing_Vale.SHA.SHA_helpers.k"
      ],
      0,
      "9461d36072f22ab27c1fc1e82c47e37b"
    ],
    [
      "Vale.X64.InsSha.va_quick_SHA256_rnds2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "c334b242383f3e345c3d77b18d43852b"
    ],
    [
      "Vale.X64.InsSha.va_lemma_SHA256_msg1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256", "int_inversion",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "3f09de465481ed6c9b51c5d86a2c8aef"
    ],
    [
      "Vale.X64.InsSha.va_wp_SHA256_msg1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256", "int_inversion",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "a0453bbff6b48c9d20f7f77f74fc7654"
    ],
    [
      "Vale.X64.InsSha.va_quick_SHA256_msg1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "97d4838c2cca03767cc8a472a67c5dc8"
    ],
    [
      "Vale.X64.InsSha.va_lemma_SHA256_msg2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256", "int_inversion",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "673f0b7d960b0438671220f2fa590c35"
    ],
    [
      "Vale.X64.InsSha.va_wp_SHA256_msg2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_Vale.SHA.SHA_helpers.counter",
        "equation_Vale.SHA.SHA_helpers.size_block_w_256", "int_inversion",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
      ],
      0,
      "76a99730b0cc6762c246f5a916c2ec28"
    ],
    [
      "Vale.X64.InsSha.va_quick_SHA256_msg2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "eb92b79781a05ddbc62401dd73b2b5ab"
    ]
  ]
]