[
"°<µ@q—\u00073mÆ=3ÿPÎJ",
[
[
"Hacl.Spec.Chacha20.Equiv.chacha20_init_scalar_lemma",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"ed520e81a5fc377c6c96ffe42d72287b"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_init_scalar_lemma",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd",
"equation_FStar.Seq.Properties.split",
"equation_Hacl.Spec.Chacha20.Vec.c0",
"equation_Hacl.Spec.Chacha20.Vec.c1",
"equation_Hacl.Spec.Chacha20.Vec.c2",
"equation_Hacl.Spec.Chacha20.Vec.c3",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_constants",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.nonce",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Hacl.Spec.Chacha20.Vec.size_nonce",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint32",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.op_At_Bar", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.c0", "equation_Spec.Chacha20.c1",
"equation_Spec.Chacha20.c2", "equation_Spec.Chacha20.c3",
"equation_Spec.Chacha20.chacha20_constants",
"equation_Spec.Chacha20.chacha20_init",
"equation_Spec.Chacha20.setup", "equation_Spec.Chacha20.size_key",
"equation_Spec.Chacha20.size_nonce",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Prims.int",
"function_token_typing_Spec.AES.elem",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_slice",
"lemma_FStar.Seq.Properties.slice_upd",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.Sequence.eq_elim",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_04794afcf1170d0969f10a6dd6cb6bb2",
"refinement_interpretation_Tm_refine_07e3c00f5f36be0ccf9c5cc34b067a94",
"refinement_interpretation_Tm_refine_0af5ca259dd2af8001ffb48fef2e22c5",
"refinement_interpretation_Tm_refine_0b72b617030921a422a8020811c2f320",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_1104ef1656c24daae724b2b877eaf1e7",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_12503c32aa61f087c2c1e92cfd90a57d",
"refinement_interpretation_Tm_refine_177932ae27bb622da89916ff70731255",
"refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_27680283e93f30a8d9ac7d3b22ec31bf",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_335626c2eaf67fc0a348fa9b35c6a16c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_4270b1248937acecd1355a3637aba71b",
"refinement_interpretation_Tm_refine_52e6356ebab4c2ff5f21a8697a214954",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_62f60abd66f9e5691abea0fb1a86f07d",
"refinement_interpretation_Tm_refine_677ec457f418e5bc9656a8488d2b415d",
"refinement_interpretation_Tm_refine_6dfa0aabd3eca03168e7c0b2ca9e28f0",
"refinement_interpretation_Tm_refine_7acf795d50ec256996534a97e12bfa61",
"refinement_interpretation_Tm_refine_7e3e90b0465db5acb652414f12044e9a",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8f55bbdc42d259d64eef7ece9ec1b162",
"refinement_interpretation_Tm_refine_9755734cb31a51dcd1cb3aedc6aef669",
"refinement_interpretation_Tm_refine_98f257e774755b2cad1878fbadfac5a6",
"refinement_interpretation_Tm_refine_99f14447f260f18281f5b38bd5e50414",
"refinement_interpretation_Tm_refine_9e7b7ec534a2a9a23ec52880cc32ece2",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_acae6aa8b03d229f2ea8e8fe49d8cac5",
"refinement_interpretation_Tm_refine_adf5913975d75267a2e4ab7a6ee0567f",
"refinement_interpretation_Tm_refine_b70196a9547e1e5243d93163999e93f0",
"refinement_interpretation_Tm_refine_b982c49920f17cb189b64b1977cb1ad9",
"refinement_interpretation_Tm_refine_c06bb74baf7ca2c4e87221aa34e2a953",
"refinement_interpretation_Tm_refine_c13133d0178b1be173b4fac2c5c7b32e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c30578bdd54b06389407d193becb6c7c",
"refinement_interpretation_Tm_refine_c539d77ab3c34d2a40e9413fc0d13c72",
"refinement_interpretation_Tm_refine_c91ae56ff6de446e4a00ac265e32a3d4",
"refinement_interpretation_Tm_refine_ccbef96ee6e044a9cf0b4353c2d1f06e",
"refinement_interpretation_Tm_refine_d0cfd89eb4ef1a6cf97f64b48cd2fe0c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_dfe2a8918fdd59609d3be2f34d23d76b",
"refinement_interpretation_Tm_refine_edd509798995789e68db734094d4972f",
"refinement_interpretation_Tm_refine_fad90920b494fed63d6a7c69741fbb7b",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
"typing_Lib.Sequence.index", "typing_Lib.Sequence.sub",
"typing_Lib.Sequence.to_seq", "typing_Lib.Sequence.update_sub",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"5f973bbe186002af38eaa8cac653aca0"
],
[
"Hacl.Spec.Chacha20.Equiv.add_counter_lemma_aux",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5735b1ab474347e6de95ca72d148f746",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"97b1cb03f8e183257c2a91435982dd23"
],
[
"Hacl.Spec.Chacha20.Equiv.add_counter_lemma_aux",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.IntVector.width",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "int_typing", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.add_mod_lemma", "lemma_Lib.IntTypes.v_injective",
"primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f8afeac9e2ffeddc59f60e88d12cebc",
"refinement_interpretation_Tm_refine_27680283e93f30a8d9ac7d3b22ec31bf",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5735b1ab474347e6de95ca72d148f746",
"refinement_interpretation_Tm_refine_6140b6af3dde6fccc61c8c2fbb95f76d",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_9b478475b04df0ab8fa7def9b7e13f10",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"ed3b28edc450f66fa6620b427f7a0551"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_core_scalar_lemma",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.state", "equation_Spec.GaloisField.gf",
"int_inversion", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5735b1ab474347e6de95ca72d148f746",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"53c91488e42e7f31f4ed40a27a113782"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_core_scalar_lemma",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9",
"Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
"Spec.Chacha20_interpretation_Tm_arrow_4b33d7ce430158ea8a765f054f81aab2",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Chacha20.chacha20_add_counter",
"equation_Spec.Chacha20.chacha20_core",
"equation_Spec.Chacha20.rounds", "equation_Spec.Chacha20.shuffle",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20.state",
"equation_Spec.Chacha20.sum_state", "equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.add_mod",
"function_token_typing_Lib.IntTypes.uint32", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_mod_lemma",
"lemma_Lib.IntTypes.v_injective", "lemma_Lib.Sequence.eq_elim",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f8afeac9e2ffeddc59f60e88d12cebc",
"refinement_interpretation_Tm_refine_1b2331b6c4b36f26f6b70b89a12a667d",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5735b1ab474347e6de95ca72d148f746",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_5fc72a0921f08146665e361716c12b50",
"refinement_interpretation_Tm_refine_62f60abd66f9e5691abea0fb1a86f07d",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
"refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90",
"refinement_interpretation_Tm_refine_9b478475b04df0ab8fa7def9b7e13f10",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.mk_int", "typing_Lib.Sequence.index",
"typing_Lib.Sequence.map2", "typing_Lib.Sequence.upd",
"typing_Spec.AES.gf8", "typing_Spec.Chacha20.rounds",
"typing_Spec.Chacha20.size_nonce", "typing_Spec.Chacha20.sum_state",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"1f717108d01a7db8b4c19284c6e0449a"
],
[
"Hacl.Spec.Chacha20.Equiv.kb_equiv_lemma",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5735b1ab474347e6de95ca72d148f746",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"96bfb62e86717356fc4f53e05f4c23ae"
],
[
"Hacl.Spec.Chacha20.Equiv.kb_equiv_lemma",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"Lib.IntTypes_interpretation_Tm_arrow_feb4494e55abb95bc979559ccab03ad0",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.c0",
"equation_Hacl.Spec.Chacha20.Vec.c1",
"equation_Hacl.Spec.Chacha20.Vec.c2",
"equation_Hacl.Spec.Chacha20.Vec.c3",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_constants",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.nonce",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Hacl.Spec.Chacha20.Vec.size_nonce",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.size_t",
"equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.op_At_Bar",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.c0", "equation_Spec.Chacha20.c1",
"equation_Spec.Chacha20.c2", "equation_Spec.Chacha20.c3",
"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",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.secret",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0b72b617030921a422a8020811c2f320",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5735b1ab474347e6de95ca72d148f746",
"refinement_interpretation_Tm_refine_576183a4f8267f6296f94f4827351efd",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0",
"refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_ccbef96ee6e044a9cf0b4353c2d1f06e",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_fb77d4109290540100357b20e0a78486",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"token_correspondence_Lib.IntTypes.secret",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
"typing_Hacl.Spec.Chacha20.Vec.chacha20_constants",
"typing_Lib.ByteSequence.uints_from_bytes_le",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.mk_int", "typing_Lib.Sequence.create",
"typing_Lib.Sequence.index", "typing_Lib.Sequence.map",
"typing_Lib.Sequence.op_At_Bar", "typing_Lib.Sequence.to_seq",
"typing_Lib.Sequence.upd", "typing_Lib.Sequence.update_sub",
"typing_Spec.AES.gf8", "typing_Spec.Chacha20.chacha20_init",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"c88180ea069c4a1f6b70d71b7858d83d"
],
[
"Hacl.Spec.Chacha20.Equiv.line_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.rotval",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0da46ef8643a6f8ea97a3358bc923338",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"0ba2197c4ee2c7f9d5764075b5d5215b"
],
[
"Hacl.Spec.Chacha20.Equiv.line_lemma_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Hacl.Spec.Chacha20.Vec_interpretation_Tm_arrow_a4060274569c7f2a838e81ea9e2cc28d",
"Lib.IntTypes_interpretation_Tm_arrow_8d531434920b1f664c07622b1f3aa2cb",
"Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9",
"Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b",
"Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U128@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.idx",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.line",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Hacl.Spec.Chacha20.Vec.uint32xN",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.rotate_left_i",
"equation_Lib.IntTypes.rotval", "equation_Lib.IntTypes.uint32",
"equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.op_Hat_Bar",
"equation_Lib.IntVector.op_Less_Less_Less_Bar",
"equation_Lib.IntVector.op_Plus_Bar",
"equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t",
"equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.line", "equation_Spec.Chacha20.size_nonce",
"equation_Spec.Chacha20.state", "equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.add_mod",
"function_token_typing_Lib.IntTypes.logxor",
"function_token_typing_Lib.IntTypes.rotate_left_i",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Prims.int",
"function_token_typing_Spec.Chacha20.state",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_daf746fa65a87ec0bf08afd7e16e4e61",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
"lemma_Lib.IntVector.vec_add_mod_lemma",
"lemma_Lib.IntVector.vec_rotate_left_lemma",
"lemma_Lib.IntVector.vec_xor_lemma",
"lemma_Lib.Sequence.create16_lemma", "lemma_Lib.Sequence.eq_elim",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0da46ef8643a6f8ea97a3358bc923338",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_3a68a9425e73ad476d657ea83d7d4192",
"refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_555a5d074c16bb965409b6eaa26909b7",
"refinement_interpretation_Tm_refine_5605dbd4da3cfae23467df5c86d0e6c3",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_62f60abd66f9e5691abea0fb1a86f07d",
"refinement_interpretation_Tm_refine_6f7719d2e9422e645682674727002c0b",
"refinement_interpretation_Tm_refine_798fffae8246ef9874cae28fec41f80c",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
"refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67",
"refinement_interpretation_Tm_refine_b781535c52aef96ef495875b5f58725b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c31bfb27d051fea31b6e0ff61c76fd40",
"refinement_interpretation_Tm_refine_c9d824e9d15067e06b6c696358984852",
"refinement_interpretation_Tm_refine_d5c70cc818262f9c6ef5634af7433789",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_da8a86d176ea7e588c80ec05844974b3",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_ee132209fda53d9c6beffc8f2d6d495f",
"refinement_interpretation_Tm_refine_eed4d09eb128b34344be994ea8db7328",
"refinement_interpretation_Tm_refine_fe1f2b0fb92318a15c076125042e53a3",
"token_correspondence_Lib.IntTypes.rotate_left_i",
"token_correspondence_Lib.IntVector.op_Hat_Bar",
"token_correspondence_Lib.IntVector.op_Less_Less_Less_Bar",
"token_correspondence_Lib.IntVector.op_Plus_Bar",
"token_correspondence_Lib.IntVector.vec_add_mod",
"token_correspondence_Lib.IntVector.vec_rotate_left",
"token_correspondence_Lib.IntVector.vec_xor",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Spec.Chacha20.Vec.transpose_state",
"typing_Hacl.Spec.Chacha20.Vec.uint32xN", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.rotate_left",
"typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.createi",
"typing_Lib.Sequence.index", "typing_Lib.Sequence.map",
"typing_Lib.Sequence.map2", "typing_Lib.Sequence.upd",
"typing_Spec.AES.gf8", "typing_Spec.Chacha20.size_nonce",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Tm_abs_daf746fa65a87ec0bf08afd7e16e4e61",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"415c8ce0329a498c06e11f686fd4db87"
],
[
"Hacl.Spec.Chacha20.Equiv.quarter_round_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"b189a7affe2859aa372eb1ef3992d5b4"
],
[
"Hacl.Spec.Chacha20.Equiv.quarter_round_lemma_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.idx",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.op_At",
"equation_Hacl.Spec.Chacha20.Vec.quarter_round",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Chacha20.idx",
"equation_Spec.Chacha20.op_At",
"equation_Spec.Chacha20.quarter_round",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20.state",
"equation_Spec.GaloisField.gf",
"function_token_typing_Hacl.Spec.Chacha20.Vec.line",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Spec.Chacha20.line",
"function_token_typing_Spec.Chacha20.state", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.v_mk_int",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5605dbd4da3cfae23467df5c86d0e6c3",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_6f7719d2e9422e645682674727002c0b",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c6feac2aa24aad15055cb8a088fbc725",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"token_correspondence_Hacl.Spec.Chacha20.Vec.op_At",
"token_correspondence_Hacl.Spec.Chacha20.Vec.quarter_round",
"token_correspondence_Spec.Chacha20.line",
"token_correspondence_Spec.Chacha20.op_At",
"token_correspondence_Spec.Chacha20.quarter_round",
"typing_Hacl.Spec.Chacha20.Vec.transpose_state",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.mk_int",
"typing_Lib.IntTypes.v", "typing_Lib.Sequence.index",
"typing_Spec.AES.gf8", "typing_Spec.Chacha20.line",
"typing_Spec.Chacha20.size_nonce",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"6e4898e66fe6db3bee1cf4ff872a8275"
],
[
"Hacl.Spec.Chacha20.Equiv.column_round_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"044331a6f65fb0f3f525a8a743fc7431"
],
[
"Hacl.Spec.Chacha20.Equiv.column_round_lemma_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Spec.Chacha20_interpretation_Tm_arrow_4b33d7ce430158ea8a765f054f81aab2",
"Spec.Chacha20_interpretation_Tm_arrow_9fea18bc71360024910da8573c78716e",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.column_round",
"equation_Hacl.Spec.Chacha20.Vec.idx",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.op_At",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint32",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Chacha20.column_round",
"equation_Spec.Chacha20.idx", "equation_Spec.Chacha20.op_At",
"equation_Spec.Chacha20.quarter_round",
"equation_Spec.Chacha20.shuffle",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20.state",
"equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Spec.Chacha20.quarter_round",
"function_token_typing_Spec.Chacha20.state", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_3f264366769b519c220f75be46303d08",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5605dbd4da3cfae23467df5c86d0e6c3",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_6f7719d2e9422e645682674727002c0b",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"token_correspondence_Hacl.Spec.Chacha20.Vec.column_round",
"token_correspondence_Hacl.Spec.Chacha20.Vec.op_At",
"token_correspondence_Hacl.Spec.Chacha20.Vec.quarter_round",
"token_correspondence_Spec.Chacha20.op_At",
"token_correspondence_Spec.Chacha20.quarter_round",
"typing_Hacl.Spec.Chacha20.Vec.transpose_state",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.v", "typing_Lib.Sequence.index",
"typing_Spec.AES.gf8", "typing_Spec.AES.irred",
"typing_Spec.Chacha20.size_nonce",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"8763c328c08f01c5adccfba77cd29c96"
],
[
"Hacl.Spec.Chacha20.Equiv.diagonal_round_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"153a3c0a6bd482338096bdab71aeb0b0"
],
[
"Hacl.Spec.Chacha20.Equiv.diagonal_round_lemma_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Spec.Chacha20_interpretation_Tm_arrow_4b33d7ce430158ea8a765f054f81aab2",
"Spec.Chacha20_interpretation_Tm_arrow_9fea18bc71360024910da8573c78716e",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.diagonal_round",
"equation_Hacl.Spec.Chacha20.Vec.idx",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.op_At",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint32",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Chacha20.diagonal_round",
"equation_Spec.Chacha20.idx", "equation_Spec.Chacha20.op_At",
"equation_Spec.Chacha20.quarter_round",
"equation_Spec.Chacha20.shuffle",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20.state",
"equation_Spec.GaloisField.gf",
"function_token_typing_Hacl.Spec.Chacha20.Vec.op_At",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Spec.Chacha20.quarter_round",
"function_token_typing_Spec.Chacha20.state", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5605dbd4da3cfae23467df5c86d0e6c3",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_6f7719d2e9422e645682674727002c0b",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_cb4549f0ec0c35e6edd202313f2e3930",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"token_correspondence_Hacl.Spec.Chacha20.Vec.diagonal_round",
"token_correspondence_Hacl.Spec.Chacha20.Vec.op_At",
"token_correspondence_Hacl.Spec.Chacha20.Vec.quarter_round",
"token_correspondence_Spec.Chacha20.op_At",
"token_correspondence_Spec.Chacha20.quarter_round",
"typing_Hacl.Spec.Chacha20.Vec.transpose_state",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.v", "typing_Lib.Sequence.index",
"typing_Spec.AES.gf8", "typing_Spec.AES.irred",
"typing_Spec.Chacha20.size_nonce",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"109896a4d6cc30ff905da867c64a5a2d"
],
[
"Hacl.Spec.Chacha20.Equiv.double_round_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"f2b2bb72f3d70b2afb1502e269598705"
],
[
"Hacl.Spec.Chacha20.Equiv.double_round_lemma_i",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Hacl.Spec.Chacha20.Vec_interpretation_Tm_arrow_a4060274569c7f2a838e81ea9e2cc28d",
"Spec.Chacha20_interpretation_Tm_arrow_4b33d7ce430158ea8a765f054f81aab2",
"equation_Hacl.Spec.Chacha20.Vec.double_round",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.op_At",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Lib.IntTypes.uint32", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.Chacha20.column_round",
"equation_Spec.Chacha20.diagonal_round",
"equation_Spec.Chacha20.double_round",
"equation_Spec.Chacha20.op_At",
"equation_Spec.Chacha20.quarter_round",
"equation_Spec.Chacha20.shuffle", "equation_Spec.Chacha20.state",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Spec.Chacha20.state", "int_inversion",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"token_correspondence_Hacl.Spec.Chacha20.Vec.column_round",
"token_correspondence_Hacl.Spec.Chacha20.Vec.diagonal_round",
"token_correspondence_Hacl.Spec.Chacha20.Vec.double_round",
"token_correspondence_Hacl.Spec.Chacha20.Vec.op_At",
"token_correspondence_Spec.Chacha20.op_At",
"typing_Lib.Sequence.createi", "typing_Spec.Chacha20.column_round",
"typing_Spec.Chacha20.diagonal_round", "typing_Spec.Chacha20.op_At",
"typing_Tm_abs_daf746fa65a87ec0bf08afd7e16e4e61"
],
0,
"c73e0b6d0fefa7f2af3dcb798cd58cc9"
],
[
"Hacl.Spec.Chacha20.Equiv.scalar_rounds_unroll_lemma",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_Hacl.Spec.Chacha20.Equiv.scalar_rounds",
"equation_Lib.IntTypes.uint32", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Spec.Chacha20.double_round",
"equation_Spec.Chacha20.rounds", "equation_Spec.Chacha20.state",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Lib.LoopCombinators.repeat",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Hacl.Spec.Chacha20.Equiv.scalar_rounds"
],
0,
"1a26cb2b139ef2fdba6a077a71461413"
],
[
"Hacl.Spec.Chacha20.Equiv.rounds_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"583ab21f9239f45070407d2dec228d70"
],
[
"Hacl.Spec.Chacha20.Equiv.rounds_lemma_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Hacl.Spec.Chacha20.Vec_interpretation_Tm_arrow_07e810fae05085a14d274f070c6516bb",
"Hacl.Spec.Chacha20.Vec_interpretation_Tm_arrow_da59c35bb903b57bfda5660ba4ce773d",
"Spec.Chacha20_interpretation_Tm_arrow_4b33d7ce430158ea8a765f054f81aab2",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.scalar_rounds",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.rounds",
"equation_Hacl.Spec.Chacha20.Vec.shuffle",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Chacha20.double_round",
"equation_Spec.Chacha20.shuffle", "equation_Spec.Chacha20.state",
"equation_Spec.GaloisField.gf",
"function_token_typing_Hacl.Spec.Chacha20.Vec.double_round",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Spec.Chacha20.state", "int_inversion",
"lemma_FStar.Seq.Base.lemma_eq_elim", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5605dbd4da3cfae23467df5c86d0e6c3",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f57b857c54258c85c6acfa6699b4bbd3",
"token_correspondence_Hacl.Spec.Chacha20.Vec.double_round",
"token_correspondence_Spec.Chacha20.op_At",
"typing_Hacl.Spec.Chacha20.Vec.transpose_state",
"typing_Lib.IntTypes.bits", "typing_Lib.Sequence.index",
"typing_Spec.AES.gf8", "typing_Spec.Chacha20.double_round",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"c24c5371381187014d60469a43d081b6"
],
[
"Hacl.Spec.Chacha20.Equiv.sum_state_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"6bdd314888dd84ce937b994b916c7381"
],
[
"Hacl.Spec.Chacha20.Equiv.sum_state_lemma_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Hacl.Spec.Chacha20.Vec_interpretation_Tm_arrow_a4060274569c7f2a838e81ea9e2cc28d",
"Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9",
"Lib.IntVector_interpretation_Tm_arrow_52fccec682b990f2bce95a533bf79897",
"Lib.IntVector_interpretation_Tm_arrow_760746993345c1327f70c87a340d60e0",
"Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.sum_state",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Hacl.Spec.Chacha20.Vec.uint32xN",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.op_Plus_Bar",
"equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t",
"equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20.state",
"equation_Spec.Chacha20.sum_state", "equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.add_mod",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Lib.IntVector.vec_add_mod",
"function_token_typing_Spec.Chacha20.state", "int_inversion",
"int_typing",
"interpretation_Tm_abs_daf746fa65a87ec0bf08afd7e16e4e61",
"lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntVector.vec_add_mod_lemma",
"lemma_Lib.Sequence.create16_lemma", "lemma_Lib.Sequence.eq_elim",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_17d16e9c737427ac2c4296f811d628e0",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5605dbd4da3cfae23467df5c86d0e6c3",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_62f60abd66f9e5691abea0fb1a86f07d",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"token_correspondence_Lib.IntVector.vec_add_mod",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Spec.Chacha20.Vec.sum_state",
"typing_Hacl.Spec.Chacha20.Vec.uint32xN", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.minint", "typing_Lib.IntVector.op_Plus_Bar",
"typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.createi",
"typing_Lib.Sequence.index", "typing_Lib.Sequence.map2",
"typing_Spec.AES.gf8", "typing_Spec.Chacha20.size_nonce",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Tm_abs_daf746fa65a87ec0bf08afd7e16e4e61",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"3563361dd4a8fbdbcd2ab18835c33324"
],
[
"Hacl.Spec.Chacha20.Equiv.add_counter_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.width", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e8e712c693d2a3966788ccb7b46638e3",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"434bd98e8aeca3e9ee494248a4a9314c"
],
[
"Hacl.Spec.Chacha20.Equiv.add_counter_lemma_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Hacl.Spec.Chacha20.Vec_interpretation_Tm_arrow_a4060274569c7f2a838e81ea9e2cc28d",
"Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9",
"Lib.IntVector_interpretation_Tm_arrow_760746993345c1327f70c87a340d60e0",
"Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U1",
"disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.add_counter",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Hacl.Spec.Chacha20.Vec.uint32xN",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.op_Plus_Bar",
"equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t",
"equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.chacha20_add_counter",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20.state",
"equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.add_mod",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Lib.IntVector.vec_add_mod",
"function_token_typing_Spec.Chacha20.state", "int_inversion",
"int_typing",
"interpretation_Tm_abs_daf746fa65a87ec0bf08afd7e16e4e61",
"lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.IntTypes.mul_lemma", "lemma_Lib.IntTypes.v_injective",
"lemma_Lib.IntVector.vec_add_mod_lemma",
"lemma_Lib.Sequence.create16_lemma", "lemma_Lib.Sequence.eq_elim",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f8afeac9e2ffeddc59f60e88d12cebc",
"refinement_interpretation_Tm_refine_13f4756222ad7b5ca687d4b9b9007711",
"refinement_interpretation_Tm_refine_27680283e93f30a8d9ac7d3b22ec31bf",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5605dbd4da3cfae23467df5c86d0e6c3",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_62f60abd66f9e5691abea0fb1a86f07d",
"refinement_interpretation_Tm_refine_6e9be704ead8ad76f9833bf58145f462",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
"refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_9ff150f589411d5a40376aa0c5e1ca86",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e8e712c693d2a3966788ccb7b46638e3",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"token_correspondence_Lib.IntVector.op_Plus_Bar",
"token_correspondence_Lib.IntVector.vec_add_mod",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Spec.Chacha20.Vec.add_counter",
"typing_Hacl.Spec.Chacha20.Vec.uint32xN",
"typing_Lib.IntTypes.add_mod", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.minint", "typing_Lib.IntVector.vec_add_mod",
"typing_Lib.IntVector.vec_load", "typing_Lib.IntVector.vec_v",
"typing_Lib.Sequence.create", "typing_Lib.Sequence.createi",
"typing_Lib.Sequence.index", "typing_Lib.Sequence.map2",
"typing_Lib.Sequence.upd", "typing_Spec.AES.gf8",
"typing_Spec.Chacha20.size_nonce",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Tm_abs_daf746fa65a87ec0bf08afd7e16e4e61",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"d9f2dcfb598bfeaa27cefa6931459d86"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_core_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.width", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e8e712c693d2a3966788ccb7b46638e3",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"2ba95e82af5ee6b6799aa32fddd3022f"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_core_lemma_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Hacl.Spec.Chacha20.Vec_interpretation_Tm_arrow_a4060274569c7f2a838e81ea9e2cc28d",
"Lib.LoopCombinators_interpretation_Tm_arrow_fcd589b21e6efcf1e5d17b07c282a015",
"Spec.Chacha20_interpretation_Tm_arrow_4b33d7ce430158ea8a765f054f81aab2",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.add_counter",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_core",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.rounds",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.sum_state",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Hacl.Spec.Chacha20.Vec.uint32xN",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred",
"equation_Spec.Chacha20.chacha20_add_counter",
"equation_Spec.Chacha20.chacha20_core",
"equation_Spec.Chacha20.double_round",
"equation_Spec.Chacha20.rounds", "equation_Spec.Chacha20.shuffle",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20.state",
"equation_Spec.Chacha20.sum_state", "equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Spec.Chacha20.state", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e8e712c693d2a3966788ccb7b46638e3",
"token_correspondence_Lib.LoopCombinators.repeat",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Spec.Chacha20.Vec.uint32xN",
"typing_Lib.IntTypes.add_mod", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.mk_int", "typing_Lib.LoopCombinators.repeat",
"typing_Lib.Sequence.createi", "typing_Lib.Sequence.index",
"typing_Lib.Sequence.to_seq", "typing_Lib.Sequence.upd",
"typing_Spec.AES.gf8", "typing_Spec.Chacha20.double_round",
"typing_Spec.Chacha20.size_nonce", "typing_Spec.Chacha20.sum_state",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Tm_abs_daf746fa65a87ec0bf08afd7e16e4e61",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"fe876cbac0250326eb05f0001c301e11"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_init_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_42301dcb830ffc7b7fa39e72eb736b5b",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"1c9ef0065738ae9c717d4a77fd40fad6"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_init_lemma_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Hacl.Spec.Chacha20.Equiv_interpretation_Tm_arrow_e972cbc0ccd0e7fc81d6aae7f35de6ee",
"Hacl.Spec.Chacha20.Vec_interpretation_Tm_arrow_a4060274569c7f2a838e81ea9e2cc28d",
"Lib.IntTypes_interpretation_Tm_arrow_2b601ac3b6dd5023f5acf9aca946a2fa",
"Lib.IntTypes_interpretation_Tm_arrow_b6c7b131dcab59a8eb8f50c70226d5b9",
"Lib.IntTypes_interpretation_Tm_arrow_feb4494e55abb95bc979559ccab03ad0",
"Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.c0",
"equation_Hacl.Spec.Chacha20.Vec.c1",
"equation_Hacl.Spec.Chacha20.Vec.c2",
"equation_Hacl.Spec.Chacha20.Vec.c3",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_constants",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_init",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.nonce",
"equation_Hacl.Spec.Chacha20.Vec.setup1",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Hacl.Spec.Chacha20.Vec.size_nonce",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Hacl.Spec.Chacha20.Vec.uint32xN",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.op_At_Percent_Dot",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.size_t",
"equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "equation_Lib.IntVector.op_Plus_Bar",
"equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t",
"equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.op_At_Bar", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.c0", "equation_Spec.Chacha20.c1",
"equation_Spec.Chacha20.c2", "equation_Spec.Chacha20.c3",
"equation_Spec.Chacha20.chacha20_constants",
"equation_Spec.Chacha20.chacha20_init",
"equation_Spec.Chacha20.setup", "equation_Spec.Chacha20.size_key",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20.state",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.add_mod",
"function_token_typing_Lib.IntTypes.mk_int",
"function_token_typing_Lib.IntTypes.secret",
"function_token_typing_Lib.IntTypes.size_t",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Prims.int",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Spec.Chacha20.state",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing",
"interpretation_Tm_abs_daf746fa65a87ec0bf08afd7e16e4e61",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.add_mod_lemma",
"lemma_Lib.IntTypes.v_injective",
"lemma_Lib.IntVector.vec_add_mod_lemma",
"lemma_Lib.Sequence.create16_lemma", "lemma_Lib.Sequence.eq_elim",
"primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0b72b617030921a422a8020811c2f320",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0ec48bed5965799623c798caf51f1eef",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_19b8de81f52a75b322b8ec818cd2a773",
"refinement_interpretation_Tm_refine_27680283e93f30a8d9ac7d3b22ec31bf",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_41fed56db65f78481d28c1d5f46c599a",
"refinement_interpretation_Tm_refine_42301dcb830ffc7b7fa39e72eb736b5b",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_576183a4f8267f6296f94f4827351efd",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_6140b6af3dde6fccc61c8c2fbb95f76d",
"refinement_interpretation_Tm_refine_62f60abd66f9e5691abea0fb1a86f07d",
"refinement_interpretation_Tm_refine_68ee6d2c8678eb431259a3d4f412550b",
"refinement_interpretation_Tm_refine_6e9be704ead8ad76f9833bf58145f462",
"refinement_interpretation_Tm_refine_7629ad3165e055b3ac6daa2aec6feff9",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_86db23da4ecbc1ed2d2a4c9723698246",
"refinement_interpretation_Tm_refine_87b488a9cf5689c8094f1a153b9356a0",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
"refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_a495e2754242366d1e2dc852effbf6d9",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_abbfe228c7a3d1ae1f16ed243e0e6a67",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_ccbef96ee6e044a9cf0b4353c2d1f06e",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_ddf4c714c12de43e19564d375356f323",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_e4e8563543350376eabac40c2526e67e",
"refinement_interpretation_Tm_refine_e5ff1c4eea1b1f89cbb6a51f7c90d7d6",
"refinement_interpretation_Tm_refine_fb77d4109290540100357b20e0a78486",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"token_correspondence_Hacl.Spec.Chacha20.Vec.vec_load_i",
"token_correspondence_Lib.IntTypes.mk_int",
"token_correspondence_Lib.IntTypes.secret",
"token_correspondence_Lib.IntVector.op_Plus_Bar",
"token_correspondence_Lib.IntVector.vec_add_mod",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Spec.Chacha20.Vec.transpose_state",
"typing_Hacl.Spec.Chacha20.Vec.uint32xN",
"typing_Hacl.Spec.Chacha20.Vec.vec_load_i",
"typing_Lib.ByteSequence.uints_from_bytes_le",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
"typing_Lib.IntTypes.mk_int", "typing_Lib.IntTypes.v",
"typing_Lib.IntVector.vec_v", "typing_Lib.Sequence.create",
"typing_Lib.Sequence.createi", "typing_Lib.Sequence.index",
"typing_Lib.Sequence.map", "typing_Lib.Sequence.map2",
"typing_Lib.Sequence.op_At_Bar", "typing_Lib.Sequence.sub",
"typing_Lib.Sequence.to_seq", "typing_Lib.Sequence.upd",
"typing_Lib.Sequence.update_sub", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred", "typing_Spec.Chacha20.chacha20_constants",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_Tm_abs_daf746fa65a87ec0bf08afd7e16e4e61",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"8b06f74835f13ae2ffe33a41b93dcfc2"
],
[
"Hacl.Spec.Chacha20.Equiv.lemma_i_div_w4",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.pos",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "int_inversion",
"primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"03773a4389332b87cec59bf982ab8849"
],
[
"Hacl.Spec.Chacha20.Equiv.lemma_i_div_w4",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"927ac7bd69bd6a6e9e74624d10dda50d"
],
[
"Hacl.Spec.Chacha20.Equiv.lemma_i_div_blocksize",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"2b9c33325c39706847cd7ecf4ce889a1"
],
[
"Hacl.Spec.Chacha20.Equiv.lemma_i_div_blocksize",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"f07eb5d8da494a726ec94d2de2175cf0"
],
[
"Hacl.Spec.Chacha20.Equiv.xor_block_vec_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.blocks",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.xor_block",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"int_inversion", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7acf795d50ec256996534a97e12bfa61",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Hacl.Spec.Chacha20.Vec.xor_block",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"99d12dd5b5dffabdda78390a54a81efb"
],
[
"Hacl.Spec.Chacha20.Equiv.xor_block_vec_lemma_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Hacl.Spec.Chacha20.Vec_interpretation_Tm_arrow_cfb6e7971a2156f7d20e16568d5fc8f6",
"Lib.IntTypes_interpretation_Tm_arrow_f4a9562bad893d799188b75efefcbe4b",
"Lib.IntVector_interpretation_Tm_arrow_760746993345c1327f70c87a340d60e0",
"Lib.Sequence_interpretation_Tm_arrow_31983ce7bb3fa3288ec94b088df0f02a",
"Lib.Sequence_interpretation_Tm_arrow_d3b9c37343cabe37d3e11c0a1cafa7da",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.blocks",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.uint32xN",
"equation_Hacl.Spec.Chacha20.Vec.xor_block",
"equation_Hacl.Spec.Chacha20.Vec.xor_block_f",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.uint32",
"equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.op_Hat_Bar",
"equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.vec_v_t",
"equation_Lib.IntVector.width", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Chacha20.size_key",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Hacl.Spec.Chacha20.Vec.xor_block_f",
"function_token_typing_Lib.IntTypes.logxor",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Lib.IntVector.vec_xor",
"function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.Seq.Properties.slice_slice",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
"lemma_Lib.IntVector.vec_from_bytes_le_lemma",
"lemma_Lib.IntVector.vec_to_bytes_le_lemma",
"lemma_Lib.IntVector.vec_xor_lemma", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_1b43ad09734150a98a09eb8af4f2257c",
"refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_634e327f7229300b8bca6528f0f839cd",
"refinement_interpretation_Tm_refine_662415da0484477c4b367b5d92bc2a31",
"refinement_interpretation_Tm_refine_6b212cc4409cac236104605b933db44d",
"refinement_interpretation_Tm_refine_6fa9dbb32250e2c5b3bbd565a9949df9",
"refinement_interpretation_Tm_refine_7acf795d50ec256996534a97e12bfa61",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8cff11614032f73ae1a9478d68aab0b2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_9341db820105e61c7250a290c9437d90",
"refinement_interpretation_Tm_refine_98791b04164e0ec70d2ca29d010fdf16",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e78eb6947886b7563bc92d925f37e010",
"refinement_interpretation_Tm_refine_e8ff591ad259d5a2e8105899c7d165d3",
"refinement_interpretation_Tm_refine_f4ec0a04344e7130939ebe4f31f6bd8f",
"refinement_interpretation_Tm_refine_f4f040c0afc8e02646bd007fb369c803",
"refinement_interpretation_Tm_refine_f589786c97b4c07119c99688fe202777",
"refinement_interpretation_Tm_refine_ff0d8d69da9f11332eb9ad2b09219f48",
"token_correspondence_Lib.IntVector.op_Hat_Bar",
"token_correspondence_Lib.IntVector.vec_xor",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_Hacl.Spec.Chacha20.Vec.uint32xN",
"typing_Hacl.Spec.Chacha20.Vec.xor_block",
"typing_Lib.IntTypes.bits", "typing_Lib.IntVector.vec_from_bytes_le",
"typing_Lib.Sequence.index", "typing_Lib.Sequence.map2",
"typing_Lib.Sequence.map_blocks_multi", "typing_Lib.Sequence.to_seq",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"2450f80213641d31dd9ef506f0ea8086"
],
[
"Hacl.Spec.Chacha20.Equiv.xor_block_scalar_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.block", "equation_Spec.Chacha20.size_block",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"int_inversion", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_91daafe4a50a104515c66cb31e4a8eaa",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.Chacha20.xor_block",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"4999bdf40b6653d63a69cfa9716eeccd"
],
[
"Hacl.Spec.Chacha20.Equiv.xor_block_scalar_lemma_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Chacha20.block",
"equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.xor_block",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_14fe017a75745924dcc47b11c3a84378",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_6f7719d2e9422e645682674727002c0b",
"refinement_interpretation_Tm_refine_7acf795d50ec256996534a97e12bfa61",
"refinement_interpretation_Tm_refine_91daafe4a50a104515c66cb31e4a8eaa",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_ed1d8a8110680776917967702c15f2f5",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Lib.Sequence.index", "typing_Spec.AES.gf8",
"typing_Spec.Chacha20.xor_block",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"bc035e5ec9203f491e7201b55794b6d5"
],
[
"Hacl.Spec.Chacha20.Equiv.transpose_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.transpose",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Hacl.Spec.Chacha20.Vec.uint32xN",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.vec_v_t",
"equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Prims.nonzero",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Division",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Hacl.Spec.Chacha20.Vec.transpose",
"typing_Hacl.Spec.Chacha20.Vec.transpose_state",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"b5638ec50b846c3682c7434be327783f"
],
[
"Hacl.Spec.Chacha20.Equiv.transpose_lemma_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.transpose",
"equation_Hacl.Spec.Chacha20.Vec.transpose1",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Hacl.Spec.Chacha20.Vec.uint32xN",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.uint32", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_2f9c3b898a76110b738f46ef969785d6",
"refinement_interpretation_Tm_refine_4350bf9489acca1d3f689adadf32137a",
"refinement_interpretation_Tm_refine_4ae19fb70eec46886fc5fc1fc4cd0e44",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e73f6e7bcf5930b2927b2a5854af7cb8",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Spec.Chacha20.Vec.transpose",
"typing_Hacl.Spec.Chacha20.Vec.transpose_state",
"typing_Hacl.Spec.Chacha20.Vec.uint32xN", "typing_Lib.IntTypes.bits",
"typing_Lib.Sequence.index", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"081a622a42ecb000fc905fb7cda3c47b"
],
[
"Hacl.Spec.Chacha20.Equiv.xor_block_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.blocks",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Chacha20.block",
"equation_Spec.Chacha20.size_block", "equation_Spec.Chacha20.state",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"int_inversion", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7f0e1f6727e61a9019c13155aed4e875",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_91daafe4a50a104515c66cb31e4a8eaa",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e73f6e7bcf5930b2927b2a5854af7cb8",
"typing_Hacl.Spec.Chacha20.Vec.transpose",
"typing_Hacl.Spec.Chacha20.Vec.transpose_state",
"typing_Hacl.Spec.Chacha20.Vec.xor_block",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.Chacha20.xor_block",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"ad7c990d42569144cee5ab34e179e854"
],
[
"Hacl.Spec.Chacha20.Equiv.xor_block_lemma_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.blocks",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.transpose",
"equation_Hacl.Spec.Chacha20.Vec.transpose1",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Hacl.Spec.Chacha20.Vec.uint32xN",
"equation_Hacl.Spec.Chacha20.Vec.xor_block",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.vec_v_t", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Chacha20.block",
"equation_Spec.Chacha20.size_block", "equation_Spec.Chacha20.state",
"equation_Spec.Chacha20.xor_block",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.Seq.Properties.slice_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_3f3b2c65a66eafa835007433af839225",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_6b212cc4409cac236104605b933db44d",
"refinement_interpretation_Tm_refine_7acf795d50ec256996534a97e12bfa61",
"refinement_interpretation_Tm_refine_7f0e1f6727e61a9019c13155aed4e875",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_81927eebe349dd77b039bd1f295ee7f4",
"refinement_interpretation_Tm_refine_8ca4e0a204eada0d8e809851bbeb5cd8",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_91daafe4a50a104515c66cb31e4a8eaa",
"refinement_interpretation_Tm_refine_c3d27b3f58e1066d9ca19ecf293ad33f",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d5690d50d7b913cf86ab71d66836f2cb",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e73f6e7bcf5930b2927b2a5854af7cb8",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Spec.Chacha20.Vec.transpose",
"typing_Hacl.Spec.Chacha20.Vec.transpose_state",
"typing_Hacl.Spec.Chacha20.Vec.xor_block",
"typing_Lib.IntTypes.bits", "typing_Lib.Sequence.index",
"typing_Lib.Sequence.to_seq", "typing_Spec.AES.gf8",
"typing_Spec.Chacha20.xor_block",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"43f83a2254e9de32597a7082bd358487"
],
[
"Hacl.Spec.Chacha20.Equiv.encrypt_block_scalar_lemma_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5735b1ab474347e6de95ca72d148f746",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"9dec3f4cab42fe3cb01653bf4f55b6e2"
],
[
"Hacl.Spec.Chacha20.Equiv.encrypt_block_scalar_lemma_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.nonce",
"equation_Hacl.Spec.Chacha20.Vec.setup1",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Hacl.Spec.Chacha20.Vec.size_nonce",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.uint32", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.width", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Chacha20.block",
"equation_Spec.Chacha20.chacha20_core",
"equation_Spec.Chacha20.chacha20_encrypt_block",
"equation_Spec.Chacha20.chacha20_init",
"equation_Spec.Chacha20.counter", "equation_Spec.Chacha20.key",
"equation_Spec.Chacha20.nonce", "equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20.state",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Spec.Chacha20.state", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5735b1ab474347e6de95ca72d148f746",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Spec.Chacha20.Vec.chacha20_init",
"typing_Hacl.Spec.Chacha20.Vec.setup1",
"typing_Hacl.Spec.Chacha20.Vec.transpose_state",
"typing_Lib.Sequence.index", "typing_Spec.AES.gf8",
"typing_Spec.Chacha20.chacha20_core",
"typing_Spec.Chacha20.chacha20_encrypt_block",
"typing_Spec.Chacha20.chacha20_init",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"101446fed5d0a4f8ad6b3140b5cd80bd"
],
[
"Hacl.Spec.Chacha20.Equiv.encrypt_block_lemma_st0_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.blocks",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.block", "equation_Spec.Chacha20.size_block",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"int_inversion", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e8e712c693d2a3966788ccb7b46638e3",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"5848e7aa0d6c05f3ce50825edcf8e645"
],
[
"Hacl.Spec.Chacha20.Equiv.encrypt_block_lemma_st0_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Spec.Chacha20_interpretation_Tm_arrow_4b33d7ce430158ea8a765f054f81aab2",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.blocks",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_encrypt_block",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Hacl.Spec.Chacha20.Vec.uint32xN",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint32",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.Lemmas.get_block_s",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.chacha20_add_counter",
"equation_Spec.Chacha20.chacha20_core",
"equation_Spec.Chacha20.chacha20_encrypt_block",
"equation_Spec.Chacha20.rounds", "equation_Spec.Chacha20.shuffle",
"equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20.state",
"equation_Spec.Chacha20.sum_state",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Spec.Chacha20.state", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
"refinement_interpretation_Tm_refine_9d3fd79fd314167f1a9c213a188da3ec",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e8e712c693d2a3966788ccb7b46638e3",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Spec.Chacha20.Vec.chacha20_core",
"typing_Hacl.Spec.Chacha20.Vec.transpose_state",
"typing_Hacl.Spec.Chacha20.Vec.uint32xN",
"typing_Lib.IntTypes.add_mod", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.mk_int", "typing_Lib.Sequence.index",
"typing_Lib.Sequence.sub", "typing_Lib.Sequence.to_seq",
"typing_Lib.Sequence.upd", "typing_Spec.AES.gf8",
"typing_Spec.Chacha20.rounds", "typing_Spec.Chacha20.size_block",
"typing_Spec.Chacha20.size_nonce", "typing_Spec.Chacha20.sum_state",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"5c794b6dfc9fa1c1ec60eef30f659a23"
],
[
"Hacl.Spec.Chacha20.Equiv.encrypt_block_lemma_bs_i",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.blocks",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.block", "equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e8e712c693d2a3966788ccb7b46638e3",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"d5cbb707700d8d378d45974c67d82f44"
],
[
"Hacl.Spec.Chacha20.Equiv.encrypt_block_lemma_bs_i",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.blocks",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.setup1",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Hacl.Spec.Chacha20.Vec.transpose_state",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_Spec.AES.elem", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Chacha20.block",
"equation_Spec.Chacha20.chacha20_init",
"equation_Spec.Chacha20.counter",
"equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key", "equation_Spec.Chacha20.state",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Spec.Chacha20.state", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_42301dcb830ffc7b7fa39e72eb736b5b",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e8e712c693d2a3966788ccb7b46638e3",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Spec.Chacha20.Vec.chacha20_init",
"typing_Hacl.Spec.Chacha20.Vec.setup1",
"typing_Hacl.Spec.Chacha20.Vec.transpose_state",
"typing_Lib.Sequence.index", "typing_Spec.AES.gf8",
"typing_Spec.Chacha20.chacha20_encrypt_block",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"e9b050bb004d43c3ab4f372cdb6ed913"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_map_blocks_multi_vec_equiv_pre_k",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_2f273971278fdcc596c11b6c03de04f5",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"ac808a48817b5fa16ab5b6cf263373a8"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_map_blocks_multi_vec_equiv_pre_k",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"fe7a3eef151a626838376dd9a371d9e2"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_map_blocks_multi_vec_equiv_pre_k",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8", "eq2-interp",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.blocks",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_encrypt_block",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_init",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.nonce",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Hacl.Spec.Chacha20.Vec.size_nonce",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.Lemmas.get_block_s",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Lib.Vec.Lemmas.map_blocks_multi_vec_equiv_pre_k",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.block", "equation_Spec.Chacha20.counter",
"equation_Spec.Chacha20.key", "equation_Spec.Chacha20.nonce",
"equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key",
"equation_Spec.Chacha20.size_nonce",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Hacl.Spec.Chacha20.Vec.chacha20_encrypt_block",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Spec.Chacha20.chacha20_encrypt_block",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_2f273971278fdcc596c11b6c03de04f5",
"refinement_interpretation_Tm_refine_3833667c59aecdf581ef615fb6194b08",
"refinement_interpretation_Tm_refine_42301dcb830ffc7b7fa39e72eb736b5b",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_87f4f4d27aa724cb70fe8fdc53664aca",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c37230a0b45bfa733513e4ce89ef34d6",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e8e712c693d2a3966788ccb7b46638e3",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_Hacl.Spec.Chacha20.Vec.chacha20_core",
"typing_Hacl.Spec.Chacha20.Vec.chacha20_encrypt_block",
"typing_Hacl.Spec.Chacha20.Vec.chacha20_init",
"typing_Hacl.Spec.Chacha20.Vec.transpose",
"typing_Hacl.Spec.Chacha20.Vec.xor_block",
"typing_Lib.Sequence.Lemmas.get_block_s",
"typing_Lib.Sequence.index", "typing_Spec.AES.gf8",
"typing_Spec.Chacha20.chacha20_encrypt_block",
"typing_Spec.Chacha20.chacha20_init",
"typing_Spec.Chacha20.size_block",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"97e7424aeb2cb47638ecf68e13d6e0a3"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_is_append",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_2057733be200c152a41705bd9fd424a6",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"60a36f99ad0ac2c0c331df9e0149314f"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_is_append",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f"
],
0,
"41aa0f96607ef4ab391cc355e248102c"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_is_append",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_FStar.Pervasives.Native.fst",
"equation_FStar.Pervasives.Native.snd",
"equation_FStar.Seq.Properties.split",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice", "lemma_Lib.Sequence.eq_elim",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_17631fa6304dcc08d028bd475a6dd078",
"refinement_interpretation_Tm_refine_2057733be200c152a41705bd9fd424a6",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_3f7df05abb8d4c7a2f53bf61c574ac9b",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7ec114c6d7ebf77ef9def228380f63e8",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"typing_FStar.Pervasives.Native.__proj__Mktuple2__item___2",
"typing_FStar.Pervasives.Native.fst",
"typing_FStar.Pervasives.Native.snd", "typing_FStar.Seq.Base.append",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Properties.split",
"typing_Lib.IntTypes.minint", "typing_Lib.Sequence.index",
"typing_Lib.Sequence.seq", "typing_Lib.Sequence.sub",
"typing_Lib.Sequence.to_seq", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"840f1170110b57c985181b70a3c0421c"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_block_lemma_k",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_4138b1b2dda6b375d86a9918f866afd6",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_4756eacc277e50995a2680263b3d05e9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c37230a0b45bfa733513e4ce89ef34d6",
"refinement_interpretation_Tm_refine_ccb9fc6d9b1f5ba53aabf522a7465b42",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"7bd61ec9e32b9c39f6bd83184f4404ba"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_block_lemma_k",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.pos",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"7478610fb5cd6a8168c4c43eecafed00"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_block_lemma_k",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.Lemmas.get_block_s",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_4138b1b2dda6b375d86a9918f866afd6",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_4756eacc277e50995a2680263b3d05e9",
"refinement_interpretation_Tm_refine_4bb4e9fe71e4be79ded02ec9e9944a2c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_67f67a461ee73a36733875e052e6beee",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c37230a0b45bfa733513e4ce89ef34d6",
"refinement_interpretation_Tm_refine_ccb9fc6d9b1f5ba53aabf522a7465b42",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.minint",
"typing_Lib.Sequence.sub", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"3af2e5d2b5adc5775038d92586828d8f"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_block_lemma",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_4138b1b2dda6b375d86a9918f866afd6",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_4756eacc277e50995a2680263b3d05e9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_c37230a0b45bfa733513e4ce89ef34d6",
"refinement_interpretation_Tm_refine_ccb9fc6d9b1f5ba53aabf522a7465b42",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"5c1bf3b9986dd9540dabd3ff209aac2a"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_block_lemma",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.pos",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"b9664d7e33f17ccc14cc73fa57e117d4"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_block_lemma",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.Lemmas.get_block_s",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "lemma_FStar.UInt.pow2_values",
"lemma_Lib.Sequence.eq_elim", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_4138b1b2dda6b375d86a9918f866afd6",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_4756eacc277e50995a2680263b3d05e9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_c37230a0b45bfa733513e4ce89ef34d6",
"refinement_interpretation_Tm_refine_ccb9fc6d9b1f5ba53aabf522a7465b42",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Lib.Sequence.index", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"8eae8c61e438d5ac2a7d827f72afbca6"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_last_lemma_plain_k",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_25bbcf70217dbbb47215f7c1afb6c333",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"refinement_interpretation_Tm_refine_eeb59caff9a959bab0eef3a399bf14b7",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"752a89152986bd4ce785a9b51a29ac9e"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_last_lemma_plain_k",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.pos",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"d0318c5b0c249fa9069bded60162002a"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_last_lemma_plain_k",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.Lemmas.get_last_s",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_1afec1f5fbaba2ad1fa6305748f635c2",
"refinement_interpretation_Tm_refine_25bbcf70217dbbb47215f7c1afb6c333",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_41ffb19cbfecb4535126fa045b2153d4",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ab8f2ad159c18e6509305326b2e3a627",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"refinement_interpretation_Tm_refine_eeb59caff9a959bab0eef3a399bf14b7",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.minint", "typing_Lib.Sequence.sub",
"typing_Lib.Sequence.to_seq", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"be0b72d76ef3e09c2258e3f4dfef3495"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_last_lemma_plain_v_k",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThan", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_4138b1b2dda6b375d86a9918f866afd6",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_4756eacc277e50995a2680263b3d05e9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_ccb9fc6d9b1f5ba53aabf522a7465b42",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"refinement_interpretation_Tm_refine_eeb59caff9a959bab0eef3a399bf14b7",
"typing_Lib.IntTypes.bits", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"25af36382f0e6df7ff8d7126cc51339c"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_last_lemma_plain_v_k",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.pos",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"25e3d57f5184058386ced0e2816d4610"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_last_lemma_plain_v_k",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.Lemmas.get_block_s",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_4138b1b2dda6b375d86a9918f866afd6",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_4756eacc277e50995a2680263b3d05e9",
"refinement_interpretation_Tm_refine_4bb4e9fe71e4be79ded02ec9e9944a2c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_67f67a461ee73a36733875e052e6beee",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_ccb9fc6d9b1f5ba53aabf522a7465b42",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"refinement_interpretation_Tm_refine_eeb59caff9a959bab0eef3a399bf14b7",
"refinement_interpretation_Tm_refine_f68d603fb50670b846a70537ca08277e",
"typing_FStar.Seq.Base.create", "typing_Lib.IntTypes.bits",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"d4a9a4ec51d9a87b91f310cd5ce52cc6"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_last_lemma",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_4138b1b2dda6b375d86a9918f866afd6",
"refinement_interpretation_Tm_refine_41ffb19cbfecb4535126fa045b2153d4",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_4756eacc277e50995a2680263b3d05e9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_ccb9fc6d9b1f5ba53aabf522a7465b42",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"refinement_interpretation_Tm_refine_eeb59caff9a959bab0eef3a399bf14b7",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"89fe7fd022cb14d64eeed082766951f8"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_last_lemma",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Prims.pos",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.GaloisField.gf",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"66b06471593558fdfa9b2ca3f841cf81"
],
[
"Hacl.Spec.Chacha20.Equiv.update_sub_get_last_lemma",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "lemma_Lib.Sequence.eq_elim",
"primitive_Prims.op_Addition", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_25bbcf70217dbbb47215f7c1afb6c333",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_4138b1b2dda6b375d86a9918f866afd6",
"refinement_interpretation_Tm_refine_41ffb19cbfecb4535126fa045b2153d4",
"refinement_interpretation_Tm_refine_44540322a5aeeac77ad2eb12638c2b4f",
"refinement_interpretation_Tm_refine_4756eacc277e50995a2680263b3d05e9",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7d90ff2f12815f81a295a11e6f29235e",
"refinement_interpretation_Tm_refine_a8ac4e0098b50328dadbc05b3b27c877",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_ccb9fc6d9b1f5ba53aabf522a7465b42",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e37a8a81b6e72b6dae52414929365d29",
"refinement_interpretation_Tm_refine_eeb59caff9a959bab0eef3a399bf14b7",
"refinement_interpretation_Tm_refine_f37327594b97f54132ce6bcb98ee4847",
"refinement_interpretation_Tm_refine_fc1f69e4229a94f85b0de30f1747a8d3",
"typing_FStar.Seq.Base.length", "typing_Lib.Sequence.index",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"82e405f628d143eb45ab2e76e52fad60"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_map_blocks_vec_equiv_pre_k0",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_3b5af034ac9e48a9e28d8570d73de634",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_75da5346210d72f30a5c42fa3898ed1f",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"5b93553c5619df672d44eb8d132e8ade"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_map_blocks_vec_equiv_pre_k0",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"196da88287377ed166af8f15def237bf"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_map_blocks_vec_equiv_pre_k0",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8", "eq2-interp",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.blocks",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_encrypt_block",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_encrypt_last",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_init",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.uint32xN",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.width", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Lib.Sequence.to_seq",
"equation_Lib.Vec.Lemmas.map_blocks_vec_equiv_pre_k",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.block", "equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Hacl.Spec.Chacha20.Vec.chacha20_encrypt_last",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Spec.Chacha20.chacha20_encrypt_block",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_3b5af034ac9e48a9e28d8570d73de634",
"refinement_interpretation_Tm_refine_42301dcb830ffc7b7fa39e72eb736b5b",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_75da5346210d72f30a5c42fa3898ed1f",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_870808e8db8a4aca51f3e4883aa8a003",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_91dd079dd20040117b26e33ccecdc4cd",
"refinement_interpretation_Tm_refine_955474df0c6eb86cf15485e506bbaa3b",
"refinement_interpretation_Tm_refine_c105789aebaa605cb35b0e347d2554de",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e8e712c693d2a3966788ccb7b46638e3",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Spec.Chacha20.Vec.chacha20_core",
"typing_Hacl.Spec.Chacha20.Vec.chacha20_init",
"typing_Hacl.Spec.Chacha20.Vec.transpose",
"typing_Hacl.Spec.Chacha20.Vec.xor_block",
"typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.v",
"typing_Lib.Sequence.index", "typing_Lib.Sequence.sub",
"typing_Spec.AES.gf8", "typing_Spec.AES.irred",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"7d8694fcb6e9ea4ab381cb531fee0f24"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_map_blocks_vec_equiv_pre_k1",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_3b5af034ac9e48a9e28d8570d73de634",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_64be6dbc9729c30e6127ca432f44d79e",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"3f4d0f70735b77c8a945ec9507e4d853"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_map_blocks_vec_equiv_pre_k1",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"143a74d737b45055ab183dc7ae365231"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_map_blocks_vec_equiv_pre_k1",
3,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"FStar.FunctionalExtensionality_interpretation_Tm_arrow_6980332764c4493a7b0df5c02f7aefbe",
"Hacl.Spec.Chacha20.Vec_interpretation_Tm_arrow_7b152b521a36c1dc1fcd81c092909f6d",
"Lib.IntVector_interpretation_Tm_arrow_760746993345c1327f70c87a340d60e0",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "eq2-interp",
"equality_tok_Lib.IntTypes.SEC@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.blocks",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_encrypt_block",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_encrypt_last",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_init",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.nonce",
"equation_Hacl.Spec.Chacha20.Vec.setup1",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Hacl.Spec.Chacha20.Vec.size_nonce",
"equation_Hacl.Spec.Chacha20.Vec.state",
"equation_Hacl.Spec.Chacha20.Vec.uint32xN",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.uint32",
"equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.op_Plus_Bar",
"equation_Lib.IntVector.v_inttype", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.Lemmas.get_block_s",
"equation_Lib.Sequence.Lemmas.get_last_s",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Lib.Sequence.to_seq",
"equation_Lib.Vec.Lemmas.map_blocks_vec_equiv_pre_k",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.block",
"equation_Spec.Chacha20.chacha20_encrypt_last",
"equation_Spec.Chacha20.chacha20_init",
"equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key",
"equation_Spec.Chacha20.size_nonce", "equation_Spec.Chacha20.state",
"equation_Spec.GaloisField.felem", "equation_Spec.GaloisField.gf",
"function_token_typing_Hacl.Spec.Chacha20.Vec.chacha20_encrypt_last",
"function_token_typing_Hacl.Spec.Chacha20.Vec.vec_load_i",
"function_token_typing_Lib.IntTypes.uint32",
"function_token_typing_Lib.IntVector.vec_add_mod",
"function_token_typing_Spec.AES.elem",
"function_token_typing_Spec.Chacha20.chacha20_encrypt_last",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_0f7f5bcf08e8db1ef86bd2d55b0d74fb",
"refinement_interpretation_Tm_refine_11888fecf812f197898447624c24e106",
"refinement_interpretation_Tm_refine_246dc5aa3b4786f3f5c07ad899d5a37c",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_3b5af034ac9e48a9e28d8570d73de634",
"refinement_interpretation_Tm_refine_40d37ebab7c1b683bff04f4efbb0b134",
"refinement_interpretation_Tm_refine_42301dcb830ffc7b7fa39e72eb736b5b",
"refinement_interpretation_Tm_refine_48486e77aa5457d9a27027fef170c244",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5d7fc65a01f63f2bc577298c179f855a",
"refinement_interpretation_Tm_refine_60773d8a2ad53f7660dcd264d95a9b44",
"refinement_interpretation_Tm_refine_64be6dbc9729c30e6127ca432f44d79e",
"refinement_interpretation_Tm_refine_6e9be704ead8ad76f9833bf58145f462",
"refinement_interpretation_Tm_refine_716f5ae59c0acd5cc9bdc787abede05e",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_870808e8db8a4aca51f3e4883aa8a003",
"refinement_interpretation_Tm_refine_87f4f4d27aa724cb70fe8fdc53664aca",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_90cd95ca0632502fc3300a400d8c5438",
"refinement_interpretation_Tm_refine_91dd079dd20040117b26e33ccecdc4cd",
"refinement_interpretation_Tm_refine_955474df0c6eb86cf15485e506bbaa3b",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_a17ef47f0ed9863dfad27c4c128f46fa",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d88f260aa55cbfa41135f023e41e305b",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"refinement_interpretation_Tm_refine_e8e712c693d2a3966788ccb7b46638e3",
"token_correspondence_Hacl.Spec.Chacha20.Vec.vec_load_i",
"token_correspondence_Lib.IntVector.op_Plus_Bar",
"token_correspondence_Lib.IntVector.vec_add_mod",
"typing_FStar.Seq.Base.length",
"typing_Hacl.Spec.Chacha20.Vec.chacha20_core",
"typing_Hacl.Spec.Chacha20.Vec.chacha20_encrypt_block",
"typing_Hacl.Spec.Chacha20.Vec.setup1",
"typing_Hacl.Spec.Chacha20.Vec.transpose",
"typing_Hacl.Spec.Chacha20.Vec.uint32xN",
"typing_Hacl.Spec.Chacha20.Vec.xor_block",
"typing_Lib.IntTypes.minint", "typing_Lib.IntTypes.v",
"typing_Lib.IntVector.vec_counter", "typing_Lib.Sequence.index",
"typing_Lib.Sequence.map", "typing_Lib.Sequence.sub",
"typing_Lib.Sequence.upd", "typing_Spec.AES.gf8",
"typing_Spec.AES.irred",
"typing_Spec.Chacha20.chacha20_encrypt_block",
"typing_Spec.GaloisField.__proj__GF__item__t",
"typing_tok_Lib.IntTypes.SEC@tok", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"b9a678587380d0d4a19cb51557d3f7e1"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_map_blocks_vec_equiv_pre_k",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntVector.width",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_00db4a5c18abaae9a3787937e850b5f3",
"refinement_interpretation_Tm_refine_3b5af034ac9e48a9e28d8570d73de634",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"a4d51fa874b38e7297c911d0eb0ca901"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_map_blocks_vec_equiv_pre_k",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Spec.AES.elem",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"42d658f1706de2380e26b0db2eb117f0"
],
[
"Hacl.Spec.Chacha20.Equiv.chacha20_map_blocks_vec_equiv_pre_k",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.GaloisField.gf",
"int_inversion", "primitive_Prims.op_LessThan",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"75b622f5e76f97e1bd999f64a1928114"
],
[
"Hacl.Spec.Chacha20.Equiv.lemma_chacha20_vec_equiv",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equality_tok_Lib.IntTypes.U8@tok",
"equation_Lib.IntTypes.uint8", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Spec.AES.gf8",
"equation_Spec.AES.irred", "equation_Spec.Chacha20.size_block",
"equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.uint8",
"primitive_Prims.op_Division", "proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c5579466c1fcb6457bba4b009a86e2ac",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.Sequence.length", "typing_Spec.AES.gf8",
"typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"7153b08c44b8ac94827833dbec1aa21d"
],
[
"Hacl.Spec.Chacha20.Equiv.lemma_chacha20_vec_equiv",
2,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok",
"equation_Hacl.Spec.Chacha20.Equiv.blocksize",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_encrypt_bytes",
"equation_Hacl.Spec.Chacha20.Vec.chacha20_update",
"equation_Hacl.Spec.Chacha20.Vec.counter",
"equation_Hacl.Spec.Chacha20.Vec.key",
"equation_Hacl.Spec.Chacha20.Vec.lanes",
"equation_Hacl.Spec.Chacha20.Vec.size_block",
"equation_Hacl.Spec.Chacha20.Vec.size_key",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.uint8", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntVector.width", "equation_Lib.Sequence.length",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.seq",
"equation_Prims.nat", "equation_Spec.AES.elem",
"equation_Spec.AES.gf8", "equation_Spec.AES.irred",
"equation_Spec.Chacha20.chacha20_encrypt_bytes",
"equation_Spec.Chacha20.chacha20_update",
"equation_Spec.Chacha20.size_block",
"equation_Spec.Chacha20.size_key", "equation_Spec.GaloisField.felem",
"equation_Spec.GaloisField.gf",
"function_token_typing_Lib.IntTypes.uint8",
"function_token_typing_Spec.AES.elem", "int_inversion",
"lemma_FStar.Seq.Base.lemma_eq_refl", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"proj_equation_Spec.GaloisField.GF_t",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_Spec.GaloisField.GF_t",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_3a89882cedd4be6e9c17c4c8eceb90fb",
"refinement_interpretation_Tm_refine_42301dcb830ffc7b7fa39e72eb736b5b",
"refinement_interpretation_Tm_refine_50745f4abd3b1f3a36148d2dfd3f8dde",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6ea782d20d3a5b4d53411900c5408b2a",
"refinement_interpretation_Tm_refine_8f5bacb69a016785e5356e99e7760edf",
"refinement_interpretation_Tm_refine_c5579466c1fcb6457bba4b009a86e2ac",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Lib.Sequence.length",
"typing_Spec.AES.gf8", "typing_Spec.GaloisField.__proj__GF__item__t"
],
0,
"743d8e9b1bc75f2937954dbfb41888b9"
]
]
]