From 7692a585c6ae4ddf0f5e21bda24e3f94392f8eb7 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 7 Feb 2024 15:52:37 -0800 Subject: [PATCH] Pulse.Steel.Wrapper long gone --- lib/steel/pulse/Makefile | 2 - lib/steel/pulse/Pulse.Steel.Wrapper.fst.hints | 343 ------------------ .../pulse/Pulse.Steel.Wrapper.fsti.hints | 26 -- 3 files changed, 371 deletions(-) delete mode 100644 lib/steel/pulse/Pulse.Steel.Wrapper.fst.hints delete mode 100644 lib/steel/pulse/Pulse.Steel.Wrapper.fsti.hints diff --git a/lib/steel/pulse/Makefile b/lib/steel/pulse/Makefile index 285d3998a..236da4407 100755 --- a/lib/steel/pulse/Makefile +++ b/lib/steel/pulse/Makefile @@ -14,8 +14,6 @@ include ../runlim.mk MY_FSTAR=$(RUNLIM) $(FSTAR) $(SIL) $(FSTAR_OPTIONS) -Pulse.Steel.Wrapper.fst.checked: FSTAR_OPTIONS+=--load_cmxs steel - %.checked: $(call msg, "CHECK", $(basename $(notdir $@))) @# You can debug with --debug $(basename $(notdir $<)) diff --git a/lib/steel/pulse/Pulse.Steel.Wrapper.fst.hints b/lib/steel/pulse/Pulse.Steel.Wrapper.fst.hints deleted file mode 100644 index d88b647dc..000000000 --- a/lib/steel/pulse/Pulse.Steel.Wrapper.fst.hints +++ /dev/null @@ -1,343 +0,0 @@ -[ - "±aDGÇ\u0007ýgcB\u0003‰ø\u00035G", - [ - [ - "Pulse.Steel.Wrapper.intro_vprop_post_equiv", - 1, - 2, - 1, - [ "@query" ], - 0, - "4dcf36fc0a22f8520417d345b09f24fa" - ], - [ - "Pulse.Steel.Wrapper.elim_vprop_post_equiv", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "defn_equation_Pulse.Steel.Wrapper.vprop_post_equiv", - "equation_Prims.prop", "equation_Prims.subtype_of", - "l_quant_interp_25c78b80b0f4b31a65cc09c664681812", - "refinement_interpretation_Tm_refine_73f210ca6e0061ed4a3150f69b8f33bf", - "typing_Pulse.Steel.Wrapper.vprop_post_equiv", "unit_inversion" - ], - 0, - "fff893434424528f9f3094d54ecd4b39" - ], - [ - "Pulse.Steel.Wrapper.vprop_equiv_refl", - 1, - 2, - 1, - [ "@query" ], - 0, - "85543fa0c63a89062919747a57a84a9a" - ], - [ - "Pulse.Steel.Wrapper.vprop_equiv_sym", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_Prims.squash", - "equation_Pulse.Steel.Wrapper.vprop_equiv", - "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" - ], - 0, - "fbdfe8174f3cb114115e513e6194bbad" - ], - [ - "Pulse.Steel.Wrapper.vprop_equiv_trans", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_Prims.squash", - "equation_Pulse.Steel.Wrapper.vprop_equiv", - "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" - ], - 0, - "46f653007066b100a40b56a2984f4325" - ], - [ - "Pulse.Steel.Wrapper.vprop_equiv_unit", - 1, - 2, - 1, - [ "@query" ], - 0, - "47faecfa68a5c5aabbb18a06433aa176" - ], - [ - "Pulse.Steel.Wrapper.vprop_equiv_comm", - 1, - 2, - 1, - [ "@query" ], - 0, - "63b1e8b07e9c4bb05242c63a30549a87" - ], - [ - "Pulse.Steel.Wrapper.vprop_equiv_assoc", - 1, - 2, - 1, - [ "@query" ], - 0, - "e4dad550308a30ab67d487ac02caec9f" - ], - [ - "Pulse.Steel.Wrapper.vprop_equiv_cong", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_Prims.squash", - "equation_Pulse.Steel.Wrapper.vprop_equiv", - "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" - ], - 0, - "608f666c4f1712a322048d8ce9e3b4e8" - ], - [ - "Pulse.Steel.Wrapper.vprop_equiv_ext", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_0dee8cb03258a67c2f7ec66427696212" - ], - 0, - "1cee3ce40946fd5d87fa194896cf6b6b" - ], - [ - "Pulse.Steel.Wrapper.bind_stt_atomic_ghost", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "Pulse.Steel.Wrapper_interpretation_Tm_arrow_44a3bfa508921f33b48c300bd121e494", - "equation_Pulse.Steel.Wrapper.non_informative_witness", - "lemma_FStar.Ghost.reveal_hide", - "refinement_interpretation_Tm_refine_0384ec095b850a18864324063aca63b2", - "typing_FStar.Ghost.hide" - ], - 0, - "1f037524e0311658be3974a46d9c43a9" - ], - [ - "Pulse.Steel.Wrapper.bind_stt_ghost_atomic", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "Pulse.Steel.Wrapper_interpretation_Tm_arrow_44a3bfa508921f33b48c300bd121e494", - "equation_Pulse.Steel.Wrapper.non_informative_witness", - "lemma_FStar.Ghost.reveal_hide", - "refinement_interpretation_Tm_refine_0384ec095b850a18864324063aca63b2", - "typing_FStar.Ghost.hide" - ], - 0, - "14698f20db00ec863c5de7acc6dbae0a" - ], - [ - "Pulse.Steel.Wrapper.lift_stt_ghost", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "Pulse.Steel.Wrapper_interpretation_Tm_arrow_44a3bfa508921f33b48c300bd121e494", - "lemma_FStar.Ghost.reveal_hide", - "refinement_interpretation_Tm_refine_0384ec095b850a18864324063aca63b2", - "typing_FStar.Ghost.hide" - ], - 0, - "32e418b9b4e8336e45430417cf08fe56" - ], - [ - "Pulse.Steel.Wrapper.sub_stt", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_Prims.squash", - "equation_Pulse.Steel.Wrapper.vprop_equiv", - "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" - ], - 0, - "01967ab2357c4986d592093bca7101fe" - ], - [ - "Pulse.Steel.Wrapper.sub_stt_atomic", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_Prims.squash", - "equation_Pulse.Steel.Wrapper.vprop_equiv", - "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" - ], - 0, - "01a897571846411b8bcbbcc4e9805378" - ], - [ - "Pulse.Steel.Wrapper.sub_stt_ghost", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_Prims.squash", - "equation_Pulse.Steel.Wrapper.vprop_equiv", - "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" - ], - 0, - "670cf6e150bc8244be720ed660bbbf2c" - ], - [ - "Pulse.Steel.Wrapper.rewrite", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_Prims.squash", - "equation_Pulse.Steel.Wrapper.vprop_equiv", - "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" - ], - 0, - "425d1f1f2a86cf1626eafcb14578eef9" - ], - [ - "Pulse.Steel.Wrapper.read", - 1, - 2, - 1, - [ "@query", "eq2-interp", "equation_Steel.Effect.Common.prop_and" ], - 0, - "05d416a03e335f95cd2ed392b761d245" - ], - [ - "Pulse.Steel.Wrapper.read_atomic", - 1, - 2, - 1, - [ "@query", "eq2-interp", "equation_Pulse.Steel.Wrapper.eq2_prop" ], - 0, - "5b062595f1a422a565ba88ebf4ffce0b" - ], - [ - "Pulse.Steel.Wrapper.gread", - 1, - 2, - 1, - [ - "@query", "eq2-interp", "equation_Prims.l_True", - "equation_Steel.Effect.Common.prop_and", "true_interp" - ], - 0, - "1726a551f20d6cac6f0799d2cd9cadfd" - ], - [ - "Pulse.Steel.Wrapper.ggather", - 1, - 2, - 1, - [ - "@query", "eq2-interp", "equation_Prims.l_True", - "equation_Steel.Effect.Common.prop_and", "true_interp" - ], - 0, - "38ea133bf768bbd3b6f35bf5eaf37ea6" - ], - [ - "Pulse.Steel.Wrapper.op_Array_Access", - 1, - 2, - 1, - [ "@query" ], - 0, - "cb374cef653283d380796969eebf5b06" - ], - [ - "Pulse.Steel.Wrapper.op_Array_Access", - 2, - 2, - 1, - [ "@query" ], - 0, - "337764123fbdb89f8327ddb577e86cce" - ], - [ - "Pulse.Steel.Wrapper.op_Array_Assignment", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_a32a4320cf25bdfeab0502d89cf19d62" - ], - 0, - "41c9fc6415878ebd330a1b14698f38e5" - ], - [ - "Pulse.Steel.Wrapper.op_Array_Assignment", - 2, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_a32a4320cf25bdfeab0502d89cf19d62" - ], - 0, - "bfe2748b6fc4f54ec65578bb51dfdf97" - ], - [ - "Pulse.Steel.Wrapper.elim_pure_explicit", - 1, - 2, - 1, - [ "@query" ], - 0, - "450b191d693f5e2b9552dc73ae6325e1" - ], - [ - "Pulse.Steel.Wrapper.elim_pure", - 1, - 2, - 1, - [ "@query" ], - 0, - "cd6a1ac63fd483fc646545d0a18928bc" - ], - [ - "Pulse.Steel.Wrapper.intro_pure", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", "equation_Prims.squash", - "refinement_interpretation_Tm_refine_2de20c066034c13bf76e9c0b94f4806c" - ], - 0, - "2ffa187cc2c50d96fac95de1561695b7" - ], - [ - "Pulse.Steel.Wrapper.stt_ghost_reveal", - 1, - 2, - 1, - [ - "@query", "eq2-interp", "equation_Prims.l_True", - "equation_Pulse.Steel.Wrapper.eq2_prop", - "equation_Steel.Effect.Common.prop_and", "true_interp" - ], - 0, - "2a00d0a25ed5851245590ff2c1812d1d" - ] - ] -] \ No newline at end of file diff --git a/lib/steel/pulse/Pulse.Steel.Wrapper.fsti.hints b/lib/steel/pulse/Pulse.Steel.Wrapper.fsti.hints deleted file mode 100644 index aa7df6e09..000000000 --- a/lib/steel/pulse/Pulse.Steel.Wrapper.fsti.hints +++ /dev/null @@ -1,26 +0,0 @@ -[ - "\n\u000esþŒ\u000eeƒñZÏÓVžöö", - [ - [ - "Pulse.Steel.Wrapper.op_Array_Access", - 1, - 2, - 1, - [ "@query" ], - 0, - "2098a8199b0eabb28f6dc24aa2d7bcad" - ], - [ - "Pulse.Steel.Wrapper.op_Array_Assignment", - 1, - 2, - 1, - [ - "@MaxIFuel_assumption", "@query", - "refinement_interpretation_Tm_refine_a32a4320cf25bdfeab0502d89cf19d62" - ], - 0, - "ae87195f730889f7479ff1ce98af9fa6" - ] - ] -] \ No newline at end of file