I finally fixed the branch logic, and proved that it works with this simple counter that uses the conditional BGE (branch if greater than or equal) instruction.