# Li — curated handbook for agents> Fetch https://docs.lilangverse.xyz/llms.txt first if you only need the map.> Read verification/provability-gaps.md before claiming what lic build proves.

<!-- source: for-agents.md -->

# For agents and chats

This handbook is for people and for agents. Do not scrape the HTML. Fetch the markdown.

## Start here

| File | What it is |
|------|------------|
| [llms.txt](https://docs.lilangverse.xyz/llms.txt) | Curated index. Fetch this first. |
| [llms-full.txt](https://docs.lilangverse.xyz/llms-full.txt) | The same core pages, concatenated. |
| [raw/](https://docs.lilangverse.xyz/raw/) | One page at a time, as Markdown. Example: [raw/guide/hello-world.md](https://docs.lilangverse.xyz/raw/guide/hello-world.md). |
| [robots.txt](https://docs.lilangverse.xyz/robots.txt) | Allows crawlers; points at `llms.txt` and the sitemap. |

HTML lives at the same path without `raw/` and without `.md`. GitLab source of truth: [li-langverse/lic-docs](https://gitlab.lilangverse.xyz/li-langverse/lic-docs).

## Read before you claim what Li does

1. [Provability gaps](verification/provability-gaps.md) — **today** vs **target**. `lic build` is not a Lean certificate yet.
2. [Agent handover formats](ecosystem/agent-handover-formats.md) — how Li expects agents to work in a repo.
3. [li-agent-manifest.toml](ecosystem/li-agent-manifest.toml) — commands to run (`lic check`, `lic diagnose`, tests).
4. [Documentation style](contributing/documentation.md) — do not invent features; do not skip the gap register.

## Suggested ingest

```text
1. GET https://docs.lilangverse.xyz/llms.txt
2. If the task is small, GET the linked raw/*.md pages you need.
3. If the task is “learn Li” or you have budget, GET llms-full.txt.
4. Before writing code or promising proofs, GET raw/verification/provability-gaps.md.
```

In a clone of this repo, read `docs/` directly. Do not paste secrets, tokens, or `.env` files into a chat.

## What not to do

- Do not treat the styled HTML as the source. The source is Markdown.
- Do not say `lic build` runs Lean or closes all proofs unless the gap page says that row is closed.
- Do not copy ten-page tables from the design spec into a prompt when a link will do.
- Release notes and daily reports are optional; they are not in `llms-full.txt` on purpose.

## Related

- [Language handbook](language/overview.md)
- [Hello world](guide/hello-world.md)
- [LLM-first design (research)](superpowers/specs/2026-05-16-li-llm-first-design.md)
- [Diagnostic schema](schemas/diagnostic-v1.json)


<!-- source: getting-started.md -->

# Getting started

This page orients you in the repository. For a friendlier walkthrough, start with the [Guide](guide/hello-world.md).

## What Li is

Li is a compiled language for scientific and systems programming where **only provable programs build**. You write readable code with small promises (`requires`, `ensures`, `decreases`); `lic build` checks them before producing a binary.

## Install

See [Getting started — tools](guide/getting-started-tools.md) for macOS, Linux, and Windows notes.

## First commands

```bash
./scripts/build.sh
./build/compiler/lic/lic build examples/hello.li -o hello
./hello
```

## Learn by example

| Goal | Page |
|------|------|
| Hello world | [guide/hello-world.md](guide/hello-world.md) |
| SIMD + parallel | [guide/fast-math-and-parallelism.md](guide/fast-math-and-parallelism.md) |
| More snippets | [guide/examples-gallery.md](guide/examples-gallery.md) |

## Go deeper

| Topic | Page |
|-------|------|
| All types and features | [language/overview.md](language/overview.md) |
| Compile pipeline | [compiler/build-pipeline.md](compiler/build-pipeline.md) |
| Mathematical provability | [compiler/why-provable.md](compiler/why-provable.md) |
| Tests & security | [testing/overview.md](testing/overview.md) |

## Repository layout

```
li/
  compiler/     # lic — lexer, types, MIR, LLVM
  runtime/      # Small C runtime (print, OpenMP driver, …)
  std/          # Standard library (.li)
  examples/     # hello, tetris, …
  benchmarks/   # Physics & perf harness
  li-tests/     # All automated tests
  docs/         # This documentation
```

## Implementation order

Follow the [master plan](superpowers/plans/2026-05-14-li-master-plan.md) — do not skip the Lean verification phases for release builds.


<!-- source: guide/hello-world.md -->

# Hello world

Li programs are made of **procedures** (`def`). Each function states what it needs, what it guarantees, and how it stops.

## Minimal program

```nim
def main() -> int
  requires true
  ensures result == 0
  decreases 0
=
  echo "Hello from Li"
  return 0
```

| Line | Meaning |
|------|---------|
| `def main() -> int` | Entry function; returns an integer exit code |
| `requires true` | Precondition (here: always allowed to run) |
| `ensures result == 0` | Postcondition: return value is 0 |
| `decreases 0` | This procedure does not loop — trivially finishes |
| `=` | Start of the body (indentation continues the block) |

## Build

```bash
lic build hello.li -o hello
./hello
```

## What “requires / ensures / decreases” are for

Think of them as **promises**:

- **requires** — “I only run when this is true.”
- **ensures** — “When I finish, this will be true.”
- **decreases** — “Something counts down so I cannot loop forever.”

Li uses these promises during **`lic build`**. If Li cannot see that your promises are consistent with your code, the build fails. That is intentional: you learn about mistakes before you run anything.

## Printing text

`echo` works on integers and strings (when the runtime supports them):

```nim
def main() -> int
  requires true
  ensures result == 0
  decreases 0
=
  echo 42
  return 0
```

## Calling other procedures

```nim
def greet() -> int
  requires true
  ensures result == 0
  decreases 0
=
  echo "Hi"
  return 0

def main() -> int
  requires true
  ensures result == 0
  decreases 0
=
  greet()
  return 0
```

Next: [Examples gallery](examples-gallery.md) or the [Language handbook](../language/overview.md).


<!-- source: guide/getting-started-tools.md -->

# Getting started — tools

You need a C++ compiler, CMake, Ninja, and **LLVM 22** once. After that, building Li is one command.

## macOS

```bash
brew install llvm@22 cmake ninja
export LLVM_DIR="$(brew --prefix llvm@22)/lib/cmake/llvm"
export CC=clang CXX=clang++
./scripts/build.sh
./build/compiler/lic/lic --version
```

## Linux (Ubuntu 24.04+)

```bash
sudo apt-get install cmake ninja-build clang-22 llvm-22-dev lld-22
export LLVM_DIR=/usr/lib/llvm-22/lib/cmake/llvm
export CC=clang-22 CXX=clang++-22
./scripts/build.sh
```

If `clang-22` is not found, use [apt.llvm.org](https://apt.llvm.org/):

```bash
wget -O /tmp/llvm.sh https://apt.llvm.org/llvm.sh
chmod +x /tmp/llvm.sh
sudo /tmp/llvm.sh 22
sudo apt-get install -y clang-22 llvm-22-dev lld-22
```

## Linux (Debian 12 bookworm)

Debian main repos do not ship LLVM 22; use apt.llvm.org:

```bash
sudo apt-get install -y cmake ninja-build wget gnupg zlib1g-dev libzstd-dev python3
wget -O /tmp/llvm.sh https://apt.llvm.org/llvm.sh
chmod +x /tmp/llvm.sh
sudo /tmp/llvm.sh 22
sudo apt-get install -y clang-22 llvm-22-dev lld-22
export LLVM_DIR=/usr/lib/llvm-22/lib/cmake/llvm
export CC=clang-22 CXX=clang++-22
./scripts/build.sh
```

Or `./scripts/build.sh` after `export LLVM_DIR=...` — it auto-detects via `scripts/llvm-env.sh`.

**Cloud Agent VMs:** use [cloud-agent-vm.md](../ecosystem/cloud-agent-vm.md) — `bash scripts/cloud-vm-bootstrap.sh`.

**Dedicated dev box (e.g. `engine`):** use the idempotent script and agent-oriented guide — [devbox Li development](devbox-li-development.md).

```bash
sudo bash scripts/setup-li-devbox.sh --full
```

## Windows

Use the GitHub Actions recipe as a reference: LLVM 22 via Chocolatey, then `cmake -B build` with `LLVM_DIR` pointing at the install.

## Lean 4 (proof gate — optional for quick builds, required for full CI)

```bash
bash /home/s4il0r/Documents/Cursor/li-langverse/lic/scripts/ci-install-lean.sh
export PATH="$HOME/.elan/bin:$PATH"
cd /home/s4il0r/Documents/Cursor/li-langverse/lic/docs/semantics && lake build
```

Without `lake`, `lic build` still runs but skips semantics verification (see [provability-gaps.md](../verification/provability-gaps.md)).

## Your first build

```bash
./build/compiler/lic/lic build examples/hello.li -o hello --release
./hello
```

## Commands you will use

| Command | What it does |
|---------|----------------|
| `lic parse file.li` | Is the syntax OK? |
| `lic check file.li` | Syntax + types (quick, for the editor) |
| `lic build file.li -o app` | Full pipeline → runnable program |
| `lic build file.li -o app --release` | Optimized native binary |
| `lic build file.li -o app --threads=8` | Hint OpenMP to use 8 threads (when parallel code is present) |

`lic check` is for speed while you type. **`lic build` is the real gate** when you want a program you trust.

## Run the project’s tests

```bash
./scripts/ci.sh
```

That builds Li, runs security checks, and runs the full `li-tests` suite.

Next: [Hello world in depth](hello-world.md).


<!-- source: language/overview.md -->

# Language handbook — overview

Li is a **compiled**, **statically typed** language for science and systems that must be **correct**. This handbook describes the language as designed and notes what the current `lic` compiler accepts today.

For the normative technical spec, see the [language design spec](../superpowers/specs/2026-05-14-li-language-design.md).

## Design goals (plain language)

1. **No silent lies** — types and contracts must agree; the build fails otherwise.
2. **Readable code** — **does what it reads like it does** (Python-style simplicity: clear names, obvious flow). See [Philosophy](philosophy.md).
3. **Real speed** — after proof, LLVM produces native code with SIMD and multiple cores.

## Program shape

```nim
# optional types and imports at top level

def name(arg: T) -> R
  requires <precondition>
  ensures <postcondition>
  decreases <measure>
=
  <statements>
```

- **Top level:** `proc`, `type`, `object`, `enum`, `extern proc`.
- **No `Any`**, no `unsafe`, no `sorry` in user code.

## Handbook map

| Topic | Page |
|-------|------|
| Philosophy & naming | [Philosophy](philosophy.md) |
| Naming conventions (PascalCase types) | [Naming conventions](naming-conventions.md) |
| Full OOP roadmap (methods, traits) | [OOP roadmap](../superpowers/plans/2026-05-20-li-oop-roadmap.md) |
| Imports | [Import style](import-style.md) |
| Types & data | [Types and data](types-and-data.md) |
| Scalar precision (`float32`, `binary`, suffixes) | [Scalar precision](scalar-precision.md) |
| Math/physics at any width | [Precision polymorphism](precision-polymorphism.md) |
| Numbers | [Numerics](numerics.md) |
| Vectors & parallel | [SIMD and parallel](simd-parallel.md) |
| Contracts & proof | [Contracts and proofs](contracts-and-proofs.md) |
| Control flow & functions | [Control flow and functions](control-flow-and-functions.md) |
| Collections & generics | [Collections and generics](collections-generics.md) |
| Effects & I/O | [Effects and I/O](effects-and-io.md) |

## What every compiling program includes

| Feature | Required? |
|---------|-----------|
| `requires` / `ensures` on each `def` | Yes |
| `decreases` on each loop | Yes |
| `invariant` on `while` loops (when used) | Yes |
| Disjoint proof on `parallel for` | Yes |
| Explicit effects (`raises IO`, etc.) when using I/O | Yes |

## Commands

| Command | Purpose |
|---------|---------|
| `lic parse` | Syntax only |
| `lic check` | Fast feedback (not a certificate) |
| `lic build` | Full gate → binary |

## Status honesty

The compiler is **growing**. Some spec features are fully implemented; others are parsed or typechecked only. When in doubt, look at `li-tests/` for a working `.li` example or run `lic build` on your file.

**Canonical gap list:** [Provability gaps (current compiler)](../verification/provability-gaps.md) — what is **not** proved or not wired yet (Lean gate, decorator elaboration, math surface, heuristic parallel checks, …).

Implementation phases: [Master plan](../superpowers/plans/2026-05-14-li-master-plan.md).


<!-- source: language/philosophy.md -->

# Li language philosophy — simplicity and readable code

**What this page is for:** How Li should *feel* when you read and write it — close to Python’s “code is read more than written,” with Li’s proof gate on top.

## One sentence

**Li does what it reads like it does** — names and layout should be obvious enough that pseudocode and real Li are almost the same, and the compiler proves the promises you wrote in plain language.

## What we take from Python (PEP 20 and practice)

Python’s [Zen of Python (PEP 20)](https://peps.python.org/pep-0020/) is not a checklist to copy; it is a **bias toward the reader**. Li adopts the same bias:

| Aphorism | Li reading |
|----------|------------|
| **Simple is better than complex** | Prefer one clear `def` over clever metaprogramming. Sugar must desugar to a small core the prover understands. |
| **Readability counts** | If a teammate cannot skim it in one pass, rename or split it — proof obligations do not excuse opaque names. |
| **Explicit is better than implicit** | Effects (`raises IO`), contracts (`requires` / `ensures`), and types are written out — no hidden globals, no `Any`. |
| **There should be one obvious way** | One idiomatic import (`import physics.runtime`), one obvious loop shape with `decreases`, one obvious parallel form with `disjoint`. |
| **If the implementation is hard to explain, it’s a bad idea** | Applies to **language design** and **your** code: if you cannot say what a `proc` does in one English sentence, refactor. |
| **Namespaces are a great idea** | Dotted modules (`math.numerics`, `physics.fluids`) and small packages — see [import style](import-style.md). |

Python also teaches **practicality beats purity** — Li allows that *after* proof: e.g. `--release` for speed, optional `--numerically-stable` for FP — never by skipping the proof gate.

## Li’s ordering (proof does not fight simplicity)

```text
1. Correct   — types, contracts, memory, termination (lic build)
2. Clear     — reads like prose; names match the domain
3. Fast      — LLVM, SIMD, parallel — only after 1 and 2 for shipped code
```

**Correct** is stricter than Python. **Clear** should be *easier* than C++ template soup: indentation, familiar types, domain words in identifiers.

## Read like prose

Good Li reads as **short sentences**:

```li
def advance_orbit(body: Body, dt: float) -> unit
  requires dt > 0
  ensures energy_drift(body) < max_drift
  decreases 0
=
  var force: Vec3 = gravity_from(body.position)
  body.velocity = body.velocity + force * dt
  body.position = body.position + body.velocity * dt
```

A reader should infer: *for a positive timestep, advance velocity then position, and energy drift stays bounded.*

Contracts are **promises in English-shaped logic**, not magic comments:

- `requires dt > 0` — “only call with positive dt”
- `ensures result >= 0` — “never returns negative”
- `decreases n` — “this loop gets closer to done”

## Naming (packages, types, functions, variables)

**Canonical table:** [Naming conventions](naming-conventions.md) — PascalCase **`ClassName`** for types/objects; snake_case for `def`, variables, and fields.

### Packages and imports

| Do | Don’t |
|----|--------|
| `import physics.relativity` | `import li_std_physics_relativity` |
| GitHub repo `li-physics-relativity` | `li-std-physics-relativity` (legacy) |

Rule: **import path = how you talk about the domain.** See [import-style.md](import-style.md) and [repo naming](../ecosystem/repo-naming.md).

### Functions (`def`)

Li uses Python-style **`def`** for functions. Legacy docs may mention `proc`; new code and game-dev vision use **`def`** only.

- **Verb phrases:** `step_world`, `load_scene`, `compute_forces`, `normalize_velocity`
- **Say what, not how:** `merge_collisions` not `do_pass_2`
- **Units in the name when it matters:** `distance_meters`, `angle_rad`

### Types and objects (class names)

Li uses `type Name = object`, not a `class` keyword — but **type names follow class naming:**

- **PascalCase** (`ClassName`): `Body`, `PhysicsWorld`, `RigidBody`, `CollisionPair`
- **Not** snake_case or camelCase for types: no `rigid_body`, no `physicsWorld`
- **Fields** stay **snake_case:** `position`, `mass`, `velocity` — not `p`, `m`, `v` in public APIs

### Variables

- **Short scope → short name is OK:** loop index `i`, `j`
- **Long scope → full words:** `accumulated_energy`, `time_step`
- **Booleans read as questions:** `is_visible`, `has_collision`, `can_merge`

### Casing (summary)

| Kind | Style |
|------|--------|
| `def`, variables, fields, modules | **snake_case** (Python-like) |
| `type` / `object` names | **PascalCase** (`ClassName`) |

## Pseudocode ↔ Li

Li is designed so design docs can stay almost literal:

| Pseudocode | Li |
|------------|-----|
| `for each body in world: apply gravity` | `while i < n` + indexed loop or future `for` when specified |
| `distance = sqrt(dx*dx + dy*dy)` | `li_rt_hypot(dx, dy)` or explicit ops |
| `require dt > 0` | `requires dt > 0` on the `proc` |

If pseudocode needs a footnote to map to Li, the **surface syntax** should be improved (RFC), not the pseudocode.

## What we avoid (anti-python in the good sense)

| Pattern | Why |
|---------|-----|
| `Any`, unchecked `cast`, `unsafe` | Breaks proof and “what you read is what runs” |
| Hungarian notation (`strName`, `iCount`) | Noise; types are static |
| Abbreviation soup (`cfg`, `mgr`, `tmp` in APIs) | Saves typing, costs comprehension |
| Clever one-liners that hide effects | Effects must stay explicit |

## For agents and reviewers

When changing Li code or docs:

1. Read the `proc` names aloud — do they sound like steps in a story?
2. Prefer extending [easy imports](../../.cursor/rules/li-easy-imports.mdc) over new opaque module prefixes.
3. Do not trade readability for “fewer lines” in examples users copy.

## Related

- [Language handbook overview](overview.md)
- [Control flow and functions](control-flow-and-functions.md)
- [Language design spec](../superpowers/specs/2026-05-14-li-language-design.md) — normative pillars
- [Import style](import-style.md)
- Python: [PEP 20](https://peps.python.org/pep-0020/), [PEP 8](https://peps.python.org/pep-0008/) (style guide for names and layout)


<!-- source: language/types-and-data.md -->

# Types and data

Li’s type system follows **Python 3.14 typing** habits, but programs compile to **fixed-size machine types**. There is no `Any`.

## Scalar types (everyday names)

| Li name | Machine type | Notes |
|---------|--------------|-------|
| `int` | `i64` | Default integer; not unlimited precision |
| `uint` | `u64` | Unsigned; no silent mix with `int` |
| `float` | `float64` | IEEE binary64 |
| `bool` | `bool` | Not a number |
| `str` | string | UTF-8 at runtime |
| `unit` | void-like | “No useful value” |
| `binary` | bit-packed | Quantized masks / weights (`0b…` literals); not `bytes` |

## Fixed-width integers and floats

Full tables (including `float4` … `float512`, `int4` … `int512`): **[Scalar precision](scalar-precision.md)**.

| Signed | Unsigned | Float (examples) |
|--------|----------|-------------------|
| `i8` … `i128`, `int32` | `u8` … `u128`, `uint32` | `float16`, `float32`, `float64` (`float`) |
| `int4` … `int512` | `uint4` … `uint512` | `float4`, `float8`, … `float512` |

Mixing widths without a cast is an error. The ecosystem does **not** enforce one global accuracy — projects and physics profiles choose per module.

## Complex numbers

| Type | Layout |
|------|--------|
| `complex` / `complex128` | Two `float64`: real + imaginary |
| `complex64` | Two `float32` |

## SIMD vectors

```nim
var v: simd[f64, 4]
var w: simd[f32, 8]
```

Packed lanes for HPC. See [SIMD and parallel](simd-parallel.md).

## Arrays (fixed size)

```nim
var grid: array[64, float]
var ids: array[128, int]
```

- Size `N` is part of the type.
- Indexing must stay in bounds (proved or checked).

## Collections (heap)

| Type | Python analogue |
|------|-----------------|
| `list[T]` | `list` |
| `dict[K, V]` | `dict` |
| `tuple[...]` | `tuple` |
| `TypedDict` | `TypedDict` |
| `frozenset[T]` | immutable set view |

Allocation may carry `raises Alloc`.

## Named shapes

Type and object names use **PascalCase** (`ClassName`) — see [Naming conventions](naming-conventions.md). Fields use **snake_case**.

```nim
type Point = object
  x: float
  y: float

type Color = enum
  Red, Green, Blue
```

## Refinement types (value domains)

```li
type NonNeg = {x: int | x >= 0}
type Index = {i: int | 0 <= i and i < N}
```

A refinement declares **which values** a name may take. Parameters and `var` bindings of that type are checked at **calls** and **initializers**:

- Provably **outside** the predicate → **E0305** (compile error).
- **Inside** but not yet provable → proof obligation (see [Refinement types](refinement-types.md)).

Index refinements (`Index`, `Index10`, …) use the same syntax for array safety; see `li-tests/contracts_verify/index_refinement.li`.

## Callable and Protocol

```nim
type Handler = Callable[[int], bool]
type Sized = Protocol["__len__", int]
```

Generics use PEP 695 style:

```nim
def identity[T](x: T) -> T
```

## What is forbidden

| Forbidden | Why |
|-----------|-----|
| `Any` | No static guarantee |
| `unsafe` | Bypasses proof |
| Bare `cast[T](e)` | Need proof-carrying cast |
| `sorry` / `assume` | Fake proofs |

## Cast with proof

```nim
cast[T](value, proof)
```

Only when a proof term shows the cast is valid.

More numbers detail: [Numerics](numerics.md).


<!-- source: language/contracts-and-proofs.md -->

# Contracts and proofs

Li is **provable-only** by design: if proof obligations are not discharged, there should be **no binary**.

!!! note "Implementation status"
    **Today:** every `lic build` emits `build/generated/AutoVC.lean` and runs **Lean typecheck** when `lake` is installed; **open** obligations fail the build unless `--allow-open-vc`. Kernel discharge of all ensures is still **partial** — see **[Provability gaps](../verification/provability-gaps.md)**.

## On every procedure

```nim
def sqrt_pos(x: float) -> float
  requires x >= 0.0
  ensures result >= 0.0
  decreases 0
=
  ...
```

| Clause | Role |
|--------|------|
| `requires` | Precondition — caller must establish this |
| `ensures` | Postcondition — true on return (`result` names the return value) |
| `decreases` | Termination measure for the procedure body |

## On every loop

```nim
while n < limit
  invariant 0 <= n and n <= limit
  decreases limit - n
=
  n = n + 1
```

| Clause | Role |
|--------|------|
| `invariant` | True at the start of each iteration |
| `decreases` | Strictly decreases each iteration — proves the loop ends |

`parallel for` also carries `requires` (disjointness), `invariant`, and `decreases`.

## What gets proved

| Property | How |
|----------|-----|
| Type safety | Static checker |
| Index bounds | Refinements + checks |
| Value domains (`{x: int \| …}`) | Refinement types — **E0305** when provably violated; VC otherwise ([refinement-types](refinement-types.md)) |
| Memory / borrow | Borrow checker |
| Contract obligations | Lean 4 VC generation (**partial** — proc + call-site `requires` + refinement VCs; see [gaps](../verification/provability-gaps.md)) |
| Parallel races | Disjointness + `Send`/`Sync` (**partial** — policy heuristics today) |
| No `Any` / `sorry` | Hard reject |

## `lic check` vs `lic build`

| Command | Proof certificate? |
|---------|-------------------|
| `lic check` | **No** — IDE-speed feedback |
| `lic build` | **Target:** Lean must accept remaining goals · **Today:** static gate only ([gaps](../verification/provability-gaps.md)) |

When Phase **2f** lands, treat `lic build` like signing a theorem: the executable is the certificate artifact.

## Trusted base (tiny)

Only `docs/semantics/trusted.lean` may contain unproved axioms — minimal `IO` and audited `extern`. User application code never goes there.

## Why this is “mathematical”

Proofs are checked by the **Lean 4 kernel**, not by “we ran tests and it looked fine.” See [Why Li is provable](../compiler/why-provable.md).

## Common mistakes

| Mistake | What Li does |
|---------|----------------|
| Missing `decreases` | Compile error |
| `ensures true` on `-> float` / `-> int` / struct | **Compile error E0303** — postcondition must mention `result` |
| `ensures` too weak | May still prove, but you lied — review specs |
| `ensures` too strong | Proof fails — strengthen code or weaken spec honestly |
| Using `sorry` | Rejected |

More: [Verification overview](../verification/overview.md) · [Provability gaps](../verification/provability-gaps.md).


<!-- source: language/numerics.md -->

# Numerics

Li uses **Python-like names** with **compiled fixed-width** behavior. This catches common scientific bugs (like adding an `int` to a `float` by accident).

## Default mappings

| You write | Machine |
|-----------|---------|
| `int` | 64-bit signed |
| `float` | 64-bit IEEE |
| `42` | integer literal → `i64` |
| `3.14` | float literal → `f64` |

**Full width tables, suffixes, `binary`, and physics metadata:** [Scalar precision](scalar-precision.md) (canonical).

**You choose precision** — explicit types (`float32`), suffixes (`3.14f32`), optional `li.toml` `[numerics]`, and physics `float_bits` are all **per-project / per-module** choices; the org does not enforce one global width. See [You set precision yourself](scalar-precision.md#you-set-precision-yourself).

## Literal suffixes

```
42       # int (i64)
42u      # uint (u64)
42i32    # int32
255u8    # uint8
3.14     # float64
3.14f32  # float32
1.0f16   # float16
0b1011   # binary
2.0 + 1.0i   # complex
```

## Operators (important rules)

| Expression | Result |
|------------|--------|
| `int + int` | `int` |
| `float + float` | `float` |
| `int + float` | **Error** (must cast explicitly) |
| `int / int` | `float` (Python 3 division) |
| `int // int` | floor division |

## Overflow

Default integers are **checked**: overflow must be impossible to prove, or you use an explicit mode:

| Mode | Meaning |
|------|---------|
| `checked int` | Default — must prove no overflow |
| `wrapping i32` | Modular arithmetic with proof |
| `saturating i32` | Clamped arithmetic with proof |

There is **no** silent `unchecked int`.

## Effects on numeric ops

| Situation | Effect |
|-----------|--------|
| Division by zero | `raises DivZero` or compile error if divisor is literal 0 |
| `sqrt` of negative | `raises Float` (by default) |

## SIMD numerics

`simd[T, N]` supports lane-wise `+`, `*`, and intrinsics such as horizontal sum. Element type `T` is typically `f32` or `f64`.

See [SIMD and parallel](simd-parallel.md).

## Roadmap (not all shipped yet)

| Phase | Features |
|-------|----------|
| v1 | Scalars, complex, SIMD, parallel CPU |
| v2 | `f16`, `bf16`, async generators |
| v3 | `tensor[Shape, T]`, GPU buffers |

Full tables: [design spec — numeric roadmap](../superpowers/specs/2026-05-14-li-language-design.md#numeric-roadmap).


<!-- source: language/simd-parallel.md -->

# SIMD and parallel execution

Li targets **CPU HPC**: vector lanes on one core, many cores on shared memory — **without** user-installed parallel frameworks.

!!! note "Provability status"
    Disjointness for `parallel for` is enforced today partly via **string heuristics** in `policy.cpp`, not full Lean discharge. Decorators (`@parallel`, …) **parse** but do not yet elaborate. See **[Provability gaps](../verification/provability-gaps.md)** (**G-par**, **G-dec**).

## Two layers

| Layer | Syntax | Hardware |
|-------|--------|----------|
| SIMD | `simd[T, N]` | AVX / NEON vector units |
| Multi-core | `parallel for` | `li_parallel_for` (`--cores`) (linked by `lic build`) |

Inner SIMD + outer `parallel for` is the standard Li pattern for hot loops.

## SIMD type

```nim
var a: simd[f64, 4]
var b: simd[f32, 8]
```

Rules (v1):

- `T` ∈ integer or float lane types (`f32`, `f64`, `i32`, …).
- `N` ∈ `{4, 8}` in the current compiler (spec allows more).
- No silent fallback to scalar if the CPU cannot do `N` lanes.

### Intrinsics (today)

| Intrinsic | Role |
|-----------|------|
| `__li_simd_splat_f64(x)` | Broadcast scalar |
| `__li_simd_mul_f64(a, b)` | Lane-wise multiply |
| `__li_simd_add_f64(a, b)` | Lane-wise add |
| `__li_horiz_sum_f64(v)` | Sum lanes to scalar |

Stdlib names like `horizontal_sum` and `dot` are planned to wrap these.

## `parallel for`

```nim
parallel for i in 0..<N
  requires disjoint_row(i, grid)
  invariant row_ok(i, grid)
  decreases N - i
=
  compute_row(grid, i)
```

### Proof names the checker knows

Include a disjointness clause in source, for example:

- `disjoint_row(i, grid)`
- `disjoint_elem(i, buf)`
- `disjoint_slice(...)`

Without such a clause, **`lic build` rejects** the loop.

### What is rejected (by design)

| Pattern | Result |
|---------|--------|
| All threads write `buf[0]` | Compile error |
| Overlapping `par_slice` ranges | Compile error |
| Mutable capture without `Sync` | Compile error |
| `borrow mut` across iterations | Compile error |
| Fake disjoint proof | Lean / VC rejection |

Exploit fixtures live in `li-tests/race_shared_memory/`.

## Thread count

```bash
lic build app.li -o app --cores=8 --threads-per-core=1
./app
```

See [execution surface](../superpowers/specs/2026-05-25-li-execution-surface.md). Native pool replaces OpenMP on user link path.

## `Send` and `Sync` (spec)

Values captured into parallel regions must be safe to share. Laws are defined in the Lean semantics; the surface syntax enforces `Sync` when shared mutable state appears.

## GPU (future)

`gpu proc` and device buffers are **not** v1 — CPU SIMD + OpenMP first.

Benchmarks: [Benchmarks guide](../benchmarks.md).


<!-- source: compiler/why-provable.md -->

# Why Li is mathematically provable

“Mathematically provable” means: the important properties of your program are **theorems** checked by a small, trusted proof engine — not hopes backed by testing alone.

## The proof gate

```
lic build  →  binary exists  ⟺  proofs closed   (target)
lic check  →  fast feedback only (no certificate)
```

**Today:** `lic build` runs parse, policy, typecheck, borrow, and codegen — **without** Lean yet. See **[Provability gaps](../verification/provability-gaps.md)**.

When Phase **2f** lands: if Lean still has open goals, **no executable ships**.

## What is being proved?

| Claim | Mechanism |
|-------|-----------|
| Types line up | Typechecker |
| Indices in range | Refinements + VCs |
| Memory safe | Borrow checker |
| Preconditions hold | `requires` / `ensures` |
| Loops terminate | `decreases` |
| Parallel loops race-free | Disjointness + Sync laws |
| No escape hatches | Reject `Any`, `sorry`, bare `cast` |

Together, these are stronger than “we fuzzed it.”

## Why Lean 4?

Lean’s **kernel** checks proof terms. If the kernel accepts a proof, the logical chain is valid relative to the axioms you started from.

Li is not “SMT said maybe” or “tests passed” — it is **proof objects** checked by the kernel.

This is the same assurance culture as **Coq**-style verification, using Lean 4 as the engine.

## What you write vs what Lean sees

You write Nim-like code with contracts. The compiler:

1. Typechecks and borrows.
2. Generates **verification conditions** (VCs).
3. Sends obligations to Lean.
4. Only then emits LLVM.

So the binary is a **compiled proof artifact**, not a separate “verified mode.”

## Trusted axioms (minimal)

Real programs need a little I/O. Li keeps a **small** trusted file:

`docs/semantics/trusted.lean`

Only this file may contain unproved axioms (bounded, reviewed). Application logic stays in user code with full contracts.

## Honest limits

| Limit | Explanation |
|-------|-------------|
| **Implementation gaps** | Features listed in the spec but not fully proved yet — **[gap register](../verification/provability-gaps.md)** |
| Wrong spec | You can prove the wrong theorem perfectly |
| Trusted base growth | Must stay tiny and audited |
| Compiler correctness | Proving the C++ compiler matches Lean is future meta-work |
| CPU behavior | Proofs are about the Li model, not flaky hardware |

## Parallelism and proof

Shared-memory parallelism is the hardest part of HPC correctness. Li’s answer: **reject** `parallel for` unless disjointness is stated and checked. See `li-tests/race_shared_memory/`.

## Learn more

- [Provability gaps (today)](../verification/provability-gaps.md)
- [Contracts and proofs](../language/contracts-and-proofs.md)
- [Verification overview](../verification/overview.md)
- [Language design — pillars](../superpowers/specs/2026-05-14-li-language-design.md)


<!-- source: compiler/build-pipeline.md -->

# How `lic build` works

When you run `lic build program.li -o app`, Li runs a **fixed pipeline**. If any stage fails, you get diagnostics — not a broken binary.

## Stages (in order)

```mermaid
flowchart TD
  src[.li source]
  lex[Lexer]
  parse[Parser]
  policy[Policy checks]
  types[Typecheck + borrow]
  mir[MIR lower]
  llvm[LLVM IR]
  link[Clang link + li_rt]
  bin[Native binary]
  src --> lex --> parse --> policy --> types --> mir --> llvm --> link --> bin
```

| Stage | What it does |
|-------|----------------|
| **Lexer** | Text → tokens (indentation-aware) |
| **Parser** | Tokens → AST |
| **Policy** | Forbidden constructs (`Any`, bad parallel patterns, …) |
| **Typecheck** | Types, effects, contracts surface |
| **Borrow** | Memory exclusivity |
| **Lean** (full gate) | Discharge proof obligations — **not wired yet** ([gaps](../verification/provability-gaps.md) **G-lean**) |
| **MIR** | Typed AST → mid-level IR (SIMD, loops, calls) |
| **LLVM** | MIR → `.ll` IR |
| **Link** | Clang links IR + `runtime/li_rt.c` (+ OpenMP if needed) |

`lic parse` and `lic check` stop earlier for speed.

## What happens at compile time vs run time

| Compile time | Run time |
|--------------|----------|
| Type errors | — |
| Out-of-bounds proofs | Optional bounds trap in debug |
| Parallel race rejection | — |
| LLVM optimization (`--release`) | CPU executes machine code |
| OpenMP team creation | Threads run parallel loops |

Most safety wins are **before** you run the program. The full proof gate is still **in progress** — see **[Provability gaps](../verification/provability-gaps.md)**.

## Flags

| Flag | Effect |
|------|--------|
| `--release` | `-O2` style optimization at link |
| `--jobs=N` | Parallel compile workers |
| `--cores=N` | Runtime parallel team from hardware cores |
| `--threads-per-core=M` | Threads per core (default 1); team = min(N×M, 64) |
| `--threads=N` | Total runtime parallel team (overrides `--cores` when both set) |
| `-o path` | Output binary path |

Environment:

| Variable | Effect |
|----------|--------|
| `LI_EXTRA_C` | Extra `.c` files to link (benchmarks) |
| `LI_OMP_THREADS` | Deprecated; use `--threads=N` (team baked into binary at build) |
| `CC` / `CXX` | C compiler for final link |

## Artifacts

- Intermediate LLVM IR is written temporarily during build.
- Final output is a native executable depending on `li_rt` (panic, print, OpenMP driver, math helpers).

## Architecture detail

Module layout: [Architecture overview](../architecture/overview.md).

## LLVM types and C ABI

Which LLVM types correspond to `int`, `str`, `bytes`, and `extern` calls — and how that must match `runtime/li_rt.c` — is documented in **[LLVM codegen and native ABI](llvm-abi.md)**. Read that before adding new `extern proc` or changing pointer parameter types.


<!-- source: verification/provability-gaps.md -->

# Provability gaps (current compiler)

**Last updated:** 2026-05-30  
**Audience:** contributors, package authors, anyone relying on `lic build` as a proof certificate  

Li’s **north star** is: user logic is proved before ship; runtime failures for proved programs → **~0%**. That is the **target**, not a complete description of **`lic` today**.

**Policy vs implementation:** [Strict by default](../ecosystem/strict-by-default.md) — there is **no optional provability** by default. Rows below are **compiler maturity** (what is not wired yet), **not** permission for users to turn proof off without an explicit `li.toml` / documented downgrade.

This page is the **honest inventory** of what is **not** fully proved or not yet wired. When a gap closes, update this file in the **same PR** as the implementation.

**Related:** [Verification overview](overview.md) · [Master plan — Doc phase & compiler task map](../superpowers/plans/2026-05-14-li-master-plan.md#documentation--provability-honesty-cross-cutting) · [Trusted axioms](../semantics/README.md)

---

## Summary (read this first)

| | Target (spec) | Today (`lic` on `dev`) |
|---|----------------|-------------------------|
| **`lic build` = proof certificate** | Lean 4 kernel closes all VCs | **No** — parse, policy strings, typecheck, borrow, LLVM link only |
| **`lic check`** | Fast IDE feedback | **Yes** — no Lean, not a certificate |
| **Parallel disjointness** | Lean + structured proofs | **Partial** — substring heuristics in `policy.cpp` |
| **Index bounds (release)** | Refinement / proved → no user traps | **Partial** — MIR/runtime paths still evolving |
| **Decorators (`@parallel`, …)** | Compile-time elaboration + proofs | **Partial** — parse + policy (7d-a/e); no MIR lowering yet |
| **Math / linalg surface** | Static shapes, compile-time lowering | **Partial** — shape tests + **P-linalg** closed VCs (2i / 7e) |
| **Zero user runtime errors** | All above + 2f gate | **In progress** — see table below |

---

## Still open (report every session)

**Done:** **G-test-verify** (manifest `prove_lean_ok`). **Closed slices** inside **Partial** rows (e.g. P-linalg closed specimens, static `ensures` witnesses). All other **G-*** rows remain **Partial** or **Missing**.

| ID | Status | What remains |
|----|--------|----------------|
| **G-lean** | Partial | **Tier B (default when lake installed):** `lic build` runs `lake build AutoVC` (typecheck only; `--no-lean-verify` opt-out). **Strict** open goals: `--strict-lean`. Open obligations: fail unless `--allow-open-vc` (CLI only; env bypass removed). **`LiArray`** + fib/recursive call-site + parallel `_par*` VCs typecheck. **Closed slice:** `sqrt_open_bound` via `Li.Discharge` + `Li.Trusted.li_rt_sqrt_square_bound` (**G-hw**). **Still open:** `mat2_at2_eval` trusted vs MIR `@` (semantic closed in `Discharge.lean`) |
| **G-vc** | Partial | **Closed slice:** `sqrt_open_bound` float `abs` bound (trusted libm axiom). Still open: opaque `vec3_dot`-style returns; loop implementations vs closed-form `ensures` |
| **G-par** | Partial | AST `policy_module` rejects missing disjoint, false `disjoint_row`, mut capture, borrow-in-par; Lean proofs open |
| **G-dec** | Partial | **Closed slice:** MIR telemetry + corpus scripts; Lean **P-dec** open |
| **G-math** | Partial | **Closed slice (tier-1):** `matmul_naive`, `horner_pure_li` ≤1.2× C++ (`check-tier1-li-vs-cpp.sh`, loop matmul + FMA horner). **Closed slice:** full 2×2 float `@` Lean Prop (`linalg_mat2_at2_float_closed`, `mat2_at2_float_spec`). **Closed slice:** `linalg_dot4_float_closed` (prelude `dot`), `linalg_mat2_callproc_float_closed`, prelude `norm`/`axpy`/**, IKJ `ArrayMatMul2DF64` enforced only with `LI_TIER1_PERF_STRICT=1` (`check-tier1-li-vs-cpp.sh` reports gaps by default). **Closed slice:** prelude `norm`, `axpy`, same-length `**`, scalar×array, `math_linalg/reductions/`, loop-dot witness, P-linalg corpus |
| **G-bnd** | Partial | **Closed slice:** `bounds_refinement_release_ok.li` + `check_release_bounds_ir.sh`; `discharge_refinement_lean.sh` |
| **G-def** | Partial+ | Cross-module method privacy proofs; virtual dispatch deferred |
| **G-oop** | Partial | Lean `ensures` on methods; trait laws in kernel |
| **G-math-syn** | Partial | **Closed slice:** `for i in start..<end` (`math_syntax/for_range_sum.li`); Python `range()` / dynamic bounds open |
| **G-stdlib** | Partial | Full workspace cycle + seal edge cases |
| **G-narrow** | Partial | Proved width narrowing (beyond `cast[` reject) |
| **G-async** | Partial | `await` + structured concurrency proofs |
| **G-net** | Partial | Net effect codegen + proofs |
| **G-trust** | Stub | `Core.lean` / `MIR.lean` semantics, not placeholder |
| **G-ann** | Missing | PEP 649 deferred annotations |
| **G-gpu** | Partial | **Closed slice:** `@gpu` / `@gpu(devices=N)` are MIR-visible (`mir_gpu_def`, `mir_gpu_multi_device_def`) with `devices >= 1` policy. Still open: address-space proofs, LKIR lowering, device buffers, and vendor codegen |
| **G-meta** | Missing | Compiler ↔ Lean equivalence (research) |
| **G-authz** | Missing | Capability / IDOR (OS phase) |
| **G-test-verify** | **Done** | `prove_lean_ok` in `run_all.sh`; 14 closed `contracts_verify` specimens |
| **G-proof-db** | Partial | [Proof database](proof-database.md): register at `docs/verification/proof-database/entries/physics-*.toml` (`P-AX-*`, `P-LM-*`) |
| **G-physics** | Partial | **P-physics** slice: 7× `P-AX-*` + 3× `P-LM-*`; 2× proved scalar lemmas in `Discharge.lean`; tier-2 **modeling_gap** on extern stubs |
| **G-hw** | Axiomatic | FP/hardware model limit (documented, not closable) |
| **G-num** | Stub | **WP0-A:** planned entries/num-*.toml + proof-db/num/; Peano/order linkage via **G-math**; no discharge slice yet |
| **G-discrete** | Stub | **WP0-A:** combinatorics / finitary specs; catalog rows TBD; specimens after num axiom layer |
| **G-stats** | Stub | **WP0-A:** descriptive stats + confidence stubs; tier-2 bench hooks (**5b**) TBD |
| **G-ml** | Stub | **WP0-C:** [ml-convergence-program](ml-convergence-program.md) — parallel Lean + specimen tracks; no closed convergence VC |
| **G-graph** | Stub | **WP0-A:** graph invariants (connectivity, bounds); proof-db/graph/ layout TBD |
| **G-erdos** | Partial | **WP0-B:** proof-db/erdos/register.json → erdos-register.toml (E-*); **WP1+** Lean per 	arget row |
| **G-chem** | Stub | **WP0-D:** reaction / stoichiometry catalog; tier-2 chem benches (**5b**) TBD |
| **G-bio** | Stub | **WP0-D:** population / sequence toy models; tier-2 bio benches (**5b**) TBD |
| **G-wrong-spec** | Social | User theorem quality (not tool-closable) |

**Proof backlog still open:** **P-refine**, **P-ensures-witness**, **P-float**, **P-linalg** (float `@` Props; full matmul), **P-par**, **P-dec**, **P-bnd**, **P-http**, **P-narrow**, **P-meta**, **P-physics**, **P-num**, **P-discrete**, **P-stats**, **P-ml-convergence**, **P-graph**, **P-erdos**, **P-chem**, **P-bio** — see [proof-corpus-roadmap](proof-corpus-roadmap.md). **P-linalg partial:** closed dot/sum/matmul-entry + **loop dot** (`linalg_dot4_int_loop_open`, `dot4_int_loop_eval_spec`); open float `vec3_dot`, 2D CallProc. **P-physics partial:** [proof-database.md](proof-database.md) index + `docs/verification/proof-database/entries/physics-*.toml` (`P-AX-*`, `P-LM-*`, pin `a9542bfc`); tier-2 wrappers still **modeling_gap** (`ensures true` on extern kernels).

### Proof-db discrepancy appendix

[`../../proof-database/DISCREPANCIES.md`](../../proof-database/DISCREPANCIES.md) — `python3 scripts/proof-db/compare_reference.py --write`. Kinds: `missing_lemma`, `open_vc`, `spec_drift`, `trusted_axiom`, `hardware_axiom` (**G-hw**).

### Proof-db discrepancy appendix

[`../../proof-database/DISCREPANCIES.md`](../../proof-database/DISCREPANCIES.md) — `python3 scripts/proof-db/compare_reference.py --write`. Kinds: `missing_lemma`, `open_vc`, `spec_drift`, `trusted_axiom`, `hardware_axiom` (**G-hw**).

!!! warning "Do not overclaim in docs or packages"
    Until **Phase 2f** lands, saying “`lic build` proves your program in Lean” is **aspirational**. Prefer: “`lic build` runs the current static gate; see [provability gaps](provability-gaps.md).”

---

## Gap register

Status legend: **Missing** · **Stub** · **Partial** · **CI only** · **Done**

| ID | Area | Spec / promise | Current state | Phase | How we know |
|----|------|----------------|---------------|-------|-------------|
| **G-lean** | Lean 4 gate | `lic build` fails if any VC open | **Partial** — Tier B `lake build AutoVC` when installed; **closed slice:** 14× `prove_lean_ok` corpus; `sqrt_open_bound` intentional open; kernel not universal certificate | **2f** | `discharge_trivial_lean.sh`, `discharge_linalg_int_lean.sh`, `contracts_discharge_corpus.sh`, `check-autovc-open-goals.sh`, `li-tests/run_all.sh` `prove_lean_ok` |
| **G-vc** | VC generation | Contracts → proof obligations | **Partial** — **closed slice:** call-site `requires`, const-local discharge, E0303/E0304/E0305; open: float `abs`, opaque returns | **2e** | `vc_emit_contracts.sh`, `mir_vc_witness.sh`, `discharge_caller_requires_lean.sh`, `discharge_caller_requires_local_lean.sh`, `contracts_discharge_corpus.sh`, `prove_reject/weak_ensures_true.li` |
| **G-par** | `parallel for` safety | Proved iteration independence | **Partial** — **closed slice:** 6× `compile_fail` + `good_disjoint_parallel.li` `verify_ok`; Lean disjoint proofs open | **7b**, **7d-c** | `li-tests/race_shared_memory/`, `decorator_exploits/missing_disjoint_at_parallel.li`, `run_all.sh` suite `race_shared_memory` |
| **G-stdlib** | Prelude / std seal | User cannot shadow builtin or `std/` names | **Partial** — `check_stdlib_seal` + `resolve_imports` for `std.*` / workspace; cycle detect at load | **4s** | `li-tests/stdlib_seal/`, `li-tests/modules/` |
| **G-dec** | Execution decorators | Static elaboration; reserved names; no runtime | **Partial** — **closed slice:** 4× `decorator_exploits` `compile_fail`; `@vectorized` on `for` (`vectorized_for_scope_ok.li`); `MIR proc tags + corpus scripts | **7d** | `contracts_discharge_corpus.sh`, `decorator_exploits/` |
| **G-math** | Math / `A @ B` | Shape errors at compile time; no user `simd(...)` | **Partial** — **closed slice:** 9× `prove_lean_ok` linalg + `discharge_linalg_int_lean.sh`; `math_linalg/` compile tests; tier-1 `tier1_li_vs_cpp.sh` | **2i**, **7e**, **2f** | `li-tests/math_linalg/`, `li-tests/contracts_verify/linalg_*_closed.li`, `li-tests/tooling/discharge_linalg_int_lean.sh`, `li-tests/tooling/tier1_li_vs_cpp.sh` |
| **G-bnd** | Bounds in release | No reliance on `li_bounds_fail` for proved indices | **Partial** — [bounds-release-path](bounds-release-path.md) | **2e**, **3** | `check_release_bounds_ir.sh` |
| **G-def** | `def` / `object` / visibility | Handbook surface | **Partial+** — methods/`self`, `private def`, MIR in-out write-back (**2j-a/b/c**); inheritance/traits open (**2j-d–f**) | **2j** | `li-tests/encapsulation/`, `composable/import_physics_runtime.li` |
| **G-oop** | Full OOP | Methods, traits, inheritance, cross-module encapsulation | **Partial** — **2j-a…f** surface done; Lean `ensures` on methods / trait laws open | **2j** | `li-tests/encapsulation/trait_*.li`, `method_call_requires_*.li` |
| **G-math-syn** | Python-math (`**`, `for`, …) | Ergonomic surface | **Partial** — `%`, `//`, `**` on `int`; **`for i in 0..<n`** (`for_range_sum.li`); `range()` helper + dynamic bounds open | **2h** | `li-tests/math_syntax/` |
| **G-ann** | Deferred annotations (PEP 649) | Lazy resolve at check | **Missing** — shown in pipeline diagram as planned | **4** | Not in compiler tree |
| **G-gpu** | `@gpu` / device buffers | Separate address space proofs | **Partial** — `@gpu` / `@gpu(devices=N)` MIR telemetry plus `devices >= 1` policy; no address-space proofs, LKIR lowering, device buffers, or vendor codegen yet | **3+**, **7d** | `li-tests/decorators/gpu_*`, `scripts/check-mir-gpu-decorator.sh` |
| **G-async** | `@async` / `raises Async` | Structured concurrency proofs | **Partial** — `@async` requires `raises Async`; await not parsed | **2+**, **7d** | `li-tests/effects/` |
| **G-net** | `raises Net` | Trusted syscall surface | **Partial** — effect propagation + `trusted.lean` axioms; no codegen | **H**, **2f** | `li-tests/effects/net_*.li` |
| **G-trust** | Trusted base growth | Only `trusted.lean` | **Stub** — file exists; `Core.lean` / `MIR.lean` **planned** | **2f** | [semantics/README.md](../semantics/README.md) |
| **G-meta** | Compiler correctness | C++ compiler ≡ Lean semantics | **Missing** (research) | long-term | Not started |
| **G-hw** | Hardware / FP | Model vs IEEE / CPU bugs | **Axiomatic** | — | Documented limit |
| **G-wrong-spec** | User contracts | Correct theorem | **Social** — tool cannot fix | — | Review culture |
| **G-narrow** | Narrowing conversions | Ariane-class truncations rejected without proof | **Partial** — policy rejects `cast[`; width types + proved narrowing pending | **2e** | `historic_ariane5_narrowing.li` |
| **G-authz** | Capability / IDOR | Object capabilities in OS services | **Missing** | OS phase | `historic-bugs.toml` firefly-iii-idor |
| **G-test-verify** | Manifest honesty | `verify_ok` vs Lean QED | **Done** — `prove_lean_ok` outcome; 14 closed `contracts_verify` rows | **2f** | `li-tests/run_all.sh`, `li-tests/manifest.toml`, `contracts_discharge_corpus.sh` |
| **G-proof-db** | Proof database | Axiom → lemma → discharge status vs `lic` commit | **Partial** — physics TOML under `docs/verification/proof-database/entries/physics-*.toml` | **Doc**, **2f**, **5b** | [proof-database.md](proof-database.md) |
| **G-physics** | Classical physics proofs | Newton + conservation linked to tier-2 benches | **Partial** — `entries/physics-*.toml`; 2× `proved` + 1× open `P-LM-*` in `Discharge.lean` | **Doc**, **2f**, **5b** | [proof-database/entries/physics-*.toml](proof-database/entries/physics-mechanics.toml), `benchmarks/tier2_physics/`, `Discharge.lean` |
| **G-num** | Number theory / arithmetic | Peano-through-primes lemmas in proof-db catalog | **Stub** — **WP0-A** entry TOML + proof-db/num/ not wired | **Doc**, **2f**, WP0-A | proof-db/math/ axiom overlap; scripts/proof-db/proof-db.py list --field num (planned) |
| **G-discrete** | Discrete math | Combinatorial identities, finite sums | **Stub** — **WP0-A** catalog + specimens TBD | **Doc**, **2f**, WP0-A | Depends on **G-num** axiom layer |
| **G-stats** | Statistics | Estimators, CLT-class bounds (axiomatic first) | **Stub** — **WP0-A** | **Doc**, **2f**, **5b**, WP0-A | Tier-2 stats benches (planned) |
| **G-ml** | ML training safety | Optimizer step contracts, convergence guards | **Stub** — [ml-convergence-program](ml-convergence-program.md) (**WP0-C**) | **Doc**, **2f**, WP0-C | proof-db/ml/ (planned); **P-ml-convergence** |
| **G-graph** | Graph theory | Reachability, coloring bounds | **Stub** — **WP0-A** | **Doc**, **2f**, WP0-A | proof-db/graph/ (planned) |
| **G-erdos** | Erdős problem register | Curated open problems → catalog E-* | **Partial** — **WP0-B** register + sync; Lean per row **WP1+** | **Doc**, **2f**, WP0-B | proof-db/erdos/register.json, proof-db/erdos/ROADMAP.md |
| **G-chem** | Chemistry models | Stoichiometry, energy bookkeeping | **Stub** — **WP0-D** | **Doc**, **5b**, WP0-D | Tier-2 chem benches (planned) |
| **G-bio** | Biology models | Growth / sequence toy dynamics | **Stub** — **WP0-D** | **Doc**, **5b**, WP0-D | Tier-2 bio benches (planned) |

---

## `lic build` today (actual pipeline)

What **`lic build`** runs **now** (see `compiler/lic/main.cpp`):

1. `check_source_policies()` — string/heuristic policy  
2. `parse_module()`  
3. `typecheck_module()` + borrow  
4. `compile_module()` → MIR → LLVM → link `li_rt`  
5. `write_vcs_lean()` → `build/generated/AutoVC.lean` (typed `Prop` obligations)  

**`lic verify --lean`**: VC counts + `lake build` on `docs/semantics` — see `compiler/verify/`.

What **`lic build`** does **not** run yet (unless Lean 4 installed and not `--no-lean-verify`):

- Lean 4 kernel discharge of non-trivial ensures  
- Lean 4 kernel as default hard gate  
- Decorator elaboration  
- Math-shape checking beyond ordinary types  

```mermaid
flowchart LR
  subgraph today [lic build today]
    pol[policy.cpp heuristics]
    par[parse]
    tc[typecheck + borrow]
    vc[AutoVC.lean Props]
    mir[MIR + LLVM]
    pol --> par --> tc --> vc
    tc --> mir
  end
  subgraph missing [not wired]
    lean[Lean kernel discharge]
    dec[decorator elaborate]
  end
  vc -.->|Phase 2f| lean
  par -.->|Phase 7d| dec
  dec -.-> mir
```

---

## Runtime vs compile-time (honest)

| Mechanism | Intended end state | Today |
|-----------|-------------------|--------|
| Type / borrow errors | Compile-time only | **Mostly** at typecheck |
| `parallel for` races | Compile-time reject | **Heuristic** policy + tests |
| Out-of-bounds | Compile-time proof | **May** still hit `li_bounds_fail` in debug paths |
| Decorators | Never interpreted at run time | **N/A** — not executed; not elaborated yet |
| `li_panic` / contract fail | No user path in proved release | **Runtime** hooks exist in `li_rt` |
| OpenMP | Native threads | **Runtime** library (not user logic validation) |
| Fuzz / TSan | Find compiler bugs | **CI optional** — not user proof |

**Goal unchanged:** shrink the right-hand column until user logic never depends on the runtime column for correctness.

---

## Tests vs proofs

| Suite | What it proves |
|-------|----------------|
| `li-tests/race_shared_memory/` | Policy + typecheck **reject** bad parallel patterns (not Lean) |
| `li-tests/decorator_exploits/` | **Planned** — reserved names, macro hijack (7d-e) |
| `li-tests/math_linalg/` | **Partial** — 1d/2d `@`, element-wise, matmul compile tests (2i/7e) |
| `li-tests/contracts_verify/` | **Partial** — 14× `prove_lean_ok` closed corpus; `sqrt_open_bound` intentional open (`verify_open_ok`); refinements on `verify_ok` |
| `li-tests/tooling/discharge_linalg_int_lean.sh` | P-linalg closed specimens → zero open AutoVC goals |
| `li-tests/tooling/vc_emit_contracts.sh` | `sqrt_contract` AutoVC uses `≥` / `Float.abs`, not `True` stubs |
| `li-tests/tooling/discharge_trivial_lean.sh` | `discharge_trivial.li` → zero open Prop goals + `lake build` when Lean installed |
| `li-tests/prove_reject/` | Rejection of forbidden constructs (where present) |
| Fuzz (`compiler/fuzz/`) | Parser robustness — **not** end-to-end proof |

Passing **`./li-tests/run_all.sh`** means the **current** gate holds — not the full spec gate.

**Corpus inventory, run commands, and proof backlog for the master plan:** [proof-corpus-roadmap.md](proof-corpus-roadmap.md).

### Proof-db discrepancy appendix

[`../../proof-database/DISCREPANCIES.md`](../../proof-database/DISCREPANCIES.md) — `python3 scripts/proof-db/compare_reference.py --write`. Kinds: `missing_lemma`, `open_vc`, `spec_drift`, `trusted_axiom`, `hardware_axiom` (**G-hw**).

---

## Documentation that must stay aligned

When editing handbook pages, do **not** imply features beyond this register without a “**Status:** implemented” note.

| Doc | Alignment action |
|-----|------------------|
| [Contracts and proofs](../language/contracts-and-proofs.md) | Points here for `lic build` vs Lean |
| [Build pipeline](../compiler/build-pipeline.md) | Lean stage marked *planned* |
| [Why provable](../compiler/why-provable.md) | Links here under honest limits |
| [Language overview](../language/overview.md) | “Status honesty” links here |
| [SIMD and parallel](../language/simd-parallel.md) | Note heuristic disjoint until 7d-c |
| Decorator / math spec stubs | Say “planned” until gaps closed |

---

## Closing gaps (priority)

Rough order from [master plan](../superpowers/plans/2026-05-14-li-master-plan.md) § *Compiler tasks vs proof gaps*:

1. **2e** — VC generation (**G-vc**)  
2. **2f** — Lean 4 in `lic build` (**G-lean**, **G-vc**, **G-trust**)  
3. **7b / 7d-c** — structured `disjoint=` (**G-par**)  
4. **7d** — decorator elaboration (**G-dec**)  
5. **2i / 7e** — math surface (**G-math**)  

**Documentation:** Phase **Doc** (Doc-a … Doc-e) in the master plan — update this file and handbook pages in the **same PR** as each compiler row moves to **Partial** or **Done**.


<!-- source: ecosystem/agent-handover-formats.md -->

# Agent handover formats

**What this page is for:** Compare how coding agents discover repo context, tools, and errors — and what Li standardizes on.

**Prerequisites:** [agent-coordination.md](agent-coordination.md), [li-agent-manifest.toml](li-agent-manifest.toml).

## Comparison

| Format | Primary consumer | Strengths | Weaknesses for Li |
|--------|------------------|-----------|-------------------|
| **AGENTS.md** | Cursor, Codex, generic agents | Simple markdown at repo root; human + agent readable | Unstructured; drifts from CI truth |
| **Cursor rules (`.mdc`)** | Cursor | Always-on policy; globs | Editor-specific; not machine-validated |
| **A2A (Agent-to-Agent)** | Multi-agent orchestrators | Task/capability envelopes, RPC-ish | Heavy; Li not running agent mesh yet |
| **OpenAI function / tool schemas** | API agents | Strict JSON Schema; great for single-shot tools | Not a repo map; no file context |
| **MCP tool descriptors** | Cursor / Claude MCP | Discoverable tools + resources | Per-server; Li needs `lic` as first-class tool |
| **LSP** | IDEs | Locations, codes, incremental | No proof status; not all agents speak LSP |
| **Continue / Devin patterns** | SaaS agents | Handoff = issue + branch + test command | Proprietary; map to manifest commands |
| **li-agent-manifest.toml** | Li ecosystem | Canonical commands + schema paths | New; v0 stub |

## Li recommendation (v0)

Use a **layered handover**:

1. **Published handbook** — [llms.txt](https://docs.lilangverse.xyz/llms.txt) and [raw Markdown](https://docs.lilangverse.xyz/raw/for-agents.md). Chats and remote agents should fetch these, not scrape HTML. See [For agents](../for-agents.md).
2. **`AGENTS.md`** — pillar order, PR-only, three gates (short; link out).
3. **`docs/ecosystem/li-agent-manifest.toml`** — canonical commands (`check_json`, `diagnose`, `tests`, `bench`).
4. **`docs/schemas/diagnostic-v1.json`** — stable error envelope for fix loops.
5. **`.cursor/rules/*.mdc`** — editor policy (provability, llm-first token discipline).
6. **Generated (optional):** `scripts/gen-li-agent-manifest.sh` → `li-agent.json` + `.cursor/AGENTS.generated.md`.

Do **not** duplicate full language spec in handover files — link to `docs/superpowers/specs/`.

### Agent fix loop (recommended)

```mermaid
sequenceDiagram
  participant A as Agent
  participant L as lic
  participant T as li-tests
  A->>L: lic diagnose file.li
  L-->>A: diagnostic-v1 JSON
  A->>A: edit source
  A->>L: lic check file.li
  A->>T: ./li-tests/run_all.sh suite
```

## Learned from

- **LSP** — file/line/col + stable codes → Li `type.index`, `parse.indent`, etc.
- **MCP** — explicit tool list → manifest `[commands]` table.
- **AGENTS.md** — onboarding without reading entire handbook.

## Related

- [2026-05-16-li-llm-first-design.md](../superpowers/specs/2026-05-16-li-llm-first-design.md)
- [Engineering standards](https://github.com/li-langverse/roadmap/blob/main/docs/ecosystem/engineering-standards.md)


<!-- source: ecosystem/overview.md -->

# Overview

<!-- DOC-ecosystem-stub-overview.md -->

**Canonical doc:** [overview.md](https://github.com/li-langverse/roadmap/blob/main/docs/ecosystem/overview.md) in [`li-langverse/roadmap`](https://github.com/li-langverse/roadmap).

Do not edit ecosystem policy here — open a PR to the roadmap repo (human merge for governance paths).

## Related

- [Roadmap milestones](https://github.com/li-langverse/roadmap/blob/main/docs/roadmap/milestones.md)
- [Benchmarks dashboard](https://li-langverse.github.io/benchmarks/)
- [lic master plan](https://github.com/li-langverse/lic/blob/main/docs/superpowers/plans/2026-05-14-li-master-plan.md)


<!-- source: contributing/documentation.md -->

# Documentation style guide

> **Repository:** Edit handbook pages in [li-langverse/lic-docs](https://github.com/li-langverse/lic-docs). This file is published at [li-langverse.github.io/lic-docs](https://li-langverse.github.io/lic-docs/contributing/documentation/).
Li docs should read like a clear technical blog post: precise, friendly, and useful on first read. This guide applies to everything under `docs/` and the root `README.md`.

## Audience

Assume the reader:

- Writes code in Python, Rust, Nim, or C++  
- Cares about simulation/HPC correctness and performance  
- Does **not** already know Li’s phase plan or internal module names  

Define terms on first use. Link to the design spec instead of copying ten-page tables.

Agents and chats should ingest [For agents](../for-agents.md) — `llms.txt` and `raw/*.md` — not the styled HTML. When you add a nav page that agents should know, add a blurb in `scripts/export-agent-docs.py`.

## Voice and tone

**Do:**

- Use full sentences  
- State the goal of the page in the first paragraph  
- Explain *why* a design choice exists (e.g. LLVM-only, Python 3.14 types)  
- Give copy-pasteable commands and small complete examples  

**Avoid:**

- Bullet-only pages with no connective prose  
- Internal codenames without context  
- “Simply” / “just” when the step is not simple  
- Promising dates without pointing to the master plan phases  
- Claiming **`lic build` runs Lean** or full proof discharge before **Phase 2f** lands  

## Provability and “today vs target”

When documenting proofs, `lic build`, decorators, parallelism, or math notation:

1. Read **[Provability gaps](../verification/provability-gaps.md)** first.  
2. Use **target** vs **today** language (see that page’s summary table).  
3. When a gap closes in code, update the **gap register** in the **same PR** as the implementation.  

Handbook pages should link to the gap doc where the spec promise exceeds the compiler.

## Page template

```markdown
# Title

One sentence: what this page helps you do.

## Background (optional, 1 short paragraph)

## Main content (sections with headings)

## Traceability and official packages

When documenting **standard** or **first-party** packages:

- Assign a `PKG-*` id and list it in [official-packages.md](../ecosystem/official-packages.md) (see [ecosystem governance plan](../superpowers/plans/2026-05-16-li-ecosystem-governance.md)).
- Link tests via `T-*` notes in `li-tests/manifest.toml` where behavior is normative.
- Use **Keep a Changelog** and **SemVer** for release notes; **SPDX** license identifiers in `li.toml`.

Ecosystem pages use HTML comments for doc IDs: `<!-- DOC-ecosystem-lip -->` (optional, for traceability tooling).

## Related links
```

## Code examples

- Shell blocks: full commands, no `...`  
- Li surface syntax: use ` ```nim ` fences (indentation-based)  
- When teaching types, show one valid example and one compile error  

Example:

```nim
type Board = array[20, array[10, Cell]]   # OK
# board[25, 0] = ...                       # error: row index out of range
```

## Linking

- Prefer relative links within `docs/`  
- Point to the [language design spec](../superpowers/specs/2026-05-14-li-language-design.md) for normative rules  
- Point to [phase plans](../superpowers/plans/2026-05-14-li-master-plan.md) for implementation order  

## Diagrams

Use Mermaid or ASCII for pipelines and phase order when it saves a paragraph of confusion.

## Keeping docs honest

Mark pages **Planning** vs **Active** when the compiler lands. If CMake flags or CLI names change, update `getting-started.md` in the same PR as the code.

## Cursor rules

Editor agents load rules from `.cursor/rules/`:

| Rule | Scope |
|------|--------|
| `li-project.mdc` | Always — project context |
| `documentation-style.mdc` | `docs/**`, README |
| `li-language.mdc` | `**/*.li` |
| `compiler-cpp.mdc` | `compiler/**` |
| `benchmarks.mdc` | `benchmarks/**` |