Revision b5e85960e109efb08b9c65a4ab85c9b4ef926419 authored by Jay Bosamiya on 04 June 2019, 18:24:09 UTC, committed by Jay Bosamiya on 04 June 2019, 18:24:09 UTC
1 parent 2a5defc
Vale.AES.X64.GCMdecrypt.fsti.hints
[
"�gm))>7�3\u0004ej݃�`",
[
[
"Vale.AES.X64.GCMdecrypt.va_req_gcm_decrypt2_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"equation_Prims.l_and", "equation_Prims.squash",
"equation_Prims.subtype_of",
"l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"unit_typing"
],
0,
"167f919c3528d986a3bcb15e0593e1e7"
],
[
"Vale.AES.X64.GCMdecrypt.va_ens_gcm_decrypt2_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f8666440faa91836cc5a13998af863fc",
"Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
"bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"constructor_distinct_Vale.Interop.Types.TUInt128", "eq2-interp",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equality_tok_Vale.Interop.Types.TUInt128@tok",
"equation_Prims.l_and", "equation_Prims.nat",
"equation_Prims.squash", "equation_Prims.subtype_of",
"equation_Vale.AES.AES_s.is_aes_key",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.X64.GCMdecrypt.va_req_gcm_decrypt2_stdcall",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
"equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.X64.Decls.va_state_eq",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"l_quant_interp_0235708612358a0dd8d2d21a7f9984d9",
"lemma_FStar.Seq.Base.lemma_init_len",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
"typing_Tm_abs_b39953460d24ff94efd756bca22ff955",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.State.__proj__Mkstate__item__mem",
"typing_tok_Vale.Interop.Types.TUInt128@tok", "unit_typing"
],
0,
"f852ceada1ac2667565b785d4812751c"
],
[
"Vale.AES.X64.GCMdecrypt.va_lemma_gcm_decrypt2_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
"bool_inversion", "constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"constructor_distinct_Vale.Interop.Types.TUInt128", "eq2-interp",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equality_tok_Vale.Interop.Types.TUInt128@tok",
"equality_tok_Vale.X64.Machine_s.Secret@tok", "equation_Prims.nat",
"equation_Vale.AES.AES_s.is_aes_key",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.AES.GCM_helpers.bytes_to_quad_size",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
"equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat64",
"equation_Vale.Def.Words_s.nat8", "equation_Vale.Def.Words_s.natN",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.X64.Decls.validDstAddrs128",
"equation_Vale.X64.Decls.validSrcAddrs128",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_inversion",
"int_typing", "kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_init_len",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
"refinement_interpretation_Tm_refine_6f7408bd5b3fb5406dc1512dac63da88",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
"typing_Tm_abs_b39953460d24ff94efd756bca22ff955",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.State.__proj__Mkstate__item__mem",
"typing_tok_Vale.Interop.Types.TUInt128@tok"
],
0,
"7d56bb716f2b2b385cb1bde9520ea338"
],
[
"Vale.AES.X64.GCMdecrypt.va_wp_gcm_decrypt2_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_320365ceb6468c29e8eba757f3baa574",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Def.Words.Seq_s_interpretation_Tm_arrow_dc9d041e9889259a3dc473e95d76f904",
"constructor_distinct_Vale.AES.AES_s.AES_128",
"constructor_distinct_Vale.AES.AES_s.AES_256",
"constructor_distinct_Vale.Interop.Types.TUInt128", "eq2-interp",
"equality_tok_Vale.AES.AES_s.AES_128@tok",
"equality_tok_Vale.AES.AES_s.AES_256@tok",
"equality_tok_Vale.Interop.Types.TUInt128@tok", "equation_Prims.nat",
"equation_Vale.AES.AES_s.is_aes_key",
"equation_Vale.AES.AES_s.is_aes_key_LE",
"equation_Vale.Def.Types_s.quad32",
"equation_Vale.Def.Words.Seq_s.seq4",
"equation_Vale.Def.Words.Seq_s.seq_four_to_seq_LE",
"equation_Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_LE",
"equation_Vale.Def.Words.Seq_s.seqn",
"equation_Vale.Def.Words_s.nat32", "equation_Vale.Def.Words_s.nat8",
"equation_Vale.Lib.Seqs_s.compose",
"equation_Vale.Lib.Seqs_s.seq_map",
"equation_Vale.X64.Decls.va_upd_reg",
"equation_Vale.X64.Decls.va_upd_xmm",
"equation_Vale.X64.Memory.base_typ_as_vale_type",
"equation_Vale.X64.Memory.buffer128",
"equation_Vale.X64.State.update_reg",
"equation_Vale.X64.State.update_xmm",
"fuel_guarded_inversion_Vale.X64.State.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Vale.Def.Words_s.nat32",
"function_token_typing_Vale.Def.Words_s.nat8", "int_typing",
"kinding_Vale.Def.Words_s.four@tok",
"lemma_FStar.Seq.Base.lemma_init_len",
"proj_equation_Vale.X64.State.Mkstate_mem",
"proj_equation_Vale.X64.State.Mkstate_memTaint",
"proj_equation_Vale.X64.State.Mkstate_ok",
"proj_equation_Vale.X64.State.Mkstate_stack",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Vale.X64.State.Mkstate_mem",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_5834f17226f258d10f6cc5e617bb0da1",
"refinement_interpretation_Tm_refine_8545a50511781623fc41e3fb8428bce0",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ad1b7a4ad4a7492235749f17c7fc2f27",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.length",
"typing_Tm_abs_45bc106d66ff9e2c3c9f4100524b39b3",
"typing_Tm_abs_b39953460d24ff94efd756bca22ff955",
"typing_Vale.Def.Types_s.reverse_bytes_quad32",
"typing_Vale.Def.Words.Seq_s.four_to_seq_BE",
"typing_Vale.X64.Memory.buffer_read",
"typing_Vale.X64.State.__proj__Mkstate__item__mem",
"typing_tok_Vale.Interop.Types.TUInt128@tok"
],
0,
"cb31d1a21f103db88eb9d945da9ef7e2"
],
[
"Vale.AES.X64.GCMdecrypt.va_wpProof_gcm_decrypt2_stdcall",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.squash",
"refinement_interpretation_Tm_refine_8d65e998a07dd53ec478e27017d9dba5"
],
0,
"acb5d37d04f67b18d096f3408d4b91a1"
]
]
]
Computing file changes ...
