Abstract equality in JSCert - argument order flipping

[tilk]

I noticed that in some cases in the definition of abstract equality, the type conversion cause the order of arguments to flip in the recursive call. This happens when the argument to be converted is the first (left) argument. So, the definition in JSCert does not follow the ES5 spec literally. This does not change semantics, but it makes this definition harder to work with. I am now trying to prove correctness of abstract equality in LambdaJS using JSCert, and with the current definition of abstract equality in JSCert, I have to account for this argument order flipping in the proof. The proof would be simpler if the argument order was preserved.

[Mbodin]

Hi,
We can annotate both side of an equality in Coq. For instance, we can
type « (t1 : T) = t2 ». I guess that it would help Coq to figure the
right coercion to be applied. Would that be better this way?
Just to know, how many such cases are there in JSCert?
Martin.

I noticed that in some cases in the definition of abstract equality,
the type conversion cause the order of arguments to flip in the
recursive call. This happens when the argument to be converted is the
first (left) argument. So, the definition in JSCert does not follow
the ES5 spec literally. This does not change semantics, but it makes
this definition harder to work with. I am now trying to prove
correctness of abstract equality in LambdaJS using JSCert, and with
the current definition of abstract equality in JSCert, I have to
account for this argument order flipping in the proof. The proof would
be simpler if the argument order was preserved.

[tilk]

I believe my question was not understood properly. I was talking about the rule red_spec_equal_1_diff_type:

      | red_spec_equal_1_diff_type : forall S C v1 v2 ty1 ty2 ext o,
          ext =
            (If ty1 = type_null /\ ty2 = type_undef then (spec_equal_2 true)
            else If ty1 = type_undef /\ ty2 = type_null then (spec_equal_2 true)
            else If ty1 = type_number /\ ty2 = type_string then (spec_equal_3 v1 spec_to_number v2)
            else If ty1 = type_string /\ ty2 = type_number then (spec_equal_3 v2 spec_to_number v1)
            else If ty1 = type_bool then (spec_equal_3 v2 spec_to_number v1)
            else If ty2 = type_bool then (spec_equal_3 v1 spec_to_number v2)
            else If (ty1 = type_string \/ ty1 = type_number) /\ ty2 = type_object then (spec_equal_3 v1 spec_to_primitive_auto v2)
            else If ty1 = type_object /\ (ty2 = type_string \/ ty2 = type_number) then (spec_equal_3 v2 spec_to_primitive_auto v1)
            else (spec_equal_2 false)) ->
          red_expr S C ext o ->
          red_expr S C (spec_equal_1 ty1 ty2 v1 v2) o

The problem is on 4th, 5th and 8th If.

[Mbodin]

OK. Here follows my thoughts about this rule: it’s not following what I
consider pretty-big-step (as we formalised it in CPP 2015, typically :p)
and thus should be changed.
It would be much better to have 9 rules much closer to the standard that
do the same.
I guess that changing would break the correctness proof, but this is
easy to fix.
Martin.

I believe my question was not understood properly. I was talking about
the rule red_spec_equal_1_diff_type:

| | red_spec_equal_1_diff_type : forall S C v1 v2 ty1 ty2 ext o,
ext =
(If ty1 = type_null /\ ty2 = type_undef then (spec_equal_2 true)
else If ty1 = type_undef /\ ty2 = type_null then (spec_equal_2 true)
else If ty1 = type_number /\ ty2 = type_string then (spec_equal_3 v1 spec_to_number v2)
else If ty1 = type_string /\ ty2 = type_number then (spec_equal_3 v2 spec_to_number v1)
else If ty1 = type_bool then (spec_equal_3 v2 spec_to_number v1)
else If ty2 = type_bool then (spec_equal_3 v1 spec_to_number v2)
else If (ty1 = type_string / ty1 = type_number) /\ ty2 = type_object then (spec_equal_3 v1 spec_to_primitive_auto v2)
else If ty1 = type_object /\ (ty2 = type_string / ty2 = type_number) then (spec_equal_3 v2 spec_to_primitive_auto v1)
else (spec_equal_2 false)) ->
red_expr S C ext o ->
red_expr S C (spec_equal_1 ty1 ty2 v1 v2) o
|

The problem is on 4th, 5th and 8th |If|.

[tilk]

I will write these rules and submit them when I'm finished.

[tilk]

By the way, I see several ways to write the rules, and they all have their drawbacks.

1. The rule red_spec_equal_1_diff_type is expanded to 9 rules, all defining the semantics for the ext_expr spec_equal_1. Here, the problem is the "otherwise" case: a condition would need to be written to list all the unhandled cases (something like ty1 = type_null \/ ty1 = type_undefined /\ ty2 = type_string \/ ty2 = type_number \/ ty2 = type_object and likewise for the symmetric case).
2. Add more ext_exprs to explicitly model the sequence of the comparisons. Then each ext_expr would have two rules, for when the relevant condition is true or false. This would be a whole lot of rules.
3. Use "continuation-passing style rules", as you do in some other parts of JSCert, to factor out the common parts of the computation. This would result in two or three rules, but a large ext_expr describing the necessary sequence of actions would need to be written.

Either way, splitting this rule alone does not really help to solve my problem; to do this, I need to change the rules for red_spec_equal_3 and red_spec_equal_4, so that a type conversion could happen for left or right argument as needed. (Currently only the right argument can be converted, which is the source of the problem.) Probably it would be enough to have two sets of rules, one for converting the left argument, and the other for the right argument.

[Mbodin]

I understand the problem.
I think that the best way to do it is the second solution you suggested. More accurately, I think that what we want is to reuse the same style than the Ecma specification.
If I’m not mistaking, we are dealing with its Section 11.9.3, “The Abstract Equality Comparison Algorithm”. This section has more than ten steps, each of them describing one of these operation.

When Arthur will succeed making the OcamlJsRef, we will have something in this form anyway: I think it’s better to start having such a form as soon as possible.
This may require some additional amount of work to write down all these new ext_expr, though…
Martin.