Pixel expressions compile to native x86-64 for TempleOS through an Isabelle/HOL compiler, with proofs of constant folding, register allocation, bounded branching and instruction-level execution of the emitted bytes

Build

make check
make payload

It uses:

• Isabelle2026 and its bundled Poly/ML toolchain
• Python

Copy .build/payload/* onto C:/ in TempleOS and run:

#include "C:/Remy.HC";
Verify;
Show(0);

Usage

The byte interpreter follows encoded jumps and consumes a synthetic return address through ret. Compare its result with eval using the same x, y and t arguments

.build/remy examples/Rings.remy /tmp/rings.bin
.build/remy simulate /tmp/rings.bin 17 23 41
.build/remy eval examples/Rings.remy 17 23 41

Both evaluations return 3. make measure compares the original stack backend with the current compiler on the three examples and reports bytes, static stack instructions and median host pixel-kernel time

Live

The HOL packet builder serialises native code, its source snapshot and 512 reference rows for the trusted local compiler. The guest checks lengths, a checksum and every reference result before switching shaders between frames

make guest tests a copy of an official TempleOS RedSea ISO and leaves a bootable image that starts Live(0) automatically. Start that image with COM1 attached to a Unix socket, then edit the watched source file

make guest TEMPLE_ISO=/path/to/TempleOS.ISO
qemu-system-x86_64 -m 512 -smp 2 -cdrom .build/guest.iso \
  -chardev socket,id=live,path=/tmp/remy.sock,server=on,wait=off \
  -serial chardev:live &
python3 cli/watch.py examples/Rings.remy --socket /tmp/remy.sock

The watcher keeps one transfer in flight and coalesces edits while awaiting its acknowledgement. Syntax errors and rejected packets leave the current shader running, and Escape stops the guest renderer and receiver

Correctness

Lexical bindings share the evaluation stack with spilled intermediates. The allocator keeps one intermediate in a register and adjusts variable offsets when it must spill, while the branching compiler preserves the incoming frame and returns the expression result

The encoder proves inversion and byte bounds for immediate operands and stack displacements, while native lowering uses the following register convention to keep pixel inputs available across expression evaluation

Registers	Role
r8, r9, rdx	Preserved inputs x, y, t
rax	Accumulator and result
rcx, rbx	Scratch

Arithmetic wraps modulo 2^64 and shifts mask their count to six bits

Nonconstant conditionals use forward jz and jmp instructions so only the selected arm runs. The validator checks both arms for matching stack heights and protected input registers, with a proved 512-word bound above the caller frame. The HolyC runner masks each result to four bits for the TempleOS palette

The x86 model follows the Intel instruction descriptions for the emitted subset using a word-addressed stack. The proved function body preserves its incoming stack and pointer, then ret removes the return address and advances that pointer by eight bytes. Arithmetic flags that the compiler never reads are abstracted, and hardware faults, the HolyC bridge, extraction and the OS remain outside the proof