# LOGOS — full documentation for language models

This is the llms-full.txt companion to /llms.txt: the complete LOGOS
curriculum in one file. LOGOS is the English programming language —
https://logicaffeine.com — and its toolchain is also an MCP server
(`claude mcp add logos -- largo mcp`).


================================================================
SOURCE: LOGOS_QUICKGUIDE.md — LOGOS Quickguide — the whole language on one page
================================================================

# LOGOS Quick Guide

How to write and work with every construct in LOGOS, in one place. Each table
shows the **canonical** form, the **ambiguous alternatives that also parse** (LOGOS
supports many surfaces for one meaning), and what it **lowers to** internally.

Forms marked **(proposed)** are designed but not yet implemented — they are
listed here so this guide doubles as the target spec. Everything not so
marked works in-tree today.

---

## 1. Program structure

LOGOS source is literate Markdown; `##` headers introduce definitions.

| Construct | Form | Notes |
|-----------|------|-------|
| Entry point | `## Main` | the program body |
| Function | `## To f (n: Int) -> Int:` | return type optional |
| Procedure | `## To greet (name: Text):` | no return |
| Native import | `## To native parseInt (s: Text) -> Int` | FFI declaration |
| Struct | `## A Point has:` | fields indented below |
| Enum | `## A Shape is one of:` | variants indented below |
| Theorem | `## Theorem: Socrates` | with `Given/Prove/Proof: Auto.` |

---

## 2. Variables & mutation

| Meaning | Canonical | Also works | Lowers to |
|---------|-----------|------------|-----------|
| Bind | `Let x be 5.` | `Let x: Int be 5.` | `Stmt::Let` |
| Mutable bind | `Let mutable x be 5.` | `Let mut x be 5.` | `Stmt::Let{mutable}` |
| Reassign | `Set x to 10.` | — | `Stmt::Set` |
| Increment | `Set i to i + 1.` | **(proposed)** `Increase i by 1.` · `i += 1.` | `Stmt::Set` |
| Decrement | `Set i to i - 1.` | **(proposed)** `Decrease i by 1.` · `i -= 1.` | `Stmt::Set` |

---

## 3. Arithmetic, comparison, logic, bitwise

| Meaning | Symbolic | English | Lowers to |
|---------|----------|---------|-----------|
| Add / sub | `x + y` · `x - y` | — | `BinaryOp Add/Subtract` |
| Mul / div / mod | `x * y` · `x / y` · `x % y` | — | `Multiply/Divide/Modulo` |
| Concatenate (Text) | **(proposed)** `"a" + "b"` | `"a" combined with "b"` | `BinaryOp Concat` |
| Equal | `x == y` | `x equals y` · `x is equal to y` | `Eq` |
| Not equal | `x != y` | `x is not y` | `NotEq` |
| Greater / less | `x > y` · `x < y` | `x is greater than y` · `x is less than y` | `Gt/Lt` |
| ≥ / ≤ | `x >= y` · `x <= y` | `x is at least y` · `x is at most y` | `GtEq/LtEq` |
| Chained | `lo <= x <= hi` | — | `(lo <= x) and (x <= hi)` |
| Range test | — | `x is between lo and hi` | inclusive `lo <= x and x <= hi` |
| Parity / divisibility | — | `x is even` · `x is odd` · `x is divisible by n` | `x % 2 == 0` · `== 1` · `x % n == 0` |
| Logical | — | `a and b` · `a or b` · `not a` | `And/Or/Not` (truthiness → Bool, short-circuit) |
| Bitwise and/or | `x & y` · `x \| y` | — | `BitAnd/BitOr` (Set: intersection/union) |
| Bitwise xor | `x ^ y` | `x xor y` | `BitXor` (Set: symmetric difference) |
| Bitwise not | `~x` | — | lowers to `x ^ -1` |
| Shift | — | `x shifted left by n` · `x shifted right by n` | `Shl/Shr` |
| Negate | `-x` | — | `0 - x` |
| Popcount | — | `count_ones(x)` | builtin |

Note: `and`/`or`/`not` are LOGICAL — truthiness in, `Bool` out, short-circuit. Falsy:
`false`, `0`, `0.0`, `nothing`, empty Text/Seq/Map/Set (so `If items:` tests emptiness).
The bitwise spellings are the symbols `&`/`|`/`^`/`~`; on Sets, `&`/`|`/`^`/`-` are
intersection/union/symmetric-difference/difference (`a without b` is the English difference).

---

## 4. Strings

| Meaning | Canonical | Also works | Lowers to |
|---------|-----------|------------|-----------|
| Concatenate | `a combined with b` | **(proposed)** `a + b` | `Concat` |
| Interpolate | `"Hello, {name}!"` | — | `InterpolatedString` |
| Format precision | `"{pi:.2}"` | — | `StringPart{format_spec}` |
| Align | `"{s:>10}"` · `"{s:<10}"` · `"{s:^10}"` | — | format spec |
| Debug | `"{v=}"` | — | format spec `debug` |
| Currency | `"{price:$}"` | — | format spec |
| Multiline | `"""…"""` | — | literal |
| split/join/trim/case/replace | **(proposed)** `s.split(",")` · `join(parts, ", ")` | — | new builtins (phantom today) |

---

## 5. Collections

### 5.1 Create

| Type | Canonical | Also works | Lowers to |
|------|-----------|------------|-----------|
| List, empty | `a new Seq of Int` | `a new List of Int` · `a new Vec of Int` · `[] of Int` · **(proposed)** `a new Array of Int` | `Expr::New{Seq}` |
| List, literal | `[1, 2, 3]` | — | `Expr::List` |
| List, pre-sized | `a new Seq of Int with capacity n` | — | `Expr::WithCapacity` |
| Map, empty | `a new Map of Text to Int` | `a new HashMap of Text to Int` · **(proposed)** `a new Dictionary of …` | `Expr::New{Map}` |
| Map, with capacity | `a new Map of Int to Int with capacity n` | — | `WithCapacity` |
| Map, literal | **(proposed)** `{ "a": 1, "b": 2 }` · empty `{} of Text to Int` | — | `New{Map}` + inserts |
| Set, empty | `a new Set of Int` | `a new HashSet of Int` | `Expr::New{Set}` |
| Set, literal | **(proposed)** `{1, 2, 3}` (no `:` ⇒ set) | — | `New{Set}` + adds |

### 5.2 Read, write, slice

| Meaning | Canonical | Also works | Lowers to |
|---------|-----------|------------|-----------|
| Index read (1-based) | `item i of xs` | `xs[i]` · **(proposed)** `xs at i` | `Expr::Index` |
| Map lookup | `item k of m` | `m[k]` | `Expr::Index` |
| Index write | `Set item i of xs to v` | `Set xs[i] to v` | `Stmt::SetIndex` |
| Map insert | `Set m at k to v` | `Set item k of m to v` · `Set m[k] to v` | `SetIndex` |
| Slice (inclusive) | `items a through b of xs` | `items a through b` (collection inferred) · **(proposed)** `xs[a:b]` | `Expr::Slice` |
| Length | `length of xs` | `length(xs)` · **(proposed)** `xs.length` | `Expr::Length` |
| Membership | `xs contains v` | `v in xs` | `Expr::Contains` |
| Copy | `copy of xs` | `copy(xs)` | `Expr::Copy` |

> ⚠️ Indexing is **1-based**: `item 1 of xs` and `xs[1]` are the *first* element.
> `item 0 of xs` is a compile error; `xs[0]` currently underflows.
> A project may opt into 0-based indexing
> **(proposed)** via `logos.toml`.

### 5.3 Mutate (lists & sets)

| Meaning | Form | Lowers to |
|---------|------|-----------|
| Append | `Push v to xs.` | `Stmt::Push` |
| Pop | `Pop from xs.` · `Pop from xs into y.` | `Stmt::Pop` |
| Set add | `Add v to s.` | `Stmt::Add` |
| Set remove | `Remove v from s.` | `Stmt::Remove` |
| Union / intersection | `a union b` · `a intersection b` | `Union`/`Intersection` |

### 5.4 Iterate & transform

| Meaning | Canonical | Also works | Lowers to |
|---------|-----------|------------|-----------|
| For-each | `Repeat for x in xs:` | `for x in xs:` · `Repeat x in xs:` | `Stmt::Repeat` |
| Counted | `for i from 1 to n:` | `Repeat for i from 1 to n:` | `Repeat` over `Range` |
| Pairs (map) | `Repeat for (k, v) in m:` | — | `Repeat` + tuple `Pattern` |
| Map / filter | **(proposed)** `[f(x) for x in xs if p(x)]` · `xs.map(f)` · `each x in xs mapped to f(x)` | — | desugar to `Repeat`+`Push` |
| Reduce / sum | **(proposed)** `the sum of xs` · `xs.reduce(...)` | — | new builtins |
| Sort | **(proposed)** `xs sorted` · `xs sorted by (x) -> x's age` · `xs.sort()` | — | new builtins |
| any / all / count | **(proposed)** `every x in xs satisfies p` · `xs.any(p)` | — | new builtins |

---

## 6. Control flow

| Construct | Form | Notes |
|-----------|------|-------|
| If / else | `If c:` … `Otherwise:` … | `Stmt::If` |
| Else-if | `elif c:` · `Else If c:` · `Otherwise If c:` | all valid; **canonical: `elif`** |
| While | `While c:` | `Stmt::While` |
| While + variant | `While c (decreasing e):` | termination proof |
| Break | `Break.` | innermost loop |
| Return | `Return x.` · `Return.` | `Stmt::Return` |
| Conditional value | **(proposed)** `a if c else b` | `Expr::IfExpr` |
| Match | `Inspect t:` `When V (a, b):` … `Otherwise:` … | `Stmt::Inspect` |

---

## 7. Functions & closures

| Construct | Form | Notes |
|-----------|------|-------|
| Define | `## To add (a: Int, b: Int) -> Int:` | comma params work today |
| Define (prose) | `## To add (a: Int) and (b: Int) -> Int:` | `and` between groups optional |
| Define (prepositional) | `## To withdraw (amount: Int) from (balance: Int):` | prepositions allowed |
| Call | `add(3, 7)` | `Expr::Call` |
| Call (statement) | `Call process with data.` · `Call f with a and b.` | `Stmt::Call` |
| Closure (expr) | `(x: Int) -> x + 1` | `Expr::Closure` |
| Closure (block) | `(x: Int) ->:` then indented body with `Return` | `Closure{Block}` |
| HOF parameter | `## To apply (f: fn(Int) -> Int) and (x: Int) -> Int:` | function-typed param |
| Return a closure | `Return (x: Int) -> x + n.` | closures are first-class |
| Call a closure value | `f(42)` | `Expr::CallExpr` |

---

## 8. Structs, enums & field access

| Construct | Form | Also works | Lowers to |
|-----------|------|------------|-----------|
| Struct def | `## A Point has:` then `An x: Int.` `A y: Int.` | — | `StructDef` |
| Construct | `a new Point` | `a new Point with x 10 and y 20` | `Expr::New` |
| Field read | `p's x` | `p.x` | `FieldAccess` |
| Nested field | `b's location's x` | `b.location.x` | chained `FieldAccess` |
| Field write | `Set p's x to 5.` | `Set p.x to 5.` · `p.x = 5.` | `SetField` |
| Method (UFCS) | `f(xs, a)` | `xs.f(a)` · `xs.f().g()` · `(5).double()` | same `Call` (receiver is arg 0) |
| Enum def | `## A Shape is one of:` then `A Circle with radius Int.` | — | enum `StructDef` |
| Variant construct | `a new Circle with radius 10` | — | `NewVariant` |
| Match variant | `Inspect s:` `When Circle (r):` … | — | `Inspect` |

---

## 9. Options & pattern matching

| Meaning | Form | Lowers to |
|---------|------|-----------|
| Some | `some 30` | `OptionSome` |
| None | `none` | `OptionNone` |
| Match | `Inspect maybe:` `When OptionSome (v):` … `When OptionNone:` … | `Inspect` |
| Optional chaining | **(proposed)** `p?.address?.city` | future |

---

## 10. Contracts: refinement, assert, trust, check

| Meaning | Form | Notes |
|---------|------|-------|
| Refinement type | `Let x: Int where x > 0 be 5.` | constraint binds the declared name |
| Compound refinement | `Let x: Int where x > 0 and x < 100 be 50.` | — |
| Assert (debug) | `Assert that x is equal to 42.` | `RuntimeAssert` |
| Trust (justified) | `Trust that x is greater than 0 because "set to 10".` | carries a reason |
| Check (mandatory) | `Check that balance is at least amount.` | security gate |

---

## 11. Temporal literals

| Kind | Examples |
|------|----------|
| Duration | `50ns` · `100us` · `500ms` · `2s` · `5min` · `1h` |
| Date | `2026-05-20` |
| Time of day | `9am` · `4pm` · `noon` · `9:30am` |
| Calendar span | `2 weeks` · `3 months` · `1 year and 2 months and 5 days` |
| Combined | `2026-05-20 at 4pm` |

---

## 12. Distributed: CRDT, concurrency, networking, zones

| Construct | Form | Notes |
|-----------|------|-------|
| Shared struct | `A Counter is Shared and has:` then `points: ConvergentCount.` | CRDT field types |
| CRDT increment | `Increase c's points by 10.` | `IncreaseCrdt` (CRDT fields only today) |
| CRDT decrement | `Decrease g's score by 30.` | `DecreaseCrdt` |
| CRDT merge | `Merge remote into local.` | conflict-free |
| Shared set | `Add "Alice" to p's guests.` | ORSet semantics |
| Shared sequence | `Append "Line 1" to doc's lines.` | RGA semantics |
| Spawn agent | `Spawn an EchoAgent called "echo".` | actor |
| Zone (arena) | `Inside a zone called "Scratch":` | scoped allocation |
| Listen | `Listen on "/ip4/0.0.0.0/tcp/8000".` | raw multiaddr (low-level) |

---

## 13. Output

| Meaning | Form |
|---------|------|
| Print | `Show x.` · `Show "Hello, World!".` |
| Print formatted | `Show "{result:.15}".` |
| Move into a sink | `Give x to consume.` (ownership move) · `Show x to display.` (borrow) |

---

### Legend

- **(proposed)** — designed but not yet implemented.
- "Lowers to" names the AST node in `crates/logicaffeine_language/src/ast/stmt.rs`.
- Everything unmarked parses in-tree today.


================================================================
SOURCE: docs/architecture.md — Architecture
================================================================

# Architecture

How Logicaffeine is put together: the compilation pipeline, the crate tier graph, the four
dependency invariants that keep it honest, and the dual-AST model that lets one parser serve both
modes.

## The pipeline

One front-end, two modes, many back-ends. The parser switches mode on block headers (`## Main` /
`## To …` select the imperative grammar; otherwise the declarative/logic grammar applies).

```
                         English source
                              │
                         Lexer  (logicaffeine_language: lexer.rs)
                              │  tokens
                         Parser (logicaffeine_language: parser/)
                         ┌────┴────┐
              Declarative│         │Imperative
                         ▼         ▼
                  LogicExpr AST   Stmt/Expr AST
                  (ast/logic.rs)  (ast/stmt.rs)
                         │         │
                         ▼         ▼
                  Transpile      Analysis (types, ownership)
                  → FOL          │
            (Unicode/LaTeX/      ├─ Tree-walking interpreter
             SimpleFOL/Kripke)   ├─ Bytecode VM ──► copy-and-patch JIT (native)
                                 ├─ AOT Rust codegen
                                 ├─ Direct WASM backend (--emit wasm, no rustc)
                                 ├─ AOT C codegen (benchmark subset)
                                 └─ SVA/PSL codegen (hardware verification)
```

The declarative side can also feed the **proof engine** (`logicaffeine_proof`) and, when enabled,
**Z3 verification** (`logicaffeine_verify`). See [Logic mode](logic-mode.md),
[Execution & performance](execution-and-performance.md), and
[Proof & verification](proof-and-verification.md).

## The dual-AST model

| Mode | Block header | AST | Output |
|------|-------------|-----|--------|
| Declarative | `## Theorem`, default | `LogicExpr` ([`ast/logic.rs`](../crates/logicaffeine_language/src/ast/logic.rs)) | First-Order Logic |
| Imperative | `## Main`, `## To …` | `Stmt` / `Expr` ([`ast/stmt.rs`](../crates/logicaffeine_language/src/ast/stmt.rs)) | Executable code |

The **Assert Bridge** connects them: an imperative program can `Assert that <logic>`, tying
verifiable logical claims to executable code.

## The crate tier graph

Crates are layered so dependencies only ever point *down* a tier. Tiers are reconstructed from the
actual `Cargo.toml` dependency edges.

```
Tier 0   base · runtime · forge                  (no internal deps)
Tier 1   lexicon · kernel · data                 → base
Tier 2   system · proof                          → base, (data | kernel)
Tier 3   language · compile                       → tiers 0–2
Tier 4   jit · lsp · cli · web                    → tiers 0–3
Z3-gated verify · tv · synth                       (opt-in; outside default-members)
```

| Crate | Tier | Role |
|-------|------|------|
| [base](../crates/logicaffeine_base/README.md) | 0 | Arenas, interning, spans, errors |
| [runtime](../crates/logicaffeine_runtime/README.md) | 0 | Deterministic concurrency runtime (tokio-free, WASM-safe) |
| [forge](../crates/logicaffeine_forge/README.md) | 0 | Copy-and-patch JIT executable-memory layer (native) |
| [lexicon](../crates/logicaffeine_lexicon/README.md) | 1 | English vocabulary types + compile-time lexicon |
| [kernel](../crates/logicaffeine_kernel/README.md) | 1 | Calculus of Constructions + decision procedures |
| [data](../crates/logicaffeine_data/README.md) | 1 | Runtime values + CRDTs (IO-free) |
| [system](../crates/logicaffeine_system/README.md) | 2 | Platform IO, networking, persistence |
| [proof](../crates/logicaffeine_proof/README.md) | 2 | Backward-chaining proof engine + Socratic hints |
| [language](../crates/logicaffeine_language/README.md) | 3 | English → First-Order Logic pipeline |
| [compile](../crates/logicaffeine_compile/README.md) | 3 | LOGOS compilation, interpretation, and codegen |
| [jit](../crates/logicaffeine_jit/README.md) | 4 | Wires the forge JIT into the VM (native) |
| [lsp](../crates/logicaffeine_lsp/README.md) | 4 | Language Server Protocol |
| [verify](../crates/logicaffeine_verify/README.md) | — | Z3 static verification |
| [tv](../crates/logicaffeine_tv/README.md) | — | SMT translation validation |
| [synth](../crates/logicaffeine_synth/README.md) | — | EXODIA stencil synthesis & witness checking |

> `verify`, `tv`, `synth`, and `wirebench` are excluded from `default-members` in the root
> [`Cargo.toml`](../Cargo.toml), so a plain `cargo build`/`cargo test` needs no Z3 toolchain. They
> build whenever the `verification` feature pulls them in.

## The four invariants

Each is a deliberate *absent* dependency, enforced at the crate boundary and documented in the
crate's own source. They keep components reusable and portable:

| Invariant | Crate | The forbidden dependency | Why |
|-----------|-------|--------------------------|-----|
| **Milner** | `kernel` | no path to the lexicon ([`kernel/src/lib.rs`](../crates/logicaffeine_kernel/src/lib.rs), `kernel/Cargo.toml`) | the type theory never sees English words, so the lexicon can change without touching the kernel |
| **Liskov** | `proof` | no dependency on `language` ([`proof/Cargo.toml`](../crates/logicaffeine_proof/Cargo.toml)) | the proof engine is reusable across front-ends |
| **Lamport** | `data` | no IO dependencies ([`data/src/lib.rs`](../crates/logicaffeine_data/src/lib.rs), `data/Cargo.toml`) | data structures stay WASM-safe and clock-agnostic |
| **Tarski** | `verify` | verification IR decoupled from the main AST ([`verify/src/lib.rs`](../crates/logicaffeine_verify/src/lib.rs)) | verification is front-end-agnostic |

## Platform gating

- **Native-only**: `forge` and `jit` (executable-memory JIT), plus the work-stealing scheduler in
  `runtime` — all `cfg`-gated off `wasm32`.
- **WASM**: the `web` app and the full engine (parser, interpreter, VM, proof engine, codegen) run
  in the browser; `system` abstracts IO across native and WASM targets.

## Where to look next

- The execution tiers in detail → [Execution & performance](execution-and-performance.md)
- The test suite as the living spec → [`crates/logicaffeine_tests/`](../crates/logicaffeine_tests/)
- Each crate's own `README.md` for its public API

---
[Docs index](README.md) · [Root README](../README.md) · [Changelog](../CHANGELOG.md)


================================================================
SOURCE: docs/cli.md — The largo CLI
================================================================

# The `largo` CLI

`largo` is the LOGOS build tool and package manager — Cargo for English, and the front door to the
whole engine. It scaffolds projects, compiles LOGOS to Rust (and on to a native binary) or directly
to WASM, runs programs through the interpreter, hosts the interactive REPL, translates English to
First-Order Logic, proves theorems kernel-certified, solves DIMACS SAT instances, formats source,
performs static verification, and talks to the package registry.

Source of truth: [`apps/logicaffeine_cli/src/cli.rs`](../apps/logicaffeine_cli/src/cli.rs) (the
command surface) and [`apps/logicaffeine_cli/src/project/`](../apps/logicaffeine_cli/src/project/)
(manifest, build, registry, credentials).

## Installing

One line on Linux and macOS (x64 + arm64):

```bash
curl -fsSL https://logicaffeine.com/install.sh | sh
```

Windows (x64):

```powershell
powershell -ExecutionPolicy Bypass -c "irm https://logicaffeine.com/install.ps1 | iex"
```

The installer downloads the prebuilt binary for your platform from the GitHub release, verifies
its SHA-256 against the release's `SHA256SUMS`, and installs it atomically as `largo` in
`~/.local/bin` (Windows: `%LOCALAPPDATA%\Programs\largo`). It never uses sudo and never edits
shell configuration — if the directory isn't on your `PATH`, it prints the exact line to add.

| Flag | Effect |
|------|--------|
| `--full` | Install the full build: Z3 static verification bundled (`largo verify` works out of the box; still license-gated at runtime). ~30 MB larger. |
| `--version vX.Y.Z` | Install an exact release instead of the latest. |
| `--to DIR` | Install directory override (also: `LARGO_INSTALL_DIR`). |

Both flavors install as `largo`; `largo --version` reports `X.Y.Z (full)` for the full build.
Prebuilt platforms: `linux-x64`, `linux-arm64`, `darwin-x64`, `darwin-arm64`, `win32-x64`.
Re-running the installer upgrades in place. Uninstall by deleting the binary.

### From source

```bash
cargo install logicaffeine-cli           # needs a Rust toolchain
# or, in the repo:
cargo build -p logicaffeine-cli          # debug build → target/debug/largo
cargo build -p logicaffeine-cli --release
```

## Commands

The full subcommand set (from the `Commands` enum in `cli.rs`):

**Project**

| Command | Purpose |
|---------|---------|
| `largo new <name>` | Scaffold a new project in a new `<name>/` directory |
| `largo init [--name <name>]` | Scaffold a project in the current directory |
| `largo add <spec> [--path\|--git]` | Add a dependency to `Largo.toml` (format-preserving edit) |
| `largo remove <name>` | Remove a dependency from `Largo.toml` |
| `largo clean [--all]` | Delete `target/` (`--all` also clears the `.logos-native/` cache) |

**Build & run**

| Command | Purpose |
|---------|---------|
| `largo build [flags]` | Compile LOGOS → Rust, then `cargo build` the result (or `--emit wasm`) |
| `largo run [flags] [-- args…]` | Build and run — compiled, interpreted, or as WASM; `--max-steps` / `--timeout` / `--seed` / `--json` bound and reproduce runs |
| `largo check [--deep] [--json]` | Parse + type-check without producing a binary |
| `largo emit rust\|c\|wasm\|wasm-linked [file] [-o path]` | Print/write the compiled translation without building a binary |
| `largo fmt [paths…] [--check] [--json]` | Format LOGOS sources (same rules as the language server) |
| `largo opts <file> [--json]` | Report which optimizations actually fired for a file |

**Agents**

| Command | Purpose |
|---------|---------|
| `largo explain <topic> [--json]` | Look up a diagnostic code or a construct, offline |
| `largo mcp` | Serve the whole toolchain over the Model Context Protocol (stdio) |

**Logic, proof & SAT**

| Command | Purpose |
|---------|---------|
| `largo logic "<sentence>" [flags]` | English → First-Order Logic from the terminal |
| `largo prove [file] [--trace\|--json]` | Prove `## Theory` / `## Theorem` blocks, kernel-certified |
| `largo sat <file.cnf> [--proof <path>] [--stats]` | The certified SAT engine on DIMACS CNF (exit 10/20) |
| `largo verify [--license <key>]` | Run Z3 static verification only (Pro+) |

**Interactive & docs**

| Command | Purpose |
|---------|---------|
| `largo repl [--logic] [--format <f>] [--load <file>]` | The interactive session (imperative + logic modes) |
| `largo doc [--out <dir>]` | Generate markdown docs from the project's `##` blocks |

**Registry**

| Command | Purpose |
|---------|---------|
| `largo publish [flags]` | Package and upload to the registry |
| `largo login [--registry <url>] [--token <key>]` | Store a registry token |
| `largo logout [--registry <url>]` | Remove stored credentials |

**Environment**

| Command | Purpose |
|---------|---------|
| `largo doctor [--registry <url>]` | Diagnose the toolchain, wasm32 target, node, registry, project health |
| `largo completions <shell>` | Shell completions (bash, zsh, fish, powershell, elvish) |

Every command takes the global flags `-q/--quiet`, `-v/--verbose` (repeatable), and
`--color auto|always|never` (`NO_COLOR` respected). `largo test` is reserved for the future LOGOS
test framework.

### `new` / `init`

`new` creates `<name>/` containing a `Largo.toml`, a `src/main.lg` entry point with a hello-world
example, a `.gitignore`, and an `AGENTS.md` that teaches AI agents the check/run loop and the
classic LOGOS mistakes. `init` does the same in an existing directory (the package name
defaults to the directory name, or `--name`).

```bash
largo new my_project
cd my_project
largo run
```

### `build`

Compiles the LOGOS source to Rust, then invokes `cargo build` on the generated crate.

| Flag | Effect |
|------|--------|
| `-r`, `--release` | Optimized build |
| `--verify` | Run Z3 static verification after compilation (needs a Pro+ license) |
| `--license <key>` | License key for verification (or set `LOGOS_LICENSE`) |
| `--lib` | Generate a library (`lib.rs`, `crate-type = ["cdylib"]`) instead of a binary |
| `--target <triple>` | Cross-compile; `wasm` is shorthand for `wasm32-unknown-unknown` |
| `--native-functions` | Pre-build every `is exported for native` function into a cached cdylib under `.logos-native/` |
| `--emit wasm` | Compile DIRECTLY to a self-contained `target/<name>.wasm` via the built-in backend — no rustc, cargo, or wasm-bindgen in the loop; milliseconds |
| `--emit wasm-linked` | As `--emit wasm`, but links the real `logicaffeine_base::BigInt` runtime via `rust-lld`, so overflowing integer arithmetic computes the exact big number instead of wrapping (needs the Rust toolchain + a wasm32 `base` build) |

### `run`

`largo build` followed by executing the binary; the program's exit code is propagated.

| Flag | Effect |
|------|--------|
| `-r`, `--release` | Optimized build before running |
| `-i`, `--interpret` | Skip Rust compilation; execute via the tree-walking interpreter for sub-second feedback |
| `--emit wasm` \| `wasm-linked` | Compile directly to `.wasm` (built-in backend) and run it through the emitted Node.js host shim — compile-and-run in one step |
| `--max-steps <N>` | Stop the interpreter after N engine steps — deterministic (the identical op on every run, JIT tiering suspended so nothing escapes the count). Exhaustion exits **122** with the partial output delivered. The safety rail for running generated code |
| `--timeout <dur>` | Kill the run (`500ms`, `10s`, `2m`) after the wall clock expires — works on the interpreter AND the compiled child. Expiry exits **124** (the GNU timeout convention) |
| `--seed <N>` | Set `LOGOS_SEED` for this run (and any compiled child): concurrent scheduling reproduces byte-for-byte |
| `--json` | Print one `logos-run/1` envelope on stdout: `outcome` (`ok` \| `runtime-error` \| `budget-exceeded` \| `timeout`), `lines`, `error`, `steps_used` |
| `-- <args…>` | Arguments passed through to the program |

### `check`

Parses and type-checks without the full build pipeline — fast validation during development.
`--deep` also runs rustc's analysis over the generated code (the same pass the IDE's flycheck
uses) and translates its findings back to LOGOS terms.

`--json` prints one `logos-check/1` envelope on stdout — `ok` plus `diagnostics`, each carrying
a stable kebab-case `code` (see [ERROR_CATALOG.md](ERROR_CATALOG.md)), byte and line/column
spans, a one-line `message`, the full Socratic `explanation`, and a `suggestion` when a close
known word exists. The human prose keeps flowing to stderr; exit codes are unchanged. This is
the same diagnostic object the MCP `logos_check` tool returns. `largo build --json` speaks the
same envelope (a cargo-phase failure reports as one `build-failure` diagnostic).

```bash
largo check --json
largo check --json | jq -r '.diagnostics[0].code'
```

### `opts`

Compiles a `.lg` file on the AOT, run-path, and VM-compile paths with the optimization firing trace
on, then lists the optimizations that *genuinely changed* the program (not merely the ones enabled).
`--json` emits the fired-optimization keyword list as JSON.

```bash
largo opts src/main.lg
largo opts src/main.lg --json
```

### `verify`

Runs Z3 static verification of the project's logical constraints without building, gated on a Pro+
license (via `--license` or the `LOGOS_LICENSE` environment variable). See
[Proof & verification](proof-and-verification.md).

> The verifier ships behind a build-time gate: a default `largo` build answers `verify` (and
> `build --verify`) with a notice that verification has to be compiled in, because it pulls in the
> Z3-backed [`logicaffeine_verify`](../crates/logicaffeine_verify/README.md) crate (kept out of the
> default build so the common path needs no Z3 toolchain).

### `publish` / `login` / `logout`

`publish` packages the project as a tarball and uploads it. Pre-flight checks confirm the entry
point exists, the git working directory is clean (override with `--allow-dirty`), and the auth token
is valid. `--dry-run` validates without uploading; `--registry <url>` overrides the default.

`login` stores an API token (interactive prompt, or `--token`); `logout` removes it. Tokens live in
`~/.config/logos/credentials.toml`.

### `emit`

Prints the generated Rust or C translation of the program, or writes a self-contained `.wasm`
module (built-in backend, no rustc) with its Node.js host shim. Without a file argument it uses the
current project's entry; with one, it works on any standalone `.lg`/`.md` source. `-o` writes to a
path instead of stdout (rust/c) or the default module path (wasm).

```bash
largo emit rust                       # generated Rust on stdout
largo emit c standalone.lg            # the C translation of one file
largo emit wasm-linked -o dist/app.wasm
```

### `fmt`

Applies the canonical style (4-space indentation, no tabs, no trailing whitespace) — the exact
rules the language server's formatting provider uses, so the CLI and the editor can never disagree.
Without paths it formats the whole project; with paths, exactly those files. `--check` writes
nothing and exits 1 if anything would change (the CI gate). `--check --json` prints one
`logos-fmt/1` envelope (`clean` + `unformatted`) instead of the plain file list.

### `add` / `remove`

Format-preserving `Largo.toml` edits (comments and layout survive). `add` accepts `name` (any
version), `name@version`, or `logos:name` (the registry URI form); `--path` and `--git` record
local and git dependencies. `remove` deletes the named `[dependencies]` entry and leaves the rest
of the manifest byte-identical.

### `clean`

Deletes the project's `target/` directory. `--all` also removes the `.logos-native/`
compiled-function bundle cache produced by `largo build --native-functions`.

### `repl`

The interactive session — two modes in one. `logos>` runs imperative statements against a
persistent interpreter session (the exact `run --interpret` engine, so REPL semantics cannot drift
from program semantics); `logic>` is English → FOL with discourse-aware anaphora. `:help` lists the
meta-commands (`:mode`, `:format`, `:readings`, `:vars`, `:explain <word>`, `:save` — which writes
the session back out as a runnable program). Line editing and keyword completion on a TTY; a plain
scriptable line loop on a pipe.

```bash
largo repl
largo repl --logic --format latex
printf 'Let x be 5.\nShow x.\n' | largo repl
```

### `logic`

Logic mode from the terminal: compiles an English sentence (inline, `--file`, or piped stdin) to
First-Order Logic, printing bare FOL on stdout so it pipes cleanly. `--format
unicode|latex|ascii|kripke` selects the rendering, `--all-readings` enumerates every quantifier
scope and parse-forest reading (numbered), `--pragmatic` enriches with scalar implicature, and
`--discourse` treats each input line as one sentence of a discourse with shared anaphora context.

```bash
largo logic "Every woman loves a man." --all-readings
printf 'A farmer owns a donkey.\nHe feeds it.' | largo logic --discourse
```

### `prove`

Proves the theorems in a LOGOS source file: `## Theory` developments (formal Axiom/Theorem
declarations, proved in citation order) and English `## Theorem` blocks (Given/Prove/Proof) run
through the proof engine, and every ✓ is certified by the type-theory kernel — a mere derivation
never counts. `--trace` renders the derivation tree under each proved theorem; `--json` emits
machine-readable results.

### `sat`

The SAT Competition interface as a largo verb: solves a DIMACS CNF with the certified engine,
printing `s SATISFIABLE` with a `v` model or `s UNSATISFIABLE`, with competition exit codes
(10 = SAT, 20 = UNSAT, 1 = error). `--proof <path>` exports the UNSAT certificate (DRAT; DPR/SR
for the symmetry routes) for external checkers like drat-trim; `--stats` prints solver statistics
to stderr.

### `doc`

Renders a markdown reference from the literate structure of the entry file — `## To` signatures,
type definitions, notes, examples, and formal blocks, in source order (`## Main` is omitted).
Output goes to `target/doc` or `--out <dir>`.

### `doctor`

Diagnoses the environment largo runs in: the Rust toolchain (needed by `build`/`run`), the wasm32
target, node (for `--emit wasm`), the verification flavor, registry reachability and credentials,
update freshness, and — inside a project — manifest health. Degradations are warnings; only a
broken project fails. Works offline.

### `completions`

Writes a completion script for bash, zsh, fish, powershell, or elvish to stdout — source it from
your shell's configuration for tab completion on every largo command and flag.

```bash
largo completions zsh > ~/.zfunc/_largo
```

### `explain`

Looks a topic up offline, in two namespaces: diagnostic codes first (every `code` from
`check --json`, `run` failures, and the MCP tools — the full list lives in
[ERROR_CATALOG.md](ERROR_CATALOG.md)), then language constructs from the teach lessons.
No project or network needed; `--json` emits a `logos-explain/1` document.

```bash
largo explain zero-index
largo explain use-after-move
largo explain Let
largo explain type-mismatch --json
```

### `mcp`

Serves the whole toolchain over the Model Context Protocol — JSON-RPC 2.0 on stdio, one JSON
object per line. Built for AI agents: register once and the agent gets six tools plus the
learning corpus as resources.

```bash
claude mcp add logos -- largo mcp
```

| Tool | What it does |
|------|--------------|
| `logos_check` | Parse + type-check → `{ok, diagnostics}` with stable codes, spans, Socratic explanations |
| `logos_run` | Execute in a sandboxed subprocess: deterministic with `seed`, always bounded by `timeout_ms` |
| `logos_logic` | English → FOL (default / pragmatic / kripke / all_scopes / discourse) |
| `logos_prove` | Prove every `## Theory` / `## Theorem` in the source, kernel-certified |
| `logos_emit` | Generated code: rust, c, isa, or wasm (base64) |
| `logos_opts` | Which optimizations fired, per tier |

Resources: `logos://quickguide` and `logos://docs/*` (this documentation, embedded in the
binary — an installed `largo` teaches the language offline). One prompt, `write-logos`,
orients an agent before its first program. Every tool accepts inline `source` or a `file`
path, and a check that *finds* errors is a successful call — read `ok`, not `isError`.

## The `Largo.toml` manifest

Defined by the `Manifest`/`Package` structs in
[`project/manifest.rs`](../apps/logicaffeine_cli/src/project/manifest.rs):

```toml
[package]
name = "my_project"
version = "0.1.0"
description = "..."          # optional
authors = ["You <you@example.com>"]   # optional
entry = "src/main.lg"        # entry point

[dependencies]
std  = "logos:std"                    # simple form: a version/URI string
math = { path = "./math" }            # detailed form: { version, path, git }
```

## Environment variables

Read by the CLI (grep of `apps/logicaffeine_cli/src/`):

| Variable | Effect |
|----------|--------|
| `LOGOS_SEED` | Scheduler seed for deterministic concurrent runs (`largo run --seed` sets it for you) |
| `LOGOS_NO_JIT` | Skip the JIT; run on the bytecode VM only |
| `LOGOS_LICENSE` | License key for `verify` / `build --verify` |
| `LOGOS_TOKEN` | Registry auth token (alternative to `largo login`) |
| `LOGOS_CREDENTIALS_PATH` | Override the credentials file location |
| `LOGOS_MAX_AST_DEPTH` | Raise/lower the AST nesting-depth limit (default 128). The default is sized for the smallest standard stacks (worker threads, browser wasm); machines with deep stacks can raise it for heavily generated code, constrained embedders can lower it |

The default registry is `https://registry.logicaffeine.com`.

---
[Docs index](README.md) · [Root README](../README.md) · [Changelog](../CHANGELOG.md)


================================================================
SOURCE: docs/imperative-mode.md — Imperative mode
================================================================

# Imperative mode — the LOGOS language

Imperative LOGOS is a statically-typed programming language written in English. The same source
runs through an interpreter, a bytecode VM, and a JIT, or compiles ahead-of-time to Rust or
directly to WebAssembly (see [Execution & performance](execution-and-performance.md)).

```rust
let rust = logicaffeine_compile::compile_to_rust(source)?;   // English → Rust
```

Source of truth: the parser and AST in
[`crates/logicaffeine_language/src/ast/stmt.rs`](../crates/logicaffeine_language/src/ast/stmt.rs),
the code generators in
[`crates/logicaffeine_compile/src/codegen/`](../crates/logicaffeine_compile/src/codegen/), and the
`e2e_*` tests in [`crates/logicaffeine_tests/tests/`](../crates/logicaffeine_tests/tests/). Every
snippet below is taken from a passing test.

## Program structure

A program is made of `##` blocks. `## Main` is the entry point; `## To <name> …` defines a function;
`## A <Name> has:` / `## A <Name> is one of:` define types.

```logos
## Main
Let x be 5.
Set x to 10.
Show x.
```
→ prints `10`.

## Variables & mutation

`Let <name> be <expr>` binds a variable; `Set <name> to <expr>` mutates it. Type annotations are
optional (`Let x: Int be 5`); types are otherwise inferred.

## Primitive types & operators

`Int` (i64), `Nat` (u64), `Real` (f64; `Float` is an alias), `Rational` (exact fractions), `Bool`,
`Text`, `Char`, `Byte` (u8), the machine words `Word8`/`Word16`/`Word32`/`Word64` (wrapping
ℤ/2ⁿ ring arithmetic — the crypto substrate), and `Uuid` (RFC 9562, every version from nil/max
through v1–v8). Operators: arithmetic `+ - * / %` (also the words `plus`, `minus`,
`times`, `divided by`); comparisons `== != < > <= >=` (also `is less than`, `is at most`, …); logical
`and` / `or` / `not`; bitwise shifts and xor. (`e2e_primitives`, `e2e_expressions`,
`e2e_comparisons`, `e2e_operators`, `phase_bitwise`, `e2e_codegen_uuid`, `e2e_md5_logos`.)

## Functions

```logos
## To classify (n: Int) -> Text:
    If n is less than 0:
        Return "negative".
    Return "non-negative".
```
compiles to:
```rust
#[inline]
fn classify(n: i64) -> String {
    if (n < 0) {
        return String::from("negative");
    }
    return String::from("non-negative");
}
```

Parameters are typed; return types are explicit (`-> T`) or inferred. Multiple parameters use
`and`: `## To add (a: Int) and (b: Int) -> Int:`. Recursion, closures, generics, and FFI
(`native "…"`, `is exported for native`/`wasm`) are all supported. (`e2e_functions`,
`phase32_functions`, `e2e_closures`, `phase34_generics`, `e2e_recursive_factorial`.)

## Collections — 1-indexed

English speakers count from one, and so does LOGOS. Slices are inclusive on both ends.

```logos
## Main
Let items be [1, 2].
Push 3 to items.
Let first be item 1 of items.        # → 1
Let middle be items 2 through 4.     # inclusive slice
Set item 2 of items to 99.
Show item 3 of items.
```

`Seq` (sequences), `Set`, `Map`, and `Tuple` are all available, with `length of`, `Push`/`Pop`,
`Add`/`Remove`, and map/tuple indexing. (`e2e_collections`, `e2e_sets`, `e2e_maps`, `e2e_tuples`.)

## Control flow

```logos
## Main
Let sum be 0.
Repeat for x in [1, 2, 3]:
    Set sum to sum + x.
Show sum.                            # → 6
```

`If … Otherwise …`, `While …` (with an optional `(decreasing <expr>)` termination measure),
`Repeat for <x> in <collection>`, `Repeat for i from 1 to n` (inclusive), `Break`, and `Return`.
(`e2e_control_flow`, `e2e_iteration`, `phase30_iteration`.)

## Structs

```logos
## A Point has:
    An x: Int.
    A y: Int.

## Main
Let p be a new Point.
Show p's x.
```

Field access and mutation use the possessive: `p's x`, `Set p's x to 100`. (`e2e_structs`,
`phase31_structs`.)

## Enums & pattern matching

```logos
## A Color is one of:
    A Red.
    A Green.
    A Blue.

## Main
Let c be a new Red.
Inspect c:
    When Red: Show "red".
    When Green: Show "green".
    When Blue: Show "blue".
```

`Inspect … When …` matches enum variants with exhaustiveness checking. (`e2e_enums`,
`phase33_enums`.)

## Ownership & borrowing

LOGOS tracks ownership. `copy of <x>` makes an explicit copy (used throughout the
[merge-sort example](../README.md#a-complete-example-merge-sort)); move/borrow verbs and
use-after-move detection are handled by the ownership analysis. (`phase21_ownership`,
[`analysis/ownership.rs`](../crates/logicaffeine_compile/src/analysis/ownership.rs).)

## I/O & assertions

`Show <expr>` prints; `Read … from console`/`from file "…"` reads; `Write "…" to file "…"` writes.
`Require that <cond>` / `Assert that <logic>` connect to the logic side — `Assert that …` is the
**Assert Bridge** into [Proof & verification](proof-and-verification.md). (`phase10_io`,
`phase25_assertions`.)

## Standard library

A small standard library ships with the compiler
([`assets/std/`](../crates/logicaffeine_compile/assets/std/)) — modules for core types plus `io`,
`file`, `time`, `random`, `env`, `crdt`, `concurrency`, `net`, `crypto`, and `uuid`, exposing
functions like `now`, `sleep`, `randomInt`, and `randomFloat`.

The `crypto` and `uuid` modules are themselves written in LOGOS:
[`crypto.lg`](../crates/logicaffeine_compile/assets/std/crypto.lg) carries the post-quantum
ML-KEM-768 building blocks (NTT with SIMD lanes, Montgomery/Barrett reduction) and ChaCha20, and
[`uuid.lg`](../crates/logicaffeine_compile/assets/std/uuid.lg) implements RFC 9562 UUIDs with the
MD5 and SHA-1 digests as LOGOS source — proven bit-exact against FIPS and reference-crate oracles
across the execution tiers (`mlkem768_logos`, `mlkem768_oracle`, `e2e_codegen_uuid`,
`e2e_uuid_logos_gen`).

Imports are **demand-driven and invisible**:
[`apply_prelude`](../crates/logicaffeine_compile/src/loader.rs) prepends a module only when your
program references one of its names *and* doesn't define them itself ("declarer wins", so your own
`Message`/`args` is never shadowed). Programs that touch no stdlib vocabulary compile byte-for-byte
unchanged, and the same seam serves both the interpreter and the AOT compiler. Opt out entirely with
a `## NoPrelude` marker.

## Concurrency

Structured concurrency, channels, agents, and CRDTs are part of the language too — see
[Concurrency & distributed](concurrency.md).

## See also

- How it runs and how fast → [Execution & performance](execution-and-performance.md)
- The compiler crate → [`logicaffeine_compile`](../crates/logicaffeine_compile/README.md)

---
[Docs index](README.md) · [Root README](../README.md) · [Changelog](../CHANGELOG.md)


================================================================
SOURCE: docs/logic-mode.md — Logic mode
================================================================

# Logic mode — English → First-Order Logic

Logic mode parses an English sentence and emits formal logic. It is deterministic: where a sentence
is genuinely ambiguous, LOGOS can return *every* reading rather than guessing one. It also parses
*strictly* — a sentence whose words can't all be consumed fails with a `TrailingTokens` error rather
than yielding a silent partial reading, so dropped meaning is a bug, not a style nit.

```rust
let fol = logicaffeine_language::compile("Every man is mortal.")?;
// → "∀x((Man(x) → Mortal(x)))"
```

Source of truth: [`crates/logicaffeine_language/`](../crates/logicaffeine_language/) — the lexer
([`lexer.rs`](../crates/logicaffeine_language/src/lexer.rs)), the parser modules
([`parser/`](../crates/logicaffeine_language/src/parser/)), the AST
([`ast/logic.rs`](../crates/logicaffeine_language/src/ast/logic.rs)), and the transpiler
([`transpile.rs`](../crates/logicaffeine_language/src/transpile.rs)). Every example below is produced
by the actual compiler.

## The API

| Function | Signature | Notes |
|----------|-----------|-------|
| `compile` | `(&str) -> Result<String, ParseError>` | one reading |
| `compile_forest` | `(&str) -> Vec<String>` | every reading (infallible), up to `MAX_FOREST_READINGS` |
| `compile_all_scopes` | `(&str) -> Result<Vec<String>, ParseError>` | the distinct quantifier-scope readings |
| `compile_with_options` | `(&str, CompileOptions) -> Result<String, ParseError>` | choose the output format / pragmatics |

Output formats (`OutputFormat`): **Unicode** (default), **LaTeX**, **SimpleFOL**, and **Kripke**
(modals lowered to explicit world quantification).

## The shape of the output

LOGOS does not stop at surface predicates. Two features show up throughout:

- **Neo-Davidsonian event semantics** — verbs introduce an event variable `e` with explicit
  thematic roles (`Agent`, `Theme`, `Past`, …):

  ```
  "John loved Mary."
  → ∃e(Love(e) ∧ Agent(e, John) ∧ Theme(e, Mary) ∧ Past(e))
  ```

- **Ontology expansion** — nouns carry their semantic class, so a *dog* is also an *animal* and a
  *mammal*:

  ```
  "Every dog barks."
  → ∀x((((Dog(x) ∧ Animal(x)) ∧ Mammal(x)) → ∃e(Bark(e) ∧ Agent(e, x))))
  ```

## Quantifiers

```
"Some cat sleeps."
→ ∃x((((Cat(x) ∧ Animal(x)) ∧ Mammal(x)) ∧ ∃e(Sleep(e) ∧ Agent(e, x))))

"No bird flies."
→ ∀x(((Bird(x) ∧ Animal(x)) → ¬∃e(Fly(e) ∧ Agent(e, x))))
```

Universal (`every`, `all`, `each`), existential (`some`, `a`, `an`), negative (`no`, `none`),
cardinals, and generic readings are all handled (`QuantifierKind` in `ast/logic.rs`; see the
`phase20_axioms`, `phase112_partitive_quantifiers`, `phase117_cumulative` tests).

## Connectives & negation

`and` (∧), `or` (∨), `if…then` (→), `iff` (↔), and `not` (¬). `and` binds tighter than `or`.

```
"John does not run."
→ ¬HAB(∃e(Run(e) ∧ Agent(e, John)))
```

(`HAB` is the habitual-aspect operator — see below.) Tests: `phase2_polarity`, `phase15_negation`.

## Modality

Modal verbs lower to Kripke-style modal operators with a force value (`□` necessity, `◇`
possibility), over alethic / deontic / temporal domains.

```
"Every student must study."
→ ∀x((Student(x) → □_{1.0} ∃e(Study(e) ∧ Agent(e, x))))
```

Use `OutputFormat::Kripke` to lower modals to explicit world quantification. Tests:
`phase139_modal_frames`, `phase123_evidentials`, `phase125_optatives`.

## Tense & aspect

Past/future tense and progressive / perfect / habitual / iterative aspect are tracked (Prior-style
operators plus LTL operators for hardware temporal logic). `"John loved Mary."` carries `Past(e)`;
present-tense generics carry `HAB`. Tests: `phase3_time`, `phase3_aspect`, `phase16_aspect`,
`phase_hw_temporal`.

## Comparatives

```
"John is taller than Mary."
→ Taller(John, Mary)
```

Degree semantics with comparatives and superlatives: `phase8_degrees`, `phase17_degrees`,
`phase119_equatives`, `phase126_degree_standard`.

## Relative clauses

```
"The man who owns a dog is happy."
→ ∃x(((Man(x) ∧ (((Dog(y) ∧ Animal(y)) ∧ Mammal(y)) ∧ ∃e(Own(e) ∧ Agent(e, x) ∧ Theme(e, y)))) ∧ Happy(x)))
```

Tests: `phase5_wh_movement`, `phase135_appositive_rc`.

## Reciprocals & plurals

A reciprocal is symmetric, so it is genuinely ambiguous — `compile` returns *both* numbered readings
rather than guessing:

```
"John and Mary love each other."
→ 1) Love(John, Mary)  2) Love(Mary, John)
```

Reciprocals (`phase4_reciprocals`), collective vs distributive plurals (`phase18_plurality`,
`phase19_group_plurals`, `phase44_distributive`).

## Scope ambiguity

When a sentence has more than one reading, `compile_forest` / `compile_all_scopes` return them all
instead of committing to one — this is the determinism guarantee in practice.

```rust
let readings = logicaffeine_language::compile_forest("Every man loves a woman.");
// → surface scope (∀ > ∃) and inverse scope (∃ > ∀); compile_forest is infallible
```

Tests: `phase12_ambiguity`, `phase116_island_scope`.

## The long tail

LOGOS covers a wide range of linguistic phenomena, each pinned by a phase test in
[`crates/logicaffeine_tests/tests/`](../crates/logicaffeine_tests/tests/):

| Phenomenon | Test file |
|------------|-----------|
| Garden-path sentences | `phase1_garden_path` |
| Wh-questions | `phase5_wh_movement`, `question.rs` |
| Ellipsis / sluicing / gapping | `phase10_ellipsis`, `phase10b_sluicing`, `phase132_gapping` |
| Event semantics & thematic roles | `phase65_event_semantics`, `phase41_event_adjectives` |
| Higher-order / λ-calculus (Montague) | `phase66_higher_order` |
| Presupposition projection | `phase113_presupposition_projection`, `phase142_vandersandt` |
| Counterfactual conditionals | `phase110_counterfactuals` |
| Binding & coreference | `phase114_binding_theory`, `phase143_binding` |
| Scalar implicature & focus | `phase130_implicature`, `pragmatics.rs` |
| Causality / concession | `phase122_causal_concessive` |
| Mass vs count | `phase115_mass_count` |
| Metaphor / metonymy / deixis / vagueness | `phase11_metaphor`, `phase129_metonymy`, `phase128_deixis`, `phase127_vagueness` |
| Discourse / anaphora (multi-sentence) | `phase42_drs`, `phase45_session` (the `Session` API) |

The test suite is the living specification — when in doubt about what a construction yields, the
phase test shows the exact output.

## See also

- The implementation crate → [`logicaffeine_language`](../crates/logicaffeine_language/README.md)
- The proof side (what you can *do* with the logic) → [Proof & verification](proof-and-verification.md)

---
[Docs index](README.md) · [Root README](../README.md) · [Changelog](../CHANGELOG.md)


================================================================
SOURCE: docs/concurrency.md — Concurrency
================================================================

# Concurrency & distributed systems

LOGOS treats concurrency, message passing, replicated state, and networking as first-class language
features. They are backed by a deterministic, replayable runtime and run across native and browser
targets.

Source of truth: the statement set in
[`ast/stmt.rs`](../crates/logicaffeine_language/src/ast/stmt.rs), the runtime
([`logicaffeine_runtime`](../crates/logicaffeine_runtime/README.md)), the CRDTs
([`logicaffeine_data/src/crdt/`](../crates/logicaffeine_data/src/crdt/)), and networking
([`logicaffeine_system/src/`](../crates/logicaffeine_system/src/)). Tests live in
`phase46_agents` … `phase54_concurrency` and the `e2e_concurrency` suite.

## The runtime

[`logicaffeine_runtime`](../crates/logicaffeine_runtime/README.md) is a **deterministic** scheduler
— pure `std`, tokio-free, and WASM-safe (the **Lamport invariant** keeps the data layer IO-free).
Scheduling decisions come from a `Chooser` driven by a seed (`SchedSeed`) or a recorded trace
(`SchedTrace`), so a concurrent run is **reproducible and replayable** (`run_with_seed`,
`run_with_trace`). There are two drivers behind one model:

- **Cooperative M:1** (the WASM path) — single-threaded, deterministic.
- **Work-stealing M:N** (native, `cfg(not(wasm32))`) — genuine multicore.

The runtime is used by the interpreter/VM tiers; AOT-compiled binaries lower to host primitives
(tokio / rayon / libp2p via [`logicaffeine_system`](../crates/logicaffeine_system/README.md))
instead, and are never linked against the runtime.

## Structured concurrency

```logos
## Main
Attempt all of the following:      # async / I/O-bound — joined
    Show "fetch A".
    Show "fetch B".
Simultaneously:                    # CPU-bound — run in parallel
    Show "crunch X".
    Show "crunch Y".
```

(`Concurrent` and `Parallel` in `ast/stmt.rs`; `phase9_structured_concurrency`.)

## Tasks, channels & select

Green threads and Go-style channels (`Pipe`). A producer task feeds a consumer:

```logos
## To produce (ch: Int):
    Send 1 into ch.
    Send 2 into ch.

## Main
    Let jobs be a Pipe of Int.
    Launch a task to produce with jobs.
    Receive first from jobs.
    Receive second from jobs.
    Show first.
    Show second.
```

`Select` waits on whichever arm is ready first — a receive or a timeout:

```logos
Await the first of:
    Receive x from jobs:
        Show x.
    After 1 seconds:
        Show "timeout".
```

The full set: `LaunchTask` (`Launch a task to <fn> with <args>`), `LaunchTaskWithHandle`
(`Let h be Launch a task to <fn>`) and `StopTask` (`Stop h.`), `CreatePipe` (`Let ch be a Pipe of T`),
`SendPipe`/`ReceivePipe` and their `Try…` variants (`Try to send <v> into ch`), and `Select`. All are
wired through the interpreter, the VM (channel/spawn/select opcodes), the JIT, and AOT codegen.
(`interp_concurrency`, `vm_concurrency`, `phase54_concurrency`.)

## Agents (message passing)

```logos
Spawn a Worker called "w1".
Send Ping to "w1".
Await response from "w1" into reply.
```

Messages can be `compressed` (Lz4/Deflate/Zstd), `cached` (schema dictionary), or `unchecked`
(latency trade-off). (`Spawn`, `SendMessage`, `AwaitMessage`; `phase46_agents`.)

A `Send` can also choose a **wire layout** — a size↔speed↔resilience dial the sender picks for its
link, orthogonal to the modifiers above:

| Word | Layout | For |
|------|--------|-----|
| `fast` / `quickly` | fixed-width (memcpy) | latency-bound / fat links (LAN, datacenter, RDMA) |
| `compact` / `small` | varint (the default) | mobile / WAN / metered |
| `packed` | SIMD group-varint | the balanced middle |
| `smallest` / `best` | per-column compression menu | bandwidth-bound, CPU cheap |
| `redundant` / `tough` | Reed-Solomon FEC shards | lossy / one-way links (UDP, multicast, BLE, LoRa) — reconstruct from any *K* |

```logos
Send redundant Ping to "w1".   # survives shard loss with no retransmit
```

The `redundant` layout splits the message into Reed-Solomon shards
([`concurrency/fec.rs`](../crates/logicaffeine_compile/src/concurrency/fec.rs)). The layout menu
(`ast::SendLayout`) runs on the interpreter/VM concurrency path today; AOT codegen lowering is in
progress.

## CRDTs

[`logicaffeine_data/src/crdt/`](../crates/logicaffeine_data/src/crdt/) defines **eight** conflict-free
replicated types, all sharing a `Merge` trait and causal metadata (dots, vector clocks), with delta
support where applicable:

| CRDT | File | What it is |
|------|------|-----------|
| `GCounter` | `gcounter.rs` | Grow-only counter |
| `PNCounter` | `pncounter.rs` | Increment/decrement counter |
| `LWWRegister` | `lww.rs` | Last-write-wins register |
| `MVRegister` | `mvregister.rs` | Multi-value register (concurrent writes = conflict set) |
| `ORSet` | `orset.rs` | Observed-remove set (add-wins / remove-wins bias) |
| `ORMap` | `ormap.rs` | Observed-remove map |
| `RGA` | `sequence/rga.rs` | Replicated growable array (sequence) |
| `YATA` | `sequence/yata.rs` | Collaborative-text sequence |

### Declaring a shared type

A replicated type is declared `Shared`; each field names the CRDT it converges as. The compiler
emits a `Merge` impl for the whole struct (`phase49_crdt`, `e2e_crdt`):

```logos
## Definition
A Counter is Shared and has:
    a points, which is ConvergentCount.
    a name, which is LastWriteWins of Text.

## Main
    Let c be a new Counter.
```

The field-type keywords map onto the structs above:

| Declared as | CRDT |
|-------------|------|
| `ConvergentCount` | `GCounter` |
| `a Tally` | `PNCounter` |
| `LastWriteWins of T` | `LWWRegister<T>` |
| `a Divergent T` | `MVRegister<T>` |
| `a SharedSet of T` | `ORSet<T>` |
| `a SharedSequence of T` | `RGA` |

### Mutating and merging

Once declared, CRDT operations read naturally:

```logos
Increase local's points by 10.       # GCounter
Decrease game's score by 5.          # PNCounter
Append "Hello" to doc's lines.       # RGA sequence
Resolve page's title to "Final".     # MVRegister
Merge remote into local.
```

(`IncreaseCrdt`, `DecreaseCrdt`, `AppendToSequence`, `ResolveConflict`, `MergeCrdt`;
`phase49_crdt`, `e2e_crdt`.)

## Networking & persistence

[`logicaffeine_system`](../crates/logicaffeine_system/README.md) provides the transports, gated by
Cargo features (`relay`, `networking`, `persistence`, `concurrency`):

- **libp2p mesh** ([`network/`](../crates/logicaffeine_system/src/network/)) — TCP + QUIC, mDNS
  discovery, request/response, and **GossipSub** pub/sub for CRDT sync.
- **Thin WebSocket relay** ([`relay.rs`](../crates/logicaffeine_system/src/relay.rs) native +
  [`relay_browser.rs`](../crates/logicaffeine_system/src/relay_browser.rs) WASM, over the shared
  [`relay_proto`](../crates/logicaffeine_system/src/relay_proto.rs)) — bridges the browser to the mesh
  without libp2p.

The distributed verbs tie state to the network and disk:

```logos
Listen on "/ip4/127.0.0.1/tcp/8000".
Connect to "/ip4/127.0.0.1/tcp/8000".
Sync counter on "scores".            # subscribe to a GossipSub topic; auto-publish + auto-merge
Mount counter at "data/counter.journal".   # journal to disk (WAL + snapshots)
```

(`Listen`, `ConnectTo`, `Sync`, `Mount`; `phase48_network`, `phase51_mesh`, `phase52_sync`,
`phase53_persistence`.)

## Determinism in practice

Because scheduling is seed/trace driven, a concurrent program can be run identically on the
interpreter, the VM, and (for single-task replay) AOT — the differential tests assert the tiers agree
byte-for-byte. This is what makes "concurrent" and "reproducible" coexist.

## See also

- The execution tiers → [Execution & performance](execution-and-performance.md)
- The runtime, data, and system crates' own READMEs

---
[Docs index](README.md) · [Root README](../README.md) · [Changelog](../CHANGELOG.md)


================================================================
SOURCE: docs/proof-and-verification.md — Proof & verification
================================================================

# Proof & verification

LOGOS can do more than translate logic — it can *check* it. There are three layers, increasing in
power and in trust assumptions:

1. **The kernel** — a small, pure type-theory core that *checks* proofs.
2. **The proof engine** — searches for proofs and gives Socratic hints; everything it finds is
   checked by the kernel.
3. **Z3 verification** — an optional SMT/model-checking layer for static verification and hardware
   assertions.

## The kernel

[`logicaffeine_kernel`](../crates/logicaffeine_kernel/README.md) is a Calculus of Constructions type
checker — the trusted base. It is pure: by the **Milner invariant** it has no path to the lexicon
(see [Architecture](architecture.md)). Core surface
([`kernel/src/lib.rs`](../crates/logicaffeine_kernel/src/lib.rs)):

- `Term`, `Universe`, `Literal`, `Context` — the term language and typing context.
- `infer_type`, `is_subtype` — type checking and cumulativity.
- `normalize` — β/δ-reduction to normal form.

It ships decision procedures as modules, each a checkable engine:
[`ring`](../crates/logicaffeine_kernel/src/ring.rs) (polynomial/ring equalities),
[`lia`](../crates/logicaffeine_kernel/src/lia.rs) (linear integer arithmetic),
[`omega`](../crates/logicaffeine_kernel/src/omega.rs) (Presburger/integer arithmetic),
[`cc`](../crates/logicaffeine_kernel/src/cc.rs) (congruence closure),
[`bitvector`](../crates/logicaffeine_kernel/src/bitvector.rs),
[`simp`](../crates/logicaffeine_kernel/src/simp.rs) (simplification), and
[`termination`](../crates/logicaffeine_kernel/src/termination.rs). Proof **certificates** can be
serialized and re-checked independently. Tests: `phase69_kernel_coc`, `phase73_certifier`,
`phase86_kernel_primitives`, and the incompleteness arc (`phase93_diagonal_lemma` …
`phase95_incompleteness`).

## The proof engine

[`logicaffeine_proof`](../crates/logicaffeine_proof/README.md) is a backward-chaining prover over an
arena-independent IR (`ProofExpr` / `ProofTerm`). By the **Liskov invariant** it has no dependency on
the language crate, so it is reusable across front-ends. It produces a proof tree (each `leaf` tagged
with the `InferenceRule` used) and **Socratic hints** (`SocraticHint`, `SuggestedTactic`) that guide
a learner toward the next step rather than just reporting failure. Tests: `phase60_proof_engine`,
`phase61_induction`, `phase96_tactics`, `phase97_deep_induction`.

Beyond backward chaining, the crate ships its own **Z3-free SAT/BMC core**
([`cdcl.rs`](../crates/logicaffeine_proof/src/cdcl.rs)): the `sat` module does CDCL model finding,
equivalence (`prove_equivalence`), and unsat proofs; the `bmc` module does bounded model checking,
k-induction (`prove_invariant`), counterexample search, and vacuity (`check_vacuity`). Because it
needs no external solver, it runs in the browser — it is the engine behind Studio's
[Hardware mode](studio-and-learn.md) in-browser proving (Z3 stays a native-only backend).

A theorem is written in English as a named block of `Given:` premises and a `Prove:` goal:

```logos
## Theorem: Socrates_Mortality_Verified
Given: Socrates is a man.
Given: Every man is mortal.
Prove: Socrates is mortal.
```

Each line is parsed as a sentence (see [Logic mode](logic-mode.md)); the engine then proves the goal
from the premises. The English → `ProofExpr` lowering lives in the language crate
([`proof_convert.rs`](../crates/logicaffeine_language/src/proof_convert.rs)), preserving the Liskov boundary. See
`phase78_e2e_verification` and `phase84_extraction` (extracting proven properties to Rust
assertions).

## Z3 verification (optional, Pro+)

[`logicaffeine_verify`](../crates/logicaffeine_verify/README.md) is an SMT-backed verification and
model-checking engine. By the **Tarski invariant** its IR (`VerifyExpr` / `VerifyType`,
[`verify/src/ir.rs`](../crates/logicaffeine_verify/src/ir.rs)) is decoupled from the main AST, so it
is front-end-agnostic. The crate is **excluded from `default-members`**: a plain build needs no Z3.
It is reached via the `verification` feature and is **license-gated** (Pro+, validated against the
licensing service — [`license.rs`](../crates/logicaffeine_verify/src/license.rs)).

It is far more than an assertion checker. Public modules
([`verify/src/lib.rs`](../crates/logicaffeine_verify/src/lib.rs)) include:

- `equivalence` (`check_equivalence`), `consistency` — tautology/contradiction/equivalence checking.
- `ic3` (IC3/PDR), `kinduction` (k-induction), `interpolation` (Craig interpolation), `liveness`,
  `multiclock`, `parameterized` — a full hardware model-checking stack.
- `solver` (`Verifier`, `VerificationSession`), `smtlib`, `incremental`, `abstraction`, `automata`,
  `strategy`, `synthesis`, `security`.

This backs the **English → SVA/PSL** path (the SVA code generator,
[`compile/src/codegen_sva/`](../crates/logicaffeine_compile/src/codegen_sva/)) for formal hardware
verification. Verification errors are written as Socratic explanations with counter-examples. Run it
with `largo verify` / `largo build --verify` (see [the CLI guide](cli.md)).

Tests: `phase42` (Z3), `phase99_solver`, `phase104_induction_vs_z3`, `phase102_unified_verification`,
and the many `phase_hw_*` hardware-verification suites.

## Translation validation

[`logicaffeine_tv`](../crates/logicaffeine_tv/README.md) closes the loop on the compiler itself: it
uses SMT to prove the emitted Rust is observationally equivalent to the LOGOS source
(`check_encoder_sound`, `summarize_logos`). It depends on both `compile` and `verify` and, like them,
is opt-in.

## Synthesis (EXODIA)

[`logicaffeine_synth`](../crates/logicaffeine_synth/README.md) is offline tooling that uses Z3 to
verify JIT stencil specifications against witness inputs (`all_specs`, `check_spec_with_witnesses`) —
it never runs inside the language at runtime; it validates the JIT back-end ahead of time.

## The trust story

The kernel is the small trusted base; the proof engine, Z3, and translation validation all *produce*
artifacts the kernel (or an independent re-check) can verify. The point: search can be heuristic, but
acceptance is checked.

## See also

- [Logic mode](logic-mode.md) — where the propositions come from
- [Architecture](architecture.md) — the Milner / Liskov / Tarski invariants

---
[Docs index](README.md) · [Root README](../README.md) · [Changelog](../CHANGELOG.md)


================================================================
SOURCE: docs/execution-and-performance.md — Execution & performance
================================================================

# Execution & performance

One front-end, several back-ends. A LOGOS program can be interpreted for instant feedback, run on a
bytecode VM that tiers up to native machine code, compiled ahead-of-time to Rust, or emitted
directly as a self-contained WebAssembly module. All of it is benchmarked.

Source of truth: [`crates/logicaffeine_compile/src/`](../crates/logicaffeine_compile/src/) (the
tiers), [`crates/logicaffeine_forge/`](../crates/logicaffeine_forge/README.md) +
[`crates/logicaffeine_jit/`](../crates/logicaffeine_jit/README.md) (the JIT), and
[`benchmarks/`](../benchmarks/).

## The five execution tiers

| Tier | Where | Target | Notes |
|------|-------|--------|-------|
| **Tree-walking interpreter** | [`interpreter.rs`](../crates/logicaffeine_compile/src/interpreter.rs) | native + WASM | Direct AST evaluation; sub-second feedback (`largo run --interpret`) |
| **Bytecode VM** | [`vm/`](../crates/logicaffeine_compile/src/vm/) (`compiler.rs`, `machine.rs`) | native + WASM | Register-based; portable; JIT-eligible; the browser engine |
| **Copy-and-patch JIT (EXODIA)** | [`forge/`](../crates/logicaffeine_forge/) + [`jit/`](../crates/logicaffeine_jit/) | native only | Tiers up from hot VM functions/loops (`vm/native_tier.rs`) |
| **AOT Rust codegen** | [`codegen/`](../crates/logicaffeine_compile/src/codegen/) | native + WASM | The performance gold standard (`largo build`) |
| **Direct WASM backend** | [`vm/wasm/`](../crates/logicaffeine_compile/src/vm/wasm/) | WebAssembly | Emits a self-contained `.wasm` module with no `rustc`/`cargo`/`wasm-bindgen` in the loop — milliseconds (`largo build --emit wasm`); `--emit wasm-linked` links the real `logicaffeine_base::BigInt` runtime via `rust-lld` for exact arbitrary-precision integers |

Two special-purpose emitters sit beside the tiers:

| Emitter | Where | Notes |
|---------|-------|-------|
| **AOT C codegen** | [`codegen_c/`](../crates/logicaffeine_compile/src/codegen_c/) | Experimental benchmark/embedding subset |
| **SVA/PSL codegen** | [`codegen_sva/`](../crates/logicaffeine_compile/src/codegen_sva/) | English → SystemVerilog Assertions + runtime monitors for hardware verification (see [Proof & verification](proof-and-verification.md)) |

## How tier-up works

The VM runs bytecode; when a function or loop gets hot, the **copy-and-patch JIT** — the tier is
named **EXODIA** — (`ForgeTier`, installed via
[`logicaffeine_jit::install`](../crates/logicaffeine_jit/src/lib.rs)) compiles it to native machine
code by stitching pre-built stencils and patching in the live operands — fast compilation, native
execution — with a register-allocating x86-64 backend (`regalloc.rs`) above per-stencil dispatch. JIT regions carry **deoptimization guards**: if a region sees
data it didn't specialize for, it bails safely back to bytecode. Set `LOGOS_NO_JIT` to stay on the
VM. (`vm/native_tier.rs`, `vm/aot_tier.rs`.)

In the browser, the interpreter and VM run in WebAssembly and produce byte-identical results to
native — that is what powers the in-page [Studio](studio-and-learn.md). The direct WASM backend is
the complement: instead of running the engine *in* WASM, it compiles the program *to* a WASM module
(locked to VM/interpreter behavior by the `wasm_aot_lock` differentials); the `wasm-jit` feature
additionally lets JIT'd hot regions execute in-browser (`vm/wasm/region_jit.rs`).

## The optimizer

Optimizations are registry-driven. Each pass is registered in
[`logicaffeine_language/src/optimization.rs`](../crates/logicaffeine_language/src/optimization.rs) and
toggled through a single `OptimizationConfig`, with per-program control via `## No <X>` decorators in
the source. The passes themselves live in
[`compile/src/optimize/`](../crates/logicaffeine_compile/src/optimize/) and the code generators in
[`codegen/`](../crates/logicaffeine_compile/src/codegen/) — covering bounds-check elimination, loop
transforms, scalarization, de-`Rc`, inlining, dense-map specialization, and more.

To see exactly which optimizations *fired* for a program:

```bash
largo opts src/main.lg          # human-readable
largo opts src/main.lg --json   # keyword list
```

## Benchmarks

The [`benchmarks/`](../benchmarks/) directory holds the harness and recorded results
([`benchmarks/results/`](../benchmarks/results/)). LOGOS is measured two ways:

- **AOT** (compiled Rust/C) against C, Rust, Zig, Go, Java, JavaScript, Python, Ruby, and Nim on a
  shared set of compute kernels.
- **Interpreter + VM + JIT** against V8, to track the non-compiled path.

Results are published live on the [`/benchmarks`](https://logicaffeine.com/benchmarks) page; the JSON
under `benchmarks/results/` is the raw data. Because numbers move with every optimization, this guide
points at the live data rather than freezing a figure here. Broadly: the AOT path reaches C-level
performance on same-algorithm kernels (and wins outright where it can prove a better algorithm),
while the VM+JIT path is competitive with V8 and beats it on float-heavy work.

## Verifying the compiler itself

Two mechanisms keep the tiers honest:

- **Differential tests** (`e2e_differential`, `e2e_feature_matrix`) assert the interpreter, VM, JIT,
  and AOT paths agree on output.
- **Translation validation** ([`logicaffeine_tv`](../crates/logicaffeine_tv/README.md)) uses SMT to
  prove the emitted Rust matches the LOGOS source.

## See also

- The language being executed → [Imperative mode](imperative-mode.md)
- The crate layout and gating → [Architecture](architecture.md)

---
[Docs index](README.md) · [Root README](../README.md) · [Changelog](../CHANGELOG.md)


================================================================
SOURCE: docs/studio-and-learn.md — Studio & Learn
================================================================

# Studio & Learn

The [`logicaffeine_web`](../apps/logicaffeine_web/README.md) app is a Dioxus + WebAssembly single-page
site that runs the **entire LOGOS engine in the browser** — parser, interpreter, VM, proof engine,
and code generation all execute client-side. No server round-trip.

Source of truth: [`apps/logicaffeine_web/src/`](../apps/logicaffeine_web/src/) — the router
([`ui/router.rs`](../apps/logicaffeine_web/src/ui/router.rs)), the pages
([`ui/pages/`](../apps/logicaffeine_web/src/ui/pages/)), and the learner model (the modules listed
below).

## Studio — the playground

[`/studio`](https://logicaffeine.com/studio) is a multi-mode editor
([`ui/pages/studio.rs`](../apps/logicaffeine_web/src/ui/pages/studio.rs)):

- **Logic mode** — parse English to First-Order Logic with an AST view. The output toggles between
  the FOL interpretation, generated Rust, and synthesized SVA (`LogicView`).
- **Code mode** — write imperative LOGOS with a streaming REPL; the output toggles between
  interpreter output and the generated Rust (`CodeOutputMode`). Execution uses the engine's
  [`interpret_streaming`](../crates/logicaffeine_compile/src/ui_bridge.rs) API, which emits output
  lines incrementally and can route file I/O through an in-browser virtual file system.
- **Math mode** — define theorems and types and prove them interactively, with tactic hints from the
  [proof engine](proof-and-verification.md).
- **Hardware mode** — write an English hardware spec; the engine synthesizes SystemVerilog
  Assertions (SVA), PSL, and a Rust runtime monitor
  ([`codegen_sva/`](../crates/logicaffeine_compile/src/codegen_sva/)), then proves the properties
  in-browser and renders a **counterexample waveform** when one fails. Logic mode's "Compile to SVA"
  reuses the same synthesis. See [Proof & verification](proof-and-verification.md).

## Learn Logic — the curriculum

[`/learn`](https://logicaffeine.com/learn) is a gamified course. The content is embedded at compile
time from [`apps/logicaffeine_web/assets/`](../apps/logicaffeine_web/assets/) (via `include_dir`) and
organized into four **eras**:

```
01_first-steps  →  02_building-blocks  →  03_expanding-horizons  →  04_mastery
```

Each era holds modules; each module holds sections (prose, definitions, examples, symbol glossaries)
and exercises. Exercise types (`ExerciseType` in
[`content.rs`](../apps/logicaffeine_web/src/content.rs)):

- **Translation** — translate English to FOL (graded structurally).
- **MultipleChoice** — pick the correct reading.
- **Ambiguity** — identify the distinct readings of an ambiguous sentence.

The learner model is built from focused modules under
[`apps/logicaffeine_web/src/`](../apps/logicaffeine_web/src/):

| Module | Role |
|--------|------|
| [`srs.rs`](../apps/logicaffeine_web/src/srs.rs) | SM-2 spaced repetition (`ResponseQuality`, ease factor, intervals) |
| [`grader.rs`](../apps/logicaffeine_web/src/grader.rs) | Structural AST-similarity grading with partial credit |
| [`progress.rs`](../apps/logicaffeine_web/src/progress.rs) | Per-learner progress + review scheduling |
| [`struggle.rs`](../apps/logicaffeine_web/src/struggle.rs) | Struggle detection → adaptive hints |
| [`achievements.rs`](../apps/logicaffeine_web/src/achievements.rs) | XP, streaks, rewards |
| [`unlock.rs`](../apps/logicaffeine_web/src/unlock.rs) | Prerequisite-gated unlocks |
| [`game.rs`](../apps/logicaffeine_web/src/game.rs) | Session/game state |

Grading normalizes whitespace and Unicode and compares FOL *structurally*, so an answer that is
formally equivalent is accepted regardless of cosmetic differences.

## The rest of the site

The router defines these routes (from `ui/router.rs`):

| Route | Page |
|-------|------|
| `/` | Landing |
| `/studio` | Studio playground |
| `/learn` | Learn Logic curriculum |
| `/benchmarks` | Live performance benchmarks ([Execution & performance](execution-and-performance.md)) |
| `/registry`, `/registry/package/:name` | Package registry browser |
| `/guide` | Documentation & tutorials |
| `/crates` | Crate documentation browser |
| `/news`, `/news/:slug` | Release announcements |
| `/roadmap` | Roadmap |
| `/pricing` | Plans & licensing |
| `/profile` | User settings & progress |
| `/workspace/:subject` | Subject workspace |

Persistence (progress, license, theme) uses browser storage; file I/O in Studio uses an OPFS /
IndexedDB-backed virtual file system.

## Running it locally

```bash
dx serve -p logicaffeine-web    # from the repo root
```

## See also

- The app's own developer README → [`apps/logicaffeine_web/README.md`](../apps/logicaffeine_web/README.md)
- What the engine does → [Imperative mode](imperative-mode.md), [Logic mode](logic-mode.md)

---
[Docs index](README.md) · [Root README](../README.md) · [Changelog](../CHANGELOG.md)


================================================================
SOURCE: docs/ERROR_CATALOG.md — Error catalog
================================================================

# LOGOS Error Catalog

Every diagnostic the LOGOS toolchain emits, keyed by its stable
`logos-diagnostic/1` code — the `code` field of `largo check --json`,
`largo run --json`, and the MCP `logos_check` tool. Look a code up here
or with `largo explain <code>`.

Generated from `logicaffeine_language::diagnostic::catalog()`. Do not
edit by hand; run `./scripts/gen-error-catalog.sh` after changing
`ParseErrorKind`.

## `unexpected-token`

- **Severity**: error
- **Variant**: `UnexpectedToken`

**Example**:

```text
expected a period ('.'), found a comma (',')
```

> I was following your sentence but stumbled here: I expected a period ('.'), and found a comma (',') instead. The structure so far commits me to a period ('.') next. Is a word missing just before this, or did two thoughts run together? Splitting the sentence in two often shows which.

## `expected-content-word`

- **Severity**: error
- **Variant**: `ExpectedContentWord`

**Example**:

```text
expected a content word, found a comma (',')
```

> This spot needs a content word — a noun, a verb, or an adjective — but I found a comma (',') instead. Content words carry the meaning; the little words only arrange them. What thing, action, or quality did you mean to name here? Put that word in and the sentence grounds itself.

## `expected-copula`

- **Severity**: error
- **Variant**: `ExpectedCopula`

**Example**:

```text
expected 'is' or 'are'
```

> The subject here is waiting for 'is' or 'are' to link it to its predicate. English predication runs through a copula — without one, the two halves never connect. What is the subject supposed to BE? Write it as 'X is Y' ('are' for plurals).

## `unknown-quantifier`

- **Severity**: error
- **Variant**: `UnknownQuantifier`

**Example**:

```text
expected a quantifier, found a comma (',')
```

> I needed a quantifier here — a word like 'all', 'some', or 'no' — but found a comma (','). Quantifiers say how many things the sentence talks about, and that choice decides the whole logical shape. How many did you mean: every one, at least one, or none? Lead with the word that says so.

## `unknown-modal`

- **Severity**: error
- **Variant**: `UnknownModal`

**Example**:

```text
expected a modal, found a comma (',')
```

> I needed a modal here — 'must', 'can', 'may', 'should' — but found a comma (','). Modals set the strength of the claim: necessity, possibility, permission, obligation. Which strength did you mean? Pick the modal that carries it and the logic follows.

## `expected-verb`

- **Severity**: error
- **Variant**: `ExpectedVerb`

**Example**:

```text
expected a verb, found a comma (',')
```

> Every sentence needs a verb, and this one's verb should appear here — I found a comma (',') instead. The verb names the action or state everything else hangs on. What is the subject doing (or being)? Give the sentence that verb.

## `expected-temporal-adverb`

- **Severity**: error
- **Variant**: `ExpectedTemporalAdverb`

**Example**:

```text
expected a temporal adverb
```

> I expected a time word here — 'yesterday', 'tomorrow', 'always'. Temporal adverbs anchor the sentence on the timeline, and this construction promised one. When does this happen? Say it with a temporal adverb, or drop the construction that required one.

## `expected-presupposition-trigger`

- **Severity**: error
- **Variant**: `ExpectedPresuppositionTrigger`

**Example**:

```text
expected a presupposition trigger
```

> I expected a presupposition trigger here — a word like 'stopped', 'realized', or 'regrets'. These verbs quietly assume something was already true; that hidden assumption is what this construction works with. What background fact is being taken for granted? The trigger word is what carries it.

## `expected-focus-particle`

- **Severity**: error
- **Variant**: `ExpectedFocusParticle`

**Example**:

```text
expected a focus particle
```

> I expected a focus particle here — 'only', 'even', 'just'. Focus particles single out one part of the sentence against its alternatives. Which word should the emphasis land on? Put the particle directly before it.

## `expected-scopal-adverb`

- **Severity**: error
- **Variant**: `ExpectedScopalAdverb`

**Example**:

```text
expected a scopal adverb
```

> I expected a scopal adverb here — a word like 'necessarily' or 'possibly' that comments on the whole claim rather than the verb alone. Is the adverb meant to cover the entire sentence? If it only describes the action, it belongs next to the verb instead.

## `expected-superlative-adjective`

- **Severity**: error
- **Variant**: `ExpectedSuperlativeAdjective`

**Example**:

```text
expected a superlative adjective
```

> I expected a superlative here — 'tallest', 'fastest', the '-est' form. A superlative ranks one thing against all the others, and that is the comparison this sentence set up. Are you comparing against everything, or just one other thing? Use '-est' for everything, '-er than' for one.

## `expected-comparative-adjective`

- **Severity**: error
- **Variant**: `ExpectedComparativeAdjective`

**Example**:

```text
expected a comparative adjective
```

> I expected a comparative here — 'taller', 'faster', the '-er' form. A comparative weighs exactly two things against each other. What quality are the two compared on? Name it in its '-er' form and follow with 'than'.

## `expected-than`

- **Severity**: error
- **Variant**: `ExpectedThan`

**Example**:

```text
expected 'than' to complete the comparison
```

> A comparative opened a comparison, and 'than' introduces the other side — but it is missing here. Taller than what, exactly? Add 'than' plus the thing being compared against.

## `expected-number`

- **Severity**: error
- **Variant**: `ExpectedNumber`

**Example**:

```text
expected a number
```

> This measure phrase needs a number — '2', '3.14' — and none appeared. A measure without a quantity measures nothing. How much, exactly? Put the number in front of the unit.

## `empty-restriction`

- **Severity**: error
- **Variant**: `EmptyRestriction`

**Example**:

```text
empty relative clause
```

> This relative clause is empty — 'the X that ...' with nothing after 'that'. A restriction narrows the noun down, so an empty one narrows nothing. Which ones did you mean? State the property that picks them out, or drop the 'that' entirely.

## `gapping-resolution-failed`

- **Severity**: error
- **Variant**: `GappingResolutionFailed`

**Example**:

```text
no verb to borrow for the gapped clause
```

> This reads like a gapped construction — '... and Mary, a pear' — where the verb is borrowed from the previous clause, but I found no verb there to borrow. What is the second subject doing? Either repeat the verb outright, or make sure the first clause states it plainly.

## `stative-progressive-conflict`

- **Severity**: error
- **Variant**: `StativeProgressiveConflict`

**Example**:

```text
stative verb used in the progressive
```

> A stative verb like 'know' or 'love' is in the progressive here, and states do not run in progress — they simply hold or they don't. Is this a state or an ongoing activity? States take the simple form ('knows'); only activities take '-ing'.

## `undefined-variable`

- **Severity**: error
- **Variant**: `UndefinedVariable`
- **Quickfix**: Did you mean '<nearest definition>'?
- **Guide**: <https://github.com/Brahmastra-Labs/logicaffeine/blob/main/LOGOS_QUICKGUIDE.md#2-variables--mutation>

**Example**:

```text
'x' is not declared
```

> I found 'x', but nothing has declared it. Every variable starts life in a Let — reading a name before it exists gives me no value to read. Where should 'x' get its first value? Add 'Let x be ...' above this line, or check the spelling against the name you declared.

## `use-after-move`

- **Severity**: error
- **Variant**: `UseAfterMove`
- **Quickfix**: Use 'a copy of …' instead
- **Guide**: <https://github.com/Brahmastra-Labs/logicaffeine/blob/main/LOGOS_QUICKGUIDE.md#13-output>

**Example**:

```text
cannot use 'x' after giving it away
```

> Cannot use 'x' after giving it away. 'Give x to ...' transferred ownership — 'x' belongs to the receiver now, and this later use has nothing left to hold. Who really needs to own 'x' here? To lend it and keep it, 'Show x'; to hand over a duplicate, give 'a copy of x'.

## `is-value-equality`

- **Severity**: warning
- **Variant**: `IsValueEquality`
- **Quickfix**: Use 'equals' for value comparison
- **Guide**: <https://github.com/Brahmastra-Labs/logicaffeine/blob/main/LOGOS_QUICKGUIDE.md#3-arithmetic-comparison-logic-bitwise>

**Example**:

```text
'x is 5' compares values; use 'equals'
```

> 'x is 5' reads as a type or predicate claim — 'is' asks what something IS, not which value it holds. Value comparison is spelled 'equals'. Are you asking what 'x' is, or whether it holds 5? For the value question, write 'x equals 5'.

## `zero-index`

- **Severity**: info
- **Variant**: `ZeroIndex`
- **Quickfix**: Use 1-based indexing
- **Guide**: <https://github.com/Brahmastra-Labs/logicaffeine/blob/main/LOGOS_QUICKGUIDE.md#5-collections>

**Example**:

```text
indices start at 1; there is no item 0
```

> This asks for item 0, but LOGOS indices start at 1 — in English, 'the 1st item' is the first one; there is no item 0. Which element did you want? The first is 'item 1 of xs' — the zero-based habit is the only thing to unlearn.

## `expected-statement`

- **Severity**: error
- **Variant**: `ExpectedStatement`

**Example**:

```text
expected a statement
```

> I expected a statement here — a sentence that does something, like 'Let', 'Set', 'Show', or 'Return'. What should happen at this point in the program? Start the line with the verb that does it, and end with a period.

## `expected-keyword`

- **Severity**: error
- **Variant**: `ExpectedKeyword`

**Example**:

```text
expected the word 'to'
```

> This construction needs the word 'to' here to complete its shape. Statement forms have fixed connecting words — they are the joints of the sentence. Which form did you start? Insert 'to' where I stopped, or compare your line against that form's example.

## `expected-expression`

- **Severity**: error
- **Variant**: `ExpectedExpression`

**Example**:

```text
expected an expression
```

> I expected an expression here — a value: a number, a variable, a call, or a computation. Something just before this (a 'be', a 'to', an operator) promised a value that never arrived. What value should flow into this spot? Write it, or remove the connector that promised it.

## `expected-identifier`

- **Severity**: error
- **Variant**: `ExpectedIdentifier`

**Example**:

```text
expected a name
```

> I expected a name here — an identifier for a variable, function, or field. This position says which thing the statement acts on, so a keyword or symbol cannot stand in. What is the thing called? Use its declared name, or declare it first with Let.

## `respectively-length-mismatch`

- **Severity**: error
- **Variant**: `RespectivelyLengthMismatch`

**Example**:

```text
'respectively' lists differ: 2 subject(s) vs 3 object(s)
```

> 'Respectively' pairs the two lists one-to-one, but the subject side has 2 element(s) and the object side has 3. With uneven lists, something ends up with no partner. Which pairing did you intend? Even the lists out, or split the sentence so each pairing is explicit.

## `type-mismatch`

- **Severity**: error
- **Variant**: `TypeMismatch`, `TypeMismatchDetailed`
- **Guide**: <https://github.com/Brahmastra-Labs/logicaffeine/blob/main/LOGOS_QUICKGUIDE.md#2-variables--mutation>

**Example**:

```text
expected 'Int', found 'Text'
```

> This slot is typed 'Int', but the value here is 'Text'. LOGOS holds every value to its declared type — that agreement is what the later guarantees stand on. Which side is right, the annotation or the value? Change the one that is lying.

**Example**:

```text
expected 'Int', found 'Text' (in argument 2 of 'compute')
```

> I expected 'Int' here but found 'Text' (in argument 2 of 'compute'). The two sides of this position must agree on one type. Which side has it right? Adjust the annotation or the value so they tell the same story.

## `infinite-type`

- **Severity**: error
- **Variant**: `InfiniteType`

**Example**:

```text
infinite type: T would contain itself
```

> This would make an infinite type: T would have to equal Seq of T, which contains it — a type inside itself, forever. This usually means a value is being folded into its own container. Did you mean to push into the collection rather than rebuild it? A named struct or one level of indirection breaks the cycle.

## `arity-mismatch`

- **Severity**: error
- **Variant**: `ArityMismatch`
- **Guide**: <https://github.com/Brahmastra-Labs/logicaffeine/blob/main/LOGOS_QUICKGUIDE.md#7-functions--closures>

**Example**:

```text
'greet' takes 2 argument(s), but this call passes 1
```

> 'greet' takes 2 argument(s), but this call passes 1. A call must fill every parameter — each one is a promise the function body relies on. Which parameter went missing, or which extra snuck in? Line the call up against the function's '## To' header.

## `field-not-found`

- **Severity**: error
- **Variant**: `FieldNotFound`
- **Guide**: <https://github.com/Brahmastra-Labs/logicaffeine/blob/main/LOGOS_QUICKGUIDE.md#8-structs-enums--field-access>

**Example**:

```text
'Point' has no field named 'z'
```

> 'Point' has no field named 'z'. A struct's fields are fixed at its definition — reads cannot invent new ones. Available fields: x, y. Did you mean one of those, or should the '## A Point has:' definition grow a 'z'?

## `not-a-function`

- **Severity**: error
- **Variant**: `NotAFunction`
- **Guide**: <https://github.com/Brahmastra-Labs/logicaffeine/blob/main/LOGOS_QUICKGUIDE.md#7-functions--closures>

**Example**:

```text
cannot call a value of type 'Int'
```

> This tries to call a value of type 'Int', but only functions and closures can be called. Parentheses after a name mean 'invoke this'. Did you want a function with a similar name, or is this variable shadowing the function you meant?

## `invalid-refinement-predicate`

- **Severity**: error
- **Variant**: `InvalidRefinementPredicate`

**Example**:

```text
refinement predicate is not checkable
```

> This refinement predicate is not one I can check — refinements are comparisons over the declared name, like 'x > 0' or 'n < 100'. What must always be true of this value? State it as a simple comparison; anything richer belongs in an Assert.

## `grammar-error`

- **Severity**: warning
- **Variant**: `GrammarError`

**Example**:

```text
grammar: its vs it's
```

> Grammar: its vs it's. Small grammar slips change the logical reading, so I stop rather than guess. Which meaning did you intend? Adjust the wording — the right form usually reads aloud correctly.

## `scope-violation`

- **Severity**: error
- **Variant**: `ScopeViolation`

**Example**:

```text
scope: pronoun trapped in negation
```

> Scope problem: pronoun trapped in negation. A pronoun can only reach referents its clause can see — things introduced under a negation or inside an 'or' are walled off from later sentences. Who is the pronoun meant to point at? Name the referent outright, or introduce it outside the wall.

## `unresolved-pronoun`

- **Severity**: error
- **Variant**: `UnresolvedPronoun`

**Example**:

```text
pronoun 'she' has no antecedent
```

> This pronoun ('she') has nothing to refer to — no earlier sentence introduced a matching referent this clause can reach. Pronouns only look backward through accessible discourse. Who is 'she' here? Introduce that referent in an earlier sentence, or use the name directly.

## `trailing-tokens`

- **Severity**: error
- **Variant**: `TrailingTokens`

**Example**:

```text
input left over, beginning with a comma (',')
```

> I understood the sentence up to here, but the rest — beginning with a comma (',') — does not fit the structure I built. Accepting it would silently drop that meaning, and LOGOS never drops meaning. Is a connective missing, or are two sentences sharing one period? End the first thought with '.' and start fresh.

## `ast-too-deep`

- **Severity**: error
- **Variant**: `AstTooDeep`

**Example**:

```text
AST nests 3000 levels deep; the limit is 2048
```

> This program nests expressions or blocks 3000 levels deep, past the current 2048-level limit — a tower this tall usually comes from generated code, and every downstream walker would overflow on it. Could each layer land in its own 'Let'? Intermediate bindings reset the depth to one; or raise the gate with LOGOS_MAX_AST_DEPTH=4096 if your stacks are deep.

## `custom`

- **Severity**: error
- **Variant**: `Custom`

**Example**:

```text
zone escape
```

> zone escape