from __future__ import annotations

from abc import ABC, abstractmethod
from dataclasses import dataclass


@dataclass
class LeanResult:
    passed: bool
    error: str
    latency_ms: int
    raw_stderr: str


class LeanBackend(ABC):
    @abstractmethod
    def verify(
        self,
        spec_module: str,
        function_name: str,
        code: str,
        symbol_name: str | None = None,
        extra_imports: list[str] | None = None,
        sample_checks: list[str] | None = None,
    ) -> LeanResult:
        raise NotImplementedError

    @abstractmethod
    def verify_proof(self, spec_module: str, proof_code: str) -> LeanResult:
        raise NotImplementedError