fix: reference implementation ByteArray.copySlice

src/Init/Data/ByteArray/Basic.lean

@@ -81,7 +81,7 @@ def isEmpty (s : ByteArray) : Bool :=
   If `exact` is `false`, the capacity will be doubled when grown. -/
 @[extern "lean_byte_array_copy_slice"]
 def copySlice (src : @& ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff len : Nat) (exact : Bool := true) : ByteArray :=
-  ⟨dest.data.extract 0 destOff ++ src.data.extract srcOff (srcOff + len) ++ dest.data.extract (destOff + len) dest.data.size⟩
+  ⟨dest.data.extract 0 destOff ++ src.data.extract srcOff (srcOff + len) ++ dest.data.extract (destOff + min len (src.data.size - srcOff)) dest.data.size⟩
 
 def extract (a : ByteArray) (b e : Nat) : ByteArray :=
   a.copySlice b empty 0 (e - b)

tests/lean/run/2966.lean

@@ -0,0 +1,81 @@
+import Lean
+
+def testCopySlice (src : Array UInt8) (srcOff : Nat) (dest : Array UInt8) (destOff len : Nat) : Bool :=
+  (ByteArray.copySlice ⟨src⟩ srcOff ⟨dest⟩ destOff len |>.toList) ==
+    (ByteArray.copySlice ⟨src⟩ srcOff ⟨dest⟩ destOff len |>.toList)
+
+-- We verify that the `@[extern]` implementation of `ByteArray.copySlice` matches the formal definition,
+-- by equating two copies using `==`, unfolding the definition of one, and then calling `native_decide`
+macro "testCopySliceTactic" : tactic =>
+  `(tactic|
+      (dsimp [testCopySlice]
+       conv =>
+        congr
+        congr
+        dsimp [ByteArray.copySlice]
+       native_decide))
+
+-- These used to fail, as reported in #2966
+
+example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 6 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 20 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 1 #[4, 5, 6] 0 6 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 6 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 20 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 6 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 20 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 6 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 20 := by
+  testCopySliceTactic
+
+
+-- These worked prior to #2966; extra text cases can't hurt!
+
+example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 2 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 1 #[4, 5, 6] 0 2 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 2 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 1 #[4, 5, 6] 1 2 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 1 #[4, 5, 6] 1 6 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 2 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 0 #[4, 5, 6] 0 2 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 2 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 0 #[4, 5, 6] 1 2 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 0 #[4, 5, 6] 1 6 := by
+  testCopySliceTactic
+
+example : testCopySlice #[1,2,3] 0 #[4, 5, 6] 0 6 := by
+  testCopySliceTactic

tests/lean/test_extern.lean.expected.out

@@ -1,11 +1 @@
 test_extern.lean:7:0-7:17: error: test_extern: HAdd.hAdd does not have an @[extern] attribute
-test_extern.lean:9:0-9:86: error: native implementation did not agree with reference implementation!
-Compare the outputs of:
-#eval ByteArray.copySlice { data := #[1, 2, 3] } 1 { data := #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] } 0 6
- and
-#eval {
-  data :=
-    Array.extract { data := #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] }.data 0 0 ++
-        Array.extract { data := #[1, 2, 3] }.data 1 (1 + 6) ++
-      Array.extract { data := #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] }.data (0 + 6)
-        (Array.size { data := #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] }.data) }