hax icon indicating copy to clipboard operation
hax copied to clipboard

Add automatic invariants for functions with `&mut` inputs

Open W95Psp opened this issue 1 year ago • 8 comments

When we translate a function with an &mut input, some properties can be guaranteed: for instance, mutating a slice will never change the size of the slice.

I think this property exist only for slices, and any type that ship a slice.

W95Psp avatar Sep 02 '24 11:09 W95Psp

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] avatar Nov 02 '24 02:11 github-actions[bot]

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.

github-actions[bot] avatar Nov 10 '24 02:11 github-actions[bot]

That is still something we want.

W95Psp avatar Nov 18 '24 08:11 W95Psp

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] avatar Jan 23 '25 01:01 github-actions[bot]

I'm having this issue in ML-DSA.

W95Psp avatar Jan 28 '25 16:01 W95Psp

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] avatar May 15 '25 00:05 github-actions[bot]

Still needed

W95Psp avatar Jul 03 '25 06:07 W95Psp

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] avatar Nov 06 '25 00:11 github-actions[bot]