From 43a4914fe14af42187cc680d494308abd268f894 Mon Sep 17 00:00:00 2001
From: Alessandro Gatti <a.gatti@frob.it>
Date: Sun, 15 Feb 2026 21:22:31 +0100
Subject: [PATCH] tests/micropython: Add a test for checking viper value
 clobbering.

This commit introduces a test that should check whether viper load or
store operations won't clobber either the buffer address or the index
value being used.

Signed-off-by: Alessandro Gatti <a.gatti@frob.it>
---
 .../micropython/viper_preserve_invariants.py  | 39 +++++++++++++++++++
 .../viper_preserve_invariants.py.exp          |  6 +++
 2 files changed, 45 insertions(+)
 create mode 100644 tests/micropython/viper_preserve_invariants.py
 create mode 100644 tests/micropython/viper_preserve_invariants.py.exp

diff --git a/tests/micropython/viper_preserve_invariants.py b/tests/micropython/viper_preserve_invariants.py
new file mode 100644
index 0000000000..26f6003aba
--- /dev/null
+++ b/tests/micropython/viper_preserve_invariants.py
@@ -0,0 +1,39 @@
+RESULTS = []
+
+LOAD_TEMPLATE_REG = """
+BUFFER = bytearray([1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12])
+OFFSET = 1
+@micropython.viper
+def test_invariants_load{}_reg(buf: ptr{}, offset: int):
+    offset_copy1: int = offset
+    temporary1 = buf[offset]
+    offset_copy2: int = offset
+    temporary2 = buf[offset]
+    RESULTS.append(["LOAD{}", temporary1 == temporary2, offset == offset_copy1 == offset_copy2])
+test_invariants_load{}_reg(BUFFER, OFFSET)
+"""
+
+
+STORE_TEMPLATE_REG = """
+BUFFER = bytearray([1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12])
+OFFSET = 1
+@micropython.viper
+def test_invariants_store{}_reg(buf: ptr{}, offset: int):
+    offset_copy: int = offset
+    value: uint = {}
+    buf[offset] = value
+    temporary = buf[offset]
+    RESULTS.append(["STORE{}", temporary == value, offset == offset_copy])
+test_invariants_store{}_reg(BUFFER, OFFSET)
+"""
+
+try:
+    for width, value in ((8, 0x11), (16, 0x1111), (32, 0x11111111)):
+        exec(LOAD_TEMPLATE_REG.format(width, width, width, width, width))
+        exec(STORE_TEMPLATE_REG.format(width, width, value, width, width, width))
+except MemoryError:
+    print("SKIP-TOO-LARGE")
+    raise SystemExit
+
+for line in RESULTS:
+    print(" ".join([str(i) for i in line]))
diff --git a/tests/micropython/viper_preserve_invariants.py.exp b/tests/micropython/viper_preserve_invariants.py.exp
new file mode 100644
index 0000000000..21c6625243
--- /dev/null
+++ b/tests/micropython/viper_preserve_invariants.py.exp
@@ -0,0 +1,6 @@
+LOAD8 True True
+STORE8 True True
+LOAD16 True True
+STORE16 True True
+LOAD32 True True
+STORE32 True True