From 43e65278564edc622d38d3bd24a8b989050f71c5 Mon Sep 17 00:00:00 2001
From: Paul Govereau <govereau@amazon.com>
Date: Fri, 6 Feb 2026 11:43:55 -0500
Subject: [PATCH] fix: ensure scalar offsets are BIR access patterns

When using an access as a scalar offset, it must be a BIR
access pattern, otherwise it will be translated incorrectly
down stream.
---
 KLR/Trace/Term.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/KLR/Trace/Term.lean b/KLR/Trace/Term.lean
index ef5772b1..f693c899 100644
--- a/KLR/Trace/Term.lean
+++ b/KLR/Trace/Term.lean
@@ -659,7 +659,9 @@ nki builtin.access.ap
   | .simple t =>
       let pattern := pattern.map fun (s,c) => Core.APPair.mk s c 0
       let scalarOffset <- scalar_offset.mapM fun
-        | .inl a => pure (.acc a)
+        | .inl a => do
+           let ap <- a.toAP
+           pure (.acc $ .birPattern $ Core.BirAccessPattern.fromAccessPattern ap)
         | .inr r => match r with
           | .scalar s => pure (.reg s.toString)
           | _ => throw s!"scalar_offset requires scalar argument, got {r.kindStr}"