grep

A trusted clauz3 layer that searches files for a substring — a real (non-mock) substitute for an agent's ripgrep tool.

grep builds on filesystem. A grep call reads a file, so it carries the same read marker as read_file, and the filesystem read policies (only_read_under, never_read_under) apply to grep calls unchanged. grep adds its own search-specific contracts on top.

Install

grep depends on the filesystem layer, so install both:

clauz3 install stdlib:filesystem
clauz3 install stdlib:grep

Prove a program against both trusted roots:

clauz3 prove \
  --trusted-roots tools/grep/trusted tools/filesystem/trusted \
  plan.py

Effect

Import with from tools.grep.trusted.effects import grep:

• grep(pattern: str, path: str) -> list[str] — return the lines in path that contain the substring pattern. Precondition: both pattern and path are non-empty. Recorded under the read marker.

Contracts

Import with from tools.grep.trusted import contracts as grep_rules:

• grep_rules.no_guarantees() — explicit null contract.
• grep_rules.only_read_under(root) — every search reads a file under root.
• grep_rules.never_read_under(prefix) — no search reads under prefix.
• grep_rules.searches_at_most(count) — at most count searches occur.
• grep_rules.only_pattern(pattern) — every search uses exactly pattern.

only_read_under and never_read_under delegate to the filesystem read policies, so they also constrain any read_file calls in the same program.

Example

import clauz3
from tools.grep.trusted import contracts as grep_rules
from tools.grep.trusted.effects import grep


@clauz3.guarantee(grep_rules.only_read_under("/repo"))
@clauz3.guarantee(grep_rules.searches_at_most(3))
def main() -> None:
    grep("TODO", "/repo/src/app.py")
    grep("FIXME", "/repo/src/util.py")

A search of /etc/shadow would fail the only_read_under("/repo") proof.

Tests

just -f tests/Justfile test

The grep test Justfile points at both the grep and filesystem layers, since grep imports filesystem.

Source

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

"""Trusted grep effect: a real (non-mock) substitute for an agent's ripgrep.

``grep`` reads a file, so it carries deal's ``read`` marker. That means the
filesystem read policies (``only_read_under``, ``never_read_under``, ...) apply
to grep calls in exactly the same way they apply to ``read_file``. The prover
records each call as a fact; the body runs only under ``clauz3 run``.
"""

from pathlib import Path

import deal


@deal.pre(
    lambda pattern, path: len(pattern) >= 1 and len(path) >= 1,
    message="pattern and path must be non-empty",
)
@deal.has("read", "trusted")
def grep(pattern: str, path: str) -> list[str]:
    """Return the lines in ``path`` that contain the substring ``pattern``."""
    text = Path(path).read_text(encoding="utf-8")
    return [line for line in text.splitlines() if pattern in line]

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

"""Contract vocabulary for the grep tool.

grep is a read effect, so this module builds directly on the ``filesystem``
layer: the path policies below delegate to the filesystem read contracts, and
a grep call is governed by them because it shares the ``read`` marker. grep
also adds its own search-specific contracts (``searches_at_most``,
``only_pattern``).

Requires the ``filesystem`` trusted layer to be installed alongside grep.
"""

from tools.filesystem.trusted import contracts as filesystem

from clauz3.spec import ContractSpec, contract, effect

Grep = effect("grep")


@contract
def no_guarantees() -> ContractSpec:
    """Make no guarantees about grep (or other read) effects."""
    return filesystem.no_guarantees()


@contract
def only_read_under(root: str) -> ContractSpec:
    """Guarantee every grep search reads a file under ``root``."""
    return filesystem.only_read_under(root)


@contract
def never_read_under(prefix: str) -> ContractSpec:
    """Guarantee no grep search reads a file under ``prefix``."""
    return filesystem.never_read_under(prefix)


@contract
def searches_at_most(count: int) -> ContractSpec:
    """Guarantee at most ``count`` grep searches occur."""
    return Grep.count() <= count


@contract
def only_pattern(pattern: str) -> ContractSpec:
    """Guarantee every grep search uses exactly this pattern."""
    return Grep.all(lambda e: e.pattern == pattern)

All cases

Browse the full set on the all-cases page.