[ "\u0001X+Z`EU@gOv%", [ [ "Hacl.Impl.Salsa20.state", 1, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.op_Less_Less_Less", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "bool_typing", "data_elim_FStar.UInt32.Mk", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.sub", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_Hacl.Impl.Salsa20.u32", "equation_Spec.Salsa20.constant2", "fuel_guarded_inversion_FStar.UInt32.t_", "function_token_typing_Spec.Salsa20.constant2", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt32.Mk_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.UInt32.Mk_v", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_c8815129b4a7e19454e6f8a062b651d7", "typing_FStar.UInt32.v" ], 0 ], [ "Hacl.Impl.Salsa20.setup", 1, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.setup", 2, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.setup", 3, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.UInt32.t", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_34c713272d4138e534ee70be89b06637", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_59174d15900b1aac0e68774108209b07" ], 0 ], [ "Hacl.Impl.Salsa20.setup", 4, 0, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented", "@query", "assumption_FStar.Monotonic.HyperHeap.HasEq_rid", "bool_inversion", "data_elim_FStar.Buffer.MkBuffer", "data_elim_FStar.Monotonic.HyperStack.HS", "data_elim_FStar.Monotonic.HyperStack.MkRef", "eq2-interp", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.content", "equation_FStar.Buffer.disjoint", "equation_FStar.Buffer.equal", "equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.idx", "equation_FStar.Buffer.includes", "equation_FStar.Buffer.length", "equation_FStar.Buffer.live", "equation_FStar.Buffer.sub", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.HyperStack.reference", "equation_FStar.Monotonic.HyperHeap.map_invariant", "equation_FStar.Monotonic.HyperHeap.t", "equation_FStar.Monotonic.HyperStack.contains", "equation_FStar.Monotonic.HyperStack.equal_domains", "equation_FStar.Monotonic.HyperStack.frameOf", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.hh", "equation_FStar.Monotonic.HyperStack.is_in", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.live_region", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Set.eqtype", "equation_FStar.UInt.add", "equation_FStar.UInt32.add", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Cast.uint32_to_sint32", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.Lib.Create.h32", "equation_Prims.eqtype", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant1", "equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.constant3", "equation_Spec.Salsa20.setup", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference", "fuel_guarded_inversion_FStar.UInt32.t_", "fuel_guarded_inversion_FStar.UInt64.t_", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_FStar.Monotonic.HyperHeap.rid", "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok", "lemma_FStar.Buffer.lemma_disjoint_sub", "lemma_FStar.Buffer.lemma_disjoint_symm", "lemma_FStar.Buffer.lemma_equal_domains_2", "lemma_FStar.Buffer.lemma_fresh_poppable", "lemma_FStar.Buffer.lemma_live_disjoint", "lemma_FStar.Buffer.lemma_modifies_0_1", "lemma_FStar.Buffer.lemma_modifies_0_1_", "lemma_FStar.Buffer.lemma_sub_spec", "lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped", "lemma_FStar.Buffer.modifies_poppable_1", "lemma_FStar.Buffer.modifies_popped_1", "lemma_FStar.Buffer.modifies_subbuffer_1", "lemma_FStar.Buffer.no_upd_fresh", "lemma_FStar.Buffer.no_upd_lemma_0", "lemma_FStar.Buffer.no_upd_lemma_1", "lemma_FStar.Buffer.no_upd_popped", "lemma_FStar.Set.lemma_equal_elim", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_disEquality", "proj_equation_FStar.Buffer.MkBuffer_content", "proj_equation_FStar.Buffer.MkBuffer_idx", "proj_equation_FStar.Buffer.MkBuffer_length", "proj_equation_FStar.Buffer.MkBuffer_max_length", "proj_equation_FStar.Monotonic.HyperStack.HS_h", "proj_equation_FStar.Monotonic.HyperStack.HS_tip", "proj_equation_FStar.Monotonic.HyperStack.MkRef_id", "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Buffer.MkBuffer_idx", "projection_inverse_FStar.UInt32.Mk_v", "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9", "refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_0418702750d54a72833a38f310956e3d", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_38d52172626ad62ce3b0e4245dab71ed", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_b05295ea25e1fbfe5a4bd48cb81ddfff", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_34c713272d4138e534ee70be89b06637", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_59174d15900b1aac0e68774108209b07", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_75b40552a174a1363c5e0311450b0452", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_91bf11ca596227ccc8e0d88461b1158c", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "typing_FStar.Buffer.__proj__MkBuffer__item__content", "typing_FStar.Buffer.__proj__MkBuffer__item__idx", "typing_FStar.Buffer.__proj__MkBuffer__item__length", "typing_FStar.Buffer.content", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperHeap.includes", "typing_FStar.Monotonic.HyperStack.__proj__HS__item__h", "typing_FStar.Monotonic.HyperStack.__proj__HS__item__tip", "typing_FStar.Monotonic.HyperStack.poppable" ], 0 ], [ "Hacl.Impl.Salsa20.line", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.v", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.idx", "equation_Hacl.Impl.Salsa20.state", "lemma_FStar.Buffer.lemma_size", "primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5fd76f96dd8842f1d4e9ef690b5c4ee7", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_c8815129b4a7e19454e6f8a062b651d7", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "typing_FStar.UInt32.v" ], 0 ], [ "Hacl.Impl.Salsa20.line", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.UInt32.t", "equation_FStar.UInt32.v", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.idx", "equation_Hacl.Impl.Salsa20.op_Less_Less_Less", "equation_Hacl.Impl.Salsa20.state", "equation_Spec.Lib.op_Less_Less_Less", "equation_Spec.Lib.rotate_left", "equation_Spec.Salsa20.line", "equation_Spec.Salsa20.state", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "fuel_guarded_inversion_FStar.UInt32.t_", "interpretation_Spec.Salsa20_Tm_abs_c99d884abfcd935d4c8bcf43ad8d4dcf", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5fd76f96dd8842f1d4e9ef690b5c4ee7", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "refinement_interpretation_Spec.Lib_Tm_refine_08b7b502ca9d52863cc90a1acbeae1a4", "token_correspondence_Spec.Salsa20.line" ], 0 ], [ "Hacl.Impl.Salsa20.quarter_round", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.v", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.idx", "equation_Hacl.Impl.Salsa20.state", "lemma_FStar.Buffer.lemma_size", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5fd76f96dd8842f1d4e9ef690b5c4ee7", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "typing_FStar.UInt32.v" ], 0 ], [ "Hacl.Impl.Salsa20.quarter_round", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.live", "equation_FStar.Monotonic.HyperHeap.contains_ref", "equation_FStar.Monotonic.HyperStack.contains", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "equation_Spec.Lib.op_At", "equation_Spec.Salsa20.quarter_round", "equation_Spec.Salsa20.state", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "kinding_FStar.UInt32.t_@tok", "lemma_FStar.Buffer.lemma_modifies_1_trans", "lemma_FStar.Monotonic.HyperStack.lemma_equal_domains_trans", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan", "proj_equation_FStar.UInt32.Mk_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.UInt32.Mk_v", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "token_correspondence_Spec.Lib.op_At", "token_correspondence_Spec.Salsa20.line", "token_correspondence_Spec.Salsa20.quarter_round" ], 0 ], [ "Hacl.Impl.Salsa20.column_round", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.UInt32.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8" ], 0 ], [ "Hacl.Impl.Salsa20.column_round", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "equation_Spec.Lib.op_At", "equation_Spec.Salsa20.column_round", "equation_Spec.Salsa20.state", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "kinding_FStar.UInt32.t_@tok", "lemma_FStar.Buffer.lemma_modifies_1_trans", "lemma_FStar.Monotonic.HyperStack.lemma_equal_domains_trans", "proj_equation_FStar.UInt32.Mk_v", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.UInt32.Mk_v", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "token_correspondence_Spec.Lib.op_At", "token_correspondence_Spec.Salsa20.quarter_round" ], 0 ], [ "Hacl.Impl.Salsa20.row_round", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.UInt32.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8" ], 0 ], [ "Hacl.Impl.Salsa20.row_round", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "equation_Spec.Lib.op_At", "equation_Spec.Salsa20.row_round", "equation_Spec.Salsa20.state", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "kinding_FStar.UInt32.t_@tok", "lemma_FStar.Buffer.lemma_modifies_1_trans", "lemma_FStar.Monotonic.HyperStack.lemma_equal_domains_trans", "proj_equation_FStar.UInt32.Mk_v", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.UInt32.Mk_v", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "token_correspondence_Spec.Lib.op_At", "token_correspondence_Spec.Salsa20.quarter_round" ], 0 ], [ "Hacl.Impl.Salsa20.double_round", 1, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.double_round", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.UInt32.t", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8" ], 0 ], [ "Hacl.Impl.Salsa20.double_round", 3, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.as_seq", "equation_FStar.UInt32.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Spec.Lib.op_At", "equation_Spec.Salsa20.double_round", "equation_Spec.Salsa20.state", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "kinding_FStar.UInt32.t_@tok", "lemma_FStar.Buffer.lemma_modifies_1_trans", "lemma_FStar.Monotonic.HyperStack.lemma_equal_domains_trans", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "token_correspondence_Spec.Salsa20.column_round", "token_correspondence_Spec.Salsa20.row_round" ], 0 ], [ "Hacl.Impl.Salsa20.rounds", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.UInt32.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8" ], 0 ], [ "Hacl.Impl.Salsa20.rounds", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion", "data_elim_FStar.UInt32.Mk", "eq2-interp", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.live", "equation_FStar.Monotonic.HyperHeap.t", "equation_FStar.Monotonic.HyperStack.hh", "equation_FStar.Monotonic.HyperStack.is_in", "equation_FStar.UInt.fits", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "equation_Prims.nat", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.rounds", "equation_Spec.Salsa20.state", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "function_token_typing_FStar.Monotonic.HyperHeap.root", "function_token_typing_Spec.Salsa20.constant0", "int_inversion", "interpretation_Hacl.Impl.Salsa20_Tm_abs_2e6873bdea443a1156756a9ef1c5ca10", "kinding_FStar.UInt32.t_@tok", "l_and-interp", "lemma_FStar.Buffer.lemma_modifies_1_trans", "lemma_FStar.Buffer.lemma_modifies_sub_1", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Monotonic.HyperStack.HS_h", "proj_equation_FStar.UInt32.Mk_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.UInt32.Mk_v", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_38d52172626ad62ce3b0e4245dab71ed", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_df782de28d42cc81ec07e4d442f8388e", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "typing_FStar.Monotonic.HyperStack.__proj__HS__item__h", "typing_FStar.Monotonic.HyperStack.is_in", "typing_FStar.UInt32.v" ], 0 ], [ "Hacl.Impl.Salsa20.sum_states", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Prims.nat", "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166" ], 0 ], [ "Hacl.Impl.Salsa20.sum_states", 2, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.UInt32.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd" ], 0 ], [ "Hacl.Impl.Salsa20.sum_states", 3, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.length", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "fuel_guarded_inversion_FStar.UInt32.t_", "kinding_FStar.UInt32.t_@tok", "proj_equation_FStar.Buffer.MkBuffer_length", "proj_equation_FStar.UInt32.Mk_v", "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd", "typing_FStar.Buffer.__proj__MkBuffer__item__length" ], 0 ], [ "Hacl.Impl.Salsa20.copy_state", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "eq2-interp", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.equal", "equation_FStar.Buffer.length", "equation_FStar.Buffer.live", "equation_FStar.Monotonic.HyperHeap.contains_ref", "equation_FStar.Monotonic.HyperHeap.test0", "equation_FStar.Monotonic.HyperStack.contains", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "equation_Prims._assert", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "fuel_guarded_inversion_FStar.UInt32.t_", "function_token_typing_FStar.Monotonic.HyperHeap.test0", "kinding_FStar.UInt32.t_@tok", "lemma_FStar.Buffer.lemma_disjoint_symm", "lemma_FStar.Buffer.no_upd_lemma_1", "lemma_FStar.Seq.Properties.slice_length", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "proj_equation_FStar.Buffer.MkBuffer_length", "proj_equation_FStar.UInt32.Mk_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.UInt32.Mk_v", "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.Buffer_Tm_refine_f9aa6ef37604d5d974d2a349d4f300e4", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd", "typing_FStar.Buffer.__proj__MkBuffer__item__length", "typing_FStar.Buffer.as_seq", "unit_inversion" ], 0 ], [ "Hacl.Impl.Salsa20.log_t_", 1, 0, 1, [ "@query", "assumption_FStar.Seq.Base.seq_haseq", "assumption_FStar.UInt8.t__haseq", "equation_FStar.UInt8.t", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen", "haseqFStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "kinding_FStar.UInt8.t_@tok" ], 0 ], [ "Hacl.Impl.Salsa20.__proj__MkLog__item__k", 1, 0, 1, [ "@query" ], 0 ], [ "Hacl.Impl.Salsa20.__proj__MkLog__item__n", 1, 0, 1, [ "@query" ], 0 ], [ "Hacl.Impl.Salsa20.u64_of_u32s", 1, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "data_elim_FStar.UInt32.Mk", "data_elim_FStar.UInt64.Mk", "data_elim_Spec.CTR.Mkblock_cipher_ctx", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.logor", "equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_left", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_Prims.nat", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_ctx", "fuel_guarded_inversion_FStar.UInt32.t_", "function_token_typing_FStar.UInt32.n", "function_token_typing_FStar.UInt64.n", "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion", "int_typing", "lemma_FStar.Buffer.lemma_size", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.UInt32.Mk_v", "projection_inverse_FStar.UInt64.Mk_v", "refinement_interpretation_FStar.Int.Cast_Tm_refine_c43881637fea8b5528f4439c75737f91", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "typing_FStar.Int.Cast.uint32_to_uint64" ], 0 ], [ "Hacl.Impl.Salsa20.u64_of_u32s", 2, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.low32_of_u64", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "data_elim_FStar.UInt64.Mk", "equation_FStar.UInt.fits", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "fuel_guarded_inversion_FStar.UInt64.t_", "int_inversion", "primitive_Prims.op_AmpAmp", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87" ], 0 ], [ "Hacl.Impl.Salsa20.low32_of_u64", 2, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.high32_of_u64", 1, 0, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "data_elim_FStar.UInt32.Mk", "data_elim_FStar.UInt64.Mk", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_right", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_Spec.Salsa20.constant2", "fuel_guarded_inversion_FStar.UInt64.t_", "function_token_typing_Spec.Salsa20.constant2", "int_inversion", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.UInt32.Mk_v", "projection_inverse_FStar.UInt64.Mk_v", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87" ], 0 ], [ "Hacl.Impl.Salsa20.high32_of_u64", 2, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.invariant", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.contains", "equation_FStar.Buffer.live", "equation_FStar.Monotonic.HyperHeap.contains_ref", "equation_FStar.Monotonic.HyperStack.contains", "equation_FStar.UInt32.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "primitive_Prims.op_AmpAmp", "proj_equation_FStar.Buffer.MkBuffer_content", "proj_equation_FStar.Monotonic.HyperStack.HS_h", "proj_equation_FStar.Monotonic.HyperStack.MkRef_id", "proj_equation_FStar.Monotonic.HyperStack.MkRef_ref", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_invariant", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.UInt32.t", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.low32_of_u64", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.state", "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok", "lemma_FStar.Seq.Base.lemma_len_upd", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Seq.Base_Tm_refine_2ca062977a42c36634b89c1c4f193f79", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_87a8b71348d8fdaab777237aed4f24d5", "refinement_interpretation_Spec.Salsa20_Tm_refine_aca10fb50cc7162d8b55c168416f714b", "typing_FStar.Seq.Base.length" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_invariant", 2, 0, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented", "@query", "Seq.Create_interpretation_Tm_arrow_5283c32b82bbd8c49fcb3c4afd352987", "data_elim_Spec.CTR.Mkblock_cipher_ctx", "data_typing_intro_FStar.UInt64.Mk@tok", "equation_FStar.UInt.shift_right", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_right", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.n", "equation_FStar.UInt8.t", "equation_Hacl.Cast.uint32_to_sint32", "equation_Hacl.Impl.Salsa20.high32_of_u64", "equation_Hacl.Impl.Salsa20.low32_of_u64", "equation_Hacl.Spec.Endianness.h64_to_u64", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant1", "equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.constant3", "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.setup", "equation_Spec.Salsa20.state", "function_token_typing_FStar.UInt64.n", "function_token_typing_FStar.UInt8.n", "function_token_typing_Seq.Create.create_16", "function_token_typing_Spec.Salsa20.constant0", "function_token_typing_Spec.Salsa20.constant1", "function_token_typing_Spec.Salsa20.constant2", "function_token_typing_Spec.Salsa20.constant3", "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion", "int_typing", "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_index_upd1", "lemma_FStar.Seq.Base.lemma_index_upd2", "lemma_FStar.Seq.Base.lemma_len_upd", "primitive_Prims.op_Multiply", "proj_equation_FStar.UInt32.Mk_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.UInt32.Mk_v", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f", "refinement_interpretation_FStar.Seq.Base_Tm_refine_2ca062977a42c36634b89c1c4f193f79", "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349", "refinement_interpretation_FStar.Seq.Base_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d", "refinement_interpretation_Hacl.Cast_Tm_refine_14dd5323a9a1a912dd915232f8c7d221", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ad73429f90f4e2d794c61307d038fc0f", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b", "refinement_interpretation_Seq.Create_Tm_refine_03488b8732f12d7416d4f57733783c65", "refinement_interpretation_Spec.Salsa20_Tm_refine_aca10fb50cc7162d8b55c168416f714b", "token_correspondence_Seq.Create.create_16", "typing_FStar.Int.Cast.uint64_to_uint32", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.shift_right", "typing_FStar.UInt64.v", "typing_Hacl.Impl.Salsa20.high32_of_u64", "typing_Hacl.Impl.Salsa20.low32_of_u64", "typing_Seq.Create.create_16", "typing_Spec.Lib.uint32s_from_le", "typing_Spec.Salsa20.setup" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_state_counter", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.t", "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.setup", "equation_Spec.Salsa20.state", "int_inversion", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Spec.Salsa20_Tm_refine_aca10fb50cc7162d8b55c168416f714b", "typing_Spec.Salsa20.setup" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_state_counter", 2, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "data_elim_Spec.CTR.Mkblock_cipher_ctx", "data_typing_intro_FStar.UInt32.Mk@tok", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.shift_right", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_right", "equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant1", "equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.constant3", "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.setup", "equation_Spec.Salsa20.state", "function_token_typing_FStar.UInt32.n", "function_token_typing_FStar.UInt64.n", "function_token_typing_Spec.Salsa20.constant0", "function_token_typing_Spec.Salsa20.constant1", "function_token_typing_Spec.Salsa20.constant2", "function_token_typing_Spec.Salsa20.constant3", "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion", "int_typing", "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok", "lemma_FStar.Buffer.lemma_size", "lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt.shift_right_value_lemma", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.UInt32.Mk_v", "projection_inverse_FStar.UInt64.Mk_v", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f", "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349", "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860", "refinement_interpretation_FStar.UInt64_Tm_refine_5c114bc17b55577083d2f1232d5b463f", "refinement_interpretation_FStar.UInt64_Tm_refine_b0d613e63865150efd1f73378fdc77ae", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b", "refinement_interpretation_Seq.Create_Tm_refine_03488b8732f12d7416d4f57733783c65", "refinement_interpretation_Spec.Salsa20_Tm_refine_aca10fb50cc7162d8b55c168416f714b", "typing_FStar.BitVector.shift_right_vec", "typing_FStar.Int.Cast.uint64_to_uint32", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt.from_vec", "typing_FStar.UInt.to_vec", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_FStar.UInt64.shift_right", "typing_FStar.UInt64.uint_to_t", "typing_Seq.Create.create_16", "typing_Spec.Lib.uint32s_from_le", "typing_Spec.Salsa20.setup", "unit_typing" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_u64_of_u32s", 1, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "data_elim_FStar.UInt32.Mk", "data_elim_Spec.CTR.Mkblock_cipher_ctx", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_right", "equation_FStar.UInt64.t", "equation_Hacl.Impl.Salsa20.high32_of_u64", "equation_Hacl.Impl.Salsa20.low32_of_u64", "equation_Hacl.Impl.Salsa20.u64_of_u32s", "equation_Prims.nat", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_ctx", "fuel_guarded_inversion_FStar.UInt32.t_", "function_token_typing_FStar.UInt32.n", "function_token_typing_Spec.Salsa20.constant2", "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion", "int_typing", "lemma_FStar.Buffer.lemma_size", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt32.Mk_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.UInt32.Mk_v", "refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f", "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860", "refinement_interpretation_FStar.UInt64_Tm_refine_2cdf10a0b17b1e313a0b7d29add2d0a1", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_38ba181c174bc0df2d51f0fb09d5a895", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ad73429f90f4e2d794c61307d038fc0f", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "typing_FStar.Int.Cast.uint64_to_uint32", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt64.shift_right", "typing_FStar.UInt64.v", "typing_Hacl.Impl.Salsa20.high32_of_u64", "typing_Hacl.Impl.Salsa20.low32_of_u64", "typing_Hacl.Impl.Salsa20.u64_of_u32s" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_u64_of_u32s", 2, 0, 1, [ "@query", "assumption_FStar.UInt32.t__haseq", "equation_FStar.UInt32.t" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_u64_of_u32s", 3, 0, 1, [ "@query", "assumption_FStar.UInt32.t__haseq", "equation_FStar.UInt32.t" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_u64_of_u32s", 4, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_u64_of_u32s", 5, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n", "haseqFStar.UInt_Tm_refine_81528fa45830671a34dc41538a864b77", "projection_inverse_BoxInt_proj_0" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_core", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.UInt32.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.invariant", "equation_Hacl.Impl.Salsa20.state", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_512d2e36eceaae5937ab1ff1eef964fd", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_core", 2, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "FStar.UInt32_interpretation_Tm_arrow_15569832cb7b48ce3fe999c98911dd3f", "Hacl.Impl.Salsa20_pretyping_a87e903bbc455531fa4b8b47a243ed22", "b2t_def", "bool_inversion", "bool_typing", "data_elim_FStar.UInt32.Mk", "data_elim_FStar.UInt64.Mk", "data_elim_Hacl.Impl.Salsa20.MkLog", "data_elim_Spec.CTR.Mkblock_cipher_ctx", "eq2-interp", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.equal", "equation_FStar.Buffer.get", "equation_FStar.Buffer.live", "equation_FStar.Monotonic.HyperHeap.contains_ref", "equation_FStar.Monotonic.HyperStack.contains", "equation_FStar.UInt.fits", "equation_FStar.UInt.logor", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.shift_right", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.logor", "equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_left", "equation_FStar.UInt64.shift_right", "equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.n", "equation_FStar.UInt8.t", "equation_Hacl.Cast.uint32_to_sint32", "equation_Hacl.Cast.uint64_to_sint64", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.high32_of_u64", "equation_Hacl.Impl.Salsa20.invariant", "equation_Hacl.Impl.Salsa20.log_t", "equation_Hacl.Impl.Salsa20.low32_of_u64", "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.Impl.Salsa20.u64_of_u32s", "equation_Hacl.Spec.Endianness.h32_to_u32", "equation_Hacl.Spec.Endianness.h64_to_u64", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_core", "equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.setup", "equation_Spec.Salsa20.state", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.UInt32.t_", "fuel_guarded_inversion_FStar.UInt64.t_", "fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_", "function_token_typing_FStar.UInt32.n", "function_token_typing_FStar.UInt64.n", "function_token_typing_FStar.UInt64.v", "function_token_typing_FStar.UInt8.n", "function_token_typing_Spec.Salsa20.constant2", "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion", "int_typing", "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok", "kinding_Hacl.Impl.Salsa20.log_t_@tok", "lemma_FStar.Buffer.lemma_disjoint_symm", "lemma_FStar.Buffer.lemma_modifies_1_1", "lemma_FStar.Buffer.lemma_modifies_1_trans", "lemma_FStar.Buffer.lemma_modifies_2_1", "lemma_FStar.Buffer.no_upd_lemma_1", "lemma_FStar.Buffer.no_upd_lemma_2", "lemma_FStar.Monotonic.HyperStack.lemma_equal_domains_trans", "lemma_FStar.Seq.Base.lemma_index_upd1", "lemma_FStar.Seq.Base.lemma_index_upd2", "lemma_FStar.UInt.shift_right_value_lemma", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual", "proj_equation_FStar.Monotonic.HyperStack.HS_h", "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v", "proj_equation_Hacl.Impl.Salsa20.MkLog_k", "proj_equation_Hacl.Impl.Salsa20.MkLog_n", "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.UInt32.Mk_v", "projection_inverse_FStar.UInt64.Mk_v", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f", "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349", "refinement_interpretation_FStar.Seq.Base_Tm_refine_b5ad1dbfbd48faaf34d92bafda76205d", "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860", "refinement_interpretation_FStar.UInt64_Tm_refine_5c114bc17b55577083d2f1232d5b463f", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_38ba181c174bc0df2d51f0fb09d5a895", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_512d2e36eceaae5937ab1ff1eef964fd", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ad73429f90f4e2d794c61307d038fc0f", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_c183f792a86570f8cbdc987c371a7442", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e008bc85a6406729442060d7942e9ff0", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b", "refinement_interpretation_Spec.Salsa20_Tm_refine_aca10fb50cc7162d8b55c168416f714b", "token_correspondence_FStar.UInt64.v", "typing_FStar.Buffer.as_seq", "typing_FStar.Ghost.reveal", "typing_FStar.Seq.Base.length", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt64.shift_right", "typing_Hacl.Impl.Salsa20.high32_of_u64", "typing_Hacl.Impl.Salsa20.low32_of_u64", "typing_Hacl.Impl.Salsa20.u64_of_u32s" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_block", 1, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_block", 2, 0, 1, [ "@query" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_block", 3, 0, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented", "@query", "Hacl.Impl.Salsa20_pretyping_a87e903bbc455531fa4b8b47a243ed22", "assumption_FStar.Monotonic.HyperHeap.HasEq_rid", "b2t_def", "bool_inversion", "bool_typing", "data_elim_FStar.Monotonic.HyperStack.MkRef", "data_elim_FStar.UInt32.Mk", "data_elim_FStar.UInt64.Mk", "data_elim_Hacl.Impl.Salsa20.MkLog", "data_elim_Spec.CTR.Mkblock_cipher_ctx", "eq2-interp", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.content", "equation_FStar.Buffer.equal", "equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.length", "equation_FStar.Buffer.live", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.HyperStack.reference", "equation_FStar.Monotonic.HyperHeap.t", "equation_FStar.Monotonic.HyperStack.contains", "equation_FStar.Monotonic.HyperStack.equal_domains", "equation_FStar.Monotonic.HyperStack.frameOf", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.hh", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.live_region", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_FStar.Set.eqtype", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.logor", "equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_right", "equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.high32_of_u64", "equation_Hacl.Impl.Salsa20.invariant", "equation_Hacl.Impl.Salsa20.log_t", "equation_Hacl.Impl.Salsa20.low32_of_u64", "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.Impl.Salsa20.u64_of_u32s", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.Spec.Endianness.h32_to_u32", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant1", "equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.constant3", "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_block", "equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.setup", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference", "fuel_guarded_inversion_FStar.UInt32.t_", "fuel_guarded_inversion_FStar.UInt64.t_", "fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_", "function_token_typing_FStar.Monotonic.Heap.emp", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_FStar.Monotonic.HyperHeap.rid", "function_token_typing_FStar.UInt32.n", "function_token_typing_Spec.Salsa20.constant0", "function_token_typing_Spec.Salsa20.constant1", "function_token_typing_Spec.Salsa20.constant2", "function_token_typing_Spec.Salsa20.constant3", "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion", "int_typing", "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok", "kinding_Hacl.Impl.Salsa20.log_t_@tok", "lemma_FStar.Buffer.lemma_disjoint_symm", "lemma_FStar.Buffer.lemma_equal_domains_2", "lemma_FStar.Buffer.lemma_fresh_poppable", "lemma_FStar.Buffer.lemma_live_disjoint", "lemma_FStar.Buffer.lemma_modifies_0_2_", "lemma_FStar.Buffer.lemma_modifies_2_1__", "lemma_FStar.Buffer.lemma_modifies_3_2_comm", "lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped", "lemma_FStar.Buffer.modifies_poppable_0", "lemma_FStar.Buffer.modifies_poppable_1", "lemma_FStar.Buffer.modifies_poppable_2", "lemma_FStar.Buffer.modifies_popped_3_2", "lemma_FStar.Buffer.no_upd_fresh", "lemma_FStar.Buffer.no_upd_lemma_0", "lemma_FStar.Buffer.no_upd_lemma_1", "lemma_FStar.Buffer.no_upd_lemma_2", "lemma_FStar.Buffer.no_upd_popped", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Monotonic.HyperStack.lemma_equal_domains_trans", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_disEquality", "proj_equation_FStar.Buffer.MkBuffer_content", "proj_equation_FStar.Monotonic.HyperStack.HS_h", "proj_equation_FStar.Monotonic.HyperStack.MkRef_id", "proj_equation_FStar.Monotonic.HyperStack.MkRef_ref", "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v", "proj_equation_Hacl.Impl.Salsa20.MkLog_k", "proj_equation_Hacl.Impl.Salsa20.MkLog_n", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Monotonic.HyperStack.HS_h", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.UInt32.Mk_v", "projection_inverse_FStar.UInt64.Mk_v", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_38d52172626ad62ce3b0e4245dab71ed", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_b05295ea25e1fbfe5a4bd48cb81ddfff", "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349", "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860", "refinement_interpretation_FStar.UInt64_Tm_refine_5c114bc17b55577083d2f1232d5b463f", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_38ba181c174bc0df2d51f0fb09d5a895", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_401c6dceec5f7ff8e777e09ee5a25c1c", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_7b8277f4aac7937ca94306760a67d045", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ad73429f90f4e2d794c61307d038fc0f", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b", "refinement_interpretation_Seq.Create_Tm_refine_03488b8732f12d7416d4f57733783c65", "typing_FStar.Buffer.__proj__MkBuffer__item__content", "typing_FStar.Buffer.frameOf", "typing_FStar.Buffer.length", "typing_FStar.Ghost.reveal", "typing_FStar.Int.Cast.uint64_to_uint32", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.HyperStack.__proj__HS__item__h", "typing_FStar.Monotonic.HyperStack.__proj__HS__item__tip", "typing_FStar.Monotonic.HyperStack.poppable", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length", "typing_FStar.Set.complement", "typing_FStar.Set.singleton", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt64.shift_right", "typing_Hacl.Impl.Salsa20.high32_of_u64", "typing_Hacl.Impl.Salsa20.low32_of_u64", "typing_Hacl.Impl.Salsa20.u64_of_u32s", "typing_Seq.Create.create_16", "typing_Spec.Lib.uint32s_from_le" ], 0 ], [ "Hacl.Impl.Salsa20.alloc", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.unmapped_in", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "proj_equation_FStar.UInt32.Mk_v", "projection_inverse_FStar.UInt32.Mk_v", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8" ], 0 ], [ "Hacl.Impl.Salsa20.init", 1, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.init", 2, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.init", 3, 0, 1, [ "@query" ], 0 ], [ "Hacl.Impl.Salsa20.init", 4, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented", "@query", "Seq.Create_interpretation_Tm_arrow_5283c32b82bbd8c49fcb3c4afd352987", "b2t_def", "data_elim_Spec.CTR.Mkblock_cipher_ctx", "eq2-interp", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.equal", "equation_FStar.Buffer.length", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_right", "equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.invariant", "equation_Hacl.Impl.Salsa20.log_t", "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.Impl.Salsa20.u64_of_u32s", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.Spec.Endianness.h32_to_u32", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant1", "equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.constant3", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.setup", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.UInt32.t_", "function_token_typing_FStar.UInt64.n", "function_token_typing_Seq.Create.create_16", "function_token_typing_Spec.Salsa20.constant0", "function_token_typing_Spec.Salsa20.constant1", "function_token_typing_Spec.Salsa20.constant2", "function_token_typing_Spec.Salsa20.constant3", "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion", "int_typing", "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok", "lemma_FStar.Buffer.no_upd_lemma_1", "lemma_FStar.Ghost.hide_reveal", "lemma_FStar.Ghost.reveal_hide", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Buffer.MkBuffer_length", "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.UInt32.Mk_v", "projection_inverse_FStar.UInt64.Mk_v", "projection_inverse_Hacl.Impl.Salsa20.MkLog_k", "projection_inverse_Hacl.Impl.Salsa20.MkLog_n", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f", "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349", "refinement_interpretation_FStar.UInt64_Tm_refine_5c114bc17b55577083d2f1232d5b463f", "refinement_interpretation_FStar.UInt64_Tm_refine_b0d613e63865150efd1f73378fdc77ae", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_34c713272d4138e534ee70be89b06637", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_38ba181c174bc0df2d51f0fb09d5a895", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_59174d15900b1aac0e68774108209b07", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_6aa1ec763d1c295e2e04032d3f087688", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_a4c77d45897f44b25f77ea93cf941da6", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_f1bff5a109be7d28c81090d4cf9894b0", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b", "refinement_interpretation_Seq.Create_Tm_refine_03488b8732f12d7416d4f57733783c65", "refinement_kinding_Hacl.Impl.Salsa20_Tm_refine_a4c77d45897f44b25f77ea93cf941da6", "refinement_kinding_Hacl.Impl.Salsa20_Tm_refine_f1bff5a109be7d28c81090d4cf9894b0", "token_correspondence_Seq.Create.create_16", "typing_FStar.Buffer.__proj__MkBuffer__item__length", "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length", "typing_FStar.Ghost.hide", "typing_FStar.Int.Cast.uint64_to_uint32", "typing_FStar.Seq.Base.index", "typing_FStar.UInt64.shift_right", "typing_FStar.UInt64.uint_to_t", "typing_Hacl.Impl.Salsa20.u64_of_u32s", "typing_Prims.pow2", "typing_Spec.Lib.uint32s_from_le" ], 0 ], [ "Hacl.Impl.Salsa20.init", 5, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.init", 6, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.init", 7, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.init", 8, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.init", 9, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.init", 10, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1", 1, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n", "haseqHacl.Impl.Salsa20_Tm_refine_530be526726c3b66223dd819f9d65058", "projection_inverse_BoxInt_proj_0" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1", 2, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n", "haseqHacl.Impl.Salsa20_Tm_refine_530be526726c3b66223dd819f9d65058", "projection_inverse_BoxInt_proj_0" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1", 3, 0, 1, [ "@MaxIFuel_assumption", "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.t", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat", "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d287bdb5105268f1b0702cd0a5b01379" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1", 4, 0, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "data_elim_FStar.UInt32.Mk", "equation_FStar.Buffer.buffer", "equation_FStar.UInt.fits", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.block", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_block", "equation_Spec.Salsa20.salsa20_ctx", "fuel_guarded_inversion_FStar.Buffer._buffer", "function_token_typing_Spec.Salsa20.constant0", "int_inversion", "int_typing", "kinding_FStar.UInt8.t_@tok", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d287bdb5105268f1b0702cd0a5b01379", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "typing_FStar.Buffer.length", "typing_FStar.UInt64.v", "typing_Spec.Salsa20.salsa20_block" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1", 5, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_correspondence_Spec.CTR.counter_mode_blocks.fuel_instrumented", "@query", "Spec.CTR_interpretation_Tm_arrow_8c1eb20ec87e56ca23946ea5f24a1c2a", "b2t_def", "bool_inversion", "equation_FStar.Buffer.buffer", "equation_FStar.Seq.Base.op_At_Bar", "equation_FStar.Seq.Properties.split", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat", "equation_Spec.CTR.block", "equation_Spec.CTR.block_cipher", "equation_Spec.CTR.counter", "equation_Spec.CTR.counter_mode", "equation_Spec.CTR.key", "equation_Spec.CTR.nonce", "equation_Spec.CTR.xor", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.block", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_block", "equation_Spec.Salsa20.salsa20_cipher", "equation_Spec.Salsa20.salsa20_ctx", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "fuel_guarded_inversion_FStar.UInt64.t_", "function_token_typing_Spec.Salsa20.salsa20_cipher", "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion", "int_typing", "kinding_FStar.UInt8.t_@tok", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen", "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_Spec.CTR.Mkblock_cipher_ctx_blocklen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.Seq.Base_Tm_refine_03127b5d59ee3055620018693b4264e8", "refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9", "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349", "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68", "refinement_interpretation_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_FStar.Seq.Base_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_81037de341b1e2ded11074428c6d80d7", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_9faf2d7f785796ced455a352d9a5c100", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d287bdb5105268f1b0702cd0a5b01379", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b", "token_correspondence_Spec.Salsa20.salsa20_block", "typing_FStar.Seq.Base.createEmpty", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "typing_Spec.CTR.__proj__Mkblock_cipher_ctx__item__blocklen", "typing_Spec.Salsa20.salsa20_block" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1", 6, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1", 7, 0, 1, [ "@MaxIFuel_assumption", "@query", "assumption_Prims.HasEq_int", "equation_FStar.Buffer.buffer", "equation_FStar.UInt32.t", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat", "fuel_guarded_inversion_FStar.Buffer._buffer", "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d287bdb5105268f1b0702cd0a5b01379" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1", 8, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_2", 1, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n", "haseqHacl.Impl.Salsa20_Tm_refine_530be526726c3b66223dd819f9d65058", "projection_inverse_BoxInt_proj_0" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_2", 2, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n", "haseqHacl.Impl.Salsa20_Tm_refine_530be526726c3b66223dd819f9d65058", "projection_inverse_BoxInt_proj_0" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_2", 3, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_2", 4, 0, 1, [ "@query", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_ctx", "primitive_Prims.op_Multiply", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_2", 5, 0, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "data_elim_FStar.Monotonic.HyperStack.MkRef", "data_elim_FStar.UInt32.Mk", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.idx", "equation_FStar.Buffer.length", "equation_FStar.Buffer.sel", "equation_FStar.HyperStack.reference", "equation_FStar.Seq.Properties.split", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_ctx", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference", "fuel_guarded_inversion_FStar.UInt64.t_", "function_token_typing_Spec.Salsa20.constant0", "int_inversion", "int_typing", "kinding_FStar.UInt8.t_@tok", "lemma_FStar.Buffer.lemma_size", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Buffer.MkBuffer_content", "proj_equation_FStar.Buffer.MkBuffer_length", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen", "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_Spec.CTR.Mkblock_cipher_ctx_blocklen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen", "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d", "refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9", "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68", "refinement_interpretation_FStar.Seq.Properties_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_4d5f76b1705708752e4f3bb8d5a207ec", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ac03c6b5bfee50cc2664154412b8d06c", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "refinement_kinding_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d", "typing_FStar.Buffer.__proj__MkBuffer__item__content", "typing_FStar.Buffer.__proj__MkBuffer__item__idx", "typing_FStar.Buffer.__proj__MkBuffer__item__length", "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.idx", "typing_FStar.Buffer.length", "typing_FStar.Monotonic.HyperStack.sel", "typing_FStar.UInt32.v", "typing_FStar.UInt64.v" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_2", 6, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_correspondence_Spec.CTR.counter_mode_blocks.fuel_instrumented", "@fuel_irrelevance_Spec.CTR.counter_mode_blocks.fuel_instrumented", "@query", "Spec.CTR_interpretation_Tm_arrow_8c1eb20ec87e56ca23946ea5f24a1c2a", "b2t_def", "bool_inversion", "bool_typing", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.Seq.Base.op_At_Bar", "equation_FStar.Seq.Properties.split", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat", "equation_Spec.CTR.block", "equation_Spec.CTR.block_cipher", "equation_Spec.CTR.counter", "equation_Spec.CTR.key", "equation_Spec.CTR.nonce", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.block", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_cipher", "equation_Spec.Salsa20.salsa20_ctx", "equation_with_fuel_Spec.CTR.counter_mode_blocks.fuel_instrumented", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "function_token_typing_Spec.Salsa20.salsa20_cipher", "int_typing", "kinding_FStar.UInt8.t_@tok", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen", "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_Spec.CTR.Mkblock_cipher_ctx_blocklen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_4d5f76b1705708752e4f3bb8d5a207ec", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "token_correspondence_Spec.Salsa20.salsa20_block", "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length", "typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits", "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "typing_Spec.Salsa20.salsa20_block", "unit_typing" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_0", 1, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n", "haseqHacl.Impl.Salsa20_Tm_refine_530be526726c3b66223dd819f9d65058", "projection_inverse_BoxInt_proj_0" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_0", 2, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n", "haseqHacl.Impl.Salsa20_Tm_refine_530be526726c3b66223dd819f9d65058", "projection_inverse_BoxInt_proj_0" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_0", 3, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_0", 4, 0, 1, [ "@MaxIFuel_assumption", "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat", "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_0", 5, 0, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "data_elim_FStar.UInt32.Mk", "equation_FStar.Buffer.buffer", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_ctx", "fuel_guarded_inversion_FStar.Buffer._buffer", "function_token_typing_Spec.Salsa20.constant0", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_241d61c8ad097706dd0ca2556ca9bdf1", "typing_FStar.UInt64.v" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_0", 6, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Spec.CTR.counter_mode_blocks.fuel_instrumented", "@query", "b2t_def", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.UInt.fits", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat", "equation_Spec.Salsa20.salsa20_cipher", "equation_Spec.Salsa20.salsa20_ctx", "equation_with_fuel_Spec.CTR.counter_mode_blocks.fuel_instrumented", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "kinding_FStar.UInt8.t_@tok", "primitive_Prims.op_Equality", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_241d61c8ad097706dd0ca2556ca9bdf1", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_75fe8a65f5666eaf920693fe19efc919", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "typing_FStar.Buffer.as_seq", "typing_FStar.Seq.Base.createEmpty", "typing_FStar.UInt32.v" ], 0 ], [ "Hacl.Impl.Salsa20.update_last", 1, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n", "haseqHacl.Impl.Salsa20_Tm_refine_530be526726c3b66223dd819f9d65058", "projection_inverse_BoxInt_proj_0" ], 0 ], [ "Hacl.Impl.Salsa20.update_last", 2, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n", "haseqHacl.Impl.Salsa20_Tm_refine_530be526726c3b66223dd819f9d65058", "projection_inverse_BoxInt_proj_0" ], 0 ], [ "Hacl.Impl.Salsa20.update_last", 3, 0, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "data_elim_FStar.UInt32.Mk", "data_elim_Hacl.Impl.Salsa20.MkLog", "equation_FStar.Buffer.length", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.log_t", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat", "equation_Spec.CTR.block", "equation_Spec.CTR.counter", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.block", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_cipher", "equation_Spec.Salsa20.salsa20_ctx", "fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_", "function_token_typing_Spec.Salsa20.constant0", "int_inversion", "int_typing", "kinding_FStar.UInt8.t_@tok", "kinding_Hacl.Impl.Salsa20.log_t_@tok", "lemma_FStar.Seq.Base.lemma_len_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349", "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_cdd15a61a8a8f4424284702869adc760", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d287bdb5105268f1b0702cd0a5b01379", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "token_correspondence_Spec.Salsa20.salsa20_block", "typing_FStar.Buffer.length", "typing_FStar.Ghost.reveal", "typing_FStar.UInt64.v", "typing_Spec.Lib.uint32s_from_le", "typing_Spec.Salsa20.salsa20_block" ], 0 ], [ "Hacl.Impl.Salsa20.update_last", 4, 0, 1, [ "@MaxIFuel_assumption", "@query", "FStar.Map_interpretation_Tm_arrow_d02b23aab265d753a600adf301de862a", "Hacl.Impl.Salsa20_pretyping_a87e903bbc455531fa4b8b47a243ed22", "Spec.CTR_interpretation_Tm_arrow_8c1eb20ec87e56ca23946ea5f24a1c2a", "assumption_FStar.Monotonic.HyperHeap.HasEq_rid", "bool_inversion", "data_elim_FStar.Buffer.MkBuffer", "data_elim_FStar.Monotonic.HyperStack.HS", "data_elim_FStar.Monotonic.HyperStack.MkRef", "eq2-interp", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.content", "equation_FStar.Buffer.equal", "equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.idx", "equation_FStar.Buffer.includes", "equation_FStar.Buffer.length", "equation_FStar.Buffer.live", "equation_FStar.Buffer.sel", "equation_FStar.Buffer.sub", "equation_FStar.Buffer.unused_in", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.HyperStack.reference", "equation_FStar.Monotonic.HyperHeap.t", "equation_FStar.Monotonic.HyperStack.contains", "equation_FStar.Monotonic.HyperStack.equal_domains", "equation_FStar.Monotonic.HyperStack.frameOf", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.hh", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.live_region", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_FStar.Set.eqtype", "equation_FStar.UInt.add", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.add", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.invariant", "equation_Hacl.Impl.Salsa20.log_t", "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.eqtype", "equation_Prims.nat", "equation_Spec.CTR.block", "equation_Spec.CTR.block_cipher", "equation_Spec.CTR.counter", "equation_Spec.CTR.key", "equation_Spec.CTR.nonce", "equation_Spec.CTR.xor", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_block", "equation_Spec.Salsa20.salsa20_cipher", "equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.setup", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference", "fuel_guarded_inversion_FStar.UInt32.t_", "function_token_typing_FStar.Map.domain", "function_token_typing_FStar.Monotonic.Heap.emp", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_FStar.Monotonic.HyperHeap.rid", "function_token_typing_FStar.UInt64.n", "function_token_typing_Spec.Salsa20.salsa20_cipher", "int_inversion", "int_typing", "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok", "kinding_Hacl.Impl.Salsa20.log_t_@tok", "lemma_FStar.Buffer.lemma_disjoint_symm", "lemma_FStar.Buffer.lemma_equal_domains_2", "lemma_FStar.Buffer.lemma_fresh_poppable", "lemma_FStar.Buffer.lemma_live_disjoint", "lemma_FStar.Buffer.lemma_modifies_0_2_", "lemma_FStar.Buffer.lemma_modifies_2_1__", "lemma_FStar.Buffer.lemma_modifies_3_2_comm", "lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped", "lemma_FStar.Buffer.modifies_poppable_1", "lemma_FStar.Buffer.modifies_popped_3_2", "lemma_FStar.Buffer.no_upd_fresh", "lemma_FStar.Buffer.no_upd_lemma_0", "lemma_FStar.Buffer.no_upd_lemma_1", "lemma_FStar.Buffer.no_upd_lemma_2_1", "lemma_FStar.Buffer.no_upd_popped", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Monotonic.HyperStack.lemma_equal_domains_trans", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_slice", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Negation", "primitive_Prims.op_disEquality", "proj_equation_FStar.Buffer.MkBuffer_content", "proj_equation_FStar.Buffer.MkBuffer_idx", "proj_equation_FStar.Buffer.MkBuffer_length", "proj_equation_FStar.Buffer.MkBuffer_max_length", "proj_equation_FStar.Monotonic.HyperStack.HS_h", "proj_equation_FStar.Monotonic.HyperStack.HS_tip", "proj_equation_FStar.Monotonic.HyperStack.MkRef_id", "proj_equation_FStar.Monotonic.HyperStack.MkRef_ref", "proj_equation_FStar.UInt32.Mk_v", "proj_equation_Hacl.Impl.Salsa20.MkLog_k", "proj_equation_Hacl.Impl.Salsa20.MkLog_n", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Buffer.MkBuffer_idx", "projection_inverse_FStar.Monotonic.HyperStack.HS_h", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.UInt32.Mk_v", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9", "refinement_interpretation_FStar.Buffer_Tm_refine_8518e8b728e19b2937c780d25ff7abcb", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.Buffer_Tm_refine_ba20691c598b7aba0d11d91ead0d6da1", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_0418702750d54a72833a38f310956e3d", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_38d52172626ad62ce3b0e4245dab71ed", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_b05295ea25e1fbfe5a4bd48cb81ddfff", "refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9", "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68", "refinement_interpretation_FStar.Seq.Properties_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_82db053939908f699a97088907080433", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d287bdb5105268f1b0702cd0a5b01379", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd", "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "refinement_kinding_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d", "token_correspondence_FStar.Map.domain", "token_correspondence_Spec.Salsa20.salsa20_block", "typing_FStar.Buffer.__proj__MkBuffer__item__content", "typing_FStar.Buffer.__proj__MkBuffer__item__length", "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.content", "typing_FStar.Buffer.idx", "typing_FStar.Buffer.length", "typing_FStar.Buffer.sel", "typing_FStar.Ghost.reveal", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.HyperStack.__proj__HS__item__h", "typing_FStar.Monotonic.HyperStack.__proj__HS__item__tip", "typing_FStar.Monotonic.HyperStack.poppable", "typing_FStar.Monotonic.HyperStack.remove_elt", "typing_FStar.Monotonic.HyperStack.sel", "typing_FStar.Set.complement", "typing_FStar.Set.intersect", "typing_FStar.Set.singleton", "typing_FStar.UInt64.v" ], 0 ], [ "Hacl.Impl.Salsa20.update", 1, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.update", 2, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.update", 3, 0, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "data_elim_FStar.UInt32.Mk", "equation_FStar.UInt.fits", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.block", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.counter", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_cipher", "equation_Spec.Salsa20.salsa20_ctx", "function_token_typing_Spec.Salsa20.constant0", "primitive_Prims.op_AmpAmp", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen", "projection_inverse_BoxBool_proj_0", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_1d668d298fe099f2dd7e1e24c538b64a", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ce01e3cba2a2fbf2c025b891a51ea08e", "token_correspondence_Spec.Salsa20.salsa20_block", "typing_FStar.UInt64.v", "typing_Spec.Salsa20.salsa20_block" ], 0 ], [ "Hacl.Impl.Salsa20.update", 4, 0, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented", "@query", "Hacl.Impl.Salsa20_pretyping_a87e903bbc455531fa4b8b47a243ed22", "assumption_FStar.Monotonic.HyperHeap.HasEq_rid", "bool_inversion", "data_elim_FStar.Buffer.MkBuffer", "data_elim_FStar.Monotonic.HyperStack.HS", "data_elim_FStar.Monotonic.HyperStack.MkRef", "data_elim_Hacl.Impl.Salsa20.MkLog", "data_elim_Spec.CTR.Mkblock_cipher_ctx", "eq2-interp", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.content", "equation_FStar.Buffer.disjoint", "equation_FStar.Buffer.equal", "equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.idx", "equation_FStar.Buffer.includes", "equation_FStar.Buffer.length", "equation_FStar.Buffer.live", "equation_FStar.Buffer.sub", "equation_FStar.Buffer.unused_in", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.HyperStack.reference", "equation_FStar.Monotonic.HyperHeap.t", "equation_FStar.Monotonic.HyperStack.contains", "equation_FStar.Monotonic.HyperStack.equal_domains", "equation_FStar.Monotonic.HyperStack.frameOf", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.hh", "equation_FStar.Monotonic.HyperStack.is_in", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.live_region", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Set.eqtype", "equation_FStar.UInt.add", "equation_FStar.UInt32.add", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.logor", "equation_FStar.UInt64.n", "equation_FStar.UInt64.shift_right", "equation_FStar.UInt64.t", "equation_FStar.UInt64.uint_to_t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.high32_of_u64", "equation_Hacl.Impl.Salsa20.invariant", "equation_Hacl.Impl.Salsa20.log_t", "equation_Hacl.Impl.Salsa20.low32_of_u64", "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.Impl.Salsa20.u64_of_u32s", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.Impl.Xor.Lemmas.u32", "equation_Hacl.Spec.Endianness.h32_to_u32", "equation_Prims.nat", "equation_Prims.pos", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant1", "equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.constant3", "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.nonce", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_block", "equation_Spec.Salsa20.salsa20_cipher", "equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.setup", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference", "fuel_guarded_inversion_FStar.UInt32.t_", "fuel_guarded_inversion_FStar.UInt64.t_", "fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_FStar.Monotonic.HyperHeap.rid", "function_token_typing_Spec.Salsa20.constant0", "function_token_typing_Spec.Salsa20.constant1", "function_token_typing_Spec.Salsa20.constant2", "function_token_typing_Spec.Salsa20.constant3", "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_typing", "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok", "kinding_Hacl.Impl.Salsa20.log_t_@tok", "lemma_FStar.Buffer.lemma_disjoint_sub", "lemma_FStar.Buffer.lemma_disjoint_sub_", "lemma_FStar.Buffer.lemma_disjoint_symm", "lemma_FStar.Buffer.lemma_equal_domains_2", "lemma_FStar.Buffer.lemma_fresh_poppable", "lemma_FStar.Buffer.lemma_live_disjoint", "lemma_FStar.Buffer.lemma_modifies_0_2", "lemma_FStar.Buffer.lemma_modifies_1_1", "lemma_FStar.Buffer.lemma_modifies_1_trans", "lemma_FStar.Buffer.lemma_modifies_2_1_", "lemma_FStar.Buffer.lemma_modifies_2_1__", "lemma_FStar.Buffer.lemma_modifies_3_2_comm", "lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped", "lemma_FStar.Buffer.modifies_poppable_1", "lemma_FStar.Buffer.modifies_popped_3_2", "lemma_FStar.Buffer.modifies_subbuffer_1", "lemma_FStar.Buffer.modifies_subbuffer_2", "lemma_FStar.Buffer.no_upd_fresh", "lemma_FStar.Buffer.no_upd_lemma_0", "lemma_FStar.Buffer.no_upd_lemma_1", "lemma_FStar.Buffer.no_upd_lemma_2", "lemma_FStar.Buffer.no_upd_lemma_2_1", "lemma_FStar.Buffer.no_upd_popped", "lemma_FStar.Ghost.hide_reveal", "lemma_FStar.Monotonic.HyperStack.lemma_equal_domains_trans", "primitive_Prims.op_Addition", "primitive_Prims.op_Multiply", "primitive_Prims.op_disEquality", "proj_equation_FStar.Buffer.MkBuffer_content", "proj_equation_FStar.Buffer.MkBuffer_idx", "proj_equation_FStar.Buffer.MkBuffer_length", "proj_equation_FStar.Buffer.MkBuffer_max_length", "proj_equation_FStar.Monotonic.HyperStack.HS_h", "proj_equation_FStar.Monotonic.HyperStack.HS_tip", "proj_equation_FStar.Monotonic.HyperStack.MkRef_id", "proj_equation_FStar.Monotonic.HyperStack.MkRef_ref", "proj_equation_FStar.UInt32.Mk_v", "proj_equation_FStar.UInt64.Mk_v", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Buffer.MkBuffer_idx", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.UInt32.Mk_v", "projection_inverse_FStar.UInt64.Mk_v", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_0418702750d54a72833a38f310956e3d", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_38d52172626ad62ce3b0e4245dab71ed", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_b05295ea25e1fbfe5a4bd48cb81ddfff", "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349", "refinement_interpretation_FStar.UInt64_Tm_refine_5c114bc17b55577083d2f1232d5b463f", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_1d668d298fe099f2dd7e1e24c538b64a", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_38ba181c174bc0df2d51f0fb09d5a895", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_7b8277f4aac7937ca94306760a67d045", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_82db053939908f699a97088907080433", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_a020878d088ac42f674702039e62fe9b", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ad73429f90f4e2d794c61307d038fc0f", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ce01e3cba2a2fbf2c025b891a51ea08e", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b", "refinement_interpretation_Seq.Create_Tm_refine_03488b8732f12d7416d4f57733783c65", "token_correspondence_Spec.Salsa20.salsa20_block", "typing_FStar.Buffer.__proj__MkBuffer__item__content", "typing_FStar.Buffer.__proj__MkBuffer__item__idx", "typing_FStar.Buffer.__proj__MkBuffer__item__length", "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.content", "typing_FStar.Ghost.reveal", "typing_FStar.Int.Cast.uint64_to_uint32", "typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperStack.__proj__HS__item__h", "typing_FStar.Monotonic.HyperStack.__proj__HS__item__tip", "typing_FStar.Monotonic.HyperStack.poppable", "typing_FStar.Seq.Base.index", "typing_FStar.UInt64.shift_right", "typing_Hacl.Impl.Salsa20.high32_of_u64", "typing_Hacl.Impl.Salsa20.low32_of_u64", "typing_Hacl.Impl.Salsa20.u64_of_u32s", "typing_Seq.Create.create_16", "typing_Spec.Lib.uint32s_from_le" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_aux_modifies_2", 1, 0, 1, [ "@MaxIFuel_assumption", "@query", "assumption_FStar.Monotonic.HyperHeap.HasEq_rid", "bool_inversion", "data_elim_FStar.Monotonic.HyperStack.MkRef", "eq2-interp", "equation_FStar.Buffer.as_addr", "equation_FStar.Buffer.as_ref", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.content", "equation_FStar.Buffer.disjoint", "equation_FStar.Buffer.equal", "equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.live", "equation_FStar.Buffer.modifies_buf_1", "equation_FStar.Buffer.modifies_buf_2", "equation_FStar.Buffer.to_set_2", "equation_FStar.Buffer.unused_in", "equation_FStar.HyperStack.reference", "equation_FStar.Monotonic.Heap.modifies", "equation_FStar.Monotonic.Heap.modifies_t", "equation_FStar.Monotonic.HyperHeap.contains_ref", "equation_FStar.Monotonic.HyperHeap.modifies_just", "equation_FStar.Monotonic.HyperHeap.modifies_one", "equation_FStar.Monotonic.HyperHeap.modifies_rref", "equation_FStar.Monotonic.HyperHeap.t", "equation_FStar.Monotonic.HyperHeap.unused_in", "equation_FStar.Monotonic.HyperStack.as_addr", "equation_FStar.Monotonic.HyperStack.as_ref", "equation_FStar.Monotonic.HyperStack.contains", "equation_FStar.Monotonic.HyperStack.frameOf", "equation_FStar.Monotonic.HyperStack.hh", "equation_FStar.Monotonic.HyperStack.modifies_one", "equation_FStar.Monotonic.HyperStack.modifies_ref", "equation_FStar.Monotonic.HyperStack.unused_in", "equation_FStar.Set.eqtype", "equation_FStar.Set.subset", "equation_Prims.eqtype", "equation_Prims.nat", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_FStar.Monotonic.HyperHeap.rid", "lemma_FStar.Buffer.lemma_modifies_sub_2", "lemma_FStar.Buffer.no_upd_lemma_2", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomConcat", "lemma_FStar.Map.lemma_InDomRestrict", "lemma_FStar.Map.lemma_SelConcat1", "lemma_FStar.Map.lemma_SelConcat2", "lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_equal_intro", "lemma_FStar.Monotonic.HyperStack.lemma_live_1", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "proj_equation_FStar.Buffer.MkBuffer_content", "proj_equation_FStar.Monotonic.HyperStack.MkRef_id", "proj_equation_FStar.Monotonic.HyperStack.MkRef_ref", "projection_inverse_BoxBool_proj_0", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_38d52172626ad62ce3b0e4245dab71ed", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_347cdcabc7e8becd6dd649804986fa75", "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "refinement_kinding_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d", "typing_FStar.Buffer.__proj__MkBuffer__item__content", "typing_FStar.Buffer.frameOf", "typing_FStar.Map.concat", "typing_FStar.Map.contains", "typing_FStar.Map.restrict", "typing_FStar.Monotonic.HyperHeap.unused_in", "typing_FStar.Monotonic.HyperStack.__proj__HS__item__h", "typing_FStar.Monotonic.HyperStack.__proj__MkRef__item__id", "typing_FStar.Monotonic.HyperStack.__proj__MkRef__item__ref", "typing_FStar.Set.complement", "typing_FStar.Set.singleton", "typing_FStar.Set.union" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_def_0", 1, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_def_0", 2, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_Prims.nat", "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_def_0", 3, 0, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "data_elim_FStar.UInt32.Mk", "equation_FStar.UInt.fits", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_ctx", "function_token_typing_Spec.Salsa20.constant0", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen", "refinement_interpretation_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_6327bcdcb29e444a89cbcc4fdd08e098" ], 0 ], [ "Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_def_0", 4, 1, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Spec.CTR.counter_mode_blocks.fuel_instrumented", "@query", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Prims.nat", "equation_Spec.Salsa20.salsa20_cipher", "equation_Spec.Salsa20.salsa20_ctx", "equation_with_fuel_Spec.CTR.counter_mode_blocks.fuel_instrumented", "kinding_FStar.UInt8.t_@tok", "lemma_FStar.Seq.Base.lemma_eq_elim", "primitive_Prims.op_Equality", "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349", "refinement_interpretation_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "typing_FStar.Seq.Base.createEmpty" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_counter_mode_blocks", 1, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_counter_mode_blocks", 2, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_Prims.nat", "haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_counter_mode_blocks", 3, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "data_elim_FStar.UInt32.Mk", "data_elim_Spec.CTR.Mkblock_cipher_ctx", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.idx", "equation_FStar.Buffer.length", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_ctx", "fuel_guarded_inversion_FStar.Buffer._buffer", "function_token_typing_FStar.UInt64.n", "function_token_typing_Spec.Salsa20.constant0", "function_token_typing_Spec.Salsa20.salsa20_ctx", "kinding_FStar.UInt8.t_@tok", "lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Buffer.MkBuffer_idx", "proj_equation_FStar.Buffer.MkBuffer_length", "proj_equation_FStar.Buffer.MkBuffer_max_length", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_82db053939908f699a97088907080433", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_c605ad52f2c3598e8c57d9bb607e8bab", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "typing_FStar.Seq.Base.length" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_counter_mode_blocks", 4, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "data_elim_FStar.Buffer.MkBuffer", "data_elim_FStar.Monotonic.HyperStack.MkRef", "data_elim_FStar.UInt32.Mk", "eq2-interp", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.disjoint", "equation_FStar.Buffer.equal", "equation_FStar.Buffer.idx", "equation_FStar.Buffer.includes", "equation_FStar.Buffer.length", "equation_FStar.Buffer.live", "equation_FStar.Buffer.offset", "equation_FStar.Buffer.sel", "equation_FStar.Buffer.sub", "equation_FStar.HyperStack.reference", "equation_FStar.Monotonic.HyperHeap.contains_ref", "equation_FStar.Monotonic.HyperStack.contains", "equation_FStar.Preorder.preorder", "equation_FStar.Preorder.relation", "equation_FStar.Seq.Properties.split", "equation_FStar.UInt.add", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.sub", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.add", "equation_FStar.UInt32.n", "equation_FStar.UInt32.sub", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.invariant", "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.nat", "equation_Spec.CTR.xor", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_cipher", "equation_Spec.Salsa20.salsa20_ctx", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference", "fuel_guarded_inversion_FStar.UInt32.t_", "fuel_guarded_inversion_FStar.UInt64.t_", "function_token_typing_Spec.Salsa20.constant2", "int_inversion", "int_typing", "interpretation_Hacl.Impl.Salsa20_Tm_abs_e23371132ccdf7555cde94b05bce6e6a", "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok", "l_and-interp", "lemma_FStar.Buffer.lemma_disjoint_sub", "lemma_FStar.Buffer.lemma_disjoint_sub_", "lemma_FStar.Buffer.lemma_disjoint_symm", "lemma_FStar.Buffer.lemma_modifies_2_trans_", "lemma_FStar.Buffer.lemma_offset_spec", "lemma_FStar.Buffer.lemma_size", "lemma_FStar.Buffer.lemma_sub_spec", "lemma_FStar.Buffer.lemma_sub_spec_", "lemma_FStar.Buffer.modifies_subbuffer_2", "lemma_FStar.Buffer.no_upd_lemma_2", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Seq.Properties.slice_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Buffer.MkBuffer_content", "proj_equation_FStar.Buffer.MkBuffer_idx", "proj_equation_FStar.Buffer.MkBuffer_length", "proj_equation_FStar.Buffer.MkBuffer_max_length", "proj_equation_FStar.Monotonic.HyperStack.HS_h", "proj_equation_FStar.UInt32.Mk_v", "proj_equation_Hacl.Impl.Salsa20.MkLog_k", "proj_equation_Hacl.Impl.Salsa20.MkLog_n", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Buffer.MkBuffer_idx", "projection_inverse_FStar.Buffer.MkBuffer_length", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.UInt32.Mk_v", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen", "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9", "refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75", "refinement_interpretation_FStar.Buffer_Tm_refine_95dc1e33dd60ad6482e32befcb68dd47", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.Buffer_Tm_refine_ba20691c598b7aba0d11d91ead0d6da1", "refinement_interpretation_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d", "refinement_interpretation_FStar.Int.Cast_Tm_refine_c43881637fea8b5528f4439c75737f91", "refinement_interpretation_FStar.Preorder_Tm_refine_bd10f09297e0e7dc08314f7d9211801c", "refinement_interpretation_FStar.Seq.Base_Tm_refine_03127b5d59ee3055620018693b4264e8", "refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9", "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349", "refinement_interpretation_FStar.Seq.Base_Tm_refine_559c261b1c3777929ea329abfe70ab33", "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68", "refinement_interpretation_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_FStar.Seq.Base_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b", "refinement_interpretation_FStar.Seq.Properties_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a", "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860", "refinement_interpretation_FStar.UInt32_Tm_refine_8af61d0447e6887060c2411d0a533c0b", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_03b8e2da233e9469375bdd2aeea0d898", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_13fe60d1a58ee3ca21c0a22cb56aa0c4", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_1939c57ed0c4d00b8a860ca6efb0065c", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_48e1d639f7bfe20139b9a08d7ef9c41f", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_4ab2e194b59a9877b8ec5be853390d54", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5690982ce2c559840a2bb26948ccca3b", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_60a3cbff79c8123cece9cf1ac707c385", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_75fe8a65f5666eaf920693fe19efc919", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_7ef6588018260ed3205c9e2f80e9a646", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_82db053939908f699a97088907080433", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_9f568c1b7d9c8202f130827bb225e6f3", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_b5d04c70984498c5652d371fda6f160b", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_c605ad52f2c3598e8c57d9bb607e8bab", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ca2c77f69acff4fca0b44c61a9e317a7", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_f860aaeb13179b5961dba56d31280224", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "refinement_kinding_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d", "typing_FStar.Buffer.__proj__MkBuffer__item__content", "typing_FStar.Buffer.__proj__MkBuffer__item__idx", "typing_FStar.Buffer.__proj__MkBuffer__item__length", "typing_FStar.Buffer.__proj__MkBuffer__item__max_length", "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.idx", "typing_FStar.Buffer.length", "typing_FStar.Buffer.sel", "typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.Monotonic.HyperStack.sel", "typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.createEmpty", "typing_FStar.Seq.Base.slice", "typing_FStar.UInt32.__proj__Mk__item__v", "typing_FStar.UInt32.add", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_FStar.UInt64.v" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_counter_mode", 1, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n", "haseqHacl.Impl.Salsa20_Tm_refine_530be526726c3b66223dd819f9d65058", "projection_inverse_BoxInt_proj_0" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_counter_mode", 2, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n", "haseqHacl.Impl.Salsa20_Tm_refine_530be526726c3b66223dd819f9d65058", "projection_inverse_BoxInt_proj_0" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_counter_mode", 3, 0, 1, [ "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query", "b2t_def", "data_elim_FStar.UInt32.Mk", "equation_FStar.Buffer.idx", "equation_FStar.Buffer.length", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_ctx", "function_token_typing_Spec.Salsa20.constant0", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5ecfbc3b1fb0a18cc9b570ff75576d79" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_counter_mode", 4, 0, 1, [ "@MaxFuel_assumption", "@MaxIFuel_assumption", "@fuel_correspondence_Prims.pow2.fuel_instrumented", "@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented", "@query", "b2t_def", "bool_inversion", "bool_typing", "data_elim_FStar.Buffer.MkBuffer", "data_elim_FStar.Monotonic.HyperStack.MkRef", "data_elim_FStar.UInt32.Mk", "data_elim_Hacl.Impl.Salsa20.MkLog", "data_elim_Spec.CTR.Mkblock_cipher_ctx", "eq2-interp", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.disjoint", "equation_FStar.Buffer.equal", "equation_FStar.Buffer.idx", "equation_FStar.Buffer.includes", "equation_FStar.Buffer.length", "equation_FStar.Buffer.live", "equation_FStar.Buffer.offset", "equation_FStar.Buffer.sel", "equation_FStar.Buffer.sub", "equation_FStar.HyperStack.reference", "equation_FStar.Monotonic.HyperHeap.contains_ref", "equation_FStar.Monotonic.HyperHeap.test0", "equation_FStar.Monotonic.HyperStack.contains", "equation_FStar.Seq.Base.op_At_Bar", "equation_FStar.Seq.Properties.split", "equation_FStar.UInt.add", "equation_FStar.UInt.fits", "equation_FStar.UInt.gt", "equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int", "equation_FStar.UInt.size", "equation_FStar.UInt.sub", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.add", "equation_FStar.UInt32.gt", "equation_FStar.UInt32.logand", "equation_FStar.UInt32.n", "equation_FStar.UInt32.sub", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt32.v", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.invariant", "equation_Hacl.Impl.Salsa20.log_t", "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims._assert", "equation_Prims.nat", "equation_Spec.CTR.counter_mode", "equation_Spec.CTR.xor", "equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_cipher", "equation_Spec.Salsa20.salsa20_ctx", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference", "fuel_guarded_inversion_FStar.UInt32.t_", "fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_", "function_token_typing_FStar.Monotonic.HyperHeap.test0", "function_token_typing_FStar.UInt32.n", "function_token_typing_Spec.Salsa20.constant2", "function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion", "int_typing", "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok", "kinding_Hacl.Impl.Salsa20.log_t_@tok", "lemma_FStar.Buffer.lemma_disjoint_sub", "lemma_FStar.Buffer.lemma_disjoint_sub_", "lemma_FStar.Buffer.lemma_disjoint_symm", "lemma_FStar.Buffer.lemma_modifies_2_trans_", "lemma_FStar.Buffer.lemma_offset_spec", "lemma_FStar.Buffer.lemma_size", "lemma_FStar.Buffer.lemma_sub_spec", "lemma_FStar.Buffer.lemma_sub_spec_", "lemma_FStar.Buffer.modifies_subbuffer_2", "lemma_FStar.Buffer.no_upd_lemma_2", "lemma_FStar.Monotonic.HyperStack.lemma_equal_domains_trans", "lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.Seq.Base.lemma_eq_intro", "lemma_FStar.Seq.Base.lemma_index_app1", "lemma_FStar.Seq.Base.lemma_index_app2", "lemma_FStar.Seq.Base.lemma_index_slice", "lemma_FStar.Seq.Base.lemma_len_append", "lemma_FStar.Seq.Base.lemma_len_slice", "lemma_FStar.Seq.Properties.slice_is_empty", "lemma_FStar.Seq.Properties.slice_length", "lemma_FStar.Seq.Properties.slice_slice", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan", "primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction", "proj_equation_FStar.Buffer.MkBuffer_content", "proj_equation_FStar.Buffer.MkBuffer_idx", "proj_equation_FStar.Buffer.MkBuffer_length", "proj_equation_FStar.Buffer.MkBuffer_max_length", "proj_equation_FStar.UInt32.Mk_v", "proj_equation_Hacl.Impl.Salsa20.MkLog_k", "proj_equation_Hacl.Impl.Salsa20.MkLog_n", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_FStar.Buffer.MkBuffer_idx", "projection_inverse_FStar.Buffer.MkBuffer_length", "projection_inverse_FStar.Pervasives.Native.Mktuple2__1", "projection_inverse_FStar.Pervasives.Native.Mktuple2__2", "projection_inverse_FStar.UInt32.Mk_v", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen", "refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e", "refinement_interpretation_FStar.Buffer_Tm_refine_1a84e78220991a93402184b67dad5da7", "refinement_interpretation_FStar.Buffer_Tm_refine_2a5224b41e2469fc580fef08e3dbb3c1", "refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9", "refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75", "refinement_interpretation_FStar.Buffer_Tm_refine_95dc1e33dd60ad6482e32befcb68dd47", "refinement_interpretation_FStar.Buffer_Tm_refine_9bfa201ea86c38505bfbda4d2a64c994", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.Buffer_Tm_refine_ba20691c598b7aba0d11d91ead0d6da1", "refinement_interpretation_FStar.Buffer_Tm_refine_ba56e54aa82f2631b0e7a66e112023c8", "refinement_interpretation_FStar.Int.Cast_Tm_refine_c43881637fea8b5528f4439c75737f91", "refinement_interpretation_FStar.Seq.Base_Tm_refine_03127b5d59ee3055620018693b4264e8", "refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9", "refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349", "refinement_interpretation_FStar.Seq.Base_Tm_refine_559c261b1c3777929ea329abfe70ab33", "refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68", "refinement_interpretation_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17", "refinement_interpretation_FStar.Seq.Base_Tm_refine_cd046bc4a887ee7e1b05946e0bf5772b", "refinement_interpretation_FStar.Seq.Properties_Tm_refine_528d1ac7a4a801fe55aa0f436f85ad2a", "refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5ecfbc3b1fb0a18cc9b570ff75576d79", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_75fe8a65f5666eaf920693fe19efc919", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_7be296ac13e03747b2adc677bea00ce5", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_7ef6588018260ed3205c9e2f80e9a646", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_82db053939908f699a97088907080433", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_a0e640e09ac87230dc09e4ef89465b9b", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_f860aaeb13179b5961dba56d31280224", "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d", "typing_FStar.Buffer.__proj__MkBuffer__item__content", "typing_FStar.Buffer.__proj__MkBuffer__item__idx", "typing_FStar.Buffer.__proj__MkBuffer__item__length", "typing_FStar.Buffer.__proj__MkBuffer__item__max_length", "typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.idx", "typing_FStar.Buffer.length", "typing_FStar.Buffer.offset", "typing_FStar.Buffer.sel", "typing_FStar.Ghost.reveal", "typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.Monotonic.HyperStack.sel", "typing_FStar.Seq.Base.createEmpty", "typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "typing_Spec.Lib.uint32s_from_le" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_counter_mode", 5, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20_counter_mode", 6, 0, 1, [ "@query", "equation_FStar.UInt32.n", "projection_inverse_BoxInt_proj_0" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20", 1, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n", "haseqHacl.Impl.Salsa20_Tm_refine_530be526726c3b66223dd819f9d65058", "projection_inverse_BoxInt_proj_0" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20", 2, 0, 1, [ "@query", "assumption_Prims.HasEq_int", "equation_FStar.UInt32.n", "haseqHacl.Impl.Salsa20_Tm_refine_530be526726c3b66223dd819f9d65058", "projection_inverse_BoxInt_proj_0" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20", 3, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20", 4, 0, 1, [ "@query", "assumption_Prims.HasEq_int" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20", 5, 0, 1, [ "@MaxIFuel_assumption", "@query", "b2t_def", "data_elim_FStar.UInt32.Mk", "equation_FStar.Buffer.length", "equation_FStar.UInt.fits", "equation_FStar.UInt.size", "equation_FStar.UInt.uint_t", "equation_FStar.UInt32.n", "equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t", "equation_FStar.UInt64.n", "equation_FStar.UInt64.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen", "equation_Spec.Salsa20.salsa20_ctx", "function_token_typing_Spec.Salsa20.constant0", "primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division", "primitive_Prims.op_Multiply", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen", "proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen", "projection_inverse_BoxBool_proj_0", "projection_inverse_BoxInt_proj_0", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen", "projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen", "refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166", "refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_94403ae1db118a2daa8d61fa9d371d82", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_f7f92882b9facb724e48fab91677a95d" ], 0 ], [ "Hacl.Impl.Salsa20.salsa20", 6, 0, 1, [ "@MaxIFuel_assumption", "@query", "assumption_FStar.Monotonic.HyperHeap.HasEq_rid", "bool_inversion", "data_elim_FStar.Monotonic.HyperStack.HS", "data_elim_FStar.Monotonic.HyperStack.MkRef", "eq2-interp", "equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer", "equation_FStar.Buffer.content", "equation_FStar.Buffer.equal", "equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.live", "equation_FStar.Buffer.unmapped_in", "equation_FStar.HyperStack.ST.inline_stack_inv", "equation_FStar.HyperStack.reference", "equation_FStar.Monotonic.HyperHeap.t", "equation_FStar.Monotonic.HyperStack.contains", "equation_FStar.Monotonic.HyperStack.equal_domains", "equation_FStar.Monotonic.HyperStack.frameOf", "equation_FStar.Monotonic.HyperStack.fresh_frame", "equation_FStar.Monotonic.HyperStack.hh", "equation_FStar.Monotonic.HyperStack.is_tip", "equation_FStar.Monotonic.HyperStack.live_region", "equation_FStar.Monotonic.HyperStack.pop", "equation_FStar.Monotonic.HyperStack.poppable", "equation_FStar.Monotonic.HyperStack.popped", "equation_FStar.Monotonic.HyperStack.remove_elt", "equation_FStar.Set.eqtype", "equation_FStar.UInt32.t", "equation_FStar.UInt64.v", "equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state", "equation_Hacl.Impl.Salsa20.uint8_p", "equation_Prims.eqtype", "equation_Spec.CTR.counter_mode", "equation_Spec.Salsa20.salsa20_cipher", "equation_Spec.Salsa20.salsa20_ctx", "fuel_guarded_inversion_FStar.Buffer._buffer", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem", "fuel_guarded_inversion_FStar.Monotonic.HyperStack.mreference", "function_token_typing_FStar.Monotonic.Heap.emp", "function_token_typing_FStar.Monotonic.Heap.heap", "function_token_typing_FStar.Monotonic.HyperHeap.rid", "kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok", "lemma_FStar.Buffer.lemma_disjoint_symm", "lemma_FStar.Buffer.lemma_equal_domains_2", "lemma_FStar.Buffer.lemma_fresh_poppable", "lemma_FStar.Buffer.lemma_live_disjoint", "lemma_FStar.Buffer.lemma_modifies_0_1_", "lemma_FStar.Buffer.lemma_modifies_0_2", "lemma_FStar.Buffer.live_fresh", "lemma_FStar.Buffer.live_popped", "lemma_FStar.Buffer.modifies_poppable_2", "lemma_FStar.Buffer.modifies_popped_1", "lemma_FStar.Buffer.no_upd_fresh", "lemma_FStar.Buffer.no_upd_lemma_0", "lemma_FStar.Buffer.no_upd_popped", "lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Monotonic.HyperStack.lemma_equal_domains_trans", "lemma_FStar.Set.lemma_equal_elim", "lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect", "lemma_FStar.Set.mem_singleton", "primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar", "primitive_Prims.op_Equality", "primitive_Prims.op_Negation", "primitive_Prims.op_disEquality", "proj_equation_FStar.Buffer.MkBuffer_content", "proj_equation_FStar.Monotonic.HyperStack.HS_h", "proj_equation_FStar.Monotonic.HyperStack.HS_tip", "proj_equation_FStar.Monotonic.HyperStack.MkRef_id", "projection_inverse_BoxBool_proj_0", "projection_inverse_FStar.Monotonic.HyperStack.HS_h", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_0418702750d54a72833a38f310956e3d", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_38d52172626ad62ce3b0e4245dab71ed", "refinement_interpretation_FStar.Monotonic.HyperStack_Tm_refine_b05295ea25e1fbfe5a4bd48cb81ddfff", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_5ecfbc3b1fb0a18cc9b570ff75576d79", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_94403ae1db118a2daa8d61fa9d371d82", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd", "refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_f7f92882b9facb724e48fab91677a95d", "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f", "typing_FStar.Buffer.__proj__MkBuffer__item__content", "typing_FStar.Map.contains", "typing_FStar.Map.domain", "typing_FStar.Monotonic.HyperStack.__proj__HS__item__h", "typing_FStar.Monotonic.HyperStack.__proj__HS__item__tip", "typing_FStar.Monotonic.HyperStack.poppable", "typing_FStar.Set.complement", "typing_FStar.Set.intersect", "typing_FStar.Set.singleton" ], 0 ] ] ]