Revision cef6a8e821f55e71b791555d22b45bd3debc2596 authored by Jonathan Protzenko on 08 May 2020, 16:26:29 UTC, committed by GitHub on 08 May 2020, 16:26:29 UTC
OCaml API: Don't run unit tests which require unsupported features
Hacl.Impl.Curve25519.Fields.fst.hints
[
"�n>'}PS\b�1�\u0002�W%_",
[
[
"Hacl.Impl.Curve25519.Fields.create_felem",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Hacl.Impl.Curve25519.Fields.Core.felem",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.Core.field_spec",
"function_token_typing_Lib.IntTypes.uint64",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"typing_Lib.Buffer.length", "typing_tok_Lib.Buffer.MUT@tok"
],
0,
"4c393a7d814e92134b530bb0f29d5ac8"
],
[
"Hacl.Impl.Curve25519.Fields.create_felem",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.Core.M51",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.Core.M64",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Hacl.Impl.Curve25519.Fields.Core.M51",
"disc_equation_Hacl.Impl.Curve25519.Fields.Core.M64",
"equality_tok_Hacl.Impl.Curve25519.Fields.Core.M51@tok",
"equality_tok_Hacl.Impl.Curve25519.Fields.Core.M64@tok",
"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.HyperStack.is_stack_region",
"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",
"equation_Hacl.Impl.Curve25519.Field64.as_nat",
"equation_Hacl.Impl.Curve25519.Field64.felem",
"equation_Hacl.Impl.Curve25519.Fields.Core.as_nat",
"equation_Hacl.Impl.Curve25519.Fields.Core.f64_as_nat",
"equation_Hacl.Impl.Curve25519.Fields.Core.felem",
"equation_Lib.Buffer.as_seq", "equation_Lib.Buffer.buffer_t",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.length",
"equation_Lib.Buffer.stack_allocated", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.to_seq",
"equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.Core.field_spec",
"function_token_typing_Lib.IntTypes.uint64", "int_typing",
"lemma_FStar.UInt.pow2_values", "lemma_FStar.UInt32.uv_inv",
"lemma_FStar.UInt32.vu_inv", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"refinement_interpretation_Tm_refine_f63e058f9631c11993f3ef0430296051",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"typing_FStar.UInt.fits", "typing_FStar.UInt32.v",
"typing_Lib.Buffer.as_seq", "typing_Lib.Buffer.length",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v",
"typing_Lib.Sequence.create", "typing_Lib.Sequence.index",
"typing_LowStar.Buffer.trivial_preorder",
"typing_LowStar.Monotonic.Buffer.len",
"typing_tok_Lib.Buffer.MUT@tok", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"ec7069a97a785d4fb2c5104e64b2a9b3"
],
[
"Hacl.Impl.Curve25519.Fields.load_felem",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"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.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.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint64", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_LowStar.Buffer.buffer",
"equation_LowStar.Buffer.trivial_preorder",
"equation_LowStar.Monotonic.Buffer.length", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Lib.IntTypes.uint64", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_FStar.UInt32.vu_inv", "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_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_Prims.pow2.fuel_instrumented",
"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,
"2a4dcd7743062739f3f1745a599f8851"
],
[
"Hacl.Impl.Curve25519.Fields.load_felem",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.Core.M51",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.Core.M64",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Hacl.Impl.Curve25519.Fields.Core.M51",
"disc_equation_Hacl.Impl.Curve25519.Fields.Core.M64",
"equality_tok_Hacl.Impl.Curve25519.Fields.Core.M51@tok",
"equality_tok_Hacl.Impl.Curve25519.Fields.Core.M64@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equation_Hacl.Impl.Curve25519.Field51.as_nat",
"equation_Hacl.Impl.Curve25519.Field51.mul_inv_t",
"equation_Hacl.Impl.Curve25519.Field64.as_nat",
"equation_Hacl.Impl.Curve25519.Fields.Core.as_nat",
"equation_Hacl.Impl.Curve25519.Fields.Core.f64_as_nat",
"equation_Hacl.Impl.Curve25519.Fields.Core.felem",
"equation_Hacl.Impl.Curve25519.Fields.Core.state_inv_t",
"equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.IntTypes.uint64",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.Core.field_spec",
"function_token_typing_Lib.IntTypes.uint64",
"lemma_LowStar.Monotonic.Buffer.loc_disjoint_sym_",
"refinement_interpretation_Tm_refine_470aaadd8acd372a5128b93b0d81a445",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_c719433cbf3fb77a65a7472809cffc2b",
"refinement_interpretation_Tm_refine_ef74734f92d450d3cdc082893a1e114b",
"true_interp", "typing_Lib.Buffer.loc",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"189fe7b8f703c9db71836e92e22c44d1"
],
[
"Hacl.Impl.Curve25519.Fields.store_felem",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"assumption_Hacl.Impl.Curve25519.Fields.Core.field_spec__uu___haseq",
"bool_inversion", "constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_FStar.HyperStack.ST.equal_domains",
"equation_FStar.Monotonic.HyperHeap.hmap",
"equation_FStar.Monotonic.HyperStack.is_wf_with_ctr_and_tip",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.Buffer.modifies",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.Curve25519.elem", "equation_Spec.Curve25519.prime",
"function_token_typing_FStar.Monotonic.Heap.heap",
"function_token_typing_Lib.IntTypes.uint64", "int_typing",
"lemma_FStar.Map.lemma_ContainsDom",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_Spec.Curve25519.Lemmas.lemma_pow2_256",
"lemma_Spec.Curve25519.Lemmas.lemma_prime_value",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05e15190c946858f68c69156f585f95a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_85ecd7f653e1b5e74710d5c4a04e67f9",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_c9f318957334bae90e9d8f370d26a655",
"typing_FStar.Map.contains", "typing_FStar.Map.domain",
"typing_FStar.Monotonic.HyperHeap.rid",
"typing_FStar.Monotonic.HyperHeap.root",
"typing_FStar.Monotonic.HyperStack.get_hmap",
"typing_Lib.Buffer.length", "typing_tok_Lib.Buffer.MUT@tok"
],
0,
"6fecdd9e76f3f7118457c86ede01e888"
],
[
"Hacl.Impl.Curve25519.Fields.store_felem",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.Core.M51",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.Core.M64",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Hacl.Impl.Curve25519.Fields.Core.M51",
"disc_equation_Hacl.Impl.Curve25519.Fields.Core.M64",
"equality_tok_Hacl.Impl.Curve25519.Fields.Core.M51@tok",
"equality_tok_Hacl.Impl.Curve25519.Fields.Core.M64@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equation_FStar.Monotonic.HyperStack.mem",
"equation_Hacl.Impl.Curve25519.Field51.as_nat",
"equation_Hacl.Impl.Curve25519.Field51.fevalh",
"equation_Hacl.Impl.Curve25519.Field51.mul_inv_t",
"equation_Hacl.Impl.Curve25519.Field64.as_nat",
"equation_Hacl.Impl.Curve25519.Field64.fevalh",
"equation_Hacl.Impl.Curve25519.Fields.Core.as_nat",
"equation_Hacl.Impl.Curve25519.Fields.Core.f64_as_nat",
"equation_Hacl.Impl.Curve25519.Fields.Core.felem",
"equation_Hacl.Impl.Curve25519.Fields.Core.feval",
"equation_Hacl.Impl.Curve25519.Fields.Core.state_inv_t",
"equation_Lib.Buffer.disjoint", "equation_Lib.Buffer.lbuffer_t",
"equation_Lib.Buffer.loc", "equation_Lib.Buffer.modifies",
"equation_Lib.Buffer.op_Bar_Plus_Bar", "equation_Lib.Buffer.union",
"equation_Lib.IntTypes.uint64",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.Core.field_spec",
"function_token_typing_Lib.IntTypes.uint64",
"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",
"refinement_interpretation_Tm_refine_0a2bc3456ab5d2529deef0cf55bfcb91",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_c007638b1d4ef7e66e6c5a80ab3319ff",
"refinement_interpretation_Tm_refine_c8ceecb817f306c82df370d5b4c19b28",
"typing_Lib.Buffer.loc", "typing_Lib.Buffer.op_Bar_Plus_Bar",
"typing_tok_Lib.Buffer.MUT@tok"
],
0,
"81f26f67a1d87a7df4e4024e4d4956c6"
],
[
"Hacl.Impl.Curve25519.Fields.set_zero",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.Core.M51",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.Core.M64",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Hacl.Impl.Curve25519.Fields.Core.M51",
"disc_equation_Hacl.Impl.Curve25519.Fields.Core.M64",
"equality_tok_Hacl.Impl.Curve25519.Fields.Core.M51@tok",
"equality_tok_Hacl.Impl.Curve25519.Fields.Core.M64@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equation_Hacl.Impl.Curve25519.Field51.as_nat",
"equation_Hacl.Impl.Curve25519.Field64.as_nat",
"equation_Hacl.Impl.Curve25519.Fields.Core.as_nat",
"equation_Hacl.Impl.Curve25519.Fields.Core.f64_as_nat",
"equation_Hacl.Impl.Curve25519.Fields.Core.felem",
"equation_Lib.Buffer.lbuffer_t",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.Core.field_spec",
"refinement_interpretation_Tm_refine_8cc8cfcb64d575010750a5c00af3e912",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_b7157694aac1b0440d3dbc917c3c7f5f"
],
0,
"5eab14cb2e2fae37ccbf283006f37b50"
],
[
"Hacl.Impl.Curve25519.Fields.set_one",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.Core.M51",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.Core.M64",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Hacl.Impl.Curve25519.Fields.Core.M51",
"disc_equation_Hacl.Impl.Curve25519.Fields.Core.M64",
"equality_tok_Hacl.Impl.Curve25519.Fields.Core.M51@tok",
"equality_tok_Hacl.Impl.Curve25519.Fields.Core.M64@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equation_Hacl.Impl.Curve25519.Field51.as_nat",
"equation_Hacl.Impl.Curve25519.Field64.as_nat",
"equation_Hacl.Impl.Curve25519.Fields.Core.as_nat",
"equation_Hacl.Impl.Curve25519.Fields.Core.f64_as_nat",
"equation_Hacl.Impl.Curve25519.Fields.Core.felem",
"equation_Lib.Buffer.lbuffer_t",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.Core.field_spec",
"refinement_interpretation_Tm_refine_8cc8cfcb64d575010750a5c00af3e912",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_b7157694aac1b0440d3dbc917c3c7f5f"
],
0,
"d0ec433434671d71ddaec5014c119a5f"
],
[
"Hacl.Impl.Curve25519.Fields.copy_felem",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.Buffer.MUT@tok",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Hacl.Impl.Curve25519.Fields.Core.felem",
"equation_Lib.Buffer.lbuffer_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint64",
"equation_Lib.IntTypes.v", "equation_Prims.nat",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.Core.field_spec",
"function_token_typing_Lib.IntTypes.uint64",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"typing_Lib.Buffer.length", "typing_tok_Lib.Buffer.MUT@tok"
],
0,
"e685189ee9945a0fe6b80e240a2d76ac"
],
[
"Hacl.Impl.Curve25519.Fields.copy_felem",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.Core.M51",
"constructor_distinct_Hacl.Impl.Curve25519.Fields.Core.M64",
"constructor_distinct_Lib.Buffer.MUT",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Hacl.Impl.Curve25519.Fields.Core.M51",
"disc_equation_Hacl.Impl.Curve25519.Fields.Core.M64",
"equality_tok_Hacl.Impl.Curve25519.Fields.Core.M51@tok",
"equality_tok_Hacl.Impl.Curve25519.Fields.Core.M64@tok",
"equality_tok_Lib.Buffer.MUT@tok",
"equation_Hacl.Impl.Curve25519.Fields.Core.felem",
"equation_Lib.Buffer.lbuffer_t",
"fuel_guarded_inversion_Hacl.Impl.Curve25519.Fields.Core.field_spec",
"refinement_interpretation_Tm_refine_9d89bf7b57667578cd0e1f4470daef3b",
"refinement_interpretation_Tm_refine_c719433cbf3fb77a65a7472809cffc2b",
"refinement_interpretation_Tm_refine_ce574fceac2f5d96ea03a3c9c2638559"
],
0,
"60f7b716b9b027b70b88b8bfbaaafe1f"
]
]
]
Computing file changes ...
