Proxy exotic object’s [[GetOwnProperty]] algorithm permits invariant violation

[bathos]

In § 10.5.5 [[GetOwnProperty]] of Proxy exotic objects:

There is an ordering issue here. If ToPropertyDescriptor follows target.[[GetOwnProperty]], then it is possible to deceive the invariant checks which follow by returning a descriptor object that matches the descriptor returned at step 9 while deferring mutations to step 11 or step 12.

This can be leveraged to violate invariants indirectly using “layered” proxies, where the target of one proxy is another proxy. For example, it can be used to make [[Set]] return a result that violates the following invariant:

If P was previously observed as a non-configurable, non-writable own data property of the target, then [[Set]] must return false unless V is the SameValue as P's [[Value]] attribute.

"use strict";

let step = 0;

let obj = new Proxy(new Proxy({}, {
  getOwnPropertyDescriptor(target, key) {
    if (step === 0) {
      // initially called at ordinary [[Set]] -> [[DefineOwnProperty]]
      step++;
      return Reflect.getOwnPropertyDescriptor(target, key);
    } else if (step === 1) {
      // called from outer proxy exotic object [[Set]] algorithm to verify
      step++;
      return {
        ...Reflect.getOwnPropertyDescriptor(target, key),
        get writable() {
          Reflect.defineProperty(target, key, {
            configurable: false,
            enumerable: false,
            value: 7777,
            writable: false
          });
          return true;
        }
      };
    } else {
      return Reflect.getOwnPropertyDescriptor(target, key);
    }
  }
}), {
  set(target, key, value, receiver) {
    // Even though just delegating, needs to exist so that result gets verified (when step === 1)
    return Reflect.set(target, key, value, receiver);
  }
});

obj.foo = 1; // Does not throw; [[Set]] returns true
Reflect.getOwnPropertyDescriptor(obj, "foo");

// {value: 7777, writable: false, enumerable: false, configurable: false}

Here a synchronous mutation of the innermost target was successfully performed prior to [[Set]] returning a result based on “stale information”. If [[Set]] had current information when it performed subsequent validation steps, it would return false (and given the example here is in strict mode, it would throw).

I wondered if “was previously observed...” provided an out here, but it doesn’t seem to. It was observed as an unconfigurable, unenumerable, unwritable property with a different value prior to [[Set]] reporting success based on the stale information at the defineProperty call in the writable accessor. This is indirect: what is actually observed is another fact that causes the requirement to exist for the outer object. The indirection doesn't matter, though, and the reason why becomes clearer if framed in terms of consequences for the “knowledge model”: if [[Set]] can report a stale result, then no juncture exists where the caller is granted guaranteed-until-control-yield knowledge that conforms to the invariant, which is the same as saying the purported invariant cannot be observed to exist ... which is the same as saying it doesn’t exist.

The proxy trap algorithms appear to have been designed carefully to avoid things like this. Nested proxies don’t open up holes like this in any other traps AFAIK because ordering ensures that even in reentrant cases it’s never possible for the outer internal method’s verification steps to operate on stale information. I believe the [[GetOwnProperty]] steps could also be reordered to, like the others, avoid validating stale information too. It would need to be something like this (note 12 must also precede 11 for similar reasons to what was demonstrated above):

• 7
• 8
• 12
• 11
• 9
• 10

If this were to be fixed, it would be an observable/normative change. The result would not be that mutations of the kind shown above would become impossible, it would be that [[Set]] (or other “outer” internal methods that rely on the inner [[GetOwnProperty]] would throw if they occurred and a normal completion would report reliably truthful information.

(@erights I think this is in your wheelhouse — perhaps you could verify that what I’ve described makes sense.)

[bathos]

One thing I should add: this can get really confusing really quickly because you have to think about nested sequences of traps and how the algorithms are (normally) ensuring soundness despite various forms of possible reentry. I sat on this for a while before opening the issue trying to confirm whether (a) this does actually constitute a violation and (b) if so, whether it's remediable. I am now pretty confident that both are true, but it's tricky to sum up. I may lack certain vocabulary that would be useful.

[bakkot]

That's a nice find!

I agree it would make more sense for the ToPropertyDescriptor call to be earlier, since it's observable, but I am not yet convinced that the current semantics actually violate the invariants. In particular, you can accomplish the same thing as your code snippet with

let obj = {
  set foo(x) {
    Object.defineProperty(this, 'foo', { writable: false, configurable: false, value: 7777 }); 
  },
};

obj.foo = 1; // Does not throw; [[Set]] returns true
Reflect.getOwnPropertyDescriptor(obj, 'foo');

The reason it doesn't violate the invariant because the invariant is phrased as "if you observe a property to be non-configurable non-writable, then its value doesn't change", which places absolutely no requirements on properties which are configurable. Your trick doesn't allow you to get around that, from what I can tell: the [[Set]] succeeding certainly does not imply the property is non-configurable, so it's only in the very last line that you observe the property to be non-configurable non-writable, and indeed the value can never thereafter change. Right?

[erights]

Still absorbing. Thanks for finding and explaining!

Attn @tvcutsem

[bathos]

In particular, you can accomplish the same thing as your code snippet with [...]

The invariant in question was this:

If P was previously observed as a non-configurable, non-writable own data property of the target, then [[Set]] must return false unless V is the SameValue as P's [[Value]] attribute.

My contention is that it was effectively observed as an unconfigurable data property:

This is indirect: what is actually observed is another fact* that causes the requirement to exist for the outer object**.

* that the target has an unconfigurable data property — this observation occurs when it gets defined as unconfigurable prior to [[Set]] returning

** if the target is observed to have an unconfigurable data property, then other invariants establish that the proxy also does.

I am not yet convinced that the current semantics actually violate the invariants

I’m with you there. I went back and forth trying to figure that out a lot and my conclusion could be wrong, or could be wrong wrt [[Set]] specifically. I’d considered the accessor case and although I hesitated to make this claim because of how silly it would sound, I believe that ... also violates the invariant. Bear with me: what I mean is that I think the invariant itself is written slightly wrong. The “previously” in other cases seems to mean “at any point prior to returning,” not “at any point prior to invocation of this internal method”. The Proxy trap algorithms go to some lengths ensuring the “at any point prior to returning” behavior — apart from this one case, which appears likely accidental.

In any case, it may also be that [[Set]] was a poor choice for demonstration. The GOPD “hook” affects other operations as well, some of which have no (seemingly?) analogous accessor realization.

"use strict";

let obj = new Proxy(new Proxy({}, {
  getOwnPropertyDescriptor(target, key) {
    return {
      get configurable() {
        Reflect.defineProperty(target, key, { configurable: false, value: 3 });
        console.log("(inner)", key, "exists and is unconfigurable?", !Reflect.getOwnPropertyDescriptor(target, key).configurable);
        return true;
      }
    };
  }
}), {
  has(target, key) {
    return Reflect.has(target, key);
  }
});

console.log("(outer) foo exists?", "foo" in obj);
// (inner) foo exists and is unconfigurable? true
// (outer) foo exists? false

And keep in mind that if the above works (and it does), then the invariant “A property cannot be reported as non-existent, if it exists as a non-configurable own property of the target object.” becomes meaningless because it cannot be reliably observed to be true or false; code cannot rely on it holding. If not for the GOPD ordering issue, a false return value for "foo" in obj would prove that obj, at that specific moment, does not have an unconfigurable "foo" (and that “fact” can be derived from the claimed invariants if read like uh ... those logic puzzles with the big grid that I remember from elementary school ... god I loved those).

[claudepache]

Hi,

I think indeed (after a cursory review) that the ? IsExtensible(target) call should be done before the ? _target_.[[GetOwnProperty]](_P_) call, both in the [[GetOwnProperty]] and the [[[DefineOwnProperty]] algorithms. Some time ago, I intended to analyse the case of multiple checks on exotic targets in /claudepache/es-invariants ; but until now it’s not done.

Even more mind-blowing, there is the case of reentrancy, where an inner call to a proxy trap is triggered after, but returns (and is observed) before, an outer call.

Swapping the ? _target_.[[GetOwnProperty]](_P_) and ? IsExtensible(target) calls might be sufficient for not-too-weird exotic targets, i.e. those that doesn’t trigger reentrancy. However, when the target is itself a proxy, I think that the checks should be done on the target’s target instead, which I claim is equivalent to doing the checks on the target when the target’s traps are side-effect free (but I must still prove it).

[bathos]

However, when the target is itself a proxy, I think that the checks should be done on the target’s target instead, which I claim is equivalent to doing the checks on the target when the target’s traps are side-effect free (but I must still prove it).

That is very interesting. It would require a pretty rigorous proof but it seemingly should be true in all normal-completion scenarios - and it would eliminate not only the issue described here, but also would significantly reduce the risk of other issues like it (and perhaps would afford implementations more flexibility for optimization of PEOs?).

However it would not be equivalent in abrupt completion scenarios and that might actually matter. Currently it is possible to realize the behavior of a revoked PEO with an unrevoked PEO (modulo the piercing behaviors of IsArray / GetFunctionRealm) just by having every handler throw. If the validation pierced, this would no longer be generically true. It also wouldn't be surprising if there's existing code whose behavior depends in some way on the current observability of these checks for target-is-also-a-PEO cases. So I'm not sure if it's a plausible change, though I share your intuition that in all "normal" cases it should be correct.

[bakkot]

My contention is that it was effectively observed as an unconfigurable data property:

This is indirect: what is actually observed is another fact* that causes the requirement to exist for the outer object**.

• that the target has an unconfigurable data property — this observation occurs when it gets defined as unconfigurable prior to [[Set]] returning ** if the target is observed to have an unconfigurable data property, then other invariants establish that the proxy also does.

I'm still not following. How is anyone observing a non-configurable property on the Proxy prior to the last line? Observations about the target aren't relevant - the only point of the target is to enforce invariants about what someone who is interacting with only the Proxy observes.

It's true that this allows the Proxy's code to observe a fact about the target of the Proxy which is inconsistent with what other code is going to subsequently observe about the Proxy itself, but that does not by itself constitute a violation of the invariant. The invariant is only about a single object, in this case the Proxy. The fact that this is internally enforced by checks against the target is irrelevant; the invariant doesn't say anything about the target.

---

I believe that ... also violates the invariant. Bear with me: what I mean is that I think the invariant itself is written slightly wrong.

I'm not seeing it. As far as I can tell, in the snippet of code I gave, there are exactly two places that the consumer of obj observes facts about its foo property - first in the obj.foo = 1 line, where it observes the property either 1.) already has the value 1, 2.) has a non-throwing setter, or 3.) is writable, and second in the explict getOwnPropertyDescriptor, where it observes a full non-configurable non-writable property descriptor.

Since there is no observation of obj which happens subsequent to the point where it is observed to be non-configurable non-writable, I don't see how it could possibly violate the invariant.

---

console.log("(outer) foo exists?", "foo" in obj);

And keep in mind that if the above works (and it does), then the invariant “A property cannot be reported as non-existent, if it exists as a non-configurable own property of the target object.” becomes meaningless because it cannot be reliably observed to be true or false; code cannot rely on it holding. If not for the GOPD ordering issue, a false return value for "foo" in obj would prove that obj, at that specific moment, does not have an unconfigurable "foo"

So, two things. First, no, it would not prove that; it's possible even without trapped property descriptors:

let inner = new Proxy({}, {
  isExtensible(t) {
    Object.defineProperty(t, 'foo', { value: 'I exist', configurable: false });
    return Reflect.isExtensible(t);
  },
  getOwnPropertyDescriptor(t, k) {
    if (k in t) {
      return Reflect.getOwnPropertyDescriptor(t, k);
    }
    return { value: null, configurable: true };
  },
});
let outer = new Proxy(inner, {
  has(t, k) {
    return Reflect.has(t, k);
  },
});

console.log('foo' in outer); // false
console.log(Reflect.getOwnPropertyDescriptor(outer, 'foo')); // { value: 'I exist', ... }

and second, to the extent this particular example is a problem, it's a problem with the Notes about a Proxy's [[GOPD]]/[[Has]], not about the actual object invariants.

The point of the target is to enforce that consumers of the Proxy observe certain invariants. (For this reason I prefer to call the thing currently called the "target" instead the "witness".) Those invariants are primarily of the form "once you see the object has is locked down in a certain way, it does not subsequently change with respect to that". So the fact that the target can be in a weird state with respect to what consumers of the Proxy will subsequently observe can never be a problem with the fundamental invariants, in itself; to get an invariant violation, you have to have a consumer of the Proxy see a property of the Proxy which is locked down and subsequently changes.

Consumers of the Proxy which observe a property to be not locked down get absolutely no guarantees about that property. It may (or may not) be the case that there are certain guarantees you actually can get about the object not changing, because of the particular order in which Proxy traps happen to be invoked, but that fact is entirely incidental; it's not something which is intentional (and host exotics would be permitted to violate it). The only invariants you're supposed to get are these.

In other words, "A property cannot be reported as non-existent, if it exists as a non-configurable own property of the target object" isn't supposed to be something the consumer of the Proxy can rely on, because it's a fact about the relationship of the Proxy and its target, rather than about the Proxy considered as a single object. The point of the Notes which make this claim is to explain how the Proxy checks enforce the fundamental invariants, not to lay out new ones.

We could make the Notes more precise by changing the current "A property cannot be reported as non-existent, if it exists as a non-configurable own property of the target object" to the more precise "A property cannot be reported as non-existent, if it existed as a non-configurable own property of the target object prior to invoking this internal method". All the Proxy notes could reasonably be rephrased in a similar manner, since that's all they're supposed to claim: "if a particular thing was true of the target/witness prior to invoking the trap, then it constrains the result of the trap in a particular way", which allows you to draw conclusions about the invariants observed by the consumer of the Proxy. They're not intended to say anything about weirdness in the middle of the execution of the trap.

[bathos]

That makes sense. I think the example you gave could also be interpreted as the IsExtensible check in [[HasProperty]] being another ordering issue, but that it was one I didn't catch gives me plenty of pause about my prior interpretation.

We could make the Notes more precise by changing the current "A property cannot be reported as non-existent, if it exists as a non-configurable own property of the target object" to the more precise "A property cannot be reported as non-existent, if it existed as a non-configurable own property of the target object prior to invoking this internal method".

I think this is a very good idea. If the examples thus far aren't invariant-violating, this language would make it a lot more clear why that would be the case; it is currently very tempting to view the invariants (including their "note" versions) as forming a kind of truth table where more facts are "transitive" than may be intended.

Regardless of its status as violating, it seems you agreed that an ordering change in [[GetOwnProperty]] was potentially desirable. (It would seemingly reduce the range of possible shenanigans a good deal.) Is that still true, and do others agree?

[bakkot]

I think this is a very good idea.

PRs welcome! Otherwise I'll get to it eventually, but likely not as a high priority.

it seems you agreed that an ordering change in [[GetOwnProperty]] was potentially desirable

Well, I definitely agree that it would be better if it had been specified the way you suggest originally (at least moving the ToPropertyDescriptor up), but I'm not totally convinced it's worth the effort to change it now, which is to say, to ask all committee members to spend time thinking about it and to ask implementors to do the work of rewriting this part of their Proxy implementations and risk shipping a breaking change. Though the risk of breakage seems low and I suppose most implementations have implementations for the Proxy traps which are pretty straightforward translations of the spec steps (e.g. here's V8's), so it's probably not that much work.

I'm unlikely to champion this change, but maybe someone else is more enthusiastic about it.

[bathos]

BTW regarding

Observations about the target aren't relevant - the only point of the target is to enforce invariants about what someone who is interacting with only the Proxy observes. [...]

We can adjust the demonstration to directly hit the outer object and it will still work. Assuming the invariant concerns only "prior to this invocation" observation as you stated, this doesn't alter your central point - but it is possible to interleave things so that the unconfigurable property of the outermost proxy itself gets observed prior to the outer invocation's completion.

"use strict";

let obj = new Proxy(new Proxy({}, {
  getOwnPropertyDescriptor(target, key) {
    if (Object.hasOwn(target, key)) return Reflect.getOwnPropertyDescriptor(target, key);

    return {
      get configurable() {
        Reflect.defineProperty(target, key, { configurable: false, value: 3 });
        console.log("(outer)", key, "exists and is unconfigurable?", !Reflect.getOwnPropertyDescriptor(obj, key).configurable);
        return true;
      }
    };
  }
}), {
  has(target, key) {
    return Reflect.has(target, key);
  }
});

console.log("(outer) foo exists?", "foo" in obj);
// (outer) foo exists and is unconfigurable? true
// (outer) foo exists? false

[bakkot]

Aha, very clever. I think that one does arguably constitute a violation of the essential invariants, given how they're written, though it's a little hard to say - the invariants are phrased as if "observations" occur at a single instant, whereas for Proxies the observation (that is, the invocation of the traps) takes place over a period of time, during which other stuff can be happening. It's not clear how the invariants are supposed to apply to observations which take place during other observations.

Specifically, the relevant invariant is

If P was previously observed as a non-configurable own data or accessor property of the target, [[HasProperty]] must return true.

("target" meaning "the thing on which [[HasProperty]] is being invoked", nothing to do with proxies)

and it's not clear if "previously" means "prior to the invocation of [[HasProperty]] or "prior to [[HasProperty]] returning".

[bathos]

Exactly, yep. It seems you have successfully transformed my confusing "hey I'm pretty sure this is weird and maybe wrong somewhere, also I think it can be fixed in this particular case but maybe not" into a way more cogent general problem statement, thanks for talking this through.

[claudepache]

the invariants are phrased as if "observations" occur at a single instant, whereas for Proxies the observation (that is, the invocation of the traps) takes place over a period of time, during which other stuff can be happening.

An “observation” should be deemed to happen the precise instant the corresponding essential method returns nonabruptly – which, for trapped methods, is happening after the result returned by the trap has been successfully sanitised and validated.

[bathos]

@claudepache The oddness here, in particular in the most recent example, is that there’s an observation of the "foo" property of the “witness object” as an extant unconfigurable/unwritable property which occurs before witness.[[HasProperty]] returns a normal completion value of false.

The observation in question happens during the evaluation of witness.[[HasProperty]], though, which bakkot contends (I think) should probably be kosher (but tentatively(?) agrees that the current spec text is either ambiguous about this matter or incorrect).

My original expectation was that the order of operations within the PEO internal methods should ensure that such things aren’t possible to begin with, but I’m no longer sure that would actually be possible to achieve: there are some cases where reordering would “fix” this, but perhaps not all. If it isn’t possible (or if it is, but isn’t considered worthwhile or safe to change), then I think it becomes necessary to consider only observations that occurred prior to invocation of the internal method to be relevant to the invariants. This makes “what happens during invocation” a kind of no-mans-land where it’s acknowledged that something that really isn’t a “single instant” is “simulating” one and that a few laws of physics get a lil loopy.

In a sense that means it’s the “start” rather than the “end” that would constitute an observation (though “start” and “end” are indistinguishable for everything except proxies). If during-invocation observations are considered “after”, with the answer to “but ... we didn’t return a result yet...!” being “hush! begone ye foul imp!”, no invariants end up violated.

[claudepache]

Hoisting the “? ToPropertyDescriptor(trapResult)” step (and other similar steps in other algorithms) before any invocation on the target will resolve the specific examples given in this thread. But (in the [[GetOwnProperty]] algorithm) there is no way to reorder the to following invocations on the target in order to tame the weirdest cases:

• S1 — ? target.[[GetOwnProperty]](P)
• S2 — ? IsExtensible(target)

Indeed, consider the following situation:

• The proxy trap corresponding to [[GetOwnProperty]](P) claims that the property P exists and is configurable.

In the sanity check that follows the call to the trap and the (now hoisted) “? ToPropertyDescriptor(trapResult)” step, we need to perform one or more of S1 or S2. The two following conditions, must be checked:

• C1 — P should not be a nonconfigurable property on the target; for checking this, S1 must be triggered.
• C2 — In case the property P is absent on the target, the target must be extensible; for checking this, S2 may need to be triggered.

With a carefully crafted target, a call to S1 might invalidate C2, and a call to S2 might invalidate C1.

However, in order to turn such an invalidation into an effective violation of an invariant, S1 or S2 must not only invalidate the relevant condition, but also trigger a corresponding observation on the original proxy. (Recall that we have already moved the other potentially side-effectful operation before any invocation on the target, so that the observation must be done inside S1 or S2.) That requires that the proxy and its target carefully conspire. Constructing such an example is an order of magnitude more brain-twisting than the examples given in its thread, because these ones did not require cooperation between the traps and the target.

---

I think that the only solution to this fringe edgy corner case, is to disregard the target if it is a proxy and to do the check on the target’s target. The main BC issue is that it would no longer be possible for the intermediate target to deny access (willfully or accidentally) to the result by throwing. (But note that the target cannot deny access to the operation itself, only to its result, because it is consulted only after the trap is triggered.)

But in any case (whether we take this route or not), we could already review all the algorithms, and make sure that any potentially side-effectful operation that does not involve the target (such as “?ToPropertyDescriptor(trapResultObj)”) is performed before any access to the target itself. That would limit the problems to weird targets coupled in a weird way to weird traps, and it would no longer be possible to make the demonstration with a sane proxy around a weird target as @bathos did.

[bakkot]

[edit: ah, I see @claudepache posted much the same comment while I was typing this. Still, perhaps the concrete example is helpful.]

Indeed, as @bathos speculates, it is not possible to ensure this invariant holds if the observation is deemed to happen when a method returns.

The fundamental problem is that checking some invariants requires invoking multiple proxy traps, which can invoke arbitrary other code, some of which may change earlier invariants and observe that change.

For example, if [[HasProperty]] is to return false it needs to check 1.) if the target has that property as non-configurable and 2.) if it does not, that the target is extensible. This means it will necessarily need to invoke both the [[GetOwnProperty]] and the [[IsExtensible]] traps on the target. And whichever is invoked second can, in at least some circumstances, change the result of future invocations of the other and then observe it before returning.

Concretely, given how [[HasProperty]] is currently specified, you can do that with

'use strict';

// If P was previously observed as a non-configurable own data or accessor property of the target, [[HasProperty]] must return true. 

function observeOuterFoo() {
  console.log('outer.foo is', Object.getOwnPropertyDescriptor(outer, 'foo'));
}

let hitTrap = false;
let inner = new Proxy({ foo: 0 }, {
  isExtensible(target) {
    if (!hitTrap) {
      hitTrap = true;
      Object.defineProperty(target, 'foo', { value: 1, configurable: false });
      observeOuterFoo();
    }
    return true;
  },
});

let outer = new Proxy(inner, {
  getOwnPropertyDescriptor(target, key) {
    return Reflect.getOwnPropertyDescriptor(target, key);
  },
  has(target, key) {
    if (key === 'foo' && !hitTrap) {
      return false;
    }
    return Reflect.has(target, key);
  }
});

console.log('foo in outer:', 'foo' in outer);

which prints

outer.foo is { value: 1, configurable: false }
foo in outer: false

which, if observations are understood to happen when an internal method returns, is a violation of the invariant that

If P was previously observed as a non-configurable own data or accessor property of the target, [[HasProperty]] must return true.

since in this example foo is observed to be a non-configurable own data property and then subsequently [[HasProperty]] returns false. And this is not repairable by re-ordering the calls to the traps; you have to call both isExtensible and getOwnPropertyDescriptor on the target in some order, and whichever is second can (unless the target is already locked down) change what would be returned by the other and observe that change.

I think the invariants need to be phrased as "if some property was observed prior to invoking the internal method, then it constrains the return value of the internal method".

[bakkot]

I think that the only solution to this fringe edgy corner case, is to disregard the target if it is a proxy and to do the check on the target’s target.

I really don't want to pierce through the Proxy to the target if it's at all avoidable.

I think my proposed fix works: rephrase the invariants to say "if some property was observed prior to invoking the internal method, then it constrains the return value of the internal method". Then it doesn't matter that an internal method might check two traps on an inner proxy which may invalidate each other, because that invalidation necessarily happens after the internal method begins execution.

[claudepache]

I think that the only solution to this fringe edgy corner case, is to disregard the target if it is a proxy and to do the check on the target’s target.

I really don't want to pierce through the Proxy to the target if it's at all avoidable.

It would be hardly more piercing than the current situation: the only way that a Proxy (in our case, a Proxy which is a target of another Proxy) may avoid any call to its own target (as part of a sanity check), is to have traps that throw. Also, note that, anyway, the results of the calls made during the sanity checks are never disclosed.

[bakkot]

It's less about revealing information about the target and more about clarity - it's already hard to reason about Proxies, and adding more special cases when the target is itself a Proxy would make it significantly more so.

Besides, it doesn't actually solve the problem, since host exotic objects are also permitted to have side-effecting traps without specifically being Proxies. It's much cleaner to handle all kinds of target objects equivalently.

[bathos]

I wish claudepache's solution were on the table (I think it makes things simpler, not more complex? ~I'm unclear on how it would lead to a need for branching on proxy vs non-proxy in the invariants, at least~ edit: misread that, got it now) - but I would be very surprised if it were not too aggro of an overhaul to be viable / be web safe / garner interest. I also have a hunch that the block-by-throwing case has to be maintained as-is. Not that a hunch is worth much ... but maybe somebody with a sharper brain will be able tell me where that intuition is coming from and whether it's actually true :)

(Much admiration tho for both claude's elegant vision for how it probably should have worked and bakkot's clever & tidy but this is how it does work solutions.)