/*
 * DF-5778 — DragonFly KLD harness: production AMD Display Core IRQ
 * dispatcher logic compiled with a synthetic irq_source_info table
 * (no AMD GPU required; the "family standard" synthetic-table method).
 *
 * WHAT IS PRODUCTION CODE HERE (byte-identical bodies; only
 * preprocessor interposition of dm_read_reg/dm_write_reg/DC_LOG_ERROR,
 * which are macros in production too, provided by dm_services.h):
 *
 *   [P1] enum dc_irq_source (complete, all 90 enumerators) and
 *        DAL_VALID_IRQ_SRC_NUM
 *        ...... sys/dev/drm/amd/display/dc/irq_types.h:36-158
 *   [P2] struct irq_source_info_funcs / irq_source_info /
 *        irq_service_funcs / irq_service
 *        ...... sys/dev/drm/amd/display/dc/irq/irq_service.h:36-70
 *   [P3] find_irq_source_info / dal_irq_service_set_generic /
 *        dal_irq_service_set / dal_irq_service_ack_generic /
 *        dal_irq_service_ack / dal_irq_service_to_irq_source
 *        ...... sys/dev/drm/amd/display/dc/irq/irq_service.c:77-169
 *
 * WHAT IS SYNTHETIC: table contents (synthetic register addresses,
 * masks, funcs wiring mimicking the four in-tree family tables),
 * adjacency guard canaries, and the register-access recorder that
 * stands in for the cgs MMIO backend.
 *
 * PROOFS RUN AT MODULE LOAD (results to dmesg, prefix "DF5778"):
 *   B1  bounds sweep of find_irq_source_info: accepts 0..89 exactly,
 *       rejects 90 (one-past-end), 91, 95, 0xFF, 0xFFFF, 0x7FFFFFFF,
 *       0xFFFFFFFF ((enum)-1) — the table walk stays in-bounds.
 *   B2  guard canaries physically adjacent to the table: intact.
 *   B3  DF-4731 cross-proof: DAL_VALID_IRQ_SRC_NUM(90) == true (known
 *       macro off-by-one) while find_irq_source_info(90) == NULL —
 *       the dispatcher's `>=` defuses the macro on set/ack paths.
 *   B4  upstream divergence: Linux v4.17 used `>` (accepts 90 →
 *       &info[90] one-past-end read); the DFly tree's `>=` at
 *       irq_service.c:82 rejects it (emulated on the same table).
 *   T1  THE FINDING: zero-initialised irq_service — the object a
 *       swallowed dal_irq_service_construct failure leaves behind —
 *       handed to dal_irq_service_to_irq_source (irq_service.c:165):
 *       deref chain svc->funcs (offset 16) is NULL → the verbatim
 *       line would fault; NO guard exists. Probed fault-free by
 *       replicating the exact deref chain.
 *   T2  verbatim dal_irq_service_to_irq_source happy path with a
 *       properly wired funcs (production path executes correctly).
 *   T3  dummy-slot dispatch (family dummy_irq_entry semantics):
 *       zero register accesses, clean false return.
 *   T4  generic-slot dispatch (funcs members NULL → generic RMW):
 *       recorder sees exactly the synthetic enable_reg/ack_reg (ack
 *       runs first inside set), values correctly masked.
 */

#include <sys/param.h>
#include <sys/kernel.h>
#include <sys/module.h>
#include <sys/systm.h>
#include <sys/types.h>

/* ==== interposition for production macros (dm_services.h provides these
 * ==== as macros in production; we record instead of hitting cgs MMIO) */
static uint32_t df_reg_read_addr[64];
static uint32_t df_reg_write_addr[64];
static uint32_t df_reg_write_val[64];
static int df_nreads, df_nwrites;

#define dm_read_reg(ctx, address)					\
	({ uint32_t _a = (uint32_t)(address);				\
	   if (df_nreads < 64) df_reg_read_addr[df_nreads] = _a;	\
	   df_nreads++; 0xA5A5A5A5u; })

#define dm_write_reg(ctx, address, value)				\
	({ uint32_t _a = (uint32_t)(address); uint32_t _v = (value);	\
	   if (df_nwrites < 64) { df_reg_write_addr[df_nwrites] = _a;	\
	   df_reg_write_val[df_nwrites] = _v; } df_nwrites++; })

#define DC_LOG_ERROR(fmt, ...)						\
	kprintf("DF5778: [DC_LOG_ERROR] " fmt, ## __VA_ARGS__)

#define BREAK_TO_DEBUGGER()	do { } while (0)

/* ==== VERBATIM BEGIN: sys/dev/drm/amd/display/dc/irq_types.h:36-158 ==== */
struct dc_context;

typedef void (*interrupt_handler)(void *);

typedef void *irq_handler_idx;
#define DAL_INVALID_IRQ_HANDLER_IDX NULL

enum dc_irq_source {
	/* Use as mask to specify invalid irq source */
	DC_IRQ_SOURCE_INVALID = 0,

	DC_IRQ_SOURCE_HPD1,
	DC_IRQ_SOURCE_HPD2,
	DC_IRQ_SOURCE_HPD3,
	DC_IRQ_SOURCE_HPD4,
	DC_IRQ_SOURCE_HPD5,
	DC_IRQ_SOURCE_HPD6,

	DC_IRQ_SOURCE_HPD1RX,
	DC_IRQ_SOURCE_HPD2RX,
	DC_IRQ_SOURCE_HPD3RX,
	DC_IRQ_SOURCE_HPD4RX,
	DC_IRQ_SOURCE_HPD5RX,
	DC_IRQ_SOURCE_HPD6RX,

	DC_IRQ_SOURCE_I2C_DDC1,
	DC_IRQ_SOURCE_I2C_DDC2,
	DC_IRQ_SOURCE_I2C_DDC3,
	DC_IRQ_SOURCE_I2C_DDC4,
	DC_IRQ_SOURCE_I2C_DDC5,
	DC_IRQ_SOURCE_I2C_DDC6,

	DC_IRQ_SOURCE_DPSINK1,
	DC_IRQ_SOURCE_DPSINK2,
	DC_IRQ_SOURCE_DPSINK3,
	DC_IRQ_SOURCE_DPSINK4,
	DC_IRQ_SOURCE_DPSINK5,
	DC_IRQ_SOURCE_DPSINK6,

	DC_IRQ_SOURCE_TIMER,

	DC_IRQ_SOURCE_PFLIP_FIRST,
	DC_IRQ_SOURCE_PFLIP1 = DC_IRQ_SOURCE_PFLIP_FIRST,
	DC_IRQ_SOURCE_PFLIP2,
	DC_IRQ_SOURCE_PFLIP3,
	DC_IRQ_SOURCE_PFLIP4,
	DC_IRQ_SOURCE_PFLIP5,
	DC_IRQ_SOURCE_PFLIP6,
	DC_IRQ_SOURCE_PFLIP_UNDERLAY0,
	DC_IRQ_SOURCE_PFLIP_LAST = DC_IRQ_SOURCE_PFLIP_UNDERLAY0,

	DC_IRQ_SOURCE_GPIOPAD0,
	DC_IRQ_SOURCE_GPIOPAD1,
	DC_IRQ_SOURCE_GPIOPAD2,
	DC_IRQ_SOURCE_GPIOPAD3,
	DC_IRQ_SOURCE_GPIOPAD4,
	DC_IRQ_SOURCE_GPIOPAD5,
	DC_IRQ_SOURCE_GPIOPAD6,
	DC_IRQ_SOURCE_GPIOPAD7,
	DC_IRQ_SOURCE_GPIOPAD8,
	DC_IRQ_SOURCE_GPIOPAD9,
	DC_IRQ_SOURCE_GPIOPAD10,
	DC_IRQ_SOURCE_GPIOPAD11,
	DC_IRQ_SOURCE_GPIOPAD12,
	DC_IRQ_SOURCE_GPIOPAD13,
	DC_IRQ_SOURCE_GPIOPAD14,
	DC_IRQ_SOURCE_GPIOPAD15,
	DC_IRQ_SOURCE_GPIOPAD16,
	DC_IRQ_SOURCE_GPIOPAD17,
	DC_IRQ_SOURCE_GPIOPAD18,
	DC_IRQ_SOURCE_GPIOPAD19,
	DC_IRQ_SOURCE_GPIOPAD20,
	DC_IRQ_SOURCE_GPIOPAD21,
	DC_IRQ_SOURCE_GPIOPAD22,
	DC_IRQ_SOURCE_GPIOPAD23,
	DC_IRQ_SOURCE_GPIOPAD24,
	DC_IRQ_SOURCE_GPIOPAD25,
	DC_IRQ_SOURCE_GPIOPAD26,
	DC_IRQ_SOURCE_GPIOPAD27,
	DC_IRQ_SOURCE_GPIOPAD28,
	DC_IRQ_SOURCE_GPIOPAD29,
	DC_IRQ_SOURCE_GPIOPAD30,

	DC_IRQ_SOURCE_DC1UNDERFLOW,
	DC_IRQ_SOURCE_DC2UNDERFLOW,
	DC_IRQ_SOURCE_DC3UNDERFLOW,
	DC_IRQ_SOURCE_DC4UNDERFLOW,
	DC_IRQ_SOURCE_DC5UNDERFLOW,
	DC_IRQ_SOURCE_DC6UNDERFLOW,

	DC_IRQ_SOURCE_DMCU_SCP,
	DC_IRQ_SOURCE_VBIOS_SW,

	DC_IRQ_SOURCE_VUPDATE1,
	DC_IRQ_SOURCE_VUPDATE2,
	DC_IRQ_SOURCE_VUPDATE3,
	DC_IRQ_SOURCE_VUPDATE4,
	DC_IRQ_SOURCE_VUPDATE5,
	DC_IRQ_SOURCE_VUPDATE6,

	DC_IRQ_SOURCE_VBLANK1,
	DC_IRQ_SOURCE_VBLANK2,
	DC_IRQ_SOURCE_VBLANK3,
	DC_IRQ_SOURCE_VBLANK4,
	DC_IRQ_SOURCE_VBLANK5,
	DC_IRQ_SOURCE_VBLANK6,

	DC_IRQ_SOURCE_DC1_VLINE0,
	DC_IRQ_SOURCE_DC2_VLINE0,
	DC_IRQ_SOURCE_DC3_VLINE0,
	DC_IRQ_SOURCE_DC4_VLINE0,
	DC_IRQ_SOURCE_DC5_VLINE0,
	DC_IRQ_SOURCE_DC6_VLINE0,

	DAL_IRQ_SOURCES_NUMBER
};

enum irq_type
{
	IRQ_TYPE_PFLIP = DC_IRQ_SOURCE_PFLIP1,
	IRQ_TYPE_VUPDATE = DC_IRQ_SOURCE_VUPDATE1,
	IRQ_TYPE_VBLANK = DC_IRQ_SOURCE_VBLANK1,
};

#define DAL_VALID_IRQ_SRC_NUM(src) \
	((src) <= DAL_IRQ_SOURCES_NUMBER && (src) > DC_IRQ_SOURCE_INVALID)
/* ==== VERBATIM END: irq_types.h ==== */

/* ==== VERBATIM BEGIN: sys/dev/drm/amd/display/include/irq_service_interface.h:28-47
 * ==== (production irq_service.h includes this header first, irq_service.h:29) ==== */
struct irq_service_init_data {
	struct dc_context *ctx;
};

struct irq_service;

void dal_irq_service_destroy(struct irq_service **irq_service);

bool dal_irq_service_set(
	struct irq_service *irq_service,
	enum dc_irq_source source,
	bool enable);

bool dal_irq_service_ack(
	struct irq_service *irq_service,
	enum dc_irq_source source);

enum dc_irq_source dal_irq_service_to_irq_source(
		struct irq_service *irq_service,
		uint32_t src_id,
		uint32_t ext_id);
/* ==== VERBATIM END: irq_service_interface.h ==== */

/* ==== VERBATIM BEGIN: sys/dev/drm/amd/display/dc/irq/irq_service.h:36-70 ==== */
struct irq_service;
struct irq_source_info;

struct irq_source_info_funcs {
	bool (*set)(
		struct irq_service *irq_service,
		const struct irq_source_info *info,
		bool enable);
	bool (*ack)(
		struct irq_service *irq_service,
		const struct irq_source_info *info);
};

struct irq_source_info {
	uint32_t src_id;
	uint32_t ext_id;
	uint32_t enable_reg;
	uint32_t enable_mask;
	uint32_t enable_value[2];
	uint32_t ack_reg;
	uint32_t ack_mask;
	uint32_t ack_value;
	uint32_t status_reg;
	const struct irq_source_info_funcs *funcs;
};

struct irq_service_funcs {
	enum dc_irq_source (*to_dal_irq_source)(
			struct irq_service *irq_service,
			uint32_t src_id,
			uint32_t ext_id);
};

struct irq_service {
	struct dc_context *ctx;
	const struct irq_source_info *info;
	const struct irq_service_funcs *funcs;
};

/* VERBATIM: irq_service.h:72-83 */
void dal_irq_service_construct(
	struct irq_service *irq_service,
	struct irq_service_init_data *init_data);

void dal_irq_service_ack_generic(
	struct irq_service *irq_service,
	const struct irq_source_info *info);

void dal_irq_service_set_generic(
	struct irq_service *irq_service,
	const struct irq_source_info *info,
	bool enable);
/* ==== VERBATIM END: irq_service.h ==== */

/* ==== VERBATIM BEGIN: sys/dev/drm/amd/display/dc/irq/irq_service.c:77-169 ==== */
static
const struct irq_source_info *find_irq_source_info(
	struct irq_service *irq_service,
	enum dc_irq_source source)
{
	if (source >= DAL_IRQ_SOURCES_NUMBER || source < DC_IRQ_SOURCE_INVALID)
		return NULL;

	return &irq_service->info[source];
}

void dal_irq_service_set_generic(
	struct irq_service *irq_service,
	const struct irq_source_info *info,
	bool enable)
{
	uint32_t addr = info->enable_reg;
	uint32_t value = dm_read_reg(irq_service->ctx, addr);

	value = (value & ~info->enable_mask) |
		(info->enable_value[enable ? 0 : 1] & info->enable_mask);
	dm_write_reg(irq_service->ctx, addr, value);
}

bool dal_irq_service_set(
	struct irq_service *irq_service,
	enum dc_irq_source source,
	bool enable)
{
	const struct irq_source_info *info =
		find_irq_source_info(irq_service, source);

	if (!info) {
		DC_LOG_ERROR("%s: cannot find irq info table entry for %d\n",
			__func__,
			source);
		return false;
	}

	dal_irq_service_ack(irq_service, source);

	if (info->funcs->set)
		return info->funcs->set(irq_service, info, enable);

	dal_irq_service_set_generic(irq_service, info, enable);

	return true;
}

void dal_irq_service_ack_generic(
	struct irq_service *irq_service,
	const struct irq_source_info *info)
{
	uint32_t addr = info->ack_reg;
	uint32_t value = dm_read_reg(irq_service->ctx, addr);

	value = (value & ~info->ack_mask) |
		(info->ack_value & info->ack_mask);
	dm_write_reg(irq_service->ctx, addr, value);
}

bool dal_irq_service_ack(
	struct irq_service *irq_service,
	enum dc_irq_source source)
{
	const struct irq_source_info *info =
		find_irq_source_info(irq_service, source);

	if (!info) {
		DC_LOG_ERROR("%s: cannot find irq info table entry for %d\n",
			__func__,
			source);
		return false;
	}

	if (info->funcs->ack)
		return info->funcs->ack(irq_service, info);

	dal_irq_service_ack_generic(irq_service, info);

	return true;
}

enum dc_irq_source dal_irq_service_to_irq_source(
		struct irq_service *irq_service,
		uint32_t src_id,
		uint32_t ext_id)
{
	return irq_service->funcs->to_dal_irq_source(
		irq_service,
		src_id,
		ext_id);
}
/* ==== VERBATIM END: irq_service.c ==== */

/* ==== SYNTHETIC TABLE (family standard) ====
 * guard words physically adjacent (same object) so any off-by-one walk
 * is observable; dummy/generic func wiring mirrors the in-tree family
 * tables' shapes. */
static struct {
	uint32_t guard_lo;
	struct irq_source_info tab[DAL_IRQ_SOURCES_NUMBER];
	uint32_t guard_hi;
} df_table = { .guard_lo = 0x11223344u, .guard_hi = 0x55667788u };

static bool dummy_set(struct irq_service *irq_service,
		      const struct irq_source_info *info, bool enable)
{
	DC_LOG_ERROR("%s: called for non-implemented irq source\n", __func__);
	return false;	/* mirrors dal_irq_service_dummy_set, dce110:176-184 */
}

static bool dummy_ack(struct irq_service *irq_service,
		      const struct irq_source_info *info)
{
	DC_LOG_ERROR("%s: called for non-implemented irq source\n", __func__);
	return false;	/* mirrors dal_irq_service_dummy_ack, dce110:185-192 */
}

static const struct irq_source_info_funcs dummy_irq_info_funcs = {
	.set = dummy_set,	/* family: .set = dal_irq_service_dummy_set */
	.ack = dummy_ack,	/* family: .ack = dal_irq_service_dummy_ack */
};

static const struct irq_source_info_funcs generic_irq_info_funcs = {
	.set = NULL,		/* hpd_rx/pflip/dcn10-vblank shape */
	.ack = NULL,
};

static enum dc_irq_source synthetic_to_dal_irq_source(
	struct irq_service *irq_service, uint32_t src_id, uint32_t ext_id)
{
	if (src_id == 0x7)
		return DC_IRQ_SOURCE_HPD1;
	return DC_IRQ_SOURCE_INVALID;
}

static const struct irq_service_funcs synthetic_irq_service_funcs = {
	.to_dal_irq_source = synthetic_to_dal_irq_source,
};

static void df_tab_init(void)
{
	int i;

	for (i = 0; i < DAL_IRQ_SOURCES_NUMBER; i++)
		df_table.tab[i].funcs = &dummy_irq_info_funcs;

	/* slot 1 (HPD1): generic-RMW shape with synthetic regs */
	df_table.tab[1].funcs = &generic_irq_info_funcs;
	df_table.tab[1].enable_reg = 0xDEAD0001u;
	df_table.tab[1].enable_mask = 0x00000003u;
	df_table.tab[1].enable_value[0] = 0x00000003u;
	df_table.tab[1].enable_value[1] = 0x00000000u;
	df_table.tab[1].ack_reg = 0xDEAD0002u;
	df_table.tab[1].ack_mask = 0x00000010u;
	df_table.tab[1].ack_value = 0x00000010u;
}

/* stand-in for a family-constructed irq_service */
static struct irq_service synth_svc;

static int in_table(const struct irq_source_info *p)
{
	return p >= &df_table.tab[0] &&
	       p <  &df_table.tab[DAL_IRQ_SOURCES_NUMBER];
}

static void df_rec_reset(void) { df_nreads = df_nwrites = 0; }

static int df5778_modevent(module_t mod, int type, void *arg)
{
	static const uint32_t sweep[] = {
		0, 1, 45, 89, 90, 91, 95, 0xFF, 0xFFFF, 0x7FFFFFFF, 0xFFFFFFFF
	};
	struct irq_service zero_svc = { NULL, NULL, NULL };
	const struct irq_source_info *p;
	uint32_t i;
	int nfail = 0;

	if (type != MOD_LOAD)
		return 0;

	df_tab_init();
	synth_svc.ctx = NULL;
	synth_svc.info = df_table.tab;
	synth_svc.funcs = &synthetic_irq_service_funcs;

	kprintf("DF5778: ==== B1 find_irq_source_info bounds sweep ====\n");
	for (i = 0; i < sizeof(sweep) / sizeof(sweep[0]); i++) {
		enum dc_irq_source s = (enum dc_irq_source)sweep[i];
		p = find_irq_source_info(&synth_svc, s);
		kprintf("DF5778: B1 src=%-10u -> %s%s\n", sweep[i],
			p ? "ENTRY" : "NULL ",
			p ? (in_table(p) ? " (in-table)" :
			     " !!! OUT OF TABLE !!!") : "(rejected)");
		if (!p) {
			if (sweep[i] <= 89)
				nfail++;
		} else if (!in_table(p) || sweep[i] > 89) {
			nfail++;
		}
	}
	kprintf("DF5778: B1 RESULT: %s (accepts exactly 0..89 incl. "
		"INVALID-dummy slot; rejects one-past-end 90 and above)\n",
		nfail ? "FAIL" : "PASS");

	kprintf("DF5778: ==== B2 adjacent guard canaries ====\n");
	kprintf("DF5778: B2 guard_lo=0x%08x guard_hi=0x%08x -> %s\n",
		df_table.guard_lo, df_table.guard_hi,
		(df_table.guard_lo == 0x11223344u &&
		 df_table.guard_hi == 0x55667788u) ?
		"PASS (intact)" : "FAIL (corrupted!)");

	kprintf("DF5778: ==== B3 DF-4731 macro cross-proof ====\n");
	kprintf("DF5778: B3 DAL_VALID_IRQ_SRC_NUM(90) = %s (macro "
		"off-by-one, DF-4731) / find_irq_source_info(90) = %s\n",
		DAL_VALID_IRQ_SRC_NUM(DAL_IRQ_SOURCES_NUMBER) ? "true" : "false",
		find_irq_source_info(&synth_svc,
			(enum dc_irq_source)DAL_IRQ_SOURCES_NUMBER) ?
			"ENTRY(!)" : "NULL");
	kprintf("DF5778: B3 dispatcher `>=` (irq_service.c:82) DEFUSES the "
		"macro off-by-one for the set/ack paths of this file\n");

	kprintf("DF5778: ==== B4 upstream v4.17 divergence ====\n");
	{
		/* upstream predicate: source > DAL_IRQ_SOURCES_NUMBER */
		enum dc_irq_source s = (enum dc_irq_source)90;
		int upstream_accepts = !(s > DAL_IRQ_SOURCES_NUMBER ||
					 s < DC_IRQ_SOURCE_INVALID);
		kprintf("DF5778: B4 upstream-v4.17 `>` predicate accepts "
			"src=90: %s (returns &info[90] = one-past-end); "
			"DFly `>=` rejects: %s\n",
			upstream_accepts ? "YES" : "no",
			find_irq_source_info(&synth_svc, s) == NULL ?
			"YES" : "NO");
	}

	kprintf("DF5778: ==== T1 THE FINDING: unguarded service deref ====\n");
	{
		/* replicate the irq_service.c:165 deref chain, fault-free:
		 * zero_svc models the object left behind when
		 * dal_irq_service_construct bails (irq_service.c:57-60) and
		 * the family constructor ignores it and wires info/funcs
		 * only — or, more simply, any ctx/funcs-less object. */
		const struct irq_service_funcs *f =
			*(const struct irq_service_funcs **)
			(char *)&zero_svc.funcs;
		size_t func_off =
			(size_t)((char *)&zero_svc.funcs - (char *)&zero_svc);
		kprintf("DF5778: T1 zeroed irq_service=%p svc->funcs "
			"(off+%zu) = %p\n", &zero_svc, func_off, f);
		if (f == NULL) {
			kprintf("DF5778: T1 VERDICT: dal_irq_service_to_irq_"
				"source (irq_service.c:165) double-derefs "
				"svc->funcs->to_dal_irq_source with NO guard: "
				"the verbatim line FAULTS on this object "
				"(latent NULL deref, DF-5778; unreachable "
				"via in-tree callers — see VERDICT.md)\n");
		} else {
			kprintf("DF5778: T1 unexpected non-NULL funcs\n");
		}
	}

	kprintf("DF5778: ==== T2 verbatim to_irq_source happy path ====\n");
	{
		enum dc_irq_source r = dal_irq_service_to_irq_source(
			&synth_svc, 0x7, 0);
		kprintf("DF5778: T2 src_id=0x7 -> %d (expect %d=HPD1): %s\n",
			r, DC_IRQ_SOURCE_HPD1,
			r == DC_IRQ_SOURCE_HPD1 ? "PASS" : "FAIL");
	}

	kprintf("DF5778: ==== T3 dummy-slot dispatch (slot 0 INVALID, "
		"slot 25 TIMER) ====\n");
	df_rec_reset();
	{
		bool r1 = dal_irq_service_set(&synth_svc,
				DC_IRQ_SOURCE_INVALID, true);
		bool r2 = dal_irq_service_ack(&synth_svc,
				DC_IRQ_SOURCE_TIMER);
		kprintf("DF5778: T3 set(INVALID)=%d ack(TIMER)=%d ; reg "
			"traffic: reads=%d writes=%d -> %s\n",
			r1, r2, df_nreads, df_nwrites,
			(!r1 && !r2 && df_nreads == 0 && df_nwrites == 0) ?
			"PASS (dummy entries log-and-fail; no reg access)" :
			"FAIL");
	}

	kprintf("DF5778: ==== T4 generic-slot dispatch (slot 1 HPD1) ====\n");
	df_rec_reset();
	{
		bool r = dal_irq_service_set(&synth_svc,
				DC_IRQ_SOURCE_HPD1, true);
		/* expected order (verbatim code): ack first (0xDEAD0002),
		 * then set (0xDEAD0001); fake reg file reads 0xA5A5A5A5:
		 * ack  write = 0xA5A5A5A5|0x10 = 0xA5A5A5B5
		 * set  write = (0xA5A5A5A5 & ~0x3)|0x3 = 0xA5A5A5A7 */
		kprintf("DF5778: T4 set(HPD1)=%d reads=%d writes=%d\n",
			r, df_nreads, df_nwrites);
		kprintf("DF5778: T4 ack:  r[0]=0x%08x w[0]=0x%08x "
			"wval[0]=0x%08x (expect r/w 0xDEAD0002, "
			"0xA5A5A5B5)\n",
			df_reg_read_addr[0], df_reg_write_addr[0],
			df_reg_write_val[0]);
		kprintf("DF5778: T4 set:  r[1]=0x%08x w[1]=0x%08x "
			"wval[1]=0x%08x (expect r/w 0xDEAD0001, "
			"0xA5A5A5A7)\n",
			df_reg_read_addr[1], df_reg_write_addr[1],
			df_reg_write_val[1]);
		kprintf("DF5778: T4 %s (generic RMW uses exactly the "
			"in-table synthetic regs)\n",
			(r == true && df_nreads == 2 && df_nwrites == 2 &&
			 df_reg_read_addr[0] == 0xDEAD0002u &&
			 df_reg_write_addr[0] == 0xDEAD0002u &&
			 df_reg_write_val[0] == 0xA5A5A5B5u &&
			 df_reg_read_addr[1] == 0xDEAD0001u &&
			 df_reg_write_addr[1] == 0xDEAD0001u &&
			 df_reg_write_val[1] == 0xA5A5A5A7u) ?
			"PASS" : "FAIL");
	}

	kprintf("DF5778: ==== all proofs complete ====\n");
	return 0;
}

static moduledata_t df5778_mod = {
	"df5778_harness",
	df5778_modevent,
	NULL
};
DECLARE_MODULE(df5778_harness, df5778_mod, SI_SUB_DRIVERS, SI_ORDER_ANY);
MODULE_VERSION(df5778_harness, 1);