#!/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())