distributed_verification/
kani_list.rs

1use crate::{ProofKind, Result, SerFunction};
2use eyre::ContextCompat;
3use indexmap::{IndexMap, IndexSet};
4use serde::{Deserialize, Serialize};
5use std::{collections::HashMap, process::Command};
6
7/// Output of `kani list` command.
8#[derive(Debug, Serialize, Deserialize, Clone)]
9#[serde(rename_all = "kebab-case")]
10pub struct KaniList {
11    pub kani_version: String,
12    pub file_version: String,
13    pub standard_harnesses: IndexMap<String, IndexSet<String>>,
14    pub contract_harnesses: IndexMap<String, IndexSet<String>>,
15    pub contracts: IndexSet<ContractedFunction>,
16    pub totals: Total,
17}
18
19#[derive(Debug, Serialize, Deserialize, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
20pub struct ContractedFunction {
21    pub function: String,
22    pub file: String,
23    pub harnesses: Vec<String>,
24}
25
26#[derive(Debug, Serialize, Deserialize, Clone)]
27#[serde(rename_all = "kebab-case")]
28pub struct Total {
29    pub standard_harnesses: usize,
30    pub contract_harnesses: usize,
31    pub functions_under_contract: usize,
32}
33
34/// Get kani list and check if it complies with Vec<SerFunction>.
35pub fn check(file: &str, v_ser_fun: &[&SerFunction]) {
36    let list = get_kani_list(file).unwrap();
37    check_proofs(&list, v_ser_fun).unwrap();
38}
39
40/// Run `kani list` on single rust file.
41pub fn get_kani_list(rs_file_path: &str) -> Result<KaniList> {
42    // kani list -Zlist -Zfunction-contracts --format=json file.rs
43    let args = ["list", "-Zlist", "-Zfunction-contracts", "--format=json", rs_file_path];
44    let output = Command::new("kani").args(args).output()?;
45    assert!(
46        output.status.success(),
47        "Failed to run `kani list -Zlist -Zfunction-contracts --format=json {rs_file_path}`:\n{}",
48        std::str::from_utf8(&output.stderr).unwrap()
49    );
50
51    // read kani-list.json
52    read_kani_list("kani-list.json")
53}
54
55/// Read a kani-list.json
56pub fn read_kani_list(kani_list_path: &str) -> Result<KaniList> {
57    let _span = debug_span!("read_kani_list", kani_list_path).entered();
58    let file_json = std::fs::File::open(kani_list_path)?;
59    Ok(serde_json::from_reader(file_json)?)
60}
61
62/// Check if all proofs matches in kani-list.json and SerFunctions.
63pub fn check_proofs(list: &KaniList, v_ser_fun: &[&SerFunction]) -> Result<()> {
64    // sanity check
65    let totals = &list.totals;
66    {
67        let len = v_ser_fun.len();
68        let total = totals.standard_harnesses + totals.contract_harnesses;
69        ensure!(
70            len == total,
71            "The length of Vec<SerFunction> is {len}, but total {total} proofs in kani list."
72        );
73    }
74    {
75        let len = list.standard_harnesses.values().map(|s| s.len()).sum::<usize>();
76        let total = totals.standard_harnesses;
77        ensure!(
78            len == total,
79            "Found {len} standard proofs, but kani list reports {total} of them."
80        );
81    }
82    {
83        let len = list.contract_harnesses.values().map(|s| s.len()).sum::<usize>();
84        let total = totals.contract_harnesses;
85        ensure!(
86            len == total,
87            "Found {len} contract proofs, but kani list reports {total} of them."
88        );
89    }
90
91    let map: HashMap<_, _> = v_ser_fun
92        .iter()
93        .enumerate()
94        .map(|(idx, f)| ((&*f.file, &*f.name), (idx, f.proof_kind)))
95        .collect();
96
97    // check all standard proofs are in distributed-verification json
98    for (path, proofs) in &list.standard_harnesses {
99        for proof in proofs {
100            let key = (path.as_str(), proof.as_str());
101            map.get(&key).with_context(|| {
102                format!(
103                    "The standard proof {key:?} exists in kani list, \
104                     but not in distributed-verification JSON."
105                )
106            })?;
107        }
108    }
109
110    // check all contract proofs are in distributed-verification json
111    for (path, proofs) in &list.contract_harnesses {
112        for proof in proofs {
113            let key = (path.as_str(), proof.as_str());
114            map.get(&key).with_context(|| {
115                format!(
116                    "The contract proof {key:?} exists in kani list, \
117                     but not in distributed-verification JSON."
118                )
119            })?;
120        }
121    }
122
123    // double check
124    for (&(path, proof), &(_, kind)) in &map {
125        let harnesses = match kind {
126            Some(ProofKind::Standard) => &list.standard_harnesses[path],
127            Some(ProofKind::Contract) => &list.contract_harnesses[path],
128            None => continue,
129        };
130        harnesses.get(proof).with_context(|| {
131            format!(
132                "The {kind:?} proof {harnesses:?} exists in \
133                     distributed-verification JSON, but not in kani list."
134            )
135        })?;
136    }
137
138    Ok(())
139}
distributed_verification/kani_list.rs

distributed_verification/
kani_list.rs
