From 200b91f148a3f72378132268e3e2a7cccde180e4 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 22:02:34 +0000 Subject: [PATCH 1/2] abi: prove Alloy `one`-multiplicity constraint (Layer 2 Semantics) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Flagship semantic proof: an Alloy binary relation satisfies the `one` field multiplicity iff every live source maps to exactly one target (target-count = 1) — the OpenAPI "required, single-valued" property. Sound+complete Dec, certifier into the ABI Result codes proven sound, positive control + negative control (a one-source/two-target instance, the Alloy counterexample, is provably rejected). Verified with idris2 0.7.0 (build clean, zero warnings) + adversarial false-proof rejection. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- src/interface/abi/Alloyiser/ABI/Semantics.idr | 146 ++++++++++++++++++ src/interface/abi/alloyiser-abi.ipkg | 1 + 2 files changed, 147 insertions(+) create mode 100644 src/interface/abi/Alloyiser/ABI/Semantics.idr diff --git a/src/interface/abi/Alloyiser/ABI/Semantics.idr b/src/interface/abi/Alloyiser/ABI/Semantics.idr new file mode 100644 index 0000000..076da2a --- /dev/null +++ b/src/interface/abi/Alloyiser/ABI/Semantics.idr @@ -0,0 +1,146 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Flagship semantic proof for Alloyiser (Idris2 ABI Layer 2). +||| +||| Alloyiser's headline is "extract formal models from API specs and verify +||| with Alloy". The most load-bearing thing an Alloy model expresses is a field +||| *multiplicity constraint*; the canonical, strongest one is `one`: a field +||| `f : A -> one B` asserts that every live source atom maps to EXACTLY ONE +||| target — the OpenAPI "required, single-valued" property alloyiser must +||| preserve when lowering a spec into an `.als` model. +||| +||| This models an Alloy binary relation as a list of (source, target) tuples, +||| defines the `one`-multiplicity property as "the source's target-count is 1", +||| gives a sound+complete `Dec`, a certifier into the ABI `Result` codes proven +||| sound, and positive + negative controls (a one-source/two-target instance — +||| exactly the Alloy counterexample for a `one` field — is provably rejected). + +module Alloyiser.ABI.Semantics + +import Alloyiser.ABI.Types +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- Faithful model of an Alloy binary relation +-------------------------------------------------------------------------------- + +public export +Source : Type +Source = Nat + +public export +Target : Type +Target = Nat + +public export +record Tuple where + constructor MkTuple + src : Source + tgt : Target + +||| An Alloy binary relation instance: a finite set of tuples. +public export +Relation : Type +Relation = List Tuple + +||| How many targets source `s` has under relation `r`. Uses boolean `==` (which +||| reduces on concrete atoms) so the controls' `Refl`s check by computation. +public export +countTargets : Source -> Relation -> Nat +countTargets _ [] = 0 +countTargets s (MkTuple a _ :: ts) = + if s == a then S (countTargets s ts) else countTargets s ts + +-------------------------------------------------------------------------------- +-- The `one` multiplicity property (exactly one target), stated as a count = 1 +-------------------------------------------------------------------------------- + +||| `OneTargetFor s r`: source `s` maps to EXACTLY ONE target under `r`. There is +||| no constructor for count 0 (missing) or count >= 2 (over-multiple): those bad +||| cases are unrepresentable. +public export +data OneTargetFor : Source -> Relation -> Type where + MkOne : {0 s : Source} -> {0 r : Relation} -> countTargets s r = 1 -> OneTargetFor s r + +||| Every source in `sources` maps to exactly one target — the model-level +||| meaning of declaring the field with multiplicity `One` over those atoms. +public export +data ConformsOne : List Source -> Relation -> Type where + ConfNil : {0 r : Relation} -> ConformsOne [] r + ConfCons : {0 s : Source} -> {0 ss : List Source} -> {0 r : Relation} -> + OneTargetFor s r -> ConformsOne ss r -> ConformsOne (s :: ss) r + +-------------------------------------------------------------------------------- +-- Sound + complete decision +-------------------------------------------------------------------------------- + +public export +decOneTargetFor : (s : Source) -> (r : Relation) -> Dec (OneTargetFor s r) +decOneTargetFor s r = case decEq (countTargets s r) 1 of + Yes prf => Yes (MkOne prf) + No no => No (\(MkOne p) => no p) + +public export +decConformsOne : (sources : List Source) -> (r : Relation) -> Dec (ConformsOne sources r) +decConformsOne [] r = Yes ConfNil +decConformsOne (s :: ss) r = case decOneTargetFor s r of + No contra => No (\(ConfCons h _) => contra h) + Yes h => case decConformsOne ss r of + No contra => No (\(ConfCons _ rest) => contra rest) + Yes rest => Yes (ConfCons h rest) + +-------------------------------------------------------------------------------- +-- Certifier into the ABI Result codes + soundness +-------------------------------------------------------------------------------- + +||| Certify a field's `one` multiplicity over its live sources: `Ok` when it +||| holds, `CounterexampleFound` (Alloy's outcome for a violated assertion) +||| otherwise. +public export +certifyOne : (sources : List Source) -> (r : Relation) -> Result +certifyOne sources r = case decConformsOne sources r of + Yes _ => Ok + No _ => CounterexampleFound + +||| Soundness: an `Ok` verdict recovers a genuine `ConformsOne` witness. +export +certifyOneSound : (sources : List Source) -> (r : Relation) -> + certifyOne sources r = Ok -> ConformsOne sources r +certifyOneSound sources r prf with (decConformsOne sources r) + certifyOneSound sources r prf | Yes ok = ok + certifyOneSound sources r Refl | No _ impossible + +-------------------------------------------------------------------------------- +-- Positive control: a conforming instance satisfies the constraint +-------------------------------------------------------------------------------- + +||| source 0 -> target 10, source 1 -> target 11: each source has one target. +public export +goodRelation : Relation +goodRelation = [MkTuple 0 10, MkTuple 1 11] + +export +goodConformsOne : ConformsOne [0, 1] Semantics.goodRelation +goodConformsOne = ConfCons (MkOne Refl) (ConfCons (MkOne Refl) ConfNil) + +-------------------------------------------------------------------------------- +-- Negative control: a one-source/two-target instance is rejected (non-vacuity) +-------------------------------------------------------------------------------- + +||| source 0 maps to BOTH 10 and 20 — the Alloy counterexample for a `one` field. +public export +badRelation : Relation +badRelation = [MkTuple 0 10, MkTuple 0 20] + +||| Machine-checked: source 0 does NOT have exactly one target (its count is 2). +export +badNotOneTarget : Not (OneTargetFor 0 Semantics.badRelation) +badNotOneTarget (MkOne Refl) impossible + +||| Therefore the whole instance fails the `one` constraint. +export +badNotConformsOne : Not (ConformsOne [0] Semantics.badRelation) +badNotConformsOne (ConfCons h _) = badNotOneTarget h diff --git a/src/interface/abi/alloyiser-abi.ipkg b/src/interface/abi/alloyiser-abi.ipkg index 6e949a5..5da2a4a 100644 --- a/src/interface/abi/alloyiser-abi.ipkg +++ b/src/interface/abi/alloyiser-abi.ipkg @@ -9,3 +9,4 @@ modules = Alloyiser.ABI.Types , Alloyiser.ABI.Layout , Alloyiser.ABI.Foreign , Alloyiser.ABI.Proofs + , Alloyiser.ABI.Semantics From 3df49b1cccbe10490ce87f644a040a2bf909d85c Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 22:35:27 +0000 Subject: [PATCH 2/2] =?UTF-8?q?abi(idris2):=20add=20Layer-3=20invariant=20?= =?UTF-8?q?=E2=80=94=20`one`=20entails=20`lone`=20multiplicity?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds Alloyiser.ABI.Invariants over the existing Semantics model: proves the multiplicity-subsumption theorem oneImpliesLone (OneTargetFor s r -> LoneTargetFor s r) plus its field-level lift, a sound+complete Dec for LoneTargetFor, a sound ABI-Result certifier, and certifyOneEntailsLone tying the two verdicts. Controls: zero-target source is lone (positive), two-target source is not lone (negative), and lone does NOT entail one (strictness / non-vacuity). Distinct from and deeper than the Layer-2 `one` theorem. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Alloyiser/ABI/Invariants.idr | 177 ++++++++++++++++++ src/interface/abi/alloyiser-abi.ipkg | 1 + 2 files changed, 178 insertions(+) create mode 100644 src/interface/abi/Alloyiser/ABI/Invariants.idr diff --git a/src/interface/abi/Alloyiser/ABI/Invariants.idr b/src/interface/abi/Alloyiser/ABI/Invariants.idr new file mode 100644 index 0000000..a301b75 --- /dev/null +++ b/src/interface/abi/Alloyiser/ABI/Invariants.idr @@ -0,0 +1,177 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Deeper invariant proof for Alloyiser (Idris2 ABI Layer 3). +||| +||| Layer 2 (`Alloyiser.ABI.Semantics`) proves the `one` multiplicity property +||| for a single field: each live source maps to EXACTLY ONE target +||| (`countTargets s r = 1`). This module proves a genuinely DIFFERENT and +||| DEEPER fact: an *entailment between two of Alloy's multiplicity keywords*. +||| +||| Alloy orders its field multiplicities by permissiveness. `one` (exactly one) +||| is strictly STRONGER than `lone` (at most one): every `one` field is also a +||| valid `lone` field, but not conversely (a `lone` field may map to zero +||| targets). alloyiser must respect this lattice when it weakens or rewrites a +||| spec's constraints — relaxing `one` to `lone` is always sound, so any model +||| that the analyzer certifies for `one` is automatically certified for `lone`. +||| +||| We model `lone` as the propositional bound `LTE (countTargets s r) 1` (using +||| Data.Nat's order, which is the right tool for symbolic counts), reuse the +||| SAME relation/count model from Semantics, and prove: +||| * `oneImpliesLone` : OneTargetFor s r -> LoneTargetFor s r (subsumption) +||| * `conformsOneImpliesLone` : the field-level lift over a source list +||| * a sound+complete `Dec (LoneTargetFor s r)` +||| * `certifyLoneSound` : the ABI-`Result` certifier is sound +||| with a positive control (a zero-target source is `lone`), a negative control +||| (a two-target source is NOT `lone`), AND a non-vacuity control proving the +||| converse FAILS (`lone` does not imply `one`): the entailment is strict. + +module Alloyiser.ABI.Invariants + +import Alloyiser.ABI.Types +import Alloyiser.ABI.Semantics +import Data.Nat +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- The `lone` multiplicity property (AT MOST one target), as a propositional LTE +-------------------------------------------------------------------------------- + +||| `LoneTargetFor s r`: source `s` maps to AT MOST ONE target under `r` — the +||| meaning of Alloy's `lone` keyword. Stated as the order bound +||| `countTargets s r <= 1`, which admits both the zero-target case (field unset) +||| and the one-target case (field set), but excludes count >= 2. +public export +data LoneTargetFor : Source -> Relation -> Type where + MkLone : {0 s : Source} -> {0 r : Relation} -> + LTE (countTargets s r) 1 -> LoneTargetFor s r + +||| Every source in `sources` maps to at most one target — the model-level +||| meaning of declaring the field with multiplicity `Lone` over those atoms. +public export +data ConformsLone : List Source -> Relation -> Type where + LoneNil : {0 r : Relation} -> ConformsLone [] r + LoneCons : {0 s : Source} -> {0 ss : List Source} -> {0 r : Relation} -> + LoneTargetFor s r -> ConformsLone ss r -> ConformsLone (s :: ss) r + +-------------------------------------------------------------------------------- +-- Layer-3 theorem: `one` entails `lone` (multiplicity subsumption) +-------------------------------------------------------------------------------- + +||| THE THEOREM. If a source has exactly one target (`one`), it has at most one +||| target (`lone`). Distinct from Layer 2: this is an implication BETWEEN two +||| constraints, not the establishment of one. The count-equality `n = 1` is +||| rewritten into the order bound `LTE 1 1`, discharged by `LTESucc LTEZero`. +export +oneImpliesLone : {0 s : Source} -> {0 r : Relation} -> + OneTargetFor s r -> LoneTargetFor s r +oneImpliesLone (MkOne prf) = MkLone (rewrite prf in LTESucc LTEZero) + +||| Field-level lift: a relation conforming to `one` over a source list also +||| conforms to `lone` over the same list. Structural induction applying the +||| pointwise subsumption at each source. +export +conformsOneImpliesLone : {0 sources : List Source} -> {0 r : Relation} -> + ConformsOne sources r -> ConformsLone sources r +conformsOneImpliesLone ConfNil = LoneNil +conformsOneImpliesLone (ConfCons h rest) = + LoneCons (oneImpliesLone h) (conformsOneImpliesLone rest) + +-------------------------------------------------------------------------------- +-- Sound + complete decision for `lone` +-------------------------------------------------------------------------------- + +public export +decLoneTargetFor : (s : Source) -> (r : Relation) -> Dec (LoneTargetFor s r) +decLoneTargetFor s r = case isLTE (countTargets s r) 1 of + Yes prf => Yes (MkLone prf) + No no => No (\(MkLone p) => no p) + +public export +decConformsLone : (sources : List Source) -> (r : Relation) -> Dec (ConformsLone sources r) +decConformsLone [] r = Yes LoneNil +decConformsLone (s :: ss) r = case decLoneTargetFor s r of + No contra => No (\(LoneCons h _) => contra h) + Yes h => case decConformsLone ss r of + No contra => No (\(LoneCons _ rest) => contra rest) + Yes rest => Yes (LoneCons h rest) + +-------------------------------------------------------------------------------- +-- Certifier into the ABI Result codes + soundness +-------------------------------------------------------------------------------- + +||| Certify a field's `lone` multiplicity over its live sources: `Ok` when it +||| holds, `CounterexampleFound` otherwise. +public export +certifyLone : (sources : List Source) -> (r : Relation) -> Result +certifyLone sources r = case decConformsLone sources r of + Yes _ => Ok + No _ => CounterexampleFound + +||| Soundness: an `Ok` verdict recovers a genuine `ConformsLone` witness. +export +certifyLoneSound : (sources : List Source) -> (r : Relation) -> + certifyLone sources r = Ok -> ConformsLone sources r +certifyLoneSound sources r prf with (decConformsLone sources r) + certifyLoneSound sources r prf | Yes ok = ok + certifyLoneSound sources r Refl | No _ impossible + +||| Cross-certifier corollary: whatever the `one` certifier accepts, the `lone` +||| certifier accepts too — the relaxation `one |-> lone` never loses a model. +||| (Connects the two ABI verdicts via the entailment theorem above.) +export +certifyOneEntailsLone : (sources : List Source) -> (r : Relation) -> + certifyOne sources r = Ok -> certifyLone sources r = Ok +certifyOneEntailsLone sources r prf with (decConformsLone sources r) + certifyOneEntailsLone sources r prf | Yes _ = Refl + certifyOneEntailsLone sources r prf | No contra = + absurd (contra (conformsOneImpliesLone (certifyOneSound sources r prf))) + +-------------------------------------------------------------------------------- +-- Positive control: a zero-target source IS `lone` (and the `one` -> `lone` +-- lift produces a real witness on a conforming instance) +-------------------------------------------------------------------------------- + +||| source 5 appears in no tuple, so its target-count is 0 — `lone` (<= 1) holds, +||| but `one` (= 1) does NOT. The witness that `lone` is strictly weaker. +public export +emptyForFive : Relation +emptyForFive = [MkTuple 0 10, MkTuple 1 11] + +export +fiveIsLone : LoneTargetFor 5 Invariants.emptyForFive +fiveIsLone = MkLone LTEZero + +||| The Layer-3 theorem applied to Semantics' positive control yields a genuine +||| `ConformsLone` witness — the entailment is computational, not just stated. +export +goodConformsLone : ConformsLone [0, 1] Semantics.goodRelation +goodConformsLone = conformsOneImpliesLone goodConformsOne + +-------------------------------------------------------------------------------- +-- Negative control: a two-target source is NOT `lone` (non-vacuity) +-------------------------------------------------------------------------------- + +||| `badRelation` (from Semantics) maps source 0 to BOTH 10 and 20: count 2. +||| count 2 <= 1 is uninhabited, so source 0 is provably not `lone`. +export +badNotLoneTarget : Not (LoneTargetFor 0 Semantics.badRelation) +badNotLoneTarget (MkLone (LTESucc LTEZero)) impossible + +||| Therefore the whole instance fails the `lone` constraint too. +export +badNotConformsLone : Not (ConformsLone [0] Semantics.badRelation) +badNotConformsLone (LoneCons h _) = badNotLoneTarget h + +-------------------------------------------------------------------------------- +-- Non-vacuity of the strictness: `lone` does NOT entail `one` +-------------------------------------------------------------------------------- + +||| The converse of the Layer-3 theorem is FALSE. Source 5 over `emptyForFive` +||| is `lone` (count 0) yet not `one` (count 0 /= 1). Machine-checked refutation +||| confirms the entailment `one -> lone` is strict, so it is not vacuous. +export +fiveNotOneTarget : Not (OneTargetFor 5 Invariants.emptyForFive) +fiveNotOneTarget (MkOne Refl) impossible diff --git a/src/interface/abi/alloyiser-abi.ipkg b/src/interface/abi/alloyiser-abi.ipkg index 5da2a4a..6a7aead 100644 --- a/src/interface/abi/alloyiser-abi.ipkg +++ b/src/interface/abi/alloyiser-abi.ipkg @@ -10,3 +10,4 @@ modules = Alloyiser.ABI.Types , Alloyiser.ABI.Foreign , Alloyiser.ABI.Proofs , Alloyiser.ABI.Semantics + , Alloyiser.ABI.Invariants