Function verify_function

examples/06_effectful_verifier/python/refine.py:183–234

Verify all ``assert_refined`` calls in *fn* hold given its refinements. 1. Inspect *fn*'s type annotations → create ``defop(int)`` per param + preconditions from ``Gt`` / ``Ge`` metadata. 2. Execute *fn* symbolically → collect VC ``Term``s from ``assert_refined``. 3. Convert each

(fn, lib, kernel)

def verify_function(fn, lib, kernel) -> list[VerificationResult]:
    """Verify all ``assert_refined`` calls in *fn* hold given its refinements.

    1. Inspect *fn*'s type annotations → create ``defop(int)`` per param +
       preconditions from ``Gt`` / ``Ge`` metadata.
    2. Execute *fn* symbolically → collect VC ``Term``s from ``assert_refined``.
    3. Convert each VC to a ``Lean.Expr`` tree and a display string.
    4. Send Expr to Lean (``goalFromExpr`` + ``intros; omega``).
    """
    hints = get_type_hints(fn, include_extras=True)
    params = inspect.signature(fn).parameters

    # Create symbolic vars and extract preconditions.
    var_ops: dict[str, Operation] = {}
    var_names: list[str] = []
    precond_terms = []

    for name in params:
        var_op = defop(int, name=name)
        var_ops[name] = var_op
        var_names.append(name)

        annotation = hints.get(name)
        if hasattr(annotation, "__metadata__"):
            for meta in annotation.__metadata__:
                if isinstance(meta, Gt):
                    precond_terms.append(var_op() > meta.n)
                elif isinstance(meta, Ge):
                    precond_terms.append(var_op() >= meta.n)

    # Execute symbolically and collect VCs.
    vc_terms: list = []

    def _handle_assert(value, refinement):
        if isinstance(refinement, Gt):
            vc_terms.append(value > refinement.n)
        elif isinstance(refinement, Ge):
            vc_terms.append(value >= refinement.n)

    with handler({assert_refined: _handle_assert}):
        fn(**{name: var_ops[name]() for name in params})

    # Convert each VC to Lean.Expr + description string, then verify.
    eb = ExprBuilder(lib)
    results: list[VerificationResult] = []
    for vc_term in vc_terms:
        desc = _build_lean_str(vc_term, var_names, var_ops, precond_terms)
        lean_expr = _build_vc_expr(eb, vc_term, var_names, var_ops, precond_terms)
        ok = _verify_expr(lib, kernel, lean_expr)
        results.append(VerificationResult(desc, ok))

    return results


# ---------------------------------------------------------------------------