WASM: Priority list of runtime & operators

[jeromesimeon]

Part of #153.

Operators

• EJsonOpNot
• EJsonOpNeg
• EJsonOpAnd
• EJsonOpOr
• EJsonOpLt
• EJsonOpLe
• EJsonOpGt
• EJsonOpGe
• EJsonOpAddString
• EJsonOpAddNumber
• EJsonOpSub
• EJsonOpMult
• EJsonOpDiv
• EJsonOpStrictEqual ( currently = EJsonRuntimeEqual)
• EJsonOpStrictDisequal ( currently = not EJsonRuntimeEqual)
• EJsonOpArray (n-ary, handled by compiler)
• EJsonOpArrayLength
• EJsonOpArrayPush
• EJsonOpArrayAccess
• EJsonOpObject _ (n-ary, handled by compiler)
• EJsonOpAccess _
• EJsonOpHasOwnProperty _
• EJsonOpMathMin
• EJsonOpMathMax
• EJsonOpMathPow
• EJsonOpMathExp
• EJsonOpMathAbs
• EJsonOpMathLog
• EJsonOpMathLog10
• EJsonOpMathSqrt
• EJsonOpMathCeil
• EJsonOpMathFloor
• EJsonOpMathTrunc

Runtime

• EJsonRuntimeEqual (** XXX First *)
• EJsonRuntimeCompare
• EJsonRuntimeToString ( XXX Third )
• EJsonRuntimeToText ( will be removed )

Record

• EJsonRuntimeRecConcat (** XXX First *)
• EJsonRuntimeRecMerge (** XXX Second *)
• EJsonRuntimeRecRemove (** XXX Second *)
• EJsonRuntimeRecProject (** XXX Second *)
• EJsonRuntimeRecDot (** XXX First *) ( = EJsonOpAccess)

Array

• EJsonRuntimeArray (n-ary, handled by compiler) = EJsonOpArray
• EJsonRuntimeArrayLength (= EJsonOpArrayLength)
• EJsonRuntimeArrayPush (** XXX Third = EJsonOpArrayPush **)
• EJsonRuntimeArrayAccess (** XXX Third = EJsonOpArrayAccess **)

Sum

• EJsonRuntimeEither (** XXX First *)
• EJsonRuntimeToLeft (** XXX First *)
• EJsonRuntimeToRight (** XXX First *)

Brand

• EJsonRuntimeBrand (** XXX Second -- not existing / eliminated? *)
• EJsonRuntimeUnbrand (** XXX Second -- eliminate with runtimeRecDot "$data" ? *)
• EJsonRuntimeCast (** XXX Second -- maybe eliminate *)

Collection

• EJsonRuntimeDistinct
• EJsonRuntimeSingleton (** XXX Second *)
• EJsonRuntimeFlatten (** XXX Second *)
• EJsonRuntimeUnion (** XXX Second *)
• EJsonRuntimeMinus (** XXX Second *)
• EJsonRuntimeMin
• EJsonRuntimeMax
• EJsonRuntimeNth (** XXX Second *)
• EJsonRuntimeCount (** XXX Second *) ( redundant with OpArrayLength )
• EJsonRuntimeContains
• EJsonRuntimeSort (** XXX Ignore *)
• EJsonRuntimeGroupBy (** XXX Ignore *)

String

• EJsonRuntimeLength
• EJsonRuntimeSubstring
• EJsonRuntimeSubstringEnd
• EJsonRuntimeStringJoin
• EJsonRuntimeLike (** XXX Not used in Ergo *)

Integer

• EJsonRuntimeNatLt
• EJsonRuntimeNatLe
• EJsonRuntimeNatPlus
• EJsonRuntimeNatMinus
• EJsonRuntimeNatMult
• EJsonRuntimeNatDiv
• EJsonRuntimeNatRem
• EJsonRuntimeNatAbs
• EJsonRuntimeNatLog2
• EJsonRuntimeNatSqrt
• EJsonRuntimeNatMinPair
• EJsonRuntimeNatMaxPair
• EJsonRuntimeNatSum
• EJsonRuntimeNatMin
• EJsonRuntimeNatMax
• EJsonRuntimeNatArithMean
• EJsonRuntimeFloatOfNat

Float

• EJsonRuntimeFloatSum
• EJsonRuntimeFloatArithMean
• EJsonRuntimeFloatMin
• EJsonRuntimeFloatMax
• EJsonRuntimeNatOfFloat

Foreign

• EJsonRuntimeForeign ( to be implemented before toString )

[pkel]

The array operators are missing on this list. They are probably important?

https://github.com/querycert/qcert/blob/wasm/compiler/core/EJson/Operators/EJsonRuntimeOperators.v#L48-L51

RuntimeArray is n-ary and the n is not known locally. I need to know the n for compilation.

[pkel]

Just updated the list to reflect the latest state. Also added the non-runtime operators.

[pkel]

I made some progress in 9578251.
I think implementing and debugging the runtime would benefit from a set of unit tests per operator. How would you do it? My current best guess is to add Imp tests per operator under /tests/operators/<operatorName>.imp_ejson. Or do you have something like this already?

[jeromesimeon]

I made some progress in 9578251.
I think implementing and debugging the runtime would benefit from a set of unit tests per operator. How would you do it? My current best guess is to add Imp tests per operator under /tests/operators/<operatorName>.imp_ejson. Or do you have something like this already?

hm. that's a really good question. And no, we don't have anything of the kind even for JS. This would be super great though.

I think one question is whether those tests are written in imp_ejson or are they written against the runtime itself (i.e., in JS, AssemblyScript).

[pkel]

I'd implement them in imp_ejson. Makes them reusable for other backends / runtime implementations.

[jeromesimeon]

I'd implement them in imp_ejson. Makes them reusable for other backends / runtime implementations.

agreed. Not sure how to make those systematic, would we like a syntax for those things.

[pkel]

Your imp_ejson parser undestands runtime operators like Runtime.array(arg0, ...). How much effort is it to do something similar for non-runtime Operators? E.g. something like Op.object(keys)(val1, val2) which translates directly to the variant type in EJsonOperators.v.

Currently, I do not fully understand the semantics of imp_ejson. Maybe such a change will help.

[jeromesimeon]

Your imp_ejson parser undestands runtime operators like Runtime.array(arg0, ...). How much effort is it to do something similar for non-runtime Operators? E.g. something like Op.object(keys)(val1, val2) which translates directly to the variant type in EJsonOperators.v.

Currently, I do not fully understand the semantics of imp_ejson. Maybe such a change will help.

🤔 I forgot we had two kinds of operators in Imp... Let me look at the parser, I think there was a reason why I only did it for runtime operators, but let me double check.

[pkel]

Now I get what you meant with "syntax for those things". I think we could do something like this.

{ "name": "Runtime Operator Equal",
  "operator": "EJsonRuntimeEqual",
  "type": "ejson_runtime_op",
  "inputs": [ [ ejson_test0_arg0, ejson_test0_arg1 ],
              [ ejson_test1_arg1, ejson_test1_arg2 ],
              ...
]}

The ejson_* parts would be actual EJson values. The semantics of the test would be

1. parse above json
2. foreach args in inputs
   1. a := imp eval operator with arguments in verified system
   2. b := wasm/js eval compiled version of the statement in unverified system
   3. if a != b then fail and print name/operator/type/args

That would be super useful. Requires some plumping on your side, though.

[jeromesimeon]

Now I get what you meant with "syntax for those things". I think we could do something like this.

{ "name": "Runtime Operator Equal",
  "operator": "EJsonRuntimeEqual",
  "type": "ejson_runtime_op",
  "inputs": [ [ ejson_test0_arg0, ejson_test0_arg1 ],
              [ ejson_test1_arg1, ejson_test1_arg2 ],
              ...
]}

yes that's what I was wondering!

The ejson_* parts would be actual EJson values. The semantics of the test would be

1. parse above json

2. foreach args in inputs

   1. a := imp eval operator with arguments in verified system
   2. b := wasm/js eval compiled version of the statement in unverified system
   3. if a != b then fail and print name/operator/type/args

That would be super useful. Requires some plumping on your side, though.

Sounds good. Let me see if I can get some traction on this, will need to page in current status. Thanks for a concrete proposal! I'll see if I can start with that.

Will need to figure out how to write ejson values (in JSON? maybe that's too obvious)

[pkel]

Will need to figure out how to write ejson values (in JSON? maybe that's too obvious)

Yes in JSON. I think you already have serializer/parsers? That's my main reason for writing the tests in JSON. I'd appreciate another format for writing the tests. Something supporting comments. But I guess that would be more work?

[jeromesimeon]

Will need to figure out how to write ejson values (in JSON? maybe that's too obvious)

Yes in JSON. I think you already have serializer/parsers? That's my main reason for writing the tests in JSON. I'd appreciate another format for writing the tests. Something supporting comments. But I guess that would be more work?

JSON = 👍

proper syntax would be more work, but yes I'd love that too. main factor will be available time I'm afraid.

[pkel]

Coming back to the operator unit test proposed above.

I think we save a lot of time by coding the tests in OCaml. I've a basic proof-of-concept working. I compose small Imp functions with one expression and one operator. Then I evaluate these function using Imp's eval and Wasm's eval and compare the result. In my opinion, the syntax is effective.

qcert/tests/operators/main.ml

Lines 87 to 99 in fd57281

	let _ =
	let open Const in
	test_op
	EJsonOpAddNumber
	[ [number 41.; number 1.]
	; [number (-1.); number 1e32]
	; [number (-1.); number Float.infinity]
	];
	test_rtop
	EJsonRuntimeNatPlus
	[ [bigint 41; bigint 1]
	; [bigint 43; bigint (-1)]
	]