Evaluation of λCON. The evaluation judgment is similar to a standard big-step evaluation judgment except that its input ranges over intermediate terms and its output is a behavior. The judgment states that the evaluation of term t with initial store σ, constraint list ς, environment ρ, and context κ results in a final heap σr, constraint list ςr, and behavior b: κ, ρ € σ, ς, t ⇓ σr, ςr, b Figure 5.8 and 5.9 defines the standard evaluation rules for expressions e in λCON . The evaluation rules for expressions are mostly standard. Each rule for a composite expression evaluates exactly one sub-expression and then recursively invokes the evaluation judgment to continue. Once all sub-expressions are evaluated, the respective rule performs the desired operation. The corresponding straightforward error propagation rules are disjoint to the remaining rules because they fire only if an intermediate-term contains an error. Figure 5.10 defines the evaluation rules for intermediate terms with nested terms, and the rule set in Figure 5.11 defines error handling, which always propagates an error to the top level. | ∫ The rules Const, Var, and Undef are standard. Rule Op applies a primitive operation to its argument values. The extended set of objects requires to revisit primitive operations on values. Function v σ (Figure 5.12) first erases all contract monitors and sandbox wrappers from its argument values before it proceeds with the usual operation. This unwrapping makes proxies transparent with respect to primitive operations on locations. Rule Abs allocates a new function object consisting of a closure with the current environ- ment and rule New allocates a new native object based on the evaluated prototype. Function application, property lookup, and property assignment distinguish two cases: either the operation applies directly to a target object (non-proxy object) or it applies to a proxy. If the given reference is a non-proxy object, then the usual rules apply: App for function application, Get for property lookup, and Put for property assignment. The evaluation rules for the non-standard cases are given in Section 5.4.5 and Section 5.4.6. The rules Get, Get-Proto, and Get-Undef implement JavaScript’s lookup operation through prototype chains. Each object has an internal prototype property which links to another object or to a constant value, signaling the end of the chain. If a property is not contained in the object’s dictionary rule Get-Proto forwards the lookup to the prototy...
