I don't believe ZKPs are capable of proving that a program has been run correctly, where correctly would mean that the verifier can confirm that $f(x)=y$ is true knowing only $x$ and $y$.
Logically we can imagine that a malicious actor could produce two programs $f(x)=y$ and $f'(x)=y'$ where $f'$ is a corrupted version of $f$. Without knowing any details about $f$ or $f'$ it is impossible to distinguish whether $y$ or $y'$ is the "correct" result of the correctly run program $f$.
It may be possible to construct a more efficient form of $f$ that maps the same inputs to the same outputs but is faster to run. However, this is a problem more specific to compilers - you can never guarantee that 'circuits' (programs) of a shorter length will behave the same.
As for the second part of your question this would depend a lot on the specific ZKP algorithm used. In most algorithms the most computationally expensive part is converting everything that needs to be proven into a format that is provable (i.e. turning $x=25$ into some polynomial equation of a large degree).
Therefore the less you need to convert, the more efficient the proof will be. This would mean that you could potentially produce a more efficient operation by hiding less of the information (though as above, I don't believe this would help in the example of Miden).