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 `+guix 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,140 @@
+https://github.com/sponsors/hyperpolymath[image:https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github[Sponsor]]
+
+== What Is This?
+
+ATSiser analyses C source code, identifies memory-critical patterns
+(malloc/free pairs, buffer accesses, pointer arithmetic, struct
+ownership), and generates *ATS2 wrappers* with linear type annotations
+that enforce memory safety at compile time — then compiles those
+wrappers back to C with zero runtime overhead.
+
+https://www.cs.bu.edu/~hwxi/atslangweb/[ATS] (Applied Type System) by
+Hongwei Xi at Boston University provides linear types, dependent types,
+and theorem proving while compiling to C. ATSiser uses ATS2’s
+`+viewtype+` and `+dataviewtype+` constructs to express pointer
+ownership, array bounds, and proof obligations over existing C
+interfaces — *without rewriting the original C code*.
+
+== How It Works
+
+Describe your C interface in `+atsiser.toml+`. ATSiser:
+
+[arabic]
+. *Parses C headers* — identifies allocation sites, pointer ownership
+patterns, buffer accesses, and struct field layouts
+. *Generates ATS2 wrappers* — creates `+viewtype+` annotations for
+pointer ownership, `+arrayview+` proofs for buffer bounds, and
+`+dataviewtype+` encodings for resource lifecycles
+. *Emits proof obligations* — generates ATS2 proof terms (`+praxi+`,
+`+prfun+`) that the ATS2 compiler checks at compile time
+. *Compiles to C* — ATS2 erases all proofs during compilation, producing
+C code with identical performance to the original
+. *Bridges via Zig FFI* — integration layer for non-C consumers
+
+=== Example Manifest
+
+[source,toml]
+----
+[workload]
+name = "my-legacy-lib"
+description = "Harden libfoo with linear type safety"
+
+[source]
+headers = ["include/foo.h", "include/bar.h"]
+sources = ["src/*.c"]
+
+[analysis]
+track-allocations = true        # Follow malloc/free pairs
+track-buffers = true            # Bound-check array accesses
+track-ownership = true          # Prove pointer ownership transfer
+
+[output]
+ats2-wrappers = "generated/ats2/"
+c-headers = "generated/abi/"
+proofs = "generated/proofs/"
+----
+
+== Key Value
+
+* *Memory safety for legacy C* — no rewrites, no new runtime, no garbage
+collector
+* *Zero runtime overhead* — ATS2 proofs are erased at compile time;
+generated C is identical in performance to handwritten C
+* *Gradual adoption* — wrap critical functions first, expand coverage
+over time
+* *Formal guarantees* — no leaks, no use-after-free, no double-free, no
+out-of-bounds access — all proven at compile time via linear types
+
+== Architecture
+
+Follows the hyperpolymath -iser pattern:
+
+* *Manifest* (`+atsiser.toml+`) — describe WHAT C code you want hardened
+* *C Source Analysis* (`+src/core/+`) — parse headers, identify
+allocation patterns, track pointer ownership through call graphs
+* *Idris2 ABI* (`+src/interface/abi/+`) — formal proofs that the
+generated wrappers correctly model memory safety properties (ownership
+transfer, buffer bounds, allocation/deallocation pairing)
+* *Zig FFI* (`+src/interface/ffi/+`) — C-ABI bridge for integration with
+non-C consumers
+* *ATS2 Codegen* (`+src/codegen/+`) — generates ATS2 source with
+`+viewtype+`, `+dataviewtype+`, `+praxi+`, and `+prfun+` annotations
+* *Rust CLI* (`+src/main.rs+`) — orchestrates analysis, generation, and
+compilation
+
+User writes zero ATS2 code. ATSiser generates everything from the
+manifest and C source analysis.
+
+=== ATS2 Concepts Used
+
+* *viewtype* — linear types that track pointer ownership; consuming a
+`+viewtype+` value proves the pointer was freed exactly once
+* *dataviewtype* — algebraic data types with linear semantics for
+modelling resource states (allocated, borrowed, freed)
+* *arrayview* — dependent-type proofs that array accesses are within
+bounds
+* *praxi / prfun* — proof-level functions that establish safety
+invariants without generating any runtime code
+
+== CLI Commands
+
+[source,bash]
+----
+# Initialise a new manifest
+atsiser init
+
+# Validate manifest and C sources
+atsiser validate -m atsiser.toml
+
+# Analyse C code and generate ATS2 wrappers
+atsiser generate -m atsiser.toml -o generated/atsiser
+
+# Build generated artifacts (ATS2 → C compilation)
+atsiser build -m atsiser.toml
+
+# Show analysis summary
+atsiser info -m atsiser.toml
+----
+
+== Use Cases
+
+* *Legacy C library hardening* — wrap libc, OpenSSL, or custom C
+libraries with compile-time memory safety proofs
+* *Embedded systems safety* — add formal guarantees to
+resource-constrained C code without any runtime cost
+* *Gradual migration from C to safe C* — incrementally wrap functions,
+building a safety envelope around existing codebases
+* *Compliance* — generate machine-checkable proofs of memory safety for
+safety-critical or regulated codebases
+
+Part of the https://github.com/hyperpolymath/iseriser[-iser family] of
+acceleration frameworks.
+
+== Status
+
+*Codebase in progress.* Architecture defined, CLI scaffolded, codegen
+and C source analysis pending implementation.
+
+== License
+
+SPDX-License-Identifier: CC-BY-SA-4.0