Can't resolve quantifiers for int_power but it works for ^

[Timmmm]

This is kind of surprising, unless I'm missing something:

val int_power = pure {ocaml: "int_power", interpreter: "int_power", lem: "pow", coq: "pow", c: "pow_int"}
  : forall 'x 'e, 'e >= 0. (int('x), int('e)) -> {'y, 'y >= 0 | ('x < 0 & mod('e, 2) != 0). int('y)}

overload operator ^ = {int_power}

val get_lmul_pow : unit -> {-3, -2, -1, 0, 1, 2, 3}
function get_lmul_pow() = 2
val get_sew_pow : unit -> {3, 4, 5, 6}
function get_sew_pow() = 6
val get_vlen_pow : unit -> {5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16}
function get_vlen_pow() = 5

function main() -> unit = {
    let SEW_pow  = get_sew_pow();
    let LMUL_pow = get_lmul_pow();
    let VLEN_pow = get_vlen_pow();

    let e = LMUL_pow + VLEN_pow - SEW_pow;

    let VLMAX = 2 ^ e;
    let VLMAX = int_power(2, e);
}

Output:

Type error:
main.sail:21.16-31:
21 |    let VLMAX = int_power(2, e);
   |                ^-------------^
   | Could not resolve quantifiers for int_power
   | * (('_#LMUL_pow + '_#VLEN_pow) - '_#SEW_pow) >= 0

So ^ works, but int_power() doesn't, even though they're the same?

[Timmmm]

Oh wait, actually never mind - it's because prelude.sail (which I am including) has this:

val int_power = {lem: "pow"} : (int, int) -> int

So I guess it selects that option when the more restrictive int_power fails? I'm kind of surprised it lets you declare the same val twice with different types...

Also we added that fancier type for some CHERI thing that I don't remember, but I feel like it did have some effect... is that impossible because Sail tries overloads in order and takes the first one that works?

[Timmmm]

In fact the existing type definition is definitely wrong. It allows compiling this:

print_endline(dec_str(2 ^ -3));

which prints 8.

I may have gone a bit overboard with

 : forall 'x 'e, 'e >= 0. (int('x), int('e)) -> {'y, 'y >= 0 | ('x < 0 & mod('e, 2) != 0). int('y)}

but it should probably be at least (int, nat) -> int.

[Timmmm]

it's because prelude.sail (which I am including) has this

Wait no it doesn't. I was accidentally looking at aarch64/prelude.sail which has that but lib/prelude.sail doesn't.

It seems like there's some built-in definition of ^ or something that works for integers and propagates type information properly. Is there even any need for int_power?

[Timmmm]

Oooooh wait it's because it's specifically 2^, and that has special support. Ok never mind, sorry for the noise!