fix: R-0004 slice 4 (part) — kernel replay resolves its workspace from the input

`--report check-proofs` invoked `lake env lean` with no `cwd`, and `lake` finds
its workspace by walking up from wherever it is invoked. So the verdict depended
on where the caller stood. Same file, same compiler, absolute path:

  from the repo root : 3 verified, 0 failed
  from /tmp          : 0 verified, 3 failed   [E0806] ... failure=theorem_lookup

The second answer is wrong twice over — the proofs do verify, and the reported
cause sends the reader to look for missing theorems that are not missing. The
workspace was simply never found.

`findLakeWorkspace` now walks up from the input file for a lakefile and passes
that as `cwd`, so the answer is a property of what is being checked rather than
of the caller's shell. It returns `none` rather than guessing a default: a wrong
workspace would replay against the wrong library and report confident nonsense.
That case is now named ("cannot locate a Lake workspace for ...") and exits
non-zero — replay fails closed.

Gated in check_proof_freshness.sh (now 17 checks): identical verdict from two
directories, the missing-workspace case named, no theorem blamed for it, and a
non-zero exit. Verified load-bearing by reverting the fix — the gate reports the
exact 3-verified/0-verified split.

Note on that check: the first reversion attempt left `ws` unused, Lean's linter
rejected the file, and the gate then ran against a STALE BINARY and passed. A
sensitivity check has to compile, or it measures the previous build.

Author: unbalancedparentheses

Main.lean

@@ -854,6 +854,29 @@ def renderContracts (parsedModules : List Concrete.Module) (registry : Concrete.
     ++ Report.renderDiv divObls omegaProved
     ++ Report.renderOverflow ovfObls omegaProved bvProved
 
+/-- Walk up from `path` for the directory holding a Lake workspace.
+
+Kernel replay used to invoke `lake` with no `cwd`, so the workspace came from the
+PROCESS working directory and the verdict depended on where the caller stood
+(R-0004 slice 4). Resolving from the input makes the answer a property of what is
+being checked. Returns `none` rather than guessing a default: a wrong workspace
+would replay against the wrong library and report confident nonsense. -/
+partial def findLakeWorkspace (path : String) : IO (Option System.FilePath) := do
+  let abs ← IO.FS.realPath (System.FilePath.mk path)
+  let rec up (dir : System.FilePath) (fuel : Nat) : IO (Option System.FilePath) := do
+    match fuel with
+    | 0 => return none
+    | fuel + 1 =>
+      if (← (dir / "lakefile.toml").pathExists) || (← (dir / "lakefile.lean").pathExists) then
+        return some dir
+      match dir.parent with
+      | some p => if p == dir then return none else up p fuel
+      | none => return none
+  -- Start at the file's directory; a file path has a parent, a directory is its
+  -- own starting point.
+  let start := if (← abs.isDir) then abs else (abs.parent.getD abs)
+  up start 64
+
 /-- Run pipeline and check a profile constraint.
     If the input file lives inside a `Concrete.toml` project, route
     through project mode so std and other dependencies resolve. -/
@@ -1292,10 +1315,30 @@ def compileAndReport (inputPath : String) (reportType : String)
       for (fn, thm) in ensuresThms do
         leanSrc := leanSrc ++ s!"-- {fn} (ensures)\n#check @{thm}\n\n"
       IO.FS.writeFile ⟨tmpPath⟩ leanSrc
-      -- Invoke lake env lean to check the file
+      -- Resolve the proof workspace from the INPUT, not the process working
+      -- directory (R-0004 slice 4). `lake` finds its workspace by walking up
+      -- from wherever it is invoked, so with no `cwd` set this verdict depended
+      -- on where the user happened to stand: the same file by absolute path gave
+      -- "3 verified, 0 failed" from the repo root and "0 verified, 3 failed"
+      -- from /tmp. Worse, it blamed each theorem with `theorem_lookup` — the
+      -- theorems were fine; the workspace was never found.
+      let wsRoot ← findLakeWorkspace inputPath
+      match wsRoot with
+      | none =>
+        -- Say what is actually wrong. Reporting N missing theorems for one
+        -- missing workspace sends the reader to look for the wrong thing.
+        let msg := s!"cannot locate a Lake workspace for '{inputPath}' (no lakefile.toml or lakefile.lean in any parent directory), so the Lean theorems it references cannot be replayed"
+        if reportJson then
+          IO.println s!"\{\n  \"schema_version\": \"1\",\n  \"all_checked\": false,\n  \"checks\": [],\n  \"lean_error\": \"{msg}\",\n  \"summary\": \{\"verified\": 0, \"failed\": 0, \"total\": 0}\n}"
+        else
+          IO.println s!"=== Lean Proof Kernel Check ===\n\nerror: {msg}"
+        return 1
+      | some ws =>
+      -- Invoke lake env lean to check the file, from the resolved workspace.
       let result ← IO.Process.output {
         cmd := "lake"
         args := #["env", "lean", tmpPath]
+        cwd := ws
         env := #[("LAKE_TERM_ANSI", "0")]
       }
       -- Parse results: Lean may put errors on stdout or stderr

ROADMAP.md

@@ -932,9 +932,16 @@ Land this task in seven explicit slices:
    `proved_by_lean_modulo_trusted`, never unqualified `proved_by_lean`
    (`composition_trusted_helper`). The receipt must carry the same distinction.
 
-   Make `--report check-proofs`
-   resolve the proof workspace from the input project/repository rather than
-   the process working directory. Define a versioned `ProofEvidenceReceipt`
+   The workspace-resolution half has LANDED: `--report check-proofs` resolves the
+   Lake workspace by walking up from the INPUT rather than using the process
+   working directory. It previously invoked `lake` with no `cwd`, so the verdict
+   depended on where the caller stood — the same file by absolute path gave
+   "3 verified, 0 failed" from the repo root and "0 verified, 3 failed" from
+   /tmp, blaming each theorem with `theorem_lookup` when the theorems were fine
+   and the workspace was simply never found. An input with no workspace above it
+   now says so and exits non-zero. Gated in `check_proof_freshness.sh`.
+
+   What remains in this slice: define a versioned `ProofEvidenceReceipt`
    envelope and deterministic workspace/import/toolchain identities. This
    slice may establish replay and serialization plumbing, but it cannot upgrade
    a legacy body hash to a complete proof claim.

scripts/tests/check_proof_freshness.sh

@@ -204,6 +204,41 @@ grep -q "(stale)" <<<"$DEPS0" \
   && no "the UNEDITED chain already reports a stale edge — the 062 witness proves nothing" \
   || ok "the unedited chain has no stale edge"
 
+echo
+echo "=== R-0004 slice 4: the replay verdict does not depend on the caller's cwd ==="
+# `lake` finds its workspace by walking up from where it is invoked, so kernel
+# replay with no `cwd` answered according to where the user happened to stand:
+# the same file by absolute path gave "3 verified, 0 failed" from the repo root
+# and "0 verified, 3 failed" from /tmp — and blamed each theorem with
+# `theorem_lookup`, sending the reader after the wrong thing entirely.
+CDIR="$ROOT_DIR/examples/proof_patterns/composition/src/main.con"
+ABS_COMPILER="$(cd "$(dirname "$COMPILER")" && pwd)/$(basename "$COMPILER")"
+from_root="$("$ABS_COMPILER" "$CDIR" --report check-proofs 2>&1 | grep -oE '[0-9]+ verified, [0-9]+ failed' | tail -1)"
+from_tmp="$(cd "$TMP" && "$ABS_COMPILER" "$CDIR" --report check-proofs 2>&1 | grep -oE '[0-9]+ verified, [0-9]+ failed' | tail -1)"
+if [ -n "$from_root" ] && [ "$from_root" = "$from_tmp" ]; then
+  ok "same verdict from the repo root and from elsewhere ($from_root)"
+else
+  no "the replay verdict moved with the working directory: root='$from_root' elsewhere='$from_tmp'"
+fi
+
+# An input with no workspace above it must SAY SO and fail closed, not report a
+# pile of missing theorems that are not missing.
+NOWS="$TMP/nows"; mkdir -p "$NOWS"; cp "$CDIR" "$NOWS/main.con"
+nows_out="$(cd "$NOWS" && "$ABS_COMPILER" "$NOWS/main.con" --report check-proofs 2>&1)"
+nows_rc=0; (cd "$NOWS" && "$ABS_COMPILER" "$NOWS/main.con" --report check-proofs >/dev/null 2>&1) || nows_rc=$?
+if grep -q "cannot locate a Lake workspace" <<<"$nows_out"; then
+  ok "a missing workspace is reported as a missing workspace"
+else
+  no "a missing workspace is not named; got: $(printf '%s' "$nows_out" | tr '\n' ' ' | head -c 200)"
+fi
+if grep -qi "theorem_lookup" <<<"$nows_out"; then
+  no "a missing workspace is still blamed on the theorems (theorem_lookup)"
+else
+  ok "no theorem is blamed for a workspace that was never found"
+fi
+[ "$nows_rc" -ne 0 ] && ok "unreplayable input fails closed (rc=$nows_rc)" \
+                     || no "unreplayable input exited 0 — replay must fail closed"
+
 echo
 echo "PROOF-FRESHNESS: PASS=$PASS FAIL=$FAIL"
 [ "$FAIL" -eq 0 ]