gf2bv
allows you to build and solve linear systems over GF(2) by manipulating bitvectors, based on M4RI.
First, you need to have m4ri
installed on your system, try some package names like mr4i
, libm4ri-dev
or something else depending on your system.
Clone the repository and install the package with pip:
pip install .
Requires Python 3.11 or later.
You can also set the GF2BV_BUILD_M4RI
environment variable to automatically build m4ri
from source:
GF2BV_BUILD_M4RI=1 pip install .
Define a linear system using LinearSystem
and get the symbolic bitvectors with gens()
, then use the them to build the equations you want to solve. Equations are represented as a list of symbolic bitvectors that evaluate to zero named zeros
(You can choose other names if you want), then pass them to solve_one
or solve_all
to get the solutions.
from gf2bv import LinearSystem
lin = LinearSystem([1, 1, 1, 1])
a, b, c, d = lin.gens()
"""
This is the system we want to solve:
a + b + c = 1
b + d = 0
a + c = 1
"""
zeros = [a ^ b ^ c ^ 1, b ^ d, a ^ c ^ 1]
for sol in lin.solve_all(zeros):
print(sol)
from gf2bv import LinearSystem
import secrets
MASK64 = (1 << 64) - 1
def just_some_hash(x, y):
z1 = x ^ (y >> 22)
z2 = y ^ (x << 13) & MASK64
z1 ^= (z2 >> 5) & 0xDEADBEEFDEADBEEF
z2 ^= (z1 << 7) | 0x1337314213373142
return z1, z2
x, y = secrets.randbits(64), secrets.randbits(64)
z1, z2 = just_some_hash(x, y)
lin = LinearSystem([64, 64])
xx, yy = lin.gens()
zz1, zz2 = just_some_hash(xx, yy)
zeros = [zz1 ^ z1, zz2 ^ z2]
sol = lin.solve_one(zeros)
assert sol == (x, y)
assert just_some_hash(*sol) == (z1, z2)
print(sol)
Check the examples directory for more examples.
This package is pretty similar to xorsat, but I keep most of the code in Python for flexibility and ease of use.