Comment: = high, and low is never read in the program.
In language based NIF the attacker is outside the system and
can observe all low variables at the end.
In model based NIF the attacker is part of the system and
can only perform (defined) actions. low := high is secure
if there is no action that observes low.
consider prog: followed by v := v for all v in vars(prog)
as actions. Then observe = vars.