snap

FStarLang · Jul 26, 2023 · 41a2f68 · 41a2f68
1 parent b55484d
commit 41a2f68
Show file tree

Hide file tree

Showing 112 changed files with 7,389 additions and 6,942 deletions.
diff --git a/lib/steel/pulse/Pulse.Checker.Abs.fst.hints b/lib/steel/pulse/Pulse.Checker.Abs.fst.hints
@@ -1,5 +1,5 @@
 [
-  "�t�n9�U�L\u001fZc\u001e�\u000e>",
+  "j�R\u0005���h��\u0004�*ۓz",
   [
     [
       "Pulse.Checker.Abs.check_effect_annotation",
@@ -13,7 +13,7 @@
         "string_typing"
       ],
       0,
-      "35e023a0fc1fe95626112d8357759639"
+      "e3ed564cdb21aa89d1f311e001c5aa9a"
     ],
     [
       "Pulse.Checker.Abs.check_abs",
@@ -48,6 +48,7 @@
         "equation_FStar.Sealed.Inhabited.sealed",
         "equation_FStar.Sealed.Inhabited.sealed_", "equation_Prims.eqtype",
         "equation_Prims.nat", "equation_Pulse.Checker.Pure.push_context",
+        "equation_Pulse.Syntax.Base.comp_st",
         "equation_Pulse.Syntax.Base.index",
         "equation_Pulse.Syntax.Base.nvar",
         "equation_Pulse.Syntax.Base.ppname_default",
@@ -115,6 +116,7 @@
         "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
         "refinement_interpretation_Tm_refine_6c182d6f9819de8b46a7a4d39f909d33",
         "refinement_interpretation_Tm_refine_6e8e5238aadfc712ef5fa6bc6310c384",
+        "refinement_interpretation_Tm_refine_78cf9fabb706bab7e54de904b7db9d2a",
         "refinement_interpretation_Tm_refine_7f3ad0958305f2921bfac06f466396ae",
         "refinement_interpretation_Tm_refine_8c22aa61a47c16d0229ef090894097c8",
         "refinement_interpretation_Tm_refine_ba488b4f12660f6fd23fa65ec4b4a4ff",
@@ -136,7 +138,7 @@
         "typing_Pulse.Typing.Env.push_binding"
       ],
       0,
-      "85aa26bf0c11aef9fef5b754dfc2e923"
+      "b392d6b9fe11f6e3b5eb6649a0773099"
     ]
   ]
 ]
diff --git a/lib/steel/pulse/Pulse.Checker.Admit.fst.hints b/lib/steel/pulse/Pulse.Checker.Admit.fst.hints
@@ -1,5 +1,5 @@
 [
-  "��Lzp��\u007f0�\r|kȲ\u001f",
+  "\u007fO����`\u0011�����Z#",
   [
     [
       "Pulse.Checker.Admit.post_hint_compatible",
@@ -11,7 +11,7 @@
         "lemma_FStar.Pervasives.invertOption"
       ],
       0,
-      "3bd7c950f7ea9004a5f6eec1ac143e79"
+      "47e3c39481aa9899af8f9bc13b9d21f1"
     ],
     [
       "Pulse.Checker.Admit.check",
@@ -24,6 +24,8 @@
         "@fuel_irrelevance_Pulse.Syntax.Naming.freevars.fuel_instrumented",
         "@query",
         "FStar.Pervasives.Native_pretyping_b53dbd183c526bc5d0f20d7b966ae125",
+        "Prims_pretyping_ce036b6b736ef4e0bc3a9ff132a12aed",
+        "Pulse.Syntax.Base_pretyping_fe09dc1e796799f4bac0760e63f30d40",
         "bool_inversion",
         "constructor_distinct_FStar.Pervasives.Native.None",
         "constructor_distinct_FStar.Pervasives.Native.Some",
@@ -33,6 +35,8 @@
         "constructor_distinct_Pulse.Syntax.Base.C_STAtomic",
         "constructor_distinct_Pulse.Syntax.Base.C_STGhost",
         "constructor_distinct_Pulse.Syntax.Base.STT",
+        "constructor_distinct_Pulse.Syntax.Base.STT_Atomic",
+        "constructor_distinct_Pulse.Syntax.Base.STT_Ghost",
         "constructor_distinct_Pulse.Syntax.Base.Tm_Admit",
         "data_elim_Pulse.Typing.Mkpost_hint_t",
         "disc_equation_FStar.Pervasives.Native.None",
@@ -45,22 +49,19 @@
         "equation_Pulse.Checker.Admit.post_hint_compatible",
         "equation_Pulse.Syntax.Base.index", "equation_Pulse.Syntax.Base.typ",
         "equation_Pulse.Syntax.Base.v_as_nv",
-        "equation_Pulse.Syntax.Base.var",
+        "equation_Pulse.Syntax.Base.var", "equation_Pulse.Syntax.Base.vprop",
         "equation_Pulse.Syntax.Naming.close_term",
         "equation_Pulse.Syntax.Naming.open_term",
         "equation_Pulse.Syntax.Pure.tm_type",
-        "equation_Pulse.Typing.Env.dom",
-        "equation_Pulse.Typing.Env.env_extends",
-        "equation_Pulse.Typing.Env.extends_with",
-        "equation_Pulse.Typing.Env.lookup",
+        "equation_Pulse.Typing.Env.dom", "equation_Pulse.Typing.Env.lookup",
         "equation_Pulse.Typing.FV.set_minus",
         "equation_Pulse.Typing.comp_admit",
         "equation_Pulse.Typing.fresh_wrt",
-        "equation_Pulse.Typing.post_hint_for_env_p",
         "equation_Pulse.Typing.post_hint_opt",
         "fuel_guarded_inversion_FStar.Pervasives.Native.option",
         "fuel_guarded_inversion_FStar.Tactics.Result.__result",
         "fuel_guarded_inversion_Pulse.Syntax.Base.ctag",
+        "fuel_guarded_inversion_Pulse.Syntax.Base.st_term",
         "fuel_guarded_inversion_Pulse.Syntax.Base.term",
         "fuel_guarded_inversion_Pulse.Typing.post_hint_t",
         "function_token_typing_Prims.__cache_version_number__",
@@ -82,7 +83,6 @@
         "proj_equation_Pulse.Syntax.Base.Mkst_comp_pre",
         "proj_equation_Pulse.Syntax.Base.Mkst_comp_res",
         "proj_equation_Pulse.Syntax.Base.Mkst_comp_u",
-        "proj_equation_Pulse.Typing.Mkpost_hint_t_g",
         "proj_equation_Pulse.Typing.Mkpost_hint_t_post",
         "proj_equation_Pulse.Typing.Mkpost_hint_t_ret_ty",
         "proj_equation_Pulse.Typing.Mkpost_hint_t_u",
@@ -107,23 +107,27 @@
         "projection_inverse_Pulse.Syntax.Base.Mkst_comp_res",
         "projection_inverse_Pulse.Syntax.Base.Mkst_comp_u",
         "projection_inverse_Pulse.Syntax.Base.Tm_Admit__0",
-        "refinement_interpretation_Tm_refine_0e05a441736ee1a990510e8440d3b4d7",
         "refinement_interpretation_Tm_refine_262f039a938fc14ac016e995f8cd074e",
         "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
         "refinement_interpretation_Tm_refine_542f9d4f129664613f2483a6c88bc7c2",
+        "refinement_interpretation_Tm_refine_717807cab8f2d0ea552aff3c667b3f67",
         "refinement_interpretation_Tm_refine_ba488b4f12660f6fd23fa65ec4b4a4ff",
         "refinement_interpretation_Tm_refine_ecc02256d87cc95183f37fc512700b64",
+        "refinement_interpretation_Tm_refine_eed994d15518279ab75d745192d0d368",
+        "string_typing",
         "token_correspondence_Pulse.Syntax.Naming.freevars.fuel_instrumented",
         "typing_FStar.Pervasives.Native.uu___is_None",
         "typing_FStar.Reflection.V2.Data.var", "typing_FStar.Set.complement",
         "typing_FStar.Set.mem", "typing_FStar.Set.singleton",
+        "typing_Pulse.Syntax.Base.__proj__Mkst_term__item__range",
         "typing_Pulse.Syntax.Naming.close_term",
         "typing_Pulse.Syntax.Naming.freevars",
         "typing_Pulse.Typing.Env.as_map", "typing_Pulse.Typing.Env.dom",
-        "typing_Pulse.Typing.Env.fstar_env"
+        "typing_Pulse.Typing.Env.fstar_env",
+        "typing_Pulse.Typing.Env.push_context"
       ],
       0,
-      "aa5544803dcd5a35cb45892a02c3e128"
+      "3089e3801a376cde2895ac975287e48a"
     ]
   ]
 ]
diff --git a/lib/steel/pulse/Pulse.Checker.Admit.fsti.hints b/lib/steel/pulse/Pulse.Checker.Admit.fsti.hints
@@ -1 +1 @@
-[ "�A�\r��\u001e<�uZ���p\t", [] ]
+[ "���V��UPh!G�%\u0010H�", [] ]
diff --git a/lib/steel/pulse/Pulse.Checker.AssertWithBinders.fst.hints b/lib/steel/pulse/Pulse.Checker.AssertWithBinders.fst.hints
@@ -1,5 +1,5 @@
 [
-  "*-\u001bՒ�C\u0013�)\b>\u001f\u001d�",
+  "���v5_<��%w��[�",
   [
     [
       "Pulse.Checker.AssertWithBinders.option_must",
@@ -8,7 +8,7 @@
       1,
       [ "@query", "lemma_FStar.Pervasives.invertOption" ],
       0,
-      "ebb3e7478db6b3278a09d981bf96431c"
+      "223601c56f746132bd21e5bdb42bfa1b"
     ],
     [
       "Pulse.Checker.AssertWithBinders.refl_abs_binders",
@@ -18,12 +18,20 @@
       [
         "@MaxIFuel_assumption", "@query",
         "Prims_pretyping_ce036b6b736ef4e0bc3a9ff132a12aed",
+        "constructor_distinct_FStar.Tactics.Result.Failed",
+        "constructor_distinct_FStar.Tactics.Result.Success",
         "equation_FStar.Sealed.Inhabited.is_sealed",
         "fuel_guarded_inversion_FStar.Tactics.Result.__result",
-        "string_typing", "true_interp"
+        "projection_inverse_FStar.Tactics.Result.Failed_a",
+        "projection_inverse_FStar.Tactics.Result.Failed_exn",
+        "projection_inverse_FStar.Tactics.Result.Failed_ps",
+        "projection_inverse_FStar.Tactics.Result.Success_a",
+        "projection_inverse_FStar.Tactics.Result.Success_ps",
+        "projection_inverse_FStar.Tactics.Result.Success_v", "string_typing",
+        "true_interp"
       ],
       0,
-      "0adc76f14300d9b954fe51db69b64517"
+      "15b3120f0dc57ee5bfead3be7616d0e5"
     ],
     [
       "Pulse.Checker.AssertWithBinders.infer_binder_types",
@@ -78,7 +86,7 @@
         "typing_tok_FStar.Reflection.V2.Data.Q_Explicit@tok"
       ],
       0,
-      "3ecd2bec4058f5b9a86f8173732126c2"
+      "c1aedee9309bebe7c96b357c0b495da1"
     ],
     [
       "Pulse.Checker.AssertWithBinders.open_binders",
@@ -134,7 +142,7 @@
         "typing_Pulse.Typing.Env.fstar_env"
       ],
       0,
-      "a1f922564db0ab0d5f5d0ee635b838f7"
+      "a0c40b167498c1b0be38918dff6b69a2"
     ],
     [
       "Pulse.Checker.AssertWithBinders.close_binders",
@@ -157,20 +165,26 @@
       [
         "@MaxIFuel_assumption", "@query",
         "Prims_pretyping_ce036b6b736ef4e0bc3a9ff132a12aed",
+        "constructor_distinct_FStar.Pervasives.Native.None",
+        "constructor_distinct_FStar.Pervasives.Native.Some",
+        "constructor_distinct_FStar.Tactics.Result.Failed",
         "constructor_distinct_FStar.Tactics.Result.Success",
         "equation_Prims.eqtype",
         "equation_Pulse.Syntax.Base.range_singleton_trigger",
         "fuel_guarded_inversion_FStar.Tactics.Result.__result",
         "function_token_typing_Prims.string", "kinding_Prims.list@tok",
         "lemma_FStar.Pervasives.invertOption",
+        "projection_inverse_FStar.Tactics.Result.Failed_a",
+        "projection_inverse_FStar.Tactics.Result.Failed_exn",
+        "projection_inverse_FStar.Tactics.Result.Failed_ps",
         "projection_inverse_FStar.Tactics.Result.Success_a",
         "projection_inverse_FStar.Tactics.Result.Success_ps",
         "projection_inverse_FStar.Tactics.Result.Success_v",
         "refinement_interpretation_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
         "string_typing"
       ],
       0,
-      "1a62ee8ce2a47156dcb65222bb5458ab"
+      "f09e54dd66c1f55c55a09afb285920cb"
     ],
     [
       "Pulse.Checker.AssertWithBinders.check_unfoldable",
@@ -214,19 +228,20 @@
         "equation_FStar.Reflection.V2.Data.var",
         "equation_FStar.Set.disjoint", "equation_Prims.nat",
         "equation_Pulse.Checker.Base.checker_res_matches_post_hint",
+        "equation_Pulse.Checker.Base.checker_result_inv",
         "equation_Pulse.Syntax.Base.not_tv_unknown",
         "equation_Pulse.Syntax.Base.typ", "equation_Pulse.Syntax.Base.var",
         "equation_Pulse.Typing.Env.disjoint",
         "equation_Pulse.Typing.Env.dom",
-        "equation_Pulse.Typing.Env.env_extends",
-        "equation_Pulse.Typing.Env.extends_with",
         "equation_Pulse.Typing.post_hint_for_env_p",
         "equation_Pulse.Typing.post_hint_opt",
         "fuel_guarded_inversion_FStar.Pervasives.Native.option",
         "fuel_guarded_inversion_FStar.Tactics.Result.__result",
         "fuel_guarded_inversion_Pulse.Syntax.Base.proof_hint_type",
+        "fuel_guarded_inversion_Pulse.Syntax.Base.st_term",
         "function_token_typing_Prims.__cache_version_number__",
-        "int_inversion", "kinding_Pulse.Typing.post_hint_t@tok",
+        "int_inversion", "kinding_Pulse.Syntax.Base.term@tok",
+        "kinding_Pulse.Typing.post_hint_t@tok",
         "lemma_FStar.Pervasives.invertOption",
         "lemma_FStar.Reflection.Typing.inspect_pack",
         "lemma_FStar.Set.lemma_equal_elim",
@@ -235,6 +250,7 @@
         "lemma_Pulse.Typing.Env.env_extends_trans",
         "lemma_Pulse.Typing.Env.mk_env_dom", "primitive_Prims.op_AmpAmp",
         "proj_equation_FStar.Pervasives.Native.Some_v",
+        "proj_equation_Prims.Mkdtuple2__1",
         "proj_equation_Pulse.Typing.Mkpost_hint_t_g",
         "projection_inverse_BoxBool_proj_0",
         "projection_inverse_FStar.Tactics.Result.Failed_a",
@@ -244,22 +260,26 @@
         "projection_inverse_FStar.Tactics.Result.Success_ps",
         "projection_inverse_FStar.Tactics.Result.Success_v",
         "projection_inverse_Pulse.Syntax.Base.Tm_ProofHintWithBinders__0",
-        "refinement_interpretation_Tm_refine_0e7cec6ed8f6e8567fd60faa69f1ee6b",
+        "refinement_interpretation_Tm_refine_22829e142fee025de3f65b2dd8597285",
         "refinement_interpretation_Tm_refine_262f039a938fc14ac016e995f8cd074e",
-        "refinement_interpretation_Tm_refine_30687c6bbf76a4ea67eae131536eafd7",
+        "refinement_interpretation_Tm_refine_7ad5682d990eaec6510764d663af54de",
         "refinement_interpretation_Tm_refine_ba488b4f12660f6fd23fa65ec4b4a4ff",
         "refinement_interpretation_Tm_refine_bf49085558242af8c310020a9c32bdc7",
+        "refinement_interpretation_Tm_refine_c368f222d3b510422f50624ef34643bf",
         "refinement_interpretation_Tm_refine_dd3396f06b5a01f3df9ed905e57d2aab",
-        "refinement_interpretation_Tm_refine_de1d02ad66483edc481b70db20a6b9af",
+        "refinement_interpretation_Tm_refine_eed994d15518279ab75d745192d0d368",
+        "string_typing", "typing_FStar.Map.domain",
         "typing_FStar.Reflection.Typing.unit_fv",
         "typing_FStar.Reflection.V2.Data.var", "typing_FStar.Set.empty",
         "typing_FStar.Set.intersect", "typing_FStar.Set.mem",
-        "typing_Pulse.Typing.Env.dom", "typing_Pulse.Typing.Env.fstar_env",
-        "typing_Pulse.Typing.Env.mk_env",
+        "typing_Pulse.Syntax.Base.__proj__Mkst_term__item__range",
+        "typing_Pulse.Typing.Env.as_map", "typing_Pulse.Typing.Env.dom",
+        "typing_Pulse.Typing.Env.fstar_env",
+        "typing_Pulse.Typing.Env.push_context",
         "typing_Pulse.Typing.__proj__Mkpost_hint_t__item__g"
       ],
       0,
-      "a56a99ca49f6a093f034d5d278aadf37"
+      "c6f591576fce77169b45becce2f77642"
     ]
   ]
 ]
diff --git a/lib/steel/pulse/Pulse.Checker.AssertWithBinders.fsti.hints b/lib/steel/pulse/Pulse.Checker.AssertWithBinders.fsti.hints
@@ -1 +1 @@
-[ "�\u001d���,-\b\u001dmU�\u0015��w", [] ]
+[ ",��rf5���\u0017H\u0010�,�K", [] ]