Could not resolve quantifiers for newtype

[trdthg]

type regidx_range('n) = 'n <= 1 & 'n >= 0

newtype regidx('n), regidx_range('n) = Regidx : int('n)

type s_regidx = { 'n, regidx_range('n) . regidx('n) }

mapping int_string : int <-> string = {
  0 <-> "0",
  1 <-> "1",
}

mapping encdec_reg : s_regidx <-> string = { 
  forwards Regidx(r) => int_string(r),
  backwards int_string(c) => Regidx(c), // failed here
}

Logs sail -dtc_verbose 1

Binding int_string(c) to string
Unify string and string for 
Adding type variable '_#c : Int
Binding c to int('_#c)
Adding local binding c : int('_#c)
|   Check Regidx(c) <= s_regidx
|   Function Regidx
|   Adding type variable 'n : Int
|   Adding constraint ('n <= 1 & 'n >= 0)
|   Adding constraint ('n <= 1 & 'n >= 0)
|   |   Infer c => int('_#c)
|   Unify int('n) and int('_#c) for 'n
|   Adding constraint ('n <= 1 & 'n >= 0)
|   Prove  |- regidx_range('_#c)
Type error:
../sail/test/builtins/range.sail:21.29-38:
21 |  backwards int_string(c) => Regidx(c),
   |                             ^-------^
   | Could not resolve quantifiers for Regidx
   | * regidx_range('_#c)

---

Another case

mapping encdec_reg : s_regidx <-> string = { 
  Regidx(r) => int_string(r)
}

If you run sail --just-check, it works, but if you run sail with -c, it failed. 😵‍💫

if you comment the rewriter "realize_mappings" in c_plugin, it works.

Check function encdec_reg_backwards
Binding arg# to string
Adding local binding arg# : string
|   Check match arg# { int_string(r) => Regidx(r) } <= {('n : Int), ('n <= 1 & 'n >= 0). regidx('n)}
|   |   Infer arg# => string
|   Binding int_string(r) to string
|   Unify string and string for 
|   Adding type variable '_#r : Int
|   Binding r to int('_#r)
|   Adding local binding r : int('_#r)
|   |   Check Regidx(r) <= {('n : Int), ('n <= 1 & 'n >= 0). regidx('n)}
|   |   Function Regidx
|   |   Adding type variable 'n : Int
|   |   Adding constraint ('n <= 1 & 'n >= 0)
|   |   Adding constraint ('n <= 1 & 'n >= 0)
|   |   |   Infer r => int('_#r)
|   |   Unify int('n) and int('_#r) for 'n
|   |   Adding constraint ('n <= 1 & 'n >= 0)
|   |   Prove  |- regidx_range('_#r)
Type error:
../sail/test/builtins/range.sail:20.2-11:
20 |  Regidx(r) <-> int_string(r),
   |  ^-------^
   | Could not resolve quantifiers for Regidx
   | * regidx_range('_#r)

[Alasdair]

I can't reproduce the discrepancy between --just-check and -c, but I think the failure is expected.

In the case:

backwards int_string(c) => Regidx(c),

int_string will convert a string to an int c, which we try to use to create a register index, but the integer is not guaranteed to be in the correct range, hence the error when constructing the regidx type.

You could add a guard like:

mapping encdec_reg : s_regidx <-> string = {
  forwards Regidx(r) => int_string(r),
  backwards int_string(c) if 0 <= c & c <= 1 => Regidx(c),
}

[Alasdair]

I think this case would benefit greatly from an improved error message though.

[trdthg]

but the integer is not guaranteed to be in the correct range, hence the error when constructing the regidx type.

I originally thought the type checker could not only bind c and '_#c(name from the first verbose log), but also '_#c and regidx_range('n) which came from newtype regidx('n), regidx_range('n) = Regidx : int('n).

 int_string(c)     Regidx(c)
       |              |
       c --------- int('_#c) <------- (I'm not sure are c and '_#c should be here)
                      | <------- but this couldn't be binded, right?
                      'n
                      |
                regidx_range('n)
                      |
              'n <= 1 & 'n >= 0

I can't reproduce the discrepancy between --just-check and -c

you can check the test pr #1325