From 200b91f148a3f72378132268e3e2a7cccde180e4 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 22:02:34 +0000 Subject: [PATCH 1/3] 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/3] =?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 From f0190b90cf4e12fa1d5af9ced135bbe0a9ab3fc6 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 05:39:31 +0000 Subject: [PATCH 3/3] abi: seal ABI<->FFI seam with Layer-4 soundness proof (FfiSeam) Prove the alloyiser FFI result-code encoding is sound: distinct ABI outcomes never collide on the C wire and the integer faithfully round-trips back to the ABI value. - intToResult decoder (boolean Bits32 == so round-trip Refls reduce) - resultRoundTrip : intToResult (resultToInt r) = Just r - resultToIntInjective derived from the round-trip via justInj+cong - positive controls (decode 0/7/8) and a machine-checked non-vacuity control (resultToInt Ok /= resultToInt Error) Genuine proof only: no believe_me/postulate/assert_total/%hint. multToInt is export-only (non-reducing across modules) so it is out of scope here without widening Foreign's visibility. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- src/interface/abi/Alloyiser/ABI/FfiSeam.idr | 132 ++++++++++++++++++++ src/interface/abi/alloyiser-abi.ipkg | 1 + 2 files changed, 133 insertions(+) create mode 100644 src/interface/abi/Alloyiser/ABI/FfiSeam.idr diff --git a/src/interface/abi/Alloyiser/ABI/FfiSeam.idr b/src/interface/abi/Alloyiser/ABI/FfiSeam.idr new file mode 100644 index 0000000..a43a14b --- /dev/null +++ b/src/interface/abi/Alloyiser/ABI/FfiSeam.idr @@ -0,0 +1,132 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Layer 4 — sealing the ABI <-> FFI seam for alloyiser. +||| +||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris2 ABI +||| enum and the Zig FFI enum agree by name+value. This module supplies the +||| PROOF-SIDE guarantee that the encoding itself is SOUND: +||| +||| * `resultToInt` is injective — distinct ABI outcomes never collide on the +||| C wire (no two `Result` values share an integer code), so a C consumer +||| can never confuse two outcomes. +||| * The encoding is FAITHFUL / lossless — there is a decoder `intToResult` +||| such that decoding an encoded value recovers exactly the original +||| `Result`. Injectivity is then DERIVED from the round-trip. +||| +||| Scope note: the other FFI enum encoder in this ABI, `multToInt` +||| (`Alloyiser.ABI.Foreign`), is declared `export` rather than `public export`, +||| so its defining clauses do not reduce in importing modules and no +||| computational property of it can be honestly proved from here. We therefore +||| seal the `Result` encoder, which is `public export` and reduces. (Extending +||| the seam to `multToInt` would require widening its visibility in Foreign, +||| which is out of scope for this proof module.) +||| +||| Idiom note: the decoder is written with boolean `Bits32` equality +||| (`if x == 0 then ... else ...`), which reduces on concrete literals, so +||| every round-trip clause checks by `Refl`. Distinct primitive `Bits32` +||| literals are provably unequal, which discharges the negative control. +||| +||| STRICT: genuine proof only. No `believe_me`, `idris_crash`, `assert_total`, +||| `postulate`, `sorry`, or `%hint` hacks anywhere in this module. + +module Alloyiser.ABI.FfiSeam + +import Alloyiser.ABI.Types + +%default total + +-------------------------------------------------------------------------------- +-- Local lemma: Just is injective +-------------------------------------------------------------------------------- + +||| Injectivity of the `Just` constructor, proved by pattern matching on the +||| equality witness (no library dependency, no axioms). +justInj : {0 x, y : a} -> Just x = Just y -> x = y +justInj Refl = Refl + +-------------------------------------------------------------------------------- +-- Result : faithful decoder +-------------------------------------------------------------------------------- + +||| Decode a C integer back into a `Result`. Built with boolean `Bits32` +||| equality so it reduces definitionally on the concrete literals produced by +||| `resultToInt`, which is what lets the round-trip below check by `Refl`. +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 if x == 5 then Just ModelParseError + else if x == 6 then Just SolverTimeout + else if x == 7 then Just CounterexampleFound + else Nothing + +||| Faithfulness: encoding then decoding recovers exactly the original Result. +||| The C integer round-trips back to the ABI value with no loss and no aliasing. +export +resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r +resultRoundTrip Ok = Refl +resultRoundTrip Error = Refl +resultRoundTrip InvalidParam = Refl +resultRoundTrip OutOfMemory = Refl +resultRoundTrip NullPointer = Refl +resultRoundTrip ModelParseError = Refl +resultRoundTrip SolverTimeout = Refl +resultRoundTrip CounterexampleFound = Refl + +||| Injectivity of `resultToInt`, DERIVED from the round-trip via +||| `justInj . cong intToResult`. Distinct ABI outcomes never collide on the +||| wire: if their integer codes are equal, the outcomes are equal. +||| +||| Derivation: if `resultToInt a = resultToInt b`, then applying `intToResult` +||| to both sides gives `intToResult (resultToInt a) = intToResult (resultToInt b)`; +||| by `resultRoundTrip` both sides are `Just a` and `Just b`, so `Just a = Just b`, +||| and `justInj` yields `a = b`. +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) +-------------------------------------------------------------------------------- + +||| The integer 0 decodes to Ok. +export +decodeZeroIsOk : intToResult 0 = Just Ok +decodeZeroIsOk = Refl + +||| The integer 7 decodes to CounterexampleFound (the highest Result code). +export +decodeSevenIsCounterexample : intToResult 7 = Just CounterexampleFound +decodeSevenIsCounterexample = Refl + +||| An out-of-range code decodes to Nothing (the decoder is partial, faithfully). +export +decodeOutOfRangeIsNothing : intToResult 8 = Nothing +decodeOutOfRangeIsNothing = Refl + +-------------------------------------------------------------------------------- +-- Negative / non-vacuity control +-------------------------------------------------------------------------------- + +||| Two DISTINCT result codes have DISTINCT integer encodings — machine-checked. +||| This rules out the vacuous reading of injectivity: the seam is genuinely +||| discriminating, not trivially collapsing every outcome onto one code. +export +okNotError : Not (resultToInt Ok = resultToInt Error) +okNotError = \case Refl impossible + +||| A second distinct pair, for good measure. +export +solverTimeoutNotCounterexample + : Not (resultToInt SolverTimeout = resultToInt CounterexampleFound) +solverTimeoutNotCounterexample = \case Refl impossible diff --git a/src/interface/abi/alloyiser-abi.ipkg b/src/interface/abi/alloyiser-abi.ipkg index 6a7aead..68b5d27 100644 --- a/src/interface/abi/alloyiser-abi.ipkg +++ b/src/interface/abi/alloyiser-abi.ipkg @@ -11,3 +11,4 @@ modules = Alloyiser.ABI.Types , Alloyiser.ABI.Proofs , Alloyiser.ABI.Semantics , Alloyiser.ABI.Invariants + , Alloyiser.ABI.FfiSeam