https://github.com/project-everest/hacl-star
Tip revision: af3c346cc67161fd260dbfb48e5f6087ff119b57 authored by Jonathan Protzenko on 26 May 2017, 13:33:56 UTC
Final Makefile fixup; fix breakage with recent F* versions
Final Makefile fixup; fix breakage with recent F* versions
Tip revision: af3c346
Hacl.Impl.Salsa20.fst.hints
[
"ü┤fú N\u0010,¥░Å»4$¡\u0018",
[
[
"Hacl.Impl.Salsa20.state",
1,
2,
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",
"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_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.u32",
"equation_Hacl.UInt32.t", "equation_Prims.nat",
"equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant0",
"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_Spec.Salsa20.constant0",
"function_token_typing_Spec.Salsa20.constant2",
"function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion",
"lemma_FStar.Buffer.lemma_size", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_9941a4ed3911ef331a8db7c7fbf2373b",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"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_Hacl.UInt32.t",
"equation_Hacl.UInt8.t", "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", "@query",
"assumption_FStar.HyperHeap.HasEq_rid", "b2t_def", "bool_inversion",
"bool_typing", "data_elim_FStar.Buffer.MkBuffer",
"data_elim_FStar.HyperStack.HS", "data_elim_FStar.HyperStack.MkRef",
"data_elim_FStar.UInt32.Mk", "data_elim_FStar.UInt64.Mk",
"data_elim_Spec.CTR.Mkblock_cipher_ctx",
"equation_FStar.Buffer.buffer", "equation_FStar.Buffer.contains",
"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.HyperHeap.map_invariant",
"equation_FStar.HyperHeap.t", "equation_FStar.HyperStack.contains",
"equation_FStar.HyperStack.equal_domains",
"equation_FStar.HyperStack.frameOf",
"equation_FStar.HyperStack.fresh_frame",
"equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_in",
"equation_FStar.HyperStack.is_tip",
"equation_FStar.HyperStack.live_region",
"equation_FStar.HyperStack.pop",
"equation_FStar.HyperStack.poppable", "equation_FStar.Mul.op_Star",
"equation_FStar.ST.inline_stack_inv", "equation_FStar.Set.eqtype",
"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.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.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_Hacl.UInt32.t", "equation_Hacl.UInt8.t",
"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.keylen", "equation_Spec.Salsa20.noncelen",
"equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.setup",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.HyperStack.mem",
"fuel_guarded_inversion_FStar.HyperStack.reference",
"fuel_guarded_inversion_FStar.UInt32.t_",
"fuel_guarded_inversion_FStar.UInt64.t_",
"function_token_typing_FStar.Heap.heap",
"function_token_typing_FStar.HyperHeap.rid",
"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",
"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.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.HyperStack.lemma_equal_domains_trans",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "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.HyperStack.HS_h",
"proj_equation_FStar.HyperStack.HS_tip",
"proj_equation_FStar.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",
"refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
"refinement_interpretation_FStar.HyperStack_Tm_refine_17c32ea1674222a60392f05cf1ea594b",
"refinement_interpretation_FStar.HyperStack_Tm_refine_4c3d3c35ed77aaa549ae6f40eebffd27",
"refinement_interpretation_FStar.HyperStack_Tm_refine_f724abd6de992fc2f861487694296e1a",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"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",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.Buffer.__proj__MkBuffer__item__content",
"typing_FStar.Buffer.__proj__MkBuffer__item__length",
"typing_FStar.Buffer.content", "typing_FStar.Buffer.length",
"typing_FStar.HyperHeap.includes",
"typing_FStar.HyperStack.__proj__HS__item__h",
"typing_FStar.HyperStack.__proj__HS__item__tip",
"typing_FStar.HyperStack.poppable", "typing_FStar.Map.contains",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v"
],
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",
"equation_Hacl.UInt32.t", "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.line",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.as_seq",
"equation_FStar.Buffer.buffer", "equation_FStar.UInt32.add_mod",
"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_Hacl.UInt32.t",
"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.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",
"equation_Hacl.UInt32.t", "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", "b2t_def", "bool_inversion",
"bool_typing", "data_elim_FStar.UInt32.Mk",
"equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
"equation_FStar.Buffer.contains", "equation_FStar.Buffer.live",
"equation_FStar.HyperHeap.contains_ref",
"equation_FStar.HyperStack.contains", "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_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.idx",
"equation_Hacl.Impl.Salsa20.state", "equation_Hacl.UInt32.t",
"equation_Spec.Lib.op_At", "equation_Spec.Salsa20.constant2",
"equation_Spec.Salsa20.quarter_round", "equation_Spec.Salsa20.state",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.HyperStack.mem",
"function_token_typing_Spec.Salsa20.constant2",
"kinding_FStar.UInt32.t_@tok",
"lemma_FStar.Buffer.lemma_modifies_1_trans",
"lemma_FStar.HyperStack.lemma_equal_domains_trans",
"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_Hacl.Impl.Salsa20_Tm_refine_5fd76f96dd8842f1d4e9ef690b5c4ee7",
"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",
"typing_FStar.UInt32.v"
],
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",
"equation_Hacl.UInt32.t",
"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", "b2t_def", "bool_inversion",
"bool_typing", "data_elim_FStar.UInt32.Mk",
"data_elim_Spec.CTR.Mkblock_cipher_ctx",
"equation_FStar.Buffer.buffer", "equation_FStar.Buffer.contains",
"equation_FStar.Buffer.live",
"equation_FStar.HyperHeap.contains_ref",
"equation_FStar.HyperStack.contains", "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_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
"equation_Hacl.UInt32.t", "equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Lib.op_At", "equation_Spec.Salsa20.blocklen",
"equation_Spec.Salsa20.column_round",
"equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant2",
"equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
"equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.state",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.HyperStack.mem",
"function_token_typing_Spec.Salsa20.constant0",
"function_token_typing_Spec.Salsa20.constant2",
"function_token_typing_Spec.Salsa20.salsa20_ctx",
"kinding_FStar.UInt32.t_@tok",
"lemma_FStar.Buffer.lemma_modifies_1_trans",
"lemma_FStar.HyperStack.lemma_equal_domains_trans",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"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_e6f73d69171d3f532dd3233ed82d65f8",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"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",
"equation_Hacl.UInt32.t",
"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", "b2t_def", "bool_inversion",
"bool_typing", "data_elim_FStar.UInt32.Mk",
"data_elim_Spec.CTR.Mkblock_cipher_ctx",
"equation_FStar.Buffer.buffer", "equation_FStar.Buffer.contains",
"equation_FStar.Buffer.live",
"equation_FStar.HyperHeap.contains_ref",
"equation_FStar.HyperStack.contains", "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_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
"equation_Hacl.UInt32.t", "equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Lib.op_At", "equation_Spec.Salsa20.blocklen",
"equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant2",
"equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
"equation_Spec.Salsa20.row_round",
"equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.state",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.HyperStack.mem",
"function_token_typing_Spec.Salsa20.constant0",
"function_token_typing_Spec.Salsa20.constant2",
"function_token_typing_Spec.Salsa20.salsa20_ctx", "int_typing",
"kinding_FStar.UInt32.t_@tok",
"lemma_FStar.Buffer.lemma_modifies_1_trans",
"lemma_FStar.HyperStack.lemma_equal_domains_trans",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"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.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_Spec.Lib.op_At",
"token_correspondence_Spec.Salsa20.quarter_round",
"typing_FStar.UInt32.uint_to_t"
],
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",
"equation_Hacl.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_Hacl.UInt32.t", "equation_Spec.Lib.op_At",
"equation_Spec.Salsa20.double_round", "equation_Spec.Salsa20.state",
"fuel_guarded_inversion_FStar.HyperStack.mem",
"kinding_FStar.UInt32.t_@tok",
"lemma_FStar.Buffer.lemma_modifies_1_trans",
"lemma_FStar.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",
"equation_Hacl.UInt32.t",
"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",
"@fuel_correspondence_Spec.Loops.repeat_spec.fuel_instrumented",
"@query", "b2t_def", "bool_inversion", "bool_typing",
"data_elim_FStar.UInt32.Mk", "eq2-interp",
"equation_FStar.Buffer.buffer", "equation_FStar.Buffer.live",
"equation_FStar.HyperHeap.t", "equation_FStar.HyperStack.hh",
"equation_FStar.HyperStack.is_in", "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_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
"equation_Hacl.UInt32.t", "equation_Prims.l_and",
"equation_Prims.nat", "equation_Spec.Salsa20.constant0",
"equation_Spec.Salsa20.constant2", "equation_Spec.Salsa20.rounds",
"equation_Spec.Salsa20.state",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.HyperStack.mem",
"function_token_typing_FStar.HyperHeap.root",
"function_token_typing_Spec.Salsa20.constant0",
"function_token_typing_Spec.Salsa20.constant2", "int_inversion",
"interpretation_Hacl.Impl.Salsa20_Tm_abs_42afa9f0568a6be2243263d68a942f30",
"kinding_FStar.UInt32.t_@tok", "l_and-interp",
"lemma_FStar.Buffer.lemma_modifies_1_trans",
"lemma_FStar.Buffer.lemma_modifies_sub_1",
"lemma_FStar.Buffer.lemma_size", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_FStar.HyperStack.HS_h",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_FStar.HyperStack_Tm_refine_f724abd6de992fc2f861487694296e1a",
"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.HyperStack.__proj__HS__item__h",
"typing_FStar.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_Hacl.UInt32.t", "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",
"equation_Hacl.UInt32.t",
"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.UInt.uint_t",
"equation_FStar.UInt32.n", "equation_FStar.UInt32.t",
"equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
"equation_Hacl.UInt32.t", "kinding_FStar.UInt32.t_@tok",
"proj_equation_FStar.Buffer.MkBuffer_length",
"refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"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.UInt32.v"
],
0
],
[
"Hacl.Impl.Salsa20.copy_state",
1,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[ "Hacl.Impl.Salsa20.copy_state", 2, 0, 1, [ "@query" ], 0 ],
[
"Hacl.Impl.Salsa20.copy_state",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing", "data_elim_FStar.UInt32.Mk",
"equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
"equation_FStar.Buffer.contains", "equation_FStar.Buffer.equal",
"equation_FStar.Buffer.length", "equation_FStar.Buffer.live",
"equation_FStar.HyperHeap.contains_ref",
"equation_FStar.HyperStack.contains", "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.UInt16.n", "equation_FStar.UInt32.n",
"equation_FStar.UInt32.t", "equation_FStar.UInt32.uint_to_t",
"equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
"equation_Hacl.UInt32.t", "equation_Prims.nat",
"equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant2",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.HyperStack.mem",
"function_token_typing_FStar.UInt16.n",
"function_token_typing_Spec.Salsa20.constant0",
"function_token_typing_Spec.Salsa20.constant2", "int_inversion",
"int_typing", "kinding_FStar.UInt32.t_@tok",
"lemma_FStar.Buffer.lemma_disjoint_symm",
"lemma_FStar.Buffer.no_upd_lemma_1",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_FStar.Buffer.MkBuffer_length",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.Buffer_Tm_refine_347cdcabc7e8becd6dd649804986fa75",
"refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_75fe8a65f5666eaf920693fe19efc919",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Buffer.__proj__MkBuffer__item__length",
"typing_FStar.Buffer.as_seq", "typing_FStar.UInt32.v",
"unit_inversion", "unit_typing"
],
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,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"data_elim_FStar.UInt32.Mk", "equation_FStar.Mul.op_Star",
"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_Prims.pos",
"equation_Spec.Salsa20.constant2",
"fuel_guarded_inversion_FStar.UInt32.t_",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt64.n",
"function_token_typing_Spec.Salsa20.constant2", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"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.UInt64.Mk_v",
"refinement_interpretation_FStar.Int.Cast_Tm_refine_c43881637fea8b5528f4439c75737f91",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.UInt64.v"
],
0
],
[
"Hacl.Impl.Salsa20.u64_of_u32s",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Impl.Salsa20.u64_of_u32s",
3,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Impl.Salsa20.low32_of_u64",
1,
0,
1,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0
],
[
"Hacl.Impl.Salsa20.low32_of_u64",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Impl.Salsa20.low32_of_u64",
3,
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", "bool_inversion", "bool_typing",
"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.UInt64.n", "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.UInt64.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"typing_FStar.UInt64.v"
],
0
],
[
"Hacl.Impl.Salsa20.high32_of_u64",
2,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Impl.Salsa20.high32_of_u64",
3,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Impl.Salsa20.invariant",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.UInt32.t",
"equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
"equation_Hacl.UInt32.t", "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_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_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", "equation_FStar.Mul.op_Star", "equation_FStar.UInt32.t",
"equation_FStar.UInt64.t", "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_Hacl.UInt32.t",
"equation_Hacl.UInt64.v", "equation_Prims.nat",
"equation_Spec.Lib.lbytes", "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.setup",
"equation_Spec.Salsa20.state", "function_token_typing_FStar.UInt8.n",
"int_inversion", "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",
"projection_inverse_BoxInt_proj_0",
"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.Impl.Salsa20_Tm_refine_284965375ecf482d8c163a797855f9fb",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_54c03c78d7539eae7ee3b6a012705328",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ad73429f90f4e2d794c61307d038fc0f",
"refinement_interpretation_Hacl.Spec.Endianness_Tm_refine_cd9ef244d254c5b3dbb3e422699c3613",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.Salsa20_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Impl.Salsa20.high32_of_u64",
"typing_Hacl.Impl.Salsa20.low32_of_u64",
"typing_Spec.Lib.uint32s_from_le"
],
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,
[
"@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",
"data_typing_intro_FStar.UInt64.Mk@tok",
"equation_FStar.Mul.op_Star", "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.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",
"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.UInt.pow2_values",
"lemma_FStar.UInt.shift_right_value_lemma",
"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", "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.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",
"token_correspondence_Seq.Create.create_16",
"typing_FStar.Int.Cast.uint64_to_uint32", "typing_FStar.Mul.op_Star",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_FStar.UInt.shift_right", "typing_FStar.UInt64.uint_to_t",
"typing_Seq.Create.create_16", "typing_Spec.Lib.uint32s_from_le",
"unit_typing"
],
0
],
[
"Hacl.Impl.Salsa20.lemma_u64_of_u32s",
1,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "data_elim_FStar.UInt32.Mk", "equation_FStar.Mul.op_Star",
"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_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.constant2",
"fuel_guarded_inversion_FStar.UInt32.t_",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_Spec.Salsa20.constant2", "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",
"refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_129089aa650ccd93ce04c3c260485c61",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ad73429f90f4e2d794c61307d038fc0f",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"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_FStar.UInt32.t__haseq",
"equation_FStar.UInt32.t"
],
0
],
[
"Hacl.Impl.Salsa20.lemma_u64_of_u32s",
5,
0,
1,
[
"@query", "assumption_FStar.UInt32.t__haseq",
"equation_FStar.UInt32.t"
],
0
],
[
"Hacl.Impl.Salsa20.lemma_u64_of_u32s",
6,
0,
1,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Hacl.Impl.Salsa20.lemma_u64_of_u32s",
7,
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", "equation_Hacl.UInt32.t",
"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,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented",
"@query",
"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",
"equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
"equation_FStar.Buffer.equal", "equation_FStar.Buffer.get",
"equation_FStar.Buffer.idx", "equation_FStar.Buffer.length",
"equation_FStar.Buffer.sel", "equation_FStar.Ghost.elift1",
"equation_FStar.Ghost.reveal", "equation_FStar.HyperHeap.t",
"equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_in",
"equation_FStar.Mul.op_Star", "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.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_Hacl.UInt32.t",
"equation_Hacl.UInt32.v", "equation_Hacl.UInt64.t",
"equation_Hacl.UInt64.v", "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_core",
"equation_Spec.Salsa20.salsa20_ctx", "equation_Spec.Salsa20.setup",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.HyperStack.mem",
"fuel_guarded_inversion_FStar.UInt32.t_",
"fuel_guarded_inversion_FStar.UInt64.t_",
"fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_",
"function_token_typing_FStar.HyperHeap.root",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.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",
"interpretation_Hacl.Impl.Salsa20_Tm_abs_e4d6ac50eaa2d62b7664f2b35c63c0a0",
"kinding_FStar.UInt32.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.HyperStack.lemma_equal_domains_trans",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_FStar.Buffer.MkBuffer_content",
"proj_equation_FStar.Buffer.MkBuffer_length",
"proj_equation_FStar.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.UInt64.Mk_v",
"projection_inverse_Prims.Mktuple2__1",
"projection_inverse_Prims.Mktuple2__2",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d",
"refinement_interpretation_FStar.HyperStack_Tm_refine_f724abd6de992fc2f861487694296e1a",
"refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f",
"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_b5ad1dbfbd48faaf34d92bafda76205d",
"refinement_interpretation_FStar.UInt32_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_FStar.UInt64_Tm_refine_2cdf10a0b17b1e313a0b7d29add2d0a1",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Cast_Tm_refine_c4fd3ce9175da67bf1384c82ed404121",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_129089aa650ccd93ce04c3c260485c61",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_16ca4d57531a6a8463e17460cee0a655",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_512d2e36eceaae5937ab1ff1eef964fd",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ad73429f90f4e2d794c61307d038fc0f",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Seq.Create_Tm_refine_03488b8732f12d7416d4f57733783c65",
"refinement_kinding_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d",
"typing_FStar.Buffer.__proj__MkBuffer__item__content",
"typing_FStar.Buffer.__proj__MkBuffer__item__length",
"typing_FStar.Buffer.idx", "typing_FStar.Ghost.reveal",
"typing_FStar.HyperStack.__proj__HS__item__h",
"typing_FStar.HyperStack.is_in", "typing_FStar.HyperStack.sel",
"typing_FStar.Int.Cast.uint64_to_uint32", "typing_FStar.Mul.op_Star",
"typing_FStar.Seq.Base.index", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt64.shift_right",
"typing_Hacl.Cast.uint32_to_sint32",
"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.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.HyperHeap.HasEq_rid", "b2t_def", "bool_inversion",
"bool_typing", "data_elim_FStar.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",
"equation_FStar.Buffer.buffer", "equation_FStar.Buffer.contains",
"equation_FStar.Buffer.content", "equation_FStar.Buffer.equal",
"equation_FStar.Buffer.frameOf", "equation_FStar.Buffer.length",
"equation_FStar.Buffer.live", "equation_FStar.Ghost.reveal",
"equation_FStar.Heap.emp", "equation_FStar.HyperHeap.t",
"equation_FStar.HyperStack.contains",
"equation_FStar.HyperStack.equal_domains",
"equation_FStar.HyperStack.frameOf",
"equation_FStar.HyperStack.fresh_frame",
"equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_tip",
"equation_FStar.HyperStack.live_region",
"equation_FStar.HyperStack.pop",
"equation_FStar.HyperStack.poppable",
"equation_FStar.HyperStack.popped",
"equation_FStar.HyperStack.remove_elt", "equation_FStar.Mul.op_Star",
"equation_FStar.ST.inline_stack_inv", "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.UInt16.n",
"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_Hacl.UInt32.t",
"equation_Hacl.UInt32.v", "equation_Hacl.UInt8.t",
"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.HyperStack.reference",
"fuel_guarded_inversion_FStar.UInt32.t_",
"fuel_guarded_inversion_FStar.UInt64.t_",
"fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_",
"function_token_typing_FStar.Heap.emp",
"function_token_typing_FStar.Heap.heap",
"function_token_typing_FStar.HyperHeap.rid",
"function_token_typing_FStar.UInt16.n",
"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_1",
"lemma_FStar.Buffer.no_upd_lemma_2_1",
"lemma_FStar.Buffer.no_upd_popped",
"lemma_FStar.HyperStack.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1",
"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_GreaterThanOrEqual",
"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.Buffer.MkBuffer_length",
"proj_equation_FStar.HyperStack.HS_h",
"proj_equation_FStar.HyperStack.MkRef_id",
"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.HyperStack.HS_h",
"projection_inverse_FStar.UInt32.Mk_v",
"projection_inverse_FStar.UInt64.Mk_v",
"projection_inverse_Prims.Mktuple2__1",
"projection_inverse_Prims.Mktuple2__2",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
"refinement_interpretation_FStar.HyperStack_Tm_refine_17c32ea1674222a60392f05cf1ea594b",
"refinement_interpretation_FStar.HyperStack_Tm_refine_f724abd6de992fc2f861487694296e1a",
"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_2cdf10a0b17b1e313a0b7d29add2d0a1",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_129089aa650ccd93ce04c3c260485c61",
"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",
"refinement_kinding_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d",
"typing_FStar.Buffer.__proj__MkBuffer__item__content",
"typing_FStar.Buffer.__proj__MkBuffer__item__length",
"typing_FStar.Buffer.length", "typing_FStar.Ghost.reveal",
"typing_FStar.HyperStack.__proj__HS__item__h",
"typing_FStar.HyperStack.__proj__HS__item__tip",
"typing_FStar.HyperStack.__proj__MkRef__item__id",
"typing_FStar.HyperStack.poppable",
"typing_FStar.HyperStack.remove_elt",
"typing_FStar.Int.Cast.uint64_to_uint32",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Mul.op_Star",
"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.UInt32.v", "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.salsa20_block",
4,
0,
1,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Hacl.Impl.Salsa20.alloc",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"bool_typing", "data_elim_FStar.UInt32.Mk",
"equation_FStar.Buffer.buffer", "equation_FStar.Buffer.unmapped_in",
"equation_FStar.HyperStack.is_stack_region",
"equation_FStar.ST.inline_stack_inv", "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_Hacl.Impl.Salsa20.h32",
"equation_Hacl.Impl.Salsa20.state", "equation_Hacl.UInt32.t",
"equation_Spec.Salsa20.constant0", "equation_Spec.Salsa20.constant2",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.HyperStack.mem",
"function_token_typing_Spec.Salsa20.constant0",
"function_token_typing_Spec.Salsa20.constant2",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"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", "b2t_def", "bool_inversion",
"constructor_distinct_Hacl.Impl.Salsa20.MkLog",
"data_elim_Spec.CTR.Mkblock_cipher_ctx",
"equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
"equation_FStar.Buffer.contains", "equation_FStar.Buffer.equal",
"equation_FStar.Buffer.live", "equation_FStar.Ghost.elift2",
"equation_FStar.Ghost.hide", "equation_FStar.Ghost.reveal",
"equation_FStar.HyperHeap.contains_ref",
"equation_FStar.HyperHeap.t", "equation_FStar.HyperStack.contains",
"equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_in",
"equation_FStar.Mul.op_Star", "equation_FStar.Seq.Base.index",
"equation_FStar.Seq.Base.length", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt32.t",
"equation_FStar.UInt64.n", "equation_FStar.UInt64.t",
"equation_FStar.UInt64.v", "equation_FStar.UInt8.n",
"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_Hacl.UInt32.t",
"equation_Hacl.UInt8.t", "equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
"equation_Spec.Salsa20.noncelen",
"equation_Spec.Salsa20.salsa20_ctx",
"fuel_correspondence_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"function_token_typing_FStar.Heap.emp",
"function_token_typing_FStar.HyperHeap.root",
"function_token_typing_FStar.UInt64.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion",
"int_typing",
"interpretation_Tm_abs_63a15c105abe152a30c61ae574816e90",
"interpretation_Tm_arrow_1b11ac8ae397ade469edcdbcfe2629d5",
"kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok",
"lemma_FStar.Buffer.no_upd_lemma_1", "lemma_FStar.UInt.pow2_values",
"pretyping_6c86c071b92797cdf01eb016249a9465",
"pretyping_a87e903bbc455531fa4b8b47a243ed22",
"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.HyperStack.HS_h",
"proj_equation_FStar.Seq.Base.MkSeq_l",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Hacl.Impl.Salsa20.MkLog_k",
"projection_inverse_Hacl.Impl.Salsa20.MkLog_n",
"refinement_interpretation_Tm_refine_0dc1829dbc3c1d1c42b7a4e9e5c89884",
"refinement_interpretation_Tm_refine_162a3c2ee4d10c15b5e46cb5963460d6",
"refinement_interpretation_Tm_refine_173c3f7fb931ea8e37f2cd554b93e659",
"refinement_interpretation_Tm_refine_19ef25f2e2d3d73de8cb0dc4c23167bd",
"refinement_interpretation_Tm_refine_96a28a851eecacef3e62c1298dc55be7",
"refinement_interpretation_Tm_refine_b25bac71ace031ea1b4048c58d6ef05a",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c32bdda13bfb14d0d2f58700b5fc6c38",
"refinement_interpretation_Tm_refine_d0248a37b555c45264d4be3b1e2a8bff",
"refinement_interpretation_Tm_refine_e6f73d69171d3f532dd3233ed82d65f8",
"refinement_interpretation_Tm_refine_ec8c52b60e5c33b3ae66e4063643ec19",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.Buffer.length",
"typing_FStar.HyperStack.__proj__HS__item__h",
"typing_FStar.HyperStack.is_in", "typing_FStar.List.Tot.Base.index",
"typing_FStar.Seq.Base.__proj__MkSeq__item__l",
"typing_FStar.Seq.Base.index",
"typing_Hacl.Impl.Salsa20.u64_of_u32s", "typing_Prims.pow2"
],
0
],
[
"Hacl.Impl.Salsa20.init",
4,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "data_elim_Spec.CTR.Mkblock_cipher_ctx",
"equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
"equation_FStar.Buffer.equal", "equation_FStar.Buffer.length",
"equation_FStar.Ghost.elift2", "equation_FStar.Ghost.hide",
"equation_FStar.Ghost.reveal", "equation_FStar.Mul.op_Star",
"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.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.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_Hacl.UInt32.t",
"equation_Hacl.UInt32.v", "equation_Hacl.UInt8.t",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
"equation_Spec.Salsa20.noncelen",
"equation_Spec.Salsa20.salsa20_ctx",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.UInt32.t_",
"function_token_typing_FStar.UInt64.n",
"function_token_typing_FStar.UInt8.n",
"function_token_typing_Spec.Salsa20.salsa20_ctx", "int_inversion",
"int_typing",
"interpretation_Hacl.Impl.Salsa20_Tm_abs_d31b587ffcac8fd2ef2652970b6cbd9f",
"kinding_FStar.UInt32.t_@tok", "kinding_FStar.UInt8.t_@tok",
"lemma_FStar.Buffer.no_upd_lemma_1", "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.UInt64.Mk_v",
"projection_inverse_Hacl.Impl.Salsa20.MkLog_k",
"projection_inverse_Hacl.Impl.Salsa20.MkLog_n",
"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_2cdf10a0b17b1e313a0b7d29add2d0a1",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_129089aa650ccd93ce04c3c260485c61",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_34c713272d4138e534ee70be89b06637",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_59174d15900b1aac0e68774108209b07",
"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",
"typing_FStar.Buffer.__proj__MkBuffer__item__length",
"typing_FStar.Buffer.length",
"typing_FStar.Int.Cast.uint64_to_uint32",
"typing_FStar.Seq.Base.index", "typing_FStar.UInt64.shift_right",
"typing_Hacl.Impl.Salsa20.u64_of_u32s", "typing_Prims.pow2"
],
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.UInt8.t", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"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.Mul.op_Star", "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_Hacl.UInt8.t", "equation_Prims.nat",
"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.noncelen",
"equation_Spec.Salsa20.salsa20_block",
"equation_Spec.Salsa20.salsa20_ctx",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.UInt64.t_",
"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_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_Spec.Salsa20.salsa20_block"
],
0
],
[
"Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_1",
5,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"FStar.List.Tot.Base_interpretation_Tm_arrow_9105589d4b48c1456d0057b53f4c3752",
"Prims_interpretation_Tm_arrow_44faff5d8543c30ad9bf2eeaf1b3abcf",
"b2t_def", "bool_inversion", "equation_FStar.Buffer.buffer",
"equation_FStar.Buffer.length", "equation_FStar.Mul.op_Star",
"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.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_Hacl.UInt8.t",
"equation_Prims.nat", "equation_Spec.CTR.counter_mode",
"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.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.HyperStack.mem",
"fuel_guarded_inversion_FStar.UInt32.t_",
"fuel_guarded_inversion_FStar.UInt64.t_",
"function_token_typing_FStar.UInt8.logxor", "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_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"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_FStar.Buffer.MkBuffer_length",
"proj_equation_FStar.UInt32.Mk_v",
"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_Prims.Mktuple2__1",
"projection_inverse_Prims.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_811063936efbc06568ec405d75452cb9",
"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_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"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_0aaf78738bfac8fed3c5ec5ff4dc12d2",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_1c0ec6355580e726ab211a8765e4c345",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_3c1621bf563fce206bf87582cd7a1d56",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_47b3312849cf30a6997cda724f0e4751",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d287bdb5105268f1b0702cd0a5b01379",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.Loops_Tm_refine_16da5dd636ef303f4b4402f063fe1ef3",
"refinement_interpretation_Spec.Loops_Tm_refine_4af88ef44277488ec061969a3d7abb20",
"token_correspondence_FStar.UInt8.logxor",
"token_correspondence_Spec.Salsa20.salsa20_block",
"typing_FStar.Buffer.__proj__MkBuffer__item__length",
"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.xor",
"typing_Spec.Loops.seq_map2", "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_Hacl.UInt8.t", "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_FStar.Mul.op_Star",
"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", "data_elim_FStar.UInt32.Mk",
"equation_FStar.Buffer.buffer", "equation_FStar.Mul.op_Star",
"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.UInt64.n",
"equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
"equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p",
"equation_Hacl.UInt8.t", "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.HyperStack.mem",
"fuel_guarded_inversion_FStar.UInt64.t_",
"function_token_typing_Spec.Salsa20.constant0", "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_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_Prims.Mktuple2__1",
"projection_inverse_Prims.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_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_4d5f76b1705708752e4f3bb8d5a207ec",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_8fb7570df9352ae94ba22a780d28d11f",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ac03c6b5bfee50cc2664154412b8d06c",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Buffer.length", "typing_FStar.UInt64.v"
],
0
],
[
"Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_2",
6,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.CTR.counter_mode_blocks.fuel_instrumented",
"@fuel_irrelevance_Spec.CTR.counter_mode_blocks.fuel_instrumented",
"@query", "b2t_def", "bool_inversion",
"equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
"equation_FStar.Mul.op_Star", "equation_FStar.Seq.Base.op_At_Bar",
"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_Hacl.UInt8.t", "equation_Prims.nat",
"equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.blocklen",
"equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen",
"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.HyperStack.mem", "int_inversion",
"int_typing", "kinding_FStar.UInt8.t_@tok",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_FStar.UInt32.Mk_v",
"proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
"proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt32.Mk_v",
"projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
"projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Buffer_Tm_refine_347cdcabc7e8becd6dd649804986fa75",
"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_4d5f76b1705708752e4f3bb8d5a207ec",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.length",
"typing_FStar.Seq.Base.length", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.v", "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,
[
"@query", "assumption_Prims.HasEq_int", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0
],
[
"Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_0",
5,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.Buffer.buffer",
"equation_FStar.Mul.op_Star", "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_Hacl.UInt8.t",
"equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
"equation_Spec.Salsa20.noncelen",
"equation_Spec.Salsa20.salsa20_ctx",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"primitive_Prims.op_Addition", "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_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_Hacl.Impl.Salsa20_Tm_refine_04d3395c881847f65dd2a6cf9d8a71b5",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_241d61c8ad097706dd0ca2556ca9bdf1"
],
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", "equation_FStar.Buffer.as_seq",
"equation_FStar.Buffer.buffer", "equation_FStar.HyperHeap.t",
"equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_in",
"equation_FStar.UInt32.t", "equation_FStar.UInt64.v",
"equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p",
"equation_Hacl.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",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.HyperStack.mem",
"kinding_FStar.UInt8.t_@tok", "primitive_Prims.op_Equality",
"proj_equation_FStar.HyperStack.HS_h",
"refinement_interpretation_FStar.Buffer_Tm_refine_347cdcabc7e8becd6dd649804986fa75",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_FStar.HyperStack_Tm_refine_f724abd6de992fc2f861487694296e1a",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"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.HyperStack.__proj__HS__item__h",
"typing_FStar.Seq.Base.createEmpty"
],
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", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"data_elim_FStar.UInt32.Mk", "equation_FStar.Buffer.length",
"equation_FStar.Mul.op_Star", "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.uint8_p",
"equation_Hacl.UInt8.t", "equation_Prims.nat",
"equation_Spec.CTR.block", "equation_Spec.Lib.lbytes",
"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", "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_0aaf78738bfac8fed3c5ec5ff4dc12d2",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_cdd15a61a8a8f4424284702869adc760",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d287bdb5105268f1b0702cd0a5b01379",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Buffer.length", "typing_FStar.Seq.Base.length",
"typing_FStar.UInt64.v"
],
0
],
[
"Hacl.Impl.Salsa20.update_last",
4,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.HyperStack_interpretation_Tm_arrow_bf1d2d60dc469ea5a63f01f47ea5b1ce",
"FStar.HyperStack_pretyping_730e633374418435590e5214be2471d4",
"Hacl.Impl.Salsa20_pretyping_a87e903bbc455531fa4b8b47a243ed22",
"assumption_FStar.HyperHeap.HasEq_rid", "b2t_def", "bool_inversion",
"bool_typing", "data_elim_FStar.Buffer.MkBuffer",
"data_elim_FStar.HyperStack.HS", "data_elim_FStar.HyperStack.MkRef",
"data_elim_FStar.UInt32.Mk", "data_elim_Spec.CTR.Mkblock_cipher_ctx",
"equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
"equation_FStar.Buffer.contains", "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.sel",
"equation_FStar.Buffer.sub", "equation_FStar.Ghost.reveal",
"equation_FStar.Heap.emp", "equation_FStar.HyperHeap.t",
"equation_FStar.HyperStack.contains",
"equation_FStar.HyperStack.equal_domains",
"equation_FStar.HyperStack.frameOf",
"equation_FStar.HyperStack.fresh_frame",
"equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_tip",
"equation_FStar.HyperStack.live_region",
"equation_FStar.HyperStack.pop",
"equation_FStar.HyperStack.poppable",
"equation_FStar.HyperStack.popped",
"equation_FStar.HyperStack.remove_elt", "equation_FStar.Mul.op_Star",
"equation_FStar.ST.inline_stack_inv", "equation_FStar.Set.eqtype",
"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.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.n", "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_Hacl.UInt32.t",
"equation_Hacl.UInt8.t", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos", "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.HyperStack.mem",
"fuel_guarded_inversion_FStar.HyperStack.reference",
"fuel_guarded_inversion_FStar.UInt32.t_",
"fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_",
"function_token_typing_FStar.Heap.emp",
"function_token_typing_FStar.Heap.heap",
"function_token_typing_FStar.HyperHeap.rid",
"function_token_typing_FStar.HyperStack.__proj__MkRef__item__id",
"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_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_2_1__",
"lemma_FStar.Buffer.lemma_modifies_3_2_comm",
"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_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.HyperStack.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1",
"lemma_FStar.Seq.Base.lemma_len_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_Multiply",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"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.HyperStack.HS_h",
"proj_equation_FStar.HyperStack.HS_tip",
"proj_equation_FStar.HyperStack.MkRef_id",
"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_incr",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Buffer.MkBuffer_idx",
"projection_inverse_FStar.HyperStack.HS_h",
"projection_inverse_FStar.UInt32.Mk_v",
"projection_inverse_Prims.Mktuple2__1",
"projection_inverse_Prims.Mktuple2__2",
"projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
"projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
"refinement_interpretation_FStar.Buffer_Tm_refine_347cdcabc7e8becd6dd649804986fa75",
"refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
"refinement_interpretation_FStar.Buffer_Tm_refine_8518e8b728e19b2937c780d25ff7abcb",
"refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d",
"refinement_interpretation_FStar.HyperStack_Tm_refine_17c32ea1674222a60392f05cf1ea594b",
"refinement_interpretation_FStar.HyperStack_Tm_refine_4c3d3c35ed77aaa549ae6f40eebffd27",
"refinement_interpretation_FStar.HyperStack_Tm_refine_f724abd6de992fc2f861487694296e1a",
"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_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_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_kinding_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d",
"token_correspondence_FStar.HyperStack.__proj__MkRef__item__id",
"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.Buffer.idx", "typing_FStar.Ghost.reveal",
"typing_FStar.HyperStack.__proj__HS__item__h",
"typing_FStar.HyperStack.__proj__HS__item__tip",
"typing_FStar.HyperStack.poppable",
"typing_FStar.HyperStack.remove_elt", "typing_FStar.HyperStack.sel",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Set.complement",
"typing_FStar.Set.intersect", "typing_FStar.Set.singleton",
"typing_FStar.UInt32.v", "typing_FStar.UInt64.v", "typing_Prims.pow2"
],
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", "equation_FStar.Mul.op_Star",
"equation_FStar.UInt64.n", "equation_FStar.UInt8.t",
"equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt8.t",
"equation_Spec.CTR.block", "equation_Spec.Lib.lbytes",
"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_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_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_Hacl.Impl.Salsa20_Tm_refine_1d668d298fe099f2dd7e1e24c538b64a"
],
0
],
[
"Hacl.Impl.Salsa20.update",
4,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Spec.Lib.uint32s_from_le.fuel_instrumented",
"@query",
"FStar.Map_interpretation_Tm_arrow_d02b23aab265d753a600adf301de862a",
"FStar.Set_interpretation_Tm_arrow_f285bd18d16ed788dea4e9c47fb2243d",
"Hacl.Impl.Salsa20_pretyping_a87e903bbc455531fa4b8b47a243ed22",
"assumption_FStar.HyperHeap.HasEq_rid", "b2t_def", "bool_inversion",
"bool_typing", "data_elim_FStar.Buffer.MkBuffer",
"data_elim_FStar.HyperStack.HS", "data_elim_FStar.HyperStack.MkRef",
"data_elim_FStar.UInt32.Mk", "data_elim_Hacl.Impl.Salsa20.MkLog",
"data_elim_Spec.CTR.Mkblock_cipher_ctx",
"equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
"equation_FStar.Buffer.contains", "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.sel",
"equation_FStar.Buffer.sub", "equation_FStar.Buffer.unused_in",
"equation_FStar.Ghost.reveal", "equation_FStar.Heap.emp",
"equation_FStar.HyperHeap.sel", "equation_FStar.HyperHeap.t",
"equation_FStar.HyperStack.contains",
"equation_FStar.HyperStack.equal_domains",
"equation_FStar.HyperStack.frameOf",
"equation_FStar.HyperStack.fresh_frame",
"equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_tip",
"equation_FStar.HyperStack.live_region",
"equation_FStar.HyperStack.pop",
"equation_FStar.HyperStack.poppable",
"equation_FStar.HyperStack.popped",
"equation_FStar.HyperStack.remove_elt",
"equation_FStar.HyperStack.sel", "equation_FStar.Mul.op_Star",
"equation_FStar.ST.inline_stack_inv", "equation_FStar.Set.eqtype",
"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.uint_t",
"equation_FStar.UInt16.n", "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.n", "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_Hacl.UInt32.t",
"equation_Hacl.UInt32.v", "equation_Hacl.UInt8.t",
"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.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", "equation_Spec.Salsa20.setup",
"equation_Spec.Salsa20.state",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.HyperStack.mem",
"fuel_guarded_inversion_FStar.HyperStack.reference",
"fuel_guarded_inversion_FStar.UInt32.t_",
"fuel_guarded_inversion_FStar.UInt64.t_",
"fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_",
"function_token_typing_FStar.Heap.emp",
"function_token_typing_FStar.Heap.heap",
"function_token_typing_FStar.HyperHeap.rid",
"function_token_typing_FStar.Map.domain",
"function_token_typing_FStar.Set.singleton",
"function_token_typing_FStar.UInt16.n",
"function_token_typing_FStar.UInt8.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_1_trans",
"lemma_FStar.Buffer.lemma_modifies_2_1_",
"lemma_FStar.Buffer.lemma_modifies_2_1__",
"lemma_FStar.Buffer.lemma_modifies_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_1",
"lemma_FStar.Buffer.no_upd_popped",
"lemma_FStar.HyperStack.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1",
"lemma_FStar.Map.lemma_SelRestrict",
"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_Equality",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"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.HyperStack.HS_h",
"proj_equation_FStar.HyperStack.HS_tip",
"proj_equation_FStar.HyperStack.MkRef_id",
"proj_equation_FStar.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.HyperStack.HS_h",
"projection_inverse_FStar.UInt32.Mk_v",
"projection_inverse_FStar.UInt64.Mk_v",
"projection_inverse_Prims.Mktuple2__1",
"projection_inverse_Prims.Mktuple2__2",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Buffer_Tm_refine_347cdcabc7e8becd6dd649804986fa75",
"refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_FStar.HyperStack_Tm_refine_17c32ea1674222a60392f05cf1ea594b",
"refinement_interpretation_FStar.HyperStack_Tm_refine_4c3d3c35ed77aaa549ae6f40eebffd27",
"refinement_interpretation_FStar.HyperStack_Tm_refine_f724abd6de992fc2f861487694296e1a",
"refinement_interpretation_FStar.Int.Cast_Tm_refine_7aa05f464301e3cb4272fba6147da28f",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_FStar.UInt64_Tm_refine_2cdf10a0b17b1e313a0b7d29add2d0a1",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_129089aa650ccd93ce04c3c260485c61",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_1d668d298fe099f2dd7e1e24c538b64a",
"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",
"refinement_interpretation_Spec.Salsa20_Tm_refine_aca10fb50cc7162d8b55c168416f714b",
"refinement_kinding_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d",
"token_correspondence_FStar.Map.domain",
"token_correspondence_FStar.Set.singleton",
"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.length", "typing_FStar.Ghost.reveal",
"typing_FStar.HyperStack.__proj__HS__item__h",
"typing_FStar.HyperStack.__proj__HS__item__tip",
"typing_FStar.HyperStack.__proj__MkRef__item__id",
"typing_FStar.HyperStack.poppable",
"typing_FStar.HyperStack.remove_elt",
"typing_FStar.Int.Cast.uint64_to_uint32",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Mul.op_Star",
"typing_FStar.Seq.Base.index", "typing_FStar.Set.complement",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"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",
"typing_Seq.Create.create_16", "typing_Spec.Lib.uint32s_from_le",
"typing_Spec.Salsa20.salsa20_core", "typing_Spec.Salsa20.setup"
],
0
],
[
"Hacl.Impl.Salsa20.lemma_aux_modifies_2",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.HyperHeap.HasEq_rid", "bool_inversion",
"data_elim_FStar.Buffer.MkBuffer", "equation_FStar.Buffer.buffer",
"equation_FStar.Buffer.contains", "equation_FStar.Buffer.content",
"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.Heap.modifies",
"equation_FStar.HyperHeap.contains_ref",
"equation_FStar.HyperHeap.modifies_just",
"equation_FStar.HyperHeap.modifies_one",
"equation_FStar.HyperHeap.modifies_rref",
"equation_FStar.HyperHeap.t", "equation_FStar.HyperStack.contains",
"equation_FStar.HyperStack.frameOf", "equation_FStar.HyperStack.hh",
"equation_FStar.HyperStack.modifies_one",
"equation_FStar.HyperStack.modifies_ref",
"equation_FStar.Set.eqtype", "equation_FStar.Set.subset",
"equation_Prims.eqtype", "equation_Prims.nat",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.HyperStack.mem",
"fuel_guarded_inversion_FStar.HyperStack.reference",
"function_token_typing_FStar.Heap.heap",
"function_token_typing_FStar.HyperHeap.rid",
"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", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar",
"proj_equation_FStar.Buffer.MkBuffer_content",
"proj_equation_FStar.HyperStack.HS_h",
"proj_equation_FStar.HyperStack.MkRef_id",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_FStar.Buffer_Tm_refine_347cdcabc7e8becd6dd649804986fa75",
"refinement_interpretation_FStar.HyperStack_Tm_refine_f724abd6de992fc2f861487694296e1a",
"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.HyperStack.__proj__HS__item__h",
"typing_FStar.HyperStack.__proj__MkRef__item__id",
"typing_FStar.Map.concat", "typing_FStar.Map.contains",
"typing_FStar.Map.restrict", "typing_FStar.Set.complement",
"typing_FStar.Set.singleton", "typing_FStar.Set.union"
],
0
],
[
"Hacl.Impl.Salsa20.lemma_salsa20_counter_mode_def_0",
1,
0,
0,
[ "@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", "equation_FStar.Mul.op_Star",
"equation_FStar.UInt64.n", "equation_FStar.UInt64.t",
"equation_FStar.UInt64.v", "equation_FStar.UInt8.t",
"equation_Hacl.UInt8.t", "equation_Spec.Salsa20.blocklen",
"equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
"equation_Spec.Salsa20.salsa20_ctx", "primitive_Prims.op_Addition",
"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_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_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_Hacl.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", "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,
0,
[ "@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,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_FStar.Buffer.length", "equation_FStar.Mul.op_Star",
"equation_FStar.UInt.max_int", "equation_FStar.UInt32.t",
"equation_FStar.UInt32.v", "equation_FStar.UInt64.n",
"equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
"equation_FStar.UInt8.t", "equation_Hacl.UInt8.t",
"equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.blocklen",
"equation_Spec.Salsa20.key", "equation_Spec.Salsa20.keylen",
"equation_Spec.Salsa20.noncelen",
"equation_Spec.Salsa20.salsa20_ctx",
"function_token_typing_Spec.Salsa20.salsa20_ctx",
"kinding_FStar.UInt8.t_@tok", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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_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_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d1c0e169fc4293dab4521305058ce328",
"typing_FStar.Seq.Base.length",
"typing_Spec.CTR.__proj__Mkblock_cipher_ctx__item__counterbits"
],
0
],
[
"Hacl.Impl.Salsa20.salsa20_counter_mode_blocks",
4,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_correspondence_Spec.CTR.counter_mode_blocks.fuel_instrumented",
"@fuel_correspondence_Spec.Loops.seq_map2.fuel_instrumented",
"@query",
"FStar.HyperStack_pretyping_730e633374418435590e5214be2471d4",
"b2t_def", "bool_inversion", "bool_typing",
"data_elim_FStar.Buffer.MkBuffer", "data_elim_FStar.UInt32.Mk",
"eq2-interp", "equation_FStar.Buffer.as_seq",
"equation_FStar.Buffer.buffer", "equation_FStar.Buffer.contains",
"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.sel", "equation_FStar.Buffer.sub",
"equation_FStar.Ghost.reveal", "equation_FStar.HyperHeap.t",
"equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_in",
"equation_FStar.Mul.op_Star", "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.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.state",
"equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt32.t",
"equation_Hacl.UInt8.t", "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.HyperStack.mem",
"fuel_guarded_inversion_FStar.HyperStack.reference",
"fuel_guarded_inversion_FStar.UInt32.t_",
"fuel_guarded_inversion_FStar.UInt64.t_",
"function_token_typing_FStar.HyperHeap.root",
"function_token_typing_FStar.UInt64.n",
"function_token_typing_Spec.Salsa20.constant2", "int_inversion",
"int_typing",
"interpretation_Hacl.Impl.Salsa20_Tm_abs_bf9040e167887aa90eb7a5fc4aa6f6c2",
"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_size", "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",
"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_idx",
"proj_equation_FStar.Buffer.MkBuffer_length",
"proj_equation_FStar.Buffer.MkBuffer_max_length",
"proj_equation_FStar.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.UInt32.Mk_v",
"projection_inverse_Prims.Mktuple2__1",
"projection_inverse_Prims.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_347cdcabc7e8becd6dd649804986fa75",
"refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
"refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_FStar.Buffer_Tm_refine_ba56e54aa82f2631b0e7a66e112023c8",
"refinement_interpretation_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d",
"refinement_interpretation_FStar.HyperStack_Tm_refine_f724abd6de992fc2f861487694296e1a",
"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.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_0de213661af4524df5c2ffb01c96de98",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_13fe60d1a58ee3ca21c0a22cb56aa0c4",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_48e1d639f7bfe20139b9a08d7ef9c41f",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_4ab2e194b59a9877b8ec5be853390d54",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_60a3cbff79c8123cece9cf1ac707c385",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_679e5a489c5f6bbaf25cc86648fed51b",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_685f257d77150ce5845a6cf52a449fb9",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_75fe8a65f5666eaf920693fe19efc919",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_7ba7dce0ca667ccfc5ad984d79f2f52d",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_7ef6588018260ed3205c9e2f80e9a646",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_82db053939908f699a97088907080433",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_ca2c77f69acff4fca0b44c61a9e317a7",
"refinement_interpretation_Hacl.Impl.Salsa20_Tm_refine_d1c0e169fc4293dab4521305058ce328",
"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",
"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.__proj__MkBuffer__item__max_length",
"typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.idx",
"typing_FStar.Buffer.length",
"typing_FStar.HyperStack.__proj__HS__item__h",
"typing_FStar.HyperStack.is_in", "typing_FStar.HyperStack.sel",
"typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.Mul.op_Star",
"typing_FStar.Seq.Base.createEmpty", "typing_FStar.Seq.Base.slice",
"typing_FStar.UInt32.__proj__Mk__item__v", "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", "@query", "equation_FStar.Buffer.length",
"equation_FStar.Mul.op_Star", "equation_FStar.UInt64.n",
"equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
"equation_FStar.UInt8.t", "equation_Hacl.UInt8.t",
"equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.keylen",
"equation_Spec.Salsa20.noncelen",
"equation_Spec.Salsa20.salsa20_ctx", "primitive_Prims.op_Addition",
"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_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_Hacl.Impl.Salsa20_Tm_refine_0aaf78738bfac8fed3c5ec5ff4dc12d2"
],
0
],
[
"Hacl.Impl.Salsa20.salsa20_counter_mode",
4,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_correspondence_Spec.CTR.counter_mode_blocks.fuel_instrumented",
"@query",
"FStar.Ghost_interpretation_Tm_arrow_f529f4c9cbc78ef050cefd8cf570168e",
"FStar.HyperStack_pretyping_730e633374418435590e5214be2471d4",
"b2t_def", "bool_inversion", "bool_typing",
"data_elim_FStar.Buffer.MkBuffer",
"data_elim_FStar.HyperStack.MkRef", "data_elim_FStar.UInt32.Mk",
"data_elim_Hacl.Impl.Salsa20.MkLog", "equation_FStar.Buffer.as_seq",
"equation_FStar.Buffer.buffer", "equation_FStar.Buffer.contains",
"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.sel", "equation_FStar.Buffer.sub",
"equation_FStar.Ghost.reveal", "equation_FStar.Mul.op_Star",
"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.uint_t",
"equation_FStar.UInt32.add", "equation_FStar.UInt32.gt",
"equation_FStar.UInt32.logand", "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_Hacl.UInt32.t",
"equation_Hacl.UInt8.t", "equation_Prims.nat",
"equation_Spec.CTR.counter_mode", "equation_Spec.CTR.xor",
"equation_Spec.Lib.lbytes", "equation_Spec.Salsa20.block",
"equation_Spec.Salsa20.blocklen", "equation_Spec.Salsa20.constant2",
"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",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.HyperStack.mem",
"fuel_guarded_inversion_FStar.HyperStack.reference",
"fuel_guarded_inversion_FStar.UInt32.t_",
"fuel_guarded_inversion_Hacl.Impl.Salsa20.log_t_",
"function_token_typing_FStar.UInt64.n",
"function_token_typing_Spec.Salsa20.constant2",
"function_token_typing_Spec.Salsa20.salsa20_block", "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_size", "lemma_FStar.Buffer.lemma_sub_spec",
"lemma_FStar.Buffer.modifies_subbuffer_2",
"lemma_FStar.Buffer.no_upd_lemma_2",
"lemma_FStar.HyperStack.lemma_equal_domains_trans",
"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",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan",
"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.HyperStack.MkRef_id",
"proj_equation_FStar.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_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.UInt32.Mk_v",
"projection_inverse_Prims.Mktuple2__1",
"projection_inverse_Prims.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_347cdcabc7e8becd6dd649804986fa75",
"refinement_interpretation_FStar.Buffer_Tm_refine_811063936efbc06568ec405d75452cb9",
"refinement_interpretation_FStar.Buffer_Tm_refine_8518e8b728e19b2937c780d25ff7abcb",
"refinement_interpretation_FStar.Buffer_Tm_refine_8ba095f5457984257bc763075993de75",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d",
"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.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_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_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"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.__proj__MkBuffer__item__max_length",
"typing_FStar.Buffer.as_seq", "typing_FStar.Buffer.idx",
"typing_FStar.Buffer.length", "typing_FStar.Ghost.reveal",
"typing_FStar.HyperStack.sel",
"typing_FStar.Int.Cast.uint32_to_uint64", "typing_FStar.Mul.op_Star",
"typing_FStar.Seq.Base.createEmpty", "typing_FStar.Seq.Base.slice",
"typing_FStar.UInt32.v", "typing_FStar.UInt64.v",
"typing_Spec.CTR.xor", "unit_typing"
],
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", "equation_FStar.Buffer.length",
"equation_FStar.Mul.op_Star", "equation_FStar.UInt64.n",
"equation_FStar.UInt64.t", "equation_FStar.UInt64.v",
"equation_FStar.UInt8.t", "equation_Hacl.Impl.Salsa20.uint8_p",
"equation_Hacl.UInt8.t", "equation_Spec.Salsa20.blocklen",
"equation_Spec.Salsa20.keylen", "equation_Spec.Salsa20.noncelen",
"equation_Spec.Salsa20.salsa20_ctx", "primitive_Prims.op_Addition",
"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_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_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",
"FStar.HyperStack_interpretation_Tm_arrow_44cc1777afbdbed9bdd3d9b2ecbc41b2",
"FStar.HyperStack_interpretation_Tm_arrow_bf1d2d60dc469ea5a63f01f47ea5b1ce",
"FStar.HyperStack_pretyping_730e633374418435590e5214be2471d4",
"assumption_FStar.HyperHeap.HasEq_rid", "bool_inversion",
"data_elim_FStar.Buffer.MkBuffer", "data_elim_FStar.HyperStack.HS",
"equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
"equation_FStar.Buffer.contains", "equation_FStar.Buffer.content",
"equation_FStar.Buffer.equal", "equation_FStar.Buffer.frameOf",
"equation_FStar.Buffer.live", "equation_FStar.Buffer.sel",
"equation_FStar.Buffer.unmapped_in", "equation_FStar.Heap.emp",
"equation_FStar.HyperHeap.sel", "equation_FStar.HyperHeap.t",
"equation_FStar.HyperStack.contains",
"equation_FStar.HyperStack.equal_domains",
"equation_FStar.HyperStack.frameOf",
"equation_FStar.HyperStack.fresh_frame",
"equation_FStar.HyperStack.hh", "equation_FStar.HyperStack.is_tip",
"equation_FStar.HyperStack.live_region",
"equation_FStar.HyperStack.pop",
"equation_FStar.HyperStack.poppable",
"equation_FStar.HyperStack.popped",
"equation_FStar.HyperStack.remove_elt",
"equation_FStar.HyperStack.sel",
"equation_FStar.ST.inline_stack_inv", "equation_FStar.Set.eqtype",
"equation_FStar.UInt32.t", "equation_FStar.UInt8.t",
"equation_Hacl.Impl.Salsa20.h32", "equation_Hacl.Impl.Salsa20.state",
"equation_Hacl.Impl.Salsa20.uint8_p", "equation_Hacl.UInt32.t",
"equation_Hacl.UInt8.t", "equation_Prims.eqtype",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.HyperStack.mem",
"fuel_guarded_inversion_FStar.HyperStack.reference",
"function_token_typing_FStar.Heap.emp",
"function_token_typing_FStar.Heap.heap",
"function_token_typing_FStar.HyperHeap.rid",
"function_token_typing_FStar.HyperStack.__proj__MkRef__item__id",
"function_token_typing_FStar.HyperStack.remove_elt",
"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.HyperStack.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1",
"lemma_FStar.Map.lemma_SelRestrict",
"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.HyperStack.HS_h",
"proj_equation_FStar.HyperStack.HS_tip",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_FStar.HyperStack.HS_h",
"refinement_interpretation_FStar.HyperStack_Tm_refine_17c32ea1674222a60392f05cf1ea594b",
"refinement_interpretation_FStar.HyperStack_Tm_refine_4c3d3c35ed77aaa549ae6f40eebffd27",
"refinement_interpretation_FStar.HyperStack_Tm_refine_f724abd6de992fc2f861487694296e1a",
"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",
"refinement_kinding_FStar.Buffer_Tm_refine_cdfdd8eed51fd09dfdab5bde10aa9e9d",
"token_correspondence_FStar.HyperStack.__proj__MkRef__item__id",
"token_correspondence_FStar.HyperStack.remove_elt",
"typing_FStar.Buffer.__proj__MkBuffer__item__content",
"typing_FStar.HyperStack.__proj__HS__item__h",
"typing_FStar.HyperStack.__proj__HS__item__tip",
"typing_FStar.HyperStack.poppable", "typing_FStar.Map.contains",
"typing_FStar.Map.domain", "typing_FStar.Set.complement",
"typing_FStar.Set.singleton"
],
0
]
]
]