variables abstraction

This commit is contained in:
2026-07-13 10:53:12 +02:00
parent baa9bdb16d
commit 1e80bb1235
3 changed files with 66 additions and 49 deletions
+1 -1
View File
@@ -56,7 +56,7 @@ def build_target_poly(
if rounds < start:
raise ValueError(f"rounds={rounds} is smaller than current step_count={start}")
for _ in range(rounds - start):
model.step(skip_abstract=True)
model.step(skip_abstract_R=True, skip_abstract_x=False, skip_abstract_r=False)
return model.R_bits[target_reg][target_bit]
+4 -2
View File
@@ -20,7 +20,9 @@ def run_precompute_cli():
raw1 = input("Bits to set to 1: ").strip()
one_bits = raw1.split() if raw1 else []
skip_abs = prompt_choice("Skip abstraction (R-register monomial replacement)? (0/1): ", {0, 1})
skip_abstract_R = prompt_choice("Skip R abstraction (R-register monomial replacement)? (0/1): ", {0, 1})
skip_abstract_r = prompt_choice("Skip r abstraction? (0/1): ", {0, 1})
skip_abstract_x = prompt_choice("Skip x abstraction? (0/1): ", {0, 1})
filename = input("File to save the model (e.g. 'model_8steps.sobj'): ").strip()
if not filename:
@@ -39,7 +41,7 @@ def run_precompute_cli():
print(f"Running {steps} steps")
for i in range(steps):
model.step(skip_abstract=skip_abs)
model.step(skip_abstract_R=skip_abstract_R, skip_abstract_r=skip_abstract_r, skip_abstract_x=skip_abstract_x)
print(f" Step {i+1} done.")
# save
+61 -46
View File
@@ -12,11 +12,11 @@ class Tea3Model:
self.step_count = 0
names = (
[f"x{i}{j}" for i in range(5) for j in range(8)] + # 039
[f"y{i}{j}" for i in range(5) for j in range(8)] + # 4079
[f"r{i}{j}" for i in range(5) for j in range(8)] + # 80119
[f"R{i}{j}" for i in range(8) for j in range(8)] + # 120183
["g"] # 184
[f"x{i}{j}" for i in range(5) for j in range(8)] + # 0-39
[f"y{i}{j}" for i in range(5) for j in range(8)] + # 40-79
[f"r{i}{j}" for i in range(5) for j in range(8)] + # 80-119
[f"R{i}{j}" for i in range(8) for j in range(8)] + # 120-183
["g", "h", "l"]
)
name_string = ",".join(names)
@@ -27,49 +27,60 @@ class Tea3Model:
self.y_bits = [list(self.v[40 + i*8 : 40 + (i+1)*8 ]) for i in range(5)]
self.r_bits = [list(self.v[80 + i*8 : 80 + (i+1)*8 ]) for i in range(5)]
self.R_bits = [list(self.v[120 + i*8 : 120 + (i+1)*8]) for i in range(8)]
self.g = self.v[-1]
self.g = self.v[-3]
self.h = self.v[-2]
self.l = self.v[-1]
def _abstract_poly(self, poly, abstract_prefixes, abstract_var):
"""
Abstract all monomials involving intermediate ``abstract_prefixes`` variables.
For each polynomial, monomials containing any ``abstract_prefixes`` or ``abstract_var`` variable are replaced with a variable ``abstract_var``.
Monomials involving only other variables are kept unchanged.
"""
one = self.S.one()
zero = self.S.zero()
abstract_prefixes = set(abstract_prefixes)
def is_abstract_var(v):
name = str(v)
return name[0] in abstract_prefixes
result = zero
if poly.constant_coefficient():
result += one
for monom in poly:
vars_ = list(monom.variables())
if not vars_:
continue
if not any(is_abstract_var(v) for v in vars_):
result += monom
else:
kept_vars = [v for v in vars_ if not is_abstract_var(v)]
kept_monom = reduce(mul, kept_vars, one) if kept_vars else one
result += kept_monom * abstract_var
return result
def _abstract_vec(self, vec, abstract_prefixes, abstract_var):
return [self._abstract_poly(p, abstract_prefixes, abstract_var) for p in vec]
def _abstract_r(self):
self.r_bits = [self._abstract_vec(vec, {"r"}, self.h) for vec in self.r_bits]
self.x_bits = [self._abstract_vec(vec, {"r"}, self.h) for vec in self.x_bits]
self.R_bits = [self._abstract_vec(vec, {"r"}, self.h) for vec in self.R_bits]
def _abstract_x(self):
self.x_bits = [self._abstract_vec(vec, {"x"}, self.l) for vec in self.x_bits]
self.R_bits = [self._abstract_vec(vec, {"x"}, self.l) for vec in self.R_bits]
def _abstract_R(self):
"""
Abstract all monomials involving intermediate R variables.
self.R_bits = [self._abstract_vec(vec, {"R"}, self.g) for vec in self.R_bits]
For each polynomial in ``R_bits``, monomials containing any ``R`` or ``g`` variable are replaced with a variable ``g``.
Monomials involving only ``x``, ``y``, and ``r`` variables are kept unchanged.
"""
one = self.S.one()
zero = self.S.zero()
for i in range(8):
for j in range(8):
poly = self.R_bits[i][j]
groups = {}
pure_xyr = zero
const = one if bool(poly.constant_coefficient()) else zero
for monom in poly:
term_vars = monom.variables()
if not term_vars:
continue
xyr_vars = [v for v in term_vars if str(v)[0] in ('x', 'y', 'r')]
Rg_vars = [v for v in term_vars if str(v)[0] in ('R', 'g')]
xyr_mono = reduce(mul, (self.S(v) for v in xyr_vars), one)
xyr_key = frozenset(str(v) for v in xyr_vars)
if not Rg_vars:
pure_xyr += xyr_mono
else:
groups[xyr_key] = xyr_mono
result = pure_xyr + const
for xyr_key, xyr_mono in groups.items():
result += xyr_mono * self.g
self.R_bits[i][j] = result
def step(self, skip_abstract: bool = False):
def step(self, skip_abstract_R: bool = False, skip_abstract_r: bool = False, skip_abstract_x: bool = True):
R = self.R_bits.copy()
x = self.x_bits.copy()
r = self.r_bits.copy()
@@ -102,8 +113,12 @@ class Tea3Model:
self.R_bits[1] = R0
self.R_bits[0] = xor_vec(x0, xor_vec(R7, xor_vec(BP(R4), F32(R2, R1))))
if not skip_abstract:
if not skip_abstract_R:
self._abstract_R()
if not skip_abstract_x:
self._abstract_x()
if not skip_abstract_r:
self._abstract_r()
self.step_count += 1