SM孵化乱数調査で実用化されなかったこと

この記事はPokémon RNG Advent Calendar 2016の19日目の記事です．

SM孵化乱数調整の調査の上で実用化されなかったものを紹介します．

はじめに


この1ヶ月も経たないうちに当初予想されていた形の”乱数調整”を遥かに上回るレベルでSMの孵化乱数調整が可能になりました．その結果12月19日現在，調査に加わっていた人やツール開発者以外の人でも乱数調整が可能な世界になりました．
私もサンムーンの取扱説明書を読んで他の人の助けもあり，内部で使われている乱数生成器がTiny Mersenne Twisterだと特定するなど貢献しました．
このように乱数調整の実用化に役立ったこともあれば，逆に調べたが見当違いだったことやより良い手法が発見されたため実用化されなかったこともありました．
この記事ではその実用化されなかったことを，同じことを他の人が調査するのを防止するためにも公開します．

初期seedの決定に使われるbit数

TinyMTの考案者が書いた実装では，tinymt32.cにあるように，初期化するための関数がtinymt32_init_by_arrayとtinymt32_initの二つあります．TinyMTの初期化に前者は任意のbit数の数値を使えるのですが，後者は32bitの数値しか使うことが出来ません．これを見た私はゲームの開発者が32bitの初期seedで初期化していることを信じて，次のような初期seedを全探索するコードを書いて調査してみました．

マシンパワーに物を言わせてプログラムを走らせましたが，結果が出力されることはありませんでした．
流石に32bitより多いbit数の数値でTinyMTを初期化しているようです．

Z3を使ったseedの特定

Z3とはMicrosoft Researchが開発している定理証明のソフトウェアです．簡単に言うと幾つかの等式や不等式の条件を渡すと，それを満たすような解を自動的に見つけてくれるものです．
これを使ってseedを特定できるのでは？との期待があった時もありましたが，water_blow さんがTinyMTの調律は最下位1bitに関しては線形だという発見をされてからはお蔵入りになりました．実はこいつを使うと，性格値や暗号化定数に相当する32bitの数値が8つ連続で観測できれば，現実的な時間でseedを特定することが出来ます．Z3のpythonラッパーであるZ3pyを使った実装が次です．

前述した通り，ゲーム内の127連続する1bitを観測することでseedが特定できると分かったので実用化されることはありませんでした．

終わりに

少数ですがSM孵化乱数調査で実用化されなかったことを紹介しました．
カメールアイコンの人がSMを買うとのことなので，さらに乱数調整の調査が進むといいですね．