Allow table.copy between tables with different index types

interpreter/syntax/types.ml

@@ -106,7 +106,6 @@ let match_extern_type et1 et2 =
   | ExternGlobalType gt1, ExternGlobalType gt2 -> match_global_type gt1 gt2
   | _, _ -> false
 
-
 (* String conversion *)
 
 let string_of_num_type = function

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 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

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
     - ```

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"
+)