Merge main into git-reticulator standardization PR

Author: hyperpolymath

.github/ISSUE_TEMPLATE/bug_report.md

@@ -0,0 +1,38 @@
+---
+name: Bug report
+about: Create a report to help us improve
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Describe the bug**
+A clear and concise description of what the bug is.
+
+**To Reproduce**
+Steps to reproduce the behavior:
+1. Go to '...'
+2. Click on '....'
+3. Scroll down to '....'
+4. See error
+
+**Expected behavior**
+A clear and concise description of what you expected to happen.
+
+**Screenshots**
+If applicable, add screenshots to help explain your problem.
+
+**Desktop (please complete the following information):**
+ - OS: [e.g. iOS]
+ - Browser [e.g. chrome, safari]
+ - Version [e.g. 22]
+
+**Smartphone (please complete the following information):**
+ - Device: [e.g. iPhone6]
+ - OS: [e.g. iOS8.1]
+ - Browser [e.g. stock browser, safari]
+ - Version [e.g. 22]
+
+**Additional context**
+Add any other context about the problem here.

.github/ISSUE_TEMPLATE/custom.md

@@ -0,0 +1,10 @@
+---
+name: Custom issue template
+about: Describe this issue template's purpose here.
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+

.github/ISSUE_TEMPLATE/feature_request.md

@@ -0,0 +1,20 @@
+---
+name: Feature request
+about: Suggest an idea for this project
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Is your feature request related to a problem? Please describe.**
+A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]
+
+**Describe the solution you'd like**
+A clear and concise description of what you want to happen.
+
+**Describe alternatives you've considered**
+A clear and concise description of any alternative solutions or features you've considered.
+
+**Additional context**
+Add any other context or screenshots about the feature request here.

.github/workflows/casket-pages.yml

@@ -18,10 +18,10 @@ concurrency:
 jobs:
   build:
     runs-on: ubuntu-latest
-    timeout-minutes: 15
+    timeout-minutes: 10
     steps:
       - name: Checkout
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4
 
       - name: Setup Pages
         uses: actions/configure-pages@45bfe0192ca1faeb007ade9deae92b16b8254a0d # v6.0.0
@@ -36,8 +36,8 @@ jobs:
       name: github-pages
       url: ${{ steps.deployment.outputs.page_url }}
     runs-on: ubuntu-latest
-    timeout-minutes: 15
     needs: build
+    timeout-minutes: 10
     steps:
       - name: Deploy to GitHub Pages
         id: deployment

.github/workflows/hypatia-scan.yml

@@ -25,6 +25,5 @@ permissions:
 
 jobs:
   hypatia:
-    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@6cd3772824e59c8c9affeab66061e25383544242
-    timeout-minutes: 10
+    uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@915139d73560e65a8240b8fc7768698658502c89
     secrets: inherit

.github/workflows/mirror.yml

@@ -0,0 +1,15 @@
+# SPDX-License-Identifier: MPL-2.0
+name: Mirror to Git Forges
+
+on:
+  push:
+    branches: [main]
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  mirror:
+    uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@e6b2884722350515934d443daf23442f2195796f
+    secrets: inherit

.github/workflows/proof-corpus.yml

@@ -0,0 +1,67 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# proof-corpus.yml — machine-checks the git-reticulator Idris2 proof corpus.
+#
+# First mechanized proofs for the lattice core (see PROOF-NEEDS.md): elementary
+# order theory (P1a witnessed, P2a essence). The gate fails if the corpus stops
+# typechecking under idris2 0.8.0, or if a proof-escape symbol is introduced.
+# Mirrors the canonical vcl-ut `proof-corpus.yml`, plus `libgmp-dev` (required by
+# the Idris2 RefC support lib and missing from the vcl-ut recipe).
+
+name: Proof Corpus
+
+on:
+  pull_request:
+    branches: ['**']
+  push:
+    branches: [main, master]
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  machine-check:
+    name: idris2 0.8.0 --build git-reticulator-proofs
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+
+      # Idris2 0.8.0 from PINNED official source (tag v0.8.0 == this commit).
+      # No maintained setup action exists; a SHA-pinned source build is
+      # deterministic and depends on no third-party action.
+      - name: Build & install Idris2 0.8.0 from pinned source
+        run: |
+          set -euo pipefail
+          sudo apt-get update -qq
+          sudo apt-get install -y --no-install-recommends chezscheme make gcc libgmp-dev
+          git clone --no-checkout https://github.com/idris-lang/Idris2.git /tmp/Idris2
+          git -C /tmp/Idris2 checkout 15a3e4e70843f7a34100f6470c04b791330788df
+          make -C /tmp/Idris2 bootstrap SCHEME=chezscheme
+          make -C /tmp/Idris2 install PREFIX="$HOME/.idris2"
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+          echo "IDRIS2_PREFIX=$HOME/.idris2" >> "$GITHUB_ENV"
+
+      - name: Proof-escape audit (no believe_me / postulate / assert_* / sorry)
+        run: |
+          set -euo pipefail
+          files="verification/proofs/Lattice/Order.idr"
+          if grep -nE '\b(believe_me|really_believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry)\b' \
+               $files | grep -vE ':\s*(--|\|\|\|)' ; then
+            echo "::error::proof-escape symbol found in the corpus"
+            exit 1
+          fi
+          echo "OK: zero proof-escape symbols outside comments"
+
+      - name: Build the proof corpus
+        run: |
+          set -euo pipefail
+          idris2 --version
+          cd verification/proofs && idris2 --build git-reticulator-proofs.ipkg

.github/workflows/rust-ci.yml

@@ -14,5 +14,4 @@ permissions:
 
 jobs:
   rust-ci:
-    uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@f5f0506a6ec88e574753eee701a268e0d4b3a7f2
-    timeout-minutes: 10
+    uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@cc5a372af1af1b202c17f1b21efd954e6c038bef

.github/workflows/scorecard.yml

@@ -0,0 +1,26 @@
+# SPDX-License-Identifier: MPL-2.0
+name: Scorecards supply-chain security
+
+on:
+  branch_protection_rule:
+  schedule:
+    - cron: '23 4 * * 1'
+  push:
+    branches: [main]
+
+# Workflow-level permissions are read-only. The job that calls the reusable
+# upgrades to the writes `ossf/scorecard-action` requires. Job-level
+# permissions REPLACE workflow-level for that job, so `contents: read` here
+# plus the writes below yields the correct effective set and avoids the
+# `read-all` startup_failure seen estate-wide. Matches the canonical caller in
+# hyperpolymath/standards/.github/workflows/scorecard-reusable.yml.
+permissions:
+  contents: read
+
+jobs:
+  analysis:
+    permissions:
+      security-events: write
+      id-token: write
+    uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@e03686486e11b662834d7090dffae54c3e96fd59
+    secrets: inherit

.github/workflows/secret-scanner.yml

@@ -0,0 +1,19 @@
+# SPDX-License-Identifier: MPL-2.0
+name: Secret Scanner
+
+on:
+  pull_request:
+  push:
+    branches: [main]
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  scan:
+    uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@3e4bd4c93911750727e2e4c66dff859e00079da0
+    secrets: inherit