使用 Z3 证明函数是满射函数

Question

我试图了解如何有效地使用 Z3 证明一个有点简单的函数f : u32 -> u32是双射的：

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

我已经知道它是双射的，因为它是通过双射函数的组合获得的，所以这更像是一个计算问题。

现在，知道域和协域是有限的并且大小相同，我想首先通过要求 Z3 找到一个反例

来做到这一点：

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

然而，这需要相当长的时间(> 10 分钟，但之后关闭它(，而且合理，因为搜索空间几乎是 64 位，并且该函数可能非常复杂，因为它混合了大量乘法与二进制算术，所以我想知道是否有可能通过满射来证明它， 也许结果更快。

这是否实际上更快，或者是否有一种方法可以有效地解决这个问题可能是另一个问题，但是我一直在思考如何通过超射来证明它，那就是要求 Z3 找到一个M这样f(N) != M forall N。

这与证明注射性有什么不同吗？

如何在 Z3 的 python 绑定中声明它？

是否有可能从满射陈述中删除存在限定词？

有没有更有效的方法来证明函数是双射的？因为对于这样的事情，暴力搜索可能更有效，因为 32 位矢量所需的内存应该不多，但这种方法肯定不适用于 64 位输入/输出。

Answer 1

你可以按如下方式写出超射率：

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)

不幸的是，向位向量添加量词会使逻辑通常不可判定，z3 在我的机器上大约 10 秒后就放弃了：

unknown

一般来说，添加量词只会使 z3(或任何其他 SMT 求解器(的问题变得非常困难。您的原始编码：

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

可能是对此问题进行编码的最佳方法。事实上，如果你将范围从 10 更改为更小(我尝试了最多 3(，z3 的答案unsat相对较快。但显然，求解器时间将随着函数f迭代次数的增加呈指数级增长。

SMT 求解器可能不是证明此类属性的最佳工具。你当然可以表达这样的约束，但充其量你会得到unknown答案，最坏的情况是它会永远循环。一个适当的定理证明器(如Isabelle，HOL，Coq，ACL2等(将提供一个更好的(代价是自动化程度较低(的平台来完成这些证明。