[
  "��\u0011\u001a\u0007�\u001f\f��p���Y�",
  [
    [
      "Vale.AES.X64.AESGCM.aes_reqs_offset",
      1,
      1,
      0,
      [ "@query" ],
      0,
      "a43d63f689b661b043dceb27aa8f4b3d"
    ],
    [
      "Vale.AES.X64.AESGCM.va_lemma_AES_GCM_encrypt_6mult",
      1,
      1,
      0,
      [ "@query", "equation_Vale.AES.X64.AESGCM.aes_reqs_offset" ],
      0,
      "b3fa25eefef09c57ed6bc3c73f3e4a7d"
    ],
    [
      "Vale.AES.X64.AESGCM.va_wp_AES_GCM_encrypt_6mult",
      1,
      1,
      0,
      [ "@query", "equation_Vale.AES.X64.AESGCM.aes_reqs_offset" ],
      0,
      "1fd059423cbf74a73e3b87cf74305d73"
    ],
    [
      "Vale.AES.X64.AESGCM.va_quick_AES_GCM_encrypt_6mult",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "98a6c89e85370a767a179f12394e0ae4"
    ],
    [
      "Vale.AES.X64.AESGCM.va_lemma_AES_GCM_decrypt_6mult",
      1,
      1,
      0,
      [ "@query", "equation_Vale.AES.X64.AESGCM.aes_reqs_offset" ],
      0,
      "9d629718ab7c8db8283e2c3ad155a49c"
    ],
    [
      "Vale.AES.X64.AESGCM.va_wp_AES_GCM_decrypt_6mult",
      1,
      1,
      0,
      [ "@query", "equation_Vale.AES.X64.AESGCM.aes_reqs_offset" ],
      0,
      "d00e5ccf660f61df5f2c3d412e8643a3"
    ],
    [
      "Vale.AES.X64.AESGCM.va_quick_AES_GCM_decrypt_6mult",
      1,
      1,
      0,
      [
        "@MaxIFuel_assumption", "@query",
        "fuel_guarded_inversion_FStar.Pervasives.Native.tuple3"
      ],
      0,
      "1d0fe73df1d61904b6c796117c74bc5e"
    ]
  ]
]