[DID-Lab-SZU]

--targets selected packages, which collided with the CPU target. The CPU
architecture was hard-coded to x86_64-unknown-none in
VERIFICATION_RUST_TARGET. Follow cargo-verus naming: --package/-p selects
packages and --target selects the Rust target triple, so a later architecture
can be verified without changing dv again.

Changes

• Packages: --package/-p on verify, focus, build, doc (was
  --target), and count. This frees -p in count, which was --print-all;
  --print-all now uses -a. Breaking for count -p: callers that used
  count -p for print-all must switch to count -a.
• Architecture: --target <TRIPLE> on verify, focus, build, doc, and
  count, defaulting to x86_64-unknown-none. Unsupported triples are rejected
  at parse time; experimental triples are accepted with a warning.
• verus.rs: DEFAULT_RUST_TARGET, parse_rust_target, SUPPORTED_RUST_TARGETS
  (accepted) and VALIDATED_RUST_TARGETS (x86 only). The triple is passed to
  cargo-verus --target, dependency resolution, and the cached dependency file,
  named {package}.{triple}.{release|debug}.deps.toml.
• doc.rs: the triple is used for rustdoc --target and for locating artifacts
  under the triple-prefixed directories. The missing-dependency error suggests
  the exact cargo dv build --package <dep> --target <triple> command.
• count.rs: the triple is used to find cargo-verus dep-info. count --module
  selects the #[path] declaration whose cfg(target_arch) matches the target
  (previously always the first, the x86 arch module). Error messages suggest
  cargo dv verify --package <name>.
• README.md: documents --package, --target, and the experimental triples.

Behavior is unchanged for the default target: every command without the flags
builds and verifies exactly as before.

Compatibility

• --targets is replaced by --package. --target is a new flag; there is no
  released --rust-target interface. Callers must use --package and --target.
• --disasm still reads library_path(), which ignores the triple. The flag is
  currently unused (disassemble() has no caller), so this is not reachable.

Verification

• cargo test --lib --bin rust-dv: 11 + 6 passed. Four new tests cover the
  default target, rejection of an unsupported triple, cargo --target
  propagation, and count --module target selection. The count test was
  checked by mutation: disabling the cfg match makes it fail.
• rustfmt --check on the changed files: clean.
• Every README example parses with the built binary; the old --targets is
  rejected.
• rust-dv count --module arch::irq --target <triple> on the real ostd tree
  resolves x86, riscv, and loongarch to their own irq.rs.

Known test issues, both present on the base commit and unrelated to this PR:

• cargo test --test helper_tests: test_get_dependency fails with
  No targets found (it runs from the dv directory, which has no vostd
  workspace). Not fixed here.
• test_new_package writes verification/test-package and inserts a
  workspace = ... line at the top of dv/Cargo.toml. Run it only in a clean
  checkout, or revert those two changes afterwards.

Related issues: none.

[Marsman1996]

And for count and doc command, we may need to add the corresponding commands suggestion in the error message.

Also the README needs update

[Marsman1996]

@rikosellic
I'm now wondering why we use --target(s) for package in dv,
maybe we shall use --package/-p for package, and --target for arch?

[rikosellic]

@rikosellic I'm now wondering why we use --target(s) for package in dv, maybe we shall use --package/-p for package, and --target for arch?

This follows the legacy design by @chrihop, in dv we use VerusTarget to distinguish the packages internally, so we use the name --targets. Since this is now conflicting with the arch, I endorse using --package instead.

[Marsman1996]

@DID-Lab-SZU
Then we shall refactor dv, use --package/-p for package, and --target for arch
to match with cargo-verus

[rikosellic]

Sounds good to me.

[Marsman1996]

LGTM, and I will open a sync PR in VOSTD later

[rikosellic]

Please post this on Zulip so others can know about the command change. We may also need to change our CI.