# elicitation_verus
Verus formal verification proofs for [`elicitation`] contract types.
This crate contains **proof functions** for every contract type in the
elicitation framework using [Verus] — a Rust verification tool that uses
Z3 as its SMT back-end and supports explicit `requires`/`ensures` contracts,
executable specifications (`spec fn`), and ghost variables, all written
directly in Rust syntax inside a `verus! { … }` macro block.
> **Note:** This crate is excluded from the Cargo workspace and requires a
> separate Verus toolchain installation. It produces no compiled library
> output — only verification artifacts.
## What Verus does
Verus performs *unbounded* symbolic verification: given a function annotated
with a precondition (`requires`) and a postcondition (`ensures`), it
translates the code to its own VIR (Verus Intermediate Representation),
then passes the resulting SMT obligations to Z3. Unlike bounded model
checking, this is not limited by loop depth or input size — the proof holds
for all mathematically possible inputs satisfying the precondition.
```rust
verus! {
pub fn new(value: i32) -> (result: Result<I32Positive, ValidationError>)
ensures
value > 0 ==> (result matches Ok(p) && p.value == value),
value <= 0 ==> (result matches Err(_)),
{
if value > 0 { Ok(I32Positive { value }) }
else { Err(ValidationError::NotPositive) }
}
}
```
Z3 discharges both obligations — the success branch and the failure branch
— for every possible `i32`, giving an unbounded proof of constructor
correctness.
## Proof patterns
### Requires / ensures on constructors
Every contract type has a constructor proof covering both `Ok` and `Err`
outcomes:
```rust
ensures
value > 0 ==> (result matches Ok(p) && p.value == value),
value <= 0 ==> (result matches Err(ValidationError::NotPositiveI32(v)) && v == value),
```
The `==>` (implies) combinator lets each branch of the match be stated as a
separate logical obligation.
### Accessor proofs
Accessor methods carry `ensures` clauses that tie their return value back to
the construction parameter:
```rust
pub fn get(&self) -> (result: i32)
requires self.value > 0,
ensures result == self.value,
```
### Ghost state
Some types carry a `validated: bool` ghost field used purely for proof
bookkeeping — it tracks whether the construction contract was satisfied and
lets Verus reason about compound types without re-proving sub-contracts:
```rust
pub struct VecNonEmpty { pub validated: bool }
pub fn is_validated(&self) -> (result: bool)
ensures result == self.validated,
{ self.validated }
```
### Compositional proofs
Tuple types compose validation flags with logical conjunction, proving that
a pair type is valid exactly when both components are valid:
```rust
pub fn is_validated(&self) -> (result: bool)
ensures result == (self.first_validated && self.second_validated),
```
### Abstraction for external crates
Operations that depend on external crates (regex parsing, UUID construction,
IEEE 754 float semantics, Unicode character properties) are abstracted as
boolean parameters rather than called directly. We prove the *wrapper logic*
without trying to verify the external library:
```rust
// Instead of calling regex::Regex::new(pattern):
pub fn new(compiles: bool) -> (result: Result<RegexValid, ValidationError>)
ensures
compiles ==> (result matches Ok(_)),
!compiles ==> (result matches Err(_)),
```
This is the **castle on cloud** principle applied to Verus: trust the
foundations (external crates), verify the walls (our contract logic).
## Coverage
| `primitives` | `i8`–`i64`, `u8`–`u64`, `f32`, `f64`, `bool`, `char` base proofs |
| `bools` | `BoolTrue`, `BoolFalse` |
| `chars` | `CharAlphabetic`, `CharAlphanumeric`, `CharNumeric` |
| `integers` | `I8`/`I16`/`U8`/`U16` Positive, NonNegative, NonZero |
| `floats` | `F32`/`F64` Positive, NonNegative, Finite |
| `strings` | `StringNonEmpty`, `StringBounded`, `StringNonEmptyBounded` |
| `collections` | `VecNonEmpty`, `VecBounded`, `VecNonEmptyBounded`, `OptionSome`, `ResultOk` |
| `tuples` | `Tuple2`, `Tuple3`, `Tuple4` compositional validity |
| `stdlib_collections` | Generic `Option`, `Result`, 2/3/4-tuple composition |
| `durations` | `DurationPositive` |
| `networks` | `IpPrivate`, `IpPublic`, `IpV4`, `IpV6` |
| `paths` | `PathNonEmpty`, `PathAbsolute`, `PathRelative` |
| `ipaddr_bytes` | `Ipv4Bytes`, `Ipv6Bytes`, private/public classification |
| `macaddr` | `MacAddr` unicast/multicast/universal/local bit patterns |
| `socketaddr` | `SocketAddrV4Bytes`, `SocketAddrV6Bytes`, privileged port classification |
| `utf8` | `Utf8Valid`, `Utf8Bounded` length and validity |
| `pathbytes` | `PathBytes`, `PathAbsolute`, `PathRelative` (Unix) |
| `urlbytes` | `UrlBytes`, `SchemeBytes`, `AuthorityBytes` |
| `regexbytes` | `RegexBytes`, `BalancedDelimiters` |
| `uuid_bytes` | `UuidBytes`, `UuidV4`, `UuidNonNil` |
| `external_types` | `Regex`, `Url`, `Uuid`, `DateTime`, `IP`, `PathBuf`, `Duration`, `serde_json::Value` |
| `datetimes` | `DateTimeUtcAfter`, `DateTimeUtcBefore` |
| `urls` | `UrlValid`, `UrlHttps`, `UrlHttp` |
| `uuids` | `UuidV4`, `UuidNonNil` |
| `regexes` | `RegexValid`, `RegexCaseInsensitive` |
| `values` | `ValueObject`, `ValueArray`, `ValueNonNull` |
## Running the proofs
Install Verus following the [official instructions][verus-install], then
verify the crate directly:
```bash
verus crates/elicitation_verus/src/lib.rs
```
Verus writes intermediate files to a `.verus-log/` directory:
- `.vir` / `-sst.vir` — Verus Intermediate Representation
- `.air` / `-final.air` — Anvil IR passed to Z3
- `.smt2` — SMT-LIB2 queries sent to the solver
- `.smt_transcript` — Z3 interaction log
For failed proofs, `.interp` files contain counterexample models from Z3.
## Integration with the elicitation crate
`elicitation_verus` depends on the main `elicitation` crate with the
`verification` feature enabled:
```toml
[dependencies]
elicitation = { version = "0.8", features = ["verification"] }
```
The main crate defines the contract types; this crate proves their
constructors and accessors are correct. Because verification produces no
compiled output, there is zero runtime overhead — the proofs exist solely
as logical witnesses.
The crate is **excluded from the workspace** (`exclude = [...]` in the root
`Cargo.toml`) because it requires Verus's own modified Rust toolchain and
cannot be built with standard `cargo`.
## Verus vs. Kani vs. Creusot
The elicitation workspace maintains three independent formal verification
back-ends. They address different points on the verification spectrum:
| `elicitation_verus` | [Verus] | Unbounded SMT (Z3) | Complex contracts, ghost variables, composition |
| `elicitation_kani` | [Kani] | Bounded model checking | Memory safety, no-panic, bit-level patterns |
| `elicitation_creusot` | [Creusot] | Deductive (Why3 + SMT) | Functional correctness, loop invariants |
Verus is the natural choice when you need to express rich *logical*
properties — implications, conjunctions over compound types, conditional
postconditions — and want a single self-contained toolchain (no Why3
ecosystem required). Kani is faster for concrete numeric/bit properties.
Creusot shines for loop-heavy algorithms.
A property proved by all three tools independently has been checked by three
completely separate verification paths, providing very high confidence.
## License
Licensed under either of [Apache License 2.0](../../LICENSE-APACHE) or
[MIT License](../../LICENSE-MIT) at your option.
[Verus]: https://verus-lang.github.io/verus/
[verus-install]: https://verus-lang.github.io/verus/guide/getting_started.html
[Kani]: https://model-checking.github.io/kani/
[Creusot]: https://github.com/creusot-rs/creusot
[`elicitation`]: https://crates.io/crates/elicitation