delete_file: no sha precondition, and a directory path deletes the whole subtree #3757

Describe the bug

delete_file does not use DELETE /repos/{owner}/{repo}/contents/{path} (which requires the blob sha). It builds a tree entry {path, mode 100644, type blob, sha: nil} on top of the branch's current head and commits it through the Git Data API. That has two effects:

1. No precondition. The input schema has no sha property. A sha argument is accepted and silently ignored. A file another writer changed after the caller read it is deleted anyway.
2. No type check on the path. A directory path removes every file under it, recursively, and the tool reports success.

Code (main 99d6d65, unchanged since v2.1.0): pkg/github/repositories.go:1333 (DeleteFile; required owner, repo, path, message, branch, no sha), :1430-1441 (nil-sha tree entry, CreateTree on the head's tree).

Affected version

v2.1.0 (image sha256:f6056fc1…0f8a, commit 4bcdcdf) and main nightly (image sha256:48bc16d0…338f, revision 99d6d65). Local stdio, fine-grained PAT.

Steps to reproduce the behavior

Stale delete:

1. On branch test, create p4/del.txt with content d0. Its blob sha is S0.
2. A second writer updates the file (PUT /contents with sha: S0, content d1-written-after-read). Its blob sha is now S1.
3. Call:

   {"name":"delete_file","arguments":{"owner":"OWNER","repo":"REPO","branch":"test","path":"p4/del.txt","message":"delete","sha":"S0"}}

4. Result: success with a new commit. GET /contents/p4/del.txt?ref=test returns 404. The newer content is gone, although S0 != S1.

Directory path:

1. push_files p4/dir/a.txt and p4/dir/sub/b.txt to test.
2. Call:

   {"name":"delete_file","arguments":{"owner":"OWNER","repo":"REPO","branch":"test","path":"p4/dir","message":"delete"}}

3. Result: success. Tree before: p4/dir/a.txt, p4/dir/sub/b.txt. Tree after: neither file.

Expected vs actual behavior

Expected:

• A sha parameter, as create_or_update_file has, checked against the current blob. A stale sha is refused, or at the least an unsupported sha argument is not silently accepted.
• A directory path is rejected ("path is a directory").

Actual: both calls succeed. The schema gives a caller no way to make the delete conditional.

Suggested fix: before building the tree, fetch the entry at path on branch. Refuse if it is not a blob, and refuse if a supplied sha differs from its sha. Using the Contents DELETE endpoint would enforce both, but the comment above DeleteFile (repositories.go:1327-1331) says the Git Data route is deliberate, because the Contents endpoint does not sign the deletion commit. A pre-check on the current code path avoids that trade-off. Note: open PR #3288 moves delete_file onto a shared commit path that retries a ref conflict by rebuilding on the latest tip. Without a sha check, that retry would also delete content written during the retry window.

Logs

delete_file (stale sha S0, current S1)  -> OK {"commit":{"sha":"f9953c67…", …}}   (v2.1.0)
                                        -> OK {"commit":{"sha":"a5e7ecf5…", …}}   (main)
GET contents p4/del.txt                 -> 404
delete_file path "p4/dir"               -> OK {"commit":{"sha":"47c16484…", …}}   (v2.1.0); 3b1e4ad3… (main)
tree p4/* before: p4/dir/a.txt, p4/dir/sub/b.txt, p4/stale.txt   after: p4/stale.txt
tools/list delete_file properties: branch, message, owner, path, repo

Found during an independent audit of v2.1.0 on a throwaway org and private test repo. Prepared with AI assistance (Claude Code); reproduced by two independent test runs before filing.