`private function`s in Stateen support broke Lean extraction

[Ptival]

In the process of updating my "CI for Lean emulator" PR (#1541), I discovered that the Lean output was actually broken a couple of weeks ago.

The problem seems to be with 13a6693 wherein:

private function get_mstateen(idx : range(0, 3)) -> bits(64) = ...

private function get_hstateen(idx : range(0, 3)) -> bits(64) = ...

were defined.

What seems to happen for the Lean extracted code is that these functions don't appear in the output, my guess is because of this private keyword, but unfortunately, the check_stateen_bit function is extracted, and calls the above functions, resulting in:

error: LeanRV64DExecutable/Types.lean:527:60: Unknown identifier `get_sstateen`
error: LeanRV64DExecutable/Types.lean:529:52: Unknown identifier `get_hstateen`
error: LeanRV64DExecutable/Types.lean:531:53: Unknown identifier `get_hstateen`
error: LeanRV64DExecutable/Types.lean:531:88: Unknown identifier `get_sstateen`

Is anyone knowledgeable about why the functions are marked private, and what should happen in the backends?

[pmundkur]

Those functions are private since they are internal to the Stateen_regs module, so I think it's a legitimate use of the private keyword. This might be a bug in the Lean backend.

[Ptival]

Ah, I misidentified the problem!

It turns out the definitions of get_hstateen and get_sstateen are in the file, they are just after their use rather than prior.
However, they are defined within a mutual block, so the error message seems weird, I will investigate a little more.

[Ptival]

Alright, nevermind, this error was caused by a type error elsewhere that ended up creating all these spurious error messages. There are no issues with the Lean extraction.