228 lines
8.3 KiB
Python
228 lines
8.3 KiB
Python
#!/usr/bin/env python3
|
|
"""
|
|
Generate an SMT-LIB bit-vector query for reverse-searching slime chunk patterns.
|
|
|
|
This is an experiment, not a replacement for the CUDA brute-force scanner. It
|
|
uses an approximate nextInt(10) predicate with the Java rejection loop removed:
|
|
|
|
((next48 >> 17) % 10) == 0
|
|
|
|
The approximation is useful because it removes the rare retry branch and gives a
|
|
clean fixed one-step LCG constraint. Any model from this script should still be
|
|
verified with the exact Java nextInt(10) implementation before being trusted.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
import argparse
|
|
import pathlib
|
|
import re
|
|
import shutil
|
|
import subprocess
|
|
import sys
|
|
|
|
JAVA_MULT = 0x5DEECE66D
|
|
JAVA_ADD = 0xB
|
|
SLIME_XOR = 987234911
|
|
|
|
|
|
def bv(value: int, bits: int) -> str:
|
|
return f"(_ bv{value & ((1 << bits) - 1)} {bits})"
|
|
|
|
|
|
def signed_bv32(value: int) -> str:
|
|
return bv(value, 32)
|
|
|
|
|
|
def cell_order(n: int, mode: str) -> list[tuple[int, int]]:
|
|
cells = [(dx, dz) for dx in range(n) for dz in range(n)]
|
|
if mode == "all":
|
|
return cells
|
|
if mode == "corners":
|
|
return [(0, 0), (n - 1, 0), (0, n - 1), (n - 1, n - 1)]
|
|
if mode == "border":
|
|
return [(dx, dz) for dx, dz in cells if dx in (0, n - 1) or dz in (0, n - 1)]
|
|
if mode == "diagonal":
|
|
return [(i, i) for i in range(n)]
|
|
raise ValueError(f"unknown cell mode: {mode}")
|
|
|
|
|
|
def smt_prelude() -> str:
|
|
xor48 = bv(SLIME_XOR, 48)
|
|
mult48 = bv(JAVA_MULT, 48)
|
|
add48 = bv(JAVA_ADD, 48)
|
|
return f"""
|
|
(set-logic QF_BV)
|
|
|
|
(define-fun i32_to_i64 ((v (_ BitVec 32))) (_ BitVec 64)
|
|
((_ sign_extend 32) v))
|
|
|
|
(define-fun coordXTerm64 ((x (_ BitVec 32))) (_ BitVec 64)
|
|
(bvadd
|
|
(i32_to_i64 (bvmul (bvmul x x) {bv(4987142, 32)}))
|
|
(i32_to_i64 (bvmul x {bv(5947611, 32)}))))
|
|
|
|
(define-fun coordZTerm64 ((z (_ BitVec 32))) (_ BitVec 64)
|
|
(bvadd
|
|
(bvmul (i32_to_i64 (bvmul z z)) {bv(4392871, 64)})
|
|
(i32_to_i64 (bvmul z {bv(389711, 32)}))))
|
|
|
|
(define-fun coordTerm48 ((x (_ BitVec 32)) (z (_ BitVec 32))) (_ BitVec 48)
|
|
((_ extract 47 0) (bvadd (coordXTerm64 x) (coordZTerm64 z))))
|
|
|
|
(define-fun lcgNext48 ((state (_ BitVec 48))) (_ BitVec 48)
|
|
(bvadd (bvmul state {mult48}) {add48}))
|
|
|
|
(define-fun slimeApprox ((seed48 (_ BitVec 48)) (x (_ BitVec 32)) (z (_ BitVec 32))) Bool
|
|
(= (bvurem
|
|
((_ extract 47 17)
|
|
(lcgNext48
|
|
(bvxor (bvxor (bvadd seed48 (coordTerm48 x z)) {xor48}) {mult48})))
|
|
{bv(10, 31)})
|
|
{bv(0, 31)}))
|
|
"""
|
|
|
|
|
|
def generate(args: argparse.Namespace) -> str:
|
|
lines: list[str] = [smt_prelude()]
|
|
lines.append("(declare-const seed48 (_ BitVec 48))")
|
|
|
|
if args.seed_start is not None:
|
|
lines.append(f"(assert (bvuge seed48 {bv(args.seed_start, 48)}))")
|
|
if args.seed_end is not None:
|
|
lines.append(f"(assert (bvult seed48 {bv(args.seed_end, 48)}))")
|
|
|
|
if args.x is None:
|
|
lines.append("(declare-const chunkX (_ BitVec 32))")
|
|
lines.append(f"(assert (bvsge chunkX {signed_bv32(-args.radius)}))")
|
|
lines.append(f"(assert (bvsle chunkX {signed_bv32(args.radius)}))")
|
|
else:
|
|
lines.append(f"(define-fun chunkX () (_ BitVec 32) {signed_bv32(args.x)})")
|
|
|
|
if args.z is None:
|
|
lines.append("(declare-const chunkZ (_ BitVec 32))")
|
|
lines.append(f"(assert (bvsge chunkZ {signed_bv32(-args.radius)}))")
|
|
lines.append(f"(assert (bvsle chunkZ {signed_bv32(args.radius)}))")
|
|
else:
|
|
lines.append(f"(define-fun chunkZ () (_ BitVec 32) {signed_bv32(args.z)})")
|
|
|
|
cells = cell_order(args.n, args.cells)
|
|
if args.limit_cells is not None:
|
|
cells = cells[: args.limit_cells]
|
|
|
|
for dx, dz in cells:
|
|
lines.append(
|
|
"(assert (slimeApprox seed48 "
|
|
f"(bvadd chunkX {bv(dx, 32)}) "
|
|
f"(bvadd chunkZ {bv(dz, 32)})))"
|
|
)
|
|
|
|
lines.append("(check-sat)")
|
|
lines.append("(get-value (seed48 chunkX chunkZ))")
|
|
return "\n".join(lines) + "\n"
|
|
|
|
|
|
def parse_model(output: str) -> tuple[int | None, int | None, int | None]:
|
|
values: dict[str, int] = {}
|
|
for name, token in re.findall(r"\((seed48|chunkX|chunkZ)\s+(#x[0-9a-fA-F]+|\(_ bv\d+ \d+\))\)", output):
|
|
if token.startswith("#x"):
|
|
values[name] = int(token[2:], 16)
|
|
else:
|
|
match = re.match(r"\(_ bv(\d+) \d+\)", token)
|
|
if match:
|
|
values[name] = int(match.group(1))
|
|
|
|
def as_i32(value: int | None) -> int | None:
|
|
if value is None:
|
|
return None
|
|
value &= 0xFFFFFFFF
|
|
return value - 0x100000000 if value & 0x80000000 else value
|
|
|
|
return values.get("seed48"), as_i32(values.get("chunkX")), as_i32(values.get("chunkZ"))
|
|
|
|
|
|
def java_int_as_long(value: int) -> int:
|
|
value &= 0xFFFFFFFF
|
|
return value - 0x100000000 if value & 0x80000000 else value
|
|
|
|
|
|
def coord_term(x: int, z: int) -> int:
|
|
return (
|
|
java_int_as_long(x * x * 4987142)
|
|
+ java_int_as_long(x * 5947611)
|
|
+ java_int_as_long(z * z) * 4392871
|
|
+ java_int_as_long(z * 389711)
|
|
) & ((1 << 64) - 1)
|
|
|
|
|
|
def exact_slime(seed48: int, x: int, z: int) -> bool:
|
|
state = ((seed48 + coord_term(x, z)) ^ SLIME_XOR ^ JAVA_MULT) & ((1 << 48) - 1)
|
|
while True:
|
|
state = (state * JAVA_MULT + JAVA_ADD) & ((1 << 48) - 1)
|
|
bits = state >> 17
|
|
val = bits % 10
|
|
if bits - val + 9 <= 0x7FFFFFFF:
|
|
return val == 0
|
|
|
|
|
|
def verify(seed48: int, x: int, z: int, n: int) -> bool:
|
|
return all(exact_slime(seed48, x + dx, z + dz) for dx in range(n) for dz in range(n))
|
|
|
|
|
|
def main() -> int:
|
|
parser = argparse.ArgumentParser(description="Generate/run an SMT reverse search for slime chunk squares.")
|
|
parser.add_argument("-n", type=int, default=4, help="square size to constrain")
|
|
parser.add_argument("-r", "--radius", type=int, default=128, help="signed coordinate bound when x/z are not fixed")
|
|
parser.add_argument("--x", type=int, help="fix left x coordinate")
|
|
parser.add_argument("--z", type=int, help="fix top z coordinate")
|
|
parser.add_argument("-s", "--seed-start", type=int, help="inclusive low-48 seed bound")
|
|
parser.add_argument("-e", "--seed-end", type=int, help="exclusive low-48 seed bound")
|
|
parser.add_argument("--cells", choices=["all", "border", "corners", "diagonal"], default="all")
|
|
parser.add_argument("--limit-cells", type=int, help="only assert the first k cells from the selected order")
|
|
parser.add_argument("-o", "--output", default="exp/slime_reverse.smt2", help="SMT-LIB output path")
|
|
parser.add_argument("--run", action="store_true", help="run the solver after writing the query")
|
|
parser.add_argument("--solver", default="z3", help="solver executable, e.g. z3, boolector, cvc5")
|
|
parser.add_argument("--verify", action="store_true", help="verify a SAT model with exact Java nextInt(10)")
|
|
args = parser.parse_args()
|
|
|
|
if args.n <= 0 or args.radius < 0:
|
|
parser.error("n must be positive and radius must be non-negative")
|
|
if args.seed_start is not None and args.seed_end is not None and args.seed_start >= args.seed_end:
|
|
parser.error("seed-start must be less than seed-end")
|
|
|
|
output_path = pathlib.Path(args.output)
|
|
output_path.parent.mkdir(parents=True, exist_ok=True)
|
|
output_path.write_text(generate(args), encoding="utf-8")
|
|
print(f"wrote {output_path}")
|
|
|
|
if not args.run:
|
|
print(f"run with: {args.solver} {output_path}")
|
|
return 0
|
|
|
|
solver = shutil.which(args.solver)
|
|
if solver is None:
|
|
print(f"solver not found: {args.solver}", file=sys.stderr)
|
|
return 2
|
|
|
|
completed = subprocess.run([solver, str(output_path)], text=True, capture_output=True, check=False)
|
|
if completed.stdout:
|
|
print(completed.stdout, end="")
|
|
if completed.stderr:
|
|
print(completed.stderr, file=sys.stderr, end="")
|
|
if completed.returncode != 0:
|
|
return completed.returncode
|
|
|
|
first_line = completed.stdout.splitlines()[0].strip() if completed.stdout.splitlines() else ""
|
|
if args.verify and first_line == "sat":
|
|
seed48, x, z = parse_model(completed.stdout)
|
|
if seed48 is None or x is None or z is None:
|
|
print("could not parse model for exact verification", file=sys.stderr)
|
|
return 3
|
|
ok = verify(seed48, x, z, args.n)
|
|
print(f"exact_verify seed48={seed48} x={x} z={z} n={args.n}: {'pass' if ok else 'fail'}")
|
|
|
|
return 0
|
|
|
|
|
|
if __name__ == "__main__":
|
|
raise SystemExit(main())
|