#include <assert.h>
#include <stdbool.h>
#include <stdio.h>
#include <string.h>

typedef int esp_err_t;
typedef int mdns_if_t;
typedef int mdns_ip_protocol_t;
enum { ESP_OK, ESP_ERR_NO_MEM, ESP_ERR_INVALID_STATE };
enum { MDNS_IP_PROTOCOL_V4, MDNS_IP_PROTOCOL_V6, MDNS_IP_PROTOCOL_MAX };
#define MDNS_MAX_INTERFACES 2
#define MDNS_SERVICE_PORT 5353
struct udp_pcb { int mcast_ttl, remote_port, remote_ip; };
static int any_address;
#define IP_ANY_TYPE (&any_address)
#define ip_addr_copy(to, from) ((to) = (from))
static void receive(void) {}
static struct udp_pcb storage;
static bool allocated, fail_alloc, fail_bind, fail_join, fail_leave;
static int allocations, removals, joins[2][2], leaves[2][2], references[2][2];
static struct udp_pcb *udp_new(void)
{
    if (fail_alloc) return NULL;
    assert(!allocated);
    allocated = true;
    allocations++;
    return &storage;
}
static int udp_bind(struct udp_pcb *pcb, const int *address, int port)
{
    assert(pcb == &storage && address == IP_ANY_TYPE && port == 5353);
    return fail_bind;
}
static void udp_remove(struct udp_pcb *pcb)
{
    assert(pcb == &storage && allocated);
    allocated = false;
    removals++;
}
static void udp_recv(struct udp_pcb *pcb, void (*callback)(void), void *arg)
{ assert(pcb == &storage); (void)callback; (void)arg; }
static void udp_disconnect(struct udp_pcb *pcb) { assert(pcb == &storage); }
static esp_err_t join_group(mdns_if_t interface, mdns_ip_protocol_t family, bool join)
{
    if (join) {
        joins[interface][family]++;
        if (fail_join) return ESP_ERR_INVALID_STATE;
        references[interface][family]++;
        /* A real lwIP group has a bounded use count: never accumulate it. */
        assert(references[interface][family] == 1);
    } else {
        leaves[interface][family]++;
        if (fail_leave) return ESP_ERR_INVALID_STATE;
        assert(references[interface][family] == 1);
        references[interface][family]--;
    }
    return ESP_OK;
}

#include "actual_functions.inc"

static void reset(void)
{
    assert(!allocated && s_pcb_main == NULL);
    memset(s_interfaces, 0, sizeof(s_interfaces));
    memset(joins, 0, sizeof(joins));
    memset(leaves, 0, sizeof(leaves));
    memset(references, 0, sizeof(references));
    allocations = removals = 0;
    fail_alloc = fail_bind = fail_join = fail_leave = false;
}
static void check(int interface, int family, bool active)
{
    assert(!!mdns_priv_if_ready(interface, family) == active);
    assert(references[interface][family] == (int)active);
    assert(joins[interface][family] - leaves[interface][family] == (int)active);
}
static void transitions(int family)
{
    reset();
    int other = 1 - family;
    assert(pcb_if_init(0, family) == ESP_OK);
    assert(pcb_if_init(0, other) == ESP_OK);
    for (int i = 0; i < 512; i++) {
        pcb_if_deinit(0, family);
        check(0, family, false);
        check(0, other, true);
        assert(s_interfaces[0].ready && allocated && removals == 0);
        pcb_if_deinit(0, family); /* Already-disabled family must not leave again. */
        check(0, family, false);
        assert(pcb_if_init(0, family) == ESP_OK);
        check(0, family, true);
        int before = joins[0][family];
        assert(pcb_if_init(0, family) == ESP_ERR_INVALID_STATE);
        assert(joins[0][family] == before);
    }
    pcb_if_deinit(0, other);
    assert(s_interfaces[0].ready && allocated);
    pcb_if_deinit(0, family);
    assert(!s_interfaces[0].ready && !allocated);
    assert(allocations == 1 && removals == 1);
    pcb_if_deinit(0, family);
    pcb_if_deinit(0, other);
    check(0, family, false);
    check(0, other, false);
}
static void failures(int family)
{
    reset();
    pcb_if_deinit(0, family);
    assert(leaves[0][family] == 0 && removals == 0);
    fail_join = true;
    assert(pcb_if_init(0, family) == ESP_ERR_INVALID_STATE);
    assert(!s_interfaces[0].ready && s_interfaces[0].proto == 0);
    assert(allocations == 0 && leaves[0][family] == 0);
    fail_join = false;
    for (int mode = 0; mode < 2; mode++) {
        fail_alloc = mode == 0;
        fail_bind = mode == 1;
        for (int i = 0; i < 512; i++) {
            int before = leaves[0][family];
            assert(pcb_if_init(0, family) == (fail_alloc ? ESP_ERR_NO_MEM : ESP_ERR_INVALID_STATE));
            assert(leaves[0][family] == before + 1);
            assert(references[0][family] == 0 && !allocated && !s_pcb_main);
            assert(!s_interfaces[0].ready && s_interfaces[0].proto == 0);
            pcb_if_deinit(0, family);
            assert(leaves[0][family] == before + 1);
        }
    }
    fail_alloc = fail_bind = false;
    assert(pcb_if_init(0, family) == ESP_OK);
    pcb_if_deinit(0, family);
    assert(!allocated && references[0][family] == 0);

    /* Preserve upstream best-effort leave semantics when netif has gone down. */
    reset();
    assert(pcb_if_init(0, family) == ESP_OK);
    fail_leave = true;
    pcb_if_deinit(0, family);
    pcb_if_deinit(0, family);
    assert(leaves[0][family] == 1 && !s_interfaces[0].ready && !allocated);
    references[0][family] = 0; /* Model netif teardown clearing its memberships. */
    reset();
    fail_alloc = fail_leave = true;
    assert(pcb_if_init(0, family) == ESP_ERR_NO_MEM);
    assert(leaves[0][family] == 1 && !s_interfaces[0].ready && !allocated);
    references[0][family] = 0;
}
static void shared_pcb(int family)
{
    reset();
    assert(pcb_if_init(1, 1 - family) == ESP_OK);
    for (int i = 0; i < 512; i++) {
        assert(pcb_if_init(0, family) == ESP_OK);
        pcb_if_deinit(0, family);
        pcb_if_deinit(0, family);
        check(0, family, false);
        check(1, 1 - family, true);
        assert(!s_interfaces[0].ready && allocated && removals == 0);
    }
    assert(allocations == 1);
    pcb_if_deinit(1, 1 - family);
    assert(!allocated && removals == 1);
}
int main(void)
{
    for (int family = 0; family < 2; family++) {
        transitions(family);
        failures(family);
        shared_pcb(family);
    }
    puts("PASS: actual mDNS functions, 512 cycles per family/scenario, failure unwind and shared PCB");
    return 0;
}