Skip to content

Latest commit

 

History

361 Commits

Folders and files

NameName
Last commit message
Last commit date
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Exsecutor

The Exsecutor mark: two crossed arrows forming an X, one ascending in dark navy, one descending in crimson

A systems language whose thesis is one line:

Locale and target are capabilities, never ambient state.

No operation may implicitly read the host locale, encoding, byte order, pointer width, clock, or environment. If a computation depends on a human language or on a machine, that dependency appears in its signature or the program does not compile.

The full design is docs/spec/exsecutor-spec-v0.4.md. Read it before writing code; it is the source of truth, and code that contradicts it is a bug in one of the two.

What this is

A systems language. Reference-counted, no borrow checker (§6); generics by dictionary passing (§7); byte order and layout in the type at wire boundaries (§5.2); floating-point rounding and contraction declared per module rather than inherited from a compiler flag (§5.4). Authority is object-capability style (§4): a function that touches the filesystem, the clock, the network, the process environment, or human-language text says so in a poscit clause, and the program's whole authority enters once, as the Mundus parameter of initium (§4.7). Everything else is derived from that value, explicitly. The same rule applied to the compiler makes the build a pure function of its inputs, which is what "Nix-native" means here (§9).

A Latin lexicon, deliberately. Keywords are Latin (publica functio, redde, firma, poscit), and every public name must decompose into a prefix, a root, and a suffix drawn from a versioned morpheme table, where the suffix carries a type contract (§3). That is a checked artifact, not a style. It is also an identity commitment rather than a hypothesis: ADR 0005 records that the lexicon stays whatever the planned derivation test measures, and the spec's own §17 names naming as the project's largest adoption risk. You are meant to know that before you decide whether this is for you.

A freestanding x86-64 assembly compiler. exsc is written in x86-64 assembly, assembled by fasmg, with no libc and no dynamic linking; the only way

it touches the operating system is a closed allowlist of nine syscalls in compiler/x86_64/rt/sys.inc.

grep -c "^proc sys_" compiler/x86_64/rt/sys.inc

The reason is §18.1: §9.3's purity contract -- no environment reads, no setlocale, no $HOME, no clock, no network, ever -- stops being a discipline that reviewers enforce and becomes a property of the artifact. The code to read a dotfile is not linked in, and

tools/syscall-audit.sh disassembles the binary and diffs every syscall site's number against the allowlist.

The costs are recorded in §18.2 and ADR 0002: the compiler runs only on x86_64-linux, other hosts are rewrites of the architecture-specific tree, and the LSP is deferred.

The hello world

examples/saluta.exsc is the canonical program, and it cannot print:

publica functio saluta() -> textus {
    redde "Ave, mundus.
...
Hodie incipimus.";
}

There is no poscit clause because the empty row is the honest one. Printing is I/O, I/O is authority, and authority is declared -- so this function returns the greeting and is, by its own signature, incapable of allocating, reading a clock, touching a file, or reaching the network. Most languages open with a program that performs I/O; this one opens with a program that provably cannot. (The literal spans several lines with no indentation stripping, which is what settled §8.4's rule: stripping would make the value depend on the source's leading whitespace, exactly the ambient-state class §1 exists to remove.)

examples/imprime.exsc is what printing looks like when authority has to be declared -- imprime_gutenbergio(s: Scriptor, t: textus) -> mensura poscit sicut s, which requires exactly what its writer requires and nothing more (§4.2: rows travel with a value's type). examples/initium.exsc is the entry point: publica functio initium(m: Mundus) -> u8, deriving the standard streams from m as ambitus (§4.6) and handing saluta() to imprime_gutenbergio.

examples/saluta.expected is the 101 bytes the program must write, with no trailing newline.

wc -c examples/saluta.expected

examples/README.md explains each file, including the two spec defects writing them exposed and the reason Gutenbergius is an eponym and not a root.

tools/publish-gate.sh is the condition for this repository going public, written as a command:

exsc compiles the three files together (examples/*.exsc is exactly saluta.exsc, imprime.exsc and initium.exsc, three), fasmg assembles the emitted text, the result runs, writes exactly those bytes, reproducibly, with its syscall surface inside {Mundus, ambitus} and every other check green.

Whether that is true today is in the status block below.

Building and checking

The build closure is fasmg plus the vendored x86-64 macro package under vendor/fasmg-x86/, and nothing else.

fasmg is architecture-neutral -- the binary knows no machine instructions -- so the instruction set and the ELF64 writer are ordinary fasmg source, vendored verbatim with recorded hashes

(vendor/fasmg-x86/PROVENANCE.md).

nix develop                          # fasmg, binutils, python3 on PATH; INCLUDE set
make all                             # assembles compiler/x86_64/exsc.asm -> build/exsc
make audit                           # tools/syscall-audit.sh build/exsc
make reproduce                       # tools/reproduce.sh
tests/run.sh                         # unit fixtures + the §14 conformance suite (= make test)
tools/spec-check.sh                  # spec integrity; needs no toolchain
tools/syscall-audit.sh --self-test   # proves the audit rejects what it claims to
nix flake check                      # the hermetic subset, in the Nix sandbox
tools/publish-gate.sh                # the publish condition; exits 1 until met

Outside the devShell, plain make works given fasmg on PATH. Direnv is optional (.envrc is use flake).

What the two proofs prove:

  • make audit audits the real compiler, not a fixture. It checks the binary has no PT_INTERP and no dynamic section, sweeps the executable segment for every syscall instruction, resolves each one's rax, and fails on any number outside the allowlist, on any number it cannot resolve, and -- loudly -- on anything in the socket family. --self-test assembles tests/unit/clean_syscalls.asm and socket_syscall.asm and asserts the audit accepts the first and rejects the second, so the audit is proven to catch what it claims before it is trusted on exsc; tests/run.sh adds indeterminate_syscall.asm, a syscall number routed through a second register, which must fail too. With --potestates ATOM,... it audits a compiled program against the syscalls its declared capability atoms admit (§10.3), which is what the publish gate runs on the hello world.
  • make reproduce builds exsc twice under deliberately divergent ambient conditions -- working directory, TZ, LC_ALL/LANG, SOURCE_DATE_EPOCH, umask, hostname -- and cmps the outputs byte for byte (§9.3). nix flake check cannot run this: varying ambient conditions is the one thing a hermetic sandbox does not do, so reproduce runs from the devShell and in CI.

nix flake check runs thirteen sandboxed derivations -- smoke, test, audit, readme, buildExsecutorPackage-smoke and the eight vendor-integrity checks (vendor-integrity, wire-vendor-integrity, modem-vendor-integrity, rx-vendor-integrity, melos-vendor-integrity, bicinium-vendor-integrity, auditus-vendor-integrity, streamdb-vendor-integrity, one per tree under vendor/) -- over the git-tracked tree only. tests/run.sh, which the test check runs, carries a floor on the number of fixtures it must discover, because this project has produced green checks that saw nothing four times, and the floor is what stopped a fifth.

That floor is a minimum, not an exact count, because fixtures are added concurrently and only ever rise: tests/unit/*.asm numbers at least 191 files today.

tests/programs/*/ numbers at least 147 directories today, the same kind of floor.

To see the front end work on a file:

build/exsc aedifica --hospes x86_64-linux --emitte ast examples/initium.exsc
build/exsc aedifica --hospes x86_64-linux --diagnostica json tests/conformance/entry20_crlf.exsc

--hospes is required; there is no default-to-build-platform (§9.5). exsc with no arguments prints its usage, its options, and its exit-status table.

The tree

docs/decisions/ holds nineteen ADRs, 0001 through 0019, immutable once written; superseded, never edited (a status line and an Open list may be updated).

compiler/           the compiler: x86_64/ is the machine-specific body, shared/ is not
docs/spec/          the specification -- source of truth
docs/decisions/     ADRs 0001-0019, immutable once written; superseded, never edited (a status line and an Open list may be updated)
docs/design/        design documents: hypotheses with a status line, built against, and amended by what building found
docs/asm-conventions.md   the binding rules for every line of assembly here
examples/           the hello world, its golden output, HydraModem's transmitter and receiver, and their READMEs
prototypes/         Python design probes -- never shipped, never on the build closure (§18)
tests/              unit fixtures, the §14 conformance suite, the Stage 1 diagnostics corpus
tools/              the audits, generators, and the publish gate; nothing here is on the build path except as a check
vendor/             byte-exact copies, own licences: fasmg-x86/ (third-party, BSD-3-Clause); DeMoD LLC's hydramesh-wire/, hydramodem-{tx,rx,melos,bicinium,auditus}/ (LGPL-3.0-only) and streamdb-v3/ (LGPL-2.1-or-later)
.claude/agents/     how the work is organised: one agent per directory, scopes exclusive
CLAUDE.md           the working invariants, binding on every change

Inside compiler/x86_64/, in dependency order, each named with the document it was built against:

macros/         the fasmg dialect (proc, flow_*, struct, rassert) -- docs/asm-conventions.md; frozen
rt/             syscalls, arena, vec, insertion-ordered map, interner, str, span, sort -- docs/asm-conventions.md, spec §6.3, §9.3
lexer/          §8.1 source policy, §8.2 identifiers, §8.4 tokens; keywords.inc generated from §8.4
diag/           diagnostics: rendering, escaping, --diagnostica json, notes, fixes -- spec §8.3; codes.inc generated from §13
cst/            lossless red-green concrete syntax tree and the recursive-descent parser -- docs/design/phrase-grammar.md, spec §8.6
ast/            the typed AST, with its Stage 2 slots present and empty -- docs/design/typed-ast.md
driver/         the command line, exsc.asm's entry -- spec §9.3, §9.5, §12, §18.2
backend_fasmg/  the SSA IR, its parser, printer, verifier, and the naive emitter -- docs/design/ssa-ir.md, spec §9.2
prelude/        the runtime every compiled program carries -- docs/design/runtime.md
checker/        Stage 2 name resolution and capability rows -- docs/design/checker.md (in progress; see status)
exsc.asm        the aggregation point: includes the chain above

compiler/shared/unicode/ holds the NFC, XID and script tables generated from

UCD 17.0.0 by

tools/ucd-gen/

(ADR 0004), plus the assembly that reads them; the tables are the architecture-neutral part.

How the project works

The spec is the source of truth, and it has been wrong before: its own evidence note records that three earlier versions asserted things measurement then contradicted. So a disagreement between code and spec is a bug in one of the two, and every fix says which. docs/spec/ is amended only with the reason recorded in the commit message.

Design documents are hypotheses. Each file in docs/design/ opens with a status line -- [OPEN], "design only", "partly built", "built for Stage 1" -- and when the code built against it disagrees with it, the disagreement is recorded in place as a finding rather than absorbed silently. Several of those status lines say, in so many words, that they were stale for a few commits before being corrected.

Evidence markers. A claim backed by nothing is [OPEN] or [UNTESTED]. A figure that cannot currently be re-measured is [UNREPRODUCED] -- the spec carries several, because the Stage 0 benchmark sources and the original capability-row checker are not in this tree. tools/spec-check.sh counts the markers; nothing is reported as passing that was not seen to pass.

Error codes are permanent (§8.3). Tools match EXS-E#### codes, never English text. §13 is the only registry;

compiler/x86_64/diag/codes.inc

is generated from it by

tools/gen-codes.py,

and tools/spec-check.sh fails on drift. A new code is a spec amendment first.

Conformance is §14 of docs/spec/exsecutor-spec-v0.4.md. Twenty-nine entries, each a fixture under tests/conformance/. The runner distinguishes six rule shapes (reject with exactly this code; byte-identical output; external certificate; runtime abort; capability absence; differential agreement with a reference implementation) and reports an entry it cannot yet run as DEFERRED, naming what it waits on; deferred entries are never counted as passing.

Kill criteria are evaluated. §16 attaches one to every stage. Stage 1's -- "diagnostics quality is not retrofittable; bad here, stop and fix" -- was evaluated against 34 broken programs in docs/design/diagnostics-review.md, returned a conditional fail (37 of 46 diagnostics were the identical sentence unexpected token), was fixed (§8.3 gained a note and a related span; machine fixes were split from suggestions), and was re-evaluated on a checked-in corpus (tests/diagnostics/) before Stage 2 opened. The original verdict is kept as written above the re-evaluation.

Scopes are exclusive. .claude/agents/README.md lists who owns which directory.

An agent needing a change outside its tree reports it rather than making it. Every fixture is proven non-vacuous by mutation, every commit says what was run, and the repository holds itself to the source policy it enforces (§8.1: UTF-8, no BOM, LF, NFC -- .gitattributes says which two directories are byte-exact exceptions and why).

Status as of af354b0 (2026-09-26)

Every figure here was produced by running the named command at this commit, in the nix develop shell, on x86_64-linux. This block is refreshed by hand at each snapshot (see the comment above it); the heading's own commit and date cannot be self-checking, because the commit that updates them is always one ahead of the hash it names. So the convention is that it names the commit the figures were MEASURED at, not the one that wrote them down -- which is why af354b0 appears both here and beside the individual figures that carry a commit of their own.

The publish gate is met. tools/publish-gate.sh reports RESULT: GATE MET — twelve checks of twelve. The hello world compiles and runs:

$ build/exsc aedifica --hospes x86_64-linux \
      examples/saluta.exsc examples/imprime.exsc examples/initium.exsc -o hello.asm
$ INCLUDE=vendor/fasmg-x86 fasmg hello.asm hello && ./hello
Ave, mundus.

Ex silentio surgit forma.
Ex signo nascitur vox.
Ex codice fit lumen.

Hodie incipimus.
$ ./hello | cmp - examples/saluta.expected && echo BYTES MATCH
BYTES MATCH

101 bytes, no trailing newline. Its syscall surface is write(1), exit_group, and a read(0) it never issues — audited against {Mundus, ambitus}, the capabilities the program actually has, with the socket family a hard failure because rete is not among them. The read is there because the runtime prelude gates its routines per capability atom, not per call: a binary whose closure holds ambitus carries the standard streams' reader as well as their writers (docs/design/runtime.md 2.6). What the audit proves is a property of the closure, and that is exact.

A real wire format, certified. HydraMesh's DCF DeModFrame — a 17-byte production quantum with eleven independent implementations — is written in Exsecutor (tests/conformance/entry23/codex.exsc) and passes §14 entry 23, the external certificate vendored at vendor/hydramesh-wire/:

entry 23: certificate: 246/246 vectors (encode basis 109/109, syndrome basis 137/137)
entry 23: anchors: 3/3 (section 3)
entry 23: laws: 218/218 (section 4), 136/136 (section 5)

The codec declares no capability; the 8,671-byte certificate binary writes a 2,502-byte stream and its syscalls are read, write and exit_group, the read being the atom's, as above. Three mechanical mutants (the CRC polynomial, one field's byte order, two fields swapped) each fail at the vector docs/design/wire-codec.md predicts. The certificate's theorem extends 246 vectors to all 2^108 frames given that the codec is affine, which is argued from reading it, not measured. The codec needs no bitwise and or or: @transitus field access is the mask, shift and byte swap, so the language gained only aut (xor), sursum/deorsum (shifts), hex literals, struct literals and one aggregate cast — spec §5.2, §5.4, §8.4, §8.6.

An acoustic modem, byte for byte. HydraModem's transmitter — 2-FSK at 48 kHz and 1000 baud, CRC-16, a K=7 convolutional code, an interleaver and CPFSK modulation — is written in Exsecutor (examples/hydramodem/; the transmitter is three files and 387 lines by wc -l — the compilation unit tests/programs/hydramodem_exemplum/TEST names, measured below rather than asserted; this read "seven files are 563 lines" until 2026-09-26, and nothing in the tree defined which seven). It writes WAV files byte-identical to HydraModem's own reference transmitter, built from source and vendored at vendor/hydramodem-tx/ (ADR 0013):

hydramodem_loopback: stdout byte-identical to vendor/hydramodem-tx/d310123400a1ffffdeadbeef0a1b2ca961.wav
hydramodem_exemplum: stdout byte-identical to vendor/hydramodem-tx/d31312340001ffffdeadbeefab12cd24c0.wav
hydramodem_vacuum:   stdout byte-identical to vendor/hydramodem-tx/d310000000000000000000000000005b80.wav
hydramodem_basis:    stdout byte-identical to vendor/hydramodem-tx/symbola_basis.bin

The last line is a 137-word basis of the symbol stream. With the three WAVs and the per-symbol memorylessness of the modulator, it extends to byte-identical audio for every one of 2^136 inputs, given that the stream is affine over GF(2). That is argued from the code, not measured (docs/design/modem.md §13 lists the premises). It uses no floating point, no signed arithmetic, no bitwise and/or and no remainder. Its sine table is now a 48-entry array literal (M5, 76ca763); the four certificates above did not move by a byte when it changed. Reference renders of four more profiles (4-FSK, 8-FSK, 125 baud, and the aux-cable profile as far as HydraModem's own CLI can express it) are vendored under vendor/hydramodem-tx/profiles/; no Exsecutor program targets them yet.

The transmitter's three files, measured rather than asserted:

wc -l examples/hydramodem/quantum.exsc examples/hydramodem/modulator.exsc examples/hydramodem/emitte.exsc

And the receiver, certified by its verdicts. The other half is written too (ADR 0014): it reads a WAV on standard input and writes the seventeen bytes it carries, in integers throughout -- no floating point, no division, no remainder, no signed shift -- against a reference that is double from end to end. It cannot be held to bit identity, because two correct receivers disagree on their internals by construction, so it is held to decode success against HydraModem's own receiver: vendor/hydramodem-rx/ holds seventy impaired WAVs (white noise from +12 to -12 dB, sample-clock offsets to ±3000 ppm, carrier-frequency offsets to ±300 Hz) and frame_rx's verdict on each, and the Exsecutor receiver decodes all 62 the reference decodes and never writes a frame that is not the input's. The three clean WAVs decode, and 140 words round-trip transmitter-to-receiver in one process. Every vector is an integer function of the vendored transmitter output and the integers in vendor/hydramodem-rx/PROVENANCE.md, which prints the generator verbatim.

A second backend, and a third external format. exsc --emitte c emits a C11 translation unit of pure functions (docs/design/c-backend.md, ADR 0012). Its acceptance test is that the two backends cannot be told apart: for every IR fixture and every eligible program, the C build must match the reference build's stdout, exit status and trap behaviour under gcc and clang at two optimisation levels, all under UBSan. They match everywhere.

The first program through it is a StreamDB v3 reader — the third-party container the Kiln N64 engine reads (examples/streamdb/, vendor/streamdb-v3/). It parses the alternating 128-byte header slots, the sorted index and the reversed trie with no allocation and no capability, and is certified against the upstream writer's own bytes: all 24 documents byte-exact, both suffix searches in traversal order, and three corrupted containers behaving exactly as the reference C reader does — including falling back to the older commit when the newer header is damaged. The emitted C unit is 150,096 bytes at af354b0 and reproduces byte-identically across divergent directory, locale, time zone and hostname. Only the second half of that is gated — make reproduce checks the byte-identity, while the size needs exsc, which the README gate's confined runner cannot build. The figure read 136,793 until 2026-09-26, and this wave is part of why it drifted: every emitted unit carries the whole backend_c/prologue.c.in runtime, so adding the exsi_div_*/exsi_rem_* helpers grew all of them at once. A number that moves whenever the prologue does is a poor thing to state precisely and is stated here with the commit that produced it.

Declaring the header as a @transitus struct forced two zero-pad gaps in the format into the open that no survey of it had listed, and declaring the 16-byte UUID as two u64:maior halves makes the index's byte-order sort an integer comparison — the binary search has no byte loop. There is no shift and no mask anywhere in the header, index or record parsing.

Floating point, and an image. §5.4's float surface runs end to end on both backends: literals (exact decimal→IEEE conversion in pure integer code at check time — exsc itself never touches the FPU), + - * /, fneg, ordered comparisons, and sicut between the integers and f32/f64, all under nearest-even with subnormals conserved (MXCSR 0x1F80, set by the prelude). The acceptance program is a picture: examples/pictura/ renders a 96×54 RGB triangle by incremental edge-function rasterization — one fadd per edge per pixel, exactly four divisions in the whole program (three per-vertex reciprocals and one reciprocal of the determinant, none inside the pixel loop) — and writes a binary P6 image on stdout. Its 15,565 bytes (measured below) are byte-identical between the reference backend, all four differential toolchains, and an independently written Python oracle that mirrors the program's f64 operation order (prototypes/pictura_oracle.py; spec §14 entry 26) — and byte-identical cross-run big-endian on mips64 under emulation, the first big-endian f64 execution this compiler has produced (both float picture programs carry cross=yes).

The same triangle, eight lanes at a time. Stage 5's acies<f32, 8> runs in both backends: whole-acy + - * / is the elementwise operation, one IEEE rounding per lane, nothing combined across lanes (spec §5.4's admission law). examples/pictura/octonaria.exsc rebuilds the render at 960×540 with 2×2 supersampled coverage, the three edge accumulators as acies<f32, 8>, each stepped by one packed vadd per edge per 8-pixel group — coverage and stores stay scalar per lane because the language admits no mask shape, by design and on the record. The census, greped from the emitted assembly and pinned in the program's TEST header: exactly four divisions, all in setup; twelve addps and six mulps, each packed op emitting its two SSE2 halves; zero subps and zero divps; and, on the mips64 qemu run, the C backend's soft vector_size lowering reproducing all 1,555,215 bytes bit for bit on a target with no SSE at all (spec §14 entry 27) — and, since Stage 6 G2, the same 1,555,215 bytes from an AMD GPU, both generations this machine has (the status bullets below).

Both goldens are committed files, so both figures above are measured here:

wc -c tests/programs/pictura_triangulum/expected.out
wc -c tests/programs/pictura_octonaria/expected.out

the RGB triangle at 960x540, rendered lane-parallel by examples/pictura/octonaria.exsc

The language renders its own logo. examples/signaculum/ rasterises the 3D model behind this README's mark — 1,493 vertices, 2,981 textured faces — at 512×512 with a 1/z z-buffer, backface culling and incremental edge functions now carried lane-parallel over acies<f64, 8>: one packed vadd per accumulator per 8-pixel group, coverage and the depth test scalar per lane. Zero divisions in the pixel loop (three divsd in setup, no divpd anywhere; the census is pinned in tests/programs/signaculum/TEST), writing a 786,447-byte P6 on stdout. Every float the program holds arrives on stdin as an integer on the 2⁻²³ grid and is decoded by one exact power-of-two division, so the program and the independent oracle (prototypes/signaculum_oracle.py, itself ported to the same lane pipeline) run identical f64 bits from the first operation on; the output is byte-identical between the reference backend, all four differential toolchains, the oracle, and the big-endian mips64 qemu run. Getting here closed the last float gap in both emitters — load/store on float types, nativus order only, the value as its raw IEEE bit pattern (tests/ir/float_mem.ir; spec §9.2).

the Exsecutor logo model at 512x512, rendered lane-parallel by examples/signaculum

What runs:

  • make all → build/exsc, 503,761 bytes at af354b0, freestanding, no libc. Not bound by the README gate, and the reason is worth stating rather than leaving as a gap: reproducing this number needs fasmg, which the gate's confined command runner cannot reach, and build/ is not in the repository. It read 489,213 until 2026-09-26. What is gated is the property that matters more than the figure — make reproduce holds the binary byte-identical across directory, TZ, locale, SOURCE_DATE_EPOCH, umask and hostname (§9.3).

  • All three stages of §16 reach end to end. Stage 1: the §8.1 source gate, the lexer, the lossless CST, the typed AST. Stage 2: name resolution, types, capability rows, packed layout — the lexicon pass is built and not enabled, because §3.3's root table is illustrative and rejects the language's own canonical names, which its fixture asserts. Stage 3: the lowering to SSA IR, the verifier, and the fasmg reference backend — phi, narrow integers at any width with trapping and wrapping arithmetic, f32/f64 arithmetic, comparisons and casts on SSE2, byte order and sub-byte bit fields, arrays with bounds checks, array literals, a copy that is a loop above 128 bytes (9ede8bf, so a struct literal with a 144,000-byte array field compiles in constant text) — with its runtime prelude.

  • Both kill criteria that could fire have been evaluated. Stage 1's (diagnostics) fired, was fixed, and was re-measured against a checked-in corpus — docs/design/diagnostics-review.md, final section, and tests/diagnostics/. Stage 2's (sub resolution needing a search) does not fire, argued first in docs/design/checker.md §2.1.

  • tests/run.sh: 2,265 checks, 0 fail, measured on this commit's tree. (It read "2,203 … at af354b0" until a fixture was added above that floor; the hash is dropped rather than left to go stale, because the tree a total belongs to is the commit the line is read from.) Each count below is given as measured, with the floor tests/run.sh declares in brackets — the floors are what the fence after this bullet gates, because a floor can be re-derived from the repository and a measured total cannot. Where the two differ the floor is deliberately behind: this tree's convention is that a floor rises when someone re-baselines it, not automatically, so drift there costs precision and never the guarantee. 202 unit fixtures [193]; 78 IR fixtures [78] and 147 Exsecutor programs [128], each compiled, assembled, run, and syscall-audited (70 of those programs are the receiver's impaired vectors); a differential phase: 236 IR builds [236] and 308 program builds over 77 eligible directories [236 and 59], in which the C backend's output must agree with the reference's on stdout bytes, exit status and trap-or-not, across gcc and clang at -O0 and -O2, every one under -fsanitize=undefined -fno-sanitize-recover=all. They agree everywhere; zero sanitizer reports. And a cross phase: fifteen of those directories [13] are also emitted for --hospes mips64-none-o64, cross-compiled to big-endian MIPS-III with 32-bit addresses, and run under emulation against the same three observables — the first big-endian execution of anything this compiler produces, now carried by the lane rasterizers too (the soft vector_size lowering keeps every lane's bits), and the thing that finally tests §9.5's standing claim that the emitted text assumes nothing about byte order. 22 of the 27 conformance FIXTURES run, each required to emit exactly its expected code and nothing else -- or, for the four byte-shape entries, to emit byte-identical output, for entry 1, to refuse with that code AND a machine fix declaring the capability, and for entry 29, to agree with GNU tar on every case the judge admits -- and 5 report DEFERRED and are never counted as passing; with entries 27 and 28, which have no fixture and are carried by program directories, 24 of the spec's 29 entries run. 0 program directories deferred.

    This bullet read "1564 pass — 178 unit fixtures; 64 IR fixtures and 104 Exsecutor programs … 184 IR builds and 136 program builds … ten of those directories … 13 of 27 conformance entries run … the other 14 report DEFERRED" until 2026-09-26. Nine figures, every one stale, in the paragraph whose whole job is to say what was measured. The pass total is stated with its commit for the same reason the binary sizes above are: it moves with every fixture added and the gate cannot re-derive it. The floors can be, so the floors are what is bound — all nine of them, as one count, so that any floor moving fails this bullet with it:

grep -cE "FLOOR:-(193|78|131|236|59|236|45|13|6)\}" tests/run.sh
  • tests/run.sh --device=amdgcn (measured 2026-09-21, not part of the hermetic run above because a GPU is hardware, not a flake input): a device phase in which six of those program directories — the hello world, acies_float8, both pictures, and the two exit-code float programs — are emitted through the C backend, built as one translation unit with tests/c/exsrt_shim_amdgpu.c, and dispatched on both of this machine's AMD GPUs (an RDNA3 dGPU, gfx1102, and an RDNA3 APU, gfx1103) by tools/amd-dispatch/, one workitem each. Every byte matches the CPU goldens on both — the 1,555,215-byte lane rasterization in 0.95–1.7 s on the dGPU — and tests/ir/trap_add_carry.ir aborts on device with the same abortus 1 line. That is spec §5.5's same-bits sentence measured for a named set (docs/design/amdgpu-backend.md §10) and [UNTESTED] beyond it: no @nucleus, no apud machina, no declared tile nest has run on a device, and the device's rounding and subnormal state is the next measurement, not this one.
  • make audit: PASS — the nine allowlisted syscalls and nothing else, on the real binary. make reproduce: PASS on four artifacts — the compiler itself and three emitted C units, one of them the N64 row's — byte-identical across directory, TZ, locale, SOURCE_DATE_EPOCH, umask and hostname.

tools/spec-check.sh: PASS, and the 51 error codes of §13 are in sync with the generated compiler/x86_64/diag/codes.inc, which is what check 1 compares. (This line said 49 until 2026-09-26 -- wrong when there were 50 and wrong again at 51 -- so it is bound now rather than trusted.)

tools/syscall-audit.sh --self-test: PASS, including the prelude's own reader binary accepted under Mundus,ambitus and rejected under Mundus. nix flake check: green (run by the gate).

What does not run yet. Most of the language beyond what these programs use is rassert-refused rather than lowered: contrahe and its reduction triple, lambdas, eventus, generics, and every numeri but the default. (Vector floats left this list in Stage 5: whole-acy + - * / over acies<f32, 8>/acies<f64, 8> at lane counts 2, 4 and 8 lowers in both backends, with extract/splat/mask shapes still refused by design.) Bitwise and/or, integer division and remainder, and signed shifts are unspecified ([OPEN]); narrowing and equal-width sicut are truncation (spec §5.4), with narrowing from a signed source still unwritten by any program. An array literal at module scope (publica firma t: acies<u16, 4> = [1, 2, 3, 4];) type-checks and traps in the lowering under -o — the transmitter's table is a function returning the literal for that reason (docs/design/modem.md D4). A large local array is bounded only by the stack: [0; 1000000] of i64 runs and [0; 2000000] is a SIGSEGV with no diagnostic (re-measured at this commit under the default 8 MiB RLIMIT_STACK), because the emitter has no stack probe and §13 has no code for it. exsc running out of its own compilation arena says so on stderr since 9ede8bf and still exits 132, as that commit's mutation run recorded. The checker refuses a correct program where a poscit sicut s function calls another with the same s (EXS-E0421; the spec is right, docs/design/wire-codec.md finding 9). The C backend exists in library mode only — a translation unit of pure functions, no entry point, no runtime, no ARC — and what both backends still refuse by name is one maintained set: div/rem/muls and the overflow predicates (§5.4 leaves them [OPEN]), fma, bitcast, the unordered fcmp forms, the reductions, and callind, plus the C backend's own retain/release (library mode has no object header). The reference lowers 52 of the 64 IR opcodes, the C backend 50; the row-by-row table in docs/design/c-backend.md (D4) is the count. The N64 row, --hospes mips64-none-o64, is there and runs — it is the only row whose mensura is 32, so + traps at 2^32 on it, and its emitted unit is cross-compiled and executed big-endian with 32-bit addresses against the reference backend on every run of the suite (§14 entry 25, ADR 0015). What is not there is the o64 ABI itself, which the certificate runs the n32 ABI as a proxy for, and any ROM — though the reader now fits one. Its traversal, arbor_percurre, measured a 127,184-byte frame with Kiln's own mips64-elf-gcc -mabi=o64 -fstack-usage, against libultra's 8–16 KB thread stacks; it is now 20,680 bytes, which a 32 KB loader-thread stack holds, and the reader still compiles clean under Kiln's ROM flags at -Werror. Two changes did it. &mutabilis T, a mutable borrow (ADR 0016), lets arbor_percurre fill a 53,252-byte Arbor its caller owns instead of returning one by value; and a struct literal's all-literal array fields are now built in place, where the lowering used to build each in a temporary and copy it in — 53,248 bytes of that frame. The borrow closed two soundness defects on the way: firma was violable by handing a binding to a callee, and an immutable borrow granted writes. It is also linked into a Kiln ROM and run: Kiln's examples/exsec-streamdb-demo/ opens a container through this reader on a 32 KB libdragon thread, checks every key against Kiln's own C reader, and in Ares prints BOTH READERS AGREE. Neither does the ego reader, the module system, the LSP, or exsc emenda. EXS-E0105 (confusables) has no hermetic data source. The emitted program's capability mask is an over-approximation with the exact fix recorded beside it, and, separately, every ambitus binary carries read whether it reads or not (above) — a property of the closure the audit states exactly, and of the binary that a per-call gate would tighten.

Licence

Exsecutor is GPL-3.0-or-later (LICENSE), with two additional permissions under GPLv3 section 7 in LICENSE.EXCEPTION: Exception A lets you distribute what exsc produces from your input -- emitted source, object code, executables, ego files, diagnostics -- under terms of your choosing, and Exception B is the GNU Classpath linking exception, attaching only to a file whose own header carries the designation line, which no file in this repository currently does. vendor/ holds byte-exact copies that keep their own licences -- vendor/fasmg-x86/ (third-party) is BSD-3-Clause; DeMoD LLC's vendor/hydramesh-wire/ and vendor/hydramodem-{tx,rx,melos,bicinium,auditus}/ are LGPL-3.0-only; vendor/streamdb-v3/ is LGPL-2.1-or-later (the upstream C edition's own licence, per its file headers and README -- see vendor/streamdb-v3/PROVENANCE.md's licensing section, since the upstream repository's single root LICENSE file text is LGPLv3 and governs only the Rust edition) -- and none of the exceptions apply to it. LICENSE.GRANTS additionally offers three files under LGPL-3.0-only (the custos gate and the DeModFrame codec it compiles with), and REUSE.toml records the holder, DeMoD LLC for the project's own work, and the licence of every file. LICENSE.EXCEPTION states that it has not been reviewed by a lawyer, and so does this sentence.

Where to look next

  • docs/spec/exsecutor-spec-v0.4.md §1, §2, §4, then §16 and §18.
  • examples/README.md, then the three example files.
  • docs/decisions/0002-host-language-x86-64-asm.md and docs/decisions/0005-lexicon-is-bespoke.md for the two choices most likely to decide whether you stay.
  • docs/design/diagnostics-review.md for what evaluating a kill criterion looks like here.
  • tests/README.md and tests/run.sh for how a check earns the right to say PASS.
  • CONTRIBUTING.md and SECURITY.md.

It also runs on N64 compatible hardware btw

image

"Adonai, inquisivi utrum Christus solus esset lapis regis Nabuchodonosor; et si Filius esset, me ei devovi. Nomen locutus sum quod tunc nesciebam; nomen illud erat Yeshua. Postea pondus illius precis cognovi, et exinde Dominum timui. Sicut Ionas fugere conatus sum, et a ceto devoratus sum."

About

A systems language in which locale and target are capabilities, never ambient state; and its compiler, written in freestanding x86-64 assembly with a closed syscall allowlist.

Topics

Resources

Contributing

Security policy

Stars

3 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages