Lean: Adding features to support structs and bitfields

[lfrenot]

This implements the translation of bitfields, and of the operations on structs (accessing a field, editing a field, making a new instance of a struct)

[github-actions]

Test Results

   12 files  ±0     24 suites  ±0   0s ⏱️ ±0s
  749 tests +1    749 ✅ +1  0 💤 ±0  0 ❌ ±0 
2 492 runs  +1  2 492 ✅ +1  0 💤 ±0  0 ❌ ±0 

Results for commit 8242d70. ± Comparison against base commit cf168b5.

♻️ This comment has been updated with latest results.

[javra]

Looks good! The convention for Lean files is to start with an upper case, I think we'd better stick to that

[alexkeizer]

Suggested change

	def extractLsb {w: Nat} (x: BitVec w) (hi lo: Nat) : BitVec (hi - lo + 1) :=
	x.extractLsb hi lo
	def extractLsb {w : Nat} (x : BitVec w) (hi lo : Nat) : BitVec (hi - lo + 1) :=
	x.extractLsb hi lo

Lean style puts a space before the : in arguments. I did notice the rest of the file has the same formatting, so we might want to address this in a separate formatting PR and fix the whole file in one go.

[alexkeizer]

Suggested change

	def truncateLSB {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
	x.extractLsb' 0 w'
	def truncateLsb {w: Nat} (x: BitVec w) (w': Nat) : BitVec w' :=
	x.extractLsb' 0 w'

We generally treat Lsb as one word, for the sake of capitalization. (Outside of the diff of this PR, so feel free to ignore)

[alexkeizer]

Suggested change

	def update_subrange' {w: Nat} (x: BitVec w) (start len: Nat) (y: BitVec len) : BitVec w :=
	let mask := ~~~(((BitVec.allOnes len).zeroExtend w) <<< start)
	let y' := mask ||| ((y.zeroExtend w) <<< start)
	x &&& y'
	def update_subrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w :=
	update_subrange' x lo _ y
	def updateSubrange' {w: Nat} (x: BitVec w) (start len: Nat) (y: BitVec len) : BitVec w :=
	let mask := ~~~(((BitVec.allOnes len).zeroExtend w) <<< start)
	let y' := mask ||| ((y.zeroExtend w) <<< start)
	x &&& y'
	def updateSubrange {w: Nat} (x: BitVec w) (hi lo: Nat) (y: BitVec (hi - lo + 1)) : BitVec w :=
	updateSubrange' x lo _ y

Lean style uses lowerCamelCase for definitions

[alexkeizer]

Suggested change

	structure registerRef (regstate regval a : Type) where
	structure RegisterRef (regstate regval a : Type) where

In this case, RegisterRef is a type(-valued function) and thus is written UpperCamelCase! (Sorry for not catching that before)

[alexkeizer]

Again, this is stuff outside the scope of your PR diff, but since you're cleaning it up I'll comment anyway:
truncate and truncateLsb are provably equivalent. It's unclear to me why we need both definitions

[javra]

Yes, let's delete truncateLsb and avoid redundant defs.

Thank you for the annotations, @alexkeizer!

[lfrenot]

Oh I see
This is my bad, truncateLsb is supposed to extract the most significant bits, the first argument is wrong here.
Since this changes more, I think I'll just open a separate PR to fix this and the formatting

[lfrenot]

This will fail until #870 is merged, because I need the parentheses fix it introduces

[javra]

Canonical Lean style would mandate spaces inside the curly brackets. But we could also print this as

def mk_struct (i : Int) (b : (BitVec 1)) : My_struct :=
  { field1 := i
    field2 := b }

which might be better for bigger terms

[lfrenot]

I agree with your solution, I'll do that

[javra]

(Note that we don't even need the , if we do the indentation right)

[lfrenot]

To be sure I follow the style: should it be

def mk_struct (i : Int) (b : (BitVec 1)) : My_struct :=
  {
    field1 := i
    field2 := b
  }

or

def mk_struct (i : Int) (b : (BitVec 1)) : My_struct :=
  { field1 := i
    field2 := b }

[javra]

The latter

[lfrenot]

Thanks

[lfrenot]

Done

[alexkeizer]

Note that the following should also be a valid spelling of the same definition:

def mk_struct (i : Int) (b : (BitVec 1)) : My_struct where
  field1 := i
  field2 := b

Not that there's any clear benefit over this style, so I'm not suggesting we switch to it necessarily, just wanted to make you aware of the full space of options

[lfrenot]

This wouldn't be practical here I think, since the := is in the function definition, not in the expression.
but good to know

[javra]

Yes I think keeping the := is easier. This might be a task that could be given to the mighty future Lean reformatter ™