Revision 059787e63538941130606248805cab290fdbc5d7 authored by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC, committed by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC
1 parent 03f1e46
Vale.X64.Machine_Semantics_s.fst.hints
[
"�\u0004����#E�'S�S(6�",
[
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateXor64__item___0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateXor64",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_b130da2079b7fa62c26741e2adf7f0b6"
],
0,
"8811f44f83c6c3bca8ff7a33f682badc"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotatePxor__item___0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotatePxor",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_1f3942d454de893b05458ec4d1c706ea"
],
0,
"68d59f14ef0269acbec4f838ce09f037"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateVPxor__item___0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateVPxor",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_1216058de9517c69bc27db9254c96884"
],
0,
"69c8815aa543c300484881cf82f759d1"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateGhost__item___0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateGhost",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_88de194ba1a429314be6d962ee8dcd55"
],
0,
"e79738e758783c0b47cb02b5844415a3"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateComment__item__s",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateComment",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_a397e1de1afa063619902744449c5e04"
],
0,
"4c668c1335013a1a881391cd913e1190"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateLargeComment__item__s",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateLargeComment",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_9dd9fe06365981e05262991b18115375"
],
0,
"d405de7fd57adc4bdef74288e2e61725"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateNewline__item___0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateNewline",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_307e8b79480c21c30833ffd526d922ce"
],
0,
"6fc212890ed1a1677d4969d232b50a46"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateSpace__item__n",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateSpace",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_43c2b9cb91b9ab74fb17d37cea025163"
],
0,
"975f7adef5184e1a65c6c2db7494bacf"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateMovbe64__item___0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateMovbe64",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_61aae70ccfd51a81499c7f591b806638"
],
0,
"3d37f7ae01042491518ede1ea0a4e252"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateMov64__item___0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateMov64",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_a8abe1e6a958f78b4aac201ed11608cc"
],
0,
"b275c082a9ff5e07cff142b4308e02f3"
],
[
"Vale.X64.Machine_Semantics_s.get_fst_ocmp",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Bytes_Code_s.OEq",
"disc_equation_Vale.X64.Bytes_Code_s.OGe",
"disc_equation_Vale.X64.Bytes_Code_s.OGt",
"disc_equation_Vale.X64.Bytes_Code_s.OLe",
"disc_equation_Vale.X64.Bytes_Code_s.OLt",
"disc_equation_Vale.X64.Bytes_Code_s.ONe", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"aa99640bee8c234e6121578040284d13"
],
[
"Vale.X64.Machine_Semantics_s.get_snd_ocmp",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Bytes_Code_s.OEq",
"disc_equation_Vale.X64.Bytes_Code_s.OGe",
"disc_equation_Vale.X64.Bytes_Code_s.OGt",
"disc_equation_Vale.X64.Bytes_Code_s.OLe",
"disc_equation_Vale.X64.Bytes_Code_s.OLt",
"disc_equation_Vale.X64.Bytes_Code_s.ONe", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"dc9af609a79dc3e1527795801196c134"
],
[
"Vale.X64.Machine_Semantics_s.eval_reg_64",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"0e25c8cbcd25e53637dadafff2db0bcc"
],
[
"Vale.X64.Machine_Semantics_s.eval_reg_xmm",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_xmm",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"b7487cdc0ab965f762a9a37f9f256ac3"
],
[
"Vale.X64.Machine_Semantics_s.eval_maddr",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MConst",
"disc_equation_Vale.X64.Machine_s.MIndex",
"disc_equation_Vale.X64.Machine_s.MReg",
"fuel_guarded_inversion_Vale.X64.Machine_s.maddr"
],
0,
"fbb90c6b4fd6b6c0198c58c51b5b3a78"
],
[
"Vale.X64.Machine_Semantics_s.eval_operand",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"0cfae1a004f4a4a0bcaa8c99aa17ebce"
],
[
"Vale.X64.Machine_Semantics_s.eval_mov128_op",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"c6a5ca17ce2bcd442681171fe2bf2aeb"
],
[
"Vale.X64.Machine_Semantics_s.eval_ocmp",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Bytes_Code_s.OEq",
"disc_equation_Vale.X64.Bytes_Code_s.OGe",
"disc_equation_Vale.X64.Bytes_Code_s.OGt",
"disc_equation_Vale.X64.Bytes_Code_s.OLe",
"disc_equation_Vale.X64.Bytes_Code_s.OLt",
"disc_equation_Vale.X64.Bytes_Code_s.ONe", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"22d9063c8880667ec66648d684346b93"
],
[
"Vale.X64.Machine_Semantics_s.update_reg'",
1,
1,
0,
[
"@query", "assumption_Vale.X64.Machine_s.reg__uu___haseq",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0"
],
0,
"8234b42d4fc0bd40fd95612789f1febf"
],
[
"Vale.X64.Machine_Semantics_s.update_reg_64'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"916275c914ff84b85ec725e3e7450fa2"
],
[
"Vale.X64.Machine_Semantics_s.update_reg_xmm'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_xmm",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"48d1d9b9c9ce63c09f4ecf52fe16b0e0"
],
[
"Vale.X64.Machine_Semantics_s.match_n",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"binder_x_ae567c2fb75be05905677af440075565_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.X64.Machine_s.Public@tok", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_tok_Vale.X64.Machine_s.Public@tok",
"well-founded-ordering-on-nat"
],
0,
"6840e1b66c97d9e37a0c4d0662af863a"
],
[
"Vale.X64.Machine_Semantics_s.update_n",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"binder_x_ae567c2fb75be05905677af440075565_0",
"binder_x_b2ecc36deaf346c775ae2b728a51b51e_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_d3cd8a6631433ad48d6b3e9c57c54ea1_2",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Arch.HeapTypes_s.memTaint_t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "int_inversion", "int_typing",
"kinding_Vale.Arch.HeapTypes_s.taint@tok",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_SelUpd1",
"lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0030c490ddf8a8ae33d539152b909139",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_742a75c94d067ae9ad1d95ebb6c84de8",
"refinement_interpretation_Tm_refine_c2c488db3214c38826155caf10d30036",
"typing_FStar.Map.domain", "typing_FStar.Map.upd",
"typing_FStar.Set.complement", "typing_FStar.Set.empty",
"typing_Vale.X64.Machine_Semantics_s.update_n",
"typing_tok_Vale.Arch.HeapTypes_s.Public@tok",
"well-founded-ordering-on-nat"
],
0,
"e96bbc78a72915b6788edfa221d95d1d"
],
[
"Vale.X64.Machine_Semantics_s.lemma_is_machine_heap_update64",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Map_interpretation_Tm_arrow_b19283e90b47034162373413c6a19933",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Vale.Arch.MachineHeap_s.is_machine_heap_update",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Arch.MachineHeap_s.update_heap64_def",
"equation_Vale.Arch.MachineHeap_s.valid_addr",
"equation_Vale.Def.Words.Two_s.nat_to_two",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_FStar.Map.upd",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Arch.MachineHeap_s.update_heap64",
"function_token_typing_Vale.Arch.MachineHeap_s.valid_addr64",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_1eab5700ef81b3c102d114cb086eb6dc",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_singleton",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"proj_equation_Vale.Def.Words_s.Mktwo_hi",
"proj_equation_Vale.Def.Words_s.Mktwo_lo",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mktwo_hi",
"projection_inverse_Vale.Def.Words_s.Mktwo_lo",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap64_def",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.upd", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_Prims.pow2", "typing_Vale.Arch.MachineHeap_s.update_heap64",
"typing_Vale.Arch.MachineHeap_s.valid_addr",
"typing_Vale.Def.Words.Four_s.nat_to_four",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1"
],
0,
"882f66a1feec6cf8d564e11f7e413153"
],
[
"Vale.X64.Machine_Semantics_s.update_mem_and_taint",
1,
1,
0,
[
"@query",
"lemma_Vale.X64.Machine_Semantics_s.lemma_is_machine_heap_update64",
"projection_inverse_BoxBool_proj_0",
"typing_Vale.Arch.Heap.heap_get",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap"
],
0,
"54c40564f351459866adf12fe9e85265"
],
[
"Vale.X64.Machine_Semantics_s.lemma_is_machine_heap_update128",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Map_interpretation_Tm_arrow_b19283e90b47034162373413c6a19933",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"equation_Prims.nat",
"equation_Vale.Arch.MachineHeap_s.is_machine_heap_update",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Arch.MachineHeap_s.update_heap128_def",
"equation_Vale.Arch.MachineHeap_s.update_heap32_def",
"equation_Vale.Arch.MachineHeap_s.valid_addr",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_FStar.Map.upd",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Arch.MachineHeap_s.update_heap128",
"function_token_typing_Vale.Arch.MachineHeap_s.update_heap32",
"function_token_typing_Vale.Arch.MachineHeap_s.valid_addr128",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing",
"interpretation_Tm_abs_14d403333eed8abd9b38f58babfc702d",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro", "lemma_FStar.Set.mem_singleton",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_kinding_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap128_def",
"token_correspondence_Vale.Arch.MachineHeap_s.update_heap32_def",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.upd", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_Vale.Arch.MachineHeap_s.update_heap128",
"typing_Vale.Arch.MachineHeap_s.update_heap32",
"typing_Vale.Arch.MachineHeap_s.valid_addr",
"typing_Vale.Def.Words.Four_s.nat_to_four",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi2",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__hi3",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo1"
],
0,
"85c76196eb52b378f5eda707adf9dfc7"
],
[
"Vale.X64.Machine_Semantics_s.update_mem128_and_taint",
1,
1,
0,
[
"@query",
"lemma_Vale.X64.Machine_Semantics_s.lemma_is_machine_heap_update128",
"projection_inverse_BoxBool_proj_0",
"typing_Vale.Arch.Heap.heap_get",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap"
],
0,
"d5647401645c21bc998f46e98fa68bba"
],
[
"Vale.X64.Machine_Semantics_s.valid_src_operand",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"d8d2f995de7885f668d041e344f617d5"
],
[
"Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"f809c58ce864b634c1f3650a57d970f3"
],
[
"Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"d93f9dcc956aad22047f499f59a8fda6"
],
[
"Vale.X64.Machine_Semantics_s.valid_ocmp",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Bytes_Code_s.OEq",
"disc_equation_Vale.X64.Bytes_Code_s.OGe",
"disc_equation_Vale.X64.Bytes_Code_s.OGt",
"disc_equation_Vale.X64.Bytes_Code_s.OLe",
"disc_equation_Vale.X64.Bytes_Code_s.OLt",
"disc_equation_Vale.X64.Bytes_Code_s.ONe",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp"
],
0,
"65998283daeab60fd50a3ec908eeb081"
],
[
"Vale.X64.Machine_Semantics_s.valid_dst_operand64",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"399843bd758a1c146f866e9711ddc7e4"
],
[
"Vale.X64.Machine_Semantics_s.valid_dst_operand128",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"9c9ea008864b3c4a2e01bd458f90f771"
],
[
"Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags''",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"74785b024b4505a6a597501498256fbb"
],
[
"Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags''",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"9a95142b06fc6bd971cda24b4bd30e5a"
],
[
"Vale.X64.Machine_Semantics_s.update_rsp'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"c5af83451223a479c9a94bd8e2578e0a"
],
[
"Vale.X64.Machine_Semantics_s.update_cf'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144",
"equation_FStar.FunctionalExtensionality.feq",
"equation_Vale.X64.Machine_Semantics_s.cf",
"equation_Vale.X64.Machine_s.flag", "int_typing",
"interpretation_Tm_abs_1abb9d76d736bf6d3482913e489aefa3",
"interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
"refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
"typing_Tm_abs_1abb9d76d736bf6d3482913e489aefa3",
"typing_Tm_abs_f086d77986b470aab4bfebc171e6c366"
],
0,
"1bc7599bf2fa4b4b4f31ee83f5b5b260"
],
[
"Vale.X64.Machine_Semantics_s.update_of'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144",
"equation_FStar.FunctionalExtensionality.feq",
"equation_Vale.X64.Machine_Semantics_s.overflow",
"equation_Vale.X64.Machine_s.flag", "int_typing",
"interpretation_Tm_abs_93c792d4b39973d40853929beafbfdcb",
"interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
"refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
"typing_Tm_abs_93c792d4b39973d40853929beafbfdcb",
"typing_Tm_abs_f086d77986b470aab4bfebc171e6c366"
],
0,
"76dacb5e784712b9c7cdec6cc814a8cf"
],
[
"Vale.X64.Machine_Semantics_s.try_option",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"lemma_FStar.Pervasives.invertOption",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some"
],
0,
"5862b6fc6d9c47dd8fe8bd496c156c0d"
],
[
"Vale.X64.Machine_Semantics_s.bind_option",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"lemma_FStar.Pervasives.invertOption",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some"
],
0,
"a789d399e48c56587a7e6b13200280af"
],
[
"Vale.X64.Machine_Semantics_s.operand_obs",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"78be7bd341833c3ac4a7810647d0abc0"
],
[
"Vale.X64.Machine_Semantics_s.operand_obs128",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"a2a832e7f514755b27507148f7d824b6"
],
[
"Vale.X64.Machine_Semantics_s.obs_operand_explicit",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Instruction_s.IOp64",
"disc_equation_Vale.X64.Instruction_s.IOpXmm",
"equation_Vale.X64.Instruction_s.instr_operand_t",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit",
"projection_inverse_BoxBool_proj_0"
],
0,
"6f061d934d14c1ca6ee4983210582adb"
],
[
"Vale.X64.Machine_Semantics_s.obs_operand_implicit",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Instruction_s.IOp64One",
"disc_equation_Vale.X64.Instruction_s.IOpFlagsCf",
"disc_equation_Vale.X64.Instruction_s.IOpFlagsOf",
"disc_equation_Vale.X64.Instruction_s.IOpXmmOne",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit"
],
0,
"fbf88e52e29e5558d8a3ab77d4a96362"
],
[
"Vale.X64.Machine_Semantics_s.obs_args",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@query", "binder_x_5b8a55910a662c783b1ed3212549410e_0",
"constructor_distinct_Prims.Cons",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"subterm_ordering_Prims.Cons"
],
0,
"ce41fd3b8aa766d96261554230e9a186"
],
[
"Vale.X64.Machine_Semantics_s.obs_inouts",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@query",
"Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6",
"binder_x_5b8a55910a662c783b1ed3212549410e_1",
"binder_x_67735fae8b4e79dde4eed727828e245d_2",
"binder_x_9480187c8e85713ad9eae72e33c57410_0",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"data_typing_intro_Vale.X64.Instruction_s.Out@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"subterm_ordering_Prims.Cons"
],
0,
"fb29165bcee3b6998aa065e493028230"
],
[
"Vale.X64.Machine_Semantics_s.ins_obs",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Bytes_Code_s.Alloc",
"disc_equation_Vale.X64.Bytes_Code_s.Dealloc",
"disc_equation_Vale.X64.Bytes_Code_s.Instr",
"disc_equation_Vale.X64.Bytes_Code_s.Noop",
"disc_equation_Vale.X64.Bytes_Code_s.Pop",
"disc_equation_Vale.X64.Bytes_Code_s.Push",
"equation_Vale.X64.Machine_Semantics_s.ins",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.instruction_t"
],
0,
"2d4fd8617522ed9ccc0bc5e812cb4322"
],
[
"Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Instruction_s.IOp64",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpXmm",
"disc_equation_Vale.X64.Instruction_s.IOp64",
"disc_equation_Vale.X64.Instruction_s.IOpXmm",
"equation_Vale.X64.Instruction_s.instr_operand_t",
"equation_Vale.X64.Instruction_s.instr_val_t",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0"
],
0,
"5475b5791fe694f0f28af967bb434ffb"
],
[
"Vale.X64.Machine_Semantics_s.instr_eval_operand_implicit",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Instruction_s.IOp64One",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"constructor_distinct_Vale.X64.Instruction_s.IOpXmmOne",
"disc_equation_Vale.X64.Instruction_s.IOp64One",
"disc_equation_Vale.X64.Instruction_s.IOpFlagsCf",
"disc_equation_Vale.X64.Instruction_s.IOpFlagsOf",
"disc_equation_Vale.X64.Instruction_s.IOpXmmOne",
"equation_Vale.X64.Instruction_s.instr_val_t",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Instruction_s.IOp64One_o",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"projection_inverse_Vale.X64.Instruction_s.IOpXmmOne_o",
"typing_Vale.X64.Machine_Semantics_s.eval_mov128_op",
"typing_Vale.X64.Machine_Semantics_s.eval_operand"
],
0,
"8133b90d619d476d07971361b1ce637c"
],
[
"Vale.X64.Machine_Semantics_s.instr_apply_eval_args",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@query", "binder_x_38287ca2033f50691479ff837e9de132_2",
"binder_x_5b8a55910a662c783b1ed3212549410e_1",
"binder_x_9480187c8e85713ad9eae72e33c57410_0",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"subterm_ordering_Prims.Cons"
],
0,
"71514cabfdb5be6c8e87fd31a23b1b14"
],
[
"Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@query",
"Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6",
"binder_x_093c08543626f27b65f30658d7fc39bc_4",
"binder_x_5b8a55910a662c783b1ed3212549410e_2",
"binder_x_9480187c8e85713ad9eae72e33c57410_0",
"binder_x_9480187c8e85713ad9eae72e33c57410_1",
"binder_x_f5c27ac55c99c39df8fbe4adb077bc73_3",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"constructor_distinct_Vale.X64.Instruction_s.InOut",
"constructor_distinct_Vale.X64.Instruction_s.Out",
"data_elim_Prims.Cons",
"data_typing_intro_Vale.X64.Instruction_s.Out@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"disc_equation_Vale.X64.Instruction_s.InOut",
"disc_equation_Vale.X64.Instruction_s.Out",
"equality_tok_Vale.X64.Instruction_s.InOut@tok",
"equality_tok_Vale.X64.Instruction_s.Out@tok",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_inout",
"kinding_Vale.X64.Instruction_s.instr_operand@tok",
"kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_Prims.Cons_hd",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"subterm_ordering_Prims.Cons",
"typing_FStar.Pervasives.Native.__proj__Mktuple2__item___1"
],
0,
"23ddd9fbbbfcfd9b0a088b9127199e0b"
],
[
"Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_16a847f7ad5358b11ce3fc0b9b7c693c_0",
"binder_x_2e7889c48d02ab427547828997693498_2",
"binder_x_f15a914b50f33f676dd71c15920680b1_1",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOp64",
"disc_equation_Vale.X64.Instruction_s.IOpXmm",
"equation_Vale.X64.Instruction_s.instr_operand_t",
"equation_Vale.X64.Instruction_s.instr_val_t",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0"
],
0,
"9325d8bc68cc3a8df54e750e9b958991"
],
[
"Vale.X64.Machine_Semantics_s.instr_write_output_implicit",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_7199321999326f8357c41289e834c92f_1",
"binder_x_dfa9c2e22fe11011bf212d55e07ed9db_0",
"constructor_distinct_Vale.X64.Instruction_s.IOp64One",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"constructor_distinct_Vale.X64.Instruction_s.IOpXmmOne",
"disc_equation_Vale.X64.Instruction_s.IOp64One",
"disc_equation_Vale.X64.Instruction_s.IOpFlagsCf",
"disc_equation_Vale.X64.Instruction_s.IOpFlagsOf",
"disc_equation_Vale.X64.Instruction_s.IOpXmmOne",
"equation_Vale.X64.Instruction_s.instr_val_t",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Instruction_s.IOp64One_o",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"projection_inverse_Vale.X64.Instruction_s.IOpXmmOne_o"
],
0,
"525dbbba6627d7ef489ec4c5cd1620c8"
],
[
"Vale.X64.Machine_Semantics_s.instr_write_outputs",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@query",
"Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6",
"binder_x_44c6303725e907c3759d9004241619c7_2",
"binder_x_5b8a55910a662c783b1ed3212549410e_1",
"binder_x_9480187c8e85713ad9eae72e33c57410_0",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"data_typing_intro_Vale.X64.Instruction_s.Out@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_Vale.X64.Instruction_s.instr_val_t",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit",
"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_Prims.Nil_a",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"subterm_ordering_Prims.Cons", "unit_typing"
],
0,
"a9b0c8e5825833bfa98a56aa97de0586"
],
[
"Vale.X64.Machine_Semantics_s.eval_instr",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@query", "disc_equation_Vale.X64.Instruction_s.HavocFlags",
"disc_equation_Vale.X64.Instruction_s.PreserveFlags",
"equation_Vale.X64.Instruction_s.instr_eval_t",
"equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.Instruction_s.flag_havoc",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_args",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"typing_Vale.X64.Instruction_s.instr_eval"
],
0,
"0e0470316af6bc272304fb65575edc56"
],
[
"Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Bytes_Code_s.Alloc",
"disc_equation_Vale.X64.Bytes_Code_s.Dealloc",
"disc_equation_Vale.X64.Bytes_Code_s.Instr",
"disc_equation_Vale.X64.Bytes_Code_s.Noop",
"disc_equation_Vale.X64.Bytes_Code_s.Pop",
"disc_equation_Vale.X64.Bytes_Code_s.Push", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.instruction_t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"9672b78f3a550e293d81f6941f924ddf"
],
[
"Vale.X64.Machine_Semantics_s.machine_eval_code",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"binder_x_97ef5ff619e486c846fe112d821f649f_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"disc_equation_Vale.X64.Machine_s.Block",
"disc_equation_Vale.X64.Machine_s.IfElse",
"disc_equation_Vale.X64.Machine_s.Ins",
"disc_equation_Vale.X64.Machine_s.While",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.codes",
"fuel_guarded_inversion_Vale.X64.Machine_s.precode", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Vale.X64.Machine_s.Block",
"subterm_ordering_Vale.X64.Machine_s.IfElse",
"subterm_ordering_Vale.X64.Machine_s.While",
"typing_tok_Prims.LexTop@tok"
],
0,
"9270848ae90df7c0e35c1f8be8408b03"
],
[
"Vale.X64.Machine_Semantics_s.machine_eval_code",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"binder_x_69b3af25a4334715774d1242034fc6f2_0",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.X64.Bytes_Code_s.codes_t",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.codes",
"fuel_guarded_inversion_Prims.list", "int_inversion",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Prims.Cons",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_tok_Prims.LexTop@tok"
],
0,
"fb49b3f16e98243c82b9a62920b27f3d"
],
[
"Vale.X64.Machine_Semantics_s.machine_eval_code",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"int_inversion", "int_typing",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_tok_Prims.LexTop@tok", "well-founded-ordering-on-nat"
],
0,
"86c1f177e699d8d68ba87cff19125768"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateXor64__item___0",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateXor64",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_b130da2079b7fa62c26741e2adf7f0b6"
],
0,
"95cfab4fc71a103498b86f7359df6c21"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotatePxor__item___0",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotatePxor",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_1f3942d454de893b05458ec4d1c706ea"
],
0,
"76cedfe70c76531de077b0cab7f62797"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateVPxor__item___0",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateVPxor",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_1216058de9517c69bc27db9254c96884"
],
0,
"5df675c9ead354f334e12bdde4fd68f9"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateGhost__item___0",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateGhost",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_88de194ba1a429314be6d962ee8dcd55"
],
0,
"9d54aee8aaf379b226440c4d4a9972fb"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateComment__item__s",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateComment",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_a397e1de1afa063619902744449c5e04"
],
0,
"323632076b1c1e178c98eddc7b6ef45f"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateLargeComment__item__s",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateLargeComment",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_9dd9fe06365981e05262991b18115375"
],
0,
"417558a903804e63f7ec7338cdd9f491"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateNewline__item___0",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateNewline",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_307e8b79480c21c30833ffd526d922ce"
],
0,
"f515ce8662603b02c6285224bcca34b1"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateSpace__item__n",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateSpace",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_43c2b9cb91b9ab74fb17d37cea025163"
],
0,
"3865811195d9156a87041ad5599a2ee9"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateMovbe64__item___0",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateMovbe64",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_61aae70ccfd51a81499c7f591b806638"
],
0,
"e98313d0df090df624e0f2ed3e93f810"
],
[
"Vale.X64.Machine_Semantics_s.__proj__AnnotateMov64__item___0",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_Semantics_s.AnnotateMov64",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_a8abe1e6a958f78b4aac201ed11608cc"
],
0,
"4726022b98bf26d589ce2cdfdf4a0f23"
],
[
"Vale.X64.Machine_Semantics_s.get_fst_ocmp",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Bytes_Code_s.OEq",
"disc_equation_Vale.X64.Bytes_Code_s.OGe",
"disc_equation_Vale.X64.Bytes_Code_s.OGt",
"disc_equation_Vale.X64.Bytes_Code_s.OLe",
"disc_equation_Vale.X64.Bytes_Code_s.OLt",
"disc_equation_Vale.X64.Bytes_Code_s.ONe", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"4d72466fcc4eb176bcc6609cef1e18b5"
],
[
"Vale.X64.Machine_Semantics_s.get_fst_ocmp",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"13c492cbf6efa3a153617ab9ea864a40"
],
[
"Vale.X64.Machine_Semantics_s.get_snd_ocmp",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Bytes_Code_s.OEq",
"disc_equation_Vale.X64.Bytes_Code_s.OGe",
"disc_equation_Vale.X64.Bytes_Code_s.OGt",
"disc_equation_Vale.X64.Bytes_Code_s.OLe",
"disc_equation_Vale.X64.Bytes_Code_s.OLt",
"disc_equation_Vale.X64.Bytes_Code_s.ONe", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"9697633ae5473c7fb8f29439efa057cb"
],
[
"Vale.X64.Machine_Semantics_s.get_snd_ocmp",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"33cafce383725260b55ae34a453cca71"
],
[
"Vale.X64.Machine_Semantics_s.eval_reg_64",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"f2d712666a18a3d218129d3524109bb9"
],
[
"Vale.X64.Machine_Semantics_s.eval_reg_xmm",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_xmm",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"f93370cb8b147b7622f061f4a6fed1d8"
],
[
"Vale.X64.Machine_Semantics_s.eval_maddr",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.MConst",
"disc_equation_Vale.X64.Machine_s.MIndex",
"disc_equation_Vale.X64.Machine_s.MReg",
"fuel_guarded_inversion_Vale.X64.Machine_s.maddr"
],
0,
"b03126ef3a40eced06071561bf868c02"
],
[
"Vale.X64.Machine_Semantics_s.eval_operand",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"d4db4aaca96410d216b2ddaab0f40529"
],
[
"Vale.X64.Machine_Semantics_s.eval_mov128_op",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"95737cb6c291be3ce5cca0b8d79c0bf6"
],
[
"Vale.X64.Machine_Semantics_s.eval_ocmp",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Bytes_Code_s.OEq",
"disc_equation_Vale.X64.Bytes_Code_s.OGe",
"disc_equation_Vale.X64.Bytes_Code_s.OGt",
"disc_equation_Vale.X64.Bytes_Code_s.OLe",
"disc_equation_Vale.X64.Bytes_Code_s.OLt",
"disc_equation_Vale.X64.Bytes_Code_s.ONe", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"234a3dfa1dc71048f8a2c159d31d2157"
],
[
"Vale.X64.Machine_Semantics_s.update_reg'",
2,
1,
0,
[
"@query", "assumption_Vale.X64.Machine_s.reg__uu___haseq",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0"
],
0,
"cafbb47565123d31bb6559eaaeeaec49"
],
[
"Vale.X64.Machine_Semantics_s.update_reg_64'",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"ff589d560c4b054588b20abbdc954b14"
],
[
"Vale.X64.Machine_Semantics_s.update_reg_xmm'",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_xmm",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"2df64952c5e33933c316530194262949"
],
[
"Vale.X64.Machine_Semantics_s.match_n",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"binder_x_ae567c2fb75be05905677af440075565_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.X64.Machine_s.Public@tok", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_tok_Vale.X64.Machine_s.Public@tok",
"well-founded-ordering-on-nat"
],
0,
"7963d014cb6d108827e4129c5799f6a6"
],
[
"Vale.X64.Machine_Semantics_s.update_n",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"binder_x_ae567c2fb75be05905677af440075565_0",
"binder_x_b2ecc36deaf346c775ae2b728a51b51e_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_d3cd8a6631433ad48d6b3e9c57c54ea1_2",
"equality_tok_Prims.LexTop@tok",
"equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Arch.HeapTypes_s.memTaint_t",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "int_inversion", "int_typing",
"kinding_Vale.Arch.HeapTypes_s.taint@tok",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_SelUpd1",
"lemma_FStar.Map.lemma_SelUpd2", "lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_Negation", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0030c490ddf8a8ae33d539152b909139",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_742a75c94d067ae9ad1d95ebb6c84de8",
"refinement_interpretation_Tm_refine_c2c488db3214c38826155caf10d30036",
"typing_FStar.Map.domain", "typing_FStar.Map.upd",
"typing_FStar.Set.complement", "typing_FStar.Set.empty",
"typing_Vale.X64.Machine_Semantics_s.update_n",
"typing_tok_Vale.Arch.HeapTypes_s.Public@tok",
"well-founded-ordering-on-nat"
],
0,
"1cba19a2697ca18584e0046315e37753"
],
[
"Vale.X64.Machine_Semantics_s.update_mem_and_taint",
2,
1,
0,
[
"@query",
"lemma_Vale.X64.Machine_Semantics_s.lemma_is_machine_heap_update64",
"projection_inverse_BoxBool_proj_0",
"typing_Vale.Arch.Heap.heap_get",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap"
],
0,
"21bb4ba9199eb42f36db534eac7056cf"
],
[
"Vale.X64.Machine_Semantics_s.update_mem128_and_taint",
2,
1,
0,
[
"@query",
"lemma_Vale.X64.Machine_Semantics_s.lemma_is_machine_heap_update128",
"projection_inverse_BoxBool_proj_0",
"typing_Vale.Arch.Heap.heap_get",
"typing_Vale.X64.Machine_Semantics_s.__proj__Mkmachine_state__item__ms_heap"
],
0,
"87f7e2b9e27e5eb3c753fc7950e4d814"
],
[
"Vale.X64.Machine_Semantics_s.valid_src_operand",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"b1adfe9ad4338a7aa8b460fcaa988cc6"
],
[
"Vale.X64.Machine_Semantics_s.valid_src_operand64_and_taint",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"3403b408e3006cda95eeca5d432f6915"
],
[
"Vale.X64.Machine_Semantics_s.valid_src_operand128_and_taint",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"c027bfb92c9ee948d9c1731ef61a533d"
],
[
"Vale.X64.Machine_Semantics_s.valid_ocmp",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Bytes_Code_s.OEq",
"disc_equation_Vale.X64.Bytes_Code_s.OGe",
"disc_equation_Vale.X64.Bytes_Code_s.OGt",
"disc_equation_Vale.X64.Bytes_Code_s.OLe",
"disc_equation_Vale.X64.Bytes_Code_s.OLt",
"disc_equation_Vale.X64.Bytes_Code_s.ONe",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.ocmp"
],
0,
"9dbddedf8e1691fc1dca52ce67fb9732"
],
[
"Vale.X64.Machine_Semantics_s.valid_dst_operand64",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"e75bbc19e477aa3a304b2f248af64f7a"
],
[
"Vale.X64.Machine_Semantics_s.valid_dst_operand128",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"e496854cb40f5852a3bbf0a9d132d9b0"
],
[
"Vale.X64.Machine_Semantics_s.update_operand64_preserve_flags''",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"61c89f1d60dceb1c56386ab80e294d55"
],
[
"Vale.X64.Machine_Semantics_s.update_operand128_preserve_flags''",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"1907eacf94382373073793ab4dd92702"
],
[
"Vale.X64.Machine_Semantics_s.update_rsp'",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_7d29e56e66c8277ffbad10980c3bdf4c",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"c949bb204953b9482a3e0062513ce4df"
],
[
"Vale.X64.Machine_Semantics_s.update_cf'",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144",
"equation_FStar.FunctionalExtensionality.feq",
"equation_Vale.X64.Machine_Semantics_s.cf",
"equation_Vale.X64.Machine_s.flag", "int_typing",
"interpretation_Tm_abs_1abb9d76d736bf6d3482913e489aefa3",
"interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
"refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
"typing_Tm_abs_1abb9d76d736bf6d3482913e489aefa3",
"typing_Tm_abs_f086d77986b470aab4bfebc171e6c366"
],
0,
"758095863c4f4a99ebd7cc2baebd5b24"
],
[
"Vale.X64.Machine_Semantics_s.update_of'",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_a7d5cc170be69663c495e8582d2bc62a",
"Prims_interpretation_Tm_arrow_2eaa01e78f73e9bab5d0955fc1a662da",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_59570c1b09fcfe77d38fb81f91091100",
"Vale.X64.Machine_Semantics_s_interpretation_Tm_arrow_6d1d81ae558d658d7d34082785eb5144",
"equation_FStar.FunctionalExtensionality.feq",
"equation_Vale.X64.Machine_Semantics_s.overflow",
"equation_Vale.X64.Machine_s.flag", "int_typing",
"interpretation_Tm_abs_93c792d4b39973d40853929beafbfdcb",
"interpretation_Tm_abs_f086d77986b470aab4bfebc171e6c366",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"primitive_Prims.op_Equality", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_72758763fd3a331db555502c82719e64",
"refinement_kinding_Tm_refine_72758763fd3a331db555502c82719e64",
"typing_Tm_abs_93c792d4b39973d40853929beafbfdcb",
"typing_Tm_abs_f086d77986b470aab4bfebc171e6c366"
],
0,
"4b1d85c00c8df5159412a0d0e2480165"
],
[
"Vale.X64.Machine_Semantics_s.try_option",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"lemma_FStar.Pervasives.invertOption",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some"
],
0,
"1c757e728bcc8020deac5bdb66ff6f6d"
],
[
"Vale.X64.Machine_Semantics_s.bind_option",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"lemma_FStar.Pervasives.invertOption",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some"
],
0,
"a7b09dcf85aeb69eec381cd14cf7d4bf"
],
[
"Vale.X64.Machine_Semantics_s.operand_obs",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.operand64",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"e904dbc8161fbbb3a355b6c5fc3005c7"
],
[
"Vale.X64.Machine_Semantics_s.operand_obs128",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OStack",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.X64.Machine_s.operand128",
"equation_Vale.X64.Machine_s.reg_xmm",
"fuel_guarded_inversion_Vale.X64.Machine_s.operand"
],
0,
"e2a6ef1b4ca378c57f21dbde99300539"
],
[
"Vale.X64.Machine_Semantics_s.obs_operand_explicit",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Instruction_s.IOp64",
"disc_equation_Vale.X64.Instruction_s.IOpXmm",
"equation_Vale.X64.Instruction_s.instr_operand_t",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit",
"projection_inverse_BoxBool_proj_0"
],
0,
"0793359224fba4fcb7afb43da27ae207"
],
[
"Vale.X64.Machine_Semantics_s.obs_operand_implicit",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Instruction_s.IOp64One",
"disc_equation_Vale.X64.Instruction_s.IOpFlagsCf",
"disc_equation_Vale.X64.Instruction_s.IOpFlagsOf",
"disc_equation_Vale.X64.Instruction_s.IOpXmmOne",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit"
],
0,
"3ba42314386e389d9d220c9cbaf17e05"
],
[
"Vale.X64.Machine_Semantics_s.obs_args",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@query", "binder_x_5b8a55910a662c783b1ed3212549410e_0",
"constructor_distinct_Prims.Cons",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"subterm_ordering_Prims.Cons"
],
0,
"b2f15eb0eef3c7b6bff349a0671f5fe7"
],
[
"Vale.X64.Machine_Semantics_s.obs_inouts",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@query",
"Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6",
"binder_x_5b8a55910a662c783b1ed3212549410e_1",
"binder_x_67735fae8b4e79dde4eed727828e245d_2",
"binder_x_9480187c8e85713ad9eae72e33c57410_0",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"data_typing_intro_Vale.X64.Instruction_s.Out@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"subterm_ordering_Prims.Cons"
],
0,
"9d4549e31fb213d042b6ceeee7b4bad6"
],
[
"Vale.X64.Machine_Semantics_s.ins_obs",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Bytes_Code_s.Alloc",
"disc_equation_Vale.X64.Bytes_Code_s.Dealloc",
"disc_equation_Vale.X64.Bytes_Code_s.Instr",
"disc_equation_Vale.X64.Bytes_Code_s.Noop",
"disc_equation_Vale.X64.Bytes_Code_s.Pop",
"disc_equation_Vale.X64.Bytes_Code_s.Push",
"equation_Vale.X64.Machine_Semantics_s.ins",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.instruction_t"
],
0,
"2505800298366c26400f08fa0ec1b618"
],
[
"Vale.X64.Machine_Semantics_s.instr_eval_operand_explicit",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Instruction_s.IOp64",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpXmm",
"disc_equation_Vale.X64.Instruction_s.IOp64",
"disc_equation_Vale.X64.Instruction_s.IOpXmm",
"equation_Vale.X64.Instruction_s.instr_operand_t",
"equation_Vale.X64.Instruction_s.instr_val_t",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0"
],
0,
"9874575b513c5f6decb7e10cb78a2d44"
],
[
"Vale.X64.Machine_Semantics_s.instr_eval_operand_implicit",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Instruction_s.IOp64One",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"constructor_distinct_Vale.X64.Instruction_s.IOpXmmOne",
"disc_equation_Vale.X64.Instruction_s.IOp64One",
"disc_equation_Vale.X64.Instruction_s.IOpFlagsCf",
"disc_equation_Vale.X64.Instruction_s.IOpFlagsOf",
"disc_equation_Vale.X64.Instruction_s.IOpXmmOne",
"equation_Vale.X64.Instruction_s.instr_val_t",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Instruction_s.IOp64One_o",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"projection_inverse_Vale.X64.Instruction_s.IOpXmmOne_o",
"typing_Vale.X64.Machine_Semantics_s.eval_mov128_op",
"typing_Vale.X64.Machine_Semantics_s.eval_operand"
],
0,
"595feb9faf62343875b99237dec7304d"
],
[
"Vale.X64.Machine_Semantics_s.instr_apply_eval_args",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"@query", "binder_x_38287ca2033f50691479ff837e9de132_2",
"binder_x_5b8a55910a662c783b1ed3212549410e_1",
"binder_x_9480187c8e85713ad9eae72e33c57410_0",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_with_fuel_Vale.X64.Instruction_s.instr_args_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t_args.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"subterm_ordering_Prims.Cons"
],
0,
"032ee2e39ab72c7ede21043e102b6ba5"
],
[
"Vale.X64.Machine_Semantics_s.instr_apply_eval_inouts",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@query",
"Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6",
"binder_x_093c08543626f27b65f30658d7fc39bc_4",
"binder_x_5b8a55910a662c783b1ed3212549410e_2",
"binder_x_9480187c8e85713ad9eae72e33c57410_0",
"binder_x_9480187c8e85713ad9eae72e33c57410_1",
"binder_x_f5c27ac55c99c39df8fbe4adb077bc73_3",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"constructor_distinct_Vale.X64.Instruction_s.InOut",
"constructor_distinct_Vale.X64.Instruction_s.Out",
"data_elim_Prims.Cons",
"data_typing_intro_Vale.X64.Instruction_s.Out@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"disc_equation_Vale.X64.Instruction_s.InOut",
"disc_equation_Vale.X64.Instruction_s.Out",
"equality_tok_Vale.X64.Instruction_s.InOut@tok",
"equality_tok_Vale.X64.Instruction_s.Out@tok",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_inout",
"kinding_Vale.X64.Instruction_s.instr_operand@tok",
"kinding_Vale.X64.Instruction_s.instr_operand_inout@tok",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_Prims.Cons_hd",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"subterm_ordering_Prims.Cons",
"typing_FStar.Pervasives.Native.__proj__Mktuple2__item___1"
],
0,
"a8c8b26e161dfa77577d92810405d2cf"
],
[
"Vale.X64.Machine_Semantics_s.instr_write_output_explicit",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOp64",
"disc_equation_Vale.X64.Instruction_s.IOpXmm",
"equation_Vale.X64.Instruction_s.instr_operand_t",
"equation_Vale.X64.Instruction_s.instr_val_t",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0"
],
0,
"9f19666551be023d2d934ba90fb7c2cc"
],
[
"Vale.X64.Machine_Semantics_s.instr_write_output_implicit",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Instruction_s.IOp64One",
"constructor_distinct_Vale.X64.Instruction_s.IOpIm",
"constructor_distinct_Vale.X64.Instruction_s.IOpXmmOne",
"disc_equation_Vale.X64.Instruction_s.IOp64One",
"disc_equation_Vale.X64.Instruction_s.IOpFlagsCf",
"disc_equation_Vale.X64.Instruction_s.IOpFlagsOf",
"disc_equation_Vale.X64.Instruction_s.IOpXmmOne",
"equation_Vale.X64.Instruction_s.instr_val_t",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Instruction_s.IOp64One_o",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"projection_inverse_Vale.X64.Instruction_s.IOpXmmOne_o"
],
0,
"5dbd155c88f0d05cc190cd5535b43168"
],
[
"Vale.X64.Machine_Semantics_s.instr_write_outputs",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@query",
"Vale.X64.Instruction_s_pretyping_2fb66fcb47c648644e76dfa1323a4ab6",
"binder_x_44c6303725e907c3759d9004241619c7_2",
"binder_x_5b8a55910a662c783b1ed3212549410e_1",
"binder_x_9480187c8e85713ad9eae72e33c57410_0",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Vale.X64.Instruction_s.IOpEx",
"data_typing_intro_Vale.X64.Instruction_s.Out@tok",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.X64.Instruction_s.IOpEx",
"disc_equation_Vale.X64.Instruction_s.IOpIm",
"equation_Vale.X64.Instruction_s.instr_out",
"equation_Vale.X64.Instruction_s.instr_val_t",
"equation_with_fuel_Vale.X64.Instruction_s.instr_operands_t.fuel_instrumented",
"equation_with_fuel_Vale.X64.Instruction_s.instr_ret_t.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_explicit",
"fuel_guarded_inversion_Vale.X64.Instruction_s.instr_operand_implicit",
"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_Prims.Nil_a",
"projection_inverse_Vale.X64.Instruction_s.IOpEx__0",
"projection_inverse_Vale.X64.Instruction_s.IOpIm__0",
"subterm_ordering_Prims.Cons", "unit_typing"
],
0,
"8fa23ddabeab32185276bdb465857818"
],
[
"Vale.X64.Machine_Semantics_s.eval_instr",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@fuel_irrelevance_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@query", "disc_equation_Vale.X64.Instruction_s.HavocFlags",
"disc_equation_Vale.X64.Instruction_s.PreserveFlags",
"equation_Vale.X64.Instruction_s.instr_eval_t",
"equation_with_fuel_Vale.X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"fuel_guarded_inversion_Vale.X64.Instruction_s.flag_havoc",
"fuel_guarded_inversion_Vale.X64.Machine_Semantics_s.machine_state",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_args",
"proj_equation_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_args",
"projection_inverse_Vale.X64.Instruction_s.InstrTypeRecord_outs",
"typing_Vale.X64.Instruction_s.instr_eval"
],
0,
"4c619d7d4d10912a7c87ef30052071e1"
],
[
"Vale.X64.Machine_Semantics_s.machine_eval_ins_st",
2,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Bytes_Code_s.Alloc",
"disc_equation_Vale.X64.Bytes_Code_s.Dealloc",
"disc_equation_Vale.X64.Bytes_Code_s.Instr",
"disc_equation_Vale.X64.Bytes_Code_s.Noop",
"disc_equation_Vale.X64.Bytes_Code_s.Pop",
"disc_equation_Vale.X64.Bytes_Code_s.Push", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.natN",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.X64.Bytes_Code_s.instruction_t",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"198751466ef87e586d53267f3b5cfb13"
],
[
"Vale.X64.Machine_Semantics_s.machine_eval_code",
4,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"binder_x_97ef5ff619e486c846fe112d821f649f_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"disc_equation_Vale.X64.Machine_s.Block",
"disc_equation_Vale.X64.Machine_s.IfElse",
"disc_equation_Vale.X64.Machine_s.Ins",
"disc_equation_Vale.X64.Machine_s.While",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.codes",
"fuel_guarded_inversion_Vale.X64.Machine_s.precode", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Vale.X64.Machine_s.Block",
"subterm_ordering_Vale.X64.Machine_s.IfElse",
"subterm_ordering_Vale.X64.Machine_s.While",
"typing_tok_Prims.LexTop@tok"
],
0,
"8aa356cbf629d0b570fe87783aef925b"
],
[
"Vale.X64.Machine_Semantics_s.machine_eval_code",
5,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"Vale.X64.Machine_Semantics_s_pretyping_8afd38cc1321157644dafce503e55d5a",
"binder_x_69b3af25a4334715774d1242034fc6f2_0",
"binder_x_8afd38cc1321157644dafce503e55d5a_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.X64.Bytes_Code_s.codes_t",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_Vale.X64.Machine_Semantics_s.codes",
"fuel_guarded_inversion_Prims.list", "int_inversion",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"subterm_ordering_Prims.Cons",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_tok_Prims.LexTop@tok"
],
0,
"8e59e8c8f450328c8124b59d224e2fb3"
],
[
"Vale.X64.Machine_Semantics_s.machine_eval_code",
6,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_e4836109f73687024ac3edd113084865",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"int_inversion", "int_typing",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Equality",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Pervasives.Native.uu___is_None",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_tok_Prims.LexTop@tok", "well-founded-ordering-on-nat"
],
0,
"d4e59bca58f47e6d6e58308e0c2bbd45"
]
]
]
Computing file changes ...
