// SPDX-License-Identifier: CC-BY-SA-4.0
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
= Idrisiser
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
:toc: left
:icons: font

== What Is This?

Idrisiser is the **meta-prover** of the
https://github.com/hyperpolymath/iseriser[-iser family].  It takes any
interface definition — OpenAPI specs, C header files, `.proto` schemas, or
bare type signatures — and generates **Idris2 dependent-type wrappers** that
_formally prove_ the interface contract is correct, then compiles those proofs
down to a native wrapper via Zig FFI.

Idris2 is the sole formal verification language in the hyperpolymath ecosystem
(chosen over ATS2, Coq, Lean, and Agda for its dependent types, first-class
elaborator reflection, and quantitative type theory).  Idrisiser therefore
sits just below `iseriser` itself in the -iser hierarchy: every other -iser
that needs formal guarantees routes through Idrisiser.

== Why Idrisiser?

Idris2 can prove code correct at compile time, but the learning curve is
brutal.  Idrisiser makes dependent-type proofs accessible to developers who
should not need a PhD in type theory:

* **Automatic formal verification of _any_ interface** — preconditions,
  postconditions, invariants, and totality are proved, not tested.
* **Impossible states become impossible** — dependent types enforce contracts
  at the type level; invalid calls cannot compile.
* **Zero runtime cost** — proofs are erased at compile time; the final native
  wrapper carries no proof overhead.

== How It Works

Describe your interface in an `idrisiser.toml` manifest.  Idrisiser then
executes a six-stage pipeline:

[source,text]
----
idrisiser.toml          <1>
  ↓
Interface Parser         <2>  OpenAPI / .h / .proto / type sigs → IR
  ↓
Idris2 ABI Generation    <3>  Dependent types + proof obligations
  ↓
Proof Compilation         <4>  Totality checker, elaborator reflection
  ↓
Zig FFI Bridge            <5>  C-ABI native wrapper, zero overhead
  ↓
Native Wrapper            <6>  Statically linked, provably correct
----

<1> User writes only the manifest.
<2> Parser extracts interface contracts from heterogeneous sources.
<3> Generates `Types.idr`, `Layout.idr`, `Foreign.idr` with proof obligations.
<4> Idris2 compiler verifies totality, termination, and invariant preservation.
<5> Zig FFI implements C-ABI functions declared in the Idris2 ABI layer.
<6> Output is a native shared/static library with formally verified behaviour.

== Architecture

[source,text]
----
idrisiser/
├── Cargo.toml                # Rust CLI orchestrator
├── src/
│   ├── main.rs               # CLI entry point (init, validate, generate, build, run)
│   ├── lib.rs                # Library API
│   ├── manifest/             # idrisiser.toml parser & validator
│   ├── codegen/              # Idris2 + Zig code generation
│   ├── core/                 # Proof obligation engine
│   ├── definitions/          # Interface definition IR
│   ├── contracts/            # Contract extraction from parsed interfaces
│   ├── errors/               # Structured diagnostics
│   ├── bridges/              # Bridge adapters (OpenAPI, protobuf, C headers)
│   └── interface/
│       ├── abi/              # Idris2 ABI — formal proofs (Types.idr, Layout.idr, Foreign.idr)
│       ├── ffi/              # Zig FFI — C-ABI bridge implementation
│       └── generated/        # Auto-generated C headers
├── verification/             # Property-based and proof verification harnesses
├── examples/                 # End-to-end worked examples
└── docs/                     # Technical documentation
----

=== Key Idris2 Concepts Used

* **Dependent types** — types that depend on values, so a function's return
  type can encode its postcondition.
* **Totality checking** — the compiler proves every function terminates and
  handles every input; partial functions are rejected.
* **Elaborator reflection** — Idris2 metaprogramming that generates proof
  terms at compile time from the parsed interface definition.
* **Quantitative type theory (QTT)** — track how many times a value is used;
  enforce linear or affine resource protocols in the generated wrapper.

== Use Cases

* **Proving REST API contracts** — parse an OpenAPI spec, generate Idris2
  types that prove request/response schemas, status codes, and auth flows.
* **Safe database query wrappers** — generate wrappers that prove query
  parameters are well-typed and result sets match declared schemas.
* **Protocol state machine verification** — prove that a protocol (TLS
  handshake, OAuth flow) can only transition through valid states.
* **Provably-correct serialisation** — generate encoders/decoders with proofs
  that round-tripping preserves data identity.
* **C header safety** — parse `.h` files, generate wrappers proving null
  safety, bounds checking, and resource cleanup.

== Quick Start

[source,bash]
----
# Initialise a manifest
idrisiser init

# Edit idrisiser.toml to describe your interface

# Validate the manifest
idrisiser validate

# Generate proven-correct wrapper
idrisiser generate -o generated/my-api

# Build native artifacts
idrisiser build --release
----

== Status

**Codebase in progress.**  Scaffold phase is complete (CLI, manifest parser,
ABI/FFI stubs, RSR template with full CI/CD).  Interface parser and proof
generation are the active implementation frontier.  See `ROADMAP.adoc`.

== License

SPDX-License-Identifier: CC-BY-SA-4.0
