Revision cef6a8e821f55e71b791555d22b45bd3debc2596 authored by Jonathan Protzenko on 08 May 2020, 16:26:29 UTC, committed by GitHub on 08 May 2020, 16:26:29 UTC
OCaml API: Don't run unit tests which require unsupported features
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,
"a4fe0c5542a5eec10422b9e3497347b7"
],
[
"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,
"b0cc20b6e1375e22daf38886f20da2f5"
],
[
"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,
"600a8bf47e9530ee57cadfdb67d9b457"
],
[
"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,
"fbfefcb1c47556727a5cf5d96ddec88d"
],
[
"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,
"1df887b444bffd43b532fb6ea4710c67"
],
[
"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,
"055dc7d916b60a8b26ab4abbaf04ff66"
],
[
"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_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.b8_preorder",
"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", "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",
"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",
"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",
"typing_Vale.Interop.Base.__proj__TD_Base__item___0"
],
0,
"abcb71295bc481d7f404a9423fde8298"
],
[
"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,
"75d7c75caf93d1c30c3ce4975a1b3c36"
],
[
"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,
"9881bb3d7eb6ab191f551f0bad92ce73"
],
[
"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,
"0194f67e74db53c5232fcd8717ef50cb"
],
[
"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,
"f36d6f3ead53ac392bdde394c2bf6b8e"
],
[
"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,
"dd59b1e444bd1f921c983fff4464c966"
],
[
"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,
"28f6c05feafb673f64c472702b99d8bd"
],
[
"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,
"66d708701fc88aae8485babba7d68faf"
],
[
"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,
"c3b16d3006148c79784fde89945ef290"
],
[
"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,
"16bc1c842954b44fade6f2e62394b6d8"
],
[
"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_Vale.Interop.Base.arg",
"equation_Vale.Interop.Types.b8_preorder",
"fuel_guarded_inversion_Prims.dtuple2",
"fuel_guarded_inversion_Vale.Interop.Base.td",
"proj_equation_Prims.Mkdtuple2__1"
],
0,
"eca239792ec567d776981b421faf8735"
],
[
"Vale.Interop.X64.taint_arg_b8",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"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.Arch.HeapTypes_s.Public@tok",
"equation_Vale.Interop.Base.buf_t",
"equation_Vale.Interop.Base.ibuf_t",
"equation_Vale.Interop.Base.td_as_type",
"equation_Vale.Interop.Types.b8_preorder",
"equation_Vale.Interop.X64.taint_of_arg",
"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",
"refinement_interpretation_Tm_refine_1665f1ce84843a1b3ee2b366c7c855b4",
"refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80",
"refinement_interpretation_Tm_refine_affb1db09d141d21b1ea1c7345183b10",
"typing_tok_Vale.Arch.HeapTypes_s.Public@tok"
],
0,
"a0709dcc273d1a99354de3cd1d5ece9a"
],
[
"Vale.Interop.X64.taint_arg_args_b8_mem",
1,
1,
0,
[ "@query" ],
0,
"b8716afde00a9b7460651f9f1a3ddea8"
],
[
"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.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"Vale.Interop.Base_interpretation_Tm_ghost_arrow_b4807c7d80613e9375ee60bb79d0087e",
"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.Arch.HeapTypes_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.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", "kinding_Vale.Interop.Types.b8@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_9efdbb0756b059e2036eecbec13c6ae0",
"refinement_interpretation_Tm_refine_affb1db09d141d21b1ea1c7345183b10",
"subterm_ordering_Prims.Cons",
"typing_Tm_abs_a2786036ea22e3f98fc00d3061020b9d",
"typing_Vale.Interop.Base.args_b8",
"typing_Vale.Interop.X64.taint_arg_b8"
],
0,
"245268c36b15518a1619d297e906b050"
],
[
"Vale.Interop.X64.mk_taint_equiv",
1,
1,
0,
[ "@query" ],
0,
"65158d7b42ffeab6d104ca1f627965bd"
],
[
"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.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"Vale.Def.Words.Four_s_interpretation_Tm_arrow_ca13e3f48edab78b734271373e04eb58",
"Vale.Interop.Base_interpretation_Tm_arrow_3b54e6762f20b0c8a1ed0db43e4767dd",
"Vale.Interop.Types_pretyping_cc6beaf9e2624d0643670c917b6f53e1",
"Vale.Interop.X64_interpretation_Tm_ghost_arrow_d6f82824c3ba801ab0a4e5fe0071f859",
"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.Arch.HeapTypes_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.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_89e176a9e84a687a65f35a76255cd46e",
"kinding_Tm_ghost_arrow_6b4b417e1383ee3b4792f0b5428180ab",
"kinding_Vale.Interop.Types.b8@tok", "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_1665f1ce84843a1b3ee2b366c7c855b4",
"refinement_interpretation_Tm_refine_2c7ecebd8a41d0890aab4251b61d6458",
"refinement_interpretation_Tm_refine_85be0c420eb68f4e7a21abb89e018245",
"refinement_interpretation_Tm_refine_affb1db09d141d21b1ea1c7345183b10",
"refinement_interpretation_Tm_refine_b1ecbb54de43c72e39a025eeadb88801",
"refinement_kinding_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"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,
"092759c6bfd3120d6130841bf9e3d23e"
],
[
"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.Arch.HeapTypes_s_pretyping_b2ecc36deaf346c775ae2b728a51b51e",
"bool_inversion", "equality_tok_Vale.Arch.HeapTypes_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.Arch.HeapTypes_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",
"projection_inverse_Vale.X64.Machine_s.Reg_rf",
"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.Arch.HeapTypes_s.Public@tok"
],
0,
"b9d1f343fb56f27a6ef83b8c4e43c481"
],
[
"Vale.Interop.X64.return_val_t",
1,
1,
0,
[ "@query" ],
0,
"c5c520302ef99444b53ddf3e5d05625a"
],
[
"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,
"894391fd220da80b0e639a48be70784f"
],
[
"Vale.Interop.X64.prediction_post",
1,
1,
0,
[ "@query" ],
0,
"aa47d92a132772d58b4942a54d05c87b"
],
[
"Vale.Interop.X64.as_lowstar_sig_post",
1,
1,
0,
[ "@query", "equation_Vale.Interop.X64.prediction_pre" ],
0,
"bcd142e71740b42814c6a65cf1bae279"
],
[
"Vale.Interop.X64.as_lowstar_sig",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_31fb0c066152aad9773967074755b671"
],
0,
"a8e31a30f758d552b291c779246da1f3"
],
[
"Vale.Interop.X64.wrap_variadic",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.X64_interpretation_Tm_ghost_arrow_0d4779e4452bcc98cf90aa3d3290d68f",
"Vale.Interop.X64_interpretation_Tm_ghost_arrow_44657b0dc6094dfa0cb4d159b23c54a2",
"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_3f90fa33cc8dc8eb12be164f44f029dc",
"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_efd0f8a81ce2caa3973fda37b5c108c1",
"refinement_interpretation_Tm_refine_f416aaa513efc2872a5219f88f959c6a",
"token_correspondence_Vale.Interop.X64.create_initial_trusted_state",
"typing_FStar.Pervasives.Native.fst",
"typing_Tm_abs_3f90fa33cc8dc8eb12be164f44f029dc"
],
0,
"ccfe8e50a08dc3df3184dcb976373f4a"
],
[
"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,
"cf60d61148e9815da6be0403784f0660"
],
[
"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,
"ce00655121fa06fecc122e482c83351a"
],
[
"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,
"944f1fbb4933505afd0d309be3a91a86"
],
[
"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,
"abe7a90a27c9a7c07c3e7b0fdf05edda"
],
[
"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,
"d6a69204f9e61912b717f52027d1f7cb"
],
[
"Vale.Interop.X64.prediction_t",
4,
1,
0,
[ "@query" ],
0,
"93bf09cd74e8d5469194bee38ab0e2d1"
],
[
"Vale.Interop.X64.prediction_t",
5,
1,
0,
[ "@query" ],
0,
"7ea45f77f04ffab58cf58b052bf2aab3"
],
[
"Vale.Interop.X64.prediction_t",
6,
1,
0,
[ "@query" ],
0,
"a39e890e1e5fd77aa7d87c718fe07d5d"
],
[
"Vale.Interop.X64.prediction_t",
7,
1,
0,
[ "@query" ],
0,
"0025e00cc2758e842acf0d4a43db52c3"
],
[
"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,
"531d4afdc57b323c8ac71112c287d71d"
],
[
"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,
"ee605b77b464e265cc004b5d75f043e3"
],
[
"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,
"00a14414c5ded5d30da99b2942c7f5c1"
],
[
"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,
"c1c86357ef3194f1612068de768bb3be"
],
[
"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,
"1bd4cdb8c24194340523a514c249e558"
],
[
"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,
"df3ad0694c6c976121d0ce6a9fbe4ce6"
],
[
"Vale.Interop.X64.as_lowstar_sig_t",
4,
1,
0,
[ "@query" ],
0,
"f90055d395c27d730e696e8cf2309242"
],
[
"Vale.Interop.X64.as_lowstar_sig_t",
5,
1,
0,
[ "@query" ],
0,
"42194c39713f8841a54ec98946e474dc"
],
[
"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,
"8a92804873bda60cd80c3c6836939a6d"
],
[
"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,
"d6db20d4db92dc04d32140d05105b505"
],
[
"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,
"62f706d329fcc387513e25cebf291dc7"
],
[
"Vale.Interop.X64.wrap_aux",
4,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"ee8f56b6a2fb518c3e588403c39ff108"
],
[
"Vale.Interop.X64.wrap_aux",
5,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"2b5289d1d7282957b712783f58ca23f3"
],
[
"Vale.Interop.X64.wrap_aux",
6,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"f497b4359ac7fda2b92cb5cd5a816371"
],
[
"Vale.Interop.X64.wrap_aux",
7,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"c597fdf262194d765c633bb65a80be09"
],
[
"Vale.Interop.X64.wrap_aux",
8,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"8367148e90f2f6eac047d546e8c610b7"
],
[
"Vale.Interop.X64.wrap_aux",
9,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"2fa4910854b0892c9ead9cda6c095531"
],
[
"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,
"7db275fb0b064a22df7204a219b5bdfe"
],
[
"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,
"8cd6bad4b0630823ad865677a176fba7"
],
[
"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,
"ed072e82524f0310ac7e171907df5b6d"
],
[
"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,
"7b50bcdee8d88e13dd8308f50a8c5d8e"
],
[
"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,
"b231f727dc0b04959c22d3707bbff470"
],
[
"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,
"869f81f82cee532992f1a13e0a3b2665"
],
[
"Vale.Interop.X64.as_lowstar_sig_t_weak'",
4,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"3bc959bb89a61ff51f49c2e9c347ef4d"
],
[
"Vale.Interop.X64.as_lowstar_sig_t_weak'",
5,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"5112b8e54f71087889cccf9922810bbc"
],
[
"Vale.Interop.X64.as_lowstar_sig_t_weak'",
6,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"f6759d44e9aad4a436e7b59e917bde52"
],
[
"Vale.Interop.X64.as_lowstar_sig_t_weak'",
7,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"a0ea50a05d781f5ba78c9b0237b10679"
],
[
"Vale.Interop.X64.as_lowstar_sig_t_weak'",
8,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"05aa28d058dbad63a8d8858a48412415"
],
[
"Vale.Interop.X64.as_lowstar_sig_t_weak'",
9,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"028860744af8c5312552f04f02ca7c67"
],
[
"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,
"0a0f792f8097b5be5f7e4878f10a28cd"
],
[
"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.eqtype",
"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_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_414d0a9f578ab0048252f8c8f552b99f",
"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_FStar.UInt64.t",
"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,
"e84fe8c1d23daeb99aabcbbd10fdec86"
],
[
"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,
"4705e02c75a6a8dcfaa6d45343e643a9"
],
[
"Vale.Interop.X64.wrap_aux_weak",
4,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"ffd8fa37558e8fab09982608e29ca272"
],
[
"Vale.Interop.X64.wrap_aux_weak",
5,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"aa3e664854814b5732cfbc4ed6357d27"
],
[
"Vale.Interop.X64.wrap_aux_weak",
6,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"806f31566ae561c2e5c2c28fb1775624"
],
[
"Vale.Interop.X64.wrap_aux_weak",
7,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"e683af51d5851c485fe0d73a0a2d23e1"
],
[
"Vale.Interop.X64.wrap_aux_weak",
8,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"2e4f57b6d53b37b44d365d652e52c1c6"
],
[
"Vale.Interop.X64.wrap_aux_weak",
9,
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",
"typing_FStar.List.Tot.Base.length"
],
0,
"17246e3d5d1e7b3d8db7d9e0a787098c"
],
[
"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,
"7da431de4d20b2e0709beade365f37ec"
],
[
"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,
"a78f0fd6f81d14bb590a7fcb54459004"
],
[
"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,
"3fbcc23a64e838d1fc012c5df83ceb05"
],
[
"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,
"a8d8eff11442aa3c895ab83d30eadef6"
],
[
"Vale.Interop.X64.as_lowstar_sig_t_weak",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_d1d8f590ca65fc47bf004e71761d3452"
],
0,
"a2bb972a7487b6b4e936cc95e20db4c5"
],
[
"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,
"67f6e0d3d154aa737f93af6bede72560"
],
[
"Vale.Interop.X64.wrap_weak",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_d1d8f590ca65fc47bf004e71761d3452"
],
0,
"87022ddc77f426d3160746dfbf6e8ed4"
],
[
"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,
"678e92986bd2295adc1cce94d7f1a01d"
],
[
"Vale.Interop.X64.arg_of_register",
1,
1,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0,
"edf1a8953e2c09080c03ee301655e898"
],
[
"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,
"fd61296e8166885ed08c95ef83801edd"
],
[
"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,
"f7481253a4589041401980d525dcca92"
]
]
]
Computing file changes ...
