From eb79f07bf7d2f8e91c78562d57bb5ebae4da2c0d Mon Sep 17 00:00:00 2001
From: Claude Pache <claude.pache@gmail.com>
Date: Fri, 12 Aug 2016 19:32:52 +0200
Subject: [PATCH] Normative: Add three missing checks in proxy internal methods
 (#666)

---
 spec.html | 21 ++++++++++++++++++---
 1 file changed, 18 insertions(+), 3 deletions(-)

diff --git a/spec.html b/spec.html
index d3ecb6fec6f..d9d17b850e3 100644
--- a/spec.html
+++ b/spec.html
@@ -8968,6 +8968,8 @@ <h1>[[GetOwnProperty]] ( _P_ )</h1>
         1. If _resultDesc_.[[Configurable]] is *false*, then
           1. If _targetDesc_ is *undefined* or _targetDesc_.[[Configurable]] is *true*, then
             1. Throw a *TypeError* exception.
+          1. If _resultDesc_ has a [[Writable]] field and _resultDesc_.[[Writable]] is *false*, then
+            1. If _targetDesc_.[[Writable]] is *true*, throw a *TypeError* exception.
         1. Return _resultDesc_.
       </emu-alg>
       <emu-note>
@@ -8980,13 +8982,16 @@ <h1>[[GetOwnProperty]] ( _P_ )</h1>
             A property cannot be reported as non-existent, if it exists as a non-configurable own property of the target object.
           </li>
           <li>
-            A property cannot be reported as non-existent, if it exists as an own property of the target object and the target object is not extensible.
+            A property cannot be reported as non-existent, if the target object is not extensible, unless it does not exist as an own property of the target object.
+          </li>
+          <li>
+            A property cannot be reported as existent, if the target object is not extensible, unless it exists as an own property of the target object.
           </li>
           <li>
-            A property cannot be reported as existent, if it does not exist as an own property of the target object and the target object is not extensible.
+            A property cannot be reported as non-configurable, unless it exists as a non-configurable own property of the target object.
           </li>
           <li>
-            A property cannot be reported as non-configurable, if it does not exist as an own property of the target object or if it exists as a configurable own property of the target object.
+            A property cannot be reported as both non-configurable and non-writable, unless it exists as a non-configurable, non-writable own property of the target object.
           </li>
         </ul>
       </emu-note>
@@ -9018,6 +9023,8 @@ <h1>[[DefineOwnProperty]] ( _P_, _Desc_ )</h1>
         1. Else,
           1. If IsCompatiblePropertyDescriptor(_extensibleTarget_, _Desc_, _targetDesc_) is *false*, throw a *TypeError* exception.
           1. If _settingConfigFalse_ is *true* and _targetDesc_.[[Configurable]] is *true*, throw a *TypeError* exception.
+          1. If IsDataDescriptor(_targetDesc_) is *true*, _targetDesc_.[[Configurable]] is *false*, and _targetDesc_.[[Writable]] is *true*, then
+            1. If _Desc_ has a [[Writable]] field and _Desc_.[[Writable]] is *false*, throw a *TypeError* exception.
         1. Return *true*.
       </emu-alg>
       <emu-note>
@@ -9032,6 +9039,9 @@ <h1>[[DefineOwnProperty]] ( _P_, _Desc_ )</h1>
           <li>
             A property cannot be non-configurable, unless there exists a corresponding non-configurable own property of the target object.
           </li>
+          <li>
+            A non-configurable property cannot be non-writable, unless there exists a corresponding non-configurable, non-writable own property of the target object.
+          </li>
           <li>
             If a property has a corresponding target object property then applying the Property Descriptor of the property to the target object using [[DefineOwnProperty]] will not throw an exception.
           </li>
@@ -9165,6 +9175,8 @@ <h1>[[Delete]] ( _P_ )</h1>
         1. Let _targetDesc_ be ? _target_.[[GetOwnProperty]](_P_).
         1. If _targetDesc_ is *undefined*, return *true*.
         1. If _targetDesc_.[[Configurable]] is *false*, throw a *TypeError* exception.
+        1. Let _extensibleTarget_ be ? IsExtensible(_target_).
+        1. If _extensibleTarget_ is *false*, throw a *TypeError* exception.
         1. Return *true*.
       </emu-alg>
       <emu-note>
@@ -9176,6 +9188,9 @@ <h1>[[Delete]] ( _P_ )</h1>
           <li>
             A property cannot be reported as deleted, if it exists as a non-configurable own property of the target object.
           </li>
+          <li>
+            A property cannot be reported as deleted, if it exists as an own property of the target object and the target object is non-extensible.
+          </li>
         </ul>
       </emu-note>
     </emu-clause>