From 8a7e7ebe5b20e579cfd4daa32556cb460ff7f66d Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Tue, 15 Oct 2024 19:39:43 -0700 Subject: [PATCH 1/8] Verify setup (#1) Add verus tool setup scripts + CI + dependencies + import some proofs from verismo Signed-off-by: Ziqiao Zhou --- .cargo/config.toml | 4 + .github/workflows/rust.yml | 2 +- .github/workflows/signed-off.yml | 4 +- .github/workflows/verify.yml | 53 +++ Cargo.lock | 390 +++++++++++++------ Cargo.toml | 13 + Documentation/docs/developer/VERIFICATION.md | 57 +++ kernel/Cargo.toml | 13 +- kernel/build.rs | 42 +- kernel/src/address.rs | 44 +++ kernel/src/address.verus.rs | 210 ++++++++++ kernel/src/lib.rs | 2 + kernel/src/mm/page_visibility.rs | 8 +- kernel/src/svsm.rs | 2 +- scripts/vfmt.sh | 13 + scripts/vinstall.sh | 12 + scripts/vpath.sh | 4 + verismo/Cargo.toml | 21 + verismo/build.rs | 26 ++ verismo/src/bits.rs | 8 + verismo/src/bits.verus.rs | 221 +++++++++++ verismo/src/layout.rs | 8 + verismo/src/layout.verus.rs | 12 + verismo/src/lib.rs | 12 + 24 files changed, 1048 insertions(+), 133 deletions(-) create mode 100644 .github/workflows/verify.yml create mode 100644 Documentation/docs/developer/VERIFICATION.md create mode 100644 kernel/src/address.verus.rs create mode 100755 scripts/vfmt.sh create mode 100755 scripts/vinstall.sh create mode 100755 scripts/vpath.sh create mode 100644 verismo/Cargo.toml create mode 100644 verismo/build.rs create mode 100644 verismo/src/bits.rs create mode 100644 verismo/src/bits.verus.rs create mode 100644 verismo/src/layout.rs create mode 100644 verismo/src/layout.verus.rs create mode 100644 verismo/src/lib.rs diff --git a/.cargo/config.toml b/.cargo/config.toml index 0777ed2ed..35342d8f2 100644 --- a/.cargo/config.toml +++ b/.cargo/config.toml @@ -11,3 +11,7 @@ rustflags = [ rustflags = [ "-C", "code-model=kernel", ] + +[alias] +vfmt = "run-script vfmt" # Format verus codes +verify = "v build --features verus" diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 668670ada..6d0c786fa 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -4,7 +4,7 @@ on: push: branches: [ "main" ] pull_request: - branches: [ "main" ] + branches: [ "main", "verify" ] env: CARGO_TERM_COLOR: always diff --git a/.github/workflows/signed-off.yml b/.github/workflows/signed-off.yml index f49c02fd6..3c0a2cfab 100644 --- a/.github/workflows/signed-off.yml +++ b/.github/workflows/signed-off.yml @@ -1,6 +1,8 @@ name: SignedOff -on: [pull_request] +on: + pull_request: + branches: [ "main" ] jobs: check: diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml new file mode 100644 index 000000000..94e54647f --- /dev/null +++ b/.github/workflows/verify.yml @@ -0,0 +1,53 @@ +name: Verification + +on: + push: + branches: [ "verify" ] + pull_request: + branches: [ "verify" ] + +env: + CARGO_TERM_COLOR: always + +jobs: + check: + name: Verification Check + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v3 + + - name: fetch verus via metadata + run: | + source ./scripts/vpath.sh + echo "VERUS_PATH=$(echo $VERUS_PATH)" >> $GITHUB_ENV + + - uses: Swatinem/rust-cache@v2 + with: + cache-directories: ${{ env.VERUS_PATH }}/source/target-verus + workspaces: | + ${{ github.workspace }} -> target + ${{ env.VERUS_PATH }}/source -> target + ${{ env.VERUS_PATH }}/tools/vargo -> target + + - name: Install specified rust toolchain + uses: actions-rs/toolchain@v1 + with: + toolchain: nightly-2023-12-22 + target: x86_64-unknown-none + profile: minimal + + - name: Install verus toolchains + run: ./scripts/vinstall.sh + + - name: Build with verus + run: cargo verify + working-directory: kernel + + - name: Build without verifying + run: cargo build + working-directory: kernel + + - name: Format rust code + run: verusfmt --check `find ./ -name *.verus.rs` + diff --git a/Cargo.lock b/Cargo.lock index dd58cad3d..3879b805b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -39,9 +39,9 @@ dependencies = [ [[package]] name = "anstream" -version = "0.6.14" +version = "0.6.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "418c75fa768af9c03be99d17643f93f79bbba589895012a80e3452a19ddda15b" +checksum = "64e15c1ab1f89faffbf04a634d5e1962e9074f2741eef6d97f3c4e322426d526" dependencies = [ "anstyle", "anstyle-parse", @@ -54,33 +54,33 @@ dependencies = [ [[package]] name = "anstyle" -version = "1.0.7" +version = "1.0.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "038dfcf04a5feb68e9c60b21c9625a54c2c0616e79b72b0fd87075a056ae1d1b" +checksum = "1bec1de6f59aedf83baf9ff929c98f2ad654b97c9510f4e70cf6f661d49fd5b1" [[package]] name = "anstyle-parse" -version = "0.2.4" +version = "0.2.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c03a11a9034d92058ceb6ee011ce58af4a9bf61491aa7e1e59ecd24bd40d22d4" +checksum = "eb47de1e80c2b463c735db5b217a0ddc39d612e7ac9e2e96a5aed1f57616c1cb" dependencies = [ "utf8parse", ] [[package]] name = "anstyle-query" -version = "1.1.0" +version = "1.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ad186efb764318d35165f1758e7dcef3b10628e26d41a44bc5550652e6804391" +checksum = "6d36fc52c7f6c869915e99412912f22093507da8d9e942ceaf66fe4b7c14422a" dependencies = [ "windows-sys", ] [[package]] name = "anstyle-wincon" -version = "3.0.3" +version = "3.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "61a38449feb7068f52bb06c12759005cf459ee52bb4adc1d5a7c4322d716fb19" +checksum = "5bf74e1b6e971609db8ca7a9ce79fd5768ab6ae46441c572e46cf596f59e57f8" dependencies = [ "anstyle", "windows-sys", @@ -97,9 +97,9 @@ dependencies = [ [[package]] name = "autocfg" -version = "1.3.0" +version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0c4b4d0bd25bd0b74681c0ad21497610ce1b7c91b1022cd21c80c6fbdd9476b0" +checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" [[package]] name = "base16ct" @@ -127,7 +127,18 @@ checksum = "adc0846593a56638b74e136a45610f9934c052e14761bebca6b092d5522599e3" dependencies = [ "proc-macro2", "quote", - "syn 2.0.66", + "syn 2.0.82", +] + +[[package]] +name = "bitfield-struct" +version = "0.7.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6c2ce686adbebce0ee484a502c440b4657739adbad65eadf06d64f5816ee9765" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.82", ] [[package]] @@ -138,9 +149,9 @@ checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" [[package]] name = "bitflags" -version = "2.5.0" +version = "2.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cf4b9d6a944f767f8e5e0db018570623c85f3d925ac718db4e06d0187adb21c1" +checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" [[package]] name = "block-buffer" @@ -155,7 +166,25 @@ dependencies = [ name = "bootlib" version = "0.1.0" dependencies = [ - "zerocopy 0.8.2", + "zerocopy 0.8.7", +] + +[[package]] +name = "builtin" +version = "0.1.0" +source = "git+https://github.com/verus-lang/verus?rev=0ee96be2#0ee96be22afe96fc15a228db7eaba8350e9bcbf8" + +[[package]] +name = "builtin_macros" +version = "0.1.0" +source = "git+https://github.com/verus-lang/verus?rev=0ee96be2#0ee96be22afe96fc15a228db7eaba8350e9bcbf8" +dependencies = [ + "prettyplease_verus", + "proc-macro2", + "quote", + "syn 1.0.109", + "syn_verus", + "synstructure", ] [[package]] @@ -166,13 +195,13 @@ checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b" [[package]] name = "cc" -version = "1.0.98" +version = "1.1.31" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "41c270e7540d725e65ac7f1b212ac8ce349719624d7bcff99f8e2e488e8cf03f" +checksum = "c2e7962b54006dcfcc61cb72735f4d89bb97061dd6a7ed882ec6b8ee53714c6f" dependencies = [ "jobserver", "libc", - "once_cell", + "shlex", ] [[package]] @@ -193,9 +222,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.5.4" +version = "4.5.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "90bc066a67923782aa8515dbaea16946c5bcc5addbd668bb80af688e53e548a0" +checksum = "b97f376d85a664d5837dbae44bf546e6477a679ff6610010f17276f686d867e8" dependencies = [ "clap_builder", "clap_derive", @@ -203,9 +232,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.2" +version = "4.5.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ae129e2e766ae0ec03484e609954119f123cc1fe650337e155d03b022f24f7b4" +checksum = "19bc80abd44e4bed93ca373a0704ccbd1b710dc5749406201bb018272808dc54" dependencies = [ "anstream", "anstyle", @@ -215,27 +244,27 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.5.4" +version = "4.5.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "528131438037fd55894f62d6e9f068b8f45ac57ffa77517819645d10aed04f64" +checksum = "4ac6a0c7b1a9e9a5186361f67dfa1b88213572f427fb9ab038efb2bd8c582dab" dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.66", + "syn 2.0.82", ] [[package]] name = "clap_lex" -version = "0.7.0" +version = "0.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "98cc8fbded0c607b7ba9dd60cd98df59af97e84d24e49c8557331cfc26d301ce" +checksum = "1462739cb27611015575c0c11df5df7601141071f07518d56fcc1be504cbec97" [[package]] name = "colorchoice" -version = "1.0.1" +version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b6a852b24ab71dffc585bcb46eaf7959d175cb865a7152e35b348d1b2960422" +checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0" [[package]] name = "const-oid" @@ -247,15 +276,15 @@ checksum = "c2459377285ad874054d797f3ccebf984978aa39129f6eafde5cdc8315b612f8" name = "cpuarch" version = "0.1.0" dependencies = [ - "bitfield-struct", - "zerocopy 0.8.2", + "bitfield-struct 0.6.2", + "zerocopy 0.8.7", ] [[package]] name = "cpufeatures" -version = "0.2.12" +version = "0.2.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "53fe5e26ff1b7aef8bca9c6080520cfb8d9333c7568e1829cef191a9723e5504" +checksum = "608697df725056feaccfa42cffdaeeec3fccc4ffc38358ecd19b243e716a78e0" dependencies = [ "libc", ] @@ -319,7 +348,7 @@ checksum = "67e77553c4162a157adbf834ebae5b415acbecbeafc7a74b0e886657506a7611" dependencies = [ "proc-macro2", "quote", - "syn 2.0.66", + "syn 2.0.82", ] [[package]] @@ -352,7 +381,7 @@ dependencies = [ name = "elf" version = "0.1.0" dependencies = [ - "bitflags 2.5.0", + "bitflags 2.6.0", ] [[package]] @@ -453,6 +482,12 @@ dependencies = [ "subtle", ] +[[package]] +name = "hashbrown" +version = "0.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" + [[package]] name = "heck" version = "0.5.0" @@ -485,11 +520,11 @@ dependencies = [ [[package]] name = "igvm" -version = "0.3.2" +version = "0.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7dea806ed3176461d48d0bba25d7945621311ce73b0a89d98db4f5860a64c499" +checksum = "7984b10433b50e06a06bd50c69bca4888a5d7de8975f64ea4c2a7687eb99b09d" dependencies = [ - "bitfield-struct", + "bitfield-struct 0.7.0", "crc32fast", "hex", "igvm_defs", @@ -497,19 +532,19 @@ dependencies = [ "range_map_vec", "thiserror", "tracing", - "zerocopy 0.7.34", + "zerocopy 0.7.35", ] [[package]] name = "igvm_defs" -version = "0.3.2" +version = "0.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "35e19348da04f61332a5c2c845933b8d071cba2105c86f6b7295456e711941a0" +checksum = "b64ec5588c475372ae830475d3ee9a7bd255407dcb9f03faf6d493556eb6105a" dependencies = [ - "bitfield-struct", + "bitfield-struct 0.7.0", "open-enum", "static_assertions", - "zerocopy 0.7.34", + "zerocopy 0.7.35", ] [[package]] @@ -521,8 +556,8 @@ dependencies = [ "igvm", "igvm_defs", "uuid", - "zerocopy 0.7.34", - "zerocopy 0.8.2", + "zerocopy 0.7.35", + "zerocopy 0.8.7", ] [[package]] @@ -534,8 +569,18 @@ dependencies = [ "igvm_defs", "p384", "sha2", - "zerocopy 0.7.34", - "zerocopy 0.8.2", + "zerocopy 0.7.35", + "zerocopy 0.8.7", +] + +[[package]] +name = "indexmap" +version = "1.9.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99" +dependencies = [ + "autocfg", + "hashbrown", ] [[package]] @@ -549,24 +594,24 @@ dependencies = [ [[package]] name = "intrusive-collections" -version = "0.9.6" +version = "0.9.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b694dc9f70c3bda874626d2aed13b780f137aab435f4e9814121955cf706122e" +checksum = "189d0897e4cbe8c75efedf3502c18c887b05046e59d28404d4d8e46cbc4d1e86" dependencies = [ "memoffset", ] [[package]] name = "is_terminal_polyfill" -version = "1.70.0" +version = "1.70.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f8478577c03552c21db0e2724ffb8986a5ce7af88107e6be5d2ee6e158c12800" +checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf" [[package]] name = "jobserver" -version = "0.1.31" +version = "0.1.32" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d2b099aaa34a9751c5bf0878add70444e1ed2dd73f347be99003d4577277de6e" +checksum = "48d1dbcbbeb6a7fec7e059840aa538bd62aaccf972c7346c4d9d2059312853d0" dependencies = [ "libc", ] @@ -582,9 +627,9 @@ dependencies = [ [[package]] name = "libc" -version = "0.2.155" +version = "0.2.161" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "97b3888a4aecf77e811145cadf6eef5901f4782c53886191b2f693f24761847c" +checksum = "8e9489c2807c139ffd9c1794f4af0ebe86a828db53ecdc7fea2111d0fed085d1" [[package]] name = "libfuzzer-sys" @@ -613,9 +658,9 @@ dependencies = [ [[package]] name = "log" -version = "0.4.21" +version = "0.4.22" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "90ed8c1e510134f979dbc4f070f87d4313098b704861a105fe34231c70a3901c" +checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24" [[package]] name = "managed" @@ -643,9 +688,9 @@ dependencies = [ [[package]] name = "once_cell" -version = "1.19.0" +version = "1.20.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92" +checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775" [[package]] name = "opaque-debug" @@ -655,22 +700,22 @@ checksum = "c08d65885ee38876c4f86fa503fb49d7b507c2b62552df7c70b2fce627e06381" [[package]] name = "open-enum" -version = "0.5.1" +version = "0.5.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0e88e2e4e7b332f23a96ece6261bae7cc7446b8a38439c0bae6fce02168cf16f" +checksum = "2eb2508143a400b3361812094d987dd5adc81f0f5294a46491be648d6c94cab5" dependencies = [ "open-enum-derive", ] [[package]] name = "open-enum-derive" -version = "0.5.1" +version = "0.5.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2f51a157e01c7343a7c31f540309b3b8b2c9751f3adb6d040373e3139aa2e2e0" +checksum = "8d1296fab5231654a5aec8bf9e87ba4e3938c502fc4c3c0425a00084c78944be" dependencies = [ "proc-macro2", "quote", - "syn 2.0.66", + "syn 2.0.82", ] [[package]] @@ -690,7 +735,7 @@ name = "packit" version = "0.1.1" source = "git+https://github.com/coconut-svsm/packit#e2508f686440f6a703fb6c5c0c2fd338e55f1d38" dependencies = [ - "zerocopy 0.7.34", + "zerocopy 0.7.35", ] [[package]] @@ -736,6 +781,15 @@ dependencies = [ "universal-hash", ] +[[package]] +name = "prettyplease_verus" +version = "0.1.15" +source = "git+https://github.com/verus-lang/verus?rev=0ee96be2#0ee96be22afe96fc15a228db7eaba8350e9bcbf8" +dependencies = [ + "proc-macro2", + "syn_verus", +] + [[package]] name = "primeorder" version = "0.13.6" @@ -747,18 +801,18 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.85" +version = "1.0.89" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "22244ce15aa966053a896d1accb3a6e68469b97c7f33f284b99f0d576879fc23" +checksum = "f139b0662de085916d1fb67d2b4169d1addddda1919e696f3252b740b629986e" dependencies = [ "unicode-ident", ] [[package]] name = "quote" -version = "1.0.36" +version = "1.0.37" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0fa76aaf39101c457836aec0ce2316dbdc3ab723cdda1c6bd4e6ad4208acaca7" +checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" dependencies = [ "proc-macro2", ] @@ -788,6 +842,15 @@ dependencies = [ "subtle", ] +[[package]] +name = "rustc_version" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92" +dependencies = [ + "semver", +] + [[package]] name = "rustversion" version = "1.0.18" @@ -834,6 +897,18 @@ dependencies = [ "zeroize", ] +[[package]] +name = "semver" +version = "1.0.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "61697e0a1c7e512e84a621326239844a24d8207b4669b41bc18b32ea5cbf988b" + +[[package]] +name = "seq-macro" +version = "0.3.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a3f0bf26fd526d2a95683cd0f87bf103b8539e2ca1ef48ce002d67aad59aa0b4" + [[package]] name = "sha2" version = "0.10.8" @@ -845,6 +920,12 @@ dependencies = [ "digest", ] +[[package]] +name = "shlex" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" + [[package]] name = "signature" version = "2.2.0" @@ -874,6 +955,17 @@ dependencies = [ "der", ] +[[package]] +name = "state_machines_macros" +version = "0.1.0" +source = "git+https://github.com/verus-lang/verus?rev=0ee96be2#0ee96be22afe96fc15a228db7eaba8350e9bcbf8" +dependencies = [ + "indexmap", + "proc-macro2", + "quote", + "syn_verus", +] + [[package]] name = "static_assertions" version = "1.1.0" @@ -888,18 +980,20 @@ checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" [[package]] name = "subtle" -version = "2.5.0" +version = "2.6.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "81cdd64d312baedb58e21336b31bc043b77e01cc99033ce76ef539f78e965ebc" +checksum = "13c2bddecc57b384dee18652358fb23172facb8a2c51ccc10d74c157bdea3292" [[package]] name = "svsm" version = "0.1.0" dependencies = [ "aes-gcm", - "bitfield-struct", - "bitflags 2.5.0", + "bitfield-struct 0.6.2", + "bitflags 2.6.0", "bootlib", + "builtin", + "builtin_macros", "cpuarch", "elf", "gdbstub", @@ -909,10 +1003,13 @@ dependencies = [ "libmstpm", "log", "packit", + "rustc_version", "syscall", "tdx-tdcall", "test", - "zerocopy 0.8.2", + "verismo", + "vstd", + "zerocopy 0.8.7", ] [[package]] @@ -937,15 +1034,37 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.66" +version = "2.0.82" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c42f3f41a2de00b01c0aaad383c5a45241efc8b2d1eda5661812fda5f3cdcff5" +checksum = "83540f837a8afc019423a8edb95b52a8effe46957ee402287f4292fae35be021" dependencies = [ "proc-macro2", "quote", "unicode-ident", ] +[[package]] +name = "syn_verus" +version = "1.0.95" +source = "git+https://github.com/verus-lang/verus?rev=0ee96be2#0ee96be22afe96fc15a228db7eaba8350e9bcbf8" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "synstructure" +version = "0.12.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f36bdaa60a83aca3921b5259d5400cbf5e90fc51931376a9bd4a0eb79aa7210f" +dependencies = [ + "proc-macro2", + "quote", + "syn 1.0.109", + "unicode-xid", +] + [[package]] name = "syscall" version = "0.1.0" @@ -969,22 +1088,22 @@ version = "0.1.0" [[package]] name = "thiserror" -version = "1.0.61" +version = "1.0.65" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c546c80d6be4bc6a00c0f01730c08df82eaa7a7a61f11d656526506112cc1709" +checksum = "5d11abd9594d9b38965ef50805c5e469ca9cc6f197f883f717e0269a3057b3d5" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.61" +version = "1.0.65" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "46c3384250002a6d5af4d114f2845d37b57521033f30d5c3f46c4d70e1197533" +checksum = "ae71770322cbd277e69d762a16c444af02aa0575ac0d174f0b9562d3b37f8602" dependencies = [ "proc-macro2", "quote", - "syn 2.0.66", + "syn 2.0.82", ] [[package]] @@ -1006,7 +1125,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.66", + "syn 2.0.82", ] [[package]] @@ -1026,9 +1145,15 @@ checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825" [[package]] name = "unicode-ident" -version = "1.0.12" +version = "1.0.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" + +[[package]] +name = "unicode-xid" +version = "0.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" +checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853" [[package]] name = "universal-hash" @@ -1042,21 +1167,32 @@ dependencies = [ [[package]] name = "utf8parse" -version = "0.2.1" +version = "0.2.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a" +checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821" [[package]] name = "uuid" -version = "1.8.0" +version = "1.11.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a183cf7feeba97b4dd1c0d46788634f6221d87fa961b305bed08c851829efcc0" +checksum = "f8c5f0a0af699448548ad1a2fbf920fb4bee257eae39953ba95cb84891a0446a" + +[[package]] +name = "verismo" +version = "0.1.0" +dependencies = [ + "builtin", + "builtin_macros", + "paste", + "seq-macro", + "vstd", +] [[package]] name = "version_check" -version = "0.9.4" +version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" +checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" [[package]] name = "volatile" @@ -1064,6 +1200,16 @@ version = "0.4.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "442887c63f2c839b346c192d047a7c87e73d0689c9157b00b53dcc27dd5ea793" +[[package]] +name = "vstd" +version = "0.1.0" +source = "git+https://github.com/verus-lang/verus?rev=0ee96be2#0ee96be22afe96fc15a228db7eaba8350e9bcbf8" +dependencies = [ + "builtin", + "builtin_macros", + "state_machines_macros", +] + [[package]] name = "wasi" version = "0.11.0+wasi-snapshot-preview1" @@ -1081,9 +1227,9 @@ dependencies = [ [[package]] name = "windows-targets" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6f0713a46559409d202e70e28227288446bf7841d3211583a4b53e3f6d96e7eb" +checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" dependencies = [ "windows_aarch64_gnullvm", "windows_aarch64_msvc", @@ -1097,51 +1243,51 @@ dependencies = [ [[package]] name = "windows_aarch64_gnullvm" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7088eed71e8b8dda258ecc8bac5fb1153c5cffaf2578fc8ff5d61e23578d3263" +checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" [[package]] name = "windows_aarch64_msvc" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9985fd1504e250c615ca5f281c3f7a6da76213ebd5ccc9561496568a2752afb6" +checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" [[package]] name = "windows_i686_gnu" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "88ba073cf16d5372720ec942a8ccbf61626074c6d4dd2e745299726ce8b89670" +checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" [[package]] name = "windows_i686_gnullvm" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "87f4261229030a858f36b459e748ae97545d6f1ec60e5e0d6a3d32e0dc232ee9" +checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" [[package]] name = "windows_i686_msvc" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "db3c2bf3d13d5b658be73463284eaf12830ac9a26a90c717b7f771dfe97487bf" +checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" [[package]] name = "windows_x86_64_gnu" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4e4246f76bdeff09eb48875a0fd3e2af6aada79d409d33011886d3e1581517d9" +checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" [[package]] name = "windows_x86_64_gnullvm" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "852298e482cd67c356ddd9570386e2862b5673c85bd5f88df9ab6802b334c596" +checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" [[package]] name = "windows_x86_64_msvc" -version = "0.52.5" +version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bec47e5bfd1bff0eeaf6d8b485cc1074891a197ab4225d504cb7a1ab88b02bf0" +checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" [[package]] name = "x86_64" @@ -1150,50 +1296,50 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "96cb6fd45bfeab6a5055c5bffdb08768bd0c069f1d946debe585bbb380a7c062" dependencies = [ "bit_field", - "bitflags 2.5.0", + "bitflags 2.6.0", "rustversion", "volatile", ] [[package]] name = "zerocopy" -version = "0.7.34" +version = "0.7.35" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ae87e3fcd617500e5d106f0380cf7b77f3c6092aae37191433159dda23cfb087" +checksum = "1b9b4fd18abc82b8136838da5d50bae7bdea537c574d8dc1a34ed098d6c166f0" dependencies = [ "byteorder", - "zerocopy-derive 0.7.34", + "zerocopy-derive 0.7.35", ] [[package]] name = "zerocopy" -version = "0.8.2" +version = "0.8.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fdf8d0ac51277f0e70d6dcb000b7bfa817968d66df9f5772e731a1d1bc6fc5c6" +checksum = "bb3da5f7220f919a6c7af7c856435a68ee1582fd7a77aa72936257d8335bd6f6" dependencies = [ - "zerocopy-derive 0.8.2", + "zerocopy-derive 0.8.7", ] [[package]] name = "zerocopy-derive" -version = "0.7.34" +version = "0.7.35" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "15e934569e47891f7d9411f1a451d947a60e000ab3bd24fbb970f000387d1b3b" +checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.66", + "syn 2.0.82", ] [[package]] name = "zerocopy-derive" -version = "0.8.2" +version = "0.8.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2cf1fea9437ee18b719f41c597b00c1745d7ff77184daf6ac8c61110a0115161" +checksum = "2e5f54f3cc93cd80745404626681b4b9fca9a867bad5a8424b618eb0db1ae6ea" dependencies = [ "proc-macro2", "quote", - "syn 2.0.66", + "syn 2.0.82", ] [[package]] diff --git a/Cargo.toml b/Cargo.toml index 682019d5a..a7843c6c3 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -14,6 +14,8 @@ members = [ "libmstpm", # syscall interface definitions "syscall", + # verification library for svsm + "verismo", ] @@ -50,6 +52,14 @@ zerocopy = { version = "0.8.2", features = ["alloc", "derive"] } # other repos packit = { git = "https://github.com/coconut-svsm/packit", version = "0.1.1" } +# Verus repos +builtin = { git = "https://github.com/verus-lang/verus", rev ="0ee96be2", default-features = false } +builtin_macros = { git = "https://github.com/verus-lang/verus", rev ="0ee96be2", default-features = false } +vstd = { git = "https://github.com/verus-lang/verus", rev ="0ee96be2", features = ["alloc"], default-features = false } + +# Verification libs +verismo = { path = "verismo", default-features = false } + [workspace.lints.rust] future_incompatible = { level = "deny", priority = 127 } nonstandard_style = { level = "deny", priority = 126 } @@ -81,3 +91,6 @@ suboptimal_flops = "warn" # TODO: fires many times, fix then enable. # undocumented_unsafe_blocks = "warn" unnecessary_box_returns = "warn" + +[workspace.metadata.scripts] +vfmt = "verusfmt `find ./ -name *.verus.rs`" diff --git a/Documentation/docs/developer/VERIFICATION.md b/Documentation/docs/developer/VERIFICATION.md new file mode 100644 index 000000000..2805c5a10 --- /dev/null +++ b/Documentation/docs/developer/VERIFICATION.md @@ -0,0 +1,57 @@ +VERIFICATION +======= + +To run verification, we will need to a few steps to setup the build toolchains. + + +## Build + +### Install verification tools + +``` +cd svsm +./scripts/vinstall.sh +``` + +### Build svsm with verification + +``` +cd svsm/kernel +cargo verify +``` + +By default, it will verify all crates (except for vstd), if you do not want to +verify other crates, use `cargo verify --features verus_no_dep_verify`. + + +### Pass verus arguments for verification. + +It is helpful to pass extra args for verification debugging. + +You can pass extra verus arguments via {crate}_{lib/bin}_VERUS_ARGS to a specific crate +{crate} or VERUS_ARGS to all crates. + +`svsm_lib_VERUS_ARGS="--no-verify" cargo verify` compiles the code without verifying +svsm crate. + +`svsm_lib_VERUS_ARGS="--verify-module address" cargo verify` verify only address +module in the crate svsm. + + + +### Build without verification + +``` +cd svsm/kernel +cargo build +``` + +## Manage specification and proof codes + +* Minimize annotations inside executable Rust. +* Define specification and proof code in `*.verus.rs` or in a different crates. Those codes wrapped in verus!{} macro and need verusfmt to format. + +``` +cd svsm +cargo vfmt +``` diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml index ca650067e..3af6265dc 100644 --- a/kernel/Cargo.toml +++ b/kernel/Cargo.toml @@ -2,7 +2,7 @@ name = "svsm" version = "0.1.0" edition = "2021" -rust-version = "1.82.0" +rust-version = "1.77.0" [[bin]] name = "stage2" @@ -37,6 +37,11 @@ tdx-tdcall.workspace = true libmstpm = { workspace = true, optional = true } zerocopy.workspace = true +builtin = { workspace = true, optional = true } +builtin_macros = { workspace = true } +vstd = { workspace = true, optional = true } +verismo = { workspace = true, optional = true} + [target."x86_64-unknown-none".dev-dependencies] test.workspace = true @@ -46,8 +51,14 @@ enable-gdb = ["dep:gdbstub", "dep:gdbstub_arch"] mstpm = ["dep:libmstpm"] nosmep = [] nosmap = [] +verus_no_dep_verify = ["verus", "verismo/noverify"] +verus = ["vstd", "builtin", "verismo/verus"] +noverify = [] [dev-dependencies] +[build-dependencies] +rustc_version = "0.4" + [lints] workspace = true diff --git a/kernel/build.rs b/kernel/build.rs index 526b10203..cb7b7c3fd 100644 --- a/kernel/build.rs +++ b/kernel/build.rs @@ -4,10 +4,27 @@ // // Author: Joerg Roedel +use rustc_version::{Channel, Version}; + fn main() { - // Extra cfgs - println!("cargo::rustc-check-cfg=cfg(fuzzing)"); - println!("cargo::rustc-check-cfg=cfg(test_in_svsm)"); + let rust_version = rustc_version::version_meta().unwrap(); + // Check if the version is nightly and higher than 1.78.0 + let is_expected_version = rust_version.semver >= Version::new(1, 78, 0); + if !is_expected_version { + if rust_version.channel == Channel::Nightly { + // Print the cargo:rustc-cfg directive to enable the feature + println!("cargo:rustc-cfg=RUST_BEFORE_1_78"); + } else { + // Optionally handle the case for non-nightly versions + panic!("Requires the nightly version or stable version >= 1.78."); + } + } else { + // Extra cfgs + println!("cargo::rustc-check-cfg=cfg(fuzzing)"); + println!("cargo::rustc-check-cfg=cfg(test_in_svsm)"); + println!("cargo::rustc-check-cfg=cfg(verus_keep_ghost)"); + println!("cargo::rustc-check-cfg=cfg(RUST_BEFORE_1_78)"); + } // Stage 2 println!("cargo:rustc-link-arg-bin=stage2=-nostdlib"); @@ -35,4 +52,23 @@ fn main() { println!("cargo:rerun-if-changed=kernel/src/stage2.lds"); println!("cargo:rerun-if-changed=kernel/src/svsm.lds"); + println!("cargo:rerun-if-changed=build.rs"); + init_verify(); +} + +fn init_verify() { + if cfg!(feature = "noverify") { + println!("cargo:rustc-env=VERUS_ARGS=--no-verify"); + } else { + let verus_args = [ + "--rlimit=8000", + "--expand-errors", + "--multiple-errors=5", + "--triggers-silent", + "--no-auto-recommends-check", + "--trace", + "-Z unstable-options", + ]; + println!("cargo:rustc-env=VERUS_ARGS={}", verus_args.join(" ")); + } } diff --git a/kernel/src/address.rs b/kernel/src/address.rs index 9936d2950..eb268f68f 100644 --- a/kernel/src/address.rs +++ b/kernel/src/address.rs @@ -10,14 +10,22 @@ use core::ops; use core::slice; +use builtin_macros::*; + // The backing type to represent an address; type InnerAddr = usize; +#[verus_verify] const SIGN_BIT: usize = 47; +include!("address.verus.rs"); + #[inline] +#[verus_verify] +#[ensures(|ret: InnerAddr| [sign_extend_ensures(addr, ret)])] const fn sign_extend(addr: InnerAddr) -> InnerAddr { let mask = 1usize << SIGN_BIT; + if (addr & mask) == mask { addr | !((1usize << SIGN_BIT) - 1) } else { @@ -106,6 +114,7 @@ pub trait Address: #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord)] #[repr(transparent)] +#[verus_verify] pub struct PhysAddr(InnerAddr); impl PhysAddr { @@ -197,10 +206,13 @@ impl Address for PhysAddr {} #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord)] #[repr(transparent)] +#[verus_verify] pub struct VirtAddr(InnerAddr); +#[verus_verify] impl VirtAddr { #[inline] + #[verus_verify] pub const fn null() -> Self { Self(0) } @@ -208,6 +220,8 @@ impl VirtAddr { // const traits experimental, so for now we need this to make up // for the lack of VirtAddr::from() in const contexts. #[inline] + #[verus_verify] + #[ensures(|ret: VirtAddr| ret.new_ensures(addr))] pub const fn new(addr: InnerAddr) -> Self { Self(sign_extend(addr)) } @@ -255,6 +269,9 @@ impl VirtAddr { .flatten() } + #[verus_verify] + #[requires(self.const_add_requires(offset))] + #[ensures(|ret: VirtAddr| [self.const_add_ensures(offset, ret)])] pub const fn const_add(&self, offset: usize) -> Self { VirtAddr::new(self.0 + offset) } @@ -290,15 +307,21 @@ impl fmt::LowerHex for VirtAddr { } } +#[verus_verify] impl From for VirtAddr { #[inline] + #[verus_verify] + #[ensures(|ret: VirtAddr| ret.new_ensures(addr))] fn from(addr: InnerAddr) -> Self { Self(sign_extend(addr)) } } +#[verus_verify] impl From for InnerAddr { #[inline] + #[verus_verify] + #[ensures(|ret: InnerAddr| addr@ == ret)] fn from(addr: VirtAddr) -> Self { addr.0 } @@ -312,47 +335,68 @@ impl From for VirtAddr { } } +#[verus_verify] impl From for u64 { #[inline] + #[verus_verify] + #[ensures(|ret: Self| ret == addr@)] fn from(addr: VirtAddr) -> Self { addr.0 as u64 } } +#[verus_verify] impl From<*const T> for VirtAddr { #[inline] + #[verus_verify] + #[requires(vaddr_is_valid(ptr as usize))] fn from(ptr: *const T) -> Self { Self(ptr as InnerAddr) } } +#[verus_verify] impl From<*mut T> for VirtAddr { + #[verus_verify] + #[requires(vaddr_is_valid(ptr as usize))] fn from(ptr: *mut T) -> Self { Self(ptr as InnerAddr) } } +#[verus_verify] impl ops::Sub for VirtAddr { type Output = InnerAddr; #[inline] + #[verus_verify] + #[requires(self.sub_requires(other))] + #[ensures(|ret: InnerAddr| self.sub_ensures(other, ret))] fn sub(self, other: VirtAddr) -> Self::Output { sign_extend(self.0 - other.0) } } +#[verus_verify] impl ops::Sub for VirtAddr { type Output = Self; #[inline] + #[verus_verify] + #[requires(self.sub_usize_requires(other))] + #[ensures(|ret: Self| self.sub_usize_ensures(other, ret))] fn sub(self, other: usize) -> Self { VirtAddr::from(self.0 - other) } } +#[verus_verify] impl ops::Add for VirtAddr { type Output = VirtAddr; + #[verus_verify] + #[requires(self.const_add_requires(other))] + #[ensures(|ret: VirtAddr| [self.const_add_ensures(other, ret)])] fn add(self, other: InnerAddr) -> Self { VirtAddr::from(self.0 + other) } diff --git a/kernel/src/address.verus.rs b/kernel/src/address.verus.rs new file mode 100644 index 000000000..3c1ea382b --- /dev/null +++ b/kernel/src/address.verus.rs @@ -0,0 +1,210 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou +verus! { + +#[cfg(verus_keep_ghost)] +use vstd::prelude::*; + +pub broadcast group sign_extend_proof { + verismo::bits::lemma_bit_usize_not_is_sub, + verismo::bits::lemma_bit_usize_shl_values, + verismo::bits::lemma_bit_usize_or_mask, + verismo::bits::lemma_bit_usize_and_mask, +} + +broadcast group vaddr_properties { + sign_extend_proof, + lemma_inner_addr_as_vaddr, +} + +broadcast use vaddr_properties; +/// Define a broadcast function and its related spec function calls in a inner +/// module to avoid cyclic self-reference + +#[cfg(verus_keep_ghost)] +mod address_spec { + use super::*; + + #[verifier(inline)] + pub spec const VADDR_LOWER_MASK: InnerAddr = 0x7FFF_FFFF_FFFF as InnerAddr; + + #[verifier(inline)] + pub spec const VADDR_UPPER_MASK: InnerAddr = !VADDR_LOWER_MASK; + + #[verifier(inline)] + pub open spec fn check_signed(addr: InnerAddr) -> bool { + addr & (1usize << 47) == 1usize << 47 + } + + #[verifier(inline)] + pub open spec fn vaddr_lower_bits(addr: InnerAddr) -> InnerAddr { + addr & VADDR_LOWER_MASK + } + + #[verifier(inline)] + pub open spec fn vaddr_upper_bits(addr: InnerAddr) -> InnerAddr { + addr & VADDR_UPPER_MASK + } + + #[verifier(inline)] + pub open spec fn vaddr_is_signed(addr: InnerAddr) -> bool { + addr & VADDR_UPPER_MASK == VADDR_UPPER_MASK + } + + #[verifier(inline)] + pub open spec fn vaddr_is_valid(addr: InnerAddr) -> bool { + addr & VADDR_UPPER_MASK == 0 + } + + pub broadcast proof fn lemma_inner_addr_as_vaddr(bits: InnerAddr) + ensures + vaddr_is_signed(bits) == (bits >= VADDR_UPPER_MASK), + vaddr_is_valid(bits) == (bits <= VADDR_LOWER_MASK), + vaddr_is_valid(bits) ==> #[trigger] vaddr_lower_bits(bits) == bits, + vaddr_is_signed(bits) ==> vaddr_upper_bits(bits) + vaddr_lower_bits(bits) == bits, + VADDR_UPPER_MASK > VADDR_LOWER_MASK, + vaddr_is_signed(bits) ==> check_signed(bits), + { + broadcast use sign_extend_proof; + + assert(vaddr_is_signed(bits) == (bits >= VADDR_UPPER_MASK)) by (bit_vector); + assert(vaddr_is_signed(bits) ==> check_signed(bits)) by (bit_vector); + assert(vaddr_is_valid(bits) == (bits <= VADDR_LOWER_MASK)) by (bit_vector); + } + +} + +#[cfg(verus_keep_ghost)] +use address_spec::*; + +#[verifier(inline)] +pub open spec fn sign_extend_spec(addr: InnerAddr) -> InnerAddr { + if check_signed(addr) { + (vaddr_lower_bits(addr) + VADDR_UPPER_MASK) as InnerAddr + } else { + vaddr_lower_bits(addr) + } +} + +/// Ensures that ret is a new canonical address, throwing out bits 48..64. +#[verifier(inline)] +pub open spec fn sign_extend_ensures(addr: InnerAddr, ret: InnerAddr) -> bool { + &&& ret == sign_extend_spec(addr) + &&& vaddr_lower_bits(ret) == vaddr_lower_bits(addr) + &&& check_signed(addr) ==> vaddr_is_signed(ret) + &&& !check_signed(addr) ==> vaddr_is_valid(ret) +} + +// Define a view (@) for VirtAddr +#[cfg(verus_keep_ghost)] +impl View for VirtAddr { + type V = InnerAddr; + + closed spec fn view(&self) -> InnerAddr { + self.0 + } +} + +impl VirtAddr { + /// A valid virtual address have a canonical form where the upper bits + /// are either all zeroes or all ones + #[verifier::type_invariant] + pub closed spec fn is_canonical_vaddr(&self) -> bool { + vaddr_is_valid(self@) || vaddr_is_signed(self@) + } + + pub closed spec fn lower_bits(&self) -> InnerAddr { + vaddr_lower_bits(self@) + } + + pub closed spec fn valid_access(&self) -> bool { + vaddr_is_valid(self@) + } + + pub open spec fn new_ensures(self, addr: InnerAddr) -> bool { + sign_extend_ensures(addr, self@) + } + + /* Specifications for methods */ + // requires that adding offset will not cause not overflow. + // If the address is valid, it should not exceed max valid address; + // If the address is invalid, it will not exceed usize::max; + pub open spec fn const_add_requires(&self, offset: usize) -> bool { + &&& self.is_canonical_vaddr() + &&& self@ + offset <= usize::MAX + &&& self.valid_access() ==> (self@ + offset <= VADDR_LOWER_MASK || offset + == VADDR_UPPER_MASK) + } + + #[inline] + pub open spec fn const_add_ensures(&self, offset: usize, ret: VirtAddr) -> bool { + &&& ret.is_canonical_vaddr() + &&& self.valid_access() ==> (ret@ == self@ + offset) + &&& (offset != VADDR_UPPER_MASK) ==> ret.valid_access() == self.valid_access() + &&& (offset == VADDR_UPPER_MASK) ==> !ret.valid_access() + } + + pub open spec fn sub_requires(&self, other: Self) -> bool { + &&& self.is_canonical_vaddr() + &&& other.is_canonical_vaddr() + &&& self@ >= other@ + } + + /// Substract a address from another should only make sense if they are both + /// valid or invalid. If self is invalid while other is valid, the + /// sign_extend(self@-other) can be confusing, which could be + /// self@.lower_bits() - other.lower_bits() or self@ - other or 1usize<<47 + + /// self@.lower_bits() - other.lower_bits() + pub open spec fn sub_ensures(&self, other: Self, ret: InnerAddr) -> bool { + let valid_sub = self.valid_access() == other.valid_access(); + &&& valid_sub ==> ret == self@ - other@ + &&& valid_sub ==> ret == sign_extend_spec((self@ - other@) as InnerAddr) + } + + // For a valid address, other must be smaller than self.lower_bits() + // Otherwise, this operation may accidentally make an invalid address valid. + // We may convert an invalid to valid only when other == VADDR_UPPER_MASK. + pub open spec fn sub_usize_requires(&self, other: usize) -> bool { + &&& self.is_canonical_vaddr() + &&& self@ >= other + &&& (other <= self.lower_bits() || other == VADDR_UPPER_MASK) + } + + pub open spec fn sub_usize_ensures(&self, other: usize, ret: Self) -> bool { + ret.const_add_ensures(other, *self) + } + + // Proves that a valid virtual address falls into [0, 0x00007FFFFFFFFFFF] + broadcast proof fn lemma_range(vaddr: VirtAddr) + requires + #[trigger] vaddr.is_canonical_vaddr(), + ensures + vaddr.valid_access() == (vaddr@ <= VADDR_LOWER_MASK), + !vaddr.valid_access() == (vaddr@ >= VADDR_UPPER_MASK), + vaddr.valid_access() ==> vaddr@ == vaddr.lower_bits(), + !vaddr.valid_access() ==> vaddr@ == vaddr.lower_bits() + VADDR_UPPER_MASK, + { + } +} + +} // verus! +#[cfg(verus_keep_ghost)] +mod another_impl { + use super::*; + + /// A different implementation of sign_extend2. + /// The expected results is the same but impl and proof could be different. + #[verus_verify] + #[ensures(|ret: InnerAddr| [sign_extend_ensures(addr, ret)])] + const fn sign_extend_different_impl(addr: InnerAddr) -> InnerAddr { + let left_bits = InnerAddr::BITS as usize - SIGN_BIT - 1; + proof! { + assert(sign_extend_ensures(addr, ((addr << 16) as i64 >> 16) as InnerAddr)) + by (bit_vector); + } + ((addr << left_bits) as i64 >> left_bits) as InnerAddr + } +} diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs index 250b94e0b..187853e78 100644 --- a/kernel/src/lib.rs +++ b/kernel/src/lib.rs @@ -5,6 +5,8 @@ // Author: Nicolai Stange #![no_std] +#![cfg_attr(RUST_BEFORE_1_78, feature(offset_of))] // stable feature after v1.78 but nightly feature in v1.77 +#![cfg_attr(RUST_BEFORE_1_78, feature(inline_const))] // stable feature in v1.78 but nightly feature in v1.77 #![cfg_attr(all(test, test_in_svsm), no_main)] #![cfg_attr(all(test, test_in_svsm), feature(custom_test_frameworks))] #![cfg_attr(all(test, test_in_svsm), test_runner(crate::testing::svsm_test_runner))] diff --git a/kernel/src/mm/page_visibility.rs b/kernel/src/mm/page_visibility.rs index f442cb3d9..039c5619e 100644 --- a/kernel/src/mm/page_visibility.rs +++ b/kernel/src/mm/page_visibility.rs @@ -131,7 +131,7 @@ impl SharedBox { copy_bytes( self.ptr.as_ptr() as usize, out as *const T as usize, - size_of::(), + core::mem::size_of::(), ); } } @@ -146,7 +146,7 @@ impl SharedBox { copy_bytes( value as *const T as usize, self.ptr.as_ptr() as usize, - size_of::(), + core::mem::size_of::(), ); } } @@ -171,7 +171,7 @@ impl SharedBox<[T; N]> { unsafe { // SAFETY: `self.ptr` is valid and we did a bounds check on `n`. - write_bytes(self.ptr.as_ptr() as usize, size_of::() * n, 0); + write_bytes(self.ptr.as_ptr() as usize, core::mem::size_of::() * n, 0); } Ok(()) @@ -206,7 +206,7 @@ unsafe impl Sync for SharedBox where T: Sync {} impl Drop for SharedBox { fn drop(&mut self) { // Re-encrypt the pages. - let res = (0..size_of::()) + let res = (0..core::mem::size_of::()) .step_by(PAGE_SIZE) .try_for_each(|offset| unsafe { make_page_private(self.addr() + offset) }); diff --git a/kernel/src/svsm.rs b/kernel/src/svsm.rs index 9126ee690..7b2c946cc 100755 --- a/kernel/src/svsm.rs +++ b/kernel/src/svsm.rs @@ -96,7 +96,7 @@ global_asm!( static CPUID_PAGE: ImmutAfterInitCell = ImmutAfterInitCell::uninit(); static LAUNCH_INFO: ImmutAfterInitCell = ImmutAfterInitCell::uninit(); -const _: () = assert!(size_of::() <= PAGE_SIZE); +const _: () = assert!(core::mem::size_of::() <= PAGE_SIZE); fn copy_cpuid_table_to_fw(fw_addr: PhysAddr) -> Result<(), SvsmError> { let guard = PerCPUPageMappingGuard::create_4k(fw_addr)?; diff --git a/scripts/vfmt.sh b/scripts/vfmt.sh new file mode 100755 index 000000000..e2b668127 --- /dev/null +++ b/scripts/vfmt.sh @@ -0,0 +1,13 @@ +for f in `find ./ -type f -name "*.verus.rs"` +do +output=$(verusfmt $f $@ 2>&1) +if [ $? -ne 0 ]; then + # Check if the output contains "Failed to parse" + if echo "$output" | grep -q "Failed to parse"; then + echo "Continuing despite parse failure: $output" + else + echo "Error occurred: $output" + exit 1 + fi +fi +done diff --git a/scripts/vinstall.sh b/scripts/vinstall.sh new file mode 100755 index 000000000..037d5cdfc --- /dev/null +++ b/scripts/vinstall.sh @@ -0,0 +1,12 @@ +#!/bin/bash +VERISMO_REV=7c9c445 +cargo install --git https://github.com/microsoft/verismo/ --rev $VERISMO_REV cargo-v +builtin=`cargo metadata --format-version 1 | jq -r '.packages[] | select(.name == "builtin_macros") | .targets[].src_path'` +verus=`dirname $builtin`/../../../source/target-verus/release/verus +if [ -f ${verus} ]; then + echo "verus (${verus}) is already built" +else + cargo v prepare-verus +fi +cargo install --git https://github.com/microsoft/verismo/ --rev $VERISMO_REV verus-rustc +curl --proto '=https' --tlsv1.2 -LsSf https://github.com/verus-lang/verusfmt/releases/download/v0.4.3/verusfmt-installer.sh | sh diff --git a/scripts/vpath.sh b/scripts/vpath.sh new file mode 100755 index 000000000..54ccf5668 --- /dev/null +++ b/scripts/vpath.sh @@ -0,0 +1,4 @@ +builtin=`cargo metadata --format-version 1 | jq -r '.packages[] | select(.name == "builtin_macros") | .targets[].src_path'` +verus=`dirname $builtin`/../../../ +verus=`realpath $verus` +export VERUS_PATH=$verus diff --git a/verismo/Cargo.toml b/verismo/Cargo.toml new file mode 100644 index 000000000..e41c3d193 --- /dev/null +++ b/verismo/Cargo.toml @@ -0,0 +1,21 @@ +[package] +name = "verismo" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +builtin = { workspace = true, optional = true } +builtin_macros = { workspace = true } +vstd = { workspace = true, optional = true } +paste = "1.0" +seq-macro = "0.3" + +[lints] +workspace = true + +[features] +default = [] +noverify = [] +verus = ["builtin", "vstd"] diff --git a/verismo/build.rs b/verismo/build.rs new file mode 100644 index 000000000..17735a5fe --- /dev/null +++ b/verismo/build.rs @@ -0,0 +1,26 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou + +fn main() { + init_verify(); +} + +fn init_verify() { + if cfg!(feature = "noverify") { + println!("cargo:rustc-env=VERUS_ARGS=--no-verify"); + } else { + let verus_args = [ + "--rlimit=8000", + "--expand-errors", + "--multiple-errors=5", + "--triggers-silent", + "--no-auto-recommends-check", + "--trace", + "-Z unstable-options", + ]; + println!("cargo:rustc-env=VERUS_ARGS={}", verus_args.join(" ")); + } +} diff --git a/verismo/src/bits.rs b/verismo/src/bits.rs new file mode 100644 index 000000000..479172526 --- /dev/null +++ b/verismo/src/bits.rs @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou + +#[cfg(verus_keep_ghost)] +include!("bits.verus.rs"); diff --git a/verismo/src/bits.verus.rs b/verismo/src/bits.verus.rs new file mode 100644 index 000000000..9106127b9 --- /dev/null +++ b/verismo/src/bits.verus.rs @@ -0,0 +1,221 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou +use vstd::prelude::*; + +verus! { + +#[verifier(inline)] +pub open spec fn bit_value(n: u64) -> u64 + recommends + n < 64, +{ + if n == 0 { + 0x1 + } else if n == 1 { + 0x2 + } else if n == 2 { + 0x4 + } else if n == 3 { + 0x8 + } else if n == 4 { + 0x10 + } else if n == 5 { + 0x20 + } else if n == 6 { + 0x40 + } else if n == 7 { + 0x80 + } else if n == 8 { + 0x100 + } else if n == 9 { + 0x200 + } else if n == 10 { + 0x400 + } else if n == 11 { + 0x800 + } else if n == 12 { + 0x1000 + } else if n == 13 { + 0x2000 + } else if n == 14 { + 0x4000 + } else if n == 15 { + 0x8000 + } else if n == 16 { + 0x10000 + } else if n == 17 { + 0x20000 + } else if n == 18 { + 0x40000 + } else if n == 19 { + 0x80000 + } else if n == 20 { + 0x100000 + } else if n == 21 { + 0x200000 + } else if n == 22 { + 0x400000 + } else if n == 23 { + 0x800000 + } else if n == 24 { + 0x1000000 + } else if n == 25 { + 0x2000000 + } else if n == 26 { + 0x4000000 + } else if n == 27 { + 0x8000000 + } else if n == 28 { + 0x10000000 + } else if n == 29 { + 0x20000000 + } else if n == 30 { + 0x40000000 + } else if n == 31 { + 0x80000000 + } else if n == 32 { + 0x100000000 + } else if n == 33 { + 0x200000000 + } else if n == 34 { + 0x400000000 + } else if n == 35 { + 0x800000000 + } else if n == 36 { + 0x1000000000 + } else if n == 37 { + 0x2000000000 + } else if n == 38 { + 0x4000000000 + } else if n == 39 { + 0x8000000000 + } else if n == 40 { + 0x10000000000 + } else if n == 41 { + 0x20000000000 + } else if n == 42 { + 0x40000000000 + } else if n == 43 { + 0x80000000000 + } else if n == 44 { + 0x100000000000 + } else if n == 45 { + 0x200000000000 + } else if n == 46 { + 0x400000000000 + } else if n == 47 { + 0x800000000000 + } else if n == 48 { + 0x1000000000000 + } else if n == 49 { + 0x2000000000000 + } else if n == 50 { + 0x4000000000000 + } else if n == 51 { + 0x8000000000000 + } else if n == 52 { + 0x10000000000000 + } else if n == 53 { + 0x20000000000000 + } else if n == 54 { + 0x40000000000000 + } else if n == 55 { + 0x80000000000000 + } else if n == 56 { + 0x100000000000000 + } else if n == 57 { + 0x200000000000000 + } else if n == 58 { + 0x400000000000000 + } else if n == 59 { + 0x800000000000000 + } else if n == 60 { + 0x1000000000000000 + } else if n == 61 { + 0x2000000000000000 + } else if n == 62 { + 0x4000000000000000 + } else if n == 63 { + 0x8000000000000000 + } else { + 0 + } +} + +pub open spec fn is_pow_of_2(val: u64) -> bool { + seq_macro::seq! {N in 0..63 {#( + val == bit_value(N) || + )* false + }} +} + +} // verus! +macro_rules! bit_shl_values { + ($typ:ty, $styp:ty, $one: expr, $pname: ident) => { + verus! { + #[doc = "Proof that shifting 1 by N has a bound."] + pub broadcast proof fn $pname(offset: $typ) + requires 0 <= offset < $styp::BITS + ensures + #[trigger]($one << offset) == bit_value(offset as u64), + { + assert($one << offset == bit_value(offset as u64)) by(bit_vector); + } + } + }; +} + +macro_rules! bit_not_properties { + ($typ:ty, $styp:ty, $sname: ident, $autopname: ident) => { + verus! { + #[doc = "Proof that !a is equal to max - a, and !!a == a"] + pub broadcast proof fn $autopname(a: $typ) + ensures + #[trigger]!a == sub($styp::MAX as $typ, a), + !(!a) == a, + { + assert(!(!a) == a) by(bit_vector); + assert((!a) == $styp::MAX - a) by(bit_vector); + } + } + }; +} + +macro_rules! bit_set_clear_mask { + ($typ:ty, $styp:ty, $pname_or_mask: ident, $pname_and_mask: ident) => { + verus! { + #[doc = "Proof that a mask m is set with or operation."] + #[verifier(bit_vector)] + pub broadcast proof fn $pname_or_mask(a: $typ, m: $typ) + ensures + (#[trigger](a | m)) & m == m, + (a | m) & (!m) == a & (!m), + a | m >= a, + a | m >= m, + a == (a|m) - m + (a|!m) - !m + {} + + #[doc = "Proof that a mask m is cleared with and operation."] + #[verifier(bit_vector)] + pub broadcast proof fn $pname_and_mask(a: $typ, m: $typ) + ensures + (#[trigger](a & m)) & !m == 0, + (a & m) & m == a & m, + a & m <= m, + a & m <= a, + a == add(a & m, a & !m), + {} + } + }; +} + +bit_shl_values! {u64, u64, 1u64, lemma_bit_u64_shl_values} +bit_not_properties! {u64, u64, spec_bit_u64_not_properties, lemma_bit_u64_not_is_sub} +bit_set_clear_mask! {u64, u64, lemma_bit_u64_or_mask, lemma_bit_u64_and_mask} + +bit_shl_values! {usize, u64, 1usize, lemma_bit_usize_shl_values} +bit_not_properties! {usize, u64, spec_bit_usize_not_properties, lemma_bit_usize_not_is_sub} +bit_set_clear_mask! {usize, u64, lemma_bit_usize_or_mask, lemma_bit_usize_and_mask} diff --git a/verismo/src/layout.rs b/verismo/src/layout.rs new file mode 100644 index 000000000..ea1928bfb --- /dev/null +++ b/verismo/src/layout.rs @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou + +#[cfg(feature = "verus")] +include!("layout.verus.rs"); diff --git a/verismo/src/layout.verus.rs b/verismo/src/layout.verus.rs new file mode 100644 index 000000000..cc88d045f --- /dev/null +++ b/verismo/src/layout.verus.rs @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou +use vstd::prelude::*; + +verus! { + +global size_of usize == 8; + +} // verus! diff --git a/verismo/src/lib.rs b/verismo/src/lib.rs new file mode 100644 index 000000000..5777b0d1f --- /dev/null +++ b/verismo/src/lib.rs @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou + +#![no_std] +#![allow(unused_braces)] +#![allow(unexpected_cfgs)] + +pub mod bits; +pub mod layout; From 2a20c9b478aca63eec55553f9ed81ce8cee26a6e Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Tue, 22 Oct 2024 22:24:19 -0700 Subject: [PATCH 2/8] Verify addr (#2) Verify more in address mod & Split verismo to verify_proof and verify_external. * Verify more in address mod. * Rename spec and improve the definition of canonical address * Most functions for VirtAddr are verified. * Move broadcast proofs into address_inner.verus.rs * Split verismo lib into verify_proof and verify_external. * Improve verification.md * Add verify_external to define spec for externals * No dep verify by default * Fix CI * Revert changes in existing ci * change name in verify.yml * Use verus main branch * Upgrade verus lib to latest main branch Signed-off-by: ziqiao zhou --------- Signed-off-by: ziqiao zhou Signed-off-by: Ziqiao Zhou --- .github/workflows/rust.yml | 2 +- .github/workflows/signed-off.yml | 4 +- .github/workflows/verify.yml | 9 +- Cargo.lock | 26 +- Cargo.toml | 14 +- Documentation/docs/developer/VERIFICATION.md | 59 ++- kernel/Cargo.toml | 8 +- kernel/build.rs | 2 +- kernel/src/address.rs | 63 ++- kernel/src/address.verus.rs | 270 ++++++------ kernel/src/address_inner.verus.rs | 175 ++++++++ kernel/src/types.rs | 7 + .../src/types.verus.rs | 8 +- scripts/vinstall.sh | 1 + verify_external/Cargo.toml | 17 + {verismo => verify_external}/build.rs | 2 +- .../src/convert.rs | 4 +- verify_external/src/convert.verus.rs | 79 ++++ verify_external/src/lib.rs | 31 ++ verify_external/src/vstd.verus.rs | 43 ++ {verismo => verify_proof}/Cargo.toml | 2 +- verify_proof/build.rs | 27 ++ {verismo => verify_proof}/src/bits.rs | 0 verify_proof/src/bits.verus.rs | 387 ++++++++++++++++++ {verismo => verify_proof}/src/lib.rs | 8 +- verismo/src/bits.verus.rs | 221 ---------- 26 files changed, 1062 insertions(+), 407 deletions(-) create mode 100644 kernel/src/address_inner.verus.rs rename verismo/src/layout.verus.rs => kernel/src/types.verus.rs (56%) create mode 100644 verify_external/Cargo.toml rename {verismo => verify_external}/build.rs (95%) rename verismo/src/layout.rs => verify_external/src/convert.rs (72%) create mode 100644 verify_external/src/convert.verus.rs create mode 100644 verify_external/src/lib.rs create mode 100644 verify_external/src/vstd.verus.rs rename {verismo => verify_proof}/Cargo.toml (94%) create mode 100644 verify_proof/build.rs rename {verismo => verify_proof}/src/bits.rs (100%) create mode 100644 verify_proof/src/bits.verus.rs rename {verismo => verify_proof}/src/lib.rs (77%) delete mode 100644 verismo/src/bits.verus.rs diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 6d0c786fa..668670ada 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -4,7 +4,7 @@ on: push: branches: [ "main" ] pull_request: - branches: [ "main", "verify" ] + branches: [ "main" ] env: CARGO_TERM_COLOR: always diff --git a/.github/workflows/signed-off.yml b/.github/workflows/signed-off.yml index 3c0a2cfab..f49c02fd6 100644 --- a/.github/workflows/signed-off.yml +++ b/.github/workflows/signed-off.yml @@ -1,8 +1,6 @@ name: SignedOff -on: - pull_request: - branches: [ "main" ] +on: [pull_request] jobs: check: diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 94e54647f..00f319d89 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -1,8 +1,7 @@ name: Verification on: - push: - branches: [ "verify" ] + workflow_dispatch: pull_request: branches: [ "verify" ] @@ -40,10 +39,14 @@ jobs: - name: Install verus toolchains run: ./scripts/vinstall.sh - - name: Build with verus + - name: Verify svsm with verus run: cargo verify working-directory: kernel + - name: Verify extra proof libs with verus + run: cargo verify + working-directory: verify_proof + - name: Build without verifying run: cargo build working-directory: kernel diff --git a/Cargo.lock b/Cargo.lock index 3879b805b..03c829da0 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -172,12 +172,12 @@ dependencies = [ [[package]] name = "builtin" version = "0.1.0" -source = "git+https://github.com/verus-lang/verus?rev=0ee96be2#0ee96be22afe96fc15a228db7eaba8350e9bcbf8" +source = "git+https://github.com/verus-lang/verus?rev=2776465#27764656a55aa214134f79187aac28435ae52ebc" [[package]] name = "builtin_macros" version = "0.1.0" -source = "git+https://github.com/verus-lang/verus?rev=0ee96be2#0ee96be22afe96fc15a228db7eaba8350e9bcbf8" +source = "git+https://github.com/verus-lang/verus?rev=2776465#27764656a55aa214134f79187aac28435ae52ebc" dependencies = [ "prettyplease_verus", "proc-macro2", @@ -784,7 +784,7 @@ dependencies = [ [[package]] name = "prettyplease_verus" version = "0.1.15" -source = "git+https://github.com/verus-lang/verus?rev=0ee96be2#0ee96be22afe96fc15a228db7eaba8350e9bcbf8" +source = "git+https://github.com/verus-lang/verus?rev=2776465#27764656a55aa214134f79187aac28435ae52ebc" dependencies = [ "proc-macro2", "syn_verus", @@ -958,7 +958,7 @@ dependencies = [ [[package]] name = "state_machines_macros" version = "0.1.0" -source = "git+https://github.com/verus-lang/verus?rev=0ee96be2#0ee96be22afe96fc15a228db7eaba8350e9bcbf8" +source = "git+https://github.com/verus-lang/verus?rev=2776465#27764656a55aa214134f79187aac28435ae52ebc" dependencies = [ "indexmap", "proc-macro2", @@ -1007,7 +1007,8 @@ dependencies = [ "syscall", "tdx-tdcall", "test", - "verismo", + "verify_external", + "verify_proof", "vstd", "zerocopy 0.8.7", ] @@ -1046,7 +1047,7 @@ dependencies = [ [[package]] name = "syn_verus" version = "1.0.95" -source = "git+https://github.com/verus-lang/verus?rev=0ee96be2#0ee96be22afe96fc15a228db7eaba8350e9bcbf8" +source = "git+https://github.com/verus-lang/verus?rev=2776465#27764656a55aa214134f79187aac28435ae52ebc" dependencies = [ "proc-macro2", "quote", @@ -1178,7 +1179,16 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f8c5f0a0af699448548ad1a2fbf920fb4bee257eae39953ba95cb84891a0446a" [[package]] -name = "verismo" +name = "verify_external" +version = "0.1.0" +dependencies = [ + "builtin", + "builtin_macros", + "vstd", +] + +[[package]] +name = "verify_proof" version = "0.1.0" dependencies = [ "builtin", @@ -1203,7 +1213,7 @@ checksum = "442887c63f2c839b346c192d047a7c87e73d0689c9157b00b53dcc27dd5ea793" [[package]] name = "vstd" version = "0.1.0" -source = "git+https://github.com/verus-lang/verus?rev=0ee96be2#0ee96be22afe96fc15a228db7eaba8350e9bcbf8" +source = "git+https://github.com/verus-lang/verus?rev=2776465#27764656a55aa214134f79187aac28435ae52ebc" dependencies = [ "builtin", "builtin_macros", diff --git a/Cargo.toml b/Cargo.toml index a7843c6c3..c68b9d9a3 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -14,8 +14,9 @@ members = [ "libmstpm", # syscall interface definitions "syscall", - # verification library for svsm - "verismo", + # verification libraries for svsm + "verify_proof", + "verify_external", ] @@ -53,12 +54,13 @@ zerocopy = { version = "0.8.2", features = ["alloc", "derive"] } packit = { git = "https://github.com/coconut-svsm/packit", version = "0.1.1" } # Verus repos -builtin = { git = "https://github.com/verus-lang/verus", rev ="0ee96be2", default-features = false } -builtin_macros = { git = "https://github.com/verus-lang/verus", rev ="0ee96be2", default-features = false } -vstd = { git = "https://github.com/verus-lang/verus", rev ="0ee96be2", features = ["alloc"], default-features = false } +builtin = { git = "https://github.com/verus-lang/verus", rev ="2776465", default-features = false } +builtin_macros = { git = "https://github.com/verus-lang/verus", rev ="2776465", default-features = false } +vstd = { git = "https://github.com/verus-lang/verus", rev ="2776465", features = ["alloc"], default-features = false } # Verification libs -verismo = { path = "verismo", default-features = false } +verify_proof = { path = "verify_proof", default-features = false } +verify_external = { path = "verify_external", default-features = false } [workspace.lints.rust] future_incompatible = { level = "deny", priority = 127 } diff --git a/Documentation/docs/developer/VERIFICATION.md b/Documentation/docs/developer/VERIFICATION.md index 2805c5a10..ff646f139 100644 --- a/Documentation/docs/developer/VERIFICATION.md +++ b/Documentation/docs/developer/VERIFICATION.md @@ -1,18 +1,20 @@ -VERIFICATION -======= +# VERIFICATION -To run verification, we will need to a few steps to setup the build toolchains. +Formal verification is done via [Verus](https://github.com/verus-lang/verus). +To run verification, you need to setup the verification tools in order to run +`cargo verify`. +## Setup -## Build - -### Install verification tools +Run the following commands to install verus and cargo-verify. ``` cd svsm ./scripts/vinstall.sh ``` +## Build + ### Build svsm with verification ``` @@ -20,22 +22,29 @@ cd svsm/kernel cargo verify ``` -By default, it will verify all crates (except for vstd), if you do not want to -verify other crates, use `cargo verify --features verus_no_dep_verify`. +By default, it only verifies the current crate. ### Pass verus arguments for verification. -It is helpful to pass extra args for verification debugging. - -You can pass extra verus arguments via {crate}_{lib/bin}_VERUS_ARGS to a specific crate +For debugging purposes, it may be helpful to pass additional Verus arguments. +You can specify extra arguments using environmental variable +{crate}_{lib/bin}_VERUS_ARGS to a specific crate {crate} or VERUS_ARGS to all crates. -`svsm_lib_VERUS_ARGS="--no-verify" cargo verify` compiles the code without verifying -svsm crate. +**Examples** + +* Compiles a crate without verifying svsm crate: -`svsm_lib_VERUS_ARGS="--verify-module address" cargo verify` verify only address -module in the crate svsm. + ``` + svsm_lib_VERUS_ARGS="--no-verify" cargo verify + ``` + +* Compiles a crate while only verifying address module in svsm crate: + + ``` + svsm_lib_VERUS_ARGS="--verify-module address" cargo verify + ``` @@ -46,10 +55,26 @@ cd svsm/kernel cargo build ``` -## Manage specification and proof codes +## Developing specification and proof + +While Verus allows you to write specifications and proofs in Rust, it's +beneficial to use the verus!{} macro for a more concise, mathematical syntax +similar to Dafny, F*, and Coq. To get started, be sure to read the [Verus +Tutorial](https://verus-lang.github.io/verus/guide/overview.html) + + +### Development Guidelines * Minimize annotations inside executable Rust. -* Define specification and proof code in `*.verus.rs` or in a different crates. Those codes wrapped in verus!{} macro and need verusfmt to format. +* For a module `x`, define code-related specification and proof in `x.verus.rs` . +* Codes wrapped in verus!{} macro could be formatted via verusfmt. + ./script/vfmt.sh triggers verusfmt for `*.verus.rs` +* Use external specification and proofs from + [vstd](https://verus-lang.github.io/verus/verusdoc/vstd/) when possible. +* When verifying with functions/structs/traits from external crates, define + specifications in `verify_external/` if `vstd` does not provide. +* Expensive and reusable proofs are stored in `verify_proof/` if `vstd` does not + provide. ``` cd svsm diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml index 3af6265dc..24c937b88 100644 --- a/kernel/Cargo.toml +++ b/kernel/Cargo.toml @@ -40,7 +40,8 @@ zerocopy.workspace = true builtin = { workspace = true, optional = true } builtin_macros = { workspace = true } vstd = { workspace = true, optional = true } -verismo = { workspace = true, optional = true} +verify_proof = { workspace = true, optional = true} +verify_external = { workspace = true, optional = true} [target."x86_64-unknown-none".dev-dependencies] test.workspace = true @@ -51,8 +52,9 @@ enable-gdb = ["dep:gdbstub", "dep:gdbstub_arch"] mstpm = ["dep:libmstpm"] nosmep = [] nosmap = [] -verus_no_dep_verify = ["verus", "verismo/noverify"] -verus = ["vstd", "builtin", "verismo/verus"] + +verus_all = ["vstd", "builtin", "verify_proof/verus", "verify_external/verus"] +verus = ["verus_all", "verify_proof/noverify", "verify_external/noverify"] noverify = [] [dev-dependencies] diff --git a/kernel/build.rs b/kernel/build.rs index cb7b7c3fd..a87372b27 100644 --- a/kernel/build.rs +++ b/kernel/build.rs @@ -61,7 +61,7 @@ fn init_verify() { println!("cargo:rustc-env=VERUS_ARGS=--no-verify"); } else { let verus_args = [ - "--rlimit=8000", + "--rlimit=1", "--expand-errors", "--multiple-errors=5", "--triggers-silent", diff --git a/kernel/src/address.rs b/kernel/src/address.rs index eb268f68f..4274d555f 100644 --- a/kernel/src/address.rs +++ b/kernel/src/address.rs @@ -12,20 +12,20 @@ use core::slice; use builtin_macros::*; +#[cfg(verus_keep_ghost)] +include!("address.verus.rs"); + // The backing type to represent an address; type InnerAddr = usize; #[verus_verify] const SIGN_BIT: usize = 47; -include!("address.verus.rs"); - #[inline] #[verus_verify] -#[ensures(|ret: InnerAddr| [sign_extend_ensures(addr, ret)])] +#[ensures(|ret: InnerAddr| sign_extend_ensures(addr, ret))] const fn sign_extend(addr: InnerAddr) -> InnerAddr { let mask = 1usize << SIGN_BIT; - if (addr & mask) == mask { addr | !((1usize << SIGN_BIT) - 1) } else { @@ -33,72 +33,104 @@ const fn sign_extend(addr: InnerAddr) -> InnerAddr { } } +#[verus_verify] pub trait Address: Copy + From + Into + PartialEq + Eq + PartialOrd + Ord { // Transform the address into its inner representation for easier /// arithmetic manipulation #[inline] + #[verus_verify] + #[ensures(|ret: InnerAddr| ret === from_spec(*self))] fn bits(&self) -> InnerAddr { (*self).into() } #[inline] + #[verus_verify] + #[ensures(|ret: bool| ret == (from_spec(*self) === 0usize))] fn is_null(&self) -> bool { self.bits() == 0 } #[inline] + #[verus_verify] + #[requires(align_up_requires(from_spec(*self), align))] + #[ensures(|ret: Self| ret === addr_align_up(*self, align))] fn align_up(&self, align: InnerAddr) -> Self { Self::from((self.bits() + (align - 1)) & !(align - 1)) } #[inline] + #[verus_verify] + #[requires(align_up_requires(from_spec(*self), PAGE_SIZE))] + #[ensures(|ret: Self| ret === addr_page_align_up(*self))] fn page_align_up(&self) -> Self { self.align_up(PAGE_SIZE) } #[inline] + #[verus_verify] + #[requires(align_requires(PAGE_SIZE))] + #[ensures(|ret: Self| ret === addr_page_align_down(*self))] fn page_align(&self) -> Self { Self::from(self.bits() & !(PAGE_SIZE - 1)) } #[inline] + #[verus_verify] + #[requires(align_requires(align))] + #[ensures(|ret: bool| ret == addr_is_aligned_spec(*self, align))] fn is_aligned(&self, align: InnerAddr) -> bool { (self.bits() & (align - 1)) == 0 } #[inline] + #[verus_verify(external_body)] + #[requires(align_requires(core::mem::align_of::()))] + #[ensures(|ret: bool| ret == addr_is_aligned_spec(*self, core::mem::align_of::()))] fn is_aligned_to(&self) -> bool { self.is_aligned(core::mem::align_of::()) } #[inline] + #[verus_verify] + #[ensures(|ret: bool| ret == addr_is_page_aligned_spec(*self))] fn is_page_aligned(&self) -> bool { self.is_aligned(PAGE_SIZE) } #[inline] + #[verus_verify] fn checked_add(&self, off: InnerAddr) -> Option { self.bits().checked_add(off).map(|addr| addr.into()) } #[inline] + #[verus_verify] fn checked_sub(&self, off: InnerAddr) -> Option { self.bits().checked_sub(off).map(|addr| addr.into()) } #[inline] + #[verus_verify] fn saturating_add(&self, off: InnerAddr) -> Self { Self::from(self.bits().saturating_add(off)) } #[inline] + #[verus_verify] fn page_offset(&self) -> usize { self.bits() & (PAGE_SIZE - 1) } #[inline] + #[verus_verify] + #[requires( + size > 0, + from_spec::<_, InnerAddr>(*self) + size <= InnerAddr::MAX + )] + #[ensures(|ret: bool | ret == crosses_page_spec(*self, size))] fn crosses_page(&self, size: usize) -> bool { let start = self.bits(); let x1 = start / PAGE_SIZE; @@ -107,6 +139,8 @@ pub trait Address: } #[inline] + #[verus_verify] + #[ensures(|ret: InnerAddr| ret == pfn_spec(from_spec(*self)))] fn pfn(&self) -> InnerAddr { self.bits() >> PAGE_SHIFT } @@ -114,7 +148,6 @@ pub trait Address: #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, PartialOrd, Ord)] #[repr(transparent)] -#[verus_verify] pub struct PhysAddr(InnerAddr); impl PhysAddr { @@ -227,6 +260,9 @@ impl VirtAddr { } /// Returns the index into page-table pages of given levels. + #[verus_verify] + #[requires(L <= 5)] + #[ensures(|ret: usize| self.pgtbl_idx_ensures(L, ret))] pub const fn to_pgtbl_idx(&self) -> usize { (self.0 >> (12 + L * 9)) & 0x1ffusize } @@ -271,8 +307,9 @@ impl VirtAddr { #[verus_verify] #[requires(self.const_add_requires(offset))] - #[ensures(|ret: VirtAddr| [self.const_add_ensures(offset, ret)])] + #[ensures(|ret: VirtAddr| self.const_add_ensures(offset, ret))] pub const fn const_add(&self, offset: usize) -> Self { + proof! {use_type_invariant(self);} VirtAddr::new(self.0 + offset) } @@ -329,6 +366,8 @@ impl From for InnerAddr { impl From for VirtAddr { #[inline] + #[verus_verify(external_body)] + #[ensures(|ret: Self| ret.new_ensures(addr as usize))] fn from(addr: u64) -> Self { let addr: usize = addr.try_into().unwrap(); VirtAddr::from(addr) @@ -349,18 +388,16 @@ impl From for u64 { impl From<*const T> for VirtAddr { #[inline] #[verus_verify] - #[requires(vaddr_is_valid(ptr as usize))] fn from(ptr: *const T) -> Self { - Self(ptr as InnerAddr) + Self::from(ptr as InnerAddr) } } #[verus_verify] impl From<*mut T> for VirtAddr { #[verus_verify] - #[requires(vaddr_is_valid(ptr as usize))] fn from(ptr: *mut T) -> Self { - Self(ptr as InnerAddr) + Self::from(ptr as InnerAddr) } } @@ -396,14 +433,17 @@ impl ops::Add for VirtAddr { #[verus_verify] #[requires(self.const_add_requires(other))] - #[ensures(|ret: VirtAddr| [self.const_add_ensures(other, ret)])] + #[ensures(|ret: VirtAddr| self.const_add_ensures(other, ret))] fn add(self, other: InnerAddr) -> Self { + proof! {use_type_invariant(self);} VirtAddr::from(self.0 + other) } } +#[verus_verify] impl Address for VirtAddr { #[inline] + #[verus_verify] fn checked_add(&self, off: InnerAddr) -> Option { self.bits() .checked_add(off) @@ -411,6 +451,7 @@ impl Address for VirtAddr { } #[inline] + #[verus_verify] fn checked_sub(&self, off: InnerAddr) -> Option { self.bits() .checked_sub(off) diff --git a/kernel/src/address.verus.rs b/kernel/src/address.verus.rs index 3c1ea382b..89e856ab6 100644 --- a/kernel/src/address.verus.rs +++ b/kernel/src/address.verus.rs @@ -5,84 +5,50 @@ // Author: Ziqiao Zhou verus! { -#[cfg(verus_keep_ghost)] use vstd::prelude::*; +use verify_external::convert::{FromSpec, from_spec, axiom_from_spec}; pub broadcast group sign_extend_proof { - verismo::bits::lemma_bit_usize_not_is_sub, - verismo::bits::lemma_bit_usize_shl_values, - verismo::bits::lemma_bit_usize_or_mask, - verismo::bits::lemma_bit_usize_and_mask, + verify_proof::bits::lemma_bit_usize_not_is_sub, + verify_proof::bits::lemma_bit_usize_shl_values, + verify_proof::bits::lemma_bit_usize_or_mask, + verify_proof::bits::lemma_bit_usize_and_mask, + lemma_check_sign_bit, +} + +pub broadcast group address_align_proof { + crate::types::group_types_proof, + axiom_from_spec, + verify_proof::bits::lemma_bit_usize_and_mask_is_mod, + address_spec::proof_align_up, + address_spec::lemma_align_down, } -broadcast group vaddr_properties { +broadcast group vaddr_impl_proof { sign_extend_proof, - lemma_inner_addr_as_vaddr, + address_spec::lemma_inner_addr_as_vaddr, + address_spec::lemma_upper_address_has_sign_bit, + verify_proof::bits::lemma_bit_usize_and_mask_is_mod, + address_align_proof, + address_spec::reveal_pfn, } -broadcast use vaddr_properties; +broadcast use vaddr_impl_proof; /// Define a broadcast function and its related spec function calls in a inner /// module to avoid cyclic self-reference -#[cfg(verus_keep_ghost)] -mod address_spec { - use super::*; - - #[verifier(inline)] - pub spec const VADDR_LOWER_MASK: InnerAddr = 0x7FFF_FFFF_FFFF as InnerAddr; - - #[verifier(inline)] - pub spec const VADDR_UPPER_MASK: InnerAddr = !VADDR_LOWER_MASK; - - #[verifier(inline)] - pub open spec fn check_signed(addr: InnerAddr) -> bool { - addr & (1usize << 47) == 1usize << 47 - } - - #[verifier(inline)] - pub open spec fn vaddr_lower_bits(addr: InnerAddr) -> InnerAddr { - addr & VADDR_LOWER_MASK - } - - #[verifier(inline)] - pub open spec fn vaddr_upper_bits(addr: InnerAddr) -> InnerAddr { - addr & VADDR_UPPER_MASK - } - - #[verifier(inline)] - pub open spec fn vaddr_is_signed(addr: InnerAddr) -> bool { - addr & VADDR_UPPER_MASK == VADDR_UPPER_MASK - } - - #[verifier(inline)] - pub open spec fn vaddr_is_valid(addr: InnerAddr) -> bool { - addr & VADDR_UPPER_MASK == 0 - } - - pub broadcast proof fn lemma_inner_addr_as_vaddr(bits: InnerAddr) - ensures - vaddr_is_signed(bits) == (bits >= VADDR_UPPER_MASK), - vaddr_is_valid(bits) == (bits <= VADDR_LOWER_MASK), - vaddr_is_valid(bits) ==> #[trigger] vaddr_lower_bits(bits) == bits, - vaddr_is_signed(bits) ==> vaddr_upper_bits(bits) + vaddr_lower_bits(bits) == bits, - VADDR_UPPER_MASK > VADDR_LOWER_MASK, - vaddr_is_signed(bits) ==> check_signed(bits), - { - broadcast use sign_extend_proof; - - assert(vaddr_is_signed(bits) == (bits >= VADDR_UPPER_MASK)) by (bit_vector); - assert(vaddr_is_signed(bits) ==> check_signed(bits)) by (bit_vector); - assert(vaddr_is_valid(bits) == (bits <= VADDR_LOWER_MASK)) by (bit_vector); - } - -} +mod address_spec { include!("address_inner.verus.rs"); } #[cfg(verus_keep_ghost)] use address_spec::*; +pub open spec fn is_valid_addr(addr: InnerAddr) -> bool { + addr <= VADDR_LOWER_MASK || addr >= VADDR_UPPER_MASK +} + #[verifier(inline)] pub open spec fn sign_extend_spec(addr: InnerAddr) -> InnerAddr { - if check_signed(addr) { + if check_sign_bit(addr) { (vaddr_lower_bits(addr) + VADDR_UPPER_MASK) as InnerAddr } else { vaddr_lower_bits(addr) @@ -94,8 +60,53 @@ pub open spec fn sign_extend_spec(addr: InnerAddr) -> InnerAddr { pub open spec fn sign_extend_ensures(addr: InnerAddr, ret: InnerAddr) -> bool { &&& ret == sign_extend_spec(addr) &&& vaddr_lower_bits(ret) == vaddr_lower_bits(addr) - &&& check_signed(addr) ==> vaddr_is_signed(ret) - &&& !check_signed(addr) ==> vaddr_is_valid(ret) + &&& check_sign_bit(addr) ==> top_all_ones(ret) + &&& !check_sign_bit(addr) ==> top_all_zeros(ret) +} + +pub open spec fn addr_align_up(addr: A, align: InnerAddr) -> A { + from_spec(align_up_spec(from_spec(addr), align)) +} + +pub open spec fn addr_page_align_up(addr: A) -> A { + from_spec(align_up_spec(from_spec(addr), PAGE_SIZE)) +} + +pub open spec fn addr_page_align_down(addr: A) -> A { + from_spec(align_down_spec(from_spec(addr), PAGE_SIZE) as usize) +} + +pub open spec fn is_aligned_spec(val: InnerAddr, align: InnerAddr) -> bool { + val % align == 0 +} + +pub open spec fn addr_is_aligned_spec(addr: A, align: InnerAddr) -> bool { + is_aligned_spec(from_spec(addr), align) +} + +pub open spec fn addr_is_page_aligned_spec(addr: A) -> bool { + is_aligned_spec(from_spec(addr), PAGE_SIZE) +} + +pub open spec fn pt_idx_spec(addr: usize, l: usize) -> usize + recommends + l <= 5, +{ + let upper = match l { + 0usize => { addr >> 12 }, + 1usize => { addr >> 21 }, + 2usize => { addr >> 30 }, + 3usize => { addr >> 39 }, + 4usize => { addr >> 48 }, + 5usize => { addr >> 57 }, + _ => { 0 }, + }; + upper % 512 +} + +pub open spec fn crosses_page_spec>(addr: T, size: InnerAddr) -> bool { + let inner = from_spec::<_, InnerAddr>(addr); + pfn_spec(inner) != pfn_spec((inner + size - 1) as InnerAddr) } // Define a view (@) for VirtAddr @@ -109,102 +120,111 @@ impl View for VirtAddr { } impl VirtAddr { - /// A valid virtual address have a canonical form where the upper bits - /// are either all zeroes or all ones + /// Canonical form addresses run from 0 through 00007FFF'FFFFFFFF, + /// and from FFFF8000'00000000 through FFFFFFFF'FFFFFFFF. #[verifier::type_invariant] - pub closed spec fn is_canonical_vaddr(&self) -> bool { - vaddr_is_valid(self@) || vaddr_is_signed(self@) + pub open spec fn is_canonical(&self) -> bool { + self.is_low() || self.is_high() + } + + /// Property: + /// A valid virtual address have a canonical form where the upper bits + /// are either all zeroes or all ones. + proof fn property_canonical(&self) + ensures + self.is_canonical() == (top_all_zeros(self@) || top_all_ones(self@)), + { } - pub closed spec fn lower_bits(&self) -> InnerAddr { - vaddr_lower_bits(self@) + pub open spec fn is_low(&self) -> bool { + self@ <= VADDR_LOWER_MASK } - pub closed spec fn valid_access(&self) -> bool { - vaddr_is_valid(self@) + pub open spec fn is_high(&self) -> bool { + self@ >= VADDR_UPPER_MASK + } + + // Virtual memory offset indicating the distance from 0 + pub open spec fn offset(&self) -> int { + if self.is_low() { + self@ as int + } else { + self@ - VADDR_UPPER_MASK + VADDR_LOWER_MASK + 1 + } } pub open spec fn new_ensures(self, addr: InnerAddr) -> bool { sign_extend_ensures(addr, self@) } + pub open spec fn pgtbl_idx_ensures(&self, l: usize, ret: usize) -> bool { + ret == pt_idx_spec(self@, l) + } + + pub open spec fn pfn_spec(&self) -> InnerAddr { + pfn_spec(self@) + } + /* Specifications for methods */ // requires that adding offset will not cause not overflow. - // If the address is valid, it should not exceed max valid address; - // If the address is invalid, it will not exceed usize::max; + // If a low address, adding offset to it should not have set any bits in upper 16 bits. + // If a high address, should not exceed usize::MAX pub open spec fn const_add_requires(&self, offset: usize) -> bool { - &&& self.is_canonical_vaddr() - &&& self@ + offset <= usize::MAX - &&& self.valid_access() ==> (self@ + offset <= VADDR_LOWER_MASK || offset - == VADDR_UPPER_MASK) + self.offset() + offset < VADDR_RANGE_SIZE } - #[inline] pub open spec fn const_add_ensures(&self, offset: usize, ret: VirtAddr) -> bool { - &&& ret.is_canonical_vaddr() - &&& self.valid_access() ==> (ret@ == self@ + offset) - &&& (offset != VADDR_UPPER_MASK) ==> ret.valid_access() == self.valid_access() - &&& (offset == VADDR_UPPER_MASK) ==> !ret.valid_access() + &&& self.offset() + offset == ret.offset() } + // The current implementation assumes they are both high or low address. pub open spec fn sub_requires(&self, other: Self) -> bool { - &&& self.is_canonical_vaddr() - &&& other.is_canonical_vaddr() &&& self@ >= other@ + &&& other.is_high() || self.is_low() } - /// Substract a address from another should only make sense if they are both - /// valid or invalid. If self is invalid while other is valid, the - /// sign_extend(self@-other) can be confusing, which could be - /// self@.lower_bits() - other.lower_bits() or self@ - other or 1usize<<47 + - /// self@.lower_bits() - other.lower_bits() + // ret is the size of availabe virtual memory between the two addresses. pub open spec fn sub_ensures(&self, other: Self, ret: InnerAddr) -> bool { - let valid_sub = self.valid_access() == other.valid_access(); - &&& valid_sub ==> ret == self@ - other@ - &&& valid_sub ==> ret == sign_extend_spec((self@ - other@) as InnerAddr) + &&& ret == self.offset() - other.offset() } - // For a valid address, other must be smaller than self.lower_bits() - // Otherwise, this operation may accidentally make an invalid address valid. - // We may convert an invalid to valid only when other == VADDR_UPPER_MASK. pub open spec fn sub_usize_requires(&self, other: usize) -> bool { - &&& self.is_canonical_vaddr() - &&& self@ >= other - &&& (other <= self.lower_bits() || other == VADDR_UPPER_MASK) + self.offset() >= other } pub open spec fn sub_usize_ensures(&self, other: usize, ret: Self) -> bool { - ret.const_add_ensures(other, *self) + ret.offset() == self.offset() - other } +} - // Proves that a valid virtual address falls into [0, 0x00007FFFFFFFFFFF] - broadcast proof fn lemma_range(vaddr: VirtAddr) - requires - #[trigger] vaddr.is_canonical_vaddr(), - ensures - vaddr.valid_access() == (vaddr@ <= VADDR_LOWER_MASK), - !vaddr.valid_access() == (vaddr@ >= VADDR_UPPER_MASK), - vaddr.valid_access() ==> vaddr@ == vaddr.lower_bits(), - !vaddr.valid_access() ==> vaddr@ == vaddr.lower_bits() + VADDR_UPPER_MASK, - { +impl FromSpec<*mut T> for VirtAddr { + closed spec fn from_spec(v: *mut T) -> Self { + VirtAddr(sign_extend_spec(v as InnerAddr)) } } -} // verus! -#[cfg(verus_keep_ghost)] -mod another_impl { - use super::*; - - /// A different implementation of sign_extend2. - /// The expected results is the same but impl and proof could be different. - #[verus_verify] - #[ensures(|ret: InnerAddr| [sign_extend_ensures(addr, ret)])] - const fn sign_extend_different_impl(addr: InnerAddr) -> InnerAddr { - let left_bits = InnerAddr::BITS as usize - SIGN_BIT - 1; - proof! { - assert(sign_extend_ensures(addr, ((addr << 16) as i64 >> 16) as InnerAddr)) - by (bit_vector); - } - ((addr << left_bits) as i64 >> left_bits) as InnerAddr +impl FromSpec<*const T> for VirtAddr { + closed spec fn from_spec(v: *const T) -> Self { + VirtAddr(sign_extend_spec(v as InnerAddr)) + } +} + +impl FromSpec for VirtAddr { + closed spec fn from_spec(v: InnerAddr) -> Self { + VirtAddr(sign_extend_spec(v)) } } + +impl FromSpec for InnerAddr { + open spec fn from_spec(v: VirtAddr) -> Self { + v@ + } +} + +impl FromSpec for u64 { + open spec fn from_spec(v: VirtAddr) -> Self { + v@ as u64 + } +} + +} // verus! diff --git a/kernel/src/address_inner.verus.rs b/kernel/src/address_inner.verus.rs new file mode 100644 index 000000000..c3e5022b7 --- /dev/null +++ b/kernel/src/address_inner.verus.rs @@ -0,0 +1,175 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou +use super::*; + +verus! { + +broadcast use verify_proof::bits::lemma_bit_usize_shl_values; + +#[verifier(inline)] +pub spec const VADDR_MAX_BITS: nat = 48; + +#[verifier(inline)] +pub spec const VADDR_LOWER_MASK: InnerAddr = 0x7fff_ffff_ffff as InnerAddr; + +#[verifier(inline)] +pub spec const VADDR_UPPER_MASK: InnerAddr = !VADDR_LOWER_MASK; + +#[verifier(inline)] +pub spec const VADDR_RANGE_SIZE: InnerAddr = 0x1_0000_0000_0000u64 as InnerAddr; + +#[verifier(inline)] +pub open spec fn check_sign_bit(addr: InnerAddr) -> bool { + addr & (1usize << (VADDR_MAX_BITS - 1) as InnerAddr) == 1usize << (VADDR_MAX_BITS + - 1) as InnerAddr +} + +#[verifier(inline)] +pub open spec fn vaddr_lower_bits(addr: InnerAddr) -> InnerAddr { + addr & VADDR_LOWER_MASK +} + +#[verifier(inline)] +pub open spec fn vaddr_upper_bits(addr: InnerAddr) -> InnerAddr { + addr & VADDR_UPPER_MASK +} + +#[verifier(inline)] +pub open spec fn top_all_ones(addr: InnerAddr) -> bool { + addr & VADDR_UPPER_MASK == VADDR_UPPER_MASK +} + +#[verifier(inline)] +pub open spec fn top_all_zeros(addr: InnerAddr) -> bool { + addr & VADDR_UPPER_MASK == 0 +} + +pub broadcast proof fn lemma_check_sign_bit(bits: InnerAddr) + requires + bits < VADDR_RANGE_SIZE, + ensures + #![trigger bits & 1usize << (VADDR_MAX_BITS - 1)] + check_sign_bit(bits) == (bits > VADDR_LOWER_MASK), +{ + assert(check_sign_bit(bits) == (bits > VADDR_LOWER_MASK)) by (bit_vector) + requires + bits < VADDR_RANGE_SIZE, + ; +} + +pub broadcast proof fn lemma_upper_address_has_sign_bit(bits: InnerAddr) + ensures + #![trigger vaddr_upper_bits(bits)] + top_all_ones(bits) ==> check_sign_bit(bits), +{ + assert(top_all_ones(bits) ==> check_sign_bit(bits)) by (bit_vector); +} + +pub broadcast proof fn lemma_inner_addr_as_vaddr(bits: InnerAddr) + ensures + top_all_ones(bits) == (bits >= VADDR_UPPER_MASK), + top_all_zeros(bits) == (bits <= VADDR_LOWER_MASK), + top_all_zeros(bits) ==> #[trigger] vaddr_lower_bits(bits) == bits, + top_all_ones(bits) ==> vaddr_upper_bits(bits) + vaddr_lower_bits(bits) == bits, + VADDR_UPPER_MASK > VADDR_LOWER_MASK, +{ + broadcast use sign_extend_proof; + broadcast use verify_proof::bits::lemma_bit_usize_shl_values; + + assert(top_all_ones(bits) == (bits >= VADDR_UPPER_MASK)) by (bit_vector); + assert(top_all_zeros(bits) == (bits <= VADDR_LOWER_MASK)) by (bit_vector); + assert(VADDR_UPPER_MASK > VADDR_LOWER_MASK); +} + +pub closed spec fn pfn_spec(addr: usize) -> usize { + addr / PAGE_SIZE +} + +pub broadcast proof fn reveal_pfn(addr: usize) + ensures + #[trigger] pfn_spec(addr) == addr / PAGE_SIZE, + pfn_spec(addr) == addr >> PAGE_SHIFT, +{ + broadcast use verify_proof::bits::lemma_bit_usize_shl_values; + + verify_proof::bits::lemma_bit_usize_shr_is_div(addr, PAGE_SHIFT); +} + +pub open spec fn align_requires(align: InnerAddr) -> bool { + &&& verify_proof::bits::is_pow_of_2(align as u64) +} + +pub open spec fn _align_up_requires(bits: InnerAddr, align: InnerAddr) -> bool { + &&& align_requires(align) + &&& bits + (align - 1) <= InnerAddr::MAX +} + +pub open spec fn align_up_requires(bits: InnerAddr, align: InnerAddr) -> bool { + &&& _align_up_requires(bits, align) +} + +pub open spec fn align_up_spec(val: InnerAddr, align: InnerAddr) -> InnerAddr { + let r = val % align; + &&& if r == 0 { + val + } else { + (val - r + align) as InnerAddr + } +} + +pub open spec fn align_down_spec(val: InnerAddr, align: InnerAddr) -> int { + val - val % align +} + +broadcast group align_proof { + verify_proof::bits::lemma_bit_usize_not_is_sub, + verify_proof::bits::lemma_bit_usize_shl_values, + verify_proof::bits::lemma_bit_u64_shl_values, + vstd::bits::lemma_u64_pow2_no_overflow, + verify_proof::bits::lemma_bit_usize_and_mask, + verify_proof::bits::lemma_bit_usize_and_mask_is_mod, +} + +pub broadcast proof fn proof_align_up(x: usize, align: usize) + requires + align_up_requires(x, align), + ensures + #[trigger] add(x, sub(align, 1)) & !sub(align, 1) == align_up_spec(x, align), +{ + broadcast use align_proof; + + let mask = (align - 1) as usize; + let y = (x + mask) as usize; + assert(y & !mask == sub(y, y & mask)); + + if x % align == 0 { + assert((x + (align - 1)) % (align as int) == align - 1) by (nonlinear_arith) + requires + x % align == 0, + align > 0, + ; + } else { + assert((x + (align - 1)) % (align as int) == (x % align - 1) as int) by (nonlinear_arith) + requires + x % align != 0, + align > 0, + ; + } +} + +pub broadcast proof fn lemma_align_down(x: usize, align: usize) + requires + align_requires(align), + ensures + #[trigger] (x & !((align - 1) as usize)) == align_down_spec(x, align), +{ + broadcast use align_proof; + + let mask: usize = sub(align, 1); + assert(x == (x & !mask) + (x & mask)); +} + +} // verus! diff --git a/kernel/src/types.rs b/kernel/src/types.rs index ec42b99f9..b1394fee5 100644 --- a/kernel/src/types.rs +++ b/kernel/src/types.rs @@ -7,6 +7,11 @@ use crate::error::SvsmError; use crate::sev::vmsa::VMPL_MAX; +use builtin_macros::*; +include!("types.verus.rs"); + +verus! { + pub const PAGE_SHIFT: usize = 12; pub const PAGE_SHIFT_2M: usize = 21; pub const PAGE_SHIFT_1G: usize = 30; @@ -14,6 +19,8 @@ pub const PAGE_SIZE: usize = 1 << PAGE_SHIFT; pub const PAGE_SIZE_2M: usize = 1 << PAGE_SHIFT_2M; pub const PAGE_SIZE_1G: usize = 1 << PAGE_SHIFT_1G; +} + #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub enum PageSize { Regular, diff --git a/verismo/src/layout.verus.rs b/kernel/src/types.verus.rs similarity index 56% rename from verismo/src/layout.verus.rs rename to kernel/src/types.verus.rs index cc88d045f..3dcb87dff 100644 --- a/verismo/src/layout.verus.rs +++ b/kernel/src/types.verus.rs @@ -3,10 +3,12 @@ // Copyright (c) Microsoft Corporation // // Author: Ziqiao Zhou -use vstd::prelude::*; - verus! { -global size_of usize == 8; +pub broadcast group group_types_proof { + verify_proof::bits::lemma_bit_usize_shl_values, +} + +broadcast use group_types_proof; } // verus! diff --git a/scripts/vinstall.sh b/scripts/vinstall.sh index 037d5cdfc..67cf2a4da 100755 --- a/scripts/vinstall.sh +++ b/scripts/vinstall.sh @@ -10,3 +10,4 @@ else fi cargo install --git https://github.com/microsoft/verismo/ --rev $VERISMO_REV verus-rustc curl --proto '=https' --tlsv1.2 -LsSf https://github.com/verus-lang/verusfmt/releases/download/v0.4.3/verusfmt-installer.sh | sh +sudo apt-get install build-essential ninja-build libclang-dev diff --git a/verify_external/Cargo.toml b/verify_external/Cargo.toml new file mode 100644 index 000000000..7e9be0748 --- /dev/null +++ b/verify_external/Cargo.toml @@ -0,0 +1,17 @@ +[package] +name = "verify_external" +version = "0.1.0" +edition = "2021" + +[dependencies] +builtin = { workspace = true, optional = true } +builtin_macros = { workspace = true } +vstd = { workspace = true, optional = true } + +[lints] +workspace = true + +[features] +default = [] +noverify = [] +verus = ["builtin", "vstd"] diff --git a/verismo/build.rs b/verify_external/build.rs similarity index 95% rename from verismo/build.rs rename to verify_external/build.rs index 17735a5fe..ae3325284 100644 --- a/verismo/build.rs +++ b/verify_external/build.rs @@ -13,7 +13,7 @@ fn init_verify() { println!("cargo:rustc-env=VERUS_ARGS=--no-verify"); } else { let verus_args = [ - "--rlimit=8000", + "--rlimit=1", "--expand-errors", "--multiple-errors=5", "--triggers-silent", diff --git a/verismo/src/layout.rs b/verify_external/src/convert.rs similarity index 72% rename from verismo/src/layout.rs rename to verify_external/src/convert.rs index ea1928bfb..1bbe2f2b7 100644 --- a/verismo/src/layout.rs +++ b/verify_external/src/convert.rs @@ -4,5 +4,5 @@ // // Author: Ziqiao Zhou -#[cfg(feature = "verus")] -include!("layout.verus.rs"); +#[cfg(verus_keep_ghost)] +include!("convert.verus.rs"); diff --git a/verify_external/src/convert.verus.rs b/verify_external/src/convert.verus.rs new file mode 100644 index 000000000..e1521d8fd --- /dev/null +++ b/verify_external/src/convert.verus.rs @@ -0,0 +1,79 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou +use vstd::prelude::*; +verus! { + +pub broadcast group convert_group { + axiom_from_spec, +} + +pub trait FromSpec: Sized { + spec fn from_spec(v: T) -> Self; +} + +macro_rules! def_primitive_from{ + ($toty: ty, $($fromty: ty),*) => { + $(verus!{ + impl FromSpec<$fromty> for $toty { + open spec fn from_spec(v: $fromty) -> Self { + v as $toty + } + }})* + } +} + +def_primitive_from!{u16, u8, u16} + +def_primitive_from!{u32, u8, u16, u32} + +def_primitive_from!{u64, u8, u16, u32, usize} + +def_primitive_from!{usize, u8, u16, u32, usize} + +pub open spec fn from_spec(v: T1) -> T2; + +#[verifier(inline)] +pub open spec fn default_into_spec>(v: T) -> U { + from_spec(v) +} + +#[verifier(external_body)] +pub broadcast proof fn axiom_from_spec>(v: T) + ensures + #[trigger] from_spec::(v) === U::from_spec(v), +{ +} + +#[verifier::external_trait_specification] +pub trait ExInto: Sized { + type ExternalTraitSpecificationFor: core::convert::Into; + + fn into(self) -> (ret: T) + ensures + from_spec(self) === ret, + ; +} + +#[verifier::external_trait_specification] +pub trait ExFrom: Sized { + type ExternalTraitSpecificationFor: core::convert::From; + + fn from(v: T) -> (ret: Self) + ensures + from_spec(v) === ret, + ; +} + +#[verifier::external_fn_specification] +#[verifier::when_used_as_spec(default_into_spec)] +pub fn ex_into>(a: T) -> (ret: U) + ensures + ret === from_spec(a), +{ + a.into() +} + +} // verus! diff --git a/verify_external/src/lib.rs b/verify_external/src/lib.rs new file mode 100644 index 000000000..ea2338b73 --- /dev/null +++ b/verify_external/src/lib.rs @@ -0,0 +1,31 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou +// +// Goal: This crate provides specifications for external, unverified libraries. +// These specifications are placeholders, and the number of verification targets +// should always remain zero since these libraries are not formally verified. +// Why: While vstd defines some specifications for std/core, these are +// incomplete. SVSM may also rely on other unverified crates, which necessitates +// these specifications. + +#![no_std] +#![allow(unused_braces)] +#![allow(unexpected_cfgs)] + +// Add spec for convert traits +pub mod convert; + +#[cfg(verus_keep_ghost)] +include!("vstd.verus.rs"); + +use builtin_macros::*; + +verus! { +#[cfg_attr(verus_keep_ghost, verifier::broadcast_use_by_default_when_this_crate_is_imported)] +pub broadcast group external_axiom { + convert::convert_group +} +} diff --git a/verify_external/src/vstd.verus.rs b/verify_external/src/vstd.verus.rs new file mode 100644 index 000000000..01fb66e20 --- /dev/null +++ b/verify_external/src/vstd.verus.rs @@ -0,0 +1,43 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou +use vstd::prelude::*; +verus! { + +#[verifier::external_fn_specification] +pub fn ex_map U>(a: Option, f: F) -> (ret: Option) + requires + a.is_some() ==> call_requires(f, (a.unwrap(),)), + ensures + ret.is_some() ==> a.is_some(), + ret.is_some() ==> call_ensures(f, (a.unwrap(),), ret.unwrap()), +{ + a.map(f) +} + +} // verus! +macro_rules! num_specs { + ($uN:ty) => { + verus! { + pub open spec fn saturating_add(x: $uN, y: $uN) -> $uN { + if x + y > <$uN>::MAX { + <$uN>::MAX + } else { + (x + y) as $uN + } + } + + #[verifier::external_fn_specification] + #[verifier::when_used_as_spec(saturating_add)] + pub fn ex_saturating_add(x: $uN, y: $uN) -> (res: $uN) + ensures res == saturating_add(x, y) + { + x.saturating_add(y) + } + } + }; +} + +num_specs! {usize} diff --git a/verismo/Cargo.toml b/verify_proof/Cargo.toml similarity index 94% rename from verismo/Cargo.toml rename to verify_proof/Cargo.toml index e41c3d193..bee3b9066 100644 --- a/verismo/Cargo.toml +++ b/verify_proof/Cargo.toml @@ -1,5 +1,5 @@ [package] -name = "verismo" +name = "verify_proof" version = "0.1.0" edition = "2021" diff --git a/verify_proof/build.rs b/verify_proof/build.rs new file mode 100644 index 000000000..e51606f27 --- /dev/null +++ b/verify_proof/build.rs @@ -0,0 +1,27 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou + +fn main() { + init_verify(); +} + +fn init_verify() { + if cfg!(feature = "noverify") { + println!("cargo:rustc-env=VERUS_ARGS=--no-verify"); + } else { + // Set rlimit higher here for expensive but reusable proofs. + let verus_args = [ + "--rlimit=4", + "--expand-errors", + "--multiple-errors=5", + "--triggers-silent", + "--no-auto-recommends-check", + "--trace", + "-Z unstable-options", + ]; + println!("cargo:rustc-env=VERUS_ARGS={}", verus_args.join(" ")); + } +} diff --git a/verismo/src/bits.rs b/verify_proof/src/bits.rs similarity index 100% rename from verismo/src/bits.rs rename to verify_proof/src/bits.rs diff --git a/verify_proof/src/bits.verus.rs b/verify_proof/src/bits.verus.rs new file mode 100644 index 000000000..31295bac8 --- /dev/null +++ b/verify_proof/src/bits.verus.rs @@ -0,0 +1,387 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou +use vstd::arithmetic::power2::pow2; +use vstd::bits::low_bits_mask; +use vstd::prelude::*; + +#[macro_export] +macro_rules! POW2_VALUE { + (0) => { + 0x1u64 + }; + (1) => { + 0x2u64 + }; + (2) => { + 0x4u64 + }; + (3) => { + 0x8u64 + }; + (4) => { + 0x10u64 + }; + (5) => { + 0x20u64 + }; + (6) => { + 0x40u64 + }; + (7) => { + 0x80u64 + }; + (8) => { + 0x100u64 + }; + (9) => { + 0x200u64 + }; + (10) => { + 0x400u64 + }; + (11) => { + 0x800u64 + }; + (12) => { + 0x1000u64 + }; + (13) => { + 0x2000u64 + }; + (14) => { + 0x4000u64 + }; + (15) => { + 0x8000u64 + }; + (16) => { + 0x10000u64 + }; + (17) => { + 0x20000u64 + }; + (18) => { + 0x40000u64 + }; + (19) => { + 0x80000u64 + }; + (20) => { + 0x100000u64 + }; + (21) => { + 0x200000u64 + }; + (22) => { + 0x400000u64 + }; + (23) => { + 0x800000u64 + }; + (24) => { + 0x1000000u64 + }; + (25) => { + 0x2000000u64 + }; + (26) => { + 0x4000000u64 + }; + (27) => { + 0x8000000u64 + }; + (28) => { + 0x10000000u64 + }; + (29) => { + 0x20000000u64 + }; + (30) => { + 0x40000000u64 + }; + (31) => { + 0x80000000u64 + }; + (32) => { + 0x100000000u64 + }; + (33) => { + 0x200000000u64 + }; + (34) => { + 0x400000000u64 + }; + (35) => { + 0x800000000u64 + }; + (36) => { + 0x1000000000u64 + }; + (37) => { + 0x2000000000u64 + }; + (38) => { + 0x4000000000u64 + }; + (39) => { + 0x8000000000u64 + }; + (40) => { + 0x10000000000u64 + }; + (41) => { + 0x20000000000u64 + }; + (42) => { + 0x40000000000u64 + }; + (43) => { + 0x80000000000u64 + }; + (44) => { + 0x100000000000u64 + }; + (45) => { + 0x200000000000u64 + }; + (46) => { + 0x400000000000u64 + }; + (47) => { + 0x800000000000u64 + }; + (48) => { + 0x1000000000000u64 + }; + (49) => { + 0x2000000000000u64 + }; + (50) => { + 0x4000000000000u64 + }; + (51) => { + 0x8000000000000u64 + }; + (52) => { + 0x10000000000000u64 + }; + (53) => { + 0x20000000000000u64 + }; + (54) => { + 0x40000000000000u64 + }; + (55) => { + 0x80000000000000u64 + }; + (56) => { + 0x100000000000000u64 + }; + (57) => { + 0x200000000000000u64 + }; + (58) => { + 0x400000000000000u64 + }; + (59) => { + 0x800000000000000u64 + }; + (60) => { + 0x1000000000000000u64 + }; + (61) => { + 0x2000000000000000u64 + }; + (62) => { + 0x4000000000000000u64 + }; + (63) => { + 0x8000000000000000u64 + }; + ($_:expr) => { + 0u64 + }; +} + +verus! { + +#[verifier(inline)] +pub open spec fn bit_value(n: u64) -> u64 + recommends + n < 64, +{ + seq_macro::seq! { N in 1..64 { + if n == 0 { + POW2_VALUE!(0) + } + #(else if n == N { + POW2_VALUE!(N) + })* + else { + 0 + } +} +} +} + +} // verus! +verus! { + +pub open spec fn is_pow_of_2(val: u64) -> bool { + seq_macro::seq! {N in 0..64 {#( + val == 1u64 << N || + )* false + }} +} + +#[verifier(inline)] +pub open spec fn pow2_to_bits(val: u64) -> u64 { + choose|ret: u64| (1u64 << ret) == val && 0 <= ret < 64 +} + +} // verus! +#[rustfmt::skip] +macro_rules! bit_shl_values { + ($typ:ty, $styp:ty, $one: expr, $pname: ident) => { + seq_macro::seq! {N in 0..64 {verus! { + #[doc = "Proof that shifting 1 by N has a bound."] + pub broadcast proof fn $pname() + ensures + #( + N < $styp::BITS ==> ($one << N) == POW2_VALUE!(N), + )* + { + #(assert($one << N == POW2_VALUE!(N)) by(compute_only);)* + } + } +}} + }; +} + +macro_rules! bit_not_properties { + ($typ:ty, $styp:ty, $sname: ident, $autopname: ident) => { + verus! { + #[doc = "Proof that !a is equal to max - a, and !!a == a"] + pub broadcast proof fn $autopname(a: $typ) + ensures + #[trigger]!a == sub($styp::MAX as $typ, a), + !(!a) == a, + { + assert(!(!a) == a) by(bit_vector); + assert((!a) == $styp::MAX - a) by(bit_vector); + } + } + }; +} + +macro_rules! bit_set_clear_mask { + ($typ:ty, $styp:ty, $pname_or_mask: ident, $pname_and_mask: ident) => { + verus! { + #[doc = "Proof that a mask m is set with or operation."] + #[verifier(bit_vector)] + pub broadcast proof fn $pname_or_mask(a: $typ, m: $typ) + ensures + (#[trigger](a | m)) & m == m, + (a | m) & (!m) == a & (!m), + a | m >= a, + a | m >= m, + a == (a|m) - m + (a|!m) - !m + {} + + #[doc = "Proof that a mask m is cleared with and operation."] + #[verifier(bit_vector)] + pub broadcast proof fn $pname_and_mask(a: $typ, m: $typ) + ensures + (#[trigger](a & m)) & !m == 0, + (a & m) & m == a & m, + a & m <= m, + a & m <= a, + a == add(a & m, a & !m), + {} + } + }; +} + +verus! { + +pub broadcast proof fn lemma_bit_u64_and_mask_is_mod(x: u64, mask: u64) + requires + mask < u64::MAX, + is_pow_of_2((mask + 1) as u64), + ensures + #[trigger] (x & mask) == x as int % (mask + 1), +{ + broadcast use lemma_bit_u64_shl_values; + broadcast use vstd::bits::lemma_u64_pow2_no_overflow; + + let align = mask + 1; + let bit = pow2_to_bits(align as u64) as nat; + assert(1u64 << bit == pow2(bit)) by { + broadcast use vstd::bits::lemma_u64_shl_is_mul; + + } + assert(mask == low_bits_mask(bit)); + assert(x & (low_bits_mask(bit) as u64) == x as nat % (pow2(bit))) by { + broadcast use vstd::bits::lemma_u64_low_bits_mask_is_mod; + + } +} + +} // verus! +macro_rules! bit_and_mask_is_mod { + ($typ:ty, $pname: ident) => { + verus! { + pub broadcast proof fn $pname(x: $typ, mask: $typ) + requires + mask < $typ::MAX, + is_pow_of_2((mask + 1) as u64), + ensures + #[trigger] (x & mask) == (x as int) % (mask + 1), + { + lemma_bit_u64_and_mask_is_mod(x as u64, mask as u64); + } + } + }; +} + +bit_shl_values! {u64, u64, 1u64, lemma_bit_u64_shl_values} +bit_not_properties! {u64, u64, spec_bit_u64_not_properties, lemma_bit_u64_not_is_sub} +bit_set_clear_mask! {u64, u64, lemma_bit_u64_or_mask, lemma_bit_u64_and_mask} + +bit_shl_values! {usize, u64, 1usize, lemma_bit_usize_shl_values} +bit_not_properties! {usize, u64, spec_bit_usize_not_properties, lemma_bit_usize_not_is_sub} +bit_set_clear_mask! {usize, u64, lemma_bit_usize_or_mask, lemma_bit_usize_and_mask} +bit_and_mask_is_mod! {usize, lemma_bit_usize_and_mask_is_mod} + +verus! { + +pub broadcast proof fn lemma_pow2_eq_bit_value(n: nat) + requires + n < u64::BITS, + ensures + bit_value(n as u64) == #[trigger] pow2(n), + decreases n, +{ + vstd::arithmetic::power2::lemma2_to64(); + if n > 0 { + vstd::arithmetic::power2::lemma_pow2_unfold(n); + } + if n > 32 { + lemma_pow2_eq_bit_value((n - 1) as nat); + } +} + +pub broadcast proof fn lemma_bit_usize_shr_is_div(v: usize, n: usize) + requires + n < usize::BITS, + ensures + (#[trigger] (v >> n)) == v as int / bit_value(n as u64) as int, +{ + vstd::bits::lemma_u64_shr_is_div(v as u64, n as u64); + lemma_pow2_eq_bit_value(n as nat); +} + +} // verus! diff --git a/verismo/src/lib.rs b/verify_proof/src/lib.rs similarity index 77% rename from verismo/src/lib.rs rename to verify_proof/src/lib.rs index 5777b0d1f..cc39bd5bf 100644 --- a/verismo/src/lib.rs +++ b/verify_proof/src/lib.rs @@ -7,6 +7,12 @@ #![no_std] #![allow(unused_braces)] #![allow(unexpected_cfgs)] +use builtin_macros::*; pub mod bits; -pub mod layout; + +verus! { + +global size_of usize == 8; + +} diff --git a/verismo/src/bits.verus.rs b/verismo/src/bits.verus.rs deleted file mode 100644 index 9106127b9..000000000 --- a/verismo/src/bits.verus.rs +++ /dev/null @@ -1,221 +0,0 @@ -// SPDX-License-Identifier: MIT OR Apache-2.0 -// -// Copyright (c) Microsoft Corporation -// -// Author: Ziqiao Zhou -use vstd::prelude::*; - -verus! { - -#[verifier(inline)] -pub open spec fn bit_value(n: u64) -> u64 - recommends - n < 64, -{ - if n == 0 { - 0x1 - } else if n == 1 { - 0x2 - } else if n == 2 { - 0x4 - } else if n == 3 { - 0x8 - } else if n == 4 { - 0x10 - } else if n == 5 { - 0x20 - } else if n == 6 { - 0x40 - } else if n == 7 { - 0x80 - } else if n == 8 { - 0x100 - } else if n == 9 { - 0x200 - } else if n == 10 { - 0x400 - } else if n == 11 { - 0x800 - } else if n == 12 { - 0x1000 - } else if n == 13 { - 0x2000 - } else if n == 14 { - 0x4000 - } else if n == 15 { - 0x8000 - } else if n == 16 { - 0x10000 - } else if n == 17 { - 0x20000 - } else if n == 18 { - 0x40000 - } else if n == 19 { - 0x80000 - } else if n == 20 { - 0x100000 - } else if n == 21 { - 0x200000 - } else if n == 22 { - 0x400000 - } else if n == 23 { - 0x800000 - } else if n == 24 { - 0x1000000 - } else if n == 25 { - 0x2000000 - } else if n == 26 { - 0x4000000 - } else if n == 27 { - 0x8000000 - } else if n == 28 { - 0x10000000 - } else if n == 29 { - 0x20000000 - } else if n == 30 { - 0x40000000 - } else if n == 31 { - 0x80000000 - } else if n == 32 { - 0x100000000 - } else if n == 33 { - 0x200000000 - } else if n == 34 { - 0x400000000 - } else if n == 35 { - 0x800000000 - } else if n == 36 { - 0x1000000000 - } else if n == 37 { - 0x2000000000 - } else if n == 38 { - 0x4000000000 - } else if n == 39 { - 0x8000000000 - } else if n == 40 { - 0x10000000000 - } else if n == 41 { - 0x20000000000 - } else if n == 42 { - 0x40000000000 - } else if n == 43 { - 0x80000000000 - } else if n == 44 { - 0x100000000000 - } else if n == 45 { - 0x200000000000 - } else if n == 46 { - 0x400000000000 - } else if n == 47 { - 0x800000000000 - } else if n == 48 { - 0x1000000000000 - } else if n == 49 { - 0x2000000000000 - } else if n == 50 { - 0x4000000000000 - } else if n == 51 { - 0x8000000000000 - } else if n == 52 { - 0x10000000000000 - } else if n == 53 { - 0x20000000000000 - } else if n == 54 { - 0x40000000000000 - } else if n == 55 { - 0x80000000000000 - } else if n == 56 { - 0x100000000000000 - } else if n == 57 { - 0x200000000000000 - } else if n == 58 { - 0x400000000000000 - } else if n == 59 { - 0x800000000000000 - } else if n == 60 { - 0x1000000000000000 - } else if n == 61 { - 0x2000000000000000 - } else if n == 62 { - 0x4000000000000000 - } else if n == 63 { - 0x8000000000000000 - } else { - 0 - } -} - -pub open spec fn is_pow_of_2(val: u64) -> bool { - seq_macro::seq! {N in 0..63 {#( - val == bit_value(N) || - )* false - }} -} - -} // verus! -macro_rules! bit_shl_values { - ($typ:ty, $styp:ty, $one: expr, $pname: ident) => { - verus! { - #[doc = "Proof that shifting 1 by N has a bound."] - pub broadcast proof fn $pname(offset: $typ) - requires 0 <= offset < $styp::BITS - ensures - #[trigger]($one << offset) == bit_value(offset as u64), - { - assert($one << offset == bit_value(offset as u64)) by(bit_vector); - } - } - }; -} - -macro_rules! bit_not_properties { - ($typ:ty, $styp:ty, $sname: ident, $autopname: ident) => { - verus! { - #[doc = "Proof that !a is equal to max - a, and !!a == a"] - pub broadcast proof fn $autopname(a: $typ) - ensures - #[trigger]!a == sub($styp::MAX as $typ, a), - !(!a) == a, - { - assert(!(!a) == a) by(bit_vector); - assert((!a) == $styp::MAX - a) by(bit_vector); - } - } - }; -} - -macro_rules! bit_set_clear_mask { - ($typ:ty, $styp:ty, $pname_or_mask: ident, $pname_and_mask: ident) => { - verus! { - #[doc = "Proof that a mask m is set with or operation."] - #[verifier(bit_vector)] - pub broadcast proof fn $pname_or_mask(a: $typ, m: $typ) - ensures - (#[trigger](a | m)) & m == m, - (a | m) & (!m) == a & (!m), - a | m >= a, - a | m >= m, - a == (a|m) - m + (a|!m) - !m - {} - - #[doc = "Proof that a mask m is cleared with and operation."] - #[verifier(bit_vector)] - pub broadcast proof fn $pname_and_mask(a: $typ, m: $typ) - ensures - (#[trigger](a & m)) & !m == 0, - (a & m) & m == a & m, - a & m <= m, - a & m <= a, - a == add(a & m, a & !m), - {} - } - }; -} - -bit_shl_values! {u64, u64, 1u64, lemma_bit_u64_shl_values} -bit_not_properties! {u64, u64, spec_bit_u64_not_properties, lemma_bit_u64_not_is_sub} -bit_set_clear_mask! {u64, u64, lemma_bit_u64_or_mask, lemma_bit_u64_and_mask} - -bit_shl_values! {usize, u64, 1usize, lemma_bit_usize_shl_values} -bit_not_properties! {usize, u64, spec_bit_usize_not_properties, lemma_bit_usize_not_is_sub} -bit_set_clear_mask! {usize, u64, lemma_bit_usize_or_mask, lemma_bit_usize_and_mask} From ce8d7bf5cd8e8145aa2d14f68983dbdd9ae29e75 Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Fri, 25 Oct 2024 11:46:52 -0700 Subject: [PATCH 3/8] Improve the bit_value. (#3) Simplify the seq_macros Refine the specification for Option::map Signed-off-by: Ziqiao Zhou --- verify_external/src/vstd.verus.rs | 2 +- verify_proof/src/bits.verus.rs | 11 ++++------- 2 files changed, 5 insertions(+), 8 deletions(-) diff --git a/verify_external/src/vstd.verus.rs b/verify_external/src/vstd.verus.rs index 01fb66e20..18e7dabc7 100644 --- a/verify_external/src/vstd.verus.rs +++ b/verify_external/src/vstd.verus.rs @@ -11,7 +11,7 @@ pub fn ex_map U>(a: Option, f: F) -> (ret: Option) requires a.is_some() ==> call_requires(f, (a.unwrap(),)), ensures - ret.is_some() ==> a.is_some(), + ret.is_some() == a.is_some(), ret.is_some() ==> call_ensures(f, (a.unwrap(),), ret.unwrap()), { a.map(f) diff --git a/verify_proof/src/bits.verus.rs b/verify_proof/src/bits.verus.rs index 31295bac8..6c6f0b77b 100644 --- a/verify_proof/src/bits.verus.rs +++ b/verify_proof/src/bits.verus.rs @@ -213,14 +213,11 @@ pub open spec fn bit_value(n: u64) -> u64 recommends n < 64, { - seq_macro::seq! { N in 1..64 { - if n == 0 { - POW2_VALUE!(0) - } - #(else if n == N { + seq_macro::seq! { N in 0..64 { + #(if n == N { POW2_VALUE!(N) - })* - else { + } else)* + { 0 } } From 8681b35eaa05cac98bd6e58f1996b8ad44ca30ce Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Wed, 30 Oct 2024 09:59:33 -0700 Subject: [PATCH 4/8] Upgrade to Rust-1.82 (#4) * Upgrade verus to support v1.82. * Cleanup build.rs * Set verus lib and tool to the rev supporting v1.82 Signed-off-by: Ziqiao Zhou * Move vstd.verus.rs to verus vstd & mark memory-related as external * memory related verification needs to add a memory permission and will do it later Signed-off-by: Ziqiao Zhou * Revert unnecessary change after verus upgrade * revert rust version * revert some code due to version change Signed-off-by: Ziqiao Zhou * fmt --------- Signed-off-by: Ziqiao Zhou --- Cargo.lock | 66 +++++++++++++++---------------- Cargo.toml | 6 +-- kernel/Cargo.toml | 2 +- kernel/build.rs | 28 +++++-------- kernel/src/address.rs | 5 +++ kernel/src/address.verus.rs | 2 +- kernel/src/lib.rs | 2 - kernel/src/mm/page_visibility.rs | 8 ++-- kernel/src/svsm.rs | 2 +- scripts/vinstall.sh | 4 +- verify_external/src/lib.rs | 3 -- verify_external/src/vstd.verus.rs | 43 -------------------- 12 files changed, 59 insertions(+), 112 deletions(-) delete mode 100644 verify_external/src/vstd.verus.rs diff --git a/Cargo.lock b/Cargo.lock index 03c829da0..e49d79a19 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -39,9 +39,9 @@ dependencies = [ [[package]] name = "anstream" -version = "0.6.15" +version = "0.6.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "64e15c1ab1f89faffbf04a634d5e1962e9074f2741eef6d97f3c4e322426d526" +checksum = "23a1e53f0f5d86382dafe1cf314783b2044280f406e7e1506368220ad11b1338" dependencies = [ "anstyle", "anstyle-parse", @@ -54,33 +54,33 @@ dependencies = [ [[package]] name = "anstyle" -version = "1.0.8" +version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1bec1de6f59aedf83baf9ff929c98f2ad654b97c9510f4e70cf6f661d49fd5b1" +checksum = "8365de52b16c035ff4fcafe0092ba9390540e3e352870ac09933bebcaa2c8c56" [[package]] name = "anstyle-parse" -version = "0.2.5" +version = "0.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eb47de1e80c2b463c735db5b217a0ddc39d612e7ac9e2e96a5aed1f57616c1cb" +checksum = "3b2d16507662817a6a20a9ea92df6652ee4f94f914589377d69f3b21bc5798a9" dependencies = [ "utf8parse", ] [[package]] name = "anstyle-query" -version = "1.1.1" +version = "1.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6d36fc52c7f6c869915e99412912f22093507da8d9e942ceaf66fe4b7c14422a" +checksum = "79947af37f4177cfead1110013d678905c37501914fba0efea834c3fe9a8d60c" dependencies = [ "windows-sys", ] [[package]] name = "anstyle-wincon" -version = "3.0.4" +version = "3.0.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5bf74e1b6e971609db8ca7a9ce79fd5768ab6ae46441c572e46cf596f59e57f8" +checksum = "2109dbce0e72be3ec00bed26e6a7479ca384ad226efdd66db8fa2e3a38c83125" dependencies = [ "anstyle", "windows-sys", @@ -127,7 +127,7 @@ checksum = "adc0846593a56638b74e136a45610f9934c052e14761bebca6b092d5522599e3" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.85", ] [[package]] @@ -138,7 +138,7 @@ checksum = "6c2ce686adbebce0ee484a502c440b4657739adbad65eadf06d64f5816ee9765" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.85", ] [[package]] @@ -172,12 +172,12 @@ dependencies = [ [[package]] name = "builtin" version = "0.1.0" -source = "git+https://github.com/verus-lang/verus?rev=2776465#27764656a55aa214134f79187aac28435ae52ebc" +source = "git+https://github.com/verus-lang/verus?rev=31a272f#31a272f54dd2cce746eb64c54b05be0f825deddf" [[package]] name = "builtin_macros" version = "0.1.0" -source = "git+https://github.com/verus-lang/verus?rev=2776465#27764656a55aa214134f79187aac28435ae52ebc" +source = "git+https://github.com/verus-lang/verus?rev=31a272f#31a272f54dd2cce746eb64c54b05be0f825deddf" dependencies = [ "prettyplease_verus", "proc-macro2", @@ -251,7 +251,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.85", ] [[package]] @@ -262,9 +262,9 @@ checksum = "1462739cb27611015575c0c11df5df7601141071f07518d56fcc1be504cbec97" [[package]] name = "colorchoice" -version = "1.0.2" +version = "1.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0" +checksum = "5b63caa9aa9397e2d9480a9b13673856c78d8ac123288526c37d7839f2a86990" [[package]] name = "const-oid" @@ -348,7 +348,7 @@ checksum = "67e77553c4162a157adbf834ebae5b415acbecbeafc7a74b0e886657506a7611" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.85", ] [[package]] @@ -715,7 +715,7 @@ checksum = "8d1296fab5231654a5aec8bf9e87ba4e3938c502fc4c3c0425a00084c78944be" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.85", ] [[package]] @@ -755,9 +755,9 @@ dependencies = [ [[package]] name = "pin-project-lite" -version = "0.2.14" +version = "0.2.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02" +checksum = "915a1e146535de9163f3987b8944ed8cf49a18bb0056bcebcdcece385cece4ff" [[package]] name = "pkcs8" @@ -784,7 +784,7 @@ dependencies = [ [[package]] name = "prettyplease_verus" version = "0.1.15" -source = "git+https://github.com/verus-lang/verus?rev=2776465#27764656a55aa214134f79187aac28435ae52ebc" +source = "git+https://github.com/verus-lang/verus?rev=31a272f#31a272f54dd2cce746eb64c54b05be0f825deddf" dependencies = [ "proc-macro2", "syn_verus", @@ -958,7 +958,7 @@ dependencies = [ [[package]] name = "state_machines_macros" version = "0.1.0" -source = "git+https://github.com/verus-lang/verus?rev=2776465#27764656a55aa214134f79187aac28435ae52ebc" +source = "git+https://github.com/verus-lang/verus?rev=31a272f#31a272f54dd2cce746eb64c54b05be0f825deddf" dependencies = [ "indexmap", "proc-macro2", @@ -1035,9 +1035,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.82" +version = "2.0.85" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "83540f837a8afc019423a8edb95b52a8effe46957ee402287f4292fae35be021" +checksum = "5023162dfcd14ef8f32034d8bcd4cc5ddc61ef7a247c024a33e24e1f24d21b56" dependencies = [ "proc-macro2", "quote", @@ -1047,7 +1047,7 @@ dependencies = [ [[package]] name = "syn_verus" version = "1.0.95" -source = "git+https://github.com/verus-lang/verus?rev=2776465#27764656a55aa214134f79187aac28435ae52ebc" +source = "git+https://github.com/verus-lang/verus?rev=31a272f#31a272f54dd2cce746eb64c54b05be0f825deddf" dependencies = [ "proc-macro2", "quote", @@ -1104,7 +1104,7 @@ checksum = "ae71770322cbd277e69d762a16c444af02aa0575ac0d174f0b9562d3b37f8602" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.85", ] [[package]] @@ -1126,7 +1126,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.85", ] [[package]] @@ -1213,7 +1213,7 @@ checksum = "442887c63f2c839b346c192d047a7c87e73d0689c9157b00b53dcc27dd5ea793" [[package]] name = "vstd" version = "0.1.0" -source = "git+https://github.com/verus-lang/verus?rev=2776465#27764656a55aa214134f79187aac28435ae52ebc" +source = "git+https://github.com/verus-lang/verus?rev=31a272f#31a272f54dd2cce746eb64c54b05be0f825deddf" dependencies = [ "builtin", "builtin_macros", @@ -1228,9 +1228,9 @@ checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" [[package]] name = "windows-sys" -version = "0.52.0" +version = "0.59.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" +checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" dependencies = [ "windows-targets", ] @@ -1338,7 +1338,7 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.85", ] [[package]] @@ -1349,7 +1349,7 @@ checksum = "2e5f54f3cc93cd80745404626681b4b9fca9a867bad5a8424b618eb0db1ae6ea" dependencies = [ "proc-macro2", "quote", - "syn 2.0.82", + "syn 2.0.85", ] [[package]] diff --git a/Cargo.toml b/Cargo.toml index c68b9d9a3..de2c67080 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -54,9 +54,9 @@ zerocopy = { version = "0.8.2", features = ["alloc", "derive"] } packit = { git = "https://github.com/coconut-svsm/packit", version = "0.1.1" } # Verus repos -builtin = { git = "https://github.com/verus-lang/verus", rev ="2776465", default-features = false } -builtin_macros = { git = "https://github.com/verus-lang/verus", rev ="2776465", default-features = false } -vstd = { git = "https://github.com/verus-lang/verus", rev ="2776465", features = ["alloc"], default-features = false } +builtin = { git = "https://github.com/verus-lang/verus", rev ="31a272f", default-features = false } +builtin_macros = { git = "https://github.com/verus-lang/verus", rev ="31a272f", default-features = false } +vstd = { git = "https://github.com/verus-lang/verus", rev ="31a272f", features = ["alloc"], default-features = false } # Verification libs verify_proof = { path = "verify_proof", default-features = false } diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml index 24c937b88..6be02f5d7 100644 --- a/kernel/Cargo.toml +++ b/kernel/Cargo.toml @@ -2,7 +2,7 @@ name = "svsm" version = "0.1.0" edition = "2021" -rust-version = "1.77.0" +rust-version = "1.82.0" [[bin]] name = "stage2" diff --git a/kernel/build.rs b/kernel/build.rs index a87372b27..692970f76 100644 --- a/kernel/build.rs +++ b/kernel/build.rs @@ -4,27 +4,17 @@ // // Author: Joerg Roedel -use rustc_version::{Channel, Version}; - fn main() { - let rust_version = rustc_version::version_meta().unwrap(); - // Check if the version is nightly and higher than 1.78.0 - let is_expected_version = rust_version.semver >= Version::new(1, 78, 0); - if !is_expected_version { - if rust_version.channel == Channel::Nightly { - // Print the cargo:rustc-cfg directive to enable the feature - println!("cargo:rustc-cfg=RUST_BEFORE_1_78"); - } else { - // Optionally handle the case for non-nightly versions - panic!("Requires the nightly version or stable version >= 1.78."); - } - } else { - // Extra cfgs - println!("cargo::rustc-check-cfg=cfg(fuzzing)"); - println!("cargo::rustc-check-cfg=cfg(test_in_svsm)"); - println!("cargo::rustc-check-cfg=cfg(verus_keep_ghost)"); - println!("cargo::rustc-check-cfg=cfg(RUST_BEFORE_1_78)"); + // Verification tool only support rust version lower than 1.82 + // If new features are used, may need to disable them until verus is upraded. + if rustc_version::version_meta().unwrap().semver > rustc_version::Version::new(1, 80, 2) { + println!("cargo:rustc-cfg=RUST_VERSION_AFTER_VERUS"); } + // Extra cfgs + println!("cargo::rustc-check-cfg=cfg(fuzzing)"); + println!("cargo::rustc-check-cfg=cfg(test_in_svsm)"); + println!("cargo::rustc-check-cfg=cfg(verus_keep_ghost)"); + println!("cargo::rustc-check-cfg=cfg(RUST_VERSION_AFTER_VERUS)"); // Stage 2 println!("cargo:rustc-link-arg-bin=stage2=-nostdlib"); diff --git a/kernel/src/address.rs b/kernel/src/address.rs index 4274d555f..3a68d4b85 100644 --- a/kernel/src/address.rs +++ b/kernel/src/address.rs @@ -268,11 +268,13 @@ impl VirtAddr { } #[inline] + #[verus_verify(external_body)] pub fn as_ptr(&self) -> *const T { self.0 as *const T } #[inline] + #[verus_verify(external_body)] pub fn as_mut_ptr(&self) -> *mut T { self.0 as *mut T } @@ -285,6 +287,7 @@ impl VirtAddr { /// All safety requirements for pointers apply, minus alignment and NULL /// checks, which this function already does. #[inline] + #[verus_verify(external_body)] pub unsafe fn aligned_ref<'a, T>(&self) -> Option<&'a T> { self.is_aligned_to::() .then(|| self.as_ptr::().as_ref()) @@ -299,6 +302,7 @@ impl VirtAddr { /// All safety requirements for pointers apply, minus alignment and NULL /// checks, which this function already does. #[inline] + #[verus_verify(external)] pub unsafe fn aligned_mut<'a, T>(&self) -> Option<&'a mut T> { self.is_aligned_to::() .then(|| self.as_mut_ptr::().as_mut()) @@ -327,6 +331,7 @@ impl VirtAddr { /// /// All Safety requirements from [`core::slice::from_raw_parts`] for the /// data pointed to by the `VirtAddr` apply here as well. + #[verus_verify(external_body)] pub unsafe fn to_slice(&self, len: usize) -> &[T] { slice::from_raw_parts::(self.as_ptr::(), len) } diff --git a/kernel/src/address.verus.rs b/kernel/src/address.verus.rs index 89e856ab6..ca5211e13 100644 --- a/kernel/src/address.verus.rs +++ b/kernel/src/address.verus.rs @@ -34,9 +34,9 @@ broadcast group vaddr_impl_proof { } broadcast use vaddr_impl_proof; + /// Define a broadcast function and its related spec function calls in a inner /// module to avoid cyclic self-reference - mod address_spec { include!("address_inner.verus.rs"); } #[cfg(verus_keep_ghost)] diff --git a/kernel/src/lib.rs b/kernel/src/lib.rs index 187853e78..250b94e0b 100644 --- a/kernel/src/lib.rs +++ b/kernel/src/lib.rs @@ -5,8 +5,6 @@ // Author: Nicolai Stange #![no_std] -#![cfg_attr(RUST_BEFORE_1_78, feature(offset_of))] // stable feature after v1.78 but nightly feature in v1.77 -#![cfg_attr(RUST_BEFORE_1_78, feature(inline_const))] // stable feature in v1.78 but nightly feature in v1.77 #![cfg_attr(all(test, test_in_svsm), no_main)] #![cfg_attr(all(test, test_in_svsm), feature(custom_test_frameworks))] #![cfg_attr(all(test, test_in_svsm), test_runner(crate::testing::svsm_test_runner))] diff --git a/kernel/src/mm/page_visibility.rs b/kernel/src/mm/page_visibility.rs index 039c5619e..f442cb3d9 100644 --- a/kernel/src/mm/page_visibility.rs +++ b/kernel/src/mm/page_visibility.rs @@ -131,7 +131,7 @@ impl SharedBox { copy_bytes( self.ptr.as_ptr() as usize, out as *const T as usize, - core::mem::size_of::(), + size_of::(), ); } } @@ -146,7 +146,7 @@ impl SharedBox { copy_bytes( value as *const T as usize, self.ptr.as_ptr() as usize, - core::mem::size_of::(), + size_of::(), ); } } @@ -171,7 +171,7 @@ impl SharedBox<[T; N]> { unsafe { // SAFETY: `self.ptr` is valid and we did a bounds check on `n`. - write_bytes(self.ptr.as_ptr() as usize, core::mem::size_of::() * n, 0); + write_bytes(self.ptr.as_ptr() as usize, size_of::() * n, 0); } Ok(()) @@ -206,7 +206,7 @@ unsafe impl Sync for SharedBox where T: Sync {} impl Drop for SharedBox { fn drop(&mut self) { // Re-encrypt the pages. - let res = (0..core::mem::size_of::()) + let res = (0..size_of::()) .step_by(PAGE_SIZE) .try_for_each(|offset| unsafe { make_page_private(self.addr() + offset) }); diff --git a/kernel/src/svsm.rs b/kernel/src/svsm.rs index 7b2c946cc..9126ee690 100755 --- a/kernel/src/svsm.rs +++ b/kernel/src/svsm.rs @@ -96,7 +96,7 @@ global_asm!( static CPUID_PAGE: ImmutAfterInitCell = ImmutAfterInitCell::uninit(); static LAUNCH_INFO: ImmutAfterInitCell = ImmutAfterInitCell::uninit(); -const _: () = assert!(core::mem::size_of::() <= PAGE_SIZE); +const _: () = assert!(size_of::() <= PAGE_SIZE); fn copy_cpuid_table_to_fw(fw_addr: PhysAddr) -> Result<(), SvsmError> { let guard = PerCPUPageMappingGuard::create_4k(fw_addr)?; diff --git a/scripts/vinstall.sh b/scripts/vinstall.sh index 67cf2a4da..1c6673c7b 100755 --- a/scripts/vinstall.sh +++ b/scripts/vinstall.sh @@ -1,5 +1,5 @@ #!/bin/bash -VERISMO_REV=7c9c445 +VERISMO_REV=5186244 cargo install --git https://github.com/microsoft/verismo/ --rev $VERISMO_REV cargo-v builtin=`cargo metadata --format-version 1 | jq -r '.packages[] | select(.name == "builtin_macros") | .targets[].src_path'` verus=`dirname $builtin`/../../../source/target-verus/release/verus @@ -9,5 +9,5 @@ else cargo v prepare-verus fi cargo install --git https://github.com/microsoft/verismo/ --rev $VERISMO_REV verus-rustc -curl --proto '=https' --tlsv1.2 -LsSf https://github.com/verus-lang/verusfmt/releases/download/v0.4.3/verusfmt-installer.sh | sh +curl --proto '=https' --tlsv1.2 -LsSf https://github.com/verus-lang/verusfmt/releases/download/v0.5.0/verusfmt-installer.sh | sh sudo apt-get install build-essential ninja-build libclang-dev diff --git a/verify_external/src/lib.rs b/verify_external/src/lib.rs index ea2338b73..124c602a2 100644 --- a/verify_external/src/lib.rs +++ b/verify_external/src/lib.rs @@ -18,9 +18,6 @@ // Add spec for convert traits pub mod convert; -#[cfg(verus_keep_ghost)] -include!("vstd.verus.rs"); - use builtin_macros::*; verus! { diff --git a/verify_external/src/vstd.verus.rs b/verify_external/src/vstd.verus.rs deleted file mode 100644 index 18e7dabc7..000000000 --- a/verify_external/src/vstd.verus.rs +++ /dev/null @@ -1,43 +0,0 @@ -// SPDX-License-Identifier: MIT OR Apache-2.0 -// -// Copyright (c) Microsoft Corporation -// -// Author: Ziqiao Zhou -use vstd::prelude::*; -verus! { - -#[verifier::external_fn_specification] -pub fn ex_map U>(a: Option, f: F) -> (ret: Option) - requires - a.is_some() ==> call_requires(f, (a.unwrap(),)), - ensures - ret.is_some() == a.is_some(), - ret.is_some() ==> call_ensures(f, (a.unwrap(),), ret.unwrap()), -{ - a.map(f) -} - -} // verus! -macro_rules! num_specs { - ($uN:ty) => { - verus! { - pub open spec fn saturating_add(x: $uN, y: $uN) -> $uN { - if x + y > <$uN>::MAX { - <$uN>::MAX - } else { - (x + y) as $uN - } - } - - #[verifier::external_fn_specification] - #[verifier::when_used_as_spec(saturating_add)] - pub fn ex_saturating_add(x: $uN, y: $uN) -> (res: $uN) - ensures res == saturating_add(x, y) - { - x.saturating_add(y) - } - } - }; -} - -num_specs! {usize} From 0f633aa3eec4bcfe3dfc8eca126b73803cce2f8a Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Thu, 31 Oct 2024 13:14:11 -0700 Subject: [PATCH 5/8] Update verification document. Add example & links about verus Signed-off-by: Ziqiao Zhou --- .cargo/config.toml | 1 - Documentation/docs/developer/VERIFICATION.md | 123 ++++++++++++++----- 2 files changed, 93 insertions(+), 31 deletions(-) diff --git a/.cargo/config.toml b/.cargo/config.toml index 35342d8f2..079d24ee4 100644 --- a/.cargo/config.toml +++ b/.cargo/config.toml @@ -13,5 +13,4 @@ rustflags = [ ] [alias] -vfmt = "run-script vfmt" # Format verus codes verify = "v build --features verus" diff --git a/Documentation/docs/developer/VERIFICATION.md b/Documentation/docs/developer/VERIFICATION.md index ff646f139..e81a09832 100644 --- a/Documentation/docs/developer/VERIFICATION.md +++ b/Documentation/docs/developer/VERIFICATION.md @@ -1,12 +1,12 @@ # VERIFICATION -Formal verification is done via [Verus](https://github.com/verus-lang/verus). -To run verification, you need to setup the verification tools in order to run +Formal verification is done via [Verus](https://github.com/verus-lang/verus). +To execute verification, ensure you have set up the necessary tools to run `cargo verify`. ## Setup -Run the following commands to install verus and cargo-verify. +Run the following commands to install Verus tools. ``` cd svsm @@ -22,15 +22,16 @@ cd svsm/kernel cargo verify ``` -By default, it only verifies the current crate. +By default, it only verifies the current crate (`cargo verify` is an alias of `cargo v --features verus`), while using spec/proof from external crates. To verify all external crates, run `cargo v --features verusall` -### Pass verus arguments for verification. -For debugging purposes, it may be helpful to pass additional Verus arguments. -You can specify extra arguments using environmental variable -{crate}_{lib/bin}_VERUS_ARGS to a specific crate -{crate} or VERUS_ARGS to all crates. +### Pass verus arguments for verification + +For debugging purposes, it is helpful to pass additional Verus arguments. +You can specify extra arguments using the environmental variable +{crate}_{lib/bin}_VERUS_ARGS for a specific crate +{crate} or VERUS_ARGS for all crates. **Examples** @@ -43,11 +44,9 @@ You can specify extra arguments using environmental variable * Compiles a crate while only verifying address module in svsm crate: ``` - svsm_lib_VERUS_ARGS="--verify-module address" cargo verify + svsm_lib_VERUS_ARGS="--verify-module address --verify-function VirtAddr::new" cargo verify ``` - - ### Build without verification ``` @@ -55,28 +54,92 @@ cd svsm/kernel cargo build ``` -## Developing specification and proof +All Verus-related annotations, specifications, and proofs are ignored. -While Verus allows you to write specifications and proofs in Rust, it's -beneficial to use the verus!{} macro for a more concise, mathematical syntax -similar to Dafny, F*, and Coq. To get started, be sure to read the [Verus -Tutorial](https://verus-lang.github.io/verus/guide/overview.html) +## Verification Plan + +- [x] Set up verification as an experimental development. +- [ ] Verify SVSM kernel protocol (similar to [VeriSMo](https://github.com/microsoft/verismo)) + - [ ] Allocator + - [ ] Page table + - [ ] Protocol +- [ ] Verifying other security-critical components. + +## Verification Development + +To enable verification, developers need to add annotations in executable Rust +and to write specification and proofs in ghost mode. ### Development Guidelines -* Minimize annotations inside executable Rust. -* For a module `x`, define code-related specification and proof in `x.verus.rs` . -* Codes wrapped in verus!{} macro could be formatted via verusfmt. - ./script/vfmt.sh triggers verusfmt for `*.verus.rs` -* Use external specification and proofs from +* Code Collaboration: Unverified and verified code can co-exist. See [SVSM VeriSMo meeting](https://github.com/coconut-svsm/governance/blob/main/Meetings/Data/verismo-10-23-2024-talk.pdf) for more details. +* Minimize Annotations: Keep simple annotations in executable Rust, by defining + complicated specifications in spec functions and group proofs. +* Specification and Proof Structure: For each module `x`, define code-related + specification and proof in `x.verus.rs` . +* Code Formatting: Use `cargo fmt` for excutable Rust. Codes wrapped in verus!{} + macro could be formatted via verusfmt. Run `./script/vfmt.sh` to format + `*.verus.rs` +* Reusing spec/proof: Use external specification and proofs from [vstd](https://verus-lang.github.io/verus/verusdoc/vstd/) when possible. -* When verifying with functions/structs/traits from external crates, define - specifications in `verify_external/` if `vstd` does not provide. -* Expensive and reusable proofs are stored in `verify_proof/` if `vstd` does not - provide. - -``` -cd svsm -cargo vfmt +* Specifications for dependencies (external crates): If functions, structs, or + traits from external crates lack specifications from vstd, define their + specifications in `verify_external/`. +* Performance: Store expensive and reusable proofs in `verify_proof/` if not + provided by `vstd`. The `svsm/build.rs` sets `rlimit=1`, while + `verify_proof/build.rs` sets `rlimit=4`, helping developers decide when they + need more proof engineering to run verification within minutes. + +### Annotation in Executable Rust + +* #[verus_verify]: Indicates the item is Verus-aware. +* #[verus_verify(external_body)]: Indicates the item is Verus-aware, but marks the function body as uninterpreted by the verifier. +* #[verus_verify(external)]: Instructs Verus to ignore the item. By default, items are treated as #[verus_verify(external)]. +* #[requires(x,y,z)]: Specifies preconditions to a function. +* #[ensures(|ret: RetType| [x,y,z])]: Specifies postconditions to a function. +* #[invariant(x,y,z)]: Specifies loop invariant. +* proof!{...}: Inserts proofs to help solver to avoid false positives or improve + performance. You can also add assert(..) inside proof macro to statically + check assertions. + +For example, + +```rust + +use vstd::prelude::*; +#[verus_verify] +trait A: Sized { + #[requires(m > 0)] + #[ensures(|ret: usize| 0 <= ret < m )] + fn op(self, m: usize) -> usize; +} + +#[verus_verify] +impl A for usize { + // Failed postcondition. + fn op(self, m: usize) -> usize { + self + } +} + +#[verus_verify] +impl A for u64 { + // Verified. + fn op(self, m: usize) -> usize { + (self % (m as u64)) as usize + } +} ``` + +### Developing specification and proof (Verification developers) + +While Verus allows you to write specifications and proofs in Rust, it's +beneficial to use the verus!{} macro for a more concise, mathematical syntax +similar to Dafny, F*, and Coq. To get started, be sure to read the [Verus +Tutorial](https://verus-lang.github.io/verus/guide/overview.html). To find +examples about recursive proof, quantifier, traits, pointers, type invariant, or +other advanced usage, please refer to [Verus +Tests](https://github.com/verus-lang/verus/tree/main/source/rust_verify_test/tests) +and [Verus +Examples](https://github.com/verus-lang/verus/tree/main/source/rust_verify/example). From 6ef53266ec63e40a95a73cd6177d0672c4f5bc7f Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Wed, 30 Oct 2024 13:19:22 -0700 Subject: [PATCH 6/8] Remove verify.yml. Do not run CI for verification. Signed-off-by: Ziqiao Zhou --- .github/workflows/verify.yml | 56 ------------------------------------ 1 file changed, 56 deletions(-) delete mode 100644 .github/workflows/verify.yml diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml deleted file mode 100644 index 00f319d89..000000000 --- a/.github/workflows/verify.yml +++ /dev/null @@ -1,56 +0,0 @@ -name: Verification - -on: - workflow_dispatch: - pull_request: - branches: [ "verify" ] - -env: - CARGO_TERM_COLOR: always - -jobs: - check: - name: Verification Check - runs-on: ubuntu-latest - steps: - - name: Checkout - uses: actions/checkout@v3 - - - name: fetch verus via metadata - run: | - source ./scripts/vpath.sh - echo "VERUS_PATH=$(echo $VERUS_PATH)" >> $GITHUB_ENV - - - uses: Swatinem/rust-cache@v2 - with: - cache-directories: ${{ env.VERUS_PATH }}/source/target-verus - workspaces: | - ${{ github.workspace }} -> target - ${{ env.VERUS_PATH }}/source -> target - ${{ env.VERUS_PATH }}/tools/vargo -> target - - - name: Install specified rust toolchain - uses: actions-rs/toolchain@v1 - with: - toolchain: nightly-2023-12-22 - target: x86_64-unknown-none - profile: minimal - - - name: Install verus toolchains - run: ./scripts/vinstall.sh - - - name: Verify svsm with verus - run: cargo verify - working-directory: kernel - - - name: Verify extra proof libs with verus - run: cargo verify - working-directory: verify_proof - - - name: Build without verifying - run: cargo build - working-directory: kernel - - - name: Format rust code - run: verusfmt --check `find ./ -name *.verus.rs` - From cb630bec923520b36dc8acb097010a062b8230a3 Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Tue, 12 Nov 2024 13:14:06 -0800 Subject: [PATCH 7/8] Remove verify warnings on triggers & avoid scripts from internet. * Upgrade verus to avoid warn in global size * Install verusfmt via cargo install Signed-off-by: Ziqiao Zhou --- Cargo.lock | 12 ++++++------ Cargo.toml | 6 +++--- scripts/vinstall.sh | 13 +++++++++---- verify_proof/src/bits.verus.rs | 2 +- 4 files changed, 19 insertions(+), 14 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index e49d79a19..3f4cd93a7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -172,12 +172,12 @@ dependencies = [ [[package]] name = "builtin" version = "0.1.0" -source = "git+https://github.com/verus-lang/verus?rev=31a272f#31a272f54dd2cce746eb64c54b05be0f825deddf" +source = "git+https://github.com/verus-lang/verus?rev=943ba63#943ba63e0a33b668f840f8e0cb0b6e4d59759a8e" [[package]] name = "builtin_macros" version = "0.1.0" -source = "git+https://github.com/verus-lang/verus?rev=31a272f#31a272f54dd2cce746eb64c54b05be0f825deddf" +source = "git+https://github.com/verus-lang/verus?rev=943ba63#943ba63e0a33b668f840f8e0cb0b6e4d59759a8e" dependencies = [ "prettyplease_verus", "proc-macro2", @@ -784,7 +784,7 @@ dependencies = [ [[package]] name = "prettyplease_verus" version = "0.1.15" -source = "git+https://github.com/verus-lang/verus?rev=31a272f#31a272f54dd2cce746eb64c54b05be0f825deddf" +source = "git+https://github.com/verus-lang/verus?rev=943ba63#943ba63e0a33b668f840f8e0cb0b6e4d59759a8e" dependencies = [ "proc-macro2", "syn_verus", @@ -958,7 +958,7 @@ dependencies = [ [[package]] name = "state_machines_macros" version = "0.1.0" -source = "git+https://github.com/verus-lang/verus?rev=31a272f#31a272f54dd2cce746eb64c54b05be0f825deddf" +source = "git+https://github.com/verus-lang/verus?rev=943ba63#943ba63e0a33b668f840f8e0cb0b6e4d59759a8e" dependencies = [ "indexmap", "proc-macro2", @@ -1047,7 +1047,7 @@ dependencies = [ [[package]] name = "syn_verus" version = "1.0.95" -source = "git+https://github.com/verus-lang/verus?rev=31a272f#31a272f54dd2cce746eb64c54b05be0f825deddf" +source = "git+https://github.com/verus-lang/verus?rev=943ba63#943ba63e0a33b668f840f8e0cb0b6e4d59759a8e" dependencies = [ "proc-macro2", "quote", @@ -1213,7 +1213,7 @@ checksum = "442887c63f2c839b346c192d047a7c87e73d0689c9157b00b53dcc27dd5ea793" [[package]] name = "vstd" version = "0.1.0" -source = "git+https://github.com/verus-lang/verus?rev=31a272f#31a272f54dd2cce746eb64c54b05be0f825deddf" +source = "git+https://github.com/verus-lang/verus?rev=943ba63#943ba63e0a33b668f840f8e0cb0b6e4d59759a8e" dependencies = [ "builtin", "builtin_macros", diff --git a/Cargo.toml b/Cargo.toml index de2c67080..8cb6587fb 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -54,9 +54,9 @@ zerocopy = { version = "0.8.2", features = ["alloc", "derive"] } packit = { git = "https://github.com/coconut-svsm/packit", version = "0.1.1" } # Verus repos -builtin = { git = "https://github.com/verus-lang/verus", rev ="31a272f", default-features = false } -builtin_macros = { git = "https://github.com/verus-lang/verus", rev ="31a272f", default-features = false } -vstd = { git = "https://github.com/verus-lang/verus", rev ="31a272f", features = ["alloc"], default-features = false } +builtin = { git = "https://github.com/verus-lang/verus", rev ="943ba63", default-features = false } +builtin_macros = { git = "https://github.com/verus-lang/verus", rev ="943ba63", default-features = false } +vstd = { git = "https://github.com/verus-lang/verus", rev ="943ba63", features = ["alloc"], default-features = false } # Verification libs verify_proof = { path = "verify_proof", default-features = false } diff --git a/scripts/vinstall.sh b/scripts/vinstall.sh index 1c6673c7b..e5861503c 100755 --- a/scripts/vinstall.sh +++ b/scripts/vinstall.sh @@ -1,13 +1,18 @@ #!/bin/bash -VERISMO_REV=5186244 +VERISMO_REV=9864eac cargo install --git https://github.com/microsoft/verismo/ --rev $VERISMO_REV cargo-v builtin=`cargo metadata --format-version 1 | jq -r '.packages[] | select(.name == "builtin_macros") | .targets[].src_path'` verus=`dirname $builtin`/../../../source/target-verus/release/verus if [ -f ${verus} ]; then echo "verus (${verus}) is already built" else - cargo v prepare-verus + # build the verus using the source code from builtin/vstd defined in + # Cargo.toml so that the verus lib and tool are compatible. + cargo v prepare-verus fi + +# verus-rustc as a wrapper to call verus with proper rustc flags. cargo install --git https://github.com/microsoft/verismo/ --rev $VERISMO_REV verus-rustc -curl --proto '=https' --tlsv1.2 -LsSf https://github.com/verus-lang/verusfmt/releases/download/v0.5.0/verusfmt-installer.sh | sh -sudo apt-get install build-essential ninja-build libclang-dev + +# verus formatter +cargo install --git https://github.com/verus-lang/verusfmt --rev v0.5.0 diff --git a/verify_proof/src/bits.verus.rs b/verify_proof/src/bits.verus.rs index 6c6f0b77b..fdc914052 100644 --- a/verify_proof/src/bits.verus.rs +++ b/verify_proof/src/bits.verus.rs @@ -248,7 +248,7 @@ macro_rules! bit_shl_values { pub broadcast proof fn $pname() ensures #( - N < $styp::BITS ==> ($one << N) == POW2_VALUE!(N), + N < $styp::BITS ==> #[trigger]($one << N) == POW2_VALUE!(N), )* { #(assert($one << N == POW2_VALUE!(N)) by(compute_only);)* From b306bbdf8aa3eb9a6c9362fbf66d1fea21f59355 Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Tue, 12 Nov 2024 17:08:06 -0800 Subject: [PATCH 8/8] Add license for scripts. * Remove vpath.sh since it is only used in verify.yml CI Signed-off-by: Ziqiao Zhou --- scripts/vfmt.sh | 8 ++++++++ scripts/vinstall.sh | 7 +++++++ scripts/vpath.sh | 4 ---- 3 files changed, 15 insertions(+), 4 deletions(-) delete mode 100755 scripts/vpath.sh diff --git a/scripts/vfmt.sh b/scripts/vfmt.sh index e2b668127..e7d7229ab 100755 --- a/scripts/vfmt.sh +++ b/scripts/vfmt.sh @@ -1,3 +1,11 @@ +#!/bin/bash +# SPDX-License-Identifier: MIT OR Apache-2.0 +# +# Copyright (c) Microsoft Corporation +# +# Author: Ziqiao Zhou +# A script to format code inside verus macro. + for f in `find ./ -type f -name "*.verus.rs"` do output=$(verusfmt $f $@ 2>&1) diff --git a/scripts/vinstall.sh b/scripts/vinstall.sh index e5861503c..511b77a27 100755 --- a/scripts/vinstall.sh +++ b/scripts/vinstall.sh @@ -1,4 +1,11 @@ #!/bin/bash +# SPDX-License-Identifier: MIT OR Apache-2.0 +# +# Copyright (c) Microsoft Corporation +# +# Author: Ziqiao Zhou +# A script to install verus tools + VERISMO_REV=9864eac cargo install --git https://github.com/microsoft/verismo/ --rev $VERISMO_REV cargo-v builtin=`cargo metadata --format-version 1 | jq -r '.packages[] | select(.name == "builtin_macros") | .targets[].src_path'` diff --git a/scripts/vpath.sh b/scripts/vpath.sh deleted file mode 100755 index 54ccf5668..000000000 --- a/scripts/vpath.sh +++ /dev/null @@ -1,4 +0,0 @@ -builtin=`cargo metadata --format-version 1 | jq -r '.packages[] | select(.name == "builtin_macros") | .targets[].src_path'` -verus=`dirname $builtin`/../../../ -verus=`realpath $verus` -export VERUS_PATH=$verus