filesystem

A trusted clauz3 layer for reading and writing files, with path-prefix policies an agent can prove before any file is touched.

Unlike the layers under examples/, these effects are real, not mocks: read_file actually reads and write_file actually writes. The prover never runs their bodies — it records each call as a fact and proves the contract. The bodies run only under clauz3 run, after a program is proved and approved.

Install

clauz3 install stdlib:filesystem

This copies tools/filesystem/ into your project. Then prove a program against it:

clauz3 prove --trusted-root tools/filesystem/trusted plan.py

Effects

Import with from tools.filesystem.trusted.effects import read_file, write_file:

• read_file(path: str) -> str — read a UTF-8 text file. Precondition: path is non-empty. Recorded under the read marker.
• write_file(path: str, content: str) -> None — write UTF-8 text, creating parent directories. Precondition: path is non-empty. Recorded under the write marker.

Contracts

Import with from tools.filesystem.trusted import contracts as fs:

• fs.no_guarantees() — explicit null contract.
• fs.read_only() — the program performs no writes.
• fs.no_reads() — the program reads no files.
• fs.only_read_under(root) — every read path is under root.
• fs.only_write_under(root) — every write path is under root.
• fs.never_read_under(prefix) — no read path is under prefix.
• fs.never_write_under(prefix) — no write path is under prefix.
• fs.writes_at_most(count) — at most count writes occur.

only_* and never_* are path-prefix policies, compiled to str.startswith over the symbolic call argument.

Example

import clauz3
from tools.filesystem.trusted import contracts as fs
from tools.filesystem.trusted.effects import read_file, write_file


@clauz3.guarantee(fs.only_read_under("/repo"))
@clauz3.guarantee(fs.only_write_under("/repo/build"))
def main() -> None:
    source = read_file("/repo/src/app.py")
    write_file("/repo/build/app.txt", source)

Stacking guarantees confines the program to reading under /repo and writing under /repo/build. A write to /etc/passwd or a read of /home/user/.ssh/id_rsa would fail the proof.

Tests

just -f tests/Justfile test

tests/cases/*_pass.py must prove; tests/cases/*_fail.py must not.

Source

src/clauz3/stdlib/filesystem/tools/filesystem/trusted/effects.py

"""Trusted filesystem effects.

These are real (non-mock) side-effecting functions. The prover never executes
their bodies: it records each call as an effect fact and proves the declared
preconditions. The bodies run only under ``clauz3 run``, after a program has
been proved and approved.

Reads carry deal's ``read`` marker and writes carry the ``write`` marker, so
the contracts in ``contracts.py`` can constrain *where* on the filesystem a
program may read or write.
"""

from pathlib import Path

import deal


@deal.pre(lambda path: len(path) > 0, message="path must be non-empty")
@deal.has("read", "trusted")
def read_file(path: str) -> str:
    """Read and return the UTF-8 text contents of ``path``."""
    return Path(path).read_text(encoding="utf-8")


@deal.pre(lambda path, content: len(path) > 0, message="path must be non-empty")
@deal.has("write", "trusted")
def write_file(path: str, content: str) -> None:
    """Write ``content`` to ``path`` as UTF-8 text, creating parent dirs."""
    target = Path(path)
    target.parent.mkdir(parents=True, exist_ok=True)
    target.write_text(content, encoding="utf-8")

src/clauz3/stdlib/filesystem/tools/filesystem/trusted/contracts.py

"""Filesystem path policies built from generic trusted effect facts.

Reads are recorded under the ``read`` marker and writes under the ``write``
marker (see ``effects.py``). These contracts let an agent state *where* it is
allowed to read and write, as path-prefix policies. The prefix checks use the
relation-lambda ``str.startswith`` support in ``clauz3.spec``.
"""

from clauz3.spec import ContractSpec, contract, effect
from clauz3.spec import no_guarantees as core_no_guarantees

Read = effect("read")
Write = effect("write")


@contract
def no_guarantees() -> ContractSpec:
    """Make no guarantees about filesystem effects."""
    return core_no_guarantees()


@contract
def read_only() -> ContractSpec:
    """Guarantee the program performs no filesystem writes."""
    return Write.empty()


@contract
def no_reads() -> ContractSpec:
    """Guarantee the program reads no files."""
    return Read.empty()


@contract
def only_read_under(root: str) -> ContractSpec:
    """Guarantee every file read has a path under ``root``."""
    return Read.all(lambda e: e.path.startswith(root))


@contract
def only_write_under(root: str) -> ContractSpec:
    """Guarantee every file write has a path under ``root``."""
    return Write.all(lambda e: e.path.startswith(root))


@contract
def never_read_under(prefix: str) -> ContractSpec:
    """Guarantee no file read has a path under ``prefix``."""
    return Read.all(lambda e: not e.path.startswith(prefix))


@contract
def never_write_under(prefix: str) -> ContractSpec:
    """Guarantee no file write has a path under ``prefix``."""
    return Write.all(lambda e: not e.path.startswith(prefix))


@contract
def writes_at_most(count: int) -> ContractSpec:
    """Guarantee at most ``count`` file writes occur."""
    return Write.count() <= count

All cases

Browse the full set on the all-cases page.