From 200b91f148a3f72378132268e3e2a7cccde180e4 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 22:02:34 +0000 Subject: [PATCH] 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