Skip to content

Commit 62dc8d3

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 3: conjunction-of-contracts law (#47)
* Add Layer 2 semantic proof: configs self-validate against K9 contracts New module K9iser.ABI.Semantics proves the repo's headline property ("Wrap configs into self-validating K9 contracts"): a config that SATISFIES a "must"-contract (a required key present whose value lies within an inclusive numeric range) provably validates, and a config that VIOLATES it (missing key OR out-of-range value) provably does not. - Faithful model: Config = assoc list (Key, Nat); Contract = key + [lo,hi]. - Headline proposition `Validates c cfg` has constructors only for the satisfying case (resolver equation + InRange via propositional LTE); no constructor exists for a missing key or out-of-range value. - Sound + complete `decValidates : Dec (Validates c cfg)` and `decInRange`. - Certifier `certify` into the ABI Result code, with `certifySound` and `certifyComplete`. - Positive control `goodValidates` (replicas=5 in [1,10]) and two negative controls: `badRangeNotValidates` (replicas=0) and `missingNotValidates`. ABI builds clean (exit 0, zero warnings). A deliberately false witness for the out-of-range config is rejected by idris2 (non-vacuity verified). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * abi: Layer-3 conjunction-of-contracts law (K9iser.ABI.Invariants) Add a second, deeper machine-checked theorem over the existing Layer-2 Semantics model, raising the Idris2 ABI to Layer 3. Proves how config validation behaves under CONJUNCTION of K9 contracts, distinct from the Layer-2 single-contract soundness/completeness: - ValidatesBoth / ValidatesAll: binary and n-ary conjunction over the existing Validates proposition. - validatesAndIff / validatesAllConsIff: decomposition isomorphisms (real witness round-trips, = Refl). - validatesBothSym: commutativity of conjunction. - decValidatesAll: sound + complete decision, built compositionally from the Layer-2 decValidates. - validatesAllAppend{Fwd,Bwd}: distribution of conjunction over list append (induction on the bundle). - validatesAllWeaken: monotonicity / downward-closure. - certifyAll{,Sound,Complete}: certifier into the ABI Result code. - Positive controls (twoValidatesBoth / twoValidatesBundle) and negative / non-vacuity controls (mixedNotBoth / mixedNotBundle), all machine-checked; resolver equations proved via resolveHead / resolveSkip lemmas (String decEq does not reduce definitionally). No believe_me / postulate / assert_total / sorry. %default total. Registered last in k9iser-abi.ipkg. Clean build, zero warnings; a deliberately-false ValidatesAll over the out-of-range config is rejected by the type checker (non-vacuity confirmed). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 7dddd86 commit 62dc8d3

2 files changed

Lines changed: 355 additions & 0 deletions

File tree

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

Lines changed: 354 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,354 @@
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+
||| Layer-3 deepening proof for k9iser: the CONJUNCTION-OF-CONTRACTS law.
5+
|||
6+
||| The Layer-2 flagship (`K9iser.ABI.Semantics`) proves the soundness and
7+
||| completeness of validating a config against a SINGLE K9 "must"-contract.
8+
||| This module proves a genuinely different, deeper, algebraic property of the
9+
||| SAME model: how validation behaves under CONJUNCTION of contracts.
10+
|||
11+
||| A config is a self-validating K9 contract; in practice a contract is a
12+
||| *bundle* of must-rules, so the central question is compositional: does
13+
||| validating a conjoined bundle decompose into validating each conjunct?
14+
|||
15+
||| Headline theorems (over the EXISTING `Validates` from Semantics):
16+
||| * `validatesAndIff` — a config validates `c1 AND c2` IFF it validates c1
17+
||| AND validates c2 (both directions, as a real iso of
18+
||| witnesses, not a boolean tautology).
19+
||| * `validatesAllConsIff` — the n-ary version: validating `(c :: cs)`
20+
||| decomposes into the head and the tail.
21+
||| * `decValidatesAll` — a sound + COMPLETE decision for the n-ary form,
22+
||| built compositionally from the Layer-2 decision.
23+
||| * `validatesAllAppend` — DISTRIBUTION of conjunction over list append:
24+
||| validating `xs ++ ys` IFF validating xs and ys.
25+
||| * `validatesAllWeaken` — MONOTONICITY / downward-closure: a config that
26+
||| validates a bundle validates every sub-bundle
27+
||| reachable by dropping a contract (here: the tail).
28+
|||
29+
||| Plus a positive control (an inhabited witness for a concrete two-contract
30+
||| bundle) and a negative / non-vacuity control (`Not (...)`).
31+
32+
module K9iser.ABI.Invariants
33+
34+
import K9iser.ABI.Types
35+
import K9iser.ABI.Semantics
36+
import Data.Nat
37+
import Decidable.Equality
38+
import Decidable.Decidable
39+
40+
%default total
41+
42+
--------------------------------------------------------------------------------
43+
-- Local helpers. The model's `resolve` keys on `String`, whose `decEq` does NOT
44+
-- reduce definitionally (idiom 5), so `resolve k cfg = Just v` cannot be proved
45+
-- by bare `Refl` outside the defining module. We instead prove the two resolver
46+
-- steps as genuine lemmas (`with (decEq ...)`), and build range witnesses by
47+
-- reducing the public `decInRange` (which DOES reduce on concrete Nats).
48+
--------------------------------------------------------------------------------
49+
50+
||| Constructor-headed injectivity of `Just` (idiom 3), to transport a resolved
51+
||| equation at the term level in the negative control.
52+
jInj : {0 x, y : a} -> Just x = Just y -> x = y
53+
jInj Refl = Refl
54+
55+
||| The required key sits at the head: `resolve` returns its value. Proved by
56+
||| `with (decEq k k)`, discharging the impossible `No` branch with reflexivity.
57+
resolveHead : (k : Key) -> (v : Nat) -> (rest : Config) ->
58+
resolve k ((k, v) :: rest) = Just v
59+
resolveHead k v rest with (decEq k k)
60+
resolveHead k v rest | Yes _ = Refl
61+
resolveHead k v rest | No contra = absurd (contra Refl)
62+
63+
||| A distinct head key is skipped: `resolve` recurses into the tail. Proved by
64+
||| `with (decEq k k')`, discharging the impossible `Yes` branch via the
65+
||| supplied disequality.
66+
resolveSkip : (k, k' : Key) -> Not (k = k') -> (v' : Nat) -> (rest : Config) ->
67+
resolve k ((k', v') :: rest) = resolve k rest
68+
resolveSkip k k' neq v' rest with (decEq k k')
69+
resolveSkip k k' neq v' rest | Yes eq = absurd (neq eq)
70+
resolveSkip k k' neq v' rest | No _ = Refl
71+
72+
||| Build an `InRange` witness on CONCRETE operands by reducing the public
73+
||| `decInRange` (which reduces fully on concrete Nats, unlike a `with`-block on
74+
||| `String`). The `{auto}` `IsYes` proof forces the reduction to `Yes` at
75+
||| type-check time, so this is a genuine machine-checked witness — not proof
76+
||| search, not a postulate.
77+
inRangeWit : (low, high, val : Nat) ->
78+
{auto 0 ok : IsYes (decInRange low high val)} ->
79+
InRange low high val
80+
inRangeWit low high val {ok} with (decInRange low high val)
81+
inRangeWit low high val {ok = ItIsYes} | Yes prf = prf
82+
83+
--------------------------------------------------------------------------------
84+
-- Binary conjunction of contracts
85+
--------------------------------------------------------------------------------
86+
87+
||| Conjunction of two contract-validations against the SAME config. This is a
88+
||| genuine product of Layer-2 witnesses: to inhabit it you must independently
89+
||| prove the config validates c1 and validates c2. It is therefore strictly
90+
||| deeper than the single-contract `Validates`.
91+
public export
92+
data ValidatesBoth : (c1, c2 : Contract) -> (cfg : Config) -> Type where
93+
MkValidatesBoth : Validates c1 cfg ->
94+
Validates c2 cfg ->
95+
ValidatesBoth c1 c2 cfg
96+
97+
||| HEADLINE (binary), forward: validating the conjunction gives both conjuncts.
98+
public export
99+
validatesAndFwd : {0 c1, c2 : Contract} -> {0 cfg : Config} ->
100+
ValidatesBoth c1 c2 cfg ->
101+
(Validates c1 cfg, Validates c2 cfg)
102+
validatesAndFwd (MkValidatesBoth p q) = (p, q)
103+
104+
||| HEADLINE (binary), backward: both conjuncts give the conjunction.
105+
public export
106+
validatesAndBwd : {0 c1, c2 : Contract} -> {0 cfg : Config} ->
107+
(Validates c1 cfg, Validates c2 cfg) ->
108+
ValidatesBoth c1 c2 cfg
109+
validatesAndBwd (p, q) = MkValidatesBoth p q
110+
111+
||| HEADLINE (binary), iso: the two directions compose to the identity on the
112+
||| pair, witnessing that `ValidatesBoth` is exactly the conjunction (no extra
113+
||| or missing information). This `= Refl` is a real round-trip equality.
114+
public export
115+
validatesAndIff : {0 c1, c2 : Contract} -> {0 cfg : Config} ->
116+
(pq : (Validates c1 cfg, Validates c2 cfg)) ->
117+
validatesAndFwd (validatesAndBwd pq) = pq
118+
validatesAndIff (p, q) = Refl
119+
120+
||| COMMUTATIVITY of conjunction: order of conjuncts does not matter.
121+
public export
122+
validatesBothSym : {0 c1, c2 : Contract} -> {0 cfg : Config} ->
123+
ValidatesBoth c1 c2 cfg -> ValidatesBoth c2 c1 cfg
124+
validatesBothSym (MkValidatesBoth p q) = MkValidatesBoth q p
125+
126+
--------------------------------------------------------------------------------
127+
-- N-ary conjunction: validating a whole bundle of contracts
128+
--------------------------------------------------------------------------------
129+
130+
||| A config validates a BUNDLE (list) of contracts iff it validates every one.
131+
||| The empty bundle is vacuously validated; a cons requires the head to be
132+
||| validated and the tail to be validated. This is the inductive conjunction
133+
||| over the Layer-2 `Validates`.
134+
public export
135+
data ValidatesAll : (cfg : Config) -> (cs : List Contract) -> Type where
136+
ValidatesNil : ValidatesAll cfg []
137+
ValidatesCons : Validates c cfg ->
138+
ValidatesAll cfg cs ->
139+
ValidatesAll cfg (c :: cs)
140+
141+
||| HEADLINE (n-ary), forward: validating `(c :: cs)` gives the head and tail.
142+
public export
143+
validatesAllConsFwd : {0 c : Contract} -> {0 cs : List Contract} ->
144+
{0 cfg : Config} ->
145+
ValidatesAll cfg (c :: cs) ->
146+
(Validates c cfg, ValidatesAll cfg cs)
147+
validatesAllConsFwd (ValidatesCons h t) = (h, t)
148+
149+
||| HEADLINE (n-ary), backward: head + tail rebuild the bundle validation.
150+
public export
151+
validatesAllConsBwd : {0 c : Contract} -> {0 cs : List Contract} ->
152+
{0 cfg : Config} ->
153+
(Validates c cfg, ValidatesAll cfg cs) ->
154+
ValidatesAll cfg (c :: cs)
155+
validatesAllConsBwd (h, t) = ValidatesCons h t
156+
157+
||| HEADLINE (n-ary), iso: round-trip on the cons decomposition is the identity.
158+
public export
159+
validatesAllConsIff : {0 c : Contract} -> {0 cs : List Contract} ->
160+
{0 cfg : Config} ->
161+
(ht : (Validates c cfg, ValidatesAll cfg cs)) ->
162+
validatesAllConsFwd (validatesAllConsBwd ht) = ht
163+
validatesAllConsIff (h, t) = Refl
164+
165+
--------------------------------------------------------------------------------
166+
-- Sound + complete decision for the n-ary conjunction
167+
--------------------------------------------------------------------------------
168+
169+
||| There is no `ValidatesAll` witness for a cons whose HEAD fails to validate.
170+
||| Top-level refutation helper (idiom 2/3): peel the cons and discharge the
171+
||| head with the supplied refutation.
172+
headFails : {0 c : Contract} -> {0 cs : List Contract} -> {0 cfg : Config} ->
173+
Not (Validates c cfg) -> Not (ValidatesAll cfg (c :: cs))
174+
headFails noH (ValidatesCons h _) = noH h
175+
176+
||| There is no `ValidatesAll` witness for a cons whose TAIL fails to validate.
177+
tailFails : {0 c : Contract} -> {0 cs : List Contract} -> {0 cfg : Config} ->
178+
Not (ValidatesAll cfg cs) -> Not (ValidatesAll cfg (c :: cs))
179+
tailFails noT (ValidatesCons _ t) = noT t
180+
181+
||| Decide whether a config validates an entire bundle. Built COMPOSITIONALLY
182+
||| from the Layer-2 `decValidates`: this is the deeper structural result, since
183+
||| it threads the single-contract decision through induction on the bundle and
184+
||| stays both sound (a `Yes` is a real witness) and complete (a `No` is a real
185+
||| refutation) at every step.
186+
public export
187+
decValidatesAll : (cfg : Config) -> (cs : List Contract) ->
188+
Dec (ValidatesAll cfg cs)
189+
decValidatesAll cfg [] = Yes ValidatesNil
190+
decValidatesAll cfg (c :: cs) = case decValidates c cfg of
191+
No noH => No (headFails noH)
192+
Yes h => case decValidatesAll cfg cs of
193+
No noT => No (tailFails noT)
194+
Yes t => Yes (ValidatesCons h t)
195+
196+
--------------------------------------------------------------------------------
197+
-- Distribution of conjunction over list append
198+
--------------------------------------------------------------------------------
199+
200+
||| DISTRIBUTION (forward): validating `xs ++ ys` lets you split the validation
201+
||| into the xs-part and the ys-part. Proved by induction on xs.
202+
public export
203+
validatesAllAppendFwd : {0 cfg : Config} -> (xs : List Contract) ->
204+
{0 ys : List Contract} ->
205+
ValidatesAll cfg (xs ++ ys) ->
206+
(ValidatesAll cfg xs, ValidatesAll cfg ys)
207+
validatesAllAppendFwd [] vall = (ValidatesNil, vall)
208+
validatesAllAppendFwd (x :: xs) (ValidatesCons h t) =
209+
let (vxs, vys) = validatesAllAppendFwd xs t in
210+
(ValidatesCons h vxs, vys)
211+
212+
||| DISTRIBUTION (backward): validations of xs and ys recombine into a
213+
||| validation of `xs ++ ys`. Proved by induction on the xs witness.
214+
public export
215+
validatesAllAppendBwd : {0 cfg : Config} ->
216+
{0 xs, ys : List Contract} ->
217+
ValidatesAll cfg xs -> ValidatesAll cfg ys ->
218+
ValidatesAll cfg (xs ++ ys)
219+
validatesAllAppendBwd ValidatesNil vys = vys
220+
validatesAllAppendBwd (ValidatesCons h t) vys =
221+
ValidatesCons h (validatesAllAppendBwd t vys)
222+
223+
--------------------------------------------------------------------------------
224+
-- Monotonicity / downward-closure
225+
--------------------------------------------------------------------------------
226+
227+
||| MONOTONICITY: validating a bundle implies validating its tail (dropping a
228+
||| conjunct can only weaken the requirement). This is the downward-closure
229+
||| direction of the conjunction lattice.
230+
public export
231+
validatesAllWeaken : {0 c : Contract} -> {0 cs : List Contract} ->
232+
{0 cfg : Config} ->
233+
ValidatesAll cfg (c :: cs) -> ValidatesAll cfg cs
234+
validatesAllWeaken (ValidatesCons _ t) = t
235+
236+
--------------------------------------------------------------------------------
237+
-- Certifier for the n-ary conjunction + soundness/completeness into Result
238+
--------------------------------------------------------------------------------
239+
240+
||| Certify a whole bundle into the ABI `Result` code: `Ok` iff every contract
241+
||| validates, `ConstraintViolation` otherwise.
242+
public export
243+
certifyAll : (cfg : Config) -> (cs : List Contract) -> Result
244+
certifyAll cfg cs = case decValidatesAll cfg cs of
245+
Yes _ => Ok
246+
No _ => ConstraintViolation
247+
248+
||| Soundness: a bundle certified `Ok` really validates every contract.
249+
public export
250+
certifyAllSound : (cfg : Config) -> (cs : List Contract) ->
251+
certifyAll cfg cs = Ok -> ValidatesAll cfg cs
252+
certifyAllSound cfg cs prf with (decValidatesAll cfg cs)
253+
certifyAllSound cfg cs prf | Yes ok = ok
254+
certifyAllSound cfg cs Refl | No _ impossible
255+
256+
||| Completeness: if a bundle validates, certification reports `Ok`.
257+
public export
258+
certifyAllComplete : (cfg : Config) -> (cs : List Contract) ->
259+
ValidatesAll cfg cs -> certifyAll cfg cs = Ok
260+
certifyAllComplete cfg cs vall with (decValidatesAll cfg cs)
261+
certifyAllComplete cfg cs vall | Yes _ = Refl
262+
certifyAllComplete cfg cs vall | No bad = absurd (bad vall)
263+
264+
--------------------------------------------------------------------------------
265+
-- Controls (non-vacuity)
266+
--------------------------------------------------------------------------------
267+
268+
||| First concrete contract over the SAME model: key "replicas" in [1, 10].
269+
||| (A literal-key local copy of the Layer-2 contract so the `key` projection
270+
||| reduces inside this module; the bundle below mixes two distinct contracts.)
271+
public export
272+
replicasContract : Contract
273+
replicasContract = MkContract "replicas" 1 10
274+
275+
||| Second concrete contract over the SAME model: key "timeout" in [1, 30].
276+
public export
277+
timeoutContract : Contract
278+
timeoutContract = MkContract "timeout" 1 30
279+
280+
||| A single config carrying both required keys, used for the controls. Each
281+
||| required key is placed so that `resolve` reduces on concrete data.
282+
public export
283+
twoConfig : Config
284+
twoConfig = [("replicas", 5), ("timeout", 20)]
285+
286+
||| `"timeout"` and `"replicas"` are distinct keys (primitive String literals).
287+
neqTimeoutReplicas : Not ("timeout" = "replicas")
288+
neqTimeoutReplicas = \case Refl impossible
289+
290+
||| Witness that `twoConfig` validates the replicas contract. The resolver
291+
||| equation comes from `resolveHead`; `inRangeWit` supplies the machine-checked
292+
||| range proof for 5 in [1, 10].
293+
public export
294+
twoValidatesReplicas : Validates Invariants.replicasContract Invariants.twoConfig
295+
twoValidatesReplicas =
296+
MkValidates 5 (resolveHead "replicas" 5 [("timeout", 20)]) (inRangeWit 1 10 5)
297+
298+
||| Witness that `twoConfig` validates the timeout contract. `resolve "timeout"`
299+
||| skips the head ("replicas", via `resolveSkip`) then matches ("timeout", via
300+
||| `resolveHead`); the two steps compose with `trans`.
301+
public export
302+
twoValidatesTimeout : Validates Invariants.timeoutContract Invariants.twoConfig
303+
twoValidatesTimeout =
304+
MkValidates 20
305+
(trans (resolveSkip "timeout" "replicas" neqTimeoutReplicas 5 [("timeout", 20)])
306+
(resolveHead "timeout" 20 []))
307+
(inRangeWit 1 30 20)
308+
309+
||| POSITIVE CONTROL (binary): `twoConfig` validates the conjunction.
310+
public export
311+
twoValidatesBoth : ValidatesBoth Invariants.replicasContract
312+
Invariants.timeoutContract Invariants.twoConfig
313+
twoValidatesBoth = MkValidatesBoth twoValidatesReplicas twoValidatesTimeout
314+
315+
||| POSITIVE CONTROL (n-ary): `twoConfig` validates the BUNDLE
316+
||| `[replicasContract, timeoutContract]`.
317+
public export
318+
twoValidatesBundle : ValidatesAll Invariants.twoConfig
319+
[Invariants.replicasContract, Invariants.timeoutContract]
320+
twoValidatesBundle =
321+
ValidatesCons twoValidatesReplicas
322+
(ValidatesCons twoValidatesTimeout ValidatesNil)
323+
324+
||| NEGATIVE / NON-VACUITY CONTROL: a config satisfying the replicas contract
325+
||| but NOT the timeout contract (timeout = 99 is out of [1, 30]) does NOT
326+
||| validate the conjunction. This rules out a vacuous `ValidatesAll`/`Both`.
327+
public export
328+
mixedConfig : Config
329+
mixedConfig = [("timeout", 99), ("replicas", 5)]
330+
331+
||| `timeout = 99` is out of range [1, 30]. `resolveHead` pins
332+
||| `resolve "timeout" mixedConfig = Just 99`; composing with the witness's own
333+
||| equation and `jInj` yields `99 = v` (idiom 3); then `LTE v 30` becomes the
334+
||| uninhabited `LTE 99 30`.
335+
timeoutFailsMixed : Not (Validates Invariants.timeoutContract Invariants.mixedConfig)
336+
timeoutFailsMixed (MkValidates v prf (MkInRange _ hiOk)) =
337+
let resolved = the (resolve "timeout" Invariants.mixedConfig = Just 99)
338+
(resolveHead "timeout" 99 [("replicas", 5)])
339+
vEq = the (99 = v) (jInj (trans (sym resolved) prf)) in
340+
absurd (replace {p = \w => LTE w 30} (sym vEq) hiOk)
341+
342+
||| NEGATIVE CONTROL (binary): `mixedConfig` does not validate the conjunction,
343+
||| because the timeout conjunct fails.
344+
public export
345+
mixedNotBoth : Not (ValidatesBoth Invariants.replicasContract
346+
Invariants.timeoutContract Invariants.mixedConfig)
347+
mixedNotBoth (MkValidatesBoth _ vt) = timeoutFailsMixed vt
348+
349+
||| NEGATIVE CONTROL (n-ary): `mixedConfig` does not validate the bundle
350+
||| `[replicasContract, timeoutContract]`, because the tail (timeout) fails.
351+
public export
352+
mixedNotBundle : Not (ValidatesAll Invariants.mixedConfig
353+
[Invariants.replicasContract, Invariants.timeoutContract])
354+
mixedNotBundle (ValidatesCons _ (ValidatesCons vt _)) = timeoutFailsMixed vt

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,4 @@ modules = K9iser.ABI.Types
1010
, K9iser.ABI.Foreign
1111
, K9iser.ABI.Proofs
1212
, K9iser.ABI.Semantics
13+
, K9iser.ABI.Invariants

0 commit comments

Comments
 (0)