From d13e435ddd8ba80ef3a3b12a492f87e10d65554a Mon Sep 17 00:00:00 2001
From: Sam Clegg <sbc@chromium.org>
Date: Fri, 24 May 2024 09:45:56 -0700
Subject: [PATCH 1/2] Allow table.copy between tables with different index
 types

See #7
See #6
---
 interpreter/syntax/types.ml     |  4 +++
 interpreter/valid/valid.ml      |  6 ++---
 proposals/memory64/Overview.md  |  6 ++---
 test/core/table_copy_mixed.wast | 48 +++++++++++++++++++++++++++++++++
 4 files changed, 57 insertions(+), 7 deletions(-)
 create mode 100644 test/core/table_copy_mixed.wast

diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
index 493ebde96..be5da5e3d 100644
--- a/interpreter/syntax/types.ml
+++ b/interpreter/syntax/types.ml
@@ -106,6 +106,10 @@ let match_extern_type et1 et2 =
   | ExternGlobalType gt1, ExternGlobalType gt2 -> match_global_type gt1 gt2
   | _, _ -> false
 
+let min_index_type it1 it2 =
+  match it1, it2 with
+  | I64IndexType, I64IndexType -> I64IndexType
+  | _, _ -> I32IndexType
 
 (* String conversion *)
 
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index be1966b08..2a8738934 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -340,13 +340,11 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
   | TableCopy (x, y) ->
     let TableType (_lim1, it1, t1) = table c x in
     let TableType (_lim2, it2, t2) = table c y in
+    let it3 = min_index_type it1 it2 in
     require (t1 = t2) x.at
       ("type mismatch: source element type " ^ string_of_ref_type t1 ^
        " does not match destination element type " ^ string_of_ref_type t2);
-    require (it1 = it2) x.at
-      ("type mismatch: source index type " ^ string_of_index_type it1 ^
-       " does not match destination index type " ^ string_of_index_type it2);
-    [value_type_of_index_type it1; value_type_of_index_type it1; value_type_of_index_type it1] --> []
+    [value_type_of_index_type it1; value_type_of_index_type it2; value_type_of_index_type it3] --> []
 
   | TableInit (x, y) ->
     let TableType (_lim, it, t1) = table c x in
diff --git a/proposals/memory64/Overview.md b/proposals/memory64/Overview.md
index ff4bfcfe5..23958bd84 100644
--- a/proposals/memory64/Overview.md
+++ b/proposals/memory64/Overview.md
@@ -203,9 +203,9 @@ have to support 32-bit memory addresses in their ABI.
       ```
   - table.copy x y
     - ```
-          C.tables[x] = it limits t
-      ----------------------------------
-      C ⊦ table.copy x : [it it it] → []
+        C.tables[d] = iN limits t   C.tables[s] = iM limits t    K = min {N, M}
+      -----------------------------------------------------------------------------
+      C ⊦ table.copy d s : [iN iM iK] → []
       ```
   - table.init x y
     - ```
diff --git a/test/core/table_copy_mixed.wast b/test/core/table_copy_mixed.wast
new file mode 100644
index 000000000..e34cde0d0
--- /dev/null
+++ b/test/core/table_copy_mixed.wast
@@ -0,0 +1,48 @@
+;; Valid cases
+(module
+  (table $t32 30 30 funcref)
+  (table $t64 i64 30 30 funcref)
+
+  (func (export "test32")
+    (table.copy $t32 $t32 (i32.const 13) (i32.const 2) (i32.const 3)))
+
+  (func (export "test64")
+    (table.copy $t64 $t64 (i64.const 13) (i64.const 2) (i64.const 3)))
+
+  (func (export "test_64to32")
+    (table.copy $t32 $t64 (i32.const 13) (i64.const 2) (i32.const 3)))
+
+  (func (export "test_32to64")
+    (table.copy $t64 $t32 (i64.const 13) (i32.const 2) (i32.const 3)))
+)
+
+;; Invalid cases
+(assert_invalid (module
+  (table $t32 30 30 funcref)
+  (table $t64 i64 30 30 funcref)
+
+  (func (export "bad_size_arg")
+    (table.copy $t32 $t64 (i32.const 13) (i64.const 2) (i64.const 3)))
+  )
+  "type mismatch"
+)
+
+(assert_invalid (module
+  (table $t32 30 30 funcref)
+  (table $t64 i64 30 30 funcref)
+
+  (func (export "bad_src_idx")
+    (table.copy $t32 $t64 (i32.const 13) (i32.const 2) (i32.const 3)))
+  )
+  "type mismatch"
+)
+
+(assert_invalid (module
+  (table $t32 30 30 funcref)
+  (table $t64 i64 30 30 funcref)
+
+  (func (export "bad_dst_idx")
+    (table.copy $t32 $t64 (i64.const 13) (i64.const 2) (i32.const 3)))
+  )
+  "type mismatch"
+)

From aebbe4459682d7c777d61aa0b1079718b00616e9 Mon Sep 17 00:00:00 2001
From: Sam Clegg <sbc@chromium.org>
Date: Fri, 24 May 2024 10:30:32 -0700
Subject: [PATCH 2/2] feedback

---
 interpreter/syntax/types.ml | 5 -----
 interpreter/valid/valid.ml  | 2 +-
 2 files changed, 1 insertion(+), 6 deletions(-)

diff --git a/interpreter/syntax/types.ml b/interpreter/syntax/types.ml
index be5da5e3d..0e5729089 100644
--- a/interpreter/syntax/types.ml
+++ b/interpreter/syntax/types.ml
@@ -106,11 +106,6 @@ let match_extern_type et1 et2 =
   | ExternGlobalType gt1, ExternGlobalType gt2 -> match_global_type gt1 gt2
   | _, _ -> false
 
-let min_index_type it1 it2 =
-  match it1, it2 with
-  | I64IndexType, I64IndexType -> I64IndexType
-  | _, _ -> I32IndexType
-
 (* String conversion *)
 
 let string_of_num_type = function
diff --git a/interpreter/valid/valid.ml b/interpreter/valid/valid.ml
index 2a8738934..c39e80dba 100644
--- a/interpreter/valid/valid.ml
+++ b/interpreter/valid/valid.ml
@@ -340,7 +340,7 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
   | TableCopy (x, y) ->
     let TableType (_lim1, it1, t1) = table c x in
     let TableType (_lim2, it2, t2) = table c y in
-    let it3 = min_index_type it1 it2 in
+    let it3 = min it1 it2 in
     require (t1 = t2) x.at
       ("type mismatch: source element type " ^ string_of_ref_type t1 ^
        " does not match destination element type " ^ string_of_ref_type t2);