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
Vale.Poly1305.Equiv.fst.hints
[
"�\u001fhʢq�y��[�uM\\\u000f",
[
[
"Vale.Poly1305.Equiv.block_fun",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.size_block",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_127",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"435c0daef1890f3b040471bafd922732"
],
[
"Vale.Poly1305.Equiv.lemma_poly1305_equiv_rec",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.size_block",
"primitive_Prims.op_LessThanOrEqual",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_1bac668dddcac6fb0e52f0c9514b035e",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_449625ce4ad52aa2ec0cbe0bec458d86",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"09550c46421893869aab85c5495ea746"
],
[
"Vale.Poly1305.Equiv.lemma_poly1305_equiv_rec",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_correspondence_Vale.Poly1305.Spec_s.poly1305_hash_blocks.fuel_instrumented",
"@fuel_irrelevance_Vale.Poly1305.Spec_s.poly1305_hash_blocks.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Poly1305.Equiv_interpretation_Tm_arrow_750b542a74c0f6cef7bc9c9174882097",
"Vale.Poly1305.Spec_s_interpretation_Tm_arrow_6c528cb178c0356159679935f3a11594",
"b2t_def", "binder_x_11f88ae15b1e5de7ff355bd1d7c52426_0",
"binder_x_2d0bd80df28aa2f2169bec182f0e740d_1",
"binder_x_2d0bd80df28aa2f2169bec182f0e740d_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equality_tok_Prims.LexTop@tok",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length",
"equation_Lib.Sequence.repeat_blocks_f", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.encode",
"equation_Spec.Poly1305.fadd", "equation_Spec.Poly1305.felem",
"equation_Spec.Poly1305.poly1305_update1",
"equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_block",
"equation_Vale.Def.Words_s.nat128", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Poly1305.Equiv.block_fun",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"equation_with_fuel_Vale.Poly1305.Spec_s.poly1305_hash_blocks.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Vale.Poly1305.Equiv.block_fun",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_1bac668dddcac6fb0e52f0c9514b035e",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_2df60152c11f8fa3e12a9a666c0e23b7",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"token_correspondence_Spec.Poly1305.poly1305_update1",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Vale.Poly1305.Equiv.block_fun",
"well-founded-ordering-on-nat"
],
0,
"0a470b0eec34085852736d78aac9af6f"
],
[
"Vale.Poly1305.Equiv.lemma_poly1305_equiv_last",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.SEC",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Lib.ByteSequence.nat_from_bytes_le",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.encode", "equation_Spec.Poly1305.fadd",
"equation_Spec.Poly1305.felem",
"equation_Spec.Poly1305.poly1305_update1",
"equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_block",
"equation_Vale.Poly1305.Equiv.block_fun",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_3fd10d79e1f4b0d8069ab6e203bd2713",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_Lib.Sequence.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_block"
],
0,
"e6ee5dfb0ce500eadc0ff6b2e00bd77d"
],
[
"Vale.Poly1305.Equiv.lemma_poly1305_equiv_r",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok",
"equality_tok_Lib.IntTypes.U8@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.IntTypes.bits", "equation_Lib.IntTypes.logand_v",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.key", "equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "equation_Spec.Poly1305.to_felem",
"equation_Vale.Def.Words_s.nat64", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Poly1305.Math.lowerUpper128_def",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Vale.Poly1305.Math.lowerUpper128",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_127",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_153bfbd15dbb4a9c413275083059c752",
"refinement_interpretation_Tm_refine_2897f455bd1a2e7bd7f8f1aa6ce63472",
"refinement_interpretation_Tm_refine_3e9d04c89ab3a202cd1b97a76ce93dbd",
"refinement_interpretation_Tm_refine_4ae12848fac0601da6605bac9d6872f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"token_correspondence_Vale.Poly1305.Math.lowerUpper128_def",
"typing_FStar.UInt.fits",
"typing_Lib.ByteSequence.nat_from_bytes_le",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
"typing_Lib.Sequence.length", "typing_Prims.pow2",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_block", "typing_Vale.Def.Types_s.iand",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U64@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"b1ab9efa896868b8262761db87c35ff9"
],
[
"Vale.Poly1305.Equiv.lemma_poly1305_equiv",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf", "equation_Spec.Poly1305.key",
"equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.ByteSequence.nat_from_bytes_le",
"typing_Lib.IntTypes.minint", "typing_Lib.Sequence.length",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"2f468604069243eba0b018fc4732d9ba"
],
[
"Vale.Poly1305.Equiv.lemma_poly1305_equiv",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.slice",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"equation_Spec.Poly1305.felem", "equation_Spec.Poly1305.fmul",
"equation_Spec.Poly1305.from_felem", "equation_Spec.Poly1305.key",
"equation_Spec.Poly1305.poly1305_finish",
"equation_Spec.Poly1305.poly1305_init",
"equation_Spec.Poly1305.poly1305_mac",
"equation_Spec.Poly1305.poly1305_update",
"equation_Spec.Poly1305.poly1305_update1",
"equation_Spec.Poly1305.poly1305_update_last",
"equation_Spec.Poly1305.prime", "equation_Spec.Poly1305.size_block",
"equation_Spec.Poly1305.size_key", "equation_Spec.Poly1305.to_felem",
"equation_Spec.Poly1305.zero",
"equation_Vale.Poly1305.Spec_s.make_r",
"equation_Vale.Poly1305.Spec_s.poly1305_hash",
"equation_Vale.Poly1305.Spec_s.poly1305_hash_all",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Vale.Poly1305.Equiv.block_fun",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Lib.IntTypes.pow2_127", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_1bac668dddcac6fb0e52f0c9514b035e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_63efca340ea10f520d98d30b7bd6d230",
"refinement_interpretation_Tm_refine_72530680bea79807d75cb9d6e7632258",
"refinement_interpretation_Tm_refine_7469e637a8c96cb70cd78854c6904f1b",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7f16c7b57ef8bef37e694fdc293f58a5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_b980dd096af896d3c53bb79f2279e581",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795",
"refinement_interpretation_Tm_refine_f1f3a6a6d3da045b35e7ba130c8b362a",
"typing_FStar.Seq.Base.length",
"typing_Lib.ByteSequence.nat_from_bytes_le",
"typing_Lib.ByteSequence.nat_to_bytes_le",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
"typing_Lib.Sequence.length", "typing_Lib.Sequence.slice",
"typing_Lib.Sequence.sub", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Spec.Poly1305.size_block", "typing_Spec.Poly1305.size_key",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"923a5db0d38409a1e4aab09e4133b709"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...