Skip to content

Commit 7274b8f

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 3: monotonicity of cost accounting + downward-closed budget (#33)
## Summary Layer 3 (second, deeper invariant): proves **monotonicity** of cost accounting — `prefixMonotone` (a prefix never costs more than the whole) — and that budget compliance is **downward-closed** (within budget B ⇒ within any B′≥B). Distinct from and deeper than the Layer-2 additivity equality. New module `Eclexiaiser.ABI.Invariants` (imports the Layer-2 `Semantics` model). Positive + non-vacuity controls. ## Testing Idris2 0.7.0 `--build` → exit 0, zero warnings. Adversarial rejection confirmed. `build/` removed. No `believe_me`/`postulate`/`sorry`. 🤖 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)_ --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>
1 parent b67f59e commit 7274b8f

2 files changed

Lines changed: 141 additions & 0 deletions

File tree

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

Lines changed: 140 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,140 @@
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+
||| Monotonicity invariants for Eclexiaiser (Idris2 ABI Layer 3).
5+
|||
6+
||| Layer 2 (`Eclexiaiser.ABI.Semantics`) proved *conservation*: cost is exactly
7+
||| additive over composition (an equality). This module proves the deeper,
8+
||| distinct *ordering* structure of cost accounting — monotonicity and the
9+
||| downward-closure of budget compliance — reusing the Layer-2 model
10+
||| (`Ledger`, `totalCost`, `WithinBudget`) without redefining any datatype:
11+
|||
12+
||| 1. `costMonotoneAppend` — appending a step never DECREASES total cost:
13+
||| LTE (totalCost xs) (totalCost (xs ++ [c])).
14+
||| This is an inequality, not the Layer-2 equality, and is the core
15+
||| monotonicity guarantee: instrumentation can only ever add cost.
16+
|||
17+
||| 2. `prefixMonotone` — any prefix is no more costly than the whole ledger:
18+
||| LTE (totalCost xs) (totalCost (xs ++ ys)).
19+
||| The general monotonicity law of which (1) is the singleton case.
20+
|||
21+
||| 3. `budgetWeakening` — budget compliance is downward-closed in the budget:
22+
||| WithinBudget b l -> LTE b b2 -> WithinBudget b2 l.
23+
||| A larger budget can never reject a ledger a smaller one accepted; this
24+
||| uses LTE transitivity over the Layer-2 `WithinBudget` proposition.
25+
|||
26+
||| 4. `decBudgetLE` — a sound+complete decision for the budget-ordering side
27+
||| condition (LTE on Nat), so the weakening lemma is mechanically usable.
28+
|||
29+
||| Controls: a POSITIVE inhabited witness (monotone step on a concrete ledger,
30+
||| and a weakened budget witness), plus a NEGATIVE / non-vacuity control
31+
||| (`appendStrictlyIncreasesNotEq`: a `Not` proof that a non-zero step makes the
32+
||| totals differ, ruling out the vacuous "cost never changes" reading; and a
33+
||| `Not (LTE ...)` showing weakening genuinely needs the ordering side condition).
34+
35+
module Eclexiaiser.ABI.Invariants
36+
37+
import Eclexiaiser.ABI.Types
38+
import Eclexiaiser.ABI.Semantics
39+
import Data.Nat
40+
41+
%default total
42+
43+
--------------------------------------------------------------------------------
44+
-- 1. Monotonicity: appending a step never decreases total cost
45+
--------------------------------------------------------------------------------
46+
47+
||| The general monotonicity law: the cost of a prefix is no greater than the
48+
||| cost of the whole. Proven by rewriting through Layer-2 conservation
49+
||| (`additivity`) and then observing `n <= n + m`.
50+
export
51+
prefixMonotone : (xs, ys : Ledger) ->
52+
LTE (totalCost xs) (totalCost (xs ++ ys))
53+
prefixMonotone xs ys =
54+
rewrite additivity xs ys in
55+
lteAddRight (totalCost xs)
56+
57+
||| Appending a single step never decreases the total cost — the singleton
58+
||| instance of `prefixMonotone`. Instrumentation can only add cost.
59+
export
60+
costMonotoneAppend : (xs : Ledger) -> (c : Nat) ->
61+
LTE (totalCost xs) (totalCost (xs ++ [c]))
62+
costMonotoneAppend xs c = prefixMonotone xs [c]
63+
64+
--------------------------------------------------------------------------------
65+
-- 2. A sound+complete decision for the budget-ordering side condition
66+
--------------------------------------------------------------------------------
67+
68+
||| Decide the budget-ordering side condition used by weakening. `isLTE` from
69+
||| Data.Nat is already sound+complete; we expose it under a domain name.
70+
export
71+
decBudgetLE : (b, b2 : Nat) -> Dec (LTE b b2)
72+
decBudgetLE = isLTE
73+
74+
--------------------------------------------------------------------------------
75+
-- 3. Downward-closure: a larger budget still admits a compliant ledger
76+
--------------------------------------------------------------------------------
77+
78+
||| Budget compliance is downward-closed in the budget: if a ledger fits within
79+
||| `b`, and `b <= b2`, then it fits within `b2`. This is *not* the Layer-2
80+
||| conservation law; it is a structural property of `WithinBudget` proven by
81+
||| transitivity of LTE.
82+
||| Concrete transitivity of LTE, hand-proven so it does not depend on the
83+
||| `Transitive` interface method (whose implicits are runtime-relevant and so
84+
||| clash with the erased budget/ledger arguments here).
85+
lteTrans : {0 x, y, z : Nat} -> LTE x y -> LTE y z -> LTE x z
86+
lteTrans LTEZero _ = LTEZero
87+
lteTrans (LTESucc p) (LTESucc q) = LTESucc (lteTrans p q)
88+
89+
export
90+
budgetWeakening : {0 b : Nat} -> {0 b2 : Nat} -> {0 l : Ledger} ->
91+
WithinBudget b l -> LTE b b2 -> WithinBudget b2 l
92+
budgetWeakening (Within prf) ble = Within (lteTrans prf ble)
93+
94+
--------------------------------------------------------------------------------
95+
-- 4. Positive controls
96+
--------------------------------------------------------------------------------
97+
98+
||| Concrete monotone step: cost of [3,4] (= 7) is <= cost of [3,4,5] (= 12).
99+
export
100+
monotoneStepEx : LTE (totalCost [3, 4]) (totalCost ([3, 4] ++ [5]))
101+
monotoneStepEx = costMonotoneAppend [3, 4] 5
102+
103+
||| Concrete prefix monotonicity on a split.
104+
export
105+
prefixMonotoneEx : LTE (totalCost [3, 4]) (totalCost ([3, 4] ++ [5, 6]))
106+
prefixMonotoneEx = prefixMonotone [3, 4] [5, 6]
107+
108+
||| Weakening a budget keeps an accepted ledger accepted: `withinEx` is within
109+
||| 10; since 10 <= 20, it is within 20. The side condition `LTE 10 20` is
110+
||| obtained from the sound+complete decision procedure (no hand-built proof).
111+
export
112+
weakenedWitness : WithinBudget 20 [3, 4]
113+
weakenedWitness =
114+
case decBudgetLE 10 20 of
115+
Yes le => budgetWeakening withinEx le
116+
No contra => absurd (contra (lteAddRight 10))
117+
118+
--------------------------------------------------------------------------------
119+
-- 5. Negative / non-vacuity controls
120+
--------------------------------------------------------------------------------
121+
122+
||| Non-vacuity of monotonicity: with a *non-zero* step the totals genuinely
123+
||| DIFFER, so `costMonotoneAppend` is a real strict-increase witness and not the
124+
||| vacuous "cost is unchanged". Both sides reduce to constructor-headed Nats
125+
||| (12 vs 7), so the equality is refuted by a top-level `impossible` clause.
126+
export
127+
appendStrictlyIncreasesNotEq :
128+
Not (totalCost ([3, 4] ++ [5]) = totalCost [3, 4])
129+
appendStrictlyIncreasesNotEq Refl impossible
130+
131+
||| Non-vacuity of the weakening side condition: weakening genuinely *requires*
132+
||| `b <= b2`. Here the ordering it would need (20 <= 10) does NOT hold, so the
133+
||| lemma could not have been applied in this direction. Machine-checked `Not`.
134+
export
135+
weakeningNeedsOrder : Not (LTE 20 10)
136+
weakeningNeedsOrder le = absurd (notLTE le)
137+
where
138+
notLTE : LTE 20 10 -> Void
139+
notLTE (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc x))))))))))
140+
= absurd x

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,4 @@ modules = Eclexiaiser.ABI.Types
88
, Eclexiaiser.ABI.Foreign
99
, Eclexiaiser.ABI.Proofs
1010
, Eclexiaiser.ABI.Semantics
11+
, Eclexiaiser.ABI.Invariants

0 commit comments

Comments
 (0)