From 727f18dba7ec48877792ac066a9d79c45aa2c8f9 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 19:40:06 +0000 Subject: [PATCH 1/3] abi: prove progressive-disclosure monotonicity (Layer 2 Semantics) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add Mylangiser.ABI.Semantics, a machine-checked flagship proof for the headline domain property: progressive-disclosure interfaces only ever ADD revealed items across steps, never remove a previously-shown one. Model: a disclosure run is a sequence of revealed-item sets (List (List Nat)). A valid step Reveal before after exists only when Subset before after holds (every item visible before is still visible after) — there is no constructor that drops a revealed item. MonotoneRun is the transitive closure over steps. Includes a sound+complete decision procedure (decSubset, decReveal, decRun), a certifier into the ABI Result type with a soundness lemma (certifyRunSound), a positive control (goodRunMonotone: {1}->{1,2}->{1,2,3}) and a negative control (hidingStepInvalid / hidingRunNotMonotone: {1,2}->{1} has no valid transition proof). No believe_me/postulate/assert — fully total. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Mylangiser/ABI/Semantics.idr | 235 ++++++++++++++++++ src/interface/abi/mylangiser-abi.ipkg | 1 + 2 files changed, 236 insertions(+) create mode 100644 src/interface/abi/Mylangiser/ABI/Semantics.idr diff --git a/src/interface/abi/Mylangiser/ABI/Semantics.idr b/src/interface/abi/Mylangiser/ABI/Semantics.idr new file mode 100644 index 0000000..d19466c --- /dev/null +++ b/src/interface/abi/Mylangiser/ABI/Semantics.idr @@ -0,0 +1,235 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Flagship semantic proof for Mylangiser. +||| +||| Headline: "Generate progressive-disclosure interfaces via My-Lang". +||| +||| We model a progressive-disclosure interface as a *sequence of revealed-item +||| sets* (each step reveals more of the API to the user). The defining safety +||| property of progressive disclosure is MONOTONICITY: a disclosure step may +||| only ADD revealed items, never REMOVE a previously-shown one. An interface +||| that hides an item the user has already seen is disorienting and breaks the +||| progressive-disclosure contract. +||| +||| We make this property a *type*: a transition `Reveal before after` only has +||| an inhabitant when `before` is a subset of `after`. A step that hides a +||| previously-revealed item is then provably NOT a valid transition +||| (negative control), while a genuine add-only step has an explicit witness +||| (positive control). A whole disclosure run is `MonotoneRun`, the reflexive- +||| transitive closure of valid steps; we provide a sound + complete decision +||| procedure `decRun`, a certifier into `Result`, and a soundness lemma. + +module Mylangiser.ABI.Semantics + +import Mylangiser.ABI.Types +import Data.List +import Data.List.Elem +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- Domain model: revealed-item sets +-------------------------------------------------------------------------------- + +||| An item identifier exposed in the interface (e.g. a parameter or feature). +||| We use Nat ids so equality is decidable and lists reduce on literals. +public export +Item : Type +Item = Nat + +||| A disclosure state is the set of items currently revealed, modelled as a +||| list of item ids. (Order is irrelevant to the property; membership is what +||| matters.) +public export +State : Type +State = List Item + +||| A disclosure run is the ordered sequence of states the interface passes +||| through as the user progresses. +public export +Run : Type +Run = List State + +-------------------------------------------------------------------------------- +-- Subset relation (the heart of monotonicity) +-------------------------------------------------------------------------------- + +||| `Subset xs ys` holds when every item revealed in `xs` is also revealed in +||| `ys`. This is the "add-only" guarantee at the level of a single step. +public export +data Subset : State -> State -> Type where + ||| The empty state is a subset of anything (nothing to preserve). + SubNil : Subset [] ys + ||| If the head is still revealed in `ys` and the tail is preserved, the whole + ||| state is preserved. + SubCons : Elem x ys -> Subset xs ys -> Subset (x :: xs) ys + +-------------------------------------------------------------------------------- +-- Valid disclosure transition: a step may only ADD items +-------------------------------------------------------------------------------- + +||| `Reveal before after` is the type of *valid* progressive-disclosure steps. +||| There is exactly ONE constructor, and it demands `Subset before after`: +||| every item visible before must still be visible after. There is NO +||| constructor that lets a step drop a revealed item. +public export +data Reveal : State -> State -> Type where + MkReveal : Subset before after -> Reveal before after + +||| A monotone run: the reflexive-transitive closure of valid steps over the +||| sequence of states. An empty or single-state run is trivially monotone; +||| each adjacent pair must be a valid `Reveal`. +public export +data MonotoneRun : Run -> Type where + ||| The empty run is monotone. + RunNil : MonotoneRun [] + ||| A single-state run is monotone (no transitions to check). + RunOne : MonotoneRun [s] + ||| Prepend a valid step onto a monotone tail. + RunStep : Reveal s0 s1 -> MonotoneRun (s1 :: rest) -> + MonotoneRun (s0 :: s1 :: rest) + +-------------------------------------------------------------------------------- +-- Decision procedure for Subset (sound + complete) +-------------------------------------------------------------------------------- + +||| If a cons-state is a subset, so is its tail. (Inversion lemma.) +subsetTail : Subset (x :: xs) ys -> Subset xs ys +subsetTail (SubCons _ rest) = rest + +||| If a cons-state is a subset, its head is a member of the target. +subsetHead : Subset (x :: xs) ys -> Elem x ys +subsetHead (SubCons e _) = e + +||| Decide whether `xs` is a subset of `ys`. Returns a real proof or a real +||| refutation for every input. +public export +decSubset : (xs : State) -> (ys : State) -> Dec (Subset xs ys) +decSubset [] ys = Yes SubNil +decSubset (x :: xs) ys = + case isElem x ys of + No notThere => No (\sub => notThere (subsetHead sub)) + Yes there => + case decSubset xs ys of + Yes rest => Yes (SubCons there rest) + No notRest => No (\sub => notRest (subsetTail sub)) + +-------------------------------------------------------------------------------- +-- Decision procedure for a valid step +-------------------------------------------------------------------------------- + +||| Decide whether a single step `before -> after` is a valid (add-only) +||| disclosure transition. +public export +decReveal : (before : State) -> (after : State) -> Dec (Reveal before after) +decReveal before after = + case decSubset before after of + Yes sub => Yes (MkReveal sub) + No notSub => No (\(MkReveal sub) => notSub sub) + +-------------------------------------------------------------------------------- +-- Decision procedure for a whole run +-------------------------------------------------------------------------------- + +||| Inversion: the tail of a monotone run is itself monotone. +runTail : MonotoneRun (s0 :: s1 :: rest) -> MonotoneRun (s1 :: rest) +runTail (RunStep _ tl) = tl + +||| Inversion: the leading step of a monotone run is a valid Reveal. +runStepHead : MonotoneRun (s0 :: s1 :: rest) -> Reveal s0 s1 +runStepHead (RunStep r _) = r + +||| Worker for `decRun`: decides monotonicity of the run `prev :: rest`, +||| recursing structurally on `rest` (which strictly decreases each step), so +||| totality is manifest to the checker. +decRunFrom : (prev : State) -> (rest : Run) -> Dec (MonotoneRun (prev :: rest)) +decRunFrom prev [] = Yes RunOne +decRunFrom prev (s1 :: more) = + case decReveal prev s1 of + No notStep => No (\mr => notStep (runStepHead mr)) + Yes step => + case decRunFrom s1 more of + Yes tl => Yes (RunStep step tl) + No notTl => No (\mr => notTl (runTail mr)) + +||| Decide whether a run is monotone. Sound + complete. +public export +decRun : (r : Run) -> Dec (MonotoneRun r) +decRun [] = Yes RunNil +decRun (s0 :: rest) = decRunFrom s0 rest + +-------------------------------------------------------------------------------- +-- Certifier into the ABI Result type + soundness +-------------------------------------------------------------------------------- + +||| Certify a run: `Ok` exactly when the run is monotone, `InvalidParam` +||| otherwise. (Reuses the canonical ABI `Result` from Types.) +public export +certifyRun : Run -> Result +certifyRun r = + case decRun r of + Yes _ => Ok + No _ => InvalidParam + +||| Soundness: whenever the certifier says `Ok`, the run really is monotone. +||| This is a genuine extraction from the decision procedure, not an axiom. +public export +certifyRunSound : (r : Run) -> certifyRun r = Ok -> MonotoneRun r +certifyRunSound r prf with (decRun r) + certifyRunSound r prf | Yes mr = mr + certifyRunSound r Refl | No _ impossible + +-------------------------------------------------------------------------------- +-- POSITIVE control: a genuine add-only disclosure run has a witness +-------------------------------------------------------------------------------- + +||| A concrete progressive-disclosure run that only ever adds items: +||| {1} -> {1,2} -> {1,2,3} +||| modelling Beginner -> Intermediate -> Expert with strictly growing surface. +public export +goodRun : Run +goodRun = [[1], [1, 2], [1, 2, 3]] + +||| The good run is monotone — explicit, machine-checked witness. +public export +goodRunMonotone : MonotoneRun Semantics.goodRun +goodRunMonotone = + RunStep (MkReveal (SubCons Here SubNil)) + (RunStep (MkReveal (SubCons Here (SubCons (There Here) SubNil))) + RunOne) + +-------------------------------------------------------------------------------- +-- NEGATIVE control: a step that HIDES a revealed item is NOT a valid transition +-------------------------------------------------------------------------------- + +||| A run that hides a previously-revealed item: {1,2} -> {1}. Item 2 was shown +||| then taken away — this violates progressive disclosure. +public export +hidingRun : Run +hidingRun = [[1, 2], [1]] + +||| The single step {1,2} -> {1} is provably NOT a valid Reveal: there is no +||| way for item 2 (member of the before-state) to be a member of [1]. +||| This is the headline non-vacuity guarantee, machine-checked. +public export +hidingStepInvalid : Not (Reveal [1, 2] [1]) +hidingStepInvalid (MkReveal sub) = twoNotInOne (subsetHead (subsetTail2 sub)) + where + ||| Item 2 is not an element of the singleton list [1]. + twoNotInOne : Elem (the Item 2) [the Item 1] -> Void + twoNotInOne (There later) = absurd later + -- `Here` would require 2 = 1, which is impossible, so the only remaining + -- case is `There`, whose argument is `Elem 2 []` (uninhabited). + + ||| Drop the head of a Subset whose source is `1 :: 2 :: xs`, exposing the + ||| subset proof for `2 :: xs`. + subsetTail2 : Subset (the Item 1 :: the Item 2 :: xs) ys -> + Subset (the Item 2 :: xs) ys + subsetTail2 (SubCons _ rest) = rest + +||| Therefore the whole hiding run is NOT monotone. +public export +hidingRunNotMonotone : Not (MonotoneRun Semantics.hidingRun) +hidingRunNotMonotone mr = hidingStepInvalid (runStepHead mr) diff --git a/src/interface/abi/mylangiser-abi.ipkg b/src/interface/abi/mylangiser-abi.ipkg index 7bbc742..d737064 100644 --- a/src/interface/abi/mylangiser-abi.ipkg +++ b/src/interface/abi/mylangiser-abi.ipkg @@ -7,3 +7,4 @@ modules = Mylangiser.ABI.Types , Mylangiser.ABI.Layout , Mylangiser.ABI.Foreign , Mylangiser.ABI.Proofs + , Mylangiser.ABI.Semantics From b0799b44c5bbb93067721be348d8a680235c20e6 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 23:11:39 +0000 Subject: [PATCH 2/3] abi: add Layer-3 transitivity invariant (Mylangiser.ABI.Invariants) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds a second, deeper, distinct machine-checked theorem over the existing Semantics model. Where Layer 2 proves single-step monotonicity (one Reveal step may only add items), Layer 3 proves the multi-step disclosure relation Reaches is transitive (reachesTrans) and that reachability implies a global Subset (reachesImpliesSubset) — revealed sets only grow across many steps, a fact not implied by the local theorem. Includes the load-bearing algebraic laws subsetElem/subsetTrans/subsetRefl, a sound+complete decision procedure, a Result certifier with soundness extraction, a positive control (concrete two-hop reachability witness whose growth is machine-derived), a composed-path witness via transitivity, and negative/non-vacuity controls (hidingNotSubset, hidingNotReachable, hidingCertifyRejected). Builds clean with zero warnings; adversarial false claims are rejected by the checker. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Mylangiser/ABI/Invariants.idr | 222 ++++++++++++++++++ src/interface/abi/mylangiser-abi.ipkg | 1 + 2 files changed, 223 insertions(+) create mode 100644 src/interface/abi/Mylangiser/ABI/Invariants.idr diff --git a/src/interface/abi/Mylangiser/ABI/Invariants.idr b/src/interface/abi/Mylangiser/ABI/Invariants.idr new file mode 100644 index 0000000..625a4f1 --- /dev/null +++ b/src/interface/abi/Mylangiser/ABI/Invariants.idr @@ -0,0 +1,222 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Layer-3 invariant for Mylangiser: TRANSITIVITY of multi-step disclosure. +||| +||| The Layer-2 flagship (`Mylangiser.ABI.Semantics`) proves single-step +||| monotonicity: one `Reveal` step may only ADD items. That is a property of +||| ADJACENT states. It does NOT, on its own, say anything about what happens +||| across MANY steps — in principle a chain of individually-valid steps could +||| be reasoned about only one hop at a time. +||| +||| This module proves the genuinely deeper, distinct fact: the multi-step +||| reachability relation is TRANSITIVE, and therefore disclosure is +||| monotone GLOBALLY, not just locally. Concretely: +||| +||| * `Reaches s t` is the reflexive-transitive closure of valid `Reveal` +||| steps (the "can the interface get from disclosure state s to t by some +||| number of add-only steps?" relation). +||| +||| * `reachesTrans` : reachability composes — a state reachable from a +||| reachable state is itself reachable. (The headline transitivity result; +||| this is what single-step monotonicity does NOT give you.) +||| +||| * `subsetTrans` : the underlying subset relation is transitive — the deep +||| algebraic law that powers the global guarantee. +||| +||| * `reachesImpliesSubset` : the PAYOFF. If t is reachable from s by ANY +||| number of steps, then `Subset s t` holds: the revealed set never shrinks +||| across the whole run, however long. This collapses an unbounded chain of +||| local guarantees into one global guarantee, which is precisely the part +||| not implied by the Layer-2 single-step theorem. +||| +||| We provide a sound + complete decision procedure for the new transitive +||| subset law (`decSubsetTrans`), a POSITIVE control (a concrete multi-hop +||| reachability witness whose endpoints are provably in the subset relation), +||| and a NEGATIVE / non-vacuity control (a state that is provably NOT reachable +||| because doing so would require hiding an item). + +module Mylangiser.ABI.Invariants + +import Mylangiser.ABI.Types +import Mylangiser.ABI.Semantics +import Data.List.Elem + +%default total + +-------------------------------------------------------------------------------- +-- Deep algebraic law: the subset relation is TRANSITIVE +-------------------------------------------------------------------------------- + +||| Membership transports through subset: if every item of `xs` is in `ys`, and +||| `x` is in `xs`, then `x` is in `ys`. This is the load-bearing lemma — it is +||| what makes the subset relation behave like a genuine order. +export +subsetElem : Subset xs ys -> Elem x xs -> Elem x ys +subsetElem SubNil elemX = absurd elemX +subsetElem (SubCons h _) Here = h +subsetElem (SubCons _ rest) (There later) = subsetElem rest later + +||| Transitivity of subset: if `xs` is a subset of `ys` and `ys` of `zs`, then +||| `xs` is a subset of `zs`. NOT a restatement of single-step monotonicity: +||| this is the algebraic law that composes two separate add-only relationships. +export +subsetTrans : Subset xs ys -> Subset ys zs -> Subset xs zs +subsetTrans SubNil _ = SubNil +subsetTrans (SubCons h rest) syz = + SubCons (subsetElem syz h) (subsetTrans rest syz) + +||| Reflexivity of subset (every state contains itself) — needed for the +||| reflexive part of the reachability closure, and used as a positive witness. +export +subsetRefl : (xs : State) -> Subset xs xs +subsetRefl [] = SubNil +subsetRefl (x :: xs) = + -- Each head x is `Here` in (x :: xs); the tail is a subset of (x :: xs) + -- because it is a subset of itself, then weakened by `There`. + SubCons Here (subsetWeaken (subsetRefl xs)) + where + ||| Weaken a subset target by prepending one more available item. + subsetWeaken : Subset as bs -> Subset as (b :: bs) + subsetWeaken SubNil = SubNil + subsetWeaken (SubCons e rest) = SubCons (There e) (subsetWeaken rest) + +-------------------------------------------------------------------------------- +-- Sound + complete decision of the transitive subset relation +-------------------------------------------------------------------------------- + +||| Decide `Subset xs zs` while EXPOSING the transitive structure: given an +||| intermediate `ys` together with witnesses `Subset xs ys` and `Subset ys zs`, +||| we already KNOW the answer is Yes (by `subsetTrans`); but for a genuine +||| decision over arbitrary inputs we fall back to the complete `decSubset`. +||| This is sound (a Yes carries a real proof) and complete (a No carries a real +||| refutation), reusing the Layer-2 decider as the completeness oracle. +export +decSubsetTrans : (xs : State) -> (zs : State) -> Dec (Subset xs zs) +decSubsetTrans = decSubset + +-------------------------------------------------------------------------------- +-- Multi-step reachability: reflexive-transitive closure of valid steps +-------------------------------------------------------------------------------- + +||| `Reaches s t` holds when the interface can move from disclosure state `s` +||| to `t` by zero or more valid (add-only) `Reveal` steps. This is the +||| relational, endpoint-only view of a `MonotoneRun` (Layer 2 tracked the whole +||| intermediate sequence; here we care about composability of endpoints). +public export +data Reaches : State -> State -> Type where + ||| Zero steps: every state reaches itself. + ReachRefl : Reaches s s + ||| One valid step followed by a reachable remainder. + ReachStep : {0 s0, s2 : State} -> {s1 : State} -> + Reveal s0 s1 -> Reaches s1 s2 -> Reaches s0 s2 + +-------------------------------------------------------------------------------- +-- HEADLINE: reachability is transitive (distinct from single-step monotonicity) +-------------------------------------------------------------------------------- + +||| Transitivity of reachability: a state reachable from a reachable state is +||| itself reachable. Proven by induction on the FIRST derivation, re-grafting +||| the second chain onto the end. This is the multi-step composition law that +||| single-step monotonicity (Layer 2) does not provide. +export +reachesTrans : Reaches s0 s1 -> Reaches s1 s2 -> Reaches s0 s2 +reachesTrans ReachRefl r2 = r2 +reachesTrans (ReachStep st rest) r2 = ReachStep st (reachesTrans rest r2) + +-------------------------------------------------------------------------------- +-- PAYOFF: reachability implies global subset (sets only grow across many steps) +-------------------------------------------------------------------------------- + +||| Across an ENTIRE reachable run, however long, the revealed set never shrinks: +||| if `t` is reachable from `s`, then `Subset s t`. Each step contributes a +||| local `Subset`; `subsetTrans` chains them into one global guarantee. This is +||| the precise sense in which transitivity is DEEPER than the Layer-2 theorem. +export +reachesImpliesSubset : {s : State} -> Reaches s t -> Subset s t +reachesImpliesSubset ReachRefl = subsetRefl s +reachesImpliesSubset (ReachStep (MkReveal sub) rest) = + subsetTrans sub (reachesImpliesSubset rest) + +||| Certifier into the canonical ABI `Result`: `Ok` exactly when the endpoints +||| of a claimed run stand in the subset relation that any genuine reachability +||| must produce. Reuses Types.Result; soundness below. +export +certifyReach : State -> State -> Result +certifyReach s t = + case decSubsetTrans s t of + Yes _ => Ok + No _ => InvalidParam + +||| Soundness of the certifier: `Ok` is returned only when `Subset s t` really +||| holds — a genuine extraction from the decision procedure, not an axiom. +export +certifyReachSound : (s : State) -> (t : State) -> certifyReach s t = Ok -> + Subset s t +certifyReachSound s t prf with (decSubsetTrans s t) + certifyReachSound s t prf | Yes sub = sub + certifyReachSound s t Refl | No _ impossible + +-------------------------------------------------------------------------------- +-- POSITIVE control: a concrete multi-hop reachability witness +-------------------------------------------------------------------------------- + +||| A two-hop reachable disclosure path: {1} -> {1,2} -> {1,2,3}. Each hop is a +||| valid add-only Reveal; the whole thing is one `Reaches` value. +export +goodReach : Reaches [1] [1, 2, 3] +goodReach = + ReachStep (MkReveal (SubCons Here SubNil)) + (ReachStep (MkReveal (SubCons Here (SubCons (There Here) SubNil))) + ReachRefl) + +||| The transitive PAYOFF on the concrete path: because {1,2,3} is reachable +||| from {1}, item 1 (and everything in the start) survives to the end — +||| machine-checked via `reachesImpliesSubset`, NOT restated by hand. +export +goodReachGrows : Subset [1] [1, 2, 3] +goodReachGrows = reachesImpliesSubset Invariants.goodReach + +||| Explicit witness that transitivity composes two separate good paths into one +||| longer reachable path: {1} -> {1,2,3} (above) then {1,2,3} -> {1,2,3,4}. +export +composedReach : Reaches [1] [1, 2, 3, 4] +composedReach = + reachesTrans Invariants.goodReach + (ReachStep + (MkReveal (SubCons Here + (SubCons (There Here) + (SubCons (There (There Here)) SubNil)))) + ReachRefl) + +-------------------------------------------------------------------------------- +-- NEGATIVE / non-vacuity control: a hiding endpoint pair is NOT a subset, and +-- therefore the certifier refuses it (the relation is not trivially true). +-------------------------------------------------------------------------------- + +||| Item 2 is not an element of the singleton list [1]. +twoNotInOne : Not (Elem (the Item 2) [the Item 1]) +twoNotInOne (There later) = absurd later + +||| {1,2} is provably NOT a subset of {1}: item 2 cannot be transported. +||| (Independent re-derivation at this layer, used by the controls below.) +export +hidingNotSubset : Not (Subset [the Item 1, the Item 2] [the Item 1]) +hidingNotSubset sub = twoNotInOne (subsetElem sub (There Here)) + +||| NON-VACUITY: a state reaching one that drops a revealed item is impossible, +||| because reachability forces the subset relation that the hiding pair lacks. +||| If `Reaches` were vacuously/over-permissive this would be inhabited; it is +||| provably not. This is the key guard that the Layer-3 relation has teeth. +export +hidingNotReachable : Not (Reaches [the Item 1, the Item 2] [the Item 1]) +hidingNotReachable r = hidingNotSubset (reachesImpliesSubset r) + +||| And the certifier rejects the hiding endpoints: `certifyReach` returns +||| `InvalidParam`, never `Ok`. Machine-checked deliberately-false `= Ok` would +||| not type-check; we instead prove the true negative. +export +hidingCertifyRejected : certifyReach [the Item 1, the Item 2] [the Item 1] = InvalidParam +hidingCertifyRejected with (decSubsetTrans [the Item 1, the Item 2] [the Item 1]) + hidingCertifyRejected | Yes sub = absurd (hidingNotSubset sub) + hidingCertifyRejected | No _ = Refl diff --git a/src/interface/abi/mylangiser-abi.ipkg b/src/interface/abi/mylangiser-abi.ipkg index d737064..a332b7a 100644 --- a/src/interface/abi/mylangiser-abi.ipkg +++ b/src/interface/abi/mylangiser-abi.ipkg @@ -8,3 +8,4 @@ modules = Mylangiser.ABI.Types , Mylangiser.ABI.Foreign , Mylangiser.ABI.Proofs , Mylangiser.ABI.Semantics + , Mylangiser.ABI.Invariants From 1935c0ef7c2dd7d2aa2172c35ccc05d714d96562 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 06:06:06 +0000 Subject: [PATCH 3/3] Add Layer 4 ABI<->FFI seam proof (Mylangiser.ABI.FfiSeam) Seals the proof side of the ABI<->FFI seam: the FFI result-code encoding resultToInt : Result -> Bits32 is proven SOUND. - intToResult decoder + resultRoundTrip: encoding is lossless/faithful - resultToIntInjective: distinct ABI outcomes never collide on the wire, derived from the round-trip via cong + Just-injectivity - same round-trip + injectivity for disclosureLevelToInt (the other FFI enum encoder in this ABI) - positive controls (concrete decode = Refl) and a machine-checked non-vacuity control (distinct codes have distinct ints) Genuine proof only: no believe_me/idris_crash/assert_total/postulate. %default total throughout. Builds clean with zero warnings; a false seam claim (resultToInt Ok = resultToInt Error) is rejected by the checker. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- src/interface/abi/Mylangiser/ABI/FfiSeam.idr | 163 +++++++++++++++++++ src/interface/abi/mylangiser-abi.ipkg | 1 + 2 files changed, 164 insertions(+) create mode 100644 src/interface/abi/Mylangiser/ABI/FfiSeam.idr diff --git a/src/interface/abi/Mylangiser/ABI/FfiSeam.idr b/src/interface/abi/Mylangiser/ABI/FfiSeam.idr new file mode 100644 index 0000000..94ab318 --- /dev/null +++ b/src/interface/abi/Mylangiser/ABI/FfiSeam.idr @@ -0,0 +1,163 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Layer 4 proof: SEALING the ABI<->FFI SEAM for Mylangiser. +||| +||| The Idris2 ABI (Mylangiser.ABI.Types) defines the FFI result-code enum +||| `Result` and its on-the-wire encoding `resultToInt : Result -> Bits32` +||| (the value the Zig FFI returns to C). A separate STRUCTURAL gate +||| (scripts/abi-ffi-gate.py) checks that the Idris and Zig enums agree by +||| name + value. This module supplies the PROOF-SIDE guarantee that the +||| encoding itself is SOUND: +||| +||| (a) resultToIntInjective — distinct ABI outcomes never collide on the +||| wire (the encoding is unambiguous). +||| (b) intToResult / resultRoundTrip — the C integer faithfully round-trips +||| back to the ABI value (the encoding is lossless / faithful). +||| (c) the same injectivity for the other FFI enum encoder in this ABI, +||| disclosureLevelToInt : DisclosureLevel -> Bits32. +||| +||| Plus positive controls (concrete decode = Refl) and a non-vacuity / +||| negative control (two distinct codes have distinct ints, machine-checked). +||| +||| Genuine proof only: no believe_me / idris_crash / assert_total / postulate. + +module Mylangiser.ABI.FfiSeam + +import Mylangiser.ABI.Types + +%default total + +-------------------------------------------------------------------------------- +-- Local helper: Just is injective +-------------------------------------------------------------------------------- + +||| `Just` is injective. Used to turn a round-trip equality `Just a = Just b` +||| into the underlying `a = b`. +private +justInj : {0 a, b : t} -> Just a = Just b -> a = b +justInj Refl = Refl + +-------------------------------------------------------------------------------- +-- Primitive Bits32 disequality +-------------------------------------------------------------------------------- + +||| Distinct primitive Bits32 literals are provably unequal: the coverage +||| checker discharges `Refl impossible` for distinct primitive constants. +||| We only need the specific pairs that arise off the diagonal below; each is +||| a self-contained, machine-checked refutation with concrete literals. + +-------------------------------------------------------------------------------- +-- (b) Faithful decoder + round-trip for Result +-------------------------------------------------------------------------------- + +||| Decode a C integer back to a Result. Built with boolean Bits32 `==`, which +||| reduces on concrete literals, so the round-trip Refls below check. +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 EndpointNotFound + else if x == 6 then Just InvalidScore + else Nothing + +||| The encoding is lossless: decoding the encoded form recovers the value. +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 EndpointNotFound = Refl +resultRoundTrip InvalidScore = Refl + +-------------------------------------------------------------------------------- +-- (a) Injectivity of resultToInt, DERIVED from the round-trip +-------------------------------------------------------------------------------- + +||| The encoding is unambiguous: distinct ABI outcomes never collide on the +||| wire. Derived cleanly from the round-trip via cong + justInj. +||| +||| If resultToInt a = resultToInt b, applying intToResult to both sides gives +||| intToResult (resultToInt a) = intToResult (resultToInt b) +||| i.e. Just a = Just b by the round-trip on each side, hence 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)) + +-------------------------------------------------------------------------------- +-- (c) Injectivity of disclosureLevelToInt (the other FFI enum encoder) +-------------------------------------------------------------------------------- + +||| Faithful decoder for DisclosureLevel (Beginner=0, Intermediate=1, Expert=2). +public export +intToDisclosureLevel : Bits32 -> Maybe DisclosureLevel +intToDisclosureLevel x = + if x == 0 then Just Beginner + else if x == 1 then Just Intermediate + else if x == 2 then Just Expert + else Nothing + +||| disclosureLevelToInt is lossless. +export +disclosureLevelRoundTrip : (l : DisclosureLevel) -> + intToDisclosureLevel (disclosureLevelToInt l) = Just l +disclosureLevelRoundTrip Beginner = Refl +disclosureLevelRoundTrip Intermediate = Refl +disclosureLevelRoundTrip Expert = Refl + +||| disclosureLevelToInt is unambiguous, derived from its round-trip. +export +disclosureLevelToIntInjective : (a, b : DisclosureLevel) -> + disclosureLevelToInt a = disclosureLevelToInt b -> a = b +disclosureLevelToIntInjective a b prf = + justInj $ + trans (sym (disclosureLevelRoundTrip a)) + (trans (cong intToDisclosureLevel prf) (disclosureLevelRoundTrip b)) + +-------------------------------------------------------------------------------- +-- Positive controls (concrete decode = Refl) +-------------------------------------------------------------------------------- + +||| Decoding the encoding of Ok yields Just Ok. +export +decodeOk : intToResult (resultToInt Ok) = Just Ok +decodeOk = Refl + +||| Decoding the encoding of InvalidScore (the highest code) yields it back. +export +decodeInvalidScore : intToResult (resultToInt InvalidScore) = Just InvalidScore +decodeInvalidScore = Refl + +||| A raw integer not in range decodes to Nothing. +export +decodeUnknown : intToResult 99 = Nothing +decodeUnknown = Refl + +||| Concrete disclosure-level decode. +export +decodeExpert : intToDisclosureLevel (disclosureLevelToInt Expert) = Just Expert +decodeExpert = Refl + +-------------------------------------------------------------------------------- +-- Negative / non-vacuity control (distinct codes have distinct ints) +-------------------------------------------------------------------------------- + +||| Non-vacuity: two DISTINCT result codes encode to DISTINCT integers, so the +||| injectivity theorem is not trivially true. Machine-checked: `resultToInt Ok` +||| reduces to 0 and `resultToInt Error` to 1, and 0 = 1 is impossible. +export +okErrorDistinct : Not (resultToInt Ok = resultToInt Error) +okErrorDistinct Refl impossible + +||| Likewise for the disclosure-level encoder. +export +beginnerExpertDistinct : Not (disclosureLevelToInt Beginner = disclosureLevelToInt Expert) +beginnerExpertDistinct Refl impossible diff --git a/src/interface/abi/mylangiser-abi.ipkg b/src/interface/abi/mylangiser-abi.ipkg index a332b7a..afedeb0 100644 --- a/src/interface/abi/mylangiser-abi.ipkg +++ b/src/interface/abi/mylangiser-abi.ipkg @@ -9,3 +9,4 @@ modules = Mylangiser.ABI.Types , Mylangiser.ABI.Proofs , Mylangiser.ABI.Semantics , Mylangiser.ABI.Invariants + , Mylangiser.ABI.FfiSeam