Round-six lemma `code_runs`