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.Vale.Decls.fst.hints
[
"0;��=�X��W`4�KPO",
[
[
"X64.Vale.Decls.lemma_mul_in_bounds",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.mul_mod", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Words_s.nat64", "equation_Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.UInt.fits", "typing_FStar.UInt.mul_mod"
],
0,
"f06f861a1e69a231421768eb9c5c8741"
],
[
"X64.Vale.Decls.lemma_mul_nat",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"f8eeb68e469b82154c0e2bf37920cabc"
],
[
"X64.Vale.Decls.update_cf",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Prims.pos", "equation_Words_s.nat64",
"equation_Words_s.natN", "equation_X64.Bytes_Semantics_s.cf",
"equation_X64.Bytes_Semantics_s.overflow",
"equation_X64.Bytes_Semantics_s.update_cf_",
"equation_X64.Machine_s.int_to_nat64", "equation_X64.Vale.Decls.cf",
"equation_X64.Vale.Decls.overflow", "equation_X64.Vale.Lemmas.cf",
"equation_X64.Vale.Lemmas.overflow",
"equation_X64.Vale.Lemmas.update_cf",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1bc5c4f392722fe6a26189e86f17c270",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d309e8d463142b28bf2a4a24fcf82742",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Words_s.int_to_natN", "typing_X64.Vale.Lemmas.update_cf"
],
0,
"63a14446aef3ee12ae843512ff6c7ac9"
],
[
"X64.Vale.Decls.update_of",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"equation_Prims.nat", "equation_Prims.pos", "equation_Words_s.nat64",
"equation_Words_s.natN", "equation_X64.Bytes_Semantics_s.cf",
"equation_X64.Bytes_Semantics_s.overflow",
"equation_X64.Bytes_Semantics_s.update_of_",
"equation_X64.Machine_s.int_to_nat64", "equation_X64.Vale.Decls.cf",
"equation_X64.Vale.Decls.overflow", "equation_X64.Vale.Lemmas.cf",
"equation_X64.Vale.Lemmas.overflow",
"equation_X64.Vale.Lemmas.update_of",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1bc5c4f392722fe6a26189e86f17c270",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_feb4aba3c97fe87f182273d94c74cfa2",
"typing_Words_s.int_to_natN", "typing_X64.Vale.Decls.cf",
"typing_X64.Vale.Lemmas.update_of"
],
0,
"4615b46fd6056e8036c1c10462009023"
],
[
"X64.Vale.Decls.va_if",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"projection_inverse_BoxBool_proj_0"
],
0,
"3083e7942fc107435a29d93a476c4c93"
],
[
"X64.Vale.Decls.tainted_operand",
1,
2,
0,
[
"@query", "assumption_X64.Machine_s.maddr__uu___haseq",
"assumption_X64.Machine_s.reg__uu___haseq",
"assumption_X64.Machine_s.taint__uu___haseq"
],
0,
"3e72740719b38a97d439f4eb59ddb589"
],
[
"X64.Vale.Decls.__proj__TConst__item__n",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_X64.Vale.Decls.TConst",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_8eede0b6c514055f6927335ac482723b"
],
0,
"fdac318696b233e90a87f47a27d957bd"
],
[
"X64.Vale.Decls.__proj__TReg__item__r",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_X64.Vale.Decls.TReg",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_682f3ae59659a6bddfeeb83da8fe1944"
],
0,
"c6ca84b44fcd0225ceeaf1b376f2ca22"
],
[
"X64.Vale.Decls.__proj__TMem__item__m",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_X64.Vale.Decls.TMem",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_277edbe0d75278e702084240a6141e72"
],
0,
"19f1f63b582ffd4f29a0eebf544daf1d"
],
[
"X64.Vale.Decls.__proj__TMem__item__t",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_X64.Vale.Decls.TMem",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_277edbe0d75278e702084240a6141e72"
],
0,
"efa62cc3dc309e6acab30d257a03cb3b"
],
[
"X64.Vale.Decls.__proj__TStack__item__m",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_X64.Vale.Decls.TStack",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_17b42b6ab1b9e09f368c01e0bbc4eb8d"
],
0,
"d669b0d50c6b0d4b23995205a5b97885"
],
[
"X64.Vale.Decls.tainted_operand128",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_X64.Machine_s.maddr__uu___haseq",
"assumption_X64.Machine_s.taint__uu___haseq",
"equation_Prims.eqtype", "equation_X64.Machine_s.xmm",
"function_token_typing_Prims.int",
"haseqTm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"fa2a13a87fa30db510901794756438de"
],
[
"X64.Vale.Decls.__proj__TReg128__item__x",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_X64.Vale.Decls.TReg128",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_08b20fc77be468b2fd9149450277eb9c"
],
0,
"18ef4bae1614c026ecc2071dfce44600"
],
[
"X64.Vale.Decls.__proj__TMem128__item__m",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_X64.Vale.Decls.TMem128",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_dda93069d7e93e67c635584207e2249c"
],
0,
"b075ab949707e49a97b7d9eb9bdf0f3d"
],
[
"X64.Vale.Decls.__proj__TMem128__item__t",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_X64.Vale.Decls.TMem128",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_dda93069d7e93e67c635584207e2249c"
],
0,
"032d96d9df9c1cacd664f6b88c6ff797"
],
[
"X64.Vale.Decls.t_op_to_op",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_X64.Vale.Decls.TConst",
"disc_equation_X64.Vale.Decls.TMem",
"disc_equation_X64.Vale.Decls.TReg",
"disc_equation_X64.Vale.Decls.TStack",
"fuel_guarded_inversion_X64.Vale.Decls.tainted_operand"
],
0,
"bbe6769d3ed028a127a8f6fc2f8f7361"
],
[
"X64.Vale.Decls.t_op_to_op128",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_X64.Vale.Decls.TMem128",
"disc_equation_X64.Vale.Decls.TReg128",
"fuel_guarded_inversion_X64.Vale.Decls.tainted_operand128"
],
0,
"ff850eec8a8e44e0829d77ff7d07d3cf"
],
[
"X64.Vale.Decls.get_taint",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_X64.Vale.Decls.TConst",
"disc_equation_X64.Vale.Decls.TMem",
"disc_equation_X64.Vale.Decls.TReg",
"disc_equation_X64.Vale.Decls.TStack",
"fuel_guarded_inversion_X64.Vale.Decls.tainted_operand"
],
0,
"ba20bf6609cee3da7c63e30e89bc466d"
],
[
"X64.Vale.Decls.extract_taint",
1,
2,
0,
[ "@query", "projection_inverse_BoxBool_proj_0" ],
0,
"a54dc7c45a682a4c9cfe1f00726f9e31"
],
[
"X64.Vale.Decls.extract_taint3",
1,
2,
0,
[ "@query", "projection_inverse_BoxBool_proj_0" ],
0,
"e105efaeb7bff3226acfa548d1a2719a"
],
[
"X64.Vale.Decls.va_tl",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_X64.Vale.Decls.ins",
"equation_X64.Vale.Decls.ocmp",
"refinement_interpretation_Tm_refine_dcca6bc776074905e1b564169ca37618"
],
0,
"d3af6e05f9559873b93a7af710142845"
],
[
"X64.Vale.Decls.get_reg",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_X64.Vale.Decls.va_reg_operand",
"refinement_interpretation_Tm_refine_93c4793e88ba66df1f803c1610135c3a"
],
0,
"437de9c32fcaccafe5f56c11e1802d47"
],
[
"X64.Vale.Decls.buffer64_write",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_69ef455c2964bba317e61b9ea251d87d"
],
0,
"ed7096fa4e15ccb48ebad2d4d8b35a42"
],
[
"X64.Vale.Decls.buffer128_write",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_cb26ae5894b3dad7e96c8813f48738b2"
],
0,
"729e0d577ce11f99530916b440bd54f1"
],
[
"X64.Vale.Decls.va_op_cmp_reg",
1,
2,
0,
[
"@query", "constructor_distinct_X64.Vale.Decls.TReg",
"disc_equation_X64.Vale.Decls.TMem",
"projection_inverse_BoxBool_proj_0"
],
0,
"14b9f7a83390ac7d2863c2162c469da6"
],
[
"X64.Vale.Decls.va_const_cmp",
1,
2,
0,
[
"@query", "constructor_distinct_X64.Vale.Decls.TConst",
"disc_equation_X64.Vale.Decls.TMem",
"projection_inverse_BoxBool_proj_0"
],
0,
"db86796600e29a2df4972a7983e4a062"
],
[
"X64.Vale.Decls.va_coerce_reg_opr64_to_cmp",
1,
2,
0,
[
"@query", "constructor_distinct_X64.Machine_s.OMem",
"disc_equation_X64.Machine_s.OReg",
"disc_equation_X64.Vale.Decls.TMem",
"projection_inverse_BoxBool_proj_0"
],
0,
"04a691512d38bded5de3d549ad7f7380"
],
[
"X64.Vale.Decls.va_op_reg_oprerand_reg",
1,
2,
0,
[
"@query", "constructor_distinct_X64.Machine_s.OReg",
"disc_equation_X64.Machine_s.OReg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_X64.Machine_s.OReg_r"
],
0,
"19a15348d7e068cf46982916c9f5c0c1"
],
[
"X64.Vale.Decls.va_op_reg_opr64_reg",
1,
2,
0,
[
"@query", "constructor_distinct_X64.Machine_s.OReg",
"disc_equation_X64.Machine_s.OReg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_X64.Machine_s.OReg_r"
],
0,
"527024ee38213ecd8b2c31a7c3add68c"
],
[
"X64.Vale.Decls.va_opr_lemma_Mem",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Interop.Types.TUInt64",
"equality_tok_Interop.Types.TUInt64@tok", "equation_Prims.nat",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.Memory.base_typ_as_vale_type",
"function_token_typing_Prims.__cache_version_number__",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"22958b3478eac4df9ec0885d9d1cda1b"
],
[
"X64.Vale.Decls.va_opr_lemma_Mem",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"constructor_distinct_X64.Machine_s.MReg",
"constructor_distinct_X64.Machine_s.OMem",
"constructor_distinct_X64.Machine_s.OReg",
"constructor_distinct_X64.Vale.Decls.TMem",
"disc_equation_X64.Vale.Decls.TMem",
"disc_equation_X64.Vale.Decls.TReg",
"equality_tok_Interop.Types.TUInt64@tok",
"equation_X64.Memory.buffer64",
"equation_X64.Vale.Decls.valid_maddr",
"equation_X64.Vale.Decls.valid_mem_operand",
"equation_X64.Vale.Decls.valid_operand",
"equation_X64.Vale.State.eval_maddr",
"equation_X64.Vale.State.eval_operand",
"equation_X64.Vale.State.valid_src_operand",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"int_typing", "lemma_X64.Memory.buffer_length_buffer_as_seq",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_X64.Machine_s.MReg_offset",
"projection_inverse_X64.Machine_s.MReg_r",
"projection_inverse_X64.Machine_s.OMem_m",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Vale.Decls.TMem_m",
"projection_inverse_X64.Vale.Decls.TMem_t",
"typing_X64.Memory.valid_mem64",
"typing_X64.Vale.Decls.uu___is_TReg",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.eval_maddr",
"typing_tok_Interop.Types.TUInt64@tok"
],
0,
"4fea505b03ea0ffa5689cba1ba24e5f6"
],
[
"X64.Vale.Decls.va_opr_lemma_Stack",
1,
2,
0,
[ "@query" ],
0,
"f4c8ee2bbc611e9d9dbdb0b93c5f8813"
],
[
"X64.Vale.Decls.va_opr_lemma_Mem128",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"constructor_distinct_X64.Machine_s.MReg",
"constructor_distinct_X64.Machine_s.Mov128Mem",
"constructor_distinct_X64.Machine_s.OReg",
"constructor_distinct_X64.Vale.Decls.TMem128",
"disc_equation_X64.Vale.Decls.TMem128",
"disc_equation_X64.Vale.Decls.TReg",
"equality_tok_Interop.Types.TUInt128@tok",
"equation_X64.Memory.buffer128",
"equation_X64.Vale.Decls.valid_maddr128",
"equation_X64.Vale.Decls.valid_mem_operand128",
"equation_X64.Vale.Decls.valid_operand128",
"equation_X64.Vale.State.eval_maddr",
"equation_X64.Vale.State.eval_operand",
"equation_X64.Vale.State.valid_maddr128",
"equation_X64.Vale.State.valid_src_operand128",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"int_typing", "lemma_X64.Memory.buffer_length_buffer_as_seq",
"proj_equation_X64.Vale.State.Mkstate_mem",
"proj_equation_X64.Vale.State.Mkstate_memTaint",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_X64.Machine_s.MReg_offset",
"projection_inverse_X64.Machine_s.MReg_r",
"projection_inverse_X64.Machine_s.Mov128Mem_m",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Vale.Decls.TMem128_m",
"projection_inverse_X64.Vale.Decls.TMem128_t",
"typing_X64.Memory.valid_mem128",
"typing_X64.Vale.Decls.uu___is_TReg",
"typing_X64.Vale.State.__proj__Mkstate__item__mem",
"typing_X64.Vale.State.eval_maddr",
"typing_tok_Interop.Types.TUInt128@tok"
],
0,
"603d54f2eaf1d547d7239e3bd3d689e9"
],
[
"X64.Vale.Decls.va_update_operand",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OMem",
"constructor_distinct_X64.Machine_s.OReg",
"constructor_distinct_X64.Machine_s.OStack",
"disc_equation_X64.Machine_s.OConst",
"disc_equation_X64.Machine_s.OMem",
"disc_equation_X64.Machine_s.OReg",
"disc_equation_X64.Machine_s.OStack",
"fuel_guarded_inversion_X64.Vale.Decls.tainted_operand",
"projection_inverse_X64.Machine_s.OConst_n",
"projection_inverse_X64.Machine_s.OMem_m",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Machine_s.OStack_m"
],
0,
"eecef85112c0a7d5dc4ddb147367a57e"
],
[
"X64.Vale.Decls.va_upd_operand_dst_opr64",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OMem",
"constructor_distinct_X64.Machine_s.OReg",
"constructor_distinct_X64.Machine_s.OStack",
"disc_equation_X64.Machine_s.OConst",
"disc_equation_X64.Machine_s.OMem",
"disc_equation_X64.Machine_s.OReg",
"disc_equation_X64.Machine_s.OStack",
"fuel_guarded_inversion_X64.Vale.Decls.tainted_operand",
"projection_inverse_X64.Machine_s.OConst_n",
"projection_inverse_X64.Machine_s.OMem_m",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Machine_s.OStack_m"
],
0,
"1fd9b9ef9a19d5ae3b036518ea81dac0"
],
[
"X64.Vale.Decls.va_upd_operand_reg_opr64",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OMem",
"constructor_distinct_X64.Machine_s.OReg",
"constructor_distinct_X64.Machine_s.OStack",
"disc_equation_X64.Machine_s.OConst",
"disc_equation_X64.Machine_s.OMem",
"disc_equation_X64.Machine_s.OReg",
"disc_equation_X64.Machine_s.OStack",
"fuel_guarded_inversion_X64.Vale.Decls.tainted_operand",
"projection_inverse_X64.Machine_s.OConst_n",
"projection_inverse_X64.Machine_s.OMem_m",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Machine_s.OStack_m"
],
0,
"f6ef5aa939c34695fa4cb424135ec6bc"
],
[
"X64.Vale.Decls.va_lemma_upd_update",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "disc_equation_X64.Machine_s.OReg",
"equation_X64.Vale.Decls.va_is_dst_opr64",
"equation_X64.Vale.Decls.va_upd_operand_dst_opr64",
"equation_X64.Vale.Decls.va_upd_operand_reg_opr64",
"equation_X64.Vale.Decls.va_upd_operand_xmm",
"equation_X64.Vale.Decls.va_upd_reg",
"equation_X64.Vale.Decls.va_update_operand",
"equation_X64.Vale.State.eval_operand",
"fuel_guarded_inversion_X64.Vale.State.state",
"projection_inverse_BoxBool_proj_0"
],
0,
"6d59bcb973962adcbd1c94c0c9f8e30a"
],
[
"X64.Vale.Decls.va_cmp_eq",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OReg",
"disc_equation_X64.Machine_s.OMem",
"disc_equation_X64.Machine_s.OStack",
"disc_equation_X64.Vale.Decls.TMem",
"disc_equation_X64.Vale.Decls.TStack", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_d7e265851e934efc0f40db411eade264"
],
0,
"3af08a7c0abd5a9cb912ec9783c06317"
],
[
"X64.Vale.Decls.va_cmp_ne",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OReg",
"disc_equation_X64.Machine_s.OMem",
"disc_equation_X64.Machine_s.OStack",
"disc_equation_X64.Vale.Decls.TMem",
"disc_equation_X64.Vale.Decls.TStack", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_d7e265851e934efc0f40db411eade264"
],
0,
"7694037e27d3f824fb721f8838bc9d2e"
],
[
"X64.Vale.Decls.va_cmp_le",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OReg",
"disc_equation_X64.Machine_s.OMem",
"disc_equation_X64.Machine_s.OStack",
"disc_equation_X64.Vale.Decls.TMem",
"disc_equation_X64.Vale.Decls.TStack", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_d7e265851e934efc0f40db411eade264"
],
0,
"3b74ff1c05d66469cc87a8e7d5ab7c03"
],
[
"X64.Vale.Decls.va_cmp_ge",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OReg",
"disc_equation_X64.Machine_s.OMem",
"disc_equation_X64.Machine_s.OStack",
"disc_equation_X64.Vale.Decls.TMem",
"disc_equation_X64.Vale.Decls.TStack", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_d7e265851e934efc0f40db411eade264"
],
0,
"06f3a80bb846f22e26cd7ec987689438"
],
[
"X64.Vale.Decls.va_cmp_lt",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OReg",
"disc_equation_X64.Machine_s.OMem",
"disc_equation_X64.Machine_s.OStack",
"disc_equation_X64.Vale.Decls.TMem",
"disc_equation_X64.Vale.Decls.TStack", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_d7e265851e934efc0f40db411eade264"
],
0,
"ec09bf4a93ae3b01d352f795f2a7660a"
],
[
"X64.Vale.Decls.va_cmp_gt",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "constructor_distinct_Tm_unit",
"constructor_distinct_X64.Machine_s.OConst",
"constructor_distinct_X64.Machine_s.OReg",
"disc_equation_X64.Machine_s.OMem",
"disc_equation_X64.Machine_s.OStack",
"disc_equation_X64.Vale.Decls.TMem",
"disc_equation_X64.Vale.Decls.TStack", "primitive_Prims.op_BarBar",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_d7e265851e934efc0f40db411eade264"
],
0,
"70f989e75a3359c9ece027d0b6100c4c"
],
[
"X64.Vale.Decls.buffers_readable",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_45b5651ccff53142641c62adf4cca7a0_1",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok", "equation_X64.Memory.buffer64",
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"ffc3d116a665e3e01008dc7372e40730"
],
[
"X64.Vale.Decls.loc_locs_disjoint_rec128",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_c4a9282b94ca5d93dd2c295d6c086c07_1",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok", "equation_X64.Memory.buffer128",
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"c5169d7fb9e6ac09f4cee95903dc3790"
],
[
"X64.Vale.Decls.lemma_cmp_eq",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_X64.Bytes_Semantics_s.OEq",
"disc_equation_X64.Machine_s.OMem",
"disc_equation_X64.Machine_s.OStack",
"disc_equation_X64.Vale.Decls.TMem",
"disc_equation_X64.Vale.Decls.TStack",
"equality_tok_X64.Machine_s.Public@tok",
"equation_X64.Taint_Semantics_s.get_fst_ocmp",
"equation_X64.Taint_Semantics_s.get_snd_ocmp",
"equation_X64.Vale.Decls.eval_ocmp", "equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_cmp_eq",
"fuel_guarded_inversion_X64.Vale.State.state",
"lemma_X64.Vale.Lemmas.lemma_cmp_eq", "primitive_Prims.op_BarBar",
"proj_equation_X64.Taint_Semantics_s.TaintedOCmp_o",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_X64.Bytes_Semantics_s.OEq_o1",
"projection_inverse_X64.Bytes_Semantics_s.OEq_o2",
"projection_inverse_X64.Taint_Semantics_s.TaintedOCmp_o",
"refinement_interpretation_Tm_refine_3138bad0898641bfca626f44b720c051",
"refinement_interpretation_Tm_refine_926c1cdaa5b20ba51edf05d73b47a319",
"refinement_interpretation_Tm_refine_d7e265851e934efc0f40db411eade264",
"typing_X64.Machine_s.uu___is_OMem",
"typing_X64.Machine_s.uu___is_OStack",
"typing_X64.Taint_Semantics_s.__proj__TaintedOCmp__item__o",
"typing_X64.Taint_Semantics_s.get_fst_ocmp",
"typing_X64.Taint_Semantics_s.get_snd_ocmp",
"typing_X64.Vale.Decls.uu___is_TMem",
"typing_X64.Vale.Decls.uu___is_TStack",
"typing_X64.Vale.Decls.va_cmp_eq",
"typing_tok_X64.Machine_s.Public@tok"
],
0,
"659ecf95932e01758ca0c2a26f784e9f"
],
[
"X64.Vale.Decls.lemma_cmp_ne",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Words_s.nat64", "equation_Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"296ec7d3d15ba3a332f582f8e9633ba7"
],
[
"X64.Vale.Decls.lemma_cmp_ne",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_X64.Bytes_Semantics_s.ONe",
"disc_equation_X64.Machine_s.OMem",
"disc_equation_X64.Machine_s.OStack",
"disc_equation_X64.Vale.Decls.TMem",
"disc_equation_X64.Vale.Decls.TStack",
"equality_tok_X64.Machine_s.Public@tok",
"equation_X64.Taint_Semantics_s.get_fst_ocmp",
"equation_X64.Taint_Semantics_s.get_snd_ocmp",
"equation_X64.Vale.Decls.eval_ocmp", "equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_cmp_ne",
"fuel_guarded_inversion_X64.Vale.State.state",
"lemma_X64.Vale.Lemmas.lemma_cmp_ne", "primitive_Prims.op_BarBar",
"proj_equation_X64.Taint_Semantics_s.TaintedOCmp_o",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_X64.Bytes_Semantics_s.ONe_o1",
"projection_inverse_X64.Bytes_Semantics_s.ONe_o2",
"projection_inverse_X64.Taint_Semantics_s.TaintedOCmp_o",
"refinement_interpretation_Tm_refine_3138bad0898641bfca626f44b720c051",
"refinement_interpretation_Tm_refine_926c1cdaa5b20ba51edf05d73b47a319",
"refinement_interpretation_Tm_refine_d7e265851e934efc0f40db411eade264",
"typing_X64.Machine_s.uu___is_OMem",
"typing_X64.Machine_s.uu___is_OStack",
"typing_X64.Taint_Semantics_s.__proj__TaintedOCmp__item__o",
"typing_X64.Taint_Semantics_s.get_fst_ocmp",
"typing_X64.Taint_Semantics_s.get_snd_ocmp",
"typing_X64.Vale.Decls.uu___is_TMem",
"typing_X64.Vale.Decls.uu___is_TStack",
"typing_X64.Vale.Decls.va_cmp_ne",
"typing_tok_X64.Machine_s.Public@tok"
],
0,
"9ab5072293cc4936c8d8b1c3dd8a51f3"
],
[
"X64.Vale.Decls.lemma_cmp_le",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_X64.Bytes_Semantics_s.OLe",
"equality_tok_X64.Machine_s.Public@tok",
"equation_X64.Taint_Semantics_s.get_fst_ocmp",
"equation_X64.Taint_Semantics_s.get_snd_ocmp",
"equation_X64.Vale.Decls.eval_ocmp", "equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_cmp_le",
"fuel_guarded_inversion_X64.Vale.State.state",
"lemma_X64.Vale.Lemmas.lemma_cmp_le",
"proj_equation_X64.Taint_Semantics_s.TaintedOCmp_o",
"projection_inverse_X64.Bytes_Semantics_s.OLe_o1",
"projection_inverse_X64.Bytes_Semantics_s.OLe_o2",
"projection_inverse_X64.Taint_Semantics_s.TaintedOCmp_o",
"refinement_interpretation_Tm_refine_3138bad0898641bfca626f44b720c051",
"refinement_interpretation_Tm_refine_926c1cdaa5b20ba51edf05d73b47a319",
"typing_X64.Taint_Semantics_s.__proj__TaintedOCmp__item__o",
"typing_X64.Taint_Semantics_s.get_fst_ocmp",
"typing_X64.Taint_Semantics_s.get_snd_ocmp",
"typing_X64.Vale.Decls.va_cmp_le",
"typing_tok_X64.Machine_s.Public@tok"
],
0,
"18e0ceaee82d2a168a184af873c949b0"
],
[
"X64.Vale.Decls.lemma_cmp_ge",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_X64.Bytes_Semantics_s.OGe",
"equality_tok_X64.Machine_s.Public@tok",
"equation_X64.Taint_Semantics_s.get_fst_ocmp",
"equation_X64.Taint_Semantics_s.get_snd_ocmp",
"equation_X64.Vale.Decls.eval_ocmp", "equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_cmp_ge",
"fuel_guarded_inversion_X64.Vale.State.state",
"lemma_X64.Vale.Lemmas.lemma_cmp_ge",
"proj_equation_X64.Taint_Semantics_s.TaintedOCmp_o",
"projection_inverse_X64.Bytes_Semantics_s.OGe_o1",
"projection_inverse_X64.Bytes_Semantics_s.OGe_o2",
"projection_inverse_X64.Taint_Semantics_s.TaintedOCmp_o",
"refinement_interpretation_Tm_refine_3138bad0898641bfca626f44b720c051",
"refinement_interpretation_Tm_refine_926c1cdaa5b20ba51edf05d73b47a319",
"typing_X64.Taint_Semantics_s.__proj__TaintedOCmp__item__o",
"typing_X64.Taint_Semantics_s.get_fst_ocmp",
"typing_X64.Taint_Semantics_s.get_snd_ocmp",
"typing_X64.Vale.Decls.va_cmp_ge",
"typing_tok_X64.Machine_s.Public@tok"
],
0,
"bb9ac561817e590a029ee9c94b52e996"
],
[
"X64.Vale.Decls.lemma_cmp_lt",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_X64.Bytes_Semantics_s.OLt",
"equality_tok_X64.Machine_s.Public@tok",
"equation_X64.Taint_Semantics_s.get_fst_ocmp",
"equation_X64.Taint_Semantics_s.get_snd_ocmp",
"equation_X64.Vale.Decls.eval_ocmp", "equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_cmp_lt",
"fuel_guarded_inversion_X64.Vale.State.state",
"lemma_X64.Vale.Lemmas.lemma_cmp_lt",
"proj_equation_X64.Taint_Semantics_s.TaintedOCmp_o",
"projection_inverse_X64.Bytes_Semantics_s.OLt_o1",
"projection_inverse_X64.Bytes_Semantics_s.OLt_o2",
"projection_inverse_X64.Taint_Semantics_s.TaintedOCmp_o",
"refinement_interpretation_Tm_refine_3138bad0898641bfca626f44b720c051",
"refinement_interpretation_Tm_refine_926c1cdaa5b20ba51edf05d73b47a319",
"typing_X64.Taint_Semantics_s.__proj__TaintedOCmp__item__o",
"typing_X64.Taint_Semantics_s.get_fst_ocmp",
"typing_X64.Taint_Semantics_s.get_snd_ocmp",
"typing_X64.Vale.Decls.va_cmp_lt",
"typing_tok_X64.Machine_s.Public@tok"
],
0,
"534cbdc44ea5bbb13719ff3cb67334b3"
],
[
"X64.Vale.Decls.lemma_cmp_gt",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_X64.Bytes_Semantics_s.OGt",
"equality_tok_X64.Machine_s.Public@tok",
"equation_X64.Taint_Semantics_s.get_fst_ocmp",
"equation_X64.Taint_Semantics_s.get_snd_ocmp",
"equation_X64.Vale.Decls.eval_ocmp", "equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_cmp_gt",
"fuel_guarded_inversion_X64.Vale.State.state",
"lemma_X64.Vale.Lemmas.lemma_cmp_gt",
"proj_equation_X64.Taint_Semantics_s.TaintedOCmp_o",
"projection_inverse_X64.Bytes_Semantics_s.OGt_o1",
"projection_inverse_X64.Bytes_Semantics_s.OGt_o2",
"projection_inverse_X64.Taint_Semantics_s.TaintedOCmp_o",
"refinement_interpretation_Tm_refine_3138bad0898641bfca626f44b720c051",
"refinement_interpretation_Tm_refine_926c1cdaa5b20ba51edf05d73b47a319",
"typing_X64.Taint_Semantics_s.__proj__TaintedOCmp__item__o",
"typing_X64.Taint_Semantics_s.get_fst_ocmp",
"typing_X64.Taint_Semantics_s.get_snd_ocmp",
"typing_X64.Vale.Decls.va_cmp_gt",
"typing_tok_X64.Machine_s.Public@tok"
],
0,
"11cd2fa16cb9a2b6f85cbeb5ee11a491"
],
[
"X64.Vale.Decls.lemma_valid_cmp_eq",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"X64.Machine_s_pretyping_644ad5cdcea42fa4e9e52bbdd5021fb9",
"constructor_distinct_X64.Bytes_Semantics_s.OEq",
"data_elim_X64.Bytes_Semantics_s.OEq",
"equality_tok_X64.Machine_s.Public@tok",
"equation_X64.Bytes_Semantics_s.valid_ocmp",
"equation_X64.Vale.Decls.ocmp", "equation_X64.Vale.Decls.va_cmp_eq",
"equation_X64.Vale.Decls.valid_ocmp",
"equation_X64.Vale.Decls.valid_operand",
"equation_X64.Vale.Lemmas.valid_ocmp",
"fuel_guarded_inversion_X64.Vale.State.state",
"lemma_X64.Vale.StateLemmas.lemma_to_valid_operand",
"primitive_Prims.op_AmpAmp",
"proj_equation_X64.Taint_Semantics_s.TaintedOCmp_o",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_X64.Bytes_Semantics_s.OEq_o1",
"projection_inverse_X64.Bytes_Semantics_s.OEq_o2",
"projection_inverse_X64.Taint_Semantics_s.TaintedOCmp_o",
"refinement_interpretation_Tm_refine_926c1cdaa5b20ba51edf05d73b47a319",
"typing_X64.Taint_Semantics_s.__proj__TaintedOCmp__item__o",
"typing_X64.Vale.Decls.va_cmp_eq"
],
0,
"f934ac6470829db993f8ac379e332de7"
],
[
"X64.Vale.Decls.lemma_valid_cmp_ne",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"data_elim_X64.Bytes_Semantics_s.ONe",
"equality_tok_X64.Machine_s.Public@tok",
"equation_X64.Vale.Decls.ocmp", "equation_X64.Vale.Decls.va_cmp_ne",
"equation_X64.Vale.Decls.valid_ocmp",
"equation_X64.Vale.Decls.valid_operand",
"fuel_guarded_inversion_X64.Vale.State.state",
"lemma_X64.Vale.Lemmas.lemma_valid_cmp_ne",
"proj_equation_X64.Taint_Semantics_s.TaintedOCmp_o",
"projection_inverse_X64.Taint_Semantics_s.TaintedOCmp_o",
"typing_X64.Taint_Semantics_s.__proj__TaintedOCmp__item__o",
"typing_X64.Vale.Decls.va_cmp_ne",
"typing_tok_X64.Machine_s.Public@tok"
],
0,
"544b3dafd8c11149ec1615217e58aadb"
],
[
"X64.Vale.Decls.lemma_valid_cmp_le",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"data_elim_X64.Bytes_Semantics_s.OLe",
"equality_tok_X64.Machine_s.Public@tok",
"equation_X64.Vale.Decls.ocmp", "equation_X64.Vale.Decls.va_cmp_le",
"equation_X64.Vale.Decls.valid_ocmp",
"equation_X64.Vale.Decls.valid_operand",
"fuel_guarded_inversion_X64.Vale.State.state",
"lemma_X64.Vale.Lemmas.lemma_valid_cmp_le",
"proj_equation_X64.Taint_Semantics_s.TaintedOCmp_o",
"projection_inverse_X64.Taint_Semantics_s.TaintedOCmp_o",
"typing_X64.Taint_Semantics_s.__proj__TaintedOCmp__item__o",
"typing_X64.Vale.Decls.va_cmp_le",
"typing_tok_X64.Machine_s.Public@tok"
],
0,
"25bff2a9d43b3d431c3296f00ace87b5"
],
[
"X64.Vale.Decls.lemma_valid_cmp_ge",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"data_elim_X64.Bytes_Semantics_s.OGe",
"equality_tok_X64.Machine_s.Public@tok",
"equation_X64.Vale.Decls.ocmp", "equation_X64.Vale.Decls.va_cmp_ge",
"equation_X64.Vale.Decls.valid_ocmp",
"equation_X64.Vale.Decls.valid_operand",
"fuel_guarded_inversion_X64.Vale.State.state",
"lemma_X64.Vale.Lemmas.lemma_valid_cmp_ge",
"proj_equation_X64.Taint_Semantics_s.TaintedOCmp_o",
"projection_inverse_X64.Taint_Semantics_s.TaintedOCmp_o",
"typing_X64.Taint_Semantics_s.__proj__TaintedOCmp__item__o",
"typing_X64.Vale.Decls.va_cmp_ge",
"typing_tok_X64.Machine_s.Public@tok"
],
0,
"b7794580343efd71b7f1fbd66249032d"
],
[
"X64.Vale.Decls.lemma_valid_cmp_lt",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"data_elim_X64.Bytes_Semantics_s.OLt",
"equality_tok_X64.Machine_s.Public@tok",
"equation_X64.Vale.Decls.ocmp", "equation_X64.Vale.Decls.va_cmp_lt",
"equation_X64.Vale.Decls.valid_ocmp",
"equation_X64.Vale.Decls.valid_operand",
"fuel_guarded_inversion_X64.Vale.State.state",
"lemma_X64.Vale.Lemmas.lemma_valid_cmp_lt",
"proj_equation_X64.Taint_Semantics_s.TaintedOCmp_o",
"projection_inverse_X64.Taint_Semantics_s.TaintedOCmp_o",
"typing_X64.Taint_Semantics_s.__proj__TaintedOCmp__item__o",
"typing_X64.Vale.Decls.va_cmp_lt",
"typing_tok_X64.Machine_s.Public@tok"
],
0,
"bce362a1e84be7a3008f46202dd69e53"
],
[
"X64.Vale.Decls.lemma_valid_cmp_gt",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"data_elim_X64.Bytes_Semantics_s.OGt",
"equality_tok_X64.Machine_s.Public@tok",
"equation_X64.Vale.Decls.ocmp", "equation_X64.Vale.Decls.va_cmp_gt",
"equation_X64.Vale.Decls.valid_ocmp",
"equation_X64.Vale.Decls.valid_operand",
"fuel_guarded_inversion_X64.Vale.State.state",
"lemma_X64.Vale.Lemmas.lemma_valid_cmp_gt",
"proj_equation_X64.Taint_Semantics_s.TaintedOCmp_o",
"projection_inverse_X64.Taint_Semantics_s.TaintedOCmp_o",
"typing_X64.Taint_Semantics_s.__proj__TaintedOCmp__item__o",
"typing_X64.Vale.Decls.va_cmp_gt",
"typing_tok_X64.Machine_s.Public@tok"
],
0,
"d8e07c9e8cd8e6facc264a402cb5190d"
],
[
"X64.Vale.Decls.va_lemma_merge_total",
1,
2,
0,
[ "@query" ],
0,
"4cfe2c544804806c712b1f91890575be"
],
[
"X64.Vale.Decls.va_lemma_merge_total",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_X64.Taint_Semantics_s.tainted_code",
"equation_X64.Vale.Decls.eval_code", "equation_X64.Vale.Decls.ins",
"equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_compute_merge_total",
"equation_X64.Vale.Decls.va_fuel",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad"
],
0,
"e7546dffc9903629fa8647ff928ca33d"
],
[
"X64.Vale.Decls.va_lemma_empty_total",
1,
2,
0,
[
"@query", "equation_X64.Vale.Decls.eval_code",
"equation_X64.Vale.Decls.ins", "equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_fuel"
],
0,
"aa15cc0218da1610a6267610eebb517f"
],
[
"X64.Vale.Decls.va_lemma_ifElse_total",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_X64.Vale.Decls.eval_ocmp",
"equation_X64.Vale.Decls.va_fuel",
"fuel_guarded_inversion_X64.Taint_Semantics_s.tainted_ocmp"
],
0,
"14ffd270c065c221e1a151d8405c022e"
],
[
"X64.Vale.Decls.va_lemma_ifElseTrue_total",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_X64.Vale.Decls.eval_code",
"equation_X64.Vale.Decls.eval_ocmp", "equation_X64.Vale.Decls.ins",
"equation_X64.Vale.Decls.ocmp", "equation_X64.Vale.Decls.valid_ocmp",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad"
],
0,
"b47a9083c170f586c061ae72543667ba"
],
[
"X64.Vale.Decls.va_lemma_ifElseFalse_total",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_X64.Vale.Decls.eval_code",
"equation_X64.Vale.Decls.eval_ocmp", "equation_X64.Vale.Decls.ins",
"equation_X64.Vale.Decls.ocmp", "equation_X64.Vale.Decls.valid_ocmp",
"fuel_guarded_inversion_X64.Vale.State.state", "int_inversion",
"refinement_interpretation_Prims_Tm_refine_a4038d5aed1633b5ecbb4e499b1c66ad"
],
0,
"1435edb4594ed0f72a8eaddad4107cb3"
],
[
"X64.Vale.Decls.va_lemma_while_total",
1,
2,
0,
[
"@query", "equation_X64.Vale.Decls.eval_while_inv",
"equation_X64.Vale.Decls.ins", "equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_fuel"
],
0,
"1b55bc870775b8aaee056e158dfafe7d"
],
[
"X64.Vale.Decls.va_lemma_whileTrue_total",
1,
2,
0,
[
"@query", "equation_X64.Vale.Decls.eval_ocmp",
"equation_X64.Vale.Decls.va_fuel"
],
0,
"42c2f0f7b2291b48e175625df8179564"
],
[
"X64.Vale.Decls.va_lemma_whileFalse_total",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_X64.Vale.Decls.eval_code",
"equation_X64.Vale.Decls.eval_ocmp",
"equation_X64.Vale.Decls.eval_while_inv",
"equation_X64.Vale.Decls.ins", "equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_fuel",
"equation_X64.Vale.Decls.valid_ocmp",
"fuel_guarded_inversion_X64.Vale.State.state"
],
0,
"171fd81657d790267567e1c22ff80214"
],
[
"X64.Vale.Decls.va_lemma_whileMerge_total",
1,
2,
0,
[ "@query" ],
0,
"97a8d899a53498a14bb243104a9fc6b8"
],
[
"X64.Vale.Decls.va_lemma_whileMerge_total",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_X64.Machine_s.While",
"equation_X64.Vale.Decls.eval_code",
"equation_X64.Vale.Decls.eval_ocmp",
"equation_X64.Vale.Decls.eval_while_inv",
"equation_X64.Vale.Decls.ins", "equation_X64.Vale.Decls.ocmp",
"equation_X64.Vale.Decls.va_fuel",
"equation_X64.Vale.Decls.valid_ocmp",
"fuel_guarded_inversion_X64.Vale.State.state",
"projection_inverse_BoxBool_proj_0"
],
0,
"5828318d0a20cb63aa0eabae914a8bc2"
]
]
]
Computing file changes ...
