refactor: migrate Markdown to AsciiDoc

CODE_OF_CONDUCT.adoc

@@ -0,0 +1,24 @@
+== Contributor Covenant Code of Conduct
+
+=== Our Pledge
+
+We pledge to make participation a harassment-free experience for
+everyone.
+
+=== Our Standards
+
+*Positive behavior:* * Using welcoming language * Being respectful of
+differing viewpoints * Accepting constructive criticism * Focusing on
+what is best for the community
+
+*Unacceptable behavior:* * Harassment, trolling, or personal attacks *
+Publishing private information without permission
+
+=== Enforcement
+
+Report issues to the maintainers. All complaints will be reviewed.
+
+=== Attribution
+
+Adapted from https://www.contributor-covenant.org/[Contributor Covenant]
+v2.1.

CONTRIBUTING.adoc

@@ -0,0 +1,71 @@
+== Contributing
+
+Thank you for your interest in contributing! We follow a "`Dual-Track`"
+architecture where human-readable documentation lives in the root and
+machine-readable policies live in `+.machine_readable/+`.
+
+=== How to Contribute
+
+We welcome contributions in many forms:
+
+* *Code:* Improving the core stack or extensions
+* *Documentation:* Enhancing docs or AI manifests
+* *Testing:* Adding property-based tests or formal proofs
+* *Bug reports:* Filing clear, reproducible issues
+
+=== Getting Started
+
+[arabic]
+. *Read the AI Manifest:* Start with `+0-AI-MANIFEST.a2ml+` (if present)
+to understand the repository structure.
+. *Environment:* Use `+nix develop+` or `+direnv allow+` to set up your
+tools.
+. *Task Runner:* Use `+just+` to see available commands
+(`+just --list+`).
+
+=== Development Workflow
+
+==== Branch Naming
+
+....
+docs/short-description       # Documentation
+test/what-added              # Test additions
+feat/short-description       # New features
+fix/issue-number-description # Bug fixes
+refactor/what-changed        # Code improvements
+security/what-fixed          # Security fixes
+....
+
+==== Commit Messages
+
+We follow https://www.conventionalcommits.org/[Conventional Commits]:
+
+....
+<type>(<scope>): <description>
+
+[optional body]
+
+[optional footer]
+....
+
+Types: `+feat+`, `+fix+`, `+docs+`, `+test+`, `+refactor+`, `+ci+`,
+`+chore+`, `+security+`
+
+=== Reporting Bugs
+
+Before reporting: 1. Search existing issues 2. Check if it’s already
+fixed in `+main+`
+
+When reporting, include: - Clear, descriptive title - Environment
+details (OS, versions, toolchain) - Steps to reproduce - Expected vs
+actual behaviour
+
+=== Code of Conduct
+
+All contributors are expected to adhere to our
+link:CODE_OF_CONDUCT.md[Code of Conduct].
+
+=== License
+
+By contributing, you agree that your contributions will be licensed
+under the same license as the project (see LICENSE).

README.adoc

@@ -0,0 +1,139 @@
+== 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 ①
+  ↓
+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
+----
+
+[arabic]
+. User writes only the manifest.
+. Parser extracts interface contracts from heterogeneous sources.
+. Generates `+Types.idr+`, `+Layout.idr+`, `+Foreign.idr+` with proof
+obligations.
+. Idris2 compiler verifies totality, termination, and invariant
+preservation.
+. Zig FFI implements C-ABI functions declared in the Idris2 ABI layer.
+. 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