aver/codegen/lean/tactic_ir.rs
1//! Structured Lean tactic-combinator tree — the proof-output substrate.
2//!
3//! Auto-proofs are assembled today as raw `first | (…) | (…) | sorry` STRINGS
4//! (`AutoProof.proof_lines`). Every rung KNOWS its portfolio of alternatives,
5//! then immediately flattens it to a string — which forces any later
6//! proof-output pass (`--minimize`, marker instrumentation, `--explain`) to
7//! re-parse the multi-line, nested Lean it just produced. That round-trip is
8//! the brittleness.
9//!
10//! This thin tree keeps the CONTROL structure — sequencing, `first`
11//! alternation, induction arms — first-class. Leaves stay opaque tactic text
12//! (`simp only […] <;> omega`, `grind […]; done`, `exact …`): we model how a
13//! proof is *assembled*, not Lean's tactic semantics. With the structure
14//! retained, `--minimize` collapses a [`Tactic::First`] to its winning branch
15//! STRUCTURALLY (pick a child, re-print), never by text surgery; the only thing
16//! that still has to consult Lean is *which* branch won — and that is one
17//! instrumented `lake build`, not a parser.
18// Foundation module: the type + printer land first, then the ~18 `first | …`
19// emit sites migrate onto it and `--minimize` consumes it. Allow dead_code
20// until those consumers are wired (next slice).
21#![allow(dead_code)]
22
23use std::collections::BTreeMap;
24
25/// A Lean tactic, modelled at the control level only.
26#[derive(Debug, Clone, PartialEq, Eq)]
27pub enum Tactic {
28 /// One opaque tactic. May contain `;` / `<;>` internally — not modelled.
29 Leaf(String),
30 /// The `sorry` floor — rendered bare (`sorry`), never parenthesised.
31 Sorry,
32 /// A `by`-block sequence: each step rendered on its own line, in order.
33 Seq(Vec<Tactic>),
34 /// `first | b₁ | b₂ | …` — the portfolio a minimizer collapses to one
35 /// branch. Lean commits to the leftmost branch that closes, so the winner
36 /// reported by the marker build is exactly the branch to keep.
37 First(Vec<Tactic>),
38 /// `induction <target> with` + one arm per variant. Arm bodies are
39 /// themselves tactics (they routinely contain their own [`Tactic::First`]).
40 Induction {
41 target: String,
42 arms: Vec<InductionArm>,
43 },
44}
45
46/// One `| <pattern> => <body>` arm of an [`Tactic::Induction`].
47#[derive(Debug, Clone, PartialEq, Eq)]
48pub struct InductionArm {
49 /// The pattern after `|` and before `=>`, e.g. `nil` or `cons head tail ih`.
50 pub pattern: String,
51 pub body: Tactic,
52}
53
54impl Tactic {
55 /// Wrap already-rendered proof lines as an opaque sequence — the
56 /// behavior-preserving bridge for proofs not yet structured into `First`
57 /// nodes. `raw(lines).render() == lines`, so migrating a site to
58 /// `body: Tactic::raw(<old proof_lines>)` is a no-op on the emitted Lean;
59 /// only the portfolio sites that later become real [`Tactic::First`] trees
60 /// gain anything for `--minimize`.
61 pub fn raw(lines: Vec<String>) -> Tactic {
62 Tactic::Seq(lines.into_iter().map(Tactic::Leaf).collect())
63 }
64
65 /// Like [`raw`](Self::raw) but first strips the lines' common leading
66 /// indent (keeping relative nesting). Use when wrapping already-rendered
67 /// lines as a [`Tactic::First`] BRANCH: a branch is re-based under its `| (`
68 /// at render time, and when `--minimize` collapses the portfolio the branch
69 /// is promoted flush with its new siblings — both want it authored at its
70 /// own zero indent, not carrying the caller's baked 2-space.
71 pub fn raw_dedented(lines: Vec<String>) -> Tactic {
72 Tactic::raw(relative_dedent(&lines))
73 }
74
75 /// Render to the proof-body lines that follow `:= by` (the caller supplies
76 /// the theorem-level indent when it stitches these into the file). Produces
77 /// valid Lean; formatting is normalised (it need not be byte-identical to
78 /// the legacy string emit — the contract is that the proof still closes).
79 pub fn render(&self) -> Vec<String> {
80 self.render_indent(0)
81 }
82
83 /// Render the proof body as it sits under a theorem's `:= by` — at the
84 /// canonical 2-space indent.
85 ///
86 /// `raw`-migrated bodies carry a baked-in leading indent in their leaf
87 /// strings (the legacy emit indented every proof line by 2). Re-indenting
88 /// that on top would double it, so this first strips the tree's common
89 /// leaf indent (preserving any deeper *relative* nesting) and then renders
90 /// at indent 1. For a uniformly 2-space-baked body that is byte-identical
91 /// to the legacy output; for a structured body (a real [`Tactic::First`]
92 /// authored without baked indent) it lays the `first`/`|` keywords at the
93 /// 2-space column the surrounding `intro` sits at — which Lean's
94 /// column-sensitive `by` block requires.
95 pub fn render_body(&self) -> Vec<String> {
96 // Under an active `--minimize` pass (thread-local, set by `cmd_proof`),
97 // rewrite the tree first: Instrument prefixes each `First` branch with a
98 // winner-probe marker; Collapse drops each `First` to its proven winner.
99 // Outside a minimize pass this is a no-op clone.
100 let tree = minimize::apply(self);
101 let strip = tree.leaf_min_indent().unwrap_or(0);
102 tree.strip_leaf_indent(strip).render_indent(1)
103 }
104
105 /// The smallest leading-space count across every non-blank line of every
106 /// leaf in the tree (`None` if the tree has no non-blank leaf line).
107 /// Structural keywords (`first`, `| …`, `induction … with`) are NOT leaves
108 /// and do not count — only authored tactic text does.
109 fn leaf_min_indent(&self) -> Option<usize> {
110 match self {
111 Tactic::Leaf(s) => s
112 .lines()
113 .filter(|l| !l.trim().is_empty())
114 .map(leading_spaces)
115 .min(),
116 Tactic::Sorry => None,
117 Tactic::Seq(ts) | Tactic::First(ts) => {
118 ts.iter().filter_map(Tactic::leaf_min_indent).min()
119 }
120 Tactic::Induction { arms, .. } => {
121 arms.iter().filter_map(|a| a.body.leaf_min_indent()).min()
122 }
123 }
124 }
125
126 /// Strip up to `n` leading spaces from every line of every leaf — the
127 /// un-bake step paired with [`render_body`]. Clamped per line so a line
128 /// shallower than `n` is left flush, never over-stripped into its content.
129 fn strip_leaf_indent(self, n: usize) -> Tactic {
130 match self {
131 Tactic::Leaf(s) => Tactic::Leaf(
132 s.lines()
133 .map(|l| {
134 let k = leading_spaces(l).min(n);
135 l[k..].to_string()
136 })
137 .collect::<Vec<_>>()
138 .join("\n"),
139 ),
140 Tactic::Sorry => Tactic::Sorry,
141 Tactic::Seq(ts) => {
142 Tactic::Seq(ts.into_iter().map(|t| t.strip_leaf_indent(n)).collect())
143 }
144 Tactic::First(ts) => {
145 Tactic::First(ts.into_iter().map(|t| t.strip_leaf_indent(n)).collect())
146 }
147 Tactic::Induction { target, arms } => Tactic::Induction {
148 target,
149 arms: arms
150 .into_iter()
151 .map(|a| InductionArm {
152 pattern: a.pattern,
153 body: a.body.strip_leaf_indent(n),
154 })
155 .collect(),
156 },
157 }
158 }
159
160 fn render_indent(&self, indent: usize) -> Vec<String> {
161 let pad = " ".repeat(indent);
162 match self {
163 // An empty leaf stays a truly empty line — never padded. (A
164 // `String::new()` step in a `raw`-wrapped proof is a blank
165 // separator; emitting `pad` instead would leave trailing
166 // whitespace and break byte-identity when rendered at depth.)
167 Tactic::Leaf(s) if s.is_empty() => vec![String::new()],
168 // Preserve an empty leaf as an empty line (`"".lines()` yields
169 // NOTHING, which would silently drop blank lines from `raw`-wrapped
170 // proofs); only split a genuinely multi-line leaf.
171 Tactic::Leaf(s) if !s.contains('\n') => vec![format!("{pad}{s}")],
172 Tactic::Leaf(s) => s.lines().map(|l| format!("{pad}{l}")).collect(),
173 Tactic::Sorry => vec![format!("{pad}sorry")],
174 Tactic::Seq(steps) => steps.iter().flat_map(|t| t.render_indent(indent)).collect(),
175 Tactic::First(branches) => render_first(branches, indent),
176 Tactic::Induction { target, arms } => {
177 let mut out = vec![format!("{pad}induction {target} with")];
178 for arm in arms {
179 // `| pat =>` then the body inline if single-line, else the
180 // body indented under the arm.
181 let body = arm.body.render_indent(indent + 1);
182 if body.len() == 1 {
183 out.push(format!(
184 "{pad}| {} => {}",
185 arm.pattern,
186 body[0].trim_start()
187 ));
188 } else {
189 out.push(format!("{pad}| {} =>", arm.pattern));
190 out.extend(body);
191 }
192 }
193 out
194 }
195 }
196 }
197
198 /// The `--minimize` primitive: walk the tree, and for each [`Tactic::First`]
199 /// ask `pick` which branch won (by the branch list); `Some(i)` collapses the
200 /// portfolio to branch `i` (recursively minimized), `None` keeps it intact.
201 /// `pick` is fed the [`Tactic::First`] nodes in pre-order, so a marker pass
202 /// that numbered them in the same order can answer by index.
203 pub fn collapse_firsts(self, pick: &mut impl FnMut(&[Tactic]) -> Option<usize>) -> Tactic {
204 match self {
205 leaf @ (Tactic::Leaf(_) | Tactic::Sorry) => leaf,
206 Tactic::Seq(steps) => {
207 Tactic::Seq(steps.into_iter().map(|t| t.collapse_firsts(pick)).collect())
208 }
209 Tactic::First(branches) => match pick(&branches) {
210 Some(i) if i < branches.len() => {
211 branches.into_iter().nth(i).unwrap().collapse_firsts(pick)
212 }
213 _ => Tactic::First(
214 branches
215 .into_iter()
216 .map(|t| t.collapse_firsts(pick))
217 .collect(),
218 ),
219 },
220 Tactic::Induction { target, arms } => Tactic::Induction {
221 target,
222 arms: arms
223 .into_iter()
224 .map(|a| InductionArm {
225 pattern: a.pattern,
226 body: a.body.collapse_firsts(pick),
227 })
228 .collect(),
229 },
230 }
231 }
232
233 /// Count of [`Tactic::First`] nodes, in pre-order — the number of marker
234 /// sites the instrument pass will emit and the winner pass will read back.
235 pub fn first_count(&self) -> usize {
236 match self {
237 Tactic::Leaf(_) | Tactic::Sorry => 0,
238 Tactic::Seq(ts) => ts.iter().map(Tactic::first_count).sum(),
239 Tactic::First(bs) => 1 + bs.iter().map(Tactic::first_count).sum::<usize>(),
240 Tactic::Induction { arms, .. } => arms.iter().map(|a| a.body.first_count()).sum(),
241 }
242 }
243
244 /// Instrument every [`Tactic::First`] for the `--minimize` winner probe:
245 /// prefix each branch with a `trace "AVERMIN:<idx>:<b>"` marker, where
246 /// `<idx>` is the node's global pre-order index (drawn from `next`) and
247 /// `<b>` is the branch position. Lean's `first` runs branches left-to-right
248 /// and commits to the first that closes, tracing each it tries — so after
249 /// one instrumented `lake build` the WINNING branch of node `idx` is the
250 /// MAX `<b>` that surfaced (failed branches trace too; they are not rolled
251 /// back). Indices are assigned by a pure structural walk so this pass and
252 /// [`collapse_by_index`](Self::collapse_by_index) agree node-for-node.
253 fn instrument_markers(self, next: &mut usize) -> Tactic {
254 match self {
255 leaf @ (Tactic::Leaf(_) | Tactic::Sorry) => leaf,
256 Tactic::Seq(ts) => {
257 Tactic::Seq(ts.into_iter().map(|t| t.instrument_markers(next)).collect())
258 }
259 Tactic::First(branches) => {
260 let idx = *next;
261 *next += 1;
262 Tactic::First(
263 branches
264 .into_iter()
265 .enumerate()
266 .map(|(b, branch)| {
267 // Recurse before prepending the marker so nested
268 // `First`s take indices AFTER this node (pre-order).
269 let inner = branch.instrument_markers(next);
270 Tactic::Seq(vec![
271 Tactic::Leaf(format!("trace \"AVERMIN:{idx}:{b}\"")),
272 inner,
273 ])
274 })
275 .collect(),
276 )
277 }
278 Tactic::Induction { target, arms } => Tactic::Induction {
279 target,
280 arms: arms
281 .into_iter()
282 .map(|a| InductionArm {
283 pattern: a.pattern,
284 body: a.body.instrument_markers(next),
285 })
286 .collect(),
287 },
288 }
289 }
290
291 /// Collapse each [`Tactic::First`] to its winning branch per `winners`
292 /// (keyed by the SAME global pre-order index
293 /// [`instrument_markers`](Self::instrument_markers) assigned). A node absent
294 /// from the map — never executed in the probe build, so no marker surfaced —
295 /// is left intact. Walks ALL branches even when collapsing, so `next`
296 /// advances exactly as in the instrument pass and downstream indices stay
297 /// aligned; only the chosen branch's rewrite is kept.
298 fn collapse_by_index(self, next: &mut usize, winners: &BTreeMap<usize, usize>) -> Tactic {
299 match self {
300 leaf @ (Tactic::Leaf(_) | Tactic::Sorry) => leaf,
301 Tactic::Seq(ts) => Tactic::Seq(
302 ts.into_iter()
303 .map(|t| t.collapse_by_index(next, winners))
304 .collect(),
305 ),
306 Tactic::First(branches) => {
307 let idx = *next;
308 *next += 1;
309 // An out-of-range winner (should never happen) degrades to
310 // "keep the whole portfolio" rather than dropping every branch.
311 let n = branches.len();
312 let winner = winners.get(&idx).copied().filter(|&w| w < n);
313 let mut chosen = None;
314 let mut kept: Vec<Tactic> = Vec::with_capacity(branches.len());
315 for (b, branch) in branches.into_iter().enumerate() {
316 let collapsed = branch.collapse_by_index(next, winners);
317 match winner {
318 Some(w) if w == b => chosen = Some(collapsed),
319 Some(_) => {}
320 None => kept.push(collapsed),
321 }
322 }
323 match chosen {
324 Some(t) => t,
325 None => Tactic::First(kept),
326 }
327 }
328 Tactic::Induction { target, arms } => Tactic::Induction {
329 target,
330 arms: arms
331 .into_iter()
332 .map(|a| InductionArm {
333 pattern: a.pattern,
334 body: a.body.collapse_by_index(next, winners),
335 })
336 .collect(),
337 },
338 }
339 }
340}
341
342/// Count of leading ASCII spaces on a line.
343fn leading_spaces(l: &str) -> usize {
344 l.len() - l.trim_start().len()
345}
346
347/// Strip the common leading indent shared by all non-blank lines, preserving
348/// each line's *relative* nesting (blank lines stay blank). Used to re-base a
349/// multi-line `first` branch under its `| (` wrapper without flattening the
350/// branch's own internal structure (an `induction`/`cases` ladder).
351fn relative_dedent(lines: &[String]) -> Vec<String> {
352 let min = lines
353 .iter()
354 .filter(|l| !l.trim().is_empty())
355 .map(|l| leading_spaces(l))
356 .min()
357 .unwrap_or(0);
358 lines
359 .iter()
360 .map(|l| {
361 if l.trim().is_empty() {
362 String::new()
363 } else {
364 l[min..].to_string()
365 }
366 })
367 .collect()
368}
369
370/// Render a `First`: inline (`first | (b₀) | (b₁) | sorry`) when every branch is
371/// a single line, else multi-line with each branch on its own `|` line.
372fn render_first(branches: &[Tactic], indent: usize) -> Vec<String> {
373 let pad = " ".repeat(indent);
374 let rendered: Vec<Vec<String>> = branches.iter().map(|b| b.render_indent(0)).collect();
375 let all_single = rendered.iter().all(|b| b.len() == 1);
376 if all_single {
377 let parts: Vec<String> = branches
378 .iter()
379 .zip(&rendered)
380 .map(|(b, lines)| match b {
381 Tactic::Sorry => "sorry".to_string(),
382 _ => format!("({})", lines[0].trim_start()),
383 })
384 .collect();
385 vec![format!("{pad}first | {}", parts.join(" | "))]
386 } else {
387 let mut out = vec![format!("{pad}first")];
388 for (b, lines) in branches.iter().zip(&rendered) {
389 match b {
390 Tactic::Sorry => out.push(format!("{pad}| sorry")),
391 _ if lines.len() == 1 => out.push(format!("{pad}| ({})", lines[0].trim_start())),
392 _ => {
393 out.push(format!("{pad}| ("));
394 // Re-base the branch relative to `| (`, keeping its own
395 // internal nesting (trimming each line would flatten an
396 // induction ladder inside the branch).
397 for l in relative_dedent(lines) {
398 if l.is_empty() {
399 out.push(String::new());
400 } else {
401 out.push(format!("{pad} {l}"));
402 }
403 }
404 out.push(format!("{pad})"));
405 }
406 }
407 }
408 out
409 }
410}
411
412/// The `--minimize` driver state, thread-local so the two re-emit passes
413/// (instrument, then collapse) can steer [`Tactic::render_body`] without
414/// threading a mode + counter through every codegen signature. Codegen runs
415/// single-threaded per `transpile`, and a normal `aver proof` never enters a
416/// pass, so the default ([`Mode::Off`]) leaves emission untouched.
417pub mod minimize {
418 use super::{BTreeMap, Tactic};
419 use std::cell::RefCell;
420
421 #[derive(Clone)]
422 enum Mode {
423 Off,
424 Instrument,
425 Collapse(BTreeMap<usize, usize>),
426 }
427
428 thread_local! {
429 // (mode, global pre-order `First` counter advanced across all bodies).
430 static STATE: RefCell<(Mode, usize)> = const { RefCell::new((Mode::Off, 0)) };
431 }
432
433 /// Enter the instrument pass: emit winner-probe markers, counter reset to 0.
434 pub fn begin_instrument() {
435 STATE.with(|s| *s.borrow_mut() = (Mode::Instrument, 0));
436 }
437
438 /// Enter the collapse pass with the parsed winners, counter reset to 0.
439 pub fn begin_collapse(winners: BTreeMap<usize, usize>) {
440 STATE.with(|s| *s.borrow_mut() = (Mode::Collapse(winners), 0));
441 }
442
443 /// Leave the minimize pass — emission returns to byte-for-byte normal.
444 pub fn end() {
445 STATE.with(|s| *s.borrow_mut() = (Mode::Off, 0));
446 }
447
448 /// Apply the active pass's rewrite to `t`, advancing the shared counter.
449 /// Returns a plain clone when no pass is active.
450 pub(super) fn apply(t: &Tactic) -> Tactic {
451 STATE.with(|s| {
452 let mut st = s.borrow_mut();
453 let mode = st.0.clone();
454 let mut counter = st.1;
455 let out = match mode {
456 Mode::Off => t.clone(),
457 Mode::Instrument => t.clone().instrument_markers(&mut counter),
458 Mode::Collapse(winners) => t.clone().collapse_by_index(&mut counter, &winners),
459 };
460 st.1 = counter;
461 out
462 })
463 }
464
465 /// Parse the winning branch of every instrumented `First` from a `lake
466 /// build` log. Markers surface as `… AVERMIN:<idx>:<branch>`; `first` traces
467 /// every branch it tries and stops at the first that closes, so the winner
468 /// of node `idx` is the MAXIMUM branch index seen for it.
469 pub fn parse_winners(build_output: &str) -> BTreeMap<usize, usize> {
470 let mut winners: BTreeMap<usize, usize> = BTreeMap::new();
471 for line in build_output.lines() {
472 let Some(pos) = line.find("AVERMIN:") else {
473 continue;
474 };
475 let rest = &line[pos + "AVERMIN:".len()..];
476 let mut it = rest.split(|c: char| !c.is_ascii_digit());
477 let (Some(i), Some(b)) = (it.next(), it.next()) else {
478 continue;
479 };
480 let (Ok(idx), Ok(branch)) = (i.parse::<usize>(), b.parse::<usize>()) else {
481 continue;
482 };
483 let e = winners.entry(idx).or_insert(branch);
484 *e = (*e).max(branch);
485 }
486 winners
487 }
488}
489
490/// The speculative-universal driver state — the "try-universal,
491/// fall-back-to-sampled" mechanism for SINGLE-LIST conditional laws (the Gap-1
492/// statement-form decision layer; analog of [`minimize`] but choosing the
493/// theorem's STATEMENT FORM, not collapsing a tactic portfolio).
494///
495/// A single-list `when`-law (zero partner lists — sortedness, the
496/// per-element-fold-with-Bool-fold-premise shape, json roundtrips) cannot be
497/// statically classified as "the generic conditional driver will close it
498/// universally": the shapes are too diverse. So the decision is made
499/// EMPIRICALLY by a probe build, exactly as `--minimize` learns the winning
500/// branch from one instrumented build:
501/// - [`begin_probe`] makes [`admits`] return `true` for EVERY such law (so the
502/// probe emit states each universally, floored with an `AVERSPEC_SORRY:<id>`
503/// trace) and records the admitted `fn.law` ids in a sink.
504/// - one `lake build` runs; a law whose portfolio fell through to the trace
505/// floor (didn't close) surfaces its id in the build log (see
506/// [`parse_failures`]).
507/// - [`set_committed`] is then given `probed − failures` (the laws that
508/// CLOSED). In the committed (Off) mode [`admits`] returns `true` only for
509/// that set, so the re-emit states the closed laws universally and the rest
510/// fall back to their sound bounded sampled-domain statement.
511///
512/// `COMMITTED` PERSISTS across the commit re-emit, any `--minimize` re-emit, and
513/// the final `--check` build (the recognizer is the single source of truth for
514/// the statement form, the `omit_domain` driver, the class marker, AND the proof
515/// emit — all keyed on [`admits`], so they always agree). The default state
516/// (`Off` + `COMMITTED = None`) admits nothing, leaving single-list conditionals
517/// on their current bounded fallback — byte-identical to before this mechanism.
518pub mod speculative {
519 use std::cell::RefCell;
520 use std::collections::HashSet;
521
522 #[derive(Clone, PartialEq)]
523 enum Mode {
524 Off,
525 Probe,
526 }
527
528 thread_local! {
529 // (mode, committed `fn.law` ids admitted in Off mode, probe sink).
530 static STATE: RefCell<(Mode, Option<HashSet<String>>, HashSet<String>)> =
531 RefCell::new((Mode::Off, None, HashSet::new()));
532 }
533
534 /// Enter the probe pass: [`admits`] returns `true` for every single-list
535 /// candidate (and records it), so the emit states each universally with an
536 /// `AVERSPEC_SORRY` trace floor. Clears the probe sink.
537 pub fn begin_probe() {
538 STATE.with(|s| {
539 let mut st = s.borrow_mut();
540 st.0 = Mode::Probe;
541 st.2 = HashSet::new();
542 });
543 }
544
545 /// Commit the empirically-determined set of laws that CLOSED universally:
546 /// switch to Off mode where [`admits`] returns `true` only for `closed`.
547 /// Persists through subsequent re-emits and the `--check` build.
548 pub fn set_committed(closed: HashSet<String>) {
549 STATE.with(|s| {
550 let mut st = s.borrow_mut();
551 st.0 = Mode::Off;
552 st.1 = Some(closed);
553 });
554 }
555
556 /// Full reset to the default (admit nothing) — the fail-safe path and the
557 /// no-candidate skip both restore byte-identical baseline emission.
558 pub fn clear() {
559 STATE.with(|s| *s.borrow_mut() = (Mode::Off, None, HashSet::new()));
560 }
561
562 /// Whether a conditional law with this `fn.law` id should be stated
563 /// universally. In probe mode: always (the probe attempts every structurally
564 /// eligible candidate). In Off mode WITH a committed set: only if it closed
565 /// (`set.contains(id)`). In Off mode with NO committed set (a direct
566 /// `transpile` outside any probe — a unit test, or the CLI's pre-probe
567 /// baseline): fall back to `default`. `default` is the law's PRE-probe
568 /// disposition — two-list conditionals were attempted directly (default
569 /// `true`), single-list ones declined to bounded (default `false`) — so a
570 /// no-probe emission stays byte-compatible with the pre-probe behavior, while
571 /// a probe-then-commit run lets the empirical result override it (promoting a
572 /// single-list closer, DEMOTING a two-list non-closer like `prop_42`). Pure —
573 /// does NOT record; the probe sink is populated at the floor-emission site
574 /// (see [`record_probed`]) so it counts only laws that emit a trace floor.
575 pub fn admits(id: &str, default: bool) -> bool {
576 STATE.with(|s| {
577 let st = s.borrow();
578 match st.0 {
579 Mode::Probe => true,
580 Mode::Off => match st.1.as_ref() {
581 Some(set) => set.contains(id),
582 None => default,
583 },
584 }
585 })
586 }
587
588 /// Whether a probe pass is active — the emit reads this to floor each
589 /// speculative portfolio with the `AVERSPEC_SORRY:<id>` trace instead of a
590 /// bare `sorry`, so a non-closing law is observable in the build log.
591 pub fn probing() -> bool {
592 STATE.with(|s| s.borrow().0 == Mode::Probe)
593 }
594
595 /// Record that this law actually EMITTED an `AVERSPEC_SORRY` trace floor in
596 /// the probe — i.e. its universal `∀`-theorem was emitted (not suppressed by
597 /// `skip_universal`) and can surface a failure. `closed = probed_ids −
598 /// parse_failures`, so the sink must hold exactly the laws that can trace,
599 /// never one whose theorem was dropped (which would never trace and be
600 /// miscounted "closed"). Called only under [`probing`].
601 pub fn record_probed(id: &str) {
602 STATE.with(|s| {
603 s.borrow_mut().2.insert(id.to_string());
604 });
605 }
606
607 /// The `fn.law` ids that emitted a probe trace floor (single-list candidates
608 /// whose universal `∀`-theorem was actually emitted). `closed = probed_ids −
609 /// parse_failures`.
610 pub fn probed_ids() -> HashSet<String> {
611 STATE.with(|s| s.borrow().2.clone())
612 }
613
614 /// Parse the `fn.law` ids whose speculative portfolio fell through to its
615 /// `AVERSPEC_SORRY:<id>` trace floor (did NOT close) from a `lake build` log.
616 /// `first` commits to the leftmost closing branch and never runs a later
617 /// branch's trace, so the marker surfaces IFF the portfolio reached its
618 /// sorry floor — a direct "this law did not close", no warning-location
619 /// mapping or separate `#print axioms` run required.
620 pub fn parse_failures(build_output: &str) -> HashSet<String> {
621 const MARKER: &str = "AVERSPEC_SORRY:";
622 let mut failed = HashSet::new();
623 for line in build_output.lines() {
624 let Some(pos) = line.find(MARKER) else {
625 continue;
626 };
627 let rest = &line[pos + MARKER.len()..];
628 let id: String = rest
629 .chars()
630 .take_while(|c| c.is_alphanumeric() || *c == '_' || *c == '.')
631 .collect();
632 if !id.is_empty() {
633 failed.insert(id);
634 }
635 }
636 failed
637 }
638}
639
640#[cfg(test)]
641mod tests {
642 use super::*;
643
644 fn leaf(s: &str) -> Tactic {
645 Tactic::Leaf(s.to_string())
646 }
647
648 #[test]
649 fn renders_flat_portfolio_inline_with_bare_sorry() {
650 // The String-length-additivity rung shape.
651 let t = Tactic::Seq(vec![
652 leaf("intro a b"),
653 Tactic::First(vec![
654 leaf("simp only [String.add_eq_append, String.length_append] <;> omega"),
655 Tactic::Sorry,
656 ]),
657 ]);
658 assert_eq!(
659 t.render(),
660 vec![
661 "intro a b".to_string(),
662 "first | (simp only [String.add_eq_append, String.length_append] <;> omega) | sorry"
663 .to_string(),
664 ]
665 );
666 }
667
668 #[test]
669 fn renders_grind_wrapped_two_level_portfolio() {
670 // The 2-level grind-wrap: `first | (grind…) | (<inner first>)`.
671 let inner = Tactic::First(vec![
672 leaf("exact AverMap.len_set_ge_one _ _ _"),
673 Tactic::Sorry,
674 ]);
675 let t = Tactic::Seq(vec![
676 leaf("intro m k v"),
677 Tactic::First(vec![leaf("grind [_root_.after]; done"), inner]),
678 ]);
679 // Both branches are single-line, so the whole thing is inline.
680 assert_eq!(
681 t.render(),
682 vec![
683 "intro m k v".to_string(),
684 "first | (grind [_root_.after]; done) | (first | (exact AverMap.len_set_ge_one _ _ _) | sorry)".to_string(),
685 ]
686 );
687 }
688
689 #[test]
690 fn renders_induction_arms() {
691 let t = Tactic::Seq(vec![
692 leaf("intro xs"),
693 Tactic::Induction {
694 target: "xs".to_string(),
695 arms: vec![
696 InductionArm {
697 pattern: "nil".to_string(),
698 body: Tactic::First(vec![leaf("simp [f]"), Tactic::Sorry]),
699 },
700 InductionArm {
701 pattern: "cons h t ih".to_string(),
702 body: leaf("simp_all [f]"),
703 },
704 ],
705 },
706 ]);
707 assert_eq!(
708 t.render(),
709 vec![
710 "intro xs".to_string(),
711 "induction xs with".to_string(),
712 "| nil => first | (simp [f]) | sorry".to_string(),
713 "| cons h t ih => simp_all [f]".to_string(),
714 ]
715 );
716 }
717
718 #[test]
719 fn first_count_is_preorder_total() {
720 let t = Tactic::Seq(vec![
721 Tactic::First(vec![leaf("a"), Tactic::Sorry]),
722 Tactic::Induction {
723 target: "xs".to_string(),
724 arms: vec![InductionArm {
725 pattern: "cons h t".to_string(),
726 body: Tactic::First(vec![leaf("b"), leaf("c")]),
727 }],
728 },
729 ]);
730 assert_eq!(t.first_count(), 2);
731 }
732
733 #[test]
734 fn render_body_is_byte_identical_for_baked_raw() {
735 // A `raw`-migrated body carries the legacy baked 2-space indent (with a
736 // deeper 4-space continuation). `render_body` strips the common 2 and
737 // re-adds it at indent 1 — reproducing the exact legacy lines.
738 let baked = vec![
739 " intro xs".to_string(),
740 " induction xs with".to_string(),
741 " | nil => simp".to_string(),
742 " | cons h t ih =>".to_string(),
743 " simp [ih]".to_string(),
744 ];
745 let body = Tactic::raw(baked.clone());
746 assert_eq!(body.render_body(), baked);
747 }
748
749 #[test]
750 fn render_body_lays_out_grind_wrapped_first_at_two_space() {
751 // The grind-wrap shape: un-baked intro + `First`, the body branch a
752 // baked multi-line `raw`. `render_body` must put `first`/`|` at the
753 // 2-space column (matching `intro`) and re-base the body branch under
754 // `| (` without flattening it.
755 let body = Tactic::Seq(vec![
756 leaf("intro a b"),
757 Tactic::First(vec![
758 leaf("grind [f]; done"),
759 Tactic::raw(vec![
760 " simp [f]".to_string(),
761 " omega".to_string(),
762 " sorry".to_string(),
763 ]),
764 ]),
765 ]);
766 assert_eq!(
767 body.render_body(),
768 vec![
769 " intro a b".to_string(),
770 " first".to_string(),
771 " | (grind [f]; done)".to_string(),
772 " | (".to_string(),
773 " simp [f]".to_string(),
774 " omega".to_string(),
775 " sorry".to_string(),
776 " )".to_string(),
777 ]
778 );
779 }
780
781 #[test]
782 fn collapse_firsts_picks_the_winning_branch() {
783 // Minimize: pick branch 0 of every First — drops the alternation + sorry.
784 let t = Tactic::Seq(vec![
785 leaf("intro a b"),
786 Tactic::First(vec![
787 leaf("the_winner <;> omega"),
788 leaf("loser"),
789 Tactic::Sorry,
790 ]),
791 ]);
792 let mut pick = |_branches: &[Tactic]| Some(0usize);
793 let minimized = t.collapse_firsts(&mut pick);
794 assert_eq!(
795 minimized.render(),
796 vec!["intro a b".to_string(), "the_winner <;> omega".to_string()]
797 );
798 }
799
800 #[test]
801 fn speculative_parse_failures_reads_fn_law_ids() {
802 // A single-list portfolio that fell through to its floor traces
803 // `AVERSPEC_SORRY:<fn.law>`; one that closed never runs the floor's
804 // trace, so its id is absent. The id allows dots and underscores.
805 let log = "\
806info: F.lean:50:5: AVERSPEC_SORRY:parseArrayElems.renderJsonListElemsRoundtrip
807info: F.lean:62:5: AVERSPEC_SORRY:parseObjFields.renderJsonEntriesFieldsRoundtrip
808warning: declaration uses 'sorry'
809";
810 let failed = super::speculative::parse_failures(log);
811 assert!(failed.contains("parseArrayElems.renderJsonListElemsRoundtrip"));
812 assert!(failed.contains("parseObjFields.renderJsonEntriesFieldsRoundtrip"));
813 assert_eq!(failed.len(), 2);
814 // A closed law (no trace) is not reported failed.
815 assert!(!failed.contains("sumList.sumAllZero"));
816 }
817
818 #[test]
819 fn speculative_admits_only_committed_in_off_mode() {
820 use super::speculative;
821 // No committed set: `admits` returns the law's `default` disposition — a
822 // single-list candidate (default false) stays bounded, a two-list one
823 // (default true) is attempted directly. Byte-compatible with pre-probe.
824 speculative::clear();
825 assert!(!speculative::admits("f.law", false));
826 assert!(speculative::admits("g.two", true));
827 assert!(!speculative::probing());
828 // Probe: admit everything regardless of default; the sink is populated by
829 // `record_probed` at the floor-emission site (not by `admits`).
830 speculative::begin_probe();
831 assert!(speculative::probing());
832 assert!(speculative::admits("f.law", false));
833 assert!(speculative::admits("g.two", true));
834 assert!(speculative::probed_ids().is_empty());
835 speculative::record_probed("f.law");
836 speculative::record_probed("g.two");
837 assert!(speculative::probed_ids().contains("f.law"));
838 // Commit: admit only the closed set, IGNORING default — so a two-list
839 // non-closer (default true) is DEMOTED, a single-list closer promoted.
840 let mut closed = std::collections::HashSet::new();
841 closed.insert("f.law".to_string());
842 speculative::set_committed(closed);
843 assert!(!speculative::probing());
844 assert!(speculative::admits("f.law", false));
845 assert!(!speculative::admits("g.two", true));
846 speculative::clear();
847 assert!(!speculative::admits("f.law", false));
848 }
849
850 #[test]
851 fn parse_winners_takes_max_branch_per_index() {
852 // First 0 traced branches 0 then 1 (1 won); First 1 traced only 0
853 // (0 won); a duplicate re-elaboration line must not change the max.
854 let log = "\
855info: F.lean:3:5: AVERMIN:0:0
856info: F.lean:4:5: AVERMIN:0:1
857info: G.lean:9:5: AVERMIN:1:0
858info: F.lean:4:5: AVERMIN:0:1
859warning: declaration uses 'sorry'
860";
861 let w = minimize::parse_winners(log);
862 assert_eq!(w.get(&0), Some(&1));
863 assert_eq!(w.get(&1), Some(&0));
864 assert_eq!(w.len(), 2);
865 }
866
867 #[test]
868 fn instrument_markers_number_firsts_in_preorder() {
869 // Outer First (idx 0) whose branch 1 holds a nested First (idx 1).
870 let inner = Tactic::First(vec![leaf("a"), Tactic::Sorry]);
871 let t = Tactic::First(vec![leaf("grind; done"), inner]);
872 let mut next = 0;
873 let instrumented = t.instrument_markers(&mut next);
874 assert_eq!(next, 2); // two First nodes numbered
875 let rendered = instrumented.render().join("\n");
876 // Outer node 0: both branches marked; nested node 1: both branches marked.
877 assert!(rendered.contains("AVERMIN:0:0"));
878 assert!(rendered.contains("AVERMIN:0:1"));
879 assert!(rendered.contains("AVERMIN:1:0"));
880 assert!(rendered.contains("AVERMIN:1:1"));
881 }
882
883 #[test]
884 fn collapse_by_index_keeps_winner_and_stays_index_aligned() {
885 // Same shape as the instrument test. Winner of outer (0) is branch 1
886 // (the nested First); winner of nested (1) is branch 0 (`a`).
887 let inner = Tactic::First(vec![leaf("a"), Tactic::Sorry]);
888 let t = Tactic::Seq(vec![
889 leaf("intro x"),
890 Tactic::First(vec![leaf("grind; done"), inner]),
891 ]);
892 let winners = BTreeMap::from([(0usize, 1usize), (1usize, 0usize)]);
893 let mut next = 0;
894 let collapsed = t.collapse_by_index(&mut next, &winners);
895 assert_eq!(next, 2); // walked ALL branches, both Firsts counted
896 assert_eq!(
897 collapsed.render(),
898 vec!["intro x".to_string(), "a".to_string()]
899 );
900 }
901
902 #[test]
903 fn collapse_to_the_sorry_floor_keeps_the_sorry() {
904 // When nothing real closes, `first` falls to its `sorry` floor — the
905 // last branch traced, so the MAX-index winner. Minimize must collapse
906 // to bare `sorry`, never silently drop the honest gap. (Status-
907 // preserving: a sorry proof stays a sorry proof.)
908 let portfolio = || {
909 Tactic::Seq(vec![
910 leaf("intro a b"),
911 Tactic::First(vec![leaf("grind; done"), leaf("simp_all"), Tactic::Sorry]),
912 ])
913 };
914 // The instrumented build reported branch 2 (the sorry floor) as winner.
915 minimize::begin_collapse(BTreeMap::from([(0usize, 2usize)]));
916 let collapsed = portfolio().render_body();
917 minimize::end();
918 assert_eq!(
919 collapsed,
920 vec![" intro a b".to_string(), " sorry".to_string()]
921 );
922 }
923
924 #[test]
925 fn render_body_round_trips_instrument_then_collapse() {
926 // The grind-wrap shape. Instrument emits markers; suppose the probe
927 // build reports the body branch (1) as the winner — collapse drops the
928 // grind arm, leaving just the body.
929 let grind_wrap = || {
930 Tactic::Seq(vec![
931 leaf("intro a b"),
932 Tactic::First(vec![
933 leaf("grind [f]; done"),
934 Tactic::raw_dedented(vec![" simp [f]".to_string(), " sorry".to_string()]),
935 ]),
936 ])
937 };
938
939 minimize::begin_instrument();
940 let instrumented = grind_wrap().render_body().join("\n");
941 minimize::end();
942 assert!(instrumented.contains("AVERMIN:0:0"));
943 assert!(instrumented.contains("AVERMIN:0:1"));
944
945 minimize::begin_collapse(BTreeMap::from([(0usize, 1usize)]));
946 let collapsed = grind_wrap().render_body();
947 minimize::end();
948 assert_eq!(
949 collapsed,
950 vec![
951 " intro a b".to_string(),
952 " simp [f]".to_string(),
953 " sorry".to_string(),
954 ]
955 );
956
957 // Pass ended → emission is byte-for-byte normal again.
958 assert_eq!(
959 grind_wrap().render_body(),
960 vec![
961 " intro a b".to_string(),
962 " first".to_string(),
963 " | (grind [f]; done)".to_string(),
964 " | (".to_string(),
965 " simp [f]".to_string(),
966 " sorry".to_string(),
967 " )".to_string(),
968 ]
969 );
970 }
971}