Run the spending-limit proof
===========================

This example checks a mathematical integer model with Z3 4.15.4.
It does not prove the JavaScript on the website or a production payment system.

These commands target macOS or Linux. Requirements: Git, Python 3.11 or later,
Python venv support, and an internet connection for setup. On Debian or Ubuntu,
install the python3-venv package if creating the environment reports that
ensurepip is unavailable.
No cloud credentials or paid services are needed. After setup, checks run offline.

1. Download the repository:

   git clone https://github.com/pb3975/proof-driven-development.git
   cd proof-driven-development

2. Create an isolated Python environment:

   python3 -m venv .venv

3. Install the pinned solver:

   .venv/bin/python -m pip install z3-solver==4.15.4.0

4. Activate the environment:

   . .venv/bin/activate

5. Run the checks:

   python3 site/examples/check-proof.py

Expected output:

   PASS correct rule: unsat
   PASS buggy rule: sat
   Counterexample: spent=..., amount=..., limit=...
   The contract allows the payment. The buggy rule rejects it.

The exact counterexample can vary. It must satisfy spent + amount = limit.
For example, spent=40, amount=60, limit=100 exposes the same bug.

If you downloaded the three raw files instead, keep correct.smt2, buggy.smt2,
and check-proof.py in one directory. Run python3 check-proof.py there after
installing and activating the solver as above.

Read the model
--------------

Preconditions:
  - spent and limit are nonnegative mathematical integers.
  - amount is a positive mathematical integer.
  - spent does not exceed limit.

Contract:
  A payment is allowed if and only if amount <= limit - spent.

Correct rule:
  spent + amount <= limit

Buggy rule:
  spent + amount < limit

Each file asks whether the implementation can disagree with the contract.
For the correct rule, Z3 returns unsat: the negated claim is unsatisfiable.
There is no disagreeing input in this model, under these preconditions.
For the bug, Z3 returns sat: a disagreeing input exists. Z3 prints one.
This catches a completeness failure: rejecting a valid boundary payment.
It is not an overspending example.

Limits
------

The model has unbounded mathematical integers. It does not model machine
integer overflow, concurrent payments, database balances, persistence, external
services, or a full application. The browser accepts whole numbers up to
1,000,000 only; the formal model has no such upper bound.

The conclusion depends on the model, its preconditions, the encoded claim,
and the solver working as intended. An incorrect specification can prove the
wrong requirement. Review those artifacts before trusting the result.

Source and corrections:
https://github.com/pb3975/proof-driven-development