# 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**: 13 small systems tasks (`bench/tasks/`), from `clamp` and `binary-search` to a
  ring buffer, a bump allocator and a protocol state machine. Each has a prompt, a C header, hidden
  tests, a C reference, a sysp reference and a sysp stub. The scorer compiles any candidate,
  runs the tests 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 15/15, sysp references 15/15; 17 of 17 seeded bugs in the references are
rejected by the verifier. **No model runs have been recorded yet** — that is the experiment this
all exists for.

## 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.
- `(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: `& | ^ ~ << >>`, 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)
```

## Requirements

- Racket 8.10+ (`brew install --cask racket`)
- Z3 4.12+ on `PATH` (`brew install z3`), or set `SYSP_Z3` / pass `--z3`
- a C11 compiler (`cc`)

## 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
bin/sysp build FILE.sysp -o out.c     # C11 output (only if everything is proven)
bin/sysp check --cache DIR FILE...    # keep proofs in DIR; prove again only what changed (016)
bin/sysp fmt [-w | --check] FILE...   # canonical formatting

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
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.