Revision 724d1045f60f13d79df1afc5190955afdfa73ec1 authored by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC, committed by Victor Dumitrescu on 16 April 2020, 09:31:08 UTC
Co-authored-by: @protz
1 parent ca37fbf
Vale.AES.GHash_s.fst.hints
[
"\u0000l\u001e?@\b�O\u0003j�]���G",
[
[
"Vale.AES.GHash_s.ghash_plain_LE",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat32",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.hasEq_lemma",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.Def.Types_s.quad32"
],
0,
"ee49d67f0ea82141940300db3f9e8713"
],
[
"Vale.AES.GHash_s.ghash_LE_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_cee79fb2a0b31329a2e2b29d477b66be_1",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.AES.GHash_s.ghash_plain_LE",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Lib.Seqs_s.all_but_last",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3cde0f73125500a52bff30114a1a1137",
"refinement_interpretation_Tm_refine_3e04674625ba1e90ddf6da6977508e33",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_FStar.Seq.Base.length",
"typing_Vale.Lib.Seqs_s.all_but_last", "well-founded-ordering-on-nat"
],
0,
"6b07c5184cf0f875729b6df40153e3c9"
],
[
"Vale.AES.GHash_s.ghash_LE_reveal",
1,
1,
0,
[ "@query" ],
0,
"7f776de9cbac96ccb6afaa7fa75ca384"
],
[
"Vale.AES.GHash_s.ghash_plain_LE",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat32",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.hasEq_lemma",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.Def.Types_s.quad32"
],
0,
"164416d7230e1a690410069d906bd7ff"
],
[
"Vale.AES.GHash_s.ghash_LE_def",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_cee79fb2a0b31329a2e2b29d477b66be_1",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_Vale.AES.GHash_s.ghash_plain_LE",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"equation_Vale.Lib.Seqs_s.all_but_last",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3cde0f73125500a52bff30114a1a1137",
"refinement_interpretation_Tm_refine_3e04674625ba1e90ddf6da6977508e33",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_FStar.Seq.Base.length",
"typing_Vale.Lib.Seqs_s.all_but_last", "well-founded-ordering-on-nat"
],
0,
"242f7c32883f5b656f93c49952870f1d"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...