LA Overworld Legend Group Seed Solver.cs

void Main()
{
    // Files for verification; needs at least the first one and another one within the next 4.
	// Link the folder that your 2 Pokémon are in.
    var files = Directory.EnumerateFiles(@"C:\Users\Crowley\Mons", "*.PA8", SearchOption.TopDirectoryOnly);
    List<PA8> data = new();

    foreach (var file in files)
        data.Add(new PA8(File.ReadAllBytes(file)));

    var entities = data.ToArray();
    var mon_ECs = entities.Select(z => z.EncryptionConstant).ToArray();

    for (int i = 0; i < entities.Length; i++)
    {
        var entity = entities[i];
        Console.WriteLine($"Checking {entity.FileName}");

        var matches = GetAllSeeds(entity);
        foreach (var match in matches)
        {
            Console.WriteLine($"Pokemon Seed: {match:x16}\n");
            var gen_seed_matches = FindPotentialGenSeeds(match);
            foreach (var gen_match in gen_seed_matches)
            {
                Console.WriteLine($"-Generator Seed: {gen_match:x16}");
                var groupSeed = GetGroupSeed(gen_match);
                Console.WriteLine($"-Group Seed: {groupSeed:x16}\n");
                if (!IsValidGroupSeed(groupSeed, mon_ECs))
                    continue;
                Console.WriteLine($"Found a matching group seed: {groupSeed:x16}");
                return;
            }
        }
    }
}

private static readonly Context ctx = new(new Dictionary<string, string> { { "model", "true" } });

/// <summary>
/// Middle level seed calculation for the Generator Seed
/// </summary>
/// <param name="seed">Bottom level Entity seed.</param>
[MethodImpl(MethodImplOptions.AggressiveInlining)]
public static IEnumerable<ulong> FindPotentialGenSeeds(ulong seed)
{
    var exp = CreateGenSeedModel(seed);

    // Z3 is a theorem prover, and only proves if the model can be solved.
    // To yield multiple possible values from the expression, we must re-evaluate with added constraints.
    // Add each previously valid result as an "and this must not be a result".
    // Yield until no results found.
    while (Check(exp) is { } m)
    {
        foreach (var kvp in m.Consts) // should only be 1
        {
            var tmp = (BitVecNum)kvp.Value;
            var possible = tmp.UInt64;
            yield return possible;

            // Force the model to ignore the above result for s0, so we may get a new result if any.
            var constraint = ctx.MkNot(ctx.MkEq(GenSeedResult, tmp));
            exp = ctx.MkAnd(exp, constraint);
        }
    }
}

private static readonly BitVecExpr GenSeedResult = ctx.MkBVConst("s0", 64);
private static readonly BitVecExpr GenSeedExpression = GetBaseGenSeedModel();

[MethodImpl(MethodImplOptions.AggressiveInlining)]
private static BoolExpr CreateGenSeedModel(ulong seed)
{
    var real_seed = ctx.MkBV(seed, 64);
    return ctx.MkEq(real_seed, GenSeedExpression);
}

[MethodImpl(MethodImplOptions.AggressiveInlining)]
private static BitVecExpr GetBaseGenSeedModel()
{
    BitVecExpr s0 = GenSeedResult;
    BitVecExpr s1 = ctx.MkBV(Xoroshiro128Plus.XOROSHIRO_CONST, 64);

    // var slotRand = ctx.MkBVAdd(s0, s1);
    s1 = ctx.MkBVXOR(s0, s1);
    var tmp = ctx.MkBVRotateLeft(24, s0);
    var tmp2 = ctx.MkBV(1 << 16, 64);
    s0 = ctx.MkBVXOR(tmp, ctx.MkBVXOR(s1, ctx.MkBVMul(s1, tmp2)));
    s1 = ctx.MkBVRotateLeft(37, s1);
    return ctx.MkBVAdd(s0, s1); // genseed
    // no rot/xor needed, the add result is enough.
}

[MethodImpl(MethodImplOptions.AggressiveInlining)]
private static Model Check(BoolExpr cond)
{
    Solver solver = ctx.MkSolver();
    solver.Assert(cond);
    Status q = solver.Check();
    if (q != Status.SATISFIABLE)
        return null;
    return solver.Model;
}
    
[MethodImpl(MethodImplOptions.AggressiveInlining)]
public static ulong GetGroupSeed(ulong seed)
{
    return unchecked(seed - Xoroshiro128Plus.XOROSHIRO_CONST);
}

[MethodImpl(MethodImplOptions.AggressiveInlining)]
private static bool IsValidGroupSeed(ulong seed, ReadOnlySpan<uint> ecs)
{
    int matched = 0;

    var rng = new Xoroshiro128Plus(seed);
    for (int count = 0; count < 4; count++)
    {
        var genseed = rng.Next();
        _ = rng.Next(); // unknown

        var slotrng = new Xoroshiro128Plus(genseed);
        _ = slotrng.Next(); // slot
        var mon_seed = slotrng.Next();
     // _ = slotrng.Next(); // level

        var monrng = new Xoroshiro128Plus(mon_seed);
        var ec = (uint)monrng.NextInt();

        var index = ecs.IndexOf(ec);
        if (index != -1)
            matched++;

		var newseed = rng.Next();
		rng = new Xoroshiro128Plus(newseed);
    }
    return matched == ecs.Length;
}

[MethodImpl(MethodImplOptions.AggressiveInlining)]
private static BitVecExpr AdvanceSymbolicNext(Context ctx, ref BitVecExpr s0, ref BitVecExpr s1)
{
    var and_val = ctx.MkBV(0xFFFFFFFFFFFFFFFF, 64);
    var res = ctx.MkBVAND(ctx.MkBVAdd(s0, s1), and_val);
    s1 = ctx.MkBVXOR(s0, s1);
    var tmp = ctx.MkBVRotateLeft(24, s0);
    var tmp2 = ctx.MkBV(1 << 16, 64);
    s0 = ctx.MkBVXOR(tmp, ctx.MkBVXOR(s1, ctx.MkBVMul(s1, tmp2)));
    s1 = ctx.MkBVRotateLeft(37, s1);
    return res;
}

[MethodImpl(MethodImplOptions.AggressiveInlining)]
public static List<ulong> GetAllSeeds(PA8 mon)
{
    var result = new List<ulong>();
    ConcurrentBag<ulong> seeds = new();
    
    if (mon.IsShiny)
    {
        FindPotentialSeedsShiny(seeds, mon.PID & 0xFFFF, mon.EncryptionConstant);
    }
    else
    {
        FindPotentialSeeds(seeds, mon.PID, mon.EncryptionConstant);
        if (IsPotentialAntiShiny(mon.TID16, mon.SID16, mon.PID))
            FindPotentialSeeds(seeds, mon.PID ^ 0x1000_0000, mon.EncryptionConstant);
    }

    foreach (var seed in seeds)
    {
        for (int ivs = 0; ivs <= 4; ivs++)
        {
            // Verify the IVs; only 0, 3, and 4 fixed IVs exist.
            if (ivs > 0 && ivs < 3)
                ivs = 3;

            if (mon.FlawlessIVCount >= ivs && IsMatch(seed, ivs, mon, out uint shiny_xor))
                result.Add(seed);
        }
    }
    return result;
}

[MethodImpl(MethodImplOptions.AggressiveInlining)]
public static bool IsPotentialAntiShiny(int tid, int sid, uint pid)
{
    return GetIsShiny(tid, sid, pid ^ 0x1000_0000);
}

[MethodImpl(MethodImplOptions.AggressiveInlining)]
private static bool GetIsShiny(int tid, int sid, uint pid)
{
    return GetShinyXor(pid, (uint)((sid << 16) | tid)) < 16;
}

[MethodImpl(MethodImplOptions.AggressiveInlining)]
public static void FindPotentialSeeds(ConcurrentBag<ulong> all_seeds, uint pid, uint ec)
{
    ulong start_seed = ec - unchecked((uint)Xoroshiro128Plus.XOROSHIRO_CONST);

    Parallel.For(0, 0xFFFF, i =>
    {
        var test = start_seed | (ulong)((ulong)i << 48);
        for (int x = 0; x < 65536; x++)
        {
            var seed = CheckSeed(test, pid);
            if (seed != 0)
                all_seeds.Add(seed);
            test += 0x1_0000_0000;
        }
    });
}

[MethodImpl(MethodImplOptions.AggressiveInlining)]
public static void FindPotentialSeedsShiny(ConcurrentBag<ulong> all_seeds, uint pid, uint ec)
{
    ulong start_seed = ec - unchecked((uint)Xoroshiro128Plus.XOROSHIRO_CONST);
    Console.WriteLine($"Starting seed: {start_seed:x16}");

    Parallel.For(0, 0xFFFF, i =>
    {
        var test = start_seed | (ulong)((ulong)i << 48);
        for (int x = 0; x < 65536; x++)
        {
            var seed = CheckSeedShiny(test, pid);
            if (seed != 0)
                all_seeds.Add(seed);
            test += 0x1_0000_0000;
        }
    });
}

[MethodImpl(MethodImplOptions.AggressiveInlining)]
private static ulong CheckSeed(ulong seed, uint monpid)
{
    var rng = new Xoroshiro128Plus(seed);
    rng.NextInt(); // EC
    rng.NextInt(); // fakeTID

    var pid = rng.NextInt();
    if (pid == monpid)
        return seed;
    return 0;
}

[MethodImpl(MethodImplOptions.AggressiveInlining)]
private static ulong CheckSeedShiny(ulong seed, uint monpid)
{
    ulong seed0 = seed;
    var rng = new Xoroshiro128Plus(seed0);
    rng.NextInt(); // EC
    rng.NextInt(); // fakeTID

    var pid = rng.NextInt();
    if (monpid == (pid & 0xFFFF))
        return seed0;
    return 0;
}

[MethodImpl(MethodImplOptions.AggressiveInlining)]
public static bool IsMatch(ulong seed, int fixed_ivs, PA8 mon, out uint shiny_xor)
{
    Span<int> IVs = stackalloc int[6];
    mon.GetIVs(IVs);
    (IVs[5], IVs[3], IVs[4]) = (IVs[3], IVs[4], IVs[5]);
    
    var rng = new Xoroshiro128Plus(seed);
    rng.NextInt(); // EC
    uint fakeTID = (uint)rng.NextInt(); // TID

    uint pid = (uint)rng.NextInt(); // PID

    // Record whether this was a shiny seed or not.
    shiny_xor = GetShinyXor(pid, fakeTID);

    if (!mon.IsShiny && mon.PID != pid && mon.PID != (pid ^ 0x10000000))
        return false;
    if (mon.IsShiny && (mon.PID & 0xFFFF) != (pid & 0xFFFF))
        return false;

    int[] check_ivs = { -1, -1, -1, -1, -1, -1 };
    for (int i = 0; i < fixed_ivs; i++)
    {
        uint slot;
        do
        {
            slot = (uint)rng.NextInt(6);
        } while (check_ivs[slot] != -1);

        if (IVs[(int)slot] != 31)
            return false;

        check_ivs[slot] = 31;
    }
    for (int i = 0; i < 6; i++)
    {
        if (check_ivs[i] != -1)
            continue; // already verified?

        uint iv = (uint)rng.NextInt(32);
        if (iv != IVs[i])
            return false;
    }

    var ability = (int)rng.NextInt(2) + 1; // Ability 1 or 2 only -- potentially could be changed with transfers?
    if (ability != mon.AbilityNumber)
        return false;

    var genderratio = PersonalTable.LA[mon.Species].Gender;
    if (genderratio is not (PersonalInfo.RatioMagicGenderless or PersonalInfo.RatioMagicFemale or PersonalInfo.RatioMagicMale))
    {
        var gender = (int)rng.NextInt(253) + 1 < genderratio ? 1 : 0; // Gender
        if (gender != mon.Gender)
            return false;
    }
    
    var nature = (int)rng.NextInt(25); // Nature -- no synchronize in LA
    if (nature != (int)mon.Nature)
        return false;

    if (mon.IsAlpha)
        return true;

    // Hacky way to skip static encounters, validate yourself.
    if (mon.HeightScalar == 127 && mon.WeightScalar == 127)
        return true;

    var height = (int)rng.NextInt(0x81) + (int)rng.NextInt(0x80);
    if (height != mon.HeightScalar)
        return false;
    var weight = (int)rng.NextInt(0x81) + (int)rng.NextInt(0x80);
    if (weight != mon.WeightScalar)
        return false;

    return true;
}

[MethodImpl(MethodImplOptions.AggressiveInlining)]
private static uint GetShinyXor(uint pid, uint oid)
{
    var xor = pid ^ oid;
    return (xor ^ (xor >> 16)) & 0xFFFF;
}

/// <summary>
/// Self-modifying RNG structure that implements xoroshiro128+
/// </summary>
/// <remarks>https://en.wikipedia.org/wiki/Xoroshiro128%2B</remarks>
public ref struct Xoroshiro128Plus
{
    public const ulong XOROSHIRO_CONST0= 0x0F4B17A579F18960;
    public const ulong XOROSHIRO_CONST = 0x82A2B175229D6A5B;

    private ulong s0, s1;

    public Xoroshiro128Plus(ulong s0 = XOROSHIRO_CONST0, ulong s1 = XOROSHIRO_CONST) => (this.s0, this.s1) = (s0, s1);

    public (ulong s0, ulong s1) GetState() => (s0, s1);
    public string FullState => $"{s1:X16}{s0:X16}";

    [MethodImpl(MethodImplOptions.AggressiveInlining)]
    private static ulong RotateLeft(ulong x, int k) => System.Numerics.BitOperations.RotateLeft(x, k);    

    /// <summary>
    /// Gets the next random <see cref="ulong"/>.
    /// </summary>
    [MethodImpl(MethodImplOptions.AggressiveInlining)]
    public ulong Next()
    {
        var _s0 = s0;
        var _s1 = s1;
        ulong result = _s0 + _s1;

        _s1 ^= _s0;
        // Final calculations and store back to fields
        s0 = RotateLeft(_s0, 24) ^ _s1 ^ (_s1 << 16);
        s1 = RotateLeft(_s1, 37);

        return result;
    }

    /// <summary>
    /// Gets the next previous <see cref="ulong"/>.
    /// </summary>
    [MethodImpl(MethodImplOptions.AggressiveInlining)]
    public ulong Prev()
    {
        var _s0 = s0;
        var _s1 = s1;
        _s1 = RotateLeft(_s1, 27);
        _s0 = _s0 ^ _s1 ^ (_s1 << 16);
        _s0 = RotateLeft(_s0, 40);
        _s1 ^= _s0;
        ulong result = _s0 + _s1;

        s0 = _s0;
        s1 = _s1;
        return result;
    }

    /// <summary>
    /// Gets a random value that is less than <see cref="MOD"/>
    /// </summary>
    /// <param name="MOD">Maximum value (exclusive). Generates a bitmask for the loop.</param>
    /// <returns>Random value</returns>
    [MethodImpl(MethodImplOptions.AggressiveInlining)]
    public ulong NextInt(ulong MOD = 0xFFFFFFFF)
    {
        ulong mask = GetBitmask(MOD);
        ulong res;
        do
        {
            res = Next() & mask;
        } while (res >= MOD);
        return res;
    }

    /// <summary>
    /// Next Power of Two
    /// </summary>
    [MethodImpl(MethodImplOptions.AggressiveInlining)]
    private static ulong GetBitmask(ulong x)
    {
        x--; // comment out to always take the next biggest power of two, even if x is already a power of two
        x |= x >> 1;
        x |= x >> 2;
        x |= x >> 4;
        x |= x >> 8;
        x |= x >> 16;
        return x;
    }

    /// <summary>
    /// Gets a random float value.
    /// </summary>
    /// <param name="range">Range of values permitted [0,n)</param>
    /// <param name="bias">Number to add to the resultant amplified range.</param>
    /// <returns>Random value</returns>
    public float NextFloat(float range, float bias = 0f)
    {
        const float inv_64_f = 5.421e-20f; // 1/(2^64) as a float; 0x1F800000u moved into a float register.
        ulong next = Next();
        return (range * (next * inv_64_f)) + bias;
    }
}

This script is for solving for group seeds for overworld legendaries in LA such as Heatran and Enamorus for RNG manipulation.

Adapted from EtumrepMMO (this is from when I was figuring out a method to solve MMOs, and modified for legends spawning 1 instead of 4 at a time).

Setup is:

1. Download/install LINQPad 7 from https://www.linqpad.net/LINQPad7.aspx
2. Download dev build PKHeX from https://projectpokemon.org/home/files/file/2445-pkhex-development-build/
3. Download z3 for your platform from https://nuget.info/packages/Microsoft.Z3/4.12.2.
   • Grab Microsoft.z3.dll from /lib/netstandard2.0/.
   • Grab libz3.dll from /runtimes/win-x64/native/.
   • Put both Microsoft.Z3.dll and libz3.dll in the same folder.
4. Press F4 in LINQPad and add PKHeX.Core.dll and Microsoft.Z3.dll to first tab.
5. Add the following to the second tab.

Microsoft.Z3
PKHeX.Core
System.Collections.Concurrent
System.Runtime.CompilerServices
System.Threading.Tasks

7. Click OK to close this window.
8. Enable "compiler optimizations" by clicking the button at the bottom right of the window.
9. Change the language at the top to C# program, then copy/paste the script in verbatim.
10. Edit the link at the top to a folder with 2 consecutive overworld legendary Pokémon in it (save, catch one, dump it, reset, advance 1, catch the second one, dump it).
11. Click run.

This is not meant to be a polished or complete tool in itself, nor are there plans to make an easier tool with a GUI.