Is there a Sokoban level where it is always possible to move at least one box? Sokoban is a game played on a grid where each square is a floor or wall, some floor squares contain boxes, and some floor squares are marked. The goal is for the player (who can only stand on floor squares) to push the boxes onto the marked squares. A box is pushed when, for example, the player is standing in the square directly to the right of a box moves left, and the square immediately to the left of the box is an unoccupied floor square. (Boxes cannot be pushed into walls, and cannot be pushed onto other boxes, and only one box can be pushed at a time.)
Is it possible to create a finite Sokoban level so that regardless of what moves the player makes, there will always be at least one box that can be pushed? For this we can completely ignore the marked goal squares.
For example, consider this attempt

Here red is the player, yellow is a box, dark blue is target, and light blue is floor, and white are walls. So, here obviously we need to push box in upper right corner. But, if we do that (or if we push it in any corner) we will not be able to move it anymore.
Here is another unsuccessful attempt to make such a level:

If you move top left box to right, you can then push bottom left box down in corner, so this is still not the a level I am searching for.
I tried to prove it for a long time, but it turned out to be harder than I thought.
 A: Nice question. I think I have a proof that there is no such level if we have exactly one box:
I start with some definitions:
Choose a coordinate system parallel to the grid, put the origin in the center of one grid cell, then each grid square can be named/identified with the (integer) coordinates of its center. 
I define a floor plan F as a set if grid squares, they are the grid squares that contain floor tiles. The connection graph $C_F$ of F is the simple graph with nodes F and an edge between two nodes if the corresponding squares have an edge in common. In other words, $C_F$ describes how the player can move around F if it contains no boxes.
A game state is a triple $S=(F,p,B)$ with $p \in F, B \subset F$ and $p \notin B$, where $p$ is the grid square containing the player and $B$ the set of squares where the boxes are. I'll use the terms player position for $p$ and box position for any $b \in B$.
A legal move (as defined in the question) is therefore a transformation of one position $S=(F,p,B)$ into $S'=(F,p',B')$, which is called a successor of $S$ ($S'$ succeeds $S$). If $B=B'$, then no boxes were moved in that move. 
Let's define as $\sigma(S)$ the set of all game states that can be reached from $S$ by a finite (possibly empty) series of moves. If $F$ is finite, then obviously $\sigma(S)$ is also finite.
The original question then becomes the following:
Is there a game state $S_0=(F,p_0,B_0)$ with finite $F$ and nonempty $B_0$ such that for each $S \in \sigma(S_0)$ there exist a $T \in \sigma(S)$ with $B_T \neq B_S$.
Assume there is such game state and that $\left|{B_0}\right|=1$. Calculate $\bigcup_{S \in \sigma(S_0)}B_S$, that is the set of all the possible positions that our box can reach when we start at $S_0$. Choose one such game state with minimal $\left|\bigcup_{S \in \sigma(S_0)}B_S\right|$. In other words, choose a counterexample $S_0$ where the set of reachable box positions is as small as possible.
Find the square $(x_{tr},y_{tr})$ in $\bigcup_{S \in \sigma(S_0)}B_S$ with the highest $y$ value; if there are several, take the one with the highest $x$ among them. $(x_{tr},y_{tr})$ is the most topright position the box can have. Let $S_1 \in \sigma(S_0)$ be a game state with $B_1=\{(x_{tr},y_{tr})\}$. Since the box must be pushable away from $(x_{tr},y_{tr})$ after state $S_1$, there is a game state $S_2 \in \sigma(S_1) \subseteq \sigma(S_0)$ where $B_2 \neq \{(x_{tr},y_{tr})\}$. 
If there was $(x_{tr},y_{tr}) \notin \bigcup_{S \in \sigma(S_2)}B_S$, then we would have found a starting game state ($S_2$) with an even smaller set of reachable box positions than $S_0$: Since $\sigma(S_2) \subseteq \sigma(S_0)$ we would have $\bigcup_{S \in \sigma(S_2)}B_S \subseteq \bigcup_{S \in \sigma(S_0)}B_S$ and because $(x_{tr},y_{tr})$ is contained in the right side but not on the left the inequality would be sharp, in contradiction to our choice of $S_0$. 
This means it holds $(x_{tr},y_{tr}) \in \bigcup_{S \in \sigma(S_2)}B_S$ and therefore we have a game state $S_3\in \sigma(S_2)$ where we have just pushed the box into $(x_{tr},y_{tr})$ (that means $B_3=\{(x_{tr},y_{tr})\}$. By the way a box push works, the player ends up in the position the box was before the push. The box could not have been coming from the positions $(x_{tr}+1,y_{tr})$ or $(x_{tr},y_{tr}+1)$, as that would have contradicted the definition of $(x_{tr},y_{tr})$ as the topright reachable box position. It must therefore have come from position $(x_{tr}-1,y_{tr})$ or $(x_{tr},y_{tr}-1)$. Let's assume w.l.o.g. that it is the latter and thus the player position in $S_3$ is $(x_{tr},y_{tr}-1)$.
In the following, the game state $S_3$ is graphically represented around the square $(x_{tr},y_{tr})$. The letter b (marking the box) is placed in the center, the letter p (marking the player) below. All the other squares are unknown, marked with '?'.
$$ S_3 (\text{centered at }(x_{tr},y_{tr})) =
\begin{array}{ccc} 
 ? & ? & ? \\ 
 ? & b & ? \\ 
 ? & p & ? \\ 
\end{array}$$
If $(x_{tr},y_{tr}+1)$ was a floor tile, we could immediately push the box onto it from state $S_3$, which would contradict the choice of $(x_{tr},y_{tr})$. It must therefore be a wall tile, marked with 'x':
$$ S_3 (\text{centered at }(x_{tr},y_{tr})) =
\begin{array}{ccc} 
 ? & x & ? \\ 
 ? & b & ? \\ 
 ? & p & ? \\ 
\end{array}$$
Since the box must be pushable away from $(x_{tr},y_{tr})$ after $S_3$, and since this cannot be done vertically (it would have to be pushed from or onto the wall tile $(x_{tr},y_{tr}+1)$) it must be done horizontally. Therefore both the tile to the left and to the right of it must be floor tiles (marked with '.':
$$ S_3 (\text{centered at }(x_{tr},y_{tr})) =
\begin{array}{ccc} 
 ? & x & ? \\ 
 . & b & . \\ 
 ? & p & ? \\ 
\end{array}$$
If the player could reach square $(x_{tr}-1,y_{tr})$ from $(x_{tr},y_{tr}-1)$ without moving the box at $(x_{tr},y_{tr})$, the box could be pushed onto $(x_{tr}+1,y_{tr})$, which would contradict the choice of $(x_{tr},y_{tr})$ as the topright position the box can ever get to from $S_0$. 
That means in our connection graph $C_F$, any walk between $(x_{tr}-1,y_{tr})$ and $(x_{tr},y_{tr}-1)$ must go through $(x_{tr},y_{tr})$. This will be the statement later to be contradicted.
So we see that the only way to push the box away from square $(x_{tr},y_{tr})$ is if the player is at $(x_{tr}+1,y_{tr})$ and pushes the box onto $(x_{tr}+1,y_{tr})$:
\begin{array}{ccccccc} 
 ? & x & ? &   & ? & x & ? \\ 
 . & b & p & \rightarrow  & b & p & .\\ 
 ? & . & ? &   & ? & . & ? \\ 
\end{array}
Let's call the game state on the right $S_4$. As we saw earlier, it must still be possible to get the box back onto $(x_{tr},y_{tr})$ from state $S_4$. So we have a series of states $T_1,\ldots,T_n$ where $T_1$ succeeds $S_4$, $T_{i+1}$ succeeds $T_i$ for $i=1,\ldots,n-1$ and the box position in $T_n$ is $(x_{tr},y_{tr})$. We can also assume that the box position in $T_i$ is never $(x_{tr},y_{tr})$ for $i < n$ (otherwise, we just take the smallest such $i$ as our new $n$). Let's also define $T_0:=S_4$.
Let's try to find the box position in $T_{n-1}$, the state from which we push the box onto $(x_{tr},y_{tr})$ in $T_n$. Since boxes (if they move at all during a move) just move from one floor tile square to an adjacent floor tile square, the box position in $T_{n-1}$ must be an adjacent tile to $(x_{tr},y_{tr})$. 
Looking at the last picture of $S_3$ above, we see that for each of the 4 squares adjacent  to $(x_{tr},y_{tr})$ we know if it is a floor or a wall tile: $(x_{tr},y_{tr}+1)$ is a wall tile, the other three are floor tiles. The box position in $T_{n-1}$ can therefore not be $(x_{tr},y_{tr}+1)$ (wall tile), nor can it be $(x_{tr}+1,y_{tr})$ (choice of $(x_{tr},y_{tr})$ as topright reachable box position).
It can also not be $(x_{tr}-1,y_{tr})$, because that would mean that the player position in $T_n$ would be $(x_{tr}-1,y_{tr})$ and we would have
$$T_n (\text{centered at }(x_{tr},y_{tr})) =
\begin{array}{ccc} 
 ? & x & ? \\ 
 p & b & . \\ 
 ? & . & ? \\ 
\end{array}$$
But this would mean the box could immediately be pushed onto $(x_{tr}+1,y_{tr})$, which contradicts the choice of $(x_{tr},y_{tr})$. This means the only possible box position in $T_{n-1}$ is $(x_{tr},y_{tr}-1)$.
In some moves from $T_i$ to $T_{i+1}$ the box will not move ($B_{T_i} = B_{T_{i+1}}$), in others it will move, and then from a tile floor square to an adjacent tile floor square. That means the sequence $B_{T_i}$ from $i=0,\ldots,n-1$ is a sequence of tile floor squares where consecutive entries are either the same or adjacent. 
Since $T_i=S_4$ we have $B_{T_i} = \{(x_{tr}-1,y_{tr})\}$. In addition, we just proved $B_{T_{n-1}} = \{(x_{tr},y_{tr}-1)\}$. That means the sequence $B_{T_i}$ from $i=0,\ldots,n-1$ is a sequence of adjacent floor tile squares starting from $(x_{tr}-1,y_{tr})$ and ending in $(x_{tr},y_{tr}-1)$. None of those tiles is $(x_{tr},y_{tr})$. 
In other words we found a walk in $C_F$ that connects $(x_{tr}-1,y_{tr})$ with $(x_{tr},y_{tr}-1)$ and doesn't go through $(x_{tr},y_{tr})$. This is in  contradiction to the bolded part mentioned earlier. $\blacksquare$
The problem I have with extending this to game states with several boxes is that we need to technically write down what it means that from game state $S_3$ (where the player is at $(x_{tr},y_{tr}-1)$) we cannot get the player to reach square $(x_{tr}-1,y_{tr})$ without moving the box at $(x_{tr},y_{tr})$. If there are more boxes in the game state, then this is not easily describable with $C_F$, because there might be a walk from  $(x_{tr},y_{tr}-1)$ to $(x_{tr}-1,y_{tr})$ not going through $(x_{tr},y_{tr})$, but it might still not be possible for the player to get there because other boxes are blocking the way.
