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,9 @@
+== Contributing
+
+[arabic]
+. Fork the repository
+. Create a feature branch
+. Ensure SPDX headers on all files
+. Submit a pull request
+
+*Author:* Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk

PROOF-NEEDS.adoc

@@ -0,0 +1,135 @@
+== Proof Requirements — KATAGORIA
+
+=== Proof Tier
+
+*Tier*: T3 — Standard
+
+=== Proof Categories
+
+[width="100%",cols="24%,36%,40%",options="header",]
+|===
+|Code |Meaning |Applies?
+|*TP* |Typing Proofs (type soundness, type safety) |Yes
+
+|*INV* |Invariant Proofs (state machines, monotonicity, bounds) |
+
+|*SEC* |Security Proofs (crypto, injection freedom, access control) |
+
+|*CONC* |Concurrency Proofs (linearizability, deadlock freedom) |
+
+|*ALG* |Algorithm Proofs (termination, correctness, bounds) |
+
+|*ABI* |ABI/FFI Proofs (memory layout, pointer safety, platform compat)
+|Yes
+
+|*DOM* |Domain-Specific Proofs (bespoke to this project) |
+|===
+
+=== Mandatory Proofs (All RSR Repos)
+
+These proofs come from the rsr-template-repo and MUST be present in
+every repo:
+
+==== ABI/FFI Boundary Proofs (Idris2)
+
+[width="100%",cols="13%,29%,33%,25%",options="header",]
+|===
+|# |Proof |Status |File
+|ABI-1 |Non-null pointer proofs (`+So (ptr /= 0)+`) |Needed
+|`+verification/proofs/idris2/ABI/Pointers.idr+`
+
+|ABI-2 |Memory layout correctness (`+HasSize+`, `+HasAlignment+`)
+|Needed |`+verification/proofs/idris2/ABI/Layout.idr+`
+
+|ABI-3 |Platform type size proofs (per platform) |Needed
+|`+verification/proofs/idris2/ABI/Platform.idr+`
+
+|ABI-4 |FFI function return type proofs |Needed
+|`+verification/proofs/idris2/ABI/Foreign.idr+`
+
+|ABI-5 |C ABI compliance (`+CABICompliant+`, `+FieldsAligned+`) |Needed
+|`+verification/proofs/idris2/ABI/Compliance.idr+`
+|===
+
+==== Typing Proofs (Prover Varies)
+
+[width="100%",cols="13%,29%,33%,25%",options="header",]
+|===
+|# |Proof |Status |File
+|TP-1 |Core data type well-formedness |Needed
+|`+verification/proofs/idris2/Types.idr+`
+
+|TP-2 |Public API type safety (exported functions) |Needed
+|`+verification/proofs/lean4/ApiTypes.lean+`
+|===
+
+=== Project-Specific Proofs
+
+[cols=",,,,,",options="header",]
+|===
+|# |Proof Needed |Category |Prover |Priority |File(s)
+| | | | | |
+|===
+
+=== Dangerous Patterns (BANNED)
+
+The following MUST NOT appear anywhere in proof files:
+
+[cols=",,",options="header",]
+|===
+|Pattern |Language |Meaning
+|`+believe_me+` |Idris2 |Unsafe cast / trust-me
+|`+assert_total+` |Idris2 |Skip totality check
+|`+postulate+` |Idris2/Agda |Unproven axiom
+|`+sorry+` |Lean4 |Incomplete proof
+|`+Admitted+` |Coq |Incomplete proof
+|`+unsafeCoerce+` |Haskell |Unsafe type cast
+|`+Obj.magic+` |OCaml/ReScript |Unsafe type cast
+|`+unsafe+` (unaudited) |Rust |Unsafe block without safety comment
+|===
+
+CI will reject any PR introducing these patterns (enforced by
+`+panic-attack assail+`).
+
+=== Prover Selection Guide
+
+[width="100%",cols="31%,55%,14%",options="header",]
+|===
+|Use Case |Recommended Prover |Why
+|ABI/FFI boundaries |*Idris2* |Dependent types model layouts precisely
+
+|Type system proofs |*Coq* or *Lean4* |Mature proof assistants for
+metatheory
+
+|Algebraic properties |*Lean4* |Good mathlib support
+
+|Inductive/coinductive |*Agda* |Native support for (co)induction
+
+|Distributed systems |*TLA+* |Model checking for protocols
+
+|Numerical properties |*Isabelle* |Strong real analysis library
+|===
+
+=== Proof File Locations
+
+....
+verification/proofs/
+├── idris2/          # Idris2 proofs (ABI, dependent types)
+│   ├── ABI/         # ABI-specific proofs
+│   └── *.idr        # Project-specific Idris2 proofs
+├── lean4/           # Lean4 proofs (algebra, lattices)
+│   └── *.lean
+├── agda/            # Agda proofs (induction, metatheory)
+│   └── *.agda
+├── coq/             # Coq proofs (type systems, compilation)
+│   └── *.v
+└── tlaplus/         # TLA+ specs (distributed protocols)
+    └── *.tla
+....
+
+=== References
+
+* Master list: `+~/Desktop/PROOF-REQUIREMENTS-MASTER.md+`
+* Proof status tracking: `+PROOF-STATUS.md+` (this repo)
+* Proven library: `+proven+` repo (Idris2 verified foundations)
+* Template: `+rsr-template-repo/PROOF-NEEDS.md+`