Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Vale.Interop.X64.fst.hints
[
"|o���[=�%���t",
[
[
"Vale.Interop.X64.calling_conventions",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg", "int_inversion",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_Vale.X64.Machine_s.__proj__Reg__item__rf"
],
0,
"5c88d773107b3dce9d959314d641c3b7"
],
[
"Vale.Interop.X64.arg_reg_relation'",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Interop.X64.reg_nat",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"b530df7122aaea687a6b75c8c8b96d89"
],
[
"Vale.Interop.X64.__proj__Rel__item__of_arg",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Interop.X64.reg_nat",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"a4fccfca5eca34391423fe82cce85fdd"
],
[
"Vale.Interop.X64.__proj__Rel__item__of_arg",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Interop.X64.reg_nat",
"equation_Vale.X64.Machine_s.reg_64",
"fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"haseqTm_refine_c365eb902b454950de62fba701d9049d",
"proj_equation_Vale.Interop.X64.Rel_of_reg",
"projection_inverse_Vale.Interop.X64.Rel_of_reg",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"token_correspondence_Vale.Interop.X64.__proj__Rel__item__of_reg"
],
0,
"fcdd41498c54ccb02211eae7c140e368"
],
[
"Vale.Interop.X64.arg_reg_relation",
1,
1,
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,
"50123313f2008f7ee835c8cf0f54efdc"
],
[
"Vale.Interop.X64.upd_reg",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"0f9c9b76cd1b96224178f0bc4d0791e1"
],
[
"Vale.Interop.X64.arg_as_nat64",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt16",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt32",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt64",
"constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8",
"constructor_distinct_Vale.Interop.Base.TD_Base",
"constructor_distinct_Vale.Interop.Base.TD_Buffer",
"constructor_distinct_Vale.Interop.Base.TD_ImmBuffer",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt16",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt32",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt64",
"disc_equation_Vale.Arch.HeapTypes_s.TUInt8",
"disc_equation_Vale.Interop.Base.TD_Base",
"disc_equation_Vale.Interop.Base.TD_Buffer",
"disc_equation_Vale.Interop.Base.TD_ImmBuffer",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt16@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt32@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt64@tok",
"equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_LowStar.Buffer.trivial_preorder", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Interop.Base.buf_t",
"equation_Vale.Interop.Base.ibuf_t",
"equation_Vale.Interop.Base.td_as_type",
"equation_Vale.Interop.Base.valid_base_type",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Vale.Arch.HeapTypes_s.base_typ",
"fuel_guarded_inversion_Vale.Interop.Base.td", "int_inversion",
"int_typing",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Vale.Interop.Base.TD_Base__0",
"proj_equation_Vale.Interop.Types.Buffer_rel",
"proj_equation_Vale.Interop.Types.Buffer_rrel",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Interop.Base.TD_Base__0",
"projection_inverse_Vale.Interop.Base.TD_Buffer__0",
"projection_inverse_Vale.Interop.Base.TD_Buffer__1",
"projection_inverse_Vale.Interop.Base.TD_Buffer__2",
"projection_inverse_Vale.Interop.Base.TD_ImmBuffer__0",
"projection_inverse_Vale.Interop.Base.TD_ImmBuffer__1",
"projection_inverse_Vale.Interop.Base.TD_ImmBuffer__2",
"projection_inverse_Vale.Interop.Types.Buffer_rel",
"projection_inverse_Vale.Interop.Types.Buffer_rrel",
"projection_inverse_Vale.Interop.Types.Buffer_writeable",
"refinement_interpretation_Tm_refine_1665f1ce84843a1b3ee2b366c7c855b4",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7ddc9affe1c24b533b166e85103903e5",
"refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80",
"refinement_interpretation_Tm_refine_cc44fd36d5a2aa45d2e509a17f81b635",
"token_correspondence_Prims.pow2.fuel_instrumented",
"token_correspondence_Vale.Interop.Types.__proj__Buffer__item__rel",
"token_correspondence_Vale.Interop.Types.__proj__Buffer__item__rrel",
"true_interp", "typing_Vale.Interop.Base.__proj__TD_Base__item___0"
],
0,
"14201825eee0708dc8733630163c1f9b"
],
[
"Vale.Interop.X64.register_of_args",
1,
1,
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,
"55eff9c9aaa4104dc854ff1cc8bf0f7f"
],
[
"Vale.Interop.X64.register_of_args",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.X64_interpretation_Tm_arrow_8586951a648edf3e1a4ab7205cd76f9a",
"binder_x_a2968b5aedabccc4f9a87ef4627271f7_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_d44bc976b7abffa2383f9beda9ed2be2_3",
"constructor_distinct_Prims.Cons", "constructor_distinct_Tm_unit",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Prims.nat", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arg_as_nat64",
"equation_Vale.Interop.X64.arg_list",
"equation_Vale.Interop.X64.upd_reg",
"equation_Vale.Interop.X64.update_regs",
"equation_Vale.X64.Machine_s.reg_64",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.Interop.X64.__proj__Rel__item__of_arg",
"int_inversion", "int_typing",
"interpretation_Tm_abs_40c176358d0f08dc3044d9601a70555e",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan",
"proj_equation_FStar.Pervasives.Native.Some_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"refinement_interpretation_Tm_refine_14339eb8533e3614a873a95b131397c3",
"refinement_interpretation_Tm_refine_15685006ec438bc2f8ca7bff4430c057",
"refinement_interpretation_Tm_refine_27d2df70cea38c5a8832d2b54b387e26",
"refinement_interpretation_Tm_refine_30717a2fe2b5f84dbb8dbb8d5f517985",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0",
"refinement_interpretation_Tm_refine_aedc138702446b65fd6f58c5f54c76e5",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"token_correspondence_Vale.Interop.X64.update_regs",
"well-founded-ordering-on-nat"
],
0,
"593087aa10efbd7e60c745c7e63ccc4c"
],
[
"Vale.Interop.X64.register_of_args",
3,
1,
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,
"5f77378ad800cd1c81d17ac81254ff9f"
],
[
"Vale.Interop.X64.register_of_args",
4,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"985f70444b0c900e655a74a23d267f6d"
],
[
"Vale.Interop.X64.register_of_args",
5,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"9af607d45ab8a0bc09e9180cec0da6ff"
],
[
"Vale.Interop.X64.stack_of_args",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"3b38bfd7994987d9ffe2dfb1fa2adc2c"
],
[
"Vale.Interop.X64.stack_of_args",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_f1a25a7a9568029cc84ed0689b5f2730_3",
"constructor_distinct_Prims.Cons", "constructor_distinct_Tm_unit",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Prims.nat", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arg_list",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg", "int_inversion",
"int_typing", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"refinement_interpretation_Tm_refine_2023a85859015575478d3c82f97e9605",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0",
"token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"well-founded-ordering-on-nat"
],
0,
"93df1354e94f8598af7d5f9b53d05617"
],
[
"Vale.Interop.X64.stack_of_args",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"297864da89b276b80931907923895ec6"
],
[
"Vale.Interop.X64.stack_of_args",
4,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"8441cc8738cdb618f5b6f6e85ec4456f"
],
[
"Vale.Interop.X64.upd_taint_map_arg",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query", "data_elim_Prims.Mkdtuple2",
"disc_equation_Vale.Interop.Base.TD_Base",
"disc_equation_Vale.Interop.Base.TD_Buffer",
"disc_equation_Vale.Interop.Base.TD_ImmBuffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.Types.base_typ_as_type",
"fuel_guarded_inversion_Prims.dtuple2",
"fuel_guarded_inversion_Vale.Interop.Base.td",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"proj_equation_Prims.Mkdtuple2__1",
"proj_equation_Vale.Interop.Types.Buffer_rel",
"proj_equation_Vale.Interop.Types.Buffer_rrel",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Mkdtuple2__1",
"projection_inverse_Vale.Interop.Base.TD_Buffer__0",
"projection_inverse_Vale.Interop.Types.Buffer_rel",
"projection_inverse_Vale.Interop.Types.Buffer_rrel",
"projection_inverse_Vale.Interop.Types.Buffer_writeable",
"token_correspondence_Vale.Interop.Types.__proj__Buffer__item__rel",
"token_correspondence_Vale.Interop.Types.__proj__Buffer__item__rrel",
"true_interp"
],
0,
"77a4b6b13d4a113fd6373a01c5f48a8f"
],
[
"Vale.Interop.X64.taint_arg_b8",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_Vale.Interop.Base.TD_Buffer",
"constructor_distinct_Vale.Interop.Base.TD_ImmBuffer",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Vale.Interop.Base.TD_Buffer",
"disc_equation_Vale.Interop.Base.TD_ImmBuffer",
"equality_tok_Vale.X64.Machine_s.Public@tok",
"equation_LowStar.Buffer.trivial_preorder",
"equation_Vale.Interop.Base.buf_t",
"equation_Vale.Interop.Base.ibuf_t",
"equation_Vale.Interop.Base.td_as_type",
"equation_Vale.Interop.X64.taint_of_arg",
"interpretation_Tm_abs_612136ee4143d24977831c80e4f470a1",
"proj_equation_Vale.Interop.Types.Buffer_rel",
"proj_equation_Vale.Interop.Types.Buffer_rrel",
"proj_equation_Vale.Interop.Types.Buffer_writeable",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_Prims.Mkdtuple2__1",
"projection_inverse_Vale.Interop.Base.TD_Buffer__0",
"projection_inverse_Vale.Interop.Base.TD_Buffer__1",
"projection_inverse_Vale.Interop.Base.TD_Buffer__2",
"projection_inverse_Vale.Interop.Base.TD_ImmBuffer__0",
"projection_inverse_Vale.Interop.Base.TD_ImmBuffer__1",
"projection_inverse_Vale.Interop.Base.TD_ImmBuffer__2",
"projection_inverse_Vale.Interop.Types.Buffer_rel",
"projection_inverse_Vale.Interop.Types.Buffer_rrel",
"projection_inverse_Vale.Interop.Types.Buffer_writeable",
"refinement_interpretation_Tm_refine_1665f1ce84843a1b3ee2b366c7c855b4",
"refinement_interpretation_Tm_refine_81ccb32c02ec946601a86ab897f3370e",
"refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80",
"token_correspondence_Vale.Interop.Types.__proj__Buffer__item__rel",
"token_correspondence_Vale.Interop.Types.__proj__Buffer__item__rrel",
"true_interp", "typing_tok_Vale.X64.Machine_s.Public@tok"
],
0,
"1c8b749cf6caaa886ade13d4de5134d2"
],
[
"Vale.Interop.X64.taint_arg_args_b8_mem",
1,
1,
0,
[ "@query" ],
0,
"e64aba902d468d8203981afdb3ff2e40"
],
[
"Vale.Interop.X64.taint_arg_args_b8_mem",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@query",
"FStar.List.Tot.Base_interpretation_Tm_ghost_arrow_d7e9834b8fd0407a723f5f3f4b012fdd",
"Vale.Interop.Base_interpretation_Tm_ghost_arrow_b4807c7d80613e9375ee60bb79d0087e",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"binder_x_49b65ff426cd1f25d61dfaad9d6052cd_0",
"binder_x_c8ae51e7e32588c3fc442c63c1bb566c_1",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit", "data_elim_Prims.Mkdtuple2",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_Vale.X64.Machine_s.Secret@tok",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil", "eq2-interp",
"equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.Base.args_b8",
"equation_Vale.Interop.Base.mut_to_b8",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.X64.arg_list",
"equation_Vale.Interop.X64.taint_arg_b8",
"equation_with_fuel_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"false_interp", "fuel_guarded_inversion_Prims.dtuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Interop.Base.td",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_Vale.Interop.Base.arg",
"interpretation_Tm_abs_a2786036ea22e3f98fc00d3061020b9d",
"kinding_Prims.list@tok", "l_or-interp",
"primitive_Prims.op_Addition", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_81ccb32c02ec946601a86ab897f3370e",
"refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"subterm_ordering_Prims.Cons",
"typing_Tm_abs_a2786036ea22e3f98fc00d3061020b9d",
"typing_Vale.Interop.Base.args_b8",
"typing_Vale.Interop.X64.taint_arg_b8"
],
0,
"9624d208c7962e6ef260d9e41aaa4588"
],
[
"Vale.Interop.X64.mk_taint_equiv",
1,
1,
0,
[ "@query" ],
0,
"ee6a8520038f9c12220ecf13cdaaa145"
],
[
"Vale.Interop.X64.mk_taint_equiv",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.BigOps.pairwise_op_.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_correspondence_FStar.List.Tot.Base.memP.fuel_instrumented",
"@fuel_irrelevance_FStar.BigOps.pairwise_op_.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.memP.fuel_instrumented",
"@query",
"FStar.BigOps_interpretation_Tm_ghost_arrow_4893cf450fdcb12f9a707dc878f6dac3",
"FStar.List.Tot.Base_interpretation_Tm_ghost_arrow_d7e9834b8fd0407a723f5f3f4b012fdd",
"Prims_interpretation_Tm_arrow_289ee2cc5874944bf725b9e3db8c0fd6",
"Vale.Def.Words.Four_s_interpretation_Tm_arrow_ca13e3f48edab78b734271373e04eb58",
"Vale.Interop.Base_interpretation_Tm_arrow_3b54e6762f20b0c8a1ed0db43e4767dd",
"Vale.Interop.X64_interpretation_Tm_ghost_arrow_d6f82824c3ba801ab0a4e5fe0071f859",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"binder_x_1cd5ca4beffacc47a478b6133a0431ac_0",
"binder_x_c8ae51e7e32588c3fc442c63c1bb566c_1",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"constructor_distinct_Tm_unit",
"constructor_distinct_Vale.Interop.Base.TD_Base",
"constructor_distinct_Vale.Interop.Base.TD_Buffer",
"constructor_distinct_Vale.Interop.Base.TD_ImmBuffer",
"data_elim_Prims.Mkdtuple2",
"data_typing_intro_Vale.X64.Machine_s.Secret@tok",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"disc_equation_Vale.Interop.Base.TD_Base",
"disc_equation_Vale.Interop.Base.TD_Buffer",
"disc_equation_Vale.Interop.Base.TD_ImmBuffer", "eq2-interp",
"equation_FStar.BigOps.map_op_",
"equation_FStar.BigOps.pairwise_and_", "equation_Prims.eq2",
"equation_Prims.l_True", "equation_Prims.logical",
"equation_Prims.squash", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.Base.disjoint_not_eq",
"equation_Vale.Interop.Base.disjoint_or_eq",
"equation_Vale.Interop.Base.disjoint_or_eq_1",
"equation_Vale.Interop.Base.ibuf_t",
"equation_Vale.Interop.Base.imm_to_b8",
"equation_Vale.Interop.Base.td_as_type",
"equation_Vale.Interop.Types.b8",
"equation_Vale.Interop.X64.arg_list_sb",
"equation_Vale.Interop.X64.mk_taint",
"equation_Vale.Interop.X64.taint_arg_b8",
"equation_Vale.Interop.X64.taint_map",
"equation_Vale.Interop.X64.taint_of_arg",
"equation_Vale.Interop.X64.upd_taint_map_arg",
"equation_Vale.Interop.X64.upd_taint_map_b8",
"equation_with_fuel_FStar.BigOps.pairwise_op_.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.fold_right_gtot.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"equation_with_fuel_FStar.List.Tot.Base.memP.fuel_instrumented",
"false_interp", "fuel_guarded_inversion_Prims.dtuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Interop.Base.td",
"fuel_guarded_inversion_Vale.Interop.Types.b8_",
"function_token_typing_Prims.l_True",
"function_token_typing_Prims.l_and",
"function_token_typing_Prims.logical",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.Interop.Base.disjoint_or_eq_1",
"function_token_typing_Vale.Interop.X64.upd_taint_map_arg",
"interpretation_Tm_abs_d457eaa84df0779f49818802d5572945",
"kinding_Tm_ghost_arrow_0ffaae0d0679fffbd6ed3d4448c53757",
"l_and-interp", "l_or-interp", "primitive_Prims.op_Addition",
"proj_equation_FStar.Pervasives.Native.Some_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"projection_inverse_Prims.Mkdtuple2__1",
"projection_inverse_Prims.Mkdtuple2__2",
"projection_inverse_Prims.Nil_a",
"projection_inverse_Vale.Interop.Base.TD_Base__0",
"projection_inverse_Vale.Interop.Base.TD_Buffer__0",
"projection_inverse_Vale.Interop.Base.TD_Buffer__1",
"projection_inverse_Vale.Interop.Base.TD_Buffer__2",
"projection_inverse_Vale.Interop.Base.TD_ImmBuffer__0",
"projection_inverse_Vale.Interop.Base.TD_ImmBuffer__1",
"projection_inverse_Vale.Interop.Base.TD_ImmBuffer__2",
"projection_inverse_Vale.Interop.Types.Buffer_bsrc",
"projection_inverse_Vale.Interop.Types.Buffer_src",
"projection_inverse_Vale.Interop.Types.Buffer_writeable",
"refinement_interpretation_Tm_refine_2c7ecebd8a41d0890aab4251b61d6458",
"refinement_interpretation_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"refinement_interpretation_Tm_refine_81ccb32c02ec946601a86ab897f3370e",
"refinement_interpretation_Tm_refine_85be0c420eb68f4e7a21abb89e018245",
"refinement_interpretation_Tm_refine_a09a35eaf316de2d2c4b28c7aed610ab",
"refinement_interpretation_Tm_refine_b1ecbb54de43c72e39a025eeadb88801",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_kinding_Tm_refine_703c6f879c5b001c36b204e25e1b2371",
"subterm_ordering_Prims.Cons", "token_correspondence_Prims.l_and",
"token_correspondence_Vale.Interop.X64.mk_taint",
"token_correspondence_Vale.Interop.X64.upd_taint_map_arg",
"typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
"typing_Prims.eq2", "typing_Vale.Interop.Base.imm_to_b8",
"typing_Vale.Interop.X64.init_taint",
"typing_Vale.Interop.X64.taint_arg_b8", "unit_inversion",
"unit_typing"
],
0,
"7fc02c90735640cfc5e8a38c3b2938fc"
],
[
"Vale.Interop.X64.create_initial_trusted_state",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.X64.Machine_s_pretyping_38835f297fb700457da67879cc31d6a6",
"bool_inversion", "equality_tok_Vale.X64.Machine_s.Public@tok",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arg_list",
"equation_Vale.X64.Machine_s.n_reg_files",
"equation_Vale.X64.Machine_s.n_regs",
"equation_Vale.X64.Machine_s.reg_file_id",
"equation_Vale.X64.Machine_s.reg_id",
"equation_Vale.X64.Machine_s.t_reg",
"equation_Vale.X64.Machine_s.t_reg_file",
"fuel_guarded_inversion_Vale.X64.Machine_s.reg",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Interop.Assumptions.init_regs",
"function_token_typing_Vale.Interop.X64.register_of_args",
"int_inversion", "kinding_Vale.X64.Machine_s.taint@tok",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomConstMap",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_empty",
"primitive_Prims.op_Negation",
"proj_equation_Vale.X64.Machine_s.Reg_rf",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0559236e7a05befcc7b6302f3642ad81",
"refinement_interpretation_Tm_refine_19df052c5be3a78e6dc7481200c8be37",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_610f1abe8da643877455975003828a15",
"refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0",
"refinement_interpretation_Tm_refine_d9979b96a3f2b18961b3dd63a2783b64",
"typing_FStar.Map.const", "typing_FStar.Map.domain",
"typing_FStar.Set.complement", "typing_FStar.Set.empty",
"typing_FStar.Set.mem",
"typing_Vale.X64.Machine_s.__proj__Reg__item__rf",
"typing_tok_Vale.X64.Machine_s.Public@tok"
],
0,
"f4090069773a51edec6208f254f7c431"
],
[
"Vale.Interop.X64.return_val_t",
1,
1,
0,
[ "@query" ],
0,
"0eac6fa91632801c0828f9488e27d24d"
],
[
"Vale.Interop.X64.return_val",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"2068f91134c406e39f83c861de0c6cfb"
],
[
"Vale.Interop.X64.prediction_post",
1,
1,
0,
[ "@query" ],
0,
"61ef5e0bb0b0ce2ea3bb951bc5a60249"
],
[
"Vale.Interop.X64.as_lowstar_sig_post",
1,
1,
0,
[ "@query", "equation_Vale.Interop.X64.prediction_pre" ],
0,
"2876e34d39002f728c2b8d2a3296b1d6"
],
[
"Vale.Interop.X64.as_lowstar_sig",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_31fb0c066152aad9773967074755b671"
],
0,
"7ff750e86f1b02da1b257ddd81be108c"
],
[
"Vale.Interop.X64.wrap_variadic",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.X64_interpretation_Tm_ghost_arrow_44657b0dc6094dfa0cb4d159b23c54a2",
"Vale.Interop.X64_interpretation_Tm_ghost_arrow_4f4cf7c0f62b3b7d68410e41fe1b0a1d",
"constructor_distinct_FStar.Pervasives.Native.Mktuple2",
"constructor_distinct_Tm_unit",
"data_typing_intro_Vale.Interop.X64.As_lowstar_sig_ret@tok",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.nat",
"equation_Vale.Interop.Base.mem_roots",
"equation_Vale.Interop.X64.as_lowstar_sig_post",
"equation_Vale.Interop.X64.create_initial_trusted_state",
"equation_Vale.Interop.X64.prediction",
"equation_Vale.Interop.X64.prediction_post",
"equation_Vale.Interop.X64.prediction_pre",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple3",
"fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_",
"int_inversion",
"interpretation_Tm_abs_c89261782627dd11bdd84e5ca9256e4e",
"kinding_Vale.Interop.Heap_s.interop_heap@tok",
"kinding_Vale.Interop.X64.as_lowstar_sig_ret@tok",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"lemma_FStar.Ghost.reveal_hide",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Vale.Interop.X64.As_lowstar_sig_ret_args",
"proj_equation_Vale.Interop.X64.As_lowstar_sig_ret_final_mem",
"proj_equation_Vale.Interop.X64.As_lowstar_sig_ret_fuel",
"proj_equation_Vale.Interop.X64.As_lowstar_sig_ret_n",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_Vale.Interop.X64.As_lowstar_sig_ret_args",
"projection_inverse_Vale.Interop.X64.As_lowstar_sig_ret_final_mem",
"projection_inverse_Vale.Interop.X64.As_lowstar_sig_ret_fuel",
"projection_inverse_Vale.Interop.X64.As_lowstar_sig_ret_n",
"refinement_interpretation_Tm_refine_31fb0c066152aad9773967074755b671",
"refinement_interpretation_Tm_refine_427964005be28d37845727035e1dec26",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9830ee27acdcae7bf2ebc8334f96d818",
"refinement_interpretation_Tm_refine_a3541cbaa1e5d11c6f771b017004cb9c",
"refinement_interpretation_Tm_refine_aedc138702446b65fd6f58c5f54c76e5",
"refinement_interpretation_Tm_refine_e7cbd317e4d64bcd92cf380f399d4bb7",
"refinement_interpretation_Tm_refine_efd0f8a81ce2caa3973fda37b5c108c1",
"token_correspondence_Vale.Interop.X64.create_initial_trusted_state",
"typing_FStar.Pervasives.Native.fst",
"typing_Tm_abs_c89261782627dd11bdd84e5ca9256e4e"
],
0,
"071aa037b424ce584c62a4035785bf31"
],
[
"Vale.Interop.X64.rel_gen_t",
1,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "binder_x_419a1f9cfe95c45ddf8352069090c461_3",
"binder_x_539449a65710b411a0d6ba2b5dcd2e3e_2",
"constructor_distinct_Prims.Cons", "disc_equation_Prims.Cons",
"disc_equation_Prims.Nil", "equation_Prims.nat",
"equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arg_list",
"equation_Vale.Interop.X64.op_Plus_Plus",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"function_token_typing_Vale.Interop.Base.arg",
"kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7f4d02dbd27ce887ddfabaa0a6cb4e3f",
"refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0",
"subterm_ordering_Prims.Cons",
"token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"typing_Vale.Interop.X64.op_Plus_Plus"
],
0,
"588866ed5cb30e295d503b3dcaa0f103"
],
[
"Vale.Interop.X64.elim_rel_gen_t_cons",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Cons",
"data_typing_intro_Prims.Cons@tok", "equation_Prims.nat",
"equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arg_list",
"equation_Vale.Interop.X64.op_Plus_Plus",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0",
"refinement_interpretation_Tm_refine_ee32529582ab288f5f4d513adc54182a",
"token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"typing_Vale.Interop.X64.op_Plus_Plus"
],
0,
"3e0b6e4f4802521668b6190e9b9bb6d6"
],
[
"Vale.Interop.X64.prediction_t",
1,
1,
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,
"c504f42d8348c1891b25db8742b654d1"
],
[
"Vale.Interop.X64.prediction_t",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_correspondence_Vale.Interop.X64.rel_gen_t.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.X64_interpretation_Tm_arrow_c500d95a1aae296c9b882c37ef8e9551",
"Vale.Interop.X64_interpretation_Tm_arrow_d4536d6667b09fb97c97e4fd518201d7",
"binder_x_07bf7a800fe5b6f7326c4a1398117bb8_8",
"binder_x_539449a65710b411a0d6ba2b5dcd2e3e_5",
"binder_x_7cb5666207c5130a392b3a823a693392_6",
"binder_x_97ef5ff619e486c846fe112d821f649f_4",
"binder_x_a2968b5aedabccc4f9a87ef4627271f7_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_c9a5b2c01f528cab5ea8751bf4318890_7",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Prims.nat", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arg_list",
"equation_Vale.Interop.X64.op_Plus_Plus",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"equation_with_fuel_Vale.Interop.X64.rel_gen_t.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.Interop.X64.prediction_post_rel_t",
"function_token_typing_Vale.Interop.X64.prediction_pre_rel_t",
"int_inversion", "kinding_Vale.Interop.Base.td@tok",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_183fa7eb53b3817742e19ea929ff4910",
"refinement_interpretation_Tm_refine_27d2df70cea38c5a8832d2b54b387e26",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6ff49fd1edd7220d4f3ccd4421aaa025",
"refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0",
"subterm_ordering_Prims.Cons",
"token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"token_correspondence_Vale.Interop.X64.prediction_post_rel_t",
"token_correspondence_Vale.Interop.X64.prediction_pre_rel_t",
"typing_Vale.Interop.X64.op_Plus_Plus"
],
0,
"d04925b760d91419f0506e5c80f4ac3f"
],
[
"Vale.Interop.X64.prediction_t",
3,
1,
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,
"b1084972423ee683ce1c384aa9085b25"
],
[
"Vale.Interop.X64.elim_predict_t_nil",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok",
"equation_Vale.Interop.X64.arg_list",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"kinding_Vale.Interop.Base.td@tok",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0"
],
0,
"15b8c795f482088b2413cf56390416d9"
],
[
"Vale.Interop.X64.elim_predict_t_cons",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.Base_pretyping_2f6f4dabbf5d6144c841ea9fcae77848",
"constructor_distinct_Prims.Cons",
"data_typing_intro_Prims.Cons@tok",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"refinement_interpretation_Tm_refine_41c6a2194855737ab1ee36516ff41a5e"
],
0,
"a8c6da737afcef20d5f050ec5b85e9f2"
],
[
"Vale.Interop.X64.elim_predict_t_cons",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Cons",
"data_typing_intro_Prims.Cons@tok", "equation_Prims.nat",
"equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arg_list",
"equation_Vale.Interop.X64.op_Plus_Plus",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"kinding_Vale.Interop.Base.td@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"refinement_interpretation_Tm_refine_41c6a2194855737ab1ee36516ff41a5e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0",
"typing_FStar.List.Tot.Base.length",
"typing_Vale.Interop.X64.op_Plus_Plus"
],
0,
"c395a94c1b2650c48d859ff924c5b0a0"
],
[
"Vale.Interop.X64.as_lowstar_sig_t",
1,
1,
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,
"1b6cfbfa063fbbaa808a4285ee722aa5"
],
[
"Vale.Interop.X64.as_lowstar_sig_t",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_correspondence_Vale.Interop.X64.rel_gen_t.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.X64_interpretation_Tm_arrow_c500d95a1aae296c9b882c37ef8e9551",
"Vale.Interop.X64_interpretation_Tm_arrow_d4536d6667b09fb97c97e4fd518201d7",
"binder_x_539449a65710b411a0d6ba2b5dcd2e3e_5",
"binder_x_5af8168932a4bf3947dc018963e66e23_8",
"binder_x_66831f94ffcc1a2a32f7393d1a9f2388_6",
"binder_x_97ef5ff619e486c846fe112d821f649f_4",
"binder_x_a2968b5aedabccc4f9a87ef4627271f7_1",
"binder_x_b9f940dce8bb49bea5d289cc241fd504_7",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Prims.nat", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arg_list",
"equation_Vale.Interop.X64.op_Plus_Plus",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"equation_with_fuel_Vale.Interop.X64.rel_gen_t.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.Interop.X64.prediction_post_rel_t",
"function_token_typing_Vale.Interop.X64.prediction_pre_rel_t",
"int_inversion", "kinding_Vale.Interop.Base.td@tok",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_183fa7eb53b3817742e19ea929ff4910",
"refinement_interpretation_Tm_refine_27d2df70cea38c5a8832d2b54b387e26",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0",
"refinement_interpretation_Tm_refine_a31f7a9e4f73955bed5763b111fc28da",
"refinement_interpretation_Tm_refine_b024999814ba64acd5a9575e2d26ee00",
"subterm_ordering_Prims.Cons",
"token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"token_correspondence_Vale.Interop.X64.prediction_post_rel_t",
"token_correspondence_Vale.Interop.X64.prediction_pre_rel_t",
"typing_Vale.Interop.X64.op_Plus_Plus"
],
0,
"c8987ac0ef5c048cb0690a5357d0ff62"
],
[
"Vale.Interop.X64.as_lowstar_sig_t",
3,
1,
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,
"803843e99f1f5fb4db8574a9fe58658e"
],
[
"Vale.Interop.X64.wrap_aux",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@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",
"kinding_Vale.Interop.Base.td@tok",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c289d1660fd1af0575d3ae62d7f9de71",
"typing_FStar.List.Tot.Base.length"
],
0,
"3a9451e931f6f9bdb85c32bc50fe3273"
],
[
"Vale.Interop.X64.wrap_aux",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_correspondence_Vale.Interop.X64.rel_gen_t.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.X64_interpretation_Tm_arrow_094cffd6b008f86820e77aea17a251f5",
"Vale.Interop.X64_interpretation_Tm_arrow_9cbac494a47f7def70a027d5494bb917",
"Vale.Interop.X64_interpretation_Tm_arrow_c500d95a1aae296c9b882c37ef8e9551",
"Vale.Interop.X64_interpretation_Tm_arrow_d4536d6667b09fb97c97e4fd518201d7",
"binder_x_0ab31921e53c31b3d0553d0dc91d1f61_8",
"binder_x_539449a65710b411a0d6ba2b5dcd2e3e_5",
"binder_x_71f892a0e85507a0e6bcd4bb506ce2af_6",
"binder_x_97ef5ff619e486c846fe112d821f649f_4",
"binder_x_a2968b5aedabccc4f9a87ef4627271f7_1",
"binder_x_a99b3e1b3ee33581bc2caa29083fff1b_7",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Prims.nat", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arg_list",
"equation_Vale.Interop.X64.elim_rel_gen_t_nil",
"equation_Vale.Interop.X64.op_Plus_Plus",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"equation_with_fuel_Vale.Interop.X64.rel_gen_t.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.Interop.X64.prediction_post_rel_t",
"function_token_typing_Vale.Interop.X64.prediction_pre_rel_t",
"int_inversion", "kinding_Vale.Interop.Base.td@tok",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"refinement_interpretation_Tm_refine_183fa7eb53b3817742e19ea929ff4910",
"refinement_interpretation_Tm_refine_27d2df70cea38c5a8832d2b54b387e26",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0",
"refinement_interpretation_Tm_refine_aab1f6c3af5a5d18fbf1f6c548d272de",
"refinement_interpretation_Tm_refine_cf180dee30a3514b7c9a5a7000d8334e",
"refinement_interpretation_Tm_refine_f6e3e083abdf41ba5cdfcdbf53bd59b4",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Interop.X64.elim_rel_gen_t_nil",
"token_correspondence_Vale.Interop.X64.prediction_post_rel_t",
"token_correspondence_Vale.Interop.X64.prediction_pre_rel_t",
"typing_FStar.List.Tot.Base.length",
"typing_Tm_abs_3f50ee6e2ed0fdae3704b80b11005055",
"typing_Vale.Interop.X64.op_Plus_Plus"
],
0,
"d42df431a00cd713a3993d6f57d3b8d2"
],
[
"Vale.Interop.X64.wrap_aux",
3,
1,
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,
"fa64b5cc5e4943a8893a83a1507e765f"
],
[
"Vale.Interop.X64.wrap'",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "equation_Vale.Interop.Base.arg",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b"
],
0,
"3e324efa8c58f801ad2c4a0e50614b3f"
],
[
"Vale.Interop.X64.wrap'",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "equation_Vale.Interop.Base.arg",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b"
],
0,
"e0daeeef04f1ba9c71a9e34659eb1938"
],
[
"Vale.Interop.X64.wrap'",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "equation_Vale.Interop.Base.arg",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b"
],
0,
"4fab85ff83df118068db6683a4d18880"
],
[
"Vale.Interop.X64.as_lowstar_sig_t_weak'",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@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",
"kinding_Vale.Interop.Base.td@tok",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c289d1660fd1af0575d3ae62d7f9de71",
"typing_FStar.List.Tot.Base.length"
],
0,
"ddb4217994ce4c0119ff74cd652956a2"
],
[
"Vale.Interop.X64.as_lowstar_sig_t_weak'",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_correspondence_Vale.Interop.X64.rel_gen_t.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.X64_interpretation_Tm_arrow_c500d95a1aae296c9b882c37ef8e9551",
"Vale.Interop.X64_interpretation_Tm_arrow_d4536d6667b09fb97c97e4fd518201d7",
"binder_x_0ab31921e53c31b3d0553d0dc91d1f61_8",
"binder_x_539449a65710b411a0d6ba2b5dcd2e3e_5",
"binder_x_71f892a0e85507a0e6bcd4bb506ce2af_6",
"binder_x_97ef5ff619e486c846fe112d821f649f_4",
"binder_x_a2968b5aedabccc4f9a87ef4627271f7_1",
"binder_x_a99b3e1b3ee33581bc2caa29083fff1b_7",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_Prims.nat", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arg_list",
"equation_Vale.Interop.X64.op_Plus_Plus",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"equation_with_fuel_Vale.Interop.X64.rel_gen_t.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.Interop.X64.prediction_post_rel_t",
"function_token_typing_Vale.Interop.X64.prediction_pre_rel_t",
"int_inversion", "kinding_Vale.Interop.Base.td@tok",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_183fa7eb53b3817742e19ea929ff4910",
"refinement_interpretation_Tm_refine_27d2df70cea38c5a8832d2b54b387e26",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0",
"refinement_interpretation_Tm_refine_cf180dee30a3514b7c9a5a7000d8334e",
"refinement_interpretation_Tm_refine_f6e3e083abdf41ba5cdfcdbf53bd59b4",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Interop.X64.prediction_post_rel_t",
"token_correspondence_Vale.Interop.X64.prediction_pre_rel_t",
"typing_FStar.List.Tot.Base.length",
"typing_Vale.Interop.X64.op_Plus_Plus"
],
0,
"f79bbf12229cb1eb0c19c91c09dce731"
],
[
"Vale.Interop.X64.as_lowstar_sig_t_weak'",
3,
1,
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,
"1edd56213133ada1cdd04beb27cb5175"
],
[
"Vale.Interop.X64.wrap_aux_weak",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@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",
"kinding_Vale.Interop.Base.td@tok",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c289d1660fd1af0575d3ae62d7f9de71",
"typing_FStar.List.Tot.Base.length"
],
0,
"b3b17bf98dcac5531967f0916a19abb9"
],
[
"Vale.Interop.X64.wrap_aux_weak",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@fuel_correspondence_Vale.Interop.X64.rel_gen_t.fuel_instrumented",
"@fuel_irrelevance_FStar.List.Tot.Base.length.fuel_instrumented",
"@query",
"Vale.Interop.X64_interpretation_Tm_arrow_33afdcf6a0b392aeb39811347623ec9c",
"Vale.Interop.X64_interpretation_Tm_arrow_7ce33a73121f98da3b5328c0b8dab0d3",
"Vale.Interop.X64_interpretation_Tm_arrow_980b79c62767264e2d550623d192cfbc",
"Vale.Interop.X64_interpretation_Tm_arrow_c500d95a1aae296c9b882c37ef8e9551",
"Vale.Interop.X64_interpretation_Tm_arrow_d4536d6667b09fb97c97e4fd518201d7",
"Vale.Interop.X64_interpretation_Tm_ghost_arrow_b9642c00164ecb8b7f18f2a75fdd241c",
"binder_x_0ab31921e53c31b3d0553d0dc91d1f61_8",
"binder_x_539449a65710b411a0d6ba2b5dcd2e3e_5",
"binder_x_71f892a0e85507a0e6bcd4bb506ce2af_6",
"binder_x_97ef5ff619e486c846fe112d821f649f_4",
"binder_x_a2968b5aedabccc4f9a87ef4627271f7_1",
"binder_x_a99b3e1b3ee33581bc2caa29083fff1b_7",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"constructor_distinct_Prims.Cons", "constructor_distinct_Prims.Nil",
"data_elim_FStar.Pervasives.Native.Some",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_Prims.Cons", "disc_equation_Prims.Nil",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Pervasives.Native.fst", "equation_Prims.nat",
"equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.Base.mem_roots",
"equation_Vale.Interop.X64.als_ret",
"equation_Vale.Interop.X64.arg_list",
"equation_Vale.Interop.X64.as_lowstar_sig_post",
"equation_Vale.Interop.X64.as_lowstar_sig_post_weak",
"equation_Vale.Interop.X64.elim_predict_t_nil",
"equation_Vale.Interop.X64.elim_rel_gen_t_nil",
"equation_Vale.Interop.X64.op_Plus_Plus",
"equation_Vale.Interop.X64.prediction_post",
"equation_Vale.Interop.X64.state_builder_t",
"equation_Vale.X64.Machine_Semantics_s.code",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"equation_with_fuel_Vale.Interop.X64.rel_gen_t.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_Vale.Interop.X64.arg_reg_relation_",
"function_token_typing_FStar.UInt64.t",
"function_token_typing_Vale.Interop.Base.arg",
"function_token_typing_Vale.Interop.X64.create_initial_trusted_state",
"function_token_typing_Vale.Interop.X64.prediction_post_rel_t",
"function_token_typing_Vale.Interop.X64.prediction_pre_rel_t",
"int_inversion", "kinding_Vale.Interop.Base.td@tok",
"kinding_Vale.Interop.Heap_s.interop_heap@tok",
"kinding_Vale.Interop.X64.as_lowstar_sig_ret@tok",
"kinding_Vale.X64.Machine_Semantics_s.machine_state@tok",
"primitive_Prims.op_Addition",
"proj_equation_FStar.Pervasives.Native.Some_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_Prims.Cons_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl",
"refinement_interpretation_Tm_refine_183fa7eb53b3817742e19ea929ff4910",
"refinement_interpretation_Tm_refine_27d2df70cea38c5a8832d2b54b387e26",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9830ee27acdcae7bf2ebc8334f96d818",
"refinement_interpretation_Tm_refine_9efdbb0756b059e2036eecbec13c6ae0",
"refinement_interpretation_Tm_refine_aab1f6c3af5a5d18fbf1f6c548d272de",
"refinement_interpretation_Tm_refine_aedc138702446b65fd6f58c5f54c76e5",
"refinement_interpretation_Tm_refine_cf180dee30a3514b7c9a5a7000d8334e",
"refinement_interpretation_Tm_refine_f6e3e083abdf41ba5cdfcdbf53bd59b4",
"subterm_ordering_Prims.Cons",
"token_correspondence_Vale.Interop.X64.create_initial_trusted_state",
"token_correspondence_Vale.Interop.X64.elim_rel_gen_t_nil",
"token_correspondence_Vale.Interop.X64.prediction_post_rel_t",
"token_correspondence_Vale.Interop.X64.prediction_pre_rel_t",
"typing_FStar.Ghost.erased", "typing_FStar.Ghost.reveal",
"typing_FStar.List.Tot.Base.length",
"typing_FStar.Pervasives.Native.__proj__Mktuple2__item___1",
"typing_FStar.Pervasives.Native.snd",
"typing_Tm_abs_94ccf6309093b3b002127c057db2dfa7",
"typing_Vale.Interop.X64.__proj__As_lowstar_sig_ret__item__final_mem",
"typing_Vale.Interop.X64.__proj__As_lowstar_sig_ret__item__fuel",
"typing_Vale.Interop.X64.op_Plus_Plus",
"typing_Vale.X64.Machine_Semantics_s.machine_eval_code"
],
0,
"e2318218c67ea620cd9b6eae7f495f71"
],
[
"Vale.Interop.X64.wrap_aux_weak",
3,
1,
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,
"4d8ea6f5822d667954787be924348469"
],
[
"Vale.Interop.X64.wrap_weak'",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "equation_Vale.Interop.Base.arg",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b"
],
0,
"5073194a4295736a01cb4197a80511fe"
],
[
"Vale.Interop.X64.wrap_weak'",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "equation_Vale.Interop.Base.arg",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b"
],
0,
"809305d3059ed3985e67f66722efa495"
],
[
"Vale.Interop.X64.wrap_weak'",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "equation_Vale.Interop.Base.arg",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_5509ec561ba73ab2bcb6cca1d1c4673b"
],
0,
"7f754b021f17544f85ef77e32401d6a1"
],
[
"Vale.Interop.X64.as_lowstar_sig_t_weak",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "equation_Prims.nat", "kinding_Vale.Interop.Base.td@tok",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9c77630db93706b12998369544649e46",
"refinement_interpretation_Tm_refine_d1d8f590ca65fc47bf004e71761d3452",
"typing_FStar.List.Tot.Base.length"
],
0,
"e846b9de5d1c7ecd292eaf95a7816100"
],
[
"Vale.Interop.X64.as_lowstar_sig_t_weak",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_d1d8f590ca65fc47bf004e71761d3452"
],
0,
"4eaa2086ad6f895b481e99669232b229"
],
[
"Vale.Interop.X64.wrap_weak",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
"@query", "constructor_distinct_Prims.Nil",
"data_typing_intro_Prims.Nil@tok", "equation_Vale.Interop.Base.arg",
"equation_Vale.Interop.X64.arity_ok",
"equation_with_fuel_FStar.List.Tot.Base.length.fuel_instrumented",
"function_token_typing_Vale.Interop.Base.arg",
"projection_inverse_BoxInt_proj_0", "projection_inverse_Prims.Nil_a",
"refinement_interpretation_Tm_refine_b8c08cb8894cdb660d32da1093433103",
"refinement_interpretation_Tm_refine_d1d8f590ca65fc47bf004e71761d3452"
],
0,
"d084852f3cf53c936d91735b23860ea3"
],
[
"Vale.Interop.X64.wrap_weak",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_d1d8f590ca65fc47bf004e71761d3452"
],
0,
"0b28a5aeccf8fa21f17853f4a24f6d6f"
],
[
"Vale.Interop.X64.register_of_arg_i",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Interop.X64.reg_nat", "int_inversion",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"0b5aec385eac070b495c5870d05d9d07"
],
[
"Vale.Interop.X64.arg_of_register",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"c57065dd1c753744d67bd9160fbe4015"
],
[
"Vale.Interop.X64.arg_reg_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.X64_interpretation_Tm_arrow_2d6da19097b39247da65144806c55e59",
"Vale.Interop.X64_interpretation_Tm_arrow_2edbb0578f9dff3b4204c811921185bb",
"Vale.Interop.X64_interpretation_Tm_arrow_7b93b99fb8000cd672145629f584ce31",
"bool_inversion", "constructor_distinct_BoxInt",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Tm_unit",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat2", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Interop.X64.arg_of_register",
"equation_Vale.Interop.X64.max_stdcall",
"equation_Vale.Interop.X64.reg_nat",
"equation_Vale.Interop.X64.register_of_arg_i",
"equation_Vale.X64.Machine_s.reg_64",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat2",
"function_token_typing_Vale.Interop.X64.__proj__Rel__item__of_arg",
"function_token_typing_Vale.Interop.X64.arg_of_register",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c365eb902b454950de62fba701d9049d", "int_inversion",
"lemma_FStar.Pervasives.invertOption",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_Vale.Interop.X64.Rel_of_arg",
"proj_equation_Vale.Interop.X64.Rel_of_reg",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"projection_inverse_Vale.Interop.X64.Rel_of_arg",
"projection_inverse_Vale.Interop.X64.Rel_of_reg",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a",
"refinement_interpretation_Tm_refine_5035dbea9ab31384d60f7061d33efd0e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c365eb902b454950de62fba701d9049d",
"token_correspondence_Vale.Interop.X64.__proj__Rel__item__of_arg",
"token_correspondence_Vale.Interop.X64.__proj__Rel__item__of_reg",
"token_correspondence_Vale.Interop.X64.arg_of_register",
"token_correspondence_Vale.Interop.X64.register_of_arg_i",
"typing_FStar.Pervasives.Native.__proj__Some__item__v",
"typing_Vale.Interop.X64.arg_of_register",
"typing_Vale.Interop.X64.max_stdcall",
"typing_Vale.Interop.X64.reg_nat",
"typing_Vale.Interop.X64.register_of_arg_i"
],
0,
"7e92262bc480e0c326d664bfd28ae1b8"
],
[
"Vale.Interop.X64.regs_modified_stdcall",
1,
1,
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,
"4f0609fef78d3664f35a7a5840a57e0a"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...