Add ASN.1 primitives to `vest-examples`#38

Open

zhengyao-lin wants to merge 9 commits intosecure-foundations:mainfrom

zhengyao-lin:asn1

Commits on Jan 27, 2026

Start migrating verdict asn.1

y1ca1
authored and
zhengyao-lin
committed
Rename `builtin_macros` to `verus::prelude`

y1ca1
authored and
zhengyao-lin
committed
Migration step1: adapt to vest's new trait interfaces

y1ca1
authored and
zhengyao-lin
committed
Migration step2: make rustc happy

y1ca1
authored and
zhengyao-lin
committed
Migration step3: make verus happy modulo `external_body`

y1ca1
authored and
zhengyao-lin
committed
Migration step4: fix all proofs

y1ca1
authored and
zhengyao-lin
committed
Migrate to the latest vest
zhengyao-lin
committed
Merge verdict-polyfill into verdict-parser and remove unnecessary wrappers
zhengyao-lin
committed
Move asn1 to verdict-examples
zhengyao-lin
committed