refactor: migrate Markdown to AsciiDoc

ARCHITECTURE.adoc

@@ -0,0 +1,48 @@
+== Architecture
+
+=== Overview
+
+This repository follows a modular, maintainable architecture designed
+for clarity, scalability, and long-term sustainability.
+
+=== Directory Structure
+
+....
+.
+├── src/           # Source code
+├── tests/        # Test suites
+├── docs/         # Documentation
+├── scripts/      # Utility scripts
+├── config/       # Configuration files
+├── LICENSE       # License file
+├── LICENSES/     # Full license texts
+└── README.adoc   # Project documentation
+....
+
+=== Design Principles
+
+* *Separation of Concerns*: Each module has a single responsibility
+* *Testability*: Code is written to be easily testable
+* *Documentation*: All public APIs are documented
+* *Configuration*: Environment-specific settings are externalized
+
+=== Dependencies
+
+* External dependencies are minimized and clearly declared
+* Version pinning is used for reproducibility
+
+=== Security Considerations
+
+* Sensitive data is never committed to the repository
+* Secrets are managed through environment variables or secure vaults
+* Regular dependency audits are performed
+
+=== Maintainability
+
+* Code follows consistent style guidelines
+* Pull requests require review and CI checks
+* Issues and discussions are tracked transparently
+
+'''''
+
+_Last updated: 2026-07-18_

CODE_OF_CONDUCT.adoc

@@ -0,0 +1,49 @@
+== Code of Conduct
+
+This project adopts the
+https://www.contributor-covenant.org/version/2/1/code_of_conduct/[Contributor
+Covenant 2.1]. The key obligations are summarised inline so they are
+enforceable directly from this repository.
+
+=== Our Pledge
+
+We pledge to make participation in echo-types a *harassment*-free
+experience for everyone, regardless of age, body size, visible or
+invisible disability, ethnicity, sex characteristics, gender identity
+and expression, level of experience, education, socio-economic status,
+nationality, personal appearance, race, religion, or sexual identity and
+orientation.
+
+=== Unacceptable Behaviour
+
+Unacceptable behaviour includes: *harassment* in any form, public or
+private; trolling, insulting, or derogatory comments; personal or
+political attacks; publishing others’ private information without
+explicit permission; and other conduct which could reasonably be
+considered inappropriate in a professional setting.
+
+=== Enforcement
+
+Instances of abusive, harassing, or otherwise unacceptable behaviour may
+be reported confidentially to the maintainer at
+`+j.d.a.jewell@open.ac.uk+`. All complaints will be reviewed and
+investigated promptly and fairly. Reports are confidential by default.
+
+==== Enforcement procedures
+
+Maintainers follow these Community Impact Guidelines in determining the
+consequences for any action they deem in violation of this Code of
+Conduct:
+
+[arabic]
+. *Correction* — a private, written warning for unprofessional conduct.
+. *Warning* — a warning with consequences for continued behaviour; no
+interaction with the people involved for a specified period.
+. *Temporary ban* — a temporary ban from any interaction or public
+communication with the community.
+. *Permanent ban* — a permanent ban from any public interaction within
+the community.
+
+Maintainers who do not follow or enforce this Code of Conduct in good
+faith may face temporary or permanent repercussions as determined by the
+project’s leadership.

CONTRIBUTING.adoc

@@ -0,0 +1,84 @@
+== Contributing to echo-types
+
+Thank you for your interest. Echo-types is a constructive Agda
+formalisation; contribution discipline reflects the proof-bearing nature
+of the codebase.
+
+=== Sign-off
+
+All commits require Developer Certificate of Origin sign-off:
+
+....
+git commit -s -m "feat: ..."
+....
+
+=== Branches
+
+* `+main+` — protected; only fast-forward from approved PRs.
+* `+feat/<topic>+` — feature branches, squash-merge.
+* `+fix/<topic>+` — bug-fix branches.
+
+=== Pre-merge checklist
+
+[arabic]
+. `+just verify+` passes (full Agda type-check pass against
+`+proofs/agda/All.agda+` and the test suites).
+. CHANGELOG.md updated under `+[Unreleased]+`.
+. `+.machine_readable/6a2/STATE.a2ml+` `+last-updated+` bumped if the
+change is significant.
+. *Banned constructs.* No new `+believe_me+`, `+assert_total+`,
+`+postulate+`, `+sorry+`, `+Admitted+`, `+unsafeCoerce+`, or
+`+Obj.magic+` introduced. Estate-wide policy.
+. *Guardrails are CI-enforced.* All `+.agda+` files under
+`+proofs/agda/**+` must declare `+{-# OPTIONS --safe --without-K #-}+`
+at the top. `+tools/check-guardrails.sh+` runs at CI time across every
+file (regardless of `+All.agda+` membership) and fails on: missing
+`+--safe+` / `+--without-K+`, escape pragmas (`+TERMINATING+`,
+`+REWRITE+`, `+NO_POSITIVITY_CHECK+`, etc.), `+postulate+` in code, or
+unsafe primitives (`+primTrustMe+`, `+primEraseEquality+`, `+trustMe+`).
+The `+Exploratory+` classification in
+`+docs/echo-types/echo-kernel-note.adoc+` only excuses `+All.agda+`
+membership — it does NOT excuse the guardrail. If you need postulates
+for a demo or earn-back-gate consumer, the file must live outside
+`+proofs/agda/+` (no current non-guarded path exists; widening the
+guardrail’s allowlist requires a separate design discussion).
+. *EI-2 discipline.* Per `+.machine_readable/6a2/STATE.a2ml § ei-2+`,
+the integration-recipe distinctness investigation is _terminated
+negatively_ and is not to be reopened. If a change touches that
+territory, read `+STATE.a2ml § ei-2+` first; the
+`+forbidden-rebrandings+` list is a hard fence.
+. *Naming traps.* `+ModeGraded+` (with trailing `+d+`) is canonical;
+never `+ModeGrade+`. See `+STATE.a2ml § naming-traps+`.
+
+=== Reviews
+
+At least one maintainer review (see MAINTAINERS.adoc). Bridge-module
+changes (the cross-system bridges in `+proofs/agda/Echo*Bridge*.agda+`)
+need attention because they fix the load-bearing distinctness story;
+flag them for explicit review.
+
+=== Contribution model — Tri-Perimeter Contribution Framework (TPCF)
+
+echo-types follows the estate-wide *Tri-Perimeter Contribution Framework
+(TPCF)* — graduated trust without gatekeeping:
+
+* *Perimeter 1 — Core Systems (maintainers only).* The proof kernel:
+`+proofs/agda/Echo.agda+`, the identity-claim spine, the bridge modules,
+the `+All.agda+` / `+Smoke.agda+` wiring, and the guardrail tooling.
+Direct commits by maintainers only.
+* *Perimeter 2 — Expert Extensions (trusted contributors).* New proof
+modules, decoration instances, and ordinal-track slices. Apply via issue
+→ review → merge under the relevant `+proofs/agda/+` path with the build
+invariant green.
+* *Perimeter 3 — Community Sandbox (open to all).* Docs (`+.adoc+`),
+tutorial walkthroughs, wiki pages, `+.well-known/+` content, and spec
+proposals.
+
+==== Fork workflow
+
+External contributors use the standard *fork*-and-pull-request workflow:
+fork the repository, branch from `+main+`, run `+just validate+` locally
+(full Agda verify + kernel-guard), and open a PR. Maintainers (Perimeter
+1) may commit directly to feature branches. Every PR must keep
+`+All.agda+` + `+Smoke.agda+` green under `+--safe --without-K+` and
+introduce no banned constructs (see the pre-merge checklist above).