https://github.com/project-everest/hacl-star
Tip revision: 01833dd5c374063356d6528dc613859d7c672130 authored by prosecco on 23 January 2018, 14:39:39 UTC
current
current
Tip revision: 01833dd
Hacl.Impl.Salsa20.fst.hints
[
"\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
]
]
]