tests/test_verification_semantics.py

from __future__ import annotations

from lean_migrate.env.tasks import get_task
from lean_migrate.env.verification_semantics import get_function_semantics


def test_verification_semantics_registry_covers_current_functions() -> None:
    expected_function_names = {
        "rbac_auth": {"findRole", "hasDirectPermission", "canAccess"},
        "pricing_engine": {
            "subtotal",
            "taxRateBps",
            "couponDiscount",
            "loyaltyDiscount",
            "finalPrice",
        },
        "payment_saga": {"transition", "runSaga", "isCharged"},
    }

    for task_id, function_names in expected_function_names.items():
        task = get_task(task_id)
        for function_name in function_names:
            function_spec = task.get_function(function_name)
            assert function_spec is not None

            semantics = get_function_semantics(task_id, function_name)
            assert callable(semantics.oracle)
            assert callable(semantics.lean_value)
            assert callable(semantics.lean_call)