Skip to content

Commit 1f72b7e

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 2: prove Kleene ternary-logic soundness — flagship Idris2 proof (#39)
## Summary Raises betlangiser's Idris2 ABI to **Layer 2** with its first flagship semantic proof. betlangiser's headline is ternary probabilistic modelling; the logical substrate is three-valued (Kleene) logic over `Trit = T | U | F`. This proves that substrate is algebraically sound: negation is an involution, De Morgan holds, and `Designated` (classical truth) is a decidable proposition with `and3` preservation. Mirrors the estate flagship-proof pattern: faithful model, universal laws proven by total case analysis, sound+complete `Dec`, certifier proven sound, positive + non-vacuous negative controls. ## Changes - Adds `src/interface/abi/Betlangiser/ABI/Semantics.idr` — `not3`/`and3`/`or3`, `doubleNeg`, `deMorgan`, `Designated`/`decDesignated`, `andDesignated`, `certifyDesignatedSound`, and negative controls (`negationNotIdentity`, `uNotDesignated`, `fNotDesignated`). - Registers the module in `betlangiser-abi.ipkg`. ## RSR Quality Checklist ### Required - [x] Tests pass — ABI builds clean (see Testing) - [x] Linter clean — zero warnings - [x] No banned language patterns - [x] No banned functions — genuine proof - [x] SPDX headers present - [x] No secrets ### As Applicable - [x] ABI/FFI changes validated — additive proof; FFI untouched ## Testing Verified with **Idris2 0.7.0**: `idris2 --build betlangiser-abi.ipkg` → exit 0, 5/5 modules, zero warnings. **Adversarial check**: a deliberately-false proof (`Designated F = DesT`) was rejected by the type checker. `build/` removed. 🤖 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)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent e59dbe0 commit 1f72b7e

2 files changed

Lines changed: 161 additions & 0 deletions

File tree

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

Lines changed: 160 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,160 @@
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 Betlangiser (Idris2 ABI Layer 2).
5+
|||
6+
||| Betlangiser's headline is "ternary probabilistic modelling". The logical
7+
||| substrate is three-valued (Kleene) logic over `Trit = T | U | F` (true /
8+
||| unknown / false). This module proves that substrate is algebraically sound:
9+
|||
10+
||| 1. negation is an involution (`doubleNeg`: not3 (not3 x) = x);
11+
||| 2. De Morgan holds (`deMorgan`: not3 (and3 x y) = or3 (not3 x) (not3 y));
12+
||| 3. `Designated` (classical truth, = T) is a decidable proposition with a
13+
||| sound+complete `Dec`, a certifier proven sound, and `and3` preserves it;
14+
||| 4. positive + negative controls, the negative ones machine-checking that the
15+
||| laws are non-vacuous (negation is genuinely not the identity; U and F are
16+
||| genuinely not designated).
17+
18+
module Betlangiser.ABI.Semantics
19+
20+
import Betlangiser.ABI.Types
21+
import Decidable.Equality
22+
23+
%default total
24+
25+
--------------------------------------------------------------------------------
26+
-- The three truth values and the Kleene connectives
27+
--------------------------------------------------------------------------------
28+
29+
public export
30+
data Trit = T | U | F
31+
32+
public export
33+
not3 : Trit -> Trit
34+
not3 T = F
35+
not3 U = U
36+
not3 F = T
37+
38+
||| Kleene conjunction (the min under F < U < T).
39+
public export
40+
and3 : Trit -> Trit -> Trit
41+
and3 F _ = F
42+
and3 _ F = F
43+
and3 T T = T
44+
and3 T U = U
45+
and3 U T = U
46+
and3 U U = U
47+
48+
||| Kleene disjunction (the max under F < U < T).
49+
public export
50+
or3 : Trit -> Trit -> Trit
51+
or3 T _ = T
52+
or3 _ T = T
53+
or3 F F = F
54+
or3 F U = U
55+
or3 U F = U
56+
or3 U U = U
57+
58+
--------------------------------------------------------------------------------
59+
-- Algebraic laws (universally quantified, proven by total case analysis)
60+
--------------------------------------------------------------------------------
61+
62+
||| Negation is an involution.
63+
export
64+
doubleNeg : (x : Trit) -> not3 (not3 x) = x
65+
doubleNeg T = Refl
66+
doubleNeg U = Refl
67+
doubleNeg F = Refl
68+
69+
||| De Morgan: negating a conjunction is the disjunction of the negations.
70+
export
71+
deMorgan : (x, y : Trit) -> not3 (and3 x y) = or3 (not3 x) (not3 y)
72+
deMorgan T T = Refl
73+
deMorgan T U = Refl
74+
deMorgan T F = Refl
75+
deMorgan U T = Refl
76+
deMorgan U U = Refl
77+
deMorgan U F = Refl
78+
deMorgan F T = Refl
79+
deMorgan F U = Refl
80+
deMorgan F F = Refl
81+
82+
--------------------------------------------------------------------------------
83+
-- Designated truth as a decidable proposition (no inhabitant for U or F)
84+
--------------------------------------------------------------------------------
85+
86+
||| A `Designated` value is classically true — in Kleene logic, exactly `T`.
87+
||| There is no constructor for `U` or `F`.
88+
public export
89+
data Designated : Trit -> Type where
90+
DesT : Designated T
91+
92+
export
93+
Uninhabited (Designated U) where
94+
uninhabited DesT impossible
95+
96+
export
97+
Uninhabited (Designated F) where
98+
uninhabited DesT impossible
99+
100+
public export
101+
decDesignated : (t : Trit) -> Dec (Designated t)
102+
decDesignated T = Yes DesT
103+
decDesignated U = No absurd
104+
decDesignated F = No absurd
105+
106+
||| Truth-functional soundness: conjunction preserves designation.
107+
export
108+
andDesignated : Designated x -> Designated y -> Designated (and3 x y)
109+
andDesignated DesT DesT = DesT
110+
111+
--------------------------------------------------------------------------------
112+
-- Certifier into the ABI Result, proven sound
113+
--------------------------------------------------------------------------------
114+
115+
public export
116+
certifyDesignated : Trit -> Result
117+
certifyDesignated t = case decDesignated t of
118+
Yes _ => Ok
119+
No _ => Error
120+
121+
export
122+
certifyDesignatedSound : (t : Trit) -> certifyDesignated t = Ok -> Designated t
123+
certifyDesignatedSound t prf with (decDesignated t)
124+
certifyDesignatedSound t prf | Yes d = d
125+
certifyDesignatedSound t Refl | No _ impossible
126+
127+
--------------------------------------------------------------------------------
128+
-- Positive controls
129+
--------------------------------------------------------------------------------
130+
131+
export
132+
tDesignated : Designated T
133+
tDesignated = DesT
134+
135+
export
136+
andTTDesignated : Designated (and3 T T)
137+
andTTDesignated = andDesignated DesT DesT
138+
139+
export
140+
certifyTAccepts : certifyDesignated T = Ok
141+
certifyTAccepts = Refl
142+
143+
--------------------------------------------------------------------------------
144+
-- Negative controls — the laws are non-vacuous
145+
--------------------------------------------------------------------------------
146+
147+
||| Negation is genuinely not the identity (so `doubleNeg` is non-trivial).
148+
export
149+
negationNotIdentity : Not (not3 T = T)
150+
negationNotIdentity Refl impossible
151+
152+
||| `U` is not designated — Kleene "unknown" is not classical truth.
153+
export
154+
uNotDesignated : Not (Designated U)
155+
uNotDesignated = absurd
156+
157+
||| `F` is not designated.
158+
export
159+
fNotDesignated : Not (Designated F)
160+
fNotDesignated = absurd

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,3 +7,4 @@ modules = Betlangiser.ABI.Types
77
, Betlangiser.ABI.Layout
88
, Betlangiser.ABI.Foreign
99
, Betlangiser.ABI.Proofs
10+
, Betlangiser.ABI.Semantics

0 commit comments

Comments
 (0)