hadlink v1.0.1

What's Changed

• Update healthcheck endpoint to GET /health by @Jbsco in #15

Also now available from the AUR.

yay -S hadlink-bin

Full Changelog: v1.0.0...v1.0.1

hadlink v1.0.0

Full Changelog: v0.1.0...v1.0.0

v0.1.0 Public Release

What's Changed

• Set clear FFI boundary by @Jbsco in #1
• Implement rate limiting & property testing in the Haskell layer by @Jbsco in #2
• Implement continuous integration actions for GitHub by @Jbsco in #3
• Update documentation to include DO-278A language and objective mappings by @Jbsco in #4
• Restructure http https equivalence (near-Gold level SPARK assurance) by @Jbsco in #5
• Proof of work integration by @Jbsco in #6
• Docker and Systemd deployment implementation by @Jbsco in #7
• Security self audit by @Jbsco in #8
• V1 documentation by @Jbsco in #9

Full Changelog: v0.1.0-dev...v0.1.0

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