Skip to content

Commit b67f59e

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 2: prove cost conservation (additivity) + budget compliance — flagship Idris2 proof (#32)
## Summary Raises eclexiaiser's Idris2 ABI to **Layer 2** with its first flagship semantic proof. eclexiaiser's headline is adding energy/carbon/resource-cost awareness; the foundational guarantee is that accounting **conserves** cost. This proves `additivity` (`totalCost (xs ++ ys) = totalCost xs + totalCost ys`, by induction) — accounting neither loses nor invents cost — plus `WithinBudget` budget compliance as a decidable proposition. Mirrors the estate flagship-proof pattern: ledger model, the conservation equality, sound+complete `Dec`, certifier proven sound, positive + negative controls. ## Changes - Adds `src/interface/abi/Eclexiaiser/ABI/Semantics.idr` — `totalCost`, `additivity`, `WithinBudget`/`decWithinBudget`, `certifyBudgetSound`, and negative control `certifyOverRejects`. - Registers the module in `eclexiaiser-abi.ipkg`. ## RSR Quality Checklist ### Required - [x] Tests pass — ABI builds clean (see Testing) - [x] Linter clean — zero warnings - [x] No banned language patterns - [x] No banned functions — genuine proof - [x] SPDX headers present - [x] No secrets ### As Applicable - [x] ABI/FFI changes validated — additive proof; FFI untouched ## Testing Verified with **Idris2 0.7.0**: `idris2 --build eclexiaiser-abi.ipkg` → exit 0, zero warnings. **Adversarial check**: a deliberately-false proof (accepting an over-budget ledger) was rejected. `build/` removed. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- _Generated by [Claude Code](https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent b1d4db5 commit b67f59e

2 files changed

Lines changed: 109 additions & 0 deletions

File tree

‎src/interface/abi/Eclexiaiser/ABI/Semantics.idr‎

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,108 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
||| Flagship semantic proof for Eclexiaiser (Idris2 ABI Layer 2).
5+
|||
6+
||| Eclexiaiser's headline is "add energy/carbon/resource-cost awareness". The
7+
||| foundational guarantee of any cost-accounting layer is that accounting
8+
||| *conserves* cost — the cost of a composite computation is exactly the sum of
9+
||| its parts, so the accounting can neither lose nor invent cost. This module
10+
||| proves:
11+
|||
12+
||| 1. `additivity` — totalCost (xs ++ ys) = totalCost xs + totalCost ys, by
13+
||| induction (the conservation law);
14+
||| 2. `WithinBudget` — budget compliance as a decidable proposition with a
15+
||| sound+complete `Dec`, a certifier proven sound, and positive + negative
16+
||| controls (an over-budget ledger is provably rejected).
17+
18+
module Eclexiaiser.ABI.Semantics
19+
20+
import Eclexiaiser.ABI.Types
21+
import Data.Nat
22+
import Decidable.Equality
23+
24+
%default total
25+
26+
--------------------------------------------------------------------------------
27+
-- A cost ledger and its total
28+
--------------------------------------------------------------------------------
29+
30+
||| A ledger of per-step resource costs.
31+
public export
32+
Ledger : Type
33+
Ledger = List Nat
34+
35+
public export
36+
totalCost : Ledger -> Nat
37+
totalCost [] = 0
38+
totalCost (c :: cs) = c + totalCost cs
39+
40+
--------------------------------------------------------------------------------
41+
-- Conservation: cost is additive over composition
42+
--------------------------------------------------------------------------------
43+
44+
||| The conservation law: the cost of concatenated work equals the sum of the
45+
||| costs — accounting neither loses nor invents resource cost.
46+
export
47+
additivity : (xs, ys : Ledger) -> totalCost (xs ++ ys) = totalCost xs + totalCost ys
48+
additivity [] ys = Refl
49+
additivity (x :: xs) ys =
50+
trans (cong (x +) (additivity xs ys))
51+
(plusAssociative x (totalCost xs) (totalCost ys))
52+
53+
--------------------------------------------------------------------------------
54+
-- Budget compliance as a decidable proposition
55+
--------------------------------------------------------------------------------
56+
57+
public export
58+
data WithinBudget : (budget : Nat) -> Ledger -> Type where
59+
Within : {0 b : Nat} -> {0 l : Ledger} -> LTE (totalCost l) b -> WithinBudget b l
60+
61+
public export
62+
decWithinBudget : (b : Nat) -> (l : Ledger) -> Dec (WithinBudget b l)
63+
decWithinBudget b l = case isLTE (totalCost l) b of
64+
Yes prf => Yes (Within prf)
65+
No no => No (\(Within p) => no p)
66+
67+
--------------------------------------------------------------------------------
68+
-- Certifier into the ABI Result, proven sound
69+
--------------------------------------------------------------------------------
70+
71+
public export
72+
certifyBudget : Nat -> Ledger -> Result
73+
certifyBudget b l = case decWithinBudget b l of
74+
Yes _ => Ok
75+
No _ => Error
76+
77+
export
78+
certifyBudgetSound : (b : Nat) -> (l : Ledger) ->
79+
certifyBudget b l = Ok -> WithinBudget b l
80+
certifyBudgetSound b l prf with (decWithinBudget b l)
81+
certifyBudgetSound b l prf | Yes w = w
82+
certifyBudgetSound b l Refl | No _ impossible
83+
84+
--------------------------------------------------------------------------------
85+
-- Positive controls
86+
--------------------------------------------------------------------------------
87+
88+
||| Conservation holds on a concrete split.
89+
export
90+
splitConserves : totalCost ([3, 4] ++ [5]) = totalCost [3, 4] + totalCost [5]
91+
splitConserves = additivity [3, 4] [5]
92+
93+
export
94+
certifyWithinAccepts : certifyBudget 10 [3, 4] = Ok
95+
certifyWithinAccepts = Refl
96+
97+
||| A genuine `WithinBudget` witness, derived from the sound certifier.
98+
export
99+
withinEx : WithinBudget 10 [3, 4]
100+
withinEx = certifyBudgetSound 10 [3, 4] certifyWithinAccepts
101+
102+
--------------------------------------------------------------------------------
103+
-- Negative control: an over-budget ledger is rejected (non-vacuity)
104+
--------------------------------------------------------------------------------
105+
106+
export
107+
certifyOverRejects : certifyBudget 5 [3, 4] = Error
108+
certifyOverRejects = Refl

‎src/interface/abi/eclexiaiser-abi.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,3 +7,4 @@ modules = Eclexiaiser.ABI.Types
77
, Eclexiaiser.ABI.Layout
88
, Eclexiaiser.ABI.Foreign
99
, Eclexiaiser.ABI.Proofs
10+
, Eclexiaiser.ABI.Semantics

0 commit comments

Comments
 (0)