Development

.github/PULL_REQUEST_TEMPLATE.md

@@ -6,7 +6,7 @@
 
 - [ ] Mock path: `bash scripts/ci.sh` (or relevant demos) when touching receipts / guests / gRPC
 - [ ] Rust: `cd host && cargo test -p lean_tee_receipt -p lean_tee_compliance` if host crypto/guests change
-- [ ] SP1: note `sp1-execute` impact if guest/runtime/digests change
+- [ ] SP1: if guest/runtime/digests change, run `scripts/sp1_execute_ci.sh` locally (CI smoke is manual-only for now)
 - [ ] Docs/proto updated if wire or Accept semantics change
 
 ## Checklist

.github/dependabot.yml

@@ -5,11 +5,29 @@ updates:
     schedule:
       interval: monthly
     open-pull-requests-limit: 5
+    ignore:
+      # bincode 3.0.0 is an intentional unmaintained stub that only fails to compile.
+      - dependency-name: bincode
+        update-types: ["version-update:semver-major"]
+    groups:
+      tonic-prost:
+        patterns:
+          - "tonic"
+          - "tonic-*"
+          - "prost"
+          - "prost-*"
   - package-ecosystem: cargo
     directory: /clients/rust
     schedule:
       interval: monthly
     open-pull-requests-limit: 3
+    groups:
+      tonic-prost:
+        patterns:
+          - "tonic"
+          - "tonic-*"
+          - "prost"
+          - "prost-*"
   - package-ecosystem: github-actions
     directory: /
     schedule:

.github/workflows/ci.yml

@@ -9,7 +9,7 @@ jobs:
   lean-mock:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v7
       - name: Install deps
         run: |
           sudo apt-get update -qq
@@ -47,7 +47,7 @@ jobs:
   rust-mock:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v7
       - uses: dtolnay/rust-toolchain@stable
       - name: Test receipt + compliance
         working-directory: host

.github/workflows/sp1-execute.yml

@@ -1,49 +1,31 @@
 name: sp1-execute
 
-# SP1 path: PR/push (path-filtered), weekly execute + digest pin check,
-# weekly heavy prove on a larger runner, manual dispatch overrides.
+# SP1 Lean guest smoke + digest pin. Manual only for now — GitHub-hosted
+# runners do not have enough RAM/CPU for reliable execute/prove. Run locally
+# (or on a suitably sized self-hosted runner) via:
+#   bash scripts/sp1_execute_ci.sh
+#   gh workflow run sp1-execute.yml -f prove_one=false -f prove_heavy=false
+# Re-enable pull_request / push / schedule when adequate compute is available.
 
 on:
-  pull_request:
-    paths: &sp1_paths
-      - "host/guest_lean/**"
-      - "host/guest_lean_spike/**"
-      - "host/lean_sp1_runtime/**"
-      - "host/lean_sp1_init_min/**"
-      - "host/prove_server/**"
-      - "LeanTee/GuestSp1.lean"
-      - "LeanTee/GuestProg.lean"
-      - "scripts/sp1_*"
-      - "artifacts/sp1_guest_digests.json"
-      - ".github/workflows/sp1-execute.yml"
-  push:
-    branches: [main, lean-sp1-guest]
-    paths: *sp1_paths
-  schedule:
-    - cron: "17 6 * * 1" # weekly Monday 06:17 UTC — execute + digest pin
-    - cron: "47 7 * * 1" # weekly Monday 07:47 UTC — real CPU prove (larger runner)
   workflow_dispatch:
     inputs:
       prove_one:
         description: "Also run one prove (mock unless prove_heavy)"
         type: boolean
-        default: true
+        default: false
       prove_heavy:
         description: "Real CPU prove+verify of Lean ELF (needs prove_one; uses larger runner job)"
         type: boolean
         default: false
 
 jobs:
   sp1-execute:
-    if: |
-      github.event_name == 'pull_request' ||
-      github.event_name == 'push' ||
-      (github.event_name == 'schedule' && github.event.schedule == '17 6 * * 1') ||
-      (github.event_name == 'workflow_dispatch' && !inputs.prove_heavy)
+    if: ${{ !inputs.prove_heavy }}
     runs-on: ubuntu-latest
     timeout-minutes: 180
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v7
         with:
           path: lean-tee
       - uses: dtolnay/rust-toolchain@stable
@@ -72,28 +54,26 @@ jobs:
       - name: SP1 Lean guest smoke (execute + digest pin)
         working-directory: lean-tee
         env:
-          # PR: execute + mock prove-one. Schedule: execute-only. Manual: inputs.
-          SP1_PROVE_ONE: ${{ github.event_name == 'pull_request' && '1' || (github.event_name == 'workflow_dispatch' && inputs.prove_one && '1' || '0') }}
+          SP1_PROVE_ONE: ${{ inputs.prove_one && '1' || '0' }}
           SP1_PROVE_HEAVY: "0"
           SP1_CHECK_DIGESTS: "1"
           CARGO_TERM_COLOR: always
         run: bash scripts/sp1_execute_ci.sh
       - name: Upload guest digests
-        uses: actions/upload-artifact@v4
+        uses: actions/upload-artifact@v7
         with:
           name: sp1-guest-digests
           path: lean-tee/artifacts/sp1_guest_digests.json
           if-no-files-found: error
 
   sp1-prove-heavy:
-    # 32 GiB RAM — enable GitHub larger runners for the org/repo if this job queues forever.
+    # Needs a larger runner (≈32 GiB). Skip unless org has ubuntu-latest-8-cores
+    # (or equivalent) enabled — otherwise this job queues forever / OOMs.
     runs-on: ubuntu-latest-8-cores
-    if: |
-      (github.event_name == 'schedule' && github.event.schedule == '47 7 * * 1') ||
-      (github.event_name == 'workflow_dispatch' && inputs.prove_one && inputs.prove_heavy)
+    if: ${{ inputs.prove_one && inputs.prove_heavy }}
     timeout-minutes: 240
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@v7
         with:
           path: lean-tee
       - uses: dtolnay/rust-toolchain@stable
@@ -124,7 +104,7 @@ jobs:
           CARGO_TERM_COLOR: always
         run: bash scripts/sp1_execute_ci.sh
       - name: Upload guest digests (post-prove)
-        uses: actions/upload-artifact@v4
+        uses: actions/upload-artifact@v7
         with:
           name: sp1-guest-digests-heavy
           path: lean-tee/artifacts/sp1_guest_digests.json

CHANGELOG.md

@@ -2,6 +2,9 @@
 
 ## 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)
 - Mid-tier Lean SP1 guest + `sp1_lean_mid_smoke --prove` (Init-free mix/rounds; laptop-oriented)
 - Spike smoke: optional `--prove` for CPU prove+verify

CONTRIBUTING.md

@@ -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
@@ -71,7 +74,7 @@ Do not run real CPU `SP1_PROVER=cpu --prove-one` on ≤16 GiB machines without
 
 1. Branch from `main` (or the active integration branch agreed with maintainers).
 2. Ensure mock CI paths pass locally when touching receipts, guests, or gRPC.
-3. If you change the Lean SP1 guest or runtime patches, run or note `sp1-execute` workflow impact.
+3. If you change the Lean SP1 guest or runtime patches, run `bash scripts/sp1_execute_ci.sh` locally (and refresh `artifacts/sp1_guest_digests.json` from Linux if digests change). Automatic `sp1-execute` CI is off for now — GH runners lack the compute.
 4. Describe **why** in the PR body; link issues if any.
 5. Do not commit secrets, `.env` files, `host/target/`, `.cache/`, or editor junk (e.g. `.#`).
 

artifacts/sp1_guest_digests.json

@@ -3,7 +3,7 @@
   "profile": "lean-tee-v2",
   "code_id_example": "lean-tee/compliance_operator/lean-sp1/v1",
   "code_hash": "bec5a1b6fd790b3332da9ebdd744dbe4d58612fa9de64321298ddea05a40784f",
-  "elf_sha256": "23e1bf0a53cc733746c898e561fde4eeffef403f53425f1e49c62d05f524744a",
+  "elf_sha256": "cfaef020528620feed5e970d4828137f443a53328539b3a64483a84ad3ef3554",
   "elf_bytes": 2128064,
   "vk_hash_bytes": "49223f521ef81309217bbfb46f9820ed68a26bf52a5911801b90df8a025bd915",
   "vk_bytes32": "0x0092447ea47be04c250bddfda6f9820edd144d7eaa9644600dc86fc5025bd915",