Revision b06f899cc120e08d2b3ecce79abc2c014fb6080c authored by Santiago Zanella-Beguelin on 29 November 2019, 13:25:44 UTC, committed by GitHub on 29 November 2019, 13:25:44 UTC
Only add libintvector.h include when necessary for mozilla dist
Lib.ByteSequence.fsti.hints
[
"�ͣ-������+��6",
[
[
"Lib.ByteSequence.bytes_l",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"projection_inverse_BoxBool_proj_0"
],
0,
"64592def8b107f62d906a1218e1eb195"
],
[
"Lib.ByteSequence.lbytes_l",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"projection_inverse_BoxBool_proj_0"
],
0,
"bec6147caa9c53ba6e9559457fd406a5"
],
[
"Lib.ByteSequence.seq_eq_mask",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.SEC@tok", "equation_Lib.IntTypes.int_t",
"equation_Lib.Sequence.lseq", "equation_Lib.Sequence.to_seq",
"equation_Prims.nat", "int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_2ef8f43a290174b3a89dd42b03d028a5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"3f780704beb2d5aeffb4f0d7434484fb"
],
[
"Lib.ByteSequence.lbytes_empty",
1,
2,
1,
[
"@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.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos", "int_typing",
"lemma_Lib.IntTypes.pow2_3", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"b5c2b826602d11e0882c56c47168a36e"
],
[
"Lib.ByteSequence.nat_from_intseq_be",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
"equation_Lib.Sequence.length", "equation_Prims.nat",
"fuel_guarded_inversion_Lib.IntTypes.inttype",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.int_t", "typing_Lib.Sequence.length"
],
0,
"930f8a90d63c40e17fe589cfe6152dbe"
],
[
"Lib.ByteSequence.nat_from_intseq_le",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
"equation_Lib.Sequence.length", "equation_Prims.nat",
"fuel_guarded_inversion_Lib.IntTypes.inttype",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.int_t", "typing_Lib.Sequence.length"
],
0,
"dce4428f0551a638bf0d5f7098f6ec48"
],
[
"Lib.ByteSequence.nat_from_bytes_be",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"85afe3e9725cdd0dd5853b159fbcb634"
],
[
"Lib.ByteSequence.nat_from_bytes_le",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"f0fdf709cd0e9c1327487114d9c054a2"
],
[
"Lib.ByteSequence.nat_to_intseq_be",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
"equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
"int_inversion", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"d33fb7c37386bbe320c67dd68911fcaf"
],
[
"Lib.ByteSequence.nat_to_intseq_le",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
"equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
"int_inversion", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"1f3bbbc52cc65a33cbfd8c29b10eb346"
],
[
"Lib.ByteSequence.nat_to_bytes_be",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"df6f72b726d4dbde392576d2afad9528"
],
[
"Lib.ByteSequence.nat_to_bytes_le",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"21c7c2d20c8190570df842e49512bf7c"
],
[
"Lib.ByteSequence.uint_to_bytes_le",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Lib.IntTypes.inttype", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"d9d43a6740723bcee4dc5689231572bd"
],
[
"Lib.ByteSequence.index_uint_to_bytes_le",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "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.to_seq",
"equation_Prims.nat", "equation_Prims.nonzero", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Lib.IntTypes.inttype", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0766302b68bb44ab7aff8c4d8be0b46f",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6995b0f4000fa0c5e6436e1dd45f3269",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.ByteSequence.uint_to_bytes_le",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned",
"typing_Prims.pow2", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"5d1032876be2107c26c445f231680741"
],
[
"Lib.ByteSequence.uint_to_bytes_be",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Lib.IntTypes.inttype", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"2d912f6a5443d76938784ee00e40b6bd"
],
[
"Lib.ByteSequence.uint_from_bytes_le",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Lib.IntTypes.inttype", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"7042466808b3936e59c5607142f0f863"
],
[
"Lib.ByteSequence.uint_from_bytes_be",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Lib.IntTypes.inttype", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"8523b583e6e6f5c80bd2fdb830411f56"
],
[
"Lib.ByteSequence.uints_to_bytes_le",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"bb6fb7e563c41d2abf10a0ad7ca002f8"
],
[
"Lib.ByteSequence.index_uints_to_bytes_le",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Lib.IntTypes.inttype", "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",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_2f9afc482a008cf7515f2d7246def051",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.ByteSequence.uints_to_bytes_le",
"typing_Lib.IntTypes.numbytes", "typing_Lib.IntTypes.unsigned"
],
0,
"9f127ce595f6010803e99f9b3c09ed3b"
],
[
"Lib.ByteSequence.uints_to_bytes_be",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"6185fd9a741cf1436a287c87b77c7ec4"
],
[
"Lib.ByteSequence.index_uints_to_bytes_be",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.to_seq", "equation_Prims.nat",
"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",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_2f9afc482a008cf7515f2d7246def051",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.ByteSequence.uints_to_bytes_be",
"typing_Lib.IntTypes.numbytes", "typing_Lib.IntTypes.unsigned"
],
0,
"243f735c5b40890bff4a07ec1e216697"
],
[
"Lib.ByteSequence.uints_from_bytes_le",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"fuel_guarded_inversion_Lib.IntTypes.inttype",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e"
],
0,
"c921001b109d376b860c9066cc5cd0a2"
],
[
"Lib.ByteSequence.index_uints_from_bytes_le",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_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.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Lib.IntTypes.inttype", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.int_t", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"110f2a08ac4bd0d0d8eea56797313d9f"
],
[
"Lib.ByteSequence.uints_from_bytes_be",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"fuel_guarded_inversion_Lib.IntTypes.inttype",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e"
],
0,
"7c1bf65059f9cc83e514b7b2310b3fb5"
],
[
"Lib.ByteSequence.index_uints_from_bytes_be",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_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_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.lseq",
"equation_Lib.Sequence.seq", "equation_Prims.nat",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Lib.IntTypes.inttype", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2b9ac1d6c43e9e240d84837e7e466c45",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.int_t", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"9f571dc1ef03c2e67782c24efb93bee4"
],
[
"Lib.ByteSequence.uint_at_index_le",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"fuel_guarded_inversion_Lib.IntTypes.inttype",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e"
],
0,
"0eef399c1d28d378a7904ac8051d0492"
],
[
"Lib.ByteSequence.uint_at_index_be",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.numbytes",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"fuel_guarded_inversion_Lib.IntTypes.inttype",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e"
],
0,
"57a711877fff392642d6fed3203b1138"
],
[
"Lib.ByteSequence.nat_from_intseq_le_lemma0",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_Lib.IntTypes.inttype", "int_typing",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"902b61ecf672bd39421d20138eff9fb8"
],
[
"Lib.ByteSequence.nat_from_intseq_le_slice_lemma",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d"
],
0,
"a47070c9ac509f67c5695a71eb3ae640"
],
[
"Lib.ByteSequence.nat_from_intseq_be_lemma0",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.unsigned",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"6e81b090a986f23f60baf5d99660d81f"
],
[
"Lib.ByteSequence.nat_from_intseq_be_slice_lemma",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Lib.Sequence.lseq",
"equation_Prims.nat", "int_inversion", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_11b83665e32383185d53564ec9a712ff",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42"
],
0,
"3e350eec58818f3f75fa29f2751c78a2"
],
[
"Lib.ByteSequence.uints_from_bytes_le_slice_lemma",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"bool_inversion", "constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "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_Prims.pos", "int_inversion",
"int_typing", "lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_88074ad798c65c6eaeec61d580898f58",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_a35511c8b912f5e79132bcf9d346d70c",
"refinement_interpretation_Tm_refine_d8d83307254a8900dd20598654272e42",
"refinement_interpretation_Tm_refine_edccc421660c61e3591d98071500d795",
"typing_FStar.Seq.Base.length", "typing_Lib.IntTypes.bits",
"typing_Lib.IntTypes.int_t", "typing_Lib.IntTypes.unsigned",
"typing_Lib.IntTypes.uu___is_U1", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"e28dc9a40a79e321e87a701ca070aeb5"
],
[
"Lib.ByteSequence.uints_from_bytes_le_nat_lemma",
1,
2,
1,
[
"@MaxIFuel_assumption", "@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.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2cca38936105581d33d174270a457f3d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e"
],
0,
"08fd506381987d025fa72d21bd01db0a"
],
[
"Lib.ByteSequence.uints_to_bytes_le_nat_lemma",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.numbytes", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Prims.nat",
"fuel_guarded_inversion_Lib.IntTypes.inttype", "int_inversion",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2196484e7ee5e6900b19fbaf8536cbec",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_614d8d7e05b589a57a746d819d64b1dd",
"refinement_interpretation_Tm_refine_9920ad7fdb83d776ac74c5ec84d5fe0e",
"refinement_interpretation_Tm_refine_be9f3762ef829e4292fadae5bee9b36d",
"typing_Lib.IntTypes.unsigned"
],
0,
"0857ef19f04f14fb5930609aeeebea98"
],
[
"Lib.ByteSequence.nat_from_intseq_le_inj",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Prims.nat",
"fuel_guarded_inversion_Lib.IntTypes.inttype",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.int_t", "typing_Lib.Sequence.length"
],
0,
"8e4af833269cc2bc2b89c58d32375ee0"
],
[
"Lib.ByteSequence.nat_from_intseq_be_inj",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.int_t", "typing_Lib.Sequence.length"
],
0,
"db80627a2b093021ec9ea3965c530fb1"
],
[
"Lib.ByteSequence.lemma_nat_to_from_bytes_be_preserves_value",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c2154f649da6a11d3390e748c5a9761d",
"refinement_interpretation_Tm_refine_c58ed13380a3b1fc4b109d0b978f6850"
],
0,
"60023775bc6370c102da2b01b04c7492"
],
[
"Lib.ByteSequence.lemma_nat_to_from_bytes_le_preserves_value",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c58ed13380a3b1fc4b109d0b978f6850"
],
0,
"72fbb02ce79922844fbab6135ec8805d"
],
[
"Lib.ByteSequence.lemma_uint_to_bytes_le_preserves_value",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.unsigned"
],
0,
"7b8ebf86c3dfa05b2b07f100d78aa163"
],
[
"Lib.ByteSequence.lemma_uint_to_bytes_be_preserves_value",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.unsigned"
],
0,
"af5bcb4300e23de8e69ae42cc2f720ec"
],
[
"Lib.ByteSequence.lemma_nat_from_to_intseq_le_preserves_value",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
"equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_28a7794573a2e47cefd724414092f328",
"refinement_interpretation_Tm_refine_387e6d282145573240ab7b8a4b94cce5",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"2e64d7f56afdbdbdac7d66eb290bc397"
],
[
"Lib.ByteSequence.lemma_nat_from_to_bytes_le_preserves_value",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned", "equation_Lib.Sequence.length",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_c58ed13380a3b1fc4b109d0b978f6850",
"typing_Prims.pow2"
],
0,
"dc6e122bfd4cd2839a34c71f459c5389"
],
[
"Lib.ByteSequence.lemma_reveal_uint_to_bytes_le",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"assumption_Lib.IntTypes.inttype__uu___haseq",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c5d756cb3510dba10939d8b44925c326",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.int_t", "typing_Lib.Sequence.length",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"c009af11a65150e1bd34cb5309a6f714"
],
[
"Lib.ByteSequence.lemma_reveal_uint_to_bytes_be",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"assumption_Lib.IntTypes.inttype__uu___haseq",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.U1", "equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"equation_Lib.Sequence.length", "equation_Prims.nat",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c5d756cb3510dba10939d8b44925c326",
"refinement_interpretation_Tm_refine_de8080fdc4bd6678af723874a7d70466",
"typing_Lib.IntTypes.int_t", "typing_Lib.Sequence.length",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"81bb829dbfef8d6c07ae26c21d4c76b5"
]
]
]
Computing file changes ...
