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