Merge branch 'main' into feat/ocaml-binding-standup

Author: hyperpolymath

.claude/settings.json

@@ -0,0 +1,12 @@
+{
+  "permissions": {
+    "allow": [
+      "Bash(cargo check)",
+      "Bash(cargo check *)",
+      "Bash(gh project item-list *)",
+      "Bash(gh project list)",
+      "Bash(gh project list *)",
+      "Bash(git grep *)"
+    ]
+  }
+}

.clusterfuzzlite/Dockerfile

@@ -4,38 +4,27 @@
 # ClusterFuzzLite fuzzing container for proven.
 #
 # Base: ClusterFuzzLite's rust image (libfuzzer + cargo-fuzz pre-installed)
-# Adds: Zig + Idris2 so build.sh can compile libproven.so prior to
-# building the fuzz targets.
+# Adds: Zig so build.sh can compile the standalone libproven.so fixture
+# prior to building the supported fuzz targets.
 
-FROM gcr.io/oss-fuzz-base/base-builder-rust:v1@sha256:5c2cdc8a9d8b6ad0bf7e9f44fdcd0d7cd7a8b6eca5e8d3c5a89e3e5d8e1c7a3f
+FROM gcr.io/oss-fuzz-base/base-builder-rust:v1@sha256:8a9f7d1ee933da04fc7b616c51d3fb99009692f6aa93ca9e972a6a39730e14f5
 
-# Idris2 + Zig dependencies. ChezScheme is the Idris2 bootstrap target;
-# gmp is the bignum dependency.
+# Zig download dependencies.
 RUN apt-get update && apt-get install -y --no-install-recommends \
-      chezscheme \
-      libgmp-dev \
       curl \
       ca-certificates \
-      git \
-      build-essential \
+      xz-utils \
     && rm -rf /var/lib/apt/lists/*
 
-# Pin Zig 0.13.0 (matches proven's .github/workflows/zig-ffi.yml).
-ARG ZIG_VERSION=0.13.0
-RUN curl -sL "https://ziglang.org/download/${ZIG_VERSION}/zig-linux-x86_64-${ZIG_VERSION}.tar.xz" \
-      | tar -xJ -C /opt \
-    && ln -s "/opt/zig-linux-x86_64-${ZIG_VERSION}/zig" /usr/local/bin/zig
-
-# Build Idris2 0.8.0 from source (matches proven's idris2-ci.yml).
-ARG IDRIS2_VERSION=0.8.0
-RUN git clone --depth 1 --branch "v${IDRIS2_VERSION}" \
-      https://github.com/idris-lang/Idris2.git /tmp/idris2 \
-    && cd /tmp/idris2 \
-    && make bootstrap SCHEME=chezscheme \
-    && make install \
-    && rm -rf /tmp/idris2
-
-ENV PATH="/root/.idris2/bin:${PATH}"
+# Pin Zig 0.15.2 (matches ffi/zig/build.zig.zon's minimum).
+ARG ZIG_VERSION=0.15.2
+ARG ZIG_TARBALL="https://ziglang.org/download/${ZIG_VERSION}/zig-x86_64-linux-${ZIG_VERSION}.tar.xz"
+ARG ZIG_SHA256="02aa270f183da276e5b5920b1dac44a63f1a49e55050ebde3aecc9eb82f93239"
+RUN curl -fsSL "$ZIG_TARBALL" -o /tmp/zig.tar.xz \
+    && echo "$ZIG_SHA256  /tmp/zig.tar.xz" | sha256sum -c - \
+    && tar -xJ -C /opt -f /tmp/zig.tar.xz \
+    && ln -s "/opt/zig-x86_64-linux-${ZIG_VERSION}/zig" /usr/local/bin/zig \
+    && rm /tmp/zig.tar.xz
 
 # Project source is mounted at $SRC/proven by ClusterFuzzLite.
 WORKDIR $SRC/proven

.clusterfuzzlite/build.sh

@@ -2,9 +2,9 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
-# ClusterFuzzLite build script. Builds libproven via Zig (which compiles
-# Idris2 RefC output) and then builds the cargo-fuzz targets that link
-# against it.
+# ClusterFuzzLite build script. Builds the standalone Zig FFI surface as
+# libproven.so, then builds the cargo-fuzz targets that are backed by that
+# surface.
 #
 # Runs inside the ClusterFuzzLite container (see Dockerfile). Outputs
 # the fuzz target binaries to $OUT, the path the runner expects.
@@ -17,43 +17,46 @@
 set -euo pipefail
 
 echo "=== ClusterFuzzLite build: proven ==="
+mkdir -p "$OUT"
 
-# Build libproven via the Zig FFI bridge. The container has Idris2 + Zig
-# baked in; this step compiles Idris2 → C → libproven.so.
+# Build the standalone Zig FFI fixture as libproven.so. The full Idris RefC
+# bridge is exercised by ffi-full-integration.yml when its private dependency
+# credential is configured; this PR fuzz gate must stay self-contained.
 if [[ -f ffi/zig/build.zig ]]; then
   pushd ffi/zig >/dev/null
-  zig build || {
-    echo "WARN: Zig FFI build failed; fuzz targets will not link." >&2
-    echo "      Investigate libproven build before re-running." >&2
+  mkdir -p zig-out/lib
+  zig build-lib -static -O ReleaseSafe -fno-stack-check -fPIC --name proven \
+    -femit-bin=zig-out/lib/libproven.a src/main.zig -lc || {
+    echo "WARN: standalone Zig FFI build failed; fuzz targets will not link." >&2
     exit 1
   }
+
   popd >/dev/null
 fi
 
 # Make libproven discoverable to the cargo-fuzz linker.
 export PROVEN_LIB_DIR="$PWD/ffi/zig/zig-out/lib"
 export LD_LIBRARY_PATH="$PROVEN_LIB_DIR:${LD_LIBRARY_PATH:-}"
+export CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }-stdlib=libstdc++"
 
 # Build cargo-fuzz targets and stage them at $OUT (ClusterFuzzLite
 # convention; runner reads from there).
 pushd bindings/rust/fuzz >/dev/null
-cargo fuzz build -O --debug-assertions
+cargo +nightly fuzz build safe_path_has_traversal -O --debug-assertions
 
 # Copy each compiled fuzzer + libproven.so into $OUT.
 TARGETS_DIR="target/x86_64-unknown-linux-gnu/release"
-for fuzzer in safe_url_parse safe_email_is_valid safe_json_is_valid safe_path_has_traversal; do
+for fuzzer in safe_path_has_traversal; do
   if [[ -f "$TARGETS_DIR/$fuzzer" ]]; then
     cp "$TARGETS_DIR/$fuzzer" "$OUT/"
   else
     echo "WARN: missing fuzz binary $fuzzer (build failed)" >&2
   fi
 done
 
-# Bundle libproven.so so the runner can find it at exec time.
-mkdir -p "$OUT/lib"
-if [[ -f "$PROVEN_LIB_DIR/libproven.so" ]]; then
-  cp "$PROVEN_LIB_DIR/libproven.so" "$OUT/lib/"
-fi
+# Bundle libproven.a so the fuzzer build can find it (for static linking).
+# Note: ClusterFuzzLite binaries should be self-contained; static linking
+# is preferred to avoid runtime library loading issues.
 popd >/dev/null
 
 echo "=== Build complete. Staged to $OUT. ==="

.github/copilot/coding-agent.yml

@@ -0,0 +1,6 @@
+mcp_servers:
+  boj-server:
+    command: npx
+    args: ["-y", "@hyperpolymath/boj-server@latest"]
+    env:
+      BOJ_URL: http://localhost:7700

.github/workflows/boj-build.yml

@@ -29,7 +29,7 @@ jobs:
           BRANCH: ${{ github.ref_name }}
         run: |
           # Send a secure trigger to boj-server to build this repository.
-          # Payload values are passed via env vars rather than ${{ }}
+          # Payload values are passed via env vars rather than workflow expressions
           # interpolation to avoid shell-injection by branch name.
           payload=$(jq -nc \
             --arg repo "$REPO" \

.github/workflows/clusterfuzzlite.yml

@@ -29,7 +29,7 @@ concurrency:
 
 jobs:
   pr-fuzzing:
-    if: github.event_name == 'pull_request' && hashFiles('bindings/rust/fuzz/Cargo.toml') != ''
+    if: github.event_name == 'pull_request'
     runs-on: ubuntu-latest
     timeout-minutes: 30
     steps:

.github/workflows/dogfood-gate.yml

@@ -257,27 +257,28 @@ jobs:
           echo "has_manifest=true" >> "$GITHUB_OUTPUT"
 
           # Validate TOML structure using Python 3.11+ tomllib
-          python3 -c "
-import tomllib, sys
-with open('eclexiaiser.toml', 'rb') as f:
-    data = tomllib.load(f)
-project = data.get('project', {})
-if not project.get('name', '').strip():
-    print('ERROR: project.name is required', file=sys.stderr)
-    sys.exit(1)
-functions = data.get('functions', [])
-if not functions:
-    print('ERROR: at least one [[functions]] entry is required', file=sys.stderr)
-    sys.exit(1)
-for fn in functions:
-    if not fn.get('name', '').strip():
-        print('ERROR: function name cannot be empty', file=sys.stderr)
-        sys.exit(1)
-    if not fn.get('source', '').strip():
-        print(f'ERROR: function {fn[\"name\"]} has no source path', file=sys.stderr)
-        sys.exit(1)
-print(f'Valid: {project[\"name\"]} ({len(functions)} function(s))')
-" || {
+          python3 <<'PY' || {
+          import tomllib, sys
+
+          with open('eclexiaiser.toml', 'rb') as f:
+              data = tomllib.load(f)
+          project = data.get('project', {})
+          if not project.get('name', '').strip():
+              print('ERROR: project.name is required', file=sys.stderr)
+              sys.exit(1)
+          functions = data.get('functions', [])
+          if not functions:
+              print('ERROR: at least one [[functions]] entry is required', file=sys.stderr)
+              sys.exit(1)
+          for fn in functions:
+              if not fn.get('name', '').strip():
+                  print('ERROR: function name cannot be empty', file=sys.stderr)
+                  sys.exit(1)
+              if not fn.get('source', '').strip():
+                  print(f'ERROR: function {fn["name"]} has no source path', file=sys.stderr)
+                  sys.exit(1)
+          print(f'Valid: {project["name"]} ({len(functions)} function(s))')
+          PY
             echo "::error file=eclexiaiser.toml::Invalid eclexiaiser.toml — see step output for details"
             exit 1
           }
@@ -378,4 +379,3 @@ print(f'Valid: {project[\"name\"]} ({len(functions)} function(s))')
           *Generated by the [Dogfood Gate](https://github.com/hyperpolymath/rsr-template-repo) workflow.*
           *Dogfooding is guinea pig fooding — we test our tools on ourselves.*
           EOF
-

.github/workflows/ffi-full-integration.yml

@@ -0,0 +1,140 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
+name: FFI Full Integration
+
+permissions:
+  contents: read
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - 'src/**'
+      - 'ffi/zig/**'
+      - 'proven-ffi.ipkg'
+      - 'scripts/build-refc.sh'
+      - '.github/workflows/ffi-full-integration.yml'
+  pull_request:
+    branches: [main]
+    paths:
+      - 'src/**'
+      - 'ffi/zig/**'
+      - 'proven-ffi.ipkg'
+      - 'scripts/build-refc.sh'
+      - '.github/workflows/ffi-full-integration.yml'
+  workflow_dispatch:
+
+concurrency:
+  group: ffi-full-integration-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  idris-refc-zig:
+    name: Idris -> RefC -> Zig
+    runs-on: ubuntu-latest
+    timeout-minutes: 45
+    if: github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository
+
+    env:
+      IDRIS2_VERSION: '0.8.0'
+      ZIG_VERSION: '0.15.2'
+
+    steps:
+      - name: Checkout proven
+        uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+        with:
+          persist-credentials: false
+
+      - name: Check language-bridges credential
+        id: bridge-token
+        env:
+          LANGUAGE_BRIDGES_TOKEN: ${{ secrets.LANGUAGE_BRIDGES_TOKEN }}
+        run: |
+          set -euo pipefail
+          if [ -z "$LANGUAGE_BRIDGES_TOKEN" ]; then
+            echo "available=false" >> "$GITHUB_OUTPUT"
+            echo "::notice::LANGUAGE_BRIDGES_TOKEN is not configured; skipping private full FFI integration."
+          else
+            echo "available=true" >> "$GITHUB_OUTPUT"
+          fi
+
+      - name: Checkout language-bridges
+        if: steps.bridge-token.outputs.available == 'true'
+        uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+        with:
+          repository: nextgen-languages/language-bridges
+          path: nextgen-languages/language-bridges
+          token: ${{ secrets.LANGUAGE_BRIDGES_TOKEN }}
+          persist-credentials: false
+
+      - name: Install Idris 2 dependencies
+        if: steps.bridge-token.outputs.available == 'true'
+        run: |
+          set -euo pipefail
+          sudo apt-get update
+          sudo apt-get install -y chezscheme libgmp-dev
+
+      - name: Cache Idris 2
+        if: steps.bridge-token.outputs.available == 'true'
+        id: cache-idris2
+        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
+        with:
+          path: |
+            ~/.idris2
+            ~/idris2-${{ env.IDRIS2_VERSION }}
+          key: idris2-refc-${{ env.IDRIS2_VERSION }}-${{ runner.os }}
+
+      - name: Install Idris 2
+        if: steps.bridge-token.outputs.available == 'true' && steps.cache-idris2.outputs.cache-hit != 'true'
+        run: |
+          set -euo pipefail
+          git clone --depth 1 --branch v${{ env.IDRIS2_VERSION }} https://github.com/idris-lang/Idris2.git ~/idris2-${{ env.IDRIS2_VERSION }}
+          cd ~/idris2-${{ env.IDRIS2_VERSION }}
+          make bootstrap SCHEME=chezscheme
+          make install
+
+      - name: Add Idris 2 to PATH
+        if: steps.bridge-token.outputs.available == 'true'
+        run: echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+
+      - name: Setup Zig
+        if: steps.bridge-token.outputs.available == 'true'
+        uses: mlugg/setup-zig@e7d1537c378b83b8049f65dda471d87a2f7b2df2 # v1
+        with:
+          version: ${{ env.ZIG_VERSION }}
+
+      - name: Build Idris RefC output
+        if: steps.bridge-token.outputs.available == 'true'
+        run: scripts/build-refc.sh --verbose
+
+      - name: Build and test libproven
+        if: steps.bridge-token.outputs.available == 'true'
+        run: |
+          set -euo pipefail
+          IDRIS2_PREFIX="$(idris2 --prefix)"
+          REFC_RUNTIME="$(find "$IDRIS2_PREFIX" -path '*/support/refc' -type d 2>/dev/null | head -1)"
+          C_SUPPORT="$(find "$IDRIS2_PREFIX" -path '*/support/c' -type d 2>/dev/null | head -1)"
+          SUPPORT_LIB_FILE="$(find "$IDRIS2_PREFIX" -path '*/lib/libidris2_support.*' 2>/dev/null | head -1)"
+
+          test -n "$REFC_RUNTIME"
+          test -n "$C_SUPPORT"
+          test -n "$SUPPORT_LIB_FILE"
+          SUPPORT_LIB="$(dirname "$SUPPORT_LIB_FILE")"
+          test -d "$GITHUB_WORKSPACE/build/refc"
+          test -d "$REFC_RUNTIME"
+          test -d "$C_SUPPORT"
+          test -d "$SUPPORT_LIB"
+
+          cd ffi/zig
+          zig build \
+            -Didris-refc="$GITHUB_WORKSPACE/build/refc" \
+            -Didris-refc-runtime="$REFC_RUNTIME" \
+            -Didris-c-support="$C_SUPPORT" \
+            -Didris-support-lib="$SUPPORT_LIB"
+          zig build test \
+            -Didris-refc="$GITHUB_WORKSPACE/build/refc" \
+            -Didris-refc-runtime="$REFC_RUNTIME" \
+            -Didris-c-support="$C_SUPPORT" \
+            -Didris-support-lib="$SUPPORT_LIB"
+          ls -la zig-out/lib/libproven.*