Module pathjail_write 

Write destinations below a trusted root that refuse symlinked components.

Project data (<project>/.lean-ctx/...) lives inside a working tree that other people, checkouts and tools can populate. A symlinked .lean-ctx, proofs or target file there must not redirect a LeanCTX write outside the project, so these writes rebuild the path component by component below the trusted root and fail closed on any link. The mechanics (directory handles, O_NOFOLLOW, renameat) live in lean_ctx_fs::confined_write.

Functions

project_data_destination

Check a destination <project>/.lean-ctx/<rel> without writing it.

rebuild_below

Rebuild root/rel component by component, refusing every symlinked component below root (a check only; nothing is created).

relative_below

path as plain components below root: lexically first (so a symlinked component stays visible and is refused), then against the canonical root for a caller that already resolved it.

write_below

Write content to root/rel (file mode on Unix), creating missing directories, without following a symlink anywhere below root.

write_project_data

Write <project>/.lean-ctx/<rel>: the project root is trusted, .lean-ctx and everything below it must not be a symlink.

write_requested_below

Write a caller-chosen destination below root: the lexical requested path when it names plain components below root (a symlinked component then stays visible and is refused), else the jail-resolved jailed path.