Hard-Mask Payloads

Conversions between typed Boolean tensors and the row-major masks stored in NN.IR.OpKind. Keeping this bridge in one module gives graph builders, evaluators, and verifier passes the same validation rule for mask payloads.

def NN.IR.HardMask.ofTensor {s : Spec.Shape} (mask : Spec.Tensor Bool s) : HardMask

Flatten a typed Boolean mask into an IR payload.

def NN.IR.HardMask.validateAs (mask : HardMask) (expected : Spec.Shape) : Except String (PLift (mask.shape = expected))

Check a hard-mask payload and return the equality needed to recover its typed shape.

def NN.IR.HardMask.toTensor? (mask : HardMask) : Except String (Spec.Tensor Bool mask.shape)

Reconstruct a typed mask, rejecting a payload whose flat length disagrees with its shape.

def NN.IR.HardMask.toTensorAs? (mask : HardMask) (expected : Spec.Shape) : Except String (Spec.Tensor Bool expected)

Decode a hard-mask payload at an expected shape.

This is the common validation boundary for graph evaluation and executable lowering. It checks both the shape tag and the row-major payload length before transporting the decoded tensor to the requested type.

@[simp]

theorem NN.IR.HardMask.toTensor?_ofTensor {s : Spec.Shape} (mask : Spec.Tensor Bool s) : (ofTensor mask).toTensor? = Except.ok mask

Encoding and then decoding a typed mask preserves every Boolean entry.

@[simp]

theorem NN.IR.HardMask.toTensorAs?_ofTensor {s : Spec.Shape} (mask : Spec.Tensor Bool s) : (ofTensor mask).toTensorAs? s = Except.ok mask

Encoding a typed mask and decoding it at the same expected shape is a round trip.