Skip to content

Instantly share code, notes, and snippets.

@taotao54321

taotao54321/game.py

Created October 20, 2024 18:51
Show Gist options
  • Save taotao54321/2d7033484b92b298180de4794b6b39df to your computer and use it in GitHub Desktop.
Save taotao54321/2d7033484b92b298180de4794b6b39df to your computer and use it in GitHub Desktop.
Download ZIP
NES Wizardry (J): solver for save glitch TAS
Raw
game.py
# ゲームロジック関連。
import z3
# 8bit の BitVecVal を返す。
def BYTE(value):
return z3.BitVecVal(value, 8)
# BitVec 変数の範囲制約を返す。
def bitvec_minmax(bv: z3.BitVecRef, min_, max_):
return z3.And(z3.UGE(bv, min_), z3.ULE(bv, max_))
# 暗号化/復号におけるバイトの変換。
#
# これは対称な変換である。つまり、2 回行うと元に戻る。
def scramble(b):
return ~z3.RotateLeft(b, 4)
# 正当な新規冒険者の制約を返す。
#
# NOTE: 以下の制約は緩和できそう:
#
# * 酒場外フラグ: 仲間に加えてセーブするだけで 0x80 にできる
# * 年齢 (週): 馬小屋に泊まるだけで +1 できる
def new_hero_is_ok(hero):
scenario_id = hero[0x00]
xl_hi = hero[0x23]
xl_lo = hero[0x24]
status = hero[0x25]
ac = hero[0x28]
poison = hero[0x61]
badges = hero[0x62]
unused = hero[0x63:][:13]
# シナリオIDは 1 固定。
scenario_id_ok = scenario_id == 1
# レベルは 1 固定。
xl_ok = z3.And(xl_hi == 0, xl_lo == 1)
# 状態は OK 固定。
status_ok = status == 0
# ACは 10 固定。
ac_ok = ac == 10
# 毒値は 0 固定。
poison_ok = poison == 0
# 称号は 0 固定。
badges_ok = badges == 0
# 未使用領域はゼロクリアされている。
unused_ok = z3.And([b == 0 for b in unused])
return z3.And(
scenario_id_ok,
name_is_ok(hero),
build_is_ok(hero),
gold_is_ok(hero),
xp_is_ok(hero),
hp_is_ok(hero),
xl_ok,
status_ok,
age_is_ok(hero),
ac_ok,
spell_is_ok(hero),
inventory_is_ok(hero),
place_is_ok(hero),
poison_ok,
badges_ok,
unused_ok,
checksums_is_ok(hero),
crc_is_ok(hero),
)
# 冒険者の名前に関する制約を返す。
def name_is_ok(hero):
name_len = hero[0x01]
name = hero[0x02:][:8]
# 名前長は 1..=8。
name_len_ok = bitvec_minmax(name_len, 1, 8)
# 名前内のバイトは、名前長の範囲内では正しいバイトでなければならず、
# 範囲外は末尾まで空白 (0x24) パディングされていなければならない。
name_ok = z3.And([
z3.If(z3.UGT(name_len, i), name_byte_is_ok(name[i]), name[i] == 0x24) for i in range(8)
])
return z3.And(name_len_ok, name_ok)
# 冒険者の名前内のバイトに関する制約を返す。
def name_byte_is_ok(b):
return z3.Or(
z3.ULE(b, 0x24),
b == 0x2A,
b == 0x2B,
b == 0x2D,
b == 0x2E,
b == 0x30,
b == 0x31,
b == 0x32,
bitvec_minmax(b, 0x34, 0x63),
bitvec_minmax(b, 0x65, 0x9F),
)
# 新規冒険者のビルドに関する制約を返す。
def build_is_ok(hero):
race = hero[0x0A]
clas = hero[0x0B]
alignment = hero[0x0C]
stats = hero[0x0D:][:6]
# 種族, 職業, 性格の値が正しくなければならない (新規冒険者は君主/忍者にはなれないことに注意)。
race_ok = z3.ULE(race, 4)
class_ok = z3.ULE(clas, 5)
alignment_ok = z3.ULE(alignment, 2)
# 全ての特性値は 18 以下でなければならない。
stats_ok = z3.And([z3.ULE(stat, 18) for stat in stats])
# 値の組み合わせに関する制約を全て満たさなければならない。
return z3.And(
race_ok,
class_ok,
alignment_ok,
stats_ok,
race_stats_is_ok(race, stats),
class_alignment_is_ok(clas, alignment),
class_stats_is_ok(clas, stats),
)
# 種族と特性値の組み合わせの制約を返す。
def race_stats_is_ok(race, stats):
# 種族の基本特性値を得る。
stats_min = [race_basic_stat(race, i) for i in range(6)]
# 全ての特性値は種族の基本値以上でなければならない。
min_ok = z3.And([z3.UGE(stats[i], stats_min[i]) for i in range(6)])
# ボーナスポイントがゲーム内で出現しうる値でなければならない。
bp = z3.BitVecVal(0, 8)
for i in range(6):
bp += stats[i] - stats_min[i]
bp_ok = bonuspoint_is_ok(bp)
return z3.And(min_ok, bp_ok)
# 種族の特性値の基本値を返す。
def race_basic_stat(race, stat_idx):
return [
# 人 エ ド ノ ホ
z3.If(race == 0, BYTE(8), z3.If(race == 1, BYTE( 7), z3.If(race == 2, BYTE(10), z3.If(race == 3, BYTE( 7), z3.If(race == 4, BYTE( 5), BYTE(0)))))),
z3.If(race == 0, BYTE(8), z3.If(race == 1, BYTE(10), z3.If(race == 2, BYTE( 7), z3.If(race == 3, BYTE( 7), z3.If(race == 4, BYTE( 7), BYTE(0)))))),
z3.If(race == 0, BYTE(5), z3.If(race == 1, BYTE(10), z3.If(race == 2, BYTE(10), z3.If(race == 3, BYTE(10), z3.If(race == 4, BYTE( 7), BYTE(0)))))),
z3.If(race == 0, BYTE(8), z3.If(race == 1, BYTE( 6), z3.If(race == 2, BYTE(10), z3.If(race == 3, BYTE( 8), z3.If(race == 4, BYTE( 6), BYTE(0)))))),
z3.If(race == 0, BYTE(8), z3.If(race == 1, BYTE( 9), z3.If(race == 2, BYTE( 5), z3.If(race == 3, BYTE(10), z3.If(race == 4, BYTE(10), BYTE(0)))))),
z3.If(race == 0, BYTE(9), z3.If(race == 1, BYTE( 6), z3.If(race == 2, BYTE( 6), z3.If(race == 3, BYTE( 7), z3.If(race == 4, BYTE(15), BYTE(0)))))),
][stat_idx]
# ゲーム内で出現しうるボーナスポイントの制約を返す。
def bonuspoint_is_ok(bp):
return z3.Or(
bitvec_minmax(bp, 5, 9),
bitvec_minmax(bp, 15, 19),
bp == 25,
bp == 29
)
# 職業と性格の組み合わせの制約を返す。
def class_alignment_is_ok(clas, alignment):
return z3.If(clas == 0, z3.BoolVal(True), # 戦
z3.If(clas == 1, z3.BoolVal(True), # 魔
z3.If(clas == 2, z3.Or(alignment == 0, alignment == 2), # 僧
z3.If(clas == 3, z3.Or(alignment == 1, alignment == 2), # 盗
z3.If(clas == 4, z3.Or(alignment == 0, alignment == 2), # 司
z3.If(clas == 5, z3.Or(alignment == 0, alignment == 1), # 侍
z3.BoolVal(False)))))))
# 職業と特性値の組み合わせの制約を返す。
def class_stats_is_ok(clas, stats):
return z3.If(clas == 0, z3.UGE(stats[0], 11), # 戦
z3.If(clas == 1, z3.UGE(stats[1], 11), # 魔
z3.If(clas == 2, z3.UGE(stats[2], 11), # 僧
z3.If(clas == 3, z3.UGE(stats[4], 11), # 盗
z3.If(clas == 4, z3.And(z3.UGE(stats[1], 12), # 司
z3.UGE(stats[2], 12)),
z3.If(clas == 5, z3.And(z3.UGE(stats[0], 15), # 侍
z3.UGE(stats[1], 11),
z3.UGE(stats[2], 10),
z3.UGE(stats[3], 14),
z3.UGE(stats[4], 10)),
z3.BoolVal(False)))))))
# 新規冒険者の所持金に関する制約を返す。
def gold_is_ok(hero):
gold = hero[0x13:][:6]
# 金は 100..=199 でなければならない (12 桁 packed BCD, 上位桁が先)。
conds = [b == 0 for b in gold[:4]]
conds.append(gold[4] == 0x01)
conds.append(is_packed_bcd(gold[5]))
return z3.And(conds)
# 新規冒険者の経験値に関する制約を返す。
def xp_is_ok(hero):
xp = hero[0x19:][:6]
# 経験値は 0 でなければならない (12 桁 packed BCD, 上位桁が先)。
return z3.And([b == 0 for b in xp])
# packed BCD バイトの制約を返す。
def is_packed_bcd(b: z3.BitVecRef):
lo_ok = z3.ULE(b & 0x0F, 9)
hi_ok = z3.ULE(z3.LShR(b, 4), 9)
return z3.And(lo_ok, hi_ok)
# 新規冒険者のHPに関する制約を返す。
def hp_is_ok(hero):
clas = hero[0x0B]
hp_hi = hero[0x1F]
hp_lo = hero[0x20]
maxhp_hi = hero[0x21]
maxhp_lo = hero[0x22]
# 現在HP/最大HPともに上位バイトは 0。
hi_ok = z3.And(hp_hi == 0, maxhp_hi == 0)
# HPの初期値の範囲は職業依存。
lo_ok = z3.If(clas == 0, bitvec_minmax(hp_lo, 8, 14),
z3.If(clas == 1, bitvec_minmax(hp_lo, 2, 6),
z3.If(clas == 2, bitvec_minmax(hp_lo, 6, 12),
z3.If(clas == 3, bitvec_minmax(hp_lo, 4, 8),
z3.If(clas == 4, bitvec_minmax(hp_lo, 4, 8),
z3.If(clas == 5, bitvec_minmax(hp_lo, 12, 18),
z3.BoolVal(False)))))))
return z3.And(
hi_ok,
lo_ok,
hp_lo == maxhp_lo, # 現在HPと最大HPは等しい。
)
# 新規冒険者の年齢に関する制約を返す。
def age_is_ok(hero):
age_year = hero[0x26]
age_week = hero[0x27]
# 年齢の初期値は 14..=16 年 24 週。
return z3.And(
bitvec_minmax(age_year, 14, 16),
age_week == 24,
)
# 新規冒険者の初期習得呪文に関する制約を返す。
def spell_is_ok(hero):
clas = hero[0x0B]
iq = hero[0x0E]
piety = hero[0x0F]
mag_mps = hero[0x29:][:7]
pri_mps = hero[0x30:][:7]
mag_maxmps = hero[0x37:][:7]
pri_maxmps = hero[0x3E:][:7]
spell_mask = hero[0x45:][:7]
# 呪文LV2以上は全て未習得かつMP 0。
others_ok = z3.And(
z3.And([value == 0 for value in mag_mps[1:]]),
z3.And([value == 0 for value in pri_mps[1:]]),
z3.And(
spell_mask[1] == 0,
spell_mask[4] == 0,
spell_mask[5] == 0,
spell_mask[6] == 0,
),
)
# 初期習得呪文は職業と特性値に依存する。
lv1_ok = z3.If(z3.Or(clas == 1, clas == 4), mag_bis_spell_is_ok(iq, mag_mps[0], pri_mps[0], spell_mask),
z3.If(clas == 2, pri_spell_is_ok(piety, mag_mps[0], pri_mps[0], spell_mask),
others_spell_is_ok(mag_mps[0], pri_mps[0], spell_mask)))
# 全ての最大MPは現在MPに等しい。
maxmps_ok = z3.And(
z3.And([mag_mps[i] == mag_maxmps[i] for i in range(7)]),
z3.And([pri_mps[i] == pri_maxmps[i] for i in range(7)]),
)
return z3.And(others_ok, lv1_ok, maxmps_ok)
# 魔/司の初期習得呪文に関する制約を返す。
def mag_bis_spell_is_ok(iq, mag1_mp, pri1_mp, spell_mask):
# 魔LV1呪文を (知恵)/6 個覚える (KATINO, HALITO, DUMAPIC の順)。
# 知恵は 11 以上のはずなので、少なくとも 1 個は覚える。
mag_ok = z3.If(iq == 18, z3.And(mag1_mp == 3, spell_mask[0] == 0b1101),
z3.If(z3.UGE(iq, 12), z3.And(mag1_mp == 2, spell_mask[0] == 0b0101),
z3.And(mag1_mp == 1, spell_mask[0] == 0b0100)))
# 僧LV1呪文は覚えない。
pri_ok = z3.And(pri1_mp == 0, spell_mask[2] == 0, spell_mask[3] == 0)
return z3.And(mag_ok, pri_ok)
# 僧の初期習得呪文に関する制約を返す。
def pri_spell_is_ok(piety, mag1_mp, pri1_mp, spell_mask):
# 魔LV1呪文は覚えない。
mag_ok = z3.And(mag1_mp == 0, spell_mask[0] == 0)
# 僧LV1呪文を (信仰心)/6 個覚える (DIOS, KALKI, MILWA の順)。
pri_ok = z3.If(piety == 18, z3.And(pri1_mp == 3, spell_mask[2] == 0b01100000, spell_mask[3] == 1),
z3.If(z3.UGE(piety, 12), z3.And(pri1_mp == 2, spell_mask[2] == 0b01100000, spell_mask[3] == 0),
z3.And(pri1_mp == 1, spell_mask[2] == 0b01000000, spell_mask[3] == 0)))
return z3.And(mag_ok, pri_ok)
# 初期習得呪文のない職業 (魔/僧/司 以外) に関する制約を返す。
def others_spell_is_ok(mag1_mp, pri1_mp, spell_mask):
# 魔LV1呪文は覚えない。
mag_ok = z3.And(mag1_mp == 0, spell_mask[0] == 0)
# 僧LV1呪文は覚えない。
pri_ok = z3.And(pri1_mp == 0, spell_mask[2] == 0, spell_mask[3] == 0)
return z3.And(mag_ok, pri_ok)
# 新規冒険者のインベントリに関する制約を返す。
def inventory_is_ok(hero):
item_flags = hero[0x4C:][:8]
item_ids = hero[0x54:][:8]
inventory_len = hero[0x5C]
# インベントリは空。
return z3.And(
z3.And([item_flag == 0 for item_flag in item_flags]),
z3.And([item_id == 0 for item_id in item_ids]),
inventory_len == 0,
)
# 新規冒険者の現在位置に関する制約を返す。
def place_is_ok(hero):
out_of_tavern = hero[0x5D]
place_x = hero[0x5E]
place_y = hero[0x5F]
place_depth = hero[0x60]
# 酒場内におり、座標は (0, 0, 0) となっている。
return z3.And(
out_of_tavern == 0,
place_x == 0,
place_y == 0,
place_depth == 0,
)
# 新規冒険者のチェックサム配列に関する制約を返す。
def checksums_is_ok(hero):
cksums = hero[0x70:][:14]
return z3.And([wizardry_checksum(hero[8*i:][:8]) == cksums[i] for i in range(14)])
# 原作のチェックサム (8 バイト単位)。
def wizardry_checksum(buf):
assert len(buf) == 8
cksum = z3.BitVecVal(8, 8)
carry = z3.BoolVal(False)
for b in buf:
cksum, carry = adc(cksum, b, carry)
return cksum
# 6502 の adc。
def adc(lhs, rhs, carry):
sum_ = z3.ZeroExt(1, lhs) + z3.ZeroExt(1, rhs)
sum_ += z3.If(carry, z3.BitVecVal(1, 9), z3.BitVecVal(0, 9))
sum_res = z3.Extract(7, 0, sum_)
carry_res = z3.LShR(sum_, 8) != 0
return sum_res, carry_res
# 新規冒険者の CRC に関する制約を返す。
def crc_is_ok(hero):
return wizardry_crc(hero) == 0
# 原作の CRC。
def wizardry_crc(hero):
assert len(hero) == 0x80
crc = ((z3.ZeroExt(8, hero[0]) << 8) | (z3.ZeroExt(8, hero[1]))) ^ 0xFFFF
for b in hero[2:]:
for i in range(8):
carry = z3.LShR(crc, 15) != 0
crc = z3.If(carry, (crc << 1) ^ 0x1021, crc << 1)
crc ^= z3.ZeroExt(8, b)
return crc
Raw
solve.py
#!/usr/bin/env python3
# FC Wizardry #1 save glitch 探索用スクリプト
#
# アイテム所持数 0xFF の冒険者構造体バックアップを捏造しうる冒険者構造体を探索する。
# サブフレームリセットを用いてバックアップの部分的な暗号化/復号を繰り返すことで「正当」なバックアップが作れる。
#
# 結果はカレントディレクトリの以下のファイルに書き出される:
#
# * orig.bin - 元となる冒険者構造体
# * fake.bin - 捏造後の「正当」な冒険者構造体
import z3
import game
def main():
# 元の平文。
orig = [z3.BitVec(f"orig{i}", 8) for i in range(0x80)]
# 偽平文。
fake = orig_to_fake(orig)
solver = z3.Solver()
solver.add(orig_is_ok(orig))
solver.add(fake_is_ok(fake))
if solver.check() == z3.sat:
print("SAT")
else:
print("UNSAT")
return
model = solver.model()
fs_write("orig.bin", model_get_hero(model, orig))
fs_write("fake.bin", model_get_hero(model, fake))
# 元の平文を偽平文に変換する規則。
def orig_to_fake(orig):
fake = [None] * 0x80
# NOTE: これが 0x05..=0x09 あたりだと解けるっぽい。
end0 = 0x05
# シナリオID〜名前をそのままコピー。
# これらが暗号化され、チェックサム[6..=13], CRC となる。
# NOTE: この境界を 1 バイト手前にしたら解けた!ので、上の end0 で調整するようにした。
for i in range(0, end0):
fake[i] = orig[i]
fake[0x7F - i] = game.scramble(orig[i])
# NOTE: UNSAT を避けるため、ここの境界をいろいろ試している。
end1 = 0x10
# 〜チェックサム[0..=5] をそのままコピー。
# これらが暗号化され、種族〜となる。
for i in range(end0, end1):
fake[0x7F - i] = orig[0x7F - i]
fake[i] = game.scramble(orig[0x7F - i])
# 〜最大HPをそのままコピー。
# これらが暗号化され、酒場フラグ〜となる。
for i in range(end1, 0x23):
fake[i] = orig[i]
fake[0x7F - i] = game.scramble(orig[i])
# NOTE: UNSAT を避けるため、ここの境界をいろいろ試している。
end2 = 0x5C
# レベル〜境界をそのままコピー。
for i in range(0x23, end2):
fake[i] = orig[i]
# 境界〜アイテム個数はレベル上位バイトを暗号化した値とする。
for i in range(end2, 0x5D):
fake[i] = game.scramble(orig[0x7F - i])
return fake
# 元の平文についての制約を返す。
def orig_is_ok(orig):
hp_lo = orig[0x20]
# 元の平文は正当な新規冒険者でなければならない。
new_hero_ok = game.new_hero_is_ok(orig)
# 酒場フラグを false にするため、HPは 8 以上でなければならない。
hp_ok = z3.UGE(hp_lo, 8)
return z3.And(
new_hero_ok,
hp_ok,
)
# 偽平文についての制約を返す。
def fake_is_ok(fake):
cksums = fake[0x70:][:14]
# チェックサム配列が正しくなければならない。
checksums_ok = z3.And([game.wizardry_checksum(fake[8*i:][:8]) == cksums[i] for i in range(14)])
# CRC が正しくなければならない。
crc_ok = game.wizardry_crc(fake) == 0
# TODO: できれば名前などに魔除けのアイテムIDを含んでいてほしい。
#amulet_addrs = list(range(0x00, 0x10)) + list(range(0x61, 0x70))
#solver.add(z3.Or(list(map(lambda addr: fake[addr] == 0x5E, amulet_addrs))))
return z3.And(
checksums_ok,
crc_ok,
)
# モデル内の冒険者構造体をバイト列として得る。
def model_get_hero(model, hero):
assert len(hero) == 0x80
return bytes([model.eval(b).as_long() for b in hero])
def fs_write(path, buf):
open(path, "wb").write(buf)
main()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment