Extraction

example/Example.Pump.Extract.fst

@@ -9,15 +9,8 @@ module Example.Pump.Extract
 
 open Example.Pump.Check
 
-%splice [
-    controller_body_state; __extractable_controller_body;
-    controller_body_system; controller_body_reset; controller_body_step
-  ]
+%splice[]
   (Pipit.Plugin.Extract.extract (`%controller_body))
 
-%splice [
-    controller_state; __extractable_controller;
-    controller_system; controller_reset; controller_step
-  ]
+%splice[]
   (Pipit.Plugin.Extract.extract (`%controller))
-

example/Example.Simple.Extract.fst

@@ -15,8 +15,5 @@ module Example.Simple.Extract
 
 open Example.Simple.Check
 
-%splice [
-    count_when_state; __extractable_count_when;
-    count_when_system; count_when_reset; count_when_step
-  ]
+%splice[]
   (Pipit.Plugin.Extract.extract (`%count_when))

example/Makefile

@@ -8,6 +8,15 @@ FSTAR_ALREADY_CACHED ?=
 # Note: example/ttcan/ is currently disabled (see example/readme.md); it has
 # its own dormant wiring and is not picked up here.
 
+# Silence F* warning 249 ("Losing precision when encoding a function literal")
+# emitted by the SMT encoder for each Pulse [fn] splice in this component.
+# The warning is encoder imprecision, not a soundness issue; see the comment
+# above [mk_reset] / [mk_step] in [pipit/extract/Pipit.Exec.Pulse.fst] for
+# details. An in-file [#set-options]/[#push-options] pragma only catches half
+# of the warnings emitted during splice processing, so we apply the flag at
+# the CLI level here.
+FSTAR_EXTRA_OPT += --warn_error -249
+
 include $(ROOT_DIR)/make/include/base.mk
 
 extract: $(BUILD)/Example.Simple.Extract.extract

pipit/base/Pipit.Tactics.Base.fst

@@ -120,3 +120,28 @@ let rec mk_list (tms: list Tac.term): Tac.Tac Tac.term =
   | a :: tms ->
     let tms = mk_list tms in
     `((`#a) :: (`#tms))
+
+
+(* Walk [t] and accumulate the distinct fully-qualified names that occur
+  as a [Tv_FVar] or [Tv_UInst] head AND are present in [forbidden].
+  Result preserves first-encounter order with no duplicates. Used by
+  fail-loud specialization tactics to report which "must not survive"
+  names are still present in a goal after normalization. *)
+let term_collect_fqns (forbidden: list string) (t: Tac.term)
+  : Tac.Tac (list string)
+=
+  let acc: Tac.tref (list string) = Tac.alloc [] in
+  let visit (sub: Tac.term): Tac.Tac Tac.term =
+    (match Tac.inspect sub with
+      | Tac.Tv_FVar fv
+      | Tac.Tv_UInst fv _ ->
+        let nm = Ref.implode_qn (Tac.inspect_fv fv) in
+        let seen = Tac.read acc in
+        if List.mem nm forbidden && not (List.mem nm seen)
+        then Tac.write acc (List.append seen [nm])
+        else ()
+      | _ -> ());
+    sub
+  in
+  let _ = FStar.Tactics.Visit.visit_tm visit t in
+  Tac.read acc

pipit/core/Pipit.Exp.Checked.Base.fst

@@ -145,3 +145,18 @@ and bless_apps (#t: table) (#c: context t) (#a: funty t.ty) (e: exp_apps t c a):
   match e with
   | XPrim p -> XPrim p
   | XApp f e -> XApp (bless_apps f) (bless e)
+
+(* Construct a contract node from an already-typed rely, guarantee, and
+   implementation. The rely is NOT recursively blessed: the rely is a
+   precondition that the contract's *caller* is obliged to discharge,
+   so any check / inner contract sitting inside it must stay unknown
+   until those callsites are verified. The guar and impl are blessed
+   recursively because the contract assembly is responsible for the
+   body's internal obligations. The top-level status is PSUnknown for
+   the same reason as the rely. *)
+let bless_contract (#t: table) (#c: context t) (#a: t.ty)
+  (r: exp t       c        t.propty)
+  (g: exp t (a :: c)       t.propty)
+  (b: exp t       c        a):
+  Tot (exp t c a) =
+  XContract PM.PSUnknown r (bless g) (bless b)

pipit/core/Pipit.Exp.Checked.Compound.fst

@@ -37,10 +37,7 @@ let bless (#a: ('t).ty) (#c: context 't) (e: cexp 't c a { check_all PM.check_mo
 
 
 let bless_contract (#a: ('t).ty) (#c: context 't) (r: cexp 't c ('t).propty) (g: cexp 't (a :: c) ('t).propty) (b: cexp 't c a { contract_valid r g b }): cexp 't c a =
-  let rely = r in
-  let guar = Pipit.Exp.Checked.Base.bless g in
-  let body = Pipit.Exp.Checked.Base.bless b in
-  let e' = XContract PM.PSUnknown rely guar body in
+  let e' = Pipit.Exp.Checked.Base.bless_contract r g b in
   XCB.lemma_sealed_of_bless true g;
   XCB.lemma_sealed_of_bless false b;
   XCB.lemma_check_all_bless_contract r g b;