Lean: Fix an issue where fp_bits compilation was skipped in the float library

[nek0las]

This PR aims to fix Issue #1472. The Lean 4 backend currently skips the compilation of fp_bits because the underscore placeholder cannot infer the current Nat in BitVec(_).

This problem seems unavoidable with the current Lean 4 backend implementation, because underscores (_) are used for automatic implicit inference in existential contexts. This works in most cases as long as Lean 4 can determine the exact length from the surrounding context (for example, in Issue #1136, where the value on the RHS is known). However, when the value is an abbreviation for a type related to the existential type, Lean cannot infer the length, and a dependent pair is required to satisfy the type checker.

To minimize the impact, I reused the dependent-pair generation logic and used it in Lean 4 only when it encountered the abbrev and existential type. Broadly changing the decision logic for when to use dependent pairs versus underscores would require significant refactoring of the backend, so this PR focuses on resolving the fp_bits/abrrev related issue specifically.

The code from sail will be compiled from

type fp_bits = { 'n, 'n in {16, 32, 64, 128}. bits('n) } /* Floating-point in bits. */
type fp_bits_x2 = { 'n, 'n in {16, 32, 64, 128}. (bits('n), bits('n)) } /* Floating point x2 tuple */

to

abbrev fp_bits := Sigma (fun k_n => (BitVec k_n))
abbrev fp_bits := Sigma (fun k_n => ((BitVec k_n) × (BitVec k_n))

[bacam]

You might find test/coq/pass/existential*.sail and test/c/type_if_bits.sail useful for testing.

[github-actions]

Test Results

   16 files     36 suites   0s ⏱️
1 021 tests 1 018 ✅  3 💤 0 ❌
4 938 runs  4 896 ✅ 42 💤 0 ❌

Results for commit 2e981cc.

♻️ This comment has been updated with latest results.

[nek0las]

This change fixes the specific case of existential types introduced via type abbreviations, and the corresponding if_bits tests now pass.

The tests under test/coq/pass/existential*.sail still fail, because existential types arising from other definitions (e.g. union and struct types) are not handled yet. Supporting those cases requires a more general solution than I initially expected.

I wanted to share this status update before proceeding further, and I’d appreciate any guidance on whether extending the fix to those cases is the right next step.

[bacam]

You might find it useful to look at commit ebb9f6f5, where the Rocq support was added. It's probably a bit more complicated than the Lean backend needs; partly because that commit removes some old stuff, and partly because I think the extra explicit casts that the Rocq backend uses might be getting in the way.