# sysp

An experiment in an **AI-first systems language**: a small language designed for a loop in which a
model writes the code, the toolchain checks it, and a human reviews and steers. The language's job
is to make a model's typical failures — overflow, bounds, ownership, broken invariants — cheap to
catch, locally and mechanically, and to explain them in a form a program can act on.

The **benchmark came first** and decides what the language becomes (see the
[constitution](.specify/memory/constitution.md)).

## What exists (feature 001)

- **Benchmark**: 24 small systems tasks (`bench/tasks/`), from `clamp` and `binary-search` to a
  ring buffer, a bump allocator and a protocol state machine; since 040 also strict decoders
  (UTF-8, LEB128, base64), an overflow-checked dot product and a free-list pool; since 048 a
  table of open files. Each has a prompt, a C header, hidden tests, a C reference, a sysp
  reference and a sysp stub. Since 043,
  three are changes instead: a working program in each language (a hash map, an arena, a gap
  buffer) and a request to change it; a sysp change is also read for the guarantees (`requires`,
  `ensures`, struct invariants) of the program it changed that it no longer states. The scorer compiles any candidate,
  runs the tests under UBSan and ASan with a time limit, and reports PASS or why not.
- **sysp core**: typed s-expressions with parameter modes (`own`, `ref`, `mut`), linear ownership
  of buffers, a mandatory `effects` clause, `requires`/`ensures`, loop invariants, quantified specs,
  and typed holes (`?name`).
- **Verifier**: symbolic execution with Z3. Every index, every arithmetic operation and every
  contract is proven or the program is rejected, with a counterexample.
- **Diagnostics as an API**: stable codes, spans, obligations, counterexamples and fixes, as JSON
  (`--json`) or text rendered from it.
- **C11 backend**: verified programs compile warning-free under `-Wall -Wextra -Werror` (gcc and
  clang) with no runtime checks.
- **Model loop**: runs a model through write → check → repair on every task, in sysp or C, with
  identical rules, and records every attempt.

Status: C references 24/24, sysp references 24/24; 17 of 17 seeded bugs in the references are
rejected by the verifier. The model runs are recorded in `specs/039-first-run/results.md`,
`specs/040-hard-tasks/results.md` and `specs/041-unstated-traps/results.md`.

## Freestanding mode (feature 002)

For writing an operating system:
- `extern fn` declares functions implemented in assembly. Their contracts are trusted, and every
  build lists them (W002).
- An `io` effect, string literals, and `replace` for moving owned values in and out of slots.
- Several files can be checked as one program.
- `sysp build --freestanding` emits C without libc.

Its first user is the sibling project [sysk](../sysk), a kernel written in sysp that boots on
RV64 in QEMU.

## Spec predicates and rely/guarantee (features 003, 004)

- `(pred name ((x T) ...) body)` names a specification, so an invariant is written once.
- `(spec name ((x T) ...) R (decreases m) body)` is one of any scalar type, which may call itself
  (071): z3 knows it by its definition, unfolded once where it is used, and a buffer argument is
  its slice, so `(dec-value (view t k n))` survives writes beside it. sysl's `text-dec` and
  `scan-dec` are proven to write and read a number's value this way. Only a function that names
  one unfolds it (075): to the others it is an unknown value, so callers pay nothing for it; and
  only at the applications its own text makes, not those in a callee's postcondition (078).
  `(opaque spec ...)` hides one from other files as an opaque `pred` is hidden (093), so a byte
  format's laws cost its callers nothing.
- A call changes of a `mut` argument only what the callee may write (097), read from its body and
  its callees': a field it never writes keeps its value with no frame in its contract, and a loop
  around the call keeps it too. On sysf, 686 million units of z3's work became 149.
- `(secret key (field s w))` and `(declassify result)` say what a function keeps secret and what it
  makes public (102): checked before any proof, a secret reaches no branch, loop bound, index,
  division or extern, and ends only where named, through callees as their bodies allow. sysc's
  corpus: its 42 keyed functions pass, its 6 mistakes are refused.
- `(layout name size (field kind offset) ...)` declares a record of bytes once (104): sysp writes
  its struct, put and get and proves both laws (a get after a put gives the record back; what a get
  accepts was a put's writing), each field an opaque spec to callers, which pay almost nothing.
- `(lemma name ((x T) ...) (requires c) (ensures c) (decreases m) body)` is a proof a function
  calls for its ensures (090): proven as a function, by induction when it calls itself with a
  smaller measure, and no code.
- `(x (shared T R))` marks state that other tasks (or interrupt handlers) may change, only in the
  ways the predicate `R(before, after)` allows. Shared state is touched only inside
  `(atomic ...)`, which runs with interrupts off. The verifier assumes interference between atomic
  blocks, proves that each block keeps `R`, and proves that `R` is reflexive and transitive.
  sysk's preemptive scheduler is verified this way.

## Words (feature 017)

`i64` and `u8` are numbers: arithmetic is exact and overflow is an error. Words, `w8` `w16` `w32`
`w64`, are bit patterns: `& | ^ ~ << >>`, `rotl` and `rotr` by any amount modulo the width
(070), and `+ - *` modulo 2^n. `as` is the only bridge and it proves the value fits. Words are
SMT bit-vectors and numbers stay integers, because no encoding
of bitwise operators on integers was fast enough (`specs/017-words/plan.md` has the measurements),
so each theory does what it is good at. Shifts by the width or more are rejected (V013), never
undefined behaviour in C.

```lisp
(fn set-bit ((m w32) (i i64)) w32
  (effects)
  (requires (and (<= 0 i) (< i 32)))
  (ensures (!= (& result (<< 1 i)) 0))
  (| m (<< 1 i)))
```

## Character literals (feature 020)

`(== c #\()` instead of `(== c 40)`: a byte written as its character, typed by where it is used
like any integer literal. It changes no meaning, so the constitution (0.4.0) admits it on
readability: a wrong ASCII code verifies just as well as the right one, so only the reader can
catch it, and only if the code names the character. sysk's text code uses them (sysk 021).

## Constants (feature 021)

`(const page (* 4 kib))`: a name for an integer literal, defined once at top level and used
anywhere, in code and contracts, with the type its use gives it, as the literal would. The
parser puts the literal in place of the name, so nothing after it changes, and every message,
which quotes the source, shows the name. No binding may take a constant's name, so a name never
means two things. Constitution 0.5.0 admits constants as the program's own spelling of a
literal: a number written once cannot drift between copies that never meet in a proof. sysk
names its device addresses, sizes and bounds with them (sysk 025).

```lisp
(const plic-base 0xc000000)
(const plic-end (+ plic-base 0x400000))
(private const status 0x70)
```

## Tables (feature 048)

`(buf S)` for a struct of plain data: one buffer of rows instead of a buffer per field held to
one length, or records packed into bytes at computed offsets. A row's field is read as
`(. (get b i) f)` and set in place with `(set (. (get b i) f) v)`. The verifier keeps one array
per field (the component-as-array model of Burstall and Bornat), so a write to one field leaves
every fact about the others standing; a struct's invariant holds for every row at function
boundaries, and `buf-new`, which makes rows of zeros, proves a zero row keeps it. In C a table
is an array of the struct. A row's field may be lent or swapped, and the rows may be resources
(081): made by `buf-of`, or by `retype` with the rows in memory the caller has (085), ended row by
row by `buf-end`, which gives the memory back, never copied.

```lisp
(struct Chan (queued i64) (ended bool))

(fn drain ((chans (mut (buf Chan))) (c i64)) unit
  (effects)
  (requires (and (<= 0 c) (< c (len chans))))
  (ensures (== (. (get chans c) queued) 0))
  (set (. (get chans c) queued) 0))
```

## Retype (feature 064)

`(retype (buf U) b)` gives back an owned buffer's memory as rows of another type, nothing
copied: an allocator's bytes as words or a table, and back. `(size-of T)` is C's `sizeof`. The
bytes must be whole rows. Rows of bits (integers, words, structs of these without an invariant)
may be any bytes, and the verifier carries only zero across, both ways; other rows (a `bool`, an
enum) come only from bytes proven zero, as rows of zeros. The prior art is Rust's `bytemuck` and
`zerocopy`.

```lisp
(fn words ((b (buf u8))) (buf w32)
  (effects)
  (requires (== (len b) 64))
  (ensures (== (len result) 16))
  (retype (buf w32) b))
```

## Requirements

- Racket 8.10+ (`brew install --cask racket`)
- Z3 4.12+ on `PATH` (`brew install z3`), or set `SYSP_Z3` / pass `--z3`
- z3's checks share slots with every sysp you run on the machine, one per processor, in
  `/tmp/sysx-z3-UID`: a check waits for one, so several sessions proving at once share the
  processors instead of crowding them (047). The z3 `SYSP_Z3` names, if another machine's, has
  slots of its own: `SYSX_Z3_SLOTS` of them (`SYSX_Z3_SLOTS_DIR` to put them elsewhere), which
  describe that z3's slots, or without `SYSP_Z3` the PATH's (059, 063)
- a C11 compiler (`cc`)
- for the freestanding tests, a clang with an RV64 target (`brew install llvm lld`): `clang` on
  `PATH`, or set `CLANG`, as sysk's and sysi's tests read it

## Use

```sh
make                 # compile the Racket modules
make test            # all test suites (raco test tests)
make bench-refs      # score the C and sysp reference solutions

bin/sysp check FILE.sysp [--json]     # check + verify, diagnostics as text or JSON
                                      # (--report FILE: JSON to FILE, text printed; also build)
bin/sysp build FILE.sysp -o out.c     # C11 output (only if everything is proven)
bin/sysp build --no-verify ...        # C from a program checked but not proven, and said so (062)
bin/sysp check --cache DIR FILE...    # keep proofs in DIR; prove again only what changed (016)
                                      # (z3's answers kept by each check, 060, 094; --cold reads none)
bin/sysp check --work-max N FILE...   # a function's budget of z3's work, 50000000 by default: V016 (059, 061)
                                      # (--work-allow FILE: those allowed; --check-work N: one check's bound,
                                      #  3000000 for a check of a path alone, when lower: 099)
bin/sysp fmt [-w | --check] FILE...   # canonical formatting
bin/sysp layout [--json] FILE...      # each layout's table of bytes, from its declaration (109)

bin/bench score --lang c|sysp [--solutions DIR] [--tasks a,b] [-v]
bin/bench loop --model anthropic:MODEL_ID --lang sysp --attempts 4   # needs ANTHROPIC_API_KEY
bin/bench summary bench/results/RUN...
```

The first real experiment: run `bench loop` with the same model and attempt budget for
`--lang c` and `--lang sysp`, then compare with `bench summary` (solved counts, attempts to
solve, tokens per solved task).

## A taste

```lisp
(fn binary-search ((a (ref (buf i64))) (key i64)) i64
  (effects)
  (requires
    (forall ((i i64) (j i64)) (=> (and (<= 0 i) (<= i j) (< j (len a))) (<= (get a i) (get a j)))))
  (var lo 0)
  (var hi (len a))
  (while (< lo hi)
    (invariant (and (<= 0 lo) (<= lo hi) (<= hi (len a))))
    (let mid (/ (+ lo hi) 2))
    ...
```

```
$ bin/sysp check binary-search.sysp
binary-search.sysp:17:17: error[V004]: `(+ lo hi)` may overflow i64
    obligation: (and (<= -9223372036854775808 (+ lo hi)) (<= (+ lo hi) 9223372036854775807))
    counterexample: a = [-9223372036854767445,-9223372036854767445,-9223372036854767445,-9223372036854767445,-9223372036854767445,-9223372036854767445,...], lo = 4611686018427387904, hi = 4611686018427387905, len(a) = 4611686018427387905, key = -9223372036854767443
    fix: inside a loop the verifier knows only the invariants about variables the loop changes: add an invariant that implies this obligation, or rewrite the expression so the invariants suffice
FAILED: 1 error(s), 0 hole(s), 14/15 obligations proven
```

The fix is `(+ lo (/ (- hi lo) 2))`, which is what the reference solution does.

## Layout

```
sysp/        compiler: reader, formatter, checker, verifier (smt.rkt drives z3), C backend, CLI
bench/       tasks/, include/ (C ABI), scorer, model loop, summaries, results/
docs/        reference.md — the whole language in ~5.5k tokens; also the model's system prompt
             ideas.md — ideas discussed and parked, with the case for and against
             research.md — features to consider, scored, with their prior art
tools/       docs.rkt (the site's facts; the reviews are the root's tools/docs.rkt, 053), examples.rkt;
             host.rkt — another part's host/host.sysp run on the host behind a record shim, for
             its tests (051), held to the work budget but for what the part's work.allow lists (065);
             `#:on 'iss` runs it built by sysi on sysr's ISS instead, the same records (072); its
             sizes are the program's rec-max and out-size, and harness.sysp says rec-hdr once (073)
tests/       rackunit suites; corpus/ has one program per diagnostic code
specs/       spec-kit feature specs (001: spec, plan, research, contracts, tasks)
.specify/    spec-kit configuration and the constitution
```

Work is driven through [spec-kit](https://github.com/github/spec-kit): constitution → specify →
plan → tasks → implement, one numbered feature directory per change.

## Related

`../agent-lisp` is a sibling experiment (a persistent, model-editable program between an agent and
its tools). Its main lesson shaped this project: a language showed no benefit when nothing went
wrong, so measure against baselines and under failure, and report counts.