/**
 * SMT Prover — Uses Z3 (WASM) for arithmetic bounds and mutual exclusion proofs.
 * Taint analysis uses graph reachability (no SMT needed).
 *
 * Z3 result strings: 'sat' | 'unsat' | 'unknown'
 * - unsat  → the negation is unsatisfiable → original property IS proven
 * - sat    → counterexample exists → property is NOT proven
 */
export interface ArithmeticBoundInput {
    variable: string;
    expression: string;
    constraints: string[];
    bound: {
        min: number | string;
        max: number | string;
    };
}
export interface MutualExclusionInput {
    condition1: string;
    condition2: string;
    variables: Record<string, 'int' | 'string' | 'bool'>;
}
export interface TaintInput {
    source: string;
    sink: string;
    sanitizers: string[];
}
export interface ProofResult {
    proven: boolean;
    counterexample?: string;
    evidence: string;
}
/**
 * Uses Z3 to prove that `variable = expression` stays within [min, max]
 * given the provided constraints.
 *
 * Strategy:
 *   - Assert all constraints on input variables.
 *   - Assert the NEGATION of the bound: expr < min OR expr > max.
 *   - If UNSAT → bound is always respected → proven.
 *   - If SAT   → counterexample found → not proven.
 */
export declare function proveArithmeticBound(input: ArithmeticBoundInput): Promise<ProofResult>;
/**
 * Proves that condition1 and condition2 cannot both be true simultaneously.
 *
 * For string equality on the SAME variable (`x === "a"` vs `x === "b"`):
 * trivially proven without Z3 (two different string literals can't equal the same var).
 *
 * For numeric conditions: creates Z3 integer variables and checks satisfiability
 * of (condition1 AND condition2). If UNSAT → mutually exclusive.
 */
export declare function proveMutualExclusion(input: MutualExclusionInput): Promise<ProofResult>;
/**
 * Determines whether tainted data flows from `source` to `sink` without
 * passing through a sanitizer.
 *
 * Algorithm:
 *   1. Extract the source variable name from the source path.
 *   2. For each sanitizer, check if it transforms the source into a new variable.
 *   3. Check if the sink uses the original tainted variable directly.
 *      If the sink uses only sanitized forms, the data is taint-free.
 *
 * This is intentionally a string-matching approximation — full taint analysis
 * would require an AST; this handles the common cases tested in the spec.
 */
export declare function proveTaintFree(input: TaintInput): Promise<ProofResult>;