A “refinement record” is the canonical refinement-via-opaque
pattern: a single-field record X { carrier: T } paired with a
validating smart constructor
fn fromX(p: T) -> Result<X, _> body = match <pred-in-p> with true -> Result.Ok(X(carrier = p)) false -> Result.Err("...")
The pure recursive fns that THREAD an accumulator over a USER-ADT driver —
a param fed a RECONSTRUCTED expression in every self-call
(param_threaded_in_recursion) while NO param is a structural List
(single_list_structural_param_index is None), the triTR / qfac /
qexp shape. These are exactly the fns the recursion classifier learned to
accept as structural defs (single_adt_structural_param_index): before, a
growing accumulator left them unclassified, so law_calls_unclassified_fn
bounded every law that referenced them; now they are classified and that gate
no longer fires. A law verified ON such a fn closes by induction … generalizing acc, but a law that merely REFERENCES one (fac(x) => qfac(x, 1) verified on fac) still can’t close by simple induction — it needs the
inner fn’s accumulator-decomposition lemma. The list-accumulator folds
(qrev) are DELIBERATELY excluded: they were always ListStructural
(classified), the fuel gate never bounded laws over them, and a consumer law
myRev(x) => Lib.qrev(x, []) genuinely closes by citing the dep’s proven
qrev law — re-gating those would regress the cross-file law pool.
A verify fn law … given a: T = [v] with one value per given binds
the law to a single concrete point. Combined with
law_rhs_is_independent_of_givens this is the “sample-only”
shape — the universal form is vacuous (RHS is a constant,
LHS-with-one-input doesn’t span anything). Asociative-style laws
also have singleton givens but their RHS uses the bound names
(add a (add b c)), so the universal form there is genuinely
the asociativity statement and stays.
Dafny’s bound-vs-attempt decision for a law touching an accumulator fold,
now that the Dafny backend HAS a datatype-induction generalizing emit. Bound
(sample-only) when:
Basename for the entry file emitted by Lean / Dafny. Prefer the
source-declared module name (module Foo → Foo) so the entry
file’s name matches what the user wrote; fall back to a capitalised
project name when no module declaration is present. Lake’s
path-as-module-name convention forces this for Lean — Dafny doesn’t
strictly need it but the same basename keeps the two backends
aligned (no more playground.dfy vs OracleTrace.lean).
Convenience: find_fn_contract_scoped with the scope resolved
by pointer-eq against ctx.modules. Use this from emit sites
that have &FnDef in hand — never the bare-name variant — so a
module-owned recursive fn always resolves to its OWN canonical
slot, even if another module exports a same-bare-name fn.
Scope-aware fn-contract resolver. scope = Some(prefix) directs
bare-name lookups to that module’s slot before falling back to
entry / module-walk. Mirror of find_refined_type_scoped for fn
contracts — without it, two modules with same-bare-name
recursive fns silently merge under whichever module-walk hit
first.
Refined-type lookup for a Type::Named ref. Prefers the
id-direct path when id: Some(_) is stamped, falls back to the
name-keyed resolution chain otherwise (builtins, unresolved
refs).
Module-scope-aware variant of find_refined_type. When the
caller knows which module’s emit-pass is in flight (scope = Some(module.prefix)), the resolver tries Module.Namebefore
falling back to module-walk ordering. Two modules with same-bare
refined records (A.Natural + B.Natural, distinct predicates)
then resolve to the current scope’s entry — bare references
inside module B’s emit pick up B.Natural, not whichever module
happened to populate first.
Canonical-key-aware resolver — returns (canonical_key, decl)
so consumers thread one stable identifier through refinement
lift / strip-wrappers / when-redundancy / backend emit instead
of recomputing identity from bare AST names.
Round-4 central canonical resolver. Both find_refined_type and
find_refined_type_scoped reduce to this. Returns the exact
(canonical_name, &decl) pair stored in ProofIR.refined_types
so downstream code can re-key safely (no string heuristics). The
canonical name is the string form of the TypeKey the IR resolved
the decl from (e.g. AAA.Natural) — even though the map itself is
keyed by opaque TypeId after phase E2, consumers expect a
human-readable identifier here for diagnostics and defmt-style
canonical comparison.
Flatten a chain of Bool.and(a, b) calls into the flat list of
leaf predicates. Aver’s when a >= 0 / when b >= 0 syntax folds
multiple when lines into nested Bool.and(prev, next) at parse
time (see parser/blocks.rs’s law-block loop), so the predicate
arrives at codegen as Bool.and(Bool.and(p1, p2), p3). Identity
checks against per-given refinement invariants need the flat shape.
ResolvedExpr mirror of flatten_bool_and_conjuncts. After the
resolver lifts Bool.and(a, b) into
ResolvedExpr::Call(ResolvedCallee::Builtin("Bool.and"), args),
the same recursive split holds.
Resolve &FnDef to the opaque crate::ir::FnId from the
symbol table. Pointer-eq scope detection routes module-owned
fns through their canonical Module.fn key. Returns None when
the fn isn’t registered (built-ins / synthesized variants the
table excludes by design).
Resolve a dotted source-level name (fn, Module.fn) to the
opaque FnId. Used by emit code that walks AST expressions
(e.g. detecting calls to opaque-emitted fns inside a law body)
— keeps the FnKey resolution in one place instead of letting
each walker re-derive identity from bare strings.
Round-7: build a crate::ir::FnKey from a borrowed &FnDef.
The owning module is resolved by pointer-comparison against
ctx.modules[*].fn_defs (entry items / synthesized variants /
extra_fn_defs fall through to FnKey::entry). This is the
single resolver consumers should reach for from emit code with
a &FnDef in hand — produces the typed key the IR maps store
instead of leaving the bare-name collision risk in place.
Round-6: resolve a &FnDef’s owning scope by pointer comparison
against ctx.modules[*].fn_defs. Pointer-eq sidesteps the
bare-name collision — &CountdownA.fn_defs[0] and
&CountdownB.fn_defs[0] are distinct addresses even with
fd.name = "countdown" in both.
Granular variant of is_recursive_type_def taking a sum’s
(name, variants) split — some backends already have the parts
separated and don’t want to rebuild a TypeDef just to query.
True iff a two-arm bool match is the canonical refinement shape:
true -> Result.Ok(<TypeName>(<carrier_field> = <param>)) and
false -> Result.Err(_). Required so we don’t mis-classify a
random match … -> Result.Ok(...) | -> Result.Err(...) (e.g. an
effectful pipeline) as a smart constructor.
true iff law’s lhs/rhs calls a recursive accumulator-threading fn OTHER
than verified_fn — the foreign-fold hazard (see
accumulator_fold_fn_names). Such a law can’t close by simple induction
(it needs the inner fn’s accumulator-decomposition lemma) and must stay
bounded, exactly as it did before the recursion classifier learned the
threaded-accumulator shape. The verified fn is excluded so an accumulator-
generalizing law verified ON the fold (triTR(n, acc) => plus(triSpec(n), acc)) is NOT gated — Lean closes it by induction … generalizing acc.
Lean uses THIS (it has the generalizing emit); Dafny uses
[law_calls_any_accumulator_fold] because it has no such emit.
true iff a Nat accumulator-generalizing law verified ON verified_fn can
CLOSE its universal on Dafny. Unlike Lean (which bridges the user monoid fn
to builtin Nat arithmetic that Z3 knows is associative/commutative), Dafny
sees the user plus / mul over the ADT as opaque, so the datatype-induction
proof only discharges when the file ALSO provides commutativity AND
associativity laws for the fold’s combine fn — which the generic driver
proves and cites. Absent those helpers the universal would ERROR (Dafny
cannot sorry), so it must stay sample-only. The List corner never reaches
here (its accumulator combine is a builtin BinOp, so accfold_combine_fn
is None, and list folds are excluded from accumulator_fold_fn_names).
Structural equality on Aver predicate expressions with commutator
relaxation: at every BinOp comparator node, allow the operands +
operator to be swapped. Both a >= 0 and 0 <= a compare equal,
recursively. Non-comparator BinOps (Add, Sub, …) and other
Expr variants fall through to the derived PartialEq on
Spanned<Expr> (which compares .node only — line numbers don’t
participate). Used by the when-vs-refinement-invariant identity
check so a redundantly-written user when gets recognised even when
the operand order doesn’t match the smart constructor’s predicate
verbatim.
Strip RecordCreate { type_name: X, fields: [(_, Ident(g))] } →
Ident(g) when g is in lifted_vars and X is the refined
type those vars were lifted to. Used after refinement_lift_for_ given decides the lift: theorem body talks about g : Natural
directly, so the Natural(value = g) wrapper that aver source
wrote becomes redundant noise.
Rewrite bare references to refinement-lifted given variables
(a → a.val) inside scalar / arithmetic contexts so the emitted
Lean expression typechecks against the Subtype carrier.
Inspect inputs for a refinement-via-opaque record by type_name.
Returns Some(info) iff there’s exactly one matching smart
constructor and the record has a single carrier field.
Module-scoped variant of refinement_info_for. scope = None means “look in entry items only”; scope = Some(prefix)
means “look in the dep module whose prefix matches”.
Walk lhs/rhs looking for RecordCreate { type_name: X, fields: [(_, Ident(given_name))] } where X is a refinement record whose
carrier matches given_type. Returns the refined type name when
found, so callers can lift given_name’s quantifier from the
carrier type to the refined type. Without this, theorems would
emit ∀ (a : Int), … RecordCreate(a) … where the smart-
constructor predicate has to be discharged from a’s when
clause inside the theorem type — which is exactly what the
previous heuristic-laden auto-proof had to work around.
Same resolution shape as find_refined_type but driven by the
in-flight refined_types map plus dep-module list — used inside
proof_lower where there is no CodegenContext yet. Resolves
name → TypeKey → opaque TypeId through the supplied symbol
table, then looks up the decl by id.
Same as resolve_refined_type_in but returns the canonical
TypeId paired with the decl — used by IR-internal callers
(the proof-lower side walk_for_refinement_carrier) so they
thread the opaque identity through downstream comparisons
without re-introducing bare-name heuristics.
Walk expr and rename every Ident(from) / Resolved { name: from } to Ident(to). Lives here (not in recursion) because three
proof-mode predicate sources reach for the same substitution:
caller-guard extraction translates caller’s local-var name to
callee’s param name; opaque-type when-redundancy check translates
smart constructor’s param name to the law’s given name; future
callers (verify-law domain translation, etc.) will too. Single
definition keeps Lean and Dafny in sync.
ResolvedExpr mirror of substitute_ident_in_expr. Rewrites
every Ident(from) / Resolved { name: from, .. } leaf to
Ident(to) — the slot identity (if any) is dropped because the
substitution targets a free variable name that doesn’t have a
slot in the resolver’s local table. Used by proof-mode
when-redundancy check + smart-guard predicate substitution
after the IR carries pre-resolved expressions.
Swap a comparison BinOp’s operands canonically: a OP b ≡ b OP' a
where OP’ is the commutator-flipped op (Lt ↔ Gt, Lte ↔ Gte,
Eq and Neq symmetric). Returns None for non-comparator BinOps.
Used by predicate_syntactic_eq so 0 <= a matches a >= 0 for the
when-vs-refinement-invariant check.
Round-7: build a crate::ir::TypeKey from a borrowed
&TypeDef. Same shape as fn_key_for_decl — pointer-eq
against ctx.modules[*].type_defs resolves the owning module.
Round-7: resolve a (possibly bare) type name from the AST into
a crate::ir::TypeKey. scope is the emit-time current scope
(Some(prefix) inside a per-module emit loop, None for
entry). Bare names prefer the current scope, then entry, then
fall back to module-walk first match — mirroring
find_refined_type_scoped’s resolution order.
Issue #128: extract fn names from proof_ir.unclassified_fns
messages. The diagnostic prose is the source of truth (the
UnclassifiedFn struct doesn’t carry a separate name field
today); each message starts recursive function 'NAME' is outside proof subset (...). Extract the quoted name so the law gate has
a HashSet<String> to test fn-call expressions against.
Stable identity key for a verify block’s case-index space, shared by the
Lean emitter’s per-block case counters and the CLI’s VM ground-truth
collection (CodegenContext::sample_expected).
True iff every refinement-lifted given’s invariant is
syntactically captured by some clause of when (and vice versa —
a bijection between conjuncts). Used by both Lean and Dafny law
emitters to decide whether when is provably redundant with the
types of the lifted givens; if yes, drop it from the theorem
premise (carrier is now the type’s invariant); if no, keep it so
the user’s stronger / orthogonal predicate stays part of the claim
and isn’t silently lost.