v0.1.0-dev

hadlink v0.1.0-dev

First development release of hadlink, a self-hosted, high-assurance URL shortener.

Highlights

• SPARK-verified core: URL validation and short code generation run through formally-verified SPARK code via FFI
• Deterministic short codes: Same URL always produces the same 8-character Base62 code (HMAC-SHA256 via SPARKNaCl)
• Working HTTP API: Create and resolve short links

What Works

• POST /api/create - Create short links with URL validation
• GET /{code} / HEAD /{code} - 302 redirect to original URL
• SPARK proofs at 99% coverage
• SQLite storage with WAL mode
• Local development via redo run-shorten

Not Yet Integrated

• Rate limiting (structure exists, not wired in)
• Proof-of-Work verification (implemented, not wired in)
• API key validation
• Property test suite

Quick Start

# Prerequisites: redo, stack, alire
redo all
redo run-shorten

# In another terminal
curl -X POST http://localhost:8080/api/create \
-d "url=https://example.com/path"

Architecture

Haskell (Warp HTTP server) → FFI → SPARK (URL canonicalization, short code generation) → SQLite

See docs/ROADMAP.md for development phases.

Third-Party Acknowledgments

• dinkelk/redo (MIT) - Build system
• Alire (GPL-3.0) - Ada package manager
• GNAT/GNATprove (GPL-3.0 with RLE) - Ada/SPARK toolchain
• SPARKNaCl (BSD 3-Clause) - Cryptographic primitives
• GHC (BSD 3-Clause) - Haskell compiler
• Stack (BSD 3-Clause) - Haskell build tool
• curl (curl license) - HTTP client for examples