[ "\bVA,5\\", [ [ "Vale.X64.Instructions_s.eval_Add64", 1, 1, 0, [ "@query" ], 0, "fce27c26ee49785c8e8c3e122f992297" ], [ "Vale.X64.Instructions_s.eval_AddLea64", 1, 1, 0, [ "@query" ], 0, "a99b8ec0fcdb6530178a92921291149f" ], [ "Vale.X64.Instructions_s.eval_AddCarry64", 1, 1, 0, [ "@query" ], 0, "233eba34f2cd6ded7a194ce8c476c00a" ], [ "Vale.X64.Instructions_s.eval_Adcx64_Adox64", 1, 1, 0, [ "@query" ], 0, "52b41d9c8d4ba621da6aa4ac39dea3ba" ], [ "Vale.X64.Instructions_s.eval_Sub64", 1, 1, 0, [ "@query" ], 0, "5edcc5499eff48efa92cc4c5bb25aa17" ], [ "Vale.X64.Instructions_s.eval_Sbb64", 1, 1, 0, [ "@query" ], 0, "b738181b59e3f73e83db951e87e79629" ], [ "Vale.X64.Instructions_s.eval_Mul64", 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_FStar.UInt.uint_t", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec" ], 0, "45a24fdfb173bfa61673e6d3005cf269" ], [ "Vale.X64.Instructions_s.eval_Mulx64", 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_FStar.UInt.uint_t", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec" ], 0, "e99328cedfb44dcba9b1edcccf80409c" ], [ "Vale.X64.Instructions_s.eval_IMul64", 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", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "fbcc0142399dd4dbd47e9e24c6662669" ], [ "Vale.X64.Instructions_s.eval_Paddd_raw", 1, 1, 0, [ "@query" ], 0, "e1114a5c090d5b2167b21b734826a7ce" ], [ "Vale.X64.Instructions_s.eval_Psrldq", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "function_token_typing_Vale.Def.Words_s.nat8", "int_inversion", "int_typing", "lemma_FStar.Seq.Base.lemma_create_len", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_FStar.Seq.Base.length" ], 0, "55a16df5440a9853eb7f16b0b3153500" ], [ "Vale.X64.Instructions_s.eval_Pcmpeqd", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "263a502ec4857a57ea3ebf21dd32c204" ], [ "Vale.X64.Instructions_s.eval_Pextrq", 1, 1, 0, [ "@query" ], 0, "757eb6baa9eebcb1af3aec1c1ffb5bfd" ], [ "Vale.X64.Instructions_s.eval_Pinsrd", 1, 1, 0, [ "@query" ], 0, "d30db427c9bbef7cccad193099890c50" ], [ "Vale.X64.Instructions_s.eval_Pinsrq", 1, 1, 0, [ "@query" ], 0, "111ff859b529878cab4f72c65f20e51e" ], [ "Vale.X64.Instructions_s.eval_AESNI_keygen_assist", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c" ], 0, "88af1606bbb4fce8a0323b5f44f057c6" ], [ "Vale.X64.Instructions_s.ins_SHA256_rnds2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Vale.X64.Machine_s.reg_xmm", "function_token_typing_Prims.int", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "haseqTm_refine_c365eb902b454950de62fba701d9049d", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f" ], 0, "08fa1920eaf10b541102f19c536ee29f" ] ] ]