Rustdis

mkdir rustdis && cd rustdis
overplane init
overplane sandbox build
overplane spec new   # 001-resp-server.md
overplane spec new   # 002-strings-keyspace.md
overplane spec new   # 003-expiration.md
overplane spec new   # 004-collections.md
overplane spec new   # 005-concurrency-performance.md
overplane spec new   # 006-ir-property-tests.md
overplane spec new   # 007-model-checking.md

overplane build all

---
id: '#0001'
title: RESP Server Core
status: active
tags: [core]
---

# RESP Server Core

## Goal

Create a Rust Cargo project in the working directory that builds a single
binary called `rustdis`: a wire-compatible Redis clone. This spec covers the
RESP2 protocol layer and the TCP server shell. The runtime must use only the
Rust standard library — no external crates in `[dependencies]` — so the result
is one small binary with zero runtime dependencies. (Dev-dependencies for
testing are allowed and arrive in a later spec.)

## Requirements

* CLI: `rustdis [--port N] [--bind ADDR]`, defaulting to `127.0.0.1:6379`.
  `rustdis --help` prints polished, colorized usage. `rustdis --version`
  prints the version.

* RESP2 protocol, both directions, as its own module with a clean boundary:
  - Parse client requests as RESP arrays of bulk strings, plus the inline
    command format (a bare line like `PING\r\n`) for telnet compatibility.
  - Serialize simple strings, errors, integers, bulk strings (including null),
    and arrays (including nested and null).
  - The parser must be a pure, panic-free function from bytes to
    `Result<Command, ProtocolError>`: malformed input never panics and never
    kills the connection loop. Enforce sane limits (max bulk length 512 MB,
    max array elements 1M) with clean RESP errors.

* Commands in this spec: `PING [msg]`, `ECHO msg`, `QUIT`, and a stub
  `COMMAND` (and `COMMAND DOCS`) that returns an empty array so `redis-cli`
  connects without complaint. Unknown commands get
  `-ERR unknown command 'name'`. Command names are case-insensitive.

* Startup banner on stderr: name, version, bind address, with tasteful ANSI
  color. Log one concise line per connection accept/close. Keep stdout clean.

* Structure for growth: a `Command` enum, a dispatch table, and a storage
  module boundary that later specs extend.

## Acceptance

- `cargo build --release` succeeds with an empty `[dependencies]` section.
- With the server running, `redis-cli -p 6379 PING` returns `PONG`,
  `redis-cli ECHO hello` returns `hello`.
- `printf 'PING\r\n' | timeout 2 nc 127.0.0.1 6379` (inline command) returns
  `+PONG`.
- Malformed bytes (e.g. `printf '*1\r\n$4\r\nPING'` truncated, or random
  garbage) never crash the server; the connection is answered with a RESP
  error or closed cleanly.

---
id: '#0002'
title: Strings & Keyspace
status: active
tags: [core]
---

# Strings & Keyspace

## Goal

Give `rustdis` its keyspace: binary-safe string values with Redis-compatible
command semantics, exact reply types, and exact error messages where Redis
documents them.

## Requirements

* String commands: `GET`, `SET` (with `EX`, `PX`, `NX`, `XX`, `GET` options),
  `SETNX`, `GETSET`, `MGET`, `MSET`, `APPEND`, `STRLEN`, `GETRANGE`,
  `INCR`, `DECR`, `INCRBY`, `DECRBY`.

* Keyspace commands: `DEL`, `EXISTS` (variadic, counts duplicates), `TYPE`,
  `KEYS pattern` (glob: `*`, `?`, `[...]`, `\` escape), `DBSIZE`, `FLUSHDB`,
  `FLUSHALL`, `RANDOMKEY`, `RENAME`, `SELECT` (accept index 0 only; other
  indexes get `-ERR DB index is out of range`).

* Semantics to match Redis exactly:
  - Keys and values are arbitrary byte strings (binary-safe, no UTF-8
    assumption anywhere in the data path).
  - `INCR` family: values are parsed as signed 64-bit integers;
    non-numeric values answer `-ERR value is not an integer or out of range`;
    overflow answers `-ERR increment or decrement would overflow`.
  - `SET key val NX` on an existing key returns null bulk; `XX` on a missing
    key returns null bulk; otherwise `+OK`.
  - Wrong-type operations (arriving with later specs' types) answer
    `-WRONGTYPE Operation against a key holding the wrong kind of value`.
  - Wrong arity answers `-ERR wrong number of arguments for 'cmd' command`.

## Acceptance

- A `redis-cli` session exercising each command above against `rustdis` and
  against a real `redis-server` (both are installed in the sandbox) produces
  byte-identical replies for a scripted command list; commit that script as
  `compat/compat.sh` and make `compat/compat.sh` runnable against any port.
- `redis-cli SET k v NX` twice: first `OK`, second `(nil)`.
- `redis-cli INCR k` on a non-integer value returns the documented error.

---
id: '#0003'
title: Expiration
status: active
tags: [core]
---

# Expiration

## Goal

Add Redis-compatible key expiration to `rustdis`: per-key absolute deadlines,
TTL introspection, lazy expiry on access, and an active background sweep.

## Requirements

* Commands: `EXPIRE`, `PEXPIRE`, `EXPIREAT`, `PEXPIREAT`, `TTL`, `PTTL`,
  `PERSIST`. `SET` with `EX`/`PX` uses the same machinery; plain `SET` on an
  existing key clears any TTL (Redis semantics). `GETEX` with
  `EX`/`PX`/`PERSIST` options.

* Semantics to match Redis exactly:
  - `TTL`/`PTTL` return `-2` for a missing key, `-1` for a key with no TTL.
  - `EXPIRE` with a non-positive timeout deletes the key immediately and
    returns `1`; `EXPIRE` on a missing key returns `0`.
  - Expiry deadlines are absolute monotonic-clock instants computed once at
    set time; a key past its deadline is indistinguishable from a missing key
    to every command (lazy expiry), regardless of whether the sweeper has
    collected it yet.

* Active expiry: a background sweep that samples keys with TTLs and removes
  expired ones, bounded so it never stalls foreground traffic. Document the
  chosen sampling strategy in a code comment referencing how Redis does it.

* Invariants (these will be verified against the IR in a later spec):
  - A key never resurrects: once expired, no read may observe the old value.
  - `PERSIST` then any delay never expires the key.
  - TTL is monotonically non-increasing between writes to the key's TTL.

## Acceptance

- `redis-cli SET k v PX 100`, then `GET k` after 200 ms returns `(nil)` and
  `TTL k` returns `-2`.
- `redis-cli SET k v EX 100; PERSIST k; TTL k` returns `-1`.
- `compat/compat.sh` is extended with an expiration section and still
  produces byte-identical output against real `redis-server` (allowing a
  tolerance mechanism for timing-dependent TTL remainders).

---
id: '#0004'
title: Collections
status: active
tags: [core]
---

# Collections

## Goal

Extend the `rustdis` value model beyond strings: lists, hashes, and sets,
with Redis-compatible reply shapes and edge-case behavior.

## Requirements

* Lists: `LPUSH`, `RPUSH`, `LPOP`, `RPOP` (with optional count), `LLEN`,
  `LRANGE` (negative indexes, out-of-range clamping), `LINDEX`, `LSET`,
  `LTRIM`.

* Hashes: `HSET` (variadic field/value pairs), `HGET`, `HMGET`, `HDEL`,
  `HGETALL`, `HEXISTS`, `HLEN`, `HKEYS`, `HVALS`, `HINCRBY`.

* Sets: `SADD`, `SREM`, `SISMEMBER`, `SMEMBERS`, `SCARD`, `SPOP` (optional
  count), `SINTER`, `SUNION`, `SDIFF`.

* Semantics to match Redis exactly:
  - Deleting the last element of a collection deletes the key: an empty
    collection is never observable (`EXISTS` returns `0`, `TYPE` says none).
  - All collection commands on a key of the wrong type answer the standard
    `-WRONGTYPE` error; `TYPE` reports `list`, `hash`, `set` correctly.
  - `LPUSH`/`RPUSH` return the new length; `SADD` returns the number of
    members actually added; `HSET` returns the number of new fields.
  - Expiration from the previous spec applies uniformly to every type.

* Keep the storage module's type dispatch table-driven so the IR's
  entity/variant structure maps visibly onto the code (one value enum,
  one variant per type).

## Acceptance

- `compat/compat.sh` gains list/hash/set sections and still produces
  byte-identical output against real `redis-server` (sort set replies where
  Redis ordering is unspecified).
- `redis-cli RPUSH l a b c; LRANGE l 0 -1` returns a, b, c;
  `LPOP l 3` empties the list and `EXISTS l` then returns `0`.
- `redis-cli HSET h f1 v1 f2 v2; HGETALL h` returns all pairs;
  `SADD s a b; SADD s b` returns `1`.

---
id: '#0005'
title: Concurrency & Performance
status: active
tags: [performance]
---

# Concurrency & Performance

## Goal

Make `rustdis` fast under real load. Choose the concurrency architecture by
measurement, not fashion, and make the server a first-class `redis-benchmark`
target.

## Requirements

* Concurrency architecture, chosen empirically (still std-only):
  - Candidates: (a) thread-per-connection over a sharded store,
    (b) a fixed worker pool over a sharded store, (c) a single-threaded
    event loop. Prototype at least two, measure with
    `redis-benchmark -t set,get -n 100000 -c 50 -P 16` in the sandbox, keep
    the winner, and record the numbers and the decision in `ARCHITECTURE.md`.
  - The store must be sharded (hash-partitioned across N locks or N owned
    shards) so writes scale on multi-core; a single global mutex is
    unacceptable.
  - The expiration sweeper from spec #0003 must respect the chosen
    architecture (no global stop-the-world).

* Pipelining: many commands per read buffer must be parsed and answered
  in order without per-command syscalls; responses are batched per read.
  This is what `redis-benchmark -P` exercises.

* `redis-benchmark` compatibility: implement enough of `CONFIG GET`
  (`save`, `appendonly` — return standard stub values), `INFO` (at least
  `server`, `clients`, `memory`, `stats` sections with honest values),
  `DEBUG JMAP`/`DEBUG SLEEP` may be rejected, but `redis-benchmark`'s
  default and `-t set,get,incr,lpush,rpush,sadd,hset` suites must run to
  completion.

* Performance bar, measured in the sandbox against the real `redis-server`
  installed there (same machine, default configs, `-n 100000 -c 50`):
  `rustdis` must reach at least 70% of Redis's requests/sec on `SET` and
  `GET`, both unpipelined and with `-P 16`. Record the comparison table in
  `ARCHITECTURE.md`.

## Acceptance

- `redis-benchmark -t set,get,incr,lpush,rpush,sadd,hset -n 100000 -c 50 -q`
  completes against `rustdis` with zero errors.
- `ARCHITECTURE.md` contains the measured candidate comparison and the
  final rustdis-vs-redis table meeting the 70% bar.
- `redis-cli INFO server` shows `rustdis` identity fields alongside
  Redis-compatible field names (`redis_version` present for tool compat).

---
id: '#0006'
title: IR-Derived Property Tests
status: active
tags: [verification]
---

# IR-Derived Property Tests

## Goal

Turn the formal IR that Overplane raised from specs #0001–#0005 into an
executable property-based test suite. The IR directories are mounted
read-only at `/ir/<spec-file>/` (`ir.yaml`, `consistency.smt2`); treat them
as the authoritative source of properties — do not invent properties that
have no IR node, and do not skip IR nodes that are runtime-checkable.

## Requirements

* Add `proptest` (latest 1.x) as a dev-dependency only; `[dependencies]`
  stays empty.

* Traceability is the point. Create `tests/ir_properties.rs` where every
  property test is named `prop_<spec>_<ir_node_id>` (e.g.
  `prop_0003_no_resurrection`) and carries a doc comment quoting the IR
  node's `description` and assertion. Cover every `invariant`, `constraint`,
  and `rule` node from the IR of specs #0001–#0005 that is checkable at the
  library level; list any node that is not runtime-checkable (e.g. purely
  visual or timing-hardware ones) in a `SKIPPED` table in
  `VERIFICATION.md` with a one-line reason each.

* Required property classes (all derived from IR nodes):
  - RESP round-trip: for arbitrary commands built from arbitrary binary
    keys/values, serialize → parse is the identity, and the parser never
    panics on arbitrary byte input (fuzz-style property over raw bytes).
  - Model-based command sequences: generate random sequences of commands
    (across strings, expiry, lists, hashes, sets) and run them against both
    the real store and a naive reference model (`BTreeMap`-based, written
    for clarity not speed); the observable replies must be identical. Use a
    virtual clock so expiry properties are deterministic.
  - Expiry invariants: no resurrection after expiry, `PERSIST` durability,
    TTL monotonicity — as stated in the #0003 IR.
  - Collection invariants: empty collections are never observable; type
    errors are total (every command × wrong-type combination answers
    `-WRONGTYPE`).

* The store and protocol layers must be testable in-process (no TCP) via a
  library-level API; refactor if needed, without changing the binary's
  behavior.

* `VERIFICATION.md` documents the full verification story: the IR → SMT
  consistency check that already ran at build time, the IR-node → property
  mapping table (node id, property name, one-line description), the SKIPPED
  table, and how to run everything.

## Acceptance

- `cargo test` passes; the proptest suite runs at least 256 cases per
  property by default.
- Every runtime-checkable IR node id from specs #0001–#0005 appears either
  in `tests/ir_properties.rs` or in the `VERIFICATION.md` SKIPPED table —
  no third bucket.
- Reverting the spec #0003 "plain SET clears TTL" behavior by hand makes
  `prop_` tests fail (spot-check that the suite has teeth; describe the
  mutation you tried in `VERIFICATION.md`).

---
id: '#0007'
title: Model Checking the Core
status: active
tags: [verification]
---

# Model Checking the Core

## Goal

Go beyond sampling: use the Kani model checker to *prove* — for all inputs up
to a bound, not just tested ones — that the pure core of `rustdis` cannot
panic and that key IR invariants hold. Kani was chosen over KLEE (research-
grade Rust support, pinned old toolchains) and Lean (proves a hand-translated
model, not this code); record that rationale in `VERIFICATION.md`.

## Requirements

* Add Kani proof harnesses under `src/` behind `#[cfg(kani)]` (they must be
  invisible to normal builds and `cargo test`). Name each harness
  `verify_<spec>_<ir_node_id>` mirroring the proptest naming so the three
  verification layers (SMT / proptest / Kani) line up in the mapping table.

* Harnesses to include, derived from the IR:
  - RESP parser total safety: for any byte buffer up to a fixed bound
    (e.g. 64 bytes), parsing never panics and either yields a command or a
    `ProtocolError` (#0001's parser purity/panic-freedom node).
  - RESP length-prefix arithmetic: no overflow for any advertised bulk/array
    length (bounded).
  - TTL arithmetic: deadline computation never overflows and preserves
    ordering for any `EXPIRE`/`PEXPIRE` argument (#0003 TTL monotonicity
    node, bounded).
  - Integer command arithmetic: `INCRBY`/`DECRBY` overflow detection is
    exact — errors if and only if the mathematical result exits i64
    (#0002's overflow node).

* Bounds and any `kani::assume` preconditions must be stated in doc comments
  with a one-line justification.

* Tooling: `verify.sh` at the project root installs Kani if absent
  (`cargo install --locked kani-verifier && cargo kani setup`) and runs
  `cargo kani`. Add the harness list and expected `VERIFICATION SUCCESSFUL`
  output to `VERIFICATION.md`. If Kani cannot complete inside the sandbox,
  the harnesses must still be committed and `verify.sh` must work on a
  standard Linux host; note the attempt's outcome in `VERIFICATION.md`.

## Acceptance

- `cargo build --release` and `cargo test` are unaffected by the harness
  files ([dependencies] still empty; `kani` appears nowhere in Cargo.toml —
  attributes are cfg-gated only).
- `verify.sh` runs `cargo kani` and every harness reports
  `VERIFICATION:- SUCCESSFUL` on a host with Kani available.
- `VERIFICATION.md`'s mapping table now has three columns per IR node:
  SMT (build-time), proptest, Kani — with `—` where a layer does not apply.