Osgiliath — Haskell Hyperdimensional Computing Framework

Connecting Arthedain's HDC engine to verified, type-safe, hardware-synthesisable Haskell.

Osgiliath is a repo that provides the formal and high-performance backbone for Arthedain, a 125+ module Hyperdimensional Computing (HDC) / Vector Symbolic Architecture (VSA) library. Arthedain is written in Python + PyTorch; Osgiliath is written in Haskell with Clash for hardware synthesis.

Repository Structure

Osgiliath/
├── cabal.project              # Monorepo build file
├── clash-hdc/                 # Type-Safe Hardware HDC Generator
├── hdc-theory/                # Category-Theoretic Formal Foundation
├── hdc-compiler/              # Verified Multi-Backend HDC DSL
├── hdc-quickcheck/            # Formal Property Testing Framework

Packages

clash-hdc — Type-Safe Hardware HDC Generator

Uses Clash (Haskell-to-hardware compiler) to generate verified, parameterised Verilog from high-level HDC descriptions. Arthedain's hardware/ layer is currently hand-written Verilog (fragile, hard to parameterise). Clash lets Haskell types encode HV dimension, VSA algebra (MAP/FHRR/VTB/BSC), and binding operations — catching invalid hardware configurations at compile time.

Key modules:

• ClashHDC.Types — Type-level HDC dimension, algebra kind, hypervector types
• ClashHDC.Algebra — VSA algebra implementations as type classes
• ClashHDC.Core — LIF neuron, Hebbian trace, weight update as Clash circuits
• ClashHDC.Top — Arthedain top-level architecture (like arthedain_lif.v)
• Hardware.Synthesis — Tcl scripts, XDC constraints, Makefile integration

hdc-theory — Category-Theoretic Formal Foundation

Arthedain's hdc/category_algebra.py (HDCategory, Morphism, Functor, NaturalTransformation, CompositionalAlgebra) expressed in Haskell's type system — the formally verified specification that the Python approximates.

Key modules:

• HDC.Category — HDCategory, Morphism, OpType as type-level constructs
• HDC.Functor — Structure-preserving maps between HDC spaces
• HDC.NaturalTransformation — Transformations between functors
• HDC.CompositionalAlgebra — Algebraic laws proven via types
• HDC.Concentration — Concentration of measure formulas (from concentration.py)
• HDC.FractionalPower — Fractional Power Encoding (from vsa_algebras.py)

hdc-compiler — Verified Multi-Backend HDC DSL

An EDSL compiling HDC model descriptions to:

• Python bindings for Arthedain
• Optimized C for STM32/RISC-V microcontrollers
• Verilog via Clash
• Loihi 2 Lava cross-assembly

Key modules:

• HDC.Compiler.Core — Core IR for HDC expressions
• HDC.Compiler.Rewrite — Algebraic rewrite rules
• HDC.Compiler.Backend.Python — Python/Arthedain codegen
• HDC.Compiler.Backend.C — C for microcontrollers
• HDC.Compiler.Backend.Clash — Verilog via Clash
• HDC.Compiler.Backend.Lava — Loihi 2 Lava cross-assembly

hdc-quickcheck — Formal Property Testing Framework

QuickCheck/SmallCheck properties for the entire HDC algebra: concentration of measure, fault tolerance guarantees, cleanup memory capacity bounds — replacing empirical Python tests with formally verified properties.

Key modules:

• HDC.Properties.Concentration — Concentration of measure properties

• HDC.Properties.Algebra — Algebraic law properties

• HDC.Properties.Cleanup — Cleanup memory capacity bounds

• HDC.Properties.FaultTolerance — Fault tolerance guarantees

• HDC.Properties.Encoding — Encoding fidelity properties

• Category theory is Haskell's native paradigm — Arthedain's OpType enum and Morphism.compose() become first-class type-level constructs

• Clash directly targets the FPGA hardware Arthedain already synthesises to (~2.5 mW on Artix-7)

• Algebraic optimisations work naturally as Haskell rewrite rules (fusion of bind chains, dead-code elimination of unused dimensions)

• Every Python HDC module in the 125-module library has a natural Haskell counterpart with stronger guarantees

Building

# Install GHC 9.4+, cabal-install 3.8+, and ghcup
curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | sh

# Build all packages
cabal build all

# Run tests
cabal test all

# Build specific package
cabal build clash-hdc
cabal build hdc-theory
cabal build hdc-compiler
cabal build hdc-quickcheck

# Generate Verilog with Clash
cabal run clash-hdc:clash-hdc-exe -- --generate-verilog

License

BSD 3-Clause (same as Arthedain)