Skip to content

Conversation

fdupress
Copy link
Member

This opaquely defines ceil from floor so all results on ceil apply to floor and don't need copied. We still start copying them.

This is minimally done for the purpose of a specific proof for now; feel free to ask me to make it draft for now.

@fdupress fdupress requested a review from strub May 22, 2025 12:50
@fdupress fdupress self-assigned this May 22, 2025
@strub
Copy link
Member

strub commented May 24, 2025

Overall, this is ok. But I don't understand why this PR breaks external devs.

@fdupress
Copy link
Member Author

I don't either, I'll draft it until I understand what I need for the dev anyway.

I expect some brittle SMT solvers are made cranky by the fact that there is slightly more transparency here. (And if some solvers or their why3 driver defines floor in terms of ceil, for example, we could have some looping that evades detection during saturation.)

@strub
Copy link
Member

strub commented May 24, 2025

I on't remember wether opaque definitions are sent to SMT. I'll check.

This opaquely defines ceil from floor so all results on ceil apply
to floor and don't need copied.
@strub
Copy link
Member

strub commented Aug 23, 2025

smt_opaque is the answer.

@fdupress fdupress merged commit 6ead268 into main Aug 27, 2025
15 checks passed
@fdupress fdupress deleted the better-ceil branch August 27, 2025 10:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants