Shared definitions for the graph CROWN engine.

This file contains the rank-one tensor representation, parameter stores, interval boxes, shape permutation helpers, and tensor casts used by the IBP, derivative, affine, CROWN, and backward objective passes.

structure NN.MLTheory.CROWN.Graph.FlatTensor (α : Type) [TorchLean.Storage α] [Context α] : Type

An existentially sized rank-one tensor used by the flat LiRPA engine.

Graph nodes carry dimensions discovered while lowering, so the dimension cannot always appear in the surrounding static type. The field n is the hidden tensor dimension, not duplicate runtime storage.

• n : ℕ

  Number of scalar entries.

• v : TorchLean.Tensor α [self.n]

  Rank-one tensor payload (shape .dim n .scalar).

structure NN.MLTheory.CROWN.Graph.LinParams (α : Type) [TorchLean.Storage α] [Context α] : Type

Parameters for a linear layer y = W*x + b in flattened form.

m is the output dimension and n is the input dimension.

• m : ℕ

  Output dimension.

• n : ℕ

  Input dimension.

• w : TorchLean.Tensor α [self.m, self.n]

  Weight matrix W (shape m × n).

• b : TorchLean.Tensor α [self.m]

  Bias tensor b (shape m).

structure NN.MLTheory.CROWN.Graph.MatParams (α : Type) [TorchLean.Storage α] [Context α] : Type

Matrix parameters for bias-free matmul: y = W x.

• m : ℕ

  Output dimension.

• n : ℕ

  Input dimension.

• w : TorchLean.Tensor α [self.m, self.n]

  Weight matrix W (shape m × n).

def NN.MLTheory.CROWN.Graph.axisCoordinateOfFlat (shape : Spec.Shape) (axis idx : ℕ) : ℕ

Coordinate on axis corresponding to a row-major flat index.

def NN.MLTheory.CROWN.Graph.batchNormEvalScale {α : Type} [TorchLean.Storage α] [Context α] (config : IR.BatchNormEvalParams α) (ci : Fin config.c) : α

Eval BatchNorm scale for one channel.

def NN.MLTheory.CROWN.Graph.batchNormEvalBias {α : Type} [TorchLean.Storage α] [Context α] (config : IR.BatchNormEvalParams α) (ci : Fin config.c) : α

Eval-mode BatchNorm bias after folding one channel's running statistics into an affine map.

def NN.MLTheory.CROWN.Graph.batchNormEvalLinear? {α : Type} [TorchLean.Storage α] [Context α] (parentShape : Spec.Shape) (channelAxis : ℕ) (config : IR.BatchNormEvalParams α) : Option (LinParams α)

Build the exact diagonal affine form for eval-mode BatchNorm on an arbitrary channel axis.

The graph records the channel axis while the payload stores one scale and bias per channel. A malformed axis or mismatched channel extent has no verifier transfer rule.

structure NN.MLTheory.CROWN.Graph.ParamStore (α : Type) [TorchLean.Storage α] [Context α] : Type

Parameters keyed by node id (weights, biases, constants, and seeded input boxes).

This is kept compact: it is the graph interpreter used to run IBP/CROWN on a pure Graph without pulling in a heavyweight runtime.

• inputBoxes : Std.HashMap ℕ (FlatBox α)

  Seed boxes for designated input nodes (id -> FlatBox).

• constVals : Std.HashMap ℕ (FlatTensor α)

  Constants (id -> FlatTensor).

• linearWB : Std.HashMap ℕ (LinParams α)

  Linear layer params (id -> (W,b)).

• matmulW : Std.HashMap ℕ (MatParams α)

  Matmul params (id -> W) for bias-free multiplication.

• convCfg : Std.HashMap ℕ (IR.ConvParams α)

  Convolution specs (id -> convolution configuration).

• batchNormEval : Std.HashMap ℕ (IR.BatchNormEvalParams α)

  Eval-mode BatchNorm parameters (id -> gamma/beta/running stats).

• layerNorm : Std.HashMap ℕ (IR.LayerNormParams α)

  Affine LayerNorm parameters keyed by node id.

  Last-axis value bounds use the stored scale, bias, and epsilon. An absent payload selects unit scale, zero bias, and default epsilon. Payload derivative bounds remain unresolved until a rule accounts for all three parameters.

def NN.MLTheory.CROWN.Graph.ParamStore.seedInputBox {α : Type} [TorchLean.Storage α] [Context α] (ps : ParamStore α) (inputId : ℕ) (xB : FlatBox α) : ParamStore α

Insert an input interval box for a graph node.

def NN.MLTheory.CROWN.Graph.ParamStore.seedLInfBall {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (ps : ParamStore α) (inputId : ℕ) (center : TorchLean.Tensor α s) (eps : α) : ParamStore α

Seed a graph input with a uniform ℓ∞ box around a shaped tensor.

def NN.MLTheory.CROWN.Graph.convTransferSupported {α : Type} [TorchLean.Storage α] [Context α] (configuration : IR.ConvConfig) (parameters : IR.ConvParams α) (parentShape outShape : Spec.Shape) : Bool

Whether the current dense convolution transfer exactly matches the corresponding IR semantics.

The flattened CROWN rule implements channel-first convolution without leading batch axes, channel groups, dilation, or asymmetric padding. The payload must also agree with the configuration stored in the graph node; otherwise executable IR evaluation and bound propagation would denote different operators.

def NN.MLTheory.CROWN.Graph.crownNodeSemanticsSupported {α : Type} [TorchLean.Storage α] [Context α] (nodes : Array Node) (ps : ParamStore α) (id : ℕ) : Bool

Check the graph-level semantic restrictions imposed by the current CROWN engine.

Unsupported convolutions, non-leading-axis concatenation, and LayerNorm over more than the last axis are left without bounds. LayerNorm payloads must match that axis's shape exactly. This predicate checks the common shape contract; individual transfers also check their arithmetic and derivative requirements.

def NN.MLTheory.CROWN.Graph.crownGraphSemanticsSupported {α : Type} [TorchLean.Storage α] [Context α] (g : Graph) (ps : ParamStore α) : Bool

Whether every node in a graph is interpreted exactly by the current CROWN engine.

def NN.MLTheory.CROWN.Graph.outputBox? {α : Type} [TorchLean.Storage α] [Context α] (boxes : Array (Option (FlatBox α))) (outId : ℕ) : Except String (FlatBox α)

Read a node's interval box from an IBP-style result array.

@[instance_reducible]

instance NN.MLTheory.CROWN.Graph.instInhabitedFlatBox {α : Type} [TorchLean.Storage α] [Context α] : Inhabited (FlatBox α)

Default inhabitant for FlatBox (a 0-dimensional box at 0).

def NN.MLTheory.CROWN.Graph.boxMulElem {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (B1 B2 : FlatBox α) : Option (FlatBox α)

Elementwise product of two FlatBoxes (interval product per component). Requires equal dims.

def NN.MLTheory.CROWN.Graph.chainMul {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (dZ dF : FlatBox α) : Option (FlatBox α)

Chain-rule multiplication for derivative intervals. Returns none on dimension mismatch.

def NN.MLTheory.CROWN.Graph.toFlatBox {α : Type} [TorchLean.Storage α] [Context α] (n : ℕ) (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : FlatBox α

Convert a dependent Box of shape .dim n .scalar into a FlatBox with dim := n.

def NN.MLTheory.CROWN.Graph.ofFlatBox {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) : Box α (Spec.Shape.dim B.dim Spec.Shape.scalar)

Convert a FlatBox to a dependent Box at shape .dim B.dim .scalar.

def NN.MLTheory.CROWN.Graph.boxAdd {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (B1 B2 : FlatBox α) : FlatBox α

Add two flat interval boxes coordinatewise; dimension mismatches preserve the left box.

def NN.MLTheory.CROWN.Graph.boxSub {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (B1 B2 : FlatBox α) : FlatBox α

Interval subtraction on FlatBox endpoints (sound enclosure).

def NN.MLTheory.CROWN.Graph.boxSum {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (B : FlatBox α) : FlatBox α

Sum all coordinates of a flat box with directed accumulation.

def NN.MLTheory.CROWN.Graph.boxMean? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (B : FlatBox α) : Option (FlatBox α)

Average all coordinates of a nonempty flat box with directed division.

def NN.MLTheory.CROWN.Graph.boxRelu {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) : FlatBox α

Apply ReLU to both endpoints of a FlatBox (monotone activation, so endpoints suffice).

def NN.MLTheory.CROWN.Graph.boxAbs {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) : FlatBox α

Componentwise absolute value bounds. Soundly encloses abs over each interval component.

traverseFin is plumbing, so it lives in Internal like the rest of the codebase's plumbing. This namespace used to be called boxUnaryEnclosure, after the function below that is its only caller, which was misleading twice over: that caller is actually spelled boxUnaryEnclosure?, and traverseFin knows nothing about boxes or enclosures.

def NN.MLTheory.CROWN.Graph.Internal.traverseFin {β : Type} {n : ℕ} (f : Fin n → Option β) : Option (Fin n → β)

Traverse a finite family without converting its index to an untyped list.

theorem NN.MLTheory.CROWN.Graph.Internal.traverseFin_eq_some_iff {β : Type} {n : ℕ} {f : Fin n → Option β} {g : Fin n → β} : traverseFin f = some g ↔ ∀ (i : Fin n), f i = some (g i)

traverseFin succeeds exactly when every component does, and then returns those components.

This is the only fact the box operations need about it: it lets a coordinatewise enclosure argument be read off from the aggregate Option without ever mentioning the dif in the definition.

def NN.MLTheory.CROWN.Graph.boxUnaryEnclosure? {α : Type} [TorchLean.Storage α] [Context α] [NonlinearBoundOps α] (enclose : α → α → Option (α × α)) (B : FlatBox α) : Option (FlatBox α)

Apply a scalar interval enclosure coordinatewise to a flat box.

def NN.MLTheory.CROWN.Graph.boxSqrt? {α : Type} [TorchLean.Storage α] [Context α] [NonlinearBoundOps α] (B : FlatBox α) : Option (FlatBox α)

Componentwise square-root bounds, failing when a coordinate interval reaches below zero.

def NN.MLTheory.CROWN.Graph.boxSoftplus? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (B : FlatBox α) : Option (FlatBox α)

Softplus bounds, applied independently at every tensor coordinate.

def NN.MLTheory.CROWN.Graph.boxSafeLog? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (B epsilon : FlatBox α) : Option (FlatBox α)

SafeLog bounds with one shared scalar epsilon interval.

The epsilon parent must contain one scalar. Keeping this check here makes direct graph construction follow the same contract as the typed builder and IR shape inference.

def NN.MLTheory.CROWN.Graph.boxInv? {α : Type} [TorchLean.Storage α] [Context α] [NonlinearBoundOps α] (B : FlatBox α) : Option (FlatBox α)

Componentwise reciprocal bounds, failing when an input coordinate interval crosses zero.

def NN.MLTheory.CROWN.Graph.derivBoxExp? {α : Type} [TorchLean.Storage α] [Context α] [NonlinearBoundOps α] (zB : FlatBox α) : Option (FlatBox α)

Derivative range for exp; exp' = exp.

def NN.MLTheory.CROWN.Graph.derivBoxLog? {α : Type} [TorchLean.Storage α] [Context α] [NonlinearBoundOps α] (zB : FlatBox α) : Option (FlatBox α)

Derivative range for log; log' x = 1/x on a strictly positive interval.

def NN.MLTheory.CROWN.Graph.secondDerivBoxLog? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (zB : FlatBox α) : Option (FlatBox α)

Second-derivative range for log; log'' x = -1/x² on a positive interval.

def NN.MLTheory.CROWN.Graph.boxNeg {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) : FlatBox α

Negate an interval box by swapping and negating its endpoints.

def NN.MLTheory.CROWN.Graph.permuteSomeTensor? {α : Type} [TorchLean.Storage α] [Context α] (v : Spec.SomeTensor α) (perm : Array ℕ) : Option (Spec.SomeTensor α)

Apply a full axis permutation to a shape-tagged tensor when the permutation is valid.

def NN.MLTheory.CROWN.Graph.flatAxisPermutation? (sourceShape : Spec.Shape) (perm : Array ℕ) (n : ℕ) : Option (Fin n → Fin n)

Return the flat-coordinate permutation induced by an axis permutation.

perm follows the tensor convention used by Shape.permute?: output axis i is read from input axis perm[i]. The resulting function therefore maps each output flat coordinate to the input flat coordinate from which its value is taken. Invalid permutations and inconsistent dimensions are rejected.

def NN.MLTheory.CROWN.Graph.boxMaxElem {α : Type} [TorchLean.Storage α] [Context α] (B1 B2 : FlatBox α) : FlatBox α

Componentwise max bounds: max(x,y) over interval boxes.

def NN.MLTheory.CROWN.Graph.boxMinElem {α : Type} [TorchLean.Storage α] [Context α] (B1 B2 : FlatBox α) : FlatBox α

Componentwise min bounds: min(x,y) over interval boxes.

def NN.MLTheory.CROWN.Graph.boxSquare {α : Type} [TorchLean.Storage α] [Context α] (B : FlatBox α) : FlatBox α

Componentwise square of an interval box: for each component [l,u] produce [min (l^2,u^2), max (l^2,u^2)], with 0 as the minimum when the interval crosses 0.

The body is exposed because the proof layer theorem module unfolds this executable rule when proving dimension preservation and pointwise enclosure.

def NN.MLTheory.CROWN.Graph.intervalMul {α : Type} [Context α] (aLo aHi bLo bHi : α) : α × α

Interval multiplication for scalar endpoints: given [aLo,aHi] and [bLo,bHi], return bounds on the product.

def NN.MLTheory.CROWN.Graph.lastDimLen : Spec.Shape → ℕ

Length of the last axis of a shape; scalars are treated as length one.

def NN.MLTheory.CROWN.Graph.ibpUnflatten {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (dim : ℕ) (t : TorchLean.Tensor α [dim]) (h : dim = s.size) : TorchLean.Tensor α s

Reinterpret a flattened tensor as shape s when the element counts agree.

def NN.MLTheory.CROWN.Graph.ibpBroadcastTo {α : Type} [TorchLean.Storage α] [Context α] (s₁ s₂ : Spec.Shape) (Xin : FlatBox α) : Option (FlatBox α)

IBP rule for broadcasting a flattened input box to a target shape.

def NN.MLTheory.CROWN.Graph.ibpReduceSumAxis {α : Type} [TorchLean.Storage α] [Context α] (axis : ℕ) (Xin : FlatBox α) (s : Spec.Shape) : Option (FlatBox α)

IBP rule for reducing a shaped box by summing along one axis.

def NN.MLTheory.CROWN.Graph.ibpReduceMeanAxis {α : Type} [TorchLean.Storage α] [Context α] (axis : ℕ) (Xin : FlatBox α) (s : Spec.Shape) : Option (FlatBox α)

IBP rule for reducing a shaped box by averaging along one axis.

def NN.MLTheory.CROWN.Graph.ibpSoftmaxRange {α : Type} [TorchLean.Storage α] [Context α] (s : Spec.Shape) (dim : ℕ) : FlatBox α

Format-independent softmax enclosure on a flattened tensor.

A singleton row is exactly one. Every coordinate of a longer row lies in [0,1]. This deliberately forgoes the tighter exponential formula above so executable checking does not assume a directed transcendental implementation that its scalar backend has not supplied.

Hard-masked softmax IBP (last axis)

Blocked coordinates have weight zero. An allowed coordinate lies in [0,1], and it has weight one when it is the only allowed coordinate in its row. These bounds do not evaluate exp or division, so they remain valid for executable endpoint types whose BoundOps instance covers only directed arithmetic. A tighter transfer rule requires separately certified directed bounds for transcendental operations.

def NN.MLTheory.CROWN.Graph.ibpHardMaskedSoftmaxLastTensor {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} : TorchLean.Tensor α s → TorchLean.Tensor α s → TorchLean.Tensor Bool s → TorchLean.Tensor α s × TorchLean.Tensor α s

Conservative interval bounds for hard-masked softmax along the last tensor axis.

LayerNorm IBP (last axis)

Layer normalization (Ba et al.) computes, per vector, something like:

y = (x - mean(x)) / sqrt(var(x) + eps).

We implement a conservative enclosure by:

1. Bounding mean using sums of endpoints.
2. Bounding variance using a max-deviation upper bound.
3. Bounding the per-component ratio by checking endpoint combinations against a positive denominator interval.

This is intended as a simple checker-side transfer rule. It is conservative and is not an optimized relaxation.

References:

• Ba, Kiros, Hinton, "Layer Normalization", 2016: https://arxiv.org/abs/1607.06450
• Bound propagation context: Xu et al., 2020 (auto_LiRPA): https://arxiv.org/abs/2002.12920

def NN.MLTheory.CROWN.Graph.idealLayerNormVarianceUpper {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (lo hi : TorchLean.Tensor α [n]) (muLo muHi : α) : α

Ideal-arithmetic upper bound on the variance term used by analytic LayerNorm rules.

Given endpoint bounds for a vector and bounds on its mean, each coordinate is at most max |x_i - μ| away from the bounded mean interval. Squaring and summing those coordinate radii gives a conservative variance upper bound. The implementation uses ordinary scalar arithmetic and is called only from exact-arithmetic branches; executable endpoint propagation uses ibpLayerNormRange? instead.

def NN.MLTheory.CROWN.Graph.idealLayerNormMeanBounds {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (lo hi : TorchLean.Tensor α [n]) : α × α

Ideal-arithmetic mean bounds for a nonempty vector with bounded coordinates.

For n = 0, the mathematical mean is undefined; this total helper returns (0,0) so callers do not accidentally divide by zero while they reject or totalize the empty case.

def NN.MLTheory.CROWN.Graph.idealLayerNormCenteredBounds {α : Type} [TorchLean.Storage α] [Context α] {n : ℕ} (lo hi : TorchLean.Tensor α [n]) (muLo muHi : α) : TorchLean.Tensor α [n] × TorchLean.Tensor α [n]

Ideal-arithmetic bounds for x - μ when x and μ are bounded by intervals.

LayerNorm transfer rules repeatedly need this centered interval for the input, first derivative, and second derivative streams. Keeping it here avoids duplicating the same endpoint arithmetic in IBP and derivative propagation.

def NN.MLTheory.CROWN.Graph.idealLayerNormInvStdBounds {α : Type} [Context α] (varHi : α) : α × α

Ideal-arithmetic reciprocal-denominator bounds from an upper variance bound.

def NN.MLTheory.CROWN.Graph.idealLayerNormLastTensor {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} : TorchLean.Tensor α s → TorchLean.Tensor α s → TorchLean.Tensor α s × TorchLean.Tensor α s

Analytic real-arithmetic LayerNorm bounds on the last axis, lifted over leading dimensions.

def NN.MLTheory.CROWN.Graph.ibpLayerNormRange? {α : Type} [TorchLean.Storage α] [Context α] [NonlinearBoundOps α] (s : Spec.Shape) (dim : ℕ) : Option (FlatBox α)

Uniform finite enclosure for last-axis layer normalization.

For a row of length n, exact LayerNorm without affine scale or bias satisfies |yᵢ| ≤ sqrt n; a singleton row is identically zero. Backends provide the outward-rounded bound through NonlinearBoundOps.layerNormAbsBound. Returning none is preferable to evaluating the normalization with unqualified host division and square root.

def NN.MLTheory.CROWN.Graph.directedLayerNormRow? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] {n : ℕ} (lo hi gamma beta : TorchLean.Tensor α [n]) (epsilon : α) : Option (TorchLean.Tensor α [n] × TorchLean.Tensor α [n])

Directed bounds for one LayerNorm row with explicit affine parameters.

The order follows Spec.layerNorm: center the input, center again inside reduceVar, square, average, clamp variance to zero, add epsilon, take a square root, and divide the first centered values directly. Each coordinate is then multiplied by its gamma and shifted by its beta; negative gamma reverses the interval endpoints.

Epsilon must be finite and positive, and the row and affine parameters must be finite. Division and square root use the selected nonlinear backend. Invalid or non-finite intermediate intervals return none. An end-to-end soundness theorem for this sequence and a proof of agreement with native arithmetic remain open obligations.

def NN.MLTheory.CROWN.Graph.directedLayerNormLastTensor? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] {s : Spec.Shape} : TorchLean.Tensor α s → TorchLean.Tensor α s → Option (TorchLean.Tensor α s × TorchLean.Tensor α s)

Input-dependent last-axis LayerNorm enclosure with unit scale, zero bias, and the default epsilon.

Each row uses directedLayerNormRow?, including the second centering and direct division in the specification. Leading dimensions select independent rows.

def NN.MLTheory.CROWN.Graph.ibpLayerNormBox? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (s : Spec.Shape) (input : FlatBox α) : Option (FlatBox α)

Use the backend's uniform LayerNorm range when available; otherwise propagate the supplied input box through the directed normalization sequence.

def NN.MLTheory.CROWN.Graph.ibpLayerNormPayloadBox? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (s : Spec.Shape) (axis : ℕ) (parameters : IR.LayerNormParams α) (input : FlatBox α) : Option (FlatBox α)

Enclose a last-axis LayerNorm payload using its full epsilon, gamma, and beta.

The matrix view and affine suffix are checked by the same helpers used in IR evaluation. Bounds are propagated separately for each row, then flattened back into the graph's storage order. Every payload, including one with default parameter values, uses the directed normalization sequence with its stored affine parameters and epsilon.

def NN.MLTheory.CROWN.Graph.getDimScalarFn {α : Type} [TorchLean.Storage α] {n : ℕ} (t : TorchLean.Tensor α [n]) : Fin n → TorchLean.Tensor α Spec.Shape.scalar

For tensors known to have shape .dim n .scalar, extract the underlying function.

def NN.MLTheory.CROWN.Graph.castBoxDim {α : Type} [TorchLean.Storage α] {n n' : ℕ} (h : n = n') (B : Box α (Spec.Shape.dim n Spec.Shape.scalar)) : Box α (Spec.Shape.dim n' Spec.Shape.scalar)

Cast a 1D Box along an equality of dimensions.

def NN.MLTheory.CROWN.Graph.castRelax {α : Type} {n n' : ℕ} (h : n = n') (r : TorchLean.Tensor (Runtime.Ops.ReLURelax α) [n]) : TorchLean.Tensor (Runtime.Ops.ReLURelax α) [n']

Cast a ReLU relaxation vector across a proven-equal hidden dimension.

def NN.MLTheory.CROWN.Graph.castAffineIn {α : Type} [TorchLean.Storage α] {n n' m : ℕ} (h : n = n') (a : AffineVec α n m) : AffineVec α n' m

Cast the input dimension of an affine map across a proven equality.

def NN.MLTheory.CROWN.Graph.castAffineOut {α : Type} [TorchLean.Storage α] {n m m' : ℕ} (h : m = m') (a : AffineVec α n m) : AffineVec α n m'

Cast the output dimension of an affine map across a proven equality.

@[reducible, inline]

abbrev NN.MLTheory.CROWN.Graph.castDimScalar {α : Type} [TorchLean.Storage α] {n n' : ℕ} (h : n = n') (t : TorchLean.Tensor α [n]) : TorchLean.Tensor α [n']

Cast a dim-scalar tensor across an equality of dimensions.

We keep this as an abbrev so it unfolds aggressively in simp-based soundness proofs.

@[simp]

theorem NN.MLTheory.CROWN.Graph.castDimScalar_self {α : Type} [TorchLean.Storage α] {n : ℕ} (h : n = n) (t : TorchLean.Tensor α [n]) : castDimScalar h t = t

Casting a flat vector tensor along an equality from a dimension to itself changes no data.

def NN.MLTheory.CROWN.Graph.ibpLinearParams {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (p : LinParams α) (Xin : FlatBox α) : Option (FlatBox α)

IBP propagation through explicit linear parameters.

def NN.MLTheory.CROWN.Graph.ibpLinear {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (id : ℕ) (ps : ParamStore α) (Xin : FlatBox α) : Option (FlatBox α)

IBP propagation for a .linear node using ParamStore.linearWB.

def NN.MLTheory.CROWN.Graph.ibpMatmul {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] (id : ℕ) (ps : ParamStore α) (Xin : FlatBox α) : Option (FlatBox α)

IBP propagation for a .matmul node (bias-free) using ParamStore.matmulW.

def NN.MLTheory.CROWN.Graph.ibpConvNode {α : Type} [TorchLean.Storage α] [Context α] (configuration : IR.ConvConfig) (parentShape outShape : Spec.Shape) (id : ℕ) (ps : ParamStore α) (Xin : FlatBox α) : Option (FlatBox α)

IBP transfer for a supported convolution node whose parameters are stored in ParamStore.convCfg.

def NN.MLTheory.CROWN.Graph.ibpMonotoneSomeTensor? {α : Type} [TorchLean.Storage α] [Context α] (parentShape outShape : Spec.Shape) (op : Spec.SomeTensor α → Except String (Spec.SomeTensor α)) (input : FlatBox α) : Option (FlatBox α)

Apply a monotone SomeTensor operation independently to both interval endpoints.