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_at_[hidden]>
> To: std-proposals_at_[hidden] <std-proposals_at_[hidden]>
> Subject: Re: [std-proposals] Float the idea: First-class effect
> annotations and resource contracts for C++
> Message-ID:
> <
> zarafa.6a2809d4.27d3.3d53e9c628cddc73_at_lvps176-28-11-36.dedicated.hosteurope.
> >
>
> 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_at_[hidden]>
> 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_at_[hidden];
> CC:Rainer Deyke <rainerd_at_[hidden]>;
> 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_at_[hidden]
> --
> Std-Proposals mailing list
> Std-Proposals_at_[hidden]
> 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_at_[hidden]>
> To: std-proposals_at_[hidden]
> Subject: Re: [std-proposals] Float the idea: First-class effect
> annotations and resource contracts for C++
> Message-ID: <2lq5BoRTSK2cz3gq8GciRw_at_[hidden]>
> 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_at_[hidden]>
> To: std-proposals_at_[hidden]
> Subject: Re: [std-proposals] Float the idea: First-class effect
> annotations and resource contracts for C++
> Message-ID: <6dbbfd30-90bb-47b6-9770-6a7a6354730d_at_[hidden]>
> 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_at_[hidden]
>
>
> ------------------------------
>
> Message: 4
> Date: Tue, 9 Jun 2026 17:46:19 +0200
> From: Sebastian Wittmeier <wittmeier_at_[hidden]>
> To: std-proposals_at_[hidden] <std-proposals_at_[hidden]>
> Subject: Re: [std-proposals] Float the idea: First-class effect
> annotations and resource contracts for C++
> Message-ID:
> <
> zarafa.6a28354b.2978.553747124a82ac70_at_lvps176-28-11-36.dedicated.hosteurope.
> >
>
> 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_at_[hidden]>
> 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_at_[hidden];
> CC:Rainer Deyke <rainerd_at_[hidden]>;
>
>
> 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_at_[hidden]
> --
> Std-Proposals mailing list
> Std-Proposals_at_[hidden]
> 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_at_[hidden]
> https://lists.isocpp.org/mailman/listinfo.cgi/std-proposals
>
>
> ------------------------------
>
> End of Std-Proposals Digest, Vol 87, Issue 27
> *********************************************
>