search

querycert / qcert

Compilation and Verification of Data-Centric Languages
https://querycert.github.io/
Apache License 2.0
56 stars 9 forks source link

Suspicous EJson compare in qcert-runtime-core.js #159

Open pkel opened 3 years ago

pkel commented 3 years ago

I'm implementing the last operators for the wasm runtime. I came across the implementation of EJsonRuntimeCompare in qcert-runtime-core.js. It looks a bit suspicious to me. I cannot judge whether it's a bug or not.

https://github.com/querycert/qcert/blob/0f07b1cd6c2ca53330dc0290d5d7a64a542116b4/runtimes/javascript/qcert-runtime-core.js#L79-L133

> compare({'a': true}, {'b': true})
-1
> compare({'b': true}, {'a': true})
-1

Coq/ImpEJson specifies this compare only for floats and integers. The JS runtime uses the compare on other types (and combinations of two different types) to speed up set union and intersection (function min and function max in the linked JS file).

pkel commented 3 years ago

Further, it seems that the JS implementation of EJsonRuntimeEqual which is based on the above compare does not align with the Coq/ImpEJson specification.

Javascript runtime yields:

> compare ([1, 2], [2, 1])
0
> equal([1, 2], [2, 1])
true

ImpEJson eval (Coq/OCaml) returns false (not equal) on the same input.

pkel commented 3 years ago

My wasm implementation can be found here https://github.com/querycert/qcert/blob/a9a5365be5e0c82b861d52a65a43ec81dee66c86/runtimes/assemblyscript/assembly/index.ts#L627-L652. It aligns with ImpEJson eval according to a few tests. It easily translates to javascript. Should I open a PR?