fix(lock): support NOWAIT and FOR SHARE SKIP LOCKED

.agents/skills/mo-dev/references/cgo-build-test.md

@@ -82,14 +82,63 @@ Prefer the repository wrapper for arbitrary packages and test flags:
 .agents/skills/mo-dev/scripts/mo-cgo-test -race -count=1 -timeout=240s ./pkg/target/...
 ```
 
+Linked worktrees do not contain ignored build artifacts. When the current
+worktree lacks `cgo/libmo.dylib` on macOS or `cgo/libmo.so` on Linux (or lacks
+`thirdparties/install`), the wrapper automatically considers the primary
+worktree's platform-matched artifacts. It reuses them only when `Makefile`,
+`cgo/`, and `thirdparties/` are clean and identical at both revisions and the
+primary artifact carries a matching source/platform/build-key provenance
+stamp written by the top-level `make cgo` target. The target owns a
+`prepare -> clean when required -> begin -> build -> record` protocol: CGo
+source/header and CPU/GPU or release/debug changes clean all CGo outputs;
+SIMSIMD, Makefile, thirdparty, platform, missing-stamp, or corrupt-stamp changes
+clean both thirdparties and CGo. An interrupted generation stays non-reusable
+and is cleaned again on the next build. This prevents an incremental no-op from
+simply relabeling an old library as current. Missing, stale, CPU/GPU/SIMSIMD-
+mismatched, or post-stamp-modified artifacts are rejected with a local rebuild
+request. The first top-level build after this guard is introduced intentionally
+performs one full native rebuild before reuse is possible.
+
+Cross-worktree reuse is best-effort, never required for correctness. Git
+layouts that do not expose a real primary checkout (for example, a linked
+worktree created from an unconfigured `--separate-git-dir` repository) are
+rejected instead of guessing a filesystem path; build the native artifacts in
+the current worktree in that environment.
+
+An exported/non-Git source tree keeps the historical incremental `make cgo`
+behavior and never publishes a reusable stamp. `make -n`, `make -t`, and
+`make -q` also remain non-mutating; they do not create generation markers or
+clean native outputs.
+
+Do not invoke the provenance helper's `record` operation directly or manually
+create symlinks before trying the wrapper. The former is rejected without the
+build-generation marker, and the latter bypasses the guard and leaves untracked
+setup residue in the review worktree. Validate changes to this protocol with:
+
+Top-level `make cgo` already builds and stages thirdparties as the single
+complete-generation owner. Do not precede it with standalone `make
+thirdparties`: a partial generation has no complete stamp and is intentionally
+discarded by `make cgo`. Direct `make -C thirdparties` followed by `make -C
+cgo` remains the separate ordered contract used by Docker native stages.
+
+```bash
+.agents/skills/mo-dev/scripts/mo-native-provenance-test
+.agents/skills/mo-dev/scripts/mo-native-build-contract-test
+.agents/skills/mo-dev/scripts/mo-cgo-test-worktree-artifacts-test
+```
+
 It verifies host/target and CGo prerequisites, enforces the repository's
 `GOWORK=off` and `-mod=readonly` contract, removes ambient CGo flag drift,
 chooses the supported OS library/loader form, and gives temporary test
 executables absolute rpaths. It is a local CPU-test entry point; GPU and static
 cross-builds have different toolchain contracts and remain explicit workflows.
-`GOFLAGS`, `GOEXPERIMENT`, `CC`, and `CXX` remain caller-owned inputs; record
-them when attribution or reproducibility depends on them, and ensure native
-artifacts were built from the same source generation.
+`GOFLAGS` and `GOEXPERIMENT` remain caller-owned Go inputs. Native provenance
+also hashes supported compiler/SDK/flag override values (including `CC`,
+`CXX`, and GPU environment selectors), so a custom profile cannot alias the
+default profile. It does not fingerprint compiler or SDK installation bytes;
+record exact tool versions separately when attribution or reproducibility
+depends on them. GPU Pixi lock changes invalidate the common provenance and
+force a full thirdparty rebuild even if compiler paths stay unchanged.
 
 ### Why test rpaths differ from packaged binaries
 
@@ -287,66 +336,66 @@ cannot erase the evidence before comparison.
 
 GPU support compiles the CUDA-backed vector index algorithms (**CAGRA**, **IVF-PQ**) into `libmo` and turns on the `gpu` Go build tag. Linux x86_64 only. The macOS Makefile branch carries no CUDA flags, so macOS builds are CPU-only. Do not try to enable it on Darwin.
 
-Prerequisites:
-
-1. CUDA toolkit matching the versions pinned by
-   `optools/images/gpu/Dockerfile` and
-   `optools/images/gpu/go_cuda-130_arch-x86_64.yaml`, installed under the path
-   expected by those files. Do not infer an unsupported version range.
-2. cuVS Go bindings installed from the repository's Linux x86_64 environment
-   file and the environment activated so `CONDA_PREFIX` is exported. Prefer the
-   builder stage in `optools/images/gpu/Dockerfile` when a container runtime is
-   available. Building does not require a GPU device; executing GPU workloads
-   requires a compatible NVIDIA host/runtime.
+GPU builds use the frozen Pixi profile in `optools/gpu/pixi.toml`; system
+CUDA/Conda and a separate GPU toolchain manifest are not providers. CPU-only
+builds do not invoke Pixi. MO GPU-only builds use MO's profile; combined
+MO/Sirius builds use Sirius's `mo` profile for both components. Compilation
+needs no GPU device, but execution needs a compatible NVIDIA host driver.
 
 ```bash
-conda env create --name go -f optools/images/gpu/go_cuda-130_arch-x86_64.yaml
-conda activate go
-```
-
-Build:
-
-```bash
-MO_CL_CUDA=1 make -j8
+cd optools/gpu
+pixi run --frozen make -C ../.. MO_CL_CUDA=1 -j8
 ```
 
 What `MO_CL_CUDA=1` flips:
 
 | Layer | CPU build | GPU build (`MO_CL_CUDA=1`) |
 |-------|-----------|----------------------------|
 | Go build tag | none | `-tags gpu` -- registers CAGRA + IVF-PQ, compiles `*_gpu.go` |
-| `cgo/` compiler | `gcc`/`clang` | `/usr/local/cuda/bin/nvcc` |
+| `cgo/` compiler | `gcc`/`clang` | Pixi `bin/nvcc` with Pixi host compiler |
 | `libmo` objects | C objects only | + `cuda/*.o` + `cuvs/*.o` |
+| Runtime sidecar | none | `mocl_kernel64.fatbin` beside `mo-service` |
 | Link flags | `-lusearch_c -lroaring` | + `-lcuvs -lcuvs_c -lcudart -lcuda -lrmm -lstdc++` |
-| Header/lib roots | thirdparties only | + `$CONDA_PREFIX/{include,lib}`, `/usr/local/cuda/...` |
+| Header/lib roots | thirdparties only | + Pixi `include/lib` and `targets/x86_64-linux/include/lib` |
 
 Guardrails:
 
-- `CONDA_PREFIX env variable not found`: conda env not activated. Run `conda activate <env>` first. This is not a code bug.
+- Missing Pixi activation or CUDA/cuVS files: use `pixi run --frozen` and
+  verify the locked environment. There is no system CUDA fallback. A shell
+  stays activated after
+  `eval "$(pixi shell-hook --manifest-path optools/gpu/pixi.toml --frozen)"`;
+  plain `make MO_CL_CUDA=1 -j8` then works from the repository root.
+- `gmake[2]: *** internal error: invalid --jobserver-auth string 'fifo:...'`:
+  CMake ran the host `gmake` under Pixi's make 4.4. The Pixi activation sets
+  `CMAKE_GENERATOR=Ninja`; the error means the build ran without it. Do not pass
+  `--jobserver-style=pipe`: ninja ignores a pipe jobserver and schedules
+  outside the outer `-j` budget.
 - `libmo` is re-linked on every GPU build deliberately because `mo-service` loads `libmo.so` dynamically. A stale `.so` silently runs old C++.
+- Use the top-level build owner. It content-binds and atomically stages
+  `mocl_kernel64.fatbin` beside `mo-service`; direct `make -C cgo` does not
+  produce a complete distributable GPU generation.
 - Always pass `-j8`. The cuVS/CUDA objects dominate a GPU build and a single-threaded `make` stalls the edit-build-test loop for minutes at a time.
 
 The `gpu` tag gates index-plugin registration. CAGRA and IVF-PQ register only under `//go:build gpu` (`pkg/indexplugin/all/all_gpu.go`). On a CPU binary their plugins are absent from the registry, so `CREATE INDEX ... USING ivfpq|cagra` fails cleanly at plan-build with `unsupported index type: <algo>` before hidden table creation. Do not move those imports into `all.go`.
 
 The linked `libmo` must itself be GPU-built:
 
 ```bash
-MO_CL_CUDA=1 make -j8 cgo
+cd optools/gpu
+pixi run --frozen make -C ../.. MO_CL_CUDA=1 -j8 cgo
 ```
 
-GPU tests need `-tags gpu` plus CUDA search paths. Linux only:
+GPU tests need the `gpu` tag and Pixi CUDA search paths. The repository
+wrapper supplies both after validating the native generation. Linux only:
 
 ```bash
-gpu_package=./pkg/vectorindex/ivfpq/... # set to the affected GPU algorithm package
-CGO_CFLAGS="-I$(pwd)/cgo -I$(pwd)/thirdparties/install/include -I$CONDA_PREFIX/include -I/usr/local/cuda/include" \
-CGO_LDFLAGS="-L$(pwd)/thirdparties/install/lib -lusearch_c -L$CONDA_PREFIX/lib -lcuvs -lcuvs_c" \
-LD_LIBRARY_PATH="$(pwd)/cgo:$(pwd)/thirdparties/install/lib:$CONDA_PREFIX/lib:/usr/local/cuda/lib64" \
-GOWORK=off go test -mod=readonly -tags gpu \
-  -ldflags="-extldflags '-L$(pwd)/cgo -lmo -L$(pwd)/thirdparties/install/lib -Wl,-rpath,$(pwd)/cgo -Wl,-rpath,$(pwd)/thirdparties/install/lib -Wl,-rpath,$CONDA_PREFIX/lib -Wl,-rpath,/usr/local/cuda/lib64 -fopenmp'" \
-  -v -count=1 -timeout 300s "$gpu_package"
+pixi run --frozen env MO_CL_CUDA=1 \
+  ../../.agents/skills/mo-dev/scripts/mo-cgo-test \
+  -v -count=1 -timeout=300s ./pkg/vectorindex/ivfpq/...
 ```
 
-The authoritative flag source is the Makefile (`CUDA_CFLAGS` / `CUDA_LDFLAGS`), not this snippet. If a GPU link error appears, diff your flags against those lines.
+The authoritative flag source is the Pixi profile consumed by Make and the
+wrapper. Do not hand-assemble a second CUDA search path.
 
 Tag-split test files are a trap: `*_gpu.go` / `//go:build gpu` tests compile only under `-tags gpu`. A plain `go test ./pkg/vectorindex/ivfpq/...` runs `//go:build !gpu` / `*_cpu.go` stubs instead. CPU tests passing does not test the GPU path.
 
@@ -394,6 +443,12 @@ and appending would discard the caller's. The effect was a false green:
 package's 2 GPU test files while reporting a pass. `mo-cgo-test-tags-test` pins every form
 and needs no GPU, CUDA toolkit or built libmo.
 
+Go test executables run from temporary directories, so they cannot find the
+production sidecar beside the repository's `mo-service`. The wrapper verifies
+the selected generation and exports `MO_CUDA_FATBIN_PATH` to its stamped
+executable-side copy before starting `go test`; do not copy an arbitrary fatbin
+into Go's temporary build directories.
+
 Stubbing `go` is not enough to earn that, and the first version of the test wrongly
 claimed it: the wrapper resolves its repository from its own location and rejects the run
 unless `cgo/libmo.so` and `thirdparties/install/include` exist there, before it would ever
@@ -410,4 +465,3 @@ predates it ignores `MO_CL_CUDA` entirely and fails to link a GPU-built `libmo`
 `grep -c MO_CL_CUDA .agents/skills/mo-dev/scripts/mo-cgo-test` before concluding the tree is
 broken; borrow a newer copy into the repo root if needed (it derives the repo from its own
 location, so it must sit inside the worktree).
-

.agents/skills/mo-dev/references/counterexample-testing.md

@@ -45,7 +45,10 @@ Comments and implementation assumptions are not evidence. A nil check proves def
 4. Add the narrowest white-box test when it proves a distinct internal transformation, totality, or state-boundary claim.
 5. Vary independent dimensions around the witness, including both controls and counterexamples.
 6. Use differential or metamorphic relationships where a direct expected value would duplicate implementation logic.
-7. Run the tests against the unfixed revision and record the intended failure reason.
+7. Establish or reuse evidence valid under
+   [validation-evidence.md](validation-evidence.md) that the same tests fail on
+   the unfixed revision for the intended semantic reason; do not make every
+   reviewer rerun an identical historical baseline.
 8. Apply the production fix, then rerun the same tests.
 9. Remove redundant cases and retain one reason for every remaining row.
 10. Place tests at their natural ownership layer: focused unit coverage near the invariant and public-path regression coverage near the user-visible contract.
@@ -187,7 +190,7 @@ Before accepting a regression change, verify:
 ```text
 □ The invariant and its negation are explicit.
 □ For an externally visible claim, the public-path witness proves the internal state is reachable; an internal-only contract is explicitly documented as such.
-□ The unfixed revision fails for the claimed reason.
+□ Valid, reviewable evidence shows the unfixed revision fails for the claimed reason.
 □ The fixed revision passes with the same assertions.
 □ A black-box semantic oracle exists when behavior is externally visible.
 □ White-box assertions inspect stable typed structure, not incidental layout.