Skip to content

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")

src/clauz3/stdlib/filesystem/tests/cases/writes_at_most_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.writes_at_most(2))
def main() -> None:
    write_file("/sandbox/a.txt", "a")
    write_file("/sandbox/b.txt", "b")