Revision 3f979cc1cb15a4491f8b804bbafeabeffe5a1ab1 authored by Aseem Rastogi on 09 April 2019, 11:31:34 UTC, committed by Aseem Rastogi on 09 April 2019, 11:31:34 UTC
1 parent 74a8710
Hacl.Impl.Curve25519.Finv.fst.hints
[
"?�xC\u001aGu���+ݗ�8�",
[
[
"Hacl.Impl.Curve25519.Finv.fsquare_times_inv",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_Hacl.Impl.Curve25519.Fields.M51",
"disc_equation_Hacl.Impl.Curve25519.Fields.M64",
"equality_tok_Lib.Buffer.MUT@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_Hacl.Impl.Curve25519.Fields.felem",
"equation_Lib.Buffer.lbuffer_t",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"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"
],
0,
"f685faa8e36efbb155dd2738d272f11b"
],
[
"Hacl.Impl.Curve25519.Finv.fsqr_s",
1,
2,
1,
[ "@query" ],
0,
"a86815e7db50ae18ec2df4d4e3e4b9a5"
],
[
"Hacl.Impl.Curve25519.Finv.fsqr_s",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Hacl.Impl.Curve25519.Fields.M51",
"disc_equation_Hacl.Impl.Curve25519.Fields.M64",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@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.Impl.Curve25519.Field51.as_felem",
"equation_Hacl.Impl.Curve25519.Field51.felem_fits",
"equation_Hacl.Impl.Curve25519.Field51.fevalh",
"equation_Hacl.Impl.Curve25519.Field51.mul_inv_t",
"equation_Hacl.Impl.Curve25519.Field64.Core.fevalh",
"equation_Hacl.Impl.Curve25519.Fields.as_nat",
"equation_Hacl.Impl.Curve25519.Fields.felem",
"equation_Hacl.Impl.Curve25519.Fields.felem_wide",
"equation_Hacl.Impl.Curve25519.Fields.feval",
"equation_Hacl.Impl.Curve25519.Finv.fsquare_times_inv",
"equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1",
"equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5",
"equation_Hacl.Spec.Curve25519.Field51.Definition.max51",
"equation_Hacl.Spec.Curve25519.Field51.mul_inv_t",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union",
"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.nat",
"equation_Prims.pos",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
"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__",
"int_inversion", "int_typing", "l_and-interp",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__5",
"refinement_interpretation_Tm_refine_6b804acad6c47a08aeb8f504b73f942b",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a15bbcba47d15796626b088bbeee51de",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"refinement_interpretation_Tm_refine_ca3c25188b8dc280e8f5a658bfdd7c9b",
"refinement_interpretation_Tm_refine_ce5b59a5dee91f7ed09b53e8e3b4b20a",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_FStar.UInt32.v",
"typing_Hacl.Spec.Curve25519.Field51.Definition.max51",
"typing_Hacl.Spec.Curve25519.Field51.Definition.pow51",
"typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_X64.CPU_Features_s.adx_enabled",
"typing_X64.CPU_Features_s.bmi2_enabled",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"74929ee74c31e2b3c1047e32e6958a7c"
],
[
"Hacl.Impl.Curve25519.Finv.fmuls_pre",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"disc_equation_Hacl.Impl.Curve25519.Fields.M51",
"disc_equation_Hacl.Impl.Curve25519.Fields.M64",
"equality_tok_Lib.Buffer.MUT@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_Hacl.Impl.Curve25519.Fields.felem",
"equation_Lib.Buffer.lbuffer_t",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
"function_token_typing_FStar.Monotonic.Heap.heap",
"lemma_FStar.Map.lemma_ContainsDom",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"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"
],
0,
"a975a872baf092a82872f4ed90a3e1a6"
],
[
"Hacl.Impl.Curve25519.Finv.fmul_s",
1,
2,
1,
[ "@query" ],
0,
"3ea36c2ef6880c3335207d35ff17faed"
],
[
"Hacl.Impl.Curve25519.Finv.fmul_s",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Lib.IntTypes_interpretation_Tm_arrow_69980de4b69ce434f89b12e4cb716d05",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Hacl.Impl.Curve25519.Fields.M51",
"disc_equation_Hacl.Impl.Curve25519.Fields.M64",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.SEC@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.Impl.Curve25519.Field51.as_felem",
"equation_Hacl.Impl.Curve25519.Field51.felem_fits",
"equation_Hacl.Impl.Curve25519.Field51.fevalh",
"equation_Hacl.Impl.Curve25519.Field51.mul_inv_t",
"equation_Hacl.Impl.Curve25519.Field64.Core.fevalh",
"equation_Hacl.Impl.Curve25519.Fields.as_nat",
"equation_Hacl.Impl.Curve25519.Fields.felem",
"equation_Hacl.Impl.Curve25519.Fields.felem_wide2",
"equation_Hacl.Impl.Curve25519.Fields.feval",
"equation_Hacl.Impl.Curve25519.Finv.fmuls_pre",
"equation_Hacl.Impl.Curve25519.Finv.fsquare_times_inv",
"equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits1",
"equation_Hacl.Spec.Curve25519.Field51.Definition.felem_fits5",
"equation_Hacl.Spec.Curve25519.Field51.Definition.max51",
"equation_Hacl.Spec.Curve25519.Field51.mul_inv_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.op_Bar_Plus_Bar", "equation_Lib.Buffer.union",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.op_Plus_Dot",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.uint128", "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",
"equation_Prims.pos",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.add_mod",
"function_token_typing_Lib.IntTypes.uint128",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "l_and-interp",
"lemma_FStar.Map.lemma_ContainsDom", "lemma_FStar.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv", "lemma_Lib.IntTypes.add_mod_lemma",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.loc_includes_union_l_",
"lemma_LowStar.Monotonic.Buffer.loc_union_comm",
"lemma_LowStar.Monotonic.Buffer.modifies_loc_includes",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__4",
"projection_inverse_FStar.Pervasives.Native.Mktuple5__5",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_7fe6111180fe8e3cd3731b2f51635491",
"refinement_interpretation_Tm_refine_8a918203fe2e74ec3fb4116578424a94",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a15bbcba47d15796626b088bbeee51de",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"refinement_interpretation_Tm_refine_f3b200c54a27304abddc91d4bfaa6f2b",
"token_correspondence_Lib.IntTypes.add_mod",
"token_correspondence_Lib.IntTypes.op_Plus_Dot",
"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_Hacl.Spec.Curve25519.Field51.Definition.max51",
"typing_Hacl.Spec.Curve25519.Field51.Definition.pow51",
"typing_Lib.Buffer.length", "typing_Lib.Buffer.loc",
"typing_Lib.Buffer.op_Bar_Plus_Bar",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_X64.CPU_Features_s.adx_enabled",
"typing_X64.CPU_Features_s.bmi2_enabled",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"0ea8e374ed23ae8e6111055d77d0a7ae"
],
[
"Hacl.Impl.Curve25519.Finv.fsquare_times_",
1,
2,
1,
[ "@query" ],
0,
"9af9df4a4ce6aec362dd1913e73b7a3e"
],
[
"Hacl.Impl.Curve25519.Finv.fsquare_times_",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
"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_Hacl.Impl.Curve25519.Fields.felem",
"equation_Hacl.Impl.Curve25519.Fields.felem_wide",
"equation_Hacl.Impl.Curve25519.Finv.fsquare_times_inv",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.op_Subtraction_Bang",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.uint128", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
"equation_LowStar.Buffer.buffer", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
"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__",
"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_Lib.IntTypes.sub_lemma",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"lemma_LowStar.Monotonic.Buffer.modifies_trans_linear",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
"refinement_interpretation_Tm_refine_1580bc5dc4014e45b099bcbe769deb7b",
"refinement_interpretation_Tm_refine_475ff7eb8bf7fe3c3ef9391f1b4f7592",
"refinement_interpretation_Tm_refine_51088e5977aadb578dd4eeb699a6f9c4",
"refinement_interpretation_Tm_refine_52008963f9c27294f4f19c787e5c1411",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_961f6f8ae4e1f44a35c50230f5decf42",
"refinement_interpretation_Tm_refine_9702ab95cfa331008cb31d9e91b297df",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_a505e2c51057febbd6fbabb2d0647ff2",
"refinement_interpretation_Tm_refine_b97caa1fc4a5fb85628d4b1566e4594b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_Lib.IntTypes.op_Subtraction_Bang",
"token_correspondence_Lib.IntTypes.sub", "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.loc",
"typing_Lib.Buffer.union", "typing_Lib.IntTypes.uint_v",
"typing_LowStar.Buffer.trivial_preorder", "typing_Prims.pow2",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"751953f0c34aec7316c32c614733a2db"
],
[
"Hacl.Impl.Curve25519.Finv.fsquare_times",
1,
2,
1,
[ "@query" ],
0,
"c1763b158180e5fdf3b5e7d0aa671814"
],
[
"Hacl.Impl.Curve25519.Finv.fsquare_times",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Hacl.Impl.Curve25519.Fields.M51",
"disc_equation_Hacl.Impl.Curve25519.Fields.M64",
"equality_tok_Hacl.Impl.Curve25519.Fields.M51@tok",
"equality_tok_Hacl.Impl.Curve25519.Fields.M64@tok",
"equality_tok_Lib.Buffer.MUT@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_Hacl.Impl.Curve25519.Fields.felem",
"equation_Hacl.Impl.Curve25519.Fields.felem_wide",
"equation_Hacl.Impl.Curve25519.Finv.fsquare_times_inv",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.loc", "equation_Lib.IntTypes.uint128",
"equation_Lib.IntTypes.uint64",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint128",
"function_token_typing_Lib.IntTypes.uint64",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_Lib.Buffer.modifies_preserves_live",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_065528c86c57fcefee742b1d674df8be",
"refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
"refinement_interpretation_Tm_refine_51088e5977aadb578dd4eeb699a6f9c4",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_b85c206e38ca319dc7709bc452abc53d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"true_interp", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_Lib.Buffer.loc",
"typing_Lib.Buffer.op_Bar_Plus_Bar", "typing_tok_Lib.Buffer.MUT@tok"
],
0,
"1211ef48f63093a8cf1b58b2a9ad2742"
],
[
"Hacl.Impl.Curve25519.Finv.finv0",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"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.U128@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_FStar.Monotonic.HyperHeap.hmap",
"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.Impl.Curve25519.Fields.felem",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.length", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.op_Star_Bang",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.uint128", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.uint_t", "equation_Lib.IntTypes.uint_v",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Prims.pos",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
"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.UInt32.vu_inv",
"lemma_Lib.IntTypes.mul_lemma", "lemma_Lib.IntTypes.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
"refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
"refinement_interpretation_Tm_refine_449ba593891ef077b0c39a9c30aa1294",
"refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"refinement_interpretation_Tm_refine_e07d49bf7ed472bccb081418af1bddb0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"token_correspondence_Lib.IntTypes.mul",
"token_correspondence_Lib.IntTypes.op_Star_Bang",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Map.contains", "typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"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", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"39a7c74d5f59e89993ca9d7120705ca0"
],
[
"Hacl.Impl.Curve25519.Finv.finv0",
2,
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.U1",
"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.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Hacl.Impl.Curve25519.Fields.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.Monotonic.Buffer.length", "equation_Prims.nat",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
"function_token_typing_Lib.IntTypes.uint64",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"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_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"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,
"d3b56d8c55c82240d83058c1f4113270"
],
[
"Hacl.Impl.Curve25519.Finv.finv0",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Hacl.Impl.Curve25519.Fields.M51@tok",
"equality_tok_Hacl.Impl.Curve25519.Fields.M64@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U128@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_Hacl.Impl.Curve25519.Field51.as_nat",
"equation_Hacl.Impl.Curve25519.Field51.felem_fits",
"equation_Hacl.Impl.Curve25519.Field64.Core.as_nat",
"equation_Hacl.Impl.Curve25519.Fields.as_nat",
"equation_Hacl.Impl.Curve25519.Fields.felem",
"equation_Hacl.Impl.Curve25519.Fields.felem_wide2",
"equation_Hacl.Impl.Curve25519.Fields.feval",
"equation_Hacl.Impl.Curve25519.Finv.fmuls_pre",
"equation_Hacl.Impl.Curve25519.Finv.fsquare_times_inv",
"equation_Hacl.Spec.Curve25519.Finv.finv0",
"equation_Hacl.Spec.Curve25519.Finv.fsquare_times",
"equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.gsub",
"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.union",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.op_Plus_Dot",
"equation_Lib.IntTypes.op_Star_Bang",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.uint128", "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.l_True",
"equation_Prims.logical", "equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul",
"fuel_guarded_inversion_FStar.Pervasives.Native.tuple2",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
"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__",
"int_inversion", "int_typing",
"interpretation_Tm_abs_2d4a1d05236e82a428a71813e1ca9661",
"l_and-interp",
"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.add_mod_lemma", "lemma_Lib.IntTypes.mul_lemma",
"lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"lemma_LowStar.Monotonic.Buffer.length_null_1",
"lemma_LowStar.Monotonic.Buffer.length_null_2",
"lemma_LowStar.Monotonic.Buffer.live_gsub",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_union_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r_",
"lemma_LowStar.Monotonic.Buffer.loc_includes_refl",
"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_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer_weak",
"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_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_06cfcb127be76f1e2de3e2fbe462beb0",
"refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
"refinement_interpretation_Tm_refine_17ae54512d74dca5cf8551d4fcdd291d",
"refinement_interpretation_Tm_refine_1bc5af098f09030db44fed0be1424962",
"refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
"refinement_interpretation_Tm_refine_28126c3229332b283e908c1fa6d2bdda",
"refinement_interpretation_Tm_refine_369d61bb384f6181cd6f792cf86a5d86",
"refinement_interpretation_Tm_refine_449ba593891ef077b0c39a9c30aa1294",
"refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
"refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
"refinement_interpretation_Tm_refine_51088e5977aadb578dd4eeb699a6f9c4",
"refinement_interpretation_Tm_refine_651efe5f33512cba7dd578af110e437e",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_6e0752342dfed3b3058e56e9396850f5",
"refinement_interpretation_Tm_refine_8a918203fe2e74ec3fb4116578424a94",
"refinement_interpretation_Tm_refine_92de0ce42220c9145ec8da27261df8f0",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_a505e2c51057febbd6fbabb2d0647ff2",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"refinement_interpretation_Tm_refine_d7282577b344258eb4de4fb6a801cae7",
"refinement_interpretation_Tm_refine_e07d49bf7ed472bccb081418af1bddb0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_f16347476b439776210c3eceabc4f49d",
"refinement_interpretation_Tm_refine_fb1be1d1726d5678dace30d0f3d47eff",
"token_correspondence_Lib.IntTypes.add_mod",
"token_correspondence_Lib.IntTypes.mul",
"token_correspondence_Lib.IntTypes.op_Plus_Dot",
"token_correspondence_Lib.IntTypes.op_Star_Bang",
"token_correspondence_Prims.pow2.fuel_instrumented", "true_interp",
"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_Hacl.Impl.Curve25519.Fields.feval",
"typing_Hacl.Spec.Curve25519.Finv.fsquare_times",
"typing_Hacl.Spec.Curve25519.Finv.pow", "typing_Lib.Buffer.length",
"typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar",
"typing_Lib.IntTypes.uint_v",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.address_liveness_insensitive_locs",
"typing_LowStar.Monotonic.Buffer.len",
"typing_LowStar.Monotonic.Buffer.loc_buffer",
"typing_LowStar.Monotonic.Buffer.mgsub",
"typing_Spec.Curve25519.fmul",
"typing_tok_Hacl.Impl.Curve25519.Fields.M51@tok",
"typing_tok_Hacl.Impl.Curve25519.Fields.M64@tok",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"dfc7d49d65dbeaec93fa2a1bd5865198"
],
[
"Hacl.Impl.Curve25519.Finv.finv_",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Spec.Curve25519.prime",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"3a98a55191aca263cd0ff7cd6ca94347"
],
[
"Hacl.Impl.Curve25519.Finv.finv_",
2,
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_Hacl.Impl.Curve25519.Fields.M51",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U128",
"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.U128@tok",
"equality_tok_Lib.IntTypes.U32@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_stack_region",
"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.Impl.Curve25519.Field51.as_nat",
"equation_Hacl.Impl.Curve25519.Field51.felem_fits",
"equation_Hacl.Impl.Curve25519.Field64.Core.as_nat",
"equation_Hacl.Impl.Curve25519.Fields.as_nat",
"equation_Hacl.Impl.Curve25519.Fields.felem",
"equation_Hacl.Impl.Curve25519.Fields.felem_wide2",
"equation_Hacl.Impl.Curve25519.Fields.feval",
"equation_Hacl.Impl.Curve25519.Finv.fmuls_pre",
"equation_Hacl.Impl.Curve25519.Finv.fsquare_times_inv",
"equation_Hacl.Spec.Curve25519.Finv.finv",
"equation_Hacl.Spec.Curve25519.Finv.finv0",
"equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.gsub",
"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.op_Star_Bang",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.pub_int_v",
"equation_Lib.IntTypes.uint128", "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.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.fmul",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
"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", "l_and-interp",
"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_extends_includes",
"lemma_FStar.Monotonic.HyperHeap.lemma_extends_parent",
"lemma_FStar.Monotonic.HyperHeap.lemma_includes_refl",
"lemma_FStar.Monotonic.HyperStack.lemma_mk_mem__projectors",
"lemma_FStar.Monotonic.HyperStack.lemma_tip_top_smt",
"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.UInt32.uv_inv", "lemma_FStar.UInt32.vu_inv",
"lemma_Lib.Buffer.modifies_preserves_live",
"lemma_Lib.IntTypes.mul_lemma", "lemma_Lib.IntTypes.pow2_values",
"lemma_LowStar.Monotonic.Buffer.address_liveness_insensitive_buffer",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_loc_not_unused_in_disjoint",
"lemma_LowStar.Monotonic.Buffer.fresh_frame_modifies",
"lemma_LowStar.Monotonic.Buffer.lemma_live_equal_mem_domains",
"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_gsub_buffer",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_includes_r",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_none_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_gsub_buffer_r_",
"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_buffer_elim",
"lemma_LowStar.Monotonic.Buffer.modifies_liveness_insensitive_buffer",
"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_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__3",
"projection_inverse_FStar.Pervasives.Native.Mktuple4__4",
"refinement_interpretation_Tm_refine_2011e81e05d092e08833cbfdaea77df9",
"refinement_interpretation_Tm_refine_244cb7c5828c28d18595aa07064423c4",
"refinement_interpretation_Tm_refine_28126c3229332b283e908c1fa6d2bdda",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_449ba593891ef077b0c39a9c30aa1294",
"refinement_interpretation_Tm_refine_485b1639e956873bf6de53e6ff9e6b14",
"refinement_interpretation_Tm_refine_4fa8e2dd96f8bb1e23e6574326e9e019",
"refinement_interpretation_Tm_refine_6c25b42778726de94cd4dac42edb4860",
"refinement_interpretation_Tm_refine_7bc6330d006be2101418673df5a895e6",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
"refinement_interpretation_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"refinement_interpretation_Tm_refine_e07d49bf7ed472bccb081418af1bddb0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Tm_refine_f0496eb03f3fb51b5e4ca0d53ea58c01",
"refinement_interpretation_Tm_refine_ff563099e22dae2b404da6132c755639",
"token_correspondence_Lib.IntTypes.mul",
"token_correspondence_Lib.IntTypes.op_Star_Bang",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Map.restrict", "typing_FStar.Monotonic.Heap.emp",
"typing_FStar.Monotonic.HyperHeap.includes",
"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.is_stack_region",
"typing_FStar.Monotonic.HyperStack.remove_elt",
"typing_FStar.Set.complement", "typing_FStar.Set.intersect",
"typing_FStar.Set.mem", "typing_FStar.Set.singleton",
"typing_FStar.Set.union", "typing_FStar.UInt.fits",
"typing_FStar.UInt32.uint_to_t", "typing_FStar.UInt32.v",
"typing_Hacl.Impl.Curve25519.Fields.feval",
"typing_Hacl.Spec.Curve25519.Finv.finv", "typing_Lib.Buffer.length",
"typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar",
"typing_Lib.IntTypes.pub_int_v", "typing_Lib.IntTypes.uint_v",
"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_buffer",
"typing_LowStar.Monotonic.Buffer.loc_none",
"typing_LowStar.Monotonic.Buffer.loc_not_unused_in",
"typing_LowStar.Monotonic.Buffer.loc_regions",
"typing_LowStar.Monotonic.Buffer.loc_union",
"typing_LowStar.Monotonic.Buffer.mgsub",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"68a7720a32637d7ae9c67d787627281b"
],
[
"Hacl.Impl.Curve25519.Finv.finv",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Spec.Curve25519.prime",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"fa52fd99fa102341d426def95f323273"
],
[
"Hacl.Impl.Curve25519.Finv.finv",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.M51",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.M64",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Hacl.Impl.Curve25519.Fields.M51",
"disc_equation_Hacl.Impl.Curve25519.Fields.M64",
"equality_tok_Hacl.Impl.Curve25519.Fields.M51@tok",
"equality_tok_Hacl.Impl.Curve25519.Fields.M64@tok",
"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_Hacl.Impl.Curve25519.Fields.felem",
"equation_Hacl.Impl.Curve25519.Fields.felem_wide2",
"equation_Hacl.Impl.Curve25519.Finv.fsquare_times_inv",
"equation_Lib.Buffer.buffer_t", "equation_Lib.Buffer.disjoint",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.uint128",
"equation_Lib.IntTypes.uint64",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.field_spec",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_0773a299ec43f8fb537ec511f9cd85af",
"refinement_interpretation_Tm_refine_5e9d01688e782e890c1771e34048cde0",
"refinement_interpretation_Tm_refine_76cbddfcb439cc2a5d1b5c6a016a28b2",
"refinement_interpretation_Tm_refine_9a74d818566e70513bc032cc3b65a144",
"refinement_interpretation_Tm_refine_c2215b703b2340e9e4551c4e8820d7c8",
"refinement_interpretation_Tm_refine_da193190735123e260342f6f64171d0f",
"true_interp", "typing_FStar.Map.contains",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_FStar.Monotonic.HyperStack.get_tip", "typing_Lib.Buffer.loc",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"9b698383f84b4ab6d45cb6b2be2ea5f4"
]
]
]
Computing file changes ...
