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_

CHANGELOG.adoc

@@ -0,0 +1,70 @@
+== 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]
+
+==== Fixed
+
+* *Formal proofs now actually machine-check.* The 7 Idris2/Lean4 proofs
+were marked "`100% proven`" since 2026-04-16, but
+`+Foreign+`/`+Platform+`/`+Compliance+` never compiled (Idris2
+unbound-implicit auto-binding; unary-`+Nat+` blow-up on 65536-scale
+arithmetic) and no CI job ever ran a prover. All 6 Idris2 modules + the
+Lean4 module now pass.
+* *Justfile was unparseable by `+just+`* (line 2 used `+//+` instead of
+`+#+`), which broke every recipe including `+build-wasm+` used by the
+e2e gate. Fixed.
+* *Proof gate was decorative.* `+just proof-check-*+` used a broken
+`+idris2 --check+` invocation (no `+--source-dir+`, never resolved the
+`+ABI.*+` graph) and silently passed when the prover was absent (SKIP =
+exit 0). Now uses the correct invocation and fails-on-skip.
+* *`+checked_add+` made genuinely checked.* The export was a wrapping
+`+a +% b+` despite its name (the GAP-1b metamorphic gate surfaced the
+misnomer). It is now a real checked add: overflow TRAPS
+(`+@addWithOverflow+` + `+unreachable+` → WASM trap → `+{:error, _}+`,
+BEAM survives) in all build modes, and a non-overflowing add returns the
+exact sum. Signature unchanged (the ABI gate stays green); the
+metamorphic oracle now asserts trap-on-overflow.
+
+==== Changed
+
+* Project gloss *"`Safe NIFs`" → "`Safer NIFs`"* (acronym SNIF
+unchanged): WASM sandboxing makes NIFs _safer_, not provably _safe_.
+Living docs + paper/citation titles updated. NOTE: the paper carries
+Zenodo DOI 10.5281/zenodo.19520245 under the old title — the rename
+should be reflected on the next Zenodo version/deposit.
+* Re-modeled `+Platform.idr+` WASM memory-size facts over `+Integer+`
+(was unary `+Nat+`).
+
+==== Added
+
+* `+.github/workflows/proofs.yml+` — real CI proof gate (Idris2 + Lean4
+via Nix).
+* *SNIFs 2 — sharpened verification.* SEC-1 (`+SnifIsolation.agda+`) now
+wires confidentiality into the operational theorem (deniability
+re-derived over the actual run via `+run-deniable+` /
+`+fault-via-observe+` + a two-distinct-secret `+SecretWitness+`), models
+the real 6-origin error taxonomy (`+TrapOrigin+` guestFault / hostBudget
+/ preExec + a `+call+` front-end + `+PreExecWitness+`), and adds a
+non-trivial-`+Alive+` recovery witness (`+PartialAlive+`) — all
+mutation-confirmed load-bearing by a 4-skeptic adversarial re-audit
+(`+--safe --without-K+`, every targeted mutation rejected).
+* *ABI-7 buffer-guest coverage.*
+`+verification/proofs/idris2/ABI/BufferAbi.idr+` models all 7
+`+buffer_abi+` exports (multi-value/void-faithful `+WasmSig+`), raising
+gated ABI coverage to 15 of 20 Zig export sites;
+`+verification/tools/abi_conformance.py+` is now guest-aware (per-guest
+model manifest, multi-value/void parsing). The conformance gate now runs
+in CI (`+proofs.yml+`, CI-1).
+* *GAP-1b behaviour gate.* `+demo/test/snif_metamorphic_test.exs+` —
+dependency-free metamorphic relations over the scalar kernels (fibonacci
+recurrence + base cases; `+checked_add+` non-overflow = exact-sum /
+overflow = trap oracle).
+* `+AFFIRMATION.adoc+` — point-in-time, ground-truthed honesty snapshot
+(the README/EXPLAINME/AFFIRMATION trio); SPDX header parked for the
+owner to add + sign.

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

GOVERNANCE.adoc

@@ -0,0 +1,60 @@
+== Governance
+
+=== Overview
+
+This project is governed by the following principles and structures to
+ensure transparent, inclusive, and effective decision-making.
+
+=== Roles and Responsibilities
+
+==== Maintainers
+
+Maintainers are responsible for: - Reviewing and merging pull requests -
+Managing releases and versioning - Ensuring code quality and standards -
+Triaging issues and bug reports - Community engagement and support
+
+==== Contributors
+
+Contributors are expected to: - Follow the code of conduct - Submit
+well-documented pull requests - Write tests for new functionality -
+Maintain existing tests - Update documentation as needed
+
+=== Decision Making
+
+==== Minor Changes
+
+* Can be made by any maintainer
+* Include bug fixes, documentation updates, dependency updates
+
+==== Major Changes
+
+* Require discussion in issues or pull requests
+* Include new features, architectural changes, API changes
+* Need approval from at least 2 maintainers
+
+==== Breaking Changes
+
+* Require RFC (Request for Comments) process
+* Need approval from majority of maintainers
+* Must include migration guide
+
+=== Code of Conduct
+
+All participants are expected to follow our Code of Conduct. Violations
+can be reported to the maintainers.
+
+=== Communication
+
+* *Issues*: For bug reports and feature requests
+* *Discussions*: For questions and general discussion
+* *Pull Requests*: For code contributions
+
+=== Licensing
+
+All contributions are made under the terms of the repository’s LICENSE
+file. By submitting a pull request, you agree to license your
+contributions accordingly.
+
+'''''
+
+_Last updated: 2026-07-18_