tini-2026-10-12

.github/CODEOWNERS

@@ -2,13 +2,13 @@
 # CODEOWNERS - Define code review assignments
 # See: https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-code-owners
 #
-# Replace {{OWNER}} with your GitHub username or team
+# Repository owner: hyperpolymath
 
 # Default owners for everything
-* @{{OWNER}}
+* @hyperpolymath
 
 # Security-sensitive files require explicit review
-SECURITY.md @{{OWNER}}
-.github/workflows/ @{{OWNER}}
-Trustfile.a2ml @{{OWNER}}
-.machine_readable/ @{{OWNER}}
+SECURITY.md @hyperpolymath
+.github/workflows/ @hyperpolymath
+Trustfile.a2ml @hyperpolymath
+.machine_readable/ @hyperpolymath

.machine_readable/root-allow.txt

@@ -38,6 +38,10 @@ CLAUDE.md                  # generated arrival pack; the generator, pre-commit a
 Justfile                   # thin; delegates phases to build/just/*.just
 coordination.k9.ncl        # repo-local session binding (template-mandated)
 
+# ─── Project-specific root entries ───────────────────────────────────────────
+PROOF-STATUS.adoc          # project theorem evidence and fragment limits, linked from README.adoc
+secret-types.agda-lib      # Agda discovers library descriptors at the project root
+
 # ─── Conventional dotfiles (tool-required at root) ───────────────────────────
 .editorconfig
 .envrc

PROOF-STATUS.adoc

@@ -0,0 +1,51 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= secret-types — Proof Status
+:revdate: 2026-10-12
+
+Statuses: PROVEN / TESTED / ASSUMED / DESIGNED / OPEN. Every PROVEN line
+names its module; all modules are `--safe --without-K --no-libraries`,
+checked with `--double-check`, no postulates.
+
+== Fragment (stated before the claims)
+
+One public and one secret variable; 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 the two-point lattice. Not in the fragment:
+n variables / arbitrary lattices, declassification, procedures, concurrency,
+timing. Termination is the one channel the theorem names as open.
+
+== Claims
+
+[cols="1,3,1",options="header"]
+|===
+| ID | Claim | Status
+| N-1 | *TINI*: `pc ⊢ c → s ≈ s' → exec n c s ≡ just t → exec n' c s' ≡ just t' → t ≈ t'`, fuels independent | PROVEN (`Noninterference.tini`)
+| N-2 | Public expressions read the same in low-equivalent stores | PROVEN (`eval-low`)
+| N-3 | Confinement: under a secret program counter the public variable is unchanged, loops included | PROVEN (`confine`)
+| 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: the proof uses only the two-point order (`⊔-L₁`, `⊔-L₂`, `H ⊔ y = H`) and decidable zero-testing of naturals; no lattice law beyond that | ASSUMED by inspection (no parametric lattice to certify against yet)
+|===
+
+== Separation from siblings (criterion 2 of the family bar)
+
+* Noninterference is a property of *two* runs. Echo grades, tropical grades
+  and occupancy grades are accumulations over *one* run; none of them can
+  state N-1. That is the separation, and it is why this is a family and not
+  a view. The converse connection — that a well-typed program's low
+  observer has an Echo fibre that does not separate secret inputs — is a
+  CONJECTURE, recorded in the README, not claimed here.
+* A label is not an epistemic standpoint (README). The Kripke frame built
+  for choreographic-types indexes knowledge by *views*; a label indexes
+  *permission to flow*. Nothing here imports epistemic-types, deliberately.
+
+== Open
+
+* Termination-sensitive noninterference (close the named channel): needs a
+  stronger typing rule for `while` on secret guards. Pre-registered:
+  the falsifier is `secret-loop` above, which TSNI must refuse.
+* Arbitrary lattices (parametric in a `Lattice` record, with the census in
+  N-6 then certifiable the way resource-algebra's is).
+* Declassification; multiple variables.
+* CI (`proofs.yml`): DESIGNED until first green run on the 2.6.4.3 pin.

README.adoc

@@ -10,7 +10,7 @@ image:https://img.shields.io/badge/Code-MPL--2.0-blue.svg?logo=mozilla[Code lice
 image:https://img.shields.io/badge/Docs-CC--BY--SA--4.0-blue.svg?logo=creativecommons[Docs licence: CC-BY-SA-4.0,link="https://creativecommons.org/licenses/by-sa/4.0/"]
 
 // ── Status ──────────────────────────────────────────────────────────────────
-image:https://img.shields.io/badge/Stage-specification--only-orange[Specification only: no code, no proofs]
+image:https://img.shields.io/badge/Proof-core_theorem_proven-brightgreen[Core theorem proven,link="PROOF-STATUS.adoc"]
 image:https://img.shields.io/badge/RSR-Rhodium_Standard-9C27B0[Rhodium Standard Repository,link="https://github.com/hyperpolymath/rhodium-standard-repositories"]
 
 Confidentiality labels that constrain value flow, with declassification only at
@@ -38,17 +38,18 @@ this standalone home), the first model, and the explicit non-claims.
 
 == Status
 
-* *Specification only.* There is no `Secret` type, no information-flow
-  calculus, no declassification rule, no noninterference theorem and no
-  cross-repository import in this project.
-* *Minted 2026-10-04 in scope, not yet in scaffolding.* The scope statement and
-  this README are real project content. The RSR template placeholder sweep
-  (`just repo-init`) has not been run across the tree yet, so other files still
-  carry `{{TOKEN}}` template text; that sweep is tracked in
-  link:https://github.com/hyperpolymath/secret-types/issues/2[issue #2].
-* *No progress grade claimed.* A documentation link is not a mechanised
-  dependency; an integration may only be claimed once a real import builds in
-  CI.
+Core theorem PROVEN (2026-10-12): termination-insensitive noninterference
+for the two-point lattice, `src/SecretTypes/Noninterference.agda`
+(`tini`), with the explicit and implicit flows refused by the type system
+and shown to leak by computation (`tests/reject/`, `Witness.agda`). The
+fragment is one public and one secret variable with a `while` language and
+fuel semantics; 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
+Echo fibre over its outputs does not separate secret inputs — the Echo
+reading of noninterference, and the first candidate connection
+Secret → Echo for `nextgen-typing/docs/TYPE-CONNECTIONS.adoc`.
 
 == Where things belong
 

docs/MAINTAINERS.adoc

@@ -12,9 +12,9 @@ earlier duplicates at `.github/MAINTAINERS` and `docs/attribution/MAINTAINERS.ad
 |===
 | Name | Role | Contact
 
-| {{AUTHOR}}
+| Jonathan D.A. Jewell
 | Lead Maintainer
-| https://github.com/{{OWNER}}[@{{OWNER}}]
+| https://github.com/hyperpolymath[@hyperpolymath]
 |===
 
 == Responsibilities

docs/README-section.adoc

@@ -0,0 +1,15 @@
+// Splice into README.adoc, replacing "== Status" (specification only).
+== Status
+
+Core theorem PROVEN (2026-10-12): termination-insensitive noninterference
+for the two-point lattice, `src/SecretTypes/Noninterference.agda`
+(`tini`), with the explicit and implicit flows refused by the type system
+and shown to leak by computation (`tests/reject/`, `Witness.agda`). The
+fragment is one public and one secret variable with a `while` language and
+fuel semantics; 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
+Echo fibre over its outputs does not separate secret inputs — the Echo
+reading of noninterference, and the first candidate connection
+Secret → Echo for `nextgen-typing/docs/TYPE-CONNECTIONS.adoc`.

docs/architecture/REPOSITORY-MAP.adoc

@@ -113,6 +113,10 @@ predecessors did.
 | yes
 | REUSE licence texts, dual-licence model (code MPL-2.0 / docs CC-BY-SA-4.0)
 
+| `PROOF-STATUS.adoc`
+| yes
+| project theorem evidence and fragment limits, linked from README.adoc
+
 | `README.adoc`
 | yes
 | -
@@ -161,6 +165,10 @@ predecessors did.
 | yes
 | repo helper scripts
 
+| `secret-types.agda-lib`
+| yes
+| Agda discovers library descriptors at the project root
+
 | `session/`
 | yes
 | dispatch.sh, custom-checks.k9.ncl, local-hooks.sh

scripts/check.sh

@@ -0,0 +1,36 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Core proofs plus expected rejections.  Pattern: residual-evidence-types.
+set -euo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+export LC_ALL="${LC_ALL:-C.UTF-8}"
+prover="${AGDA:-agda}"
+"$prover" --version
+flags=(--safe --without-K --no-libraries --ignore-interfaces --double-check -i src)
+"$prover" "${flags[@]}" src/SecretTypes/All.agda
+mkdir -p _build/check-logs
+shopt -s nullglob
+rejects=(tests/reject/*.agda)
+shopt -u nullglob
+if (( ${#rejects[@]} == 0 )); then
+  echo 'ERROR: no expected-rejection modules found under tests/reject' >&2
+  exit 1
+fi
+for file in "${rejects[@]}"; do
+  name="$(basename -- "$file" .agda)"
+  log="_build/check-logs/$name.log"
+  if "$prover" "${flags[@]}" -i tests/reject "$file" >"$log" 2>&1; then
+    cat "$log"
+    echo "ERROR: invalid proof accepted: $name" >&2
+    exit 1
+  fi
+  if ! grep -Eq "/$name\.agda:[0-9]+,[0-9]+" "$log" ||
+     ! grep -q 'when checking that' "$log" ||
+     grep -Eq 'Not in scope|Failed to find|Unsolved|Parse error' "$log"; then
+    cat "$log"
+    echo "ERROR: unexpected failure while checking $name" >&2
+    exit 1
+  fi
+  echo "PASS: rejected $name at its invalid declaration"
+done
+echo "PASS: core proofs and all ${#rejects[@]} expected rejections"

secret-types.agda-lib

@@ -0,0 +1,3 @@
+name: secret-types
+include: src
+flags: --safe --without-K

src/SecretTypes/All.agda

@@ -0,0 +1,9 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+module SecretTypes.All where
+import SecretTypes.Prelude
+import SecretTypes.Lattice
+import SecretTypes.Lang
+import SecretTypes.Typing
+import SecretTypes.Noninterference
+import SecretTypes.Witness

src/SecretTypes/Lang.agda

@@ -0,0 +1,86 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+--
+-- A small while-language with one public and one secret variable, 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
+
+open import SecretTypes.Prelude
+open import SecretTypes.Lattice
+
+data Var : Set where
+  lo hi : Var
+
+-- Classify the public variable as L and the secret variable as H.
+label : Var → Label
+label lo = L
+label hi = H
+
+record Store : Set where
+  constructor ⟨_,_⟩
+  field
+    low  : Nat
+    high : Nat
+open Store public
+
+data Expr : Set where
+  lit  : Nat → Expr
+  var  : Var → Expr
+  plus : Expr → Expr → Expr
+
+infixr 5 _﹔_
+data Cmd : Set where
+  skip  : Cmd
+  _≔_   : Var → Expr → Cmd
+  _﹔_   : Cmd → Cmd → Cmd
+  ifz   : Expr → Cmd → Cmd → Cmd      -- if e = 0 then c₁ else c₂
+  while : Expr → Cmd → Cmd            -- while e = 0 do c
+
+-- Evaluate an expression using the store's current variable values.
+eval : Store → Expr → Nat
+eval s (lit n)    = n
+eval s (var lo)   = low s
+eval s (var hi)   = high s
+eval s (plus a b) = eval s a + eval s b
+
+-- Return a store with the selected variable replaced, preserving the other.
+update : Var → Nat → Store → Store
+update lo n ⟨ l , h ⟩ = ⟨ n , h ⟩
+update hi n ⟨ l , h ⟩ = ⟨ l , n ⟩
+
+-- 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,
+-- even when its guard is non-zero.  At zero fuel, while returns `nothing`.
+-- Other commands consume no fuel; sequence reuses it for both commands,
+-- and a loop's body and continuation each receive the remaining fuel.
+exec      : Nat → Cmd → Store → Maybe Store
+-- Run the first branch for guard value zero, otherwise the second, using
+-- the supplied fuel unchanged; return the selected branch's result.
+execIf    : Nat → Nat → Cmd → Cmd → Store → Maybe Store      -- guard value, branches
+-- Continue a loop after its fuel decrement, using the supplied guard value.
+-- Non-zero returns `just s`; zero runs the body then repeats the loop with
+-- the same remaining fuel, re-evaluating e in the updated store.  Return
+-- `nothing` if either the body or the repeated loop exhausts its fuel.
+execWhile : Nat → Nat → Expr → Cmd → Store → Maybe Store     -- remaining fuel, guard value
+
+exec fuel skip          s = just s
+exec fuel (x ≔ e)       s = just (update x (eval s e) s)
+exec fuel (c₁ ﹔ c₂)     s = bind (exec fuel c₁ s) (exec fuel c₂)
+exec fuel (ifz e c₁ c₂) s = execIf fuel (eval s e) c₁ c₂ s
+exec zero       (while e c) s = nothing
+exec (suc fuel) (while e c) s = execWhile fuel (eval s e) e c s
+
+execIf fuel zero    c₁ c₂ s = exec fuel c₁ s
+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/Lattice.agda

@@ -0,0 +1,33 @@
+{-# OPTIONS --safe --without-K #-}
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+-- The two-point lattice Public ⊑ Secret.  A label is a flow constraint, not
+-- an epistemic standpoint (README, "A label is not an epistemic standpoint").
+module SecretTypes.Lattice where
+
+open import SecretTypes.Prelude
+
+data Label : Set where
+  L H : Label        -- L = Public, H = Secret
+
+infix 4 _⊑_
+data _⊑_ : Label → Label → Set where
+  L⊑L : L ⊑ L
+  L⊑H : L ⊑ H
+  H⊑H : H ⊑ H
+
+infixl 6 _⊔_
+-- Combine flow labels: the result is secret if either input is secret.
+_⊔_ : Label → Label → Label
+L ⊔ y = y
+H ⊔ y = H
+
+-- A public join guarantees that its left input is public.
+⊔-L₁ : ∀ {x y} → x ⊔ y ≡ L → x ≡ L
+⊔-L₁ {L} _ = refl
+⊔-L₁ {H} ()
+
+-- A public join guarantees that its right input is public.
+⊔-L₂ : ∀ {x y} → x ⊔ y ≡ L → y ≡ L
+⊔-L₂ {L} e = e
+⊔-L₂ {H} ()