https://github.com/project-everest/hacl-star
Tip revision: 37b8a39e2ffd970444f7864cc1b32da48ac8111c authored by Tahina Ramananandro on 14 June 2018, 22:31:20 UTC
Remove all proof annotations about modifies
Remove all proof annotations about modifies
Tip revision: 37b8a39
Hacl.Chacha20.Vec128.fst.hints
[
"FW>xRx`�\u000e�\\*��`W",
[
[
"Hacl.Chacha20.Vec128.chacha20",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_Prims.HasEq_int", "eq2-interp",
"equation_FStar.Buffer.as_seq", "equation_FStar.Buffer.buffer",
"equation_FStar.Buffer.equal", "equation_FStar.UInt.uint_t",
"equation_FStar.UInt32.n",
"equation_Hacl.Chacha20.Vec128.op_String_Access",
"equation_Hacl.Impl.Chacha20.Vec128.uint8_p",
"equation_Spec.Chacha20.blocklen",
"equation_Spec.Chacha20.chacha20_ctx",
"equation_Spec.Chacha20.keylen", "equation_Spec.Chacha20.noncelen",
"equation_Spec.Chacha20_vec.blocklen",
"equation_Spec.Chacha20_vec.keylen",
"equation_Spec.Chacha20_vec.noncelen",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"fuel_guarded_inversion_FStar.Monotonic.HyperStack.mem",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.t",
"haseqHacl.Chacha20.Vec128_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
"haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
"int_inversion", "lemma_FStar.Buffer.no_upd_lemma_1",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"proj_equation_Spec.CTR.Mkblock_cipher_ctx_blocklen",
"proj_equation_Spec.CTR.Mkblock_cipher_ctx_counterbits",
"proj_equation_Spec.CTR.Mkblock_cipher_ctx_incr",
"proj_equation_Spec.CTR.Mkblock_cipher_ctx_keylen",
"proj_equation_Spec.CTR.Mkblock_cipher_ctx_noncelen",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.CTR.Mkblock_cipher_ctx_blocklen",
"projection_inverse_Spec.CTR.Mkblock_cipher_ctx_counterbits",
"projection_inverse_Spec.CTR.Mkblock_cipher_ctx_incr",
"projection_inverse_Spec.CTR.Mkblock_cipher_ctx_keylen",
"projection_inverse_Spec.CTR.Mkblock_cipher_ctx_noncelen",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_FStar.UInt_Tm_refine_a347709bfeba48709474ad26f4f6be87",
"refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_655f435aca33aabc4a1ca1fab5c827b9",
"refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_89cfbffaea7abb55d8cc65915541f2c9",
"refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_94403ae1db118a2daa8d61fa9d371d82",
"refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_df99644bbde6f04a0650fc350b008827",
"refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
"typing_FStar.Buffer.as_seq", "typing_FStar.UInt32.v"
],
0,
"2cf0ca557a30f3cb52b642e7d71db505"
],
[
"Hacl.Chacha20.Vec128.chacha20",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_Prims.HasEq_int", "equation_FStar.Buffer.buffer",
"equation_FStar.UInt32.n",
"equation_Hacl.Chacha20.Vec128.op_String_Access",
"equation_Hacl.Impl.Chacha20.Vec128.uint8_p",
"equation_Spec.Chacha20_vec.keylen",
"equation_Spec.Chacha20_vec.noncelen",
"fuel_guarded_inversion_FStar.Buffer._buffer",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.t",
"haseqHacl.Chacha20.Vec128_Tm_refine_1ec852aff28ab568526a8c54c3e853ec",
"haseqHacl.Spec.Endianness_Tm_refine_7f014d1f670e5d2ecdc0d7946b4a693d",
"refinement_interpretation_FStar.Buffer_Tm_refine_ac61996218e7c5b51c85527152e93166",
"refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_5ecfbc3b1fb0a18cc9b570ff75576d79",
"refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_655f435aca33aabc4a1ca1fab5c827b9",
"refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_89cfbffaea7abb55d8cc65915541f2c9",
"refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_94403ae1db118a2daa8d61fa9d371d82",
"refinement_interpretation_Hacl.Chacha20.Vec128_Tm_refine_ea0cdb077ae78da455b9677f874da9dd",
"typing_FStar.Buffer.as_seq"
],
0,
"a1f212454d357e81397a9e649d9318a4"
]
]
]