feat(lang): variables as a parameter; TINI for any decidable variable set

PROOF-STATUS.adoc

@@ -1,6 +1,6 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 = secret-types — Proof Status
-:revdate: 2026-10-19
+:revdate: 2026-10-27
 
 Statuses: PROVEN / TESTED / ASSUMED / DESIGNED / OPEN. Every PROVEN line
 names its module; all modules are `--safe --without-K --no-libraries`,
@@ -12,18 +12,20 @@ whose log ends `PASS: minimal-laws certificate (3 laws, each needed)`.
 
 == Fragment (stated before the claims)
 
-Two variables, `lo` and `hi`; naturals; expressions `lit`, `var`, `plus`;
-commands `skip`, assignment, sequence, `ifz`, `while`; fuel-indexed big-step
-semantics (`nothing` when fuel runs out). Volpano–Smith typing with a
-program-counter label over any instance of the `Lattice` record
-(`SecretTypes.Lattice.Record`), with the variables' labels a parameter
-`label : Var → Carrier`. An observer is a down-closed set of labels; the
-principal observer at `o` sees exactly the labels `ℓ ⊑ o`. The two-point
-lattice `L ⊑ H` is the first instance (`Lattice.two-point`), with `lo`
-labelled `L` and `hi` labelled `H`, and its public observer is the principal
-observer at `L`. Not in the fragment: n variables, declassification,
-procedures, concurrency, timing. Termination is the one channel the theorem
-names as open.
+Variables of any type with decidable equality (the `Vars` record,
+`SecretTypes.Vars`), a store giving each a natural; expressions `lit`,
+`var`, `plus`; commands `skip`, assignment, sequence, `ifz`, `while`;
+fuel-indexed big-step semantics (`nothing` when fuel runs out).
+Volpano–Smith typing with a program-counter label over any instance of the
+`Lattice` record (`SecretTypes.Lattice.Record`), with the variables' labels
+a parameter `label : Var → Carrier`. An observer is a down-closed set of
+labels; the principal observer at `o` sees exactly the labels `ℓ ⊑ o`. The
+two-point development uses two variables, `lo` and `hi`
+(`SecretTypes.Lang.Two`), and the two-point lattice `L ⊑ H`
+(`Lattice.two-point`), with `lo` labelled `L` and `hi` labelled `H`; its
+public observer is the principal observer at `L`. Not in the fragment:
+declassification, procedures, concurrency, timing. Termination is the one
+channel the theorem names as open.
 
 == Claims
 
@@ -36,7 +38,7 @@ names as open.
 | N-4 | The typing side-condition is load-bearing: an explicit flow and an implicit flow are each refused (`L != H` at the `⊑` obligation) *and* each actually leaks from low-equivalent stores | TESTED (`tests/reject/ExplicitFlow`, `ImplicitFlow`; `Witness.explicit-leaks`, `implicit-leaks`)
 | N-5 | Termination-insensitivity is real, not vacuous: a well-typed program spins on one secret and stops on another; TINI says nothing about that pair, by design | TESTED (`Witness.secret-loop-spins/stops`)
 | N-6 | Laws census: generic TINI uses exactly `⊔-upper₁`, `⊔-upper₂` and the observer's down-closure; principal observers add `⊑-trans`, which is what makes "flows to `o`" down-closed. It uses no decidability (of `⊑` or of observers), no `⊥ ⊑ x` (`⊥ₗ` labels literals and needs no law), no reflexivity, antisymmetry, leastness of `⊔` or top | TESTED (`scripts/minimal-laws.sh`: `Noninterference.Generic` checks against `tests/minimal-laws`, a record with only those three laws; removing any one of them is refused; prints `PASS: minimal-laws certificate (3 laws, each needed)`)
-| N-7 | *TINI over the record*: for every `Lattice`, labelling `label` and down-closed observer `V`, two finishing runs of a well-typed command from stores agreeing on what `V` sees end agreeing on it, fuels independent | PROVEN (`Noninterference.Generic.tini : (V : Observer 𝓛) → TINI (Observer.sees V)`; statement `Noninterference.Statement.TINI`)
+| N-7 | *TINI over the record*: for every set of variables with decidable equality, `Lattice`, labelling `label` and down-closed observer `V`, two finishing runs of a well-typed command from stores agreeing on what `V` sees end agreeing on it, fuels independent. Of the variables the proof uses only decidable equality, to tell the written variable from the rest | PROVEN (`Noninterference.Generic.tini : (V : Observer 𝓛) → TINI (Observer.sees V)`, module parameters `𝓥 : Vars`, `𝓛`, `label`; statement `Noninterference.Statement.TINI`); the rules at three variables refuse a flow into a third (`tests/reject/ThirdVariable`, TESTED)
 | N-8 | Each census law is necessary: dropping `⊔-upper₁`, `⊔-upper₂` or observer down-closure, with the others kept and the typing rules unchanged, admits a well-typed program that leaks. `⊑-trans` is necessary for principal observers: without it "flows to `o`" can fail to be down-closed, and TINI fails for that observer | PROVEN (`Countermodels.NoUpper₁.refutes`, `NoUpper₂.refutes`, `NoDownClosure.refutes`; `NoTrans.refutes` for the principal observer; each `¬ TINI _`)
 |===
 
@@ -69,4 +71,4 @@ double negation.
   N-7 already covers it, but no union combinator or coalition instance is
   stated here. In a reader-set lattice a coalition is not a principal
   observer.
-* Declassification; multiple variables.
+* Declassification.

README.adoc

@@ -46,8 +46,9 @@ and shown to leak by computation (`tests/reject/`, `Witness.agda`). Since
 `Lattice` record and any down-closed observer
 (`src/SecretTypes/Noninterference/Generic.agda`), and the laws the proof
 uses are certified (`scripts/minimal-laws.sh`) and each shown necessary
-(`Countermodels.agda`). The fragment is two variables with a `while`
-language and fuel semantics; see link:PROOF-STATUS.adoc[]. Termination is
+(`Countermodels.agda`). The fragment is a `while` language with fuel
+semantics over any variables with decidable equality (two, `lo` and `hi`,
+in the two-point development); see link:PROOF-STATUS.adoc[]. Termination is
 the channel the theorem leaves open, by name.
 
 Conjecture (not claimed): for a well-typed program, the public observer's

docs/README-section.adoc

@@ -9,8 +9,9 @@ and shown to leak by computation (`tests/reject/`, `Witness.agda`). Since
 `Lattice` record and any down-closed observer
 (`src/SecretTypes/Noninterference/Generic.agda`), and the laws the proof
 uses are certified (`scripts/minimal-laws.sh`) and each shown necessary
-(`Countermodels.agda`). The fragment is two variables with a `while`
-language and fuel semantics; see link:PROOF-STATUS.adoc[]. Termination is
+(`Countermodels.agda`). The fragment is a `while` language with fuel
+semantics over any variables with decidable equality (two, `lo` and `hi`,
+in the two-point development); see link:PROOF-STATUS.adoc[]. Termination is
 the channel the theorem leaves open, by name.
 
 Conjecture (not claimed): for a well-typed program, the public observer's

src/SecretTypes/All.agda

@@ -4,7 +4,9 @@ module SecretTypes.All where
 import SecretTypes.Prelude
 import SecretTypes.Lattice.Record
 import SecretTypes.Lattice
+import SecretTypes.Vars
 import SecretTypes.Lang
+import SecretTypes.Lang.Two
 import SecretTypes.Typing.Generic
 import SecretTypes.Typing
 import SecretTypes.Noninterference.Statement

src/SecretTypes/Countermodels.agda

@@ -23,7 +23,7 @@
 module SecretTypes.Countermodels where
 
 open import SecretTypes.Prelude
-open import SecretTypes.Lang hiding (_≈_)
+open import SecretTypes.Lang.Two hiding (_≈_)
 open import SecretTypes.Lattice using (Label; L; H; _⊑_; L⊑L; L⊑H; H⊑H; _⊔_)
 
 private
@@ -58,7 +58,7 @@ module NoUpper₁ where
   not-upper₁ h with h H L
   ... | ()
 
-  open import SecretTypes.Noninterference.Statement _⊑_ _⊔ʳ_ L std
+  open import SecretTypes.Noninterference.Statement two _⊑_ _⊔ʳ_ L std
 
   -- Reveal whether hi is zero by writing 0 or 1 to lo.
   implicit : Cmd
@@ -95,7 +95,7 @@ module NoUpper₂ where
   not-upper₂ h with h L H
   ... | ()
 
-  open import SecretTypes.Noninterference.Statement _⊑_ _⊔ˡ_ L std
+  open import SecretTypes.Noninterference.Statement two _⊑_ _⊔ˡ_ L std
 
   -- Copy the secret value directly into the public variable.
   explicit : Cmd
@@ -128,7 +128,7 @@ module NoDownClosure where
   not-down-closed h with h L⊑H refl
   ... | ()
 
-  open import SecretTypes.Noninterference.Statement _⊑_ _⊔_ L std
+  open import SecretTypes.Noninterference.Statement two _⊑_ _⊔_ L std
 
   -- Copy the unseen lo value into the seen variable hi.
   up : Cmd
@@ -238,7 +238,7 @@ module NoTrans where
   label lo = M
   label hi = H′
 
-  open import SecretTypes.Noninterference.Statement _≤_ _∨_ B label
+  open import SecretTypes.Noninterference.Statement two _≤_ _∨_ B label
 
   -- Copy hi at H′ into lo at M, along an allowed flow.
   explicit : Cmd

src/SecretTypes/Lang.agda

@@ -2,27 +2,25 @@
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 --
--- A small while-language with two variables, lo and hi, and a
--- fuel-indexed big-step semantics.  Fuel is what makes "termination-
--- insensitive" a real qualifier: a loop that does not finish within the
--- fuel returns `nothing`, and the theorem is stated only for runs that
--- return `just`.
-module SecretTypes.Lang where
-
+-- A small while-language over any variables with decidable equality
+-- (SecretTypes.Vars), with a fuel-indexed big-step semantics.  Fuel is what
+-- makes "termination-insensitive" a real qualifier: a loop that does not
+-- finish within the fuel returns `nothing`, and the theorem is stated only
+-- for runs that return `just`.  The two-variable instance is
+-- SecretTypes.Lang.Two.
 open import SecretTypes.Prelude
+open import SecretTypes.Vars
+
+module SecretTypes.Lang (𝓥 : Vars) where
 
-data Var : Set where
-  lo hi : Var
+open Vars 𝓥 public
 
 -- Variables carry no label here: the labelling is a parameter of typing
 -- (SecretTypes.Typing.Generic), and the two-point one is SecretTypes.Typing.label.
 
-record Store : Set where
-  constructor ⟨_,_⟩
-  field
-    low  : Nat
-    high : Nat
-open Store public
+-- A store gives every variable its current value.
+Store : Set
+Store = Var → Nat
 
 data Expr : Set where
   lit  : Nat → Expr
@@ -39,19 +37,23 @@ data Cmd : Set where
 
 -- Read a variable's current value from the store.
 read : Store → Var → Nat
-read s lo = low s
-read s hi = high s
+read s x = s x
 
 -- Evaluate an expression using the store's current variable values.
 eval : Store → Expr → Nat
 eval s (lit n)    = n
 eval s (var x)    = read s x
 eval s (plus a b) = eval s a + eval s b
 
--- Return a store with the selected variable replaced, preserving the other.
+-- The first value when the decision holds, the second otherwise.
+select : ∀ {P : Set} → Dec P → Nat → Nat → Nat
+select (yes _) n _ = n
+select (no  _) _ m = m
+
+-- Return a store with the selected variable replaced, preserving the others:
+-- each variable is compared with the written one.
 update : Var → Nat → Store → Store
-update lo n ⟨ l , h ⟩ = ⟨ n , h ⟩
-update hi n ⟨ l , h ⟩ = ⟨ l , n ⟩
+update x n s y = select (x ≟ᵥ y) n (s y)
 
 -- exec fuel c s: `just t` if c runs to completion within fuel, else `nothing`.
 -- Fuel bounds recursive loop evaluation: each while consumes one unit,
@@ -80,8 +82,3 @@ execIf fuel (suc _) c₁ c₂ s = exec fuel c₂ s
 
 execWhile fuel zero    e c s = bind (exec fuel c s) (exec fuel (while e c))
 execWhile fuel (suc _) e c s = just s
-
--- Low-equivalence: the public observer sees the same thing.
-infix 4 _≈_
-_≈_ : Store → Store → Set
-s ≈ s' = low s ≡ low s'

src/SecretTypes/Lang/Two.agda

@@ -0,0 +1,43 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+--
+-- The language at two variables, lo and hi: the first instance of
+-- SecretTypes.Vars, and the fragment the two-point development
+-- (SecretTypes.Typing, SecretTypes.Noninterference, SecretTypes.Witness,
+-- SecretTypes.Countermodels) is stated in.
+module SecretTypes.Lang.Two where
+
+open import SecretTypes.Prelude
+open import SecretTypes.Vars
+
+data Var : Set where
+  lo hi : Var
+
+infix 4 _≟ᵥ_
+-- Decide equality of the two variables.
+_≟ᵥ_ : (x y : Var) → Dec (x ≡ y)
+lo ≟ᵥ lo = yes refl
+lo ≟ᵥ hi = no λ ()
+hi ≟ᵥ lo = no λ ()
+hi ≟ᵥ hi = yes refl
+
+two : Vars
+two = record { Var = Var ; _≟ᵥ_ = _≟ᵥ_ }
+
+open import SecretTypes.Lang two public hiding (Var; _≟ᵥ_)
+
+-- The store with lo at l and hi at h.
+⟨_,_⟩ : Nat → Nat → Store
+⟨ l , h ⟩ lo = l
+⟨ l , h ⟩ hi = h
+
+-- The two variables' values, by name.
+low high : Store → Nat
+low  s = s lo
+high s = s hi
+
+-- Low-equivalence: the public observer sees the same thing.
+infix 4 _≈_
+_≈_ : Store → Store → Set
+s ≈ s' = low s ≡ low s'

src/SecretTypes/Noninterference.agda

@@ -22,9 +22,9 @@ module SecretTypes.Noninterference where
 open import SecretTypes.Prelude
 open import SecretTypes.Lattice
 open import SecretTypes.Lattice.Record using (Observer; principal)
-open import SecretTypes.Lang
+open import SecretTypes.Lang.Two
 open import SecretTypes.Typing
-import SecretTypes.Noninterference.Generic two-point label as G
+import SecretTypes.Noninterference.Generic two two-point label as G
 
 -- The public observer sees exactly the labels that flow to L.
 public-observer : Observer two-point

src/SecretTypes/Noninterference/Generic.agda

@@ -7,9 +7,9 @@
 --
 --   tini V : TINI (sees V)
 --
--- Instantiate with a lattice and a labelling of the variables:
+-- Instantiate with variables, a lattice and a labelling of the variables:
 --
---   open import SecretTypes.Noninterference.Generic 𝓛 label
+--   open import SecretTypes.Noninterference.Generic 𝓥 𝓛 label
 --
 -- which also brings the typing rules and the statement into scope.  A
 -- principal observer (SecretTypes.Lattice.Record.principal) is the usual
@@ -22,15 +22,18 @@
 -- the two runs may branch differently the proof case-splits on whether V
 -- sees the branch label.  That split needs no decidability: the goal is an
 -- equation between naturals, so it is stable, and excluded middle holds
--- under double negation.
+-- under double negation.  Of the variables only decidable equality is
+-- used, to tell the written variable from the rest of the store.
 open import SecretTypes.Prelude
+open import SecretTypes.Vars
 open import SecretTypes.Lattice.Record
-open import SecretTypes.Lang hiding (_≈_)
 
-module SecretTypes.Noninterference.Generic (𝓛 : Lattice) (label : Var → Lattice.Carrier 𝓛) where
+module SecretTypes.Noninterference.Generic
+  (𝓥 : Vars) (𝓛 : Lattice) (label : Vars.Var 𝓥 → Lattice.Carrier 𝓛) where
 
 open Lattice 𝓛
-open import SecretTypes.Noninterference.Statement _⊑_ _⊔_ ⊥ₗ label public
+open import SecretTypes.Lang 𝓥
+open import SecretTypes.Noninterference.Statement 𝓥 _⊑_ _⊔_ ⊥ₗ label public
 
 module _ (V : Observer 𝓛) where
   open Observer V
@@ -69,12 +72,12 @@ module _ (V : Observer 𝓛) where
   ----------------------------------------------------------------------
   private
     -- An assignment allowed under an unseen counter targets an unseen
-    -- variable, so every seen variable keeps its value.
+    -- variable, so every seen variable keeps its value: a seen variable is
+    -- not the written one.
     confine-assign : ∀ {pc} x e n s → ¬ sees pc → (pc ⊔ lab e) ⊑ label x → update x n s ≈ s
-    confine-assign lo e n s np ok lo v = ⊥-elim (unseen-⊔ (lab e) np (sees-↓ ok v))
-    confine-assign lo e n s np ok hi v = refl
-    confine-assign hi e n s np ok lo v = refl
-    confine-assign hi e n s np ok hi v = ⊥-elim (unseen-⊔ (lab e) np (sees-↓ ok v))
+    confine-assign x e n s np ok y v with x ≟ᵥ y
+    ... | yes refl = ⊥-elim (unseen-⊔ (lab e) np (sees-↓ ok v))
+    ... | no  _    = refl
 
   -- Confinement: under a program counter V cannot see, nothing V sees
   -- changes.  Requires evidence that execution finishes with the fuel.
@@ -113,13 +116,13 @@ module _ (V : Observer 𝓛) where
   ----------------------------------------------------------------------
   private
     -- An allowed assignment to a seen variable assigns an expression whose
-    -- label V sees, so both runs assign the same value.
+    -- label V sees, so both runs assign the same value; every other
+    -- variable keeps the agreement it had.
     tini-assign : ∀ {pc} x e {s s'} → (pc ⊔ lab e) ⊑ label x → s ≈ s'
                 → update x (eval s e) s ≈ update x (eval s' e) s'
-    tini-assign lo e ok eq lo v = eval-low e (sees-↓ (⊔-upper₂ _ _) (sees-↓ ok v)) eq
-    tini-assign lo e ok eq hi v = eq hi v
-    tini-assign hi e ok eq lo v = eq lo v
-    tini-assign hi e ok eq hi v = eval-low e (sees-↓ (⊔-upper₂ _ _) (sees-↓ ok v)) eq
+    tini-assign x e ok eq y v with x ≟ᵥ y
+    ... | yes refl = eval-low e (sees-↓ (⊔-upper₂ _ _) (sees-↓ ok v)) eq
+    ... | no  _    = eq y v
 
   -- Finishing runs of a well-typed command preserve agreement for V.
   -- The fuel bounds may differ; runs returning nothing are not covered.

src/SecretTypes/Noninterference/Statement.agda

@@ -8,17 +8,19 @@
 -- law; SecretTypes.Noninterference.Generic proves it for every Lattice and
 -- every down-closed observer.
 open import SecretTypes.Prelude
-open import SecretTypes.Lang hiding (_≈_)
+open import SecretTypes.Vars
 
 module SecretTypes.Noninterference.Statement
+  (𝓥 : Vars)
   {Carrier : Set}
   (_⊑_ : Carrier → Carrier → Set)
   (_⊔_ : Carrier → Carrier → Carrier)
   (⊥ₗ : Carrier)
-  (label : Var → Carrier)
+  (label : Vars.Var 𝓥 → Carrier)
   where
 
-open import SecretTypes.Typing.Generic _⊑_ _⊔_ ⊥ₗ label public
+open import SecretTypes.Lang 𝓥
+open import SecretTypes.Typing.Generic 𝓥 _⊑_ _⊔_ ⊥ₗ label public
 
 -- Two stores agree for an observer when they agree on every variable whose
 -- label it sees.

src/SecretTypes/Typing.agda

@@ -7,7 +7,7 @@
 module SecretTypes.Typing where
 
 open import SecretTypes.Lattice
-open import SecretTypes.Lang
+open import SecretTypes.Lang.Two
 
 -- Classify the public variable as L and the secret variable as H.
 label : Var → Label
@@ -16,4 +16,4 @@ label hi = H
 
 -- lab classifies an expression as secret exactly when it mentions hi;
 -- literals and expressions using only lo are public.
-open import SecretTypes.Typing.Generic _⊑_ _⊔_ L label public
+open import SecretTypes.Typing.Generic two _⊑_ _⊔_ L label public