The following proposition is there in Pink's lecture notes on finite group schemes.
Let $k$ be an algebraically closed field of characteristic $p$. The category of finite length $W(k)$-modules $N$ with a $\sigma$-linear automorphism ($\sigma$ is the Witt vector frobenius) $F: N \to N$ is equivalent to the category of finite length $\mathbb Z_p$ modules (i.e., finite abelian $p$-groups). In particular, $\text{length} _{W(k)} N = \text{log}_p |N^F|$ where $N^F$ is the subset of $N$ fixed by $F$.
In the lecture notes there is a proof by using Lang's theorem. I think there is a more straightforward proof without using Lang theorem but just by following the technique of Fontaine's Galois descent proof in the case of Witt-vectors. Edit:For whatever its worth, here is that proof.
Given such a module $N$, we send it to $N^F$ and for a finite length $\mathbb Z_p$ module $N$ we send it to $W(k) \otimes_{\mathbb Z_p} N$ with an $F$ action given by $\sigma \otimes id$. We show that the map $W(k) \otimes_{\mathbb Z_p} N^F \to N$ () given by $x \otimes n \to xn$ is an isomorphism. We choose an (infinite) basis $x_i$ of $k$ over $\mathbb F_p$. Then the Teichmuller lifts $\underline{x_i}$ forms a basis of $W(k)$ over $\mathbb Z_p$. We show that the map defined in () is injective. Any element in the tensor product can be written as a finite sum $\sum_{i=1}^{m}{\underline{x_i} \otimes n_i}$. We assume that it is in the kernel of the map i.e., $\sum_{i=1}^{m}{\underline{x_i} n_i} = 0$. We apply $F, F^2,\ldots, F^m$ to this equation to get $\sum_{i=1}^{m} \underline{{x_i}^{p^j}} n_i = 0$ for each $j = 1, \ldots, m$. This is an expression in the $W(k)$ module $N$. We claim that the matrix $(\underline{{x_i}^{p^j}})$ is invertible in $W(k)$, from which it will follow that $n_i = 0$. It is enough to show that the determinant of $({{x_i}^{p^j}})$ is nonzero in $k$. This is a Moore determinant and from the fact that $x_i$-s are linearly independent over $\mathbb F_p$ it follows that the determinant is indeed nonzero {\cite[Lemma 1.3.3]{Goss}}. So we are done proving injectivity. For surjectivity, it would be enough to show that $\text{length}_{\mathbb{Z}_p} N^F = \text{length}_{W(k)} N$. First we note that if $N \ne 0$, then $N^F \ne 0$. This follows from induction on $\text{length}_{W(k)}N$ and the fact that a frobenius semi-linear map on an algbraically closed field has a fixed point. Now we proceed onto proving $\text{length}_{\mathbb{Z}_p} N^F = \text{length}_{W(k)} N$. we again use induction on $\text{length}_{W(k)}N$. If $\text{length}_{W(k)}N = 1$, we are done since $N^F \ne 0$. So we suppose $\text{length}_{W(k)}N > 1$. We pick $x \in N^F$ such that $x \ne 0$ and $px= 0$. So we get an exact sequence $0 \to k \to N \to N' \to 0$ of $W(k)$ modules with $\sigma $ semi-linear automorphism $F$. We apply $(.)^F$ to the exact sequence to get an exact sequence of $\mathbb Z_p$ modules : $0 \to \mathbb{F}_p \to N^F \to N'^F $. We show that the last map is surjective. Indeed, let $\overline{n} \in N'$ be fixed by $F$. Then $F(n) = n+ tx$ for some $t \in W(k)$. Since $k$ is algebraically closed, we can find an $u \in W(k)$ such that $t + \sigma(u) = u$. Then $F(n + ux) = F(n) + \sigma(u) x = n + (t+\sigma(u)) x = n + u x$. Therefore, we have produced an $F$ invariant lift of $\overline{n}$. Now the equality of length follows from induction and the fact that length is additive on short exact sequences.
Question: Does anyone have a reference to the theorem or any of the proofs?
