From e938d0d1d61d5f8833d2432dba79382e10a5e02d Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 21:52:54 +0000 Subject: [PATCH 1/2] 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 From e0782edbaf1594e38af1eef96f2975a0da727107 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 22:49:59 +0000 Subject: [PATCH 2/2] feat(abi): add Layer-3 monotonicity invariants over the cost model MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add Eclexiaiser.ABI.Invariants, a second, deeper machine-checked theorem distinct from the Layer-2 conservation (additivity) proof. Reuses the existing Semantics model (Ledger, totalCost, WithinBudget) without redefining datatypes, and proves the ordering structure of cost accounting: - prefixMonotone / costMonotoneAppend: appending work never decreases total cost (an LTE inequality, derived via additivity + lteAddRight) — not the Layer-2 equality. - budgetWeakening: budget compliance is downward-closed in the budget (WithinBudget b l -> LTE b b2 -> WithinBudget b2 l), via hand-proven LTE transitivity. - decBudgetLE: sound+complete decision for the ordering side condition. - Positive controls (concrete monotone step, prefix split, weakened witness) plus non-vacuity controls (Not on a false equality and on a false ordering), all machine-checked. Builds with exit 0 and zero warnings; adversarial false-statement checks are rejected by the type-checker. Registered last in the .ipkg. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Eclexiaiser/ABI/Invariants.idr | 140 ++++++++++++++++++ src/interface/abi/eclexiaiser-abi.ipkg | 1 + 2 files changed, 141 insertions(+) create mode 100644 src/interface/abi/Eclexiaiser/ABI/Invariants.idr diff --git a/src/interface/abi/Eclexiaiser/ABI/Invariants.idr b/src/interface/abi/Eclexiaiser/ABI/Invariants.idr new file mode 100644 index 0000000..c4ae512 --- /dev/null +++ b/src/interface/abi/Eclexiaiser/ABI/Invariants.idr @@ -0,0 +1,140 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Monotonicity invariants for Eclexiaiser (Idris2 ABI Layer 3). +||| +||| Layer 2 (`Eclexiaiser.ABI.Semantics`) proved *conservation*: cost is exactly +||| additive over composition (an equality). This module proves the deeper, +||| distinct *ordering* structure of cost accounting — monotonicity and the +||| downward-closure of budget compliance — reusing the Layer-2 model +||| (`Ledger`, `totalCost`, `WithinBudget`) without redefining any datatype: +||| +||| 1. `costMonotoneAppend` — appending a step never DECREASES total cost: +||| LTE (totalCost xs) (totalCost (xs ++ [c])). +||| This is an inequality, not the Layer-2 equality, and is the core +||| monotonicity guarantee: instrumentation can only ever add cost. +||| +||| 2. `prefixMonotone` — any prefix is no more costly than the whole ledger: +||| LTE (totalCost xs) (totalCost (xs ++ ys)). +||| The general monotonicity law of which (1) is the singleton case. +||| +||| 3. `budgetWeakening` — budget compliance is downward-closed in the budget: +||| WithinBudget b l -> LTE b b2 -> WithinBudget b2 l. +||| A larger budget can never reject a ledger a smaller one accepted; this +||| uses LTE transitivity over the Layer-2 `WithinBudget` proposition. +||| +||| 4. `decBudgetLE` — a sound+complete decision for the budget-ordering side +||| condition (LTE on Nat), so the weakening lemma is mechanically usable. +||| +||| Controls: a POSITIVE inhabited witness (monotone step on a concrete ledger, +||| and a weakened budget witness), plus a NEGATIVE / non-vacuity control +||| (`appendStrictlyIncreasesNotEq`: a `Not` proof that a non-zero step makes the +||| totals differ, ruling out the vacuous "cost never changes" reading; and a +||| `Not (LTE ...)` showing weakening genuinely needs the ordering side condition). + +module Eclexiaiser.ABI.Invariants + +import Eclexiaiser.ABI.Types +import Eclexiaiser.ABI.Semantics +import Data.Nat + +%default total + +-------------------------------------------------------------------------------- +-- 1. Monotonicity: appending a step never decreases total cost +-------------------------------------------------------------------------------- + +||| The general monotonicity law: the cost of a prefix is no greater than the +||| cost of the whole. Proven by rewriting through Layer-2 conservation +||| (`additivity`) and then observing `n <= n + m`. +export +prefixMonotone : (xs, ys : Ledger) -> + LTE (totalCost xs) (totalCost (xs ++ ys)) +prefixMonotone xs ys = + rewrite additivity xs ys in + lteAddRight (totalCost xs) + +||| Appending a single step never decreases the total cost — the singleton +||| instance of `prefixMonotone`. Instrumentation can only add cost. +export +costMonotoneAppend : (xs : Ledger) -> (c : Nat) -> + LTE (totalCost xs) (totalCost (xs ++ [c])) +costMonotoneAppend xs c = prefixMonotone xs [c] + +-------------------------------------------------------------------------------- +-- 2. A sound+complete decision for the budget-ordering side condition +-------------------------------------------------------------------------------- + +||| Decide the budget-ordering side condition used by weakening. `isLTE` from +||| Data.Nat is already sound+complete; we expose it under a domain name. +export +decBudgetLE : (b, b2 : Nat) -> Dec (LTE b b2) +decBudgetLE = isLTE + +-------------------------------------------------------------------------------- +-- 3. Downward-closure: a larger budget still admits a compliant ledger +-------------------------------------------------------------------------------- + +||| Budget compliance is downward-closed in the budget: if a ledger fits within +||| `b`, and `b <= b2`, then it fits within `b2`. This is *not* the Layer-2 +||| conservation law; it is a structural property of `WithinBudget` proven by +||| transitivity of LTE. +||| Concrete transitivity of LTE, hand-proven so it does not depend on the +||| `Transitive` interface method (whose implicits are runtime-relevant and so +||| clash with the erased budget/ledger arguments here). +lteTrans : {0 x, y, z : Nat} -> LTE x y -> LTE y z -> LTE x z +lteTrans LTEZero _ = LTEZero +lteTrans (LTESucc p) (LTESucc q) = LTESucc (lteTrans p q) + +export +budgetWeakening : {0 b : Nat} -> {0 b2 : Nat} -> {0 l : Ledger} -> + WithinBudget b l -> LTE b b2 -> WithinBudget b2 l +budgetWeakening (Within prf) ble = Within (lteTrans prf ble) + +-------------------------------------------------------------------------------- +-- 4. Positive controls +-------------------------------------------------------------------------------- + +||| Concrete monotone step: cost of [3,4] (= 7) is <= cost of [3,4,5] (= 12). +export +monotoneStepEx : LTE (totalCost [3, 4]) (totalCost ([3, 4] ++ [5])) +monotoneStepEx = costMonotoneAppend [3, 4] 5 + +||| Concrete prefix monotonicity on a split. +export +prefixMonotoneEx : LTE (totalCost [3, 4]) (totalCost ([3, 4] ++ [5, 6])) +prefixMonotoneEx = prefixMonotone [3, 4] [5, 6] + +||| Weakening a budget keeps an accepted ledger accepted: `withinEx` is within +||| 10; since 10 <= 20, it is within 20. The side condition `LTE 10 20` is +||| obtained from the sound+complete decision procedure (no hand-built proof). +export +weakenedWitness : WithinBudget 20 [3, 4] +weakenedWitness = + case decBudgetLE 10 20 of + Yes le => budgetWeakening withinEx le + No contra => absurd (contra (lteAddRight 10)) + +-------------------------------------------------------------------------------- +-- 5. Negative / non-vacuity controls +-------------------------------------------------------------------------------- + +||| Non-vacuity of monotonicity: with a *non-zero* step the totals genuinely +||| DIFFER, so `costMonotoneAppend` is a real strict-increase witness and not the +||| vacuous "cost is unchanged". Both sides reduce to constructor-headed Nats +||| (12 vs 7), so the equality is refuted by a top-level `impossible` clause. +export +appendStrictlyIncreasesNotEq : + Not (totalCost ([3, 4] ++ [5]) = totalCost [3, 4]) +appendStrictlyIncreasesNotEq Refl impossible + +||| Non-vacuity of the weakening side condition: weakening genuinely *requires* +||| `b <= b2`. Here the ordering it would need (20 <= 10) does NOT hold, so the +||| lemma could not have been applied in this direction. Machine-checked `Not`. +export +weakeningNeedsOrder : Not (LTE 20 10) +weakeningNeedsOrder le = absurd (notLTE le) + where + notLTE : LTE 20 10 -> Void + notLTE (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc x)))))))))) + = absurd x diff --git a/src/interface/abi/eclexiaiser-abi.ipkg b/src/interface/abi/eclexiaiser-abi.ipkg index dd3be55..8b44efe 100644 --- a/src/interface/abi/eclexiaiser-abi.ipkg +++ b/src/interface/abi/eclexiaiser-abi.ipkg @@ -8,3 +8,4 @@ modules = Eclexiaiser.ABI.Types , Eclexiaiser.ABI.Foreign , Eclexiaiser.ABI.Proofs , Eclexiaiser.ABI.Semantics + , Eclexiaiser.ABI.Invariants