Enforce that bitvectors have non-negative indices always

[Alasdair]

This commit changes the type system so that in order for bitvector('n) to be well-formed, it must be the case that 'n >= 0. To avoid making this change extremely painful, it adds a new kind Nat, which can be used in types like:

forall ('n : Nat). int('n) -> bool

The trick is then to update kind inference so

forall 'n. bits('n) -> bool

now infers Nat rather than Int for 'n. Other than taking part this extra kind-inference Nat is desugared into Int and >= 0 constraint, so there is no significant difference in how the type system works.

This means that the vast majority of Sail code should work as is, including the Sail RISC-V spec with only very minor changes. It is still a breaking change as previously we allowed

let x : list(bits(-1)) = [||]

which is now forbidden. It worked previously as bits with a negative index was treated as an uninhabited type, so while it couldn't be constructed, it could still appear in type signatures like above.

Adding this extra rule requires some refactoring of the typing context, so now we always check that unexpanded types are wellformed, rather than only checking wellformedness of expanded types.

[Alasdair]

Should not be merged before riscv/sail-riscv#559, as this change makes undefined have stricter constraints for bitvectors.

[github-actions]

Test Results

   10 files  ±0     22 suites  ±0   0s ⏱️ ±0s
  701 tests ±0    701 ✅ ±0  0 💤 ±0  0 ❌ ±0 
2 181 runs   - 1  2 180 ✅  - 1  1 💤 ±0  0 ❌ ±0 

Results for commit 6799dfb. ± Comparison against base commit 5df9e7f.

♻️ This comment has been updated with latest results.

[tobiasgrosser]

Should not be merged before riscv/sail-riscv#559, as this change makes undefined have stricter constraints for bitvectors.

This is merged already. 👍

[Alasdair]

I checked and everything is fine for sail-arm (at least the 9.4 model) and sail-riscv, but sail-cheri-riscv is pinned to an older commit of sail-riscv which doesn't typecheck with this change. I need to figure out the best way to proceed there.

I could make this a flag, either opt-in or opt-out, or we could submit a PR to that repository either with a quick patch fix to the version it's using or by doing a full update.

[tobiasgrosser]

I checked and everything is fine for sail-arm (at least the 9.4 model) and sail-riscv, but sail-cheri-riscv is pinned to an older commit of sail-riscv which doesn't typecheck with this change. I need to figure out the best way to proceed there.

I could make this a flag, either opt-in or opt-out, or we could submit a PR to that repository either with a quick patch fix to the version it's using or by doing a full update.

@Alasdair, I am happy with either of these choices. Do you favour one in particular?

[Alasdair]

I've added a flag for now, if the CI is happy I should be good to merge it.

[tobiasgrosser]

Nice.