Why are inputs assumed mutable?

[amacfie]

According to PEP 316, post: ... and post[]: ... are equivalent, but CrossHair treats them differently, specifically in the former case input objects are assumed mutable. Since the CrossHair docs say "never target code that can directly or indirectly call mutating side-effects", should CrossHair default to assuming inputs are immutable? Currently with icontract I don't see a way of expressing mutability or immutability so it always assumes mutability.

Addendum: How are class invariants supposed to work if CrossHair isn't intended for side-effects?

[pschanely]

The thing you noticed about post[]: ... vs post: ... is indeed one of the places where we currently diverge from the spec. It's a decision I'd be open to revisiting, FWIW. The idea is that it sometimes helps CrossHair to know that a function will not mutate its inputs. (and it might help the end user to be able to verify such things as well)

The docs are far too vague on the "side effect" warnings right now (thanks for helping me realize this!). In general, reasoning about mutation is supported by CrossHair, and that's why we have things like class invariants.

There are two real requirements that I'm trying to express with this warning:

1. The analyzed code should not perform IO, or any other side effect that's external to the program.
2. The analyzed code must behave deterministically and must not alter global state (singletons, etc) in ways that could compromise the deterministic behavior of itself or other analyzed functions.

In fact, probably the docs should instead just state these two bullets above, explicitly. WDYT?

[amacfie]

Yeah that sounds like a good suggestion for the docs. My main issue is that with icontract there's no way to tell CrossHair that arguments aren't mutated (even when they're typically immutable types like ints) and this prevents CrossHair from using inner functions' contracts to shortcut.

[pschanely]

BTW: it's impressive that you've figured out so much of how CrossHair works on your own!

@mristin FYI. We could probably introduce some kind of new "does not modify arguments" marker (whether that's inside or outside of icontract). In fact, maybe the docstring parser should use that marker too, and then we could be more compliant with the PEP. Note that we care about "deep" immutability here, and so it's probably not useful for enforcement in production/runtime code.

Another idea is that we do type inspection for very simple immutable cases, like ints. This won't catch all possible immutable scenarios, but would perhaps get us pretty far.

Out of curiosity, do you have a real-world example? One recurring problem you'll notice is that we have no shortage of ideas and heuristics that we could implement. I'd really like to have a "benchmark" repository of faulty code + contracts that anyone could contribute to. Then, for any CrossHair code change, we could measure something like mean time-to-detection. In recent times, I've been unclear about how much function short-circuiting really buys us. Having more realistic examples would help us convince ourselves that it's important!

[mristin]

@amacfie could you please give a short example just that I understand a bit more precisely what you mean? You are not referring to conditions in the contracts mutating the input, but specifying somehow that the function does not mutate the inputs (similar to C++ const methods)?

I wrote once to python-idea asking for const in typing similar to how it works and propagates in C++, but it did not resonate with the folks.

Perhaps I misunderstood, but at the moment you can use immutable structures such as Mapping, Sequence and dataclass (with frozen=True) to achieve immutability at static time analysis.

[amacfie]

@pschanely I don't know about "real-world" but this short circuiting is essential for verifying recursive functions via proof by induction. This allows CrossHair to not get stuck in loops: convert the loop to a recursive function and put the loop invariant as contract.

[amacfie]

@mristin The idea was to specify somehow that the function does not mutate some or all input objects. I agree we should probably infer immutability from types like int (which was my original use case).

If CrossHair knows that an inner function doesn't mutate its arguments, then CrossHair can try skipping the execution of the function and rely on the inner function's contract to check the outer function. Here's an example where CrossHair can't skip the inner function.

import icontract

@icontract.require(lambda s: s == '')
@icontract.ensure(lambda result: result == '')
def f1(s: str) -> str:
    s = f2(s)
    return s

@icontract.ensure(lambda s, result: result == s)
def f2(s: str) -> str:
    s.append('b')
    return s

CrossHair currently does support inferring immutability from PEP 316 contracts although this support is not exactly in adherence with PEP 316 semantics (see above).

[mristin]

@amacfie that would be precisely the case for `Const[T]` or `ReadOnly[T]`, wouldn't it? (Edit: corrected the addressee)

[mristin]

Also this one: python/typing#242

[pschanely]

Really interesting background discussions here - thanks! I also dug up python/mypy#4468

Yeah, @amacfie, we could start and advocate for a new Python convention here - some kind of pure hint that's initially just advisory (although, CrossHair could be used to check the correctness of such purity hints!). It does seem like there are other people out there that care about this. And getting enough people to adopt a convention might eventually motivate a core language feature.
WDYT about creating a github repo with just a readme that defines it, and then we have a place to hang discussions etc with the broader community?

To be clear, CrossHair's specific need here is deep immutability. What I mean by that is a Const[Tuple] might still hold a reference to a mutable list - CrossHair needs to know that the list isn't mutated too!

[amacfie]

I don't mind creating a repo but we should probably do some more thinking first. I guess the restriction that a function doesn't mutate an argument actually should be expressed by the type of the function rather than the types of its arguments. In Python as far as I know the type of a function is just the list of types of its arguments and return value unlike the more flexible function types in say F*. However def f(s: ReadOnly[str]) might be a reasonable abuse of notation. Without changing the Python syntax here are some options:

• Define a generic type ReadOnly in icontract or CrossHair or something so it could be used by doing from icontract import ReadOnly.
• Use docstring or comments or variable name convention.
• Add an option to contracts, e.g. @icontract.ensure(..., mutates=False). Not sure how it would work if you want to say only certain arguments are not mutated.

If icontract wants to check if immutability is respected at runtime I guess it would make deep copies and then check for equality?

Then there's the additional question of how to annotate a function to say that it's pure and doesn't mutate globals either which might be useful.

With or without any new convention, to infer deep immutability just from argument types I guess it would have to be done recursively, e.g. if it's Tuple[X, Y], we recursively see if X and Y are immutable types. Maybe it's possible to check frozen (dataclass or attrs) classes by recursively checking members. The pyrsistent package also defines some immutable types but too many of these special cases would be messy.

[mristin]

@amacfie you can already do that using snapshots in icontract:

@snapshot(lambda lst: lst[:])
@ensure(lambda lst, OLD: lst == OLD.lst)
def some_func(lst: List[int])->None:
    ...

My idea was that the user needs to steer how much copying is needed in most cases as otherwise the performance would suffer. This construct is also versatile enough to allow you to check for specific side effects. (Admittedly, it is a bit cumbersome to write...)

The deal contract library has checks for pure functions: https://deal.readthedocs.io/basic/side-effects.html. If I understand correctly, they use static analysis to enforce purity based on one or more markers.

[amacfie]

Aha. Maybe CrossHair can check for such conditions.

[mristin]

Here are the slides from a lecture I had at the university (this is the newest version from 2020): https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Courses/AS2020/Coop/lecture%2006%20-%20object%20structures.pdf

It might be a quick introduction for the interested people not familiar with the details. The section "6.3 Read-only Types" is relevant for this discussion.

[mristin]

I also found this paper informative for an introduction back in the day: http://pm.inf.ethz.ch/publications/getpdf.php?bibname=Own&id=MuellerPoetzsch-Heffter01a.pdf