rakovskij-stanislav.github.io

Назад

Так вот, программа состоит из единого блока на скрэтче, который можно логически поделить на несколько частей:

1. Блок первоначальной подготовки: очищаются массивы nums и binums, массив alpha заполняется значениями a-z, отчет начинается с единицы:
2. У нас спрашивается флаг, проверяется, что его длина равна 29 и все значения принадлежат массиву alpha.
3. Значения флага конвертируются в числа от 1 до 26 согласно порядковому номеру.
4. Заполняются значения массива binums по формуле (если считать с нуля):

   b[i] = a[i]*27+ a[-i-1]
   

5. Проверяется, удовлетворяет ли массив binums тридцати условиям вида:

   const[i] == b[k]*b[l] (+|-) b[s]*b[t]
   

   

6. Если всё ок, то из массива alpha генерируется флаг и выводится пользователю.

Для решения таска воспользуемся z3

from z3 import *

s = Solver()

v = IntVector("a", 29)

for iv in v:
    s.add(iv>=1)
    s.add(iv<=26)

b = IntVector("b", 15)

for i in range(15):
    s.add(b[i] == v[i]*27+ v[-i-1])

# констрейнты, заботливо перепечатанные двумя участницами команды Похитителей котят,
# ибо их реально много

s.add(51483 == b[3]*b[5]+b[10]*b[11]) 
s.add(1398 == b[0]*b[1]-b[13]*b[14]) 
s.add(284699 == b[0]*b[2]+b[6]*b[14]) 
s.add(103842 == b[1]*b[3]+b[8]*b[12]) 
s.add(45888 == b[1]*b[8]+b[11]*b[14]) 
s.add(262607 == b[0]*b[2]-b[9]*b[14]) 
s.add(-94878 == b[3]*b[9]-b[10]*b[12]) 
s.add(30933 == b[1]*b[3]+b[5]*b[7]) 
s.add(61731 == b[1]*b[3]+b[6]*b[7]) 
s.add(108513 == b[3]*b[7]+b[10]*b[12]) 
s.add(101403 == b[3]*b[5]+b[10]*b[12]) 
s.add(38466 == b[1]*b[4]-b[9]*b[12]) 
s.add(-42775 == b[0]*b[3]-b[4]*b[11]) 
s.add(-966 == b[6]*b[9]-b[11]*b[14]) 
s.add(14298 == b[1]*b[3]+b[11]*b[14]) 
s.add(111924 == b[0]*b[8]-b[10]*b[12]) 
s.add(-20322 == b[1]*b[2]-b[7]*b[12]) 
s.add(45551 == b[4]*b[5]-b[9]*b[12])
s.add(123890 == b[0]*b[2]-b[4]*b[7]) 
s.add(118902 == b[0]*b[9]+b[10]*b[12]) 
s.add(-73678 == b[0]*b[1]-b[6]*b[13]) 
s.add(37182 == b[0]*b[1]-b[11]*b[14]) 
s.add(130378 == b[1]*b[5]+b[6]*b[13]) 
s.add(62599 == b[5]*b[2]+b[9]*b[12]) 
s.add(-11208 == b[1]*b[8]-b[10]*b[11]) 
s.add(-97720 == b[3]*b[2]-b[4]*b[6]) 
s.add(17772 == b[5]*b[8]-b[9]*b[13]) 
s.add(-98827 == b[6]*b[2]-b[10]*b[13]) 
s.add(156359 == b[4]*b[5]+b[7]*b[10]) 
s.add(-37566 == b[6]*b[9]-b[10]*b[11])

if s.check() == sat:
    keys = "abcdefghijklmnopqrstuvwxyz" # from string import printable
    m = s.model()
    for i in range(29):
        print(keys[ int(m[v[i]].__str__()) -1], end="")
    print()
        
else:
    print("unsat")

В итоге получаем ключ: scratchinanditchinforreversin

Скармливаем его медузке.

Назад