Writeup for Seed me

Seed Me.md

Seed Me

"Seed Me" was supposed to be a variant of the Minecraft seed searches, where the game might use N rng outputs to flip a coin about unimportant things like "Should this rock have moss?" and then decide if something important should spawn or not. There's a vast amount of research on the Java LCG due to this, just not in the normal channels people get their papers from :)

The parameters were deliberately chosen to make it slightly out of bounds for naïve CVP/LLL, which means the solvers need to figure out another way to constraint the solution space. One way is to combine lattices and linear programming, such that we can get a bunch of bounds on the values. From there, it's possible to use the "Branch and Bound" approach to shrink the solution space. It has exponential run time, but with good constraints it's fairly fast.

A good video that explains the basics

Author solution uses the LattiCG library to accomplish this, although some also succeeded by prodding the parameters in LLL or even by letting Z3 run for a few hours.

import com.seedfinding.latticg.reversal.DynamicProgram;
import com.seedfinding.latticg.util.LCG;
import com.seedfinding.latticg.reversal.calltype.java.JavaCalls;

class Solve {
    public static void main(String[] args) {
        float lim = 7.331f*.1337f;
        int val = 2047;
        DynamicProgram device = DynamicProgram.create(LCG.JAVA);
        device.skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 1
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 2
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 3
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 4
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 5
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 6
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 7
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 8
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 9
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 10
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 11
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 12
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 13
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 14
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)) // 15
            .skip(val)
            .add(JavaCalls.nextFloat().greaterThan(lim)); // 16
        device.reverse().forEach(System.out::println); // Need to XOR with 0x5DEECE66D
    }
}

Run time is about 1 second, and it finds 79 valid solutions