How to build a TM which decides $L_k := \{(\langle M \rangle ,x)\in HP : |(\langle M \rangle ,x)| \le k \}$
You cannot construct an explicit algorithm/TM which will decide the language $L_k$. Regarding your attempt at the proof: you are right that there is no guarantee that the configuration will repeat because these machines are not given to be space bounded. 

The TM $M_k$ to decide $L_k$ will have all the tuples (which are finite in number) which are accepted hard coded in it. The TM will basically perform a search in a look up table: if that tuple is found then accept it, else reject. 
We don't care how these tuples are actually obtained.

We can perhaps even prove that a general method to construct such TM $M_k$ for each $L_k$ cannot exists: Suppse there exists, then for a given input $&lt;M,x&gt;$, find the length of input, let it be $k$ and construct the TM $M_k$. Simulate $M_k$ over $&lt;M,x&gt;$. This will act as a decider for Halting Problem: which we know is undecidable. Hence, the assumption that we can have such a method is false.