The bounds check of .at() is probably implemented by the following wasm instructions:

• i32.load: This loads a 32-bit value from a memory address given by an operand plus an offset.

  For example, i32.load offset=4 means load a 32-bit value from the address given by the operand plus 4 bytes. This is used to access the elements of the vectors.

• i32.eq: This compares two 32-bit values for equality and returns 1 if they are equal or 0 if they are not.

  For example, local.get 5 local.get 4 i32.eq means compare the values of local variables 5 and 4 and return the result (push to stack). This is used to check if the index is equal to the size of the vector.

• i32.le_u: This compares two 32-bit values for unsigned less than or equal and returns 1 if the first value is less than or equal to the second value or 0 if it is not.

  For example, i32.le_u local.get 13 local.get 12 means compare the values of local variables 13 and 12 and return the result. This is used to check if the index is within the bounds of the vector.

• br_if: This branches to a given label if a condition is true.

  For example, br_if 0 (;@2;) means branch to label @2 if the top of the stack is true (non-zero). This is used to exit a block or a loop if a bounds check fails.

In the with_bc.wat, the bounds checking of .at() is done by comparing the vector size and the index before accessing the memory. For example, in this part of the code:

local.get 15
local.get 16
i32.eq
br_if 0 (;@1;)
local.get 2
i32.load offset=4
local.get 2
i32.load
local.tee 7
i32.eq
br_if 0 (;@1;)
local.get 7
i32.load offset=4
local.get 7
i32.load
i32.sub
i32.const 2
i32.shr_s
local.get 1
i32.gt_u
drop
end
call $abort
unreachable)

The program checks if the vector size (local.get 15) and the index (local.get 16) are equal, and if so, it branches to label @1 which is the end of the function. Otherwise, it checks if the second vector size (local.get 2) and the second index (local.get 7) are equal, and if so, it also branches to label @1. Otherwise, it checks if the second index is greater than the difference between the second vector end and start (local.get 7), and if so, it calls $abort which throws an exception. These checks ensure that the index is within the bounds of the vector before accessing the memory.

Notes about reading wasm code

First, I looked at the function signature and the parameters. The function takes three i32 parameters, which are pointers to the vectors A, B and C. So I knew that local.get 0, local.get 1 and local.get 2 are the pointers to those vectors. I noticed that local 0 is used to store the return value of the function, so I assumed it corresponds to C. local 1 is used as the first parameter of the function $std::__2::vector<int__std::__2::allocator<int>>::at_unsigned_long_, so I assumed it corresponds to A and local 2 corresponds to B.

Second, I looked at how the vectors are initialized and accessed. The vectors are stored as arrays of i32 values, with the first element being the pointer to the data, the second element being the pointer to the end of the data, and the third element being the pointer to the capacity. So I knew that i32.load and i32.store are used to read and write the vector elements, and i32.load offset=4 and i32.store offset=4 are used to read and write the vector end pointers.

Third, I looked at how the loop variables are updated and compared. The loop variables are incremented by one in each iteration, and compared with the vector sizes or indices. So I knew that local.get 13, local.get 7 and local.get 2 are the loop variables for i, j, k respectively. I also knew that local.get 12, local.get 15, local.get 17 and local.get 16 are the vector sizes or indices for A.size(), C.size(), B.size() and C.at(i).size() respectively.

Fourth, I looked at how the matrix elements are computed and stored. The matrix elements are multiplied by each other and added to the previous value. I noticed that local 15 and local 16 are used to store the results of calling $std::__2::vector<int__std::__2::allocator<int>>::at_unsigned_long_ on A and B respectively, so I assumed they correspond to A.at(i).at(k) and B.at(k).at(j) respectively.