Lucas Franceschino
Lucas Franceschino
We had the issue with @cmester0 very recently. I looked half an hour in this, and we should kill the type `lhs` in favor of plain `expr`s. Then, phases can...
Related: - https://github.com/hacspec/hax/pull/970
Still relevant
We also had one student here at Inria that did some work on F* verification of some post-quantum stuff that required floats, and he wanted to try Hax for that...
It seems like this still reproduce, but I recall you did something around this @maximebuyse: do you remember something as well?
Sorry Franziskus, I missed that comment. @maximebuyse I think we wanted to fix this at some point, this should not be too complicated, what do you think?
Indeed, I agree: from a Rust perspective, an assert (that is, a conditional panic) can be seen as a side effect. However, in hax, panics are not effectful: a panic...
This is related to: - #1135
Still relevant, we discussed that recently with @maximebuyse
@maximebuyse can you look at it?