// What a VERA reset leaves behind.
//
// video.c keeps three copies of the sprite attributes: the VRAM mirror the
// guest reads, a sprite_data[] shadow the renderer's raw source, and a
// sprite_properties[] array of values derived from that shadow. The hardware
// keeps one. Every extra copy is a chance for reset to clear some of them and
// leave the machine describing a state that no longer exists -- which has
// already happened once for layers, and is why video_reset_layer_pipeline()
// exists (video.c:255-260).
//
// This file checks that reset leaves nothing behind that still describes the
// pre-reset machine. Sprites are the subject because they are the only derived
// state with an observation channel that needs no framebuffer: a collision
// reaches ISR bits 7:4.
//
// ORACLE: B -- X16Community/vera-module Verilog, tag v47.0.2
// (45cc1f053376dae12173ea63612820e4d289c0da), for the claim that the hardware
// has nothing to go stale. sprite_renderer.v:73-85 decodes every attribute
// from sprite_attr, read from the attribute RAM as the sprite is rendered, and
// sprite_renderer.v:408-417 resets the renderer's own registers. There is no
// derived copy to refresh.
//
// One assertion needs no oracle at all and is marked as such below.

#include "support/video_fixture.h"
#include "support/harness.h"

#include "video.h"

#include <stdint.h>

#define VERA_CTRL 0x05
#define VERA_ISR  0x07

#define SPRITE_ATTR 0x1FC00
#define SPRITE_GFX  0x01000

#define ATTR_ZDEPTH 6

static void
step_frame(void)
{
	for (unsigned i = 0; i < 525; i++) {
		video_step(25.0f, 801.0f, false);
	}
}

// video_reset() fills VRAM with rand(), so the sprite bitmap has to be laid
// down after every reset or a collision would depend on the random contents
// rather than on what this file is measuring.
static void
opaque_graphics(void)
{
	for (unsigned i = 0; i < 16 * 8; i++) {
		video_space_write(SPRITE_GFX + i, 0x11);
	}
}

static void
place_sprite(unsigned n, uint8_t mask, uint8_t zdepth)
{
	const uint32_t attr = SPRITE_ATTR + n * 8;

	video_space_write(attr + 0, SPRITE_GFX >> 5);
	video_space_write(attr + 1, 0x00);
	video_space_write(attr + 2, 0x00);
	video_space_write(attr + 3, 0x00);
	video_space_write(attr + 4, 0x00);
	video_space_write(attr + 5, 0x00);
	video_space_write(attr + ATTR_ZDEPTH, (uint8_t)(mask | (zdepth << 2)));
	video_space_write(attr + 7, 0x50);
}

static void
enable_sprites(void)
{
	video_write(VERA_CTRL, 0x00);
	video_write(0x09, 0x41); // DCSEL 0, $9F29: sprites on, VGA output
}

// Two sprites on the same pixels with masks that share bits 6 and 4, so a
// collision reports 0x50 in ISR bits 7:4.
static void
arm_colliding_sprites(void)
{
	opaque_graphics();
	place_sprite(0, 0x70, 1);
	place_sprite(1, 0xD0, 1);
	enable_sprites();
}

static uint8_t
collision_after_a_frame(void)
{
	step_frame();
	return video_read(VERA_ISR, true) & 0xF0;
}

// The control. Everything below rests on a collision being visible when the
// sprites are there and absent when they are not, so prove the channel before
// using it to measure a reset.
static void
test_the_collision_channel_follows_the_attributes(void)
{
	video_reset();
	arm_colliding_sprites();
	check_eq(collision_after_a_frame(), 0x50, "two armed sprites collide");

	// A guest taking a sprite out of the picture is an ordinary attribute
	// write, and the renderer follows it.
	place_sprite(1, 0xD0, 0);
	check_eq(collision_after_a_frame(), 0x00, "and stop when one is given no z-depth");
}

// The renderer holds no attribute state of its own -- sprite_renderer.v:73-85
// decodes each one out of the attribute RAM as it goes -- so clearing the
// attributes is enough to stop a sprite, and a reset that clears them must
// stop it too.
static void
test_reset_stops_sprites_configured_before_it(void)
{
	video_reset();
	arm_colliding_sprites();
	check_eq(collision_after_a_frame(), 0x50, "sprites collide before the reset");

	video_reset();
	opaque_graphics();
	enable_sprites();

	check_divergent(collision_after_a_frame() == 0x00,
	                "a reset stops sprites that were running before it",
	                "video.c:339 clears sprite_data but never re-derives "
	                "sprite_properties, whose only writers are the two "
	                "video_space_write() paths at video.c:2396 and video.c:2425, so "
	                "the renderer keeps drawing the pre-reset sprites");
}

// ORACLE: none, and none is needed. Storing a byte that is already there is a
// no-op by definition, whatever the hardware does with it. This is the same
// statement as above with the reset taken out of it, so it holds even if the
// reset value is ever argued about.
static void
test_writing_a_byte_that_is_already_there_changes_nothing(void)
{
	video_reset();
	arm_colliding_sprites();
	step_frame();

	video_reset();
	opaque_graphics();
	enable_sprites();

	const uint8_t before = collision_after_a_frame();

	// sprite_data[] reads back as zero for both sprites after the reset, so
	// this stores the value already held.
	video_space_write(SPRITE_ATTR + 0 * 8 + ATTR_ZDEPTH, 0x00);
	video_space_write(SPRITE_ATTR + 1 * 8 + ATTR_ZDEPTH, 0x00);

	check_divergent(collision_after_a_frame() == before,
	                "rewriting an attribute byte with its own value does not move the machine",
	                "the write re-derives sprite_properties, which the reset did not, so "
	                "storing a zero over a zero is what actually stops the sprites");
}

// The frame accumulator is cleared (video.c:355), matching
// sprite_renderer.v:416. Recorded so the two halves of the reset are not
// confused: this one is right, the derived attributes are not.
static void
test_reset_clears_the_collision_accumulator(void)
{
	video_reset();
	arm_colliding_sprites();

	// Part of a frame, so collisions are accumulated but not yet latched.
	for (unsigned i = 0; i < 32; i++) {
		video_step(25.0f, 801.0f, false);
	}

	video_reset();

	// Reading ISR here would say nothing -- reset clears ISR itself, so the
	// nibble is zero whatever the accumulator holds. The accumulator is only
	// visible once a vblank latches it, so run a frame. The reset also turned
	// sprites off, so nothing new can accumulate during it and what latches is
	// exactly what the reset left behind.
	check_eq(collision_after_a_frame(), 0x00, "reset clears the pending collisions");
}

int
main(void)
{
	test_the_collision_channel_follows_the_attributes();
	test_reset_stops_sprites_configured_before_it();
	test_writing_a_byte_that_is_already_there_changes_nothing();
	test_reset_clears_the_collision_accumulator();
	return x16_test_summary("vera_reset");
}