* Consolidate wasm features in `config.rs`

Use the `WASM3` fixed feature set which Wasmtime now implements by
default.

* Adjust some comments

* Changes to the veri subtree: replace entire verification engine

Co-authored-by: Michael McLoughlin <mmcloughlin@gmail.com>

* New ISLE spec files

Co-authored-by: Michael McLoughlin <mmcloughlin@gmail.com>

* ISLE implementation changes

Co-authored-by: Michael McLoughlin <mmcloughlin@gmail.com>

* Changes to existing ISLE backend files and related

Co-authored-by: Michael McLoughlin <mmcloughlin@gmail.com>

* Remaining broader changes.

Co-authored-by: Michael McLoughlin <mmcloughlin@gmail.com>

* Update comment

* Delete some output files

* More cleanup

* Reference tweaks

* More cleanup

* Remove unneeded rec tag

* Remove pub comments, revert more unneeded changes

* More veri prelude files to spec subdir

* fmt

* Update CI exclude

* Workspace deps, clippy

* Update github workflow

* Remove more pub comments

* Missing docs reason

* More format

* fmt

* Update threading logic, README

* Depend on upstream ASLp and aslp-rpc for ISA spec generation

Replace the personal mmcloughlin/aslp fork with the upstream UQ-PAC
packages: aslp 0.3.2 (symbolic-opcode support, merged via PR #145) plus
the aslp_server_http server, which migrated to the aslp-rpc repo
(v0.1.4). The server is wire-compatible, so the Rust client and parser
are unchanged.

setup/install-aslp.sh installs both packages into a dedicated `aslp`
opam switch (OCaml >= 5.0, required by aslp_server_http's eio deps) via
opam pin, replacing the fork tarball + dune build. The installers (aslp,
cvc5, z3) move from veri/script/install/ to a shared setup/ dir at the
subtree root, matching wasmtime's flat install-<tool>.sh convention.
generate.sh and the aslp test-data script launch aslp_server_http / asli
via `opam exec --switch` (overridable with ASLP_SWITCH); no PATH setup.
README updated accordingly.

EXTR is temporarily disabled in the alu_rrr_shift sweep: upstream 0.3.2
cannot lift it (the symbolic lsb yields an unsimplified, non-constant
slice width that the RASL backend rejects), a regression vs the fork.
Tracked separately.

* Enable EXTR via PR-fork ASLp pin; regenerate specs

Temporarily pin asli to mmcloughlin/aslp#extr-fix (UQ-PAC/aslp PR #152),
which fixes symbolic-EXTR lifting: is_pure_exp now treats bit-literals as
pure, so sym_sub_int folds EXTR's slice width to a constant instead of
leaving a non-constant expression the RASL check rejects. With that,
isaspec can lift EXTR again, so re-enable ALUOp::Extr in the
alu_rrr_shift sweep.

Regenerate the AArch64 ISA specs with upstream ASLp + the fix. EXTR
returns to alu_rrr_shift.isle; the rest of the churn is upstream's
equivalent reformulation -- loads keep the loaded value in a constdecl
(new RASL load invariant), conds use a branchless bitvector mux, SDIV
drops a redundant INT_MIN/-1 special-case, and loads/stores gain
`modifies` annotations.

Revert the asli pin to an upstream release once PR #152 merges.

* Small readme tweak

* Clarify ASLp fork-pin comment in install-aslp.sh

* Drop reqwest from the ASLp client

Drive hyper over a tokio TcpStream instead, removing reqwest's async/TLS tree
and the duplicate hyper/http/base64 versions it introduced. No new lockfile
crates; regenerated specs are byte-identical.

* Drop proc-macro-error from veri test-macros

Parse attributes with syn::meta::parser and report errors via an `expand`
function returning syn::Result + into_compile_error, matching the convention in
the other wasmtime proc-macros. Removes the unmaintained proc-macro-error
(RUSTSEC-2024-0370) and the syn 1.0 duplicate it pulled in.

* Drop enquote from the ASLp parser

Make the ident/bits grammar rules compound-atomic so their quoted content
comes through as inner pairs, and read those directly instead of stripping
quotes with enquote. Regenerated specs are byte-identical.

* Define veri-only deps in their own crate manifests

Move pest/pest_derive (aslp) and num-bigint/num-traits/easy-smt (veri) out of
the workspace root and into the single crate that uses each, keeping the shared
workspace dependencies to crates with more than one consumer. Versions and lock
resolution are unchanged.

* Update veri-only deps to current versions

Bump pest/pest_derive to 2.8.6, num-bigint to 0.4.6, and num-traits to 0.2.19
(version-floor hygiene; lock unchanged), and easy-smt 0.2 -> 0.3.2, adjusting
for its ContextBuilder solver/solver_args split.

* Remove veri_ir

* Pin ASLp to upstream now that UQ-PAC/aslp#152 has landed

The symbolic-EXTR lift fix merged upstream (UQ-PAC/aslp#152), so asli no longer
needs the fork. Pin it to the upstream merge commit (not yet in a tagged
release). Regenerated specs are byte-identical.

* Pin ASLp to the 0.3.4 release

UQ-PAC/aslp 0.3.4 shipped with the symbolic-EXTR fix, so pin asli to the release
tag instead of the merge commit. 0.3.4 differs from the previously pinned commit
only by a CHANGES.md edit (no code change), so the generated specs are
unaffected.

* Cranelift: Remove the `{band,bor,bxor}_not` instructions (bytecodealliance#13590)

They were immediately legalized into `op(x, bnot(y))` so instead we just emit
those instructions immediately in `InstBuilder` convenience/backwards-compat
methods.

* Remove some uses of `ir::GlobalValue`s from Wasm-to-CLIF translation (bytecodealliance#13593)

* Cranelift: use the vmctx param directly in `vmctx_val`

Return the function's `VMContext` special parameter instead of emitting a
`global_value` instruction, which is exactly what the legalizer would
desugar it into.

* Cranelift: load the `*mut VMStoreContext` directly in `get_vmstore_context_ptr`

* Cranelift: use the vmctx value directly in `epoch_ptr`

Instead of via the `ir::GlobalValue`.

* Enable the Wasm GC proposal by default (bytecodealliance#13594)

* Enable the Wasm GC proposal by default

And also the function references proposal, which was effectively folded into the
GC proposal.

Resolves bytecodealliance#13216

Resolves bytecodealliance#5032

* Also update docs/stability-tiers.md

* review feedback

* wizer: support init func as a wave function call (components only) (bytecodealliance#13582)

* wizer: support init func as a wave function call (components only)

* rustfmt

* wizer: test program using wit interfaces and wave expressions

* wizer: wasmtime-cli fixes and tests

* wasmtime-cli: improve doc text for wizer and run --invoke

* wizer: plumb through output of init func as Val / wave func results

* rustfmt

* fix test

* Update wasi-testsuite and get it running (bytecodealliance#13592)

* Update wasi-testsuite and get it running

This commit updates wasi-testsuite to its latest revision and updates to
run the new `*.json` infrastructure that's present. This involves more
functionality such as making TCP connections, making HTTP requests,
reading/writing stdio, etc.

prtest:full

* Try to add some debugging

* Always serve on localhost

* Update some deps on their major version tracks (bytecodealliance#13570)

* Update webpki-roots dependency

Move it onto the 1.x.y version track.

* Update mutates to 0.5.x

* Update similar to 3.x.y

* Update cpp_demangle to 0.5.x

* Add another license

* Update wasi-testsuite again (bytecodealliance#13595)

Pull in a fix to ungate a test on Linux.

Closes bytecodealliance#13396

* Fix some build warnings on macos (bytecodealliance#13598)

* Set `IPV6_V6ONLY` for UDP sockets (bytecodealliance#13596)

* Set `IPV6_V6ONLY` for UDP sockets

Addresses a failure in an upstream wasi-testsuite test. The remaining
`sockets-udp-send` test is not fully passing just yet but this at least
gets it a bit further.

Closes bytecodealliance#12475

* Print more error information

prtest:full

* Windows error code

* Do not use `ir::GlobalValue`s for GC heap base and bound (bytecodealliance#13600)

* Cranelift: load the GC heap base directly in `get_gc_heap_base`

* Cranelift: load the GC heap bound directly in `get_gc_heap_bound`

* review feedback

* Always use the vmctx alias region for all loads from within the vmctx (bytecodealliance#13599)

Additionally slightly refactors `AliasRegionKey` to have a `Vm { ty: VmType,
... }` variant instead of `AliasRegionKey::VMContext` and
`AliasRegionKey::VMStoreContext` variants (and `VMMemoryDefinition`,
`VMTableDefinition`, etc... in commits to follow this one).

* Wasmtime: enable exception-handling by default. (bytecodealliance#13603)

* Wasmtime: enable exception-handling by default.

Following [discussion in the most recent Wasmtime
meeting](https://github.com/bytecodealliance/meetings/blob/main/wasmtime/2026/wasmtime-06-04.md),
and following the enablement by default of garbage collection (bytecodealliance#13594),
we are now ready to ship [Wasm exception
handling](https://github.com/WebAssembly/exception-handling) as well. It
has been fuzzed for a while now, has good test coverage, has not had a
reported bug for quite a while, and in general meets our requirements
for tier-1 features. This PR thus promotes it to tier 1 (on all
platforms, with the Cranelift compiler backend) and enables it by
default.

May exceptions be the norm!

* Exceptions on by default only when `gc` build-time feature is enabled.

* Flag most wasi-testsuite tests as expected to pass (bytecodealliance#13602)

Upstream refactorings mean that we should be able to ratchet this for
all tests now to keep them passing on all platforms.

prtest:full

* fix: substituted_component_type panic on guest-exported resources (bytecodealliance#13608)

* add test for `substituted_component_type` panic

`Linker::substituted_component_type` builds a `types::Component` whose
resource substitution map is `Some(..)` but only covers the component's
*imported* resources. Introspecting an exported function that references
an *exported* (non-imported) resource then panics with an
index-out-of-bounds, because `InstanceType::resource_type` hard-indexes
that partial map (`matching.rs`) instead of falling back to treating an
absent resource as uninstantiated.

This adds a test that builds a component exporting a resource plus a
constructor returning `own<t>` and a method taking `borrow<t>`, then
walks the introspected function types via `substituted_component_type`.
It panics today (index out of bounds) and will pass once the resolver
falls back gracefully.

Assisted-by: claude:claude-opus-4-8

* fix panic on guest-exported resources

`Linker::substituted_component_type` constructs the introspection type
with `resources: Some(&cx.imported_resources)`, a map that only contains
the component's *imported* resources. `InstanceType::resource_type`
previously hard-indexed that map (`self.resources.map(|t| t[ty])`), so
resolving a resource that is not in the map -- e.g. a resource the
component *exports* -- panicked with an index-out-of-bounds whenever an
exported function's params/results referenced it.

Fix this by using a fallible lookup and falling back to
`ResourceType::uninstantiated` when the resource is absent from the map,
exactly as the `resources: None` path already does. This is the
semantically correct behavior: a resource that has no substitution is
"not (yet) instantiated", which is also what `Component::component_type()`
relies on (it passes `resources: None`). With this fix the same safe,
public introspection API no longer panics depending on which (also
public) API produced the `types::Component`.

Assisted-by: claude:claude-opus-4-8

* fix(tests): loosen p3 outbound content length error conditions (bytecodealliance#13606)

This commit updates the test to allow for timings that match
non-wasmtime implementations (i.e. Jco), which may not report the
intermediate error (`ErrorCode::HttpProtocolError`) ahead of the
"real" expected error (`ErrorCode::HttpRequestBodySize`)

* Remove `ExceptionTable::lookup_pc_tag` (bytecodealliance#13604)

This helps keep wasm/clif-util using the same exact code and
additionally removes the implicit assumption that tags are sorted which
isn't always the case for wasm. The replacement isn't a perfect fit but
it's workable enough for clif-util.

* Add bounds-checked unsafe intrinsics (bytecodealliance#13597)

* Add bounds-checked unsafe intrinsics

These intrinsics are similar to the unchecked versions, but instead of taking a
raw address, take a base, offset, and length. They do a bounds check first, and
trap on out-of-bounds accesses or perform the actual in-bounds access. When
Spectre mitigations are enabled, their bounds check has Spectre mitigations
applied.

* review feedback

* fix i686 tests in CI

* fix i686 tests, take two

prtest:full

* Use `TranslateTrap` instead of emitting `trap[n]z` directly

This means we will correctly call the raise-trap libcall when signals-based
traps are disabled. However, it also means that `UnsafeIntrinsicCompiler` needed
to be refactored a bit to take a `FuncBuilder` rather than a `FuncCursor`, and
additionally take a generic `T: TranslateTrap`.

This should fix the s390x errors in CI.

* Reuse `UnsafeIntrinsicCompiler` inside `TrampolineCompiler` (bytecodealliance#13601)

Rather than duplicating all the compilation of unsafe intrinsics.

* Consolidate wasm features in `config.rs` (bytecodealliance#13605)

* Consolidate wasm features in `config.rs`

Use the `WASM3` fixed feature set which Wasmtime now implements by
default.

* Adjust some comments

* [gc_fuzz]: Add and complete i31 (bytecodealliance#13609)

* Add and complete i31

* Add forgotten import

* Fix x64 rules, update filtering/printing logic, remove dead/unused aarch64 rules

* fix merge

* fix merge

* fmt

* Config files; prtest:all

* clippy; prtest:all

* Remove expected lint failure because the aarch64 ISLE sufficiently changed to not hit it; prtest:all

* fix doc error in now-public files; prtest:all

* Add config files, modify publish for isle crate; prtest:all

* Tweak rerun-if-changed for isle printer tests in isle build.rs; prtest:all

* Only keep existing isle printer test; prtest:all

* fmt; prtest:all

* printer tests fix; prtest:all

* revert most Cargo.lock changes; prtest:all

* Minimize Cargo.lock diff against main

An earlier incidental `cargo update` bumped ~hundreds of transitive deps
(tracing, clap, cc, ...), inflating the cargo-vet backlog to ~425k LoC. Reset
Cargo.lock to main's versions and re-resolve, so the only additions are the
veri crates' genuine deps (num-bigint, the pest family, easy-smt). The vet
backlog drops to ~51k LoC, and everything else stays at main's vetted versions.

* fix merge; prtest:all

* Avoid stack overflow in ISLE parser by raising stack size; prtest:all

* Verification: avoid stack overflow in Cranelift build by excluding specs. (#104)

The deeply-nested parsing requiring a larger stack in `build.rs`
probably also slows down the Cranelift build, which we also don't
want. On further thought the root issue is actually that we're trying
to parse these specs at all during an ordinary Cranelift
build (verification is a separate run). This commit excludes the
relevant ISLE sources entirely during normal builds, re-enabling them
when the `spec` Cargo feature (set by the veri-related crates) is
enabled.

* Exempt dependencies exclusively related to verification from vetting

* tweak unknown handling

* More unknown handling

---------

Co-authored-by: Michael McLoughlin <mmcloughlin@gmail.com>
Co-authored-by: Michael McLoughlin <mcloughlin@cmu.edu>
Co-authored-by: Nick Fitzgerald <fitzgen@gmail.com>
Co-authored-by: Pat Hickey <p.hickey@f5.com>
Co-authored-by: Alex Crichton <alex@alexcrichton.com>
Co-authored-by: Chris Fallin <chris@cfallin.org>
Co-authored-by: Roman Volosatovs <rvolosatovs@users.noreply.github.com>
Co-authored-by: Victor Adossi <123968127+vados-cosmonic@users.noreply.github.com>
Co-authored-by: Khagan (Khan) Karimov <127453117+khagankhan@users.noreply.github.com>