refactor: migrate Markdown to AsciiDoc

CHANGELOG.adoc

@@ -0,0 +1,9 @@
+== Changelog
+
+All notable changes to this project will be documented in this file.
+
+The format is based on https://keepachangelog.com/en/1.1.0/[Keep a
+Changelog], and this project adheres to
+https://semver.org/spec/v2.0.0.html[Semantic Versioning].
+
+=== [Unreleased]

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,95 @@
+== 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
+
+=== Contribution model — Tri-Perimeter Contribution Framework (TPCF)
+
+kategoria follows the estate-wide *Tri-Perimeter Contribution Framework
+(TPCF)* — graduated trust without gatekeeping:
+
+* *Perimeter 1 — Core Systems (maintainers only).* The proof kernel: the
+level-indexed routes (`+routes/+`), the soundness/metatheory modules,
+and the build/CI tooling. Direct commits by maintainers only (see
+`+MAINTAINERS.adoc+`).
+* *Perimeter 2 — Expert Extensions (trusted contributors).* New proof
+routes, demos (`+examples/+`), and dependently-typed extensions. Apply
+via issue → review → merge, with every Idris module type-checking under
+`+idris2 --check+`.
+* *Perimeter 3 — Community Sandbox (open to all).* Docs (`+.adoc+`),
+`+.well-known/+` content, AI manifests, and spec proposals.
+
+==== Fork workflow
+
+External contributors use the standard *fork*-and-pull-request workflow:
+fork the repository, branch from `+main+`, run `+just quality+` (and
+`+idris2 --check+` on any touched proof module) locally, then open a PR.
+Maintainers (Perimeter 1) may commit directly to feature branches. Proof
+modules must type-check before review — a red Idris check blocks merge.
+
+=== 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).

PROOF-NEEDS.adoc

@@ -0,0 +1,49 @@
+== PROOF-NEEDS.md — kategoria
+
+=== Current State
+
+* **src/abi/*.idr**: NO
+* *Dangerous patterns*: 1 `+believe_me+` in `+Level09_SessionTypes.idr+`
+(runtime placeholder for recv)
+* *LOC*: ~4,400 (Idris2 routes + Nickel)
+* *ABI layer*: Missing (but routes contain Idris2 type safety challenge
+levels)
+
+=== What Needs Proving
+
+[width="100%",cols="51%,27%,22%",options="header",]
+|===
+|Component |What |Why
+|Session types (Level09) |Remove `+believe_me+` placeholder with real
+recv implementation |Current believe_me bypasses type checker for
+session receive
+
+|Cubical types (Level10) |Complete type equality proofs without
+believe_me |Level10 notes need for believe_me; should use proper cubical
+path types
+
+|Route completeness |All 5 routes (alpha-epsilon) have total, proven
+implementations |Challenge levels should themselves be provably correct
+
+|K9 contractile guards |believe_me/assert_total ceiling enforcement is
+sound |Meta-level: the guards themselves need correctness proofs
+|===
+
+=== Recommended Prover
+
+*Idris2* — The repo IS an Idris2 type safety challenge. The believe_me
+in Level09 is the primary proof gap. Level10 cubical types may benefit
+from *Agda* with cubical support.
+
+=== Priority
+
+*MEDIUM* — Educational/challenge repo, but the believe_me in Level09
+undermines the repo’s own thesis. Fixing it would demonstrate the very
+point the challenge makes.
+
+=== Template ABI Cleanup (2026-03-29)
+
+Template ABI removed – was creating false impression of formal
+verification. The removed files (Types.idr, Layout.idr, Foreign.idr)
+contained only RSR template scaffolding with unresolved
+\{\{PROJECT}}/\{\{AUTHOR}} placeholders and no domain-specific proofs.