/** Sorts of the variables the IR can declare. Kept minimal and concrete so the
 *  obligation maps cleanly onto a quantifier-free SMT theory. */
export type IRSort = 'Bool' | 'Int' | 'String';
/** A declared variable in the feasibility obligation. */
export interface IRVariable {
    name: string;
    sort: IRSort;
    /** Where this variable comes from: the requested action or the granted
     *  delegation envelope. Advisory metadata; does not affect the obligation. */
    origin: 'action' | 'delegation';
    /** Human-readable note on what the variable models. */
    comment: string;
}
/** The relational/logical operators the IR constraint language supports.
 *  Deliberately small: equality, integer comparison, set membership, boolean. */
export type IRConstraintKind = 'eq' | 'le' | 'ge' | 'member' | 'bool';
/** A single feasibility constraint. */
export interface IRConstraint {
    /** Stable identifier for this constraint, e.g. 'scope_granted'. Used to sort
     *  constraints into a deterministic order and to label SMT assertions. */
    id: string;
    kind: IRConstraintKind;
    /** Left operand: a declared variable name. */
    lhs: string;
    /** Right operand for eq/le/ge: a variable name or a literal. Absent for
     *  'bool' (the lhs boolean must hold) and for 'member' (see set). */
    rhs?: {
        var: string;
    } | {
        lit: string | number | boolean;
    };
    /** Membership set for 'member' constraints. Sorted strings. */
    set?: string[];
    /** Human-readable explanation of the obligation this constraint encodes. */
    comment: string;
}
/** A compiled feasibility obligation. This is the IR. */
export interface FeasibilityIR {
    /** IR format version. Bump on any breaking change to the structure. */
    version: string;
    /** sha256 hex of the canonical inputs this IR was compiled from. Lets a
     *  consumer tie an IR back to its (policy, delegation) source without
     *  replaying the compile. */
    sourceHash: string;
    /** Logic the obligation targets, e.g. 'QF_SLIA' (quantifier-free strings +
     *  linear integer arithmetic). Advisory; this module emits but never solves. */
    logic: string;
    /** Declared variables, sorted by name. */
    variables: IRVariable[];
    /** Constraints, sorted by id. The obligation is the conjunction of these. */
    constraints: IRConstraint[];
    /** Honest-scope note: what compiling this IR establishes and what it does not. */
    scopeNote: {
        asserts: string;
        does_not_assert: string[];
    };
}
//# sourceMappingURL=ir.d.ts.map