[adamtobey]

Confidence Score: 3/5

Fix Linux sandbox startup and move native calls off HTTP workers before merging.

Findings

1.  Linux proof builds cannot start ▶
2.  Lean requests stall other routes ▶

Fix with agent prompt

### Issue 1
crates/temper-lean/src/process.rs:155
`Command::new("bwrap")` searches the child’s `PATH`, but this function replaces it with only `root/bin`. CI installs Bubblewrap under `/usr/bin`, outside the Lean toolchain. Every isolated proof build therefore fails to start, blocking verification, native builds, and artifact reload.

Resolve Bubblewrap to an absolute path before clearing the environment.

### Issue 2
crates/temper-platform/src/lean.rs:96-97
The async HTTP handler calls `core.invoke` directly. That function waits on a blocking `Mutex` and runs native Lean code on the HTTP worker. With a slow reviewed component, concurrent requests can occupy every worker: one runs Lean while the others wait for its lock. Unrelated requests and timers then stop making progress until those calls finish.

Move the call and its lock wait to `spawn_blocking`, with a bound on queued work.

---

For each issue above, determine whether it is valid and should be fixed. If so, fix it directly.

Summary

Adds verified native Lean components and a proof-preserving optimization loop.

• Temper checks Lean cores against a fixed contract before it builds them.
• Authenticated callers can invoke reviewed Lean cores for their tenant.
• Lean cores can exchange typed values and binary buffers with Rust.
• The RAW compaction example checks that optimized cores preserve and reorder rows.

Review checks were static. git diff --check passed; native execution was not verified.

Diagram

%%{init: {'theme': 'neutral'}}%%
flowchart TD
  S[Specification and manifest] --> V[Check specification proofs]
  V --> C[Check candidate proofs]
  C --> N[Build native artifact]
  N --> B[Benchmark and select]
  B --> C
  B --> R[Review exact artifact]
  R --> L[Load reviewed core]
  L --> H[Authenticated tenant request]
  H --> A[Check Cedar permission]
  A --> I[Invoke native Lean]

Loading

_{Reviews (1) · Last reviewed commit: "feat(lean): add typed buffer FFI and sus..." · Reviewed by Greptile}

[greptile-apps]

Linux proof builds cannot start

Command::new("bwrap") searches the child’s PATH, but this function replaces it with only root/bin. CI installs Bubblewrap under /usr/bin, outside the Lean toolchain. Every isolated proof build therefore fails to start, blocking verification, native builds, and artifact reload.

Resolve Bubblewrap to an absolute path before clearing the environment.

Prompt To Fix With AI

This is a comment left during a code review.
Path: crates/temper-lean/src/process.rs
Line: 155

Comment:
**Linux proof builds cannot start**

`Command::new("bwrap")` searches the child’s `PATH`, but this function replaces it with only `root/bin`. CI installs Bubblewrap under `/usr/bin`, outside the Lean toolchain. Every isolated proof build therefore fails to start, blocking verification, native builds, and artifact reload.

Resolve Bubblewrap to an absolute path before clearing the environment.

---

For each issue above, determine whether it is valid and should be fixed. If so, fix it directly.

[greptile-apps]

Lean requests stall other routes

The async HTTP handler calls core.invoke directly. That function waits on a blocking Mutex and runs native Lean code on the HTTP worker. With a slow reviewed component, concurrent requests can occupy every worker: one runs Lean while the others wait for its lock. Unrelated requests and timers then stop making progress until those calls finish.

Move the call and its lock wait to spawn_blocking, with a bound on queued work.

Prompt To Fix With AI

This is a comment left during a code review.
Path: crates/temper-platform/src/lean.rs
Line: 96-97

Comment:
**Lean requests stall other routes**

The async HTTP handler calls `core.invoke` directly. That function waits on a blocking `Mutex` and runs native Lean code on the HTTP worker. With a slow reviewed component, concurrent requests can occupy every worker: one runs Lean while the others wait for its lock. Unrelated requests and timers then stop making progress until those calls finish.

Move the call and its lock wait to `spawn_blocking`, with a bound on queued work.

---

For each issue above, determine whether it is valid and should be fixed. If so, fix it directly.