Documentation

LeanMlir.ParamLayouts

The verified trainers' packed-parameter layouts #

One namespace per net family (MlpLayout, CnnLayout, CifarLayout, ResNet34Layout, MobileNetV2Layout, EfficientNetLayout, ConvNeXtLayout, ViTLayout): each net's (dims, initKind) list in the train step's argument order, its sizes, and the packed shape descriptors (packShapes, packXShape) the runtime passes to the FFI. Pure data — importing only LEBytes — so the spec side (VerifiedNetsCore's #guard spec.toSpecs == XLayout.specs) can read the tables without importing the runtime; IreeRuntime re-exports them.

def MlpLayout.nW0 :

Equations

MlpLayout.nW0 = 784 * 512

Instances For

def MlpLayout.nb0 :

Equations

MlpLayout.nb0 = 512

Instances For

def MlpLayout.nW1 :

Equations

MlpLayout.nW1 = 512 * 512

Instances For

def MlpLayout.nb1 :

Equations

MlpLayout.nb1 = 512

Instances For

def MlpLayout.nW2 :

Equations

MlpLayout.nW2 = 512 * 10

Instances For

def MlpLayout.nb2 :

Equations

MlpLayout.nb2 = 10

Instances For

def MlpLayout.nParams :

Equations

MlpLayout.nParams = MlpLayout.nW0 + MlpLayout.nb0 + MlpLayout.nW1 + MlpLayout.nb1 + MlpLayout.nW2 + MlpLayout.nb2

Instances For

def MlpLayout.lossIdx :

Equations

MlpLayout.lossIdx = MlpLayout.nParams

Instances For

def packShapes (shapes : Array (Array Nat)) :

Pack param shape descriptors: [nParams, rank0, d0..., rank1, d1..., ...] as int32 LE.

Equations

One or more equations did not get rendered due to their size.

Instances For

def packXShape (dims : Array Nat) :

Pack a single shape: [rank, d0, d1, ...] as int32 LE (for x input).

Equations

One or more equations did not get rendered due to their size.

Instances For

def CnnLayout.paramShapes :

Array (Array Nat)

Equations

CnnLayout.paramShapes = #[#[32, 1, 3, 3], #[32], #[32, 32, 3, 3], #[32], #[6272, 512], #[512], #[512, 512], #[512], #[512, 10], #[10]]

Instances For

def CnnLayout.nParams :

Equations

CnnLayout.nParams = 32 * 1 * 3 * 3 + 32 + 32 * 32 * 3 * 3 + 32 + 6272 * 512 + 512 + 512 * 512 + 512 + 512 * 10 + 10

Instances For

def CnnLayout.lossIdx :

Equations

CnnLayout.lossIdx = CnnLayout.nParams

Instances For

def CnnLayout.shapesBA :

Equations

CnnLayout.shapesBA = packShapes CnnLayout.paramShapes

Instances For

def CnnLayout.xShape (batch : Nat) :

Equations

CnnLayout.xShape batch = packXShape #[batch, 784]

Instances For

def CifarLayout.paramShapes :

Array (Array Nat)

Equations

CifarLayout.paramShapes = #[#[32, 3, 3, 3], #[32], #[32, 32, 3, 3], #[32], #[64, 32, 3, 3], #[64], #[64, 64, 3, 3], #[64], #[4096, 512], #[512], #[512, 512], #[512], #[512, 10], #[10]]

Instances For

def CifarLayout.nParams :

Equations

CifarLayout.nParams = 32 * 3 * 3 * 3 + 32 + 32 * 32 * 3 * 3 + 32 + 64 * 32 * 3 * 3 + 64 + 64 * 64 * 3 * 3 + 64 + 4096 * 512 + 512 + 512 * 512 + 512 + 512 * 10 + 10

Instances For

def CifarLayout.lossIdx :

Equations

CifarLayout.lossIdx = CifarLayout.nParams

Instances For

def CifarLayout.shapesBA :

Equations

CifarLayout.shapesBA = packShapes CifarLayout.paramShapes

Instances For

def CifarLayout.xShape (batch : Nat) :

Equations

CifarLayout.xShape batch = packXShape #[batch, 3072]

Instances For

def ResNet34Layout.specs :

Array (Array Nat × Nat)

(dims, initKind) for every param, in func-arg order.

Equations

One or more equations did not get rendered due to their size.

Instances For

def ResNet34Layout.paramShapes :

Array (Array Nat)

Equations

ResNet34Layout.paramShapes = Array.map (fun (x : Array Nat × Nat) => x.fst) ResNet34Layout.specs

Instances For

def ResNet34Layout.nParams :

Equations

ResNet34Layout.nParams = Array.foldl (fun (x1 x2 : Nat) => x1 + x2) 0 (Array.map (fun (s : Array Nat × Nat) => Array.foldl (fun (x1 x2 : Nat) => x1 * x2) 1 s.fst) ResNet34Layout.specs)

Instances For

def ResNet34Layout.shapesBA :

Equations

ResNet34Layout.shapesBA = packShapes ResNet34Layout.paramShapes

Instances For

def ResNet34Layout.xShape (batch : Nat) :

Equations

ResNet34Layout.xShape batch = packXShape #[batch, 3 * 224 * 224]

Instances For

def MobileNetV2Layout.specs :

Array (Array Nat × Nat)

(dims, initKind) for every param, in func-arg order.

Equations

One or more equations did not get rendered due to their size.

Instances For

def MobileNetV2Layout.paramShapes :

Array (Array Nat)

Equations

MobileNetV2Layout.paramShapes = Array.map (fun (x : Array Nat × Nat) => x.fst) MobileNetV2Layout.specs

Instances For

def MobileNetV2Layout.nParams :

Equations

One or more equations did not get rendered due to their size.

Instances For

def MobileNetV2Layout.shapesBA :

Equations

MobileNetV2Layout.shapesBA = packShapes MobileNetV2Layout.paramShapes

Instances For

def MobileNetV2Layout.xShape (batch : Nat) :

Equations

MobileNetV2Layout.xShape batch = packXShape #[batch, 3 * 224 * 224]

Instances For

def EfficientNetLayout.specs :

Array (Array Nat × Nat)

(dims, initKind) for every param, in func-arg order — generated from the B0 stage spec exactly as tests/TestEfficientNet*.lean blocks (stem out 32, prev threading).

Equations

One or more equations did not get rendered due to their size.

Instances For

def EfficientNetLayout.paramShapes :

Array (Array Nat)

Equations

EfficientNetLayout.paramShapes = Array.map (fun (x : Array Nat × Nat) => x.fst) EfficientNetLayout.specs

Instances For

def EfficientNetLayout.nParams :

Equations

One or more equations did not get rendered due to their size.

Instances For

def EfficientNetLayout.shapesBA :

Equations

EfficientNetLayout.shapesBA = packShapes EfficientNetLayout.paramShapes

Instances For

def EfficientNetLayout.xShape (batch : Nat) :

Equations

EfficientNetLayout.xShape batch = packXShape #[batch, 3 * 224 * 224]

Instances For

def ConvNeXtLayout.specs :

Array (Array Nat × Nat)

(dims, initKind) for every param, in func-arg order.

⚠ §2m moved three things at once: every LN affine went rank-0 #[] → per-channel #[c], the stem LN appeared, and the head LN went away. The first two were right; the third was not, and the note that used to sit here — "the last two nearly cancel … so a matching parameter count is a decomposition test, not an architecture check" — was the correct warning drawn at the wrong conclusion. The residue is not noise, it IS the missing layer: 28,587,592 against timm.create_model('convnext_tiny')'s 28,589,128 is short by exactly 2×768 = 1,536.

⭐ The head LN is back (2026-08-30, §7.1), so the head is GAP → LN(768) → dense as in both the paper (self.norm(x.mean([-2,-1])), nn.LayerNorm(dims[-1], eps=1e-6)) and timm (NormMlpClassifierHead). 182 param tensors; the floats are 27,827,818 at K = 10, i.e. 28,589,128 at K = 1000 — timm's count exactly.

Equations

One or more equations did not get rendered due to their size.

Instances For

def ConvNeXtLayout.paramShapes :

Array (Array Nat)

Equations

ConvNeXtLayout.paramShapes = Array.map (fun (x : Array Nat × Nat) => x.fst) ConvNeXtLayout.specs

Instances For

def ConvNeXtLayout.nParams :

Equations

ConvNeXtLayout.nParams = Array.foldl (fun (x1 x2 : Nat) => x1 + x2) 0 (Array.map (fun (s : Array Nat × Nat) => Array.foldl (fun (x1 x2 : Nat) => x1 * x2) 1 s.fst) ConvNeXtLayout.specs)

Instances For

def ConvNeXtLayout.shapesBA :

Equations

ConvNeXtLayout.shapesBA = packShapes ConvNeXtLayout.paramShapes

Instances For

def ConvNeXtLayout.xShape (batch : Nat) :

Equations

ConvNeXtLayout.xShape batch = packXShape #[batch, 3 * 224 * 224]

Instances For

def ViTLayout.specs :

Array (Array Nat × Nat)

(dims, initKind) for every param, in @vit_train_step func-arg order.

Equations

One or more equations did not get rendered due to their size.

Instances For

def ViTLayout.paramShapes :

Array (Array Nat)

Equations

ViTLayout.paramShapes = Array.map (fun (x : Array Nat × Nat) => x.fst) ViTLayout.specs

Instances For

def ViTLayout.nParams :

Equations

ViTLayout.nParams = Array.foldl (fun (x1 x2 : Nat) => x1 + x2) 0 (Array.map (fun (s : Array Nat × Nat) => Array.foldl (fun (x1 x2 : Nat) => x1 * x2) 1 s.fst) ViTLayout.specs)

Instances For

def ViTLayout.shapesBA :

Equations

ViTLayout.shapesBA = packShapes ViTLayout.paramShapes

Instances For

def ViTLayout.xShape (batch : Nat) :

Equations

ViTLayout.xShape batch = packXShape #[batch, 3 * 224 * 224]

Instances For

def MlpLayout.paramShapes :

Array (Array Nat)

Equations

MlpLayout.paramShapes = #[#[784, 512], #[512], #[512, 512], #[512], #[512, 10], #[10]]

Instances For

def MlpLayout.shapesBA :

Equations

MlpLayout.shapesBA = packShapes MlpLayout.paramShapes

Instances For