From caca31f9c106a0b1b632c5d05f4ec83414baa993 Mon Sep 17 00:00:00 2001
From: Nada Amin <namin@alum.mit.edu>
Date: Mon, 13 Jul 2026 01:02:02 -0400
Subject: [PATCH 1/2] better safe slice function

---
 examples/safeSlice.dfy     | 48 ++++++++++++++++++++++++++++++++++++++
 examples/safeSlice.dfy.gen | 48 ++++++++++++++++++++++++++++++++++++++
 examples/safeSlice.ts      | 21 +++++++++++++++++
 tools/src/dafny-emit.ts    | 17 ++++++++++----
 4 files changed, 130 insertions(+), 4 deletions(-)
 create mode 100644 examples/safeSlice.dfy
 create mode 100644 examples/safeSlice.dfy.gen
 create mode 100644 examples/safeSlice.ts

diff --git a/examples/safeSlice.dfy b/examples/safeSlice.dfy
new file mode 100644
index 0000000..6be0eb4
--- /dev/null
+++ b/examples/safeSlice.dfy
@@ -0,0 +1,48 @@
+// Generated by lsc from safeSlice.ts
+
+function NormalizeSliceIndex(n: nat, i: int): int
+  ensures 0 <= NormalizeSliceIndex(n, i) <= n as int
+{
+  if i < 0 then
+    if n as int + i < 0 then 0 else n as int + i
+  else if i > n as int then n as int
+  else i
+}
+
+function SafeSlice<T>(s: seq<T>, lo: int, hi: int): seq<T>
+  ensures |SafeSlice(s, lo, hi)| <= |s|
+{
+  var lo' := NormalizeSliceIndex(|s|, lo);
+  var hi' := NormalizeSliceIndex(|s|, hi);
+  if hi' < lo' then [] else s[lo'..hi']
+}
+
+function sliceNegativeStart(): seq<int>
+{
+  SafeSlice([1, 2], -1, 2)
+}
+
+lemma sliceNegativeStart_ensures()
+  ensures (sliceNegativeStart() == [2])
+{
+}
+
+function sliceNegativeEnd(): seq<int>
+{
+  SafeSlice([1, 2], 0, -1)
+}
+
+lemma sliceNegativeEnd_ensures()
+  ensures (sliceNegativeEnd() == [1])
+{
+}
+
+function sliceNegativeBounds(): seq<int>
+{
+  SafeSlice([1, 2, 3, 4], -3, -1)
+}
+
+lemma sliceNegativeBounds_ensures()
+  ensures (sliceNegativeBounds() == [2, 3])
+{
+}
diff --git a/examples/safeSlice.dfy.gen b/examples/safeSlice.dfy.gen
new file mode 100644
index 0000000..6be0eb4
--- /dev/null
+++ b/examples/safeSlice.dfy.gen
@@ -0,0 +1,48 @@
+// Generated by lsc from safeSlice.ts
+
+function NormalizeSliceIndex(n: nat, i: int): int
+  ensures 0 <= NormalizeSliceIndex(n, i) <= n as int
+{
+  if i < 0 then
+    if n as int + i < 0 then 0 else n as int + i
+  else if i > n as int then n as int
+  else i
+}
+
+function SafeSlice<T>(s: seq<T>, lo: int, hi: int): seq<T>
+  ensures |SafeSlice(s, lo, hi)| <= |s|
+{
+  var lo' := NormalizeSliceIndex(|s|, lo);
+  var hi' := NormalizeSliceIndex(|s|, hi);
+  if hi' < lo' then [] else s[lo'..hi']
+}
+
+function sliceNegativeStart(): seq<int>
+{
+  SafeSlice([1, 2], -1, 2)
+}
+
+lemma sliceNegativeStart_ensures()
+  ensures (sliceNegativeStart() == [2])
+{
+}
+
+function sliceNegativeEnd(): seq<int>
+{
+  SafeSlice([1, 2], 0, -1)
+}
+
+lemma sliceNegativeEnd_ensures()
+  ensures (sliceNegativeEnd() == [1])
+{
+}
+
+function sliceNegativeBounds(): seq<int>
+{
+  SafeSlice([1, 2, 3, 4], -3, -1)
+}
+
+lemma sliceNegativeBounds_ensures()
+  ensures (sliceNegativeBounds() == [2, 3])
+{
+}
diff --git a/examples/safeSlice.ts b/examples/safeSlice.ts
new file mode 100644
index 0000000..44a6a34
--- /dev/null
+++ b/examples/safeSlice.ts
@@ -0,0 +1,21 @@
+// examples/safeSlice.ts
+
+//@ backend dafny
+//@ safe-slice
+
+
+
+function sliceNegativeStart(): number[] {
+  //@ ensures \result === [2]
+  return [1, 2].slice(-1, 2);
+}
+
+function sliceNegativeEnd(): number[] {
+  //@ ensures \result === [1]
+  return [1, 2].slice(0, -1);
+}
+
+function sliceNegativeBounds(): number[] {
+  //@ ensures \result === [2, 3]
+  return [1, 2, 3, 4].slice(-3, -1);
+}
diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts
index 8522268..9d600ed 100644
--- a/tools/src/dafny-emit.ts
+++ b/tools/src/dafny-emit.ts
@@ -1003,12 +1003,21 @@ const SEQ_JOIN = `function SeqJoin(s: seq<string>, sep: string): string
   else s[0] + sep + SeqJoin(s[1..], sep)
 }`;
 
-const SAFE_SLICE = `function SafeSlice<T>(s: seq<T>, lo: int, hi: int): seq<T>
+const SAFE_SLICE = `function NormalizeSliceIndex(n: nat, i: int): int
+  ensures 0 <= NormalizeSliceIndex(n, i) <= n as int
+{
+  if i < 0 then
+    if n as int + i < 0 then 0 else n as int + i
+  else if i > n as int then n as int
+  else i
+}
+
+function SafeSlice<T>(s: seq<T>, lo: int, hi: int): seq<T>
   ensures |SafeSlice(s, lo, hi)| <= |s|
 {
-  var lo' := if lo < 0 then 0 else if lo > |s| as int then |s| else lo;
-  var hi' := if hi > |s| as int then |s| else if hi < lo' then lo' else hi;
-  s[lo'..hi']
+  var lo' := NormalizeSliceIndex(|s|, lo);
+  var hi' := NormalizeSliceIndex(|s|, hi);
+  if hi' < lo' then [] else s[lo'..hi']
 }`;
 
 const STRING_INDEX_OF = `function StringIndexOf(s: string, sub: string): int

From 5cdbbd86dc49fd6993744ef716a526f62e84773b Mon Sep 17 00:00:00 2001
From: Nada Amin <namin@alum.mit.edu>
Date: Mon, 13 Jul 2026 01:07:08 -0400
Subject: [PATCH 2/2] retrigger CI after update of opencode case study