git

A trusted clauz3 layer for running local git from a proved program, with subcommand, location, and push-target policies an agent can prove before any command runs.

These effects are real, not mocks: git shells out to the git binary and git_push actually pushes. 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. Arguments are passed as an explicit vector (never a shell string), so a subcommand and its arguments cannot smuggle extra commands.

Install

clauz3 install stdlib:git

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

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

Effects

Import with from tools.git.trusted.effects import git, git_push:

• git(subcommand: str, args: list[str], cwd: str) -> str — run git <subcommand> <args...> in cwd and return its stdout. Precondition: subcommand and cwd non-empty.
• git_push(remote: str, branch: str, cwd: str) -> str — push branch to remote from the repo at cwd. Precondition: all three non-empty.

Contracts

Import with from tools.git.trusted import contracts as git_rules:

• git_rules.no_guarantees() — explicit null contract.
• git_rules.no_git() — the program runs no local git subcommands (does not by itself forbid git_push; stack no_push()).
• git_rules.read_only() — every subcommand is a read-only inspection command (READ_ONLY_SUBCOMMANDS: status, log, diff, show, branch, ...).
• git_rules.only_subcommands(allowlist) — every subcommand is in allowlist.
• git_rules.never_subcommands(blocklist) — no subcommand is in blocklist.
• git_rules.only_in(root) — every subcommand runs in a directory under root.
• git_rules.runs_at_most(count) — at most count subcommands run.
• git_rules.no_push() — the program performs no pushes.
• git_rules.only_push_to_remote(remote) — every push targets remote.
• git_rules.only_push_to_branch(branch) — every push targets branch.

read_only, only_subcommands, and never_subcommands are subcommand-name policies; only_in is a path-prefix policy compiled to str.startswith.

Example

import clauz3
from tools.git.trusted import contracts as git_rules
from tools.git.trusted.effects import git, git_push


@clauz3.guarantee(git_rules.never_subcommands(["reset", "clean"]))
@clauz3.guarantee(git_rules.only_in("/repo"))
@clauz3.guarantee(git_rules.only_push_to_branch("main"))
def main() -> None:
    git("add", ["-A"], "/repo")
    git("commit", ["-m", "automated update"], "/repo")
    git_push("origin", "main", "/repo")

Stacking guarantees confines the program to a single working tree, forbids destructive subcommands, and pins the push target to main. A git("clean", ...) or a git_push("origin", "release", ...) 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/git/tools/git/trusted/effects.py

"""Trusted git effects: real (non-mock) local ``git`` subprocesses.

The workhorse ``git`` effect runs any git subcommand in a working directory and
returns its stdout. It is recorded by name so the contracts in
``contracts.py`` can scope *which* subcommands an agent may run (the headline
``read_only`` guard), *where* they run, and *how many* times.

``git_push`` is split out as its own effect: pushing is the one
local-git operation that mutates a remote and touches the network, so its
remote and branch target deserve their own policy surface rather than being
folded into an opaque argument list.

The bodies shell out with an explicit argument vector (never a shell string),
so a subcommand and its arguments cannot smuggle extra commands. Each body uses
``subprocess.run``, so ``syscall`` is declared among their deal markers. The
prover never runs these bodies — it records each call as a fact and proves
the declared contracts. The bodies run only under ``clauz3 run``.
"""

import subprocess

import deal

import clauz3
from clauz3._path_safety import has_no_parent_segments

DEFAULT_TIMEOUT_SECONDS = 120


@clauz3.requires(
    lambda subcommand, args, cwd: has_no_parent_segments(cwd),
    message="cwd must not contain parent-directory segments",
)
@clauz3.requires(
    lambda subcommand, args, cwd: len(subcommand) > 0 and len(cwd) > 0,
    message="subcommand and cwd must be non-empty",
)
@deal.has("io", "syscall")
@clauz3.trusted
def git(subcommand: str, args: list[str], cwd: str) -> str:
    """Run ``git <subcommand> <args...>`` in ``cwd`` and return its stdout.

    Arguments are passed as an explicit vector, so neither ``subcommand`` nor
    any entry of ``args`` is interpreted by a shell. Which subcommands may run
    (e.g. ``read_only``) and where they may run (``only_in``) are agent-stated
    guarantees over the ``git`` effect.
    """
    completed = subprocess.run(  # noqa: S603
        ["git", "-C", cwd, subcommand, *args],
        capture_output=True,
        text=True,
        timeout=DEFAULT_TIMEOUT_SECONDS,
        check=True,
    )
    return completed.stdout


@clauz3.requires(
    lambda remote, branch, cwd: has_no_parent_segments(cwd),
    message="cwd must not contain parent-directory segments",
)
@clauz3.requires(
    lambda remote, branch, cwd: len(remote) > 0 and len(branch) > 0 and len(cwd) > 0,
    message="remote, branch, and cwd must be non-empty",
)
@deal.has("network", "io", "syscall")
@clauz3.trusted
def git_push(remote: str, branch: str, cwd: str) -> str:
    """Push ``branch`` to ``remote`` from the repository at ``cwd``.

    Recorded as its own effect so ``contracts.no_push()`` can forbid
    pushing entirely, while ``only_push_to_remote`` / ``only_push_to_branch``
    pin the destination an agent is allowed to publish to.
    """
    completed = subprocess.run(  # noqa: S603
        ["git", "-C", cwd, "push", remote, branch],
        capture_output=True,
        text=True,
        timeout=DEFAULT_TIMEOUT_SECONDS,
        check=True,
    )
    return completed.stdout

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

"""Git subcommand and push policies built from generic trusted effect facts.

Local git subcommands are recorded as the ``git`` effect and pushes as
``git_push`` (see ``effects.py``). These contracts let an agent state which
subcommands it may run, where they run, how many run, and — for pushes — which
remote and branch it is allowed to publish to.

``read_only`` is the headline guard: it pins every subcommand to a fixed set of
inspection commands that cannot mutate the working tree, the index, or any
remote, which is exactly what you want when handing a repository to an agent
that should only look.
"""

from tools.git.trusted.effects import git, git_push

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

Git = effect(git)
Push = effect(git_push)

#: Subcommands that only read repository state — they touch neither the working
#: tree, the index, nor any remote. ``read_only`` pins every subcommand to this
#: set. Deliberately excludes network commands like ``fetch``/``pull`` and any
#: mutation (``commit``, ``checkout``, ``reset``, ``clean``, ``rebase``, ...).
READ_ONLY_SUBCOMMANDS = [
    "status",
    "log",
    "diff",
    "show",
    "branch",
    "remote",
    "rev-parse",
    "ls-files",
    "ls-tree",
    "blame",
    "describe",
    "tag",
    "shortlog",
    "reflog",
    "cat-file",
    "config",
]


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


@contract
def no_git() -> ContractSpec:
    """Guarantee the program runs no local git subcommands.

    Does not by itself forbid ``git_push``; stack ``no_push()`` for that.
    """
    return Git.empty()


@contract
def read_only() -> ContractSpec:
    """Guarantee every git subcommand is a read-only inspection command.

    Pins each subcommand to ``READ_ONLY_SUBCOMMANDS``, so the program cannot
    mutate the working tree, index, or any remote via the ``git`` effect.
    """
    return Git.all(lambda e: e.subcommand in READ_ONLY_SUBCOMMANDS)


@contract
def only_subcommands(allowlist: list[str]) -> ContractSpec:
    """Guarantee every git subcommand is in ``allowlist``."""
    return Git.all(lambda e: e.subcommand in allowlist)


@contract
def never_subcommands(blocklist: list[str]) -> ContractSpec:
    """Guarantee no git subcommand is in ``blocklist``.

    Useful to veto specific destructive subcommands (``reset``, ``clean``,
    ``rebase``) while leaving the rest of git available.
    """
    return Git.all(lambda e: e.subcommand not in blocklist)


@contract
def only_in(root: str) -> ContractSpec:
    """Guarantee every git subcommand runs in a directory under ``root``."""
    return Git.all(lambda e: e.cwd.startswith(root))


@contract
def runs_at_most(count: int) -> ContractSpec:
    """Guarantee at most ``count`` git subcommands run."""
    return Git.count() <= count


@contract
def no_push() -> ContractSpec:
    """Guarantee the program performs no git pushes."""
    return Push.empty()


@contract
def only_push_to_remote(remote: str) -> ContractSpec:
    """Guarantee every push targets the remote named ``remote``."""
    return Push.all(lambda e: e.remote == remote)


@contract
def only_push_to_branch(branch: str) -> ContractSpec:
    """Guarantee every push targets the branch named ``branch``."""
    return Push.all(lambda e: e.branch == branch)

All cases

Browse the full set on the all-cases page.