possible way to use it with dataframes?

[petrusboniatus]

Hello.

I'm trying to make this tool work on dataframes (pandas, pyspark, polars, etc...) as most of the code that involve this abstraction tends to be a super buggy and tedious to test.

My first idea was to implement a very small subset of the api in pure python (as suggested in plugins documentation). I have tried a POC using a DfSymbolicInternal = Dict[str, Union[List[int], ..]and it kind of works. The problem is that for operations involving joins is not usable because it spends more than a minute even for the most trivial checks:

def select_should_fail(k: DfSymbolicInternal, p: DfSymbolicInternal) -> bool:
    """
    pre: valid_dataframe(k)
    pre: "a" in k and "b" in k
    pre: valid_dataframe(p)
    pre: "a" in p
    post: __return__ == True
    """

    k = select(k, {"a", "b"})
    k = join(k, p, on={"a"})
    k = select(k, {"k"})

    return True

-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
  File "/home/pedro/git/CrossHair/crosshair/core.py", line 1319, in attempt_call
    __return__ = unenforced_fn(*bargs, **bkwargs)
  File "/home/pedro/git/CrossHair/crosshair/condition_parser.py", line 102, in __call__
    return self.fn(*a, **kw)
  File "/home/pedro/git/sfdf/tests/test_sfdf.py", line 16, in select_should_fail
    k = select(k, {"k"})
  File "/home/pedro/git/CrossHair/crosshair/enforce.py", line 100, in _crosshair_wrapper
    raise PreconditionFailed(

I found an exception while running your function.
/home/pedro/git/sfdf/tests/test_sfdf.py:16:
|
|    k = select(k, {"a", "b"})
|    k = join(k, p, on={"a"})
>    k = select(k, {"k"})
|    print(k)
|
|    return True

PreconditionFailed: Precondition "all(c in df for c in cols)" was not satisfied before calling "select"
when calling select_should_fail({'a': v1:=[0], '': [0.0], 'b': [0.0]}, {'a': v1})
-------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
  Analyzed 3170 paths in "test_sfdf.py".

I also notice that it only uses one core, but I'm not sure how parallel this can be.

It is possible to speed this up just changing the formulation of the preconditions somehow or it would be necessary z3 and implement an specific modulo theory for dataframes? What would be your recommendation to try to solve this?

[pschanely]

So exciting.

• First, what you've started is awesome, and I'd love to contribute (directly, even, if you intend to open source it).
• Thanks for filing this bug, too. If people don't do that, I don't get realistic cases to optimize. With your permission, I'd love to add some adaptation of your code to CrossHair's benchmark suite.
• Right now, parallelization only happens at the file-level, just because that's what's convenient. Parallelizing the checking for a single condition is possible in theory, but we might want a way for the workers to communicate about the paths they've explored - it's nontrivial.
• I am pretty confident that we can get this kind of example to run faster. I doubt we need to go into Z3; much more likely is that we should tweak CrossHair's path search heuristics or modeling on dictionaries, lists, or unions. I suspect I'll have some time tomorrow to dig in. More soon!

[pschanely]

Fantastic. I didn't have AS MUCH time as I'd hoped, but I did implement one important improvement on the CrossHair side and push it this morning: support for collapsing branches that are internal to any() and all() when the yielded values are symbolic. Since you already know some Z3, you might be interested in the implementation. At any rate, this seems to give me a ~3X speedup locally. I know there is more that can be done, though - I'll continue to investigate this week.

[petrusboniatus]

I have made some benchmarks. Still can not pr any of it into the crosshair's benchmarks because they take more than a minute.

I was checking out the new commit with them and sadly I got a performance decrease, most notably the 005 It passes from ~1.5 mins in commit (8966c4f) to ~3 mins in commit (d1d978e). Tested both 2 times.

The good news are that most of the errors were actually detected, just with that I think is great if we can get decent times. I have some ideas for that, but first thing I will plain around a little bit z3 to see if I can get most common preconditions symbolically.

[pschanely]

After a little more digging: a small adjustment on the preconditions: consider list(k.keys()) == ["a", "b"] instead of the in operator (where appropriate); this prevents us from having to consider tables with arbitrary additional columns, and importantly re-orderings of the same columns (Python dictionaries are ordered - that's one of the reasons CrossHair doesn't implement dictionaries directly with Z3 arrays). Dropping this check before the valid_dataframe seems to be slightly better too.

As an alternative to the type annotation ideas below, perhaps valid_dataframe grows a bunch of kwargs that do column name and type checks - then we have the ability to carefully architect how those checks are performed inside the library.

Finally, CrossHair often doesn't model Python types using the Z3 capabilities you'd expect, and the reasons for this can be pretty involved. Sometimes though, those reasons are just "Z3 didn't handle these edge cases well when I tried it 2 years ago." So, I don't want to discourage you from investigating it from the Z3 side of things, but be prepared for some significant discussion when you have a proposal!

[petrusboniatus]

Update on this. After tinkering with z3 features I basically encounter that integer stuff (and fixed point grammars) scale much better that the rest, having learnt that I came out with a dataframe formulation that actually scales to the sizes needed at least for preconditions.

This takes 59 seconds:

from dataclasses import dataclass
from typing import List
from enum import Enum
from typing import Literal

class ColType(Enum):
    String = 1
    Float = 2
    Integer = 3
    # Adding more stuff for PKs and external relations

@dataclass
class ColSpec:
    typ: ColType
    l_0: int
    l_1: int
    l_2: int
    l_3: int
    l_rest: List[int]

@dataclass
class NewDF:
    size: int
    col_hashes: List[int]
    col_spces: List[ColSpec]
    possible_string_values: List[str]
    possible_float_values: List[float]

def required_cols(df: NewDF, cols: List[int]): # adaptation of list(k.keys()) == ["a", "b"]
    return df.col_hashes[:len(cols)] == [c for c in cols]

def valid_df(df: NewDF):
    return (len(df.col_hashes) == len(df.col_spces)
            and len(df.possible_string_values) > 10
            and len(df.possible_float_values) > 10)


def get_element(df: NewDF, col: int, row: int):
    spec = df.col_spces[col]
    if row >= df.size:
        raise IndexError
    spec_list = [spec.l_0, spec.l_1, spec.l_2, spec.l_3] + spec.l_rest
    if spec.typ == ColType.Integer:
        return spec_list[row % len(spec_list)]
    elif spec.typ == ColType.String:
        return df.possible_string_values[spec_list[row % len(spec_list)]]
    elif spec.typ == ColType.Float:
        return df.possible_float_values[spec_list[row % len(spec_list)]]


df1_expected_cols = [hash(f"{e}nth_col") for e in range(15)]
df2_expected_cols = [hash(f"{e}nth_col") for e in range(15)]
def check_equal_join(df_1: NewDF, df_2: NewDF) -> bool:
    """
    pre: valid_df(df_1)
    pre: valid_df(df_2)
    pre: df_1.size > 100
    pre: df_2.size > 100
    pre: required_cols(df_1, df1_expected_cols)
    pre: required_cols(df_2, df2_expected_cols)
    pre: get_element(df_1, 5, 30) == get_element(df_2, 0, 0)
    pre: get_element(df_2, 4, 0) == "best potato"
    pre: get_element(df_2, 4, 1) == "worst potato"
    post: __return__ == True
    """
    return False

One thing that came as a shock to me is that without precomputing the hash outside the function it does not end, I still don´t understand why is the case because number of iterations shown by crorsshair does not seem high enough for this to matter and this should happens in pure python. Anyway I think a hack can be engineered in order to hide this to the user. Maybe you have a better understanding on why it might be the case.

I have also ran in some of the edge cases I think have prevented this library to fully use the Sequence features. The only Sequence that works without unexpected "unknown" when scaling a little bit is the Integer Sequence.

[pschanely]

Neat trick with using the enum to switch on the types: although ugly, you might consider even dropping the enum and just using an int; like Union[]s, enums are case-split at symbolic generation time, but a plain int can remain symbolic until a comparison happens on it.

With regards to the hash problem, I've forked issue #190 : but as a workaround (and something you likely want to do anyway), you can guard the hash computation in a with crosshair.NoTracing(): block. This disables many of CrossHair's runtime interceptions, but is safe to use anytime you know that you are not working with any symbolic values.

I have also ran in some of the edge cases I think have prevented this library to fully use the Sequence features. The only Sequence that works without unexpected "unknown" when scaling a little bit is the Integer Sequence.

If you go into a little more detail, I'm more than happy to research. LMK!

[petrusboniatus]

Hello, I was digging into this trying to isolate the problem that part of the problem might be how the 'in' operator is mapped to z3.

Crosshair watch returns something on this function after 55 seconds, meaning (if I understand correctly this part) it takes that time to generate an example given the pre-conditions. Because post-conditions are never met it should fail in the first example. This happens also with dictionaries and Sets.

def keys_in_an_array(arr: List[str]) -> bool:
    """
    pre: "a" in arr
    pre: "b" in arr
    pre: "c" in arr
    pre: "d" in arr
    pre: "e" in arr
    post: __return__ == True
    """
    return False if "a" in arr else True

But solving the same constraints in z3 takes 0.1s

In [15]: import z3
    ...: import time
    ...: start_time = time.time()
    ...: s = z3.Solver()
    ...: sseq = z3.Const('sseq', z3.SeqSort(z3.StringSort()))
    ...: s.add(z3.Contains(sseq, z3.Unit(z3.StringVal("a"))))
    ...: s.add(z3.Contains(sseq, z3.Unit(z3.StringVal("b"))))
    ...: s.add(z3.Contains(sseq, z3.Unit(z3.StringVal("c"))))
    ...: s.add(z3.Contains(sseq, z3.Unit(z3.StringVal("d"))))
    ...: s.add(z3.Contains(sseq, z3.Unit(z3.StringVal("e"))))
    ...: s.add(z3.Contains(sseq, z3.Unit(z3.StringVal("f"))))
    ...: s.check()
    ...: print(s.model())
    ...: print("--- %s seconds ---" % (time.time() - start_time))
[sseq = Concat(Unit("c"),
               Concat(Unit(""),
                      Concat(Unit("f"),
                             Concat(Unit(""),
                                    Concat(Unit("d"),
                                        Concat(Unit(""),
                                        Concat(Unit("e"),
                                        Concat(Unit(""),
                                        Concat(Unit("a"),
                                        Concat(Unit(""),
                                        Unit("b")))))))))))]
--- 0.01843857765197754 seconds ---

Sorry if I misunderstood something, I am still trying to get my head around the internals of it.

[pschanely]

You're understanding correctly; in early versions, CrossHair attempted to use Z3's native string & sequence support, but for a variety of reasons it has fallen back to using less advanced capabilities. I won't get into those immediately, but let me fork this into another discussion.

Also. One fundamental decision in CrossHair: use the actual interpreter to run the user's code, while patching values/functions/opcodes as necessary. Therefore, a list of asserts is really like a big binary tree exploration. Other people have made attempts at an AST-level analysis. In theory, that gives us a lot more power, but it is a lot more development effort to faithfully reproduce Python's behavior.

[pschanely]

Side thread: Have you ever tried anything like strictly-typed-pandas? Or, perhaps you'd invent your own more-strongly-typed dataframes?

Having the actual columns and types at generation time would help a lot. You can hook into how crosshair generates values from a type with register_type():

def make_dataset(creator: crosshair.SymbolicFactory, typearg):
  fields = typing.get_type_hints(typearg)
  if len(fields) == 0:
    return {}
  data = {name: creator(List[typ]) for (name, typ) in fields.items()}
  with crosshair.ResumedTracing():
    lengths = [len(v) for v in data.values()]
    if lengths[0] == 0:
        raise crosshair.IgnoreAttempt
    if any(len(v) != lengths[0] for v in data.values()):
        raise crosshair.IgnoreAttempt
  return data
      
crosshair.register_type(strictly_typed_pandas.DataSet, make_dataset)

Then also you could dispense with many of those fiddly preconditions checking column names and types; e.g.:

class XYDataFrame:
  x: float
  y: float

def test_fn(k: strictly_typed_pandas.DataSet[XYDataFrame]):
  ...

And CrossHair will run this quite fast, I think.

[petrusboniatus]

Hi,
I only have experienced the dependent type side so my opinion is biased. I think the case of dataframe might be one the few cases where dependent types are cleaner because you can call normal function to construct your type witch comes very handy, one very good example is the transpose function.
I think this is also a strong point of crosshair, because the user can "define the type" by calling normal python functions she already knows.

Also being myself a fan of typing, my personal experience in professional settings tells me that the best approach with python is usually to focus less on typing and more on testing, there are just too many possible runtime errors.

[pschanely]

@ConnorBaker If you haven't already seen them, you might be interested in some of my experiments with CrossHair + numpy; here is a simple shape arithmetic example. To your point about FFI, without a pure-Python numpy implementation, these examples are effectively just doing randomized property testing. I haven't played with it, but since phantom-tensors has runtime checks, CrossHair might be able to analyze it by faking the underlying arrays in a similar way.

My understanding is that the Liquid* systems constrain the language of the refinements to ensure solver ~efficiency and soundness. CrossHair does not, which makes it a poor choice for verification; but in exchange we get some usability things that @petrusboniatus mentioned, like the ability to just using the regular old Python that you already know.

[ConnorBaker]

@pschanely Any thoughts on implementing something which supports libraries which comply with the Array API (https://data-apis.org/array-api/latest/)? I know that Hypothesis is using it as a way to support more numerical libraries: https://hypothesis.readthedocs.io/en/latest/numpy.html#. NumPy offers support, though it's marked as experimental (https://numpy.org/doc/stable/reference/array_api.html). PyTorch has an issue they're using to track API compliance (pytorch/pytorch#58743).

Reading through Hypothesis' ArrayStrategy (https://github.com/HypothesisWorks/hypothesis/blob/master/hypothesis-python/src/hypothesis/extra/array_api.py#L326) was interesting; I'd love to hear any thoughts you have!

[pschanely]

I wasn't aware of the Array API! It looks like a good interface to target for a pure Python implementation (sadly, it looks like a reference implementation is out-of-scope), which CrossHair could then analyze. And it would then be trivial to have CrossHair plugins that bridge specific libraries with the pure implementation e.g. register_type(np.array_api._typing.Array, lambda c: c(PurePythonArrayImpl)).

I am confident that I wouldn't have time in the near-ish future to work on such a project, but would be very happy to support a motivated party!

[petrusboniatus]

@ConnorBaker That standard is very interesting.

Currently I am working on trying to improve the performance over sequence and sets. But my end goal here is to "fix" datasience projects, basically the 4 elements in the roadmap I think are:

1. Sql
2. Dataframes
3. N-Dimensional arrays
4. Add easier tools to treat with non python code
   Of course 1, 2, 3 are very related: dataframes are implemented with ndarrays and you can map al sql to dataframes calls.
   For arrays I also came across this library that is pure python, maybe it can be adapted to fit specifications. If that is too costly (either in computation or in work) I think we can at least work around a decent amount of predicates about shape, value bounds, etc... around the standard.

So I deferentially will contribute to this project or create it myself eventually if nobody does.