The README makes claims. This file backs them up with evidence.
Formal Verification — Idris2 ABI proofs for protocol correctness, encryption invariants, and bridge safety
Evidence: The project maintains 5 Idris2 proof files in src/abi/:
- Types.idr: Core types with C ABI sizes and injectivity proofs
- Protocol.idr: IPP op-code injectivity and job state machine transitions
- Encryption.idr: encrypt/decrypt roundtrip identity and ciphertext bounds
- Layout.idr: Struct memory layout alignment for FFI boundary safety
- Bridge.idr: Toll-free bridging (iOS), keychain semantics, thread safety, JNI invariants
Every unsafe block in Rust references the specific ABI proof that justifies it. This is verifiable in crates/presswerk-security/src/bridge.rs and crates/presswerk-bridge/src/lib.rs where SAFETY comments cite Bridge.idr proofs (see README line 161).
Caveat: Formal verification covers the ABI layer and encryption boundary only, not the entire application. The UI and document processing logic rely on Rust’s type system without dependent type proofs.
Encrypted Storage — age (X25519) encryption at rest for all local data
Evidence: The Cargo.toml workspace (line 36-56) declares 6 crates with dependency ordering: presswerk-core → presswerk-security → presswerk-document → presswerk-print → presswerk-bridge → presswerk-app. The security crate depends on
ageandring(line 64-65, README). The audit trail is append-only encrypted SQLite (line 27 README). Encryption for print server mode uses age (X25519) demonstrated in RFC 8010/8011 IPP client implementation with downgrade safety (IPPS → IPP → LPR → Raw TCP per line 19-20).Caveat: X25519 is proven secure, but key management (generation, storage on-device in iOS Keychain / Android Keystore) relies on platform security, not formal verification.
== Technology Choices
Technology Learn More Rust
https://www.rust-lang.org (6 crates, 46 source files, 10,749 lines)
Dioxus 0.7+
https://dioxuslabs.com (mobile UI, React-like pure Rust)
age (X25519)
https://age-encryption.org (encryption at rest)
Idris2 ABI
https://www.idris-lang.org (formal proofs, 5 files, 0 Admitted)
Zig FFI
https://ziglang.org (C-compatible iOS/Android bridge)
== Dogfooded Across The Account
Uses the hyperpolymath ABI/FFI standard (Idris2 + Zig). Same pattern across proven, burble, and gossamer.
Presswerk-specific: -
src/abi/Bridge.idr— Proves toll-free bridging for iOS UIKit and Android JNI -ffi/zig/src/— Zig FFI implementation for platform native calls -crates/presswerk-bridge/src/— Rust FFI wrappers calling Zig layer== File Map: Key Modules
Path What’s There
crates/presswerk-core/Shared types, errors, configuration (no internal deps)
crates/presswerk-security/Encrypted storage (age, ring, rustls, rusqlite audit trail)
crates/presswerk-document/PDF read/write/merge/split, image processing, OCR
crates/presswerk-print/IPP client/server, mDNS discovery, job queue
crates/presswerk-bridge/Native platform FFI (objc2 iOS, jni Android)
crates/presswerk-app/Dioxus UI (10 pages, routing, state management)
src/abi/5 Idris2 ABI proofs (Types, Protocol, Encryption, Layout, Bridge)
ffi/zig/5 Zig FFI test files, C-compatible implementations
.bot_directives/7 bot configurations for automation
== Questions?
Open an issue in the hyperpolymath/presswerk repository for details on formal verification approach, encryption strategy, or mobile FFI integration.