Skip to content

Cloud spend caps — all cases

Every case file under examples/cloud/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/cloud/cases/cap_bounds_then_removed_fail.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy, remove_spend_cap

import clauz3


@clauz3.guarantee(cloud.cap_at_most(100))
@clauz3.guarantee(cloud.total_caps_at_most(150))
@clauz3.guarantee(cloud.all_services_capped_at_end())
def main() -> None:
    deploy("api", 50)
    remove_spend_cap("api")  # the end-state guarantee rejects this

examples/cloud/cases/cap_bounds_then_removed_pass.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy, remove_spend_cap

import clauz3


# Proves: cap bounds only constrain deploy caps. They do not see the later
# removal, so the service ends up billing without limit. See the paired
# _fail case for the guarantee that closes this gap.
@clauz3.guarantee(cloud.cap_at_most(100))
@clauz3.guarantee(cloud.total_caps_at_most(150))
def main() -> None:
    deploy("api", 50)
    remove_spend_cap("api")

examples/cloud/cases/cap_too_high_fail.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy

import clauz3


@clauz3.guarantee(cloud.cap_at_most(100))
def main() -> None:
    deploy("api", 50)
    deploy("worker", 5000)  # one service's cap breaks the per-service bound

examples/cloud/cases/capped_at_end_fail.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy, remove_spend_cap

import clauz3


@clauz3.guarantee(cloud.all_services_capped_at_end())
def main() -> None:
    deploy("api", 50)
    deploy("worker", 20)
    remove_spend_cap("worker")  # worker is left billing without limit

examples/cloud/cases/capped_at_end_pass.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy, remove_spend_cap

import clauz3


@clauz3.guarantee(cloud.all_services_capped_at_end())
def main() -> None:
    # Lift the cap for a one-off backfill, then redeploy with a cap.
    deploy("api", 50)
    remove_spend_cap("api")
    deploy("api", 50)

examples/cloud/cases/capped_deploy_pass.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy

import clauz3


@clauz3.guarantee(cloud.cap_at_most(100))
@clauz3.guarantee(cloud.only_services(["api", "worker"]))
def main() -> None:
    deploy("api", 50)
    deploy("worker", 20)

examples/cloud/cases/estimate_clamped_pass.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy, estimate_monthly_cost

import clauz3


@clauz3.guarantee(cloud.cap_at_most(100))
def main() -> None:
    headroom = 2 * estimate_monthly_cost("api")
    if headroom > 100:
        deploy("api", 100)
    elif headroom > 0:
        deploy("api", headroom)
    else:
        deploy("api", 1)

examples/cloud/cases/estimate_unclamped_fail.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy, estimate_monthly_cost

import clauz3


@clauz3.guarantee(cloud.cap_at_most(100))
def main() -> None:
    headroom = 2 * estimate_monthly_cost("api")
    deploy("api", headroom + 1)  # unclamped: a large estimate exceeds the cap

examples/cloud/cases/only_services_fail.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy

import clauz3


@clauz3.guarantee(cloud.only_services(["api", "worker"]))
def main() -> None:
    deploy("api", 50)
    deploy("crypto-miner", 20)  # not in the allowlist

examples/cloud/cases/remove_cap_fail.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy, remove_spend_cap

import clauz3


@clauz3.guarantee(cloud.never_remove_caps())
def main() -> None:
    deploy("api", 50)
    remove_spend_cap("api")
    deploy("api", 50)  # restored, but the cap was still removed meanwhile

examples/cloud/cases/total_caps_fail.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy

import clauz3


@clauz3.guarantee(cloud.cap_at_most(50))
@clauz3.guarantee(cloud.total_caps_at_most(150))
def main() -> None:
    # Each service's cap is within the per-service bound; together they are not.
    deploy("api", 50)
    deploy("worker", 50)
    deploy("scheduler", 50)
    deploy("cron", 50)

examples/cloud/cases/total_caps_pass.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy

import clauz3


@clauz3.guarantee(cloud.cap_at_most(50))
@clauz3.guarantee(cloud.total_caps_at_most(150))
def main() -> None:
    deploy("api", 50)
    deploy("worker", 50)
    deploy("scheduler", 50)

examples/cloud/cases/zero_cap_precondition_fail.py

# ruff: noqa: F821
from tools.cloud.trusted import contracts as cloud
from tools.cloud.trusted.effects import deploy

import clauz3


@clauz3.guarantee(cloud.cap_at_most(100))
def main() -> None:
    deploy("api", 0)  # refutes deploy's own precondition, not the guarantee