Skip to content

Commit 5dc3cc9

Browse files
claudeclaude
committed
feat(abi): prove correct-by-construction max meets its Dafny postcondition
Add Dafniser.ABI.Semantics raising the Idris2 ABI to Layer 2 with a genuine, machine-checked semantic proof of the repo's headline ("correct-by-construction code generation"). Model: a Dafny spec as the postcondition MaxPost a b r — a real proposition inhabited only when r dominates both inputs and equals one of them. The generated body genMax returns its result paired with a MaxPost proof (correct-by-construction). genMaxCorrect derives all three ensures conjuncts (result>=a, result>=b, result==a||result==b) for all inputs; noUndershootLeft refutes the bad case. A sound certifier (certifyMax/certifyMaxSound) emits the ABI's VerificationResult. Positive control maxPositive : MaxPost 7 3 7 and negative control maxNegative : Not (MaxPost 7 3 2) are machine-checked; an adversarial false proof (MaxPost 7 3 2) is rejected by idris2, confirming non-vacuity. Builds clean (idris2 0.7.0, exit 0, zero warnings). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
1 parent 78da95e commit 5dc3cc9

2 files changed

Lines changed: 209 additions & 1 deletion

File tree

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

Lines changed: 207 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,207 @@
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 Dafniser (Idris2 ABI Layer 2).
5+
|||
6+
||| Dafniser's headline: "Generate correct-by-construction code using Dafny".
7+
||| The essence of correct-by-construction is that a *generated* function
8+
||| provably satisfies its declared *postcondition* whenever its
9+
||| *precondition* holds. This module models that contract for a concrete,
10+
||| representative generated function — integer `max` over `Nat` — and proves,
11+
||| in the Idris2 type system, that the generated body meets the postcondition
12+
||| Dafny would have to discharge to Z3:
13+
|||
14+
||| ensures result >= a && result >= b && (result == a || result == b)
15+
|||
16+
||| The proof is genuine: `MaxPost` is a real proposition built from
17+
||| propositional `LTE` and a disjunction, the postcondition for the bad case
18+
||| (a result smaller than an input, or a result equal to neither) is
19+
||| *uninhabited*, and we provide a sound certifier together with positive and
20+
||| negative machine-checked controls.
21+
22+
module Dafniser.ABI.Semantics
23+
24+
import Dafniser.ABI.Types
25+
import Data.Nat
26+
import Decidable.Equality
27+
28+
%default total
29+
30+
--------------------------------------------------------------------------------
31+
-- A faithful model of a Dafny spec: precondition + postcondition + body
32+
--------------------------------------------------------------------------------
33+
34+
||| The postcondition of the generated `max` function, as a real proposition.
35+
||| `MaxPost a b r` holds exactly when `r` is a correct maximum of `a` and `b`:
36+
||| it dominates both inputs and is equal to one of them. There is NO way to
37+
||| build a `MaxPost` for an incorrect result — the type itself is the contract.
38+
public export
39+
data MaxPost : (a, b, r : Nat) -> Type where
40+
||| `r` came from the left input: r = a, and a dominates b.
41+
FromLeft : (geA : LTE b a) -> MaxPost a b a
42+
||| `r` came from the right input: r = b, and b dominates a.
43+
FromRight : (geB : LTE a b) -> MaxPost a b b
44+
45+
||| The *generated* body of `max` (what Dafniser would emit as target code).
46+
||| Correct-by-construction means: we do not merely assert it works — we return
47+
||| the body together with a proof that it satisfies `MaxPost`.
48+
public export
49+
genMax : (a, b : Nat) -> (r : Nat ** MaxPost a b r)
50+
genMax a b with (isLTE a b)
51+
genMax a b | Yes prf = (b ** FromRight prf)
52+
genMax a b | No contra = (a ** FromLeft (lteSuccLeft (notLTEImpliesGT contra)))
53+
54+
--------------------------------------------------------------------------------
55+
-- The headline property: the generated body meets its postcondition
56+
--------------------------------------------------------------------------------
57+
58+
||| `MaxPost` genuinely implies the three Dafny `ensures` conjuncts.
59+
||| (a) the result dominates the left input.
60+
public export
61+
postDominatesLeft : {a, r : Nat} -> MaxPost a b r -> LTE a r
62+
postDominatesLeft (FromLeft geA) = reflexive
63+
postDominatesLeft (FromRight geB) = geB
64+
65+
||| (b) the result dominates the right input.
66+
public export
67+
postDominatesRight : {b, r : Nat} -> MaxPost a b r -> LTE b r
68+
postDominatesRight (FromLeft geA) = geA
69+
postDominatesRight (FromRight geB) = reflexive
70+
71+
||| (c) the result equals one of the two inputs.
72+
public export
73+
postIsOneInput : MaxPost a b r -> Either (r = a) (r = b)
74+
postIsOneInput (FromLeft geA) = Left Refl
75+
postIsOneInput (FromRight geB) = Right Refl
76+
77+
||| The headline theorem: for ALL inputs there EXISTS a generated result that
78+
||| satisfies every clause of its postcondition simultaneously. This is the
79+
||| machine-checked correct-by-construction guarantee for `max`.
80+
public export
81+
genMaxCorrect : (a, b : Nat) ->
82+
(r : Nat ** (LTE a r, LTE b r, Either (r = a) (r = b)))
83+
genMaxCorrect a b =
84+
let (r ** pf) = genMax a b in
85+
(r ** (postDominatesLeft pf, postDominatesRight pf, postIsOneInput pf))
86+
87+
--------------------------------------------------------------------------------
88+
-- Soundness: the bad case has no inhabitant
89+
--------------------------------------------------------------------------------
90+
91+
||| No natural number is strictly below itself (S r <= r is impossible).
92+
notSuccLTE : {r : Nat} -> Not (LTE (S r) r)
93+
notSuccLTE {r = 0} le = absurd le
94+
notSuccLTE {r = S k} (LTESucc le) = notSuccLTE le
95+
96+
||| A result strictly below the left input can NEVER satisfy the postcondition.
97+
||| This is the non-vacuity core: it refutes the "incorrect max" case.
98+
public export
99+
noUndershootLeft : {a, b, r : Nat} -> LT r a -> Not (MaxPost a b r)
100+
noUndershootLeft ltRA post =
101+
-- LTE a r (from the postcondition) together with r < a (i.e. S r <= a)
102+
-- gives S r <= r, which is absurd.
103+
let leAR = postDominatesLeft post -- a <= r
104+
srLer = transitive ltRA leAR -- S r <= r
105+
in notSuccLTE srLer
106+
107+
--------------------------------------------------------------------------------
108+
-- Sound certifier over the ABI's VerificationResult type
109+
--------------------------------------------------------------------------------
110+
111+
||| Generic refutation: if `r` equals neither input then no postcondition holds.
112+
notNeither : Not (r = a) -> Not (r = b) -> Not (MaxPost a b r)
113+
notNeither na nb (FromLeft geA) = na Refl
114+
notNeither na nb (FromRight geB) = nb Refl
115+
116+
||| Every postcondition proof exposes which input the result came from,
117+
||| as a propositional equality. Used to discharge the awkward branch where
118+
||| `r = a` but the proof claims `FromRight` (forcing `a = b`).
119+
maxPostInput : MaxPost a b r -> Either (r = a) (r = b)
120+
maxPostInput (FromLeft geA) = Left Refl
121+
maxPostInput (FromRight geB) = Right Refl
122+
123+
||| Decide the postcondition for concrete inputs, returning a real proof.
124+
||| Strategy: a valid result must equal one of the inputs, and that input must
125+
||| dominate the other. We test `r = a` (needs b <= a) then `r = b`
126+
||| (needs a <= b); anything else is refuted by `notNeither`.
127+
public export
128+
decMaxPost : (a, b, r : Nat) -> Dec (MaxPost a b r)
129+
decMaxPost a b r with (decEq r a)
130+
decMaxPost a b a | Yes Refl with (isLTE b a)
131+
decMaxPost a b a | Yes Refl | Yes geA = Yes (FromLeft geA)
132+
decMaxPost a b a | Yes Refl | No nGeA with (decEq a b)
133+
-- r = a = b: FromRight reflexive is a valid witness.
134+
decMaxPost a a a | Yes Refl | No nGeA | Yes Refl = Yes (FromRight reflexive)
135+
-- r = a, a /= b, and not (b <= a): genuinely no witness.
136+
decMaxPost a b a | Yes Refl | No nGeA | No nEqAB = No notLeftBad
137+
where
138+
notLeftBad : Not (MaxPost a b a)
139+
notLeftBad p = case p of
140+
FromLeft geA => nGeA geA
141+
FromRight geB => nGeA geB
142+
decMaxPost a b r | No nEqA with (decEq r b)
143+
decMaxPost a b b | No nEqA | Yes Refl with (isLTE a b)
144+
decMaxPost a b b | No nEqA | Yes Refl | Yes geB = Yes (FromRight geB)
145+
decMaxPost a b b | No nEqA | Yes Refl | No nGeB = No notRightBad
146+
where
147+
notRightBad : Not (MaxPost a b b)
148+
notRightBad p = case p of
149+
FromRight geB => nGeB geB
150+
FromLeft geA => nGeB geA
151+
decMaxPost a b r | No nEqA | No nEqB = No (notNeither nEqA nEqB)
152+
153+
||| Certify a generated `max` instance against its postcondition, producing the
154+
||| ABI's `VerificationResult`. `Verified` is emitted only when a real
155+
||| `MaxPost` proof exists; otherwise a `Counterexample` is reported.
156+
public export
157+
certifyMax : (a, b, r : Nat) -> VerificationResult
158+
certifyMax a b r = case decMaxPost a b r of
159+
Yes _ => Verified "max" 0
160+
No _ => Counterexample "max" "ensures result>=a && result>=b && (result==a||result==b)" "incorrect result"
161+
162+
||| Soundness of the certifier: a `Verified` verdict guarantees the
163+
||| postcondition genuinely holds.
164+
public export
165+
certifyMaxSound : (a, b, r : Nat) -> certifyMax a b r = Verified "max" 0 -> MaxPost a b r
166+
certifyMaxSound a b r prf with (decMaxPost a b r)
167+
certifyMaxSound a b r prf | Yes post = post
168+
certifyMaxSound a b r prf | No _ = absurd (counterNotVerified prf)
169+
where
170+
counterNotVerified : Counterexample "max" _ _ = Verified "max" 0 -> Void
171+
counterNotVerified Refl impossible
172+
173+
--------------------------------------------------------------------------------
174+
-- Positive control: an explicit inhabited witness
175+
--------------------------------------------------------------------------------
176+
177+
||| genMax 7 3 produces 7, and 7 is a correct max of 7 and 3.
178+
public export
179+
maxPositive : MaxPost 7 3 7
180+
maxPositive = FromLeft %search
181+
182+
||| The generated body agrees with the witness on concrete inputs.
183+
public export
184+
genMaxConcrete : fst (genMax 7 3) = 7
185+
genMaxConcrete = Refl
186+
187+
||| The certifier accepts the correct instance.
188+
public export
189+
certifyAccepts : certifyMax 7 3 7 = Verified "max" 0
190+
certifyAccepts = Refl
191+
192+
--------------------------------------------------------------------------------
193+
-- Negative control: the bad case is machine-checked impossible
194+
--------------------------------------------------------------------------------
195+
196+
||| There is NO correct-max proof for result 2 on inputs 7 and 3 (2 undershoots
197+
||| both, and equals neither). This is the negative control: the contract
198+
||| rejects the incorrect generated result.
199+
public export
200+
maxNegative : Not (MaxPost 7 3 2)
201+
maxNegative (FromLeft geA) impossible
202+
maxNegative (FromRight geB) impossible
203+
204+
||| The certifier rejects the incorrect instance.
205+
public export
206+
certifyRejects : certifyMax 7 3 2 = Counterexample "max" "ensures result>=a && result>=b && (result==a||result==b)" "incorrect result"
207+
certifyRejects = Refl

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,5 @@ sourcedir = "."
66
modules = Dafniser.ABI.Types,
77
Dafniser.ABI.Layout,
88
Dafniser.ABI.Foreign,
9-
Dafniser.ABI.Proofs
9+
Dafniser.ABI.Proofs,
10+
Dafniser.ABI.Semantics

0 commit comments

Comments
 (0)