[ "f\u000f\u001dDQ\u0000vQ\u0007.Z", [ [ "Vale.Stdcalls.X64.GCMdecrypt.as_t", 1, 1, 0, [ "@query" ], 0, "8a9bed0a0fa9ca9f3cbdfa654881ce7b" ], [ "Vale.Stdcalls.X64.GCMdecrypt.as_normal_t", 1, 1, 0, [ "@query" ], 0, "ea95d7af21c506c63997caba31489209" ], [ "Vale.Stdcalls.X64.GCMdecrypt.dom", 1, 1, 0, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "1a48ada2c45be0965321c3e6ece94473" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm128_pre", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "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.nat32", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Types.view_n", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e", "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Math.Poly2.Bits.of_nat32", "typing_Vale.Math.Poly2_s.degree" ], 0, "8bbc2c4dc986aae07db25a1be6e4bc7c" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm128_post", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "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.nat32", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Types.view_n", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e", "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Math.Poly2.Bits.of_nat32", "typing_Vale.Math.Poly2_s.degree" ], 0, "929f95880874e607a2057330d234ed1a" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm128_lemma'", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4", "Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Vale.AES.AES_s.AES_128", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "eq2-interp", "equality_tok_Vale.AES.AES_s.AES_128@tok", "equality_tok_Vale.Interop.Types.TUInt128@tok", "equality_tok_Vale.Interop.Types.TUInt8@tok", "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.GCM_helpers.bytes_to_quad_size", "equation_Vale.AES.X64.GCMdecrypt.va_ens_gcm_decrypt2_stdcall", "equation_Vale.AES.X64.GCMdecrypt.va_req_gcm_decrypt2_stdcall", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall", "equation_Vale.AsLowStar.ValeSig.vale_save_reg", "equation_Vale.AsLowStar.ValeSig.vale_save_xmm", "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Types.view_n", "equation_Vale.Interop.X64.regs_modified_stdcall", "equation_Vale.Interop.X64.xmms_modified_stdcall", "equation_Vale.Stdcalls.X64.GCMdecrypt.b128", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm128_post", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm128_pre", "equation_Vale.Stdcalls.X64.GCMdecrypt.uint64", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "function_token_typing_Vale.Interop.X64.regs_modified_stdcall", "function_token_typing_Vale.Interop.X64.xmms_modified_stdcall", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "int_typing", "interpretation_Tm_abs_552bcdab3a2dcaa6093987c035c90d48", "interpretation_Tm_abs_fc552ac6d480bd078bbd98d062a95a0a", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6ac5defca41e11e356d38353adc1f8fe", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_dd592ff911d0f80cdf0ace6c4224ff73", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_Vale.Interop.X64.regs_modified_stdcall", "token_correspondence_Vale.Interop.X64.xmms_modified_stdcall", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm128_post", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm128_pre", "typing_FStar.Ghost.reveal", "typing_FStar.Seq.Base.seq", "typing_FStar.UInt64.v", "typing_Vale.AES.AES_s.key_to_round_keys_LE", "typing_Vale.AES.X64.GCMdecrypt.va_code_gcm_decrypt2_stdcall", "typing_Vale.AES.X64.GCMdecrypt.va_lemma_gcm_decrypt2_stdcall", "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes", "typing_Vale.Interop.Assumptions.win", "typing_Vale.X64.Memory.buffer_as_seq", "typing_Vale.X64.MemoryAdapters.as_vale_buffer", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_tok_Vale.AES.AES_s.AES_128@tok", "typing_tok_Vale.Interop.Types.TUInt128@tok", "typing_tok_Vale.Interop.Types.TUInt8@tok" ], 0, "195688d57866bfd8d7f5e07eeef1f470" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm128_lemma", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "eq2-interp", "equality_tok_Vale.AES.AES_s.AES_128@tok", "equality_tok_Vale.Interop.Types.TUInt128@tok", "equality_tok_Vale.Interop.Types.TUInt8@tok", "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.X64.GCMdecrypt.va_ens_gcm_decrypt2_stdcall", "equation_Vale.AES.X64.GCMdecrypt.va_req_gcm_decrypt2_stdcall", "equation_Vale.AsLowStar.ValeSig.fuel_of", "equation_Vale.AsLowStar.ValeSig.state_of", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall", "equation_Vale.AsLowStar.ValeSig.vale_save_reg", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.view_n", "equation_Vale.Stdcalls.X64.GCMdecrypt.b128", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm128_post", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm128_pre", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "interpretation_Tm_abs_552bcdab3a2dcaa6093987c035c90d48", "interpretation_Tm_abs_fc552ac6d480bd078bbd98d062a95a0a", "lemma_Vale.X64.Memory.loc_includes_refl", "lemma_Vale.X64.Memory.loc_includes_union_l_buffer", "lemma_Vale.X64.Memory.modifies_buffer_readable", "lemma_Vale.X64.Memory.modifies_goal_directed_refl", "lemma_Vale.X64.Memory.modifies_goal_directed_trans", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm128_post", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm128_pre", "typing_Vale.AsLowStar.ValeSig.state_of", "typing_Vale.Interop.Assumptions.win", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.loc_none", "typing_Vale.X64.Memory.loc_union", "typing_Vale.X64.MemoryAdapters.as_vale_buffer", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_tok_Vale.Interop.Types.TUInt128@tok", "typing_tok_Vale.Interop.Types.TUInt8@tok" ], 0, "762b3771ef51fc81b7131de020b1d555" ], [ "Vale.Stdcalls.X64.GCMdecrypt.lowstar_gcm128_t", 1, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.squash", "equation_Vale.Interop.Base.arg", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "dc2984e9575c9dd2aa967dd946665a2a" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm256_pre", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "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.nat32", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Types.view_n", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e", "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Math.Poly2.Bits.of_nat32", "typing_Vale.Math.Poly2_s.degree" ], 0, "f6df9d02341cee8409218f1995338540" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm256_post", 1, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "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.nat32", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Types.view_n", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e", "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Math.Poly2.Bits.of_nat32", "typing_Vale.Math.Poly2_s.degree" ], 0, "afaf1b3a44a28e1611fa359724f779c2" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm256_lemma'", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "FStar.Seq.Base_pretyping_7efa52b424e80c83ad68a652aa3561e4", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4", "Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Vale.AES.AES_s.AES_256", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "eq2-interp", "equality_tok_Vale.AES.AES_s.AES_256@tok", "equality_tok_Vale.Interop.Types.TUInt128@tok", "equality_tok_Vale.Interop.Types.TUInt8@tok", "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.AES_s.is_aes_key_LE", "equation_Vale.AES.GCM_helpers.bytes_to_quad_size", "equation_Vale.AES.X64.GCMdecrypt.va_ens_gcm_decrypt2_stdcall", "equation_Vale.AES.X64.GCMdecrypt.va_req_gcm_decrypt2_stdcall", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall", "equation_Vale.AsLowStar.ValeSig.vale_save_reg", "equation_Vale.AsLowStar.ValeSig.vale_save_xmm", "equation_Vale.Def.Types_s.le_seq_quad32_to_bytes", "equation_Vale.Def.Types_s.quad32", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Base.buf_t", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.view_n", "equation_Vale.Interop.X64.regs_modified_stdcall", "equation_Vale.Interop.X64.xmms_modified_stdcall", "equation_Vale.Stdcalls.X64.GCMdecrypt.b128", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm256_post", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm256_pre", "equation_Vale.Stdcalls.X64.GCMdecrypt.uint64", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_FStar.UInt8.t", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "function_token_typing_Vale.Interop.X64.regs_modified_stdcall", "function_token_typing_Vale.Interop.X64.xmms_modified_stdcall", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "int_inversion", "int_typing", "interpretation_Tm_abs_1cfffe5e7914603434ba24f2557e5654", "interpretation_Tm_abs_8852f0eb87ddd122c854e36d4951dca1", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_Vale.AsLowStar.MemoryHelpers.as_vale_buffer_len", "lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "lemma_Vale.X64.Memory.modifies_buffer_addr", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_6ac5defca41e11e356d38353adc1f8fe", "refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647", "refinement_interpretation_Tm_refine_bc38afef117cbc3a0ecea14bc8e8d59b", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_dd592ff911d0f80cdf0ace6c4224ff73", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_Vale.Interop.X64.regs_modified_stdcall", "token_correspondence_Vale.Interop.X64.xmms_modified_stdcall", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm256_post", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm256_pre", "typing_FStar.Ghost.reveal", "typing_FStar.Seq.Base.seq", "typing_FStar.UInt64.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.length", "typing_Vale.AES.AES_s.key_to_round_keys_LE", "typing_Vale.AES.X64.GCMdecrypt.va_code_gcm_decrypt2_stdcall", "typing_Vale.AES.X64.GCMdecrypt.va_lemma_gcm_decrypt2_stdcall", "typing_Vale.Def.Types_s.le_seq_quad32_to_bytes", "typing_Vale.Interop.Assumptions.win", "typing_Vale.X64.Memory.buffer_as_seq", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.MemoryAdapters.as_vale_buffer", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_tok_Vale.AES.AES_s.AES_256@tok", "typing_tok_Vale.Interop.Types.TUInt128@tok", "typing_tok_Vale.Interop.Types.TUInt8@tok" ], 0, "f7bfd6423a5752f1f5bcf08aa411346b" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm256_lemma", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "eq2-interp", "equality_tok_Vale.AES.AES_s.AES_256@tok", "equality_tok_Vale.Interop.Types.TUInt128@tok", "equality_tok_Vale.Interop.Types.TUInt8@tok", "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.X64.GCMdecrypt.va_ens_gcm_decrypt2_stdcall", "equation_Vale.AES.X64.GCMdecrypt.va_req_gcm_decrypt2_stdcall", "equation_Vale.AsLowStar.ValeSig.fuel_of", "equation_Vale.AsLowStar.ValeSig.state_of", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall", "equation_Vale.AsLowStar.ValeSig.vale_save_reg", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.view_n", "equation_Vale.Stdcalls.X64.GCMdecrypt.b128", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm256_post", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm256_pre", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "interpretation_Tm_abs_1cfffe5e7914603434ba24f2557e5654", "interpretation_Tm_abs_8852f0eb87ddd122c854e36d4951dca1", "lemma_Vale.X64.Memory.loc_includes_refl", "lemma_Vale.X64.Memory.loc_includes_union_l_buffer", "lemma_Vale.X64.Memory.modifies_buffer_readable", "lemma_Vale.X64.Memory.modifies_goal_directed_refl", "lemma_Vale.X64.Memory.modifies_goal_directed_trans", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm256_post", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm256_pre", "typing_Vale.AsLowStar.ValeSig.state_of", "typing_Vale.Interop.Assumptions.win", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.loc_none", "typing_Vale.X64.Memory.loc_union", "typing_Vale.X64.MemoryAdapters.as_vale_buffer", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_tok_Vale.Interop.Types.TUInt128@tok", "typing_tok_Vale.Interop.Types.TUInt8@tok" ], 0, "8fb6e390c93e6f4c06e803548265e14d" ], [ "Vale.Stdcalls.X64.GCMdecrypt.lowstar_gcm256_t", 1, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.squash", "equation_Vale.Interop.Base.arg", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "f4acd5755668b4f1473617ed647444d1" ], [ "Vale.Stdcalls.X64.GCMdecrypt.lowstar_gcm128", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.squash", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "4e0a12491aca28ddac1b11c4c3327382" ], [ "Vale.Stdcalls.X64.GCMdecrypt.lowstar_gcm256", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.squash", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "42f8b64ed5220c8ecef33fdc151d23d4" ], [ "Vale.Stdcalls.X64.GCMdecrypt.as_t", 2, 1, 0, [ "@query" ], 0, "b539b0756356a8169185d72ba1c067ee" ], [ "Vale.Stdcalls.X64.GCMdecrypt.as_normal_t", 2, 1, 0, [ "@query" ], 0, "620ea066222062f5793ddf691ed5c260" ], [ "Vale.Stdcalls.X64.GCMdecrypt.dom", 2, 1, 0, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "4d0b5a0cbceffb1c31af8bafdf436296" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm128_pre", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "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.nat32", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Types.view_n", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e", "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Math.Poly2.Bits.of_nat32", "typing_Vale.Math.Poly2_s.degree" ], 0, "3ddf3589c90f555fa04b145dd0e215e4" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm128_post", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "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.nat32", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Types.view_n", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e", "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Math.Poly2.Bits.of_nat32", "typing_Vale.Math.Poly2_s.degree" ], 0, "cc2b554c30ecf978d0f8af2c99f78216" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm128_lemma'", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4", "Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Vale.AES.AES_s.AES_128", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "eq2-interp", "equality_tok_Vale.AES.AES_s.AES_128@tok", "equality_tok_Vale.Interop.Types.TUInt128@tok", "equality_tok_Vale.Interop.Types.TUInt8@tok", "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.GCM_helpers.bytes_to_quad_size", "equation_Vale.AES.X64.GCMdecrypt.va_ens_gcm_decrypt2_stdcall", "equation_Vale.AES.X64.GCMdecrypt.va_req_gcm_decrypt2_stdcall", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall", "equation_Vale.AsLowStar.ValeSig.vale_save_reg", "equation_Vale.AsLowStar.ValeSig.vale_save_xmm", "equation_Vale.Interop.Base.buf_t", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.view_n", "equation_Vale.Interop.X64.regs_modified_stdcall", "equation_Vale.Interop.X64.xmms_modified_stdcall", "equation_Vale.Stdcalls.X64.GCMdecrypt.b128", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm128_post", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm128_pre", "equation_Vale.Stdcalls.X64.GCMdecrypt.uint64", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_state_eq", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_stackTaint", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.State.state_eq", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_FStar.UInt8.t", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq", "function_token_typing_Vale.Interop.X64.regs_modified_stdcall", "function_token_typing_Vale.Interop.X64.xmms_modified_stdcall", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "int_inversion", "interpretation_Tm_abs_552bcdab3a2dcaa6093987c035c90d48", "interpretation_Tm_abs_fc552ac6d480bd078bbd98d062a95a0a", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_ok", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_6ac5defca41e11e356d38353adc1f8fe", "refinement_interpretation_Tm_refine_bc38afef117cbc3a0ecea14bc8e8d59b", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_Vale.Interop.X64.regs_modified_stdcall", "token_correspondence_Vale.Interop.X64.xmms_modified_stdcall", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm128_post", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm128_pre", "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Vale.AES.X64.GCMdecrypt.va_code_gcm_decrypt2_stdcall", "typing_Vale.AES.X64.GCMdecrypt.va_lemma_gcm_decrypt2_stdcall", "typing_Vale.Interop.Assumptions.win", "typing_Vale.X64.MemoryAdapters.as_vale_buffer", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_tok_Vale.AES.AES_s.AES_128@tok", "typing_tok_Vale.Interop.Types.TUInt128@tok", "typing_tok_Vale.Interop.Types.TUInt8@tok" ], 0, "ed81bdface83f5c88a10b16e8dbb8f72" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm128_lemma", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "eq2-interp", "equality_tok_Vale.AES.AES_s.AES_128@tok", "equality_tok_Vale.Interop.Types.TUInt128@tok", "equality_tok_Vale.Interop.Types.TUInt8@tok", "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.X64.GCMdecrypt.va_ens_gcm_decrypt2_stdcall", "equation_Vale.AES.X64.GCMdecrypt.va_req_gcm_decrypt2_stdcall", "equation_Vale.AsLowStar.ValeSig.fuel_of", "equation_Vale.AsLowStar.ValeSig.state_of", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall", "equation_Vale.AsLowStar.ValeSig.vale_save_reg", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.view_n", "equation_Vale.Stdcalls.X64.GCMdecrypt.b128", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm128_post", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm128_pre", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "interpretation_Tm_abs_552bcdab3a2dcaa6093987c035c90d48", "interpretation_Tm_abs_fc552ac6d480bd078bbd98d062a95a0a", "lemma_Vale.X64.Memory.loc_includes_refl", "lemma_Vale.X64.Memory.loc_includes_union_l_buffer", "lemma_Vale.X64.Memory.modifies_buffer_readable", "lemma_Vale.X64.Memory.modifies_goal_directed_refl", "lemma_Vale.X64.Memory.modifies_goal_directed_trans", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm128_post", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm128_pre", "typing_Vale.AsLowStar.ValeSig.state_of", "typing_Vale.Interop.Assumptions.win", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.loc_none", "typing_Vale.X64.Memory.loc_union", "typing_Vale.X64.MemoryAdapters.as_vale_buffer", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_tok_Vale.Interop.Types.TUInt128@tok", "typing_tok_Vale.Interop.Types.TUInt8@tok" ], 0, "fbaff3e0c8fb3230aaa0b6b1c4e932ed" ], [ "Vale.Stdcalls.X64.GCMdecrypt.lowstar_gcm128_t", 2, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.squash", "equation_Vale.Interop.Base.arg", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "e70bd35a5f27f9eab5e3e008593915af" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm256_pre", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "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.nat32", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Types.view_n", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e", "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Math.Poly2.Bits.of_nat32", "typing_Vale.Math.Poly2_s.degree" ], 0, "54e7835f2feb927078e7a36ebd9b1066" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm256_post", 2, 1, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "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.nat32", "equation_Vale.Def.Words_s.natN", "equation_Vale.Interop.Types.view_n", "equation_with_fuel_Prims.pow2.fuel_instrumented", "function_token_typing_Vale.Math.Poly2.Bits.of_nat32_ones", "int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values", "lemma_Vale.Math.Poly2.Lemmas.lemma_ones_degree", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_10fce5557d0593095ff373cff619471e", "refinement_interpretation_Tm_refine_37b3edec16faddba730e4e710f565937", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "typing_Vale.Math.Poly2.Bits.of_nat32", "typing_Vale.Math.Poly2_s.degree" ], 0, "b762d8698e55f9f2b8c7cc654f1fc6ba" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm256_lemma'", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4", "Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf", "b2t_def", "bool_inversion", "bool_typing", "constructor_distinct_Vale.AES.AES_s.AES_256", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "eq2-interp", "equality_tok_Vale.AES.AES_s.AES_256@tok", "equality_tok_Vale.Interop.Types.TUInt128@tok", "equality_tok_Vale.Interop.Types.TUInt8@tok", "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.GCM_helpers.bytes_to_quad_size", "equation_Vale.AES.X64.GCMdecrypt.va_ens_gcm_decrypt2_stdcall", "equation_Vale.AES.X64.GCMdecrypt.va_req_gcm_decrypt2_stdcall", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall", "equation_Vale.AsLowStar.ValeSig.vale_save_reg", "equation_Vale.AsLowStar.ValeSig.vale_save_xmm", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Interop.Base.buf_t", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.view_n", "equation_Vale.Interop.X64.regs_modified_stdcall", "equation_Vale.Interop.X64.xmms_modified_stdcall", "equation_Vale.Stdcalls.X64.GCMdecrypt.b128", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm256_post", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm256_pre", "equation_Vale.Stdcalls.X64.GCMdecrypt.uint64", "equation_Vale.X64.Decls.va_ensure_total", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Memory.base_typ_as_vale_type", "equation_Vale.X64.Memory.buffer128", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_FStar.UInt8.t", "function_token_typing_Prims.__cache_version_number__", "function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Interop.X64.regs_modified_stdcall", "function_token_typing_Vale.Interop.X64.xmms_modified_stdcall", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "int_inversion", "int_typing", "interpretation_Tm_abs_1cfffe5e7914603434ba24f2557e5654", "interpretation_Tm_abs_8852f0eb87ddd122c854e36d4951dca1", "lemma_Vale.X64.Memory.buffer_length_buffer_as_seq", "lemma_Vale.X64.Memory.modifies_buffer_addr", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "proj_equation_Vale.X64.State.Mkvale_state_vs_stackTaint", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_regs", "projection_inverse_Vale.X64.State.Mkvale_state_vs_stack", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_6ac5defca41e11e356d38353adc1f8fe", "refinement_interpretation_Tm_refine_bc38afef117cbc3a0ecea14bc8e8d59b", "refinement_interpretation_Tm_refine_dd592ff911d0f80cdf0ace6c4224ff73", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_Vale.Interop.X64.regs_modified_stdcall", "token_correspondence_Vale.Interop.X64.xmms_modified_stdcall", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm256_post", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm256_pre", "typing_FStar.Ghost.reveal", "typing_FStar.Seq.Base.seq", "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Vale.AES.AES_s.key_to_round_keys_LE", "typing_Vale.AES.X64.GCMdecrypt.va_code_gcm_decrypt2_stdcall", "typing_Vale.AES.X64.GCMdecrypt.va_lemma_gcm_decrypt2_stdcall", "typing_Vale.Interop.Assumptions.win", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.MemoryAdapters.as_vale_buffer", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_tok_Vale.AES.AES_s.AES_256@tok", "typing_tok_Vale.Interop.Types.TUInt128@tok", "typing_tok_Vale.Interop.Types.TUInt8@tok" ], 0, "d9b5efb35b8eee97ec9f4dcfa652318b" ], [ "Vale.Stdcalls.X64.GCMdecrypt.gcm256_lemma", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "bool_inversion", "constructor_distinct_Vale.Interop.Types.TUInt128", "constructor_distinct_Vale.Interop.Types.TUInt8", "eq2-interp", "equality_tok_Vale.AES.AES_s.AES_256@tok", "equality_tok_Vale.Interop.Types.TUInt128@tok", "equality_tok_Vale.Interop.Types.TUInt8@tok", "equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_Prims.eq2", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.X64.GCMdecrypt.va_ens_gcm_decrypt2_stdcall", "equation_Vale.AES.X64.GCMdecrypt.va_req_gcm_decrypt2_stdcall", "equation_Vale.AsLowStar.ValeSig.fuel_of", "equation_Vale.AsLowStar.ValeSig.state_of", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions", "equation_Vale.AsLowStar.ValeSig.vale_calling_conventions_stdcall", "equation_Vale.AsLowStar.ValeSig.vale_save_reg", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.view_n", "equation_Vale.Stdcalls.X64.GCMdecrypt.b128", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm256_post", "equation_Vale.Stdcalls.X64.GCMdecrypt.gcm256_pre", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_upd_flags", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_stack", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_Semantics_s.code", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_FStar.Pervasives.Native.tuple2", "fuel_guarded_inversion_Vale.X64.State.vale_state", "function_token_typing_Vale.AsLowStar.MemoryHelpers.fuel_eq", "function_token_typing_Vale.X64.MemoryAdapters.code_equiv", "interpretation_Tm_abs_1cfffe5e7914603434ba24f2557e5654", "interpretation_Tm_abs_8852f0eb87ddd122c854e36d4951dca1", "lemma_Vale.X64.Memory.loc_includes_refl", "lemma_Vale.X64.Memory.loc_includes_union_l_buffer", "lemma_Vale.X64.Memory.modifies_buffer_readable", "lemma_Vale.X64.Memory.modifies_goal_directed_refl", "lemma_Vale.X64.Memory.modifies_goal_directed_trans", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.X64.State.Mkvale_state_vs_flags", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_memTaint", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "proj_equation_Vale.X64.State.Mkvale_state_vs_regs", "proj_equation_Vale.X64.State.Mkvale_state_vs_stack", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm256_post", "token_correspondence_Vale.Stdcalls.X64.GCMdecrypt.gcm256_pre", "typing_Vale.AsLowStar.ValeSig.state_of", "typing_Vale.Interop.Assumptions.win", "typing_Vale.X64.Memory.loc_buffer", "typing_Vale.X64.Memory.loc_none", "typing_Vale.X64.Memory.loc_union", "typing_Vale.X64.MemoryAdapters.as_vale_buffer", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_heap", "typing_tok_Vale.Interop.Types.TUInt128@tok", "typing_tok_Vale.Interop.Types.TUInt8@tok" ], 0, "cfd867292285608d80a20ff254a52f94" ], [ "Vale.Stdcalls.X64.GCMdecrypt.lowstar_gcm256_t", 2, 1, 0, [ "@MaxIFuel_assumption", "@fuel_correspondence_FStar.List.Tot.Base.length.fuel_instrumented", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.squash", "equation_Vale.Interop.Base.arg", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "b4afb4f475646eacfa67fb72016d9ad8" ], [ "Vale.Stdcalls.X64.GCMdecrypt.lowstar_gcm128", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.squash", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "121b5317fe68f9977ae4e6c897e4610e" ], [ "Vale.Stdcalls.X64.GCMdecrypt.lowstar_gcm256", 2, 1, 0, [ "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.squash", "equation_Vale.X64.Machine_Semantics_s.ins", "equation_Vale.X64.Machine_Semantics_s.ocmp", "function_token_typing_Vale.X64.MemoryAdapters.ins_equiv", "function_token_typing_Vale.X64.MemoryAdapters.ocmp_equiv", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" ], 0, "ca2d10778cd6ec43cae8601f390d8cf2" ] ] ]