From 30cb01778dd6275d35ddcb4c70499da150c89ec9 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 25 Jun 2026 20:02:57 +0100 Subject: [PATCH] docs(readme): convert README.adoc -> Markdown README.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit README must be real Markdown to render in GitHub community-health, the GitHub profile, and external MCP directories (Glama) — AsciiDoc shows as raw markup there. pandoc asciidoc->GFM, badges fixed to clickable, SPDX header kept as an HTML comment, duplicate README.adoc removed. Co-Authored-By: Claude Opus 4.8 --- README.adoc | 139 --------------------------------------------- README.md | 160 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 160 insertions(+), 139 deletions(-) delete mode 100644 README.adoc create mode 100644 README.md diff --git a/README.adoc b/README.adoc deleted file mode 100644 index e908889..0000000 --- a/README.adoc +++ /dev/null @@ -1,139 +0,0 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -= Atsiser -Jonathan D.A. Jewell -:toc: left -:icons: font - -image:https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github[Sponsor,link=https://github.com/sponsors/hyperpolymath] - -== 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: - -1. **Parses C headers** — identifies allocation sites, pointer ownership patterns, - buffer accesses, and struct field layouts -2. **Generates ATS2 wrappers** — creates `viewtype` annotations for pointer - ownership, `arrayview` proofs for buffer bounds, and `dataviewtype` encodings - for resource lifecycles -3. **Emits proof obligations** — generates ATS2 proof terms (`praxi`, `prfun`) - that the ATS2 compiler checks at compile time -4. **Compiles to C** — ATS2 erases all proofs during compilation, producing C - code with identical performance to the original -5. **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 diff --git a/README.md b/README.md new file mode 100644 index 0000000..5375740 --- /dev/null +++ b/README.md @@ -0,0 +1,160 @@ + + +[![Sponsor](https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github)](https://github.com/sponsors/hyperpolymath) + +# 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. + +[ATS](https://www.cs.bu.edu/~hwxi/atslangweb/) (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: + +1. **Parses C headers** — identifies allocation sites, pointer + ownership patterns, buffer accesses, and struct field layouts + +2. **Generates ATS2 wrappers** — creates `viewtype` annotations for + pointer ownership, `arrayview` proofs for buffer bounds, and + `dataviewtype` encodings for resource lifecycles + +3. **Emits proof obligations** — generates ATS2 proof terms (`praxi`, + `prfun`) that the ATS2 compiler checks at compile time + +4. **Compiles to C** — ATS2 erases all proofs during compilation, + producing C code with identical performance to the original + +5. **Bridges via Zig FFI** — integration layer for non-C consumers + +## Example Manifest + +```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 + +```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 [-iser family](https://github.com/hyperpolymath/iseriser) 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