diff --git a/.cargo/config.toml b/.cargo/config.toml index 0777ed2ed..079d24ee4 100644 --- a/.cargo/config.toml +++ b/.cargo/config.toml @@ -11,3 +11,6 @@ rustflags = [ rustflags = [ "-C", "code-model=kernel", ] + +[alias] +verify = "v build --features verus" diff --git a/Cargo.lock b/Cargo.lock index dd58cad3d..3f4cd93a7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -39,9 +39,9 @@ dependencies = [ [[package]] name = "anstream" -version = "0.6.14" +version = "0.6.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "418c75fa768af9c03be99d17643f93f79bbba589895012a80e3452a19ddda15b" +checksum = "23a1e53f0f5d86382dafe1cf314783b2044280f406e7e1506368220ad11b1338" dependencies = [ "anstyle", "anstyle-parse", @@ -54,33 +54,33 @@ dependencies = [ [[package]] name = "anstyle" -version = "1.0.7" +version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "038dfcf04a5feb68e9c60b21c9625a54c2c0616e79b72b0fd87075a056ae1d1b" +checksum = "8365de52b16c035ff4fcafe0092ba9390540e3e352870ac09933bebcaa2c8c56" [[package]] name = "anstyle-parse" -version = "0.2.4" +version = "0.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c03a11a9034d92058ceb6ee011ce58af4a9bf61491aa7e1e59ecd24bd40d22d4" +checksum = "3b2d16507662817a6a20a9ea92df6652ee4f94f914589377d69f3b21bc5798a9" dependencies = [ "utf8parse", ] [[package]] name = "anstyle-query" -version = "1.1.0" +version = "1.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ad186efb764318d35165f1758e7dcef3b10628e26d41a44bc5550652e6804391" +checksum = "79947af37f4177cfead1110013d678905c37501914fba0efea834c3fe9a8d60c" dependencies = [ "windows-sys", ] [[package]] name = "anstyle-wincon" -version = "3.0.3" +version = "3.0.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "61a38449feb7068f52bb06c12759005cf459ee52bb4adc1d5a7c4322d716fb19" +checksum = "2109dbce0e72be3ec00bed26e6a7479ca384ad226efdd66db8fa2e3a38c83125" 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.85", +] + +[[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.85", ] [[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=943ba63#943ba63e0a33b668f840f8e0cb0b6e4d59759a8e" + +[[package]] +name = "builtin_macros" +version = "0.1.0" +source = "git+https://github.com/verus-lang/verus?rev=943ba63#943ba63e0a33b668f840f8e0cb0b6e4d59759a8e" +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.85", ] [[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.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b6a852b24ab71dffc585bcb46eaf7959d175cb865a7152e35b348d1b2960422" +checksum = "5b63caa9aa9397e2d9480a9b13673856c78d8ac123288526c37d7839f2a86990" [[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.85", ] [[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.85", ] [[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]] @@ -710,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" @@ -736,6 +781,15 @@ dependencies = [ "universal-hash", ] +[[package]] +name = "prettyplease_verus" +version = "0.1.15" +source = "git+https://github.com/verus-lang/verus?rev=943ba63#943ba63e0a33b668f840f8e0cb0b6e4d59759a8e" +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=943ba63#943ba63e0a33b668f840f8e0cb0b6e4d59759a8e" +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,14 @@ dependencies = [ "libmstpm", "log", "packit", + "rustc_version", "syscall", "tdx-tdcall", "test", - "zerocopy 0.8.2", + "verify_external", + "verify_proof", + "vstd", + "zerocopy 0.8.7", ] [[package]] @@ -937,15 +1035,37 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.66" +version = "2.0.85" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c42f3f41a2de00b01c0aaad383c5a45241efc8b2d1eda5661812fda5f3cdcff5" +checksum = "5023162dfcd14ef8f32034d8bcd4cc5ddc61ef7a247c024a33e24e1f24d21b56" dependencies = [ "proc-macro2", "quote", "unicode-ident", ] +[[package]] +name = "syn_verus" +version = "1.0.95" +source = "git+https://github.com/verus-lang/verus?rev=943ba63#943ba63e0a33b668f840f8e0cb0b6e4d59759a8e" +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 +1089,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.85", ] [[package]] @@ -1006,7 +1126,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.66", + "syn 2.0.85", ] [[package]] @@ -1026,9 +1146,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 = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" +checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" + +[[package]] +name = "unicode-xid" +version = "0.2.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853" [[package]] name = "universal-hash" @@ -1042,21 +1168,41 @@ 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 = "verify_external" +version = "0.1.0" +dependencies = [ + "builtin", + "builtin_macros", + "vstd", +] + +[[package]] +name = "verify_proof" +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 +1210,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=943ba63#943ba63e0a33b668f840f8e0cb0b6e4d59759a8e" +dependencies = [ + "builtin", + "builtin_macros", + "state_machines_macros", +] + [[package]] name = "wasi" version = "0.11.0+wasi-snapshot-preview1" @@ -1072,18 +1228,18 @@ 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", ] [[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 +1253,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 +1306,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.85", ] [[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.85", ] [[package]] diff --git a/Cargo.toml b/Cargo.toml index 682019d5a..8cb6587fb 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -14,6 +14,9 @@ members = [ "libmstpm", # syscall interface definitions "syscall", + # verification libraries for svsm + "verify_proof", + "verify_external", ] @@ -50,6 +53,15 @@ 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 ="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 } +verify_external = { path = "verify_external", default-features = false } + [workspace.lints.rust] future_incompatible = { level = "deny", priority = 127 } nonstandard_style = { level = "deny", priority = 126 } @@ -81,3 +93,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..e81a09832 --- /dev/null +++ b/Documentation/docs/developer/VERIFICATION.md @@ -0,0 +1,145 @@ +# VERIFICATION + +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 tools. + +``` +cd svsm +./scripts/vinstall.sh +``` + +## Build + +### Build svsm with verification + +``` +cd svsm/kernel +cargo verify +``` + +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 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** + +* Compiles a crate without verifying svsm crate: + + ``` + 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 --verify-function VirtAddr::new" cargo verify + ``` + +### Build without verification + +``` +cd svsm/kernel +cargo build +``` + +All Verus-related annotations, specifications, and proofs are ignored. + +## 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 + +* 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. +* 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). diff --git a/kernel/Cargo.toml b/kernel/Cargo.toml index ca650067e..6be02f5d7 100644 --- a/kernel/Cargo.toml +++ b/kernel/Cargo.toml @@ -37,6 +37,12 @@ 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 } +verify_proof = { workspace = true, optional = true} +verify_external = { workspace = true, optional = true} + [target."x86_64-unknown-none".dev-dependencies] test.workspace = true @@ -47,7 +53,14 @@ mstpm = ["dep:libmstpm"] nosmep = [] nosmap = [] +verus_all = ["vstd", "builtin", "verify_proof/verus", "verify_external/verus"] +verus = ["verus_all", "verify_proof/noverify", "verify_external/noverify"] +noverify = [] + [dev-dependencies] +[build-dependencies] +rustc_version = "0.4" + [lints] workspace = true diff --git a/kernel/build.rs b/kernel/build.rs index 526b10203..692970f76 100644 --- a/kernel/build.rs +++ b/kernel/build.rs @@ -5,9 +5,16 @@ // Author: Joerg Roedel fn main() { + // 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"); @@ -35,4 +42,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=1", + "--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..3a68d4b85 100644 --- a/kernel/src/address.rs +++ b/kernel/src/address.rs @@ -10,12 +10,20 @@ use core::ops; 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; #[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 { @@ -25,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; @@ -99,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 } @@ -197,10 +239,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,21 +253,28 @@ 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)) } /// 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 } #[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 } @@ -235,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()) @@ -249,13 +302,18 @@ 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()) .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 { + proof! {use_type_invariant(self);} VirtAddr::new(self.0 + offset) } @@ -273,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) } @@ -290,15 +349,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 } @@ -306,60 +371,84 @@ 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) } } +#[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] 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] fn from(ptr: *mut T) -> Self { - Self(ptr as InnerAddr) + Self::from(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 { + 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) @@ -367,6 +456,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 new file mode 100644 index 000000000..ca5211e13 --- /dev/null +++ b/kernel/src/address.verus.rs @@ -0,0 +1,230 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou +verus! { + +use vstd::prelude::*; +use verify_external::convert::{FromSpec, from_spec, axiom_from_spec}; + +pub broadcast group sign_extend_proof { + 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_impl_proof { + sign_extend_proof, + 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_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)] +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_sign_bit(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_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 +#[cfg(verus_keep_ghost)] +impl View for VirtAddr { + type V = InnerAddr; + + closed spec fn view(&self) -> InnerAddr { + self.0 + } +} + +impl VirtAddr { + /// Canonical form addresses run from 0 through 00007FFF'FFFFFFFF, + /// and from FFFF8000'00000000 through FFFFFFFF'FFFFFFFF. + #[verifier::type_invariant] + 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 open spec fn is_low(&self) -> bool { + self@ <= VADDR_LOWER_MASK + } + + 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 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.offset() + offset < VADDR_RANGE_SIZE + } + + pub open spec fn const_add_ensures(&self, offset: usize, ret: VirtAddr) -> bool { + &&& 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@ >= other@ + &&& other.is_high() || self.is_low() + } + + // ret is the size of availabe virtual memory between the two addresses. + pub open spec fn sub_ensures(&self, other: Self, ret: InnerAddr) -> bool { + &&& ret == self.offset() - other.offset() + } + + pub open spec fn sub_usize_requires(&self, other: usize) -> bool { + self.offset() >= other + } + + pub open spec fn sub_usize_ensures(&self, other: usize, ret: Self) -> bool { + ret.offset() == self.offset() - other + } +} + +impl FromSpec<*mut T> for VirtAddr { + closed spec fn from_spec(v: *mut T) -> Self { + VirtAddr(sign_extend_spec(v 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/kernel/src/types.verus.rs b/kernel/src/types.verus.rs new file mode 100644 index 000000000..3dcb87dff --- /dev/null +++ b/kernel/src/types.verus.rs @@ -0,0 +1,14 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou +verus! { + +pub broadcast group group_types_proof { + verify_proof::bits::lemma_bit_usize_shl_values, +} + +broadcast use group_types_proof; + +} // verus! diff --git a/scripts/vfmt.sh b/scripts/vfmt.sh new file mode 100755 index 000000000..e7d7229ab --- /dev/null +++ b/scripts/vfmt.sh @@ -0,0 +1,21 @@ +#!/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) +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..511b77a27 --- /dev/null +++ b/scripts/vinstall.sh @@ -0,0 +1,25 @@ +#!/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'` +verus=`dirname $builtin`/../../../source/target-verus/release/verus +if [ -f ${verus} ]; then + echo "verus (${verus}) is already built" +else + # 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 + +# verus formatter +cargo install --git https://github.com/verus-lang/verusfmt --rev v0.5.0 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/verify_external/build.rs b/verify_external/build.rs new file mode 100644 index 000000000..ae3325284 --- /dev/null +++ b/verify_external/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=1", + "--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/verify_external/src/convert.rs b/verify_external/src/convert.rs new file mode 100644 index 000000000..1bbe2f2b7 --- /dev/null +++ b/verify_external/src/convert.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!("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..124c602a2 --- /dev/null +++ b/verify_external/src/lib.rs @@ -0,0 +1,28 @@ +// 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; + +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_proof/Cargo.toml b/verify_proof/Cargo.toml new file mode 100644 index 000000000..bee3b9066 --- /dev/null +++ b/verify_proof/Cargo.toml @@ -0,0 +1,21 @@ +[package] +name = "verify_proof" +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/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/verify_proof/src/bits.rs b/verify_proof/src/bits.rs new file mode 100644 index 000000000..479172526 --- /dev/null +++ b/verify_proof/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/verify_proof/src/bits.verus.rs b/verify_proof/src/bits.verus.rs new file mode 100644 index 000000000..fdc914052 --- /dev/null +++ b/verify_proof/src/bits.verus.rs @@ -0,0 +1,384 @@ +// 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 0..64 { + #(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 ==> #[trigger]($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/verify_proof/src/lib.rs b/verify_proof/src/lib.rs new file mode 100644 index 000000000..cc39bd5bf --- /dev/null +++ b/verify_proof/src/lib.rs @@ -0,0 +1,18 @@ +// SPDX-License-Identifier: MIT OR Apache-2.0 +// +// Copyright (c) Microsoft Corporation +// +// Author: Ziqiao Zhou + +#![no_std] +#![allow(unused_braces)] +#![allow(unexpected_cfgs)] +use builtin_macros::*; + +pub mod bits; + +verus! { + +global size_of usize == 8; + +}