Computationally Sound Typing for Non-interference: The Case of Deterministic Encryption