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
Vale.Math.Bits.fst.hints
[
"����\"\u0010X����X���\f",
[
[
"Vale.Math.Bits.b_i2b",
1,
1,
0,
[ "@query" ],
0,
"9324988ce74d3bb66dc77821eacdf8b7"
],
[
"Vale.Math.Bits.b_i2b",
2,
1,
0,
[ "@query" ],
0,
"10176636b42f5a5c6cb56c234e08d983"
],
[
"Vale.Math.Bits.b_b2i",
1,
1,
0,
[ "@query" ],
0,
"c9f6f1943be768de536e8a1bcade6189"
],
[
"Vale.Math.Bits.b_b2i",
2,
1,
0,
[ "@query" ],
0,
"885ee37dd9bd2e285fd45b13d6daf467"
],
[
"Vale.Math.Bits.b_uext",
1,
1,
0,
[ "@query" ],
0,
"90c2c8a7b76383ddb7a5caba9f243544"
],
[
"Vale.Math.Bits.b_uext",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"0287ca86b1b4a418d4944732b9c2bb32"
],
[
"Vale.Math.Bits.b_and",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"f3bfd47134f6de5cad39d182e4e46ded"
],
[
"Vale.Math.Bits.b_and",
2,
1,
0,
[ "@query" ],
0,
"fd94cd111d001f6b81ae519d43209283"
],
[
"Vale.Math.Bits.b_or",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"30243d163524447e9eecca1a0aa7e67e"
],
[
"Vale.Math.Bits.b_or",
2,
1,
0,
[ "@query" ],
0,
"813b16e8c9eb2c3a2e466e960cdc8c18"
],
[
"Vale.Math.Bits.b_xor",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"69756db9654dbb8ef0f7662c217ee1ee"
],
[
"Vale.Math.Bits.b_xor",
2,
1,
0,
[ "@query" ],
0,
"65530978024ba3d1f47b687107a18c63"
],
[
"Vale.Math.Bits.b_not",
1,
1,
0,
[ "@query" ],
0,
"d341a71ab9f319258d6f4228f198b86e"
],
[
"Vale.Math.Bits.b_not",
2,
1,
0,
[ "@query" ],
0,
"db3282b8e334131d72a2222a5bbdf852"
],
[
"Vale.Math.Bits.b_shl",
1,
1,
0,
[ "@query" ],
0,
"76b2bfaab0c184ac6b05dff2893890c0"
],
[
"Vale.Math.Bits.b_shl",
2,
1,
0,
[ "@query" ],
0,
"ec0b2d3b494390f0a0217f5bf3b16c8b"
],
[
"Vale.Math.Bits.b_shr",
1,
1,
0,
[ "@query" ],
0,
"55143d49c01429744f77be909da2c176"
],
[
"Vale.Math.Bits.b_shr",
2,
1,
0,
[ "@query" ],
0,
"438090baf57b0411ec9b161e3a8efc5f"
],
[
"Vale.Math.Bits.b_add",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"c9e22d2e9a5282a542519ee35100c415"
],
[
"Vale.Math.Bits.b_add",
2,
1,
0,
[ "@query" ],
0,
"491cd108d38c285e93461dee8189f239"
],
[
"Vale.Math.Bits.b_sub",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"c24155d77ba14b7d325d713a82e5ca29"
],
[
"Vale.Math.Bits.b_sub",
2,
1,
0,
[ "@query" ],
0,
"993070ef8a7a116de0d201e564d40138"
],
[
"Vale.Math.Bits.b_mul",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"61b7d911746c06b966efdeb071529dda"
],
[
"Vale.Math.Bits.b_mul",
2,
1,
0,
[ "@query" ],
0,
"20e5a24025d5ac314bb359e8dd857c91"
],
[
"Vale.Math.Bits.b_div",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"0a1deefb54e697b4b783ff6604720961"
],
[
"Vale.Math.Bits.b_div",
2,
1,
0,
[ "@query" ],
0,
"152f558a9b2b6d96a1223e42c40b3ff1"
],
[
"Vale.Math.Bits.b_mod",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"e9b25385cfee82bf9ce056ee19c27133"
],
[
"Vale.Math.Bits.b_mod",
2,
1,
0,
[ "@query" ],
0,
"8dcf4585dd9d9904f3c18c779857d57b"
],
[
"Vale.Math.Bits.uext",
1,
1,
0,
[ "@query" ],
0,
"9bc00a61e41ccc2344c6eaaf54817a79"
],
[
"Vale.Math.Bits.uext",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"primitive_Prims.op_AmpAmp", "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_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"20b8c3d78b28d3d3c2bb65b66b2a4d7d"
],
[
"Vale.Math.Bits.lemma_i2b_eq",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"625299c9b4d7c03dde10e7e881e1a30f"
],
[
"Vale.Math.Bits.lemma_i2b_eq",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"0b51e06ea77dc82dc69a2ff2c694957b"
],
[
"Vale.Math.Bits.lemma_i2b_eq",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"9f6d306ebc1d4498db5b2362ed790cfc"
],
[
"Vale.Math.Bits.lemma_i2b_uext",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.pos",
"equation_Vale.Math.Bits.uext",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "primitive_Prims.op_AmpAmp",
"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_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"5d883e056fabb1883eedffc869c38d3a"
],
[
"Vale.Math.Bits.lemma_i2b_uext",
2,
1,
0,
[ "@query" ],
0,
"fa0d311d3408025c8e2b029a3d9542c0"
],
[
"Vale.Math.Bits.lemma_i2b_uext",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Prims.pos", "equation_Vale.Math.Bits.uext",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "primitive_Prims.op_AmpAmp",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"d67fee299ca2d1e822e3dd36bbe8933a"
],
[
"Vale.Math.Bits.lemma_i2b_and",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"def68759f662aa3b578adb505dd7e1bd"
],
[
"Vale.Math.Bits.lemma_i2b_and",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"4326e6c9ac698fc8811c68c8d9959d2a"
],
[
"Vale.Math.Bits.lemma_i2b_and",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.BitVector.logand_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented", "@query",
"equation_FStar.UInt.logand", "equation_FStar.UInt.uint_t",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.BitVector.logand_vec", "typing_FStar.UInt.logand",
"typing_FStar.UInt.to_vec"
],
0,
"08bbdd4cf9e70822870183af0b442e9e"
],
[
"Vale.Math.Bits.lemma_i2b_or",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"7cad06d714caa58d95cfb217fcf274a4"
],
[
"Vale.Math.Bits.lemma_i2b_or",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"a3e97ca9ad9ca46fc7e4d0600ff9cb55"
],
[
"Vale.Math.Bits.lemma_i2b_or",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.BitVector.logor_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented", "@query",
"equation_FStar.UInt.logor", "equation_FStar.UInt.uint_t",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.BitVector.logor_vec", "typing_FStar.UInt.logor",
"typing_FStar.UInt.to_vec"
],
0,
"ba052215b61d18e66092249425d95b5e"
],
[
"Vale.Math.Bits.lemma_i2b_xor",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"951c398b2d455f74b0831cb1f974a36d"
],
[
"Vale.Math.Bits.lemma_i2b_xor",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"806eda33def75670e195055e6df0070b"
],
[
"Vale.Math.Bits.lemma_i2b_xor",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.BitVector.logxor_vec.fuel_instrumented",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "bool_typing",
"equation_FStar.UInt.logxor", "equation_FStar.UInt.uint_t",
"equation_Prims.eqtype", "equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.bool", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_create_len",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.BitVector.logxor_vec", "typing_FStar.UInt.logxor",
"typing_FStar.UInt.to_vec"
],
0,
"ae1009f3fae4d3cef7123b538b612061"
],
[
"Vale.Math.Bits.lemma_i2b_shl",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"2471b19a2c0a5a5fecb97a0c8c5b4a44"
],
[
"Vale.Math.Bits.lemma_i2b_shl",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"e66cbe7b5ea7ea099738bc24933637ca"
],
[
"Vale.Math.Bits.lemma_i2b_shl",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented", "@query",
"Prims_pretyping_f537159ed795b314b4e58c260361ae86", "b2t_def",
"bool_typing", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.shift_left",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.BitVector.shift_left_vec", "typing_FStar.UInt.to_vec"
],
0,
"37195be0659f90b16dc2958c8e3fc07a"
],
[
"Vale.Math.Bits.lemma_i2b_shr",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"11ed6be8b7860be6b2127ad7d79eaddb"
],
[
"Vale.Math.Bits.lemma_i2b_shr",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"0094f26299377f6a2f339e169dea0ee5"
],
[
"Vale.Math.Bits.lemma_i2b_shr",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_FStar.UInt.from_vec.fuel_instrumented",
"@fuel_irrelevance_FStar.UInt.from_vec.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.shift_right", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_FStar.UInt.from_vec.fuel_instrumented",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.BitVector.shift_right_vec", "typing_FStar.UInt.to_vec"
],
0,
"587ab7fc703f5f45f4b64d7cadcb8a2c"
],
[
"Vale.Math.Bits.lemma_i2b_add",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"7f45125db40464c2bac32ba9baf083a2"
],
[
"Vale.Math.Bits.lemma_i2b_add",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"e6a2221aec0c71ef05c281dfe7a366c3"
],
[
"Vale.Math.Bits.lemma_i2b_add",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_FStar.UInt.add_mod", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Prims.pow2"
],
0,
"54673b0ea9a687ef5158f29844eb1545"
],
[
"Vale.Math.Bits.lemma_i2b_sub",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"e96cd530394d1b0b6a40f9e924b30757"
],
[
"Vale.Math.Bits.lemma_i2b_sub",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"e1032dea13009fabbcda8bad0f61ef80"
],
[
"Vale.Math.Bits.lemma_i2b_sub",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_FStar.UInt.sub_mod", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Multiply", "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"
],
0,
"9265a2176b24e42e035a6dce4a34c31d"
],
[
"Vale.Math.Bits.lemma_i2b_mul",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"c1cd6052eeb385db129f5ba609c33ec5"
],
[
"Vale.Math.Bits.lemma_i2b_mul",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"9b95e3bd06871d6579e73a2604d263be"
],
[
"Vale.Math.Bits.lemma_i2b_mul",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_FStar.UInt.mul_mod", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"ee01183e08e5f20ec25fb81363b4dc05"
],
[
"Vale.Math.Bits.lemma_i2b_div",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"bb3e43d0f5a24df0cf1cc9e255933354"
],
[
"Vale.Math.Bits.lemma_i2b_div",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"aab5044aacd3d03355dcc3fbcf04175b"
],
[
"Vale.Math.Bits.lemma_i2b_div",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.UInt.udiv",
"equation_Prims.pos", "primitive_Prims.op_Division",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"bfbf2e6d13ee5a4b833ed9ec01da9b59"
],
[
"Vale.Math.Bits.lemma_i2b_mod",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"18850c8d68488bdef5dc513ab1721819"
],
[
"Vale.Math.Bits.lemma_i2b_mod",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"1a005ad8f492b497745326472433f372"
],
[
"Vale.Math.Bits.lemma_i2b_mod",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"cdf6a10e8ea251faf8dd2292390cbfe6"
],
[
"Vale.Math.Bits.add_hide",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"f213f34a37fa4f78a7e8325d1fdeb0b1"
],
[
"Vale.Math.Bits.add_hide",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"9c1448fb044f80985a288b67d078290e"
],
[
"Vale.Math.Bits.add_hide",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"equation_FStar.UInt.add_mod", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.pos", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"5fbca362433a9ff9c634df2d2cecc31a"
],
[
"Vale.Math.Bits.sub_hide",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"549f4e0ceefbf7668e8446e9317bd2d9"
],
[
"Vale.Math.Bits.sub_hide",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"4b3ac0da2a040fe5d960ed5e366cac50"
],
[
"Vale.Math.Bits.sub_hide",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.sub_mod", "equation_FStar.UInt.uint_t",
"equation_Prims.pos", "int_inversion", "int_typing",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"12d35fd5874c7814851a16d9441011f1"
],
[
"Vale.Math.Bits.mul_hide",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"ea9bea9c7d20624b206e61a48bd0e096"
],
[
"Vale.Math.Bits.mul_hide",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"7a00adc064b99cf3afdd584190738a06"
],
[
"Vale.Math.Bits.mul_hide",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"equation_FStar.UInt.fits", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_FStar.UInt.uint_t",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"1f9861baf945e0b29eadea9dee1e5881"
],
[
"Vale.Math.Bits.lemmas_i2b_all",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.pos",
"equation_Vale.Math.Bits.uext",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "primitive_Prims.op_AmpAmp",
"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_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"1224e6abe91e1c16e696298ce176f1d7"
],
[
"Vale.Math.Bits.lemma_i2b_all",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.pos",
"equation_Vale.Math.Bits.add_hide",
"equation_Vale.Math.Bits.lemmas_i2b_all",
"equation_Vale.Math.Bits.mul_hide",
"equation_Vale.Math.Bits.sub_hide", "equation_Vale.Math.Bits.uext",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "primitive_Prims.op_AmpAmp",
"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_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"265b01dc326b3026080269296de3e8d2"
],
[
"Vale.Math.Bits.lemma_i2b_with_all",
1,
1,
0,
[ "@query" ],
0,
"81b1fd12ac2c7cbdff444025dd7f2b8d"
],
[
"Vale.Math.Bits.lemma_i2b_equal",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"2fc34c0eccbee3ff587022e1b302a615"
],
[
"Vale.Math.Bits.lemma_i2b_equal",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"721d61ff343168f5bc5c60952f6590fe"
],
[
"Vale.Math.Bits.lemma_i2b_equal",
3,
1,
0,
[ "@query" ],
0,
"e6fdfe98fbcfcc8b3c81f7b9355c9d68"
],
[
"Vale.Math.Bits.is_bv8",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_e894bfc63f13ed92c34b8ee70610cbb6"
],
0,
"e691d1f216dd06e149a0ad047cadcd93"
],
[
"Vale.Math.Bits.is_bv16",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_83a3ed182b7b68b570641be544c91207"
],
0,
"343ec48198f0502dc0ddfd4b71247aef"
],
[
"Vale.Math.Bits.is_bv32",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_16ea53d011c0f3209db910ba5d81e7cc",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"15376663d3df56214361633c12403358"
],
[
"Vale.Math.Bits.is_bv64",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_typing",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_3ed95dcedf79b1d3435cb465289dbdb0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"7d4b9939bdc60eebe8b240bdac4d25c6"
],
[
"Vale.Math.Bits.bveq",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"815f9fd833edbf23d618e5bcf4be5ef0"
],
[
"Vale.Math.Bits.bveq",
2,
1,
0,
[ "@query" ],
0,
"a7f21bab6835ed00567131c32ad2f49e"
],
[
"Vale.Math.Bits.lemma_bveq",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"7d600f5d53312305358f9ab8ed24d02e"
],
[
"Vale.Math.Bits.lemma_bveq",
2,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"37e1f5bb73ea741504f88cceb16a2fa9"
],
[
"Vale.Math.Bits.lemma_bveq",
3,
0,
0,
[
"@MaxIFuel_assumption", "@query", "equation_FStar.UInt.logxor",
"equation_FStar.UInt.zero", "equation_Prims.pos", "int_inversion",
"lemma_FStar.BV.inverse_num_lemma",
"lemma_FStar.BV.inverse_vec_lemma",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_FStar.UInt.logxor"
],
0,
"fdad70145b8033f8be795c8ebb25d739"
],
[
"Vale.Math.Bits.lemma_to_is_bv8_bv",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.nat", "int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"4e2724a7bb2af4df6fab18206f286b36"
],
[
"Vale.Math.Bits.lemma_to_is_bv8",
1,
0,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "bool_inversion", "bool_typing",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Prims.nat", "int_inversion",
"int_typing", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec"
],
0,
"8e25ae5760f890b74bb7a7b651cbbd00"
]
]
]
Computing file changes ...
