The evaluation with its verdict read, and the two exits #
The forward run of a clocked program at the file the register channel hands it
assumes the sentence and runs into the accepting phase. A backward reading
cannot assume it – the verdict is what it is trying to determine – so this file
carries the evaluation in the other form: the run exists whatever the stage says,
and the accepting bit it leaves is the sentence's value
(nexProgHanded_reachesIn_eval_verdict).
The two exits of the walks home come with it (exitG_at_marker): they are facts
about where the marker is, and nothing about what the machine has written, so
both directions of the correctness supply them the same way.