Skip to content

README.md

Latest commit

 

History

History
139 lines (106 loc) · 5.13 KB

README.md

File metadata and controls

139 lines (106 loc) · 5.13 KB

Sponsor

// SPDX-License-Identifier: MPL-2.0 // 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: MPL-2.0