Rainer, thank you — your last sentence is, almost word for word, the model the draft commits to: the source states a claim; the implementation verifies it where it can, and where it can't, the claim is explicitly downgraded to assumed-and-monitored, or handed to an external analyzer.
 
Since I told Arthur upthread I had no glib answer to his example, here is the considered one. (In the draft these are contract-side assertions, budget(stack).peak <= N, rather than annotations — the question is the same in either syntax.)
 
What the number on `f` *means*: a call to `f`, callees included, consumes at most 1024 bytes of stack, relative to a named platform/ABI model. None of the four sums is the meaning; they are analyses of different precision. Composition for stack peak is own-frame + max over simultaneously-live callees — the deepest live path — not a sum. At an opaque call site the callee's *declared* bound is the assumption; where the definition is visible, the implementation may do better, which is exactly your inlining case.
 
Worked at declaration level: `buf` (1024) is live across the call to `g` and dead before `h`, so the conservative worst case is max(1024+256, 512) plus frame/call overhead — north of 1280, and `f` *fails* its own declaration at that precision. Your optimizer proves ~512 and accepts it. The meaning is fixed; provability is toolchain- and configuration-dependent. That is why the draft has three discharge modes instead of pretending everything is provable, and why the portable artefact is the form of the claim plus its discharge status — the byte value is per-model by construction.
 
Whether this layer is worth standardizing at all is the question I deliberately left open upthread, and I'm not reopening it here; I only wanted to show the semantics is pinned down rather than left to intuition.
 
— Michael




----------------------------------------------------------------------

Message: 1
Date: Tue, 9 Jun 2026 14:40:52 +0200
From: Sebastian Wittmeier <wittmeier@projectalpha.org>
To: std-proposals@lists.isocpp.org  <std-proposals@lists.isocpp.org>
Subject: Re: [std-proposals] Float the idea: First-class effect
        annotations and resource contracts for C++
Message-ID:
        <zarafa.6a2809d4.27d3.3d53e9c628cddc73@lvps176-28-11-36.dedicated.hosteurope.de>

Content-Type: text/plain; charset="utf-8"

Then any constructs, which dynamically allocate stack space have to be forbidden or need an upper limit.

?
?- no implementation specific alloca()

?- no recursion

?- function pointers including virtual functions only from a pre-defined set

?- interrupt handlers only with a separate stack

?
It should be possible to create a finite tree of possible calls and assign a fixed amount of stack space.

?
If this is possible, then instead of stack frames, one could use fixed memory locations.

?
?
?
Only with an optimizer looking deeply into the functions and the conditions, why other functions are called, variable stack frames could be more memory optimal:

?
main->A->B is possible (if condition is true)

main->A->B->D is never possible

main->B->D is possible (if condition is false)

?
A non-optimizing? system would reserve stack space for main->A->B->D. An optimizing system would use different locations for the stackframe for B, depending on whether main->A->B or main->B->D is currently executed.

?
?
?
bool condition;

?
void A() {

??? if (condition)

??????? B();

??? else

??????? C();

}

?
void B() {

??? if (!condition)

??????? D();

}

?
int main() {

??? condition = ...;

??? A();

??? B();

??? return 0;

}

?

?
-----Urspr?ngliche Nachricht-----
Von:Rainer Deyke via Std-Proposals <std-proposals@lists.isocpp.org>
Gesendet:Di 09.06.2026 13:44
Betreff:Re: [std-proposals] Float the idea: First-class effect annotations and resource contracts for C++
An:std-proposals@lists.isocpp.org;
CC:Rainer Deyke <rainerd@eldwood.com>;
On 6/8/26 17:28, Arthur O'Dwyer via Std-Proposals wrote:
> ? ? ?[[=stack_usage(256)]] void g() { }
> ? ? ?[[=stack_usage(512)]] void h();
> ? ? ?[[=stack_usage(1024)]] void f() {
> ? ? ? ?{ char buf[1024]; g(); }
> ? ? ? ?h();
> ? ? ?}
> Does `f` use 1024 bytes of stack, 1024+256 bytes, 1024+512 bytes, or
> 1024+512+256 bytes?

Assuming a halfway competent optimizer, it uses up to somewhat more than
512 bytes. ?The call to 'g' is inlined and optimized away and the 'buf'
variable is optimized away, so we're left with the call to 'h', which is
declared to take 512 bytes, plus the non-zero stack space used by the
function call itself. ?It is not possible to know how much stack space a
function actually uses in a portable manner just by looking at it, but
it's possible for the compiler to verify an upper limit to stack usage
in some cases.


--
Rainer Deyke - rainerd@eldwood.com
--
Std-Proposals mailing list
Std-Proposals@lists.isocpp.org
https://lists.isocpp.org/mailman/listinfo.cgi/std-proposals

-------------- next part --------------
HTML attachment scrubbed and removed

------------------------------

Message: 2
Date: Tue, 09 Jun 2026 07:29:39 -0700
From: Thiago Macieira <thiago@macieira.org>
To: std-proposals@lists.isocpp.org
Subject: Re: [std-proposals] Float the idea: First-class effect
        annotations and resource contracts for C++
Message-ID: <2lq5BoRTSK2cz3gq8GciRw@macieira.org>
Content-Type: text/plain; charset="utf-8"

On Tuesday, 9 June 2026 04:44:17 Pacific Daylight Time Rainer Deyke via Std-
Proposals wrote:
> Assuming a halfway competent optimizer, it uses up to somewhat more than
> 512 bytes.  The call to 'g' is inlined and optimized away and the 'buf'
> variable is optimized away, so we're left with the call to 'h', which is
> declared to take 512 bytes, plus the non-zero stack space used by the
> function call itself.  It is not possible to know how much stack space a
> function actually uses in a portable manner just by looking at it, but
> it's possible for the compiler to verify an upper limit to stack usage
> in some cases.

I don't think you can estimate the stack usage in a portable manner with any
precision. You'll have to make a massive overestimation.

For example, we have not investigated why, but recent experience is that with
MSVC 64-bit on Windows, we are getting ~300 recursions in a 1 MB stack before
a stack overflow. That's a 3400 bytes per frame, which is way more than the
local variables in our code would seem to suggest, especially when the stack
overflow on Linux (granted, 8MB stacks) takes one or two more orders of
magnitude of recursion. With just this information, I'd guess the compiler has
inserted some stack canaries to detect and prevent ROP.

So if you make a reasonable estimate with one compiler, then run another and
the value is insufficient, is that an error?

--
Thiago Macieira - thiago (AT) macieira.info - thiago (AT) kde.org
  Principal Engineer - Intel Data Center - Platform & Sys. Eng.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 870 bytes
Desc: This is a digitally signed message part.
URL: <https://lists.isocpp.org/std-proposals/attachments/20260609/c99e2551/attachment.sig>

------------------------------

Message: 3
Date: Tue, 9 Jun 2026 17:38:03 +0200
From: Rainer Deyke <rainerd@eldwood.com>
To: std-proposals@lists.isocpp.org
Subject: Re: [std-proposals] Float the idea: First-class effect
        annotations and resource contracts for C++
Message-ID: <6dbbfd30-90bb-47b6-9770-6a7a6354730d@eldwood.com>
Content-Type: text/plain; charset=UTF-8; format=flowed



On 6/9/26 16:29, Thiago Macieira via Std-Proposals wrote:
> On Tuesday, 9 June 2026 04:44:17 Pacific Daylight Time Rainer Deyke via Std-
> Proposals wrote:
>> Assuming a halfway competent optimizer, it uses up to somewhat more than
>> 512 bytes.  The call to 'g' is inlined and optimized away and the 'buf'
>> variable is optimized away, so we're left with the call to 'h', which is
>> declared to take 512 bytes, plus the non-zero stack space used by the
>> function call itself.  It is not possible to know how much stack space a
>> function actually uses in a portable manner just by looking at it, but
>> it's possible for the compiler to verify an upper limit to stack usage
>> in some cases.
>
> I don't think you can estimate the stack usage in a portable manner with any
> precision. You'll have to make a massive overestimation.

I completely agree.  In fact, you'll end up with massive overestimation
even if you limit yourself to a specific compiler and specific compiler
settings for all but the most trivial functions, because the function
arguments and the execution environment can have massive effects on the
amount of stack space a function uses.

But sometimes a massive overestimation is acceptable because provable
correctness is more important that efficiency.  Same with programs that
avoid dynamic memory allocation: horrible for efficiency (because all
memory is allocated at program start and never released), but provably
safe within its limits.

> So if you make a reasonable estimate with one compiler, then run another and
> the value is insufficient, is that an error?

There are two possible, contradictory meanings to a manually provided
stack size limit for a function:
   - I require this function to be within this limit.  The compiler
should check for me that this is the case, and fail hard when it cannot
verify that the limit is correct.
   - I know better than the compiler, and I have verified that the
function is within this limit (for this specific compiler and these
specific compiler settings).

The former sounds far more useful to me than the latter, but it's
possible to have both by adding an attribute that turns the checking off.


--
Rainer Deyke - rainerd@eldwood.com


------------------------------

Message: 4
Date: Tue, 9 Jun 2026 17:46:19 +0200
From: Sebastian Wittmeier <wittmeier@projectalpha.org>
To: std-proposals@lists.isocpp.org  <std-proposals@lists.isocpp.org>
Subject: Re: [std-proposals] Float the idea: First-class effect
        annotations and resource contracts for C++
Message-ID:
        <zarafa.6a28354b.2978.553747124a82ac70@lvps176-28-11-36.dedicated.hosteurope.de>

Content-Type: text/plain; charset="utf-8"

I professionally do a lot of programming in the Nvidia Cuda ecosystem.

?
On that platform there is manually indexed scratch and data exchange space (shared memory), temporary data with (compile-time) fixed indices (huge register file) and everything going beyond in a stack-like or indexable fashion (local memory).

?
When compiling a function one can limit the number of registers and the amount of shared memory used and can see, whether local memory is needed at all (and how much).

?
So at least for some C++ compilers and target platforms statically checking the needed stack memory is already done.
?
-----Urspr?ngliche Nachricht-----
Von:Rainer Deyke via Std-Proposals <std-proposals@lists.isocpp.org>
Gesendet:Di 09.06.2026 17:38
Betreff:Re: [std-proposals] Float the idea: First-class effect annotations and resource contracts for C++
An:std-proposals@lists.isocpp.org;
CC:Rainer Deyke <rainerd@eldwood.com>;


On 6/9/26 16:29, Thiago Macieira via Std-Proposals wrote:
> On Tuesday, 9 June 2026 04:44:17 Pacific Daylight Time Rainer Deyke via Std-
> Proposals wrote:
>> Assuming a halfway competent optimizer, it uses up to somewhat more than
>> 512 bytes. ?The call to 'g' is inlined and optimized away and the 'buf'
>> variable is optimized away, so we're left with the call to 'h', which is
>> declared to take 512 bytes, plus the non-zero stack space used by the
>> function call itself. ?It is not possible to know how much stack space a
>> function actually uses in a portable manner just by looking at it, but
>> it's possible for the compiler to verify an upper limit to stack usage
>> in some cases.
>
> I don't think you can estimate the stack usage in a portable manner with any
> precision. You'll have to make a massive overestimation.

I completely agree. ?In fact, you'll end up with massive overestimation
even if you limit yourself to a specific compiler and specific compiler
settings for all but the most trivial functions, because the function
arguments and the execution environment can have massive effects on the
amount of stack space a function uses.

But sometimes a massive overestimation is acceptable because provable
correctness is more important that efficiency. ?Same with programs that
avoid dynamic memory allocation: horrible for efficiency (because all
memory is allocated at program start and never released), but provably
safe within its limits.

> So if you make a reasonable estimate with one compiler, then run another and
> the value is insufficient, is that an error?

There are two possible, contradictory meanings to a manually provided
stack size limit for a function:
 ? - I require this function to be within this limit. ?The compiler
should check for me that this is the case, and fail hard when it cannot
verify that the limit is correct.
 ? - I know better than the compiler, and I have verified that the
function is within this limit (for this specific compiler and these
specific compiler settings).

The former sounds far more useful to me than the latter, but it's
possible to have both by adding an attribute that turns the checking off.


--
Rainer Deyke - rainerd@eldwood.com
--
Std-Proposals mailing list
Std-Proposals@lists.isocpp.org
https://lists.isocpp.org/mailman/listinfo.cgi/std-proposals

-------------- next part --------------
HTML attachment scrubbed and removed

------------------------------

Subject: Digest Footer

Std-Proposals mailing list
Std-Proposals@lists.isocpp.org
https://lists.isocpp.org/mailman/listinfo.cgi/std-proposals


------------------------------

End of Std-Proposals Digest, Vol 87, Issue 27
*********************************************