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
Spec.Chacha20.fst.hints
[
"�/�}L\u0018\u0013\u001aE��ϕ5bL",
[
[
"Spec.Chacha20.key",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat", "equation_Spec.Chacha20.size_key",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"63362b27ea97afae9d279d293ff6cb17"
],
[
"Spec.Chacha20.block",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat", "equation_Spec.Chacha20.size_block",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"3748996521dbeb83b87405d11d90f3d4"
],
[
"Spec.Chacha20.nonce",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat", "equation_Spec.Chacha20.size_nonce",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"d3f166be05454de53335ec48e05a145e"
],
[
"Spec.Chacha20.state",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"445d5bf47e167532e94cc33cc321871c"
],
[
"Spec.Chacha20.line",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.rotval", "equation_Lib.IntTypes.uint32",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Chacha20.idx", "equation_Spec.Chacha20.state",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1ea68a279729ff6339fd1b6dd1b3240d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_ca66e862440932a48c8f6220ee94a170",
"refinement_interpretation_Tm_refine_cdc36a88bd3b51d8ada6273fa2e8c71d",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"bcd717f24048b9e2968bb795709a3f5e"
],
[
"Spec.Chacha20.quarter_round",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.size", "equation_Prims.nat",
"equation_Spec.Chacha20.size_nonce",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_e7baecf1446b738b3604b097069629a3",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.uint",
"typing_Spec.Chacha20.size_nonce", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"9ff32a0d32ceaec1c14a7b3e1208ba1f"
],
[
"Spec.Chacha20.column_round",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Chacha20.size_key",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Prims.pow2", "typing_Spec.Chacha20.size_key"
],
0,
"f4381ef73f90ee4e090b477ac035905a"
],
[
"Spec.Chacha20.diagonal_round",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Chacha20.size_key",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Prims.pow2", "typing_Spec.Chacha20.size_key"
],
0,
"b06d96f0ba9f9b79122273850981871b"
],
[
"Spec.Chacha20.sum_state",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"c90dfd3d24f129a8a105dce4bc77b718"
],
[
"Spec.Chacha20.add_counter",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"1969d808acaef18487c2f668ec9f5900"
],
[
"Spec.Chacha20.chacha20_constants",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat", "equation_Spec.Chacha20.size_key",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Spec.Chacha20.size_key"
],
0,
"d6c43bf0868f7196b20d44be04c009c1"
],
[
"Spec.Chacha20.setup",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint32",
"equation_Lib.IntTypes.uint8", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.Chacha20.chacha20_constants",
"equation_Spec.Chacha20.counter", "equation_Spec.Chacha20.key",
"equation_Spec.Chacha20.size_key", "equation_Spec.Chacha20.state",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_17d83e88725a541d974ce3b0e2cf7136",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_8dcb417a772f6c5e7ae392dac31c7530",
"refinement_interpretation_Tm_refine_94f861c3dbd34b89a580014c6ecbf1c5",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de6c87a3d985f153a087e0711048d944",
"refinement_interpretation_Tm_refine_f3b05e043b07af88e4da4693a6a4c220",
"refinement_interpretation_Tm_refine_ffa64495c1bd1fe762a1617a9b87f7bc",
"typing_FStar.Seq.Base.length"
],
0,
"067d9427ef4e086c00ac2212e8b5a267"
],
[
"Spec.Chacha20.setup_",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Spec.Chacha20.key", "equation_Spec.Chacha20.size_key",
"function_token_typing_Lib.IntTypes.uint8",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length"
],
0,
"64ceb623c5e25b52572704aeb5813709"
],
[
"Spec.Chacha20.chacha20_init",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.uint8", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Spec.Chacha20.key",
"equation_Spec.Chacha20.size_key",
"function_token_typing_Lib.IntTypes.uint8",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length"
],
0,
"363ae9ed6155f2367f8c1eba6ad5e624"
],
[
"Spec.Chacha20.chacha20_set_counter",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"424e87d1eac894c818ed75668ef43bca"
],
[
"Spec.Chacha20.chacha20_key_block0",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint8",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.pos", "equation_Spec.Chacha20.key",
"equation_Spec.Chacha20.size_key",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_FStar.Seq.Base.length", "typing_Prims.pow2"
],
0,
"9b860d0eb08ca147b49d78d839cb5a87"
],
[
"Spec.Chacha20.xor_block",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Prims.nat",
"equation_Spec.Chacha20.size_key",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Spec.Chacha20.size_key"
],
0,
"a206a76eb5e4ccbe886bf6da743c3d0b"
],
[
"Spec.Chacha20.chacha20_encrypt_last",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.uint_v",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Spec.Chacha20.size_block",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1d4d2f8b8fbff081eab2b93d03e505db",
"refinement_interpretation_Tm_refine_2916d2aac0fcf68a5f50242b2777e093",
"refinement_interpretation_Tm_refine_5b2f5014684740e0d3c157810833864e",
"refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
"refinement_interpretation_Tm_refine_985eae0e8197d947f04b8bd48b48f67b",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"e3f371bcb410308db63afb04467b4080"
],
[
"Spec.Chacha20.chacha20_update",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat", "equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Spec.Chacha20.size_key"
],
0,
"a4a7a7ba5a19f12483d24a483fea9370"
],
[
"Spec.Chacha20.chacha20_update",
2,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Prims.nat", "equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_Spec.Chacha20.size_key"
],
0,
"6bed2801d2a25f5aca05b9981e261842"
],
[
"Spec.Chacha20.chacha20_update",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.uint_v",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20.state",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Prims.__cache_version_number__",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0e9f32456d359fe7dfefb11c65a88a34",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
"refinement_interpretation_Tm_refine_a023f390483b324d20370f23ed0795dc",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.uint_v", "typing_Lib.Sequence.index",
"typing_Spec.Chacha20.size_nonce", "typing_tok_Lib.IntTypes.SEC@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"1cd4032c323e36089f5399641c87a6e1"
],
[
"Spec.Chacha20.chacha20_encrypt_bytes",
1,
0,
1,
[
"@query", "equation_Spec.Chacha20.size_block",
"projection_inverse_BoxInt_proj_0"
],
0,
"7dd9800c4f729f2489f76b881d79a581"
],
[
"Spec.Chacha20.chacha20_encrypt_bytes",
2,
0,
1,
[
"@query", "equation_Spec.Chacha20.size_block",
"projection_inverse_BoxInt_proj_0"
],
0,
"f9e102bc15709f53ae376d7483e624cf"
],
[
"Spec.Chacha20.chacha20_encrypt_bytes",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Spec.Chacha20_interpretation_Tm_arrow_ca10d6ab9df780d1c8bdc8ab7639176e",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.size_t",
"equation_Lib.IntTypes.u32", "equation_Lib.IntTypes.uint32",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.uint_v",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.Chacha20.chacha20_constants",
"equation_Spec.Chacha20.chacha20_init",
"equation_Spec.Chacha20.counter", "equation_Spec.Chacha20.key",
"equation_Spec.Chacha20.nonce", "equation_Spec.Chacha20.setup",
"equation_Spec.Chacha20.size_key",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20.state",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.__cache_version_number__", "int_typing",
"lemma_Lib.IntTypes.pow2_values",
"partial_app_typing_96ee34eab48dac8467b7ad56a11543af",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_4727b13a1b784fdaac756067cab5a811",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
"refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
"refinement_interpretation_Tm_refine_821e27eade7723db8acd26afdaff1037",
"refinement_interpretation_Tm_refine_8bdecfb5d16fa4a517d5fa57acd2da6d",
"refinement_interpretation_Tm_refine_b2dc89f387bfa24b5213901f5d1fd0a7",
"refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_cf14376579474f96d93270c75f31a45f",
"refinement_interpretation_Tm_refine_d856f709de20bfa4e940d47b1570ef4d",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f17ce12623fb5401c9c6496441382e03",
"refinement_interpretation_Tm_refine_f25e99b5e06e76eab911df032fe48dbc",
"token_correspondence_Lib.IntTypes.secret",
"typing_FStar.Seq.Base.length",
"typing_Lib.ByteSequence.uints_from_bytes_le",
"typing_Lib.IntTypes.u32", "typing_Lib.Sequence.create",
"typing_Lib.Sequence.map", "typing_Lib.Sequence.upd",
"typing_Lib.Sequence.update_sub",
"typing_Spec.Chacha20.chacha20_constants",
"typing_Spec.Chacha20.chacha20_init",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"aecc6b4cb594cc5fb7c0d4f0a2db1829"
],
[
"Spec.Chacha20.chacha20_decrypt_bytes",
1,
0,
1,
[
"@query", "equation_Spec.Chacha20.size_block",
"projection_inverse_BoxInt_proj_0"
],
0,
"2e49dc71df6ee209563320cce9cbaff9"
],
[
"Spec.Chacha20.chacha20_decrypt_bytes",
2,
0,
1,
[
"@query", "equation_Spec.Chacha20.size_block",
"projection_inverse_BoxInt_proj_0"
],
0,
"a7f3004881dfa4cb6503fef284fe7843"
],
[
"Spec.Chacha20.chacha20_decrypt_bytes",
3,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_interpretation_Tm_arrow_9cb3c953faf527c316d427b2ce8bd81b",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Spec.Chacha20_interpretation_Tm_arrow_ca10d6ab9df780d1c8bdc8ab7639176e",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.size_t",
"equation_Lib.IntTypes.u32", "equation_Lib.IntTypes.uint32",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.uint_v",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.Chacha20.chacha20_constants",
"equation_Spec.Chacha20.chacha20_init",
"equation_Spec.Chacha20.counter", "equation_Spec.Chacha20.key",
"equation_Spec.Chacha20.nonce", "equation_Spec.Chacha20.setup",
"equation_Spec.Chacha20.size_key",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20.state",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "lemma_Lib.IntTypes.pow2_values",
"partial_app_typing_96ee34eab48dac8467b7ad56a11543af",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_4727b13a1b784fdaac756067cab5a811",
"refinement_interpretation_Tm_refine_4c640aac30047af80af31869dcf9d35b",
"refinement_interpretation_Tm_refine_5a4fe33be2b93c781e552e491bb9dd31",
"refinement_interpretation_Tm_refine_70597463dd221580f371f83615527f81",
"refinement_interpretation_Tm_refine_78ea63ceb027a3f1c790955bc68a707b",
"refinement_interpretation_Tm_refine_821e27eade7723db8acd26afdaff1037",
"refinement_interpretation_Tm_refine_8bdecfb5d16fa4a517d5fa57acd2da6d",
"refinement_interpretation_Tm_refine_b2dc89f387bfa24b5213901f5d1fd0a7",
"refinement_interpretation_Tm_refine_b7c6ab0416aa19b9be0f0ab3d684c8cc",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_cf14376579474f96d93270c75f31a45f",
"refinement_interpretation_Tm_refine_d856f709de20bfa4e940d47b1570ef4d",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_f17ce12623fb5401c9c6496441382e03",
"refinement_interpretation_Tm_refine_f25e99b5e06e76eab911df032fe48dbc",
"token_correspondence_Lib.IntTypes.secret",
"typing_FStar.Seq.Base.length",
"typing_Lib.ByteSequence.uints_from_bytes_le",
"typing_Lib.IntTypes.u32", "typing_Lib.Sequence.create",
"typing_Lib.Sequence.map", "typing_Lib.Sequence.upd",
"typing_Lib.Sequence.update_sub",
"typing_Spec.Chacha20.chacha20_constants",
"typing_Spec.Chacha20.chacha20_init",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"feacc9ea906e758718566cc9ebc614ab"
]
]
]
Computing file changes ...
