RileyBetts · robertbetts · Aug 6, 2026 · Aug 6, 2026
@@ -2,6 +2,7 @@
 
 ## Unreleased
 
+- First-class Linux + macOS: `sealed_worker` cfg-splits Linux `prctl` / macOS `PT_DENY_ATTACH`; SP1 scripts use portable mem/`PROTOC` helpers (`scripts/lib/platform.sh`)
 - SP1 `sp1-execute` CI: disable PR/push/schedule; keep `workflow_dispatch` only (GH runners lack SP1 compute) — run `scripts/sp1_execute_ci.sh` locally
 - Coordinated Dependabot upgrades: tonic/tonic-prost/prost 0.14, sha2 0.11, Actions checkout/upload-artifact v7; ignore bincode majors (3.0.0 is an unmaintained stub)
 - Pin lean-grpc dependency to **v1.1.0** (was v1.0.0)

@@ -6,6 +6,7 @@ By participating, you agree to follow our [Code of Conduct](CODE_OF_CONDUCT.md).
 ## Before you start
 
 - Read [docs/GETTING_STARTED.md](docs/GETTING_STARTED.md) for toolchain setup.
+- **Supported platforms:** Linux and macOS (CI is Linux; macOS is first-class locally).
 - **Mock path** (`lean-tee-v1`) is the default for local iteration — no SP1 required.
 - **Production integrity** (`lean-tee-v2`) needs SP1; see [host/README.md](host/README.md).
 
@@ -16,7 +17,9 @@ git clone https://github.com/RileyBetts/lean-tee.git
 cd lean-tee
 # elan installs Lean 4.32.1 from lean-toolchain
 curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
-sudo apt-get install -y libssl-dev pkg-config   # Debian/Ubuntu
+# Linux:  sudo apt-get install -y libssl-dev pkg-config
+# macOS:  brew install openssl pkg-config
+#         export PKG_CONFIG_PATH="$(brew --prefix openssl)/lib/pkgconfig"
 
 lake update    # fetches lean-grpc v1.1.0 into .lake/packages
 lake build receiptTests teeServer teeClient

@@ -39,7 +39,9 @@ bash scripts/confidentiality_local_demo.sh
 
 The `sealed_worker` process:
 
-- Sets `RLIMIT_CORE=0` and `PR_SET_DUMPABLE=0` (harder unprivileged ptrace / core dumps)
+- Sets `RLIMIT_CORE=0` on Linux and macOS (no core dumps)
+- **Linux:** `PR_SET_DUMPABLE=0` (harder unprivileged ptrace / Yama)
+- **macOS:** `PT_DENY_ATTACH` (best-effort anti-attach; not Yama-equivalent)
 - Zeroizes secret buffers after use
 - Never logs secret bytes
 - Optional `LEAN_TEE_SEALED_MLOCK=1` (`mlockall`, best-effort)

@@ -2,12 +2,14 @@
 
 This guide gets you from a fresh clone to a **working mock demo** in under fifteen minutes. Production SP1 integrity (`lean-tee-v2`) is covered at the end.
 
+**Supported platforms:** Linux and macOS (CI reference is Linux; macOS is first-class for local build and smokes).
+
 ## What you need
 
 | Tool | Version / notes |
 | --- | --- |
 | [Lean 4](https://leanprover.github.io/lean4/doc/setup.html) (elan) | **4.32.1** — pinned in [`lean-toolchain`](../lean-toolchain) |
-| OpenSSL dev | `libssl-dev` + `pkg-config` (host Lake build links `-lssl`) |
+| OpenSSL dev | Host Lake build links `-lssl` (see install below) |
 | Rust (optional) | Stable — for `host/` crates and clients |
 | Python 3 (optional) | Stdlib client; `pytest` for tests |
 | [SP1](https://docs.succinct.xyz/docs/sp1/getting-started/install) (optional) | **6.3.1** — only for `lean-tee-v2` prove path |
@@ -24,7 +26,12 @@ cd lean-tee
 curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \
   | sh -s -- -y --default-toolchain leanprover/lean4:v4.32.1
 
-sudo apt-get install -y libssl-dev pkg-config   # Debian/Ubuntu; adjust on macOS
+# OpenSSL + pkg-config
+# Linux (Debian/Ubuntu):
+sudo apt-get install -y libssl-dev pkg-config
+# macOS (Homebrew):
+#   brew install openssl pkg-config
+#   export PKG_CONFIG_PATH="$(brew --prefix openssl)/lib/pkgconfig"
 
 lake update
 lake build receiptTests teeServer teeClient teeLoopback
@@ -70,18 +77,20 @@ assert ok, reason
 
 Mock prove is **CI/demo only**. For production integrity:
 
-1. Install SP1: `curl -L https://sp1up.succinct.xyz | bash && sp1up && sp1up --c-toolchain`
-2. Build host: `cd host && cargo build -p lean_tee_prove_server --release --features sp1`
-3. Smoke: `bash scripts/sp1_execute_ci.sh` (execute + digest pin)
-4. Run `prove_server` with `SP1_PROVER=cpu` and point `teeServer` at it:
+1. Install SP1: `curl -L https://sp1.succinct.xyz | bash && sp1up && sp1up --c-toolchain`
+2. **macOS only:** Homebrew libs for the SP1 RISC-V gcc (`cc1plus` dylibs):
+   `brew install isl gmp mpfr libmpc`
+3. Build host: `cd host && cargo build -p lean_tee_prove_server --release --features sp1`
+4. Smoke: `bash scripts/sp1_execute_ci.sh` (execute + digest pin; portable on Linux and macOS)
+5. Run `prove_server` with `SP1_PROVER=cpu` and point `teeServer` at it:
 
 ```bash
 export LEAN_TEE_DEFAULT_PROFILE=lean-tee-v2
 export LEAN_TEE_PROVE_ADDR=127.0.0.1:50072
 # prove_server in one terminal; teeServer in another
 ```
 
-Pin counterparties to published digests in [`artifacts/sp1_guest_digests.json`](../artifacts/sp1_guest_digests.json). Plain-English SP1 background: [sp1-integrity-crib-sheet.html](sp1-integrity-crib-sheet.html).
+Pin counterparties to published digests in [`artifacts/sp1_guest_digests.json`](../artifacts/sp1_guest_digests.json) (Linux CI is the pin source of truth; local Mac rebuilds may differ). Plain-English SP1 background: [sp1-integrity-crib-sheet.html](sp1-integrity-crib-sheet.html).
 
 Details: [host/README.md](../host/README.md), [LEAN_SP1_GUEST.md](LEAN_SP1_GUEST.md).
 

@@ -2,6 +2,8 @@
 
 Requires [SP1](https://docs.succinct.xyz/docs/sp1/getting-started/install) (`sp1up` → `cargo prove`, version **6.3.1** aligned with this workspace).
 
+**Platforms:** Linux and macOS. Published ELF/vk digests are pinned from Linux CI; Mac rebuilds may produce different digests.
+
 ## Layout
 
 | Crate | Role |
@@ -17,7 +19,11 @@ Requires [SP1](https://docs.succinct.xyz/docs/sp1/getting-started/install) (`sp1
 curl -L https://sp1.succinct.xyz | bash
 source ~/.bashrc   # or: export PATH="$HOME/.sp1/bin:$PATH"
 sp1up
+sp1up --c-toolchain   # RISC-V gcc for Lean guest C
 cargo prove --version   # expect sp1 ~6.3.x
+
+# macOS: libs expected by SP1's riscv64-unknown-elf-g++ (cc1plus)
+# brew install isl gmp mpfr libmpc
 ```
 
 ## Thorough SP1 test (careful / low OOM risk)

@@ -13,17 +13,25 @@ use std::process;
 use zeroize::{Zeroize, Zeroizing};
 
 fn harden_against_weaker_agents() {
-    // Disable core dumps for this process.
+    // Disable core dumps for this process (Linux + macOS).
     #[cfg(unix)]
     unsafe {
         let lim = libc::rlimit {
             rlim_cur: 0,
             rlim_max: 0,
         };
         let _ = libc::setrlimit(libc::RLIMIT_CORE, &lim);
-        // Not dumpable → harder for unprivileged ptrace attach (Yama/ptrace).
+    }
+    // Not dumpable → harder for unprivileged ptrace attach (Yama/ptrace). Linux only.
+    #[cfg(target_os = "linux")]
+    unsafe {
         let _ = libc::prctl(libc::PR_SET_DUMPABLE, 0, 0, 0, 0);
     }
+    // Best-effort Darwin anti-attach (not equivalent to Linux PR_SET_DUMPABLE / Yama).
+    #[cfg(target_os = "macos")]
+    unsafe {
+        let _ = libc::ptrace(libc::PT_DENY_ATTACH, 0, std::ptr::null_mut(), 0);
+    }
     // Optional mlock of current pages (best-effort; ignore failure).
     if std::env::var("LEAN_TEE_SEALED_MLOCK").ok().as_deref() == Some("1") {
         #[cfg(unix)]

@@ -0,0 +1,81 @@
+# Copyright © 2026 Riley Betts Ltd (rileybetts.ai)
+# SPDX-License-Identifier: Apache-2.0
+
+# Portable helpers for Linux + macOS SP1 / host scripts.
+# shellcheck shell=bash
+
+# Print a short memory summary. Never fails under `set -e`.
+print_mem_summary() {
+  if command -v free >/dev/null 2>&1; then
+    free -h | head -2 || true
+  elif [[ "$(uname -s)" == "Darwin" ]]; then
+    local pages page_size free_p inactive_p avail_kib memsize
+    page_size="$(pagesize 2>/dev/null || sysctl -n hw.pagesize 2>/dev/null || echo 4096)"
+    pages="$(vm_stat 2>/dev/null || true)"
+    free_p="$(printf '%s\n' "$pages" | awk '/Pages free/ {gsub(/\./,"",$3); print $3}')"
+    inactive_p="$(printf '%s\n' "$pages" | awk '/Pages inactive/ {gsub(/\./,"",$3); print $3}')"
+    free_p="${free_p:-0}"
+    inactive_p="${inactive_p:-0}"
+    avail_kib=$(( (free_p + inactive_p) * page_size / 1024 ))
+    memsize="$(sysctl -n hw.memsize 2>/dev/null || echo 0)"
+    echo "Darwin mem: hw.memsize=${memsize} approx_available_kib=${avail_kib} (free+inactive pages)"
+  else
+    echo "mem summary unavailable on $(uname -s)"
+  fi
+}
+
+# Approximate available memory in KiB (nonempty integer).
+# Linux: MemAvailable from /proc/meminfo.
+# Darwin: (Pages free + Pages inactive) * pagesize / 1024.
+mem_available_kib() {
+  local kib
+  if [[ -r /proc/meminfo ]]; then
+    kib="$(awk '/MemAvailable:/ {print $2}' /proc/meminfo 2>/dev/null || true)"
+    if [[ -n "${kib:-}" ]]; then
+      echo "$kib"
+      return 0
+    fi
+  fi
+  if [[ "$(uname -s)" == "Darwin" ]]; then
+    local page_size free_p inactive_p pages
+    page_size="$(pagesize 2>/dev/null || sysctl -n hw.pagesize 2>/dev/null || echo 4096)"
+    pages="$(vm_stat 2>/dev/null || true)"
+    free_p="$(printf '%s\n' "$pages" | awk '/Pages free/ {gsub(/\./,"",$3); print $3}')"
+    inactive_p="$(printf '%s\n' "$pages" | awk '/Pages inactive/ {gsub(/\./,"",$3); print $3}')"
+    free_p="${free_p:-0}"
+    inactive_p="${inactive_p:-0}"
+    echo $(( (free_p + inactive_p) * page_size / 1024 ))
+    return 0
+  fi
+  echo 0
+}
+
+# Resolve a protoc binary: PATH first, else cargo vendored crate by OS/arch.
+default_protoc() {
+  if command -v protoc >/dev/null 2>&1; then
+    command -v protoc
+    return 0
+  fi
+  local os arch tag crate_dir
+  case "$(uname -s)" in
+    Linux) os=linux ;;
+    Darwin) os=macos ;;
+    *) os=linux ;;
+  esac
+  case "$(uname -m)" in
+    x86_64|amd64) arch=x86_64 ;;
+    aarch64|arm64) arch=aarch_64 ;;
+    *) arch=x86_64 ;;
+  esac
+  tag="${os}-${arch}"
+  crate_dir="$(
+    ls -d "${HOME}/.cargo/registry/src"/index.crates.io-*/protoc-bin-vendored-"${tag}"-* 2>/dev/null \
+      | sort -V | tail -1 || true
+  )"
+  if [[ -n "${crate_dir}" && -x "${crate_dir}/bin/protoc" ]]; then
+    echo "${crate_dir}/bin/protoc"
+    return 0
+  fi
+  # Last resort: historical linux x86_64 pin (CI).
+  echo "${HOME}/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/protoc-bin-vendored-linux-x86_64-3.2.0/bin/protoc"
+}
@@ -6,10 +6,12 @@
 # Measured guest is Lean-compiled (`lean_tee_guest_lean`).
 set -euo pipefail
 ROOT="$(cd "$(dirname "$0")/.." && pwd)"
+# shellcheck source=lib/platform.sh
+source "$ROOT/scripts/lib/platform.sh"
 export PATH="${HOME}/.elan/bin:${HOME}/.sp1/bin:${HOME}/.sp1/riscv/bin:${PATH}"
 export CARGO_TARGET_DIR="${CARGO_TARGET_DIR:-$ROOT/host/target}"
 export SP1_PROVER="${SP1_PROVER:-cpu}"
-export PROTOC="${PROTOC:-$HOME/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/protoc-bin-vendored-linux-x86_64-3.2.0/bin/protoc}"
+export PROTOC="${PROTOC:-$(default_protoc)}"
 export CC_riscv64im_succinct_zkvm_elf="${CC_riscv64im_succinct_zkvm_elf:-$HOME/.sp1/riscv/bin/riscv64-unknown-elf-gcc}"
 
 if ! command -v cargo-prove >/dev/null 2>&1; then
@@ -30,7 +32,7 @@ if [[ ! -d "$ROOT/.lake/packages/lean-grpc" && ! -d "$ROOT/../lean-grpc" ]]; the
   lake update
 fi
 echo "== free memory =="
-free -h | head -2
+print_mem_summary
 
 echo "== Lean SP1 runtime + guest archive =="
 bash scripts/sp1_lean_runtime_fetch.sh
@@ -63,9 +65,9 @@ if [[ "${SP1_PROVE_ONE:-}" == "1" ]]; then
   if [[ "${SP1_PROVE_HEAVY:-}" == "1" ]]; then
     # Real CPU prove of the Lean ELF routinely needs >>8 GiB free; on 16 GiB
     # laptops this has hard-locked the machine. Abort unless explicitly forced.
-    avail_kib="$(awk '/MemAvailable:/ {print $2}' /proc/meminfo 2>/dev/null || echo 0)"
+    avail_kib="$(mem_available_kib)"
     need_kib=$((10 * 1024 * 1024)) # 10 GiB
-    free -h | head -2
+    print_mem_summary
     if [[ "${SP1_PROVE_HEAVY_FORCE:-}" != "1" && "${GITHUB_ACTIONS:-}" != "true" && "${avail_kib}" -lt "${need_kib}" ]]; then
       echo "SP1_PROVE_HEAVY refused: MemAvailable=${avail_kib} KiB (<10 GiB)." >&2
       echo "Use Actions prove_heavy / a larger machine, or SP1_PROVE_HEAVY_FORCE=1 (OOM/lockup risk)." >&2

@@ -6,11 +6,13 @@
 # Wire Measurement stays codeHash+configHash; these digests pin the executable.
 set -euo pipefail
 ROOT="$(cd "$(dirname "$0")/.." && pwd)"
+# shellcheck source=lib/platform.sh
+source "$ROOT/scripts/lib/platform.sh"
 OUT="${1:-$ROOT/artifacts/sp1_guest_digests.json}"
 export PATH="${HOME}/.elan/bin:${HOME}/.sp1/bin:${HOME}/.sp1/riscv/bin:${PATH}"
 export CARGO_TARGET_DIR="${CARGO_TARGET_DIR:-$ROOT/host/target}"
 export SP1_PROVER="${SP1_PROVER:-cpu}"
-export PROTOC="${PROTOC:-$HOME/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/protoc-bin-vendored-linux-x86_64-3.2.0/bin/protoc}"
+export PROTOC="${PROTOC:-$(default_protoc)}"
 export CC_riscv64im_succinct_zkvm_elf="${CC_riscv64im_succinct_zkvm_elf:-$HOME/.sp1/riscv/bin/riscv64-unknown-elf-gcc}"
 
 if ! command -v cargo-prove >/dev/null 2>&1; then

@@ -5,10 +5,12 @@
 # Staged SP1 tests — avoids proving three cases back-to-back (OOM risk on 16GB).
 set -euo pipefail
 ROOT="$(cd "$(dirname "$0")/.." && pwd)"
+# shellcheck source=lib/platform.sh
+source "$ROOT/scripts/lib/platform.sh"
 export PATH="${HOME}/.sp1/bin:${PATH}"
 export CARGO_TARGET_DIR="${CARGO_TARGET_DIR:-$ROOT/host/target}"
 export SP1_PROVER="${SP1_PROVER:-cpu}"
-export PROTOC="${PROTOC:-$HOME/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/protoc-bin-vendored-linux-x86_64-3.2.0/bin/protoc}"
+export PROTOC="${PROTOC:-$(default_protoc)}"
 
 if ! command -v cargo-prove >/dev/null 2>&1; then
   echo "cargo-prove not on PATH; run: source ~/.bashrc && sp1up" >&2
@@ -18,7 +20,7 @@ fi
 cd "$ROOT/host"
 
 echo "== free memory =="
-free -h | head -2
+print_mem_summary
 
 echo "== Lean SP1 runtime + guest archive =="
 cd "$ROOT"
@@ -37,9 +39,9 @@ echo "== SP1 prove+verify one case (default: mock — safe on 16GB laptops) =="
 echo "   Real CPU prove is gated (can hard-lock ≤16GB hosts)."
 echo "   Prefer GitHub Actions prove_heavy, or: SP1_PROVE_HEAVY=1 SP1_PROVE_HEAVY_FORCE=1 $0"
 if [[ "${SP1_PROVE_HEAVY:-}" == "1" ]]; then
-  avail_kib="$(awk '/MemAvailable:/ {print $2}' /proc/meminfo 2>/dev/null || echo 0)"
+  avail_kib="$(mem_available_kib)"
   need_kib=$((10 * 1024 * 1024))
-  free -h | head -2
+  print_mem_summary
   if [[ "${SP1_PROVE_HEAVY_FORCE:-}" != "1" && "${GITHUB_ACTIONS:-}" != "true" && "${avail_kib}" -lt "${need_kib}" ]]; then
     echo "SP1_PROVE_HEAVY refused: MemAvailable=${avail_kib} KiB (<10 GiB)." >&2
     echo "Do not force on a laptop you care about; use CI prove_heavy / a big machine." >&2