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
MerkleTree.Spec.fst.hints
[
"\b�\u0001\u001c�Cq��{� �L�\u0002",
[
[
"MerkleTree.Spec.hash2_raw",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"constructor_distinct_FStar.Integers.W32",
"constructor_distinct_FStar.Integers.W63",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U1",
"constructor_distinct_Lib.IntTypes.U8",
"constructor_distinct_Spec.Hash.Definitions.SHA2_256",
"equality_tok_FStar.Integers.W32@tok",
"equality_tok_FStar.Integers.W63@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Spec.Hash.Definitions.SHA2_256@tok",
"equation_Lib.IntTypes.uint8", "equation_MerkleTree.Spec.hash_alg",
"equation_MerkleTree.Spec.hash_raw", "equation_Prims.nat",
"equation_Spec.Hash.Definitions.block_length",
"equation_Spec.Hash.Definitions.block_word_length",
"equation_Spec.Hash.Definitions.bytes",
"equation_Spec.Hash.Definitions.bytes_hash",
"equation_Spec.Hash.Definitions.hash_length",
"equation_Spec.Hash.Definitions.hash_word_length",
"equation_Spec.Hash.Definitions.word_length",
"function_token_typing_Lib.IntTypes.uint8", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_b3e3751c3894f166dfde09b500dd73a6",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.length",
"typing_MerkleTree.Spec.hash_alg",
"typing_Spec.Hash.Definitions.block_length"
],
0,
"ef4c38bb3714e8b55353ff20d6444551"
],
[
"MerkleTree.Spec.__proj__HRaw__item__hr",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_MerkleTree.Spec.HRaw",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_063a76819a1472a4e99c861adf5ddd89"
],
0,
"48b3dbf6f6a465869602ac9fd44a68ab"
],
[
"MerkleTree.Spec.hash2",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"disc_equation_MerkleTree.Spec.HPad",
"disc_equation_MerkleTree.Spec.HRaw",
"fuel_guarded_inversion_MerkleTree.Spec.hash", "inversion-interp",
"proj_equation_FStar.Pervasives.Native.Mktuple2__1",
"proj_equation_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2"
],
0,
"79e6cd302e3caaa2aa539adbfc8e43bd"
],
[
"MerkleTree.Spec.merkle_tree",
1,
2,
1,
[ "@query" ],
0,
"6e8237e6e70ea071821be0aa8da4fd4e"
],
[
"MerkleTree.Spec.mt_get",
1,
0,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_MerkleTree.Spec.merkle_tree",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311"
],
0,
"63e5afaf9d268f2e429446fc007016f6"
],
[
"MerkleTree.Spec.mt_left",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"b99356fdbf38ecc0618b97f1cb350d9a"
],
[
"MerkleTree.Spec.mt_left",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"data_typing_intro_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"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_44b773e7bd23d63db1729dc48dc75643",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6ed4fdba1ed3b2f4b96dac68faab3b9a",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"typing_FStar.Seq.Base.length"
],
0,
"fb4ad2ad401a0e2b6f610b47da9294c5"
],
[
"MerkleTree.Spec.mt_left",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"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_6ed4fdba1ed3b2f4b96dac68faab3b9a",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_FStar.Seq.Base.length", "typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"79b7a315b4ca79f2b05a1b067332732a"
],
[
"MerkleTree.Spec.mt_right",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"c8efbe1082f5ed3398a40666fb054c71"
],
[
"MerkleTree.Spec.mt_right",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"data_typing_intro_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"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_44b773e7bd23d63db1729dc48dc75643",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"typing_FStar.Seq.Base.length", "typing_Prims.pow2"
],
0,
"55ce2143e0b7fa4e6863851561755f8b"
],
[
"MerkleTree.Spec.mt_right",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"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_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_FStar.Seq.Base.length", "typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"90fdb5857d31d90a151bf3bf00d754d5"
],
[
"MerkleTree.Spec.mt_left_right",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"data_typing_intro_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Base.op_At_Bar",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_left",
"equation_MerkleTree.Spec.mt_right", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"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_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_44b773e7bd23d63db1729dc48dc75643",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar",
"typing_MerkleTree.Spec.mt_left", "typing_MerkleTree.Spec.mt_right",
"typing_Prims.pow2"
],
0,
"31431df60d2f6e33881b905ca573ed0e"
],
[
"MerkleTree.Spec.mt_left_right",
2,
1,
0,
[ "@query" ],
0,
"62ae3a054a49d3b9a7c3befd61c7e44f"
],
[
"MerkleTree.Spec.mt_left_right",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Base.op_At_Bar",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_left",
"equation_MerkleTree.Spec.mt_right", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"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_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.op_At_Bar",
"typing_MerkleTree.Spec.mt_left", "typing_MerkleTree.Spec.mt_right",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"4b82403e0c6a00da7047c21c2a73512a"
],
[
"MerkleTree.Spec.hs_next_lv",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"bd69026f0c4089839a2423bc2991cf01"
],
[
"MerkleTree.Spec.hs_next_lv",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"8de6792a2d8de6e619065ad30bada033"
],
[
"MerkleTree.Spec.hs_next_lv",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_74e85aa672b15838ae0cbea432fb7aab_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Properties.cons",
"equation_MerkleTree.Spec.hash_seq", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"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_23198fb1eb94d082115a4c69de813cb0",
"refinement_interpretation_Tm_refine_2c4e1c971bb0b5100a4cfae9ed3843c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"4b96d5e6022c36c2947805197b50de18"
],
[
"MerkleTree.Spec.hs_next_lv_index",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_MerkleTree.Spec.hs_next_lv"
],
0,
"3d80d157d6a481cd72380924ec937dbb"
],
[
"MerkleTree.Spec.hs_next_lv_index",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_7fd955f9dfae0f9cdc7a6c3521db7fb4",
"typing_MerkleTree.Spec.hs_next_lv"
],
0,
"561415c192cd5363d78ac93b7790dd62"
],
[
"MerkleTree.Spec.hs_next_lv_index",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_74e85aa672b15838ae0cbea432fb7aab_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_e1beddd2e70f1dfd04dde9bc6d0479db_2",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Properties.cons",
"equation_MerkleTree.Spec.hash2",
"equation_MerkleTree.Spec.hash_seq", "equation_Prims.nat",
"equation_with_fuel_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "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_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2c4e1c971bb0b5100a4cfae9ed3843c2",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_dbafcf6ee852392ba6d4465af96e1a6f",
"token_correspondence_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_MerkleTree.Spec.hash2", "typing_MerkleTree.Spec.hs_next_lv",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"87d8622fcaa66344b20bd72f36dbc4ec"
],
[
"MerkleTree.Spec.hs_next_lv_slice",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash_seq", "equation_Prims.nat",
"int_inversion", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"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_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8900c7662303173c9b65a70de0db9314",
"refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
"typing_MerkleTree.Spec.hs_next_lv",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"c6d62c82e485227811a2aad7ca28e78d"
],
[
"MerkleTree.Spec.hs_next_lv_slice",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash_seq", "equation_Prims.nat",
"int_inversion", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"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_122e30c14c97dc2041716cbe93e891a5",
"refinement_interpretation_Tm_refine_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8900c7662303173c9b65a70de0db9314",
"typing_MerkleTree.Spec.hs_next_lv",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"f05eb30c32c73226bfabf484462fae48"
],
[
"MerkleTree.Spec.hs_next_lv_slice",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_74e85aa672b15838ae0cbea432fb7aab_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_f6d4b18f07322bcfa4e6a482d27a0ca2_3",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equality_tok_Prims.LexTop@tok", "equation_MerkleTree.Spec.hash_seq",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_with_fuel_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.cons_index_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Seq.Properties.slice_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"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_055a3359dfb26bc47e1615a1b6632c6a",
"refinement_interpretation_Tm_refine_09d2e9ab3b9c121b24316d151747e281",
"refinement_interpretation_Tm_refine_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_1c7aee6393ba3979da6d719ae7f71ff7",
"refinement_interpretation_Tm_refine_2c4e1c971bb0b5100a4cfae9ed3843c2",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_MerkleTree.Spec.hs_next_lv",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"6961218daf9ae46a3511ff223c49cf77"
],
[
"MerkleTree.Spec.mt_next_lv",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"521bfda33a46a52d636b32e1338bb1f5"
],
[
"MerkleTree.Spec.mt_next_lv",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44b773e7bd23d63db1729dc48dc75643",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001"
],
0,
"1d3d4f727a1cb935c72224f9d536ddea"
],
[
"MerkleTree.Spec.mt_next_lv",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311"
],
0,
"5a0a7a3638438c3d3d55635727cd7549"
],
[
"MerkleTree.Spec.mt_next_lv_mt_left",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_f641999d6ed36014062ea5dbfe670585"
],
0,
"1c279df900a0ff6cf98da9ec1db7e536"
],
[
"MerkleTree.Spec.mt_next_lv_mt_left",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_left",
"equation_MerkleTree.Spec.mt_next_lv", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"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_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_9439a21fa960e31671c16e484ec50b5d",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"refinement_interpretation_Tm_refine_f641999d6ed36014062ea5dbfe670585",
"typing_MerkleTree.Spec.hs_next_lv",
"typing_MerkleTree.Spec.mt_left",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"c9efa67c8f7cb5f770cf804ae6dd15cb"
],
[
"MerkleTree.Spec.mt_next_lv_mt_right",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_f641999d6ed36014062ea5dbfe670585"
],
0,
"cf26b308f89fd5a1110361ad3378d2ca"
],
[
"MerkleTree.Spec.mt_next_lv_mt_right",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_next_lv",
"equation_MerkleTree.Spec.mt_right", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"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_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"refinement_interpretation_Tm_refine_f641999d6ed36014062ea5dbfe670585",
"typing_MerkleTree.Spec.hs_next_lv",
"typing_MerkleTree.Spec.mt_right",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"f1fb75782e02feab5c0ee200350fdd45"
],
[
"MerkleTree.Spec.hs_next_lv_equiv",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Division",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_60d621a26e5887485ae506e453a89824",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"4ba2015f5e4352bb7fb602c35994cfef"
],
[
"MerkleTree.Spec.hs_next_lv_equiv",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash_seq", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"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_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_60d621a26e5887485ae506e453a89824",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f97fad2c1fb2db1c8f88c401525f4a64",
"typing_FStar.Seq.Base.slice", "typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"54f9952f805ed6cb01cee0880c1bc99e"
],
[
"MerkleTree.Spec.mt_next_lv_equiv",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"primitive_Prims.op_Division", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0c2c2fc2e950c568d5764840f56db0fe",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_MerkleTree.Spec.mt_next_lv"
],
0,
"a2cfe06b112500670de26bb124ce038f"
],
[
"MerkleTree.Spec.mt_next_lv_equiv",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_next_lv", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44b773e7bd23d63db1729dc48dc75643",
"refinement_interpretation_Tm_refine_4e0e1fb5fb12de93e935ac38694f02cb",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"edcbc614668e3074eaf2e1bba668f911"
],
[
"MerkleTree.Spec.mt_next_lv_equiv",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_next_lv", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0c2c2fc2e950c568d5764840f56db0fe",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311"
],
0,
"0648f2232288a5be44bc00c164161397"
],
[
"MerkleTree.Spec.hs_next_rel",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"c2c8fc627c4377e80669596fe3f35c66"
],
[
"MerkleTree.Spec.hs_next_rel",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"48e5a15355c110249f84d1f24f88204f"
],
[
"MerkleTree.Spec.hs_next_rel",
3,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c"
],
0,
"e371c1002160323ab076660db997c157"
],
[
"MerkleTree.Spec.mt_next_rel",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"119b9e27640986c4f23363155ff601f2"
],
[
"MerkleTree.Spec.mt_next_rel",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"9d60e8de6783fadba434427db7227f9a"
],
[
"MerkleTree.Spec.mt_next_rel",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"kinding_MerkleTree.Spec.hash@tok", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_FStar.Seq.Base.length", "typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"71bc506c329932660bb887bcf9942710"
],
[
"MerkleTree.Spec.hs_next_rel_next_lv",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"7c9fce9e5fdbddd034d8559fe5829f5a"
],
[
"MerkleTree.Spec.hs_next_rel_next_lv",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"c0f5b6aabb9373bc9363c074cffb1448"
],
[
"MerkleTree.Spec.hs_next_rel_next_lv",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_74e85aa672b15838ae0cbea432fb7aab_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_de0af632c07461500a53c61a5f345eaf_2",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Properties.cons",
"equation_MerkleTree.Spec.hash2",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.hs_next_rel", "equation_Prims.nat",
"equation_with_fuel_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"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_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2c4e1c971bb0b5100a4cfae9ed3843c2",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_6d6565172f85a789b3f79e0a34b51e79",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_MerkleTree.Spec.hash2",
"typing_MerkleTree.Spec.hs_next_lv",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"0051e634ba68359244c3d130aa843643"
],
[
"MerkleTree.Spec.hs_next_rel_next_lv",
4,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"a5f2ea356a8803536d24019a3d2271b5"
],
[
"MerkleTree.Spec.hs_next_rel_next_lv",
5,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.eqtype",
"equation_Prims.nat", "function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"6c155b20d7c4cb18df50dd1352d3e9d8"
],
[
"MerkleTree.Spec.mt_next_rel_next_lv",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"853e132bfdf28c9df36f966ae4b21024"
],
[
"MerkleTree.Spec.mt_next_rel_next_lv",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"5d2bd0905f8033666156529da59bb0b0"
],
[
"MerkleTree.Spec.mt_next_rel_next_lv",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_next_lv",
"equation_MerkleTree.Spec.mt_next_rel", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"kinding_MerkleTree.Spec.hash@tok", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_FStar.Seq.Base.length", "typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"1e7fb2d72f99df9a49311efd5dae51ee"
],
[
"MerkleTree.Spec.mt_next_rel_upd_even",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_len_upd", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_846c786b74a0ea856ce37380641c5798",
"refinement_interpretation_Tm_refine_ab0ebeb866adf6f02fb0a71da7fe725d",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"cbbf28005e4eb91c01bca653ddec4572"
],
[
"MerkleTree.Spec.mt_next_rel_upd_even",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"001c6c3fad9c7e9e80f2a0056c537e14"
],
[
"MerkleTree.Spec.mt_next_rel_upd_even",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash2",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.hs_next_rel",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_next_rel", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"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_846c786b74a0ea856ce37380641c5798",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_FStar.Seq.Base.index", "typing_MerkleTree.Spec.hash2",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"d8597f657a1c2c1fee054ef9ec612a5e"
],
[
"MerkleTree.Spec.mt_next_rel_upd_even_pad",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_len_upd", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_846c786b74a0ea856ce37380641c5798",
"refinement_interpretation_Tm_refine_ab0ebeb866adf6f02fb0a71da7fe725d",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"8cc9157d7a7e54e88739c0b91c9fa7b6"
],
[
"MerkleTree.Spec.mt_next_rel_upd_even_pad",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"19e186b279315b55bf1c31ced599425d"
],
[
"MerkleTree.Spec.mt_next_rel_upd_even_pad",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"constructor_distinct_MerkleTree.Spec.HPad",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash2",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.hs_next_rel",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_next_rel", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"primitive_Prims.op_Addition", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_846c786b74a0ea856ce37380641c5798",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"ca3fffe95599a31f1fc458e6f4184994"
],
[
"MerkleTree.Spec.mt_next_rel_upd_odd",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_len_upd", "primitive_Prims.op_Addition",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_2ca062977a42c36634b89c1c4f193f79",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_846c786b74a0ea856ce37380641c5798",
"refinement_interpretation_Tm_refine_ab0ebeb866adf6f02fb0a71da7fe725d",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"263061654b53e90c390bff8e4e32023a"
],
[
"MerkleTree.Spec.mt_next_rel_upd_odd",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"int_inversion", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"b70138f81d3e751250653aedcdd5e225"
],
[
"MerkleTree.Spec.mt_next_rel_upd_odd",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash2",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.hs_next_rel",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_next_rel", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"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_846c786b74a0ea856ce37380641c5798",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_FStar.Seq.Base.index", "typing_MerkleTree.Spec.hash2",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"1eb61a0509a18548b8956e31a518e54f"
],
[
"MerkleTree.Spec.mt_get_root",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_0d7a6896029700a85fe0c3d10ba2ae3d_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_Prims.pow2", "well-founded-ordering-on-nat"
],
0,
"e55ec918035c3c58cdbe64c5f2d0c5b4"
],
[
"MerkleTree.Spec.mt_get_root_step",
1,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"2638a19ab68c56ce3ea5b691afdfaae7"
],
[
"MerkleTree.Spec.mt_get_root_step",
2,
2,
0,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.pos",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5"
],
0,
"d39903bd0dbf37e690f50ec7ffe3ebb3"
],
[
"MerkleTree.Spec.mt_get_root_step",
3,
2,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"@fuel_correspondence_MerkleTree.Spec.mt_get_root.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.mt_get_root.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_8dc66d82b3c89c3d7652aca061721fce_1",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Properties.cons",
"equation_MerkleTree.Spec.hash2",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_left",
"equation_MerkleTree.Spec.mt_next_lv",
"equation_MerkleTree.Spec.mt_right", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"equation_with_fuel_MerkleTree.Spec.mt_get_root.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "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_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.empty",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_MerkleTree.Spec.hash2", "typing_MerkleTree.Spec.mt_get_root",
"typing_MerkleTree.Spec.mt_left",
"typing_MerkleTree.Spec.mt_next_lv",
"typing_MerkleTree.Spec.mt_right", "typing_Prims.pow2",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"12d443f895b87e5c1fe3f4d949a3d0ed"
],
[
"MerkleTree.Spec.mt_get_path",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_0d7a6896029700a85fe0c3d10ba2ae3d_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_d4bca0c4915c238b6addaedcb52016ab_2",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Properties.cons",
"equation_FStar.Seq.Properties.lseq",
"equation_MerkleTree.Spec.merkle_path",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality", "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_00bcd8319bec077649985b5de4f97724",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.empty",
"typing_FStar.Seq.Base.length",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"0df266cdd37243ff71575223952e43de"
],
[
"MerkleTree.Spec.mt_verify_",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"binder_x_6162d906b2260bad672319e640fcb372_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_d4bca0c4915c238b6addaedcb52016ab_2",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Properties.lseq",
"equation_FStar.Seq.Properties.tail",
"equation_MerkleTree.Spec.merkle_path", "equation_Prims.nat",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"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_00bcd8319bec077649985b5de4f97724",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"af8d0410bc1785e317e51a5440ca763f"
],
[
"MerkleTree.Spec.mt_verify",
1,
2,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.mt_verify_.fuel_instrumented",
"@query", "equation_Prims.eq2", "equation_Prims.squash",
"equation_Prims.subtype_of",
"l_quant_interp_5b2993f9f2c0eba3627049a3b4167c7a",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c"
],
0,
"da86ba542fdddef877efac0e8992413b"
],
[
"MerkleTree.Spec.hs_next_lv_get",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"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_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_9581c37592f14f4e9181b056e5f7db68"
],
0,
"650bb9d254b61528f3d30c043000ad65"
],
[
"MerkleTree.Spec.hs_next_lv_get",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat", "equation_Prims.pos",
"function_token_typing_Prims.__cache_version_number__",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality", "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_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_a493152fcc101b98bcb97e0f9144b010"
],
0,
"929959a1a59bdff1c213411137d4bf9a"
],
[
"MerkleTree.Spec.hs_next_lv_get",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_144ae6abe17a1cfabe55c8653e1130b6_2",
"binder_x_f23bbb683acf794ae7f814ebe04d18bc_1",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Properties.cons",
"equation_MerkleTree.Spec.hash2",
"equation_MerkleTree.Spec.hash_seq", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual", "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_092798ae5a6cef9c1c82401e5fdac3d8",
"refinement_interpretation_Tm_refine_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_a61c908bd5cb2ea8836adb7f08ff9bba",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e10240bee6c2fbc030cf8b9170454570",
"token_correspondence_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_MerkleTree.Spec.hash2", "typing_MerkleTree.Spec.hs_next_lv",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"1be24fdc0ce64db11b238c9befe160f8"
],
[
"MerkleTree.Spec.mt_next_lv_get",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"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_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_baba3c4ff195e8afc82d572a0bec0709",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_MerkleTree.Spec.mt_next_lv"
],
0,
"dcaa2fe64b0dab860dfef513856e4f24"
],
[
"MerkleTree.Spec.mt_next_lv_get",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_next_lv", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_44b773e7bd23d63db1729dc48dc75643",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_baba3c4ff195e8afc82d572a0bec0709"
],
0,
"aa45effd8ac997ee483293f4adc54c8d"
],
[
"MerkleTree.Spec.mt_next_lv_get",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_next_lv", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_baba3c4ff195e8afc82d572a0bec0709",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311"
],
0,
"b73bb52a50b7fd088477fa78d12d36ed"
],
[
"MerkleTree.Spec.mt_get_path_ok_",
1,
2,
1,
[ "@query" ],
0,
"134066b6a60b084f783edfbc14d778ee"
],
[
"MerkleTree.Spec.mt_get_path_ok_",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.mt_get_path.fuel_instrumented",
"@fuel_correspondence_MerkleTree.Spec.mt_get_root.fuel_instrumented",
"@fuel_correspondence_MerkleTree.Spec.mt_verify_.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.mt_get_path.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.mt_get_root.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.mt_verify_.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_0d7a6896029700a85fe0c3d10ba2ae3d_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0",
"binder_x_d4bca0c4915c238b6addaedcb52016ab_2",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Properties.cons",
"equation_FStar.Seq.Properties.head",
"equation_FStar.Seq.Properties.lseq",
"equation_FStar.Seq.Properties.tail",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_path",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_get",
"equation_MerkleTree.Spec.mt_next_lv", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_MerkleTree.Spec.mt_get_path.fuel_instrumented",
"equation_with_fuel_MerkleTree.Spec.mt_get_root.fuel_instrumented",
"equation_with_fuel_MerkleTree.Spec.mt_verify_.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual", "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_00bcd8319bec077649985b5de4f97724",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_baba3c4ff195e8afc82d572a0bec0709",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"token_correspondence_MerkleTree.Spec.mt_get_path.fuel_instrumented",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_MerkleTree.Spec.mt_get",
"typing_MerkleTree.Spec.mt_get_path",
"typing_MerkleTree.Spec.mt_next_lv",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"16dd8514eef083ee0f6e9bb658a4b0d5"
],
[
"MerkleTree.Spec.raw_hashes",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"binder_x_1874aac7ff73f5008d26e73923d0310d_0",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.tail",
"equation_MerkleTree.Spec.hash_seq", "equation_Prims.nat",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Equality", "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_81407705a0828c2c1b1976675443f647",
"typing_FStar.Seq.Base.length",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"72db97d09c3c93b50bf18b40797eb40d"
],
[
"MerkleTree.Spec.raw_hashes_raws",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"b2t_def", "binder_x_baf33fe09ef48fe410db04c4a9678d12_0",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.tail",
"equation_MerkleTree.Spec.hash_seq", "equation_Prims.nat",
"equation_with_fuel_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"l_and-interp", "lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Equality", "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_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_98ad48bdc5613c44800483a86ff65dea",
"typing_FStar.Seq.Base.length",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"66556066708f4ae605cbe95652aa68b4"
],
[
"MerkleTree.Spec.raw_hashes_index",
1,
2,
1,
[ "@query" ],
0,
"6d635b78b1da4143574251f56ceb2655"
],
[
"MerkleTree.Spec.raw_hashes_index",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"binder_x_1874aac7ff73f5008d26e73923d0310d_0",
"binder_x_f327f36093d0fca65c344e5891b0e2a5_1",
"disc_equation_MerkleTree.Spec.HRaw",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.head",
"equation_FStar.Seq.Properties.tail",
"equation_MerkleTree.Spec.hash_seq", "equation_Prims.nat",
"equation_with_fuel_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"l_and-interp", "lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_077d3dfe05d71a635f5cb31ad78c5142",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_4b3ffcb73dba2b49ff1889589ba27d4d",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"typing_FStar.Seq.Base.length",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"bdac9266ab921c156e7a6152f6090d53"
],
[
"MerkleTree.Spec.raw_hashes_slice",
1,
2,
1,
[ "@query" ],
0,
"a3e5205679bf0b3d2840aefb7f850373"
],
[
"MerkleTree.Spec.raw_hashes_slice",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"binder_x_1874aac7ff73f5008d26e73923d0310d_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_dfe151a9f596e665b9f5c1efdef2e56c_2",
"disc_equation_MerkleTree.Spec.HRaw",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.head",
"equation_MerkleTree.Spec.hash_seq", "equation_Prims.eqtype",
"equation_Prims.nat",
"equation_with_fuel_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.lemma_tail_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_a198230921c96fcb46227477f6787e51",
"refinement_interpretation_Tm_refine_b138bd5848d4184f7632587e6e4bcf9f",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"true_interp", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_tok_MerkleTree.Spec.HPad@tok",
"well-founded-ordering-on-nat"
],
0,
"1bcb652c771a437c6c4ee23cfcc33498"
],
[
"MerkleTree.Spec.pad_hashes_slice",
1,
2,
1,
[ "@query" ],
0,
"a422330e17e7eee068535736b0cdd4eb"
],
[
"MerkleTree.Spec.pad_hashes_slice",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_1874aac7ff73f5008d26e73923d0310d_0",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_dfe151a9f596e665b9f5c1efdef2e56c_2",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equality_tok_Prims.LexTop@tok", "equation_MerkleTree.Spec.hash_seq",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_with_fuel_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_a198230921c96fcb46227477f6787e51",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.empty",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"3c4445b26c63553baec251f17ceaffba"
],
[
"MerkleTree.Spec.rpmt",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_62965edeceead4d487e326631269edf4",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311"
],
0,
"40848ad8daef8c90eeacb0f776fe107e"
],
[
"MerkleTree.Spec.rpmt_raws",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.rpmt", "equation_Prims.nat",
"int_inversion", "primitive_Prims.op_LessThanOrEqual",
"projection_inverse_BoxBool_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_62965edeceead4d487e326631269edf4",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"refinement_interpretation_Tm_refine_fe5bfde21a5cf527c4834d999126bd26"
],
0,
"364a84fcc4477a6ef144a7bfd514575b"
],
[
"MerkleTree.Spec.rpmt_i_0",
1,
2,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Prims.pow2"
],
0,
"3cc17f1cc38485c3b901d5126e545f4b"
],
[
"MerkleTree.Spec.rpmt_i_0",
2,
2,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.pos",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"typing_Prims.pow2"
],
0,
"842358c3e32d4ff230f73b3dd217e67b"
],
[
"MerkleTree.Spec.rpmt_i_0",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.rpmt", "equation_Prims.nat",
"equation_with_fuel_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"int_inversion", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Properties.slice_length",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"refinement_interpretation_Tm_refine_fe5bfde21a5cf527c4834d999126bd26",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"899d615eb7a98b82e72ecaa861086d36"
],
[
"MerkleTree.Spec.rpmt_left",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion",
"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_62965edeceead4d487e326631269edf4",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001"
],
0,
"3e010331380b8f12a95881135fceef3a"
],
[
"MerkleTree.Spec.rpmt_left",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"data_typing_intro_MerkleTree.Spec.HPad@tok",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_left", "equation_MerkleTree.Spec.rpmt",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.Seq.Properties.slice_slice",
"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_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_44b773e7bd23d63db1729dc48dc75643",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_62965edeceead4d487e326631269edf4",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_ceff76a60859de17cf8827afe3dd6dac",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f718e85bbba8993735044bc51d331c54",
"refinement_interpretation_Tm_refine_fe5bfde21a5cf527c4834d999126bd26",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.empty",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_MerkleTree.Spec.mt_left",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"f0bcce3770688a90d60ab3b2131cbc30"
],
[
"MerkleTree.Spec.rpmt_left",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_left", "equation_MerkleTree.Spec.rpmt",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.Seq.Properties.slice_slice",
"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_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_4a5da65b7b8968b5aec399d91ecaf336",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_62965edeceead4d487e326631269edf4",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_ceff76a60859de17cf8827afe3dd6dac",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"refinement_interpretation_Tm_refine_f718e85bbba8993735044bc51d331c54",
"refinement_interpretation_Tm_refine_fe5bfde21a5cf527c4834d999126bd26",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.empty",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_MerkleTree.Spec.mt_left",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"511d373071900ada745cd0d8fd82a1c8"
],
[
"MerkleTree.Spec.rpmt_right",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_Prims.pow2.fuel_instrumented", "int_inversion",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Multiply",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_62965edeceead4d487e326631269edf4",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001"
],
0,
"e30fa3e680a999ddddc02ab69c633b4e"
],
[
"MerkleTree.Spec.rpmt_right",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"@fuel_correspondence_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "data_typing_intro_MerkleTree.Spec.HPad@tok",
"disc_equation_MerkleTree.Spec.HRaw",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Properties.head",
"equation_FStar.Seq.Properties.tail", "equation_FStar.UInt.fits",
"equation_FStar.UInt.max_int", "equation_FStar.UInt.min_int",
"equation_FStar.UInt.size", "equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_right", "equation_MerkleTree.Spec.rpmt",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Poly1305.size_key",
"equation_with_fuel_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"equation_with_fuel_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"l_and-interp", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.Seq.Properties.slice_slice",
"lemma_Lib.IntTypes.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_AmpAmp", "primitive_Prims.op_Equality",
"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_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_44b773e7bd23d63db1729dc48dc75643",
"refinement_interpretation_Tm_refine_4a5da65b7b8968b5aec399d91ecaf336",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_62965edeceead4d487e326631269edf4",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_a78e81a34494fa620ef91991a1267b1f",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_fe5bfde21a5cf527c4834d999126bd26",
"true_interp", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_FStar.UInt.fits",
"typing_MerkleTree.Spec.mt_right", "typing_Prims.pow2",
"typing_Spec.Poly1305.size_key",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"a70bdd3f3273d9058e2eb3bc920c499a"
],
[
"MerkleTree.Spec.rpmt_right",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"@fuel_correspondence_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"disc_equation_MerkleTree.Spec.HRaw",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Properties.head",
"equation_FStar.Seq.Properties.tail",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_right", "equation_MerkleTree.Spec.rpmt",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"equation_with_fuel_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"l_and-interp", "lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_eq_refl",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.lemma_tail_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.Seq.Properties.slice_slice",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"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_1ba8fd8bb363097813064c67740b2de5",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_4a5da65b7b8968b5aec399d91ecaf336",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_62965edeceead4d487e326631269edf4",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_b138bd5848d4184f7632587e6e4bcf9f",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"refinement_interpretation_Tm_refine_fe5bfde21a5cf527c4834d999126bd26",
"true_interp", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_MerkleTree.Spec.mt_right",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"3e9a5305235395589fb91b1d50e9baea"
],
[
"MerkleTree.Spec.__proj__Collision__item__mt2",
1,
1,
0,
[
"@query", "proj_equation_MerkleTree.Spec.Collision_mt1",
"projection_inverse_MerkleTree.Spec.Collision_mt1"
],
0,
"1587685ab7392be6ec49517ad98e7638"
],
[
"MerkleTree.Spec.__proj__Collision2__item__rh2",
1,
2,
1,
[
"@query", "proj_equation_MerkleTree.Spec.Collision2_lh1",
"proj_equation_MerkleTree.Spec.Collision2_lh2",
"proj_equation_MerkleTree.Spec.Collision2_rh1",
"projection_inverse_MerkleTree.Spec.Collision2_lh1",
"projection_inverse_MerkleTree.Spec.Collision2_lh2",
"projection_inverse_MerkleTree.Spec.Collision2_rh1"
],
0,
"8af248bcdddc70d87b3242a6eec47c4e"
],
[
"MerkleTree.Spec.rpmt_pad_hashes_0",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"@fuel_correspondence_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"constructor_distinct_MerkleTree.Spec.HPad",
"disc_equation_MerkleTree.Spec.HRaw",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Properties.head",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.rpmt", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"equation_with_fuel_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"l_and-interp", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_62965edeceead4d487e326631269edf4",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"refinement_interpretation_Tm_refine_fe5bfde21a5cf527c4834d999126bd26",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_Prims.pow2",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"13f4ae35e3008da191258d46ef1bbd69"
],
[
"MerkleTree.Spec.rpmt_pad_hashes_index_0",
1,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.rpmt", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"refinement_interpretation_Tm_refine_fe5bfde21a5cf527c4834d999126bd26",
"typing_Prims.pow2"
],
0,
"97dd9344334ffbfdc882e688a9e47579"
],
[
"MerkleTree.Spec.rpmt_pad_hashes_index_0",
2,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"@fuel_correspondence_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"constructor_distinct_MerkleTree.Spec.HPad",
"disc_equation_MerkleTree.Spec.HPad",
"disc_equation_MerkleTree.Spec.HRaw",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Properties.head",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.rpmt", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"equation_with_fuel_MerkleTree.Spec.raw_hashes.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"l_and-interp", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_62965edeceead4d487e326631269edf4",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"refinement_interpretation_Tm_refine_fe5bfde21a5cf527c4834d999126bd26",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_Prims.pow2",
"typing_tok_MerkleTree.Spec.HPad@tok"
],
0,
"4f3984803dadfcfdd816c70d1eb4b209"
],
[
"MerkleTree.Spec.mt_get_root_pad_index_0",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_Prims.pow2"
],
0,
"d506164616fdbf848fdc98d739c769bd"
],
[
"MerkleTree.Spec.mt_get_root_pad_index_0",
2,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.pos",
"refinement_interpretation_Tm_refine_3432b2dbe094a412e293cd4108a8ddd3",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"typing_Prims.pow2"
],
0,
"c56bc9d4d13d356723ea4ca4887a9bec"
],
[
"MerkleTree.Spec.mt_get_root_pad_index_0",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"@fuel_correspondence_MerkleTree.Spec.mt_get_root.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.mt_get_root.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_0d7a6896029700a85fe0c3d10ba2ae3d_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "bool_inversion",
"bool_typing", "constructor_distinct_MerkleTree.Spec.HPad",
"constructor_distinct_MerkleTree.Spec.HRaw",
"constructor_distinct_Tm_unit", "disc_equation_MerkleTree.Spec.HPad",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Properties.cons",
"equation_MerkleTree.Spec.hash2",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_next_lv", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"equation_with_fuel_MerkleTree.Spec.mt_get_root.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_index_app1",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"refinement_interpretation_Tm_refine_1bf5eca9600b9497f280acb06109e29b",
"refinement_interpretation_Tm_refine_2df74817c65a36b1b7800cc93eecfaaa",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"token_correspondence_MerkleTree.Spec.hs_next_lv.fuel_instrumented",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_MerkleTree.Spec.hash2", "typing_MerkleTree.Spec.mt_get_root",
"typing_MerkleTree.Spec.uu___is_HPad", "typing_Prims.pow2",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"da6007293b8042dd8c75a4c766187547"
],
[
"MerkleTree.Spec.rpmt_get_root_pad_hashes",
1,
2,
1,
[ "@query" ],
0,
"facf1517cd6dbe1b59e32ffae410876b"
],
[
"MerkleTree.Spec.rpmt_get_root_pad",
1,
2,
1,
[ "@query" ],
0,
"d2baf37213e691f284a82ec0c845302e"
],
[
"MerkleTree.Spec.rpmt_get_root_raw",
1,
2,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.mt_get_root.fuel_instrumented",
"@query", "disc_equation_MerkleTree.Spec.HPad",
"disc_equation_MerkleTree.Spec.HRaw",
"equation_MerkleTree.Spec.rpmt", "equation_Prims.nat",
"fuel_guarded_inversion_MerkleTree.Spec.hash", "int_inversion",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_62965edeceead4d487e326631269edf4",
"refinement_interpretation_Tm_refine_fe5bfde21a5cf527c4834d999126bd26",
"typing_MerkleTree.Spec.mt_get_root"
],
0,
"ca314b6645a065051938db9ed74a52f3"
],
[
"MerkleTree.Spec.extract",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.Spec.mt_get_root.fuel_instrumented",
"@fuel_correspondence_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"MerkleTree.Spec_pretyping_ecd3b9e5340b1979e8fd7a847e58cd73",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_3f3e2f87dc0a13852db02e3e849ea666_1",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_0", "bool_inversion",
"constructor_distinct_MerkleTree.Spec.HPad",
"disc_equation_MerkleTree.Spec.HPad",
"disc_equation_MerkleTree.Spec.HRaw", "eq2-interp",
"equality_tok_MerkleTree.Spec.HPad@tok",
"equation_FStar.Seq.Base.op_At_Bar",
"equation_MerkleTree.Spec.hash2",
"equation_MerkleTree.Spec.hash2_raw",
"equation_MerkleTree.Spec.hash_raw",
"equation_MerkleTree.Spec.hash_seq",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_left",
"equation_MerkleTree.Spec.mt_right", "equation_MerkleTree.Spec.rpmt",
"equation_MerkleTree.Spec.rpmt_left",
"equation_MerkleTree.Spec.rpmt_right", "equation_Prims.l_not",
"equation_Prims.logical", "equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_MerkleTree.Spec.mt_get_root.fuel_instrumented",
"equation_with_fuel_MerkleTree.Spec.pad_hashes.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_MerkleTree.Spec.hash_raw",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "kinding_MerkleTree.Spec.hash@tok",
"l_not-interp", "lemma_FStar.Seq.Base.lemma_eq_elim",
"lemma_FStar.Seq.Base.lemma_eq_intro",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_length",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_BarBar",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Multiply", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_MerkleTree.Spec.HRaw_hr",
"refinement_interpretation_Tm_refine_2c7ecebd8a41d0890aab4251b61d6458",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_814624efcb3b6884bea7fec1215a7044",
"refinement_interpretation_Tm_refine_a970a7bb9adaf2032bbaef5941d92541",
"refinement_interpretation_Tm_refine_b34704ce9941b10cc043bcd0d26b585e",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_e18ab4a50c2390ee0bac8f9f64c08311",
"refinement_interpretation_Tm_refine_fe5bfde21a5cf527c4834d999126bd26",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.op_At_Bar",
"typing_FStar.StrongExcludedMiddle.strong_excluded_middle",
"typing_MerkleTree.Spec.mt_get_root",
"typing_MerkleTree.Spec.mt_left", "typing_MerkleTree.Spec.mt_right",
"typing_Prims.eq2", "typing_Prims.l_not",
"typing_tok_MerkleTree.Spec.HPad@tok", "well-founded-ordering-on-nat"
],
0,
"5440ca0acb6a10ae1f280a61c816ee23"
]
]
]
Computing file changes ...
