Revision 9a1c35986c9ec0d91b29ce0fcc77700ae032310a authored by Aseem Rastogi on 01 April 2021, 08:46:33 UTC, committed by Aseem Rastogi on 01 April 2021, 08:46:33 UTC
1 parent 122750f
Vale.Interop.fsti.hints
[
"��g��\u0002\u0015y\u0019�����d=",
[
[
"Vale.Interop.same_unspecified_down",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"refinement_interpretation_Tm_refine_011c19c35e55781ddb5bbdc0d9eead95"
],
0,
"d46dc4ce5d696579f556327b1056afd2"
],
[
"Vale.Interop.get_seq_heap",
1,
1,
0,
[
"@MaxFuel_assumption", "@MaxIFuel_assumption",
"@fuel_correspondence_Prims.pow2.fuel_instrumented",
"@fuel_irrelevance_Prims.pow2.fuel_instrumented", "@query",
"FStar.Seq.Base_interpretation_Tm_arrow_44bb45ed5c2534b346e0f58ea5033251",
"Prims_pretyping_ae567c2fb75be05905677af440075565",
"Vale.Interop_interpretation_Tm_arrow_26ff148c0f90a45f463a84c61946fd2d",
"b2t_def", "equation_FStar.UInt.fits", "equation_FStar.UInt.max_int",
"equation_FStar.UInt.min_int", "equation_FStar.UInt.size",
"equation_Prims.eqtype", "equation_Prims.nat",
"equation_Vale.Def.Words_s.nat8",
"equation_Vale.Interop.Types.base_typ_as_type",
"equation_Vale.Interop.Types.down_view",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_Vale.Interop.Types.b8", "int_typing",
"lemma_FStar.Seq.Base.lemma_init_len",
"lemma_FStar.UInt.pow2_values", "primitive_Prims.op_AmpAmp",
"primitive_Prims.op_LessThanOrEqual",
"primitive_Prims.op_Subtraction",
"proj_equation_Vale.Interop.Types.Buffer_src",
"projection_inverse_BoxBool_proj_0",
"projection_inverse_BoxInt_proj_0",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
"refinement_interpretation_Tm_refine_9bdf64b2660adb592eaffa73ced680cc",
"refinement_interpretation_Tm_refine_c1424615841f28cac7fc34e92b7ff33c",
"typing_FStar.UInt8.t",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.down_view"
],
0,
"d897d2dec837be98a16843d91c887ccd"
],
[
"Vale.Interop.up_mem",
1,
1,
0,
[ "@query" ],
0,
"ab056d6bd24f1b63495fd95f53f09699"
],
[
"Vale.Interop.down_up_identity",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"Vale.Interop.Heap_s_interpretation_Tm_ghost_arrow_918a6217dad728349cf023555f8761c0",
"equation_Vale.Interop.Heap_s.correct_down",
"equation_Vale.Interop.Heap_s.down_mem_t",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"refinement_interpretation_Tm_refine_b50f45fba9bc6f60eec05ca9dc1f94ef",
"typing_Vale.Interop.down_mem"
],
0,
"e58e8218ad8efbfb60f4479846c0184a"
],
[
"Vale.Interop.up_down_identity",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"refinement_interpretation_Tm_refine_3a2dd58f50cd5923bb942c80f67255f6"
],
0,
"ff2a519fe693569e9e335ccf74232cda"
],
[
"Vale.Interop.update_buffer_up_mem",
1,
1,
0,
[
"@MaxIFuel_assumption", "@query",
"equation_FStar.Seq.Properties.lseq",
"equation_LowStar.BufferView.Down.buffer", "equation_Prims.eqtype",
"equation_Vale.Arch.MachineHeap_s.machine_heap",
"equation_Vale.Def.Words_s.nat8",
"equation_Vale.Interop.Heap_s.correct_down",
"equation_Vale.Interop.Types.down_view",
"equation_Vale.Interop.Types.get_downview",
"fuel_guarded_inversion_FStar.Pervasives.dtuple4",
"fuel_guarded_inversion_LowStar.BufferView.Down.view",
"fuel_guarded_inversion_Vale.Interop.Heap_s.interop_heap",
"fuel_guarded_inversion_Vale.Interop.Types.b8",
"function_token_typing_Prims.int",
"function_token_typing_Vale.Def.Words_s.nat8",
"lemma_FStar.Set.lemma_equal_elim",
"lemma_LowStar.BufferView.Down.as_buffer_mk_buffer_view",
"proj_equation_FStar.Pervasives.Mkdtuple4__1",
"proj_equation_FStar.Pervasives.Mkdtuple4__2",
"proj_equation_FStar.Pervasives.Mkdtuple4__3",
"refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
"refinement_interpretation_Tm_refine_50d3b3dd51fb0799a5eeaaea500ed7b0",
"refinement_interpretation_Tm_refine_76e59c7a065e37ed8356ffe7fa5f9837",
"refinement_interpretation_Tm_refine_a0cd7d06c5da6444b6b51b319febde8e",
"refinement_interpretation_Tm_refine_b50f45fba9bc6f60eec05ca9dc1f94ef",
"refinement_interpretation_Tm_refine_f053bb82fde0bb5e3b79f846e507678a",
"typing_FStar.Map.domain", "typing_FStar.UInt8.t",
"typing_Vale.Interop.Heap_s.__proj__InteropHeap__item__hs",
"typing_Vale.Interop.Types.__proj__Buffer__item__bsrc",
"typing_Vale.Interop.Types.__proj__Buffer__item__src",
"typing_Vale.Interop.Types.__proj__Buffer__item__writeable",
"typing_Vale.Interop.Types.b8_preorder",
"typing_Vale.Interop.Types.base_typ_as_type",
"typing_Vale.Interop.Types.down_view"
],
0,
"dd329bd19281d4baac7bdedcdbcbc09e"
]
]
]
Computing file changes ...