Wheeler

Bootstrap and Trust

A compiler can reproduce its own mistake. Byte equality establishes a fixed point. It does not establish a trustworthy ancestry.

Wheeler's promotion gate therefore requires two independent forms of evidence:

  1. stage 0 builds stage 1, and stage 1 builds a byte-identical stage 2.
  2. an independently derived trusted compiler produces the same bytes without first

    3. running candidate-produced code.

The repository does not yet contain wheeler.bootstrap.yaml because the Wheeler compiler has not completed that self-hosting gate. Creating the manifest early would give an absent event a convincing seal.

Present stage-0 work

Ordinary acceptance begins by rebuilding the alternate Java seed from source:

./bootstrap/gradlew -p bootstrap :stage0:clean :stage0:build

This supplies routine reproduction of the current alternate implementation. It is neither a Wheeler fixed point nor an independent derivation.

Three different paths provide native evidence today:

For admitted successful classical executions, the test report's workflow_steps field carries completed transitions of the tested artifact. It includes calls, callee bodies, executed inverse bodies, and termination. It excludes work performed by the outer native interpreter. It is not elapsed time or a proof bound. Native execution and report identities bind this retained count.

The retained source route admits 64 ordered identifier arguments in ordinary root and loop calls. Mixed scalars, UTF-8 and byte-view loans, and mutable word, byte, region, and map loans retain exact types. Qualified imported initializer, void, and forwarded-result calls pass. A forwarded return must be exactly return callee(arguments);. Unsupported expression tails reject before publication. Its 256 call rows share 16,384 argument entries per column. Argument 65 rejects before argument or artifact publication. The separate bounded helper compiler still admits at most seven arguments per call. Generated inverses still reject argument-bearing calls. These are implementation bounds, not language arity rules.

Counted archive compilation accepts the shared front's empty module qualifier for a class-only source. Callable and claim names remain bare, with no injected module declaration. Named sources keep their qualified names. The current native verifier accepts 24 final functions, including a library's synthetic entry, even though source staging admits 64 callable rows. Block comments use the scanner's existing 262,144-byte input bound. Source-product windows remain 32,768 bytes.

The bounded helper compiler can assign a signed call result to its existing class-state slot. These calls admit zero through seven signed arguments. A prior wrong-type or ambiguous local name rejects instead of falling back to state. Helper selection, canonical names, and entry emission keep the destination global. This does not provide general global tables, nominal test-body compilation, or an inverse for argument-bearing calls.

Direct signed less-than assertions accept literals, folded constants, prior signed locals or parameters, and the existing state slot on either side. Both operands retain their complete signed value or slot index. Native encoding evaluates each once in source order. False comparisons compile and trap before later mutation. This does not supply general Boolean expressions or direct global literal-call arguments.

Retained package-manifest products cover lexical and canonical policy, names, paths, semantic versions, headers, target fields, selector admission and coverage, collection policy, and row publication. Dependency and capability entry products check capacity before field validation and ordering. They publish complete rows before advancing counts and preserve exact failure offsets. Dependencies sort by name. Capabilities sort by name, then path. Rejected rows leave storage untouched. The source-list product owns traversal, ordering, coverage, and count commits for up to 1,024 selectors per target. Failed collections retain admitted selector prefixes, but publish neither a collection count nor a target row. Absent lists remain valid for nonmodular targets. Present empty lists reject. Fixed manifest words now use exact classification, not polynomial hash equality. Malformed aliases cannot impersonate keys, kinds, or Booleans. Lock, workspace, and snapshot readers share exact word admission without a hash-only compatibility path. Complete target admission returns a validated tail coordinate after head, module, collection, and test checks. The parser derives row fields without a target-result carrier. Target capacity, adjacent ordering, publication orchestration, the remaining collection loops, and other compiler modules still need physical integration.

Archive emission takes module and class names from lexical declaration products. It checks class-name extents inside the owning source before publishing callable or callable-free artifacts. Comments do not define another declaration identity. Direct statements and loop limits resolve constants against packed name bytes. They do not search raw source for a representative use. Unused names cannot alias the module header, and invalid matching products cannot hide behind valid ones.

Nominal carrier coordinates name actual frame locals. They do not count the optional serialized function result type. Final type linking preserves that result and rejects carriers outside the frame. Complete type-linker artifacts and typed-call execution remain distinct from nominal source compilation.

Imported nominal source writers share a checked declaration encoder. Temporary IDs cannot overwrite their record or variant kind tag. Complete selection, type, and byte windows validate before any caller storage changes. These fragments remain scaffolding, not retained semantic artifacts.

The final product publisher measures section extents before allocating artifact storage. It verifies the complete private container before changing caller output. Invalid code, types, entry, or proofs leave every caller byte unchanged. Accepted publication preserves the unused output tail. Framing checks alone do not establish executable validity.

Counted classical certificates carry generated-inverse or static-step claims. The product boundary retains both argument words and rejects circuit rules rather than rebasing circuit subjects as functions. Final verification checks a step claim against the composed body and manifest limit.

The scalar constant evaluator now accepts exact expression-token windows against counted products. It shares declaration precedence, consumes the complete window, and checks equality-token adjacency. Dependency source is not an input to a product-only evaluation.

Source classical claims now bind through shared member fronts and counted local callables. Qualified callable names must name the source module. The source table retains up to 64 inverse or positive signed step claims and copies each name into at most 256 bytes. A separate two-column origin table retains declaration byte starts and lengths, including visibility modifiers through the final semicolon. Its claim ordinal joins the unchanged five semantic columns. Malformed batches change no caller name, semantic cell, or origin cell. These are bound claims, not accepted proofs of final code. Ordinary structured compilation binds them from the complete detached scalar packet before artifact composition. The archive boundary validates every packet row, including unused constants. Identifiers and module qualifiers share a copied view with both starts rebased. The reduced body columns do not replace that seven-column expression packet. The classical artifact publisher consumes the same five-column claims, preserves both argument words, and merges proof names into the existing canonical string table without duplicating IDs. It verifies the final private container before publishing bytes or identity. Claim-free ordinary modules reuse private scratch without allocating new owned buffers. Generated-inverse coverage remains a separate homogeneous-callable policy. The intact mixed-member runner join remains open.

projectSourceClaimOrigins blanks a validated origin window in a private source copy. It checks the whole ordered, nonoverlapping batch and UTF-8 byte boundaries before changing a byte. Line endings, source length, and all other bytes survive. The caller retains the original semantic claims. This projection neither proves source absence nor decides a bound against primitive placeholders.

Source-local artifacts now retain up to eight declared signed globals, including unused state and full signed initial values. Initializers consume the complete scoped scalar packet, not dependency bodies. Callable and callable-free archive paths share canonical name ordering and write global descriptors before final verification. Shared spellings reuse string IDs. Adding a global also remaps class and callable name IDs where necessary. Invalid later declarations cannot publish earlier globals. Root scalar reads and stores now use explicit frame or global locations. Loads observe current state, stores keep declaration ordinals, and binary values reserve two operand locals plus their result. Complete artifact and callable execution checks compare against independent stage 0. They do not establish general scope admission or nested global lowering. Root assertions now share those locations and scalar emission. A predicate must produce a Boolean, and literal-left comparisons preserve operand order. Complete type/code preflight precedes publication. False assertions compile and reject at runtime without changing the failing instruction's machine state. Root signed call results also store at validated declaration ordinals. Argument preparation and one result local precede the store, without a synthetic global local. Nested call assignments reject until their owning lowering path can bind the destination. Imported signatures produce verifier stubs and identity relocations without dependency body source. Native retained global-instruction linking, global conditions, nested control, nominal/entry composition, and the intact mixed-member runner remain open.

An exact assert(global == literal) uses zero-local EXPECT_EQ when the state declaration precedes the assertion. Source-global products retain the original declaration-name byte range for this selection. Later declarations, named constants, and other predicates retain their generic scalar instructions.

Active source leases now accept exact immutable ASCII archive ranges. The publisher validates the complete range before copying into one of eight generation-checked slots. Symbol and callable intake no longer create an intermediate archive copy. Scheduling uses two regions and seven buffers for any admitted module count, including 512. This preserves the 32,768-byte source limit and removes per-owner lifetime-buffer consumption from scheduling.

Counted archive compilation takes an explicit deployable, tool, or library target kind. Executables bind exactly one ordinary entry void main and retain its source-local ordinal. Their artifacts omit the synthetic library name and function and terminate the selected body with HALT. Libraries retain their canonical synthetic entry. The admitted source body profile does not expand merely because entry binding succeeds.

Source binding and bytecode verification share the six canonical host-loan shapes. Native verification selects the manifest entry rather than requiring the final function. Calls and proofs may name later helpers, subject to their existing signature, inverse, and actual-code checks. Entry and helper claims verify before complete artifact hashing and publication. Relocation reports use the same prepublication result record rather than allocating a replacement afterward.

Callable coordinate staging now uses the shared member, modifier, parameter, and type fronts. It preserves source-relative module names and archive-relative callable and parameter ranges. Its mutable columns are private scratch, not published products. The closure owner validates every module before publishing rows and reports. The aggregate adapter consumes this staging boundary through its counted, claim-free primitive compiler. Original claims and globals still need their aggregate coordinate joins before final nominal publication. The adapter keeps carrier rows private through compilation and composition. Separate phases bind original values and resolve supplemental operations. The adapter validates every output backing before owned staging allocation, then constructs the complete report before publishing any caller output. The counted compiler borrows its selected source window without an additional exact-source copy. Late nominal rejection preserves every caller buffer, not just the artifact and identity. The remaining aggregate orchestrator still needs native frame extraction.

Local target binding handles the complete qualified name. Its byte walk uses the sum of the qualifier bound, the :: separator, and the identifier bound: 256 + 2 + 256. Neither name component may exceed 256 bytes.

Root manifest facts now reach final emission as an immutable product, not a borrowed artifact view. Source-local emission shares its byte encoder. Name and entry binding validate complete owner windows before rebasing. This closes one metadata handoff, not complete nominal source compilation.

Source keywords, Boolean literals, primitive types, intrinsics, and native test metadata now use exact word codes instead of token hashes. The fixed vocabulary contains 72 spellings and does not limit identifier length. The scanner admits source whitespace, including tabs and Unicode separators but not nonbreaking spaces. The exact set is U+0009..U+000D, U+001C..U+0020, U+1680, U+2000..U+200A except U+2007, U+2028..U+2029, U+205F, and U+3000. Line comments end at carriage return or line feed. ASCII classification does not enter the Unicode whitespace helper. Test discovery indexes recognized names before selection instead of reclassifying earlier token prefixes for every name. These changes do not complete class-member validation. Automatic test discovery can still ignore malformed member fronts, a separate open frontend boundary.

Source aggregate products now admit enum Flag { case Ready; } as a nonempty, payload-free variant. Enum tags follow lexical case order. Ordinary variants keep declaration order. The unchanged 64-aggregate and 128-case bounds apply before caller publication. An enum's name and each case name fit at most 256 copied bytes. This does not complete nominal body compilation or its test-runner integration.

The evidence tests derive their graph and archive from checked-in source. Comparable products match stage 0 byte for byte. Every selected imported-call product matches complete frame metadata and forward/inverse instructions after identity relocation. The tests also verify the linked container and pin its identity. These subset checks do not establish a complete compiler fixed point.

Platform ABI and native image plans

The first native profile has a canonical platform descriptor. It fixes loader format, architecture, minimum OS ABI, little-endian 64-bit pointers, page and alignment rules, resource bounds, CPU features, baseline libraries, and an exact host-service set. Required services cover process arguments and exit, standard streams, capability-relative file access and atomic replacement, directory manifests, and raw page reservation, release, and protection. Monotonic deadlines and target submission are optional named services.

Host calls use fixed-width scalars, checked byte spans, owned handles, and stable status codes. They do not pass host objects or exceptions through Wheeler frames. Profile 1 has no environment, wall-clock, network, random-device, unrestricted path, dynamic-loader, or process-creation service. A host cannot grant one by quietly noticing that its operating system has it.

PlatformAbi emits canonical schema-1 bytes and their SHA-256 identity. NativeImagePlan binds that identity beside the portable WBC, capsule, backend, runtime, compiler, sysroot, provider closure, options, link arguments, target, runtime mode, and sealing and stripping policy. The plan identifies build inputs. Unsigned native bytes receive a separate PREV. UnsignedNativeImageRecord binds complete adapter-verified format, target, plan, ABI, capsule, PREV, and byte count. NativeImageSigningRecord separately binds ELF repository signatures, Apple code signatures, or PE Authenticode distribution bytes and evidence. Signing products cannot alter the plan or PREV. image record-elf, record-macho, and record-pe publish unsigned records. record-signing publishes attached Apple or Authenticode metadata. record-repository-signing requires a domain-separated Ed25519 authorization and a matching key in one enabled repository policy entry. These commands do not invoke a signer. Apple notarization and Authenticode certificate validation remain outside this profile.

Platform ABI, image plan, output, and signing records have strict 16 KiB canonical parsers. They reject malformed UTF-8, schema or field drift, unknown values, reordered records, comments, trailing data, and numeric overflow rather than repairing transport.

The format-neutral application capsule is also fixed. Its bounded binary header carries exact lengths and counts. One root binds the package instance, selected target, qualified entry function, WBC, runtime mode, required capabilities, and runtime, bytecode, proof, target, platform, and limit profiles. Sorted package receipts bind repository, package revision, build input, PREV, export, and package instance evidence without performing runtime resolution.

A sorted entry table carries WBC, immutable resources, proof data, native provider data, and provenance. Each uncompressed entry has one logical name, SHA-256 identity, checked absolute range, power-of-two alignment, and fixed flags. The sole startup flag belongs to the root WBC. Padding is zero, the transport is consumed exactly, and SHA-256 of the complete canonical bytes is the capsule identity. Schema 1 admits at most 128 entries, 64 receipts, 32 capabilities, and 32 MiB in total.

wheeler image inspect <application.capsule> verifies this framing and renders root, profile, receipt, and entry metadata without execution. wheeler image verify <application.capsule> additionally verifies and canonically re-encodes every WBC, then requires the startup WBC's entry function to match the root exactly. Both commands consume one bounded physical file and perform no package resolution, adjacent lookup, extraction, provider loading, or capability grant.

Format-neutral embedded startup accepts the retained capsule bytes and an explicit launch context. Capsule, runtime, bytecode, proof, target, platform, and limit identities must match. The sorted capability grant must equal the root request and the verified entry's no-input, UTF-8, binary, output, or duplex signature. Startup rejects AOT, nonclassical roots, and external proof or native-provider payloads, then executes one fresh root exactly once. It never accepts a path.

The first native adapters emit position-independent ELF64 for x86-64 or AArch64 Linux, static Mach-O for arm64 Darwin, and PE32+ for x86-64 or arm64 Windows. One R-X segment or section contains a fixed image-relative locator and exact runtime text. A separate page-aligned R-- segment or section contains the capsule. ELF keeps the stack nonexecutable and omits section headers. Mach-O fixes page-zero, arm64 entry state, and platform-version commands. PE fixes DOS, COFF, optional, data-directory, section, alignment, and padding fields. No format maps writable executable bytes. Verification checks every loader field and identity, rebuilds exact bytes, and publishes the unsigned PREV only after success. Runtime text is an input bound by the image plan. Signing and notarization remain separate output identities.

wheeler image build-elf, wheeler image build-macho, and wheeler image build-pe consume exact physical capsule, runtime, plan, and ABI files. They verify all WBC before construction, self-verify the selected image before atomic publication, and print the unsigned PREV. Their matching inspect-elf, inspect-macho, and inspect-pe commands report canonically verified structure, identities, and ranges. The verify commands additionally check every WBC and the exact root without execution.

wheeler image runtime-elf-x86-64 -o <runtime.bin> atomically publishes the first maintained x86-64 Linux entry shim. Its 113 import-free bytes locate mapped ELF capsule framing without reopening the image, check the locator and capsule magic, complete one fixed standard-output write, and exit through the kernel. This proves loader entry and two host-service leaves. It does not verify WBC or execute the capsule root. No complete native runtime or recovery image ships yet.

wheeler image runtime-elf-x86-64-aot <root.wbc> --capsule <application.capsule> -o <runtime.bin> adds the first native backend leaf. Lowering verifies every capsule WBC, the exact root bytes and function, AOT mode, and entry capabilities. The loaded runtime compares the complete mapped capsule with one immutable copy of those verified canonical bytes before application execution. The former unbound WBC-only path is gone. It accepts one canonical classical WBC containing one zero-initialized status global, up to 31 additional shared signed globals, one to twenty-four dense functions, bounded constants, checked global addition and subtraction, global XOR and expectations, shared swaps, logged global replacement, forward checkpoint and commit markers, scalar updates, checked signed arithmetic, bitwise and 32-bit rotate operations, comparisons, assertions, status reads and helper-owned status publication, forward branches and 4,096-iteration checked loops, bounded recursive signed-result, Boolean-result, or void calls and parameterless forward or inverse helper calls, up to sixteen exact signed or Boolean arguments, status stores, returns, and halt. Recursion stops at 64 simultaneous calls. Six arguments use the private register order. Up to ten more use one aligned caller-owned stack area. An output-bearing entry may retain up to 4,096 constant application bytes and 64 locals. An exact byteview, bytes or utf8, bytes entry may instead read up to 4,096 complete stdin bytes and compute bounded stdout and process status at runtime. Canonical reborrows may carry those byte handles through bounded helper calls. Signed and Boolean helpers may fill and exactly clear caller-owned result slots through forward and inverse relations. Those inverse calls prove current state and do not claim history rewind. One 65,536-instruction fuel cell bounds the selected entry and complete helper call tree. Other entries retain up to 256 locals and 512 instructions per function. Computed values 0 through 124 become distinct x86-64 Linux process statuses. Unsupported programs reject without projection or fallback. Output-bearing AOT replaces the fixed loader probe with exact source-declared bytes. Dynamic I/O repeats native reads until EOF, rejects input byte 4,097, validates status before output, and reports that status as input-dependent. Borrowed helpers retain the same frame bounds and cannot return or store handles as scalar values. Fuel instruction 65,537 traps before an effect and before application output publication. Typed UTF-8 input uses strict RFC 3629 validity, scalar count, scalar, and width operations without locale or replacement. Helpers share all scalar global state, including status. One status writer must be reachable from the entry. The checked entry epilogue alone commits final process status. The status-73 fixture launches as a complete capsule-bound AOT ELF. General classical bytecode execution remains.

Deriving the profile and graph

Publish the accepted feature contract:

wheeler bootstrap-features \
  --profile bootstrap-1 \
  --output wheeler.bootstrap-features.yaml

Unknown profiles fail without output. Schema 1 contains exactly seventeen sorted version-1 features:

affine-borrows
boolean-scalars
bounded-loops
byte-output
byteview-input
checked-arithmetic
compile-time-constants
exhaustive-variants
fixed-scalar-array-fields
generated-inverse-proofs
module-linking
nominal-records
owned-regions
signed-scalars
static-calls
strict-utf8-input
word-buffers

Derive the compiler module graph from the canonical source archive:

wheeler bootstrap-modules \
  --source-archive wheeler.compiler.wpk \
  --output wheeler.bootstrap-modules.yaml

The module manifest names schema, profile, root, external modules, and every local module's canonical name, source path, source identity, and sorted imports. The checker requires unique paths, closed local imports, declared externals, rooted reachability, and an acyclic graph.

Schema ceilings are 10,000 local modules, 10,000 external modules, and 100,000 direct imports. The current native identity path accepts 512 local modules, 64 externals, 3,072 imports, and 262,144 input bytes, which covers the present compiler graph.

Options and limits

The accepted options record is:

schema: 1
compiler:
  profile: "bootstrap-1"
  source-maps: false

Source maps may be enabled only when normalized logical source identities enter canonical output.

The limits record is:

schema: 1
limits:
  source-bytes: 16777216
  tokens: 100000
  nesting: 256
  declarations: 10000
  symbols: 10000
  instructions: 1000000
  diagnostics: 1000
  heap-bytes: 268435456
  stack-depth: 1024
  steps: 10000000

Every value is a positive canonical integer no greater than 1,073,741,824. Both derivations must use the named limits. Hashing one file while executing another policy would make the provenance false.

Toolchain provenance

Each ordinary and diverse toolchain uses canonical wheeler.toolchain.yaml:

schema: 1
toolchain:
  kind: "independent-stage0"
  source: "<sha256>"
  builder: "<sha256>"
  dependencies: "<sha256>"
  environment: "<sha256>"

kind is recovery-seed, independent-stage0, or host-source. The remaining fields bind reviewed source, builder, closed dependencies, and normalized environment.

The category alone proves no independence. Promotion requires distinct complete provenance and compiler identities, followed by review of the derivations.

Seed ancestry

wheeler.seed.yaml binds one seed artifact to kind, target platform, output identity and length, source revision and identity, build command, working directory, builder, closed dependencies, environment, parent, and independent attestations.

Accepted kinds are alternate-stage0, recovery-release, system-toolchain, and opaque-root. An opaque root has no source or parent and must state origin, transport, acquisition date, and reason. Other kinds require source correspondence.

The seed-chain index uses SHA-256 identity of canonical record bytes. Every parent and attestation must be present. Parent walks must be acyclic. An attestation names the same source and output under a builder identity unused by the subject or another attestation.

This forms a closed evidence graph. It cannot transform an opaque root into source-derived bytes.

wheeler.recovery.yaml binds the graph, opaque-root totals, source archive, lock, options, limits, fixed-point result, diverse-compilation result, acceptance set, and parent recovery release. Validation rederives chain and opaque totals.

Evidence command

The final stage-0 gate is:

wheeler bootstrap-manifest \
  --source-archive wheeler.compiler.wpk \
  --source-lock wheeler.package.lock.yaml \
  --feature-manifest wheeler.bootstrap-features.yaml \
  --module-manifest wheeler.bootstrap-modules.yaml \
  --options-manifest wheeler.compiler-options.yaml \
  --limits-manifest wheeler.compiler-limits.yaml \
  --ordinary-toolchain ordinary-toolchain.provenance \
  --ordinary-compiler stage0.compiler \
  --ordinary-runtime stage1.runtime \
  --ordinary-verifier verifier.wbc \
  --stage-1 compiler-stage1.wbc \
  --stage-2 compiler-stage2.wbc \
  --ordinary-diagnostics ordinary.diagnostics \
  --diverse-toolchain diverse-toolchain.provenance \
  --diverse-compiler trusted.compiler \
  --diverse-runtime trusted.runtime \
  --diverse-verifier trusted.verifier \
  --diverse-output compiler-diverse.wbc \
  --diverse-diagnostics diverse.diagnostics \
  --acceptance-artifacts acceptance \
  --output wheeler.bootstrap.yaml

Every file argument names a physical nonsymlink file no larger than 16 MiB. Only the two diagnostic files may be empty. The acceptance directory contains a closed canonical artifact set and must include the compiler fixed point.

The command checks each input before and after reading, strictly decodes the compiler archive and lock, validates profile and graph closure, hashes every module source, independently decodes and re-encodes compiler artifacts, compares complete bytes and diagnostics, verifies distinct derivations, and rederives the acceptance-set identity. It never executes a candidate artifact.

Canonical bootstrap manifest

Schema 2 binds twenty-one lowercase SHA-256 identities:

schema: 2
source:
  archive: "<sha256>"
  manifest: "<sha256>"
  lock: "<sha256>"
  profile: "bootstrap-1"
  features: "<sha256>"
  modules: "<sha256>"
  options: "<sha256>"
  limits: "<sha256>"
ordinary:
  toolchain: "<sha256>"
  compiler: "<sha256>"
  runtime: "<sha256>"
  verifier: "<sha256>"
  stage-1: "<sha256>"
  stage-2: "<sha256>"
  diagnostics: "<sha256>"
diverse:
  toolchain: "<sha256>"
  compiler: "<sha256>"
  runtime: "<sha256>"
  verifier: "<sha256>"
  output: "<sha256>"
  diagnostics: "<sha256>"
acceptance:
  artifact-set: "<sha256>"

Construction enforces:

ordinary.stage-1 == ordinary.stage-2
ordinary.stage-1 == diverse.output
ordinary.diagnostics == diverse.diagnostics
ordinary.toolchain != diverse.toolchain
ordinary.compiler != diverse.compiler

These relationships remain evidence components. Review, reproducible host builds, strict verification, source comparison, and independent derivation complete the trust case.

Publication

A recovery candidate contains the compiler artifact, canonical source archive and lock, bootstrap manifest, every provenance input, and the closed acceptance set. Publication is content-addressed and all-or-nothing.

Cache paths, aliases, URLs, CI numbers, wall time, and usernames are transport details outside artifact identity. The bootstrap manifest is generated and never hand-edited. Losing a referenced provenance object makes the candidate unverifiable and ineligible for promotion.

The package appendix defines the archive, lock, repository, and artifact-set identities used here.