EJsonRuntimeCompare is actually a EJsonRuntimeCompareNegative

When translating Imp to Webassembly, I stumbled upon a small oddity in EJsonRuntimeOperators.v.

Section Evaluation.
...
      | EJsonRuntimeCompare =>
        apply_binary
          (fun d1 d2 =>
             match d1, d2 with
             | ejnumber n1, ejnumber n2 =>
               if float_lt n1 n2
               then
                 Some (ejnumber float_one)
               else if float_gt n1 n2
                    then
                      Some (ejnumber float_neg_one)
                    else
                      Some (ejnumber float_zero)   
...

From reading the eval, it seems that EJsonRuntimeCompare a b returns sign(b - a). The usual interpretation is sign(a - b) (ARM, OCaml).

Not sure whether this is worth fixing. It certainly doesn't matter for the verified parts.

querycert / qcert

EJsonRuntimeCompare is actually a EJsonRuntimeCompareNegative #144