Repository navigation
feat(lang): variables as a parameter; TINI for any decidable variable set - #13
Merged
Merged
Conversation
… set 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
Contributor
|
No actionable comments were generated in the recent review.
 |
| Layer / File(s) | Summary |
|---|---|
Variable-parameterised language src/SecretTypes/Vars.agda, src/SecretTypes/Lang.agda, src/SecretTypes/Lang/Two.agda, README.adoc, docs/README-section.adoc |
Vars pairs a variable type with decidable equality. Lang uses a function from variables to naturals as its store, and Lang.Two provides the lo/hi instance. The README descriptions now distinguish the general language from that instance. |
Generic typing and noninterference rules src/SecretTypes/Typing/Generic.agda, src/SecretTypes/Noninterference/Statement.agda, src/SecretTypes/Noninterference/Generic.agda, tests/reject/ThirdVariable.agda, PROOF-STATUS.adoc |
The generic typing and noninterference modules take a variable set as a parameter. Assignment proofs use variable equality, and the new three-variable test declares an assignment expected to fail. The proof-status text updates the scope of N-7 and the fragment description. |
Two-variable client updates src/SecretTypes/Typing.agda, src/SecretTypes/Noninterference.agda, src/SecretTypes/Countermodels.agda, src/SecretTypes/Witness.agda, src/SecretTypes/All.agda, tests/reject/ExplicitFlow.agda, tests/reject/ImplicitFlow.agda |
Existing modules and rejection tests use Lang.Two; generic module calls pass two as the variable-set argument. All imports Vars and Lang.Two. |
Priority:
Estimated code review effort: 3 (Moderate) | ~25 minutes
Change: Feature
Possibly related issues
- feat(lattice): observer union and coalition TINI in the Record module (from Lintel) #12: This change broadens the scope stated for N-7 and updates the Open list, but it does not add the requested union combinators to
Lattice.Record.
Possibly related PRs
- hyperpolymath/secret-types#10: This PR extends the generic typing and noninterference interfaces introduced there with a variable-set parameter and retains the two-variable development as an instance.
Merge Risk: 
ee01d
-
No actionable issue remains identified; the change is mergeable after normal checks.
Pre-merge checks: 
-
Check name Status Explanation Title check The title names the main change: the language and noninterference development now take the variable set as a parameter, with the two-variable proof kept as an instance. It is specific and matches the … Description check The description follows the template. It has Summary, Changes, the RSR Quality Checklist with the required items checked, and Testing, which lists the gate results. It also includes a breaking-change … Linked Issues check Check skipped because no linked issues were found for this pull request. Out of Scope Changes check Check skipped because no linked issues were found for this pull request. Full details: Title check
-
Explanation
The title names the main change: the language and noninterference development now take the variable set as a parameter, with the two-variable proof kept as an instance. It is specific and matches the summary and objectives. The title is 73 characters, which is slightly long but readable.
Full details: Description check
-
Explanation
The description follows the template. It has Summary, Changes, the RSR Quality Checklist with the required items checked, and Testing, which lists the gate results. It also includes a breaking-change note for consumers. The Screenshots section is absent, which is acceptable because it is marked as applicable only when relevant. The CHANGELOG item is left unchecked and the author says it was not touched. That is noted openly.
-
Finishing Touches
-
🛠️ Fix failing CI checks
-
- Commit to this branch
- Create a new PR
-
- Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.
Comment @coderabbitai help to get the list of available commands.
Merged
9 of 10 tasks
|
Owner
Author
|
Two checks are red on
Both come from secret-types never having been minted from rsr-template-repo; Lintel needed the same mint in metadatastician/lintel#3. I have no fix to port. Doing the mint here is the owner's call and a change separate from this one. I'm not re-running these checks, because they fail the same way on The check this PR does own is Generated by Claude Code |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
hyperpolymath
added a commit
to metadatastician/lintel
that referenced
this pull request
Oct 27, 2026
…full (#17) ## Summary Stacked on [hyperpolymath/secret-types#13](hyperpolymath/secret-types#13), which makes the variables a parameter. Pinned to that branch's commit `ee01db4` for now; I re-pin to the merge commit once it lands, and this stays a draft until then. Lintel now names its own variables: `addr` (the address), `qn` (the query name) and `local`, the client's local state, labelled client-only. That closes the two scope caveats #14 recorded: - **L-7** had only the corollary half. With two incomparable fields no typed command moves information between them at all, so "no command writes the link" followed from that. With a client-only variable the informative statement holds and is not vacuous: `link-written-to-local` (a typed write depending on both fields targets `local` and nothing else) and `link-writable` (a typed command does write the link into `local`). - **A-1**: `tini-coalition proxy target` said no more than determinism, since the coalition saw every variable. It does not see `local` (`coalition-blind`), so it now relates stores that differ there (`coalition-agrees`, `stores-differ`). ## Changes - `src/Lintel/Instance.agda`: `Field`, `_≟f_`, `fields : Vars`, `field-label local = observer client`; `coalition-blind`, `store₀`/`store₁`, `coalition-agrees`, `stores-differ`. Re-exports `SecretTypes.Lang fields`. - `src/Lintel/Composition.agda`: the generic part is over any `Vars` and labelling; `no-link-written` is replaced by `link-written-to-local` and `link-writable`. - `tests/accept/ProgramLinkLocal.agda` (new): the positive control for `tests/reject/ProgramLink.agda`, the same sum written into `local`. The four existing program fixtures move to the new names (`lo`→`addr`, `hi`→`qn`). - `scripts/fetch-siblings.sh`, module pin headers, README footer: secret-types `ccdcb3e` → `ee01db4`. - `README.adoc`: L-6, L-7 and A-1 restated; L-7's scope caveat and A-1's determinism note removed, because what they described no longer holds. Statuses unchanged: L-6/L-7 PROVEN, A-1 ASSUMED. ## RSR Quality Checklist ### Required - [x] Tests pass: `bash scripts/fetch-siblings.sh && bash scripts/check.sh` with a fresh fetch of the pin → `PASS: Lintel proofs, 5 positive control(s), 4 expected rejection(s), negative control`. - [x] Code is formatted. - [x] Linter is clean: `-W error`. - [x] No banned language patterns. - [x] No `unsafe` blocks. - [x] No banned functions; no postulates. - [x] SPDX headers present. - [x] No secrets. ### As Applicable - [x] Documentation updated (README status table). - [ ] `CHANGELOG`: not touched. ## Testing Gate as above. Mutation, checked locally: labelling `local` as the address breaks `coalition-blind` and `link-writable`. `link-written-to-local` alone would still hold under that mutation (its `local` case is `refl`). What carries the content is the pair, and the README says it in those terms. --- _Generated by [Claude Code](https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs)_ Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
enabled auto-merge (squash)
October 27, 2026 05:35
hyperpolymath
disabled auto-merge
October 27, 2026 05:38
hyperpolymath
enabled auto-merge (squash)
October 27, 2026 05:38
Contributor
|
Add Carrot credits or activate Agent usage billing to use Autofix |
Contributor
|
✅ Coding Agent task started: View task and status The task will inspect the CI failures, validate its fix, and commit the fix to this branch automatically.
⏭️ Checks skipped: 4 · already failing on `main` (not caused by this PR)
|
hyperpolymath
disabled auto-merge
October 27, 2026 11:42
hyperpolymath
enabled auto-merge (squash)
October 27, 2026 11:42
hyperpolymath
disabled auto-merge
October 27, 2026 14:32
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes the "multiple variables" item of PROOF-STATUS's Open list. The fragment had two variables,
loandhi, fixed inSecretTypes.Lang, so a consumer could not add one. Lintel needed exactly that: its L-7 had only the corollary half (two incomparable fields, so no typed command moves anything between them), and its coalition TINI had no variable the coalition cannot see, so it said no more than determinism. The consumer change is metadatastician/lintel#17.The variables are now a record, like the lattice:
SecretTypes.Vars(a type and decidable equality), the first module parameter ofLang,Typing.Generic,Noninterference.StatementandNoninterference.Generic.Changes
src/SecretTypes/Vars.agda(new):record VarswithVarand_≟ᵥ_.src/SecretTypes/Lang.agda: parameterised by𝓥 : Vars; a store isVar → Nat;updatecompares each variable with the written one.src/SecretTypes/Noninterference/Generic.agda: the proof changes in two lemmas only,confine-assignandtini-assign, which split onx ≟ᵥ yinstead of onlo/hi. That is the only use of the variables' structure.src/SecretTypes/Lang/Two.agda(new): the two-variable instance (lo,hi,⟨_,_⟩,low,high,_≈_).Typing,Noninterference,Witness,Countermodelsand the two reject fixtures import it; their content is unchanged.tests/reject/ThirdVariable.agda(new): the rules at three variables refuse a flow into a third.PROOF-STATUS.adoc: fragment restated, N-7 widened to everyVars, "multiple variables" removed from Open.README.adocanddocs/README-section.adocfollow.RSR Quality Checklist
Required
scripts/check.sh→PASS: core proofs and all 3 expected rejections;scripts/minimal-laws.sh→PASS: minimal-laws certificate (3 laws, each needed)(Agda 2.6.4.3, the CI pin).-W error, no warnings.unsafeblocks.As Applicable
CHANGELOG: not touched.Testing
Both gates locally, as above.
ThirdVariablewas first refused for the wrong reason (its_≟_clashed with the Prelude's), which the gate caught as an unexpected failure; renamed. Its corrected form (c ≔ var a) is accepted, as the negative control.Downstream: Lintel's full gate passes against this commit fetched fresh by its pin (
PASS: Lintel proofs, 5 positive control(s), 4 expected rejection(s), negative control).Breaking for consumers:
SecretTypes.Langis now a parameterised module, soopen import SecretTypes.LangbecomesSecretTypes.Lang.Two(orSecretTypes.Lang 𝓥), andNoninterference.Generic 𝓛 labelbecomesNoninterference.Generic 𝓥 𝓛 label. Lintel is the only consumer I know of, and it pins by commit.Generated by Claude Code