[ "<`¤\u0005KÐ\u001eî?Í\fŽ\u0014öK(", [ [ "Vale.Stdcalls.X64.GCM_IV.as_t", 1, 1, 0, [ "@query" ], 0, "945dc3cd63a01a9163373b7592ee9fa4" ], [ "Vale.Stdcalls.X64.GCM_IV.as_normal_t", 1, 1, 0, [ "@query" ], 0, "83be85bed5b6befae88d1e1815052bab" ], [ "Vale.Stdcalls.X64.GCM_IV.dom", 1, 1, 0, [ "@query", "projection_inverse_BoxInt_proj_0" ], 0, "a9ffb992e83b4d9530492794f3b797b7" ], [ "Vale.Stdcalls.X64.GCM_IV.compute_iv_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, "f03da93c0ecc2c8a29fd252aa2585575" ], [ "Vale.Stdcalls.X64.GCM_IV.compute_iv_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, "198c9e434ef34e1ef0110e9c99cc8407" ], [ "Vale.Stdcalls.X64.GCM_IV.compute_iv_lemma'", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "Prims_pretyping_ae567c2fb75be05905677af440075565", "Vale.Interop.X64_interpretation_Tm_arrow_829b64a0a0118c2bcbf8116d158118c4", "Vale.Interop.X64_interpretation_Tm_arrow_972e4e2c724f700a5019205902fe83cf", "bool_inversion", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt128", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash", "equation_Vale.AES.X64.GCMencryptOpt.va_ens_Compute_iv_stdcall", "equation_Vale.AES.X64.GCMencryptOpt.va_req_Compute_iv_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.GCM_IV.b128", "equation_Vale.Stdcalls.X64.GCM_IV.compute_iv_post", "equation_Vale.Stdcalls.X64.GCM_IV.compute_iv_pre", "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.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Machine_s.reg_64", "equation_Vale.X64.Memory.get_vale_heap", "equation_Vale.X64.Memory.set_vale_heap", "equation_Vale.X64.State.update_reg", "equation_Vale.X64.State.update_reg_64", "equation_Vale.X64.State.update_reg_xmm", "fuel_guarded_inversion_Vale.X64.State.vale_state", "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", "int_typing", "interpretation_Tm_abs_02372ed63056d20fa848fd795bdc90ef", "interpretation_Tm_abs_11a08b99d0b34794b3b4c7b9434881df", "lemma_LowStar.Monotonic.Buffer.length_null_1", "lemma_LowStar.Monotonic.Buffer.length_null_2", "lemma_Vale.AsLowStar.MemoryHelpers.as_vale_buffer_len", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "proj_equation_Vale.X64.State.Mkvale_state_vs_ok", "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.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5", "refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80", "token_correspondence_Vale.Interop.X64.regs_modified_stdcall", "token_correspondence_Vale.Interop.X64.xmms_modified_stdcall", "token_correspondence_Vale.Stdcalls.X64.GCM_IV.compute_iv_post", "token_correspondence_Vale.Stdcalls.X64.GCM_IV.compute_iv_pre", "typing_FStar.UInt8.t", "typing_LowStar.Buffer.trivial_preorder", "typing_Vale.Interop.Assumptions.win", "typing_Vale.Interop.Types.view_n", "typing_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok" ], 0, "0007e39d5c498017e0af02e59b739aeb" ], [ "Vale.Stdcalls.X64.GCM_IV.compute_iv_lemma", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "eq2-interp", "equality_tok_Vale.Arch.HeapTypes_s.Secret@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok", "equation_FStar.Pervasives.Native.fst", "equation_FStar.Pervasives.Native.snd", "equation_FStar.UInt.fits", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_LowStar.Buffer.buffer", "equation_Prims.eq2", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.squash", "equation_Vale.AES.X64.GCMencryptOpt.va_ens_Compute_iv_stdcall", "equation_Vale.AES.X64.GCMencryptOpt.va_req_Compute_iv_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.Base.buf_t", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Stdcalls.X64.GCM_IV.b128", "equation_Vale.Stdcalls.X64.GCM_IV.compute_iv_post", "equation_Vale.Stdcalls.X64.GCM_IV.compute_iv_pre", "equation_Vale.X64.Decls.va_require_total", "equation_Vale.X64.Decls.va_upd_mem", "equation_Vale.X64.Decls.va_upd_mem_layout", "equation_Vale.X64.Decls.va_upd_ok", "equation_Vale.X64.Decls.va_upd_reg64", "equation_Vale.X64.Decls.va_upd_xmm", "equation_Vale.X64.Decls.validDstAddrs", "equation_Vale.X64.Decls.validDstAddrs128", "equation_Vale.X64.Decls.validSrcAddrs", "equation_Vale.X64.Decls.validSrcAddrs128", "equation_Vale.X64.Memory.buffer128", "equation_Vale.X64.Memory.get_vale_heap", "equation_Vale.X64.Memory.set_vale_heap", "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", "interpretation_Tm_abs_02372ed63056d20fa848fd795bdc90ef", "interpretation_Tm_abs_11a08b99d0b34794b3b4c7b9434881df", "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", "primitive_Prims.op_AmpAmp", "proj_equation_FStar.Pervasives.Native.Mktuple2__1", "proj_equation_FStar.Pervasives.Native.Mktuple2__2", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "proj_equation_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_layout", "proj_equation_Vale.X64.State.Mkvale_state_vs_heap", "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_BoxBool_proj_0", "projection_inverse_Vale.Arch.HeapImpl.Mkvale_full_heap_vf_heap", "projection_inverse_Vale.X64.State.Mkvale_state_vs_heap", "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_83bd940927020bb51199658f6752ed80", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "token_correspondence_Vale.Stdcalls.X64.GCM_IV.compute_iv_post", "token_correspondence_Vale.Stdcalls.X64.GCM_IV.compute_iv_pre", "typing_FStar.UInt32.v", "typing_FStar.UInt8.t", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_Vale.AsLowStar.ValeSig.state_of", "typing_Vale.Interop.Assumptions.win", "typing_Vale.X64.Memory.get_vale_heap", "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_Vale.X64.State.__proj__Mkvale_state__item__vs_ok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt128@tok", "typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok" ], 0, "d67995d19e1abed7b7b54826907a671b" ], [ "Vale.Stdcalls.X64.GCM_IV.lowstar_compute_iv_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, "2c7e48e310528c27230845ddd19676f8" ], [ "Vale.Stdcalls.X64.GCM_IV.lowstar_compute_iv", 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, "1e01e434289ed4a0e18de299a5986454" ] ] ]