AW: [std-proposals] Using [[assume]] attribute in contracts pre() and post() blocks

Hello. I'm wanting to make a tiny proposal of syntax, sorry in advance if I'm making it wrongly. I will be glad if you correct me how to make it correctly, if I make it in a wrong way, or the letter is in incorrect format

I'm learning new C++26 features, contracts in particular. I really like the idea, but I don't like that there is no way to treat them like a sort of invariant, that programmers can formalize, and compilers can optimize. There is an attribute [[assume(expression)]], that can be used in a function body for this purpose. But it's only about functions bodies. The contracts introduce the new syntax where you can place conditions outside the body, and it would be nice to allow using this syntax not only for asserts, but also for assumes. I'm suggesting this syntax:

int myFunction(int* ptr)

pre([[assume]] ptr != nullptr)

post([[assume]] r : r > 0);

Use [[assume]] attribute without an expression, inside "pre" and "post" conditions. What do you think about this? My key idea is to share the outside of body syntax with the different meaning of postulating pre and post conditions. Instead of "we need to be careful that this is always true", it's "I swear it's always true, I have validated it mathematically". The both ideas are good in different situations, and I think the pre() and post() syntax should be available for both of them

Alternatives can be:

Existing [[assume(expression)]] inside pre() and post() blocks, in addition to the assert expression:

int myFunction(int* ptr)

pre([[assume(ptr != nullptr)]] /* nothing here or the regular assert condition */)

post([[assume(r : r > 0)]]);

However I don't think it's a good idea to mix assume and assert in the same block. And also, assume and assert expressions can, and probably will test the same, what's incorrect, because after assuming, we cannot expect it to be false

Or:

Works as [[assume]] in ignore contracts mode, otherwise as assert:

int myFunction(int* ptr)

pre([[assume_on_ignore]] ptr != nullptr)

post([[assume_on_ignore]] r : r > 0);

But it's dangerous, because you can have radically different behavior in debug and release builds