---
tags: prusti, prusti-student-projects
---

# Prusti PW project: IDE improvements

Mondays at 11:00-12:00, 26. 9. 2022 - (6 months)

in prusti-dev
- `prusti-server`
- `prusti-contracts/prusti-specs`
- `prusti-viper/src/encoder/mir/specifications`

## Task overview

### Flowistry-related

- ~~[Flowistry](https://github.com/willcrichton/flowistry)~~

- Selective verification: select function in the source, verify only that method
- Declare an extern spec for the selected call ~~(might require using Flowistry etc to map a selected span -> call `DefId`)~~

fn main() {
    let m = HashMap::new();
    m.get(&5); // <- declare extern_spec for this call
}

#[extern_spec]
impl<K, V, S> HashMap<K, V, S>
where
    K: Eq + ::std::hash::Hash,
    S: BuildHasher,
{
    // ... contract
    pub fn get<Q: ?Sized>(&self, k: &Q) -> Option<&V>
    where
        K: Borrow<Q>,
        Q: Hash + Eq;
}

- ~~Map position in source code to position in Viper file? Would be useful for us, but I don't know if we can get more granularity than methods…~~

### Quantifier-related

- Map quantifiers from Rust to Viper to Z3 and back
- Report quantifier instantiations
- Report chosen quantifier triggers

### Other

- Counterexample reporting: I think we can use "inlay hints" to report counterexample values rather than the current error notes
- More robustness in general (did the dependencies download? interrupted download? rustup version? prusti version? etc)

## Tasks (Joseph)

- [x] (Joseph) Map quantifiers from Rust to Viper to Z3 and back
- [x] (Joseph) Report quantifier instantiations
- [x] (Joseph) Do not report SIGKILL as a crash
- [x] (Joseph) Differentiate between compilation errors and verification errors, e.g. in the status bar
- [x] (Joseph) Report chosen quantifier triggers (if possible easily)

## Tasks (Cedric)

- [x] (Cedric) Selective verification
- [x] (Cedric) Declare an extern spec for the selected call
- [ ] multiple bounds on a single generic
- [ ] default types?
- [x] (Cedric) Report per-method verification times
- [x] (Cedric) Indicate which functions are even verified
- [x] (Cedric) Update snippets for more Prusti annotations (not yet for pledges)
- [x] (Cedric) Mark currently cached methods in the IDE
- [x] (Cedric) Show contract on hover via "peek definition"

---

## Minutes, more tasks, etc

### 2022-09-16

- for next time
- set up Overleaf, initial draft of project description based on the tasklist

### 2022-10-17: new tasks

- Show (abbreviated?) contract on hover
- Indicate which functions are even verified (see green checkmarks in Dafny extension)

### 2022-10-31: new tasks

- Rerun Prusti if `Prusti.toml` was saved

### 2022-12-19: client/server architecture

- VS Code
- running
- Prusti Assistant extension
- (also spawns `prusti-server`)
- invoking as a process
- `prusti-client`
- multiple blocking HTTP requests with Viper ASTs/methods
-> potential refactor: long polling HTTP requests for async reports
- `prusti-server`
- invokes via JNI
- Silicon/Viper