# Theory

Theory Core IR is an Elixir-oriented meta-compiler for deriving computation code
from formal evidence.

The project direction is not to prove the whole Rust language. A complete proof
of Rust would require redoing the ownership model, unsafe aliasing/provenance
rules, compiler semantics, LLVM memory semantics, trait solving, and large parts
of the existing formal Rust ecosystem. That is not the short bridge.

The short bridge is narrower: define a small certified Core IR, prove its local
judgments with Theoria, and lower checked programs into Rust, C, or LLVM IR under
explicit backend boundaries.

## Installation

After publication, add `theory` to your dependencies:

```elixir
def deps do
  [
    {:theory, "~> 0.1.0"}
  ]
end
```

## Theoria

Theoria: <https://github.com/elixir-vibe/theoria>

Theory uses Theoria as the proof kernel for Core IR obligations. Theoria should
not be treated as a Lean replacement for large mathematical libraries. Its role
here is to check compact certificates generated by Elixir tooling.

A near-term prerequisite is a minimal Prelude for the proof surface:

- `Option`
- `Prod`
- `Exists`

Until those are available, existential statements can be represented as explicit
certificate records.

## Core Claim

Theoria proves a small and hard Core IR. Elixir generates that IR and the
corresponding proof obligations. Backends then lower the certified IR into
computation targets.

```text
Elixir DSL / macros
  -> Core IR
  -> Theoria obligations
  -> checked certificates
  -> Rust / C / LLVM IR
```

This frames Rust, C, and LLVM IR as lowering targets rather than the primary
objects of proof.

## Certified Core

The Core IR should stay small enough to audit and strong enough to express real
systems code. The initial surface should include:

- typed SSA / ANF
- total functions
- algebraic data
- ownership tokens / affine capabilities
- region and lifetime judgments
- effect rows: `alloc`, `read`, `write`, `free`, `call`
- explicit no-UB obligations

## Proof Surface

Theoria should check judgments over Core IR programs, including:

- `well_typed`
- `borrow_graph_valid`
- `initialized_before_read`
- `no_use_after_free`
- `bounds_safe`
- `no_alias_for_mut`
- `effect_allowed`
- `lowering_preserves_semantics`

These judgments are scoped to the Core IR. They do not imply that arbitrary Rust,
C, or LLVM IR programs are verified.

## Backend Strategy

### Stage 1: Safe Rust

Generate safe Rust first. This lets `rustc` continue to enforce borrow checking,
MIR validation, and ordinary code generation. Theoria proves that the Elixir
source IR satisfies its own resource, bounds, and protocol obligations before
lowering.

This stage is suitable for IDR systems, state machines, protocols, codecs,
CRDTs, schedulers, and other bounded systems code.

### Stage 2: Unsafe Rust With A Tiny Runtime

Unsafe Rust should be introduced only behind a small trusted runtime surface.
Each unsafe primitive must have an explicit contract and a corresponding proof
or audit boundary.

### Stage 3: C / LLVM IR

C and LLVM IR require stronger backend discipline. LLVM in particular exposes
`undef`, `poison`, provenance, alignment, lifetime, and UB-sensitive behavior.

The conservative path is translation validation: each generated artifact should
produce backend-specific obligations, instead of assuming the lowering pass is
correct by construction.

## Boundary

Theory should prove its own computation manifold: the Core IR, its certificates,
and the preservation properties of selected lowering paths.

It should not claim to prove all of Rust, all of C, or all of LLVM. Those
languages remain projection targets. The certified object is the Core IR and the
checked path from Elixir into those targets.