import type { EdictModule, FunctionDef } from "../ast/nodes.js";
import type { StructuredError } from "../errors/structured-errors.js";
import { type AnalysisDiagnostic } from "../errors/structured-errors.js";
import type { SolverContext } from "./solver-context.js";
/**
 * Result of contract verification: errors (violations) + diagnostics (skipped checks).
 */
export interface ContractVerifyResult {
    errors: StructuredError[];
    diagnostics: AnalysisDiagnostic[];
    /** Cache hit/miss statistics for this verification run. */
    cacheStats?: {
        hits: number;
        misses: number;
    };
}
/** Options for contractVerify. */
export interface ContractVerifyOptions {
    /**
     * When true (default), uncached verifications run in a worker thread
     * to keep the main event loop responsive. Set to false for tests
     * that need to avoid worker overhead or test verification logic directly.
     */
    useWorker?: boolean;
}
/** Clear the verification cache. Used by tests for isolation. */
export declare function clearVerificationCache(): void;
/**
 * Verify all pre/post contracts in the module using Z3 SMT solver.
 *
 * For each postcondition, checks: `preconditions ∧ ¬postcondition`.
 * Results: unsat → proven, sat → counterexample error, unknown → timeout error.
 * Caches proven results per-function. Uncached verifications run in a worker thread
 * by default to keep the MCP server responsive.
 *
 * @param module - A validated, resolved, type-checked, and effect-checked Edict module
 * @param options - Optional: `{ useWorker?: boolean }` — set `false` for tests
 * @returns `{ errors, diagnostics, cacheStats }` — contract violations, skipped-check diagnostics, and cache statistics
 */
export declare function contractVerify(module: EdictModule, options?: ContractVerifyOptions): Promise<ContractVerifyResult>;
/**
 * Worker entry point — called from the inline worker script.
 * Receives the module and a list of work items specifying which
 * functions to verify and which phase (post or callsite).
 * Exported so the worker can import and call it.
 */
export declare function contractVerifyWorkerEntry(module: EdictModule, workItems: {
    fnName: string;
    phase: "post" | "callsite";
}[]): Promise<VerifyFunctionResult>;
interface VerifyFunctionResult {
    errors: StructuredError[];
    diagnostics: AnalysisDiagnostic[];
}
/**
 * Verify all contracts for a single function using Z3.
 *
 * For each postcondition: translates preconditions + body + negated postcondition
 * into Z3 constraints. If unsatisfiable → proven; if satisfiable → counterexample.
 *
 * @param ctx - Z3 context instance
 * @param fn - The function definition whose contracts to verify
 * @param module - The containing module (needed for callsite precondition analysis)
 * @returns `{ errors, diagnostics }` — contract violation errors and skipped-check diagnostics
 */
export declare function verifyFunction(ctx: SolverContext, fn: FunctionDef, module: EdictModule): Promise<VerifyFunctionResult>;
/**
 * Verify that a function's call sites satisfy callee preconditions.
 * For each call f(...args) where f has preconditions, check that
 * the caller's context (params + own preconditions) implies each
 * callee precondition with args substituted for params.
 */
export declare function verifyCallSitePreconditions(ctx: SolverContext, callerFn: FunctionDef, functionDefs: Map<string, FunctionDef>, module: EdictModule): Promise<VerifyFunctionResult>;
/**
 * Synchronous contract verification using a solver with checkSync() support.
 *
 * Same semantics as contractVerify() but fully synchronous — designed for
 * environments like QuickJS where async/await is unavailable.
 *
 * @param module - A validated, resolved, type-checked, and effect-checked Edict module
 * @param ctx - A SolverContext whose Solver implements checkSync()
 * @returns `{ errors, diagnostics }` — contract violations and skipped-check diagnostics
 */
export declare function contractVerifySync(module: EdictModule, ctx: SolverContext): ContractVerifyResult;
export {};
//# sourceMappingURL=verify.d.ts.map