Revision b5e85960e109efb08b9c65a4ab85c9b4ef926419 authored by Jay Bosamiya on 04 June 2019, 18:24:09 UTC, committed by Jay Bosamiya on 04 June 2019, 18:24:09 UTC
1 parent 2a5defc
Spec.Loops.fst.hints
[
"�,�bQb��/ (��8�",
[
[
"Spec.Loops.seq_map",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"f864eeb4d9da2edfab872f8313c58001"
],
[
"Spec.Loops.seq_map",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"fa8ce84438f63625270486e9e5f3445c"
],
[
"Spec.Loops.seq_map",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_b1c102bc33763b5f709e32a86e66e509_5",
"binder_x_fe28d8bcde588226b4e538b35321de05_2",
"binder_x_fe28d8bcde588226b4e538b35321de05_3",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.cons",
"equation_FStar.Seq.Properties.head",
"equation_FStar.Seq.Properties.tail", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing", "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_Equality",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_7eb35313f5968be47f3ac748f31513a5",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"well-founded-ordering-on-nat"
],
0,
"68b57f75e42cdc39d08eada19ed7ac84"
],
[
"Spec.Loops.seq_map2",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_16da5dd636ef303f4b4402f063fe1ef3",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f"
],
0,
"9a69dd78a60915de8262e50a692df007"
],
[
"Spec.Loops.seq_map2",
2,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.eqtype", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_c0f4bc4da515d45449a577a9f159288e"
],
0,
"c0c01736072ec437fcdf3ee1bf80ca20"
],
[
"Spec.Loops.seq_map2",
3,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_47e4abf01510896a8bb55a562b825fad_7",
"binder_x_bb8275b22c53d0aea56f4be775119f23_8",
"binder_x_fe28d8bcde588226b4e538b35321de05_3",
"binder_x_fe28d8bcde588226b4e538b35321de05_4",
"binder_x_fe28d8bcde588226b4e538b35321de05_5",
"equality_tok_Prims.LexTop@tok",
"equation_FStar.Seq.Properties.cons",
"equation_FStar.Seq.Properties.head",
"equation_FStar.Seq.Properties.tail", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing", "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_Equality",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_03127b5d59ee3055620018693b4264e8",
"refinement_interpretation_Tm_refine_13a07fb1cde7ffdfc00b5d05f14b9231",
"refinement_interpretation_Tm_refine_3321cbe2f573e3c988fd0895bf1f0cf9",
"refinement_interpretation_Tm_refine_36f208f2b1019ab7b5d9be73f4c89349",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_559c261b1c3777929ea329abfe70ab33",
"refinement_interpretation_Tm_refine_8918b2bc6e465d437bb39793b6ca9a8b",
"refinement_interpretation_Tm_refine_aebc5aa9049e78f605051015a3436e68",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"typing_FStar.Seq.Base.create", "typing_FStar.Seq.Base.length",
"well-founded-ordering-on-nat"
],
0,
"24101915dca0f377577ac7a3c937d3b7"
],
[
"Spec.Loops.repeat",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_e22ba7a032a73f6d0678d3d186686631_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Equality",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"well-founded-ordering-on-nat"
],
0,
"cf90d10462f5f59d599d5376ea67efb5"
],
[
"Spec.Loops.repeat_induction",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"35080bc24b9e48742b810ea9398f106f"
],
[
"Spec.Loops.repeat_induction",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query", "equation_Prims.nat",
"primitive_Prims.op_Subtraction", "projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b"
],
0,
"fc04db5001844a7647760a92173565a9"
],
[
"Spec.Loops.repeat_induction",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.Loops.repeat.fuel_instrumented",
"@fuel_irrelevance_Spec.Loops.repeat.fuel_instrumented", "@query",
"Prims_interpretation_Tm_arrow_f82c3fb9ac6610efb97620a59b378092",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Spec.Loops_interpretation_Tm_arrow_8c8934e3a7b15f7be1355c13a19da978",
"binder_x_c922332b908e83ec0f65ad526f2301b0_2",
"binder_x_e09860b75d8922ab497a3e5bc9347578_4",
"binder_x_fdaebe99fa97539a8a4800ef6e7c601d_3",
"binder_x_fe28d8bcde588226b4e538b35321de05_1", "equation_Prims.nat",
"equation_with_fuel_Spec.Loops.repeat.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Equality",
"primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_f048236b5f8051f83b495ea5eaa6127b",
"typing_Spec.Loops.repeat", "well-founded-ordering-on-nat"
],
0,
"507c30841e1dd725ffd784e8eb821e30"
],
[
"Spec.Loops.repeat_base",
1,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.Loops.repeat.fuel_instrumented", "@query",
"Prims_interpretation_Tm_arrow_f82c3fb9ac6610efb97620a59b378092",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Spec.Loops_interpretation_Tm_arrow_8c8934e3a7b15f7be1355c13a19da978",
"binder_x_e09860b75d8922ab497a3e5bc9347578_4",
"binder_x_fc697b78a0c828f4048fddb2afa0b488_2",
"binder_x_fdaebe99fa97539a8a4800ef6e7c601d_3",
"binder_x_fe28d8bcde588226b4e538b35321de05_1", "equation_Prims.nat",
"equation_with_fuel_Spec.Loops.repeat.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"primitive_Prims.op_Equality",
"refinement_interpretation_Tm_refine_13822e8d415cca32657fdd044ba9fbfb"
],
0,
"80ee85e1e683c5841f0100d0231dfbf8"
],
[
"Spec.Loops.repeat_range",
1,
0,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"binder_x_87b0233b076df7813353d7b4874cca47_3",
"binder_x_e22ba7a032a73f6d0678d3d186686631_2",
"equality_tok_Prims.LexTop@tok", "equation_Prims.eqtype",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"function_token_typing_Prims.int",
"haseqTm_refine_ba523126f67e00e7cd55f0b92f16681d", "int_inversion",
"int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_89cd9b8a599e5c52602994792409ef80",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"well-founded-ordering-on-nat"
],
0,
"25db2f12143fe038382164468c839d2d"
],
[
"Spec.Loops.repeat_range_base",
1,
1,
1,
[ "@query" ],
0,
"421025bed6e468165e4122f991d4894e"
],
[
"Spec.Loops.repeat_range_base",
2,
1,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.Loops.repeat_range.fuel_instrumented",
"@query", "equation_Prims.nat",
"equation_with_fuel_Spec.Loops.repeat_range.fuel_instrumented",
"int_inversion", "primitive_Prims.op_Equality",
"refinement_interpretation_Tm_refine_5d68b4aedab07e9543c96792e76744c9",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"91f031a230c3c2c7ec4560abf2c85e5d"
],
[
"Spec.Loops.repeat_range_induction",
1,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_85e9bb54d06cdc6388e1f9b9ed33ad11",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"6365fdd700a96f9dde06c21d68163c9a"
],
[
"Spec.Loops.repeat_range_induction",
2,
2,
1,
[
"@MaxIFuel_assumption", "@query",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"equation_Prims.nat",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_85e9bb54d06cdc6388e1f9b9ed33ad11",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d"
],
0,
"576ee0a1e1b272234c265690ae27e449"
],
[
"Spec.Loops.repeat_range_induction",
3,
2,
1,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Spec.Loops.repeat_range.fuel_instrumented",
"@fuel_irrelevance_Spec.Loops.repeat_range.fuel_instrumented",
"@query", "Prims_pretyping_ae567c2fb75be05905677af440075565",
"Spec.Loops_interpretation_Tm_arrow_4141e6858c055a47126e62563c8ecb9c",
"Spec.Loops_interpretation_Tm_arrow_98fde83ce818818ff1faa8a640d3828e",
"binder_x_1e0f8672a4975ce7d2cc30a0ee1aac4e_4",
"binder_x_b6d6358812bcbffc794863c1d43a0a72_3",
"binder_x_e09860b75d8922ab497a3e5bc9347578_5",
"binder_x_e22ba7a032a73f6d0678d3d186686631_2",
"binder_x_fe28d8bcde588226b4e538b35321de05_1",
"equality_tok_Prims.LexTop@tok", "equation_Prims.nat",
"equation_with_fuel_Spec.Loops.repeat_range.fuel_instrumented",
"function_token_typing_Prims.__cache_version_number__",
"int_inversion", "int_typing", "primitive_Prims.op_Addition",
"primitive_Prims.op_Equality", "primitive_Prims.op_Subtraction",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_5514fbe9e08dfda40f950a7b9f1b2b98",
"refinement_interpretation_Tm_refine_5d68b4aedab07e9543c96792e76744c9",
"refinement_interpretation_Tm_refine_8a5c487710ddd5afb20bad277b9090cf",
"refinement_interpretation_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
"refinement_interpretation_Tm_refine_bfcfd9addb1bdb729b6b744fb84dc05e",
"typing_Spec.Loops.repeat_range", "well-founded-ordering-on-nat"
],
0,
"a64a3597a3447ac3c768a4bbf5316684"
]
]
]
Computing file changes ...
