From ee01db4dc34e457cbc32cfb1b7abd737ea8f075a Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Tue, 27 Oct 2026 05:14:23 +0000
Subject: [PATCH] feat(lang): variables as a parameter; TINI for any decidable
 variable set
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The fragment had two variables, lo and hi, fixed in SecretTypes.Lang, so a
consumer could not add a variable: Lintel's L-7 needed a client-only sink
and its coalition TINI had no variable the coalition cannot see (Lintel
README L-7, A-1; PROOF-STATUS Open, "multiple variables").

The variables are now a record, SecretTypes.Vars (a type and decidable
equality), and SecretTypes.Lang, Typing.Generic, Noninterference.Statement
and Noninterference.Generic take it as their first module parameter, as
they take the Lattice.  A store is a function Var → Nat and update compares
each variable with the written one.  The proof changes in two lemmas only,
confine-assign and tini-assign, which now split on x ≟ᵥ y instead of on
lo/hi; that is the only use of the variables' structure.

SecretTypes.Lang.Two is the two-variable instance (lo, hi, ⟨_,_⟩, low,
high, _≈_), and the two-point development (Typing, Noninterference,
Witness, Countermodels, tests/reject) is unchanged in content and now
imports it.  tests/reject/ThirdVariable checks the rules at three
variables; its corrected form is accepted (checked locally as the
negative control).

Gates, Agda 2.6.4.3:
  scripts/check.sh:        PASS: core proofs and all 3 expected rejections
  scripts/minimal-laws.sh: PASS: minimal-laws certificate (3 laws, each needed)

PROOF-STATUS: fragment restated, N-7 widened to every Vars, "multiple
variables" removed from Open.  README and its section copy follow.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs
---
 PROOF-STATUS.adoc                             | 32 +++++++------
 README.adoc                                   |  5 +-
 docs/README-section.adoc                      |  5 +-
 src/SecretTypes/All.agda                      |  2 +
 src/SecretTypes/Countermodels.agda            | 10 ++--
 src/SecretTypes/Lang.agda                     | 47 +++++++++----------
 src/SecretTypes/Lang/Two.agda                 | 43 +++++++++++++++++
 src/SecretTypes/Noninterference.agda          |  4 +-
 src/SecretTypes/Noninterference/Generic.agda  | 35 +++++++-------
 .../Noninterference/Statement.agda            |  8 ++--
 src/SecretTypes/Typing.agda                   |  4 +-
 src/SecretTypes/Typing/Generic.agda           |  7 ++-
 src/SecretTypes/Vars.agda                     | 20 ++++++++
 src/SecretTypes/Witness.agda                  |  2 +-
 tests/reject/ExplicitFlow.agda                |  2 +-
 tests/reject/ImplicitFlow.agda                |  2 +-
 tests/reject/ThirdVariable.agda               | 37 +++++++++++++++
 17 files changed, 188 insertions(+), 77 deletions(-)
 create mode 100644 src/SecretTypes/Lang/Two.agda
 create mode 100644 src/SecretTypes/Vars.agda
 create mode 100644 tests/reject/ThirdVariable.agda

diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 1fb7d1f..e62b723 100644
--- a/PROOF-STATUS.adoc
+++ b/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.
diff --git a/README.adoc b/README.adoc
index d0338a6..ef90492 100644
--- a/README.adoc
+++ b/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
diff --git a/docs/README-section.adoc b/docs/README-section.adoc
index 824a15b..04abf0c 100644
--- a/docs/README-section.adoc
+++ b/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
diff --git a/src/SecretTypes/All.agda b/src/SecretTypes/All.agda
index a6847a6..55e7457 100644
--- a/src/SecretTypes/All.agda
+++ b/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
diff --git a/src/SecretTypes/Countermodels.agda b/src/SecretTypes/Countermodels.agda
index a27dbf0..ac74784 100644
--- a/src/SecretTypes/Countermodels.agda
+++ b/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
diff --git a/src/SecretTypes/Lang.agda b/src/SecretTypes/Lang.agda
index 53bfda2..b8028c9 100644
--- a/src/SecretTypes/Lang.agda
+++ b/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,8 +37,7 @@ 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
@@ -48,10 +45,15 @@ 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'
diff --git a/src/SecretTypes/Lang/Two.agda b/src/SecretTypes/Lang/Two.agda
new file mode 100644
index 0000000..836b3e8
--- /dev/null
+++ b/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'
diff --git a/src/SecretTypes/Noninterference.agda b/src/SecretTypes/Noninterference.agda
index 7233849..4760de3 100644
--- a/src/SecretTypes/Noninterference.agda
+++ b/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
diff --git a/src/SecretTypes/Noninterference/Generic.agda b/src/SecretTypes/Noninterference/Generic.agda
index 2afe960..fe0c1d5 100644
--- a/src/SecretTypes/Noninterference/Generic.agda
+++ b/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.
diff --git a/src/SecretTypes/Noninterference/Statement.agda b/src/SecretTypes/Noninterference/Statement.agda
index ba856d9..509958d 100644
--- a/src/SecretTypes/Noninterference/Statement.agda
+++ b/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.
diff --git a/src/SecretTypes/Typing.agda b/src/SecretTypes/Typing.agda
index 1635e81..d50cd42 100644
--- a/src/SecretTypes/Typing.agda
+++ b/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
diff --git a/src/SecretTypes/Typing/Generic.agda b/src/SecretTypes/Typing/Generic.agda
index 177e5b0..9da3ae6 100644
--- a/src/SecretTypes/Typing/Generic.agda
+++ b/src/SecretTypes/Typing/Generic.agda
@@ -7,16 +7,19 @@
 -- program-counter label.  The rules use the operations only, no laws, so a
 -- structure that breaks a law still has these rules
 -- (SecretTypes.Countermodels).
-open import SecretTypes.Lang
+open import SecretTypes.Vars
 
 module SecretTypes.Typing.Generic
+  (𝓥 : Vars)                     -- the variables
   {Carrier : Set}
   (_⊑_ : Carrier → Carrier → Set)
   (_⊔_ : Carrier → Carrier → Carrier)
   (⊥ₗ : Carrier)                 -- the label of a literal
-  (label : Var → Carrier)        -- the label of each variable
+  (label : Vars.Var 𝓥 → Carrier) -- the label of each variable
   where
 
+open import SecretTypes.Lang 𝓥
+
 -- Module parameters take no fixity, so joins and flows are parenthesised.
 
 -- Classify expressions with ⊥ₗ for literals and label for variables,
diff --git a/src/SecretTypes/Vars.agda b/src/SecretTypes/Vars.agda
new file mode 100644
index 0000000..8928de8
--- /dev/null
+++ b/src/SecretTypes/Vars.agda
@@ -0,0 +1,20 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+--
+-- The variables of the language: any type with decidable equality.  The
+-- language (SecretTypes.Lang), typing and TINI are stated over a value of
+-- this record, as they are over the Lattice record; the two-point
+-- development uses the two variables lo and hi (SecretTypes.Lang.Two), a
+-- consumer names its own.  Decidable equality is what a store update needs
+-- to tell the written variable from the others; nothing else is asked of
+-- the variables.
+module SecretTypes.Vars where
+
+open import SecretTypes.Prelude
+
+record Vars : Set₁ where
+  infix 4 _≟ᵥ_
+  field
+    Var  : Set
+    _≟ᵥ_ : (x y : Var) → Dec (x ≡ y)
diff --git a/src/SecretTypes/Witness.agda b/src/SecretTypes/Witness.agda
index cafb327..20cb31d 100644
--- a/src/SecretTypes/Witness.agda
+++ b/src/SecretTypes/Witness.agda
@@ -6,7 +6,7 @@ module SecretTypes.Witness where
 
 open import SecretTypes.Prelude
 open import SecretTypes.Lattice
-open import SecretTypes.Lang
+open import SecretTypes.Lang.Two
 open import SecretTypes.Typing
 open import SecretTypes.Noninterference
 
diff --git a/tests/reject/ExplicitFlow.agda b/tests/reject/ExplicitFlow.agda
index 76541bf..4061890 100644
--- a/tests/reject/ExplicitFlow.agda
+++ b/tests/reject/ExplicitFlow.agda
@@ -3,7 +3,7 @@
 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 module ExplicitFlow where
 open import SecretTypes.Lattice
-open import SecretTypes.Lang
+open import SecretTypes.Lang.Two
 open import SecretTypes.Typing
 
 -- Must fail: assigning the secret variable to the public one needs H ⊑ L.
diff --git a/tests/reject/ImplicitFlow.agda b/tests/reject/ImplicitFlow.agda
index 1e8e65a..5d1fea7 100644
--- a/tests/reject/ImplicitFlow.agda
+++ b/tests/reject/ImplicitFlow.agda
@@ -3,7 +3,7 @@
 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 module ImplicitFlow where
 open import SecretTypes.Lattice
-open import SecretTypes.Lang
+open import SecretTypes.Lang.Two
 open import SecretTypes.Typing
 
 -- Must fail: branching on the secret raises the program counter to H, so
diff --git a/tests/reject/ThirdVariable.agda b/tests/reject/ThirdVariable.agda
new file mode 100644
index 0000000..f5265fa
--- /dev/null
+++ b/tests/reject/ThirdVariable.agda
@@ -0,0 +1,37 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+module ThirdVariable where
+open import SecretTypes.Prelude
+open import SecretTypes.Vars
+open import SecretTypes.Lattice
+
+-- Three variables: the rules are not tied to lo and hi.
+data V : Set where
+  a b c : V
+
+_≟V_ : (x y : V) → Dec (x ≡ y)
+a ≟V a = yes refl
+a ≟V b = no λ ()
+a ≟V c = no λ ()
+b ≟V a = no λ ()
+b ≟V b = yes refl
+b ≟V c = no λ ()
+c ≟V a = no λ ()
+c ≟V b = no λ ()
+c ≟V c = yes refl
+
+three : Vars
+three = record { Var = V ; _≟ᵥ_ = _≟V_ }
+
+label : V → Label
+label a = L
+label b = H
+label c = L
+
+open import SecretTypes.Lang three
+open import SecretTypes.Typing.Generic three _⊑_ _⊔_ L label
+
+-- Must fail: copying the secret b into the public c needs H ⊑ L.
+invalid : L ⊢ (c ≔ var b)
+invalid = assign L⊑L