Prove it, then skip it

The last experiment still made me write the clever part by hand. In The programming before programming, a small planner collapsed 256 configurations into eight useful specialization keys. That saved repeated compilation, but something still had to run the planner to discover the key.

I wanted the compiler to discover when it could skip that step too. After a first execution, could it prove that a whole range of inputs would produce the same plan? Then, after I edited the planner, could it check that the proof still held instead of starting over for every input?

I built that version. On the shared-plan workload below, 2,048 concrete planner executions became eight. After an equivalent source edit, they became zero, with eight region checks instead. The useful surprise was that the proof could cover configurations I had never executed.

There is a correctness argument and a runnable experiment here. The literature search also found close relatives, including checked proof templates in neural-network verification. I do not have evidence for a first-ever technique. I do have a working extension of the previous article, and enough detail to separate what it accomplishes from what the word “breakthrough” would otherwise conceal.

A cache entry for inputs I have not seen#

The companion implements a small staging language in Python. Its programs are pure, acyclic integer instruction graphs. A program takes a configuration and produces a tuple of constants. A separate lowering function uses that tuple to emit a C++ kernel body.

The workload has four inputs: width, salt, an enabled flag, and a label. Width chooses a bucket. Salt matters only when enabled. The label must satisfy the input schema but does not affect the generated arithmetic. This is the equivalent reference calculation; the loop becomes a finite graph in the staging language.

# Mathematical reference for the generated staging program.# The real compiler interprets an acyclic instruction graph.bucket = width // 64effective_salt = salt if enabled else 0seed = 17 + bucketplan = []for _ in range(64):    seed = (seed * 1664525 + 1013904223 + effective_salt) % 65536    plan.append(seed)

Each of the 64 resulting constants appears in the emitted kernel. There is no sleep, artificial busy loop, or unused result inserted to make evaluation look expensive. It is still a synthetic arithmetic workload, chosen because its behavior and sharing opportunities are easy to check.

Now compile one configuration and then a different one. The following is executable code from the companion, not a proposed API:

# Run inside examples/prove-it-then-skip-it.from regions import Compilerfrom experiment import workloadcompiler = Compiler(workload(), mode="region")a = compiler.compile((129, 99, 0, 1))b = compiler.compile((150, 77, 0, 2))assert a is bassert compiler.stats["evaluations"] == 1

The first request discovers and checks the following region. Width can change anywhere inside the interval. Salt and label can vary across their valid ranges. Enabled remains zero.

width:    [128, 191]salt:     [0, 65535]enabled:  [0, 0]label:    [0, 1000000]# Every valid tuple in this box has the same complete plan.# The checker establishes that claim; sampling does not.

The second request passes ordinary input validation and four interval-membership tests. It does not execute the planner, construct the plan tuple again, or regenerate the body. The returned artifact is the same immutable pair of plan and generated source.

A full-input cache would miss because the tuples differ. A result-keyed cache would share the body, but only after computing the result. The region lets this implementation stop earlier. That is the operational distinction I wanted to test.

Work backward to suggest a region#

After a concrete evaluation, the producer starts with a demand: every output must retain its observed value. It walks the graph backward, translating output demands into constraints on operands.

Some inverse rules are very cheap. A demand on addition by a known constant shifts the interval. Multiplication by a constant adjusts its endpoints. Integer division by a positive constant turns one demanded quotient into a range of permitted dividends.

# For integer x and positive d:lo <= x // d <= hi# Exactly when:lo * d <= x <= (hi + 1) * d - 1# Demanding x // 64 == 2 therefore gives:128 <= x <= 191

Other cases deliberately lose precision. When addition involves two independently varying operands, this producer freezes both to their observed values instead of solving a relationship between them. Remainder stays within one observed quotient cell. These choices can make a region smaller than necessary, but they keep proposal construction to one backward pass.

Selection has a useful extra case. If both arms can be constrained to the required output, the producer does not need to preserve the comparison outcome. With salt equal to zero, enabled may vary between zero and one: both branches supply zero. A test changes that flag and still obtains a hit. This goes beyond replaying exactly the same branch decisions.

I did not make the producer responsible for convincing me that any of this was safe. It proposes a box. A separate piece of code decides whether the box is usable.

Check forward before trusting anything#

The checker runs the current program over intervals rather than individual integers. Addition combines endpoint bounds. A comparison selects a definite arm when its intervals establish the outcome; otherwise the result includes both arms. Every operation must overapproximate all concrete results represented by its inputs.

This is standard abstract interpretation. The important application here is the final condition: every output interval must collapse to the exact claimed value. Being “probably unchanged” does not pass.

# The final step of check(), after checking shape and domains.ranges = abstract(program.nodes, cert.box)return all(    ranges[i] == (v, v)    for i, v in zip(program.outputs, cert.plan))

The checker also verifies that the proposed box is well formed and contained in the declared input domain. It never authorizes reuse by sampling a few inputs. A bad proposal falls back to a checked singleton-input box; if checking cannot establish even that, compilation continues without adding a region.

The tests inject a producer that lies and claims the entire input domain. They also widen a width interval across a bucket boundary, alter a claimed output, and allow a previously inactive salt to become active. Those certificates must fail. An optimization should be able to be wrong about where to look without becoming wrong about the answer.

Calling this a certificate does not mean the prototype ships a large derivation for a tiny proof kernel. The certificate contains the box and result. The forward interpreter rechecks the graph. Its cost is worthwhile only when enough concrete executions can share the answer.

The claim I can prove#

Let P be an admissible staging program, B an input box, and r the claimed plan. The statement is small enough to write directly:

check(P, (B, r)) = true    implies: for every x in B, P(x) = rWith the same lowering context K:    K(P(x)) = K(r)

The proof is induction over the instruction graph. Literals and inputs satisfy their intervals. Each transfer rule encloses the possible results of its operands. Therefore every concrete output lies in its computed output interval. If that interval contains exactly r[i], the concrete output must equal r[i]. Apply that to every output, then pass the equal tuples to the same deterministic lowering function.

The full proof note covers negative integers, floor division, remainder, selection, source changes, and the trust assumptions. It is a handwritten argument, not a proof-assistant verification of the Python implementation. Its mathematical foundation comes from interval analysis; I am not presenting the induction itself as new research.

The model matters. Programs have no effects, pointers, mutable state, recursion, or unbounded loops. Selection chooses between already-computed values. All intermediates must fit the constructor's conservative 256-bit bound. The generated kernels expose no specialization-local state or meaningful function identity. Those restrictions are what make exact plan equality sufficient.

Every request still checks its complete input schema before looking in the cache. An invalid label remains invalid even though labels are absent from the generated arithmetic. This preserves the prototype's validation behavior; it does not claim to solve all the diagnostics and effects of a production language.

Now edit the planner#

A source hash is a useful invalidation signal, but it does not tell me whether a particular cached result changed. I edited every recurrence step in the planner, replacing one multiplication with a multiplication and an addition.

# Old planner instruction:product = seed * 1664525# Edited planner instructions, same mathematical integer result:product = seed * 1664524 + seedcompiler.install(workload(edit=True))c = compiler.compile((191, 42, 0, 3))assert c is aassert compiler.stats["evaluations"] == 1

install checks each saved box and plan against the new program. It does not assume the edit is equivalent because I called it a refactor. If the forward checker still produces those exact singleton outputs, the entry survives. If not, the entry loses its region and future requests evaluate normally.

The argument is local. The old and new planners may differ elsewhere. Reuse requires agreement throughout the retained box, not whole-program equivalence. Changing a recurrence constant fails that check in the tests. Tightening the label domain also rejects old boxes that extend beyond the new domain.

A separate test makes the planners genuinely different: x < 64 ? 0 : 7 becomes x < 64 ? 0 : 8. The certificate for the lower half survives. The one for the upper half fails, and a later request gets the new answer. Agreement where we reuse is enough; agreement everywhere is unnecessary.

A changed lowerer, target convention, or relevant build option is different: that changes the context in which a plan becomes code. The prototype flushes the cache when its context changes. It does not persist native objects, and its caller must route program/context changes through this installation API.

What the measurements actually count#

I compared three implementations: full-input keys, result-plan keys, and checked regions. All use the same planner and body generator. The shared workload has 2,048 distinct configurations but eight effective width buckets. The cold timer includes constructing the program, its whole-domain admissibility pass, validation, evaluation, proposal/checking, lookups, and generated bodies.

The edit experiment includes constructing the changed program, rechecking regions, making the changed request sequence, and processing it. Its separately measured initial builds were 128.1, 99.5, and 9.5 milliseconds respectively. Every output is checked against a direct-formula reference outside the timed region.

These are Python frontend timings on a small staged language. They establish avoided work in this implementation, not a prediction for Zig's evaluator or Rust's compiler. The mechanism does not need the frontend to be slow in absolute terms, but its practical value depends on how much work the planner represents.

I also compiled generated C++ to native object files. For that test I used 128 configurations and 32 rounds, included generation and source writing, and ended the timer after object output. Linking and the independent runtime checks were outside the timer.

The plan and region variants generate byte-identical C++ source. Their native compilation times are similar and their observed total-time ranges overlap. The large saving over the full-input version belongs to body sharing, which the previous article already demonstrated. The extra mechanism saves planner executions; it does not deserve credit for an imaginary improvement inside Clang.

The case where I should leave it off#

Next I removed the duplicate plans. With width divided by one rather than 64, all 128 configurations in the control produce different plans. Full-input caching took a median 7.7 milliseconds. Result-plan caching took 8.0. Checked regions took 18.6, with zero hits.

The region version paid to propose and check entries nobody reused, then searched them. Its 32-region cap bounded the damage, but did not make the work profitable. A general compiler would need a policy for where to try this. The experiment implements a cap, not an adaptive profitability model.

Intervals also fail to represent useful relationships. If two changing values cancel, a rectangular box often cannot express the necessary correlation. A solver or relational abstract domain could prove more cases, at a different cost. I have not implemented either, and no result here assumes one.

All recorded runs use Python 3.13.5 and the installed Clang 17.0.0 on Linux x86-64. Modes receive one unrecorded warm-up and five samples in rotating order. The machine is shared and unpinned, with warm filesystem caches. Frontend cases start fresh compiler instances; native compilations start fresh processes. There is no outlier filtering or statistical significance claim.

The raw report keeps every reported sample, counters, versions, source fingerprints, and object sizes. The seventeen-test suite includes 63,504 small-domain interval-containment checks and 9,134 concrete comparisons inside generated certified boxes, alongside invalidation, hostile-producer, and native-code tests.

python3 -m unittest discover -s examples/prove-it-then-skip-it -p 'test_*.py' -vpython3 examples/prove-it-then-skip-it/experiment.py --cxx clang++ --output /tmp/region-results.json

The correctness suite is wired into repository validation. Timing thresholds are not. These measurements do not cover production application builds, runtime throughput, memory usage, or a persistent object cache. The finite exhaustive checks exercise the implementation; they are additional evidence rather than the quantified proof.

What survived the prior-art search#

I wanted a genuinely new mechanism, so I searched before claiming one. The first overlap was Selective Memoization by Acar, Blelloch, and Harper: programmer control over equality and precise dependencies is already part of that work. Describing the new cache as “memoization, but only the important inputs” would hide the existing idea.

The closest broader match was Shared Certificates for Neural Network Verification. It uses checked templates and containment to avoid repeated verification work. Its soundness discussion also separates heuristic template generation from the check that makes reuse safe. That is substantial overlap with the broad mechanism here, even though this prototype's property is equality of a complete compilation plan.

Rechecking after source edits also has history. Incremental Abstraction-Carrying Code considers certificates and untrusted program updates. Demanded Abstract Interpretation combines incremental analysis and changing demands. My implementation simply rechecks the whole graph for each retained box; it does not reproduce those systems' machinery.

Result-based reuse itself is familiar from Rust's incremental query model. And 2026 research on the limits of proof sharing studies when templates are worth their overhead. Even the proposed next step of being selective about profitability needs that context.

There is still a precise contribution to inspect: this article's implementation automatically pulls input boxes backward from exact plan demands, checks them independently, reuses generated bodies on unseen inputs, and revalidates the boxes after a planner edit. The benchmark separates those effects from ordinary result-plan sharing and includes a failure case. The code and search record make that contribution falsifiable.

What I can establish is that the implementation behaves differently from the explicitly defined full-input and result-plan baselines. That does not establish that nobody has published an equivalent combination. A correctness proof says the transformation preserves the modeled result. A novelty claim needs a defensible distinction from prior work. The first does not supply the second.

The part I would take into a real compiler#

I would start at an existing pure, bounded compile-time boundary whose result already controls expensive downstream work: a layout planner, a generated decoder description, or a specialization plan. Give it a small immutable result. Track every input it reads. Keep source locations and current validation separate from reusable code where semantics permit that separation.

Then profile repeated planner executions before adding proof machinery. A handful of cheap calls will not repay it. A large family of configurations that differs mostly inside constant-output regions might. The negative control is a reminder to keep ordinary result caching as a cheap fallback.

The experiment gave me a concrete improvement over where the previous article stopped. I no longer have to hand-write every reduced key, and an equivalent source edit does not automatically make every input start from scratch. Eight checked regions were enough for this workload. That is a useful result to build on without pretending the literature began with this repository.