Suspicous EJson compare in qcert-runtime-core.js

[pkel]

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.

qcert/runtimes/javascript/qcert-runtime-core.js

Lines 79 to 133 in 0f07b1c

	function compare(v1, v2) {
	var t1 = typeof v1, t2 = typeof v2;
	if (t1 === 'object' && v1 !== null) {
	if (isNat(v1)) { t1 = 'number'; v1 = unboxNat(v1); }
	if (isBoxColl(v1)) {
	v1 = unboxColl(v1).slice(0, collLength(v1));
	}
	};
	if (t2 === 'object' && v2 !== null) {
	if (isNat(v2)) { t2 = 'number'; v2 = unboxNat(v2); }
	if (isBoxColl(v2)) {
	v2 = unboxColl(v2).slice(0, collLength(v2));
	}
	}
	if (t1 != t2) {
	return t1 < t2 ? -1 : +1;
	}
	var a1 = {}.toString.apply(v1), a2 = {}.toString.apply(v2);
	if (a1 != a2) {
	return a1 < a2 ? -1 : +1;
	}
	if (a1 === '[object Array]') {
	v1 = v1.slice(); /* Sorting in place leads to inconsistencies, notably as it re-orders the input WM in the middle of processing */
	v2 = v2.slice(); /* So we do the sort/compare on a clone of the original array */
	v1.sort(compare);
	v2.sort(compare);
	}
	if (t1 === 'object') {
	var fields1 = [];
	var fields2 = [];
	for (var f1 in v1) { fields1.push(f1); }
	for (var f2 in v2) { fields2.push(f2); }
	fields1 = fields1.sort(compare);
	fields2 = fields2.sort(compare);
	for (var i = 0; i < fields1.length; i=i+1) {
	if (!(Object.prototype.hasOwnProperty.call(v2,fields1[i]))) {
	return -1;
	}
	var fc = compare(v1[fields1[i]], v2[fields1[i]]);
	if (fc != 0) {
	return fc;
	}
	}
	for (var i = 0; i < fields2.length; i=i+1) {
	if (!(Object.prototype.hasOwnProperty.call(v1,fields2[i]))) {
	return +1;
	}
	}
	return 0;
	}
	if (v1 != v2) {
	return v1 < v2 ? -1 : +1;
	}
	return 0;
	}

> 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]

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]

My wasm implementation can be found here

qcert/runtimes/assemblyscript/assembly/index.ts

Lines 627 to 652 in a9a5365

	if (a instanceof EjArray && b instanceof EjArray) {
	let va = changetype<EjArray>(a).values.slice() ;
	let vb = changetype<EjArray>(b).values.slice() ;
	let i = 0;
	while (i < va.length && i < vb.length) {
	let c = compare(va[i], vb[i]);
	if (c != 0) { return c; };
	i++;
	}
	return compare_base<i32>(va.length, vb.length);
	}
	if (a instanceof EjObject && b instanceof EjObject) {
	let oa = changetype<EjObject>(a).values ;
	let ob = changetype<EjObject>(b).values ;
	let ka = oa.keys().sort();
	let kb = ob.keys().sort();
	let i = 0
	while (i < ka.length && i < kb.length) {
	let c = compare_base<string>(ka[i], kb[i]);
	if (c != 0) { return c; };
	c = compare(oa[ka[i]], ob[kb[i]]);
	if (c != 0) { return c; };
	i++;
	}
	return compare_base<i32>(ka.length, kb.length);
	}

. It aligns with ImpEJson eval according to a few tests. It easily translates to javascript. Should I open a PR?