Revision c596c6bb21e6e478e0b46159ef182ccce6a695cb authored by Konrad Kohbrok on 16 April 2018, 13:51:58 UTC, committed by Konrad Kohbrok on 16 April 2018, 13:51:58 UTC
1 parent 68d3953
Spec.Chacha20Poly1305.fst.hints
[
"\u0012\bN}\u0014Ìê\u001f覈\u001eë\t«ý",
[
[
"Spec.Chacha20Poly1305.key",
1,
0,
0,
[
"@query", "equation_Spec.Chacha20Poly1305.keylen",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Spec.Chacha20Poly1305.nonce",
1,
0,
0,
[
"@query", "equation_Spec.Chacha20Poly1305.noncelen",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Spec.Chacha20Poly1305.bytes",
1,
0,
0,
[ "@query", "projection_inverse_BoxInt_proj_0" ],
0
],
[
"Spec.Chacha20Poly1305.pad_16",
1,
0,
0,
[
"@query", "b2t_def", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt32.n",
"equation_FStar.UInt8.n", "equation_Prims.nat", "equation_Prims.pos",
"fuel_correspondence_Prims.pow2.fuel_instrumented",
"function_token_typing_FStar.UInt32.n",
"function_token_typing_FStar.UInt8.n",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Prims.pow2"
],
0
],
[
"Spec.Chacha20Poly1305.pad_16",
2,
0,
0,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.Chacha20Poly1305.poly1305_aad",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"equation_FStar.Mul.op_Star", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt32.uint_to_t",
"equation_FStar.UInt32.v", "equation_FStar.UInt8.t",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Chacha20.block", "equation_Spec.Chacha20.blocklen",
"equation_Spec.Chacha20.chacha20_block",
"equation_Spec.Chacha20.keylen",
"equation_Spec.Chacha20Poly1305.bytes",
"equation_Spec.Chacha20Poly1305.key",
"equation_Spec.Chacha20Poly1305.keylen", "equation_Spec.Lib.lbytes",
"int_typing", "kinding_FStar.UInt8.t_@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "proj_equation_FStar.UInt32.Mk_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.UInt32.Mk_v",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_FStar.Seq.Base_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Prims_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"refinement_interpretation_Spec.Chacha20Poly1305_Tm_refine_6f26e0f319127d2eaaacb2de398dad6c",
"typing_FStar.Seq.Base.length", "typing_Prims.pow2"
],
0
],
[
"Spec.Chacha20Poly1305.aead_chacha20_poly1305_encrypt",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_FStar.UInt8.t", "equation_Prims.nat",
"equation_Spec.Chacha20.blocklen",
"equation_Spec.Chacha20Poly1305.bytes", "int_typing",
"kinding_FStar.UInt8.t_@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.Chacha20Poly1305_Tm_refine_6f26e0f319127d2eaaacb2de398dad6c",
"typing_FStar.Seq.Base.length"
],
0
],
[
"Spec.Chacha20Poly1305.aead_chacha20_poly1305_encrypt",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"equation_FStar.Mul.op_Star", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt8.t",
"equation_Spec.Chacha20.blocklen",
"equation_Spec.Chacha20.chacha20_ctx",
"equation_Spec.Chacha20.keylen", "equation_Spec.Chacha20.noncelen",
"equation_Spec.Chacha20Poly1305.bytes",
"equation_Spec.Chacha20Poly1305.key",
"equation_Spec.Chacha20Poly1305.keylen",
"equation_Spec.Chacha20Poly1305.noncelen",
"equation_Spec.Lib.lbytes", "kinding_FStar.UInt8.t_@tok",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"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_BoxBool_proj_0",
"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.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Spec.Chacha20Poly1305_Tm_refine_6f26e0f319127d2eaaacb2de398dad6c",
"typing_FStar.Seq.Base.length"
],
0
],
[
"Spec.Chacha20Poly1305.aead_chacha20_poly1305_decrypt",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_FStar.UInt8.t", "equation_Prims.nat",
"equation_Spec.Chacha20.blocklen",
"equation_Spec.Chacha20Poly1305.bytes", "int_typing",
"kinding_FStar.UInt8.t_@tok", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Spec.Chacha20Poly1305_Tm_refine_6f26e0f319127d2eaaacb2de398dad6c",
"typing_FStar.Seq.Base.length"
],
0
],
[
"Spec.Chacha20Poly1305.aead_chacha20_poly1305_decrypt",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.Mul.op_Star", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt8.t",
"equation_Spec.Chacha20.blocklen",
"equation_Spec.Chacha20.chacha20_ctx",
"equation_Spec.Chacha20.keylen", "equation_Spec.Chacha20.noncelen",
"equation_Spec.Chacha20Poly1305.bytes",
"equation_Spec.Chacha20Poly1305.key",
"equation_Spec.Chacha20Poly1305.keylen",
"equation_Spec.Chacha20Poly1305.noncelen",
"equation_Spec.Lib.lbytes", "kinding_FStar.UInt8.t_@tok",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"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_BoxBool_proj_0",
"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.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Spec.Chacha20Poly1305_Tm_refine_6f26e0f319127d2eaaacb2de398dad6c",
"typing_FStar.Seq.Base.length"
],
0
],
[
"Spec.Chacha20Poly1305.aead_chacha20_poly1305_decrypt",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"assumption_FStar.Seq.Base.seq_haseq",
"assumption_FStar.UInt8.t__haseq", "assumption_Prims.HasEq_int",
"equation_FStar.UInt8.t", "equation_Prims.nat",
"haseqPrims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"haseqSpec.Chacha20Poly1305_Tm_refine_3074964b5d8d3a92c5e95cf66d069e80",
"int_typing", "kinding_FStar.UInt8.t_@tok",
"projection_inverse_BoxInt_proj_0"
],
0
],
[
"Spec.Chacha20Poly1305.test",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_FStar.UInt8.t", "equation_Spec.Chacha20.blocklen",
"equation_Spec.Chacha20Poly1305.bytes",
"equation_Spec.Chacha20Poly1305.k",
"equation_Spec.Chacha20Poly1305.keylen",
"equation_Spec.Chacha20Poly1305.noncelen",
"equation_Spec.Lib.lbytes",
"function_token_typing_Spec.Chacha20Poly1305.k",
"kinding_FStar.UInt8.t_@tok", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Spec.Chacha20Poly1305_Tm_refine_6f26e0f319127d2eaaacb2de398dad6c",
"typing_FStar.List.Tot.Base.length"
],
0
],
[
"Spec.Chacha20Poly1305.test",
2,
0,
0,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.Chacha20Poly1305.test",
3,
0,
0,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.Chacha20Poly1305.test",
4,
0,
0,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.Chacha20Poly1305.test",
5,
0,
0,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.Chacha20Poly1305.test",
6,
0,
0,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.Chacha20Poly1305.test",
7,
0,
0,
[ "@query", "assumption_Prims.HasEq_int" ],
0
],
[
"Spec.Chacha20Poly1305.test",
8,
0,
0,
[
"@query", "assumption_FStar.Seq.Base.seq_haseq",
"assumption_FStar.UInt8.t__haseq", "equation_FStar.UInt8.t",
"kinding_FStar.UInt8.t_@tok"
],
0
],
[
"Spec.Chacha20Poly1305.test",
9,
0,
0,
[
"@query", "assumption_FStar.Seq.Base.seq_haseq",
"assumption_FStar.UInt8.t__haseq", "equation_FStar.UInt8.t",
"kinding_FStar.UInt8.t_@tok"
],
0
],
[
"Spec.Chacha20Poly1305.test",
10,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_FStar.Pervasives.Native.option_haseq",
"assumption_FStar.Seq.Base.seq_haseq",
"assumption_FStar.UInt8.t__haseq", "equation_FStar.UInt8.t",
"equation_Spec.Chacha20Poly1305.bytes", "equation_Spec.Lib.lbytes",
"haseqFStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"kinding_FStar.UInt8.t_@tok",
"refinement_interpretation_FStar.BitVector_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Spec.Chacha20Poly1305_Tm_refine_6f26e0f319127d2eaaacb2de398dad6c",
"typing_FStar.Seq.Base.length", "typing_Spec.Lib.lbytes"
],
0
]
]
]
Computing file changes ...
