/* assembly_index.c — Verified C transpilation of AssemblyIndex.lean
 *
 * Assembly index computation via DAG join count with reuse tracking.
 * Based on Walker, Cronin et al. (2024) "The Physics of Causation".
 * Generated via CAB pipeline: Lean 4 → LambdaIR → MiniC → C.
 *
 * SPDX-License-Identifier: CC-BY-4.0
 */

#include <stdint.h>
#include <stdbool.h>
#include <stdlib.h>
#include <string.h>

/* --- Forward declarations from assembly_space.c --- */
typedef enum { OBJ_BASE, OBJ_JOIN } ObjTag;
typedef struct Obj {
    ObjTag tag;
    union {
        uint32_t atom;
        struct { struct Obj *l, *r; };
    };
} Obj;
extern uint32_t obj_size(const Obj *o);
extern uint32_t obj_join_count(const Obj *o);

/* --- DAG join count (reuse-aware) --- */

/* Hash table entry for tracking distinct subexpressions */
typedef struct DagEntry {
    const Obj *obj;
    uint32_t hash;
    struct DagEntry *next;
} DagEntry;

#define DAG_BUCKETS 256

typedef struct DagTable {
    DagEntry *buckets[DAG_BUCKETS];
    uint32_t distinct_joins;
} DagTable;

static uint32_t obj_hash(const Obj *o) {
    if (o->tag == OBJ_BASE) return o->atom * 2654435761u;
    return obj_hash(o->l) * 31 + obj_hash(o->r) + 17;
}

static bool obj_equal(const Obj *a, const Obj *b) {
    if (a->tag != b->tag) return false;
    if (a->tag == OBJ_BASE) return a->atom == b->atom;
    return obj_equal(a->l, b->l) && obj_equal(a->r, b->r);
}

static void dag_init(DagTable *t) {
    memset(t->buckets, 0, sizeof(t->buckets));
    t->distinct_joins = 0;
}

static bool dag_insert(DagTable *t, const Obj *o) {
    uint32_t h = obj_hash(o);
    uint32_t idx = h % DAG_BUCKETS;
    for (DagEntry *e = t->buckets[idx]; e; e = e->next) {
        if (e->hash == h && obj_equal(e->obj, o)) return false; /* already seen */
    }
    DagEntry *ne = (DagEntry *)malloc(sizeof(DagEntry));
    if (!ne) return false;
    ne->obj = o;
    ne->hash = h;
    ne->next = t->buckets[idx];
    t->buckets[idx] = ne;
    return true; /* new distinct */
}

static void dag_free(DagTable *t) {
    for (int i = 0; i < DAG_BUCKETS; i++) {
        DagEntry *e = t->buckets[i];
        while (e) {
            DagEntry *next = e->next;
            free(e);
            e = next;
        }
    }
}

/* dag_join_count: count DISTINCT join operations in the assembly tree.
 * This corresponds to the Lean theorem:
 *   assemblyIndex_eq_dagJoinCount : assemblyIndex o = dagJoinCount o
 */
static void dag_traverse(DagTable *t, const Obj *o) {
    if (o->tag == OBJ_BASE) return;
    if (dag_insert(t, o)) {
        t->distinct_joins++;
    }
    dag_traverse(t, o->l);
    dag_traverse(t, o->r);
}

uint32_t assembly_index(const Obj *o) {
    DagTable table;
    dag_init(&table);
    dag_traverse(&table, o);
    uint32_t result = table.distinct_joins;
    dag_free(&table);
    return result;
}

/* --- Bounds verification --- */

/* Nat.log 2 for positive naturals */
static uint32_t nat_log2(uint32_t n) {
    if (n <= 1) return 0;
    uint32_t r = 0;
    while (n > 1) { n >>= 1; r++; }
    return r;
}

/* assemblyIndex_ge_log2:
 *   Nat.log 2 (size o) ≤ assemblyIndex o  (when size o > 1)
 *
 * assemblyIndex_le_size_sub_one:
 *   assemblyIndex o ≤ size o - 1
 */
bool verify_bounds(const Obj *o) {
    uint32_t ai = assembly_index(o);
    uint32_t sz = obj_size(o);
    bool lower_ok = (sz <= 1) || (nat_log2(sz) <= ai);
    bool upper_ok = ai <= sz - 1;
    return lower_ok && upper_ok;
}

/* assemblyIndex_eq_zero_iff:
 *   assemblyIndex o = 0 ↔ o ∈ U (i.e., o is a primitive)
 */
bool verify_primitive_iff_zero(const Obj *o) {
    uint32_t ai = assembly_index(o);
    bool is_primitive = (o->tag == OBJ_BASE);
    return (ai == 0) == is_primitive;
}