search

hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
180 stars 20 forks source link

Monomorphize `unsize` #566

Open W95Psp opened 7 months ago

W95Psp commented 7 months ago

Currently, the engine assumes unsize will be an overloaded function in the backends. But only a few Rust types can be unsized, so we should monomorphize unsize in multiple specific operators.

Also, unsize on an empty array breaks F* inference.

github-actions[bot] commented 1 month ago

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

github-actions[bot] commented 1 month ago

This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.

W95Psp commented 1 month ago

Still relevant

W95Psp commented 1 month ago

This was mostly fixed in https://github.com/hacspec/hax/pull/856. But now we should investigate wether it is possible or not to remove altogether the overloaded unsize.