Enum ProofStrategy 

pub enum ProofStrategy {
    Reflexive,
    SimpOverLemmas(Vec<String>),
    Commutative {
        op: BinOp,
    },
    Associative {
        op: BinOp,
    },
    IdentityElement {
        op: BinOp,
    },
    AntiCommutative {
        op: BinOp,
        neg_on_rhs: bool,
    },
    UnaryEqualsBinary {
        inner_fn: String,
    },
    LinearArithmetic {
        unfold_fns: Vec<String>,
        wrapper_return: bool,
        smart_guard: Option<SmartGuard>,
        lifted: bool,
    },
    Induction {
        param: String,
    },
    LibraryAxiom {
        axiom: String,
        args: Vec<Spanned<ResolvedExpr>>,
    },
    MapUpdatePostcondition {
        outer_fn: String,
        kind: MapUpdatePostconditionKind,
        map_arg: Spanned<ResolvedExpr>,
        key_arg: Spanned<ResolvedExpr>,
        extra_unfolds: Vec<String>,
    },
    MapKeyTrackedIncrement {
        outer_fn: String,
        map_arg: Spanned<ResolvedExpr>,
        key_arg: Spanned<ResolvedExpr>,
    },
    SpecEquivalence {
        extra_unfolds: Vec<String>,
    },
    SpecEquivalenceSimpNormalized {
        extra_unfolds: Vec<String>,
    },
    LinearIntSpecEquivalence {
        unfolded_impl: Spanned<ResolvedExpr>,
        unfolded_spec: Spanned<ResolvedExpr>,
    },
    EffectfulSpecEquivalence {
        impl_fn: String,
        spec_fn: String,
    },
    LinearRecurrence2SpecEquivalence {
        impl_fn: String,
        spec_fn: String,
        helper_fn: String,
    },
    BoundedUniversal,
    ResultPipelineChain {
        chain_qm_fn: String,
        chain_manual_fn: String,
        step_fns: Vec<String>,
    },
    WrapperOverRecursion {
        wrapper_fn: String,
        inner_fn: String,
        other_fn: String,
        combine_op: BinOp,
        driver: WrapperDriver,
        combine_fn: Option<String>,
    },
    TailRecFixedBaseFold {
        spec_fn: String,
        loop_fn: String,
        combine_fn: String,
        combine_op: BinOp,
        type_name: String,
    },
    EnumConstantFold {
        unfold_fns: Vec<String>,
    },
    FiniteDomainCases {
        givens: Vec<String>,
    },
    SimpOverPreludeLemmas {
        unfold_fns: Vec<String>,
        fuel_fns: Vec<String>,
        builtins: Vec<String>,
    },
    IntDecimalRoundtrip {
        parse_fn: String,
        neg_fn: String,
        pos_fn: String,
        sign_fn: String,
        scanner_fn: String,
        predicate_fn: String,
        finish_fn: String,
        finish_int_fn: String,
        serializer_fn: String,
    },
    StringEscapeRoundtrip(Box<StringEscapeRoundtripPin>),
    RingIdentity {
        unfold_fns: Vec<String>,
    },
    FloorDivWindow {
        figure: FloorWindowFigure,
    },
    Sorry,
    BackendDispatch,
}

LinearArithmetic is named for the semantic, not the tactic.

Variants

Reflexive

rfl / definitional equality — lhs ≡ rhs syntactically.

SimpOverLemmas(Vec<String>)

simp chain over named lemmas. The discovery feedback loop (lemma_discovery::committed) pins this when a committed DiscoveredLemmas.lean holds kernel-proved lemmas in-scope for an Induction law: the names are the discovered theorem names, and the Lean renderer reuses the induction ladder with those lemmas embedded + joined to its simp sets. Pinned by the CLI (post-lowering re-pin), never by classify_law_strategy — discovery feedback is opt-in via the committed artifact.

Commutative

∀ a b, f(a, b) = f(b, a) — commutativity of the law’s fn, whose body reduces to a <op> b. The op tag lets backends pick their own lemma vocabulary (Lean: Int.add_comm, Dafny: built-in arithmetic axioms).

Fields

op: BinOp

Associative

∀ a b c, f(f(a,b),c) = f(a,f(b,c)) — associativity of f.

Fields

op: BinOp

IdentityElement

∀ a, f(a, e) = a (or the swapped f(e, a) = a) — the identity-element law for the underlying op (e = 0 for Add / Sub, 1 for Mul). Backends emit simp [fn] (the wrapper’s body unfolds to the identity equation, which simp closes); the variant doesn’t need a side field because the emit is symmetric — Sub is naturally one-sided (only right-identity), Add/Mul accept either side. The lowerer guarantees the law’s actual shape matches the op’s identity behaviour before pinning.

Fields

op: BinOp

AntiCommutative

∀ a b, f(a, b) = -f(b, a) (or the swapped negation). neg_on_rhs records which side carries the - wrap so backends with directional lemmas (Lean’s Int.neg_sub b a : -(b - a) = a - b) can flip via .symm correctly.

Fields

op: BinOp

neg_on_rhs: bool

true for f(a, b) = -f(b, a) (negation on rhs); false for the swapped arrangement.

UnaryEqualsBinary

∀ a, g(a) = f(a, c) or f(c, a) — the unary fn g is the binary fn f with one argument bound to constant c. Backends unfold both fns to expose the underlying op; the IR carries inner_fn (the binary’s source name) so the unfold list is unambiguous.

Fields

inner_fn: String

Source-level name of the binary fn the unary one equals.

LinearArithmetic

“Linear arithmetic over an unfold chain” — the law’s two sides reduce to a flat linear equation on Int once every reachable user fn is unfolded. Generic catch-all for Int laws that don’t fit a named algebraic property. The IR captures the unfold list + wrapper-return signal + refinement smart-constructor guard; backends translate to their decision procedure (Lean: simp + omega, Dafny: Z3 linear int prover). Named for the semantic (“linear arithmetic”), not the Lean tactic.

Fields

unfold_fns: Vec<String>

Ordered fn unfold list. Top-level law fn first — Lean’s unfold resolves left-to-right and the call layer the tactic peels at each step must match the goal shape.

wrapper_return: bool

true when at least one fn in unfold_fns returns a wrapper (Result, Option, …). Drives extra case-split machinery in the emit — pure linear-arithmetic provers can’t close constructor-equality goals, so the wrapper case splits on the smart-constructor guard first.

smart_guard: Option<SmartGuard>

Smart-constructor guard pulled from a refinement fromX(p: Int) -> Result<X, _> in the unfold chain. Some when one was found; None falls back to a conservative (n ≥ 0) default when wrapper_return forces case-splitting.

lifted: bool

true when at least one law given is lifted to a refinement type (given a: Int used as Refined(value = a) in the law body). The Subtype/subset lift carries the invariant in the type, so the by_cases case-split that wrapper_return would otherwise force is unnecessary — backends emit a plain unfold + simp against arithmetic lemmas.

Induction

Structural induction on a recursive ADT parameter.

Fields

param: String

LibraryAxiom

Library axiom instance — the law instantiates a named data-structure axiom (e.g. AverMap’s has_set_self or get_set_self). Backends map the axiom name to their lemma vocabulary (Lean: AverMap.has_set_self; Dafny: its own set/lookup axioms; Z3: built-in array theory). Args carry the call-site expressions the axiom applies to.

Fields

axiom: String

Canonical axiom name. Recognised values today: "Map.has_set_self", "Map.get_set_self". Open string so future axioms (List, Set, Array, …) extend without enum churn.

args: Vec<Spanned<ResolvedExpr>>

Arguments in the order the axiom expects. For Map axioms: [m, k, v] (the map, key, value the axiom reasons about).

MapUpdatePostcondition

Post-condition of an inline-defined map-update fn. The outer fn outer(m, k) has body shape let v = Map.get m k; match v { Some(_) -> Map.set m k _; None -> Map.set m k _ } — i.e. it inspects the existing value and writes some new value at key k in every arm. The law asserts a post-condition on that update — Map.has(outer(m, k), k) == true (HasAfter), or Map.get(outer(m, k), k) == Option.Some(...) (GetAfter).

Backends emit a 2-step proof: unfold the outer fn, case-split on Map.get m k (the same value outer inspected), apply the Map.set-axioms on each branch. Named after the law’s algebraic content, not the Lean tactic.

Fields

outer_fn: String

Source name of the outer update fn.

kind: MapUpdatePostconditionKind

Which post-condition the law asserts.

map_arg: Spanned<ResolvedExpr>

The map argument as it appears at the law’s call site.

key_arg: Spanned<ResolvedExpr>

The key argument as it appears at the law’s call site.

extra_unfolds: Vec<String>

Additional helper-fn source names to unfold on top of outer_fn — only used for GetAfter, where the rhs’s Option.Some(...) typically wraps the prior value via a pure user helper (e.g. addOne(...)). Source names; backends translate to their lemma vocabulary.

MapKeyTrackedIncrement

Counter-increment specialisation of [MapUpdatePostcondition]. The outer fn outer(m, k) is the canonical “tracked counter” shape:

let v = Map.get m k
match v {
  Some(n) -> Map.set m k (n + 1)
  None    -> Map.set m k 1
}

The law states the algebraic content: Option.withDefault(Map.get(outer(m, k), k), 0) == Option.withDefault(Map.get(m, k), 0) + 1 — get-or-default after the increment equals the prior get-or-default plus 1. Tighter than [MapUpdatePostcondition] because both the body template AND the rhs + 1 shape are pinned.

Fields

outer_fn: String

Source name of the outer increment fn.

map_arg: Spanned<ResolvedExpr>

The map argument as it appears at the law’s call site.

key_arg: Spanned<ResolvedExpr>

The key argument as it appears at the law’s call site.

SpecEquivalence

Functional equivalence between an impl fn and a (declared) spec fn — the law states impl(args) == spec(args) and the two fn bodies are syntactically identical (after typecheck). Backends close the goal by unfolding both fns; their bodies reduce to the same term and the equality holds by reflexivity modulo simp normalisation. Lean emits simpa [<unfolds>], Dafny would reveal both and let Z3 prove the equivalence. Named for the algebraic content (functional equivalence), not the backend tactic.

Fields

extra_unfolds: Vec<String>

All user fn source names to unfold — impl + spec + any transitively-reached helpers from law sides. Source names; backends translate to their lemma vocabulary.

SpecEquivalenceSimpNormalized

Broader [SpecEquivalence] for cases where impl and spec bodies are NOT syntactically identical but normalize to the same expression under arg substitution + simp arithmetic identity folding (a + 0 == a, a * 1 == a, a * 0 == 0). Backends close via simp (no simpa — there’s no trivial-rfl goal to discharge; simp normalisation does the closing). Same extra_unfolds payload as SpecEquivalence.

Fields

extra_unfolds: Vec<String>

All user fn source names to unfold — impl + spec + any transitively-reached helpers from law sides.

LinearIntSpecEquivalence

Linear-Int spec equivalence — impl and spec bodies are both linear arithmetic expressions over Int givens (only Literal::Int, given idents, Add, Sub) after arg substitution. Bodies may differ syntactically but the equivalence is decidable by a linear-arithmetic solver (Presburger / omega / Z3 LIA). Backends emit a change <impl_unfolded> = <spec_unfolded> rewrite then close via their decision procedure; the IR carries the substituted expressions so the backend can render them via its own emit_expr.

Fields

unfolded_impl: Spanned<ResolvedExpr>

Impl body with formal params substituted by call-site args. Linear-arithmetic-only after substitution.

unfolded_spec: Spanned<ResolvedExpr>

Spec body with formal params substituted by call-site args. Linear-arithmetic-only after substitution.

EffectfulSpecEquivalence

Functional equivalence between an effectful impl fn and a spec fn. Same “claim states impl(args) == spec(args)” content as [SpecEquivalence], but the law’s source-level shape is non-canonical (impl call usually omits oracle args the spec call carries explicitly). The lowerer runs an Oracle Lift over both sides — injecting oracle args from given oracle: Random.int = ... into every classified effectful call site — and matches the canonical shape on the rewritten form. Backends emit simp [impl, spec]; both definitions unfold to the same oracle call after lifting.

Fields

impl_fn: String

Source name of the impl fn (= vb.fn_name).

spec_fn: String

Source name of the spec fn (the other side of the law).

LinearRecurrence2SpecEquivalence

Second-order linear recurrence spec equivalence — impl is a tail-recursive Int linear-pair wrapper (e.g. fib dispatching on n < 0 and calling a 3-arg fibTR(n, 0, 1) helper) and spec is a direct second-order recurrence (match n { 0 -> b0; 1 -> b1; _ -> recurrence(spec(n-1), spec(n-2)) }). The impl’s helper implements the same affine recurrence as the spec’s _ arm. Both Lean and Dafny render via a Nat-keyed helper + shift lemma + helper-seed bridge; the algebraic content (a fixed-point of the recurrence) is the same in both targets but the syntactic proof template differs per backend.

Fields

impl_fn: String

Source name of the impl (tail-recursive wrapper) fn.

spec_fn: String

Source name of the spec (direct recurrence) fn.

helper_fn: String

Source name of the worker fn called by impl_fn.

BoundedUniversal

Bounded universal: case-split over the declared given domain, dispatch each case to a per-sample lemma.

ResultPipelineChain

?-propagating Result chain equals a manual match-version: the law states chain_qm(x) == chain_manual(x) where the LHS uses ? for short-circuit Err propagation and the RHS writes the same flow as nested match Result.Err -> Err arms. Both sides unfold to the same nested match; the proof closes by unfolding all step fns and case-splitting on each step’s Result discriminator. Demonstrated by examples/core/result_chain.av. Stage 8b of #232.

Fields

chain_qm_fn: String

Source name of the ?-chain fn (the wrapper). LHS of the law.

chain_manual_fn: String

Source name of the manual match-chain fn. RHS of the law.

step_fns: Vec<String>

Source names of every step fn the two chains thread through, in pipeline order. Drives the unfold list for both backends.

WrapperOverRecursion

Monoidal-accumulator wrapper-over-recursion: a non-recursive wrapper_fn(xs) = inner_fn(xs, neutral) paired with a direct- recurrence other_fn such that the law states wrapper_fn(xs) == other_fn(xs). The inner fn has shape match xs { [] -> acc; [h, ..t] -> inner_fn(t, acc <op> h) } where <op> is monoidal (Add / Mul / Sub on Int) with known neutral element. Strategy emits an aux accumulator- decomposition lemma plus the main universal lemma; Z3 closes both via list induction. Demonstrated by examples/data/sum_acc.av.

Stage 8 of #232 — first ProofStrategy variant that consumes a ModulePattern from analysis::shape.

Fields

wrapper_fn: String

Source name of the non-recursive wrapper (e.g. "sum").

inner_fn: String

Source name of the self-recursive inner (e.g. "sumTR").

other_fn: String

Source name of the direct-recurrence fn the law compares the wrapper against (e.g. "sumDirect").

combine_op: BinOp

Binary op the inner threads through its accumulator (Add / Mul / Sub). Drives the aux lemma’s RHS.

driver: WrapperDriver

Driver of the inner recursion: a List<_> structural fold (the additive sum_acc shape) or a Peano-Nat countdown (factTR). Selects the backend’s induction skeleton and the closing tactic family.

combine_fn: Option<String>

For a Peano-Nat fold whose step is a named monoid fn (mul(n, acc) / plus(n, acc)), the combine fn’s source name. None for an inline-binop List fold (acc + h).

TailRecFixedBaseFold

Tail-recursive fold with a FIXED base parameter — the qexp shape (TIP prop_35). The law spec(x, y) == loop(x, y, neutral) equates a 2-arg structural recurrence on the DRIVER y: spec(x, y) = match y { Z -> neutral; S n -> combine(x, spec(x, n)) } against a 3-arg tail-recursive form carrying an accumulator: loop(x, y, z) = match y { Z -> z; S n -> loop(x, n, combine(x, z)) }. Unlike WrapperOverRecursion, the extra param x is FIXED across the recursion (the base), the combine multiplies the accumulator by x (not by the matched subject), and the law binds TWO givens with the wrapper call written inline (no separate wrapper fn). Backends emit the accumulator-generalization lemma loop x y z = combine (loop x y neutral) z (induct on y, generalize z; x fixed) plus the main universal law; the multiplicative algebra closes via the isNatMul bridge to core Nat.mul_* (no Mathlib). Today: multiplicative (Mul, neutral S(Z)) and additive (Add, neutral Z) Peano combines.

Fields

spec_fn: String

Source name of the direct recurrence the law’s other side calls (e.g. "exp"). Recurses on the driver, base param fixed.

loop_fn: String

Source name of the 3-arg tail-recursive loop (e.g. "qexp").

combine_fn: String

Source name of the binary monoid combine fn (mult / plus).

combine_op: BinOp

Combine op classified from the monoid fn’s base arm.

type_name: String

Source type name of the driving Peano Nat ADT.

EnumConstantFold

Ground constant-fold over fixed ADT/enum constructor arguments. The law’s call(s) pin every non-Int param of the verified fn to a constructor literal (CellContent.Empty, Color.Black); any scalar givens are quantified but irrelevant to the chosen branch (the constructor selects a fixed arm). The verified fn and its transitively-reached callees are non-recursive, so the whole call tree folds to a closed term and the goal becomes a decidable ground equality. Backends unfold the fn + callees (the same unfold_fns list the LinearArithmetic detector builds) and close with a split/rfl/decide cascade. Demonstrated by examples/games/checkers/ai.av (centerBonus.emptyNeutral, pieceValue.antisymmetry, pieceValue.kingWorthTripleMan). Named for the algebraic content (constant-folding over a fixed constructor), not the Lean tactic.

Fields

unfold_fns: Vec<String>

Ordered fn unfold list — top-level law fn first, then transitively-reached non-recursive callees. Source names; backends translate to their lemma vocabulary.

FiniteDomainCases

Closed finite-domain enumeration over the law’s givens. Every given ranges over a closed, small domain — Bool or a user-declared enum whose constructors are ALL fieldless — with the product of domain sizes ≤ 16, so exhaustive cases over the givens yields ground goals that compute out (rfl / decide). Fuel-wrapped callees are NOT an obstacle: constant-measure constructor args compute through fuel. The detector deliberately has NO call-shape inspection, NO return-type gate and NO recursion gate — closed enumeration makes those irrelevant, which is why this is a NEW strategy and not a relaxation of ProofStrategy::EnumConstantFold, whose literal-pinning / non-recursive / scalar-return gates are load-bearing for its simp cascade. Motivating shapes: examples/data/json.av parseLiteral.boolRoundtrip (closes genuinely with intro b; cases b <;> rfl) and the EscapeCode laws (escapeJsonChar.encodesEscapeCode, parseEscape.escapeCodeRoundtrip). A non-closing leaf degrades to an honest caught sorry — never a build error and never native_decide.

Fields

givens: Vec<String>

Law given names in intro order — the Lean emitter’s cases targets. Source names; backends translate.

SimpOverPreludeLemmas

Builtin-roundtrip simp over the prelude’s spec-lemma registry — the last typed fallback before BackendDispatch, and the only strategy the Lean backend renders AFTER its legacy ad-hoc chain (so it fires precisely where the sampled-sorry fallback used to emit a bare-sorry universal). A no-when law whose lhs call cone reduces to builtin String/Int operations once the user fns unfold: the Lean emit is intro <givens>; first | (simp [<unfold set>, <registry lemmas>, Int.add_sub_cancel]; done) | sorry. The done + first | … | sorry alternation is the honest floor — a simp that fails OR leaves a residual goal degrades to a caught sorry, NEVER a build error and NEVER native_decide. Motivating shapes: examples/data/json.av finishInt.fromCanonicalInt (closes via Int.fromString_fromInt), finishNumber.fromCanonicalIntSlice / afterIntChar.terminatedIntRoundtrip (slice-prefix lemmas through the toString fuel wrapper) and finishString.plainSegmentRoundtrip (String.slice_append_prefix

• String.intercalate_singleton).

Deliberately a NEW variant and not a reuse of ProofStrategy::SimpOverLemmas: that variant is the discovery feedback loop’s re-pin channel (lemma_discovery::committed re-pins an Induction law when committed discovered lemma texts are in scope, and the backend routes it through the induction emit with embedded lemma bodies). This strategy carries no lemma texts and never inducts — it names static prelude lemmas that the Lean emitter ships demand-driven (see lean::prelude_spec_lemmas_for_builtins, the single source of truth for the builtin → lemma-name registry). Keeping the two apart means neither the discovery CLI nor committed.rs ever has to reason about this variant.

Fields

unfold_fns: Vec<String>

Ordered fn unfold list — law subject fn first, then the transitively-reached NON-recursive callees (sorted). Source names; backends translate.

fuel_fns: Vec<String>

Recursive (fuel-emitted) fns called DIRECTLY in the law lhs with measure-closed args (constructor-headed over scalar-only payloads, or literals) — the fuel value computes to a Nat literal, so simp drives the __fuel equations through. The Lean emitter expands each name to wrapper + <name>__fuel + its measure-helper names. Recursive fns reached only transitively (inside cone bodies) are NOT listed: they stay opaque — usually dead branches under the law’s pinned literal args, and if live the simp falls to the honest caught sorry.

builtins: Vec<String>

Builtin call names observed in the law sides + cone bodies (sorted; includes the synthetic String.concat marker for string +). Registry keys — the Lean emitter maps them to prelude spec lemma names via prelude_spec_lemmas_for_builtins.

IntDecimalRoundtrip

Decimal-Int parse/serialize roundtrip over the canonical single-scanner decimal parser shape: the law states parse(ser(C(n)), 0) = Ok(C(n), String.len(ser(C(n)))) for an unconstrained given n: Int, where parse dispatches the head char ("-" → sign path, "0" → leading-zero scan, _ → digit path), both paths funnel into ONE recognized fuelized string-position scanner (proof_recognize::detect_string_pos_scan — the same gate that makes the Lean backend synthesize the scanner’s <fn>__fuel_scan companion lemma), and the cone bottoms out in String.fromInt / Int.fromString.

The detector validates the ENTIRE canonical shape (arm literals, arm order, scanner pins, finish-fn slice + Int.fromString leaf), so the Lean emission can render the fixed sign-split proof skeleton ported from the verified json hand proof: serializer reduces by rfl (ADT-measure fuel), rcases Int.ofNat | Int.negSucc, head-char dispatch via String.mk-form rfl, split + digitChar contradiction lemmas, the synthesized scan lemma, and Int.fromString_fromInt at the finish_int_fn leaf. The whole emission is wrapped in first | (… ; done) | sorry — a non-closing case degrades to a caught honest sorry, never a build error, and native_decide never appears. Dafny treats the pin as BackendDispatch (exports byte-identical).

Demonstrated by examples/data/json.av parseNumber.fromIntRoundtrip — the first universal close through the fuel-unfolding barrier on a string whose length is symbolic.

Fields

parse_fn: String

Subject parser fn (parseNumber). Source names throughout.

neg_fn: String

"-"-arm continuation (parseNumberSign).

pos_fn: String

Wildcard-arm digit dispatcher (startNumberDigits).

sign_fn: String

Sign path’s digit dispatcher (startSignDigit).

scanner_fn: String

The recognized fuelized scanner (scanIntTail).

predicate_fn: String

The scanner’s char-class predicate (isDigit).

finish_fn: String

Scanner exit continuation (finishNumber).

finish_int_fn: String

Int leaf — slices + Int.fromString (finishInt).

serializer_fn: String

Serializer the law’s lhs feeds the parser (toString).

StringEscapeRoundtrip(Box<StringEscapeRoundtripPin>)

String escape/parse roundtrip over the canonical segment-chunking string scanner: the law states parse(<open> + escape(s) + <terminator>, 1) = Ok(StrCtor(s), String.len(escape(s)) + 2) for an unconstrained given s: String (or the same claim entered at the scanner itself with pos = segmentStart = 1, chunks = []). The producer is a per-char classifier fold (two-char escape table + hex control escapes + printable passthrough); the consumer is a fuel mutual SCC (scan / escape-dispatch / validate / unicode chain) whose per-arm shapes the detector validates EXACTLY — see StringEscapeRoundtripPin for every captured name and literal, and proof_lower::string_escape_roundtrip for the gates.

The Lean emission renders the suffix-invariant proof skeleton ported from the verified json hand proof (kernel-checked on Lean 4.15, #print axioms = [propext, Quot.sound]): a drop-form suffix-cursor prelude, the producer fold’s accumulator homomorphism, one step lemma per consumer fuel arm, and a chunk invariant with the carried scanner state (segmentStart, chunks) universally quantified, closed by per-char classification. Every synthesized lemma carries a first | (…; done) | sorry floor — a template regression degrades to caught honest sorries (loud budget red), never a build error, and native_decide never appears. Dafny treats the pin as BackendDispatch (exports byte-identical).

Demonstrated by examples/data/json.av escapeJsonString.parseStringRoundtrip and parseStringChunk.escapedStringRoundtrip — the parser workhorse pair that closes json’s pinned Lean budget to 0.

RingIdentity

Unconditional ring identity over Int-component records — the algebra-law family of an exact-rationals library (a record with Int numerator/denominator fields, non-normalizing arithmetic, equality by cross-multiplication): add/mul commutativity and associativity, distributivity, neg/sub normal forms, identity elements. The law has no when, every given is Int or a record whose fields are ALL Int (at least one such record given), and the claim’s whole unfold cone is non-recursive pure arithmetic — record constructions / field projections, Int literals, +, -, *, unary negation — with the equality bottoming out in Int == (a Bool comparator fn applied at the law root, compared to true) or direct value equality of two such arithmetic expressions. Both sides are then polynomial identities: distributing products over sums and AC-normalizing monomials and sums makes the two sides’ monomial multisets identical, no coefficient collection needed.

The Lean emit is intro <givens>; first | (simp [<unfold cone>, <fixed core AC-ring lemma package>]; done) | sorry — the honest caught-sorry floor; never native_decide, never a build error. The package is SCOPED TO THIS STRATEGY’s emission: its permutational rewrites (Int.mul_comm, Int.add_comm, …) loop or destroy the normal forms other strategies’ simp sets rely on, so they are never added to the shared prelude registry. Dafny needs no special handling — Z3 decides these nonlinear identities push-button — and treats the pin like BackendDispatch (exports stay byte-identical). Demonstrated by examples/data/rational.av.

Fields

unfold_fns: Vec<String>

Ordered fn unfold list — law subject fn first, then the transitively-reached callees (sorted). Source names; backends translate to their lemma vocabulary.

FloorDivWindow

Floor-division window family — laws over a power-of-two fn (match n <= 0 { true -> 1; false -> 2 * pow(n - 1) }), a floor-halving binary-exponent fn (the RecursionContract::WellFoundedToNat class with divisor 2), and the scaled-significand / bit-width window predicates built from them. Each FloorWindowFigure is a fully-validated shape with a fixed proof template on both backends (Lean: the core Int.le_ediv_iff_mul_le / Int.ediv_lt_iff_lt_mul floor bridges + power algebra by functional induction; Dafny: a proved division-window prelude + branch-split helper lemmas). The recognizers are deliberately narrow — exactly the hand-validated figures; everything else declines and keeps the prior emission.

Fields

figure: FloorWindowFigure

Sorry

No automated strategy — emit with sorry (Lean) / assume {:axiom} (Dafny). User fills in manually.

BackendDispatch

Lowerer has not pinned a strategy for this law; the backend’s or_else chain decides. Today reached by linear-recurrence- spec equivalence (Lean-specific, ~50-line support theorems stay in the backend) and the sampled / guarded-domain fallback. The backend treats BackendDispatch as “fall through to ad-hoc strategy chain”; pinned variants above short-circuit to a known emit.

Trait Implementations

impl Clone for ProofStrategy

fn clone(&self) -> ProofStrategy

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ProofStrategy

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.