[
  "\u0005�;��\u000e\u001e+q�a\u000f�ꄀ",
  [
    [
      "X64.GHash.get_last_slice_workaround",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
        "bool_typing", "equation_Prims.nat", "equation_Types_s.quad32",
        "equation_Words_s.nat32",
        "function_token_typing_Prims.__cache_version_number__",
        "function_token_typing_Words_s.nat32", "int_inversion",
        "kinding_Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_len_slice",
        "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
        "primitive_Prims.op_LessThanOrEqual",
        "primitive_Prims.op_Subtraction",
        "projection_inverse_BoxBool_proj_0",
        "projection_inverse_BoxInt_proj_0",
        "refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
        "refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
      ],
      0,
      "461fa602134291e0b6fde808deb4ac89"
    ],
    [
      "X64.GHash.va_wpProof_compute_ghash_incremental_register",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "dbdb8f373bcee63c803247ef294635bf"
    ],
    [
      "X64.GHash.va_wpProof_compute_ghash_incremental",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "8e390d043f3858861d4e362abbb8f46b"
    ],
    [
      "X64.GHash.va_lemma_ghash_incremental_bytes_no_extra",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "dbb339be4fb65453f6365f3dd6b282da"
    ],
    [
      "X64.GHash.va_wp_ghash_incremental_bytes_no_extra",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "44023694ee93ae948e41956d9fc4714c"
    ],
    [
      "X64.GHash.va_wpProof_ghash_incremental_bytes_no_extra",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "a3af1e8935b72d18828790c027d7db2f"
    ],
    [
      "X64.GHash.va_lemma_ghash_incremental_bytes_register",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "25d7a37b0a87ab5fc39034af6fd826ab"
    ],
    [
      "X64.GHash.va_wp_ghash_incremental_bytes_register",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "8c69389acd0e4cb32cdbf77a094d5378"
    ],
    [
      "X64.GHash.va_wpProof_ghash_incremental_bytes_register",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "8175a129ca4473b75d68df63880343e9"
    ],
    [
      "X64.GHash.va_lemma_ghash_incremental_bytes_extra",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "098267f977a8e96a81b6119b2b3d9fbf"
    ],
    [
      "X64.GHash.va_wp_ghash_incremental_bytes_extra",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "0e044221d744f8cfbd1878c0f35bfdd4"
    ],
    [
      "X64.GHash.va_wpProof_ghash_incremental_bytes_extra",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "81e7930343a13e2101b70c7906fd1bd3"
    ],
    [
      "X64.GHash.va_lemma_ghash_incremental_bytes",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "988baa4fe75aa7da1c8ba48b03953105"
    ],
    [
      "X64.GHash.va_wp_ghash_incremental_bytes",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "ed20bee88c132d94a49dcd3d99a93ed5"
    ],
    [
      "X64.GHash.va_wpProof_ghash_incremental_bytes",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query", "equation_Prims.squash",
        "refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
      ],
      0,
      "13e88f54af5a5995d3d7cc636be1d02b"
    ]
  ]
]