From edf26390ae3eb8281b7adc9bb0e40f56de1941a8 Mon Sep 17 00:00:00 2001 From: james Date: Sun, 1 Nov 2026 02:59:43 +0000 Subject: [PATCH] feat(allocator): retain intermediates in registers and spill nested values --- Makefile | 7 +- README.md | 4 +- ROOT | 13 ++-- cli/driver.ML | 3 +- src/Allocation.thy | 123 ++++++++++++++++++++++++++++++++++++ src/Export.thy | 2 +- src/Frontend.thy | 19 ++++-- src/{ => core}/Checker.thy | 0 src/{ => core}/Compiler.thy | 0 src/{ => core}/Encoding.thy | 0 src/{ => core}/Model.thy | 0 src/{ => core}/Native.thy | 0 tests/cli.py | 5 ++ tests/measure.c | 72 +++++++++++++++++++++ tests/measure.py | 42 ++++++++++++ tests/native.py | 3 + 16 files changed, 276 insertions(+), 17 deletions(-) create mode 100644 src/Allocation.thy rename src/{ => core}/Checker.thy (100%) rename src/{ => core}/Compiler.thy (100%) rename src/{ => core}/Encoding.thy (100%) rename src/{ => core}/Model.thy (100%) rename src/{ => core}/Native.thy (100%) create mode 100644 tests/measure.c create mode 100644 tests/measure.py diff --git a/Makefile b/Makefile index 4c2636fec4244d9ff27459dcdef9595a11d1ff0d..1e5c4a2fa286df67ab86e8419a1a9d31e9f7c310 100644 --- a/Makefile +++ b/Makefile @@ -1,10 +1,10 @@ ISABELLE ?= isabelle -.PHONY: all check payload clean +.PHONY: all check measure payload clean all: .build/ready -.build/ready: ROOT $(wildcard src/*.thy) cli/driver.ML Makefile +.build/ready: ROOT $(wildcard src/*.thy src/core/*.thy) cli/driver.ML Makefile @test "$$('$(ISABELLE)' version)" = Isabelle2026 "$(ISABELLE)" build -D . -j 1 -o threads=1 -o parallel_proofs=0 "$(ISABELLE)" export -n -d . -O .build -x 'Remy.Export:code/remy.ML' Remy @@ -15,6 +15,9 @@ check: all python3 tests/native.py python3 tests/cli.py +measure: all + python3 tests/measure.py + payload: all @mkdir -p .build/payload @set -e; for name in Rings Weave Cells; do .build/remy examples/$$name.remy .build/payload/$$name.BIN; .build/remy vectors examples/$$name.remy .build/payload/$$name.DAT; cp examples/$$name.remy .build/payload/$$name.TXT; done diff --git a/README.md b/README.md index e1f6882183a63819d949bb162dc51ac51ae74402..c73138d1a7a6e58d6522ad3af2ba699827675b26 100644 --- a/README.md +++ b/README.md @@ -23,9 +23,9 @@ Show(0); ## Correctness -Each `let` pushes a binding onto the evaluation stack. [Compilation](src/Compiler.thy) adjusts variable offsets as intermediate values accumulate above those bindings and proves that execution leaves the result followed by the original stack whereas accepted programs stay within 512 evaluation words at every instruction boundary +Each `let` pushes a binding onto the evaluation stack. [Compilation](src/core/Compiler.thy) adjusts variable offsets as intermediate values accumulate above those bindings and proves that execution leaves the result followed by the original stack whereas accepted programs stay within 512 evaluation words at every instruction boundary -[Native lowering](src/Native.thy) puts the result in `rax` and preserves `r8`, `r9` and `rdx` which carry `x`, `y` and `t`. The temporary registers are `rax`, `rcx` and `rbx` while the [Encoding](src/Encoding.thy) proves decoder inversion and byte bounds for the emitted blocks including their immediate operands and stack displacements +[Native lowering](src/core/Native.thy) puts the result in `rax` and preserves `r8`, `r9` and `rdx` which carry `x`, `y` and `t`. The temporary registers are `rax`, `rcx` and `rbx` while the [Encoding](src/core/Encoding.thy) proves decoder inversion and byte bounds for the emitted blocks including their immediate operands and stack displacements ![Source eval](media/correspondence.svg) diff --git a/ROOT b/ROOT index 8c8ff3030ab35903f85b5ca2564fb7d38db787ed..17e99d32826e9a232063e02d3b4b8d00f584fdc5 100644 --- a/ROOT +++ b/ROOT @@ -1,19 +1,20 @@ -session Remybase = HOL + +session Remybase in "src/core" = HOL + options [document = false] sessions "HOL-Library" theories "HOL-Library.Word" "HOL-Library.Code_Target_Numeral" - -session Remy in src = Remybase + - options [document = false] - sessions "HOL-Library" - theories Model Compiler Native Encoding Checker + +session Remy in src = Remybase + + options [document = false] + sessions "HOL-Library" + theories + Allocation Frontend Examples Export diff --git a/cli/driver.ML b/cli/driver.ML index 493b9abaad5bab3d5ecaf8c97eb661d5bb1e25b8..a6fdd8790a436ed4f8ec9eef28e19ca34e1201a7 100644 --- a/cli/driver.ML +++ b/cli/driver.ML @@ -71,8 +71,9 @@ fun main () = emit destination (Remy.configured (chars depth) (chars nodes) (chars stack) (read source)) | ["check", binary] => output (Remy.validate (read binary)) | ["disassemble", binary] => output (Remy.disassemble (read binary)) + | ["baseline", source, destination] => emit destination (Remy.baseline (read source)) | [source, destination] => emit destination (Remy.artifact (read source)) - | _ => raise Fail "usage: remy check binary | remy disassemble binary | remy limits depth nodes stack source binary | remy source binary | remy vectors source data | remy eval source x y t (source - reads standard input)") + | _ => raise Fail "usage: remy check binary | remy disassemble binary | remy baseline source binary | remy limits depth nodes stack source binary | remy source binary | remy vectors source data | remy eval source x y t (source - reads standard input)") handle exn => (TextIO.output (TextIO.stdErr, "remy: " ^ General.exnMessage exn ^ "\n"); OS.Process.exit OS.Process.failure); diff --git a/src/Allocation.thy b/src/Allocation.thy new file mode 100644 index 0000000000000000000000000000000000000000..8996ec6735e13f9713bf06a39244fe4bbedb29ad --- /dev/null +++ b/src/Allocation.thy @@ -0,0 +1,123 @@ +theory Allocation + imports "Remybase.Checker" +begin + +fun allocate :: "bool \ expression \ nat list \ opcode list" where + "allocate free (Literal v) slots = [Immediate v]" +| "allocate free (Input i) slots = [Move Rax (input_register i)]" +| "allocate free (Variable i) slots = [Peek (slots ! i)]" +| "allocate free (Binary op a b) slots = (if free then + allocate True a slots @ [Move Rbx Rax] @ allocate False b slots @ + [Move Rcx Rbx, Arithmetic op] + else allocate False a slots @ [Push Rax] @ allocate False b (map Suc slots) @ + [Pop Rcx, Arithmetic op])" +| "allocate free (Cond c a b) slots = [Push Rbx] @ + allocate True c (map Suc slots) @ [Push Rax] @ + allocate True a (map (\i. Suc (Suc i)) slots) @ [Push Rax] @ + allocate True b (map (\i. Suc (Suc (Suc i))) slots) @ + [Pop Rcx, Pop Rbx, Conditional, Pop Rbx]" +| "allocate free (Let a b) slots = allocate free a slots @ [Push Rax] @ + allocate free b (0 # map Suc slots) @ [Pop Rcx]" + +definition allocated_result :: "bool \ expression \ pixel list \ machine \ machine \ bool" where + "allocated_result free e env s q \ + registers q Rax = evaluate e env (inputs s) \ stack q = stack s \ + inputs q = inputs s \ (\ free \ registers q Rbx = registers s Rbx)" + +theorem allocate_correct: + assumes "scoped (length env) e" "represents slots (stack s) env" + shows "\q. run (allocate free e slots) s = Some q \ allocated_result free e env s q" + using assms +proof (induction e arbitrary: free slots env s) + case (Literal v) + then show ?case by (auto simp: allocated_result_def) +next + case (Input i) + then show ?case by (auto simp: allocated_result_def inputs_def fun_eq_iff) +next + case (Variable i) + then show ?case by (auto simp: allocated_result_def represents_def) +next + case (Binary op a b) + obtain p where a: "run (allocate free a slots) s = Some p" + and p: "allocated_result free a env s p" + using Binary.IH(1)[of env slots s free] Binary.prems by auto + show ?case + proof (cases free) + case True + let ?p = "p\registers := (registers p)(Rbx := registers p Rax)\" + obtain q where b: "run (allocate False b slots) ?p = Some q" + and q: "allocated_result False b env ?p q" + using Binary.IH(2)[of env slots ?p False] Binary.prems p + by (auto simp: allocated_result_def) + show ?thesis using a b p q True + by (auto simp: allocated_result_def run_append; auto simp: inputs_def fun_eq_iff) + next + case False + let ?p = "p\stack := registers p Rax # stack p\" + obtain q where b: "run (allocate False b (map Suc slots)) ?p = Some q" + and q: "allocated_result False b env ?p q" + using Binary.IH(2)[of env "map Suc slots" ?p False] Binary.prems p + represents_push[OF Binary.prems(2), of "registers p Rax"] + by (auto simp: allocated_result_def) + show ?thesis using a b p q False + by (auto simp: allocated_result_def run_append; auto simp: inputs_def fun_eq_iff) + qed +next + case (Cond c a b) + have sc: "scoped (length env) c" and sa: "scoped (length env) a" + and sb: "scoped (length env) b" using Cond.prems by auto + let ?s = "s\stack := registers s Rbx # stack s\" + have repc: "represents (map Suc slots) (stack ?s) env" + using represents_push[OF Cond.prems(2)] by simp + obtain p where c: "run (allocate True c (map Suc slots)) ?s = Some p" + and p: "allocated_result True c env ?s p" + using Cond.IH(1)[of env "map Suc slots" ?s True] sc repc by blast + let ?p = "p\stack := registers p Rax # stack p\" + have repa: "represents (map (\i. Suc (Suc i)) slots) (stack ?p) env" + using Cond.prems(2) p by (auto simp: allocated_result_def represents_def) + obtain q where a: "run (allocate True a (map (\i. Suc (Suc i)) slots)) ?p = Some q" + and q: "allocated_result True a env ?p q" + using Cond.IH(2)[of env "map (\i. Suc (Suc i)) slots" ?p True] sa repa by blast + let ?q = "q\stack := registers q Rax # stack q\" + have repb: "represents (map (\i. Suc (Suc (Suc i))) slots) (stack ?q) env" + using Cond.prems(2) p q by (auto simp: allocated_result_def represents_def) + obtain r where b: "run (allocate True b (map (\i. Suc (Suc (Suc i))) slots)) ?q = Some r" + and r: "allocated_result True b env ?q r" + using Cond.IH(3)[of env "map (\i. Suc (Suc (Suc i))) slots" ?q True] sb repb by blast + show ?case using c a b p q r + by (auto simp: allocated_result_def run_append; auto simp: inputs_def fun_eq_iff) +next + case (Let a b) + obtain p where a: "run (allocate free a slots) s = Some p" + and p: "allocated_result free a env s p" + using Let.IH(1)[of env slots s free] Let.prems by auto + let ?p = "p\stack := registers p Rax # stack p\" + obtain q where b: "run (allocate free b (0 # map Suc slots)) ?p = Some q" + and q: "allocated_result free b (registers p Rax # env) ?p q" + using Let.IH(2)[of "registers p Rax # env" "0 # map Suc slots" ?p free] + Let.prems p represents_bind[OF Let.prems(2), of "registers p Rax"] + by (auto simp: allocated_result_def) + show ?case using a b p q + by (auto simp: allocated_result_def run_append; auto simp: inputs_def fun_eq_iff) +qed + +definition allocated :: "expression \ opcode list" where + "allocated e = transfers (allocate True (optimise e) [])" + +theorem allocated_return: + "scoped 0 e \ \q. run (allocated e) s = Some q \ + registers q Rax = evaluate e [] (inputs s) \ stack q = stack s \ inputs q = inputs s" + using allocate_correct[where env="[]" and slots="[]" and free=True and e="optimise e"] + optimise_scoped + by (auto simp: allocated_def transfers_correct allocated_result_def represents_def optimise_correct) + +definition allocated_bytes :: "expression \ nat list" where + "allocated_bytes e = concat (map encode (allocated e)) @ [195]" + +lemma allocated_add: + "allocated (Binary Add (Input X) (Input Y)) = + [Move Rax R8, Move Rbx Rax, Move Rax R9, Move Rcx Rbx, Arithmetic Add]" + by eval + +end diff --git a/src/Export.thy b/src/Export.thy index 59645e51ace074e1b2eb1209334a656c7633b4b5..fc998bf86c76156cb000a945530ba76398fa910a 100644 --- a/src/Export.thy +++ b/src/Export.thy @@ -6,6 +6,6 @@ definition ascii :: "integer \ char" where "ascii = char_of" definition ordinal :: "char \ integer" where "ordinal = of_char" -export_code validate disassemble configured artifact vectors reference ascii ordinal in SML module_name Remy file_prefix remy +export_code validate disassemble configured artifact baseline vectors reference ascii ordinal in SML module_name Remy file_prefix remy end diff --git a/src/Frontend.thy b/src/Frontend.thy index 6736bff479cbe7313ce5d7b19aa6b4bf446de24c..d3da4b74eb6fd2be8d1e5784fdb5be9ad286bb1e 100644 --- a/src/Frontend.thy +++ b/src/Frontend.thy @@ -1,5 +1,5 @@ theory Frontend - imports Checker + imports Allocation begin fun finish :: "string \ string list \ string list" where @@ -35,8 +35,11 @@ definition number :: "string \ nat option" where if a = CHR ''0'' \ (b = CHR ''x'' \ b = CHR ''X'') then parse_digits 16 rest else parse_digits 10 s | _ \ parse_digits 10 s)" +lemma parse_digits_bound: "parse_digits base s = Some n \ n < 2 ^ 64" + by (auto simp only: parse_digits_def Let_def option.inject option.distinct split: if_splits) + theorem number_bound: "number s = Some n \ n < 2 ^ 64" - by (auto simp: number_def parse_digits_def Let_def split: list.splits if_splits) + using parse_digits_bound by (auto simp: number_def split: list.splits if_splits) definition valid_name :: "string \ bool" where "valid_name s = (case s of [] \ False | c # cs \ @@ -269,9 +272,11 @@ definition source_error_with :: "limits \ string \ strin definition artifact_with :: "limits \ string \ (bool \ string) \ string" where "artifact_with lim s = (case prepare_with lim s of None \ ((False,[]), source_error_with lim s) - | Some e \ let opt = optimise e; bytes = executable e in - ((True, map char_of_nat bytes), decimal (nodes e) @ '' nodes -> '' @ decimal (nodes opt) @ - '' nodes, '' @ decimal (length bytes) @ '' bytes, '' @ decimal (demand opt) @ '' stack words'' @ newline))" + | Some e \ let opt = optimise e; code = allocated e; bytes = allocated_bytes e in + if audit code 0 = Some 0 \ list_all encodable code then + ((True, map char_of_nat bytes), decimal (nodes e) @ '' nodes -> '' @ decimal (nodes opt) @ + '' nodes, '' @ decimal (length bytes) @ '' bytes, '' @ decimal (demand opt) @ '' stack words'' @ newline) + else ((False,[]),''allocated code exceeds native limits'' @ newline))" definition source_error :: "string \ string" where "source_error = source_error_with defaults" @@ -279,6 +284,10 @@ definition source_error :: "string \ string" where definition artifact :: "string \ (bool \ string) \ string" where "artifact = artifact_with defaults" +definition baseline :: "string \ (bool \ string) \ string" where + "baseline s = (case prepare s of None \ ((False,[]),source_error s) + | Some e \ ((True,map char_of_nat (executable e)),''stack backend'' @ newline))" + definition configured :: "string \ string \ string \ string \ (bool \ string) \ string" where "configured depth count stacktext source = (case (number depth, number count, number stacktext) of (Some d,Some n,Some k) \ artifact_with \depth_budget=d, node_budget=n, stack_budget=k\ source diff --git a/src/Checker.thy b/src/core/Checker.thy similarity index 100% rename from src/Checker.thy rename to src/core/Checker.thy diff --git a/src/Compiler.thy b/src/core/Compiler.thy similarity index 100% rename from src/Compiler.thy rename to src/core/Compiler.thy diff --git a/src/Encoding.thy b/src/core/Encoding.thy similarity index 100% rename from src/Encoding.thy rename to src/core/Encoding.thy diff --git a/src/Model.thy b/src/core/Model.thy similarity index 100% rename from src/Model.thy rename to src/core/Model.thy diff --git a/src/Native.thy b/src/core/Native.thy similarity index 100% rename from src/Native.thy rename to src/core/Native.thy diff --git a/tests/cli.py b/tests/cli.py index 61e8d8eb7986efb37d5e43ff6c31dc4443398264..8a08a79998a552cc3e15360d300828d08a30698a 100644 --- a/tests/cli.py +++ b/tests/cli.py @@ -53,6 +53,11 @@ def main(): invoke(source,binary) listing = invoke('disassemble',binary) assert 'mov rax r9' in listing and 'arithmetic add' in listing and 'ret' in listing + assert 'push' not in listing and 'pop' not in listing + source.write_text('(- x (- y (- t x)))') + invoke(source,binary) + listing = invoke('disassemble',binary) + assert 'push rax' in listing and 'pop rcx' in listing for malformed in [b'',bytes([195,0]),bytes([72,199,192,0]),bytes([80])]: binary.write_bytes(malformed) assert 'invalid native' in invoke('disassemble',binary,ok=False) diff --git a/tests/measure.c b/tests/measure.c new file mode 100644 index 0000000000000000000000000000000000000000..8f9cf4fefe63efabe171108926e00109138cf84e --- /dev/null +++ b/tests/measure.c @@ -0,0 +1,72 @@ +#define _GNU_SOURCE +#include +#include +#include +#include +#include +#include +#include +#include + +static uint64_t ticks(void) +{ + struct timespec now; + if (clock_gettime(CLOCK_MONOTONIC, &now)) { + perror("clock_gettime"); + exit(1); + } + return (uint64_t)now.tv_sec * UINT64_C(1000000000) + now.tv_nsec; +} + +int main(int argc, char **argv) +{ + if (argc != 2) return 1; + FILE *file = fopen(argv[1], "rb"); + if (!file) return 1; + if (fseek(file, 0, SEEK_END)) { + fclose(file); + return 1; + } + long size = ftell(file); + long page = sysconf(_SC_PAGESIZE); + if (size <= 0 || size > 65536 || page <= 0 || fseek(file, 0, SEEK_SET)) { + fclose(file); + return 1; + } + size_t offset = ((size_t)size + page - 1) / page * page; + size_t capacity = offset + page; + unsigned char *image = mmap(NULL, capacity, PROT_READ | PROT_WRITE, + MAP_PRIVATE | MAP_ANONYMOUS, -1, 0); + if (image == MAP_FAILED) { + fclose(file); + return 1; + } + int failed = fread(image, 1, size, file) != (size_t)size; + failed |= fclose(file) != 0; + if (failed) { + munmap(image, capacity); + return 1; + } + unsigned char bridge[] = {0x53,0x49,0x89,0xf8,0x49,0x89,0xf1,0x48,0xb8, + 0,0,0,0,0,0,0,0,0xff,0xd0,0x5b,0xc3}; + uint64_t address = (uintptr_t)image; + memcpy(bridge + 9, &address, sizeof(address)); + memcpy(image + offset, bridge, sizeof(bridge)); + if (mprotect(image, capacity, PROT_READ | PROT_EXEC)) { + munmap(image, capacity); + return 1; + } + uint64_t (*pixel)(uint64_t, uint64_t, uint64_t) = (void *)(image + offset); + uint64_t checksum = 0; + uint64_t begin = ticks(); + for (uint64_t t = 0; t < 64; t++) { + for (uint64_t y = 0; y < 112; y++) { + for (uint64_t x = 0; x < 160; x++) { + checksum += pixel(x, y, 2*t) & 15; + } + } + } + uint64_t elapsed = ticks() - begin; + printf("%" PRIu64 " %" PRIu64 "\n", elapsed / 64, checksum); + return munmap(image, capacity) != 0; +} diff --git a/tests/measure.py b/tests/measure.py new file mode 100644 index 0000000000000000000000000000000000000000..53018d8ae1499db97a0d1dd747d6b9c4d9850b28 --- /dev/null +++ b/tests/measure.py @@ -0,0 +1,42 @@ +from pathlib import Path +import statistics +import subprocess +import tempfile + + +ROOT = Path(__file__).resolve().parents[1] + + +def main(): + with tempfile.TemporaryDirectory() as directory: + directory = Path(directory) + runner = directory / 'measure' + subprocess.run(['cc', '-std=c11', '-O2', '-Wall', '-Wextra', '-Werror', + ROOT / 'tests/measure.c', '-o', runner], check=True) + print('example backend bytes stack_instructions median_frame_ns checksum') + for source in sorted((ROOT / 'examples').glob('*.remy')): + checksums = set() + for backend in ('baseline', 'allocated'): + binary = directory / backend + args = ['baseline'] if backend == 'baseline' else [] + subprocess.run([ROOT / '.build/remy', *args, source, binary], + check=True, capture_output=True) + subprocess.run([ROOT / '.build/remy', 'check', binary], + check=True, capture_output=True) + listing = subprocess.run([ROOT / '.build/remy', 'disassemble', binary], + check=True, capture_output=True, text=True).stdout + traffic = sum(' push ' in row or ' pop ' in row for row in listing.splitlines()) + samples = [] + for _ in range(9): + result = subprocess.run([runner, binary], check=True, capture_output=True, + text=True, timeout=30) + elapsed, checksum = map(int, result.stdout.split()) + samples.append(elapsed) + checksums.add(checksum) + print(source.stem, backend, binary.stat().st_size, traffic, + int(statistics.median(samples)), checksum) + assert len(checksums) == 1, (source, checksums) + + +if __name__ == '__main__': + main() diff --git a/tests/native.py b/tests/native.py index a2eed95bce29f2ac12c0321dd23f27c1bb27ea3f..626496abf5ceb046eec097cd0bde8d70b5802ee4 100644 --- a/tests/native.py +++ b/tests/native.py @@ -122,6 +122,9 @@ def main(): cases += [("let", "x1", ("+", "x", 1), ("*", "x1", "x1"))] cases += [("let", "a", ("+", "x", 3), ("+", "y", ("let", "b", "t", ("*", "a", "b")))), ("let", "x", "y", ("if", "t", ("+", "x", 1), ("-", "x", 1)))] + cases += [("-", "x", ("if", "t", ("+", "x", "y"), ("*", "y", "t"))), + ("shl", "x", ("let", "a", ("+", "y", "t"), ("-", "a", "x"))), + ("let", "a", "x", ("+", ("if", "y", "a", "t"), ("if", "t", "y", "a")))] cases += [generate(rng, 5, ["x", "y", "t"]) for _ in range(117)] atoms = (0,1,MASK,'x','y','t') exhaustive = list(atoms)