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,
    MatchDispatcherFold {
        fold_fn: String,
        spec_fn: String,
    },
    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,
    },
    Sorry,
    BackendDispatch,
}

Algebraic / proof-theoretic shape of a verify-law theorem.

Naming rule: variants describe what the law says, not how a backend proves it. The IR is target-agnostic — Lean maps Commutative { op: Add } to simp [fn, Int.add_comm], Dafny maps the same variant to its own lemma vocabulary, a Z3 backend could ship a different tactic again. Tactic names (SimpOverLemmas, simp+omega) do not appear in variant names; 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 (e.g. [Int.add_comm, Int.mul_comm]). Legacy draft variant; not yet emitted by the lowerer — kept for future use when a strategy wants to hand the backend a specific lemma list.

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.

MatchDispatcherFold

Two MatchDispatcherFold fns over the same List<T> param compute the same result via slightly different but structurally identical match-on-list bodies. The law states fold_fn(xs) == spec_fn(xs); the proof closes by induction on xs with both nil and cons cases reducing to arithmetic identities. Demonstrated by examples/data/list_length_fold.av (lengthFwd(xs) = 1 + lengthFwd(t) vs lengthSwap(xs) = lengthSwap(t) + 1 — equivalent via commutativity, closes via omega).

Stage 8c of #232 — third typed-pattern consumer in proof_lower.

Fields

fold_fn: String

Source name of the LHS fold fn (the law’s surrounding fn).

spec_fn: String

Source name of the RHS spec fn — also a list-fold of the same shape.

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.

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.