Lean using nat subtraction where int needed

[Alasdair]

For the test test/c/new_bitfields.sail we generate (simplifying redundant arithmetic to illustrate the issue):

def _update_B_Field0 (v : (BitVec 32)) (x : (BitVec 24)) : (BitVec 32) :=
  (Sail.BitVec.updateSubrange
    (Sail.BitVec.updateSubrange v 31 16
      (Sail.BitVec.extractLsb x 23 8) 7 0
    (Sail.BitVec.extractLsb x 7
      ((7 - 8) + 1)))

which leads to an off-by-one error as I think lean calculates (7 - 8) + 1 using natural number subtraction to 1 rather than 0.

In this case it's particularly subtle because it doesn't cause a compile error it just silently breaks the semantics.

[Alasdair]

Although it looks like it shouldn't type check because it's putting a length 7 bitvector into a length 8 place, but I guess the Coe stuff is probably kicking in somehow?

[javra]

Yes, the coercion will just silently truncate or pad

[Alasdair]

The test in question still seems to be failing on the same line, could be another issue but I don't see any other reason

[Alasdair]

It is using the -i operator, but it looks like it still thinks (7 -i 8) + 1 == 1

[Alasdair]

Could the + be casting to Nat somehow? All this implicit casting the lean is doing is pretty scary to me

[javra]

((7 -i 8) + 1) does evaluate to 0 : Int, but since extractLsb expects a Nat, it treats the addition as one in Nat and casts both summands to Nat 🤡

It's indeed quite messy, with the clean way out of it being to just have a wrapper around BitVec and all the library functions that expect an Int width. 😢

[javra]

Could we do a

val add_int = ...

val add_nat = ...

overload operator + = {add_atom, add_int, add_nat}

in arith.lean in order to assign the normal addition + whenever we have nats in Sail, and an addition +i enforcing an Int outcome (like we do for subtraction) for arbitrary ints?

[Alasdair]

Is there no way for us to just make + and - always integer arithmetic in the translated Lean?

((7 -i 8) + 1) does evaluate to 0 : Int, but since extractLsb expects a Nat, it treats the addition as one in Nat and casts both summands to Nat 🤡

Way back, we used to have both implicit casting and operator overloading in Sail, but I purged the implicit casting from the language because it leads to insanity like this where the ordering between overloading and casting matters. If Lean overloaded to the integer plus and then cast the result to nat it would work.

overload operator + = {add_atom, add_int, add_nat}

I think because of how nat in Sail is just a refinement of int this actually won't do anything. Adding a sub_nat to operator - would be incredibly dangerous though, because it has different semantics.

[javra]

Is there no way for us to just make + and - always integer arithmetic in the translated Lean?

Overloading the notation is not really advisable, but we could just have all arithmetic operations be mapped to something like -i and +i. Maybe that's what I suppose we should do as a last resort.