# Logicaffeine API documentation

> The Rust API of LOGOS, the English programming language: English sentences in, first-order logic out; a small Calculus-of-Constructions kernel that checks every proof; certified SAT, algebraic and arithmetic proof engines; exact mathematics; and the compiler and runtime that run English programs. Generated by rustdoc from the source on every build.

LOGOS reads English. Logic mode turns sentences into first-order logic; Math mode proves theorems the kernel checks; Imperative mode runs English programs through an interpreter, a bytecode VM with a JIT, and Rust, C and WASM backends. The language itself — syntax, guides, examples, error codes — is described at https://logicaffeine.com/llms.txt and, in one file, https://logicaffeine.com/llms-full.txt. This site is the API underneath it.

## How to navigate this site

- Every crate has a complete map, `/llms/<crate>.txt`: each public module and item with its kind, its one-line summary and its address. Fetch the one you need and search it — the crates are listed below.
- Addresses are extensionless: a module at `/<crate>/<module path>/`, an item at `/<crate>/<module path>/<kind>.<Name>` (`struct.`, `enum.`, `trait.`, `fn.`, `type.`, `constant.`, `macro.`), every item of a crate on one page at `/<crate>/all`, source at `/src/<crate>/<file>`.
- Item pages carry the full signature, documentation, trait implementations and a source link.
- An address that does not exist answers 404 with a page of routes into every crate — never a copy of another page.
- Every page: [sitemap.xml](https://docs.logicaffeine.com/sitemap.xml).

## Start here

Where each kind of work begins — logic, proof, mathematics, verification and programs.

### Logic: English in, first-order logic out
- [Turn an English sentence into first-order logic](https://docs.logicaffeine.com/logicaffeine_language/compile/fn.compile): The one-call entry point, default options; the `compile_*` functions beside it add output formats, discourse, ambiguity and scope.
- [Get every quantifier-scope reading of a sentence](https://docs.logicaffeine.com/logicaffeine_language/compile/fn.compile_all_scopes): One formula per scope permutation when a sentence has several quantifiers.
- [Get every parse of an ambiguous sentence](https://docs.logicaffeine.com/logicaffeine_language/compile/fn.compile_forest): All valid readings, lexical (noun/verb) and structural.
- [Carry pronouns and tense across sentences](https://docs.logicaffeine.com/logicaffeine_language/compile/fn.compile_discourse): Compiles a discourse, tracking temporal order; `compile_with_discourse` shares state across calls.
- [Lower modal operators to possible worlds](https://docs.logicaffeine.com/logicaffeine_language/compile/fn.compile_kripke): Kripke semantics: necessity and possibility become explicit quantification over worlds.
- [Add conversational implicatures](https://docs.logicaffeine.com/logicaffeine_language/compile/fn.compile_pragmatic): Scalar implicature enrichment on top of the literal reading.
- [Render a formula in another notation](https://docs.logicaffeine.com/logicaffeine_language/formatter/): The output formatters for logical expressions.
- [Parse English into a syntax tree](https://docs.logicaffeine.com/logicaffeine_language/parser/): The recursive-descent parser for natural language; the tree it builds is in `ast`.
- [Resolve anaphora and scope](https://docs.logicaffeine.com/logicaffeine_language/drs/): Discourse Representation Structures.
- [Look up how a word behaves](https://docs.logicaffeine.com/logicaffeine_lexicon/types/): The lexicon's grammatical and semantic categories: verb classes, transitivity, animacy, gender, number.

### Proof: every theorem checked by a small kernel
- [Prove a goal from premises and get a kernel-checked proof](https://docs.logicaffeine.com/logicaffeine_proof/verify/fn.prove_certify_check): Backward-chaining search, certification into a kernel term, and a kernel type-check in one call.
- [Prove a theorem written in English](https://docs.logicaffeine.com/logicaffeine_language/compile/fn.compile_theorem): Compiles and proves a theorem block.
- [Find out whether premises contradict each other](https://docs.logicaffeine.com/logicaffeine_proof/verify/fn.detect_conflict): Returns a kernel-checked proof of False and the clashing premises.
- [Prove a library of theorems in citation order](https://docs.logicaffeine.com/logicaffeine_proof/verify/fn.prove_library): Each theorem proved from its premises plus the conclusions it cites.
- [Type-check a term in the Calculus of Constructions](https://docs.logicaffeine.com/logicaffeine_kernel/fn.infer_type): The kernel itself: `Term`, `Context`, `normalize` and the universe hierarchy sit beside it.
- [Talk to the kernel in its vernacular](https://docs.logicaffeine.com/logicaffeine_kernel/interface/): The command language, its term parser and the REPL.
- [Re-check a proof term independently](https://docs.logicaffeine.com/logicaffeine_kernel/recheck/): A second checker, the de Bruijn criterion taken seriously; re-checkable certificates are in `certificate`.
- [Decide ring equalities](https://docs.logicaffeine.com/logicaffeine_kernel/ring/): Polynomial equality by normalization.
- [Decide integer arithmetic](https://docs.logicaffeine.com/logicaffeine_kernel/omega/): The Omega test; Fourier–Motzkin linear arithmetic is in `lia`.
- [Simplify and close goals by rewriting](https://docs.logicaffeine.com/logicaffeine_kernel/simp/): The simplifier tactic; congruence closure is in `cc`.
- [Prove interactively with tactics](https://docs.logicaffeine.com/logicaffeine_proof/tactic/): A tactic framework with a first-class goal state.
- [Write a proof as a script](https://docs.logicaffeine.com/logicaffeine_proof/tactic_script/): Proofs as text over the tactic combinators, the way a Lean or Coq proof reads.
- [Search a named lemma library](https://docs.logicaffeine.com/logicaffeine_proof/lemma_index/): `exact?`, `apply?` and premise selection over certified lemmas.
- [Get a counterexample when a goal is false](https://docs.logicaffeine.com/logicaffeine_proof/counterexample/): Exhibits a model instead of failing silently.
- [Read formal first-order logic text](https://docs.logicaffeine.com/logicaffeine_proof/formula/): A parser from formal FOL surface syntax into the prover's expressions.

### Solving: SAT and certified refutations
- [Decide a CNF formula](https://docs.logicaffeine.com/logicaffeine_proof/solve/fn.solve_structured): Routes through every cheap specialist before CDCL; `solve_comprehensive` runs the full arsenal.
- [Use the CDCL SAT core directly](https://docs.logicaffeine.com/logicaffeine_proof/cdcl/): Conflict-driven clause learning.
- [Read and write DIMACS CNF](https://docs.logicaffeine.com/logicaffeine_proof/dimacs/): The SAT-competition interchange format.
- [Emit a refutation other checkers accept](https://docs.logicaffeine.com/logicaffeine_proof/proof_emit/): DRAT, LRAT and DPR traces.
- [Check a refutation](https://docs.logicaffeine.com/logicaffeine_proof/rup/): Reverse unit propagation; propagation-redundancy checking is in `pr`.
- [Break symmetry, with a certificate](https://docs.logicaffeine.com/logicaffeine_proof/sym_certify/): Lex-leader symmetry-breaking predicates that come with a proof.
- [Count models, weighted and up to symmetry](https://docs.logicaffeine.com/logicaffeine_proof/solve/fn.weighted_model_count): The partition function, one solve per model orbit.
- [Reason with cardinality and pseudo-Boolean constraints](https://docs.logicaffeine.com/logicaffeine_proof/pseudo_boolean/): Cutting planes, a proof system stronger than resolution.
- [Reason about parity](https://docs.logicaffeine.com/logicaffeine_proof/xorsat/): XOR-SAT by Gaussian elimination over GF(2).
- [Model-check without Z3](https://docs.logicaffeine.com/logicaffeine_proof/bmc/): Bounded model checking, k-induction and vacuity, certified and browser-ready.

### Mathematics: exact, and certified where it counts
- [Solve linear systems exactly over the rationals](https://docs.logicaffeine.com/logicaffeine_proof/linalg/): Exact linear algebra over ℚ.
- [Turn an exact solve into a kernel-checked proof](https://docs.logicaffeine.com/logicaffeine_proof/linalg_certify/): Kernel-certified linear algebra.
- [Do linear algebra modulo a prime or a composite](https://docs.logicaffeine.com/logicaffeine_proof/modp/): GF(p); composite moduli by the Chinese Remainder Theorem are in `modm`.
- [Refute with polynomials](https://docs.logicaffeine.com/logicaffeine_proof/polycalc/): Polynomial calculus and the Nullstellensatz over GF(2); other fields and rings are in `polycalc_gfp` and `polycalc_zm`.
- [Refute with sums of squares](https://docs.logicaffeine.com/logicaffeine_proof/sos/): Positivstellensatz refutations over ℚ, kept exact.
- [Reduce a lattice](https://docs.logicaffeine.com/logicaffeine_proof/lattice/): LLL lattice reduction.
- [Compute on elliptic curves](https://docs.logicaffeine.com/logicaffeine_proof/elliptic/): Elliptic-curve primitives over ℤ/N.
- [Walk isogeny graphs](https://docs.logicaffeine.com/logicaffeine_proof/isogeny/): Certified isogeny torsion-image witnesses; 𝔽_{p²} arithmetic and the supersingular graph are in `fp2`.
- [Work with permutation groups](https://docs.logicaffeine.com/logicaffeine_proof/permgroup/): Schreier–Sims: a base and strong generating set.
- [Hold a homotopy type as an object](https://docs.logicaffeine.com/logicaffeine_proof/eilenberg_maclane/): Eilenberg–MacLane spaces K(A, n); Kan complexes are in `kan_complex`.
- [Attack a multivariate quadratic system](https://docs.logicaffeine.com/logicaffeine_proof/xl/): XL algebraic cryptanalysis by linearization.
- [Compute with arbitrary-precision integers](https://docs.logicaffeine.com/logicaffeine_base/numeric/): The numeric tower's foundation.
- [Carry physical units through a computation](https://docs.logicaffeine.com/logicaffeine_base/quantity/): Exact magnitudes with a physical dimension and a unit.
- [Count money exactly](https://docs.logicaffeine.com/logicaffeine_base/money/): An exact amount in a specific currency; exact calendar time is in `temporal`.
- [Compute in finite fields and wrapping rings](https://docs.logicaffeine.com/logicaffeine_base/gf256/): GF(2⁸); the wrapping integer rings ℤ/2ᵏ are in `word`.

### Verification: specifications against implementations
- [Prove two programs or specifications equivalent](https://docs.logicaffeine.com/logicaffeine_verify/equivalence/): Z3-backed semantic equivalence; the verify crate needs Z3 and a Pro-or-higher license.
- [Prove unbounded safety](https://docs.logicaffeine.com/logicaffeine_verify/ic3/): IC3/PDR; k-induction and interpolation are in `kinduction` and `interpolation`.
- [Synthesize a controller from temporal logic](https://docs.logicaffeine.com/logicaffeine_verify/synthesis/): Reactive synthesis from LTL.
- [Prove the compiled Rust matches the LOGOS source](https://docs.logicaffeine.com/logicaffeine_tv/): SMT translation validation.
- [Turn English hardware specs into assertions](https://docs.logicaffeine.com/logicaffeine_compile/codegen_sva/): SVA and PSL generation for hardware verification.

### Programs: running English code
- [Compile a LOGOS program](https://docs.logicaffeine.com/logicaffeine_compile/compile/): The compilation pipeline.
- [Run a program on the tree-walking interpreter](https://docs.logicaffeine.com/logicaffeine_compile/interpreter/): The tree-walking interpreter for imperative LOGOS.
- [Run a program on the bytecode VM](https://docs.logicaffeine.com/logicaffeine_compile/vm/): The register VM the JIT tiers up from.
- [Generate Rust from LOGOS](https://docs.logicaffeine.com/logicaffeine_compile/codegen/): Code generation from the LOGOS AST to Rust source.
- [Extract a program from a proof](https://docs.logicaffeine.com/logicaffeine_compile/extraction/): Program extraction from kernel terms to Rust.
- [Run concurrent programs deterministically](https://docs.logicaffeine.com/logicaffeine_runtime/): The scheduler, channels, seeds and choice traces behind reproducible concurrency.
- [Replicate data without conflicts](https://docs.logicaffeine.com/logicaffeine_data/crdt/): Conflict-free replicated data types.
- [Reach files, storage and the network](https://docs.logicaffeine.com/logicaffeine_system/): Platform IO, persistence, HTTP and post-quantum crypto kernels.
- [Drive the toolchain from the command line](https://docs.logicaffeine.com/logicaffeine_cli/cli/): largo: new, build, run, check, verify, publish.
- [Serve LOGOS to an editor](https://docs.logicaffeine.com/logicaffeine_lsp/): The language server.

## Crates

Every crate the site documents: its description, its map, and its top-level modules.

### [logicaffeine_language](https://docs.logicaffeine.com/logicaffeine_language/)
The LOGOS front end: English sentences to first-order logic, and the parser for LOGOS programs and LGX pages

- Map: [llms/logicaffeine_language.txt](https://docs.logicaffeine.com/llms/logicaffeine_language.txt) — 65 modules, 737 items
- [mod analysis](https://docs.logicaffeine.com/logicaffeine_language/analysis/): Static analysis passes for type and policy discovery.
- [mod arena](https://docs.logicaffeine.com/logicaffeine_language/arena/)
- [mod arena_ctx](https://docs.logicaffeine.com/logicaffeine_language/arena_ctx/): Arena context for AST allocation.
- [mod ast](https://docs.logicaffeine.com/logicaffeine_language/ast/): Abstract Syntax Tree types for both logical expressions and imperative statements.
- [mod ast_depth](https://docs.logicaffeine.com/logicaffeine_language/ast_depth/): The AST depth gate — “parsed ⇒ bounded”.
- [mod ast_map](https://docs.logicaffeine.com/logicaffeine_language/ast_map/): An exhaustive, rebuilding traversal of the imperative AST.
- [mod compile](https://docs.logicaffeine.com/logicaffeine_language/compile/): Compilation API
- [mod debug](https://docs.logicaffeine.com/logicaffeine_language/debug/): Debug display utilities for AST types with interner access.
- [mod diagnostic](https://docs.logicaffeine.com/logicaffeine_language/diagnostic/): The canonical machine-readable diagnostic surface: `logos-diagnostic/1`.
- [mod drs](https://docs.logicaffeine.com/logicaffeine_language/drs/): Discourse Representation Structure (DRS) for anaphora resolution and scope tracking.
- [mod error](https://docs.logicaffeine.com/logicaffeine_language/error/): Error types and display formatting for parse errors.
- [mod formatter](https://docs.logicaffeine.com/logicaffeine_language/formatter/): Output formatters for logical expressions.
- [mod import_format](https://docs.logicaffeine.com/logicaffeine_language/import_format/): Canonical formatting of a module’s `Import` statements — the pit-of-success default so import blocks never need manual bikeshedding.
- [mod intern](https://docs.logicaffeine.com/logicaffeine_language/intern/)
- [mod lambda](https://docs.logicaffeine.com/logicaffeine_language/lambda/): Lambda calculus transformations for Montague-style compositional semantics.
- [mod lexer](https://docs.logicaffeine.com/logicaffeine_language/lexer/): Two-stage lexer for LOGOS natural language input.
- [mod lexicon](https://docs.logicaffeine.com/logicaffeine_language/lexicon/): Lexicon: Vocabulary lookup functions
- [mod lgx](https://docs.logicaffeine.com/logicaffeine_language/lgx/): LGX — the LOGOS web framework’s template layer: real HTML with Jinja-style `{…}` tags, component-scoped CSS, and the structural checks a template needs before any LOGOS expression inside it is parsed.
- [mod lint](https://docs.logicaffeine.com/logicaffeine_language/lint/): The value-semantics copy lint.
- [mod mwe](https://docs.logicaffeine.com/logicaffeine_language/mwe/): Multi-Word Expression (MWE) processing.
- [mod ontology](https://docs.logicaffeine.com/logicaffeine_language/ontology/): Ontology module for bridging anaphora and sort compatibility checking.
- [mod optimization](https://docs.logicaffeine.com/logicaffeine_language/optimization/): The registry of compiler optimization toggles.
- [mod parser](https://docs.logicaffeine.com/logicaffeine_language/parser/): Recursive descent parser for natural language to first-order logic.
- [mod pragmatics](https://docs.logicaffeine.com/logicaffeine_language/pragmatics/): Post-parse pragmatic inference transformations.
- [mod printer](https://docs.logicaffeine.com/logicaffeine_language/printer/): English rendering of imperative expressions — the shared surface behind power-assert failure messages, property counterexamples, and mutation survivor reports.
- [mod proof_convert](https://docs.logicaffeine.com/logicaffeine_language/proof_convert/): Conversion from parser AST to proof engine representation.
- [mod registry](https://docs.logicaffeine.com/logicaffeine_language/registry/): Symbol registry for consistent variable naming in FOL output.
- [mod runtime_lexicon](https://docs.logicaffeine.com/logicaffeine_language/runtime_lexicon/): Runtime JSON-based lexicon loading (requires `dynamic-lexicon` feature).
- [mod scope](https://docs.logicaffeine.com/logicaffeine_language/scope/): Scope stack for variable binding during code generation.
- [mod semantics](https://docs.logicaffeine.com/logicaffeine_language/semantics/): Semantic transformations for logical expressions.
- [mod session](https://docs.logicaffeine.com/logicaffeine_language/session/): Session Manager for Incremental Evaluation
- [mod source_format](https://docs.logicaffeine.com/logicaffeine_language/source_format/): The canonical LOGOS source formatter.
- [mod style](https://docs.logicaffeine.com/logicaffeine_language/style/): ANSI terminal color styling for error messages.
- [mod suggest](https://docs.logicaffeine.com/logicaffeine_language/suggest/): Spelling suggestions for unknown words.
- [mod symbol_dict](https://docs.logicaffeine.com/logicaffeine_language/symbol_dict/): Symbol Dictionary Extraction
- [mod teach](https://docs.logicaffeine.com/logicaffeine_language/teach/): The lesson table for LOGOS constructs: every lesson a surface shows (LSP hover, completion documentation, the REPL’s `:explain`) comes from this table, so the editor and the terminal always teach the same thing.
- [mod token](https://docs.logicaffeine.com/logicaffeine_language/token/): Token types for the LOGOS lexer and parser.
- [mod token_class](https://docs.logicaffeine.com/logicaffeine_language/token_class/): How LOGOS tokens are classified for highlighting: parts of speech are the syntax — verbs paint as functions, nouns as types, adjectives as modifiers. Every highlighting surface (LSP semantic tokens, the terminal REPL, any future renderer) derives its colors from this mapping, so they can never disagree.
- [mod transpile](https://docs.logicaffeine.com/logicaffeine_language/transpile/): Transpilation from AST to first-order logic notation.
- [mod view](https://docs.logicaffeine.com/logicaffeine_language/view/): Owned view types for AST serialization and display.
- [mod visitor](https://docs.logicaffeine.com/logicaffeine_language/visitor/): AST visitor pattern for traversing logical expressions.

### [logicaffeine_compile](https://docs.logicaffeine.com/logicaffeine_compile/)
The LOGOS compiler: type checking, the optimizer, the interpreter and bytecode VM, and the Rust, C, WASM, RISC-V, CUDA and hardware backends

- Map: [llms/logicaffeine_compile.txt](https://docs.logicaffeine.com/llms/logicaffeine_compile.txt) — 445 modules, 5770 items
- [mod accel](https://docs.logicaffeine.com/logicaffeine_compile/accel/): The accelerator backends’ shared framework: the analog plane, the Plasticine PCU mesh and the SambaNova RDU all run a program the same way, as a host program with device regions.
- [mod analysis](https://docs.logicaffeine.com/logicaffeine_compile/analysis/): Compile-time analysis passes for the LOGOS compilation pipeline.
- [mod aot_unsupported](https://docs.logicaffeine.com/logicaffeine_compile/aot_unsupported/): The ops no single-device AOT backend can run — concurrency, virtual-time scheduling, and networking — classified once so the device tiers (Tenstorrent baby core, one CUDA kernel launch) cannot drift apart on their refusal set.
- [mod arena](https://docs.logicaffeine.com/logicaffeine_compile/arena/)
- [mod arena_ctx](https://docs.logicaffeine.com/logicaffeine_compile/arena_ctx/)
- [mod ast](https://docs.logicaffeine.com/logicaffeine_compile/ast/): Abstract Syntax Tree types for both logical expressions and imperative statements.
- [mod bringup](https://docs.logicaffeine.com/logicaffeine_compile/bringup/): Model bring-up: a checkpoint’s one program, lowered by every chip that runs it.
- [mod codegen](https://docs.logicaffeine.com/logicaffeine_compile/codegen/): Code generation from LOGOS AST to Rust source code.
- [mod codegen_ana](https://docs.logicaffeine.com/logicaffeine_compile/codegen_ana/): LOGOS → analog spatial fabric (FPAA-style mixed-signal coprocessor) — the analog lane.
- [mod codegen_c](https://docs.logicaffeine.com/logicaffeine_compile/codegen_c/)
- [mod codegen_cuda](https://docs.logicaffeine.com/logicaffeine_compile/codegen_cuda/): LOGOS → CUDA AOT codegen tier. Emits ONE self-contained CUDA program — a `__global__` kernel that runs a whole LOGOS program on a single GPU thread, plus a host orchestrator — for the integer/bool scalar fragment of the language.
- [mod codegen_dram](https://docs.logicaffeine.com/logicaffeine_compile/codegen_dram/): codegen_dram — the DRAM compute-in-memory target (ComputeDRAM bulk bitwise + RowClone).
- [mod codegen_mx](https://docs.logicaffeine.com/logicaffeine_compile/codegen_mx/): LOGOS → mixed-signal XPU — the unification of the digital whole-program engine (`crate::codegen_sva`’s wprog engine, exact ≡VM) and the analog plane (`crate::codegen_ana`, ε-certified floats / ½-grid-certified-exact integers).
- [mod codegen_riscv](https://docs.logicaffeine.com/logicaffeine_compile/codegen_riscv/): LOGOS → RISC-V AOT codegen tier. Lowers the register bytecode `CompiledProgram` — the SAME IR the WASM backend and the Silicon ISA emitter consume — to RV64GC assembly text (SysV lp64d ABI, glibc), which a RISC-V GCC assembles+links and `qemu-user` runs, byte-for-byte identical to the VM.
- [mod codegen_sass](https://docs.logicaffeine.com/logicaffeine_compile/codegen_sass/): codegen_sass — the foundation of our OWN sm_86 SASS assembler (the MaxAs / turingas lever).
- [mod codegen_sva](https://docs.logicaffeine.com/logicaffeine_compile/codegen_sva/): SVA/PSL Code Generation for Hardware Verification
- [mod codegen_tt](https://docs.logicaffeine.com/logicaffeine_compile/codegen_tt/): LOGOS → Tenstorrent (TT-Metalium) AOT codegen tier. Emits a complete single-Tensix-core TT-Metalium program — a host orchestrator plus a data-movement compute kernel that runs on one baby RISC-V core (`DataMovementProcessor::RISCV_0`) — for the scalar-compute fragment of the benchmark suite.
- [mod compile](https://docs.logicaffeine.com/logicaffeine_compile/compile/): LOGOS Compilation Pipeline
- [mod concurrency](https://docs.logicaffeine.com/logicaffeine_compile/concurrency/): Concurrency determinacy model + classifier.
- [mod crypto_accel](https://docs.logicaffeine.com/logicaffeine_compile/crypto_accel/): Native SHA-256 / HMAC-SHA256 / PBKDF2-HMAC-SHA256, byte-identical to the pure-LOGOS reference in `assets/std/crypto.lg`.
- [mod debug](https://docs.logicaffeine.com/logicaffeine_compile/debug/): The bytecode debugger bridge — drives the LOGOS VM one op at a time for the Studio debug drawer, with breakpoints, step-over / step-out, and time-travel (step backwards through executed ops). Single-task, bytecode tier (`tier: None`) so granularity is exactly one op and behaviour is identical to a normal run.
- [mod debug_session](https://docs.logicaffeine.com/logicaffeine_compile/debug_session/): W11 — `DebugSession`: the one seam the DAP adapter and the Studio drawer both sit on.
- [mod diagnostic](https://docs.logicaffeine.com/logicaffeine_compile/diagnostic/): Diagnostic bridge for translating Rust errors to LOGOS.
- [mod drs](https://docs.logicaffeine.com/logicaffeine_compile/drs/): Discourse Representation Structure (DRS) for anaphora resolution and scope tracking.
- [mod error](https://docs.logicaffeine.com/logicaffeine_compile/error/): Error types and display formatting for parse errors.
- [mod extraction](https://docs.logicaffeine.com/logicaffeine_compile/extraction/): Program extraction from kernel terms to Rust.
- [mod formatter](https://docs.logicaffeine.com/logicaffeine_compile/formatter/): Output formatters for logical expressions.
- [mod frame_eval](https://docs.logicaffeine.com/logicaffeine_compile/frame_eval/): FrameEval — evaluate a LOGOS expression against a paused frame’s bindings.
- [mod intern](https://docs.logicaffeine.com/logicaffeine_compile/intern/)
- [mod interpreter](https://docs.logicaffeine.com/logicaffeine_compile/interpreter/): Tree-walking interpreter for LOGOS imperative code.
- [mod lexer](https://docs.logicaffeine.com/logicaffeine_compile/lexer/): Two-stage lexer for LOGOS natural language input.
- [mod loader](https://docs.logicaffeine.com/logicaffeine_compile/loader/): Module loader for multi-file LOGOS projects.
- [mod model](https://docs.logicaffeine.com/logicaffeine_compile/model/): Models as data. A checkpoint’s own metadata describes its architecture (`spec`); this module reads it — a GGUF file (`gguf`), or a Hugging Face directory of safetensors shards in place (`hf`, `safetensors`) —, dequantizes its weights in every format a model ships in (`quant`), tokenizes text as the checkpoint’s vocabulary does (`tokenizer`), hashes Qwen3.8-Flash-Next’s n-gram embedding rows (`ngram_hash`), writes what it computes as a LOGOS program (`author`) whose weights it binds to the checkpoint’s tensors (`bind`) as the layout its arms read presents them (`layout`), names each cut of that one program every backend lowers (`program`), and evaluates that computation in `f64` as the oracle every lane is measured against (`reference`).
- [mod monomorphize](https://docs.logicaffeine.com/logicaffeine_compile/monomorphize/): Monomorphization: a generic program rewritten into the concrete program it stands for, for the tiers with no generics of their own.
- [mod mwe](https://docs.logicaffeine.com/logicaffeine_compile/mwe/): Multi-Word Expression (MWE) processing.
- [mod observe](https://docs.logicaffeine.com/logicaffeine_compile/observe/): The observation channel’s emission buffer. When an observation statement (`Note`/`Warn`/`Record`) executes, it emits a structured `ObsEvent` to a per-run thread-local buffer, drained by sinks (the in-memory test sink today; console and wire in Wave 16). This is the SEPARATE observation channel (D0.1) — it never touches program output.
- [mod optimization](https://docs.logicaffeine.com/logicaffeine_compile/optimization/): The registry of compiler optimization toggles.
- [mod optimize](https://docs.logicaffeine.com/logicaffeine_compile/optimize/)
- [mod page_host](https://docs.logicaffeine.com/logicaffeine_compile/page_host/): One driver, several page tiers.
- [mod parser](https://docs.logicaffeine.com/logicaffeine_compile/parser/): Recursive descent parser for natural language to first-order logic.
- [mod program_bindings](https://docs.logicaffeine.com/logicaffeine_compile/program_bindings/): Program bindings on the tiers that compile a program ahead of time.
- [mod registry](https://docs.logicaffeine.com/logicaffeine_compile/registry/)
- [mod repl](https://docs.logicaffeine.com/logicaffeine_compile/repl/): `ReplSession` — the replay-based interactive session behind `largo repl` (and any future notebook surface).
- [mod replay](https://docs.logicaffeine.com/logicaffeine_compile/replay/): The `.replay` failure artifact.
- [mod semantics](https://docs.logicaffeine.com/logicaffeine_compile/semantics/): The shared semantics kernel.
- [mod sourcemap](https://docs.logicaffeine.com/logicaffeine_compile/sourcemap/): Source map for the diagnostic bridge.
- [mod spatial](https://docs.logicaffeine.com/logicaffeine_compile/spatial/): The spatial IR — the one program every spatial backend lowers FROM.
- [mod style](https://docs.logicaffeine.com/logicaffeine_compile/style/)
- [mod tensor_graph](https://docs.logicaffeine.com/logicaffeine_compile/tensor_graph/): The tensor graph — programs as tensor ops, and the transforms over them.
- [mod tensor_recognize](https://docs.logicaffeine.com/logicaffeine_compile/tensor_recognize/): Backend-neutral tensor-op recognition (LOGOS AST → typed specs), shared by every codegen backend. Backend-agnostic tensor-op recognition — LOGOS AST -> typed op specs, shared by every codegen backend.
- [mod testrun](https://docs.logicaffeine.com/logicaffeine_compile/testrun/): The `largo test` runner core.
- [mod token](https://docs.logicaffeine.com/logicaffeine_compile/token/): Token types for the LOGOS lexer and parser.
- [mod ui_bridge](https://docs.logicaffeine.com/logicaffeine_compile/ui_bridge/): UI bridge for web interface integration.
- [mod vm](https://docs.logicaffeine.com/logicaffeine_compile/vm/): Register bytecode VM.
- [mod web_host](https://docs.logicaffeine.com/logicaffeine_compile/web_host/): The browser host for a LOGOS→WASM DOM app — shared by the CLI (`largo emit wasm-dom` / `largo serve`) and the web Studio’s live preview so both render a LOGOS app identically. It supplies the real DOM behind the `dom_*` imports, allocates host `Text` into linear memory, and fires event/fetch callbacks through the exported `__logos_call_closure` trampoline (the production analog of the test `MockDom`). It also carries the default theme, the favicon, and the build-error overlay so a fresh LOGOS web app is beautiful — and legible when it breaks — with zero CSS written.

### [logicaffeine_proof](https://docs.logicaffeine.com/logicaffeine_proof/)
Kernel-checked proof search and tactics, certified SAT/CDCL with DRAT/LRAT output, and a number-theory and cryptanalysis library

- Map: [llms/logicaffeine_proof.txt](https://docs.logicaffeine.com/llms/logicaffeine_proof.txt) — 109 modules, 1118 items
- [mod affine](https://docs.logicaffeine.com/logicaffeine_proof/affine/): The affine group `AGL(n,2)` — the symmetry a permutation break cannot see.
- [mod affine_gfp](https://docs.logicaffeine.com/logicaffeine_proof/affine_gfp/): The affine group `AGL(n,p)` over `GF(p)` — the mod-`p` generalization of the affine break.
- [mod aig](https://docs.logicaffeine.com/logicaffeine_proof/aig/): And-inverter graphs: a circuit as two-input AND gates over complemented edges, read and written in the AIGER format (Biere, The AIGER And-Inverter Graph Format, Version 20071012, and its 1.9 extension).
- [mod ait](https://docs.logicaffeine.com/logicaffeine_proof/ait/): Algorithmic information theory — certified description-length objects
- [mod arith](https://docs.logicaffeine.com/logicaffeine_proof/arith/): Proof-PRODUCING arithmetic oracle (untrusted search, kernel-checked proof).
- [mod bmc](https://docs.logicaffeine.com/logicaffeine_proof/bmc/): Bounded model checking, k-induction, and vacuity over `ProofExpr` — pure-Rust, certified, Z3-free, browser-ready.
- [mod cardinality](https://docs.logicaffeine.com/logicaffeine_proof/cardinality/): Cardinality constraints over boolean `ProofExpr` atoms — the missing primitive that lets the certified solver answer “at most / at least / exactly `k` of these are true”. Encoded with Sinz’s sequential counter (linear in `n·k`, fresh auxiliary atoms under a caller-chosen prefix), so the result is an ordinary boolean obligation the existing CNF/CDCL/RUP pipeline discharges. This is the building block for SAT-based optimization (`crate::optimize`).
- [mod cdcl](https://docs.logicaffeine.com/logicaffeine_proof/cdcl/): A conflict-driven clause-learning (CDCL) SAT core — the modern competition-grade engine, built to the lineage that made SAT practical: two-watched-literal unit propagation (Moskewicz et al., Chaff, 2001), first-UIP conflict analysis with learned clauses and non-chronological backtracking (Marques-Silva & Sakallah, GRASP, 1996), VSIDS-style activity decisions, and Luby restarts (Luby et al., 1993). The clean reference implementation it follows is Eén & Sörensson’s MiniSat (2003).
- [mod certifier](https://docs.logicaffeine.com/logicaffeine_proof/certifier/): The Certifier: Converts DerivationTrees to Kernel Terms.
- [mod cnf](https://docs.logicaffeine.com/logicaffeine_proof/cnf/): Tseitin clausification: a grounded, quantifier-free `ProofExpr` → CNF over the CDCL core’s `Lit`s (Tseitin, 1968 — the standard linear-size equisatisfiable transform that introduces one auxiliary variable per compound subformula). This is the bridge from the logic-grid encoding (closures, at-most-one, of-pair, clue clauses) to the `crate::cdcl` SAT engine, giving the Untrusted trust tier: solve `premises ∧ ¬goal`; UNSAT ⇒ the goal is entailed. The same CNF feeds the RUP checker (the fast trust tier) and is the input an AllDifferent GAC propagator filters.
- [mod coalgebra](https://docs.logicaffeine.com/logicaffeine_proof/coalgebra/): The coalgebraic / `Poly` view, made into checked code rather than narration.
- [mod complexity](https://docs.logicaffeine.com/logicaffeine_proof/complexity/): Certified complexity bounds — a refutation that carries a checkable proof of its own size.
- [mod counterexample](https://docs.logicaffeine.com/logicaffeine_proof/counterexample/): Counterexamples — when a goal is FALSE, exhibit a model instead of failing silently. Lean ships no built-in counterexample finder with its automation; this closes that gap.
- [mod counting_principle](https://docs.logicaffeine.com/logicaffeine_proof/counting_principle/): Fast refuter for the modular counting principle `Count_q(n)`: partition an `n`-element set into blocks of size `q`. Encoded as: one Boolean per `q`-subset (block); a coverage clause per element (the incident blocks, at least one chosen); and a disjointness clause for every pair of overlapping blocks. It is unsatisfiable exactly when `q ∤ n`.
- [mod crush](https://docs.logicaffeine.com/logicaffeine_proof/crush/): `crush` — the grind-style closer: E-match quantified equality lemmas into the ground e-graph, then discharge the goal by certified congruence closure.
- [mod cubical](https://docs.logicaffeine.com/logicaffeine_proof/cubical/): A general `d`-dimensional cubical-homology engine — one engine, every rung of the ladder.
- [mod cycle_ratio](https://docs.logicaffeine.com/logicaffeine_proof/cycle_ratio/): The maximum cycle ratio of a weighted digraph, exact and certified: the bound a loop puts on a clock period.
- [mod cyclotomic](https://docs.logicaffeine.com/logicaffeine_proof/cyclotomic/): Power-of-two cyclotomic ring `R = ℤ[X]/(Xⁿ + 1)`, `n = 2ᵏ`
- [mod decide](https://docs.logicaffeine.com/logicaffeine_proof/decide/): `decide` — proof by evaluation for closed decidable goals.
- [mod development](https://docs.logicaffeine.com/logicaffeine_proof/development/): A formal-development parser: the body of a `## Theory` block — a sequence of `Axiom` and `Theorem` declarations in formal notation — into the axioms and `LibraryTheorem`s the multi-theorem driver consumes.
- [mod dimacs](https://docs.logicaffeine.com/logicaffeine_proof/dimacs/): DIMACS CNF parsing and printing — the SAT-competition interchange format, and the front door for running arbitrary instances through the solver.
- [mod discrimination](https://docs.logicaffeine.com/logicaffeine_proof/discrimination/): First-order discrimination tree: the shared pattern index under `simp` rule lookup, `exact?`/`apply?` library search, and `crush`’s E-matching.
- [mod eilenberg_maclane](https://docs.logicaffeine.com/logicaffeine_proof/eilenberg_maclane/): The general Eilenberg–MacLane construction `K(A, n)` — one engine, every rung of the tower.
- [mod elliptic](https://docs.logicaffeine.com/logicaffeine_proof/elliptic/): Elliptic-curve primitives over ℤ/N — the additive→multiplicative lift
- [mod engine](https://docs.logicaffeine.com/logicaffeine_proof/engine/): Backward chaining proof engine.
- [mod error](https://docs.logicaffeine.com/logicaffeine_proof/error/): Error types for proof search and unification.
- [mod factor](https://docs.logicaffeine.com/logicaffeine_proof/factor/): Structural factoring: the AIT thesis applied to public-key crypto.
- [mod families](https://docs.logicaffeine.com/logicaffeine_proof/families/): Parametric generators for symmetry-rich SAT families — the canonical hard cases where symmetry breaking earns its keep. They are programmatic (reproducible, offline, parametric) rather than vendored `.cnf` files, and each is pinned to its known verdict so the solver and the certified pipeline can be tested against ground truth.
- [mod formula](https://docs.logicaffeine.com/logicaffeine_proof/formula/): A self-contained parser from formal first-order-logic surface text to `ProofExpr`.
- [mod fp2](https://docs.logicaffeine.com/logicaffeine_proof/fp2/): 𝔽_{p²} arithmetic and the supersingular isogeny graph
- [mod fraig](https://docs.logicaffeine.com/logicaffeine_proof/fraig/): Combinational equivalence by incremental SAT sweeping, certified by one derivation.
- [mod gf2](https://docs.logicaffeine.com/logicaffeine_proof/gf2/): The general linear group GL(n,2) and the invertibility constant — where the reciprocal SAT-threshold sum comes home.
- [mod grid_solver](https://docs.logicaffeine.com/logicaffeine_proof/grid_solver/): A fast, certified finite-domain (logic-grid) solver.
- [mod grounding](https://docs.logicaffeine.com/logicaffeine_proof/grounding/): Finite-domain grounding.
- [mod groupoid](https://docs.logicaffeine.com/logicaffeine_proof/groupoid/): The action groupoid — what symmetry breaking means, categorically, as checked code.
- [mod hints](https://docs.logicaffeine.com/logicaffeine_proof/hints/): Socratic Hint Engine - Generates pedagogical hints for proof guidance.
- [mod hornsat](https://docs.logicaffeine.com/logicaffeine_proof/hornsat/): Horn-SAT in linear time via unit propagation (forward chaining).
- [mod hypercube](https://docs.logicaffeine.com/logicaffeine_proof/hypercube/): The Boolean hypercube `{0,1}ⁿ` and its subcube cover — the geometric substrate beneath SAT, and the executable form of the Lean formalization’s `HypercubeSAT`.
- [mod hyperelliptic](https://docs.logicaffeine.com/logicaffeine_proof/hyperelliptic/): Genus-2 curves and the Richelot (2,2)-isogeny — the abelian-surface mechanism
- [mod inprocess](https://docs.logicaffeine.com/logicaffeine_proof/inprocess/): Certified inprocessing: clause-database simplifications that emit a machine-checkable proof.
- [mod interval_replay](https://docs.logicaffeine.com/logicaffeine_proof/interval_replay/): Independent range-safety checker for analog netlist claims — the trust core of the analog lane’s `RangeCertificate`, in the same spirit as this crate’s PR/RUP checker: a small, dependency-free replay the certificate producer cannot influence.
- [mod interval_sched](https://docs.logicaffeine.com/logicaffeine_proof/interval_sched/): Interval scheduling in O(n log n) via a sweep line — the matching/Hall reasoner reaching into resource allocation over time.
- [mod isogeny](https://docs.logicaffeine.com/logicaffeine_proof/isogeny/): Certified isogeny torsion-image witnesses — the SIDH/SIKE public-data structure, in the prover
- [mod kan_complex](https://docs.logicaffeine.com/logicaffeine_proof/kan_complex/): Actually having an ∞-groupoid — not its invariants, the object itself, with its defining property machine-verified.
- [mod lattice](https://docs.logicaffeine.com/logicaffeine_proof/lattice/): LLL lattice reduction — the geometric lens of the compression campaign.
- [mod lemma_index](https://docs.logicaffeine.com/logicaffeine_proof/lemma_index/): `exact?` / `apply?` and premise selection: search over a NAMED, certified lemma library.
- [mod linalg](https://docs.logicaffeine.com/logicaffeine_proof/linalg/): Exact linear algebra over ℚ — the certified core of the LOGOS numerical stack.
- [mod linalg_certify](https://docs.logicaffeine.com/logicaffeine_proof/linalg_certify/): Kernel-certified linear algebra: turn an exact solve into a KERNEL-CHECKED PROOF TERM.
- [mod linarith_solve](https://docs.logicaffeine.com/logicaffeine_proof/linarith_solve/): The decision core for linear integer arithmetic: Fourier-Motzkin elimination that tracks the non-negative combination it eliminates with, so an unsatisfiable system yields its Farkas certificate — the multipliers `λᵢ ≥ 0` on the original constraints such that `Σ λᵢ·constraintᵢ` is a positive constant `≤ 0` (a contradiction). The proof engine reconstructs a kernel proof from those multipliers via `le_mul_nonneg`/`le_add_mono` + the Bool no-confusion discriminator. Pure and self-contained — no kernel, no certificates here.
- [mod lll](https://docs.logicaffeine.com/logicaffeine_proof/lll/): Satisfiability from sparsity — the Lovász Local Lemma certificate and its constructive Moser–Tardos witness. The lower bookend to the first-moment bound.
- [mod lrat](https://docs.logicaffeine.com/logicaffeine_proof/lrat/): LRAT refutations at scale: hint chains found by watched-literal propagation, trimmed to the clauses a refutation uses, and replayed by a checker that trusts nothing the search did.
- [mod lyapunov](https://docs.logicaffeine.com/logicaffeine_proof/lyapunov/): Lyapunov-function synthesis — don’t search for the proof, discover the measure that collapses the problem, and let the proof fall out as a corollary.
- [mod macaulay](https://docs.logicaffeine.com/logicaffeine_proof/macaulay/): Monomials and the Macaulay matrix — the combinatorial skeleton of the XL algorithm.
- [mod matching](https://docs.logicaffeine.com/logicaffeine_proof/matching/): Certified bipartite-matching infeasibility — the polynomial reasoner for pigeonhole-shaped problems that are exponential for resolution (and therefore for any CDCL SAT solver, ours included).
- [mod min_cost_flow](https://docs.logicaffeine.com/logicaffeine_proof/min_cost_flow/): Minimum-cost flow, exact and certified: the dual of every scheduling and retiming problem whose constraints are differences of two variables, which is how a register cut of least area at a target clock is found.
- [mod modm](https://docs.logicaffeine.com/logicaffeine_proof/modm/): Linear algebra over `ℤ/m` for composite `m`, by the Chinese Remainder Theorem — the multiplicative symmetry break. A system `Σ aᵢ·xᵢ ≡ c (mod m)` over a squarefree modulus `m = p₁·…·p_t` factors, through the ring isomorphism `ℤ/m ≅ GF(p₁) × … × GF(p_t)`, into one independent system over each prime field — each decided by `crate::modp::solve` — and the per-field solutions are recombined by CRT. The factorization of the modulus is the symmetry that splits the problem; the prime fields are the irreducible pieces:
- [mod modp](https://docs.logicaffeine.com/logicaffeine_proof/modp/): Linear algebra over `GF(p)` — the mod-`p` generalization of the GF(2) parity cut (`crate::xorsat`).
- [mod omega_solve](https://docs.logicaffeine.com/logicaffeine_proof/omega_solve/): `omega` — linear INTEGER arithmetic, the discreteness-aware layer over the rational Farkas core.
- [mod optimize](https://docs.logicaffeine.com/logicaffeine_proof/optimize/): Certified SAT-based optimization. We have no native MaxSAT/ILP solver, so we minimise an integer cost the honest way: binary-search the smallest feasible cost bound, where each query is a certified decision (`prove_unsat` → `Sat` witness or RUP-`Refuted`). The result is a certified optimum — a witness at the optimum and a refutation at optimum−1 — not merely a value we happened to find.
- [mod ordering](https://docs.logicaffeine.com/logicaffeine_proof/ordering/): The ordering-principle specialist — a polynomial-time recognizer + refuter for GT(n), the linear-ordering contradiction. GT(n) asserts a strict total order (totality + antisymmetry + transitivity) in which every element has a strictly greater one (“no maximum”). That is impossible: a finite strict total order always has a maximum. So a complete GT(n) core is unsatisfiable, and any formula containing it (a superset of an UNSAT core) is UNSAT.
- [mod parity_cardinality](https://docs.logicaffeine.com/logicaffeine_proof/parity_cardinality/): Fast refuter for the coupled exactly-one + parity family. An exactly-one group (an at-least-one clause plus the full at-most-one clique over its variables) forces EXACTLY one of its selectors true, so their XOR is `1` (odd). If the formula’s parity substructure forces that same XOR to `0` (even), the two are inconsistent and the formula is UNSAT — the mixed obstruction neither theory sees alone.
- [mod period](https://docs.logicaffeine.com/logicaffeine_proof/period/): The period / order seam — the classical shell of Shor’s algorithm
- [mod permgroup](https://docs.logicaffeine.com/logicaffeine_proof/permgroup/): Schreier–Sims: a base and strong generating set (BSGS) for a permutation group — the non-abelian generalization of Gaussian elimination, and the last rung of the algebra ladder (GF(2)→GF(p)→ℤ/m linear; this is the group level).
- [mod pigeonhole](https://docs.logicaffeine.com/logicaffeine_proof/pigeonhole/): Pigeonhole / bipartite-matching detection for the general solver — the cardinality reasoning that lets `prove_unsat` win on pigeonhole-shaped formulas in POLYNOMIAL time.
- [mod polycalc](https://docs.logicaffeine.com/logicaffeine_proof/polycalc/): Polynomial Calculus / Nullstellensatz over `GF(2)` — the algebraic proof system that subsumes the linear cuts (parity is its degree-1 fragment) and, at higher degree, refutes strictly more.
- [mod postnikov](https://docs.logicaffeine.com/logicaffeine_proof/postnikov/): The Postnikov `k`-invariant — the gluing data of a 2-type, and the obstruction to breaking it into a product.
- [mod pr](https://docs.logicaffeine.com/logicaffeine_proof/pr/): The PR (propagation-redundancy) checker — the trust tier for model-removing clause additions, and the keystone that makes certified symmetry breaking possible.
- [mod progress_complex](https://docs.logicaffeine.com/logicaffeine_proof/progress_complex/): Genuine higher homotopy, at last — `π₁ ≠ 0` from real concurrency, the hole is the deadlock.
- [mod proof](https://docs.logicaffeine.com/logicaffeine_proof/proof/): Shared proof-step vocabulary for the certified checkers.
- [mod proof_emit](https://docs.logicaffeine.com/logicaffeine_proof/proof_emit/): Standard proof-trace emission — DRAT, LRAT, and DPR text from our in-memory `ProofStep` stream, so the certified refutations this crate produces are not merely self-checked but replayable by the SAT community’s independent (and in `cake_lpr`’s case formally verified) checkers.
- [mod proof_rewrite](https://docs.logicaffeine.com/logicaffeine_proof/proof_rewrite/): The proof-rewrite 2-cells — independent refutation steps commute, and the commutation squares make the space of proof-orderings a contractible `CAT(0)` cube complex. This is the honest higher structure the symmetry tower pointed at, and it is genuine 2-dimensional homotopy: not a faked `π₂`, but the coherence theorem for proofs — every way of reordering independent steps is coherently the same, up to all higher homotopies.
- [mod pseudo_boolean](https://docs.logicaffeine.com/logicaffeine_proof/pseudo_boolean/): Pseudo-Boolean constraints + cutting planes — a proof system STRICTLY STRONGER than resolution.
- [mod rainbow](https://docs.logicaffeine.com/logicaffeine_proof/rainbow/): Rainbow — Jintai Ding & Dieter Schmidt’s multilayer Oil-and-Vinegar signature (ACNS 2005), the multivariate scheme our XL engine is built to attack. This is a faithful reference over GF(2^8): a two-layer central map `F`, invertible affine transforms `S` and `T`, public key `P = S ∘ F ∘ T`, and the Oil-and-Vinegar trapdoor that inverts `F` at signing time.
- [mod register_alloc](https://docs.logicaffeine.com/logicaffeine_proof/register_alloc/): Certified linear-scan register allocation — the matching/Hall reasoner as a compiler back-end.
- [mod relax_replay](https://docs.logicaffeine.com/logicaffeine_proof/relax_replay/): Settled-answer replay — the residual certificate for physics-solved linear systems.
- [mod revgate](https://docs.logicaffeine.com/logicaffeine_proof/revgate/): Certify reversible logic gates as bijections.
- [mod rule_search](https://docs.logicaffeine.com/logicaffeine_proof/rule_search/): `aesop`-style rule-set search: turn `auto`’s fixed cascade into an extensible, best-first search over registered rules.
- [mod rup](https://docs.logicaffeine.com/logicaffeine_proof/rup/): The RUP (Reverse Unit Propagation) linear checker — the fast default trust tier.
- [mod sat](https://docs.logicaffeine.com/logicaffeine_proof/sat/): Propositional SAT-discharge of a `ProofExpr` obligation — the engine behind in-browser, Z3-free hardware proving.
- [mod satcli](https://docs.logicaffeine.com/logicaffeine_proof/satcli/): The SAT command-line driver shared by `logos-sat` and `largo sat`.
- [mod sdcl](https://docs.logicaffeine.com/logicaffeine_proof/sdcl/): Satisfaction-Driven Clause Learning (Heule, Kiesl & Seidl) — the engine that reasons at the Extended-Frege level by discovering propagation-redundant clauses, not just learning implied ones. It is symmetry breaking taken to its limit: where certified symmetry breaking needs an automorphism to supply a witness, SDCL finds the witness by solving the positive reduct — a smaller SAT problem — so it works on any structure, symmetric or not.
- [mod seq_equiv](https://docs.logicaffeine.com/logicaffeine_proof/seq_equiv/): Sequential equivalence by unrolling: a pipelined circuit proven equal to its combinational reference at its latency, or two pipelines of different depths proven to compute the same transaction.
- [mod simp](https://docs.logicaffeine.com/logicaffeine_proof/simp/): `simp` rule sets: oriented rewrite rules compiled from proved lemmas, indexed for fast lookup, instantiated by matching.
- [mod solve](https://docs.logicaffeine.com/logicaffeine_proof/solve/): Structure-detecting solve front-end — the auto-dispatcher that puts our whole arsenal behind a single entry point.
- [mod sos](https://docs.logicaffeine.com/logicaffeine_proof/sos/): Sum-of-Squares / Positivstellensatz refutation over ℚ — kept EXACT (no SDP, no floating point) by the LP slice of the cone. True SoS is a semidefinite program over the reals; that would forfeit our certified guarantee. Instead we take the diagonal (fixed-square-basis) Positivstellensatz, which is an exact rational linear program: a CNF is lifted to degree-2 pseudo-Boolean inequalities and the lift is refuted by exact Fourier–Motzkin / Farkas elimination.
- [mod steenrod](https://docs.logicaffeine.com/logicaffeine_proof/steenrod/): The Steenrod algebra acting on `H*(BZ/2; Z/2) = Z/2[x]` — the deepest layer of cohomology operations, and a place where homotopy theory turns out to be number theory.
- [mod streams](https://docs.logicaffeine.com/logicaffeine_proof/streams/): Stream equivalence over units proven apart: two circuits that take a stream of tokens through a valid-ready handshake and give a stream back, each at its own width and its own pace, decided equal token for token under an arrival pattern.
- [mod sweep](https://docs.logicaffeine.com/logicaffeine_proof/sweep/): Combinational equivalence: two circuits’ outputs proven equal, or told apart by an input assignment that replays, every equality carried by a lemma whose LRAT proof a small checker re-validates.
- [mod sym_break](https://docs.logicaffeine.com/logicaffeine_proof/sym_break/): Complete lex-leader symmetry breaking, driven by the Schreier–Sims backend.
- [mod sym_certify](https://docs.logicaffeine.com/logicaffeine_proof/sym_certify/): Certified symmetry breaking — the centerpiece. Given a formula and a set of verified symmetry generators, add lex-leader symmetry-breaking predicates as PR steps (each self-checked, fail-closed), solve the augmented formula, and emit a single composed refutation that an independent checker accepts against the original formula alone.
- [mod sym_dynamic](https://docs.logicaffeine.com/logicaffeine_proof/sym_dynamic/): Dynamic symmetry breaking — Symmetric Explanation Learning (SEL), the in-search tier.
- [mod symmetry](https://docs.logicaffeine.com/logicaffeine_proof/symmetry/): Symmetry breaking for the general solver — the second pillar (with `crate::pigeonhole` cardinality reasoning) for winning on pigeonhole.
- [mod symmetry_detect](https://docs.logicaffeine.com/logicaffeine_proof/symmetry_detect/): General symmetry detection for CNF — the engine behind certified symmetry breaking.
- [mod tactic](https://docs.logicaffeine.com/logicaffeine_proof/tactic/): A tactic framework with a first-class goal state — the interactive proof interface (ROOT R5 of the Lean-competitive architecture).
- [mod tactic_cert](https://docs.logicaffeine.com/logicaffeine_proof/tactic_cert/): Certificate producers and independent checkers shared with the kernel rechecker.
- [mod tactic_script](https://docs.logicaffeine.com/logicaffeine_proof/tactic_script/): A tiny proof-script language over the `crate::tactic` combinators — proofs as TEXT, the way a Lean/Coq proof reads. This is the self-contained seam toward a full English vernacular: it has no dependency on the surface language, so it compiles a script string straight into a composed `Tactic`.
- [mod thermal_replay](https://docs.logicaffeine.com/logicaffeine_proof/thermal_replay/): Thermal-map replay — the independent judge of a claimed steady-state temperature map.
- [mod trace_determinism](https://docs.logicaffeine.com/logicaffeine_proof/trace_determinism/): The concurrency tie made literal: determinism = contractibility, on a real machine.
- [mod two_group](https://docs.logicaffeine.com/logicaffeine_proof/two_group/): The 2-group frontier — climbing past `K(G,1)` to genuine 2-types, honestly.
- [mod two_type](https://docs.logicaffeine.com/logicaffeine_proof/two_type/): A genuinely 2-truncated ∞-groupoid, had as an object: the minimal `K(A, 2)`.
- [mod twosat](https://docs.logicaffeine.com/logicaffeine_proof/twosat/): 2-SAT in linear time via the implication graph + strongly-connected components.
- [mod unify](https://docs.logicaffeine.com/logicaffeine_proof/unify/): First-order unification for proof search.
- [mod units](https://docs.logicaffeine.com/logicaffeine_proof/units/): Equivalence over units proven apart: two circuits built of units (adders, multipliers, any module already proven equal to its counterpart), each unit cut out of its circuit — its results free inputs, its operands outputs — and the two decided over the units as functions they know nothing of, a unit’s own proof standing for what it computes.
- [mod verify](https://docs.logicaffeine.com/logicaffeine_proof/verify/): Unified theorem verification — the single door.
- [mod xl](https://docs.logicaffeine.com/logicaffeine_proof/xl/): XL — algebraic cryptanalysis of multivariate quadratic (MQ) systems by linearization.
- [mod xor_drat](https://docs.logicaffeine.com/logicaffeine_proof/xor_drat/): The CNF→GF(2) bridge: compile a Gaussian (XOR linear-dependency) refutation into a strict DRAT proof that an external checker (`drat-trim`) accepts.
- [mod xor_engine](https://docs.logicaffeine.com/logicaffeine_proof/xor_engine/): DPLL(XOR) — the live GF(2) reasoning engine.
- [mod xorsat](https://docs.logicaffeine.com/logicaffeine_proof/xorsat/): XOR-SAT via Gaussian elimination over GF(2) — the parity analog of the pigeonhole/matching supercrush.

### [logicaffeine_kernel](https://docs.logicaffeine.com/logicaffeine_kernel/)
Calculus of Constructions proof kernel with inductive types, universes, quotients, a second checker and Lean 4 import

- Map: [llms/logicaffeine_kernel.txt](https://docs.logicaffeine.com/llms/logicaffeine_kernel.txt) — 68 modules, 580 items
- [mod bitvector](https://docs.logicaffeine.com/logicaffeine_kernel/bitvector/): Bitvector reflection-symmetry decision procedure.
- [mod cc](https://docs.logicaffeine.com/logicaffeine_kernel/cc/): Congruence Closure Tactic
- [mod certificate](https://docs.logicaffeine.com/logicaffeine_kernel/certificate/): Independently re-checkable proof certificates — the De Bruijn criterion.
- [mod dag](https://docs.logicaffeine.com/logicaffeine_kernel/dag/): The kernel core: a type theory over a hash-consed expression DAG, in two modes (`tc::Theory`): Lean 4’s theory exactly, and LOGOS’s Calculus of Inductive Constructions.
- [mod elaborate](https://docs.logicaffeine.com/logicaffeine_kernel/elaborate/): R4 — the elaborator: metavariables, unification, and implicit-argument inference.
- [mod equations](https://docs.logicaffeine.com/logicaffeine_kernel/equations/): Equation lemmas — Lean’s `f.eq_def`, `f.eq_1 … f.eq_n` — the NAME a proof cites when it appeals to a definition’s behaviour, which is what `rw [f]` / `simp [f]` / `unfold f` all need.
- [mod eval](https://docs.logicaffeine.com/logicaffeine_kernel/eval/): A call-by-value evaluator for the kernel’s computational fragment — the engine behind `native_decide`.
- [mod field_algebra](https://docs.logicaffeine.com/logicaffeine_kernel/field_algebra/): Kernel algebra for the prime field 𝔽_q of ML-KEM / ML-DSA — the certified arithmetic substrate (F2 seed).
- [mod inductive_compile](https://docs.logicaffeine.com/logicaffeine_kernel/inductive_compile/): Nested-inductive compiler (K3) — the UNTRUSTED front-end for inductives that recur nested inside a container, `RTree := rnode : TList RTree → RTree`.
- [mod int_inductive](https://docs.logicaffeine.com/logicaffeine_kernel/int_inductive/): `Int` as a real inductive — Lean’s `ofNat | negSucc` with its arithmetic defined rather than assumed (`Init/Data/Int/Basic.lean:40-45`, `:78-166`). The construction, packaged so the prelude adopts it in one call; the module header carries how Lean keeps it fast anyway. `Int` as a REAL INDUCTIVE — Lean’s `ofNat | negSucc`, with its arithmetic DEFINED.
- [mod interface](https://docs.logicaffeine.com/logicaffeine_kernel/interface/): Vernacular interface for the Kernel.
- [mod lia](https://docs.logicaffeine.com/logicaffeine_kernel/lia/): Linear Integer Arithmetic via Fourier-Motzkin Elimination
- [mod observational](https://docs.logicaffeine.com/logicaffeine_kernel/observational/): Certified universe-polymorphic quotient primitives. Observational equality: `Obs.{u} A a b : SProp`, an equality over every type that computes on the weak-head normal form of `A`, with `Obs_refl`, `Obs_transp` (its elimination, into `SProp` only) and `Obs_cast` (a value carried along an equality of types), after Pujet and Tabareau’s CC^obs.
- [mod omega](https://docs.logicaffeine.com/logicaffeine_kernel/omega/): Omega Test: True Integer Arithmetic Decision Procedure
- [mod positivity](https://docs.logicaffeine.com/logicaffeine_kernel/positivity/): Strict positivity checking for inductive types.
- [mod prelude](https://docs.logicaffeine.com/logicaffeine_kernel/prelude/): Standard Library for the Kernel.
- [mod quotient](https://docs.logicaffeine.com/logicaffeine_kernel/quotient/): Certified universe-polymorphic quotient primitives for kernel importers.
- [mod recheck](https://docs.logicaffeine.com/logicaffeine_kernel/recheck/): An independent proof-term re-checker (the de Bruijn criterion taken seriously).
- [mod recursor](https://docs.logicaffeine.com/logicaffeine_kernel/recursor/): R2 — auto-derived recursors (dependent eliminators) for inductive types.
- [mod reify](https://docs.logicaffeine.com/logicaffeine_kernel/reify/): Shared reification substrate for the arithmetic decision procedures.
- [mod ring](https://docs.logicaffeine.com/logicaffeine_kernel/ring/): Ring Tactic: Polynomial Equality by Normalization
- [mod simp](https://docs.logicaffeine.com/logicaffeine_kernel/simp/): Simplifier Tactic
- [mod tactic_cert](https://docs.logicaffeine.com/logicaffeine_kernel/tactic_cert/): Independent verification of reflected ring, linear-arithmetic, and congruence goals.
- [mod tactics](https://docs.logicaffeine.com/logicaffeine_kernel/tactics/): Tactics over the kernel’s own goals: a goal state of metavariables, outside the trusted base.
- [mod term_store](https://docs.logicaffeine.com/logicaffeine_kernel/term_store/): Hash-consed term storage — the representation a kernel needs to be as fast as Lean’s.
- [mod termination](https://docs.logicaffeine.com/logicaffeine_kernel/termination/): Termination checking for fixpoints.
- [mod word_ring](https://docs.logicaffeine.com/logicaffeine_kernel/word_ring/): Kernel ring proofs for the word ring ℤ/2ⁿ (`Word8`/`Word16`/`Word32`/`Word64`).

### [logicaffeine_verify](https://docs.logicaffeine.com/logicaffeine_verify/)
Z3-based static verification and model checking for Logicaffeine

- Map: [llms/logicaffeine_verify.txt](https://docs.logicaffeine.com/llms/logicaffeine_verify.txt) — 21 modules, 98 items
- [mod abstraction](https://docs.logicaffeine.com/logicaffeine_verify/abstraction/): Predicate Abstraction with CEGAR Refinement
- [mod automata](https://docs.logicaffeine.com/logicaffeine_verify/automata/): Automata for Reactive Synthesis
- [mod certificate](https://docs.logicaffeine.com/logicaffeine_verify/certificate/): Self-Certifying Proof Certificates
- [mod compositional](https://docs.logicaffeine.com/logicaffeine_verify/compositional/): Assume-Guarantee Compositional Reasoning
- [mod consistency](https://docs.logicaffeine.com/logicaffeine_verify/consistency/): Multi-Property Consistency Checking
- [mod equivalence](https://docs.logicaffeine.com/logicaffeine_verify/equivalence/): Semantic Equivalence Checking — The Core Contribution
- [mod error](https://docs.logicaffeine.com/logicaffeine_verify/error/): Verification error types with Socratic error messages.
- [mod ic3](https://docs.logicaffeine.com/logicaffeine_verify/ic3/): IC3/PDR (Property-Directed Reachability)
- [mod incremental](https://docs.logicaffeine.com/logicaffeine_verify/incremental/): Incremental Verification
- [mod interpolation](https://docs.logicaffeine.com/logicaffeine_verify/interpolation/): Interpolation-Based Model Checking
- [mod ir](https://docs.logicaffeine.com/logicaffeine_verify/ir/): Verification IR (Intermediate Representation)
- [mod kinduction](https://docs.logicaffeine.com/logicaffeine_verify/kinduction/): k-Induction for Unbounded Safety Verification
- [mod liveness](https://docs.logicaffeine.com/logicaffeine_verify/liveness/): Liveness-to-Safety Reduction
- [mod multiclock](https://docs.logicaffeine.com/logicaffeine_verify/multiclock/): Multi-Clock Domain Modeling
- [mod parameterized](https://docs.logicaffeine.com/logicaffeine_verify/parameterized/): Parameterized Verification
- [mod security](https://docs.logicaffeine.com/logicaffeine_verify/security/): Security Property Verification — Non-Interference
- [mod smtlib](https://docs.logicaffeine.com/logicaffeine_verify/smtlib/): SMT-LIB2 Export
- [mod solver](https://docs.logicaffeine.com/logicaffeine_verify/solver/): Z3 solver wrapper for Logicaffeine verification.
- [mod strategy](https://docs.logicaffeine.com/logicaffeine_verify/strategy/): Strategy Selection Engine
- [mod synthesis](https://docs.logicaffeine.com/logicaffeine_verify/synthesis/): Reactive Synthesis from LTL
- [mod type_infer](https://docs.logicaffeine.com/logicaffeine_verify/type_infer/): Constraint-based type inference for VerifyExpr.

### [logicaffeine_tv](https://docs.logicaffeine.com/logicaffeine_tv/)
Translation validation for LOGOS: a symbolic encoder of the source, checked with Z3 against the tree-walking interpreter per program

- Map: [llms/logicaffeine_tv.txt](https://docs.logicaffeine.com/llms/logicaffeine_tv.txt) — 5 modules, 15 items
- [mod equiv](https://docs.logicaffeine.com/logicaffeine_tv/equiv/): The SMT equivalence primitive, built on `logicaffeine_verify::check_equivalence`.
- [mod parse](https://docs.logicaffeine.com/logicaffeine_tv/parse/): Parse a LOGOS source string into the arena-allocated AST and hand it to a callback, mirroring the front-end of `compile::compile_program_full`.
- [mod symexec](https://docs.logicaffeine.com/logicaffeine_tv/symexec/): Big-step symbolic execution of the LOGOS Verifiable Core into `VerifyExpr`.
- [mod tensor](https://docs.logicaffeine.com/logicaffeine_tv/tensor/): A rewrite of the one IR, proven: the obligation `tensor_graph::smt` prints for two graphs, discharged by Z3.
- [mod verdict](https://docs.logicaffeine.com/logicaffeine_tv/verdict/): Result types for the translation validator.

### [logicaffeine_lexicon](https://docs.logicaffeine.com/logicaffeine_lexicon/)
The English vocabulary behind LOGOS: verb, noun and adjective metadata for build-time lookup tables, plus an optional runtime JSON index

- Map: [llms/logicaffeine_lexicon.txt](https://docs.logicaffeine.com/llms/logicaffeine_lexicon.txt) — 2 modules, 27 items
- [mod runtime](https://docs.logicaffeine.com/logicaffeine_lexicon/runtime/): Runtime JSON-based lexicon loading (requires `dynamic-lexicon` feature).
- [mod types](https://docs.logicaffeine.com/logicaffeine_lexicon/types/): Lexicon type definitions for grammatical and semantic categories. Lexicon type definitions

### [logicaffeine_base](https://docs.logicaffeine.com/logicaffeine_base/)
Foundation types for Logicaffeine: arenas, string interning, spans, and exact integers, decimals, quantities, money, dates and UUIDs

- Map: [llms/logicaffeine_base.txt](https://docs.logicaffeine.com/llms/logicaffeine_base.txt) — 46 modules, 654 items
- [mod algebraic](https://docs.logicaffeine.com/logicaffeine_base/algebraic/): Real algebraic numbers: exact roots of integer polynomials, with decidable equality and order.
- [mod arena](https://docs.logicaffeine.com/logicaffeine_base/arena/): Arena allocation for stable AST references.
- [mod closure](https://docs.logicaffeine.com/logicaffeine_base/closure/): The real closure of the values of several infinitesimals: `√(dt + dx)`, `∛(h + dt)`, every root the program’s arithmetic reaches among the values of more than one infinitesimal, held exactly.
- [mod complex_algebraic](https://docs.logicaffeine.com/logicaffeine_base/complex_algebraic/): Complex algebraic numbers `re + im·i` with real algebraic parts, and every complex root of a polynomial with rational coefficients.
- [mod describe](https://docs.logicaffeine.com/logicaffeine_base/describe/): Integer-sequence description-length codec (the MDL primitive)
- [mod dimension](https://docs.logicaffeine.com/logicaffeine_base/dimension/): Physical dimensions as an abelian group of rational exponent vectors.
- [mod elimination](https://docs.logicaffeine.com/logicaffeine_base/elimination/): Elimination: polynomials in several variables over the rationals, held sparse, and their resultants.
- [mod error](https://docs.logicaffeine.com/logicaffeine_base/error/): Error types with source location tracking.
- [mod exact_codec](https://docs.logicaffeine.com/logicaffeine_base/exact_codec/): Canonical byte encodings of the exact numbers — the one form they cross a task boundary, the wire and storage in.
- [mod exact_real](https://docs.logicaffeine.com/logicaffeine_base/exact_real/): Exact real numbers: every computable real, to any precision, with equality decided wherever a theorem decides it.
- [mod expansion](https://docs.logicaffeine.com/logicaffeine_base/expansion/): Expansions of the values of several infinitesimals in their smallest one.
- [mod extension](https://docs.logicaffeine.com/logicaffeine_base/extension/): The builtins of the exact extension, read and run once for every value model. A program calls them by name (`infinitesimal`, `standardPart`, `tripCount`, …), the declarations and the supertask engine’s resolved loops call them too, and the interpreter and a compiled program both answer through `call`, so a builtin computes the same value and refuses in the same words on every tier.
- [mod fec](https://docs.logicaffeine.com/logicaffeine_base/fec/): Reed-Solomon forward error correction — the erasure codec that lets a lossy transport reconstruct dropped packets without a retransmit round-trip.
- [mod germ](https://docs.logicaffeine.com/logicaffeine_base/germ/): Germs at `dt = 0`: the hyperreals a loop of infinitely many infinitesimal steps leaves, known by the series of their expansion in `dt` with exact computable-real coefficients.
- [mod gf256](https://docs.logicaffeine.com/logicaffeine_base/gf256/): GF(2^8) — the finite field with 256 elements, the shared substrate for erasure coding, multivariate cryptography (Oil-and-Vinegar / Rainbow), and the algebraic (XL) cryptanalysis engine.
- [mod hash](https://docs.logicaffeine.com/logicaffeine_base/hash/): Cryptographic hash primitives — MD5 (RFC 1321) and SHA-1 (RFC 3174), rolled in pure Rust.
- [mod hybrid](https://docs.logicaffeine.com/logicaffeine_base/hybrid/): Hybrid flows: loops of infinitesimal steps whose state flows between jumps — a bouncing ball, a thermostat — run exactly, as the ideal hybrid system their steps follow to within an infinitesimal.
- [mod hypernatural](https://docs.logicaffeine.com/logicaffeine_base/hypernatural/): Infinite integers generated by the program’s generator `H` (`dt = 1/H`) — the trip counts of supertasks.
- [mod hyperreal](https://docs.logicaffeine.com/logicaffeine_base/hyperreal/): Hyperreal numbers generated by the program’s infinitesimal `dt` — exact, ordered, decidable.
- [mod intern](https://docs.logicaffeine.com/logicaffeine_base/intern/): String interning for O(1) equality comparison.
- [mod limit_value](https://docs.logicaffeine.com/logicaffeine_base/limit_value/): Values at the end of a supertask: what depends on the infinite generator’s residue, the limit rules that turn such a value into one number, and the provisional answer of an unfinished search.
- [mod matrix_exp](https://docs.logicaffeine.com/logicaffeine_base/matrix_exp/): The exact matrix exponential `e^{t·M}` of a rational matrix.
- [mod money](https://docs.logicaffeine.com/logicaffeine_base/money/): Money — an exact monetary amount in a specific currency (UNIVERSAL_TYPES Part V).
- [mod multi](https://docs.logicaffeine.com/logicaffeine_base/multi/): Values of several ordered infinitesimals: `dt`, `dx` declared much smaller than `dt`, and so on.
- [mod nested](https://docs.logicaffeine.com/logicaffeine_base/nested/): Germs of several infinitesimals: a value of `dx`, declared much smaller than `dt`, known by its expansion in `dx` whose coefficients are values of `dt` and of the infinitesimals larger than it, not all of them exact — `exp(dt + dx) = Σ (e^dt/k!)·dx^k`, `ln(1 + dt + dx)`, the state a loop stepped by `dx` leaves when its rate is a value of `dt`.
- [mod nested_flow](https://docs.logicaffeine.com/logicaffeine_base/nested_flow/): Flows across infinitesimals: the state a loop stepped by one infinitesimal leaves when its affine update holds values of others.
- [mod number](https://docs.logicaffeine.com/logicaffeine_base/number/): A number of the exact tower as base holds one itself: the coefficient of an expansion of a value of several infinitesimals whose coefficients are not all exact — `exp(dt + dx)`, whose coefficients in `dx` are the germ of `e^dt` — and the value the flows of such expansions start from.
- [mod numeric](https://docs.logicaffeine.com/logicaffeine_base/numeric/): The numeric tower’s foundation: a hand-rolled arbitrary-precision integer.
- [mod ode](https://docs.logicaffeine.com/logicaffeine_base/ode/): Validated integration of a polynomial differential equation `x' = f(x)`.
- [mod ordered_field](https://docs.logicaffeine.com/logicaffeine_base/ordered_field/): Polynomials over an ordered field with exact arithmetic, the coefficient rings of the hyperreals.
- [mod ordinal](https://docs.logicaffeine.com/logicaffeine_base/ordinal/): Ordinals below ε₀ in Cantor normal form — the stage counter of transfinite execution.
- [mod poly](https://docs.logicaffeine.com/logicaffeine_base/poly/): Exact univariate polynomials over ℚ — the algebra under the real algebraic numbers.
- [mod puiseux](https://docs.logicaffeine.com/logicaffeine_base/puiseux/): The real closure of the hyperreals: real algebraic Puiseux series in `dt`, exactly.
- [mod quantity](https://docs.logicaffeine.com/logicaffeine_base/quantity/): Quantities: an exact magnitude carrying a physical `Dimension` and a unit.
- [mod sha_ops](https://docs.logicaffeine.com/logicaffeine_base/sha_ops/): The four Intel SHA-1 (SHA-NI) operations, in SOFTWARE — the exact bit-for-bit semantics of `sha1rnds4` / `sha1msg1` / `sha1msg2` / `sha1nexte`. These are the spec the tree-walker runs so that SHA-1 written in LOGOS over these ops produces the identical result whether it is interpreted (software here) or AOT-compiled to the real hardware instruction (`core::arch::x86_64`). Same idea as the scalar-lane spec behind `Lanes8Word32` → AVX2.
- [mod si](https://docs.logicaffeine.com/logicaffeine_base/si/): SI-dimensioned f64 newtypes — the characterized-descriptor surface types.
- [mod span](https://docs.logicaffeine.com/logicaffeine_base/span/): Source location tracking for error reporting.
- [mod supertask](https://docs.logicaffeine.com/logicaffeine_base/supertask/): The run-time half of the supertask engine: the exact operations the statements it writes call, generic over a value model (`ValueAlgebra`) so the interpreter and a compiled program run one implementation.
- [mod temporal](https://docs.logicaffeine.com/logicaffeine_base/temporal/): Exact calendar primitives — the bedrock of the time tower.
- [mod tower](https://docs.logicaffeine.com/logicaffeine_base/tower/): The exact real types in a program’s value model: real algebraic numbers, computable reals, the program’s infinitesimal and the hyperreals it generates, infinite integers, ordinals, and the values a supertask leaves.
- [mod union_find](https://docs.logicaffeine.com/logicaffeine_base/union_find/): Union-Find (disjoint set) with path compression and union by rank.
- [mod uuid](https://docs.logicaffeine.com/logicaffeine_base/uuid/): UUID — a 128-bit universally-unique identifier (RFC 9562, superseding RFC 4122).
- [mod word](https://docs.logicaffeine.com/logicaffeine_base/word/): Fixed-width wrapping integers — the ring ℤ/2ᵏℤ.

### [logicaffeine_data](https://docs.logicaffeine.com/logicaffeine_data/)
LOGOS runtime values, collections, wire format and CRDTs, shared by native and WASM builds

- Map: [llms/logicaffeine_data.txt](https://docs.logicaffeine.com/llms/logicaffeine_data.txt) — 13 modules, 191 items
- [mod backpressure](https://docs.logicaffeine.com/logicaffeine_data/backpressure/): `BoundedRing<T>` — a fixed-capacity queue that drops the OLDEST item on overflow.
- [mod crdt](https://docs.logicaffeine.com/logicaffeine_data/crdt/): CRDT (Conflict-free Replicated Data Types)
- [mod exact](https://docs.logicaffeine.com/logicaffeine_data/exact/): The value a compiled LOGOS program holds wherever the exact extension reaches: real algebraic numbers, computable reals, the infinitesimal and the hyperreals it generates, infinite integers, ordinals, residue-dependent and provisional values — and every standard value that meets them.
- [mod failure](https://docs.logicaffeine.com/logicaffeine_data/failure/): The sentences a program stops with, written once for every tier.
- [mod fmt](https://docs.logicaffeine.com/logicaffeine_data/fmt/): The ONE float-display path.
- [mod indexing](https://docs.logicaffeine.com/logicaffeine_data/indexing/): Polymorphic indexing traits for Logos collections.
- [mod ops](https://docs.logicaffeine.com/logicaffeine_data/ops/): Exact numeric comparison for GENERATED code.
- [mod opt](https://docs.logicaffeine.com/logicaffeine_data/opt/): A value or `nothing`: what a compiled program keeps in a place the VM can store `nothing` in.
- [mod temporal](https://docs.logicaffeine.com/logicaffeine_data/temporal/): The temporal values of a compiled program: a calendar date, an instant, a time of day and a calendar span, with the arithmetic and the printing every tier shares (base’s `temporal`), and each as an `OtherValue` a `LogosValue` holds, so the exact extension’s values meet them as the interpreter’s do. Reading the clock is the system’s (`logicaffeine_system::temporal::now`).
- [mod types](https://docs.logicaffeine.com/logicaffeine_data/types/): Core runtime type definitions.
- [mod wire](https://docs.logicaffeine.com/logicaffeine_data/wire/): Shared wire-codec core — the exact byte format of the peer/transport codec (`logicaffeine_compile::concurrency::marshal`), factored out so that TWO value models encode and decode through ONE definition:

### [logicaffeine_system](https://docs.logicaffeine.com/logicaffeine_system/)
Platform IO, networking, HTTP serving, persistence, and post-quantum crypto (Keccak/SHA-3, ChaCha20-Poly1305, ML-KEM, ML-DSA) for LOGOS

- Map: [llms/logicaffeine_system.txt](https://docs.logicaffeine.com/llms/logicaffeine_system.txt) — 31 modules, 331 items
- [mod addr](https://docs.logicaffeine.com/logicaffeine_system/addr/): Address normalization — libp2p multiaddr → WebSocket URL.
- [mod aead](https://docs.logicaffeine.com/logicaffeine_system/aead/): ChaCha20-Poly1305 AEAD (RFC 8439) — the symmetric seal that closes the post-quantum channel: an ML-KEM-768 handshake establishes the shared secret, HKDF derives this 32-byte key, and every wire message is sealed here. ChaCha20 is a pure `Word32` ARX cipher (the same primitive the `assets/std/crypto.lg` `chacha20Block` ships in Logos); Poly1305 is the one-time authenticator in constant-time 5×26-bit limbs (no bignum). Verified against the RFC 8439 §2.4.2 / §2.5.2 / §2.8.2 known-answer vectors. The tag compare is constant-time.
- [mod csrf](https://docs.logicaffeine.com/logicaffeine_system/csrf/): The page half of CSRF: a page document carries its visitor’s token in its head, where the browser host reads it and sends it back as `x-csrf-token` on the page’s state-changing requests to its own server. One definition for every tier that composes or reads a page — the dev server, a compiled server, the in-process host and the browser runtime’s shared name.
- [mod env](https://docs.logicaffeine.com/logicaffeine_system/env/): Environment Variable and Argument Access
- [mod failure](https://docs.logicaffeine.com/logicaffeine_system/failure/): Where a failure ends: the program, or the boundary that catches it.
- [mod file](https://docs.logicaffeine.com/logicaffeine_system/file/): Simple File I/O Operations
- [mod fmt](https://docs.logicaffeine.com/logicaffeine_system/fmt/): Formatting utilities
- [mod fs](https://docs.logicaffeine.com/logicaffeine_system/fs/): Virtual File System Abstraction
- [mod http](https://docs.logicaffeine.com/logicaffeine_system/http/): A native HTTP/1.1 server — the runtime a LOGOS program’s `Serve` statement executes on.
- [mod io](https://docs.logicaffeine.com/logicaffeine_system/io/): I/O Operations for LOGOS Programs
- [mod keccak](https://docs.logicaffeine.com/logicaffeine_system/keccak/): Keccak-f[1600] + SHA-3 / SHAKE runtime kernels — the symmetric/hash layer ML-KEM is built on (SHA3-256/512 for hashing, SHAKE128 for matrix expansion, SHAKE256 for the PRF). Reached from compiled LOGOS via the `sha3_256` / `sha3_512` / `shake128` / `shake256` stdlib functions. Verified against the NIST FIPS-202 KATs (see the tests). Input/output are LOGOS `Int` bytes (0..255) carried in a `Seq of Int`.
- [mod mldsa](https://docs.logicaffeine.com/logicaffeine_system/mldsa/): ML-DSA-65 (FIPS-204 / Dilithium) runtime kernels — the post-quantum SIGNATURE scheme that complements ML-KEM-768 in the channel. This module builds bottom-up: the length-256 NTT over the Dilithium prime `q = 8380417` (a COMPLETE transform, unlike Kyber’s incomplete one — `q ≡ 1 (mod 512)`, so `X²⁵⁶+1` splits fully), with signed Montgomery reduction. Validated against the schoolbook negacyclic convolution.
- [mod mlkem](https://docs.logicaffeine.com/logicaffeine_system/mlkem/): ML-KEM-768 (FIPS-203) keygen / encapsulation / decapsulation as a Rust composition of the verified native kernels in `crate::ntt` (NTT, base-multiply, CBD, compress, byte-encode, 4-way AVX2 matrix expansion) and `crate::keccak` (SHA3-256/512, SHAKE256). This is the exact same primitive set the `assets/std/crypto.lg` Logos ML-KEM orchestrates and that the `logicaffeine-tests` AOT gates prove bit-exact vs the FIPS-203 reference — here orchestrated in Rust so the post-quantum channel (`logicaffeine_compile::concurrency::channel`) can run the handshake. Coefficients ride the fast `Word16` carrier throughout.
- [mod net](https://docs.logicaffeine.com/logicaffeine_system/net/): `Net` — the cross-target relay-backed network handle the interpreter holds.
- [mod ntt](https://docs.logicaffeine.com/logicaffeine_system/ntt/): ML-KEM (Kyber) negacyclic NTT runtime kernel — the verified scalar reference + AVX2 i16×16 path that compiled LOGOS reaches through the `mlkemNtt` stdlib function. Ported from the validated `scripts/dev/ntt_simd_proto.rs` (round-trip + AVX2==scalar bit-identical). q = 3329, R = 2¹⁶, the incomplete 7-level transform over ℤ_q[X]/(X²⁵⁶+1). The Montgomery reduction it uses is kernel-certified (`logicaffeine_kernel::field_algebra::montgomery_reduction_*`).
- [mod obs](https://docs.logicaffeine.com/logicaffeine_system/obs/): The observation channel for COMPILED (AOT-Rust) programs — Wave 13.
- [mod random](https://docs.logicaffeine.com/logicaffeine_system/random/): Random Number Generation
- [mod relay](https://docs.logicaffeine.com/logicaffeine_system/relay/): Thin WebSocket relay — the v1 browser↔mesh bridge.
- [mod relay_proto](https://docs.logicaffeine.com/logicaffeine_system/relay_proto/): The relay wire protocol — shared verbatim by the native server/client (`super::relay`) and the browser client (`super::relay_browser`). Both targets serialize the SAME `RelayFrame` with `bincode`, so a browser tab and a native node speak an identical language across the WebSocket.
- [mod stack](https://docs.logicaffeine.com/logicaffeine_system/stack/): The stack a compiled program’s `Main` runs on.
- [mod storage](https://docs.logicaffeine.com/logicaffeine_system/storage/): Persistent Storage with Journaling
- [mod tcp](https://docs.logicaffeine.com/logicaffeine_system/tcp/): TCP client natives (tcp.lg): the SYNC implementations the AOT tier calls via `map_native_function`, plus the shared error-message formatters every tier reuses — one wording, so the tiers cannot drift even in their `Err` text.
- [mod temporal](https://docs.logicaffeine.com/logicaffeine_system/temporal/): Temporal types for Logicaffeine. The date, moment, time-of-day and calendar span values are `logicaffeine-data`’s (`logicaffeine_data::temporal`), where every value model reaches them, re-exported here beside what only a system has: the clock, and how `Show` prints them.
- [mod testworld](https://docs.logicaffeine.com/logicaffeine_system/testworld/): The sealed test world.
- [mod text](https://docs.logicaffeine.com/logicaffeine_system/text/)
- [mod time](https://docs.logicaffeine.com/logicaffeine_system/time/): Time Utilities
- [mod word_rt](https://docs.logicaffeine.com/logicaffeine_system/word_rt/): Runtime support for the `Word8`/`Word16`/`Word32`/`Word64` ring types in COMPILED LOGOS.

### [logicaffeine_runtime](https://docs.logicaffeine.com/logicaffeine_runtime/)
Deterministic, replayable concurrency runtime for the LOGOS interpreter and VM: task scheduler, channels, Select, timers, seed and trace

- Map: [llms/logicaffeine_runtime.txt](https://docs.logicaffeine.com/llms/logicaffeine_runtime.txt) — 7 modules, 30 items
- [mod channel](https://docs.logicaffeine.com/logicaffeine_runtime/channel/): Channels — FIFO, bounded, move-semantics pipes (the language’s `Pipe`).
- [mod config](https://docs.logicaffeine.com/logicaffeine_runtime/config/): Scheduler configuration — annotatable knobs with a nice default.
- [mod executor](https://docs.logicaffeine.com/logicaffeine_runtime/executor/): The work-stealing M:N native driver.
- [mod payload](https://docs.logicaffeine.com/logicaffeine_runtime/payload/): `RtPayload` — the `Send`-able value subset that crosses task (and OS-thread) boundaries via channels.
- [mod scheduler](https://docs.logicaffeine.com/logicaffeine_runtime/scheduler/): The scheduler core + cooperative driver.
- [mod seed](https://docs.logicaffeine.com/logicaffeine_runtime/seed/): Seed, deterministic RNG, and the choice trace — the determinism contract.
- [mod task](https://docs.logicaffeine.com/logicaffeine_runtime/task/): Tasks — the unit the scheduler multiplexes.

### [logicaffeine_forge](https://docs.logicaffeine.com/logicaffeine_forge/)
The machine-code layer of the LOGOS copy-and-patch JIT: W^X executable memory, build-time stencils, a register-allocating x86-64 backend

- Map: [llms/logicaffeine_forge.txt](https://docs.logicaffeine.com/llms/logicaffeine_forge.txt) — 7 modules, 4348 items
- [mod buffer](https://docs.logicaffeine.com/logicaffeine_forge/buffer/): The copy-and-patch assembler: glue stencils into executable code.
- [mod jit](https://docs.logicaffeine.com/logicaffeine_forge/jit/): J1: the straight-line micro-op compiler — bytecode in, native code out.
- [mod patch](https://docs.logicaffeine.com/logicaffeine_forge/patch/): Relocation patchers — pure byte math, compiled (and unit-tested) on EVERY host so the x86-64 patchers are exercised on an arm64 dev machine and vice versa. Each function rewrites one relocation site in a staging buffer given the site’s final runtime address and its target’s address.
- [mod regalloc](https://docs.logicaffeine.com/logicaffeine_forge/regalloc/): Contiguous register-allocated region codegen for EXODIA, the copy-and-patch JIT.
- [mod segv_trace](https://docs.logicaffeine.com/logicaffeine_forge/segv_trace/): Diagnostic SIGSEGV/SIGBUS tracer for root-causing faults inside JIT’d code.
- [mod vectorize](https://docs.logicaffeine.com/logicaffeine_forge/vectorize/): Element-wise map vectorization — the general, sound SIMD lever.
- [mod x64asm](https://docs.logicaffeine.com/logicaffeine_forge/x64asm/): A minimal x86-64 instruction encoder for the contiguous register-allocated region backend (`compile_region_regalloc`).

### [logicaffeine_jit](https://docs.logicaffeine.com/logicaffeine_jit/)
Native execution tier for the LOGOS bytecode VM: hot functions and loops tier up to x86-64 machine code

- Map: [llms/logicaffeine_jit.txt](https://docs.logicaffeine.com/llms/logicaffeine_jit.txt) — 1 modules, 41 items
- [mod image](https://docs.logicaffeine.com/logicaffeine_jit/image/): Build and execute self-contained optimized bytecode images. Precompiled bytecode images for the native JIT.

### [logicaffeine_lsp](https://docs.logicaffeine.com/logicaffeine_lsp/)
The LOGOS language server (LSP): diagnostics, completion, hover, navigation and refactoring for .lg files, literate .md files and LGX pages

- Map: [llms/logicaffeine_lsp.txt](https://docs.logicaffeine.com/llms/logicaffeine_lsp.txt) — 29 modules, 123 items
- [mod call_hierarchy](https://docs.logicaffeine.com/logicaffeine_lsp/call_hierarchy/): Call hierarchy over the `SymbolIndex`’s call sites: who calls this function, and what does it call. `## Main` callers have no hierarchy item (Main is the program, not a function) — their calls simply don’t appear as incoming edges.
- [mod code_actions](https://docs.logicaffeine.com/logicaffeine_lsp/code_actions/)
- [mod code_lens](https://docs.logicaffeine.com/logicaffeine_lsp/code_lens/)
- [mod completion](https://docs.logicaffeine.com/logicaffeine_lsp/completion/)
- [mod definition](https://docs.logicaffeine.com/logicaffeine_lsp/definition/)
- [mod diagnostics](https://docs.logicaffeine.com/logicaffeine_lsp/diagnostics/)
- [mod document](https://docs.logicaffeine.com/logicaffeine_lsp/document/)
- [mod document_highlights](https://docs.logicaffeine.com/logicaffeine_lsp/document_highlights/): Document highlights: every occurrence of the symbol under the cursor, with WRITE kind on binding and mutation sites and READ everywhere else — the cursor-hold highlight editors render natively.
- [mod document_symbols](https://docs.logicaffeine.com/logicaffeine_lsp/document_symbols/)
- [mod flycheck](https://docs.logicaffeine.com/logicaffeine_lsp/flycheck/): The rustc flycheck: on save, compile the document through the AOT backend’s mapped codegen and run `cargo check` over it, translating every finding back to English with real user-source spans — the borrow checker, speaking LOGOS.
- [mod folding](https://docs.logicaffeine.com/logicaffeine_lsp/folding/)
- [mod formatting](https://docs.logicaffeine.com/logicaffeine_lsp/formatting/)
- [mod hover](https://docs.logicaffeine.com/logicaffeine_lsp/hover/)
- [mod index](https://docs.logicaffeine.com/logicaffeine_lsp/index/)
- [mod inlay_hints](https://docs.logicaffeine.com/logicaffeine_lsp/inlay_hints/)
- [mod line_index](https://docs.logicaffeine.com/logicaffeine_lsp/line_index/)
- [mod pipeline](https://docs.logicaffeine.com/logicaffeine_lsp/pipeline/)
- [mod references](https://docs.logicaffeine.com/logicaffeine_lsp/references/)
- [mod rename](https://docs.logicaffeine.com/logicaffeine_lsp/rename/)
- [mod scheduler](https://docs.logicaffeine.com/logicaffeine_lsp/scheduler/)
- [mod selection_ranges](https://docs.logicaffeine.com/logicaffeine_lsp/selection_ranges/): Selection ranges: expand-selection follows English structure — word → sentence → block → document.
- [mod semantic_tokens](https://docs.logicaffeine.com/logicaffeine_lsp/semantic_tokens/)
- [mod server](https://docs.logicaffeine.com/logicaffeine_lsp/server/)
- [mod signature_help](https://docs.logicaffeine.com/logicaffeine_lsp/signature_help/)
- [mod state](https://docs.logicaffeine.com/logicaffeine_lsp/state/)
- [mod stdlib_docs](https://docs.logicaffeine.com/logicaffeine_lsp/stdlib_docs/): The stdlib teaching registry: every prelude definition’s literate documentation, read once from the RAW embedded module sources (`loader::prelude_module_sources` — Notes included) through `teach::extract_literate_docs`. Hover, completion, and signature help fall back here when a name has no local definition, so `md5` teaches in the editor exactly what its `## Note` says in the source.
- [mod teach_md](https://docs.logicaffeine.com/logicaffeine_lsp/teach_md/): Markdown rendering for the shared teaching brain (`logicaffeine_language::teach`) — the LSP’s presentation of a lesson.
- [mod template](https://docs.logicaffeine.com/logicaffeine_lsp/template/): The LGX template vocabulary the editor completes and paints with.
- [mod workspace](https://docs.logicaffeine.com/logicaffeine_lsp/workspace/): Workspace-wide symbol index: every `.lg`/`.md` file under the workspace folders, analyzed in the background, so symbols resolve across files the user never opened.

### [logicaffeine_cli](https://docs.logicaffeine.com/logicaffeine_cli/)
largo — the LOGOS build tool: projects, builds, tests, serving, proofs, and the package registry

- Map: [llms/logicaffeine_cli.txt](https://docs.logicaffeine.com/llms/logicaffeine_cli.txt) — 48 modules, 651 items
- [mod analysis](https://docs.logicaffeine.com/logicaffeine_cli/analysis/): Re-export of analysis utilities from the compile crate.
- [mod browser](https://docs.logicaffeine.com/logicaffeine_cli/browser/): A real browser as a page tier: headless Chrome, driven over the DevTools protocol.
- [mod cli](https://docs.logicaffeine.com/logicaffeine_cli/cli/): LOGOS CLI (largo) — argument parsing and dispatch.
- [mod compile](https://docs.logicaffeine.com/logicaffeine_cli/compile/): LOGOS Compilation Pipeline for CLI
- [mod dap](https://docs.logicaffeine.com/logicaffeine_cli/dap/): `largo dap` — the LOGOS debugger served over the Debug Adapter Protocol.
- [mod interface](https://docs.logicaffeine.com/logicaffeine_cli/interface/): Re-export of the LOGOS interface types from the kernel crate.
- [mod mcp](https://docs.logicaffeine.com/logicaffeine_cli/mcp/): `largo mcp` — the LOGOS toolchain served over the Model Context Protocol.
- [mod project](https://docs.logicaffeine.com/logicaffeine_cli/project/): Phase 36/37/39: Project Module System
- [mod ui](https://docs.logicaffeine.com/logicaffeine_cli/ui/): Terminal output substrate for `largo`.

### [logicaffeine_web](https://docs.logicaffeine.com/logicaffeine_web/)
The logicaffeine.com site (Dioxus/WASM): LOGOS Studio with live LGX previews, Learn, Syntax Guide, benchmarks, news and the registry browser

- Map: [llms/logicaffeine_web.txt](https://docs.logicaffeine.com/llms/logicaffeine_web.txt) — 112 modules, 579 items
- [mod composer](https://docs.logicaffeine.com/logicaffeine_web/composer/): Composing a formula by hand: the symbol buttons beside a typed answer, and where a click puts its symbol.
- [mod content](https://docs.logicaffeine.com/logicaffeine_web/content/)
- [mod generator](https://docs.logicaffeine.com/logicaffeine_web/generator/): Exercise generation from templates.
- [mod grader](https://docs.logicaffeine.com/logicaffeine_web/grader/)
- [mod guide_review](https://docs.logicaffeine.com/logicaffeine_web/guide_review/): The Syntax Guide’s SM-2 deck: recap self-marks and graded exercise results feed the same spaced-repetition engine as Learn, under a `guide/` key namespace so the two decks coexist in one `UserProgress` without collision. Due guide cards surface on the Review page beside Learn cards.
- [mod learn_state](https://docs.logicaffeine.com/logicaffeine_web/learn_state/): Learn page state: where the learner stands on the roadmap, the question that closes a lesson, and the optional practice behind it.
- [mod progress](https://docs.logicaffeine.com/logicaffeine_web/progress/): What a learner has done, kept in the browser’s local storage under `logos_user_progress`.
- [mod sitemap](https://docs.logicaffeine.com/logicaffeine_web/sitemap/): Sitemap + prerender route enumeration for SEO.
- [mod srs](https://docs.logicaffeine.com/logicaffeine_web/srs/)
- [mod storage](https://docs.logicaffeine.com/logicaffeine_web/storage/): LocalStorage persistence layer for user progress.
- [mod struggle](https://docs.logicaffeine.com/logicaffeine_web/struggle/): Struggle Detection Logic
- [mod ui](https://docs.logicaffeine.com/logicaffeine_web/ui/)