From 5ae0ff8681ce99f0be1be4fcf263848bfc415a22 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Wed, 31 Jul 2024 06:21:34 -0400
Subject: [PATCH 01/11] crucible-wasm: Fix -Wunused-imports warning

---
 crucible-wasm/src/Lang/Crucible/Wasm/Memory.hs | 1 -
 1 file changed, 1 deletion(-)

diff --git a/crucible-wasm/src/Lang/Crucible/Wasm/Memory.hs b/crucible-wasm/src/Lang/Crucible/Wasm/Memory.hs
index 24ad55191..08c768aa8 100644
--- a/crucible-wasm/src/Lang/Crucible/Wasm/Memory.hs
+++ b/crucible-wasm/src/Lang/Crucible/Wasm/Memory.hs
@@ -32,7 +32,6 @@ import qualified Lang.Crucible.LLVM.MemModel.Generic as G
 import qualified Lang.Crucible.LLVM.MemModel.Partial as Partial
 
 import What4.Interface
-import What4.InterpretedFloatingPoint
 
 import Lang.Crucible.Wasm.Utils
 

From 04afc3b833b7646a52e2987a1deb78ca4ffc6275 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Wed, 31 Jul 2024 06:25:05 -0400
Subject: [PATCH 02/11] crucible-wasm: Make it build after haskell-wasm added
 reference types and values

This bumps the `haskell-wasm` commit to
https://github.com/SPY/haskell-wasm/commit/51cf7e753bd19896712d71b0f50932d181852ad7
and does the minimum amount of work needed to make `crucible-wasm` continue to
compile after these changes. For now, we do not implement full support for
Wasm's reference types and values, as that would require a non-trivial amount
of work to support. See #1228.
---
 crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs | 3 +++
 crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs   | 9 +++++++++
 dependencies/haskell-wasm                           | 2 +-
 3 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs b/crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs
index f5a0998c6..04498665d 100644
--- a/crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs
+++ b/crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs
@@ -273,6 +273,9 @@ valueTypeToType Wasm.I32 = Some (BVRepr (knownNat @32))
 valueTypeToType Wasm.I64 = Some (BVRepr (knownNat @64))
 valueTypeToType Wasm.F32 = Some (FloatRepr SingleFloatRepr)
 valueTypeToType Wasm.F64 = Some (FloatRepr DoubleFloatRepr)
+-- See https://github.com/GaloisInc/crucible/issues/1228
+valueTypeToType Wasm.Func   = error "Func reference types are not currently supported"
+valueTypeToType Wasm.Extern = error "Extern reference types are not currently supported"
 
 valueTypesToContext :: [Wasm.ValueType] -> Some (Assignment TypeRepr)
 valueTypesToContext = fromList . map valueTypeToType
diff --git a/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs b/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
index 584a5ecba..929bead41 100644
--- a/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
+++ b/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
@@ -334,6 +334,11 @@ translateFunction fty fn@Wasm.Function{ .. } im st hdl =
   setupLocal Wasm.F64 =
     do r <- newReg (App (DoubleLit 0.0))
        modify (addLocal r)
+  -- See https://github.com/GaloisInc/crucible/issues/1228
+  setupLocal Wasm.Func =
+    unimplemented "Func reference values"
+  setupLocal Wasm.Extern =
+    unimplemented "Extern reference values"
 
   genReturn :: WasmGenerator s ret (Expr WasmExt s ret)
   genReturn = computeReturn (handleReturnType hdl) (Wasm.results fty)
@@ -801,6 +806,10 @@ genInstruction genReturn im st ctrlStack instr =
     -- IReinterpretF BitSize
     -- FReinterpretI BitSize
 
+    -- RefNull ElemType
+    -- RefIsNull
+    -- RefFunc FuncIndex
+
     _ -> unimplemented $ unwords ["Instruction not implemented", show instr]
 
 invokeFn ::
diff --git a/dependencies/haskell-wasm b/dependencies/haskell-wasm
index efba9c2b5..51cf7e753 160000
--- a/dependencies/haskell-wasm
+++ b/dependencies/haskell-wasm
@@ -1 +1 @@
-Subproject commit efba9c2b504e793776f328c8ba661811e120021d
+Subproject commit 51cf7e753bd19896712d71b0f50932d181852ad7

From 03d618fbb89648c7a0c2f841b8bdd7a254550c54 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Thu, 1 Aug 2024 06:22:16 -0400
Subject: [PATCH 03/11] crucible-wasm: Adapt to new elem format in Wasm 2.0

This bumps the `haskell-wasm` commit to
https://github.com/SPY/haskell-wasm/commit/de40134caf10c99d2b50a485f66dae9a7e73cd81
and does the minimum amount of work needed to make `crucible-wasm` continue to
compile after these changes. For now, we do not implement full support for Wasm
2.0's new element segment features, as that would require a non-trivial amount
of work to support. See #1228.
---
 .../src/Lang/Crucible/Wasm/Instantiate.hs     | 27 ++++++++++++++++---
 dependencies/haskell-wasm                     |  2 +-
 2 files changed, 24 insertions(+), 5 deletions(-)

diff --git a/crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs b/crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs
index 04498665d..786f452ed 100644
--- a/crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs
+++ b/crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs
@@ -404,12 +404,18 @@ installElemSegment ::
   Wasm.ElemSegment ->
   InstM ()
 installElemSegment im es@Wasm.ElemSegment{ .. } =
-  do I32Val tblOff <- evalConst im offset
+  do (tableIndex, offset) <-
+       case mode of
+         Wasm.Active idx off -> pure (idx, off)
+         Wasm.Passive -> unimplemented "Passive element segments"
+         Wasm.Declarative -> unimplemented "Declarative element segments"
+     I32Val tblOff <- evalConst im offset
+     funcIndexes <- traverse evalConstFuncIndex elements
      st <- lift get
      debug "installing element segment"
      debug (show es)
      debug (show (instTableAddrs im))
-     case updStore (fromIntegral tblOff) st of
+     case updStore tableIndex funcIndexes (fromIntegral tblOff) st of
        Nothing  -> instErr ("failed to evaluate element segment: " <> TL.pack (show es))
        Just st' -> lift (put st')
 
@@ -418,8 +424,8 @@ installElemSegment im es@Wasm.ElemSegment{ .. } =
     do hdl <- Seq.lookup faddr (storeFuncs st)
        pure (updateFuncTable loc fty hdl ft)
 
-  updStore :: Int -> Store -> Maybe Store
-  updStore off st =
+  updStore :: Wasm.TableIndex -> [Wasm.FuncIndex] -> Int -> Store -> Maybe Store
+  updStore tableIndex funcIndexes off st =
     do (Wasm.TableType (Wasm.Limit lmin _) Wasm.FuncRef, addr) <- resolveTableIndex tableIndex im
        functab <- Seq.lookup addr (storeTables st)
        guard (toInteger off + toInteger (length funcIndexes) <= toInteger lmin)
@@ -463,6 +469,19 @@ evalConst i [Wasm.GetGlobal idx] =
 
 evalConst _ _ = instErr "expression not a constant!"
 
+-- | Evaluate a constant 'Wasm.Expression' that is expected to be a single
+-- 'Wasm.RefFunc' instruction, returning the underlying 'Wasm.FuncIndex'.
+-- Currently, this is only used when computing element segments.
+
+-- TODO: Ideally, we would merge this function with 'evalConst' above by adding
+-- references to functions as a first-class 'ConstantValue'. Doing so would
+-- require fixing https://github.com/GaloisInc/crucible/issues/1228 first,
+-- however.
+evalConstFuncIndex :: Wasm.Expression -> InstM Wasm.FuncIndex
+evalConstFuncIndex [Wasm.RefFunc fi] = pure fi
+evalConstFuncIndex e =
+  instErr $ "expression not a function index constant: " <> fromString (show e)
+
 bindImport :: Namespace -> ModuleInstance -> Wasm.Import -> InstM ExternalValue
 bindImport ns i Wasm.Import{ .. } =
   case namespaceLookup (Wasm.Ident sourceModule) name ns of
diff --git a/dependencies/haskell-wasm b/dependencies/haskell-wasm
index 51cf7e753..de40134ca 160000
--- a/dependencies/haskell-wasm
+++ b/dependencies/haskell-wasm
@@ -1 +1 @@
-Subproject commit 51cf7e753bd19896712d71b0f50932d181852ad7
+Subproject commit de40134caf10c99d2b50a485f66dae9a7e73cd81

From 3f21102862345a3287f487c1b510d4e938921ef9 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Thu, 1 Aug 2024 06:58:33 -0400
Subject: [PATCH 04/11] crucible-wasm: Adapt to new table instructions in Wasm
 2.0

This bumps the `haskell-wasm` commit to
https://github.com/SPY/haskell-wasm/commit/4753ebceb4ab24c77a50791e14baa524454e9c72.
For now, we do not implement Wasm 2.0's new table-related instructions, as that
would require a non-trivial amount of work to support. See #1228.
---
 crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs | 8 ++++++++
 dependencies/haskell-wasm                         | 2 +-
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs b/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
index 929bead41..0dc06a0bd 100644
--- a/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
+++ b/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
@@ -810,6 +810,14 @@ genInstruction genReturn im st ctrlStack instr =
     -- RefIsNull
     -- RefFunc FuncIndex
 
+    -- TableInit TableIndex ElemIndex
+    -- TableGrow TableIndex
+    -- TableSize TableIndex
+    -- TableFill TableIndex
+    -- TableGet TableIndex
+    -- TableSet TableIndex
+    -- TableCopy TableIndex TableIndex
+
     _ -> unimplemented $ unwords ["Instruction not implemented", show instr]
 
 invokeFn ::
diff --git a/dependencies/haskell-wasm b/dependencies/haskell-wasm
index de40134ca..4753ebceb 160000
--- a/dependencies/haskell-wasm
+++ b/dependencies/haskell-wasm
@@ -1 +1 @@
-Subproject commit de40134caf10c99d2b50a485f66dae9a7e73cd81
+Subproject commit 4753ebceb4ab24c77a50791e14baa524454e9c72

From 375d1a3b541f0c54f3267aeacefbff125d473d18 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Thu, 1 Aug 2024 07:03:51 -0400
Subject: [PATCH 05/11] crucible-wasm: Adapt to elem.drop and call_indirect
 having a table index

This bumps the `haskell-wasm` commit to
https://github.com/SPY/haskell-wasm/commit/82defff0768225317d3d5f4ca91da05625ea5637
and does the minimum amount of work needed to make `crucible-wasm` continue to
compile after these changes. In particular:

* The `call_indirect` instruction has been generalized so that it can accept an
  arbitrary table index, rather than always hard-coding the table index to 0.
  This is straightforward to generalize on the `crucible-wasm` side as well.
* Wasm 2.0 has a new `elem.drop` instruction. For now, we do not implement
  support for this instruction.
---
 crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs | 13 +++++++------
 dependencies/haskell-wasm                         |  2 +-
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs b/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
index 0dc06a0bd..7154cdb7d 100644
--- a/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
+++ b/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
@@ -552,13 +552,12 @@ genInstruction genReturn im st ctrlStack instr =
             Nothing -> panic "genInstruction: Call" ["Could not resolve function address " ++ show addr]
             Just (SomeHandle h) -> invokeFn fty (handleType h) (App (HandleLit h))
 
-    Wasm.CallIndirect tidx ->
-      case resolveTypeIndex tidx im of
-        Nothing -> panic "genInstruction: CallIndirect" ["Could not resolve type index " ++ show tidx]
+    Wasm.CallIndirect tableIdx typeIdx ->
+      case resolveTypeIndex typeIdx im of
+        Nothing -> panic "genInstruction: CallIndirect" ["Could not resolve type index " ++ show typeIdx]
         Just fty ->
-          -- NB, table index hard-coded to 0 in Wasm 1.0
-          case resolveTableIndex 0 im of
-            Nothing -> panic "genInstruction: CallIndirect" ["Could not resolve table index 0"]
+          case resolveTableIndex tableIdx im of
+            Nothing -> panic "genInstruction: CallIndirect" ["Could not resolve table index " ++ show tableIdx]
             Just (_tty, tbladdr) ->
               case Seq.lookup tbladdr (storeTables st) of
                 Nothing -> panic "genInstruction: CallIndirect" ["Could not resolve table address " ++ show tbladdr]
@@ -818,6 +817,8 @@ genInstruction genReturn im st ctrlStack instr =
     -- TableSet TableIndex
     -- TableCopy TableIndex TableIndex
 
+    -- ElemDrop ElemIndex
+
     _ -> unimplemented $ unwords ["Instruction not implemented", show instr]
 
 invokeFn ::
diff --git a/dependencies/haskell-wasm b/dependencies/haskell-wasm
index 4753ebceb..82defff07 160000
--- a/dependencies/haskell-wasm
+++ b/dependencies/haskell-wasm
@@ -1 +1 @@
-Subproject commit 4753ebceb4ab24c77a50791e14baa524454e9c72
+Subproject commit 82defff0768225317d3d5f4ca91da05625ea5637

From f7c697e5898eb2ad45202a179dabe8968bbe9deb Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Thu, 1 Aug 2024 07:27:24 -0400
Subject: [PATCH 06/11] crucible-wasm: Adapt to select having an optional value
 type

This bumps the `haskell-wasm` commit to
https://github.com/SPY/haskell-wasm/commit/c743e11ffd621c871ab98068fee4d08f21f42d14
and does the minimum amount of work needed to make `crucible-wasm` continue to
compile after these changes. In particular, the `select` instruction now has an
optional value type indicating the type of its first and second operand, which
`crucible-wasm` ignores. This is OK for now, as `crucible-wasm`'s
implementation is currently simple enough where the types of all its stack
values can be inferred without any additional type information.
---
 crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs | 7 ++++++-
 dependencies/haskell-wasm                         | 2 +-
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs b/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
index 7154cdb7d..4d9bfe55c 100644
--- a/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
+++ b/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
@@ -573,7 +573,12 @@ genInstruction genReturn im st ctrlStack instr =
     Wasm.Drop ->
       void $ popStack
 
-    Wasm.Select ->
+    -- The `select` instruction includes an optional value type, which indicates
+    -- the type of its first and second operands. We do not currently make use
+    -- of this type, however, as crucible-wasm's implementation is simple enough
+    -- where the types of all possible stack values can be inferred without any
+    -- additional type information.
+    Wasm.Select _mbValTypes ->
       do c <- popTest
          y <- popStack
          x <- popStack
diff --git a/dependencies/haskell-wasm b/dependencies/haskell-wasm
index 82defff07..c743e11ff 160000
--- a/dependencies/haskell-wasm
+++ b/dependencies/haskell-wasm
@@ -1 +1 @@
-Subproject commit 82defff0768225317d3d5f4ca91da05625ea5637
+Subproject commit c743e11ffd621c871ab98068fee4d08f21f42d14

From ee20b4d65bf56a482e22d818ef33f87c75e9670b Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Thu, 1 Aug 2024 07:32:42 -0400
Subject: [PATCH 07/11] crucible-wasm: Adapt to new data segment format in Wasm
 2.0

This bumps the `haskell-wasm` commit to
https://github.com/SPY/haskell-wasm/commit/32392dcc29ef3fef3a0e363d3c04d44f3082c881
and does the minimum amount of work needed to make `crucible-wasm` continue
to compile after these changes. For now, we do not implement full support
for Wasm 2.0's new data segment features, as that would require a
non-trivial amount of work to support. See #1228.
---
 crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs | 6 +++++-
 dependencies/haskell-wasm                           | 2 +-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs b/crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs
index 786f452ed..5c8966e0c 100644
--- a/crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs
+++ b/crucible-wasm/src/Lang/Crucible/Wasm/Instantiate.hs
@@ -388,7 +388,11 @@ computeDataSegment ::
   Wasm.DataSegment ->
   InstM (GlobalVar WasmMem, Word32, LBS.ByteString)
 computeDataSegment i Wasm.DataSegment{ .. } =
-  do st <- lift get
+  do (memIndex, offset) <-
+       case dataMode of
+         Wasm.ActiveData memIndex offset -> pure (memIndex, offset)
+         Wasm.PassiveData -> unimplemented "Passive data segments"
+     st <- lift get
      case resolveMemIndex memIndex i of
        Nothing -> instErr ("Could not resolve memory index " <> fromString (show memIndex))
        Just (_,_,addr) ->
diff --git a/dependencies/haskell-wasm b/dependencies/haskell-wasm
index c743e11ff..32392dcc2 160000
--- a/dependencies/haskell-wasm
+++ b/dependencies/haskell-wasm
@@ -1 +1 @@
-Subproject commit c743e11ffd621c871ab98068fee4d08f21f42d14
+Subproject commit 32392dcc29ef3fef3a0e363d3c04d44f3082c881

From 2bb15511f4166ef0f039c22d6c8a33ab62bc3ad4 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Thu, 1 Aug 2024 07:38:57 -0400
Subject: [PATCH 08/11] crucible-wasm: Adapt to new memory-related instructions
 in Wasm 2.0

This bumps the `haskell-wasm` commit to
https://github.com/SPY/haskell-wasm/commit/2bf6e8807299441739ceec89269938d0a0ca5ebb
and does the minimum amount of work needed to make `crucible-wasm` continue
to compile after these changes. In particular:

* `CurrentMemory` and `GrowMemory` were renamed to `MemorySize` and
  `MemoryGrow`, so I've performed the corresponding renaming on the
  `crucible-wasm` side as well.
* For now, I have not added support for the `memory.fill`, `memory.copy`,
  `memory.init`, or `data.drop` instructions, all of which are new in Wasm 2.0.
---
 crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs | 9 +++++++--
 dependencies/haskell-wasm                         | 2 +-
 2 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs b/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
index 4d9bfe55c..12bba7f3e 100644
--- a/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
+++ b/crucible-wasm/src/Lang/Crucible/Wasm/Translate.hs
@@ -622,11 +622,11 @@ genInstruction genReturn im st ctrlStack instr =
             Just (ConstantGlobal _) -> panic "genInstruction: SetGlobal" ["setGlobal of constant global"]
             Just (MutableGlobal gv) -> writeGlobal gv =<< checkStackVal (globalType gv) =<< popStack
 
-    Wasm.CurrentMemory ->
+    Wasm.MemorySize ->
       do gv <- getMemVar im st
          pushStack =<< extensionStmt (Wasm_MemSize gv)
 
-    Wasm.GrowMemory ->
+    Wasm.MemoryGrow ->
       do gv <- getMemVar im st
          n <- popInteger32
          void $ extensionStmt (Wasm_MemGrow gv n)
@@ -822,7 +822,12 @@ genInstruction genReturn im st ctrlStack instr =
     -- TableSet TableIndex
     -- TableCopy TableIndex TableIndex
 
+    -- MemoryFill
+    -- MemoryCopy
+    -- MemoryInit DataIndex
+
     -- ElemDrop ElemIndex
+    -- DataDrop DataIndex
 
     _ -> unimplemented $ unwords ["Instruction not implemented", show instr]
 
diff --git a/dependencies/haskell-wasm b/dependencies/haskell-wasm
index 32392dcc2..2bf6e8807 160000
--- a/dependencies/haskell-wasm
+++ b/dependencies/haskell-wasm
@@ -1 +1 @@
-Subproject commit 32392dcc29ef3fef3a0e363d3c04d44f3082c881
+Subproject commit 2bf6e8807299441739ceec89269938d0a0ca5ebb

From 191fb9430c8dc2217854636553bf7cb69d835519 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Thu, 1 Aug 2024 07:43:20 -0400
Subject: [PATCH 09/11] Bump haskell-wasm to latest master commit

---
 dependencies/haskell-wasm | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dependencies/haskell-wasm b/dependencies/haskell-wasm
index 2bf6e8807..23aef0009 160000
--- a/dependencies/haskell-wasm
+++ b/dependencies/haskell-wasm
@@ -1 +1 @@
-Subproject commit 2bf6e8807299441739ceec89269938d0a0ca5ebb
+Subproject commit 23aef00097039faf240746a64c5f9ac2c90efdf6

From 58345caff5e460b0dd84a2e6a0fd387611733021 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Wed, 31 Jul 2024 07:44:44 -0400
Subject: [PATCH 10/11] crucible-wasm: Add elem-related test case

We have recently made some changes to the way `crucible-wasm` handled element
segments, so this test case helps ensure that we have not broken anything that
used to work before.
---
 crucible-wasm/test-data/elem.good |   1 +
 crucible-wasm/test-data/elem.wast | 141 ++++++++++++++++++++++++++++++
 2 files changed, 142 insertions(+)
 create mode 100644 crucible-wasm/test-data/elem.good
 create mode 100644 crucible-wasm/test-data/elem.wast

diff --git a/crucible-wasm/test-data/elem.good b/crucible-wasm/test-data/elem.good
new file mode 100644
index 000000000..9c7ea10d9
--- /dev/null
+++ b/crucible-wasm/test-data/elem.good
@@ -0,0 +1 @@
+[Crux] Overall status: Valid.
diff --git a/crucible-wasm/test-data/elem.wast b/crucible-wasm/test-data/elem.wast
new file mode 100644
index 000000000..9d729ecda
--- /dev/null
+++ b/crucible-wasm/test-data/elem.wast
@@ -0,0 +1,141 @@
+;; Test the element section
+;;
+;; Adapted from the elem test case in
+;;
+;;   https://github.com/WebAssembly/spec/blob/351d8b1026a2a820e88baae54557c43e775fd5a5/test/core/elem.wast
+
+;; Syntax
+(module
+  (table $t 10 funcref)
+  (func $f)
+  (func $g)
+
+  ;; Active
+  (elem (table $t) (i32.const 0) funcref)
+  (elem (table $t) (i32.const 0) funcref (ref.func $f) (ref.func $g))
+  (elem (table $t) (i32.const 0) func)
+  (elem (table $t) (i32.const 0) func $f $g)
+  (elem (table $t) (offset (i32.const 0)) funcref)
+  (elem (table $t) (offset (i32.const 0)) func $f $g)
+  (elem (table 0) (i32.const 0) func)
+  (elem (table 0x0) (i32.const 0) func $f $f)
+  (elem (table 0x000) (offset (i32.const 0)) func)
+  (elem (table 0) (offset (i32.const 0)) func $f $f)
+  (elem (table $t) (i32.const 0) func)
+  (elem (table $t) (i32.const 0) func $f $f)
+  (elem (table $t) (offset (i32.const 0)) func)
+  (elem (table $t) (offset (i32.const 0)) func $f $f)
+  (elem (offset (i32.const 0)))
+  (elem (offset (i32.const 0)) funcref (ref.func $f) (ref.func $g))
+  (elem (offset (i32.const 0)) func $f $f)
+  (elem (offset (i32.const 0)) $f $f)
+  (elem (i32.const 0))
+  (elem (i32.const 0) funcref (ref.func $f) (ref.func $g))
+  (elem (i32.const 0) func $f $f)
+  (elem (i32.const 0) $f $f)
+  (elem (i32.const 0) funcref (item (ref.func $f)) (item (ref.func $g)))
+
+  (elem $a1 (table $t) (i32.const 0) funcref)
+  (elem $a2 (table $t) (i32.const 0) funcref (ref.func $f) (ref.func $g))
+  (elem $a3 (table $t) (i32.const 0) func)
+  (elem $a4 (table $t) (i32.const 0) func $f $g)
+  (elem $a9 (table $t) (offset (i32.const 0)) funcref)
+  (elem $a10 (table $t) (offset (i32.const 0)) func $f $g)
+  (elem $a11 (table 0) (i32.const 0) func)
+  (elem $a12 (table 0x0) (i32.const 0) func $f $f)
+  (elem $a13 (table 0x000) (offset (i32.const 0)) func)
+  (elem $a14 (table 0) (offset (i32.const 0)) func $f $f)
+  (elem $a15 (table $t) (i32.const 0) func)
+  (elem $a16 (table $t) (i32.const 0) func $f $f)
+  (elem $a17 (table $t) (offset (i32.const 0)) func)
+  (elem $a18 (table $t) (offset (i32.const 0)) func $f $f)
+  (elem $a19 (offset (i32.const 0)))
+  (elem $a20 (offset (i32.const 0)) funcref (ref.func $f) (ref.func $g))
+  (elem $a21 (offset (i32.const 0)) func $f $f)
+  (elem $a22 (offset (i32.const 0)) $f $f)
+  (elem $a23 (i32.const 0))
+  (elem $a24 (i32.const 0) funcref (ref.func $f) (ref.func $g))
+  (elem $a25 (i32.const 0) func $f $f)
+  (elem $a26 (i32.const 0) $f $f)
+)
+
+(module
+  (func $f)
+  (func $g)
+
+  (table $t funcref (elem (ref.func $f) (ref.func $g) (ref.func $g)))
+)
+
+
+;; Basic use
+
+(module
+  (table 10 funcref)
+  (func $f)
+  (elem (i32.const 0) $f)
+)
+
+(module
+  (table 10 funcref)
+  (func $f)
+  (elem (i32.const 0) $f)
+  (elem (i32.const 3) $f)
+  (elem (i32.const 7) $f)
+  (elem (i32.const 5) $f)
+  (elem (i32.const 3) $f)
+)
+
+(module
+  (type $out-i32 (func (result i32)))
+  (table 10 funcref)
+  (elem (i32.const 7) $const-i32-a)
+  (elem (i32.const 9) $const-i32-b)
+  (func $const-i32-a (type $out-i32) (i32.const 65))
+  (func $const-i32-b (type $out-i32) (i32.const 66))
+  (func (export "call-7") (type $out-i32)
+    (call_indirect (type $out-i32) (i32.const 7))
+  )
+  (func (export "call-9") (type $out-i32)
+    (call_indirect (type $out-i32) (i32.const 9))
+  )
+)
+(assert_return (invoke "call-7") (i32.const 65))
+(assert_return (invoke "call-9") (i32.const 66))
+
+;; Corner cases
+
+(module
+  (table 10 funcref)
+  (func $f)
+  (elem (i32.const 9) $f)
+)
+
+(module
+  (table 0 funcref)
+  (elem (i32.const 0))
+)
+
+(module
+  (table 0 0 funcref)
+  (elem (i32.const 0))
+)
+
+(module
+  (table 20 funcref)
+  (elem (i32.const 20))
+)
+
+;; Two elements target the same slot
+
+(module
+  (type $out-i32 (func (result i32)))
+  (table 10 funcref)
+  (elem (i32.const 9) $const-i32-a)
+  (elem (i32.const 9) $const-i32-b)
+  (func $const-i32-a (type $out-i32) (i32.const 65))
+  (func $const-i32-b (type $out-i32) (i32.const 66))
+  (func (export "call-overwritten") (type $out-i32)
+    (call_indirect (type $out-i32) (i32.const 9))
+  )
+)
+(assert_return (invoke "call-overwritten") (i32.const 66))

From c0666116e788ee3a37a9768c0b9e346465d8da27 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Thu, 1 Aug 2024 08:15:51 -0400
Subject: [PATCH 11/11] crucible-wasm: Add select-related test case

We have recently made some changes to the way `crucible-wasm` handled the
`select` instruction, so this test case helps ensure that we have not broken
anything that used to work before.
---
 crucible-wasm/test-data/select.good |   1 +
 crucible-wasm/test-data/select.wast | 311 ++++++++++++++++++++++++++++
 2 files changed, 312 insertions(+)
 create mode 100644 crucible-wasm/test-data/select.good
 create mode 100644 crucible-wasm/test-data/select.wast

diff --git a/crucible-wasm/test-data/select.good b/crucible-wasm/test-data/select.good
new file mode 100644
index 000000000..9c7ea10d9
--- /dev/null
+++ b/crucible-wasm/test-data/select.good
@@ -0,0 +1 @@
+[Crux] Overall status: Valid.
diff --git a/crucible-wasm/test-data/select.wast b/crucible-wasm/test-data/select.wast
new file mode 100644
index 000000000..f57c4791c
--- /dev/null
+++ b/crucible-wasm/test-data/select.wast
@@ -0,0 +1,311 @@
+;; Adapted from the select test case in
+;;
+;;   https://github.com/WebAssembly/spec/blob/351d8b1026a2a820e88baae54557c43e775fd5a5/test/core/select.wast
+
+(module
+  ;; Auxiliary
+  (func $dummy)
+  (table $tab funcref (elem $dummy))
+  (memory 1)
+
+  (func (export "select-i32") (param i32 i32 i32) (result i32)
+    (select (local.get 0) (local.get 1) (local.get 2))
+  )
+  (func (export "select-i64") (param i64 i64 i32) (result i64)
+    (select (local.get 0) (local.get 1) (local.get 2))
+  )
+  (func (export "select-f32") (param f32 f32 i32) (result f32)
+    (select (local.get 0) (local.get 1) (local.get 2))
+  )
+  (func (export "select-f64") (param f64 f64 i32) (result f64)
+    (select (local.get 0) (local.get 1) (local.get 2))
+  )
+
+  (func (export "select-i32-t") (param i32 i32 i32) (result i32)
+    (select (result i32) (local.get 0) (local.get 1) (local.get 2))
+  )
+  (func (export "select-i64-t") (param i64 i64 i32) (result i64)
+    (select (result i64) (local.get 0) (local.get 1) (local.get 2))
+  )
+  (func (export "select-f32-t") (param f32 f32 i32) (result f32)
+    (select (result f32) (local.get 0) (local.get 1) (local.get 2))
+  )
+  (func (export "select-f64-t") (param f64 f64 i32) (result f64)
+    (select (result f64) (local.get 0) (local.get 1) (local.get 2))
+  )
+
+  ;; As the argument of control constructs and instructions
+
+  (func (export "as-select-first") (param i32) (result i32)
+    (select (select (i32.const 0) (i32.const 1) (local.get 0)) (i32.const 2) (i32.const 3))
+  )
+  (func (export "as-select-mid") (param i32) (result i32)
+    (select (i32.const 2) (select (i32.const 0) (i32.const 1) (local.get 0)) (i32.const 3))
+  )
+  (func (export "as-select-last") (param i32) (result i32)
+    (select (i32.const 2) (i32.const 3) (select (i32.const 0) (i32.const 1) (local.get 0)))
+  )
+
+  (func (export "as-loop-first") (param i32) (result i32)
+    (loop (result i32) (select (i32.const 2) (i32.const 3) (local.get 0)) (call $dummy) (call $dummy))
+  )
+  (func (export "as-loop-mid") (param i32) (result i32)
+    (loop (result i32) (call $dummy) (select (i32.const 2) (i32.const 3) (local.get 0)) (call $dummy))
+  )
+  (func (export "as-loop-last") (param i32) (result i32)
+    (loop (result i32) (call $dummy) (call $dummy) (select (i32.const 2) (i32.const 3) (local.get 0)))
+  )
+
+  (func (export "as-if-condition") (param i32)
+    (select (i32.const 2) (i32.const 3) (local.get 0)) (if (then (call $dummy)))
+  )
+  (func (export "as-if-then") (param i32) (result i32)
+    (if (result i32) (i32.const 1) (then (select (i32.const 2) (i32.const 3) (local.get 0))) (else (i32.const 4)))
+  )
+  (func (export "as-if-else") (param i32) (result i32)
+    (if (result i32) (i32.const 0) (then (i32.const 2)) (else (select (i32.const 2) (i32.const 3) (local.get 0))))
+  )
+
+  (func (export "as-br_if-first") (param i32) (result i32)
+    (block (result i32) (br_if 0 (select (i32.const 2) (i32.const 3) (local.get 0)) (i32.const 4)))
+  )
+  (func (export "as-br_if-last") (param i32) (result i32)
+    (block (result i32) (br_if 0 (i32.const 2) (select (i32.const 2) (i32.const 3) (local.get 0))))
+  )
+
+  (func (export "as-br_table-first") (param i32) (result i32)
+    (block (result i32) (select (i32.const 2) (i32.const 3) (local.get 0)) (i32.const 2) (br_table 0 0))
+  )
+  (func (export "as-br_table-last") (param i32) (result i32)
+    (block (result i32) (i32.const 2) (select (i32.const 2) (i32.const 3) (local.get 0)) (br_table 0 0))
+  )
+
+  (func $func (param i32 i32) (result i32) (local.get 0))
+  (type $check (func (param i32 i32) (result i32)))
+  (table $t funcref (elem $func))
+  (func (export "as-call_indirect-first") (param i32) (result i32)
+    (block (result i32)
+      (call_indirect $t (type $check)
+        (select (i32.const 2) (i32.const 3) (local.get 0)) (i32.const 1) (i32.const 0)
+      )
+    )
+  )
+  (func (export "as-call_indirect-mid") (param i32) (result i32)
+    (block (result i32)
+      (call_indirect $t (type $check)
+        (i32.const 1) (select (i32.const 2) (i32.const 3) (local.get 0)) (i32.const 0)
+      )
+    )
+  )
+  (func (export "as-call_indirect-last") (param i32) (result i32)
+    (block (result i32)
+      (call_indirect $t (type $check)
+        (i32.const 1) (i32.const 4) (select (i32.const 2) (i32.const 3) (local.get 0))
+      )
+    )
+  )
+
+  (func (export "as-store-first") (param i32)
+    (select (i32.const 0) (i32.const 4) (local.get 0)) (i32.const 1) (i32.store)
+  )
+  (func (export "as-store-last") (param i32)
+    (i32.const 8) (select (i32.const 1) (i32.const 2) (local.get 0)) (i32.store)
+  )
+
+  ;; (func (export "as-memory.grow-value") (param i32) (result i32)
+  ;;   (memory.grow (select (i32.const 1) (i32.const 2) (local.get 0)))
+  ;; )
+
+  (func $f (param i32) (result i32) (local.get 0))
+
+  (func (export "as-call-value") (param i32) (result i32)
+    (call $f (select (i32.const 1) (i32.const 2) (local.get 0)))
+  )
+  (func (export "as-return-value") (param i32) (result i32)
+    (select (i32.const 1) (i32.const 2) (local.get 0)) (return)
+  )
+  (func (export "as-drop-operand") (param i32)
+    (drop (select (i32.const 1) (i32.const 2) (local.get 0)))
+  )
+  (func (export "as-br-value") (param i32) (result i32)
+    (block (result i32) (br 0 (select (i32.const 1) (i32.const 2) (local.get 0))))
+  )
+  (func (export "as-local.set-value") (param i32) (result i32)
+    (local i32) (local.set 0 (select (i32.const 1) (i32.const 2) (local.get 0))) (local.get 0)
+  )
+  (func (export "as-local.tee-value") (param i32) (result i32)
+    (local.tee 0 (select (i32.const 1) (i32.const 2) (local.get 0)))
+  )
+  (global $a (mut i32) (i32.const 10))
+  (func (export "as-global.set-value") (param i32) (result i32)
+    (global.set $a (select (i32.const 1) (i32.const 2) (local.get 0)))
+    (global.get $a)
+  )
+  (func (export "as-load-operand") (param i32) (result i32)
+    (i32.load (select (i32.const 0) (i32.const 4) (local.get 0)))
+  )
+
+  (func (export "as-unary-operand") (param i32) (result i32)
+    (i32.eqz (select (i32.const 0) (i32.const 1) (local.get 0)))
+  )
+  (func (export "as-binary-operand") (param i32) (result i32)
+    (i32.mul
+      (select (i32.const 1) (i32.const 2) (local.get 0))
+      (select (i32.const 1) (i32.const 2) (local.get 0))
+    )
+  )
+  (func (export "as-test-operand") (param i32) (result i32)
+    (block (result i32)
+      (i32.eqz (select (i32.const 0) (i32.const 1) (local.get 0)))
+    )
+  )
+
+  (func (export "as-compare-left") (param i32) (result i32)
+    (block (result i32)
+      (i32.le_s (select (i32.const 1) (i32.const 2) (local.get 0)) (i32.const 1))
+    )
+  )
+  (func (export "as-compare-right") (param i32) (result i32)
+    (block (result i32)
+      (i32.ne (i32.const 1) (select (i32.const 0) (i32.const 1) (local.get 0)))
+    )
+  )
+
+  ;; (func (export "as-convert-operand") (param i32) (result i32)
+  ;;   (block (result i32)
+  ;;     (i32.wrap_i64 (select (i64.const 1) (i64.const 0) (local.get 0)))
+  ;;   )
+  ;; )
+)
+
+(assert_return (invoke "select-i32" (i32.const 1) (i32.const 2) (i32.const 1)) (i32.const 1))
+(assert_return (invoke "select-i64" (i64.const 2) (i64.const 1) (i32.const 1)) (i64.const 2))
+;; (assert_return (invoke "select-f32" (f32.const 1) (f32.const 2) (i32.const 1)) (f32.const 1))
+;; (assert_return (invoke "select-f64" (f64.const 1) (f64.const 2) (i32.const 1)) (f64.const 1))
+
+(assert_return (invoke "select-i32" (i32.const 1) (i32.const 2) (i32.const 0)) (i32.const 2))
+(assert_return (invoke "select-i32" (i32.const 2) (i32.const 1) (i32.const 0)) (i32.const 1))
+(assert_return (invoke "select-i64" (i64.const 2) (i64.const 1) (i32.const -1)) (i64.const 2))
+(assert_return (invoke "select-i64" (i64.const 2) (i64.const 1) (i32.const 0xf0f0f0f0)) (i64.const 2))
+
+;; (assert_return (invoke "select-f32" (f32.const nan) (f32.const 1) (i32.const 1)) (f32.const nan))
+;; (assert_return (invoke "select-f32" (f32.const nan:0x20304) (f32.const 1) (i32.const 1)) (f32.const nan:0x20304))
+;; (assert_return (invoke "select-f32" (f32.const nan) (f32.const 1) (i32.const 0)) (f32.const 1))
+;; (assert_return (invoke "select-f32" (f32.const nan:0x20304) (f32.const 1) (i32.const 0)) (f32.const 1))
+;; (assert_return (invoke "select-f32" (f32.const 2) (f32.const nan) (i32.const 1)) (f32.const 2))
+;; (assert_return (invoke "select-f32" (f32.const 2) (f32.const nan:0x20304) (i32.const 1)) (f32.const 2))
+;; (assert_return (invoke "select-f32" (f32.const 2) (f32.const nan) (i32.const 0)) (f32.const nan))
+;; (assert_return (invoke "select-f32" (f32.const 2) (f32.const nan:0x20304) (i32.const 0)) (f32.const nan:0x20304))
+
+;; (assert_return (invoke "select-f64" (f64.const nan) (f64.const 1) (i32.const 1)) (f64.const nan))
+;; (assert_return (invoke "select-f64" (f64.const nan:0x20304) (f64.const 1) (i32.const 1)) (f64.const nan:0x20304))
+;; (assert_return (invoke "select-f64" (f64.const nan) (f64.const 1) (i32.const 0)) (f64.const 1))
+;; (assert_return (invoke "select-f64" (f64.const nan:0x20304) (f64.const 1) (i32.const 0)) (f64.const 1))
+;; (assert_return (invoke "select-f64" (f64.const 2) (f64.const nan) (i32.const 1)) (f64.const 2))
+;; (assert_return (invoke "select-f64" (f64.const 2) (f64.const nan:0x20304) (i32.const 1)) (f64.const 2))
+;; (assert_return (invoke "select-f64" (f64.const 2) (f64.const nan) (i32.const 0)) (f64.const nan))
+;; (assert_return (invoke "select-f64" (f64.const 2) (f64.const nan:0x20304) (i32.const 0)) (f64.const nan:0x20304))
+
+(assert_return (invoke "select-i32-t" (i32.const 1) (i32.const 2) (i32.const 1)) (i32.const 1))
+(assert_return (invoke "select-i64-t" (i64.const 2) (i64.const 1) (i32.const 1)) (i64.const 2))
+;; (assert_return (invoke "select-f32-t" (f32.const 1) (f32.const 2) (i32.const 1)) (f32.const 1))
+;; (assert_return (invoke "select-f64-t" (f64.const 1) (f64.const 2) (i32.const 1)) (f64.const 1))
+
+(assert_return (invoke "select-i32-t" (i32.const 1) (i32.const 2) (i32.const 0)) (i32.const 2))
+(assert_return (invoke "select-i32-t" (i32.const 2) (i32.const 1) (i32.const 0)) (i32.const 1))
+(assert_return (invoke "select-i64-t" (i64.const 2) (i64.const 1) (i32.const -1)) (i64.const 2))
+(assert_return (invoke "select-i64-t" (i64.const 2) (i64.const 1) (i32.const 0xf0f0f0f0)) (i64.const 2))
+
+;; (assert_return (invoke "select-f32-t" (f32.const nan) (f32.const 1) (i32.const 1)) (f32.const nan))
+;; (assert_return (invoke "select-f32-t" (f32.const nan:0x20304) (f32.const 1) (i32.const 1)) (f32.const nan:0x20304))
+;; (assert_return (invoke "select-f32-t" (f32.const nan) (f32.const 1) (i32.const 0)) (f32.const 1))
+;; (assert_return (invoke "select-f32-t" (f32.const nan:0x20304) (f32.const 1) (i32.const 0)) (f32.const 1))
+;; (assert_return (invoke "select-f32-t" (f32.const 2) (f32.const nan) (i32.const 1)) (f32.const 2))
+;; (assert_return (invoke "select-f32-t" (f32.const 2) (f32.const nan:0x20304) (i32.const 1)) (f32.const 2))
+;; (assert_return (invoke "select-f32-t" (f32.const 2) (f32.const nan) (i32.const 0)) (f32.const nan))
+;; (assert_return (invoke "select-f32-t" (f32.const 2) (f32.const nan:0x20304) (i32.const 0)) (f32.const nan:0x20304))
+;;
+;; (assert_return (invoke "select-f64-t" (f64.const nan) (f64.const 1) (i32.const 1)) (f64.const nan))
+;; (assert_return (invoke "select-f64-t" (f64.const nan:0x20304) (f64.const 1) (i32.const 1)) (f64.const nan:0x20304))
+;; (assert_return (invoke "select-f64-t" (f64.const nan) (f64.const 1) (i32.const 0)) (f64.const 1))
+;; (assert_return (invoke "select-f64-t" (f64.const nan:0x20304) (f64.const 1) (i32.const 0)) (f64.const 1))
+;; (assert_return (invoke "select-f64-t" (f64.const 2) (f64.const nan) (i32.const 1)) (f64.const 2))
+;; (assert_return (invoke "select-f64-t" (f64.const 2) (f64.const nan:0x20304) (i32.const 1)) (f64.const 2))
+;; (assert_return (invoke "select-f64-t" (f64.const 2) (f64.const nan) (i32.const 0)) (f64.const nan))
+;; (assert_return (invoke "select-f64-t" (f64.const 2) (f64.const nan:0x20304) (i32.const 0)) (f64.const nan:0x20304))
+
+(assert_return (invoke "as-select-first" (i32.const 0)) (i32.const 1))
+(assert_return (invoke "as-select-first" (i32.const 1)) (i32.const 0))
+(assert_return (invoke "as-select-mid" (i32.const 0)) (i32.const 2))
+(assert_return (invoke "as-select-mid" (i32.const 1)) (i32.const 2))
+(assert_return (invoke "as-select-last" (i32.const 0)) (i32.const 2))
+(assert_return (invoke "as-select-last" (i32.const 1)) (i32.const 3))
+
+(assert_return (invoke "as-loop-first" (i32.const 0)) (i32.const 3))
+(assert_return (invoke "as-loop-first" (i32.const 1)) (i32.const 2))
+(assert_return (invoke "as-loop-mid" (i32.const 0)) (i32.const 3))
+(assert_return (invoke "as-loop-mid" (i32.const 1)) (i32.const 2))
+(assert_return (invoke "as-loop-last" (i32.const 0)) (i32.const 3))
+(assert_return (invoke "as-loop-last" (i32.const 1)) (i32.const 2))
+
+(assert_return (invoke "as-if-condition" (i32.const 0)))
+(assert_return (invoke "as-if-condition" (i32.const 1)))
+(assert_return (invoke "as-if-then" (i32.const 0)) (i32.const 3))
+(assert_return (invoke "as-if-then" (i32.const 1)) (i32.const 2))
+(assert_return (invoke "as-if-else" (i32.const 0)) (i32.const 3))
+(assert_return (invoke "as-if-else" (i32.const 1)) (i32.const 2))
+
+(assert_return (invoke "as-br_if-first" (i32.const 0)) (i32.const 3))
+(assert_return (invoke "as-br_if-first" (i32.const 1)) (i32.const 2))
+(assert_return (invoke "as-br_if-last" (i32.const 0)) (i32.const 2))
+(assert_return (invoke "as-br_if-last" (i32.const 1)) (i32.const 2))
+
+(assert_return (invoke "as-br_table-first" (i32.const 0)) (i32.const 3))
+(assert_return (invoke "as-br_table-first" (i32.const 1)) (i32.const 2))
+(assert_return (invoke "as-br_table-last" (i32.const 0)) (i32.const 2))
+(assert_return (invoke "as-br_table-last" (i32.const 1)) (i32.const 2))
+
+(assert_return (invoke "as-call_indirect-first" (i32.const 0)) (i32.const 3))
+(assert_return (invoke "as-call_indirect-first" (i32.const 1)) (i32.const 2))
+(assert_return (invoke "as-call_indirect-mid" (i32.const 0)) (i32.const 1))
+(assert_return (invoke "as-call_indirect-mid" (i32.const 1)) (i32.const 1))
+(assert_trap (invoke "as-call_indirect-last" (i32.const 0)) "undefined element")
+(assert_trap (invoke "as-call_indirect-last" (i32.const 1)) "undefined element")
+
+(assert_return (invoke "as-store-first" (i32.const 0)))
+(assert_return (invoke "as-store-first" (i32.const 1)))
+(assert_return (invoke "as-store-last" (i32.const 0)))
+(assert_return (invoke "as-store-last" (i32.const 1)))
+
+;; (assert_return (invoke "as-memory.grow-value" (i32.const 0)) (i32.const 1))
+;; (assert_return (invoke "as-memory.grow-value" (i32.const 1)) (i32.const 3))
+
+(assert_return (invoke "as-call-value" (i32.const 0)) (i32.const 2))
+(assert_return (invoke "as-call-value" (i32.const 1)) (i32.const 1))
+(assert_return (invoke "as-return-value" (i32.const 0)) (i32.const 2))
+(assert_return (invoke "as-return-value" (i32.const 1)) (i32.const 1))
+(assert_return (invoke "as-drop-operand" (i32.const 0)))
+(assert_return (invoke "as-drop-operand" (i32.const 1)))
+(assert_return (invoke "as-br-value" (i32.const 0)) (i32.const 2))
+(assert_return (invoke "as-br-value" (i32.const 1)) (i32.const 1))
+(assert_return (invoke "as-local.set-value" (i32.const 0)) (i32.const 2))
+(assert_return (invoke "as-local.set-value" (i32.const 1)) (i32.const 1))
+(assert_return (invoke "as-local.tee-value" (i32.const 0)) (i32.const 2))
+(assert_return (invoke "as-local.tee-value" (i32.const 1)) (i32.const 1))
+(assert_return (invoke "as-global.set-value" (i32.const 0)) (i32.const 2))
+(assert_return (invoke "as-global.set-value" (i32.const 1)) (i32.const 1))
+(assert_return (invoke "as-load-operand" (i32.const 0)) (i32.const 1))
+(assert_return (invoke "as-load-operand" (i32.const 1)) (i32.const 1))
+
+(assert_return (invoke "as-unary-operand" (i32.const 0)) (i32.const 0))
+(assert_return (invoke "as-unary-operand" (i32.const 1)) (i32.const 1))
+(assert_return (invoke "as-binary-operand" (i32.const 0)) (i32.const 4))
+(assert_return (invoke "as-binary-operand" (i32.const 1)) (i32.const 1))
+(assert_return (invoke "as-test-operand" (i32.const 0)) (i32.const 0))
+(assert_return (invoke "as-test-operand" (i32.const 1)) (i32.const 1))
+(assert_return (invoke "as-compare-left" (i32.const 0)) (i32.const 0))
+(assert_return (invoke "as-compare-left" (i32.const 1)) (i32.const 1))
+(assert_return (invoke "as-compare-right" (i32.const 0)) (i32.const 0))
+(assert_return (invoke "as-compare-right" (i32.const 1)) (i32.const 1))
+;; (assert_return (invoke "as-convert-operand" (i32.const 0)) (i32.const 0))
+;; (assert_return (invoke "as-convert-operand" (i32.const 1)) (i32.const 1))