Repository navigation
feat(lattice): parametrise Typing and Noninterference over a Lattice record (LNT-01 sibling) #9
Description
Summary
PROOF-STATUS (at 833715c) lists under Open: "Arbitrary lattices (parametric in a Lattice record, with the census in N-6 then certifiable the way resource-algebra's is)". This issue is that step. It has a first customer waiting.
metadatastician/lintel#2 (LNT-01) adds a privacy lattice whose laws typecheck under --safe --without-K --no-libraries --double-check (Agda 2.6.4.3), in src/Lintel/Lattice.agda:
- Carrier: reader sets over the oblivious-DNS roles {client, proxy, target}, with eight labels.
- Operations: ⊑ is reverse inclusion, ⊔ is intersection, ⊓ is union, ⊥ =
anyoneand ⊤ =no-one. - Shape: joins and meets are proved for every pair, so it is a lattice, not a poset completed by hand.
By owner decision (2026-10-14), Lintel proves the laws as lemmas and holds no copy of the record. The record is defined once, here, and Lintel instantiates it by pin. Lintel's tini instance, and with it its "self-defeating compositions are unconstructible" claim, waits on this issue.
Proof work that applies now
| ID | Claim | Status | Artefact |
|---|---|---|---|
| N-1 | TINI over the two-point lattice | PROVEN | Noninterference.tini (re-checked by Lintel's gate at 833715c) |
| N-6 | laws census: only ⊔-L₁, ⊔-L₂, H ⊔ y = H |
ASSUMED by inspection | nothing parametric to certify against yet |
| — | the same census stated at Lintel's lattice | PROVEN | Lintel ⊔-anyone₁, ⊔-anyone₂, no-one-⊔, anyone-⊔ |
| — | parametric Lattice record |
OPEN | this issue |
Census by inspection (to be certified, not trusted)
This is a reading of Noninterference.agda at 833715c. Each two-point step is listed with the general law it appears to need once the low observer becomes an observer level o, with s ≈ₒ s' meaning the stores agree on every variable x with label x ⊑ o:
| Where | Two-point use | General form | From |
|---|---|---|---|
eval-low (plus) |
⊔-L₁, ⊔-L₂ |
x ⊔ y ⊑ o → x ⊑ o and → y ⊑ o |
⊔ upper bounds + ⊑-trans |
eval-low (lit) |
lab (lit _) = L |
⊥ ⊑ o |
a least element |
tini (assign to the observed variable) |
low-pc : x ⊑ L → x ≡ L |
pc ⊔ lab e ⊑ label x ⊑ o → lab e ⊑ o |
upper bound + trans |
tiniIf / tiniW case split |
ℓ ∈ {L, H} by pattern |
Dec (ℓ ⊑ o) |
decidable order |
confine (secret pc) |
H ⊔ y = H |
pc ⋢ o → pc ⊔ y ⋢ o, and an assignment under pc ⋢ o only reaches variables with label x ⋢ o |
upper bound + trans |
The candidate minimal record is: a carrier, ⊑ with transitivity, ⊔ with both upper-bound laws, ⊥ with ⊥ ⊑ x, and decidable ⊑. By this reading, the proof would not use antisymmetry, leastness of ⊔ or a top. Whether that reading is right is exactly what minimal-laws.sh should settle.
Proposed work
- Record. Add a
Latticerecord (inSecretTypes/Lattice.agdaor a new module) and keep the two-point lattice as its first instance, soWitnessandtests/rejectstay as they are. - Parametrise. Make
TypingandNoninterferencetake the record, an observer level and alabel : Var → Carrierinstead of the fixedL/H. Lintel's labels are per field, solo/hibecome two fields whose labels are parameters. - N-6 ASSUMED → TESTED. Add
scripts/minimal-laws.sh, following the choreographic-types K-4 pattern: checkNoninterferenceagainst a record carrying only the named laws. - Proofs CI.
proofs.ymlis DESIGNED in PROOF-STATUS. The Debian 13 /agda-bin=2.6.4.3-1+b2recipe that choreographic-types and Lintel use would close it.
Acceptance criteria
-
Latticerecord defined once in this repo; the two-point lattice is an instance and N-1…N-5 still hold at it. -
tinistated and proved over the record (observer level and variable labelling as parameters). -
minimal-laws.shpasses against a record with only the census laws (N-6 → TESTED), and fails if one of them is removed. - The commit that lands this is announced on LNT-01 so Lintel can re-pin and instantiate.
Out of scope
TSNI, declassification and multiple variables are each already Open in PROOF-STATUS. Lintel's lattice itself stays in Lintel.
As this lands
Lintel re-pins scripts/fetch-siblings.sh to the landing commit, packages its lemmas as one record value, instantiates tini once per role observer (observer client|proxy|target), and moves its README row from OPEN to PROVEN. Note for that re-pin: Lintel.Lattice declares its own Dec, because SecretTypes.Prelude has none at 833715c. If this work adds Dec to the Prelude, Lintel drops its copy.
Activity
feat(lattice): Lintel's privacy lattice, its laws, and the pinned Agd…
ci: re-pin secret-scanner and hypatia-scan to standards@75bd5994; CI …
docs(lattice): scope N-8 so NoTrans speaks for principal observers only
style(scripts): use [[ ]] for tests in the proof gates (SonarCloud)
chore(agda): stop tracking .agdai interface files
feat(lattice): TINI over a Lattice record and down-closed observers, …
hyperpolymath commentedon Oct 19, 2026
Landed in #10 as
ccdcb3ec42792337a9ab6047e1f99de9d20a4f96, a squash commit signed by GitHub. Its tree is identical to the PR head 9bd1e94, where the Agda proofs job passed in CI.Against the acceptance criteria:
Latticerecord is defined once, and the two-point lattice is an instance. The record is inSecretTypes.Lattice.Recordand the instance isSecretTypes.Lattice.two-point. N-1 to N-5 still hold at it:Noninterference.tini,eval-lowandconfinekeep their original statements, andWitnessandtests/rejectare unchanged.tiniis stated and proved over the record. It isNoninterference.Generic.tini : (V : Observer 𝓛) → TINI (Observer.sees V), with the labellinglabel : Var → Carrieras a module parameter. Observers are down-closed sets of labels;principal ois the "level o" observer.minimal-laws.shpasses with only the census laws and fails if one is removed. N-6 moved ASSUMED → TESTED. The census differs from the hypothesis here:⊔-upper₁,⊔-upper₂and observer down-closure;⊑-transis needed only to buildprincipal;⊥ ⊑ xnor decidable⊑is used.SecretTypes.Countermodelsshows each law is necessary (N-8).Dec(now a hardMultiple definitionserror) and adds a checked instance snippet. A coalition-observer follow-up is Coalition observers: state TINI for colluding roles and narrow assumption A-1 metadatastician/lintel#12.The Prelude gained
⊥-elim,Dec,_≟_,dec-stableand¬¬-dec; Lintel must drop its ownDecwhen it re-pins.Generated by Claude Code