From 21d77cf288325dcfb456295637061e22fb3d28e9 Mon Sep 17 00:00:00 2001
From: james <j@cpl0.zip>
Date: Sat, 19 Sep 2026 12:00:00 +0100
Subject: [PATCH] feat(frontend): parse bounded hexadecimal word literals

---
 Makefile         |  1 +
 src/Examples.thy |  9 +++++++++
 src/Frontend.thy | 20 +++++++++++++++++---
 tests/cli.py     | 34 ++++++++++++++++++++++++++++++++++
 4 files changed, 61 insertions(+), 3 deletions(-)
 create mode 100644 tests/cli.py

diff --git a/Makefile b/Makefile
index d1c19434a24fa5f5b4814d844c38e43f68240bf8..4c2636fec4244d9ff27459dcdef9595a11d1ff0d 100644
--- a/Makefile
+++ b/Makefile
@@ -13,6 +13,7 @@ all: .build/ready
 
 check: all
 	python3 tests/native.py
+	python3 tests/cli.py
 
 payload: all
 	@mkdir -p .build/payload
diff --git a/src/Examples.thy b/src/Examples.thy
index 3a9cea3d5e0bf8b414b584797f2ef5cecc6f1874..ab0fdbecfd0352478c9c3f456fed2a0aea5a6edd 100644
--- a/src/Examples.thy
+++ b/src/Examples.thy
@@ -90,6 +90,15 @@ lemma trailing_rejected: "prepare ''(+ x y) 1'' = None"
 lemma literal_overflow_rejected: "prepare ''18446744073709551616'' = None"
   by eval
 
+lemma hexadecimal_boundaries:
+  "number ''0xffffffffffffffff'' = Some (2 ^ 64 - 1) \<and>
+    number ''0x10000000000000000'' = None"
+  by eval
+
+lemma hexadecimal_execution:
+  "reference ''(+ x 0XfF)'' ''0x1'' ''0'' ''0'' = (True,''256'' @ newline)"
+  by eval
+
 lemma incomplete_rejected: "prepare ''(if x y)'' = None"
   by eval
 
diff --git a/src/Frontend.thy b/src/Frontend.thy
index 6e019fbdab00423ef66656c89317d2f4c5cf1f77..601aa012d72fb4a5e1b702c0202ebce2af8d29ce 100644
--- a/src/Frontend.thy
+++ b/src/Frontend.thy
@@ -13,11 +13,25 @@ fun lex :: "string \<Rightarrow> string \<Rightarrow> string list \<Rightarrow>
     else if c = CHR ''('' \<or> c = CHR '')'' then lex cs [] ([c] # finish word out)
     else lex cs (c # word) out)"
 
-definition number :: "string \<Rightarrow> nat option" where
-  "number s = (if s = [] \<or> \<not> list_all (\<lambda>c. 48 \<le> nat_of_char c \<and> nat_of_char c < 58) s
-    then None else let n = foldl (\<lambda>n c. min (2 ^ 64) (10 * n + nat_of_char c - 48)) 0 s in
+fun digit :: "char \<Rightarrow> nat" where
+  "digit c = (let n = nat_of_char c in
+    if 48 \<le> n \<and> n < 58 then n - 48 else
+    if 65 \<le> n \<and> n < 71 then n - 55 else
+    if 97 \<le> n \<and> n < 103 then n - 87 else 16)"
+
+definition parse_digits :: "nat \<Rightarrow> string \<Rightarrow> nat option" where
+  "parse_digits base s = (if s = [] \<or> \<not> list_all (\<lambda>c. digit c < base) s
+    then None else let n = foldl (\<lambda>n c. min (2 ^ 64) (base * n + digit c)) 0 s in
     if n < 2 ^ 64 then Some n else None)"
 
+definition number :: "string \<Rightarrow> nat option" where
+  "number s = (case s of a # b # rest \<Rightarrow>
+    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)"
+
+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)
+
 definition valid_name :: "string \<Rightarrow> bool" where
   "valid_name s = (s \<noteq> [] \<and> list_all (\<lambda>c. (97 \<le> nat_of_char c \<and> nat_of_char c \<le> 122)) s
     \<and> s \<noteq> ''let'' \<and> s \<noteq> ''if'')"
diff --git a/tests/cli.py b/tests/cli.py
new file mode 100644
index 0000000000000000000000000000000000000000..6a7df59e70c558ab5b269f6dafbcaf94012a7e8b
--- /dev/null
+++ b/tests/cli.py
@@ -0,0 +1,34 @@
+from pathlib import Path
+import subprocess
+import tempfile
+
+
+ROOT = Path(__file__).resolve().parents[1]
+
+
+def invoke(*args, ok=True, data=None, preexec_fn=None):
+    result = subprocess.run([str(ROOT / '.build/remy'), *map(str, args)], input=data,
+        capture_output=True, text=True, timeout=30, preexec_fn=preexec_fn)
+    assert (result.returncode == 0) == ok, (args, result.stdout, result.stderr)
+    return result.stdout if ok else result.stderr
+
+
+def main():
+    with tempfile.TemporaryDirectory() as directory:
+        source, binary = Path(directory) / 'source', Path(directory) / 'binary'
+        for text, expected in [('0x0',0),('0xff',255),('0X7F',127),('0xffffffffffffffff',(1 << 64)-1),
+            ('(+ 0xffffffffffffffff 1)',0),('(< 0x8000000000000000 0xffffffffffffffff)',1)]:
+            source.write_text(text)
+            assert int(invoke('eval',source,'0','0','0')) == expected, text
+        source.write_text('(+ x y)')
+        assert int(invoke('eval',source,'0xFF','0x1','0x0')) == 256
+        for text in ['0x','0x10000000000000000','0xfg','0xffextra','-0x1']:
+            source.write_text(text)
+            binary.write_bytes(b'preserve')
+            invoke(source,binary,ok=False)
+            assert binary.read_bytes() == b'preserve', text
+    print('CLI literal and rejection checks passed')
+
+
+if __name__ == '__main__':
+    main()