Checking if a value is a number

[developedby]

This issue follows this discussion on Reddit: https://www.reddit.com/r/Kindelia/comments/vxlys5/how_to_match_numbers_in_hvm/

AFAIK, there is currently no way to check in HVM whether a value is a number or some other arbitrary term.
This would be useful for validating the input of functions on Kindelia.

Take the following contract as an example:

ctr {Inc} // Inc: action that incs the counter
ctr {Add n} // Add: action that adds to the counter
ctr {Get} // Get: action that gets the counter

fun (Counter action) {

  (Counter {Inc}) =
    ask x = (Take);
    ask (Save (+ x #1));
    (Done #0)

  (Counter {Add n}) =
      ask x = (Take);
      ask (Save (+ x n));
      (Done #0)

  (Counter {Get}) =
    ask x = (Load);
    (Done x)

} with { #0 }

When matching on constructors only, it's easy to validate the input of the Counter function, since there is only a finite and small number of acceptable constructors (Inc, Add and Get in this case).

However, for numbers it's not practical to add a rule for each possible value. Even if we were to only use a small subset of numbers, that would still possibly be hundreds or thousands of rules long.

But if we don't validate n in this function, someone could call it with (Counter {Add {Tuple0}}) and change the state to an unacceptable (+ #0 {Tuple0}) since the numeric operations only reduce when given two numbers.

What is missing here is a way to check if the input is a number and have different behaviour on each case. What I think would make sense is to have a way of matching on numbers only inside of a rule. Something like (Counter {Add #n} = ... to bind numbers only to the variable n. This would be the cheapest way in terms of mana cost.

Another alternative would be to have an operation that returns if a given value is a number or some other term. Something like (IsNum number) = #1) and (IsNum ~) = #0, where IsNum behaves in a similar way to the numeric operators.

A third way, which is what I think Kelvinss sugested in the reddit thread (edit: i misunderstood him), is to have an operator that checks if any two arbitrary values are equal, and then we could check whether it's a number with something like (Equal (% n #1) #0), where Equal returns 1 when the two terms are equal and 0 otherwise.

[developedby]

Kelvinss corrected me on reddit, it is already possible by having the following function

fun (IsZero n) {
  (IsZero #0) = #1 
  (IsZero ~ ) = #0
}

And calling it with (IsZero (% n #1)).

A wrapper like fun (IsNum n) { (IsNum n) = (IsZero (% n #1)) } achieves the second alternative in my message above, but is pretty expensive with two function calls and 1 numeric operation.

In my opinion, there should be a more idiomatic way of doing this, preferably one with very little mana cost, since I think this is a pretty common operation.

[VictorTaelin]

But if we don't validate n in this function, someone could call it with (Counter {Add {Tuple0}}) and change the state to an unacceptable (+ #0 {Tuple0}) since the numeric operations only reduce when given two numbers.

Actually this shouldn't happen. This is equivalent to a runtime error (since Kindelia's language is untyped), and should cause the whole operation to fail. It failing right now, though. Kindelia's HVM should be updated to account for that. That is an important point that I overlooked.

A IsNum operation wouldn't solve the problem regardless, since there are other ways to make computations get stuck, which would also lead to invalid states. Also, IsNum would be akin to a typeof, which is incompatible with theorem proving, since no common proof language (Coq, Idris, Agda, Lean, Kind, etc.) has runtime type-inspecting operators.

As for actually matching numbers, i don't think IsZero is too common. What is probably very common is U60.if:

(U60.if #0 t f) = f
(U60.if  n t f) = t

Which is a pretty-cheap way to perform if-then-else with a U60 condition, just like in C. Getting and setting individual bits can be done with bitwise operators.

[developedby]

If doing these operations should cause the node to reject the block, I think I'll close this issue then, since it won't be a problem.

As for actually matching numbers, i don't think IsZero is too common. What is probably very common is U60.if

Yes, I meant this general construction is common, which encompasses an if expression and some other ways to write it. I think I just worded it poorly.

Do you want me to open another issue for the problem you mentioned?