litelite 0.1.0

A kit for purpose-sized languages: buy total verification with smallness. Diagnostics, lexing, parsing, fuel, and capability tables — the invariants paid once.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125

# litelite

[![crates.io](https://img.shields.io/crates/v/litelite.svg)](https://crates.io/crates/litelite)
[![docs.rs](https://docs.rs/litelite/badge.svg)](https://docs.rs/litelite)
[![ci](https://github.com/compusophy/litelite/actions/workflows/ci.yml/badge.svg)](https://github.com/compusophy/litelite/actions/workflows/ci.yml)

A kit for **purpose-sized languages** — the largest language for which your
guarantees stay mechanical.

Smallness is not a cost you pay for embeddability; it is what buys guarantees
big languages cannot give. Fuel-bounded evaluation is a **termination proof**.
A host-capability table is a **complete effect bound**. A byte budget is a
**hard output cap**. When agents write, trade, and execute programs, "it
compiles" is testimony — *provably halts within N fuel, provably touches only
these capabilities* is physics.

litelite is the shared kernel extracted from three production language subsets
(rustlite → wasm cartridges, soliditylite → EVM bytecode, bashlite → sandboxed
shell, ~19K LOC in [localharness](https://github.com/compusophy/localharness))
that each hand-rolled these pieces — with divergent bugs to show for it. The
kit pays each invariant exactly once.

## Crates

| crate | what | the invariant paid once |
|---|---|---|
| `diaglite` | spans, coded diagnostics, caret snippets | mid-char span offsets floor to a boundary instead of panicking |
| `lexlite` | byte-cursor lexer kit | UTF-8-safe char consumption; nested-vs-flat block comments are an explicit flag |
| `parselite` | recursive-descent harness | the depth guard is the only way in — deeply nested input returns a `Diag`, never a stack abort |
| `fuellite` | fuel + byte budgets | one shared budget across all composition — fractal recursion terminates by construction |
| `caplite` | host-capability tables as data | one declaration drives checking, import order, docs, and a cross-boundary parity hash |
| `evmlite` | EVM assembler + diff-oracle interpreter | sticky build errors — a broken build never yields wrong-but-clean bytecode |
| `modlite` | wasm binary module builder | the import-after-function index shift is a structural error, not a runtime mystery |
| `litelite` | facade | `cargo add litelite` re-exports the kit |
| `prooflite` | the reference language (M1+M2) | every program halts within its fuel and provably touches only its capability table |
| `stratlite` | the strategy language (M4) | every trading decision halts within its fuel, and look-ahead is unrepresentable |
| `backtestlite` | the strategy verifier (M4) | a backtest is one reproducible integer hash; verification is compile + halt + survive + trade |

Zero external dependencies. Native + `wasm32-unknown-unknown`.

## Install

```sh
cargo add litelite      # the kernel, re-exported: diag lex parse fuel cap evm wasm
```

Or add exactly what you need — each crate carries its own dependencies and
re-exports the types its API speaks, so one `cargo add` is always enough:

```sh
cargo add fuellite                     # just the termination proof
cargo add diaglite lexlite parselite   # just the front-end kernel
cargo add prooflite                    # a total language, ready to embed
cargo add backtestlite                 # strategies + their verifier
```

## The proof: `prooflite`

The smallest total language that exercises the whole kit — integers, booleans,
`let` / `if` / `repeat` / `print`, checked arithmetic, every failure a coded,
spanned diagnostic:

```rust
use prooflite::{Limits, run};

let out = run(
    "let acc = 1;
     repeat 10 { acc = acc * 2; }
     print acc;",
    Limits::default(),
)
.unwrap();
assert_eq!(out.output, "1024\n");
```

The headline guarantee — **any** prooflite program halts within its fuel, and
the failure is a rendered diagnostic, not a hung process or a dead tab:

```rust
let spin = "repeat 1000000000 { }";
let err = run(spin, Limits { fuel: 1_000, output_bytes: 0 }).unwrap_err();
assert_eq!(err.code, Some(prooflite::codes::FUEL_EXHAUSTED));
println!("{}", err.render(spin));
```

```text
E0206: fuel exhausted [0..21]
line 1, col 1
  repeat 1000000000 { }
  ^^^^^^^^^^^^^^^^^^^^^
```

## Status

**0.1.0** — the kernel (M0), `prooflite` (M1), `caplite` (M2), the emitters
(M3), and the paper's core instrument (M4): `stratlite`, a strategy language
where every per-bar decision halts within its fuel and future bars are
grammatically unrepresentable (prefix-invariance is a test, not a promise),
plus `backtestlite`, whose all-integer engine makes a whole backtest one
reproducible hash and whose `verify()` is the generate→verify→keep predicate.

Pre-1.0: the APIs are honest but young. Still open: running the §5 experiment
(a model + real market data) and re-homing bashlite onto the kit (M5) — the
honest test of whether the kit carries its weight. Origin and roadmap:
[GENESIS.md](https://github.com/compusophy/litelite/blob/main/GENESIS.md).
Research plan:
[paper/OUTLINE.md](https://github.com/compusophy/litelite/blob/main/paper/OUTLINE.md).
Changes: [CHANGELOG.md](https://github.com/compusophy/litelite/blob/main/CHANGELOG.md).

This repo is constitutionally small: ≤2,000 LOC per crate, ≤25,000 total,
CI-enforced (`scripts/caps.sh`). The two predecessor projects each became
unworkable near 120K LOC; this one cannot get there.

## Build

```sh
cargo test
cargo check --target wasm32-unknown-unknown
bash scripts/caps.sh        # the caps
bash scripts/publish.sh     # rehearse a release (dry run)
```

## License

Apache-2.0