Revision 059787e63538941130606248805cab290fdbc5d7 authored by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC, committed by Dzomo the everest Yak on 20 April 2020, 08:21:22 UTC
1 parent 03f1e46
X64.Leakage_Ins_Xmm.fst.hints
[
"��\u0004�Nr�锓h����J",
[
[
"X64.Leakage_Ins_Xmm.check_if_pxor_leakage_free",
1,
4,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
"X64.Leakage_Ins_Xmm_interpretation_Tm_arrow_bdda86793821fc687c53232715f5c21f",
"X64.Taint_Semantics_s_pretyping_cc24b69d9ea89f288186d79510eec4aa",
"X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
"bool_inversion", "bool_typing", "constructor_distinct_Prims.Nil",
"constructor_distinct_X64.Machine_s.Ins",
"constructor_distinct_X64.Machine_s.Public",
"constructor_distinct_X64.Machine_s.Secret",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_X64.Bytes_Semantics_s.Mkstate",
"data_elim_X64.Leakage_s.TaintState",
"data_elim_X64.Taint_Semantics_s.MktraceState",
"data_typing_intro_X64.Machine_s.Ins@tok",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_X64.Bytes_Semantics_s.MOVDQU",
"disc_equation_X64.Bytes_Semantics_s.Pxor",
"disc_equation_X64.Machine_s.Public",
"disc_equation_X64.Machine_s.Secret",
"equality_tok_X64.Machine_s.Public@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_FStar.List.Tot.Base.op_At",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Types_s.quad32", "equation_Types_s.quad32_xor",
"equation_X64.Bytes_Semantics_s.eval_ins",
"equation_X64.Bytes_Semantics_s.update_xmm_",
"equation_X64.Bytes_Semantics_s.update_xmm_preserve_flags",
"equation_X64.Bytes_Semantics_s.xmms_t",
"equation_X64.Instruction_s.instr_out",
"equation_X64.Leakage_Helpers.merge_taint",
"equation_X64.Leakage_Ins_Xmm.set_xmm_taint",
"equation_X64.Leakage_Ins_Xmm.xmm_taint",
"equation_X64.Leakage_s.constTimeInvariant",
"equation_X64.Leakage_s.isConstantTime",
"equation_X64.Leakage_s.isConstantTimeGivenStates",
"equation_X64.Leakage_s.isExplicitLeakageFree",
"equation_X64.Leakage_s.isExplicitLeakageFreeGivenStates",
"equation_X64.Leakage_s.isLeakageFree",
"equation_X64.Leakage_s.is_explicit_leakage_free_lhs",
"equation_X64.Leakage_s.is_explicit_leakage_free_rhs",
"equation_X64.Leakage_s.publicCfFlagValuesAreSame",
"equation_X64.Leakage_s.publicFlagValuesAreSame",
"equation_X64.Leakage_s.publicMemValuesAreSame",
"equation_X64.Leakage_s.publicRegisterValuesAreSame",
"equation_X64.Leakage_s.publicValuesAreSame",
"equation_X64.Leakage_s.publicXmmValuesAreSame",
"equation_X64.Machine_s.xmm",
"equation_X64.Taint_Semantics_s.extract_operands",
"equation_X64.Taint_Semantics_s.ins_obs",
"equation_X64.Taint_Semantics_s.taint_eval_ins",
"equation_X64.Taint_Semantics_s.tainted_code",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
"fuel_guarded_inversion_Prims.list",
"fuel_guarded_inversion_X64.Bytes_Semantics_s.state",
"fuel_guarded_inversion_X64.Leakage_s.taintState",
"fuel_guarded_inversion_X64.Machine_s.taint",
"fuel_guarded_inversion_X64.Taint_Semantics_s.tainted_ins",
"fuel_guarded_inversion_X64.Taint_Semantics_s.traceState",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
"function_token_typing_X64.Leakage_s.__proj__TaintState__item__regTaint",
"function_token_typing_X64.Leakage_s.__proj__TaintState__item__xmmTaint",
"interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
"interpretation_Tm_abs_43918b1939ad3e5b5ff1258e63680b46",
"interpretation_Tm_abs_4a1a6682764b8be475443da6650b9908",
"interpretation_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
"interpretation_Tm_abs_728e959e62c634798059835f229c48f4",
"interpretation_Tm_abs_a14e8343067a7b0a5181716bef5e4040",
"interpretation_Tm_abs_fe44d2820bd291cbabc93d338ef2fb23",
"kinding_X64.Machine_s.observation@tok",
"kinding_X64.Taint_Semantics_s.tainted_ins@tok",
"kinding_X64.Taint_Semantics_s.tainted_ocmp@tok",
"kinding_X64.Taint_Semantics_s.traceState@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_FStar.List.Tot.Properties.append_l_nil",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_flags",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_stack",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
"proj_equation_X64.Leakage_s.TaintState_cfFlagsTaint",
"proj_equation_X64.Leakage_s.TaintState_flagsTaint",
"proj_equation_X64.Leakage_s.TaintState_regTaint",
"proj_equation_X64.Leakage_s.TaintState_xmmTaint",
"proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
"proj_equation_X64.Taint_Semantics_s.MktraceState_state",
"proj_equation_X64.Taint_Semantics_s.MktraceState_trace",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
"projection_inverse_BoxBool_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.Nil_a",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_stack",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
"projection_inverse_X64.Bytes_Semantics_s.Pxor_dst",
"projection_inverse_X64.Bytes_Semantics_s.Pxor_src",
"projection_inverse_X64.Leakage_s.TaintState_cfFlagsTaint",
"projection_inverse_X64.Leakage_s.TaintState_flagsTaint",
"projection_inverse_X64.Leakage_s.TaintState_regTaint",
"projection_inverse_X64.Leakage_s.TaintState_xmmTaint",
"projection_inverse_X64.Machine_s.Ins_ins",
"projection_inverse_X64.Machine_s.Ins_t_ins",
"projection_inverse_X64.Machine_s.Ins_t_ocmp",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a",
"refinement_interpretation_Tm_refine_854519393548eef59ce2768ec2f66bb1",
"refinement_interpretation_Tm_refine_b0ec1ad4c766f179179881d04d9cace4",
"token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
"token_correspondence_X64.Bytes_Semantics_s.eval_ins",
"token_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"typing_FStar.Pervasives.Native.__proj__Some__item__v",
"typing_Tm_abs_4a1a6682764b8be475443da6650b9908",
"typing_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
"typing_Tm_abs_728e959e62c634798059835f229c48f4",
"typing_Tm_abs_fe44d2820bd291cbabc93d338ef2fb23",
"typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__ok",
"typing_X64.CPU_Features_s.avx_enabled",
"typing_X64.Leakage_Ins_Xmm.xmm_taint", "typing_X64.Machine_s.xmm",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__memTaint",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__trace",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__i",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__t",
"typing_X64.Taint_Semantics_s.extract_operands",
"typing_X64.Taint_Semantics_s.ins_obs",
"typing_X64.Taint_Semantics_s.operand_obs_list",
"typing_X64.Taint_Semantics_s.taint_eval_code",
"typing_X64.Taint_Semantics_s.taint_eval_ins", "unit_typing"
],
0,
"7a48ca3dec742787f62a2bac2f361327"
],
[
"X64.Leakage_Ins_Xmm.check_if_paddd_leakage_free",
1,
4,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_X64.Instruction_s.instr_args_t.fuel_instrumented",
"@fuel_correspondence_X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@fuel_correspondence_X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
"@fuel_irrelevance_X64.Instruction_s.instr_args_t.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"X64.Bytes_Semantics_s_interpretation_Tm_arrow_17742a16dc7ea8ebf4db7d06d09f33c0",
"X64.Bytes_Semantics_s_interpretation_Tm_arrow_626ff301f063a811cbcf87a3e20980fc",
"X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
"X64.Instruction_s_interpretation_Tm_arrow_94d321b6f8e3baaa56e0d113b67d0389",
"X64.Instruction_s_pretyping_d0ada7b4345467e8cc9363a726e7763c",
"X64.Leakage_Ins_Xmm_interpretation_Tm_arrow_bdda86793821fc687c53232715f5c21f",
"X64.Taint_Semantics_s_pretyping_cc24b69d9ea89f288186d79510eec4aa",
"X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
"bool_inversion", "bool_typing", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil",
"constructor_distinct_X64.Instruction_s.IOpEx",
"constructor_distinct_X64.Instruction_s.IOpXmm",
"constructor_distinct_X64.Instruction_s.InOut",
"constructor_distinct_X64.Machine_s.Ins",
"constructor_distinct_X64.Machine_s.Public",
"constructor_distinct_X64.Machine_s.Secret",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_X64.Bytes_Semantics_s.Mkstate",
"data_elim_X64.Leakage_s.TaintState",
"data_elim_X64.Taint_Semantics_s.MktraceState",
"data_elim_X64.Taint_Semantics_s.TaintedIns",
"data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_X64.Instruction_s.IOpEx@tok",
"data_typing_intro_X64.Instruction_s.Out@tok",
"data_typing_intro_X64.Machine_s.Ins@tok",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_X64.Bytes_Semantics_s.Ins_ioXmm_Xmm",
"disc_equation_X64.Bytes_Semantics_s.MOVDQU",
"disc_equation_X64.Machine_s.Public",
"disc_equation_X64.Machine_s.Secret",
"equality_tok_X64.Instruction_s.IOpXmm@tok",
"equality_tok_X64.Instruction_s.InOut@tok",
"equality_tok_X64.Instruction_s.PreserveFlags@tok",
"equality_tok_X64.Machine_s.Public@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_FStar.List.Tot.Base.op_At",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Types_s.quad32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.Bytes_Semantics_s.eval_ins",
"equation_X64.Bytes_Semantics_s.st",
"equation_X64.Bytes_Semantics_s.update_xmm_",
"equation_X64.Bytes_Semantics_s.update_xmm_preserve_flags",
"equation_X64.Bytes_Semantics_s.xmms_t",
"equation_X64.Instruction_s.arrow",
"equation_X64.Instruction_s.instr_out",
"equation_X64.Instruction_s.instr_val_t",
"equation_X64.Leakage_Helpers.merge_taint",
"equation_X64.Leakage_Ins_Xmm.set_xmm_taint",
"equation_X64.Leakage_Ins_Xmm.xmm_taint",
"equation_X64.Leakage_s.constTimeInvariant",
"equation_X64.Leakage_s.isConstantTime",
"equation_X64.Leakage_s.isConstantTimeGivenStates",
"equation_X64.Leakage_s.isExplicitLeakageFree",
"equation_X64.Leakage_s.isExplicitLeakageFreeGivenStates",
"equation_X64.Leakage_s.isLeakageFree",
"equation_X64.Leakage_s.is_explicit_leakage_free_lhs",
"equation_X64.Leakage_s.is_explicit_leakage_free_rhs",
"equation_X64.Leakage_s.publicCfFlagValuesAreSame",
"equation_X64.Leakage_s.publicFlagValuesAreSame",
"equation_X64.Leakage_s.publicMemValuesAreSame",
"equation_X64.Leakage_s.publicRegisterValuesAreSame",
"equation_X64.Leakage_s.publicValuesAreSame",
"equation_X64.Leakage_s.publicXmmValuesAreSame",
"equation_X64.Machine_s.xmm",
"equation_X64.Taint_Semantics_s.extract_operands",
"equation_X64.Taint_Semantics_s.ins_obs",
"equation_X64.Taint_Semantics_s.taint_eval_ins",
"equation_X64.Taint_Semantics_s.tainted_code",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_X64.Instruction_s.instr_args_t.fuel_instrumented",
"equation_with_fuel_X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"equation_with_fuel_X64.Instruction_s.instr_ret_t.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_X64.Bytes_Semantics_s.state",
"fuel_guarded_inversion_X64.Leakage_s.taintState",
"fuel_guarded_inversion_X64.Machine_s.taint",
"fuel_guarded_inversion_X64.Taint_Semantics_s.tainted_ins",
"fuel_guarded_inversion_X64.Taint_Semantics_s.traceState",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
"function_token_typing_X64.Bytes_Semantics_s.eval_ins",
"function_token_typing_X64.Instruction_s.instr_eval",
"function_token_typing_X64.Instruction_s.instr_out",
"function_token_typing_X64.Leakage_s.__proj__TaintState__item__regTaint",
"function_token_typing_X64.Leakage_s.__proj__TaintState__item__xmmTaint",
"int_inversion",
"interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
"interpretation_Tm_abs_43918b1939ad3e5b5ff1258e63680b46",
"interpretation_Tm_abs_4a1a6682764b8be475443da6650b9908",
"interpretation_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
"interpretation_Tm_abs_728e959e62c634798059835f229c48f4",
"interpretation_Tm_abs_74722fb662ef15cb6b81bf92b6bcee49",
"interpretation_Tm_abs_a14e8343067a7b0a5181716bef5e4040",
"interpretation_Tm_abs_fe44d2820bd291cbabc93d338ef2fb23",
"kinding_X64.Instruction_s.instr_operand@tok",
"kinding_X64.Instruction_s.instr_operand_inout@tok",
"kinding_X64.Machine_s.observation@tok",
"kinding_X64.Taint_Semantics_s.tainted_ins@tok",
"kinding_X64.Taint_Semantics_s.tainted_ocmp@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_FStar.List.Tot.Properties.append_l_nil",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_flags",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_stack",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
"proj_equation_X64.Leakage_s.TaintState_cfFlagsTaint",
"proj_equation_X64.Leakage_s.TaintState_flagsTaint",
"proj_equation_X64.Leakage_s.TaintState_regTaint",
"proj_equation_X64.Leakage_s.TaintState_xmmTaint",
"proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
"proj_equation_X64.Taint_Semantics_s.MktraceState_state",
"proj_equation_X64.Taint_Semantics_s.MktraceState_trace",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
"projection_inverse_BoxBool_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_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_X64.Bytes_Semantics_s.Ins_ioXmm_Xmm_dst",
"projection_inverse_X64.Bytes_Semantics_s.Ins_ioXmm_Xmm_i",
"projection_inverse_X64.Bytes_Semantics_s.Ins_ioXmm_Xmm_src",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_stack",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
"projection_inverse_X64.Instruction_s.IOpEx__0",
"projection_inverse_X64.Leakage_s.TaintState_cfFlagsTaint",
"projection_inverse_X64.Leakage_s.TaintState_flagsTaint",
"projection_inverse_X64.Leakage_s.TaintState_regTaint",
"projection_inverse_X64.Leakage_s.TaintState_xmmTaint",
"projection_inverse_X64.Machine_s.Ins_ins",
"projection_inverse_X64.Machine_s.Ins_t_ins",
"projection_inverse_X64.Machine_s.Ins_t_ocmp",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
"refinement_interpretation_Tm_refine_0aee0ed1490a04484e9a5dc777a73107",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_b0ec1ad4c766f179179881d04d9cace4",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
"token_correspondence_X64.Bytes_Semantics_s.eval_ins",
"token_correspondence_X64.Instruction_s.instr_eval",
"token_correspondence_X64.Leakage_s.__proj__TaintState__item__regTaint",
"token_correspondence_X64.Leakage_s.__proj__TaintState__item__xmmTaint",
"typing_Tm_abs_4a1a6682764b8be475443da6650b9908",
"typing_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
"typing_Tm_abs_728e959e62c634798059835f229c48f4",
"typing_Tm_abs_fe44d2820bd291cbabc93d338ef2fb23",
"typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__ok",
"typing_X64.Leakage_Ins_Xmm.xmm_taint",
"typing_X64.Leakage_s.__proj__TaintState__item__cfFlagsTaint",
"typing_X64.Machine_s.uu___is_Secret", "typing_X64.Machine_s.xmm",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__memTaint",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__trace",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__i",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__t",
"typing_X64.Taint_Semantics_s.extract_operands",
"typing_X64.Taint_Semantics_s.ins_obs",
"typing_X64.Taint_Semantics_s.operand_obs_list",
"typing_X64.Taint_Semantics_s.taint_eval_code",
"typing_X64.Taint_Semantics_s.taint_eval_ins",
"typing_tok_X64.Instruction_s.IOpXmm@tok",
"typing_tok_X64.Instruction_s.InOut@tok",
"typing_tok_X64.Instruction_s.PreserveFlags@tok", "unit_inversion",
"unit_typing"
],
0,
"73bcd4e87fb6f3dbf305034d12016b51"
],
[
"X64.Leakage_Ins_Xmm.check_if_pslld_leakage_free",
1,
4,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_X64.Instruction_s.instr_args_t.fuel_instrumented",
"@fuel_correspondence_X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@fuel_correspondence_X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"X64.Bytes_Semantics_s_interpretation_Tm_arrow_17742a16dc7ea8ebf4db7d06d09f33c0",
"X64.Bytes_Semantics_s_interpretation_Tm_arrow_626ff301f063a811cbcf87a3e20980fc",
"X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
"X64.Instruction_s_interpretation_Tm_arrow_94d321b6f8e3baaa56e0d113b67d0389",
"X64.Instruction_s_pretyping_d0ada7b4345467e8cc9363a726e7763c",
"X64.Leakage_Ins_Xmm_interpretation_Tm_arrow_bdda86793821fc687c53232715f5c21f",
"X64.Taint_Semantics_s_pretyping_cc24b69d9ea89f288186d79510eec4aa",
"X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
"bool_inversion", "bool_typing", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil",
"constructor_distinct_X64.Instruction_s.IOpEx",
"constructor_distinct_X64.Instruction_s.IOpXmm",
"constructor_distinct_X64.Instruction_s.InOut",
"constructor_distinct_X64.Machine_s.Ins",
"constructor_distinct_X64.Machine_s.Public",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_X64.Bytes_Semantics_s.Mkstate",
"data_elim_X64.Leakage_s.TaintState",
"data_elim_X64.Taint_Semantics_s.MktraceState",
"data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_X64.Instruction_s.IOpEx@tok",
"data_typing_intro_X64.Instruction_s.Out@tok",
"data_typing_intro_X64.Machine_s.Ins@tok",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_X64.Bytes_Semantics_s.Ins_ioXmm",
"disc_equation_X64.Bytes_Semantics_s.MOVDQU",
"disc_equation_X64.Machine_s.Public",
"equality_tok_X64.Instruction_s.IOpXmm@tok",
"equality_tok_X64.Instruction_s.InOut@tok",
"equality_tok_X64.Instruction_s.PreserveFlags@tok",
"equality_tok_X64.Machine_s.Public@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_FStar.List.Tot.Base.op_At",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Types_s.quad32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.Bytes_Semantics_s.eval_ins",
"equation_X64.Bytes_Semantics_s.st",
"equation_X64.Bytes_Semantics_s.update_xmm_",
"equation_X64.Bytes_Semantics_s.update_xmm_preserve_flags",
"equation_X64.Bytes_Semantics_s.xmms_t",
"equation_X64.Instruction_s.arrow",
"equation_X64.Instruction_s.instr_out",
"equation_X64.Instruction_s.instr_val_t",
"equation_X64.Leakage_Ins_Xmm.set_xmm_taint",
"equation_X64.Leakage_Ins_Xmm.xmm_taint",
"equation_X64.Leakage_s.constTimeInvariant",
"equation_X64.Leakage_s.isConstantTime",
"equation_X64.Leakage_s.isConstantTimeGivenStates",
"equation_X64.Leakage_s.isExplicitLeakageFree",
"equation_X64.Leakage_s.isExplicitLeakageFreeGivenStates",
"equation_X64.Leakage_s.isLeakageFree",
"equation_X64.Leakage_s.is_explicit_leakage_free_lhs",
"equation_X64.Leakage_s.is_explicit_leakage_free_rhs",
"equation_X64.Leakage_s.publicCfFlagValuesAreSame",
"equation_X64.Leakage_s.publicFlagValuesAreSame",
"equation_X64.Leakage_s.publicMemValuesAreSame",
"equation_X64.Leakage_s.publicRegisterValuesAreSame",
"equation_X64.Leakage_s.publicValuesAreSame",
"equation_X64.Leakage_s.publicXmmValuesAreSame",
"equation_X64.Machine_s.xmm",
"equation_X64.Taint_Semantics_s.extract_operands",
"equation_X64.Taint_Semantics_s.ins_obs",
"equation_X64.Taint_Semantics_s.taint_eval_ins",
"equation_X64.Taint_Semantics_s.tainted_code",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_X64.Instruction_s.instr_args_t.fuel_instrumented",
"equation_with_fuel_X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"equation_with_fuel_X64.Instruction_s.instr_ret_t.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_X64.Bytes_Semantics_s.state",
"fuel_guarded_inversion_X64.Leakage_s.taintState",
"fuel_guarded_inversion_X64.Machine_s.reg",
"fuel_guarded_inversion_X64.Machine_s.taint",
"fuel_guarded_inversion_X64.Taint_Semantics_s.tainted_ins",
"fuel_guarded_inversion_X64.Taint_Semantics_s.traceState",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
"function_token_typing_X64.Bytes_Semantics_s.eval_ins",
"function_token_typing_X64.Instruction_s.instr_eval",
"function_token_typing_X64.Instruction_s.instr_out",
"function_token_typing_X64.Leakage_s.__proj__TaintState__item__regTaint",
"function_token_typing_X64.Leakage_s.__proj__TaintState__item__xmmTaint",
"int_inversion",
"interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
"interpretation_Tm_abs_43918b1939ad3e5b5ff1258e63680b46",
"interpretation_Tm_abs_4a1a6682764b8be475443da6650b9908",
"interpretation_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
"interpretation_Tm_abs_728e959e62c634798059835f229c48f4",
"interpretation_Tm_abs_74722fb662ef15cb6b81bf92b6bcee49",
"interpretation_Tm_abs_a14e8343067a7b0a5181716bef5e4040",
"interpretation_Tm_abs_fe44d2820bd291cbabc93d338ef2fb23",
"kinding_X64.Instruction_s.instr_operand@tok",
"kinding_X64.Instruction_s.instr_operand_inout@tok",
"kinding_X64.Machine_s.observation@tok",
"kinding_X64.Taint_Semantics_s.tainted_ins@tok",
"kinding_X64.Taint_Semantics_s.tainted_ocmp@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_FStar.List.Tot.Properties.append_l_nil",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_flags",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_stack",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
"proj_equation_X64.Leakage_s.TaintState_cfFlagsTaint",
"proj_equation_X64.Leakage_s.TaintState_flagsTaint",
"proj_equation_X64.Leakage_s.TaintState_regTaint",
"proj_equation_X64.Leakage_s.TaintState_xmmTaint",
"proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
"proj_equation_X64.Taint_Semantics_s.MktraceState_state",
"proj_equation_X64.Taint_Semantics_s.MktraceState_trace",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
"projection_inverse_BoxBool_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_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_X64.Bytes_Semantics_s.Ins_ioXmm_dst",
"projection_inverse_X64.Bytes_Semantics_s.Ins_ioXmm_i",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_stack",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
"projection_inverse_X64.Instruction_s.IOpEx__0",
"projection_inverse_X64.Leakage_s.TaintState_cfFlagsTaint",
"projection_inverse_X64.Leakage_s.TaintState_flagsTaint",
"projection_inverse_X64.Leakage_s.TaintState_regTaint",
"projection_inverse_X64.Leakage_s.TaintState_xmmTaint",
"projection_inverse_X64.Machine_s.Ins_ins",
"projection_inverse_X64.Machine_s.Ins_t_ins",
"projection_inverse_X64.Machine_s.Ins_t_ocmp",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_5e18095c08e7538e57b0bceb2412c75e",
"refinement_interpretation_Tm_refine_b0ec1ad4c766f179179881d04d9cace4",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"token_correspondence_X64.Bytes_Semantics_s.eval_ins",
"token_correspondence_X64.Instruction_s.instr_eval",
"typing_Tm_abs_4a1a6682764b8be475443da6650b9908",
"typing_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
"typing_Tm_abs_728e959e62c634798059835f229c48f4",
"typing_Tm_abs_fe44d2820bd291cbabc93d338ef2fb23",
"typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__ok",
"typing_X64.Leakage_Ins_Xmm.xmm_taint", "typing_X64.Machine_s.xmm",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__memTaint",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__trace",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__i",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__t",
"typing_X64.Taint_Semantics_s.extract_operands",
"typing_X64.Taint_Semantics_s.ins_obs",
"typing_X64.Taint_Semantics_s.operand_obs_list",
"typing_X64.Taint_Semantics_s.taint_eval_code",
"typing_X64.Taint_Semantics_s.taint_eval_ins",
"typing_tok_X64.Instruction_s.IOpXmm@tok",
"typing_tok_X64.Instruction_s.InOut@tok",
"typing_tok_X64.Instruction_s.PreserveFlags@tok", "unit_inversion",
"unit_typing"
],
0,
"c36b81350a48b424ea84b71204678e33"
],
[
"X64.Leakage_Ins_Xmm.check_if_pshufd_leakage_free",
1,
4,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_X64.Instruction_s.instr_args_t.fuel_instrumented",
"@fuel_correspondence_X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"@fuel_correspondence_X64.Instruction_s.instr_ret_t.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
"@fuel_irrelevance_X64.Instruction_s.instr_args_t.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
"X64.Instruction_s_interpretation_Tm_arrow_94d321b6f8e3baaa56e0d113b67d0389",
"X64.Instruction_s_pretyping_d0ada7b4345467e8cc9363a726e7763c",
"X64.Leakage_Ins_Xmm_interpretation_Tm_arrow_bdda86793821fc687c53232715f5c21f",
"X64.Taint_Semantics_s_pretyping_cc24b69d9ea89f288186d79510eec4aa",
"X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
"bool_inversion", "bool_typing", "constructor_distinct_Prims.Cons",
"constructor_distinct_Prims.Nil",
"constructor_distinct_X64.Instruction_s.IOpEx",
"constructor_distinct_X64.Instruction_s.IOpXmm",
"constructor_distinct_X64.Instruction_s.Out",
"constructor_distinct_X64.Machine_s.Ins",
"constructor_distinct_X64.Machine_s.Public",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_elim_FStar.Pervasives.Native.Some",
"data_elim_X64.Bytes_Semantics_s.Mkstate",
"data_elim_X64.Leakage_s.TaintState",
"data_elim_X64.Taint_Semantics_s.MktraceState",
"data_typing_intro_FStar.Pervasives.Native.Mktuple2@tok",
"data_typing_intro_Prims.Cons@tok",
"data_typing_intro_Prims.Nil@tok",
"data_typing_intro_X64.Instruction_s.IOpEx@tok",
"data_typing_intro_X64.Instruction_s.Out@tok",
"data_typing_intro_X64.Machine_s.Ins@tok",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_X64.Bytes_Semantics_s.Ins_Xmm_Xmm",
"disc_equation_X64.Bytes_Semantics_s.MOVDQU",
"disc_equation_X64.Machine_s.Public",
"equality_tok_X64.Instruction_s.IOpXmm@tok",
"equality_tok_X64.Instruction_s.Out@tok",
"equality_tok_X64.Instruction_s.PreserveFlags@tok",
"equality_tok_X64.Machine_s.Public@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.FunctionalExtensionality.restricted_t",
"equation_FStar.List.Tot.Base.op_At",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Types_s.quad32",
"equation_Words_s.nat64", "equation_Words_s.natN",
"equation_X64.Bytes_Semantics_s.eval_ins",
"equation_X64.Bytes_Semantics_s.update_xmm_",
"equation_X64.Bytes_Semantics_s.update_xmm_preserve_flags",
"equation_X64.Bytes_Semantics_s.xmms_t",
"equation_X64.Instruction_s.arrow",
"equation_X64.Instruction_s.instr_out",
"equation_X64.Instruction_s.instr_val_t",
"equation_X64.Leakage_Ins_Xmm.set_xmm_taint",
"equation_X64.Leakage_Ins_Xmm.xmm_taint",
"equation_X64.Leakage_s.constTimeInvariant",
"equation_X64.Leakage_s.isConstantTime",
"equation_X64.Leakage_s.isConstantTimeGivenStates",
"equation_X64.Leakage_s.isExplicitLeakageFree",
"equation_X64.Leakage_s.isExplicitLeakageFreeGivenStates",
"equation_X64.Leakage_s.isLeakageFree",
"equation_X64.Leakage_s.is_explicit_leakage_free_lhs",
"equation_X64.Leakage_s.is_explicit_leakage_free_rhs",
"equation_X64.Leakage_s.publicCfFlagValuesAreSame",
"equation_X64.Leakage_s.publicFlagValuesAreSame",
"equation_X64.Leakage_s.publicMemValuesAreSame",
"equation_X64.Leakage_s.publicRegisterValuesAreSame",
"equation_X64.Leakage_s.publicValuesAreSame",
"equation_X64.Leakage_s.publicXmmValuesAreSame",
"equation_X64.Machine_s.xmm",
"equation_X64.Taint_Semantics_s.extract_operands",
"equation_X64.Taint_Semantics_s.ins_obs",
"equation_X64.Taint_Semantics_s.taint_eval_ins",
"equation_X64.Taint_Semantics_s.tainted_code",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_X64.Instruction_s.instr_args_t.fuel_instrumented",
"equation_with_fuel_X64.Instruction_s.instr_inouts_t.fuel_instrumented",
"equation_with_fuel_X64.Instruction_s.instr_ret_t.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_match_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.update_taint_list.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"fuel_guarded_inversion_X64.Bytes_Semantics_s.state",
"fuel_guarded_inversion_X64.Leakage_s.taintState",
"fuel_guarded_inversion_X64.Machine_s.reg",
"fuel_guarded_inversion_X64.Machine_s.taint",
"fuel_guarded_inversion_X64.Taint_Semantics_s.tainted_ins",
"fuel_guarded_inversion_X64.Taint_Semantics_s.traceState",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
"function_token_typing_X64.Instruction_s.instr_eval",
"function_token_typing_X64.Instruction_s.instr_out",
"function_token_typing_X64.Leakage_s.__proj__TaintState__item__regTaint",
"function_token_typing_X64.Leakage_s.__proj__TaintState__item__xmmTaint",
"int_inversion",
"interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
"interpretation_Tm_abs_43918b1939ad3e5b5ff1258e63680b46",
"interpretation_Tm_abs_4a1a6682764b8be475443da6650b9908",
"interpretation_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
"interpretation_Tm_abs_728e959e62c634798059835f229c48f4",
"interpretation_Tm_abs_74722fb662ef15cb6b81bf92b6bcee49",
"interpretation_Tm_abs_a14e8343067a7b0a5181716bef5e4040",
"interpretation_Tm_abs_fe44d2820bd291cbabc93d338ef2fb23",
"kinding_X64.Instruction_s.instr_operand@tok",
"kinding_X64.Instruction_s.instr_operand_inout@tok",
"kinding_X64.Machine_s.observation@tok",
"kinding_X64.Taint_Semantics_s.tainted_ins@tok",
"kinding_X64.Taint_Semantics_s.tainted_ocmp@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_FStar.List.Tot.Properties.append_l_nil",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_AmpAmp",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_flags",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_stack",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
"proj_equation_X64.Leakage_s.TaintState_cfFlagsTaint",
"proj_equation_X64.Leakage_s.TaintState_flagsTaint",
"proj_equation_X64.Leakage_s.TaintState_regTaint",
"proj_equation_X64.Leakage_s.TaintState_xmmTaint",
"proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
"proj_equation_X64.Taint_Semantics_s.MktraceState_state",
"proj_equation_X64.Taint_Semantics_s.MktraceState_trace",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
"projection_inverse_BoxBool_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_a",
"projection_inverse_Prims.Cons_hd",
"projection_inverse_Prims.Cons_tl", "projection_inverse_Prims.Nil_a",
"projection_inverse_X64.Bytes_Semantics_s.Ins_Xmm_Xmm_dst",
"projection_inverse_X64.Bytes_Semantics_s.Ins_Xmm_Xmm_i",
"projection_inverse_X64.Bytes_Semantics_s.Ins_Xmm_Xmm_src",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_stack",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
"projection_inverse_X64.Instruction_s.IOpEx__0",
"projection_inverse_X64.Leakage_s.TaintState_cfFlagsTaint",
"projection_inverse_X64.Leakage_s.TaintState_flagsTaint",
"projection_inverse_X64.Leakage_s.TaintState_regTaint",
"projection_inverse_X64.Leakage_s.TaintState_xmmTaint",
"projection_inverse_X64.Machine_s.Ins_ins",
"projection_inverse_X64.Machine_s.Ins_t_ins",
"projection_inverse_X64.Machine_s.Ins_t_ocmp",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
"refinement_interpretation_Tm_refine_2f3cdc35e0030203ad7d8f3b5f95f8df",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_b0ec1ad4c766f179179881d04d9cace4",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f0a4eeefab9c63f31c350a802a4d45dd",
"token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"token_correspondence_X64.Bytes_Semantics_s.eval_ins",
"token_correspondence_X64.Instruction_s.instr_eval",
"typing_Tm_abs_4a1a6682764b8be475443da6650b9908",
"typing_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
"typing_Tm_abs_728e959e62c634798059835f229c48f4",
"typing_Tm_abs_fe44d2820bd291cbabc93d338ef2fb23",
"typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__ok",
"typing_X64.Instruction_s.instr_ret_t",
"typing_X64.Leakage_Ins_Xmm.xmm_taint", "typing_X64.Machine_s.xmm",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__memTaint",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__trace",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__i",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__t",
"typing_X64.Taint_Semantics_s.extract_operands",
"typing_X64.Taint_Semantics_s.ins_obs",
"typing_X64.Taint_Semantics_s.operand_obs_list",
"typing_X64.Taint_Semantics_s.taint_eval_code",
"typing_X64.Taint_Semantics_s.taint_eval_ins",
"typing_tok_X64.Instruction_s.IOpXmm@tok",
"typing_tok_X64.Instruction_s.Out@tok",
"typing_tok_X64.Instruction_s.PreserveFlags@tok", "unit_typing"
],
0,
"d40d67de2e58fb834e68be3e76d11d2d"
],
[
"X64.Leakage_Ins_Xmm.mov128_does_not_use_secret",
1,
4,
2,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_X64.Machine_s.Mov128Mem",
"disc_equation_X64.Machine_s.Mov128Stack",
"disc_equation_X64.Machine_s.Mov128Xmm",
"fuel_guarded_inversion_X64.Machine_s.mov128_op"
],
0,
"60032032f9c7d8052b00670de372f722"
],
[
"X64.Leakage_Ins_Xmm.check_if_movdqu_leakage_free_aux",
1,
4,
2,
[
"@MaxIFuel_assumption", "@query",
"data_elim_X64.Bytes_Semantics_s.MOVDQU",
"disc_equation_X64.Bytes_Semantics_s.MOVDQU",
"disc_equation_X64.Machine_s.Mov128Mem",
"disc_equation_X64.Machine_s.Mov128Stack",
"disc_equation_X64.Machine_s.Mov128Xmm",
"equality_tok_X64.Machine_s.Secret@tok",
"fuel_guarded_inversion_X64.Machine_s.mov128_op",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_X64.Bytes_Semantics_s.MOVDQU_dst",
"projection_inverse_X64.Bytes_Semantics_s.MOVDQU_src",
"refinement_interpretation_Tm_refine_69a34f712728736367447fdb81c0edd0",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__i"
],
0,
"dea1d5c3e60a1e2685f4157f1ee90d9a"
],
[
"X64.Leakage_Ins_Xmm.frame_update_heap128_x",
1,
4,
2,
[ "@query" ],
0,
"10f0f656718ace7612341c258e174cef"
],
[
"X64.Leakage_Ins_Xmm.lemma_movdqu_same_public_aux",
1,
4,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.List.Tot.Base.append.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"@query",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_interpretation_Tm_arrow_a26b6f0ab7c6505137c6de4ce0011041",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"X64.Bytes_Semantics_s_interpretation_Tm_arrow_71ff103e225169c475064edd2fb305a3",
"X64.Bytes_Semantics_s_pretyping_60dbe79bd701f5199da59ca07a16456f",
"X64.Bytes_Semantics_s_pretyping_e5ba130f8e8efa54c3d7f65c0f7d5207",
"X64.Leakage_Ins_Xmm_interpretation_Tm_arrow_bdda86793821fc687c53232715f5c21f",
"X64.Machine_s_pretyping_b7c45855ed90996ceceb34aa61de24e7",
"X64.Machine_s_pretyping_e51d9612683cb053e6b8236fad2673ca",
"X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
"bool_inversion", "bool_typing", "constructor_distinct_Prims.Nil",
"constructor_distinct_X64.Machine_s.Ins",
"constructor_distinct_X64.Machine_s.Mov128Mem",
"constructor_distinct_X64.Machine_s.Mov128Stack",
"constructor_distinct_X64.Machine_s.Mov128Xmm",
"constructor_distinct_X64.Machine_s.OReg",
"constructor_distinct_X64.Machine_s.Public",
"constructor_distinct_X64.Machine_s.Secret",
"data_elim_Words_s.Mkfour", "data_elim_X64.Bytes_Semantics_s.MOVDQU",
"data_elim_X64.Bytes_Semantics_s.Mkstate",
"data_elim_X64.Leakage_s.TaintState",
"data_elim_X64.Machine_s.MIndex", "data_elim_X64.Machine_s.MReg",
"data_elim_X64.Machine_s.Mov128Mem",
"data_elim_X64.Taint_Semantics_s.MktraceState",
"data_elim_X64.Taint_Semantics_s.TaintedIns",
"data_typing_intro_X64.Machine_s.Ins@tok",
"data_typing_intro_X64.Machine_s.Rbx@tok",
"data_typing_intro_X64.Machine_s.Secret@tok",
"disc_equation_FStar.Pervasives.Native.Some",
"disc_equation_X64.Bytes_Semantics_s.MOVDQU",
"disc_equation_X64.Machine_s.Mov128Mem",
"disc_equation_X64.Machine_s.Mov128Stack",
"disc_equation_X64.Machine_s.Mov128Xmm",
"disc_equation_X64.Machine_s.Public",
"disc_equation_X64.Machine_s.Secret",
"equality_tok_X64.Machine_s.Public@tok",
"equality_tok_X64.Machine_s.Rsp@tok",
"equality_tok_X64.Machine_s.Secret@tok",
"equation_FStar.FunctionalExtensionality.feq",
"equation_FStar.List.Tot.Base.op_At",
"equation_FStar.Pervasives.Native.snd", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Types_s.quad32",
"equation_Words_s.nat32", "equation_Words_s.nat64",
"equation_Words_s.nat8", "equation_Words_s.natN",
"equation_X64.Bytes_Semantics_s.eval_ins",
"equation_X64.Bytes_Semantics_s.eval_maddr",
"equation_X64.Bytes_Semantics_s.eval_mov128_op",
"equation_X64.Bytes_Semantics_s.get_heap_val128",
"equation_X64.Bytes_Semantics_s.get_heap_val128_def",
"equation_X64.Bytes_Semantics_s.get_heap_val32",
"equation_X64.Bytes_Semantics_s.get_heap_val32_def",
"equation_X64.Bytes_Semantics_s.op_String_Access",
"equation_X64.Bytes_Semantics_s.update_mem128",
"equation_X64.Bytes_Semantics_s.update_mov128_op_preserve_flags_",
"equation_X64.Bytes_Semantics_s.update_mov128_op_preserve_flags__",
"equation_X64.Bytes_Semantics_s.update_stack128",
"equation_X64.Bytes_Semantics_s.update_xmm_",
"equation_X64.Bytes_Semantics_s.valid_dst_mov128_op",
"equation_X64.Bytes_Semantics_s.valid_src_mov128_op",
"equation_X64.Instruction_s.instr_out",
"equation_X64.Leakage_Helpers.maddr_does_not_use_secrets",
"equation_X64.Leakage_Helpers.operand_taint",
"equation_X64.Leakage_Ins_Xmm.check_if_movdqu_leakage_free_aux",
"equation_X64.Leakage_Ins_Xmm.mov128_does_not_use_secret",
"equation_X64.Leakage_Ins_Xmm.set_xmm_taint",
"equation_X64.Leakage_Ins_Xmm.xmm_taint",
"equation_X64.Leakage_s.constTimeInvariant",
"equation_X64.Leakage_s.is_explicit_leakage_free_lhs",
"equation_X64.Leakage_s.is_explicit_leakage_free_rhs",
"equation_X64.Leakage_s.publicCfFlagValuesAreSame",
"equation_X64.Leakage_s.publicFlagValuesAreSame",
"equation_X64.Leakage_s.publicMemValuesAreSame",
"equation_X64.Leakage_s.publicRegisterValuesAreSame",
"equation_X64.Leakage_s.publicValuesAreSame",
"equation_X64.Leakage_s.publicXmmValuesAreSame",
"equation_X64.Machine_s.memTaint_t", "equation_X64.Machine_s.xmm",
"equation_X64.Taint_Semantics_s.extract_operands",
"equation_X64.Taint_Semantics_s.ins_obs",
"equation_X64.Taint_Semantics_s.taint_eval_ins",
"equation_X64.Taint_Semantics_s.taint_eval_movdqu",
"equation_X64.Taint_Semantics_s.taint_match128",
"equation_X64.Taint_Semantics_s.tainted_code",
"equation_X64.Taint_Semantics_s.update_taint128",
"equation_with_fuel_FStar.List.Tot.Base.append.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"fuel_guarded_inversion_Words_s.four",
"fuel_guarded_inversion_X64.Bytes_Semantics_s.state",
"fuel_guarded_inversion_X64.Leakage_s.taintState",
"fuel_guarded_inversion_X64.Machine_s.maddr",
"fuel_guarded_inversion_X64.Machine_s.mov128_op",
"fuel_guarded_inversion_X64.Machine_s.taint",
"fuel_guarded_inversion_X64.Taint_Semantics_s.tainted_ins",
"fuel_guarded_inversion_X64.Taint_Semantics_s.traceState",
"function_token_typing_FStar.Map.sel",
"function_token_typing_Opaque_s.make_opaque",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__regs",
"function_token_typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
"function_token_typing_X64.Bytes_Semantics_s.get_heap_val128_def",
"function_token_typing_X64.Bytes_Semantics_s.op_String_Access",
"function_token_typing_X64.Leakage_s.__proj__TaintState__item__regTaint",
"function_token_typing_X64.Leakage_s.__proj__TaintState__item__xmmTaint",
"int_inversion", "int_typing",
"interpretation_Tm_abs_1aa87ea4de26c5f807351c79780462e0",
"interpretation_Tm_abs_4371d80c10148151a6be8a394bec7d26",
"interpretation_Tm_abs_43918b1939ad3e5b5ff1258e63680b46",
"interpretation_Tm_abs_4a1a6682764b8be475443da6650b9908",
"interpretation_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
"interpretation_Tm_abs_728e959e62c634798059835f229c48f4",
"interpretation_Tm_abs_74722fb662ef15cb6b81bf92b6bcee49",
"interpretation_Tm_abs_fe44d2820bd291cbabc93d338ef2fb23",
"kinding_X64.Machine_s.observation@tok",
"kinding_X64.Machine_s.taint@tok",
"kinding_X64.Taint_Semantics_s.tainted_ins@tok",
"kinding_X64.Taint_Semantics_s.tainted_ocmp@tok",
"lemma_FStar.FunctionalExtensionality.feq_on_domain",
"lemma_FStar.List.Tot.Properties.append_l_nil",
"lemma_X64.Bytes_Semantics.correct_update_get128",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_disEquality",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_flags",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_mem",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_ok",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_regs",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_stack",
"proj_equation_X64.Bytes_Semantics_s.Mkstate_xmms",
"proj_equation_X64.Leakage_s.TaintState_cfFlagsTaint",
"proj_equation_X64.Leakage_s.TaintState_flagsTaint",
"proj_equation_X64.Leakage_s.TaintState_regTaint",
"proj_equation_X64.Leakage_s.TaintState_xmmTaint",
"proj_equation_X64.Taint_Semantics_s.MktraceState_memTaint",
"proj_equation_X64.Taint_Semantics_s.MktraceState_state",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_t",
"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.Nil_a",
"projection_inverse_Words_s.Mkfour_hi2",
"projection_inverse_Words_s.Mkfour_hi3",
"projection_inverse_Words_s.Mkfour_lo0",
"projection_inverse_Words_s.Mkfour_lo1",
"projection_inverse_X64.Bytes_Semantics_s.MOVDQU_dst",
"projection_inverse_X64.Bytes_Semantics_s.MOVDQU_src",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_flags",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_mem",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_ok",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_regs",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_stack",
"projection_inverse_X64.Bytes_Semantics_s.Mkstate_xmms",
"projection_inverse_X64.Leakage_s.TaintState_cfFlagsTaint",
"projection_inverse_X64.Leakage_s.TaintState_flagsTaint",
"projection_inverse_X64.Leakage_s.TaintState_regTaint",
"projection_inverse_X64.Leakage_s.TaintState_xmmTaint",
"projection_inverse_X64.Machine_s.Ins_ins",
"projection_inverse_X64.Machine_s.Ins_t_ins",
"projection_inverse_X64.Machine_s.Ins_t_ocmp",
"projection_inverse_X64.Machine_s.Mov128Mem_m",
"projection_inverse_X64.Machine_s.Mov128Xmm_x",
"projection_inverse_X64.Machine_s.OReg_r",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_memTaint",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_state",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_55c0b335f5121f8337daf6aff9df4280",
"refinement_interpretation_Tm_refine_69a34f712728736367447fdb81c0edd0",
"refinement_interpretation_Tm_refine_8460739bc2f4e9c8586fe62449789aa0",
"refinement_interpretation_Tm_refine_8e3aff34e2b01c410f661e3b9d75037a",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"token_correspondence_FStar.Map.sel",
"token_correspondence_Opaque_s.make_opaque",
"token_correspondence_X64.Bytes_Semantics_s.__proj__Mkstate__item__xmms",
"token_correspondence_X64.Bytes_Semantics_s.eval_ins",
"token_correspondence_X64.Bytes_Semantics_s.get_heap_val128_def",
"token_correspondence_X64.Bytes_Semantics_s.get_heap_val32_def",
"token_correspondence_X64.Bytes_Semantics_s.op_String_Access",
"token_correspondence_X64.Leakage_s.__proj__TaintState__item__regTaint",
"token_correspondence_X64.Leakage_s.__proj__TaintState__item__xmmTaint",
"typing_Tm_abs_4a1a6682764b8be475443da6650b9908",
"typing_Tm_abs_66926e89e50e2ac69caf858cc1113f07",
"typing_Tm_abs_728e959e62c634798059835f229c48f4",
"typing_Tm_abs_fe44d2820bd291cbabc93d338ef2fb23",
"typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__mem",
"typing_X64.Bytes_Semantics_s.__proj__Mkstate__item__ok",
"typing_X64.Bytes_Semantics_s.eval_maddr",
"typing_X64.Bytes_Semantics_s.eval_mov128_op",
"typing_X64.Bytes_Semantics_s.op_String_Access",
"typing_X64.Bytes_Semantics_s.update_mov128_op_preserve_flags_",
"typing_X64.Leakage_Ins_Xmm.mov128_does_not_use_secret",
"typing_X64.Leakage_Ins_Xmm.xmm_taint", "typing_X64.Machine_s.xmm",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__memTaint",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__state",
"typing_X64.Taint_Semantics_s.__proj__MktraceState__item__trace",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__i",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__t",
"typing_X64.Taint_Semantics_s.ins_obs",
"typing_X64.Taint_Semantics_s.match_n",
"typing_X64.Taint_Semantics_s.operand_obs_list",
"typing_X64.Taint_Semantics_s.taint_eval_ins",
"typing_X64.Taint_Semantics_s.update_n",
"typing_tok_X64.Machine_s.Public@tok",
"typing_tok_X64.Machine_s.Secret@tok", "unit_inversion",
"unit_typing"
],
0,
"809328f0fefbe2c00da9d44c6fab4660"
],
[
"X64.Leakage_Ins_Xmm.lemma_movdqu_same_public",
1,
4,
2,
[
"@query", "equation_X64.Leakage_s.isExplicitLeakageFreeGivenStates",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2"
],
0,
"8804574f0c96f1b688590357f851c60a"
],
[
"X64.Leakage_Ins_Xmm.check_if_movdqu_leakage_free",
1,
4,
2,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"@fuel_correspondence_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"@query",
"X64.Taint_Semantics_s_pretyping_cc24b69d9ea89f288186d79510eec4aa",
"X64.Taint_Semantics_s_pretyping_e5512f1f3d006584f1f8889e0827cf63",
"constructor_distinct_Prims.Nil",
"constructor_distinct_X64.Machine_s.Ins",
"data_elim_FStar.Pervasives.Native.Mktuple2",
"data_typing_intro_X64.Machine_s.Ins@tok",
"disc_equation_X64.Bytes_Semantics_s.MOVDQU",
"equation_Prims.eqtype", "equation_X64.Leakage_s.constTimeInvariant",
"equation_X64.Leakage_s.isConstantTime",
"equation_X64.Leakage_s.isConstantTimeGivenStates",
"equation_X64.Leakage_s.isExplicitLeakageFree",
"equation_X64.Leakage_s.isLeakageFree",
"equation_X64.Taint_Semantics_s.extract_operands",
"equation_X64.Taint_Semantics_s.ins_obs",
"equation_X64.Taint_Semantics_s.tainted_code",
"equation_with_fuel_X64.Taint_Semantics_s.operand_obs_list.fuel_instrumented",
"equation_with_fuel_X64.Taint_Semantics_s.taint_eval_code.fuel_instrumented",
"fuel_guarded_inversion_X64.Leakage_s.taintState",
"fuel_guarded_inversion_X64.Taint_Semantics_s.tainted_ins",
"fuel_guarded_inversion_X64.Taint_Semantics_s.traceState",
"kinding_X64.Taint_Semantics_s.tainted_ins@tok",
"kinding_X64.Taint_Semantics_s.tainted_ocmp@tok",
"proj_equation_FStar.Pervasives.Native.Some_v",
"proj_equation_X64.Taint_Semantics_s.MktraceState_trace",
"proj_equation_X64.Taint_Semantics_s.TaintedIns_i",
"projection_inverse_BoxBool_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.Nil_a",
"projection_inverse_X64.Machine_s.Ins_ins",
"projection_inverse_X64.Machine_s.Ins_t_ins",
"projection_inverse_X64.Machine_s.Ins_t_ocmp",
"projection_inverse_X64.Taint_Semantics_s.MktraceState_trace",
"refinement_interpretation_Tm_refine_69a34f712728736367447fdb81c0edd0",
"typing_X64.Taint_Semantics_s.__proj__TaintedIns__item__i",
"typing_X64.Taint_Semantics_s.extract_operands"
],
0,
"40f80cc905c4c31ddfe6ad4e6bbaa9c8"
],
[
"X64.Leakage_Ins_Xmm.check_if_xmm_ins_consumes_fixed_time",
1,
4,
2,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"equation_X64.Taint_Semantics_s.is_xmm_ins",
"refinement_interpretation_Tm_refine_adf012ba59e36af09f3e5d996935ffab",
"typing_X64.Taint_Semantics_s.is_xmm_ins"
],
0,
"7f078c62f5b853e261611210e6772c3f"
]
]
]
Computing file changes ...
