muro

<a href="https://muro-lang.dev"><img src="assets/muro-logo.png" alt="Muro" width="180" align="left" hspace="28"></a>

<h3>Prove real programs correct.<br>Then run them.</h3>

<br><br><br>

<a href="https://hex.pm/packages/muro"><img src="https://img.shields.io/hexpm/v/muro?style=flat-square&label=hex&labelColor=111111&color=e8e8e8" alt="Hex version"></a>

<br clear="left">

An explicit affine dependent type theory. Elixir parses, checks, and emits `.muro`. Only run terms become running code. Users do not need Agda.

Muro is built for agents to write. The agent carries the load of formal verification: every type, motive and proof step is written out and nothing is inferred, so `mix muro.check` either accepts what it wrote or names each definition that fails. Proofs are checked, then erased. Only `run` terms are emitted: as Elixir for the BEAM, as C with `mix muro.emit --backend c`, as Rust with `mix muro.emit --backend rust`, or as Cortex-M assembly with `mix muro.emit --backend asm`, from the same source. The checker's soundness is proved in Agda for a fragment of the calculus (see [Limits](manual/limits.md)); it is not a proof about every program.

The language book is [`manual/`](manual/index.md). That is what [muro-lang.dev](https://muro-lang.dev) will render. It is not ExDoc. Elixir API docs, when added, stay on `@moduledoc` / `mix docs`. Agda in `agda/Muro/` is a third layer: the rules of the calculus, not a certificate that a `.muro` file is correct.

## Install

[muro on Hex](https://hex.pm/packages/muro) is published by the [murolang](https://hex.pm/users/murolang) organization. Current release: 0.16.37. Releases are listed in [CHANGELOG.md](CHANGELOG.md).

```elixir
def deps do
  [
    {:muro, "~> 0.16.37"}
  ]
end
```

A clone is for changing the kernel. A `.muro` file is checked with `mix muro.check` from a project that depends on the package.

---

## One-shot (humans and agents)

Two jobs. Do not mix them.

| You want to… | Do this |
| --- | --- |
| Add a Muro program | Write a `.muro` file against [`manual/grammar.md`](manual/grammar.md). Check with `mix muro.check path.muro`. Do not change Agda or the Elixir kernel. |
| Change the type theory | Follow [`manual/extending.md`](manual/extending.md). Agda first, then the matching Elixir clause. Users still only run Mix. |

Agents: read [`manual/for-agents.md`](manual/for-agents.md). Copy syntax from `examples/`, not from memory.

Skeleton:

```
-- comments start with --
def plus : run Π (n : Nat) → Π (m : Nat) → Nat :=
  λ (n : Nat) → λ (m : Nat) →
    match n motive (λ _ → Nat)
      | 0 => m
      | suc np => suc(plus np m)
```

```
mix muro.check examples/your_file.muro
```

A definition is in the book the moment `Parser.parse/1` returns it. The checker sees the whole book (forward references are allowed). Emit keeps only `run`.

---

## Manual

| Page | For |
| --- | --- |
| [Start](manual/start.md) | Install, first file, emit |
| [The wall](manual/wall.md) | spec / evidence / run |
| [Terms](manual/language.md) | Π, λ, match, quantities |
| [Grammar](manual/grammar.md) | What the parser implements |
| [Examples](manual/examples.md) | Every file in `examples/` |
| [CSHRL](manual/cshrl.md) | A library on params, three environments, their agents |
| [For agents](manual/for-agents.md) | Operational contract |
| [Limits](manual/limits.md) | What the language does not do |

Index: [`manual/index.md`](manual/index.md). Machine-readable list: [`manual/manifest.yml`](manual/manifest.yml).

---

## Build

```
mise install
mix deps.get
mix test
mix muro.check
mix muro.check examples/half_ok.muro
```

Agda 2.8+ and standard library 2.3 (optional unless you change the kernel):

```
git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git vendor/agda-stdlib
make agda
```

`Muro.Lexer.tokenize/1` is the highlighter. It walks a fragment with the parser's lexical rules and returns `{kind, start, stop}` byte spans. A snippet that `Parser.parse/1` rejects still yields spans, and joining the slices gives the source back. `Muro.MakeupLexer` maps those spans onto Makeup tags (language `"muro"`, extension `.muro`) and is registered when the application starts. HTML and colors stay with the caller.

`Muro.Check.check_sig/2` returns `:ok` on the book, or every definition error in book order. Each definition is checked on its own process against the whole book; the per-definition answer is the one `checkSig-sound` is about. CI runs the Elixir job and `make agda` on every push and pull request. `make agda` checks the theorem modules (`Muro.Judgement`, `Muro.Typing`, `Muro.Wall`, `Muro.Consistency`, `Muro.Frag`, `Muro.Tag`, `Muro.Check`, `Muro.Soundness`) under `--safe`: no postulates, no `TERMINATING`. Conversion in ⊢ is a congruent relation generated by a confluent parallel reduction, `Muro.Typing` proves substitution and preservation for the fragment, `Muro.Consistency` proves that no closed normal evidence term has type Empty, and `Empty-evid` itself waits on normalisation of closed evidence. `Muro.Soundness` proves that the executable checker is sound for ⊢ on the fragment: when `Muro.Check` accepts a definition over a signature whose constructor types are telescopes into their data type (`GoodSig`), ⊢ derives it with the same uses when the subject is that term and every premise meets its rule (one direction only, for every fuel). A declared-family unfold is a derivation of the instantiated pair. The checker is structurally recursive on the term; fuel bounds only reduction, and running out is reported as `out of fuel` (`mix muro.check --fuel N`), never as a verdict. The fragment is Π, λ, application, Nat, Unit, Empty, identity, `rewrite`, `def`, annotation, pairs, `data` (constructor applications and `match`, on indexed data types too: a branch is typed at its constructor's own indices; a constructor whose numeral index clashes with the scrutinee's is skipped), and ν (Stream, `Always`, `~`, and declared families). A stream unfold is a derivation of the λ; a declared-family unfold is a derivation of the pair instantiated at the seed, and `uncons` of that pair reads it. Productivity is the guard the checker enforces and ⊢ records without rechecking. Tensor and Atom remain outside ⊢. `Type` is one impredicative sort; kinds (`Π (x : A) → Type`) are well-formed but are not terms of type `Type`, in Agda and in Elixir alike.

## Names

| | |
| --- | --- |
| Language | Muro |
| Theory | MuroTT |
| Files | `.muro` |
| Elixir | `Muro`, `Muro.Check`, `Muro.Emit`, `Muro.Parser` |
| Agda | `Muro.*` |