Keleusma Research Spike: What a Verified Bound Says About the Code That Actually Runs

Erratum, 2026-08-12

The empirical sections of this article measured code that had never been optimised, and the corrected figures reverse the direction of the finding. The measurement invoked the back end at two optimisation levels over the same intermediate representation. The pass that promotes stack slots into registers is a middle-end pass and the back end does not run it, so both figures described unpromoted code and the difference between them was back-end noise.

Three claims made below are wrong and are corrected in place, with the original figures retained so the change is visible.

The optimiser eliminates the provisioning, and does not relocate it into spill slots. Promoted then lowered, the same 19 modules occupy 5,048 bytes of frame against the 275,432 bytes reported here for unpromoted code, a factor of 54.
The proven bound exceeds the real frame in every module measured, rather than falling short of it. The ratios run from 0.12 to 0.88. The article’s claim that this fails in the dangerous direction is the reverse of what happens.
The provisioning change reported elsewhere as a large saving buys nothing for the shipped pipeline, since promotion had already removed the dead allocations.

This does not rescue the bound. Eight modules agree that it exceeds the frame and no mechanism guarantees that. The two quantities are in different units, count different things and are decided by different agents, so the agreement is coincidence and not construction. The supportable statement is that the bound is empirically conservative on this corpus under the shipped pipeline, which is much weaker than sound.

The structural contribution is unaffected, being the three-part split of the bound set out in Result 1, the literature survey, and the timing result with its stated weakness.

Somebody proves a program can never use more than a certain amount of memory. Then a compiler rewrites that program into a different form before it runs. Does the proof still apply?

The answer, for the system examined here, is that part of it does and part of it was never about the compiled program at all. The measurement that shows which is cheap and quick, which is the uncomfortable part. Nobody had run it.

This article is a case study of a mistake that is easy to make and hard to see. A property is established about one thing, and then claimed about a different thing, with a transformation standing between them that was never asked to preserve the property.

Written as a schema, with $\Phi$ the property, $A$ the thing it was established about and $\mathcal{T}$ the transformation, the mistake is to treat

\[\Phi(A) \quad\Longrightarrow\quad \Phi\bigl(\mathcal{T}(A)\bigr)\]

as though it needed no argument. It always needs one, and the argument is a statement about $\mathcal{T}$ rather than about $\Phi$. Stated that baldly it sounds like nobody would make the mistake. In practice it is everywhere.

A performance budget measured in a staging environment and quoted for production. A power draw calculated from a circuit simulation and quoted for the manufactured board. A safety margin computed for a scale model and quoted for the full-size structure. In each case something in between changed the artefact, and in each case the question is whether it changed the thing being measured.

The specific case here is a programming language whose entire reason to exist is that it refuses any program whose time and memory it cannot bound in advance. That language grew the ability to compile down to machine code. Nobody had checked whether the bounds still mean anything once the code is machine code.

What You Need to Know to Read This

No compiler background is required, and this section is the reason that claim is true. Five ideas carry the whole article.

A program is written once and exists in several forms. The form a person writes, an intermediate form convenient for machines to reason about, and the final form the processor actually executes. The system here proves its guarantees about the middle form and ships the last one.

Bytecode is that middle form. It is a simple, regular instruction set that no physical processor executes directly. A separate program called an interpreter reads it and does what it says. Because bytecode is simple and regular, it is unusually easy to reason about, which is exactly why the guarantees are proven there.

Machine code is the final form, the instructions a physical processor runs. Getting from bytecode to machine code means running an optimising compiler, and an optimising compiler is allowed to rewrite the program almost arbitrarily as long as the program still computes the same answers. It may delete work, duplicate work, reorder work and change where values are stored.

The stack frame is the block of memory a function uses for its own working values. How large it is depends on how many values the compiler decides to keep in memory rather than in registers.

Registers are the processor’s small set of very fast storage locations, and there are only a few dozen. Deciding which values live in registers and which get pushed out into the stack frame is a job called register allocation, and it is the compiler’s decision rather than the programmer’s.

That last point is the whole article. The guarantee is a statement about the middle form. The stack frame is a decision the compiler makes about the final form. They are not the same quantity, and nobody had written down an argument connecting them.

The Uncomfortable Answer

Verifying that the compiler is correct is not enough, and this is the part that surprises people who work on verified compilers for a living. A compiler proved correct guarantees that the program still computes the same answers. It says nothing whatever about how much memory or time the program uses, because resource consumption is not part of what “the same answers” means.

So a compiler can be perfectly, provably correct and still multiply a program’s memory use tenfold. Correctness and resource preservation are different properties, and having the first says nothing about the second.

What Was Measured

The system studied here is Keleusma, whose compiler backend is described in the first and second articles in this series. Three results follow, and the one that looks strong is the weak one.

Half the memory bound does not transfer, and the half that fails is not the half that matters most. The proven bound is a sum of two terms. The arena term transfers exactly, because native code allocates from the same fixed-size arena in the same bytes. The operand-slot term counts a structure native code does not have, and the machine frame it was being compared against is a third quantity nobody bounded. The stack frame is decided by the register allocator. Measured across the whole corpus, the compiler emits 38,601 stack allocations with optimisation switched off and exactly zero after the pipeline that actually ships. Promotion removes them, and the unused ones are dead code that the optimiser deletes outright. Whatever the shipped code spends on memory, the proven number is not measuring it, because the two are decided by different agents counting different things.

The time bound is in better shape and its evidence is much weaker than it looks. The argument that a fast implementation is covered by a slow one’s bound is sound in outline, and it rests on an assumption that is testable. This article tests it. The test passes and the sample has only three distinct magnitudes in it, which makes the pass very nearly meaningless.

The third result is that the two bounds fail in different ways, which decides what work each of them needs. One has to be recomputed from the shipped artefact. The other has to be measured.

The Setting

Keleusma refuses any program whose worst-case running time or worst-case memory use cannot be established before it runs. That refusal is the language’s reason to exist, and a program that survives it carries two numbers.

The first is a worst-case time. It is found by looking at every path the program could take through the bytecode, adding up the cost of each instruction along the way, and keeping the most expensive path. The cost of an instruction comes from a table of measured costs, written $c$ below, calibrated against the interpreter that executes bytecode. Formally, with $\Pi(k)$ the set of paths through a unit of code $k$,

\[T_{\mathrm{vm}}(k) \;=\; \max_{\pi \in \Pi(k)} \; \sum_{\iota \in \pi} c(\iota),\]

The other is a worst-case memory. Bytecode keeps its intermediate values on a stack, and the verifier finds the deepest that stack ever gets. Multiplying that depth by the size of one value, written $w$, and adding a separately computed allocation requirement gives

\[M_{\mathrm{vm}}(k) \;=\; w \cdot \max_{ip} \mathrm{depth}(k, ip) \;+\; \mathrm{arena}(k),\]

Both numbers are functions of the bytecode and of nothing else. That is exactly what makes them provable before the program runs, and it is exactly the property this article puts under strain, because the artefact that ships is not the bytecode.

The path from one to the other runs through LLVM, a widely used compiler toolkit. The backend translates bytecode into LLVM’s own intermediate form, and LLVM turns that into machine code for whichever processor is being targeted.

Notation

Let $P$ denote a program and $\mathcal{B}(P)$ its bytecode. Write

\[T_{\mathrm{vm}}(P), \qquad M_{\mathrm{vm}}(P)\]

for the verifier’s time and memory bounds, and

\[T_{\mathrm{nat}}(P), \qquad M_{\mathrm{nat}}(P)\]

for the true worst case of the native artefact on its target.

Two symbols carry general meanings and two carry specific ones, which is worth stating once. $\Phi$ is any property whatever and $\mathcal{T}$ any transformation, both introduced in the opening. $\mathcal{R}$ is a resource measure, which is the particular kind of property this article is about, and $\mathcal{C}$ is a compiler, which is the particular kind of transformation. Allocation counts are written out as $\mathrm{allocs}$ rather than abbreviated, so that $A$ always means the artefact a property was established about. The claim under examination is the transfer claim,

\[T_{\mathrm{nat}}(P) \le \alpha \, T_{\mathrm{vm}}(P) \quad \text{and} \quad M_{\mathrm{nat}}(P) \le \beta \, M_{\mathrm{vm}}(P)\]

for constants $\alpha, \beta$ that do not depend on $P$. Everything turns on whether such constants exist, and the two halves fail differently.

Result 1: One Term of the Memory Bound Transfers Exactly and the Other Describes Nothing Native

The proven memory bound counts slots on the bytecode’s own value stack. Quoting it in bytes means multiplying by the width of one slot, the $w$ above, which on this target is eight,

\[M_{\mathrm{vm}}^{\text{bytes}}(k) \;=\; 8 \cdot \max_{ip} \mathrm{depth}(k, ip) \;+\; \mathrm{arena}(k).\]

Across the units of code this article measures, which are the entry points of the language’s stream construct, it ranges from 384 to 2,464 bytes, with between 6 and 71 named variables each.

The bound is a sum of two terms, and only one of them is in trouble

That equation has been printed three times in this series and read as a single number. It is not a single number. It is a sum of two quantities that behave completely differently when the program is compiled, and separating them is the difference between a claim that survives challenge and one that does not.

The $\mathrm{arena}(k)$ term transfers exactly, and nothing in this article disturbs it. The language allocates dynamic data from a fixed-size arena with countable bytes, the memory-bound pass sums the size of every allocation, and native code allocates from the same arena in the same bytes. The flat memory model does not change at the compilation boundary. A bound on arena use proven of the bytecode is a bound on arena use of the machine code, with no argument required beyond noticing that the arena is the same object.

The $8 \cdot \max_{ip} \mathrm{depth}$ term is the one with no native counterpart. It counts slots on the interpreter’s operand stack, which is a growable vector inside the virtual machine. Native code has no operand stack. Those values live in registers, and where they do not fit they live wherever the register allocator puts them. Comparing that term to a machine frame compares two different things, which is why the comparison came out as badly as it did.

And the machine frame is a third quantity that the bytecode never described at all. It is not the arena term, it is not the operand-slot term, and it needs a bound of its own computed from the artefact.

This is a narrower claim than the one this article set out to make, and a sturdier one. The original framing was that a proven resource bound does not survive compilation. The supportable version is that one component survives exactly, one is an implementation detail of the interpreter with no counterpart on the machine, and a third quantity exists that was never bounded. Every measurement below is unchanged. What changes is which of the three they are about.

The stack frame contains something else entirely, and the way it is built is worth following.

The backend does not consult the proven depth at all. For every function it reserves a fixed 64 slots, whatever the verifier proved, plus one slot for each named variable. In LLVM’s intermediate form each of those reservations is a stack allocation instruction. The rest of the frame is not the backend’s choice either. It is fixed by the target processor’s calling convention, which dictates which registers a function must preserve for its caller and how the frame must be aligned, and those rules come from documents like System V AMD64 and AAPCS64.

So with optimisation switched off the frame is

\[M_{\mathrm{nat}}^{O_0}(f) \;=\; 8\bigl(64 + \mathrm{locals}(f)\bigr) + \text{callee-saved} + \text{alignment},\]

in which the verifier’s proven depth does not appear anywhere. The number of allocations this predicts is exact rather than approximate, and the measuring instrument asserts it rather than the author eyeballing it,

\[\mathrm{allocs}_{O_0} \;=\; \sum_{f} \bigl(\mathrm{MAX\_STACK} + \mathrm{locals}(f)\bigr) \;=\; 38{,}601,\]

which matches the measured count across all 19 modules with nothing left over. An equation printed in an article is a claim like any other, so this one is wired to a test that fails if the compiler ever stops behaving that way. A unit of code proven to need three slots and one proven to need sixty are given identical space.

And then the optimiser deletes all of it, in the only place the count can see.

\[\mathrm{allocs}_{O_2} \;=\; 0.\]


stack allocations emitted, optimisation level zero	38,601
stack allocations surviving the shipped pipeline	0

A standard optimisation pass notices that these values never need a memory address and moves every one of them into a register. That is where a careless reading stops, and it would be wrong. The registers the pass moves them into are virtual registers, of which the compiler may invent as many as it likes. A real processor has roughly fourteen it can use freely, so an allocator handed 64 live operand slots pushes most of them straight back onto the stack, which is called spilling.

An earlier version of this article claimed the provisioning is relocated into spill slots rather than removed. That claim was wrong, and it was wrong because the measurement behind it never ran the promotion pass. Promoted then lowered, the 19 modules occupy 5,048 bytes of frame in total, against 275,432 bytes unpromoted, a factor of 54. The provisioning really does leave.

The count going to zero is still a fact about the intermediate representation and not about memory, since what the frame ends up holding is decided afterwards by the register allocator and not by the count.

The frame that actually ships is whatever the register allocator decides it cannot keep in registers. That decision is made by the code generator from the number of registers the target processor has, the exact sequence of optimisation passes, the version of LLVM in use, and the code surrounding the function.

\[M_{\mathrm{nat}}^{O_2}(f) \;=\; \mathrm{spill}(f, \text{target}, \text{pipeline}, \text{version})\]

There is no $\beta$. The two quantities are not proportional, not ordered, and not in the same units. $M_{\mathrm{vm}}$ is a property of the program and $M_{\mathrm{nat}}$ is a property of the compiler’s decisions about the program. A bound on the first constrains the second only through an argument nobody has made.

This is the sharpest form of the finding and it is not a defect in the compiler. The translation is doing the ordinary thing that every compiler does. The defect is in the inference, which was never stated explicitly and was therefore never examined.

The frames were measured, and they run the wrong way

The argument above is structural, and a structural argument invites the reply that the numbers might come out fine anyway. They come out differently from the argument, which is worth reporting carefully.

Asking the code generator for an object file carrying a stack-size section, and reading the per-function sizes back out of it, gives the frame each module actually receives. Measured on the code that actually ships, the proven bound exceeds the real frame in every module measured.

Module	proven bound	frame	ratio
`parse`	64	56	0.88
`reconstruct`	128	104	0.81
`analyze`	64	40	0.62
`verify_structural`	64	40	0.62
`verify_typed`	64	40	0.62
`verify_depth`	64	24	0.38
`lexer`	320	40	0.12
`verify_datalayout`	64	8	0.12

Every ratio is below one, and that is the comfortable direction rather than the dangerous one. An artefact provisioned from these proven numbers would be over-provisioned, which wastes memory and keeps its promise.

This does not make the bound sound, and reading it that way would be the same error in the opposite direction. Nothing constructs the agreement. The two quantities are in different units, count different things and are decided by different agents, so eight modules agreeing is a fact about this corpus and not a mechanism. A program with deep expression nesting and few live values could plausibly invert it. The supportable statement is that the bound is empirically conservative on this corpus under the shipped pipeline.

And the ratios do not follow a constant. They range from 0.12 to 0.88 across modules, and three modules sharing a proven bound of 64 receive frames of 56, 40 and 8. A single ratio cannot map one onto the other, so this is not a scaling the project could calibrate once and then rely on.

The same architecture exists in production, and it does not transfer the bound

The closest thing to this system running in production is inside the Linux kernel, and it is worth studying because it faces exactly the same configuration.

Linux lets ordinary programs load small pieces of code into the kernel to filter network packets, trace system behaviour and so on. That is obviously dangerous, so the kernel first verifies the submitted bytecode for termination and resource use, and then compiles it to machine code for speed. A bytecode program is verified, then compiled, and the kernel must not be harmed by the result. The component that does the verifying is called the eBPF verifier.

It does not transfer a memory bound. It fixes one. The stack is capped at a constant, enforced on the bytecode, and the just-in-time compiler is written to respect that cap rather than being trusted to preserve a computed number. The bound is a contract the compiler is built against, not a quantity carried across the boundary.

WebAssembly draws the same line in a different place. Its validation step establishes properties about types and control flow, and deliberately establishes nothing at all about the resource consumption of the compiled result. Whoever embeds a WebAssembly engine is expected to bound resources by their own means while the program runs.

Neither system does what this project has been assuming. That is the most useful thing the survey contributes, and it points at the two available answers. Either fix a bound that the backend is built to respect, or compute one from the artefact that ships. Transferring a bound across the boundary is not among the options anybody deploys.

Result 2: The Time Bound’s Argument Is Sound And Its Evidence Is Thin

The argument for time is an argument from domination, and in plain terms it is this. If running each operation as machine code is never slower than running it in the interpreter, then whatever bound covers the interpreter also covers the machine code. The slow thing’s limit covers the fast thing.

Written out it needs slightly more. It needs a way of saying which machine instructions came from which bytecode instruction, written $\phi$ below, and it needs each bytecode instruction’s real machine cost to stay inside its modelled cost,

\[\forall \iota \in \mathcal{B}(P): \quad \sum_{\iota' \in \phi^{-1}(\iota)} t_{\mathrm{nat}}(\iota') \;\le\; \kappa \, c(\iota),\]

Summing that inequality along the most expensive path gives the conclusion,

\[T_{\mathrm{nat}}(P) \;=\; \sum_{\iota \in \pi^{*}} \; \sum_{\iota' \in \phi^{-1}(\iota)} t_{\mathrm{nat}}(\iota') \;\le\; \kappa \sum_{\iota \in \pi^{*}} c(\iota) \;=\; \kappa \, T_{\mathrm{vm}}(P),\]

with $\pi^{*}$ the worst path. The constant that emerges is the one the transfer claim needed, so $\alpha$ and $\kappa$ are the same number arrived at from two directions, and the article uses $\alpha$ for the claim and $\kappa$ for the per-instruction premise that would establish it.

The premise is an empirical claim and $\phi$ is the fragile part of it. An optimising compiler routinely copies a function’s body into its callers, combines several operations into one wide instruction, deletes work whose result is never used, and shares a computation between two places that both needed it. Every one of those destroys the correspondence $\phi$ presumes. After optimisation there may be no machine instruction attributable to a given bytecode instruction at all, or one machine instruction attributable to a dozen.

The argument survives only if the total inequality holds without the correspondence holding, which is a weaker thing to know and a harder thing to establish. It also requires that no operation becomes slower as machine code, which a safety check, a call back into the runtime, or a memory layout unfriendly to the processor’s cache could each violate.

The ordering is testable without any timing equipment. If the bytecode bound is standing in for machine cost, then a unit of code with a larger bound should not produce a smaller body of machine instructions.

Define an inversion as a pair of code units that the two measures order oppositely,

\[\mathrm{inv} = \bigl|\{(a,b) : T_{\mathrm{vm}}(a) < T_{\mathrm{vm}}(b) \;\wedge\; S(a) > S(b)\}\bigr|\]

with $S$ the number of machine instructions emitted. A single inversion falsifies the proxy. Only pairs that the bound actually orders can contribute, so the denominator is not the number of pairs but

\[N_{\prec} = \bigl|\{(a,b) : T_{\mathrm{vm}}(a) < T_{\mathrm{vm}}(b)\}\bigr| \;\le\; \binom{n}{2},\]

and a sample concentrated on a few distinct magnitudes drives $N_{\prec}$ far below $\binom{n}{2}$. The inversion count is the numerator of Kendall’s rank correlation, so the result can equivalently be read as

\[\tau \;=\; 1 - \frac{2\,\mathrm{inv}}{N_{\prec}},\]

and $\tau = 1$ on a sample of three magnitudes is a much smaller statement than $\tau = 1$ on a spread.

The measurement over every entry point that reaches machine code is as follows.

stream chunks with both figures : 9
comparable pairs                : 36
INVERSIONS                      : 0

Why that zero is much weaker than it appears

Seven of the nine units of code have identical figures, at $T_{\mathrm{vm}} = 14$ and $S = 72$. The sample contains exactly three distinct magnitudes.

$T_{\mathrm{vm}}$	$S$	code units
14	72	7
45	153	1
164	1,143	1

The pair counts follow from that table and are worth doing, because they turn the phrase “barely a test” into a number. With $n$ units of code falling into groups of equal bound of sizes $n_{g}$, the pairs the bound strictly orders are the total minus the ties within each group,

\[N_{\prec} \;=\; \binom{n}{2} - \sum_{g} \binom{n_{g}}{2} \;=\; \binom{9}{2} - \binom{7}{2} \;=\; 36 - 21 \;=\; 15.\]

The remaining 21 pairs are ties and cannot invert by construction. So the resolution of the test, meaning the fraction of the comparisons the sample is capable of making, is

\[\frac{N_{\prec}}{\binom{n}{2}} \;=\; \frac{15}{36} \;=\; 41.7 \text{ percent},\]

and those fifteen comparisons are drawn from only three separated size classes. The headline zero is a zero over fifteen comparisons among three values, which is barely a test at all.

Reporting it as “0 of 36” would be the same error this series has now documented three times, being a figure that is arithmetically correct and answers a smaller question than it appears to. The honest statement is that no inversion was found and that the sample lacks the resolution to find one.

Result 3: The Two Bounds Fail Differently, Which Matters For What To Do

The memory bound is broken in kind. No constant relates the two quantities, because one of them is not a property of the program at all. Fixing it means computing a memory bound from the shipped artefact and transferring nothing to it.

The time bound is unbroken in kind and unevidenced in degree. The domination argument may well hold. It rests on an assumption that has not been tested at any useful resolution, and on a unit conversion $\alpha$ that has never been calibrated. The project’s own architecture notes that the interpreter cost model does not translate and that per-platform calibration is needed, which is the same gap stated from the other side.

Writing $\mathcal{R}$ for a resource measure, and taking the memory case to mean the machine frame against the operand-slot term and not against the arena term, the two gaps differ in kind. Neither is a proven relation and they are unproven for different reasons. The memory case holds on this corpus with $\beta = 1$ and nothing establishes it, since no step of the compilation is required to maintain it. The timing case has an argument behind it and an unmeasured constant,

\[\beta = 1 \text{ observed, unproven} : \mathcal{R}^{\mathrm{frame}}_{\mathrm{nat}} \le \beta\, \mathcal{R}^{\mathrm{slots}}_{\mathrm{vm}}, \qquad \exists \alpha \text{ (uncalibrated)} : \mathcal{R}^{\mathrm{time}}_{\mathrm{nat}} \le \alpha\, \mathcal{R}^{\mathrm{time}}_{\mathrm{vm}},\]

which call for different work, being an argument in the first case and measurement in the second.

A project that shipped native artefacts today would be shipping part of the language’s central promise unsupported, and would not be lying, because the promise is about the bytecode and the bytecode still carries it. That is precisely the kind of true statement that misleads. The arena half of the promise is genuinely kept. It is the machine stack that has no guarantee behind it, and a reader told only that the memory promise holds would have no way to tell which half was meant.

Threats to Validity

The corpus is small and the part of it this article can measure is smaller. Nine units of code and three widely separated sizes. Every claim about the time proxy is bounded by that.

The instruction count is a proxy for a proxy. Native instruction count bounds execution time only under a bound on cycles per instruction,

\[T_{\mathrm{nat}}(f) \;\le\; \mathrm{CPI}_{\max} \cdot S(f),\]

and $\mathrm{CPI}_{\max}$ is exactly what cache misses, branch misprediction and memory stalls make unbounded without a target model. That is the assumption the timing-analysis literature exists to refuse. Instruction count ignores latency, cache behaviour, branch prediction and superscalar issue. A monotone relationship between bound and instruction count is weak evidence for a monotone relationship between bound and time, and no evidence at all about magnitude.

The allocation count is at the intermediate representation, and the frame was measured separately. An earlier version of this article deferred the frame measurement and gave a bad reason for doing so, namely that the per-function frame sizes live in a named section of the object file, in the sense the ELF generic binary interface gives that word and closely related to the metadata LLVM stack maps describe, which the Mach-O development host does not emit. That reasoning confused the host with the target. A compiler cross-targets by construction, so asking llc for an ELF object with a stack-size section and reading it back with llvm-readobj produces the number on any host. The equivalent capability exists in other toolchains as GCC’s -fstack-usage and Clang’s stack-size section.

The measurement is easy to get wrong and this article got it wrong once. The first attempt invoked the back end at two optimisation levels over the same intermediate representation, which never runs the promotion pass at all, so it compared unpromoted code with unpromoted code and read the difference as the effect of optimisation. The corrected measurement promotes first and then lowers, which is what the shipped pipeline does.

No constant factor relates the bound to the frame, which is the sharper point and survives the correction. The ratios run from 0.12 to 0.88, and three modules sharing a proven bound of 64 receive frames of 56, 40 and 8. A single ratio cannot map one onto the other, so the relationship is not a scaling the project could calibrate and then apply. It is the absence of a relationship.

The author wrote both the compiler being measured and the instrument measuring it. The mitigation offered is that the finding is unfavourable to the author’s own prior work and would have been more comfortable suppressed.

Pattern Extraction

Verifying the transformation does not preserve the property. Writing $\mathcal{C}$ for a formally verified compiler, which is one particular transformation $\mathcal{T}$ of the kind this article opened with, what such a compiler proves is semantic equivalence,

\[\llbracket \mathcal{C}(P) \rrbracket \;=\; \llbracket P \rrbracket,\]

while the property wanted here is a separate inequality over a resource measure $\mathcal{R}$,

\[\mathcal{R}\bigl(\mathcal{C}(P)\bigr) \;\le\; \beta \, \mathcal{R}(P).\]

Neither implies the other. Semantic equivalence quantifies over observable behaviour, and resource use is not observable behaviour in any of these semantics, so a transformation may multiply the stack tenfold and remain perfectly correct. Correctness and resource preservation are independent properties, and a project that has the first frequently believes it has the second.

A property proven of a model constrains the artefact only through a stated argument. The argument here was never written down, which is why it was never checked. Where a claim crosses a representation boundary, the crossing deserves its own explicit statement, and the absence of one is not evidence that it is trivial.

When two measures disagree in kind, no amount of correlation rescues them. The memory bound and the native frame are not weakly correlated. They measure different things, in different units, decided by different agents. Looking for a constant of proportionality between them is a category error dressed as an empirical question.

A zero result inherits the resolution of its sample. Zero inversions over three size classes is not the same claim as zero inversions over a spread, and the two are reported identically by any instrument that prints a count. Report the resolution beside the result or the result will be read as stronger than it is.

The Contemporary Literature

Five literatures bear on whether a resource bound survives translation, and one of them has solved the problem this article discovers. The others each hold a piece. What follows surveys them and marks where the present project sits, which is behind all five.

Resource analysis is a field, and it works on the artefact you intend to run

The static prediction of time and space from program text is mature. Hofmann and Jost 2003 give a type system inferring heap-space bounds for first-order functional programs, and Hoffmann, Aehlig and Hofmann 2012 extend amortised analysis to multivariate bounds. Danielsson 2008 shows the same discipline embedded lightweightly in a dependently typed language.

Directly on the present configuration, Albert and others 2007 perform cost analysis of Java bytecode, which is exactly the artefact Keleusma’s verifier analyses. That work is careful about what its bounds mean, and it means them about the bytecode, executed by a virtual machine. It does not claim them for a just-in-time compiled result.

The pattern across the field is that the analysis targets the representation that will run. Nobody in this literature proves a bound on one representation and ships another, which is what makes the present project’s assumption unusual rather than merely unverified.

96 contemporary records join the works named above. The field analyses the representation it expects to run, which is the discipline this project did not follow.

Cost-preserving compilation is the exact problem, and it has a research programme

The CerCo project is the closest existing work to what this article says is needed. Amadio and Régis-Gianas 2012 and Ayache, Amadio and Régis-Gianas 2012 build a certified C compiler that does not transfer a cost bound but lifts a cost model upward, so that the compiler emits cost annotations on the source, justified by the assembly it actually produced, so the bound the programmer reasons about is derived from the artefact and never asserted about a model of it.

That inversion is the whole idea, and it is worth writing the two directions side by side. The move this project had been assuming pushes a bound down onto the artefact, while the move CerCo makes computes it from the artefact and reports it upward,

\[\underbrace{\mathcal{R}(A) \;\longrightarrow\; \mathcal{R}\bigl(\mathcal{T}(A)\bigr)}_{\text{transfer, which needs an argument nobody supplied}} \qquad\text{against}\qquad \underbrace{\mathcal{R}\bigl(\mathcal{T}(A)\bigr) \;\longrightarrow\; \text{annotation on } A}_{\text{lifting, which needs only the compiler's own knowledge}}\]

The compiler is the thing that knows what the code became, so it is the right component to report cost, and a bound computed before compilation is computed by the component with the least information.

Carbonneaux, Hoffmann, Ramananandro and Shao 2014 do the memory half and do it end to end, giving verified stack-space bounds for C programs proven all the way down to the assembly, with the compiler’s own frame decisions inside the proof. Carbonneaux, Hoffmann and Shao 2015 generalise to compositional certified resource bounds. This is the literature that already contains the answer to Result 1, and its existence means the memory problem here is not open research but unimplemented practice.

Only 4 contemporary records carry this vocabulary at all. That is the smallest cluster in the survey by a wide margin, and the smallness is itself evidence, because the same harvest returned hundreds of records on optimisation and on timing.

Worst-case execution time analysis will not accept an operation count

This is the field that predicts how long a program can possibly take on a particular processor, and it is the field a native timing claim would have to satisfy. The standard survey, Wilhelm and others 2008, sets the requirement plainly. A sound timing analysis needs a model of the target processor’s pipeline and memory hierarchy. Heckmann and others 2003 make the sharper point that processor architecture determines what any tool can achieve, and Puschner and Burns 2000 give the earlier review of the same ground.

The techniques are specific and not one of them is a count of operations. Li and Malik 1995 turn the search for the most expensive path into an optimisation problem that a solver can answer. Ferdinand and Wilhelm predict cache behaviour precisely enough for such a search to consume. And Reineke and others 2007 show that the processor’s cache replacement policy itself determines whether prediction is possible at all, so the same program on the same instruction set can be analysable or not depending on a hardware choice nobody in the software made.

Kirner and Puschner 2008 enumerate the obstacles, and the one that matters here is stated plainly in that literature. The compiler is itself an obstacle, because optimisation destroys the correspondence between the structure a person or a verifier reasons about and the sequence of instructions that actually executes. Falk and Lokuciejewski 2010 respond by building a compiler that optimises for worst-case time, which is the constructive version of the same observation.

This is the literature that refuses the second half of the transfer claim. An operation count calibrated against an interpreter is not an input to any of these methods.

This cluster holds 460 contemporary records, more than four times the resource-analysis cluster. The disparity reflects that timing is the bound industry is required to certify while memory is mostly left to convention.

Translation validation is the technique for a compiler you cannot change

The idea is to stop trying to prove the compiler correct once and for all, and instead check each individual run. Pnueli, Siegel and Singerman 1998 introduce it and Necula 2000 applies it to an optimising compiler. Rather than proving the compiler correct, prove that this particular output is equivalent to this particular input. Sewell and others 2013 carry it to a production operating-system kernel by proving the binary refines the C.

That fits the present problem well, because the property here is per-artefact and fragile. A resource bound depends on decisions an optimiser makes for reasons specific to one program, which is precisely the situation translation validation was invented for, and it is much cheaper than verifying an entire backend.

A further 410 contemporary records develop the technique. It checks one compilation and not one compiler, which is why it needs no cooperation from LLVM and why it would have to run on every build.

Verified compilation preserves semantics and says nothing about cost

A verified compiler is one whose correctness has itself been proven mathematically, which is a formidable achievement and a narrower one than it sounds. Leroy 2009 and Leroy 2009b establish CompCert, the best known example. Blazy and Leroy 2008 give the model of memory that underpins it, and Kumar and others 2014 establish CakeML on the same principle.

None of these claims resource preservation and none is careless about saying so. The theorems are about observable behaviour. A project that reads “verified compiler” as “my bounds survive” has imported a guarantee that was never offered, which is the misreading Result 1 makes concrete rather than a strawman.

Necula 1997 gives the shape the eventual answer probably takes, in which the artefact carries machine-checkable evidence about itself, and that is what this project’s plan to export a memory requirement as a linker symbol already gestures at without yet having anything sound to put in it.

100 contemporary records extend this work, and not one of their titles claims resource preservation. The cluster is roughly a fifth the size of the timing cluster, which is worth noticing, since verifying a compiler is the harder achievement and the smaller literature.

Bounded execution in deployed systems, which is where the practice is

Regehr, Reid and Webb 2005 eliminate stack overflow by abstract interpretation of machine code, and Brylow, Damgaard and Palsberg 2001 check interrupt-driven assembly for stack bounds directly. Both make the same choice, which is to analyse the thing that executes.

For the bytecode-then-native configuration specifically, Gershuni and others 2019 give a static analysis for untrusted Linux kernel extensions, which is the research counterpart of the eBPF verifier discussed above. That system fixes a stack cap rather than transferring a computed bound, and the commercial tools StackAnalyzer and aiT recompute from the binary against a target model, because ISO 26262 and its siblings ask for evidence about the executable.

Sandboxed and isolated execution accounts for 295 contemporary records.

The mechanics the five literatures rest on

The five literatures above are the ones the article’s argument engages. They sit on a body of work about how a compiler actually moves and deletes things, and that work is a different literature from the technologies above it. The distinction matters here because Result 1 turns on a specific mechanical fact, being that the optimiser promotes stack allocations into registers, and no paper about verified compilation discusses that decision while a great many papers about register allocation do.

Code generation and optimisation itself account for 439 contemporary records.

8 concern the calling convention and the binary interface directly, which is a strikingly small number for a subject every compiler must settle.

Static analysis supplies the technique the other five borrow

Abstract interpretation is the machinery underneath most of what the preceding sections describe. The stack analyses, the cache analyses and the resource analyses are all instances of it, and the 604 records here are the general method rather than any one application of it.

The bytecode layer is where this project’s bound is actually proven

Keleusma’s verifier reasons about bytecode, so the literature on what a bytecode-executing machine guarantees is directly load-bearing for Result 1. 345 contemporary records concern bytecode, virtual machines and just-in-time compilation.

Stack and memory bounds computed on the artefact

The 155 records here compute a bound on the thing that runs instead of on a model of it, which is the move this article concludes the project must make.

Proof-carrying code and certified artefacts

An artefact carrying machine-checkable evidence about itself is the subject of 7 contemporary records. This is the second smallest of the named clusters, after cost-preserving compilation, and it is the shape the article’s conclusion suggests the eventual answer takes.

Types and semantics decide whether the question is even askable

Type systems and formal semantics account for 330 records. They belong here because a resource bound is a property of a program, and what a type system can express determines whether such a property can be stated in the source at all.

Real-time and certification, which is who consumes the evidence

814 contemporary records make this the largest of the named clusters, and its size is a fact about who pays for this work. Resource bounds are not an academic curiosity. They are a certification requirement in avionics and automotive software, and the literature is correspondingly industrial.

The general pattern, which is this article’s own contribution

160 records treat the preservation of a property across a transformation in its general form, stated for properties other than the resource bounds this article is about.

The surrounding literature

2,255 admitted records share the article’s vocabulary without addressing its question. They are listed and not discarded, because the selection that produced them is reported in full, and a survey that presents only the records supporting its thesis has selected twice, once by query and once by judgement, while reporting one selection.

The historical layer

The clusters above are drawn from work published in 2015 or later, which is the survey’s contemporary window. The older records are listed here in one place instead of being distributed through the sections above, because for this subject the pre-2015 work is mostly the foundation the contemporary work cites. There are 5,945 of them, and for a field this young that is a large fraction of the whole.

What the survey shows

The composition this project assumed does not appear anywhere. Resource analysis targets the representation that runs. Cost-preserving compilation lifts a model up from the artefact rather than pushing a bound down onto it. Timing analysis demands a target model. Verified compilation deliberately scopes itself to semantics. Deployed systems either fix a cap or recompute.

Five literatures, and not one transfers a resource bound across a compilation boundary. That is a stronger statement than saying this article found no support, and it is the survey’s actual contribution. The assumption is not merely unproven here. It is contrary to the practice of every field that has addressed the problem.

The harvested majority establishes coverage and not agreement. The survey lists 11,096 references, of which 28 were selected because a step of the argument depends on them and were read, and 11,068 were harvested by query across fifteen clusters and were not. A reader looking for the works that carry the argument should read the 28, which are named in the prose above. A reader checking whether the survey was assembled to flatter its conclusion should note that the queries were fixed before any record was seen, that every admitted record is listed including the 2,255 that are merely adjacent, and that the selection procedure is reported below with the count it discarded.

The cluster sizes are themselves a result, and the smallest one is the loudest. Cost-preserving compilation, which is the exact problem this article discovers, holds 4 contemporary records against 814 for real-time certification and 439 for compiler optimisation. The field that would solve the problem is more than two orders of magnitude smaller than the field that needs it solved.

The corollary is that Result 1 is not a research problem. Carbonneaux and others 2014 did end-to-end verified stack bounds a decade ago. What this project has is an unimplemented known technique, which is a far better position than an open question and a far worse one than the assumption it replaces.

The Source Base

The backend takes the compiler’s own in-memory representation of a module and emits LLVM’s intermediate form through the inkwell Rust bindings. The two bounds are computed by the verifier from the same bytecode.

The measuring instrument compiles the whole corpus and translates each module twice, once with optimisation switched off and once through the pipeline that actually ships, counting stack allocations in each. It then pairs every entry point’s proven bound against the number of machine instructions emitted for it. It reports and does not assert, because the distribution is a fact about this corpus and not a property the code should be held to. The whole run takes about nine seconds, which is the figure behind the claim in the opening that nobody had looked rather than that looking was hard.

How the harvested survey was assembled

The 28 hand-selected research references were chosen because a step of the argument depends on them, and each was read. The 11,068 harvested references were not chosen that way and were not read individually. Stating that plainly is the point of this subsection, because a list of several thousand citations otherwise implies a reading it does not represent. What the harvested list supports is a claim about coverage, being that the survey did not select for agreement with its conclusion, since the queries were fixed before any record was seen. What it does not support is any claim about the content of an individual harvested record beyond its title, authors, year and venue as the registry holds them.

The harvest issued 119 keyword queries against the Crossref registry across fifteen topic clusters, in seven rounds separating journal articles, conference proceedings, book chapters and defence technical reports, and separating work published through 2014 from work published since. It retrieved 60,091 records. Each was kept only if its title carried a subject anchor, meaning a term specific to computing rather than one shared with every discipline that publishes. That test discarded 48,487 of them.

The count that survives is smaller again, and the arithmetic is worth stating instead of leaving to be noticed. Of the 11,604 records the anchor test admitted, 488 were duplicates holding the same title and year under two identifiers, 21 carried a contraction or a doubled word in a verbatim title that this corpus cannot reproduce in link text, and 27 duplicated a work already cited by hand. 11,068 therefore reach the reference list. That last figure is a small piece of corroboration for the survey, because 27 of the 28 works chosen by hand before the harvest ran were independently returned by it.

The anchor filter is the step most likely to be wrong, and reading its output found five defects in it.

The word cost was admitted unqualified, so a Handbook of Army Cost Analysis Terms, a refuse-derived-fuel cost model and a cost-effectiveness compilation for heart conditions all reached the kept set. Cost analysis and cost model are complete phrases in accounting and defence procurement rather than words merely shared with them, and the harvest’s own notes had warned that resource could not be filtered while failing to apply the same reasoning to the worse case.

A qualifier written as a lookahead only sees what follows the anchor. Crafting a Java virtual machine in silicon was refused because the qualifier java was required to appear after the phrase virtual machine rather than anywhere in the title. Rewriting every qualifier to be order-free recovered 303 records. The defect is silent, because a filter that refuses a record returns a smaller corpus rather than an error, which is the failure mode this corpus keeps paying for.

A literal space in a multi-word anchor refuses the hyphenated spelling, so A Novel Common-Subexpression-Elimination Method was refused by an anchor reading common subexpression.

Registry furniture is on-subject by every anchor while not being a work at all. Session details: Memory safety is a proceedings heading. 190 such records were refused by title shape and not by subject, since narrowing the subject test to exclude them would also exclude real papers on memory safety.

And the largest defect was a venue filter inherited from a different discipline, which then took two corrections rather than one. The first rounds requested journal articles only, which is the right choice for aerospace and the wrong one for computer science, whose primary venue is the conference proceeding. Those rounds returned 19,169 records and not one paper from the CerCo project, which is the research programme this article names as the closest existing work to its own problem.

Adding conference proceedings more than doubled the corpus and still returned no CerCo paper. The reason is that Springer deposits its Lecture Notes in Computer Science volumes as book chapters rather than as proceedings articles, so an LNCS proceedings paper is typed as a chapter of a book, and both CerCo papers cited by hand above are deposited that way. A third pair of rounds was needed.

The general lesson is that a venue filter encodes a guess about how a publisher deposits metadata, and that guess cannot be checked against the size of the corpus it returns, because each of the first two attempts returned a corpus that was large and plausible and missing the same thing. It was found only by probing for a named project that the survey was known in advance to require.

Seventeen homonym families were recorded during this sweep and are held in the repository’s accumulated store and not in this article, so the next sweep inherits them. A homonym family is a phrase that means one thing in computing and another elsewhere, and each of these was found by reading a sample and not by anticipating it. They are, in the order they were found,

Stack Overflow the website against the stack overflow condition.
Circuit timing signoff, and statistical static timing analysis in particular, against software timing analysis.
Just-in-time manufacturing against just-in-time compilation.
Just-in-time instructional delivery against just-in-time compilation.
Just-in-time defect prediction, meaning prediction at commit time, against just-in-time compilation.
The compiler as a metaphor in language teaching.
Formal semantics in linguistics and philosophy of language against programming-language semantics.
The peephole as an optical and critical-theory term against the peephole optimisation.
Semantic preservation in natural language generation against semantic preservation in compilation.
The calendar timing anomaly in finance against the processor timing anomaly.
The human interpreter, and the sign language interpreter most of all, against the program interpreter.
Java the island, and pre-stack seismic imaging, against Java the language and the call stack.
Static analysis in structural and geotechnical engineering against static analysis of program text.
Vector and set optimisation in mathematical programming against vectorisation in a compiler.
The cloud virtual machine against the language virtual machine.
Web and content-delivery cache replacement against processor cache replacement.
Software cost estimation against the compiler cost model.

The count of families is not a measure of how clean the survey is. It is a measure of how many times reading a sample of thirty found something a previous reading had missed, and the last sample still found one. A sweep that reported no families would be reporting that nobody read it.

Epistemic State

Measured, and reproducible from the instrument. Across 19 lowerable modules the generator emits 38,601 stack allocations at optimisation level zero and 0 after the shipped pipeline. The fixed operand provisioning is 64 slots per function. Nine stream entry points carry both a proven bound and an emitted instruction count, and they span three distinct magnitudes, being $(14, 72)$, $(45, 153)$ and $(164, 1143)$. Over 36 pairs, of which 15 are strictly ordered, there are 0 inversions. Measured memory bounds for stream entry points range from 384 to 2,464 bytes with 6 to 71 locals. Native frame sizes were read from a stack-size section in a cross-targeted object file, and the bound proven of the bytecode exceeds every module’s frame in the conservative direction, the ratios running from 0.12 to 0.88 across the eight modules measured. Lowered for x86_64-unknown-linux-gnu the 19 modules occupy 5,048 bytes of frame in total when promoted before lowering, against 275,432 bytes when they are not, a factor of 54. An earlier version of this article reported the unpromoted figures as though they were the shipped ones, and the erratum at the head of the article records what changed.

Derived, and checkable from the definitions. That the proven operand depth does not appear in the unoptimised frame expression, since the provisioning is a constant. That a tie cannot be an inversion, so the inversion count is taken over 15 pairs rather than 36. That semantic preservation does not entail resource preservation, since a transformation may change spilling while preserving observable behaviour.

Assumed, and marked as such. That instruction count is monotone in execution time. It is not, and the article’s second result should be read as evidence about code size that is merely suggestive where time is concerned. The instrument’s nine-second runtime is the author’s report rather than an independently timed figure, and nothing in the argument depends on it.

Verified, and this time the instrument found real defects. The bibliography was submitted with 27 research identifiers, every one of which was resolved against the registry and compared to the work it is cited as. Four were wrong, an error rate of 14.8 percent, and none of the four was a false positive of the checking method. A twenty-eighth reference was added during editing and resolves correctly, so the article carries 28 hand-selected references while the error rate above describes the 27 that were submitted. The harvested references were not checked this way and are not claimed to be, since they come from the registry and not from anybody’s memory, which is the failure mode that produced all four errors. One digit was transposed, sending Static checking of interrupt-driven software to a different paper in the same proceedings. One cited the wrong volume and year for the Amadio and Régis-Gianas cost-annotation work. One attributed a 2003 paper by Heckmann and others to Wilhelm and others in 2009, wrong in author, year and identifier together. One resolved to a genuine and relevant paper that was not the one named, sending a citation of Theiling on separated cache and path analyses to Ferdinand and Wilhelm on cache behaviour prediction, and that entry was relabelled to the work the identifier actually designates rather than dropped.

This is a materially worse rate than the previous article in this series, which resolved 35 of 35, and the difference is instructive rather than random. This bibliography is larger, older, and drawn from proceedings series where adjacent identifiers differ by a single digit. The error rate rises with the volume supplied from memory, which is an argument for searching the registry by title and never recalling an identifier, and all four corrections here were obtained that way.

Harvested rather than read. 11,068 of the 11,096 research references were retrieved by keyword query and are listed on the strength of their titles, authors, years and venues as the registry holds them. Nothing in the argument rests on any one of them. The cluster sizes are the only quantitative use made of them, and the coverage claim they support is stated in full in the Source Base. The residual contamination rate is not zero. Four independent samples of thirty were read during assembly, each one found contaminants the previous round had not, and the last found roughly one in thirty. A survey that reported a clean sample would be reporting that it stopped looking.

Surveyed rather than measured. That the eBPF verifier fixes a stack cap rather than transferring a computed one, and that WebAssembly validation establishes nothing about the compiled result’s resource use, are readings of those specifications and not experiments. They are load-bearing for the conclusion’s recommendation and a reader who doubts them should check the cited documents rather than trust the summary.

What this article does not establish. The value of $\alpha$, which requires per-platform calibration. Whether the domination premise holds for every operation, which was argued and not measured. Whether any inversion exists at higher resolution.

The strongest claim the evidence supports is that the operand-slot term of the memory bound does not constrain the native frame, because the quantity it measures is absent from the frame’s determination and the provisioning it might have constrained leaves the intermediate form entirely and is deleted rather than carried into the frame. The claim does not extend to the arena term, which transfers exactly and is not in question, and the difference between those two statements is the difference between a result and an overreach. The weakest link is the timing result, whose zero inversions rest on three distinct magnitudes and should not be cited as support for the domination argument.

Out of Scope

The design of a native memory analysis, which is the obvious follow-up and is a separate subject. Per-platform timing calibration. The choice of calling convention, treated in the previous article. Register allocation and spilling as techniques. Any claim about execution time, which would require a timing rig this article does not have.

Conclusion

A language that refuses programs it cannot bound had built a compiler that discards the bound. Not through a defect, and not through carelessness in the translation, but because the inference from a verified model to a generated artefact was never written down and was therefore never examined. It reads as obvious until the moment someone counts, and then it reads as two quantities in different units decided by different agents.

The time bound may well transfer. The argument for it is reasonable, the measurement here is consistent with it, and the measurement is far too coarse to be called support.

The memory bound splits. Its arena term transfers exactly, because the machine code allocates from the same arena in the same bytes. Its operand-slot term does not transfer and could not, because it counts a structure that native code does not have, and no constant of proportionality is available between that term and the machine frame, three modules with an identical proven bound receiving three different frames. The frame is a third quantity, and the honest description is not that a bound was lost but that one was never computed.

The deployed systems point at what to do instead, and neither of them transfers. The eBPF verifier fixes a stack cap on the bytecode and builds its just-in-time compiler to respect it. The static-analysis tools the certification regimes consume recompute the property on the shipped binary against a target model.

Written against the same schema the article opened with, the two shapes are

\[\text{fix a contract:} \quad \Phi_{0} \text{ chosen in advance, and } \mathcal{T} \text{ built so that } \Phi_{0}\bigl(\mathcal{T}(A)\bigr) \text{ holds by construction,}\] \[\text{recompute:} \quad \Phi\bigl(\mathcal{T}(A)\bigr) \text{ measured on the artefact itself, with } \Phi(A) \text{ playing no part,}\]

and the third shape, the one this project had been assuming, is

\[\text{transfer:} \quad \Phi(A) \text{ proven, } \Phi\bigl(\mathcal{T}(A)\bigr) \text{ claimed, and nothing said about } \mathcal{T}.\]

Nobody deploys the third.

For this project the two shapes divide the work cleanly, which is the practical result. Dynamic data should be allocated from the arena, where the bound already transfers and no new argument is needed. The machine frame should be bounded separately and computed from the artefact, by asking the code generator for the frame sizes it chose. Neither of those is research. The first is a rule about where data lives and the second is a build step, and together they replace a bound that was assumed to carry with two that are each established where they are used.

The lesson generalises past compilers. Wherever a property is proven of a model and claimed for an artefact, the transformation between them is a premise. It is usually invisible, usually unstated, and occasionally the whole argument.