Prove a function is surjective using Z3

I'm trying to understand how to prove efficiently using Z3 that a somewhat simple function f : u32 -> u32 is bijective:

def f(n):
    for i in range(10):
        n *= 3
        n &= 0xFFFFFFFF # Let's treat this like a 4 byte unsigned number
        n ^= 0xDEADBEEF
    return n

I know already it is bijective since it's obtained by composition of bijective functions, so this is more of a computational question.

Now, knowing the domain and codomain are finite and of the same size, I thought of first doing this by asking Z3 to find a counterexample to it being injective:

N = BitVec('N', 32)
M = BitVec('M', 32)
solve(N != M, f(N) == f(M))

However this is taking quite a while (> 10 minutes but shut it down after), and reasonably so, since the search space is pretty much 64 bit and the function may be quite complex to reason about since it mixes a lot of multiplication with binary arithmetic, so I wondered whether it was possible instead to prove it by surjection, maybe resulting faster.

Whether that's actually faster or if there's even a way to solve this efficiently yet may be another question, however I was stuck on thinking how to prove it by surjection, that is ask Z3 to find an M such that f(N) != M forall N.

Is this anywhere different from proving injectivity?

How do I state it in Z3's python bindings?

Is it possible to remove existential qualifiers out of the surjective statement at all?

Are there more efficient ways to prove that a function is bijective? Since for something like this a bruteforce search may be more efficient, as the memory required shouldn't be a lot for 32 bit vectors, but the approach surely wouldn't work on 64 bit input/outputs.

You'd write the surjectivity as follows:

N = BitVec('N', 32)
M = BitVec('M', 32)
s = Solver()
s.add(ForAll([N], f(N) != M))

r = s.check()
if r == sat:
    print(s.model())
else:
    print(r)

Unfortunately adding quantifiers to bit-vectors make the logic undecidable in general, and z3 simply gives up after about 10 seconds on my machine:

unknown

In general, adding quantifiers is just going to make the problem very difficult for z3 (or any other SMT solver for that matter). Your original encoding of:

solve(N!=M, f(N) == f(M))

is probably the best way to encode this problem. And in fact, if you change the range from 10 to something smaller (I tried up-to 3), z3 answers unsat relatively quickly. But obviously the solver time will go exponentially as the number of iterations in your function f increases.

An SMT solver is probably not the best tool to prove a property like this. You can surely express such constraints, but at best you'll get unknown as an answer and at worst it'll loop forever. A proper theorem prover (like Isabelle, HOL, Coq, ACL2, etc.) would provide a much better (at the cost of being less automated) platform to do these proofs.