[
  "��՞;>w\u0015��3��a",
  [
    [
      "X64.Vale.InsSha.va_lemma_SHA256_rnds2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_SHA_helpers.counter", "equation_SHA_helpers.hash256",
        "equation_SHA_helpers.size_block_w_256", "equation_Words_s.nat32",
        "equation_X64.Machine_s.xmm",
        "fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_76eecaa5eb922850bd62c67e1b97491e",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "refinement_interpretation_Tm_refine_d87ea19ed2efd5ea1d518c459e7dcdd3",
        "refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
        "typing_SHA_helpers.k"
      ],
      0,
      "b6a09495c4577ac7ae6aeb864b00e3c3"
    ],
    [
      "X64.Vale.InsSha.va_wp_SHA256_rnds2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_SHA_helpers.counter",
        "equation_SHA_helpers.size_block_w_256",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_76eecaa5eb922850bd62c67e1b97491e",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "typing_SHA_helpers.k"
      ],
      0,
      "be8fac639ff9eb2d6287d3e0f0706e10"
    ],
    [
      "X64.Vale.InsSha.va_wpProof_SHA256_rnds2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "178e8147e287baaa45d0a2a7160fe375"
    ],
    [
      "X64.Vale.InsSha.va_lemma_SHA256_msg1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_SHA_helpers.counter", "int_inversion",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad"
      ],
      0,
      "1b203e8b5c1913f3d159e92ae9e021de"
    ],
    [
      "X64.Vale.InsSha.va_wp_SHA256_msg1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_SHA_helpers.counter", "int_inversion",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad"
      ],
      0,
      "14ff83e3a0dae0041c9a00ef981a53e5"
    ],
    [
      "X64.Vale.InsSha.va_wpProof_SHA256_msg1",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "ea3c2c369ba4f00650c6495d0ca1ada9"
    ],
    [
      "X64.Vale.InsSha.va_lemma_SHA256_msg2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_SHA_helpers.counter", "int_inversion",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad"
      ],
      0,
      "ea8b49ef88d00ec3b352b3b0f40894b4"
    ],
    [
      "X64.Vale.InsSha.va_wp_SHA256_msg2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.nat",
        "equation_SHA_helpers.counter", "int_inversion",
        "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad"
      ],
      0,
      "089a82f82a5a223a260584d27d0fea83"
    ],
    [
      "X64.Vale.InsSha.va_wpProof_SHA256_msg2",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "1e2d6fab41e471760acda94853b58a3e"
    ]
  ]
]