Skip to content

Commit c4d74f3

Browse files
chore: RSR template floor (23 files: githealth + RSR docs + dotfiles + contractiles + 4 mandatory workflows + stapeln) (#30)
## Summary Bring `echo-types` to the RSR template floor — 23 new files covering githealth, RSR docs, dotfiles, the AI manifest, the canonical 4 mandatory workflows, contractiles, and a stapeln/Containerfile pair sized for the proof-artefact-carrier shape this repo ships. This is the second of three echo-types PRs: 1. PR #29 — `.scm` → `.a2ml` for 6a2 files + Justfile `make` → `just`. (Merged or pending.) 2. **This PR** — RSR floor scaffolding. 3. Forthcoming — recognition PR against `hyperpolymath/standards` (Agda + echo-types as canonical loss-with-residue foundation). ## What's added ### Githealth (5 files, `.md` per the doc-format rule) - `CHANGELOG.md` — Keep-a-Changelog format, with the staged 7-commit integration (per STATE.a2ml § integration) under `[Unreleased]`. - `CODE_OF_CONDUCT.md` — Contributor Covenant 2.1 reference. - `CONTRIBUTING.md` — DCO, branch rules, pre-merge checklist with **estate banned-pattern list** (no new `believe_me` / `assert_total` / `postulate` / `sorry` / `Admitted` / `unsafeCoerce` / `Obj.magic`), **EI-2 discipline** (do not reopen; cite STATE), and **naming traps** (ModeGraded canonical, ModeGrade forbidden). - `SECURITY.md` — disclosure policy + posture (formal-methods library; no networked attack surface; report proof-soundness concerns to same address). - `0-AI-MANIFEST.a2ml` — agent gating: may-edit, may-not-edit, escalation triggers (especially the EI-2 mention procedure that routes to `PLAYBOOK.a2ml § on-EI-2-mention`). ### RSR docs (5 files) - `EXPLAINME.adoc` — one-paragraph + one-sentence + status snapshot. - `QUICKSTART-DEV.adoc` — toolchain, first build, common failures (banned-pattern detection, naming-trap, EI-2 reopen). - `QUICKSTART-USER.adoc` — depend on echo-types as a library; cite the formalism. - `QUICKSTART-MAINTAINER.adoc` — release procedure; new-bridge addition checklist; escalation patterns. - `TOPOLOGY.adoc` — repo layout + cross-repo dependency direction (foundation: depends on `hyperpolymath/standards` schemas only) + verification posture table per track. ### Dotfiles (3 files) - `.editorconfig` — LF, UTF-8, 2-space default; 4 for Rust; tab for Justfile/Makefile. - `.envrc` — `use flake` (flake.nix is parked per Intentfile). - `.tool-versions` — agda 2.7.0, ghc 9.8.2, cabal 3.12.1.0, rust 1.82.0, just 1.40.0. ### Contractiles (4 files) - `contractiles/Mustfile.a2ml` — invariants: license/readme/security/changelog/spdx-headers/no-banned-files/agda-typechecks/no-believe_me/no-postulates/no-sorry/mode-graded-canonical/rust-compiles. - `contractiles/Trustfile.a2ml` — license content / no secrets / images pinned (post-pin) / **ei-2-record-intact** check. - `contractiles/Dustfile.a2ml` — source-rollback / clean-build (Agda `.agdai`s + Rust `target/`) / resync-from-template. - `contractiles/Intentfile.a2ml` — RSR conformance / proofs (Buchholz close, Q2.1/Q2.3/Q2.4 discharge) / process / explicitly-parked (recipe v0.2+, full 2D iff theorem). ### Mandatory RSR workflows (4 files) Copied verbatim from `hyperpolymath/standards/.github/workflows/` (the canonical 4 per `hypatia-rules/rsr-self-compliance.a2ml @required_workflows`): - `.github/workflows/hypatia-scan.yml` - `.github/workflows/mirror.yml` - `.github/workflows/scorecard.yml` - `.github/workflows/rsr-antipattern.yml` (Existing `agda.yml` workflow remains; it's the proof-typecheck CI lane.) ### Container build - `stapeln.toml` — layered Chainguard build with **echo-types-runtime** as a `static` (artefact-carrier) image: holds the type-checked `proofs/` tree for downstream Agda projects to mount, not a service. `@sha256:` pins are `TODO(scaffold)` markers. - `Containerfile` — podman-build fallback shape. ## What's deliberately NOT in this PR Per the staged sequence and the maintainer's existing parked migrations: - `readme.adoc` (lowercase) → `README.adoc` (canonical caps) — leaving the lowercase as-is so this PR stays focused on additions; rename is a follow-up. - `roadmap.adoc` / `roadmap-gates.adoc` — same reason. - `README.md` (duplicate of `readme.adoc`) — rationalisation needs a content review beyond mechanical renaming. - `DOCUMENTATION_STATUS.md` and `docs/*.md` (~7 files) — `.md` → `.adoc` per the doc-format rule, but content review is needed; follow-up PR. - `flake.nix` / `guix.scm` — toolchain reproducibility files, listed in Intentfile but require deliberate authoring. - `.machine_readable/` reorganisation to match `hyperpolymath/standards`'s contractile-trident shape (`.machine_readable/contractiles/<verb>/...`) — substantial, separate PR. - `Abstract-Echo-Types` and `arghda-core/README.md` — kept as-is (need content judgement). ## Why merge this It brings echo-types from "minimum-viable" file presence to the RSR template floor as defined in `hyperpolymath/standards/.meta/REQUIRED-FILES.adoc` (extension fix pending — see standards PR #33). Once this lands, downstream tooling that audits hyperpolymath repos for floor conformance (e.g. `idaptik-port/tools/scaffold-component.{py,my} --audit`) will report this repo as conformant. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 5f32137 commit c4d74f3

23 files changed

Lines changed: 978 additions & 0 deletions

.editorconfig

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
root = true
3+
4+
[*]
5+
end_of_line = lf
6+
insert_final_newline = true
7+
charset = utf-8
8+
indent_style = space
9+
indent_size = 2
10+
trim_trailing_whitespace = true
11+
12+
[*.agda]
13+
indent_size = 2
14+
15+
[*.rs]
16+
indent_size = 4
17+
18+
[Makefile]
19+
indent_style = tab
20+
21+
[Justfile]
22+
indent_style = tab

.envrc

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
use flake

.github/workflows/hypatia-scan.yml

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Hypatia Neurosymbolic CI/CD Security Scan — SELF-SCAN (dogfooding)
3+
# The standards repo that defines Hypatia scans itself with Hypatia.
4+
name: Hypatia Self-Scan
5+
6+
on:
7+
push:
8+
branches: [ main ]
9+
pull_request:
10+
branches: [ main ]
11+
schedule:
12+
- cron: '0 0 * * 0' # Weekly on Sunday
13+
workflow_dispatch:
14+
15+
permissions: read-all
16+
17+
jobs:
18+
scan:
19+
name: Hypatia Neurosymbolic Analysis (Dogfooding)
20+
runs-on: ubuntu-latest
21+
22+
steps:
23+
- name: Checkout repository
24+
uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
25+
with:
26+
fetch-depth: 0
27+
28+
- name: Setup Elixir for Hypatia scanner
29+
uses: erlef/setup-beam@fc68ffb90438ef2936bbb3251622353b3dcb2f93 # v1.24.0
30+
with:
31+
elixir-version: '1.19.4'
32+
otp-version: '28.3'
33+
34+
- name: Clone Hypatia
35+
run: |
36+
git clone --depth 1 https://github.com/hyperpolymath/hypatia.git "$HOME/hypatia"
37+
38+
- name: Build Hypatia scanner
39+
run: |
40+
cd "$HOME/hypatia"
41+
if [ ! -f hypatia-v2 ]; then
42+
cd scanner && mix deps.get && mix escript.build && mv hypatia ../hypatia-v2
43+
fi
44+
45+
- name: Run Hypatia scan
46+
id: scan
47+
run: |
48+
echo "Scanning standards repo (dogfooding)"
49+
HYPATIA_FORMAT=json "$HOME/hypatia/hypatia-cli.sh" scan . > hypatia-findings.json
50+
51+
FINDING_COUNT=$(jq '. | length' hypatia-findings.json 2>/dev/null || echo 0)
52+
CRITICAL=$(jq '[.[] | select(.severity == "critical")] | length' hypatia-findings.json 2>/dev/null || echo 0)
53+
HIGH=$(jq '[.[] | select(.severity == "high")] | length' hypatia-findings.json 2>/dev/null || echo 0)
54+
MEDIUM=$(jq '[.[] | select(.severity == "medium")] | length' hypatia-findings.json 2>/dev/null || echo 0)
55+
56+
echo "findings_count=$FINDING_COUNT" >> $GITHUB_OUTPUT
57+
echo "critical=$CRITICAL" >> $GITHUB_OUTPUT
58+
echo "high=$HIGH" >> $GITHUB_OUTPUT
59+
echo "medium=$MEDIUM" >> $GITHUB_OUTPUT
60+
61+
echo "## Hypatia Self-Scan Results (Dogfooding)" >> $GITHUB_STEP_SUMMARY
62+
echo "" >> $GITHUB_STEP_SUMMARY
63+
echo "The standards repo scans itself. Findings here are compliance" >> $GITHUB_STEP_SUMMARY
64+
echo "gaps between what we define and what we practice." >> $GITHUB_STEP_SUMMARY
65+
echo "" >> $GITHUB_STEP_SUMMARY
66+
echo "| Severity | Count |" >> $GITHUB_STEP_SUMMARY
67+
echo "|----------|-------|" >> $GITHUB_STEP_SUMMARY
68+
echo "| Critical | $CRITICAL |" >> $GITHUB_STEP_SUMMARY
69+
echo "| High | $HIGH |" >> $GITHUB_STEP_SUMMARY
70+
echo "| Medium | $MEDIUM |" >> $GITHUB_STEP_SUMMARY
71+
echo "| **Total**| $FINDING_COUNT |" >> $GITHUB_STEP_SUMMARY
72+
73+
- name: Run panic-attack assail
74+
run: |
75+
# Install panic-attack if available
76+
if command -v panic-attack >/dev/null 2>&1; then
77+
panic-attack assail . > panic-attack-findings.json 2>&1 || true
78+
echo "panic-attack scan complete"
79+
else
80+
echo "panic-attack not available in CI — install from hyperpolymath/panic-attacker"
81+
echo "[]" > panic-attack-findings.json
82+
fi
83+
84+
- name: Upload findings artifacts
85+
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
86+
with:
87+
name: standards-self-scan
88+
path: |
89+
hypatia-findings.json
90+
panic-attack-findings.json
91+
retention-days: 90
92+
93+
- name: Check for critical issues
94+
if: steps.scan.outputs.critical > 0
95+
run: |
96+
echo "Critical self-scan issues found in the standards repo!"
97+
echo "The repo that defines standards has compliance gaps."
98+
echo "Review hypatia-findings.json for details."
99+
# Warn but don't fail — fix forward

.github/workflows/mirror.yml

Lines changed: 145 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,145 @@
1+
# SPDX-License-Identifier: PMPL-1.0
2+
# SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
3+
name: Mirror to Git Forges
4+
5+
on:
6+
push:
7+
branches: [main]
8+
workflow_dispatch:
9+
10+
permissions:
11+
contents: read
12+
13+
jobs:
14+
mirror-gitlab:
15+
runs-on: ubuntu-latest
16+
if: vars.GITLAB_MIRROR_ENABLED == 'true'
17+
steps:
18+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
19+
with:
20+
fetch-depth: 0
21+
22+
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
23+
with:
24+
ssh-private-key: ${{ secrets.GITLAB_SSH_KEY }}
25+
26+
- name: Mirror to GitLab
27+
run: |
28+
ssh-keyscan -t ed25519 gitlab.com >> ~/.ssh/known_hosts
29+
git remote add gitlab git@gitlab.com:hyperpolymath/${{ github.event.repository.name }}.git || true
30+
git push --force gitlab main
31+
32+
mirror-bitbucket:
33+
runs-on: ubuntu-latest
34+
if: vars.BITBUCKET_MIRROR_ENABLED == 'true'
35+
steps:
36+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
37+
with:
38+
fetch-depth: 0
39+
40+
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
41+
with:
42+
ssh-private-key: ${{ secrets.BITBUCKET_SSH_KEY }}
43+
44+
- name: Mirror to Bitbucket
45+
run: |
46+
ssh-keyscan -t ed25519 bitbucket.org >> ~/.ssh/known_hosts
47+
git remote add bitbucket git@bitbucket.org:hyperpolymath/${{ github.event.repository.name }}.git || true
48+
git push --force bitbucket main
49+
50+
mirror-codeberg:
51+
runs-on: ubuntu-latest
52+
if: vars.CODEBERG_MIRROR_ENABLED == 'true'
53+
steps:
54+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
55+
with:
56+
fetch-depth: 0
57+
58+
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
59+
with:
60+
ssh-private-key: ${{ secrets.CODEBERG_SSH_KEY }}
61+
62+
- name: Mirror to Codeberg
63+
run: |
64+
ssh-keyscan -t ed25519 codeberg.org >> ~/.ssh/known_hosts
65+
git remote add codeberg git@codeberg.org:hyperpolymath/${{ github.event.repository.name }}.git || true
66+
git push --force codeberg main
67+
68+
mirror-sourcehut:
69+
runs-on: ubuntu-latest
70+
if: vars.SOURCEHUT_MIRROR_ENABLED == 'true'
71+
steps:
72+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
73+
with:
74+
fetch-depth: 0
75+
76+
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
77+
with:
78+
ssh-private-key: ${{ secrets.SOURCEHUT_SSH_KEY }}
79+
80+
- name: Mirror to SourceHut
81+
run: |
82+
ssh-keyscan -t ed25519 git.sr.ht >> ~/.ssh/known_hosts
83+
git remote add sourcehut git@git.sr.ht:~hyperpolymath/${{ github.event.repository.name }} || true
84+
git push --force sourcehut main
85+
86+
mirror-disroot:
87+
runs-on: ubuntu-latest
88+
if: vars.DISROOT_MIRROR_ENABLED == 'true'
89+
steps:
90+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
91+
with:
92+
fetch-depth: 0
93+
94+
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
95+
with:
96+
ssh-private-key: ${{ secrets.DISROOT_SSH_KEY }}
97+
98+
- name: Mirror to Disroot
99+
run: |
100+
ssh-keyscan -t ed25519 git.disroot.org >> ~/.ssh/known_hosts
101+
git remote add disroot git@git.disroot.org:hyperpolymath/${{ github.event.repository.name }}.git || true
102+
git push --force disroot main
103+
104+
mirror-gitea:
105+
runs-on: ubuntu-latest
106+
if: vars.GITEA_MIRROR_ENABLED == 'true'
107+
steps:
108+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
109+
with:
110+
fetch-depth: 0
111+
112+
- uses: webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555 # v0.10.0
113+
with:
114+
ssh-private-key: ${{ secrets.GITEA_SSH_KEY }}
115+
116+
- name: Mirror to Gitea
117+
run: |
118+
ssh-keyscan -t ed25519 ${{ vars.GITEA_HOST }} >> ~/.ssh/known_hosts
119+
git remote add gitea git@${{ vars.GITEA_HOST }}:hyperpolymath/${{ github.event.repository.name }}.git || true
120+
git push --force gitea main
121+
122+
mirror-radicle:
123+
runs-on: ubuntu-latest
124+
if: vars.RADICLE_MIRROR_ENABLED == 'true'
125+
steps:
126+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
127+
with:
128+
fetch-depth: 0
129+
130+
- name: Setup Rust
131+
uses: dtolnay/rust-toolchain@efa25f7f19611383d5b0ccf2d1c8914531636bf9 # stable
132+
with:
133+
toolchain: stable
134+
135+
- name: Install Radicle
136+
run: |
137+
# Install via cargo (safer than curl|sh)
138+
cargo install radicle-cli --locked
139+
echo "$HOME/.cargo/bin" >> $GITHUB_PATH
140+
141+
- name: Mirror to Radicle
142+
run: |
143+
echo "${{ secrets.RADICLE_KEY }}" > ~/.radicle/keys/radicle
144+
chmod 600 ~/.radicle/keys/radicle
145+
rad sync --announce || echo "Radicle sync attempted"
Lines changed: 112 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,112 @@
1+
# SPDX-License-Identifier: PMPL-1.0
2+
# RSR Anti-Pattern CI Check
3+
#
4+
# Enforces: No TypeScript, No ReScript, No Go, No Python (except SaltStack), No npm
5+
# Allows: AffineScript, Deno, WASM, Rust, OCaml, Haskell, Guile/Scheme
6+
7+
name: RSR Anti-Pattern Check
8+
9+
on:
10+
push:
11+
branches: [main, master, develop]
12+
pull_request:
13+
branches: [main, master, develop]
14+
15+
16+
permissions:
17+
contents: read
18+
19+
jobs:
20+
antipattern-check:
21+
runs-on: ubuntu-latest
22+
permissions:
23+
contents: read
24+
steps:
25+
- uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
26+
27+
- name: Check for TypeScript
28+
run: |
29+
# Exclude bindings/deno/ - those are Deno FFI files using Deno.dlopen, not plain TypeScript
30+
# Exclude .d.ts files - generated type declarations for FFI
31+
TS_FILES=$(find . \( -name "*.ts" -o -name "*.tsx" \) | grep -v node_modules | grep -v 'bindings/deno' | grep -v '\.d\.ts$' || true)
32+
if [ -n "$TS_FILES" ]; then
33+
echo "❌ TypeScript files detected - use AffineScript instead"
34+
echo "$TS_FILES"
35+
exit 1
36+
fi
37+
echo "✅ No TypeScript files (Deno FFI bindings excluded)"
38+
39+
- name: Check for ReScript
40+
run: |
41+
# Estate policy: RS/TS/JS -> AffineScript -> typed-wasm. ReScript (.res)
42+
# is no longer used as the TS replacement; new code uses .affine instead.
43+
RES_FILES=$(find . -name "*.res" | grep -v node_modules || true)
44+
if [ -n "$RES_FILES" ]; then
45+
echo "❌ ReScript files detected - use AffineScript instead"
46+
echo "$RES_FILES"
47+
exit 1
48+
fi
49+
echo "✅ No ReScript files"
50+
51+
- name: Check for Go
52+
run: |
53+
if find . -name "*.go" | grep -q .; then
54+
echo "❌ Go files detected - use Rust/WASM instead"
55+
find . -name "*.go"
56+
exit 1
57+
fi
58+
echo "✅ No Go files"
59+
60+
- name: Check for Python (non-SaltStack)
61+
run: |
62+
PY_FILES=$(find . -name "*.py" | grep -v salt | grep -v _states | grep -v _modules | grep -v pillar | grep -v venv | grep -v __pycache__ || true)
63+
if [ -n "$PY_FILES" ]; then
64+
echo "❌ Python files detected - only allowed for SaltStack"
65+
echo "$PY_FILES"
66+
exit 1
67+
fi
68+
echo "✅ No non-SaltStack Python files"
69+
70+
- name: Check for npm lockfiles
71+
run: |
72+
if [ -f "package-lock.json" ] || [ -f "yarn.lock" ]; then
73+
echo "❌ npm/yarn lockfile detected - use Deno instead"
74+
exit 1
75+
fi
76+
echo "✅ No npm lockfiles"
77+
78+
- name: Check for tsconfig
79+
run: |
80+
if [ -f "tsconfig.json" ]; then
81+
echo "❌ tsconfig.json detected - use AffineScript instead"
82+
exit 1
83+
fi
84+
echo "✅ No tsconfig.json"
85+
86+
- name: Check for rescript.json
87+
run: |
88+
if [ -f "rescript.json" ] || [ -f "bsconfig.json" ]; then
89+
echo "❌ rescript.json/bsconfig.json detected - use AffineScript config instead"
90+
exit 1
91+
fi
92+
echo "✅ No rescript.json/bsconfig.json"
93+
94+
- name: Verify Deno presence (if package.json exists)
95+
run: |
96+
if [ -f "package.json" ]; then
97+
if [ ! -f "deno.json" ] && [ ! -f "deno.jsonc" ]; then
98+
echo "⚠️ Warning: package.json without deno.json - migration recommended"
99+
fi
100+
fi
101+
echo "✅ Deno configuration check complete"
102+
103+
- name: Summary
104+
run: |
105+
echo "╔════════════════════════════════════════════════════════════╗"
106+
echo "║ RSR Anti-Pattern Check Passed ✅ ║"
107+
echo "║ ║"
108+
echo "║ Allowed: AffineScript, Deno, WASM, Rust, OCaml, Haskell, ║"
109+
echo "║ Guile/Scheme, SaltStack (Python) ║"
110+
echo "║ ║"
111+
echo "║ Blocked: TypeScript, ReScript, Go, npm, Python (non-Salt)║"
112+
echo "╚════════════════════════════════════════════════════════════╝"

0 commit comments

Comments
 (0)