Rocq and Lean recheck legs for N-1..3, N-7..9 (PWG-2ii) by hyperpolymath · Pull Request #29 · hyperpolymath/secret-types

hyperpolymath · 2026-11-09T13:57:18Z

Summary

This PR adds the two recheck legs that PROOF-POLICY §2 asks for, Rocq and Lean, for every proved theory claim: N-1, N-2, N-3, N-7, N-8 and N-9. They are hand re-proofs, because transport is not available. Agda2Dedukti is an Agda backend pinned to a fork of Agda and cannot run on the pinned 2.6.4.3, and no Dedukti or Lambdapi exporter to Lean 4 has been released. Both legs check with no library and no axioms, and the statements are compared in a §2.2 record. With both legs in place, the claims move from PWG-3 to PWG-2ii.

This PR is stacked on #26 (--cubical-compatible), so its base is that branch. No Agda module or statement changes.

For the owner to review (doctrine 4): the statement comparison in verification/legs/README.adoc was written by Claude Code and is labelled provisional until you review it. No tool checks it. The PWG-2ii grade rests on it.

Changes

verification/legs/rocq/SecretTypes.v
- Coq 8.18.0, prelude only, with no Require.
- 11 theorems. Print Assumptions reports "Closed under the global context" for each.
verification/legs/lean/
- Lean 4.24.0, core only: the lakefile has no require, so no Mathlib.
- 11 theorems. #print axioms reports "does not depend on any axioms" for each.
- exec is defined structurally through run, so no well-founded recursion brings in propext.
scripts/check-legs.sh
- Pins both checker versions; the environment cannot override them.
- Refuses any library, and any sorry, admit, Admitted, Axiom or Parameter.
- Fails unless all 22 axiom lines are clean.
.github/workflows/proofs.yml: new legs job.
- Coq is pinned by its Ubuntu package version.
- Lean is pinned by the sha256 of its release tarball.
- It uses only the already-locked actions/checkout pin, so actions.lock is unchanged.
verification/legs/README.adoc: the §2.2 correspondence record. It covers:
- the route and the reason for it;
- versions and invocations;
- the residual assumptions (none) and the universe discipline;
- a point-by-point statement comparison: exec, Option, the Signature/Lattice split, Observer, Vars;
- a claim-by-claim map from each Agda name to its Lean and Rocq names.
- The state is RECONCILED.
scripts/grade-receipt.sh and verification/receipts/agda-pwg_praxis.deed
- The receipt gains a (legs) block: pins, invocations, axioms, and the sha256 of every leg input.
- The claims now read re-proved/re-proved at PWG-2ii.
- The script refuses a claim that counts a leg without a row in the correspondence record, and the reverse.
PROOF-STATUS.adoc, README.adoc, docs/EXPLAINME.adoc and docs/proof-debt.adoc now record the new grade and legs.
- Not PWG-1: no per-commit receipt captures each checker's observed result yet.
- Not +foundation-diverse: Agda, Rocq and Lean are all dependent type theories.

RSR Quality Checklist

Required

Tests pass. Run locally:
- check.sh: the Agda gate, with its 4 rejections;
- minimal-laws.sh;
- check-legs.sh;
- grade-receipt.sh --check;
- the proven suite;
- the invisible-character scan.
No banned language patterns. The new code is Lean, Coq and bash. lake-manifest.json is git-ignored, not committed.
No banned functions: check-legs.sh refuses sorry, admit, Admitted, Axiom and Parameter.
SPDX headers on every new file except lean-toolchain, which Lean reads whole as the toolchain name.
No secrets.

As Applicable

Documentation updated: PROOF-STATUS, README, EXPLAINME, proof-debt.

Testing

Negative controls, run by hand:

Dropping the correspondence row for N-9 makes grade-receipt.sh --check fail with only in grade-receipt.sh: N-9.
Touching a leg source makes the receipt check fail on that file's sha256.

The new legs job in CI is the first run on a clean runner.

Local output:

PASS: Rocq leg (Coq 8.18.0), 11 theorems closed under the global context
PASS: Lean leg (Lean 4.24.0, core only), 11 theorems depend on no axioms
PASS: both recheck legs
PASS: verification receipt matches the tree (15 modules, all sha256 verified)

Generated by Claude Code

PROOF-POLICY §2 asks for every Agda theory proof to be rechecked in Rocq and in Lean, transport first and hand re-proof as the fallback. Transport is not available: Agda2Dedukti is an Agda backend pinned to a fork of Agda and cannot run on the pinned 2.6.4.3, and there is no released Dedukti/Lambdapi exporter to Lean 4. So both legs are hand re-proofs: - verification/legs/rocq/SecretTypes.v: Coq 8.18.0, prelude only (no Require); 11 theorems, Print Assumptions "Closed under the global context" for each. - verification/legs/lean/: Lean 4.24.0, core only (no require, no Mathlib); 11 theorems, #print axioms "does not depend on any axioms". exec is defined structurally through run, so no well-founded recursion brings in propext. - scripts/check-legs.sh pins both checkers, refuses any library, any sorry/admit/Admitted/Axiom/Parameter, and any axiom line that is not clean. CI runs it as the new legs job (Coq by Ubuntu package version, Lean by release tarball sha256). - verification/legs/README.adoc is the §2.2 correspondence record: route and reason, versions, invocations, universe discipline, the statement comparison (exec, Option, the Signature/Lattice split, Observer, Vars) and the claim-by-claim name map, state RECONCILED. The comparison is provisional until owner review. - The receipt gains a (legs) block (pins, invocations, axioms, sha256 of every leg input) and the claims move to re-proved/re-proved at PWG-2ii; grade-receipt.sh refuses a counted leg without a correspondence row, and the reverse. - PROOF-STATUS, README, EXPLAINME and proof-debt follow. Not PWG-1: no per-commit receipt of each checker's observed result yet. Not +foundation-diverse: all three provers are dependent type theories. No Agda module or statement changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs

lean-toolchain cannot carry one: Lean reads the whole file as the toolchain name. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs

coderabbitai · 2026-11-09T13:57:26Z

Caution

Review failed

The pull request is closed.

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.

Share

…des as PROOF-POLICY §8 PWG PROOF-POLICY §2.1 names `agda --safe --without-K --cubical-compatible` as the canonical invocation; waiver W-1 kept the flag off, on the belief that only a relational big-step semantics could remove the last 13 warnings (`just`-injectivity in Noninterference.Generic). That belief was wrong: - Prelude: `just-inj` defined by `cong` through the computing projection `from-just`, which needs no unification rule. - Noninterference.Generic: the six clauses that matched `refl` against `exec … ≡ just t` now carry agreement along `just-inj` (`just-≈`, `just-≈₂`). No statement, semantics or fixture changed. - scripts/proof-flags.sh: `--cubical-compatible` added. Gate, laws certificate and receipt all run under it. - tests/flag-control/IndexedMatch.agda + scripts/check.sh: a correct proof that only the flag refuses; the gate fails if it is ever accepted. Removing the flag was tested to fail the gate. The relational route would not have sufficed on its own: a probe proving determinism of `c , s ⇓ t` raised 22 UnsupportedIndexedMatch warnings (inverting two derivations of one command needs Cmd injectivity). Grades: "mathesis Grade 3" was the unratified brief's wording. PROOF-POLICY §8 (2026-11-04) supersedes it and makes PWG-3 depend on the §2.1 invocation, so the theorems were `ungraded` while W-1 was open; they are PWG-3 now. The receipt carries the §8.5 fields (pwg, foundation-diverse, per-leg route, token and §2.2 state), derives the grade from leg states (tested: one RECONCILED leg -> 2i, two -> 2ii, BRIDGE-PENDING does not count), pins the PROOF-POLICY commit (§7), and moves from agda-grade3_praxis.deed to agda_praxis.deed because a grade is derived and can change. EXPLAINME listed --cubical-compatible as a checker flag while it was waived; that line is now true. README's Lintel pin corrected (ee01db4 -> d1d843b). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017yYi5JxzXZs6nz1ZSForfP

A list-item continuation beginning "11. The prelude's ..." parsed as an ordered list (asciidoctor: list item index: expected 1, got 11), which check-adoc-renders.sh fails. Rewrapped; the text is unchanged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs

hyperpolymath · 2026-11-09T15:13:39Z

estate-rules is red here, but the cause is not in this PR's diff.

The job fails at just repo-init failed on a Use-this-template child because of an unfilled token: mint-probe.md: {{OWNER}} (job). The same failure appears on main and on #25, #26 and #27. This PR adds the Lean and Rocq legs and their docs, and touches none of the mint machinery.

The fix is #28, the template sync, which ships the legacy-child mint guard. I am not porting it here: it is a 64-file sync, and copying it into every stacked PR would turn each one into a second copy of #28. Once #28 merges, this PR picks up the fix when its base is updated.

The new legs job is not affected; it runs separately from estate-rules. An earlier estate-rules failure on this PR was mine: a line starting "11." broke the AsciiDoc render. I fixed that in 18cbabf.

Generated by Claude Code

chatgpt-codex-connector · 2026-11-09T15:40:01Z

Codex Review Summary: ❌ Failed

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

Review	Status	Commit	Review trigger
📝 Code Review	❌ Failed 2026-11-09T15:39:55.909821Z We couldn’t complete this review. Comment `@codex review` to try again.	`18cbabf`	Draft marked ready

ℹ️ 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.

chatgpt-codex-connector · 2026-11-09T15:40:04Z

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.

github-actions · 2026-11-09T17:49:10Z

🟠 indeterminate · the verdict grid could not be rendered · 18cbabfa6bd0

The renderer pinned in metadatastician/standards@8e48b1caade0 was missing or did not match its recorded sha256.

Orange means the evidence for this lane was unavailable, not that the repository passed.

## Summary The proof gate now runs PROOF-POLICY §2.1's canonical invocation, `agda --safe --without-K --cubical-compatible`, with `--no-libraries --ignore-interfaces --double-check -W error`. Waiver W-1 is retired. The 13 remaining `UnsupportedIndexedMatch` warnings (in `tini`, `go`, `confine` and `confineW`) all came from clauses that matched `refl : just s ≡ just t`, which relies on the injectivity of `just`. W-1 said the way out was a relational big-step semantics, with a consequence for how N-5 states divergence. That change is not needed. The clauses now take the equation as a variable and use `Prelude.just-inj`, defined as `cong` of a total projection (`from-just`). `cong` matches `refl` only against a variable, so no clause asks for constructor injectivity. **No theorem statement changed**, and the fuel semantics is untouched. ## Changes - `src/SecretTypes/Prelude.agda`: `from-just`, `just-inj` (cubical-compatible) and `subst₂`. The comment explains why the old matching lemma was refused. - `src/SecretTypes/Noninterference/Generic.agda`: six clauses use `just-inj` and `subst`/`subst₂`, or `≈-from-≡` (equal stores agree), in place of a `refl` match on `just _ ≡ just _`. - `scripts/proof-flags.sh`: `--cubical-compatible` added; the rationale comment updated. - `scripts/grade-receipt.sh` and the regenerated receipt: `:cubical-compatible "met"`, pointing at the retired waiver's history. - `PROOF-STATUS.adoc` and `docs/proof-debt.adoc`: W-1 kept as a dated, retired record, with a *Closed* entry saying what closed it and why the earlier "threading the result as a variable" probe did not. ## RSR Quality Checklist ### Required - [x] Tests pass: `scripts/check.sh` (core proofs and the 4 expected rejections) and `scripts/minimal-laws.sh`, run locally, see Testing - [x] Code is formatted - [x] Linter is clean: deed lint on the receipt, `check-adoc-renders.sh` (174 files), `check-invisible-characters.sh`, `check-spdx-headers.sh`, `check-no-placeholders.sh` - [x] No banned language patterns - [x] No `unsafe` blocks without `// SAFETY:` comments (none touched) - [x] No banned functions - [x] SPDX license headers present on all new/modified source files - [x] No secrets, credentials, or `.env` files included ### As Applicable - [ ] Repo deed `(status)` / `(maturity)`: unchanged - [x] Documentation updated (PROOF-STATUS, proof-debt) ## Testing | Check | Result | |---|---| | `AGDA_VERSION=2.6.3 bash scripts/check.sh` with the new flags (local Agda 2.6.3) | trusted base, core proofs (`SecretTypes.All`), all 4 rejections at their `invalid` declaration: PASS | | `bash scripts/minimal-laws.sh` | 3 laws, each needed: PASS | | `bash scripts/grade-receipt.sh --check` (after commit) | exit 0 | | Warnings under `--cubical-compatible` before → after | 13 (4 definitions, all `just`-injectivity) → 0, with `-W error` | | Downstream: lintel's full gate against this change, with `--cubical-compatible` added there too | PASS. lintel needs its own small re-representation, coming in a lintel PR once this merges | Locally the Agda is 2.6.3, because the pinned Debian package couldn't be fetched in this session. CI on this PR runs the pinned 2.6.4.3 and is the receipt-grade evidence. `scripts/check-proofs.sh agda`'s standalone `verification/proofs/agda/Properties.agda` fails under 2.6.3 on unmodified `main` too (module/file-name rule), so for that file CI is the only evidence. The grade labels in the records (`grade-3`, mathesis wording) move to PROOF-POLICY §8 `PWG-` labels in a follow-up PR, kept separate so this one merges quickly. --- _Generated by [Claude Code](https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg)_   ## Summary by CodeRabbit * **Improvements** * Formal proof verification now meets the Cubical Agda compatibility checks, replacing the previous waiver. The verification runs with stricter checks enabled. * The proof changes preserve theorem statements and fuel behavior. * **Documentation** * Updated proof status and waiver history to reflect the completed verification and current conformance status.  --------- Co-authored-by: Claude <noreply@anthropic.com>

…#28) ## Summary **estate-rules is red on `main`.** Its step "Use-this-template mint end to end" runs `tests/e2e/use_template_mint_test.sh` as inherited from template `c481073`. That version re-mints this already-minted tree and fails on an unfilled `{{OWNER}}` token. The template fixed this across #275, #291, #293 and #294, and its current test self-skips in a minted child. I reproduced both sides: the `c481073` test fails on `main`, and the current test passes on this branch. ## Changes This is a three-way sync. The base is `c481073`, the commit this repository was minted from, and the target is template `2be7b88`. - **43 files** that this repository still held byte-identical to `c481073` take the template's current version: mint machinery, hooks, workflows, checks and tests. - **9 new machinery files**: `chain-mint`, `replay-mint`, `check-mint-drift` and `format-container-kyaml`, plus their tests. The template's own diagnostic workflow (`oracle-segfault-diag.yml`) and its lock record are left out. - **Diverged files** were three-way merged. These stay as this repository's own: - `governance.yml`, the reusable caller from #15; - `README.adoc`; - `mise.toml`, with `yq` added for `scripts/kyaml-format.sh`; - the verdict-grid lane and the rule-order policy, kept at standards `8e48b1c` because that renderer works and the template's `e064539` does not; - the rule-order checker and its test, from #22; - `CHANGELOG.adoc`, which gets one entry for this sync instead of the template's release notes. - **`secret-scanner.yml`** takes the template's inline three-scanner workflow (rsr-template-repo#295: stable status contexts, no `secrets: inherit`). Its lock record is updated and its contract test wired. - **`non_interactive_mint_test.sh` and `chain_mint_test.sh`** carry hyperpolymath/rsr-template-repo#300's guard. Without it, both tests fail in any legacy minted child. In a repository minted without `(mint-answers)`, the guard asserts that `repo-init` refuses to mint again, by name. ## RSR Quality Checklist ### Required - [x] Tests pass. Locally: - `check-lock-sync`: in sync. - `check-workflow-edges`, `check-required-contexts`, `check-root-shape`: pass. - `run-proven-suite.sh`: `ALL LANES PASSED`. - Every single-line estate-rules lane: the same five fail as on unmodified `main`. Four are environmental on this machine (asciidoctor, this machine's `yq`) and pass in CI. - [x] No banned language patterns - [x] SPDX license headers present on all new/modified source files - [x] No secrets, credentials, or `.env` files included ## Still red, and why - **`governance_policy_test`** fails because the #15 governance caller's `pull_request` trigger carries a branch filter, and the test also expects the inline standards checkout. CI never reached this step before, because the mint test failed first. Whether to keep the caller or take the template's inline governance workflow is your call. - **Canon lockstep**: fixed by #27. --- _Generated by [Claude Code](https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs)_ --------- Co-authored-by: Claude <noreply@anthropic.com>

PROOF-POLICY §2 asks for every Agda theory proof to be rechecked in Rocq and in Lean. Transport is not available (Agda2Dedukti is an Agda backend pinned to a fork and cannot run on 2.6.4.3; no released Dedukti/Lambdapi exporter to Lean 4), so both legs are hand re-proofs. They stand on secret-types' own legs at the sibling pin, as the Agda stands on secret-types' Agda: the record, the language, the typing rules and TINI are imported, never restated. - verification/legs/rocq/Lintel.v: Coq 8.18.0; the only load is secret-types' Rocq leg (and its coercions), no standard library. 36 statements, Print Assumptions "Closed under the global context" for each (transitive, so secret-types' leg is covered too). - verification/legs/lean/: Lean 4.24.0; the only require is secret-types' Lean leg in the pinned checkout, no Mathlib. 36 statements, #print axioms clean for each. - scripts/check-legs.sh pins both checkers, allows exactly that one dependency per leg, refuses escape hatches and any unclean axiom line. CI runs it as the new legs job (Coq by package version, Lean by tarball sha256), after fetch-siblings. - verification/legs/README.adoc: the §2.2 correspondence record (route, versions, invocations, universe discipline, the statement comparison and the claim-by-claim name map), state RECONCILED, provisional until owner review. - Receipt: (legs) block with pins, invocations, axioms and the sha256 of every leg input, the sibling's leg files included; claims move to re-proved/re-proved at PWG-2ii; grade-receipt.sh refuses a counted leg without a correspondence row, and the reverse. - Re-pin secret-types to 45046c2 (hyperpolymath/secret-types#29, the legs, stacked on #26). Its src/ is byte-identical to the old pin 2f342bc; only the module-header pin comments change. - PROOF-STATUS, PROOF-NEEDS (R-1, R-2 done) and README follow. Not PWG-1; not +foundation-diverse. No Agda statement or proof changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs

#27) ## Summary Canon lockstep is red on `main`. standards' `canon.lock` now records canon 2.1.5 (metadatastician/standards#1424): the gate table moved to 0.3.1 and the applicability policy changed, but the criteria did not. This deed still declares 2.1.3. This ports hyperpolymath/rsr-template-repo#298, the template's adoption. I've also ported the same commit into #25 and #26 so Canon lockstep goes green there; the port becomes a no-op once this PR merges. ## Changes - **`secret-types_chora.deed` `(canon …)`**: `:version` goes from 2.1.3 to 2.1.5, and `:gates-sha256` from `2f31f46d…` to `5c510bba…`. The criteria hash is unchanged. - **The `(provenance)` clause keeps 2.1.3.** It records the canon this repository was minted against, which is history. - **`tests/workflows/governance_policy_test.sh`** now expects the 2.1.5 tuple. ## RSR Quality Checklist ### Required - [x] Linter is clean: the DEED lint passes against standards@8e48b1c. - [x] No banned language patterns - [x] No secrets, credentials, or `.env` files included - [ ] Tests pass: `governance_policy_test.sh` already fails on `main`, before it reaches the canon assertion. Its first check rejects `governance.yml`'s `pull_request: branches: [main, master]` filter, which came in with #15's canonical caller. This PR doesn't change that; `deed-field.sh` returns the 2.1.5 tuple. ## Testing `deed-field.sh` returns version 2.1.5, criteria `6a5aa885…` and gates `5c510bba…`, the same values `canon.lock` has on standards `main`. `canon.lock` still marks 2.1.5 as `status = "draft"`. This PR adopts the identity the lock records, which is what the lockstep gate compares. --- _Generated by [Claude Code](https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs)_ Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>

## Summary This adds the two recheck legs that `PROOF-POLICY` §2 asks for, Rocq and Lean, for every proved claim (L-1 to L-4, L-6 and L-7). With them, those claims go from `PWG-3` to `PWG-2ii`. Both legs are hand re-proofs, because transport is not available: - Agda2Dedukti is an Agda backend pinned to a fork of Agda, and it cannot run on 2.6.4.3. - No Dedukti or Lambdapi exporter to Lean 4 has been released. The legs build on secret-types' own legs at the sibling pin, the same way the Agda builds on secret-types' Agda. The record, the language, the typing rules and TINI are imported, not restated. The PR is stacked on #22, so its base is that branch. It also depends on hyperpolymath/secret-types#29, the secret-types legs: the pin moves to that PR's commit `45046c2`. `src/` at that commit is byte-identical to the old pin `2f342bc`. No Agda statement or proof changes. **For the owner to review (doctrine 4):** the statement comparison in `verification/legs/README.adoc` was written by Claude Code and is labelled provisional until you review it. The `PWG-2ii` grade rests on it. ## Changes - **`verification/legs/rocq/Lintel.v`**: Coq 8.18.0. - The only load is secret-types' Rocq leg and its coercions; no standard library. - 36 statements, each with `Print Assumptions` reporting "Closed under the global context". The check is transitive, so it covers secret-types' leg too. - **`verification/legs/lean/`**: Lean 4.24.0. - The only `require` is secret-types' Lean leg in the pinned checkout; no Mathlib. - 36 statements, each with clean `#print axioms` output. - **`scripts/check-legs.sh`**: - pins both checkers; - allows exactly that one dependency per leg; - refuses escape hatches, and any axiom line that is not clean. - **New `legs` job in `.github/workflows/proofs.yml`**: - Coq pinned by package version, Lean pinned by tarball sha256; - runs after `fetch-siblings.sh`; - `actions.lock` is unchanged. - **`verification/legs/README.adoc`**: the §2.2 correspondence record, in state `RECONCILED`. It covers: - the route, versions and invocations; - the universe discipline; - a point-by-point statement comparison (`Label`, `⊒`/`⊑`, `∧`/`∨`, `Dec`, `reader-sets`, `Field`, `⊎`/`∪`, `collusion-gap`, `writes-flow`, `link-writable`); - a claim-by-claim name map. - **Receipt** (`scripts/grade-receipt.sh` and `verification/receipts/agda-pwg_praxis.deed`): - a `(legs)` block with pins, invocations, axioms, and the sha256 of every leg input, sibling leg files included; - claims now read `re-proved`/`re-proved` at `PWG-2ii`; - the script refuses a counted leg that has no correspondence row, and the reverse. - **Docs**: PROOF-STATUS, PROOF-NEEDS (R-1 and R-2 now done) and README updated. The grade is not `PWG-1` and not `+foundation-diverse`. ## RSR Quality Checklist ### Required - [x] Tests pass. Run locally: - `fetch-siblings.sh` - `check.sh` (Agda: 5 positive controls, 4 rejections, negative control) - `check-legs.sh` - `grade-receipt.sh --check` - the coverage self-test - the invisible-character scan - `check-lock-sync.sh` - [x] No banned language patterns. The new code is Lean, Coq and bash. `lake-manifest.json` is git-ignored, not committed. - [x] No banned functions: `check-legs.sh` refuses `sorry`, `admit`, `Admitted`, `Axiom` and `Parameter`. - [x] SPDX headers on every new file except `lean-toolchain`, which Lean reads whole as the toolchain name. - [x] No secrets. ### As Applicable - [x] Documentation updated (PROOF-STATUS, PROOF-NEEDS, README). ## Testing Negative controls run by hand: `check-legs.sh` fails on each of these. - A `From Coq Require Import Bool.` line in the Rocq leg. - A `[[require]] name = "mathlib"` entry in the lakefile. `fetch-siblings.sh` re-verifies that the sibling checkout is clean after both legs build into it. Only ignored build outputs are created. ``` PASS: Rocq leg (Coq 8.18.0), 36 statements closed under the global context PASS: Lean leg (Lean 4.24.0, core only), 36 statements depend on no axioms PASS: both recheck legs PASS: verification receipt matches the tree (4 Lintel modules, 7 sibling modules, all sha256 verified) ``` --- _Generated by [Claude Code](https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs)_   ## Summary by CodeRabbit * **New Features** * Added Rocq and Lean verification for information-flow, coalition, and write-confinement properties. * Automated checks now validate the proof builds and confirm the checked results use no axioms. * **Documentation** * Updated proof status for claims L-1–L-4, L-6, and L-7 to PWG-2ii, reflecting re-proofs in both systems. * Documented verification coverage and remaining review items; the claims are not yet rated PWG-1.  --------- Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>

#25) ## Summary This ports commit 8ffc72a from hyperpolymath/rsr-template-repo#290. That commit landed in the template after this repository's port, #20, had already merged without it. It clears the SonarCloud failure "C Security Rating on New Code" that #20 merged with. `reusable_source` in `scripts/check-workflow-edges.sh` fetches a called workflow with `curl -fsSL`. Because of `-L`, curl follows redirects to any protocol, so a redirect could downgrade the fetch to plain http. That is the SonarCloud annotation on line 150 ("Not enforcing HTTPS here might allow for redirections to insecure websites"). ## Changes - `scripts/check-workflow-edges.sh`: line 150 now passes `--proto =https --proto-redir =https` to curl, so both the request and any redirect must stay on https. ## RSR Quality Checklist ### Required - [x] Tests pass: `bash tests/workflows/workflow_edges_test.sh` passes 46 checks, and `bash scripts/check-workflow-edges.sh` passes on this tree. - [x] Code is formatted (one-line change) - [x] Linter is clean (no new warnings or errors) - [x] No banned language patterns - [x] No `unsafe` blocks without `// SAFETY:` comments - [x] No banned functions - [x] SPDX license headers present on all new/modified source files - [x] No secrets, credentials, or `.env` files included ### As Applicable Nothing here applies: this is a one-flag change to a check script. ## Testing - I ran the edge suite and the live checker, as listed above. - I fetched a pinned reusable from raw.githubusercontent.com with the restricted flags and the fetch succeeded. - The same change on the template turned SonarCloud's quality gate from failed to passed on #290. ## Known reds on `main`, not this PR's `main` (eee4e40) is red on three checks this PR does not touch: - **Canon lockstep.** metadatastician/standards' `canon.lock` moved to draft 2.1.5 on 2026-11-07, with a new gates hash. The deed declares 2.1.3. The template's main is red on the same check. The spine adopts first, per `[canon].order`. - **canary.** rhodibot reports one would-mutate finding, also on template main. - **estate-rules.** `just repo-init` on a Use-this-template child reports one unfilled token. --- _Generated by [Claude Code](https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs)_ --------- Co-authored-by: Claude <noreply@anthropic.com>

…F-POLICY §8 PWG (#32) ## Summary PROOF-POLICY §2.1 makes `agda --safe --without-K --cubical-compatible` the canonical invocation. Waiver W-1 kept the flag off. It assumed that only a relational big-step semantics could remove the last 13 warnings, all `just`-injectivity in `Noninterference.Generic`. That assumption was wrong. This PR puts the flag in force without changing any statement, the semantics, or any fixture. PROOF-POLICY §8 (owner ruling 2026-11-04) replaces "mathesis Grade 3" with Proof Witness Grades, and makes `PWG-3` depend on the §2.1 invocation. So while W-1 was open the theorems were `ungraded`, and the docs overclaimed. With this PR they are `PWG-3`, and the receipt records them in the §8.5 shape. First of the follow-ups agreed with the owner. In order: 1. this PR; 2. Lintel's own fix and a re-pin to this PR's merge commit; 3. a mathesis claims-registry ADR; 4. `⇓` as a second semantics with an adequacy theorem; 5. the Rocq and Lean legs, re-proved, with this repo as the pilot. ## Changes - **`Prelude.just-inj`** is defined by `cong` through the computing projection `from-just`. It matches nothing, so it needs no unification rule. - **`Noninterference.Generic`.** Six clauses matched `refl` against `exec … ≡ just t`. They now carry agreement through `just-≈` and `just-≈₂`. The diff is about 25 lines. - **`scripts/proof-flags.sh`** adds `--cubical-compatible`. The gate, the laws certificate and the receipt all run under it. - **Flag control.** `tests/flag-control/IndexedMatch.agda` is a correct proof that only the flag refuses. `scripts/check.sh` fails if it is ever accepted. - **Receipt** (`verification/receipts/agda_praxis.deed`, renamed from `agda-grade3_praxis.deed` because a grade is derived and can change): - §8.5 fields: `pwg`, `foundation-diverse`, and each leg's route, token and §2.2 state. - The grade is derived from the leg *states*. Only `RECONCILED` counts. - `PROOF-POLICY` is pinned by full commit (`hyperpolymath/standards` `9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5`, §7). - **Docs.** - PROOF-STATUS uses only the §5 vocabulary (`DESIGNED` and `REFUTED` are gone; N-9 is a proved refutation). - README, EXPLAINME, proof-debt and CHANGELOG are updated. W-1 is kept, closed, for provenance. - **Corrected along the way.** - EXPLAINME listed `--cubical-compatible` as a checker flag while it was waived; that line is now true. - README's Lintel pin was stale: `ee01db4` → `d1d843b`. ### Why not the relational semantics for this A probe proving determinism of `c , s ⇓ t` raised **22** `UnsupportedIndexedMatch` warnings. Inverting two derivations of the same command needs injectivity of `Cmd`'s constructors. So `⇓` alone does not satisfy the flag. It is still planned, as a second semantics with an adequacy theorem (`exec` finishes ⇔ `⇓`), in a later PR. ## RSR Quality Checklist ### Required - [x] Tests pass. Local, Agda 2.6.4.3: - `scripts/check.sh` is green: core proofs, 4 expected rejections, flag control. - `scripts/minimal-laws.sh` passes: `3 laws, each needed`. - `scripts/grade-receipt.sh --check` passes. - [x] Linter is clean: `-W error`, the invisible-character scan and the escape-hatch scan. - [x] No banned language patterns. - [x] No banned functions, no postulates. - [x] SPDX headers on the new fixture. - [x] No secrets. ### As Applicable - [x] Documentation updated: PROOF-STATUS, README, EXPLAINME, proof-debt, CHANGELOG. `scripts/check-adoc-renders.sh` passes on all 174 files (asciidoctor 2.0.26). - [ ] Deed `(status)`: not touched. ## Testing - **Negative controls, both directions:** - Re-planting one original `refl` match makes the gate fail (exit 42, `UnsupportedIndexedMatch`). - Deleting `--cubical-compatible` from `proof-flags.sh` makes `check.sh` fail at the flag control (`flag control accepted`). - The fixture type-checks without the flag (exit 0), so it fails for the right reason. - **Rejections** fail for their original reasons, with no cubical warnings in their logs. - **Grade derivation**, five cases: - no reconciled leg → `3`; - one `RECONCILED` leg → `2i`; - two → `2ii`; - an `open` token → `ungraded`; - `BRIDGE-PENDING` does not count. - **Downstream:** Lintel's gate is green with the flag, against this tree, after Lintel's own three-clause fix plus a computed `Writes`. That goes in a separate Lintel PR once this one merges. CI evidence for the new state comes from this PR's `Agda proofs` run. The old run links in PROOF-STATUS were for the waived flag set, so I removed them rather than carry them forward. --- _Generated by [Claude Code](https://claude.ai/code/session_017yYi5JxzXZs6nz1ZSForfP)_ Co-authored-by: Claude <noreply@anthropic.com>

The owner chose #32 as the base for the cubical-compatible change, so this branch now builds on it instead of #26. - Proof code, proof-flags.sh: #32's version (Prelude.just-inj, tests/flag-control/IndexedMatch.agda). The legs do not depend on the Agda helper names. - Receipt: verification/receipts/agda_praxis.deed (#32's name), written by grade-receipt.sh --write. #32 derives each PWG from the legs' §2.2 states, so N-1..3 and N-7..9 now carry route re-proved and state RECONCILED for both legs, and their grade derives as 2ii. A RECONCILED leg's token is proven. This branch's (legs) block, leg input hashes and the correspondence-record check are carried over. - proofs.yml: #32's receipt step plus this branch's legs job. - PROOF-STATUS, README, EXPLAINME, proof-debt: #32's wording, with this branch's leg facts and the new receipt path. Checked locally with Agda 2.6.4.3, Coq 8.18.0 and Lean 4.24.0: check.sh (core proofs, 4 rejections, flag control), minimal-laws.sh, check-legs.sh (both legs), grade-receipt.sh --check (15 modules), check-escape-hatches.sh and the invisible-character scan. Negative control: removing the N-9 row from verification/legs/README.adoc makes grade-receipt.sh --check fail with "only in grade-receipt.sh: N-9". check-adoc-renders.sh was not run here (no asciidoctor in this session). Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmAsYpFA9gxfQLF3F6 Signed-off-by: Claude <noreply@anthropic.com>

My earlier merge (ba2484f) took #32's head before #32 was updated (3bf7f8e), because the local ref was stale. So this branch lacked main's later changes (the template sync #28, canon 2.1.5 #27, https-only edges #25) and kept some #26-only text. This merge corrects that. Each conflicted file is a 3-way merge on 3bf7f8e (the #32 commit the earlier merge used), so only this PR's legs changes are carried onto main. Files the legs work does not own take main's version: tests/workflows/governance_policy_test.sh, and docs/proof-debt.adoc except its legs bullet (this restores #32's dated W-1 record). The receipt is regenerated. The diff against main is now the legs work: the Rocq and Lean sources, check-legs.sh, the legs CI job, the receipt's (legs) block and RECONCILED leg states (PWG-2ii derived), and the matching doc lines. Checked with Agda 2.6.4.3, Coq 8.18.0 and Lean 4.24.0: check.sh, minimal-laws.sh, check-legs.sh, grade-receipt.sh --check (15 modules), check-escape-hatches.sh, the invisible-character scan and tests/workflows/governance_policy_test.sh. Co-Authored-By: Claude <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0136P7ZmAsYpFA9gxfQLF3F6 Signed-off-by: Claude <noreply@anthropic.com>

sonarqubecloud · 2026-11-10T18:56:58Z

Quality Gate passed

Issues
5 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud

hyperpolymath · 2026-11-10T19:04:56Z

Superseded by #34, which is this same branch with main as its base. GitHub refuses to change the base of this PR because it is stacked on #26, and #26 is superseded by #30 and #32, both on main.

Generated by Claude Code

## Summary This PR replaces #29, on the same branch. #29 was stacked on #26, and GitHub refuses to move a stacked PR's base. #26 is superseded by #30 and #32, which are both on `main`, so this PR targets `main` directly. It adds the two recheck legs that `PROOF-POLICY` §2 asks for, Rocq and Lean, for every proved theory claim: N-1, N-2, N-3, N-7, N-8 and N-9. They are hand re-proofs, because transport is not available: Agda2Dedukti is an Agda backend pinned to a fork of Agda and cannot run on the pinned 2.6.4.3, and no Dedukti or Lambdapi exporter to Lean 4 has been released. Both legs check with no library and no axioms, and the statements are compared in a §2.2 record. `main` (#32) derives each grade from the legs' §2.2 states, and only `RECONCILED` counts. With both legs `RECONCILED`, the 6 claims derive `PWG-2ii`. **For the owner to review (doctrine 4):** the statement comparison in `verification/legs/README.adoc` was written by Claude Code and is labelled provisional until you review it. No tool checks it. The `PWG-2ii` grade rests on it. ## Changes - `verification/legs/rocq/SecretTypes.v`: Coq 8.18.0, prelude only, with no `Require`. 11 theorems. `Print Assumptions` reports "Closed under the global context" for each. - `verification/legs/lean/`: Lean 4.24.0, core only (the lakefile has no `require`, so no Mathlib). 11 theorems. `#print axioms` reports "does not depend on any axioms" for each. `exec` is defined structurally through `run`, so no well-founded recursion brings in `propext`. - `scripts/check-legs.sh`: pins both checker versions, refuses any library and any `sorry`, `admit`, `Admitted`, `Axiom` or `Parameter`, and fails unless all 22 axiom lines are clean. - `.github/workflows/proofs.yml`: new `legs` job. Coq is pinned by its Ubuntu package version, Lean by the sha256 of its release tarball. It uses only the already-locked `actions/checkout` pin. - `verification/legs/README.adoc`: the §2.2 correspondence record (route and reason, versions and invocations, residual assumptions (none), universe discipline, a point-by-point statement comparison, and a claim-by-claim map from each Agda name to its Lean and Rocq names). State: `RECONCILED`. - `scripts/grade-receipt.sh` and `verification/receipts/agda_praxis.deed`: - the 6 claims carry route `re-proved` and state `RECONCILED` for both legs, so their grade derives as `2ii`; a `RECONCILED` leg's token is `proven`; - the receipt gains a `(legs)` block: pins, invocations, axioms, and the sha256 of every leg input; - the script refuses a `RECONCILED` leg without a row in the correspondence record, and the reverse. - `PROOF-STATUS.adoc`, `README.adoc`, `docs/EXPLAINME.adoc`, `docs/proof-debt.adoc`: the new grade and legs. Not `PWG-1`: no per-commit receipt captures each checker's observed result yet. Not foundation-diverse: Agda, Rocq and Lean are all dependent type theories. ## RSR Quality Checklist ### Required - [x] Tests pass. Run locally with Agda 2.6.4.3, Coq 8.18.0 and Lean 4.24.0: `check.sh` (core proofs, 4 expected rejections, flag control), `minimal-laws.sh`, `check-legs.sh`, `grade-receipt.sh --check` (15 modules), `check-escape-hatches.sh`, the invisible-character scan, `tests/workflows/governance_policy_test.sh`, and `tests/e2e/use_template_mint_test.sh` (self-skips: this is a minted tree). - [x] No banned language patterns. The new code is Lean, Coq and bash. `lake-manifest.json` is git-ignored. - [x] No banned functions: `check-legs.sh` refuses `sorry`, `admit`, `Admitted`, `Axiom` and `Parameter`. - [x] SPDX headers on every new file except `lean-toolchain`, which Lean reads whole as the toolchain name. - [x] No secrets. ### As Applicable - [x] Documentation updated: PROOF-STATUS, README, EXPLAINME, proof-debt. ## Testing Negative controls: - Removing the N-9 row from `verification/legs/README.adoc` makes `grade-receipt.sh --check` fail with `only in grade-receipt.sh: N-9`. - Touching a leg source makes the receipt check fail on that file's sha256. Not run locally: `scripts/check-adoc-renders.sh` (no asciidoctor in the authoring session). CI runs it. --- _Generated by [Claude Code](https://claude.ai/code/session_0136P7ZmAsYpFA9gxfQLF3F6)_ --------- Signed-off-by: Claude <noreply@anthropic.com> Co-authored-by: Claude <noreply@anthropic.com>

claude added 2 commits November 9, 2026 13:56

Legs: SPDX header on the two new .gitignore files

45046c2

lean-toolchain cannot carry one: Lean reads the whole file as the toolchain name. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BYbQRtNu216R13jtZLmoqs

hyperpolymath mentioned this pull request Nov 9, 2026

Rocq and Lean recheck legs for L-1..4, L-6, L-7 (PWG-2ii) metadatastician/lintel#23

Merged

6 tasks done

claude added 2 commits November 9, 2026 14:28

hyperpolymath marked this pull request as ready for review November 9, 2026 15:39

hyperpolymath assigned Copilot Nov 9, 2026

hyperpolymath and others added 2 commits November 9, 2026 21:09

hyperpolymath added this pull request to stack #33 November 9, 2026 22:51

hyperpolymath and others added 4 commits November 10, 2026 02:30

hyperpolymath mentioned this pull request Nov 10, 2026

Rocq and Lean recheck legs for N-1..3, N-7..9 (PWG-2ii) #34

Merged

6 tasks done

hyperpolymath closed this Nov 10, 2026

Navigation Menu

Repository navigation

Rocq and Lean recheck legs for N-1..3, N-7..9 (PWG-2ii) - #29

Rocq and Lean recheck legs for N-1..3, N-7..9 (PWG-2ii)#29
hyperpolymath wants to merge 11 commits into
claude/cubical-compatiblefrom
claude/recheck-legs

hyperpolymath commented Nov 9, 2026

Uh oh!

coderabbitai Bot commented Nov 9, 2026 •

edited

Loading

Review failed

Uh oh!

hyperpolymath commented Nov 9, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 9, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 9, 2026

Uh oh!

github-actions Bot commented Nov 9, 2026 •

edited

Loading

Uh oh!

sonarqubecloud Bot commented Nov 10, 2026

Uh oh!

hyperpolymath commented Nov 10, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

hyperpolymath commented Nov 9, 2026

Summary

Changes

RSR Quality Checklist

Required

As Applicable

Testing

Uh oh!

coderabbitai Bot commented Nov 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Review failed

Uh oh!

hyperpolymath commented Nov 9, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 9, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 9, 2026

Uh oh!

github-actions Bot commented Nov 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sonarqubecloud Bot commented Nov 10, 2026

Quality Gate passed

Uh oh!

hyperpolymath commented Nov 10, 2026

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

coderabbitai Bot commented Nov 9, 2026 •

edited

Loading

github-actions Bot commented Nov 9, 2026 •

edited

Loading