= FormalSW
:idprefix:
:idseparator: -
:sectanchors:
:sectlinks:
:sectnumlevels: 6
:sectnums:
:toc: macro
:toclevels: 6
:toc-title:
Formally prove properties of https://www.python.org/[Python] code with the https://lean-lang.org/[Lean] proof assistant.
toc::[]
== Install
Install the formalsw Python library:
----
pipx install formalsw
----
Install Elan, Lean's version manager. On Linux:
----
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
----
Installation details for other systems: https://github.com/leanprover/elan
Now test it on a hello world link:tests/py/range_sum.py[]:
----
formalsw tests/py/range_sum.py
----
and if all went well you should see a message:
----
All 5 checks passed
----
and exit status 0.
== Getting started
Consider the following two alternative implementations of the sum of integers 0 to n, one naive and one optimized:
tmp.py
[source,python]
----
def sum(n: int) -> int:
if n <= 0:
return 0
return (n * (n - 1)) // 2
def sum_naive(n: int) -> int:
total = 0
for i in range(n):
total += i
return total
----
and then suppose that your goal is to formally prove that:
* for every possible input both functions return the same output, i.e. that the functions are equivalent
* both functions always return an integer value. In particular they:
** don't throw exceptions
** don't loop forever, i.e. they halt in the sense of the https://en.wikipedia.org/wiki/Halting_problem[halting problem]
** don't have multithreading deadlocks or livelocks
Traditionally, the only way to test this would be to add some tests and hope to catch all the edge cases:
----
for i in [1, 2, 3, 10]:
assert sum(i) == sum_naive(i)
----
but you can never cover all possible input values like that.
This is exactly what formal verification allows you to do.
To specify that we all the above properties to hold, we can add some magic docstring lines with the magic `@formalsw` marker:
[source,python]
----
def sum(n: int) -> int:
"""
@formalsw: Equiv(sum_naive)
"""
if n <= 0:
return 0
return (n * (n - 1)) // 2
def sum_naive(n: int) -> int:
"""
@formalsw: Returns
@formalsw: ReturnType
"""
total = 0
for i in range(n):
total += i
return total
----
Here we are specifying:
* for `sum_naive`
** `@formalsw: Returns`: the function always halts, no deadlocks, does not throw. See: <<Returns>>.
** `@formalsw: ReturnType`: it returns an `int` as specified in its docstring `-> int`. See: <<ReturnType>>.
* for `sum`:
** `@formalsw: @formalsw: Equiv(sum_naive)`: this function is equivalent to `sum_naive`, i.e. it has the same outcome for every input. Same outcome means that if one return an `int` the other also returns an `int`. See: <<Equiv>>.
After this is specified, if you run:
----
formalsw tmp.py
----
it blows up with:
----
error: tmp.py:3: missing proof file tmp.py.lean for `@formalsw: Equiv(sum_naive)`
----
which is good because haven't proven what we said we wanted to prove yet!
To create the required proofs, we must create a tmp.py.lean file containing the required theorems. The stubs can be generated automatically with:
----
formalsw --stub tmp.py > tmp.py.lean
----
it generates a file like this:
[source,lean]
----
import «.formalsw».«tmp.py.ast»
import FormalSW
open FormalSW.PyAst
namespace tmp
theorem sum.«Equiv(sum_naive)» :
FormalSW.Property.Function.Equiv TmpAst.module "sum" "sum_naive"
:= by
sorry
theorem sum_naive.«Returns» :
let _this_module := TmpAst.module;
let this_function := fun (input_0 : Int) => FormalSW.PyAst.scalarFunction TmpAst.module "sum_naive" [.int input_0];
∀ (n : Int),
Returns(this_function(n))
:= by
sorry
theorem sum_naive.«ReturnType» :
FormalSW.Property.Function.ReturnType TmpAst.module "sum_naive"
:= by
sorry
end tmp
----
Don't worry about understand it all. The important thing to note is how this file contains precise mathematical Lean statements of the things that we need to be proven: `Equiv`, and `Returns` and `ReturnType`.
And now if we try again:
----
formalsw tmp.py
----
this time it fails with:
----
proof check failed for tmp.py
Complete tmp.py.lean; remove any `sorry`; and make sure it compiles before checking requested proof obligations.
Expected proof obligations:
tmp.sum.«Equiv(sum_naive)» :
FormalSW.Property.Function.Equiv TmpAst.module "sum" "sum_naive"
tmp.sum_naive.«Returns» :
let _this_module := TmpAst.module;
let this_function := fun (input_0 : Int) => FormalSW.PyAst.scalarFunction TmpAst.module "sum_naive" [.int input_0];
∀ (n : Int),
Returns(this_function(n))
tmp.sum_naive.«ReturnType» :
FormalSW.Property.Function.ReturnType TmpAst.module "sum_naive"
Lean diagnostic:
tmp.py.lean:8:8: error: declaration uses `sorry`
tmp.py.lean:13:8: error: declaration uses `sorry`
tmp.py.lean:21:8: error: declaration uses `sorry`
error: tmp.py.lean:11: proof uses `sorry`
----
because we cheated with `sorry` in our proof stubs which, tells Lean to skip a proof.
So now the only thing left to do is to actually do those proofs proof!
Now, the final passing proof is an ungodly long file.
But I don't expect you to read and understand and even less write it.
The beauty of is is, and the entire reason for this project existing, of course, that you don't need to write that by yourself. You can just ask an LLM to do it for you!
You only need to understand the definition of properties that you care about in the comments of the source code.
Then you let the LLM loose, and so long as the LLM does not touch your .py source files during the proof step, only the .lean ones, then our scripts and the Lean formal system ensures that the property is true.
Once the proof is complete, when you run:
----
formalsw tmp.py
----
there's no output, which means that all proofs were verified!
You can check this with the following example contained in-tree:
link:tests/py/range_sum.py[]
----
formalsw tests/py/range_sum.py
----
which has a proof at link:tests/py/range_sum.py.lean[].
=== Another example: concurrency and Python specifications with `py`
FormalSW has concurrency support built-in. Its usage is so clean and self-evident it brings a tear of joy to our eyes. Check this out.
link:tests/py/parallel_shared_counter.py[] contains a simple concurrent Python code example:
[source,python]
----
from concurrent.futures import ThreadPoolExecutor
from threading import Lock
from time import sleep
def increment_unsafe(counter: list[int], mutex: Lock) -> None:
"""Increment using an unprotected read-modify-write operation.
@formalsw: Returns
@formalsw: theorem loses_an_update :
∃ (counter worker_count : PyValue),
py("valid_trial_input(counter, worker_count)") ∧
Throws(py("run_trial(this_function, counter, worker_count)"))
"""
snapshot = counter[0]
sleep(0)
counter[0] = snapshot + 1
def increment_safe(counter: list[int], mutex: Lock) -> None:
"""Hold the shared mutex for the whole read-modify-write operation.
@formalsw: Returns
@formalsw: theorem preserves_updates :
∀ (counter worker_count : PyValue),
py("valid_trial_input(counter, worker_count)") →
Returns(py("run_trial(this_function, counter, worker_count)"))
"""
mutex.acquire()
snapshot = counter[0]
sleep(0)
counter[0] = snapshot + 1
mutex.release()
def valid_trial_input(counter, worker_count):
return (
type(counter) == list
and len(counter) > 0
and all(type(item) == int for item in counter)
and type(worker_count) == int
and worker_count >= 0
)
def run_trial(increment, counter: list[int], worker_count: int):
assert valid_trial_input(counter, worker_count), "invalid trial input"
before = counter.copy()
mutex = Lock()
with ThreadPoolExecutor(max_workers=max(1, worker_count)) as workers:
futures = [workers.submit(increment, counter, mutex) for _ in range(worker_count)]
# Propagate worker exceptions; joining alone would hide them.
for future in futures:
future.result()
assert counter[0] == before[0] + worker_count, "an increment was lost"
assert counter[1:] == before[1:], "another counter element changed"
----
Just looking at the Python code, we see that there are two versions of the same dumb increment function which increments the first value of a list:
* `increment_safe` is thread safe
* `increment_unsafe` isn't and might lose updates
And additionally, we also have some Python test code:
* `run_trial` would test both `increment_safe` and `increment_unsafe` for thread safety
* `valid_trial_input` ensures that the input of `run_trial` is valid
Now let's try and understand how the FormalSW specifications above formally prove thread safety of `increment_safe`.
FormalSW natively understands that certain statements create multiple threads. In this example, when it sees:
[source,python]
----
with ThreadPoolExecutor(max_workers=max(1, worker_count)) as workers:
----
it *knows* that it will have to consider threading for some of the proofs. Conversely, it also knows that certain statements contain synchronization primitives, i.e.:
[source,python]
----
mutex = Lock()
mutex.acquire()
mutex.release()
----
In this case, the simple <<Returns>> statements:
----
@formalsw: Returns
----
already formally imply that each function does not have deadlocks or livelocks. That's already a good bang for our buck isn't it!
Next, let's take a look at the theorem statement which states that `increment_safe` actually preserves each update due to it's synchronization:
----
@formalsw: theorem preserves_updates :
∀ (counter worker_count : PyValue),
py("valid_trial_input(counter, worker_count)") →
Returns(py("run_trial(this_function, counter, worker_count)"))
----
== Specification language
The specification language is how you specify the properties of the program which must be proven.
Specifications are written as markers inside Python docstrings in lines starting with:
----
@formalsw
----
There are two types of ways to write the specification:
* <<dsl>>: what most people will use. Easy to learn and obvious. Gets translated to an equivalent Lean long form behind the scenes.
* <<raw-lean-specification>>. Harder to learn but more general than the DSL.
=== DSL
The DSL specification is a magic custom and very simple language that allows specifying commonly used properties easily.
The DSL gets converted to corresponding Lean code behind the scenes.
Each construct below includes a raw Lean equivalent. `Returns`, `Halts`, `Equiv`, `EquivReturn`, and `ReturnType` quantify over every modeled argument value. `Throws` uses an existential input, while `Not` negates the whole proposition. The examples show explicit quantifiers; `./formalsw --stub file.py` prints the exact elaborated statement for a particular function, including its globals.
==== Py
`Py` executes ordinary Python to prepare the evaluation environment for subsequent annotations. The language tag describes the setup language, independently of the language of the source being specified. It is not an assertion or a proof obligation. The current source frontend is Python.
[source,python]
----
def solve(n: int) -> int:
"""
@formalsw: Py from reference import naive
@formalsw: Requires(n >= 0)
@formalsw: Equiv(naive)
"""
return n
----
For several statements, put an indented Python block after `Py`:
[source,python]
----
def solve(n: int) -> int:
"""
@formalsw: Py
import reference
naive = reference.naive
lower = sum([0, 0])
@formalsw: Requires(n >= lower)
@formalsw: Equiv(naive)
"""
return n
----
Setup runs once per source per checker invocation, including dependency discovery, and also runs with `--stub`. Statements execute in order; a later assignment does not change an earlier annotation. Module-docstring bindings are available to function docstrings, which each receive their own binding dictionary. Normal Python object sharing and import caching still apply. `__file__` is the source path and `__name__` is `"__formalsw_spec__"`. The checker does not execute the enclosing source program merely to load its annotations; explicit Python imports execute imported modules normally. Setup can run arbitrary Python, including I/O, and failures report the source marker.
`Equiv` and `EquivReturn` can select a Python source function through setup bindings, including module attributes and expressions that return functions. The checker resolves the selected function to a module-level source definition, checks that its code matches the file, and rechecks that source and its adjacent proof. Setup selects the definition to model; it does not replace formal execution with CPython calls. Closures, runtime-dependent or modified defaults, dynamically generated functions without a matching source definition, and sources outside the checking project are rejected. Scalar setup values can be captured in `Requires`; function inputs remain symbolic, and input-dependent expressions still need execution-model support. Raw Lean statements retain Lean name resolution.
For packages outside the source directory, configure search roots relative to the current checking project in `pyproject.toml`:
[source,toml]
----
[tool.formalsw]
python-path = ["data/py"]
----
These roots precede the source directory, project directory, and existing Python search path while setup executes. This allows proof-only imports without runtime imports or symlinks in the source program.
==== Requires
`Requires(predicate)` supplies a precondition for every property in the same function docstring, including raw Lean specifications. A module-level precondition also applies to its function specifications. It does not insert a Python assertion or change normal execution.
[source,python]
----
def countdown(n: int) -> int:
"""
@formalsw: Requires(n >= 0)
@formalsw: Returns
"""
if n == 0:
return 0
return countdown(n - 1)
----
A predicate is parsed as an ordinary Python expression, including calls to Python helpers, and checked against the same execution model used for programs. Helpers may use supported branches, loops, and recursion. There is no separate arithmetic-only predicate language. Constructs without execution semantics are reported as unsupported, including in unused branches; they cannot be hidden behind a false precondition. Predicates currently use scalar inputs and module-local helpers; imported calls, heap objects, and global-state predicates still require interpreter support.
The domain consists of inputs on which the expression finishes with exactly Boolean `True`. A truthy integer or string is not `True`; an exception or nontermination does not establish the precondition. `Calls.Condition` records this finite Python execution, and `Evaluates.condition_iff` connects an evaluated result to the domain. The source AST module exposes each predicate as `requires_<function>_<index>`, so editing it changes the checked obligation. For the example, the guard is provably equivalent to `n ≥ 0`.
`Returns`, `Halts`, `ReturnType`, `Equiv`, and `EquivReturn` are required on inputs satisfying all preconditions. `Throws` needs a witness inside that domain. `Not` negates the whole guarded short obligation, so `Not Throws` excludes exceptions on valid inputs. Multiple preconditions apply together; a precondition without any property is an error. `BigO` keeps its existing structural cost abstraction and is guarded as a whole proposition; preconditions do not change the classifier or substitute a different cost model.
Raw theorems receive the precondition after their input binders. Lean's parser also recognizes leading `∀` and `∃` binders: the guard is an implication for universally quantified inputs and a conjunction for existential witnesses. This preserves the distinction between an admissible witness and a vacuous implication. Explicit theorem parameters remain in scope. link:tests/py/requires.py[] and its adjacent proof cover helper calls, every scalar short property, raw statements, chained-comparison short circuiting, signed arithmetic, and exact Boolean results.
==== Returns
`Returns` means that every input in the modeled argument domain finishes successfully. This is the usual marker for a total function:
[source,python]
----
def sum_naive(n: int) -> int:
"""@formalsw: Returns"""
total = 0
for i in range(n):
total += i
return total
----
The generated obligation is named `sum_naive.«Returns»`. `Returns` implies <<halts,Halts>> and <<not,Not>> <<throws,Throws>>. `Not Throws` alone permits nontermination.
Its raw Lean equivalent is:
[source,lean]
----
∀ n : Int,
(scalarFunction RangeSumAst.module "sum_naive" [.int n]).Returns
----
For several arguments, quantify each one: a function `f(x: int, flag: bool)` uses `∀ (x : Int) (flag : Bool), (scalarFunction module "f" [.int x, .bool flag]).Returns`. A function with no arguments needs no argument quantifier.
Successful completion includes falling off the end, bare `return`, and `return None`; all three return Python `None`, represented by `Constant.none` in Lean.
This marker supports scalar `int`, `str`, and `bool` positional arguments (including multiple or no arguments), and bare-list calls to the exact supported merge-sort implementation. Requirements involving unsupported Python constructs are rejected before proof checking; see <<unsupported-python-constructs>>.
==== Halts
`Halts` means that every modeled input finishes, either normally or by raising an exception. For example, link:tests/py/throws.py[`reject_odd`] has both `Halts` and `Throws`: all inputs terminate, and some inputs raise.
For that function, the raw Lean equivalent is:
[source,lean]
----
∀ n : Int,
(scalarFunction ThrowsAst.module "reject_odd" [.int n]).Halts
----
The generated obligation is named `function.«Halts»`. It supports the same argument domains as <<returns,Returns>>. `Not` negates the whole obligation: for a function with arguments, `Not Halts` says that not all inputs halt. Use a raw universally quantified theorem to say that every input fails to halt.
For an individual call, <<raw-lean-throws,Throws>> implies <<raw-lean-halts,Halts>>. The DSL `Throws` quantifies existentially over inputs, while `Halts` and `Returns` quantify universally: a function-level `Throws` marker therefore does not imply a function-level `Halts` marker.
See link:tests/py/termination.py[] and link:tests/py/termination.py.lean[] for an infinite `while True` loop and a termination proof for subtraction-based Euclid. Euclid preserves positive operands while strictly decreasing `a + b` until they agree; the guards handle nonpositive inputs. Its proof covers arbitrarily many iterations. The infinite-loop proof supplies an invariant closed under execution steps.
==== BigO
`BigO` bounds the cost assigned by the current structural cost model using https://en.wikipedia.org/wiki/Big_O_notation[Big O notation]. This classifier is an abstraction of recognized source shapes, not a proof that execution terminates. Use `Returns` or `Halts` for termination.
It takes two inputs:
* arbitrary Lean expression
* optional definition of lean variables from python expressions
Example:
[source,python]
----
def merge_sort(values: list) -> list:
"""
@formalsw: BigO(n * (Nat.log2 n + 1), n = len(values))
"""
# ...
----
Here:
* `n` is a lean variable
* `len(values)` is a Python expression that maps the Python into the lean variable
Python arguments annotated as `int` are automatically available in Lean under the same name, e.g. we can write the following:
[source,python]
----
def sum_naive(n: int) -> int:
"""Sum of integers from 1 to n. Return 0 if n <= 0.
@formalsw: BigO(n)
"""
----
rather than the more tedious:
----
@formalsw: BigO(n, n = n)
----
The merge_sort example above requires `merge_sort.«BigO(n * (Nat.log2 n + 1), n = len(values))»` with type:
[source,lean]
----
FormalSW.Property.Function.BigO
SortAst.module "merge_sort"
(FormalSW.PyAst.InputSize.listLength "values")
(fun n : Nat => n * (Nat.log2 n + 1))
----
Expanding that property gives the following raw Lean equivalent:
[source,lean]
----
∃ analysis,
SortAst.module.analyzeFunction "merge_sort" = some analysis ∧
analysis.inputSize = InputSize.listLength "values" ∧
∃ (c n₀ : Nat), ∀ n : Nat, n₀ ≤ n →
analysis.operations * analysis.growth.bound n ≤
c * (n * (Nat.log2 n + 1))
----
Here the universal variable is the input size used by the cost abstraction. The existential constants permit a multiplicative factor and a finite prefix of small inputs.
The analyzer checks that `values` is the actual `list` argument; changing the binding to another name does not produce a provable obligation. Integer arguments use their natural-number projection automatically. Because the current cost relation is one-dimensional, omitting the binding requires exactly one `int` argument.
Other valid bounds include `BigO(1)`, `BigO(n)`, `BigO(n * n, n = len(values))`, or a call to a user-defined Lean cost function. Because the bound is Lean rather than a second expression DSL, ordinary Lean functions and notation are available.
The cost model assigns cost 1 to every represented statement and expression operation. It then proves a constant multiple of the selected bound beyond some input-size threshold. Calls are unit-cost by default too; later standard-library models can replace that default with operation-specific complexity. The initial structural analyzer recognizes constant and iterative integer functions plus the recursive list-sort shapes demonstrated in link:tests/py/sort.py[].
==== Equiv
For proof-only dependencies, use `@formalsw: Py from reference import naive` followed by `@formalsw: Equiv(naive)`, optionally with a `Requires` input domain. Ordinary source-level imports also remain supported: `from reference import naive` (including aliases), or `from importlib import import_module` followed by `naive = import_module("reference.1").naive` for numeric filenames.
Formalsw resolves ordinary source-level imports statically; `Py` imports execute with Python as described above. Both compare the two generated AST executions on the same arguments and check the reference source and adjacent proof before the solver. `--stub` includes the reference proof import. The static source-import resolver rejects rebinding, missing sources or proofs, packages with executable initialization, and imports outside the current project. Its module lookup uses the source directory and then the current project directory; relative from-imports are also supported. This feature identifies scalar contract references with matching parameter types and no global state.
Ordinary calls to local helpers imported with `from module import function` also work in the scalar call interpreter, including relative imports and aliases. The linker appends the helper's source definitions to the generated module and inserts a forwarding function for an alias. Helper specifications are checked in their own source namespace; they are not duplicated as caller obligations. Dependencies are rechecked before the caller, and `--stub` imports their proofs. `Calls.Extends.prepend` and `ReturnsValue.extend` let a caller reuse a proved helper result while proving that linking preserves its execution. link:tests/py/linked_calls.py[] demonstrates this for every integer input.
The current linker requires disjoint module bindings and rejects cycles, rebinding, and unsupported helper bodies. It checks each helper in its own module before linking, so an unresolved helper name cannot accidentally refer to a caller definition. This is a static source transformation; ordinary imports are not executed by the linker. Source files with neither specifications nor an adjacent proof do not trigger linking when encountered on their own.
`Equiv` states that two functions have identical evaluation results for every input, i.e. that either:
* both functions return the same value if they return
* both functions throw the same exception if they throw
Example:
[source,python]
----
def sum(n: int) -> int:
"""Optimized version of sum_naive.
@formalsw: Equiv(sum_naive)
"""
if n <= 0:
return 0
return (n * (n - 1)) // 2
def sum_naive(n: int) -> int:
"""Sum of integers from 0 through n - 1. Return 0 if n <= 0.
@formalsw: Returns
"""
total = 0
for i in range(n):
total += i
return total
----
This marker requires `sum.«Equiv(sum_naive)»` with type:
[source,lean]
----
FormalSW.Property.Function.Equiv TmpAst.module "sum" "sum_naive"
----
For unary integer functions, `Equiv` now compares actual execution outcomes for every input:
[source,lean]
----
∀ n : Int,
(scalarFunction TmpAst.module "sum" [.int n]).Equiv
(scalarFunction TmpAst.module "sum_naive" [.int n])
----
`Execution.Equiv` says that each finite outcome is produced on one side exactly when it is produced on the other. An outcome is `.ok value` or `.error exception`; exceptions include their class name and evaluated positional arguments. It preserves `Returns` and `Halts` through the proved lemmas `Execution.Equiv.returns_iff` and `Execution.Equiv.halts_iff`. Thus the `sum` demo needs no duplicate `Returns` marker: its proof transfers the reference implementation's `Returns`. The exception demo similarly transfers `Halts`.
An equivalence proof by itself does not establish termination: two infinite computations may be equivalent. Requirements depending on unsupported Python constructs are rejected before proof checking, including negated equivalence requirements.
The existing list `Equiv` and `EquivReturn` demos still use the older abstract sorting model. Their canonical-result proofs do not establish termination of arbitrary Python comparison methods and do not transfer the new execution contracts. The raw merge-sort termination theorem below uses the execution model directly. List `ReturnType` also retains its older abstract evaluator.
===== Comparing object state
Python's `==` can run a user-defined `__eq__`; it need not compare stored attributes, and it can raise or loop forever. Stored-state equivalence has a separate executable Python definition in link:lang/py/graph_equivalence.py[]: `same_snapshot`. Lean parses that actual source and executes its AST using link:lang/py/FormalSW/DataRuntime.lean[]. There is no separate Lean implementation of the graph comparison algorithm, source fingerprint, or recognition of a particular function body. Changes to the Python definition change the interpreted computation; unsupported syntax anywhere in it produces a build error, including in unreachable branches.
The Python interface is link:lang/py/object_snapshot.py[]:
[source,python]
----
from lang.py.object_snapshot import equivalent, equivalent_roots
class Node:
pass
left, right = Node(), Node()
left.next, right.next = left, right
assert equivalent(left, right) # Same cyclic structure, different allocations.
shared = []
assert not equivalent([shared, shared], [[], []])
assert not equivalent(1, True) # Exact scalar types matter.
----
The comparator matches runtime types, scalar values, stored fields, container order, cycles, and sharing through a one-to-one mapping of reachable references. Unreachable objects are ignored. Lists and tuples preserve position; dictionaries preserve insertion order, including their key/value edges. Instance dictionaries preserve field order as well as names and values. Class identity matters even when two classes have the same name. User equality and getters are never invoked. Scalar identity and numeric `id()` values are outside this observation: freshly allocated containers and instances may be renamed consistently.
Compare all observable roots together when specifying function equivalence: the result, caller-owned inputs, and relevant supported global state. Comparing only results would miss whether a function returned its input or a copy:
[source,python]
----
input_left, input_right, copied_result = [1], [1], [1]
assert equivalent(input_left, copied_result)
assert not equivalent_roots(
[input_left, input_left], [copied_result, input_right]
)
----
Root positions establish the correspondence between input objects and preserve aliases between inputs and outputs. State snapshots must be taken while the observed objects are stable; this adapter does not synchronize with concurrent mutations. Class identifiers are process-local stable tokens, with classes retained to prevent identity reuse. Snapshots from separate processes need an explicitly shared type-identity table before comparison.
The current adapter supports exact `int`, `bool`, `str`, and `None`, exact `list`, `tuple`, and `dict`, and ordinary instances with a standard instance dictionary and no inherited user class. It rejects slots, custom attribute access, properties and other non-method descriptors, and unsupported builtin objects with a clear `TypeError`. Classes and their behavior are assumed fixed. This is equivalence of the captured stored state, not a promise about every Python observation: I/O, external resources, changing class attributes, weak references, allocation addresses, and finalizers are not captured.
The snapshot adapter is an explicit boundary, not a formally verified interpretation of CPython's heap. Lean consumes the corresponding finite graph encoding; the cross-language tests exercise the adapter and interpreter together. `Graph.Equivalent` requires the interpreted Python comparator to return `True`; `Graph.Equiv` uses this relation for successful execution results and still matches exceptions and termination. Both are available in raw Lean specifications. This does not silently widen the existing short-form `Equiv` frontend: its scalar and sorting backends still have the restrictions described above, and arbitrary object-manipulating Python functions are not yet executable by them. Exception matching still uses the existing modeled exception class and positional arguments.
Integers remain cheap. The Python definition checks scalar types and immediately compares scalar values, without constructing a graph. The kernel-checked theorem `Graph.equivalent_int` proves, for arbitrary integers, that this interpreted branch is equivalent to `a = b`, and is registered with `simp`. Thus proofs can use integer equality without repeatedly interpreting the comparator. The more general `Graph.equivalent_scalar` covers every modeled scalar, and `Graph.scalar_equiv_iff` proves that the existing scalar `Execution.Equiv` check is exactly the same as using the Python-defined relation. This avoids graph overhead; integer equality still has its usual cost with respect to integer size. The first graph implementation uses simple lists for its work queue and correspondence table, so large graphs can take quadratic work; a faster implementation would need to preserve the same relation.
See link:tests/py/object_equivalence.py[] for executable examples, link:tests/py/object_equivalence.lean[] for proofs of allocation renaming and detection of changed attributes and aliases, and link:tests/py/graph_equivalence_checks[] for Python/Lean comparisons and source-mutation tests. The examples do not yet prove graph isomorphism correctness or comparator termination for every well-formed heap.
==== EquivReturn
`EquivReturn(other)` states that whenever both functions return successfully
on the same modeled input, their return values are equal. Unlike `Equiv`, it
does not require their exception objects to agree:
[source,python]
----
def merge_sort_untyped(values: list) -> list:
"""
@formalsw: EquivReturn(quick_sort)
"""
# ...
----
For unary integer functions, a raw Lean equivalent of `EquivReturn(sum_naive)` on `sum` is:
[source,lean]
----
∀ (n : Int) (leftResult rightResult : Constant),
let left := scalarFunction RangeSumAst.module "sum" [.int n]
let right := scalarFunction RangeSumAst.module "sum_naive" [.int n]
Finishes left.step left.initial (.ok leftResult) →
Finishes right.step right.initial (.ok rightResult) →
leftResult = rightResult
----
For the bare-list example above, the raw Lean equivalent uses its older abstract evaluator:
[source,lean]
----
∀ (values : List Value) leftResult rightResult,
evalUnaryListFunctionOutcome SortAst.module "merge_sort_untyped" values = some (.ok leftResult) →
evalUnaryListFunctionOutcome SortAst.module "quick_sort" values = some (.ok rightResult) →
leftResult = rightResult
----
The implication is vacuously true on an input where either function throws.
This makes `EquivReturn` useful when successful results agree but exception
details or evaluation order differ.
==== Not
`Not` negates the complete DSL expression following it. For example, to state that a function does not <<throws,throw>> for any input:
my_not_example.py
[source,python]
----
def sum(n: int) -> int:
"""
@formalsw: Not Throws
"""
return n + 1
----
The marker above requires `sum.«Not Throws»`. `Not` can prefix any other DSL property recursively; for example, `Not Not Throws` has the usual double negation meaning.
The raw Lean equivalent is:
[source,lean]
----
¬ (∃ n : Int, (scalarFunction MyNotExampleAst.module "sum" [.int n]).Throws)
----
Equivalently, `∀ n : Int, ¬ (scalarFunction MyNotExampleAst.module "sum" [.int n]).Throws`. In contrast, `Not Returns` expands to `¬ (∀ n : Int, (scalarFunction module "sum" [.int n]).Returns)`: it does not claim that every input fails to return.
==== ReturnType
`ReturnType` states that every modeled invocation either throws an exception or returns a value matching the function's return annotation. For example:
[source,python]
----
def sum(n: int) -> int:
"""
@formalsw: ReturnType
"""
# ...
----
This marker requires `sum.«ReturnType»` with type:
[source,lean]
----
FormalSW.Property.Function.ReturnType TmpAst.module "sum"
----
For the supported `int -> int` case, this expands to:
[source,lean]
----
∀ n : Int,
let execution := scalarFunction TmpAst.module "sum" [.int n]
(∃ value : Int, Finishes execution.step execution.initial (.ok (.int value))) ∨
execution.Throws
----
A successful outcome must contain an `Int`; an exception outcome is also accepted because it has no return value. This property requires termination. A supported function returning the wrong type fails the property; a function containing unsupported Python constructs is rejected before proof checking. Unary `list -> list` functions are also supported by the structural list evaluator, with heterogeneous `int` and `str` inputs and exception-aware list outcomes. `list[int] -> list[int]` selects the homogeneous integer-list model.
==== Throws
`Throws` states that there is at least one input for which the function throws.
Example:
my_throws_example.py
[source,python]
----
def reject_odd(n: int) -> int:
"""
@formalsw: Throws
"""
if n % 2 != 0:
raise ValueError("odd input")
return n
----
This marker requires a theorem named `reject_odd.«Throws»` with type:
[source,lean]
----
FormalSW.Property.Function.Throws MyThrowsExampleAst.module "reject_odd"
----
which expands to:
[source,lean]
----
∃ n : Int,
(FormalSW.PyAst.scalarFunction ThrowsAst.module "reject_odd" [.int n]).Throws
----
Use `Not Throws` to state that no input throws. For a function named `sum`, this requires a theorem named `sum.«Not Throws»` with type:
[source,lean]
----
Not (FormalSW.Property.Function.Throws TmpAst.module "sum")
----
For a bare-list function, `Throws` instead provides a modeled runtime-value-list input and an exception produced by the list evaluator. The mixed input `[0, ""]` in link:tests/py/sort.py[] is one example.
=== Global state
Scalar module globals and mutable list globals are supported as additional function inputs. Python's symbol table determines the global names, so a local assignment anywhere in a function shadows the module binding unless Python declares it `global`. This supports reads without a `global` statement and assignments with one:
[source,python]
----
offset: int = 10
total: int = 0
def add_offset(n: int) -> int:
"""@formalsw: Returns"""
return n + offset
def advance(n: int) -> int:
"""@formalsw: Returns"""
global total
total += n
return total
----
`add_offset` has this raw Lean obligation:
[source,lean]
----
∀ (n offset : Int),
(scalarFunctionWithGlobals GlobalsAst.module "add_offset"
[.int n] [("offset", .int offset)]).Returns
----
The theorem covers every integer `offset`, not just its initial value of `10`. The domain comes from a module-level scalar declaration: `int`, `str`, and `bool` annotations are supported, or the type can be inferred from a scalar literal such as `offset = 10`. A declaration may use a matching literal initializer, an explicit supported type annotation without an initializer, or an alias to another supported module declaration. Module initialization is not executed by this call model; the theorem describes calls entered with values in those domains. An explicit raw hypothesis can restrict the entry state when that is intended.
In raw function-level specifications, `this_function` captures the quantified globals while retaining the Python parameter list. For example, `@formalsw: theorem returns_with_offset (n offset : Int) : Returns(this_function(n))` in `add_offset` expands to the same stateful call. Unbound globals needed by `this_function` are quantified automatically, even if their names are absent from the theorem body.
`advance` returns a completion containing both its Python result and the final `total`. If it raises after assigning `total`, the exception completion still contains that update. `Equiv` compares both outcomes and final global state; equal return values or equal exceptions alone are insufficient. Both functions receive the same initial state covering the union of their global dependencies, and untouched globals are preserved. `EquivReturn` compares the returned value and final state whenever both calls return successfully. `Returns`, `Halts`, and `ReturnType` quantify universally over argument and global values; `Throws` uses an existential assignment to both.
See link:tests/py/globals.py[] and link:tests/py/globals.py.lean[] for proofs over arbitrary integers, including a counterexample where omitting a global update changes equivalence and another where throwing before versus after an update differs. The examples also cover string and Boolean globals and local shadowing.
Mutable list globals use a shared heap, so a local alias, another global, a function argument, and a returned value can all refer to the same object:
[source,python]
----
items: list[int] = []
alias = items
def push(n: int) -> None:
"""@formalsw: Returns"""
items.append(n)
def push_via_alias(n: int) -> None:
"""@formalsw: Equiv(push)"""
local = items
local.append(n)
def replace(n: int) -> None:
"""@formalsw: Not Equiv(push)"""
global items
items = items + [n]
----
`push` mutates the existing object, so every alias sees the appended value. `replace` binds the global to a new list; callers retaining the original list still see its previous contents. Both finish with the same list elements in `items`, but their observable effects differ. Mutation does not need a `global` declaration; rebinding does.
The raw obligation for `push` is:
[source,lean]
----
∀ (heap : Mutable.Heap) (n : Int) (items : Nat),
heap.Valid →
Mutable.Value.HasType heap (.ref items) "list[int]" →
(Mutable.function MutableGlobalsAst.module "push"
[.scalar (.int n)] [("items", .ref items)] heap).Returns
----
This quantifies over every valid entry heap and list address, including empty lists. List arguments and all required list globals use addresses in that same heap; their addresses can coincide. Initializers establish input domains without fixing list contents or assuming distinct objects. `list[int]`, `list[str]`, and `list[bool]` are supported; a nonempty homogeneous literal can supply the element type, and an empty initializer needs an annotation. An annotation describes the entry state; subsequent supported scalar writes may change element types.
The heap interpreter supports list literals, scalar indexed reads and writes (including negative indices), `append`, concatenation, repetition, `len`, name assignment, name or indexed augmented assignment, scalar expressions, `if`, `while`, message-free `assert`, `return`, and ordinary builtin `raise` with scalar arguments (special constructors such as `OSError` are rejected). `list += string` appends its characters in place. Indexed augmented assignment evaluates the target once, reads before the right-hand side, and preserves Python's write order even if the right-hand side mutates the list. List operations on a function argument share the same semantics as operations on a global. Ordinary calls, slicing, other list methods, recursive list comparisons, nested mutable containers, dictionary/object globals, imported module attributes, closures (`nonlocal`), deletion of globals, and globals in the parallel or quotation backends remain unsupported. The scalar global model does not execute ordinary function calls either. These dependencies produce unsupported-construct diagnostics rather than being silently omitted. `BigO` currently rejects functions depending on globals because its single input-size abstraction does not account for additional state inputs. Explicit legacy `Property.Function`/`scalarFunction` specifications cannot discard a function's globals; use the short DSL, `scalarFunctionWithGlobals` for scalar state, or `Mutable.function` for shared list state.
Mutable completions retain global bindings and the heap on both return and exception. `Equiv` compares the outcome and the rooted final object graph, using the interpreted Python `same_snapshot` comparison; exactly identical completions are an immediate fast path. Roots include every entry object (a caller might retain it), final globals, and a successful return value. This preserves caller-visible aliases even after rebinding and permits renaming newly allocated objects and ignoring unreachable temporary allocations. Entry heap addresses keep their order as caller anchors. `EquivReturn` compares this same observable state whenever both executions return. Implicit builtin exception messages remain abstracted, as in the scalar interpreter; explicit supported exception arguments are retained.
Raw `this_function` specifications for mutable globals capture an additional `heap : Mutable.Heap` input and the global addresses. Referenced typed list arguments are addresses too. As with other raw specifications, write the desired heap-validity and input-type hypotheses explicitly; the short DSL supplies them automatically. See link:tests/py/mutable_globals.py[] and link:tests/py/mutable_globals.py.lean[] for arbitrary-heap proofs, argument/global aliasing, mutation versus rebinding, and mutation before an exception. link:tests/py/mutable_global_checks[] also compares the interpreter with real Python executions.
=== Raw Lean specification
If the specification starts with "theorem", then it is interpreted as an arbitrary Lean code to be proven.
Function-level raw theorems infer referenced Python arguments that the theorem does not bind explicitly. For example, `values` below receives the type `List FormalSW.PyAst.Value` from the bare `list` annotation:
[source,python]
----
def merge_sort_untyped(values: list) -> list:
"""
@formalsw: theorem returns_of_le_safe :
(∀ left ∈ values, ∀ right ∈ values, Returns(left <= right)) →
Returns(this_function(values))
"""
# ...
----
The enclosing function automatically prefixes an unqualified raw theorem name. This marker requires `tests.py.sort.merge_sort_untyped.returns_of_le_safe`, just as `Throws` requires `tests.py.sort.merge_sort_untyped.«Throws»`. An explicitly qualified name is used unchanged. Module-level raw theorems retain the file's proof namespace without a function prefix.
Arguments can also be bound explicitly, and hypotheses may be named, anonymous, or written as implications in ordinary Lean:
[source,python]
----
def f(n: int) -> int:
"""Identity function.
@formalsw: theorem returns_input (n : Int) :
n = n ∧ RawLeanAst.module.findFunctionBody "f" ≠ none
"""
return n
----
Continuation lines are included until a blank line or another marker. The example above requires `f.returns_input` inside the file-derived proof namespace. Raw theorem markers may also appear in a module docstring; module docstrings do not support the function-specific short forms.
The constructs below are available through `import FormalSW`. Lean parses the custom predicate and call syntax; state types and observation helpers are ordinary Lean definitions. Use ordinary Lean negation, such as `Not Throws(...)` or `¬ Throws(...)`.
[[raw-lean-this-module]]
==== _this_module
FormalSW supplies `_this_module` as the enclosing Python module's AST. Comparison syntax uses it to look up Python comparison methods, including in nested parenthesized expressions. The binding appears in generated stubs alongside `this_function`.
[[raw-lean-candeadlock]]
==== CanDeadlock
`CanDeadlock(py("run_retries(this_function, 1)"))` states that some finite schedule reaches a global deadlock: unfinished workers remain, and none can take a step. `CanDeadlock(Parallel(calls, heap))` is its explicit-call form. The `acquire_twice` example exhibits a non-reentrant self-deadlock; `lock_pair` exhibits the classic opposite-order two-lock deadlock in link:tests/py/parallel_liveness.py[]. A witness includes actual transitions, not a timeout.
[[raw-lean-candiverge]]
==== CanDiverge
`CanDiverge(py("run_retries(this_function, 2)"))` states that some schedule executes infinitely many steps. `CanDiverge(Parallel(calls, heap))` is its explicit-call form. A proof supplies a set of configurations that contains the initial configuration and always admits a next configuration within the set. The set may be infinite: the tests include a worker whose integer keeps increasing.
Livelock is an infinite execution without the desired application progress. The `retry_forever` example repeatedly acquires and releases a mutex without completing any work. Its proof repeats a schedule that advances both workers. `CanDiverge` establishes infinite execution; specifying a separate application progress property would be necessary to classify arbitrary useful infinite computations as livelock.
[[raw-lean-can-return]]
==== CanReturn
`CanReturn(run, state)` states that some modeled schedule finishes with exactly that shared state. For the counter, a final array containing one proves a lost update. The state is the result of the concurrent run, not a worker's Python return value.
It does not say every schedule fails or assign a probability to failure. `ParallelRun.Ensures.of_canReturn` says that any reachable state must satisfy an established guarantee; a reachable corrupt state can therefore disprove a proposed invariant.
[[raw-lean-data]]
==== Data
`Data` is the read-only interpreter's value domain: Python scalars (`Constant`), nested lists, and supported builtin type objects. Lists in this interpreter cannot be mutated; programs build new lists with `+`. Cycles in observed Python objects are represented by explicit graph references, not by cyclic `Data` trees.
[[raw-lean-data-function]]
==== dataFunction
`dataFunction module name arguments` executes a function's actual AST on `Data` arguments. It supports local assignments, conditionals, while loops, scalar operations, list construction and indexing, and `len`/`type`. Other constructs are rejected by `python_data%`; operations on values outside the interpreter's supported domain yield an unsupported execution. Termination uses `Execution.Finishes` with no fuel limit.
[[raw-lean-deadlockfree]]
==== DeadlockFree
`DeadlockFree(py("run_retries(this_function, 2)"))` rules out reachable global deadlock. `DeadlockFree(Parallel(calls, heap))` uses explicit worker calls. This is weaker than `Halts`: an execution can always have another enabled step and still run forever. The semantic tests prove both `DeadlockFree` and `CanDiverge` for one such worker.
Global deadlock means every unfinished worker is blocked. A subset of workers can remain blocked while another runs forever; `DeadlockFree` alone does not exclude this, but `Halts` does. No fairness assumption is hidden in these predicates.
[[raw-lean-diverges]]
==== diverges
`diverges(this_function())` proves an infinite execution by supplying an invariant that contains the initial state and always permits another execution step. `Execution.diverges_not_halts` turns this proof into `Not Halts(this_function())`. See the `forever` example in link:tests/py/termination.py.lean[].
[[raw-lean-ensures]]
==== Ensures
`Ensures(run, postcondition)` requires every maximal modeled run to finish successfully with a shared state satisfying the postcondition. For example:
[source,lean]
----
Ensures(Parallel(List.replicate 2 (this_function [.ref 0, .lock 0]),
{ objects := [.array [.int 0]] }), fun state => state.item 0 0 = some (.int 2))
----
This checks the value at index 0 of shared array 0 after both workers finish. A linked-list specification can instead check relationships between fields throughout the heap. Deadlocks, exceptions, incomplete exploration, and empty outcome sets cannot satisfy this guarantee.
[[raw-lean-execution-equiv-by]]
==== Execution.EquivBy
`Execution.EquivBy relation left right` requires every finite outcome on either side to have a matching outcome on the other. Successful results must satisfy `relation`; exceptions must have the same modeled class and arguments. Its `returns_iff` and `halts_iff` lemmas transfer termination guarantees. `Execution.equivBy_eq_iff` proves that using ordinary equality recovers `Execution.Equiv`.
[[raw-lean-graph-compare]]
==== Graph.compare
`Graph.compare left right` executes `same_snapshot(left, right)` from link:lang/py/graph_equivalence.py[]. Its arguments are encoded snapshots (`Data`), and its result is an `Execution Data`. It does not call overridable Python object equality.
[[raw-lean-graph-edge]]
==== Graph.Edge
An edge is a typed scalar value (`.scalar`) or a reference to a node index (`.ref`). Node indices are local to each heap; comparison permits consistent renaming.
[[raw-lean-graph-equiv]]
==== Graph.Equiv
`Graph.Equiv left right` abbreviates `Execution.EquivBy Graph.Equivalent left right`. The executions must return snapshots containing all observable roots. It compares captured state while preserving the existing exception and termination requirements; it does not supply a heap interpreter for unsupported Python functions.
[[raw-lean-graph-equivalent]]
==== Graph.Equivalent
`Graph.Equivalent left right` states that the interpreted Python snapshot comparator terminates and returns `True`. It does not mean Python `left == right`. `Graph.equivalent_int` reduces this relation on integer snapshots to ordinary integer equality; `simp` uses the theorem automatically.
[[raw-lean-graph-heap]]
==== Graph.Heap
A finite observation consists of an ordered `roots` list and a `nodes` list. Include the result and externally observable input/global roots together to preserve their sharing. `heap.encode` produces the same nested-list format as the Python snapshot adapter. References must identify existing nodes, and node labels/edges must follow the adapter's layout; constructing this record alone does not prove those conditions. Unreachable nodes do not affect comparison.
[[raw-lean-graph-kind]]
==== Graph.Kind
A node's kind distinguishes lists, tuples, dictionaries, and instances with a runtime type identity. Both observations must use the same type-identity scheme. Object addresses may be renamed; type identities must agree.
[[raw-lean-graph-node]]
==== Graph.Node
Each node stores its `kind`, ordered field `labels`, and outgoing `edges`. Instances use one label per field; list/tuple positions and alternating dictionary key/value positions are implicit and use an empty labels list.
[[raw-lean-graph-observed-bool]]
==== Graph.observedBool
`Graph.observedBool (execution.observe fuel)` returns `some true` or `some false` only after a Boolean return. It returns `none` for unfinished execution, unsupported operations, exceptions, or other return values. `Graph.equivalent_of_observe` turns a `True` observation into a proof of equivalence; `Graph.not_equivalent_of_observe` uses an actual `False` return to disprove it. Exhausting fuel proves neither result.
[[raw-lean-halts]]
==== Halts
`Halts(this_function(n))` states that this particular call terminates, either normally or by raising an exception. `Halts(left < right)` states the same for a comparison.
The model in link:lang/py/FormalSW/Execution.lean[] and link:lang/py/FormalSW/Runtime.lean[] uses a deterministic transition system. Termination requires a finite derivation ending in a normal or exceptional outcome. Observation fuel only limits how long an observer runs; exhausting it produces `pending`, never a fabricated return.
For concurrent trials, `Halts(py("run_retries(this_function, 2)"))` requires every enabled schedule to finish the whole helper. It excludes both deadlock and infinite execution, including livelock. It permits assertions or workers to raise, provided the joined batch finishes. `Returns` adds successful execution and successful final assertions. `Halts` implies `DeadlockFree` and excludes `CanDiverge` in the general parallel model. Negating concurrent `Halts` disproves universal termination; it does not say that every schedule fails to finish.
`Not Halts(this_function(values))` states that a deterministic call does not terminate. link:tests/py/sort.py[`Looping.__le__`] and its checked proof show that sorting two such objects does not halt. Unsupported source constructs cause validation errors and cannot be used to satisfy this requirement.
[[raw-lean-mutable-call]]
==== Mutable.Call
A heap-backed call containing an execution of `Mutable.Completion`. Its `Returns`, `Halts`, `Throws`, and `Diverges` predicates inspect the Python outcome, not the internal completion wrapper. `Call.returns_iff_halts_not_throws` proves `Returns ↔ Halts ∧ ¬ Throws`; `Call.throws_halts` proves `Throws → Halts`.
[[raw-lean-mutable-call-equiv]]
==== Mutable.Call.Equiv
`left.Equiv right` requires each finite completion on either side to have a matching `Mutable.Completion.Equivalent` completion on the other. Final global state and caller-visible mutations matter on exceptional exits too. `Call.equiv_of_finishes` proves equivalence from two matching completions.
[[raw-lean-mutable-call-equiv-return]]
==== Mutable.Call.EquivReturn
`left.EquivReturn right` compares successful completions using `Mutable.Completion.Equivalent` whenever both calls return. It does not prove termination. `Call.Equiv.equivReturn` derives it from `Equiv`.
[[raw-lean-mutable-call-finishes]]
==== Mutable.Call.Finishes
`call.Finishes completion` is a finite execution ending with that Python outcome, global bindings, and heap. `Call.finishes_of_observe` turns an actual completed observation into a proof; exhausting observation fuel is insufficient.
[[raw-lean-mutable-call-return-type]]
==== Mutable.Call.ReturnType
`call.ReturnType kind` means that the call throws or returns a value satisfying `Mutable.Value.HasType` in its final heap. For example, `"list[int]"` checks the returned reference and the exact scalar types of its elements.
[[raw-lean-mutable-completion]]
==== Mutable.Completion
A record with `outcome : Except ExceptionObject Mutable.Value`, `globals : Mutable.Globals`, `heap : Mutable.Heap`, and `anchors : Nat`. The first `anchors` heap objects existed at entry and remain observable even if a global stops referring to them.
[[raw-lean-mutable-completion-equivalent]]
==== Mutable.Completion.Equivalent
Two completions match if they are identical, or if their anchor counts, global-name order, and outcome kinds/exception objects agree and `Graph.Equivalent` holds between their snapshots. The snapshot comparison runs the Python definition of object-graph equivalence.
[[raw-lean-mutable-completion-snapshot]]
==== Mutable.Completion.snapshot
Encode the final graph as `Data` for the Python comparator. Ordered roots are entry objects, final global values, and the return value on success. Fresh unreachable objects are ignored by graph comparison; aliases between roots are preserved.
[[raw-lean-mutable-function]]
==== Mutable.function
`Mutable.function module "name" arguments globals heap` executes the actual translated Python function body with shared references. It respects whole-function local/global scope. Supplied globals unused by the body remain observable and unchanged, which allows comparing functions with different global dependencies in the same world.
[[raw-lean-mutable-globals]]
==== Mutable.Globals
A list of `(String × Mutable.Value)` module bindings. A binding such as `("items", .ref 0)` refers to object zero in the shared heap. Rebinding changes this entry; mutation changes the object.
[[raw-lean-mutable-heap]]
==== Mutable.Heap
A list of list objects, indexed by reference addresses. For example, `[[.scalar (.int 1)]]` contains one list. Arguments, globals, locals, and results share these addresses. The representation can express cycles; the current source validator restricts accessible containers to flat scalar lists.
[[raw-lean-mutable-heap-valid]]
==== Mutable.Heap.Valid
`heap.Valid` requires every reference stored in the heap to address an existing object. It does not assert that different bindings refer to different objects.
[[raw-lean-mutable-value]]
==== Mutable.Value
Either `.scalar constant` or `.ref address`. Constants use the existing `Constant` representation; references identify mutable list objects.
[[raw-lean-mutable-value-has-type]]
==== Mutable.Value.HasType
`value.HasType heap kind` is the entry-domain predicate used by the mutable-state DSL. Scalar kinds are `"int"`, `"str"`, `"bool"`, and `"None"`; list kinds check that a reference exists and, for `"list[int]"`, `"list[str]"`, or `"list[bool]"`, every element has that exact scalar type. Empty lists satisfy each scalar element domain.
[[raw-lean-mutex-ensures]]
==== Mutex.Ensures
An inductive successful-execution predicate for arbitrary finite batches protected by a common mutex. It accounts for every next lock owner and advances each body operation through the ordinary parallel interpreter. Workers waiting at acquire cannot execute while another worker owns the mutex. Source extraction checks the complete acquire/body/release region and prevents reassignment of the mutex local.
[[raw-lean-mutex-invariant]]
==== Mutex.invariant
The generic induction rule for `Mutex.Ensures`. Prove that the invariant holds initially, is preserved by any selected worker, and implies the postcondition when no workers remain. The counter proof relates the current value plus the number of pending increments to the required final value, preserving the remaining list contents throughout.
[[raw-lean-parallel]]
==== Parallel
`Parallel(calls, initialState)` explores the interleavings of an explicit list of worker calls over one shared heap. Calls may invoke different functions with different argument lists. There is no required parameter count, parameter order, shared-cell layout, or mutex argument. link:tests/py/parallel_calls.py[] demonstrates workers with one and three arguments, nonzero list indices, and no mutex parameter.
A call such as `this_function [.ref 0, .ref 2, .lock 0]` passes two object references and a mutex reference. Repeating an address shares the same object; repeating a lock identity shares the same mutex. Different mutex identities are independent: locking two different mutexes does not protect their shared data.
The interpreter supports assignments of local scalar values and references, separate reads/writes of list items and plain object fields, integer arithmetic, scalar comparisons, `not`, `if`, `while` (including `else`), mutex acquire/release, `sleep(0)`, and `pass`. Each loop guard is a scheduling step. Worker parameters use scalar, typed scalar-list, plain-class, or `Lock` annotations. Plain classes may initialize data fields in `__init__`; inheritance, descriptors, general method calls, allocation during a worker, `break`, and `continue` need further model support. Split compound shared expressions and guards into individual reads and writes so scheduling points are explicit. Primitive imports and all source branches are validated, including unreachable code.
The transition system chooses any enabled worker at each step. A blocked acquire has no transition; a finished worker has none either. A batch finishes only after every worker finishes, including when another worker has already raised: Python's executor context manager still waits during shutdown. Mutexes are non-reentrant, and releasing an unlocked mutex raises `RuntimeError`. As with Python's `Lock`, release does not require ownership.
`Halts(Parallel(calls, initialState))` requires completion on every enabled schedule. `Returns` also excludes exceptions. `Throws` exhibits one completed exceptional schedule. `ParallelRun.returns_iff_halts_not_throws` proves `Returns ↔ Halts ∧ Not Throws` for these batches; existential `Throws` does not imply universal `Halts`.
The model uses sequentially consistent atomic field/item accesses and mutex operations. There are no idle scheduler steps or fairness assumptions: an infinite schedule that continually runs some workers while neglecting another enabled worker counts against `Halts`. Total suspension by the operating system, signals, resource exhaustion, and external processes changing the modeled heap are outside the model. The livelock witness in link:tests/py/parallel_liveness.py[] repeatedly schedules both workers, so its infinite execution does not depend on starvation.
The finite explorer is an observation tool. Its default budget is the initial total operation count, sufficient for straight-line workers but potentially insufficient for branches and loops. An exhausted budget means incomplete exploration, never a proof of deadlock or divergence. Unbounded predicates use the transition system itself. The tests prove termination of a countdown even though its default observation is incomplete.
[[raw-lean-parallelconfig]]
==== ParallelConfig
A concurrent configuration contains the shared heap, each worker's remaining operations and locals, and accumulated failures. Python exceptions stop their worker while the remaining workers continue. Internal model failures cannot be hidden behind an earlier Python exception. The low-level observer reports the first encountered Python exception when several workers fail; quoted `Throws` claims exceptional completion without specifying which exception is re-raised.
[[raw-lean-parallelconfig-candiverge]]
==== ParallelConfig.CanDiverge
The infinite-execution witness underlying `CanDiverge`. Its invariant contains the starting configuration and supplies at least one enabled successor from every member. `CanDiverge.before` and `CanDiverge.of_reaches` prepend a step or a finite path.
[[raw-lean-parallelconfig-deadlocked]]
==== ParallelConfig.Deadlocked
An unfinished configuration with no enabled successor. Successfully completed configurations are not deadlocked.
[[raw-lean-parallelconfig-follow]]
==== ParallelConfig.follow
`ParallelConfig.follow initial schedule` executes a finite list of worker indices and returns the resulting configuration, even if unfinished. It rejects blocked or completed worker selections. `reaches_of_follow` turns a successful replay into a reachability proof. `canDiverge_of_follow` requires a nonempty schedule that returns to exactly its initial configuration, proving that this cycle can repeat forever.
[[raw-lean-parallelconfig-mustfinish]]
==== ParallelConfig.MustFinish
An inductive proof that every enabled schedule finishes with an accepted outcome. A completed configuration must satisfy the acceptance predicate; an unfinished one must have a successor, and every successor must itself have a termination proof. This rules out both stuck configurations and infinite executions. `mustFinish_of_explore` converts a completely explored finite tree into such a proof when the acceptance predicate rejects deadlock and incomplete exploration.
[[raw-lean-parallelconfig-reaches]]
==== ParallelConfig.Reaches
Finite reachability using zero or more enabled transitions. `Reaches.invariant` transports an invariant along such a path. Deadlock and exceptional-completion proofs use finite reachability witnesses.
[[raw-lean-parallel-replay]]
==== parallelReplay
`parallelReplay initialState schedule` executes a concrete schedule, where the initial configuration contains the shared heap and initialized workers. Worker indices start at zero. Each index selects that worker's next operation. Selecting a blocked worker makes the schedule invalid; stopping before all workers finish is incomplete.
The counter's schedule `[0, 1, 0, 1, 0, 1]` makes both workers read zero, both yield, and both write one. The doubly linked list's proof gives a longer schedule where different workers win the forward and backward pointer writes.
[[raw-lean-parallelrun]]
==== ParallelRun
An explicit list of optional compiled workers together with the initial shared heap. It retains the program, rather than only a finite list of observations. `config` initializes its transition system; a missing compiled worker prevents successful liveness claims. Its `Returns`, `Halts`, `Throws`, `CanDeadlock`, `CanDiverge`, and `DeadlockFree` properties are exposed by the corresponding specification constructs.
[[raw-lean-parallelrun-ensures-returns]]
==== ParallelRun.Ensures.returns
Converts an established finite `Ensures` guarantee into unbounded `Returns`. Any deadlock, exception, unsupported operation, or incomplete branch prevents the premise from holding.
[[raw-lean-parallelrun-eventually]]
==== ParallelRun.Eventually
`run.Eventually accept` requires successful initialization and a `ParallelConfig.MustFinish accept` proof. It expresses total correctness for a general concurrent batch. `Eventually.of_explore` accepts an explicit observation budget when a complete finite exploration suffices; the resulting proposition has no fuel bound.
[[raw-lean-parallelrun-outcomes]]
==== ParallelRun.outcomes
A bounded observation of the run. Straight-line workers need at most their initial total operation count; the same default budget may be insufficient for branching or looping workers. `.error .incomplete` is an observation limit, not a Python exception and not divergence. Increasing fuel can discover completion; an unbounded theorem can also prove it independently of this observer.
[[raw-lean-py]]
==== py
`py("...")` embeds a Python expression as a *Lean string literal*. Lean's real parser handles the theorem, comments, binders, parentheses, and string escapes. Its quotation elaborator passes the decoded string to Python's parser and translates the Python AST into modeled Lean semantics. It resolves captured variables in Lean's local context and checks that they have type `PyValue`. Generated code is a closed function applied to those captures, so its temporary names cannot capture theorem variables. Python source functions are not executed to decide whether a theorem is true.
In a proposition, `py("condition")` means that the condition evaluates successfully to Boolean `True`. `Returns(py("run_trial(this_function, counter, worker_count)"))` and `Throws(py("run_trial(this_function, counter, worker_count)"))` refer to the executable Python helper. Helper names resolve to definitions in the same source module; `this_function` denotes the enclosing worker.
These are native Lean term constructs, usable in both source docstrings and `.lean` proofs. Lean handles the surrounding logic normally: nested quantifiers, named hypotheses, conjunctions, implications, negation, and `let` bindings need no quotation-specific theorem patterns. There is no regular-expression extraction of binders or rewriting of theorem text. Unknown captures and captures of the wrong Lean type are elaboration errors.
Lean raw strings are useful for multiline Python and embedded quotes:
[source,lean]
----
py(r#"
type(counter) == list and len(counter) > 0
and all(type(item) == int for item in counter)
"#)
----
A quotation inside a Python docstring crosses two string-literal boundaries. Use a raw Python docstring (`r"""..."""`) if you need backslashes to reach Lean unchanged. Lean comments and ordinary strings containing the text `py(...)` are not quotations.
Predicates support exact `type` checks, short-circuiting Boolean `and`, guarded `len`, integer comparisons, and `all` with an unfiltered generator of Boolean predicates. Separate predicate helpers have ordinary positional arguments and one return expression. A list type guard must precede its length check and iteration; an integer guard must precede numeric comparison of an arbitrary value. Exact integer checks exclude Python booleans.
Trial helpers currently accept Python `int` and `list[int]` parameters after the worker parameter. Their first statement must be an executable `assert` establishing those types, usually by calling the same predicate used in the theorem. The compiler checks that assertion's Python AST, independently of the surrounding Lean logic. Invalid inputs raise `AssertionError`, so even negated outcome claims have a meaningful modeled input domain. Annotations guide translation but never act as assumptions. Execution assumes Python assertions are enabled.
Setup supports integer-list snapshots with `copy()`, integer-list literals, and mutex allocation. Execution uses a `ThreadPoolExecutor`, a submission comprehension, and `future.result()` for every worker. Checks support indexing, slices, integer arithmetic, and ordinary assertions; a helper may omit final assertions when only its execution matters. Worker bodies use the operations described under <<raw-lean-parallel>>.
Quoted outcomes support `Returns`, `Halts`, `Throws`, `CanDeadlock`, `DeadlockFree`, and `CanDiverge`. General proofs use the unbounded concurrent transition system. `Returns` also accepts the existing common-mutex certificate, which supports inductive proofs for arbitrary worker counts. Quoted helpers must provide enough pool threads for every submitted job: use `max_workers=max(1, worker_count)` with `range(worker_count)`, `max_workers=max(1, len(jobs))`, or a positive literal large enough for a literal range. This makes both positive and negated scheduling claims meaningful; a counterexample cannot rely on nonexistent pool capacity.
A precondition in the Lean theorem is an assumption. An `assert` in the trial is executable code whose success or failure is modeled. Unsupported Python constructs in either helper are reported for every dependent proof while other supported obligations continue to be checked.
[[raw-lean-python-comparison]]
==== python_comparison
`python_comparison(left < right)` produces the comparison execution used by `Returns`, `Halts`, and `Throws`. These wrappers expand comparisons automatically, so it is usually unnecessary to write this helper yourself.
Supported operators are `<`, `<=`, `>`, `>=`, `==`, and `!=`, with operands of type `FormalSW.PyAst.Value`. Parentheses are allowed; Python comparison chains and arithmetic on modeled values are not yet supported. Ordinary `<` outside these wrappers retains its usual Lean meaning.
For example, `python_comparison(left <= right)` expands to `comparison _this_module .ltE left right`. `.ltE` and `.lt` are Lean's shorthand for comparison-operation constructors, selected using the expected type.
Custom same-class comparisons execute the supported method AST, including loops, on empty objects or objects with an integer `value` field. `.object "Looping"` represents an empty object; `.object "DummyInt" (some 2)` represents one with `value = 2`. These Lean constructors describe object state; they do not execute Python `__init__`. Reflected comparison, `NotImplemented`, general method calls, and arbitrary object layouts remain unsupported.
[[raw-lean-python-context]]
==== python_context
`python_context "source.py" "worker" SourceAst.module in proposition` supplies the Python source, enclosing function, and imported semantic AST for quotations. FormalSW inserts it around a function's quoted specification. Generated proof stubs preserve the quoted theorem and include this context explicitly, so the same syntax works directly in Lean. Names used inside a quotation refer to the Lean scope at that quotation, including nested binders and `let` values.
[[raw-lean-python-data]]
==== python_data%
`python_data% (include_str "path/to/definition.py")` parses Python source through the existing AST bridge and validates the reusable read-only data subset. It imports the resulting AST as a Lean `Module`; it does not run the Python definition during elaboration. `include_str` makes source edits a Lake build dependency. Validation covers the whole source, including dead branches, and rejects mutation, arbitrary calls, imports, defaults, builtin shadowing, and other unsupported syntax. The graph comparator uses this entry point; it is separate from the contextual `py("...")` specification syntax.
[[raw-lean-pytrial]]
==== PyTrial
The generated trial description contains calls to actual compiled workers, their initial shared heap, and checks translated from the Python assertions. No fixed limit on list length or worker count is part of this description.
[[raw-lean-pytrial-assert-true]]
==== PyTrial.assertTrue
`PyTrial.assertTrue condition` evaluates one Python assertion condition, returning `some ()` for true and `none` for false.
[[raw-lean-pytrial-call]]
==== PyTrial.Call
The generated description of a trial call: its initial Python assertion and the concurrent body reached when that assertion succeeds.
[[raw-lean-pytrial-call-candeadlock]]
==== PyTrial.Call.CanDeadlock
The meaning of quoted `CanDeadlock`: the initial Python assertion succeeds and the body has a finite deadlock witness. A failed input assertion terminates exceptionally, so it cannot witness deadlock.
[[raw-lean-pytrial-call-candiverge]]
==== PyTrial.Call.CanDiverge
The meaning of quoted `CanDiverge`: the initial Python assertion succeeds and the concurrent body admits infinite execution.
[[raw-lean-pytrial-call-deadlockfree]]
==== PyTrial.Call.DeadlockFree
The meaning of quoted `DeadlockFree`: the input assertion fails immediately, or it succeeds and the body has a deadlock-freedom certificate. `Call.halts_deadlockFree` derives this from a quoted termination proof.
[[raw-lean-pytrial-call-halts]]
==== PyTrial.Call.Halts
The meaning of quoted `Halts`: the input assertion fails immediately, or it succeeds and the whole concurrent body terminates. `Call.returns_halts` derives this from quoted `Returns`.
[[raw-lean-pytrial-call-returns]]
==== PyTrial.Call.Returns
The meaning of `Returns(py("trial(...)"))`: the input assertion succeeds, and `PyTrial.Returns` proves successful completion and all final checks of the body.
[[raw-lean-pytrial-call-throws]]
==== PyTrial.Call.Throws
The meaning of `Throws(py("trial(...)"))`: the input assertion fails, or it succeeds and some actual modeled body execution raises a worker exception or fails a final assertion. A rejected input is an exception, not unsupported execution.
[[raw-lean-pytrial-candeadlock]]
==== PyTrial.CanDeadlock
A successfully constructed trial whose explicit worker batch satisfies `ParallelRun.CanDeadlock`. Final assertions are reached only after workers finish, so they cannot introduce a worker deadlock.
[[raw-lean-pytrial-candiverge]]
==== PyTrial.CanDiverge
A successfully constructed trial whose explicit worker batch satisfies `ParallelRun.CanDiverge`. The trial's supported final assertion checks are finite.
[[raw-lean-pytrial-deadlockfree]]
==== PyTrial.DeadlockFree
Deadlock freedom of a constructed trial, established either by a termination certificate or by the general worker batch's `DeadlockFree` proof.
[[raw-lean-pytrial-halts]]
==== PyTrial.Halts
Termination of the concurrent body, established either by an existing `Returns` certificate or by the general worker batch's `Halts` proof. Both successful and exceptional completion count; deadlock and infinite execution do not.
[[raw-lean-pytrial-mutexreturns]]
==== PyTrial.MutexReturns
The optimized successful-completion certificate for a complete common-mutex region. `Mutex.Ensures` covers all orders of the worker bodies and proves their final assertions. Extraction rejects additional locks and control flow inside that region; use the general transition proof for those programs. This preserves the arbitrary-worker-count shared-counter proof.
[[raw-lean-pytrial-observedthrows]]
==== PyTrial.ObservedThrows
A completed exceptional trial observed by the finite explorer, including failed final assertions. Incomplete observations never establish this predicate. `PyTrial.Throws` additionally accepts finite reachability witnesses that require more steps than the default observation budget.
[[raw-lean-pytrial-read-int-item]]
==== PyTrial.readIntItem
`PyTrial.readIntItem heap object index` reads an integer from a mutable list using Python's positive or negative indexing. Missing objects, out-of-range indices, and non-integer elements fail the trial check.
[[raw-lean-pytrial-returns]]
==== PyTrial.Returns
Successful execution of a concurrent body, including all final assertion checks, on every enabled schedule. Proofs can supply either `PyTrial.MutexReturns` or a general `ParallelRun.Eventually` derivation whose accepted outcomes are successful heaps satisfying the checks. The general route allows branches, loops, and multiple locks. The optimized mutex route retains inductive proofs for arbitrary worker counts.
[[raw-lean-pytrial-throws]]
==== PyTrial.Throws
Exceptional execution of a concurrent body: some actual modeled schedule finishes all workers and exposes a worker exception or fails the trial's checks. A bounded complete observation or an unbounded finite reachability derivation supplies the witness. A worker exception followed by another worker's deadlock or infinite loop does not complete the joined batch. Deadlock, divergence, and unsupported execution do not count as exceptions. Unlike a deterministic call, the existence of one exceptional schedule does not imply termination of every schedule.
[[raw-lean-pyvalue]]
==== PyValue
The common type used by Lean quantifiers over modeled Python inputs. Its values include integers, booleans, strings, `None`, finite lists, and opaque objects. Python preconditions state the intended types; the user does not need to translate `list[int]` into a Lean list type.
Each integer-list argument is materialized as a fresh mutable array for the trial. Passing it to several workers shares that array; `copy()` creates a snapshot of its initial contents. Aliasing between separate list inputs, cyclic containers, custom descriptors, and general object execution are outside the current quotation model. The shared-counter property uses one flat integer list, so its entire stated input domain is covered.
[[raw-lean-returns]]
==== Returns
`Returns(this_function(values))` states that this particular call terminates successfully. Implicit `None`, bare `return`, and `return None` all count as successful returns.
`Returns(left <= right)` states that the Python comparison terminates successfully. Both `true` and `false` count as successful comparison results; it does not assert that the comparison is true.
The execution model proves:
[source,lean]
----
Returns(f(x)) ↔ Halts(f(x)) ∧ Not Throws(f(x))
----
The merge-sort theorem above assumes successful termination of the `<=` operations the algorithm actually uses. Absence of `<` exceptions is insufficient: comparison methods may differ or loop forever. The execution model requires an exact match with the supported merge-sort AST template and produces the actual merged list. Changing the body outside that template causes a validation error for requirements needing this model.
[[raw-lean-scalar-call]]
==== ScalarCall
A call with scalar global state. Its `Returns`, `Throws`, `Halts`, and `Diverges` predicates describe the Python outcome, while its internal `execution` records a `ScalarCompletion`. `Returns(this_function(...))` and the other call predicates select the appropriate model automatically. `ScalarCall.returns_iff_halts_not_throws` proves the same contract as for stateless execution.
[[raw-lean-scalar-call-equiv]]
==== ScalarCall.Equiv
`left.Equiv right` requires identical finite Python outcomes and final global state in both directions. `ScalarCall.equiv_of_finishes` proves equivalence from matching completions. Its `returns_iff` and `halts_iff` lemmas transfer execution contracts.
[[raw-lean-scalar-call-equiv-return]]
==== ScalarCall.EquivReturn
`left.EquivReturn right` requires equal results and equal final globals whenever both calls return successfully. It imposes no agreement on exceptional completions. An `Equiv` proof implies this property through `ScalarCall.Equiv.equivReturn`.
[[raw-lean-scalar-call-finishes]]
==== ScalarCall.Finishes
`call.Finishes outcome globals` means that the Python call terminates with that normal or exceptional outcome and that final global state. `ScalarCall.finishes_of_observe` turns a completed finite observation into this unbounded semantic proposition; running out of observation fuel supplies no such proof.
[[raw-lean-scalar-call-return-type]]
==== ScalarCall.ReturnType
`call.ReturnType "int"` requires exceptional completion or successful completion with an integer result. The other supported annotations are `"str"`, `"bool"`, and `"None"`. The DSL universally quantifies the arguments and initial globals around this per-call property.
[[raw-lean-scalar-completion]]
==== ScalarCompletion
A completion pairs `outcome : Except ExceptionObject Constant` with `globals : ScalarGlobals`. Final globals are present after exceptions as well as successful returns; Python does not roll back completed assignments when it raises.
[[raw-lean-scalar-function-with-globals]]
==== scalarFunctionWithGlobals
`scalarFunctionWithGlobals module "name" arguments globals` executes the actual function AST with explicit initial scalar global bindings. Ordinary locals shadow globals according to the whole function's scope. A `global` declaration changes the assignment target to module state. All declared global names must be supplied, duplicate bindings are rejected, and extra supplied globals are preserved so two functions can share an initial comparison state.
[[raw-lean-scalar-globals]]
==== ScalarGlobals
A list of named scalar values, such as `[("offset", .int offset), ("enabled", .bool enabled)]`. The DSL supplies the required names and types automatically. Low-level calls supply unique names explicitly; the generated specifications use a stable sorted order for state comparison.
[[raw-lean-shared-object]]
==== SharedObject
`.array values` represents a mutable Python list. `.object fields` represents a plain object's mutable fields, for example `.object [("prev", .none), ("next", .ref 1)]`. List indexing includes nonzero and negative integer indices; invalid indexing produces an exception. Field access uses the field name, independently of a worker's parameter names.
Objects used by workers are created in the initial heap. The current interpreter does not execute allocation or constructors during a worker call.
[[raw-lean-shared-state]]
==== SharedState
A shared state contains `objects`, a list of <<raw-lean-shared-object,SharedObject>> values indexed by their reference addresses, and `locked`, the identities of currently held mutexes. Both default to empty lists. For example, `{ objects := [.array [.int 0]] }` creates one zero-valued counter, with all mutexes initially unlocked.
Specifications can observe `state.item address index` or `state.field address "name"`; each lookup returns `some value` when present. A successful concurrent outcome contains the complete final shared state, allowing invariants to relate multiple objects and fields.
[[raw-lean-shared-state-read-path]]
==== SharedState.readPath
`state.readPath (.ref address) ["prev", "next"]` follows fields through a finite shared heap. It returns `none` on a missing field or an attempt to dereference Python `None`. A path ending in a field containing Python `None` succeeds with `some .none`; a path that tries to continue through it fails.
[[raw-lean-shared-value]]
==== SharedValue
A worker argument or local value can be `.int n`, `.string s`, `.bool b`, `.none`, `.ref address`, or `.lock identity`. References and mutex identities have distinct namespaces: `.ref 0` identifies heap object 0, while `.lock 0` identifies mutex 0. Copying a reference preserves identity and aliasing; it does not copy the object.
[[raw-lean-this-function]]
==== this_function
`this_function` binds the enclosing Python function using its source module and name. For scalar execution, calls accept zero or more arguments, for example `Returns(this_function())`, `Throws(this_function(1))`, or `Returns(this_function(a, b))`.
In a concurrent specification, `this_function arguments` describes one worker call. `arguments` is a list of <<raw-lean-shared-value,SharedValue>> values in Python parameter order, such as `[.ref 0, .ref 2, .lock 0]`. Each call receives its own local variables while references identify shared objects and mutexes. `parallelFunction module "name" arguments` constructs a call to another function in the same module.
The binding appears in generated stubs; `dsimp only` exposes the proposition for a proof. Other Lean identifiers can be used when bound to compatible execution functions or worker-call builders.
[[raw-lean-throws]]
==== Throws
`Throws(this_function(n))` states that this particular call terminates by raising an exception. `Throws(left < right)` states the same for a comparison. The execution model proves:
[source,lean]
----
Throws(f(x)) → Halts(f(x))
----
That implication applies to deterministic calls. For a concurrent batch, `Throws` means that *some* schedule completes exceptionally, whereas `Halts` covers *every* enabled schedule; one throwing schedule does not prove universal termination.
`Not Throws(...)` permits deadlock and infinite execution. Use <<raw-lean-returns,Returns>> when successful termination is required.
== How it works
The way it all works is as follows. When you run:
----
formalsw tmp.py
----
it will determine where to create the `.formalsw` directory. When you are inside a .git repository, `.formalsw` is always placed next to the `.git`. You basically always want to use Git becuse you want to check that you LLMs haven't mofidifed your specifications in source files.
Then, inside the `.formalsw` directory, `formalsw` converts the input Python source code to a versioned JSON AST under `.formalsw/tmp.py.ast.json`.
The adjacent `.formalsw/tmp.py.ast.lean` is only a small import bridge. Lean reads the JSON with `include_str`, validates `schema_version`, and elaborates it into a typed `FormalSW.PyAst.Module`. Proofs therefore continue to use `TmpAst.module` and operate on the typed data structure, not on untrusted claims made by the converter.
Compiled Lean `.olean` files for generated ASTs, proofs, and requirement checks are written to a single mirrored cache under `.lake/build/lib/lean/`. Keeping shared module prefixes in one object tree supports proofs inside nested Git repositories. Build artifacts are never placed beside checked-in `.lean` proofs.
Imports of other Python proof sidecars or generated Python ASTs are checked against their current sources before the importing proof, once per invocation. Dependencies require an adjacent proof file. Lean's import parser handles comments and escaped module names; failed or cyclic dependencies stop the dependent proof, even if old compiled objects still exist.
The top-level JSON shape is:
[source,json]
----
{
"schema_version": 1,
"ast": {
"type": "Module",
"body": []
}
}
----
Nodes use a `type` discriminator and fields close to Python's `ast` names. For example, a name expression is `{"type": "Name", "id": "n"}` and a constant is `{"type": "Constant", "value": 1}`.
At the same time, formalsw searches for `@formalsw:` markers in Python docstrings, and when those are found, it dumps them under `.formalsw/tmp.py.reqs.lean` in such a way that unless proof of each requirement is also found, things will blow up when Lean runs.
----
example :
Not (FormalSW.Property.Function.Throws TmpAst.module "sum")
:= tmp.sum.«Not Throws»
example :
FormalSW.Property.Function.Equiv TmpAst.module "sum" "sum_naive"
:= tmp.sum.«Equiv(sum_naive)»
example :
Not (FormalSW.Property.Function.Throws TmpAst.module "sum_naive")
:= tmp.sum_naive.«Not Throws»
----
Finally, formalsw runs Lean putting everything together:
* `.formalsw/tmp.py.ast.json` with the Python AST representation
* `.formalsw/tmp.py.ast.lean` with the small JSON-to-Lean import bridge
* `.formalsw/tmp.py.reqs.lean` mentioned above with the proof requirements
* `tmp.py.lean` which is supposed to contain your proof
* link:FormalSW.lean[] as the language-neutral package facade
* link:lang/py/FormalSW/Model.lean[] which defines the Python AST,
evaluator, and Python proof properties
* plain-Python builtin models under link:lang/py/builtin/type[] and their
adjacent, generated-AST-bound Lean proofs
[[unsupported-python-constructs]]
=== Unsupported Python constructs
A requirement on a function is rejected if its body or a modeled dependency contains Python constructs that FormalSW cannot handle. The coverage check examines the whole body, including unreachable statements and both branches of conditionals. This applies to DSL properties, negated properties, and raw Lean requirements alike. Equivalence targets and modeled comparison methods are checked too.
The diagnostic identifies the requirement, function, source location, and unsupported construct. Supported requirements and other files continue through checking. The command exits unsuccessfully without appending summary counts to the diagnostics. Stub generation reports the same errors and emits only supported obligations.
The scalar interpreter supports literals, local variables, supported arithmetic and comparisons, assignments, `if`, `while`, one-argument `range` loops, builtin exception raises, and returns. The simpler execution model keeps literal-divisor arithmetic; scalar functions with variable, negative, or computed divisors use the call interpreter. Variadics, keyword-only arguments, and arbitrary list programs need further execution-model support.
Scalar functions with ordinary local calls, conditional expressions, or general integer division use `FormalSW.PyAst.Calls.function`. This interpreter supports recursive and mutually recursive calls with fresh local environments, left-to-right argument evaluation, conditional expressions, and short-circuit `and`/`or`. Its explicit continuation stack has no fixed recursion limit. Calls currently require undecorated positional functions with scalar annotations and no globals or local shadowing of call targets; their bodies support scalar expressions, assignments, flat tuple unpacking from tuple displays of the same length, `if`, `while`, builtin `range` loops with one to three arguments, and returns. Tuple right-hand sides are evaluated left to right in the original environment before any target is assigned; repeated targets are then assigned in order. Coverage checks include all reachable callees and all their branches. This model supports scalar `Returns`, `Halts`, `Throws`, `ReturnType`, `Equiv`, and `EquivReturn` contracts, with optional preconditions; raw Lean theorems can state further execution properties.
Integer `//`, `%`, `//=`, and `%=` accept variable and negative divisors in the call interpreter. Division rounds down, the remainder has the divisor’s sign, and a zero divisor raises `ZeroDivisionError`. link:tests/py/division.py[] proves successful termination for all integer numerators and nonzero divisors and checks the zero-divisor exception.
Scalar entry points that allocate or use lists, directly or through local helpers, use `HeapCalls`. Each invocation gets fresh locals while all continuations share one heap. List allocation, `append`, scalar indexing, concatenation, repetition, in-place name assignment, conditional expressions, short-circuit Boolean expressions, `if`, `while`, and integer `for ... in range(...)` loops execute with ordinary helper calls and recursion. The eager builtin composition `list(reversed(value))` makes a fresh shallow copy of a list or a reversed list of string characters; standalone reverse iterators remain unsupported. Positional `max(a, b, ...)` supports scalar values, preserves the first value on ties, and evaluates all arguments before comparison. Returned references preserve aliasing. Method lookup happens before argument evaluation, and exceptions preserve mutations already performed. Range bounds evaluate once, left to right, with mutations retained on errors; signed strides, `else`, `break`, and `continue` preserve Python loop scope. Helpers can accept lists and immutable scalar defaults; frontend entry arguments currently need scalar annotations and an explicit supported return annotation. Globals, indexed assignment, slices, generator sums, iteration outside `range`, standard-library calls, and explicit `raise` statements remain unsupported in this backend. Equality and inequality support flat scalar lists, identical references, and unequal lengths; ordering and comparisons between distinct nested lists, and conversion of lists to strings, still need further modeling; every heap-call contract therefore requires a separate `Supported` proof that execution never reaches an unsupported operation. This coverage obligation is independent of `Not`.
`HeapCalls.call` returns the alias-preserving completion used by the existing heap model. For scalar return annotations, `HeapCalls.scalarFunction` exposes scalar results and exceptions for comparison with the scalar interpreters; it rejects a returned reference instead of silently erasing it. The proof rules `HeapCalls.Evaluates`, `BlockReturns`, and `ReturnsValue` track both the initial and final heap. `BlockContinues` describes normal completion with updated locals and heap, preserving arbitrary following statements and caller continuations. Its assignment, branch, and range-loop rules compose with `append`; `returns` connects a completed block to a later return proof. `Evaluates.conditional` tracks the heap through the condition and selected expression branch. `Evaluates.reversed_list` proves the copied contents, and `compare_int_lists` relates Python list equality to Lean list equality for arbitrary integer lists. `ReturnsValue.with_defaults` reuses a proof for an omitted-argument call, and `ReturnsValue.extend` transports a helper proof into a linked module using `Calls.Extends`. See link:tests/py/heap_calls.py[] for a proof with shared references, link:tests/py/heap_ranges.py[] for an exact list-building loop proof, and link:tests/py/heap_call_checks[] for Python comparisons covering mutation, returned aliases, recursion, error order, and execution coverage.
Scalar call execution supports trailing default arguments that are immutable scalar literals: integers (including signed literals), booleans, strings, and `None`. Defaults are recorded in the imported AST and fill omitted positional arguments before the function body runs. Explicit arguments override them. Function-level contracts still quantify every declared parameter; a caller proof covers omitted arguments through `Calls.BlockReturns.function_defaults`. Mutable or computed defaults, keyword arguments, and defaults in other execution backends remain unsupported. Python setup verifies both the value and type of imported defaults against the source. See link:tests/py/defaults.py[] and link:tests/py/default_checks[].
Scalar and heap call execution support `value.bit_length()` for integers and booleans, using the existing arbitrary-precision integer model. The receiver evaluates before method lookup; strings, `None`, and lists raise `AttributeError`. Calls with arguments and standalone bound-method values remain unsupported. This operation provides exact integer logarithmic estimates without converting large integers to floating point.
The scalar call interpreter supports `sum(range(stop))`, `sum(range(start, stop))`, and `sum(range(start, stop, step))` through the same reduction as range generator sums. Bounds evaluate left to right once, Boolean bounds act as integers, and a zero step raises `ValueError`. A private iteration variable cannot shadow Python locals. Both `sum` and `range` must resolve to their unshadowed builtins. The optional starting accumulator and heap-call execution remain unsupported.
Integer `**` and `**=` support arbitrary bases and nonnegative exponents, including Boolean operands and `0 ** 0`. Operands evaluate left to right before the operation. Negative exponents require floating-point execution and remain unsupported, including cases that would raise during conversion to floating point. Functions using powers, directly or through helpers, receive an additional generated `Supported` proof obligation under their `Requires` domain. It states that every finite execution prefix stays within the model; it does not impose a step bound or require termination. Equivalence obligations check both implementations, and coverage is not negated by `Not` markers. A successful `Returns` or `Halts` proof gives coverage with `.supported`; a `Diverges` proof does too. Raw execution references also trigger coverage for the referenced function in its declared domain; raw claims about executions outside that domain must establish their own coverage. Partial operations in a `Requires` predicate get a separate coverage obligation under the preceding prerequisites, so unsupported evaluation cannot silently remove valid inputs. link:tests/py/powers.py[] includes arbitrary integer powers, augmented assignment, Boolean exponents, helper calls, and the guarded decimal digit bound used by Project Euler problem 4. link:tests/py/power_checks[] compares runtime behavior with Python and verifies that a reflexive equivalence proof alone cannot certify an unsupported execution.
`Calls.ReturnsValue` proves a function's result independently of its caller continuation; `Calls.Evaluates` and `Calls.BlockReturns` provide compositional expression and block lemmas. A `ReturnsValue` proof implies successful termination, and two such proofs with the same result imply execution equivalence. link:tests/py/recursive_calls.py[] and its adjacent Lean proof demonstrate induction over recursive calls, nested arguments, and short-circuiting around a divergent branch. link:tests/py/tuple_assignments.py[] checks simultaneous assignment, repeated targets, empty unpacking, and exception order. `Calls.BlockReturns.unpack` and `Calls.BlockReturns.while_loop` support proofs of iterative algorithms. Stepped ranges evaluate all arguments once, from left to right, then retain the start, stop, and step independently of body assignments. Positive and negative steps, empty ranges, loop `else`, and early returns are modeled; zero steps raise `ValueError`. Shadowed `range` is rejected. `Calls.BlockReturns.for_range`, `range_step`, and `range_done` support unbounded iteration proofs; link:tests/py/stepped_ranges.py[] checks these rules and exception ordering.
The scalar call interpreter supports `break` and `continue` in `for` and `while` bodies, including nested conditionals and loops. `break` skips the nearest active loop’s `else`; `continue` resumes that loop’s next iteration and allows `else` after normal exhaustion. A transfer inside a nested loop’s `else` belongs to the surrounding loop. Loop boundaries stay within the function body, so helper calls cannot transfer control out of their callers. Early returns and exceptions still leave the function. `Calls.BlockReturns.break_loop`, `continue_loop`, and `loop_resume` provide compositional proof rules. link:tests/py/loop_control.py[] and its adjacent Lean proof cover nesting, loop `else`, helper calls, iterator-variable reassignment, return and exception propagation, and induction over arbitrary iteration counts.
Scalar strings support `str()` and `str(value)` for integers, booleans, strings, and `None`, integer indexing, and slices with arbitrary integer or Boolean bounds and steps. Omitted bounds and `None` use Python defaults; negative indices and steps operate on Unicode characters. Bounds evaluate left to right before subscription validates them. Invalid types, out-of-range indices, and zero steps raise the modeled Python exception class. The string domain is Lean `String` (Unicode scalar values), without Python's isolated surrogate code points. Decimal conversion is unbounded, corresponding to CPython with `PYTHONINTMAXSTRDIGITS=0`; its configurable decimal digit cap is outside this execution model, as is the recursion-depth cap. The frontend resolves builtin calls to `Expr.builtinCall` using source bindings before appending builtin models. A local function named `str` retains ordinary call semantics, and linking rejects declarations that would capture another module's builtin calls. `Calls.Evaluates.builtin`, `subscript`, and `slice` provide compositional proofs; `Strings.slice_reverse` connects reverse slices to list reversal. link:tests/py/strings.py[] proves reversal and double-reversal properties for arbitrary strings and checks helper bounds and exception order. link:tests/py/string_checks[] compares the primitives with Python and checks binding preservation.
`sum(element for name in range(...) if ...)` is normalized to `Expr.sumRange` after checking that `sum` and `range` are unshadowed builtins. The call interpreter evaluates bounds once, retains a private generator environment, short-circuits successive filters, and evaluates only yielded elements. It supports one range generator per sum, one to three range arguments, nested sums, helper calls, and integer or Boolean elements. An invalid step or element propagates its Python exception; an empty range never evaluates its element. `Calls.Evaluates.sum_range` and `Calls.SumReturns.keep`, `skip`, and `done` support induction over arbitrary iteration counts. link:tests/py/generator_sums.py[] checks scoping, filtering, descending ranges, nested sums, and exception order. Standalone generators, multiple `for` clauses, and the optional `sum` start argument remain unsupported.
Functions without requirements do not need execution coverage unless a requirement depends on them. Module-level raw theorems about source metadata, such as AST fingerprints, can inspect source without requesting its execution semantics.
The call interpreter also recognizes explicit `from math import isqrt` bindings, including aliases. Its arbitrary-precision integer square-root model uses terminating binary search. `FormalSW.PyAst.Math.isqrt_spec` proves the defining inequalities for every natural input, so client proofs can connect it to their mathematical square-root library. Negative integers raise `ValueError`; non-integer scalar arguments raise `TypeError`; Boolean arguments follow Python's integer-index behavior. Implicit exception messages have the same abstraction as other scalar errors. Rebound or shadowed function bindings, local modules shadowing `math`, and unsupported argument forms are rejected. link:tests/py/math_isqrt.py[] checks the source-bound execution model, including aliases and exception cases.
`from math import gcd` and its aliases use a variadic integer model: no arguments return zero, signs are discarded, Booleans act as integer indices, and every argument is validated even when an earlier gcd is already one. `Math.gcdCall_pair` connects a two-integer call to `Nat.gcd` on absolute values. The source-bound proofs in link:tests/py/math_gcd.py[] cover arbitrary integers, empty calls, Booleans, and type errors; link:tests/py/math_gcd_checks[] compares the model with Python and checks import shadowing.
Both functions also support `import math` and module aliases such as `import math as arithmetic`, in scalar functions and functions sharing lists. Arguments run from left to right, including mutations before a later argument or library call raises. Module rebinding, shadowing, and direct attribute writes are rejected. See link:tests/py/math_modules.py[] for source-bound proofs.
Byte literals such as `b"\x01"` retain their binary type. Call execution supports concatenation, repetition, integer indexing, comparisons, truth tests, and `str()` representation; scalar calls also support slicing. Negative repetition counts produce empty bytes. See link:tests/py/bytes_literals.py[] for proofs over arbitrary counts.
`Calls.Extends target source` records preservation of the source module's function definitions and modeled library bindings. `ReturnsValue.extend` reuses a verified result in such a target module, and `finishes_extend` also preserves finite exceptional executions. `Extends.prepend` constructs this preservation proof when added declarations have fresh names; its conditions inspect finite name lists. The linking examples in the adjacent square-root proof demonstrate result reuse and rejection of a replaced function. Source-level imported equivalence references use the import resolver described above; ordinary calls to imported user functions still require frontend linking support.
=== Python builtin model
The reusable non-floating-point builtin semantics live under link:lang/py/builtin/type[]. Builtins that can be expressed faithfully in Python have a `.py` implementation and an adjacent `.py.lean` proof. Each source requests explicit structural and complete-AST-fingerprint theorems, so the proofs are checked against the generated AST of that exact Python file. Builtin functions are grouped in link:lang/py/builtin/function.lean[], with feasible pure and protocol-delegating implementations in link:lang/py/builtin/function.py[] and its adjacent proof.
The Lean-only primitive boundary contains arbitrary-precision `int`, mutable `list`, balanced-tree storage, object identity and the runtime type/MRO machinery, the buffer protocol behind `memoryview`, and runtime code/module/function/singleton objects. Boolean value semantics are modeled in Python as an integer restricted to zero or one; CPython singleton identity remains outside that value model. Strings, bytes, byte arrays, tuples, ranges, slices, iterators, dictionaries and their views, sets and frozen sets, context managers, descriptors, and pure or protocol-delegating builtin functions have ordinary Python models layered over those primitives. Environment-dependent functions such as `eval`, `exec`, `compile`, `open`, import, terminal I/O, help, and breakpoint remain explicit Lean effect interfaces.
Mappings preserve Python insertion order while using a size-balanced binary search tree for key lookup. Sets and frozen sets use the corresponding size-balanced tree-set representation. The Lean types bundle their tree well-formedness invariants, and link:tests/py/builtin_models.lean[] checks that the dictionary and set facades expose those proofs.
Floating-point and complex-number semantics are deliberately excluded for now. Integer operations that would necessarily produce a float, such as two-argument `pow` with a negative exponent, return an explicit `floatingPointExcluded` result; integer-only branches such as negative modular powers and negative-digit rounding remain modeled.
link:tests/py/builtin_coverage[] derives callable coverage from the CPython `functions.rst` and `stdtypes.rst` documentation, with `CPYTHON_ROOT` selecting the CPython checkout. It also checks operations and runtime types documented only in prose or tables. The normal `./test` command runs this audit and the executable Lean behavior suite.
== Development
=== Development installation
Currently formalsw is a single Python file with no dependencies outside of the standard library, so you can just:
----
./formalsw ...
----
or:
----
export PATH="$PWD:$PATH"
formalsw
----
=== Test system
Run all tests under link:tests[]:
----
./test
----
=== Coding guidelines
Asciidoc: don't wrap lines.
=== Publish to Pypi
Install the https://packaging.python.org/en/latest/tutorials/packaging-projects/[standard build and upload tools]:
----
python3 -m venv .venv-release
. .venv-release/bin/activate
python -m pip install --upgrade build twine
----
Before publishing ensure that all the tests pass:
----
./test
----
From a clean Git checkout, run:
----
./release
----
This automatically increments the minor version and resets the patch version in `pyproject.toml` and `lakefile.toml` (for example, `0.1.3` becomes `0.2.0`), commits both files, creates an annotated `vVERSION` tag, and pushes the current branch and tag together to `origin`. Then it runs `python -m build`, `twine check --strict`, and `tests/package_checks` before uploading the source distribution and wheel to PyPI with Twine. It stops on the first failure.
Enter your PyPI API token at Twine's password prompt, or set `TWINE_PASSWORD` in your environment. The script supplies `__token__` as the username.
== Bibliography
* https://github.com/arsalan0c/dafny-of-python[]: converts Python to https://github.com/dafny-lang/dafny[Dafny]. Specifications seem to be Dafny code in Python comments.
1 maintainer
Metadata
1 maintainer
Release files for formalsw 0.3.0
For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.
Source distribution (sdist)
| File | Size | Uploaded | Provenance | Actions |
|---|---|---|---|---|
| formalsw-0.3.0.tar.gz | 350.6 kB | Without provenance | Details for formalsw-0.3.0.tar.gz |
Built distribution (wheel)
| File | Interpreter | ABI | Platform | Actions Reset |
|---|---|---|---|---|
| formalsw-0.3.0-py3-none-any.whl | Python 3 | none | any | Details for formalsw-0.3.0-py3-none-any.whl |
Total release size: 586.0 kB
Release files / formalsw-0.3.0.tar.gz
| Download URL | formalsw-0.3.0.tar.gz |
|---|---|
| Size | 350.6 kB |
| Tags | Source |
|
SHA-256 checksum How to use checksums |
0b38e5b490b2b11751e1bdeda86bf38889e58f95ef1adfa4568c0fa4bd0d737d
|
|
BLAKE2b-256 checksum How to use checksums |
a507d83e5932b053ff9be58905ed600b8ec1b7b008ab64d035be8b0cbd5e7c57
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
twine/7.0.0 CPython/3.14.4
|
Release files / formalsw-0.3.0-py3-none-any.whl
| Download URL | formalsw-0.3.0-py3-none-any.whl |
|---|---|
| Size | 235.4 kB |
| Tags | Python 3 |
|
SHA-256 checksum How to use checksums |
9a3e67a2453e2d38e1078281cc8efd2f517977486af36ae39dfad1f5b9b3f8cb
|
|
BLAKE2b-256 checksum How to use checksums |
9cd63a245429d1b0d4d9073a1b12973040e1d488fa7d3d2f01a3e61daa191f12
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
twine/7.0.0 CPython/3.14.4
|
Security for formalsw 0.3.0
Provenance
Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.
No provenance found
None of the files in this release were uploaded with provenance metadata.
A note on package security
PyPI is a repository for distributing packages, not a service for auditing them. While third-party security researchers and our staff do their best to detect and remove malicious packages, PyPI cannot guarantee the quality, security or suitability of any given package.
To learn more about protecting yourself from malicious actors, visit our package security documentation.
