import java.io.IOException;
import java.math.BigInteger;
import java.nio.charset.StandardCharsets;
import java.nio.file.Files;
import java.nio.file.Path;
import java.util.ArrayList;
import java.util.Map;
import java.util.TreeMap;
import java.util.List;

public final class OmegaNaughtConformance {
    static final String EXPECTED_CONTRACT = "OMEGA_NAUGHT/1.0";
    static final String EXPECTED_ALGEBRA = "Q(T)[lambda]/(lambda^2-T*lambda-T^2)";
    static final BigInteger EXPECTED_Q = new BigInteger("339949771344778");
    static final BigInteger EXPECTED_S = new BigInteger("1000000000000000");
    static final BigInteger EXPECTED_L60 = new BigInteger("339949771344778929576702809321279193551009905014259416689444");
    static final BigInteger EXPECTED_U60 = EXPECTED_L60.add(BigInteger.ONE);
    static final BigInteger ZERO = BigInteger.ZERO;
    static final BigInteger ONE = BigInteger.ONE;

    static Map<String,String> readManifest(String file) throws IOException {
        Map<String,String> m = new TreeMap<>();
        for (String raw : Files.readAllLines(Path.of(file), StandardCharsets.UTF_8)) {
            String line = raw.trim();
            if (line.isEmpty() || line.startsWith("#")) continue;
            int p = line.indexOf('=');
            if (p < 1) throw new IllegalArgumentException("bad manifest line: " + raw);
            m.put(line.substring(0,p).trim(), line.substring(p+1).trim());
        }
        return m;
    }

    static final class Laurent {
        final TreeMap<Integer,BigInteger> c = new TreeMap<>();
        Laurent() {}
        Laurent(Map<Integer,BigInteger> src) {
            for (var e : src.entrySet()) if (e.getValue().signum() != 0) c.put(e.getKey(), e.getValue());
        }
        static Laurent mono(int exp) { return mono(exp, ONE); }
        static Laurent mono(int exp, BigInteger k) {
            Laurent r = new Laurent();
            if (k.signum() != 0) r.c.put(exp, k);
            return r;
        }
        Laurent add(Laurent o) {
            TreeMap<Integer,BigInteger> d = new TreeMap<>(c);
            for (var e : o.c.entrySet()) {
                d.merge(e.getKey(), e.getValue(), BigInteger::add);
                if (d.get(e.getKey()).signum() == 0) d.remove(e.getKey());
            }
            return new Laurent(d);
        }
        Laurent neg() {
            TreeMap<Integer,BigInteger> d = new TreeMap<>();
            for (var e : c.entrySet()) d.put(e.getKey(), e.getValue().negate());
            return new Laurent(d);
        }
        Laurent sub(Laurent o) { return add(o.neg()); }
        Laurent mul(Laurent o) {
            TreeMap<Integer,BigInteger> d = new TreeMap<>();
            for (var x : c.entrySet()) for (var y : o.c.entrySet()) {
                int k = x.getKey() + y.getKey();
                BigInteger v = x.getValue().multiply(y.getValue());
                d.merge(k, v, BigInteger::add);
                if (d.get(k).signum() == 0) d.remove(k);
            }
            return new Laurent(d);
        }
        Laurent shift(int k) {
            TreeMap<Integer,BigInteger> d = new TreeMap<>();
            for (var e : c.entrySet()) d.put(e.getKey()+k, e.getValue());
            return new Laurent(d);
        }
        boolean isZero() { return c.isEmpty(); }
        @Override public boolean equals(Object o) { return o instanceof Laurent l && c.equals(l.c); }
        @Override public int hashCode() { return c.hashCode(); }
    }

    static final class K {
        final Laurent a, b; // a(T) + b(T) lambda
        K(Laurent a, Laurent b) { this.a = a; this.b = b; }
        static K one() { return new K(Laurent.mono(0), new Laurent()); }
        static K T() { return new K(Laurent.mono(1), new Laurent()); }
        static K Tinv() { return new K(Laurent.mono(-1), new Laurent()); }
        static K lam() { return new K(new Laurent(), Laurent.mono(0)); }
        K add(K o) { return new K(a.add(o.a), b.add(o.b)); }
        K neg() { return new K(a.neg(), b.neg()); }
        K sub(K o) { return add(o.neg()); }
        K mul(K o) {
            // lambda^2 = T*lambda + T^2
            Laurent bd = b.mul(o.b);
            Laurent na = a.mul(o.a).add(bd.shift(2));
            Laurent nb = a.mul(o.b).add(b.mul(o.a)).add(bd.shift(1));
            return new K(na, nb);
        }
        boolean isZero() { return a.isZero() && b.isZero(); }
        @Override public boolean equals(Object o) { return o instanceof K k && a.equals(k.a) && b.equals(k.b); }
        @Override public int hashCode() { return 31*a.hashCode()+b.hashCode(); }
    }

    record Result(String name, boolean ok) {}
    static void check(List<Result> r, String name, boolean ok) { r.add(new Result(name, ok)); }

    public static void main(String[] args) throws Exception {
        String file = args.length > 0 ? args[0] : "OMEGA_NAUGHT_1_0.manifest";
        Map<String,String> m = readManifest(file);
        List<Result> results = new ArrayList<>();

        check(results, "manifest.contract", EXPECTED_CONTRACT.equals(m.get("contract")));
        check(results, "manifest.algebra", EXPECTED_ALGEBRA.equals(m.get("algebra")));

        int bits = Integer.parseInt(m.get("bits"));
        BigInteger Q = new BigInteger(m.get("Q"));
        BigInteger S = new BigInteger(m.get("S"));
        BigInteger L60 = new BigInteger(m.get("L60"));
        BigInteger U60 = new BigInteger(m.get("U60"));
        check(results, "manifest.expected_L60", EXPECTED_L60.equals(L60));
        check(results, "manifest.expected_U60", EXPECTED_U60.equals(U60));
        check(results, "manifest.expected_Q", EXPECTED_Q.equals(Q));
        check(results, "manifest.expected_S", EXPECTED_S.equals(S));

        K one = K.one(), T = K.T(), Ti = K.Tinv(), lam = K.lam();
        K omega = Ti, tau = T, phi = lam.mul(Ti), mu = one.sub(lam), piK = omega.sub(phi);

        check(results, "exact.omega_tau", omega.mul(tau).equals(one));
        check(results, "exact.lambda_mu", lam.add(mu).equals(one));
        check(results, "exact.lambda_relation", lam.mul(lam).sub(tau.mul(lam)).sub(tau.mul(tau)).isZero());
        check(results, "exact.phi_quadratic", phi.mul(phi).sub(phi).sub(one).isZero());
        check(results, "exact.phi_pi_omega", phi.add(piK).equals(omega));

        String qs = "";
        BigInteger ten15 = BigInteger.TEN.pow(15);
        if (S.equals(ten15) && Q.signum() >= 0 && Q.compareTo(S) < 0)
            qs = "0." + String.format("%015d", Q.longValueExact());
        check(results, "finite.qs_decimal", qs.equals("0.339949771344778"));
        check(results, "finite.ledger_adjacent", U60.subtract(L60).equals(ONE));
        check(results, "finite.qs_below_L60", Q.multiply(BigInteger.TEN.pow(45)).compareTo(L60) < 0);

        boolean replay = bits == 15;
        if (replay) {
            int limit = 1 << bits;
            for (int d = 0; d < limit; d++) {
                BigInteger D = BigInteger.valueOf(d);
                BigInteger y = Q.multiply(D);
                BigInteger f = y.divide(S);
                BigInteger rho = y.subtract(S.multiply(f));
                if (rho.signum() < 0 || rho.compareTo(S) >= 0) { replay = false; break; }
                BigInteger num = S.multiply(f).add(rho);
                BigInteger[] qr = num.divideAndRemainder(Q);
                if (qr[1].signum() != 0 || !qr[0].equals(D)) { replay = false; break; }
            }
        }
        check(results, "finite.unsigned_15bit_replay", replay);

        boolean interval = bits == 15;
        if (interval) {
            BigInteger scale = BigInteger.TEN.pow(60);
            int limit = 1 << bits;
            for (int d = 0; d < limit; d++) {
                BigInteger D = BigInteger.valueOf(d);
                BigInteger qf = Q.multiply(D).divide(S);
                if (d == 0) {
                    if (qf.signum() != 0) { interval = false; break; }
                    continue;
                }
                BigInteger lowerFloor = L60.multiply(D).divide(scale);
                BigInteger[] ur = U60.multiply(D).divideAndRemainder(scale);
                BigInteger upperFloor = ur[1].signum() == 0 ? ur[0].subtract(ONE) : ur[0];
                if (!lowerFloor.equals(upperFloor) || !lowerFloor.equals(qf)) { interval = false; break; }
            }
        }
        check(results, "finite.interval_floor_15bit", interval);

        boolean pass = true;
        for (Result r : results) {
            System.out.println(r.name() + "=" + (r.ok() ? "PASS" : "FAIL"));
            pass &= r.ok();
        }
        System.out.println("RESULT=" + (pass ? "PASS" : "FAIL"));
        if (!pass) System.exit(1);
    }
}