Revision 1539fc67ec7cd1f092967452d8ae47d170ca149b authored by Jonathan Protzenko on 24 April 2020, 23:18:32 UTC, committed by Jonathan Protzenko on 24 April 2020, 23:18:32 UTC
1 parent 56130dc
Vale.AES.GCTR.fsti.hints
[
"\u0014��\\� 8��ת!M�\fE",
[
[
"Vale.AES.GCTR.inc32lite",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Words_s.nat32",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_Vale.Def.Words_s.__proj__Mkfour__item__lo0"
],
0,
"28e10a292bd6168fae66605020b0a175"
],
[
"Vale.AES.GCTR.partial_seq_agreement",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000"
],
0,
"0d89052c553baf60ea87800e5ad5087e"
],
[
"Vale.AES.GCTR.gctr_encrypt_block_offset",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"88d991ce4e1d14a1cf7b2471f740e66b"
],
[
"Vale.AES.GCTR.gctr_encrypt_empty",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.GCTR.make_gctr_plain_LE",
"equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
"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",
"lemma_FStar.Seq.Base.hasEq_lemma",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
],
0,
"842e7b3fc5e8cc72f70e95fcffd6bf7e"
],
[
"Vale.AES.GCTR.aes_encrypt_BE",
1,
1,
0,
[ "@query" ],
0,
"8d0d121afee662799bebe97355b7ba34"
],
[
"Vale.AES.GCTR.gctr_registers_def",
1,
1,
0,
[ "@query" ],
0,
"8d4742ff1c3810b66c8ec8fcd6f17862"
],
[
"Vale.AES.GCTR.gctr_registers_reveal",
1,
1,
0,
[ "@query" ],
0,
"91438f6c9f08eeaa648fb6d627479454"
],
[
"Vale.AES.GCTR.gctr_partial_def",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000"
],
0,
"5bb69940785d1c642fe69ecd7b93fa63"
],
[
"Vale.AES.GCTR.gctr_partial_reveal",
1,
1,
0,
[ "@query" ],
0,
"d4480efc11c6c1099093290a5441f786"
],
[
"Vale.AES.GCTR.lemma_gctr_partial_append",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Base.op_At_Bar", "equation_Prims.min",
"equation_Prims.nat", "equation_Vale.AES.GCTR.gctr_partial",
"equation_Vale.AES.GCTR.gctr_partial_opaque",
"equation_Vale.AES.GCTR_s.inc32", "equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Subtraction",
"proj_equation_Vale.Def.Words_s.Mkfour_hi2",
"proj_equation_Vale.Def.Words_s.Mkfour_hi3",
"proj_equation_Vale.Def.Words_s.Mkfour_lo0",
"proj_equation_Vale.Def.Words_s.Mkfour_lo1",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi2",
"projection_inverse_Vale.Def.Words_s.Mkfour_hi3",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo0",
"projection_inverse_Vale.Def.Words_s.Mkfour_lo1",
"refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"token_correspondence_Vale.AES.GCTR.gctr_partial"
],
0,
"eb25a0f6fc0199c85f3f6a69dd720ceb"
],
[
"Vale.AES.GCTR.gctr_partial_opaque_ignores_postfix",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.min",
"equation_Prims.nat", "equation_Vale.AES.GCTR.gctr_partial",
"equation_Vale.AES.GCTR.gctr_partial_opaque",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.natN",
"fuel_guarded_inversion_Vale.Def.Words_s.four",
"function_token_typing_Vale.Def.Opaque_s.make_opaque",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition",
"primitive_Prims.op_GreaterThanOrEqual",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_05a1a488a8ea9b2e17b311a5ff0bb8b1",
"refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"token_correspondence_Vale.AES.GCTR.gctr_partial"
],
0,
"b11690dc41e9cd8840fa77b670634d07"
],
[
"Vale.AES.GCTR.gctr_partial_extend6",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"b47354e452324e427c2f828a7c90367b"
],
[
"Vale.AES.GCTR.gctr_partial_completed",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
"equation_Prims.squash", "equation_Vale.AES.GCTR.gctr_partial",
"l_and-interp",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"dd40fd2f12292362d28d2e1cb9c8d887"
],
[
"Vale.AES.GCTR.gctr_partial_opaque_completed",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.l_and",
"equation_Prims.squash", "l_and-interp",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"9751311cf6663ddc6a9c1a5d0a0f61c9"
],
[
"Vale.AES.GCTR.gctr_partial_to_full_basic",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
"equation_Vale.AES.GCTR_s.is_gctr_plain_LE", "l_and-interp",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"648483796b0bad0f722eccafbff8ae60"
],
[
"Vale.AES.GCTR.gctr_partial_to_full_advanced",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"eq2-interp", "equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
"equation_Vale.Def.Types_s.le_seq_quad32_to_bytes",
"equation_Vale.Def.Words_s.nat8",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "l_and-interp", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_Vale.Def.Types_s.le_seq_quad32_to_bytes"
],
0,
"69ac38f295015f95b9d233006ee4398b"
],
[
"Vale.AES.GCTR.gctr_encrypt_one_block",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "equation_Prims.squash",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.GCTR_s.is_gctr_plain_LE",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"2fbfa1e29f5a6566020c59ad7a980ecb"
],
[
"Vale.AES.GCTR.gctr_bytes_helper",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"eq2-interp", "equation_Prims.nat", "equation_Prims.squash",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words_s.nat32",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32", "int_inversion",
"kinding_Vale.Def.Words_s.four@tok", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_Vale.Def.Types_s.le_seq_quad32_to_bytes_length",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_FStar.Seq.Base.append"
],
0,
"b70829f09a78b2457223d785a62fd3b4"
]
]
]
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...