Revision 3f979cc1cb15a4491f8b804bbafeabeffe5a1ab1 authored by Aseem Rastogi on 09 April 2019, 11:31:34 UTC, committed by Aseem Rastogi on 09 April 2019, 11:31:34 UTC
1 parent 74a8710
X64.AESCTR.fst.hints
[
"\u0015�\u0007��821b�'��mt�",
[
[
"X64.AESCTR.aes_reqs",
1,
1,
0,
[ "@query" ],
0,
"bfebc13272883b7a27e505aef2cb7d3b"
],
[
"X64.AESCTR.finish_aes_encrypt_le",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_AES_s.is_aes_key_LE",
"equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"fade29eb6a09efe562b3fbea483b72f4"
],
[
"X64.AESCTR.finish_aes_encrypt_le",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_AES_helpers.cipher_opaque",
"equation_AES_s.aes_encrypt_LE_def",
"equation_AES_s.key_to_round_keys_LE",
"equation_GCTR.aes_encrypt_le", "equation_Types_s.quad32",
"equation_Words_s.nat32", "fuel_guarded_inversion_Words_s.four",
"function_token_typing_Opaque_s.make_opaque",
"token_correspondence_AES_s.aes_encrypt_LE_def",
"token_correspondence_AES_s.cipher"
],
0,
"7b9bb98119a30bc64ebc2ee4187caf7d"
],
[
"X64.AESCTR.finish_aes_encrypt_le",
3,
1,
1,
[
"@MaxIFuel_assumption", "@query", "disc_equation_AES_s.AES_128",
"disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
"fuel_guarded_inversion_AES_s.algorithm"
],
0,
"476725dc4388d57dfc5f162b805ae16e"
],
[
"X64.AESCTR.va_lemma_aes_round_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_X64.Machine_s.xmm", "fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_aa6a7617e7c1979a44757e4a54a1faa6",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
],
0,
"b5730b3c0b31617eaff02f6d1d2dabfe"
],
[
"X64.AESCTR.va_lemma_aes_round_4way",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_AES_s.rounds.fuel_instrumented",
"@fuel_irrelevance_AES_s.rounds.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_Prims.Cons",
"constructor_distinct_X64.Machine_s.Block",
"disc_equation_Prims.Cons", "disc_equation_X64.Machine_s.Block",
"eq2-interp", "equation_AES_helpers.rounds_opaque",
"equation_AES_s.round", "equation_Prims.nat", "equation_Prims.pos",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_X64.AESCTR.va_code_aes_round_4way",
"equation_X64.AESCTR.va_transparent_code_aes_round_4way",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"equation_with_fuel_AES_s.rounds.fuel_instrumented",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_upd_ne", "primitive_Prims.op_Equality",
"proj_equation_Prims.Cons_hd", "proj_equation_Prims.Cons_tl",
"proj_equation_X64.Machine_s.Block_block",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_X64.Machine_s.Block_block",
"projection_inverse_X64.Machine_s.Block_t_ins",
"projection_inverse_X64.Machine_s.Block_t_ocmp",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_AES_s.rounds",
"token_correspondence_Opaque_s.make_opaque",
"typing_X64.CPU_Features_s.aesni_enabled",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd"
],
0,
"609c1aea45dea49018b9e0138b6647d6"
],
[
"X64.AESCTR.va_wp_aes_round_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
],
0,
"c811ef7e74ff3a234450a9ab9d086b71"
],
[
"X64.AESCTR.va_wpMonotone_aes_round_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_X64.AESCTR.va_wp_aes_round_4way",
"equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.update_xmm", "unit_typing"
],
0,
"f78d3649d58f7b5378bbea969faa7971"
],
[
"X64.AESCTR.va_wpCompute_aes_round_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AESCTR.va_code_aes_round_4way",
"equation_X64.AESCTR.va_wp_aes_round_4way",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"refinement_interpretation_X64.Machine_s_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd"
],
0,
"6fd2b1d0a82493056de49c3c5318e153"
],
[
"X64.AESCTR.va_wpProof_aes_round_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"f8c48a5eb20770ae7803c470807d05ab"
],
[
"X64.AESCTR.va_wpProof_aes_round_4way",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Prims.pos", "equation_Types_s.quad32",
"equation_Words_s.nat32",
"equation_X64.AESCTR.va_code_aes_round_4way",
"equation_X64.AESCTR.va_wpCompute_aes_round_4way",
"equation_X64.AESCTR.va_wp_aes_round_4way",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESCTR.va_wpCompute_aes_round_4way",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.update_xmm", "typing_X64.Vale.Xmms.sel",
"typing_X64.Vale.Xmms.upd", "unit_typing"
],
0,
"19507fdbc15007a6197a74c6a1847aa5"
],
[
"X64.AESCTR.va_qcode_aes_2rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"574b0e90ae2fc2b22f8272d14094d32e"
],
[
"X64.AESCTR.va_lemma_aes_2rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_6d293ed172b8c6bee1f1c1ea11e195ca",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"32ab4156c76ac84726c400d93dfd47ed"
],
[
"X64.AESCTR.va_lemma_aes_2rounds_4way",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Prims.eq2", "equation_Prims.l_and",
"equation_Prims.pos", "equation_Prims.squash",
"equation_Types_s.quad32", "equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "l_and-interp",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_X64.CPU_Features_s.aesni_enabled",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "unit_typing"
],
0,
"d815e5fccbdbc5d4f700eac544a408a9"
],
[
"X64.AESCTR.va_wp_aes_2rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
],
0,
"89d2794009a91b8399a04715f681d5a3"
],
[
"X64.AESCTR.va_wpMonotone_aes_2rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_X64.AESCTR.va_wp_aes_2rounds_4way",
"equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.update_xmm", "unit_typing"
],
0,
"e754e0cc017df95a3623a5825bc9bad0"
],
[
"X64.AESCTR.va_wpCompute_aes_2rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AESCTR.va_wp_aes_2rounds_4way",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"b43ae94af2b3a20285fe8ae5eec03db9"
],
[
"X64.AESCTR.va_wpProof_aes_2rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"8028c23231df3c100ae5e190692c1220"
],
[
"X64.AESCTR.va_wpProof_aes_2rounds_4way",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Prims.pos", "equation_Types_s.quad32",
"equation_Words_s.nat32",
"equation_X64.AESCTR.va_wpCompute_aes_2rounds_4way",
"equation_X64.AESCTR.va_wp_aes_2rounds_4way",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESCTR.va_wpCompute_aes_2rounds_4way",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.update_xmm", "typing_X64.Vale.Xmms.sel",
"typing_X64.Vale.Xmms.upd", "unit_typing"
],
0,
"1c57cadc2e8575189a67eb0a1723a44d"
],
[
"X64.AESCTR.va_qcode_aes_3rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"7827f583c1280d30976fb873258f899f"
],
[
"X64.AESCTR.va_lemma_aes_3rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2cfddddb751004f7a7b937c5639a941d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"c4d8a098daa22695bf32764a233ea509"
],
[
"X64.AESCTR.va_lemma_aes_3rounds_4way",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Prims.eq2", "equation_Prims.l_and",
"equation_Prims.squash", "equation_Types_s.quad32",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"l_and-interp", "lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_X64.CPU_Features_s.aesni_enabled",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "unit_typing"
],
0,
"a12a6a6ed31450f24fad3c72c3d3d6b1"
],
[
"X64.AESCTR.va_wp_aes_3rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
],
0,
"d4aa0009586cb96b1d8ed2eb49f38ed8"
],
[
"X64.AESCTR.va_wpMonotone_aes_3rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_X64.AESCTR.va_wp_aes_3rounds_4way",
"equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.update_xmm", "unit_typing"
],
0,
"3c7b3f962fc9e09c3d3c450151e1f9cb"
],
[
"X64.AESCTR.va_wpCompute_aes_3rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AESCTR.va_wp_aes_3rounds_4way",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"040a4de2b62b616b1793c8b3429ca434"
],
[
"X64.AESCTR.va_wpProof_aes_3rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"b1fd7261d16aeffc450fab90cfe1951a"
],
[
"X64.AESCTR.va_wpProof_aes_3rounds_4way",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Prims.pos", "equation_Types_s.quad32",
"equation_Words_s.nat32",
"equation_X64.AESCTR.va_wpCompute_aes_3rounds_4way",
"equation_X64.AESCTR.va_wp_aes_3rounds_4way",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESCTR.va_wpCompute_aes_3rounds_4way",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.update_xmm", "typing_X64.Vale.Xmms.sel",
"typing_X64.Vale.Xmms.upd", "unit_typing"
],
0,
"508f073c9b5bcad63501b447651293a9"
],
[
"X64.AESCTR.va_qcode_aes_4rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"e4b2b5797557495fec529e88eaacb0c3"
],
[
"X64.AESCTR.va_lemma_aes_4rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_f4c9633f61eb1bbdcc147146dd360906"
],
0,
"253c2149b09f7f0651bd5730526a1397"
],
[
"X64.AESCTR.va_lemma_aes_4rounds_4way",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Prims.eq2", "equation_Prims.l_and",
"equation_Prims.pos", "equation_Prims.squash",
"equation_Types_s.quad32", "equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "l_and-interp",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_X64.CPU_Features_s.aesni_enabled",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "unit_typing"
],
0,
"ebfd1924cedb7afbad6a0a9cd68ef091"
],
[
"X64.AESCTR.va_wp_aes_4rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Prims_Tm_refine_c42d7927e44e0f393ec040dac09bfa8d"
],
0,
"229c5c8b6aca2eb4663a1d9280308bcc"
],
[
"X64.AESCTR.va_wpMonotone_aes_4rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_X64.AESCTR.va_wp_aes_4rounds_4way",
"equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.update_xmm", "unit_typing"
],
0,
"509caf3c79145dfa415b2f4e0408db6a"
],
[
"X64.AESCTR.va_wpCompute_aes_4rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AESCTR.va_wp_aes_4rounds_4way",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"8ab2da10acbe1fdef275ebb22d5a3e90"
],
[
"X64.AESCTR.va_wpProof_aes_4rounds_4way",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"f835aed45195796d77e8a6419f3129cf"
],
[
"X64.AESCTR.va_wpProof_aes_4rounds_4way",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equation_Prims.pos", "equation_Types_s.quad32",
"equation_Words_s.nat32",
"equation_X64.AESCTR.va_wpCompute_aes_4rounds_4way",
"equation_X64.AESCTR.va_wp_aes_4rounds_4way",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESCTR.va_wpCompute_aes_4rounds_4way",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.update_xmm", "typing_X64.Vale.Xmms.sel",
"typing_X64.Vale.Xmms.upd", "unit_typing"
],
0,
"14f14bddfbe2d43fe5bd7f4bed18f20c"
],
[
"X64.AESCTR.va_qcode_aes_ctr_encrypt",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "eq2-interp",
"equation_Prims.eq2", "equation_Prims.squash",
"fuel_guarded_inversion_AES_s.algorithm",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"unit_typing"
],
0,
"dc9450cde094dc630e67b95e4b5db0f3"
],
[
"X64.AESCTR.va_qcode_aes_ctr_encrypt",
2,
1,
0,
[ "@query" ],
0,
"7560493d93ace93f69ea8e8123658754"
],
[
"X64.AESCTR.va_qcode_aes_ctr_encrypt",
3,
1,
0,
[ "@query" ],
0,
"3ef9b44a82d60d1ef0602ffd6302e86a"
],
[
"X64.AESCTR.va_qcode_aes_ctr_encrypt",
4,
1,
0,
[ "@query" ],
0,
"6570c4743b9dc6bb207ac44b028678e4"
],
[
"X64.AESCTR.va_qcode_aes_ctr_encrypt",
5,
1,
0,
[ "@query" ],
0,
"bdc5ce3236a067d263909f9fb6c4b00b"
],
[
"X64.AESCTR.va_qcode_aes_ctr_encrypt",
6,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_AES_s.AES_128", "disc_equation_AES_s.AES_128",
"disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
"eq2-interp", "equation_Prims.eq2", "equation_Prims.squash",
"fuel_guarded_inversion_AES_s.algorithm",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"8fcfad095f36c7be851cb11bdd3608ab"
],
[
"X64.AESCTR.va_qcode_aes_ctr_encrypt",
7,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_AES_s.AES_128", "disc_equation_AES_s.AES_128",
"disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
"eq2-interp", "equation_Prims.eq2", "equation_Prims.squash",
"fuel_guarded_inversion_AES_s.algorithm",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"d65ffc50f2bf96d4fd091b5fb61d91f1"
],
[
"X64.AESCTR.va_qcode_aes_ctr_encrypt",
8,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_AES_s.AES_128", "disc_equation_AES_s.AES_128",
"disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
"eq2-interp", "equation_Prims.eq2", "equation_Prims.squash",
"fuel_guarded_inversion_AES_s.algorithm",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"6447f780738a9656ce33fa51168c8cde"
],
[
"X64.AESCTR.va_qcode_aes_ctr_encrypt",
9,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_AES_s.AES_128", "disc_equation_AES_s.AES_128",
"disc_equation_AES_s.AES_192", "disc_equation_AES_s.AES_256",
"eq2-interp", "equation_Prims.eq2", "equation_Prims.squash",
"fuel_guarded_inversion_AES_s.algorithm",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"7047077b90e6470bef5e50d9979cfff3"
],
[
"X64.AESCTR.va_qcode_aes_ctr_encrypt",
10,
1,
0,
[ "@query" ],
0,
"0b3a376d5479c557fce9eebddc7e1718"
],
[
"X64.AESCTR.va_qcode_aes_ctr_encrypt",
11,
1,
0,
[ "@query" ],
0,
"030389ced191d7e8954592e640025747"
],
[
"X64.AESCTR.va_qcode_aes_ctr_encrypt",
12,
1,
0,
[ "@query" ],
0,
"add6b6339202d487484f0a49c0dbc537"
],
[
"X64.AESCTR.va_qcode_aes_ctr_encrypt",
13,
1,
0,
[ "@query" ],
0,
"8fd303f4bef4ccc59e1ef5ac8b0155d1"
],
[
"X64.AESCTR.va_lemma_aes_ctr_encrypt",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"AES_s_pretyping_443f63aed29daed744644bd1799d3a91",
"constructor_distinct_AES_s.AES_128",
"constructor_distinct_AES_s.AES_256",
"equality_tok_AES_s.AES_128@tok", "equality_tok_AES_s.AES_256@tok",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_X64.AESCTR.aes_reqs",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_X64.AESCTR_Tm_refine_5aa2c403299cbc9471b78b205d35a43f",
"typing_tok_AES_s.AES_128@tok"
],
0,
"2ed75ae47b0cbe06686518463e42236f"
],
[
"X64.AESCTR.va_lemma_aes_ctr_encrypt",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"AES_s_pretyping_443f63aed29daed744644bd1799d3a91",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_AES_s.AES_128",
"constructor_distinct_AES_s.AES_192",
"constructor_distinct_AES_s.AES_256",
"constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_Tm_unit", "eq2-interp",
"equality_tok_AES_s.AES_128@tok", "equality_tok_AES_s.AES_256@tok",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_AES_s.is_aes_key_LE", "equation_GCTR.aes_encrypt_le",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Prop_s.prop0", "equation_Types_s.quad32",
"equation_Words_s.nat32", "equation_Words_s.nat64",
"equation_X64.AESCTR.aes_reqs", "equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"kinding_Words_s.four@tok", "l_and-interp",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"primitive_Prims.op_Equality",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"string_typing", "typing_FStar.Seq.Base.length",
"typing_GCTR.aes_encrypt_le", "typing_Prims.eq2",
"typing_Prims.l_and", "typing_X64.AESCTR.aes_reqs",
"typing_X64.Memory.buffer_read", "typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
"typing_tok_AES_s.AES_128@tok",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.R8@tok", "unit_inversion", "unit_typing"
],
0,
"4922f8f532c1581c62641c29d515b7ed"
],
[
"X64.AESCTR.va_wp_aes_ctr_encrypt",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"AES_s_pretyping_443f63aed29daed744644bd1799d3a91",
"constructor_distinct_AES_s.AES_128",
"constructor_distinct_AES_s.AES_256",
"equality_tok_AES_s.AES_128@tok", "equality_tok_AES_s.AES_256@tok",
"equation_X64.AESCTR.aes_reqs", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0", "typing_tok_AES_s.AES_128@tok"
],
0,
"750f7be3201569aeb70db55c96fbe9a1"
],
[
"X64.AESCTR.va_wpMonotone_aes_ctr_encrypt",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_X64.AESCTR.va_wp_aes_ctr_encrypt",
"equation_X64.Machine_s.xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_xmm", "unit_typing"
],
0,
"fc479510b26173289a995eb9e52de9c1"
],
[
"X64.AESCTR.va_wpCompute_aes_ctr_encrypt",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AESCTR.va_wp_aes_ctr_encrypt",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"76dbdbf9cbbadc9ca20a6813c9f7ac97"
],
[
"X64.AESCTR.va_wpProof_aes_ctr_encrypt",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"ad2ed575db08d03e0ed8c8b7008ead5e"
],
[
"X64.AESCTR.va_wpProof_aes_ctr_encrypt",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"AES_s_pretyping_443f63aed29daed744644bd1799d3a91",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_AES_s.AES_128@tok",
"equality_tok_AES_s.AES_256@tok", "equation_Types_s.quad32",
"equation_Words_s.nat32", "equation_X64.AESCTR.aes_reqs",
"equation_X64.AESCTR.va_wpCompute_aes_ctr_encrypt",
"equation_X64.AESCTR.va_wp_aes_ctr_encrypt",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"primitive_Prims.op_Equality",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESCTR.va_wpCompute_aes_ctr_encrypt",
"typing_GCTR.aes_encrypt_le", "typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
"typing_tok_AES_s.AES_128@tok", "unit_typing"
],
0,
"d60cdf73a3d92be5b6fb630a0fc0236e"
],
[
"X64.AESCTR.va_qcode_aes_ctr_ghash",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad"
],
0,
"d7a7b9b81d39a3ac317e6b5b483e1f1f"
],
[
"X64.AESCTR.va_lemma_aes_ctr_ghash",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Interop.Types.TUInt128",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.nat",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.validDstAddrs128",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "lemma_X64.Memory.buffer_length_buffer_as_seq",
"proj_equation_X64.Vale.State.Mkstate_mem",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_tok_Interop.Types.TUInt128@tok"
],
0,
"2a613df9808edd505be3c43bdd418945"
],
[
"X64.AESCTR.va_lemma_aes_ctr_ghash",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.logical", "equation_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.State.state_eq",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_typing",
"kinding_Words_s.four@tok",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"string_typing", "typing_GHash.ghash_incremental",
"typing_Prims.eq2", "typing_Types_s.reverse_bytes_quad32",
"typing_Workarounds.slice_work_around",
"typing_X64.Memory.buffer_as_seq",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
"typing_tok_Interop.Types.TUInt128@tok", "unit_inversion",
"unit_typing"
],
0,
"48da64af7e381f61bc34cf6e2ab79892"
],
[
"X64.AESCTR.va_wp_aes_ctr_ghash",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Interop.Types.TUInt128",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.nat",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.validDstAddrs128",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "lemma_X64.Memory.buffer_length_buffer_as_seq",
"proj_equation_X64.Vale.State.Mkstate_mem",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_tok_Interop.Types.TUInt128@tok"
],
0,
"0e9c16f80cfa71020e2d2ce93b087777"
],
[
"X64.AESCTR.va_wpMonotone_aes_ctr_ghash",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equality_tok_X64.Machine_s.R12@tok",
"equation_X64.AESCTR.va_wp_aes_ctr_ghash",
"equation_X64.Machine_s.xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_tok_X64.Machine_s.R12@tok", "unit_typing"
],
0,
"628978572cd222cd654d72933cdc4902"
],
[
"X64.AESCTR.va_wpCompute_aes_ctr_ghash",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AESCTR.va_wp_aes_ctr_ghash",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"9f9d4a2c5e11ef75a7b63b09e7cadf38"
],
[
"X64.AESCTR.va_wpProof_aes_ctr_ghash",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"522037855beaebaf84863819a27802ce"
],
[
"X64.AESCTR.va_wpProof_aes_ctr_ghash",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_X64.Machine_s.R12@tok",
"equation_Prims.nat", "equation_Types_s.quad32",
"equation_Words_s.nat32", "equation_Words_s.nat64",
"equation_Words_s.natN",
"equation_X64.AESCTR.va_wpCompute_aes_ctr_ghash",
"equation_X64.AESCTR.va_wp_aes_ctr_ghash",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESCTR.va_wpCompute_aes_ctr_ghash",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_tok_X64.Machine_s.R12@tok",
"unit_typing"
],
0,
"4ec8f61a57016561cc9d9942ba166191"
],
[
"X64.AESCTR.va_qcode_aes_ctr_loop_body",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2",
"equation_Prims.squash", "fuel_guarded_inversion_AES_s.algorithm",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"576a743a337f7c741c3bfa033b38eb27"
],
[
"X64.AESCTR.va_lemma_aes_ctr_loop_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Types_s.quad32",
"equation_Words_s.nat32", "equation_Words_s.nat64",
"equation_Words_s.natN", "fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0965742c112fd4ed732dfcb64fe12e7a",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"86a4dfbfbb6bfc015efe26188838de4c"
],
[
"X64.AESCTR.va_lemma_aes_ctr_loop_body",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"AES_s_pretyping_443f63aed29daed744644bd1799d3a91",
"FStar.Seq.Base_interpretation_Tm_arrow_f75731c55f9043e32f86307b15aa8254",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_interpretation_Tm_arrow_f82c3fb9ac6610efb97620a59b378092",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_AES_s.AES_128",
"constructor_distinct_AES_s.AES_256",
"constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
"equality_tok_AES_s.AES_128@tok", "equality_tok_AES_s.AES_256@tok",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_AES_s.is_aes_key_LE",
"equation_Arch.Types.add_wrap_quad32",
"equation_GCTR.aes_encrypt_BE", "equation_GCTR.gctr_partial",
"equation_GCTR_s.inc32", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_and",
"equation_Prims.logical", "equation_Prims.min", "equation_Prims.nat",
"equation_Prims.squash", "equation_Prop_s.prop0",
"equation_Types_s.add_wrap", "equation_Types_s.quad32",
"equation_Types_s.quad32_xor",
"equation_Types_s.reverse_bytes_nat32",
"equation_Words.Four_s.four_reverse", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.AESCTR.aes_reqs", "equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_Prims.int",
"function_token_typing_Types_s.reverse_bytes_nat32_def",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"interpretation_Tm_abs_033c986f28fa90d27d2ea96e5cb797c4",
"interpretation_Tm_abs_06fda2d59772d36c4f948076cc7cff5a",
"interpretation_Tm_abs_1560a48154565d7c95b77a91728286ef",
"interpretation_Tm_abs_26b78bca4f221b4c469edd213f71ebef",
"interpretation_Tm_abs_31a4ae7b16520800bc18cf9bbd53a44e",
"interpretation_Tm_abs_360d206e59f81e30a4f0942cf993355c",
"interpretation_Tm_abs_3e1f041a6f09814938eee18ab884436d",
"interpretation_Tm_abs_505c57c5d9692277904e6b36ccca5145",
"interpretation_Tm_abs_87d82d65cf44edfd806d90d4c7a3a37c",
"interpretation_Tm_abs_d1af12f729a4e0467aeeebb1a2d4b4fe",
"kinding_Tm_arrow_f82c3fb9ac6610efb97620a59b378092",
"kinding_Words_s.four@tok", "l_and-interp",
"lemma_Arch.Types.lemma_reverse_bytes_quad32",
"lemma_Arch.Types.lemma_reverse_reverse_bytes_nat32",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_upd",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Memory.loc_includes_refl",
"lemma_X64.Memory.modifies_buffer_addr",
"lemma_X64.Memory.modifies_buffer_elim",
"lemma_X64.Memory.modifies_buffer_readable",
"lemma_X64.Memory.modifies_goal_directed_refl",
"lemma_X64.Memory.modifies_goal_directed_trans",
"lemma_X64.Memory.modifies_goal_directed_trans2",
"lemma_X64.Memory.modifies_valid_taint128",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "proj_equation_Words_s.Mkfour_hi2",
"proj_equation_Words_s.Mkfour_hi3",
"proj_equation_Words_s.Mkfour_lo0",
"proj_equation_Words_s.Mkfour_lo1",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_5bb8ca8bd1e34326f95f9f0f9a641acf",
"refinement_interpretation_Tm_refine_6d2333afbb8ce899cd8937b56b09e98d",
"refinement_interpretation_Tm_refine_94f72bfda5e23ac3960136c8bc3f958c",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c16bc1b61f58b349bf6fc1c94dcaf83b",
"refinement_interpretation_Tm_refine_d1f295a68bb616ae63ab7b3087e3ebcc",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "token_correspondence_Opaque_s.make_opaque",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.upd",
"typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
"typing_GCTR.aes_encrypt_BE", "typing_GCTR.gctr_partial",
"typing_GCTR_s.inc32", "typing_GHash.ghash_incremental",
"typing_Opaque_s.make_opaque", "typing_Prims.eq2",
"typing_Prims.l_and",
"typing_Tm_abs_87d82d65cf44edfd806d90d4c7a3a37c",
"typing_Types_s.add_wrap", "typing_Types_s.quad32_xor",
"typing_Types_s.reverse_bytes_nat32",
"typing_Types_s.reverse_bytes_quad32",
"typing_Words_s.__proj__Mkfour__item__hi2",
"typing_Words_s.__proj__Mkfour__item__hi3",
"typing_Words_s.__proj__Mkfour__item__lo0",
"typing_Words_s.__proj__Mkfour__item__lo1",
"typing_Workarounds.slice_work_around", "typing_X64.AESCTR.aes_reqs",
"typing_X64.CPU_Features_s.pclmulqdq_enabled",
"typing_X64.Memory.buffer_addr", "typing_X64.Memory.buffer_as_seq",
"typing_X64.Memory.buffer_read", "typing_X64.Memory.buffer_readable",
"typing_X64.Memory.buffer_write",
"typing_X64.Memory.buffer_writeable", "typing_X64.Memory.loc_buffer",
"typing_X64.Memory.modifies",
"typing_X64.Vale.Decls.validDstAddrs128",
"typing_X64.Vale.Decls.validSrcAddrs128",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
"typing_tok_AES_s.AES_128@tok", "typing_tok_AES_s.AES_256@tok",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Secret@tok", "unit_inversion",
"unit_typing"
],
0,
"69ebbacba876b5504793d3ed0e444b40"
],
[
"X64.AESCTR.va_wp_aes_ctr_loop_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad"
],
0,
"631683fd519f9721ceccf8c017b99415"
],
[
"X64.AESCTR.va_wpMonotone_aes_ctr_loop_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equation_X64.AESCTR.va_wp_aes_ctr_loop_body",
"equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm",
"typing_X64.Vale.State.update_xmm",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rdx@tok", "unit_typing"
],
0,
"59a27bc6efcb15e54e52a0fd6aeccc34"
],
[
"X64.AESCTR.va_wpCompute_aes_ctr_loop_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AESCTR.va_wp_aes_ctr_loop_body",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"a0ebfd508961fbc819386c6e363b202b"
],
[
"X64.AESCTR.va_wpProof_aes_ctr_loop_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"7c0be09812a50630a4ffe56230d72082"
],
[
"X64.AESCTR.va_wpProof_aes_ctr_loop_body",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"AES_s_pretyping_443f63aed29daed744644bd1799d3a91",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_AES_s.AES_128@tok",
"equality_tok_AES_s.AES_256@tok",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rdx@tok", "equation_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.AESCTR.aes_reqs",
"equation_X64.AESCTR.va_wpCompute_aes_ctr_loop_body",
"equation_X64.AESCTR.va_wp_aes_ctr_loop_body",
"equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"kinding_Words_s.four@tok", "lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"primitive_Prims.op_Equality",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESCTR.va_wpCompute_aes_ctr_loop_body",
"typing_GHash.ghash_incremental",
"typing_Types_s.reverse_bytes_quad32",
"typing_Workarounds.slice_work_around",
"typing_X64.Memory.buffer_as_seq", "typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_tok_AES_s.AES_128@tok",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rdx@tok", "unit_typing"
],
0,
"7082103b5b8ff492966dda4161d6e9a8"
],
[
"X64.AESCTR.va_qcode_aes_counter_loop_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"532221cd69842723fc7683c5b971b9b4"
],
[
"X64.AESCTR.va_lemma_aes_counter_loop_body",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"99148f4a5da9cea83c9f3701c319c98a"
],
[
"X64.AESCTR.va_lemma_aes_counter_loop_body",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"bool_typing", "constructor_distinct_Interop.Types.TUInt128",
"eq2-interp", "equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_Prims.LexTop@tok",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_GHash.ghash_incremental0", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Prop_s.prop0", "equation_Types_s.add_wrap",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.AESCTR.aes_reqs", "equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCodes.lexCons",
"equation_X64.Vale.QuickCodes.precedes_wrap",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.state_eta",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.int",
"function_token_typing_Words_s.nat32",
"function_token_typing_Words_s.nat64", "int_inversion", "int_typing",
"kinding_Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Memory.loc_includes_refl",
"lemma_X64.Memory.modifies_buffer_elim",
"lemma_X64.Memory.modifies_goal_directed_refl",
"lemma_X64.Memory.modifies_goal_directed_trans",
"lemma_X64.Memory.modifies_goal_directed_trans2",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Regs.lemma_eta",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_eta", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.seq", "typing_GCTR.gctr_partial",
"typing_GHash.ghash_incremental0", "typing_Prims.eq2",
"typing_Types_s.reverse_bytes_quad32",
"typing_Workarounds.slice_work_around", "typing_X64.AESCTR.aes_reqs",
"typing_X64.Memory.buffer_addr", "typing_X64.Memory.buffer_as_seq",
"typing_X64.Memory.loc_buffer", "typing_X64.Memory.modifies",
"typing_X64.Vale.Decls.validDstAddrs128",
"typing_X64.Vale.Decls.validSrcAddrs128",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.lexCons",
"typing_X64.Vale.QuickCodes.precedes_wrap",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.state_eta", "typing_X64.Vale.Xmms.eta_sel",
"typing_X64.Vale.Xmms.sel", "typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_Prims.LexTop@tok", "typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Secret@tok", "unit_typing",
"well-founded-ordering-on-nat"
],
0,
"847dc27549ee3a01224c1316be93b0f1"
],
[
"X64.AESCTR.va_wp_aes_counter_loop_body",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"02bcbd247f9708db590bb66307482c55"
],
[
"X64.AESCTR.va_wpMonotone_aes_counter_loop_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_X64.Machine_s.R10",
"constructor_distinct_X64.Machine_s.R12",
"constructor_distinct_X64.Machine_s.R9",
"constructor_distinct_X64.Machine_s.Rdx",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rdx@tok", "equation_Prims.nat",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.AESCTR.va_wp_aes_counter_loop_body",
"equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_X64.Vale.Regs.lemma_upd_eq",
"lemma_X64.Vale.Regs.lemma_upd_ne",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R9@tok", "typing_tok_X64.Machine_s.Rdx@tok"
],
0,
"598d90ee67611790a0a6040f20b7d809"
],
[
"X64.AESCTR.va_wpCompute_aes_counter_loop_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AESCTR.va_wp_aes_counter_loop_body",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"6d8a1c7f5abd9cfaf72d4d7052b0dd04"
],
[
"X64.AESCTR.va_wpProof_aes_counter_loop_body",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"71de8f5f61e6b7622be7b0f81775d3a9"
],
[
"X64.AESCTR.va_wpProof_aes_counter_loop_body",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"AES_s_pretyping_443f63aed29daed744644bd1799d3a91",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"eq2-interp", "equality_tok_AES_s.AES_128@tok",
"equality_tok_AES_s.AES_256@tok",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rdx@tok", "equation_Prims.nat",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_X64.AESCTR.aes_reqs",
"equation_X64.AESCTR.va_wpCompute_aes_counter_loop_body",
"equation_X64.AESCTR.va_wp_aes_counter_loop_body",
"equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"kinding_Words_s.four@tok", "lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"primitive_Prims.op_Equality",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESCTR.va_wpCompute_aes_counter_loop_body",
"typing_GHash.ghash_incremental0",
"typing_Types_s.reverse_bytes_quad32",
"typing_Workarounds.slice_work_around",
"typing_X64.Memory.buffer_as_seq",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_tok_AES_s.AES_128@tok",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R9@tok", "typing_tok_X64.Machine_s.Rdx@tok"
],
0,
"377b671c3646dab82d7e6dba78a9948d"
],
[
"X64.AESCTR.va_code_aes_counter_loop_while",
1,
1,
0,
[
"@query", "constructor_distinct_X64.Vale.Decls.TConst",
"constructor_distinct_X64.Vale.Decls.TReg",
"disc_equation_X64.Vale.Decls.TStack",
"equality_tok_X64.Machine_s.Rdx@tok", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0"
],
0,
"a22a6a4afd389fbd50382654d9e0038b"
],
[
"X64.AESCTR.va_qcode_aes_counter_loop_while",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_X64.Vale.Decls.TConst",
"constructor_distinct_X64.Vale.Decls.TReg",
"disc_equation_X64.Vale.Decls.TStack",
"equality_tok_X64.Machine_s.Rdx@tok", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"primitive_Prims.op_BarBar", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"604f27e276085de1164c7f2555c24da1"
],
[
"X64.AESCTR.va_qcode_aes_counter_loop_while",
2,
1,
0,
[
"@query", "constructor_distinct_X64.Vale.Decls.TConst",
"constructor_distinct_X64.Vale.Decls.TReg",
"disc_equation_X64.Vale.Decls.TStack",
"equality_tok_X64.Machine_s.Rdx@tok", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0"
],
0,
"2a18639ae97e85f90d0f2a0ed1931182"
],
[
"X64.AESCTR.va_qcode_aes_counter_loop_while",
3,
1,
0,
[
"@query", "constructor_distinct_X64.Vale.Decls.TConst",
"constructor_distinct_X64.Vale.Decls.TReg",
"disc_equation_X64.Vale.Decls.TStack",
"equality_tok_X64.Machine_s.Rdx@tok", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0"
],
0,
"085510043d19802585603b0f7eb4c039"
],
[
"X64.AESCTR.va_lemma_aes_counter_loop_while",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"fb975e5c3f1acf2e9ac84cbe404700af"
],
[
"X64.AESCTR.va_lemma_aes_counter_loop_while",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Interop.Types.TUInt128", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_Prims.LexTop@tok",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Secret@tok", "equation_Prims.eq2",
"equation_Prims.eqtype", "equation_Prims.l_False",
"equation_Prims.l_and", "equation_Prims.l_imp",
"equation_Prims.l_not", "equation_Prims.logical",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Prop_s.prop0", "equation_Types_s.add_wrap",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.AESCTR.aes_reqs", "equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCodes.lexCons",
"equation_X64.Vale.QuickCodes.precedes_wrap",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.state_eta",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.int",
"function_token_typing_Words_s.nat32",
"function_token_typing_Words_s.nat64", "int_inversion", "int_typing",
"kinding_Words_s.four@tok", "l_and-interp", "l_imp-interp",
"l_not-interp", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Regs.lemma_eta",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_eta", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.seq", "typing_GCTR.gctr_partial",
"typing_GHash.ghash_incremental0", "typing_Prims.eq2",
"typing_Types_s.reverse_bytes_quad32",
"typing_Workarounds.slice_work_around", "typing_X64.AESCTR.aes_reqs",
"typing_X64.CPU_Features_s.pclmulqdq_enabled",
"typing_X64.Memory.buffer_addr", "typing_X64.Memory.buffer_as_seq",
"typing_X64.Memory.loc_buffer", "typing_X64.Memory.modifies",
"typing_X64.Vale.Decls.validDstAddrs128",
"typing_X64.Vale.Decls.validSrcAddrs128",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.state_eta", "typing_X64.Vale.Xmms.eta_sel",
"typing_X64.Vale.Xmms.sel", "typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Secret@tok", "unit_typing"
],
0,
"8af0e3006e9d38dc9120f8ce5d639010"
],
[
"X64.AESCTR.va_wp_aes_counter_loop_while",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"124b1b79616084fce57b8f4823d03320"
],
[
"X64.AESCTR.va_wpMonotone_aes_counter_loop_while",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rdx@tok", "equation_Prims.nat",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.AESCTR.va_wp_aes_counter_loop_while",
"equation_X64.Machine_s.xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R9@tok", "typing_tok_X64.Machine_s.Rdx@tok"
],
0,
"900c83cd1db8d4a1e5a41c6ebfb622a7"
],
[
"X64.AESCTR.va_wpCompute_aes_counter_loop_while",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AESCTR.va_code_aes_counter_loop_while",
"equation_X64.AESCTR.va_wp_aes_counter_loop_while",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"d1b8e4806db108890bcf3127bba498af"
],
[
"X64.AESCTR.va_wpProof_aes_counter_loop_while",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"5f8bd5003566620415868be0fc247673"
],
[
"X64.AESCTR.va_wpProof_aes_counter_loop_while",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"AES_s_pretyping_443f63aed29daed744644bd1799d3a91",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"eq2-interp", "equality_tok_AES_s.AES_128@tok",
"equality_tok_AES_s.AES_256@tok",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rdx@tok", "equation_Prims.eq2",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Types_s.quad32", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.AESCTR.aes_reqs",
"equation_X64.AESCTR.va_wpCompute_aes_counter_loop_while",
"equation_X64.AESCTR.va_wp_aes_counter_loop_while",
"equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Prims.equals",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"kinding_Words_s.four@tok", "lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"primitive_Prims.op_Equality",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESCTR.va_wpCompute_aes_counter_loop_while",
"typing_GHash.ghash_incremental0",
"typing_Types_s.reverse_bytes_quad32",
"typing_Workarounds.slice_work_around",
"typing_X64.Memory.buffer_as_seq",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_reg",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_tok_AES_s.AES_128@tok",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rdx@tok", "unit_typing"
],
0,
"160ac0c6fb146e5312a37ea0f6fab84f"
],
[
"X64.AESCTR.va_lemma_aes_counter_loop",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Words_s.nat32",
"refinement_interpretation_Tm_refine_40e17b118ab41a3ae8d523e19e589dde"
],
0,
"0d0241bd20f096dca5b3b38b80bb82aa"
],
[
"X64.AESCTR.va_lemma_aes_counter_loop",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Interop.Types.TUInt128",
"constructor_distinct_X64.Machine_s.Rax",
"disc_equation_X64.Machine_s.Rsp", "eq2-interp",
"equality_tok_Interop.Types.TUInt128@tok",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R8@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rdx@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_Arch.Types.add_wrap_quad32", "equation_GCTR.gctr_partial",
"equation_GCTR_s.inc32", "equation_GHash.ghash_incremental0",
"equation_Prims.eq2", "equation_Prims.eqtype",
"equation_Prims.l_and", "equation_Prims.logical",
"equation_Prims.min", "equation_Prims.nat", "equation_Prims.squash",
"equation_Prop_s.prop0", "equation_Types_s.add_wrap",
"equation_Types_s.insert_nat32", "equation_Types_s.quad32",
"equation_Words.Four_s.four_insert",
"equation_Words.Four_s.four_reverse", "equation_Words_s.nat32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.AESCTR.aes_reqs", "equation_X64.Machine_s.xmm",
"equation_X64.Memory.base_typ_as_vale_type",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_if",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.validDstAddrs128",
"equation_X64.Vale.Decls.validSrcAddrs128",
"equation_X64.Vale.QuickCodes.range1",
"equation_X64.Vale.State.state_eq",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Words_s.nat32", "int_inversion", "int_typing",
"interpretation_Tm_abs_f6f0cecc93a7c8177ef813c15eb178e4",
"l_and-interp", "lemma_Arch.Types.lemma_reverse_bytes_quad32",
"lemma_Arch.Types.lemma_reverse_reverse_bytes_nat32",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_X64.Memory.buffer_length_buffer_as_seq",
"lemma_X64.Memory.modifies_refl",
"lemma_X64.Vale.QuickCodes.lemma_label_bool",
"lemma_X64.Vale.Regs.lemma_equal_intro",
"lemma_X64.Vale.Xmms.lemma_equal_intro",
"primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "proj_equation_Words_s.Mkfour_hi2",
"proj_equation_Words_s.Mkfour_hi3",
"proj_equation_Words_s.Mkfour_lo0",
"proj_equation_Words_s.Mkfour_lo1",
"proj_equation_X64.Machine_s.OReg_r",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_1581adb482c799e9ba4d4a9e29e70668",
"refinement_interpretation_Tm_refine_2a09f2450e26fe8d9312d402cf7d7936",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_599e7a30819c32943c9ca3ec80925b1f",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_f3b36da01e290014f597f7e15fd42343",
"refinement_kinding_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"string_typing", "typing_FStar.Seq.Base.empty",
"typing_GCTR.gctr_partial", "typing_GCTR_s.inc32",
"typing_Prims.eq2", "typing_Types_s.add_wrap",
"typing_Types_s.reverse_bytes_nat32",
"typing_Types_s.reverse_bytes_quad32",
"typing_Words_s.__proj__Mkfour__item__hi2",
"typing_Words_s.__proj__Mkfour__item__hi3",
"typing_Words_s.__proj__Mkfour__item__lo0",
"typing_Workarounds.slice_work_around",
"typing_X64.CPU_Features_s.pclmulqdq_enabled",
"typing_X64.Memory.base_typ_as_vale_type",
"typing_X64.Memory.buffer_addr", "typing_X64.Memory.buffer_as_seq",
"typing_X64.Memory.loc_buffer", "typing_X64.Memory.modifies",
"typing_X64.Vale.Decls.validSrcAddrs128",
"typing_X64.Vale.QuickCodes.label",
"typing_X64.Vale.QuickCodes.range1", "typing_X64.Vale.Regs.eta_sel",
"typing_X64.Vale.Regs.sel",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.eta_sel", "typing_X64.Vale.Xmms.sel",
"typing_tok_Interop.Types.TUInt128@tok",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R8@tok", "typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rdx@tok",
"typing_tok_X64.Machine_s.Secret@tok", "unit_inversion",
"unit_typing"
],
0,
"6f3482f052b2d531233218a9359d8622"
],
[
"X64.AESCTR.va_wp_aes_counter_loop",
1,
1,
0,
[ "@query" ],
0,
"59a56cec5cea83d3c9a9389d81d77bfb"
],
[
"X64.AESCTR.va_wpMonotone_aes_counter_loop",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"data_typing_intro_X64.Vale.State.Mkstate@tok",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok", "equation_Types_s.quad32",
"equation_Words_s.nat32",
"equation_X64.AESCTR.va_wp_aes_counter_loop",
"equation_X64.Machine_s.xmm", "equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"typing_X64.Vale.Decls.va_upd_flags",
"typing_X64.Vale.Decls.va_upd_mem",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__memTaint",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__stack",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.State.update_xmm", "typing_X64.Vale.Xmms.upd",
"typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok", "unit_typing"
],
0,
"b2b33a3b1534a2b3cf951d2069f8eb48"
],
[
"X64.AESCTR.va_wpCompute_aes_counter_loop",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "eq2-interp",
"equation_X64.AESCTR.va_wp_aes_counter_loop",
"equation_X64.Vale.Decls.va_require_total",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"eabb2da120128948eb0d20be477c112e"
],
[
"X64.AESCTR.va_wpProof_aes_counter_loop",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"4e3236a3e75344a1d97664a46e85597e"
],
[
"X64.AESCTR.va_wpProof_aes_counter_loop",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"AES_s_pretyping_443f63aed29daed744644bd1799d3a91",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc", "bool_inversion",
"constructor_distinct_AES_s.AES_128", "eq2-interp",
"equality_tok_AES_s.AES_128@tok", "equality_tok_AES_s.AES_256@tok",
"equality_tok_X64.Machine_s.R10@tok",
"equality_tok_X64.Machine_s.R12@tok",
"equality_tok_X64.Machine_s.R9@tok",
"equality_tok_X64.Machine_s.Rax@tok",
"equality_tok_X64.Machine_s.Rdi@tok",
"equality_tok_X64.Machine_s.Rdx@tok", "equation_AES_s.is_aes_key_LE",
"equation_Prims.nat", "equation_Words_s.nat32",
"equation_X64.AESCTR.aes_reqs",
"equation_X64.AESCTR.va_wpCompute_aes_counter_loop",
"equation_X64.AESCTR.va_wp_aes_counter_loop",
"equation_X64.Machine_s.xmm",
"equation_X64.Vale.Decls.va_ensure_total",
"equation_X64.Vale.Decls.va_require_total",
"equation_X64.Vale.Decls.va_state_eq",
"equation_X64.Vale.Decls.va_upd_flags",
"equation_X64.Vale.Decls.va_upd_mem",
"equation_X64.Vale.Decls.va_upd_ok",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_upd_xmm",
"equation_X64.Vale.QuickCode.t_ensure",
"equation_X64.Vale.State.state_eq",
"equation_X64.Vale.State.update_reg",
"equation_X64.Vale.State.update_xmm",
"fuel_guarded_inversion_X64.Vale.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Words_s.nat32", "int_typing",
"lemma_X64.Vale.Regs.lemma_equal_elim",
"lemma_X64.Vale.Xmms.lemma_equal_elim",
"primitive_Prims.op_Equality",
"proj_equation_X64.Vale.State.Mkstate_flags",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"proj_equation_X64.Vale.State.Mkstate_ok",
"proj_equation_X64.Vale.State.Mkstate_regs",
"proj_equation_X64.Vale.State.Mkstate_stack",
"proj_equation_X64.Vale.State.Mkstate_xmms",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_X64.Vale.State.Mkstate_flags",
"projection_inverse_X64.Vale.State.Mkstate_mem",
"projection_inverse_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_X64.Vale.State.Mkstate_ok",
"projection_inverse_X64.Vale.State.Mkstate_regs",
"projection_inverse_X64.Vale.State.Mkstate_stack",
"projection_inverse_X64.Vale.State.Mkstate_xmms",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.AESCTR.va_wpCompute_aes_counter_loop",
"typing_FStar.Seq.Base.length", "typing_X64.Vale.Decls.va_upd_ok",
"typing_X64.Vale.Decls.va_upd_xmm", "typing_X64.Vale.Regs.sel",
"typing_X64.Vale.Regs.upd",
"typing_X64.Vale.State.__proj__Mkstate__item__flags",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.__proj__Mkstate__item__ok",
"typing_X64.Vale.State.__proj__Mkstate__item__regs",
"typing_X64.Vale.State.__proj__Mkstate__item__xmms",
"typing_X64.Vale.Xmms.sel", "typing_X64.Vale.Xmms.upd",
"typing_tok_AES_s.AES_128@tok", "typing_tok_X64.Machine_s.R10@tok",
"typing_tok_X64.Machine_s.R12@tok",
"typing_tok_X64.Machine_s.R9@tok",
"typing_tok_X64.Machine_s.Rax@tok",
"typing_tok_X64.Machine_s.Rdi@tok",
"typing_tok_X64.Machine_s.Rdx@tok", "unit_typing"
],
0,
"a13f77cc665492ea2232bf60aec26bb6"
]
]
]
Computing file changes ...
