Chapter 37

Proving it

The same step always gives the same frame, because the ride derives each frame from the four things it carries. In this chapter, we turn that sameness into a test strict enough to guard every change, down to the last pixel.

Each row is one frame of the ride. Ride to that step today, and you get that hash and that many shapes. The gate is the set of checks every change must pass before it lands, and one of them holds every row as it is.

A fixture is a value §

A test rides to any step with one call:

## The tour ridden from its start to `goal`, with the instants it passed
## behind it. The ride must not finish before `goal`.
at_step : Clock -> Tour
at_step = |goal| {
	var $tour = Tour.initial
	while Tour.instant($tour).clock != goal {
		$tour =
			match tour_after_step($tour) {
				Continued(next_tour) => next_tour
				Restarted(_) => crash "Tour.at_step: the ride finishes before step ${goal.to_str()}"
			}
	}
	$tour
}

Tour.at_step plays every step from the start up to the one asked for. Tour.step_forward rides on past the finish into a second lap, which is how the proof tools reach step 9,000. Tour.initial is a value, and each step returns a new tour, so the tour at step 1,529 is the same value in every test, on every run.

The frame hash §

The gate's proof tools are small Roc programs in gates/proof/. RasterFrame is one. It rides to a step and paints the frame into 576,000 pixels, 960 across and 600 down, in pure Roc, with SafariFrame and ShapesPixels, the Roc twin of the page's canvas. Then it prints a hash of them. The gate holds each hash to its line of gates/proof.expected, exactly. One different pixel in one frame fails it.

A frame proves only what's in it, so each step in the table is there for a scene. We add a row whenever a change could go wrong with every listed frame staying the same. The row at 3,698 is one: the truck brakes about 600 metres off, and its glow is about a pixel across.

Sums in order §

Exact hashes make the order of arithmetic matter: adding floating-point numbers in another order can change the last bit of the answer. Route.segments_with_ends adds up the route's lengths, and its doc comment says why its direction matters:

## Each of the route's segments, in order, with how far along the route it
## ends. It is the one sum of the route's lengths, which every other
## distance along the route reads. The lengths are added from the first
## segment on: a float sum's rounding depends on its order, and another order
## can move a pixel.
segments_with_ends : Route -> List({ segment : Segment, end : Distance })
segments_with_ends = |Route.(segments)|
	segments
		.fold(
			{ reached: Distance.zero, stretches: [] },
			|{ reached, stretches }, segment| {
				end = reached.plus(segment.length)
				{ reached: end, stretches: stretches.append({ segment, end }) }
			},
		)
		.stretches

A product's grouping counts as well. A beacon's angle is 2.0 * F64.pi * phase.to_f64() / Beacon.beacon_period.to_f64(). Divide the phase by the period first, and the product means the same on paper, but some beacons change in their last bits, and the gate's hash of the built page fails.

A value in an opaque type runs as the number inside it, so a change that retypes a module, to use Speed where it used plain F64s, leaves every hash where it was. That's why we rename, retype and reorganize the code freely: the compiler checks the types, and the hashes check every pixel.

Three more proofs §

ShapesFrame paints each frame twice, once with its polygons whole and once cut into triangles. The gate holds the count of pixels that differ at 0 of 576,000, at every step in the table.

StepBack steps back at points along the route, from step 10 to the finish. One step back from step 3,000 has to land on step 2,999, and as many steps back as the ride took have to land on step 0.

OnRoad rides the whole route and checks that the rider stays on the road from start to finish.

Tests beside the code §

The rest of the testing is plain expects. An expect sits at the top level of a module, under the code it checks, and roc test runs it. Safari Ride has over a thousand.

An expect can use only what its module imports, so a check that needs several modules goes in gates/expects/, a folder of modules made only for checks.

The gate makes every expect count. Each line in the source that starts with expect has to print PASS exactly once when roc test runs, so an expect has to sit in a module that a test run reaches.

Crashes that check §

Some beliefs about the program are cheaper to check as it runs. Every Fraction.of in the ride, from the “Errors as tag unions” chapter, enforces an invariant: a ratio outside 0 to 1 means a sum behind it is wrong, so the program stops, with a sentence that says so. The proof tools ride thousands of steps on every run of the gate, so each check on that path runs thousands of times.

The page itself §

This book is built from the code. Every snippet came through Roc's own parser, by name, and each program shown failing went through the compiler, with its message quoted as printed. The gate builds the book, so renaming a function quoted here fails the gate until the prose catches up.

The gate also runs lints, small programs that read the Roc source for patterns we've ruled out, each held at zero, so a vague name fails the gate before a single hash is worked out.