diff --git a/.gitbot-fleet/enrolment.json b/.gitbot-fleet/enrolment.json new file mode 100644 index 0000000..a4ace59 --- /dev/null +++ b/.gitbot-fleet/enrolment.json @@ -0,0 +1,14 @@ +{ + "schema": 1, + "reporters": { + "echidnabot": { "enrolled": false, "reason": "proofs here are gated by their own toolchains (proofs.yml: Idris2, Lean, Agda); no ECHIDNA engine is configured, so this adapter could only ever report not_run" }, + "rhodibot": { "title": "rhodibot (RSR compliance)", "enrolled": true, "gating": false }, + "panicbot": { "enrolled": false, "reason": "panic-attack already reports directly as its own row in the Hypatia verdict grid; enrolling panicbot would count the same findings twice" }, + "sustainabot": { "enrolled": false, "reason": "reserved fleet slot; no adapter exists (gitbot-fleet README)" }, + "glambot": { "title": "glambot (presentation quality)", "enrolled": true, "gating": false }, + "seambot": { "enrolled": false, "reason": "no seam register is declared (spec/seams/seam-register.json)" }, + "finishingbot": { "title": "finishingbot (release readiness)", "enrolled": true, "gating": false }, + "cipherbot": { "enrolled": false, "reason": "no cryptography is implemented in this repository; the hashes present are checksum/integrity pins, which cipherbot would report as cryptographic findings" }, + "accessibilitybot": { "enrolled": false, "reason": "no served HTML surface; this is a checker library/CLI with AsciiDoc documentation" } + } +} diff --git a/.gitbot-fleet/report-backs/README.adoc b/.gitbot-fleet/report-backs/README.adoc new file mode 100644 index 0000000..15e5180 --- /dev/null +++ b/.gitbot-fleet/report-backs/README.adoc @@ -0,0 +1,24 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <[REDACTED_EMAIL]> += gitbot-fleet report-backs + +One JSON envelope per enrolled fleet member (`.gitbot-fleet/enrolment.json`). +The Hypatia verdict grid reads this directory when it renders, so a +report-back here is the only way a member's row stops being orange. The +envelope contract is `docs/VERDICT-GRID-SPEC.adoc` in hyperpolymath/standards; +the producer is documented in gitbot-fleet's `docs/REPORT-BACK.adoc`. + +*How the files get here.* The `fleet` job of +`.github/workflows/fork-governance.yml` (gitbot-fleet's +`fleet-report-back-reusable.yml`) runs the enrolled adapters on the PR head +and uploads the envelopes as the `fleet-report-backs` artifact; the Hypatia +lane downloads that artifact into this directory just before rendering. +Nothing is ever committed here: an envelope is evidence about one commit, and +a committed one would read as current when it is stale. The directory exists +because this repository's deed declares it +(`trope-checker_chora.deed`, `:report-backs ".gitbot-fleet/report-backs/"`), +and it is empty in git on purpose. An enrolled member with no report-back +renders *orange* ("enrolled, but no report-back was received"), never green; +do not add a placeholder envelope to turn a row green. Only a real run may. + +Only files matching `*.json` are read, so this README is inert. diff --git a/.githooks/validate-a2ml.sh b/.githooks/validate-a2ml.sh index b16fa85..1ea7061 100755 --- a/.githooks/validate-a2ml.sh +++ b/.githooks/validate-a2ml.sh @@ -330,6 +330,7 @@ validate_a2ml() { # --- Check 4: Section heading syntax --- # Validate that [section] headings are well-formed (no unclosed brackets) line_num=0 + # shellcheck disable=SC2094 # report_issue annotates $file on stdout; it never writes it while IFS= read -r line; do line_num=$((line_num + 1)) # Lines starting with [ should have a matching ] diff --git a/.github/affirmation-trusted/README.adoc b/.github/affirmation-trusted/README.adoc new file mode 100644 index 0000000..d00d56a --- /dev/null +++ b/.github/affirmation-trusted/README.adoc @@ -0,0 +1,35 @@ +// SPDX-License-Identifier: MPL-2.0 += Affirmation-check trust material + +`github-web-flow.gpg` in this directory is GitHub's *current* web-flow +commit-signing public key: + +* fingerprint: `9684 79A1 AFF9 27E3 7D1A 566B B569 0EEE BB95 2194` +* created 2024-01-16, no expiry +* fetched 2026-10-28 from `gh api users/web-flow/gpg_keys` + (the entry with `key_id` `B5690EEEBB952194`) + +== Why it exists + +The Affirmation Document Gate (`hyperpolymath/cicd-suite` +`actions/affirmation-check`, run from `main-estate-audit.yml`) classifies the +signature on the commit that last changed `AFFIRMATION.adoc`. The copy of the +web-flow key vendored inside that action is GitHub's *previous* key +(`5DE3E0509C47EA3CF04A42D34AEE18F83AFDEB23`, expired 2024-01-16) — the action's +own fingerprint allowlist names the new key, but the new key is not in its +keyring. Every GitHub-signed commit (web merges, squash landings, and the +test-merge commit a shallow PR checkout consists of) therefore classified as +`E` ("cannot be checked"), which the gate treats as "bad, revoked, or failed +verification" and fails on. That was the `estate-audit` failure on PR #102. + +The workflow now runs `.github/affirmation-trusted/check.sh`, vendored from +`cicd-suite@bf7dd95cf49733019343ff485c2f45c6b261839c` with a local repair: +`E` accompanied by GnuPG's `NO_PUBKEY` is a notice; bad, revoked, and other failed +verifications still fail. The local script imports both the current and +historical vendored GitHub keys and rejects them unless their primary +fingerprints match the two pinned above. This is a contained workaround, not +the durable trust boundary: gate code in a pull-request checkout is necessarily +reviewed code, whereas the root fix belongs in `cicd-suite`, whose pinned +external action can then be restored. If GitHub rotates the web-flow key +again, re-fetch it the same way and update the fingerprint above in the same +commit. diff --git a/.github/affirmation-trusted/allowed_signers b/.github/affirmation-trusted/allowed_signers new file mode 100644 index 0000000..24ffba0 --- /dev/null +++ b/.github/affirmation-trusted/allowed_signers @@ -0,0 +1,6 @@ +# SPDX-License-Identifier: MPL-2.0 +# SSH commit-signing keys of the estate owner, from https://api.github.com/users/hyperpolymath/ssh_signing_keys +# (fetched 2026-10-02). Only the GitHub noreply principal is listed. +6759885+hyperpolymath@users.noreply.github.com namespaces="git" ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIOpGzhVGVlqEQuGus7hiS66b1PBWjel6ahCjBBLVDqCg +6759885+hyperpolymath@users.noreply.github.com namespaces="git" ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIBFX2cMllRUW/TjfJ9rHg6oALk7UfxzZrh7tDShhbLQ0 +6759885+hyperpolymath@users.noreply.github.com namespaces="git" ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIBp4I5S7wV5b8xEUfcVI+E/9FQPoA2XO/9aMPfTOGa1p diff --git a/.github/affirmation-trusted/check.sh b/.github/affirmation-trusted/check.sh new file mode 100755 index 0000000..15d12b1 --- /dev/null +++ b/.github/affirmation-trusted/check.sh @@ -0,0 +1,222 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Vendored from hyperpolymath/cicd-suite@bf7dd95cf49733019343ff485c2f45c6b261839c +# Local repair: distinguish unavailable PGP keys from failed verification. + +set -euo pipefail + +root=${GITHUB_WORKSPACE:-.} +required=${AFFIRMATION_REQUIRED:-false} +aff_file= + +for candidate in AFFIRMATION.adoc AFFIRMATION.md AFFIRMATION; do + if [[ -f "$root/$candidate" ]]; then + aff_file=$candidate + break + fi +done + +if [[ -z "$aff_file" ]]; then + if [[ "$required" == "true" ]]; then + echo "::error::AFFIRMATION.adoc is required by the declared governance-tier capability." >&2 + exit 1 + fi + echo "::notice::AFFIRMATION is not applicable: governance-tier was not required." + exit 0 +fi + +path=$root/$aff_file +echo "Found AFFIRMATION document: $aff_file" + +substantive_lines=$(awk '!/^[[:space:]]*(#|\/\/|;|$)/ { count++ } END { print count + 0 }' "$path") +if (( substantive_lines < 5 )); then + echo "::error::$aff_file has only $substantive_lines substantive lines; it is a stub, not an affirmation." >&2 + exit 1 +fi + +# An inline code span (`...`) quotes text rather than asserting it: an +# affirmation may name the placeholder syntax it swept for, e.g. "`{{PROJECT}}` +# tokens were substituted". Strip code spans before matching so that only +# placeholders left in the prose itself count. +# shellcheck disable=SC2016 # Backticks are literal AsciiDoc code-span delimiters. +placeholders=$(sed -E 's/`[^`]*`//g' "$path" | + grep -niE '\{\{|TODO: update|&2 + printf '%s\n' "$placeholders" | head -5 + exit 1 +fi + +# The signature is the signature on the commit containing this content. Text +# such as "Signed:" inside the document proves nothing. Shallow checkouts may +# not contain the file-changing commit, so report that limitation honestly. +# +# Git can only classify a signature whose key it holds; without the key it +# reports E; the raw status below distinguishes NO_PUBKEY from a broken check. +# Merges made on +# github.com (squash, merge, web edits) are signed by GitHub's web-flow key, +# so that key is vendored here and trusted inside a throwaway keyring. The +# estate owner's SSH signing keys are vendored as allowed_signers. Trust comes +# only from these files and from what the caller names explicitly — never from +# the checked-out tree by default, because on a pull request that tree is the +# contributor's. Callers may add PGP keys (AFFIRMATION_TRUSTED_GPG_KEYS, one +# armoured file) and SSH signers (AFFIRMATION_ALLOWED_SIGNERS, a git +# allowed_signers file); relative paths are resolved against the repository +# root, so name such a file only where the tree is protected. +here=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd) +github_fingerprints=" 968479A1AFF927E37D1A566BB5690EEEBB952194 5DE3E0509C47EA3CF04A42D34AEE18F83AFDEB23 " +vendored_gpg_keys=("$here/github-web-flow.gpg" "$here/github-web-flow-previous.gpg") +trusted_gpg_keys=() +if [[ -n "${AFFIRMATION_TRUSTED_GPG_KEYS:-}" ]]; then + extra_keys=$AFFIRMATION_TRUSTED_GPG_KEYS + [[ "$extra_keys" == /* ]] || extra_keys=$root/$extra_keys + trusted_gpg_keys+=("$extra_keys") +fi +signer_files=("$here/allowed_signers") +if [[ -n "${AFFIRMATION_ALLOWED_SIGNERS:-}" ]]; then + extra_signers=$AFFIRMATION_ALLOWED_SIGNERS + [[ "$extra_signers" == /* ]] || extra_signers=$root/$extra_signers + signer_files+=("$extra_signers") +fi + +# Build a private GnuPG home holding only the trusted keys, each given +# ultimate owner trust, and print its path. If a key file cannot be imported +# the home is left empty, so nothing is trusted — the runner's own keyring is +# never consulted. Prints nothing only if gpg is absent. +primary_fingerprints_in_home() { + local keyring_home=$1 + gpg --batch --homedir "$keyring_home" --with-colons --fingerprint 2>/dev/null \ + | awk -F: '$1 == "pub" { primary = 1; next } primary && $1 == "fpr" { print $10; primary = 0 }' +} + +make_trusted_gnupg_home() { + local keyring_home key_file imported_fpr + local -a imported_fprs=() + command -v gpg >/dev/null 2>&1 || return 0 + keyring_home=$(mktemp -d) + chmod 700 "$keyring_home" + for key_file in "${vendored_gpg_keys[@]}"; do + if [[ ! -s "$key_file" ]] \ + || ! gpg --batch --quiet --homedir "$keyring_home" --import "$key_file" >/dev/null 2>&1; then + echo "::warning::Trusted PGP key file could not be imported: $key_file" >&2 + rm -rf -- "$keyring_home" + keyring_home=$(mktemp -d) + chmod 700 "$keyring_home" + printf '%s\n' "$keyring_home" + return 0 + fi + done + mapfile -t imported_fprs < <(primary_fingerprints_in_home "$keyring_home") + if ((${#imported_fprs[@]} != ${#vendored_gpg_keys[@]})); then + echo "::error::Vendored GitHub web-flow key material did not import exactly the expected keys." >&2 + rm -rf -- "$keyring_home" + return 1 + fi + for imported_fpr in "${imported_fprs[@]}"; do + if [[ "$github_fingerprints" != *" $imported_fpr "* ]]; then + echo "::error::Vendored GitHub web-flow key fingerprint is not pinned: $imported_fpr" >&2 + rm -rf -- "$keyring_home" + return 1 + fi + done + for key_file in "${trusted_gpg_keys[@]}"; do + if [[ ! -s "$key_file" ]] \ + || ! gpg --batch --quiet --homedir "$keyring_home" --import "$key_file" >/dev/null 2>&1; then + echo "::warning::Trusted PGP key file could not be imported: $key_file" >&2 + rm -rf -- "$keyring_home" + keyring_home=$(mktemp -d) + chmod 700 "$keyring_home" + printf '%s\n' "$keyring_home" + return 0 + fi + done + gpg --batch --homedir "$keyring_home" --with-colons --fingerprint 2>/dev/null \ + | awk -F: '$1 == "fpr" { print $10 ":6:" }' \ + | gpg --batch --quiet --homedir "$keyring_home" --import-ownertrust >/dev/null 2>&1 || true + printf '%s\n' "$keyring_home" +} + +signature=N +signer= +primary_fpr= +last_update_ts= +if git -C "$root" rev-parse --is-inside-work-tree >/dev/null 2>&1; then + gnupg_home=$(make_trusted_gnupg_home) + [[ -n "$gnupg_home" ]] || echo "::notice::gpg is not installed; PGP-signed commits cannot be checked." + # Git takes one allowed_signers file, so the vendored and caller-named files + # are joined. Without any file Git reports an SSH signature as N (no + # signature) instead of U (valid, signer not trusted). + allowed_signers=$(mktemp) + for signers_file in "${signer_files[@]}"; do + if [[ -s "$signers_file" ]]; then + cat -- "$signers_file" >> "$allowed_signers" + else + echo "::warning::Allowed signers file could not be read: $signers_file" + fi + done + git_verify=(git -C "$root" -c "gpg.ssh.allowedSignersFile=$allowed_signers") + if [[ -n "$gnupg_home" ]]; then + git_verify=(env "GNUPGHOME=$gnupg_home" "${git_verify[@]}") + fi + sig_line=$("${git_verify[@]}" log -1 --format='%G?%x09%GP%x09%GS' -- "$aff_file" 2>/dev/null || true) + # Split on tabs by hand: `read` would merge the empty %GP of an SSH signature. + if [[ "$sig_line" == *$'\t'*$'\t'* ]]; then + signature=${sig_line%%$'\t'*} + sig_rest=${sig_line#*$'\t'} + primary_fpr=${sig_rest%%$'\t'*} + signer=${sig_rest#*$'\t'} + fi + if [[ "$signature" == E ]]; then + aff_commit=$(git -C "$root" log -1 --format='%H' -- "$aff_file") + verify_status=$("${git_verify[@]}" verify-commit --raw "$aff_commit" 2>&1 || true) + # ERRSIG reason 9 means a missing public key. GnuPG also emits its + # generic gpg-exit failure in this case; other errors must still fail. + if grep -qE '^\[GNUPG:\] NO_PUBKEY [0-9A-F]+$' <<<"$verify_status" \ + && grep -qE '^\[GNUPG:\] ERRSIG [0-9A-F]+ [0-9]+ [0-9]+ [0-9]+ [0-9]+ 9( [0-9A-F]+)?$' <<<"$verify_status" \ + && ! grep -vE '^\[GNUPG:\] FAILURE gpg-exit [0-9]+$' <<<"$verify_status" \ + | grep -E '^\[GNUPG:\] (BADSIG|REVKEYSIG|KEYREVOKED|EXPSIG|EXPKEYSIG|FAILURE|ERROR|NODATA|BADARMOR)( |$)' >/dev/null; then + signature=K + fi + fi + last_update_ts=$(git -C "$root" log -1 --format='%at' -- "$aff_file" 2>/dev/null || true) + # In a shallow clone the boundary commit appears to add every file, so the + # commit found above may only be the boundary, not the affirmation commit. + if [[ "$(git -C "$root" rev-parse --is-shallow-repository 2>/dev/null || true)" == true ]]; then + aff_commit=$(git -C "$root" log -1 --format='%H' -- "$aff_file" 2>/dev/null || true) + shallow_file=$(git -C "$root" rev-parse --path-format=absolute --git-path shallow 2>/dev/null || true) + if [[ -n "$aff_commit" && -f "$shallow_file" ]] && grep -qxF "$aff_commit" "$shallow_file"; then + echo "::notice::The checkout is shallow: $aff_commit is the history boundary, not necessarily the commit that last changed $aff_file. Fetch more history to check that commit's signature." + fi + fi + if [[ -n "$gnupg_home" ]]; then + rm -rf -- "$gnupg_home" + fi + rm -f -- "$allowed_signers" +fi + +case "$signature" in + G) echo "Affirmation commit signature verified with a trusted key: ${signer:-unknown signer}." + if [[ -n "$primary_fpr" && "$github_fingerprints" == *" $primary_fpr "* ]]; then + echo "::notice::GitHub signed this commit when it landed through github.com; an author signature, if any, is on the pull request's head commit." + fi + ;; + U) echo "::notice::Affirmation commit has a valid signature from an untrusted or locally unknown key${signer:+: $signer}." ;; + K) echo "::notice::Affirmation commit signature cannot be checked: public key unavailable." ;; + B|R|E) echo "::error::Affirmation commit signature is bad, revoked, or failed verification." >&2; exit 1 ;; + *) echo "::notice::Affirmation commit signature could not be verified from the available Git history." ;; +esac + +# A dated affirmation is a frozen receipt, not a claim that remains current +# forever. Report age without invalidating historical evidence or forcing an +# empty monthly rewrite. +if [[ -n "$last_update_ts" ]]; then + current_ts=$(date +%s) + age_days=$(( (current_ts - last_update_ts) / 86400 )) + if (( age_days > 28 )); then + echo "::warning::$aff_file is a $age_days-day-old snapshot; verify its anchor before relying on it as current." + else + echo "$aff_file snapshot age: $age_days days." + fi +fi + +echo "AFFIRMATION document validation passed." diff --git a/.github/affirmation-trusted/github-web-flow-previous.gpg b/.github/affirmation-trusted/github-web-flow-previous.gpg new file mode 100644 index 0000000..323406e --- /dev/null +++ b/.github/affirmation-trusted/github-web-flow-previous.gpg @@ -0,0 +1,41 @@ +-----BEGIN PGP PUBLIC KEY BLOCK----- + +xsBNBFmUaEEBCACzXTDt6ZnyaVtueZASBzgnAmK13q9Urgch+sKYeIhdymjuMQta +x15OklctmrZtqre5kwPUosG3/B2/ikuPYElcHgGPL4uL5Em6S5C/oozfkYzhwRrT +SQzvYjsE4I34To4UdE9KA97wrQjGoz2Bx72WDLyWwctD3DKQtYeHXswXXtXwKfjQ +7Fy4+Bf5IPh76dA8NJ6UtjjLIDlKqdxLW4atHe6xWFaJ+XdLUtsAroZcXBeWDCPa +buXCDscJcLJRKZVc62gOZXXtPfoHqvUPp3nuLA4YjH9bphbrMWMf810Wxz9JTd3v +yWgGqNY0zbBqeZoGv+TuExlRHT8ASGFS9SVDABEBAAHNNUdpdEh1YiAod2ViLWZs +b3cgY29tbWl0IHNpZ25pbmcpIDxub3JlcGx5QGdpdGh1Yi5jb20+wsBoBBMBCAAc +BQJZlGhBCRBK7hj4Ov3rIwIbAwUJDBJ3/wIZAQAA0O4IAJd0k8M+urETyMvTqNTj +/U6nbqyOdKE4V93uUj5G7sNTfno7wod/Qjj6Zv5KodvA93HmEdQqsmVq5YJ5KGiw +cmGCpd/GqJRPaYSY0hSUSBqYHiHLusCJkPBpQTBhcEMtfVCB2J6fVeoX2DV0K1xf +CGblrSVB0viAxUMnmL5C55RuvbYZsTu8szXhkvIR96CtWbJ8QGaEf1/KSpWz8ept +Y/omf3UPfvdOjnsxc8jVEqPNaR9xC6Q6t53rBa/XgMY6IYyesnyYnc5O6JuexUFa +VjykRFtAiYfDaMARpXOmgMm0lhoBRKb/uMUaN3CSYTmE4pZweJcUi7eWgmoQljX2 +ut6ZAg0EZabFdgEQALI37i+IVAzpBCgqvQDZbSsZ0yhtMnA5myjZA+l7BvIGy4ve +s1bk6YetbBcCE8o2pQjI7N2rwyhLGhNO6ouSyhqGLEQv9fafKE4HFH0aRjP+gj1H +edhwtFoVChImhV863rWimQtTNtYB6GluBPwQqWfwmwQ2rT7ScOVZCLSHZD2gaaqW +BXOyTCZVnwt7K/gyDuE3qzDJnuahl+SSkPn5TtnZdW6sLORJJ+DjNvaUxEsmizZ4 +IBzvj0QKxfS3s4F+0X5iqCMheLFeybZGtSq9Tjs6Q61l4CG8Bh6dsLemv0WFrk3G +gFQRr7XUwr1bo5xGHC/FUJSsxRHoVNJnIL/9WldNO2tGU6qlTnAYxs/fOmf2B6o5 +cKXysXv7WAA8b+j5AVBMGxUSu7CLglaiCJC5DI7AAiUV7/t29rFZkam//Jbb4veC +4vvFocoVUaxrKGWK1BDldr4/WJKApJcPJF4Jtai1+oB6ak/JIjbkseHdJxcjo2B0 +dKtIFoWiPAB+DFs9MRDpp0iwocJCh+ucus1rdQ54YMaI44rRphXeOIQMYCi5q2Q1 +/arzkSiyPV/2VoKoAfdgskPt1xKd7WIKErmpFMHIy8jJ5IPQ1s2dUwU4alfJLJa0 +pvaV2m7wBYFAmwmz0WZgFxYAYEDamn4jFoKfqsEgcixRUVE3w5VkqwSwGRbLABEB +AAG0G0dpdEh1YiA8bm9yZXBseUBnaXRodWIuY29tPokCTgQTAQoAOBYhBJaEeaGv ++SfjfRpWa7VpDu67lSGUBQJlpsV2AhsDBQsJCAcCBhUKCQgLAgQWAgMBAh4BAheA +AAoJELVpDu67lSGUgy4QAKW9XAL416iKrQB2LElmxqAoenHVCswlau0xGLh5dVNN +p5f4/W6eEL8CZI7hfF3e5Gh6Me99aHgXSCK1QnxcqCJ6Oea4ZyrsNu3k6g7Um5ca +VbYFD4yIahhXDYHSw6FYM2sgFY479YvgvKRwacC2tFfChLRbHgwLJ3O1dBjmVycJ +Zpbyu+7taZ26g6KQfgcj3uuo3nz3p1ziIEpLHwtl/7joNEIIP/lJ8AKmUHPiGznN +6fxMvzN37PGMWtdvOi1rSNIMQYr1YY7jPnlLbFJwLrO/q/cGPU5HwGzlqh0a2ZqY +dnuwT3DREmgJ83H71xH+sTzZKs5oGlVTu6st7iWDvNpo2GoN01XzKa5caYglqsOC +uZ6IHlsdL50sXMtSROCi3hEWU9r1sWIm4k3pNz20y7lElD2X/MqbEMcgpawCV7lH +rm7MSrTgu6BNAF0SisbF9AKwXaBr2dwpMMyIBOFZO9mk4/c0n9q2FlGY4GkbgH2J +HqulFTwX/4yiQbh8gzCe+06FZAWITN1OQntTkkCQ+1MCZPf+bOfC08RTsOsVZIYB +2qAgw6XE0IF4a+PAtHSoYftwH2ocMY2gMuSNpQWm7m0+/j+K+RBoeUcnGNPQgszq +N60IDMqkqHjyubrm2aslfopWmPSvaQoyxwV/uztdo+UI0IV2z9gD7Sm49vMkpYp8 +=uMz0 +-----END PGP PUBLIC KEY BLOCK----- \ No newline at end of file diff --git a/.github/affirmation-trusted/github-web-flow.gpg b/.github/affirmation-trusted/github-web-flow.gpg new file mode 100644 index 0000000..dc77d7e --- /dev/null +++ b/.github/affirmation-trusted/github-web-flow.gpg @@ -0,0 +1,28 @@ +-----BEGIN PGP PUBLIC KEY BLOCK----- + +mQINBGWmxXYBEACyN+4viFQM6QQoKr0A2W0rGdMobTJwOZso2QPpewbyBsuL3rNW +5OmHrWwXAhPKNqUIyOzdq8MoSxoTTuqLksoahixEL/X2nyhOBxR9GkYz/oI9R3nY +cLRaFQoSJoVfOt61opkLUzbWAehpbgT8EKln8JsENq0+0nDlWQi0h2Q9oGmqlgVz +skwmVZ8Leyv4Mg7hN6swyZ7moZfkkpD5+U7Z2XVurCzkSSfg4zb2lMRLJos2eCAc +749ECsX0t7OBftF+YqgjIXixXsm2RrUqvU47OkOtZeAhvAYenbC3pr9Fha5NxoBU +Ea+11MK9W6OcRhwvxVCUrMUR6FTSZyC//VpXTTtrRlOqpU5wGMbP3zpn9geqOXCl +8rF7+1gAPG/o+QFQTBsVEruwi4JWogiQuQyOwAIlFe/7dvaxWZGpv/yW2+L3guL7 +xaHKFVGsayhlitQQ5Xa+P1iSgKSXDyReCbWotfqAempPySI25LHh3ScXI6NgdHSr +SBaFojwAfgxbPTEQ6adIsKHCQofrnLrNa3UOeGDGiOOK0aYV3jiEDGAouatkNf2q +85Eosj1f9laCqAH3YLJD7dcSne1iChK5qRTByMvIyeSD0NbNnVMFOGpXySyWtKb2 +ldpu8AWBQJsJs9FmYBcWAGBA2pp+IxaCn6rBIHIsUVFRN8OVZKsEsBkWywARAQAB +tBtHaXRIdWIgPG5vcmVwbHlAZ2l0aHViLmNvbT6JAk4EEwEKADgWIQSWhHmhr/kn +430aVmu1aQ7uu5UhlAUCZabFdgIbAwULCQgHAgYVCgkICwIEFgIDAQIeAQIXgAAK +CRC1aQ7uu5UhlIMuEAClvVwC+Neoiq0AdixJZsagKHpx1QrMJWrtMRi4eXVTTaeX ++P1unhC/AmSO4Xxd3uRoejHvfWh4F0gitUJ8XKgiejnmuGcq7Dbt5OoO1JuXGlW2 +BQ+MiGoYVw2B0sOhWDNrIBWOO/WL4LykcGnAtrRXwoS0Wx4MCydztXQY5lcnCWaW +8rvu7WmduoOikH4HI97rqN5896dc4iBKSx8LZf+46DRCCD/5SfACplBz4hs5zen8 +TL8zd+zxjFrXbzota0jSDEGK9WGO4z55S2xScC6zv6v3Bj1OR8Bs5aodGtmamHZ7 +sE9w0RJoCfNx+9cR/rE82SrOaBpVU7urLe4lg7zaaNhqDdNV8ymuXGmIJarDgrme +iB5bHS+dLFzLUkTgot4RFlPa9bFiJuJN6Tc9tMu5RJQ9l/zKmxDHIKWsAle5R65u +zEq04LugTQBdEorGxfQCsF2ga9ncKTDMiAThWTvZpOP3NJ/athZRmOBpG4B9iR6r +pRU8F/+MokG4fIMwnvtOhWQFiEzdTkJ7U5JAkPtTAmT3/mznwtPEU7DrFWSGAdqg +IMOlxNCBeGvjwLR0qGH7cB9qHDGNoDLkjaUFpu5tPv4/ivkQaHlHJxjT0ILM6jet +CAzKpKh48rm65tmrJX6KVpj0r2kKMscFf7s7XaPlCNCFds/YA+0puPbzJKWKfA== +=NRlX +-----END PGP PUBLIC KEY BLOCK----- diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index 989b319..3cfb57c 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -14,18 +14,26 @@ workflows: - 'actions/checkout@v7.0.1' '.github/workflows/estate-rules.yml': - 'actions/checkout@v7.0.1' + '.github/workflows/fork-governance-publish.yml': + - 'actions/download-artifact@v8.0.2' + '.github/workflows/fork-governance.yml': + - 'actions/upload-artifact@v7.0.2' '.github/workflows/governance.yml': [] '.github/workflows/hypatia-scan.yml': [] '.github/workflows/instant-sync.yml': + - 'step-security/harden-runner@46b06cea07f9e64621fdf066ba77ac6915163d43' - 'peter-evans/repository-dispatch@v4.0.1' '.github/workflows/label-triage.yml': [] '.github/workflows/labels.yml': [] '.github/workflows/main-estate-audit.yml': - 'actions/checkout@v7.0.1' - - 'hyperpolymath/cicd-suite@main' + - 'hyperpolymath/cicd-suite@bf7dd95cf49733019343ff485c2f45c6b261839c' '.github/workflows/mirror.yml': [] '.github/workflows/openssf-compliance.yml': - 'actions/checkout@v7.0.1' + '.github/workflows/patch-bridge.yml': + - 'actions/checkout@v7.0.1' + - 'actions/upload-artifact@v7.0.2' '.github/workflows/proofs.yml': - 'actions/checkout@v7.0.1' - 'leanprover/lean-action@v1.6.2' @@ -46,11 +54,6 @@ workflows: '.github/workflows/secret-scanner.yml': [] '.github/workflows/security-policy.yml': - 'actions/checkout@v7.0.1' - '.github/workflows/static-analysis-gate.yml': - - 'actions/checkout@v7.0.1' - - 'actions/download-artifact@v8.0.2' - - 'actions/upload-artifact@v7.0.2' - - 'erlef/setup-beam@v1.24.1' '.github/workflows/trope-check.yml': - 'actions/checkout@v7.0.1' '.github/workflows/wellknown-enforcement.yml': @@ -103,9 +106,9 @@ dependencies: commit: 'sha1-9b3254085494b55a0f7c4c2b3d2d52cc712ce370' owner_id: 9919 repo_id: 259445878 - 'hyperpolymath/cicd-suite@main': + 'hyperpolymath/cicd-suite@bf7dd95cf49733019343ff485c2f45c6b261839c': ref: 'main' - commit: 'sha1-5a10b72e574ef63855fafd4568a4c178657f3294' + commit: 'sha1-bf7dd95cf49733019343ff485c2f45c6b261839c' owner_id: 6759885 repo_id: 1326697643 uses: @@ -150,3 +153,8 @@ dependencies: commit: 'sha1-efb35369e0ad2afab669f228072c1b0d510eae64' owner_id: 2242 repo_id: 204253808 + 'step-security/harden-runner@46b06cea07f9e64621fdf066ba77ac6915163d43': + ref: 'v2.22.3' + commit: 'sha1-46b06cea07f9e64621fdf066ba77ac6915163d43' + owner_id: 88700172 + repo_id: 422287306 diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml index fff8bd0..6eab120 100644 --- a/.github/workflows/boj-build.yml +++ b/.github/workflows/boj-build.yml @@ -22,6 +22,8 @@ jobs: steps: - name: Checkout uses: actions/checkout@v7.0.1 + with: + persist-credentials: false - name: Trigger BoJ Server (Casket/ssg-mcp) env: BOJ_URL: ${{ secrets.BOJ_SERVER_URL || vars.BOJ_SERVER_URL }} diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index 38cd44b..4093d83 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -41,6 +41,10 @@ jobs: with: languages: ${{ matrix.language }} build-mode: ${{ matrix.build-mode }} + # Widest bundled suite (superset of security-extended), not the + # default: for the `actions` extractor this adds the workflow + # security/quality queries that the default set omits. + queries: security-and-quality - name: Perform CodeQL Analysis uses: github/codeql-action/analyze@v4.39.1 with: diff --git a/.github/workflows/dependabot-automerge.yml b/.github/workflows/dependabot-automerge.yml index 5d25b28..555b196 100644 --- a/.github/workflows/dependabot-automerge.yml +++ b/.github/workflows/dependabot-automerge.yml @@ -42,17 +42,32 @@ on: pull_request: types: [opened, reopened, synchronize] permissions: - contents: read # needed to enable auto-merge + contents: write # needed to enable auto-merge (read is NOT enough) pull-requests: write # needed to approve # NB: keep narrow — do NOT add secrets: read or id-token: write here. jobs: automerge: - # Only run for PRs actually authored by Dependabot. - if: github.actor == 'dependabot[bot]' && github.event.pull_request.user.login == 'dependabot[bot]' + # Only run for PRs actually authored by Dependabot. The gate is the PR + # AUTHOR (event payload, unspoofable); the old belt-and-braces actor half + # moved into the first step - gating a job on github.actor is attacker- + # controllable on fork triggers (hypatia), while an in-job abort is not + # a security boundary, just noise reduction for humans pushing fixups + # onto a bot-opened branch. + if: github.event.pull_request.user.login == 'dependabot[bot]' # zizmor: ignore[bot-conditions] runs-on: ubuntu-latest timeout-minutes: 15 steps: + - name: Skip human re-triggers (bot-authored PRs only proceed on bot pushes) + env: + ACTOR: ${{ github.actor }} + id: actor-check + run: | + proceed=false + if [ "$ACTOR" = "dependabot[bot]" ]; then proceed=true; + else echo "::notice::Triggered by ${ACTOR}, not dependabot[bot]; leaving this PR to the human flow."; fi + echo "proceed=$proceed" >> "$GITHUB_OUTPUT" - name: Fetch Dependabot metadata + if: steps.actor-check.outputs.proceed == 'true' id: meta uses: dependabot/fetch-metadata@v3.1.0 with: @@ -73,6 +88,7 @@ jobs: # Otherwise: do nothing. Human reviews HIGH+CRITICAL security # updates and all non-security bumps. - name: Decide policy outcome + if: steps.actor-check.outputs.proceed == 'true' id: policy env: GHSA_ID: ${{ steps.meta.outputs.ghsa-id }} @@ -102,25 +118,30 @@ jobs: else echo "action=skip" >> "$GITHUB_OUTPUT" fi - echo "security=$is_security" >> "$GITHUB_OUTPUT" - echo "update_type=$UPDATE_TYPE" >> "$GITHUB_OUTPUT" - echo "ghsa=$GHSA_ID" >> "$GITHUB_OUTPUT" + { + echo "security=$is_security" + echo "update_type=$UPDATE_TYPE" + echo "ghsa=$GHSA_ID" + } >> "$GITHUB_OUTPUT" - name: Approve PR (if policy allows) - if: steps.policy.outputs.action == 'automerge' + if: steps.actor-check.outputs.proceed == 'true' && steps.policy.outputs.action == 'automerge' env: GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} PR_URL: ${{ github.event.pull_request.html_url }} + STEPS_POLICY_OUTPUTS_GHSA: ${{ steps.policy.outputs.ghsa }} + STEPS_POLICY_OUTPUTS_UPDATE_TYPE: ${{ steps.policy.outputs.update_type }} run: | gh pr review --approve "$PR_URL" \ - --body "Auto-approving Dependabot security update (${{ steps.policy.outputs.ghsa }}, ${{ steps.policy.outputs.update_type }}). Policy: low/moderate security patches/minors only." + --body "Auto-approving Dependabot security update ($STEPS_POLICY_OUTPUTS_GHSA, $STEPS_POLICY_OUTPUTS_UPDATE_TYPE). Policy: low/moderate security patches/minors only." - name: Enable auto-merge (if policy allows) - if: steps.policy.outputs.action == 'automerge' + if: steps.actor-check.outputs.proceed == 'true' && steps.policy.outputs.action == 'automerge' env: GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} PR_URL: ${{ github.event.pull_request.html_url }} run: | gh pr merge --auto --squash "$PR_URL" - name: Write decision to step summary + if: steps.actor-check.outputs.proceed == 'true' env: ACTION: ${{ steps.policy.outputs.action }} IS_SECURITY: ${{ steps.policy.outputs.security }} diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml index 29ba4d8..79c32ae 100644 --- a/.github/workflows/dogfood-gate.yml +++ b/.github/workflows/dogfood-gate.yml @@ -6,7 +6,11 @@ # # dogfood-gate.yml — Hyperpolymath Dogfooding Quality Gate # Validates that the repo uses hyperpolymath's own formats and tools. -# Companion to static-analysis-gate.yml (security) — this is for format compliance. +# Format-compliance PREFLIGHT only: the DEED/K9 checks below are header-level +# and fast; the authoritative conformance lanes (canonical validators, grids, +# the PR comment) run in fork-governance.yml. If the two ever disagree on +# semantics, fork-governance governs; a header-level failure here still +# blocks, because malformed syntax is wrong under either reading. name: "🟡 Check: RSR self-use (dogfooding)" on: @@ -30,6 +34,8 @@ jobs: steps: - name: Checkout repository uses: actions/checkout@v7.0.1 + with: + persist-credentials: false - name: Check for the repo deed id: detect @@ -47,8 +53,10 @@ jobs: INPUT_STRICT: "true" run: bash .githooks/validate-a2ml.sh - name: Write summary + env: + STEPS_DETECT_OUTPUTS_COUNT: ${{ steps.detect.outputs.count }} run: | - DEED_COUNT="${{ steps.detect.outputs.count }}" + DEED_COUNT="$STEPS_DETECT_OUTPUTS_COUNT" if [ "$DEED_COUNT" -eq 0 ]; then cat <<'EOF' >> "$GITHUB_STEP_SUMMARY" ## Repo deed validation @@ -58,9 +66,12 @@ jobs: Copy one from [rsr-template-repo](https://github.com/hyperpolymath/rsr-template-repo). EOF else - echo "## Repo deed validation" >> "$GITHUB_STEP_SUMMARY" - echo "" >> "$GITHUB_STEP_SUMMARY" - echo "Scanned **${DEED_COUNT}** deed file(s). See step output for details." >> "$GITHUB_STEP_SUMMARY" + { + echo "## Repo deed validation (presence + header level)" + echo "" + echo "Scanned **${DEED_COUNT}** deed file(s). See step output for details." + echo "Canonical grammar conformance runs in the Fork governance workflow's DEED syntax lane (standards deed-conformance)." + } >> "$GITHUB_STEP_SUMMARY" fi # --------------------------------------------------------------------------- @@ -74,6 +85,8 @@ jobs: steps: - name: Checkout repository uses: actions/checkout@v7.0.1 + with: + persist-credentials: false - name: Check for K9 files id: detect @@ -82,8 +95,10 @@ jobs: CONFIG_COUNT=$(find . \( -name '*.toml' -o -name '*.yaml' -o -name '*.yml' -o -name '*.json' \) \ -not -path './.git/*' -not -path './node_modules/*' -not -path './.deno/*' \ -not -name 'package-lock.json' -not -name 'Cargo.lock' -not -name 'deno.lock' | wc -l) - echo "k9_count=$COUNT" >> "$GITHUB_OUTPUT" - echo "config_count=$CONFIG_COUNT" >> "$GITHUB_OUTPUT" + { + echo "k9_count=$COUNT" + echo "config_count=$CONFIG_COUNT" + } >> "$GITHUB_OUTPUT" if [ "$COUNT" -eq 0 ] && [ "$CONFIG_COUNT" -gt 0 ]; then echo "::warning::Found $CONFIG_COUNT config files but no K9 contracts. Run k9iser to generate contracts." fi @@ -92,9 +107,12 @@ jobs: if: steps.detect.outputs.k9_count > 0 run: bash .githooks/validate-k9.sh - name: Write summary + env: + STEPS_DETECT_OUTPUTS_K9_COUNT: ${{ steps.detect.outputs.k9_count }} + STEPS_DETECT_OUTPUTS_CONFIG_COUNT: ${{ steps.detect.outputs.config_count }} run: | - K9_COUNT="${{ steps.detect.outputs.k9_count }}" - CFG_COUNT="${{ steps.detect.outputs.config_count }}" + K9_COUNT="$STEPS_DETECT_OUTPUTS_K9_COUNT" + CFG_COUNT="$STEPS_DETECT_OUTPUTS_CONFIG_COUNT" if [ "$K9_COUNT" -eq 0 ]; then cat <<'EOF' >> "$GITHUB_STEP_SUMMARY" ## K9 Contract Validation @@ -104,9 +122,12 @@ jobs: Generate contracts with: `k9iser generate .` EOF else - echo "## K9 Contract Validation" >> "$GITHUB_STEP_SUMMARY" - echo "" >> "$GITHUB_STEP_SUMMARY" - echo "Validated **${K9_COUNT}** K9 contract(s) against **${CFG_COUNT}** config file(s)." >> "$GITHUB_STEP_SUMMARY" + { + echo "## K9 Contract Validation (header level)" + echo "" + echo "Header-checked **${K9_COUNT}** K9 contract(s); found **${CFG_COUNT}** config file(s)." + echo "Canonical L0–L2 conformance and the grid run in the Fork governance workflow's K9-DEED conformance lane (standards k9-conformance)." + } >> "$GITHUB_STEP_SUMMARY" fi # --------------------------------------------------------------------------- @@ -120,6 +141,8 @@ jobs: steps: - name: Checkout repository uses: actions/checkout@v7.0.1 + with: + persist-credentials: false - name: Scan for invisible characters id: lint @@ -144,34 +167,45 @@ jobs: set -e FINDINGS=$(wc -l < /tmp/empty-lint-results.txt 2>/dev/null || echo 0) - echo "findings=$FINDINGS" >> "$GITHUB_OUTPUT" - echo "exit_code=$EL_EXIT" >> "$GITHUB_OUTPUT" - echo "ready=true" >> "$GITHUB_OUTPUT" + { + echo "findings=$FINDINGS" + echo "exit_code=$EL_EXIT" + echo "ready=true" + } >> "$GITHUB_OUTPUT" # Emit annotations for each file with invisible chars while IFS= read -r filepath; do [ -z "$filepath" ] && continue - REL_PATH="${filepath#$GITHUB_WORKSPACE/}" + REL_PATH="${filepath#"$GITHUB_WORKSPACE"/}" echo "::warning file=${REL_PATH}::Invisible Unicode characters detected (zero-width space, BOM, NBSP, etc.)" done < /tmp/empty-lint-results.txt - name: Write summary + env: + STEPS_LINT_OUTPUTS_READY: ${{ steps.lint.outputs.ready }} + STEPS_LINT_OUTPUTS_FINDINGS: ${{ steps.lint.outputs.findings }} run: | - if [ "${{ steps.lint.outputs.ready }}" = "true" ]; then - FINDINGS="${{ steps.lint.outputs.findings }}" + if [ "$STEPS_LINT_OUTPUTS_READY" = "true" ]; then + FINDINGS="$STEPS_LINT_OUTPUTS_FINDINGS" if [ "$FINDINGS" -gt 0 ] 2>/dev/null; then - echo "## Empty-Linter Results" >> "$GITHUB_STEP_SUMMARY" - echo "" >> "$GITHUB_STEP_SUMMARY" - echo "Found **${FINDINGS}** invisible character issue(s). See annotations above." >> "$GITHUB_STEP_SUMMARY" + { + echo "## Empty-Linter Results" + echo "" + echo "Found **${FINDINGS}** invisible character issue(s). See annotations above." + } >> "$GITHUB_STEP_SUMMARY" else - echo "## Empty-Linter Results" >> "$GITHUB_STEP_SUMMARY" - echo "" >> "$GITHUB_STEP_SUMMARY" - echo ":white_check_mark: No invisible character issues found." >> "$GITHUB_STEP_SUMMARY" + { + echo "## Empty-Linter Results" + echo "" + echo ":white_check_mark: No invisible character issues found." + } >> "$GITHUB_STEP_SUMMARY" fi else - echo "## Empty-Linter" >> "$GITHUB_STEP_SUMMARY" - echo "" >> "$GITHUB_STEP_SUMMARY" - echo "Skipped: empty-linter not available." >> "$GITHUB_STEP_SUMMARY" + { + echo "## Empty-Linter" + echo "" + echo "Skipped: empty-linter not available." + } >> "$GITHUB_STEP_SUMMARY" fi # --------------------------------------------------------------------------- @@ -185,6 +219,8 @@ jobs: steps: - name: Checkout repository uses: actions/checkout@v7.0.1 + with: + persist-credentials: false - name: Check for Groove manifest id: groove @@ -215,23 +251,31 @@ jobs: HAS_SERVER="true" fi - echo "has_manifest=$HAS_MANIFEST" >> "$GITHUB_OUTPUT" - echo "has_groove_code=$HAS_GROOVE_CODE" >> "$GITHUB_OUTPUT" - echo "has_server=$HAS_SERVER" >> "$GITHUB_OUTPUT" + { + echo "has_manifest=$HAS_MANIFEST" + echo "has_groove_code=$HAS_GROOVE_CODE" + echo "has_server=$HAS_SERVER" + } >> "$GITHUB_OUTPUT" if [ "$HAS_SERVER" = "true" ] && [ "$HAS_MANIFEST" = "false" ] && [ "$HAS_GROOVE_CODE" = "false" ]; then echo "::warning::This repo has server code but no Groove endpoint. Add .well-known/groove/manifest.json for service discovery." fi - name: Write summary + env: + STEPS_GROOVE_OUTPUTS_HAS_MANIFEST: ${{ steps.groove.outputs.has_manifest }} + STEPS_GROOVE_OUTPUTS_HAS_GROOVE_CODE: ${{ steps.groove.outputs.has_groove_code }} + STEPS_GROOVE_OUTPUTS_HAS_SERVER: ${{ steps.groove.outputs.has_server }} run: | - echo "## Groove Protocol Check" >> "$GITHUB_STEP_SUMMARY" - echo "" >> "$GITHUB_STEP_SUMMARY" - echo "| Check | Status |" >> "$GITHUB_STEP_SUMMARY" - echo "|-------|--------|" >> "$GITHUB_STEP_SUMMARY" - echo "| Static manifest (.well-known/groove/manifest.json) | ${{ steps.groove.outputs.has_manifest }} |" >> "$GITHUB_STEP_SUMMARY" - echo "| Groove endpoint in code | ${{ steps.groove.outputs.has_groove_code }} |" >> "$GITHUB_STEP_SUMMARY" - echo "| Has HTTP server code | ${{ steps.groove.outputs.has_server }} |" >> "$GITHUB_STEP_SUMMARY" + { + echo "## Groove Protocol Check" + echo "" + echo "| Check | Status |" + echo "|-------|--------|" + echo "| Static manifest (.well-known/groove/manifest.json) | $STEPS_GROOVE_OUTPUTS_HAS_MANIFEST |" + echo "| Groove endpoint in code | $STEPS_GROOVE_OUTPUTS_HAS_GROOVE_CODE |" + echo "| Has HTTP server code | $STEPS_GROOVE_OUTPUTS_HAS_SERVER |" + } >> "$GITHUB_STEP_SUMMARY" # --------------------------------------------------------------------------- # Job 5: eclexiaiser manifest validation @@ -244,6 +288,8 @@ jobs: steps: - name: Checkout repository uses: actions/checkout@v7.0.1 + with: + persist-credentials: false - name: Check and validate eclexiaiser manifest id: eclex @@ -271,15 +317,21 @@ jobs: if [ "$ok" = 1 ]; then echo "Valid: eclexiaiser.toml (${nfun:-0} function(s))"; else echo "::error file=eclexiaiser.toml::Invalid eclexiaiser.toml"; exit 1; fi - name: Write summary + env: + STEPS_ECLEX_OUTPUTS_HAS_MANIFEST: ${{ steps.eclex.outputs.has_manifest }} run: | - if [ "${{ steps.eclex.outputs.has_manifest }}" = "true" ]; then - echo "## Eclexiaiser Manifest" >> "$GITHUB_STEP_SUMMARY" - echo "" >> "$GITHUB_STEP_SUMMARY" - echo ":white_check_mark: **eclexiaiser.toml** present and valid." >> "$GITHUB_STEP_SUMMARY" + if [ "$STEPS_ECLEX_OUTPUTS_HAS_MANIFEST" = "true" ]; then + { + echo "## Eclexiaiser Manifest" + echo "" + echo ":white_check_mark: **eclexiaiser.toml** present and valid." + } >> "$GITHUB_STEP_SUMMARY" else - echo "## Eclexiaiser Manifest" >> "$GITHUB_STEP_SUMMARY" - echo "" >> "$GITHUB_STEP_SUMMARY" - echo ":ballot_box_with_check: No eclexiaiser.toml. Add one with \`eclexiaiser init\` for energy/carbon tracking." >> "$GITHUB_STEP_SUMMARY" + { + echo "## Eclexiaiser Manifest" + echo "" + echo ":ballot_box_with_check: No eclexiaiser.toml. Add one with \`eclexiaiser init\` for energy/carbon tracking." + } >> "$GITHUB_STEP_SUMMARY" fi # --------------------------------------------------------------------------- @@ -295,6 +347,8 @@ jobs: steps: - name: Checkout repository uses: actions/checkout@v7.0.1 + with: + persist-credentials: false - name: Generate dogfooding scorecard run: | @@ -356,7 +410,7 @@ jobs: | Tool/Format | Status | Notes | |-------------|--------|-------| - | DEED repo deed (`_chora.deed`) | ${DEED_STATUS} | Required for all RSR repos | + | DEED repo deed (\`_chora.deed\`) | ${DEED_STATUS} | Required for all RSR repos | | K9 contracts | ${K9_STATUS} | Required for repos with config files | | .editorconfig | ${EC_STATUS} | Required for all repos | | Groove endpoint | ${GROOVE_STATUS} | Required for service repos | diff --git a/.github/workflows/estate-rules.yml b/.github/workflows/estate-rules.yml index 8527264..b5444d2 100644 --- a/.github/workflows/estate-rules.yml +++ b/.github/workflows/estate-rules.yml @@ -26,6 +26,8 @@ jobs: steps: - name: Checkout uses: actions/checkout@v7.0.1 + with: + persist-credentials: false - name: Root shape allowlist run: bash scripts/check-root-shape.sh . - name: AsciiDoc by default (no .md under docs/) diff --git a/.github/workflows/fork-governance-publish.yml b/.github/workflows/fork-governance-publish.yml new file mode 100644 index 0000000..3f0a2f6 --- /dev/null +++ b/.github/workflows/fork-governance-publish.yml @@ -0,0 +1,228 @@ +# SPDX-License-Identifier: MPL-2.0 +# Only trusted default-branch code publishes the untrusted PR scan's evidence. +# Never check out the PR or execute anything downloaded from its run. +# +# Trust model: a fork PR controls the PR-side Fork governance workflow, so +# its artifacts can lie. Publication requires the PR head and base copies of +# the scan workflow to match the default branch's trusted copy byte-for-byte. +# Lane pass/fail is derived from GitHub's own run metadata (job conclusions), +# and the run must have actually called the pinned reusable workflows named by the DEFAULT branch's +# fork-governance.yml (referenced_workflows), and the artifact's lane +# claims must agree or publication is refused. What remains +# artifact-sourced is display shading only (K9/Hypatia verdict colors, +# advisory counts, grid Markdown) — produced by the real reusables the +# run is proven to have called. A PR that bumps the reusable pins gets no +# comment until it merges (the trusted pin set is the default branch's); +# that fail-closed gap is deliberate. +name: Publish fork governance + +on: + # Source identity/current head are checked below; artifacts are data only. + workflow_run: # zizmor: ignore[dangerous-triggers] + workflows: [Fork governance] + types: [completed] + +permissions: {} + +concurrency: + # Keyed on fork identity + head SHA, not the (fork-controlled, and + # colliding across forks) branch name: two forks with a `main` branch + # must not cancel each other's publisher. The publish step also + # re-checks the PR head against this SHA before posting, so a stale + # publisher for an older SHA fails closed instead of racing. + group: fork-governance-publish-${{ github.event.workflow_run.head_repository.full_name }}-${{ github.event.workflow_run.head_sha }} + cancel-in-progress: true + +jobs: + publish: + if: github.event.workflow_run.event == 'pull_request' + runs-on: ubuntu-latest + timeout-minutes: 5 + permissions: + contents: read + actions: read + pull-requests: write + steps: + - name: Verify the source run and current pull request + id: source + env: + GH_TOKEN: ${{ github.token }} + run: | + set -euo pipefail + run_id=$(jq -r '.workflow_run.id' "$GITHUB_EVENT_PATH") + gh api "repos/$GITHUB_REPOSITORY/actions/runs/$run_id" > "$RUNNER_TEMP/source-run.json" + workflow_id=$(gh api "repos/$GITHUB_REPOSITORY/actions/workflows/fork-governance.yml" --jq .id) + jq -e --argjson workflow "$workflow_id" --slurpfile event "$GITHUB_EVENT_PATH" ' + .workflow_id == $workflow and .event == "pull_request" and .status == "completed" + and .repository.full_name == $event[0].repository.full_name + and .head_sha == $event[0].workflow_run.head_sha + and .run_attempt == $event[0].workflow_run.run_attempt + ' "$RUNNER_TEMP/source-run.json" >/dev/null + sha=$(jq -r '.head_sha' "$RUNNER_TEMP/source-run.json") + # workflow_run.pull_requests can be empty for forks. Resolve the + # association through GitHub, never through a PR-supplied artifact. + gh api --paginate --slurp "repos/$GITHUB_REPOSITORY/commits/$sha/pulls" \ + > "$RUNNER_TEMP/source-prs.json" + pr=$(jq -r --arg sha "$sha" --arg repo "$GITHUB_REPOSITORY" ' + [.[][] | select(.state == "open" and .head.sha == $sha and .base.repo.full_name == $repo)] + | if length == 1 then .[0].number else empty end + ' "$RUNNER_TEMP/source-prs.json") + [ -n "$pr" ] || { echo "No unique current open PR for this run; skipping publication."; exit 0; } + echo "pr=$pr" >> "$GITHUB_OUTPUT" + echo "run=$run_id" >> "$GITHUB_OUTPUT" + # Authenticate the run itself (see trust model above): it must + # have called exactly the reusable workflows the default branch's + # fork-governance.yml names, at the same pins — a PR-edited + # workflow that fakes or swaps a lane does not satisfy this. + gh api "repos/$GITHUB_REPOSITORY/contents/.github/workflows/fork-governance.yml" \ + --jq .content | base64 -d > "$RUNNER_TEMP/trusted-fork-governance.yml" + # A malicious PR can call the pinned reusables AND forge lookalike + # jobs/artifacts. Require the actual PR head and base workflow files + # to match the trusted default, not merely the list of reusables. + gh api "repos/$GITHUB_REPOSITORY/pulls/$pr" > "$RUNNER_TEMP/current-pr.json" + jq -e --arg sha "$sha" '.state == "open" and .head.sha == $sha' \ + "$RUNNER_TEMP/current-pr.json" >/dev/null + head_repo=$(jq -r '.head.repo.full_name' "$RUNNER_TEMP/current-pr.json") + base_sha=$(jq -r '.base.sha' "$RUNNER_TEMP/current-pr.json") + gh api "repos/$head_repo/contents/.github/workflows/fork-governance.yml?ref=$sha" \ + --jq .content | base64 -d > "$RUNNER_TEMP/head-fork-governance.yml" + gh api "repos/$GITHUB_REPOSITORY/contents/.github/workflows/fork-governance.yml?ref=$base_sha" \ + --jq .content | base64 -d > "$RUNNER_TEMP/base-fork-governance.yml" + if ! cmp -s "$RUNNER_TEMP/trusted-fork-governance.yml" "$RUNNER_TEMP/head-fork-governance.yml" || + ! cmp -s "$RUNNER_TEMP/trusted-fork-governance.yml" "$RUNNER_TEMP/base-fork-governance.yml"; then + echo "::error::PR scan workflow differs from the trusted default; refusing to publish." + exit 1 + fi + grep -oE 'uses: [^[:space:]#]+' "$RUNNER_TEMP/trusted-fork-governance.yml" \ + | awk '{print $2}' | grep '/\.github/workflows/' | sort -u \ + > "$RUNNER_TEMP/expected-reusables.txt" + jq -r '.referenced_workflows[]?.path' "$RUNNER_TEMP/source-run.json" | sort -u \ + > "$RUNNER_TEMP/actual-reusables.txt" + if [ ! -s "$RUNNER_TEMP/expected-reusables.txt" ]; then + echo "::error::Could not read the trusted reusable set from the default branch; refusing to publish." >&2 + exit 1 + fi + missing=$(comm -23 "$RUNNER_TEMP/expected-reusables.txt" "$RUNNER_TEMP/actual-reusables.txt") + if [ -n "$missing" ]; then + echo "::error::Source run did not call the trusted reusables; refusing to publish. Missing:" >&2 + echo "$missing" >&2 + exit 1 + fi + # Lane pass/fail comes from GitHub's job conclusions for the run, + # never from the artifact. Job names are the reusables' own. + gh api --paginate --slurp "repos/$GITHUB_REPOSITORY/actions/runs/$run_id/jobs?per_page=100" \ + > "$RUNNER_TEMP/source-jobs.json" + jq -e ' + [.[].jobs[]] as $jobs + | def lane($name): + [$jobs[] | select(.name == $name)] + | if length == 1 then .[0].conclusion + else error("lane job missing or ambiguous: \($name)") end; + { + deed: lane("DEED syntax / lint"), + k9: lane("K9-DEED conformance / validate"), + hypatia: lane("Hypatia verdict grid / Hypatia Neurosymbolic Analysis") + } + | if all(.[]; . == "success" or . == "failure" or . == "cancelled" or . == "skipped") + then . else error("unexpected lane conclusion") end + ' "$RUNNER_TEMP/source-jobs.json" > "$RUNNER_TEMP/lanes.json" + + - name: Download lane results from the verified run + if: steps.source.outputs.pr != '' + uses: actions/download-artifact@v8.0.2 + with: + name: fork-governance-result + path: evidence + github-token: ${{ github.token }} + run-id: ${{ github.event.workflow_run.id }} + + - name: Validate lane result data + if: steps.source.outputs.pr != '' + run: | + set -euo pipefail + jq -e --slurpfile run "$RUNNER_TEMP/source-run.json" ' + def result: . == "success" or . == "failure" or . == "cancelled" or . == "skipped"; + def verdict: . == "" or . == "green" or . == "yellow" or . == "orange" + or . == "red" or . == "purple" or . == "blue" or . == "grey"; + .sha == $run[0].head_sha and .run == ($run[0].id | tostring) + and .attempt == ($run[0].run_attempt | tostring) + and (.lanes.deed.result | result) + and (.lanes.k9.result | result) and (.lanes.hypatia.result | result) + and ((.lanes.k9.outputs.verdict // "") | verdict) + and ((.lanes.hypatia.outputs.verdict // "") | verdict) + and ((.lanes.hypatia.outputs.advisory // "") + | test("^(|none|(green|yellow|orange|red|purple|blue|grey):[0-9]+:[0-9]+)$")) + ' evidence/result.json >/dev/null + # The artifact's lane claims must agree with GitHub's own job + # conclusions, or the PR-side workflow is lying: refuse to publish. + jq -e --slurpfile lanes "$RUNNER_TEMP/lanes.json" ' + .lanes.deed.result == $lanes[0].deed + and .lanes.k9.result == $lanes[0].k9 + and .lanes.hypatia.result == $lanes[0].hypatia + ' evidence/result.json >/dev/null + + - name: Download the K9 grid from the verified run + if: steps.source.outputs.pr != '' + continue-on-error: true + uses: actions/download-artifact@v8.0.2 + with: + name: k9-grid + path: k9-grid + github-token: ${{ github.token }} + run-id: ${{ github.event.workflow_run.id }} + + - name: Download the Hypatia grid from the verified run + if: steps.source.outputs.pr != '' + continue-on-error: true + uses: actions/download-artifact@v8.0.2 + with: + name: verdict-grid + path: verdict-grid + github-token: ${{ github.token }} + run-id: ${{ github.event.workflow_run.id }} + + - name: Fetch the pinned trusted renderer + if: steps.source.outputs.pr != '' + env: + GH_TOKEN: ${{ github.token }} + run: | + set -euo pipefail + gh api 'repos/metadatastician/standards/contents/scripts/fork-governance-render.sh?ref=34cf03f988b8ca95b91b45d9b3351f7d3babfb65' \ + --jq .content | base64 -d > "$RUNNER_TEMP/trusted-renderer.sh" + + - name: Render and publish the verified run's summary + if: steps.source.outputs.pr != '' + env: + GH_TOKEN: ${{ github.token }} + PR_NUMBER: ${{ steps.source.outputs.pr }} + run: | + set -euo pipefail + sha=$(jq -r '.sha' evidence/result.json) + # Check again after artifact downloads so a superseded PR head + # does not receive an obsolete verdict. + gh api "repos/$GITHUB_REPOSITORY/pulls/$PR_NUMBER" \ + | jq -e --arg sha "$sha" '.state == "open" and .head.sha == $sha' >/dev/null + args=(--out "$RUNNER_TEMP/fork-governance" + --deed-result "$(jq -r '.deed' "$RUNNER_TEMP/lanes.json")" + --k9-result "$(jq -r '.k9' "$RUNNER_TEMP/lanes.json")" + --k9-verdict "$(jq -r '.lanes.k9.outputs.verdict // ""' evidence/result.json)" + --hypatia-result "$(jq -r '.hypatia' "$RUNNER_TEMP/lanes.json")" + --hypatia-verdict "$(jq -r '.lanes.hypatia.outputs.verdict // ""' evidence/result.json)" + --hypatia-advisory "$(jq -r '.lanes.hypatia.outputs.advisory // ""' evidence/result.json)" + --sha "$sha" --run "$(jq -r '.run' evidence/result.json)" --repo "$GITHUB_REPOSITORY") + [ ! -s k9-grid/report.md ] || args+=(--k9-report k9-grid/report.md) + [ ! -s verdict-grid/report.md ] || args+=(--hypatia-report verdict-grid/report.md) + bash "$RUNNER_TEMP/trusted-renderer.sh" "${args[@]}" >/dev/null + cat "$RUNNER_TEMP/fork-governance/body.md" >> "$GITHUB_STEP_SUMMARY" + comment_id=$(gh api --paginate --slurp "repos/$GITHUB_REPOSITORY/issues/$PR_NUMBER/comments" \ + | jq -r '[.[][] | select(.user.login == "github-actions[bot]" + and ((.body // "") | contains(" + +# trope-checker wiki + +The trope-particularity checker: a portable IR + checker for the honest/deceptive +**trope grade**, backed by machine-checked proofs across Idris2, Lean 4 + Mathlib, and +Agda. + +## Verification streams + +- **Verified core** (Idris2) — `verification/proofs/idris2/`: the grade algebra reused by + the executable checker; the thing that runs is the thing that is proved. +- **Grade-algebra ground truth** (Lean 4 + Mathlib) — `verification/proofs/lean4/grade-boundary/`: + the ratified commutative `GradeR` monoid (the historical carrier is non-commutative), + full-carrier conicality, and the three-tier strict honest/deceptive cancellation + boundary. Sorry-free; axioms `propext`/`Classical.choice`/`Quot.sound` only. +- **Tropical factorisation probe** (Lean 4 + Mathlib) — `verification/proofs/lean4/grade-factorisation/`: + see [Tropical Factorisation Probe](Tropical-Factorisation-Probe.md). Ratified-carrier verdict + *(B′) FACTORS AND VERIDICALITY-SIGHTED*; historical (B) applies to the + pre-ratification carrier. A precondition only. +- **Calculus metatheory — Theorem B** (Agda `--safe --without-K`) — `verification/proofs/agda/theorem-b/`: + intrinsic graded calculus, value substitution, β/let subject reduction, Honest + Generation. Zero postulates. (`fix`/lfp open — CO-1.) + +## The central open problem + +**CO-1** — an operational model for `fix`/routing dynamics has been designed, but +not yet mechanised; full subject reduction remains open (issue #10). **O4**, the +limit-carrier question (issue #12), is resolved under the ratified carrier repair +and no longer gates CO-1. See `spec/notes/2026-07-07-co1-operational-model.adoc` +and `spec/notes/2026-07-07-l4-boundary-and-atoms.adoc` §4. + +## Gates + +```sh +just verify-all # both Lean developments + Theorem B (Agda) + honesty gate +just build-lean # grade-boundary + grade-factorisation + axiom audits +just build-agda # Theorem B (--safe --without-K) +``` + +## Honesty + +Status is ground-truthed by running the tools, not by reading prose. See +`AFFIRMATION.adoc` (dated snapshot), `AUDIT.adoc` (release gate), and +`docs/status/PROOF-NEEDS.adoc` (the proof ledger). diff --git a/wiki/README.md b/wiki/README.md new file mode 100644 index 0000000..1b278f3 --- /dev/null +++ b/wiki/README.md @@ -0,0 +1,27 @@ + + +# Wiki source (mirrored in-repo) + +These `.md` pages are the source for the project's GitHub wiki, kept in-repo so they +are versioned, reviewed, and never lost. + +**Note:** The GitHub wiki is **enabled** (`has_wiki: true`) but was **never initialised**, so the +`*.wiki.git` remote does not yet exist and cannot be pushed to. This is a one-time +manual bootstrap: + +1. In the GitHub UI, open **Wiki** and **Create the first page** (any content — it can be + empty; it just initialises the wiki git repo). +2. Then publish these pages: + +```sh +git clone git@github.com:hyperpolymath/trope-checker.wiki.git /tmp/tc-wiki +cp wiki/Home.md wiki/Tropical-Factorisation-Probe.md /tmp/tc-wiki/ +( cd /tmp/tc-wiki && git add -A && git commit -m "wiki: Home + Tropical Factorisation Probe" && git push ) +``` + +Page ↔ file mapping (GitHub wiki uses the file basename as the page title): + +| Page | Purpose | +| --- | --- | +| `Home.md` | Wiki landing page — verification streams, gates, honesty pointers. | +| `Tropical-Factorisation-Probe.md` | The probe write-up — verdict (B), proved theorems, the necessary-not-sufficient guard. | diff --git a/wiki/Tropical-Factorisation-Probe.md b/wiki/Tropical-Factorisation-Probe.md new file mode 100644 index 0000000..27de9b6 --- /dev/null +++ b/wiki/Tropical-Factorisation-Probe.md @@ -0,0 +1,75 @@ + + +# Tropical Factorisation Probe + +A dynamics-free, purely algebraic probe: *does the trope grade admit a homomorphic +projection onto a commutative tropical cost, with all non-commutativity confined to the +complement?* Source: `verification/proofs/lean4/grade-factorisation/`; full write-up: +`verification/proofs/lean4/grade-factorisation/REPORT.adoc`. + +## Verdict — (B′) FACTORS AND VERIDICALITY-SIGHTED (ratified carrier) + +Under the ratified carrier (R-2026-07-07, ADR 0004 A1/A2), a nontrivial, surjective +monoid homomorphism `πR : (GradeR, ▷, ε) → (Δ, +, Q 0)` exists (`piR_hom`, `piR_one`, +`piRHom`, `piR_nontrivial`, `piR_surjective`). It distinguishes honest `Dropped` +from deceptive `Falsified`: `∞` (`total`) versus `⊤` (`unknown`), proved by +`phiR_sighted` and `piR_sighted` in `GradeFactorisationR.lean`. + +This sightedness has a trade-off: attenuation payload `⊤` is squashed to `∞`, so +`Atten ∞` and `Atten ⊤` share a cost (`sighted_forces_squash`). `Predicated` and +`Dropped` also share the honest total-loss cost (`phiR_collapses_predicated_dropped`). +See the report's “Re-run under the ratified carrier” section for the full result. + +## Historical verdict — (B) FACTORS but VERIDICALITY-BLIND (pre-ratification) + +The following result applies only to the pre-ratification carrier, whose fate +composition has `Dropped ▷ Falsified = Dropped` and `Falsified ▷ Dropped = Falsified`. +The ratified carrier instead has `Dropped ▷ Falsified = Falsified`; the forced-collapse +claim below does not apply to it. + +A **nontrivial** monoid homomorphism `π : (Grade, ▷, ε) → (Δ, +, Q 0)` onto the +commutative tropical fidelity carrier `Δ = WithTop (WithTop ℕ)` **exists** — but **every** +multiplicative map from `Fate` (and from `Grade`) into **any** commutative monoid is +**forced** to identify the honest `dropped` with the deceptive `falsified`. So the best +case (A, veridicality-preserving) is **impossible**, and the dead case (C, no +homomorphism) is **false**. + +The blindness is **co-located** with the non-commutativity: it is the **fate-axis** +honest/deceptive distinction that collapses of necessity, because that coordinate has two +disagreeing absorbing heads. The **commutative** `Bond`/`Merge` coordinates carry no such +obstruction — their deceptions stay tropically separable. + +## Historical proofs (Lean 4 + Mathlib; sorry-free; `propext`/`Quot.sound` only) + +| Theorem | Statement | +| --- | --- | +| `pi_hom`, `pi_one`, `piHom` | `π` is a monoid homomorphism `Grade →* Multiplicative Δ`. | +| `pi_nontrivial`, `pi_surjective` | `π` separates attenuation levels and is onto `Δ` (not the trivial collapse). | +| `phiV_not_hom`, `piV_not_hom` | The veridicality-faithful candidate is **not** a homomorphism — breaker at `dropped ▷ falsified` (`total ≠ total + unknown = unknown`). | +| `forced_collapse_general`, `forced_collapse_grade` | **(axiom-free)** every multiplicative map into any commutative monoid identifies `dropped`/`falsified`. | +| `no_veridicality_faithful_hom` | Outcome (A) is impossible. | +| `psiBond_hom`, `psiBond_separates_honest_deceptive` | Bond deception **is** tropically separable — the loss is fate-specific. | +| `pi_blind_to_noncomm`, `grade_F2_noncomm`, `pi_collapses_F2` | `π` is blind to all non-commutativity; F2 confined to the complement. | + +## Necessary-not-sufficient (read this) + +A positive result means **only** "the commutative cost-quotient EXISTS — the tropical +route is NOT EXCLUDED, precondition met." It does **not** mean "tropical solves recursion." +Whether a fixpoint's grade actually lives in the commutative part needs an operational +model (**CO-1**, issue #10, gated by **O4**, issue #12) and stays parked. This probe can only +kill the tropical route or fail to kill it; it cannot confirm it. The fixpoint is **not** +solved, handled, or addressed by this work. + +## Reproduce + +```sh +cd verification/proofs/lean4/grade-factorisation +just build # green; imports grade-boundary, reuses the pinned Mathlib build +just falsify # sorry-free, axiom-clean; both falsifier witnesses live +just verdict # names the load-bearing theorems +``` + +## Next stage + +Issue #10 (CO-1 — operational model for `fix`/lfp), itself gated by issue #12 (O4 — the +limit carrier).