Land sweeps + first honest CI: compiler builds, proofs check, fail-closed gates

.github/funding.yml

@@ -0,0 +1,4 @@
+# Funding Configuration
+# See: https://docs.github.com/en/repositories/managing-your-repositorys-custom-fields/displaying-a-sponsor-button-in-your-repository
+
+github: metadatastician

.github/workflows/codeql.yml

@@ -32,11 +32,11 @@ jobs:
       - name: Checkout
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
       - name: Initialize CodeQL
-        uses: github/codeql-action/init@0d579ffd059c29b07949a3cce3983f0780820c98 # v3.28.1
+        uses: github/codeql-action/init@0d579ffd059c29b07949a3cce3983f0780820c98 # v3
         with:
           languages: ${{ matrix.language }}
           build-mode: ${{ matrix.build-mode }}
       - name: Perform CodeQL Analysis
-        uses: github/codeql-action/analyze@0d579ffd059c29b07949a3cce3983f0780820c98 # v3.28.1
+        uses: github/codeql-action/analyze@0d579ffd059c29b07949a3cce3983f0780820c98 # v3
         with:
           category: "/language:${{ matrix.language }}"

.github/workflows/proof-gates.yml

@@ -0,0 +1,137 @@
+# SPDX-License-Identifier: MPL-2.0
+#
+# Proof Gates — builds the real compiler and checks the real proofs.
+#
+# FAIL-CLOSED by design: a missing prover fails the job. This replaces
+# reliance on Rust CI (which "passes" by detecting no Cargo.toml and
+# skipping every job) and on `just proof-check-*` (which exits 0 when a
+# prover is absent). Nothing in this file is allowed to skip.
+#
+# Toolchain provenance:
+#   - compiler + agda jobs run in debian:trixie, the same distribution
+#     (and identical ocaml/dune/agda/agda-stdlib versions) the suite was
+#     verified against locally on 2026-08-03.
+#   - the idris2 job runs in a digest-pinned pack image; the suite was
+#     verified against BOTH idris2 0.7.0 (local) and 0.8.0 (this image).
+name: Proof Gates
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+  workflow_dispatch:
+permissions:
+  contents: read
+concurrency:
+  group: proof-gates-${{ github.ref }}
+  cancel-in-progress: true
+jobs:
+  compiler:
+    name: OCaml compiler + example matrix
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    container:
+      image: debian:trixie
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+      - name: Install toolchain (fail-closed)
+        run: |
+          apt-get update
+          apt-get install -y --no-install-recommends ocaml ocaml-dune
+          ocaml -version
+          dune --version
+      - name: Build compiler
+        working-directory: src/compiler
+        run: dune build
+      - name: Positive examples must type-check
+        run: |
+          KSC=src/compiler/_build/default/main.exe
+          fail=0
+          for f in examples/v2/*.ks; do
+            if ! "$KSC" check "$f"; then
+              echo "::error file=$f::positive example failed to type-check"
+              fail=1
+            fi
+          done
+          exit "$fail"
+      - name: Negative examples must be rejected
+        run: |
+          KSC=src/compiler/_build/default/main.exe
+          fail=0
+          for f in examples/v2/negative/*.ks; do
+            if "$KSC" check "$f" > /dev/null 2>&1; then
+              echo "::error file=$f::negative example was accepted (must be rejected)"
+              fail=1
+            fi
+          done
+          exit "$fail"
+
+  agda-proofs:
+    name: Agda proofs + trusted-base budget
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    container:
+      image: debian:trixie
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+      - name: Checkout echo-types (pinned)
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+        with:
+          repository: hyperpolymath/echo-types
+          ref: 900546a832ddfefb4fa48881cdebdc9b1260d1f9
+          path: .deps/echo-types
+      - name: Checkout absolute-zero (pinned)
+        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+        with:
+          repository: hyperpolymath/absolute-zero
+          ref: cef394b617869e1fa0d10f8fd9bdbba8db8d8738
+          path: .deps/absolute-zero
+      - name: Install Agda (fail-closed)
+        run: |
+          apt-get update
+          apt-get install -y --no-install-recommends agda agda-bin agda-stdlib
+          agda --version
+      - name: Check proofs
+        run: |
+          LIB="$PWD/.agda-libraries"
+          printf '%s\n' \
+            /usr/share/agda-stdlib/standard-library.agda-lib \
+            "$PWD/.deps/echo-types/echo-types.agda-lib" \
+            "$PWD/.deps/absolute-zero/absolute-zero.agda-lib" > "$LIB"
+          cd proofs/agda
+          # EchoBridge is postulate-free and must stay --safe.
+          agda --safe --library-file="$LIB" EchoBridge.agda
+          # The recipe proofs carry audited physical-world postulates
+          # (see TRUSTED-BASE.txt), so they check without --safe; the
+          # budget step below stops that trusted base growing silently.
+          for f in Dough.agda NoCurdle.agda PoachedEgg.agda; do
+            agda --library-file="$LIB" "$f"
+          done
+      - name: Trusted-base budget (no new postulates)
+        run: sh scripts/check-agda-trusted-base.sh
+
+  abi-proofs:
+    name: Idris2 ABI proof suite
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    container:
+      image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0dece3334c6a1d21d65334416e02d0e7b59da480644006b52c8b78c8cfc49f5
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
+      - name: Typecheck ABI proof suite (fail-closed)
+        working-directory: verification/proofs/idris2
+        run: |
+          idris2 --version
+          idris2 --typecheck kitchenspeak-abi-proofs.ipkg
+      - name: No dangerous escape hatches
+        run: |
+          # Matches code lines only; the file headers legitimately SAY
+          # "no believe_me, no assert_total" in comments, so lines whose
+          # content starts with the Idris comment marker are excluded.
+          hits=$(grep -rnE "believe_me|assert_total" verification/proofs/idris2 --include="*.idr" | grep -vE ":[[:space:]]*--" || true)
+          if [ -n "$hits" ]; then
+            echo "$hits"
+            echo "::error::dangerous escape hatch found in proof code"
+            exit 1
+          fi
+          echo "OK: no believe_me / assert_total in proof code."

.machine_readable/ECOSYSTEM.a2ml

@@ -2,7 +2,9 @@
 ;; Ecosystem position and relationships
 (ecosystem
   (version "1.0.0")
-  (name "{{REPO}}")
-  (type "library")
-  (purpose "{{REPO_DESCRIPTION}}")
-  (related-projects))
+  (name "kitchenspeak")
+  (type "language")
+  (purpose "Future kitchen orchestration language for IoT and IIoT")
+  (related-projects
+    (project "echo-types" "Agda Echo (fiber) substrate consumed by EchoBridge.agda")
+    (project "nextgen-languages" "coordinator that indexes this language")))

.machine_readable/META.a2ml

@@ -2,7 +2,7 @@
 ;; Architecture decisions and development practices
 (meta
   (version "1.0.0")
-  (project "{{REPO}}")
+  (project "kitchenspeak")
   (architecture-decisions)
   (development-practices
     (code-review "required")

.machine_readable/root-allow.txt

@@ -67,3 +67,20 @@ proofs/                    # Agda (now) / Lean (later) lowerings of the recipes
 .pre-commit-config.yaml    # TODO: relocate to ci/.pre-commit-config.yaml after invocation pattern decided
 affinescript/              # AffineScript source subtree consumed by this template
 tools/                     # TODO: consolidate with scripts/ or document the split (pending decision)
+
+# ─── Governance / community surfaces (GitHub reads these at root) ────────────
+# Added 2026-08-03 with the C-A-G-M sweep landing; GitHub's community-health
+# and OpenSSF tooling look for these exact root paths.
+CONTRIBUTING.md
+SECURITY.md
+GOVERNANCE.adoc
+GOVERNANCE.md              # C-A-G-M sweep counterpart of GOVERNANCE.adoc
+ARCHITECTURE.md            # C-A-G-M sweep architecture overview
+MAINTAINERS                # C-A-G-M sweep plain-text maintainer roster
+MAINTAINERS.adoc
+
+# ─── Licensing / packaging / tooling (tool-required at root) ─────────────────
+LICENSES/                  # REUSE-style full licence texts (MPL-2.0, CC-BY-SA-4.0)
+manifest.scm               # Guix manifest; `guix shell -m manifest.scm` reads root
+mise.toml                  # mise toolchain pins (sweep2); mise reads repo root
+docs-template/             # site templates consumed by the Ddraig SSG docs deploy (#14)

ARCHITECTURE.md

@@ -0,0 +1,47 @@
+# Architecture
+
+## Overview
+
+This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability.
+
+## Directory Structure
+
+```
+.
+├── src/           # Source code
+├── tests/        # Test suites
+├── docs/         # Documentation
+├── scripts/      # Utility scripts
+├── config/       # Configuration files
+├── LICENSE       # License file
+├── LICENSES/     # Full license texts
+└── README.adoc   # Project documentation
+```
+
+## Design Principles
+
+- **Separation of Concerns**: Each module has a single responsibility
+- **Testability**: Code is written to be easily testable
+- **Documentation**: All public APIs are documented
+- **Configuration**: Environment-specific settings are externalized
+
+## Dependencies
+
+- External dependencies are minimized and clearly declared
+- Version pinning is used for reproducibility
+
+## Security Considerations
+
+- Sensitive data is never committed to the repository
+- Secrets are managed through environment variables or secure vaults
+- Regular dependency audits are performed
+
+## Maintainability
+
+- Code follows consistent style guidelines
+- Pull requests require review and CI checks
+- Issues and discussions are tracked transparently
+
+---
+
+*Last updated: 2026-07-18*

GOVERNANCE.md

@@ -0,0 +1,60 @@
+# Governance
+
+## Overview
+
+This project is governed by the following principles and structures to ensure transparent, inclusive, and effective decision-making.
+
+## Roles and Responsibilities
+
+### Maintainers
+
+Maintainers are responsible for:
+- Reviewing and merging pull requests
+- Managing releases and versioning
+- Ensuring code quality and standards
+- Triaging issues and bug reports
+- Community engagement and support
+
+### Contributors
+
+Contributors are expected to:
+- Follow the code of conduct
+- Submit well-documented pull requests
+- Write tests for new functionality
+- Maintain existing tests
+- Update documentation as needed
+
+## Decision Making
+
+### Minor Changes
+- Can be made by any maintainer
+- Include bug fixes, documentation updates, dependency updates
+
+### Major Changes
+- Require discussion in issues or pull requests
+- Include new features, architectural changes, API changes
+- Need approval from at least 2 maintainers
+
+### Breaking Changes
+- Require RFC (Request for Comments) process
+- Need approval from majority of maintainers
+- Must include migration guide
+
+## Code of Conduct
+
+All participants are expected to follow our Code of Conduct. Violations can be reported to the maintainers.
+
+## Communication
+
+- **Issues**: For bug reports and feature requests
+- **Discussions**: For questions and general discussion
+- **Pull Requests**: For code contributions
+
+## Licensing
+
+All contributions are made under the terms of the repository's LICENSE file.
+By submitting a pull request, you agree to license your contributions accordingly.
+
+---
+
+*Last updated: 2026-07-18*