Revision cef6a8e821f55e71b791555d22b45bd3debc2596 authored by Jonathan Protzenko on 08 May 2020, 16:26:29 UTC, committed by GitHub on 08 May 2020, 16:26:29 UTC
OCaml API: Don't run unit tests which require unsupported features
MerkleTree.New.High.Correct.Path.fst.hints
[
"�x8b\u0019��:ey�\u001e�[��",
[
[
"MerkleTree.New.High.Correct.Path.path_spec",
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,
"7704b9512e3bc0dc230d776c942b8cee"
],
[
"MerkleTree.New.High.Correct.Path.path_spec",
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,
"1e89a41986cb74b5c883d871d333990b"
],
[
"MerkleTree.New.High.Correct.Path.path_spec",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_4694e496d4f0b8a432e24108d6cde66d_4",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_1",
"binder_x_ef3cff77d20be12dde95f0777a90f70e_2",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
"binder_x_f537159ed795b314b4e58c260361ae86_3", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"data_typing_intro_MerkleTree.Spec.HPad@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.cons",
"equation_FStar.Seq.Properties.tail",
"equation_Lib.IntTypes.unsigned",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.mt_path_length_step",
"equation_MerkleTree.New.High.path", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.padded_hash@tok",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Spec.Curve25519.Lemmas.lemma_div_n",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
"refinement_interpretation_Tm_refine_16e0de92007fd732dd390f31c7906c96",
"refinement_interpretation_Tm_refine_2eb00ca989f9ebed0ed65e52a78766e7",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_802a213e14f3196e6cb3186c5be1c692",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_bcc68ef3c23a422595f4b1d1a0a4a63d",
"token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"token_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_MerkleTree.New.High.hash",
"typing_MerkleTree.New.High.mt_path_length_step",
"well-founded-ordering-on-nat"
],
0,
"06d1f67756a22561d9af46ef06c2fd31"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_step_acc",
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,
"407762a53b58c348d29604dc0b572efd"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_step_acc",
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,
"f03baeae5c7a7234e4d3f184554f9273"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_step_acc",
3,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_Lib.IntTypes.unsigned", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_Modulus", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001"
],
0,
"ceeac938f042b0a68a145fd3fb206ecc"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_acc",
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",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d"
],
0,
"f209f6f3cfd4bbef88c573a542f5ccac"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_acc",
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",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d"
],
0,
"4a676a2f049868f57f647bdb3114dfc4"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_acc",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_53091569903cae77b4a60be8a17a11bc_4",
"binder_x_aabbf0a5d49093a6b07e3e5a24007535_3",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_c45ff54d3bb65363264cc96500ac56d5_5",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
"binder_x_f537159ed795b314b4e58c260361ae86_6", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Lib.IntTypes.U32",
"disc_equation_FStar.Pervasives.Native.Some", "eq2-interp",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.cons",
"equation_FStar.Seq.Properties.tail",
"equation_Lib.IntTypes.unsigned",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.Correct.Path.mt_get_path_step_acc",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.hashes",
"equation_MerkleTree.New.High.hashess",
"equation_MerkleTree.New.High.mt_path_length_step",
"equation_MerkleTree.New.High.path", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_Spec.Curve25519.Lemmas.lemma_div_n",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "primitive_Prims.op_Division",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual", "primitive_Prims.op_Modulus",
"primitive_Prims.op_Negation", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
"refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_65f0e5a3659a158ecfdb56e4d760ae69",
"refinement_interpretation_Tm_refine_6ed5d13caf4284d700420292b4831cbf",
"refinement_interpretation_Tm_refine_7381b22713068fe22fae5f1ab9c6c30a",
"refinement_interpretation_Tm_refine_765c5038a14ad1a170ebaf2c2e8ec7c8",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"typing_Lib.IntTypes.unsigned",
"typing_MerkleTree.New.High.Correct.Base.log2c",
"typing_MerkleTree.New.High.hash",
"typing_MerkleTree.New.High.hashes",
"typing_MerkleTree.New.High.mt_path_length",
"typing_tok_Lib.IntTypes.U32@tok", "well-founded-ordering-on-nat"
],
0,
"658d83e68ba921e90ece14e2bb1cc74b"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_step_acc_consistent",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"b2t_def", "bool_inversion",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some", "eq2-interp",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.hash", "equation_Prims.nat",
"equation_Prims.pos", "equation_Prims.squash",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "l_and-interp",
"lemma_FStar.Pervasives.invertOption", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction", "primitive_Prims.op_disEquality",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_0b724b6f6a7953a53d5fb02ee8337e6a",
"refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
"refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
"refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
"refinement_interpretation_Tm_refine_4d0ab6134173bbad75f08ef14247f657",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
"refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_MerkleTree.New.High.Correct.Base.log2",
"typing_MerkleTree.New.High.hash"
],
0,
"7c97fb48cba2372eb9334cd08c4b45b9"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_step_acc_consistent",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
],
0,
"907864f54b7feff86ee25c6f3848a369"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_step_acc_consistent",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Lib.IntTypes.U32",
"data_elim_FStar.Pervasives.Native.Some", "eq2-interp",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equation_FStar.Seq.Properties.cons",
"equation_FStar.Seq.Properties.head",
"equation_FStar.Seq.Properties.snoc",
"equation_FStar.Seq.Properties.tail",
"equation_MerkleTree.New.High.Correct.Path.mt_get_path_step_acc",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.hashes",
"equation_MerkleTree.New.High.hashess",
"equation_MerkleTree.New.High.mt_make_path_step",
"equation_MerkleTree.New.High.offset_of",
"equation_MerkleTree.New.High.path",
"equation_MerkleTree.New.High.path_insert", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "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_app1",
"lemma_FStar.Seq.Base.lemma_index_app2",
"lemma_FStar.Seq.Base.lemma_index_create",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.UInt.pow2_values",
"lemma_MerkleTree.New.High.Correct.Base.merge_hs_index",
"lemma_MerkleTree.New.High.Correct.Base.seq_head_cons",
"lemma_MerkleTree.New.High.Correct.Base.seq_tail_cons",
"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",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_0b724b6f6a7953a53d5fb02ee8337e6a",
"refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
"refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
"refinement_interpretation_Tm_refine_22125f28c20990597c03dac8bb18819e",
"refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
"refinement_interpretation_Tm_refine_4d0ab6134173bbad75f08ef14247f657",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
"refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_85b48fc854200a815ea472c3088d071c",
"refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
"refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_FStar.Seq.Properties.cons",
"typing_FStar.Seq.Properties.tail",
"typing_MerkleTree.New.High.Correct.Base.merge_hs",
"typing_MerkleTree.New.High.Correct.Path.mt_get_path_step_acc",
"typing_MerkleTree.New.High.hash",
"typing_MerkleTree.New.High.hashes",
"typing_MerkleTree.New.High.mt_make_path_step",
"typing_MerkleTree.New.High.offset_of"
],
0,
"115f6cd9903a377e0a3849b1069d558e"
],
[
"MerkleTree.New.High.Correct.Path.seq_cons_append",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Properties.cons",
"equation_FStar.Seq.Properties.tail", "equation_Prims.nat",
"int_inversion", "int_typing",
"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_len_append",
"lemma_MerkleTree.New.High.Correct.Base.seq_tail_cons",
"primitive_Prims.op_Addition", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Properties.cons",
"typing_FStar.Seq.Properties.tail"
],
0,
"96071fc6215b6a84e7dd4bfd20f7158f"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_acc_consistent",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.hashes",
"equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_06cb130490423446d04fd8da416162f0",
"refinement_interpretation_Tm_refine_0b724b6f6a7953a53d5fb02ee8337e6a",
"refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
"refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
"refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
"refinement_interpretation_Tm_refine_4d0ab6134173bbad75f08ef14247f657",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
"refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
"typing_MerkleTree.New.High.Correct.Base.log2c",
"typing_MerkleTree.New.High.hash",
"typing_MerkleTree.New.High.hashes"
],
0,
"127c2c13cd533662f7687870d01b03c4"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_acc_consistent",
2,
1,
0,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@query", "equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.hashes",
"equation_MerkleTree.New.High.hashess", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_06cb130490423446d04fd8da416162f0",
"refinement_interpretation_Tm_refine_0b724b6f6a7953a53d5fb02ee8337e6a",
"refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
"refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
"refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
"refinement_interpretation_Tm_refine_4d0ab6134173bbad75f08ef14247f657",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
"refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
"typing_FStar.Seq.Base.length",
"typing_MerkleTree.New.High.Correct.Base.log2c",
"typing_MerkleTree.New.High.hash",
"typing_MerkleTree.New.High.hashes"
],
0,
"9f60d7e021a7d48c5d2f14ce735d990a"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_acc_consistent",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Path.mt_get_path_acc.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Path.mt_get_path_acc.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_50de4ae25ca368b5de4d3ad61f7cc222_7",
"binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
"binder_x_6e1290e37a6b4e437f899d72093932a2_2",
"binder_x_8cf65b3b9d91dec7086970aa4543f287_5",
"binder_x_abefe0b518359a5a388975bd4374c4d4_6",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_3",
"binder_x_cbac39ab364bbcc08dab587ac968871a_4",
"binder_x_eb9d41692cc05f67d5dd938d707342ec_8",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
"binder_x_f537159ed795b314b4e58c260361ae86_9", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"disc_equation_FStar.Pervasives.Native.None",
"disc_equation_FStar.Pervasives.Native.Some", "eq2-interp",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.cons",
"equation_FStar.Seq.Properties.head",
"equation_FStar.Seq.Properties.tail",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.Correct.Path.mt_get_path_step_acc",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.hashes",
"equation_MerkleTree.New.High.hashess",
"equation_MerkleTree.New.High.mt_get_path_step",
"equation_MerkleTree.New.High.mt_path_length_step",
"equation_MerkleTree.New.High.offset_of",
"equation_MerkleTree.New.High.path", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_Spec.Poly1305.size_key",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Path.mt_get_path_acc.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "l_and-interp", "lemma_FStar.Pervasives.invertOption",
"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_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",
"lemma_FStar.Seq.Properties.cons_index_slice",
"lemma_FStar.Seq.Properties.lemma_tail_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.UInt.pow2_values", "lemma_Lib.IntTypes.pow2_2",
"lemma_MerkleTree.New.High.Correct.Base.merge_hs_index",
"lemma_MerkleTree.New.High.Correct.Base.seq_head_cons",
"lemma_MerkleTree.New.High.Correct.Base.seq_tail_cons",
"lemma_Spec.Curve25519.Lemmas.lemma_div_n",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "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_Negation",
"primitive_Prims.op_Subtraction",
"proj_equation_FStar.Pervasives.Native.Some_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Pervasives.Native.Some_a",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_09d2e9ab3b9c121b24316d151747e281",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
"refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
"refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
"refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
"refinement_interpretation_Tm_refine_1d6dbe1d860e2d0c6f1e24584b940fd1",
"refinement_interpretation_Tm_refine_22125f28c20990597c03dac8bb18819e",
"refinement_interpretation_Tm_refine_28c5d1085ead998d554ed5e7448a1214",
"refinement_interpretation_Tm_refine_319130ca780c778653844ecfc44d9c4d",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
"refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
"refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
"refinement_interpretation_Tm_refine_4d5241eb6fe198666a8101195bbd4a2a",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_59122260c77179a912aff4679b32096c",
"refinement_interpretation_Tm_refine_5f58f4254a1acbbedf2f52de0dbf26c1",
"refinement_interpretation_Tm_refine_64745f0bab45b9f63e6c5de7f4e31013",
"refinement_interpretation_Tm_refine_6e9e552283a82d93959794627615c964",
"refinement_interpretation_Tm_refine_6ecc26d260b07cd8c8333ca61d7545ba",
"refinement_interpretation_Tm_refine_7353c91dd3c7081589b77fa669f652e2",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_85b48fc854200a815ea472c3088d071c",
"refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_b138bd5848d4184f7632587e6e4bcf9f",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_bb2cbefb6f9a8a50a7b780a0a53e7963",
"refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
"refinement_interpretation_Tm_refine_c5f0d88a3da0ddeb45db9810df49fce9",
"refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
"refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_d87d99f22d4a7ec1b20cbca92c993502",
"refinement_interpretation_Tm_refine_db1f7a375601e94233b330488ad7e8aa",
"refinement_interpretation_Tm_refine_db34bae21652cb80fc35719f7a96b599",
"refinement_interpretation_Tm_refine_e06b062afb77272156afb40cf54499ea",
"refinement_interpretation_Tm_refine_ec91eb7c63ff09d16d5762b9a6555d2c",
"refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
"refinement_interpretation_Tm_refine_fd00e7b79c3f1d6a6049dbfa5a06447f",
"token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"token_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
"token_correspondence_MerkleTree.New.High.Correct.Path.mt_get_path_acc.fuel_instrumented",
"token_correspondence_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Pervasives.Native.__proj__Some__item__v",
"typing_FStar.Pervasives.Native.uu___is_Some",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_FStar.Seq.Properties.cons",
"typing_FStar.Seq.Properties.head",
"typing_FStar.Seq.Properties.tail",
"typing_MerkleTree.New.High.Correct.Base.log2",
"typing_MerkleTree.New.High.Correct.Base.log2c",
"typing_MerkleTree.New.High.Correct.Path.mt_get_path_acc",
"typing_MerkleTree.New.High.Correct.Path.mt_get_path_step_acc",
"typing_MerkleTree.New.High.hash",
"typing_MerkleTree.New.High.hashes",
"typing_MerkleTree.New.High.mt_get_path_step",
"typing_MerkleTree.New.High.mt_path_length",
"typing_MerkleTree.New.High.mt_path_length_step",
"typing_MerkleTree.New.High.offset_of",
"typing_Spec.Poly1305.size_key", "unit_inversion", "unit_typing",
"well-founded-ordering-on-nat"
],
0,
"a185e12a0d3450cd193582f67223e745"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_acc_consistent",
4,
1,
0,
[
"@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
],
0,
"69873b57098b6debe5dc63979710d488"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_acc_consistent",
5,
1,
0,
[
"@MaxIFuel_assumption", "@query", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91"
],
0,
"7fb3241ff9f608b9f73ce556d68e1a1b"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_acc_inv_ok",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"b2t_def", "bool_inversion", "eq2-interp",
"equation_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.hash_seq",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.squash",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"function_token_typing_MerkleTree.New.High.hash",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"l_and-interp", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_44b773e7bd23d63db1729dc48dc75643",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_54a988a65b957c32817754d209970fdb",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"typing_FStar.Seq.Base.length",
"typing_MerkleTree.New.High.Correct.Base.log2"
],
0,
"feca47fa50f4c2341a7a9088ee86d8bf"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_acc_inv_ok",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"b2t_def", "bool_inversion", "eq2-interp",
"equation_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.hash_seq",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.squash",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"function_token_typing_MerkleTree.New.High.hash",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"l_and-interp", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThan", "projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_3ba8594980e374d5a420c584ba17bd96",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_44b773e7bd23d63db1729dc48dc75643",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_54a988a65b957c32817754d209970fdb",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"typing_FStar.Seq.Base.length",
"typing_MerkleTree.New.High.Correct.Base.log2"
],
0,
"3502e957c26d462853dba93bea8f63ef"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_acc_inv_ok",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_inv_log.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_rhs_inv.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Path.mt_get_path_acc.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Path.path_spec.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@fuel_correspondence_MerkleTree.Spec.mt_get_path.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_inv_log.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.mt_rhs_inv.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Path.mt_get_path_acc.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Path.path_spec.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.mt_get_path.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_0f12bf2603e9091028a82002ad226308_3",
"binder_x_53091569903cae77b4a60be8a17a11bc_4",
"binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
"binder_x_7df3b3ce71ac0f95b834d29aa2f6700f_6",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_c45ff54d3bb65363264cc96500ac56d5_5",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
"binder_x_f537159ed795b314b4e58c260361ae86_7", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_FStar.Pervasives.Native.None",
"constructor_distinct_FStar.Pervasives.Native.Some",
"constructor_distinct_Lib.IntTypes.U32",
"data_elim_FStar.Pervasives.Native.Some",
"data_typing_intro_MerkleTree.Spec.HPad@tok",
"data_typing_intro_MerkleTree.Spec.HRaw@tok",
"disc_equation_FStar.Pervasives.Native.Some", "eq2-interp",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.cons",
"equation_FStar.Seq.Properties.head",
"equation_FStar.Seq.Properties.last",
"equation_FStar.Seq.Properties.lseq",
"equation_FStar.Seq.Properties.tail",
"equation_Lib.IntTypes.unsigned",
"equation_MerkleTree.New.High.Correct.Base.create_pads",
"equation_MerkleTree.New.High.Correct.Base.hash_seq_spec",
"equation_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.Correct.Base.mt_hashes_next_rel",
"equation_MerkleTree.New.High.Correct.Path.mt_get_path_step_acc",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.hashes",
"equation_MerkleTree.New.High.hashess",
"equation_MerkleTree.New.High.mt_path_length_step",
"equation_MerkleTree.New.High.path", "equation_MerkleTree.Spec.hash",
"equation_MerkleTree.Spec.hashes",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.mt_next_lv",
"equation_MerkleTree.Spec.path", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_inv_log.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_rhs_inv.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Path.mt_get_path_acc.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Path.path_spec.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"equation_with_fuel_MerkleTree.Spec.mt_get_path.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"fuel_guarded_inversion_FStar.Pervasives.Native.option",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.padded_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_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_index_upd1",
"lemma_FStar.Seq.Base.lemma_index_upd2",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_FStar.Seq.Properties.slice_is_empty",
"lemma_FStar.UInt.pow2_values",
"lemma_MerkleTree.New.High.Correct.Base.seq_head_cons",
"lemma_MerkleTree.New.High.Correct.Base.seq_tail_cons",
"lemma_Spec.Curve25519.Lemmas.lemma_div_n",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "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_Negation",
"primitive_Prims.op_Subtraction",
"proj_equation_FStar.Pervasives.Native.Some_v",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Some_v",
"refinement_interpretation_Tm_refine_12c34cf24b92bcab4256b0605885d7f9",
"refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
"refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
"refinement_interpretation_Tm_refine_319130ca780c778653844ecfc44d9c4d",
"refinement_interpretation_Tm_refine_33e9e47c0adfd5c76673081bc3b1f7a6",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_3a643af648e0e51f8493b1b7e51bd56c",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_43a51d2a8f887f961c9753eac43d02b7",
"refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_5e78195762268defb161e55a2c76fcbb",
"refinement_interpretation_Tm_refine_65f0e5a3659a158ecfdb56e4d760ae69",
"refinement_interpretation_Tm_refine_765c5038a14ad1a170ebaf2c2e8ec7c8",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_9c9eac66f829c9b567b9174502161d06",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_b361ba8089a6e963921008d537e799a1",
"refinement_interpretation_Tm_refine_baba3c4ff195e8afc82d572a0bec0709",
"refinement_interpretation_Tm_refine_bf21d78812fd4c0308c10c82d85f8788",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_dc0bcc5a4556355001b46ff2d8c6e5a5",
"refinement_interpretation_Tm_refine_df81b3f17797c6f405c1dbb191651292",
"refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
"refinement_interpretation_Tm_refine_e498fb51261db037ef331c43a4bc992d",
"refinement_interpretation_Tm_refine_ec91eb7c63ff09d16d5762b9a6555d2c",
"refinement_interpretation_Tm_refine_f57063d4bd004d8f89276081f45a638c",
"refinement_interpretation_Tm_refine_fd00e7b79c3f1d6a6049dbfa5a06447f",
"token_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
"token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"token_correspondence_MerkleTree.New.High.Correct.Path.mt_get_path_acc.fuel_instrumented",
"token_correspondence_MerkleTree.New.High.Correct.Path.path_spec.fuel_instrumented",
"token_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"token_correspondence_MerkleTree.Spec.mt_get_path.fuel_instrumented",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.index", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.seq", "typing_FStar.Seq.Base.slice",
"typing_FStar.Seq.Base.upd", "typing_FStar.Seq.Properties.cons",
"typing_FStar.Seq.Properties.head",
"typing_FStar.Seq.Properties.tail", "typing_Lib.IntTypes.unsigned",
"typing_MerkleTree.New.High.Correct.Base.create_pads",
"typing_MerkleTree.New.High.Correct.Base.hash_seq_spec",
"typing_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
"typing_MerkleTree.New.High.Correct.Base.log2",
"typing_MerkleTree.New.High.Correct.Base.log2c",
"typing_MerkleTree.New.High.Correct.Path.mt_get_path_acc",
"typing_MerkleTree.New.High.Correct.Path.path_spec",
"typing_MerkleTree.New.High.hash",
"typing_MerkleTree.New.High.mt_path_length",
"typing_MerkleTree.Spec.mt_get_path",
"typing_MerkleTree.Spec.mt_next_lv", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.U32@tok", "unit_inversion", "unit_typing",
"well-founded-ordering-on-nat"
],
0,
"007e81fe353011af74eb51965f91c8d1"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_inv_ok_",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"bool_inversion", "constructor_distinct_FStar.Integers.W16",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32", "eq2-interp",
"equality_tok_FStar.Integers.W16@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equation_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.hashes",
"equation_MerkleTree.New.High.path",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "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",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
"refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
"refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
"refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
"refinement_interpretation_Tm_refine_4c6cdb6946a57f770e07008f14ffd053",
"refinement_interpretation_Tm_refine_4d0ab6134173bbad75f08ef14247f657",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
"refinement_interpretation_Tm_refine_6e9e552283a82d93959794627615c964",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0633907f656a03c50a2b53dc564942",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
"refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
"refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
"refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
"refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
"refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
"typing_FStar.Seq.Base.length",
"typing_MerkleTree.New.High.Correct.Base.log2c",
"typing_MerkleTree.New.High.Correct.Base.merge_hs",
"typing_MerkleTree.New.High.hash"
],
0,
"0fb584a1e88e044cc68b2f081135bc78"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_inv_ok_",
2,
0,
1,
[
"@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_da1b0dfb8283502ec162998a8bbb6431"
],
0,
"25acb0657c6074c8299d24b40a3a4466"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_inv_ok_",
3,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Path.mt_get_path_acc.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@fuel_correspondence_MerkleTree.Spec.mt_get_path.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_inversion",
"data_typing_intro_MerkleTree.Spec.HRaw@tok", "eq2-interp",
"equation_FStar.Seq.Properties.cons",
"equation_FStar.Seq.Properties.head",
"equation_FStar.Seq.Properties.lseq",
"equation_FStar.Seq.Properties.tail",
"equation_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.hashes",
"equation_MerkleTree.New.High.hashess",
"equation_MerkleTree.New.High.path", "equation_MerkleTree.Spec.hash",
"equation_MerkleTree.Spec.hashes",
"equation_MerkleTree.Spec.merkle_tree",
"equation_MerkleTree.Spec.path", "equation_Prims.nat",
"equation_Prims.pos", "equation_Spec.Poly1305.size_key",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_hashes_lth_inv_log.fuel_instrumented",
"equation_with_fuel_Prims.pow2.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"kinding_MerkleTree.Spec.padded_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_refl",
"lemma_FStar.Seq.Base.lemma_index_slice",
"lemma_FStar.Seq.Base.lemma_len_append",
"lemma_FStar.Seq.Base.lemma_len_slice",
"lemma_MerkleTree.New.High.Correct.Base.seq_head_cons",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Division", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan", "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_06cb130490423446d04fd8da416162f0",
"refinement_interpretation_Tm_refine_0ec011aea9f93256a3547ad9f0c667f1",
"refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
"refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
"refinement_interpretation_Tm_refine_1ae2a0d6b2f4da2d4b0194885669f804",
"refinement_interpretation_Tm_refine_319130ca780c778653844ecfc44d9c4d",
"refinement_interpretation_Tm_refine_33e9e47c0adfd5c76673081bc3b1f7a6",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_42ab70f52fa85ce7b7f41db78958e96d",
"refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
"refinement_interpretation_Tm_refine_4c6cdb6946a57f770e07008f14ffd053",
"refinement_interpretation_Tm_refine_4d0ab6134173bbad75f08ef14247f657",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_5664991902867dbaea8455604edd6227",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_6e9e552283a82d93959794627615c964",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0b9b2dbca36eab00de093c1b701c6d",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_baba3c4ff195e8afc82d572a0bec0709",
"refinement_interpretation_Tm_refine_bf3340443d6edf0ae4bc4b37060534fb",
"refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
"refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_da1b0dfb8283502ec162998a8bbb6431",
"refinement_interpretation_Tm_refine_dc0bcc5a4556355001b46ff2d8c6e5a5",
"refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
"refinement_interpretation_Tm_refine_e498fb51261db037ef331c43a4bc992d",
"refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
"refinement_interpretation_Tm_refine_fd00e7b79c3f1d6a6049dbfa5a06447f",
"token_correspondence_MerkleTree.New.High.Correct.Base.hash_seq_lift.fuel_instrumented",
"token_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
"token_correspondence_Prims.pow2.fuel_instrumented",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_FStar.Seq.Properties.head",
"typing_FStar.Seq.Properties.tail",
"typing_MerkleTree.New.High.Correct.Base.hash_seq_lift",
"typing_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
"typing_MerkleTree.New.High.Correct.Base.log2c",
"typing_MerkleTree.New.High.Correct.Path.mt_get_path_acc",
"typing_MerkleTree.New.High.Correct.Path.path_spec",
"typing_MerkleTree.New.High.hash",
"typing_MerkleTree.New.High.hashes",
"typing_MerkleTree.New.High.mt_get_path_",
"typing_MerkleTree.Spec.mt_get_path",
"typing_MerkleTree.Spec.mt_next_lv", "typing_Spec.Poly1305.size_key"
],
0,
"bbb1d5daa1ef5622fa682d2fbbfc187d"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_inv_ok",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"b2t_def", "bool_inversion", "bool_typing",
"constructor_distinct_Lib.IntTypes.U8",
"equation_FStar.Seq.Properties.tail", "equation_Lib.IntTypes.minint",
"equation_Lib.IntTypes.unsigned",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.Correct.Base.mt_base",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.path",
"equation_MerkleTree.Spec.merkle_tree", "equation_Prims.l_and",
"equation_Prims.nat", "equation_Prims.pos", "equation_Prims.squash",
"equation_with_fuel_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"fuel_guarded_inversion_MerkleTree.New.High.merkle_tree",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_len_slice",
"primitive_Prims.op_Addition", "primitive_Prims.op_Equality",
"primitive_Prims.op_GreaterThan", "primitive_Prims.op_LessThan",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_MerkleTree.New.High.MT_i",
"proj_equation_MerkleTree.New.High.MT_j",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_46cf8561fcb87b3a901fbf1a5ed53e3c",
"refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7f59e1d21662a5bb0549ee09247e1710",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_9e2cc9c9dac6b0e7d2a3400258c6016f",
"refinement_interpretation_Tm_refine_aeee1ad2d9f3d1c314aee4e316971702",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_e166b70fde2cd9152c503654048d8315",
"typing_FStar.Seq.Base.length",
"typing_MerkleTree.New.High.Correct.Base.log2",
"typing_MerkleTree.New.High.Correct.Base.log2c",
"typing_MerkleTree.New.High.Correct.Base.mt_base",
"typing_MerkleTree.New.High.hash",
"typing_MerkleTree.New.High.mt_path_length", "typing_Prims.pow2"
],
0,
"af28ed9f1c33fc3053a4846d800689a6"
],
[
"MerkleTree.New.High.Correct.Path.mt_get_path_inv_ok",
2,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.mt_get_path_.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.merge_hs.fuel_instrumented",
"@query",
"FStar.Seq.Base_interpretation_Tm_arrow_1910ef5262f2ee8e712b6609a232b1ea",
"MerkleTree.New.High_pretyping_42b5f1434db9b9fcab9a3482ce626e35",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_typing",
"eq2-interp", "equation_FStar.Seq.Properties.head",
"equation_FStar.Seq.Properties.snoc",
"equation_FStar.Seq.Properties.tail",
"equation_MerkleTree.New.High.Correct.Base.hash_seq_spec_full",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.Correct.Base.mt_base",
"equation_MerkleTree.New.High.Correct.Base.mt_inv",
"equation_MerkleTree.New.High.Correct.Base.mt_olds_hs_inv",
"equation_MerkleTree.New.High.Correct.Base.mt_spec",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.hashes",
"equation_MerkleTree.New.High.hashess",
"equation_MerkleTree.New.High.mt_get_path",
"equation_MerkleTree.New.High.mt_get_root",
"equation_MerkleTree.New.High.mt_wf_elts",
"equation_MerkleTree.New.High.offset_of",
"equation_MerkleTree.New.High.path",
"equation_MerkleTree.New.High.path_insert", "equation_Prims.nat",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.mt_olds_inv.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.hs_wf_elts.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"fuel_guarded_inversion_MerkleTree.New.High.merkle_tree",
"function_token_typing_FStar.Seq.Base.index",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "l_and-interp",
"lemma_FStar.Seq.Base.lemma_create_len",
"lemma_FStar.Seq.Base.lemma_eq_elim",
"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_MerkleTree.New.High.Correct.Base.merge_hs_index",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_Equality", "primitive_Prims.op_GreaterThan",
"primitive_Prims.op_LessThan", "primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_MerkleTree.New.High.MT_hash_fun",
"proj_equation_MerkleTree.New.High.MT_hs",
"proj_equation_MerkleTree.New.High.MT_i",
"proj_equation_MerkleTree.New.High.MT_j",
"proj_equation_MerkleTree.New.High.MT_rhs_ok",
"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_FStar.Pervasives.Native.Mktuple3__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__2",
"projection_inverse_FStar.Pervasives.Native.Mktuple3__3",
"projection_inverse_MerkleTree.New.High.MT_hash_fun",
"projection_inverse_MerkleTree.New.High.MT_rhs_ok",
"refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
"refinement_interpretation_Tm_refine_16113b670c3948241b38ee17f4d8fb91",
"refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
"refinement_interpretation_Tm_refine_22125f28c20990597c03dac8bb18819e",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_46cf8561fcb87b3a901fbf1a5ed53e3c",
"refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_6e9e552283a82d93959794627615c964",
"refinement_interpretation_Tm_refine_7f59e1d21662a5bb0549ee09247e1710",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_881298fb0dff2db17e4149fcf49ad4b9",
"refinement_interpretation_Tm_refine_995516c5fe04fd93611e610195bbf9ba",
"refinement_interpretation_Tm_refine_9b2b3e7ac5f300ddc6add4181948ef22",
"refinement_interpretation_Tm_refine_9e2cc9c9dac6b0e7d2a3400258c6016f",
"refinement_interpretation_Tm_refine_ac201cf927190d39c033967b63cb957b",
"refinement_interpretation_Tm_refine_ad53f3413fd15db5258446e997071714",
"refinement_interpretation_Tm_refine_aeee1ad2d9f3d1c314aee4e316971702",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"refinement_interpretation_Tm_refine_cc7ec1228e62f637b46417d43aae0cfa",
"refinement_interpretation_Tm_refine_d022e51698263de0859911b2eaa8436b",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_d83f8da8ef6c1cb9f71d1465c1bb1c55",
"refinement_interpretation_Tm_refine_f5dcb5f7d87461830fead189c46dd01b",
"typing_FStar.Seq.Base.append", "typing_FStar.Seq.Base.create",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.index",
"typing_FStar.Seq.Base.length", "typing_FStar.Seq.Base.slice",
"typing_FStar.Seq.Properties.head",
"typing_FStar.Seq.Properties.snoc",
"typing_MerkleTree.New.High.Correct.Base.log2",
"typing_MerkleTree.New.High.Correct.Base.log2c",
"typing_MerkleTree.New.High.__proj__MT__item__hash_fun",
"typing_MerkleTree.New.High.__proj__MT__item__hs",
"typing_MerkleTree.New.High.__proj__MT__item__i",
"typing_MerkleTree.New.High.__proj__MT__item__j",
"typing_MerkleTree.New.High.__proj__MT__item__rhs",
"typing_MerkleTree.New.High.hash",
"typing_MerkleTree.New.High.hashes",
"typing_MerkleTree.New.High.mt_get_path_",
"typing_MerkleTree.New.High.mt_path_length"
],
0,
"66e0e95048b088319b0dd006b47ece87"
],
[
"MerkleTree.New.High.Correct.Path.mt_verify_ok_",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "b2t_def",
"bool_inversion", "bool_typing",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.path", "equation_Prims.nat",
"equation_Prims.pos", "equation_Prims.squash",
"equation_with_fuel_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "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_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0633907f656a03c50a2b53dc564942",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_dc0bcc5a4556355001b46ff2d8c6e5a5",
"token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"typing_FStar.Seq.Base.length", "typing_MerkleTree.New.High.hash",
"typing_MerkleTree.New.High.mt_path_length", "typing_Prims.pow2"
],
0,
"0b5290334eb66c804fce4a5c8377802e"
],
[
"MerkleTree.New.High.Correct.Path.mt_verify_ok_",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"b2t_def", "bool_inversion", "bool_typing",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.path", "equation_Prims.nat",
"equation_Prims.pos", "equation_Prims.squash",
"equation_with_fuel_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "lemma_FStar.Seq.Base.lemma_len_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_13d357a23a5e1099db9eb784ff83d223",
"refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_7e0633907f656a03c50a2b53dc564942",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_dc0bcc5a4556355001b46ff2d8c6e5a5",
"refinement_interpretation_Tm_refine_e2454d5f07d9788fccb82064eeda3336",
"token_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"typing_MerkleTree.New.High.hash",
"typing_MerkleTree.New.High.mt_path_length", "typing_Prims.pow2"
],
0,
"105527207b1cdbb89a72935ac8b9862c"
],
[
"MerkleTree.New.High.Correct.Path.mt_verify_ok_",
3,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.Correct.Path.path_spec.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.mt_verify_.fuel_instrumented",
"@fuel_correspondence_MerkleTree.Spec.mt_verify_.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.Correct.Path.path_spec.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.New.High.mt_verify_.fuel_instrumented",
"@fuel_irrelevance_MerkleTree.Spec.mt_verify_.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_3ecda020b5cf79d02cc346b352c50370_3",
"binder_x_5e20d151293c9e40e5203cbcff29aebe_1",
"binder_x_7df3b3ce71ac0f95b834d29aa2f6700f_6",
"binder_x_abda421e48b5c84421ca729d856d67d6_4",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_2",
"binder_x_bb4e1c9af0265270f8e7a5f250f730e2_5",
"binder_x_f26957a7e62b271a8736230b1e9c83c1_0",
"binder_x_f537159ed795b314b4e58c260361ae86_7", "bool_inversion",
"bool_typing", "constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"constructor_distinct_MerkleTree.Spec.HPad",
"constructor_distinct_MerkleTree.Spec.HRaw",
"data_typing_intro_MerkleTree.Spec.HPad@tok",
"data_typing_intro_MerkleTree.Spec.HRaw@tok",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U32@tok", "equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.head",
"equation_FStar.Seq.Properties.lseq",
"equation_FStar.Seq.Properties.tail",
"equation_Lib.IntTypes.unsigned",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.mt_path_length_step",
"equation_MerkleTree.New.High.path", "equation_MerkleTree.Spec.hash",
"equation_MerkleTree.Spec.padded_hash_fun",
"equation_MerkleTree.Spec.path", "equation_Prims.eqtype",
"equation_Prims.nat", "equation_Prims.pos",
"equation_with_fuel_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.Correct.Path.path_spec.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"equation_with_fuel_MerkleTree.New.High.mt_verify_.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__",
"function_token_typing_Prims.int",
"haseqTm_refine_542f9d4f129664613f2483a6c88bc7c2", "int_inversion",
"int_typing", "kinding_MerkleTree.Spec.padded_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.lemma_tail_slice",
"lemma_MerkleTree.New.High.Correct.Base.seq_head_cons",
"lemma_MerkleTree.New.High.Correct.Base.seq_tail_cons",
"lemma_Spec.Curve25519.Lemmas.lemma_div_n",
"primitive_Prims.op_Addition", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_BarBar", "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",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__1",
"projection_inverse_FStar.Pervasives.Native.Mktuple2__2",
"projection_inverse_MerkleTree.Spec.HPad_hsz",
"projection_inverse_MerkleTree.Spec.HRaw_hr",
"projection_inverse_MerkleTree.Spec.HRaw_hsz",
"refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
"refinement_interpretation_Tm_refine_167ef714932ec832fb671890fc3eee6c",
"refinement_interpretation_Tm_refine_35a0739c434508f48d0bb1d5cd5df9e8",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_47cf8b23e97a3343bc4955e0c7b0c92e",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_a2f9d31ec17fd3a91ac07742b87883aa",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_b138bd5848d4184f7632587e6e4bcf9f",
"refinement_interpretation_Tm_refine_b3090649248199ce2a2d6d6d928cff94",
"refinement_interpretation_Tm_refine_b913a3f691ca99086652e0a655e72f17",
"refinement_interpretation_Tm_refine_baba3c4ff195e8afc82d572a0bec0709",
"refinement_interpretation_Tm_refine_c87079f0f4657a4d82ef934509727b17",
"refinement_interpretation_Tm_refine_d3d07693cd71377864ef84dc97d10ec1",
"refinement_interpretation_Tm_refine_dc0bcc5a4556355001b46ff2d8c6e5a5",
"refinement_interpretation_Tm_refine_dc48f78fca6f8433edb3d5a9ad647892",
"refinement_interpretation_Tm_refine_fd00e7b79c3f1d6a6049dbfa5a06447f",
"token_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"typing_FStar.Seq.Base.empty", "typing_FStar.Seq.Base.length",
"typing_FStar.Seq.Base.slice", "typing_FStar.Seq.Properties.head",
"typing_FStar.Seq.Properties.tail", "typing_Lib.IntTypes.unsigned",
"typing_MerkleTree.New.High.Correct.Base.log2",
"typing_MerkleTree.New.High.Correct.Base.log2c",
"typing_MerkleTree.New.High.Correct.Path.path_spec",
"typing_MerkleTree.New.High.hash",
"typing_MerkleTree.New.High.mt_path_length",
"typing_MerkleTree.New.High.mt_path_length_step",
"typing_MerkleTree.New.High.mt_verify_", "typing_Prims.pow2",
"typing_tok_Lib.IntTypes.U32@tok", "unit_inversion", "unit_typing",
"well-founded-ordering-on-nat"
],
0,
"95c1a94fea3c3646aba37a67e47db31d"
],
[
"MerkleTree.New.High.Correct.Path.mt_verify_ok",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.Correct.Base.log2.fuel_instrumented",
"@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@fuel_correspondence_Prims.pow2.fuel_instrumented", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565", "bool_typing",
"constructor_distinct_FStar.Integers.W31",
"constructor_distinct_FStar.Integers.W8",
"constructor_distinct_Lib.IntTypes.U32",
"equality_tok_FStar.Integers.W31@tok",
"equality_tok_FStar.Integers.W8@tok",
"equality_tok_Lib.IntTypes.U32@tok",
"equation_FStar.Seq.Properties.tail",
"equation_Lib.IntTypes.unsigned",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.path", "equation_Prims.nat",
"equation_Prims.pos",
"equation_with_fuel_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing",
"lemma_FStar.Seq.Base.lemma_len_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",
"projection_inverse_FStar.Integers.Signed__0",
"projection_inverse_FStar.Integers.Unsigned__0",
"refinement_interpretation_Tm_refine_13d357a23a5e1099db9eb784ff83d223",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_81407705a0828c2c1b1976675443f647",
"refinement_interpretation_Tm_refine_8233d76b57e95451540fc312b717fa79",
"refinement_interpretation_Tm_refine_87faf900dfa0d2b4c1716c6e280af26b",
"refinement_interpretation_Tm_refine_afd51579b90d50ea23e03b743a1fa001",
"refinement_interpretation_Tm_refine_dc0bcc5a4556355001b46ff2d8c6e5a5",
"typing_FStar.Seq.Base.length",
"typing_MerkleTree.New.High.Correct.Base.log2",
"typing_MerkleTree.New.High.hash",
"typing_MerkleTree.New.High.mt_path_length", "typing_Prims.pow2"
],
0,
"0c1f8949653d60a8514b4cfa70ad0695"
],
[
"MerkleTree.New.High.Correct.Path.mt_verify_ok",
2,
2,
1,
[ "@query" ],
0,
"9df4ce8732b9ca1d084df45ba8a1b40f"
],
[
"MerkleTree.New.High.Correct.Path.mt_verify_ok",
3,
2,
1,
[
"@MaxIFuel_assumption",
"@fuel_correspondence_MerkleTree.New.High.mt_path_length.fuel_instrumented",
"@query", "bool_typing", "eq2-interp",
"equation_FStar.Seq.Properties.head",
"equation_FStar.Seq.Properties.tail",
"equation_MerkleTree.New.High.Correct.Base.log2c",
"equation_MerkleTree.New.High.hash",
"equation_MerkleTree.New.High.mt_verify",
"equation_MerkleTree.Spec.mt_verify", "equation_Prims.nat",
"equation_Prims.pos", "int_inversion", "primitive_Prims.op_Addition",
"projection_inverse_BoxInt_proj_0",
"projection_inverse_MerkleTree.Spec.HRaw_hr",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_571d9f74016be5357787170b42ecf913",
"refinement_interpretation_Tm_refine_774ba3f728d91ead8ef40be66c9802e5",
"refinement_interpretation_Tm_refine_8233d76b57e95451540fc312b717fa79",
"refinement_interpretation_Tm_refine_87faf900dfa0d2b4c1716c6e280af26b",
"typing_MerkleTree.New.High.mt_path_length"
],
0,
"c263969d7025e8fbda192d3ead890319"
]
]
]
Computing file changes ...
