import type { StructuredError, AnalysisDiagnostic, VerificationCoverage } from "../errors/structured-errors.js";
import type { TypedModuleInfo } from "../checker/check.js";
import type { EdictModule } from "../ast/nodes.js";
export interface IncrementalCheckResult {
    ok: boolean;
    errors: StructuredError[];
    /** The validated module AST (only present when ok === true) */
    module?: EdictModule;
    /** Side-table of inferred types (only present when ok === true) */
    typeInfo?: TypedModuleInfo;
    /** INFO-level diagnostics about skipped analyses */
    diagnostics?: AnalysisDiagnostic[];
    /** Summary of what was verified vs. skipped */
    coverage?: VerificationCoverage;
    /** Cache hit/miss statistics for contract verification */
    cacheStats?: {
        hits: number;
        misses: number;
    };
    /** Definitions that were re-verified by Z3 */
    rechecked: string[];
    /** Definitions for which Z3 verification was skipped (unchanged) */
    skipped: string[];
}
/**
 * Incremental check: runs the full pipeline on `after`, but scopes Phase 4
 * (Z3 contract verification) to only the definitions that changed relative
 * to `before` (plus their transitive dependents).
 *
 * If `before` is invalid or diffing fails, falls back to full check.
 */
export declare function incrementalCheck(before: EdictModule, after: EdictModule): Promise<IncrementalCheckResult>;
//# sourceMappingURL=check.d.ts.map