Upgrade verus to latest version (Drop verification time to 3min)#24

Merged

ziqiaozhou merged 191 commits into

mainfrom

enable-build-verus-source

Jun 8, 2026

Commits on Jun 3, 2026

Update Verus toolchain to 2026-05-24 and patch HACL for clang 20

ziqiaozhou
and
Copilot
committed
Make verismo compile with verus 2026-05-24 toolchain
Copilot
committed
Fix all in-code Verus deprecation warnings

ziqiaozhou
and
Copilot
committed

Commits on Jun 4, 2026

Commits on Jun 5, 2026

ci: use cargo verus focus for verification

Copilot
and
Copilot
committed
fmt: run verusfmt across source

Copilot
and
Copilot
committed
rlimit: drop redundant rlimit(1) annotations

Copilot
and
Copilot
committed
sectype: add broadcast axiom_uop_new_constant for cast-of-constant
Copilot
committed
sectype_test: drop redundant use_type_invariant; tighten trigger
Copilot
committed
install_verus: install verusfmt for prebuilt path too
Copilot
committed
triggers: add explicit triggers across allocator/linkedlist/debug
Copilot
committed
triggers: add explicit triggers in addr_e/pgtable_e
Copilot
committed
triggers: add explicit triggers across snp/security/ptr
Copilot
committed
triggers: add explicit triggers across boot/*
Copilot
committed
broadcast: add per-module groups + verismo umbrella

Copilot
and
Copilot
committed
broadcast: use _ type args in groups to silence hide/reveal warning

Copilot
and
Copilot
committed
triggers: add explicit triggers in mem/rawmem_p{,2}.rs
Copilot
committed
boot: remove stale-broadcast assume() cheats

Copilot
and
Copilot
committed
pgtable_e: remove stale-broadcast assume() cheats

Copilot
and
Copilot
committed
addr_e: remove stale-broadcast assume() cheats

Copilot
and
Copilot
committed
arch: remove stale-broadcast assume() cheats

Copilot
and
Copilot
committed
debug: remove stale-broadcast assume() cheats

Copilot
and
Copilot
committed
Merge rm-assumes/boot into enable-build-verus-source
Copilot
committed
Merge rm-assumes/pgtable into enable-build-verus-source
Copilot
committed
Merge rm-assumes/addr into enable-build-verus-source
Copilot
committed
Merge rm-assumes/arch into enable-build-verus-source
Copilot
committed
Merge rm-assumes/debug into enable-build-verus-source
Copilot
committed
Merge triggers/rest into enable-build-verus-source
Copilot
committed
Merge triggers/mem into enable-build-verus-source
Copilot
committed
Merge triggers/boot into enable-build-verus-source
Copilot
committed
Merge triggers/addr into enable-build-verus-source
Copilot
committed
Merge triggers/snp-security into enable-build-verus-source
Copilot
committed
snp: remove stale-broadcast assume() cheats

Copilot
and
Copilot
committed
Merge rm-assumes/snp into enable-build-verus-source
Copilot
committed
param_e: drop obsolete verus-bug assume

Copilot
and
Copilot
committed
monitor: drop obsolete assume(wf_registered) in handle_register

Copilot
and
Copilot
committed
addr_s/page: delete unused axiom_addr_type_dummy_holder

Copilot
and
Copilot
committed
fmt: cargo fmt sweep across source

Copilot
and
Copilot
committed
ghcb_print: probe print_ensures_cs conjuncts

Copilot
and
Copilot
committed
Revert "ghcb_print: probe print_ensures_cs conjuncts"
Copilot
committed
boot/snp/misc: drop redundant proof blocks superseded by broadcast group

Copilot
and
Copilot
committed
tspec: drop redundant proof blocks superseded by broadcast group

Copilot
and
Copilot
committed
ghcb_print: drop redundant proof blocks superseded by broadcast group

Copilot
and
Copilot
committed
addr/arch: drop redundant proof blocks superseded by broadcast group

Copilot
and
Copilot
committed
tspec/math: drop redundant proof blocks superseded by broadcast group

Copilot
and
Copilot
committed
Merge cleanup-misc: drop redundant proof blocks
Copilot
committed
Merge cleanup-tspec-rest: drop redundant proof blocks
Copilot
committed
Merge cleanup-debug: drop redundant proof blocks
Copilot
committed
Merge cleanup-addr-arch: drop redundant proof blocks
Copilot
committed
Merge cleanup-tspec-math: drop redundant proof blocks
Copilot
committed
verusfmt
Copilot
committed
workflow: verify all crates
Copilot
committed
fmt: cargo fmt pass before reconciling with verusfmt

Copilot
and
Copilot
committed
fmt: reconcile cargo fmt with verusfmt outputs

Copilot
and
Copilot
committed

Commits on Jun 6, 2026

remove code that is commented out but causes inconsistant verusfmt and verusfmt
Copilot
committed
ci: Do not fmt before cargo build since cargo verus will generate some .rs code
Copilot
committed
update verusfmt to 0.7.1
Copilot
committed
sectype: remove VNot workaround assume and addr_interface unused $ptype

Copilot
and
Copilot
committed
verismo_macro/bits: remove unnecessary assume in generated empty()

Copilot
and
Copilot
committed
verismo_macro/print: remove unnecessary assume in derived early_print2

Copilot
and
Copilot
committed
subseq: delete dead proof_remove_keep with admit()

Copilot
and
Copilot
committed
ghcb_print: replace assume with axiom_global_auto broadcast

Copilot
and
Copilot
committed

Commits on Jun 7, 2026

idt/dummy: drop stale comments and unnecessary let-ret rewrite

Copilot
and
Copilot
committed
README: document tools/install_verus and renumber sections

Copilot
and
Copilot
committed
addr_e: drop unnecessary let-ret rewrites and stale comments

Copilot
and
Copilot
committed
debug, mshyper: drop unnecessary let-ret/proof scaffolding

Copilot
and
Copilot
committed
page, db_p: drop verbose 'Required:' broadcast-use comments

Copilot
and
Copilot
committed
sectype: remove session-internal checkpoint references in comments

Copilot
and
Copilot
committed
Revert unnecessary lock-handle let-bindings in pte.rs and bsp.rs

Copilot
and
Copilot
committed
Drop unused ghost vars and stale lock-handle bindings in pte/lock/init

Copilot
and
Copilot
committed

Commits on Jun 8, 2026

range_interface: drop redundant proof-doc comments

Copilot
and
Copilot
committed
Drop // Justification: proof-doc comments

Copilot
and
Copilot
committed
revert target.json
Copilot
committed
update Makefile to use cargo verus
Copilot
committed
Add trace and time in CI
Copilot
committed
drop my branch in Cargo.toml
Copilot
committed