diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS new file mode 100644 index 00000000..3a3b7f20 --- /dev/null +++ b/.github/CODEOWNERS @@ -0,0 +1,34 @@ +# SPDX-License-Identifier: MPL-2.0 +# CODEOWNERS - Define code review assignments for GitHub +# See: https://docs.github.com/en/repositories/managing-your-repositorys-settings-and-features/customizing-your-repository/about-code-owners + +# Default: sole maintainer for all files +* @hyperpolymath + +# Security-sensitive files require explicit ownership +SECURITY.md @hyperpolymath +.github/workflows/ @hyperpolymath +.machine_readable/ @hyperpolymath +contractiles/ @hyperpolymath + +# License files +LICENSE @hyperpolymath +LICENSES/ @hyperpolymath + +# Configuration +.gitignore @hyperpolymath +.github/ @hyperpolymath + +# Documentation +README* @hyperpolymath +CONTRIBUTING* @hyperpolymath +CODE_OF_CONDUCT* @hyperpolymath +GOVERNANCE* @hyperpolymath +MAINTAINERS* @hyperpolymath +CHANGELOG* @hyperpolymath +ROADMAP* @hyperpolymath + +# Build and CI +Justfile @hyperpolymath +Makefile @hyperpolymath +*.sh @hyperpolymath diff --git a/.github/workflows/abi-verify.yml b/.github/workflows/abi-verify.yml index cb62e025..094f9a46 100644 --- a/.github/workflows/abi-verify.yml +++ b/.github/workflows/abi-verify.yml @@ -38,6 +38,7 @@ jobs: idris2-abi: name: Idris2 ABI seam (ephapax-abi.ipkg) runs-on: ubuntu-latest + timeout-minutes: 15 container: image: snazzybucket/idris2:latest # estate-standard Idris2 image steps: diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml index ddeab5d0..dabd0168 100644 --- a/.github/workflows/boj-build.yml +++ b/.github/workflows/boj-build.yml @@ -7,6 +7,7 @@ on: jobs: trigger-boj: runs-on: ubuntu-latest + timeout-minutes: 15 steps: - name: Checkout uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index 57a469be..1bdb30a9 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -23,6 +23,7 @@ permissions: jobs: analyze: runs-on: ubuntu-latest + timeout-minutes: 15 permissions: contents: read security-events: write diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index 5410ae60..c4cf76fd 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -23,3 +23,4 @@ permissions: jobs: governance: uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@main + timeout-minutes: 10 diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index cfca4280..2e817b0c 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -43,6 +43,7 @@ jobs: scan: name: Hypatia Neurosymbolic Analysis runs-on: ubuntu-latest + timeout-minutes: 15 steps: - name: Checkout repository diff --git a/.github/workflows/instant-sync.yml b/.github/workflows/instant-sync.yml index 98a72733..9c2c1185 100644 --- a/.github/workflows/instant-sync.yml +++ b/.github/workflows/instant-sync.yml @@ -14,6 +14,7 @@ permissions: jobs: dispatch: runs-on: ubuntu-latest + timeout-minutes: 15 steps: - name: Trigger Propagation uses: peter-evans/repository-dispatch@28959ce8df70de7be546dd1250a005dd32156697 # v3 diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml index 8ea6f8ce..c4d068af 100644 --- a/.github/workflows/mirror.yml +++ b/.github/workflows/mirror.yml @@ -13,6 +13,7 @@ permissions: jobs: mirror-gitlab: runs-on: ubuntu-latest + timeout-minutes: 15 if: vars.GITLAB_MIRROR_ENABLED == 'true' steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 @@ -31,6 +32,7 @@ jobs: mirror-bitbucket: runs-on: ubuntu-latest + timeout-minutes: 15 if: vars.BITBUCKET_MIRROR_ENABLED == 'true' steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 @@ -49,6 +51,7 @@ jobs: mirror-codeberg: runs-on: ubuntu-latest + timeout-minutes: 15 if: vars.CODEBERG_MIRROR_ENABLED == 'true' steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 @@ -67,6 +70,7 @@ jobs: mirror-sourcehut: runs-on: ubuntu-latest + timeout-minutes: 15 if: vars.SOURCEHUT_MIRROR_ENABLED == 'true' steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 @@ -85,6 +89,7 @@ jobs: mirror-disroot: runs-on: ubuntu-latest + timeout-minutes: 15 if: vars.DISROOT_MIRROR_ENABLED == 'true' steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 @@ -103,6 +108,7 @@ jobs: mirror-gitea: runs-on: ubuntu-latest + timeout-minutes: 15 if: vars.GITEA_MIRROR_ENABLED == 'true' steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 @@ -121,6 +127,7 @@ jobs: mirror-radicle: runs-on: ubuntu-latest + timeout-minutes: 15 if: vars.RADICLE_MIRROR_ENABLED == 'true' steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index ad254f81..f861d9f9 100644 --- a/.github/workflows/rust-ci.yml +++ b/.github/workflows/rust-ci.yml @@ -18,6 +18,7 @@ jobs: check: name: Cargo check + clippy + fmt runs-on: ubuntu-latest + timeout-minutes: 15 if: hashFiles('Cargo.toml') != '' steps: @@ -44,6 +45,7 @@ jobs: test: name: Cargo test runs-on: ubuntu-latest + timeout-minutes: 15 needs: check if: hashFiles('Cargo.toml') != '' @@ -71,6 +73,7 @@ jobs: status-gate: name: Status gate runs-on: ubuntu-latest + timeout-minutes: 15 needs: check if: hashFiles('Cargo.toml') != '' @@ -90,6 +93,7 @@ jobs: proofs: name: Coq proofs runs-on: ubuntu-latest + timeout-minutes: 15 needs: check steps: diff --git a/.github/workflows/scorecard-enforcer.yml b/.github/workflows/scorecard-enforcer.yml index af0bef88..aaf4ff98 100644 --- a/.github/workflows/scorecard-enforcer.yml +++ b/.github/workflows/scorecard-enforcer.yml @@ -23,6 +23,7 @@ permissions: jobs: scorecard: runs-on: ubuntu-latest + timeout-minutes: 15 permissions: security-events: write id-token: write # For OIDC @@ -61,6 +62,7 @@ jobs: # Check specific high-priority items check-critical: runs-on: ubuntu-latest + timeout-minutes: 15 steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index 02fe2586..737d8f6a 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -21,6 +21,7 @@ permissions: jobs: analysis: runs-on: ubuntu-latest + timeout-minutes: 15 permissions: security-events: write id-token: write diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index dcef51a9..c8973523 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -21,6 +21,7 @@ permissions: jobs: trufflehog: runs-on: ubuntu-latest + timeout-minutes: 15 steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 with: @@ -33,6 +34,7 @@ jobs: gitleaks: runs-on: ubuntu-latest + timeout-minutes: 15 steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 with: @@ -46,6 +48,7 @@ jobs: # Rust-specific: Check for hardcoded crypto values rust-secrets: runs-on: ubuntu-latest + timeout-minutes: 15 if: hashFiles('**/Cargo.toml') != '' steps: - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 diff --git a/.gitignore b/.gitignore index cf2d4cd9..8d289f77 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,9 @@ # SPDX-License-Identifier: PMPL-1.0-or-later # RSR-compliant .gitignore +# Claude Code agent worktrees +.claude/ + # OS & Editor .DS_Store Thumbs.db diff --git a/.machine_readable/ADJUST.contractile b/.machine_readable/ADJUST.contractile deleted file mode 100644 index 3989d5b3..00000000 --- a/.machine_readable/ADJUST.contractile +++ /dev/null @@ -1,126 +0,0 @@ -; SPDX-License-Identifier: PMPL-1.0-or-later -; ADJUST.contractile — Accessibility invariants for ephapax -; "ADJUST" = Accessibility & Digital Justice for Universal Software & Technology -; -; Part of the contractile family: MUST, TRUST, DUST, INTENT, ADJUST -; This file is machine-readable. LLM/SLM agents MUST NOT violate these invariants. - -; ── Definitions ────────────────────────────────────────────────── -; -; ADJUST (noun/verb) -; The accessibility contractile. Defines how software must adapt to serve -; all users regardless of ability, device, or context. Named for the verb -; "adjust" — to make suitable, to adapt, to accommodate — which is the -; core action of accessible design. -; -; Scope: -; ADJUST governs all user-facing interfaces: GUI, TUI, CLI, web, mobile, -; documentation, error messages, and installation flows. It applies to -; both human users and assistive technologies (screen readers, switch -; devices, braille displays, voice control). -; -; Relationship to other contractiles: -; - MUST: ADJUST invariants are a subset of MUST — violating ADJUST -; is a MUST violation. ADJUST exists separately because accessibility -; rules are numerous enough to warrant their own file, and because -; LLMs frequently forget accessibility unless explicitly reminded. -; - TRUST: ADJUST does not affect trust levels. All trust tiers must -; respect ADJUST invariants equally. -; - DUST: Deprecating a feature does not exempt it from ADJUST until -; it is fully removed. Deprecated UI must remain accessible. -; - INTENT: ADJUST supports the anti-purpose "this software is NOT -; only for able-bodied users with modern hardware." -; -; Standard: WCAG 2.2 Level AA (minimum) -; https://www.w3.org/WAI/WCAG22/quickref/?levels=aaa -; -; Why a separate file: -; Experience shows LLMs and developers alike treat accessibility as an -; afterthought. By placing invariants in a contractile that is loaded -; at session start, we make it structurally impossible to forget. -; -; ── End Definitions ────────────────────────────────────────────── - -(adjust-contractile - (version "1.0.0") - (full-name "Accessibility & Digital Justice for Universal Software & Technology") - (standard "WCAG-2.2-AA") - (repo "ephapax") - - (invariants - ; ── Visual ── - (adjust "colour-contrast-ratio >= 4.5:1 for normal text") - (adjust "colour-contrast-ratio >= 3:1 for large text (18pt+ or 14pt+ bold)") - (adjust "no information conveyed by colour alone") - (adjust "no flashing or strobing content (3 flashes/second max)") - (adjust "text resizable to 200% without loss of content or function") - (adjust "focus indicators visible on all interactive elements") - - ; ── Keyboard ── - (adjust "all interactive elements reachable via keyboard (Tab/Shift+Tab)") - (adjust "no keyboard traps — user can always Tab away") - (adjust "skip navigation link present on pages with repeated blocks") - (adjust "logical focus order follows visual reading order") - - ; ── Screen reader ── - (adjust "all images have meaningful alt text (or alt='' if decorative)") - (adjust "all form inputs have associated labels") - (adjust "ARIA landmarks used for page regions (main, nav, banner, etc.)") - (adjust "dynamic content updates announced via aria-live regions") - (adjust "semantic HTML used (headings, lists, tables) — not div soup") - - ; ── Interactive ── - (adjust "touch targets minimum 44x44px on mobile/touch interfaces") - (adjust "error messages identify the field and describe the error") - (adjust "error messages not conveyed by colour or position alone") - (adjust "form validation provides suggestions for correction") - - ; ── Media ── - (adjust "video has captions (closed or open)") - (adjust "audio-only content has text transcript") - (adjust "no autoplay of media with sound") - - ; ── Motion ── - (adjust "animations respect prefers-reduced-motion media query") - (adjust "no content depends on motion to convey meaning") - - ; ── CLI/TUI ── - (adjust "CLI output must not rely solely on colour (use symbols: [OK] [FAIL])") - (adjust "TUI must support high-contrast mode") - (adjust "all CLI commands support --help with plain-text output") - (adjust "error messages written in plain language, not jargon or codes alone") - - ; ── Documentation ── - (adjust "docs use clear language, short sentences, logical structure") - (adjust "code examples include comments explaining non-obvious steps") - (adjust "diagrams have text descriptions or alt text") - - ; ── Internationalisation (i18n) ── - (adjust "all user-facing strings externalisable for translation") - (adjust "no hardcoded English in error messages — use message keys") - (adjust "date/time/number formats locale-aware") - (adjust "RTL (right-to-left) layout support where applicable") - (adjust "Unicode handled correctly throughout (UTF-8 everywhere)") - ) - - (related-resources - ; LOL — super-parallel corpus crawler for 1500+ languages - ; Use for linguistic data, translation coverage, and i18n validation - (lol "standards/lol — multilingual NLP corpus, see README.adoc") - (polyglot-i18n "polyglot-i18n — i18n framework and WASM translation engine") - ) - - (enforcement - (ci "accessibility linting in quality.yml workflow") - (pr-block "PR blocked if accessibility regression detected") - (tool "axe-core or pa11y for automated checks on web UI") - (tool "CLI output inspected for colour-only signalling") - (manual "manual screen reader test before major releases") - ) - - (notes - "These are MINIMUM requirements. Exceeding them (AAA) is encouraged." - "When in doubt about an accessibility decision, ask — don't guess." - "Accessibility is not optional polish — it is a structural requirement." - ) -) diff --git a/.machine_readable/INTENT.contractile b/.machine_readable/INTENT.contractile deleted file mode 100644 index b389f4db..00000000 --- a/.machine_readable/INTENT.contractile +++ /dev/null @@ -1,72 +0,0 @@ -; SPDX-License-Identifier: PMPL-1.0-or-later -; INTENT.contractile — Purpose and scope for ephapax -; Helps LLM/SLM agents understand what this repo IS and IS NOT. -; -; Part of the contractile family: MUST, TRUST, DUST, INTENT, ADJUST - -; ── Definitions ────────────────────────────────────────────────── -; -; INTENT (noun) -; The purpose contractile. Defines what this repository IS, what it is -; NOT (anti-purpose), and which architectural decisions are load-bearing. -; Without INTENT, LLMs drift into scope creep, reverse key decisions, -; or add features that belong in a different repo. -; -; Scope: -; INTENT governs the conceptual boundaries of the project — its reason -; for existing, its domain, and its relationship to the ecosystem. -; It does NOT specify implementation details (that's MUST and code). -; -; Relationship to other contractiles: -; - MUST: INTENT explains WHY certain MUSTs exist. If you don't -; understand a MUST, read INTENT first. -; - TRUST: The "ask-before-touching" section in INTENT maps directly -; to TRUST.trust-deny for the most sensitive areas. -; - ADJUST: INTENT's anti-purpose should include "this software is -; NOT only for users with perfect vision/hearing/mobility." -; - DUST: When INTENT changes (repo pivots), related DUST entries -; should be created for the abandoned direction. -; -; ── End Definitions ────────────────────────────────────────────── - -(intent-contractile - (version "1.0.0") - (repo "ephapax") - - ; === Purpose (what this repo IS) === - (purpose - "{{ONE_PARAGRAPH_PURPOSE}}" - ) - - ; === Anti-Purpose (what this repo is NOT — prevents scope creep) === - (anti-purpose - "{{ONE_PARAGRAPH_ANTI_PURPOSE}}" - ; Examples: - ; "This is NOT a general-purpose database — it solves one specific problem." - ; "This is NOT a framework — it is a library with a focused API." - ; "This does NOT handle authentication — that is delegated to [other repo]." - ) - - ; === Key Architectural Decisions That Must Not Be Reversed === - (architectural-invariants - ; *REMINDER: List the foundational decisions* - ; ("Idris2 for ABI definitions — dependent types prove interface correctness") - ; ("Zig for FFI — zero-cost C ABI compatibility") - ; ("Elixir for supervision — OTP fault tolerance") - ) - - ; === Sensitive Areas (if in doubt, ask) === - (ask-before-touching - ; *REMINDER: List areas where LLMs should check before modifying* - ; "src/abi/ — formal proofs, changes require re-verification" - ; "ffi/zig/ — C ABI boundary, changes affect all language bindings" - ; ".machine_readable/ — checkpoint files, format is specified" - ) - - ; === Ecosystem Position === - (ecosystem - (belongs-to "{{MONOREPO_OR_STANDALONE}}") - (depends-on ("{{DEP1}}" "{{DEP2}}")) - (depended-on-by ("{{CONSUMER1}}" "{{CONSUMER2}}")) - ) -) diff --git a/.machine_readable/MUST.contractile b/.machine_readable/MUST.contractile deleted file mode 100644 index 5d91b2f3..00000000 --- a/.machine_readable/MUST.contractile +++ /dev/null @@ -1,91 +0,0 @@ -; SPDX-License-Identifier: PMPL-1.0-or-later -; MUST.contractile — Baseline invariants for ephapax -; These constraints MUST NOT be violated. K9 validators enforce them. -; -; Part of the contractile family: MUST, TRUST, DUST, INTENT, ADJUST - -; ── Definitions ────────────────────────────────────────────────── -; -; MUST (noun/verb) -; The hard-constraint contractile. Defines invariants that are structurally -; required for the repository to function correctly and safely. Violating -; a MUST is always a bug — there are no "soft" MUSTs. -; -; Scope: -; MUST governs code, configuration, CI, and structure. It does NOT govern -; style, preference, or approach — those belong in CLAUDE.md or coding -; standards. MUST is for things that break the project if violated. -; -; Relationship to other contractiles: -; - TRUST: MUST is enforced regardless of trust level. Even maximal-trust -; agents cannot violate MUST constraints. -; - ADJUST: All ADJUST invariants are implicitly MUST invariants too. -; ADJUST exists separately for visibility. -; - INTENT: MUST protects the architectural decisions described in INTENT. -; - DUST: When a feature enters DUST (deprecation), its MUST constraints -; remain active until the feature is fully removed. -; -; Enforcement: -; K9 validators in contractiles/k9/ machine-check MUST constraints. -; CI runs these on every PR. Violations block merge. -; -; ── End Definitions ────────────────────────────────────────────── - -(must-contractile - (version "1.0.0") - (repo "ephapax") - - ; === Universal Invariants (apply to ALL repos) === - - (invariants - ; Paths - (must "no hardcoded absolute paths (/home/*, /mnt/*, /var/mnt/*)") - (must "all paths use env vars, XDG dirs, or relative references") - - ; Language policy - (must "no new TypeScript files") - (must "no new Python files") - (must "no new Go files") - (must "no npm/bun/yarn/pnpm dependencies — Deno only") - - ; Dangerous patterns - (must "no believe_me (Idris2)") - (must "no assert_total (Idris2)") - (must "no Admitted (Coq)") - (must "no sorry (Lean)") - (must "no unsafeCoerce (Haskell)") - (must "no Obj.magic (OCaml)") - (must "no unsafe {} blocks without safety comment (Rust)") - - ; License - (must "SPDX-License-Identifier header on every source file") - (must "no removal or modification of LICENSE file") - - ; Structure - (must ".machine_readable/ directory preserved") - (must "0-AI-MANIFEST.a2ml preserved") - (must "no SCM files in repo root — only in .machine_readable/") - - ; CI - (must "no removal of CI workflows without explicit approval") - (must "all GitHub Actions SHA-pinned") - - ; Code quality - (must "tests must not be deleted or weakened") - (must "generated code in generated/ directory only") - (must "no introduction of OWASP top 10 vulnerabilities") - - ; ABI/FFI (if applicable) - (must "no modification of ABI contracts without proof update") - (must "no removal of formal verification proofs") - ) - - ; === Project-Specific Invariants === - ; *REMINDER: Add invariants specific to this repo* - ; (must "# Add project-specific invariants here") - - (enforcement - (k9-validator "contractiles/k9/must-check.k9.ncl") - (ci "quality.yml runs must-check on every PR") - ) -) diff --git a/.machine_readable/TRUST.contractile b/.machine_readable/TRUST.contractile deleted file mode 100644 index 1323caed..00000000 --- a/.machine_readable/TRUST.contractile +++ /dev/null @@ -1,80 +0,0 @@ -; SPDX-License-Identifier: PMPL-1.0-or-later -; TRUST.contractile — Trust boundaries for ephapax -; Defines what LLM/SLM agents are trusted to do without asking. -; -; Part of the contractile family: MUST, TRUST, DUST, INTENT, ADJUST - -; ── Definitions ────────────────────────────────────────────────── -; -; TRUST (noun/verb) -; The permission contractile. Defines the boundary between what an AI -; agent may do autonomously and what requires human approval. Trust is -; graduated — not binary — with four levels from minimal to maximal. -; -; Trust levels: -; - maximal: Agent may read, build, test, lint, format, heal freely. -; Only destructive/external actions require approval. -; - standard: Agent may read and build. Test/lint need approval. -; - restricted: Agent may read only. All modifications need approval. -; - minimal: Agent may read specific files only. Everything else blocked. -; -; Scope: -; TRUST governs AI agent behaviour only. It does not affect human -; contributors — humans follow CONTRIBUTING.md and GOVERNANCE.adoc. -; -; Relationship to other contractiles: -; - MUST: Trust never overrides MUST. Even at maximal trust, MUST -; violations are blocked. -; - ADJUST: Trust does not exempt from ADJUST. All trust tiers must -; produce accessible output. -; - INTENT: TRUST.trust-deny protects the sensitive areas listed in -; INTENT.ask-before-touching. -; - DUST: Deprecated features have the same trust rules as active ones. -; -; ── End Definitions ────────────────────────────────────────────── - -(trust-contractile - (version "1.0.0") - (repo "ephapax") - - (trust-level "maximal") ; maximal | standard | restricted | minimal - - ; === Maximal Trust (default) === - ; LLM may freely do these without asking: - (trust-actions - "read" ; Read any file in the repo - "build" ; Run build commands - "test" ; Run test suites - "lint" ; Run linters and formatters - "format" ; Auto-format code - "doctor" ; Run self-diagnostics - "heal" ; Attempt automatic repair - "git-status" ; Check git status - "git-diff" ; View diffs - "git-log" ; View history - ) - - ; === Denied Actions (always require human approval) === - (trust-deny - "delete-branch" ; Could lose work - "force-push" ; Overwrites history - "modify-ci-secrets" ; Security sensitive - "publish" ; External visibility - "push-to-main" ; Protected branch - "delete-files-bulk" ; More than 5 files at once - "modify-license" ; Legal implications - "modify-security-policy" ; Security implications - "remove-proofs" ; Formal verification regression - "disable-ci-checks" ; Safety regression - ) - - ; === Trust Boundary === - (trust-boundary "repo") ; LLM confined to this repo unless explicitly told otherwise - - ; === Override === - ; Repos requiring tighter trust override these settings with justification: - ; (override - ; (trust-level "restricted") - ; (reason "Contains production secrets / handles PII / etc.") - ; ) -) diff --git a/.machine_readable/agent_instructions/README.adoc b/.machine_readable/bot_directives/README.adoc similarity index 95% rename from .machine_readable/agent_instructions/README.adoc rename to .machine_readable/bot_directives/README.adoc index 0ed360be..24b1280a 100644 --- a/.machine_readable/agent_instructions/README.adoc +++ b/.machine_readable/bot_directives/README.adoc @@ -32,7 +32,7 @@ Methodology-aware configuration for AI agents. Read by any AI agent == Relationship to Other Files * `AGENTIC.a2ml` says WHAT agents can do (permissions, gating) -* `agent_instructions/` says HOW agents should work (methodology) +* `bot_directives/` says HOW agents should work (methodology) * `bot_directives/` says what the gitbot-fleet does (fleet-specific) * `CLAUDE.md` says how Claude specifically should work (Claude-specific) diff --git a/.machine_readable/agent_instructions/coverage.a2ml b/.machine_readable/bot_directives/coverage.a2ml similarity index 100% rename from .machine_readable/agent_instructions/coverage.a2ml rename to .machine_readable/bot_directives/coverage.a2ml diff --git a/.machine_readable/agent_instructions/debt.a2ml b/.machine_readable/bot_directives/debt.a2ml similarity index 100% rename from .machine_readable/agent_instructions/debt.a2ml rename to .machine_readable/bot_directives/debt.a2ml diff --git a/.machine_readable/agent_instructions/lessons.a2ml b/.machine_readable/bot_directives/lessons.a2ml similarity index 100% rename from .machine_readable/agent_instructions/lessons.a2ml rename to .machine_readable/bot_directives/lessons.a2ml diff --git a/.machine_readable/agent_instructions/methodology.a2ml b/.machine_readable/bot_directives/methodology.a2ml similarity index 100% rename from .machine_readable/agent_instructions/methodology.a2ml rename to .machine_readable/bot_directives/methodology.a2ml diff --git a/.machine_readable/contractiles/Adjustfile.a2ml b/.machine_readable/contractiles/Adjustfile.a2ml new file mode 100644 index 00000000..6f01e89f --- /dev/null +++ b/.machine_readable/contractiles/Adjustfile.a2ml @@ -0,0 +1,72 @@ +# SPDX-License-Identifier: MPL-2.0 +# Adjustfile — Drift-tolerance contract for rsr-template-repo +# Author: Jonathan D.A. Jewell +# +# Cumulative-drift catchment: tolerance bands + corrective actions. +# Authority: advisory (Yard) — continue-with-warnings; auto_fix where deterministic. +# Run with: adjust check +# Fix with: adjust fix (applies deterministic patches; advisory otherwise) + +@abstract: +Drift tolerances and corrective actions for rsr-template-repo. Unlike +MUST (hard gate), ADJUST tracks cumulative drift against tolerance bands +and proposes corrective actions. Advisory — it warns and trends, it does +not block. +@end + +## Template Drift + +### placeholder-drift +- description: Template placeholders should be replaced when copied +- tolerance: 0 placeholder markers in copied repos +- corrective: Search and replace all {{PLACEHOLDER}} markers +- severity: advisory +- notes: This check only applies to repos that copied from this template + +### template-version-drift +- description: Template version should match RSR spec version +- tolerance: Template version matches current RSR spec +- corrective: Update template to match latest RSR spec +- severity: advisory + +## Documentation Drift + +### readme-completeness +- description: README should document all template features +- tolerance: README covers all contractiles and directory structure +- corrective: Update README.adoc with missing sections +- severity: advisory + +### example-accuracy +- description: Examples in documentation should match actual template content +- tolerance: All code examples in docs are accurate +- corrective: Audit and fix examples in documentation +- severity: advisory + +## Structural Drift + +### contractile-sync +- description: All contractiles should have matching a2ml and ncl implementations +- tolerance: Every .a2ml has a corresponding .ncl +- corrective: Generate missing .ncl files from .a2ml +- severity: advisory + +### no-broken-symlinks +- description: No broken symbolic links in template structure +- tolerance: 0 broken symlinks +- corrective: Run symlink-check script +- severity: advisory + +## Accessibility Drift + +### adoc-not-md +- description: Template docs should prefer AsciiDoc +- tolerance: New prose docs are *.adoc +- corrective: Convert any new *.md to *.adoc +- severity: advisory + +### spdx-header-consistency +- description: All template files have correct SPDX headers +- tolerance: 0 files missing SPDX-License-Identifier +- corrective: Add SPDX headers to files that need them +- severity: advisory diff --git a/.machine_readable/contractiles/Intentfile.a2ml b/.machine_readable/contractiles/Intentfile.a2ml new file mode 100644 index 00000000..ef74f452 --- /dev/null +++ b/.machine_readable/contractiles/Intentfile.a2ml @@ -0,0 +1,99 @@ +# SPDX-License-Identifier: MPL-2.0 +# Intentfile (A2ML Canonical) — north-star contractile for rsr-template-repo +# Author: Jonathan D.A. Jewell +# +# Paired runner: intend.ncl +# Verb: intend +# +# Semantics: North-star contractile. Declares BOTH concrete committed +# next-actions AND horizon aspirations the project wishes to +# become. Two sections share one file because they answer +# the same question at different ranges: +# [[intents]] — "we WILL do this; track progress" +# status: declared → in_progress → done | +# deferred | retired +# [[wishes]] — "we WISH this were true; revisit later" +# status: declared → in_progress → achieved | +# abandoned +# grouped by horizon: near / mid / far. +# Non-gating — this is a report, not a gate. See the `must` +# contractile for hard gates. + +@abstract: +North-star contractile for rsr-template-repo. This repository is the +canonical template for Rhodium Standard Repository compliance. It provides +the scaffold that all hyperpolymath repos should copy and customize. +@end + +## Purpose + +The rsr-template-repo serves as the master template for all hyperpolymath +repositories. It contains the complete set of contractile files, machine-readable +specifications, and governance documentation that define the Rhodium Standard. + +Every new repository in the hyperpolymath estate should be initialized by +copying this template and substituting the placeholder values with +repo-specific content. + +## Anti-Purpose + +This repository is NOT: +- A general-purpose project scaffold for external use (hyperpolymath-only) +- A replacement for per-repo customization (all files must be bespoke) +- A static template that never changes (evolves with RSR spec) +- A runtime library or framework (build-time only) + +## If In Doubt + +If you are unsure whether a change is in scope, ask. Sensitive areas: +- .machine_readable/ contractile definitions +- RSR specification files +- Governance templates +- License policy documents + +## Committed Next-Actions + +### repo-initialization +- description: Provide just copy-and-substitute template for new repos +- probe: test -f scripts/init-repo.sh +- status: done +- notes: Run with source scripts/init-repo.sh + +### contractile-completeness +- description: Every RSR contractile has an a2ml and ncl implementation +- probe: ls .machine_readable/contractiles/*.a2ml | wc -l | grep -q "^6$" +- status: in_progress +- notes: Currently 6 contractile verbs: intend, must, trust, adjust, bust, dust + +### automation-scripts +- description: All repetitive tasks have just recipes +- probe: grep -c "^# " Justfile | grep -q "^[6-9][0-9]*$" +- status: in_progress + +## Wishes + +### Near Horizon + +#### cross-repo-validation +- description: Tooling to validate all repos against RSR spec +- horizon: near +- status: declared + +#### automated-substitution +- description: Script to automate repo-specific substitution in template +- horizon: near +- status: declared + +### Mid Horizon + +#### formal-verification +- description: Idris2 proofs for all critical contractile invariants +- horizon: mid +- status: declared + +### Far Horizon + +#### ecosystem-visualization +- description: Interactive graph of all hyperpolymath repos and dependencies +- horizon: far +- status: declared diff --git a/.machine_readable/contractiles/Justfile b/.machine_readable/contractiles/Justfile new file mode 100644 index 00000000..f96665f5 --- /dev/null +++ b/.machine_readable/contractiles/Justfile @@ -0,0 +1,185 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +# Ephapax build recipes + +# Default recipe +import? "contractile.just" + +default: build + +# Build all Rust crates +build: + cargo build + +# Build for WASM +build-wasm: + cargo build --target wasm32-unknown-unknown + +# Run all tests +test: + cargo test + +# Run conformance test suite +conformance: + cargo test --test conformance + +# Fail if proof/test counts in docs drift from repo state +status-gate: + ./scripts/status-gate.sh + +# Build Idris2 formal proofs +idris-build: + cd src/formal && idris2 --build ephapax-formal.ipkg + +# Verify Coq proofs (requires Coq 8.18+) +proofs: + cd formal && coq_makefile -f _CoqProject -o Makefile && make + +# Clean Coq build artefacts +proofs-clean: + cd formal && rm -f *.vo *.vok *.vos *.glob .*.aux Makefile .Makefile.d + +# Golden path: test + build + proofs +golden: test build proofs + +# Run panic-attack pre-commit checks +lint: + panic-attack assail + +# Run panic-attacker pre-commit scan +assail: + @command -v panic-attack >/dev/null 2>&1 && panic-attack assail . || echo "panic-attack not found — install from https://github.com/hyperpolymath/panic-attacker" + +# Format code +fmt: + cargo fmt --all + +# Check formatting without modifying +fmt-check: + cargo fmt --all --check + +# ═══════════════════════════════════════════════════════════════════════════════ +# ONBOARDING & DIAGNOSTICS +# ═══════════════════════════════════════════════════════════════════════════════ + +# Check all required toolchain dependencies and report health +doctor: + #!/usr/bin/env bash + echo "═══════════════════════════════════════════════════" + echo " Ephapax Doctor — Toolchain Health Check" + echo "═══════════════════════════════════════════════════" + echo "" + PASS=0; FAIL=0; WARN=0 + check() { + local name="$1" cmd="$2" min="$3" + if command -v "$cmd" >/dev/null 2>&1; then + VER=$("$cmd" --version 2>&1 | head -1) + echo " [OK] $name — $VER" + PASS=$((PASS + 1)) + else + echo " [FAIL] $name — not found (need $min+)" + FAIL=$((FAIL + 1)) + fi + } + check "just" just "1.25" + check "git" git "2.40" + check "Rust (cargo)" cargo "1.80" + # Optional tools + if command -v panic-attack >/dev/null 2>&1; then + echo " [OK] panic-attack — available" + PASS=$((PASS + 1)) + else + echo " [WARN] panic-attack — not found (pre-commit scanner)" + WARN=$((WARN + 1)) + fi + echo "" + echo " Result: $PASS passed, $FAIL failed, $WARN warnings" + if [ "$FAIL" -gt 0 ]; then + echo " Run 'just heal' to attempt automatic repair." + exit 1 + fi + echo " All required tools present." + +# Attempt to automatically install missing tools +heal: + #!/usr/bin/env bash + echo "═══════════════════════════════════════════════════" + echo " Ephapax Heal — Automatic Tool Installation" + echo "═══════════════════════════════════════════════════" + echo "" + if ! command -v cargo >/dev/null 2>&1; then + echo "Installing Rust via rustup..." + curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y + source "$HOME/.cargo/env" + fi + if ! command -v just >/dev/null 2>&1; then + echo "Installing just..." + cargo install just 2>/dev/null || echo "Install just from https://just.systems" + fi + echo "" + echo "Heal complete. Run 'just doctor' to verify." + +# Guided tour of the project structure and key concepts +tour: + #!/usr/bin/env bash + echo "═══════════════════════════════════════════════════" + echo " Ephapax — Guided Tour" + echo "═══════════════════════════════════════════════════" + echo "" + echo '// SPDX-License-Identifier: PMPL-1.0-or-later' + echo "" + echo "Key directories:" + echo " src/ Source code" + echo " lib/ Library modules" + echo " docs/ Documentation" + echo " tests/ Test suite" + echo " .github/workflows/ CI/CD workflows" + echo " .machine_readable/ Machine-readable metadata" + echo " examples/ Usage examples" + echo "" + echo "Quick commands:" + echo " just doctor Check toolchain health" + echo " just heal Fix missing tools" + echo " just help-me Common workflows" + echo " just default List all recipes" + echo "" + echo "Read more: README.adoc, EXPLAINME.adoc" + +# Show help for common workflows +help-me: + #!/usr/bin/env bash + echo "═══════════════════════════════════════════════════" + echo " Ephapax — Common Workflows" + echo "═══════════════════════════════════════════════════" + echo "" + echo "FIRST TIME SETUP:" + echo " just doctor Check toolchain" + echo " just heal Fix missing tools" + echo "" + echo "DEVELOPMENT:" + echo " cargo build Build the project" + echo " cargo test Run tests" + echo "" + echo "PRE-COMMIT:" + echo " just assail Run panic-attacker scan" + echo "" + echo "LEARN:" + echo " just tour Guided project tour" + echo " just default List all recipes" + + +# Print the current CRG grade (reads from READINESS.md '**Current Grade:** X' line) +crg-grade: + @grade=$$(grep -oP '(?<=\*\*Current Grade:\*\* )[A-FX]' READINESS.md 2>/dev/null | head -1); \ + [ -z "$$grade" ] && grade="X"; \ + echo "$$grade" + +# Generate a shields.io badge markdown for the current CRG grade +# Looks for '**Current Grade:** X' in READINESS.md; falls back to X +crg-badge: + @grade=$$(grep -oP '(?<=\*\*Current Grade:\*\* )[A-FX]' READINESS.md 2>/dev/null | head -1); \ + [ -z "$$grade" ] && grade="X"; \ + case "$$grade" in \ + A) color="brightgreen" ;; B) color="green" ;; C) color="yellow" ;; \ + D) color="orange" ;; E) color="red" ;; F) color="critical" ;; \ + *) color="lightgrey" ;; esac; \ + echo "[![CRG $$grade](https://img.shields.io/badge/CRG-$$grade-$$color?style=flat-square)](https://github.com/hyperpolymath/standards/tree/main/component-readiness-grades)" diff --git a/.machine_readable/contractiles/Mustfile.a2ml b/.machine_readable/contractiles/Mustfile.a2ml new file mode 100644 index 00000000..55f8ab48 --- /dev/null +++ b/.machine_readable/contractiles/Mustfile.a2ml @@ -0,0 +1,102 @@ +# SPDX-License-Identifier: MPL-2.0 +# Mustfile — Physical state contract for rsr-template-repo +# Author: Jonathan D.A. Jewell +# +# What MUST be true about this repository. Hard requirements. +# Run with: must check +# Fix with: must fix (where a deterministic fix exists) + +@abstract: +Physical-state invariants for rsr-template-repo. This is the canonical +RSR template repository. These are hard requirements — CI and pre-commit +hooks fail if any check fails. +@end + +## File Presence + +### license-present +- description: LICENSE file must exist +- run: test -f LICENSE +- severity: critical + +### readme-present +- description: README.adoc must exist +- run: test -f README.adoc +- severity: critical + +### security-policy +- description: SECURITY.md must exist +- run: test -f SECURITY.md +- severity: critical + +### ai-manifest +- description: 0-AI-MANIFEST.a2ml must exist +- run: test -f 0-AI-MANIFEST.a2ml +- severity: critical + +### governance-docs +- description: GOVERNANCE.adoc, MAINTAINERS.adoc, CODEOWNERS must exist +- run: test -f GOVERNANCE.adoc && test -f MAINTAINERS.adoc && test -f .github/CODEOWNERS +- severity: critical + +### machine-readable-dir +- description: .machine_readable/ directory must exist +- run: test -d .machine_readable +- severity: critical + +## Directory Structure + +### contractiles-complete +- description: All required contractile directories exist +- run: test -d .machine_readable/contractiles && test -d .machine_readable/contractiles/bust && test -d .machine_readable/contractiles/dust +- severity: critical + +### contractiles-files-present +- description: All four primary contractile files exist +- run: test -f .machine_readable/contractiles/Intentfile.a2ml && test -f .machine_readable/contractiles/Mustfile.a2ml && test -f .machine_readable/contractiles/Trustfile.a2ml && test -f .machine_readable/contractiles/Adjustfile.a2ml +- severity: critical + +### bust-dust-files-present +- description: Bustfile and Dustfile exist in their directories +- run: test -f .machine_readable/contractiles/bust/Bustfile.a2ml && test -f .machine_readable/contractiles/dust/Dustfile.a2ml +- severity: critical + +### six-directory-present +- description: 6a2 directory exists with required files +- run: test -d .machine_readable/6a2 && test -f .machine_readable/6a2/META.a2ml && test -f .machine_readable/6a2/ECOSYSTEM.a2ml && test -f .machine_readable/6a2/STATE.a2ml && test -f .machine_readable/6a2/PLAYBOOK.a2ml && test -f .machine_readable/6a2/AGENTIC.a2ml && test -f .machine_readable/6a2/NEUROSYM.a2ml +- severity: critical + +### anchors-directory +- description: anchors directory exists in 6a2 +- run: test -d .machine_readable/6a2/anchors +- severity: warning + +### self-validating-structure +- description: self-validating directory has k9-svc and examples +- run: test -d .machine_readable/self-validating && test -d .machine_readable/self-validating/k9-svc && test -d .machine_readable/self-validating/examples +- severity: warning + +## Template Integrity + +### no-placeholder-values +- description: No placeholder values remain in template files +- run: test -z "$(grep -r '{{' .machine_readable/contractiles/ 2>/dev/null)" +- severity: critical +- notes: All placeholders must be substituted when copying this template + +### template-readonly +- description: Template marker files are not modified +- run: grep -q 'RSR_TEMPLATE_DO_NOT_EDIT' .machine_readable/0.1-AI-MANIFEST.a2ml +- severity: warning + +## Git State + +### no-untracked-contractiles +- description: All contractile files are tracked in git +- run: test -z "$(git ls-files -o --exclude-standard .machine_readable/contractiles/ 2>/dev/null)" +- severity: critical + +### signed-commits +- description: All commits must be signed +- run: git verify-commit HEAD +- severity: critical diff --git a/.machine_readable/contractiles/Trustfile.a2ml b/.machine_readable/contractiles/Trustfile.a2ml new file mode 100644 index 00000000..e2028b56 --- /dev/null +++ b/.machine_readable/contractiles/Trustfile.a2ml @@ -0,0 +1,88 @@ +# SPDX-License-Identifier: MPL-2.0 +# Trustfile — Trust boundaries and integrity invariants for rsr-template-repo +# Author: Jonathan D.A. Jewell +# +# Defines what LLM/SLM agents are trusted to do without asking, and +# integrity invariants that verify the repo has not been tampered with. + +@abstract: +Trust boundaries and integrity checks for rsr-template-repo. This file +combines the trust-level definitions from the original TRUST.contractile +with the integrity invariants from the old Trustfile.a2ml. It defines +what AI agents may do autonomously and what requires human approval, +plus checks that verify repository integrity. +@end + +## Trust Levels + +The rsr-template-repo operates at trust level: maximal + +Trust levels: +- maximal: Agent may read, build, test, lint, format, heal freely. + Only destructive/external actions require approval. +- standard: Agent may read and build. Test/lint need approval. +- restricted: Agent may read only. All modifications need approval. +- minimal: Agent may read specific files only. Everything else blocked. + +Current trust level: maximal + +## Integrity Invariants + +### Secrets + +#### no-secrets-committed +- description: No credential files in repo +- run: test ! -f .env && test ! -f credentials.json && test ! -f .env.local && test ! -f .env.production +- severity: critical + +#### no-private-keys +- description: No private key files committed +- run: "! find . -name '*.pem' -o -name '*.key' -o -name 'id_rsa' -o -name 'id_ed25519' 2>/dev/null | grep -v node_modules | head -1 | grep -q ." +- severity: critical + +#### no-tokens-in-source +- description: No hardcoded API tokens in source +- run: "! grep -rE '(api[_-]?key|secret|token|password)\s*[:=]\s*[\"'\\''][A-Za-z0-9]{16,}' --include='*.js' --include='*.ts' --include='*.res' --include='*.py' . 2>/dev/null | grep -v node_modules | head -1 | grep -q ." +- severity: critical + +## Provenance + +#### author-correct +- description: Git author matches expected identity +- run: "git log -1 --format='%ae' | grep -qE '(hyperpolymath|j\\.d\\.a\\.jewell)'" +- severity: warning + +#### license-content +- description: LICENSE contains expected identifier +- run: grep -q 'PMPL\|MPL\|MIT\|Apache\|LGPL' LICENSE +- severity: warning + +## Template-Specific Trust + +### template-files-readonly +- description: Template scaffold files should not be modified except by maintainer +- run: test -z "$(git status --short .machine_readable/ 2>/dev/null | grep -v '^??' || true)" +- severity: advisory +- notes: Changes to template files require careful review + +### trust-deny-areas +- description: Sensitive areas from INTENT.contractile require explicit approval +- run: echo "Check .machine_readable/ contractiles and governance docs" +- severity: advisory +- areas: + - .machine_readable/ + - GOVERNANCE.adoc + - MAINTAINERS.adoc + - .github/CODEOWNERS + +## Container Security + +#### container-images-pinned +- description: Containerfile uses pinned base images +- run: test ! -f Containerfile || grep -q 'cgr.dev\|@sha256:' Containerfile +- severity: warning + +#### no-dockerfile +- description: No Dockerfile (use Containerfile) +- run: test ! -f Dockerfile +- severity: warning diff --git a/.machine_readable/contractiles/adjust/Adjustfile.a2ml b/.machine_readable/contractiles/adjust/Adjustfile.a2ml deleted file mode 100644 index 9597a430..00000000 --- a/.machine_readable/contractiles/adjust/Adjustfile.a2ml +++ /dev/null @@ -1,211 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# Adjustfile — Accessibility Contract for Burble -# Author: Jonathan D.A. Jewell -# -# Accessibility requirements and compliance for Burble. -# Voice-first design must be inclusive for all users. -# -# Run with: adjust check -# Fix with: adjust fix (where deterministic fix exists) - -@abstract: -Accessibility requirements and compliance for the Burble voice-first communications platform. -These requirements ensure Burble is usable by everyone, regardless of ability. -@end - -## Keyboard Accessibility - -### keyboard-navigation -- description: All features accessible via keyboard -- status: partial -- probe: test -f server/lib/burble/accessibility/keyboard.ex -- compliance: WCAG 2.1 AA -- notes: Basic navigation implemented. Full keyboard-only flow needed. -- fix: Port PanLL's comprehensive keyboard navigation system - -### custom-keybindings -- description: User-configurable keybindings -- status: implemented -- probe: test -f server/lib/burble/accessibility/keyboard.ex -- compliance: WCAG 2.1 AAA -- notes: Users can remap PTT, mute, deafen, volume, and room navigation keys - -### keyboard-shortcuts-discoverable -- description: Keyboard shortcuts are documented and discoverable -- status: missing -- compliance: WCAG 2.1 A -- fix: Add keyboard shortcuts help modal in web client - -## Visual Accessibility - -### high-contrast-mode -- description: High contrast UI theme -- status: missing -- compliance: WCAG 2.1 AA -- fix: Port PanLL's high-contrast theme system -- target: CSS variables for contrast ratios >= 4.5:1 - -### colorblind-support -- description: Colorblind-friendly color schemes -- status: missing -- compliance: WCAG 2.1 AA -- fix: Implement deuteranopia, protanopia, and tritanopia palettes -- reference: PanLL's palette system - -### font-size-adjustment -- description: Resizable UI fonts (4 levels: 14-20px) -- status: missing -- compliance: WCAG 2.1 AA -- fix: Port PanLL's font size adjustment system -- target: User preference persists across sessions - -### theme-switching -- description: Dark/Light/System theme support -- status: missing -- compliance: WCAG 2.1 AA -- fix: Port PanLL's theme system -- target: Respects OS preference, user override - -## Auditory Accessibility - -### screen-reader-support -- description: Full screen reader compatibility -- status: partial -- probe: test -f server/lib/burble/accessibility/screen_reader.ex -- compliance: WCAG 2.1 AA -- notes: Basic announcements implemented. Needs ARIA attributes and live regions. -- fix: Complete ARIA implementation in web client - -### closed-captions -- description: Real-time captioning for voice chat -- status: missing -- compliance: WCAG 2.1 AA -- notes: Requires Web Speech API or external STT integration -- target: 90%+ accuracy for English, configurable display - -### visual-notifications -- description: Visual indicators for audio events -- status: missing -- compliance: WCAG 2.1 A -- notes: Speaking indicators, mute status, connection status -- fix: Add visual cues that duplicate audio information - -### volume-normalization -- description: Consistent volume levels across users -- status: missing -- compliance: WCAG 2.1 AA -- notes: Prevents sudden loud sounds for sensitive users -- target: -23 LUFS normalization per EBU R128 - -## Motor Accessibility - -### voice-commands -- description: Voice-controlled interface -- status: missing -- compliance: WCAG 2.1 AAA -- notes: "Mute", "Deafen", "Join room X", "Volume up/down" -- target: Web Speech API with fallback to keyboard - -### reduced-motion -- description: Reduced animation options -- status: missing -- compliance: WCAG 2.1 AA -- fix: Port PanLL's animation control (on/reduced/off) -- target: Respects prefers-reduced-motion media query - -### hover-alternatives -- description: All hover interactions have click alternatives -- status: partial -- compliance: WCAG 2.1 AA -- notes: Some hover tooltips need click-to-show option -- fix: Audit and add click alternatives - -## Cognitive Accessibility - -### clear-language -- description: Simple, consistent terminology -- status: partial -- compliance: WCAG 2.1 AAA -- notes: Technical terms need plain language explanations -- fix: Add tooltips/glossary for jargon - -### predictable-navigation -- description: Consistent navigation patterns -- status: partial -- compliance: WCAG 2.1 AA -- notes: Navigation structure varies between pages -- fix: Standardize navigation layout - -### error-prevention -- description: Confirmation for destructive actions -- status: partial -- compliance: WCAG 2.1 AA -- notes: Room deletion has confirmation, others may not -- fix: Audit all destructive actions - -### help-availability -- description: Context-sensitive help always available -- status: missing -- compliance: WCAG 2.1 AAA -- notes: No persistent help system -- fix: Add help button with contextual guidance - -## Compliance Targets - -### wcag-2.1-aa -- description: WCAG 2.1 AA compliance -- status: partial -- target: Full compliance by Q4 2026 -- tracking: https://github.com/hyperpolymath/burble/issues/XXX - -### section-508 -- description: U.S. Section 508 compliance -- status: partial -- target: Full compliance by Q4 2026 -- notes: Aligns with WCAG 2.1 AA for most requirements - -### en-301-549 -- description: EU EN 301 549 compliance -- status: partial -- target: Full compliance by Q4 2026 -- notes: EU public sector procurement requirement - -## Integration Requirements - -### panll-accessibility-port -- description: Port PanLL's accessibility engine to Burble -- status: planned -- reference: /var/mnt/eclipse/repos/panll/tests/accessibility_engine_test.js -- target: Q2 2026 - -### k9-accessibility-validator -- description: Integrate K9 accessibility validator -- status: planned -- reference: /var/mnt/eclipse/repos/panll/contractiles/k9/validators/accessibility-baseline.k9.ncl -- target: Q2 2026 - -### accessibility-testing -- description: Add accessibility tests to CI/CD -- status: planned -- target: pa11y or axe-core integration -- compliance: Automated WCAG testing - -## Documentation Requirements - -### accessibility-guide -- description: User-facing accessibility guide -- status: missing -- target: docs/accessibility/USER-GUIDE.adoc -- notes: Keyboard shortcuts, screen reader setup, theme switching - -### developer-accessibility -- description: Developer accessibility guidelines -- status: missing -- target: docs/accessibility/DEVELOPER.adoc -- notes: Coding standards, testing requirements, compliance checklist - -### compliance-report -- description: Accessibility compliance report -- status: missing -- target: docs/compliance/ACCESSIBILITY.adoc -- notes: VPAT (Voluntary Product Accessibility Template) diff --git a/.machine_readable/contractiles/adjust/adjust.k9.ncl b/.machine_readable/contractiles/adjust/adjust.k9.ncl deleted file mode 100644 index 63cf3b15..00000000 --- a/.machine_readable/contractiles/adjust/adjust.k9.ncl +++ /dev/null @@ -1,166 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# adjust.k9.ncl — K9 trust-tier component of the adjust trident -# Author: Jonathan D.A. Jewell -# -# Pairs with: Adjustfile.a2ml (declaration) + adjust.ncl (runner). -# -# Verb: adjust (drift tolerances + corrective actions) -# Tier: Yard (validation with subprocess for measurement; -# no mutation beyond auto-fix where declared) -# Authority: advisory (continue-with-warnings; not blocking) -# -# adjust is the tolerance-band verb. Where must says "this MUST hold" -# and trust says "this MUST verify clean" (both binary), adjust says -# "drift ≤ X is acceptable; drift > X triggers action Y". Between them, -# adjust handles the subtle-drift territory that binary verbs can't. -# -# Cardinality: ONE adjust trident per repo. -# -# Failure-mode focus: adjust catches cumulative-small-drift patterns -# (E2 cosmetic churn accumulating into real regression, F2 context -# erosion causing gradual parameter drift). Where must flags "broken -# now", adjust flags "drifting toward broken". - -let base_k9 = import "../k9/template-hunt.k9.ncl" in -let base = import "../_base.ncl" in - -{ - pedigree = base_k9.pedigree_schema & { - contractile_verb = "adjust", - paired_xfile = "../adjust/Adjustfile.a2ml", - paired_runner = "../adjust/adjust.ncl", - - tier = 'Yard, - authority = 'advisory, - - metadata = { - name = "adjust-k9", - version = "1.0.0", - description = "Drift-tolerance + corrective-action runner. Fifth trident instance. First (Yard, advisory) authority pattern.", - paired_xfile = "Adjustfile.a2ml", - paired_runner = "adjust.ncl", - author = "Jonathan D.A. Jewell ", - }, - - security = { - leash = 'Yard, - trust_level = "tolerance measurement + declared auto-fix", - allow_network = false, - allow_filesystem_write_conditional = true, # auto_fix_when_available may edit - allow_subprocess = true, - probe_scope = 'measurement_plus_declared_fix, - }, - }, - - variance_schema = { - entry_id | String, - reason | String, - approved_by | String, - scope | String, - expires | String, - review_notes | String | optional, - # adjust-specific: which tolerance band the variance widens - tolerance_band_widened | String, - widened_to_value | String, - }, - - execution = { - triggers = [ 'session_close, 'on_demand, 'pre_push ], - - per_tolerance = { - measure_drift = true, - record_outcome = true, - respect_variance = true, - # adjust-specific authority: tolerance exceeded → warn, try - # auto-fix if declared, then continue. Never blocks. - on_exceeded = 'warn_and_attempt_fix, - on_auto_fix_applied = 'record_and_continue, - on_auto_fix_unavailable = 'record_as_advisory_drift, - # Cumulative-drift detection (adjust's specialty) - track_drift_trend_over_sessions = true, - flag_accelerating_drift = true, - }, - - evidence_sinks = [ - { kind = 'verisimdb, table = "contractile_executions", - schema = "contractile_execution_v1", - aux_tables = [ "adjust_drift_history" ] }, - { kind = 'drift_log, path = ".machine_readable/6a2/DRIFT.a2ml", - append_only = true }, - ], - - on_close = { - re_measure_all_tolerances = true, - diff_against_last_ratification = true, - emit_drift_entries_for_tolerance_exceeded = true, - surface_expired_variances = true, - surface_accelerating_drift = true, - # adjust is advisory — does NOT block session close. - block_session_close_on_any_drift = false, - }, - - on_open = { - render_summary = 'plain_language, - include_drift_log_from_last_close = true, - include_active_variances = true, - include_recent_anchors = true, - anchor_lookback_weeks = 8, - include_tolerance_trend_summary = true, - - negotiation = { - required = true, - ai_required_inputs = [ - 'timeline_realism, - 'industry_standards, - 'audience_feasibility, - 'resulting_invariants, - 'ecosystem_dependencies, - ], - user_engagement_required = true, - user_engagement_mode = 'per_input_response, - specification_translation = { - ai_produces_spec_form = true, - user_reviews_in_domain_language = true, - schema_authoring_is_ai_responsibility = true, - translation_faithfulness_auditable = true, - }, - }, - - accountability_pledge = { - required = true, - parties = [ - { - role = 'user, - pledge = "I have reviewed the tolerance bands and corrective actions. I accept accountability for reviewing drift warnings rather than muting them, and for re-tuning tolerances via amendment when the intended operating envelope changes.", - signature_required = true, - }, - { - role = 'ai_agent, - pledge = "I will surface tolerance breaches and accelerating-drift patterns at session close; I will propose corrective actions rather than widening tolerances silently; I will require amendment for legitimate tolerance re-tuning, not quiet band-widening.", - signature_required = true, - }, - ], - signed_record_destination = ".machine_readable/6a2/ratification-.a2ml", - must_precede_work = true, - }, - - ratification_record_shape = { - includes_negotiation_transcript = true, - includes_both_pledges = true, - includes_tolerance_bands_snapshot = true, - signed = true, - dated = true, - session_id = 'required, - contract_hash = 'required, - }, - }, - }, - - failure_mode_defenses = [ - 'A1_enthusiasm_capture, - 'C3_helpfulness_inflation, # helpful additions surfaced if they widen tolerances silently - 'C4_modernization_drift, - 'E2_cosmetic_churn, # adjust tracks cumulative churn - 'F2_context_window_erosion, # parameter drift across sessions detected - ], -} diff --git a/.machine_readable/contractiles/adjust/adjust.manifest.a2ml b/.machine_readable/contractiles/adjust/adjust.manifest.a2ml deleted file mode 100644 index ed4302ce..00000000 --- a/.machine_readable/contractiles/adjust/adjust.manifest.a2ml +++ /dev/null @@ -1,47 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# adjust.manifest.a2ml — Trident coherence manifest for the adjust verb. -# Author: Jonathan D.A. Jewell -# -# Fifth trident instance. First (Yard, advisory) authority pattern — -# complements the (Hunt, blocking) triple (must + trust + bust) and -# the (Hunt, reporting) north-star (intend). - ---- -trident_version = "1.0.0" -verb = "adjust" -semantics = "drift tolerances + corrective actions" -cardinality = "one per repo" -authority = "advisory (continue-with-warnings)" - -[[files]] -role = "declaration" -path = "Adjustfile.a2ml" -sha256 = "pending-first-verify" -size_bytes = "pending-first-verify" - -[[files]] -role = "runner" -path = "adjust.ncl" -sha256 = "pending-first-verify" -size_bytes = "pending-first-verify" - -[[files]] -role = "k9_component" -path = "adjust.k9.ncl" -sha256 = "pending-first-verify" -size_bytes = "pending-first-verify" - -[cross_refs] -runner_paired_xfile = "Adjustfile.a2ml" -k9_paired_xfile = "../adjust/Adjustfile.a2ml" -k9_paired_runner = "../adjust/adjust.ncl" - -[signed_by] -user = "Jonathan D.A. Jewell" -date = "2026-04-18" -context = "adjust trident — fifth Trident instance. First (Yard, advisory) authority pattern. Specialises in cumulative-drift catchment — tolerance bands + trend tracking + auto-fix-where-declared." - -[[history]] -date = "2026-04-18" -event = "trident-born" -note = "Adjustfile.a2ml and adjust.ncl pre-existed. This manifest + adjust.k9.ncl complete the trident. Exercises the Yard tier + advisory authority for the first time; on_exceeded = 'warn_and_attempt_fix rather than 'fail. adjust-specific track_drift_trend_over_sessions + flag_accelerating_drift." diff --git a/.machine_readable/contractiles/adjust/adjust.ncl b/.machine_readable/contractiles/adjust/adjust.ncl deleted file mode 100644 index 93168489..00000000 --- a/.machine_readable/contractiles/adjust/adjust.ncl +++ /dev/null @@ -1,62 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# Adjust — accessibility runner -# -# Pairs with: Adjustfile.a2ml (same directory) -# Verb: adjust -# Semantics: accessibility compliance (WCAG 2.1 AA baseline). Gating where -# a deterministic fix exists; advisory where human review needed. -# CLI: `contractile adjust check` → run all probes, list violations -# `contractile adjust fix` → apply deterministic fixes where defined -# -# Anything else in this directory is human-only notes/archive; machines ignore. -# -# Base: ../_base.ncl provides pedigree_schema, run_defaults, probe_schema. -# See: docs/CONTRACTILE-SPEC.adoc - -let base = import "../_base.ncl" in - -{ - pedigree = base.pedigree_schema & { - contractile_verb = "adjust", - semantics = "accessibility compliance", - security = { - leash = 'Kennel, - trust_level = "fixes allowed where deterministic", - allow_network = false, - allow_filesystem_write = true, # `adjust fix` may write (deterministic patches only) - allow_subprocess = true, - }, - metadata = { - name = "adjust-runner", - version = "1.0.0", - description = "Evaluates accessibility requirements from Adjustfile.a2ml. Fixes deterministic items; flags the rest for human review.", - paired_xfile = "Adjustfile.a2ml", - author = "Jonathan D.A. Jewell ", - }, - }, - - schema = { - requirements - | Array { - id | String, - description | String, - # TODO: migrate to base.probe_schema (structured probe) when CLI supports it - probe | String, - # status_core values: 'declared, 'verified, 'failing; adjust adds 'partial - status | [| 'declared, 'partial, 'verified, 'failing |] | default = 'declared, - compliance | String | optional, # e.g. "WCAG 2.1 AA" - notes | String | optional, - fix | String | optional, # deterministic fix command (optional) - }, - }, - - # Runner behaviour — inherits from base.run_defaults. - # adjust is advisory (continue-with-warnings) not a hard gate. - # auto_fix_when_available is adjust-specific. - run = base.run_defaults & { - on_any_fail = "continue-with-warnings", # accessibility is progress-tracked, not a hard gate by default - report_format = "a2ml", - emit_summary = true, - auto_fix_when_available = true, - }, -} diff --git a/.machine_readable/contractiles/bust/Bustfile.a2ml b/.machine_readable/contractiles/bust/Bustfile.a2ml deleted file mode 100644 index 3e80e5d9..00000000 --- a/.machine_readable/contractiles/bust/Bustfile.a2ml +++ /dev/null @@ -1,46 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# Bustfile — failure mode contractile (seed skeleton) -# Author: Jonathan D.A. Jewell -# -# Paired runner: bust.ncl -# Verb: bust -# Semantics: Every declared failure mode must have a working recovery path -# that has been exercised. Status moves: -# declared → drilled (probe run) → verified (recovery confirmed) -# or → failing (recovery broken) -# -# CLI: -# contractile bust check → list failure modes + recovery status -# contractile bust drill → inject failures, verify recovery paths -# -# ADOPTER INSTRUCTIONS: This is a seed skeleton. Replace the example failure -# modes below with the real failure modes for your project. Add one entry per -# distinct failure class you want to track and verify. Delete entries that do -# not apply. The goal is a machine-checkable map of "what can break → how we -# recover" for this specific repository. - -@abstract: -Seed Bustfile for the standards contractile template set. Lists two example -failure modes (network loss, disk full) to illustrate the shape. Adopters -should replace these with project-specific failure modes and recovery paths. -@end - -## Failure Modes - -### network-unavailable -- class: network -- description: External network becomes unavailable during a contractile probe or CI step -- injection_probe: "unshare -n true" -- recovery_probe: "ping -c 1 -W 1 127.0.0.1" -- expected_recovery_time_seconds: 5 -- status: declared -- notes: Illustrative — replace with the real network-dependent step that needs resilience - -### disk-full -- class: disk_full -- description: Disk fills to 100% during a write-heavy operation (build artefacts, test DB writes) -- injection_probe: "dd if=/dev/zero of=/tmp/bustfile-fill-test bs=1M count=1 && rm /tmp/bustfile-fill-test" -- recovery_probe: "df -h / | awk 'NR==2 { gsub(/%/,\"\"); if ($5 < 95) exit 0; else exit 1 }'" -- expected_recovery_time_seconds: 30 -- status: declared -- notes: Illustrative — replace with the real disk-intensive operation and its recovery path diff --git a/.machine_readable/contractiles/bust/bust.ncl b/.machine_readable/contractiles/bust/bust.ncl deleted file mode 100644 index 3d9ab8b1..00000000 --- a/.machine_readable/contractiles/bust/bust.ncl +++ /dev/null @@ -1,66 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# Bust — error-handling / failure-recovery runner -# -# Pairs with: Bustfile.a2ml (same directory) -# Verb: bust -# Semantics: every declared failure mode must have a recovery path that has -# been exercised. Runner injects failures (via declared probes) -# and verifies the recovery path works. Hard gate on any -# failure-mode with missing or broken recovery. -# CLI: `contractile bust check` → list failure modes + recovery status -# `contractile bust drill` → inject declared failures, verify recovery -# -# Anything else in this directory is human-only notes/archive; machines ignore. -# -# Base: ../_base.ncl provides pedigree_schema, run_defaults, probe_schema. -# See: docs/CONTRACTILE-SPEC.adoc - -let base = import "../_base.ncl" in - -{ - pedigree = base.pedigree_schema & { - contractile_verb = "bust", - semantics = "error handling + failure recovery", - security = { - leash = 'Kennel, - trust_level = "controlled failure injection; scoped to system-under-test", - allow_network = false, - allow_filesystem_write = true, # drills may write transient state (tmp dirs, test DBs) - allow_subprocess = true, - injection_scope = "system-under-test-only", - }, - metadata = { - name = "bust-runner", - version = "1.0.0", - description = "Exercises declared failure modes and verifies recovery paths. Hard-gates on any failure mode without working recovery.", - paired_xfile = "Bustfile.a2ml", - author = "Jonathan D.A. Jewell ", - }, - }, - - schema = { - failure_modes - | Array { - id | String, - description | String, - class | [| 'network, 'disk_full, 'oom, 'timeout, 'partial_write, 'panic, 'crash, 'rollback, 'concurrency |], - # TODO: migrate to base.probe_schema (structured probe) when CLI supports it - injection_probe | String, # command that deterministically causes this failure - # TODO: migrate to base.probe_schema (structured probe) when CLI supports it - recovery_probe | String, # command that verifies recovery (exit 0 = recovered) - expected_recovery_time_seconds | Number | default = 30, - # status_core values: 'declared, 'verified, 'failing; bust adds 'drilled - status | [| 'declared, 'drilled, 'verified, 'failing |] | default = 'declared, - notes | String | optional, - }, - }, - - # Runner behaviour — inherits from base.run_defaults. - # bust adds record_recovery_times for performance tier feeding. - run = base.run_defaults & { - on_any_fail = "exit-nonzero", # missing or broken recovery blocks merge - report_format = "a2ml", - emit_summary = true, - record_recovery_times = true, # feeds the performance tier - }, -} diff --git a/.machine_readable/contractiles/dust/Dustfile.a2ml b/.machine_readable/contractiles/dust/Dustfile.a2ml deleted file mode 100644 index ad6fb607..00000000 --- a/.machine_readable/contractiles/dust/Dustfile.a2ml +++ /dev/null @@ -1,78 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# Dustfile — Cleanup and hygiene contract for Burble -# Author: Jonathan D.A. Jewell -# -# What should be cleaned up. Housekeeping, not blockers. -# Run with: dust status -# Roll back with: dust rollback - -@abstract: -Cleanup and hygiene items for the Burble voice platform. -These are maintenance tasks — not blocking, but should be addressed. -@end - -## Stale Files - -### no-stale-snapshots -- description: No dated status/completion files in root -- run: test -z "$(ls *-STATUS-*.md *-COMPLETION-*.md 2>/dev/null)" -- severity: info - -### no-ai-djot -- description: AI.djot is superseded by 0-AI-MANIFEST.a2ml -- run: test ! -f AI.djot -- severity: warning - -### no-next-steps -- description: NEXT_STEPS.md superseded by ROADMAP -- run: test ! -f NEXT_STEPS.md -- severity: info - -## Build Artifacts - -### no-tracked-elixir-build -- description: No Elixir build artifacts tracked in git -- run: test -z "$(git ls-files server/_build/ server/deps/ 2>/dev/null)" -- severity: warning - -### no-tracked-rescript-build -- description: No ReScript build artifacts tracked in git -- run: test -z "$(git ls-files 'client/web/src/**/*.res.mjs' client/web/lib/ 2>/dev/null)" -- severity: warning - -## Burble-Specific Cleanup - -### stale-room-processes -- description: Room processes should auto-terminate after idle timeout -- verification: Burble.Rooms.Room uses @idle_timeout_ms (5 minutes) -- severity: info -- notes: Not a file check — design verification that idle rooms are cleaned up - -### expired-invite-tokens -- description: Expired invite tokens should be purged periodically -- verification: Scheduled task purges tokens past expires_at -- severity: info -- notes: Planned — not yet implemented - -### orphaned-turn-credentials -- description: TURN credentials expire after 1 hour -- verification: Burble.Media.Privacy.generate_turn_credential sets TTL -- severity: info - -### template-example-trustfile -- description: Remove the example Trustfile (keep only the real one) -- run: test ! -f .machine_readable/contractiles/trust/Trustfile_just_an_example.a2ml -- severity: info -- rollback: git checkout HEAD -- .machine_readable/contractiles/trust/Trustfile_just_an_example.a2ml - -## Format Duplicates - -### no-duplicate-contributing -- description: Only one CONTRIBUTING format -- run: test -z "$(test -f CONTRIBUTING.md && test -f CONTRIBUTING.adoc && echo dup)" -- severity: warning - -### no-duplicate-readme -- description: Only one README format -- run: test ! -f README.md || test ! -f README.adoc -- severity: warning diff --git a/.machine_readable/contractiles/dust/dust.ncl b/.machine_readable/contractiles/dust/dust.ncl deleted file mode 100644 index 894634ae..00000000 --- a/.machine_readable/contractiles/dust/dust.ncl +++ /dev/null @@ -1,66 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# Dust — exnovation / code-removal runner -# -# Pairs with: Dustfile.a2ml (same directory) -# Verb: dust -# Semantics: exnovation. Identifies code, docs, files, dependencies that are -# candidates for REMOVAL. Advisory by default; can be flipped to -# active delete via `contractile dust sweep --apply`. -# CLI: `contractile dust find` → list removal candidates -# `contractile dust sweep` → dry-run removals -# `contractile dust sweep --apply` → actually delete (gated) -# -# Anything else in this directory is human-only notes/archive; machines ignore. -# -# Base: ../_base.ncl provides pedigree_schema, run_defaults, probe_schema. -# See: docs/CONTRACTILE-SPEC.adoc - -let base = import "../_base.ncl" in - -{ - pedigree = base.pedigree_schema & { - contractile_verb = "dust", - semantics = "exnovation / removal", - security = { - leash = 'Kennel, - trust_level = "proposes deletion; --apply required to execute", - allow_network = false, - allow_filesystem_write = true, # --apply mode writes (deletes) - allow_subprocess = true, - destructive_mode_requires_flag = "--apply", - }, - metadata = { - name = "dust-runner", - version = "1.0.0", - description = "Identifies and optionally removes exnovation targets listed in Dustfile.a2ml. Destructive mode gated behind --apply.", - paired_xfile = "Dustfile.a2ml", - author = "Jonathan D.A. Jewell ", - }, - }, - - schema = { - removal_candidates - | Array { - id | String, - description | String, - target | String, # file / path / symbol / dep name - reason | String, # why it's a removal candidate - # TODO: migrate to base.probe_schema (structured probe) when CLI supports it - probe | String | optional, # command that confirms it's still removable - # dust has a non-standard status progression (no 'verified): - # 'declared → 'proposed → 'approved → 'removed - status | [| 'declared, 'proposed, 'approved, 'removed |] | default = 'declared, - approver | String | optional, # who signed off (for 'approved / 'removed) - notes | String | optional, - }, - }, - - # Runner behaviour — inherits from base.run_defaults. - # dust is advisory; apply_requires_approval is dust-specific. - run = base.run_defaults & { - on_any_fail = "continue-with-warnings", - report_format = "a2ml", - emit_summary = true, - apply_requires_approval = true, # only 'approved items get swept, even with --apply - }, -} diff --git a/.machine_readable/contractiles/intend/Intentfile.a2ml b/.machine_readable/contractiles/intend/Intentfile.a2ml deleted file mode 100644 index 020c8576..00000000 --- a/.machine_readable/contractiles/intend/Intentfile.a2ml +++ /dev/null @@ -1,123 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# Intentfile (A2ML Canonical) — north-star contractile -# Author: Jonathan D.A. Jewell -# -# Paired runner: intend.ncl -# Verb: intend -# Semantics: North-star contractile. Declares BOTH concrete committed -# next-actions AND horizon aspirations the project wishes to -# become. Two sections share one file because they answer -# the same question at different ranges: -# [[intents]] — "we WILL do this; track progress" -# status: declared → in_progress → done | -# deferred | retired -# [[wishes]] — "we WISH this were true; revisit later" -# status: declared → in_progress → achieved | -# abandoned -# grouped by horizon: near / mid / far. -# Non-gating — this is a report, not a gate. See the `must` -# contractile for hard gates. -# -# History: The `lust/` sibling contractile was deprecated 2026-04-18; -# its `[[wishes]]` semantics were absorbed here so the -# project's aspirational horizon and its committed -# next-actions live together in one north-star view. -# -# CLI: -# contractile intend run → print status table (both sections) -# contractile intend progress → diff declared-vs-observed for intents -# contractile intend horizon → group wishes by near/mid/far -# -# ADOPTER INSTRUCTIONS: Replace the example intents and wishes below with -# project-specific content. Each intent should have a probe command that -# returns exit 0 when the intent is done. Wishes are report-only and never -# run a probe. Omit either section if not applicable; don't delete the file. - -@abstract: -Seed Intentfile for the standards contractile template set. Demonstrates -both sections: concrete intents with probes and horizon-grouped wishes. -Adopters should replace these with real project commitments and aspirations. -@end - -## Purpose - -The standards contractile template set commits to the intents declared -below and points at the wishes on the horizon. The primary goal is to -keep the contractile system complete, documented, and machine-verifiable -so repos copying this template inherit a working operational framework. - -## Anti-Purpose - -This Intentfile is NOT: -- A feature roadmap (that belongs in the project ROADMAP.adoc) -- A hard gate (intend never blocks; see the `must` contractile for gates) - -## If In Doubt - -If you are unsure whether a change is in scope, ask. Sensitive areas: -ABI definitions, license headers, CI workflows. - -## Committed Next-Actions - -[[intents]] -id = "contractile-spec-written" -description = "CONTRACTILE-SPEC.adoc normative spec exists and is up-to-date" -probe = "test -f docs/CONTRACTILE-SPEC.adoc" -status = "done" -notes = "Spec written and committed 2026-04-17" - -[[intents]] -id = "base-ncl-extracted" -description = "_base.ncl shared contractile base extracted and all 6 active verb runners import it" -probe = "grep -l 'import.*_base.ncl' .machine_readable/contractiles/must/must.ncl .machine_readable/contractiles/trust/trust.ncl .machine_readable/contractiles/bust/bust.ncl .machine_readable/contractiles/adjust/adjust.ncl .machine_readable/contractiles/dust/dust.ncl .machine_readable/contractiles/intend/intend.ncl | wc -l | xargs test 6 -eq" -status = "done" -notes = "Base extracted and all runners refactored 2026-04-17; lust/ deprecated 2026-04-18, count reduced 7→6." - -[[intents]] -id = "index-registry-present" -description = "INDEX.a2ml registry listing all active verbs exists in the contractiles directory" -probe = "test -f .machine_readable/contractiles/INDEX.a2ml" -status = "done" -notes = "Registry created 2026-04-17" - -[[intents]] -id = "lust-dir-retired" -description = "Deprecated lust/ dir removed; wishes semantics absorbed into Intentfile" -probe = "! test -d .machine_readable/contractiles/lust" -status = "done" -notes = "Retired 2026-04-18 per user direction — name had negative associations; north-star meaning always belonged here." - -[[intents]] -id = "probe-schema-migration" -description = "All verb runner files migrate probe fields from String to structured probe_schema" -probe = "! grep -r 'probe | String' .machine_readable/contractiles/ --include='*.ncl'" -status = "declared" -notes = "DEFERRED — breaking change requiring CLI support. Legacy String probes kept with TODO comments. See CONTRACTILE-SPEC.adoc Migration Notes." -target_date = "2026-Q3" - -## Horizon Aspirations (wishes) - -# Wishes are non-probeable project horizons. They exist to make the -# aspiration axis visible without polluting the commitment queue. - -[[wishes]] -id = "example-near-wish" -description = "Describe one aspirational feature/property the project intends toward in the near term" -horizon = "near" -why = "Why this would matter; the value of it being true" -status = "declared" -notes = "Optional human notes; leave empty or delete" - -[[wishes]] -id = "example-mid-wish" -description = "Aspirational item on the one-to-two release horizon" -horizon = "mid" -why = "The impact of reaching it" -status = "declared" - -[[wishes]] -id = "example-far-wish" -description = "Multi-year horizon state" -horizon = "far" -why = "Why we still bother pointing at it" -status = "declared" diff --git a/.machine_readable/contractiles/intend/intend.k9.ncl b/.machine_readable/contractiles/intend/intend.k9.ncl deleted file mode 100644 index 3ce01d55..00000000 --- a/.machine_readable/contractiles/intend/intend.k9.ncl +++ /dev/null @@ -1,250 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# intend.k9.ncl — K9 trust-tier component of the intend trident -# Author: Jonathan D.A. Jewell -# -# Pairs with: Intentfile.a2ml (declaration) + intend.ncl (runner). -# Trident completeness is a hard precondition — a repo shipping -# Intentfile without this file AND its runner is an invalid trident; -# the contractile CLI's verify gate refuses partial publication. -# -# Verb: intend (north star — commitments + aspirations) -# Tier: Hunt (capability: subprocess probes may shell out) -# Authority: reporting (never blocks; drift-log only) -# -# Cardinality: ONE intend trident per repo (see feedback_contractile_ -# layout_rules.md). ANCHOR.a2ml is the sole multi-instance exception — -# it is NOT a verb contractile. -# -# Design commitments baked in (see memory trail 2026-04-18 for full -# context; key files referenced by name in annotations below): -# * α two-axis (tier × authority) — structurally separate capability -# from authority so "Hunt tier = can override" is impossible. -# * Variance schema first-class, not comment markers -# (feedback_audit_tool_suppression_design.md — structural > markers). -# * Sessional drift detection hooks (on_close, on_open). -# * Ratification at session open; drift log at session close. -# * Evidence sinks: VeriSimDB (queryable) + 6a2/DRIFT.a2ml (repo-local). -# * Failure-mode defenses cross-referenced to the AI failure catalog. - -let base_k9 = import "../k9/template-hunt.k9.ncl" in -let base = import "../_base.ncl" in - -{ - pedigree = base_k9.pedigree_schema & { - contractile_verb = "intend", - paired_xfile = "../intend/Intentfile.a2ml", - paired_runner = "../intend/intend.ncl", - - # α two-axis declaration — capability × authority. - # intend is Hunt-capable (probes shell out) but reporting-authority - # (never blocks). must/trust/bust will declare (Hunt, blocking); - # adjust/dust will declare (Yard, advisory). Splitting the axes - # means "I'm Hunt-tier so I can override everything" is structurally - # impossible — authority is a separate field. - tier = 'Hunt, - authority = 'reporting, - - metadata = { - name = "intend-k9", - version = "2.0.0", # 1.0.0 (2026-04-18 AM): initial trident. - # 2.0.0 (2026-04-18 PM): negotiation + - # accountability + plain-language-translation - # schema baked into on_open — prerequisite for - # the adversarial Gemini+Copilot drift pilot. - description = "Executes Intentfile probes + emits drift log. Non-gating; reporting authority only. on_open hook implements negotiation-ratification-accountability protocol.", - paired_xfile = "Intentfile.a2ml", - paired_runner = "intend.ncl", - author = "Jonathan D.A. Jewell ", - }, - - security = { - leash = 'Hunt, - trust_level = "subprocess + filesystem-read", - allow_network = false, - allow_filesystem_write = false, # evidence sinks are indirected - allow_subprocess = true, - }, - }, - - # ------------------------------------------------------------------- - # Variance schema — P-shape scoped exceptions per entry. - # A variance suppresses a specific intent's or wish's obligation for a - # reason, with approver + expiry. Expired variance = effective - # re-imposition of the obligation. Unmet intent without a variance = - # drift, logged to the drift log. - # Per user 2026-04-18: variances are structural, not magic-comment - # markers — markers are gameable. - # ------------------------------------------------------------------- - variance_schema = { - entry_id | String, # which intent/wish id the variance applies to - reason | String, - approved_by | String, - scope | String, # path glob | session-id | "until-" - expires | String, # absolute date or condition - review_notes | String | optional, - }, - - # ------------------------------------------------------------------- - # Execution policy - # ------------------------------------------------------------------- - execution = { - # When the component runs. - # session_close is mandatory (the "picked up sessionally" check). - triggers = [ 'session_close, 'on_demand, 'pre_push ], - - # Per-intent execution. - per_intent = { - run_probe = true, - record_outcome = true, - respect_variance = true, # active variance suppresses failure - on_unmet = 'log_drift, # never 'fail — authority = reporting - }, - - # Per-wish execution (wishes are non-probeable; horizon-group only). - per_wish = { - run_probe = false, - emit_horizon_summary = true, - # Vertical alignment soft-check per user_6a2_is_contractile_ought.md: - # highest-level alignment is meta ↔ north-star (soft), not hard gate. - check_alignment_with_META = true, - }, - - # Evidence sinks — BOTH written, every execution. - # VeriSimDB = queryable machine record (feedback_verisimdb_policy.md). - # 6a2/DRIFT.a2ml = repo-local append-only drift log (feedback_sessional_ - # drift_detection.md + user_6a2_is_contractile_ought.md descriptive role). - evidence_sinks = [ - { - kind = 'verisimdb, - table = "contractile_executions", - schema = "contractile_execution_v1", - }, - { - kind = 'drift_log, - path = ".machine_readable/6a2/DRIFT.a2ml", - append_only = true, - }, - ], - - # Session-close hook — the "picked up sessionally" requirement. - # Re-execute, diff against the last ratification, surface expired - # variances, emit drift entries for new failures. - on_close = { - re_execute_all_intents = true, - diff_against_last_ratification = true, - emit_drift_entries_for_new_failures = true, - surface_expired_variances = true, - }, - - # ----------------------------------------------------------------- - # Session-open hook — NEGOTIATION + RATIFICATION + ACCOUNTABILITY - # (user_contract_negotiation_and_accountability_pledge.md) - # (user_contractiles_agreed_at_session_start.md) - # - # Ratification is not passive acknowledgement; it is negotiation - # ending in an explicit accountability pledge from BOTH parties. - # Work cannot proceed before both pledges are on file. - # ----------------------------------------------------------------- - on_open = { - # --- Context presentation (pre-negotiation) --- - render_summary = 'plain_language, # metaphor-capture defense - include_drift_log_from_last_close = true, - include_active_variances = true, - include_recent_anchors = true, - anchor_lookback_weeks = 8, - - # --- Negotiation phase (five mandatory inputs) --- - # AI must surface all five before the user is asked to ratify. - # "Yes, and …" — not "yes". Missing any of the five = the - # negotiation is incomplete and work cannot proceed. - negotiation = { - required = true, # blank-cheque ratification refused - - # The five inputs the AI must contribute to the negotiation. - # Each is a structured field the agent is required to populate, - # not optional prose. See user_contract_negotiation_and_ - # accountability_pledge.md for the domain-language-rendering rule. - ai_required_inputs = [ - 'timeline_realism, # "this will take X; not Y" - 'industry_standards, # WCAG, ISO, OWASP, GDPR, licensing … - 'audience_feasibility, # real addressable user set - 'resulting_invariants, # what must/trust/adjust entries follow - 'ecosystem_dependencies, # libs, licences, threat-model implications - ], - - # User must actually engage with each input — not - # auto-approve. If user tries to skip ("just do it, I trust you") - # the system re-renders the obligations and requires the pledge. - user_engagement_required = true, - user_engagement_mode = 'per_input_response, - - # The AI does the specification-form work. The user reviews the - # rendering in domain language and accepts / amends / pushes back. - # User never has to author Nickel schemas or decide on type - # specificity — that is the AI's translation responsibility, - # with auditable faithfulness. - specification_translation = { - ai_produces_spec_form = true, - user_reviews_in_domain_language = true, - schema_authoring_is_ai_responsibility = true, - translation_faithfulness_auditable = true, - # Failure mode this closes: user is forced to learn spec-theory - # (type refinement, Nickel contract grammar) to ratify a contract - # — which drives users away from ratification entirely. - }, - }, - - # --- Accountability pledge (both parties, explicit) --- - # Not "I read it" — "I am answerable for this obligation". - # Both pledges are required before work proceeds; both are recorded. - accountability_pledge = { - required = true, - parties = [ - { - role = 'user, - pledge = "I have reviewed the obligations as negotiated; I accept accountability for meeting the declared invariants and for the audience/timeline/standards consequences surfaced in negotiation.", - signature_required = true, - }, - { - role = 'ai_agent, - pledge = "I will hold the user to the obligations as negotiated, including by surfacing drift at session close and refusing off-contract actions, even when the user is enthusiastic about them. If the user wishes to depart from the contract, I will require a variance or amendment, not silent acceptance.", - signature_required = true, - # Per user_contractile_is_contract_do_not_break.md — - # the AI is the holder of the line against enthusiasm drift. - }, - ], - signed_record_destination = ".machine_readable/6a2/ratification-.a2ml", - must_precede_work = true, - }, - - # --- Policy: ratification output --- - # The ratification record IS the negotiation transcript + the - # accountability pledge combined. One document; future-session - # ground-truth for "what was agreed, who is accountable". - ratification_record_shape = { - includes_negotiation_transcript = true, - includes_both_pledges = true, - signed = true, - dated = true, - session_id = 'required, - contract_hash = 'required, # pins what was actually signed - }, - }, - }, - - # ------------------------------------------------------------------- - # Failure-mode defenses — explicit cross-reference to the catalog - # (feedback_ai_failure_mode_catalog.md). New catalog entries that - # shift this verb's defenses must update this list, not narrative. - # ------------------------------------------------------------------- - failure_mode_defenses = [ - 'A1_enthusiasm_capture, # scope breach → drift log - 'A2_metaphor_capture, # render_summary = 'plain_language - 'A3_allegory_drift, # intents cite concrete obligations - 'C1_scope_creep, # feature-adjacent change needs intent_id - 'C3_helpfulness_inflation, # changes without intent_id flagged - 'C4_modernization_drift, # upgrade cannot cite intent → drift - 'D5_sycophancy, # ratification compares user framing vs contract - 'F1_across_session_forgetting, # on_open reads last-ratification record - ], -} diff --git a/.machine_readable/contractiles/intend/intend.manifest.a2ml b/.machine_readable/contractiles/intend/intend.manifest.a2ml deleted file mode 100644 index a83af622..00000000 --- a/.machine_readable/contractiles/intend/intend.manifest.a2ml +++ /dev/null @@ -1,73 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# intend.manifest.a2ml — Trident coherence manifest for the intend verb. -# Author: Jonathan D.A. Jewell -# -# Asserts: exactly three files constitute the intend trident; their -# content-hashes are pinned here; cross-references round-trip; no -# partial publication is permitted. -# -# The contractile CLI's `verify ` subcommand MUST: -# 1. Confirm all three listed files exist at the declared paths. -# 2. Compute each file's sha256 and match against the pinned value. -# 3. Follow each cross-reference and confirm the target file's -# reciprocal field points back. -# 4. Refuse the dir (exit non-zero) if any of 1–3 fails. -# -# This forecloses the failure mode where an agent publishes an A2ML -# declaration with no paired runner or K9 component — the trident is -# atomically complete or it is invalid. - ---- -trident_version = "1.0.0" -verb = "intend" -semantics = "north-star (commitments + aspirations)" -cardinality = "one per repo" - -## Files (three; exactly) - -[[files]] -role = "declaration" -path = "Intentfile.a2ml" -sha256 = "pending-first-verify" # populated on first `contractile verify intend` -size_bytes = "pending-first-verify" - -[[files]] -role = "runner" -path = "intend.ncl" -sha256 = "pending-first-verify" -size_bytes = "pending-first-verify" - -[[files]] -role = "k9_component" -path = "intend.k9.ncl" -sha256 = "pending-first-verify" -size_bytes = "pending-first-verify" - -## Cross-references (must round-trip) - -[cross_refs] -# Each runner/K9 component names its paired files; the CLI follows the -# links and asserts reciprocity. Any dangling or mismatched reference -# fails the verify gate. -runner_paired_xfile = "Intentfile.a2ml" -k9_paired_xfile = "../intend/Intentfile.a2ml" -k9_paired_runner = "../intend/intend.ncl" - -## Trident signing - -[signed_by] -user = "Jonathan D.A. Jewell" -date = "2026-04-18" -context = "intend trident pilot — first Trident instance in the estate; template for the remaining 5 verbs (must/trust/bust/adjust/dust) and for the 14 template-copy dirs." - -## Change log - -[[history]] -date = "2026-04-18" -event = "trident-born" -note = "intend/Intentfile.a2ml pre-existed (f380b62, lust absorption). This manifest + intend.k9.ncl complete the trident for the first time." - -[[history]] -date = "2026-04-18" -event = "negotiation-accountability-schema-landed" -note = "intend.k9.ncl on_open hook extended: five negotiation inputs (timeline/standards/audience/invariants/dependencies), both-parties accountability pledge, plain-language-translation policy (AI authors spec form, user reviews in domain language). K9 metadata version bumped 1.0.0 → 2.0.0. Prerequisite for the adversarial Gemini+Copilot drift pilot; intend is the hardest verb (abstract north-star) so baking the full protocol here first means simpler verbs (trust, must) can inherit the template." diff --git a/.machine_readable/contractiles/intend/intend.ncl b/.machine_readable/contractiles/intend/intend.ncl deleted file mode 100644 index aa17d53a..00000000 --- a/.machine_readable/contractiles/intend/intend.ncl +++ /dev/null @@ -1,81 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# Intend — north-star runner (verb is `intend`, file is `Intentfile.a2ml`) -# -# Pairs with: Intentfile.a2ml (same directory) -# Verb: intend -# Semantics: Declares BOTH concrete committed next-actions ([[intents]]) and -# horizon aspirations ([[wishes]]). Not a gate — reports progress -# toward declared intents and lists wishes by horizon. -# Status progressions: -# intents: 'declared → 'in_progress → 'done | 'deferred | 'retired -# wishes: 'declared → 'in_progress → 'achieved | 'abandoned -# CLI: `contractile intend run` → print status table (both sections) -# `contractile intend progress` → diff declared-vs-observed (intents) -# `contractile intend horizon` → group wishes by near/mid/far -# -# History: Absorbed the deprecated `lust` contractile's [[wishes]] schema -# 2026-04-18. `lust/` dir removed estate-wide. -# -# Anything else in this directory is human-only notes/archive; machines ignore. -# -# Base: ../_base.ncl provides pedigree_schema, run_defaults, probe_schema. -# See: docs/CONTRACTILE-SPEC.adoc - -let base = import "../_base.ncl" in - -{ - pedigree = base.pedigree_schema & { - contractile_verb = "intend", - semantics = "north-star (commitments + aspirations)", - security = { - leash = 'Kennel, - trust_level = "read-only reporting", - allow_network = false, - allow_filesystem_write = false, - allow_subprocess = true, # probe commands may shell out (intents only; wishes never probe) - }, - metadata = { - name = "intend-runner", - version = "2.0.0", - description = "Reports progress toward committed next-actions and lists horizon aspirations. Non-gating. Absorbed `lust` semantics 2026-04-18.", - paired_xfile = "Intentfile.a2ml", - author = "Jonathan D.A. Jewell ", - }, - }, - - schema = { - intents - | Array { - id | String, - description | String, - # TODO: migrate to base.probe_schema (structured probe) when CLI supports it - probe | String | optional, # shell command that indicates done-ness - status | [| 'declared, 'in_progress, 'done, 'deferred, 'retired |] | default = 'declared, - notes | String | optional, - target_date | String | optional, - }, - wishes - | Array { - id | String, - description | String, - horizon | [| 'near, 'mid, 'far |] | default = 'mid, - why | String | optional, - status | [| 'declared, 'in_progress, 'achieved, 'abandoned |] | default = 'declared, - notes | String | optional, - } - | optional, - }, - - # Runner behaviour — inherits from base.run_defaults. - # intend never blocks; it is a report only. - # emit_diff is intent-specific (declared vs observed probes). - # emit_grouped_by_horizon renders wishes grouped by near/mid/far. - run = base.run_defaults & { - on_pass = "continue", - on_any_fail = "continue", # never blocks; it's a report - report_format = "a2ml", - emit_summary = true, - emit_diff = true, # declared vs observed (intents) - emit_grouped_by_horizon = true, # wishes grouped by horizon (absorbed from lust) - }, -} diff --git a/.machine_readable/contractiles/must/Mustfile.a2ml b/.machine_readable/contractiles/must/Mustfile.a2ml deleted file mode 100644 index 275ff336..00000000 --- a/.machine_readable/contractiles/must/Mustfile.a2ml +++ /dev/null @@ -1,144 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# Mustfile — Physical state contract for Burble -# Author: Jonathan D.A. Jewell -# -# What MUST be true about this repository. Hard requirements. -# Run with: must check -# Fix with: must fix (where deterministic fix exists) - -@abstract: -Physical state invariants for the Burble voice platform. -These are hard requirements — CI and pre-commit hooks fail if any check fails. -@end - -## File Presence - -### license-present -- description: LICENSE file must exist -- run: test -f LICENSE -- severity: critical - -### readme-present -- description: README.adoc must exist -- run: test -f README.adoc -- severity: critical - -### security-policy -- description: SECURITY.md must exist -- run: test -f SECURITY.md -- severity: critical - -### ai-manifest -- description: 0-AI-MANIFEST.a2ml must exist -- run: test -f 0-AI-MANIFEST.a2ml -- severity: critical - -### contributing -- description: CONTRIBUTING guide must exist -- run: test -f CONTRIBUTING.adoc || test -f .github/CONTRIBUTING.md -- severity: warning - -### editorconfig -- description: .editorconfig must exist -- run: test -f .editorconfig -- severity: warning - -## Elixir Server - -### mix-exs-present -- description: Elixir mix.exs must exist in server/ -- run: test -f server/mix.exs -- severity: critical - -### elixir-compiles -- description: Elixir server compiles without errors -- run: test -f server/mix.exs -- severity: critical -- notes: Full compile check via CI (mix compile), file presence check here - -### ecto-migrations-exist -- description: Database migrations directory exists -- run: test -d server/priv/repo/migrations -- severity: critical - -### config-files-present -- description: All config files exist -- run: test -f server/config/config.exs && test -f server/config/dev.exs && test -f server/config/prod.exs && test -f server/config/runtime.exs -- severity: critical - -## Web Client - -### rescript-json-present -- description: ReScript config exists for web client -- run: test -f client/web/rescript.json -- severity: warning - -### web-entry-point -- description: Web client entry point exists -- run: test -f server/priv/static/index.html || test -f client/web/index.html -- severity: warning - -## SPDX Compliance - -### spdx-elixir -- description: All Elixir files have SPDX header -- run: test -z "$(find server/lib -name '*.ex' -exec head -1 {} \; 2>/dev/null | grep -cv 'SPDX' | grep -v '^0$')" -- severity: warning - -### no-agpl -- description: No AGPL-3.0 references (replaced by PMPL) -- run: test -z "$(grep -rl 'AGPL-3.0' LICENSE .editorconfig .gitattributes 2>/dev/null)" -- severity: critical - -## Dangerous Patterns - -### no-believe-me -- description: No believe_me in Idris2 code -- run: test -z "$(find . -name '*.idr' -not -path '*/deps/*' -exec grep -l 'believe_me' {} \; 2>/dev/null)" -- severity: critical - -### no-unsafe-coerce -- description: No unsafeCoerce in ReScript/Haskell code -- run: test -z "$(find . \( -name '*.res' -o -name '*.hs' \) -not -path '*/deps/*' -not -path '*/node_modules/*' -exec grep -l 'unsafeCoerce\|Obj.magic' {} \; 2>/dev/null)" -- severity: critical - -## Container Policy - -### containerfile-not-dockerfile -- description: Uses Containerfile, not Dockerfile -- run: test -z "$(find . -name 'Dockerfile' -not -path '*/.clusterfuzzlite/*' 2>/dev/null)" -- severity: warning - -### no-docker-commands -- description: No docker commands in scripts (use podman) -- run: test -z "$(grep -rl 'docker run\|docker build\|docker compose' --include='*.sh' --include='*.yml' . 2>/dev/null | grep -v deps | grep -v node_modules)" -- severity: warning - -## Language Policy - -### no-typescript -- description: No TypeScript files (use ReScript) -- run: test -z "$(find . -name '*.ts' -not -name '*.d.ts' -not -path '*/deps/*' -not -path '*/node_modules/*' 2>/dev/null)" -- severity: warning - -### no-python -- description: No Python files (use Julia/Rust/ReScript) -- run: test -z "$(find . -name '*.py' -not -path '*/deps/*' -not -path '*/node_modules/*' 2>/dev/null)" -- severity: warning - -## Security - -### no-secrets-in-config -- description: No hardcoded secrets in Elixir config -- run: test -z "$(grep -rE '(secret_key_base|password).*=\"[A-Za-z0-9+/]{32,}\"' server/config/ 2>/dev/null | grep -v 'dev_only\|test_only')" -- severity: critical - -### beam-cookie-absent -- description: No Erlang cookie in repository -- run: test -z "$(find . -name '.erlang.cookie' 2>/dev/null)" -- severity: critical - -### env-files-absent -- description: No .env files committed -- run: test ! -f .env && test ! -f server/.env && test ! -f .env.local && test ! -f .env.production -- severity: critical diff --git a/.machine_readable/contractiles/must/must.ncl b/.machine_readable/contractiles/must/must.ncl deleted file mode 100644 index 1d4c52c5..00000000 --- a/.machine_readable/contractiles/must/must.ncl +++ /dev/null @@ -1,64 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# Must — invariants runner -# -# Pairs with: Mustfile.a2ml (same directory) -# Verb: must (invariant assertion) -# Semantics: every check is a hard gate. A single failure blocks merge. -# CLI: `contractile must run` → reads Mustfile.a2ml, evaluates each check, -# emits pass/fail verdict per item, exits non-zero if any failed. -# -# This file is the *schema + runner* that the `contractile` CLI (at -# /var/mnt/eclipse/repos/reposystem/contractiles/cli/) loads alongside -# Mustfile.a2ml. Anything else in this directory is human-only notes/archive -# and MUST be ignored by machines. -# -# Base: ../_base.ncl provides pedigree_schema, run_defaults, probe_schema. -# See: docs/CONTRACTILE-SPEC.adoc - -let base = import "../_base.ncl" in - -{ - pedigree = base.pedigree_schema & { - contractile_verb = "must", - semantics = "invariant", - security = { - leash = 'Kennel, - trust_level = "read-only verification", - allow_network = false, - allow_filesystem_write = false, - allow_subprocess = true, # verification probes may shell out (e.g. grep, test -f) - }, - metadata = { - name = "must-runner", - version = "1.0.0", - description = "Evaluates every invariant in the adjacent Mustfile.a2ml as a hard gate.", - paired_xfile = "Mustfile.a2ml", - author = "Jonathan D.A. Jewell ", - }, - }, - - # Contract schema — the shape every Mustfile.a2ml must satisfy. - # Used by `contractile must typecheck Mustfile.a2ml`. - schema = { - invariants - | Array { - id | String, - description | String, - # TODO: migrate to base.probe_schema (structured probe) when CLI supports it - probe | String, # shell command; exit 0 = pass - # status_core values: 'declared, 'verified, 'failing - status | [| 'declared, 'verified, 'failing |] | default = 'declared, - severity | [| 'critical, 'high, 'medium |] | default = 'critical, - notes | String | optional, - fix | String | optional, - }, - }, - - # Runner behaviour — consumed by the contractile CLI dispatcher. - # Inherits from base.run_defaults; on_any_fail is the hard-gate default. - run = base.run_defaults & { - on_any_fail = "exit-nonzero", # hard gate - report_format = "a2ml", # emit a2ml report, not json - emit_summary = true, - }, -} diff --git a/.machine_readable/contractiles/trust/Trustfile.a2ml b/.machine_readable/contractiles/trust/Trustfile.a2ml deleted file mode 100644 index d4f5f8c2..00000000 --- a/.machine_readable/contractiles/trust/Trustfile.a2ml +++ /dev/null @@ -1,1124 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# ============================================================================= -# A2ML Trustfile Example (Fully Populated Reference) -# This is the complete example. The blank template is Trustfile.a2ml. -# ============================================================================= - ---- -### [META] -id: "did:web:example.com" -version: "2026.2.5-final" -context: - - "https://a2ml.org/ns/v3" - - "https://idris-lang.org/ns/v2" # TODO: replace with canonical URL once published - - "https://hypatia.scans/ns/v1" - - "https://w3id.org/security/v4" - - "https://w3id.org/transparency/v1" -meta: - generated: "2026-02-16T00:00:00Z" - expires: "2027-02-16T00:00:00Z" - signature: - algorithm: "Ed448+Dilithium5" - value: | - -----BEGIN HYBRID SIGNATURE----- - BASE64_Ed448+Dilithium5_SIGNATURE_OF_THIS_FILE - -----END HYBRID SIGNATURE----- - signedBy: "did:web:example.com#primary-sig" - proof: "https://example.com/proofs/meta.idr" - fallbackSignature: - algorithm: "SPHINCS+" - value: | - -----BEGIN SPHINCS+ SIGNATURE----- - BASE64_SPHINCS+_SIGNATURE_OF_THIS_FILE - -----END SPHINCS+ SIGNATURE----- - integrity: - sha3-512: "HEX_SHA3_512_OF_THIS_FILE" - shake256: "BASE32_SHAKE256_OF_THIS_FILE" - zonemd: "2026021601;SHA512;BASE64_SHA512_OF_ZONE;SHAKE256;BASE32_SHAKE256_OF_ZONE" - ci_cd: - github_actions: "https://github.com/hyperpolymath/example.com/blob/main/.github/workflows/trustfile.yml" - gitbot_fleet: "https://gitbot-fleet.example.com/hooks/trustfile" - hypatia_scan: "https://hypatia.scans/repos/example.com" - automation: - hashing: ["SHA3-512", "SHAKE256", "BLAKE3"] - diffing: "alert-on-unexpected-changes" - integrity: ["zonemd-consistency", "transparency-log-continuity", "idris2-proof-validity"] - ---- -### [THREAT_MODEL] -adversaries: - - type: "APT" - mitigations: - - "Capability-based auth → No lateral movement." - - "Idris2 proofs → No exploit primitives." - - "Transparency logs → Immediate detection." - - type: "Ransomware" - mitigations: - - "Consent-Aware HTTP → No bulk exfiltration." - - "SDP (CAdRE Router) → Resource isolation." - - "Immutable logs → Instant rollback." - - type: "Quantum Adversary" - mitigations: - - "Kyber1024 + Dilithium5 → PQ-resistant crypto." - - "SPHINCS+ fallback → Crypto agility." - - "GitBot-Fleet → Automated key rotation." - - type: "DDoS" - mitigations: - - "Cloudflare edge network → Absorbs volumetric attacks." - - "HTTP DDoS Managed Ruleset → Auto-mitigation at max sensitivity." - - "Challenge Passage TTL → Rate-limits challenge solvers." - - "Security Level → Adjustable based on threat intelligence." - - type: "AI Scraper" - mitigations: - - "Bot Fight Mode → Challenges known bot patterns." - - "Block AI Bots → Blocks verified AI crawlers + similar unverified." - - "AI Labyrinth → Traps scrapers in infinite maze of AI-generated decoy content." - - "AI Crawl Control → Per-crawler blocking and monitoring." - - "Managed robots.txt → Programmatic crawl directives." - - type: "Credential Stuffer" - mitigations: - - "Browser Integrity Check → Rejects headless/automated browsers." - - "Challenge Passage TTL → Forces re-challenge after 30 min." - - "HSTS preload → Prevents SSL-stripping MITM for credential capture." - - "Leaked credentials detection → (Enterprise; noted for upgrade path)." - - type: "Email Spoofing" - mitigations: - - "SPF hard fail (-all) → Rejects unauthorized senders." - - "DMARC p=reject → Instructs receivers to drop spoofed mail." - - "DKIM signing → Cryptographic message authentication." - - "CAA records → Restricts certificate issuance to authorized CAs." - ---- -### [DNS] -dnssec: - enabled: true - algorithm: "ECDSAP256SHA256" - ds_record: "{{DS_RECORD}}" - key_tag: "{{KEY_TAG}}" - digest_type: "SHA-256" - policy: "DNSSEC MUST be enabled on all zones. DS records propagated to registrar." - security: - proof: "DNS.DNSSEC.idr" - ci_cd: "verify-dnssec-propagation" -soa: - mname: "ns1.cloudflare.com." - rname: "admin.example.com." - serial: 2026021601 - refresh: 10800 - retry: 3600 - expire: 604800 - minimumTTL: 3600 - zonemd: "2026021601;SHA512;BASE64_SHA512_OF_ZONE;SHAKE256;BASE32_SHAKE256_OF_ZONE" -records: - - type: "A" - name: "@" - value: "192.0.2.1" - ttl: 3600 - proxied: true - security: - zonemd: "2026021601;SHA512;BASE64_SHA512;SHAKE256;BASE32_SHAKE256" - proof: "DNS.Core.A_Record.idr" - hypatia: "scan-dns-record" - ci_cd: "auto-hash-on-push" - - type: "AAAA" - name: "@" - value: "2001:db8::1" - ttl: 3600 - proxied: true - security: - proof: "DNS.Core.AAAA_Record.idr" - - type: "HTTPS" - name: "@" - value: '1 . alpn="h3,h2" ipv4hint=192.0.2.1 ipv6hint=2001:db8::1' - ttl: 3600 - security: - proof: "DNS.HTTPS.idr" - - type: "SVCB" - name: "@" - value: '1 . alpn="h3,h2" port=443 ipv4hint=192.0.2.1 ipv6hint=2001:db8::1' - ttl: 3600 - security: - proof: "DNS.SVCB.idr" - - type: "TXT" - name: "@" - value: '"v=DMARC1; p=reject; rua=mailto:dmarc@example.com; ruf=mailto:dmarc@example.com"' - ttl: 3600 - security: - proof: "Email.DMARC.idr" - - type: "CAA" - name: "@" - value: '0 issue "letsencrypt.org"' - ttl: 3600 - - type: "CAA" - name: "@" - value: '0 issue "digicert.com"' - ttl: 3600 - - type: "CAA" - name: "@" - value: '0 iodef "mailto:security@example.com"' - ttl: 3600 - - type: "TLSA" - name: "_443._tcp" - value: "3 1 1 D2ABDE240D7CD3EE6B4B28C54DF034B97983A1D16E8A410E4561CB106618E971" - ttl: 3600 - - type: "TLSA" - name: "_443._tcp" - value: "3 3 1 BASE32_SHAKE256_CERT_HASH" - ttl: 3600 - - type: "TXT" - name: "_cyberwar-trap" - value: '"🎣 This system is formally verified. Good luck, script kiddie."' - ttl: 3600 - security: - hypatia: "scan-for-apt-activity" - proof: "Psychological.Warfare.idr" - - type: "TXT" - name: "_capabilities" - value: '"v=OCAP1; endpoint=https://example.com/cap"' - ttl: 3600 - security: - proof: "HTTP.Capabilities.idr" - - type: "TXT" - name: "_consent" - value: '"v=CAdRE1; endpoint=https://example.com/.well-known/consent"' - ttl: 3600 - security: - proof: "HTTP.Consent.idr" - gitbot: "validate-consent-endpoint" - # Email Security Records - - type: "TXT" - name: "@" - value: '"v=spf1 -all"' - ttl: 3600 - notes: "Hard fail. No servers authorized to send. Override per-domain if email is used." - security: - proof: "Email.SPF.idr" - - type: "TXT" - name: "_dmarc" - value: '"v=DMARC1; p=reject; sp=reject; adkim=s; aspf=s; rua=mailto:dmarc@example.com; ruf=mailto:dmarc@example.com; fo=1"' - ttl: 3600 - notes: "Strict alignment. Reject all unauthenticated. Forensic reports on any failure." - security: - proof: "Email.DMARC.idr" - ci_cd: "validate-dmarc-alignment" - - type: "TXT" - name: "*._domainkey" - value: '"v=DKIM1; p="' - ttl: 3600 - notes: "Empty public key = revoked. Prevents DKIM pass on spoofed mail for non-sending domains." - security: - proof: "Email.DKIM.idr" - - type: "TXT" - name: "_mta-sts" - value: '"v=STSv1; id={{MTA_STS_ID}}"' - ttl: 3600 - notes: "MTA-STS policy ID. Rotate on policy change." - - type: "TXT" - name: "_smtp._tls" - value: '"v=TLSRPTv1; rua=mailto:tls-reports@example.com"' - ttl: 3600 - notes: "SMTP TLS Reporting (RFC 8460). Receive reports on TLS failures." - ---- -### [EMAIL_SECURITY] -overview: | - Email security posture for domains that do NOT send email. - All records configured to reject/block spoofed mail. - For domains that DO send email, override SPF with authorized senders, - configure DKIM signing keys, and set DMARC to quarantine during rollout. -policy: - non_sending_domains: - spf: "v=spf1 -all" - dmarc: "p=reject; sp=reject; adkim=s; aspf=s; fo=1" - dkim: "revoked (empty public key)" - mta_sts: "mode: enforce; max_age: 604800" - sending_domains: - spf: "v=spf1 include:_spf.google.com include:_spf.cloudflare.com -all" - dmarc: "p=reject; sp=reject; adkim=s; aspf=s; pct=100; fo=1" - dkim: "2048-bit RSA minimum; rotate annually" - mta_sts: "mode: enforce; max_age: 604800" -email_routing: - provider: "Cloudflare Email Routing" - features: - - "Custom address forwarding" - - "DMARC enforcement (rejects unauthenticated inbound)" - - "IPv6 support" - - "Automatic MX/SPF/DKIM record creation" - security: - proof: "Email.Routing.idr" -security: - proof: "Email.Policy.idr" - ci_cd: "validate-email-records-on-push" - ---- -### [TRUSTFILE] -issuer: "did:web:example.com" -keys: - - id: "#primary-sig" - type: "HybridKey2024" - classical: - algorithm: "Ed448" - publicKeyJwk: - kty: "OKP" - crv: "Ed448" - x: "BASE64URL_Ed448_PUBLIC_KEY" - postQuantum: - algorithm: "Dilithium5" - publicKeyJwk: - kty: "OKP" - crv: "Dilithium5" - x: "BASE64URL_Dilithium5_PUBLIC_KEY" - fallback: - algorithm: "SPHINCS+" - publicKeyJwk: - kty: "OKP" - crv: "SPHINCS+" - x: "BASE64URL_SPHINCS+_PUBLIC_KEY" - usage: ["authentication", "assertion"] - security: - proof: "Crypto.HybridKey.idr" - hypatia: "scan-keys" - ci_cd: "rotate-keys-on-compromise" -algorithms: - hashing: ["SHA3-512", "SHAKE256", "BLAKE3"] - kdf: "HKDF-SHAKE512" - rng: "ChaCha20-DRBG" - passwordHashing: "Argon2id (512 MiB, 8 iter, 4 lanes)" - security: - proof: "Crypto.Algorithms.idr" -policies: - dns: - rego: | - package trustfile.dns - default allow = false - allow { - input.record.security.proof != "" - input.record.security.zonemd != "" - } - idris2: "Policies.DNS.idr" - ci_cd: "validate-dns-policies-on-push" - http: - rego: | - package trustfile.http - default allow = false - allow { - input.consent.granted - valid_capability(input.capability) - } - idris2: "Policies.HTTP.idr" - php: - rego: | - package trustfile.php - default allow = false - allow { - input.php.aegis_enabled - input.php.sanctify_enabled - } - idris2: "Policies.PHP.idr" -fallbacks: - signatures: ["Ed448+Dilithium5", "SPHINCS+"] - keyExchange: ["Kyber1024-X25519", "X25519"] - ---- -### [VERIFICATION_LADDER] -overview: | - Four-tier verification claim ladder. Each capability in this Trustfile - MUST declare which tier it sits at. Claims at a tier require the evidence - at that tier; no claim may be made stronger than the evidence supports. -tiers: - - id: "idris2-proven" - description: "Formal proofs in Idris2 with %default total. IsUnbreakable or equivalent proof required before activation." - evidence_required: "Idris2 module, compiler version recorded, axioms declared, last-check date." - - id: "zig-assured" - description: "Zig boundary calls into proven-sourced safety primitives (safePathDefault, safeHeaderDefault, etc). Defense-in-depth; not formal proof but grounded in Idris2-proven predicates." - evidence_required: "Declared primitive + reference to proven-side Idris2 proof." - - id: "elixir-disciplined" - description: "Supervision trees + session-typed protocols + dialyzer + Gleam where applicable. Pattern-conforming, not proven." - evidence_required: "Supervisor module, session type declaration, dialyzer clean." - - id: "external-trust" - description: "Unverified-by-construction layer: HATs, external CLIs, third-party services. Acknowledged trust, isolated via circuit breakers." - evidence_required: "Documented trust boundary + isolation mechanism." - ---- -### [SEAMS] -overview: | - A seam is an integration boundary between two components that can be - independently versioned, built, or deployed. Every seam MUST be declared - here with: contract owner, test coverage, failure mode on mismatch. - See docs/SEAMS-SPEC.adoc for the full spec. -seams: - - id: "example-seam" - description: "Example seam declaration — replace with real entries" - from: "component-a" - to: "component-b" - contract: "path/to/abi-or-schema" - test_ref: "tests/seam/component-a-b.test" - failure_mode: "fail-closed" - tier: "zig-assured" - notes: "" -policy: - seam_check: "every PR that touches either side of a declared seam MUST exercise the P2P test for that seam before merge" -security: - proof: "Seams.Policy.idr" - ---- -### [SECRETS_HYGIENE] -at_rest: - pattern: "SOPS+age" - template_location: "web-ecosystem/lcb-website/" - adoption_status: "template + estate intent — per-repo adoption tracked below" - per_repo_adoption: - - repo: "lcb-website" - status: "DEPLOYED" - # TEMPLATE NOTE: replace {{THIS_REPO}} with the repo name (e.g. "boj-server") and - # {{REPO_SOPS_ADOPTION_STATUS}} with one of: "DEPLOYED", "PENDING — runtime-only via Rokur, - # no at-rest secrets in this repo", or a concise description of the actual status. - - repo: "{{THIS_REPO}}" - status: "{{REPO_SOPS_ADOPTION_STATUS}}" - pre_commit_hooks: - - "gitleaks" - - "plaintext detector" -delivery: - mechanism: "environment variable injection at container start" - scope: "SOPS-decrypted secrets → ROKUR_SECRET_ env vars; containers never read plaintext from disk" -gate: - tool: "Rokur" - role: "policy engine — validates required secrets present, audits, rate-limits, fail-closed" - features: - - "per-IP sliding window rate limiting (60/min general, 5/min auth-fail)" - - "structured JSONL audit logging" - - "X-Request-Id tracing" - - "policy backends: builtin or external (Ephapax adapter)" - - "SIGHUP hot-reload" -llm_agents: - tool: "RGTV" - status: "ALPHA — NOT production-ready, see RGTV/README.adoc known-unsafe list" - scope: "LLM-agent credential brokering only — opaque one-use grants" - # TEMPLATE NOTE: replace {{RGTV_ENABLED_FOR_REPO}} with "true" if this repo brokers - # LLM-agent credentials via RGTV, or "false — " if not. Most repos will be false. - # RGTV is ALPHA; see RGTV/README.adoc for the known-unsafe list. - enabled_here: "{{RGTV_ENABLED_FOR_REPO}}" -security: - proof: "Secrets.Hygiene.idr" - ci_cd: "validate-secrets-flow-on-push" - ---- -### [CI_CD] -github_actions: - name: "Trustfile Validation" - on: ["push", "pull_request"] - jobs: - validate: - runs-on: "ubuntu-latest" - steps: - - uses: "actions/checkout@v4" - - name: "Validate A2ML" - run: "a2ml validate example.com.trustfile.a2ml" - - name: "Run Idris2 Proofs" - run: "idris2 --build trust.ipkg" - - name: "Hypatia Scan" - run: "hypatia scan --config hypatia.yml" - - name: "GitBot-Fleet Passover" - run: "gitbot-fleet passover --file example.com.trustfile.a2ml" - update_integrity: - runs-on: "ubuntu-latest" - steps: - - name: "Update Hashes" - run: | - NEW_SHA3=$(sha3sum -a 512 example.com.trustfile.a2ml | awk '{print $1}') - NEW_SHAKE=$(shake256sum example.com.trustfile.a2ml | awk '{print $1}' | base32) - sed -i "s|sha3-512:.*|sha3-512: \"$NEW_SHA3\"|" example.com.trustfile.a2ml - sed -i "s|shake256:.*|shake256: \"$NEW_SHAKE\"|" example.com.trustfile.a2ml - - name: "Commit and Push" - run: | - git config --global user.name "GitBot-Fleet" - git config --global user.email "gitbot@example.com" - git add example.com.trustfile.a2ml - git commit -m "Auto-update integrity hashes [skip ci]" - git push -gitbot_fleet: - hooks: - - type: "pre-commit" - script: "a2ml validate example.com.trustfile.a2ml" - - type: "post-merge" - script: "gitbot-fleet diff --file example.com.trustfile.a2ml" -hypatia: - config: "hypatia.yml" - scans: - - type: "dns" - frequency: "daily" - - type: "crypto" - frequency: "weekly" - - type: "php" - frequency: "on-push" - ---- -### [IDRIS2_PROOFS] -theorems: - - name: "dns_correctness" - file: "DNS.Core.idr" - description: "All DNS records are conflict-free and correctly signed." - status: "proven" - ci_cd: "reprove-on-dns-change" - - name: "tls_handshake_safety" - file: "TLS.Handshake.idr" - description: "TLS 1.3 + Kyber1024 handshake resists downgrade attacks." - status: "proven" - - name: "consent_aware_http_soundness" - file: "HTTP.Consent.idr" - description: "Consent-Aware HTTP (CAdRE) enforces user intent." - status: "proven" - - name: "capability_gateway_correctness" - file: "HTTP.Capabilities.idr" - description: "OCAP-style capability gateway is safe." - status: "proven" - - name: "php_hardening_no_bypasses" - file: "PHP.Hardening.idr" - description: "PHP-Aegis + Sanctify-PHP blocks all unsafe functions." - status: "proven" - - name: "edge_ssl_no_downgrade" - file: "Cloudflare.SSL.idr" - description: "TLS 1.3 + HSTS preload prevents protocol downgrade at edge." - status: "proven" - ci_cd: "reprove-on-ssl-change" - - name: "bot_defense_coverage" - file: "Cloudflare.Bots.idr" - description: "Bot Fight Mode + AI Labyrinth + Block AI Bots covers all free-plan bot vectors." - status: "proven" - - name: "email_anti_spoofing" - file: "Email.Policy.idr" - description: "SPF -all + DMARC reject + revoked DKIM prevents email spoofing on non-sending domains." - status: "proven" - ci_cd: "reprove-on-email-record-change" - - name: "response_headers_complete" - file: "Cloudflare.ResponseHeaders.idr" - description: "All OWASP-recommended response headers enforced at edge." - status: "proven" - - name: "dnssec_chain_valid" - file: "DNS.DNSSEC.idr" - description: "DNSSEC chain of trust from root to zone is valid and signed." - status: "proven" - ci_cd: "verify-dnssec-weekly" - - name: "network_transport_safety" - file: "Cloudflare.Network.idr" - description: "HTTP/3 + 0-RTT replay protection + Onion routing correctly configured." - status: "proven" - ---- -### [PROOF_METADATA] -compiler: - idris2_version: "0.8.0" - zig_version: "0.15.2" - # TEMPLATE NOTE: replace {{LAST_PROOF_CHECK_DATE}} with the ISO-8601 date of the last - # Idris2 proof rebuild in this repo (e.g. "2026-04-17"). Updated at each proof-rebuild session. - last_check: "{{LAST_PROOF_CHECK_DATE}}" -axioms: - declared: [] - notes: "No axioms may be added without explicit justification and entry here." -drift_alert: - ci_cd: "rebuild-all-proofs-on-compiler-upgrade" - policy: "any compiler upgrade triggers full proof rebuild + signed attestation of re-check" - ---- -### [AUTOMATION] -hashing: - tool: "GitBot-Fleet" - triggers: ["pre-commit", "post-merge"] - algorithms: ["SHA3-512", "SHAKE256", "BLAKE3"] -diffing: - tool: "GitBot-Fleet" - rules: - - "alert-on-unexpected-changes" - - "require-proof-updates-for-crypto-changes" -integrity: - tool: "Hypatia + Idris2" - checks: - - "zonemd-consistency" - - "transparency-log-continuity" - - "idris2-proof-validity" - ---- -### [CAPABILITY_GATEWAY] -rules: - - resource: "/api/data" - policy: "require Ed448+Dilithium5-signed capability token" - proof: "HTTP.Capabilities.Data.idr" - - resource: "/admin" - policy: "require TPM 2.0 + YubiKey device attestation" - proof: "HTTP.Capabilities.Admin.idr" - ---- -### [SAFE_HACKING] -scope: "this-repo-only" -allowed_probe_classes: [] -probes: [] -policy: | - Authorised offensive testing scoped to this repo. Probes listed here - are actively executed during `contractile trust probe`. NEVER touches - external systems. See trust.ncl for schema; this section is the data. -policy_on_unexpected_outcome: "exit-nonzero" -security: - proof: "SafeHacking.Policy.idr" - ---- -### [VULNERABILITY_DISCLOSURE] -policy: | - Responsible disclosure welcomed. Researchers reporting real vulnerabilities - in good faith receive acknowledgement in SECURITY.adoc and in - /.well-known/security-acknowledgments. See security.txt for contact path. -# TEMPLATE NOTE: replace {{SECURITY_CONTACT}} with a mailto: URI for this repo's -# security contact, e.g. "mailto:j.d.a.jewell@open.ac.uk". -contact: "{{SECURITY_CONTACT}}" -recognition: - mechanism: "security-acknowledgments list" - url: "https://{{DOMAIN}}/.well-known/security-acknowledgments" -contractile_ref: "tracked in `contractile trust probe` — see trust.ncl safe_hacking" -security: - proof: "VulnDisclosure.Policy.idr" - ---- -### [SDP_RULES] -services: - - name: "dashboard.internal" - access: - - group: "admins" - policy: "require Ed448+Dilithium5 + device-attestation + cadre-consent" - - group: "bots" - policy: "require JWT (Kyber1024) + IP in CI_NETWORK" - proof: "SDP.Dashboard.idr" - - name: "db.internal" - access: - - group: "apps" - policy: "require mutual TLS (Kyber1024-X25519) + client cert" - proof: "SDP.Database.idr" - ---- -### [TRANSPARENCY_LOG] -rfc9162: - uri: "https://example.com/log/transparency.json" - entries: - - timestamp: "2026-02-16T00:00:00Z" - data: "BASE64_ENCODED_THIS_FILE" - signature: "BASE64_Ed448+Dilithium5_SIGNATURE" - idris2_proof: "Transparency.Log.idr" - ci_cd: "append-on-push" - ---- -### [SSL/TLS] -ciphers: - - "TLS_AES_256_GCM_SHA384" - - "TLS_CHACHA20_POLY1305_SHA256" -groups: - - "X25519Kyber768Draft00" - - "secp256r1" -protocols: - - "TLSv1.3" -minimum_version: "1.2" -notes: | - TLS 1.3 preferred with post-quantum key exchange (X25519Kyber768). - Minimum version 1.2 enforced at Cloudflare edge for clients that - don't support 1.3 yet. TLS 1.0 and 1.1 are BANNED. Cipher preference - is server-side (Cloudflare-controlled on free plan). -features: - ocspStapling: true - signedCertTimestamps: true - certificateTransparency: - logs: - - "ct.googleapis.com/aviator" - - "ct.googleapis.com/rocketeer" - monitoring: true - notes: "Cloudflare automatically includes SCT in TLS handshake for all proxied zones." - mustStaple: true - opportunistic_encryption: true - automatic_https_rewrites: true - always_use_https: true -edge_certificates: - provider: "Cloudflare Universal SSL" - type: "DV (Domain Validated)" - issuers: ["DigiCert", "Let's Encrypt", "Google Trust Services"] - auto_renewal: true - caa_restriction: true - notes: | - Cloudflare issues Universal SSL certificates automatically for all - proxied zones. CAA records restrict issuance to authorized CAs only. - Origin certificates should use Cloudflare Origin CA (15-year validity) - or publicly trusted certs for Full (Strict) mode. -security: - proof: "TLS.Configuration.idr" - ci_cd: "verify-tls-settings-drift" - ---- -### [CLOUDFLARE] -operator_trust_anchor: | - Cloudflare is an operator-chosen trust anchor for this repo. Its edge - network provides DDoS absorption, TLS termination, and WAF. This is a - single-vendor dependency: compromise or misbehaviour at Cloudflare - affects all proxied traffic. Plan for vendor-compromise scenario - documented in THREAT-MODEL.md §vendor-anchors. -waf: - ruleset: "OWASP_ModSecurity_CRS" - sensitivity: "high" - paranoiaLevel: 4 - managed_rulesets: - - name: "Cloudflare Managed Ruleset" - id: "efb7b8c949ac4650a09736fc376e9aee" - action: "execute" - phase: "http_request_firewall_managed" - - name: "Cloudflare OWASP Core Ruleset" - id: "4814384a9e5d4991b9815dcfc25d2f1f" - action: "execute" - phase: "http_request_firewall_managed" - ddos: - http: - sensitivity: "high" - action: "managed_challenge" - ruleset: "Cloudflare HTTP DDoS Attack Protection" - notes: "Always-on, unmetered DDoS protection on all plans." - security: - proof: "Cloudflare.WAF.idr" - ci_cd: "validate-waf-rulesets" -workers: - - name: "consent-aware-http" - script: "https://example.com/workers/consent.js" - routes: - - "example.com/.well-known/consent*" - - name: "capability-gateway" - script: "https://example.com/workers/cap.js" - routes: - - "example.com/cap*" - ---- -### [CLOUDFLARE_EDGE_SECURITY] -overview: | - Cloudflare edge security settings applied uniformly across all zones. - These are the maximum free-plan configurations. Settings are enforced - via API and validated by Hypatia CI scans. Any drift triggers an alert. - -ssl_tls: - mode: "strict" - min_tls_version: "1.2" - tls_1_3: "zrt" - always_use_https: true - automatic_https_rewrites: true - opportunistic_encryption: true - hsts: - enabled: true - max_age: 31536000 - include_subdomains: true - preload: true - nosniff: true - universal_ssl: true - certificate_transparency: true - ocsp_stapling: true - notes: | - TLS 1.3 with 0-RTT (zrt). HSTS preloaded at 1 year with subdomains. - SSL mode 'strict' requires valid origin certificate (Cloudflare Origin CA - or publicly trusted). Downgrade to 'full' only if origin has self-signed. - security: - proof: "Cloudflare.SSL.idr" - ci_cd: "verify-ssl-settings-drift" - -bot_defense: - bot_fight_mode: true - block_ai_bots: true - ai_labyrinth: true - ai_crawl_control: - default_action: "block" - notes: | - Block all known AI crawlers by default. AI Labyrinth traps persistent - scrapers in an infinite maze of AI-generated decoy content, wasting - their compute while protecting real content. Individual crawlers can - be allowed via per-crawler overrides if licensing agreements exist. - managed_robots_txt: true - javascript_detections: false - notes: | - JS detections require Super Bot Fight Mode (Pro+). On free plan, - Bot Fight Mode uses pattern matching only. AI Labyrinth is the - primary free-plan defense against sophisticated AI scraping. - security: - proof: "Cloudflare.Bots.idr" - ci_cd: "verify-bot-settings" - -scrape_shield: - email_obfuscation: true - hotlink_protection: true - server_side_excludes: true - notes: | - Email obfuscation rewrites email addresses in HTML to prevent - harvesting by scrapers. Hotlink protection prevents other sites - from embedding your images. Server-side excludes hide content - from suspicious visitors. - security: - proof: "Cloudflare.ScrapeShield.idr" - -browser_integrity: - browser_check: true - security_level: "medium" - challenge_ttl: 1800 - notes: | - Browser Integrity Check evaluates HTTP headers for common - characteristics of abusive traffic. Security level 'medium' - challenges visitors from IPs with moderate threat scores. - Challenge TTL of 30 minutes before re-challenge. - security: - proof: "Cloudflare.BrowserIntegrity.idr" - -page_shield: - enabled: true - script_monitoring: true - notes: | - Page Shield monitors client-side JavaScript resources loaded by - your pages. Free tier provides script detection and alerts for - new/changed scripts. Paid tiers add malicious script detection. - security: - proof: "Cloudflare.PageShield.idr" - ci_cd: "review-new-scripts" - -security_txt: - enabled: true - contact: "mailto:j.d.a.jewell@open.ac.uk" - preferred_languages: "en" - # TEMPLATE NOTE: replace {{SECURITY_TXT_EXPIRES}} with an RFC 3339 datetime 1 year from deployment, - # e.g. "2027-04-17T00:00:00Z". Auto-renewed by CI. - expires: "{{SECURITY_TXT_EXPIRES}}" - # TEMPLATE NOTE: replace {{DOMAIN}} with the canonical domain for this repo (bare domain or - # GitHub Pages URL), e.g. "boj-server.hyperpolymath.dev" or "github.com/hyperpolymath/". - # Used in all /.well-known/ paths below. - policy: "https://{{DOMAIN}}/.well-known/security-policy" - acknowledgments: "https://{{DOMAIN}}/.well-known/security-acknowledgments" - encryption: "https://{{DOMAIN}}/.well-known/pgp-key.txt" - canonical: "https://{{DOMAIN}}/.well-known/security.txt" - notes: | - RFC 9116 compliant. Served by Cloudflare at /.well-known/security.txt. - Contact is the author's university email. Expiry set to 1 year from - deployment, auto-renewed by CI. Canonical URL prevents spoofing. - security: - proof: "Cloudflare.SecurityTxt.idr" - ci_cd: "renew-security-txt-before-expiry" - -rate_limiting: - architecture: "four-tier" - tier_1_edge: - provider: "Cloudflare" - mechanisms: ["Anycast absorption", "DDoS Managed Ruleset", "per-zone rate rules"] - tier_2_gateway: - provider: "http-capability-gateway / svalinn" - mechanisms: ["per-IP token-bucket sliding window", "per-capability-token", "per-endpoint"] - status: "PENDING — http-capability-gateway wiring forthcoming" - tier_3_beam: - provider: "Elixir supervisor" - mechanisms: ["per-cartridge-invocation budget", "mailbox back-pressure"] - tier_4_cartridge: - provider: "cartridge-declared" - mechanisms: ["Nickel manifest declares per-cartridge limits"] - cross_tier: - - "RFC 9530 rate-limit headers (RateLimit-Limit, RateLimit-Remaining, RateLimit-Reset)" - - "429 + Retry-After on limit hit" - - "Turnstile challenge on high-value endpoints" - - "HMAC request signing for API clients" - - "per-cartridge circuit breakers with exponential backoff" - - "shadow-ban for persistent offenders" - cost_ceiling: - policy: "operator-managed emergency brake above tier 1" - # TEMPLATE NOTE: replace {{COST_CEILING_POLICY}} with a concise operator policy string, - # e.g. "operator-managed; emergency brake above edge-tier rate limits; specific cap TBD". - # This is an operator-choice field — no universal default. - note: "{{COST_CEILING_POLICY}}" - security: - proof: "RateLimiting.Policy.idr" - ---- -### [RESPONSE_HEADERS] -overview: | - Security response headers applied at the Cloudflare edge via Managed - Transforms and custom response header modification rules. These headers - instruct browsers to enforce security policies regardless of origin config. - -managed_transforms: - add: - - "X-Content-Type-Options: nosniff" - - "X-Frame-Options: SAMEORIGIN" - - "Referrer-Policy: strict-origin-when-cross-origin" - remove: - - "Server" - - "X-Powered-By" - notes: "Managed Transforms are Cloudflare's built-in header rules. Zero config." - -custom_headers: - - name: "Permissions-Policy" - value: "camera=(), microphone=(), geolocation=(), payment=()" - notes: "Deny all sensitive browser APIs unless explicitly needed." - - name: "Content-Security-Policy" - value: "default-src 'self'; script-src 'self'; style-src 'self' 'unsafe-inline'; img-src 'self' data: https:; frame-ancestors 'self'; base-uri 'self'; form-action 'self'" - notes: "Strict CSP baseline. Override per-project if needed (e.g., for CDN scripts)." - - name: "Cross-Origin-Opener-Policy" - value: "same-origin" - - name: "Cross-Origin-Embedder-Policy" - value: "require-corp" - - name: "Cross-Origin-Resource-Policy" - value: "same-origin" - -policy: | - All security headers are enforced at the edge. Origin servers SHOULD - also set these headers as defense-in-depth. Headers set at edge take - precedence when Managed Transforms are enabled. CSP violations are - reported to /csp-report endpoint if a report-uri directive is added. - -security: - proof: "Cloudflare.ResponseHeaders.idr" - ci_cd: "validate-response-headers" - ---- -### [NETWORK] -overview: | - Network-level settings applied at the Cloudflare edge. - These affect how traffic is transported between clients and edge. - -http2: true -http3: true -quic: true -zero_rtt: true -websockets: true -onion_routing: true -ipv6_posture: - origin: "IPv6-only (strict)" - edge: "dual-stack (Cloudflare translates IPv4 clients to IPv6-only origins)" - internal_comms: "IPv6-only between BoJ instances" - policy: "Declared 2026-04-17. IPv4 clients reach BoJ only via Cloudflare edge translation; origin never listens on IPv4." -brotli: true - -zero_rtt_policy: | - 0-RTT Connection Resumption is enabled for performance. Note: 0-RTT - data is vulnerable to replay attacks. Cloudflare mitigates this by - only allowing 0-RTT on idempotent requests (GET/HEAD). Non-idempotent - requests (POST/PUT/DELETE) always use full handshake. Applications - MUST NOT rely on 0-RTT for state-changing operations. - -onion_routing_policy: | - Tor/Onion routing enabled via Cloudflare's Opportunistic Onion - (Alt-Svc header advertising .onion endpoint). This allows Tor users - to access sites without exit node MITM risk. Does NOT create a - dedicated .onion address — uses Cloudflare's shared onion service. - -security: - proof: "Cloudflare.Network.idr" - ci_cd: "verify-network-settings" - ---- -### [ORIGIN_PROTECTION] -hidden_primary: - public_dns: "no A/AAAA records resolving directly to origin" - public_endpoint: "Cloudflare Tunnel only" - authenticated_origin_pulls: - enabled: true - mtls_ca: "Cloudflare Origin CA" - policy: "origin rejects all non-CF traffic at TCP layer" - admin_endpoints: - mechanism: "Cloudflare Access (zero-trust)" - public_endpoint: "none" - backup_origin: - mechanism: "second Cloudflare Tunnel, passive failover" - leak_checks: - - "verify no historic origin IP exposure in securitytrails.com" - - "verify no origin IP in HTTP error messages" - - "verify no origin IP in DNS MX/TXT records" -security: - proof: "OriginProtection.Policy.idr" - ci_cd: "verify-origin-hidden-weekly" - ---- -### [PERFORMANCE] -overview: | - Performance settings that have security implications. - Applied at the Cloudflare edge for all zones. - -early_hints: true -speed_brain: true -auto_minify: - javascript: true - css: true - html: true -rocket_loader: false -notes: | - Rocket Loader disabled by default — it rewrites JavaScript loading - order which can break SPAs and CSP policies. Enable per-project only - after testing. Speed Brain uses Speculation Rules API to prefetch - likely navigation targets (conservative eagerness only). - -caching: - browser_ttl: "respect-origin" - edge_ttl: "default" - always_online: true - notes: | - Always Online serves stale cached copies when origin is unreachable. - Browser TTL respects origin Cache-Control headers. Do not cache - authenticated content — use Cache-Control: private on origin. - -security: - proof: "Cloudflare.Performance.idr" - ---- -### [PHP_HARDENING] -aegis: - enabled: true - rules: - - "disable_functions=exec,popen,shell_exec,system" - - "expose_php=0" - - "session.cookie_httponly=1" - - "session.cookie_secure=1" -sanctify: - enabled: true - directives: - - "sanctify.globals=1" - - "sanctify.request=1" - - "sanctify.error_reporting=E_ALL" - ---- -### [CONTAINER_SUPPLY_CHAIN] -overview: | - Container supply-chain verification via the stapeln ecosystem. - All container images are built with Podman on Chainguard Wolfi base - images, signed as .ctp bundles via cerro-torre, and governed by - svalinn edge gateway policies. Runtime monitoring provided by vordr. - -runtime: - engine: "Podman" - policy: "Rootless containers only. Never Docker." - socket: "${XDG_RUNTIME_DIR}/podman/podman.sock" - security: - proof: "Container.Runtime.idr" - -base_images: - provider: "Chainguard" - registry: "cgr.dev/chainguard/" - allowed: - - "cgr.dev/chainguard/wolfi-base:latest" - - "cgr.dev/chainguard/static:latest" - policy: "Only Chainguard images permitted as base. Rebuilt daily, CVE-free." - security: - proof: "Container.BaseImages.idr" - ci_cd: "scan-base-images-daily" - -verified_bundles: - format: ".ctp" - tool: "cerro-torre" - operations: - pack: "ct pack -o " - sign: "cerro-sign sign --key-id " - verify: "ct verify " - push: "ct push " - explain: "ct explain " - attestations: - required: ["source-signature", "sbom-complete"] - recommended: ["security-audit", "reproducible-build"] - security: - proof: "Container.Bundles.idr" - hypatia: "scan-ctp-bundles" - -gateway: - tool: "svalinn" - policy_file: "container/.gatekeeper.yaml" - capabilities: - - "JWT/OAuth2 authentication" - - "Rate limiting (per-client, per-endpoint)" - - "Container trust enforcement (.ctp signature verification)" - - "Request validation (body size, NaN/Inf rejection)" - - "CORS policy enforcement" - - "Audit logging for write operations" - - "TLS auto-provisioning" - security: - proof: "Container.Gateway.idr" - ci_cd: "validate-gatekeeper-policy-on-push" - -monitoring: - tool: "vordr" - config_file: "container/vordr.toml" - capabilities: - - "Health endpoint monitoring" - - "Container crash detection" - - "Resource usage thresholds (CPU, memory, disk)" - - "Structured JSON log output" - - "Automatic restart on failure (configurable)" - security: - proof: "Container.Monitoring.idr" - -signing: - algorithm: "Ed25519" - tool: "cerro-torre sign / cerro-sign" - key_management: | - Signing keys are project-specific. Each service has a dedicated - Ed25519 key pair (e.g. -release). Public keys are - distributed in .gatekeeper.yaml trusted_signers section. - security: - proof: "Container.Signing.idr" - ci_cd: "rotate-signing-keys-on-compromise" - -deployment: - tool: "k9-svc" - spec_file: "container/deploy.k9.ncl" - trust_level: "Hunt" - description: | - k9-svc deployment components at Hunt trust level. Full pedigree - (L1-L5: identity, target, security, validation, recipes). - Requires cryptographic handshake before execution. Supports - dev/staging/production environments with rolling deployment. - security: - proof: "Container.Deployment.idr" - ci_cd: "validate-k9-pedigree-on-push" - ---- -### [SUPPLY_CHAIN_DEPS] -overview: | - Source-library supply chain. Chainguard covers base images; - this section tracks language-level deps. -zig: - mechanism: "build.zig.zon with SHA256 hashes" - adoption_status: "ADOPTED where Zig is used" -idris2: - mechanism: ".ipkg with dep version pinning" - adoption_status: "PENDING — estate-wide pinning in CRG contractile" -proven_library: - # TEMPLATE NOTE: replace {{PROVEN_HASH}} with the SHA-256 hex digest of - # verification-ecosystem/proven/ffi/zig/zig-out/lib/libproven_ffi.a obtained via - # `sha256sum .../libproven_ffi.a`. Set to "PENDING" with a note if the lib has not - # yet been built for this repo. - hash_attestation: "{{PROVEN_HASH}}" - source: "verification-ecosystem/proven" - verification: "libproven_ffi.a rebuilt on source change; downstream relink verified" -crg_contractile: "tracked under CRG grade requirements — see CRG-SELF-ASSESSMENT.adoc" -security: - proof: "SupplyChain.Deps.idr" - ---- -### [PLACEHOLDER_TRACKING] -overview: | - Every {{PLACEHOLDER}} in this file must resolve to a live value before - the Trustfile is considered deployed. CI enforces no-placeholder-state - on main branch. -resolution_policy: "CI check fails on any remaining {{...}} in main" -ci_cd: "enforce-no-placeholders-on-main" - ---- -### [SIGNATURE_BLOCK] -primary: - algorithm: "Ed448+Dilithium5" - signature: | - -----BEGIN HYBRID SIGNATURE----- - BASE64_Ed448+Dilithium5_SIGNATURE_OF_THIS_FILE - -----END HYBRID SIGNATURE----- - signedBy: "did:web:example.com#primary-sig" - idris2_proof: "Signature.Primary.idr" -fallback: - algorithm: "SPHINCS+" - signature: | - -----BEGIN SPHINCS+ SIGNATURE----- - BASE64_SPHINCS+_SIGNATURE_OF_THIS_FILE - -----END SPHINCS+ SIGNATURE----- - idris2_proof: "Signature.Fallback.idr" - ---- -### [DEPLOYMENT] -1. Replace all `BASE64_*`, `HEX_*`, and `DID_WEB_ID` placeholders. -2. Generate Idris2 proofs: - ```bash - idris2 --build trust.ipkg diff --git a/.machine_readable/contractiles/trust/trust.ncl b/.machine_readable/contractiles/trust/trust.ncl deleted file mode 100644 index 4c695540..00000000 --- a/.machine_readable/contractiles/trust/trust.ncl +++ /dev/null @@ -1,88 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# Trust — security + safe-hacking runner -# -# Pairs with: Trustfile.a2ml (same directory) -# Verb: trust -# Semantics: integrity / provenance / security verification PLUS a declared -# "safe hacking + testing" section — authorised offensive probes -# (pen-test harness runs, chaos-engineering probes) scoped to the -# repo under test, NEVER touching external systems. -# CLI: `contractile trust verify` → run all verifications (read-only) -# `contractile trust probe` → run declared safe-hacking probes -# -# Anything else in this directory is human-only notes/archive; machines ignore. -# -# Base: ../_base.ncl provides pedigree_schema, run_defaults, probe_schema. -# See: docs/CONTRACTILE-SPEC.adoc - -let base = import "../_base.ncl" in - -{ - pedigree = base.pedigree_schema & { - contractile_verb = "trust", - semantics = "security + provenance + safe-hacking", - security = { - leash = 'Kennel, - trust_level = "verification + authorised-probe", - allow_network = false, # verifications are offline by default - allow_filesystem_write = false, # trust writes NOTHING - allow_subprocess = true, - authorised_probes_only = true, # probe section must explicitly list allowed targets - }, - metadata = { - name = "trust-runner", - version = "1.0.0", - description = "Security + provenance verifications plus authorised safe-hacking probes. All probes are scoped to the repo under test; never hits external systems.", - paired_xfile = "Trustfile.a2ml", - author = "Jonathan D.A. Jewell ", - }, - }, - - schema = { - verifications - | Array { - id | String, - description | String, - # TODO: migrate to base.probe_schema (structured probe) when CLI supports it - probe | String, # read-only; exit 0 = pass - # status_core values: 'declared, 'verified, 'failing - status | [| 'declared, 'verified, 'failing |] | default = 'declared, - # trust uses all four severity levels (from base.severity_core) - severity | [| 'critical, 'high, 'medium, 'low |] | default = 'high, - notes | String | optional, - }, - - # Safe-hacking + testing section (added 2026-04-17 per user direction). - # Each probe here is an ACTIVELY EXECUTED test — fuzz runs, chaos probes, - # auth-bypass attempts, injection tests. All scoped to the current repo. - safe_hacking - | { - scope | String, # e.g. "this-repo-only" / "localhost" - allowed_probe_classes - | Array [| 'fuzz, 'property_test, 'chaos, 'auth_bypass, 'injection, 'timing |] - | default = [], - probes - | Array { - id | String, - class | [| 'fuzz, 'property_test, 'chaos, 'auth_bypass, 'injection, 'timing |], - description | String, - # TODO: migrate to base.probe_schema (structured probe) when CLI supports it - probe | String, # command to run the probe - expected_outcome | [| 'probe_blocks_attempt, 'probe_finds_no_issue |], - timeout_seconds | Number | default = 300, - notes | String | optional, - } - | default = [], - } - | default = { scope = "this-repo-only", allowed_probe_classes = [], probes = [] }, - }, - - # Runner behaviour — inherits from base.run_defaults. - # trust has an extra field for unexpected safe-hacking outcomes. - run = base.run_defaults & { - on_any_fail = "exit-nonzero", # hard gate on verifications - safe_hacking_on_unexpected_outcome = "exit-nonzero", # probe found what it shouldn't = block - report_format = "a2ml", - emit_summary = true, - }, -} diff --git a/.machine_readable/svc/k9/ephapax-metadata.k9.ncl b/.machine_readable/self-validating/ephapax-metadata.k9.ncl similarity index 100% rename from .machine_readable/svc/k9/ephapax-metadata.k9.ncl rename to .machine_readable/self-validating/ephapax-metadata.k9.ncl diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc new file mode 100644 index 00000000..8bbf167d --- /dev/null +++ b/GOVERNANCE.adoc @@ -0,0 +1,162 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Governance Model +:toc: preamble + +This document describes the governance model for this repository. + +== Overview + +This repository follows a **Sole Maintainer Governance Model**: + +* Single maintainer (@hyperpolymath) has full authority over the project +* All contributions are welcome and reviewed by the maintainer +* Decisions are made transparently through GitHub issues and discussions +* The project adheres to the hyperpolymath estate policies where applicable + +== Core Principles + +[cols="1,2"] +|=== +| Principle | Description + +| **Benevolent Dictatorship** | Maintainer has final decision authority but seeks community input + +| **Meritocracy** | Contributions are judged on technical merit, not contributor identity + +| **Transparency** | All significant decisions are documented publicly + +| **Consensus-Seeking** | Maintainer prefers consensus but will decide when necessary + +| **Open Contribution** | Anyone can contribute via fork and pull request + +|=== + +== Roles and Permissions + +[cols="1,2,2"] +|=== +| Role | Permissions | Assignment + +| **Maintainer** | Write access, merge rights, admin | @hyperpolymath +| **Contributors** | Read access, fork, submit PRs | All GitHub users +| **Users** | Use the software, report issues | All GitHub users + +|=== + +== Decision Making Framework + +=== Routine Decisions + +* Bug fixes +* Documentation improvements +* Minor feature additions +* Dependency updates + +**Process**: Maintainer reviews and merges PRs that meet quality standards. + +=== Significant Changes + +* New major features +* API changes +* Architecture modifications +* Breaking changes + +**Process**: +. Open issue describing the change +. Discuss with community (minimum 72 hours) +. Maintainer makes final decision +. Document rationale in issue/PR + +=== Structural Decisions + +* Repository purpose/renaming +* License changes +* Ownership transfer +* Deprecation/archival + +**Process**: +. Extended discussion (minimum 1 week) +. Maintainer makes final decision +. Document in CHANGELOG and governance docs + +== Contribution Lifecycle + +[cols="1,2"] +|=== +| Stage | Process + +| **Ideation** | Open issue, discuss feasibility + +| **Development** | Fork, implement, test thoroughly + +| **Review** | Submit PR, maintainer reviews within 7 days + +| **Merge** | Maintainer merges or requests changes + +| **Release** | Maintainer publishes according to project conventions + +|=== + +== Conflict Resolution + +In case of disagreements: + +. Discuss in the relevant GitHub issue or PR +. Provide technical justification for positions +. Maintainer mediates and makes final decision +. Decision is documented and can be revisited later + +== Project Policies + +This repository adheres to hyperpolymath estate-wide policies: + +* **License**: MPL-2.0 for code, CC-BY-SA-4.0 for prose (per standards/LICENCE-POLICY.adoc) +* **Code of Conduct**: Follows hyperpolymath CODE_OF_CONDUCT.md +* **Security**: Follows hyperpolymath SECURITY.md +* **Contributing**: Follows hyperpolymath CONTRIBUTING.adoc conventions + +== Repository-Specific Conventions + +[cols="1,2"] +|=== +| Convention | Description + +| **Signing** | All commits must be signed (SSH or GPG) + +| **SPDX Headers** | All source files must have SPDX license identifiers + +| **Contractiles** | Mustfile, Trustfile, Intendfile, Adjustfile in root + +| **Machine Readable** | META.a2ml in .machine_readable/6a2/ + +| **CI/CD** | GitHub Actions workflows in .github/workflows/ + +|=== + +== Governance Evolution + +As the project grows, this governance model may evolve: + +* **Adding Co-Maintainers**: When contribution volume warrants it +* **Forming a Team**: For complex multi-maintainer projects +* **Adopting TPCF**: For large, multi-repository projects (see rhodium-standard-repositories) + +Changes to this document require the same process as Significant Changes above. + +== See Also + +* link:MAINTAINERS.adoc[Maintainers] +* link:CODE_OF_CONDUCT.md[Code of Conduct] +* link:CONTRIBUTING.adoc[Contributing Guide] +* link:https://github.com/hyperpolymath/standards/blob/main/LICENCE-POLICY.adoc[Estate License Policy] +* link:https://github.com/hyperpolymath/standards[rhodium-standard-repositories (TPCF)] + +== Changelog + +[cols="1,1,1"] +|=== +| Date | Change | By + +| 2026-06-07 | Initial governance model established | @hyperpolymath +|=== diff --git a/MAINTAINERS.adoc b/MAINTAINERS.adoc new file mode 100644 index 00000000..9910dd8f --- /dev/null +++ b/MAINTAINERS.adoc @@ -0,0 +1,65 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Maintainers +:toc: preamble + +== Current Maintainers + +[cols="2,3,2",options="header"] +|=== +| Name | Role | Contact + +| Jonathan D.A. Jewell | Sole Maintainer | https://github.com/hyperpolymath[@hyperpolymath] +|=== + +== Maintainer Responsibilities + +As the sole maintainer, all responsibilities apply to @hyperpolymath: + +* Reviewing and merging pull requests +* Triaging issues and feature requests +* Ensuring code quality and security standards +* Managing releases and versioning +* Upholding the project's Code of Conduct +* Maintaining documentation and examples +* Responding to security vulnerabilities + +== Contribution Process + +This is a sole-maintainer project. All contributions are welcome via: + +1. **Issues**: Report bugs, request features, ask questions +2. **Pull Requests**: Submit improvements for review +3. **Discussions**: Engage in community discussions + +All contributions will be reviewed by the maintainer. + +== Decision Making + +* Routine decisions (bug fixes, minor improvements): Made by maintainer +* Significant changes: Discussed in issues before implementation +* Breaking changes: Announced in advance with migration path + +== Becoming a Maintainer + +This project currently has a single maintainer. If you're interested in becoming a co-maintainer: + +1. Demonstrate consistent, high-quality contributions +2. Show understanding of project goals and standards +3. Participate constructively in discussions +4. Express interest to the current maintainer + +Co-maintainers may be added at the discretion of the current maintainer. + +== Contact + +For questions about project governance: + +* Open a GitHub issue in this repository +* Contact: https://github.com/hyperpolymath + +== See Also + +* link:GOVERNANCE.adoc[Governance Model] +* link:CODE_OF_CONDUCT.md[Code of Conduct] +* link:CONTRIBUTING.adoc[Contributing Guide] diff --git a/contractiles/intend/Intentfile.a2ml b/contractiles/intend/Intentfile.a2ml deleted file mode 100644 index 8aae9f13..00000000 --- a/contractiles/intend/Intentfile.a2ml +++ /dev/null @@ -1,22 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# Intentfile (A2ML Canonical) -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -@abstract: -Declared intent and purpose for Ephapax. -@end - -## Purpose - -Ephapax — // SPDX-License-Identifier: PMPL-1.0-or-later - -## Anti-Purpose - -This project is NOT: -- A fork or wrapper around another tool -- A monorepo (unless explicitly structured as one) - -## If In Doubt - -If you are unsure whether a change is in scope, ask. -Sensitive areas: ABI definitions, license headers, CI workflows. diff --git a/contractiles/must/Mustfile.a2ml b/contractiles/must/Mustfile.a2ml deleted file mode 100644 index dc870c0f..00000000 --- a/contractiles/must/Mustfile.a2ml +++ /dev/null @@ -1,42 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# Mustfile (A2ML Canonical) -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -@abstract: -Physical State contract for Ephapax. Baseline UX Manifesto invariants -that MUST hold at all times. -@end - -@requires: -- section: Core-Files -- section: Banned -@end - -## Core-Files - -### license-present -- description: LICENSE file must exist -- run: test -f LICENSE -- severity: critical - -### readme-present -- description: README must exist -- run: test -f README.adoc || test -f README.md -- severity: critical - -## Banned - -### no-hardcoded-paths -- description: No hardcoded developer paths -- run: "! grep -rn '$HOME\|$ECLIPSE_DIR' --include='*.rs' --include='*.res' --include='*.ex' --include='*.gleam' --include='*.zig' --include='*.sh' . 2>/dev/null | grep -v '.git/' | grep -v 'ux-rollout.jl' | head -1" -- severity: critical - -### no-dockerfiles -- description: No Dockerfiles (use Containerfile) -- run: test ! -f Dockerfile -- severity: warning - -### no-makefiles -- description: No Makefiles (use Justfile) -- run: test ! -f Makefile -- severity: warning diff --git a/contractiles/trust/Trustfile.a2ml b/contractiles/trust/Trustfile.a2ml deleted file mode 100644 index 600c23f6..00000000 --- a/contractiles/trust/Trustfile.a2ml +++ /dev/null @@ -1,25 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# Trustfile (A2ML Canonical) -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) - -@abstract: -Trust and provenance verification for Ephapax. -Maximal trust by default — LLM may read, build, test, lint, format. -@end - -@trust-level: maximal -@trust-boundary: repo -@trust-actions: [read, build, test, lint, format] -@trust-deny: [delete-branch, force-push, modify-ci-secrets, publish] - -## Integrity - -### license-content -- description: LICENSE contains expected SPDX identifier -- run: grep -q 'SPDX\|License\|MIT\|Apache\|PMPL\|MPL' LICENSE -- severity: critical - -### no-secrets-committed -- description: No .env or credential files in repo -- run: test ! -f .env && test ! -f credentials.json && test ! -f .env.local -- severity: critical diff --git a/docs/sessions/SESSION-2026-05-20-proof-engineering-lessons.adoc b/docs/sessions/SESSION-2026-05-20-proof-engineering-lessons.adoc index aa244f74..09c19af0 100644 --- a/docs/sessions/SESSION-2026-05-20-proof-engineering-lessons.adoc +++ b/docs/sessions/SESSION-2026-05-20-proof-engineering-lessons.adoc @@ -14,7 +14,7 @@ Each lesson is named, has a reproducer, and lists where in the codebase the pattern bit us so the cross-reference is auditable. Companion machine-readable artefact: -`.machine_readable/agent_instructions/lessons.a2ml`. +`.machine_readable/bot_directives/lessons.a2ml`. PRs that surfaced these (this repo, 2026-05-20): proof-of-work#63, ephapax#92, ephapax#95, ephapax#98, ephapax#102, diff --git a/flake.nix b/flake.nix deleted file mode 100644 index 6aeaab90..00000000 --- a/flake.nix +++ /dev/null @@ -1,116 +0,0 @@ -{ - description = "ephapax - {project-description}"; - - # *REMINDER: Update inputs with actual dependencies* - inputs = { - nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable"; - flake-utils.url = "github:numtide/flake-utils"; - # Add language-specific inputs: - # rust-overlay.url = "github:oxalica/rust-overlay"; # For Rust - # fenix.url = "github:nix-community/fenix"; # Alternative Rust - }; - - outputs = { self, nixpkgs, flake-utils, ... }@inputs: - flake-utils.lib.eachDefaultSystem (system: - let - pkgs = import nixpkgs { - inherit system; - # overlays = [ (import inputs.rust-overlay) ]; # For Rust - }; - - # *REMINDER: Define build dependencies* - buildInputs = with pkgs; [ - # Language-specific dependencies: - # gnat13 # Ada - # cargo rustc # Rust - # elixir # Elixir - # For build tools: - just - podman - git - ]; - - # *REMINDER: Define development dependencies* - nativeBuildInputs = with pkgs; [ - # Development tools: - ripgrep # Code search - lychee # Link validation - # Language-specific: - # rustfmt clippy # Rust - # mix # Elixir - ]; - - in - { - # Development shell - devShells.default = pkgs.mkShell { - inherit buildInputs nativeBuildInputs; - - shellHook = '' - echo "🚀 ephapax development environment" - echo "Language: rust" - echo "" - echo "Available commands:" - echo " just --list # Show all tasks" - echo " just setup # Set up environment" - echo " just build # Build project" - echo " just test # Run tests" - echo " just validate # RSR compliance" - echo "" - # *REMINDER: Add language-specific environment setup* - # export CARGO_HOME=$PWD/.cargo # Rust - # export MIX_HOME=$PWD/.mix # Elixir - ''; - }; - - # Packages - packages.default = pkgs.stdenv.mkDerivation { - pname = "ephapax"; - version = "0.1.0"; - src = ./.; - - inherit buildInputs nativeBuildInputs; - - buildPhase = '' - # *REMINDER: Add build commands* - # For Rust: cargo build --release - # For Elixir: mix compile - # For Ada: gprbuild -P ephapax.gpr -XMODE=release - ''; - - installPhase = '' - mkdir -p $out/bin - # *REMINDER: Add install commands* - # cp target/release/ephapax $out/bin/ # Rust - # cp bin/ephapax $out/bin/ # Ada - ''; - - meta = with pkgs.lib; { - description = "{project-description}"; - homepage = "{repo-url}"; - license = with licenses; [ mit ]; # MIT + Palimpsest - maintainers = [ "{maintainer-name}" ]; - platforms = platforms.unix; - }; - }; - - # Apps - apps.default = { - type = "app"; - program = "${self.packages.${system}.default}/bin/ephapax"; - }; - - # Checks (CI/CD integration) - checks = { - build = self.packages.${system}.default; - # *REMINDER: Add test checks* - test = pkgs.runCommand "test-ephapax" { - buildInputs = [ self.packages.${system}.default ]; - } '' - # Run tests here - touch $out - ''; - }; - } - ); -} diff --git a/formal/Semantics.v b/formal/Semantics.v index 4680bbc7..0b728c1f 100644 --- a/formal/Semantics.v +++ b/formal/Semantics.v @@ -5982,11 +5982,213 @@ Proof. end). Admitted. +(** ** Step safety for preservation + + The current preservation theorem in ephapax has a known gap: when + a step exits a region [r] (via [S_Region_Exit] possibly nested + via congruence) and a sibling sub-expression of [e] syntactically + references [r], the post-step typing fails because [r] is no + longer in [R']. + + Path 2 reformulation: add a [safe_for_step] precondition that + excludes exactly this scenario. It says "any region the step + removes is not syntactically referenced outside its own [ERegion] + scopes in [e]." + + The condition is satisfied by: + - Non-region-changing steps (no [r] is removed). + - [S_Region_Enter] steps (no [r] is removed). + - Region-exiting steps where the exited region wasn't referenced + by sibling expressions (the typical well-scoped case). + + Excluded: programs that nest [ERegion r] usages such that a + sibling outside the nested scope references [r]. Such programs + are typeable in ephapax but break preservation; the precondition + makes the gap explicit at the user-facing level. *) + +Definition safe_for_step (e : expr) (R R' : region_env) : Prop := + forall r, In r R -> ~ In r R' -> expr_free_of_region r e. + +(** Trivial discharge: any step where [R = R'] satisfies [safe_for_step] vacuously. *) +Lemma safe_for_step_R_eq : + forall e R, safe_for_step e R R. +Proof. + unfold safe_for_step. intros e R r Hin Hnin. contradiction. +Qed. + +(** Trivial discharge: any step where [R' = r :: R] satisfies + [safe_for_step] (no region is removed). *) +Lemma safe_for_step_R_add : + forall e R r, safe_for_step e R (r :: R). +Proof. + unfold safe_for_step. intros e R r r0 Hin Hnin. exfalso. apply Hnin. right; exact Hin. +Qed. + +(** Projection helpers: for each compound-expression shape, deriving + [safe_for_step] on a sub-expression from [safe_for_step] on the + whole. Used in [preservation]'s congruence cases to thread Hsafe + to the IH application. *) + +Lemma safe_for_step_StringConcat_l : forall e1 e2 R R', + safe_for_step (EStringConcat e1 e2) R R' -> safe_for_step e1 R R'. +Proof. unfold safe_for_step. intros e1 e2 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [Hf _]. exact Hf. Qed. + +Lemma safe_for_step_StringConcat_r : forall e1 e2 R R', + safe_for_step (EStringConcat e1 e2) R R' -> safe_for_step e2 R R'. +Proof. unfold safe_for_step. intros e1 e2 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [_ Hf]. exact Hf. Qed. + +Lemma safe_for_step_StringLen : forall e R R', + safe_for_step (EStringLen e) R R' -> safe_for_step e R R'. +Proof. unfold safe_for_step. intros e R R' H r Hin Hnin. exact (H r Hin Hnin). Qed. + +Lemma safe_for_step_Let_l : forall e1 e2 R R', + safe_for_step (ELet e1 e2) R R' -> safe_for_step e1 R R'. +Proof. unfold safe_for_step. intros e1 e2 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [Hf _]. exact Hf. Qed. + +Lemma safe_for_step_Let_r_body : forall e1 e2 R R', + safe_for_step (ELet e1 e2) R R' -> safe_for_step e2 R R'. +Proof. unfold safe_for_step. intros e1 e2 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [_ Hf]. exact Hf. Qed. + +Lemma safe_for_step_LetLin_l : forall e1 e2 R R', + safe_for_step (ELetLin e1 e2) R R' -> safe_for_step e1 R R'. +Proof. unfold safe_for_step. intros e1 e2 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [Hf _]. exact Hf. Qed. + +Lemma safe_for_step_LetLin_r_body : forall e1 e2 R R', + safe_for_step (ELetLin e1 e2) R R' -> safe_for_step e2 R R'. +Proof. unfold safe_for_step. intros e1 e2 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [_ Hf]. exact Hf. Qed. + +Lemma safe_for_step_App_l : forall e1 e2 R R', + safe_for_step (EApp e1 e2) R R' -> safe_for_step e1 R R'. +Proof. unfold safe_for_step. intros e1 e2 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [Hf _]. exact Hf. Qed. + +Lemma safe_for_step_App_r : forall e1 e2 R R', + safe_for_step (EApp e1 e2) R R' -> safe_for_step e2 R R'. +Proof. unfold safe_for_step. intros e1 e2 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [_ Hf]. exact Hf. Qed. + +Lemma safe_for_step_Pair_l : forall e1 e2 R R', + safe_for_step (EPair e1 e2) R R' -> safe_for_step e1 R R'. +Proof. unfold safe_for_step. intros e1 e2 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [Hf _]. exact Hf. Qed. + +Lemma safe_for_step_Pair_r : forall e1 e2 R R', + safe_for_step (EPair e1 e2) R R' -> safe_for_step e2 R R'. +Proof. unfold safe_for_step. intros e1 e2 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [_ Hf]. exact Hf. Qed. + +Lemma safe_for_step_If_cond : forall e1 e2 e3 R R', + safe_for_step (EIf e1 e2 e3) R R' -> safe_for_step e1 R R'. +Proof. unfold safe_for_step. intros e1 e2 e3 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [Hf _]. exact Hf. Qed. + +Lemma safe_for_step_If_branch_2 : forall e1 e2 e3 R R', + safe_for_step (EIf e1 e2 e3) R R' -> safe_for_step e2 R R'. +Proof. unfold safe_for_step. intros e1 e2 e3 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [_ [Hf _]]. exact Hf. Qed. + +Lemma safe_for_step_If_branch_3 : forall e1 e2 e3 R R', + safe_for_step (EIf e1 e2 e3) R R' -> safe_for_step e3 R R'. +Proof. unfold safe_for_step. intros e1 e2 e3 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [_ [_ Hf]]. exact Hf. Qed. + +Lemma safe_for_step_Case_scrut : forall e e1 e2 R R', + safe_for_step (ECase e e1 e2) R R' -> safe_for_step e R R'. +Proof. unfold safe_for_step. intros e e1 e2 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [Hf _]. exact Hf. Qed. + +Lemma safe_for_step_Case_branch_l : forall e e1 e2 R R', + safe_for_step (ECase e e1 e2) R R' -> safe_for_step e1 R R'. +Proof. unfold safe_for_step. intros e e1 e2 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [_ [Hf _]]. exact Hf. Qed. + +Lemma safe_for_step_Case_branch_r : forall e e1 e2 R R', + safe_for_step (ECase e e1 e2) R R' -> safe_for_step e2 R R'. +Proof. unfold safe_for_step. intros e e1 e2 R R' H r Hin Hnin. + destruct (H r Hin Hnin) as [_ [_ Hf]]. exact Hf. Qed. + +Lemma safe_for_step_Fst : forall e R R', + safe_for_step (EFst e) R R' -> safe_for_step e R R'. +Proof. unfold safe_for_step. intros e R R' H r Hin Hnin. exact (H r Hin Hnin). Qed. + +Lemma safe_for_step_Snd : forall e R R', + safe_for_step (ESnd e) R R' -> safe_for_step e R R'. +Proof. unfold safe_for_step. intros e R R' H r Hin Hnin. exact (H r Hin Hnin). Qed. + +Lemma safe_for_step_Inl : forall T e R R', + safe_for_step (EInl T e) R R' -> safe_for_step e R R'. +Proof. unfold safe_for_step. intros T e R R' H r Hin Hnin. exact (H r Hin Hnin). Qed. + +Lemma safe_for_step_Inr : forall T e R R', + safe_for_step (EInr T e) R R' -> safe_for_step e R R'. +Proof. unfold safe_for_step. intros T e R R' H r Hin Hnin. exact (H r Hin Hnin). Qed. + +Lemma safe_for_step_Borrow : forall e R R', + safe_for_step (EBorrow e) R R' -> safe_for_step e R R'. +Proof. unfold safe_for_step. intros e R R' H r Hin Hnin. exact (H r Hin Hnin). Qed. + +Lemma safe_for_step_Drop : forall e R R', + safe_for_step (EDrop e) R R' -> safe_for_step e R R'. +Proof. unfold safe_for_step. intros e R R' H r Hin Hnin. exact (H r Hin Hnin). Qed. + +Lemma safe_for_step_Copy : forall e R R', + safe_for_step (ECopy e) R R' -> safe_for_step e R R'. +Proof. unfold safe_for_step. intros e R R' H r Hin Hnin. exact (H r Hin Hnin). Qed. + +(** [sibling_transport]: under [safe_for_step], a sibling typing at + [R] can be lifted to a typing at [R'] post-step, regardless of + which of the three R-shapes (equal / prepend / shrink) applies. + + Proof dispatches on [step_R_change_shape]: + - LEFT (R = R'): identity. + - MIDDLE (R' = r :: R): [region_add_typing]. + - RIGHT (R' = remove_first r R, In r R) splits further: + * If [In r R'] (the removed region was duplicated): membership + of R and R' agree, use [region_env_perm_typing]. + * If [~In r R'] (the removed region was unique): use + [safe_for_step]'s hypothesis to derive + [expr_free_of_region r e], then [region_shrink_preserves_typing]. *) +Lemma sibling_transport : + forall mu R mu' R' e_step e_step', + (mu, R, e_step) -->> (mu', R', e_step') -> + forall e_sib G T G', + R; G |- e_sib : T -| G' -> + safe_for_step e_sib R R' -> + R'; G |- e_sib : T -| G'. +Proof. + intros mu R mu' R' e_step e_step' Hstep e_sib G T G' Htype Hsafe. + pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) + as [HeqR | [[r [Hadd Hnotin]] | [r [Hrem HinR]]]]. + - subst R'. exact Htype. + - subst R'. apply region_add_typing. exact Htype. + - subst R'. + destruct (in_dec String.string_dec r (remove_first r R)) as [HinRem | HninRem]. + + (* r duplicated: membership equal, perm *) + eapply region_env_perm_typing. + * exact Htype. + * intro r0. + destruct (String.eqb r r0) eqn:Heqrr0. + -- apply String.eqb_eq in Heqrr0. subst r0. + split; intros; [exact HinRem | exact HinR]. + -- apply String.eqb_neq in Heqrr0. + apply (region_shrink_in_preserves r r0 R). exact Heqrr0. + + (* r unique: use safe_for_step *) + pose proof (Hsafe r HinR HninRem) as Hfree. + apply region_shrink_preserves_typing; assumption. +Qed. + Theorem preservation : forall mu R e mu' R' e', (mu, R, e) -->> (mu', R', e') -> forall G T G', R; G |- e : T -| G' -> + safe_for_step e R R' -> exists G_out, R'; G |- e' : T -| G_out. Proof. intros mu R e mu' R' e' Hstep. @@ -6021,7 +6223,7 @@ Proof. pass have unusable IHs. *) revert mu R e mu' R' e' Hcfg Hcfg'. induction Hstep; intros mu0 R0 e0 mu0' R0' e0' Hcfg Hcfg'; - intros G0 T0 G0' Htype; + intros G0 T0 G0' Htype Hsafe; inversion Hcfg; subst; inversion Hcfg'; subst; inversion Htype; subst; @@ -6036,11 +6238,33 @@ Proof. as the inner expression, the inner step hypothesis is immediately impossible). *) try solve [exfalso; match goal with [ H : (_, _, EVar _) -->> _ |- _ ] => inversion H end]. - (* Congruence: IH + reconstruct *) - all: try solve [match goal with [ IH : forall _ _ _, _ -> exists _, _ |- _ ] => + (* Congruence: IH + reconstruct. The IH now requires safe_for_step + for the inner expression — derive it from outer Hsafe via the + per-shape projection lemmas. For single-child compounds with + a single typed sub-expression, the IH + Hsafe-projection + + econstructor closes. *) + all: try solve [ match goal with [ H : has_type _ _ _ _ _ |- _ ] => - destruct (IH _ _ _ H) as [? ?]; - eexists; econstructor; try eassumption end end]. + first + [ destruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H + (safe_for_step_Fst _ _ _ Hsafe)) as [? ?] + | destruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H + (safe_for_step_Snd _ _ _ Hsafe)) as [? ?] + | destruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H + (safe_for_step_Inl _ _ _ _ Hsafe)) as [? ?] + | destruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H + (safe_for_step_Inr _ _ _ _ Hsafe)) as [? ?] + | destruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H + (safe_for_step_Borrow _ _ _ Hsafe)) as [? ?] + | destruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H + (safe_for_step_Drop _ _ _ Hsafe)) as [? ?] + | destruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H + (safe_for_step_Copy _ _ _ Hsafe)) as [? ?] + | destruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H + (safe_for_step_StringLen _ _ _ Hsafe)) as [? ?] + ]; + eexists; econstructor; try eassumption + end]. all: try solve [eexists; econstructor; try eassumption]. all: try solve [eexists; eassumption]. all: try solve [exfalso; congruence]. @@ -6373,192 +6597,219 @@ Proof. RIGHT branch (touches_region) is independently open — needs region weakening for non-values. *) - (* S_StringConcat_Step1: inner step is on e1. Use step_R_change_shape - for 3-way dispatch. LEFT and MIDDLE close via has_type_lift on the - sibling. RIGHT (remove_first) blocked on sibling-might-reference-r. *) + (* S_StringConcat_Step1: unified via sibling_transport (handles all + three R-shapes for the unchanged sibling e2) + step_output_context_eq + (bridges the post-step e1's output context to e2's input context). *) all: try solve [ match goal with | [ H1 : has_type ?R ?G ?e1 (TString ?r0) ?Gmid, H2 : has_type ?R ?Gmid ?e2 (TString ?r0) ?Gout1 |- exists _ : ctx, has_type ?Rp ?G (EStringConcat ?e1' ?e2) (TString ?r0) _ ] => - pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) - as [HeqR | [[r [Hadd Hnotin]] | [r [Hrem HinR]]]]; - [ rewrite HeqR in *; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout2 Hout]; - eexists; eapply T_StringConcat; [exact Hout | exact H2] - | subst Rp; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout2 Hout]; - pose proof (region_add_typing _ _ _ _ _ r H2) as H2lift; - eexists; eapply T_StringConcat; [exact Hout | exact H2lift] - | fail ] + edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1 + (safe_for_step_StringConcat_l _ _ _ _ Hsafe)) + as [Gout2 Hout]; + pose proof (sibling_transport _ _ _ _ _ _ Hstep _ _ _ _ H2 + (safe_for_step_StringConcat_r _ _ _ _ Hsafe)) + as H2lift; + pose proof (step_output_context_eq _ _ _ _ _ _ Hstep _ _ _ _ H1 Hout) as HGeq; + subst Gout2; + eexists; eapply T_StringConcat; [exact Hout | exact H2lift] end ]. - (* S_StringConcat_Step2: inner step is on e2; v1 is a value so - value_context_unchanged ⇒ v1's post-context equals its pre-context. *) + (* S_StringConcat_Step2: v1 is a value, e2 steps. Unified via + value_context_unchanged (aligns Gmid) + sibling_transport on v1 + (lifts v1's typing to R') + IH on e2. *) all: try solve [ match goal with | [ Hv : is_value ?v1, H1 : has_type ?R ?G ?v1 (TString ?r0) ?Gmid, H2 : has_type ?R ?Gmid ?e2 (TString ?r0) ?G' |- exists _ : ctx, has_type ?R' ?G (EStringConcat ?v1 ?e2') (TString ?r0) _ ] => - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hstep) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ rewrite <- HeqR; - assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; eassumption); - subst Gmid; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H2) as [Gout Hout]; - eexists; eapply T_StringConcat; [exact H1 | exact Hout] - | fail ] + assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; eassumption); + subst Gmid; + edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H2 + (safe_for_step_StringConcat_r _ _ _ _ Hsafe)) + as [Gout Hout]; + pose proof (sibling_transport _ _ _ _ _ _ Hstep _ _ _ _ H1 + (safe_for_step_StringConcat_l _ _ _ _ Hsafe)) + as H1lift; + eexists; eapply T_StringConcat; [exact H1lift | exact Hout] end ]. - (* S_StringLen_Step: Hb: EBorrow e : TBorrow (TString r). IH is on - the inner step on e; invert Hb to get e's typing, feed to IH, - reconstruct EStringLen e' via T_StringLen ∘ T_Borrow. *) + (* S_StringLen_Step: EStringLen e → EStringLen e'. T_StringLen's + body is typed at TBorrow (TString r), meaning body = EBorrow (...). + Inverting Hb (T_Borrow / T_Borrow_Val) forces the body's inner + to be EVar or value — neither of which steps. So this case is + vacuous: contradicts Hstep via values_dont_step or EVar-can't-step. *) all: try solve [ match goal with - | [ Hb : has_type ?R ?G (EBorrow ?e) (TBorrow (TString ?r0)) ?G' - |- exists _ : ctx, has_type ?R' ?G (EStringLen ?e') (TBase TI32) _ ] => - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hstep) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ rewrite <- HeqR; - inversion Hb; subst; - match goal with - | [ Het : has_type ?R ?G ?e (TString ?r0) ?Ge |- _ ] => - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ Het) as [Gout Hout]; - eexists; eapply T_StringLen; eapply T_Borrow; exact Hout - end - | fail ] + | [ Hb : has_type ?R ?G (EBorrow ?e_inner) (TBorrow (TString ?r0)) ?G' + |- _ ] => + inversion Hb; subst; + first + [ exfalso; + match goal with + | [ H : (_, _, EVar _) -->> _ |- _ ] => inversion H + end + | exfalso; eapply values_dont_step; eassumption ] end ]. - (* S_Let_Step *) + (* S_Let_Step: e1 steps, e2 (body) unchanged. *) all: try solve [ match goal with | [ H1 : has_type ?R ?G ?e1 ?T1 ?Gmid, H2 : has_type ?R (ctx_extend ?Gmid ?T1) ?e2 ?T0 ((?T1, true) :: ?G') |- exists _ : ctx, has_type ?R' ?G (ELet ?e1' ?e2) ?T0 _ ] => - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hstep) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ rewrite <- HeqR; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - eexists; eapply T_Let; [exact Hout | exact H2] - | fail ] + edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1 + (safe_for_step_Let_l _ _ _ _ Hsafe)) + as [Gout Hout]; + pose proof (sibling_transport _ _ _ _ _ _ Hstep _ _ _ _ H2 + (safe_for_step_Let_r_body _ _ _ _ Hsafe)) + as H2lift; + pose proof (step_output_context_eq _ _ _ _ _ _ Hstep _ _ _ _ H1 Hout) as HGeq; + subst Gout; + eexists; eapply T_Let; [exact Hout | exact H2lift] end ]. - (* S_LetLin_Step *) + (* S_LetLin_Step: same structure as S_Let_Step. *) all: try solve [ match goal with | [ Hlin : is_linear_ty ?T1 = true, H1 : has_type ?R ?G ?e1 ?T1 ?Gmid, H2 : has_type ?R (ctx_extend ?Gmid ?T1) ?e2 ?T0 ((?T1, true) :: ?G') |- exists _ : ctx, has_type ?R' ?G (ELetLin ?e1' ?e2) ?T0 _ ] => - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hstep) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ rewrite <- HeqR; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - eexists; eapply T_LetLin; [exact Hlin | exact Hout | exact H2] - | fail ] + edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1 + (safe_for_step_LetLin_l _ _ _ _ Hsafe)) + as [Gout Hout]; + pose proof (sibling_transport _ _ _ _ _ _ Hstep _ _ _ _ H2 + (safe_for_step_LetLin_r_body _ _ _ _ Hsafe)) + as H2lift; + pose proof (step_output_context_eq _ _ _ _ _ _ Hstep _ _ _ _ H1 Hout) as HGeq; + subst Gout; + eexists; eapply T_LetLin; [exact Hlin | exact Hout | exact H2lift] end ]. - (* S_App_Step1 *) + (* S_App_Step1: e1 steps, e2 unchanged. *) all: try solve [ match goal with | [ H1 : has_type ?R ?G ?e1 (TFun ?T1 ?T0) ?Gmid, H2 : has_type ?R ?Gmid ?e2 ?T1 ?G' |- exists _ : ctx, has_type ?R' ?G (EApp ?e1' ?e2) ?T0 _ ] => - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hstep) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ rewrite <- HeqR; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - eexists; eapply T_App; [exact Hout | exact H2] - | fail ] + edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1 + (safe_for_step_App_l _ _ _ _ Hsafe)) + as [Gout Hout]; + pose proof (sibling_transport _ _ _ _ _ _ Hstep _ _ _ _ H2 + (safe_for_step_App_r _ _ _ _ Hsafe)) + as H2lift; + pose proof (step_output_context_eq _ _ _ _ _ _ Hstep _ _ _ _ H1 Hout) as HGeq; + subst Gout; + eexists; eapply T_App; [exact Hout | exact H2lift] end ]. - (* S_App_Step2: v1 is a value so its post-context equals pre-context. *) + (* S_App_Step2: v1 is a value, e2 steps. *) all: try solve [ match goal with | [ Hv : is_value ?v1, H1 : has_type ?R ?G ?v1 (TFun ?T1 ?T0) ?Gmid, H2 : has_type ?R ?Gmid ?e2 ?T1 ?G' |- exists _ : ctx, has_type ?R' ?G (EApp ?v1 ?e2') ?T0 _ ] => - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hstep) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ rewrite <- HeqR; - assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; eassumption); - subst Gmid; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H2) as [Gout Hout]; - eexists; eapply T_App; [exact H1 | exact Hout] - | fail ] + assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; eassumption); + subst Gmid; + edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H2 + (safe_for_step_App_r _ _ _ _ Hsafe)) + as [Gout Hout]; + pose proof (sibling_transport _ _ _ _ _ _ Hstep _ _ _ _ H1 + (safe_for_step_App_l _ _ _ _ Hsafe)) + as H1lift; + eexists; eapply T_App; [exact H1lift | exact Hout] end ]. - (* S_If_Step *) + (* S_If_Step: cond steps, branches unchanged. *) all: try solve [ match goal with | [ H1 : has_type ?R ?G ?e1 (TBase TBool) ?Gmid, H2 : has_type ?R ?Gmid ?e2 ?T0 ?G', H3 : has_type ?R ?Gmid ?e3 ?T0 ?G' |- exists _ : ctx, has_type ?R' ?G (EIf ?e1' ?e2 ?e3) ?T0 _ ] => - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hstep) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ rewrite <- HeqR; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - eexists; eapply T_If; [exact Hout | exact H2 | exact H3] - | fail ] + edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1 + (safe_for_step_If_cond _ _ _ _ _ Hsafe)) + as [Gout Hout]; + pose proof (sibling_transport _ _ _ _ _ _ Hstep _ _ _ _ H2 + (safe_for_step_If_branch_2 _ _ _ _ _ Hsafe)) + as H2lift; + pose proof (sibling_transport _ _ _ _ _ _ Hstep _ _ _ _ H3 + (safe_for_step_If_branch_3 _ _ _ _ _ Hsafe)) + as H3lift; + pose proof (step_output_context_eq _ _ _ _ _ _ Hstep _ _ _ _ H1 Hout) as HGeq; + subst Gout; + eexists; eapply T_If; [exact Hout | exact H2lift | exact H3lift] end ]. - (* S_Pair_Step1 *) + (* S_Pair_Step1: e1 steps. *) all: try solve [ match goal with | [ H1 : has_type ?R ?G ?e1 ?T1 ?Gmid, H2 : has_type ?R ?Gmid ?e2 ?T2 ?G' |- exists _ : ctx, has_type ?R' ?G (EPair ?e1' ?e2) (TProd ?T1 ?T2) _ ] => - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hstep) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ rewrite <- HeqR; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - eexists; eapply T_Pair; [exact Hout | exact H2] - | fail ] + edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1 + (safe_for_step_Pair_l _ _ _ _ Hsafe)) + as [Gout Hout]; + pose proof (sibling_transport _ _ _ _ _ _ Hstep _ _ _ _ H2 + (safe_for_step_Pair_r _ _ _ _ Hsafe)) + as H2lift; + pose proof (step_output_context_eq _ _ _ _ _ _ Hstep _ _ _ _ H1 Hout) as HGeq; + subst Gout; + eexists; eapply T_Pair; [exact Hout | exact H2lift] end ]. - (* S_Pair_Step2: v1 is a value. *) + (* S_Pair_Step2: v1 value, e2 steps. Unified via value_context_unchanged + + sibling_transport on v1 + IH on e2. *) all: try solve [ match goal with | [ Hv : is_value ?v1, H1 : has_type ?R ?G ?v1 ?T1 ?Gmid, H2 : has_type ?R ?Gmid ?e2 ?T2 ?G' |- exists _ : ctx, has_type ?R' ?G (EPair ?v1 ?e2') (TProd ?T1 ?T2) _ ] => - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hstep) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ rewrite <- HeqR; - assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; eassumption); - subst Gmid; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H2) as [Gout Hout]; - eexists; eapply T_Pair; [exact H1 | exact Hout] - | fail ] + assert (Hgeq: Gmid = G) by (eapply value_context_unchanged; eassumption); + subst Gmid; + edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H2 + (safe_for_step_Pair_r _ _ _ _ Hsafe)) + as [Gout Hout]; + pose proof (sibling_transport _ _ _ _ _ _ Hstep _ _ _ _ H1 + (safe_for_step_Pair_l _ _ _ _ Hsafe)) + as H1lift; + eexists; eapply T_Pair; [exact H1lift | exact Hout] end ]. - (* S_Case_Step *) + (* S_Case_Step: scrutinee steps, branches unchanged. *) all: try solve [ match goal with | [ H1 : has_type ?R ?G ?e (TSum ?T1 ?T2) ?Gmid, H2 : has_type ?R (ctx_extend ?Gmid ?T1) ?e1 ?T0 ((?T1, true) :: ?G'), H3 : has_type ?R (ctx_extend ?Gmid ?T2) ?e2 ?T0 ((?T2, true) :: ?G') |- exists _ : ctx, has_type ?R' ?G (ECase ?e' ?e1 ?e2) ?T0 _ ] => - pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hstep) as Hdis; - destruct Hdis as [HeqR | HTR]; - [ rewrite <- HeqR; - edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1) as [Gout Hout]; - eexists; eapply T_Case; [exact Hout | exact H2 | exact H3] - | fail ] + edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H1 + (safe_for_step_Case_scrut _ _ _ _ _ Hsafe)) + as [Gout Hout]; + pose proof (sibling_transport _ _ _ _ _ _ Hstep _ _ _ _ H2 + (safe_for_step_Case_branch_l _ _ _ _ _ Hsafe)) + as H2lift; + pose proof (sibling_transport _ _ _ _ _ _ Hstep _ _ _ _ H3 + (safe_for_step_Case_branch_r _ _ _ _ _ Hsafe)) + as H3lift; + pose proof (step_output_context_eq _ _ _ _ _ _ Hstep _ _ _ _ H1 Hout) as HGeq; + subst Gout; + eexists; eapply T_Case; [exact Hout | exact H2lift | exact H3lift] end ]. @@ -6569,6 +6820,54 @@ Proof. requires either a typing invariant (sibling-region-disjointness) or a reformulation of preservation. *) + (* S_Region_Step: ERegion r0 e steps to ERegion r0 e' via inner + (e, e') step. Dispatch on step_R_change_shape: + - LEFT (R0 = R0'): inner Hsafe via safe_for_step_R_eq. + - MIDDLE (R0' = r1 :: R0): inner Hsafe via safe_for_step_R_add. + - RIGHT (R0' = remove_first r1 R0) with r1 ≠ r: outer Hsafe + restricted to r2 ≠ r0 gives the inner directly. + - RIGHT with r1 = r (inner exits outer's own region): admitted — + needs additional invariant on nested-region usage. *) + 1: { + pose proof (step_R_change_shape _ _ _ _ _ _ Hstep) as Hshape. + destruct Hshape as [HeqR | [[r1 [Hadd Hnotin]] | [r1 [Hrem HinR1]]]]. + - (* LEFT: R0' = R0 *) + subst R0'. + edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H8 + (safe_for_step_R_eq e _)) + as [Gout Hout]. + eexists. eapply T_Region_Active; [exact H2 | exact H5 | exact Hout]. + - (* MIDDLE: R0' = r1 :: R0 *) + subst R0'. + edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H8 + (safe_for_step_R_add e _ _)) + as [Gout Hout]. + eexists. eapply T_Region_Active; [right; exact H2 | exact H5 | exact Hout]. + - (* RIGHT: R0' = remove_first r1 R0, In r1 R0 *) + subst R0'. + destruct (String.eqb r1 r) eqn:Heqr1r. + + (* r1 = r: admit (the deeply-nested case) *) + admit. + + (* r1 ≠ r: derive inner Hsafe *) + apply String.eqb_neq in Heqr1r. + assert (Hinner_safe : safe_for_step e R0 (remove_first r1 R0)). + { unfold safe_for_step. intros r2 Hr2in Hr2nin. + pose proof (Hsafe r2 Hr2in Hr2nin) as Houter. + simpl in Houter. + destruct (String.eqb r2 r) eqn:Heqr2r. + - apply String.eqb_eq in Heqr2r. subst r2. + exfalso. apply Hr2nin. + apply (region_shrink_in_preserves r1 r R0 Heqr1r). exact Hr2in. + - destruct (String.eqb r r2) eqn:Heqrr2. + + apply String.eqb_eq in Heqrr2. subst r2. + apply String.eqb_neq in Heqr2r. contradiction. + + exact Houter. } + edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ H8 Hinner_safe) + as [Gout Hout]. + assert (Hin_r' : In r (remove_first r1 R0)) + by (apply (region_shrink_in_preserves r1 r R0 Heqr1r); exact H2). + eexists. eapply T_Region_Active; [exact Hin_r' | exact H5 | exact Hout]. + } Admitted. (* PROOF STATUS [preservation] — ADMITTED, down to 12 open goals (from 910 cross-case, via PR #102's remember-cfg + PR #106's diff --git a/formal/manifest.scm b/formal/manifest.scm new file mode 100644 index 00000000..dd942c7f --- /dev/null +++ b/formal/manifest.scm @@ -0,0 +1,24 @@ +;;; SPDX-License-Identifier: MPL-2.0 +;;; manifest.scm — Generic Guix manifest for RSR-compliant projects +;;; +;;; Usage: +;;; guix shell -m manifest.scm +;;; + +(specifications->manifest + '(;; Core development tools + "git" + "just" + "nickel" + "curl" + "bash" + "coreutils" + + ;; Documentation + "asciidoctor" + "pandoc" + + ;; Common build dependencies + "openssl" + "zlib" + "pkg-config"))