export type Primitive = string | number | boolean | null;
export type JsonValue = Primitive | JsonValue[] | {
    [key: string]: JsonValue;
};
export type ValueType = {
    kind: "enum";
    values: readonly string[];
} | {
    kind: "domain";
    name: string;
} | {
    kind: "boolean";
} | {
    kind: "range";
    min: number;
    max: number;
} | {
    kind: "null";
} | {
    kind: "option";
    value: ValueType;
} | {
    kind: "union";
    members: readonly ValueType[];
};
export type Expr = {
    kind: "lit";
    value: JsonValue;
} | {
    kind: "param";
    name: string;
} | {
    kind: "var";
    name: string;
} | {
    kind: "index";
    target: Expr;
    key: Expr;
} | {
    kind: "set";
    values: readonly Expr[];
} | {
    kind: "and";
    values: readonly Expr[];
} | {
    kind: "or";
    values: readonly Expr[];
} | {
    kind: "not";
    value: Expr;
} | {
    kind: "eq";
    left: Expr;
    right: Expr;
} | {
    kind: "lte";
    left: Expr;
    right: Expr;
} | {
    kind: "in";
    elem: Expr;
    set: Expr;
} | {
    kind: "count";
    domain: string;
    binder: string;
    where: Expr;
} | {
    kind: "forall";
    domain: string;
    binder: string;
    where: Expr;
};
export type Update = {
    kind: "setVar";
    name: string;
    value: Expr;
} | {
    kind: "setMap";
    name: string;
    key: Expr;
    value: Expr;
};
export interface ScalarVarDef {
    kind: "scalar";
    type: ValueType;
    initial: Expr;
}
export interface MapVarDef {
    kind: "map";
    domain: string;
    codomain: ValueType;
    initial: Expr;
}
export type VariableDef = ScalarVarDef | MapVarDef;
export interface ActionDef {
    actor?: string;
    params: Record<string, string>;
    guard: Expr;
    updates: readonly Update[];
}
export interface InvariantDef {
    description: string;
    formula: Expr;
}
export interface PropertyDef {
    description: string;
    formula: string;
}
export interface ModelValuesDomainDef {
    kind: "modelValues";
    prefix: string;
    size: number;
    symmetry?: boolean;
}
export interface IdsDomainDef {
    kind: "ids";
    prefix: string;
    size: number;
}
export interface DomainValuesDef {
    kind: "values";
    values: readonly string[];
}
export type ProofDomainDef = ModelValuesDomainDef | IdsDomainDef | DomainValuesDef;
export interface PgColumnExpr {
    kind: "pgColumn";
    name: string;
}
export interface PgLiteralExpr {
    kind: "pgLiteral";
    value: Primitive;
}
export type RowValueExpr = PgColumnExpr | PgLiteralExpr;
export type RowPredicateExpr = {
    kind: "pgEq";
    left: RowValueExpr;
    right: RowValueExpr;
} | {
    kind: "pgInSet";
    target: RowValueExpr;
    values: readonly Primitive[];
} | {
    kind: "pgAnd";
    values: readonly RowPredicateExpr[];
} | {
    kind: "pgOr";
    values: readonly RowPredicateExpr[];
} | {
    kind: "pgNot";
    value: RowPredicateExpr;
} | {
    kind: "pgIsNull";
    value: RowValueExpr;
} | {
    kind: "pgIsNotNull";
    value: RowValueExpr;
};
export interface PgUniqueWhereConstraintDef {
    kind: "pgUniqueWhere";
    name: string;
    schema: string;
    table: string;
    columns: readonly string[];
    where: RowPredicateExpr;
    backsInvariant?: string;
}
export interface PgCheckConstraintDef {
    kind: "pgCheck";
    name: string;
    schema: string;
    table: string;
    predicate: RowPredicateExpr;
    backsInvariant?: string;
}
export type StorageConstraintDef = PgUniqueWhereConstraintDef | PgCheckConstraintDef;
export interface ProofBudgets {
    maxEstimatedStates?: number;
    maxEstimatedBranching?: number;
}
export interface ProofTierChecks {
    deadlock?: boolean;
}
export interface ProofTierDef {
    domains: Record<string, ProofDomainDef>;
    budgets?: ProofBudgets;
    checks?: ProofTierChecks;
    invariants?: readonly string[];
    properties?: readonly string[];
    graphEquivalence?: boolean;
}
export interface MachineProofDef {
    defaultTier: string;
    tiers: Record<string, ProofTierDef>;
}
export interface RuntimeAdapterDef {
    schema?: string;
    table: string;
    rowDomain: string;
    keyColumn: string;
    keySqlType: "text" | "uuid" | "bigint";
}
export interface MachineMetadata {
    ownedTables?: readonly string[];
    ownedColumns?: Record<string, readonly string[]>;
    allowedWriterModules?: readonly string[];
    storageConstraints?: readonly StorageConstraintDef[];
    runtimeAdapter?: RuntimeAdapterDef;
}
export interface MachineDef {
    version: 2;
    moduleName: string;
    variables: Record<string, VariableDef>;
    actions: Record<string, ActionDef>;
    invariants: Record<string, InvariantDef>;
    properties?: Record<string, PropertyDef>;
    proof: MachineProofDef;
    metadata?: MachineMetadata;
}
export interface MachineEstimateFactor {
    name: string;
    formula: string;
    value: string;
}
export interface MachineEstimate {
    tier: string;
    totalStateCount: string;
    totalBranching: string;
    variables: readonly MachineEstimateFactor[];
    actions: readonly MachineEstimateFactor[];
    withinBudget: boolean;
    budgetViolations: readonly string[];
}
export interface ResolvedProofTier {
    name: string;
    domains: Record<string, ProofDomainDef>;
    symmetryDomains: readonly string[];
    budgets: ProofBudgets;
    checks: Required<ProofTierChecks>;
    invariants: readonly string[];
    properties: readonly string[];
    graphEquivalence: boolean;
}
export interface ResolvedMachineDef extends MachineDef {
    domains: Record<string, readonly string[]>;
    resolvedTier: ResolvedProofTier;
    estimate: MachineEstimate;
}
export declare const defineMachine: <const M extends MachineDef>(machine: M) => M;
export declare const lit: (value: JsonValue) => Expr;
export declare const param: (name: string) => Expr;
export declare const variable: (name: string) => Expr;
export declare const index: (target: Expr, key: Expr) => Expr;
export declare const setOf: (...values: readonly Expr[]) => Expr;
export declare function and(...values: readonly Expr[]): Expr;
export declare function and(...values: readonly RowPredicateExpr[]): RowPredicateExpr;
export declare function or(...values: readonly Expr[]): Expr;
export declare function or(...values: readonly RowPredicateExpr[]): RowPredicateExpr;
export declare function not(value: Expr): Expr;
export declare function not(value: RowPredicateExpr): RowPredicateExpr;
export declare function eq(left: Expr, right: Expr): Expr;
export declare function eq(left: Primitive | RowValueExpr, right: Primitive | RowValueExpr): RowPredicateExpr;
export declare const lte: (left: Expr, right: Expr) => Expr;
export declare const isin: (elem: Expr, set: Expr) => Expr;
export declare const count: (domain: string, binder: string, where: Expr) => Expr;
export declare const forall: (domain: string, binder: string, where: Expr) => Expr;
export declare const col: (name: string) => RowValueExpr;
export declare const inSet: (target: Primitive | RowValueExpr, values: readonly Primitive[]) => RowPredicateExpr;
export declare const isNull: (value: Primitive | RowValueExpr) => RowPredicateExpr;
export declare const isNotNull: (value: Primitive | RowValueExpr) => RowPredicateExpr;
export declare const enumType: (...values: readonly string[]) => ValueType;
export declare const domainType: (name: string) => ValueType;
export declare const boolType: () => ValueType;
export declare const rangeType: (min: number, max: number) => ValueType;
export declare const nullType: () => ValueType;
export declare const optionType: (value: ValueType) => ValueType;
export declare const unionType: (...members: readonly ValueType[]) => ValueType;
export declare const scalarVar: (type: ValueType, initial: Expr) => ScalarVarDef;
export declare const mapVar: (domain: string, codomain: ValueType, initial: Expr) => MapVarDef;
export declare const setVar: (name: string, value: Expr) => Update;
export declare const setMap: (name: string, key: Expr, value: Expr) => Update;
export declare const modelValues: (prefix: string, options: {
    size: number;
    symmetry?: boolean;
}) => ModelValuesDomainDef;
export declare const ids: (options: {
    size: number;
    prefix?: string;
}) => IdsDomainDef;
export declare const domainValues: (...values: readonly string[]) => DomainValuesDef;
export declare const pgUniqueWhere: (constraint: Omit<PgUniqueWhereConstraintDef, "kind" | "schema"> & {
    schema?: string;
}) => PgUniqueWhereConstraintDef;
export declare const pgCheck: (constraint: Omit<PgCheckConstraintDef, "kind" | "schema"> & {
    schema?: string;
}) => PgCheckConstraintDef;