Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Vale.AES.GCTR.fsti.hints
[
"R-GZ���\u0011І�p�\u001c��",
[
[
"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,
"4e959e86d4c67515c36c8c55d80171c3"
],
[
"Vale.AES.GCTR.partial_seq_agreement",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000"
],
0,
"b9766367c45668aa57a807d8ea44937a"
],
[
"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,
"c8fbc0c1173054bbf0fa037a184fca6a"
],
[
"Vale.AES.GCTR.gctr_encrypt_empty",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Seq.Base.seq__uu___haseq", "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_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,
"7c0c8320633e1705ed2e28a6c0b04635"
],
[
"Vale.AES.GCTR.aes_encrypt_BE",
1,
1,
0,
[ "@query" ],
0,
"8f0db4d3695bb99ae80943b1be03b3d8"
],
[
"Vale.AES.GCTR.gctr_registers_def",
1,
1,
0,
[ "@query" ],
0,
"5797f88ba7620f6db37bb9923f2e4000"
],
[
"Vale.AES.GCTR.gctr_partial",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_21b1463d18ebbb1eb97818a4f59e4000"
],
0,
"6870f7403acfb451de53dce479da3497"
],
[
"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,
"a500b068ab30de04acaab75ead361788"
],
[
"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,
"7a2521ae5ce7a63de80434230a434f6e"
],
[
"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,
"7ab5f22770edbd3c66c1a397513de89d"
],
[
"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,
"a4bbabe10221a8153a70e37277549017"
],
[
"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,
"9f3a3679d63a81245395ae0a839bb8fe"
],
[
"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,
"fdfe56afd0664ecd2464d44c53a63a68"
],
[
"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,
"8a76231396d6bae159a650de30a92d83"
],
[
"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,
"036c0afd4364af3fc85552167545395a"
],
[
"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,
"6c2c85d56d333695b24858aea42cee4d"
]
]
]
Computing file changes ...
