// SPDX-License-Identifier: CC-BY-SA-4.0
// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
= Eclexiaiser
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
:toc: left
:icons: font

== What Is This?

Eclexiaiser instruments existing code with **energy, carbon, and resource-cost
tracking** — making the environmental cost of computation a first-class concern.

https://github.com/hyperpolymath/eclexia[Eclexia] is one of hyperpolymath's
nextgen languages focused on sustainability. It tracks resource consumption as
a type-level constraint, so developers can write carbon-aware software that
provably stays within energy budgets. Eclexiaiser brings this to any codebase
without requiring the developer to learn Eclexia directly.

== How It Works

1. **Manifest** (`eclexiaiser.toml`) — define your functions and their energy
   budgets, carbon intensity limits, and resource bounds.
2. **Source instrumentation** — eclexiaiser analyses your code and inserts
   energy measurement hooks at function boundaries.
3. **Eclexia annotation codegen** — generates Eclexia constraint files with
   joule annotations (`@requires energy < 5kWh`), carbon intensity bounds, and
   renewable-aware scheduling hints.
4. **Idris2 ABI proofs** — the generated resource bounds are formally verified
   using dependent types. The Idris2 layer proves that your energy budget is
   satisfiable and that carbon intensity limits compose correctly across call
   chains.
5. **Zig FFI bridge** — high-performance energy measurement via RAPL (Running
   Average Power Limit), IPMI, or external APIs. Zero-overhead C-ABI interface
   for reading hardware energy counters and querying carbon intensity services.
6. **Enforcement and reporting** — violations are caught at compile time where
   possible, and at runtime otherwise. Generates sustainability reports
   compatible with the EU Corporate Sustainability Reporting Directive (CSRD).

== Key Value

* **Know the carbon cost of every function call** — joule annotations make
  energy consumption visible and enforceable at the type level
* **Enforce energy budgets** — set per-function and per-module energy limits
  that are checked at compile time via Idris2 dependent type proofs
* **Generate sustainability reports** — produce CSRD-compatible reports showing
  energy consumption, carbon emissions, and renewable energy utilisation
* **Carbon intensity API integration** — connect to WattTime or Electricity Maps
  to schedule heavy computation when the grid is cleanest
* **Renewable-aware scheduling** — defer energy-intensive work to periods of
  high renewable generation
* **Energy type system** — Eclexia's `@requires`/`@provides` constraints make
  resource costs explicit and optimisable across the entire call graph

== Architecture

Follows the hyperpolymath -iser pattern:

----
eclexiaiser.toml   (manifest: functions, budgets, carbon limits)
       |
       v
Source instrumentation (insert energy measurement hooks)
       |
       v
Eclexia annotation codegen (@requires energy, @provides carbon_report)
       |
       v
Idris2 ABI (proves resource bounds compose, budgets are satisfiable)
       |
       v
Zig FFI (RAPL/IPMI energy measurement, WattTime/Electricity Maps API)
       |
       v
Sustainability report + enforcement violations
----

Part of the https://github.com/hyperpolymath/iseriser[-iser family].

=== Key Types (Idris2 ABI)

* `EnergyBudget` — per-function energy limit in joules, proven satisfiable
* `CarbonIntensity` — grams CO2 per kilowatt-hour, sourced from grid API
* `JouleAnnotation` — type-level energy annotation for a function
* `ResourceBound` — composite bound (energy + carbon + time + memory)
* `SustainabilityReport` — aggregated metrics with CSRD field mapping

=== Zig FFI Operations

* `eclexiaiser_measure_energy` — read hardware energy counters (RAPL/IPMI)
* `eclexiaiser_query_carbon` — fetch current carbon intensity from grid API
* `eclexiaiser_enforce_budget` — check a measurement against a proven bound
* `eclexiaiser_generate_report` — produce a sustainability report struct

== Use Cases

* **Green computing** — annotate hotspots, set budgets, prove compliance
* **Data centre optimisation** — measure per-function energy, identify waste
* **Carbon-aware CI/CD** — skip heavy builds when the grid is dirty; schedule
  nightly jobs when renewables peak
* **EU CSRD compliance** — generate the energy and emissions data required by
  the Corporate Sustainability Reporting Directive
* **Cloud cost prediction** — estimate energy costs before deployment using
  the proven energy bounds

== Status

**Codebase in progress.** Scaffold complete (CLI, manifest parser, directory
structure, CI/CD). Codegen stubs in place. Idris2 ABI and Zig FFI templates
present — domain-specific types and energy measurement logic pending.

== License

SPDX-License-Identifier: CC-BY-SA-4.0
