TOPOLOGY.adoc

TOPOLOGY — eclexiaiser

Purpose

Energy, carbon, and resource-cost awareness for existing software via Eclexia economics-as-code. Instruments code with energy measurement hooks, generates Eclexia constraint annotations, and formally verifies resource bounds.

Module Map

eclexiaiser/
├── src/
│   ├── main.rs                    # CLI entry point (clap subcommands)
│   ├── lib.rs                     # Library re-exports
│   ├── manifest/mod.rs            # eclexiaiser.toml parser and validator
│   ├── codegen/mod.rs             # Eclexia annotation + instrumented source codegen
│   ├── abi/mod.rs                 # Rust-side ABI module (Idris2 proof types)
│   ├── definitions/               # Domain type definitions
│   ├── errors/                    # Error types and diagnostics
│   ├── contracts/                 # Contractile enforcement hooks
│   ├── aspects/
│   │   ├── security/              # Security aspect (audit trail for energy data)
│   │   ├── observability/         # Observability aspect (metrics, tracing)
│   │   └── integrity/             # Integrity aspect (measurement tamper detection)
│   ├── core/                      # Core logic (budget calculation, composition)
│   ├── bridges/                   # Language-specific instrumentation bridges
│   └── interface/
│       ├── abi/                   # Idris2 ABI — formal proofs of resource bounds
│       │   ├── Types.idr          # EnergyBudget, CarbonIntensity, JouleAnnotation,
│       │   │                      # ResourceBound, SustainabilityReport
│       │   ├── Layout.idr         # Energy measurement struct memory layout proofs
│       │   └── Foreign.idr        # FFI declarations for energy/carbon measurement
│       ├── ffi/                   # Zig FFI — energy measurement bridge
│       │   ├── build.zig          # Build config (shared + static lib)
│       │   ├── src/main.zig       # RAPL/IPMI energy reader, carbon API client,
│       │   │                      # budget enforcer, report generator
│       │   └── test/
│       │       └── integration_test.zig  # ABI compliance + measurement tests
│       └── generated/
│           └── abi/               # Auto-generated C headers from Idris2 ABI
├── container/                     # Stapeln container ecosystem
├── docs/
│   ├── architecture/              # THREAT-MODEL.adoc, diagrams
│   ├── developer/                 # ABI-FFI-README.adoc
│   ├── reports/                   # Quality, security, compliance, performance, maintenance
│   ├── standards/                 # Standards compliance docs
│   └── templates/                 # Contractile templates
├── examples/                      # Example manifests and instrumented projects
├── features/                      # BDD feature specs
├── tests/                         # Integration tests
├── verification/                  # Formal verification artefacts
├── .machine_readable/
│   ├── 6a2/                       # STATE, META, ECOSYSTEM, AGENTIC, NEUROSYM, PLAYBOOK
│   ├── policies/                  # Maintenance axes, checklist, dev approach
│   ├── bot_directives/            # Bot-specific instructions
│   ├── contractiles/              # k9, dust, lust, must, trust
│   ├── ai/                        # AI configuration
│   ├── configs/                   # git-cliff, etc.
│   └── anchors/                   # ANCHOR.a2ml
└── .github/workflows/             # 17 RSR-standard workflows

Data Flow

eclexiaiser.toml
    │  (manifest: function names, energy budgets, carbon limits, grid zone)
    v
┌──────────────────────┐
│  Source Instrumentation │  Parses target code, inserts measurement hooks
└──────────┬───────────┘
           v
┌──────────────────────┐
│  Eclexia Annotation    │  Generates @requires energy, @provides carbon_report
│  Codegen               │  Emits .eclexia constraint files
└──────────┬───────────┘
           v
┌──────────────────────┐
│  Idris2 ABI Proofs     │  Verifies: budgets satisfiable, bounds compose,
│  (Types.idr)           │  call-graph total fits allocation
└──────────┬───────────┘
           v
┌──────────────────────┐
│  Zig FFI Bridge        │  RAPL/IPMI energy counters, WattTime/Electricity Maps
│  (main.zig)            │  API, budget enforcement, report generation
└──────────┬───────────┘
           v
┌──────────────────────┐
│  Output                │  Sustainability report (CSRD-compatible)
│                        │  Enforcement violations (compile-time or runtime)
│                        │  Energy dashboard data (PanLL panel)
└────────────────────────┘

Key Domain Types

Type	Module	Purpose
EnergyBudget	Types.idr	Per-function energy limit in joules with satisfiability proof
CarbonIntensity	Types.idr	gCO2/kWh from grid API, indexed by zone
JouleAnnotation	Types.idr	Type-level energy annotation for a function
ResourceBound	Types.idr	Composite bound (energy + carbon + time memory)
SustainabilityReport	Types.idr	Aggregated metrics with CSRD field mapping
EnergyMeasurement	Layout.idr	C-compatible struct for hardware counter readings
CarbonQuery	Layout.idr	C-compatible struct for carbon API request/response

Integration Points

• iseriser — meta-framework that generated this scaffold

• proven — shared Idris2 verification primitives

• typell — type theory engine for constraint solving

• PanLL — real-time energy dashboard panel

• BoJ-server — remote energy analysis cartridge

• VeriSimDB — historical energy measurement storage

• WattTime / Electricity Maps — external carbon intensity APIs