ci: integrate safe issue slices for timeouts, Zig setup and ABI validation

.devcontainer/install-zig.sh

@@ -0,0 +1,71 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Opt-in, user-local Zig installation for restricted Linux web sessions.
+set -euo pipefail
+
+usage() {
+  cat <<'HELP'
+Usage: bash .devcontainer/install-zig.sh
+Install Zig 0.15.2 from checksum-pinned PyPI wheels in a private Python venv.
+Requires Linux x86_64/aarch64, python3 with venv/pip, and PyPI network access.
+No sudo, system Python changes, shell-profile edits, or automatic activation.
+Set OCHRANCE_ZIG_HOME to an absolute installation directory to override
+${XDG_DATA_HOME:-$HOME/.local/share}/ochrance/zig-0.15.2.
+After installation, add the printed bin directory to PATH for this shell.
+HELP
+}
+if [[ $# -gt 0 ]]; then
+  if [[ $# == 1 && ( $1 == --help || $1 == -h ) ]]; then usage; exit 0; fi
+  usage >&2
+  exit 2
+fi
+
+case "$(uname -s)/$(uname -m)" in
+  Linux/x86_64|Linux/aarch64) ;;
+  *) echo 'ERROR: only Linux x86_64/aarch64 wheels are pinned.' >&2; exit 1 ;;
+esac
+
+root="${OCHRANCE_ZIG_HOME:-${XDG_DATA_HOME:-$HOME/.local/share}/ochrance/zig-0.15.2}"
+case "$root" in
+  /*) ;;
+  *) echo 'ERROR: OCHRANCE_ZIG_HOME must be an absolute path.' >&2; exit 1 ;;
+esac
+if [[ "$root" == / || "$root" == *$'\n'* ]]; then
+  echo 'ERROR: unsafe installation path.' >&2
+  exit 1
+fi
+script_dir="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd)"
+
+# A completed installation needs no network (or global Python) on restart.
+if [[ -x "$root/bin/zig" ]] && [[ "$("$root/bin/zig" version)" == 0.15.2 ]]; then
+  printf 'Zig 0.15.2 already installed. Activate with:\nexport PATH=%q:"$PATH"\n' "$root/bin"
+  exit 0
+fi
+command -v python3 >/dev/null || { echo 'ERROR: python3 is required.' >&2; exit 1; }
+mkdir -p -- "$root"
+# Do not let concurrent session setup processes mutate the same venv.
+if ! mkdir -- "$root/.install-lock" 2>/dev/null; then
+  echo "ERROR: installation locked at $root/.install-lock (another install or interrupted process)." >&2
+  exit 1
+fi
+trap 'rmdir -- "$root/.install-lock"' EXIT
+
+python3 -m venv "$root/venv"
+"$root/venv/bin/python" -m pip --isolated install \
+  --index-url https://pypi.org/simple \
+  --require-hashes --only-binary=:all: --no-deps \
+  -r "$script_dir/zig-requirements.txt"
+[[ "$("$root/venv/bin/python" -m ziglang version)" == 0.15.2 ]] || {
+  echo 'ERROR: installed Zig version does not match 0.15.2.' >&2
+  exit 1
+}
+mkdir -p -- "$root/bin"
+# Resolve relative to the shim; do not embed or evaluate the installation path.
+cat > "$root/bin/zig" <<'SH'
+#!/usr/bin/env bash
+set -euo pipefail
+root="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." && pwd)"
+exec "$root/venv/bin/python" -m ziglang "$@"
+SH
+chmod +x "$root/bin/zig"
+printf 'Installed Zig 0.15.2. Activate with:\nexport PATH=%q:"$PATH"\n' "$root/bin"

.devcontainer/zig-requirements.txt

@@ -0,0 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# PyPI ziglang 0.15.2 wheels: Linux x86_64 and aarch64, respectively.
+# Distribution metadata: https://pypi.org/pypi/ziglang/0.15.2/json
+ziglang==0.15.2 \
+    --hash=sha256:806316453d1ede7174ed3fefb8e5348154629089c3bb5fe812dfd0e172fac130 \
+    --hash=sha256:edc0aa60ec964a4cf462d40f68d7de242ddf37fd9a80f2afaee6397059463230

.github/workflows/codeql.yml

@@ -15,6 +15,7 @@ permissions:
 jobs:
   analyze:
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     permissions:
       contents: read
       security-events: write

.github/workflows/guix-nix-policy.yml

@@ -17,6 +17,7 @@ permissions:
 jobs:
   check:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     permissions:
       contents: read
     steps:

.github/workflows/idris2.yml

@@ -43,6 +43,8 @@ jobs:
           version: 0.15.2
       - name: Build core (type-checks all modules under --total)
         run: idris2 --build ochrance.ipkg
+      - name: Build ABI definitions (separate package; issue 39)
+        run: idris2 --build ochrance-abi.ipkg
       - name: Install package (needed by the test ipkgs)
         run: idris2 --install ochrance.ipkg
       - name: A2ML parser tests

.github/workflows/label-triage.yml

@@ -46,6 +46,7 @@ permissions:
 jobs:
   triage:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - name: Classify and label
         env:

.github/workflows/labels.yml

@@ -32,6 +32,7 @@ permissions:
 jobs:
   sync:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     steps:
       - name: Apply canonical labels
         env:

.github/workflows/quality.yml

@@ -18,6 +18,7 @@ permissions:
 jobs:
   lint:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     permissions:
       contents: read
     steps:
@@ -50,6 +51,7 @@ jobs:
 
   docs:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     permissions:
       contents: read
     steps:

.github/workflows/security-policy.yml

@@ -17,6 +17,7 @@ permissions:
 jobs:
   check:
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     permissions:
       contents: read
     steps:

.github/workflows/zig-ffi.yml

@@ -24,8 +24,11 @@ jobs:
   zig-ffi:
     name: Zig FFI build + test
     runs-on: ubuntu-latest
+    timeout-minutes: 30
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+      - name: User-local Zig installer boundary tests (offline)
+        run: bash tests/toolchain/install_zig_test.sh
       - name: Set up Zig 0.15.2
         uses: mlugg/setup-zig@d1434d08867e3ee9daa34448df10607b98908d29 # v2.2.1
         with:

docs/ISSUE-RESOLUTION-PLAN.adoc

@@ -0,0 +1,89 @@
+// SPDX-License-Identifier: MPL-2.0
+= Issue resolution plan
+:toc:
+
+Evidence snapshot: 2026-09-25, starting from `ed6a504` on `main`.
+Scope: open issues #39–#44 in `hyperpolymath/ochrance`.
+This is a delivery plan, not a claim that the umbrella issues are complete.
+
+== Safety rules
+
+* Small, independently revertible pull requests; preserve branch protections.
+* No new axioms, proof shortcuts, cryptographic substitutions, or invented external ABIs.
+* Do not change runtime code merely to make CI green.
+* Retain existing test gates, permissions, pinned dependencies, and generous cold-build budgets.
+* Merge only after the relevant checks pass; investigate failures rather than bypassing them.
+* Never close an estate-wide issue for a local-only fix, or dismiss a security alert without evidence.
+
+== Ordered work queue
+
+[cols="1,2,4,4",options="header"]
+|===
+|Priority / issue |Disposition |Work |Acceptance / dependency
+|1 — #43 |Deliver local timeout fix now
+|Add missing timeouts to CodeQL, Guix/Nix policy, label triage, label sync, both quality jobs, security policy, and Zig FFI. Preserve existing limits, notably Pages' 60-minute cold-build allowance and Idris2's 30 minutes.
+|Every local runner job has a positive timeout. Reusable-workflow callers must not receive this unsupported key; their budgets belong upstream. Workflow security, Idris2, Zig FFI and structural checks pass.
+
+|1 — #43 remainder |Security triage blocked on evidence/access
+|Identify the historical critical finding from full scan output; compare with current findings. Check learning submission in the pinned standards reusable workflow before changing anything.
+|Record rule, location, exploitability and remediation before dismissal. Code-scanning API returned 403; latest findings artifact download failed in this session. Do not infer that the critical is fixed from a successful advisory scan. Token provisioning is an owner/estate task, not a reason to broaden local permissions or silence failures.
+
+|2 — #44 |Conventional engineering, separate PR
+|Replace the placeholder development container with a reproducible environment aligned to CI: Idris2 0.8.0 and Zig 0.15.2. Add a usable devcontainer configuration and documented non-container fallback. Reconcile `mise.toml`'s floating Zig and obsolete Justfile version guidance once the installation path is tested.
+|Build from a clean environment; verify versions; build core and ABI separately; run all three Idris suites, Zig tests, C dlopen test and Idris-to-Zig runtime test. Demonstrate restart persistence/cache behavior and checksum-verified downloads. Current sandbox has neither compiler nor container engine; avoid committing an untested replacement image. Network allowlisting remains environment administration.
+
+|3 — #39 |Split conventional FFI work from research
+|Core crypto production wiring is already present, as also noted in the issue's PR #67 update. The separate ABI `blake3Hash` still returns 32 zero bytes. Implement it only with explicit allocation/error handling and the actual library contract. Treat ECHIDNA as a separate integration requiring its authoritative ABI and available library.
+|Compile `ochrance-abi.ipkg` (not currently built by the core Idris CI job); add executable known-answer tests for empty, nonempty and binary input through the ABI wrapper, plus allocation/error-path coverage. Preserve existing Merkle proof/spec distinction. ECHIDNA requires real link/runtime success and failure tests; no fabricated theorem or assumed proof result.
+
+|4 — #40 |Cross-repository decision first
+|Compare authoritative standards and template files at recorded commits, not README summaries. Decide canonical paths and phase vocabulary with maintainers.
+|Publish a file-level reconciliation matrix and agreed authority before migrating local layout. Do not invent policy in this repository.
+
+|5 — #41 |Depends on #40
+|Import only the agreed scaffold from a pinned template revision, preserving Ochrance-specific agent instructions, debt, coverage and anchors. Root README and root-allow already exist; the issue's September update records remaining gaps.
+|Validate links and manifests, run the estate root-shape gate, and inspect bot-directive changes. Mark only the Ochrance checklist item; svalinn and ochrance-framework need their own changes.
+
+|6 — #42 |Documentation, access-dependent
+|Prepare wiki content from current checked-in proof and FFI documentation after the above state is established. The issue reports wiki access restrictions; no wiki write was attempted here.
+|Maintainer/access-enabled publication, working navigation and source revision references. Do not present speculative proofs or unimplemented FFI as shipped; other repositories remain separate.
+|===
+
+== First delivery: local CI timeout completion
+
+Eight missing limits across seven workflow files are the bounded first patch.
+Use 30 minutes for CodeQL and Zig FFI, 15 minutes for policy, label and quality jobs.
+No existing limits, commands, triggers, permissions, action pins or runtime sources change.
+Rollback is a revert of the timeout commit; no data or schema migration is involved.
+
+Local baseline: `bash tests/e2e_test.sh` reports 27 passed, 0 failed.
+This is structural validation, not compiled proof or cryptographic execution.
+The sandbox lacks Idris2 and Zig; their executable gates must run in PR CI.
+YAML inspection should check all jobs and compare the parsed before/after workflows,
+allowing only the eight new timeout values. Preserve all pre-existing timeouts.
+
+The current main run of Mirror to Git Forges was already failing before this patch;
+track any repeated failure separately rather than changing credentials or disabling it.
+
+== Follow-up integration evidence (2026-09-25)
+
+The Actions run page exposes the startup annotation hidden by the jobs API:
+`Actor is not allowed to trigger Actions workflows. Workflow file: '.github/workflows/idris2.yml'.`
+See https://github.com/hyperpolymath/ochrance/actions/runs/36128183989[Idris2 run].
+There are no jobs to debug. Repository Actions-permissions APIs also return 403.
+Do not edit workflow permissions, invent a token, or weaken branch protections.
+An authorized maintainer must rerun/trigger the checks, or the GitHub App's
+Actions-trigger authorization must be corrected. Local results are useful evidence,
+not a replacement for required GitHub checks; keep the PR unmerged until they pass.
+
+Bounded follow-ups in this branch:
+
+* #44: opt-in checksum-pinned user-local Zig installer, restart/failure tests and
+  link:WEB-TOOLCHAIN.adoc[documented usage]. Existing hook and system tools unchanged.
+* #39: compile the separate ABI package in the existing Idris2 CI job.
+  This closes a validation gap, not the zero-digest stub or ECHIDNA integration.
+  The stub's allocation/error contract still needs an explicit decision before
+  replacing it; this patch changes no public signatures or runtime implementations.
+* Real local compiled validation is now available (results and the Chez-only
+  bootstrap limitation are recorded in WEB-TOOLCHAIN.adoc), superseding the initial
+  sandbox-toolchain limitation above. No umbrella issue is closed.

docs/WEB-TOOLCHAIN.adoc

@@ -0,0 +1,79 @@
+// SPDX-License-Identifier: MPL-2.0
+= Web-session toolchain (issue #44)
+
+== Scope and safety
+
+CI pins Idris2 0.8.0 and Zig 0.15.2. The existing Claude-only SessionStart
+hook already attempts to install both, but requires system write access.
+For other/restricted sessions, the opt-in Zig installer below needs no root,
+does not modify system Python or shell profiles, and does not replace that hook.
+It is a partial delivery of #44, not a claim that every web host has persistent storage.
+
+== User-local Zig
+
+On Linux x86_64 or aarch64, with Python 3, venv/pip and network access to
+`pypi.org` and `files.pythonhosted.org`:
+
+[source,bash]
+----
+bash .devcontainer/install-zig.sh
+# Follow the printed export command to activate for this shell.
+zig version  # 0.15.2
+----
+
+The default location is `${XDG_DATA_HOME:-$HOME/.local/share}/ochrance/zig-0.15.2`.
+Set `OCHRANCE_ZIG_HOME` to an absolute path on a persistent volume if needed.
+The installer does not activate the tool implicitly: unrelated projects keep
+their existing PATH. Re-running a completed installation is offline and cheap.
+A fresh container without that volume will need a new installation.
+
+This uses the PyPI `ziglang` distribution, the same alternative distribution
+route as the existing hook, not a direct ziglang.org download. The exact
+Linux wheels are SHA-256 pinned in `.devcontainer/zig-requirements.txt`;
+other platforms and source distributions are rejected. Updating requires
+reviewing the version, wheel provenance and hashes together. No unverified
+fallback mirror is tried. Python is only the distribution launcher, not a
+new application runtime dependency.
+
+If setup fails, it exits nonzero and releases its installation lock. A killed
+process can leave `.install-lock` behind: confirm no installer is running before
+removing that empty directory. Retry explicitly after resolving dependencies or
+network access. No broad cleanup command is run against the chosen prefix.
+
+Validation:
+
+[source,bash]
+----
+bash tests/toolchain/install_zig_test.sh
+(cd ffi/zig && zig build test --summary all)
+bash ffi/zig/test/run_link_test.sh
+----
+
+== Idris2 and remaining work
+
+The existing `.github/workflows/idris2.yml` digest-pinned container is the CI
+reference. On a conventional Linux host, source bootstrap of Idris2 v0.8.0
+(commit `15a3e4e70843f7a34100f6470c04b791330788df`) requires Chez Scheme,
+a C toolchain, make and GMP development headers. Use an explicit user-local
+PREFIX when following upstream installation instructions; do not replace a
+working system compiler or assume the placeholder devcontainer is ready.
+
+The next #44 delivery should make that full bootstrap repeatable without root
+and test the image/volume lifecycle. This patch does not alter the legacy hook's
+apt behavior, install Agda, or silently change the available Idris backends.
+
+== Validation performed on 2026-09-25
+
+* Fresh user-local Zig installation with pinned wheel hashes on Linux x86_64;
+  repeat invocation reused it. aarch64 hash is supplied but execution is untested.
+* Eight offline installer boundary/restart/failure scenarios.
+* Zig 0.15.2: 25/25 tests; C dlopen known-answer/link test passed.
+* Idris2 0.8.0: core and separate ABI packages compiled; parser suite passed,
+  property suite 47/47, integration suite 55/55, Idris-to-Zig runtime suite 12/12.
+* Structural E2E: 27/27.
+
+For this session only, Chez 10.0.0 was built in ignored scratch storage and
+Idris2 bootstrapped with its Chez backend. GMP development headers were unavailable,
+so refc support was omitted in the scratch compiler build; no repository source
+or CI build was altered for that workaround. These results cover the backend
+used by CI, not a full installer/image or refc qualification.

tests/toolchain/install_zig_test.sh

@@ -0,0 +1,60 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Offline installer boundary tests. Real wheel installation is tested separately.
+set -euo pipefail
+ROOT="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../.." && pwd)"
+INSTALL="$ROOT/.devcontainer/install-zig.sh"
+work="$(mktemp -d)"
+trap 'rm -rf -- "$work"' EXIT
+
+expect_failure() {
+  local expected="$1"
+  shift
+  if "$@" > "$work/output" 2>&1; then
+    echo "FAIL: unexpectedly succeeded: $*" >&2
+    exit 1
+  fi
+  grep -Fq -- "$expected" "$work/output"
+}
+
+bash "$INSTALL" --help | grep -q 'No sudo'
+expect_failure 'Usage:' bash "$INSTALL" --unknown
+expect_failure 'absolute path' env OCHRANCE_ZIG_HOME=relative bash "$INSTALL"
+expect_failure 'unsafe installation path' env OCHRANCE_ZIG_HOME=/ bash "$INSTALL"
+
+mkdir -p "$work/mock-bin"
+cat > "$work/mock-bin/uname" <<'SH'
+#!/bin/sh
+printf 'Unsupported\n'
+SH
+chmod +x "$work/mock-bin/uname"
+expect_failure 'only Linux' env PATH="$work/mock-bin:$PATH" bash "$INSTALL"
+rm "$work/mock-bin/uname"
+
+# Restart path must accept whitespace and not invoke Python or touch the venv.
+mkdir -p "$work/installed toolchain/bin"
+cat > "$work/installed toolchain/bin/zig" <<'SH'
+#!/bin/sh
+printf '0.15.2\n'
+SH
+cat > "$work/mock-bin/python3" <<'SH'
+#!/bin/sh
+printf 'UNEXPECTED PYTHON INVOCATION\n' >&2
+exit 99
+SH
+chmod +x "$work/installed toolchain/bin/zig" "$work/mock-bin/python3"
+env PATH="$work/mock-bin:$PATH" OCHRANCE_ZIG_HOME="$work/installed toolchain" \
+  bash "$INSTALL" > "$work/output"
+grep -q 'already installed' "$work/output"
+[[ ! -e "$work/installed toolchain/venv" ]]
+
+mkdir -p "$work/locked/.install-lock"
+expect_failure 'installation locked' env OCHRANCE_ZIG_HOME="$work/locked" bash "$INSTALL"
+# A failed bootstrap must release its own lock and preserve existing files.
+mkdir -p "$work/failed"
+printf 'preserve me\n' > "$work/failed/sentinel"
+expect_failure 'UNEXPECTED PYTHON' env PATH="$work/mock-bin:$PATH" \
+  OCHRANCE_ZIG_HOME="$work/failed" bash "$INSTALL"
+[[ ! -e "$work/failed/.install-lock" ]]
+grep -q 'preserve me' "$work/failed/sentinel"
+echo 'PASS: 8 offline Zig installer scenarios'