Add termination checking for recursive functions#1092
Conversation
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
Solid PR. The architecture is clean — AdtRankAxioms for axiom generation, TerminationCheck for the pipeline phase, with good separation of concerns. The wrapImplications refactoring to share code between PrecondElim and TermCheck is well done. The List_get_non_neg/List_set_non_neg bug fixes are genuine catches. Test coverage is comprehensive (17 tests covering basic, mutual, polymorphic, error cases, preconditions, non-termination detection). Documentation is thorough and well-written.
| | some _ => none | ||
| | none => FuncAttr.findInlineIfConstr func.attr | ||
|
|
||
| /-- Extract the datatype name from a monomorphic type. -/ |
There was a problem hiding this comment.
Nit: adtNameOf silently returns "" for non-ADT types, which would produce a bogus "..adtRank" function name if it ever reached mkAdtRankLt or mkAdtRankDecls. The error checking in Step 1 of termCheck prevents this in practice, but an Option String return (or a panic!) would make the invariant explicit and prevent silent corruption if the precondition is ever violated.
There was a problem hiding this comment.
I don't think it should panic. It is possible to change to an Option but it doesn't actually help all that much: we still need a default case for the call sites (mkAdtRankLt and extractTermObligations). Since the error checking catches this already I didn't think it was worth the additional complication.
There was a problem hiding this comment.
How about:
| /-- Extract the datatype name from a monomorphic type. -/ | |
| /-- Extract the datatype name from a monomorphic type. | |
| Precondition: `ty` must be a `.tcons` (enforced by error checking in `termCheck`). -/ | |
| private def adtNameOf (ty : LMonoTy) : String := |
| go (e : Expression.Expr) (implications : List (Unit × Expression.Expr)) | ||
| : List Expression.Expr := | ||
| match _he: e with | ||
| | .ite _ c t f => | ||
| let cObs := go c implications | ||
| let tObs := go t (((), c) :: implications) | ||
| let notC : Expression.Expr := | ||
| LExpr.mkApp () (.op () "Bool.Not" (.some (LMonoTy.arrow .bool .bool))) [c] | ||
| let fObs := go f (((), notC) :: implications) | ||
| cObs ++ tObs ++ fObs | ||
| | .app _ _ _ => | ||
| match _h : getLFuncCall e with | ||
| | (op, args) => | ||
| let argObs := args.attach.flatMap fun ⟨a, _⟩ => go a implications | ||
| let callObs := match op with | ||
| | .op _ opName _ => | ||
| if opName.name ∈ recFuncNames then | ||
| match funcDecreasesMap.find? (fun (n, _, _) => n == opName.name) with | ||
| | some (_, calleeIdx, calleeAdtTy) => | ||
| match args[calleeIdx]? with | ||
| | some callArg => | ||
| let ltExpr := mkAdtRankLt callArg callerParam callerAdtTy calleeAdtTy | ||
| [wrapImplications implications ltExpr] | ||
| | none => [] | ||
| | none => [] | ||
| else [] | ||
| | _ => [] | ||
| argObs ++ callObs | ||
| | .eq _ e1 e2 => go e1 implications ++ go e2 implications | ||
| | .abs _ _ _ body => go body implications | ||
| | .quant _ _ _ _ trigger body => | ||
| go trigger implications ++ go body implications | ||
| | _ => [] | ||
| termination_by e.sizeOf | ||
| decreasing_by |
There was a problem hiding this comment.
extractTermObligations recurses into ite branches, eq, abs, quant, and function applications (via getLFuncCall). However, it does not recurse into the body of a let-binding.
In the locally nameless representation, a let-binding let x = e1 in e2 is encoded as .app _ (.abs _ _ _ e2) e1. When getLFuncCall encounters this, it returns (.abs _ _ _ e2, [e1]). The argObs recurses into e1, but e2 (the let body) is never visited — the .abs case at line 113 only fires for standalone abs nodes, not ones inside .app.
This means a recursive call inside a let body would be missed:
rec function f(@[cases] xs : IntList) : int {
let y = g(xs) in f(IntList..tl(xs)) + y
}
In practice this doesn't matter today because Core functions don't use let bindings, but it's worth a comment documenting this limitation so future maintainers don't assume full coverage:
| go (e : Expression.Expr) (implications : List (Unit × Expression.Expr)) | |
| : List Expression.Expr := | |
| match _he: e with | |
| | .ite _ c t f => | |
| let cObs := go c implications | |
| let tObs := go t (((), c) :: implications) | |
| let notC : Expression.Expr := | |
| LExpr.mkApp () (.op () "Bool.Not" (.some (LMonoTy.arrow .bool .bool))) [c] | |
| let fObs := go f (((), notC) :: implications) | |
| cObs ++ tObs ++ fObs | |
| | .app _ _ _ => | |
| match _h : getLFuncCall e with | |
| | (op, args) => | |
| let argObs := args.attach.flatMap fun ⟨a, _⟩ => go a implications | |
| let callObs := match op with | |
| | .op _ opName _ => | |
| if opName.name ∈ recFuncNames then | |
| match funcDecreasesMap.find? (fun (n, _, _) => n == opName.name) with | |
| | some (_, calleeIdx, calleeAdtTy) => | |
| match args[calleeIdx]? with | |
| | some callArg => | |
| let ltExpr := mkAdtRankLt callArg callerParam callerAdtTy calleeAdtTy | |
| [wrapImplications implications ltExpr] | |
| | none => [] | |
| | none => [] | |
| else [] | |
| | _ => [] | |
| argObs ++ callObs | |
| | .eq _ e1 e2 => go e1 implications ++ go e2 implications | |
| | .abs _ _ _ body => go body implications | |
| | .quant _ _ _ _ trigger body => | |
| go trigger implications ++ go body implications | |
| | _ => [] | |
| termination_by e.sizeOf | |
| decreasing_by | |
| | .app _ _ _ => | |
| -- Note: let-bindings (.app _ (.abs _ _ _ body) arg) are decomposed by | |
| -- getLFuncCall as (abs, [arg]). The abs body is NOT recursed into. | |
| -- This is acceptable because Core recursive functions currently don't | |
| -- use let-bindings. If that changes, this case needs updating. | |
| match _h : getLFuncCall e with |
| (emittedAdtRank : Std.HashSet String) | ||
| : CoreTransformM (Bool × List Decl) := do | ||
| match decls with | ||
| | [] => return (false, []) | ||
| | d :: rest => | ||
| match d with | ||
| | .recFuncBlock funcs md => do | ||
| -- Step 1: error checking | ||
| -- Skip polymorphic functions: adtRank axioms are monomorphic, so we | ||
| -- cannot generate them for polymorphic datatypes yet. The user-facing | ||
| -- error is in Env.addFactoryFunc; when that restriction is lifted, | ||
| -- this filter must be updated to handle polymorphic adtRank generation. | ||
| let fileRange := Imperative.getFileRange md |>.getD FileRange.unknown | ||
| let throwErr (msg : String) : CoreTransformM Unit := | ||
| throw (DiagnosticModel.withRange fileRange msg) | ||
| for func in funcs do |
There was a problem hiding this comment.
The error checking in Step 1 throws on the first error it finds. For a recFuncBlock with multiple functions, if the first function has a valid decreases but the second doesn't, only the second's error is reported. This is fine for single errors, but if multiple functions in the same block have issues, the user has to fix them one at a time.
Consider collecting all errors and throwing them together, or at minimum adding a comment noting the fail-fast behavior.
| : Option (Decl × Nat) := do | ||
| let decrIdx ← getDecreasesIdx func | ||
| let inputTys := func.inputs.values | ||
| let decrTy ← inputTys[decrIdx]? | ||
| let decrParam ← func.inputs.keys[decrIdx]? | ||
| let body ← func.body | ||
| let obligations := extractTermObligations body recFuncNames decrParam decrTy | ||
| funcDecreasesMap | ||
| if obligations.isEmpty then none | ||
| let stmts := obligations.mapIdx fun i ob => | ||
| Statement.assert s!"{func.name.name}_terminates_{i}" ob md | ||
| -- Specialize polymorphic axioms to the concrete decreasing-parameter type | ||
| let tySubst := mkTySubst tf decrTy | ||
| let specializedAxioms := adtRankAxioms.map fun (name, e) => | ||
| (name, e.applySubst tySubst) | ||
| some (.proc { | ||
| header := { | ||
| name := ⟨termProcName func.name.name, ()⟩ | ||
| typeArgs := func.typeArgs | ||
| inputs := func.inputs | ||
| outputs := [] | ||
| noFilter := true | ||
| } | ||
| spec := { preconditions := | ||
| (specializedAxioms.map fun (name, e) => | ||
| (name, { expr := e, attr := .Free })) ++ | ||
| (func.preconditions.mapIdx fun i p => | ||
| (s!"{func.name.name}_requires_{i}", { expr := p.expr, attr := .Free })), | ||
| postconditions := [] } | ||
| body := stmts | ||
| } md, obligations.length) | ||
|
|
||
| /-- Add a termination-check procedure as a leaf node in the cached call graph. -/ | ||
| private def addTermProcToCallGraph (name : String) : CoreTransformM Unit := | ||
| modify fun σ => match σ.cachedAnalyses.callGraph with | ||
| | .some cg => { σ with cachedAnalyses := { σ.cachedAnalyses with | ||
| callGraph := .some (cg.addLeafNode name) } } | ||
| | .none => σ | ||
|
|
||
| /-- Result of generating adtRank declarations for a mutual datatype block. -/ | ||
| private structure AdtRankDecls where |
There was a problem hiding this comment.
mkTermCheckProc embeds ALL adtRank axioms as preconditions of the generated $$term procedure, even axioms for datatypes not used by this particular function. For a mutual block with functions over different datatypes, each $$term proc gets axioms for all datatypes in the block.
This is sound (extra axioms don't hurt) but could make the SMT queries larger than necessary. For small programs this is fine, but for large mutual blocks with many datatypes, filtering axioms to only those relevant to the function's decreasing parameter type would reduce VC size.
| For each constructor `C` and each field of datatype type within the | ||
| mutual block `block`, generates: | ||
| `∀ fields. D'..adtRank(field_i) < D..adtRank(C(fields...))` | ||
| with trigger `D..adtRank(C(fields...))`. | ||
|
|
||
| The `block` parameter determines which field types are considered | ||
| "recursive" (i.e., belong to the mutual datatype block). -/ | ||
| def mkAdtRankPerConstrAxioms {T : LExprParams} [Inhabited T.Metadata] [Inhabited T.IDMeta] [DecidableEq T.IDMeta] | ||
| (dt : LDatatype T.IDMeta) (block : MutualDatatype T.IDMeta) | ||
| (m : T.Metadata) : List (LExpr T.mono) := | ||
| let dtTy := dataDefault dt | ||
| dt.constrs.flatMap fun c => | ||
| let numFields := c.args.length | ||
| let constrTy := LMonoTy.mkArrow' dtTy (c.args.map (·.2)) | ||
| let constrApp := c.args.foldlIdx (fun acc i _ => | ||
| .app m acc (.bvar m (numFields - 1 - i)) | ||
| ) (.op m c.name (.some constrTy)) | ||
| let adtRankTy := .arrow dtTy .int | ||
| let adtRankConstr : LExpr T.mono := | ||
| .app m (.op m (adtRankFuncName dt.name) (.some adtRankTy)) constrApp | ||
| let fieldTys := (c.args.map (·.snd)).reverse | ||
| (c.args.foldlIdx (init := []) fun acc i (_, fieldTy) => | ||
| match block.find? (fun d => fieldTy == dataDefault d) with | ||
| | none => acc | ||
| | some fieldDt => | ||
| let fieldBvar := .bvar m (numFields - 1 - i) | ||
| let fieldRankTy := .arrow (dataDefault fieldDt) .int | ||
| let adtRankField := .app m (.op m (adtRankFuncName fieldDt.name) | ||
| (.some fieldRankTy)) fieldBvar | ||
| let ltTy := .arrow .int (.arrow .int .bool) | ||
| let ltExpr := LExpr.mkApp m (.op m "Int.Lt" (.some ltTy)) | ||
| [adtRankField, adtRankConstr] | ||
| let axiom_ := match fieldTys with | ||
| | [] => ltExpr | ||
| | ty :: rest => | ||
| let inner := .quant m .all "" (.some ty) adtRankConstr ltExpr | ||
| rest.foldl (fun body ty => | ||
| .quant m .all "" (.some ty) (LExpr.noTrigger m) body | ||
| ) inner | ||
| axiom_ :: acc | ||
| ).reverse | ||
|
|
||
| /-- Generate the non-negativity axiom `∀ x. adtRank(x) >= 0` for a datatype. |
There was a problem hiding this comment.
The axiom generation is well-structured. A few observations:
- Proof opportunity: The key soundness property is that
adtRankis well-founded — i.e., there is no infinite descending chain. This follows from the fact that every constructor's recursive fields have strictly smaller rank. A formal theorem stating this would strengthen confidence:
-- Informal: For any ADT D with constructors C_i, if field f_j of C_i has type D' in the mutual block,
-- then the generated axiom `D'..adtRank(f_j) < D..adtRank(C_i(fields...))` is consistent
-- (i.e., there exists a model satisfying all axioms simultaneously).
This could be proved by exhibiting a concrete model: define adtRank as the structural depth of the ADT value.
-
Non-negativity axiom:
mkAdtRankNonNegAxiomgenerates∀ x. adtRank(x) >= 0. Combined with the per-constructor axioms, this ensuresadtRankis a well-founded measure on natural numbers. Good. -
Trigger placement: The per-constructor axioms use
adtRank(C(fields...))as the trigger, which means they only fire when the SMT solver encounters anadtRankapplication on a constructor term. This is the right choice — it avoids matching loops while ensuring the axioms fire when needed.
| | .proc proc md => do | ||
| if TermCheck.isTermProc proc.header.name.name then | ||
| let (changed, rest') ← transformDecls rest | ||
| return (changed, d :: rest') | ||
| else | ||
| let F ← getFactory |
There was a problem hiding this comment.
Good — $$term procedures are skipped by PrecondElim to avoid duplicating precondition assertions. The check uses TermCheck.isTermProc which tests for the $$term suffix.
However, this creates a coupling between PrecondElim and TerminationCheck — PrecondElim now imports TerminationCheck. If more pipeline phases need to skip $$term procedures in the future, consider adding a general skipPrecondElim flag to the procedure header (similar to noFilter) instead of hard-coding the name check.
| /- | ||
| Copyright Strata Contributors | ||
|
|
||
| SPDX-License-Identifier: Apache-2.0 OR MIT | ||
| -/ | ||
|
|
||
| import Strata.Languages.Core.Verifier | ||
|
|
||
| /-! | ||
| # Termination Checking Tests | ||
|
|
||
| Tests termination checking for recursive functions over algebraic datatypes. | ||
| -/ | ||
|
|
||
| namespace Strata.TerminationCheckTest | ||
|
|
||
| --------------------------------------------------------------------- |
There was a problem hiding this comment.
Consider adding a test for a function where the recursive call is nested inside a non-recursive function call, e.g.:
rec function f(@[cases] xs : IntList) : int {
if IntList..isNil(xs) then 0 else g(f(IntList..tl(xs)))
}
where g is a non-recursive function. This tests that extractTermObligations correctly recurses into arguments of non-recursive calls.
| | some _ => none | ||
| | none => FuncAttr.findInlineIfConstr func.attr | ||
|
|
||
| /-- Extract the datatype name from a monomorphic type. -/ |
There was a problem hiding this comment.
How about:
| /-- Extract the datatype name from a monomorphic type. -/ | |
| /-- Extract the datatype name from a monomorphic type. | |
| Precondition: `ty` must be a `.tcons` (enforced by error checking in `termCheck`). -/ | |
| private def adtNameOf (ty : LMonoTy) : String := |
| let rankX := .app m (.op m (adtRankFuncName dt.name) (.some rankTy)) | ||
| (.bvar m 0) | ||
| let geTy := .arrow .int (.arrow .int .bool) | ||
| let geExpr := .mkApp m (.op m "Int.Ge" (.some geTy)) [rankX, .intConst m 0] |
There was a problem hiding this comment.
Can we use (@intGeFunc T).opExpr which will hide hard-coded "Int.Ge" and geTy?
let geExpr := .mkApp m (@intGeFunc T).opExpr [rankX, .intConst m 0]
| let adtRankField := .app m (.op m (adtRankFuncName fieldDt.name) | ||
| (.some fieldRankTy)) fieldBvar | ||
| let ltTy := .arrow .int (.arrow .int .bool) | ||
| let ltExpr := LExpr.mkApp m (.op m "Int.Lt" (.some ltTy)) |
There was a problem hiding this comment.
Similarly to line 89, let's use
let ltExpr := .mkApp m (@intLtFunc T).opExpr [adtRankField, adtRankConstr]
| single and mutually recursive). Recursive functions are declared with the `rec` | ||
| keyword, and exactly one parameter must be annotated with `@[cases]` to indicate | ||
| the algebraic datatype argument being recursed on. | ||
| the algebraic datatype argument for per-constructor axiom generation. |
There was a problem hiding this comment.
Are the generated axioms describing the recursive function unfolded with respect to each constructor? Let's clarify this.
| else 1 + zipLen(IntList..tl(xs), IntList..tl(ys)) | ||
| }; | ||
| ``` | ||
|
|
There was a problem hiding this comment.
Can a recursive function have neither @[cases] nor decreasing (which will make termination checking impossible)? My understanding is that this is not true because exactly one argument must be annotated with @[cases] as mentioned in the previous paragraph. Let's state that as a result Strata doesn't accept a recursive function without termination hint.
| @[scope(typeArgs)] b : Bindings, | ||
| @[scope(typeArgs)] r : Type, | ||
| @[scope(b)] preconds : SpacePrefixSepBy SpecElt, | ||
| @[scope(b)] decreases : Option Measure, |
There was a problem hiding this comment.
Does it accept arbitrary expression? If it is targeting a free variable in this patch for now, what about limiting it to an identifier and gradually extending to arbitrary expressions in the future?
| if ListAny..isListAny_nil(l) then from_None() | ||
| else if i == 0 then ListAny..head!(l) | ||
| else List_get(ListAny..tail!(l), i - 1) | ||
| else List_get_non_neg(ListAny..tail!(l), i - 1) |
There was a problem hiding this comment.
Do you have a behind story about this finding & update? :)
| | .eq _ e1 e2 => go e1 implications ++ go e2 implications | ||
| | .abs _ _ _ body => go body implications | ||
| | .quant _ _ _ _ trigger body => | ||
| go trigger implications ++ go body implications |
There was a problem hiding this comment.
It seems .abs and .quant cases can be slightly complicated because visiting their bodies will have to consider bound variables. What about throwing when meeting this kind of case?
atomb
left a comment
atomb
left a comment
There was a problem hiding this comment.
I still want to do a more thorough review myself, but here are a few 🤖 notes so far.
| private def getDecreasesIdx (func : Function) : Option Nat := | ||
| match func.measure with | ||
| | some (.fvar _ id _) => func.inputs.keys.findIdx? (· == id) | ||
| | some _ => none |
There was a problem hiding this comment.
If a user writes decreases someComplexExpr (not a bare variable), this silently falls through to none, which then triggers the error "requires a 'decreases' clause or a '@[cases]' parameter". The error message is misleading — the user did provide a decreases clause, it just wasn't a simple variable reference. A more specific error message like "decreases expression must be a parameter name" would be clearer.
| : Option (Decl × Nat) := do | ||
| let decrIdx ← getDecreasesIdx func | ||
| let inputTys := func.inputs.values | ||
| let decrTy ← inputTys[decrIdx]? |
There was a problem hiding this comment.
If getDecreasesIdx returns an index that's valid for func.inputs.keys but somehow not for func.inputs.values (shouldn't happen with a well-formed ListMap, but defensive), the function returns none and no termination check is generated. The do notation with ← makes this silent.
| | ty :: rest => | ||
| let inner := .quant m .all "" (.some ty) adtRankConstr ltExpr | ||
| rest.foldl (fun body ty => | ||
| .quant m .all "" (.some ty) (LExpr.noTrigger m) body |
There was a problem hiding this comment.
The bound variable name is "" (empty string). While this works with de Bruijn indices, it makes debugging SMT output harder. The generated SMT uses __q0, __q1 etc. which is fine, but if the pretty-printer ever uses these names, they'd be unhelpful.
| @[scope(b)] decreases : Option Measure, | ||
| @[scope(b)] c : r) : RecFnDecl => | ||
| "function " name typeArgs b " : " r indent(2, preconds) "\n{\n " indent(2, c) "\n}"; | ||
| "function " name typeArgs b " : " r indent(2, preconds) "\n" indent(2, decreases) "{\n " indent(2, c) "\n}"; |
There was a problem hiding this comment.
When decreases is none, this produces an extra newline before {. This is cosmetic and may be intentional for readability, but differs from how preconds handles the empty case (no extra whitespace when empty).
5 participants
Issue #, if available:
Description of changes:
TerminationCheckpipeline phase that generates$$termverification procedures forrecFuncBlockdeclarations, asserting thatan
adtRankmeasure strictly decreases at each recursive call siteD..adtRank : D → Intuninterpreted functions and per-constructor axioms for ADTs used as decreasing measures, supporting mutualdatatypes and polymorphic datatypes instantiated at concrete types. These axioms are added as preconditions to the generated termination-checking procedures to avoid extra axioms in other contexts.
decreasessyntax for functions in Core, where thedecreasesis inferred from the@[cases]if not provided.List_get_non_neg/List_set_non_negin the Python runtime were calling the wrong sibling functions (the existing mechanism was probably fine but the termination argument is needlessly complex), andnthin tests was missing anisNilbase case guard.Note that
PrecondElimis not run on these generated procedures, since this will duplicate the precondition assertions from the original program.For the moment, only functions are checked for termination. Procedure termination checking will be added in a future PR.
Tests
-
StrataTest.DL.Lambda.AdtRankAxiomsTests— unit tests foradtRankaxiom generation (IntList, MyNat, RoseTree/RoseList mutual,no-recursive-field, polymorphic)
-
StrataTest.Languages.Core.Tests.TerminationCheckTests— tests covering termination checking, including standard recursion, mutual recursion, error cases, preconditions, polymorphic datatypes, etc.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.