CDSAT specifications

[xldenis]

I'm getting ready to open up my work on formalizing CDSAT, and it requires the following changes to compile.

• Seq::to_owned_seq which turns a Seq<&T> into Seq<T>, I used to have this called just to_owned, but now this doesn't seem to compile properly?
  • I'd like to figure out why the hell this broke, but it seems like Rust's name resolution is doing something unexpected when its called just to_owned.
• Allowing proof_assert and pearlite in pearlite functions / scopes which is usefully for proving lemma functions.
• A spec for PartialEq::ne (which, duh).
• A Real::from_int function to build real numbers in the logic.
• A fix to a crash which can occur with proof_asserts

[ratmice]

• Seq::to_owned_seq which turns a Seq<&T> into Seq<T>, I used to have this called just to_owned, but now this doesn't seem to compile properly?

Curious, I tried compiling locally renaming this back to to_owned, but everything compiled okay here. Does that only occur in something downstream, or should just building creusot reproduce it? Offhand, since Seq doesn't appear to be Clone I don't think I see any reason it would conflict with the impl<T> std::borrow::ToOwned for T where T: Clone?

[xldenis]

Curious, I tried compiling locally renaming this back to to_owned, but everything compiled okay here. Does that only occur in something downstream, or should just building creusot reproduce it?

Yea, it only occurs in a downstream proof I'm working on.

Offhand, since Seq doesn't appear to be Clone I don't think I see any reason it would conflict with the impl std::borrow::ToOwned for T where T: Clone?

I think the issue is that I was working with a Ghost<Seq<T>> and Ghost is Copy.

I'd like to fix it so it is just to_owned, but in the interest of expediency (I need this proof public in two weeks), I had to make a few compromises.

[ratmice]

Thanks for clarifying, that does seem like it could trigger it.