Extraction#21
Open
amosr wants to merge 16 commits into
Open
Conversation
Replace the legacy tac_normalize_pure / tac_extract postprocess pair on
splice-emitted state/system/reset/step sigelts with two fail-loud
tactics in pipit/extract/Pipit.Exec.Pulse.fst:
* tac_specialize_strict_pure (with NBE, for state/system)
* tac_specialize_strict_pulse (without NBE, for reset/step)
Each normalizes the goal then walks the residue with
Pipit.Tactics.Base.term_collect_fqns and fails with a diagnostic
naming any forbidden FQN that survived (Pipit_Context_Row_index,
coerce_eq, raw exp/exp_apps/exp_base, etc.) — far better than silently
letting <: any reach KaRaMeL. Split delta_only (helpers, hint) from
forbidden (true bugs, enforced); see /memories/repo/tooling-notes.md
2026-05-30 entry for the pure-vs-pulse norm-option rationale.
* pipit/base/Pipit.Tactics.Base.fst — new term_collect_fqns walker
(FStar.Tactics.Visit + Tac.alloc accumulator).
* pipit/source/Pipit.Plugin.Extract.fst — wire the splice through
tac_specialize_strict_{pure,pulse}, with per-splice extras forcing
inlining of <nm>_state and <nm>_system into <nm>_reset/<nm>_step.
* pipit/plugin-test/Plugin.Test.Simple.Extract.Debug.fst (new) —
self-contained twin of the splice pipeline, useful for poking at
norm behaviour without rebuilding the plugin.
* example/Example.{Simple,Pump}.Extract.fst — drop explicit %splice
name lists; the strict tactics now force the same outcome.
Suppress F* Warning 249 ("Losing precision when encoding a function
literal") emitted by the SMT encoder for each splice-emitted Pulse fn
postcondition. Tried five approaches (see comment block above mk_reset
in Pipit.Exec.Pulse.fst); only CLI-level --warn_error -249 works,
because in-file pragmas only catch half the warnings emitted during
splice processing. Verified: 24 -> 0 warnings; make example, make
example-extract, make plugin-test all clean.
* example/Makefile, pipit/plugin-test/Makefile —
FSTAR_EXTRA_OPT += --warn_error -249, with explanatory comment.
* pipit/extract/Pipit.Exec.Pulse.fst — documentation comment above
mk_reset/mk_step explaining why no in-source qualifier suffices.
Restructure doc/roadmap/v1-source-followups.md around the four
timeframe tiers (short / mid / long / very-long term), keyed off the
TTCAN port under example/ttcan/ as the v1-complete benchmark.
Short-term:
* Contract support ({rely; guar; body} at the surface). Biggest
single TTCAN blocker; was deleted with Pipit.Sugar.Contract in v0.
* proof_induct k for k > 1 (Fir.Check.bibo3) and a less misleading
name for k = 0 (currently absent; "induct0" suggests induction).
Resolved a previously-self-contradictory roadmap claim: TTCAN does
NOT need proof_induct k > 1; the only active uses are
system_induct_k1. proof_induct k is for bibo3.
* [@@proof_induct1] over static parameters (TTCAN's trigger_index
takes (cfg c) statics — currently hits F* Error 189 in
mk_check_induct1_decl).
* Lemma combinator (currently surfaced as lemma_pattern in TTCAN
via a ghost-stream effect — wants a plugin-recognised version).
* Top-level let rec stream-stripping in pre_decl.
Mid-term:
* CSE on the core, with [@@proof_no_cse] opt-out. Concrete
motivating cases: Pump's spec_any_needs_extra_invariant_manual_cse
and TTCAN's commented-out sofar (time_increasing now) ==> ...
contract.
* Multi-arm match on stream scrutinees (AMatch currently only
handles AppPureConst; blocks eg_streaming_match_option).
* Mutual recursion across top-level stream functions.
Long-term:
* Separate compilation/extraction (one C entry per contract).
* Meta-specialisation (fir [1;2;3] specialised at splice time;
subsumes the FirN list-recursion blocker).
Very long-term:
* Automatic invariant discovery / applicative invariants.
* Counterexample generation from SMT failures.
* Iterative proof_induct k = 0..n search.
Other gaps spotted while writing this:
* Refinement preservation (Reflect.strip_refinements drops
everything; needs dependent exp typing).
* Auto has_stream derivation in the #lang-pipit preamble (~50%
of TTCAN's surviving boilerplate is hand-written instances).
* Splice diagnostics — Error 189 surfaces with no surface-level
context.
* KRML -warn-error -26 workaround in TTCAN extraction.
Soundness (separate group, not user-facing):
* The new Pipit.Source.Ast.Lower emits exp, not cexp; bless at the
splice site claims property obligations without proving them.
Structurally easy fix, deferred to keep iteration cheap.
* Six abstract-layer admits marked TODO:ADMIT:update to latest F*
20251116 — proofs that worked before the F* dev-build bump and
broke on the new normalizer/SMT encoding (System.Ind,
System.Exp.Check.{Contracts,Obligations,Assumptions},
Exp.Checked.Bless).
* Core cexp-preservation admits: Exp.Checked.Compound.{close1,
weaken}, Exp.SimplifyLet.bigstep_simplify.
* Small bookkeeping admits in Exp.Binding and Context.Base
("TODO PROVE EASY").
* Intentional axioms listed for the record: Prim.Shallow.axiom_*,
assume val fby / check / rec'.
Out of scope for v1: FirN-style list-recursion (subsumed by long-term
meta-specialisation), mutual recursion beyond the mid-term entry,
binding new variables in streaming pattern matches.
Replace the v1 'contract { rely; guar; body }' record-literal shape
with a Pulse-style effect form in the Contract support section:
[@@proof_induct1]
let mul_underapprox (a b: stream int): Stream int
(requires true)
(ensures (fun r -> a = 0 && b = 0 ==>^ r = 0)) =
a * b
Stream is a placeholder effect (degenerate Pure alias) defined in
Pipit.Source, carrying rely/guar as effect indices; the plugin
reflecter peels them off the let-binding's computation type.
Naming follows Pulse's stt (type) / STT (effect) split, mirroring
F*'s Tot a / Pure a (...) convention: lowercase stream a is the
default value type used in parameter and trivial-return positions;
uppercase Stream a (requires R)(ensures G) is the annotated form
for contracted return positions. Inputs stay lowercase (F* Error 187
forbids effects in parameter position).
Drops the 'contract must be at body top' v1 restriction (no body-shape
restriction is needed once the contract lives in the type) and the
field-punning alternative (no longer relevant). Flags a small
verify-at-implementation-time caveat about whether F* accepts
stream-typed effect indices.
Also includes the previously-uncommitted XExtracted modular-extraction
note under the long-term 'Separate compilation and extraction'
section.
New Soundness subsection 'Unannotated bindings discharge no checks;
need a default proof strategy', flagging that today a top-level
streaming let without [@@proof_...] silently skips all check
discharge -- a real surface-level soundness gap, not just a meta
proof obligation.
Sketch of the intended shape:
* Default: run an automatic proof attempt on every unannotated
binding, starting cheap (proof_noinduct / proof_induct0) and
escalating to proof_induct1. Cheapest tier should be effectively
free for combinator bindings with no checks at all; open
question is the cost when helpers carry checks.
* [@@proof_defer]: explicit opt-out. Body may carry checks, but
the caller discharges them -- useful for contract-style
reasoning where the body is visible but obligations float to
the contract boundary.
* Existing explicit annotations (proof_induct1, proof_induct k,
proof_contract_induct1, ...) keep their current meaning and
override the default.
Reframe the Soundness section header from 'not user-facing' to
'mostly not user-facing' to acknowledge this entry is the
exception. Cross-reference proof_induct k, the static-parameter
wrapper item, and the exp-vs-cexp entry as related work.
Rework the three roadmap mentions of proof_contract_induct1 /
proof_contract_induct k to reuse the existing proof_induct1 /
proof_induct k attributes instead, dispatching on the let-binding's
computation type (Stream a (requires R) (ensures G) vs plain
stream a). Same attribute, two code paths.
Touches:
* Contract support 'Plumbing' paragraph: attribute is reused
as-is; dispatch picks contract_of_stream1 + system_induct_k1
+ stream_of_contract1 when the effect head is Stream.
* Static-parameter wrapper note: 'shared with proof_induct k and
the contract-effect dispatch above', not a separate attribute.
* Default-proof Soundness entry: explicit-annotations bullet
lists proof_induct1 / proof_induct k and notes 'no new
proof_contract_* family is needed'.
No behavioural change \u2014 doc-only.
Drop proof_induct0 and the proof_invariant / proof_check / proof_safety candidate list in favour of proof_noinduct as the attribute name for k=0. Rationale recorded inline: proof_noinduct reads as a strict weakening of proof_induct1, whereas proof_invariant / proof_safety / proof_check don't make the strength relationship obvious. Touches the proof_induct k section heading, its bullet, the Contract support 'reused literally' cross-reference, and the default-proof Soundness entry's escalation ladder.
The existing Pipit.Tactics.Cse meta-tactic is the wrong building
block for the user-visible CSE story. What we actually want:
* Run CSE on the lifted core *after* inlining every __core_<id>
reference -- the inlining is what exposes the shared subterms
that today force manual hand-extraction in Pump and TTCAN.
* Run it just before constructing the abstract transition system,
as a plain semantic exp -> exp (or cexp -> cexp) pass, not as
a tactic over F* terms.
* Handle contract-aware rearrangement: CSE-ing a subterm shared
between a guar and the body (or across neighbouring contracts)
requires hoisting bindings past contract boundaries without
changing what rely/guar say.
* Verify the pass preserves big-step semantics -- same shape of
proof as Pipit.Exp.SimplifyLet's bigstep_simplify (currently
admitted; cross-referenced from Soundness).
Mid-term work list reworded accordingly: implement the verified
pass, run it after __core_* inlining and before abstract-system
construction, plus the [@@proof_no_cse] opt-out.
Replace the 'fresh design pass' placeholder with a concrete
near-term experiment plan and call out the silent-failure problem:
* First experiment lands a lemma_pattern-style combinator in
plugin-test with user-written patterns + top-level lemmas in
exactly the shape TTCAN uses today. Minimum viable shape to
unblock the TTCAN port and gather real consumers before
designing polish.
* Later: auto-synthesise the pattern marker + top-level Lemma
skeleton from a 'lemma_blagh x y z; ...' call so the plumbing
is invisible; pattern scoping to a specific rely/guar follows
once contracts land.
* Known downside: SMT patterns fire silently. If the pattern's
preconditions don't hold in the spliced transition system the
lemma just doesn't contribute and the user sees a bare check
failure -- same shape of issue as the TTCAN sofar / contract-
state comment block flagged in the CSE entry.
* Alternative to prototype after the plain-pattern experiment is
in tree: embed FStar.Tactics.term hints inside core expressions
as a fresh XHint constructor. Computationally irrelevant (same
as XCheck), so no impact on extraction or the abstract system,
and the obligation tactic can *report* missed hints instead of
failing silently.
First experiment from the 'Lemma combinator' entry of
doc/roadmap/v1-source-followups.md.
A single new module Plugin.Test.Core.Lemma demonstrates that the
historical TTCAN trick — pairing a unit-typed pattern marker with a
top-level Lemma … [SMTPat marker_call] — works as a plain #lang-pipit
source helper, with zero changes to Source / plugin / core.
The user-facing combinator is
assume val check_pattern (pat: unit): bool
assume val check_pattern_true (pat: unit):
Lemma (check_pattern pat = true) [SMTPat (check_pattern pat)]
[@@source_mode (ModeFun Stream true Stream)]
let lemma_pattern (p: unit): unit = check (check_pattern p)
%splice[] (PPL.lift_ast_tac1 "lemma_pattern")
Demo 1 wires it up against an assume-val opaque primitive: a Lemma
with [SMTPat (lemma_opaque_double_pattern x)] is triggered by the
lifted check obligation, and the discharge wrapper (induct1 +
norm_full) verifies. Demo 2 repeats the shape inside rec' to match
TTCAN's lemma_adequate_spacing_next_inc usage; the lift succeeds (the
discharge for the recursive case is gated on proof-induction
strengthening, which is the proof_induct k follow-up).
Encoding traps documented in the file:
* The naive 'check (p = ())' doesn't work: op_Equality #unit is
decidable (unit is a singleton) so the SMT encoder folds both
sides to () and the marker subterm disappears from triggering
position.
* An 'irreducible let check_pattern (pat: unit): bool = true' keeps
the marker subterm visible but the obligation 'check_pattern p =
true' is unprovable — SMT treats irreducible bodies as
uninterpreted (same as assume val).
* The assume-val + SMTPat-lemma encoding used here gets both
properties: opaque to the encoder (the trigger survives) AND a
paired SMTPat lemma to discharge the wrapper obligation. Costs
one SMTPat hit per lemma_pattern call.
* The pattern marker itself must be irreducible — otherwise
norm_full unfolds let marker x = () and the SMTPat application
disappears from the goal before Z3 sees it.
Promotion of lemma_pattern / check_pattern / check_pattern_true from
this test module to Pipit.Source is intentionally deferred until a
real consumer (TTCAN) exercises them.
The Lemma combinator experiment (f9f7acc) verified that lemma_pattern + check_pattern + check_pattern_true work end-to-end through the lift pipeline with zero plugin / core changes. Move the three definitions from the experimental Plugin.Test.Core.Lemma module up to Pipit.Source so any #lang-pipit consumer can use them by 'open Pipit.Source' (already the standard import). Pipit.Source gains: assume val check_pattern (pat: unit): bool assume val check_pattern_true (pat: unit): Lemma (check_pattern pat = true) [SMTPat (check_pattern pat)] [@@source_mode (ModeFun Stream true Stream)] let lemma_pattern (p: unit): unit = check (check_pattern p) %splice[] (PPL.lift_ast_tac1 "lemma_pattern") with a doc comment covering the intended usage shape (irreducible pattern marker + paired top-level Lemma … [SMTPat marker_call] + lemma_pattern (marker_call …) inside a streaming body) and the non-obvious encoding choice (assume-val + paired SMTPat lemma is the only shape that's both opaque to the SMT encoder and discharges the wrapper obligation). Plugin.Test.Core.Lemma drops its local copies of the three defs, keeping only the two demos (non-recursive eg_opaque + rec' shape eg_opaque_in_rec) and the Findings comment block as a regression test / reference. Module header reframed accordingly: now 'demos for the combinator that lives in Pipit.Source' rather than 'experiment for the combinator'. make plugin-test still green.
The two source-side demos (eg_opaque and eg_opaque_in_rec) become plain stream-typed bindings under #lang-pipit -- dropping the manual [@@source_mode (ModeFun Stream true Stream)] annotations and the %splice[] (PPL.lift_ast_tac1 "...") calls in favour of automatic lifting. The Demo 2 'rec' (fun acc -> ...)' shape also becomes a natural 'let rec acc = ... in acc'. The [@@core_of_source ...] discharge wrapper (eg_opaque_check) stays in plain F* style: its signature talks about core PXB.exp / PPS.table / PSSB.shallow, which is outside #lang-pipit's rewriting scope and is exactly the layer this test is meant to exercise. The wrapper references eg_opaque_core (generated by the autolift) by name, same as before -- only the surface-side generation moves from explicit %splice to implicit. Unused module aliases PPI / PPL dropped. Header / Demo 2 comment text updated to mention 'recursive binding' rather than 'rec'' and to flag that the surface uses #lang-pipit while the discharge wrapper stays plain. Builds + verifies the same as before; no behavioural change.
Rename Plugin.Test.Core.Lemma -> Plugin.Test.Source.Lemma and drop the manual [@@core_of_source] discharge wrapper. - Demo 1 (eg_opaque): [@@proof_induct1] auto-discharges the marker-routed obligation. No more manual norm_full / bless plumbing. - Demo 2 (eg_opaque_no_pattern, new): [@@proof_induct1; proof_expect_failure] negative control. Same body as Demo 1 without the lemma_pattern call; proves the marker really is what's pulling the SMTPat into the obligation. - Demo 3 (eg_opaque_in_rec): graduates from no-discharge to [@@proof_induct1]. Surprising-but-good finding: the recursive shape with the marker on the recursive variable IS 1-inductive, because the lifted obligation puts 'prev >= 0' in the per-step hypothesis and the SMTPat fires directly. Findings section updated to reflect this.
- Replace the \u2026-laden 'intended shape' schema in the lemma_pattern doc comment with a concrete pow2 monotonicity example. The shape is the same (irreducible marker + paired Lemma [SMTPat ...] + lemma_pattern (marker ...) inside the body), just instantiated with a recognisable lemma so readers don't have to fill in the blanks. - Mark check_pattern and check_pattern_true 'private'. Both are implementation detail of the lemma_pattern encoding; only lemma_pattern itself needs to be visible to client modules. The SMTPat axiom on check_pattern_true still fires from clients because private only restricts name resolution, not SMT context. Verified: Plugin.Test.Source.Lemma still verifies (all three demos: positive, no-pattern proof_expect_failure, recursive).
Consolidate the source-FQN -> core-binding lookup into a single helper, find_core_for_source in Pipit.Source.Ast.Util. Both Pipit.Source.Ast.Lower (caller-side lifting) and Pipit.Plugin.Extract (extraction entry) now delegate to it instead of munging names with a _core suffix or scanning for core_lifted sigelts separately. The dispatch keys off [@@core_of_source nm _] and picks the most recently defined match. F*'s attribute table cons'es each new sigelt to the front of Ref.lookup_attr, so List.hd is the latest binding, mirroring the usual 'later definition wins' convention. Wrappers (e.g. body_contract, __check_<id>) emitted after the raw <id>_core splice therefore win automatically, with no extra tagging needed. Wrappers must carry [@@core_lifted] so Pipit.Tactics.norm_full can unfold them when callers' induction proofs walk in. Tag the plugin-synthesised __check_<id> binding (mk_check_induct1_decl) so caller-side proof_induct1 keeps working when a sibling wrapper overrides the dispatch. Pipit.Exp.Checked.Base gains a bless_contract term-builder; the companion in Checked.Compound delegates to it so the two stay in sync. New Plugin.Test.Core.Contract demonstrates the wiring end-to-end with a hand-written body_contract wrapper plus good_caller / bad_caller (the latter using proof_expect_failure to confirm the rely violation is caught).
Adds a new Pipit.Plugin.Interface attribute
proof_contract (`%rely) (`%guar)
that, when placed on a body's let-binding alongside [@@source_mode],
asks the preprocessor to splice an <id>_contract wrapper after the
<id>_core splice. The wrapper bundles rely_core, guar_core, body_core
via Pipit.Exp.Checked.Base.bless_contract and discharges
induct1 (system_of_contract r g b) by norm_full.
Implementation:
* Pipit_Plugin_Attributes adds a Contract { rely; guar } variant
to attr_proof_method, plus parse_proof_contract that extracts
the two vquoted idents (`%nm parses as VQuote (Var nm)).
* Pipit_Plugin_Preprocess gains mk_contract_decl, mirroring
mk_check_induct1_decl: arity-polymorphic, tagged
[@@core_of_source (`%<id>) <mode>; core_lifted] so the
latest-wins dispatch in Pipit.Source.Ast.Util routes callers
through it automatically.
* Pipit_Plugin_Support exports system_of_contract_lid,
bless_contract_lid, core_lifted_lid.
Because the wrapper references rely_core / guar_core by their splice
names, the rely and guar source bindings must precede the body in
source order; Plugin.Test.Core.Contract is rearranged accordingly and
its hand-written body_contract block deleted.
…tract
In a #lang-pipit module, a function whose return type is
Stream ret (requires R) (ensures fun r -> G)
is now rewritten by the preprocessor into three plain stream bindings
plus the `proof_contract` attribute already understood by the existing
contract-assembly machinery:
let f_rely (...): stream bool = R
let f_guar (...) (r: stream ret): stream bool = G
[@@proof_contract (`%f_rely) (`%f_guar)]
let f (...): ret = body
The rely and guar decls are emitted before the body so the synthesised
`f_contract` wrapper can reference `f_rely_core` / `f_guar_core` by
name. Only the top-level return type is desugared; uses of `Stream`
anywhere else are left for F* to reject as a misuse of the mode
constructor.
`Plugin.Test.Source.Contract` exercises the desugar end-to-end
(positive caller + proof_expect_failure negative caller), mirroring
the hand-written `Plugin.Test.Core.Contract`.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.