Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .github/workflows/agda-meta-checker.yml
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ jobs:
verify-proofs:
name: Type-check Agda proofs
runs-on: ubuntu-latest
timeout-minutes: 15
steps:
- name: Checkout
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/boj-build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ concurrency:
jobs:
trigger-boj:
runs-on: ubuntu-latest
timeout-minutes: 5
steps:
- name: Checkout
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/cargo-audit.yml
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ jobs:
audit:
name: Dependency audit
runs-on: ubuntu-latest
timeout-minutes: 10

steps:
- name: Checkout repository
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/cflite_batch.yml
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ permissions:
jobs:
BatchFuzzing:
runs-on: ubuntu-latest
timeout-minutes: 45
strategy:
fail-fast: false
matrix:
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/cflite_pr.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ permissions:
jobs:
PR:
runs-on: ubuntu-latest
timeout-minutes: 15
strategy:
fail-fast: false
matrix:
Expand Down
66 changes: 44 additions & 22 deletions .github/workflows/chapel-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,17 @@ concurrency:

permissions: read-all

# Pinned Chapel deb (Ubuntu 22.04 amd64; installs cleanly on the
# ubuntu24 runner). SHA-256 verified against the GitHub Releases asset;
# mismatch fails the install step. Bumped 2.3.0 -> 2.8.0 (issue #181)
# to track sibling estate repos proven (#141) and panic-attack (#85),
# both of which validated this URL+SHA combo against the same
# `ubuntu-latest` runner image we use here.
env:
CHAPEL_VERSION: '2.8.0'
CHAPEL_DEB_URL: 'https://github.com/chapel-lang/chapel/releases/download/2.8.0/chapel-2.8.0-1.ubuntu22.amd64.deb'
CHAPEL_DEB_SHA256: '944a454b8a791f344312fcd261b562871159b74f5ef41d81e11833eb21d85f60'

jobs:
# Job 1: Compile Chapel .chpl files into a static library.
#
Expand All @@ -35,30 +46,36 @@ jobs:
# compiling, the workflow fails.
#
# Why --static and not --dynamic:
# The official apt deb (chapel-2.3.0-1.ubuntu24.amd64.deb) ships only
# the CHPL_LIB_PIC=none runtime variant. Building a shared library
# requires CHPL_LIB_PIC=pic runtime objects which are not in the
# package; the linker rejects the non-PIC `libchpl.a` with
# The official apt deb (chapel-${CHAPEL_VERSION}-1.ubuntu22.amd64.deb)
# ships only the CHPL_LIB_PIC=none runtime variant. Building a shared
# library requires CHPL_LIB_PIC=pic runtime objects which are not in
# the package; the linker rejects the non-PIC `libchpl.a` with
# `relocation R_X86_64_TPOFF32 ... can not be used when making a
# shared object`. Until the CI image ships a PIC-enabled runtime
# (or we adopt a from-source Chapel build), the metalayer is
# (or we adopt a from-source Chapel build via the
# `chapel-pic-from-source` Justfile recipe), the metalayer is
# distributed as `libechidna_chapel.a` and the Zig FFI links it
# statically.
chapel-build:
name: Compile Chapel Metalayer
runs-on: ubuntu-latest
runs-on: ubuntu-22.04
timeout-minutes: 30
steps:
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

- name: Install Chapel
- name: Install Chapel ${{ env.CHAPEL_VERSION }} (SHA-pinned .deb)
run: |
# Install Chapel from official apt repository.
# SHA256 of the deb is pinned for supply-chain integrity; bump
# alongside the version tag when upgrading.
curl -fsSL --max-time 300 \
https://github.com/chapel-lang/chapel/releases/download/2.3.0/chapel-2.3.0-1.ubuntu24.amd64.deb \
-o /tmp/chapel.deb
sudo dpkg -i /tmp/chapel.deb || sudo apt-get install -f -y
set -euo pipefail
# libunwind-dev is a runtime link-time dep for chpl-built binaries
# on the ubuntu .deb path; sibling estate repo panic-attack (#85)
# established this preinstall as the working pattern, reused by
# proven (#141). Without it the chapel-build smoke link fails with
# `error while loading shared libraries: libunwind.so.8`.
sudo apt-get update -qq
sudo apt-get install -y libunwind-dev
curl -fsSL --max-time 300 --retry 3 -o /tmp/chapel.deb "$CHAPEL_DEB_URL"
echo "$CHAPEL_DEB_SHA256 /tmp/chapel.deb" | sha256sum --check
sudo apt-get install -y /tmp/chapel.deb
chpl --version

- name: Compile Chapel proof search library (static)
Expand Down Expand Up @@ -93,7 +110,8 @@ jobs:
# `src/zig_ffi/build.zig`.
zig-ffi:
name: Build & Test Zig FFI Bridge
runs-on: ubuntu-latest
runs-on: ubuntu-22.04
timeout-minutes: 20
steps:
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

Expand Down Expand Up @@ -121,7 +139,8 @@ jobs:
# Re-enable strict gating once #133's Chapel + FFI rehabilitation lands.
rust-chapel-feature:
name: Rust Build with Chapel Feature
runs-on: ubuntu-latest
runs-on: ubuntu-22.04
timeout-minutes: 20
needs: zig-ffi
continue-on-error: true
steps:
Expand Down Expand Up @@ -159,18 +178,21 @@ jobs:
# and flip this job to strict.
rust-chapel-real:
name: Rust Build β€” Real Chapel Library (allow-fail, L2.3+ gate)
runs-on: ubuntu-latest
runs-on: ubuntu-22.04
timeout-minutes: 30
needs: [chapel-build, zig-ffi]
continue-on-error: true
steps:
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

- name: Install Chapel
- name: Install Chapel ${{ env.CHAPEL_VERSION }} (SHA-pinned .deb)
run: |
curl -fsSL --max-time 300 \
https://github.com/chapel-lang/chapel/releases/download/2.3.0/chapel-2.3.0-1.ubuntu24.amd64.deb \
-o /tmp/chapel.deb
sudo dpkg -i /tmp/chapel.deb || sudo apt-get install -f -y
set -euo pipefail
sudo apt-get update -qq
sudo apt-get install -y libunwind-dev
curl -fsSL --max-time 300 --retry 3 -o /tmp/chapel.deb "$CHAPEL_DEB_URL"
echo "$CHAPEL_DEB_SHA256 /tmp/chapel.deb" | sha256sum --check
sudo apt-get install -y /tmp/chapel.deb
chpl --version

- name: Install Zig
Expand Down
3 changes: 3 additions & 0 deletions .github/workflows/codeql.yml
Original file line number Diff line number Diff line change
Expand Up @@ -26,12 +26,15 @@ jobs:
permissions:
contents: read
security-events: write
timeout-minutes: 15
strategy:
fail-fast: false
matrix:
include:
- language: javascript-typescript
build-mode: none
- language: cpp
build-mode: none

steps:
- name: Checkout
Expand Down
2 changes: 2 additions & 0 deletions .github/workflows/container-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,7 @@ jobs:
container-build:
name: Build & verify container image
runs-on: ubuntu-latest
timeout-minutes: 90

steps:
- name: Checkout
Expand Down Expand Up @@ -110,6 +111,7 @@ jobs:
tier3-container:
name: Tier-3 / ${{ matrix.prover }}
runs-on: ubuntu-latest
timeout-minutes: 90
# Run on schedule or when the .containerization tree changes on main.
# Not a merge gate β€” these are informational weekly builds.
if: >-
Expand Down
6 changes: 6 additions & 0 deletions .github/workflows/dogfood-gate.yml
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,7 @@ jobs:
a2ml-validate:
name: Validate A2ML manifests
runs-on: ubuntu-latest
timeout-minutes: 5

steps:
- name: Checkout repository
Expand Down Expand Up @@ -72,6 +73,7 @@ jobs:
k9-validate:
name: Validate K9 contracts
runs-on: ubuntu-latest
timeout-minutes: 5

steps:
- name: Checkout repository
Expand Down Expand Up @@ -121,6 +123,7 @@ jobs:
empty-lint:
name: Empty-linter (invisible characters)
runs-on: ubuntu-latest
timeout-minutes: 5

steps:
- name: Checkout repository
Expand Down Expand Up @@ -185,6 +188,7 @@ jobs:
groove-check:
name: Groove manifest check
runs-on: ubuntu-latest
timeout-minutes: 5

steps:
- name: Checkout repository
Expand Down Expand Up @@ -243,6 +247,7 @@ jobs:
eclexiaiser-validate:
name: Validate eclexiaiser manifest
runs-on: ubuntu-latest
timeout-minutes: 5

steps:
- name: Checkout repository
Expand Down Expand Up @@ -312,6 +317,7 @@ jobs:
dogfood-summary:
name: Dogfooding compliance summary
runs-on: ubuntu-latest
timeout-minutes: 5
needs: [a2ml-validate, k9-validate, empty-lint, groove-check, eclexiaiser-validate]
if: always()

Expand Down
2 changes: 2 additions & 0 deletions .github/workflows/formal-verification.yml
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ jobs:
stable-tests:
name: Trust-pipeline invariant tests (stable)
runs-on: ubuntu-latest
timeout-minutes: 15

steps:
- name: Checkout repository
Expand All @@ -67,6 +68,7 @@ jobs:
creusot-verify:
name: Creusot formal verification
runs-on: ubuntu-latest
timeout-minutes: 15
# No continue-on-error β€” this is a hard merge gate as of Stage 8c-M3.
# The outer-loop invariant for compute is now live; all obligations
# (PO-1..P8, PO-A1..A12) must discharge under Why3+Z3.
Expand Down
2 changes: 2 additions & 0 deletions .github/workflows/generator-generic-ossf-slsa3-publish.yml
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ on:
jobs:
build:
runs-on: ubuntu-latest
timeout-minutes: 10
outputs:
digests: ${{ steps.hash.outputs.digests }}

Expand Down Expand Up @@ -60,6 +61,7 @@ jobs:

provenance:
needs: [build]
timeout-minutes: 10
permissions:
actions: read # To read the workflow path.
id-token: write # To sign the provenance.
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/ghcr-publish.yml
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ env:
jobs:
build-and-push:
runs-on: ubuntu-latest
timeout-minutes: 10
permissions:
contents: read
packages: write
Expand Down
3 changes: 2 additions & 1 deletion .github/workflows/governance.yml
Original file line number Diff line number Diff line change
Expand Up @@ -31,4 +31,5 @@ permissions:

jobs:
governance:
uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@3f34549c03274ec7a74683068f03a492b0fa805f # main 2026-06-01 (R5 generic β€” standards#330; consumes .github/canonical-references/)
uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@861b5e911d9e5dcfb3c0ab3dd2a9a3c8fd0a1613
timeout-minutes: 10
1 change: 1 addition & 0 deletions .github/workflows/hypatia-scan.yml
Original file line number Diff line number Diff line change
Expand Up @@ -26,4 +26,5 @@ permissions:
jobs:
hypatia:
uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@915139d73560e65a8240b8fc7768698658502c89
timeout-minutes: 10
secrets: inherit
1 change: 1 addition & 0 deletions .github/workflows/idris2-abi-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ jobs:
idris2-typecheck:
name: Type-check Idris2 ABI definitions
runs-on: ubuntu-latest
timeout-minutes: 30
steps:
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2

Expand Down
1 change: 1 addition & 0 deletions .github/workflows/instant-sync.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ permissions:
jobs:
dispatch:
runs-on: ubuntu-latest
timeout-minutes: 10
steps:
- name: Trigger Propagation
uses: peter-evans/repository-dispatch@28959ce8df70de7be546dd1250a005dd32156697 # v3
Expand Down
6 changes: 6 additions & 0 deletions .github/workflows/live-provers.yml
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ jobs:
name: T1 / ${{ matrix.backend }}
if: github.event_name != 'schedule' || github.event.schedule == '0 3 * * *'
runs-on: ubuntu-latest
timeout-minutes: 15
strategy:
fail-fast: false
matrix:
Expand Down Expand Up @@ -126,6 +127,7 @@ jobs:
name: T1 Guix manifest check
if: github.event_name != 'schedule'
runs-on: ubuntu-latest
timeout-minutes: 15
continue-on-error: true
steps:
- name: Checkout
Expand All @@ -147,6 +149,7 @@ jobs:
name: T2 / ${{ matrix.backend }}
if: github.event_name == 'schedule' && github.event.schedule == '0 3 * * *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '2' || inputs.tier == 'all'))
runs-on: ubuntu-latest
timeout-minutes: 15
strategy:
fail-fast: false
matrix:
Expand Down Expand Up @@ -294,6 +297,7 @@ jobs:
name: T3 / ${{ matrix.backend }}
if: github.event_name == 'schedule' && github.event.schedule == '0 5 * * 0' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '3' || inputs.tier == 'all'))
runs-on: ubuntu-latest
timeout-minutes: 15
continue-on-error: true
strategy:
fail-fast: false
Expand Down Expand Up @@ -408,6 +412,7 @@ jobs:
name: T4 niche provers
if: github.event_name == 'schedule' && github.event.schedule == '0 6 1 */3 *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '4' || inputs.tier == 'all'))
runs-on: ubuntu-latest
timeout-minutes: 15
continue-on-error: true
steps:
- name: Checkout
Expand All @@ -427,6 +432,7 @@ jobs:
name: T4 / ${{ matrix.backend }}
if: github.event_name == 'schedule' && github.event.schedule == '0 6 1 */3 *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '4' || inputs.tier == 'all'))
runs-on: ubuntu-latest
timeout-minutes: 15
continue-on-error: true
strategy:
fail-fast: false
Expand Down
9 changes: 9 additions & 0 deletions .github/workflows/mirror.yml
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,19 @@ on:
branches: [main]
workflow_dispatch:

# Estate guardrail: cancel superseded runs so re-pushes / rebased PR
# updates do not pile up queued runs against the shared account-wide
# Actions concurrency pool. Applied only to read-only check workflows
# (no publish/mutation), so cancelling a superseded run is always safe.
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true

permissions:
contents: read

jobs:
mirror:
uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@e6b2884722350515934d443daf23442f2195796f
timeout-minutes: 10
secrets: inherit
1 change: 1 addition & 0 deletions .github/workflows/mvp-smoke.yml
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ jobs:
mvp-smoke:
name: MVP Smoke
runs-on: ubuntu-latest
timeout-minutes: 15
permissions:
contents: read
steps:
Expand Down
1 change: 1 addition & 0 deletions .github/workflows/rust-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ permissions:
jobs:
rust-ci:
uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@cc5a372af1af1b202c17f1b21efd954e6c038bef
timeout-minutes: 30
with:
enable_audit: true
enable_coverage: true
Loading
Loading