Wheeler

WIP-0014: Bounded certified program synthesis

FieldValue
StatusDraft
OwnersWheeler language, synthesis, proof, quantum, runtime, and package maintainers
Created2026-07-18
Updated2026-07-18
AreaFinite types, synthesis, model checking, quantum search, proofs, packages
Depends onWIP-0004, WIP-0007, WIP-0008, WIP-0009, WIP-0010, WIP-0011, WIP-0012, WIP-0013
SupersedesNone
Superseded byNone

Summary

Wheeler may later support bounded certified program synthesis. The system would search a finite, canonical grammar of Wheeler IR operations for a program that meets a finite mathematical specification. It would then check the program exactly, prove minimality within the chosen grammar and resource metric, and publish proof-carrying source with canonical .wbc.

Candidate syntax, search encodings, SAT terms, and provider circuits are derived data. Only independently verified closed IR and kernel evidence may be published as accepted output.

Foundry.w is the main application. Its first target is the smallest reversible comparator network, within a stated comparator limit, that sorts eight 4-bit integers while keeping and cleaning an exact inverse witness.

This WIP does not reserve source syntax today. It defines the semantic parts and acceptance rules that a later syntax proposal must satisfy.

Motivation

Wheeler already has several useful parts for bounded synthesis:

The synthesis service must not become a second compiler, proof authority, package format, or target API. Search may use heuristics, distributed workers, quantum assistance, or a different algorithm later. Acceptance remains deterministic and content-addressed.

The input is a specification, a candidate grammar, and fixed limits. There's no training dataset, model checkpoint, or sampled correctness standard.

Goals

Non-goals

Terms

A finite type has a canonical finite inhabitant set, canonical total order, canonical fixed-width or bounded encoding, and checked cardinality.

A candidate grammar is a finite typed program language with one canonical encoding per semantic candidate admitted by that grammar. Grammar identity includes instruction semantics, operand domains, normalization rules, program bounds, and resource metric.

A specification is a closed proposition over finite inputs and explicit outputs, effects, inverse witnesses, and resource claims.

A search result is evidence that identifies candidates worth exact checking. It is not a proof.

A correctness certificate proves that one exact candidate satisfies one exact specification under one semantics profile.

A minimality certificate proves that no candidate with a strictly smaller declared metric satisfies that specification within the same grammar and bounds.

Semantic model

Finite domains

Every quantified type supplies:

Cardinality arithmetic is checked and bounded. A quantifier whose domain exceeds the selected proof/checking profile is rejected before search.

Candidate identity

Candidate source text isn't the search identity. A grammar-specific canonical AST or instruction vector is. Construction or a deterministic normalization certificate removes equivalent encodings.

For comparator networks, each instruction names two distinct indices in canonical order. Inactive slots have one required zero encoding. Network length is part of the candidate value. Scheduling symmetries may be normalized only by a checked rule.

Reversible candidate evaluation

A candidate evaluator receives clean explicit workspace. It may mutate a working input and inverse witness, but must uncompute decoder scratch, temporary execution state, and oracle flags before returning. The Boolean acceptance bit is the only allowed oracle output.

Sorting is not intrinsically reversible. A compare-exchange operation records whether it swapped. Its inverse uses that bit to restore the pair and clears the bit after reconstructing the original predicate. Hidden VM history is not a substitute for this source-level witness.

Search consumes a finite candidate encoding and an exact predicate. Implementations may use classical enumeration, SAT, SMT, specialized network search, amplitude amplification, or a composition. Search algorithms are outside the trusted computing base.

A quantum execution records semantic-region identity, target descriptor, lowering policy, job lineage, shots, uncertainty, resource use, and durable event history. Measurement yields candidate evidence only.

Absence at a candidate length requires a checked nonexistence certificate. Timeout, cancellation, an empty sample set, or a provider's failure to return a candidate proves nothing.

Exact checking

The selected candidate is checked again without trusting search evidence. An implementation may use:

All methods elaborate to bounded canonical proof terms. The kernel does not invoke a solver or quantum target.

Minimality

Minimality is lexicographic only when declared as such. A metric might be comparator count, depth, expensive-gate count, ancilla width, bytecode length, or a canonical tuple. The certificate identifies the metric and proves absence for every strictly smaller metric value admitted by the bounded grammar.

The claim does not extend to another instruction set, arithmetic semantics, width, approximation policy, hidden history allowance, or computational model.

Syntax requirements

A future syntax proposal must define, instead of only illustrate:

The Foundry design page is syntax input for those proposals. It is not grammar authority.

Trusted boundary

The trusted path contains only:

  1. canonical artifact decoding.
  2. ordinary bytecode and ownership verification.
  3. finite-type and candidate-grammar identity checks.
  4. proof-term decoding and bounded kernel checking.
  5. package/archive identity verification.

Quantum targets, model checkers, SAT/SMT solvers, candidate selectors, proof search, source generation, registry transport, and user interfaces are untrusted producers. A defect may lose work or produce a rejected certificate. It cannot establish a false theorem.

Durable execution

Each search length is a transaction phase. The run records submitted work and evidence, verifies any absence certificate, then commits that length as impossible. Recovery resumes from the latest verified commit.

A candidate found after a crash is rechecked. Replay may reproduce the decision to inspect a recorded candidate but does not resubmit quantum work. Retry creates new job and evidence identities. Cancellation and timeout leave the current length unresolved.

Winning target evidence must be stored outside loop-local scope and tied to the candidate selected from it. Package provenance cannot refer to whichever evidence variable happened to be evaluated last.

Package output

The generated package contains:

Publication requires an explicit capability and follows WIP-0009 immutability rules. Search credentials, provider objects, local cache paths, and unbounded logs are excluded.

Determinism and bounds

Every source of work is bounded. Limits cover finite cardinality, candidate bits and length, interpreter steps, workspace words, qubits, gates, shots, job attempts, events, proof nodes, certificate bytes, kernel recursion, package bytes, and total duration.

Parallel or distributed search may finish in any order. Candidate selection reduces results by canonical metric then candidate encoding. Proof diagnostics and package members reduce in canonical order. Scheduling, hash iteration, wall clock, provider queue order, and allocation address cannot change a successful package.

Failure behavior

The implementation fails closed on:

No partial package is published. A failed publication leaves a checked theorem valid and creates no release.

Implementation order

  1. Complete finite widths, bounded arrays, ownership, regions, and deterministic collections.
  2. Complete module linking, package APIs, and Wheeler-native execution.
  3. Complete proposition/proof-term schemas and the finite proof kernel.
  4. Add canonical finite-type enumeration and proof rules.
  5. Add first-class canonical candidate grammars and a classical reversible interpreter.
  6. Build a tiny exhaustive synthesis fixture without quantum search.
  7. Add proof-producing correctness and bounded minimality certificates.
  8. Add durable candidate-search workflows and explicit proof-search capabilities.
  9. Add coherent candidate interpretation and quantum-search planning.
  10. Add Foundry.w only when the ordinary compiler, VM/runtime, targets, kernel, package manager, Tree-sitter grammar, tests, and documentation execute it end to end.

Progress

Testing and acceptance

Security considerations

Candidate and proof search process adversarial generated data. All decoders are bounded. Solvers and target providers run outside the trusted process or under explicit capabilities. Certificate checking does not execute producer code. Generated source receives no authority by virtue of being generated.

A proof of finite correctness is not a proof that the specification is desirable, the cost model predicts hardware, the package has no side channels outside the modeled effects, or a larger-domain generalization holds.

Alternatives

Treat exhaustive tests as a certificate

Rejected. A test transcript is too large and proves canonical coverage only when the checker already trusts its enumeration and reduction. A bounded proof term states the finite reasoning directly.

Trust the synthesis or quantum service

Rejected. Search is the largest and least deterministic component. It is the wrong trust anchor.

Publish only generated source

Rejected. Recompilation can change meaning unless compiler, dependencies, profiles, and certificate subjects are fixed. The package carries all of them.

Claim unrestricted minimality

Rejected. Minimality without a grammar and metric is not a finite proposition.

Open questions

References