WIP-0002: Unified classical and quantum semantics

Summary

Wheeler uses one typed model for classical reversible work, coherent quantum work, measurement, and host effects. A verified classical rev function that meets the coherent rules can run as WIP-0001 bytecode on a CPU. With coherent operands, the compiler may lift the same function into a unitary operation.

Quantum regions lower to backend-neutral IR inside the same .wbc artifact. They are not foreign-language text or opaque provider circuits. Source transitions may look smooth, but the IR keeps each kind of edge explicit. Classical bodies retain inverse, log, and barrier classes. Coherent bodies are exact finite permutations. Unitary bodies are quantum regions with adjoints. Measurement, reset, target submission, replay, and retry remain separate typed operations.

Known classical values may configure or prepare quantum state. Measurement consumes coherent state and returns classical observations. Quantum data is affine, so code cannot clone or inspect it. A resource must be uncomputed, measured, reset, or returned under its contract. Wheeler does not call measurement or remote submission physically reversible. It records observations and may replay or restart the workflow under WIP-0004.

Motivation

The examples require more than a classical VM plus a quantum library:

• Counter and BinaryTree need reversible classical state.
• QFT needs a closed unitary circuit and its inverse.
• QuantumOptimizer and QuantumNeuralNetwork move between quantum execution and classical optimization.
• SurfaceCode needs mid-circuit measurement, decoding, and target-side feedback.
• QuantumCompiler combines classical circuit changes with calibration work.
• QFTProof ties unitary, inverse, and resource claims to the same program.

Earlier sketches mixed boundaries that must stay separate. They placed measurement inside reversible transactions, treated arbitrary quantum state as copyable through CNOT, let clean appear to erase an unknown register, and allowed a quantum pure function to measure a qubit. One vague meaning of "reverse" cannot describe all of those operations.

The model must work for noisy gate devices, simulators, future fault-tolerant machines, and tightly coupled classical-quantum processors. Provider APIs will change. Linear quantum information, unitary evolution, measurement, and classical observation are the stable parts of the contract.

Use cases

One reversible function, two execution domains

A finite-width rev permutation is called with ordinary integers and executes as classical bytecode. The same function is called with coherently encoded basis values inside a quantum region and lowers to a unitary oracle without source duplication or a provider API.

QFT and inverse QFT

applyQFT lowers to a parameterized unitary region. uncall applyQFT or reverse applyQFT uses compiler-validated inverse order and inverse gates. The circuit runs identically under the semantic simulator or a compatible hardware target after decomposition.

Variational loop

A classical optimizer binds parameters into a quantum circuit template, submits repeated executions, receives measured classical results, and updates parameters. Source remains one hybrid workflow even when a remote target makes each quantum materialization asynchronous.

Dynamic error correction

A surface-code cycle contains coherent gates, syndrome measurement, bounded classical decoding, reset, and conditional corrections. It can execute as one region only on a target advertising the required dynamic-circuit and latency capabilities. Otherwise the compiler reports a capability error or uses an explicitly selected host-split plan.

Ancilla cleanup

A lifted reversible computation borrows ancillas initialized to zero, computes a result, copies only allowed classical-basis output, and applies its inverse so every borrowed ancilla returns to zero. The compiler rejects clean on an entangled or unknown register.

Goals

• Give classical, quantum, hybrid, rev, and pure precise, orthogonal meanings.
• Let coherently eligible reversible source run on either a classical VM or quantum target.
• Represent quantum code as typed, backend-neutral region IR in .wbc.
• Make preparation, coherent lifting, measurement, reset, and host submission explicit transitions.
• Enforce no-cloning, affine ownership, ancilla cleanup, and use-after-measure rules.
• Separate inverse execution, machine rewind, measurement replay, and workflow retry.
• Partition hybrid programs according to target capabilities without changing source-level results.
• Keep current and future target details behind WIP-0003.

Non-goals

• Promise that every classical Wheeler function can execute coherently.
• Make floating-point optimization, I/O, arbitrary allocation, exceptions, or logged history unitary.
• Hide measurement or claim that a hardware measurement can be undone.
• Define provider queues, credentials, jobs, or Qiskit transport. WIP-0003 does that.
• Define durable workflow history and retry. WIP-0004 does that.
• Accept the existing proof syntax as a sound theorem system.
• Standardize pulse-level control or one physical error-correction architecture.

Terms and semantic model

Data domains

• A classical value is ordinary copyable data represented in WIP-0001 slots or regions.
• A coherent value is a finite logical value encoded in quantum basis state and possibly superposition. It is affine and cannot be copied, compared, printed, or branched on classically without measurement. WIP-0041 qvalue<Slot<T>> is one such value with a compiler-owned valid subspace and identity behavior on padding.
• A quantum resource is a qubit, qureg, logical qubit group, or target-defined affine handle owned by one lexical or execution region.
• A classical parameter is immutable classical data used to construct gates or choose compile-time region structure without becoming quantum state.
• A measurement result is a classical observation with basis, shot, region, and target provenance.

Callable characteristics and effects

Computation domains, callable characteristics, and effects are separate. WIP-0031 names ordinary, reversible, coherent, and unitary callable kinds and canonical effect rows. This WIP owns the quantum meaning of the relevant characteristics and boundaries:

classical, quantum, and hybrid describe allowed data and lowering regions. They imply neither purity nor reversibility. A quantum function that measures carries measure and is not pure. A closed gate operation normally has the unitary characteristic. A hybrid function may sequence several explicit effects without turning any of them into an inverse.

Transition boundaries

The core transitions are:

classical known data --prepare/encode--> coherent data
coherent data --unitary/rev lift--> coherent data
coherent data --measure--> classical observation
coherent data --reset--> known coherent data
classical workflow --submit--> target job/continuation

There is no implicit coherent-to-classical conversion. Passing classical gate angles does not encode them into qubits. Measurement is explicit even when a simulator can expose amplitudes internally.

Reversibility meanings

Wheeler uses distinct terms:

• Inverse and adjoint execution applies the mathematical inverse of a classical permutation or unitary region.
• Uncompute applies inverses until temporary coherent or reversible state returns to its required clean value.
• Machine rewind consumes WIP-0001 step records for classical execution.
• Replay reuses recorded nondeterministic observations without claiming to restore physical state.
• Retry prepares a new target state and executes the region again.

Source documentation and diagnostics must name the applicable operation instead of calling all five "reverse."

Ownership and boundaries

The language owns data domains, affine use, effects, inverse declarations, preparation, measurement, reset, and source-level region composition.

The compiler owns coherent-eligibility checking, region partitioning, inverse generation, ancilla accounting, backend-neutral quantum IR, source mapping, and target requirement inference.

WIP-0001 owns classical execution, artifacts, effect barriers, and machine rewind. WIP-0003 owns target capabilities, lowering, submission, and results. WIP-0004 owns hybrid continuations, replay, retry, and committed history.

Targets own physical or simulated quantum state. Wheeler code never receives raw provider qubit objects. Hosts own credentials and target selection but do not weaken type or effect checking.

Design

Coherent lifting

A rev callable receives the WIP-0031 CoherentFunction characteristic when the compiler proves all of the following:

• inputs, outputs, and mutable state have finite exact encodings.
• every reachable operation is intrinsic or checked reversible and has a unitary lowering.
• no operation uses logged undo, measurement, reset, submission, host I/O, randomness, wall time, or exceptions.
• loops are statically bounded or lower to a verified reversible control structure.
• temporary allocation has a static bound and every ancilla is returned to its declared clean state.
• arithmetic semantics have a finite reversible representation, such as explicit modular width.
• all callees are coherently eligible.

An optional source annotation may require coherent eligibility and turn loss of eligibility into a declaration-site error. Eligibility is recorded in the function descriptor and can be independently checked from quantum-body metadata.

Calling an eligible function with classical operands uses its WIP-0001 body. Calling it with coherent encodings inside a quantum region uses its lifted unitary body. Dispatch follows static operand domains. There is no runtime provider-name overload.

A reversible in-place function lowers as a permutation of basis states. A non-bijective pure function may only become an oracle through an explicit reversible embedding such as (x, y) -> (x, y xor f(x)). That broader oracle synthesis is not implied by pure.

Affine quantum ownership

qubit and qureg values are affine. Assignment transfers ownership unless the operation explicitly borrows. Aliases may identify disjoint slices only when the compiler proves disjointness. A measured or reset-consuming handle cannot be used under its old state identity.

CNOT does not copy an arbitrary quantum state. It may copy a computational-basis bit into a clean target, or entangle a superposed control and target. The type and proof systems must not label the latter as an independent saved state.

Ancillas, uncompute, and clean

An ancilla declares its initial and required final state, normally |0> or a logical clean state. uncompute applies the validated inverse of a recorded coherent computation. It does not delete a value.

clean resource is accepted only when static analysis or a checked target operation establishes the resource's required final state. Unknown or entangled state must be uncomputed, measured, or reset according to explicit effects. History cleanup in classical code remains a WIP-0001 COMMIT, not quantum erasure.

Quantum region IR

The .wbc region graph describes dependencies among classical bodies, quantum bodies, preparation, measurement, and host materialization points. A quantum body contains typed operations for:

• logical resource declaration and disjoint slicing.
• a small semantic gate set and parameter expressions.
• calls to unitary bodies and coherently lifted reversible functions.
• adjoint and controlled application.
• barriers that constrain optimization but do not imply host synchronization.
• measurement with explicit destination and basis.
• reset and known-state preparation.
• bounded static control and target-capability-dependent dynamic control.
• source locations, inverse relationships, and resource estimates.

The IR names semantic operations, not Qiskit classes or one hardware native gate set. WIP-0003 lowering decomposes those operations for a target.

Generic quantum instruction set

Section 8 uses a provider-neutral quantum instruction stream from the first format. It does not grow by embedding QASM strings or assigning provider opcodes after the fact.

Each instruction record has this regular shape:

u32 quantum_opcode
u32 field_count
u64 fields[field_count]

The quantum opcode selects a named form with ordered semantic field groups. Gate instructions name a stable gate descriptor, an exact logical-qubit window, and an exact numeric or symbolic parameter window. Unitary calls name a verified coherent function and direction. Measurement, reset, preparation, controlled application, bounded quantum control, and barriers receive their own forms as those semantics become executable. They do not masquerade as gates.

Gate descriptors own stable identities, qubit roles, parameter roles, adjoint rules, and capability requirements. The baseline registry contains H, X, Z, PHASE, CPHASE, CNOT, CZ, and SWAP. A target may decompose them. It may not change their meaning. Later standard gates append descriptors under explicit capability and version rules without changing the instruction record.

Unknown quantum opcodes and gates fail before execution. A field count lets the decoder bound a record, but it never permits semantic skipping. Provider-native gates, pulse schedules, calibration references, and QASM remain derived target data.

This is a generic semantic ISA, not a claim that hardware shares one physical instruction set. The split keeps one portable source of truth while allowing superconducting, trapped-ion, neutral-atom, photonic, and simulated targets to choose different native bases.

Region partitioning

The compiler partitions a hybrid function into maximal regions allowed by data dependencies and target capabilities:

• compile-time classical loops around gates may be unrolled or represented symbolically.
• coherent conditions become controlled unitary operations.
• measurement-conditioned control remains target-resident only with dynamic-circuit support.
• host classical computation after measurement ends the current remote quantum region unless the target supports an uploaded bounded classical kernel.
• a later quantum region starts from explicit newly prepared or target-session state, never an assumed surviving cloud qubit handle.

Partitioning is observable in cost and latency but not in typed program results. The compiler can emit a plan explaining every split and capability requirement.

Transactions

Before measurement, a transaction consisting only of classical reversible and unitary operations may abort by applying inverses while resources remain live.

After measurement, reset, submission, or external effect, abort cannot restore an unknown physical pre-measurement state. It may restore classical state, discard observations, reset/reprepare resources, and retry according to WIP-0004. Source rollback must therefore carry an effect-sensitive type and cannot promise physical time reversal.

Example interpretation

Reversibility and history

Classical execution follows WIP-0001. Coherent bodies carry an adjoint mapping for every operation and a reversed dependency order. Gate decomposition must preserve that mapping.

Measurements emit observations, not undo records capable of recreating unknown physical amplitudes. A simulator may checkpoint its internal state for debugging, but that is an implementation feature and cannot strengthen portable language semantics.

A lifted rev body must not depend on WIP-0001 dynamic history. Information needed for inversion remains in coherent output or clean ancillas under a unitary mapping.

Concurrency and determinism

Within one quantum body, operation dependency order is deterministic. Operations on disjoint resources may be scheduled in parallel by a target when commutation and declared barriers permit it.

Measurement outcomes are nondeterministic observations. Simulators accept explicit seeds where the model supports seeded sampling. Hardware does not promise seeded outcomes. WIP-0004 records result provenance for replay.

This proposal does not define shared-memory VM threads. A later concurrency design must preserve affine quantum ownership and cannot concurrently mutate one quantum resource through aliases.

Quantum and proof implications

This proposal establishes the semantic facts a later proof system may trust: operation signatures, effect sets, affine resource flow, inverse/adjoint relationships, region boundaries, and target requirements. It does not trust textual because clauses or make a compiler test equivalent to a mathematical proof.

A future proof certificate may establish unitary equivalence, ancilla cleanup, bounds, decomposition equivalence, or properties such as QFT correctness. Runtime execution remains safe without such certificates. Unsupported optimization or theorem claims are rejected instead of assumed.

Bytecode, persistence, and compatibility

WIP-0002 activates WIP-0001 section types 7 and 8. Region and quantum records are length-delimited and versioned. Function descriptors gain explicit effect sets, coherent eligibility, and quantum-body references.

Provider-compiled circuits, physical layouts, calibration snapshots, and credentials are not canonical semantic bytecode. They may be cached as target-qualified derived artifacts keyed by semantic region hash and target fingerprint.

Changing the meaning of a semantic gate, measurement, ownership rule, or coherent-eligibility condition requires a major semantic version. Adding an optional operation requires a declared capability and canonical rejection by older runtimes.

Safety, limits, and failures

Compilation and runtime enforce bounds on logical qubits, ancillas, gates, depth estimates, parameters, controls, loop iterations, measurements, result bits, shots, and region splits. Target limits may be stricter.

The compiler rejects cloning, overlapping mutable slices, use after consume, dirty ancillas, implicit measurements, unsupported coherent lifts, unbounded dynamic control, and a pure declaration containing measurement or submission.

A target capability failure occurs before submission whenever possible. No fallback silently changes ideal semantics, noise policy, shot count, measurement basis, or error-mitigation method.

Host and target I/O boundary

WIP-0032 supplies the asynchronous lifecycle for classical target submission, cancellation, result delivery, large classical payloads, and session recovery.

Quantum state is not a byte stream, file, mapped object, direct-I/O buffer, or RDMA region. Coherent target interaction remains typed quantum-region IR. Measurement, reset, submission, classical transport, replay, and retry remain distinct transitions.

Migration and deletion

1. Define effect and affine ownership models independent of the current AST hierarchy.
2. Add coherent-eligibility checking over a small WIP-0001 reversible function subset.
3. Define canonical region graph and quantum-body records in .wbc.
4. Implement a semantic simulator for the initial gate, preparation, measurement, and lifted-function subset.
5. Compile Counter classically and one finite reversible oracle both classically and coherently.
6. Compile QFT with generated adjoint and compare it against the hand-written inverse fixture.
7. Rewrite QuantumOptimizer as the first measured hybrid fixture.
8. Correct no-cloning, cleanup, purity, transaction, and remote-lifetime violations in the larger examples.
9. Delete AST and grammar constructs that cannot be assigned accepted semantics instead of retaining nonfunctional syntax.

Progress

• [x] Classical, quantum, and hybrid program domains are represented and verified.
• [ ] Quantum resources have complete affine ownership and slice checking. The first profile prevents aliases by construction.
• [x] Coherent eligibility and lifted reversible calls work for the exact XOR subset.
• [x] Workflow and quantum body sections have canonical encoding and strict decoding.
• [x] Quantum instructions use stable opcode and gate registries, named forms, ordered roles, and bounded variable-length records.
• [ ] Measurement, reset, preparation, controlled application, and target-resident control need executable instruction forms.
• [x] The semantic state-vector simulator executes the initial gate and lifted-function subset.
• [x] Counter, coherent oracle, QFT, and the bounded measured optimizer pass end to end.

Testing and acceptance

• [x] The same eligible rev XOR function produces matching classical basis results in the WIP-0001 VM and semantic quantum simulator.
• [x] Superposition tests show the lifted function acts as a unitary permutation, not a measurement-driven classical call.
• [x] A lifted function and unitary circuit followed by its generated adjoint restore the simulated register.
• [ ] Compiler-negative tests reject cloning, dirty ancillas, overlapping slices, use after measure, hidden logged history, I/O, and unbounded loops in coherent bodies.
• [x] QFT followed by its generated adjoint restores the checked basis-state fixture within numeric tolerance.
• [x] Full-register measurement produces a typed classical observation. Broader consumed-identity checking remains.
• [ ] Static, host-split, and dynamic region plans preserve the same ideal result distributions where each is semantically valid.
• [ ] The optimizer fixture alternates parameter binding, quantum sampling, and classical updates without provider APIs in source.
• [ ] The surface-code fixture declares and checks dynamic measurement/reset/feed-forward requirements.
• [x] Every current example compiles, round-trips, parses with Tree-sitter, and executes in CI.
• [x] Current language and hybrid references distinguish inverse, uncompute, rewind, replay, and retry.

Alternatives

Separate classical and quantum languages

Rejected. It would duplicate types, modules, diagnostics, tooling, and algorithm structure, and it would prevent verified reversible functions from becoming reusable coherent operations.

Treat quantum blocks as embedded Qiskit or OpenQASM strings

Rejected. Foreign strings lose Wheeler types, source maps, inverse relationships, affine ownership, proofs, and portability to future targets.

Make transitions entirely implicit

Rejected. Automatic region partitioning is useful, but preparation and measurement change information domains and must remain visible in semantics and diagnostics.

Treat measurement as logged reversible mutation

Rejected. Recording an outcome supports deterministic workflow replay. It does not reconstruct an unknown pre-measurement physical state.

Permit arbitrary classical calls from a quantum region

Rejected. Today's devices and unitary semantics require a bounded coherent subset or an explicit host split. Provider implementation convenience cannot define language meaning.

Model CNOT as quantum copying

Rejected by no-cloning. It copies known basis information in a restricted case and entangles superposed inputs in general.

Open questions

• What source annotation should require, instead of only infer, coherent eligibility for a rev function (owner: language maintainers. Decision point: before this WIP enters Review)?
• Which additional baseline gate descriptors earn canonical identities rather than remaining verified decompositions (owner: quantum compiler maintainers. Decision point: before the first post-baseline gate enters Review)?
• Which finite classical data encodings are required in the first coherent-lifting slice beyond bits and fixed-width unsigned integers (owner: type-system maintainers. Decision point: before implementation begins)?

Integration with reversible concurrency

Classical tasks and quantum resources

WIP-0039 task, shared, blocking, and schedule-observation effects are outside coherent and unitary eligibility.

A classical task may move one affine Qreg owner to one child or proven-disjoint views to different children. Every view rejoins before cross-view work. Entanglement grants no copyable ownership.

Static parallel unitary work remains WIP-0037 DisjointGroup. Target submission and results remain WIP-0003 and WIP-0032 operations. Provider jobs are not VM tasks.

References

• WIP-0039
• WIP-0040

• WIP-0001
• WIP-0003
• WIP-0004
• WIP-0010
• WIP-0028
• WIP-0029
• WIP-0030
• WIP-0031
• WIP-0032
• Counter.w
• QFT.w
• QuantumOptimizer.w
• QuantumNeuralNetwork.w
• SurfaceCode.w
• QuantumCompiler.w