Look-Ahead-Freedom as Temporal Non-Interference: The halting reduction does not gate the future value
Section 7 claims the constructed pipeline leaks exactly when a simulated machine halts. Under the evaluation rules the paper gives in §6.2, the future value reaches the output in the never-halting case too, so the reduction does not establish what it is used for.
§7 reduces the halting problem to look-ahead-freedom: a pipeline is said to leak precisely when the simulated machine halts. Together with a decidability result on the value-independent fragment, this is presented as an exact frontier between decidable and undecidable cases.
The rules in §6.2 do three things. stamp changes only a label. val
discards that label. decide emits the result without checking availability. Nothing in
that sequence blocks a future value from reaching the output.
Take the nonconstant function to be the identity and compare future inputs 0 and 1. The two outputs are 0 and 1 whether or not the machine halts, so output dependence on the future input is present in both branches:
Changing the advertised timestamp from present to future does not change that dependence. As written the reduction also mixes raw-value and timestamped-value sorts; repairing those wrappers does not supply the missing gate.
The claimed frontier is a separate problem
Let a public natural number n carry timestamp 0, a secret bit b timestamp 1, and let the decision happen at time 0. An allowed total pure function can return b when machine M halts within n steps and 0 otherwise. Every timestamp here is a constant. Non-interference over all inputs holds exactly when M never halts. Value-independent timestamps therefore do not make the semantic property decidable once these value computations are allowed.
A conservative type checker can still have decidable acceptance and a useful soundness guarantee. That is a different statement from deciding semantic non-interference for every program, and the paper already acknowledges conservative rejection in §4.5. The type system and the framing of look-ahead-freedom as an information-flow property are unaffected.
The halting reduction in §7 fails under the evaluation rules in §6.2: future values reach the decision even when the machine never halts. Decidable type-checking is also not a decision procedure for semantic non-interference. The claimed exact decidability frontier is not established.