filesystem — all cases¶
Every case file under src/clauz3/stdlib/filesystem/tests/cases/,
inlined. _pass cases must prove; _fail cases must not.
See the curated walk-through for the trusted module and contract vocabulary.
src/clauz3/stdlib/filesystem/tests/cases/never_read_under_fail.py¶
# ruff: noqa: F821
from tools.filesystem.trusted import contracts as fs
from tools.filesystem.trusted.effects import read_file
import clauz3
@clauz3.guarantee(fs.never_read_under("/home/user/.ssh"))
def main() -> None:
read_file("/home/user/.ssh/id_rsa")
src/clauz3/stdlib/filesystem/tests/cases/never_read_under_pass.py¶
# ruff: noqa: F821
from tools.filesystem.trusted import contracts as fs
from tools.filesystem.trusted.effects import read_file
import clauz3
@clauz3.guarantee(fs.never_read_under("/home/user/.ssh"))
def main() -> None:
read_file("/repo/README.md")
src/clauz3/stdlib/filesystem/tests/cases/never_write_under_fail.py¶
# ruff: noqa: F821
from tools.filesystem.trusted import contracts as fs
from tools.filesystem.trusted.effects import write_file
import clauz3
@clauz3.guarantee(fs.never_write_under("/etc"))
def main() -> None:
write_file("/etc/passwd", "pwned")
src/clauz3/stdlib/filesystem/tests/cases/never_write_under_pass.py¶
# ruff: noqa: F821
from tools.filesystem.trusted import contracts as fs
from tools.filesystem.trusted.effects import write_file
import clauz3
@clauz3.guarantee(fs.never_write_under("/etc"))
def main() -> None:
write_file("/sandbox/notes.txt", "hi")
src/clauz3/stdlib/filesystem/tests/cases/only_read_under_pass.py¶
# ruff: noqa: F821
from tools.filesystem.trusted import contracts as fs
from tools.filesystem.trusted.effects import read_file
import clauz3
@clauz3.guarantee(fs.only_read_under("/repo"))
@clauz3.guarantee(fs.read_only())
def main() -> None:
read_file("/repo/src/app.py")
src/clauz3/stdlib/filesystem/tests/cases/only_write_under_branch_pass.py¶
# ruff: noqa: F821
from tools.filesystem.trusted import contracts as fs
from tools.filesystem.trusted.effects import write_file
import clauz3
@clauz3.guarantee(fs.only_write_under("/sandbox"))
def main(use_logs: bool) -> None:
if use_logs:
write_file("/sandbox/logs/run.txt", "log")
else:
write_file("/sandbox/out/result.txt", "result")
src/clauz3/stdlib/filesystem/tests/cases/only_write_under_fail.py¶
# ruff: noqa: F821
from tools.filesystem.trusted import contracts as fs
from tools.filesystem.trusted.effects import write_file
import clauz3
@clauz3.guarantee(fs.only_write_under("/sandbox"))
def main() -> None:
write_file("/tmp/out.txt", "hi")
src/clauz3/stdlib/filesystem/tests/cases/only_write_under_pass.py¶
# ruff: noqa: F821
from tools.filesystem.trusted import contracts as fs
from tools.filesystem.trusted.effects import write_file
import clauz3
@clauz3.guarantee(fs.only_write_under("/sandbox"))
def main() -> None:
write_file("/sandbox/out.txt", "hi")
src/clauz3/stdlib/filesystem/tests/cases/read_only_fail.py¶
# ruff: noqa: F821
from tools.filesystem.trusted import contracts as fs
from tools.filesystem.trusted.effects import read_file, write_file
import clauz3
@clauz3.guarantee(fs.read_only())
def main() -> None:
read_file("/repo/a.py")
write_file("/repo/a.py", "edited")
src/clauz3/stdlib/filesystem/tests/cases/read_only_pass.py¶
# ruff: noqa: F821
from tools.filesystem.trusted import contracts as fs
from tools.filesystem.trusted.effects import read_file
import clauz3
@clauz3.guarantee(fs.read_only())
def main() -> None:
read_file("/repo/a.py")
read_file("/repo/b.py")
src/clauz3/stdlib/filesystem/tests/cases/writes_at_most_fail.py¶
# ruff: noqa: F821
from tools.filesystem.trusted import contracts as fs
from tools.filesystem.trusted.effects import write_file
import clauz3
@clauz3.guarantee(fs.writes_at_most(1))
def main() -> None:
write_file("/sandbox/a.txt", "a")
write_file("/sandbox/b.txt", "b")