Skip to content

docs(proofs): PROOF-STATUS under the estate proof policy; ci: inline secret scanner #59

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 3 commits into from
Nov 9, 2026
Merged

docs(proofs): PROOF-STATUS under the estate proof policy; ci: inline secret scanner #59

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7d4b929
docs(proofs): PROOF-STATUS under the estate proof policy; Agda port next
hyperpolymath Nov 9, 2026
6db6c0a
ci(secret-scan): run the three scanners inline, from the RSR template
hyperpolymath Nov 9, 2026
a990ed9
docs(proofs): answer #59 review against PROOF-POLICY §8.2–§8.4 (not a…
claude Nov 9, 2026
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
2 changes: 2 additions & 0 deletions .github/workflows/actions.lock
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@ workflows:
- 'actions/checkout@v7.0.1'
- 'actions/deploy-pages@v5.0.1'
- 'actions/upload-pages-artifact@v5.0.0'
'.github/workflows/secret-scanner.yml':
- 'actions/checkout@v7.0.1'
dependencies:
'actions/cache@caa296126883cff596d87d8935842f9db880ef25':
ref: 'v5.1.0'
Expand Down
321 changes: 310 additions & 11 deletions .github/workflows/secret-scanner.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,19 +1,12 @@
# This workflow is managed by gh actions-lock.
# SPDX-License-Identifier: MPL-2.0
# Prevention workflow - scans for hardcoded secrets before they reach main.
#
# Calls the estate's shared secret scanner (gitleaks + rust-secrets +
# shell-secrets). The job key MUST stay `scan`: the estate-wide
# Secret-Scan-Floor ruleset requires the check context `scan / gitleaks`.
#
# No `secrets:` line, deliberately: the reusable references no secrets
# (gitleaks runs as a checksum-verified binary, not gitleaks-action), so
# `secrets: inherit` would only hand it every repo and org secret (CWE-250).
name: Secret Scanner

on:
pull_request:
push:
branches: [main]
workflow_dispatch:

concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
Expand All @@ -22,6 +15,312 @@ concurrency:
permissions:
contents: read

# The estate secret-scanning contract, run inline. Ported unchanged (job
# bodies) from hyperpolymath/rsr-template-repo `2be7b88`, its #295 "run all
# three secret scanners inline". The baseline is pinned to
# metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6.
#
# Why inline. The previous caller here was one job-level call to a remote
# reusable (`hyperpolymath/standards/.github/workflows/secret-scanner-
# reusable.yml@74d2f66`). It failed at startup, with zero jobs, on every run
# since it was added in #33. The template measured the same class: a remote
# reusable is not lockable by `gh actions-lock`, and check names that a
# remote repository can rename are not a contract. Here each scanner is an
# ordinary job whose `name:` is its check context:
#
# scan / gitleaks estate baseline (+ .gitleaks.toml if present):
# working tree, full history, AsciiDoc mirror
# scan / rust-secrets hardcoded literals in .rs files; self-skips
# without a Cargo.toml (marches has none)
# scan / shell-secrets hardcoded literals in shell scripts
#
# All three declare `permissions: contents: read` and no `secrets:`; none
# needs any secret (CWE-250 if one were forwarded).
#
# actions.lock: the only action is actions/checkout, pinned by the tag
# marches' lock already resolves (v7.0.1 → commit 3d3c42e…), the same commit
# the template pins by SHA. No marches ruleset requires these checks today.

jobs:
scan:
uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@74d2f66f575246cf6e313ae7775f44df6e097ff2
gitleaks:
name: "scan / gitleaks"
runs-on: ubuntu-24.04
timeout-minutes: 15
permissions:
contents: read
env:
GITLEAKS_VERSION: '8.18.4'
GITLEAKS_SHA256: 'ba6dbb656933921c775ee5a2d1c13a91046e7952e9d919f9bac4cec61d628e7d'
STANDARDS_SHA: 'e064539116c2dcfdf282a4749dbd58c69961c7e6'
steps:
- name: Checkout repository with full history
uses: actions/checkout@v7.0.1
with:
fetch-depth: 0
persist-credentials: false

- name: Checkout estate gitleaks baseline
uses: actions/checkout@v7.0.1
with:
repository: metadatastician/standards
ref: e064539116c2dcfdf282a4749dbd58c69961c7e6
path: .standards-baseline
sparse-checkout: config/gitleaks
sparse-checkout-cone-mode: true
persist-credentials: false

- name: Stage estate baseline and install pinned gitleaks
run: |
set -euo pipefail
cp .standards-baseline/config/gitleaks/estate-baseline.toml .gitleaks-estate.toml
rm -rf .standards-baseline
test -s .gitleaks-estate.toml

TARBALL="gitleaks_${GITLEAKS_VERSION}_linux_x64.tar.gz"
URL="https://github.com/gitleaks/gitleaks/releases/download/v${GITLEAKS_VERSION}/${TARBALL}"
curl -sSfL --proto '=https' --proto-redir '=https' --tlsv1.2 \
--retry 3 --retry-delay 2 \
-o "$RUNNER_TEMP/$TARBALL" "$URL"
echo "${GITLEAKS_SHA256} ${RUNNER_TEMP}/${TARBALL}" | sha256sum -c -
tar -xzf "$RUNNER_TEMP/$TARBALL" -C "$RUNNER_TEMP" gitleaks
chmod +x "$RUNNER_TEMP/gitleaks"
rm -f "$RUNNER_TEMP/$TARBALL"

- name: Gitleaks working-tree pass
run: |
set -euo pipefail
# The estate baseline always runs; a repository .gitleaks.toml adds a
# second pass and can never stand in for the baseline.
CONFIGS=(".gitleaks-estate.toml")
if [ -f .gitleaks.toml ]; then
CONFIGS+=(".gitleaks.toml")
fi
for CONFIG in "${CONFIGS[@]}"; do
"$RUNNER_TEMP/gitleaks" detect \
--source . \
--no-git \
--redact \
--no-banner \
--verbose \
--config "$CONFIG" \
--exit-code 1
done

- name: Gitleaks full-history pass
run: |
set -euo pipefail
if [ "$(git rev-parse --is-shallow-repository)" != "false" ]; then
echo "::error::checkout is shallow; refusing vacuous history scan"
exit 1
fi
# The estate baseline always runs; a repository .gitleaks.toml adds a
# second pass and can never stand in for the baseline.
CONFIGS=(".gitleaks-estate.toml")
if [ -f .gitleaks.toml ]; then
CONFIGS+=(".gitleaks.toml")
fi
for CONFIG in "${CONFIGS[@]}"; do
"$RUNNER_TEMP/gitleaks" detect \
--source . \
--redact \
--no-banner \
--verbose \
--config "$CONFIG" \
--exit-code 1
done

- name: Gitleaks AsciiDoc mirror pass
run: |
set -euo pipefail
MIRROR="$RUNNER_TEMP/adoc-mirror"
rm -rf "$MIRROR"
mkdir -p "$MIRROR"
found=0
while IFS= read -r -d '' f; do
dest="$MIRROR/$(dirname "$f")"
mkdir -p "$dest"
cp "$f" "$dest/$(basename "$f").txt"
found=$((found + 1))
done < <(find . -path ./.git -prune -o \( -name '*.adoc' -o -name '*.asciidoc' \) -type f -print0)

if [ "$found" -eq 0 ]; then
echo "No AsciiDoc files present."
exit 0
fi
# The estate baseline always runs; a repository .gitleaks.toml adds a
# second pass and can never stand in for the baseline.
CONFIGS=("$PWD/.gitleaks-estate.toml")
if [ -f .gitleaks.toml ]; then
CONFIGS+=("$PWD/.gitleaks.toml")
fi
for CONFIG in "${CONFIGS[@]}"; do
"$RUNNER_TEMP/gitleaks" detect \
--source "$MIRROR" \
--no-git \
--redact \
--no-banner \
--config "$CONFIG" \
--exit-code 1
done

rust-secrets:
name: "scan / rust-secrets"
runs-on: ubuntu-24.04
timeout-minutes: 10
permissions:
contents: read
env:
# Findings outside ./src (newly visible — see the scan-scope note in the
# step below) warn until this date, then block. Same warn-then-enforce
# idiom and same cutoff as the estate canonical reusable
# (metadatastician/standards .github/workflows/secret-scanner-reusable.yml
# at the pin named in this file's header), so this job and the reusable
# cannot disagree about when the widened scan starts blocking.
ENFORCE_RUST_WIDE_SCAN_FROM: '2026-08-21'
steps:
- name: Checkout repository
uses: actions/checkout@v7.0.1
with:
persist-credentials: false

- name: Check for hardcoded secrets in Rust
run: |
set -euo pipefail
TODAY="${RUST_TODAY:-$(date -u +%Y-%m-%d)}"

# An unparseable cutoff would pick the warn branch forever, silently
# disarming the widened scan. Refuse to run instead.
require_date() {
case "$2" in
[0-9][0-9][0-9][0-9]-[0-1][0-9]-[0-3][0-9]) : ;;
*) echo "::error::rust-secrets: $1='$2' is not YYYY-MM-DD."
echo "Refusing to run: an unparseable cutoff would disarm this gate."
exit 1 ;;
esac
}
require_date ENFORCE_RUST_WIDE_SCAN_FROM "$ENFORCE_RUST_WIDE_SCAN_FROM"
require_date RUST_TODAY "$TODAY"

# Self-skips when the tree has no Cargo.toml, so the job is safe on a
# repository that is not (yet) Rust. The check run still appears, which
# is what keeps the context stable across every generated repository.
if ! find . -name Cargo.toml -not -path './target/*' -print -quit | grep -q .; then
echo 'No Cargo.toml found — skipping Rust secrets check'
exit 0
fi

# Scan every .rs file, not just ./src. A Cargo workspace keeps its
# code in crates/*/src, and a `grep … src/` matches nothing there:
# grep exits 2 on a missing directory, which an `if` reads as "clean".
mapfile -t FILES < <(find . -name '*.rs' \
-not -path './target/*' -not -path '*/target/*' \
-not -path './vendor/*' -not -path '*/vendor/*' \
-not -path './.git/*' -print)
if [ ${#FILES[@]} -eq 0 ]; then
echo 'Cargo.toml present but no .rs files — nothing to scan'
exit 0
fi
echo "Scanning ${#FILES[@]} Rust file(s)."

# Each pattern requires an assignment DIRECTLY to a string literal of
# meaningful length, so lookups, paths and demos do not match. A
# credential shorter than 8 characters is not a credential either.
# `static` is accepted alongside `const`: a `static AUTH_KEY: &str =
# "…"` is a genuine hardcoded secret.
PATTERNS=(
'(const|static)[[:space:]]+(mut[[:space:]]+)?[A-Za-z0-9_]*SECRET[A-Za-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[^"]{8,}"'
'(const|static)[[:space:]]+(mut[[:space:]]+)?[A-Za-z0-9_]*KEY[A-Za-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[a-zA-Z0-9]{16,}"'
'(const|static)[[:space:]]+(mut[[:space:]]+)?[A-Za-z0-9_]*TOKEN[A-Za-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[^"]{8,}"'
'(let|static)[[:space:]]+(mut[[:space:]]+)?[a-z0-9_]*api_key[a-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[^"]{8,}"'
'HMAC.*"[a-fA-F0-9]{32,}"'
'[a-z0-9_]*password[a-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[^"]{8,}"'
)

# Exemptions match on the VALUE or on an explicit pragma, never on a
# file path: a path-based exemption would blind the job to a genuine
# secret in the same file.
# 1. env-lookup RHS — `env::var("NAME")` IS the practice this job
# exists to enforce, so flagging it fails the correct code.
# 2. URL values — an OAuth endpoint is public, not a credential.
# 3. comment lines — documentation of a pattern is not a secret.
# 4. inline pragma `// scanner-allow: rust-secrets`.
COMMENT='^[^:]*:[0-9][0-9]*:[[:space:]]*(//|/\*|\*)'
ENV_RHS='=[^;]*(env::var|env::var_os|std::env|env!\(|option_env!\(|from_env|dotenv)'
URL_RHS='=[[:space:]]*b?"(https?|wss?|ftp)://'
PRAGMA='scanner-allow:[[:space:]]*rust-secrets'

blocking=0
advisory=0
for pattern in "${PATTERNS[@]}"; do
hits="$(grep -nHE "$pattern" "${FILES[@]}" 2>/dev/null \
| grep -vE "$COMMENT" \
| grep -vE "$ENV_RHS" \
| grep -vE "$URL_RHS" \
| grep -vE "$PRAGMA" || [ $? -eq 1 ])"
[ -n "$hits" ] || continue

# ./src hits keep blocking. Hits outside it are newly visible, so
# they warn until the cutoff rather than reddening repositories
# whose wider tree was never actually being scanned.
old_scope="$(printf '%s\n' "$hits" | grep -E '^\./src/' || [ $? -eq 1 ])"
new_scope="$(printf '%s\n' "$hits" | grep -vE '^\./src/' || [ $? -eq 1 ])"

if [ -n "$old_scope" ]; then
printf '%s\n' "$old_scope"
echo "WARNING: Potential hardcoded secret found matching: $pattern"
blocking=1
fi
if [ -n "$new_scope" ]; then
printf '%s\n' "$new_scope"
if [[ "$TODAY" < "$ENFORCE_RUST_WIDE_SCAN_FROM" ]]; then
echo "::warning::Potential hardcoded secret outside ./src matching:" \
"$pattern — becomes BLOCKING on $ENFORCE_RUST_WIDE_SCAN_FROM (today is $TODAY)."
advisory=1
else
echo "WARNING: Potential hardcoded secret found matching: $pattern"
blocking=1
fi
fi
done

if [ "$blocking" -eq 1 ]; then
echo "::error::Potential hardcoded secrets detected. Use environment variables instead."
exit 1
fi
if [ "$advisory" -eq 1 ]; then
# Never claim a clean pass while findings are outstanding.
echo "NOT YET ENFORCED: findings outside ./src are advisory until $ENFORCE_RUST_WIDE_SCAN_FROM."
exit 0
fi
echo 'No hardcoded secrets detected in Rust sources.'

shell-secrets:
name: "scan / shell-secrets"
runs-on: ubuntu-24.04
timeout-minutes: 10
permissions:
contents: read
steps:
- name: Checkout repository
uses: actions/checkout@v7.0.1
with:
persist-credentials: false

- name: Run repository secret pattern hook
run: |
set -euo pipefail
rc=0
git grep -IlE '(ghp_[A-Za-z0-9]{36}|github_pat_[A-Za-z0-9_]{82}|glpat-[A-Za-z0-9_-]{20,}|AKIA[0-9A-Z]{16}|-----BEGIN (RSA |EC |OPENSSH )?PRIVATE KEY-----)' > "$RUNNER_TEMP/hits.txt" || rc=$?
# git grep exits 1 when nothing matches; above 1 is an error.
if [ "$rc" -gt 1 ]; then
echo "::error::Secret pattern scan failed with exit ${rc}"
exit 2
fi
# Exclude intentional scanner rules and adversarial negative test fixtures.
filtered="$(grep -vE '^(\.github/hooks/scan-secrets\.sh|\.github/workflows/secret-scanner\.yml|\.machine_readable/testing/adversarial-content\.k9\.ncl|tests/)' "$RUNNER_TEMP/hits.txt" || :)"
if [ -n "$filtered" ]; then
echo "::error::Hardcoded credential material detected:"
printf '%s\n' "$filtered"
exit 1
fi
echo "No hardcoded shell/source credentials detected."
15 changes: 12 additions & 3 deletions CLAUDE.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,16 @@
- UK English. AsciiDoc for docs (`.adoc`), not Markdown (this file and
the bootstrap prompt are the only exceptions).
- GitHub is the single source of truth; mirrors are spokes.
- No Python. Lean 4 for proofs; shell for glue; Podman if containers
are ever needed.
- No Python. Shell for glue; Podman if containers are ever needed.
- Proofs follow the estate policy (`hyperpolymath/standards`
`3-practice/PROOF-POLICY.adoc`): marches is *theory*, so Agda is the
source of truth, rechecked in Rocq and Lean, with no Mathlib. The
Lean 4 development here predates that ruling and is target-only
evidence (the Lean leg) until an Agda proof of the same statement is
checked and the two are reconciled. Every theorem is `ungraded`
(no PWG) until then; `PROOF-STATUS.adoc` holds the record. Never call
a theorem graded or "verified" under the estate policy on the
strength of the Lean build alone.
- Claim taxonomy: PROVEN / TESTED / ASSUMED / DESIGNED / OPEN.
Anti-Goodhart clause: a status upgrade must name the transcribable
artifact that discharges it (build log, eval output, test run).
Expand All @@ -17,4 +25,5 @@
- Before ending a session: update STATE.adoc, commit with a message
naming the rung, and tag only if all gates pass.
- Gates for this repo: `lake build` green; `grep -rn "sorry" Marches/`
empty; the BadGadget `#eval` prints the period-2 orbit.
empty; the BadGadget `#eval` prints the period-2 orbit. A change that
adds or alters a theorem also updates `PROOF-STATUS.adoc`.
Loading
Loading