feat(lattice): TINI over a Lattice record and down-closed observers, with a certified laws census by hyperpolymath · Pull Request #10 · hyperpolymath/secret-types

hyperpolymath · 2026-10-19T16:54:10Z

Summary

Implements #9. This repo now defines the Lattice record once, states typing and TINI over it, and keeps the two-point lattice as its first instance, so metadatastician/lintel can instantiate the record at its reader-set lattice.

Owner decisions taken before the build:

the record has its own module;
its fields are exactly the measured census;
observers are down-closed sets;
the work ships as one PR.

The census refutes two points of the hypothesis in #9. Generic TINI uses only ⊔-upper₁, ⊔-upper₂ and observer down-closure. Principal observers add ⊑-trans. Neither ⊥ ⊑ x nor decidable ⊑ is used.

Refs #9. This PR does not close #9: its last acceptance item is the announcement on LNT-01.

Changes

ci(proofs) (d6876a4)
- .github/workflows/proofs.yml copies the choreographic-types pattern: a digest-pinned Debian 13 container, agda-bin=2.6.4.3-1+b2, and a SHA-pinned checkout.
- scripts/check.sh gains the version pin, a postulate scan, -W error, and position-checked rejections.
- just test now runs the gate.
- actions.lock onboards proofs.yml and records the checkout SHA pin with ref: v7.0.1.
- It also repairs lock drift already on main: haskell-actions/setup@v2.12.1 and SonarSource/sonarqube-scan-action@v8.3.0 were missing, and v2.12.0 and v8.2.2 were stale. check-lock-sync.sh was red on main at a75798a and is green here.
feat(lattice) (968a419)
- SecretTypes.Lattice.Record defines Lattice (Carrier, _⊑_, _⊔_, ⊥ₗ, ⊑-trans, ⊔-upper₁, ⊔-upper₂), Observer (sees, sees-↓) and principal.
- Typing.Generic holds the typing rules, over the operations plus label : Var → Carrier.
- Noninterference.Statement defines _≈[_]_ and TINI.
- Noninterference.Generic proves tini : (V : Observer 𝓛) → TINI (sees V). It needs no decidability: agreement is stable, and excluded middle holds under ¬¬.
- The two-point modules re-derive tini, eval-low and confine with their original statements. Witness and tests/reject are unchanged.
- The Prelude gains ⊥-elim, Dec, _≟_, dec-stable and ¬¬-dec.
test(lattice) (f149e08)
- scripts/minimal-laws.sh checks sufficiency against tests/minimal-laws, guards against drift from the real record, and ablates each census field; each removal must be refused.
- SecretTypes.Countermodels gives one structure each for NoUpper₁, NoUpper₂ and NoDownClosure: each keeps the other two laws and has a well-typed program that leaks (¬ TINI _).
- A fourth, NoTrans, shows that without ⊑-trans the principal observer need not be down-closed, and TINI fails for it.
- PROOF-STATUS: N-6 moves ASSUMED → TESTED; N-7 and N-8 are new and PROVEN.
ci (17412e2)
- Re-pins secret-scanner.yml and hypatia-scan.yml to standards@75bd5994 and closes the lock for that commit's actions. Both had failed at job setup, on main too, with invalid lockfile pin: standards@da2c748's own lock records the checkout pin with the SHA as ref.
- PROOF-STATUS: CI row DESIGNED → TESTED, citing proofs run 39289501788.
docs(lattice) (6be6f6a): narrows N-8 so NoTrans speaks for principal observers only (CodeRabbit review). No proof changes.
style(scripts) (6be6f6a, 48d9625): named positional parameters and [[ ]] in the gate scripts (SonarCloud). Behaviour unchanged.

RSR Quality Checklist

Required

Tests pass (just test, log below; CI Agda proofs green on every head)
Code is formatted: just fmt-check passes, but just --fmt --check already differs on main, and this PR does not change that
Linter is clean: just quality passes; Agda runs with -W error; SonarCloud reports 0 new issues
No banned language patterns
No unsafe blocks without // SAFETY: comments (none)
No banned functions; no postulates (now gated)
SPDX license headers present on all new/modified source files
No secrets, credentials, or .env files included

As Applicable

.machine_readable/descriptiles/STATE.a2ml: not updated; it still carries the template's state and never recorded TINI
Documentation updated (PROOF-STATUS, README status, docs/README-section)
CHANGELOG: not updated (it is template content; the earlier TINI PR did not update it either)

Testing

Local run: Agda 2.6.4.3 from Ubuntu's agda-bin/libghc-agda-dev 2.6.4.3-1, and just 1.59.0.

Agda version 2.6.4.3
PASS: trusted base (no postulates under src/SecretTypes or tests)
PASS: core proofs (SecretTypes.All, builtins only)
PASS: rejected ExplicitFlow at its invalid declaration
PASS: rejected ImplicitFlow at its invalid declaration
PASS: core proofs and all 2 expected rejections
PASS: census record matches the real record (which adds only ⊑-trans)
PASS: generic TINI typechecks with only ⊔-upper₁ ⊔-upper₂ sees-↓
PASS: without ⊔-upper₁ generic TINI is refused (Not in scope: ⊔-upper₁)
PASS: without ⊔-upper₂ generic TINI is refused (Not in scope: ⊔-upper₂)
PASS: without sees-↓ generic TINI is refused (Not in scope: sees-↓)
PASS: minimal-laws certificate (3 laws, each needed)

I also made each new check fail on purpose, and each one did:

a wrong Agda version;
a postulate under tests/;
a rejection fixture made valid;
a fixture failing for the wrong reason;
an EmptyPrivate warning under -W error;
proofs.yml removed from the lock;
the proof starting to use ⊑-trans;
the real record gaining ⊑-refl;
a census entry the proof does not use.

These also pass: check-lock-sync.sh, check-invisible-characters.sh, check-adoc-renders.sh (asciidoctor 2.0.26) and just validate-repo-map. minimal-laws.sh also passes under mawk, Debian's default awk.

Red checks that are not this PR's (details in the PR comment):

Canon lockstep: a template-inherited job that fetches this repo's SHA from rsr-template-repo.
openssf-compliance: unfilled {{…}} tokens under www/.

Both fail the same way on main.

Anomaly, not changed here: src/SecretTypes/*.agdai are committed (since 833715c). Agda rewrites them on every gate run, so a checked-out tree goes dirty, and they are now stale relative to the sources.

🤖 Generated with Claude Code

https://claude.ai/code/session_017yYi5JxzXZs6nz1ZSForfP

…lock - .github/workflows/proofs.yml: Debian 13 container (digest-pinned), agda-bin=2.6.4.3-1+b2, actions/checkout SHA-pinned; runs scripts/check.sh. Pattern: choreographic-types. - scripts/check.sh: refuses any Agda but 2.6.4.3; scans the trusted base for postulates; adds -W error; requires each rejection to fail at or after its `invalid` line. - Justfile: `just test` runs the proof gate instead of failing as an unwired template recipe. - actions.lock: onboard proofs.yml; record the actions/checkout SHA pin with its release tag as `ref` (job setup refuses a tagged action whose record repeats the SHA, per choreographic-types' lock note of 2026-10-16); repair the drift already on main, where pages.yml and sonarqube.yml use haskell-actions/setup@v2.12.1 and SonarSource/sonarqube-scan-action@v8.3.0 but the lock still named v2.12.0 and v8.2.2. scripts/check-lock-sync.sh was red on main (a75798a) for exactly those two rows; it is green here. Refs #9 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017yYi5JxzXZs6nz1ZSForfP

…losed observers - SecretTypes.Lattice.Record: the Lattice record, defined once (Carrier, _⊑_, _⊔_, ⊥ₗ, ⊑-trans, ⊔-upper₁, ⊔-upper₂), with Observer (a down-closed set of labels) and `principal o` (sees ℓ iff ℓ ⊑ o, the only use of ⊑-trans). - SecretTypes.Typing.Generic: Volpano–Smith rules over the operations and a labelling `label : Var → Carrier`; no laws. - SecretTypes.Noninterference.Statement: observer agreement s ≈[ sees ] s' and the TINI statement, over the operations. - SecretTypes.Noninterference.Generic: `tini V : TINI (sees V)` for every Lattice and every down-closed observer V. The branch split needs no decidability: agreement is stable (Nat equality is decidable) and excluded middle holds under double negation. - The two-point lattice is the instance `two-point`; Typing and Noninterference re-derive `tini`, `eval-low` and `confine` there with their original statements, at the principal observer L. Witness and tests/reject are unchanged and still check / still fail with L != H. - Prelude gains ⊥-elim, Dec (same constructors as Lintel's copy), _≟_ on naturals, dec-stable and ¬¬-dec. Lang loses `label` (it moved to Typing) and gains `read`. Refs #9 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017yYi5JxzXZs6nz1ZSForfP

… → TESTED) - scripts/minimal-laws.sh (pattern: choreographic-types K-4): generic TINI typechecks against tests/minimal-laws, a Lattice.Record with only ⊔-upper₁, ⊔-upper₂ and observer down-closure; it checks the census record against the real one (which adds exactly ⊑-trans); removing any census field is refused with "Not in scope" for that field. - SecretTypes.Countermodels: for each law, a structure keeping the others and the unchanged typing rules in which a well-typed program leaks (`refutes : ¬ TINI _`): NoUpper₁, NoUpper₂, NoDownClosure, NoTrans. - The census refutes two points of the hypothesis in #9: neither ⊥ ⊑ x nor decidable ⊑ is used. - PROOF-STATUS: N-6 ASSUMED → TESTED; new N-7 (TINI over the record, PROVEN) and N-8 (each law necessary, PROVEN); the fragment now states the parametric setting; "arbitrary lattices" leaves Open. CI stays DESIGNED until the first green run. - proofs.yml and `just test` run the certificate. Refs #9 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017yYi5JxzXZs6nz1ZSForfP

chatgpt-codex-connector · 2026-10-19T16:55:48Z

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	⚠️ Failed 2026-10-19T18:37:33.771322Z	`9bd1e94`	New commits

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

…row → TESTED Both failed at job setup on main and on this PR with "Unable to resolve action actions/checkout@3d3c42e…: invalid lockfile pin". The cause is in the called repository: hyperpolymath/standards' own actions.lock at da2c748 records that checkout pin with the SHA repeated as `ref`, which job setup now refuses. At 75bd5994 it records `ref: 'v7.0.1'`; this is the pin choreographic-types moved to for the same failure. The callers pass no secrets, which both reusables at 75bd5994 accept. actions.lock: the standards@75bd5994 record lists the actions its two reusables use (cache, checkout, upload-artifact, setup-beam, codeql-action), each with a SHA-keyed record carrying its release tag as `ref`. check-lock-sync.sh stays green. governance, mirror, rust-ci and scorecard still pin da2c748 and are left for a separate change. PROOF-STATUS: CI DESIGNED → TESTED, citing proofs.yml run 39289501788 (green on f149e08). Refs #9 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017yYi5JxzXZs6nz1ZSForfP

hyperpolymath · 2026-10-19T16:57:51Z

CI on f149e08: the Agda proofs job is green (run 39289501788, log ends PASS: minimal-laws certificate (3 laws, each needed)), and so is the Lock Sync Gate. SonarQube now starts; it failed at startup on main.

Red checks, none caused by this PR's proof changes:

hypatia / Hypatia Neurosymbolic Analysis and scan / gitleaks, rust-secrets, shell-secrets
- The error is Unable to resolve action actions/checkout@3d3c42e…: invalid lockfile pin.
- main fails the same way (runs 39162436758 and 39162436700, at a75798a).
- The cause is in hyperpolymath/standards at da2c748: its own actions.lock records that checkout pin with the SHA as ref.
- Fix ported in 17412e2: re-pin both callers to standards@75bd5994, whose lock records ref: 'v7.0.1' (the same pin choreographic-types uses), and close our lock for the actions that commit uses.
- governance, mirror, rust-ci and scorecard still pin da2c748 and have the same defect. They are left alone here so the PR does not grow.
openssf-compliance
- It fails on unfilled template tokens ({{PROJECT_NAME}}, {{AUTHOR}}, …) under www/, e.g. www/public/index.html.
- main fails the same way, and this PR touches nothing under www/.
- No fix exists yet: whether to fill those tokens or delete those files is a content decision for the owner. I did not re-run it, because the failure is deterministic.
Canon lockstep (Dogfood Gate)
- It fails with no rsr-profile.a2ml at <sha>.
- .github/workflows/dogfood-gate.yml:412 fetches raw.githubusercontent.com/hyperpolymath/rsr-template-repo/${HEAD_SHA}/…. The job is inherited from the template and hard-codes the template repository, so in any minted repo it looks up this repo's commit in the wrong repository and always fails.
- Dogfood Gate is red on main too, and this PR does not touch the workflow.
- The fix belongs at the source, in rsr-template-repo's dogfood-gate.yml: run the job only in the template, or read ${{ github.repository }}. Nothing is ported here. I did not re-run it, because the failure is deterministic.

Generated by Claude Code

hyperpolymath · 2026-10-19T17:05:10Z

@coderabbitai review

On 17412e2 the CodeRabbit commit status failed with "Review state could not be read", and no review was posted. This asks for the review once more.

Generated by Claude Code

coderabbitai · 2026-10-19T17:06:47Z

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 48 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Advanced
Run ID: b522b0aa-924b-4f9f-b9e3-39b5f53a48e3

📥 Commits

Reviewing files that changed from the base of the PR and between 9411894 and 9bd1e94.

📒 Files selected for processing: 6

.gitignore
src/SecretTypes/Lang.agdai
src/SecretTypes/Lattice.agdai
src/SecretTypes/Noninterference.agdai
src/SecretTypes/Prelude.agdai
src/SecretTypes/Typing.agdai

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Advanced
Run ID: 8f8b4a4f-91e9-42b4-955f-3ac136de4b49

📥 Commits

Reviewing files that changed from the base of the PR and between 17412e2 and 9411894.

📒 Files selected for processing: 7

PROOF-STATUS.adoc
scripts/check.sh
scripts/minimal-laws.sh
src/SecretTypes/Countermodels.agda
src/SecretTypes/Noninterference.agda
src/SecretTypes/Noninterference/Generic.agda
src/SecretTypes/Typing/Generic.agda

Included review availability: This review used your included allowance. Your plan provides up to 1 included review per hour; 0 remain after this review.

📜 Recent review details

⚠️ CI failures not shown inline: 17

GitHub Actions: OpenSSF Compliance / 0_openssf-compliance.txt: feat(lattice): TINI over a Lattice record and down-closed observers, with a certified laws census

Conclusion: failure

View job details

##[group]Run SECFILE=""
 �[36;1mSECFILE=""�[0m
 �[36;1m[ -f "SECURITY.md" ] && SECFILE="SECURITY.md"�[0m
 �[36;1m[ -f "SECURITY.adoc" ] && SECFILE="SECURITY.adoc"�[0m
 �[36;1m[ -f ".github/SECURITY.md" ] && SECFILE=".github/SECURITY.md"�[0m
 �[36;1m�[0m
 �[36;1mif [ -z "$SECFILE" ]; then�[0m
 �[36;1m  echo "::error::SECURITY.md (or SECURITY.adoc) is required for OpenSSF Best Practices"�[0m
 �[36;1m  exit 1�[0m
 �[36;1mfi�[0m
 �[36;1m�[0m
 �[36;1mLINES=$(wc -l < "$SECFILE")�[0m
 �[36;1mif [ "$LINES" -lt 10 ]; then�[0m
 �[36;1m  echo "::error::$SECFILE has only $LINES lines — must have >10 lines of substantive content"�[0m
...
 ##[group]Run if [ ! -f "LICENSE" ] && [ ! -f "LICENSE.txt" ] && [ ! -f "LICENSE.md" ]; then
 �[36;1mif [ ! -f "LICENSE" ] && [ ! -f "LICENSE.txt" ] && [ ! -f "LICENSE.md" ]; then�[0m
 �[36;1m  echo "::error::LICENSE file is required for OpenSSF Best Practices"�[0m
...
 ##[group]Run if [ ! -f "CONTRIBUTING.md" ] && [ ! -f "CONTRIBUTING.adoc" ] \
 �[36;1mif [ ! -f "CONTRIBUTING.md" ] && [ ! -f "CONTRIBUTING.adoc" ] \�[0m
 �[36;1m   && [ ! -f ".github/CONTRIBUTING.md" ] && [ ! -f ".github/CONTRIBUTING.adoc" ]; then�[0m
 �[36;1m  echo "::error::CONTRIBUTING file is required for OpenSSF Best Practices"�[0m
...
 ##[group]Run if [ ! -f "README.md" ] && [ ! -f "README.adoc" ] && [ ! -f "README.rst" ] && [ ! -f "README.txt" ] && [ ! -f "README" ]; then
 �[36;1mif [ ! -f "README.md" ] && [ ! -f "README.adoc" ] && [ ! -f "README.rst" ] && [ ! -f "README.txt" ] && [ ! -f "README" ]; then�[0m
 �[36;1m  echo "::error::README file is required for OpenSSF Best Practices"�[0m
...
 ##[group]Run if [ ! -d ".machine_readable" ]; then
 �[36;1mif [ ! -d ".machine_readable" ]; then�[0m
 �[36;1m  echo "::error::.machine_readable/ directory is required"�[0m
 �[36;1m  exit 1�[0m
 �[36;1mfi�[0m
 �[36;1m�[0m
 �[36;1mif [ ! -f ".machine_readable/descriptiles/STATE.a2ml" ]; then�[0m
 �[36;1m  echo "::error::.machine_readable/descriptiles/STATE.a2ml is required"�[0m
...
 ...