Revision aa1ca8698adfe929a9eff86ac143eaf90fc3e8ee authored by Jay Bosamiya on 03 June 2019, 21:51:38 UTC, committed by Jay Bosamiya on 03 June 2019, 21:51:38 UTC
1 parent 6055e85
Hacl.Bignum25519.fst.hints
[
"\u0007\u0016�\u0012��ݹ\f��x\fBe",
[
[
"Hacl.Bignum25519.mask_51",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"afc7102605d433c6c45a4941b876442e"
],
[
"Hacl.Bignum25519.make_u64_5",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies1", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"12a4594c1a89484921a35bf6e7472e47"
],
[
"Hacl.Bignum25519.make_u64_10",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies1", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt.max_int",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.length",
"typing_Lib.Buffer.loc", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"33831c0ba1da28f2028149a8c4388b75"
],
[
"Hacl.Bignum25519.make_u128_9",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies1", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint128",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint128",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt.max_int",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.length",
"typing_Lib.Buffer.loc", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"4dfdda1c22403531a9021990d5b1d6f2"
],
[
"Hacl.Bignum25519.make_zero",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies1", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"9fd696ac85df0c824ce979e78dbe233c"
],
[
"Hacl.Bignum25519.make_one",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies1", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt.max_int",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.length",
"typing_Lib.Buffer.loc", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"d831aadc5a25718b5843c77a2d1f56dd"
],
[
"Hacl.Bignum25519.fcontract_first_carry_pass",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Bignum25519.felem",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_92eedd657384b0981bcfc64b33308eaf",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.length",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"bc388db65b9f1ddb12ceec59a369b432"
],
[
"Hacl.Bignum25519.carry_top",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Bignum25519.felem",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.shiftval",
"equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_92eedd657384b0981bcfc64b33308eaf",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.length",
"typing_Lib.Buffer.loc", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"180788c2e5552389f52d2cb3a5d2a5a3"
],
[
"Hacl.Bignum25519.carry_0_to_1",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Bignum25519.felem",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies", "equation_Lib.Buffer.modifies1",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.shiftval",
"equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint_t",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_92eedd657384b0981bcfc64b33308eaf",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt.max_int",
"typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"fee82aceb0c31ae333386bfcc8437716"
],
[
"Hacl.Bignum25519.reduce_513_",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Bignum25519.felem", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.IntTypes.uint64",
"function_token_typing_Lib.IntTypes.uint64",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_Lib.Buffer.loc", "typing_tok_Lib.Buffer.MUT@tok"
],
0,
"c8f22a88250c6de8780b895537eaf073"
],
[
"Hacl.Bignum25519.fdifference_reduced",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Bignum25519.felem", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.IntTypes.uint64",
"function_token_typing_Lib.IntTypes.uint64",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"refinement_interpretation_Tm_refine_289bd5094ffa8f21f0af231e7fa0ac18",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_Lib.Buffer.loc", "typing_tok_Lib.Buffer.MUT@tok"
],
0,
"4e232ca34d18d0a0dead2b1c9d5c1628"
],
[
"Hacl.Bignum25519.fcontract_first_carry_full",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Bignum25519.felem", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.IntTypes.uint64",
"function_token_typing_Lib.IntTypes.uint64",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_Lib.Buffer.loc", "typing_tok_Lib.Buffer.MUT@tok"
],
0,
"daf2dc5f92773765025c3cd1940d3dcf"
],
[
"Hacl.Bignum25519.fcontract_second_carry_pass",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Bignum25519.felem",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_92eedd657384b0981bcfc64b33308eaf",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.length",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"9119cf1bb6c4f7ec029b6e9deac181b4"
],
[
"Hacl.Bignum25519.fcontract_second_carry_full",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Bignum25519.felem", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.IntTypes.uint64",
"function_token_typing_Lib.IntTypes.uint64",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_Lib.Buffer.loc", "typing_tok_Lib.Buffer.MUT@tok"
],
0,
"2eef7a58562dac8cf12f3a56ef0579e7"
],
[
"Hacl.Bignum25519.fcontract_trim",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Bignum25519.felem",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.length", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"c06c452a9a1f17edf6ea19577a7cafe4"
],
[
"Hacl.Bignum25519.reduce_",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Bignum25519.felem", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.IntTypes.uint64",
"function_token_typing_Lib.IntTypes.uint64",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_Lib.Buffer.loc", "typing_tok_Lib.Buffer.MUT@tok"
],
0,
"c32bcc9405d794e5b6babb786f4e816c"
],
[
"Hacl.Bignum25519.times_2",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Bignum25519.felem",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3167e2cb65f6f5f927c17d6009e974fd",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.length", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"ba679955909def2c42c3ef8eff254d67"
],
[
"Hacl.Bignum25519.times_d",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Bignum25519.felem",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies1",
"equation_Lib.Buffer.stack_allocated", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_3167e2cb65f6f5f927c17d6009e974fd",
"refinement_interpretation_Tm_refine_840ea2c2f11b3d5267d3b714b8f12c1c",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ae181f81ea078eac3cd0bf9c8bd0800b",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"0c4316c6031481cf331c6787547f9950"
],
[
"Hacl.Bignum25519.times_2d",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Bignum25519.felem",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.live",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.modifies1",
"equation_Lib.Buffer.stack_allocated", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_3167e2cb65f6f5f927c17d6009e974fd",
"refinement_interpretation_Tm_refine_840ea2c2f11b3d5267d3b714b8f12c1c",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ae181f81ea078eac3cd0bf9c8bd0800b",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"c763dc036def244f82df5bdee6bd0e03"
],
[
"Hacl.Bignum25519.fsquare_times",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Bignum25519.felem",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.op_Bar_Plus_Bar",
"equation_Lib.Buffer.stack_allocated", "equation_Lib.Buffer.union",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.uint128", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint128",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_289bd5094ffa8f21f0af231e7fa0ac18",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_840ea2c2f11b3d5267d3b714b8f12c1c",
"refinement_interpretation_Tm_refine_99b943ceb49895b829e5a4b967e90f94",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
"typing_Lib.Buffer.op_Bar_Plus_Bar",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"e248143308d5da51627ca921bf4d2bae"
],
[
"Hacl.Bignum25519.fsquare_times_inplace",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.Monotonic.HyperHeap.Mod_set_def", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.HyperStack.ST.inline_stack_inv",
"equation_FStar.Monotonic.Heap.equal_dom",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.Monotonic.HyperStack.pop",
"equation_FStar.Monotonic.HyperStack.poppable",
"equation_FStar.Monotonic.HyperStack.popped",
"equation_FStar.Monotonic.HyperStack.remove_elt",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Bignum25519.felem",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.live", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.op_Bar_Plus_Bar",
"equation_Lib.Buffer.stack_allocated", "equation_Lib.Buffer.union",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.uint128", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint128",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int", "function_token_typing_Prims.nat",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_elim",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_all_regions_intro",
"lemma_FStar.HyperStack.ST.lemma_same_refs_in_non_tip_regions_elim",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomRestrict",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.Map.lemma_InDomUpd2",
"lemma_FStar.Map.lemma_SelRestrict", "lemma_FStar.Map.lemma_SelUpd2",
"lemma_FStar.Map.lemma_UpdDomain",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_FStar.Set.lemma_equal_intro",
"lemma_FStar.Set.mem_complement", "lemma_FStar.Set.mem_intersect",
"lemma_FStar.Set.mem_singleton", "lemma_FStar.Set.mem_subset",
"lemma_FStar.Set.mem_union", "lemma_FStar.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_loc_not_unused_in",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_addresses_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_addresses_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_none",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_buffer_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region",
"lemma_LowStar.Monotonic.Buffer.loc_includes_region_region_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_trans_backwards",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_remove_fresh_frame",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"lemma_LowStar.Monotonic.Buffer.popped_modifies",
"lemma_LowStar.Monotonic.Buffer.unused_in_loc_unused_in",
"lemma_LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_840ea2c2f11b3d5267d3b714b8f12c1c",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_b75e3be8b6cdfeeba9fe9a39af9ce044",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.mod_set",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_rid_ctr",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.mem",
"typing_FStar.Set.singleton", "typing_FStar.Set.union",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
"typing_Lib.Buffer.op_Bar_Plus_Bar",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.as_addr",
"typing_LowStar.Monotonic.Buffer.frameOf",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_addresses",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"7563742ce232c8f9725f7c49e9eea32f"
],
[
"Hacl.Bignum25519.inverse",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.fresh_frame",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Hacl.Bignum25519.felem",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Map.lemma_InDomUpd1", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.length", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"4daaa245e965a53bfd12c206434b5932"
],
[
"Hacl.Bignum25519.load_51",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.shiftval",
"equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
"lemma_Lib.IntTypes.size_v_size_lemma",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0a44a9c52461f7b29dab1fe1db7afc62",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_92eedd657384b0981bcfc64b33308eaf",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_b5566223946423fb6df2a0b969ca1865",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_Lib.Buffer.length", "typing_Lib.IntTypes.bits",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"aee75bb5331309f8c5e825d9fadf3a72"
],
[
"Hacl.Bignum25519.store_4",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.gsub", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.Buffer.loc",
"equation_Lib.Buffer.modifies", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_FStar.HyperStack.ST.lemma_equal_domains_trans",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.pow2_values",
"lemma_Lib.IntTypes.size_v_size_lemma",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0a44a9c52461f7b29dab1fe1db7afc62",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_7d28454cc602c65d0baeea87f419a4fa",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
"typing_Lib.IntTypes.bits", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"184714a07fba5cd76513f98d0f3a516a"
],
[
"Hacl.Bignum25519.store_51",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_tip",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.shiftval",
"equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.uint8",
"equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_92eedd657384b0981bcfc64b33308eaf",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ae4a6baeaf1394055bb285cab3ef371b",
"refinement_interpretation_Tm_refine_b5566223946423fb6df2a0b969ca1865",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.uint_to_t",
"typing_FStar.UInt32.v", "typing_Lib.Buffer.length",
"typing_Lib.IntTypes.bits", "typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"0ed8f785efe20f048d480bf490195b3e"
]
]
]
Computing file changes ...
