|
| 1 | +<!-- |
| 2 | +SPDX-License-Identifier: CC-BY-SA-4.0 |
| 3 | +SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | +--> |
| 5 | + |
| 6 | +# What Is This? |
| 7 | + |
| 8 | +Eclexiaiser instruments existing code with **energy, carbon, and |
| 9 | +resource-cost tracking** — making the environmental cost of computation |
| 10 | +a first-class concern. |
| 11 | + |
| 12 | +[Eclexia](https://github.com/hyperpolymath/eclexia) is one of |
| 13 | +hyperpolymath’s nextgen languages focused on sustainability. It tracks |
| 14 | +resource consumption as a type-level constraint, so developers can write |
| 15 | +carbon-aware software that provably stays within energy budgets. |
| 16 | +Eclexiaiser brings this to any codebase without requiring the developer |
| 17 | +to learn Eclexia directly. |
| 18 | + |
| 19 | +# How It Works |
| 20 | + |
| 21 | +1. **Manifest** (`eclexiaiser.toml`) — define your functions and their |
| 22 | + energy budgets, carbon intensity limits, and resource bounds. |
| 23 | + |
| 24 | +2. **Source instrumentation** — eclexiaiser analyses your code and |
| 25 | + inserts energy measurement hooks at function boundaries. |
| 26 | + |
| 27 | +3. **Eclexia annotation codegen** — generates Eclexia constraint files |
| 28 | + with joule annotations (`@requires` `energy` `<` `5kWh`), carbon |
| 29 | + intensity bounds, and renewable-aware scheduling hints. |
| 30 | + |
| 31 | +4. **Idris2 ABI proofs** — the generated resource bounds are formally |
| 32 | + verified using dependent types. The Idris2 layer proves that your |
| 33 | + energy budget is satisfiable and that carbon intensity limits |
| 34 | + compose correctly across call chains. |
| 35 | + |
| 36 | +5. **Zig FFI bridge** — high-performance energy measurement via RAPL |
| 37 | + (Running Average Power Limit), IPMI, or external APIs. Zero-overhead |
| 38 | + C-ABI interface for reading hardware energy counters and querying |
| 39 | + carbon intensity services. |
| 40 | + |
| 41 | +6. **Enforcement and reporting** — violations are caught at compile |
| 42 | + time where possible, and at runtime otherwise. Generates |
| 43 | + sustainability reports compatible with the EU Corporate |
| 44 | + Sustainability Reporting Directive (CSRD). |
| 45 | + |
| 46 | +# Key Value |
| 47 | + |
| 48 | +- **Know the carbon cost of every function call** — joule annotations |
| 49 | + make energy consumption visible and enforceable at the type level |
| 50 | + |
| 51 | +- **Enforce energy budgets** — set per-function and per-module energy |
| 52 | + limits that are checked at compile time via Idris2 dependent type |
| 53 | + proofs |
| 54 | + |
| 55 | +- **Generate sustainability reports** — produce CSRD-compatible reports |
| 56 | + showing energy consumption, carbon emissions, and renewable energy |
| 57 | + utilisation |
| 58 | + |
| 59 | +- **Carbon intensity API integration** — connect to WattTime or |
| 60 | + Electricity Maps to schedule heavy computation when the grid is |
| 61 | + cleanest |
| 62 | + |
| 63 | +- **Renewable-aware scheduling** — defer energy-intensive work to |
| 64 | + periods of high renewable generation |
| 65 | + |
| 66 | +- **Energy type system** — Eclexia’s `@requires`/`@provides` constraints |
| 67 | + make resource costs explicit and optimisable across the entire call |
| 68 | + graph |
| 69 | + |
| 70 | +# Architecture |
| 71 | + |
| 72 | +Follows the hyperpolymath -iser pattern: |
| 73 | + |
| 74 | + eclexiaiser.toml (manifest: functions, budgets, carbon limits) |
| 75 | + | |
| 76 | + v |
| 77 | + Source instrumentation (insert energy measurement hooks) |
| 78 | + | |
| 79 | + v |
| 80 | + Eclexia annotation codegen (@requires energy, @provides carbon_report) |
| 81 | + | |
| 82 | + v |
| 83 | + Idris2 ABI (proves resource bounds compose, budgets are satisfiable) |
| 84 | + | |
| 85 | + v |
| 86 | + Zig FFI (RAPL/IPMI energy measurement, WattTime/Electricity Maps API) |
| 87 | + | |
| 88 | + v |
| 89 | + Sustainability report + enforcement violations |
| 90 | + |
| 91 | +Part of the [-iser family](https://github.com/hyperpolymath/iseriser). |
| 92 | + |
| 93 | +## Key Types (Idris2 ABI) |
| 94 | + |
| 95 | +- `EnergyBudget` — per-function energy limit in joules, proven |
| 96 | + satisfiable |
| 97 | + |
| 98 | +- `CarbonIntensity` — grams CO2 per kilowatt-hour, sourced from grid API |
| 99 | + |
| 100 | +- `JouleAnnotation` — type-level energy annotation for a function |
| 101 | + |
| 102 | +- `ResourceBound` — composite bound (energy + carbon + time + memory) |
| 103 | + |
| 104 | +- `SustainabilityReport` — aggregated metrics with CSRD field mapping |
| 105 | + |
| 106 | +## Zig FFI Operations |
| 107 | + |
| 108 | +- `eclexiaiser_measure_energy` — read hardware energy counters |
| 109 | + (RAPL/IPMI) |
| 110 | + |
| 111 | +- `eclexiaiser_query_carbon` — fetch current carbon intensity from grid |
| 112 | + API |
| 113 | + |
| 114 | +- `eclexiaiser_enforce_budget` — check a measurement against a proven |
| 115 | + bound |
| 116 | + |
| 117 | +- `eclexiaiser_generate_report` — produce a sustainability report struct |
| 118 | + |
| 119 | +# Use Cases |
| 120 | + |
| 121 | +- **Green computing** — annotate hotspots, set budgets, prove compliance |
| 122 | + |
| 123 | +- **Data centre optimisation** — measure per-function energy, identify |
| 124 | + waste |
| 125 | + |
| 126 | +- **Carbon-aware CI/CD** — skip heavy builds when the grid is dirty; |
| 127 | + schedule nightly jobs when renewables peak |
| 128 | + |
| 129 | +- **EU CSRD compliance** — generate the energy and emissions data |
| 130 | + required by the Corporate Sustainability Reporting Directive |
| 131 | + |
| 132 | +- **Cloud cost prediction** — estimate energy costs before deployment |
| 133 | + using the proven energy bounds |
| 134 | + |
| 135 | +# Status |
| 136 | + |
| 137 | +**Codebase in progress.** Scaffold complete (CLI, manifest parser, |
| 138 | +directory structure, CI/CD). Codegen stubs in place. Idris2 ABI and Zig |
| 139 | +FFI templates present — domain-specific types and energy measurement |
| 140 | +logic pending. |
| 141 | + |
| 142 | +# License |
| 143 | + |
| 144 | +SPDX-License-Identifier: CC-BY-SA-4.0 |
0 commit comments