Revision 1539fc67ec7cd1f092967452d8ae47d170ca149b authored by Jonathan Protzenko on 24 April 2020, 23:18:32 UTC, committed by Jonathan Protzenko on 24 April 2020, 23:18:32 UTC
1 parent 56130dc
Lib.IntTypes.fsti.hints
[
"��=�\u0001�qM��`�^\bh�",
[
[
"Lib.IntTypes.numbytes",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "disc_equation_Lib.IntTypes.S128",
"disc_equation_Lib.IntTypes.S16", "disc_equation_Lib.IntTypes.S32",
"disc_equation_Lib.IntTypes.S64", "disc_equation_Lib.IntTypes.S8",
"disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128",
"disc_equation_Lib.IntTypes.U16", "disc_equation_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.U8",
"fuel_guarded_inversion_Lib.IntTypes.inttype"
],
0,
"c33774dbd33e1a362a47c8d4f14417c8"
],
[
"Lib.IntTypes.bits",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "disc_equation_Lib.IntTypes.S128",
"disc_equation_Lib.IntTypes.S16", "disc_equation_Lib.IntTypes.S32",
"disc_equation_Lib.IntTypes.S64", "disc_equation_Lib.IntTypes.S8",
"disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128",
"disc_equation_Lib.IntTypes.U16", "disc_equation_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.U8",
"fuel_guarded_inversion_Lib.IntTypes.inttype"
],
0,
"746ac6519ebba5ad49553e4cfc8a9f5e"
],
[
"Lib.IntTypes.modulus",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
"fuel_guarded_inversion_Lib.IntTypes.inttype",
"projection_inverse_BoxInt_proj_0"
],
0,
"41d07cb07cce90f26934602b6d0c664a"
],
[
"Lib.IntTypes.maxint",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned",
"fuel_guarded_inversion_Lib.IntTypes.inttype",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0"
],
0,
"fdaaf59d41d3de78bac0536d0faad28e"
],
[
"Lib.IntTypes.minint",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.unsigned",
"fuel_guarded_inversion_Lib.IntTypes.inttype",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0"
],
0,
"6d3d526824c669104e90083159569577"
],
[
"Lib.IntTypes.pub_int_t",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "disc_equation_Lib.IntTypes.S128",
"disc_equation_Lib.IntTypes.S16", "disc_equation_Lib.IntTypes.S32",
"disc_equation_Lib.IntTypes.S64", "disc_equation_Lib.IntTypes.S8",
"disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128",
"disc_equation_Lib.IntTypes.U16", "disc_equation_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.U8",
"fuel_guarded_inversion_Lib.IntTypes.inttype"
],
0,
"eb99a4fb3ec0a9980340efb356d1faa9"
],
[
"Lib.IntTypes.pub_int_v",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"b2t_def", "constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.S16",
"disc_equation_Lib.IntTypes.S32", "disc_equation_Lib.IntTypes.S64",
"disc_equation_Lib.IntTypes.S8", "disc_equation_Lib.IntTypes.U1",
"disc_equation_Lib.IntTypes.U128", "disc_equation_Lib.IntTypes.U16",
"disc_equation_Lib.IntTypes.U32", "disc_equation_Lib.IntTypes.U64",
"disc_equation_Lib.IntTypes.U8", "equality_tok_Lib.IntTypes.U1@tok",
"equation_FStar.Int.fits", "equation_FStar.Int.max_int",
"equation_FStar.Int.min_int", "equation_FStar.Int.size",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt128.n", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.pub_int_t", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"fuel_guarded_inversion_Lib.IntTypes.inttype",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Minus",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_e0b16d74ee3644bd585df5e7938934c6",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U1@tok"
],
0,
"1ef3b044043a6e87c321e4c9424bb9fa"
],
[
"Lib.IntTypes.int_t",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "disc_equation_Lib.IntTypes.PUB",
"disc_equation_Lib.IntTypes.SEC",
"fuel_guarded_inversion_Lib.IntTypes.secrecy_level"
],
0,
"6863d144daf49b1b0990d34d62e1d3af"
],
[
"Lib.IntTypes.v",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "disc_equation_Lib.IntTypes.PUB",
"disc_equation_Lib.IntTypes.SEC", "equation_Lib.IntTypes.int_t",
"fuel_guarded_inversion_Lib.IntTypes.secrecy_level",
"projection_inverse_BoxBool_proj_0"
],
0,
"1f012c95f99d0446b7942676d4d91b66"
],
[
"Lib.IntTypes.uint1",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U1",
"equality_tok_Lib.IntTypes.U1@tok", "equation_Lib.IntTypes.unsigned",
"projection_inverse_BoxBool_proj_0"
],
0,
"7c858499e411c7cec76a8181ce7181e6"
],
[
"Lib.IntTypes.uint8",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"projection_inverse_BoxBool_proj_0"
],
0,
"025195e91233d3e4a4b2879541b32556"
],
[
"Lib.IntTypes.int8",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.S8",
"equality_tok_Lib.IntTypes.S8@tok", "equation_Lib.IntTypes.signed",
"projection_inverse_BoxBool_proj_0"
],
0,
"9d398fcb39261e5b8c5ea80ddaf19d5b"
],
[
"Lib.IntTypes.uint16",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U16",
"equality_tok_Lib.IntTypes.U16@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"9620e591292724b9e64148fbb2881ddc"
],
[
"Lib.IntTypes.int16",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.S16",
"equality_tok_Lib.IntTypes.S16@tok", "equation_Lib.IntTypes.signed",
"projection_inverse_BoxBool_proj_0"
],
0,
"ef652e26f8743a8a06b4acabbe2f09a7"
],
[
"Lib.IntTypes.uint32",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"81c5b2ea2955972bbaae726b72f8c031"
],
[
"Lib.IntTypes.int32",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.S32",
"equality_tok_Lib.IntTypes.S32@tok", "equation_Lib.IntTypes.signed",
"projection_inverse_BoxBool_proj_0"
],
0,
"910f6c1caabb7cf0d63e094f82069a9a"
],
[
"Lib.IntTypes.uint64",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"b1aecbfa6f802a096761d4e792b20754"
],
[
"Lib.IntTypes.int64",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.S64",
"equality_tok_Lib.IntTypes.S64@tok", "equation_Lib.IntTypes.signed",
"projection_inverse_BoxBool_proj_0"
],
0,
"4e90c091ae3197d782d00406753afb83"
],
[
"Lib.IntTypes.uint128",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.U128@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"84718d2f69845ceb9d48e3e4580afa57"
],
[
"Lib.IntTypes.int128",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.S128",
"equality_tok_Lib.IntTypes.S128@tok", "equation_Lib.IntTypes.signed",
"projection_inverse_BoxBool_proj_0"
],
0,
"9957551ddea769520a34e7776d8e6514"
],
[
"Lib.IntTypes.bit_t",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U1",
"equality_tok_Lib.IntTypes.U1@tok", "equation_Lib.IntTypes.unsigned",
"projection_inverse_BoxBool_proj_0"
],
0,
"542a1e311e65a78f89453bc251619795"
],
[
"Lib.IntTypes.byte_t",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"projection_inverse_BoxBool_proj_0"
],
0,
"d838589d4374e3abd8e9fcf41046c5ed"
],
[
"Lib.IntTypes.size_t",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"f84b0046a316a6cb66614af8795da910"
],
[
"Lib.IntTypes.size128_t",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.U128@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"f71dad27418f654a0601acc934672c45"
],
[
"Lib.IntTypes.pub_uint8",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"projection_inverse_BoxBool_proj_0"
],
0,
"1cb6cbfc57666f6373be73a3f72ec856"
],
[
"Lib.IntTypes.pub_int8",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.S8",
"equality_tok_Lib.IntTypes.S8@tok", "equation_Lib.IntTypes.signed",
"projection_inverse_BoxBool_proj_0"
],
0,
"5fb0525fafb62db62331caa99bfe1686"
],
[
"Lib.IntTypes.pub_uint16",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U16",
"equality_tok_Lib.IntTypes.U16@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"991304ce014872a21a6edb3df5a40752"
],
[
"Lib.IntTypes.pub_int16",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.S16",
"equality_tok_Lib.IntTypes.S16@tok", "equation_Lib.IntTypes.signed",
"projection_inverse_BoxBool_proj_0"
],
0,
"805c20ae074c03d60d19987d557a0943"
],
[
"Lib.IntTypes.pub_uint32",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"cef85bd6bccfca907ed97c1850c9fd91"
],
[
"Lib.IntTypes.pub_int32",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.S32",
"equality_tok_Lib.IntTypes.S32@tok", "equation_Lib.IntTypes.signed",
"projection_inverse_BoxBool_proj_0"
],
0,
"fb6a645e09999af7d2ec83bf8a1550a1"
],
[
"Lib.IntTypes.pub_uint64",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"69a3d85577f991ebdc320dc22a6d6a33"
],
[
"Lib.IntTypes.pub_int64",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.S64",
"equality_tok_Lib.IntTypes.S64@tok", "equation_Lib.IntTypes.signed",
"projection_inverse_BoxBool_proj_0"
],
0,
"7563e7b530905330908b79a259184065"
],
[
"Lib.IntTypes.pub_uint128",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.U128@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"2d19f7b365c3aa09d53faa9175cb8160"
],
[
"Lib.IntTypes.pub_int128",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.S128",
"equality_tok_Lib.IntTypes.S128@tok", "equation_Lib.IntTypes.signed",
"projection_inverse_BoxBool_proj_0"
],
0,
"35f0b136844b19e115a1088671f8c07f"
],
[
"Lib.IntTypes.u1",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U1",
"equality_tok_Lib.IntTypes.U1@tok", "equation_Lib.IntTypes.unsigned",
"projection_inverse_BoxBool_proj_0"
],
0,
"ecd4fa97131b14a84bcaea2c8d7442a5"
],
[
"Lib.IntTypes.u8",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U8@tok", "equation_Lib.IntTypes.unsigned",
"projection_inverse_BoxBool_proj_0"
],
0,
"8e7aa029163244ece9ace20840e2ec0f"
],
[
"Lib.IntTypes.i8",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.S8",
"equality_tok_Lib.IntTypes.S8@tok", "equation_Lib.IntTypes.signed",
"projection_inverse_BoxBool_proj_0"
],
0,
"26e0794368ddec896f7fa31530300b3a"
],
[
"Lib.IntTypes.u16",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U16",
"equality_tok_Lib.IntTypes.U16@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"5c9184ec0166c60e5708b6773bcf213c"
],
[
"Lib.IntTypes.i16",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.S16",
"equality_tok_Lib.IntTypes.S16@tok", "equation_Lib.IntTypes.signed",
"projection_inverse_BoxBool_proj_0"
],
0,
"153f4f852befb233f56d8afeabc2c1f2"
],
[
"Lib.IntTypes.u32",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"95427c166c3823cf0843296985b09d0c"
],
[
"Lib.IntTypes.i32",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.IntTypes.S32",
"equality_tok_Lib.IntTypes.S32@tok", "equation_Lib.IntTypes.signed",
"equation_Lib.IntTypes.unsigned",
"projection_inverse_BoxBool_proj_0", "typing_Lib.IntTypes.signed",
"typing_tok_Lib.IntTypes.S32@tok"
],
0,
"b8a6dbfdcb19d33c4ac314e8bb8a29d9"
],
[
"Lib.IntTypes.u64",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U64@tok",
"equation_Lib.IntTypes.unsigned", "projection_inverse_BoxBool_proj_0"
],
0,
"444296329d7f5677119681ba73aaeb85"
],
[
"Lib.IntTypes.i64",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "bool_inversion",
"constructor_distinct_Lib.IntTypes.S64",
"equality_tok_Lib.IntTypes.S64@tok", "equation_Lib.IntTypes.signed",
"equation_Lib.IntTypes.unsigned",
"projection_inverse_BoxBool_proj_0", "typing_Lib.IntTypes.signed",
"typing_tok_Lib.IntTypes.S64@tok"
],
0,
"d910bfc374f5c1580593cc50b181e8f0"
],
[
"Lib.IntTypes.u128",
1,
2,
1,
[ "@query" ],
0,
"30843caf33b5c7d9d6c8305cbfe6f94d"
],
[
"Lib.IntTypes.i128",
1,
0,
1,
[ "@query" ],
0,
"9e50455fc46475d1ef8021fa118f5eae"
],
[
"Lib.IntTypes.size",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.unsigned", "equation_Prims.nat",
"int_inversion", "projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2"
],
0,
"7ac5c93161b909ffd01118230bd8ec09"
],
[
"Lib.IntTypes.byte",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.U8",
"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", "int_inversion",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_31c7d3d85d92cb942c95a78642e657c7",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U8@tok"
],
0,
"7713e8026e8fd9076e85e4103a87c8bb"
],
[
"Lib.IntTypes.byte_v",
1,
0,
1,
[
"@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.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", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"904ab0f3c40927490d3a893687ff8a42"
],
[
"Lib.IntTypes.size_to_uint64",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@tok", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "lemma_FStar.UInt.pow2_values",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits", "typing_tok_Lib.IntTypes.U32@tok",
"typing_tok_Lib.IntTypes.U64@tok"
],
0,
"4bec021e1b7b2d0ab66578ffe16a6bf6"
],
[
"Lib.IntTypes.op_At_Percent_Dot",
1,
0,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_Lib.IntTypes.bits", "equation_Lib.IntTypes.unsigned",
"equation_Prims.nat", "fuel_guarded_inversion_Lib.IntTypes.inttype",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Modulus",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"typing_Lib.IntTypes.bits"
],
0,
"5267f6eca2c62a8b7c6666ddb83c9338"
],
[
"Lib.IntTypes.to_u1",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.SEC",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.SEC@tok",
"projection_inverse_BoxBool_proj_0"
],
0,
"d66b36f66cd09e162b15db4936aaf3f8"
],
[
"Lib.IntTypes.to_u8",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.SEC",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.SEC@tok",
"projection_inverse_BoxBool_proj_0"
],
0,
"8ae3c820f81162d70236830b1df17941"
],
[
"Lib.IntTypes.to_i8",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.SEC",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.SEC@tok",
"projection_inverse_BoxBool_proj_0"
],
0,
"1c98da1d32eb1353ccaf6fc3d54effaf"
],
[
"Lib.IntTypes.to_u16",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.SEC",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.SEC@tok",
"projection_inverse_BoxBool_proj_0"
],
0,
"080f04a662981643489a88aa65f77eb0"
],
[
"Lib.IntTypes.to_i16",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.SEC",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.SEC@tok",
"projection_inverse_BoxBool_proj_0"
],
0,
"c22a2527872dcdc28cb80aab88f9d030"
],
[
"Lib.IntTypes.to_u32",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.SEC",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.SEC@tok",
"projection_inverse_BoxBool_proj_0"
],
0,
"a2043c3b0100c618fa4802d9a1d26cb0"
],
[
"Lib.IntTypes.to_i32",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.SEC",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.SEC@tok",
"projection_inverse_BoxBool_proj_0"
],
0,
"c5c0a6199f2fe0b27cc53ab7cd41ae7a"
],
[
"Lib.IntTypes.to_u64",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.SEC",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.SEC@tok",
"projection_inverse_BoxBool_proj_0"
],
0,
"d6d5a9564bcf881bab4082eb615510a5"
],
[
"Lib.IntTypes.to_i64",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.SEC",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.SEC@tok",
"projection_inverse_BoxBool_proj_0"
],
0,
"211b3313baf6728937f2c5e142980120"
],
[
"Lib.IntTypes.to_u128",
1,
2,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.SEC",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.SEC@tok",
"projection_inverse_BoxBool_proj_0"
],
0,
"69c5b29d42b3c8b4d5540970fba0dfa3"
],
[
"Lib.IntTypes.to_i128",
1,
0,
1,
[
"@query", "constructor_distinct_Lib.IntTypes.SEC",
"disc_equation_Lib.IntTypes.SEC",
"equality_tok_Lib.IntTypes.SEC@tok",
"projection_inverse_BoxBool_proj_0"
],
0,
"fa2cd19372da86b03a0a922f9813bcae"
],
[
"Lib.IntTypes.ones_v",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "disc_equation_Lib.IntTypes.S128",
"disc_equation_Lib.IntTypes.S16", "disc_equation_Lib.IntTypes.S32",
"disc_equation_Lib.IntTypes.S64", "disc_equation_Lib.IntTypes.S8",
"disc_equation_Lib.IntTypes.U1", "disc_equation_Lib.IntTypes.U128",
"disc_equation_Lib.IntTypes.U16", "disc_equation_Lib.IntTypes.U32",
"disc_equation_Lib.IntTypes.U64", "disc_equation_Lib.IntTypes.U8",
"fuel_guarded_inversion_Lib.IntTypes.inttype"
],
0,
"8a3a360299a8a051356222d7c98d59a1"
],
[
"Lib.IntTypes.logxor_lemma",
1,
0,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"equality_tok_Lib.IntTypes.U128@tok",
"equality_tok_Lib.IntTypes.U16@tok",
"equality_tok_Lib.IntTypes.U1@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equality_tok_Lib.IntTypes.U64@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",
"fuel_guarded_inversion_Lib.IntTypes.inttype", "int_typing",
"primitive_Prims.op_Minus", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Lib.IntTypes.bits", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.U128@tok",
"typing_tok_Lib.IntTypes.U16@tok", "typing_tok_Lib.IntTypes.U1@tok",
"typing_tok_Lib.IntTypes.U32@tok", "typing_tok_Lib.IntTypes.U64@tok",
"typing_tok_Lib.IntTypes.U8@tok"
],
0,
"30296ac3369e8f7c6572a14a5e7b5a66"
],
[
"Lib.IntTypes.logxor_v",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.S16",
"disc_equation_Lib.IntTypes.S32", "disc_equation_Lib.IntTypes.S64",
"disc_equation_Lib.IntTypes.S8", "equation_FStar.Int.fits",
"equation_FStar.Int.max_int", "equation_FStar.Int.min_int",
"equation_FStar.Int.size", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"fuel_guarded_inversion_Lib.IntTypes.inttype", "int_inversion",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b"
],
0,
"a502b810ec786cf66e9551b0649de35a"
],
[
"Lib.IntTypes.logand_v",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.S16",
"disc_equation_Lib.IntTypes.S32", "disc_equation_Lib.IntTypes.S64",
"disc_equation_Lib.IntTypes.S8", "equation_FStar.Int.fits",
"equation_FStar.Int.max_int", "equation_FStar.Int.min_int",
"equation_FStar.Int.size", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"fuel_guarded_inversion_Lib.IntTypes.inttype", "int_inversion",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b"
],
0,
"e6d163827a48e8d2c63e71a8d4a7aa2b"
],
[
"Lib.IntTypes.logand_mask",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_812109ba662576a3f745174092d33c56"
],
0,
"82b6dfb9da34af294747b12eb9e6ef7c"
],
[
"Lib.IntTypes.logor_disjoint",
1,
2,
1,
[ "@query" ],
0,
"2d1e5e3a4c028e27ccc76cc8a9b95908"
],
[
"Lib.IntTypes.logor_v",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"constructor_distinct_Lib.IntTypes.S128",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U128",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.S16",
"disc_equation_Lib.IntTypes.S32", "disc_equation_Lib.IntTypes.S64",
"disc_equation_Lib.IntTypes.S8", "equation_FStar.Int.fits",
"equation_FStar.Int.max_int", "equation_FStar.Int.min_int",
"equation_FStar.Int.size", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.maxint", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.unsigned",
"fuel_guarded_inversion_Lib.IntTypes.inttype", "int_inversion",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b"
],
0,
"aedb358d749659fce1f62c7861af8565"
],
[
"Lib.IntTypes.shift_right_lemma",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"5f79284644d845dac290d4c8d2af22a2"
],
[
"Lib.IntTypes.shift_left",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"c17d3c57d5bb5b816ebbe55f63fd2647"
],
[
"Lib.IntTypes.shift_left_lemma",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"refinement_interpretation_Tm_refine_4d1a190ec02a669657768f0db44948f9",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"1625f6da231acb6190f739f0e620d498"
],
[
"Lib.IntTypes.shift_right_i",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_33026181614126bf2f989b87912ad69b"
],
0,
"6dac983778e22eeb6843ea34091a6f4c"
],
[
"Lib.IntTypes.shift_right_i",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_33026181614126bf2f989b87912ad69b"
],
0,
"01fee68a666e4d9376931ab41a6c345e"
],
[
"Lib.IntTypes.shift_left_i",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_33026181614126bf2f989b87912ad69b"
],
0,
"362eba5b53c76e905fdf97d4bb794097"
],
[
"Lib.IntTypes.shift_left_i",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_33026181614126bf2f989b87912ad69b"
],
0,
"94d47750102290bde930b10b44007413"
],
[
"Lib.IntTypes.rotate_right_i",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_fe1f2b0fb92318a15c076125042e53a3"
],
0,
"9018aeae3507a257bc44483e02221a7a"
],
[
"Lib.IntTypes.rotate_right_i",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_fe1f2b0fb92318a15c076125042e53a3"
],
0,
"5a73a69a2a4c2173f31c5dad4ea57a4b"
],
[
"Lib.IntTypes.rotate_left_i",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_fe1f2b0fb92318a15c076125042e53a3"
],
0,
"8ad7893b2585f69e779d5a7de995574a"
],
[
"Lib.IntTypes.rotate_left_i",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_fe1f2b0fb92318a15c076125042e53a3"
],
0,
"49f374d6228027b95406321bfd7dd585"
],
[
"Lib.IntTypes.mod_mask",
1,
1,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.range", "equation_Lib.IntTypes.shiftval",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5",
"typing_Lib.IntTypes.v", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"039a9b7a59c73ba9b84ab8479febf325"
],
[
"Lib.IntTypes.mod_mask",
2,
1,
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.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_FStar.Int.op_At_Percent", "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.shiftval",
"equation_Lib.IntTypes.unsigned", "equation_Lib.IntTypes.v",
"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",
"lemma_Lib.IntTypes.pow2_127",
"primitive_Prims.op_GreaterThanOrEqual", "primitive_Prims.op_Minus",
"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",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_ac5393c1a5eb4d36f425e5e42929859b",
"refinement_interpretation_Tm_refine_b6806f707b80b45deafff2826c0c9018",
"refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_Lib.IntTypes.bits", "typing_Lib.IntTypes.v",
"typing_Prims.pow2", "typing_tok_Lib.IntTypes.PUB@tok",
"typing_tok_Lib.IntTypes.U32@tok"
],
0,
"435849b74d3ddb2ed0f8bd25a72ef99b"
],
[
"Lib.IntTypes.mod_mask_lemma",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_Lib.IntTypes.PUB@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equation_FStar.UInt.fits",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.int_t",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.shiftval", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_ac5393c1a5eb4d36f425e5e42929859b",
"refinement_interpretation_Tm_refine_e40dba697735a60216c598c2a27841b5",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.UInt32.v", "typing_Lib.IntTypes.v",
"typing_tok_Lib.IntTypes.PUB@tok", "typing_tok_Lib.IntTypes.U32@tok"
],
0,
"63adcf3992a5ba9642934977eabc0aef"
],
[
"Lib.IntTypes.div",
1,
2,
1,
[ "@query", "assumption_Lib.IntTypes.inttype__uu___haseq" ],
0,
"ad392da52c70b64f5aaad040bd791cd7"
],
[
"Lib.IntTypes.div_lemma",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_e450d0eda8ec6ce5c9eff42d01f0e81a"
],
0,
"d11de636ff8dab8fe89872077a4b70b3"
],
[
"Lib.IntTypes.mod",
1,
2,
1,
[ "@query", "assumption_Lib.IntTypes.inttype__uu___haseq" ],
0,
"e8d90363ea140aa4ce91fbeb2094389b"
],
[
"Lib.IntTypes.mod_lemma",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query", "b2t_def", "bool_inversion",
"constructor_distinct_Lib.IntTypes.PUB",
"constructor_distinct_Lib.IntTypes.S16",
"constructor_distinct_Lib.IntTypes.S32",
"constructor_distinct_Lib.IntTypes.S64",
"constructor_distinct_Lib.IntTypes.S8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U16",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_Lib.IntTypes.U64",
"constructor_distinct_Lib.IntTypes.U8",
"disc_equation_Lib.IntTypes.S128", "disc_equation_Lib.IntTypes.U128",
"equality_tok_Lib.IntTypes.PUB@tok", "equation_FStar.Int.int_t",
"equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_FStar.UInt.uint_t", "equation_Lib.IntTypes.bits",
"equation_Lib.IntTypes.int_t", "equation_Lib.IntTypes.maxint",
"equation_Lib.IntTypes.minint", "equation_Lib.IntTypes.pub_int_t",
"equation_Lib.IntTypes.pub_int_v", "equation_Lib.IntTypes.range",
"equation_Lib.IntTypes.signed", "equation_Lib.IntTypes.unsigned",
"equation_Lib.IntTypes.v",
"fuel_guarded_inversion_Lib.IntTypes.inttype",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_15e0fa5b1a593e81b2c5f5ce75454fde",
"refinement_interpretation_Tm_refine_83845a86f2550cdf941eeb1d9b59602b",
"refinement_interpretation_Tm_refine_b550ca9347e0645a53715102a08d8fa1",
"refinement_interpretation_Tm_refine_c156ecc6eab05d1687a383ef171435eb",
"refinement_interpretation_Tm_refine_e450d0eda8ec6ce5c9eff42d01f0e81a",
"refinement_interpretation_Tm_refine_f13070840248fced9d9d60d77bdae3ec",
"typing_FStar.Int16.v", "typing_FStar.Int32.v",
"typing_FStar.Int64.v", "typing_FStar.Int8.v",
"typing_FStar.UInt8.v", "typing_Lib.IntTypes.unsigned",
"typing_Lib.IntTypes.uu___is_S128", "typing_Lib.IntTypes.v",
"typing_tok_Lib.IntTypes.PUB@tok"
],
0,
"e883585f4b776238387263447923afcb"
]
]
]
Computing file changes ...
