From 1df3275518884b5561a0b3ea588f0f8c52eb2e86 Mon Sep 17 00:00:00 2001 From: Mingliang Zeng Date: Fri, 6 Nov 2020 20:26:38 +0800 Subject: [PATCH] theorem prover writeup --- official/超精巧的数字论证器/README.md | 53 +++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/official/超精巧的数字论证器/README.md b/official/超精巧的数字论证器/README.md index 269dd6a..c28227e 100644 --- a/official/超精巧的数字论证器/README.md +++ b/official/超精巧的数字论证器/README.md @@ -1 +1,54 @@ # 超精巧的数字论证器 + +写一个简单的搜索算法可以解决数字较小的情况。 + +但是稍作尝试就会发现，当给定的数字较大时（例如 `100000`），就很难用表达式凑出接近这个大小的值。 + +稍作分析可以发现，这是因为所有给定的二元运算符一般都会使表达值的值变小，也就是说 `a+b a-b a*b a/b a%b a^b a&b a|b` 不会比 `ab` （不插入二元运算符）的值更大。所以，如果不使用一元运算符，表达式能凑出的最大值就是 `114514`，其次就是 `114*514=58596`。它们之间的值都不能被凑出来。由于需要连续答对 32 题才能获得 flag，所以必须解决这些情况。 + +那么突破口显然就在一元运算符 `+-~` 了。`+` 运算符显然没有用处，考虑 `-` 和 `~` 即可。 + +稍作研究就可以发现一个性质：`-~x=x+1` 对于任意 `x` 都成立。**这个性质与计算机中有符号整数的二进制补码表示有关。** + +一元运算符可以不断嵌套。一个朴素的方法就是嵌套 `-~` 来不断地将表达式的值增加 1（反过来 `~-` 可以减少 1），最终得到目标值，但这样的话表达式就太长了，无法符合题目要求。 + +表达式中有 6 个数字，要好好利用它们才行。一个办法就是按照十进制的方式来凑，即 `given_number = (((((((0+a)*10+b)*10+c)*10+d)*10)+e)*10)+f` ，其中 `a b c d e f` 为 0 到 9 之间的整数。表达式中的值 `0 10 10 10 10 10` 可以分别利用 `1 1 4 5 1 4` 与嵌套 `~-` 来凑出，而 `+a +b +c +d +e +f` 可以直接利用嵌套 `~-` 来实现（不需要使用其它数字）。这样表达式就可以符合标准，而且长度不会超过限制了。 + +解题脚本（需要安装 pwntools）： + +```python +#!/usr/bin/env python3 + + +import pwn + + +def getans(number): + jz = 10 + s = [] + e = "114514" + for c in e[:1]: + s.append("~-" * (int(c)) + c) # value is zero + for c in e[1:]: + s.append("-~" * (jz - int(c)) + c) # value is jz + ans = "" + for i in range(len(e)): + digit = (number // (jz ** (len(e) - 1 - i))) % jz + ans = "(" + ans + "*" + s[i] + ")" if i > 0 else s[i] + ans = "-~" * digit + ans + return ans + + +conn = pwn.remote('202.38.93.111', 10241) # connect to the server +token = open('token', 'r').read() # read the token +conn.sendlineafter('Please input your token:', token) # send the token + +for _ in range(32): + number = int(conn.recvuntil('=').decode('utf-8').split()[-2]) # get the number + ans = getans(number) # calculate the answer + conn.sendline(ans) # send the answer + print(str(number) + ' = ' + ans + ' ' + conn.recvline().decode('utf-8').strip()) # print the result + +conn.interactive() # print the flag +``` +