ZeroToOne division implementation breaks invariant of [0, 1]

[saona-raimundo]

Hi! Thanks for the crate!

I come from your last post :)

I was checking your implementation of ZeroToOne and notice something.
You mentioned

ZeroToOne is a floating point number that is guaranteed to be between 0.0 and 1.0, inclusive.

But the implementation of division seems to break this.

There are various fixes: clamp after each division, check before dividing, etc.
Notice that the implementation of Div, DivAssign and Div<f32> are affected.

I say it "seems to break" because I could not compile cushy 0.2 in Windows :/
(error[E0446]: crate-private type InvalidationStatus in public interface)
I have not tested this repo yet.

[ecton]

Good catch on the faulty div implementations.

I say it "seems to break" because I could not compile cushy 0.2 in Windows :/
(error[E0446]: crate-private type InvalidationStatus in public interface)

Well now that's really odd, as there's no windows-specific code in the files that use that type. Can you provide me the full output including the command of what you're trying? What version of rust are you using?

[ddmgy]

I say it "seems to break" because I could not compile cushy 0.2 in Windows :/
(error[E0446]: crate-private type InvalidationStatus in public interface)
I have not tested this repo yet.

I was facing the same error a few days ago. It was resolved by updating rustc to the latest stable version (from 1.73.0 to 1.75.0).

[ecton]

Thank you for letting me know @ddmgy. I've fixed the issue for the next release, and I've added a CI job to test the latest MSRV.

I believe all of the issues have been resolved. Please let me know if any other edge cases are found or build issues arise!

[saona-raimundo]

Thanks for looking into it!

I confirm that updating Rust it compiles, sorry for that.

About the new implementation of division, it still fails :/
The division can lead to numbers larger than one that are not clamped.
Here is an example.

use cushy::animation::ZeroToOne;

fn main() {
	let a = ZeroToOne::new(1.0);
	let b: ZeroToOne = a / ZeroToOne::new(0.5);
	assert_eq!(b, 2.0);
}

The problem is in this line.
The checks done imply that the result will be positive, but not necessarily at most one.
It could be fixed clamping the result of the division.

[saona-raimundo]

If required, it seems simple to set up a verifier, for example Prusti or Kani.
It seems like the perfect use-case :)

[ecton]

Definitely not required, I just need to not be so stupid. Not sure what I was thinking either of the last times I touched this code. Added test cases for negative rhs and 1.0 / < 1.0.

I do love the idea of using Kani for some things however. It just really feels like overkill for this one type, and I'm not sure how much other stuff in Cushy itself is able to be fully formally verified. I think Figures would be amazing to have formal verification on, and I've thought of moving this ZeroToOne type to that crate because Kludgine could use it for opacity.

I confirm that updating Rust it compiles, sorry for that.

That's not your fault, that was my fault! No need to apologize. Thank you for reporting your issues!