M Makefile => Makefile +5 -2
@@ 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
M README.md => README.md +2 -2
@@ 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
M ROOT => ROOT +7 -6
@@ 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
M cli/driver.ML => cli/driver.ML +2 -1
@@ 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);
A src/Allocation.thy => src/Allocation.thy +123 -0
@@ 0,0 1,123 @@
+theory Allocation
+ imports "Remybase.Checker"
+begin
+
+fun allocate :: "bool \<Rightarrow> expression \<Rightarrow> nat list \<Rightarrow> 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 (\<lambda>i. Suc (Suc i)) slots) @ [Push Rax] @
+ allocate True b (map (\<lambda>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 \<Rightarrow> expression \<Rightarrow> pixel list \<Rightarrow> machine \<Rightarrow> machine \<Rightarrow> bool" where
+ "allocated_result free e env s q \<longleftrightarrow>
+ registers q Rax = evaluate e env (inputs s) \<and> stack q = stack s \<and>
+ inputs q = inputs s \<and> (\<not> free \<longrightarrow> registers q Rbx = registers s Rbx)"
+
+theorem allocate_correct:
+ assumes "scoped (length env) e" "represents slots (stack s) env"
+ shows "\<exists>q. run (allocate free e slots) s = Some q \<and> 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\<lparr>registers := (registers p)(Rbx := registers p Rax)\<rparr>"
+ 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\<lparr>stack := registers p Rax # stack p\<rparr>"
+ 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\<lparr>stack := registers s Rbx # stack s\<rparr>"
+ 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\<lparr>stack := registers p Rax # stack p\<rparr>"
+ have repa: "represents (map (\<lambda>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 (\<lambda>i. Suc (Suc i)) slots)) ?p = Some q"
+ and q: "allocated_result True a env ?p q"
+ using Cond.IH(2)[of env "map (\<lambda>i. Suc (Suc i)) slots" ?p True] sa repa by blast
+ let ?q = "q\<lparr>stack := registers q Rax # stack q\<rparr>"
+ have repb: "represents (map (\<lambda>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 (\<lambda>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 (\<lambda>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\<lparr>stack := registers p Rax # stack p\<rparr>"
+ 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 \<Rightarrow> opcode list" where
+ "allocated e = transfers (allocate True (optimise e) [])"
+
+theorem allocated_return:
+ "scoped 0 e \<Longrightarrow> \<exists>q. run (allocated e) s = Some q \<and>
+ registers q Rax = evaluate e [] (inputs s) \<and> stack q = stack s \<and> 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 \<Rightarrow> 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
M src/Export.thy => src/Export.thy +1 -1
@@ 6,6 6,6 @@ definition ascii :: "integer \<Rightarrow> char" where "ascii = char_of"
definition ordinal :: "char \<Rightarrow> 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
M src/Frontend.thy => src/Frontend.thy +14 -5
@@ 1,5 1,5 @@
theory Frontend
- imports Checker
+ imports Allocation
begin
fun finish :: "string \<Rightarrow> string list \<Rightarrow> string list" where
@@ 35,8 35,11 @@ definition number :: "string \<Rightarrow> nat option" where
if a = CHR ''0'' \<and> (b = CHR ''x'' \<or> b = CHR ''X'') then parse_digits 16 rest
else parse_digits 10 s | _ \<Rightarrow> parse_digits 10 s)"
+lemma parse_digits_bound: "parse_digits base s = Some n \<Longrightarrow> 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 \<Longrightarrow> 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 \<Rightarrow> bool" where
"valid_name s = (case s of [] \<Rightarrow> False | c # cs \<Rightarrow>
@@ 269,9 272,11 @@ definition source_error_with :: "limits \<Rightarrow> string \<Rightarrow> strin
definition artifact_with :: "limits \<Rightarrow> string \<Rightarrow> (bool \<times> string) \<times> string" where
"artifact_with lim s = (case prepare_with lim s of None \<Rightarrow> ((False,[]), source_error_with lim s)
- | Some e \<Rightarrow> 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 \<Rightarrow> let opt = optimise e; code = allocated e; bytes = allocated_bytes e in
+ if audit code 0 = Some 0 \<and> 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 \<Rightarrow> string" where
"source_error = source_error_with defaults"
@@ 279,6 284,10 @@ definition source_error :: "string \<Rightarrow> string" where
definition artifact :: "string \<Rightarrow> (bool \<times> string) \<times> string" where
"artifact = artifact_with defaults"
+definition baseline :: "string \<Rightarrow> (bool \<times> string) \<times> string" where
+ "baseline s = (case prepare s of None \<Rightarrow> ((False,[]),source_error s)
+ | Some e \<Rightarrow> ((True,map char_of_nat (executable e)),''stack backend'' @ newline))"
+
definition configured :: "string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> string \<Rightarrow> (bool \<times> string) \<times> string" where
"configured depth count stacktext source = (case (number depth, number count, number stacktext) of
(Some d,Some n,Some k) \<Rightarrow> artifact_with \<lparr>depth_budget=d, node_budget=n, stack_budget=k\<rparr> source
R src/Checker.thy => src/core/Checker.thy +0 -0
R src/Compiler.thy => src/core/Compiler.thy +0 -0
R src/Encoding.thy => src/core/Encoding.thy +0 -0
R src/Model.thy => src/core/Model.thy +0 -0
R src/Native.thy => src/core/Native.thy +0 -0
M tests/cli.py => tests/cli.py +5 -0
@@ 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)
A tests/measure.c => tests/measure.c +72 -0
@@ 0,0 1,72 @@
+#define _GNU_SOURCE
+#include <inttypes.h>
+#include <stdint.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <sys/mman.h>
+#include <time.h>
+#include <unistd.h>
+
+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;
+}
A tests/measure.py => tests/measure.py +42 -0
@@ 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()
M tests/native.py => tests/native.py +3 -0
@@ 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)