import type { TViolation } from "../types.js";
import type { TValidatorContext } from "./context.js";
/**
 * S-1 — FK soundness.
 *
 * For every entity in the context, check that its foreign-key fields
 * resolve to an existing target:
 * - `expression.parentId` (when non-null) resolves to another expression
 *   in the context.
 * - Claim-bound variable's `claimId` resolves to a claim in the context.
 * - Premise-bound variable's `boundPremiseId` resolves to a premise in the
 *   context **only when** the binding is internal
 *   (`boundArgumentId === argument.id`); externally-bound variables
 *   resolve in a different argument and are not S-1's concern.
 *
 * Premise `argumentId`/`argumentVersion` matching its container argument
 * is checked here too (same-FK-soundness umbrella).
 */
export declare function validateS1(ctx: TValidatorContext): readonly TViolation[];
/**
 * S-2 — Operator types. Every expression's `type` is one of `variable`,
 * `operator`, `formula`. For operator-typed expressions, the `operator`
 * field is one of `not`, `and`, `or`, `xor`, `implies`, `iff`.
 */
export declare function validateS2(ctx: TValidatorContext): readonly TViolation[];
/**
 * S-3 — Variable required reference. Every variable has either a claim ref
 * or a premise ref, not both, not neither.
 */
export declare function validateS3(ctx: TValidatorContext): readonly TViolation[];
/**
 * S-4 — No cycles. The expression tree of every premise (parent-pointer
 * graph) is acyclic.
 */
export declare function validateS4(ctx: TValidatorContext): readonly TViolation[];
/**
 * S-5 — Root-only IMPLIES/IFF. Within a single premise's AST, `implies`
 * and `iff` may appear at most once and only at the root (parentId === null).
 */
export declare function validateS5(ctx: TValidatorContext): readonly TViolation[];
/**
 * S-6 — Premise type discriminator consistency. `type='derivation'`
 * premises have a non-null `derivedClaimId`; `type='freeform'` premises
 * have no `derivedClaimId` (or it is null/undefined).
 *
 * `TCoreFreeformPremise` and `TCoreDerivationPremise` are both
 * `additionalProperties: true` in their TypeBox schemas, so a freeform
 * premise CAN carry a stray `derivedClaimId` field at runtime even
 * though the TS shape doesn't surface it. We use the `in` operator and
 * a narrow shape cast to read the field as `unknown` rather than the
 * earlier `as unknown` double-cast.
 */
export declare function validateS6(ctx: TValidatorContext): readonly TViolation[];
/**
 * S-7 — Claim type immutability. Creation-time invariant enforced by
 * `ClaimLibrary.update()` via the engine-error code `CLAIM_TYPE_IMMUTABLE`.
 * The AST-level validator is intentionally a no-op; callers cannot
 * observe a type-mutation event from a static argument snapshot.
 */
export declare function validateS7(_ctx: TValidatorContext): readonly TViolation[];
/**
 * S-8 — Binary operator arity. `implies` and `iff` have exactly 2
 * children. Child ordering (antecedent at lower position, consequent at
 * higher) is conveyed by the relative sibling positions — any
 * `[a, b]` with `a < b` is semantically equivalent to `[0, 1]`. The
 * absolute position values are sibling-ordering metadata maintained by
 * the mutation primitives and are not a Structural invariant; sibling
 * uniqueness is enforced separately by S-9.
 *
 * Pre-1.0.2 S-8 also pinned positions to literal `[0, 1]`. That check
 * was over-strict — it false-flagged existing arguments whose binary
 * operators sat at midpoint-spaced positions (e.g., `[0, 1073741823]`,
 * the default `wrapExpression` spacing for variadic operators). The
 * position pin was relaxed in 1.0.2 to arity-only.
 */
export declare function validateS8(ctx: TValidatorContext): readonly TViolation[];
/**
 * S-9 — Sibling position uniqueness. Within a single parent's children,
 * no two siblings share the same `position`.
 */
export declare function validateS9(ctx: TValidatorContext): readonly TViolation[];
/**
 * S-10 — Entity ID uniqueness. Within an argument, premises, expressions,
 * and variables each have unique IDs in their respective collection.
 */
export declare function validateS10(ctx: TValidatorContext): readonly TViolation[];
/**
 * S-11 — Variable symbol uniqueness. Within a single argument, no two
 * variables share the same `symbol`.
 */
export declare function validateS11(ctx: TValidatorContext): readonly TViolation[];
/**
 * S-12 — NOT unary arity. Every `not` expression has exactly one child.
 */
export declare function validateS12(ctx: TValidatorContext): readonly TViolation[];
/**
 * S-13 — Formula unary arity. Every `formula` expression has exactly one
 * child.
 */
export declare function validateS13(ctx: TValidatorContext): readonly TViolation[];
/**
 * S-14 — Derivation premise root operator. Every `type='derivation'`
 * premise's root expression is one of `variable`, `implies`, or `iff`.
 * (`iff` is Structurally allowed; D-1 narrows the populated form to
 * `implies` only — Derivable concern.)
 */
export declare function validateS14(ctx: TValidatorContext): readonly TViolation[];
export declare function validateStructural(ctx: TValidatorContext): readonly TViolation[];
//# sourceMappingURL=structural.d.ts.map