qcert icon indicating copy to clipboard operation
qcert copied to clipboard

Published 20 hours ago • verified publisher icon querycert

WASM: Priority list of runtime & operators

Open jeromesimeon opened this issue 5 years ago • 13 comments

Part of #153.

Operators

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

Runtime

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

Record

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

Array

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

Sum

  • [x] EJsonRuntimeEither (** XXX First *)
  • [x] EJsonRuntimeToLeft (** XXX First *)
  • [x] EJsonRuntimeToRight (** XXX First *)

Brand

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

Collection

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

String

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

Integer

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

Float

  • [x] EJsonRuntimeFloatSum
  • [x] EJsonRuntimeFloatArithMean
  • [x] EJsonRuntimeFloatMin
  • [x] EJsonRuntimeFloatMax
  • [x] EJsonRuntimeNatOfFloat

Foreign

  • [ ] EJsonRuntimeForeign ( to be implemented before toString )

jeromesimeon avatar Jul 10 '20 13:07 jeromesimeon

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 avatar Jul 13 '20 13:07 pkel

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

pkel avatar Jul 17 '20 14:07 pkel

I made some progress in 95782518286. 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?

pkel avatar Mar 08 '21 17:03 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?

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).

jeromesimeon avatar Mar 10 '21 12:03 jeromesimeon

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

pkel avatar Mar 10 '21 12:03 pkel

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.

jeromesimeon avatar Mar 10 '21 12:03 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.

pkel avatar Mar 10 '21 12:03 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.

🤔 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.

jeromesimeon avatar Mar 10 '21 12:03 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 ],
              ...
]}

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.

pkel avatar Mar 10 '21 13:03 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 ],
              ...
]}

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)

jeromesimeon avatar Mar 10 '21 13:03 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?

pkel avatar Mar 10 '21 13:03 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?

JSON = 👍

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

jeromesimeon avatar Mar 10 '21 13:03 jeromesimeon

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.

https://github.com/querycert/qcert/blob/fd572815675f125a2147bd6ebeffbb5940ce88b0/tests/operators/main.ml#L87-L99

pkel avatar May 04 '21 10:05 pkel