[hyperpolymath]

Summary

standards/3-practice/PROOF-POLICY.adoc §2.1 names agda --safe --without-K --cubical-compatible as the canonical invocation. §8.2 (owner ruling 2026-11-04) grants PWG-3 only to proofs checked under that invocation. The gate did not run --cubical-compatible (waiver W-1), so under §8 the proved rows were ungraded, although PROOF-STATUS said "mathesis Grade 3". This PR makes the gate meet §2.1 without changing any theorem statement, and records the result as PWG-3.

The last blocker was 13 -WUnsupportedIndexedMatch warnings in tini, go, confine and confineW. Each came from matching an equation exec fuel c s ≡ just t against refl, which needs just to be injective. W-1 said only a relational big-step semantics would remove them, and that this would restate N-5. It turns out not to be necessary.

SecretTypes.Prelude now defines from-just and just-injective e = cong (from-just a) e. This is a retraction: both sides reduce to the two values, so no injectivity rule is used. It is the same move suc-dec already makes with pred. The six affected clauses go through one helper, ≈-just. The semantics, N-5 and every statement are unchanged; the receipt's module hashes record the two changed modules.

Changes

• src/SecretTypes/Prelude.agda adds from-just and just-injective. They replace the comment that said such a lemma could not exist.
• src/SecretTypes/Noninterference/Generic.agda adds ≈-refl and ≈-just. Six clauses no longer match just … ≡ just ….
• scripts/proof-flags.sh adds --cubical-compatible to the single flag set that check.sh, minimal-laws.sh and the receipt all read.
• Receipt. verification/receipts/agda-grade3_praxis.deed is renamed to agda-pwg_praxis.deed, and scripts/grade-receipt.sh emits cubical-compatible "met". Each claim carries a §8.5 :pwg: 3 for the six theorems, and n/a for N-4 to N-6, which are checked demonstrations, not theorems (§8.1). The references in proofs.yml and proofs.just follow the rename.
• Records. PROOF-STATUS.adoc, README.adoc, docs/EXPLAINME.adoc and docs/proof-debt.adoc now say PWG-3 and never a bare "Grade". W-1 is recorded as closed, with its history and the corrected arm.
  • The Rocq and Lean legs stay unavailable, and the text says PWG-3 does not discharge them (§8.4).
  • EXPLAINME's ledger already listed --cubical-compatible among the checker flags. That was not true until this PR.

RSR Quality Checklist

Required

• Tests pass. Locally on Agda 2.6.4.3:
  • bash scripts/check.sh: core proofs pass, and all 4 expected rejections fail at their intended declarations.
  • bash scripts/minimal-laws.sh: 3 laws, each needed.
  • bash scripts/grade-receipt.sh --check: 15 modules, all sha256 verified.
• Code is formatted
• Linter is clean: the DEED lint of all three deeds, the new receipt included, passes against standards@8e48b1c.
• No banned language patterns
• No unsafe blocks without // SAFETY: comments
• No banned functions: scripts/check-escape-hatches.sh is clean and the trust-base counts are all 0.
• SPDX license headers present on all new/modified source files
• No secrets, credentials, or .env files included

As Applicable

• Documentation updated: PROOF-STATUS, README, EXPLAINME and proof-debt.
• Repo deed (status) / (maturity): not changed. The project state is the same; only its grade wording is corrected.

Testing

As above. I also ran metadatastician/lintel's full gate against this branch with --cubical-compatible added on lintel's side. It needs one small lintel change of its own, which will be a separate lintel PR pinned to this branch's commit.

Not in this PR

• The Rocq and Lean recheck legs (§2). These are the only way past PWG-3.
• The reds already on main: Canon lockstep (standards moved to a draft canon 2.1.5), canary, and estate-rules (the inherited mint test).

---

Generated by Claude Code

Summary by CodeRabbit

• Verification
  • The canonical proof check now includes Cubical compatibility, and the related waiver is closed.
  • The proof receipt records the updated verification status: selected claims are rated PWG-3, while independent Rocq and Lean checks remain outstanding.
• Documentation
  • Proof status, proof debt, and the proof ledger now use Proof Witness Grade terminology and point to the updated receipt.
  • Documentation clarifies which claims are proven, which remain ungraded demonstrations, and that no waivers are open.

[coderabbitai]

No actionable comments were generated in the recent review.

Walkthrough

The pull request updates the Agda proofs and canonical flags for Cubical compatibility, changes the generated verification receipt to PWG terminology, and revises the proof status, debt, policy, and governance records.

Changes: PWG proof gate and records

Layer / File(s)	Summary
Cubical-compatible proof changes src/SecretTypes/Prelude.agda, src/SecretTypes/Noninterference/Generic.agda	The Prelude adds from-just and just-injective. Confinement and noninterference cases use the helper to derive agreement for returned stores.
Canonical gate and PWG receipt scripts/proof-flags.sh, scripts/grade-receipt.sh, verification/receipts/agda-pwg_praxis.deed, .github/workflows/proofs.yml, secret-types_chora.deed, tests/workflows/governance_policy_test.sh, build/just/proofs.just	The canonical flags include --cubical-compatible. The receipt generator and receipt record PWG values and mark compatibility as met. The workflow, canon metadata, governance test, and recipe comment reference the updated receipt or canon version.
Proof status and policy documentation PROOF-STATUS.adoc, docs/proof-debt.adoc, docs/EXPLAINME.adoc, README.adoc	The documents assign PWG-3 to the listed theorems, describe the unavailable Rocq and Lean legs, and record W-1 as closed. They update receipt links and related proof-status references.

Estimated code review effort: 3 (Moderate) | ~25 minutes

Change: Bug fix

Possibly related PRs

• hyperpolymath/secret-types#14: Established the proof receipt and recorded --cubical-compatible as waived; this PR updates the flag status and receipt.
• hyperpolymath/secret-types#30: Addresses the same Cubical compatibility gap and changes the gate and noninterference proofs.
• hyperpolymath/secret-types#13: Generalized Noninterference.Generic; this PR revises proof cases in that implementation.

Merge Risk: Minimal · up to efb9a

No actionable issue introduced by this change is established; it is mergeable subject to normal checks.

Pre-merge checks: 5

Check name	Status	Explanation
Title check		The title clearly identifies the main change: enabling the canonical Agda invocation and recording the proofs as PWG-3.
Description check		The description follows the template with a summary, key changes, checklist, and testing details. It also explains the remaining Rocq and Lean obligations and out-of-scope items.
Docstring Coverage		Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentat…
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: Docstring Coverage

Explanation

Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentation-only edits and deletions within surviving functions are included; unchanged diff context and fully deleted functions are excluded. Analyzed 1 functions across 3 files. (10 skipped: 10 unsupported.)

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

• X
• Mastodon
• Reddit
• LinkedIn

Recent review info

Run configuration

• Source mode: Auto
• Repository: hyperpolymath/secret-types
• Branch: claude/cubical-compatible
• File: .coderabbit.yaml
• Commit: efb9aa9
• Layers: Repository YAML
• Review profile: CHILL
• Plan: Advanced
• Run ID: 3e8df7b1-e8c4-4dbd-a6c9-67a0b5e35d43

Commits

Reviewing files that changed from the base of the PR and between eee4e40 and efb9aa9.

Files selected for processing: 13

• .github/workflows/proofs.yml
• PROOF-STATUS.adoc
• README.adoc
• build/just/proofs.just
• docs/EXPLAINME.adoc
• docs/proof-debt.adoc
• scripts/grade-receipt.sh
• scripts/proof-flags.sh
• secret-types_chora.deed
• src/SecretTypes/Noninterference/Generic.agda
• src/SecretTypes/Prelude.agda
• tests/workflows/governance_policy_test.sh
• verification/receipts/agda-pwg_praxis.deed

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

[github-actions]

🟠 indeterminate · commit efb9aa9ab390 · run 42629878232 · scope: this change (13 file(s))

Advisory: 11 row(s), worst 🔴 high (0 critical, 9 high) — reported, never grading the change.

Reporter	Gate	Status	Critical	High	Medium	Minor	Since previous revision
Hypatia scan	gating	🟠 indeterminate	0	0	0	0	— no comparable baseline
panic-attack assail	advisory	🟢 clean	0	0	0	0	— no comparable baseline
pons asinorum	advisory	🟢 clean	0	0	0	0	— no comparable baseline
finishingbot (release readiness)	advisory	🔴 high	0	9	23	2	— no comparable baseline
glambot (presentation quality)	advisory	🔵 minor	0	0	0	9	— no comparable baseline
rhodibot (RSR compliance)	advisory	🟢 clean	0	0	0	0	— no comparable baseline
accessibilitybot	advisory	⚪ not applicable	0	0	0	0	— no comparable baseline
cipherbot	advisory	⚪ not applicable	0	0	0	0	— no comparable baseline
echidnabot	advisory	⚪ not applicable	0	0	0	0	— no comparable baseline
panicbot	advisory	⚪ not applicable	0	0	0	0	— no comparable baseline
seambot	advisory	⚪ not applicable	0	0	0	0	— no comparable baseline
sustainabot	advisory	⚪ not applicable	0	0	0	0	— no comparable baseline

Hypatia scan: error — the scanner produced no findings array

• 🟠 indeterminate: the scanner produced no findings array

panic-attack assail: 14 finding(s)

• 14 further finding(s) in files this change does not touch: reported, not graded (0 critical, 0 high).

pons asinorum: 9 finding(s)

• 9 further finding(s) in files this change does not touch: reported, not graded (0 critical, 0 high).

finishingbot (release readiness): 173 finding(s)

• high V1-DOC-ROADMAP.adoc — Required file ROADMAP.adoc not found (Project roadmap).
• high TOOL-001 — .tool-versions file not found for asdf/mise version management.
• high SCM-001-NEUROSYM.scm — Required SCM file NEUROSYM.scm not found (Neurosymbolic AI documentation).
• high SCM-001-AGENTIC.scm — Required SCM file AGENTIC.scm not found (Agentic AI integration documentation).
• high SCM-001-PLAYBOOK.scm — Required SCM file PLAYBOOK.scm not found (Operational playbooks and procedures).
• high SCM-001-ECOSYSTEM.scm — Required SCM file ECOSYSTEM.scm not found (Project's place in the ecosystem).
• high SCM-001-META.scm — Required SCM file META.scm not found (Meta-level information and architectural decisions).
• high SCM-001-STATE.scm — Required SCM file STATE.scm not found (Project state and progress tracking).
• high PH-100 — Found 124 placeholders, exceeds maximum allowed (0)
• medium V1-COM-CONTRIBUTING.md — CONTRIBUTING.md file not found (Contribution guidelines).
• medium V1-COM-CODE_OF_CONDUCT.md — CODE_OF_CONDUCT.md file not found (Code of conduct).
• medium V1-SEC-001 — SECURITY.md not found for responsible disclosure.
• medium TEST-001 — Could not determine if this is a Rust or Deno project.
• medium REL-004 — No SECURITY.md file found
• medium PH-004 — secret-types_chora.deed:943 — Found 'HACK' in: :marker-scan ("TODO" "FIXME" "XXX" "HACK" "STUB" "PARTIAL")
• medium PH-003 — secret-types_chora.deed:943 — Found 'XXX' in: :marker-scan ("TODO" "FIXME" "XXX" "HACK" "STUB" "PARTIAL")
• medium PH-002 — secret-types_chora.deed:943 — Found 'FIXME' in: :marker-scan ("TODO" "FIXME" "XXX" "HACK" "STUB" "PARTIAL")
• medium PH-001 — secret-types_chora.deed:943 — Found 'TODO' in: :marker-scan ("TODO" "FIXME" "XXX" "HACK" "STUB" "PARTIAL")
• medium PH-004 — secret-types_chora.deed:840 — Found 'HACK' in: :marker_scan_required ("TODO" "FIXME" "XXX" "HACK" "STUB" "PARTIAL")
• medium PH-003 — secret-types_chora.deed:840 — Found 'XXX' in: :marker_scan_required ("TODO" "FIXME" "XXX" "HACK" "STUB" "PARTIAL")
• 14 more graded finding(s); see the structured report in the artifact.
• 139 further finding(s) in files this change does not touch: reported, not graded (0 critical, 3 high).

glambot (presentation quality): 93 finding(s)

• info GS-001 — Install git-seo for comprehensive SEO analysis: https://github.com/hyperpolymath/git-seo
• info MACH-007 — ECOSYSTEM.scm not found in .machine_readable/ directory.
• info MACH-007 — META.scm not found in .machine_readable/ directory.
• info MACH-007 — STATE.scm not found in .machine_readable/ directory.
• info MACH-005 — No robots.txt found. Consider adding one for crawler control.
• info VIS-005 — README.adoc:8 — Line 209 characters exceeds max length of 80.
• info VIS-005 — PROOF-STATUS.adoc:14 — Line 84 characters exceeds max length of 80.
• info VIS-005 — docs/proof-debt.adoc:7 — Line 83 characters exceeds max length of 80.
• info VIS-005 — docs/EXPLAINME.adoc:4 — Line 124 characters exceeds max length of 80.
• 84 further finding(s) in files this change does not touch: reported, not graded (0 critical, 2 high).

rhodibot (RSR compliance): 13 finding(s)

• 13 further finding(s) in files this change does not touch: reported, not graded (0 critical, 12 high).

accessibilitybot: not_applicable — template default: enrol once the repository serves HTML

• ⚪ not applicable: template default: enrol once the repository serves HTML

cipherbot: not_applicable — template default: enrol once the repository implements cryptography

• ⚪ not applicable: template default: enrol once the repository implements cryptography

echidnabot: not_applicable — template default: enrol once the repository carries proofs and an ECHIDNA engine is configured

• ⚪ not applicable: template default: enrol once the repository carries proofs and an ECHIDNA engine is configured

panicbot: not_applicable — panic-attack is already graded by the verdict grid's own panic-attack row, from static-analysis-gate.yml evidence; enrolling panicbot would report one scanner twice and give two rows that can disagree

• ⚪ not applicable: panic-attack is already graded by the verdict grid's own panic-attack row, from static-analysis-gate.yml evidence; enrolling panicbot would report one scanner twice and give two rows that can disagree

seambot: not_applicable — template default: enrol once a seam register exists at spec/seams/seam-register.json

• ⚪ not applicable: template default: enrol once a seam register exists at spec/seams/seam-register.json

sustainabot: not_applicable — reserved fleet slot; no adapter exists (gitbot-fleet bots/sustainabot/README.adoc)

• ⚪ not applicable: reserved fleet slot; no adapter exists (gitbot-fleet bots/sustainabot/README.adoc)

Scope: static findings reported by each row's tool at the named commit. The table grades only findings in files this change touches, so the colour answers "does this change introduce anything?", not "what does the whole repository still carry?". Standing findings are counted in each accordion and in report.json; the baseline filter remains the place where acknowledged debt is recorded. The lane state is the worst GATING row; advisory rows are listed and counted but never set it. Purple, red, yellow and blue grade the worst GRADED finding present; orange is evidence missing, malformed or a scanner that did not run; grey is an explicit scope exclusion with its reason. No row is a security certification. report.json, badge.json and the raw findings are in the verdict-grid artifact on the linked run.

[sonarqubecloud]

Quality Gate passed

Issues
0 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]

The two reds on this PR come from main, not from this change.

• Canon lockstep: the fix from chore(canon): adopt canon 2.1.5 (gate table 0.3.1; criteria unchanged) #27 (canon 2.1.5) is now ported into this branch, as commit efb9aa9.
• estate-rules: main fails at "Use-this-template mint end to end". The inherited mint test re-mints this already-minted tree and stops on an unfilled {{OWNER}} token. The fix is chore(template): sync the mint machinery to rsr-template-repo 2be7b88 #28, a template sync that touches 64 files. That's too much to port into a proof PR, so this one goes green on estate-rules once chore(template): sync the mint machinery to rsr-template-repo 2be7b88 #28 merges.

This PR's own gates pass on 2f342bc, and the receipt check passes too:

• the proof suite, with all 4 expected rejections refused at their intended declarations;
• the laws certificate.

---

Generated by Claude Code

[chatgpt-codex-connector]

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:46:38.208978Z We couldn’t complete this review. Comment @codex review to try again.	efb9aa9	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]

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

[hyperpolymath]

Superseded: #30 landed --cubical-compatible on main, and #32 (the version the owner chose, with the flag-control fixture and grades derived from leg states) is merged on top. The legs work that was stacked here continues in #34, based on main.

---

Generated by Claude Code