field shadowing does not check for object extensibility
In the case corresponding to E-ShadowField in the semantics ("A Tested Semantics..."), the object is not checked for extensibility; the check is there in the semantics. The check is also in EcmaScript specification (8.12.4 step 8a).
The interpreter does omit this check, thanks!
S5 as a whole passes the related test cases because the 8.12.4 step 8a check is happening in the %set-property function in es5.env: https://github.com/brownplt/LambdaS5/blob/master/envs/es5.env#L1959 (which also does some work in doing the right thing for Array indices, which are another complication here).
So S5 (as a whole) correctly throws an error (assuming strict mode) on, e.g.
var o = {x: 5};
var o2 = Object.create(o);
Object.preventExtensions(o2);
o2.x = 10;
console.log(o2.x);
But the error isn't coming from the semantics, it's coming from some wrapper desugaring code.
That is definitely a check that's in the paper's semantics, and in line with the comment at https://github.com/brownplt/LambdaS5/blob/master/src/ljs/ljs_eval.ml#L73, I think I'd be happier with an extensible check in the interpreter at https://github.com/brownplt/LambdaS5/blob/master/src/ljs/ljs_eval.ml#L288, in the case where the field isn't an own property.