The state edge, live¶

True on the step a bool turns true: the signal now and not as the step began, rose = signal && !previous(signal) (lusine.events.rise). Events are lists: a game's own binding appends to its list where rose holds; Boules appends to its landings where a ball's landed rose. Below, sixteen signals are stepped on your GPU as you read, each from the bits of a word, bit t the signal in step t of a pass, for 32 steps and then false for 8, and the library's edge finds where each turns true: a run worked by hand, signals held true, held false and falling, and twelve random words drawn afresh each pass.

This page runs the program on your GPU through WebGPU, so it needs a browser with WebGPU (a recent Chrome, Edge, Safari or Firefox). Without it the program does not run and nothing is drawn below.

What it shows¶

The strip above the controls is green while every check holds, and turns red for good once one fails.
The edge: the chart draws the hand-worked signal, 0 0 1 1 1 0 1 0 0 1 1 then 0, and its rises over the last pass, a point a step: a rise on each step the signal turns true, none while it holds and none as it falls. Below it, the pass and the step within it.
The checks: worked by hand, the hand-worked signal rising at steps 2, 6 and 9 of each pass and no others; held true, once, a signal true from the first step rising there, from the pass's start, and never while it holds; held false, never; falling, once, a signal true for three steps and then false rising at its first step and not as it falls; every turning true, each signal's rises so far in the pass the turnings true its word holds up to the step, counted by bit arithmetic on the word: a bit set whose bit below is clear. Each is held at every step.

Every number here is computed by the program on the GPU; the page only reads the values back and draws them. The seed the random words are drawn from is the program's setting, which the host may write; this page offers no control to change it yet.

The program¶

The signals, the pass and the checks, the panels the page draws, and the one procedure, main, run each step: each signal's bit for the step, the library's edge, the rises counted against the word's turnings, and the checks.

// The state edge's live page: signals stepped from the bits of a word, one bit a step for 32 steps and then false for
// 8, the library's edge finding where each turns true, the rises held to a run worked by hand, to signals held true,
// held false and falling, and to the turnings true of random words counted by bit arithmetic, with the page's checks
// computed here on the GPU and shown by the panels the program declares.

namespace rise;

lusine.version version = { { number = 1 } };

// The reader's settings: the seed the random signals are drawn from.
host struct { integer seed = 3; } settings;

// The signals, each a word whose bit t is the signal in step t of a pass (a random word drawn each pass, where it is
// random): a run worked by hand, 0 0 1 1 1 0 1 0 0 1 1 then 0 (the word 1628, rising at steps 2, 6 and 9); held true
// (every bit, -1 as a signed word); held false (none); falling (true for three steps, the word 7); and twelve random
// words. Each signal now, whether it rose, the rises this pass, and the turnings true its word holds up to this step.
struct lane {
  integer number; bool random; integer word; bits trace; bool signal; bool rose; integer rises; integer turnings;
  bool held;
};
table<lane> lanes(capacity = 16) = {
  { number = 0, word = 1628 }, { number = 1, word = -1 }, { number = 2, word = 0 },
  { number = 3, word = 7 }, { number = 4, random = true }, { number = 5, random = true },
  { number = 6, random = true }, { number = 7, random = true }, { number = 8, random = true },
  { number = 9, random = true }, { number = 10, random = true }, { number = 11, random = true },
  { number = 12, random = true }, { number = 13, random = true }, { number = 14, random = true },
  { number = 15, random = true },
};

// The pass, and the step within it, from 0 to 39; the hand-worked signal and its rises, as numbers for the chart.
struct { integer pass; integer tick = -1; float signal; float rose; } edge;

// The checks: the hand-worked signal rising at steps 2, 6 and 9 and no others; held true rising once, at the first
// step; held false never; falling once, at the first step; and every signal's rises so far in the pass the turnings
// true its word holds up to the step, counted by bit arithmetic. Each at every step.
struct { bool by_hand = true; bool held = true; bool never = true; bool falling = true; bool turnings = true; }
  checks;

// A strip of lamps the page draws, lit green while every check holds and red once one fails.
struct lamp { vector<float, 4> colour; };
lattice<lamp, 2> lamps(spacing = 1 m, boundary = wall);

vector<float, 4> lamp_colour(bool holds)
{
  return holds ? vector<float, 4>(0.15, 0.6, 0.3, 1.0) : vector<float, 4>(0.75, 0.15, 0.15, 1.0);
}

// A pass's word: the fixed one, or a random one drawn for the pass.
bits traced(bits trace, bool random, integer word, integer seed, integer pass, integer number, integer tick)
{
  if (!random) return bits(word);
  if (tick != 0) return trace;
  return lusine.error.draw(seed = bits(seed), step = bits(pass), key = fnv1a("trace"), index = bits(number));
}

// The signal in a step: the word's bit at the step, for the first 32 steps of a pass, and false after.
bool sensed(bits trace, integer tick) { return tick < 32 && ((trace >> tick) & bits(1)) == bits(1); }

// The ones of a word, counted in parallel (Hacker's Delight, 5-1).
integer ones(bits word)
{
  let a = word - ((word >> 1) & bits);
  let b = (a & bits) + ((a >> 2) & bits);
  let c = (b + (b >> 4)) & bits;
  return integer((c * bits(16843009)) >> 24);
}

// The turnings true a word holds in its bits up to a step: a bit set whose bit below is clear (below bit 0, the pass's
// start, false), the bits past the step masked away.
integer turnings(bits trace, integer tick)
{
  let turned = trace & ~(trace << 1);
  let mask = tick >= 31 ? ~bits(0) : (bits(1) << (tick + 1)) - bits(1);
  return ones(word = turned & mask);
}

integer counted(integer rises, bool rose, integer tick)
{
  let before = tick == 0 ? 0 : rises;
  return rose ? before + 1 : before;
}

integer missed(table<bool> held) { return count(held) where !held; }
bool rose_of(table<bool> rose, table<integer> number, integer which)
{
  return any(rose) where rose && number == which;
}

integer rises_of(table<integer> rises, table<integer> number, integer which)
{
  return sum(rises) where number == which;
}

bool by_hand(bool rose, integer tick) { return rose == (tick == 2 || tick == 6 || tick == 9); }

output table<lusine.widget> panels = {
  lusine.series { { panel = "the edge", chart = "worked by hand", quantity = edge.signal, steps = 40,
                    label = "signal" } },
  lusine.series { { panel = "the edge", chart = "worked by hand", quantity = edge.rose, steps = 40, label = "rose" } },
  lusine.value { { panel = "the edge", quantity = edge.pass, label = "pass" } },
  lusine.value { { panel = "the edge", quantity = edge.tick, label = "step in the pass" } },
  lusine.value { { panel = "the checks", quantity = checks.by_hand, label = "worked by hand" } },
  lusine.value { { panel = "the checks", quantity = checks.held, label = "held true, once" } },
  lusine.value { { panel = "the checks", quantity = checks.never, label = "held false, never" } },
  lusine.value { { panel = "the checks", quantity = checks.falling, label = "falling, once" } },
  lusine.value { { panel = "the checks", quantity = checks.turnings, label = "every turning true" } },
};

void main()
{
  edge.tick = edge.tick >= 39 ? 0 : edge.tick + 1;
  lanes.trace = traced(lanes.trace, lanes.random, lanes.word, settings.seed, edge.pass, lanes.number, edge.tick);
  lanes.signal = sensed(lanes.trace, edge.tick);
  lanes.rose = lusine.events.rise(lanes.signal);
  lanes.rises = counted(lanes.rises, lanes.rose, edge.tick);
  lanes.turnings = turnings(lanes.trace, edge.tick);
  lanes.held = lanes.rises == lanes.turnings;
  edge.signal = rose_of(rose = lanes.signal, lanes.number, which = 0) ? 1.0 : 0.0;
  edge.rose = rose_of(lanes.rose, lanes.number, which = 0) ? 1.0 : 0.0;
  checks.by_hand = checks.by_hand && by_hand(rose = rose_of(lanes.rose, lanes.number, which = 0), edge.tick);
  checks.held = checks.held && rises_of(lanes.rises, lanes.number, which = 1) == 1;
  checks.never = checks.never && rises_of(lanes.rises, lanes.number, which = 2) == 0;
  checks.falling = checks.falling && rises_of(lanes.rises, lanes.number, which = 3) == 1;
  checks.turnings = checks.turnings && missed(lanes.held) == 0;
  edge.pass = edge.tick == 39 ? edge.pass + 1 : edge.pass;
  lamps.colour = lamp_colour(holds = checks.by_hand && checks.held && checks.never && checks.falling
                                     && checks.turnings);
}

The edge's other proof (two hundred random signals of 32 steps, item by item) is on its proof page.