/* assembly_bounds.c — Verified C transpilation of AssemblyBounds.lean
 *
 * Tight bounds on assembly index: log₂(size) ≤ AI ≤ size - 1.
 * 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>

/* Forward declarations */
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);
extern uint32_t assembly_index(const Obj *o);

/* --- Bounds check functions --- */

/* Upper bound: AI ≤ size - 1
 * Lean: assemblyIndex_le_size_sub_one
 * Proof: AI = dagJoinCount ≤ joinCount = size - 1 */
bool upper_bound_holds(const Obj *o) {
    return assembly_index(o) <= obj_size(o) - 1;
}

/* Lower bound: log₂(size) ≤ AI (when size > 1)
 * Lean: assemblyIndex_ge_log2
 * Proof: with n joins, at most 2^n leaves can be constructed (doubling argument) */
static uint32_t nat_log2_floor(uint32_t n) {
    if (n <= 1) return 0;
    uint32_t r = 0;
    while (n > 1) { n >>= 1; r++; }
    return r;
}

bool lower_bound_holds(const Obj *o) {
    uint32_t sz = obj_size(o);
    if (sz <= 1) return true; /* vacuous */
    return nat_log2_floor(sz) <= assembly_index(o);
}

/* Combined: both bounds hold simultaneously
 * Lean: dagJoinCount_bounds */
bool both_bounds_hold(const Obj *o) {
    return lower_bound_holds(o) && upper_bound_holds(o);
}

/* Tightness witness: chain of n joins gives AI = n, size = n+1 */
bool bounds_are_tight(uint32_t n) {
    /* For a linear chain: join(join(...join(base, base), base), base)
     * size = n + 1, AI = n (no reuse)
     * log₂(n+1) ≤ n ≤ (n+1) - 1 = n   ✓ */
    if (n == 0) return true;
    uint32_t sz = n + 1;
    return (nat_log2_floor(sz) <= n) && (n <= sz - 1);
}