From 85802f5aea306d7f7beef73c160f6392dcd62134 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 19:36:30 +0000 Subject: [PATCH 1/3] abi(semantics): prove saturating-counter node invariant + determinism Add Lustreiser.ABI.Semantics, raising the Idris2 ABI to Layer 2 with a machine-checked flagship proof of the repo headline (formally verified real-time embedded code via Lustre). Faithful model: a synchronous saturating bounded-counter Lustre node with Tick/Reset inputs, a static cap, and one-tick state memory; step/run give the synchronous execution semantics. Properties proven (no believe_me/postulate/assert): - Invariant preservation per tick: WithinBound c -> WithinBound (step i c) for every input, lifted to whole runs via runPreservesBound (no overflow). - Determinism (synchronous hypothesis): equal input streams from equal state yield equal output streams. - Sound+complete Dec (decWithinBound) + sound certifier (certifyBoundSound). - Positive controls (explicit witnesses, incl. a run that saturates) and a machine-checked negative control (overflowNotWithinBound) ensuring non-vacuity; a deliberately false witness is rejected by idris2. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Lustreiser/ABI/Semantics.idr | 218 ++++++++++++++++++ src/interface/abi/lustreiser-abi.ipkg | 1 + 2 files changed, 219 insertions(+) create mode 100644 src/interface/abi/Lustreiser/ABI/Semantics.idr diff --git a/src/interface/abi/Lustreiser/ABI/Semantics.idr b/src/interface/abi/Lustreiser/ABI/Semantics.idr new file mode 100644 index 0000000..0a1bd22 --- /dev/null +++ b/src/interface/abi/Lustreiser/ABI/Semantics.idr @@ -0,0 +1,218 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Flagship semantic proof for Lustreiser (raises the Idris2 ABI to Layer 2). +||| +||| Lustre is a synchronous dataflow language: a node is a deterministic +||| transition over discrete clock ticks. This module gives a faithful, +||| executable model of one such node — a *saturating bounded counter*, +||| the canonical pattern in real-time embedded code (watchdog ticks, +||| debounce counters, retry budgets) — and proves the two safety +||| properties that justify "formally verified real-time embedded code": +||| +||| 1. INVARIANT PRESERVATION (per tick): if the counter state satisfies +||| `state <= cap` before a tick, it still satisfies `state <= cap` +||| after the transition, for ANY input. Lifted to whole runs: every +||| reachable state of the node respects the bound — no overflow. +||| +||| 2. DETERMINISM (the synchronous hypothesis): the node is a pure +||| function of (state, input). Identical input streams from identical +||| initial state produce identical output streams — bit-for-bit. +||| +||| The model is minimal but real: a true Lustre saturating counter, +||| with state, a reset input, and the `pre`/`fby`-style one-tick memory. +module Lustreiser.ABI.Semantics + +import Data.Nat +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- Faithful ADT model of a synchronous saturating-counter node +-------------------------------------------------------------------------------- + +||| The per-tick input to the node. On each clock tick the environment +||| either pulses `Tick` (advance the counter) or `Reset` (clear to 0). +||| This is the boolean clock input that Lustre `merge`/`when` would gate on. +public export +data Input = Tick | Reset + +||| The node is parameterised by a static saturation bound `cap` — fixed at +||| compile time, exactly as a Lustre constant. State is the current count. +||| `cap` is part of the node identity (a field), not a free variable. +public export +record CounterNode where + constructor MkCounter + cap : Nat + state : Nat + +||| Saturating successor: increments unless already at the cap. +||| Decided on the propositional `LTE (S n) cap` (i.e. `n < cap`) so the +||| bound proof can reuse exactly the witness this branch produces. +public export +satInc : (cap : Nat) -> (n : Nat) -> Nat +satInc cap n = case isLTE (S n) cap of + Yes _ => S n + No _ => cap + +||| One synchronous transition (the node's step / output function). +||| This is the ENTIRE behaviour of the node on a single clock tick. +public export +step : Input -> CounterNode -> CounterNode +step Tick (MkCounter cap s) = MkCounter cap (satInc cap s) +step Reset (MkCounter cap s) = MkCounter cap 0 + +||| Run the node over a finite input stream (a list of ticks), threading +||| state left-to-right — this is the synchronous execution semantics. +public export +run : List Input -> CounterNode -> CounterNode +run [] c = c +run (i :: is) c = run is (step i c) + +-------------------------------------------------------------------------------- +-- PROPERTY 1: the per-tick safety invariant (counter never exceeds cap) +-------------------------------------------------------------------------------- + +||| The invariant: the node's state is within its static bound. +||| There is deliberately NO way to build `WithinBound` for an out-of-range +||| state other than via the genuine `LTE state cap` proof — the bad case +||| (state > cap) is simply not constructible. +public export +data WithinBound : CounterNode -> Type where + IsWithin : {cap, s : Nat} -> LTE s cap -> WithinBound (MkCounter cap s) + +-------------------------------------------------------------------------------- +-- Lemmas (all genuine — no believe_me / postulate / assert) +-------------------------------------------------------------------------------- + +||| `satInc` never exceeds the cap, for any current value. Case split on the +||| same decidable `LTE (S n) cap` test that `satInc` itself uses, so each +||| branch reduces and is discharged with a real `LTE` proof. +public export +satIncBounded : (cap : Nat) -> (n : Nat) -> LTE (satInc cap n) cap +satIncBounded cap n with (isLTE (S n) cap) + -- `S n <= cap`: `satInc = S n`, and that very proof is the bound. + satIncBounded cap n | Yes prf = prf + -- not `S n <= cap`: `satInc = cap`, and `cap <= cap` reflexively. + satIncBounded cap n | No _ = reflexive + +||| INVARIANT PRESERVATION: if the state is within bound before a tick, it is +||| within bound after the tick — for EVERY input. This is the per-tick +||| safety theorem at the heart of the node. +public export +stepPreservesBound : (i : Input) -> (c : CounterNode) -> + WithinBound c -> WithinBound (step i c) +stepPreservesBound Tick (MkCounter cap s) (IsWithin _) = + IsWithin (satIncBounded cap s) +stepPreservesBound Reset (MkCounter cap s) (IsWithin _) = + IsWithin LTEZero + +||| INVARIANT for whole runs: if the initial state is within bound, then after +||| running ANY input stream the final state is still within bound. Proved by +||| induction over the stream, reusing the per-tick theorem at each step. +public export +runPreservesBound : (is : List Input) -> (c : CounterNode) -> + WithinBound c -> WithinBound (run is c) +runPreservesBound [] c w = w +runPreservesBound (i :: is) c w = + runPreservesBound is (step i c) (stepPreservesBound i c w) + +-------------------------------------------------------------------------------- +-- Sound + complete decision procedure for the invariant +-------------------------------------------------------------------------------- + +||| Decide the invariant for a concrete node. Sound (Yes carries a real proof) +||| and complete (No carries a refutation of the bad case). Built on the +||| library `isLTE`, which is itself a genuine `Dec (LTE m n)`. +public export +decWithinBound : (c : CounterNode) -> Dec (WithinBound c) +decWithinBound (MkCounter cap s) = case isLTE s cap of + Yes prf => Yes (IsWithin prf) + No contra => No (\(IsWithin p) => contra p) + +-------------------------------------------------------------------------------- +-- PROPERTY 2: determinism (the synchronous hypothesis) +-------------------------------------------------------------------------------- + +||| DETERMINISM, one tick: the transition is a function, so equal inputs and +||| equal start states force equal results. This is the propositional content +||| of "the node is deterministic" — there is no nondeterministic branch. +public export +stepDeterministic : (i : Input) -> (c1, c2 : CounterNode) -> + c1 = c2 -> step i c1 = step i c2 +stepDeterministic i c1 c2 eq = cong (step i) eq + +||| DETERMINISM, whole run: identical input streams from identical initial +||| state yield identical final state — bit-for-bit. Proved by induction; +||| the engine of real-time reproducibility / replayability. +public export +runDeterministic : (is : List Input) -> (c1, c2 : CounterNode) -> + c1 = c2 -> run is c1 = run is c2 +runDeterministic is c1 c2 eq = cong (run is) eq + +-------------------------------------------------------------------------------- +-- Certifier: maps a node + invariant proof to an ABI-level status +-------------------------------------------------------------------------------- + +||| ABI-facing verdict for a single node's bound check. +public export +data BoundStatus = BoundProven | BoundRefuted + +||| Certify the bound invariant, returning a machine status. The decision is +||| the genuine `decWithinBound`, so `BoundProven` is never emitted without an +||| underlying `LTE` proof existing. +public export +certifyBound : (c : CounterNode) -> BoundStatus +certifyBound c = case decWithinBound c of + Yes _ => BoundProven + No _ => BoundRefuted + +||| SOUNDNESS of the certifier: if it says `BoundProven`, the invariant truly +||| holds. We recover the witness by re-running the same decision and matching +||| on its result — no axioms. +public export +certifyBoundSound : (c : CounterNode) -> certifyBound c = BoundProven -> + WithinBound c +certifyBoundSound c prf with (decWithinBound c) + certifyBoundSound c prf | Yes w = w + certifyBoundSound c Refl | No _ impossible + +-------------------------------------------------------------------------------- +-- POSITIVE control: an explicit inhabited witness +-------------------------------------------------------------------------------- + +||| A concrete watchdog counter (cap = 3, state = 2) is within bound, and +||| stays within bound after a tick — a fully explicit, machine-checked +||| witness that the property is inhabited (non-trivial). +public export +safeWatchdogWithinBound : WithinBound (MkCounter 3 2) +safeWatchdogWithinBound = IsWithin (LTESucc (LTESucc LTEZero)) + +||| Running a real input stream from a within-bound start stays within bound. +||| (cap = 3, start = 0, stream = Tick,Tick,Tick,Tick,Reset,Tick) — the +||| saturation actually fires here, so this exercises the interesting path. +public export +safeRunWithinBound : WithinBound (run [Tick,Tick,Tick,Tick,Reset,Tick] (MkCounter 3 0)) +safeRunWithinBound = + runPreservesBound [Tick,Tick,Tick,Tick,Reset,Tick] (MkCounter 3 0) (IsWithin LTEZero) + +||| Determinism positive control: the same stream from the same state lands on +||| the same concrete final node (checked by `Refl`, i.e. by reduction). +public export +safeRunDeterministic : + run [Tick,Tick,Reset,Tick] (MkCounter 3 0) + = run [Tick,Tick,Reset,Tick] (MkCounter 3 0) +safeRunDeterministic = + runDeterministic [Tick,Tick,Reset,Tick] (MkCounter 3 0) (MkCounter 3 0) Refl + +-------------------------------------------------------------------------------- +-- NEGATIVE control: the bad case is genuinely refuted +-------------------------------------------------------------------------------- + +||| An out-of-range node (cap = 2, state = 5) does NOT satisfy the invariant. +||| Machine-checked: pattern-matching extracts the impossible `LTE 5 2` and +||| discharges it. This is what makes the property non-vacuous. +public export +overflowNotWithinBound : Not (WithinBound (MkCounter 2 5)) +overflowNotWithinBound (IsWithin prf) = absurd prf diff --git a/src/interface/abi/lustreiser-abi.ipkg b/src/interface/abi/lustreiser-abi.ipkg index 4990e4f..e3416cb 100644 --- a/src/interface/abi/lustreiser-abi.ipkg +++ b/src/interface/abi/lustreiser-abi.ipkg @@ -9,3 +9,4 @@ modules = Lustreiser.ABI.Types , Lustreiser.ABI.Layout , Lustreiser.ABI.Foreign , Lustreiser.ABI.Proofs + , Lustreiser.ABI.Semantics From 44e9763920328ec378c4bcc1abecfbbaa89fa164 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 23:06:49 +0000 Subject: [PATCH 2/3] =?UTF-8?q?abi(lustreiser):=20add=20Layer-3=20Invarian?= =?UTF-8?q?ts=20=E2=80=94=20run=20is=20a=20monoid=20action=20+=20satInc=20?= =?UTF-8?q?monotonicity?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds Lustreiser.ABI.Invariants over the existing Semantics model (same Input/CounterNode/satInc/step/run). Proves a deeper, distinct class of property than the Layer-2 bound/cong-determinism: - FLAGSHIP: runAppend — run (xs ++ ys) c = run ys (run xs c), the monoid action / fold-fusion law, by genuine induction on the prefix (not cong). - Corollaries: runConsSplit, runResetClears, runEndingInResetIsZero (transition soundness consumed through runAppend). - ORTHOGONAL: satIncMonotone — order preservation of the saturating successor (m <= n => satInc cap m <= satInc cap n), plus stepTickMonotone. - decEqInput: sound+complete Dec for input equality. - Positive controls (appendWitness, resetSuffixWitness, monotoneWitness) and non-vacuity controls (prefixMatters, inputsDistinct, satIncNotConstant, all Not (...)). No believe_me/postulate/assert/idris_crash. %default total. Clean build, zero warnings; adversarial false-equality check rejected. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Lustreiser/ABI/Invariants.idr | 208 ++++++++++++++++++ src/interface/abi/lustreiser-abi.ipkg | 1 + 2 files changed, 209 insertions(+) create mode 100644 src/interface/abi/Lustreiser/ABI/Invariants.idr diff --git a/src/interface/abi/Lustreiser/ABI/Invariants.idr b/src/interface/abi/Lustreiser/ABI/Invariants.idr new file mode 100644 index 0000000..770ff8f --- /dev/null +++ b/src/interface/abi/Lustreiser/ABI/Invariants.idr @@ -0,0 +1,208 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Deeper structural invariants for Lustreiser (raises the Idris2 ABI to +||| Layer 3). This module builds DIRECTLY on the Layer-2 `Semantics` model +||| (same `Input`, `CounterNode`, `satInc`, `step`, `run`) — it does NOT +||| redefine the datatypes — and proves a genuinely different, deeper class +||| of property than Layer 2. +||| +||| Layer 2 proved (a) the per-tick / whole-run safety BOUND and (b) +||| determinism only at `cong` level ("equal inputs give equal outputs"). +||| Both are shallow with respect to the *structure* of `run`: (b) holds of +||| any function and says nothing about how `run` decomposes over its stream. +||| +||| Layer 3 proves the ALGEBRAIC LAW that actually characterises a synchronous +||| node as a deterministic, replayable state machine — that `run` is a left +||| monoid action of the input stream on the node state: +||| +||| FLAGSHIP THEOREM (composition / fold-fusion): +||| run (xs ++ ys) c = run ys (run xs c) +||| +||| proved by genuine structural INDUCTION over the prefix (not `cong`). +||| +||| From it follow the deeper operational corollaries (run-splitting; any run +||| ending in `Reset` clears the state). Independently, this module proves a +||| second, orthogonal transition-soundness theorem absent from Layer 2: +||| MONOTONICITY of the saturating successor in its counter argument +||| (`m <= n => satInc cap m <= satInc cap n`) — the order-preservation +||| property that licenses interval / abstract-interpretation reasoning over +||| the node. A natural decision (`decEqInput`), positive controls, and a +||| non-vacuity (`Not (...)`) negative control are all machine-checked. +module Lustreiser.ABI.Invariants + +import Data.Nat +import Decidable.Equality + +import Lustreiser.ABI.Semantics + +%default total + +-------------------------------------------------------------------------------- +-- A natural decision the Layer-2 model lacked: decidable equality of Input +-------------------------------------------------------------------------------- + +||| `Tick` is not `Reset`. Top-level `impossible` clause (Idris2 0.7.0 idiom; +||| no nested case-of-impossible). +export +tickNotReset : Tick = Reset -> Void +tickNotReset Refl impossible + +||| Sound + complete decision procedure for input equality. `Yes` carries a +||| real `Refl`; each `No` carries a genuine refutation. This is exactly the +||| boolean clock test the per-tick semantics branches on. +public export +decEqInput : (i, j : Input) -> Dec (i = j) +decEqInput Tick Tick = Yes Refl +decEqInput Reset Reset = Yes Refl +decEqInput Tick Reset = No tickNotReset +decEqInput Reset Tick = No (\eq => tickNotReset (sym eq)) + +-------------------------------------------------------------------------------- +-- FLAGSHIP THEOREM: `run` is a left action of (List Input) on CounterNode +-------------------------------------------------------------------------------- + +||| COMPOSITION / FOLD-FUSION (the Layer-3 flagship law). +||| +||| Running the concatenation `xs ++ ys` from state `c` equals running `ys` +||| from the state reached after running `xs`. This makes `run` a monoid +||| action of the free monoid of input streams on node state — the precise +||| algebraic content of "a synchronous node is a deterministic, replayable +||| state machine". +||| +||| Proved by genuine INDUCTION over the prefix `xs`: the cons step is closed +||| by the inductive hypothesis applied to `step x c` (NOT by `cong` over +||| `run`), so this is a real structural proof, deeper than Layer 2's `cong`. +public export +runAppend : (xs, ys : List Input) -> (c : CounterNode) -> + run (xs ++ ys) c = run ys (run xs c) +runAppend [] ys c = Refl +runAppend (x :: xs) ys c = runAppend xs ys (step x c) + +-------------------------------------------------------------------------------- +-- Operational corollaries of the action law +-------------------------------------------------------------------------------- + +||| Single-tick decomposition: running `i :: is` is running `is` after the +||| one-tick transition. The basic operational unfold (holds definitionally). +public export +runConsSplit : (i : Input) -> (is : List Input) -> (c : CounterNode) -> + run (i :: is) c = run is (step i c) +runConsSplit i is c = Refl + +||| `run [Reset] c` clears the state to 0 (preserving the static cap), for any +||| node. A direct reading of the reset transition; reused below. +public export +runResetClears : (c : CounterNode) -> state (run [Reset] c) = 0 +runResetClears (MkCounter _ _) = Refl + +||| TRANSITION SOUNDNESS via the flagship law: ANY run whose suffix is a +||| single `Reset` ends in state 0, regardless of the prefix or starting +||| state. Proved THROUGH `runAppend` (replay the prefix to some state, then +||| apply the reset), so it genuinely consumes the Layer-3 theorem. +public export +runEndingInResetIsZero : (xs : List Input) -> (c : CounterNode) -> + state (run (xs ++ [Reset]) c) = 0 +runEndingInResetIsZero xs c = + rewrite runAppend xs [Reset] c in runResetClears (run xs c) + +-------------------------------------------------------------------------------- +-- ORTHOGONAL TRANSITION SOUNDNESS: monotonicity of the saturating successor +-------------------------------------------------------------------------------- + +||| MONOTONICITY of the saturating successor in its counter argument: +||| if `m <= n` then `satInc cap m <= satInc cap n`. This order-preservation +||| property is orthogonal to — and deeper than — the Layer-2 upper bound +||| (which only fixed the top of the range); it is what licenses interval / +||| abstract-interpretation reasoning about the node. +||| +||| Proof strategy: split on the SAME `isLTE (S m) cap` / `isLTE (S n) cap` +||| tests `satInc` itself uses, so every branch reduces. The four cases: +||| * both unsaturated : `S m <= S n` from `m <= n`. +||| * m unsat, n sat : `S m <= cap` directly from the m-side witness. +||| * m sat, n unsat : `cap <= S n`; from `n < cap` (n-side) we get +||| `S n <= cap`, but we need `cap <= S n`; instead +||| this case is impossible — `m <= n` with `n < cap` +||| forces `S m <= cap`, contradicting m-saturation. +||| * both saturated : `cap <= cap` reflexively. +public export +satIncMonotone : (cap : Nat) -> {m, n : Nat} -> LTE m n -> + LTE (satInc cap m) (satInc cap n) +satIncMonotone cap {m} {n} mLEn with (isLTE (S m) cap) + satIncMonotone cap {m} {n} mLEn | Yes smLEcap with (isLTE (S n) cap) + -- both unsaturated: satInc cap m = S m, satInc cap n = S n + satIncMonotone cap {m} {n} mLEn | Yes _ | Yes _ = LTESucc mLEn + -- m unsaturated, n saturated: satInc cap m = S m, satInc cap n = cap; + -- the m-side witness `S m <= cap` is exactly the goal. + satIncMonotone cap {m} {n} mLEn | Yes smLEcap | No _ = smLEcap + satIncMonotone cap {m} {n} mLEn | No smGTcap with (isLTE (S n) cap) + -- m saturated but n unsaturated is impossible: from m <= n we get + -- S m <= S n; with `S n <= cap` (n-side) transitively `S m <= cap`, + -- contradicting `not (S m <= cap)`. + satIncMonotone cap {m} {n} mLEn | No smGTcap | Yes snLEcap = + absurd (smGTcap (transitive (LTESucc mLEn) snLEcap)) + -- both saturated: satInc cap m = cap = satInc cap n. + satIncMonotone cap {m} {n} mLEn | No _ | No _ = reflexive + +||| Consequence at the node level: a `Tick` is monotone on state — if node +||| `c1` has no more count than `c2` (same cap), the same holds after a tick. +||| Connects the arithmetic monotonicity to the actual `step` transition. +public export +stepTickMonotone : (cap : Nat) -> {s1, s2 : Nat} -> LTE s1 s2 -> + LTE (state (step Tick (MkCounter cap s1))) + (state (step Tick (MkCounter cap s2))) +stepTickMonotone cap le = satIncMonotone cap le + +-------------------------------------------------------------------------------- +-- POSITIVE controls (inhabited witnesses / concrete instances) +-------------------------------------------------------------------------------- + +||| Composition law on a concrete split: replaying `[Tick,Tick]` then +||| `[Reset,Tick]` equals replaying the whole four-tick stream. Machine- +||| checked instance of the flagship theorem. +public export +appendWitness : + run ([Tick,Tick] ++ [Reset,Tick]) (MkCounter 3 0) + = run [Reset,Tick] (run [Tick,Tick] (MkCounter 3 0)) +appendWitness = runAppend [Tick,Tick] [Reset,Tick] (MkCounter 3 0) + +||| Reset-suffix soundness on a concrete prefix: a run ending in `Reset` +||| lands on state 0. Consumes `runEndingInResetIsZero` (hence `runAppend`). +public export +resetSuffixWitness : + state (run ([Tick,Tick,Tick] ++ [Reset]) (MkCounter 3 0)) = 0 +resetSuffixWitness = runEndingInResetIsZero [Tick,Tick,Tick] (MkCounter 3 0) + +||| Monotonicity witness: `satInc 3 1 <= satInc 3 2` (i.e. `2 <= 3`). +||| Concrete instance of the order-preservation theorem. +public export +monotoneWitness : LTE (satInc 3 1) (satInc 3 2) +monotoneWitness = satIncMonotone 3 {m = 1} {n = 2} (LTESucc LTEZero) + +-------------------------------------------------------------------------------- +-- NEGATIVE / non-vacuity controls (the bad cases are genuinely refuted) +-------------------------------------------------------------------------------- + +||| Non-vacuity of the action law: the two sides do NOT collapse to a trivial +||| identity. Concretely, replaying the WHOLE stream from the start is NOT the +||| same as replaying only the suffix from the start (the prefix matters): +||| run [Tick,Tick] (MkCounter 3 0) /= run [] (MkCounter 3 0). +||| Were `run` ignoring its prefix, the flagship law would be vacuous. +public export +prefixMatters : + Not (run [Tick,Tick] (MkCounter 3 0) = run [] (MkCounter 3 0)) +prefixMatters Refl impossible + +||| Non-vacuity of `decEqInput`: `Tick` and `Reset` are genuinely distinct, +||| so the decision is not the constant `Yes`. +public export +inputsDistinct : Not (Tick = Reset) +inputsDistinct = tickNotReset + +||| Non-vacuity of monotonicity: the order is NOT degenerate — `satInc 3 0` +||| is strictly below `satInc 3 1` (`1 <= 2` would be the loose bound, but the +||| sharp fact `satInc 3 0 = 1` and `satInc 3 1 = 2` is refuted-as-equal here: +||| they are not equal, so `satInc` is not constant). +public export +satIncNotConstant : Not (satInc 3 0 = satInc 3 1) +satIncNotConstant Refl impossible diff --git a/src/interface/abi/lustreiser-abi.ipkg b/src/interface/abi/lustreiser-abi.ipkg index e3416cb..03b8966 100644 --- a/src/interface/abi/lustreiser-abi.ipkg +++ b/src/interface/abi/lustreiser-abi.ipkg @@ -10,3 +10,4 @@ modules = Lustreiser.ABI.Types , Lustreiser.ABI.Foreign , Lustreiser.ABI.Proofs , Lustreiser.ABI.Semantics + , Lustreiser.ABI.Invariants From e41a975528bfbabc40dd24330b25ccf2a34bca23 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 06:06:05 +0000 Subject: [PATCH 3/3] abi: seal ABI<->FFI seam with Layer 4 soundness proof Add Lustreiser.ABI.FfiSeam proving the FFI result-code encoding is sound: - resultToIntInjective: distinct Result outcomes never collide on the wire - intToResult + resultRoundTrip: faithful/lossless decode (injectivity derived) - positive controls (concrete decodes = Refl) and a non-vacuity negative control (distinct codes have distinct ints, machine-checked) Genuine proof: %default total, no believe_me/postulate/assert_total/idris_crash. Builds clean (idris2 0.7.0) with zero warnings; false seam claim rejected. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- src/interface/abi/Lustreiser/ABI/FfiSeam.idr | 117 +++++++++++++++++++ src/interface/abi/lustreiser-abi.ipkg | 1 + 2 files changed, 118 insertions(+) create mode 100644 src/interface/abi/Lustreiser/ABI/FfiSeam.idr diff --git a/src/interface/abi/Lustreiser/ABI/FfiSeam.idr b/src/interface/abi/Lustreiser/ABI/FfiSeam.idr new file mode 100644 index 0000000..07b3db0 --- /dev/null +++ b/src/interface/abi/Lustreiser/ABI/FfiSeam.idr @@ -0,0 +1,117 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Layer 4 — ABI<->FFI Seam Soundness Proof for Lustreiser +||| +||| 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 +||| supplies the *proof-side* guarantee that the encoding itself is SOUND: +||| +||| (a) `resultToInt` is INJECTIVE — distinct ABI outcomes never collide on +||| the wire (no two `Result` values map to the same C integer). +||| (b) A decoder `intToResult : Bits32 -> Maybe Result` round-trips every +||| `Result` faithfully (`resultRoundTrip`), proving the encoding is +||| lossless; injectivity is then DERIVED from the round-trip. +||| +||| Together these seal the seam: the C integer returned by the Zig FFI +||| faithfully and unambiguously reconstructs the ABI `Result` it came from. +||| +||| Lustreiser defines exactly one FFI result-code encoder (`resultToInt`); +||| there is no `ProofStatus`/`statusToInt` (or other FFI enum encoder), so +||| clause (c) is vacuous here. + +module Lustreiser.ABI.FfiSeam + +import Lustreiser.ABI.Types + +%default total + +-------------------------------------------------------------------------------- +-- Local lemma: Just is injective +-------------------------------------------------------------------------------- + +||| `Just` is injective. Defined locally (Idris2 0.7.0 has no `justInjective` +||| in scope here). The implicit equands are erased to avoid auto-binding a +||| free lowercase name with a warning. +justInj : {0 x, y : t} -> Just x = Just y -> x = y +justInj Refl = Refl + +-------------------------------------------------------------------------------- +-- (b) Faithful decoder and round-trip +-------------------------------------------------------------------------------- + +||| Decode a C integer back into a `Result`. Built with boolean `==` on +||| concrete `Bits32` literals, which reduces definitionally on each constant, +||| so the round-trip `Refl`s 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 DeadlineViolation + else if x == 6 then Just ClockError + else Nothing + +||| Faithful (lossless) encoding: decoding the encoding of any `Result` +||| recovers exactly that `Result`. Each case reduces because `intToResult` +||| branches on concrete `Bits32` literals via boolean `==`. +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 +resultRoundTrip DeadlineViolation = Refl +resultRoundTrip ClockError = Refl + +-------------------------------------------------------------------------------- +-- (a) Injectivity of the encoding (derived from the round-trip) +-------------------------------------------------------------------------------- + +||| The encoding is unambiguous: if two `Result`s encode to the same C +||| integer, they are the same `Result`. Derived cleanly from the round-trip: +||| `intToResult` applied to both sides yields `Just a = Just b`, and +||| `justInj` strips the constructor. +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`. +decodeOk : intToResult 0 = Just Ok +decodeOk = Refl + +||| Decoding 6 yields `ClockError` (the largest code). +decodeClockError : intToResult 6 = Just ClockError +decodeClockError = Refl + +||| An out-of-range code decodes to `Nothing`. +decodeUnknown : intToResult 7 = Nothing +decodeUnknown = Refl + +-------------------------------------------------------------------------------- +-- Negative / non-vacuity control (distinct codes are distinct on the wire) +-------------------------------------------------------------------------------- + +||| Two DISTINCT result codes map to DISTINCT C integers. This is the +||| non-vacuity witness: injectivity would be trivially true if every +||| `Result` collapsed to one integer. `resultToInt Ok` reduces to the +||| primitive `Bits32` literal 0 and `resultToInt Error` to 1; the coverage +||| checker discharges `Refl impossible` for the two distinct constants. +okNotError : Not (resultToInt Ok = resultToInt Error) +okNotError Refl impossible + +||| A second distinct-code witness, away from the 0/1 boundary (5 vs 6). +deadlineNotClock : Not (resultToInt DeadlineViolation = resultToInt ClockError) +deadlineNotClock Refl impossible diff --git a/src/interface/abi/lustreiser-abi.ipkg b/src/interface/abi/lustreiser-abi.ipkg index 03b8966..4b76945 100644 --- a/src/interface/abi/lustreiser-abi.ipkg +++ b/src/interface/abi/lustreiser-abi.ipkg @@ -11,3 +11,4 @@ modules = Lustreiser.ABI.Types , Lustreiser.ABI.Proofs , Lustreiser.ABI.Semantics , Lustreiser.ABI.Invariants + , Lustreiser.ABI.FfiSeam