Text — all cases

Every case file under examples/text/cases/, inlined. _pass cases should prove; _fail cases should be rejected by the prover.

See the curated walk-through for context on the trusted module and contract vocabulary.

examples/text/cases/edit_length_at_most_fail.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import edit_file

import clauz3


@clauz3.guarantee(text.edit_length_at_most(40))
def main() -> None:
    edit_file(
        "/repo/notes.txt",
        "this replacement body is well beyond the forty character limit",
    )

examples/text/cases/edit_length_at_most_pass.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import edit_file

import clauz3


@clauz3.guarantee(text.only_edit_under("/repo/"))
@clauz3.guarantee(text.edit_length_at_most(40))
def main() -> None:
    edit_file("/repo/notes.txt", "a short, bounded replacement body\n")

examples/text/cases/empty_text_precondition_fail.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.length_at_most(20))
def main() -> None:
    send_message("general", "")

examples/text/cases/length_at_least_fail.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.length_at_least(5))
def main() -> None:
    send_message("general", "hi")

examples/text/cases/length_at_least_pass.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.length_at_least(5))
def main() -> None:
    send_message("general", "hello there")

examples/text/cases/length_at_most_fail.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.length_at_most(20))
def main() -> None:
    send_message("general", "this message is clearly longer than twenty chars")

examples/text/cases/length_at_most_pass.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.length_at_most(20))
def main() -> None:
    send_message("general", "ship it")
    send_message("alerts", "deploy finished ok")

examples/text/cases/length_between_branch_pass.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.length_between(3, 20))
def main(urgent: bool) -> None:
    if urgent:
        send_message("alerts", "page on-call now")
    else:
        send_message("general", "all quiet")

examples/text/cases/length_between_pass.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.length_between(3, 20))
def main() -> None:
    send_message("general", "ready to ship")

examples/text/cases/must_contain_fail.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.must_contain("[automated]"))
def main() -> None:
    send_message("general", "build succeeded")

examples/text/cases/must_contain_pass.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.must_contain("[automated]"))
def main() -> None:
    send_message("general", "[automated] build succeeded")
    send_message("alerts", "nightly job done [automated]")

examples/text/cases/must_not_contain_fail.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.must_not_contain("password"))
def main() -> None:
    send_message("general", "the password is hunter2")

examples/text/cases/must_not_contain_pass.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.must_not_contain("password"))
def main() -> None:
    send_message("general", "rotated the credentials, all good")

examples/text/cases/no_edits_fail.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import edit_file

import clauz3


@clauz3.guarantee(text.no_edits())
def main() -> None:
    edit_file("/repo/notes.txt", "but this run does edit a file\n")

examples/text/cases/no_edits_pass.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.no_edits())
def main() -> None:
    send_message("general", "read-only run, no files touched")

examples/text/cases/no_regex_metacharacters_fail.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.no_regex_metacharacters())
def main() -> None:
    send_message("search", "(a+)+$")

examples/text/cases/no_regex_metacharacters_pass.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.no_regex_metacharacters())
def main() -> None:
    send_message("search", "plain alphanumeric query 42")

examples/text/cases/only_edit_under_fail.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import edit_file

import clauz3


@clauz3.guarantee(text.only_edit_under("/repo/src/"))
def main() -> None:
    edit_file("/etc/passwd", "root::0:0::/root:/bin/sh\n")

examples/text/cases/only_edit_under_pass.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import edit_file

import clauz3


@clauz3.guarantee(text.only_edit_under("/repo/src/"))
def main() -> None:
    edit_file("/repo/src/main.py", "print('hello')\n")
    edit_file("/repo/src/util.py", "x = 1\n")

examples/text/cases/sends_at_most_fail.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.sends_at_most(2))
def main() -> None:
    send_message("general", "one")
    send_message("general", "two")
    send_message("general", "three")

examples/text/cases/sends_at_most_pass.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.sends_at_most(2))
def main(urgent: bool) -> None:
    send_message("general", "starting run")
    if urgent:
        send_message("alerts", "needs attention")

examples/text/cases/text_no_guarantees_pass.py

# ruff: noqa: F821
from tools.text.trusted import contracts as text
from tools.text.trusted.effects import send_message

import clauz3


@clauz3.guarantee(text.no_guarantees())
def main() -> None:
    send_message("general", "anything goes here")