[ "%\u0002\nL@\u007fX0I", [ [ "Vale.Wrapper.X64.GCMencryptOpt.length_aux", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.BufferView.Down.buffer", "equation_Prims.eqtype", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.down_view", "equation_Vale.Interop.Types.get_downview", "equation_Vale.Interop.Views.down_view8", "equation_Vale.Wrapper.X64.GCMencryptOpt.uint8_p", "fuel_guarded_inversion_FStar.Pervasives.dtuple4", "lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view", "lemma_LowStar.BufferView.Down.get_view_mk_buffer_view", "proj_equation_FStar.Pervasives.Mkdtuple4__1", "proj_equation_FStar.Pervasives.Mkdtuple4__2", "proj_equation_FStar.Pervasives.Mkdtuple4__3", "proj_equation_LowStar.BufferView.Down.View_n", "projection_inverse_BoxInt_proj_0", "projection_inverse_LowStar.BufferView.Down.View_n", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "typing_FStar.UInt8.t", "typing_LowStar.Buffer.trivial_preorder", "typing_Vale.Interop.Types.down_view", "typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok" ], 0, "e65fe314c6e8d802d182b68785408ee9" ], [ "Vale.Wrapper.X64.GCMencryptOpt.length_aux2", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.BufferView.Down.buffer", "equation_Prims.eqtype", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.down_view", "equation_Vale.Interop.Types.get_downview", "equation_Vale.Interop.Views.down_view8", "equation_Vale.Wrapper.X64.GCMencryptOpt.uint8_p", "fuel_guarded_inversion_FStar.Pervasives.dtuple4", "lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view", "lemma_LowStar.BufferView.Down.get_view_mk_buffer_view", "proj_equation_FStar.Pervasives.Mkdtuple4__1", "proj_equation_FStar.Pervasives.Mkdtuple4__2", "proj_equation_FStar.Pervasives.Mkdtuple4__3", "proj_equation_LowStar.BufferView.Down.View_n", "projection_inverse_BoxInt_proj_0", "projection_inverse_LowStar.BufferView.Down.View_n", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "typing_FStar.UInt8.t", "typing_LowStar.Buffer.trivial_preorder", "typing_Vale.Interop.Types.down_view", "typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok" ], 0, "17380c51098aa19cc8ad0dca93f7986d" ], [ "Vale.Wrapper.X64.GCMencryptOpt.length_aux3", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.BufferView.Down.buffer", "equation_Prims.eqtype", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.down_view", "equation_Vale.Interop.Types.get_downview", "equation_Vale.Interop.Views.down_view8", "equation_Vale.Wrapper.X64.GCMencryptOpt.uint8_p", "fuel_guarded_inversion_FStar.Pervasives.dtuple4", "lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view", "lemma_LowStar.BufferView.Down.get_view_mk_buffer_view", "proj_equation_FStar.Pervasives.Mkdtuple4__1", "proj_equation_FStar.Pervasives.Mkdtuple4__2", "proj_equation_FStar.Pervasives.Mkdtuple4__3", "proj_equation_LowStar.BufferView.Down.View_n", "projection_inverse_BoxInt_proj_0", "projection_inverse_LowStar.BufferView.Down.View_n", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "typing_FStar.UInt8.t", "typing_LowStar.Buffer.trivial_preorder", "typing_Vale.Interop.Types.down_view", "typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok" ], 0, "0adac1ffaf925774d42eb4aa2508a783" ], [ "Vale.Wrapper.X64.GCMencryptOpt.length_aux4", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.BufferView.Down.buffer", "equation_Prims.eqtype", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.down_view", "equation_Vale.Interop.Types.get_downview", "equation_Vale.Interop.Views.down_view8", "equation_Vale.Wrapper.X64.GCMencryptOpt.uint8_p", "fuel_guarded_inversion_FStar.Pervasives.dtuple4", "lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view", "lemma_LowStar.BufferView.Down.get_view_mk_buffer_view", "proj_equation_FStar.Pervasives.Mkdtuple4__1", "proj_equation_FStar.Pervasives.Mkdtuple4__2", "proj_equation_FStar.Pervasives.Mkdtuple4__3", "proj_equation_LowStar.BufferView.Down.View_n", "projection_inverse_BoxInt_proj_0", "projection_inverse_LowStar.BufferView.Down.View_n", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "typing_FStar.UInt8.t", "typing_LowStar.Buffer.trivial_preorder", "typing_Vale.Interop.Types.down_view", "typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok" ], 0, "c5e62fb9f931f3bd427156533762e926" ], [ "Vale.Wrapper.X64.GCMencryptOpt.length_aux5", 1, 1, 0, [ "@MaxIFuel_assumption", "@query", "constructor_distinct_Vale.Arch.HeapTypes_s.TUInt8", "equality_tok_Vale.Arch.HeapTypes_s.TUInt8@tok", "equation_LowStar.Buffer.buffer", "equation_LowStar.Buffer.trivial_preorder", "equation_LowStar.BufferView.Down.buffer", "equation_Prims.eqtype", "equation_Vale.Interop.Types.base_typ_as_type", "equation_Vale.Interop.Types.down_view", "equation_Vale.Interop.Types.get_downview", "equation_Vale.Interop.Views.down_view8", "equation_Vale.Wrapper.X64.GCMencryptOpt.uint8_p", "fuel_guarded_inversion_FStar.Pervasives.dtuple4", "lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view", "lemma_LowStar.BufferView.Down.get_view_mk_buffer_view", "proj_equation_FStar.Pervasives.Mkdtuple4__1", "proj_equation_FStar.Pervasives.Mkdtuple4__2", "proj_equation_FStar.Pervasives.Mkdtuple4__3", "proj_equation_LowStar.BufferView.Down.View_n", "projection_inverse_BoxInt_proj_0", "projection_inverse_LowStar.BufferView.Down.View_n", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "typing_FStar.UInt8.t", "typing_LowStar.Buffer.trivial_preorder", "typing_Vale.Interop.Types.down_view", "typing_tok_Vale.Arch.HeapTypes_s.TUInt8@tok" ], 0, "7cba0ec4d98852c646a28841a89d85cf" ], [ "Vale.Wrapper.X64.GCMencryptOpt.encrypt_opt_stdcall_st", 1, 0, 0, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.List.Tot.Base_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe", "FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251", "Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def", "constructor_distinct_Tm_unit", "eq2-interp", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_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.eqtype", "equation_Prims.nat", "equation_Vale.AES.AES_s.is_aes_key", "equation_Vale.AES.AES_s.is_aes_key_LE", "equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE", "equation_Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8", "equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8", "equation_Vale.Lib.Seqs_s.compose", "equation_Vale.Lib.Seqs_s.seq_map", "equation_Vale.Wrapper.X64.GCMencryptOpt.uint8_p", "function_token_typing_Prims.int", "function_token_typing_Vale.Def.Words_s.nat32", "function_token_typing_Vale.Def.Words_s.nat8", "haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion", "int_typing", "kinding_Vale.Def.Words_s.four@tok", "lemma_FStar.Seq.Base.lemma_init_len", "lemma_FStar.UInt.pow2_values", "lemma_LowStar.Monotonic.Buffer.length_as_seq", "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_12cfdc5e5e9b4a21e137c684eae73d5b", "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Tm_refine_47d796a4c5bf318cb5b6b579aa95194f", "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2", "refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c", "refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55", "refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec", "typing_FStar.Ghost.reveal", "typing_FStar.Seq.Base.init", "typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.seq", "typing_FStar.UInt32.v", "typing_FStar.UInt8.t", "typing_LowStar.Buffer.trivial_preorder", "typing_LowStar.Monotonic.Buffer.len", "typing_LowStar.Monotonic.Buffer.length", "typing_Tm_abs_12f0bbc5cd2aeb167bc7e771b588a4ca", "typing_Vale.Def.Words.Seq_s.seq_four_to_seq_LE" ], 0, "2d3a4667e74d1bcff433c355b9ee7b00" ] ] ]