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

Role in the Arthedain Synthesis Pipeline

Osgiliath is Enotrium's core toolchain infrastructure — the verified path from HDC model description to hardware:

Arthedain model (Python/PyTorch HDC)
        │
        ▼
hdc-compiler (typed EDSL + core IR, algebraic rewrites)
        │
        ├─► Python bindings        (back into Arthedain)
        ├─► Optimized C            (STM32 / RISC-V microcontrollers)
        ├─► Verilog via clash-hdc  (Artix-7 / Zynq FPGA fabric)
        └─► Lava cross-assembly    (Intel Loihi 2)
                │
                ▼
Hardware.Synthesis (Tcl + XDC + Makefile) ─► Vivado ─► bitstream

This is the differentiator: competitors hand-write and hand-verify RTL for each deployment; here, hdc-theory proves the algebra at the type level, hdc-quickcheck property-tests the implementations against it, and clash-hdc generates the hardware from the same verified description. Invalid hardware configurations (wrong dimension, mismatched VSA algebra, illegal binding) fail at compile time, not on the bench.

Deployment targets include the Low-SWaP-Edge-ISR Zynq-7020 accelerator, whose hand-written RTL this toolchain is slated to replace.

Why Haskell

• 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 — claim substantiation tracked in the org evaluations repo)
• 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)