From e938d0d1d61d5f8833d2432dba79382e10a5e02d Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 21:52:54 +0000 Subject: [PATCH] abi: prove cost-conservation (additivity) + budget compliance (Layer 2) Flagship semantic proof: totalCost (xs ++ ys) = totalCost xs + totalCost ys (conservation, by induction), plus a decidable WithinBudget proposition with sound+complete Dec, certifier soundness, and positive + negative controls (an over-budget ledger is provably rejected). Verified with idris2 0.7.0 (build clean, zero warnings) + adversarial rejection. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Eclexiaiser/ABI/Semantics.idr | 108 ++++++++++++++++++ src/interface/abi/eclexiaiser-abi.ipkg | 1 + 2 files changed, 109 insertions(+) create mode 100644 src/interface/abi/Eclexiaiser/ABI/Semantics.idr diff --git a/src/interface/abi/Eclexiaiser/ABI/Semantics.idr b/src/interface/abi/Eclexiaiser/ABI/Semantics.idr new file mode 100644 index 0000000..86e0e30 --- /dev/null +++ b/src/interface/abi/Eclexiaiser/ABI/Semantics.idr @@ -0,0 +1,108 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Flagship semantic proof for Eclexiaiser (Idris2 ABI Layer 2). +||| +||| Eclexiaiser's headline is "add energy/carbon/resource-cost awareness". The +||| foundational guarantee of any cost-accounting layer is that accounting +||| *conserves* cost — the cost of a composite computation is exactly the sum of +||| its parts, so the accounting can neither lose nor invent cost. This module +||| proves: +||| +||| 1. `additivity` — totalCost (xs ++ ys) = totalCost xs + totalCost ys, by +||| induction (the conservation law); +||| 2. `WithinBudget` — budget compliance as a decidable proposition with a +||| sound+complete `Dec`, a certifier proven sound, and positive + negative +||| controls (an over-budget ledger is provably rejected). + +module Eclexiaiser.ABI.Semantics + +import Eclexiaiser.ABI.Types +import Data.Nat +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- A cost ledger and its total +-------------------------------------------------------------------------------- + +||| A ledger of per-step resource costs. +public export +Ledger : Type +Ledger = List Nat + +public export +totalCost : Ledger -> Nat +totalCost [] = 0 +totalCost (c :: cs) = c + totalCost cs + +-------------------------------------------------------------------------------- +-- Conservation: cost is additive over composition +-------------------------------------------------------------------------------- + +||| The conservation law: the cost of concatenated work equals the sum of the +||| costs — accounting neither loses nor invents resource cost. +export +additivity : (xs, ys : Ledger) -> totalCost (xs ++ ys) = totalCost xs + totalCost ys +additivity [] ys = Refl +additivity (x :: xs) ys = + trans (cong (x +) (additivity xs ys)) + (plusAssociative x (totalCost xs) (totalCost ys)) + +-------------------------------------------------------------------------------- +-- Budget compliance as a decidable proposition +-------------------------------------------------------------------------------- + +public export +data WithinBudget : (budget : Nat) -> Ledger -> Type where + Within : {0 b : Nat} -> {0 l : Ledger} -> LTE (totalCost l) b -> WithinBudget b l + +public export +decWithinBudget : (b : Nat) -> (l : Ledger) -> Dec (WithinBudget b l) +decWithinBudget b l = case isLTE (totalCost l) b of + Yes prf => Yes (Within prf) + No no => No (\(Within p) => no p) + +-------------------------------------------------------------------------------- +-- Certifier into the ABI Result, proven sound +-------------------------------------------------------------------------------- + +public export +certifyBudget : Nat -> Ledger -> Result +certifyBudget b l = case decWithinBudget b l of + Yes _ => Ok + No _ => Error + +export +certifyBudgetSound : (b : Nat) -> (l : Ledger) -> + certifyBudget b l = Ok -> WithinBudget b l +certifyBudgetSound b l prf with (decWithinBudget b l) + certifyBudgetSound b l prf | Yes w = w + certifyBudgetSound b l Refl | No _ impossible + +-------------------------------------------------------------------------------- +-- Positive controls +-------------------------------------------------------------------------------- + +||| Conservation holds on a concrete split. +export +splitConserves : totalCost ([3, 4] ++ [5]) = totalCost [3, 4] + totalCost [5] +splitConserves = additivity [3, 4] [5] + +export +certifyWithinAccepts : certifyBudget 10 [3, 4] = Ok +certifyWithinAccepts = Refl + +||| A genuine `WithinBudget` witness, derived from the sound certifier. +export +withinEx : WithinBudget 10 [3, 4] +withinEx = certifyBudgetSound 10 [3, 4] certifyWithinAccepts + +-------------------------------------------------------------------------------- +-- Negative control: an over-budget ledger is rejected (non-vacuity) +-------------------------------------------------------------------------------- + +export +certifyOverRejects : certifyBudget 5 [3, 4] = Error +certifyOverRejects = Refl diff --git a/src/interface/abi/eclexiaiser-abi.ipkg b/src/interface/abi/eclexiaiser-abi.ipkg index 713ac82..dd3be55 100644 --- a/src/interface/abi/eclexiaiser-abi.ipkg +++ b/src/interface/abi/eclexiaiser-abi.ipkg @@ -7,3 +7,4 @@ modules = Eclexiaiser.ABI.Types , Eclexiaiser.ABI.Layout , Eclexiaiser.ABI.Foreign , Eclexiaiser.ABI.Proofs + , Eclexiaiser.ABI.Semantics