Revision 724d1045f60f13d79df1afc5190955afdfa73ec1 authored by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC, committed by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC
Co-authored-by: @protz
1 parent ca37fbf
Vale.X64.Decls.fst.hints
[
"�D��%ǃ��]�*u�U",
[
[
"Vale.X64.Decls.lemma_mul_in_bounds",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.mul_mod",
"equation_FStar.UInt.size", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"45d51b4cf88cb4e8d53942162b56281f"
],
[
"Vale.X64.Decls.lemma_mul_nat",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"f5f15f643c90698c3cca9f94b27e5e6d"
],
[
"Vale.X64.Decls.cf",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Prims.eqtype", "equation_Vale.X64.Flags.flag_val_t",
"equation_Vale.X64.Lemmas.cf", "function_token_typing_Prims.bool",
"lemma_FStar.Pervasives.invertOption",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.X64.Lemmas.cf"
],
0,
"8b90ff5f24333a75c319619149adef1c"
],
[
"Vale.X64.Decls.overflow",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Prims.eqtype", "equation_Vale.X64.Flags.flag_val_t",
"equation_Vale.X64.Lemmas.overflow",
"function_token_typing_Prims.bool",
"lemma_FStar.Pervasives.invertOption",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.X64.Lemmas.overflow"
],
0,
"5d57b7f3da465aea7e42c8beac8b3a1e"
],
[
"Vale.X64.Decls.valid_cf",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Prims.eqtype", "equation_Vale.X64.Flags.flag_val_t",
"equation_Vale.X64.Lemmas.cf", "function_token_typing_Prims.bool",
"lemma_FStar.Pervasives.invertOption",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.X64.Lemmas.cf"
],
0,
"144f62788415d40f52e3197f16d6e2df"
],
[
"Vale.X64.Decls.valid_of",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion", "bool_typing",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Prims.eqtype", "equation_Vale.X64.Flags.flag_val_t",
"equation_Vale.X64.Lemmas.overflow",
"function_token_typing_Prims.bool",
"lemma_FStar.Pervasives.invertOption",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.X64.Lemmas.overflow"
],
0,
"2e0b31a730b422b0010f9fafb83fa027"
],
[
"Vale.X64.Decls.updated_cf",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"assumption_FStar.Pervasives.Native.option__uu___haseq",
"bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Tm_unit", "equation_Prims.eqtype",
"equation_Vale.X64.Decls.cf", "equation_Vale.X64.Decls.valid_cf",
"equation_Vale.X64.Flags.flag_val_t", "equation_Vale.X64.Lemmas.cf",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"function_token_typing_Prims.bool", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.X64.Lemmas.cf"
],
0,
"33b07e9c792c61c728b3f269c331f2a7"
],
[
"Vale.X64.Decls.updated_of",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"assumption_FStar.Pervasives.Native.option__uu___haseq",
"bool_inversion",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Tm_unit", "equation_Prims.eqtype",
"equation_Vale.X64.Decls.overflow",
"equation_Vale.X64.Decls.valid_of",
"equation_Vale.X64.Flags.flag_val_t",
"equation_Vale.X64.Lemmas.overflow",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"function_token_typing_Prims.bool", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.X64.Lemmas.overflow"
],
0,
"5e6c69b6cffa1a0d7fd28a3678ca0a24"
],
[
"Vale.X64.Decls.maintained_cf",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"assumption_FStar.Pervasives.Native.option__uu___haseq",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Prims.eqtype", "equation_Vale.X64.Decls.cf",
"equation_Vale.X64.Decls.valid_cf",
"equation_Vale.X64.Flags.flag_val_t", "equation_Vale.X64.Lemmas.cf",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"function_token_typing_Prims.bool",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.X64.Lemmas.cf"
],
0,
"c7f4daa860ba12509bcd6cd467fe0fdc"
],
[
"Vale.X64.Decls.maintained_of",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86",
"assumption_FStar.Pervasives.Native.option__uu___haseq",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Prims.eqtype", "equation_Vale.X64.Decls.overflow",
"equation_Vale.X64.Decls.valid_of",
"equation_Vale.X64.Flags.flag_val_t",
"equation_Vale.X64.Lemmas.overflow",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"function_token_typing_Prims.bool",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.X64.Lemmas.overflow"
],
0,
"f7c21785ec1db637c81d187f19f5b503"
],
[
"Vale.X64.Decls.va_if",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"projection_inverse_BoxBool_proj_0"
],
0,
"6d8a0285c9504847107b56ee7fb3ffc9"
],
[
"Vale.X64.Decls.total_thunk_if",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"projection_inverse_BoxBool_proj_0"
],
0,
"bd019b44f2f59ef8d1697f16056c2d51"
],
[
"Vale.X64.Decls.va_tl",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_1c9655c30deebdd07e36fb0790c48d70"
],
0,
"2346a50ffcbe9e3c1631a3d5b5ab8ea9"
],
[
"Vale.X64.Decls.reg_operand",
1,
2,
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,
"b3f33898839d578748459466cb484da0"
],
[
"Vale.X64.Decls.va_operand_reg_opr64",
1,
2,
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,
"9371c44b0129be99f90c245533ce0e59"
],
[
"Vale.X64.Decls.cmp_operand",
1,
2,
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,
"69bff1d70e9a88c5bad55a234a8239f7"
],
[
"Vale.X64.Decls.get_reason",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.Def.PossiblyMonad.Err",
"disc_equation_Vale.Def.PossiblyMonad.Ok",
"equation_Vale.X64.Decls.va_pbool",
"fuel_guarded_inversion_Vale.Def.PossiblyMonad.possibly"
],
0,
"e14f8fa71922095047158d30b922a109"
],
[
"Vale.X64.Decls.get_reg",
1,
2,
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.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"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,
"2e6e9a9f2b995c87dbe11980ebce81ff"
],
[
"Vale.X64.Decls.va_op_opr64_reg64",
1,
2,
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,
"8b73e1c4ad2858baac18ab9994623232"
],
[
"Vale.X64.Decls.va_op_reg64_reg64",
1,
2,
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,
"ae044c091292817f39a8810e9905f9a2"
],
[
"Vale.X64.Decls.va_op_opr128_xmm",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"bec34744b4008244b272697e9759228a"
],
[
"Vale.X64.Decls.va_const_opr64",
1,
2,
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,
"e6785012ac59219507ed18526cda3d8a"
],
[
"Vale.X64.Decls.va_const_shift_amt64",
1,
2,
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,
"36d97a079811ca5eea8e7cb09a0fbe5f"
],
[
"Vale.X64.Decls.va_op_shift_amt64_reg64",
1,
2,
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,
"73d3b2e78d933fb7973a046e6870908b"
],
[
"Vale.X64.Decls.va_op_cmp_reg64",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OMem", "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",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"d0652e4e2a6dea87266c743b8866dc87"
],
[
"Vale.X64.Decls.va_const_cmp",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Machine_s.OConst",
"disc_equation_Vale.X64.Machine_s.OMem", "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",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"b301c77233ed905fdbfdcf9a881ea067"
],
[
"Vale.X64.Decls.va_coerce_reg64_opr64_to_cmp",
1,
2,
0,
[
"@query", "disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Machine_s.reg_64",
"projection_inverse_BoxBool_proj_0"
],
0,
"4d1ca7ce9d6712b0847844127e570c12"
],
[
"Vale.X64.Decls.va_coerce_opr64_to_cmp",
1,
2,
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,
"da657d9e4971c70ab03d3633e336f190"
],
[
"Vale.X64.Decls.va_op_reg_opr64_reg64",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Vale.X64.Machine_s.OReg",
"disc_equation_Vale.X64.Machine_s.OReg", "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",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Vale.X64.Machine_s.OReg_r",
"projection_inverse_Vale.X64.Machine_s.OReg_tc",
"projection_inverse_Vale.X64.Machine_s.OReg_tr",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"06884a542db01faef2b04ec56a74b6ad"
],
[
"Vale.X64.Decls.va_op_dst_opr64_reg64",
1,
2,
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,
"8bc9a3c13d7a918b1020136b7f00b2fa"
],
[
"Vale.X64.Decls.va_coerce_xmm_to_opr128",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"0a491ae7b898d3fa0a0c23249d68d271"
],
[
"Vale.X64.Decls.va_opr_code_Mem64",
1,
2,
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.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"4bbbf2f9cf95a88842e1d136e492d56d"
],
[
"Vale.X64.Decls.va_opr_code_Stack",
1,
2,
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.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"c691c04b1909c663ad236488eb2f891f"
],
[
"Vale.X64.Decls.va_opr_code_Mem128",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_xmm",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d"
],
0,
"195d3f798ac7358a241c6f00d7950959"
],
[
"Vale.X64.Decls.lemma_opr_Mem64",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"b2t_def", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.X64.Machine_s.MReg",
"constructor_distinct_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Prims.squash", "equation_Vale.Arch.HeapImpl.heaplet_id",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Lib.Map16.get",
"equation_Vale.X64.Decls.valid_buf_maddr64",
"equation_Vale.X64.Decls.valid_mem_operand64",
"equation_Vale.X64.Decls.valid_operand",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.t_reg_to_int",
"equation_Vale.X64.Memory.buffer64",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.valid_buffer_read",
"equation_Vale.X64.Memory_Sems.is_full_read",
"equation_Vale.X64.State.eval_maddr",
"equation_Vale.X64.State.eval_operand",
"equation_Vale.X64.State.valid_maddr",
"equation_Vale.X64.State.valid_src_operand",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
"int_typing", "l_and-interp",
"lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.StateLemmas.lemma_load_buffer_read64",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.X64.Machine_s.MReg_offset",
"projection_inverse_Vale.X64.Machine_s.MReg_r",
"projection_inverse_Vale.X64.Machine_s.OMem_m",
"projection_inverse_Vale.X64.Machine_s.OMem_tc",
"projection_inverse_Vale.X64.Machine_s.OMem_tr",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Memory.load_mem64",
"typing_Vale.X64.Memory.valid_mem64",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_tok_Vale.Arch.HeapTypes_s.Public@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt64@tok"
],
0,
"c966cd9401577ca645e96777816baea1"
],
[
"Vale.X64.Decls.lemma_opr_Mem128",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"b2t_def", "bool_inversion",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128",
"constructor_distinct_Vale.X64.Machine_s.MReg",
"constructor_distinct_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OMem",
"disc_equation_Vale.X64.Machine_s.OReg",
"equality_tok_Vale.Arch.HeapTypes_s.Public@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Arch.HeapImpl.heaplet_id",
"equation_Vale.Arch.HeapImpl.vale_heaplets",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Lib.Map16.get",
"equation_Vale.X64.Decls.valid_buf_maddr128",
"equation_Vale.X64.Decls.valid_mem_operand128",
"equation_Vale.X64.Decls.valid_operand128",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.Machine_s.reg_xmm",
"equation_Vale.X64.Machine_s.t_reg_to_int",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.Memory.get_vale_heap",
"equation_Vale.X64.Memory.scale_by",
"equation_Vale.X64.Memory.valid_buffer_read",
"equation_Vale.X64.Memory_Sems.is_full_read",
"equation_Vale.X64.State.eval_maddr",
"equation_Vale.X64.State.eval_operand",
"equation_Vale.X64.State.valid_maddr128",
"equation_Vale.X64.State.valid_src_operand128",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Arch.HeapImpl.vale_heap",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
"int_typing", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq",
"lemma_Vale.X64.StateLemmas.lemma_load_buffer_read128",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heaplets",
"proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"proj_equation_Vale.X64.State.Mkvale_state_vs_heap",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Vale.X64.Machine_s.MReg_offset",
"projection_inverse_Vale.X64.Machine_s.MReg_r",
"projection_inverse_Vale.X64.Machine_s.OMem_m",
"projection_inverse_Vale.X64.Machine_s.OMem_tc",
"projection_inverse_Vale.X64.Machine_s.OMem_tr",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heap",
"typing_Vale.Arch.HeapImpl.__proj__Mkvale_full_heap__item__vf_heaplets",
"typing_Vale.Lib.Map16.sel", "typing_Vale.X64.Memory.valid_mem128",
"typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap",
"typing_Vale.X64.State.eval_maddr",
"typing_tok_Vale.Arch.HeapTypes_s.Public@tok",
"typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok"
],
0,
"09d9f637404395ee436cb9dd68cb90a3"
],
[
"Vale.X64.Decls.va_is_dst_opr64",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"e2d79384b70926c505eae5b748287dc6"
],
[
"Vale.X64.Decls.va_is_src_reg_opr64",
1,
2,
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,
"bc79e0f35c71b43cdf67c70666c8ef97"
],
[
"Vale.X64.Decls.va_is_dst_reg_opr64",
1,
2,
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,
"4789de97b534959f808afee5ecafd9ad"
],
[
"Vale.X64.Decls.update_operand",
1,
2,
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,
"933bd5c7faa7e2290d7f6bd7e75dbc72"
],
[
"Vale.X64.Decls.va_upd_operand_dst_opr64",
1,
2,
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,
"dd7bb17fcf3ef791b26de6711262bff9"
],
[
"Vale.X64.Decls.va_upd_operand_reg_opr64",
1,
2,
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,
"f3b7b11570c8d33df9ee876463da1331"
],
[
"Vale.X64.Decls.va_lemma_upd_update",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.OReg",
"equation_Vale.Def.Words_s.nat64",
"equation_Vale.X64.Decls.update_operand",
"equation_Vale.X64.Decls.va_is_dst_opr64",
"equation_Vale.X64.Decls.va_upd_operand_dst_opr64",
"equation_Vale.X64.Decls.va_upd_operand_reg_opr64",
"equation_Vale.X64.Decls.va_upd_operand_xmm",
"equation_Vale.X64.Decls.va_upd_reg64",
"equation_Vale.X64.Machine_s.reg_64",
"equation_Vale.X64.State.eval_operand",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"projection_inverse_BoxBool_proj_0"
],
0,
"e9547166ca10d24dbf882be5f1ed20cd"
],
[
"Vale.X64.Decls.va_cmp_eq",
1,
2,
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,
"cc13f9a5dafaad766abb3ad7ccc6e2f9"
],
[
"Vale.X64.Decls.va_cmp_eq",
2,
2,
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,
"5876fdeb507ee1261130c65ea4f8b688"
],
[
"Vale.X64.Decls.va_cmp_ne",
1,
2,
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,
"b671b1d749ebf0230481d08650a09406"
],
[
"Vale.X64.Decls.va_cmp_ne",
2,
2,
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,
"62ad0cccae593f2bcc23b204ae553352"
],
[
"Vale.X64.Decls.va_cmp_le",
1,
2,
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,
"92e22d1c4ab9254147e3570ea5975a3c"
],
[
"Vale.X64.Decls.va_cmp_le",
2,
2,
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,
"6a48569cb72f8f72ee5ab3a1f2325613"
],
[
"Vale.X64.Decls.va_cmp_ge",
1,
2,
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,
"573a17800f4f9e6a71db527c5c22d340"
],
[
"Vale.X64.Decls.va_cmp_ge",
2,
2,
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,
"3b27124f7e72627bec1043645c4d1ad0"
],
[
"Vale.X64.Decls.va_cmp_lt",
1,
2,
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,
"6e95a1ffca7aa5cd941c7b5a58921433"
],
[
"Vale.X64.Decls.va_cmp_lt",
2,
2,
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,
"1655aa6ecdbc9df193114be0bc3af17d"
],
[
"Vale.X64.Decls.va_cmp_gt",
1,
2,
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,
"a466b9a02134f1642b519863ad43eacb"
],
[
"Vale.X64.Decls.va_cmp_gt",
2,
2,
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,
"02f86c0da46b62c7d4ea1bb4dadb0ae0"
],
[
"Vale.X64.Decls.buffers_readable",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_2ba196b19be26fed8bbff92956a16ea9_1",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok", "equation_Vale.X64.Memory.buffer64",
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"fa122986d83c1175c799f5613ab82e7b"
],
[
"Vale.X64.Decls.loc_locs_disjoint_rec128",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"binder_x_b6f06d207926310c35b5daa4508dea69_1",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equality_tok_Prims.LexTop@tok",
"equation_Vale.X64.Memory.buffer128",
"fuel_guarded_inversion_Prims.list", "subterm_ordering_Prims.Cons"
],
0,
"cf75d235e729b01b1ad74186502cc3de"
],
[
"Vale.X64.Decls.va_ins_lemma",
1,
2,
0,
[
"@query",
"function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_code_ins",
"function_token_typing_Vale.X64.Machine_Semantics_s.machine_eval_code_ins_def"
],
0,
"2431b6fb99207652a2841b9780b6cc44"
],
[
"Vale.X64.Decls.lemma_cmp_eq",
1,
2,
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,
"1f6c7dd5a479f8f2df2c2e98621b61d0"
],
[
"Vale.X64.Decls.lemma_cmp_eq",
2,
2,
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,
"b9f842e834ad487944db0a5582226370"
],
[
"Vale.X64.Decls.lemma_cmp_eq",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Decls.eval_ocmp",
"equation_Vale.X64.Decls.va_cmp_eq",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Lemmas.lemma_cmp_eq"
],
0,
"25eac1689debc5ecabd2e6a5b9ab4bf1"
],
[
"Vale.X64.Decls.lemma_cmp_ne",
1,
2,
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,
"cb1b63f404c5a0462a209b3836c75a08"
],
[
"Vale.X64.Decls.lemma_cmp_ne",
2,
2,
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,
"302ba24055993939bb730c242857cebf"
],
[
"Vale.X64.Decls.lemma_cmp_ne",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Decls.eval_ocmp",
"equation_Vale.X64.Decls.va_cmp_ne",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Lemmas.lemma_cmp_ne"
],
0,
"80d9b158684928cd4b134230725d76a6"
],
[
"Vale.X64.Decls.lemma_cmp_le",
1,
2,
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,
"60f240259f86eb9f6d30a829ce89894f"
],
[
"Vale.X64.Decls.lemma_cmp_le",
2,
2,
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,
"9c64811c570bba3049131cce3d64a0e9"
],
[
"Vale.X64.Decls.lemma_cmp_le",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Decls.eval_ocmp",
"equation_Vale.X64.Decls.va_cmp_le",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Lemmas.lemma_cmp_le"
],
0,
"f6eadcffa02014aa944617a095381a15"
],
[
"Vale.X64.Decls.lemma_cmp_ge",
1,
2,
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,
"1025afbee0154f2d72b1de79397feb2e"
],
[
"Vale.X64.Decls.lemma_cmp_ge",
2,
2,
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,
"2e2b1fadaec639ab2e5fb15973a59ec0"
],
[
"Vale.X64.Decls.lemma_cmp_ge",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Decls.eval_ocmp",
"equation_Vale.X64.Decls.va_cmp_ge",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Lemmas.lemma_cmp_ge"
],
0,
"ee8eeb55bb53f80956c8a23671f3dd92"
],
[
"Vale.X64.Decls.lemma_cmp_lt",
1,
2,
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,
"d978d700f131445aba00d05785a1cfac"
],
[
"Vale.X64.Decls.lemma_cmp_lt",
2,
2,
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,
"918b7bc92d0b9a7268e1e1bb5164de3b"
],
[
"Vale.X64.Decls.lemma_cmp_lt",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Decls.eval_ocmp",
"equation_Vale.X64.Decls.va_cmp_lt",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Lemmas.lemma_cmp_lt"
],
0,
"12766abe7512872b33d57f28453193f3"
],
[
"Vale.X64.Decls.lemma_cmp_gt",
1,
2,
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,
"e618170850faf99ed792b984364c7756"
],
[
"Vale.X64.Decls.lemma_cmp_gt",
2,
2,
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,
"2e5ee5008d8b75d5d7f689f3b3417132"
],
[
"Vale.X64.Decls.lemma_cmp_gt",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Decls.eval_ocmp",
"equation_Vale.X64.Decls.va_cmp_gt",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Lemmas.lemma_cmp_gt"
],
0,
"d5b29472f025a6a4bb628ddfe3be2982"
],
[
"Vale.X64.Decls.lemma_valid_cmp_eq",
1,
2,
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,
"29075c45a8d7e793442d0807ead80277"
],
[
"Vale.X64.Decls.lemma_valid_cmp_eq",
2,
2,
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,
"b7c8906774b547a6144f376089fe6544"
],
[
"Vale.X64.Decls.lemma_valid_cmp_eq",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Decls.va_cmp_eq",
"equation_Vale.X64.Decls.valid_ocmp",
"equation_Vale.X64.Decls.valid_operand",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Lemmas.lemma_valid_cmp_eq"
],
0,
"debb16083634ff8f828e3aa1e71e239e"
],
[
"Vale.X64.Decls.lemma_valid_cmp_ne",
1,
2,
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,
"27445bda33250b37a3d937f9fbfabb91"
],
[
"Vale.X64.Decls.lemma_valid_cmp_ne",
2,
2,
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,
"b54627adac20f9580775cc65d81ef803"
],
[
"Vale.X64.Decls.lemma_valid_cmp_ne",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Decls.va_cmp_ne",
"equation_Vale.X64.Decls.valid_ocmp",
"equation_Vale.X64.Decls.valid_operand",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Lemmas.lemma_valid_cmp_ne"
],
0,
"d650887c7949172734b17cd2b5a38ac2"
],
[
"Vale.X64.Decls.lemma_valid_cmp_le",
1,
2,
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,
"3b484709ae245926883d992ca8fce6a7"
],
[
"Vale.X64.Decls.lemma_valid_cmp_le",
2,
2,
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,
"3908e133a6a8a58ed9264eafcdbea799"
],
[
"Vale.X64.Decls.lemma_valid_cmp_le",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Decls.va_cmp_le",
"equation_Vale.X64.Decls.valid_ocmp",
"equation_Vale.X64.Decls.valid_operand",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Lemmas.lemma_valid_cmp_le"
],
0,
"b8fb8c8c0d300ff45f652c01cd7e6d2f"
],
[
"Vale.X64.Decls.lemma_valid_cmp_ge",
1,
2,
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,
"9f0df5c1c174a7c869d7e6f677ff72d7"
],
[
"Vale.X64.Decls.lemma_valid_cmp_ge",
2,
2,
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,
"5b02be99df07fce1c58d29b7aee414e5"
],
[
"Vale.X64.Decls.lemma_valid_cmp_ge",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Decls.va_cmp_ge",
"equation_Vale.X64.Decls.valid_ocmp",
"equation_Vale.X64.Decls.valid_operand",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Lemmas.lemma_valid_cmp_ge"
],
0,
"7255043a1d1f4c412aee4f76b7a94475"
],
[
"Vale.X64.Decls.lemma_valid_cmp_lt",
1,
2,
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,
"85fc5258d41c0c63c7968e7496b06d7f"
],
[
"Vale.X64.Decls.lemma_valid_cmp_lt",
2,
2,
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,
"52af7f96dc7c9a9a7f993c0eaa5222c0"
],
[
"Vale.X64.Decls.lemma_valid_cmp_lt",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Decls.va_cmp_lt",
"equation_Vale.X64.Decls.valid_ocmp",
"equation_Vale.X64.Decls.valid_operand",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Lemmas.lemma_valid_cmp_lt"
],
0,
"4c1bd2bd53212363839d3fab0140693b"
],
[
"Vale.X64.Decls.lemma_valid_cmp_gt",
1,
2,
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,
"64c7a46f0a1e89754733d8a3a959db77"
],
[
"Vale.X64.Decls.lemma_valid_cmp_gt",
2,
2,
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,
"68d215229072dd49adfb1444839ec8b9"
],
[
"Vale.X64.Decls.lemma_valid_cmp_gt",
3,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Decls.va_cmp_gt",
"equation_Vale.X64.Decls.valid_ocmp",
"equation_Vale.X64.Decls.valid_operand",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"lemma_Vale.X64.Lemmas.lemma_valid_cmp_gt"
],
0,
"317dedf99e1948a4ed82beb4ff6bb3bf"
],
[
"Vale.X64.Decls.va_lemma_merge_total",
1,
2,
0,
[ "@query" ],
0,
"0a302b0dd1b4719dd41d601769b97e3d"
],
[
"Vale.X64.Decls.va_lemma_merge_total",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.X64.Bytes_Code_s.code_t",
"equation_Vale.X64.Decls.eval_code", "equation_Vale.X64.Decls.ins",
"equation_Vale.X64.Decls.ocmp",
"equation_Vale.X64.Decls.va_compute_merge_total",
"equation_Vale.X64.Decls.va_fuel",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"76ac5e532780ffd8e897965858565891"
],
[
"Vale.X64.Decls.va_lemma_empty_total",
1,
2,
0,
[
"@query", "equation_Vale.X64.Decls.eval_code",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"equation_Vale.X64.Decls.va_fuel",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp"
],
0,
"1f5cb607a29c3aa01bc0bfd737948ce7"
],
[
"Vale.X64.Decls.va_lemma_ifElse_total",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Decls.eval_ocmp",
"equation_Vale.X64.Decls.havoc_flags",
"equation_Vale.X64.Decls.va_fuel",
"fuel_guarded_inversion_Vale.X64.State.vale_state"
],
0,
"c4168b957e8b287ff6cc6ce5fdbfbae8"
],
[
"Vale.X64.Decls.va_lemma_ifElseTrue_total",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.X64.Decls.eval_code",
"equation_Vale.X64.Decls.eval_ocmp",
"equation_Vale.X64.Decls.havoc_flags", "equation_Vale.X64.Decls.ins",
"equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"45066151b76a575b5d4eec83bdf8e98d"
],
[
"Vale.X64.Decls.va_lemma_ifElseFalse_total",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.X64.Decls.eval_code",
"equation_Vale.X64.Decls.eval_ocmp",
"equation_Vale.X64.Decls.havoc_flags", "equation_Vale.X64.Decls.ins",
"equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"fuel_guarded_inversion_Vale.X64.State.vale_state", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"92110cff3efbf7a3e130f309a5335cb2"
],
[
"Vale.X64.Decls.va_lemma_while_total",
1,
2,
0,
[
"@query", "equation_Vale.X64.Decls.eval_while_inv",
"equation_Vale.X64.Decls.ins", "equation_Vale.X64.Decls.ocmp",
"equation_Vale.X64.Decls.va_fuel",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp"
],
0,
"bb7df59cd0b40788d46f875913dfd749"
],
[
"Vale.X64.Decls.va_lemma_whileTrue_total",
1,
2,
0,
[
"@query", "equation_Vale.X64.Decls.eval_ocmp",
"equation_Vale.X64.Decls.havoc_flags",
"equation_Vale.X64.Decls.va_fuel"
],
0,
"6ab37ac65e4586dbdc8c986db160e413"
],
[
"Vale.X64.Decls.va_lemma_whileFalse_total",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Vale.X64.Decls.eval_code",
"equation_Vale.X64.Decls.eval_ocmp",
"equation_Vale.X64.Decls.eval_while_inv",
"equation_Vale.X64.Decls.havoc_flags", "equation_Vale.X64.Decls.ins",
"equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.va_fuel",
"equation_Vale.X64.Decls.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"fuel_guarded_inversion_Vale.X64.State.vale_state"
],
0,
"37e3e859651b18b86e34d2cb0b1be66b"
],
[
"Vale.X64.Decls.va_lemma_whileMerge_total",
1,
2,
0,
[ "@query" ],
0,
"2e3985484e827f108b44f815ea3598d8"
],
[
"Vale.X64.Decls.va_lemma_whileMerge_total",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_Vale.X64.Machine_s.While",
"equation_Vale.X64.Decls.eval_code",
"equation_Vale.X64.Decls.eval_ocmp",
"equation_Vale.X64.Decls.eval_while_inv",
"equation_Vale.X64.Decls.havoc_flags", "equation_Vale.X64.Decls.ins",
"equation_Vale.X64.Decls.ocmp", "equation_Vale.X64.Decls.va_fuel",
"equation_Vale.X64.Decls.valid_ocmp",
"equation_Vale.X64.Machine_Semantics_s.ins",
"equation_Vale.X64.Machine_Semantics_s.ocmp",
"fuel_guarded_inversion_Vale.X64.State.vale_state",
"projection_inverse_BoxBool_proj_0"
],
0,
"573996980d657549bce70a9bb2576f19"
],
[
"Vale.X64.Decls.max_one_mem",
1,
2,
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,
"d97d94faafde1bd63a8cc0fed261014c"
]
]
]
Computing file changes ...
