Skip to content

Latest commit

 

History

History
93 lines (57 loc) · 4.96 KB

proxies-proof.md

File metadata and controls

93 lines (57 loc) · 4.96 KB

Proof of the main statement about Integrity checks on Proxies

Recall that IntegrityCheck_Method(arguments, result, target) denotes the abstract operation defining the integrity check associated to [[Method]].

Given the following condition:

I. IntegrityCheck_Method_(arguments, result, target) shall return true if all observations that would be made on the Proxy by returning result, may be made on target by invoking fundamental observation methods on it.

we want that to prove that the following condition is satisfied:

II. If the target of a Proxy is a nonquantum object that observes the Invariants of internal methods, then the Proxy shall observe those invariants.

when the IntegrityCheck_Method(arguments, result, target) abstract operations returns false unless the two following conditions are enforced:

A. For any observation “character: value” that would be made on the Proxy by returning result, if a lock “@character: valueT” may be put on target (by invoking fundemental observation methods on it), then valueT must be the same as value.

B. Assuming that all the locks that may be put on target (by invoking fundemental observation methods on it) are also put on the Proxy, for any lock “@character: value” that would be put on the Proxy by returning result, if the observation “character: valueT” may be performed on target, then valueT must be the same as value.

Necessity

Let us show that, if the integrity check is passed, Condition A and B must hold.

Consider the following programm:

1. Construct an ordinary object target for which the observation of characters using its fundemental observation methods would produce some predefined result.

2. Construct a Proxy P with target as its target object, and whose trap will return some predefined arbitrary result without modifying target, as follows:

let result
let P = Proxy(target, {
    getPrototypeOf(t) { return result }
  , setPrototypeOf(t, v) { return result }
  /* etc. */
})
/* 
result = <something>
Reflect.getPrototypeOf(result); // will return <something>
*/

3. For all locks that could be observed on target by calling its fundemental observation methods, observe the same locks on P:

result = Reflect.isExtensible(target)
Reflect.isExtensible(P)

result = Reflect.getPrototypeOf(target)
Reflect.getPrototypeOf(P)

result = Reflect.ownKeys(target)
Reflect.ownkeys(P)

foreach (let key of result) {
    result = Reflect.getOwnPropertyDescriptor(target, key)
    Reflect.getOwnPropertyDescriptor(P, key)
}

Because of Condition I, integrity checks are past and all these observations are successful.

4. Call the corresponding internal method of that would trigger the “character: value” observation if successful.

result = <desired returned value>
Reflect[Method](P, ...args)

As part of the algorithm, IntegrityCheck_Method is run, that would trigger “character: valueT” observation on target. By assumption it is passed.

5. Repeat step 3.

Now we can show:

Condition A. Let us suppose that “@character: valueT” is put on target during the integrity check of step 4. Then, the same lock is put on P during step 3. Because “character: value” is observed on P during step 4, that imposes that value shall be equal valueT.

Condition B. Let us suppose that all locks on which “@character: value” depends are put on target during the integrity check of step 4. Then the same locks are put on P during step 3, and the completion of step 4 will put the “@character: value” lock on P. Finally, step 5 will trigger the observation “character: valueT” on P, imposing that valueT shall be the same as value.

Sufficiency

Let us assume that some “@character: value” lock has been put on a proxy P, and let us show that we cannot observe “character: value2” on P unless value2 is the same as value. First, we show that

The same “@character: value” lock is put on target at the latest during the call of the internal method that put “@character: value” lock on P.

By using recursion, we can assume that this is true for all locks on which “@character: value” depends; so it suffices to show that “character: value” is observed on the target. If the internal method is not trapped, this is evident. If it is trapped, the enforcement of Condition B during the integrity check will trigger such an observation.

Now, let us attempt observe “character: value2” on P by calling some internal method on P. If it is not trapped, because of the existing “@character: value” lock on target, we observe “character: value” again. If it is trapped, the enforcement of Condition A will guarantee that value2 shall be the same as value.