codexzig is one program. Codex source in, zig out.
codexzig < prog.codex 2> prog.zig
That is the whole artifact. This repository builds it, and checks the one property that makes it trustworthy.
This is the highlight, and it is checked into the repository. Everything
under generated/ is emitted by the build — nothing there is source — but
that is exactly why it is worth reading: you can see what this transpiler
actually produces without running anything.
Start with generated/arith.zig. It is the
transpiled form of samples/arith.codex, and the build
compiles and runs it on every pass. The program is the first 79 lines; the
fixed runtime prelude follows it, behind a banner that says so. Here is eight
queens, in Codex:
q-solve : List Integer -> Integer
q-solve (placed) = if list-length placed == 8 then 1 else q-rows 1 placed
and the zig that came out:
fn q_solve(placed: *CxList(i64)) i64 {
return @as(i64, (if ((cx_list_len(placed) == 8)) 1 else q_rows(1, placed)));
}That one is a plain translation. The interesting ones are where it is not.
q-ok recurses on itself in the source; the emitter turned the self-call
into a loop:
fn q_ok(row: i64, placed: *CxList(i64), i_: i64) bool {
var _tl_i = i_;
while (true) {
if ((_tl_i == cx_list_len(placed))) { return true; } else { ... }
}
}twice triple 7 — a function passed to a function — comes out as
triple(triple(7)), with the higher-order call gone. And a bounded field,
v : Integer between 0 and 100 clamping, becomes
std.math.clamp(250, 0, 100).
Text literals look like "\x14\x0d\x17\x17\x10..." because Codex Text
is CCE-encoded; that one is hello, world.
The transpiler itself is in the same directory, as
generated/codexzig.qemu.zig — 2.3 MB of zig,
which is the whole Codex compiler plus the emitter, and again the program runs
first with the prelude underneath. It is what zig build-exe turns into a
working codexzig in two seconds.
That layout is a change we made to the emitter rather than something it did already: it used to open every file with ~800 lines of prelude and start the program past line 840. Zig does not order declarations at container scope, so moving it is inert — verified by hand-editing an emitted file before touching the plug, and confirmed after by the fixed point.
One loop:
blob -> QEMU -> zig -> exe -> (the same source again) -> zig -> diff
codexzig is built the long way, because the seed compiler emits x86 and not
zig: the seed compiles the transpiler's own source to IR under QEMU, the zig
emitter — itself compiled to a bootable kernel — turns that IR into zig, and
zig build-exe turns the zig into a binary.
Then that binary is handed the same source, and must emit the same bytes.
generated/codexzig.qemu.zig pass 1 — the emitter running under QEMU
generated/codexzig.native.zig pass 2 — the emitter running as the binary pass 1 built
-> byte-identical, or it is a finding
Said as a property: the emitter emits the same bytes for its own source whether it runs on bare metal or as a native binary. That single comparison exercises every chapter of the compiler and the whole emitter, and it costs a minute against the seven the build already spent. It is not a test suite and not a comparison against a reference implementation; it is an invariant, and it either holds or it does not.
It is not a proof of correctness. It says two independent runs of the same emitter, through two different compiler backends, produce the same bytes.
The obvious way to fake it would be a "transpiler" that emits a program which
just prints its input back — a quine trick. This one isn't, and you can check
rather than believe: every build transpiles samples/arith.codex, compiles
the result, runs it, and compares all nine lines against
samples/arith.expected. It prints 42, 92, 610 and 5050, none of which
appear in that program's source, and 92 comes out of a backtracking search.
The zig is above.
Pass 2 is handed the same source as pass 1, not the same blob bytes. A blob is that source wrapped in the guest's intake envelope, and the envelope is what makes QEMU answer with IR text rather than an x86 binary; the native binary reads plain Codex on stdin and would choke on the mode line.
That source is the unit: the bundle with what the checkout's
build/compile.ps1 would resolve ahead of it, which for a complete bundle is
Foreword ListUtils and Tuple, because for desugars to map-list and a tuple
to MkTup<N>. It is written into the bundled file itself, so both passes read
it.
| why | ||
|---|---|---|
$COBBLESTONE_ROOT |
a Cobblestone checkout | every chapter is read from here; nothing is vendored |
qemu-system-x86_64 |
any recent | the seed and the emitter run on bare metal |
zig |
0.16.0 | builds the emitted zig into the binary |
pwsh |
at ~/.local/pwsh/pwsh |
the checkout's own bundler is PowerShell |
| a quiet box | ~4 GB free RAM | see Memory below; nothing here takes a lock, and two guests thrash rather than fail |
| time | ~7 min cold, 3 s warm | measured: 3 guests in 366s, zig 2s, pass 2 58s; a warm run skips all of it |
$COBBLESTONE_ROOT is deliberately not $CODEX_ROOT. That one belongs
to the codex-zig-ladder, which moves its checkout's HEAD between branches and
pinned Updates all day as part of how it works. Point this at a checkout that
stays where it is put:
git -C <cobblestone> worktree add --detach ~/showell_repos/cobblestone-pin <rev>
CODEX_MEM_MB caps the guest (default 3072; the seed dies silently above
it on an 8 GB box). CODEX_ACCEL selects the accelerator (default tcg).
export COBBLESTONE_ROOT=~/showell_repos/cobblestone-pin
./build.py # build what is stale, then check the fixed point
./build.py --force # rebuild every stage, guests included
./build.py --check-only # check the fixed point against what is on disk
This is the requirement most likely to bite, because a guest that runs out
of room does not say so. It parks in hlt with nothing on the wire, having
already done minutes of real work, and looks identical to a slow compile. The
only evidence is its peak resident size beside its cap, which build.py
prints per stage and records in generated/PROVENANCE.
What each stage actually touches of the 3072 MB cap, measured (build.py
prints it per stage and records it in generated/PROVENANCE):
| stage | peak | |
|---|---|---|
| 2 | compile the ring plug — 304 KB in | 568 MB |
| 4 | compile the transpiler — 2.9 MB in, 9.9 MB of IR out | 2454 MB |
| 5 | transpile it — 9.9 MB of IR in, 2.3 MB of zig out | 916 MB |
| guest cap | 3072 MB (CODEX_MEM_MB); stage 4 uses 80% of it |
| host, to build | ~4 GB free — one guest at a time, plus zig |
host, to run codexzig |
3472 MB on its own 2.9 MB source |
Stage 4 is the binding one and its margin is thinner than it looks: 618 MB.
That last row is a real requirement and not a footnote. Transpiling a large
program is expensive because the allocator underneath is a bump allocator
that never frees, so peak demand is the sum of every phase's working set
rather than the largest. codexzig on its own source peaks at 3,553,024 kB —
and note that 2454 + 916 = 3370 lands right beside it, which is the same fact
seen from the other side.
The guest cannot simply be made bigger. The boot stub sets its stack from
a RAM-size cell and triple-faults on a value it cannot use: 3072 MB boots,
3584 MB and 3968 MB both die before READY, with QEMU exiting before a byte of
the banner. guest.py refuses a size at or above 4096 MB outright, because
the cell is four bytes wide and 5120 MB silently becomes 1024.
The obvious simplification is to put the compiler and the emitter in one kernel, so the bootstrap becomes compile codexzig to a kernel, then use it to transpile codexzig. That kernel was built and it is real — 1,971,047 bytes, compiled clean.
It does not fit, and the numbers leave no room to argue:
guest at 3072 MB boots, and runs every stage of the real build
guest at 3584 MB dies before READY
guest at 3968 MB dies before READY
the workload wants 3472 MB, measured natively
Merged, one guest holds the source, the AST, the IR and the emitted text at once, over an allocator that never frees — so its peak is the SUM of every phase's working set. The boot stub triple-faults on a RAM size it cannot use, putting the ceiling between 3072 and 3584, and the merged workload wants 3472. There is no guest size that is both bootable and big enough.
Splitting the front end from the emitter splits that peak across two processes, and that is what the third guest buys. It is not a historical accident, even though that is how it got here.
You do not need any of the above. generated/codexzig.qemu.zig is in this
repository, and it is the whole program:
zig build-exe generated/codexzig.qemu.zig -femit-bin=codexzig
./codexzig < prog.codex 2> prog.zig
Two seconds, no QEMU, no PowerShell, no checkout. That is why the repository tracks the zig and not the 28 MB executable — which zig does not build reproducibly anyway.
build.py prints its provenance before it spends anything, names each stage
as it runs, and marks the three that start a guest. It exits non-zero if the
fixed point breaks.
build.py the driver: eight stages, three of them guests
guest.py bare metal -- QEMU, the serial ring, the gdbstub
cobblestone.py where the sister checkout is, and which one it is
source/ the parts that are ours: two chapter lists and three Codex chapters
samples/ arith.codex and its expected output -- transpiled, built and
run on every build, so the artifact is checked doing real work
generated/ everything the build emits, tracked, including the binary
and the exact blobs bare metal ate -- see generated/README.md
docs/ how the pipeline works, and what the fixed point does not cover
Deliberately absent: any Codex source from Cobblestone (read from
$COBBLESTONE_ROOT), and the two-process codexir | zigemit pipeline that
codexzig merges (it lives in the ladder, which is where the questions it
answers are asked).
- Cobblestone — Damian's self-hosted language, compiler and OS. The compiler, the zig plug, and the seed all come from here. This repository is downstream of it and vendors none of it.
- codex-zig-ladder — the verification ladder. It compiles the compiler two ways and requires the answers to agree, across fourteen rungs, against bare metal. That is a comparison machine, and it is where defects in the zig plug get found and reported. This repository holds one invariant, and is deliberately much smaller.
The distinction matters when deciding where work goes. If the question is "does the zig backend agree with bare metal", it belongs in the ladder. If the question is "does this one program still reproduce itself", it belongs here.