If you have a getter like: function() { return this._f; } Then inside the getter stub we know the structure of 'this' - because we just checked it - so we can inspect what _f is and if it's a simple field then we can prove that the outcome of executing this function is exactly equivalent to just loading the field from 'this'. The only hard parts are: - Proving that the getter is what you thought it was. The structure doesn't tell you that so this will be an extra check. - Inspecting the getter to recognize this pattern. This should hopefully be relatively easy.