[
  "�-�e��/ ^3Q>� ݗ",
  [
    [
      "X64.GCMencryptstdcall.va_req_gcm_make_length_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc",
        "equation_Prims.l_and", "equation_Prims.squash",
        "equation_Prims.subtype_of",
        "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "unit_typing"
      ],
      0,
      "2aa1642f25d12f53150ace4f24247a14"
    ],
    [
      "X64.GCMencryptstdcall.va_ens_gcm_make_length_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
        "equation_Prims.l_and", "equation_Prims.nat",
        "equation_Prims.squash", "equation_Prims.subtype_of",
        "equation_Words_s.nat64", "equation_Words_s.natN",
        "equation_X64.GCMencryptstdcall.va_req_gcm_make_length_stdcall",
        "equation_X64.Vale.Decls.va_state_eq",
        "fuel_guarded_inversion_X64.Vale.State.state",
        "function_token_typing_Prims.__cache_version_number__",
        "int_inversion", "l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
        "unit_typing"
      ],
      0,
      "0e52c1634efbee09ea8f26a73267b4a9"
    ],
    [
      "X64.GCMencryptstdcall.va_lemma_gcm_make_length_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Words_s.nat64",
        "equation_Words_s.natN",
        "function_token_typing_Prims.__cache_version_number__",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_af5af508c49760cd16656fe18f6ab623",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "9ad063d19c89fe347920d188942502db"
    ],
    [
      "X64.GCMencryptstdcall.va_wp_gcm_make_length_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565",
        "equation_Prims.nat", "equation_Words_s.nat64",
        "equation_Words_s.natN",
        "function_token_typing_Prims.__cache_version_number__",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "4c5f2b1a370c4d8a7875367123ed46e9"
    ],
    [
      "X64.GCMencryptstdcall.va_wpProof_gcm_make_length_stdcall",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "190bbf4375f44569cb7bdf60291b38a7"
    ]
  ]
]