I don't think it is same as PVI, because i) there are a lot of possible non-determinisms still allowed and thus to be exploited, and ii) the specification will

I don't think it is same as PVI, because i) there are a lot of possible non-determinisms still allowed and thus to be exploited, and ii) the specification will have to require only the observational equivalence anyway because every optimization will be invalid otherwise. It should be definitely possible to define a very precise machine without actually mandating PVI.