Revision 0d9153dc34ee2dcf0821e3f21e825fc5bb8895b4 authored by Santiago Zanella-Beguelin on 11 December 2019, 17:46:08 UTC, committed by Santiago Zanella-Beguelin on 12 December 2019, 10:33:01 UTC
1 parent 7405f78
Vale.AES.GCTR_s.fst.hints
[
"#��/���Ti,�\u0018�",
[
[
"Vale.AES.GCTR_s.gctr_plain_LE",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Seq.Base.seq__uu___haseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat8",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"7bad99ca591c1cf89e6c88bb78aebbd5"
],
[
"Vale.AES.GCTR_s.gctr_plain_internal_LE",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Seq.Base.seq__uu___haseq", "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",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.Def.Types_s.quad32"
],
0,
"38d92ff4e6fec5282d5adad95e276ae3"
],
[
"Vale.AES.GCTR_s.inc32",
1,
1,
0,
[ "@query" ],
0,
"c5ed8dee55a51301b174ab36a7280a7e"
],
[
"Vale.AES.GCTR_s.gctr_encrypt_block",
1,
1,
0,
[ "@query" ],
0,
"901a8539afdf792b9ca5622e9c3abfbe"
],
[
"Vale.AES.GCTR_s.gctr_encrypt_recursive",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_c3b8ca4826e9e8432a34e6824d62768b_3",
"binder_x_f960072d0bfae1e534f0393998cf6653_1",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.tail", "equation_Prims.nat",
"equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.GCTR_s.gctr_plain_internal_LE",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_FStar.Seq.Base.length", "well-founded-ordering-on-nat"
],
0,
"cd0ad56639e534044ac6295b44c0a74a"
],
[
"Vale.AES.GCTR_s.pad_to_128_bits",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"7eb0e183c102545e39129074a8257f2b"
],
[
"Vale.AES.GCTR_s.gctr_encrypt_LE_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.Seq.Base.op_At_Bar",
"equation_FStar.Seq.Properties.split", "equation_Prims.nat",
"equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
"equation_Vale.AES.GCTR_s.pad_to_128_bits",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length"
],
0,
"13919fc416232ccc9fa59cbcddeac693"
],
[
"Vale.AES.GCTR_s.gctr_plain_LE",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Seq.Base.seq__uu___haseq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Def.Words_s.natN", "function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat8",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"haseqTm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"b86faad76fe9f60777fe8158f4bb0cac"
],
[
"Vale.AES.GCTR_s.gctr_plain_internal_LE",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Seq.Base.seq__uu___haseq", "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",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"typing_Vale.Def.Types_s.quad32"
],
0,
"ee7a661d8902bb864eb26ffa949f37b4"
],
[
"Vale.AES.GCTR_s.inc32",
2,
1,
0,
[ "@query" ],
0,
"7566233921a570c2e2cd70220f2837c7"
],
[
"Vale.AES.GCTR_s.gctr_encrypt_block",
2,
1,
0,
[ "@query" ],
0,
"770d354fe19105180b0af59deacad14b"
],
[
"Vale.AES.GCTR_s.gctr_encrypt_recursive",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"binder_x_c3b8ca4826e9e8432a34e6824d62768b_3",
"binder_x_f960072d0bfae1e534f0393998cf6653_1",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.tail", "equation_Prims.nat",
"equation_Vale.AES.AES_s.aes_key_LE",
"equation_Vale.AES.GCTR_s.gctr_plain_internal_LE",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7ecc9ff2104c1b3467333d052c1b37c3",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_FStar.Seq.Base.length", "well-founded-ordering-on-nat"
],
0,
"99fbc957ffe77d1c70d64992bcb772cb"
],
[
"Vale.AES.GCTR_s.pad_to_128_bits",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"5d79b87a7b1ea8b0981d75ac43d4893f"
],
[
"Vale.AES.GCTR_s.gctr_encrypt_LE_def",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.Seq.Base.op_At_Bar",
"equation_FStar.Seq.Properties.split", "equation_Prims.nat",
"equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
"equation_Vale.AES.GCTR_s.pad_to_128_bits",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length"
],
0,
"fe239943f821bc7cae5ab8345f26de9b"
]
]
]
Computing file changes ...
