x = flr(rnd(2))
y = flr(rnd(2))
z = rnd({0,1})

function test_prng_flaw(x,y,z)
  return z==(x^^y)
end
cls()
print("starting")
for i=1,10000 do
  x=rnd(2)\1
  y=rnd(2)\1
  z=rnd({0,1})
  assert(test_prng_flaw(x,y,z))
end
print("prng is flawed")

unsigned int _p8_m_high=0x1234567;
unsigned int _p8_m_low=0xDEADBEEF;
unsigned int __cdecl pico8_random(unsigned int a1)
{
  unsigned int v1; // edx
  v1 = 0;
  if ( a1 )
  {
    _p8_m_high = (_p8_m_high << 0x10 | _p8_m_high >> 0x10) + _p8_m_low;
    p8_m_low += p8_m_high;
    v1 = p8_m_high % a1;
  }
  return v1;
}

#include <stdio.h>
#include <assert.h>

// prng
// takes and returns a pico-8 number:
//   the high 16 bits are the integer part;
//   the low 16 bits are the fractional part
unsigned int _p8_m_high=0x1234567;
unsigned int _p8_m_low=0xDEADBEEF;
unsigned int _pico8_random(unsigned int n) {
  unsigned int result = 0;
  if (n != 0) {
    // advance the rng state
    _p8_m_high = (_p8_m_high << 0x10 | _p8_m_high >> 0x10) + _p8_m_low;
    _p8_m_low = _p8_m_low + _p8_m_high;
    result = _p8_m_high % n;
  }
  return result;
}

int test_prng_flaw(int x, int y, int z) {
  return z==(x^y);
}

// returns a double between 0 and n
// simulates pico-8's rnd, except that we return a double
//  (p8 returns a fixed-point value; this does not matter for this
//  test, but it's worth pointing out)
double rnd(int n) {
  return ((double)_pico8_random(n << 16))/(1<<16);
}

// in pico-8 rnd(table) returns a random element of table.
// this function returns the _index_ that pico-8 chooses;
// i.e. rnd(table) in pico8 can be simulated in c with
//  arr[choosei(n)] (where n is the array length)
int choosei(int n) {
  return _pico8_random(n);
}

int main() {
  printf("starting\n");
  for (int i=0; i<10000; ++i) {
    int x=(int)rnd(2);
    int y=(int)rnd(2);
    int z=choosei(2);
    assert(z==0 || z==1);
    assert(test_prng_flaw(x,y,z));
  }
  printf("prng is flawed\n");
}

$ clang test.c && ./a.exe
starting
prng is flawed

// run this with `clang proof.c && ./a.exe`

#include <stdio.h>
#include <assert.h>
typedef unsigned int u32;

int bit(int b, u32 x) {
  return (x&(1 << b))!=0;
}

u32 _p8_m_high=0x01234567;
u32 _p8_m_low =0xDEADBEEF;
u32 _pico8_random(u32 n) {
  if (n == 0) return 0;
  u32 swap=(_p8_m_high << 16 | _p8_m_high >> 16);
  u32 old_low=_p8_m_low;
  _p8_m_high = swap + old_low;
  _p8_m_low = swap + (old_low<<1);
  // notice:
  // * (bit(3,n) means the 3rd-least-significant bit of n)
  // * Property 1: bit(0,_p8_m_high) == (bit(0,swap)+bit(0,old_low))%2
  // * Property 2: bit(0,_p8_m_low) == bit(0,swap)
  return _p8_m_high % n;
}

void test() {
  // Lowercase letters are placeholders for bits,
  //   different from each other and not important
  // Uppercase letters are variables that always hold
  //   the same value throughout this calculation;
  //   i.e., iff A is 1 at the start, it is still 1 at the end
  _pico8_random(100);
  u32 x=_p8_m_high;

  // _p8_m_high = 0xaaaaaaaa aaaaaaaA bbbbbbbb bbbbbbbb // new var: A
  // _p8_m_low  = 0xcccccccc cccccccc dddddddd dddddddd
  _pico8_random(42);
  // swap       = 0xbbbbbbbb bbbbbbbb aaaaaaaa aaaaaaaA // notice: A
  u32 y=_p8_m_high;

  // _p8_m_high = 0xeeeeeeee eeeeeeeE ffffffff ffffffff // new var: E
  // _p8_m_low  = 0xgggggggg gggggggg hhhhhhhh hhhhhhhA // A ends up copied here (Property 2)
  _pico8_random(1337);
  // swap       = 0xffffffff ffffffff eeeeeeee eeeeeeeE // notice: E
  u32 z=_p8_m_high;

  // _p8_m_high = 0xiiiiiiii iiiiiiii jjjjjjjj jjjjjjjJ // new var: J=(E+A)%2 (Property 1)
  // _p8_m_low  = 0xkkkkkkkk kkkkkkkk llllllll llllllll

  // notice:
  // * J=(E+A)%2 (follows from Property 1)
  // * (E+A)%2 == E xor A
  //   (can be proved easily by looking at all 4 possible values for A and E)
  // * proof completed!

  assert(bit(0,z)==(bit(16,x)^bit(16,y)));
}

int main() {
  for (int i=0; i<10000; ++i) {
    test();
  }
}