From 5dc3cc973c9a4632879d4e5032e09c34426253e6 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 19:24:06 +0000 Subject: [PATCH 1/3] feat(abi): prove correct-by-construction max meets its Dafny postcondition MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- src/interface/abi/Dafniser/ABI/Semantics.idr | 207 +++++++++++++++++++ src/interface/abi/dafniser-abi.ipkg | 3 +- 2 files changed, 209 insertions(+), 1 deletion(-) create mode 100644 src/interface/abi/Dafniser/ABI/Semantics.idr diff --git a/src/interface/abi/Dafniser/ABI/Semantics.idr b/src/interface/abi/Dafniser/ABI/Semantics.idr new file mode 100644 index 0000000..442c3df --- /dev/null +++ b/src/interface/abi/Dafniser/ABI/Semantics.idr @@ -0,0 +1,207 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Flagship semantic proof for Dafniser (Idris2 ABI Layer 2). +||| +||| Dafniser's headline: "Generate correct-by-construction code using Dafny". +||| The essence of correct-by-construction is that a *generated* function +||| provably satisfies its declared *postcondition* whenever its +||| *precondition* holds. This module models that contract for a concrete, +||| representative generated function — integer `max` over `Nat` — and proves, +||| in the Idris2 type system, that the generated body meets the postcondition +||| Dafny would have to discharge to Z3: +||| +||| ensures result >= a && result >= b && (result == a || result == b) +||| +||| The proof is genuine: `MaxPost` is a real proposition built from +||| propositional `LTE` and a disjunction, the postcondition for the bad case +||| (a result smaller than an input, or a result equal to neither) is +||| *uninhabited*, and we provide a sound certifier together with positive and +||| negative machine-checked controls. + +module Dafniser.ABI.Semantics + +import Dafniser.ABI.Types +import Data.Nat +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- A faithful model of a Dafny spec: precondition + postcondition + body +-------------------------------------------------------------------------------- + +||| The postcondition of the generated `max` function, as a real proposition. +||| `MaxPost a b r` holds exactly when `r` is a correct maximum of `a` and `b`: +||| it dominates both inputs and is equal to one of them. There is NO way to +||| build a `MaxPost` for an incorrect result — the type itself is the contract. +public export +data MaxPost : (a, b, r : Nat) -> Type where + ||| `r` came from the left input: r = a, and a dominates b. + FromLeft : (geA : LTE b a) -> MaxPost a b a + ||| `r` came from the right input: r = b, and b dominates a. + FromRight : (geB : LTE a b) -> MaxPost a b b + +||| The *generated* body of `max` (what Dafniser would emit as target code). +||| Correct-by-construction means: we do not merely assert it works — we return +||| the body together with a proof that it satisfies `MaxPost`. +public export +genMax : (a, b : Nat) -> (r : Nat ** MaxPost a b r) +genMax a b with (isLTE a b) + genMax a b | Yes prf = (b ** FromRight prf) + genMax a b | No contra = (a ** FromLeft (lteSuccLeft (notLTEImpliesGT contra))) + +-------------------------------------------------------------------------------- +-- The headline property: the generated body meets its postcondition +-------------------------------------------------------------------------------- + +||| `MaxPost` genuinely implies the three Dafny `ensures` conjuncts. +||| (a) the result dominates the left input. +public export +postDominatesLeft : {a, r : Nat} -> MaxPost a b r -> LTE a r +postDominatesLeft (FromLeft geA) = reflexive +postDominatesLeft (FromRight geB) = geB + +||| (b) the result dominates the right input. +public export +postDominatesRight : {b, r : Nat} -> MaxPost a b r -> LTE b r +postDominatesRight (FromLeft geA) = geA +postDominatesRight (FromRight geB) = reflexive + +||| (c) the result equals one of the two inputs. +public export +postIsOneInput : MaxPost a b r -> Either (r = a) (r = b) +postIsOneInput (FromLeft geA) = Left Refl +postIsOneInput (FromRight geB) = Right Refl + +||| The headline theorem: for ALL inputs there EXISTS a generated result that +||| satisfies every clause of its postcondition simultaneously. This is the +||| machine-checked correct-by-construction guarantee for `max`. +public export +genMaxCorrect : (a, b : Nat) -> + (r : Nat ** (LTE a r, LTE b r, Either (r = a) (r = b))) +genMaxCorrect a b = + let (r ** pf) = genMax a b in + (r ** (postDominatesLeft pf, postDominatesRight pf, postIsOneInput pf)) + +-------------------------------------------------------------------------------- +-- Soundness: the bad case has no inhabitant +-------------------------------------------------------------------------------- + +||| No natural number is strictly below itself (S r <= r is impossible). +notSuccLTE : {r : Nat} -> Not (LTE (S r) r) +notSuccLTE {r = 0} le = absurd le +notSuccLTE {r = S k} (LTESucc le) = notSuccLTE le + +||| A result strictly below the left input can NEVER satisfy the postcondition. +||| This is the non-vacuity core: it refutes the "incorrect max" case. +public export +noUndershootLeft : {a, b, r : Nat} -> LT r a -> Not (MaxPost a b r) +noUndershootLeft ltRA post = + -- LTE a r (from the postcondition) together with r < a (i.e. S r <= a) + -- gives S r <= r, which is absurd. + let leAR = postDominatesLeft post -- a <= r + srLer = transitive ltRA leAR -- S r <= r + in notSuccLTE srLer + +-------------------------------------------------------------------------------- +-- Sound certifier over the ABI's VerificationResult type +-------------------------------------------------------------------------------- + +||| Generic refutation: if `r` equals neither input then no postcondition holds. +notNeither : Not (r = a) -> Not (r = b) -> Not (MaxPost a b r) +notNeither na nb (FromLeft geA) = na Refl +notNeither na nb (FromRight geB) = nb Refl + +||| Every postcondition proof exposes which input the result came from, +||| as a propositional equality. Used to discharge the awkward branch where +||| `r = a` but the proof claims `FromRight` (forcing `a = b`). +maxPostInput : MaxPost a b r -> Either (r = a) (r = b) +maxPostInput (FromLeft geA) = Left Refl +maxPostInput (FromRight geB) = Right Refl + +||| Decide the postcondition for concrete inputs, returning a real proof. +||| Strategy: a valid result must equal one of the inputs, and that input must +||| dominate the other. We test `r = a` (needs b <= a) then `r = b` +||| (needs a <= b); anything else is refuted by `notNeither`. +public export +decMaxPost : (a, b, r : Nat) -> Dec (MaxPost a b r) +decMaxPost a b r with (decEq r a) + decMaxPost a b a | Yes Refl with (isLTE b a) + decMaxPost a b a | Yes Refl | Yes geA = Yes (FromLeft geA) + decMaxPost a b a | Yes Refl | No nGeA with (decEq a b) + -- r = a = b: FromRight reflexive is a valid witness. + decMaxPost a a a | Yes Refl | No nGeA | Yes Refl = Yes (FromRight reflexive) + -- r = a, a /= b, and not (b <= a): genuinely no witness. + decMaxPost a b a | Yes Refl | No nGeA | No nEqAB = No notLeftBad + where + notLeftBad : Not (MaxPost a b a) + notLeftBad p = case p of + FromLeft geA => nGeA geA + FromRight geB => nGeA geB + decMaxPost a b r | No nEqA with (decEq r b) + decMaxPost a b b | No nEqA | Yes Refl with (isLTE a b) + decMaxPost a b b | No nEqA | Yes Refl | Yes geB = Yes (FromRight geB) + decMaxPost a b b | No nEqA | Yes Refl | No nGeB = No notRightBad + where + notRightBad : Not (MaxPost a b b) + notRightBad p = case p of + FromRight geB => nGeB geB + FromLeft geA => nGeB geA + decMaxPost a b r | No nEqA | No nEqB = No (notNeither nEqA nEqB) + +||| Certify a generated `max` instance against its postcondition, producing the +||| ABI's `VerificationResult`. `Verified` is emitted only when a real +||| `MaxPost` proof exists; otherwise a `Counterexample` is reported. +public export +certifyMax : (a, b, r : Nat) -> VerificationResult +certifyMax a b r = case decMaxPost a b r of + Yes _ => Verified "max" 0 + No _ => Counterexample "max" "ensures result>=a && result>=b && (result==a||result==b)" "incorrect result" + +||| Soundness of the certifier: a `Verified` verdict guarantees the +||| postcondition genuinely holds. +public export +certifyMaxSound : (a, b, r : Nat) -> certifyMax a b r = Verified "max" 0 -> MaxPost a b r +certifyMaxSound a b r prf with (decMaxPost a b r) + certifyMaxSound a b r prf | Yes post = post + certifyMaxSound a b r prf | No _ = absurd (counterNotVerified prf) + where + counterNotVerified : Counterexample "max" _ _ = Verified "max" 0 -> Void + counterNotVerified Refl impossible + +-------------------------------------------------------------------------------- +-- Positive control: an explicit inhabited witness +-------------------------------------------------------------------------------- + +||| genMax 7 3 produces 7, and 7 is a correct max of 7 and 3. +public export +maxPositive : MaxPost 7 3 7 +maxPositive = FromLeft %search + +||| The generated body agrees with the witness on concrete inputs. +public export +genMaxConcrete : fst (genMax 7 3) = 7 +genMaxConcrete = Refl + +||| The certifier accepts the correct instance. +public export +certifyAccepts : certifyMax 7 3 7 = Verified "max" 0 +certifyAccepts = Refl + +-------------------------------------------------------------------------------- +-- Negative control: the bad case is machine-checked impossible +-------------------------------------------------------------------------------- + +||| There is NO correct-max proof for result 2 on inputs 7 and 3 (2 undershoots +||| both, and equals neither). This is the negative control: the contract +||| rejects the incorrect generated result. +public export +maxNegative : Not (MaxPost 7 3 2) +maxNegative (FromLeft geA) impossible +maxNegative (FromRight geB) impossible + +||| The certifier rejects the incorrect instance. +public export +certifyRejects : certifyMax 7 3 2 = Counterexample "max" "ensures result>=a && result>=b && (result==a||result==b)" "incorrect result" +certifyRejects = Refl diff --git a/src/interface/abi/dafniser-abi.ipkg b/src/interface/abi/dafniser-abi.ipkg index 74ca50a..9a18782 100644 --- a/src/interface/abi/dafniser-abi.ipkg +++ b/src/interface/abi/dafniser-abi.ipkg @@ -6,4 +6,5 @@ sourcedir = "." modules = Dafniser.ABI.Types, Dafniser.ABI.Layout, Dafniser.ABI.Foreign, - Dafniser.ABI.Proofs + Dafniser.ABI.Proofs, + Dafniser.ABI.Semantics From 8e3f4441b8bb68cd07067048277361b419a3ca01 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 22:50:27 +0000 Subject: [PATCH 2/3] =?UTF-8?q?abi(dafniser):=20add=20Layer-3=20Invariants?= =?UTF-8?q?=20=E2=80=94=20dual=20min,=20commutativity,=20min/max=20duality?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds Dafniser.ABI.Invariants over the existing Layer-2 model (Dafniser.ABI.Semantics, reused unchanged). Three distinct, deeper machine-checked properties: 1. Relational commutativity of the max contract (MaxPost a b r <-> MaxPost b a r), with an involution proof ruling out vacuity. 2. A dual correct-by-construction generated function `min` (MinPost / genMin), with sound+complete decision procedure (decMinPost), certifier (certifyMin) and certifier soundness. 3. The min/max duality law max a b + min a b = a + b, proven relationally over any correct results and lifted to the generated bodies (genMaxMinSum). Positive controls (minPositive, commPositive, dualityConcrete, certifyMinAccepts) and negative/non-vacuity controls (minNegative, certifyMinRejects, dualityNonVacuous) all machine-checked. No believe_me/postulate/assert_total; %default total; builds with zero warnings; adversarial false statements rejected by the checker. Registers Dafniser.ABI.Invariants last in dafniser-abi.ipkg. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- src/interface/abi/Dafniser/ABI/Invariants.idr | 289 ++++++++++++++++++ src/interface/abi/dafniser-abi.ipkg | 3 +- 2 files changed, 291 insertions(+), 1 deletion(-) create mode 100644 src/interface/abi/Dafniser/ABI/Invariants.idr diff --git a/src/interface/abi/Dafniser/ABI/Invariants.idr b/src/interface/abi/Dafniser/ABI/Invariants.idr new file mode 100644 index 0000000..377667c --- /dev/null +++ b/src/interface/abi/Dafniser/ABI/Invariants.idr @@ -0,0 +1,289 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Deeper algebraic invariants for Dafniser (Idris2 ABI Layer 3). +||| +||| Layer 2 (`Dafniser.ABI.Semantics`) proves a single generated function — +||| `max` over `Nat` — meets its declared postcondition. That is the +||| correct-by-construction guarantee for ONE function in isolation. +||| +||| Layer 3 goes deeper. Correct-by-construction code generation is only +||| trustworthy if the generated operators obey the *algebraic laws* a human +||| would expect of them, and if *families* of generated functions relate to +||| one another correctly. This module establishes three such properties over +||| the SAME model (`MaxPost` / `genMax` from `Semantics`, reused unchanged): +||| +||| (1) COMMUTATIVITY of the max contract — a relational algebraic law: +||| `MaxPost a b r <-> MaxPost b a r`. The contract does not depend on +||| argument order. This is NOT the Layer-2 theorem (which is about a +||| single fixed argument order); it is a structural symmetry of the spec. +||| +||| (2) A DUAL generated function — `min` — built correct-by-construction in +||| exactly the Layer-2 style (`MinPost` / `genMin`), proven to meet its +||| own postcondition. A second, distinct checker. +||| +||| (3) A min/max DUALITY theorem tying the two operators together: +||| `max a b + min a b = a + b`. This is the deepest result here — it is +||| a property of the *pair* of generated functions, provable only because +||| both meet their contracts. It is the kind of cross-function lemma Z3 +||| would have to discharge for a Dafny program that uses both. +||| +||| The proofs are genuine: every proposition is built from propositional `LTE` +||| and equalities, the bad cases are uninhabited, there is a sound + complete +||| `Dec` for the new contract, and both a positive (inhabited witness) and a +||| negative (`Not (...)`) control are machine-checked. + +module Dafniser.ABI.Invariants + +import Dafniser.ABI.Types +import Dafniser.ABI.Semantics +import Data.Nat +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- (1) Commutativity of the max contract (relational algebraic law) +-------------------------------------------------------------------------------- + +||| The max postcondition is symmetric in its two inputs: a correct maximum of +||| `a` and `b` is also a correct maximum of `b` and `a`. This is a genuine +||| algebraic law about the *contract*, distinct from the Layer-2 claim that a +||| particular generated body satisfies the contract. +public export +maxPostComm : MaxPost a b r -> MaxPost b a r +maxPostComm (FromLeft geA) = FromRight geA -- r = a; a dominates b ==> for (b,a), r = a is the right input +maxPostComm (FromRight geB) = FromLeft geB -- r = b; b dominates a ==> for (b,a), r = b is the left input + +||| Commutativity is an involution: applying it twice is the identity. +||| This rules out a vacuous `maxPostComm` that throws information away. +public export +maxPostCommInvolutive : (p : MaxPost a b r) -> maxPostComm (maxPostComm p) = p +maxPostCommInvolutive (FromLeft geA) = Refl +maxPostCommInvolutive (FromRight geB) = Refl + +-------------------------------------------------------------------------------- +-- (2) The DUAL generated function: min, correct-by-construction +-------------------------------------------------------------------------------- + +||| The postcondition of the generated `min` function, as a real proposition. +||| `MinPost a b r` holds exactly when `r` is a correct minimum of `a` and `b`: +||| it is dominated by both inputs and is equal to one of them. As with +||| `MaxPost`, the type itself is the contract — no incorrect minimum inhabits it. +public export +data MinPost : (a, b, r : Nat) -> Type where + ||| `r` came from the left input: r = a, and a is dominated by b. + MinLeft : (leA : LTE a b) -> MinPost a b a + ||| `r` came from the right input: r = b, and b is dominated by a. + MinRight : (leB : LTE b a) -> MinPost a b b + +||| The *generated* body of `min`. Correct-by-construction: returned together +||| with a proof it satisfies `MinPost`. +public export +genMin : (a, b : Nat) -> (r : Nat ** MinPost a b r) +genMin a b with (isLTE a b) + genMin a b | Yes prf = (a ** MinLeft prf) + genMin a b | No contra = (b ** MinRight (lteSuccLeft (notLTEImpliesGT contra))) + +||| `MinPost` implies the result is dominated by the left input. +public export +minBelowLeft : {a, r : Nat} -> MinPost a b r -> LTE r a +minBelowLeft (MinLeft leA) = reflexive +minBelowLeft (MinRight leB) = leB + +||| `MinPost` implies the result is dominated by the right input. +public export +minBelowRight : {b, r : Nat} -> MinPost a b r -> LTE r b +minBelowRight (MinLeft leA) = leA +minBelowRight (MinRight leB) = reflexive + +||| `MinPost` implies the result equals one of the inputs. +public export +minIsOneInput : MinPost a b r -> Either (r = a) (r = b) +minIsOneInput (MinLeft leA) = Left Refl +minIsOneInput (MinRight leB) = Right Refl + +||| Headline correctness for the dual: for ALL inputs there EXISTS a generated +||| result meeting every `min` postcondition clause simultaneously. +public export +genMinCorrect : (a, b : Nat) -> + (r : Nat ** (LTE r a, LTE r b, Either (r = a) (r = b))) +genMinCorrect a b = + let (r ** pf) = genMin a b in + (r ** (minBelowLeft pf, minBelowRight pf, minIsOneInput pf)) + +-------------------------------------------------------------------------------- +-- Soundness of the dual contract: the bad case has no inhabitant +-------------------------------------------------------------------------------- + +||| No natural number is strictly above itself (S r <= r is impossible). +||| (Stated locally so this module does not depend on a private Semantics name.) +notSuccLTE' : {r : Nat} -> Not (LTE (S r) r) +notSuccLTE' {r = 0} le = absurd le +notSuccLTE' {r = S k} (LTESucc le) = notSuccLTE' le + +||| A result strictly ABOVE the left input can NEVER satisfy `MinPost`. +||| The non-vacuity core for the dual contract: it refutes "incorrect min". +public export +noOvershootLeft : {a, r : Nat} -> LT a r -> Not (MinPost a b r) +noOvershootLeft ltAR post = + -- r <= a (from the postcondition) together with a < r (i.e. S a <= r) + -- gives S a <= a, which is absurd. + let leRA = minBelowLeft post -- r <= a + saLea = transitive ltAR leRA -- S a <= a + in notSuccLTE' saLea + +-------------------------------------------------------------------------------- +-- Sound + complete decision procedure for the dual contract +-------------------------------------------------------------------------------- + +||| If `r` equals neither input then no `min` postcondition holds. +notNeitherMin : {0 a, b, r : Nat} -> Not (r = a) -> Not (r = b) -> Not (MinPost a b r) +notNeitherMin na nb (MinLeft leA) = na Refl +notNeitherMin na nb (MinRight leB) = nb Refl + +||| Decide the `min` postcondition for concrete inputs, returning a real proof. +||| A valid result must equal one of the inputs, and the OTHER input must +||| dominate it; anything else is refuted. +public export +decMinPost : (a, b, r : Nat) -> Dec (MinPost a b r) +decMinPost a b r with (decEq r a) + decMinPost a b a | Yes Refl with (isLTE a b) + decMinPost a b a | Yes Refl | Yes leA = Yes (MinLeft leA) + decMinPost a b a | Yes Refl | No nLeA with (decEq a b) + -- r = a = b: MinRight reflexive is a valid witness. + decMinPost a a a | Yes Refl | No nLeA | Yes Refl = Yes (MinRight reflexive) + -- r = a, a /= b, and not (a <= b): genuinely no witness. + decMinPost a b a | Yes Refl | No nLeA | No nEqAB = No notLeftBad + where + notLeftBad : Not (MinPost a b a) + notLeftBad p = case p of + MinLeft leA => nLeA leA + MinRight leB => nLeA leB + decMinPost a b r | No nEqA with (decEq r b) + decMinPost a b b | No nEqA | Yes Refl with (isLTE b a) + decMinPost a b b | No nEqA | Yes Refl | Yes leB = Yes (MinRight leB) + decMinPost a b b | No nEqA | Yes Refl | No nLeB = No notRightBad + where + notRightBad : Not (MinPost a b b) + notRightBad p = case p of + MinRight leB => nLeB leB + MinLeft leA => nLeB leA + decMinPost a b r | No nEqA | No nEqB = No (notNeitherMin nEqA nEqB) + +||| Certify a generated `min` instance against its postcondition, producing the +||| ABI's `VerificationResult`. `Verified` only when a real `MinPost` exists. +public export +certifyMin : (a, b, r : Nat) -> VerificationResult +certifyMin a b r = case decMinPost a b r of + Yes _ => Verified "min" 0 + No _ => Counterexample "min" "ensures result<=a && result<=b && (result==a||result==b)" "incorrect result" + +||| Soundness of the dual certifier: a `Verified` verdict guarantees the +||| postcondition genuinely holds. +public export +certifyMinSound : (a, b, r : Nat) -> certifyMin a b r = Verified "min" 0 -> MinPost a b r +certifyMinSound a b r prf with (decMinPost a b r) + certifyMinSound a b r prf | Yes post = post + certifyMinSound a b r prf | No _ = absurd (counterNotVerified prf) + where + counterNotVerified : Counterexample "min" _ _ = Verified "min" 0 -> Void + counterNotVerified Refl impossible + +-------------------------------------------------------------------------------- +-- (3) The min/max DUALITY theorem: max a b + min a b = a + b +-------------------------------------------------------------------------------- +-- +-- This is the deepest property in the module. It is a law about the PAIR of +-- generated functions, provable only because each meets its contract. We prove +-- it RELATIONALLY: given any correct max-result rmax and any correct +-- min-result rmin for the same inputs, their sum equals a + b. Then we obtain +-- the concrete corollary for the generated bodies genMax / genMin. + +||| Relational duality: for the SAME inputs, any correct maximum and any correct +||| minimum sum to a + b. Proof is by case analysis on which input each result +||| came from; the two "diagonal" cases use antisymmetry of LTE to collapse. +public export +maxMinSum : {a, b : Nat} -> + MaxPost a b rmax -> MinPost a b rmin -> rmax + rmin = a + b +-- max = a (b <= a), min = b (b <= a): a + b = a + b. +maxMinSum (FromLeft geA) (MinRight leB) = Refl +-- max = b (a <= b), min = a (a <= b): b + a = a + b. +maxMinSum (FromRight geB) (MinLeft leA) = plusCommutative b a +-- max = a (b <= a), min = a (a <= b): here a = b by antisymmetry, so a + a = a + b. +maxMinSum (FromLeft geA) (MinLeft leA) = + rewrite antisymmetric leA geA in Refl +-- max = b (a <= b), min = b (b <= a): here a = b by antisymmetry, so b + b = a + b. +maxMinSum (FromRight geB) (MinRight leB) = + rewrite antisymmetric geB leB in Refl + +||| Concrete duality corollary for the generated bodies: the Dafniser-emitted +||| `max` and `min` sum to a + b on every input. This is the cross-function +||| obligation a Dafny program using both operators would need discharged. +||| Helper: the sum law lifted to the dependent-pair packaging, so it can be +||| applied directly to whatever `genMax` / `genMin` return without needing the +||| opaque `fst (genMax ...)` application to reduce. +dpairSum : {a, b : Nat} -> + (p : (r : Nat ** MaxPost a b r)) -> + (q : (s : Nat ** MinPost a b s)) -> + fst p + fst q = a + b +dpairSum (rmax ** pmax) (rmin ** pmin) = maxMinSum pmax pmin + +public export +genMaxMinSum : (a, b : Nat) -> fst (genMax a b) + fst (genMin a b) = a + b +genMaxMinSum a b = dpairSum (genMax a b) (genMin a b) + +-------------------------------------------------------------------------------- +-- Positive controls: explicit inhabited witnesses / concrete instances +-------------------------------------------------------------------------------- + +||| genMin 7 3 produces 3, and 3 is a correct min of 7 and 3. +public export +minPositive : MinPost 7 3 3 +minPositive = MinRight %search + +||| The generated min body agrees with the witness on concrete inputs. +public export +genMinConcrete : fst (genMin 7 3) = 3 +genMinConcrete = Refl + +||| The dual certifier accepts the correct instance. +public export +certifyMinAccepts : certifyMin 7 3 3 = Verified "min" 0 +certifyMinAccepts = Refl + +||| The commutativity law in action: a correct max of (7,3) gives a correct +||| max of (3,7) for the same result 7. +public export +commPositive : MaxPost 3 7 7 +commPositive = maxPostComm maxPositive + +||| Concrete duality check: max 7 3 + min 7 3 = 10 = 7 + 3. +public export +dualityConcrete : fst (genMax 7 3) + fst (genMin 7 3) = 10 +dualityConcrete = Refl + +-------------------------------------------------------------------------------- +-- Negative / non-vacuity controls: bad cases machine-checked impossible +-------------------------------------------------------------------------------- + +||| There is NO correct-min proof for result 7 on inputs 7 and 3 (7 overshoots +||| the right input 3, and the genuine minimum is 3). Negative control for the +||| dual contract. +public export +minNegative : Not (MinPost 7 3 7) +minNegative (MinLeft leA) = absurd leA -- would need LTE 7 3, which is uninhabited +-- MinRight would need 7 = 3 (r = b); that case does not unify, so it is absent. + +||| The dual certifier rejects the incorrect instance. +public export +certifyMinRejects : certifyMin 7 3 7 + = Counterexample "min" "ensures result<=a && result<=b && (result==a||result==b)" "incorrect result" +certifyMinRejects = Refl + +||| Non-vacuity of the duality law: a WRONG pairing (the true max 7 with a wrong +||| "min" 7) cannot satisfy the duality sum, because that wrong min has no +||| `MinPost` proof at all. We exhibit the refutation of its premise. +public export +dualityNonVacuous : Not (MinPost 7 3 7) +dualityNonVacuous = minNegative diff --git a/src/interface/abi/dafniser-abi.ipkg b/src/interface/abi/dafniser-abi.ipkg index 9a18782..5970792 100644 --- a/src/interface/abi/dafniser-abi.ipkg +++ b/src/interface/abi/dafniser-abi.ipkg @@ -7,4 +7,5 @@ modules = Dafniser.ABI.Types, Dafniser.ABI.Layout, Dafniser.ABI.Foreign, Dafniser.ABI.Proofs, - Dafniser.ABI.Semantics + Dafniser.ABI.Semantics, + Dafniser.ABI.Invariants From 33621d7cb8452765e98277a1ac8c2e76eaca296a Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 05:48:53 +0000 Subject: [PATCH 3/3] abi: seal ABI<->FFI seam with Layer 4 soundness proof (Dafniser.ABI.FfiSeam) Prove the FFI result-code encoding is sound: - intToResult decoder + resultRoundTrip (lossless/faithful encoding) - resultToIntInjective derived from the round-trip (no collisions on the wire) - positive controls (decode 0=Ok, 4=NullPointer, 5=Nothing) - machine-checked negative/non-vacuity control (Ok and Error differ) Genuine total proof: no believe_me / postulate / assert_total / %hint. Wires Dafniser.ABI.FfiSeam into dafniser-abi.ipkg. Builds clean, zero warnings. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- src/interface/abi/Dafniser/ABI/FfiSeam.idr | 116 +++++++++++++++++++++ src/interface/abi/dafniser-abi.ipkg | 3 +- 2 files changed, 118 insertions(+), 1 deletion(-) create mode 100644 src/interface/abi/Dafniser/ABI/FfiSeam.idr diff --git a/src/interface/abi/Dafniser/ABI/FfiSeam.idr b/src/interface/abi/Dafniser/ABI/FfiSeam.idr new file mode 100644 index 0000000..7d7978f --- /dev/null +++ b/src/interface/abi/Dafniser/ABI/FfiSeam.idr @@ -0,0 +1,116 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Layer 4 — Sealing the ABI<->FFI seam for Dafniser. +||| +||| The structural gate (`scripts/abi-ffi-gate.py`) checks that the Idris2 +||| `Result` enum and the Zig FFI enum agree by name and value. This module +||| provides the PROOF-SIDE guarantee that the on-the-wire encoding is SOUND: +||| +||| (a) `resultToIntInjective` — distinct ABI outcomes never collide on the +||| integer wire (the encoding is unambiguous). +||| (b) `intToResult` + `resultRoundTrip` — the C integer faithfully +||| round-trips back to the originating ABI value (lossless decoding). +||| +||| Injectivity (a) is DERIVED from the round-trip (b): if `resultToInt a` +||| equals `resultToInt b`, applying the decoder to both sides and rewriting +||| with the round-trip lemma yields `Just a = Just b`, hence `a = b`. +||| +||| Positive controls pin concrete decodes; a machine-checked negative control +||| witnesses non-vacuity (two distinct result codes have distinct integers). +||| +||| No `believe_me`, `idris_crash`, `assert_total`, `postulate`, `sorry`, or +||| `%hint` hacks: this is a genuine, total proof. + +module Dafniser.ABI.FfiSeam + +import Dafniser.ABI.Types + +%default total + +-------------------------------------------------------------------------------- +-- Decoder: integer wire -> ABI Result +-------------------------------------------------------------------------------- + +||| Decode a C integer back into a `Result`. +||| +||| Built with boolean `Bits32` equality (`==`) rather than a `case` on +||| literal patterns: `==` on concrete `Bits32` constants reduces +||| definitionally, so the round-trip `Refl`s below check. Any integer +||| outside the encoded range `[0,4]` decodes to `Nothing`, so the decoder +||| is total and the round-trip is the only way to land on a `Just`. +public export +intToResult : Bits32 -> Maybe Result +intToResult x = + if x == 0 then Just Ok + else if x == 1 then Just Error + else if x == 2 then Just InvalidParam + else if x == 3 then Just OutOfMemory + else if x == 4 then Just NullPointer + else Nothing + +-------------------------------------------------------------------------------- +-- (b) Faithful / lossless encoding: round-trip +-------------------------------------------------------------------------------- + +||| The encoding is lossless: decoding the integer produced by `resultToInt` +||| recovers exactly the original `Result`. +public export +resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r +resultRoundTrip Ok = Refl +resultRoundTrip Error = Refl +resultRoundTrip InvalidParam = Refl +resultRoundTrip OutOfMemory = Refl +resultRoundTrip NullPointer = Refl + +-------------------------------------------------------------------------------- +-- (a) Injectivity of the encoding, DERIVED from the round-trip +-------------------------------------------------------------------------------- + +||| `Just` is injective. Defined locally to keep the dependency surface to +||| `Dafniser.ABI.Types` alone (no extra Prelude/Data imports needed). +private +justInj : {0 x, y : a} -> Just x = Just y -> x = y +justInj Refl = Refl + +||| The encoding is unambiguous: if two `Result`s encode to the same integer, +||| they are the same `Result`. Proof: apply `intToResult` to both sides of +||| the integer equality (`cong`), then rewrite each side with its round-trip +||| (`resultRoundTrip`) to obtain `Just a = Just b`, and conclude by `justInj`. +public export +resultToIntInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b +resultToIntInjective a b prf = + justInj (trans (sym (resultRoundTrip a)) + (trans (cong intToResult prf) (resultRoundTrip b))) + +-------------------------------------------------------------------------------- +-- Positive controls (concrete decodes, machine-checked = Refl) +-------------------------------------------------------------------------------- + +||| Decoding `0` yields `Ok`. +public export +decodeZeroIsOk : intToResult 0 = Just Ok +decodeZeroIsOk = Refl + +||| Decoding `4` yields `NullPointer` (the top of the encoded range). +public export +decodeFourIsNullPointer : intToResult 4 = Just NullPointer +decodeFourIsNullPointer = Refl + +||| Any out-of-range integer decodes to `Nothing` (here, `5`). +public export +decodeOutOfRangeIsNothing : intToResult 5 = Nothing +decodeOutOfRangeIsNothing = Refl + +-------------------------------------------------------------------------------- +-- Negative / non-vacuity control (distinct codes => distinct integers) +-------------------------------------------------------------------------------- + +||| Non-vacuity: two DISTINCT result codes have DISTINCT integer encodings. +||| If `resultToInt Ok` (= 0) equalled `resultToInt Error` (= 1) the encoding +||| would be collapsing; `0 = 1` on `Bits32` is uninhabited, so the coverage +||| checker discharges the `impossible` branch. This guarantees the seam is +||| not trivially satisfied by a constant encoder. +public export +okAndErrorDiffer : Not (resultToInt Ok = resultToInt Error) +okAndErrorDiffer prf = case prf of Refl impossible diff --git a/src/interface/abi/dafniser-abi.ipkg b/src/interface/abi/dafniser-abi.ipkg index 5970792..378f374 100644 --- a/src/interface/abi/dafniser-abi.ipkg +++ b/src/interface/abi/dafniser-abi.ipkg @@ -8,4 +8,5 @@ modules = Dafniser.ABI.Types, Dafniser.ABI.Foreign, Dafniser.ABI.Proofs, Dafniser.ABI.Semantics, - Dafniser.ABI.Invariants + Dafniser.ABI.Invariants, + Dafniser.ABI.FfiSeam