Skip to content

Commit 7dddd86

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
Add Layer 2 semantic proof: configs self-validate against K9 contracts (#46)
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). Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx Co-authored-by: Claude <noreply@anthropic.com>
1 parent 3341266 commit 7dddd86

2 files changed

Lines changed: 210 additions & 0 deletions

File tree

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

Lines changed: 209 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,209 @@
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 k9iser: configs as self-validating K9 contracts.
5+
|||
6+
||| Headline property — "Wrap configs into self-validating K9 contracts":
7+
||| a config that SATISFIES a contract provably validates, and a config that
8+
||| VIOLATES it provably does NOT validate. The contract here is a faithful but
9+
||| minimal "must"-rule: a named key MUST be present and its value MUST lie
10+
||| within an inclusive numeric range.
11+
|||
12+
||| The proposition `Validates` has constructors ONLY for the satisfying case
13+
||| (key present with an in-range value); there is no constructor for a missing
14+
||| key or an out-of-range value. `decValidates` is a sound + complete decision
15+
||| procedure returning a real `Dec`, `certify` is the certifier into the ABI's
16+
||| `Result` code, and `certifySound` proves the certifier is faithful. Positive
17+
||| and negative controls pin down non-vacuity.
18+
19+
module K9iser.ABI.Semantics
20+
21+
import K9iser.ABI.Types
22+
import Data.Nat
23+
import Decidable.Equality
24+
import Decidable.Decidable
25+
26+
%default total
27+
28+
--------------------------------------------------------------------------------
29+
-- Faithful domain model
30+
--------------------------------------------------------------------------------
31+
32+
||| A config value. Keep the model minimal but real: configs map keys to
33+
||| natural-number values (e.g. a port, a replica count, a timeout).
34+
public export
35+
Key : Type
36+
Key = String
37+
38+
||| A config is an association list from keys to Nat values, as produced by a
39+
||| parser front-end before contract checking.
40+
public export
41+
Config : Type
42+
Config = List (Key, Nat)
43+
44+
||| A K9 "must"-contract: the key that MUST be present, and the inclusive
45+
||| range [lo, hi] its value MUST fall within.
46+
public export
47+
record Contract where
48+
constructor MkContract
49+
key : Key
50+
lo : Nat
51+
hi : Nat
52+
53+
--------------------------------------------------------------------------------
54+
-- Lookup model (resolver equation stored in the witness, per idiom 4)
55+
--------------------------------------------------------------------------------
56+
57+
||| Resolve a key to its value in a config (first match wins).
58+
public export
59+
resolve : Key -> Config -> Maybe Nat
60+
resolve k [] = Nothing
61+
resolve k ((k', v) :: rest) = case decEq k k' of
62+
Yes _ => Just v
63+
No _ => resolve k rest
64+
65+
||| Constructor-headed injectivity of `Just`, used to transport at the term
66+
||| level (idiom 2) instead of casing on a stuck `resolve k c = Just v`.
67+
justInj : {0 x, y : a} -> Just x = Just y -> x = y
68+
justInj Refl = Refl
69+
70+
--------------------------------------------------------------------------------
71+
-- The headline proposition: NO constructor for the bad case
72+
--------------------------------------------------------------------------------
73+
74+
||| `InRange lo hi v` holds exactly when lo <= v AND v <= hi, using
75+
||| propositional `LTE` (idiom 5: Nat `<=` does not reduce for symbolic
76+
||| operands, but `LTE` is a genuine proposition).
77+
public export
78+
data InRange : (low, high, val : Nat) -> Type where
79+
MkInRange : LTE low val -> LTE val high -> InRange low high val
80+
81+
||| A config VALIDATES a contract iff the required key resolves to some value
82+
||| that is in range. The witness stores the resolver equation (idiom 4), so
83+
||| there is genuinely no way to build a `Validates` for a missing key or an
84+
||| out-of-range value.
85+
public export
86+
data Validates : Contract -> Config -> Type where
87+
MkValidates : (v : Nat) ->
88+
(prf : resolve (key c) cfg = Just v) ->
89+
InRange (lo c) (hi c) v ->
90+
Validates c cfg
91+
92+
--------------------------------------------------------------------------------
93+
-- Sound + complete decision for InRange
94+
--------------------------------------------------------------------------------
95+
96+
||| Decide membership in an inclusive range. `isLTE` is the Prelude's complete
97+
||| decision for `LTE`.
98+
public export
99+
decInRange : (lo, hi, v : Nat) -> Dec (InRange lo hi v)
100+
decInRange lo hi v = case isLTE lo v of
101+
No loBad => No (\(MkInRange loOk _) => loBad loOk)
102+
Yes loOk => case isLTE v hi of
103+
No hiBad => No (\(MkInRange _ hiOk) => hiBad hiOk)
104+
Yes hiOk => Yes (MkInRange loOk hiOk)
105+
106+
--------------------------------------------------------------------------------
107+
-- Sound + complete decision for Validates
108+
--------------------------------------------------------------------------------
109+
110+
||| Decide whether a config validates a contract. Uses `with ... proof eq` so
111+
||| the resolver equation is in scope in each branch (idiom 4), letting us both
112+
||| build the positive witness and refute the negative branches honestly.
113+
public export
114+
decValidates : (c : Contract) -> (cfg : Config) -> Dec (Validates c cfg)
115+
decValidates c cfg with (resolve (key c) cfg) proof eq
116+
_ | Nothing =
117+
-- No value resolves, so no `Validates` witness can exist.
118+
No (\(MkValidates v prf _) =>
119+
-- prf : resolve (key c) cfg = Just v; eq : ... = Nothing.
120+
case trans (sym prf) eq of Refl impossible)
121+
_ | (Just v) = case decInRange (lo c) (hi c) v of
122+
Yes ok => Yes (MkValidates v eq ok)
123+
No bad =>
124+
-- Value resolves to `v` but is out of range; any witness would
125+
-- have to use the same `v` (idiom 3) and so an in-range proof.
126+
No (\(MkValidates v' prf rng) =>
127+
let vEq = the (v' = v) (justInj (trans (sym prf) eq)) in
128+
bad (rewrite sym vEq in rng))
129+
130+
--------------------------------------------------------------------------------
131+
-- Certifier into the ABI Result code + soundness
132+
--------------------------------------------------------------------------------
133+
134+
||| Certify a config against a contract, producing an ABI `Result`:
135+
||| `Ok` when it validates, `ConstraintViolation` when it does not.
136+
public export
137+
certify : (c : Contract) -> (cfg : Config) -> Result
138+
certify c cfg = case decValidates c cfg of
139+
Yes _ => Ok
140+
No _ => ConstraintViolation
141+
142+
||| Soundness: if the certifier reports `Ok`, the config really does validate.
143+
public export
144+
certifySound : (c : Contract) -> (cfg : Config) ->
145+
certify c cfg = Ok -> Validates c cfg
146+
certifySound c cfg prf with (decValidates c cfg)
147+
certifySound c cfg prf | Yes ok = ok
148+
certifySound c cfg Refl | No _ impossible
149+
150+
||| Completeness: if the config validates, the certifier reports `Ok`.
151+
public export
152+
certifyComplete : (c : Contract) -> (cfg : Config) ->
153+
Validates c cfg -> certify c cfg = Ok
154+
certifyComplete c cfg vld with (decValidates c cfg)
155+
certifyComplete c cfg vld | Yes _ = Refl
156+
certifyComplete c cfg vld | No bad = absurd (bad vld)
157+
158+
--------------------------------------------------------------------------------
159+
-- Controls (non-vacuity)
160+
--------------------------------------------------------------------------------
161+
162+
||| A concrete contract: key "replicas" must be in [1, 10].
163+
||| Small bounds keep type-level normalisation cheap while the property stays
164+
||| faithful (a "must"-rule: required key present, value within range).
165+
public export
166+
portContract : Contract
167+
portContract = MkContract "replicas" 1 10
168+
169+
||| Helper: extract the `InRange` proof from the complete decision on concrete
170+
||| operands. `decInRange 1 10 5` evaluates to `Yes ...` at type-check time, so
171+
||| this is a genuine, machine-checked witness (not proof search).
172+
inRangeFromDec : (low, high, val : Nat) ->
173+
{auto 0 ok : IsYes (decInRange low high val)} ->
174+
InRange low high val
175+
inRangeFromDec low high val {ok} with (decInRange low high val)
176+
inRangeFromDec low high val {ok = ItIsYes} | Yes prf = prf
177+
178+
||| POSITIVE CONTROL: a config with replicas = 5 validates the contract.
179+
||| `resolve "replicas" goodConfig` reduces to `Just 5` on concrete data
180+
||| (idiom 5), so the equation is `Refl`.
181+
public export
182+
goodConfig : Config
183+
goodConfig = [("host", 1), ("replicas", 5)]
184+
185+
public export
186+
goodValidates : Validates Semantics.portContract Semantics.goodConfig
187+
goodValidates = MkValidates 5 Refl (inRangeFromDec 1 10 5)
188+
189+
||| NEGATIVE CONTROL 1 (out of range): replicas = 0 violates [1, 10].
190+
public export
191+
badRangeConfig : Config
192+
badRangeConfig = [("replicas", 0)]
193+
194+
public export
195+
badRangeNotValidates : Not (Validates Semantics.portContract Semantics.badRangeConfig)
196+
badRangeNotValidates (MkValidates v prf (MkInRange loOk _)) =
197+
-- prf : resolve "replicas" badRangeConfig = Just v, which resolves to Just 0,
198+
-- so justInj prf : 0 = v. Then loOk : LTE 1 v becomes LTE 1 0 (uninhabited).
199+
let vEq = the (0 = v) (justInj prf) in
200+
absurd (replace {p = LTE 1} (sym vEq) loOk)
201+
202+
||| NEGATIVE CONTROL 2 (missing key): no "replicas" key at all.
203+
public export
204+
missingConfig : Config
205+
missingConfig = [("host", 1)]
206+
207+
public export
208+
missingNotValidates : Not (Validates Semantics.portContract Semantics.missingConfig)
209+
missingNotValidates (MkValidates v prf _) = absurd prf

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,4 @@ modules = K9iser.ABI.Types
99
, K9iser.ABI.Layout
1010
, K9iser.ABI.Foreign
1111
, K9iser.ABI.Proofs
12+
, K9iser.ABI.Semantics

0 commit comments

Comments
 (0)