let N: int = 65536;

namespace std::convert(N);
	// Due to its name, the semantics of this function will be overridden.
	// We ensure that this happens by making it diverge in its given semantics.
    let int = [|i| int(i)];

// ORs two 32-bit numbers, byte-by-byte.
namespace Or(N);
	col fixed RESET(i) { if (i % 4) == 3 { 1 } else { 0 } };
	col fixed FACTOR(i) { 1 << (((i + 1) % 4) * 8) };

	let a = |i| i % 256;
	col fixed P_A(i) { a(i) };
	let b = |i| (i >> 8) % 256;
	col fixed P_B(i) { b(i) };
	col fixed P_C(i) { (a(i) | b(i)) & 0xff };

	// ROW RESET  FACTOR
	//   0   0    1 << 8
	//   1   0    1 << 16
	//   2   0    1 << 24
	//   3   1    1 << 0

	col witness A_byte;
	col witness B_byte;
	col witness C_byte;

	col witness A;
	col witness B;
	col witness C;

	A' = A * (1 - RESET) + A_byte * FACTOR;
	B' = B * (1 - RESET) + B_byte * FACTOR;
	C' = C * (1 - RESET) + C_byte * FACTOR;

	[A_byte, B_byte, C_byte] in [P_A, P_B, P_C];

namespace Main(N);
	col fixed a(i) { (i + 13) & 0xffffffff };
	col fixed b(i) { ((i + 19) * 17) & 0xffffffff };
	col witness c;
	col fixed NTH(i) { if i % 32 == 0 { 1 } else { 0 } };

	NTH $ [a, b, c] in Or::RESET $ [Or::A, Or::B, Or::C];

