docs: reflect 2026-06-02 session updates (#110/116-123)

[hyperpolymath]

Summary

CHANGELOG, README, and STATE.a2ml now reflect later-in-the-day PRs of 2026-06-02:

• fix(cicd): clear 2 governance reds inherited by 4 open PRs #110 governance reds cleared
• docs: followup for PRs #112 / #113 / #115 #116 doc followup gathering fix(proofs/idris2): rename AuditEntry.proof to avoid Idris2 0.8.0 keyword clash #112/fix(proofs/idris2): RMO.idr hardwareEraseIrreversible parse fix #113/proofs(idris2): close reverseConcat via Data.List.revAppend (#89 sub-marker) #115
• fix(proofs/idris2): RMO.idr overwriteIrreversible + auditTrailCompleteness type fixes #117 RMO.idr type fixes
• ci(idris2): flip build oracle to strict (closes #70 follow-up) #118 Idris2 build oracle flipped to strict
• feat(fs): O_NOATIME discipline for pure-read theorems (#94 Gap 9) #120 O_NOATIME / fs_pure.rs (Tier-S: #45 sub — 10 remaining practice gaps (3-12, gap-per-PR) #94 Gap 9; 757→764 tests)
• fix(proofs/idris2): redesign Category A non-theorems (#119A) #121 Cat A non-theorem redesigns (closes #119A)
• fix(ci): idris-verification install chez symlink for Ubuntu's chezscheme #122 idris-verification chez symlink fix
• proof(model): close equivSym via Data.Bool.andCommutative (1/5 Cat B) #123 equivSym Qed-closed (1/5 Cat B)

README also notes 4 annotated admits in proofs/coq/rmo_operations.v and the Idris2 0.8.0 keyword/parse fixes.

Test plan

• No license/SPDX content touched
• Markdown / AsciiDoc renders

[github-actions]

🔍 Hypatia Security Scan

Findings: 121 issues detected

Severity	Count
🔴 Critical	10
🟠 High	36
🟡 Medium	75

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_workflow",
    "file": "codeql.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "lean-verification.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
    "type": "download_then_run",
    "file": "rust-cli.yml",
    "action": "verify_download_integrity",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in casket-pages.yml",
    "type": "missing_timeout_minutes",
    "file": "casket-pages.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_batch.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_batch.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in cflite_pr.yml",
    "type": "missing_timeout_minutes",
    "file": "cflite_pr.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in compilation_tests.yml",
    "type": "missing_timeout_minutes",
    "file": "compilation_tests.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in compilation_tests.yml",
    "type": "missing_timeout_minutes",
    "file": "compilation_tests.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence