ATSiser wraps C codebases in ATS2 linear types for zero-cost memory safety.
It analyses C source, identifies memory-critical patterns, generates ATS2
wrappers with viewtype/dataviewtype annotations, and compiles them back
to C with proofs erased — zero runtime overhead.
atsiser/
├── src/
│ ├── main.rs # CLI entry point (clap subcommands)
│ ├── lib.rs # Library API (load, validate, generate)
│ ├── manifest/ # atsiser.toml parser and validator
│ ├── codegen/ # ATS2 wrapper code generation
│ │ ├── viewtype.rs # viewtype annotations for pointer ownership
│ │ ├── dataviewtype.rs # State machine encodings for resource lifecycle
│ │ ├── arrayview.rs # Buffer bounds proofs
│ │ └── proof.rs # praxi/prfun proof obligation emission
│ ├── core/ # C source analysis engine
│ │ ├── parser.rs # C header parsing (tree-sitter/libclang)
│ │ ├── ownership.rs # Pointer ownership graph construction
│ │ ├── allocation.rs # malloc/free pair tracking
│ │ └── bounds.rs # Array bounds detection
│ ├── abi/ # Rust-side ABI type definitions
│ ├── definitions/ # Shared type definitions
│ ├── errors/ # Error types and diagnostics
│ ├── contracts/ # Contractile integration
│ ├── bridges/ # Cross-iser bridge utilities
│ ├── aspects/ # Cross-cutting concerns
│ └── interface/ # Verified Interface Seams
│ ├── abi/ # Idris2 ABI — proves memory safety properties
│ │ ├── Types.idr # LinearPtr, Viewtype, OwnershipState, etc.
│ │ ├── Layout.idr # C struct memory layout with ownership tracking
│ │ └── Foreign.idr # C analysis and ATS2 compilation FFI
│ ├── ffi/ # Zig FFI — C-ABI bridge
│ │ ├── build.zig
│ │ ├── src/main.zig # FFI implementation
│ │ └── test/ # Integration tests
│ └── generated/ # Auto-generated C headers from Idris2 ABI
│ └── abi/
├── tests/ # Rust integration tests
├── examples/ # Example manifests and C projects
├── container/ # Stapeln container definitions
├── verification/ # Formal verification artifacts
├── features/ # Feature specifications
├── docs/
│ ├── architecture/ # Architecture diagrams, threat model
│ ├── theory/ # ATS2 type theory, linear logic background
│ ├── practice/ # How-to guides, troubleshooting
│ ├── attribution/ # Credits and citations
│ └── legal/ # License exhibits
└── .machine_readable/ # All machine-readable metadata
├── 6a2/ # STATE, META, ECOSYSTEM, AGENTIC, NEUROSYM, PLAYBOOK
├── anchors/ # ANCHOR.a2ml
├── policies/ # Maintenance policies
├── contractiles/ # k9, must, trust, dust, lust
├── bot_directives/ # rhodibot, echidnabot, panicbot, etc.
├── ai/ # AI assistant configuration
├── integrations/ # proven, verisimdb, vexometer, feedback-o-tron
├── configs/ # git-cliff, etc.
├── scripts/ # forge, lifecycle, maintenance, verification
└── compliance/ # REUSE dep5, cargo-deny
atsiser.toml C headers + sources
│ │
▼ ▼
Manifest Parser ──► C Source Analyser
│
┌─────┼─────────────┐
▼ ▼ ▼
Allocation Ownership Buffer
Tracker Graph Bounds
│ │ │
└─────┼─────────────┘
▼
ATS2 Codegen
│ │
▼ ▼
.sats files .dats files
(viewtype sigs) (proof terms)
│ │
└────┬────┘
▼
patsopt (ATS2 compiler)
│
▼
Generated C
(proofs erased,
zero overhead)