Executable proofs, input-size hiding secure computation and a new ideal world