Is pow2 of negative exponentials supported?

[Timmmm]

The 2 ^ operator is mapped to pow2, and for the C backend at least, it treats negative exponents as positive, so 2 ^ -3 is 8. _builtin_pow2 has this comment:

/* Below we need the fact that 2 ^ 'n >= 0, so we axiomatise it in the return
   type of pow2, as SMT solvers tend to have problems with exponentiation. */
val _builtin_pow2 = pure "pow2" : forall 'n, 'n >= 0. int('n) -> {'m, 'm == 2 ^ 'n & 'm >= 0. int('m)}

That suggests it is intentional. However with the OCaml backend you get a runtime error:

Exiting due to uncaught exception:
Invalid_argument("power_big_int_positive_int")

Feels like this should either be totally disallowed, or at least it should work with OCaml and should be documented because it's pretty surprising! Disallowing it may be a reasonable option - I can't really see why you'd ever need it tbh.

Not blocking or anything but a colleague asked about it and I was curious why it is like this. I think you might have explained it a long time ago but if so I've forgotten the reason.

[Alasdair]

Back in the day we didn't have the ability to check constraints as part of checking wellformedness of types, but we can do that now.

[nadime15]

Does this mean negative exponents are currently supported or will be supported?

We have this discussion going on about the vector crypto extensions that implements a function with the assumption that negative exponents are supported.

Now seeing

/* Below we need the fact that 2 ^ 'n >= 0, so we axiomatise it in the return
   type of pow2, as SMT solvers tend to have problems with exponentiation. */
val _builtin_pow2 = pure "pow2" : forall 'n, 'n >= 0. int('n) -> {'m, 'm == 2 ^ 'n & 'm >= 0. int('m)}

surprises me, because 'n should be atleast 0, so I dont understand why 2 ^ -3 results to 8? Shouldn it throw an error because of -3?

[Alasdair]

I think that definition is for some specific monomorphisation rewrite, 2 ^ n desugars to:

sail/lib/arith.sail

Line 114 in 16963e5

val pow2 = pure {lean : "_lean_pow2i", _:"pow2"} : forall 'n. int('n) -> int(2 ^ 'n)

It depends what you mean by 'support' negative exponents. The function returns an integer so it cannot return a fraction, probably best to just forbid it unless there is a good reason to take the absolute value of the exponent.

[nadime15]

The function returns an integer so it cannot return a fraction

Ok yeah true, makes sense.

Thanks!