// SPDX-License-Identifier: PMPL-1.0-or-later
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
= Atsiser
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
:toc: left
:icons: font
== 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: PMPL-1.0-or-later