Failed to prove relatively simple constraint

[Timmmm]

This code:

function write_pte forall 'n, 'n in {4, 8} . (
  pte_size : int('n),
  pte      : bits('n * 8),
) -> unit = ()

val pt_walk :
  forall 'v,
    'v in {32, 39, 48, 57} .
  (
    int('v)
  ) -> bits(if 'v == 32 then 32 else 64)

function pt_walk(
  sv_width
) = zeros()

function translate_TLB_miss
  forall 'v 'p,
    'v in {32, 39, 48, 57} &
    'p == (if 'v == 32 then 22 else 44).
(
  sv_width  : int('v),
  ppns      : bits('p),
) -> bool = {
  let pte = pt_walk(sv_width);
  let 'pte_width = if 'v == 32 then 4 else 8;
  write_pte(pte_width, pte)
}

Gives this error:

Type error:
main.sail:27.23-26:
27 |  write_pte(pte_width, pte)
   |                       ^-^ checking function argument has type bitvector(('pte_width * 8))
   | Failed to prove constraint: (if 'v == 32 then 32 else 64) == ('pte_width * 8)

Which if you expand 'pte_width is saying

   | Failed to prove constraint: (if 'v == 32 then 32 else 64) == ((if 'v == 32 then 4 else 8) * 8)

which seems quite simple to me, unless I've missed something! Any idea why this isn't working? I couldn't figure out a way around it.

[Alasdair]

I think the problem is that the if-then-else typing rule is probably inferring to something like {4, 8} and losing the connection with the 'v type variable.

I was thinking now I have if-then-else on types I can make that rule a bit more precise.

[Timmmm]

Aha, that's definitely it! If I explicitly raise let 'pte_width = if 'v == 32 then 4 else 8 to the type level by putting it in a function then it works:

...
val pte_width_bytes : forall 'v, 'v in {32, 39, 48, 57} . (int('v)) -> int(if 'v == 32 then 4 else 8)
function pte_width_bytes(sv_width) = if 'v == 32 then 4 else 8
...
  let 'pte_width = pte_width_bytes(sv_width);
  write_pte(pte_width, pte)
...

[Timmmm]

Is there a way to explicitly type annotate it too? Something like this?

let 'pte_width : {if 'v == 32 then 4 else 8} = if 'v == 32 then 4 else 8;

(I don't think I really want to use that here but I was just wondering.)

[Alasdair]

Should be fixed by: https://github.com/rems-project/sail/pull/553

You could do let 'pte_width : int(if 'v = 32 then 4 else 8) = ... I think.

[Timmmm]

Ah works perfectly now, thanks!