Skip to content

Conversation

@yoshihiro503
Copy link
Contributor

Both vtestop and vshiftop are of type N, so the code compiles. However, shouldn't the type of the first argument to app_vshiftop_str be vshiftop rather than vtestop?

see also:

Definition app_vshiftop (op: vshiftop) (v1: value_vec) (v2: i32) : value_vec :=
let v1e := encode_vec v1 in
let v2e := encode_i32 v2 in
decode_vec (app_vshiftop_str op v1e v2e).

Both `vtestop` and `vshiftop` are of type `$\mathcal{N}$`, so the code compiles. However, shouldn't the type of the first argument to `app_vshiftop_str` be `vshiftop` rather than `vtestop`?
@raoxiaojia
Copy link
Contributor

raoxiaojia commented Dec 10, 2025

Indeed, this was probably a typo I made when I was copying the lines around. Thanks for the correction!

@raoxiaojia raoxiaojia merged commit 77e1d86 into WasmCert:master Dec 10, 2025
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants